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

[Philippe Veber <philippe.veber@googlemail.com>]

[-- Attachment #1: Type: text/plain, Size: 2414 bytes --]

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
>
> 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
>

[-- Attachment #2: Type: text/html, Size: 3619 bytes --]