1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44

import Mathlib

-- Need LawfulMonad to guarentee the monad laws hold
def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM f xs >>= fun tl =>
    pure (hd :: tl)


#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5]

#eval show IO Unit from IO.println "hello world"
#reduce show IO Unit from IO.println "hello world"


class LawfulMonad2 (m : Type → Type)
  extends Pure m, Bind m where
  pure_bind {α β : Type} (a : α) (f : α → m β) :
    (pure a >>= f) = f a
  bind_pure {α : Type} (ma : m α) :
    (ma >>= pure) = ma
  bind_assoc {α β γ : Type} (f : α → m β) (g : β → m γ)
    (ma : m α) :
    ((ma >>= f) >>= g) = (ma >>= (fun a => f a >>= g))


@[grind]
def Set.pure {α : Type} : α → Set α
  | a => {a}

@[grind]
def Set.bind {α β : Type} : Set α → (α → Set β) → Set β
  | A, f => {b | ∃a, a ∈ A ∧ b ∈ f a}

instance Set.LawfulMonad : LawfulMonad2 Set where
  pure := Set.pure
  bind := Set.bind
  pure_bind := by grind
  bind_pure := by grind
  bind_assoc := by
    simp only [bind, mem_setOf_eq]
    grind