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

simplify using gadt with lambda #6800

Closed
vicuna opened this issue Mar 2, 2015 · 14 comments
Closed

simplify using gadt with lambda #6800

vicuna opened this issue Mar 2, 2015 · 14 comments

Comments

@vicuna
Copy link

vicuna commented Mar 2, 2015

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/or fail2 to be accepted by the typer ?

type _ t =
  | Int : int t
  | String : string t

(* This works as expected *)
let work1 (type s) (x : s t) : s =
  match x with
  | Int -> 0
  | String -> ""

let (>>=) : 'a -> ('a -> 'b) -> 'b = fun x f -> f x

(* This doesn't *)
let fail1 (type s) (x : s t) : s =
  x >>= fun x ->
  match x with
  | Int -> 0
  | String -> ""

(* giving a hint for the type of x doesn't work *)  
let fail2 (type s) (x : s t) : s =
  x >>= fun x ->
  match (x : s t) with
  | Int -> 0
  | String -> ""

(* giving a hint for the return of the match works.
   however the following does not because the first
   case got typed first *)
let fail3 (type s) (x : s t) : s =
  x >>= fun x ->
  match x with
  | Int -> 0
  | String -> ("" : s)

let work2 (type s) (x : s t) : s =
  x >>= fun x ->
  match x with
  | Int -> (0 : s)
  | String -> ""

File attachments

@vicuna
Copy link
Author

vicuna commented Mar 3, 2015

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.

@vicuna
Copy link
Author

vicuna commented Mar 4, 2015

Comment author: @damiendoligez

As far as I can tell, the "proper place" for a GADT annotation is around the match itself, which suggests the we should introduce a syntax for type annotations where the type comes first: instead of

  (expr : type)

one could write

  (type ??? expr)

The problem is, I don't know what kind of punctuation (or keyword) would be appropriate for this.

@vicuna
Copy link
Author

vicuna commented Mar 5, 2015

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.

@vicuna
Copy link
Author

vicuna commented Mar 6, 2015

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 -> "";;

@vicuna
Copy link
Author

vicuna commented Mar 11, 2015

Comment author: @alainfrisch

I would like is to be able to write "fun x .. z : ty -> ..."

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.

(ty ??? expr)

Even if we find a good pick for "???", I'm afraid this would result in many conflicts in the grammar.

What about:

  (: ty) expr

?

With it, one could write e.g.:

  (: arg_ty -> ret_ty) function
    | p1 -> e1
    | ...

@vicuna
Copy link
Author

vicuna commented Mar 11, 2015

Comment author: @garrigue

I concur. Both fun x ... z : ty -> ... and (: ty) ... make sense.
Note however that there is a slight difficulty the later, as if we see (: ty) as a function, only a simple expression can occur after it. I.e., you would have to write:

 (: arg_ty -> ret_ty) (function
    | p1 -> e1
    | ...)

From a parsing point of view there is of course no problem in being more laxist.
Anyway, I kind of see that as a detail, since the fun x ... z : ty -> ... covers most of the cases not handled yet.

@vicuna
Copy link
Author

vicuna commented Dec 2, 2015

Comment author: @alainfrisch

Note that "fun x : ty -> ..." has been implemented as part of #6806.

@vicuna
Copy link
Author

vicuna commented Dec 2, 2015

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;;

@github-actions
Copy link

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.

@github-actions github-actions bot added the Stale label May 11, 2020
@garrigue
Copy link
Contributor

I think that #6806 solves this issue. Or is there something left?

@gasche
Copy link
Member

gasche commented May 11, 2020

Well I still agree that (: ty) expr would be nice syntax. @alainfrisch, would you like to open a Pull Request to propose it? (Or we could discuss with other people to see if we want the syntax before implementing, which I suppose would require a fair amount of rebasing work, at least in the parser.)

@garrigue
Copy link
Contributor

I would not characterise (: ty) expr as nice.
Is it supposed to look like a C coercion?
Then I suppose we would also need (:> ty) and (: ty :> ty') for completeness, but what is the real benefit compared to the current syntax, which at least makes the target of the coercion explicit?

@gasche
Copy link
Member

gasche commented May 12, 2020

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 (: foo -> bar) function ..., which is not possible with current syntax.

This would also be useful with the new binding operators let* p = def in body (typically for monadic bind): for now we do not support the syntax let* p : ty = def in body, which is a bit tricky as it is unclear whether we should expect the type of p (eg. 'a) or the type of def (eg. 'a m). On the other hand, let* p = (: ty) def in body is an almost-readability-preserving version of the same thing: it's a completely local reformulation, whereas let* p = (def : ty) in body is impractical in many cases (the type is too far from the place where it would improve readability).

@github-actions github-actions bot removed the Stale label Jun 15, 2020
@github-actions
Copy link

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

3 participants