On Tue, Jun 17, 2008 at 2:40 PM, Ron Alford <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
