polymorphic variants and recursive functions

polymorphic variants and recursive functions

[Warren Harris]

I stumbled upon a little puzzle that I can't quite work out. I'm  
trying to use polymorphic variants as phantom types and in one  
particular situation involving a polymorphic type with an invariant  
type parameter (Lwt.t) the compiler is unhappy with a set of mutually  
recursive functions. I can appreciate at some level that an invariant  
type parameter will cause the phantom types to become unsatisfied, but  
in this particular case my sense is that they should be satisfiable,  
and feel that I might be overlooking an appropriate coercion. Perhaps  
someone here can lend a hand...


Here's the best I can do at creating a simple example: First, here's  
the case the works... I would like a family of constructors, including  
two higher-order ones, 'arr' and 'obj', such that 'arr' can only be  
constructed from 'obj' instances:

let obj (v:[> `V]) : [`O|`V] = `V
let arr (v:[> `O]) : [`V]    = `V
let v0 : [`V]                = `V

This works as expected:

let ok1 = obj v0
let ok2 = arr (obj v0)
let ok3 = obj (arr (obj v0))

and fails as expected:

let fail1 = arr v0
                   ^^
This expression has type [ `V ] but is here used with type [> `O ]
The first variant type does not allow tag(s) `O

I can now use these constructors in conjunction with some mutually- 
recursive functions (coercions are needed):

let rec eval = function
   | `Arr v -> (eval_arr v : [`V]    :> [> `V])
   | `Obj v -> (eval_obj v : [`V|`O] :> [> `V])
and eval_arr v = arr (eval_obj v)
and eval_obj v = obj (eval v)

although oddly, the coercions don't seem to affect the final type of  
eval:

val eval : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `O | `V ] = <fun>
val eval_arr : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `V ] = <fun>
val eval_obj : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `O | `V ] =  
<fun>



Now the case that doesn't work: Introducing 'a Lwt.t into the above:

open Lwt
let obj (v:[> `V]) : [`O|`V] Lwt.t = return `V
let arr (v:[> `O]) : [`V] Lwt.t    = return `V
let v0 : [`V] Lwt.t                = return `V

let ok1 = v0 >>= obj
let ok2 = v0 >>= obj >>= arr
let ok3 = v0 >>= obj >>= arr >>= obj
(*let fail1 = v0 >>= arr*)

let rec eval = function
   | `Arr v -> (eval_arr v : [`V] Lwt.t    :> [> `V] Lwt.t)
   | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t)
and eval_arr v = eval_obj v >>= arr
and eval_obj v = eval v >>= obj

     | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t)
                  ^^^^^^^^^^
This expression has type [ `O | `V ] Lwt.t but is here used with type
   [ `V ] Lwt.t
The second variant type does not allow tag(s) `O



Any suggestions would be much appreciated,

Warren

Re: [Caml-list] polymorphic variants and recursive functions

[Mauricio Fernandez]

On Wed, Mar 25, 2009 at 02:39:28PM -0700, Warren Harris wrote:
> let rec eval = function
>   | `Arr v -> (eval_arr v : [`V] Lwt.t    :> [> `V] Lwt.t)
>   | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t)
> and eval_arr v = eval_obj v >>= arr
> and eval_obj v = eval v >>= obj
>
>     | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t)
>                  ^^^^^^^^^^
> This expression has type [ `O | `V ] Lwt.t but is here used with type
>   [ `V ] Lwt.t
> The second variant type does not allow tag(s) `O

The Lwt.t type is abstract and invariant since no annotation has been given
for the type variable (you'd need it to be  type +'a t):

# let a : [`O] Lwt.t = return `O;;
val a : [ `O ] Lwt.t = <abstr>
# (a :> [`O | `V] Lwt.t);;
Error: Type [ `O ] Lwt.t is not a subtype of type [ `O | `V ] Lwt.t 
The first variant type does not allow tag(s) `V

In your example, [> `V] Lwt.t  in the second line becomes 
   [`V] Lwt.t,
(the type variable is not covariant) and you cannot do  
   [`V | `O] Lwt.t :> [`V] Lwt.t
in the third line.

Unfortunately, the type variable is in both variant and contravariant position
in the definition of Lwt.t...

-- 
Mauricio Fernandez  -   http://eigenclass.org

Re: [Caml-list] polymorphic variants and recursive functions (caml: to exclusive)

[Warren Harris]

Mauricio,

Thanks for your response...


On Mar 25, 2009, at 4:24 PM, Mauricio Fernandez - mfp@acm.org wrote:

> The Lwt.t type is abstract and invariant since no annotation has  
> been given
> for the type variable (you'd need it to be  type +'a t):
>

...

>
> Unfortunately, the type variable is in both variant and  
> contravariant position
> in the definition of Lwt.t...

Just to be sure I understand you... you're saying due to the  
definition/implementation of Lwt and the fact that the type parameter  
cannot be declared covariant, that what I'm trying to do with phantom  
types just can't work in this case. I was afraid of that. :-(

Warren