Readers
In the previous section you learned about the conceptual idea of monads. You learned
what they are, and saw how some common types like IO
and Option
work as monads. Now in this
section, you will be looking at some other useful monads. In particular, the ReaderM
monad.
How to do Global Variables in Lean?
In Lean, your code is generally "pure", meaning functions can only interact with the arguments
passed to them. This effectively means you cannot have global variables. You can have global
definitions, but these are fixed at compile time. If some user behavior might change them, you would have
to wrap them in the IO
monad, which means they can't be used from pure code.
Consider this example. Here, you want to have an Environment
containing different parameters as a
global variable. However, you want to load these parameters from the process environment variables,
which requires the IO
monad.
structureEnvironment whereEnvironment: Typepath :path: Environment → StringStringString: Typehome :home: Environment → StringStringString: Typeuser :user: Environment → StringString derivingString: TypeRepr defRepr: Type u → Type ugetEnvDefault (getEnvDefault: String → IO Stringname :name: StringString):String: TypeIOIO: Type → TypeString := do letString: Typeval? ←val?: Option StringIO.getEnvIO.getEnv: String → BaseIO (Option String)namename: Stringpure <| matchpure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f αval? with |val?: Option Stringnone =>none: {α : Type ?u.1769} → Option α"" |"": Stringsomesome: {α : Type ?u.1778} → α → Option αs =>s: Strings defs: StringloadEnv :loadEnv: IO EnvironmentIOIO: Type → TypeEnvironment := do letEnvironment: Typepath ←path: StringgetEnvDefaultgetEnvDefault: String → IO String"PATH" let"PATH": Stringhome ←home: StringgetEnvDefaultgetEnvDefault: String → IO String"HOME" let"HOME": Stringuser ←user: StringgetEnvDefaultgetEnvDefault: String → IO String"USER""USER": Stringpure {pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f αpath,path: Stringhome,home: Stringuser } defuser: Stringfunc1 (func1: Environment → Floate :e: EnvironmentEnvironment) :Environment: TypeFloat := letFloat: Typel1 :=l1: Nate.e: Environmentpath.path: Environment → Stringlength letlength: String → Natl2 :=l2: Nate.e: Environmenthome.home: Environment → Stringlength *length: String → Nat2 let2: Natl3 :=l3: Nate.e: Environmentuser.user: Environment → Stringlength *length: String → Nat3 (3: Natl1 +l1: Natl2 +l2: Natl3).l3: NattoFloat *toFloat: Nat → Float2.1 def2.1: Floatfunc2 (func2: Environment → Natenv :env: EnvironmentEnvironment) :Environment: TypeNat :=Nat: Type2 + (2: Natfunc1func1: Environment → Floatenv).env: Environmentfloor.floor: Float → FloattoUInt32.toUInt32: Float → UInt32toNat deftoNat: UInt32 → Natfunc3 (func3: Environment → Stringenv :env: EnvironmentEnvironment) :Environment: TypeString :=String: Type"Result: " ++ ("Result: ": StringtoString (toString: {α : Type} → [self : ToString α] → α → Stringfunc2func2: Environment → Natenv)) defenv: Environmentmain :main: IO UnitIOIO: Type → TypeUnit := do letUnit: Typeenv ←env: EnvironmentloadEnv letloadEnv: IO Environmentstr :=str: Stringfunc3func3: Environment → Stringenvenv: EnvironmentIO.printlnIO.println: {α : Type} → [inst : ToString α] → α → IO Unitstrstr: Stringmain -- Result: 7538main: IO Unit
The only function actually using the environment is func1. However func1 is a pure function. This means it cannot directly call loadEnv, an impure function in the IO monad. This means the environment has to be passed through as a variable to the other functions, just so they can ultimately pass it to func1. In a language with global variables, you could save env as a global value in main. Then func1 could access it directly. There would be no need to have it as a parameter to func1, func2 and func3. In larger programs, these "pass-through" variables can cause a lot of headaches.
The Reader Solution
The ReaderM
monad solves this problem. It effectively creates a global read-only value of a
specified type. All functions within the monad can "read" the type. Let's look at how the ReaderM
monad changes the shape of this code. Now the functions no longer need to be given the
Environment
as an explicit parameter, as they can access it through the monad.
defreaderFunc1 :readerFunc1: ReaderM Environment FloatReaderMReaderM: Type → Type → TypeEnvironmentEnvironment: TypeFloat := do letFloat: Typeenv ←env: Environmentread letread: {ρ : outParam Type} → {m : Type → Type} → [self : MonadReader ρ m] → m ρl1 :=l1: Natenv.env: Environmentpath.path: Environment → Stringlength letlength: String → Natl2 :=l2: Natenv.env: Environmenthome.home: Environment → Stringlength *length: String → Nat2 let2: Natl3 :=l3: Natenv.env: Environmentuser.user: Environment → Stringlength *length: String → Nat3 return (3: Natl1 +l1: Natl2 +l2: Natl3).l3: NattoFloat *toFloat: Nat → Float2.1 def2.1: FloatreaderFunc2 :readerFunc2: ReaderM Environment NatReaderMReaderM: Type → Type → TypeEnvironmentEnvironment: TypeNat :=Nat: TypereaderFunc1 >>= (funreaderFunc1: ReaderM Environment Floatx => returnx: Float2 + (2: Natx.x: Floatfloor.floor: Float → FloattoUInt32.toUInt32: Float → UInt32toNat)) deftoNat: UInt32 → NatreaderFunc3 :readerFunc3: ReaderM Environment StringReaderMReaderM: Type → Type → TypeEnvironmentEnvironment: TypeString := do letString: Typex ←x: NatreaderFunc2 returnreaderFunc2: ReaderM Environment Nat"Result: " ++"Result: ": StringtoStringtoString: {α : Type} → [self : ToString α] → α → Stringx defx: Natmain2 :main2: IO UnitIOIO: Type → TypeUnit := do letUnit: Typeenv ←env: EnvironmentloadEnv letloadEnv: IO Environmentstr :=str: Id StringreaderFunc3.readerFunc3: ReaderM Environment Stringrunrun: {ρ : Type} → {m : Type → Type} → {α : Type} → ReaderT ρ m α → ρ → m αenvenv: EnvironmentIO.printlnIO.println: {α : Type} → [inst : ToString α] → α → IO Unitstrstr: Id Stringmain2 -- Result: 7538main2: IO Unit
The ReaderM
monad provides a run
method and it is the ReaderM
run method that takes the initial
Environment
context. So here you see main2
loads the environment as before, and establishes
the ReaderM
context by passing env
to the run
method.
Side note 1: The
return
statement used above also needs some explanation. Thereturn
statement in Lean is closely related topure
, but a little different. First the similarity is thatreturn
andpure
both lift a pure value up to the Monad type. Butreturn
is a keyword so you do not need to parenthesize the expression like you do when usingpure
. (Note: you can avoid parentheses when usingpure
by using the<|
operator like we did above in the initialgetEnvDefault
function). Furthermore,return
can also cause an earlyreturn
in a monadic function similar to how it can in an imperative language whilepure
cannot.
So technically if
return
is the last statement in a function it could be replaced withpure <|
, but one could argue thatreturn
is still a little easier for most folks to read, just so long as you understand thatreturn
is doing more than other languages, it is also wrapping pure values in the monadic container type.
Side note 2: If the function
readerFunc3
also took some explicit arguments then you would have to write(readerFunc3 args).run env
and this is a bit ugly, so Lean provides an infix operator|>
that eliminates those parentheses so you can writereaderFunc3 args |>.run env
and then you can chain multiple monadic actions like thism1 args1 |>.run args2 |>.run args3
and this is the recommended style. You will see this pattern used heavily in Lean code.
The let env ← read
expression in readerFunc1
unwraps the environment from the ReaderM
so we
can use it. Each type of monad might provide one or more extra functions like this, functions that
become available only when you are in the context of that monad.
Here the readerFunc2
function uses the bind
operator >>=
just to show you that there are bind
operations happening here. The readerFunc3
function uses the do
notation you learned about in
Monads which hides that bind operation and can make the code look cleaner.
So the expression let x ← readerFunc2
is also calling the bind
function under the covers,
so that you can access the unwrapped value x
needed for the toString x
conversion.
The important difference here to the earlier code is that readerFunc3
and readerFunc2
no longer
have an explicit Environment input parameter that needs to be passed along all the way to
readerFunc1
. Instead, the ReaderM
monad is taking care of that for you, which gives you the
illusion of something like global context where the context is now available to all functions that use
the ReaderM
monad.
The above code also introduces an important idea. Whenever you learn about a monad "X", there's
often (but not always) a run
function to execute that monad, and sometimes some additional
functions like read
that interact with the monad context.
You might be wondering, how does the context actually move through the ReaderM
monad? How can you
add an input argument to a function by modifying its return type? There is a special command in
Lean that will show you the reduced types:
ReaderMReaderM: Type → Type → TypeEnvironmentEnvironment: TypeString -- Environment → StringString: Type
And you can see here that this type is actually a function! It's a function that takes an
Environment
as input and returns a String
.
Now, remember in Lean that a function that takes an argument of type Nat
and returns a String
like def f (a : Nat) : String
is the same as this function def f : Nat → String
. These are
exactly equal as types. Well this is being used by the ReaderM
Monad to add an input argument to
all the functions that use the ReaderM
monad and this is why main
is able to start things off by
simply passing that new input argument in readerFunc3.run env
. So now that you know the implementation
details of the ReaderM
monad you can see that what it is doing looks very much like the original
code we wrote at the beginning of this section, only it's taking a lot of the tedious work off your
plate and it is creating a nice clean separation between what your pure functions are doing, and the
global context idea that the ReaderM
adds.
withReader
One ReaderM
function can call another with a modified version of the ReaderM
context. You can
use the withReader
function from the MonadWithReader
type class to do this:
def readerFunc3WithReader: ReaderM Environment String
readerFunc3WithReader : ReaderM: Type → Type → Type
ReaderM Environment: Type
Environment String: Type
String := do
let x: Nat
x ← withReader: {ρ : outParam Type} → {m : Type → Type} → [self : MonadWithReader ρ m] → {α : Type} → (ρ → ρ) → m α → m α
withReader (λ env: Environment
env => { env: Environment
env with user := "new user": String
"new user" }) readerFunc2: ReaderM Environment Nat
readerFunc2
return "Result: ": String
"Result: " ++ toString: {α : Type} → [self : ToString α] → α → String
toString x: Nat
x
Here we changed the user
in the Environment
context to "new user" and then we passed that
modified context to readerFunc2
.
So withReader f m
executes monad m
in the ReaderM
context modified by f
.
Handy shortcut with (← e)
If you use the operator ←
in a let expression and the variable is only used once you can
eliminate the let expression and place the ←
operator in parentheses like this
call to loadEnv:
def main3: IO Unit
main3 : IO: Type → Type
IO Unit: Type
Unit := do
let str: Id String
str := readerFunc3: ReaderM Environment String
readerFunc3 (← loadEnv): Environment
(← loadEnv: IO Environment
loadEnv(← loadEnv): Environment
)
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println str: Id String
str
Conclusion
It might not seem like much has been accomplished with this ReaderM Environment
monad, but you will
find that in larger code bases, with many different types of monads all composed together this
greatly cleans up the code. Monads provide a beautiful functional way of managing cross-cutting
concerns that would otherwise make your code very messy.
Having this control over the inherited ReaderM
context via withReader
is actually very useful
and something that is quite messy if you try and do this sort of thing with global variables, saving
the old value, setting the new one, calling the function, then restoring the old value, making sure
you do that in a try/finally block and so on. The ReaderM
design pattern avoids that mess
entirely.
Now it's time to move on to StateM Monad which is like a ReaderM
that is
also updatable.