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!