> > 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 wrote: > Leo White wrote: > > Ben Millwood 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 >