0005867: there is no syntax to bind a type variable introduced in a gadt pattern

(0008651)
garrigue (manager)
2012-12-27 03:47

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.

(0008668)
sliquister (reporter)
2012-12-29 17:46

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.

(0008670)
mbarbin (reporter)
2012-12-29 23:59
edited on: 2012-12-30 00:00

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

(0008994)
mbarbin (reporter)
2013-03-19 17:51

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)

Issue History
Date Modified	Username	Field	Change
2012-12-26 23:33	mbarbin	New Issue
2012-12-27 03:47	garrigue	Note Added: 0008651
2012-12-27 03:47	garrigue	Assigned To	=> garrigue
2012-12-27 03:47	garrigue	Status	new => acknowledged
2012-12-29 17:46	sliquister	Note Added: 0008668
2012-12-29 23:59	mbarbin	Note Added: 0008670
2012-12-30 00:00	mbarbin	Note Edited: 0008670	View Revisions
2012-12-30 00:00	mbarbin	Note Edited: 0008670	View Revisions
2013-03-19 17:51	mbarbin	Note Added: 0008994
2013-04-23 02:09	garrigue	Relationship added	child of 0005998

Notes
(0008651) garrigue (manager) 2012-12-27 03:47	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.

(0008668) sliquister (reporter) 2012-12-29 17:46	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.

(0008670) mbarbin (reporter) 2012-12-29 23:59 edited on: 2012-12-30 00:00	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

(0008994) mbarbin (reporter) 2013-03-19 17:51	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)