Functional Programming in Lean

4. Monads

In C# and Kotlin, the ?. operator is a way to look up a property or call a method on a potentially-null value. If the receiver is null, the whole expression is null. Otherwise, the underlying non-null value receives the call. Uses of ?. can be chained, in which case the first null result terminates the chain of lookups. Chaining null-checks like this is much more convenient than writing and maintaining deeply nested ifs.

Similarly, exceptions are significantly more convenient than manually checking and propagating error codes. At the same time, logging is easiest to accomplish by having a dedicated logging framework, rather than having each function return both its log results and its return value. Chained null checks and exceptions typically require language designers to anticipate this use case, while logging frameworks typically make use of side effects to decouple code that logs from the accumulation of the logs.

  1. 4.1. One API, Many Applications
  2. 4.2. The Monad Type Class
  3. 4.3. Example: Arithmetic in Monads
  4. 4.4. do-Notation for Monads
  5. 4.5. The IO Monad
  6. 4.6. Additional Conveniences
  7. 4.7. Summary