2

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 * and k~>k as the only alternatives where k1~>k2 is (basically) the kind of (forall a::k1 . (t::k2)). It sounds like this would add k1==>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:

  1. What is a "System FC2 grammar for Kinds"? (Probably the main and the most general one, whose answer would embed the two other ones.)
  2. 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 * and k1 -> k2 the only inhabitants of the standard Haskell's kind system (fits their description: "Currently it has * and k~>k as the only alternatives"). Thus, the (forall a::k1 . (t::k2)) formula means that if we take an inhabited type k1, it can be mapped onto another k2 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 to True provable formulae (see comments) when they have an inhabited type as an inhabitant or an arbitrary type? The intuition fails in the second case.)
  3. What does the => mean in the formula for k1==>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.

Zhiltsoff Igor
  • 1,812
  • 8
  • 24
  • 2
    Personally I think Adam M is just confused. I'd ignore the comment if I were you; even setting aside whether it was more complicated than the truth or not it doesn't seem to make a lot of sense, and the bits I can decipher don't seem to be correct. – Daniel Wagner Apr 19 '21 at 02:05
  • @DanielWagner so the grammar for kinds does not go any further then `S to *, #, Constraint, ... | S to (S -> S)`? BTW, I offered a statement of my own in the second question. Can you comment on that one, please? Also, can you comment on the notion of inhabitance for kinds (the one I discussed in the second point as well). – Zhiltsoff Igor Apr 19 '21 at 07:33
  • 1
    The snippet you quoted in question 2 is specifically the bit I was most confident of deciphering and calling incorrect. I *still* don't recommend trying to extend it with your own thoughts. As for Curry-Howard... generally "true" is not a concept. There is provable and not provable; and though I don't know for certain, I suspect that the way most people use "inhabited" is to be as a synonym of "provable". – Daniel Wagner Apr 19 '21 at 13:58
  • @DanielWagner, right, sorry, I was wrong. So, namely: Pierce's law (`((P → Q) → P) → P`) is *~generally true~* in classic logic, but it is not provable as it is a **law**. Thus, there is no function of type `∀ a b. ((a -> b) -> a) -> a` and no type operator of kind `∀ p q. ((p -> q) -> p) -> q` as they would've corresponded to the non-existing Pierce's law proof. Have I finally got that right? – Zhiltsoff Igor Apr 19 '21 at 14:58
  • That all sounds right to me. – Daniel Wagner Apr 19 '21 at 16:17
  • @DanielWagner forgot to mention. I liked the trick with Pierce's law in [this Stack Overflow post](https://stackoverflow.com/a/27267992/11143763). – Zhiltsoff Igor Apr 19 '21 at 17:59

1 Answers1

2

"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:

introduced a third production in the System FC2 grammar for Kinds

is really:

added a third production rule to the grammar of kinds, as kinds are currently implemented in GHC

His claim was that the grammar for kinds currently had two production rules:

  1. * is a kind
  2. If k1 and k2 are kinds, then k1 ~> k2 is a kind.

and he was asking if this extension gave a third production rule:

  1. If k1 and k2 are kinds, then k1 ==> 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:

where k1~>k2 is (basically) the kind of (forall a::k1 . (t::k2)).

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 type forall a. t, you could instantiate it at a specific type a, and if for all a :: k1 you get t :: k2, then this polymorphic type sort of represents an implicit type function of kind k1 ~> k2. But the polymorphism / universal quantification is irrelevant here. What's important is how a appears in the expression t, and the extent to which you can express the type-level expression t as, say, a type-level function:

type Whatever a = t

or if Haskell had type-level lambdas, a type-level lambda with a as an argument and t as its body:

Lambda a. t

You won't get anywhere by trying to seriously consider forall a. t as having kind k1 -> 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 expression forall a. b was the same as the relationship between a new hypothetical kind-level operator ==> and the type-level expression a => b. I think the only reasonable way to interpret this question is to imagine that he wanted to consider the type expression a => b as being parameterized by a, the same way he was imagining forall a. b as being parameterized by a, so he wanted to consider a type-level function of the form:

type Something a = a => b

and consider the kind of Something. Here, the kind of Something is Constraint ~> *. 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 application f a whether the primitive kinds involved are * or # or Constratin. So, for example, given:

{-# LANGUAGE ConstraintKinds, RankNTypes #-}
type Whatever a = Maybe [a]
type Something a = a => Int

the kinds of Whatever and Something are both expressed in terms of the kind operator ~> (in GHC, written simply ->):

λ> :kind Whatever
Whatever :: * -> *
λ> :kind Something
Something :: Constraint -> *
marc_s
  • 732,580
  • 175
  • 1,330
  • 1,459
K. A. Buhr
  • 45,621
  • 3
  • 45
  • 71