Hacker News new | past | comments | ask | show | jobs | submit login

`Void` being the uninhabited type, in the light of the Curry-Howard isomorphism stands for a false proposition.

`a -> Void` get interpreted as "not a" or "from a follows contradiction" or equivalently "a is uninhabited". Combinatorially it's `0 ^ a` which for non-empty a is zero but is equal to 1 when a is empty (0^0=1). In other words there are no functions of type `a -> Void` for non-empty a and there's exactly one such function for uninhabited a (id :: Void -> Void).

`Void -> a` is interpreted "from falsehood, anything (follows)" https://en.wikipedia.org/wiki/Principle_of_explosion. Combinatorially a^0 = 1 for all a so there's exactly one such function. An easy way to define it is by induction on Void (which has no cases and you're done).




Yeah, Void makes for great for inductive definitions ;)




Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: