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.

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

doc: add documentation on monads #1505

Merged
merged 83 commits into from Sep 5, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
83 commits
Select commit Hold shift + click to select a range
31652d1
doc: add documentation on functors.
lovettchris Aug 24, 2022
837007e
fix: make comments green
lovettchris Aug 24, 2022
c5efc74
minor tweaks
lovettchris Aug 24, 2022
10b8697
doc: add section on Applicatives.
lovettchris Aug 24, 2022
262cdf4
doc: add some more info on the laws from Mario.
lovettchris Aug 25, 2022
a3f2dc2
doc: add law list and move lazy evaluation up so the chapter ends pro…
lovettchris Aug 25, 2022
8d20458
doc: Add something on seqLeft and seqRight.
lovettchris Aug 25, 2022
6ff0389
doc: add section on monads.
lovettchris Aug 25, 2022
54bd2d8
doc: fix some typos.
lovettchris Aug 25, 2022
8244a6f
Merge branch 'master' into clovett/monads
lovettchris Aug 25, 2022
f34cb92
doc: switch to LeanInk for chaper on Monads.
lovettchris Aug 25, 2022
c0305aa
doc: remove old files.
lovettchris Aug 25, 2022
2f12cfa
doc: fix mdbook test errors.
lovettchris Aug 26, 2022
f12bdb5
doc: add part 4: readers
lovettchris Aug 26, 2022
aa2d338
doc: add section on State monads
lovettchris Aug 26, 2022
abb8cd9
doc: fix some typos and add some more details.
lovettchris Aug 26, 2022
b5eef78
doc: fix typos and add some CR feedback.
lovettchris Aug 26, 2022
b085448
doc: add Except monad section.
lovettchris Aug 26, 2022
b9e0a39
Merge branch 'master' into clovett/monads
lovettchris Aug 27, 2022
0e97bcf
doc: add info on monad transformers.
lovettchris Aug 27, 2022
aadcdfe
Delete transformers.lean.md
lovettchris Aug 27, 2022
a1f5ffc
doc: fix some typos.
lovettchris Aug 27, 2022
750d01b
doc: fix typos and move forward reference to monad lifting.
lovettchris Aug 27, 2022
698e7ab
Merge branch 'master' into clovett/monads
lovettchris Aug 27, 2022
7acbb0b
doc: Update `State` to `StateM`
lovettchris Aug 27, 2022
c21740e
doc: fix references to State to become StateM.
lovettchris Aug 27, 2022
cda9653
doc: generalize indexOf implementation.
lovettchris Aug 27, 2022
c4b420b
Merge branch 'master' into clovett/monads
lovettchris Aug 29, 2022
5c46dbf
doc: add chapter on monad laws and move "law" sections to this chapte…
lovettchris Aug 29, 2022
040d7bd
doc: add theorem
lovettchris Aug 29, 2022
81d08a7
Delete laws.lean.md
lovettchris Aug 29, 2022
570621a
doc: fix some typos.
lovettchris Aug 29, 2022
3a05ad5
Merge branch 'clovett/monads' of github.com:lovettchris/lean4 into cl…
lovettchris Aug 29, 2022
32565c3
doc: fix broken link.
lovettchris Aug 29, 2022
354ca2e
doc: fox typos.
lovettchris Aug 29, 2022
912bfa1
fix: language changed from "us" to "you".
lovettchris Aug 29, 2022
9e8f6f3
doc: fix code review comments.
lovettchris Aug 29, 2022
e8f12ff
doc: some word smithing
lovettchris Aug 30, 2022
cfc9d60
doc: some word smithing and sample simplification.
lovettchris Aug 30, 2022
77d4408
doc: add bad_option_map example.
lovettchris Aug 30, 2022
b26b057
doc: add side note on `return` statement and fix heading level consis…
lovettchris Aug 30, 2022
a4b7a80
Add `withReader` info
lovettchris Aug 30, 2022
d76bbad
Merge branch 'master' into clovett/monads
lovettchris Aug 30, 2022
f9fa862
doc: change language from us, our, your, we, we'll, we've to "you"
lovettchris Aug 30, 2022
e3a83ef
doc: add some forward links.
lovettchris Aug 30, 2022
ed117c1
doc: put spaces around colon in function arguments like "(x : List N…
lovettchris Aug 31, 2022
e53237c
doc:
lovettchris Aug 31, 2022
753cc27
doc: Remove info about Functor in other languages.
lovettchris Aug 31, 2022
ae2bafb
doc:
lovettchris Aug 31, 2022
6fed172
doc:
lovettchris Aug 31, 2022
8dd24bc
doc: fix withReader docs
lovettchris Aug 31, 2022
9b24f8d
doc: fix bug in explanation of `let x ← readerFunc2`
lovettchris Aug 31, 2022
6205665
doc: move hasSomeItemGreaterThan to Except.lean
lovettchris Aug 31, 2022
9e2398b
doc: fix "What transformation are you referring to"
lovettchris Aug 31, 2022
d5f1b4c
doc: fix typo.
lovettchris Aug 31, 2022
2695bc6
doc: add missing period.
lovettchris Aug 31, 2022
40da0e1
doc: fix validateList
lovettchris Aug 31, 2022
6fd6e59
doc: explain `λ` notation.
lovettchris Aug 31, 2022
11ceaf2
doc: reword the map, seq, bind comparison.
lovettchris Aug 31, 2022
8f76cf2
doc: fix some more 'reader state' to 'reader context' language
lovettchris Aug 31, 2022
2861199
doc: fix wrote statement about return only works in do blocks.
lovettchris Aug 31, 2022
a73dc17
doc: fix typo
lovettchris Aug 31, 2022
f126738
doc: improve language
lovettchris Aug 31, 2022
da9dac5
doc: fix typo
lovettchris Aug 31, 2022
53b84f7
Add info on what a do block is doing for you.
lovettchris Aug 31, 2022
aed5876
doc: define definitionally equal
lovettchris Aug 31, 2022
aa8a258
doc: make `readerFunc3.run env` canonical.
lovettchris Aug 31, 2022
2cec9ff
Merge branch 'clovett/monads' of github.com:lovettchris/lean4 into cl…
lovettchris Aug 31, 2022
e876200
doc: remove unnecessary parens.
lovettchris Aug 31, 2022
59039fc
doc: fix typos
lovettchris Aug 31, 2022
2ef1e40
doc: make List.map a bit more clear in the intro to Functors.
lovettchris Aug 31, 2022
ccc360f
doc: simplify readerFunc3WithReader
lovettchris Aug 31, 2022
a06b207
doc: switch to svg for diagram so it works better on dark themes.
lovettchris Aug 31, 2022
981fb67
doc: align nodes in diagram and convert to svg.
lovettchris Aug 31, 2022
da799e3
doc: simplify playGame using while true.
lovettchris Aug 31, 2022
4b9d738
doc: drop confusing statement about "definitionally equal"
lovettchris Aug 31, 2022
7d08ea0
doc: switch to `import Lean.Data.HashMap`
lovettchris Aug 31, 2022
371d434
doc: fix typo "operatoins"
lovettchris Aug 31, 2022
2aeaca9
doc: update diagram to add more info and polish the intro paragraphs …
lovettchris Sep 1, 2022
14bcffa
Merge branch 'master' into clovett/monads
lovettchris Sep 1, 2022
b7e6f73
doc: fix typo
lovettchris Sep 1, 2022
6230e37
doc: fix typo.
lovettchris Sep 2, 2022
e2e1afd
Merge branch 'master' into clovett/monads
lovettchris Sep 3, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
9 changes: 9 additions & 0 deletions doc/SUMMARY.md
Expand Up @@ -59,6 +59,15 @@
- [Thunk](./thunk.md)
- [Task and Thread](./task.md)
- [Functions](./functions.md)
- [Monads](./monads/intro.md)
- [Functor](./monads/functors.lean.md)
- [Applicative](./monads/applicatives.lean.md)
- [Monad](./monads/monads.lean.md)
- [Reader](./monads/readers.lean.md)
- [State](./monads/states.lean.md)
- [Except](./monads/except.lean.md)
- [Transformers](./monads/transformers.lean.md)
- [Laws](./monads/laws.lean.md)

# Other

Expand Down
55 changes: 55 additions & 0 deletions doc/images/monads.dgml
@@ -0,0 +1,55 @@
<?xml version="1.0" encoding="utf-8"?>
<DirectedGraph GraphDirection="TopToBottom" Layout="Sugiyama" Offset="-1264.63833333333,-729.52" ZoomLevel="1" xmlns="http://schemas.microsoft.com/vs/2009/dgml">
<Nodes>
<Node Id="Applicative" Bounds="-839,-412,78.3066666666667,25.96" UseManualLocation="True" />
<Node Id="Bind" Bounds="-703,-412.990048779297,50,25.96" UseManualLocation="True" />
<Node Id="Except" Category="concrete" Bounds="-631,-238,54.5166666666667,25.96" UseManualLocation="True" />
<Node Id="Functor" Bounds="-890.021657986111,-509,60.2533333333333,25.96" UseManualLocation="True" />
<Node Id="List" Category="concrete" Bounds="-922,-412,50,25.96" UseManualLocation="True" />
<Node Id="Monad" Bounds="-765,-339,57.77,25.96" UseManualLocation="True" />
<Node Id="Option" Category="concrete" Bounds="-903,-238,56.8933333333333,25.96" UseManualLocation="True" />
<Node Id="Pure" Bounds="-799,-509,50,25.96" UseManualLocation="True" />
<Node Id="ReaderM" Category="concrete" Bounds="-816,-238,67.5033333333333,25.96" UseManualLocation="True" />
<Node Id="Seq" Bounds="-719,-509,50,25.96" UseManualLocation="True" />
<Node Id="SeqLeft" Bounds="-639,-509,59.4666666666667,25.96" UseManualLocation="True" />
<Node Id="SeqRight" Bounds="-544,-509,67.7233333333333,25.96" UseManualLocation="True" />
<Node Id="StateM" Category="concrete" Bounds="-718.358888888889,-238,57.28,25.96" UseManualLocation="True" />
</Nodes>
<Links>
<Link Source="Applicative" Target="Functor" Bounds="-847.12242702921,-475.387638592472,39.2404278471513,63.3876385924717" />
<Link Source="Applicative" Target="Pure" Bounds="-796.388009621993,-474.343439288465,16.6120628262117,62.3434392884653" />
<Link Source="Applicative" Target="Seq" Bounds="-785.682854982818,-476.959367842732,70.8838407724442,64.9593678427323" />
<Link Source="Applicative" Target="SeqLeft" Bounds="-774.344312027491,-478.957606209781,131.554439087217,66.9576062097807" />
<Link Source="Applicative" Target="SeqRight" Bounds="-762.225406557428,-481.91850535998,209.970366938847,70.3021737715571" />
<Link Source="Except" Target="Monad" Bounds="-711.95378637201,-307.579654923495,91.1658051838909,69.5796549234947" />
<Link Source="List" Target="Functor" Bounds="-892.034814302334,-474.634018472681,23.9591319497622,62.6340184726814" />
<Link Source="Monad" Target="Applicative" Bounds="-782.595654197137,-379.260216894652,35.1486400418858,40.2602168946518" />
<Link Source="Monad" Target="Bind" Bounds="-725.919943874952,-379.952252619104,32.1656790368972,40.9522526191042" />
<Link Source="Option" Target="Monad" Bounds="-856.761951485149,-307.735551794831,95.5848867777901,69.7355517948313" />
<Link Source="ReaderM" Target="Monad" Bounds="-776.319514851485,-304.853562563497,30.5364127352738,66.8535625634966" />
<Link Source="StateM" Target="Monad" Bounds="-726.395530552052,-304.861622913356,30.7140523342301,66.8616229133556" />
</Links>
<Categories>
<Category Id="concrete" />
</Categories>
<Properties>
<Property Id="Bounds" DataType="System.Windows.Rect" />
<Property Id="Expression" DataType="System.String" />
<Property Id="GraphDirection" DataType="Microsoft.VisualStudio.Diagrams.Layout.LayoutOrientation" />
<Property Id="GroupLabel" DataType="System.String" />
<Property Id="IsEnabled" DataType="System.Boolean" />
<Property Id="Layout" DataType="System.String" />
<Property Id="Offset" DataType="System.String" />
<Property Id="TargetType" DataType="System.Type" />
<Property Id="UseManualLocation" DataType="System.Boolean" />
<Property Id="Value" DataType="System.String" />
<Property Id="ValueLabel" DataType="System.String" />
<Property Id="ZoomLevel" DataType="System.String" />
</Properties>
<Styles>
<Style TargetType="Node" GroupLabel="concrete" ValueLabel="True">
<Condition Expression="HasCategory('concrete')" />
<Setter Property="Background" Value="#FF91E7ED" />
</Style>
</Styles>
</DirectedGraph>
106 changes: 106 additions & 0 deletions doc/images/monads.svg
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
1 change: 1 addition & 0 deletions doc/monads/.gitignore
@@ -0,0 +1 @@
*.lean.md