[Haskell] Dependent types, was:2-D Plots,
graphical representation of massive data
MR K P SCHUPKE
k.schupke at imperial.ac.uk
Tue Aug 31 07:59:18 EDT 2004
>I think you are confusing Dependent Types with Functional Dependencies.
Actually the two are not that dissimilar... If we allow types to depend
on types (which is what Functional Dependencies allow) IE:
class a b | a -> b
instance Int Float
instance Float Int
For example is really a function on the type level mapping a to b. All
that is missing is a way to make types depend on values... which can
be done with dictionary passing. Here is an example:
class ReifyBool t w where
reifyBool :: Prelude.Bool -> t -> w
instance (Apply t AllTrue w,Apply t AllFalse w) => ReifyBool t w where
reifyBool Prelude.True t = apply t AllTrue
reifyBool Prelude.False t = apply t AllFalse
The limitation here is that an 'instance' must exist for each possibility
in the program, so we are limited to a finite range of values... although
we can use type recursion in the class to make the code smaller, we still
must have some limit known at compile time, for example Int:
class (NotNegative m,NotPositive n) => ReifyNotPositive m t i n w where
reifyNotPositive :: Integral i => m -> t -> i -> n -> w
instance NotPositive n => ReifyNotPositive Zero t i n w where
reifyNotPositive _ _ _ _ = error "Number to be reified exceeds maximum range."
instance (NotPositive n,ReifyNotPositive m t i (Pre n) w,Ctrl.Apply t n w)
=> ReifyNotPositive (Suc m) t i n w where
reifyNotPositive (Suc m) t i n
| i<0 = reifyNotPositive m t (i+1) (Pre n)
| otherwise = Ctrl.apply t n
(I appologise if the code is a little verbose, but to avoid mistakes I have
cut and pasted from a working project - but you can see the important
features)...
So by combining reification to a type level representation and functional
dependancies we arrive at dependant types...
Keean./
More information about the Haskell
mailing list