Graded Monads

Type classes for functors, applicatives, and monads indexed by a grade. The raw versions require only Mul and One; the Lawful* classes require a Monoid.

@[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 GradedFunctor {G : Type} (f : GradedType G) : Type 1

Graded functor.

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

class GradedApplicative {G : Type} [One G] [Mul G] (f : GradedType G) extends GradedFunctor 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 GradedMonad {G : Type} [One G] [Mul G] (m : GradedType G) extends GradedApplicative 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) β

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} [GradedFunctor 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

@[reducible, inline]

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

gconst with the arguments flipped.

Equations

• x $>ᵍ b = 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_$>ᵍ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " $>ᵍ ") (Lean.ParserDescr.cat `term 101))

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))

class LawfulGradedFunctor {G : Type} [Monoid G] (f : GradedType G) [GradedFunctor 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 LawfulGradedApplicative {G : Type} [Monoid G] (f : GradedType G) [GradedApplicative f] extends LawfulGradedFunctor 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 LawfulGradedMonad {G : Type} [Monoid G] (m : GradedType G) [GradedMonad m] extends LawfulGradedApplicative 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