Re: [Caml-list] Polymorphic variant as a witness?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

> > * other solution: put everything inside a function, so that the
> >   type variable is still generalizable after typing the function.
> 
> In that case, the witness remains invisible, doesn't it?

No, the idea is to give the witness as argument to the function, so
that its type is inferred and generalized.
Of course this means that no side effects will occur until the
function is called, so the semantics is preserved.
And this way you can combine several such functions later by passing
the same witness to all of them.

Something like:

let touch (x:[> ] as 'a) (y:'a) = () 

let m1 w =
  let rec f1 ... = ... touch `A w ...
  and f2 ... = ... touch `B w ...
  in
  let r1 = ...
  and r2 = ...
  in
  (f1, f2, r1, f2)

let m2 w (f1, f2, r1, r2) =
  let rec f3 ... = ...
  in 
  let r3 = ...
  in
  (f3, r3)

let m1_then_m2 w = m2 w (m1 w)

These modules encoded as functions are combined in something close to
monadic style, but inside them you can just use your trick with
"touch w", with no need to sequence the witness. By the way, since w
is a function argument, it doesn't need to be of type "[> ..] ref"
here.

Note that the above approach is not going to be very precise.
If you share directly w, then m1 will have type [> `A | `B] -> ...
independently of whether f1 and f2 are actually used.
If you want to be more precise, you must parameterize functions with
witnesses.

let m1 w =
  let rec f1 w ... = ... touch `A w ...
  and f2 w ... = ... touch `B w ...
  in
  ...

This way you get a bit more control on when to merge effects.
Thanks to let polymorphism, it looks like you just get the same power
as with an effect system (you're still limited a bit by the value
restriction).

Also, you may have realized that the above code just uses functions to
do that same thing as functors. Functors would be syntactically nicer,
but they wouldn't let you infer the type of w, which is the whole
point. If getting data out of tuples proves to be a pain, you could
also return an immediate object.

Cheers,

Jacques Garrigue