haskell - 在依赖类型的函数式编程语言中扁平化列表更容易吗？

Question

当在 haskell 中寻找一个可以压平任意深度嵌套列表的函数时，即递归应用 concat 并在最后一次迭代(使用非嵌套列表)时停止的函数，我注意到这个将需要有一个更灵活的类型系统，因为随着列表深度的变化，输入类型也会发生变化。事实上，有几个 stackoverflow 问题 - 例如 this一个 - 其中响应声明“不存在将‘查看’不同深度的不同嵌套列表的函数”。

编辑:一些答案在 haskell 中提供了解决方法，无论是针对自定义数据类型还是在 TypeFamilies 或 MultiParamTypeClasses 的帮助下(如下面 Noughtmare 的回答或答案由 post above 中的“Landei”或 this 帖子中的“John L”回答)。然而，这些族和类似乎也被引入，因为在 haskell 中缺少/来替代依赖类型(例如，haskell wiki 声明 “类型族是 [...] 很像依赖类型”.

我现在的问题是，haskell 是否确实最初不是为定义此类函数而设计的(例如，将不同深度的列表展平)，此外，一旦移动，此类问题是否会消失到实现 dependent types 的语言？ (例如 Idris、Agda、Coq，...)我没有使用这些语言的经验，这就是我问的原因。

例如，在 Idris 网站上，据说“类型可以作为参数传递给函数”，因此，我认为，在列表扁平化的情况下，可以简单地将列表的类型传递为参数并以直接的方式实现所需的功能。这可能吗？

后续问题也将是:在 haskell 中解决此问题的那些 Families 和 Classes 是否提供了 haskell 中依赖类型理论的完整实现，或者如果没有，有哪些重要区别？

Answer 1

你可以在 Haskell 中创建一个不需要指定输出类型的函数:

{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}

type family FlatT a where
  FlatT [[a]] = FlatT [a]
  FlatT a = a

class Flat a where
  flat :: a -> FlatT a

instance Flat [a] => Flat [[a]] where
  flat xs = flat $ concat xs

instance {-# OVERLAPPABLE #-} FlatT a ~ a => Flat a where
  flat x = x

main = print $ flat [["Hello"," "],["World", "!"]]

仍然存在的一个问题是您的列表中可能包含一个多态类型，它本身可能是一个列表。例如你可以写一个整数列表:

main = print $ flat [[1,2],[3,4,5]]

这会给出很多关于不明确变量的错误。一个简单的解决方法是向其中一个整数添加类型签名:[[1,2],[3,4,5::Int]]。这将修复所有错误。从某种意义上说，这个错误对我来说是不可避免的，因为你可以这样写一个实例:

instance Num [Int] where
  fromInteger n = replicate (fromInteger n) (fromInteger n)

然后你可以像这样使用它:

main = print $ [[1,2],[3,4,5 :: [Int]]]

哪个会返回:

[1,2,2,3,3,3,4,4,4,4,5,5,5,5,5]

如您所见，这会额外展开一层。因此，展开的层数取决于您在签名中提供的类型。对我来说，这听起来似乎无法避免类型签名，即使是在更强大的语言中也是如此。