Graded Monads

Type classes for functors, applicatives, monads, and alternatives indexed by a monoidal grade. Composition multiplies grades via the monoid operation.

@[reducible, inline]

abbrev GradedType (G : Sort u_1) : Sort (max 2 u_1)

A type family indexed by a grade and a type.

Equations

• GradedType G = (G → Type → Type)

class GFunctor {G : Type} (f : GradedType G) : Type 1

Graded functor.

• gmap {i : G} {α β : Type} (h : α → β) : f i α → f i β

class GApplicative {G : Type} [Monoid G] (f : GradedType G) extends GFunctor f : Type 1

Graded applicative.

• gmap {i : G} {α β : Type} (h : α → β) : f i α → f i β
• gpure {α : Type} : α → f 1 α
• gseq {i j : G} {α β : Type} : f i (α → β) → (Unit → f j α) → f (i * j) β

class GMonad {G : Type} [Monoid G] (m : GradedType G) extends GApplicative m : Type 1

Graded monad.

• gmap {i : G} {α β : Type} (h : α → β) : m i α → m i β
• gpure {α : Type} : α → m 1 α
• gseq {i j : G} {α β : Type} : m i (α → β) → (Unit → m j α) → m (i * j) β
• gbind {i j : G} {α β : Type} : m i α → (α → m j β) → m (i * j) β

class GAlternative {G : Type} [Monoid G] [AddSemigroup G] [Zero G] (f : GradedType G) extends GApplicative f : Type 1

Graded alternative.

• gmap {i : G} {α β : Type} (h : α → β) : f i α → f i β
• gpure {α : Type} : α → f 1 α
• gseq {i j : G} {α β : Type} : f i (α → β) → (Unit → f j α) → f (i * j) β
• gempty {α : Type} : f 0 α
• gchoice {α : Type} {i j : G} : f i α → f j α → f (i + j) α

def gcast {G : Type} {f : GradedType G} {i j : G} {α : Type} (h : i = j) (x : f i α) : f j α

Cast the grade of a graded type

Equations

• gcast h x = h ▸ x

@[reducible, inline]

abbrev gconst {G : Type} {f : GradedType G} [GFunctor f] {i : G} {α β : Type} (b : β) (x : f i α) : f i β

Replace the result of a graded computation with a constant value.

Equations

• b <$ᵍ x = (fun (x : α) => b) <$>ᵍ x

def «term_<$>ᵍ_» : Lean.TrailingParserDescr

Equations

• «term_<$>ᵍ_» = Lean.ParserDescr.trailingNode `«term_<$>ᵍ_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <$>ᵍ ") (Lean.ParserDescr.cat `term 100))

def «term_<$ᵍ_» : Lean.TrailingParserDescr

Equations

• «term_<$ᵍ_» = Lean.ParserDescr.trailingNode `«term_<$ᵍ_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <$ᵍ ") (Lean.ParserDescr.cat `term 100))

def «term_<*>ᵍ_» : Lean.TrailingParserDescr

Equations

• «term_<*>ᵍ_» = Lean.ParserDescr.trailingNode `«term_<*>ᵍ_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <*>ᵍ ") (Lean.ParserDescr.cat `term 61))

def «term_>>=ᵍ_» : Lean.TrailingParserDescr

Equations

• «term_>>=ᵍ_» = Lean.ParserDescr.trailingNode `«term_>>=ᵍ_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >>=ᵍ ") (Lean.ParserDescr.cat `term 56))

def «term_<|>ᵍ_» : Lean.TrailingParserDescr

Equations

• «term_<|>ᵍ_» = Lean.ParserDescr.trailingNode `«term_<|>ᵍ_» 30 30 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <|>ᵍ ") (Lean.ParserDescr.cat `term 31))

class LawfulGFunctor {G : Type} (f : GradedType G) [GFunctor f] : Prop

• gmap_id {i : G} {α : Type} (x : f i α) : id <$>ᵍ x = x
• gmap_comp {i : G} {α β γ : Type} (g : β → γ) (h : α → β) (x : f i α) : (g ∘ h) <$>ᵍ x = g <$>ᵍ h <$>ᵍ x

class LawfulGApplicative {G : Type} [Monoid G] (f : GradedType G) [GApplicative f] extends LawfulGFunctor f : Prop

• gmap_id {i : G} {α : Type} (x : f i α) : id <$>ᵍ x = x
• gmap_comp {i : G} {α β γ : Type} (g : β → γ) (h : α → β) (x : f i α) : (g ∘ h) <$>ᵍ x = g <$>ᵍ h <$>ᵍ x
• gmap_gpure {α β : Type} (g : α → β) (x : α) : g <$>ᵍ gpure x = gpure (g x)
• gpure_gseq {i : G} {α β : Type} (g : α → β) (x : f i α) : (gpure g <*>ᵍ fun (x_1 : Unit) => x) ≍ g <$>ᵍ x
• gseq_gpure {i : G} {α β : Type} (u : f i (α → β)) (x : α) : (u <*>ᵍ fun (x_1 : Unit) => gpure x) ≍ (fun (x_1 : α → β) => x_1 x) <$>ᵍ u
• gseq_assoc {i j k : G} {α β γ : Type} (u : f i (β → γ)) (v : f j (α → β)) (w : f k α) : ((Function.comp <$>ᵍ u <*>ᵍ fun (x : Unit) => v) <*>ᵍ fun (x : Unit) => w) ≍ u <*>ᵍ fun (x : Unit) => v <*>ᵍ fun (x : Unit) => w

class LawfulGMonad {G : Type} [Monoid G] (m : GradedType G) [GMonad m] extends LawfulGApplicative m : Prop

