[Haskell-cafe] 3 level hierarchy of Haskell objects

[Jay Sulzberger]

On Thu, 9 Aug 2012, wren ng thornton <wren at freegeek.org> wrote:

> On 8/8/12 9:41 PM, Jay Sulzberger wrote:
>> Haskell's type classes look to me to be a provision for declaring
>> a signature in the sense of the above article.
>
> Just to clarify this in the context of my previous post, type classes define 
> signatures in two significantly different ways.
>
> (1) The first way is as you suggest: the methods of a type class specify a 
> signature, and for convenience we give that signature a name (i.e., the type 
> class' name). However, this is a signature for the term level of Haskell 
> (i.e., a signature in the Term sort not discussed previously; elements of 
> Type classify elements of Term, just as elements of Kind classify elements of 
> Type).
>
> (2) The second way is that, at the type level, the collection of type class 
> names together form a signature. Namely they form the signature comprising 
> the majority of the Context sort.
>
> Both senses are important for understanding the role of type classes in 
> Haskell, but I believe that some of Patrick Browne's confusion is due to 
> trying to conflate these into a single notion. Just as terms and types should 
> not be confused, neither should methods and type classes. In both cases, each 
> is defined in terms of the other, however they live in separate universes. 
> This is true even in languages which allow terms to occur in type expressions 
> and allow types to occur in term expressions. Terms denote values and 
> computations (even if abstractly); whereas, types denote collections of 
> expressions (proper types denote collections of term expressions; kinds 
> denote collections of type expressions;...).
>
> -- 
> Live well,
> ~wren

Thanks, wren!

I am attempting to read the Haskell 2010 standard at

   http://www.haskell.org/onlinereport/haskell2010/

It is very helpful and much less obscure than I feared it would be.

What you say about the levels seems reasonable to me now, and I
begin dimly to see an outline of a translation to non-New Type
Theory stuff, which may help me to enter the World of New Type
Theory.

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.

oo--JS.