[Haskell-cafe] 3 level hierarchy of Haskell objects

[Jay Sulzberger]

On Wed, 8 Aug 2012, Ertugrul Söylemez <es at ertes.de> wrote:

> Patrick Browne <patrick.browne at dit.ie> wrote:
>
>> Gast [1] describes a 3 level hierarchy of Haskell objects using
>> elementOf from set theory:
>>
>> value  *elementOf*  type  *elementOf*  class
>
> This hierarchy is pretty arbitrary and quickly runs into problems with
> some type system extensions.  You can find out whether the barber of
> Seville shaves himself.
>
> A better hierarchial model is related to universes and uses type
> relations (assuming a right-associative ':'):
>
>    value : type : kind : sort : ...
>    value : type : universe 0 : universe 1 : universe 2 : ...
>
> A value is of a type.  A type is of the first universe (kind).  An n-th
> universe is of the (n+1)-th universe.
>
> Type classes can be modelled as implicit arguments.
>
>
>> If we include super-classes would the following be an appropriate
>> mathematical representation?
>
> What is a superclass?  What are the semantics?
>
>
> Greets,
> Ertugrul

I know no Haskell, so my first reactions are likely to fail to grip.

There is a type theory from one generation, or perhaps two or
three, before our time's New Crazed Type Theory.  This is the
type theory of the Lower Predicate Calculus and of Universal
Algebra, style of Birkhoff's Theorem on Varieties.  An
introduction to this type theory is presented here:

   http://en.wikipedia.org/wiki/Signature_%28logic%29
   [page was last modified on 27 March 2011 at 16:54]

Haskell's type classes look to me to be a provision for declaring
a signature in the sense of the above article.  An instance of
type t which belongs to a type class tc is guaranteed to have
certain attendant structures, just as the underlying set of a
group is automatically equipped with attendant, indeed defining,
operations of 1, *, and ^-1.  1 is a zeroary operation with
codomain the set of group elements, * is a binary operation that
is, has type g x g -> g, and ^-1 has type g -> g, where g is the
type of group elements of our particular group.  That this
particular group is indeed an instance of the general concept
group requires that t be of a type class which guarantees the
attendant three group operations 1, *, and ^-1, with types as
shown.  Note that the usual definition of group has further
requirements.  These further requirements are called
"associativity of *", "1 is an identity for *", and "^-1 is an
inverse for *".  I think that in Haskell today these requirements
must, in many cases, be handled by the programmer by hand, and
are not automatically handled by the type system of Haskell.
Though, as pointed out in an earlier post, in some cases one can
use certain constructions, constructions convenient in Haskell,
to guarantee that operations so defined meet the requirements.

Here we are close to the distinction between a class of "objects
which satisfy a condition" vs "objects with added structure", for
which see:

   http://math.ucr.edu/home/baez/qg-spring2004/discussion.html
   http://ncatlab.org/nlab/show/stuff,+structure,+property

oo--JS.