如何在Idris依赖类型语言中实现0=1到Void的absurdity函数？

首先明确核心结论：不能直接编写空lambda表达式，让编译器在无任何模式匹配的情况下自动识别0与1不相等的事实、完成合法类型推导。

三类可行的实现路径 #

• 手写不可达构造器的匹配
  我们常用的=在Idris中对应内置的Equal类型，其唯一构造器为Refl : x = x。对于0 = 1这个类型，不存在任何合法的Refl实例（因为Refl要求等式两侧的值完全一致，而0和1是自然数下两个互不相同的构造项），因此可以直接写出匹配分支并标记为不可达：

  absurdity : 0 = 1 -> Void
  absurdity Refl impossible
  

  这个定义的合法性来自Idris的精细化类型检查：当编译器校验Refl的匹配逻辑时，会尝试统一等式两侧的0和1，发现二者无法匹配，因此判定该分支永远不会被实际触发，完全符合函数类型的定义要求。
• 复用标准库的内置工具
  标准库提供的absurd函数本身就支持从“不可能成立的等式”推导出任意类型（自然也包括Void），可以直接复用实现：

  absurdity : 0 = 1 -> Void
  absurdity eq = absurd eq
  

  这个标准库函数的内部实现，就是前面提到的“匹配Refl构造器并标记为不可达”的逻辑。
• 借助自动证明能力生成实现
  在支持定理自动求解的Idris版本中，可以通过%search指令让编译器自动推导函数实现：

  absurdity : 0 = 1 -> Void
  absurdity eq = %search
  

  但这个过程本质是编译器帮你检索到“0 ≠ 1”的证明项、自动完成反演生成Void，并不是空lambda带来的推导效果。

裸空lambda不合法的原因 #

不少人会尝试直接写无任何分支的空lambda（比如absurdity = \case），认为这样能触发编译器的不可能类型检查，但这种写法实际会触发穷尽性匹配错误。
逻辑很简单：编译器的穷尽检查流程是，如果你没有列出对Equal类型唯一构造器Refl的匹配项，就会默认你遗漏了所有可能的输入分支，根本不会深入到精细化校验环节、判断这个Refl能不能匹配0 = 1的场景。只有主动写出对Refl的匹配，让编译器进入匹配校验流程，它才能识别到这个分支是完全不可达的，进而接受impossible标记，完成合法的类型推导。 #

内容的提问来源于stack exchange，提问作者rambi