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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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