wren ng thornton wren at freegeek.org
Thu Aug 9 01:11:08 CEST 2012

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

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