How to write a function that returns the bottom type?

Question

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?

Answer 1

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