Topic: Haskell is inconsistent???
Kenny Lau (Apr 13 2020 at 11:12):
Looks like it is a well-known fact that Haskell is inconsistent. What does it mean and does it matter?
Mario Carneiro (Apr 13 2020 at 11:15):
If you use the Curry Howard isomorphism, aka propositions as types, any type theory has a corresponding logic. However, any programming language that is turing complete, with unguarded recursion or infinite loops, corresponds to a logic that is inconsistent. This is fine because these logics aren't being used for proving things, and it doesn't mean that you can necessarily break the type system (of course, you might still be able to break the type system for other reasons, e.g. unchecked cast).
Mario Carneiro (Apr 13 2020 at 11:16):
Here's an easy haskell style proof of false:
def foo : false := foo
Mario Carneiro (Apr 13 2020 at 11:17):
in haskell this term is called "bottom" and it inhabits every type
Reid Barton (Apr 13 2020 at 13:24):
And there are many more complicated ones, starting with the one you linked to. But happily since Haskell has general recursion anyways, we can declare them not to be problems and get lots of other nice things, like non-strictly positive inductive types and so on.
Last updated: May 11 2021 at 00:31 UTC