如何编写返回bottom type的函数？Agda实现疑问

答案是不能实现，原因如下：

• ⊥（bottom type）在Agda里是没有任何构造子的类型，它代表逻辑上的矛盾——只有当某个命题本身自带矛盾时，我们才能构造出⊥的实例。
• 你的函数签名foo : Set → ⊥的含义是：对于任意集合类型（对应Curry-Howard同构里的任意命题），都能推导出矛盾。这等价于证明“所有命题都是假的”，但在构造性逻辑里这完全不成立——比如单位类型⊤（对应真命题）有明确的构造子tt，你不可能从⊤得到⊥的实例。
• Agda接受这个类型签名，只是因为类型检查器仅验证语法和类型规则的合法性，不会提前判断函数是否存在有效实现。你可以声明这样的函数，但永远填不出右侧的定义（除非引入矛盾公理，这违背标准构造性逻辑的一致性）。

举个反例：如果真能实现foo，调用foo ⊤就能得到一个⊥的实例，这直接打破了构造性逻辑的一致性——毕竟⊤是可构造的，而⊥是不可构造的，二者不可能同时成立。

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