Monads and effects
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.
Progress is kept in this browser until you sign in
- 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