From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id OAA06901 for caml-redistribution; Thu, 23 Jan 1997 14:10:59 +0100 (MET) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA17724 for ; Wed, 22 Jan 1997 18:18:59 +0100 (MET) Received: from gemsgw.med.ge.com ([192.88.230.10]) by nez-perce.inria.fr (8.7.6/8.7.3) with SMTP id SAA11903 for ; Wed, 22 Jan 1997 18:18:52 +0100 (MET) Received: from gemed.med.ge.com (gemed.med.ge.com [3.7.12.4]) by gemsgw.med.ge.com (8.6.12/8.6.12) with ESMTP id LAA25442 for ; Wed, 22 Jan 1997 11:16:29 -0600 Received: from nmri.med.ge.com (snap.med.ge.com [3.57.196.10]) by gemed.med.ge.com (8.6.12/8.6.12) with SMTP id LAA12396; Wed, 22 Jan 1997 11:18:27 -0600 Received: from swag.med.ge.com by nmri.med.ge.com (4.1/SMI-4.1) id AA15643; Wed, 22 Jan 97 09:23:07 PST Received: by swag.med.ge.com (SMI-8.6/SMI-SVR4) id JAA16849; Wed, 22 Jan 1997 09:17:50 -0800 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 Cc: gurr@snap X-Sun-Charset: US-ASCII Sender: weis 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.