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.

## No comments:

## Post a Comment

1. Do be civil.

2. Reasonable criticisms are welcome, but personal opinions are not.

3. These posts are not for evangelizing languages, but for contemplating interesting properties.