Define `Strength` and `Map` with records.

This improves interface searching, so we no longer have to thread
`str` and `functor` around manually.

One disadvantage is that defining strengths and functoriality is now
more verbose. As the plan is to derive these from the signature, this
is not a huge problem from a UX perspective.

1 files changed, 33 insertions, 26 deletions

diff --git a/src/SOAS.idr b/src/SOAS.idr
index 80c5f7f..cc1c8ad 100644
--- a/src/SOAS.idr
+++ b/src/SOAS.idr
@@ -176,15 +176,24 @@ lift ctx f v = liftPos ctx f v.pos
 (.SortedFunctor) : (type : Type) -> Type
 type.SortedFunctor = type.SortedFamily -> type.SortedFamily
 
-0
-Strength : (f : type.SortedFunctor) -> Type
-Strength f = {0 p,x : type.SortedFamily} -> (mon : type.PointedCoalgStruct p) =>
+record Strength (f : type.SortedFunctor) where
+  constructor MkStrength
+  strength :
+    (0 p,x : type.SortedFamily) ->
+    (mon : type.PointedCoalgStruct p) ->
+    (f (x ^ p)) -|> ((f x) ^ p)
+
+(.str) :
+  Strength f ->
+  {0 p,x : type.SortedFamily} ->
+  (mon : type.PointedCoalgStruct p) =>
   (f (x ^ p)) -|> ((f x) ^ p)
+strength.str {p,x,mon} = strength.strength p x mon
 
-0
-(.Map) : type.SortedFunctor -> Type
-signature.Map
-  = {0 a,b : type.SortedFamily} -> (a -|> b) ->
+record (.Map) (signature : type.SortedFunctor) where
+  constructor MkMap
+  map :
+    {0 a,b : type.SortedFamily} -> (a -|> b) ->
     signature a -|> signature b
 
 record (.MonoidStruct)
@@ -213,7 +222,7 @@ traverse : {0 p,a : type.SortedFamily} ->
       (phi : p -|> a) ->
       (chi : meta -|> (a ^ a)) -> signature.MetaAlg meta (a ^ p)
 traverse {p,a} alg phi chi = MkMetaAlg
-      { alg = \h,s => alg $ str h s
+      { alg = \h,s => alg $ str.str h s
       , var = \v,s => phi (s v)
       , mvar = \m,e,s => chi m (\v => e v s)
       }
@@ -263,15 +272,11 @@ data (.Term) : (signature : type.SortedFunctor) ->
          (str : Strength signature) =>
          (metalg : signature.MetaAlg x a) =>
          signature.Term x -|> a
-a.sem (Op args) = metalg.alg
-                 $ functoriality {b = a}
-                   (a.sem {signature,x,str,functoriality}) args
+a.sem (Op args) = metalg.alg $ functoriality.map a.sem args
 a.sem (Va x   ) = MetaAlg.var metalg x
 a.sem (Me  m env)
   = MetaAlg.mvar metalg m
-  $ mapSubst {a=signature.Term x, b = a}
-    (a.sem {signature,x,str,functoriality})
-    env
+  $ mapSubst {a=signature.Term x, b = a} a.sem env
 
 (.envSem) : (0 a : type.SortedFamily) ->
             {0 signature : type.SortedFunctor} ->
@@ -283,10 +288,7 @@ a.sem (Me  m env)
                              a.metaEnv mctx ctx
 
 a.envSem {mctx = [<]         } menv = ()
-a.envSem {mctx = mctx :< meta} (menv,v) =
-      ( a.envSem {signature,x,str,functoriality} menv
-      , a.sem {signature,x,str,functoriality} v
-      )
+a.envSem {mctx = mctx :< meta} (menv,v) = (a.envSem menv, a.sem v)
 
 (.TermAlg) :
   (0 signature : type.SortedFunctor) ->
@@ -338,17 +340,22 @@ data STLC : TypeSTLC .SortedFunctor  where
 
 %hint
 strSTLC : Strength STLC
-strSTLC               (App f x           ) theta
-  = App (f theta) (x theta)
-strSTLC {p, mon, ctx} (Lam str {ty1} body) theta
-  = Lam str $ body $ extend p (mon.var (%% str))
-  $ \v => mon.ren (theta v)
-                  (\u => ThereVar u) -- Bug: can't eta-reduce
+strSTLC = MkStrength
+  { strength = \p,x,mon => \case
+    (App f x) => \theta => App (f theta) (x theta)
+    (Lam str {ty1} body) => \theta =>
+        Lam str $ body $ extend p (mon.var (%% str))
+      $ \v => mon.ren (theta v)
+                      (\u => ThereVar u) -- Bug: can't eta-reduce
+  }
 
 %hint
 functorialitySTLC : STLC .Map
-functorialitySTLC h (App f x) = App (h f) (h x)
-functorialitySTLC h (Lam str body) = Lam str (h body)
+functorialitySTLC = MkMap
+  { map = \h => \case
+    (App f x) => App (h f) (h x)
+    (Lam str body) => Lam str (h body)
+  }
 
 Ex1 : STLC .Term Var (B -:> (B -:> B) -:> B) [<]
 Ex1 = Op $ Lam "x" $