2

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

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

我能得到的“更好”是这样，但它不进行类型检查（预期类型是 µ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 answer解释的那样，可以定义 anewtype如下：

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，但正如这个问题所示，如果没有额外的语言构造，它就不够灵活。

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

4

1 回答 1

5

在 Haskell 中，如果没有额外的dataor ，你就无法做到这一点。newtype

为此，需要编写

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

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

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

whereF a被定义为附加类型

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

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

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

有人可能会争辩说 in是 a foo True，所以我们可以推断和。结果是。TrueBoolf = \t->ta = Boolfoo True :: (\t->t) Char = Char

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

一般来说，我们不喜欢这样。我们希望通过模式匹配f并a针对实际类型进行类型推断。为此，我们希望两者都在实际类型中f具有a相应的“明显”名称。

值得一提的是，您可以使用依赖类型的语言来执行此操作，例如 Coq、Agda、Idris 等。在那里，类型推断不适用于foo True上述代码，因为f无法推断。更糟糕的是，在这些语言中，如果bar :: f a -> ...我们调用bar [True], thenf可能无法推断出来，[]因为这不是唯一的解决方案（尽管它们确实有很好的启发式方法，但它通常仍然有效，即使一般问题无法确定）。

于 2018-06-18T14:38:46.673 回答