Typing problem

Typing problem

[Daniel Bünzli]

Hello,

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] 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 ?

Regards,

Daniel

Re: [Caml-list] Typing problem

[Jacques Garrigue]

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

Re: [Caml-list] Typing problem

[Daniel Bünzli]

Le 19 mars 06 à 12:21, Jacques Garrigue a écrit :

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

I thought about that but I wanted to avoid the need to go through  
constructors functions (or values à la bigarray). Maybe I'll simply  
statically check a little less. It's a tradeoff.


Le 19 mars 06 à 15:23, j h woodyatt a écrit :

> However, 'b is concrete in your example, so-- if it's fully  
> representative of your code-- you could just do this, and you would  
> still have only one type parameter:
>
> type 'a t = [ `A of 'a | `B of [ `U1 ] ]
>   constraint 'a = [< u ]

This won't work because, as I said, I use 'a to express static  
constraints about the value stored in the constructors therefore 'a  
must be [`U1] whenever a `B is constructed and this is not enforced  
by this definition. Having more parameters is not an option either.

Thanks to both of you for your input.

Daniel