CODEWITHSUNDEEP
agdaagda-mode
Chien
Chien

Reputation: 355

How to write a function that returns the bottom type?

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?

Upvotes: 0

Views: 270

Answers (1)

Jesper
Jesper

Reputation: 2955

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 = ⊥

Upvotes: 2

Related Questions