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
lower the usage of quote in the syntax of type variables #7464
Comments
Comment author: @gasche Currently there is an important technical difference between abstract type constructors (a) and inference variable ('a). I think we should careful about changes that improve convenience by blurring the distinction: if the concepts are not properly unified, there is a risk of the distinction leaking out in more advanced use-cases in way that make the system more confusing. |
Comment author: Christophe Raffalli My proposal is for type definition. In a type definition 'a is neither an abstract type constructor nor an inference variable. So the shorter syntax This would allow the code I use with my student to use only one syntax without quote (and this would be true for most code ?). I prefer teaching with the new syntax because it captures more bug by allowing to write a precise type for inner function like in let insert : type a. (a -> a -> bool) -> a -> a list -> a list = Remain the pb of OCaml messages, but this could be treated separatly. |
Comment author: gerd Frankly, I wouldn't recommend the new "syntax" to beginners. Because it's not only syntax. You are also enabling some features of the language that are hard to explain, like GADTs and polymorphic recursion. Old-style type variables are limited in so far (a) the compiler controls where they are bound, usually the next "let", and (b) the unification algorithm is restricted (no generation of GADT existentials, no polymorphic recursion). I also think there is something to do in order to make clearer when to use which style. However, your example of datatype definitions is a bad example, because normal (non-GADT) types are limited to uniform recursion, and hence the old-style type variables are semantically the right ones. (In some sense, there should be a symmetry: if you define the type with a certain sort of type variable, this sort should also be used by functions for this type.) Where I see room for improvement are polymorphic record fields and polymorphic methods. I think we can in deed use the new variables, e.g. method poly : type t . t -> t instead of method poly : 't . 't -> 't Also that old-style variables are used for GADT definitions is not optimal and looks messy. But I'm not an expert in such questions and there might be issues I'm not aware of. The question is then where to draw the line between the two styles, and I think we also need better names, like "auto-generalizing type variable" and "advanced polymorphism type variable" (feel free to suggest better names). The name should make clear for which purpose the variable is used best. |
Comment author: @gasche I had a discussion about this with Christophe and I am mellowing out to the idea. His point is that having this feature available would make it possible to teach students with only the explicit (I'm not convinced about error messages, though. In fact, one could argue that type variables occurring in error messages are really (flexible) unification variables rather than (rigid) polymorphic variables, so they should keep appearing as 'a. It is possible to faithfully explain those 'a to students as "a special name for an unknown variable not yet inferred by the type-checker"; it is clear why those could appear in error messages even if they are not used in the source.) This would maybe suggest to more generally start thinking of (a) as a "rigid polymorphic variable" and ('a) as a "flexible inference variable", instead of calling them "locally abstract types" and "type variables". I see this as redefining the boundaries, rather than blurring the lines. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 7464
Reporter: Christophe Raffalli
Status: acknowledged (set by @damiendoligez on 2017-02-27T14:45:52Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.04.0
Category: language features
Monitored by: @gasche gerd
Bug description
With the new syntax
let f : type a.a -> a ...
'a are mostly (only ?) used in type definition and messages from OCaml.
I think it is possible and beneficial to allow type definition without
quote like in
type a option = None | Some of a
Then, it should also be possible to remove quote from messages too (one must look for a fresh symbol, or use a number like for existential type when
the name is not fresh).
The text was updated successfully, but these errors were encountered: