Data.Void.absurd与different有什么不同？

我今天早些时候看到了荒谬功能的逆向,虽然我很清楚,任何可能的实现drusba :: a -> Void都永远不会终止(毕竟,它是不可能构建的Void),但我不明白为什么同样不是这样absurd :: Void -> a.考虑GHC的实施:

newtype Void = Void Void

absurd :: Void -> a
absurd a = a `seq` spin a where
   spin (Void b) = spin b

spin在我看来,它无休止地解开了无限系列的Void新型包装器,即使你能找到Void传递它也永远不会返回.无法区分的实现类似于:

absurd :: Void -> a
absurd a = a `seq` undefined

鉴于此,为什么我们说这absurd是一个值得生活在Data.Void中的适当函数,但是

drusba :: a -> Void
drusba = undefined

是一个不可能定义的函数？它是否像以下那样？

absurd是一个总函数,为其(空)域中的任何输入提供非底部结果,而drusba为部分,给出其域中某些(实际上所有)输入的最低结果.

chi.. 20

由于历史原因,任何Haskell数据类型(包括newtype)必须至少有一个构造函数.

因此,要定义Void"Haskell98",需要依赖类型级递归newtype Void = Void Void.此类型没有(非底部)值.

该absurd函数必须依赖(值级)递归来处理该Void类型的"怪异"形式.

在更现代的Haskell中,通过一些GHC扩展,我们可以定义零构造函数数据类型,这将导致更健全的定义.

{-# LANGUAGE EmptyDataDecls, EmptyCase #-}
data Void
absurd :: Void -> a
absurd x = case x of { }    -- empty case

这个案例是详尽无遗的 - 它确实处理了所有构造函数Void,它们都是零.因此它是完全的.

在其他一些函数式语言中,如Agda或Coq,上面案例的变体在处理空类型时是惯用的Void.

1> chi..：

---

由于历史原因,任何Haskell数据类型(包括newtype)必须至少有一个构造函数.

因此,要定义Void"Haskell98",需要依赖类型级递归newtype Void = Void Void.此类型没有(非底部)值.

该absurd函数必须依赖(值级)递归来处理该Void类型的"怪异"形式.

在更现代的Haskell中,通过一些GHC扩展,我们可以定义零构造函数数据类型,这将导致更健全的定义.

{-# LANGUAGE EmptyDataDecls, EmptyCase #-}
data Void
absurd :: Void -> a
absurd x = case x of { }    -- empty case

这个案例是详尽无遗的 - 它确实处理了所有构造函数Void,它们都是零.因此它是完全的.

在其他一些函数式语言中,如Agda或Coq,上面案例的变体在处理空类型时是惯用的Void.

---

我们现在实际上*做*看到我的回答.

---

`data Void:设置MkVoid:Void→Void`是Agda中完全有效的定义.那么是'归纳虚空:类型:= MkVoid:虚空 - >无效.你可以定义相应的`absurd`函数就好了.

2> dfeuer..：

---

Data.Void从void包移到base基本版4.8(GHC 7.10).如果您查看Cabal文件,void您会发现它仅包含Data.Void旧base版本.现在,Void定义为chi建议:

data Void

absurd :: Void -> a
absurd a = case a of {}

这是完全有效的.

---

我认为旧定义背后的想法是这样的:

考虑类型

data BadVoid = BadVoid BadVoid

此类型无法完成工作,因为实际上可以使用该类型定义非底部(coinductive)值:

badVoid = BadVoid badVoid

我们可以通过使用严格注释来解决这个问题,严格注释(至少是一种)强制类型是归纳的:

data Void = Void !Void

在可能或可能不实际持有的假设下,但至少在道德上持有,我们可以合理地对任何归纳类型进行归纳.所以

spin (Void x) = spin x

如果假设我们有类型的东西,它将永远终止Void.

最后一步是用newtype替换single-strict-constructor数据类型:

newtype Void = Void Void

这总是合法的.spin然而,由于在data和之间存在不同的模式匹配语义,因此定义已经改变了含义newtype.为了准确地保留其含义,spin应该已经写好了

spin !x = case x of Void x' -> spin x'

(避免spin !(Void x)在新类型构造函数和爆炸模式之间的交互中绕过现在修复的错误;但是对于GHC 7.10(哈!),这种形式实际上并不会产生所需的错误消息,因为它被"优化"为无限循环)点absurd = spin.

值得庆幸的是,它最终并不重要,因为整个旧定义有点愚蠢.