[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