Kinds

Created: 2023-01-11 09:39

A kind is a type of type. Values have types, types have kinds.

Saturated => has all the arguments provided

* is the most basic kind and almost everything has kind *

Anything at the value level is of kind *.

Int
Char
Bool
 
Maybe Int
Int -> Int
[[[Char]]]

Maybe on the other hand is a type level function, so its kind is * -> *.

Because the function is * -> * we cannot give it any kind, only one of *.

Maybe :: * -> *

So if we try Maybe IO we get a kind error, NOT a type error.

Some other examples:

(,,) => * -> * -> * -> *
(->) => * -> * -> *

Given:

data WrappedInt f = Wrap (f Int)

The kind the is:

WrappedInt :: (* -> *) -> *

Type classes are parameterized by types of different kinds

class Eq (a :: *) where
  a :: *
  (==) :: a -> a -> Bool
  
class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b

kind polymorphism §

In the following example, the kind of f is not * -> *, since it could take any kind.

class Foo (f :: k -> *) where
  foo :: forall (a :: k) (b :: k). f a -> f b

Wheres the case of functor, the kind is not generic because (a -> b) limits the kind of a and b to *.

Constraint kind §

Enabled with ConstraintKinds, is the kind for constraints.

Eq :: * -> Constraint

Show a => a -> String
(=>) (Show a) (a -> String)
(=>) :: Constraint -> * -> *

# kinds §

# is enabled with the MagicHash extension.

id :: a -> a

Since that works on any type, all types of kind * are actually pointers to something else that isn’t of kind * but instead it cannot be passed to *.

When we try to assign Bool as the type for the literal 3, we get an error. That is because number literals in Haskell are typed Num a.

ghci> 3 :: Bool
<interactive>:10:1: error:
    • No instance for (Num Bool) arising from the literal ‘3’
    • In the expression: 3 :: Bool
      In an equation for ‘it’: it = 3 :: Bool

But if we try to assign Int#, which is the underlaying machine integer type of Int, the error is different.

ghci> 3 :: GHC.Prim.Int#
<interactive>:11:1: error:
    • Couldn't match a lifted type with an unlifted type
      When matching types
        a0 :: *
        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
    • In the expression: 3 :: GHC.Prim.Int#
      In an equation for ‘it’: it = 3 :: GHC.Prim.Int#

# types have their own kind.

ghci> :k Num
Num :: * -> Constraint

ghci> :k Int
Int :: *

ghci> :k GHC.Prim.Int#
GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep