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 RAA30889 for caml-red; Tue, 6 Jun 2000 17:35:38 +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 RAA07641 for <caml-list@pauillac.inria.fr>; Tue, 6 Jun 2000 17:32:07 +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 e56FW3H01953;
	Tue, 6 Jun 2000 17:32:03 +0200 (MET DST)
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA22326; Tue, 6 Jun 2000 17:32:03 +0200 (MET DST)
From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <200006061532.RAA22326@pauillac.inria.fr>
Subject: Re: Typing of patterns
In-Reply-To: <20000606095555Q.garrigue@kurims.kyoto-u.ac.jp> from Jacques Garrigue at "Jun 6, 100 09:55:55 am"
To: garrigue@kurims.kyoto-u.ac.jp (Jacques Garrigue)
Date: Tue, 6 Jun 2000 17:32:03 +0200 (MET DST)
Cc: caml-list@inria.fr
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

[...]
> However, the goal is a bit different, as you can can see if you don't
> put type annotations on the output:
> 
> let (ensure_nil : 'a pliste -> 'b) = function
>   | `Cons (x, l) -> failwith "Not nil"
>   | `Nil as l -> l;;
> val ensure_nil : 'a pliste -> [> `Nil] = <fun>
> 
> With polymorphic variants we know that the output does not contain
> Cons! The disconnection between input and output variables is a mere
> consequence of that: [> `Nil] knows nothing about the type parameter
> of pliste.

Marvellous.

> This mechanism was intended as an implementation of type-based
> dispatch (with polymorhic variants type and values coincide), and you
> could say it is just an overloading of the as construct (which is OK
> since it does not change its operational meaning).
> >From the point of view of separation, it is also a bit ad-hoc, in that
> it requires the variant pattern (or an or-pattern containing only
> variants) to be immediately enclosed in the as clause, otherwise it
> reverts to the usual type-sharing behaviour:
> 
> let f1 = function `A as x -> x;;
> val f1 : [< `A] -> [> `A] = <fun>
> let f2 = function (`A, `B) as x -> x;;
> val f2 : ([< `A] as 'a) * ([< `B] as 'b) -> 'a * 'b = <fun>

Yes this is a bit strange. You may use the rule I gave in my previous
message : generalize type variables that does not appear in the type
of identifiers bound in sub-patterns.

> > Conclusion: this strongly suggests to generalize the typing of
> > synonymous identifiers in patterns, in order to obtain the same typing
> > assignments for pattern matching on ``closed'' polymorphic variants
> > and pattern matching on their (semantically equivalent) sum data types
> > counterparts.
> 
> This is indeed possible. This just requires a bit of additional code in
> the type checker. However sum data types do not allow type-based
> dispatch, so this would really only be useful for separating type
> parameters.

Yes and this is indeed desirable.

> Also, this reminds me of another problem discussed last year in this
> mailing list:
>         # type 'a t = {key: int; data: 'a};;
>         type 'a t = { key : int; data : 'a; } 
>         # let v = {key = 1; data = 1};;    
>         val v : int t = {key=1; data=1}
>         # {v with data = true};;
>         This expression has type int t but is here used with type bool t
> 
> If we separate type parameters in sums, then we will probably also
> have to do it for products, isn't it ?

Sure.

> Symmetries can bring you a long way.

Yes, and this is an easy way for the user of the language.

Pierre Weis

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