3 ms·
Curry – Howard – Lambek and the Isomorphism
- mrkeen 3y agoVery cool. What was it about proving the law of the excluded middle that required the unsafecoerce import?
- weatherlight 3y agoit states that there are no "middle" options between truth and falsehood. 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.