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

[David Allsopp <dra-news@metastack.com>]

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