Modeling heterogenous graphs in Haskell

Question

How can I model what I will call "heterogenous graphs" in haskell, such that the type-correctness of the graph can be verified at compile time?

For this purpose, a heterogenous graph is a set of nodes, each with a certain type label, and a set of edges, each with a source type label and a destination type label.

We wish to statically ensure that, when an edge is added to a graph, the source type label of that edge matches the type label of the source node, and the destination type label of that edge matches the type label of the destination node. But we don't wish to do that in the trivial way (by forcing the entire graph to contain only nodes with one particular type label).

By "type", do you mean compile-time type? If so, they're going to need some sort of run-time residue. Maybe a GADT if the set of types is easy to enumerate, maybe using Typeable if the set of types is not easy to enumerate. — Carl
Would you be interested in a safe interface that uses unsafe features internally? What operations should your graph support? And are there any restrictions on the type of the nodes? — Joachim Breitner
@JoachimBreitner Yes, using unsafe features internally would be fine. Typeable or erasing phantom node/edge types would be preferred to something like unsafeCoerce, but if its neccessary and externally safe anything goes. Now that you ask, it might be sufficient operations to, once the graph is known to be correctly typed, convert it to a homogenous representation. Maybe a TH splice that checks a homogenous representation for correctness in this sense might fulfill all my needs, I will explore that path a bit. — Doug McClean
I think one could have an implementation that stores nodes of type Any, exposes an interface using tagged types, uses unsafeCoerce internally, and maybe a higher rank type (like runST) to make sure nodes of different graphs are not confused. But it would be helpful to see the your “dream interface” first. — Joachim Breitner

Jon Purdy Jon Purdy · Accepted Answer · 2018-04-28T09:32:01

I’m not sure how I would go about enforcing this at compile time—I think it requires that your graphs be completely static?—but it’s relatively straightforward to enforce at runtime using Typeable. Here’s a sketch of what that would look like. First, I’ll start with typed Node and Edge types:

data Node a = Node a
data Edge a b = Edge !Int !Int

Wrap them in existentials:

{-# LANGUAGE ExistentialQuantification #-}

import Data.Typeable

data SomeNode
  = forall a. (Typeable a)
  => SomeNode (Node a)

data SomeEdge
  = forall a b. (Typeable a, Typeable b)
  => SomeEdge (Edge a b)

Have a heterogeneous graph data type that uses the existentially quantified types:

import Data.IntMap (IntMap)

-- Not a great representation, but simple for illustration.
data Graph = Graph !(IntMap SomeNode) [SomeEdge]

And then operations that perform dynamic type checks:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import qualified Data.IntMap as IntMap

addNode
  :: forall a. (Typeable a)
  => Int -> a -> Graph -> Maybe Graph
addNode i x (Graph ns es) = case IntMap.lookup i ns of

  -- If a node already exists at a given index:
  Just (SomeNode (existing :: Node e)) -> case eqT @e @a of

    -- Type-preserving replacement is allowed, but…
    Just Refl -> Just $ Graph ns' es

    -- …*type-changing* replacement is *not* allowed,
    -- since it could invalidate existing edges.
    Nothing -> Nothing

  -- Insertion is of course allowed.
  Nothing -> Just $ Graph ns' es

  where
    ns' = IntMap.insert i (SomeNode (Node x)) ns

-- To add an edge:
addEdge
  :: forall a b. (Typeable a, Typeable b)
  => Edge a b -> Graph -> Maybe Graph
addEdge e@(Edge f t) (Graph ns es) = do

  -- The ‘from’ node must exist…
  SomeNode (fn :: Node tfn) <- IntMap.lookup f ns
  -- …and have the correct type; and
  Refl <- eqT @a @tfn

  -- The ‘to’ node must exist…
  SomeNode (tn :: Node ttn) <- IntMap.lookup t ns
  -- …and have the correct type.
  Refl <- eqT @b @ttn

  pure $ Graph ns $ SomeEdge e : es

Now this succeeds:

pure (Graph mempty mempty)
  >>= addNode 0 (1 :: Int)
  >>= addNode 1 ('x' :: Char)
  >>= addEdge (Edge 0 1 :: Edge Int Char)

But changing Int/Char in Edge Int Char to invalid types, or 0/1 to invalid indices, will fail and return Nothing.

Modeling heterogenous graphs in Haskell

1 Answers