During the last advanced Haskell class, we discussed how to encode natural numbers in Haskell's type system with GADTs, and use classes to sum two natural numbers together. This idea can be extended to lists of items of different types, where the type of the list is a list of types. Here is an example where foldr and append are implemented.
infixr 5 :+ data Nil data a :+ r data List a where Nil :: List Nil (:+) :: a -> List c -> List (a :+c) class Append a b c | a b -> c where append :: List a -> List b -> List c instance Append Nil a a where append Nil v = v instance (Append l1 l2 r) => Append (f :+ l1) l2 (f :+ r) where append (f :+ l1) l2 = f :+ (append l1 l2) class Foldr f b a c | f -> b c, a -> f where foldrList :: List f -> b -> List a -> c instance Foldr a v Nil v where foldrList _ v _ = v instance (Foldr r1 b r2 r) => Foldr ((a -> r -> c) :+ r1) b (a :+ r2) c where foldrList (f :+ r1) b (a :+ r2) = f a (foldrList r1 b r2)
While this code might type-check without functional dependencies, the functional dependencies act a bit like uniqueness mode declarations and make type inference possible in more cases. Here is a link to the code.
Edit: In retrospect, since multiparameter typeclasses act so much like logic programming, why is there no actual mode declaration for multiparameter typeclasses? Instead there are only functional dependencies, which don't quite capture every case you want. It would be nice to direct the compiler how to unify typeclasses better without having to restrict them so much.