Re: Weak types ?

From: Pierre Weis (Pierre.Weis@inria.fr)
Date: Tue Feb 10 1998 - 19:51:08 MET


From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <199802101851.TAA16030@pauillac.inria.fr>
Subject: Re: Weak types ?
In-Reply-To: <Pine.A32.3.96.980209172455.14334H-100000@marvin> from Simon Helsen at "Feb 9, 98 05:31:32 pm"
To: helsen@informatik.uni-tuebingen.de
Date: Tue, 10 Feb 1998 19:51:08 +0100 (MET)

> yes, but it doesn't say much on the history of the problem. The Paulson
> book does, but doesn't mention Caml. What I wonder is when Caml
> adopted value polymorphism, what system was used before that and whether
> the INRIA researchers did seek for (perhaps alternative) solutions
> themselves. In the Standard ML community, the standard reference to this
> problem is a paper of Andrew Wright (1995)...
>
> Simon
>
> ----------------------- Simon Helsen ------------------------
> -- Wilhelm-Schickard-Institut fuer Informatik --
> -- Arbeitsbereich Programmierung (PU) --
> -- Universitaet Tuebingen, Germany --
> -------------------------------------------------------------
> -- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --

I've no time to describe old type systems that have been adopted in
ancient versions of Caml since 1984. Let's just say that they were not
that satisfactory, since we start studying the subject and writing
papers in 1990:

1991:

----
Publications available online
Xavier Leroy, Pierre Weis. "Polymorphic type inference and
assignment". Proceedings POPL 91.

This paper present a new approach to the polymorphic typing of data accepting in-place modification in ML-like languages. This approach is based on restrictions over type generalization, and a refined typing of functions. The type system given here leads to a better integration of imperative programming style with the purely applicative kernel of ML. In particular, generic functions that allocate mutable data can safely be given fully polymorphic types. We show the soundness of this type system, and give a type reconstruction algorithm.

1992: ----- Publications available online Xavier Leroy. "Polymorphic typing of an algorithmic language". Research report 1778, INRIA, 1992. (PhD thesis. French original also available.)

The polymorphic type discipline, as in the ML language, fits well within purely applicative languages, but does not extend naturally to the main feature of algorithmic languages: in-place update of data structures. Similar typing difficulties arise with other extensions of applicative languages: logical variables, communication channels, continuation handling. This work studies (in the setting of relational semantics) two new approaches to the polymorphic typing of these non-applicative features. The first one relies on a restriction of generalization over types (the notion of dangerous variables), and on a refined typing of functional values (closure typing). The resulting type system is compatible with the ML core language, and is the most expressive type systems for ML with imperative features proposed so far. The second approach relies on switching to ``by-name'' semantics for the constructs of polymorphism, instead of the usual ``by-value'' semantics. The resulting language differs from ML, but lends itself easily to polymorphic typing. Both approaches smoothly integrate non-applicative features and polymorphic typing.

1993: ----- Le langage Caml, Pierre Weis et Xavier Leroy, InterEditions, Paris 1993, ISBN 2-7296-0493-6. The restriction of let polymorphism to non expansive expressions is described in pages 389-390.

1995: ----- The restriction of polymorphism to non expansive expressions is implemented in version Caml-Light 0.7.

The paper you cited by Andrew Wright is still a good reference, and he really has proved that this approach could be feasible for ML-like languages, whereas we (the Caml team) were looking for an extension of the ML type-system that would preserve the typing of purely functional programs. Xavier gets such an extension in his thesis, but the type system was more complex (and more difficult to implement efficiently) than the simple ``non expansive'' restriction. Furthermore, this restriction is easy to understand and trivial to prove correct. Thus it has been adopted in the Caml compilers.

By the way, there is no ``weak type variables'' in the Caml type system. The '_a notation denotes pure type variables that have not been universally quantified in a type scheme. There is no quantification over these '_a type variables, as opposed to weak type variables.

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:13 MET