Is an infinitely recursive type useful?

Question

Lately I've been experimenting with the general question, what will GHC allow me to do? I was surprised to find, that it considers the following program as valid

module BrokenRecursiveType where

data FooType = Foo FooType

main = print "it compiles!"

At first I thought, how is this useful? Then I remembered that Haskell is lazy, so I could, perhaps, define a function like the following to use it

allTheFoos = Foo allTheFoos

Then I thought, so how is this useful?

Are there any valuable use cases (thought up or actually experienced) for types of similar form to FooType?

Answer 1

An evaluation counter

You could, hypothetically, use FooType to optionally abort a recursive function early: For example, take this code:

foo _ 0 = 1
foo (Foo x) n = n * foo x (n-1)

If you call foo allTheFoos, then you get the plain factorial function. But you can pass a different value of type FooType, e.g.

atMostFiveSteps = Foo (Foo (Foo (Foo (Foo (error "out of steps")))))

and then foo atMostFiveSteps will only work for values smaller than 6.

I’m neither saying that this is particularly useful nor that this is the best way to implement such a feature...

A void type

BTW, there is a similar construction, namely

newtype FooType' = Foo' FooType'

which is useful: It is one way to define the void type that has no values besides ⊥. You can still define

allTheFoos' = Foo' allTheFoos'

as before, but because operationally, Foo does nothing, this is equivalent to x = x and hence also ⊥.

Answer 2

Let's just slightly extend your data type - let's wrap the recursion into a type parameters:

data FooType f = Foo (f (FooType f))

(so your original data type would be FooType Identity).

Now we can modulate the recursive reference by any f :: * -> *. But this extended type is extremely useful! In fact, it can be used to express any recursive data type using a non-recursive one. One well kwnown package where it's defined is recursion-schemes, as Fix:

newtype Fix f = Fix (f (Fix f))

For example, if we define

data List' a r = Cons' a r | Nil'

then Fix (List' a) is isomorphic to [a]:

nil :: Fix (List' a)
nil = Fix Nil'

cons :: a -> Fix (List' a) -> Fix (List' a)
cons x xs = Fix (Cons' x xs)

Moreover, Fix allows us to define many generic operations on recursive data types such as folding/unfolding (catamorphisms/anamorphisms).