Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support injectivity annotations (4.12) #1444

Closed
emillon opened this issue Aug 7, 2020 · 0 comments · Fixed by #1523
Closed

Support injectivity annotations (4.12) #1444

emillon opened this issue Aug 7, 2020 · 0 comments · Fixed by #1523
Milestone

Comments

@emillon
Copy link
Collaborator

emillon commented Aug 7, 2020

Injectivity annotations are a new feature in 4.12:

  • #9500, #9727: Injectivity annotations
    One can now mark type parameters as injective, which is useful for
    abstract types:
    module Vec : sig type !'a t end = struct type 'a t = 'a array end
    On non-abstract types, this can be used to check the injectivity of
    parameters. Since all parameters of record and sum types are by definition
    injective, this only makes sense for type abbreviations:
    type !'a t = 'a list
    (Jacques Garrigue, review by Jeremy Yallop and Leo White)

ocaml/ocaml#9500
ocaml/ocaml#9727

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants