From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: weis
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA13651 for caml-redistribution; Wed, 23 Sep 1998 09:23:32 +0200 (MET DST)
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 TAA15759 for <caml-list@pauillac.inria.fr>; Tue, 22 Sep 1998 19:05:24 +0200 (MET DST)
Received: from welcome.disi.unige.it (welcome.disi.unige.it [130.251.61.111])
	by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id TAA27522;
	Tue, 22 Sep 1998 19:05:22 +0200 (MET DST)
Received: (from leroy@localhost) by welcome.disi.unige.it (8.8.3/8.6.9) id TAA17242; Tue, 22 Sep 1998 19:14:10 +0200
Message-ID: <19980922191410.C17087@welcome.disi.unige.it>
Date: Tue, 22 Sep 1998 19:14:10 +0200
From: Xavier Leroy <leroy@welcome.disi.unige.it>
To: "Pierre CREGUT - FT.BD/CNET/DTL/MSV" <pierre.cregut@cnet.francetelecom.fr>,
        Pierre Weis <Pierre.Weis@inria.fr>
Cc: Simon Helsen <helsen@informatik.uni-tuebingen.de>, caml-list@inria.fr
Subject: Re: polymorphic recursion
References: <Pine.A32.3.96.980922113949.2728U-100000@modas> <199809221506.RAA17926@pauillac.inria.fr> <19980922175023.23586@lsun564>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Mailer: Mutt 0.93.2i
In-Reply-To: <19980922175023.23586@lsun564>; from Pierre CREGUT - FT.BD/CNET/DTL/MSV on Tue, Sep 22, 1998 at 05:50:23PM +0200
Sender: weis

[On the scope and binding location of type variables in type constraints:]

> This has already been solved in the SML standard and even if it is not 
> necessarily easy to understand when formalized, this is quite intuitive :

[SML'90 rule snipped]

Actually, SML'97 adds explicit scoping of type variables if desired.
The syntax is something like

        let 'a val x = ...

(This is from memory, I don't have the '97 Definition here.)
Although those declarations are optional and the old rule is used
if they are omitted, it shows that maybe the old rule is a little too
subtle to be understood by all.

IT is amusing to notice that SML, Caml and Haskell implement three
different semantics for type variables in constraints:
  - SML: bind at "let" enclosing all mentions of the variable
  - Caml: bind at nearest "struct ... let x = ... end";
  - Haskell: bind immediately in type expression itself (I think).

This is one of those little dark spots in ML-style languages that I
hope will be cleaned some day by drastic simplifications (as the
problem with polymorphic refs was drastically simplified by the value
restriction).  (Argumented) suggestions are welcome.

- Xavier Leroy