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

Duncan Coutts duncan.coutts at worcester.oxford.ac.uk
Mon Aug 9 18:46:59 EDT 2004


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



More information about the Haskell-Cafe mailing list