Merge pull request #777 from explorable-viz/maybeJoin

Drop `BoolAlg` and explicit dom/codom on `GaloisConnection`. Add `Category` instance.

src/Desug.purs

@@ -1,25 +1,24 @@
 module Desug where
 
-import Desugarable (desug, desugBwd)
 import Prelude
+
 import Control.Monad.Error.Class (class MonadError)
+import Desugarable (desug, desugBwd)
 import Effect.Exception (Error)
 import Expr (Expr)
-import GaloisConnection (GaloisConnection)
-import Lattice (Raw, class BoundedJoinSemilattice)
+import GaloisConnection (GaloisConnection(..))
+import Lattice (class BoundedJoinSemilattice, Raw)
 import SExpr (Expr) as S
 import Util (successful)
 
-type DesugGaloisConnection a = GaloisConnection (S.Expr a) (Expr a) ()
-
 desugGC
    :: forall a m
     . MonadError Error m
    => BoundedJoinSemilattice a
    => Raw S.Expr
-   -> m (DesugGaloisConnection a)
+   -> m (GaloisConnection (S.Expr a) (Expr a))
 desugGC s0 = do
    let
       fwd s = successful $ desug s
       bwd e = desugBwd e s0
-   pure { fwd, bwd }
+   pure $ GC { fwd, bwd }

src/Dict.purs

@@ -38,14 +38,15 @@ import Util (Endo, type (×), (×), assert, definitely, error)
 
 type Dict a = O.Object a
 
+-- `Apply` instance would be an orphan
 apply :: forall a b. Dict (a -> b) -> Dict a -> Dict b
-apply d ds = intersectionWith ($) d ds
+apply = intersectionWith ($) -- why not require dicts to have same shape?
 
 apply2 :: forall f a b. Apply f => Dict (f (a -> b)) -> Dict (f a) -> Dict (f b)
-apply2 d ds = apply ((<*>) <$> d) ds
+apply2 d = apply ((<*>) <$> d)
 
 lift2 :: forall f a b c. Apply f => (a -> b -> c) -> Dict (f a) -> Dict (f b) -> Dict (f c)
-lift2 f d1 d2 = apply2 ((f <$> _) <$> d1) d2
+lift2 f d1 = apply2 ((f <$> _) <$> d1)
 
 -- Unfortunately Foreign.Object doesn't define this; could implement using Foreign.Object.ST instead.
 foreign import intersectionWith :: forall a b c. (a -> b -> c) -> Dict a -> Dict b -> Dict c

src/EvalBwd.purs

@@ -1,8 +1,6 @@
 module EvalBwd where
 
 import Prelude hiding (absurd)
-
-import BoolAlg (BoolAlg, slicesγ, slices, prod)
 import Bindings (Var, varAnon)
 import Control.Monad.Except (class MonadError, runExcept)
 import Data.Exists (mkExists, runExists)
@@ -22,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
@@ -197,18 +195,15 @@ evalBwd' v (T.LetRec ρ t) =
    γ1' × ρ' × α' = closeDefsBwd γ2
 evalBwd' _ _ = error absurd
 
-type EvalGaloisConnection a = GaloisConnection (Env a × Expr a × a) (Val a)
-   ( dom :: BoolAlg (Env a × Expr a × a)
-   , codom :: BoolAlg (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 => BoolAlg a -> Raw Env -> Raw Expr -> m (EvalGaloisConnection a)
-traceGC 𝒶 γ e = do
+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 = slicesγ 𝒶 γ `prod` (slices 𝒶 e `prod` 𝒶)
-      codom = slices 𝒶 v
       bwd v' = evalBwd γ e v' t
       fwd (γ' × e' × α) = snd $ fromRight $ runExcept $ eval γ' e' α
-   pure { dom, codom, v, fwd, bwd }
+   pure $ { gc: GC { fwd, bwd }, v }