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

Typing problem
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2006-03-19 (11:20) From: Jacques Garrigue Subject: Re: [Caml-list] Typing problem
```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

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

```