Opened 5 years ago

Closed 2 years ago

#7961 closed feature request (fixed)

Remove restrictions on promoting GADT's

Reported by: danharaj Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.6.3
Keywords: Cc: eir@…, adam.gundry@…, jstolarek, william.knop.nospam@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: dependent/should_compile/TypeLevelVec
Blocked By: Blocking:
Related Tickets: #6024 Differential Rev(s): Phab:D808
Wiki Page:

Description (last modified by simonpj)

(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.
  1. 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.

Change History (21)

comment:1 Changed 5 years ago 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"?

comment:2 Changed 5 years ago by danharaj

I will post a nice code example when I can. It is a bit late here at the moment.

comment:3 Changed 5 years ago by simonpj

Description: modified (diff)
difficulty: Unknown

comment:4 Changed 5 years ago 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?

comment:5 Changed 5 years ago by goldfire

Cc: eir@… added

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.

comment:6 Changed 5 years ago 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)

comment:7 Changed 5 years ago 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.

comment:8 Changed 5 years ago by simonpj

Richard has it right. Plus there's a closely related alternative design from Conor and Adam to think about.

Simon

comment:9 Changed 5 years ago by carter

Is there any public links to the associated Conor + Adam line of attack?

comment:10 Changed 5 years ago 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.

comment:11 Changed 5 years ago 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.

comment:12 in reply to:  9 Changed 5 years ago by adamgundry

Cc: adam.gundry@… added

Replying to 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.

comment:13 Changed 4 years ago by danharaj

This recent preprint from Sam Lindley and Conor McBride is relevant: https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf

comment:14 Changed 4 years ago by danharaj

Adam Gundry has recently published his thesis which is wholly relevant to this ticket: https://personal.cis.strath.ac.uk/adam.gundry/thesis/

comment:15 Changed 4 years ago by jstolarek

Cc: jan.stolarek@… added

comment:16 Changed 4 years ago by altaic

Cc: william.knop.nospam@… added

comment:17 Changed 3 years ago by goldfire

Differential Rev(s): Phab:D808

I have posted an early version of my patch to implement kind equalities, fixing this ticket. Comments/experimentation welcome. It is easiest to access the branch from https://github.com/goldfirere/ghc, on the nokinds branch.

comment:18 Changed 2 years ago by jstolarek

Cc: jstolarek added; jan.stolarek@… removed

comment:19 Changed 2 years ago by Richard Eisenberg <eir@…>

In 67465497/ghc:

Add kind equalities to GHC.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

comment:20 Changed 2 years ago by Richard Eisenberg <eir@…>

In 68f198f/ghc:

Test case for #7961.

Test case: dependent/shoud_compile/TypeLevelVec

comment:21 Changed 2 years ago by goldfire

Milestone: 8.0.1
Resolution: fixed
Status: newclosed
Test Case: dependent/should_compile/TypeLevelVec

All set now.

Note: See TracTickets for help on using tickets.