Re: monomorphism is ... ?

[Pierre Weis <Pierre.Weis@inria.fr>]

> >Am I right in thinking that the following holds ?
> >
> >polymorphic  = has type 'a  = for all
> >monomorphic  = has type '_a = exists
> 
> not in the type-theoretic sense of the word. Exists normally refers to
> data abstraction, whereas the '_a here is a "hack" of the ocaml
> interactive environment. As soon as it gets a type, you cannot
> "re"-instantiate it.  SML doesn't have the '_a at all and returns a dummy
> type-variable. I think (but I am not sure about this) that the batch
> compiler doesn't deal with '_a at all. 
> 
> cheers,
> 
> 	Simon

You are right, a '_a type variable cannot be reinstanciated since it
is a type unknown. However, the unknown type variable may be
incrementally refined, as in the following code:

# let f = List.map (fun x -> x);;
val f : '_a list -> '_a list = <fun>
# f [[]];;
- : '_a list list = [[]]
# f;;
- : '_a list list -> '_a list list = <fun>
# f [[[]]];;
- : '_a list list list = [[[]]]
# f;;
- : '_a list list list -> '_a list list list = <fun>

Furthermore, the batch compiler's typechecker being the same as the
toplevel's typechecker, it also handles type unknowns as examplified
by the following module ``Unknowns'':

(* File unknowns.mli (empty interface) *)

(* File unknowns.ml *)
let f = List.map (fun x -> x);;
let g l = f [l];;
let h = f;;
let i l = f [[l]];;
let j = f;;

$ocamlc -i unknowns.ml 
val f : '_a list list -> '_a list list
val g : '_a list -> '_a list list
val h : '_a list list -> '_a list list
val i : '_a -> '_a list list
val j : '_a list list -> '_a list list

You may think that the batch compiler does not handle unknowns since
it very often reports an error in case of unknowns: there is a
restriction on unknowns in modules. It states that no unknown can
escape the scope of the current module (since it is impossible to keep
track of further instanciations). So the compiler reports on error if
you try to define a global with unknowns.

For instance if we export all the identifiers of the module Unknowns
the compilation fails:

$rm unknowns.mli
$ocamlc unknowns.ml 
File "unknowns.ml", line 1, characters 8-29:
The type of this expression, '_a list list -> '_a list list,
contains type variables that cannot be generalized

This behavior of the Caml typechecker is along the lines of the value
polymorphism restriction. When typing

let ident = expr

the type of expr is not generalized if expr is an application (no for
all added for the type variables appearing in expr). In this case, the
unknown type variables remain in the type of «ident». That's exactly
what you see when using the toplevel system.

We could have choosen to systematically report an error when some type
unknown escapes in the type of a global ident. We chose instead to let
unknown appear in types, since it is simpler and it is useful in some
cases. For instance, you can now define a mutable value with an
unknown type variable, and let the system infer the appropriate
instanciation when updating the mutable value.

Instead of 
let x = (ref [] : int list ref);;

You simply define a reference to the empty list and go on:

let x = ref [];;
val x : '_a list ref = {contents=[]}

x := 1 :: !x;;
- : unit = ()

x;;
- : int list ref = {contents=[1]}

This is also usable in modules. It is provably safe, and in my opinion
it is convenient.

Best regards,

Pierre Weis

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