dag- Compile-time, type-safe directed acyclic graphs.

Safe HaskellNone




data EdgeValue from to Source

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.



data EdgeKind Source

We need this for type-level computation list.


forall from to . EdgeType from to 

type family Deducible x :: Constraint Source

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


Deducible True = () 

type family Excluding x xs :: Constraint Source

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


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 Source

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


Lookup a (`(a, v)` : xs) = Just v 
Lookup a (b : xs) = Lookup a xs 
Lookup a [] = Nothing 

type family x =/= y :: Constraint Source

Trivial inequality for non-reflexivity of edges


a =/= a = Deducible False 
a =/= b = Deducible True 

class Acceptable a oldLoops unique Source

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.


(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] Source

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


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])] Source

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.


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 Source

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


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 Source

Utility for constructing an EdgeSchema incrementally without a type signature.