Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: Simon Helsen <helsen@informatik.uni-tuebingen.de>
To: Pierre CASTERAN <Pierre.Casteran@labri.u-bordeaux.fr>
Cc: caml-list@inria.fr
Subject: Re: Weak types ?
Date: Wed, 4 Feb 1998 20:07:51 +0100 (MET)	[thread overview]
Message-ID: <Pine.A32.3.96.980204195102.14334N-100000@marvin> (raw)
In-Reply-To: <199802031546.QAA21882@scrasmeustache.labri.u-bordeaux.fr>

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






  reply	other threads:[~1998-02-05 13:18 UTC|newest]

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1998-02-03 15:46 Pierre CASTERAN
1998-02-04 19:07 ` Simon Helsen [this message]
1998-02-05 16:05 ` Juan J. Quintela
1998-02-09 16:00 ` Pierre Weis
1998-02-09 16:31   ` Simon Helsen
1998-02-10 18:51     ` Pierre Weis

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=Pine.A32.3.96.980204195102.14334N-100000@marvin \
    --to=helsen@informatik.uni-tuebingen.de \
    --cc=Pierre.Casteran@labri.u-bordeaux.fr \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox