A colleague of mine recently needed to represent DAGs (directed acyclic graphs) in Coq, and asked around for ideas. Since Coq is not a nice language to program in, I decided to use Haskell instead. Something close to dependently typed programming is possible in Haskell thanks to GADTs. And other extensions will be helpful too,

```
{-# LANGUAGE GADTs, TypeOperators, Rank2Types #-}
```

My idea is to represent a DAG as a list of nodes.
Nodes have a list of children, where each child is a reference to an element *later* in the list.

For example, the DAG

would be represented as

[Node "a" [1,2,2,4], Node "b" [3,3], Node "c" [3,4], Node "d" [], Node "e" []]

To make the above representation safe, we need to ensure two things:

- Each child-reference is greater than the index of the parent.
- Each child-reference refers to an actual node, so it must be smaller than the size of the list.

The first condition is easily satisfied, by making the reference *relative to the current position* and using natural numbers. So the representation would be

[Node "a" [0,1,1,3], Node "b" [1,1], Node "c" [0,1], Node "d" [], Node "e" []]

For the second condition we need dependent types. In particular the type `Fin n` of numbers smaller than `n`.

data Zero data Succ n data Fin n where Fin0 :: Fin (Succ n) FinS :: Fin n -> Fin (Succ n)

A node then holds a label of type `a` and a list of numbers less than `n`.

data Node a n where Node :: a -> [Fin n] -> Node a n deriving (Eq,Show)

For the list of nodes we will use a dependently typed vector,

data Vec f n where Empty :: Vec f Zero (:::) :: f n -> Vec f n -> Vec f (Succ n) infixr 5 :::

A value of `Vec f n` is a list of the form `[]` or `[x _{0}::f 0]` or [x__1::f 1, x__0::f 0]

type DAG a = Vec (Node a)

I would like to define `Eq` and `Show` instances for these datatypes. But the instance for `Vec` would look something like

instance (forall m. Eq (f m)) => Eq (Vec f n)

which is not valid Haskell, even with extensions. The solution is to use another class, `Eq1`

class Eq1 f where eq1 :: f n -> f n -> Bool

Now we can define

instance Eq1 f => Eq (Vec f n) where Empty == Empty = True (x ::: xs) == (y ::: ys) = eq1 x y && xs == ys

The boring instances for `Node` and `Fin` are

instance Eq a => Eq1 (Node a) where eq1 = (==) instance Eq1 Fin where eq1 = (==) instance Eq1 f => Eq1 (Vec f) where eq1 = (==) -- ghc can't derive this instance Eq (Fin n) where Fin0 == Fin0 = True FinS i == FinS j = i == j _ == _ = False

The same goes for `Show`

class Show1 a where showsPrec1 :: Int -> a n -> ShowS -- instances ommitted, see source code

To show that these DAGs work, we can convert from a DAG to a tree by duplicating all nodes. The tree type is a simple rose tree, as those in Data.Tree:

data Tree a = TNode a [Tree a] deriving Show

To be able to make a dag into a tree, we need to know the root node. So we give the `toTree` a `DAG n` and an `Fin n` to indicate the root.

-- Convert a DAG to a tree, using the given node index as root toTree :: Fin n -> DAG a n -> Tree a toTree Fin0 (Node x cs ::: ns) = TNode x [toTree c ns | c <- cs] toTree (FinS i) (_ ::: ns) = toTree i ns -- drop the head until we reach the root

And for convenience, a function that assumes that the first node in the list is the root.

toTree' :: DAG a (Succ n) -> Tree a toTree' = toTree Fin0

Here is the example from above

example = Node "a" [Fin0,FinS Fin0,FinS Fin0,FinS (FinS (FinS (Fin0)))] ::: Node "b" [FinS Fin0,FinS Fin0] ::: Node "c" [Fin0,FinS Fin0] ::: Node "d" [] ::: Node "e" [] ::: Empty

λ> toTree' example TNode "a" [TNode "b" [TNode "d" [],TNode "d" []] ,TNode "c" [TNode "d" [],TNode "e" []] ,TNode "c" [TNode "d" [],TNode "e" []] ,TNode "e" []]

As an image:

.

More interesting is the conversion *from* a tree *to* a DAG, in such a way that we share identical nodes.
For that we first of all need to be able to search a DAG to see if it already contains a particular node.

Let's do this a bit more generic, and define a search over any `Vec f`.

findVec :: (Eq1 f, Pred1 f) => f n -> Vec f n -> Maybe (Fin n)

What is that `Pred1` class? And why do we need it? When you have a value of type `f n`, and you want to compare it to the elements of a vector, you will quickly discover that these elements have different types, `f m` with `m < n`. So, we need to either convert the `f n` to the `f m` or vice-versa.

I'll go with the former, because that means the search can stop early. If a node refers to a child `Fin0`, that means it points to the first node in the DAG. So there is no point in looking if it is duplicated anywhere in vector, because other nodes can't possibly refer to earlier ones.

What the `Pred1` class does is tell you: "if this item occurred one place later in the vector, what would it look like?". And if it can not occur in later places return `Nothing`:

class Pred1 f where pred1 :: f (Succ n) -> Maybe (f n) instance Pred1 Fin where pred1 Fin0 = Nothing pred1 (FinS i) = Just i instance Pred1 (Node a) where pred1 (Node x cs) = Node x `fmap` mapM pred1 cs

Now the search becomes relatively straight forward:

findVec x (y ::: ys) = case pred1 x of Just x' | eq1 x' y -> Just Fin0 | otherwise -> FinS `fmap` findVec x' ys Nothing -> Nothing findVec _ _ = Nothing

The nice thing about GADTs is that it becomes almost impossible to make mistakes, because the typechecker will complain if you do.

When converting a `Tree` to a `DAG`, we do not know beforehand how many nodes that DAG is going to have.
Therefore, we need to put the produced `DAG` into an existential box, that hides the parameter `n`.

That is fine for the end result, but it will not work when incrementally constructing a DAG. Suppose you wanted to add two nodes to a DAG. Adding the first node is fine, but then you need to ensure that the children of the second node are still there. In addition, the second node will need to be adjusted: all child references have to be incremented, to skip the first added node.

That adjusting is done with the the counterpart to `Pred1`, the `Succ1` class

class Succ1 f where succ1 :: f n -> f (Succ n) instance Succ1 Fin where succ1 = FinS instance Succ1 (Node a) where succ1 (Node x cs) = Node x (map FinS cs)

Our box will come with the ability to 'lift' any succable value into it:

data Box f n where Box :: (forall g. Succ1 g => g n -> g m) -> f m -> Box f n

You can think of `Box f n` as a value of `f m` where `m >= n`. This allows turning any `g n` into a `g m`, which can be combined with the value in the box.
Before we can see `Box` in action, we will first need some functors to store things:

-- product functor data (:*:) f g a = (:*:) { fst1 :: f a, snd1 :: g a } -- functor composition newtype (:.:) f g a = Comp { getComp :: f (g a) }

Now when adding a node we check if it is already in the DAG, and if so, return the index.
If the node is not yet in the DAG, then add it. By adding the node the DAG becomes 1 larger, from a `DAG n` we get a `DAG (Succ n)`. Therefore, we need one level of `succ`.

consNode :: Eq a => Node a n -> DAG a n -> Box (Fin :*: DAG a) n consNode n dag = case findVec n dag of Just i -> Box id (i :*: dag) Nothing -> Box succ1 (Fin0 :*: (n ::: dag))

Now the ugly part: converting an entire node.

fromTree :: Eq a => Tree a -> DAG a n -> Box (Fin :*: DAG a) n fromTree (TNode x cs) dag_{0}= case fromForest cs dag_{0}of Box to_{1}(Comp cs_{1}:*: dag_{1}) -> case consNode (Node x cs_{1}) dag_{1}of Box to_{2}ans -> Box (to_{2}. to_{1}) ans

And a forest, aka. a list of trees:

