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

lower the usage of quote in the syntax of type variables #7464

Closed
vicuna opened this issue Jan 23, 2017 · 5 comments
Closed

lower the usage of quote in the syntax of type variables #7464

vicuna opened this issue Jan 23, 2017 · 5 comments

Comments

@vicuna
Copy link

vicuna commented Jan 23, 2017

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).

@vicuna
Copy link
Author

vicuna commented Jan 23, 2017

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.

@vicuna
Copy link
Author

vicuna commented Jan 23, 2017

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
without quote could be allowed there.

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 =
fun cmp a ->
let rec fn : a list -> a list = function
| [] -> []
| b :: l -> if cmp a b then a :: l else b :: fn l
in fn

Remain the pb of OCaml messages, but this could be treated separatly.

@vicuna
Copy link
Author

vicuna commented Jan 31, 2017

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.

@vicuna
Copy link
Author

vicuna commented Feb 10, 2017

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 (type a) form, without ever mentioning type variables in source code. From this perspective, allowing type a list does not add much complexity to the language, and makes this choice possible/coherent.

(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.

@github-actions
Copy link

github-actions bot commented May 9, 2020

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.

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

1 participant