Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: Documentation for the type-checker for Caml Light
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Xavier Leroy <xavier@T...>
Subject: Re: Documentation for the type-checker for Caml Light
> The code of Caml Light is not 'just' the
> Hindley/Milner/Robinson kind of thing, though there are
> similarities.

There are a number of tricks in the efficient implementation of type
inference that you won't find in Hindley, Milner, nor Robinson, indeed.
Some are described in Cardelli's paper "Basic polymorphic type-checking",
Science of computer programming, 8(2). 

The Caml Light typechecker also uses "levels" on type variables to
implement generalization efficiently. This folklore trick is described
in Weis and Leroy's book "Le langage Caml" (in French, unfortunately),
and also (but much more abstractly) in some publications by Didier
Remy. I believe Didier is on the list, so maybe he can provide more

> What are dangerous type variables

A type analysis to prevent polymorphic mutable structures (e.g.
polymorphic references), similar in purpose to imperative type
variables but much superior in my opinion. See my POPL 91 paper and
my PhD thesis (available on

> and why does
> the type checker include two unification algorithms?

I don't understand what you're alluding to. Where is the second algorithm?

- Xavier Leroy