lean-effects/Tutorial.lean at main · paulcadman/lean-effects · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
import Effects

open scoped Container


namespace Tutorial

variable
  {m}
  [Monad m]
  {effs : List Effect}

namespace StateExample
  namespace Effects

    open State

    def tick [State Nat ∈ effs] : Prog effs Unit := do
      let n ← get
      put (n + 1)

    def tickTwice [State Nat ∈ effs] : Prog effs Nat := do
      tick
      tick
      get

    def tickTwiceResult : Nat :=
      tickTwice
      |> State.eval 0
      |> Prog.run

  end Effects

  namespace MTL

    def tick [MonadState Nat m] : m Unit := do
      modify (fun n => n + 1)

    def tickTwice [MonadState Nat m] : m Nat := do
      tick
      tick
      get

    def tickTwiceResult : Nat :=
      (tickTwice : StateM Nat Nat).run' 0

    end MTL

  #guard Effects.tickTwiceResult = 2
  #guard MTL.tickTwiceResult = 2

end StateExample

namespace ExceptStateComposition

  namespace Effects

    open State
    open Exception

    def decr
      [State Int ∈ effs]
      [Exception Unit ∈ effs]
      : Prog effs Unit := do
        let x ← get
        if x > (0 : Int) then
          put (x - 1)
        else
          throwE ()

    def tripleDecr
      [State Int ∈ effs]
      [Exception Unit ∈ effs]
      : Prog effs Unit := do
        decr
        catchE (do decr; decr) pure

    def stateThenExcept : Except Unit (Int × Unit) :=
      tripleDecr
      |> State.run 2
      |> Exception.run (E := Unit)
      |> Prog.run

    def exceptThenState : Int × Except Unit Unit :=
      tripleDecr
      |> Exception.run (E := Unit)
      |> State.run 2
      |> Prog.run

  end Effects

  namespace MTL
    def decr [MonadStateOf Int m] [MonadExcept Unit m] : m Unit := do
      let x ← get
      if x > 0 then
        set (x - 1)
      else
        throw ()

    def tripleDecr [MonadStateOf Int m] [MonadExcept Unit m] : m Unit := do
      decr
      tryCatch (do decr; decr) (fun _ => pure ())

    def stateThenExcept : Except Unit (Unit × Int) :=
      (tripleDecr : StateT Int (Except Unit) Unit).run 2

    def exceptThenState : Except Unit Unit × Int :=
      (tripleDecr : ExceptT Unit (StateM Int) Unit).run 2

  end MTL


  #guard MTL.stateThenExcept = .ok ((), 1)
  #guard Effects.stateThenExcept = .ok (1, ())

  #guard MTL.exceptThenState = (.ok (), 0)
  #guard Effects.exceptThenState = (0, .ok ())

end ExceptStateComposition

namespace ChooseWithStateExample

  namespace Effects

  open State
  open NonDet

  def chooseWithState
    [NonDet ∈ effs]
    [State Nat ∈ effs] :
    Prog effs Nat := do
      let n ← get
      choice
        (pure n)
        (do
          put (n + 1)
          get)

  def localState : List (Nat × Nat) :=
    chooseWithState
    |> State.run 0
    |> NonDet.runList
    |> Prog.run

  def globalState : Nat × List Nat :=
    chooseWithState
    |> NonDet.runList
    |> State.run 0
    |> Prog.run

  end Effects

  #guard Effects.localState = [(0, 0), (1, 1)]
  #guard Effects.globalState = (1, [0, 1])

end ChooseWithStateExample

end Tutorial