haskelltypestype-familiestype-kinds

Expressing infinite kinds

When expressing infinite types in Haskell:

f x = x x -- This doesn't type check

One can use a newtype to do it:

newtype Inf = Inf { runInf :: Inf -> * }

f x = x (Inf x)

Is there a newtype equivalent for kinds that allows one to express infinite kinds?

I already found that I can use type families to get something similar:

{-# LANGUAGE TypeFamilies #-}
data Inf (x :: * -> *) = Inf
type family RunInf x :: * -> *
type instance RunInf (Inf x) = x

But I'm not satisfied with this solution - unlike the types equivalent, Inf doesn't create a new kind (Inf x has the kind *), so there's less kind safety.

Is there a more elegant solution to this problem?

Solution

  • With data-kinds, we can use a regular newtype:

    import Data.Kind (Type)

newtype Inf = Inf (Inf -> Type)

    And promote it (with ') to create new kinds to represent loops:

    {-# LANGUAGE DataKinds #-}

type F x = x ('Inf x)

    For a type to unpack its 'Inf argument we need a type-family:

    {-# LANGUAGE TypeFamilies #-}

type family RunInf (x :: Inf) :: Inf -> Type
type instance RunInf ('Inf x) = x

    Now we can express infinite kinds with a new kind for them, so no kind-safety is lost.