• gmap_id {i : G} {α : Type} (x : m i α) : id <$>ᵍ x = x
• gmap_comp {i : G} {α β γ : Type} (g : β → γ) (h : α → β) (x : m i α) : (g ∘ h) <$>ᵍ x = g <$>ᵍ h <$>ᵍ x
• gmap_gpure {α β : Type} (g : α → β) (x : α) : g <$>ᵍ gpure x = gpure (g x)
• gpure_gseq {i : G} {α β : Type} (g : α → β) (x : m i α) : (gpure g <*>ᵍ fun (x_1 : Unit) => x) ≍ g <$>ᵍ x
• gseq_gpure {i : G} {α β : Type} (u : m i (α → β)) (x : α) : (u <*>ᵍ fun (x_1 : Unit) => gpure x) ≍ (fun (x_1 : α → β) => x_1 x) <$>ᵍ u
• gseq_assoc {i j k : G} {α β γ : Type} (u : m i (β → γ)) (v : m j (α → β)) (w : m k α) : ((Function.comp <$>ᵍ u <*>ᵍ fun (x : Unit) => v) <*>ᵍ fun (x : Unit) => w) ≍ u <*>ᵍ fun (x : Unit) => v <*>ᵍ fun (x : Unit) => w
• gpure_gbind {j : G} {α β : Type} (x : α) (f : α → m j β) : gpure x >>=ᵍ f ≍ f x
• gbind_gpure {i : G} {α : Type} (x : m i α) : x >>=ᵍ gpure ≍ x
• gbind_assoc {i j k : G} {α β γ : Type} (x : m i α) (f : α → m j β) (g : β → m k γ) : x >>=ᵍ f >>=ᵍ g ≍ x >>=ᵍ fun (a : α) => f a >>=ᵍ g

class LawfulGAlternative {G : Type} [Monoid G] [AddMonoid G] (f : GradedType G) [GAlternative f] extends LawfulGApplicative f : Prop

• gmap_id {i : G} {α : Type} (x : f i α) : id <$>ᵍ x = x
• gmap_comp {i : G} {α β γ : Type} (g : β → γ) (h : α → β) (x : f i α) : (g ∘ h) <$>ᵍ x = g <$>ᵍ h <$>ᵍ x
• gmap_gpure {α β : Type} (g : α → β) (x : α) : g <$>ᵍ gpure x = gpure (g x)
• gpure_gseq {i : G} {α β : Type} (g : α → β) (x : f i α) : (gpure g <*>ᵍ fun (x_1 : Unit) => x) ≍ g <$>ᵍ x
• gseq_gpure {i : G} {α β : Type} (u : f i (α → β)) (x : α) : (u <*>ᵍ fun (x_1 : Unit) => gpure x) ≍ (fun (x_1 : α → β) => x_1 x) <$>ᵍ u
• gseq_assoc {i j k : G} {α β γ : Type} (u : f i (β → γ)) (v : f j (α → β)) (w : f k α) : ((Function.comp <$>ᵍ u <*>ᵍ fun (x : Unit) => v) <*>ᵍ fun (x : Unit) => w) ≍ u <*>ᵍ fun (x : Unit) => v <*>ᵍ fun (x : Unit) => w
• gempty_gchoice {i : G} {α : Type} (x : f i α) : (gempty <|>ᵍ x) ≍ x
• gchoice_gempty {i : G} {α : Type} (x : f i α) : (x <|>ᵍ gempty) ≍ x
• gchoice_assoc {i j k : G} {α : Type} (x : f i α) (y : f j α) (z : f k α) : (x <|>ᵍ y <|>ᵍ z) ≍ (x <|>ᵍ (y <|>ᵍ z))

class LawfulGMonadPlus {G : Type} [Monoid G] [AddMonoid G] (m : GradedType G) [GAlternative m] [GMonad m] extends LawfulGAlternative m : Prop

• gmap_id {i : G} {α : Type} (x : m i α) : id <$>ᵍ x = x
• gmap_comp {i : G} {α β γ : Type} (g : β → γ) (h : α → β) (x : m i α) : (g ∘ h) <$>ᵍ x = g <$>ᵍ h <$>ᵍ x
• gmap_gpure {α β : Type} (g : α → β) (x : α) : g <$>ᵍ gpure x = gpure (g x)
• gpure_gseq {i : G} {α β : Type} (g : α → β) (x : m i α) : (gpure g <*>ᵍ fun (x_1 : Unit) => x) ≍ g <$>ᵍ x
• gseq_gpure {i : G} {α β : Type} (u : m i (α → β)) (x : α) : (u <*>ᵍ fun (x_1 : Unit) => gpure x) ≍ (fun (x_1 : α → β) => x_1 x) <$>ᵍ u
• gseq_assoc {i j k : G} {α β γ : Type} (u : m i (β → γ)) (v : m j (α → β)) (w : m k α) : ((Function.comp <$>ᵍ u <*>ᵍ fun (x : Unit) => v) <*>ᵍ fun (x : Unit) => w) ≍ u <*>ᵍ fun (x : Unit) => v <*>ᵍ fun (x : Unit) => w
• gempty_gchoice {i : G} {α : Type} (x : m i α) : (gempty <|>ᵍ x) ≍ x
• gchoice_gempty {i : G} {α : Type} (x : m i α) : (x <|>ᵍ gempty) ≍ x
• gchoice_assoc {i j k : G} {α : Type} (x : m i α) (y : m j α) (z : m k α) : (x <|>ᵍ y <|>ᵍ z) ≍ (x <|>ᵍ (y <|>ᵍ z))
• gempty_gbind {α β : Type} {i : G} {x : α → m i β} : gempty >>=ᵍ x ≍ gempty
• gbind_gempty {α β : Type} {i : G} {x : m i α} : (x >>=ᵍ fun (x : α) => gempty) ≍ gempty