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.