Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005867OCamlOCaml typingpublic2012-12-26 23:332013-04-23 02:09
Reportermbarbin 
Assigned Togarrigue 
PrioritynoneSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.00.1 
Target VersionFixed in Version 
Summary0005867: there is no syntax to bind a type variable introduced in a gadt pattern
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)

TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

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

- 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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker