[Haskell-cafe] Haskell's type system
dons at galois.com
Tue Jun 17 22:08:27 EDT 2008
> 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?
A quick link to get you started on the topic, I'm sure others will add
Haskell's type system is based on System F, the polymorphic lambda
calculus. By the Curry-Howard isomorphism, this corresponds to
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.
More information about the Haskell-Cafe