[Caml-list] Match error with abstract types in modules

[Caml-list] Match error with abstract types in modules

[David Allsopp]

Please could someone remind me what it is about types in modules which means
that

  module Foo = struct
    type 'a foo
  end

  type _ t = A : int Foo.foo t
           | B : float Foo.foo t

  let foo A = ()

is non-exhaustive pattern matching, but:

  type 'a bar

  type _ u = C : int bar u
           | D : float bar u

  let bar C = ()

is exhaustive? Or is it actually a bug (given that foo B is a type error)?


David

Re: [Caml-list] Match error with abstract types in modules

[Leo White]

> Please could someone remind me what it is about types in modules which means
> that
>
>   module Foo = struct
>     type 'a foo
>   end
>
>   type _ t = A : int Foo.foo t
>            | B : float Foo.foo t
>
>   let foo A = ()
>
> is non-exhaustive pattern matching, but:
>
>   type 'a bar
>
>   type _ u = C : int bar u
>            | D : float bar u
>
>   let bar C = ()
>
> is exhaustive? Or is it actually a bug (given that foo B is a type error)?
>

If Foo is replaced with:

    module Foo : sig
      type 'a foo
    end = struct
      type 'a foo = unit
    end

so that `int foo` is equal to `float foo`, then your match isn't really
exhaustive.

In the second version, the compiler cheats. Since `bar` is definied in
the same module, it knows that the abstract `bar` type it can see is
actually the definition, not just an abstraction of a type defined
elsewhere, so it knows that `int bar` cannot equal `float bar`.

Personally, I dislike this behaviour and would prefer both cases to give
an error.

Regards,

Leo

RE: [Caml-list] Match error with abstract types in modules

[David Allsopp]

Leo White wrote:
> > Please could someone remind me what it is about types in modules which
> > means that
> >
> >   module Foo = struct
> >     type 'a foo
> >   end
> >
> >   type _ t = A : int Foo.foo t
> >            | B : float Foo.foo t
> >
> >   let foo A = ()
> >
> > is non-exhaustive pattern matching, but:
> >
> >   type 'a bar
> >
> >   type _ u = C : int bar u
> >            | D : float bar u
> >
> >   let bar C = ()
> >
> > is exhaustive? Or is it actually a bug (given that foo B is a type
> error)?
> >
> 
> If Foo is replaced with:
> 
>     module Foo : sig
>       type 'a foo
>     end = struct
>       type 'a foo = unit
>     end
> 
> so that `int foo` is equal to `float foo`, then your match isn't really
> exhaustive.

How so? What's (very) confusing to me is that it seems to permit nonsensical matches without warning. In both the unconstrained and constrained versions of Foo, the resulting type of the function [foo] is [int Foo.foo t -> unit] so [foo B] is always rejected. But you get no warning about an unusable match case with:

let foo = function A -> () | B -> ()

although 

let foo = function A | B -> ()

unsurprisingly does not type.

> In the second version, the compiler cheats. Since `bar` is definied in the
> same module, it knows that the abstract `bar` type it can see is actually
> the definition, not just an abstraction of a type defined elsewhere, so it
> knows that `int bar` cannot equal `float bar`.
> 
> Personally, I dislike this behaviour and would prefer both cases to give
> an error.

What's to dislike? It's rather useful - the constructors of a GADT are partionable by type. What caught me out was that two constructors with distinct types (in my actual use with different instantiations of 'a BatSet.t) were being regarded as equal in terms of pattern matching. I'd be quite happy if a type annotation were necessary to make it explicit that I meant to do it:

let foo (key : int Foo.foo t) =
  match key with A -> ()

Especially with that explicit type, I find it very odd to get a warning about a constructor whose type is not permitted in this context and so cannot be matched.

Ta for the explanation behind the difference in behaviour, regardless!


David

Re: [Caml-list] Match error with abstract types in modules

[Leo White]

>> so that `int foo` is equal to `float foo`, then your match isn't really
>> exhaustive.
>
> How so?

Both constructors would then have the same type. Since it is possible
they both have the same type, you need to match on both of them.

> What's (very) confusing to me is that it seems to permit
> nonsensical matches without warning. In both the unconstrained and
> constrained versions of Foo, the resulting type of the function [foo] is
> [int Foo.foo t -> unit] so [foo B] is always rejected. But you get no
> warning about an unusable match case with:
>
> let foo = function A -> () | B -> ()
>

This is because `foo B` may not always be rejected. Consider the
following code:

    module F (Foo : sig type 'a foo end) = struct

      type _ t = A : int Foo.foo t
           | B : float Foo.foo t

      let foo = function
        | A -> ()
        | B -> ()

      (* [foo B] would be an error here *)

    end

    module M = F(struct type 'a foo = unit end)

    (* But out here it is fine *)
    let () = M.foo M.B

> although
>
> let foo = function A | B -> ()
>
> unsurprisingly does not type.

That's due to GADTs not currently being compatible with or-patterns, it
is not related to the injectivity issues you are having.

>> In the second version, the compiler cheats. Since `bar` is definied in the
>> same module, it knows that the abstract `bar` type it can see is actually
>> the definition, not just an abstraction of a type defined elsewhere, so it
>> knows that `int bar` cannot equal `float bar`.
>> 
>> Personally, I dislike this behaviour and would prefer both cases to give
>> an error.
>
> What's to dislike?

Giving different behviour based on whether something is defined in the
same module is anti-modular, and confuses people when they try to split
their code across different modules.

> It's rather useful - the constructors of a GADT are
> partionable by type.

That is indeed useful, but only really works in OCaml if you expose the
definitions of these types, so that OCaml can see that they are
definitely not the same type. This is why you see people use:

    type z = Z

    type 'a s = S

when doing type-level arithmetic. By giving types with incompatible
definitions, rather than abstract types, OCaml can safely conclude they
are not the same type.

> What caught me out was that two constructors with
> distinct types (in my actual use with different instantiations of 'a
> BatSet.t) were being regarded as equal in terms of pattern matching. I'd
> be quite happy if a type annotation were necessary to make it explicit
> that I meant to do it:
>
> let foo (key : int Foo.foo t) =
>   match key with A -> ()
>
> Especially with that explicit type, I find it very odd to get a warning
> about a constructor whose type is not permitted in this context and so
> cannot be matched.

The problem is that OCaml has no way to know that `int Foo.foo` is not
equal to `float Foo.foo` so it must insist that you include a case for
it. OCaml also doesn't know that `int Foo.foo` does equal `float
Foo.foo` so it can't let you call `foo Foo.B` either.

Regards,

Leo

Re: [Caml-list] Match error with abstract types in modules

[Jeremy Yallop]

On 24 February 2015 at 18:26, David Allsopp <dra-news@metastack.com> wrote:
> Leo White wrote:
>> > Please could someone remind me what it is about types in modules which
>> > means that
>> >
>> >   module Foo = struct
>> >     type 'a foo
>> >   end
>> >
>> >   type _ t = A : int Foo.foo t
>> >            | B : float Foo.foo t
>> >
>> >   let foo A = ()
>> >
>> > is non-exhaustive pattern matching, but:
>> >
>> >   type 'a bar
>> >
>> >   type _ u = C : int bar u
>> >            | D : float bar u
>> >
>> >   let bar C = ()
>> >
>> > is exhaustive? Or is it actually a bug (given that foo B is a type
>> error)?
>> >
>>
>> If Foo is replaced with:
>>
>>     module Foo : sig
>>       type 'a foo
>>     end = struct
>>       type 'a foo = unit
>>     end
>>
>> so that `int foo` is equal to `float foo`, then your match isn't really
>> exhaustive.
>
> How so?

In order to understand what's going on here it helps to consider two
relations between types: compatibility and equality.

Equality's simple enough: two types are equal if they are the same
(after resolving all alises).  For example,

   float and float are equal

   int and float are not equal

   string -> bool and string -> bool are equal

   int t and int t are equal for any unary type constructor t

   int list and int option are not equal

   float t and int s might be equal if t and s are aliases.  For
example if we have type 'a t = int and type 'a s = 'a then float t and
int s are both equal to int.

Compatibility's a tiny bit more complicated.  Two types are compatible
if it's *possible* to make them equal by some instantiation of
abstract types.  For example:

   equal types are always compatible

   int list and int option are not compatible

   float t and int s are compatible if t and s are abstract types,
since there is a way to define the abtract types that makes float t
and int s equal.

GADTs are mostly about equality.  The fundamental role of GADTs is to
transport type equalities from one part of a program to another.
However, checking compatibility of GADT indexes is sometimes useful as
well.  In particular, checking the compatibility of indexes during
pattern matches allows the compiler to more precisely identify
redundant cases or inexhaustive matches.

We might imagine three possible strategies that the compiler could
take in checking a pattern match involving GADTs for exhaustiveness
and redundancy.  Suppose we have a function that matches over GADTs:

  let f : type a. (a, int) s -> unit = function ...

Then

  (1) The compiler could simply ignore type information and assume
that all cases could potentially be matched.  This was the approach
used in GHC until recently.

  (2) The compiler could check whether there is some instantiation of
locally abstract types that makes the declared type of the case
variable equal to the type of the pattern for each case.  For example,
if s is defined as follows:

      type (_, _) s =
         X : (float, int) s
       | Y : ('b, 'b) s
       | Z : (bool, float) s

   then there are choices for the variable "a" that make (a, int)
equal to the types of X and Y, but no way to choose a type for "a"
that makes (a, int) equal to the type of Z.

      Unfortunately an approach based on equality breaks down when
abstract types are involved.  (I'll show why below.)

   (3) The compiler could take the same approach as in (2), but check
for a way to make types compatible rather than equal.  This is the
approach taken in OCaml.

Let's look at your example.  You have an abstract type Foo.foo and the
following type definition:

    type _ t = A : int Foo.foo t
             | B : float Foo.foo t

Now, suppose you have a function declared like this:

    let f : int t -> unit = function

Then with approach (1) both A and B would be allowed as patterns, and
leaving them off would lead to a warning about exhaustiveness.  With
approach (2) neither A nor B would be allowed, since int t is not
equal to either int Foo.foo t or float Foo.foo t.  With approach (3)
both A and B are allowed as patterns, since int t is compatible with
both int Foo.foo t and float Foo.foo t.  Allowing both A and B as
patterns is the correct option here, since it's possible to call f
with either A or B if foo is instantiated appropriately:

   module F(Foo: sig type _ foo end) =
   struct
       type _ t = A : int Foo.foo t
                    | B : float Foo.foo t
         let f : int t -> unit = function
           A -> ()
         | B -> ()
  end

  include F(struct type _ foo = int end)

  let () = begin f A; f B end

> But you get no warning about an unusable match case with:
>
>    let foo = function A -> () | B -> ()

The reason is that the types of A and B are compatible with each other.

>> Personally, I dislike this behaviour and would prefer both cases to give
>> an error.
>
> What's to dislike? It's rather useful - the constructors of a GADT are partionable by type.

It is indeed useful, and a nice bonus is that it leads to more
efficient code.  However, one (reasonable) point of view is that there
shouldn't be a difference in behaviour between defining something
directly and having a temporary abstraction barrier in between the
definition and the use.  I tend to agree, except that I think the
desirable fix here is not to stop using the compatibility check to
improve pattern matching compilation but to add to the language a way
to express that int Foo.foo and float Foo.foo are incompatible (i.e.
that Foo.foo is injective).

More generally, I think OCaml's whole approach to exhaustiveness
checking for pattern matching with GADTs is an interesting story, and
I'd like to see it written up somewhere (assuming it isn't already).
The Haskell folk are writing a paper about new approach to
exhaustiveness checking for GADT patterns, but the issues that arise
when you have modular abstraction, as in OCaml, are quite different.

Jeremy.

Re: [Caml-list] Match error with abstract types in modules

[Ben Millwood]

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

I think the issue would be substantially mitigated were it not for the
simple fact that [type 'a t] in a signature means "abstract type", whereas
[type 'a t] in a structure means "empty type". The fact that there is no
syntactic distinction, and indeed *no way to make one* caused me a great
deal of confusion some time ago when I had a problem similar to David's.

If I had my way, [type 'a t] would mean "abstract type", and would
therefore be disallowed in structures, and there'd be a separate syntax for
empty types (although I admit not having any great ideas for what it should
be). Then if there were two empty types in a signature, they'd be
incompatible (and injective), just as two types with exposed constructors
are incompatible.

On 24 February 2015 at 19:52, Jeremy Yallop <yallop@gmail.com> wrote:

> On 24 February 2015 at 18:26, David Allsopp <dra-news@metastack.com>
> wrote:
> > Leo White wrote:
> >> > Please could someone remind me what it is about types in modules which
> >> > means that
> >> >
> >> >   module Foo = struct
> >> >     type 'a foo
> >> >   end
> >> >
> >> >   type _ t = A : int Foo.foo t
> >> >            | B : float Foo.foo t
> >> >
> >> >   let foo A = ()
> >> >
> >> > is non-exhaustive pattern matching, but:
> >> >
> >> >   type 'a bar
> >> >
> >> >   type _ u = C : int bar u
> >> >            | D : float bar u
> >> >
> >> >   let bar C = ()
> >> >
> >> > is exhaustive? Or is it actually a bug (given that foo B is a type
> >> error)?
> >> >
> >>
> >> If Foo is replaced with:
> >>
> >>     module Foo : sig
> >>       type 'a foo
> >>     end = struct
> >>       type 'a foo = unit
> >>     end
> >>
> >> so that `int foo` is equal to `float foo`, then your match isn't really
> >> exhaustive.
> >
> > How so?
>
> In order to understand what's going on here it helps to consider two
> relations between types: compatibility and equality.
>
> Equality's simple enough: two types are equal if they are the same
> (after resolving all alises).  For example,
>
>    float and float are equal
>
>    int and float are not equal
>
>    string -> bool and string -> bool are equal
>
>    int t and int t are equal for any unary type constructor t
>
>    int list and int option are not equal
>
>    float t and int s might be equal if t and s are aliases.  For
> example if we have type 'a t = int and type 'a s = 'a then float t and
> int s are both equal to int.
>
> Compatibility's a tiny bit more complicated.  Two types are compatible
> if it's *possible* to make them equal by some instantiation of
> abstract types.  For example:
>
>    equal types are always compatible
>
>    int list and int option are not compatible
>
>    float t and int s are compatible if t and s are abstract types,
> since there is a way to define the abtract types that makes float t
> and int s equal.
>
> GADTs are mostly about equality.  The fundamental role of GADTs is to
> transport type equalities from one part of a program to another.
> However, checking compatibility of GADT indexes is sometimes useful as
> well.  In particular, checking the compatibility of indexes during
> pattern matches allows the compiler to more precisely identify
> redundant cases or inexhaustive matches.
>
> We might imagine three possible strategies that the compiler could
> take in checking a pattern match involving GADTs for exhaustiveness
> and redundancy.  Suppose we have a function that matches over GADTs:
>
>   let f : type a. (a, int) s -> unit = function ...
>
> Then
>
>   (1) The compiler could simply ignore type information and assume
> that all cases could potentially be matched.  This was the approach
> used in GHC until recently.
>
>   (2) The compiler could check whether there is some instantiation of
> locally abstract types that makes the declared type of the case
> variable equal to the type of the pattern for each case.  For example,
> if s is defined as follows:
>
>       type (_, _) s =
>          X : (float, int) s
>        | Y : ('b, 'b) s
>        | Z : (bool, float) s
>
>    then there are choices for the variable "a" that make (a, int)
> equal to the types of X and Y, but no way to choose a type for "a"
> that makes (a, int) equal to the type of Z.
>
>       Unfortunately an approach based on equality breaks down when
> abstract types are involved.  (I'll show why below.)
>
>    (3) The compiler could take the same approach as in (2), but check
> for a way to make types compatible rather than equal.  This is the
> approach taken in OCaml.
>
> Let's look at your example.  You have an abstract type Foo.foo and the
> following type definition:
>
>     type _ t = A : int Foo.foo t
>              | B : float Foo.foo t
>
> Now, suppose you have a function declared like this:
>
>     let f : int t -> unit = function
>
> Then with approach (1) both A and B would be allowed as patterns, and
> leaving them off would lead to a warning about exhaustiveness.  With
> approach (2) neither A nor B would be allowed, since int t is not
> equal to either int Foo.foo t or float Foo.foo t.  With approach (3)
> both A and B are allowed as patterns, since int t is compatible with
> both int Foo.foo t and float Foo.foo t.  Allowing both A and B as
> patterns is the correct option here, since it's possible to call f
> with either A or B if foo is instantiated appropriately:
>
>    module F(Foo: sig type _ foo end) =
>    struct
>        type _ t = A : int Foo.foo t
>                     | B : float Foo.foo t
>          let f : int t -> unit = function
>            A -> ()
>          | B -> ()
>   end
>
>   include F(struct type _ foo = int end)
>
>   let () = begin f A; f B end
>
> > But you get no warning about an unusable match case with:
> >
> >    let foo = function A -> () | B -> ()
>
> The reason is that the types of A and B are compatible with each other.
>
> >> Personally, I dislike this behaviour and would prefer both cases to give
> >> an error.
> >
> > What's to dislike? It's rather useful - the constructors of a GADT are
> partionable by type.
>
> It is indeed useful, and a nice bonus is that it leads to more
> efficient code.  However, one (reasonable) point of view is that there
> shouldn't be a difference in behaviour between defining something
> directly and having a temporary abstraction barrier in between the
> definition and the use.  I tend to agree, except that I think the
> desirable fix here is not to stop using the compatibility check to
> improve pattern matching compilation but to add to the language a way
> to express that int Foo.foo and float Foo.foo are incompatible (i.e.
> that Foo.foo is injective).
>
> More generally, I think OCaml's whole approach to exhaustiveness
> checking for pattern matching with GADTs is an interesting story, and
> I'd like to see it written up somewhere (assuming it isn't already).
> The Haskell folk are writing a paper about new approach to
> exhaustiveness checking for GADT patterns, but the issues that arise
> when you have modular abstraction, as in OCaml, are quite different.
>
> Jeremy.
>
> --
> 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: 9358 bytes --]

Re: [Caml-list] Match error with abstract types in modules

[Leo White]

Ben Millwood <bmillwood@janestreet.com> writes:

> I think the issue would be substantially mitigated were it not for the simple fact that [type 'a t] in a signature
> means "abstract type", whereas [type 'a t] in a structure means "empty type". The fact that there is no syntactic
> distinction, and indeed *no way to make one* caused me a great deal of confusion some time ago when I had a problem
> similar to David's.

You can make an empty type (or at least a type for which there are no
expressions) using:

type 'a t = private T

RE: [Caml-list] Match error with abstract types in modules

[David Allsopp]

Leo White wrote:
> Ben Millwood <bmillwood@janestreet.com> writes:
> 
> > I think the issue would be substantially mitigated were it not for the
> > simple fact that [type 'a t] in a signature means "abstract type",
> > whereas [type 'a t] in a structure means "empty type". The fact that
> > there is no syntactic distinction, and indeed *no way to make one*
> > caused me a great deal of confusion some time ago when I had a problem
> > similar to David's.

The context of my original problem was the initially confusing assertion by the compiler that two "different" BatSet.t uses were the same. I guessed that what I was seeing was part of the "easy to shoot yourself in the foot" comment in its documentation!

> You can make an empty type (or at least a type for which there are no
> expressions) using:
> 
> type 'a t = private T

The obvious "solution" with sets is to use the functor version therefore and have a module for each point (I believe that's 50% of the reason for doing it - the other being that you don't need to store the comparison function in the value itself), but is there (in theory) a relatively easy kind of annotation which could be added to type 'a t in a signature which would tell the compiler that 'a t and 'b are equal and compatible iff 'a and 'b are equal/compatible but still remain abstract?


David

RE: [Caml-list] Match error with abstract types in modules

[David Allsopp]

Leo White wrote:
> >> so that `int foo` is equal to `float foo`, then your match isn't
> >> really exhaustive.
> >
> > How so?
> 
> Both constructors would then have the same type. Since it is possible they
> both have the same type, you need to match on both of them.
> 
> > What's (very) confusing to me is that it seems to permit nonsensical
> > matches without warning. In both the unconstrained and constrained
> > versions of Foo, the resulting type of the function [foo] is [int
> > Foo.foo t -> unit] so [foo B] is always rejected. But you get no
> > warning about an unusable match case with:
> >
> > let foo = function A -> () | B -> ()
> >
> 
> This is because `foo B` may not always be rejected. Consider the following
> code:
> 
>     module F (Foo : sig type 'a foo end) = struct
> 
>       type _ t = A : int Foo.foo t
>            | B : float Foo.foo t
> 
>       let foo = function
>         | A -> ()
>         | B -> ()
> 
>       (* [foo B] would be an error here *)
> 
>     end
> 
>     module M = F(struct type 'a foo = unit end)
> 
>     (* But out here it is fine *)
>     let () = M.foo M.B
> 
> > although
> >
> > let foo = function A | B -> ()
> >
> > unsurprisingly does not type.
> 
> That's due to GADTs not currently being compatible with or-patterns, it is
> not related to the injectivity issues you are having.
> 
> >> In the second version, the compiler cheats. Since `bar` is definied
> >> in the same module, it knows that the abstract `bar` type it can see
> >> is actually the definition, not just an abstraction of a type defined
> >> elsewhere, so it knows that `int bar` cannot equal `float bar`.
> >>
> >> Personally, I dislike this behaviour and would prefer both cases to
> >> give an error.
> >
> > What's to dislike?
> 
> Giving different behviour based on whether something is defined in the
> same module is anti-modular, and confuses people when they try to split
> their code across different modules.
> 
> > It's rather useful - the constructors of a GADT are partionable by
> > type.
> 
> That is indeed useful, but only really works in OCaml if you expose the
> definitions of these types, so that OCaml can see that they are definitely
> not the same type. This is why you see people use:
> 
>     type z = Z
> 
>     type 'a s = S

It turns out that this very helpful explanation has inadvertently answered an issue I had a while ago where I'd ended up leaving a comment in my code that I didn't fully understand why I needed type t = T, type s = S for doing this!

> when doing type-level arithmetic. By giving types with incompatible
> definitions, rather than abstract types, OCaml can safely conclude they
> are not the same type.
> 
> > What caught me out was that two constructors with distinct types (in
> > my actual use with different instantiations of 'a
> > BatSet.t) were being regarded as equal in terms of pattern matching.
> > I'd be quite happy if a type annotation were necessary to make it
> > explicit that I meant to do it:
> >
> > let foo (key : int Foo.foo t) =
> >   match key with A -> ()
> >
> > Especially with that explicit type, I find it very odd to get a
> > warning about a constructor whose type is not permitted in this
> > context and so cannot be matched.
> 
> The problem is that OCaml has no way to know that `int Foo.foo` is not
> equal to `float Foo.foo` so it must insist that you include a case for it.
> OCaml also doesn't know that `int Foo.foo` does equal `float Foo.foo` so
> it can't let you call `foo Foo.B` either.

Ah, I see - thanks!


David

Re: [Caml-list] Match error with abstract types in modules

[Gabriel Scherer]

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

>
> is there (in theory) a relatively easy kind of annotation which could be
> added to type 'a t in a signature which would tell the compiler that 'a t
> and 'b are equal and compatible iff 'a and 'b are equal/compatible but
> still remain abstract?


Yes, this is exactly the point of "injectivity" which has been discussed at
length in
  http://caml.inria.fr/mantis/view.php?id=5985
and summarized in a (rather difficult to follow for the non-expert) talk by
Jacques Garrigue at the OCaml Meeting 2013 in Boston,
  abstract: http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf
  slides: https://ocaml.org/meetings/ocaml/2013/slides/garrigue.pdf

It would not be difficult to teach the type-checker about injectivity, but
there is no concrete syntax in the language to discuss it, and it is not
easy to design a good one (which is why it has not been added yet). The
difficult question is whether users should add an extra mark to explicitly
require injectivity (like we do for covariance for example), or whether it
should be assumed when using the default (type 'a t) notation, with an
explicit mark to allow *non*-injectivity.

On Wed, Feb 25, 2015 at 9:41 AM, David Allsopp <dra-news@metastack.com>
wrote:

> Leo White wrote:
> > Ben Millwood <bmillwood@janestreet.com> writes:
> >
> > > I think the issue would be substantially mitigated were it not for the
> > > simple fact that [type 'a t] in a signature means "abstract type",
> > > whereas [type 'a t] in a structure means "empty type". The fact that
> > > there is no syntactic distinction, and indeed *no way to make one*
> > > caused me a great deal of confusion some time ago when I had a problem
> > > similar to David's.
>
> The context of my original problem was the initially confusing assertion
> by the compiler that two "different" BatSet.t uses were the same. I guessed
> that what I was seeing was part of the "easy to shoot yourself in the foot"
> comment in its documentation!
>
> > You can make an empty type (or at least a type for which there are no
> > expressions) using:
> >
> > type 'a t = private T
>
> The obvious "solution" with sets is to use the functor version therefore
> and have a module for each point (I believe that's 50% of the reason for
> doing it - the other being that you don't need to store the comparison
> function in the value itself), but is there (in theory) a relatively easy
> kind of annotation which could be added to type 'a t in a signature which
> would tell the compiler that 'a t and 'b are equal and compatible iff 'a
> and 'b are equal/compatible but still remain abstract?
>
>
> David
>
> --
> 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: 4221 bytes --]