"Kemps-Benedix Torsten" <[email protected]> wrote:
> 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. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
