I’m proud to announce that I’m nearing completion on a major patch to GHC, merging types and kinds. This patch has been in development since late 2012 (!), with many interruptions in the meantime. But I really do think it will make it for 7.12, due out early 2016. This post is meant to generate discussion in the community about the proposed changes and to get feedback about any user-facing aspects which might be of interest.
Motivation
The real motivation for writing this is that it’s a key step toward dependent types, as described in the paper laying out the theory that underlies this patch. But other motivation is close to hand as well. This patch fixes GHC bug #7961, which concerns promotion of GADTs – after this patch is merged, all types can be used as kinds, because kinds are the same as types! This patch also contributes toward the solution of the problems outlined in the wiki page for the concurrent upgrade to Typeable, itself part of the Distributed Haskell plan.
Examples
Below are some fun examples that compile with my patch. As usual, this page is a literate Haskell file, and these examples really do compile! (I haven’t yet implemented checking for the proposed extension StarInStar, which this will require in the end.)
> {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies #-}
> {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
>
> -- a Proxy type with an explicit kind
> data Proxy k (a :: k) = P
> prox :: Proxy * Bool
> prox = P
>
> prox2 :: Proxy Bool 'True
> prox2 = P
>
> -- implicit kinds still work
> data A
> data B :: A -> *
> data C :: B a -> *
> data D :: C b -> *
> data E :: D c -> *
> -- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> *
>
> -- a kind-indexed GADT
> data TypeRep (a :: k) where
> TInt :: TypeRep Int
> TMaybe :: TypeRep Maybe
> TApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
>
> zero :: TypeRep a -> a
> zero TInt = 0
> zero (TApp TMaybe _) = Nothing
>
> data Nat = Zero | Succ Nat
> type family a + b where
> 'Zero + b = b
> ('Succ a) + b = 'Succ (a + b)
>
> data Vec :: * -> Nat -> * where
> Nil :: Vec a 'Zero
> (:>) :: a -> Vec a n -> Vec a ('Succ n)
> infixr 5 :>
>
> -- promoted GADT, and using + as a "kind family":
> type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
> 'Nil ++ y = y
> (h ':> t) ++ y = h ':> (t ++ y)
>
> -- datatype that mentions *
> data U = Star *
> | Bool Bool
>
> -- kind synonym
> type Monadish = * -> *
> class MonadTrans (t :: Monadish -> Monadish) where
> lift :: Monad m => m a -> t m a
> data Free :: Monadish where
> Return :: a -> Free a
> Bind :: Free a -> (a -> Free b) -> Free b
>
> -- yes, * really does have type *.
> type Star = (* :: (* :: (* :: *)))
Details
More details are in the wiki page for this redesign. As stated above, I’d love your feedback on all of this!
Types and Kinds 
Since you’re asking for feedback, I’m worried about how you intend to collapse types and kinds and especially the fact that you add type-in-type at the kind level. If I correctly understand your paper, you agree that this makes type-checking of FC undecidable, but you argue that that does not mean you have to make type-checking of GHC Haskell undecidable.
I think this point is probably correct but I’m worried that adding “* :: *” may be a bad idea for other reasons. As I understand it, FC type-checking doesn’t just become undecidable, but perhaps more importantly, FC becomes inconsistent, i.e. any kind is inhabited. My gut feeling is that this removes potential applications of the type system. Any potential future applications that relies on some form of proofs encoded at the type-level become untrustworthy. The potential of making the type-level computation and type-level lambdas of FC available in source Haskell at some point in the future (to replace and/or complement MPTCs and type families) is compromised or at least become a lot more brittle if we don’t want to make Haskell type-checking undecidable too.
Generally, while FC now feels like a well-behaved and natural extension of Fomega, the proposed change would turn it into a fundamentally different and less well-behaved language and I’m worried that we will regret this change at some point in the future. I wonder if the goal of supporting GADT promotion cannot be achieved by less radical means, such as using a cumulative hierarchy of universes at the type level.
Note: If the above is based on a misunderstanding of the implications of your proposed changes, please correct me and ignore the rest of my rambling ;).
Thanks, Dominique, for your feedback!
I’m afraid somewhere the languages got swapped: having (* :: *) makes type-checking GHC/Haskell undecidable, but type-checking FC is still quite decidable. Indeed, I believe it’s linear in the size of the (FC) program text. The reason this is possible is that FC has no type-level evaluation, and there are no plans to change this, even if we add type-level lambda. Instead, FC has coercions which represent the equality between some type redex and its reduced form. So, a looping program in types may lead to an infinitely-sized FC program, because an infinite number of coercions are needed to represent the reduction of a type. This is where GHC’s Haskell type-checker diverges, before FC can really come into the picture.
The use of coercions to represent equalities is also why having all kinds be inhabited (which is indeed true) is OK. Coercions prove equality propositions. Critically, *not* all propositions are inhabited / provable. The language of coercions admits no recursion (or evaluation) at all. Because FC keeps coercions apart from types/kinds, the inconsistency of types/kinds does not threaten type safety. (Here, inconsistency of types/kinds = all kinds are inhabited.)
It’s indeed true that (* :: *) threatens the reliability of proofs in Haskell/FC. But that ship sailed a long time ago. Just like we have `undefined` at the term level, we have `Any` at the type level. It inhabits all kinds today. So (* :: *) doesn’t make this any worse. It does make the problem more entrenched, admittedly. As it stands, “proofs” in Haskell have never been and are not planned to be fully reliable.
The decision to have (* :: *) is just because we can. As you suggest, we don’t have to: the hierarchy of universes would work fine. But there seems to be no concrete downsides that will bite today about (* :: *), so we went with the simpler option. I conjecture that it would be straightforward to change to a universe hierarchy in the future if need be, modulo backward compatibility. But even that shouldn’t be too bad, as anyone who wants to eliminate (* :: *) would want that axiom missing from all modules (and no module that uses `Any` or other type system holes) — much like Safe Haskell.
Richard, thanks for the reply,
First, I’ll admit upfront that it’s been a while since I read the different papers on FC, and I should probably brush up on the precise treatment of coercions in the different papers.
Nevertheless, after re-browsing through the TLDI2007 paper on FC, it clearly says stuff like “our slogan is ‘propositions as kinds’ and ‘proofs as (coercion) types”. Your answer suggests a much more strict separation between types and coercions. Does this mean that this distinction was added in one of the later papers and if so, do you happen to know when?
I’m also surprised to hear that FC has no type-level computation. I was under the impression that it was a superset of System Fw (several of the papers mention this), which AIUI has type-level lambdas as one of its distinguishing features. Update: again after re-reading the TLDI2007 paper on FC, it clearly says that Fc omits type-level lambdas from Fw.
Finally, I’m surprised to hear about the Any type inhabiting every kind. Could you point me to some background information on that?
That slogan is a lie. 🙂
The TLDI’07 paper uses what I find to be a confusing presentation of FC. Newer papers discussing FC (such as the one I cite above and the “Giving Haskell a Promotion” paper) use a different formulation, although the systems are equivalent, modulo the extension a particular paper is discussing. The difficulty in TLDI’07 is that it uses the same grammar for types as it does for coercions and puts (t1 ~ t2) as a kind. This isn’t wrong, per se, but it’s a bit of a lie, because these are all separated out by the typing rules. Note that there are two separate judgments G |-TY s : k and G |-CO g : s ~ t, even though these schema overlap (ignoring the critical TY/CO distinction). Thus, in the TLDI’07 presentation, when we say “inhabited”, we really ought to specify which typing judgment we’re considering. Thus, my claim is that all kinds are inhabited w.r.t the |-TY judgment, but not w.r.t the |-CO judgment. In the later papers, the grammars are pulled apart, making such a statement clearer.
If a paper discusses FC as an extension of Fw, that may be in error. Could you point me to the reference? The TLDI’07 paper presents FC as an extension of F. I don’t believe any version of FC has had a type-level reduction relation or a non-trivial definitional equality (such as one that includes a beta rule).
I don’t have a paper reference about Any to hand. The type Any has been needed for quite some time as a way to fill in irrelevant type variables. If you say `tru = null []`, GHC must infer the type at which you’re calling `null :: [a] -> Bool`. Of course, this choice matters not. GHC chooses Any. These irrelevant choices can happen at any kind, so Any must exist at any kind. It used to be that Any was a special constant that existed at every kind. Nowadays, it’s just this: `type family Any :: k`, a poly-kinded type family, polymorphic in its result type, and with no instances. So even if GHC didn’t include Any, any user could define it.
Because type-checking GHC/Haskell is undecidable, it’s quite possible that GHC will loop during compilation. While this is undesirable from a user-experience standpoint, it’s not a terrible outcome: you still haven’t launched the rockets (that is, caused a type error). However, looping during compilation should happen only when the user submits a program that has a type-level loop. Just as no one frets when a programmer writes an ordinary term-level loop and then the program loops at runtime, we shouldn’t fret when a programmer writes a type-level loop and then the program loops at compiile-time. Having (* :: *) may indeed cause more ways for a determined programmer to get GHC to loop, but then that programmer gets their just deserts. What is terrible is producing a type-incorrect program that might run and launch the rockets. Undecidable type-checking won’t cause that to happen.
Regarding papers that describe FC as an extension of Fw, I’ve been browsing through some of the papers and it appears that most of them indeed do not claim this, so this is probably a misunderstanding on my part. The only one I’ve been able to find that does mention the claim is this one (on p.3): http://dl.acm.org/citation.cfm?id=2500599.
Regarding your argument about why undecidable type-checking is acceptable, this seems essentially the same reasoning as is sometimes given for accepting UndecidableInstances and the like. I’m personally not convinced by that argument, and I was under the impression that the Haskell community as a whole was not convinced by similar arguments about, e.g. UndecidableInstances or C++’s undecidable type-level computation. That said, I realise that there’s probably no real practical difference between a potentially non-terminating type-checking algorithm and one that necessarily terminates but may potentially take very very long.
All in all, for me, the main point is that I’d like the type-level language of GHC and Core to be consistent (i.e. not every kind is inhabited). I think trustworthy type-level proofs could have many interesting applications in the future and I think there’s also a kind of general virtue in keeping Haskell close to well-behaved and well-understood languages like System Fw. If you say that it would be feasible to use a cumulative hierarchy of universes instead of “* :: *”, I would humbly suggest to consider accepting the additional annoyance it brings in return for keeping the language more well-behaved and retain the potential for applications that now seem distant future, but that’s just my 2 cents of course.
Oh, and I forgot to ask something else: why isn’t it a problem that type-checking GHC/Haskell becomes undecidable?
What happend having -XStarInStar expose a Star alias for *?
The Star alias was an early thought borne of my opinion at the time that we could not keep the existing * working in the new language. But we can. The solution is to give GHC.Types.* (the kind of types with values) a magical new fixity. When GHC resolves fixities, it just treats symbols with the magical fixity as it would an alphanumeric identifier. So we can differentiate between GHC.Types.* and GHC.TypeLits.* using normal mechanisms, and everything should just work.
If you really want that synonym, just say `type Star = *` and off you go!
(I have no plans on exposing the magical fixity to users. Doing so seems to make Haskell less readable for marginal benefit. Of course, this all paves the way for Agda-style mixfix operators, but that’s a story for another day.)
So if values can be types and types and values are the same and values have type have kinds means types have type have types have types …
This … is … AMAZING! (Haskell took a long and ugly route to get to this point but AMAZING!)
(They should fold all the extensions you used into one extension called “DependentTypes”)
Sorry to burst your bubble, Chris, but values and types are still quite separate. So we’re not quite at dependent types. But, I believe any dependently typed program is encodable using singletons.
On the other hand, my work is not yet done, and I hope to have a prototype of -XDependentTypes available in 6 months or so. So stay tuned.