[...]
> 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/
This archive was generated by hypermail 2b29 : Tue Jun 06 2000 - 17:38:27 MET DST