Re: [Caml-list] Typing problem

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

From: Daniel Bünzli <daniel.buenzli@epfl.ch>

> I would like to define the following types.
> 
> > type u = [ `U1 | `U2 ]
> >
> > type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]
> 
> t's parameter is used to statically express constraints in other  
> parts of the code. My problem is that
> the constraint on 'a is downgraded to [`U1]

Indeed. Constraints are shared in the whole type, so if 'a has two
 occurences in the type they represent the same type.

> while I would like to be able to write
> 
> > let param : 'a t -> 'a = function (`A v | `B v) -> v
> 
> and get the following typing behaviour.
> 
> > let v = param (`A `U1) (* should type *)
> > let v = param (`A `U2) (* should type *)
> > let v = param (`B `U1) (* should type *)
> > let v = param (`B `U2) (* should not type *)
> 
> Is it possible to express that in ocaml's type system ?

For the above definition of param, this is clearly impossible: a
single variable can have only one (polymorphic) type.
Depending on your concrete problem, there may be a way to encode it in
the type system, but not along the lines you describe here, which are
strongly reminiscent of GADTs.

For instance:
module M : sig
  type 'a t = private [< `A of 'a | `B of 'a]
  val a : ([< `U1 | `U2 ] as 'a) -> 'a t
  val b : [ `U1 ] -> [ `U1 ] t
end = struct
  type 'a t = [`A of 'a | `B of 'a]
  let a x = `A x
  let b x = `B x
end
let param : 'a M.t -> 'a = function (`A v | `B v) -> v

The properties you describe are guaranteed, because all values must be
created through M.a and M.b.

Hope this helps.

Jacques Garrigue