英文:
How to write a function that returns the bottom type?
问题
我正在阅读PLFA书籍，已经到达否定部分，并好奇是否可以实现一个返回底部类型的函数：
foo : Set → ⊥
foo a = ?
似乎Agda接受了我的代码，但我找不到一种实现底部集合的方法，因为没有构造函数。我是否真的可以这样做？
英文:
I am reading the PLFA book and reached the section Negation, and curious to know if I can implement a function that returns the bottom type:
foo : Set → ⊥
foo a = ?
It seems agda accepts my code, but I cannot find a way to implement the bottom set as there is no constructor. Can I actually do that?
答案1
得分: 2
没有类型为 Set → ⊥ 的函数，正如您所描述的原因：无法构造类型为 ⊥ 的元素。然而，虽然不可能返回一个 ⊥ 类型的元素，但您可以编写一个函数，返回⊥类型（因为在Agda中，类型是头等对象）：
bar : Set → Set
bar a = ⊥
英文:
There is no function of type Set → ⊥, for exactly the reason you described: it is impossible to construct an element of type ⊥. However, while it is not possible to return an element of the ⊥ type, you can write a function that returns the ⊥ type (since types are first-class objects in Agda):
bar : Set → Set
bar a = ⊥
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论