[Caml-list] Propagating types to pattern-matching

[Caml-list] Propagating types to pattern-matching

[Jacques Garrigue]

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

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

[Sebastien Mondet]

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

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: 5741 bytes --]

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

[Jacques Le Normand]

[-- 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 --]

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

[Jacques Garrigue]

On 2013/02/12, at 0:31, 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>
> 

This is related, and this is the intended behavior.
For polymorphic variants, you get a warning if the type was known early enough,
and a hard error otherwise.
Actually, I see it as a progress, since the warning gives you a counter-example,
whereas the error message only gives you a discrepancy between types.

For me the only sane handling of partial matching is to see it as an error,
so use at least -warn-error P. (Or at least watch for warnings)

	Jacques Garrigue