写一个没有case的空case函数

Question

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 ???

Answer 1

好吧，你可以使用一个可怕的 CPP hack：

{-# LANGUAGE CPP #-}
#define Absurd      = \case {}

f :: X1 :~: X2 -> Void
f Absurd   -- expands to "f = case {}"

但是，如果您正在寻找使用纯 Haskell 语法的解决方案，我很确定答案是否定的。f与空情况不同，如果没有至少一种模式，则无法使用模式语法进行定义。而且，GHC 没有将任何模式理解为无人居住类型术语的秘密代码。（即使有，也没有语法允许您定义f pat没有右侧的 。）