定义具有最小不动点、求和和乘积类型的列表

Question

我只想使用此类型定义来定义列表：

data Unit = Unit
data Prod a b = P a b
data Sum a b = L a | R b
newtype Mu f = Mu (forall a . (f a -> a) -> a)

我成功定义了如下自然数：

zeroMu = Mu $ \f -> f $ L Unit
succMu (Mu g) = Mu $ \f -> f $ R $ g f

我知道如何在额外数据类型的帮助下定义列表：

data ListF a x = NilF | ConsF a x
nilMu' = Mu $ \f -> f $ NilF
consMu' x (Mu g) = Mu $ \f -> f $ ConsF x $ g f

我能得到的 'better' 是这个，但它没有类型检查（预期类型是 µL.(1+(a*L))）：

nilMu = Mu $ \f -> f $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ R $ P x $ g f

如何仅使用先前定义的类型及其构造函数来定义 nilMu 和 consMu？

编辑

正如@chi 回答所解释的那样，可以按如下方式定义 newtype：

newtype F a x = F (Sum Unit (Prod a x))
nilMu = Mu $ \f -> f $ F $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ F $ R $ P x $ g f

它进行类型检查，但需要定义一个新类型。

本题的目的是用单位、积、求和和递归类型扩展简单类型的组合逻辑。前三种类型很容易实现，引入了 7 个新组合器 (unit、pair、first、second、left、right、case).递归类型似乎也很容易实现，只需添加一个类型构造函数组合器 mu，但正如这个问题所示，如果没有额外的语言构造，它就不够灵活。

这个问题有解决办法吗？是否有递归类型的组合逻辑可供参考？

Answer 1

如果 Haskell 中没有额外的 data 或 newtype，您将无法完成此操作。

要做到这一点，需要编写

nilMu :: Mu (\l -> S (P a l) ())
consMu :: a -> Mu (\l -> S (P a l) ()) -> Mu (\l -> S (P a l) ())

但 Haskell 不允许以这种方式使用类型级函数。 Mu 只能应用于类型 * -> * 的类型构造函数，不能应用于同类的类型级函数。

nilMu :: Mu (F a)
consMu :: a -> Mu (F a) -> Mu (F a)

其中 F a 定义为附加类型

newtype F a x = F (S (P a x) ())

由于Haskell不允许类型级函数，考虑

assuming foo :: f a -> f Char
infer    foo True :: ???

有人可能会争辩说，在foo True中，True是一个Bool，因此我们可以推断出f = \t->t和a = Bool。结果是 foo True :: (\t->t) Char = Char.

有人可能还会争辩说我们可以推断出 f = \t->Bool 和 a = String，结果是 foo True :: (\t->Bool) Char = Bool

总的来说，我们不喜欢那样。我们希望通过模式匹配 f 和 a 与实际类型进行类型推断。为此，我们希望 f 和 a 在实际类型中都有对应的 "obvious" name。

对于它的价值，你可以在依赖类型的语言中做到这一点，例如 Coq、Agda、Idris 等。在那里，类型推断不适用于像这样的代码foo True 以上，因为 f 无法推断。更糟糕的是，在这些语言中，如果 bar :: f a -> ... 并且我们调用 bar [True]，那么 f 可能无法推断为 []，因为这不是唯一的解决方案（它们确实有很好的不过，启发式方法通常仍然有效，即使一般问题是不可判定的）。

定义具有最小不动点、求和和乘积类型的列表

Define lists with least fixed point, sum, and product types

haskell

type-theory

fixpoint-combinators