[Haskell-cafe] Re: Haskell.org GSoC

Achim Schneider barsoap at web.de
Fri Feb 20 08:42:28 EST 2009

"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

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.

More information about the Haskell-Cafe mailing list