[Haskell-cafe] 3 level hierarchy of Haskell objects

[wren ng thornton]

On 8/8/12 3:36 PM, Patrick Browne wrote:
> On 08/08/12, *Ertugrul Söylemez *<es at ertes.de>  wrote:
>>  So you basically just mean
>>
>>      class (Functor f) =>  Applicative f
>
> Yes, but I want to know if there is a simple mathematical relation between the
> classes and/or  their types

Let us introduce the notion of "sorts". A sort is, essentially, a 
syntactic class for defining a (logical) language. Sorts cannot, in 
general, be discussed within the language being described; though the 
language may have some proxy for referring to them (e.g., the "Set", 
"Type", and "Prop" keywords in Coq). We will discuss three sorts: Type, 
Kind, and Context.

The sort Kind is a set of all the syntactic expressions denoting 
traditional kinds; i.e.,

     Kind = {*, *->*->*, (*->*)->*,...}

The sort Type is the set of all traditional types[1]; i.e.,

     Type = { t : k | k \in Kind }

A type class is a relation on Type. Notably, a type class instantiated 
with all its arguments is not itself a type! That is, "Functor f" does 
not belong to Type, it belongs to Context. Indeed, the only constructors 
of Context are (1) type classes, and (2) the "~" for type equality 
constraints.

The simplest relation is a unary relation, which is isomorphic to a set. 
Thus, if one were so inclined, one could think of "Functor" as being a 
set of types[2], namely a set of types of kind *->*. And each instance 
"Functor f" is a proof that "f" belongs to the set "Functor".

However, once you move outside of H98, the idea of type classes as sets 
of types breaks down. In particular, once you have multi-parameter type 
classes you must admit that type classes are actually relations on types.

The "=>" arrow in type signatures is an implication in the logic that 
Haskell corresponds to. In particular, it takes multiple antecedents of 
sort Context, a single consequent of sort S \in {Type, Context}, and 
produces an expression of sort S. This is different from the "->" arrow 
which is also implication, but which takes a single antecedent of sort 
Type (namely a type of kind *) and a single consequent of sort Type 
(namely a type of kind *), and produces an expression of sort Type 
(namely a type of kind *). And naturally the "->" on Type should be 
distinguished from the "->" on Kind: which takes a single antecedent of 
sort Kind, a single consequent of sort Kind, and produces an expression 
of sort Kind. Just as Kind exists to let us typecheck expressions in 
Type, we should also consider a sort ContextKind which exists to let us 
typecheck the expressions in Context. And, to handle the fact that type 
classes have arguments of different kinds, ContextKind must have it's 
own arrow, just as Kind does.


[1] Note that for this discussion, Type includes both proper types 
(i.e., types of kind *) as well as type constructors.

[2] This must not be confused with the sense in which kinds can be 
considered to be sets of types. These two different notions of "sets of 
types" belong to different sorts. A kind is a set of types which lives 
in Kind; a unary type-class constraint is a set of types which lives in 
Context.

-- 
Live well,
~wren