如何对迭代中类型发生变化但函数形式相同的函数进行“迭代”

Posted 2021-04-07

我刚刚开始学习Haskell，我遇到了以下问题。我尝试“迭代”函数x->[x]。我希望得到结果[[8]]

foldr1 (.) (replicate 2 (x->[x])) $ (8 :: Int)

这不起作用，并给出以下错误消息：

发生检查：无法构造无限类型：a ~ [a]

预期类型：[a -> a]

实际类型：[a -> [a]]

我能理解为什么它不起作用。这是因为foldr1有类型签名foldr1 :: Foldable t => (a -> a -> a) -> a -> t a -> a，并将a -> a -> a作为其第一个参数的类型签名，而不是a -> a -> b

这也不是，出于同样的原因：

((!! 2) $ iterate (x->[x]) .) id) (8 :: Int)

但是，这有效：

(x->[x]) $ (x->[x]) $ (8 :: Int)

我明白第一个(x->[x])和第二个是不同类型（即[Int]->[[Int]]和Int->[Int]），虽然形式上看起来一样。

现在说我需要将2改为大数，比如说100。

我的问题是，有没有办法建立这样的清单？我是否必须采用模板Haskell等元编程技术？如果我不得不求助于元编程，我该怎么办呢？

作为一个侧节点，我也尝试构造这样一个列表的字符串表示和read它。虽然字符串更容易构造，我不知道如何read这样的字符串。例如，

read "[[[[[8]]]]]" :: ??

当嵌套层的数量不是先验已知时，我不知道如何构造??部分。我能想到的唯一方法就是采用元编程。

上面的问题似乎不够有趣，我有一个“现实生活”的案例。考虑以下功能：

natSucc x = [Left x,Right [x]]

这是succ中使用的formal definition of natural numbers函数。再次，我不能简单地foldr1-replicate或!!-iterate它。

任何帮助将不胜感激。关于代码样式的建议也是受欢迎的。

编辑：在查看到目前为止给出的3个答案之后（再次，非常感谢您的时间和努力）我意识到这是一个更普遍的问题，不仅限于列表。可以为每个有效类型的仿函数组成类似的问题（如果我想获得Just Just Just 8，虽然这可能没有多大意义？）。

答案

这个问题确实需要一些先进的类型级编程。

我在评论中遵循了@ chi的建议，并搜索了一个库，该库为其相应的单例提供了归纳类型级自然。我找到了fin库，用于答案。

类型级欺骗的通常扩展：

{-# language DataKinds, PolyKinds, KindSignatures, ScopedTypeVariables, TypeFamilies #-}

这是一个type family，它将类型级自然元素和元素类型映射到相应嵌套列表的类型：

import Data.Type.Nat

type family Nested (n::Nat) a where
    Nested Z a = [a]
    Nested (S n) a = [Nested n a]

例如，我们可以测试from ghci

*Main> :kind! Nested Nat3 Int
Nested Nat3 Int :: *
= [[[[Int]]]]

（Nat3是Data.Type.Nat中定义的方便别名。）

这是一个包装我们想要构造的函数的newtype。它使用类型族来表示嵌套级别

newtype Iterate (n::Nat) a = Iterate { runIterate :: (a -> [a]) -> a -> Nested n a }

鳍库提供了一个非常漂亮的induction1函数，让我们通过Nat上的归纳来计算结果。我们可以用它来计算与每个Iterate相对应的Nat。 Nat隐含地传递，作为constraint：

iterate' :: forall n a. SNatI n => Iterate (n::Nat) a
iterate' =
    let step :: forall m. SNatI m => Iterate m a -> Iterate (S m) a
        step (Iterate recN) = Iterate (f a -> [recN f a])
    in  induction1 (Iterate id) step

在ghci中测试函数（使用-XTypeApplications提供Nat）：

*Main> runIterate (iterate' @Nat3) pure True
[[[[True]]]]

另一答案

你肯定同意2 :: Int和4 :: Int有相同的类型。因为Haskell不是dependently typed†，这意味着foldr1 (.) (replicate 2 (x->[x])) (8 :: Int)和foldr1 (.) (replicate 4 (x->[x])) (8 :: Int)必须具有相同的类型，与你的想法相反，前者应该给[[8]] :: [[Int]]和后者[[[[8]]]] :: [[[[Int]]]]。特别是，应该可以将这两个表达式放在一个列表中（Haskell列表需要为其所有元素使用相同的类型）。但这只是行不通。

关键是你并不真正想要一个Haskell列表类型：你希望能够在一个结构中拥有不同深度的分支。好吧，你可以拥有它，它不需要任何聪明的类型系统黑客 - 我们只需要清楚这不是一个列表，而是一棵树。像这样的东西：

data Tree a = Leaf a | Rose [Tree a]

那你可以做

Prelude> foldr1 (.) (replicate 2 (x->Rose [x])) $ Leaf (8 :: Int)
Rose [Rose [Leaf 8]]
Prelude> foldr1 (.) (replicate 4 (x->Rose [x])) $ Leaf (8 :: Int)
Rose [Rose [Rose [Rose [Leaf 8]]]]

---

†实际上，现代GHC Haskell有很多依赖类型的功能（参见DaniDiaz的回答），但这些仍然与价值级语言明显分开。

另一答案

我想提出一个非常简单的替代方案，它不需要任何扩展或欺骗：不要使用不同的类型。

这是一种类型，可以保存包含任意数量嵌套的列表，只要你说前面有多少：

data NestList a = Zero a | Succ (NestList [a]) deriving Show
instance Functor NestList where
    fmap f (Zero a) = Zero (f a)
    fmap f (Succ as) = Succ (fmap (map f) as)

这种类型的值是一个教堂数字，表示有多少层嵌套，后面是一个有很多层嵌套的值;例如，

Succ (Succ (Zero [['a']])) :: NestList Char

写你的qazxsw poi iterator现在很容易了！因为我们想要一层嵌套，我们添加一个qazxsw poi。

x -> [x]

您可以类似地修改关于如何实现自然数的提议，以使用简单的递归类型。但标准方式更清晰：只需采取上述Succ并删除所有参数。

> iterate (x -> Succ (fmap (:[]) x)) (Zero 8) !! 5
Succ (Succ (Succ (Succ (Succ (Zero [[[[[8]]]]])))))