Re: [Caml-list] variance/injectivity/uniqueness annotations for types

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2016/03/11 15:53, Milan Stanojević wrote:
> 
> I ran into some variance/injectivty issues in my code, plus I saw some
> recent question here, and I was wondering if there was any progress on
> adding syntax so types can be annotated with proper information (as
> discussed in http://caml.inria.fr/mantis/view.php?id=5985).
> 
> I guess we don't really need new syntax, we can just use attributes
> (e.g. [@@unique] or [@@injective])
> 
> I searched mantis a bit but I don't see anything new (maybe I didn't
> search hard enough).


The situation seems to be stuck currently, waiting for concrete examples
where this is really needed, and also for a good syntax.
Indeed, in other discussions, there seemed to be an agreement that
attributes were not very good for changing the type system itself, as they
are somehow outside of the language. Moreover, injectivity would be rather
heavy, as this is a per-parameter property. Concerning uniqueness,
Alain Frisch made some interesting suggestion of using a global name or
path to make types distinguishable.

Jacques Garrigue