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

there is no syntax to bind a type variable introduced in a gadt pattern #5867

Closed
vicuna opened this issue Dec 26, 2012 · 4 comments
Closed
Assignees
Labels
duplicate feature-wish typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Dec 26, 2012

Original bug ID: 5867
Reporter: mbarbin
Assigned to: @garrigue
Status: closed (set by @alainfrisch on 2015-12-07T08:55:56Z)
Resolution: duplicate
Severity: feature
Version: 4.00.1
Category: typing
Duplicate of: #7074
Child of: #5998
Monitored by: @gasche "Julien Signoles" @hcarty @alainfrisch

Bug description

(* Given these two ways of encoding an existential type *)

type t = A : 'a -> t

module type S = sig
type a
val a : a
end

(* one can easily go from one to the other *)

let to_gadt (module S : S) = A S.a

(* however, the other way around lacks of a syntax to name the ex#i type: *)

let f = function
| A a ->
(fun (type aa) (a:aa) ->
(module (struct
type a = aa
let a = a
end) : S)
) a

(* since the scope of 'a would be the entire function the following does not work and complain that the type ex#i would escape its scope *)

let f = function
| A (a:'a) ->
(module (struct
type a = 'a
let a = a
end) : S)

@vicuna
Copy link
Author

vicuna commented Dec 27, 2012

Comment author: @garrigue

This is a well known problem since the introduction of GADTs.
However, there is currently no agreement on what the syntax should be.

Thank you for providing a nice motivating example, together
with a (I admit verbose) workaround.
Stay tuned in.

@vicuna
Copy link
Author

vicuna commented Dec 29, 2012

Comment author: @sliquister

What about:
let f = function
| A a ->
(fun (type aa where a : aa) ->
(module (struct
type a = aa
let a = a
end) : S)
)

Or maybe:

let f = function
| A a ->
let type aa where a : aa in
(module (struct
type a = aa
let a = a
end) : S)

This is not really shorter, though, but the verbosity here is mostly because of the module in the first place.

@vicuna
Copy link
Author

vicuna commented Dec 29, 2012

Comment author: mbarbin

Here is another proposal that tries to relate to existing fragments of the language :

let f (type a) (type b) (a:a) (b:b) = ...
let f (type a) = fun (a:a) -> ...

let f = function
| A (type a) (a:a) ->
(module (struct
type a = a
let a = a
end) : S)

as in the existing examples, the (type $id)* is placed between the function name and the arguments, where here it is between the constructor name and the arguments

@vicuna
Copy link
Author

vicuna commented Mar 19, 2013

Comment author: mbarbin

I just noticed page 6 of http://www.math.nagoya-u.ac.jp/~garrigue/papers/inria2011.pdf

let f = function
| type a. A (a:a) ->
(module (struct
type a = a
let a = a
end) : S)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
duplicate feature-wish typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants