diff options
| -rw-r--r-- | soas.ipkg | 1 | ||||
| -rw-r--r-- | src/Example.idr | 104 | ||||
| -rw-r--r-- | src/SOAS.idr | 5 | ||||
| -rw-r--r-- | src/SOAS/Algebra.idr | 1 | ||||
| -rw-r--r-- | src/SOAS/Context.idr | 26 | ||||
| -rw-r--r-- | src/SOAS/Strength.idr | 29 | ||||
| -rw-r--r-- | src/SOAS/Structure.idr | 14 | ||||
| -rw-r--r-- | src/SOAS/Syntax.idr | 103 | ||||
| -rw-r--r-- | src/SOAS/Theory.idr | 14 | ||||
| -rw-r--r-- | src/SOAS/Var.idr | 16 |
10 files changed, 210 insertions, 103 deletions
@@ -22,6 +22,7 @@ modules = SOAS , SOAS.Family , SOAS.Strength , SOAS.Structure + , SOAS.Syntax , SOAS.Theory , SOAS.Var diff --git a/src/Example.idr b/src/Example.idr index 3676d5e..ed7d891 100644 --- a/src/Example.idr +++ b/src/Example.idr @@ -9,77 +9,45 @@ infixr 3 -:> -- but deriving their functoriality and strength is annoying -- and not needed with enough metaprogramming -data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC - -data STLC : TypeSTLC .SortedFunctor where - App : (f : a (ty1 -:> ty2) ctx) -> - (x : a ty1 ctx) -> STLC a ty2 ctx - Lam : (x : String) -> - (body : a ty2 (ctx :< (x :- ty1))) -> - STLC a (ty1 -:> ty2) ctx - -%hint -strSTLC : Strength STLC -strSTLC = MkStrength - { strength = \p,x,mon => \case - (App f x) => \theta => App (f theta) (x theta) - (Lam str {ty1} body) => \theta => - Lam str $ body $ p.extend (mon.var (%% str)) - $ \v => mon.ren (theta v) - (\u => ThereVar u) -- Bug: can't eta-reduce - } - -%hint -functorialitySTLC : STLC .Map -functorialitySTLC = MkMap - { map = \h => \case - (App f x) => App (h f) (h x) - (Lam str body) => Lam str (h body) - } +%hide Syntax.PreorderReasoning.prefix.(|~) +%hide Syntax.PreorderReasoning.Generic.prefix.(|~) -data Term : (meta : type.SortedFamily) -> type.SortedFamily where - Va : Var -|> Term meta - Me : meta -|> Term meta ^ Term meta - Op : STLC (Term meta) -|> Term meta --- -- La : (x : String) -> bind [< x :- ty1 ] (Term meta) ty2 -||> Term meta (ty1 -:> ty2) --- -- bug: unification error in Ex1 --- La : (x : String) -> Term meta ty2 (ctx :< (x :- ty1)) -> Term meta (ty1 -:> ty2) ctx --- -- Ap : Term meta (ty1 -:> ty2) -||> Term meta ty1 =||> Term meta ty2 --- Ap : Term meta (ty1 -:> ty2) ctx -> Term meta ty1 ctx -> Term meta ty2 ctx +data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC -%hint -TermMetaAlg : STLC .MetaAlg meta (Term meta) -TermMetaAlg = MkMetaAlg - { alg = Op - , var = Va - , mvar = Me - } +data OpSTLC : TypeSTLC -> (TypeSTLC .Ctx, TypeSTLC).Ctx -> Type where + App : OpSTLC ty2 [<"f" :- ([<], ty1 -:> ty2), "x" :- ([<], ty1)] + Lam : OpSTLC (ty1 -:> ty2) [<"body" :- ([<"x" :- ty1], ty2)] -%hint -TermInitial : STLC .Initial meta (Term meta) -TermInitial = MkInitial - { metalg = TermMetaAlg - , bang = bang - } - where - bang : (0 b : TypeSTLC .SortedFamily) -> (metalg : STLC .MetaAlg meta b) -> Term meta -|> b - bang b metalg (Va v) = metalg.var v - bang b metalg (Me m theta) = metalg.mvar m (\v => bang b metalg (theta v)) - bang b metalg (Op (Lam str body)) = metalg.alg (Lam str (bang b metalg body)) - bang b metalg (Op (App f x)) = metalg.alg (App (bang b metalg f) (bang b metalg x)) +STLC : TypeSTLC .Signature +STLC = MkSig OpSTLC $ \case + App => [<Z, Z] + Lam => [<S Z] -Ex1 : Term Var (B -:> (B -:> B) -:> B) [<] -Ex1 = Op $ Lam "x" $ Op $ Lam "f" $ Op $ App (Va $ %% "f") (Va $ %% "x") +Ex1 : STLC .Term Var (B -:> (B -:> B) -:> B) [<] +Ex1 = + Alg $ Op Lam [<Bind [<"x"] $ + Alg $ Op Lam [<Bind [<"f"] $ + Alg $ Op App [<[] (Var (%% "f")), [] (Var (%% "x"))]]] beta : - {0 body : Term Var ty2 (ctx :< (x :- ty1))} -> - Singleton (Op $ App (Op $ Lam x body) t) -> Term Var ty2 ctx -beta (Val (Op $ App (Op $ Lam x body) t)) = TermInitial .monStruct.sub body t - -Ex2 : Term Var (B -:> B) [<] -Ex2 = Op $ App - (Op $ Lam "f" $ Op $ Lam "x" $ Op $ App (Va $ %% "f") (Va $ (%% "x") {pos = Here})) - (Op $ Lam "x" $ Va $ %% "x") - -Ex3 : Term Var (B -:> B) [<] -Ex3 = beta $ Val Ex2 + {0 body : STLC .Term Var ty2 (ctx :< (x :- ty1))} -> + Singleton (Alg $ Op App [<[] (Alg $ Op Lam [<Bind [<x] body]), [] t]) -> + STLC .Term Var ty2 ctx +beta (Val $ Alg $ Op App [<Bind [<] $ Alg $ Op Lam [<Bind [<x] body], Bind [<] t]) = + (STLC .Term Var).sub body t + +eta : STLC .Term Var (ty1 -:> ty2) ctx -> STLC .Term Var (ty1 -:> ty2) ctx +eta t = + Alg $ Op Lam [<Bind [<"x"] $ + Alg $ Op App [<[] ((STLC .Term Var).wkn t), [] (Var $ %% "x")]] + +Ex2 : STLC .Term Var (B -:> B) [<] +Ex2 = + Alg $ Op App + [<[] (Alg $ Op Lam [<Bind [<"f"] $ + Alg $ Op Lam [<Bind [<"x"] $ + Alg $ Op App [<[] (Var $ (%% "f") {pos = There Here}), [] (Var $ %% "x")]]]) + , [] (Alg $ Op Lam [<Bind [<"x"] $ Var $ %% "x"])] + +Ex3 : STLC .Term Var (B -:> B) [<] +Ex3 = eta $ beta $ Val Ex2 diff --git a/src/SOAS.idr b/src/SOAS.idr index 892f039..9eb7c4c 100644 --- a/src/SOAS.idr +++ b/src/SOAS.idr @@ -5,6 +5,7 @@ import public SOAS.Context import public SOAS.Family import public SOAS.Strength import public SOAS.Structure +import public SOAS.Syntax import public SOAS.Theory import public SOAS.Var @@ -88,7 +89,3 @@ import public SOAS.Var -- prod : (signatures : List $ type.SortedFunctor) -> -- type.SortedFunctor -- (prod signatures) x ty ctx = All (\sig => sig x ty ctx) signatures - -public export -bind : (tys : type.Ctx) -> type.SortedFunctor -bind tys = (<<< tys) diff --git a/src/SOAS/Algebra.idr b/src/SOAS/Algebra.idr index 7dff735..db701d3 100644 --- a/src/SOAS/Algebra.idr +++ b/src/SOAS/Algebra.idr @@ -27,7 +27,6 @@ record (.MetaAlg) 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) -> diff --git a/src/SOAS/Context.idr b/src/SOAS/Context.idr index ef657ae..e2f3c03 100644 --- a/src/SOAS/Context.idr +++ b/src/SOAS/Context.idr @@ -16,7 +16,7 @@ data (.Ctx) : (type : Type) -> Type where public export data (.Erased) : type.Ctx -> Type where Z : [<].Erased - S : ctx.Erased -> (ctx :< x).Erased + S : ctx.Erased -> (ctx :< (n :- ty)).Erased public export (.toNat) : ctx.Erased -> Nat @@ -27,3 +27,27 @@ public export (++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx ctx1 ++ [<] = ctx1 ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty + +namespace All + public export + data (.All) : type.Ctx -> (p : (0 n : String) -> type -> Type) -> Type where + Lin : [<].All p + (:<) : ctx.All p -> p n ty -> (ctx :< (n :- ty)).All p + + public export + head : (ctx :< (n :- ty)).All p -> p n ty + head (sx :< px) = px + + public export + tail : (ctx :< (n :- ty)).All p -> ctx.All p + tail (sx :< px) = sx + +public export +(.rename) : (ctx : type.Ctx) -> (0 names : ctx.All (\_,_ => String)) -> type.Ctx +[<].rename names = [<] +(ctx :< (_ :- ty)).rename names = ctx.rename (tail names) :< (head names :- ty) + +export +erasedRename : ctx.Erased -> (ctx.rename names).Erased +erasedRename Z = Z +erasedRename (S length) = S (erasedRename length) diff --git a/src/SOAS/Strength.idr b/src/SOAS/Strength.idr index f902ad4..2174baf 100644 --- a/src/SOAS/Strength.idr +++ b/src/SOAS/Strength.idr @@ -1,5 +1,6 @@ module SOAS.Strength +import SOAS.Context import SOAS.Family import SOAS.Structure import SOAS.Var @@ -12,22 +13,28 @@ 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) -> + str : + {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 + +public export +bind : (tys : type.Ctx) -> type.SortedFunctor +bind tys = (<<< tys) + +public export +record BindRename (tys : type.Ctx) (a : type.SortedFamily) (ty : type) (ctx : type.Ctx) where + constructor Bind + 0 names : tys.All (\_,_ => String) + body : a ty (ctx ++ tys.rename names) + +public export +Nil : a -|> BindRename [<] a +[] x = Bind [<] x diff --git a/src/SOAS/Structure.idr b/src/SOAS/Structure.idr index 5f9e1c9..8c5bb5d 100644 --- a/src/SOAS/Structure.idr +++ b/src/SOAS/Structure.idr @@ -34,14 +34,20 @@ record (.MonStruct) (type : Type) (m : type.SortedFamily) where mult : m -|> (m ^ m) export +(.wkn) : + (0 m : type.SortedFamily) -> (mon : type.PointedCoalgStruct m) => + m sy ctx -> m sy (ctx :< (n :- ty)) +m.wkn t = mon.ren t (weakl {length = S Z}) + +export (.sub) : - (mon : type.MonStruct m) -> + (0 m : type.SortedFamily) -> (mon : type.MonStruct m) => m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx -mon.sub t s = mon.mult t (m.extend s mon.var) +m.sub t s = mon.mult t (m.extend s mon.var) export (.sub2) : - (mon : type.MonStruct m) -> + (0 m : type.SortedFamily) -> (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 (m.extend s2 (m.extend s1 mon.var)) +m.sub2 t s1 s2 = mon.mult t (m.extend s2 (m.extend s1 mon.var)) diff --git a/src/SOAS/Syntax.idr b/src/SOAS/Syntax.idr new file mode 100644 index 0000000..7f0e3be --- /dev/null +++ b/src/SOAS/Syntax.idr @@ -0,0 +1,103 @@ +module SOAS.Syntax + +import SOAS.Algebra +import SOAS.Context +import SOAS.Family +import SOAS.Strength +import SOAS.Structure +import SOAS.Theory +import SOAS.Var + +-------------------------------------------------------------------------------- +-- Signatures + +public export +(.ParamsErased) : (type.Ctx, type).Ctx -> Type +params.ParamsErased = params.All (\_, extty => (fst extty).Erased) + +public export +record (.Signature) (type : Type) where + constructor MkSig + 0 ops : (ty : type) -> (params : (type.Ctx, type).Ctx) -> Type + erased : + {0 ty : type} -> {0 params : (type.Ctx, type).Ctx} -> + (op : ops ty params) -> params.ParamsErased + +-------------------------------------------------------------------------------- +-- Functor + +public export +data (.Args) : (type.Ctx, type).Ctx -> type.SortedFamily -> type.Family where + Lin : [<].Args a ctx + (:<) : + params.Args a ctx -> + BindRename ext a ty ctx -> + (params :< (n :- (ext, ty))).Args a ctx + +public export +data (.functor) : type.Signature -> type.SortedFunctor where + Op : (op : sig.ops ty params) -> (args : params.Args a ctx) -> sig.functor a ty ctx + +-------------------------------------------------------------------------------- +-- Functoriality + +argsMap : (a -|> b) -> params.Args a -||> params.Args b +argsMap f [<] = [<] +argsMap f (sx :< (Bind names x)) = argsMap f sx :< (Bind names $ f x) + +export +%hint +(.functorMap) : (0 sig : type.Signature) -> sig.functor.Map +sig.functorMap = MkMap $ \f => \(Op op args) => Op op (argsMap f args) + +-------------------------------------------------------------------------------- +-- Strength + +argsStr : + (erased : params.ParamsErased) -> (mon : type.PointedCoalgStruct p) => + params.Args (x ^ p) -||> params.Args x ^^ p +argsStr [<] [<] {ctx} theta = [<] +argsStr (erased :< length) (sx :< (Bind names x)) {ctx} theta = + argsStr erased sx theta :< (Bind names $ x $ lift (erasedRename length) theta) + +export +%hint +(.functorStrength) : + (sig : type.Signature) -> Strength sig.functor +sig.functorStrength = MkStrength $ + \(Op op args), theta => Op op (argsStr (sig.erased op) args theta) + +-------------------------------------------------------------------------------- +-- Terms + +public export +data (.Term) : (sig : type.Signature) -> type.SortedFunctor where + Var : Var -|> sig.Term a + Alg : sig.functor (sig.Term a) -|> sig.Term a + MVar : a -|> sig.Term a ^ sig.Term a + +%hint +export +(.TermMetalg) : (sig : type.Signature) -> sig.functor.MetaAlg meta (sig.Term meta) +sig.TermMetalg = MkMetaAlg { alg = Alg, var = Var, mvar = MVar } + +%hint +export +(.TermInitial) : (sig : type.Signature) -> sig.functor.Initial meta (sig.Term meta) +sig.TermInitial = MkInitial + { metalg = sig.TermMetalg + , sem = sem + } + where + sem : (0 b : type.SortedFamily) -> (metalg : sig.functor.MetaAlg meta b) => sig.Term meta -|> b + semArgs : + (0 b : type.SortedFamily) -> (metalg : sig.functor.MetaAlg meta b) => + {0 params : (type.Ctx, type).Ctx} -> + params.Args (sig.Term meta) -||> params.Args b + + sem b (Var v) = metalg.var v + sem b (Alg (Op op args)) = metalg.alg $ Op op $ semArgs b args + sem b (MVar m f) = metalg.mvar m $ \v => sem b (f v) + + semArgs b [<] = [<] + semArgs b (sx :< (Bind names x)) = semArgs b sx :< (Bind names $ sem b x) diff --git a/src/SOAS/Theory.idr b/src/SOAS/Theory.idr index f36e7a1..43bb024 100644 --- a/src/SOAS/Theory.idr +++ b/src/SOAS/Theory.idr @@ -14,22 +14,14 @@ record (.Initial) (a : type.SortedFamily) where constructor MkInitial metalg : signature.MetaAlg meta a - bang : + sem : (0 b : type.SortedFamily) -> - (metalg : signature.MetaAlg meta b) -> + (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 @@ -41,7 +33,6 @@ init.pointedCoalgStruct = MkPointedCoalgStruct %hint public export (.monStruct) : - (functoriality : signature.Map) => (str : Strength signature) => signature.Initial meta a -> type.MonStruct a init.monStruct = MkSubstMonoidStruct @@ -52,7 +43,6 @@ init.monStruct = MkSubstMonoidStruct %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 index 22e8028..8362126 100644 --- a/src/SOAS/Var.idr +++ b/src/SOAS/Var.idr @@ -7,7 +7,7 @@ import SOAS.Context import SOAS.Family prefix 4 %% -infixr 3 ~> , ~:> +infixr 3 ~> , ~:>, ^, ^^ -------------------------------------------------------------------------------- -- Variables @@ -127,8 +127,12 @@ x.extend {ty} u theta = x.copair (S Z) theta (x.singleton u) -- Families public export 0 +(^^) : (tgt : type.Family) -> (src : type.SortedFamily) -> type.Family +(tgt ^^ src) ctx = src.subst ctx -||> tgt + +public export 0 (^) : (tgt, src : type.SortedFamily) -> type.SortedFamily -(tgt ^ src) ty ctx = src.subst ctx -||> tgt ty +(tgt ^ src) ty = tgt ty ^^ src public export 0 Nil : type.SortedFamily -> type.SortedFamily @@ -138,3 +142,11 @@ Nil f = f ^ Var (*) : (derivative, tangent : type.SortedFamily) -> type.SortedFamily (derivative * tangent) ty ctx = (ctx' : type.Ctx ** (derivative ty ctx' , tangent.subst ctx' ctx)) + +-------------------------------------------------------------------------------- +-- Utilities + +export +lookup : ctx.All p -> {k : Nat} -> (0 pos : ctx.varAt n k ty) -> p n ty +lookup (sx :< px) Here = px +lookup (sx :< px) (There v) = lookup sx v |