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.