Re: [Caml-list] Closed variants, type constraints and module signature

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Philippe Veber <philippe.veber@googlemail.com>
> 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 :
...
>> > 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 beginner-list 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