Re: [Caml-list] Type variables (was: Odd Type Checking Problem)

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: Markus Mottl <markus@oefai.at>
> On Thu, 07 Feb 2002, Alain Frisch wrote:
> > Actually, I feel myself somewhat confused with implicit introduction and
> > scoping of type variables.
> > 
> > These one are refused:
> > 
> > let f (x : 'a) = let module M = struct exception X of 'a end in ();;
> > let f (x : 'a) = let module M = struct type t = 'a end in ();;
> [snip]
> > Is there a way to use a type variable such as the 'a above to define
> > types in a local structure ?
> 
> This issue has already popped up in the past. See, for example:
> 
>   http://caml.inria.fr/archives/200107/msg00223.html
> 
> There is unfortunately no way (yet) to use type variables in the way
> shown above. When there is a type variable in a type definition, the type
> checker will look for a binding at the level of the type definition,
> not any further (I hope this explanation comes close to what is really
> happening).

This is actually worse than that: the interaction between let module
and type annotations in an expression is not well defined.

Here is an example of that:

# let f x (y : 'a) = (x : 'a);;
val f : 'a -> 'a -> 'a = <fun>
# let f x (y : 'a) = let module M = struct let z = 1 end in (x : 'a);;
val f : 'a -> 'b -> 'a = <fun>

Basically, what happens is that you forget all type annotations
everytime you type anything inside a module. So what you believed to
be a related use of 'a is actually a completely different type
variable.
This should probably be corrected: at least restore original binding
of type variables when exiting a module.

> Are there any plans to lift this restriction? This would e.g. allow using
> polymorphic types in functor arguments that expect monomorphic instances,
> because the free variable could be bound in an outer scope. For instance,
> one could create "polymorphic" sets of elements with the already existing
> Set-implementation.

Interesting point. It looks like it could work locally. Notice however
that you wouldn't be able to to return such a set from the scope of
the let module. So basically you've not not earned a lot: just the
capacity to hide the fact you're calling a functor inside your
function. Currently you would have to make your function into a functor.

Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr