Effects, monads and dependent programs
Move from Option.bind and desugared do notation through Except, functors, applicatives, IO, arrays and pure loop syntax. Then implement a lawful Monad, prove the StateM laws, combine state with errors through StateT, and use dependent indices to make invalid workflows impossible.
Sign in to track your progress
- Failure and sequencing3 lessons
- Option as a monadReplace nested matches with bind and short-circuit a two-step safe division.18 min
- Do notation, desugaredWrite the exact >>= chain behind two left-arrow bindings.18 min
- Errors that carry a reasonRefactor safeDiv from Option to Except while keeping the pipeline.20 min
- Abstraction ladder1 lesson
- Functor and ApplicativeMap one contextual value and combine two independent ones.20 min
- Execution and performance3 lessons
- IO and the proof boundaryRead a file, print a result, and understand why IO stays opaque.18 min
- Array, List and access patternsUse array literals, map and safe indexing, then prove size preservation.20 min
- Mutable syntax is a foldWrite let mut and for, then prove the loop equals its fold specification.22 min
- Lawful effects3 lessons
- Write a Monad and prove its lawsImplement a Trace monad and prove left identity, right identity and associativity.32 min
- StateM and a verified counterThread state through two actions and prove the state-monad laws.26 min
- Combine state and errors with StateTBuild a failing balance computation and reason about transformer order.26 min
- Dependent programs1 lesson
- Make invalid workflows impossibleIndex commands by protocol state and prove typed composition laws.30 min