[Haskell-cafe] 3 level hierarchy of Haskell objects

[wren ng thornton]

On 8/13/12 5:42 PM, Jay Sulzberger wrote:
> One difficulty which must impede many who study this stuff is
> that just getting off the ground seems to require a large number
> of definitions of objects of logically different kinds. (By
> "logic" I mean real logic, not any particular formalized system.)
> We must have "expressions", values, type expressions, rules of
> transformation at the various levels, the workings of the
> type/kind/context inference system, etc., to get started.
> Seemingly Basic and Scheme require less, though I certainly
> mention expressions and values and types and
> objects-in-the-Lisp-world in my Standard Rant on^W^WIntroduction
> to Scheme.

Indeed, starting with Haskell's type system is jumping in at the deep 
end. And there isn't a very good tutorial on how to get started learning 
type theory. Everyone I know seems to have done the "stumble around 
until it clicks" routine--- including the folks whose stumbling was 
guided by formal study in programming language theory.

However, a good place to start ---especially viz a vis Scheme/Lisp--- is 
to go back to the beginning: the simply-typed lambda-calculus[1]. STLC 
has far fewer moving parts. You have type expressions, term expressions, 
term reduction, and that's it.

Other lambda calculi add all manner of bells and whistles, but STLC is 
the core of what lambda calculus and type systems are all about. So you 
should be familiar with it as a touchstone. After getting a handle on 
STLC, then it's good to see the Barendregt cube. Don't worry too much 
about understanding it yet, just think of it as a helpful map of a few 
of the major landmarks in type theory. It's an incomplete map to be 
sure. One major landmark that's suspiciously missing lays about halfway 
between STLC and System F: that's Hindley--Milner--Damas, or ML-style, 
lambda calculus.[2]

After seeing the Barendregt cube, then you can start exploring in those 
various directions. Notably, you don't need to think about the kind 
level until you start heading towards LF, MLTT, System Fw, or CC, since 
those are were you get functions/reduction at the type level and/or 
multiple sorts at the type level.

Haskell98 (and the official Haskell2010) take Hindley--Milner--Damas as 
the starting point and then add some nice things like algebraic data 
types and type classes (neither of which are represented on the 
Barendregt cube). This theory is still relatively simple and easy to 
understand, albeit in a somewhat ad-hoc manner.

Modern "Haskell" lives somewhere beyond the top plane of the cube. We 
have all of polymorphism (aka System F, aka second-order quantification; 
via -XRankNTypes), most of type operators (i.e., extending System F to 
System Fw; via type families etc), some dependent types (aka first-order 
quantification; via GADTs), plus things not represented on the cube 
(e.g., (co)inductive data types, type classes, etc). Trying to grok all 
of that at once without prior understanding of the pieces is daunting to 
be sure.


[1] Via Curry--Howard, the pure STLC corresponds to natural deduction 
for the implicational fragment of intuitionistic propositional logic. Of 
course, you can add products (tuples), coproducts (Either), and 
absurdity to get natural deduction for the full intuitionistic 
propositional logic.

[2] That is: STLC extended with rank-1 second-order quantification, 
which is a sweet spot in the tapestry of expressivity, decidability, et 
al. I don't think anyone knows exactly _why_ it's so sweet, but it truly is.

-- 
Live well,
~wren