Re: [Haskell-cafe] 3 level hierarchy of Haskell objects

On Wed, 8 Aug 2012, Ertugrul Söylemez wrote:

Patrick Browne 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.