ronwalf:
I'm trying to wrap my head around the theoretical aspects of haskell's type system. Is there a discussion of the topic separate from the language itself?
Since I come from a rather logic-y background, I have this (far-fetched) hope that there is a translation from haskell's type syntax to first order logic (or an extension there-of). Is this done? Doable?
A quick link to get you started on the topic, I'm sure others will add more material. Haskell's type system is based on System F, the polymorphic lambda calculus. By the Curry-Howard isomorphism, this corresponds to second-order logic. The GHC compiler itself implements Haskell and extensions by encoding them in System Fc internally, "which extends System F with support for non-syntactic type equality.". JHC, I believe, encodes Haskell into a pure type system internally, some sort of higher order dependently-typed polymorphic lambda calculus. -- Don