On Mon, 2004-08-09 at 18:05, Graham Klyne wrote: [snip]
and have found myself wondering if type-level lambda abstraction wouldn't be a useful feature to overcome this.
Your suggestion seems to be another feature in the same vein: extending data features to types. I find myself wondering where this might all end. If types acquire many of the manipulations that are available for data values, then might one find that, in turn, cases will be found that seem to require similar capabilities for kinds?
Is there any possibility of a theory that will avoid the need to replicate features at higher and higher levels?
As people have bee discussing recently on this list, this is what dependent types gives you. Instead of having a hierarchy of values->types->kinds-> ... where each is classified by the one above it (values by types, types by kinds), dependent types allow you to have types that depend on values in your program. It does indeed allow you to manipulate types using the same manipulations that are available for ordinary data values. The trade off however is that the value system must be decidable (no bottom allowed) or otherwise the type system is undecidable. There are other ways of making the trade off that do allow you use general recursion when you really need to (as Conor posted recently), but then you loose the ability to prove certain things about your programs within the type checking framework and you would have to go back to external proofs. (Of course this is the situation in Haskell anyway, that these kinds of proofs have to be done externally to the program) Duncan