[Haskell-cafe] Re: Haskell.org GSoC

[Achim Schneider]

"Kemps-Benedix Torsten" <torsten.kemps-benedix at sks-ub.de> 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.