🧩 [consolidate]: Category instance for GC.

src/Desug.purs

@@ -6,8 +6,8 @@ import Control.Monad.Error.Class (class MonadError)
 import Desugarable (desug, desugBwd)
 import Effect.Exception (Error)
 import Expr (Expr)
-import GaloisConnection (GaloisConnection)
-import Lattice (class BoundedJoinSemilattice, Raw, botOf)
+import GaloisConnection (GaloisConnection(..))
+import Lattice (class BoundedJoinSemilattice, Raw)
 import SExpr (Expr) as S
 import Util (successful)
 
@@ -19,8 +19,6 @@ desugGC
    -> m (GaloisConnection (S.Expr a) (Expr a))
 desugGC s0 = do
    let
-      dom = botOf s0
-      codom = botOf $ successful $ desug s0
       fwd s = successful $ desug s
       bwd e = desugBwd e s0
-   pure { dom, codom, fwd, bwd }
+   pure $ GC { fwd, bwd }

src/EvalBwd.purs

@@ -20,7 +20,7 @@ import Dict (fromFoldable, singleton, toUnfoldable) as D
 import Effect.Exception (Error)
 import Eval (eval)
 import Expr (Cont(..), Elim(..), Expr(..), RecDefs, VarDef(..), bv)
-import GaloisConnection (GaloisConnection)
+import GaloisConnection (GaloisConnection(..))
 import Lattice (Raw, bot, botOf, expand, (∨))
 import Partial.Unsafe (unsafePartial)
 import Trace (AppTrace(..), Trace(..), VarDef(..)) as T
@@ -195,12 +195,15 @@ evalBwd' v (T.LetRec ρ t) =
    γ1' × ρ' × α' = closeDefsBwd γ2
 evalBwd' _ _ = error absurd
 
-traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (GaloisConnection (Env a × Expr a × a) (Val a))
+type TracedEval a =
+   { gc :: GaloisConnection (Env a × Expr a × a) (Val a)
+   , v :: Raw Val
+   }
+
+traceGC :: forall a m. MonadError Error m => Ann a => Raw Env -> Raw Expr -> m (TracedEval a)
 traceGC γ e = do
    t × v <- eval γ e bot
    let
-      dom = (botOf <$> γ) × botOf e × bot
-      codom = botOf v
       bwd v' = evalBwd γ e v' t
       fwd (γ' × e' × α) = snd $ fromRight $ runExcept $ eval γ' e' α
-   pure { dom, codom, fwd, bwd }
+   pure $ { gc: GC { fwd, bwd }, v }

src/EvalGraph.purs

@@ -23,7 +23,7 @@ import DataType (checkArity, arity, consistentWith, dataTypeFor, showCtr)
 import Dict (disjointUnion, fromFoldable, empty, get, keys, lookup, singleton) as D
 import Effect.Exception (Error)
 import Expr (Cont(..), Elim(..), Expr(..), VarDef(..), RecDefs, Module(..), fv, asExpr)
-import GaloisConnection (GaloisConnection)
+import GaloisConnection (GaloisConnection(..))
 import Graph (class Graph, Vertex, sinks)
 import Graph (vertices) as G
 import Graph.GraphWriter (class MonadGraphAlloc, alloc, new, runWithGraphAllocT)
