[Haskell-cafe] 3 level hierarchy of Haskell objects
jays at panix.com
Sat Aug 18 22:32:05 CEST 2012
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
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!
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. 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
> 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
> 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.
>>  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.
>>  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,
> Thanks, wren!
More information about the Haskell-Cafe