I'm trying to wrap my head around this blog post about the ConstraintKinds
extension.
There was a post in the comment section which I totally did not understand. Here it is:
Adam M says: 14 September 2011 19:53 UTC
Wow, this sounds great. Is it scheduled to be part of the official
GHC 7.4
? Also, does this mean that you've introduced a third production in the in System FC2 grammar for Kinds? Currently it has*
andk~>k
as the only alternatives wherek1~>k2
is (basically) the kind of(forall a::k1 . (t::k2))
. It sounds like this would addk1==>k2
which is the kind of(a::k1 => (t::k2))
. Or are the two kinds actually the same?
Could someone, please analyze this step-by-step or at least provide some links which would help me wrap my head around this myself. Some key moments I should pinpoint:
- What is a "System FC2 grammar for Kinds"? (Probably the main and the most general one, whose answer would embed the two other ones.)
- I tried explaining why "
k1~>k2
is (basically) the kind of(forall a::k1 . (t::k2))
"? As far as I understand,~>
is some special notation for->
in kinds, as*
andk1 -> k2
the only inhabitants of the standard Haskell's kind system (fits their description: "Currently it has*
andk~>k
as the only alternatives"). Thus, the(forall a::k1 . (t::k2))
formula means that if we take an inhabited typek1
, it can be mapped onto anotherk2
iff it is inhabited (due to Curry-Howard working for kinds the same way it works for types). Is that right? (P.S.: I see how this intuition fails if I do not understand the notion of inhabitance for kinds; do kinds correspond toTrueprovable formulae (see comments) when they have an inhabited type as an inhabitant or an arbitrary type? The intuition fails in the second case.) - What does the
=>
mean in the formula fork1==>k2
, namely(a::k1 => (t::k2))
?
The response this comment got:
Max says: 14 September 2011 21:11 UTC
Adam: it's not that complicated! It just adds the base kind
Constraint
to the grammar of kinds. This is a kind of types inhabited by values, just like the existing kinds*
and#
.
So the author claims that Adam M overcomplicated the extension. Their response is quite easy to understand. Anyway, even if Adam M's comment is not true, I think it is totally worth attention as it introduced some unfamiliar concepts to me.
"System FC2" is a term coined by Weirich et al in their 2010 paper "Generative type abstraction and type-level computation" (link). It refers to the addition of "roles" to System FC and formed the basis for the implementation in GHC described in the 2016 paper "Safe Zero-cost Coercions for Haskell. System FC, in turn, is the system originally described in this paper (or actually an earlier paper of which this is post-publication extended version), which extended the usual polymorphic lambda calculus of System F with type equalities.
However, I think Adam M was probably using the term "System FC2" less formally to refer to whatever type system GHC was implementing at the time the comment was written. So, the meaning of the phrase:
is really:
His claim was that the grammar for kinds currently had two production rules:
*
is a kindk1
andk2
are kinds, thenk1 ~> k2
is a kind.and he was asking if this extension gave a third production rule:
k1
andk2
are kinds, thenk1 ==> k2
is a kind.As you've guessed, he introduced the operator
~>
to differentiate the kind-level arrow from the type-level arrow. (In GHC, both the kind-level and type-level arrow operators are written the same way->
.) He gave a definition of~>
as:which is interpretable, but very imprecise. He was trying to use
forall
here as a sort of type-level lambda. It's not, but you can imagine that if you had a typeforall a. t
, you could instantiate it at a specific typea
, and if for alla :: k1
you gett :: k2
, then this polymorphic type sort of represents an implicit type function of kindk1 ~> k2
. But the polymorphism / universal quantification is irrelevant here. What's important is howa
appears in the expressiont
, and the extent to which you can express the type-level expressiont
as, say, a type-level function:or if Haskell had type-level lambdas, a type-level lambda with
a
as an argument andt
as its body:You won't get anywhere by trying to seriously consider
forall a. t
as having kindk1 -> k2
.Based on this loose interpretation of
~>
, he tried to ask if there was a new, kind-level operator==>
such that the relationship between the kind-level operator~>
and the type-level expressionforall a. b
was the same as the relationship between a new hypothetical kind-level operator==>
and the type-level expressiona => b
. I think the only reasonable way to interpret this question is to imagine that he wanted to consider the type expressiona => b
as being parameterized bya
, the same way he was imaginingforall a. b
as being parameterized bya
, so he wanted to consider a type-level function of the form:and consider the kind of
Something
. Here, the kind ofSomething
isConstraint ~> *
. So, I guess the answer to his final question is, "the two kinds are actually the same", and no other kind-level operator besides~>
is needed.Max's reply explained that the extension didn't add any new kind-level operator but merely added a new primitive kind,
Constraint
at the same grammatical level as the kinds*
and#
. The kind-level~>
operator has the same relationship to type-level applicationf a
whether the primitive kinds involved are*
or#
orConstratin
. So, for example, given:the kinds of
Whatever
andSomething
are both expressed in terms of the kind operator~>
(in GHC, written simply->
):