Re: Typing of patterns

From: Jacques Garrigue (garrigue@kurims.kyoto-u.ac.jp)
Date: Tue Jun 06 2000 - 02:55:55 MET DST

  • Next message: Patrick M Doane: "Re: Typing of patterns"

    From: Pierre Weis <Pierre.Weis@inria.fr>

    > We can observe the same kind of behaviour with polymorphic variants:
    >
    > type 'a pliste = [`Nil | `Cons of 'a * 'a pliste];;
    [...]
    > However, we get a strange difference in typing since, as you
    > mentioned, the explicit ``as clause'' does not set up a typing
    > connection between input and output :
    >
    > let (ensure_nil : 'a pliste -> 'b pliste) = function
    > | `Cons (x, l) -> failwith "Not nil"
    > | `Nil as l -> l;;
    > val ensure_nil : 'a pliste -> 'b pliste = <fun>
    >
    > 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 ?)...

    Ok, with polymorphic variants the as clause has a special meaning:
    typingwise it does the same thing as an explicit copy, but without the
    operational cost involved.

    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.

    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>

    > 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.
    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 ?
    Symmetries can bring you a long way.

    Cheers,

            Jacques
    ---------------------------------------------------------------------------
    Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp
                    <A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>



    This archive was generated by hypermail 2b29 : Tue Jun 06 2000 - 09:35:18 MET DST