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

doc(init/category/lift): expand docs and note similarities to layers package

Browse source
This commit is contained in:
Sebastian Ullrich 2018-03-06 16:34:37 +01:00 • committed by Leonardo de Moura
parent 36f623af42
commit 4c877cff07
1 changed files with 32 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
library/init/category/lift.lean
View file

@ -2,6 +2,11 @@
Copyright (c) 2016 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Sebastian Ullrich
Classy functions for lifting monadic actions of different shapes.
This theory is roughly modeled after the Haskell 'layers' package https://hackage.haskell.org/package/layers-0.1.
Please see https://hackage.haskell.org/package/layers-0.1/docs/Documentation-Layers-Overview.html for an exhaustive discussion of the different approaches to lift functions.
-/
prelude
import init.function init.coe
@ -9,19 +14,28 @@ import init.category.monad
universes u v w
/-- A function for lifting a computation from an inner monad to an outer monad.
Like [MonadTrans](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html),
but `n` does not have to be a monad transformer.
Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/
class has_monad_lift (m : Type u → Type v) (n : Type u → Type w) :=
(monad_lift : ∀ α, m α → n α)
(monad_lift {} : ∀ {α}, m α → n α)
/-- The reflexive-transitive closure of `has_monad_lift`.
`monad_lift` is used to transitively lift monadic computations such as `state_t.get` or `state_t.put s`.
Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/
class has_monad_lift_t (m : Type u → Type v) (n : Type u → Type w) :=
(monad_lift {} : ∀ {α}, m α → n α)
export has_monad_lift_t (monad_lift)
/-- A coercion that may reduce the need for explicit lifting.
Because of [limitations of the current coercion resolution](https://github.com/leanprover/lean/issues/1402), this definition is not marked as a global instance and should be marked locally instead. -/
@[reducible] def has_monad_lift_to_has_coe {m n} [has_monad_lift_t m n] {α} : has_coe (m α) (n α) :=
⟨monad_lift⟩
instance has_monad_lift_t_trans (m n o) [has_monad_lift n o] [has_monad_lift_t m n] : has_monad_lift_t m o :=
⟨λ α (ma : m α), has_monad_lift.monad_lift o α $ @monad_lift m n _ _ ma⟩
⟨λ α ma, has_monad_lift.monad_lift (monad_lift ma : n α)⟩
instance has_monad_lift_t_refl (m) : has_monad_lift_t m m :=
⟨λ α, id⟩
@ -30,21 +44,22 @@ instance has_monad_lift_t_refl (m) : has_monad_lift_t m m :=
/-- A functor in the category of monads. Can be used to lift monad-transforming functions.
Based on https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html,
but not restricted to monad transformers. -/
Based on pipes' [MFunctor](https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html),
but not restricted to monad transformers.
Alternatively, an implementation of [MonadTransFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor). -/
class monad_functor (m m' : Type u → Type v) (n n' : Type u → Type w) :=
(monad_map {} {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
/-- The reflexive-transitive closure of `monad_functor` instances. -/
/-- The reflexive-transitive closure of `monad_functor`.
`monad_map` is used to transitively lift monad morphisms such as `state_t.zoom`.
A generalization of [MonadLiftFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLiftFunctor), which can only lift endomorphisms (i.e. m = m', n = n'). -/
class monad_functor_t (m m' : Type u → Type v) (n n' : Type u → Type w) :=
(monad_map {} {α : Type u} : (∀ {α}, m α → m' α) → n α → n' α)
export monad_functor_t (monad_map)
def monad_map' {α : Type u} (m m' : Type u → Type v) (n n' : Type u → Type w) [monad_functor_t (λ (α : Type u), m α) (λ (α : Type u), m' punit) n (λ {α : Type u}, n' punit)] : (∀ {α}, m α → m' punit) → n α → n' punit :=
monad_map
instance monad_functor_t_trans (m m' n n' o o') [monad_functor n n' o o'] [monad_functor_t m m' n n'] : monad_functor_t m m' o o' :=
instance monad_functor_t_trans (m m' n n' o o') [monad_functor n n' o o'] [monad_functor_t m m' n n'] :
monad_functor_t m m' o o' :=
⟨λ α f, monad_functor.monad_map (λ α, (monad_map @f : n α → n' α))⟩
instance monad_functor_t_refl (m m') : monad_functor_t m m' m m' :=
@ -55,7 +70,14 @@ instance monad_functor_t_refl (m m') : monad_functor_t m m' m m' :=
/-- Run a monad stack to completion.
`run` should be the composition of the transformers' individual `run` functions.
`unrun` should be its inverse. -/
`unrun` should be its inverse.
This class mostly saves some typing when using highly nested monad stacks:
```
@[reducible] def my_monad := reader_t my_cfg $ state_t my_state $ except_t my_err id
-- def my_monad.run {α : Type} (x : my_monad α) (cfg : my_cfg) (st : my_state) := ((x.run cfg).run st).run
def my_monad.run {α : Type} (x : my_monad α) := monad_run.run x
```
-/
class monad_run (out : out_param $ Type u → Type v) (m : Type u → Type v) :=
(run {} {α : Type u} : m α → out α)
(unrun {} {α : Type u} : out α → m α)