Expressing infinite kinds

Question

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?

Answer 1

Responding to:

Like recursion-schemes, I want a way to construct ASTs, except I want my ASTs to be able to refer to each other - that is a term can contain a type (for a lambda parameter), a type can contain a row-type in it and vice-versa. I'd like the ASTs to be defined with an external fix-point (so one can have "pure" expressions or ones annotated with types after type inference), but I also want these fix-points to be able to contain other types of fix-points (just like terms can contain terms of different types). I don't see how Fix helps me there

I have a method, which maybe is near what you are asking for, that I have been experimenting with. It seems to be quite powerful, though the abstractions around this construction need some development. The key is that there is a kind Label which indicates from where the recursion will continue.

{-# LANGUAGE DataKinds #-}

import Data.Kind (Type)

data Label = Label ((Label -> Type) -> Type)
type L = 'Label

L is just a shortcut to construct labels.

Open-fixed-point definitions are of kind (Label -> Type) -> Type, that is, they take a "label interpretation (type) function" and give back a type. I called these "shape functors", and abstractly refer to them with the letter h. The simplest shape functor is one that does not recurse:

newtype LiteralF a f = Literal a  -- does not depend on the interpretation f
type Literal a = L (LiteralF a)

Now we can make a little expression grammar as an example:

data Expr f
    = Lit (f (Literal Integer))
    | Let (f (L Defn)) (f (L Expr))
    | Var (f (L String))
    | Add (f (L Expr)) (f (L Expr))

data Defn f
    = Defn (f (Literal String)) (f (L Expr))

Notice how we pass labels to f, which is in turn responsible for closing off the recursion. If we just want a normal expression tree, we can use Tree:

data Tree :: Label -> Type where
    Tree :: h Tree -> Tree (L h)

Then a Tree (L Expr) is isomorphic to the normal expression tree you would expect. But this also allows us to, e.g., annotate the tree with a label-dependent annotation at each level of the tree:

data Annotated :: (Label -> Type) -> Label -> Type where
    Annotated :: ann (L h) -> h (Annotated ann) -> Annotated ann (L h)

In the repo ann is indexed by a shape functor rather than a label, but this seems cleaner to me now. There are a lot of little decisions like this to be made, and I have yet to find the most convenient pattern. The best abstractions to use around shape functors still needs exploration and development.

There are many other possibilities, many of which I have not explored. If you end up using it I would love to hear about your use case.

Answer 2

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.

• Thanks to @luqui for pointing out the DataKinds part in his answer!

Answer 3

I think you're looking for Fix which is defined as

data Fix f = Fix (f (Fix f))

Fix gives you the fixpoint of the type f. I'm not sure what you're trying to do but such infinite types are generally used when you use recursion scehemes (patterns of recursion that you can use) see recursion-schemes package by Edward Kmett or with free monads which among other things allow you to construct ASTs in a monadic style.