[Haskell-cafe] Haskell's type system

[Edsko de Vries]

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