"Kemps-Benedix Torsten"
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.
Am I right?
Have a look at http://www.cs.nott.ac.uk/~wss/Publications/ThePowerOfPi.pdf http://www.cs.nott.ac.uk/~txa/publ/pisigma.pdf http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ You probably want to give type signatures... as you want the compiler to help you to construct a valid proof of what you claimed in it. It isn't much help if the compiler just tells you "that code you gave, it denotes _|_", if you get my meaning. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.