2010/5/14 Jacques Garrigue
<garrigue@math.nagoya-u.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
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