Typing problem

Daniel_Bünzli
 Jacques Garrigue
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060319 (11:20) 
From:  Jacques Garrigue <garrigue@m...> 
Subject:  Re: [Camllist] 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 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