polymorphic variant oddity

polymorphic variant oddity

[Julian Assange]

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?

Re: polymorphic variant oddity

[Pierre Weis]

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/

Re: polymorphic variant oddity

[Markus Mottl]

On Sat, 07 Oct 2000, Julian Assange wrote:
> 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 the same as saying, e.g.:

  let Some x = Some 3;;

"x" will be bound to "3".

"let", too, can be used for pattern matching. Of course, one can only match
one pattern at a time with it, which rules it out for sum types that have
several instances (as in the above example -> "Some/None"): a match error
may occur.

Normally, this kind of pattern matching is only used for patterns that
never fail ("irrefutable patterns"), e.g. tuples:

  let x, y = 1, 2 in ...

Best regards,
Markus Mottl

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

Re: polymorphic variant oddity

[John Prevost]

>>>>> "ja" == Julian Assange <proff@iq.org> writes:

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

  ja> What exactly is the meaning this?

Looks like normal pattern matching to me:


# let Some x = x;;
Unbound value x
# let Some x = 1;;
This expression has type int but is here used with type 'a option
# let Some x = Some 1;;
Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
None
val x : int = 1
# Some 4;; 
- : int option = Some 4

What did you expect to happen?

John.