From 829292b51384293976a33210bb6e61321121d46e Mon Sep 17 00:00:00 2001 From: Justin Le Date: Tue, 8 Jan 2019 23:44:21 -0800 Subject: [PATCH 1/6] starting on Free --- Free/Type | 1 + Free/applicative | 23 +++++++++++++++++++++++ Free/foldFree | 16 ++++++++++++++++ Free/functor | 15 +++++++++++++++ Free/hoist | 9 +++++++++ Free/iter | 5 +++++ Free/iterA | 10 ++++++++++ Free/liftF | 11 +++++++++++ Free/monad | 16 ++++++++++++++++ Free/package.dhall | 15 +++++++++++++++ Free/recursive | 16 ++++++++++++++++ Free/retract | 11 +++++++++++ Free/transformer | 13 +++++++++++++ Free/wrap | 11 +++++++++++ FreeF/Type | 1 + 15 files changed, 173 insertions(+) create mode 100644 Free/Type create mode 100644 Free/applicative create mode 100644 Free/foldFree create mode 100644 Free/functor create mode 100644 Free/hoist create mode 100644 Free/iter create mode 100644 Free/iterA create mode 100644 Free/liftF create mode 100644 Free/monad create mode 100644 Free/package.dhall create mode 100644 Free/recursive create mode 100644 Free/retract create mode 100644 Free/transformer create mode 100644 Free/wrap create mode 100644 FreeF/Type diff --git a/Free/Type b/Free/Type new file mode 100644 index 0000000..3f37842 --- /dev/null +++ b/Free/Type @@ -0,0 +1 @@ +λ(f : Type → Type) → λ(a : Type) → ∀(r : Type) → (a → r) → (f r → r) → r diff --git a/Free/applicative b/Free/applicative new file mode 100644 index 0000000..7196cb4 --- /dev/null +++ b/Free/applicative @@ -0,0 +1,23 @@ + let Applicative = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type + +in λ(f : Type → Type) + → { ap = + λ(a : Type) + → λ(b : Type) + → λ(mf : ./Type f (a → b)) + → λ(mx : ./Type f a) + → λ(r : Type) + → λ(kp : b → r) + → λ(kf : f r → r) + → mf r (λ(ff : a → b) → mx r (λ(xx : a) → kp (ff xx)) kf) kf + , pure = + λ(a : Type) + → λ(x : a) + → λ(r : Type) + → λ(kp : a → r) + → λ(kf : f r → r) + → kp x + } + ∧ ./functor f + : Applicative (./Type f) diff --git a/Free/foldFree b/Free/foldFree new file mode 100644 index 0000000..8bf5a90 --- /dev/null +++ b/Free/foldFree @@ -0,0 +1,16 @@ + let Monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type + +in let Monad/monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall + +in λ(f : Type → Type) + → λ(g : Type → Type) + → λ(monad : Monad g) + → λ(a : Type) + → λ(n : ∀(x : Type) → f x → g x) + → λ(m : ./Type f a) + → m + (g a) + (monad.pure a) + (λ(q : f (g a)) → (Monad/monad g monad).join a (n (g a) q)) diff --git a/Free/functor b/Free/functor new file mode 100644 index 0000000..4737bed --- /dev/null +++ b/Free/functor @@ -0,0 +1,15 @@ + let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + +in λ(f : Type → Type) + → { map = + λ(a : Type) + → λ(b : Type) + → λ(g : a → b) + → λ(m : ./Type f a) + → λ(r : Type) + → λ(kp : b → r) + → λ(kf : f r → r) + → m r (λ(x : a) → kp (g x)) kf + } + : Functor (./Type f) diff --git a/Free/hoist b/Free/hoist new file mode 100644 index 0000000..d4a0685 --- /dev/null +++ b/Free/hoist @@ -0,0 +1,9 @@ + λ(f : Type → Type) +→ λ(g : Type → Type) +→ λ(a : Type) +→ λ(n : ∀(x : Type) → f x → g x) +→ λ(m : ./Type f a) +→ λ(r : Type) +→ λ(kp : a → r) +→ λ(kf : g r → r) +→ m r kp (λ(q : f r) → kf (n r q)) diff --git a/Free/iter b/Free/iter new file mode 100644 index 0000000..d38e56a --- /dev/null +++ b/Free/iter @@ -0,0 +1,5 @@ + λ(f : Type → Type) +→ λ(a : Type) +→ λ(phi : f a → a) +→ λ(m : ./Type f a) +→ m a (λ(x : a) → x) phi diff --git a/Free/iterA b/Free/iterA new file mode 100644 index 0000000..c52752d --- /dev/null +++ b/Free/iterA @@ -0,0 +1,10 @@ + let Applicative = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type + +in λ(f : Type → Type) + → λ(g : Type → Type) + → λ(applicative : Applicative g) + → λ(a : Type) + → λ(phi : f (g a) → g a) + → λ(m : ./Type f a) + → m (g a) (applicative.pure a) phi diff --git a/Free/liftF b/Free/liftF new file mode 100644 index 0000000..2bf16c8 --- /dev/null +++ b/Free/liftF @@ -0,0 +1,11 @@ + let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + +in λ(f : Type → Type) + → λ(functor : Functor f) + → λ(a : Type) + → λ(x : f a) + → λ(r : Type) + → λ(kp : a → r) + → λ(kf : f r → r) + → kf (functor.map a r kp x) diff --git a/Free/monad b/Free/monad new file mode 100644 index 0000000..32b8655 --- /dev/null +++ b/Free/monad @@ -0,0 +1,16 @@ + let Monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type + +in λ(f : Type → Type) + → { bind = + λ(a : Type) + → λ(b : Type) + → λ(m : ./Type f a) + → λ(g : a → ./Type f b) + → λ(r : Type) + → λ(kp : b → r) + → λ(kf : f r → r) + → m r (λ(x : a) → g x r kp kf) kf + } + ∧ ./applicative f + : Monad (./Type f) diff --git a/Free/package.dhall b/Free/package.dhall new file mode 100644 index 0000000..2918aba --- /dev/null +++ b/Free/package.dhall @@ -0,0 +1,15 @@ + λ(f : Type → Type) +→ { iter = + ./iter f + , iterA = + ./iterA f + , retract = + ./retract f + , wrap = + ./wrap f + , liftF = + ./liftF f + , foldFree = + ./foldFree f + } + ∧ ./monad f ⫽ ./transformer diff --git a/Free/recursive b/Free/recursive new file mode 100644 index 0000000..64b241f --- /dev/null +++ b/Free/recursive @@ -0,0 +1,16 @@ + let Free = ./Type + +in let FreeF = ./../FreeF/Type + +in λ(f : Type → Type) + → λ(a : Type) + → { cata = + λ(b : Type) + → λ(alg : ./../algebra (FreeF f a) b) + → λ(fa : Free f a) + → fa + b + (λ(x : a) → alg ((FreeF f a b).Pure x)) + (λ(x : f b) → alg ((FreeF f a b).Free x)) + } + : ./../Recursive/Type (Free f a) (FreeF f a) diff --git a/Free/retract b/Free/retract new file mode 100644 index 0000000..6420f0c --- /dev/null +++ b/Free/retract @@ -0,0 +1,11 @@ + let Monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type + +in let Monad/monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall + +in λ(f : Type → Type) + → λ(a : Type) + → λ(monad : Monad f) + → λ(m : ./Type f a) + → m (f a) (monad.pure a) ((Monad/monad f monad).join a) diff --git a/Free/transformer b/Free/transformer new file mode 100644 index 0000000..93116bd --- /dev/null +++ b/Free/transformer @@ -0,0 +1,13 @@ + let Monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type + +in let Transformer = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Transformer/Type + +in { lift = + λ(m : Type → Type) + → λ(monad : Monad m) + → λ(a : Type) + → ./liftF m { map = monad.map } a + } + : Transformer ./Type diff --git a/Free/wrap b/Free/wrap new file mode 100644 index 0000000..be24491 --- /dev/null +++ b/Free/wrap @@ -0,0 +1,11 @@ + let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + +in λ(f : Type → Type) + → λ(a : Type) + → λ(functor : Functor f) + → λ(x : f (./Type f a)) + → λ(r : Type) + → λ(kp : a → r) + → λ(kf : f r → r) + → kf (functor.map (./Type f a) r (λ(m : ./Type f a) → m r kp kf) x) diff --git a/FreeF/Type b/FreeF/Type new file mode 100644 index 0000000..953f49d --- /dev/null +++ b/FreeF/Type @@ -0,0 +1 @@ +λ(f : Type → Type) → λ(a : Type) → λ(b : Type) → < Pure : a | Free : f b > From 47eae650e68d8d329bdd5548fe7594f3b9f725c6 Mon Sep 17 00:00:00 2001 From: Justin Le Date: Wed, 9 Jan 2019 00:05:28 -0800 Subject: [PATCH 2/6] formatting tweaks to match style --- Free/foldFree | 24 +++++++++++++----------- Free/retract | 20 ++++++++++++-------- Free/wrap | 4 ++-- 3 files changed, 27 insertions(+), 21 deletions(-) diff --git a/Free/foldFree b/Free/foldFree index 8bf5a90..e66e225 100644 --- a/Free/foldFree +++ b/Free/foldFree @@ -1,16 +1,18 @@ let Monad = https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type -in let Monad/monad = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall - -in λ(f : Type → Type) +in λ ( f + : Type → Type + ) → λ(g : Type → Type) → λ(monad : Monad g) - → λ(a : Type) - → λ(n : ∀(x : Type) → f x → g x) - → λ(m : ./Type f a) - → m - (g a) - (monad.pure a) - (λ(q : f (g a)) → (Monad/monad g monad).join a (n (g a) q)) + → let join = + ( https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall + g + monad + ).join + + in λ(a : Type) + → λ(n : ∀(x : Type) → f x → g x) + → λ(m : ./Type f a) + → m (g a) (monad.pure a) (λ(q : f (g a)) → join a (n (g a) q)) diff --git a/Free/retract b/Free/retract index 6420f0c..1b87628 100644 --- a/Free/retract +++ b/Free/retract @@ -1,11 +1,15 @@ - let Monad = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type + let Monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type -in let Monad/monad = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall - -in λ(f : Type → Type) +in λ ( f + : Type → Type + ) → λ(a : Type) → λ(monad : Monad f) - → λ(m : ./Type f a) - → m (f a) (monad.pure a) ((Monad/monad f monad).join a) + → let join = + ( https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall + f + monad + ).join + + in λ(m : ./Type f a) → m (f a) (monad.pure a) (join a) diff --git a/Free/wrap b/Free/wrap index be24491..4ce1dfc 100644 --- a/Free/wrap +++ b/Free/wrap @@ -1,5 +1,5 @@ - let Functor = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type in λ(f : Type → Type) → λ(a : Type) From d9f2666730955b74cb2510eb87d9df5635e08ff9 Mon Sep 17 00:00:00 2001 From: Justin Le Date: Wed, 9 Jan 2019 00:37:53 -0800 Subject: [PATCH 3/6] steppable instances for Free --- Free/recursive | 8 +++----- Free/steppable | 44 ++++++++++++++++++++++++++++++++++++++++++++ FreeF/functor | 20 ++++++++++++++++++++ 3 files changed, 67 insertions(+), 5 deletions(-) create mode 100644 Free/steppable create mode 100644 FreeF/functor diff --git a/Free/recursive b/Free/recursive index 64b241f..8f80526 100644 --- a/Free/recursive +++ b/Free/recursive @@ -1,16 +1,14 @@ - let Free = ./Type - -in let FreeF = ./../FreeF/Type + let FreeF = ./../FreeF/Type in λ(f : Type → Type) → λ(a : Type) → { cata = λ(b : Type) → λ(alg : ./../algebra (FreeF f a) b) - → λ(fa : Free f a) + → λ(fa : ./Type f a) → fa b (λ(x : a) → alg ((FreeF f a b).Pure x)) (λ(x : f b) → alg ((FreeF f a b).Free x)) } - : ./../Recursive/Type (Free f a) (FreeF f a) + : ./../Recursive/Type (./Type f a) (FreeF f a) diff --git a/Free/steppable b/Free/steppable new file mode 100644 index 0000000..a577c34 --- /dev/null +++ b/Free/steppable @@ -0,0 +1,44 @@ +let Free = ./Type + +let FreeF = ./../FreeF/Type + +let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + +in λ(f : Type → Type) + → λ(functor : Functor f) + → λ(a : Type) + → let cata = (./recursive f a).cata + + in let embed + : FreeF f a (Free f a) → Free f a + = λ(fm : FreeF f a (Free f a)) + → λ(r : Type) + → λ(kp : a → r) + → λ(kf : f r → r) + → merge + { Pure = + λ(x : a) → kp x + , Free = + λ(x : f (Free f a)) + → kf + ( functor.map + (Free f a) + r + (λ(y : Free f a) → y r kp kf) + x + ) + } + fm + + in { embed = + embed + , project = + ./../lambek + (./Type f a) + (FreeF f a) + cata + embed + (./../FreeF/functor f functor a) + } + : ./../Steppable/Type (./Type f a) (FreeF f a) diff --git a/FreeF/functor b/FreeF/functor new file mode 100644 index 0000000..f7cd276 --- /dev/null +++ b/FreeF/functor @@ -0,0 +1,20 @@ + let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + +in λ(f : Type → Type) + → λ(functor : Functor f) + → λ(c : Type) + → { map = + λ(a : Type) + → λ(b : Type) + → λ(g : a → b) + → λ(m : ./Type f c a) + → merge + { Pure = + λ(x : c) → (./Type f c b).Pure x + , Free = + λ(x : f a) → (./Type f c b).Free (functor.map a b g x) + } + m + } + : Functor (./Type f c) From 491e3271c984d574e637fa23ff42f5d9044fb42b Mon Sep 17 00:00:00 2001 From: Justin Le Date: Mon, 14 Jan 2019 22:53:02 -0800 Subject: [PATCH 4/6] style adjustments for Free --- Free/foldFree | 30 ++++++++++++---------- Free/fromMu | 9 +++++++ Free/functor | 16 ++++++------ Free/package.dhall | 4 +++ Free/recursive | 21 ++++++++-------- Free/retract | 18 ++++---------- Free/steppable | 62 ++++++++++++++++++++++------------------------ Free/toMu | 8 ++++++ Free/transformer | 2 +- FreeF/bifunctor | 25 +++++++++++++++++++ FreeF/functor | 29 ++++++++-------------- 11 files changed, 127 insertions(+), 97 deletions(-) create mode 100644 Free/fromMu create mode 100644 Free/toMu create mode 100644 FreeF/bifunctor diff --git a/Free/foldFree b/Free/foldFree index e66e225..14f68f8 100644 --- a/Free/foldFree +++ b/Free/foldFree @@ -1,18 +1,22 @@ let Monad = https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type -in λ ( f - : Type → Type - ) +in let Monad/package = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall + +in λ(f : Type → Type) → λ(g : Type → Type) → λ(monad : Monad g) - → let join = - ( https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall - g - monad - ).join - - in λ(a : Type) - → λ(n : ∀(x : Type) → f x → g x) - → λ(m : ./Type f a) - → m (g a) (monad.pure a) (λ(q : f (g a)) → join a (n (g a) q)) + → λ(a : Type) + → λ(n : ∀(x : Type) → f x → g x) + → (./recursive f a).cata + (g a) + ( λ(free : ./../FreeF/Type f a (g a)) + → merge + { Pure = + monad.pure a + , Free = + λ(q : f (g a)) → (Monad/package g monad).join a (n (g a) q) + } + free + ) diff --git a/Free/fromMu b/Free/fromMu new file mode 100644 index 0000000..e8bbd5f --- /dev/null +++ b/Free/fromMu @@ -0,0 +1,9 @@ +let FreeF = ./../FreeF/Type + +in λ(f : Type → Type) + → λ(a : Type) + → λ(m : ./../Mu/Type (FreeF f a)) + → λ(r : Type) + → λ(kp : a → r) + → λ(kf : f r → r) + → m r (λ(free : FreeF f a r) → merge { Pure = kp, Free = kf } free) diff --git a/Free/functor b/Free/functor index 4737bed..ccd3625 100644 --- a/Free/functor +++ b/Free/functor @@ -1,15 +1,17 @@ let Functor = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type -in λ(f : Type → Type) +in let FreeF = ./../FreeF/Type + +in λ(F : Type → Type) → { map = λ(a : Type) → λ(b : Type) - → λ(g : a → b) - → λ(m : ./Type f a) + → λ(f : a → b) + → λ(m : ./Type F a) → λ(r : Type) → λ(kp : b → r) - → λ(kf : f r → r) - → m r (λ(x : a) → kp (g x)) kf + → λ(kf : F r → r) + → m r (λ(x : a) → kp (f x)) kf } - : Functor (./Type f) + : Functor (./Type F) diff --git a/Free/package.dhall b/Free/package.dhall index 2918aba..f586d8c 100644 --- a/Free/package.dhall +++ b/Free/package.dhall @@ -11,5 +11,9 @@ ./liftF f , foldFree = ./foldFree f + , toMu = + ./toMu f + , fromMu = + ./fromMu f } ∧ ./monad f ⫽ ./transformer diff --git a/Free/recursive b/Free/recursive index 8f80526..a4889f2 100644 --- a/Free/recursive +++ b/Free/recursive @@ -1,14 +1,13 @@ - let FreeF = ./../FreeF/Type - -in λ(f : Type → Type) - → λ(a : Type) - → { cata = + λ(f : Type → Type) +→ λ(a : Type) +→ let FreeF = ./../FreeF/Type f a + + in let Mu/recursive = ./../Mu/recursive FreeF + + in { cata = λ(b : Type) - → λ(alg : ./../algebra (FreeF f a) b) + → λ(alg : ./../algebra FreeF b) → λ(fa : ./Type f a) - → fa - b - (λ(x : a) → alg ((FreeF f a b).Pure x)) - (λ(x : f b) → alg ((FreeF f a b).Free x)) + → Mu/recursive.cata b alg (./toMu f a fa) } - : ./../Recursive/Type (./Type f a) (FreeF f a) + : ./../Recursive/Type (./Type f a) FreeF diff --git a/Free/retract b/Free/retract index 1b87628..3addc68 100644 --- a/Free/retract +++ b/Free/retract @@ -1,15 +1,7 @@ - let Monad = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type + let Monad = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type -in λ ( f - : Type → Type - ) - → λ(a : Type) +in λ(f : Type → Type) → λ(monad : Monad f) - → let join = - ( https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall - f - monad - ).join - - in λ(m : ./Type f a) → m (f a) (monad.pure a) (join a) + → λ(a : Type) + → ./foldFree f f monad a (λ(b : Type) → λ(x : f b) → x) diff --git a/Free/steppable b/Free/steppable index a577c34..d985422 100644 --- a/Free/steppable +++ b/Free/steppable @@ -1,44 +1,40 @@ -let Free = ./Type - -let FreeF = ./../FreeF/Type - let Functor = https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type in λ(f : Type → Type) → λ(functor : Functor f) → λ(a : Type) - → let cata = (./recursive f a).cata + → let Free = ./Type f a - in let embed - : FreeF f a (Free f a) → Free f a - = λ(fm : FreeF f a (Free f a)) - → λ(r : Type) - → λ(kp : a → r) - → λ(kf : f r → r) - → merge - { Pure = - λ(x : a) → kp x - , Free = - λ(x : f (Free f a)) - → kf - ( functor.map - (Free f a) - r - (λ(y : Free f a) → y r kp kf) - x - ) - } - fm + in let FreeF = ./../FreeF/Type f a + + in let FreeF/functor = ./../FreeF/functor f functor a + + in let MuFree = ./../Mu/Type FreeF + + in let Mu/steppable = ./../Mu/steppable FreeF FreeF/functor + + in let toMu = ./toMu f a + + in let fromMu = ./fromMu f a in { embed = - embed + λ(fm : FreeF Free) + → fromMu + ( Mu/steppable.embed + ( FreeF/functor.map + Free + MuFree + toMu + fm + ) + ) , project = - ./../lambek - (./Type f a) - (FreeF f a) - cata - embed - (./../FreeF/functor f functor a) + λ(fm : Free) + → FreeF/functor.map + MuFree + Free + fromMu + (Mu/steppable.project (toMu fm)) } - : ./../Steppable/Type (./Type f a) (FreeF f a) + : ./../Steppable/Type Free FreeF diff --git a/Free/toMu b/Free/toMu new file mode 100644 index 0000000..2226095 --- /dev/null +++ b/Free/toMu @@ -0,0 +1,8 @@ + λ(F : Type → Type) +→ λ(a : Type) +→ λ(m : ./Type F a) +→ λ(r : Type) +→ let FreeF = ./../FreeF/Type F a r + + in λ(f : FreeF → r) + → m r (λ(x : a) → f (FreeF.Pure x)) (λ(x : F r) → f (FreeF.Free x)) diff --git a/Free/transformer b/Free/transformer index 93116bd..ed2023f 100644 --- a/Free/transformer +++ b/Free/transformer @@ -8,6 +8,6 @@ in { lift = λ(m : Type → Type) → λ(monad : Monad m) → λ(a : Type) - → ./liftF m { map = monad.map } a + → ./liftF m monad.{map} a } : Transformer ./Type diff --git a/FreeF/bifunctor b/FreeF/bifunctor new file mode 100644 index 0000000..747a3bf --- /dev/null +++ b/FreeF/bifunctor @@ -0,0 +1,25 @@ + let Bifunctor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Bifunctor/Type + +in let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + +in λ(F : Type → Type) + → λ(functor : Functor F) + → { bimap = + λ(a : Type) + → λ(b : Type) + → λ(c : Type) + → λ(d : Type) + → λ(f : a → c) + → λ(g : b → d) + → λ(m : ./Type F a b) + → merge + { Pure = + λ(x : a) → (./Type F c d).Pure (f x) + , Free = + λ(x : F b) → (./Type F c d).Free (functor.map b d g x) + } + m + } + : Bifunctor (./Type F) diff --git a/FreeF/functor b/FreeF/functor index f7cd276..5668dca 100644 --- a/FreeF/functor +++ b/FreeF/functor @@ -1,20 +1,11 @@ - let Functor = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type - -in λ(f : Type → Type) - → λ(functor : Functor f) + let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + +in let second = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Bifunctor/second + +in λ(F : Type → Type) + → λ(functor : Functor F) → λ(c : Type) - → { map = - λ(a : Type) - → λ(b : Type) - → λ(g : a → b) - → λ(m : ./Type f c a) - → merge - { Pure = - λ(x : c) → (./Type f c b).Pure x - , Free = - λ(x : f a) → (./Type f c b).Free (functor.map a b g x) - } - m - } - : Functor (./Type f c) + → { map = second (./Type F) (./bifunctor F functor) c } + : Functor (./Type F c) From 583b885dc6bff1b6958a045759b3cfdf62513904 Mon Sep 17 00:00:00 2001 From: Justin Le Date: Tue, 15 Jan 2019 01:21:03 -0800 Subject: [PATCH 5/6] Foldable, Traversable for Free and FreeF --- Free/foldable | 33 +++++++++++++++++++++++++++++++ Free/functor | 2 -- Free/steppable | 25 +++++++++--------------- Free/transformer | 5 ++++- Free/traversable | 50 +++++++++++++++++++++++++++++++++++++++++++++++ FreeF/foldable | 21 ++++++++++++++++++++ FreeF/traversable | 42 +++++++++++++++++++++++++++++++++++++++ 7 files changed, 159 insertions(+), 19 deletions(-) create mode 100644 Free/foldable create mode 100644 Free/traversable create mode 100644 FreeF/foldable create mode 100644 FreeF/traversable diff --git a/Free/foldable b/Free/foldable new file mode 100644 index 0000000..a4595ed --- /dev/null +++ b/Free/foldable @@ -0,0 +1,33 @@ + let Foldable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type + +in let Function/category = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Function/category + +in λ(F : Type → Type) + → λ(foldable : Foldable F) + → { fold = + λ(a : Type) + → λ(ts : ./Type F a) + → λ(b : Type) + → λ(f : a → b → b) + → (./recursive F a).cata + (b → b) + ( λ(x : ./../FreeF/Type F a (b → b)) + → merge + { Pure = + λ(x : a) → f x + , Free = + λ(x : F (b → b)) + → foldable.fold + (b → b) + x + (b → b) + (Function/category.compose b b b) + (Function/category.identity b) + } + x + ) + ts + } + : Foldable (./Type F) diff --git a/Free/functor b/Free/functor index ccd3625..9d8f685 100644 --- a/Free/functor +++ b/Free/functor @@ -1,8 +1,6 @@ let Functor = https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type -in let FreeF = ./../FreeF/Type - in λ(F : Type → Type) → { map = λ(a : Type) diff --git a/Free/steppable b/Free/steppable index d985422..add2717 100644 --- a/Free/steppable +++ b/Free/steppable @@ -1,5 +1,5 @@ -let Functor = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type + let Functor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type in λ(f : Type → Type) → λ(functor : Functor f) @@ -7,28 +7,21 @@ in λ(f : Type → Type) → let Free = ./Type f a in let FreeF = ./../FreeF/Type f a - + in let FreeF/functor = ./../FreeF/functor f functor a - + in let MuFree = ./../Mu/Type FreeF - + in let Mu/steppable = ./../Mu/steppable FreeF FreeF/functor - + in let toMu = ./toMu f a - + in let fromMu = ./fromMu f a - + in { embed = λ(fm : FreeF Free) → fromMu - ( Mu/steppable.embed - ( FreeF/functor.map - Free - MuFree - toMu - fm - ) - ) + (Mu/steppable.embed (FreeF/functor.map Free MuFree toMu fm)) , project = λ(fm : Free) → FreeF/functor.map diff --git a/Free/transformer b/Free/transformer index ed2023f..0238d36 100644 --- a/Free/transformer +++ b/Free/transformer @@ -3,11 +3,14 @@ in let Transformer = https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Transformer/Type + +in let extractFunctor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/extractFunctor in { lift = λ(m : Type → Type) → λ(monad : Monad m) → λ(a : Type) - → ./liftF m monad.{map} a + → ./liftF m (extractFunctor m monad) a } : Transformer ./Type diff --git a/Free/traversable b/Free/traversable new file mode 100644 index 0000000..3d3ea1e --- /dev/null +++ b/Free/traversable @@ -0,0 +1,50 @@ + let Applicative = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type + +in let Foldable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type + +in let Traversable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/Type + +in let extractFoldable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFoldable + +in let extractFunctor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFunctor + +in let sequence = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/sequence + +in λ(F : Type → Type) + → λ(traversable : Traversable F) + → { traverse = + λ(G : Type → Type) + → λ(applicative : Applicative G) + → λ(a : Type) + → λ(b : Type) + → λ(f : a → G b) + → (./recursive F a).cata + (G (./Type F b)) + ( λ(x : ./../FreeF/Type F a (G (./Type F b))) + → merge + { Pure = + λ(x : a) + → applicative.map + b + (./Type F b) + ((./applicative F).pure b) + (f x) + , Free = + λ(x : F (G (./Type F b))) + → applicative.map + (F (./Type F b)) + (./Type F b) + (./wrap F b (extractFunctor F traversable)) + (sequence F traversable G applicative (./Type F b) x) + } + x + ) + } + ∧ ./foldable F (extractFoldable F traversable) ⫽ ./functor F + : Traversable (./Type F) diff --git a/FreeF/foldable b/FreeF/foldable new file mode 100644 index 0000000..dffcbf9 --- /dev/null +++ b/FreeF/foldable @@ -0,0 +1,21 @@ + let Foldable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type + +in λ(F : Type → Type) + → λ(foldable : Foldable F) + → λ(c : Type) + → { fold = + λ(a : Type) + → λ(ts : ./Type F c a) + → λ(b : Type) + → λ(f : a → b → b) + → λ(z : b) + → merge + { Pure = + λ(x : c) → z + , Free = + λ(x : F a) → foldable.fold a x b f z + } + ts + } + : Foldable (./Type F c) diff --git a/FreeF/traversable b/FreeF/traversable new file mode 100644 index 0000000..8b2a507 --- /dev/null +++ b/FreeF/traversable @@ -0,0 +1,42 @@ +let Applicative = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type + +let Foldable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type + +let Traversable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/Type + +let extractFoldable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFoldable + +let extractFunctor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFunctor + +in λ(F : Type → Type) + → λ(traversable : Traversable F) + → λ(c : Type) + → { traverse = + λ(G : Type → Type) + → λ(applicative : Applicative G) + → λ(a : Type) + → λ(b : Type) + → λ(f : a → G b) + → λ(ts : ./Type F c a) + → merge + { Pure = + λ(x : c) + → applicative.pure (./Type F c b) ((./Type F c b).Pure x) + , Free = + λ(x : F a) + → applicative.map + (F b) + (./Type F c b) + (λ(y : F b) → (./Type F c b).Free y) + (traversable.traverse G applicative a b f x) + } + ts + } + ∧ ./foldable F (extractFoldable F traversable) c + ⫽ ./functor F (extractFunctor F traversable) c + : Traversable (./Type F c) From a018facdd1024e74f822fb1004549889db254732 Mon Sep 17 00:00:00 2001 From: Justin Le Date: Tue, 15 Jan 2019 01:27:33 -0800 Subject: [PATCH 6/6] fixed some formatting and clarity for traversable instances --- Free/traversable | 3 --- FreeF/traversable | 46 ++++++++++++++++++++++------------------------ 2 files changed, 22 insertions(+), 27 deletions(-) diff --git a/Free/traversable b/Free/traversable index 3d3ea1e..a5e27a9 100644 --- a/Free/traversable +++ b/Free/traversable @@ -1,9 +1,6 @@ let Applicative = https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type -in let Foldable = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type - in let Traversable = https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/Type diff --git a/FreeF/traversable b/FreeF/traversable index 8b2a507..6c1094b 100644 --- a/FreeF/traversable +++ b/FreeF/traversable @@ -1,17 +1,14 @@ -let Applicative = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type + let Applicative = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/Type -let Foldable = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Foldable/Type +in let Traversable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/Type -let Traversable = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/Type +in let extractFoldable = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFoldable -let extractFoldable = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFoldable - -let extractFunctor = - https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFunctor +in let extractFunctor = + https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Traversable/extractFunctor in λ(F : Type → Type) → λ(traversable : Traversable F) @@ -23,19 +20,20 @@ in λ(F : Type → Type) → λ(b : Type) → λ(f : a → G b) → λ(ts : ./Type F c a) - → merge - { Pure = - λ(x : c) - → applicative.pure (./Type F c b) ((./Type F c b).Pure x) - , Free = - λ(x : F a) - → applicative.map - (F b) - (./Type F c b) - (λ(y : F b) → (./Type F c b).Free y) - (traversable.traverse G applicative a b f x) - } - ts + → let FreeF = ./Type F c b + + in merge + { Pure = + λ(x : c) → applicative.pure FreeF (FreeF.Pure x) + , Free = + λ(x : F a) + → applicative.map + (F b) + FreeF + FreeF.Free + (traversable.traverse G applicative a b f x) + } + ts } ∧ ./foldable F (extractFoldable F traversable) c ⫽ ./functor F (extractFunctor F traversable) c