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 JAA07103 for caml-red; Sat, 3 Jun 2000 09:30:55 +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 PAA18954 for <caml-list@pauillac.inria.fr>; Thu, 1 Jun 2000 15:23:53 +0200 (MET DST)
Received: from miss.wu-wien.ac.at (miss.wu-wien.ac.at [137.208.107.17])
	by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e51DNpj18035
	for <caml-list@inria.fr>; Thu, 1 Jun 2000 15:23:51 +0200 (MET DST)
Received: (from mottl@localhost)
	by miss.wu-wien.ac.at (8.9.0/8.9.0) id PAA27518
	for caml-list@inria.fr; Thu, 1 Jun 2000 15:23:40 +0200 (MET DST)
Date: Thu, 1 Jun 2000 15:23:39 +0200
From: Markus Mottl <mottl@miss.wu-wien.ac.at>
To: OCAML <caml-list@inria.fr>
Subject: Typing of patterns
Message-ID: <20000601152339.A23433@miss.wu-wien.ac.at>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
User-Agent: Mutt/1.2i
Sender: weis

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