[Haskell-cafe] Re: exceptions vs. Either

[MR K P SCHUPKE]

>You should include the definitions of the classes before saying

HOrderedList l' just has to prove by induction that for any element
in the list, the next element is greater, so the class is simply:

class HOrderedList l
instance HNil
instance HCons a HNil
instance (HOrderedList (HCons b l),HLe a b) => HCons a (HCons b l)

which is the equivalent type level program to  

ordered :: [Int] -> Bool
ordered [] = True
ordered [a] = True
ordered (a:(b:l)) = if a<=b then ordered (b:l) else False
ordered _ = False

It is obvious by observation that the a<=b ensures order.
This is a lot simpler than say a heap-sort.       

I suppose you could contend that there are some classes above
I still haven't defined - but you wouldn't expect to see definitions
for (<=) which is defined in the prelude. Of course to show statically
that order is preserved the 'value' of the elements to be ordered must
be visible to the type system - so the values must be reified to types...
This can be done for any Haskell type, but for numbers we would
use Peano numbers - the HLe class for these is again easily defined
by induction:

class HLe n n' 
instance HLe HZero HZero
instance HLe x y => HLe (HSucc x) (HSucc y)


	Keean.