From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA07819 for caml-red; Tue, 6 Jun 2000 09:25:04 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA24324 for <caml-list@pauillac.inria.fr>; Tue, 6 Jun 2000 09:24:40 +0200 (MET DST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e567OdH15099
	for <caml-list@inria.fr>; Tue, 6 Jun 2000 09:24:39 +0200 (MET DST)
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA08806 for caml-list@inria.fr; Tue, 6 Jun 2000 09:24:39 +0200 (MET DST)
From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <200006060724.JAA08806@pauillac.inria.fr>
Subject: Re: Typing of patterns
To: caml-list@inria.fr
Date: Tue, 6 Jun 2000 09:24:39 +0200 (MET DST)
X-Mailer: ELM [version 2.4ME+ PL28 (25)]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: weis

[...]
> Ah - I think I see now: I was fooled by the syntactic "disguise" of the
> problem! So this is similar to:
> 
> This does not work:
> 
>   fun id -> id 42, id "foo"
> 
> This works:
> 
>   let id x = x in id 42, id "foo"

Exactly.

[...]
> So the restriction is required to prevent problems with references, I
> think, but those cannot occur if the type parameter is not used by any of
> the parameters of the constructor, i.e. they are monomorphic (or there are
> no parameters as in our case).

There is nothing special with references here: restriction for
references is just for generalization of types in let binding (roughly
speaking, when typing let x = e, x is monomorphic if e is an
application of the form f y). Here the restriction is just to be
correct: fun x -> x should have type 'a -> 'a, not 'a -> 'b; however
in case of complex pattern matching the rule is a bit too restrictive,
and can be relaxed in some cases as we saw.

> > Jacques may explain us if the above suggested generalization scheme is
> > used for identifiers bound in as clauses of patterns (and if not,
> > which scheme is used ?)...
> 
> I first thought it was some strange "special feature" of polymorphic
> variants, but as it seems then, it is just that the corresponding typing
> rule is obviously implemented differently...

I don't know if it is an implementation of the relaxed type-checking of
as identifiers or a special feature... Jacques will tell us...

[...]

> Since we are at it, there is another sometimes annoying type restriction,
> this time with record updates, that comes to my mind, e.g.:
> 
>   type 'a t = { foo : 'a; bar : int };;
> 
>   let x = { foo = "foo"; bar = 3 };;
> 
>   let ok = { x with foo = "bla" };;
>   let not_ok = { x with foo = 7 };;
> 
> Here the updated record "x" could have a less rigidly typed "foo"-field -
> or should we rather say it has a "default" type if the field is not
> updated? It can be a bit painful to do updates without such a
> generalisation if there are many record names that one would have to
> mention explicitely to create the wanted value as in:
> 
>   let now_ok = { foo = 7; bar = x.bar }

In some sense the problem is similar, since it is a problem of type
sharing. However it is a bit simpler in this case:

{ x with foo = "bla" } should be simply treated as a macro and typechecked
exactly as its equivalent unsuggared expression :

{foo = "bla"; bar = x.bar}

This would be more general and regular.

Best regards,

Pierre Weis

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