fromForest :: Eq a => [Tree a] -> DAG a n -> Box (([] :.: Fin) :*: DAG a) n fromForest [] dag = Box id $ Comp [] :*: dag fromForest (x:xs) dag_{0}= case fromForest xs dag_{0}of Box to_{1}(Comp xs_{1}:*: dag_{1}) -> case fromTree x dag_{1}of Box to_{2}(x_{2}:*: dag_{2}) -> Box (to_{2}. to_{1}) (Comp (x_{2}: map to_{2}xs_{1}) :*: dag_{2})

At the top level we start with an empty DAG, and ignore the index of the root (which will always be Fin0).

fromTree' :: Eq a => Tree a -> Box (DAG a) Zero fromTree' x = case fromTree x Empty of Box to_{1}(_ :*: dag_{1}) -> Box to_{1}dag_{1}

To understand these functions, you should ignore the `Box` constructors, what you are left with is

fromTree_{pseudo}(TNode x cs) dag = let (cs',dag') = fromForest_{pseudo}cs dag in constNode (Node x cs') dag fromForest_{pseudo}[] dag = dag fromForest_{pseudo}(x:xs) dag = let (ns,dag') = fromForest_{pseudo}xs (n,dag'') = fromTree_{pseudo}x dag' in (n:ns,dag'')

Here is a test that shows that we are able to recover the sharing that was removed by `toTree'`:

λ> fromTree' (toTree' example) Node "a" [0,1,1,3] ::: Node "b" [1,1] ::: Node "c" [0,1] ::: Node "d" [] ::: Node "e" [] ::: Empty λ> fromTree' (toTree' example) == Box (succ1 . succ1 . succ1 . succ1 . succ1) example True

All this wrapping and unwrapping of `Box` is really ugly. It should also remind you of something.
That something is a monad. And `Box` is indeed a monad, just not a normal Haskell one.
Instead it is (surprise, surprise) a 'Monad1':

class Monad1 m where return1 :: f a -> m f a (>>>=) :: m f a -> (forall b. f b -> m g b) -> m g a instance Monad1 Box where return1 = Box id Box l x >>>= f = case f x of Box l' y -> Box (l' . l) y

Combine this with two utility functions:

-- Lift a value y into a Box boxLift :: Succ1 g => Box f n -> g n -> Box (f :*: g) n boxLift (Box l x) y = Box l (x :*: l y)

-- Apply one level of succ before putting things into a Box boxSucc :: Box f (Succ n) -> Box f n boxSucc (Box l x) = Box (l . succ1) x

And one more `Succ1` instance:

instance (Functor f, Succ1 g) => Succ1 (f :.: g) where succ1 (Comp x) = Comp (fmap succ1 x)

Now we can write this slightly less ugly code

fromTree_{m}:: Eq a => Tree a -> DAG a n -> Box (Fin :*: DAG a) n fromTree_{m}(TNode x cs) dag_{0}= fromForest_{m}cs dag_{0}>>>= \(Comp cs_{1}:*: dag_{1}) -> consNode (Node x cs_{1}) dag_{1}fromForest_{m}:: Eq a => [Tree a] -> DAG a n -> Box (([] :.: Fin) :*: DAG a) n fromForest_{m}[] dag = return1 $ Comp [] :*: dag fromForest_{m}(x:xs) dag_{0}= fromForest_{m}xs dag_{0}>>>= \(xs_{1}:*: dag_{1}) -> fromTree_{m}x dag_{1}`boxLift` xs_{1}>>>= \(x_{2}:*: dag_{2}:*: Comp xs_{2}) -> return1 $ Comp (x_{2}: xs_{2}) :*: dag_{2}

This might be even nicer when we add in a state monad for the `DAG`, but I'll leave that for (maybe) another time.

If you don't like existential boxes, then here is another way to define the `Box` monad.

