[Caml-list] Comments on type variables

[Caml-list] Comments on type variables

[Alain Frisch]

Hello list,

I'd like to make a few comments on the manipulation of type variables
in OCaml. They range from some points that could be worth mentioning
somewhere (FAQ, manual) to "features" that may be considered as bugs,
IMHO.

Feel free to comment, and sorry for this long mail in a random order ...


Generalization of explicit variables
------------------------------------

Explicit variables are generalized only at toplevel let-declarations
(see bug report 1156:
http://caml.inria.fr/bin/caml-bugs/open?id=1156;page=3;user=guest):

# let f x =
    let g (y : 'a) : 'a = y in
    (g x, g (x,x));;
This expression has type 'a * 'a but is here used with type 'a

# let f (x : 'a) : 'a * 'a = (x,x) in (f 1, f true);;
This expression has type bool but is here used with type int

# let a (x : 'a) = x+1 in let b (x : 'a) = x ^ "a" in ();;
This expression has type int but is here used with type string

Variables do not add polymorphism
-----------------------------------

Contrary to the intuition one could have, variable never allow
more polymorphism (exception for polymorphic methods); indeed, they
_restrict_ the polymorphism.

Variables are generalized only on toplevel let-declarations;

# let f x =
    let g (y : 'a) : 'a = y in
    (g x, g (x,x));;
This expression has type 'a * 'a but is here used with type 'a

# let f (x : 'a) : 'a * 'a = (x,x) in (f 1, f true);;
This expression has type bool but is here used with type int


One could expect polymorphic recursion to be allowed when
function interfaces are explicitely given; this is not the case:

# let rec f : 'a -> unit = fun x -> f (x,x);;
This expression has type 'a -> unit but is here used with type
  'a * 'a -> unit
This expression has type 'a * 'a but is here used with type 'a

Actually, "function interfaces are explicitely given" does not mean
anything, as universal quantification can only be infered.

A paragraph in the FAQ is somewhat misleading:

<< Polymorphism appears when we introduce type schemes, that is types
   with universally quantified type variables.
...
   The polymorphism is only introduced by the definition of names during
   a let construct (either local, or global).
>>

The last sentence seems to contradict the first; the programmer doesn't
introduce type schemes.


Variables do not guaranty polymorphism
--------------------------------------

Variables can't be simply used to make the typechecker enforce
polymorphism:

# let f (x : 'a) : 'a = x + 1;;
val f : int -> int = <fun>

We have to rely on the module system:
# module M : sig val f : 'a -> 'a end = struct let f x = x + 1 end;;


Would it be possible to declare variables that have to remain polymorphic
(I don't know how to formalize this; just an idea ...), so as to reject
the following ?

let 'a. f (x : 'a) : 'a = x + 1;;


Variable scoping rules
----------------------

The scoping rules for type variables do not seem uniform.

In a structure, the scope of a variable in an expression is the toplevel
element:

# module M = struct let f (x : 'a)  = x   let g (x : 'a) = x + 1 end;;
module M : sig val f : 'a -> 'a val g : int -> int end

... whereas for objects, the scope is the class definition:

# class o = object method f (x : 'a) = x   method g (x : 'a) = x + 1 end;;
class o : object method f : int -> int method g : int -> int end


Interaction with local modules
------------------------------

Inside a local module, type variables introduced outside the module are
invisible:

# let f (x : 'a) =
    let module M = struct type t = 'a list end in ();;
Unbound type parameter 'a

# let f (x : 'a) =
    let module M = Set.Make(struct type t = 'a end) in ();;
Unbound type parameter 'a


# let f (x : 'a) =
    let module M = struct let g (y : 'a) = y end in M.g 2;;
val f : 'a -> int = <fun>


Type declaration flushes the introduced variables:

# let f (x : 'a) = let module M = struct type t end in (2 : 'a);;
val f : 'a -> int = <fun>

Too bad, when one need such a variable to restrict polymorphism:

# class ['a] o =
  object
    val z = let module M = struct type t end in ()
    method f (x : 'a) : 'a = x
  end;;
Some type variables are unbound in this type:
  class ['a] o : object val x : unit method f : 'b -> 'b end
The method f has type 'a -> 'a where 'a is unbound


Objects
-------

At least it is clear for polymorphic methods where type variables
are introduced.

For class types, the explicit quantification is optional:

# class type o = object method f : 'a -> 'a method g : 'b -> 'b end;;
class type o = object method f : 'a. 'a -> 'a method g : 'b. 'b -> 'b end
# class type ['a] o = object method f : 'a -> 'a method g : 'b -> 'b end;;
class type ['a] o = object method f : 'a -> 'a method g : 'b. 'b -> 'b end
# type 'a t = { x : 'a; y : 'b };;
type 'a t = { x : 'a; y : 'b. 'b; }

BTW, I don't understand the following error message:

# class type o = object method f : 'a -> 'a method g : 'a -> 'a end;;
The method g has type 'a -> 'b but is expected to have type 'c


Also, why are class parameters enclosed in brackets ?
type 'a t = ...
but:
class ['a] t = ...
and not:
class 'a t = ...



'_a variables
-------------

It is not possible to specify "impure" type variables:

# let z = let g y = y in g [];;
val z : '_a list = []
# let z : '_a list = [];;
val z : 'a list = []

Then, how do we specify an interface for the module struct let x = ref [] end ?

#  module M = (struct let x = ref [] end : sig val x : '_a list ref end);;
Signature mismatch:
Modules do not match:
  sig val x : '_a list ref end
is not included in
  sig val x : 'a list ref end
Values do not match:
  val x : '_a list ref
is not included in


Variable name in error message
------------------------------

Error messages would be more readable if they retained (when possible)
variable names:

# let f (a : 'a) (b : 'b list) = b + 1;;
This expression has type 'a list but is here used with type int


-- Alain

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Comments on type variables

[Francois Pottier]

   
Alain,   
  
You are right -- the way type variable names are introduced and managed
is a mess in O'Caml. I (could be wrong but I) don't think much thought 
was ever given to this aspect of the language.

It would be possible to have constructs to introduce such type names,
with lexical scope, at any point within an expression. It would also
be possible to give such names existential or universal meaning. That
is, we could have two expression forms

  exists 'a in e
  forall 'a in e

In both cases, 'a is bound within e. In the former case, it may be
instantiated to any type, while in the latter case, it must remain
polymorphic within e. Currently O'Caml only gives existential meaning
to type variables, as you notice.

I don't think it would be difficult to implement these constructs.
The required machinery, I believe, has already been introduced in
order to support local modules (`let module'). I could be wrong, since
I'm not familiar with O'Caml's typechecker.

> Interaction with local modules
> ------------------------------
>
> Inside a local module, type variables introduced outside the module are
> invisible:
>
> # let f (x : 'a) =
>     let module M = struct type t = 'a list end in ();;
> Unbound type parameter 'a

I would call it a bug, and a very annoying one.

> '_a variables
> -------------
>
> It is not possible to specify "impure" type variables:
>
> # let z = let g y = y in g [];;
> val z : '_a list = []
> # let z : '_a list = [];;
> val z : 'a list = []

There is no such thing as an "impure" type variable. A much cleaner
notion is that of an variable which has been (existentially) bound
somewhere higher up. For instance, instead of writing

> # module M = (struct let x = ref [] end : sig val x : '_a list ref end);;

you could write

  # exists 'a
  # module M = (struct let x = ref [] end : sig val x : 'a list ref end)
   
(I'm using here a toplevel variant of the `exists 'a in e' expression form.)
Here, 'a is explicitly introduced at a certain point, and it is then referenced
in the signature. This looks perfectly fine to me; the only problem is that
it must be clear that 'a is not locally universally quantified in the signature,
and this requires either that universal quantifiers be explicitly listed in
signatures (cumbersome) or that any type names which happen to be in scope
*not* be considered as implicitly locally universally quantified. (I don't
know if I'm being clear enough, but I can clarify if there's interest.)

> Variable name in error message 
> ------------------------------
> 
> Error messages would be more readable if they retained (when possible)
> variable names:
>
> # let f (a : 'a) (b : 'b list) = b + 1;;
> This expression has type 'a list but is here used with type int

The (early prototype) implementation of my toy language does this, at least
for variable names introduced by `forall'. So you can type:

  let forall a b . f (a :: a) (b :: list b) = b + 1
  *** Error: int = list b

It makes sense to keep track of names for variables introduced with universal
meaning, because they will never be unified with some other variable, so they
really have their own identity, in a way. For those variables introduced by with
existential meaning, it would be more problematic; these variables are typically
unified with arbitrary types.
 
These issues are discussed in a recent paper by Peyton Jones and Shields,
which is worth reading; see 

  http://research.microsoft.com/Users/simonpj/papers/scoped-tyvars/

--
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Comments on type variables

[Jacques Garrigue]

From: Alain Frisch <frisch@clipper.ens.fr>

> I'd like to make a few comments on the manipulation of type variables
> in OCaml. They range from some points that could be worth mentioning
> somewhere (FAQ, manual) to "features" that may be considered as bugs,
> IMHO.

At least I'll try to define what is a feature and what is a bug.
In Caml named type variables are handled in the following way:

1) Annotations and coercions
  Type annotations (expr : t), let ... : t = expr, etc are constraints
  applied to inferred types. As such type variables in them have just
  an existential meaning, and they only affect sharing. In an alias
  (t as 'a), 'a is handled as an instance variable.
  Since sharing can happen with any other annotation in the same
  expression, we have to be careful when generalizing types. 
  Caml chooses to only allow generalizing them at the level of the
  whole expression/definition. That is, just like for recursive
  functions, named typed variables inside an expression are
  monomorphic during the typing of this expression.
  If you don't need sharing, you can use "_" as variable name, which
  can be generalized as needed.

2) Type definitions
  All type variables are universally bound in the head of the
  definition.
  They may be constrained, but only explicitly. That is, they are
  quantified universally,
    type 'a t = texp1 constraint 'a = texp2
  meaning
    type t = /\'a < texp2. texp1
   where 'a is bound to be an instance of texp2.

3) Interfaces
  The semantics is the same as for type definitions, but the
  quantification is implicit. Constraint may appear from the use of
  aliases.
    val f : (#c as 'a) -> 'a
  means
    f : /\'a < #c. 'a -> 'a

4) Classes
  They mix features from expressions and types, but the semantics of
  type variables is still the same: they are all bound at the level at
  the level of the class. Inside a definition group the quantification
  is existential, even in interfaces (some constraints may be
  inherited, or appear due to mutual recursion).
  A small discrepancy appears in constraints on the class type:
    class [tvars] c : ctype = cexpr
  Here tvars are shared in both ctype and cexpr, but variables
  appearing in ctype are not shared with does appearing in cexpr.
  I'm not sure of why it is so, but Jerome Vouilon may be able to
  explain.

5) Polymorphic methods
  They form an exception to above rules.
  While their types appear inside class definitions or descriptions,
  they are quantified explicitly at the level of the method:
    method fold : 'a. (t -> 'a -> 'a) -> 'a -> 'a = ...
  In interfaces, the quantification is implicit for newly introduced
  variables
    method fold : (t -> 'a -> 'a) -> 'a -> 'a
  As you can see the exception is in the location of the
  quantification, otherwise they behave like type of  value descriptions.

6) Local modules
  They do not have any specific behaviour, but definitions inside them
  have their type variables quantified independently, as you would
  expect if the module were defined at toplevel.

So there are lots of cases to consider, but I would not describe it as
messy: the basic idea is the scope is the definition, and you cannot
generalize before getting out of the scope.


> Generalization of explicit variables
> ------------------------------------
> 
> Explicit variables are generalized only at toplevel let-declarations
> (see bug report 1156:
> http://caml.inria.fr/bin/caml-bugs/open?id=1156;page=3;user=guest):
> 
> # let f (x : 'a) : 'a * 'a = (x,x) in (f 1, f true);;
> This expression has type bool but is here used with type int

Yes. This is a side-effect of using named variables.

> Variables do not add polymorphism
> -----------------------------------
> 
> Contrary to the intuition one could have, variable never allow
> more polymorphism (exception for polymorphic methods); indeed, they
> _restrict_ the polymorphism.

Yes. This is a property of ocaml that dropping parts of a term can
only improve its polymorphism.

> One could expect polymorphic recursion to be allowed when
> function interfaces are explicitely given; this is not the case:

Yes. Polymorphic recursion is not a magical feature. The existential
semantics of type annotations do not allow to infer anything about
polymorphism from a type annotation.

> A paragraph in the FAQ is somewhat misleading:
> 
> << Polymorphism appears when we introduce type schemes, that is types
>    with universally quantified type variables.
> ...
>    The polymorphism is only introduced by the definition of names during
>    a let construct (either local, or global).
> >>
> 
> The last sentence seems to contradict the first; the programmer doesn't
> introduce type schemes.

The first instance is about types, the second about terms.
In fact, to recover symmetry, the first sentence should probably be
<< Polymorphism appears when we introduce values whose types are
schemes, ... >>

> Variables do not guaranty polymorphism
> --------------------------------------

Fully yes for expressions. Partially yes for type definitions and
interfaces: a variable can only be constrained explicitly. If their is
no constraint on a variable, then it is guaranteed polymorphic.

> We have to rely on the module system:
> # module M : sig val f : 'a -> 'a end = struct let f x = x + 1 end;;

Indeed.

> Would it be possible to declare variables that have to remain polymorphic
> (I don't know how to formalize this; just an idea ...), so as to reject
> the following ?
> 
> let 'a. f (x : 'a) : 'a = x + 1;;

Perfectly possible. But I'm not sure this is sufficient, as we are
also interested by constrained variables.
Maybe allow
  let 'a = texp. f .....

Another way is to integrate it with explicit polymorphism:
  let f : 'a. 'a -> 'a = ...

The real question is what we are going to do with this information.
If we don't use it, then interfaces are probably sufficient.
But we could use it for polymorphism recursion, or first class
polymorphism.

> Variable scoping rules
> ----------------------
> 
> The scoping rules for type variables do not seem uniform.

There are only two exceptions, and they concern classes.
Otherwise the scoping is the single phrase, or a group of phrase
connected by and for term definitions.
Maybe restricting to a single phrase even for simultaneous term
definitions would be more uniform.
 
> In a structure, the scope of a variable in an expression is the toplevel
> element:
> 
> # module M = struct let f (x : 'a)  = x   let g (x : 'a) = x + 1 end;;
> module M : sig val f : 'a -> 'a val g : int -> int end
> 
> ... whereas for objects, the scope is the class definition:
> 
> # class o = object method f (x : 'a) = x   method g (x : 'a) = x + 1 end;;
> class o : object method f : int -> int method g : int -> int end

Yes, a class is not a structure. A class is both an expression and a
type definition, and as such rules common to expressions and type
definitions apply.

> Interaction with local modules
> ------------------------------
> 
> Inside a local module, type variables introduced outside the module are
> invisible:
> 
> # let f (x : 'a) =
>     let module M = struct type t = 'a list end in ();;
> Unbound type parameter 'a

To be expected by the rules above. Functions with local modules are
not functors. 'a is not a type constructor.

> # let f (x : 'a) =
>     let module M = Set.Make(struct type t = 'a end) in ();;
> Unbound type parameter 'a

Idem.

> # let f (x : 'a) =
>     let module M = struct let g (y : 'a) = y end in M.g 2;;
> val f : 'a -> int = <fun>

Side-effect of the independence of members in a structure.
Is there a better semantics?

> Type declaration flushes the introduced variables:
> 
> # let f (x : 'a) = let module M = struct type t end in (2 : 'a);;
> val f : 'a -> int = <fun>

That one is a bug. Bad one. And not immediate to correct, as type
variables are reset all over the place.
Thanks for reporting.

> Too bad, when one need such a variable to restrict polymorphism:

Indeed. If class typing were principal, there would be no such
problem...

> Objects
> -------
> 
> At least it is clear for polymorphic methods where type variables
> are introduced.
> 
> For class types, the explicit quantification is optional:
> 
> # class type o = object method f : 'a -> 'a method g : 'b -> 'b end;;
> class type o = object method f : 'a. 'a -> 'a method g : 'b. 'b -> 'b end
> # class type ['a] o = object method f : 'a -> 'a method g : 'b -> 'b end;;
> class type ['a] o = object method f : 'a -> 'a method g : 'b. 'b -> 'b end

Yes

> # type 'a t = { x : 'a; y : 'b };;
> type 'a t = { x : 'a; y : 'b. 'b; }

That one is not valid any more. In records, one might expect
quantification to be existential (at the level of the whole record),
so it seemed better to make the quantification explicit.

> BTW, I don't understand the following error message:
> 
> # class type o = object method f : 'a -> 'a method g : 'a -> 'a end;;
> The method g has type 'a -> 'b but is expected to have type 'c

Such error message occurs when 'a or 'b is a universal variable, and
you try to unify it with a type variable, against quantification
rules. I must find a way to get better error messages.

This is the case here because 'a is universal after the typing of f,
but is reused (and shared) in the typing of g.

I'm undecided about whether reuse on non-explicitly quantified
universal variables should be allowed. This might be confusing if the
intent was really sharing.

> Also, why are class parameters enclosed in brackets ?
> type 'a t = ...
> but:
> class ['a] t = ...
> and not:
> class 'a t = ...

That's a purely syntactic problem
  class c = [int] t
must be distinguished from
  class c = int t -> ...
at parsing time.

> '_a variables
> -------------
> 
> It is not possible to specify "impure" type variables:
> 
> # let z = let g y = y in g [];;
> val z : '_a list = []
> # let z : '_a list = [];;
> val z : 'a list = []

Indeed, there is no such concept as "impure" variable in input type
expressions. What it should mean is not so clear.

> Then, how do we specify an interface for the module struct let x = ref [] end ?
> 
> #  module M = (struct let x = ref [] end : sig val x : '_a list ref end);;

You must choose a type. Anyway, you will have to choose one at some
time, so why wait?
Note that it is illegal to export a non-generic type variable from a
compilation unit.

> Variable name in error message
> ------------------------------
> 
> Error messages would be more readable if they retained (when possible)
> variable names:
> 
> # let f (a : 'a) (b : 'b list) = b + 1;;
> This expression has type 'a list but is here used with type int

I see. As Francois Pottier pointed out, it's not clear what it would
mean when type variables are only quantified existentially, and can be
merged all over the place.
Note also that the unification algorithm may introduce new type
variables, or create type which were not in the input. Hard to follow
anyway.

Hope this helps.

     Jacques
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Comments on type variables

[Pierre Weis]

Hello Alain,

There already had been a long thread on the subject in this list.

You are right and I guess all the implemnetors aggree with you :
therés a problem with type constraints.

[...]


> A paragraph in the FAQ is somewhat misleading:
> 
> << Polymorphism appears when we introduce type schemes, that is types
>    with universally quantified type variables.
> ...
>    The polymorphism is only introduced by the definition of names during
>    a let construct (either local, or global).
> >>
> 
> The last sentence seems to contradict the first; the programmer doesn't
> introduce type schemes.

The first occurrence of ``we'' means we, type theorists, not we,
actual programmers; in effect, as you said, there is no means for the
Caml programmer to introduce type scheme parameters (or polymorphic
variables as you said). (Except recently for method definitions, and
the notation used could probably be extended to the rest of type
constraints).

You may also have a look at the french version: I may have made a
mistake or oversimplification when translating into english.

[...]
> Also, why are class parameters enclosed in brackets ?
> type 'a t = ...
> but:
> class ['a] t = ...
> and not:
> class 'a t = ...

Ask Yacc! As far as I remember, we needed those explicit brackets to
delimit type parameters of a class from type parameters of types, when
mixing types and classes...

> '_a variables
> -------------
> 
> It is not possible to specify "impure" type variables:

You are right, and it is probably desirable to clarify a lot of examples.

> Variable name in error message
> ------------------------------
> 
> Error messages would be more readable if they retained (when possible)
> variable names:
> 
> # let f (a : 'a) (b : 'b list) = b + 1;;
> This expression has type 'a list but is here used with type int

This is a long standing misfeature of Caml, that is unfortunately not
at all easy to fix.

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Comments on type variables

[Laurent Vibert]

On Fri, 7 Jun 2002, Jacques Garrigue wrote:

> > Interaction with local modules
> > ------------------------------
> > 
> > Inside a local module, type variables introduced outside the module are
> > invisible:
> > 
> > # let f (x : 'a) =
> >     let module M = struct type t = 'a list end in ();;
> > Unbound type parameter 'a
> 
> To be expected by the rules above. Functions with local modules are
> not functors. 'a is not a type constructor.

this has a draw-back : some local modules don't have any valid
signature :
for exemple, what is the signature of the module M ?

let f (x:'a) = 
  let module M = struct let v = x end
  in ...

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners