From: Xavier Leroy <xavier@Theory.Stanford.EDU>
To: mael@id.dth.dk (Martin Elsman)
Cc: caml-list@margaux.inria.fr
Subject: Re: Documentation for the type-checker for Caml Light
Date: Tue, 1 Mar 1994 11:45:03 -0800 (PST) [thread overview]
Message-ID: <9403011945.AA24974@Thelonius.Stanford.EDU> (raw)
In-Reply-To: <199403011535.QAA06835@idfs3.id.dth.dk> from "Martin Elsman" at Mar 1, 94 04:35:27 pm
> 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
next prev parent reply other threads:[~1994-03-02 14:09 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
1994-03-01 15:35 Martin Elsman
1994-03-01 19:45 ` Xavier Leroy [this message]
1994-03-02 14:37 ` Didier Remy
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=9403011945.AA24974@Thelonius.Stanford.EDU \
--to=xavier@theory.stanford.edu \
--cc=caml-list@margaux.inria.fr \
--cc=mael@id.dth.dk \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox