Curry – Howard – Lambek and the Isomorphism
timothysamson.github.io
timothysamson.github.io
What was it about proving the law of the excluded middle that required the unsafecoerce import?
In the context of Haskell and the Curry-Howard correspondence, the LEM is not directly provable in a pure, total functional programming language. This is because such languages correspond to intuitionistic logic, a form of logic that does not accept the LEM as a given.
The unsafeCoerce function in Haskell is a way to bypass the type system. It allows you to coerce one type into another without any checks or balances. This is generally considered "unsafe" because it can lead to runtime errors if used incorrectly. however, in this case, it's used to "force" the proof of the LEM.
the author is using unsafeCoerce to demonstrate that while you can't prove the LEM within the confines of the type system (which corresponds to intuitionistic logic), you can still "cheat" and assert it by stepping outside of the system. This is a reflection of the fact that while the LEM is not accepted in intuitionistic logic, it is still accepted in classical logic, which allows for such "unsafe" maneuvers.