This is a linkpost for https://www.overleaf.com/read/tpprrdczvfkp
Haskell doesn't actually let you do this as far as I can tell, but the natural computational way to implement a function is with a case expression with no cases. This is sensible because 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 is just the -ary sum type.
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.