Closed variants, type constraints and module signature

Philippe Veber

Jacques Garrigue
 Philippe Veber

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:  20100514 (21:33) 
From:  Philippe Veber <philippe.veber@g...> 
Subject:  Re: [Camllist] Closed variants, type constraints and module signature 
2010/5/14 Jacques Garrigue <garrigue@math.nagoyau.ac.jp> > From: Philippe Veber <philippe.veber@googlemail.com> > > > I'd like to define a type with a variable that is constrained to accept > only > > polymorphic variant types included in a given set of tags. That is how I > > believed one should do : > > > > Objective Caml version 3.11.2 > > > > # type 'a t = 'a constraint 'a = [< `a  `b ];; > > type 'a t = 'a constraint 'a = [< `a  `b ] > > > > But I stumbled upon the following problem, when trying to use this > > definition > > > > > > # module type S = sig > > val v : 'a t > > end;; > > module type S = sig val v : [< `a  `b ] t end > > > > # module I : S = struct > > let v = `a > > end;; > > > > Error: Signature mismatch: > > Modules do not match: sig val v : [> `a ] end is not included in S > > Values do not match: > > val v : [> `a ] > > is not included in > > val v : [< `a  `b ] t > > > > Does anyone know why the definition of module I is rejected ? And if this > is > > the intended behavior, why does the following work ? > > > > # let v : 'a t = `a > > ;; > > val v : [< `a  `b > `a ] t = `a > > But it doesn't really work! > More precisely, the type [< `a  `b > `a ] t is an instance of 'a t, > not 'a t itself, an a module interface should give a type at most as > general as the implementation. > Right, I understand now there are two different mechanisms at hand here : in the module case, the type annotation for v is a specification, in the let binding case, it is a constraint. Seems like my question was better suited to beginners list ! Just to be sure : module I is rejected because v should have type 'a t for all 'a satisfying the constraint 'a = [< `a  `b ], that contain in particular [ `b ], which is incompatible with the type of v. Is that correct ? > > In your case, you should simply write > > type t = [`a  `b] > > since you don't know what v may be. > If i absolutely wanted to forbid other tags than `a and `b, while keeping the possibility to manage subtype hierarchies, maybe I could also change the code this way : type u = [`a  `b] type 'a t = 'a constraint 'a = [< u ] module type S = sig val v : u t val f : 'a t > [`a] t end module I : S = struct let v = `a let f _ = v end At least now the interpreter doesn't complain. Many thanks ! Philippe. > > Jacques Garrigue >