在依赖类型的函数式编程语言中,展平列表是否更容易? [英] Is flattening a list easier in dependently typed functional programming languages?
本文介绍了在依赖类型的函数式编程语言中,展平列表是否更容易?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
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屋!
查看全文