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 XAA28084 for caml-red; Sun, 8 Oct 2000 23:09:36 +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 SAA31817 for <caml-list@pauillac.inria.fr>; Sun, 8 Oct 2000 18:01:16 +0200 (MET DST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e98G0wX19758;
	Sun, 8 Oct 2000 18:00:58 +0200 (MET DST)
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA30931; Sun, 8 Oct 2000 18:00:57 +0200 (MET DST)
From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <200010081600.SAA30931@pauillac.inria.fr>
Subject: Re: polymorphic variant oddity
In-Reply-To: <wxitr4naws.fsf@suburbia.net> from Julian Assange at "Oct 7, 100 10:33:23 pm"
To: proff@iq.org (Julian Assange)
Date: Sun, 8 Oct 2000 18:00:57 +0200 (MET DST)
Cc: caml-list@inria.fr
X-Mailer: ELM [version 2.4ME+ PL28 (25)]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: weis@pauillac.inria.fr

Julian Assange played with polymorphic variants:

> let `F x = x;;   
> Unbound value x
> # let `F x = 1;;
> This expression has type int but is here used with type [< `F of 'a | ..]
> # let `F x = `F 1;;
> val x : int = 1
> # `F 4;;
> - : [> `F of int] = `F 4
> 
> What exactly is the meaning this?

This is not specific to polymorphic variants, you may observe the same
behaviour with regular concrete data types. Since, it is simpler with
usual types and constructors, let's explain with a simple type with F
as single constructor:

type 'a t = F of 'a;;

# let F x = x;;
            ^
Unbound value x

Explanation: when defining let pattern = expr, the compiler
verifies that the expr can be computed; it is not the case here, since
x is unknown (as not been previously defined). Is there something
surprising here ?

# let F x = 1;;
            ^
This expression has type int but is here used with type 'a t

When writing let pattern = expr with a complex pattern such that F x,
your using a ``destructuring let'', which means that the value of expr
will be matched against pattern, and the variables in pattern will be
bound to the corresponding parts in (the computed value of)
expr. Hence expr should have the same type as pattern. Hence the type
checking error since F x has type 'a t and 1 has type int.

# let F x = F 1;;
val x : int = 1

One successful destructurig let, that bounds x (the variable of the
left-hand pattern) to 1 (the value corresponding to that variable in
the right-hand expression).

# F 4;;
- : int t = F 4

Nothing strange: we just build a value of type t.

Is there some more magic to explain ?

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/