Skip to content

church-encoded Free monad #8

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

Open
mstksg 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 3 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

@sellout sellout Jan 10, 2019

Copy link
Copy Markdown
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.

@mstksg mstksg Jan 10, 2019 •
edited
Loading

Copy link
Copy Markdown
Author

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)
18 changes: 18 additions & 0 deletions Free/foldFree
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
let Monad =
https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type

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))

@sellout sellout Jan 10, 2019

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

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

This should probably look similar to the Free/retract one I proposed.

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)
→ λ(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)

@sellout sellout Jan 10, 2019

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

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

And this can be

  λ(f : Type → Type)
→ ../../Mu/functor (../../FreeF/Type f) (../../FreeF/bifunctor f)

@mstksg mstksg Jan 15, 2019

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

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

Trying this out with the alternative representation; this doesn't quite work because it requires Functor f. We can implement it directly using the FreeF implementation, but we just can't do it through Mu FreeF, unfortunately :(

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)
15 changes: 15 additions & 0 deletions Free/package.dhall
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
14 changes: 14 additions & 0 deletions Free/recursive
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
let FreeF = ./../FreeF/Type

in λ(f : Type → Type)
→ λ(a : Type)
→ { cata =
λ(b : Type)
→ λ(alg : ./../algebra (FreeF f a) 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))
}
: ./../Recursive/Type (./Type f a) (FreeF f a)

@sellout sellout Jan 10, 2019

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

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

This can be

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

15 changes: 15 additions & 0 deletions Free/retract
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
let Monad =
https://raw.githubusercontent.com/FormationAI/dhall-bhat/8afbcee6dfd092764df9e9456fe2a2650748dce2/Monad/Type

in λ ( f
: Type → Type
)
→ λ(a : Type)
→ λ(monad : Monad f)
→ let join =
( https://raw.githubusercontent.com/FormationAI/dhall-bhat/6f66fc588c9d49a662794a32b29962341c373eb4/Monad/package.dhall
Comment thread
mstksg marked this conversation as resolved.
Outdated
f
monad
).join

in λ(m : ./Type f a) → m (f a) (monad.pure a) (join a)

@sellout sellout Jan 10, 2019

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

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

  λ(f : Type → Type)
→ λ(monad : Monad f) -- note instance immediately after type
→ λ(a : Type)
→ ./recursive.cata
  a
  (  λ(free : ../../FreeF/Type f a (f a))
   → merge { Pure = monad.pure, Free = join } free)

and the merge would be cleaner if I ever got my changes into the spec, then it could be

→ ./recursive.cata (f a) (merge { Pure = monad.pure, Free = join })

@sellout sellout Jan 10, 2019

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

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

Basically, anything that applies m is going to instead do ./recursive.cata … merge

44 changes: 44 additions & 0 deletions Free/steppable
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)

@sellout sellout Jan 10, 2019

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

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

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

13 changes: 13 additions & 0 deletions Free/transformer
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
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 >
Comment thread
mstksg marked this conversation as resolved.
20 changes: 20 additions & 0 deletions FreeF/functor
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
Comment thread
mstksg marked this conversation as resolved.
Outdated