Closed variants, type constraints and module signature

Philippe Veber

Jacques Garrigue

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:   (:) 
From:  Jacques Garrigue <garrigue@m...> 
Subject:  Re: [Camllist] Closed variants, type constraints and module signature 
From: Philippe Veber <philippe.veber@googlemail.com> > 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 : ... >> > 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 ? Yes, this is exactly the point I was trying to make. But it was a good idea to post it here: this is a rather technical point, I don't read the beginnerlist usually, and your explanation is probably better than mine. >> 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 ! This indeed works, but I'm not sure of why you insist on defining a constrained type. What is wrong with writing directly the following? module type S = sig val v : u val f : [< u] > [`a] end Constrained types have their uses, but I find them often confusing as the type variable you write is not really a type variable. Question of taste. Jacques Garrigue