[Haskell-cafe] Haskell's type system
Luke Palmer
lrpalmer at gmail.com
Wed Jun 18 01:00:36 EDT 2008
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
More information about the Haskell-Cafe
mailing list