data Box' f n where Box0 :: f n -> Box' f n BoxS :: Box' f (Succ n) -> Box' f n instance Monad1 Box' where return1 = Box0 Box0 x >>>= y = y x BoxS x >>>= y = BoxS (x >>>= y) boxSucc' :: Box' f (Succ n) -> Box' f n boxSucc' = BoxS boxLift' :: Succ1 g => Box' f n -> g n -> Box' (f :*: g) n boxLift' (Box0 x) y = Box0 (x :*: y) boxLift' (BoxS x) y = BoxS (boxLift' x (succ1 y))

The two types are equivalent, as shown by

equiv_{1}:: Box' f n -> Box f n equiv_{1}(Box0 x) = return1 x equiv_{1}(BoxS x) = boxSucc (equiv_{1}x) equiv_{2}:: Box f n -> Box' f n equiv_{2}(Box l x) = runUnBox' (l (UnBox' id)) (Box0 x) newtype UnBox' f m n = UnBox' {runUnBox' :: Box' f n -> Box' f m} instance Succ1 (UnBox' r f) where succ1 f = UnBox' (runUnBox' f . BoxS)

## Comments

Nice article, from memory Agda's Data.Graph library does something similar for finite graphs. A slight error - in the second and third code blocks there are two "d" nodes, the second node should be "e".

Could you explain why Fin is numbers smaller than n?

I read that class, probably incorrectly as the axioms For Fin (succ n) is true If Fin n is true then Fin (succ n) is true. seems like all numbers bigger than n.

What am I missing?

You shouldn't read it as an implication. If you make the

ntype parameter explicit, you get:I see what you are saying, I admit that I am still missing your intuition. I don't see how you go from the type-definition to your verbal explanation.

Trying to clarify this more mechanically:

If I understand correctly, for type 'Fin n': Fin0 says: This is a data-constructor with as type 'Fin (Succ n)'. How does this ever terminate? FinS says: I am a function wrapping my own type and making a type 'Fin (Succ n)'.

Is this correct? How does that get to your intuition? How does 'Zero' ever enter the story?

Termination doesn't become an issue, because it is up to the user of the type what

nis inFin (Succ n). Just like a regular type, say[a]is not a problem. It can be instantiated to[Int], but also to[[[[Int]]]].Together the two constructors mean that a value of type

Fin mcan either beFin0, but only ifm ~ Succ n; or it can look likeFinS x, but only ifx :: Fin nandm ~ Succ n. If you have trouble understanding how this makesFin nthe type of numbers less than n, try to work out for yourself what the possible values ofFin (Succ (Succ Zero))are.It doesn't really, except in the sense that

Fin0can be of typeFin0 :: Succ ZeroorFin0 :: Succ (Succ Zero), etc. Unfortunately in Haskell there is no kind system to prevent you from writingFin0 :: Succ Banana.I fiddled about transposing this to use the new 'kind promotion' in ghc-7.4, so you just use `data Nat = Zero | Succ Nat` This excludes `Fin0 :: Fin (Succ Banana)` but permits `Fin0 :: Fin ('Succ 'Zero)` (using an apostrophe to mark the 'promotion' of constructors into the type system). It only took a few changes before everything compiled. I didn't get to the point of reasoning whether it would suggest a different approach to `fromTree` and `toTree` and so on.

Forgot to paste the link: http://hpaste.org/65615

End of last year I started implementing a graph unification algorithm with underlying Hamana-style typed search trees that can represent sharing and cycles. Added the mildly interesting feature that any non-pointer node represents a fresh {symbol, variable}. The code is here: http://code.google.com/p/omega/source/browse/mosaic/Unify.lhs

You can restrict it using Type Classes.

Jorge, you can do with with the kind system of ghc-7.4 as I show in my simple-minded paste, http://hpaste.org/65615 -- with the addition of

data Banana = BananaYes applicative. That was quite interesting, I didn't know about kind promotion. But I thought I'd present my solution in any case, since it relies on a much more well established extension.

Although I have to be honest and say that, as a first impression of kind polymorphism, it seems a bit confusing to see value constructors as types and types as kinds, on what is not supposed to be a language with dependent types. But I'll have to use it a bit before making up my mind.

## Reply