Data.Graph.DAG.Edge

Documentation

data EdgeValue from to

We use promoted symbol values for the from and to type parameters. This is the user-level data type when declaring the list of edges.

Constructors

Edge

data EdgeKind

We need this for type-level computation list.

Constructors

forall from to . EdgeType from to

type family Deducible x :: Constraint

Some people just want to watch the world burn. Ideally, this shouldn't exist; poor error messages, and is very square peg - round hole.

Equations

Deducible True = ()

type family Excluding x xs :: Constraint

not . elem for lists of types, resulting in a constraint.

Equations

Excluding a (Just []) = Deducible True

Excluding a Nothing = Deducible True

Excluding a (Just (a : ts)) = Deducible False

Excluding a (Just (b : ts)) = Excluding a (Just ts)

type family Lookup index map :: Maybe k2

A simple Data.List.lookup function for type maps.

Equations

Lookup a (`(a, v)` : xs) = Just v

Lookup a (b : xs) = Lookup a xs

Lookup a [] = Nothing

type family x =/= y :: Constraint

Trivial inequality for non-reflexivity of edges

Equations

a =/= a = Deducible False

a =/= b = Deducible True

class Acceptable a oldLoops unique

Simply reject anything that's been reached in the other direction. We expect an explicit type signature when uniqueness is needed, otherwise we will wait until invocation to see if the edges are unique.

Instances

(Excluding Symbol from (Lookup [Symbol] Symbol to excludeMap), Excluding Symbol to (Lookup [Symbol] Symbol from excludeMap), (=/=) Symbol Symbol from to) => Acceptable (EdgeType Symbol Symbol from to) excludeMap True

(Excluding Symbol from (Lookup [Symbol] Symbol to excludeMap), (=/=) Symbol Symbol from to) => Acceptable (EdgeType Symbol Symbol from to) excludeMap False

type family PrependIfElem test a xs :: [k]

Add an explicit element to the head of a list, if the test is inside that list.

Equations

PrependIfElem t a (t : xs) = a : (t : xs)

PrependIfElem t a (u : xs) = u : PrependIfElem t a xs

PrependIfElem t a [] = []

type family DisallowIn new oldLoops keyFoundYet :: [(Symbol, [Symbol])]

Update the exclusion map with the new edge: the from key gets to added, likewise with keys that have from in it's value list. We need to track if the key exists yet.

Equations

DisallowIn (EdgeType from to) (`(from, xs)` : es) False = `(from, to : xs)` : DisallowIn (EdgeType from to) es True

DisallowIn (EdgeType from to) (`(key, vs)` : es) keyFoundYet = `(key, PrependIfElem from to vs)` : DisallowIn (EdgeType from to) es keyFoundYet

DisallowIn a [] True = []

DisallowIn (EdgeType from to) [] False = `(from, to : [])` : []

data EdgeSchema edges nearLoops unique where

edges is a list of types with kind EdgeKind, while nearLoops is a map of the nodes transitively reachable by each node.

Constructors

ENil :: EdgeSchema [] [] unique

ECons :: (Acceptable b oldLoops unique, EdgeValue from to ~ a, EdgeType from to ~ b, DisallowIn b oldLoops False ~ c) => !a -> !(EdgeSchema old oldLoops unique) -> EdgeSchema (b : old) c unique

unique :: EdgeSchema [] [] True

Utility for constructing an EdgeSchema incrementally without a type signature.

notUnique :: EdgeSchema [] [] False