[Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Abdallah Saffidine]

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

Hi all,

I am reposting this SO question
<http://stackoverflow.com/questions/33093807/how-to-use-gadts-across-modules-in-ocaml-without-raising-warnings>.
I suspect there might be a bug in the implementation of Warning 8.

Thanks,
Abdallah

I have two files: gadt1.ml and gadt2.ml and the second depends on the first.

gadt1.ml:

type nevertype _ t1 = A1 : never  t1 | B1 : bool t1type _ t2 = A2 :
string t2 | B2 : bool t2let get1 : bool t1 -> bool = function B1 ->
truelet get2 : bool t2 -> bool = function B2 -> true

gadt2.ml:

let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> truelet get2 :
bool Gadt1.t2 -> bool = function Gadt.B2 -> true

when I compile using ocaml 4.02.3 (ocamlbuild gadt2.native), I get a
warning 8 about the function Gadt2.get1 not being exhaustive. I am quite
puzzled that Gadt2.get1 raises a warning while Gadt1.get1 and Gadt2.get2
don't.

My assumption was that the empty type never cannot be equal to bool so
Gadt2.get1 should not raise a warning. On the other hand, if I call
Gadt2.get1 with argument A1, I get a type error (as desired). Is the
warning expected behaviour or a bug? What did I miss?

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

Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Stefan Holdermans]

Abdallah,

> gadt1.ml:
> 
> type
>  never
> 
> type _ t1 = A1 : never  t1 | B1 :
>  bool t1
> 
> type _ t2 = A2 : string t2 | B2 :
>  bool t2
> 
> let get1 : bool t1 -> bool = function B1 -> true
> let get2 : bool t2 -> bool = function B2 -> true
> gadt2.ml:
> 
> let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> true
> let get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true
> when I compile using ocaml 4.02.3 (ocamlbuild gadt2.native), I get a warning 8 about the function Gadt2.get1 not being exhaustive. I am quite puzzled that Gadt2.get1 raises a warning while Gadt1.get1 and Gadt2.get2 don’t.

I suppose that, from the perspective of ‘Gadt2', ‘Gadt1.never’ is an abstract datatype that *could* have been implemented by ‘Gadt1’ as

  type never = bool

Perhaps there’s a design priciple emerging here? Concrete GADTs do not mix well with abstract type arguments.

Cheers,

  Stefan

Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Philippe Veber]

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

Hi Abdallah,

  I came across the very same observation a few days ago. I'm not an expert
on typing but here's how I understand it: in gadt1.ml the declaration of
never makes it clear it is an empty type, which in particular is different
from bool. Now the signature of Gadt1 as seen by Gadt2 is:

module Gadt1 : sig
  type never
  type _ t1 = A1 : never t1 | B1 : bool t1
  [...]
end

This implies that Gadt2 doesn't see Gadt1.never as an empty type, but
rather as an abstract type, and so has no indication that it is different
from bool. The signature could as well be hiding a definition like type
never = bool. So in Gadt2, the exhaustiveness checker has no way to do its
job, hence the puzzling behavior you observe.

In my case I changed the definition of my phantom types from empty to
polymorphic variant types and made them explicit in the signature of the
module.

module Gadt1 : sig
  type never = [`never]
  [...]
end

I hope this intuitive explanation is not too far from the truth :o)!

Cheers,
  Philippe.


2015-10-13 7:27 GMT+02:00 Abdallah Saffidine <abdallah.saffidine@gmail.com>:

> Hi all,
>
> I am reposting this SO question
> <http://stackoverflow.com/questions/33093807/how-to-use-gadts-across-modules-in-ocaml-without-raising-warnings>.
> I suspect there might be a bug in the implementation of Warning 8.
>
> Thanks,
> Abdallah
>
> I have two files: gadt1.ml and gadt2.ml and the second depends on the
> first.
>
> gadt1.ml:
>
> type nevertype _ t1 = A1 : never  t1 | B1 : bool t1type _ t2 = A2 : string t2 | B2 : bool t2let get1 : bool t1 -> bool = function B1 -> truelet get2 : bool t2 -> bool = function B2 -> true
>
> gadt2.ml:
>
> let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> truelet get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true
>
> when I compile using ocaml 4.02.3 (ocamlbuild gadt2.native), I get a
> warning 8 about the function Gadt2.get1 not being exhaustive. I am quite
> puzzled that Gadt2.get1 raises a warning while Gadt1.get1 and Gadt2.get2
> don't.
>
> My assumption was that the empty type never cannot be equal to bool so
> Gadt2.get1 should not raise a warning. On the other hand, if I call
> Gadt2.get1 with argument A1, I get a type error (as desired). Is the
> warning expected behaviour or a bug? What did I miss?
>
>

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

Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Ben Millwood]

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

I answered the SO question, with broadly the same answer as everyone else
gave. This issue has come at least twice before on this mailing list -- I
feel like there really is a missing feature here in terms of proper support
for empty types.

I'll advance on others' advice by pointing out that if you say:

type never = private [`never]

