[Haskell-cafe] Signature of a function

[Keean Schupke]

Conor McBride wrote:

> Types can be seen as a highly expressive and compact language of
> design statements for both humans and machines to read: this design
> statement determines the space of essential choices for the programmer,
> and programming can, if we choose, consist of navigating that space.
> Machines can map that space out for us, and they can fill in all the
> no-choice bits and pieces once we decide which way to go.

For me this is the most important aspect. As programs become more complex,
and as optimisation techniques are applied (or algorithms changed), Types
can act as 'contracts'. Infact I would like to see type expressiveness 
expanded...

Imagine for examle (and this can be done in Haskell with the HList 
library) adding
a static constraint requiring proof at compile time that a list was 
ordered (according
to some criteria:

    mysort :: (HList a, HOrderedList b) => a -> b
 
Now the definition of the constraint for orderedness is quite simple, 
and easy
to understand (as as it plays no part in the final program efficiency is 
not an
issue) - we are now free to write a heap sort or whatever, knowing it 
will only
compile if it obeys the constraint.

Obviously the above only works when the input list is statically 
determined at
compile time...

We can easily insert run-time checks in code - but it would be much 
better to
have the compiler proove that the code obeys the criteria under all 
circumstances.

In other words rather than saying for a specific list the result should 
be ordered,
it should be ordered forall a.

    Keean.