max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

style(init/category): consistently use Greek letters for type parameters (well, except for m)

Browse source
This commit is contained in:
Sebastian Ullrich 2018-03-05 17:21:09 +01:00 • committed by Leonardo de Moura
parent c56606d06a
commit 1bd73f191f
3 changed files with 49 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/init/category/cont.lean
View file

@ -10,33 +10,33 @@ prelude
import init.category.alternative init.category.combinators init.category.lift
universes u v w
structure cont_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
(run : (α → m r) → m r)
structure cont_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
(run : (α → m ρ) → m ρ)
attribute [pp_using_anonymous_constructor] cont_t
class monad_cont (m : Type u → Type v) :=
(call_cc {α β : Type u} : ((α → m β) → m α) → m α)
@[reducible] def cont (r α : Type u) : Type u := cont_t r id α
@[reducible] def cont (ρ α : Type u) : Type u := cont_t ρ id α
namespace cont_t
section
parameters {r : Type u} {m : Type u → Type v}
parameters {ρ : Type u} {m : Type u → Type v}
protected def pure {α : Type u} (a : α) : cont_t r m α :=
protected def pure {α : Type u} (a : α) : cont_t ρ m α :=
⟨λ cc, cc a⟩
protected def bind {α β : Type u} (ma : cont_t r m α) (f : α → cont_t r m β) : cont_t r m β :=
protected def bind {α β : Type u} (ma : cont_t ρ m α) (f : α → cont_t ρ m β) : cont_t ρ m β :=
⟨λ cc, ma.run (λ a, (f a).run cc)⟩
instance : monad (cont_t r m) :=
instance : monad (cont_t ρ m) :=
{ pure := @pure, bind := @bind }
protected def call_cc {α β : Type u} (f : (α → cont_t r m β) → cont_t r m α) : cont_t r m α :=
protected def call_cc {α β : Type u} (f : (α → cont_t ρ m β) → cont_t ρ m α) : cont_t ρ m α :=
⟨λ cc, (f (λ a, ⟨λ _, cc a⟩)).run cc⟩
instance : monad_cont (cont_t r m) :=
instance : monad_cont (cont_t ρ m) :=
⟨@call_cc⟩
end
end cont_t

36
library/init/category/lawful.lean
View file

