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

Adding expressiveness to polymorphic variants #5924

Closed
vicuna opened this issue Feb 17, 2013 · 1 comment
Closed

Adding expressiveness to polymorphic variants #5924

vicuna opened this issue Feb 17, 2013 · 1 comment

Comments

@vicuna
Copy link

vicuna commented Feb 17, 2013

Original bug ID: 5924
Reporter: jpdeplaix
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:30Z)
Resolution: won't fix
Priority: normal
Severity: minor
Version: 4.00.1
Category: typing

Bug description

Hi,

I'd like to be able to do the kind of functions described here:
http://caml.inria.fr/pub/docs/manual-ocaml/manual006.html

This function:
let f = function A -> C | B -> D | x -> x
is typed as:
val f : ([> A | B | C | D ] as 'a) -> 'a
but a more fine type would be:
val f : [ A | B | 'r ] -> [ C | D | 'r ]

gasche already told me that it is choice made by the caml developers, but I'm very interested in making such functions. So, if someone can add this expressiveness to the language or explain me why it is really not possible to add this, it would be very helpful.

@vicuna
Copy link
Author

vicuna commented Feb 18, 2013

Comment author: @garrigue

This is not strictly impossible to do that, but this requires huge changes in the type system.

  • since we would have explicit row variables, you need to introduce a notion of type variable sort

  • one would need to add exclusion information on row variables. For instance, with your example,
    we would the information that 'r cannot contain any of A, B, C, D. This is implicit in the type
    of f, but it can become hidden in more complex functions, so it would have to be explicit.

  • typing of pattern-matching would have to compute remaining cases, which is not trivial in the general case.

For all these reasons there is no plan to introduce something like that at this point.

If you are interested in this subject, you can read papers by Didier Rémy and, more recently, Matthias Blume.

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

No branches or pull requests

2 participants