[Haskell] Dependent Types in Haskell [was: Eliminating Array Bound Checking through Non-dependent] types

[MR K P SCHUPKE]

>This will only work for terminating programs!

Interesting point, but thats because all the operations are at
the type level - therefore if a type is unknown at compile time
we cannot produce a program. 

With this type class stuff values can depend on types, but
not the other way around. You can sort of do reification
(types depend on values) for limited finite cases where
it ends up getting implemented as dictionary passing.

an example of reification is:

class (NotNegative m,NotNegative n) => ReifyNotNegative m t i n w where
        reifyNotNegative :: Integral i => m -> t -> i -> n -> w
instance NotNegative n => ReifyNotNegative Zero t i n w where
        reifyNotNegative _ _ _ _ = error "Number to be reified exceeds maximum range."
instance (NotNegative n,ReifyNotNegative m t i (Suc n) w,Ctrl.Apply t n w)
        => ReifyNotNegative (Suc m) t i n w where
        reifyNotNegative (Suc m) t i n
                | i>0 = reifyNotNegative m t (i-1) (Suc n)
                | otherwise = Ctrl.apply t n

(The apply in the above is a 'prolog' like apply, where 't' is a unique
type used to identify the 'function' to apply)



Anyway in this way the whole types depending on values issue is
sidestepped.

	Keean.