Tuesday, February 7, 2012

Logic Programming with GADTs and Classes.

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.