Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

church-encoded Free monad #8

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

church-encoded Free monad #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
829292b
starting on Free
mstksg Jan 9, 2019
47eae65
formatting tweaks to match style
mstksg Jan 9, 2019
d9f2666
steppable instances for Free
mstksg Jan 9, 2019
491e327
style adjustments for Free
mstksg Jan 15, 2019
583b885
Foldable, Traversable for Free and FreeF
mstksg Jan 15, 2019
a018fac
fixed some formatting and clarity for traversable instances
mstksg Jan 15, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Free/Type
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
λ(f : Type → Type) → λ(a : Type) → ∀(r : Type) → (a → r) → (f r → r) → r
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should now look like

λ(f : Type → Type) → λ(a : Type) → ../../Mu/Type (../../FreeF/Type f a)

Also, it doesn’t exist on master yet, but I’ve started putting types like this (i.e., recursive types) into a “data/” directory, so this would then be “data/Free/Type”. There are some examples of this on the kind-polymorphism branch.

Copy link
Author

@mstksg mstksg Jan 10, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, even though the two types are the same, I think there's some benefit in separating the fixed-point from the base functor. Basically like how we have List a and XNor, and we have Natural with Maybe, and we have NonEmpty and AndMaybe. And one benefit in implementing Free directly is that we can work directly with Free as a "normal function", instead of importing an intermediate data type to use it.

(edit: Although, now that I think about it, merge doesn't require importing constructor names, so it'd be possible to "make" a Free value without importing FreeF, but you'd need to import FreeF to use a Free value.)

In the end it might just be a stylistic thing, and I think there could be benefits both ways.

23 changes: 23 additions & 0 deletions Free/applicative
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
22 changes: 22 additions & 0 deletions Free/foldFree
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
let Monad =
https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/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)
→ λ(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
)
33 changes: 33 additions & 0 deletions Free/foldable
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
9 changes: 9 additions & 0 deletions Free/fromMu
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
15 changes: 15 additions & 0 deletions Free/functor
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
→ λ(f : a → b)
→ λ(m : ./Type F a)
→ λ(r : Type)
→ λ(kp : b → r)
→ λ(kf : F r → r)
→ m r (λ(x : a) → kp (f x)) kf
}
: Functor (./Type F)
9 changes: 9 additions & 0 deletions Free/hoist
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))
5 changes: 5 additions & 0 deletions Free/iter
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
λ(f : Type → Type)
→ λ(a : Type)
→ λ(phi : f a → a)
→ λ(m : ./Type f a)
→ m a (λ(x : a) → x) phi
10 changes: 10 additions & 0 deletions Free/iterA
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
11 changes: 11 additions & 0 deletions Free/liftF
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
16 changes: 16 additions & 0 deletions Free/monad
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
19 changes: 19 additions & 0 deletions Free/package.dhall
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
λ(f : Type → Type)
→ { iter =
./iter f
, iterA =
./iterA f
, retract =
./retract f
, wrap =
./wrap f
, liftF =
./liftF f
, foldFree =
./foldFree f
, toMu =
./toMu f
, fromMu =
./fromMu f
}
∧ ./monad f ⫽ ./transformer
13 changes: 13 additions & 0 deletions Free/recursive
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
λ(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 b)
→ λ(fa : ./Type f a)
→ Mu/recursive.cata b alg (./toMu f a fa)
}
: ./../Recursive/Type (./Type f a) FreeF
7 changes: 7 additions & 0 deletions Free/retract
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
let Monad =
https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type

in λ(f : Type → Type)
→ λ(monad : Monad f)
→ λ(a : Type)
→ ./foldFree f f monad a (λ(b : Type) → λ(x : f b) → x)
33 changes: 33 additions & 0 deletions Free/steppable
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
let Functor =
https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Functor/Type

in λ(f : Type → Type)
→ λ(functor : Functor f)
→ λ(a : 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))
, project =
λ(fm : Free)
→ FreeF/functor.map
MuFree
Free
fromMu
(Mu/steppable.project (toMu fm))
}
: ./../Steppable/Type Free FreeF
8 changes: 8 additions & 0 deletions Free/toMu
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))
16 changes: 16 additions & 0 deletions Free/transformer
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
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 let extractFunctor =
https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/extractFunctor

in { lift =
λ(m : Type → Type)
→ λ(monad : Monad m)
→ λ(a : Type)
→ ./liftF m (extractFunctor m monad) a
}
: Transformer ./Type
47 changes: 47 additions & 0 deletions Free/traversable
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
let Applicative =
https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Applicative/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)
11 changes: 11 additions & 0 deletions Free/wrap
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
1 change: 1 addition & 0 deletions FreeF/Type
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
λ(f : Type → Type) → λ(a : Type) → λ(b : Type) → < Pure : a | Free : f b >
mstksg marked this conversation as resolved.
Show resolved Hide resolved
25 changes: 25 additions & 0 deletions FreeF/bifunctor
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
21 changes: 21 additions & 0 deletions FreeF/foldable
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
11 changes: 11 additions & 0 deletions FreeF/functor
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
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 = second (./Type F) (./bifunctor F functor) c }
: Functor (./Type F c)
Loading