どうData.Void.absurdは⊥と異なっているのですか？

Question

今日はInverse of the absurd functionが見えましたが、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のnewtypeラッパーの無限級数を解明されているようだ、とあなたはそれを渡すために Voidを見つけることができる場合であっても戻らないだろう。区別できない実装はのようになります。

ことを考えると

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

、なぜ我々はabsurdがData.Voidに住むに値する適切な機能であると言うが、

drusba :: a -> Void 
drusba = undefined 

はAですかおそらく定義できない関数ですか？それは次のようなものですか？そのドメイン

absurddrusbaは、一部の底結果を与え、部分的であるのに対し、その（空の）ドメイン内の任意の入力のための非底結果を与え、合計関数である（実際にはすべての）入力。

Answer 1

Data.Voidvoidパッケージから（GHC 7.10）のbaseパッケージに移動されました。あなたはvoidためカバルファイルを見れば、あなたはそれが唯一の古いバージョンのbaseData.Voidが含まれていることがわかります。 Now, Void is defined as chi suggests：

data Void 

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

これは完全に有効です。

---

私は古い定義の背後にある考え方は、このようなものだと思う。それは定義して実際に可能だから

は、タイプ

data BadVoid = BadVoid BadVoid 

このタイプは、仕事を得るはありません考えてみましょうそのタイプの非ボトム（コインシデンス）値：

badVoid = BadVoid badVoid 

タイプを強制的に（少なくとも一種の）厳密アノテーションを、使用して誘導されるように：

か、実際に保持しない場合があります仮定の下で

data Void = Void !Void 

が、少なくとも道徳的に保持するには、我々は合法的に任意の誘導に誘導を行うことができますタイプ。 、仮に、私たちはタイプVoidの何かを持っているのであれば

spin (Void x) = spin x 

は常に終了します。

最後のステップは、のnewtypeで単厳密・コンストラクタデータ型を置き換えて：

newtype Void = Void Void 

これは常に正当なものです。しかし、spinの定義は、dataとnewtypeのパターンマッチングセマンティクスが異なるため、意味が変わりました。しかし、GHC 7.10（HA）のために、このフォームはdoesnの！;正確な意味を維持するために、spinはおそらくnewtypeのコンストラクタと強打パターン間の相互作用になりました - バグを修正スカートしspin !(Void x)を回避

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

を（書かれている必要があります無限ループに「最適化」されているため、実際には希望のエラーメッセージが生成されます）。absurd = spin。

ありがたいことに、古い定義全体がちょっとした馬鹿げた行為なので、結局は実際には問題ではありません。

Answer 2

歴史的な理由から、Haskellのデータ型（newtypeを含む）には少なくとも1つのコンストラクタが必要です。

したがって、 "Haskell98"でVoidを定義するには、型レベルの再帰newtype Void = Void Voidに依存する必要があります。このタイプのない（非ボトム）値はありません。

関数は、「奇妙な」形式のVoid型に対処するために（値レベル）再帰に頼らなければなりません。

は、より現代的なHaskellでは、いくつかのGHC拡張で、私たちは正気の定義につながるゼロコンストラクタデータ型を定義することができます。

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

ケースが網羅ある - それは、Voidのすべてのコンストラクタを処理し、それらのすべてはゼロ。したがって、それは合計です。

AgdaやCoqのような他の関数型言語では、Voidのような空の型を扱う場合、上記のケースの変種が慣用的です。