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
simplify using gadt with lambda #6800
Comments
Comment author: @gasche Hugo's question is about expected type propagation, but one think I would like is to be able to write "fun x .. z : ty -> ..." to signify the expected return type of a function abstraction. This would allow to conveniently write the GADT-annotation at the proper place here, but would also be helpful in other situations. Note that "fun x .. z -> ( ... : ty )" is available but doesn't scale as well in terms of readability. |
Comment author: @damiendoligez As far as I can tell, the "proper place" for a GADT annotation is around the
one could write
The problem is, I don't know what kind of punctuation (or keyword) would be appropriate for this. |
Comment author: @gasche Not quite: GADT annotations need to share a type constructor (the "type a" kind of variables) between the scrutinee of the match and the return type of the clauses. This cannot be done a posteriori if the scrutinee is already in context, so it occurs on fun-bindings (sometimes artificially introduced for this purpose, it is the so-called "convoy pattern") rather than the match itself. |
Comment author: @hhugo Also let work3 (type s) f g (x : s t) : s =
x >>= fun x ->
match x with
| Int -> f 0
| String -> g "";;
let fail4 (type s) f g (x : s t) : s =
x >>= fun x ->
match x with
| Int -> f 0
| String -> "";;
let fail5 (type s) (f : int -> int) g (x : s t) : s =
x >>= fun x ->
match x with
| Int -> f 0
| String -> g "";;
let f_infered_with_s (type s) f (x : s t) : s =
x >>= fun x ->
match x with
| Int -> (f 0 : s)
| String -> "";;
let f_infered_with_int (type s) f (x : s t) : s =
x >>= fun x ->
match x with
| Int -> (f 0 : int :> s)
| String -> "";; |
Comment author: @alainfrisch
I fully support that. Even more importantly, it would also be useful to allow specifying the argument and/or return types in "function p1 -> e1 | ... | pn -> en" with something lighter than "((function ...) : t -> s)". Specifying input/output types has become more important since the introduction of type-based disambiguation for constructors. At least, if we had a prefix form for type constraint as Damien suggests, this be already be better.
Even if we find a good pick for "???", I'm afraid this would result in many conflicts in the grammar. What about:
? With it, one could write e.g.:
|
Comment author: @garrigue I concur. Both
From a parsing point of view there is of course no problem in being more laxist. |
Comment author: @alainfrisch Note that "fun x : ty -> ..." has been implemented as part of #6806. |
Comment author: @alainfrisch Attached a patch which implements prefix type constraint syntax "(:ty) expr". This is not parsed as function application, and it allows "expr" to be e.g. a pattern matching or a function: (: _ -> int) fun x -> x;; |
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. |
I think that #6806 solves this issue. Or is there something left? |
Well I still agree that |
I would not characterise |
Whenever the type is small and the expression is large, it is very useful to be able to annotate with the type going first. See the example of @alainfrisch above about being able to write This would also be useful with the new binding operators |
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: 6800
Reporter: @hhugo
Status: confirmed (set by @damiendoligez on 2015-03-03T20:15:36Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.1
Target version: undecided
Category: typing
Related to: #6806
Monitored by: @gasche @yallop @hcarty
Bug description
Would it be possible to have the
fail1
add/orfail2
to be accepted by the typer ?File attachments
The text was updated successfully, but these errors were encountered: