在依赖类型的函数式编程语言中，展平列表是否更容易？ [英] Is flattening a list easier in dependently typed functional programming languages?

问题描述

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

编辑：有些答案在Haskell中提供了解决办法，用于自定义数据类型，或者借助TypeFamilies或MultiParamTypeClasses(如下面Noughtmare的答案或post above中的‘Landei’的答案或this帖子中的‘John L’的答案)。 然而，这些族和类似乎也是由于Haskell中缺少/替换依赖类型而引入的(例如，haskell wiki状态为[...]非常类似于依赖类型&。

我现在的问题是，Haskell从一开始确实不是用来定义这样的函数的(例如，扁平化不同深度的列表)，而且，一旦转移到实现dependent types的语言，这些问题是否就会消失？(例如，Idris、AGDA、Coq等...)我没有使用这些语言的经验，这就是我问的原因。

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

后续问题还将是：在Haskell中解决此问题的那些系列和类是否在Haskell中提供了依赖类型理论的完整实现，如果不是，有哪些重要的区别？

推荐答案

您可以在不需要指定输出类型的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]

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

这篇关于在依赖类型的函数式编程语言中，展平列表是否更容易？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！