In Haskell there is a term undefined :: a, which is said to be a term
representation of a bad computation or endless loop. Since undefined has
type a, them it's possible to create any syntactic correct type by
applying type substitutions. So undefined has any type and the o inverse is also true: any type has undefined, which is the bottom value living inside of any type (including the Void type, right?).
Curry-Howard isomorphism gives more than proposition as types, it also gives habited types as theorems.
A logic system with all propositions as theorems is said to be inconsistent.
So, Haskell's type system isomorphic to an inconsistent logic system?
If so, what are the consequences?
If Haskell's type system is a inconsistent proof system, them we can't trust it?
Would be possible to represent endless loop with no undefined?