Haskell doesn’t actually let you do this as far as I can tell, but the natural computational way to implement a function Bot−>A is with a case expression with no cases. This is sensible because Bot has no constructors, so it should be possible to pattern match it with such an expression. Another way of thinking of this is that we can use pattern matching on sum types and Bot is just the 0-ary sum type.
Thanks for pointing that out. My feeling is still “well yes, that’s technically true, but it still seems unnatural, and explosion is still the odd axiom out”.
Coq, for example, allows empty case expressions (for empty types), and I expect that other languages which double as proof assistants would support them as well… for the very purpose of satisfying explosion. General purpose languages like Haskell (and I just checked OCaml too) can seemingly overlook explosion/empty cases with few if any practical problems.
Interesting! Can you make a specific model of a 5-and-10 failure in minimal logic, using something similar to the “malicious proof search ordering” 5-and-10 failure in classical logic?
Thanks for the suggestion, Patrick. I’ve now adapted Tsvi’s formal argument to the reframed “5-equals-10 problem” and added it into the last section of my writeup.
Haskell doesn’t actually let you do this as far as I can tell, but the natural computational way to implement a function Bot−>A is with a case expression with no cases. This is sensible because Bot has no constructors, so it should be possible to pattern match it with such an expression. Another way of thinking of this is that we can use pattern matching on sum types and Bot is just the 0-ary sum type.
Thanks for pointing that out. My feeling is still “well yes, that’s technically true, but it still seems unnatural, and explosion is still the odd axiom out”.
Coq, for example, allows empty case expressions (for empty types), and I expect that other languages which double as proof assistants would support them as well… for the very purpose of satisfying explosion. General purpose languages like Haskell (and I just checked OCaml too) can seemingly overlook explosion/empty cases with few if any practical problems.
Interesting! Can you make a specific model of a 5-and-10 failure in minimal logic, using something similar to the “malicious proof search ordering” 5-and-10 failure in classical logic?
Thanks for the suggestion, Patrick. I’ve now adapted Tsvi’s formal argument to the reframed “5-equals-10 problem” and added it into the last section of my writeup.