[Caml-list] explaining polymorphic variants

[Caml-list] explaining polymorphic variants

[Yaron Minsky]

A question that came up in the section of Real World OCaml on
polymorphic variants.

I'm wondering if someone can explain the error in the third definition
below.

    # let handle_a `A = "a";;
    val handle_a : [< `A ] -> string = <fun>
    # let handle_ab (x: [`A | `B ])  =
        match x with
        |`B -> "b"
        | `A as a -> handle_a a
      ;;
    val handle_ab : [ `A | `B ] -> string = <fun>
    # let handle_ab' (x: [`A | `B ])  =
        match x with
        | `B -> "b"
        | a -> handle_a a
      ;;
    Characters 86-87:
        | a -> handle_a a
                        ^
    Error: This expression has type [ `A | `B ]
           but an expression was expected of type [< `A ]
           The second variant type does not allow tag(s) `B

I understand roughly what's going on here.  In the definition of
handle_ab, there is a straightforward syntactic basis for narrowing
the type of the variable a.  In the case of handle_ab', that syntactic
basis is no longer available, and so the type of a is not narrowed.

But the question is: why isn't it narrowed based on the other
information available?  It seems in theory possible to infer the
narrower type in this case.  Does anyone have a satisfying explanation
as to why?

y

Re: [Caml-list] explaining polymorphic variants

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 1996 bytes --]

Well, for one, the patterns are typed independently of the type of the
guard. For two, this wouldn't work for nested patterns.
Do we want to make an exception for the case when there are only simple
patterns and when the type of the guard has been fully determined? I don't
know if it's worth the trouble, especially when it can usually be handled
with the # operator.
On Oct 28, 2012 6:50 AM, "Yaron Minsky" <yminsky@janestreet.com> wrote:

> A question that came up in the section of Real World OCaml on
> polymorphic variants.
>
> I'm wondering if someone can explain the error in the third definition
> below.
>
>     # let handle_a `A = "a";;
>     val handle_a : [< `A ] -> string = <fun>
>     # let handle_ab (x: [`A | `B ])  =
>         match x with
>         |`B -> "b"
>         | `A as a -> handle_a a
>       ;;
>     val handle_ab : [ `A | `B ] -> string = <fun>
>     # let handle_ab' (x: [`A | `B ])  =
>         match x with
>         | `B -> "b"
>         | a -> handle_a a
>       ;;
>     Characters 86-87:
>         | a -> handle_a a
>                         ^
>     Error: This expression has type [ `A | `B ]
>            but an expression was expected of type [< `A ]
>            The second variant type does not allow tag(s) `B
>
> I understand roughly what's going on here.  In the definition of
> handle_ab, there is a straightforward syntactic basis for narrowing
> the type of the variable a.  In the case of handle_ab', that syntactic
> basis is no longer available, and so the type of a is not narrowed.
>
> But the question is: why isn't it narrowed based on the other
> information available?  It seems in theory possible to infer the
> narrower type in this case.  Does anyone have a satisfying explanation
> as to why?
>
> y
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 2695 bytes --]