This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

polymorphic variants and recursive functions
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2009-03-25 (21:39) From: Warren Harris Subject: polymorphic variants and recursive functions
```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

```