then you neither "use up" a constructor name nor is it possible to write an
expression with type never. Unfortunately, the compiler still doesn't
realise that, so it doesn't help you for pattern-matching.

On 13 October 2015 at 14:09, Philippe Veber <philippe.veber@gmail.com>
wrote:

> Hi Abdallah,
>
>   I came across the very same observation a few days ago. I'm not an
> expert on typing but here's how I understand it: in gadt1.ml the
> declaration of never makes it clear it is an empty type, which in
> particular is different from bool. Now the signature of Gadt1 as seen by
> Gadt2 is:
>
> module Gadt1 : sig
>   type never
>   type _ t1 = A1 : never t1 | B1 : bool t1
>   [...]
> end
>
> This implies that Gadt2 doesn't see Gadt1.never as an empty type, but
> rather as an abstract type, and so has no indication that it is different
> from bool. The signature could as well be hiding a definition like type
> never = bool. So in Gadt2, the exhaustiveness checker has no way to do its
> job, hence the puzzling behavior you observe.
>
> In my case I changed the definition of my phantom types from empty to
> polymorphic variant types and made them explicit in the signature of the
> module.
>
> module Gadt1 : sig
>   type never = [`never]
>   [...]
> end
>
> I hope this intuitive explanation is not too far from the truth :o)!
>
> Cheers,
>   Philippe.
>
>
> 2015-10-13 7:27 GMT+02:00 Abdallah Saffidine <abdallah.saffidine@gmail.com
> >:
>
>> Hi all,
>>
>> I am reposting this SO question
>> <http://stackoverflow.com/questions/33093807/how-to-use-gadts-across-modules-in-ocaml-without-raising-warnings>.
>> I suspect there might be a bug in the implementation of Warning 8.
>>
>> Thanks,
>> Abdallah
>>
>> I have two files: gadt1.ml and gadt2.ml and the second depends on the
>> first.
>>
>> gadt1.ml:
>>
>> type nevertype _ t1 = A1 : never  t1 | B1 : bool t1type _ t2 = A2 : string t2 | B2 : bool t2let get1 : bool t1 -> bool = function B1 -> truelet get2 : bool t2 -> bool = function B2 -> true
>>
>> gadt2.ml:
>>
>> let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> truelet get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true
>>
>> when I compile using ocaml 4.02.3 (ocamlbuild gadt2.native), I get a
>> warning 8 about the function Gadt2.get1 not being exhaustive. I am quite
>> puzzled that Gadt2.get1 raises a warning while Gadt1.get1 and Gadt2.get2
>> don't.
>>
>> My assumption was that the empty type never cannot be equal to bool so
>> Gadt2.get1 should not raise a warning. On the other hand, if I call
>> Gadt2.get1 with argument A1, I get a type error (as desired). Is the
>> warning expected behaviour or a bug? What did I miss?
>>
>>
>

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

Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Jeremy Yallop]

On 13 October 2015 at 07:15, Ben Millwood <bmillwood@janestreet.com> wrote:
> I'll advance on others' advice by pointing out that if you say:
>
> type never = private [`never]
>
> then you neither "use up" a constructor name nor is it possible to write an
> expression with type never.

A nit: there are lots of *expressions* of type 'never', such as
'(assert false: never)'.  However, there are no (closed) *values* of
type 'never'.

> Unfortunately, the compiler still doesn't realise that, so it
> doesn't help you for pattern-matching.

