last day (14 days later) » 

12:19 AM
4
A: Kind-polymorphism in classes

pigworkerThis is a job for GHC 8 and TypeInType, which allows much more amusing forms of dependency. The following minor edit of your code typechecks. {-# LANGUAGE PolyKinds, RankNTypes, KindSignatures, DataKinds, TypeInType #-} module KP where import Data.Kind class Foo (f :: forall k. k -> *) w...

 
Can you explain how this is different than the GADT example? Why do I need TypeInType here, but not there?
 
Well, before TypeInType, the correct kind annotation on f was a syntax error. And there's a genuine question of where k should be quantified: is it local to f or to Foo? Your GADT example, where you say "GADTs require kind signatures where they should be inferred...it's clear from the GADT constructors that a :: *" makes unwarranted assumptions about what is inferrable. For interesting patterns of abstraction, "guess the pattern" inference is now hopeless; "instantiate the pattern" inference is still pretty good, though.
 
In my GADT example, I managed to apply the first type parameter of Foo to two types of different kinds (namely Nat and *), without needing TypeInType. I think that's exactly what I'm trying to do in my example, so I'm not sure why the extension is required.
 
Write down the types (that we used to call "kinds") of the GADT constructor and the type class, with all foralls explicit. Your GADT has iiuc rank-1 polymorphism, but your typeclass has rank-2. Before TypeInType that (like a bunch of other stuff, e.g. GADT promotion) was beyond what was obviously manageable in GHC core. The TypeInType generalisation makes the treatment of polymorphism and equality constraints more uniform: equations between polymorphic types now work sensibly (i.e., heterogeneously), allowing higher-rank types in more places.
 
I edited the question to include a concrete GADT example. My understanding is that the constructor C requires rank-2 polymorphism, because we can never unify the kinds of x and '(x,x). This is accomplished without TypeInType.
 
12:19 AM
You are incorrect, as you can easily find out for yourself by asking ghci. Neither your GADT type constructor Foo, nor its value constructor C has a rank-2 polymorphic type: they do not need to abstract over polymorphic things. Your class Foo is not a translation to classes of your GADT, so you are making an apples-oranges comparison. The type of the class Foo is (forall k. k -> *) -> Constraint which really is rank-2.
 
@pigworker I see that GHCi gives C :: Foo * x -> Foo (*, *) '(x, x). I agree that this signature isn't (kind) polymorphic at all. However, I think GHCi is lying to me. By adding a base-case constructor, I can easily build a x :: Foo (GHC.Types.Nat, GHC.Types.Nat) '(3, 3). So which is it? Does C product a Foo (*,*), or a Foo (Nat,Nat)? It seems that GHCi isn't telling the whole story.
I appreciate you trying to get this through my think skill; I might actually learn something.
 
But the kind signature you say ghci gives you for C doesn't claim that it produces a Foo (*, *) at all! It claims to produce a Foo (x, x), where x :: * -- and Foo (Nat, Nat) fits that pattern perfectly fine since Nat :: *.
 
Err, it claims Foo (x,x) where x :: *, I agree. But I made a Foo '(3,3), where 3 has kind Nat...right?
TypeInType is off for the purposes of the present discussion, so Nat is a kind, right? It has sort *, but that's not relevant I think/hope. So why do you say Nat :: *?
 
Hm, perhaps you can help me reproduce what you're seeing. When I ask :t Foo I don't see what you do: I see C :: Foo x -> Foo '(x, x), which is much less informative.
And I agree my previous comment doesn't seem right.
Here's the complete file I tried to load to follow along:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
data Foo (x :: k) where
V :: proxy x -> Foo x
C :: Foo x -> Foo '(x,x)
Oh bother, does markdown not work in chat?
 
with -fprint-explicit-kinds:
*Main> :t C
C :: Foo * x -> Foo (*, *) '(x, x)
*Main> :kind! Foo
Foo :: k -> *
= Foo
*Main> :t x
x :: Foo (GHC.Types.Nat, GHC.Types.Nat) '(3, 3)
sorry, and here's the code:
{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}

data Foo :: k -> * where
C :: Foo (x :: k) -> Foo '(x,x)
NZ :: Foo (x :: k)

x = C (NZ :: Foo 3)
right, your code and mine look isomorphic. -fprint-explicit-kinds may help.
 
12:35 AM
I agree. I think ghci is lying.
 
okay, that's a good start. So the question remains: does C have rank-2 kind polymorphism or not?
 
I think it should be C :: forall k. Foo k x -> Foo (k, k) '(x, x) or so. But that still looks rank-1 to me.
 
Ah, I see why it's rank 1 now.
do I?
let me think...
your signature is analogous to the type signature c :: forall a . D a -> D (a,a), right?
I agree that that is rank-1 type-polymorphism
the kinds confuse me a bit though
 
Yes, the syntax is a bit confusing, because it doesn't distinguish between types and kinds.
C :: forall kinds k. forall types x :: k. Foo (kind k) (type x) -> Foo (kind (k, k)) (type (x, x)) but this is so unwieldy
 
So the point here is that the kind of x in the input and output is the same
let me see if I can break that...
 
12:43 AM
Perhaps the TypeApplications syntax would be clearer: C :: forall k (x :: k). Foo @k x -> Foo @(k, k) (x, x).
 
okay, so even though the kind of the type parameter is changing (from k to (k,k)), the kind parameter doesn't change from one application to the other, making it rank-1
is that about right?
 
no no
rank-1 isn't about what types/kinds are applied to other types/kinds at all
We could have Foo @k and Foo @nose in the same expression without getting out of rank-1 land.
Rank 1 just means none of the arguments are themselves polymorphic.
So if we had something like (forall k. Foo @k x) -> ..., then this is rank-2, because the argument of this itself must be polymorphic. Whereas in forall k. Foo @k x -> ..., we first choose k and then have a monomorphic Foo @k x to provide.
 
right
okay, I think I've got it now
thanks for your help!
 
Great! Sorry for the false start.
I get tied up in levels a bit myself. =)
 
so that GHCi issue would be a bug, right?
unless it's some sort of GHCi defaulting??
 
12:51 AM
Indeed, there might be some kind-level defaulting. I'd say look through the docs for such a thing briefly, and if you don't find it go ahead and file a bug.
 
great. thanks again!
If you :set -XPolyKinds in GHCi and then ask for the type of C, you get C :: forall k (x :: k). Foo k x -> Foo (k, k) '(x, x)
 

last day (14 days later) »