@@ -173,13 +173,21 @@ eval_module γ = go D.empty
       γ'' <- closeDefs (γ <+> γ') ρ αs
       go (γ' <+> γ'') (Module ds) αs
 
+type GraphEval g =
+   { gc :: GaloisConnection (Set Vertex) (Set Vertex)
+   , γα :: Env Vertex
+   , eα :: Expr Vertex
+   , g :: g
+   , vα :: Val Vertex
+   }
+
 graphGC
    :: forall g m
     . MonadError Error m
    => Graph g
    => GraphConfig g
    -> Raw Expr
-   -> m (GaloisConnection (Set Vertex) (Set Vertex) × Expr Vertex × g × Val Vertex)
+   -> m (GraphEval g)
 graphGC { g, n, γα } e = do
    (g' × _) × eα × vα <- do
       runWithGraphAllocT (g × n) $ do
@@ -188,8 +196,6 @@ graphGC { g, n, γα } e = do
          pure (eα × vα)
    let
       -- TODO: want (vertices eα `union` foldMap vertices γα) rather than sinks g' here?
-      dom = sinks g'
-      codom = vertices vα
-      fwd αs = G.vertices (fwdSlice αs g') `intersection` codom
-      bwd αs = G.vertices (bwdSlice αs g') `intersection` dom
-   pure $ { dom, codom, fwd, bwd } × eα × g' × vα
+      fwd αs = G.vertices (fwdSlice αs g') `intersection` vertices vα
+      bwd αs = G.vertices (bwdSlice αs g') `intersection` sinks g'
+   pure { gc: GC { fwd, bwd }, γα, eα, g: g', vα }

src/GaloisConnection.purs

@@ -1,25 +1,25 @@
 module GaloisConnection where
 
 import Prelude
-import Data.Function (identity) as F
+
+import Data.Newtype (class Newtype)
 import Lattice (class BooleanLattice, neg)
 import Util (Endo)
 
--- a and b are posets, but we don't enforce that here. Use record rather than type class so we can extend with
--- explicit value-level representation of domain/codomain.
-type GaloisConnection a b =
-   { dom :: a
-   , codom :: b
-   , fwd :: a -> b
-   , bwd :: b -> a
-   }
+newtype GaloisConnection a b = GC { fwd :: a -> b, bwd :: b -> a }
+
+derive instance Newtype (GaloisConnection a b) _
 
 deMorgan :: forall a b. BooleanLattice a => BooleanLattice b => Endo (a -> b)
 deMorgan = (neg >>> _) >>> (_ >>> neg)
 
 -- Could unify deMorgan and dual but would need to reify notion of opposite category.
 dual :: forall a b. BooleanLattice a => BooleanLattice b => GaloisConnection a b -> GaloisConnection b a
-dual gc = gc { dom = gc.codom, codom = gc.dom, fwd = deMorgan gc.bwd, bwd = deMorgan gc.fwd }
+dual (GC { fwd, bwd }) = GC { fwd: deMorgan bwd, bwd: deMorgan fwd }
+
+instance Semigroupoid GaloisConnection where
+   compose (GC { fwd: fwd1, bwd: bwd1 }) (GC { fwd: fwd2, bwd: bwd2 }) =
+      GC { fwd: fwd1 <<< fwd2, bwd: bwd1 >>> bwd2 }
 
-identity :: forall a. a -> GaloisConnection a a
-identity a = { dom: a, codom: a, fwd: F.identity, bwd: F.identity }
+instance Category GaloisConnection where
+   identity = GC { fwd: identity, bwd: identity }

test/Util.purs

@@ -22,10 +22,12 @@ import Effect.Class.Console (log)
 import Effect.Exception (Error)
 import EvalBwd (traceGC)
 import EvalGraph (GraphConfig, graphGC)
-import Graph (sinks, vertices)
+import Graph (sinks)
+import Graph (vertices) as G
 import Graph.GraphImpl (GraphImpl)
 import Graph.Slice (bwdSliceDual, fwdSliceDual, fwdSliceDeMorgan) as G
-import Graph.Slice (selectαs, select𝔹s)
+import Graph.Slice (selectαs, select𝔹s, vertices)
+import GaloisConnection (GaloisConnection(..))
 import Heterogeneous.Mapping (hmap)
 import Lattice (Raw, botOf, erase)
 import Module (parse)
@@ -66,18 +68,18 @@ testParse s = do
 testTrace :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff TraceRow
 testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
    -- | Desugaring Galois connections for Unit and Boolean type selections
-   desug <- desugGC s
-   desug𝔹 <- desugGC s
+   GC desug <- desugGC s
+   GC desug𝔹 <- desugGC s
 
    -- | Eval
    let e = desug.fwd s
    t_eval1 <- preciseTime
-   eval <- traceGC (erase <$> γα) e
+   { gc: GC eval, v } <- traceGC (erase <$> γα) e
    t_eval2 <- preciseTime
 
    -- | Backward
    t_bwd1 <- preciseTime
-   let γ𝔹 × e𝔹 × _ = eval.bwd (δv (botOf eval.codom))
+   let γ𝔹 × e𝔹 × _ = eval.bwd (δv (botOf v))
    t_bwd2 <- preciseTime
    let s𝔹 = desug𝔹.bwd e𝔹
 
@@ -88,37 +90,37 @@ testTrace s { γα } { δv, bwd_expect, fwd_expect } = do
    t_fwd2 <- preciseTime
 
    lift do
-      unless (isGraphical eval.codom) $
+      unless (isGraphical v) $
          log (prettyP v𝔹)
       -- | Check backward selections
       unless (null bwd_expect) $
          checkPretty "Trace-based source selection" bwd_expect s𝔹
       -- | Check round-trip selections
-      unless (isGraphical eval.codom) $
+      unless (isGraphical v) $
          checkPretty "Trace-based value" fwd_expect v𝔹
 
    pure { tEval: tdiff t_eval1 t_eval2, tBwd: tdiff t_bwd1 t_bwd2, tFwd: tdiff t_fwd1 t_fwd2 }
 
 testGraph :: Raw SE.Expr -> GraphConfig GraphImpl -> TestConfig -> MayFailT Aff GraphRow
 testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Desugaring Galois connections for Unit and Boolean type selections
-   gc_desug <- desugGC s
-   gc_desug𝔹 <- desugGC s
+   GC desug <- desugGC s
+   GC desug𝔹 <- desugGC s
 
    -- | Eval
-   let e = gc_desug.fwd s
+   let e = desug.fwd s
    t_eval1 <- preciseTime
-   gc × eα × g × vα <- graphGC gconfig e
+   { gc: GC eval, eα, g, vα } <- graphGC gconfig e
    t_eval2 <- preciseTime
 
    -- | Backward
    t_bwd1 <- preciseTime
    let
       αs_out = selectαs (δv (botOf vα)) vα
-      αs_in = gc.bwd αs_out
+      αs_in = eval.bwd αs_out
       e𝔹 = select𝔹s eα αs_in
    t_bwd2 <- preciseTime
-   let s𝔹 = gc_desug𝔹.bwd e𝔹
+   let s𝔹 = desug𝔹.bwd e𝔹
 
    -- | De Morgan dual of backward
    t_bwdDual1 <- preciseTime
@@ -132,28 +134,28 @@ testGraph s gconfig { δv, bwd_expect, fwd_expect } = do
    -- | Backward (all outputs selected)
    t_bwdAll1 <- preciseTime
    let
-      e𝔹_all = select𝔹s eα $ gc.bwd $ gc.codom
+      e𝔹_all = select𝔹s eα $ eval.bwd (vertices vα)
    t_bwdAll2 <- preciseTime
 
    -- | Forward (round-tripping)
    t_fwd1 <- preciseTime
    let
-      αs_out' = gc.fwd αs_in
+      αs_out' = eval.fwd αs_in
       v𝔹 = select𝔹s vα αs_out'
    t_fwd2 <- preciseTime
 
    -- | De Morgan dual of forward
    t_fwdDual1 <- preciseTime
    let
       gfwd_dual = G.fwdSliceDual αs_in g
-      v𝔹_dual = select𝔹s vα (vertices gfwd_dual)
+      v𝔹_dual = select𝔹s vα (G.vertices gfwd_dual)
    t_fwdDual2 <- preciseTime
 
    -- | Forward (round-tripping) using De Morgan dual
    t_fwdAsDeMorgan1 <- preciseTime
    let
       gfwd_demorgan = G.fwdSliceDeMorgan αs_in g
-      v𝔹_demorgan = select𝔹s vα (vertices gfwd_demorgan) <#> not
+      v𝔹_demorgan = select𝔹s vα (G.vertices gfwd_demorgan) <#> not
    t_fwdAsDeMorgan2 <- preciseTime
 
    lift do