Lawful monad experiments

Changes

1 changed files (+33/-0)

• monad.lean
  • @@ -1,3 +1,5 @@
    + import Mathlib + -- Need LawfulMonad to guarentee the monad laws hold def mapM [Monad m] (f : α → m β) : List α → m (List β) | [] => pure []
  • @@ -11,3 +13,34 @@ def mapM [Monad m] (f : α → m β) : List α → m (List β)
    #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)) + + + def Set.pure {α : Type} : α → Set α + | a => {a} + def Set.bind {α β : Type} : Set α → (α → Set β) → Set β + | A, f => {b | ∃a, a ∈ A ∧ b ∈ f a} + instance Set.LawfulMonad : LawfulMonad2 Set := + { pure := Set.pure + bind := Set.bind + pure_bind := by + intro α β a f + simp [Pure.pure, Bind.bind, Set.pure, Set.bind] + bind_pure := by + intro α ma + simp [Pure.pure, Bind.bind, Set.pure, Set.bind] + bind_assoc := by + intro α β γ f g ma + simp [Pure.pure, Bind.bind, Set.pure, Set.bind] + apply Set.ext + aesop }