Re: [Caml-list] Comments on type variables

[Francois Pottier <francois.pottier@inria.fr>]

   
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