[Caml-list] Matching exhausitvity with GADT and modules

[Caml-list] Matching exhausitvity with GADT and modules

[Joris Giovannangeli]

Hi,

The following snippet is compiling without warning :

module A = struct

  type foo
  type bar

  type 'a gadt =
      Foo : int -> foo gadt
    | Bar : int -> bar gadt

  let f = function
     | Foo i -> i
end

But if I split the code into two modules :

module A = struct

  type foo
  type bar

  type 'a gadt =
      Foo : int -> foo gadt
    | Bar : int -> bar gadt

end

module B = struct
  include A

  let f : foo gadt -> int = function
     | Foo i -> i
end

I get the following warning :

Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Bar _

How can i work around this issue ? As far as i can tell, it is not
possible for Bar to be matched by the function f.

Best regards,
joris

Re: [Caml-list] Matching exhausitvity with GADT and modules

[Ben Millwood]

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

This is a common problem that has annoyed me as well. The issue is that B
sees foo and bar as abstract types, so cannot be sure they are different,
so cannot be sure that a value of type foo gadt can't be constructed with
Bar. If you add explicit constructors for both currently-empty types, then
their inequality will be exposed and your pattern match should work.

On 27 May 2015 at 16:04, Joris Giovannangeli <joris@giovannangeli.fr> wrote:

> Hi,
>
> The following snippet is compiling without warning :
>
> module A = struct
>
>   type foo
>   type bar
>
>   type 'a gadt =
>       Foo : int -> foo gadt
>     | Bar : int -> bar gadt
>
>   let f = function
>      | Foo i -> i
> end
>
> But if I split the code into two modules :
>
> module A = struct
>
>   type foo
>   type bar
>
>   type 'a gadt =
>       Foo : int -> foo gadt
>     | Bar : int -> bar gadt
>
> end
>
> module B = struct
>   include A
>
>   let f : foo gadt -> int = function
>      | Foo i -> i
> end
>
> I get the following warning :
>
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> Bar _
>
> How can i work around this issue ? As far as i can tell, it is not
> possible for Bar to be matched by the function f.
>
> Best regards,
> joris
>
>
> --
> 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: 2319 bytes --]

Re: [Caml-list] Matching exhausitvity with GADT and modules

[Joris Giovannangeli]

> This is a common problem that has annoyed me as well. The issue is that
> B sees foo and bar as abstract types, so cannot be sure they are
> different, so cannot be sure that a value of type foo gadt can't be
> constructed with Bar. If you add explicit constructors for both
> currently-empty types, then their inequality will be exposed and your
> pattern match should work.

That's a nice workaround in the case where foo and bar and phantom types
indeed. Just adding a dummy constructor. In case they are real abstract
type, someone advised me to disable the exhaustivity warning locally
with [@@warning "-8"] code annotation, which is a bit more hack-ish.

Thanks

Re: [Caml-list] Matching exhausitvity with GADT and modules

[Yannis Juglaret]

Hi,

Removing this warning is not a good solution, because this warning may 
be relevant the day you update your GADT. As far as I know, you should 
always be using concrete types. Read for example: 
<http://stackoverflow.com/questions/20692885/gadt-definition>.

This is a question to the list: is there any good reason for allowing 
abstract types in module implementations, and not just in module 
signatures -- where they can actually be used to abstract types?

-- Yannis

Le 27/05/2015 17:22, Joris Giovannangeli a écrit :
>
>> This is a common problem that has annoyed me as well. The issue is that
>> B sees foo and bar as abstract types, so cannot be sure they are
>> different, so cannot be sure that a value of type foo gadt can't be
>> constructed with Bar. If you add explicit constructors for both
>> currently-empty types, then their inequality will be exposed and your
>> pattern match should work.
>
> That's a nice workaround in the case where foo and bar and phantom types
> indeed. Just adding a dummy constructor. In case they are real abstract
> type, someone advised me to disable the exhaustivity warning locally
> with [@@warning "-8"] code annotation, which is a bit more hack-ish.
>
> Thanks
>
>

Re: [Caml-list] Matching exhausitvity with GADT and modules

[Arseniy Alekseyev]

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

Interestingly, giving names to constructors is not sufficient. You must
give *distinct* names. In particular, the following produces a warning for
[g], but not for [f]:

module A= struct

  type foo = T
  type bar = T

  type 'a gadt =
      Foo : int -> foo gadt
    | Bar : int -> bar gadt

  let f : foo gadt -> int = function
     | Foo i -> i

end

module B = struct
  open A

  let g : foo gadt -> int = function
     | Foo i -> i
end

Joris, I think you can still kind-of use this idea for abstract data types,
at the cost of adding a wrapper type. In particular, this works:

module A= struct

  type foo
  type bar
  type foo_marker = Foo of foo
  type bar_marker = Bar of bar

  type 'a gadt =
      Foo : int -> foo_marker gadt
    | Bar : int -> bar_marker gadt

  let f : foo_marker gadt -> int = function
     | Foo i -> i

end

module B = struct
  open A

  let g : foo_marker gadt -> int = function
     | Foo i -> i
end



On Wed, May 27, 2015 at 4:14 PM, Ben Millwood <bmillwood@janestreet.com>
wrote:

> This is a common problem that has annoyed me as well. The issue is that B
> sees foo and bar as abstract types, so cannot be sure they are different,
> so cannot be sure that a value of type foo gadt can't be constructed with
> Bar. If you add explicit constructors for both currently-empty types, then
> their inequality will be exposed and your pattern match should work.
>
> On 27 May 2015 at 16:04, Joris Giovannangeli <joris@giovannangeli.fr>
> wrote:
>
>> Hi,
>>
>> The following snippet is compiling without warning :
>>
>> module A = struct
>>
>>   type foo
>>   type bar
>>
>>   type 'a gadt =
>>       Foo : int -> foo gadt
>>     | Bar : int -> bar gadt
>>
>>   let f = function
>>      | Foo i -> i
>> end
>>
>> But if I split the code into two modules :
>>
>> module A = struct
>>
>>   type foo
>>   type bar
>>
>>   type 'a gadt =
>>       Foo : int -> foo gadt
>>     | Bar : int -> bar gadt
>>
>> end
>>
>> module B = struct
>>   include A
>>
>>   let f : foo gadt -> int = function
>>      | Foo i -> i
>> end
>>
>> I get the following warning :
>>
>> Warning 8: this pattern-matching is not exhaustive.
>> Here is an example of a value that is not matched:
>> Bar _
>>
>> How can i work around this issue ? As far as i can tell, it is not
>> possible for Bar to be matched by the function f.
>>
>> Best regards,
>> joris
>>
>>
>> --
>> 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: 4344 bytes --]

Re: [Caml-list] Matching exhausitvity with GADT and modules

[Alain Frisch]

On 27/05/2015 17:36, Yannis Juglaret wrote:
> This is a question to the list: is there any good reason for allowing
> abstract types in module implementations, and not just in module
> signatures -- where they can actually be used to abstract types?

Abstract types in structures can be used to represent opaque foreign 
values manipulated through the FFI (typically custom blocks, or blocks 
which cannot -- or need not -- be described as OCaml types).


Alain