Is an infinitely recursive type useful?

Question

I have been experimenting with a general question lately, what will the GHC allow me? I was surprised to find that he considers the next program valid.

module BrokenRecursiveType where data FooType = Foo FooType main = print "it compiles!" 

At first I thought how useful it is? Then I remembered that Haskell was lazy, so I could perhaps define a function for it like using

 allTheFoos = Foo allTheFoos 

Then I thought, since this is useful?

Are there any valuable use cases (invented or really experimental) for similar form types for FooType ?

Answer 1

Grade Counter

You could presumably use FooType to optionally interrupt a recursive function earlier: for example, take this code:

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

If you call foo allTheFoos , you get an equal factorial function. But you can pass another value of type FooType , for example.

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

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

I also do not say that this is especially useful, and that this is the best way to implement such a function ...

Type of emptiness

BTW, there is a similar design, namely

 newtype FooType' = Foo' FooType' 

which is useful: this is one way to determine the type of void that has no values ​​other than ⊥. You can still determine

 allTheFoos' = Foo' allTheFoos' 

as before, but since Foo does nothing expeditiously, this is equivalent to x = x and therefore also ⊥.

Answer 2

Let’s just expand your data type a bit - allow the recursion to be transferred to type parameters:

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

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

Now we can modulate the recursive link with 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 kwnown well package, where it is defined, is recurrence schemes, since Fix :

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

For example, if we define

 data List' ar = Cons' ar | 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) 

In addition, Fix allows you to define many common operations on recursive data types, such as folding / expanding ( catamorphisms / anamorphisms ).

Answer 3

 data FooType = Foo FooType allTheFoos = Foo allTheFoos 

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

Firstly, this is a “moral” way — a general approach when we pretend that Haskell types do not have “lower” (non-limiting) values. From this point of view, FooType is a type of type -a, which 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 point of view of “immorality” (when bottoms are allowed), FooType is either an endless tower of Foo constructors or an end tower of Foo constructors with a bottom at the bottom. This is similar to a “moral” interpretation of this type:

 data Nat = Zero | Succ Nat 

... but with a lower value instead of zero, which means that you cannot write functions like this:

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

Where does this leave us? I think the conclusion is that FooType not a very useful type, because:

• If you look at it “morally,” it is equivalent to () .
• If you look at it “immorally”, it is like Nat , but any functions that try to combine “zero” do not end there.

Answer 4

Extending your FooType can be an abstract syntax tree. Taking a simple example language with only integers, sums, and inversions, a type definition would be

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

All of the following 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 Foo replaced).

Answer 5

Next type:

 newtype H ab = Fn {invoke :: H ba -> b} 

while not quite the same as yours, but in a similar spirit, Launchbury, Krstic and Sauerwein were shown to have interesting applications for corouitining: https://arxiv.org/pdf/1309.5135.pdf