packages feed

dag (empty) → 0.0.1

raw patch · 6 files changed

+324/−0 lines, 6 filesdep +QuickCheckdep +basedep +constraintssetup-changed

Dependencies added: QuickCheck, base, constraints, hspec, quickcheck-instances

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Athan Clark++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Athan Clark nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ dag.cabal view
@@ -0,0 +1,83 @@+Name:                   dag+Version:                0.0.1+Author:                 Athan Clark <athan.clark@gmail.com>+Maintainer:             Athan Clark <athan.clark@gmail.com>+License:                BSD3+License-File:           LICENSE+Synopsis:               Basic type-safe directed acyclic graphs.+Description:+  This is a type-safe approach for a directed acyclic graph.+  .+  Edge construction is inductive, creating a "schema":+  .+  >  import Data.Graph.DAG.Edge+  >+  >  -- | Edges are statically defined:+  >  edges = ECons (Edge :: EdgeValue "foo" "bar") $+  >    ECons (Edge :: EdgeValue "bar" "baz") $+  >    ECons (Edge :: EdgeValue "foo" "baz")+  >    unique -- ENil, but for uniquely edged graphs+  .+  Which we use to populate nodes with values:+  .+  >  data Cool = AllRight+  >            | Radical+  >            | SuperDuper+  >+  >  graph = GCons "foo" AllRight $+  >    GCons "bar" Radical $+  >    GCons "baz" SuperDuper $+  >    GNil edges+  .+  It's an instance of `Functor`, but we haven't done much here - it will require+  a lot of reflection that I don't have time to implement right now - there isn't+  even binding of value-based `GCons` keys and `ECons` edge node labels.+  .+  Some type tomfoolery:+  .+  >  *Data.Graph.DAG> :t edges+  >  edges+  >    :: EdgeSchema+  >         '['EdgeType "foo" "bar", 'EdgeType "bar" "baz",+  >           'EdgeType "foo" "baz"] -- Type list of edges+  >         '['("foo", '["bar", "baz"]), '("bar", '["baz"])] -- potential loops+  >         'True -- uniqueness+  .+  >  *Data.Graph.DAG> :t getSpanningTrees $ edges+  >  getSpanningTrees $ edges+  >    :: Data.Proxy.Proxy+  >         '['Node "foo" '['Node "bar" '['Node "baz" '[]],+  >                         'Node "baz" '[]],+  >           'Node "bar" '['Node "baz" '[]],+  >           'Node "baz" '[]]+  .+  This library is still very naive, but it will give us compile-time enforcement+  of acyclicity (and uniqueness) in these graphs - ideal for dependency graphs.++Cabal-Version:          >= 1.20+Build-Type:             Simple++Library+  Default-Language:     Haskell2010+  HS-Source-Dirs:       src+  GHC-Options:          -Wall+  Exposed-Modules:      Data.Graph.DAG+                        Data.Graph.DAG.Edge+  Build-Depends:        base >= 4 && < 5+                      , constraints++Test-Suite spec+  Type:                 exitcode-stdio-1.0+  Default-Language:     Haskell2010+  Hs-Source-Dirs:       src+                      , test+  Ghc-Options:          -Wall+  Main-Is:              Spec.hs+  Build-Depends:        base+                      , hspec+                      , QuickCheck+                      , quickcheck-instances++Source-Repository head+  Type:                 git+  Location:             https://github.com/athanclark/dag
+ src/Data/Graph/DAG.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}++module Data.Graph.DAG+        ( module Data.Graph.DAG.Edge+        , DAG (..)+        , glookup+        ) where++import Data.Graph.DAG.Edge++data DAG es a where+  GNil :: EdgeSchema es x unique -> DAG es a+  GCons :: (String ~ key) =>+           key+        -> a -- value+        -> DAG es a+        -> DAG es a++instance Functor (DAG es) where+  fmap f (GNil e) = GNil e+  fmap f (GCons k x xs) = GCons k (f x) $+    fmap f xs+++glookup :: String -> DAG es a -> Maybe a+glookup _ (GNil _) = Nothing+glookup k (GCons k2 a gs) | k == k2   = Just a+                          | otherwise = glookup k gs
+ src/Data/Graph/DAG/Edge.hs view
@@ -0,0 +1,179 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Data.Graph.DAG.Edge where++import Data.Constraint+import GHC.TypeLits+import Data.Proxy++-- | 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 EdgeValue (from :: Symbol) (to :: Symbol) = Edge++-- | We need this for type-level computation list.+data EdgeKind = forall from to. EdgeType from to++-- | 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 Deducible (x :: Bool) :: Constraint where+  Deducible 'True = ()++-- | @not . elem@ for lists of types, resulting in a constraint.+type family Excluding (x :: k) (xs :: Maybe [k]) :: Constraint where+  Excluding a ('Just '[]) = Deducible 'True -- Basis+  Excluding a 'Nothing    = Deducible 'True -- Basis+  Excluding a ('Just (a ': ts)) = Deducible 'False -- Reject & Refute+  Excluding a ('Just (b ': ts)) = Excluding a ('Just ts) -- continue++-- | A simple @Data.List.lookup@ function for type maps.+type family Lookup (index :: k) ( map :: [(k, k2)] ) :: Maybe k2 where+  Lookup a ( '( a, v) ': xs ) = 'Just v+  Lookup a (b ': xs) = Lookup a xs+  Lookup a '[] = 'Nothing++-- | Trivial inequality for non-reflexivity of edges+type family (x :: k1) =/= (y :: k2) :: Constraint where+  a =/= a = Deducible 'False+  a =/= b = Deducible 'True++-- | 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.+class Acceptable (a :: EdgeKind)+                 ( oldLoops :: [(Symbol, [Symbol])] )+                 (unique :: Bool) where+instance ( Excluding from (Lookup to excludeMap)+         , from =/= to ) =>+            Acceptable ('EdgeType from to) excludeMap 'False where+instance ( Excluding from (Lookup to excludeMap)+         , Excluding to (Lookup from excludeMap)+         , from =/= to ) =>+            Acceptable ('EdgeType from to) excludeMap 'True where++-- | Add an explicit element to the head of a list, if the test is inside that+-- list.+type family PrependIfElem (test :: k) (a :: k) (xs :: [k]) :: [k] where+  PrependIfElem t a (t ': xs) = a ': t ': xs+  PrependIfElem t a (u ': xs) = u ': (PrependIfElem t a xs)+  PrependIfElem t a '[]       = '[]++-- | 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.+type family DisallowIn+              (new :: EdgeKind)+              ( oldLoops :: [(Symbol, [Symbol])] )+              (keyFound :: Bool) :: [(Symbol, [Symbol])] where+-- When @from ~ key@:+  DisallowIn ('EdgeType from to) ( '(from, xs) ': es) 'False =+    '(from, (to ': xs)) ':                      -- add @to@ to transitive reach list+      (DisallowIn ('EdgeType from to) es 'True) -- continue+-- When @from ~/~ key@, and @from ~/~ head value@+  DisallowIn ('EdgeType from to) ( '(key, vs) ': es ) keyFound =+    '(key, (PrependIfElem from to vs)) ':            -- find the needle if it exists+        (DisallowIn ('EdgeType from to) es keyFound) -- continue+-- Basis+  DisallowIn a '[] 'True = '[] -- search over.+-- Growth via append+  DisallowIn ('EdgeType from to) '[] 'False = ('(from, (to ': '[])) ': '[])++-- | @edges@ is a list of types with kind @EdgeKind@, while @nearLoops@ is a+-- map of the nodes transitively reachable by each node.+data EdgeSchema (edges :: [EdgeKind])+                (nearLoops :: [(Symbol, [Symbol])])+                (unique :: Bool) 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++-- | Utility for constructing an @EdgeSchema@ granularly+unique :: EdgeSchema '[] '[] 'True+unique = ENil++notUnique :: EdgeSchema '[] '[] 'False+notUnique = ENil++-- | Trivial rose tree for creating spanning trees+data Tree a = Node a [Tree a]++-- | Adds an empty @c@ tree to the list of trees uniquely+type family AppendIfNotElemTrees (c :: k) (trees :: [Tree k]) :: [Tree k] where+  AppendIfNotElemTrees c ((Node c xs) ': xss) = (Node c xs) ': xss+  AppendIfNotElemTrees c ((Node x xs) ': xss) = (Node x xs) ':+    (AppendIfNotElemTrees c xss)+  AppendIfNotElemTrees c '[] = (Node c '[]) ': '[]++-- | Adds @c@ as a child of any tree with a root @t@. Assumes unique roots.+type family AddChildTo (test :: k)+                       (child :: k)+                       (trees :: [Tree k]) :: [Tree k] where+  AddChildTo t c ((Node t xs) ': xss) =+    (Node t (AppendIfNotElemTrees c xs)) ': (AddChildTo t c xss)+  AddChildTo t c ((Node x xs) ': xss) =+    (Node x (AddChildTo t c xs)) ': (AddChildTo t c xss)+  AddChildTo t c '[] = '[]++-- | We need to track if @from@ has is a root node or not. TODO: Some code repeat.+type family AddEdge' (edge :: EdgeKind)+                     (trees :: [Tree Symbol])+                     (hasFromRoot :: Bool)+                     (hasToRoot :: Bool):: [Tree Symbol] where+  AddEdge' ('EdgeType from to) '[] 'False 'False =+    (Node from ((Node to '[]) ': '[])) ': (Node to '[]) ': '[]++  AddEdge' ('EdgeType from to) '[] 'True 'False =+    (Node to                     '[])  ':                  '[]++  AddEdge' ('EdgeType from to) '[] 'False 'True =+    (Node from ((Node to '[]) ': '[])) ':                  '[]++  AddEdge' x '[] 'True 'True = '[]++  AddEdge' ('EdgeType from to) ((Node from xs) ': xss) hasFromRoot hasToRoot =+    (Node from (AppendIfNotElemTrees to xs)) ':+      (AddEdge' ('EdgeType from to) xss 'True hasToRoot)++  AddEdge' ('EdgeType from to) ((Node to xs) ': xss) hasFromRoot hasToRoot =+    (Node to (AddEdge' ('EdgeType from to) xs 'True 'True)) ':+      (AddEdge' ('EdgeType from to) xss hasFromRoot 'True)++  -- Go downward, and laterally (I think).+  AddEdge' ('EdgeType from to) ((Node x xs) ': xss) hasFromRoot hasToRoot =+    (Node x (AddEdge' ('EdgeType from to) xs 'True 'True)) ':+      (AddEdge' ('EdgeType from to) xss hasFromRoot hasToRoot)++-- | Add @to@ as a child to every @from@ node in the accumulator.+type family AddEdge (edge :: EdgeKind)+                    (trees :: [Tree Symbol]) :: [Tree Symbol] where+  AddEdge a trees = AddEdge' a trees 'False 'False++-- | Auxilliary function normally defined in a @where@ clause for manual folding.+type family SpanningTrees' (edges :: [EdgeKind])+                           (acc :: [Tree Symbol]) :: [Tree Symbol] where+  SpanningTrees' '[] trees = trees+  SpanningTrees' (('EdgeType from to) ': es) trees =+    SpanningTrees' es (AddEdge ('EdgeType from to) trees)++-- | Expects edges to already be type-safe+type family SpanningTrees (edges :: [EdgeKind]) :: [Tree Symbol] where+  SpanningTrees edges = SpanningTrees' edges '[]++getSpanningTrees :: EdgeSchema es x unique -> Proxy (SpanningTrees es)+getSpanningTrees _ = Proxy
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}