Oddness with recursive polymorphic variants

Oddness with recursive polymorphic variants

[Jeremy Yallop]

I have two polymorphic variant types, as follows:

   type f = [`A | `B of f]
   type g = [f | `C]

Next, I have a function from f to g:

   let s1 : f -> g = function
     | `A -> `A
     | `B b -> b

Sadly, the compiler rejects this:

     Characters 57-58:
       | `B b -> b;;
                 ^
   This expression has type f but is here used with type g
   The first variant type does not allow tag(s) `C

The error message seems odd.  Why should it matter that g has more tags 
than f, since every value of f is a value of g (by definition)?

Indeed, minor variants of the function are accepted.  Both of the 
following are ok:

   let s2 : f -> g = function
     | `A -> `A
     | `B (#f as b) -> b

   let s3 : f -> g = function
     | `A -> `A
     | `B ((`A|`B _) as b) -> b

Am I missing something, or is this a bug?

Thanks,

Jeremy.

Re: [Caml-list] Oddness with recursive polymorphic variants

[Nils Gesbert]

Jeremy Yallop <j.d.yallop@sms.ed.ac.uk> a écrit :

» I have two polymorphic variant types, as follows:
» 
»    type f = [`A | `B of f]
»    type g = [f | `C]
» 
» Next, I have a function from f to g:
» 
»    let s1 : f -> g = function
»      | `A -> `A
»      | `B b -> b
» 
» Sadly, the compiler rejects this:
» 
»      Characters 57-58:
»        | `B b -> b;;
»                  ^
»    This expression has type f but is here used with type g
»    The first variant type does not allow tag(s) `C
» 
» The error message seems odd.  Why should it matter that g has more tags 
» than f, since every value of f is a value of g (by definition)?

f is indeed a subtype of g, but to forget the precise type of b (that is, forget the information that it cannot contain the tag `C), you have to use explicit coercion, i. e. :

  let s1 : f -> g = function
     | `A -> `A
     | `B b -> (b :> g)

Re: [Caml-list] Oddness with recursive polymorphic variants

[Nils Gesbert]

Alternatively, you may also coerce directly the function :
let s1 = ((function `A -> `A | `B b -> b) :> f -> g)

Re: [Caml-list] Oddness with recursive polymorphic variants

[Jeremy Yallop]

Thanks for all the replies.  My current understanding is as follows:

Given the types

    type f = [`A]
    type g = [f | `C]

then the following function is not acceptable

    let k (x:f) = (x:g)

because f and g are not unifiable: they are "closed rows" with different 
fields.  There are a number of ways to "open" the row, however:

    let k (#f as x:f) = (x:g)

This one is acceptable because the pattern "#f" means "an open row that 
includes all the tags in f".  (That's its type on the rhs, anyway.  The 
pattern (and the function) will accept exactly those tags in the type 
"f").  The type annotation on the parameter doesn't affect the type of 
"x", although the compiler does check that the type of the annotation 
and of the pattern can be unified.  The case where all the tags (only 
one in this case) are enumerated is treated identically:

    let k (`A as x:f) = (x:g)

Finally, the explicit coercion (:>).  Like the acceptable patterns, this 
"opens" the row, allowing it to be unified with "g" (or, indeed, with 
any other row type whose tag parameters don't clash with those of "f").

How does that sound?

Jeremy.

Oddness with recursive polymorphic variants

[Jeremy Yallop]

I have two polymorphic variant types, as follows:

   type f = [`A | `B of f]
   type g = [f | `C]

Next, I have a function from f to g:

   let s1 : f -> g = function
     | `A -> `A
     | `B b -> b

Sadly, the compiler rejects this:

     Characters 57-58:
       | `B b -> b;;
                 ^
   This expression has type f but is here used with type g
   The first variant type does not allow tag(s) `C

The error message seems odd.  Why should it matter that g has more tags 
than f, since every value of f is a value of g (by definition)?

Indeed, minor variants of the function are accepted.  Both of the 
following are ok:

   let s2 : f -> g = function
     | `A -> `A
     | `B (#f as b) -> b

   let s3 : f -> g = function
     | `A -> `A
     | `B ((`A|`B _) as b) -> b

Am I missing something, or is this a bug?

Thanks,

Jeremy.

Re: [Caml-list] Oddness with recursive polymorphic variants

[Luc Maranget]

> I have two polymorphic variant types, as follows:
> 
>   type f = [`A | `B of f]
>   type g = [f | `C]
> 
> Next, I have a function from f to g:
> 
>   let s1 : f -> g = function
>     | `A -> `A
>     | `B b -> b
> 
> Sadly, the compiler rejects this:
> 
>     Characters 57-58:
>       | `B b -> b;;
>                 ^
>   This expression has type f but is here used with type g
>   The first variant type does not allow tag(s) `C
> 
> The error message seems odd.  Why should it matter that g has more tags 
> than f, since every value of f is a value of g (by definition)?


I cannot really explain why it matters, but I can supply a minimal (?) example

type f = [`A ]
type g = [f | `C]

let k (x:f) = (x:g);;
               ^
This expression has type f but is here used with type g
The first variant type does not allow tag(s) `C


-- Luc

Re: [Caml-list] Oddness with recursive polymorphic variants

[Michael Wohlwend]

On Thursday 04 May 2006 19:10, Luc Maranget wrote:
> > I have two polymorphic variant types, as follows:
> >
> >   type f = [`A | `B of f]
> >   type g = [f | `C]
> >
> > Next, I have a function from f to g:
> >
> >   let s1 : f -> g = function
> >
> >     | `A -> `A
> >     | `B b -> b
> >
> > Sadly, the compiler rejects this:
> >
> >     Characters 57-58:
> >       | `B b -> b;;
> >

that may be too complicated, but it works :-)

type 'a f = [`A | `B of 'a];;
type 'a g = ['a f | `C];;

let s1 (p : 'a f) : 'a g = match p with
  `A -> `A
  | `B b -> b;;

# s1 (`B (`B `A));;
- : 'a g as 'a = `B `A


 Michael


-- 
C offers you enough rope to hang yourself.
C++ offers a fully equipped firing squad, a last cigarette and
a blindfold.

Re: [Caml-list] Oddness with recursive polymorphic variants

[brogoff]

On Thu, 4 May 2006, Luc Maranget wrote:
> I cannot really explain why it matters, but I can supply a minimal (?) example
>
> type f = [`A ]
> type g = [f | `C]
>
> let k (x:f) = (x:g);;
>                ^
> This expression has type f but is here used with type g
> The first variant type does not allow tag(s) `C

Not enough polymorphism, the error message seems clear

type 'a h = 'a constraint 'a = [> `A];;
let k (x : 'a h) = (x : g)

works.

-- Brian

Re: [Caml-list] Oddness with recursive polymorphic variants

[Jeremy Yallop]

brogoff wrote:
> On Thu, 4 May 2006, Luc Maranget wrote:
> 
>>I cannot really explain why it matters, but I can supply a minimal (?) example
>>
>>type f = [`A ]
>>type g = [f | `C]
>>
>>let k (x:f) = (x:g);;
>>               ^
>>This expression has type f but is here used with type g
>>The first variant type does not allow tag(s) `C
> 
> 
> Not enough polymorphism, the error message seems clear
> 
> type 'a h = 'a constraint 'a = [> `A];;
> let k (x : 'a h) = (x : g)

Thanks for the reply.  That doesn't seem to be what I want, though.  The 
input to k should have type 'f'.  The output should have type 'g'.  Your 
'k' can be called with values that don't match type 'f':

    # k `C;;
    - : g = `C

The following does what I want:

    let k (#f as x:f) = (x:g)

I'd like to understand why it behaves differently from the following:

    let k (x:f) = (x:g)

Jeremy.

Re: [Caml-list] Oddness with recursive polymorphic variants

[brogoff]

On Thu, 4 May 2006, Jeremy Yallop wrote:
> Thanks for the reply.  That doesn't seem to be what I want, though.  The
> input to k should have type 'f'.  The output should have type 'g'.  Your
> 'k' can be called with values that don't match type 'f':
>
>     # k `C;;
>     - : g = `C
>
> The following does what I want:
>
>     let k (#f as x:f) = (x:g)
>
> I'd like to understand why it behaves differently from the following:
>
>     let k (x:f) = (x:g)

Right, others have shown that you can do what you want with a coercion. The
problem is that you are using exact types ("[" rather than "[>" ) and there
is a mismatch of exact types. ":" is not a coercion, it just tells the type
that should be there. ":>" coerces. x is not of type g, but it can be coerced to
g.

-- Brian

Re: [Caml-list] Oddness with recursive polymorphic variants

[Luc Maranget]

> > I'd like to understand why it behaves differently from the following:
> >
> >     let k (x:f) = (x:g)
> 
> Right, others have shown that you can do what you want with a coercion. The
> problem is that you are using exact types ("[" rather than "[>" ) and there
> is a mismatch of exact types. ":" is not a coercion, it just tells the type
> that should be there. ":>" coerces. x is not of type g, but it can be coerced to
> g.
> 

Indeed,

# let kk (x:f) = (x :> g);;
val kk : f -> g = <fun>

Thanks,

--Luc