[Haskell] Dependent Types in Haskell [was: Eliminating Array
Bound Checking through Non-dependent] types
MR K P SCHUPKE
k.schupke at imperial.ac.uk
Wed Aug 11 05:09:34 EDT 2004
>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
More information about the Haskell