Re: Weak types ?

[Pierre Weis <Pierre.Weis@inria.fr>]

> 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/