Re: Typing of patterns

[Pierre Weis <Pierre.Weis@inria.fr>]

[...]
> 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/