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?
With data-kinds, we can use a regular newtype:
And promote it (with
'
) to create new kinds to represent loops:For a type to unpack its
'Inf
argument we need a type-family:Now we can express infinite kinds with a new kind for them, so no kind-safety is lost.
DataKinds
part in his answer!