Typing of patterns

From: Markus Mottl (mottl@miss.wu-wien.ac.at)
Date: Thu Jun 01 2000 - 15:23:39 MET DST

  • Next message: Brian Rogoff: "Re: How do you declare infix in Ocaml"

    Hello,

    I would like to know something about the typing rules of identifiers that
    are bound in pattern matching:

    Let's consider this small example:

      module type FUNCTOR = sig
        type 'a t
        val map : ('a -> 'b) -> ('a t -> 'b t)
      end

      type 'a expr = Num of int | Add of 'a * 'a

      module ExprFun : FUNCTOR = struct
        type 'a t = 'a expr

        let map f = function
          | Num n as num -> num
          | Add (e, e') -> Add (f e, f e')
      end

    This will lead to the (shortened) error message:

      Values do not match:
        val map : ('a -> 'a) -> 'a expr -> 'a expr
      is not included in
        val map : ('a -> 'b) -> 'a t -> 'b t

    The problem arises in this line:

      | Num n as num -> num

    This looks perfectly ok at first sight, but a closer look reveals that
    "num" is not only bound to the value "Num n", it also has the exact type of
    the left-hand side. Thus, the rhs will also be forced to have this type if
    we use this pattern name.

    To correct the problem, we can write:

      | Num n -> Num n

    But isn't this a bit strange that an identifier cannot be used in a context
    where replacing it syntactically with its bound value would be perfectly
    ok?

    Or has experience shown that using more general types in such cases leads
    to more programming errors?

    One can, of course, always explicitely restrict the type of an identifier,
    but in the upper example we want to have the opposite, i.e. have it more
    general. One side effect of this problem is that we cannot efficiently
    return the value "as is": we have to construct it again, which may come
    with a not insignficant performance penalty...

    Are there any deeper insights behind this rationale? (The given code works
    without problems if polymorphic variants are used instead).

    Best regards,
    Markus Mottl

    -- 
    Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl
    



    This archive was generated by hypermail 2b29 : Sat Jun 03 2000 - 09:36:30 MET DST