5

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?

AJF
  • 11,767
  • 2
  • 37
  • 64
mjgpy3
  • 8,597
  • 5
  • 30
  • 51

5 Answers5

9

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 ⊥.

raam86
  • 6,785
  • 2
  • 31
  • 46
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139
4

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).

Community
  • 1
  • 1
Petr
  • 62,528
  • 13
  • 153
  • 317
1
data FooType = Foo FooType

allTheFoos = Foo allTheFoos

I think there are two useful ways to look at this type.

First is the "moral" way—the common approach where we pretend that Haskell types don't have "bottom" (non-terminating) values. From this perspective, FooType is a unit type—a type that has only one value, just like (). This is because if you forbid bottoms, then the only value of type Foo is your allTheFoos.

From the "immoral" perspective (where bottoms are allowed), FooType is either an infinite tower of Foo constructors, or a finite tower of Foo constructors with a bottom at the bottom. This is similar to the "moral" interpretation of this type:

data Nat = Zero | Succ Nat

...but with bottom instead of zero, which means that you can't write functions like this one:

plus :: Nat -> Nat -> Nat
plus Zero y = y
plus (Succ x) y = Succ (x `plus` y)

Where does that leave us? I think the conclusion is that FooType isn't really an useful type, because:

  1. If you look at it "morally" it's equivalent to ().
  2. If you look at it "immorally" it's similar to Nat but any functions that tries to match a "zero" is non-terminating.
Luis Casillas
  • 29,802
  • 7
  • 49
  • 102
1

An extension of your FooType could be an abstract syntax tree. Taking a simple example language only having integers, sums and inverses, the type definition would be

data Exp = AnInt Integer
         | AnInverse Exp
         | ASum Exp Exp

All the following would be Exp instances:

AnInt 2  -- 2
AnInverse ( AnInt 2 )  -- 1 / 2
AnInverse ( ASum ( AnInt 2 ) ( AnInt 3 ) )  -- 1 / ( 2 + 3 )
AnInverse ( ASum 1 ( AnInverse 2 ) )  -- 1 / ( 1 + 1 / 2 )

If we removed AnInt and ASum from the Exp definition, the type would be isomorphic to your FooType (with AnInverse replacing Foo).

asterione
  • 11
  • 1
0

The following type:

newtype H a b = Fn {invoke :: H b a -> b}

while not exactly the same as yours but is in a similar spirit, have been shown by Launchbury, Krstic, and Sauerwein to have interesting uses regarding corouitining: https://arxiv.org/pdf/1309.5135.pdf

alias
  • 28,120
  • 2
  • 23
  • 40