2010/5/15 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
>
Well, nothing ! I'm affraid I chose an inappropriate solution to an
irrelevant problem. Initially i just wanted to be sure my polymorphic type
'a t would not be used with funny tags in 'a (I mean tags that have nothing
to do with t). But after all, there is (in my case) no rationale for this.
Second, types may be shorter to write :

val f : 'a t -> int

instead of

val f : [< u] t -> int

or

val f : [< My_type.u ] My_type.t -> int

if in another module. Well, now it's clearer for me it was not such a smart
idea. Your proposal is simpler and more natural.



> Constrained types have their uses,

which are, in brief ? Now I can't see a typical use for closed polymorphic
variant types (I mean types of the form 'a t constraint 'a = [< ... ])

but I find them often confusing as
> the type variable you write is not really a type variable.
>
why isn't it the case ? Aren't they simply type variables restricted to a
finite number of types ?

Anyway, thanks a lot for commenting on my problem !

Philippe.






> Question of taste.
>
> Jacques Garrigue
>