无限递归类型有用吗？

Question

最近我一直在试验一般性问题，GHC 允许我做什么？我惊讶地发现，它认为以下程序有效

module BrokenRecursiveType where

data FooType = Foo FooType

main = print "it compiles!"

起初我想，这有什么用？ 然后我想起 Haskell 是惰性的，所以我也许可以定义一个像下面这样的函数来使用它

allTheFoos = Foo allTheFoos

然后我想，这有什么用？

对于与 FooType 形式相似的类型，是否有任何有价值的用例（想到的或实际体验过的）？

Answer 1

评估计数器

假设您可以使用 FooType 有选择地提前中止递归函数：例如，采用以下代码：

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

如果您调用 foo allTheFoos，您将获得普通的阶乘函数。但是您可以传递 FooType 类型的不同值，例如

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

然后 foo atMostFiveSteps 仅适用于小于 6 的值。

我并不是说这特别有用，也不是说这是实现此类功能的最佳方式...

空类型

顺便说一句，还有一个类似的构造，即

newtype FooType' = Foo' FooType'

这很有用：这是定义除 ⊥ 外没有任何值的 void 类型的一种方法。你仍然可以定义

allTheFoos' = Foo' allTheFoos'

和以前一样，但是因为在操作上，Foo 什么都不做，这等同于 x = x 因此也是 ⊥.

Answer 2

data FooType = Foo FooType

allTheFoos = Foo allTheFoos

我认为有两种有用的方法来看待这种类型。

首先是 "moral" 方式——我们假装 Haskell 类型没有 "bottom"（非终止）值的常用方法。从这个角度看，FooType是一个单位类型——一种只有一个值的类型，就像()一样。这是因为如果你禁止底部，那么 Foo 类型的唯一值就是你的 allTheFoos.

从"immoral"的角度来看（允许底部），FooType要么是Foo个构造函数的无限塔，要么是Foo个构造函数的有限塔底部的底部。这类似于"moral"这种类型的解释：

data Nat = Zero | Succ Nat

...但是底部不是零，这意味着你不能写这样的函数：

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

那会给我们留下什么？我认为结论是 FooType 并不是真正有用的类型，因为：

如果你看一下 "morally" 它等同于 ().
如果你看一下它 "immorally" 它类似于 Nat 但任何试图匹配 "zero" 的函数都是非终止的。

Answer 3

您的 FooType 的扩展可以是抽象语法树。以一个简单的示例语言为例，它只有整数、和和倒数，类型定义为

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

以下所有都是 Exp 实例：

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 )

如果我们从 Exp 定义中删除 AnInt 和 ASum，该类型将与您的 FooType 同构（用 AnInverse 替换 Foo）。

Answer 4

让我们稍微扩展一下您的数据类型 - 让我们将递归包装到一个类型参数中：

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

（因此您的原始数据类型为 FooType Identity）。

现在我们可以通过任何 f :: * -> * 来调制递归引用。但是这个扩展类型非常有用！事实上，它可以用于使用非递归数据类型来表达任何递归数据类型。一个众所周知的包是 recursion-schemes，如 Fix:

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

例如，如果我们定义

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

那么 Fix (List' a) 同构于 [a]:

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

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

此外，Fix允许我们在递归数据类型上定义许多通用操作，例如folding/unfolding (catamorphisms/anamorphisms).

Answer 5

以下类型：

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

虽然与您的不完全相同，但具有相似的精神，Launchbury、Krstic 和 Sauerwein 已经证明在协程方面有有趣的用途：https://arxiv.org/pdf/1309.5135.pdf

无限递归类型有用吗？

Is an infinitely recursive type useful?

haskell

ghc

评估计数器

空类型