They said it couldn't be done! They said Haskell didn't have dependent types! Here's a way to mimic dependent types using existential types, illustrated by an implementation of modular arithmetic. To try it out, load modulus.hs and try something like Modulus> inModulus (mkModulus (1234567890123::Integer)) (^98765432198765) 2 1160454313058 to compute 2 to the 98765432198765'th power modulo 1234567890123. The key is the definitions at the top of TypeVal.hs:

class TypeVal a t | t -> a where -- typeToVal should ignore its argument. typeToVal :: t -> a

data Wrapper a = forall t . (TypeVal a t) => Wrapper t

class ValToType a where valToType :: a -> Wrapper a

`valToType' takes a value `x' and returns a (wrapped version of a) fake value in a new type; from the new type, `x' can be recovered by applying typeToVal. This code works under ghc. It uses existentially quantified data constructors, scoped type variables, and explicit universal quantification. Enjoy, Dylan Thurston