@ -173,51 +173,51 @@ instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (ε : Type u) : i
namespace reader_t
section
variable {r : Type u}
variable {ρ : Type u}
variable {m : Type u → Type v}
variables {α β : Type u}
variables (x : reader_t r m α) (cfg : r)
variables (x : reader_t ρ m α) (r : ρ)
lemma ext {x x' : reader_t r m α} (h : ∀ cfg, x.run cfg = x'.run cfg) : x = x' :=
lemma ext {x x' : reader_t ρ m α} (h : ∀ r, x.run r = x'.run r) : x = x' :=
by cases x; cases x'; simp [show x = x', from funext h]
variable [monad m]
@[simp] lemma run_pure (a) : (pure a : reader_t r m α).run cfg = pure a := rfl
@[simp] lemma run_bind (f : α → reader_t r m β) :
(x >>= f).run cfg = x.run cfg >>= λ a, (f a).run cfg := rfl
@[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run cfg = f <$> x.run cfg :=
@[simp] lemma run_pure (a) : (pure a : reader_t ρ m α).run r = pure a := rfl
@[simp] lemma run_bind (f : α → reader_t ρ m β) :
(x >>= f).run r = x.run r >>= λ a, (f a).run r := rfl
@[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run r = f <$> x.run r :=
by rw ←bind_pure_comp_eq_map m; refl
@[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) :
(monad_lift x : reader_t r m α).run cfg = (monad_lift x : m α) := rfl
(monad_lift x : reader_t ρ m α).run r = (monad_lift x : m α) := rfl
@[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) :
(monad_map @f x : reader_t r m' α).run cfg = monad_map @f (x.run cfg) := rfl
@[simp] lemma run_read : (reader_t.read : reader_t r m r).run cfg = pure cfg := rfl
(monad_map @f x : reader_t ρ m' α).run r = monad_map @f (x.run r) := rfl
@[simp] lemma run_read : (reader_t.read : reader_t ρ m ρ).run r = pure r := rfl
end
end reader_t
instance (r : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (reader_t r m) :=
instance (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (reader_t ρ m) :=
{ id_map := by intros; apply reader_t.ext; intro; simp,
pure_bind := by intros; apply reader_t.ext; intro; simp,
bind_assoc := by intros; apply reader_t.ext; intro; simp [bind_assoc] }
namespace cont_t
variable {r : Type u}
variable {ρ : Type u}
variable {m : Type u → Type v}
variables {α β : Type u}
variables (x : cont_t r m α)
variables (x : cont_t ρ m α)
lemma ext {x x' : cont_t r m α} (h : ∀ cc, x.run cc = x'.run cc) : x = x' :=
lemma ext {x x' : cont_t ρ m α} (h : ∀ cc, x.run cc = x'.run cc) : x = x' :=
by cases x; cases x'; simp [show x = x', from funext h]
@[simp] lemma run_pure (a : α) (cc : α → m r) : (pure a : cont_t r m α).run cc = cc a := rfl
@[simp] lemma run_bind (f : α → cont_t r m β) (cc : β → m r) :
@[simp] lemma run_pure (a : α) (cc : α → m ρ) : (pure a : cont_t ρ m α).run cc = cc a := rfl
@[simp] lemma run_bind (f : α → cont_t ρ m β) (cc : β → m ρ) :
(x >>= f).run cc = x.run (λ a, (f a).run cc) := rfl
@[simp] lemma run_map (f : α → β) (cc : β → m r) : (f <$> x).run cc = x.run (cc ∘ f) := rfl
@[simp] lemma run_map (f : α → β) (cc : β → m ρ) : (f <$> x).run cc = x.run (cc ∘ f) := rfl
end cont_t
instance (r : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (cont_t r m) :=
instance (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (cont_t ρ m) :=
{ id_map := by intros; apply cont_t.ext; simp,
pure_bind := by intros; apply cont_t.ext; simp,
bind_assoc := by intros; apply cont_t.ext; simp }

44
library/init/category/reader.lean
View file

@ -10,38 +10,38 @@ prelude
import init.category.lift init.category.id
universes u v w
structure reader_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
(run : r → m α)
structure reader_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
(run : ρ → m α)
@[reducible] def reader (r : Type u) := reader_t r id
@[reducible] def reader (ρ : Type u) := reader_t ρ id
attribute [pp_using_anonymous_constructor] reader_t
namespace reader_t
section
variable {r : Type u}
variable {ρ : Type u}
variable {m : Type u → Type v}
variable [monad m]
variables {α β : Type u}
protected def read : reader_t r m r :=
protected def read : reader_t ρ m ρ :=
⟨pure⟩
protected def pure (a : α) : reader_t r m α :=
protected def pure (a : α) : reader_t ρ m α :=
⟨λ r, pure a⟩
protected def bind (x : reader_t r m α) (f : α → reader_t r m β) : reader_t r m β :=
protected def bind (x : reader_t ρ m α) (f : α → reader_t ρ m β) : reader_t ρ m β :=
⟨λ r, do a ← x.run r,
(f a).run r⟩
instance : monad (reader_t r m) :=
instance : monad (reader_t ρ m) :=
{ pure := @reader_t.pure _ _ _, bind := @reader_t.bind _ _ _ }
protected def lift (a : m α) : reader_t r m α :=
protected def lift (a : m α) : reader_t ρ m α :=
⟨λ r, a⟩
instance (m) [monad m] : has_monad_lift m (reader_t r m) :=
⟨@reader_t.lift r m _⟩
instance (m) [monad m] : has_monad_lift m (reader_t ρ m) :=
⟨@reader_t.lift ρ m _⟩
protected def monad_map {r m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : reader_t r m α → reader_t r m' α :=
λ x, ⟨λ r, f (x.run r)⟩
@ -52,31 +52,31 @@ end
end reader_t
/-- A specialization of `monad_lift` to `reader_t` that allows `r` to be inferred. -/
class monad_reader_lift (r : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
[has_lift : has_monad_lift_t (reader_t r m) n]
/-- A specialization of `monad_lift` to `reader_t` that allows `ρ` to be inferred. -/
class monad_reader_lift (ρ : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
[has_lift : has_monad_lift_t (reader_t ρ m) n]
attribute [instance] monad_reader_lift.mk
local attribute [instance] monad_reader_lift.has_lift
def monad_reader_lift.read {r : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_reader_lift r m n] : n r :=
@monad_lift _ _ _ _ (reader_t.read : reader_t r m _)
def monad_reader_lift.read {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_reader_lift ρ m n] : n ρ :=
@monad_lift _ _ _ _ (reader_t.read : reader_t ρ m _)
export monad_reader_lift (read)
/-- A specialization of `monad_map` to `reader_t` that allows `r` to be inferred. -/
class monad_reader_functor (r r' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
[functor {} : monad_functor_t (reader_t r m) (reader_t r' m) n n']
class monad_reader_functor (ρ ρ' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
[functor {} : monad_functor_t (reader_t ρ m) (reader_t ρ' m) n n']
attribute [instance] monad_reader_functor.mk
local attribute [instance] monad_reader_functor.functor
def with_reader_t {r r' m} [monad m] {α} (f : r' → r) : reader_t r m α → reader_t r' m α :=
def with_reader_t {ρ ρ' m} [monad m] {α} (f : ρ' → ρ) : reader_t ρ m α → reader_t ρ' m α :=
λ x, ⟨λ r, x.run (f r)⟩
def with_reader {r r'} {m n n'} [monad m] [monad_reader_functor r r' m n n'] {α : Type u} (f : r' → r) : n α → n' α :=
monad_map $ λ α, (with_reader_t f : reader_t r m α → reader_t r' m α)
def with_reader {ρ ρ'} {m n n'} [monad m] [monad_reader_functor ρ ρ' m n n'] {α : Type u} (f : ρ' → ρ) : n α → n' α :=
monad_map $ λ α, (with_reader_t f : reader_t ρ m α → reader_t ρ' m α)
instance (r : Type u) (m out) [monad_run out m] : monad_run (λ α, r → out α) (reader_t r m) :=
instance (ρ : Type u) (m out) [monad_run out m] : monad_run (λ α, ρ → out α) (reader_t ρ m) :=
⟨λ α x, run ∘ x.run, λ α a, reader_t.mk (unrun ∘ a)⟩