Jac*_*han 72 polymorphism haskell parametric-polymorphism
其他潜在贡献者请注意:请不要犹豫,使用抽象或数学符号来表达您的观点.如果我发现你的答案不清楚,我会要求澄清,但你可以随意以舒适的方式表达自己.
要明确:我不是在寻找"安全" head,也不是head特别有意义的选择.问题的关键在于讨论head和讨论,并head'提供了背景.
我几个月来一直在用Haskell进行攻击(直到它已经成为我的主要语言),但我对一些更先进的概念以及语言哲学的细节都不了解(尽管我非常愿意学习).那么我的问题不是技术问题(除非它是,我只是没有意识到),因为它是一种哲学.
对于这个例子,我说的是head.
我想你会知道,
Prelude> head []
*** Exception: Prelude.head: empty list
这是从head :: [a] -> a.很公平.显然,一个人不能返回(挥手)没有类型的元素.但与此同时,定义它很简单(如果不是微不足道的话)
head' :: [a] -> Maybe a
head' [] = Nothing
head' (x:xs) = Just x
我见过一些这方面的讨论很少在这里的某些语句的注释部分.值得注意的是,一位Alex Stangl说
"有充分的理由不让一切都"安全",并在违反前提条件时抛出异常.
我不一定质疑这个断言,但我很好奇这些"好理由"是什么.
此外,保罗约翰逊说,
'例如你可以定义"safeHead :: [a] - >也许是",但现在不是处理空列表或证明它不会发生,你必须处理"没什么"或证明它不会发生".
我从该评论中读到的语气表明,这是难度/复杂度/事物的显着增加,但我不确定我是否掌握了他在那里推出的内容.
一位Steven Pruzina说(2011年,不低于),
"有一个更深层次的原因,例如'head'不能防止崩溃.要进行多态而处理空列表,'head'必须始终返回任何特定空列表中不存在的类型变量.它将是Delphic如果Haskell能做到这一点......".
允许空列表处理会导致多态性丢失吗？如果是这样,怎么样,为什么？是否有特殊情况会使这一点变得明显？本节由@Russell O'Connor充分回答.当然,任何进一步的想法都会受到赞赏.
我会根据清晰度和建议来编辑这个.您可以提供的任何想法,论文等都将非常感激.
Rus*_*nor 98
允许空列表处理会导致多态性丢失吗？如果是这样,怎么样,为什么？是否有特殊情况会使这一点变得明显？
免费的定理head指出,
f . head = head . $map f
应用这个定理[]意味着
f (head []) = head (map f []) = head []
这个定理必须适用于每一个f,所以特别是它必须适用于const True和const False.这意味着
True = const True (head []) = head [] = const False (head []) = False
因此,如果head是正确的多态并且head []是总值,则True相等False.
PS.我还有一些关于你的问题背景的评论,如果你有一个前提条件,你的列表是非空的,那么你应该通过在函数签名中使用非空列表类型而不是使用列表来强制执行它.
Tsu*_*Ito 23
为什么有人使用head :: [a] -> a而不是模式匹配？其中一个原因是因为您知道参数不能为空并且不想编写代码来处理参数为空的情况.
当然,您head'的类型[a] -> Maybe a在标准库中定义为Data.Maybe.listToMaybe.但是如果你替换了headwith 的用法listToMaybe,你必须编写代码来处理空案例,这违背了使用目的head.
我并不是说使用head是一种很好的风格.它隐藏了它可能导致异常的事实,从这个意义上来说它并不好.但它有时很方便.关键在于head服务于某些无法满足的目的listToMaybe.
问题中的最后一个引用(关于多态)只是意味着不可能定义一个[a] -> a在空列表中返回值的类型函数(正如Russell O'Connor在他的答案中解释的那样).
期望以下内容是很自然的:xs === head xs : tail xs- 列表与其第一个元素相同,其次是其余元素.似乎合乎逻辑,对吧？
现在,让我们计算一下conses(应用程序:)的数量,忽略实际的元素,在应用声称的"法律"时[]:[]应该是相同的foo : bar,但前者有0个conses,而后者有(至少)一个.哦,哦,有些东西不在这里!
Haskell的类型系统尽管有其优势,但并不能表达出你应该只调用head一个非空列表(并且'law'仅对非空列表有效)的事实.使用head将证明的负担转移给程序员,程序员应该确保它不在空列表中使用.我相信像Agda这样依赖类型的语言可以在这里提供帮助.
最后,一个稍微更具操作性的哲学描述:应该如何head ([] :: [a]) :: a实施？用a薄薄的空气来扼杀一种类型的价值是不可能的(想想无人居住的类型data Falsum),并且相当于证明什么(通过Curry-Howard同构).