Re: [Caml-list] Propagating types to pattern-matching

[Jacques Le Normand <rathereasy@gmail.com>]

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

In this particular case those prudent enough to use '-warn-error -a' will
get a more informative error message, which is nice. Furthermore, for those
who think of polymorphic variants as an extension of variants, this makes
more sense.

On Mon, Feb 11, 2013 at 7:31 AM, Sebastien Mondet <
sebastien.mondet@gmail.com> wrote:

>
> Hi Jacques
>
> I don't know if this directly related, or if it is actually intended, but
> this looks like a regression to me:
>
>
> With OCaml version 4.00.1+dev2_2012-08-06  (4.00.1+short-types in Opam):
>
> # let f = function 0 -> `zero | 1 -> `one | _ -> `some;;
> val f : int -> [> `one | `some | `zero ] = <fun>
>
> # let g x = match f x with `one -> 1 | `zero -> 0;;
> Error: This pattern matches values of type [< `one | `zero ]
>
>        but a pattern was expected which matches values of type
>          [> `one | `some | `zero ]
>        The first variant type does not allow tag(s) `some
>
> which is the nice behavior we were used to,
> but with OCaml version 4.01.0+dev10-2012-10-16  (a.k.a.
> 4.01.0dev+short-paths), the error has been downgraded to a warning:
>
> # let f = function 0 -> `zero | 1 -> `one | _ -> `some;;
> val f : int -> [> `one | `some | `zero ] = <fun>
>
> # let g x = match f x with `one -> 1 | `zero -> 0;;
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> `some
> val g : int -> int = <fun>
>
>
> Is it intended?
>
> Cheers
> Seb
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> On Tue, Jan 15, 2013 at 12:59 AM, Jacques Garrigue <
> garrigue@math.nagoya-u.ac.jp> wrote:
>
>> Dear Camlers,
>>
>> It is a bit unusual, but this message is about changes in trunk.
>>
>> As you may be aware from past threads, since the introduction of GADTs
>> in 4.00, some type information is propagated to pattern-matching, to allow
>> it to refine types.
>> More recently, types have started being used to disambiguate constructors
>> and record fields, which means some more dependency on type information
>> in pattern-matching.
>>
>> However, a weakness of this approach was that propagation was disabled
>> as soon as a pattern contained polymorphic variants. The reason is that
>> typing rules for polymorphic variants in patterns and expression are
>> subtly
>> different, and mixing information without care would lose principality.
>>
>> At long last I have removed this restriction on the presence of
>> polymorphic
>> variants, but this has some consequences on typing:
>>
>> * while type information is now propagated, information about possibly
>>   present constructors still has to be discarded. For instance this means
>> that
>>   the following code will not be typed as you could expect:
>>
>>         let f (x : [< `A | `B]) = match x with `A -> 1 | _ -> 2;;
>>         val f : [< `A | `B > `A ] -> int
>>
>>   What happens is that inside pattern-matching, only required constructors
>>   are propagated, which reduces the type of x to [> ] (a polymorphic
>> variant
>>   type with any constructor…)
>>   As before, to give an upper bound to the matched type, the type
>> annotation
>>   must be inside a pattern:
>>
>>         let f = function (`A : [< `A | `B]) -> 1 | _ -> 2;;
>>         val f : [< `A | `B ] -> int = <fun>
>>
>> * the propagation of type information may lead to failure in some cases
>> that
>>   where typable before:
>>
>>         type ab = [ `A | `B ];;
>>         let f (x : [`A]) = match x with #ab -> 1;;
>>         Error: This pattern matches values of type [? `A | `B ]
>>                but a pattern was expected which matches values of type [
>> `A ]
>>                The second variant type does not allow tag(s) `B
>>
>>   During pattern-matching it is not allowed to match on absent type
>> constructors,
>>   even though the type of the patterns would eventually be [< `A | `B],
>> which allows
>>   discarding `B. ([? `A | `B] denotes a type obeying the rules of
>> pattern-matching)
>>
>> * for the sake of coherence, even if a type was not propagated because it
>>   was not known when typing a pattern-matching, we are still going to
>> fail if a
>>   matched constructor appears to be absent after typing the whole
>> function.
>>   (This only applies to propagable types, i.e. polymorphic variant types
>> that
>>    contain only required constructors)
>>
>> In particular the last two points are important, because previously such
>> uses
>> would not have triggered even a warning.
>>
>> The idea is that allowing propagation of types is more important than
>> keeping some not really useful corner cases, but if this is of concern
>> to you, I'm interested in feedback.
>>
>>         Jacques Garrigue
>> --
>> 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: 6307 bytes --]