Is Haskell's type system isomorphic to an inconsistent logic system? If so, what are the consequences? : <p>In Haskell there is a term <code>undefined :: a</code>, which is said to be a term
representation of a bad computation or endless loop. Since <code>undefined</code> has
type <code>a</code>, them it's possible to create any syntactic correct type by 
applying type substitutions. So <code>undefined</code> has any type and the o inverse is also true: any type has <code>undefined</code>, which is the bottom value living inside of any type (including the <code>Void</code> type, right?).</p>

<p>Curry-Howard isomorphism gives more than proposition as types, it also gives habited types as theorems.</p>

<p>A logic system with all propositions as theorems is said to be inconsistent.</p>

<p>So, Haskell's type system isomorphic to an inconsistent logic system?</p>

<p>If so, what are the consequences?</p>

<p>If Haskell's type system is a inconsistent proof system, them we can't trust it?</p>

<p>Would be possible to represent endless loop with no <code>undefined</code>?</p>
