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

Question

在 Haskell 中寻找一个可以将任意深度嵌套列表展平的函数时，即一个concat递归应用并在最后一次迭代（使用非嵌套列表）时停止的函数，我注意到这需要有一个更灵活的类型系统，因为列表深度不同，输入类型也不同。事实上，有几个 stackoverflow 问题——比如这个问题——其中的回答指出“不存在一个函数可以‘查看’不同深度的不同嵌套列表”。

编辑：一些答案提供哈斯克尔的解决方法，无论是对自定义数据类型或具有帮助TypeFamilies或MultiParamTypeClasses（如在由Noughtmare下面的答案，或者通过“Landei”在回答上述职位或由“约翰·L”回答这个职位）。然而，这些家族和类似乎也是因为缺少/替代haskell 中的依赖类型而引入的（例如，haskell wiki声明“类型家族 [...] 很像依赖类型”。

我现在的问题是，如果这是真的，哈斯克尔的确originially没有定义此类功能（即如扁平化不同深度的列表），而且，如果这些问题就会消失，一旦一个移动到语言实现由依赖类型？（例如 Idris、Agda、Coq 等）我没有使用这些语言的经验，这就是我问的原因。

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

一个后续问题也将是：在haskell 中解决这个问题的那些族和类是否在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]

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