Re: Weak types ?

From: Simon Helsen (helsen@informatik.uni-tuebingen.de)
Date: Wed Feb 04 1998 - 20:07:51 MET


Date: Wed, 4 Feb 1998 20:07:51 +0100 (MET)
From: Simon Helsen <helsen@informatik.uni-tuebingen.de>
To: Pierre CASTERAN <Pierre.Casteran@labri.u-bordeaux.fr>
Subject: Re: Weak types ?
In-Reply-To: <199802031546.QAA21882@scrasmeustache.labri.u-bordeaux.fr>
Message-Id: <Pine.A32.3.96.980204195102.14334N-100000@marvin>

> I suppose the following problem concerns "weak" types, but i don't see
> the reason (I have no assignment at all in this definitions !)
>
> let toto =
> let id x = x
> in id id;;
> (*
> val toto : '_a -> '_a = <fun>
> ^ ^
>
> why not " 'a " ?
>
> *)

the problem is due to the polymorphic application (id id). Caml uses
something which is called "value polymorphism", a restriction which is
also adopted in SML'97, although Caml still allows you to use this
pseudo-polymorphic function (i.e. it allows you to instantiate the
poly-variable once and then fixing it). It has absolutely nothing to do
with the use of assignments or anything alike. As far as I know, a
variable (e.g. toto) can only be given a (true) polymorphic type scheme if
the exp (e.g. id id) is "non-expansive" (Standard ML terminology).
However, every application *is* expansive. This is just a syntactic
restriction which definitely avoids the known problems with polymorphic
references, but is indeed sometimes a bit to restrictive, although it
appears to be rarely a problem in practice. This scheme is now also
adopted in SML because other more semantic based approaches (like tracing
references etc.) turned out to be ugly and could mess up the signatures of
modules.

> toto 5;;
> (* ok *)
>
> toto (fun z -> z);;
>
> (*
> This expression has type 'a -> 'a but is here used with type int
> *)

Exactly. The pseudo-poly var. has been already instantiated with an
integer and is now fixed to that, meaning it can't be used otherwise. This
exactly avoids the type-problems in case of references. Note that in SML
your definition of toto would be refused in the first place.

cheers,

Simon

----------------------- Simon Helsen ------------------------
-- Wilhelm-Schickard-Institut fuer Informatik --
-- Arbeitsbereich Programmierung (PU) --
-- Universitaet Tuebingen, Germany --
-------------------------------------------------------------
-- http://www-pu.informatik.uni-tuebingen.de/users/helsen/ --



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