forall in a kind signature

user_1378868 0
Viewed 104

In singletons-2.6, Sigma is defined as

data Sigma (s :: Type) :: (s ~> Type) -> Type

and GHC 8.8.4 tells that its kind is

> :k Sigma
Sigma :: forall s -> (s ~> *) -> *

So what is this forall in this kind signature?

Apparently, it's different from

data Sigma :: forall s. Type -> (s ~> Type) -> Type

in which case its kind is, of course,

Sigma :: * -> (s ~> *) -> *

Also, it seems different from

data Sigma :: f s -> (s ~> *) -> *

It seems to me that the promoted kind of the type variable s in s :: Type is unified with the kind variable s in (s ~> Type) -> Type, but does it what happens? I have a feeling that I'm missing something very basic.

I tried finding any documents describing this, but I had no luck.

singleton-type data-kinds dependent-type haskell
1 Answers

Now, I got some ideas from dependent haskell in GHC Wiki.

We can now pass a kind to a type constructor just like we can pass a type to a data constructor (we still need to pass a singleton instead of a type itself though).

In this declaration of Sigma,

data Sigma (s :: Type) :: (s ~> Type) -> Type

s in s :: Type is a kind variable of Type kind-kind and this kind has to be passed explicitly when you use Sigma. And in its kind signature,

Sigma :: forall s -> (s ~> *) -> *

forall s means s is a visible kind. It means you need to pass it explicitly when you say it's visible. You can read it as Sigma is a type constructor taking a kind s and a type of kind s ~> Type, and returning a type of kind Type.

You cannot write this type signature directly in GHC 8.8.4, but you can write it using StandaloneKindSignatures in GHC 8.10.1.

Update (2021/9/30):

It's called Visible Dependent Quantification. You can find a good explanation about it at Visible dependent quantification in Haskell.

user_13788680
Related