maybe_t

maybe_t.lean

universes u v w

structure maybe_t (m : Type u → Type v) (α : Type u) :=
(run : Π {β : Type u}, (α → m β) → (unit → m β) → m β)

section
variables {m : Type u → Type v} {α β : Type u}

def maybe_t.return (a : α) : maybe_t m α :=
⟨λ _ k₁ k₂, k₁ a⟩

def maybe_t.bind (x : maybe_t m α) (f : α → maybe_t m β) : maybe_t m β :=
⟨λ _ k₁ k₂, x.run (λ a, (f a).run k₁ k₂) k₂⟩

def maybe_t.fail : maybe_t m α :=
⟨λ _ k₁ k₂, k₂ ()⟩

instance (m : Type u → Type v) : monad (maybe_t m) :=
{ pure := @maybe_t.return m,
  bind := @maybe_t.bind m }

instance (m : Type u → Type v) : is_lawful_functor (maybe_t m) :=
{ id_map   := begin intros, simp [id, functor.map, maybe_t.return, maybe_t.bind], cases x, refl end,
  comp_map := begin intros, simp [functor.map, function.comp, maybe_t.bind, maybe_t.return] end 
}

instance (m : Type u → Type v) : is_lawful_monad (maybe_t m) :=
{ pure_bind  := begin intros, simp [has_bind.bind, pure, maybe_t.return, maybe_t.bind], cases (f x), refl end,
  bind_assoc := begin intros, simp [has_bind.bind, maybe_t.bind] end
}

def maybe_t.orelse (x y : maybe_t m α) : maybe_t m α :=
⟨λ _ k₁ k₂, x.run k₁ (λ _, y.run k₁ k₂)⟩

end