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

[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

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.