On Thu, 9 Aug 2012, wren ng thornton <w...@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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
