From dc6e48a6d632053047fc34e68d0b39a208d78d60 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 10 Apr 2024 21:55:30 +1000 Subject: [PATCH 1/3] doccs: add doc-string for LawfulMonad/Applicative --- src/Init/Control/Lawful/Basic.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index aeeec3b42282..598d93f117ed 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -12,6 +12,11 @@ open Function @[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x := rfl +/-- +The `Functor` typeclass only contains the operations of a functor. +`LawfulFunctor` further asserts that these operations satisfy the laws of a functor, +including the preservation of the identity and composition laws. +-/ class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where map_const : (Functor.mapConst : α → f β → f α) = Functor.map ∘ const β id_map (x : f α) : id <$> x = x @@ -24,6 +29,10 @@ attribute [simp] id_map @[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x := id_map x +/-- +The `Applicative` typeclass only contains the operations of an applicative functor. +`LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor. +-/ class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop where seqLeft_eq (x : f α) (y : f β) : x <* y = const β <$> x <*> y seqRight_eq (x : f α) (y : f β) : x *> y = const α id <$> x <*> y @@ -42,6 +51,11 @@ attribute [simp] map_pure seq_pure @[simp] theorem pure_id_seq [Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x := by simp [pure_seq] +/-- +The `Monad` typeclass only contains the operations of a monad. +`LawfulMonad` further asserts that these operations satisfy the laws of a monad, +including associativity and identity laws for `bind`. +-/ class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop where bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x bind_map {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = f <*> x From d4efda44a3be7a8af6835a56af389849aa97b3d3 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 10 Apr 2024 22:07:11 +1000 Subject: [PATCH 2/3] mk' --- src/Init/Control/Lawful/Basic.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index 598d93f117ed..0a2139ca261c 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -55,6 +55,8 @@ attribute [simp] map_pure seq_pure The `Monad` typeclass only contains the operations of a monad. `LawfulMonad` further asserts that these operations satisfy the laws of a monad, including associativity and identity laws for `bind`. + +`LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields. -/ class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop where bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x From 265de42909f9184d4fbb17fdb6808c8015d71b66 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 17 Apr 2024 14:39:15 +1000 Subject: [PATCH 3/3] Apply suggestions from code review Co-authored-by: Mario Carneiro --- src/Init/Control/Lawful/Basic.lean | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index 0a2139ca261c..3b31d69c4e53 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -15,7 +15,11 @@ open Function /-- The `Functor` typeclass only contains the operations of a functor. `LawfulFunctor` further asserts that these operations satisfy the laws of a functor, -including the preservation of the identity and composition laws. +including the preservation of the identity and composition laws: +``` +id <$> x = x +(h ∘ g) <$> x = h <$> g <$> x +``` -/ class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where map_const : (Functor.mapConst : α → f β → f α) = Functor.map ∘ const β @@ -31,7 +35,13 @@ attribute [simp] id_map /-- The `Applicative` typeclass only contains the operations of an applicative functor. -`LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor. +`LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor: +``` +pure id <*> v = v +pure (·∘·) <*> u <*> v <*> w = u <*> (v <*> w) +pure f <*> pure x = pure (f x) +u <*> pure y = pure (· y) <*> u +``` -/ class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop where seqLeft_eq (x : f α) (y : f β) : x <* y = const β <$> x <*> y @@ -54,7 +64,12 @@ attribute [simp] map_pure seq_pure /-- The `Monad` typeclass only contains the operations of a monad. `LawfulMonad` further asserts that these operations satisfy the laws of a monad, -including associativity and identity laws for `bind`. +including associativity and identity laws for `bind`: +``` +pure x >>= f = f x +x >>= pure = x +x >>= f >>= g = x >>= (fun x => f x >>= g) +``` `LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields. -/