Am Freitag, 20. Februar 2009 09:42 schrieben Sie:
Hello,
but to specify that “this function turns a list into its sorted equivalent” would probably require to specify e.g. "sort" in terms of the type system and to write code that actually does the sorting. The first task is much like specifying what a sorted list is in first-order-logic (much like a Prolog program) and the second task is a regular functional program.
If this is correct, dependent types would become more useful if the first task could be done by the compiler - which is probably impossible in general.
I might not really understand you. Do you mean the compiler should be able to infer the specification from the implementation? In a dependently-typed programming language this would just mean type inference since specifications are types. However, type inference isn’t possible for dependent type systems. Personally, I think, it makes more sense to start with a specification (type) and then provide implementations. Systems like Agda and Epigram can actually use the reach information from the types to assist you in writing your implementation. Best wishes, Wolfgang