From mboxrd@z Thu Jan 1 00:00:00 1970 Received: by pauillac.inria.fr; Wed, 2 Mar 94 15:09:17 +0100 Received: from margaux.inria.fr by pauillac.inria.fr; Tue, 1 Mar 94 20:45:36 +0100 Received: from concorde.inria.fr by margaux.inria.fr, Tue, 1 Mar 94 20:45:32 +0100 Received: from Thelonius.Stanford.EDU (Thelonius.Stanford.EDU [36.28.0.15]) by concorde.inria.fr (8.6.5/8.6.5) with SMTP id UAA26210 for ; Tue, 1 Mar 1994 20:45:31 +0100 Received: by Thelonius.Stanford.EDU (5.61/25-theory-eef) id AA24974; Tue, 1 Mar 94 11:45:04 -0800 From: Xavier Leroy Message-Id: <9403011945.AA24974@Thelonius.Stanford.EDU> Subject: Re: Documentation for the type-checker for Caml Light To: mael@id.dth.dk (Martin Elsman) Date: Tue, 1 Mar 1994 11:45:03 -0800 (PST) Cc: caml-list@margaux.inria.fr In-Reply-To: <199403011535.QAA06835@idfs3.id.dth.dk> from "Martin Elsman" at Mar 1, 94 04:35:27 pm Content-Type: text Sender: weis@pauillac.inria.fr > 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 references. > 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 ftp.inria.fr:INRIA/Projects/cristal/Xavier.Leroy). > 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