[Haskell-cafe] Haskell's type system

[Luke Palmer]

On Tue, Jun 17, 2008 at 2:40 PM, Ron Alford <ronwalf at volus.net> wrote:
> 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?

Sort of, via the Curry-Howard Correspondence.  Haskell's type system
corresponds to a constructive logic (no law of excluded middle).
Arbitrary quantifiers are also introduced via the RankNTypes (I think
that's what it's called) extension.

Haskell's type system is a straightforward polymorphic type system for
the lambda calculus, so researching the Curry-Howard Correspondence
will probably get you what you want.

Luke