diff --git a/dag.cabal b/dag.cabal --- a/dag.cabal +++ b/dag.cabal @@ -1,5 +1,5 @@ Name: dag -Version: 0.0.1 +Version: 0.0.2 Author: Athan Clark Maintainer: Athan Clark License: BSD3 @@ -8,48 +8,55 @@ Description: This is a type-safe approach for a directed acyclic graph. . - Edge construction is inductive, creating a "schema": + Edge construction is incremental, creating a "schema": . > import Data.Graph.DAG.Edge > > -- | Edges are statically defined: - > edges = ECons (Edge :: EdgeValue "foo" "bar") $ + > edges = + > ECons (Edge :: EdgeValue "foo" "bar") $ > ECons (Edge :: EdgeValue "bar" "baz") $ > ECons (Edge :: EdgeValue "foo" "baz") - > unique -- ENil, but for uniquely edged graphs + > unique -- ENil, but casted for uniquely edged graphs . - Which we use to populate nodes with values: + The nodes are separate from edges; graph may be not connected: . > data Cool = AllRight > | Radical > | SuperDuper > - > graph = GCons "foo" AllRight $ + > 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" '[]] + > + > *Data.Graph.DAG> reflect $ getSpanningTrees $ edges + > + > [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. @@ -63,8 +70,10 @@ GHC-Options: -Wall Exposed-Modules: Data.Graph.DAG Data.Graph.DAG.Edge + Data.Graph.DAG.Edge.Utils Build-Depends: base >= 4 && < 5 , constraints + , singletons Test-Suite spec Type: exitcode-stdio-1.0 diff --git a/src/Data/Graph/DAG.hs b/src/Data/Graph/DAG.hs --- a/src/Data/Graph/DAG.hs +++ b/src/Data/Graph/DAG.hs @@ -1,29 +1,47 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE ScopedTypeVariables #-} module Data.Graph.DAG ( module Data.Graph.DAG.Edge + , module Data.Graph.DAG.Edge.Utils , DAG (..) , glookup ) where import Data.Graph.DAG.Edge +import Data.Graph.DAG.Edge.Utils +import Data.List (lookup) + +-- | The graph may be not connected data DAG es a where - GNil :: EdgeSchema es x unique -> DAG es a - GCons :: (String ~ key) => - key + GNil :: forall es a x unique. EdgeSchema es x unique + -> DAG es a + GCons :: String -> a -- value -> DAG es a -> DAG es a - +{- +-- | Convenience function. +getEdgeSchema :: DAG es a -> EdgeSchema es x unique +getEdgeSchema (GNil e) = (e :: EdgeSchema es x unique) +getEdgeSchema (GCons _ _ gs) = getEdgeSchema gs +-} instance Functor (DAG es) where fmap f (GNil e) = GNil e fmap f (GCons k x xs) = GCons k (f x) $ fmap f xs - +-- | A simple @Data.Map.lookup@ duplicate. glookup :: String -> DAG es a -> Maybe a glookup _ (GNil _) = Nothing glookup k (GCons k2 a gs) | k == k2 = Just a | otherwise = glookup k gs + + +{- +gtree :: String -> DAG es a -> Maybe (Tree a) +gtree k g = lookup k $ force $ reflect $ getSpanningTrees $ getEdgeSchema g +-} diff --git a/src/Data/Graph/DAG/Edge.hs b/src/Data/Graph/DAG/Edge.hs --- a/src/Data/Graph/DAG/Edge.hs +++ b/src/Data/Graph/DAG/Edge.hs @@ -11,6 +11,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} module Data.Graph.DAG.Edge where @@ -100,7 +101,7 @@ , EdgeType from to ~ b , DisallowIn b oldLoops 'False ~ c ) => !a - -> EdgeSchema old oldLoops unique + -> !(EdgeSchema old oldLoops unique) -> EdgeSchema (b ': old) c unique -- | Utility for constructing an @EdgeSchema@ granularly @@ -109,71 +110,3 @@ 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 diff --git a/src/Data/Graph/DAG/Edge/Utils.hs b/src/Data/Graph/DAG/Edge/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Data/Graph/DAG/Edge/Utils.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Graph.DAG.Edge.Utils where + +import Data.Graph.DAG.Edge + +import GHC.TypeLits +import Data.Singletons.TH +import Data.Singletons.Prelude +import Data.Proxy + + +-- | Trivial rose tree for creating spanning trees +$(singletons [d| + data Tree a = Node a [Tree a] deriving (Show, Eq) + |]) + +-- | Gives us a generic way to get our spanning trees of the graph, as a value. +-- Credit goes to . +reflect :: + forall (a :: k). + (SingI a, SingKind ('KProxy :: KProxy k)) => + Proxy a -> Demote a +reflect _ = fromSing (sing :: Sing 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