Safe Haskell | None |
---|---|

Language | Haskell2010 |

- data EdgeValue from to = Edge
- data EdgeKind = forall from to . EdgeType from to
- type family Deducible x :: Constraint
- type family Excluding x xs :: Constraint
- type family Lookup index map :: Maybe k2
- type family x =/= y :: Constraint
- class Acceptable a oldLoops unique
- type family PrependIfElem test a xs :: [k]
- type family DisallowIn new oldLoops keyFoundYet :: [(Symbol, [Symbol])]
- data EdgeSchema edges nearLoops unique where
- 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
- notUnique :: EdgeSchema [] [] False

# Documentation

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.

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.

type family Excluding x xs :: Constraint Source

`not . elem`

for lists of types, resulting in a constraint.

type family x =/= y :: Constraint Source

Trivial inequality for non-reflexivity of edges

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.

notUnique :: EdgeSchema [] [] False Source