Ensuring correctness of data

Question

I have been programming in Haskell for a few months now, and am really enjoying it. I feel that I have a decent grasp of monads, functors, purity, etc. Now that I have been using this nice type system so much the idea of it being possible to express something that is incorrect sounds horrible to me. Haskell allows you to sometimes solve this by moving properties of of data into the type system. For example using GADTs you can define a balanced tree that cannot be constructed in an unbalanced way:

https://stackoverflow.com/a/16251496/5725848

Because of this you guarantee any function you implement on the tree will produce a correct tree. But there are other situations where I do not see how one could constrain the data at the type level.

Here is the situation I am thinking about specifically. I would like to represent a graph where every edge points to a node that exists. So you could not for example define a edge that goes to node 5 if only nodes 1-4 exist. I know something like this for DAG style graphs but have not seen something like this for graphs with cycles. How would I go about expressing something like this?

Answer 1

It is common to represent (small) directed graphs as adjacency matrices. If you create an n*n matrix of Bools, you can represent exactly all graphs with n nodes. Of course you need a good matrix library to represent this (not [[Bool]], which can have invalid values), preferably something with type-level numbers encoding the size, so you can require them to be square.

A small example to illustrate this:

Matrix.hs:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Matrix (Matrix, fromLists, toLists, Proxy(..)) where

import GHC.TypeLits

-- Yeah, I just said "don't use [[Bool]]"
-- But the Matrix constructor is not exported, the only way
-- users of this API can construct matrices is by using the
-- fromLists function, which only accepts [[a]] when the size
-- matches the expected matrix.
-- It's a bad choice for memory-consumption, but keeps the
-- example simple.
data Matrix (n :: Nat) (m :: Nat) a = Matrix [[a]]
    deriving (Show)

-- We use these proxies so we can pass the type-level numbers
-- as arguments.
data Proxy (a :: k) = Proxy

fromLists :: (KnownNat n, KnownNat m)
          => Proxy n
          -> Proxy m
          -> [[a]]
          -> Maybe (Matrix n m a)
fromLists proxyN proxyM lists
    -- "Downgrade" the type-level numbers to value level integers
    -- and verify that the input is sound.
    | fromIntegral (length lists) == natVal proxyN
    , all (\list -> fromIntegral (length list) == natVal proxyM) lists
    = Just (Matrix lists)
fromLists _ _ _
    = Nothing

toLists :: Matrix n m a -> [[a]]
toLists (Matrix lists) = lists

Graph.hs:

{-# LANGUAGE DataKinds #-}

import Matrix
import GHC.TypeLits

-- Represents a graph with n vertices.
type Graph n = Matrix n n Bool

-- Turns a graph back into an adjacency list.
toEdgeList :: (KnownNat n) => Graph n -> [(Integer, [Integer])]
toEdgeList graph
    = let
        adjecency = toLists graph
      in zipWith (\i row -> (i, map fst $ filter snd $ zip [0..] row)) [0..] adjecency

main = do
    case fromLists (Proxy :: Proxy 4) (Proxy :: Proxy 4)
        [ [True,  False, False, True ]
        , [False, True,  False, False]
        , [False, False, False, False]
        , [True,  True,  True,  True ]
        ] of
        (Just graph) -> print (toEdgeList graph)

Result:

[(0,[0,3]),(1,[1]),(2,[]),(3,[0,1,2,3])]

This approach hasn't made invalid graphs unrepresentable, it has only made them unconstructable by hiding the Matrix constructor and only exposing fromLists as a "smart constructor". As long as all the functions exported from Matrix.hs maintain the invariants, this is safe.

---

When the graph is large but sparse and constructing the entire adjacency matrix in memory is impossible, then you can fall back to adjacency lists. We can use the same type-level tricks to create bounded natural numbers that could be used here:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
import GHC.TypeLits

data BoundedInteger (n :: Nat) = BoundedInteger Integer

instance Show (BoundedInteger n) where
    show (BoundedInteger i) = show i

data Proxy (n :: k) = Proxy

boundedFromInteger :: (KnownNat n) => Proxy n -> Integer -> Maybe (BoundedInteger n)
boundedFromInteger proxy n
    | 0 <= n
    , n <= natVal proxy
    = Just (BoundedInteger n)
boundedFromInteger _ _ = Nothing

Again, only the smart constructor boundedFromInteger is exported, not BoundedInteger. With this, we can define a graph as:

type Graph n = Map (BoundedInteger n) (Set (BoundedInteger n))