Closed variants, type constraints and module signature

Closed variants, type constraints and module signature

[Philippe Veber]

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

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


Philippe.

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

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

[Jacques Garrigue]

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.

In your case, you should simply write

  type t = [`a | `b]

since you don't know what v may be.

Jacques Garrigue

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

[Philippe Veber]

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

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

[Jacques Garrigue]

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

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

[Philippe Veber]

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

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
>

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

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

[Jacques Garrigue]

From: Philippe Veber <philippe.veber@googlemail.com>
>> 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 = [< ... ])

A typical use would be for objects, particularly when representing
virtual types (see the advanced part of the tutorial, in the reference
manual).
Another application is to use a record notation for type variables:

  type 'r t = .... constraint 'r = < env:'env; loc:'loc; typ:'typ; .. >
 
This way you can share multiple type parameters at once, and even
allow transparent addition of new parameters. This was not the
original goal of constraints, but I find it handy.

I have no immediate example with polymorphic variants, but your
arguments about scalability are valid: in some cases, constraints
allow more compact types. But at a cost.

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

Yes they are constrained type variables.
But the problem is that the constraint is left implicit.

For instance, if somewhere you have defined

  type 'a t constraint 'a = [< `a | `b]

and inside an interface you write

  val f : 'a t -> int

the real meaning is

  val f : [< `a | `b] t -> int

I.e., you are hiding something.

This is not the same thing as type abbreviations, because constraints
are applied from the outside, while abbreviations just have to be
expanded.

Jacques Garrigue