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

On 8/8/12 3:36 PM, Patrick Browne wrote:

On 08/08/12, *Ertugrul Söylemez * 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