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

Syntax shortcut for putting a type annotation on a record field #6806

Closed
vicuna opened this Issue Mar 10, 2015 · 17 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Mar 10, 2015

Original bug ID: 6806
Reporter: @sliquister
Assigned to: @diml
Status: closed (set by @xavierleroy on 2017-02-16T14:16:21Z)
Resolution: fixed
Priority: normal
Severity: feature
Fixed in version: 4.03.0+dev / +beta1
Category: ~DO NOT USE (was: OCaml general)
Related to: #6800
Monitored by: @diml jmeber @hcarty

Bug description

I'd like the syntax for record literals to be extended so one can write:

{ f1 : typ = e } to mean { f1 = (e : typ) }
{ f1 : typ } to mean { f1 = (f1 : typ) }

(see attached patch)
This is because I have a preprocessor that transforms a restricted subset
of expressions (mostly data constructors) into sexps, but any expression
can be used provided its type is given.
So we frequently end up writing things like:

<:structural_sexp< { a = (a : int); b = (b : int) } >>

which I would prefer to write:

<:structural_sexp< { a : int; b : int } >>

(which of course I could do myself with camlp4 right now but not when it becomes a ppx rewriter)

File attachments

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 11, 2015

Comment author: @gasche

Looks very reasonable to me.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 11, 2015

Comment author: @alainfrisch

I like it too, it's very coherent with "let x : t = e" or "module X : S = E".

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 11, 2015

Comment author: @sliquister

(as a side effect of reusing the "type_constraint" nonterminal, the patch also adds the other forms { a :> int } and { a : int :> int }, which are also allowed on let bindings:

let x :> [ A | B ] = (A : [ A ]);;

val x : [ A | B ] = `A

let x : [ A ] :> [ A | B ] = A;;

val x : [ A | B ] = `A
)

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 12, 2015

Comment author: @garrigue

I have mixed feelings on this one.
On the one hand, this is coherent with the rest of the language, in particular labeled arguments.
On the other hand, records are defined, so usually there is no need for type annotations there...
Also, the patch is only for expressions. One would expect the same behavior in patterns (should be easy).

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 12, 2015

Comment author: @sliquister

You're right, I attached a new patch:

fun { contents : int } -> contents;;

  • : int ref -> int =

And yes I agree type annotations are not super useful on records in general, that's why I explained why I wanted this piece of syntax. There could be cases like with references where the record is polymorphic in some fields but that's not too common.

While I was there I tried adding a type annotation before the "->" of "fun" (as mentioned in some other issue), but there is a conflict between the arrow in the construct and the one in types ("fun x : int -> int"), so I stopped there instead of figuring out how to convince the parser to reduce.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 12, 2015

Comment author: @gasche

It's very nice of you to work on this. You should use the class 'simple_core_type' (which does not allow "foo -> bar" unparenthesized) rather than 'core_type'.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Mar 12, 2015

Comment author: @sliquister

Fair enough, I added it (in the same patch as the other changes but the one line could be extracted).

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Aug 23, 2015

Comment author: @sliquister

Any chance the patch can go in, in the end?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Aug 24, 2015

Comment author: @gasche

Thanks for the reminder.

I think these are two separate changes that should go in two separate patches.

Besides, I would like to see the new syntax introduced exercised somewhere in the testsuite. Could you convert some, but not all, uses of (fun .. -> (x : ..)) to the new syntax (for example the one in typing-warnings/coercions.ml), and add the record syntax to tests/exotic-syntax/exotic.ml?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Aug 25, 2015

Comment author: @garrigue

Honestly, I'm not yet convinced of how much useful it is.
Did we have a discussion about the need to be able to write type annotations in every special compact form? Particularly when the type can actually be inferred?
For records usually the type annotation would go on the whole record, not on a specific field.

Note that some people already have preprocessors that work after type-checking, and eventually we will probably have a standard way to do that.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Aug 25, 2015

Comment author: @gasche

On the other hand, it serves a clearly expressed user purpose now (whereas there is no time estimation for when typedtree will be usable enough for non-experts to process), and it is a very simple patch, which does not significantly increase the complexity of the parser -- the only show-stopper would be if it added conflicts, but I assume that sliquister checked and that it did not. I would rather be in favor of merging (why not?).

I am under the impression that there is consensus that the other part of the change that sliquister included in the same patch, (fun x y : foo -> e) as a synonym of (fun x y -> (e : foo)), is very useful. At least there was in the last GADT discussion where this feature was evoked.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Aug 25, 2015

Comment author: @lpw25

The difference between let bindings and record field bindings frequently annoys me (the other aspect is not being able to write function field definitions like { f x = x }), so I'm in favour of this change.

It is not hugely useful, but it has a low cost and improves the consistency of the syntax.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Aug 25, 2015

Comment author: @sliquister

To be clear, there is no record type corresponding to the record expression. So a post-typing hook wouldn't work, since the code wouldn't type to begin with. Perhaps a hook during typing on uninterpreted extension would work, by synthetizing the record definition, but it comes with the problem of ambiguity, since not all types that unify are serialized the same way.
Not having a record type is most of the interest of the syntax extensions, since they would be one off definitions.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Aug 26, 2015

Comment author: @sliquister

I added the tests you suggested and split the two changes.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 4, 2015

Comment author: @diml

For records usually the type annotation would go on the whole record, not on a specific field.

Now that type annotations are used for disambiguation I think it's useful to be able to put annotations in more places. I recently wrote some code where I put a type annotation on a specific field in a record pattern. It was possible to put the annotation on the whole record pattern but it was heavier.

On another note the syntax is already relaxed in other places that don't make sense for OCaml but might for ppx rewriters. For instance you can write "for a, b = ..." which is accepted by the parser but later rejected by the typer. This change is useful for both ppx rewriters and regular OCaml, so it's one more reason to accept it.

Unless other objections I'm planning to merge the patches.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 4, 2015

Comment author: @gasche

Thanks!

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 5, 2015

Comment author: @diml

I merged the two patches in trunk:

26657d5
6676784

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.