Split monolithic file into modules.

Prove metatheory for generic initial algebras, instead of a clunky
concrete one.

7 files changed, 353 insertions, 0 deletions

diff --git a/src/SOAS/Algebra.idr b/src/SOAS/Algebra.idr
new file mode 100644
index 0000000..7dff735
--- /dev/null
+++ b/src/SOAS/Algebra.idr
@@ -0,0 +1,40 @@
+module SOAS.Algebra
+
+import SOAS.Context
+import SOAS.Family
+import SOAS.Strength
+import SOAS.Structure
+import SOAS.Var
+
+public export
+record (.MonoidStruct)
+         (signature : type.SortedFunctor)
+         (x : type.SortedFamily) where
+  constructor MkSignatureMonoid
+  mon : type.MonStruct x
+  alg : signature x -|> x
+
+public export
+record (.MetaAlg)
+         (signature : type.SortedFunctor)
+         (meta : type.SortedFamily)
+         (a : type.SortedFamily) where
+  constructor MkMetaAlg
+  alg : signature a -|> a
+  var : Var -|> a
+  mvar : meta -|> (a ^ a)
+
+export
+traverse : {0 p,a : type.SortedFamily} ->
+      {0 signature : type.SortedFunctor} ->
+      (functoriality : signature.Map) =>
+      (str : Strength signature) =>
+      (coalg : type.PointedCoalgStruct p) =>
+      (alg : signature a -|> a) ->
+      (phi : p -|> a) ->
+      (chi : meta -|> (a ^ a)) -> signature.MetaAlg meta (a ^ p)
+traverse {p,a} alg phi chi = MkMetaAlg
+      { alg = \h,s => alg $ str.str h s
+      , var = \v,s => phi (s v)
+      , mvar = \m,e,s => chi m (\v => e v s)
+      }
diff --git a/src/SOAS/Context.idr b/src/SOAS/Context.idr
new file mode 100644
index 0000000..25d2308
--- /dev/null
+++ b/src/SOAS/Context.idr
@@ -0,0 +1,24 @@
+module SOAS.Context
+
+infixr 4 :-
+
+public export
+record (.extension) (type : Type) where
+  constructor (:-)
+  0 name : String
+  ofType : type
+
+public export
+data (.Ctx) : (type : Type) -> Type where
+  Lin : type.Ctx
+  (:<) : (ctx : type.Ctx) -> (namety : type.extension) -> type.Ctx
+
+public export
+data (.Erased) : type.Ctx -> Type where
+  Z : [<].Erased
+  S : ctx.Erased -> (ctx :< x).Erased
+
+public export
+(++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
+ctx1 ++ [<] = ctx1
+ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
diff --git a/src/SOAS/Family.idr b/src/SOAS/Family.idr
new file mode 100644
index 0000000..cd3ae58
--- /dev/null
+++ b/src/SOAS/Family.idr
@@ -0,0 +1,43 @@
+module SOAS.Family
+
+import SOAS.Context
+
+infixr 3 -|> , -||> , -<>, =||> , =|> , >>> , ^
+infixl 3 <<<
+
+public export
+(.Family), ( .SortedFamily) : Type -> Type
+type.Family = type.Ctx -> Type
+type.SortedFamily = type -> type.Family
+
+public export 0
+(-||>) : {type : Type} -> (src,tgt : type.Family) -> Type
+(src -||> tgt) = {0 ctx : type.Ctx} -> src ctx -> tgt ctx
+
+public export 0
+(-|>) : {type : Type} -> (src,tgt : type.SortedFamily) -> Type
+(src -|> tgt) = {0 ty : type} -> src ty -||> tgt ty
+
+public export
+(<<<) : type.SortedFamily -> type.Ctx -> type.SortedFamily
+(f <<< ctx0) ty ctx = f ty (ctx ++ ctx0)
+
+public export
+(>>>) : type.SortedFamily -> type.Ctx -> type.SortedFamily
+(f >>> ctx0) ty ctx = f ty (ctx0 ++ ctx)
+
+public export 0
+(-<>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
+(src -<> tgt) ty ctx = src ty -||> (tgt >>> ctx) ty
+
+public export
+(=||>) : (src, tgt : type.Family) -> type.Family
+(src =||> tgt) ctx = src ctx -> tgt ctx
+
+public export
+(=|>) : (src, tgt : type.SortedFamily) -> type.SortedFamily
+(src =|> tgt) ty = src ty =||> tgt ty
+
+public export 0
+(.gensubst) : (type : Type) -> (from,to : type.SortedFamily) -> (src,tgt : type.Ctx) -> Type
+type.gensubst from to src tgt = {0 ty : type} -> from ty src -> to ty tgt
diff --git a/src/SOAS/Strength.idr b/src/SOAS/Strength.idr
new file mode 100644
index 0000000..f902ad4
--- /dev/null
+++ b/src/SOAS/Strength.idr
@@ -0,0 +1,33 @@
+module SOAS.Strength
+
+import SOAS.Family
+import SOAS.Structure
+import SOAS.Var
+
+public export
+0
+(.SortedFunctor) : (type : Type) -> Type
+type.SortedFunctor = type.SortedFamily -> type.SortedFamily
+
+public export
+record Strength (f : type.SortedFunctor) where
+  constructor MkStrength
+  strength :
+    (0 p,x : type.SortedFamily) ->
+    (mon : type.PointedCoalgStruct p) ->
+    (f (x ^ p)) -|> ((f x) ^ p)
+
+export
+(.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
+
+public export
+record (.Map) (signature : type.SortedFunctor) where
+  constructor MkMap
+  map :
+    {0 a,b : type.SortedFamily} -> (a -|> b) ->
+    signature a -|> signature b
diff --git a/src/SOAS/Structure.idr b/src/SOAS/Structure.idr
new file mode 100644
index 0000000..854725f
--- /dev/null
+++ b/src/SOAS/Structure.idr
@@ -0,0 +1,54 @@
+module SOAS.Structure
+
+import SOAS.Context
+import SOAS.Family
+import SOAS.Var
+
+-- Pointed Coalgebra
+
+public export
+record (.PointedCoalgStruct) type (x : type.SortedFamily) where
+  constructor MkPointedCoalgStruct
+  ren : x -|> [] x
+  var : Var -|> x
+
+%hint
+(.VarPointedCoalgStruct) : (0 type : Type) -> type.PointedCoalgStruct Var
+type.VarPointedCoalgStruct = MkPointedCoalgStruct
+  { ren = \i, f => f i
+  , var = id
+  }
+
+liftPos :
+  (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) =>
+  (p.subst ctx1 ctx2) -> p.substNamed (ctx1 ++ ctx) (ctx2 ++ ctx)
+liftPos Z     f x = f x.toVar
+liftPos (S l) f Here        = mon.var (Here .toVar)
+liftPos (S l) f (There pos) = mon.ren (liftPos l f pos) ThereVar
+
+export
+lift :
+  (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) =>
+  (p.subst ctx1 ctx2) -> p.subst (ctx1 ++ ctx) (ctx2 ++ ctx)
+lift ctx f v = liftPos ctx f v.pos
+
+-- Substitution Monoid
+
+public export
+record (.MonStruct) (type : Type) (m : type.SortedFamily) where
+  constructor MkSubstMonoidStruct
+  var : Var -|> m
+  mult : m -|> (m ^ m)
+
+export
+(.sub) :
+  (mon : type.MonStruct m) ->
+  m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
+mon.sub t s = mon.mult t (extend m s mon.var)
+
+export
+(.sub2) :
+  (mon : type.MonStruct m) ->
+  m sy (ctx :< (x :- ty1) :< (x :- ty2)) ->
+  m ty1 ctx ->  m ty2 ctx -> m sy ctx
+mon.sub2 t s1 s2 = mon.mult t (extend m s2 (extend m s1 mon.var))
diff --git a/src/SOAS/Theory.idr b/src/SOAS/Theory.idr
new file mode 100644
index 0000000..f36e7a1
--- /dev/null
+++ b/src/SOAS/Theory.idr
@@ -0,0 +1,58 @@
+module SOAS.Theory
+
+import SOAS.Algebra
+import SOAS.Context
+import SOAS.Family
+import SOAS.Strength
+import SOAS.Structure
+import SOAS.Var
+
+public export
+record (.Initial)
+         (signature : type.SortedFunctor)
+         (meta : type.SortedFamily)
+         (a : type.SortedFamily) where
+  constructor MkInitial
+  metalg : signature.MetaAlg meta a
+  bang :
+    (0 b : type.SortedFamily) ->
+    (metalg : signature.MetaAlg meta b) ->
+    a -|> b
+
+public export
+(.sem) :
+  signature .Initial meta a ->
+  (0 b : type.SortedFamily) -> (metalg : signature.MetaAlg meta b) =>
+  a -|> b
+init.sem b = init.bang b metalg
+
+%hint
+public export
+(.pointedCoalgStruct) :
+  (functoriality : signature.Map) =>
+  (str : Strength signature) =>
+  signature.Initial meta a -> type.PointedCoalgStruct a
+init.pointedCoalgStruct = MkPointedCoalgStruct
+  { ren = init.sem ([] a) @{traverse init.metalg.alg init.metalg.var init.metalg.mvar}
+  , var = init.metalg.var
+  }
+
+
+%hint
+public export
+(.monStruct) :
+  (functoriality : signature.Map) =>
+  (str : Strength signature) =>
+  signature.Initial meta a -> type.MonStruct a
+init.monStruct = MkSubstMonoidStruct
+  { var = init.metalg.var
+  , mult = init.sem (a ^ a) @{traverse init.metalg.alg id init.metalg.mvar}
+  }
+
+%hint
+public export
+(.monoidStruct) :
+  (functoriality : signature.Map) =>
+  (str : Strength signature) =>
+  signature.Initial meta a -> signature.MonoidStruct a
+init.monoidStruct = MkSignatureMonoid { mon = init.monStruct , alg = init.metalg.alg }
diff --git a/src/SOAS/Var.idr b/src/SOAS/Var.idr
new file mode 100644
index 0000000..f3129f9
--- /dev/null
+++ b/src/SOAS/Var.idr
@@ -0,0 +1,101 @@
+module SOAS.Var
+
+import SOAS.Context
+import SOAS.Family
+
+prefix 4 %%
+infixr 3 ~> , ~:>
+
+public export
+data (.varPos) : (ctx : type.Ctx) -> (0 x : String) -> type -> Type
+    where [search x]
+  Here  : (ctx :< (x :- ty)).varPos x ty
+  There : ctx.varPos x ty -> (ctx :< sy).varPos x ty
+
+public export
+data (.var) : type.Ctx -> type -> Type where
+  (%%) : (0 name : String) -> {auto pos : ctx.varPos name ty} -> ctx.var ty
+
+0
+(.name) : ctx.var ty -> String
+(%% name).name = name
+
+export
+(.pos) : (v : ctx.var ty) -> ctx.varPos v.name ty
+((%% name) {pos}).pos = pos
+
+export
+(.toVar) : (v : ctx.varPos x ty) -> ctx.var ty
+pos.toVar {x} = (%% x) {pos}
+
+export
+ThereVar : (v : ctx.var ty) -> (ctx :< ex).var ty
+ThereVar v = (%% v.name) {pos = There v.pos}
+
+public export
+Var : type.SortedFamily
+Var = flip (.var)
+
+public export 0
+(.subst) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
+f.subst ctx1 ctx2 = type.gensubst Var f ctx1 ctx2
+
+public export 0
+(.substNamed) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
+f.substNamed ctx1 ctx2 = {0 x : String} -> {0 ty : type} -> ctx1.varPos x ty -> f ty ctx2
+
+public export 0
+(~>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
+(~>) = (Var).subst
+
+public export 0
+(~:>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
+(~:>) = (Var).substNamed
+
+weakl : (ctx1, ctx2 : type.Ctx) -> ctx1 ~> (ctx1 ++ ctx2)
+weakl ctx1 [<] x = x
+weakl ctx1 (ctx2 :< z) x = ThereVar (weakl ctx1 ctx2 x)
+
+weakrNamed : (ctx1, ctx2 : type.Ctx) -> ctx2 ~:> (ctx1 ++ ctx2)
+weakrNamed ctx1 (ctx :< (x :- ty)) Here = (%% x) {pos = Here}
+weakrNamed ctx1 (ctx :< sy) (There pos) =
+  ThereVar $ weakrNamed ctx1 ctx pos
+
+weakr : (ctx1, ctx2 : type.Ctx) -> ctx2 ~> (ctx1 ++ ctx2)
+weakr ctx1 ctx2 ((%% name) {pos}) = weakrNamed ctx1 ctx2 pos
+
+(.copairPos) :
+  (0 x : type.SortedFamily) -> {auto length : ctx2.Erased} ->
+  x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.substNamed (ctx1 ++ ctx2) ctx
+x.copairPos {length = Z} g1 g2 pos = g1 $ pos.toVar
+x.copairPos {length = S l} g1 g2 Here = g2 (Here .toVar)
+x.copairPos {length = S l} g1 g2 (There pos) =
+  x.copairPos g1 (g2 . ThereVar) pos
+
+(.copair) :
+  (0 x : type.SortedFamily) -> {auto length : ctx2.Erased} ->
+  x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.subst (ctx1 ++ ctx2) ctx
+x.copair g1 g2 v = x.copairPos g1 g2 v.pos
+
+export
+extend :
+  (0 x : type.SortedFamily) ->
+  x ty ctx2 -> x.subst ctx1 ctx2 ->
+  x.subst (ctx1 :< (n :- ty)) ctx2
+extend x {ctx2, ty} u theta = x.copair {length = S Z} theta workaround -- (\case {Here => x})
+    where
+      workaround : x.subst [< (n :- ty)] ctx2
+      workaround ((%% _) {pos = Here}) = u
+
+public export 0
+(^) : (tgt, src : type.SortedFamily) -> type.SortedFamily
+(tgt ^ src) ty ctx = src.subst ctx -||> tgt ty
+
+public export 0
+Nil : type.SortedFamily -> type.SortedFamily
+Nil f = f ^ Var
+
+0
+(*) : (derivative, tangent : type.SortedFamily) -> type.SortedFamily
+(derivative * tangent) ty ctx =
+  (ctx' : type.Ctx ** (derivative ty ctx' , tangent.subst ctx' ctx))