Haskell kinds. Beginner

Question

What is the kind of f?

class C f where
    comp :: f b c -> f a b -> f a c

I have written: (* -> *) -> * -> * Is this correct? c is a concrete type *. a is a type that takes a type and produces a type. And these both are the parameters for f? Is my argumentation correct?

What is kind of T?

data T f g = T (f String Int) (g Bool)

f has two concrete types as parameters (String and Int). g has one parameter (Bool) These both are the parameters for T. So I have: (*->*->*)->(*->*)->*. Is this correct? Thank you

Answer 1

GHCi can tell you the kinds of various things. For example, if you put:

data T f g = T (f String Int) (g Bool)

in a file Kinds.hs, you can load it into GHCi and ask for the kind of T:

> :l Kinds.hs
> :k T
T :: (* -> * -> *) -> (* -> *) -> *
>

so it looks like GHCi agrees with your solution.

For your first question, you can't ask GHCi to tell you the kind of f directly, but since f is a parameter to the typeclass C, you can ask for the kind of C:

> :k C
C :: (* -> * -> *) -> Constraint
>

meaning that C takes a type of kind * -> * -> * to produce a constraint. So, GHCi disagrees with you and thinks that f is of kind * -> * -> *.

Looking at the type signature for:

comp :: f b c -> f a b -> f a c

note that you couldn't have f of kind (* -> *) -> * -> * because f b c would imply that b was of kind * -> * while f a b would imply that b of of kind *, and it can't be both.

It turns out that the most general possible kind would be:

f :: k -> k -> *

where the first two arguments are forced to have the same kind k because b is used in both positions (in f a b and f b c respectively), and the final result is forced to have kind * because f b c, f a b, and f a c all need to be concrete types in order for the type signature of comp to make sense.

However, Haskell98 (no extensions) doesn't infer the most general possible kind, so it chooses k to be *, giving the kind signature * -> * -> *. It turns out that if you enable a certain extension (PolyKinds), then the kind signature will be k -> k -> * instead.

Answer 2

For the first question, I don't see why you have decided that a has kind * -> *. From what is written, a is just a *, nothing more. Therefore, the kind of f is * -> * -> *.

For the second question, you are correct.