Date: Wed, 22 Jan 1997 09:17:50 -0800
From: gurr@snap.med.ge.com (David Gurr)
Message-Id: <199701221717.JAA16849@swag.med.ge.com>
To: caml-list@inria.fr
Subject: Re: ergonomie du compilateur
I think that the biggest difficulty people have with types in ML is
conceptual. Neither Lisp/Scheme nor C/C++/Pascal programmers are
likely to understand types and their role in ML. Maybe the following
pedantic exposition would make things clearer. A ML system has two
separate things that effectively execute code;ie two "interpreters". The
first is the value interpreter and is more or less the same as a Scheme
interpreter, the second is the type interpreter and can be thought of
as a very specialized Prolog interpreter. When you enter a line of
code on a ML interpreter, it is executed by *both* interpreters. The
type interpreter does a unification driven search for the type of the
code. And the value interpreter does a reduction driven simplification
for the value of the code. The single bit of subtilety is that the
value interpreter actually interpretes the code after it has been
rewritten with explicit types (using the type determined by the type
interpreter).
This points out three areas of conceptual difficulty. Because type
inference is done at compile time, and because it resembles "type
checking" a la C etc, people often think of type checking as being part
of parsing rather than as part of the execution of the program.
Because types are trivial in the common languages, people do not
recognize that types are as integral to the meta-level execution of ML
(which takes place during compilation) as values are to the
iso/base-level execution of ML (which takes place during runtime).
Because logic programming is not common, people are befuddled by ML
type inference.
So what could the compiler do to help? I suppose that it would be
possible for the toplevel to throw you into a prolog like interpreter
when it hits a type error. You could enter type variables and it would
reply with the type that is the value of the type variable, etc. There
would be a predefined predicate |- for type judgements. This would make
the metalevel type inference as accessable and perhaps as understandable
as the baselevel values.
-D
My apologies for no French version, you would rather not find out how
bad my French is.
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:09 MET