[GHC] #7961: Remove restrictions on promoting GADT's
#7961: Remove restrictions on promoting GADT's -----------------------------+---------------------------------------------- Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Blockedby: Blocking: | Related: #6204 -----------------------------+---------------------------------------------- (Also allow the promotion of data types whose kind is not (* -> ... -> *)) I have been using -XDataKinds lately to explore the sorts of dependently typed programming that are currently possible in GHC. I am particularly interested in DSL's and embedding other languages' type systems into Haskell so that GHC can help verify the correctness of the program fragments I construct for those languages. From my point of view as an end-user, the restrictions on what data get promoted is inconsistent and oftentimes annoying to deal with. There are two related issues on my end: 1. The restriction that a data type cannot have a kind mentioning a promoted kind means that the way I stratify my type machinery impacts whether or not GHC will promote everything as I would like. 2. The inability to use promoted GADT's forces me to encode relationships between my type building blocks in trickier ways, and sometimes I am simply unable to come up with an alternative. I have found that these issues get in my way as a programmer of modest skill. Oftentimes I will explore a particular design but be forced to abandon it because my "natural" line of reasoning runs into GHC's restrictions. With sufficient cleverness you can do quite a lot of impressive stuff with the current system, but I am often not sufficiently clever nor am I equipped to determine when something is outright ''impossible''. Lifting these restriction, from ''my'' point of view, would simplify the machinery a great deal and allow me to do type-level programming that is currently out of my reach. It would make the kind extensions more uniform and more complete to us end-users. #6204 would complete them in another way. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's -----------------------------+---------------------------------------------- Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Blockedby: Blocking: | Related: #6204 -----------------------------+---------------------------------------------- Comment(by carter): Hey Dan, could you give some examples of "code you'd want to be able to write" vs "ways you have to encode it as ghc currently stands"? Also, the ticket number your refer to doesn't exist, which ticket do you mean? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's -----------------------------+---------------------------------------------- Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Component: Compiler Version: 7.6.3 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Blockedby: Blocking: | Related: #6204 -----------------------------+---------------------------------------------- Comment(by danharaj): Woops. That should be #6024. I will post a nice code example when I can. It is a bit late here at the moment. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Changes (by simonpj): * difficulty: => Unknown Old description:
(Also allow the promotion of data types whose kind is not (* -> ... -> *))
I have been using -XDataKinds lately to explore the sorts of dependently typed programming that are currently possible in GHC. I am particularly interested in DSL's and embedding other languages' type systems into Haskell so that GHC can help verify the correctness of the program fragments I construct for those languages. From my point of view as an end-user, the restrictions on what data get promoted is inconsistent and oftentimes annoying to deal with. There are two related issues on my end:
1. The restriction that a data type cannot have a kind mentioning a promoted kind means that the way I stratify my type machinery impacts whether or not GHC will promote everything as I would like.
2. The inability to use promoted GADT's forces me to encode relationships between my type building blocks in trickier ways, and sometimes I am simply unable to come up with an alternative.
I have found that these issues get in my way as a programmer of modest skill. Oftentimes I will explore a particular design but be forced to abandon it because my "natural" line of reasoning runs into GHC's restrictions. With sufficient cleverness you can do quite a lot of impressive stuff with the current system, but I am often not sufficiently clever nor am I equipped to determine when something is outright ''impossible''.
Lifting these restriction, from ''my'' point of view, would simplify the machinery a great deal and allow me to do type-level programming that is currently out of my reach. It would make the kind extensions more uniform and more complete to us end-users. #6204 would complete them in another way.
New description: (Also allow the promotion of data types whose kind is not (* -> ... -> *)) I have been using -XDataKinds lately to explore the sorts of dependently typed programming that are currently possible in GHC. I am particularly interested in DSL's and embedding other languages' type systems into Haskell so that GHC can help verify the correctness of the program fragments I construct for those languages. From my point of view as an end-user, the restrictions on what data get promoted is inconsistent and oftentimes annoying to deal with. There are two related issues on my end: 1. The restriction that a data type cannot have a kind mentioning a promoted kind means that the way I stratify my type machinery impacts whether or not GHC will promote everything as I would like. 2. The inability to use promoted GADT's forces me to encode relationships between my type building blocks in trickier ways, and sometimes I am simply unable to come up with an alternative. I have found that these issues get in my way as a programmer of modest skill. Oftentimes I will explore a particular design but be forced to abandon it because my "natural" line of reasoning runs into GHC's restrictions. With sufficient cleverness you can do quite a lot of impressive stuff with the current system, but I am often not sufficiently clever nor am I equipped to determine when something is outright ''impossible''. Lifting these restriction, from ''my'' point of view, would simplify the machinery a great deal and allow me to do type-level programming that is currently out of my reach. It would make the kind extensions more uniform and more complete to us end-users. #6024 would complete them in another way. -- -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by thoughtpolice): Related: Richard Eisenberg's recent paper, "Towards dependently typed Haskell: System FC with kind equality" attacks almost exactly these problems I think. Or at least, it addresses the notion of promoting GADTs and indexing them by e.g. kinds (and the usual kin: kind families, etc.) http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf (Section 2, "Shallow Embedding" followed by "Deep embedding" gives an example of promoting GADTs.) I don't know what the status of this work is, but at the least you can use this paper as a basis to discuss precisely what you do/do not want? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Changes (by goldfire): * cc: eir@… (added) Comment: For full disclosure: Dan (the OP) contacted me (Richard E) after having found that paper and was wondering when/if the implementation of the ideas there would be merged. I encouraged him to post the feature request to stimulate a wider discussion. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by carter): Interesting paper! (and the examples therein are nice!) on the associated project page http://www.cis.upenn.edu/~eir/packages/nokinds/ it says " ... seem to have accepted the inevitability that these ideas will some day be merged. " Is that a quirk of turn of phrase, or is there some downside to this direction that isn't in the paper/documentation I see? (I'd assume the former, but doesn't hurt to ask explicitly) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by goldfire): I'm curious to see Simon speak for himself here, but that comment was inspired by the fact that implementing the type system in that paper adds a reasonable-sized dollop of complexity to GHC, and to a specific spot on which the soundness of the whole operation depends. (Reasonable people differ on what a reasonable-sized dollop of complexity is, of course.) Simon has expressed reluctance at merging and complicating GHC. We are consumed by other tasks at the moment, but I'm looking forward to pressing this issue more in a few weeks. The comment that it could be merged by midsummer remains a hopeful but sensible goal. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by simonpj): Richard has it right. Plus there's a closely related alternative design from Conor and Adam to think about. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by carter): Is there any public links to the associated Conor + Adam line of attack? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by carter): @richard, I'll be at hacphi this weekend, so if you're around and time permits, I'd love to better understand this matter a smidge. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by goldfire): Would love to be, but I'm currently at Microsoft Research Cambridge for the summer. I hope to make it to Hac Phi next year. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Changes (by adamgundry): * cc: adam.gundry@… (added) Comment: Replying to [comment:9 carter]:
Is there any public links to the associated Conor + Adam line of attack?
Not yet, sadly. My thesis (coming real soon now) explores some alternatives in the presentation of the core language, and builds on Richard's work to add Pi-types. The basic plan (to make things more uniform by eliminating the type/kind distinction) is a good one. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6024 | ---------------------------------+------------------------------------------ Changes (by danharaj): * related: #6204 => #6024 Comment: This recent preprint from Sam Lindley and Conor McBride is relevant: https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC