[Haskell-cafe] Haskell's type system

Don Stewart dons at galois.com
Tue Jun 17 22:08:27 EDT 2008


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


More information about the Haskell-Cafe mailing list