The gadt-warnings branch, which is described here:

   GADTs and exhaustiveness: looking for the impossible
   Jacques Garrigue's and Jacques Le Normand
   ACM SIGPLAN Workshop on ML, September 2015
   http://www.mlworkshop.org/gadts-and-exhaustiveness-looking-for-the-impossible.pdf

includes better supports for "empty" types.  For example, here's a
definition of an empty type 'wrong':

   type 'a is_true = T: [`True] is_true
   type wrong = [`False] is_true

and here's a function definition which omits a case that you can
deduce is unmatchable when you know that 'wrong' is empty:

   let f : wrong option -> unit = fun None -> ()

The current OCaml compiler (4.02.3) issues a warning for 'f':

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

In contrast, the compiler in the gadt-warnings branch compiles 'f'
without complaint (and generates more efficient code, since there's no
need to inspect the argument).

Jeremy.

Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Abdallah Saffidine]

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

Dear all,

Thanks a lot for your help. Things are much clearer now.

Abdallah

2015-10-13 20:45 GMT+11:00 Jeremy Yallop <yallop@gmail.com>:

> On 13 October 2015 at 07:15, Ben Millwood <bmillwood@janestreet.com>
> wrote:
> > I'll advance on others' advice by pointing out that if you say:
> >
> > type never = private [`never]
> >
> > then you neither "use up" a constructor name nor is it possible to write
> an
> > expression with type never.
>
> A nit: there are lots of *expressions* of type 'never', such as
> '(assert false: never)'.  However, there are no (closed) *values* of
> type 'never'.
>
> > Unfortunately, the compiler still doesn't realise that, so it
> > doesn't help you for pattern-matching.
>
> The gadt-warnings branch, which is described here:
>
>    GADTs and exhaustiveness: looking for the impossible
>    Jacques Garrigue's and Jacques Le Normand
>    ACM SIGPLAN Workshop on ML, September 2015
>
> http://www.mlworkshop.org/gadts-and-exhaustiveness-looking-for-the-impossible.pdf
>
> includes better supports for "empty" types.  For example, here's a
> definition of an empty type 'wrong':
>
>    type 'a is_true = T: [`True] is_true
>    type wrong = [`False] is_true
>
> and here's a function definition which omits a case that you can
> deduce is unmatchable when you know that 'wrong' is empty:
>
>    let f : wrong option -> unit = fun None -> ()
>
> The current OCaml compiler (4.02.3) issues a warning for 'f':
>
>    Warning 8: this pattern-matching is not exhaustive.
>    Here is an example of a value that is not matched:
>    Some _
>
> In contrast, the compiler in the gadt-warnings branch compiles 'f'
> without complaint (and generates more efficient code, since there's no
> need to inspect the argument).
>
> Jeremy.
>

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

Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings?

[Jacques Garrigue]

On 2015/10/13 14:27, Abdallah Saffidine wrote:
> 
> Hi all,
> 
> I am reposting this SO question. I suspect there might be a bug in the implementation of Warning 8.
> 
> Thanks,
> Abdallah
> 
> I have two files: gadt1.ml and gadt2.ml and the second depends on the first.
> 
> gadt1.ml:
> 
> type
>  never
> 
> type _ t1 = A1 : never  t1 | B1 :
>  bool t1
> 
> type _ t2 = A2 : string t2 | B2 :
>  bool t2
> 
> let get1 : bool t1 -> bool = function B1 -> true
> let get2 : bool t2 -> bool = function B2 -> true
> gadt2.ml:
> 
> let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> true
> let get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true
> when I compile using ocaml 4.02.3 (ocamlbuild gadt2.native), I get a warning 8 about the function Gadt2.get1 not being exhaustive. I am quite puzzled that Gadt2.get1 raises a warning while Gadt1.get1 and Gadt2.get2 don't.
> 
> My assumption was that the empty type never cannot be equal to bool so Gadt2.get1 should not raise a warning. On the other hand, if I call Gadt2.get1 with argument A1, I get a type error (as desired). Is the warning expected behaviour or a bug? What did I miss?

A explained by Stefan, abstract types coming from other modules cannot be proved distinct.
Only predefined types such as string or array are handled specially.

The simplest solution is to add a constructor to your type:

	type never = Never

Better to do it when in the same module too.

Jacques Garrigue