例如，我可以用空殼寫一些不可能的東西，并將其與. 一起使用Decision。
{-# LANGUAGE DataKinds, EmptyCase, LambdaCase, TypeOperators #-}
import Data.Type.Equality
import Data.Void
data X = X1 | X2
f :: X1 :~: X2 -> Void
f = \case {}
-- or
-- f x = case x of {}
case有沒有辦法通過直接模式匹配引數來撰寫等效項而不使用？
f :: X1 :~: X2 -> Void
f ???
uj5u.com熱心網友回復：
好吧，您可以使用可怕的 CPP hack：
{-# LANGUAGE CPP #-}
#define Absurd = \case {}
f :: X1 :~: X2 -> Void
f Absurd -- expands to "f = case {}"
但是，如果您正在尋找使用純 Haskell 語法的解決方案，我很確定答案是否定的。與空案例不同，您不能f在沒有至少一種模式的情況下使用模式語法進行定義。而且，GHC 沒有將模式理解為無人居住型別術語的密碼。（即使有，也沒有語法允許您定義f pat沒有右手邊的 a。）
uj5u.com熱心網友回復：
這是使用模式同義詞的嘗試。它并不完全令人滿意，可能不是你真正想要的。它只能實作\case{}從你的眼睛移開。我們仍然需要absurd在某些方面使用。
{-# LANGUAGE PatternSynonyms, ViewPatterns, GADTs #-}
{-# LANGUAGE DataKinds, EmptyCase, LambdaCase, TypeOperators #-}
import Data.Type.Equality
import Data.Void
data X = X1 | X2
pattern Abs :: Void -> a
pattern Abs x <- (\case{} -> x)
f :: 'X1 :~: 'X2 -> Void
f (Abs x) = x
g :: 'X1 :~: 'X2 -> a
g (Abs x) = absurd x
{-
Pattern match(es) are non-exhaustive
In an equation for `h':
Patterns of type 'X1 :~: 'X1 not matched: Refl
-}
h :: 'X1 :~: 'X1 -> Void
h (Abs x) = x
另一種選擇可能是利用 Template Haskell。
uj5u.com熱心網友回復：
我認為如果您想模仿這一點，最簡單的方法類似于評論中發布的答案：
f _ = undefined
但是，這是懶惰的：
f (error "aw beans") -- undefined
雖然空殼是嚴格的：
(\ case {} :: X1 :~: X2 -> Void) (error "aw beans") -- beans
所以更好的替代品將使用seq：
impossible :: a -> Void
impossible x = x `seq` impossible x
或者BangPatterns：
{-# Language BangPatterns #-}
impossible :: a -> Void
impossible !x = impossible x
然后你可以寫f = impossible，這對我來說似乎很不錯。（量詞在a邏輯上更像是“for any”而不是“for all”，但是哦，好吧。）你當然可以拋出一些更具描述性的東西，而不是陷入無限回圈，以防這種情況實際上并非不可能—— error "the impossible was possible after all"。
Void這也應該適用于asdata Void = Void !Void或newtype Void = Void Voidinvoid包的老式定義。
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/487889.html
標籤：哈斯克尔
上一篇：對Haskell中資料型別的困惑