Haskell is inconsistent???

Stream: general

[Kenny Lau]

Looks like it is a well-known fact that Haskell is inconsistent. What does it mean and does it matter?

[Mario Carneiro]

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]

Here's an easy haskell style proof of false:

def foo : false := foo

[Mario Carneiro]

in haskell this term is called "bottom" and it inhabits every type

[Reid Barton]

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.