[Haskell-cafe] Signature of a function
k.schupke at imperial.ac.uk
Thu Jan 13 07:15:30 EST 2005
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
Imagine for examle (and this can be done in Haskell with the HList
a static constraint requiring proof at compile time that a list was
to some criteria:
mysort :: (HList a, HOrderedList b) => a -> b
Now the definition of the constraint for orderedness is quite simple,
to understand (as as it plays no part in the final program efficiency is
issue) - we are now free to write a heap sort or whatever, knowing it
compile if it obeys the constraint.
Obviously the above only works when the input list is statically
We can easily insert run-time checks in code - but it would be much
have the compiler proove that the code obeys the criteria under all
In other words rather than saying for a specific list the result should
it should be ordered forall a.
More information about the Haskell-Cafe