[Haskell-cafe] 3 level hierarchy of Haskell objects

[Jay Sulzberger]

When I was last on the best rooftop in the Mid Upper West Side of
Manhattan I was told of the work on logical relations.  I did not
know of this three decades old line of work.  I have grabbed

http://homepages.inf.ed.ac.uk/gdp/publications/Par_Poly.pdf

To me, the style is comfortable and the matter feels solid.
That is, the authors and I know some of the same kennings.

Thanks Lispers!  Thanks Haskellers!

oo--JS.


On Thu, 16 Aug 2012, Jay Sulzberger wrote:

>
>
> On Wed, 15 Aug 2012, wren ng thornton <wren at freegeek.org> wrote:
>
>> 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.
>
> Yes.  The simply-typed lambda-calculus presents as a different
> sort of thing from the "untyped" lambda calculus, and the many
> complexly typed calculi.
>
> I'd add the list of components of the base machine of STLC these
> things:
>
> 1. The model theory, which is close to the model theory of the
>   Lower Predicate Calculus.
>
> 2. The explication of "execution of a program", which is more
>   subtle than anything right at the beginning of the study of
>   the Lower Predicate Calculus.  It certainly requires a score
>   of definitions to lay it out clearly.
>
> But, to say again, yes the STLC can, like linear algebra 101, be
> presented in this way: The machine stands alone in bright
> sunlight.  There are no shadows.  Every part can be seen plainly.
> The eye sees all and is satisfied.
>
> ad 2: It would be worthwhile to have an introduction to STLC
> which compares STLC's explication of "execution of a program"
> with other standard explications, such as these:
>
> 1. the often not explicitly presented explication that appears in
>   textbooks on assembly and introductory texts on computer hardware
>
> 2. the usually more explicitly presented explication that appears
>   in texts on Basic or Fortran
>
> 3. the often explicit explication that appears in texts on Snobol
>
> 4. various explications of what a database management system does
>
> 5. explications of how various Lisp variants work
>
> 6. explications of how Prolog works
>
> 7. explications of how general constraint solvers work, including
>   "proof finders"
>
>> 
>> 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]
>
> 8. explication of how Hindley--Milner--Damas works
>
>> 
>> 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.
>
> Unexpectedly, to me, missing word in explications of algebraic
> data types and "pattern matching": "magma".
>
>> 
>> 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.
>
> Yes.
>
>> 
>> 
>> [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
>
> Thanks, wren!
>
> oo--JS.
>
>