[Haskell-cafe] closed classes [was: Re: exceptions vs. Either]

[MR K P SCHUPKE]

>Is there any possibility of a theory that will avoid the need to replicate
>features at higher and higher levels?

If we consider types, types are a collection of values, for example we could
consider Int to be:

data Int = One | Two | Three | Four ...

Okay, so the values in an integer are connected by functions (operations
like plus, multiply) - but we can consider these externally defined (as they
are primitives). Also we have special symbols for the values of this type
(type constructors are 'values') like 1, 2, 3... etc.

Likewise Char is effectively an enumeration of ascii values (or Unicode
values). All these standard types behave like enumerations of values.

Lists are effectively nested binary products:

data List a = Cons a (List a)

But I digress, my point is that types are a 'set' of values, and so
we can consider the simplest example:

data Bool = True | False

So bool is a type and True and False are the values 'in' that type - _but_
we can also write:

kind Bool = True | False

Where Bool is a kind and True and False are values, Kinds are really a different
name for "type_of_types"... and this continues upwards forever (a 
type_of_type_of_types) ... we can effectively flatten this by considering
types as values and kinds as types. What is the difference between a type
and a value? 

So we can consider: "data Bool = True | False" to be a relationship between
elements at the Nth level (the RHS) and the N+1th level (the LHS). This
relationship could be applied at any level, and it should be possible to
detemine the level at which we wish to apply this relationship by the
context in which it is used.

Imagine a function 'not':

not :: Bool -> Bool
not True = False
not False = True

we could apply this at the values level:

> not True
False

The type level:

class (Bool a,Bool b) => Not a b
	| a -> b
instance True False
instance False True

How does this differ from the original functional form?
can we imagine doing:

not' :: Not a b => a -> b

but perhaps writing it:

not' :: Bool a => a -> not a

After all is not 'not'  a complete function from Bool to Bool, whatever Bool is?
(Bool could be a type or a type of types, or a type of type of types...)

Would this not result in greater code re-use? Perhaps classes would become redundant
(apart from being used to allow overloading...)

My theory here is a bit shakey - but the name Martin Lof springs to mind.

	Keean.

*errata - when I said "Where Bool is a kind and True and False are values" I of course
meant w
true and false are types!