Filter
Top Products
4.3. IMPERATIVE FEATURES 45
4.3.4 Interaction with the type system
While polymorphism works very well for the pure functional core of CAML, it has
unfortunate interactions with some imperative features. For example, consider the
following:
#let l = ref [];;
Then l would seem to have polymorphic type α list ref. In accordance with
the usual rules of let-polymorphism we should be able to use it with two different
types, e.g. first
#l := [1];;
and then
#hd(!l) = true;;
But this isn’t reasonable, because we would actually be writing something as an
object of type int then reading it as an object of type bool. Consequently, some
restriction on the usual rule of let polymorphism is called for where references are
concerned. There have been many attempts to arrive at a sound but convenient
restriction of the ML type system, some of them very complicated. Recently, dif-
ferent versions of ML seem to be converging on a relatively simple method, called
the value restriction, due to Wright (1996), and CAML implements this restriction,
with a twist regarding toplevel bindings. Indeed, the above sequence fails. But the
intermediate behaviour is interesting. If we look at the first line we see:
#let l = ref [];;
l : ’_a list ref = ref []
The underscore on the type variable indicates that l is not polymorphic in
the usual sense; rather, it has a single fixed type, although that type is as yet
undetermined. The second line works fine:
#l := [1];;
it : unit = ()
but if we now look at the type of l, we see that:
#l;;
it : int list ref = ref [1]
The pseudo-polymorphic type has now been fixed. Granted this, it is clear that
the last line must fail:
#hd(!l) = true;;
Toplevel input:
>hd(!l) = true;;
> ^^^^
This expression has type bool,
but is used with type int.
So far, this seems quite reasonable, but we haven’t yet explained why the same
underscored type variables occur in apparently quite innocent purely functional
expressions, and why, moreover, they often disappear on eta-expansion, e.g.