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? -Ron
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
On Jun 17, 2008, at 11:08 PM, Don Stewart wrote:
Haskell's type system is based on System F, the polymorphic lambda calculus. By the Curry-Howard isomorphism, this corresponds to second-order logic.
just nitpicking a little.... this should read "second-order propositional logic", right? daniel
On Tue, Jun 17, 2008 at 2:40 PM, Ron Alford
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
On Tue, Jun 17, 2008 at 04:40:51PM -0400, Ron Alford 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?
I'll give you some terms to Google for. The "ideal" type system for Haskell (ignoring type classes) is System F. Haskell'98 doesn't quite get there, but recent extensions such as boxy types and FPH do. System F corresponds to second order propositional logic: types correspond to propositions in this logic, and Haskell programs as the corresponding proofs (by the Curry-Howard isomorphism). The type system of Haskell'98 is a bit weird from a logical perspective, and sort of corresponds to the rank 1.5 predicative fragment of second order propositional logic (I say rank 1.5 because although no abstraction over rank 1 types is allowed normally, limited abstractions over rank 1 types is allowed through let-polymorphism -- so this is *almost* first order logic but not quite: slightly more powerful). Regarding type classes, I'm not 100% what the logical equivalent is, although one can regard a type such as forall a. Eq a => a -> a as requiring a proof (evidence) that equality on a is decidable. Where this sits formally as a logic I'm not sure though. Edsko
On 6/18/08, Edsko de Vries
Regarding type classes, I'm not 100% what the logical equivalent is, although one can regard a type such as
forall a. Eq a => a -> a
as requiring a proof (evidence) that equality on a is decidable. Where this sits formally as a logic I'm not sure though.
You can take the minimalist view and treat a typeclass parameter as an explicitly passed dictionary; that is: (Eq a => a -> a) is isomorphic to (a -> a -> Bool, a -> a -> Bool) -> a -> a In fact, this is basically what GHC does. You then treat an instance declaration: instance Eq Int where (==) = eqInt# (/=) = neqInt# as just a constant Eq_Int = (eqInt#, neqInt#) -- ryan
participants (6)
-
Daniel Gorín -
Don Stewart -
Edsko de Vries -
Luke Palmer -
Ron Alford -
Ryan Ingram