Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156// Monad transformers -- the stack-building layer over any `Monad`.//// Opt-in like `init.foldable` (not re-exported from `lib.mo`). `StateT`,// `ResultT` and `OptionT` are here; `IdentityT`, `ReaderT`, and `WriterT`// are the intended rest, each to follow the same shape: a// `Functor`/`Applicative`/`Monad` instance over any underlying monad, plus// `run`/`lift` and the effect operations.//// Every instance here is `[Monad M]`-constrained: resolving e.g.// `Monad (StateT S M)` at a concrete call site recursively resolves// `Monad M` underneath it, so stacks resolve one level at a time down// to a base monad (`Id`, `IO`, ...). Because instance resolution is a// run-time step in Monad, `transformers_tests.mo` has to EXECUTE every// instance -- `check` alone cannot see a missing one. (The `bind` half// of the `StateT` instance was long unexercised, blamed on a// StateT-specific lowering bug; the real cause was the checker's// dictionary-resolution gap for `[Monad M]` dictionary arguments// resolved from a partially-applied spine, and `test_statet_bind` now// passes.)// Future transformers (WriterT) will need Monoid/Semigroup from foldable.// use lib::foldable {Monoid, Semigroup}/// State transformer: `StateT S M A = S -> M (Pair S A)` threads a state/// `S` through the underlying monad `M`.////// A single-constructor `type` rather than a `struct`, deliberately: a/// parameterized `struct`'s constructor does not generalize its type/// parameters on the Rust host (construction at `StateT.mk` fails with/// ``type mismatch: `StateT` vs. `((StateT ?) ?) ?` `` while pattern/// matching works), and no parameterized struct exists anywhere in the/// corpus to prove otherwise. The single-constructor `type` is the shape/// `examples/state_monad.mo` already uses; construction (`StateT.mk`),/// matching, and everything else are spelled identically.pub type StateT (S : Type) (M : Type -> Type) (A : Type) { mk (run : S -> M (Pair S A))}/// Run a `StateT` computation from an initial state, giving the final/// state paired with the result.pub def StateT.run (m : StateT S M A) (s : S) : M (Pair S A) := match m { StateT.mk r => r s }/// Evaluate the stateful computation, returning only the result.pub def StateT.eval [Monad M] {S : Type} {A : Type} (m : StateT S M A) (s : S) : M A := match m { StateT.mk r => Monad.bind (r s) (fn p => match p { Pair.pair _ a => Monad.pure a }) }/// Execute the stateful computation, returning only the final state.pub def StateT.exec [Monad M] {S : Type} {A : Type} (m : StateT S M A) (s : S) : M S := match m { StateT.mk r => Monad.bind (r s) (fn p => match p { Pair.pair st _ => Monad.pure st }) }/// Lift an underlying computation, leaving the state untouched.pub def StateT.lift [Monad M] {S : Type} {A : Type} (m : M A) : StateT S M A := StateT.mk (fn s => Monad.bind m (fn a => Monad.pure (Pair.pair s a)))/// Internal: unwrap a `Pair S A` and run the continuation in the new/// state. Extracted so the instance body stays single-line (the parser/// doesn't accept multi-line lambdas inside instance bodies); it is the/// `ResultT`/`OptionT` `bind_step` pattern exactly, and it carries no/// `[Monad M]` dictionary parameter of its own -- its body never/// references the class, so the call the instance body makes to it needs/// no dictionary argument (see `collect_def_constraints`, lang/scope.mo).def StateT.bind_step [Monad M] {S : Type} {A : Type} {B : Type} (f : A -> StateT S M B) (p : Pair S A) : M (Pair S B) := match p { Pair.pair s2 a => StateT.run (f a) s2 }/// The instance body references `Monad.bind` DIRECTLY (through the/// single-line lambda `StateT.mk`'s field needs), not through an/// extracted helper: the promoted method's own `[Monad M]` dictionary/// parameter (Phase 3) is what serves that reference (D5 forwarding),/// and a helper call in between is resolved against the call's own/// argument carriers -- abstract inside an instance body, so the/// variable-headed prelude bridge matches and the helper runs with the/// WRONG dictionary (the `driver exited -1` this file's own test/// history records). The `ResultT`/`OptionT` instances below, whose/// bodies already reference `Monad.bind` directly, are the green/// precedent for exactly this shape.pub instance [Monad M] Monad (StateT S M) { def pure (a : A) : StateT S M A := StateT.mk (fn s => Monad.pure (Pair.pair s a)) def bind (ma : StateT S M A) (f : A -> StateT S M B) : StateT S M B := StateT.mk (fn (s : S) => Monad.bind (StateT.run ma s) (StateT.bind_step f))}/// Result transformer: `ResultT E M A = M (Result E A)` short-circuits the/// underlying monad's sequencing on `Result.err`, the same way `IO (Result/// String A)` already does by hand everywhere in this codebase (`motes//// moose/src/client.mo`'s continuation chaining, for one) -- this gives/// that exact shape real `do`-notation instead.pub type ResultT (E : Type) (M : Type -> Type) (A : Type) { mk (run : M (Result E A))}pub def ResultT.run (m : ResultT E M A) : M (Result E A) := match m { ResultT.mk r => r }/// Lift an underlying computation that cannot itself fail.pub def ResultT.lift [Monad M] {E : Type} {A : Type} (m : M A) : ResultT E M A := ResultT.mk (Monad.bind m (fn a => Monad.pure (Result.ok a)))/// Internal: run the continuation only on `Result.ok`, short-circuiting/// `Result.err` straight through -- extracted for the same reason/// `StateT.bind_go` is (the parser doesn't accept a multi-line lambda/// inside an instance body).def ResultT.bind_step [Monad M] {E : Type} {A : Type} {B : Type} (f : A -> ResultT E M B) (r : Result E A) : M (Result E B) := match r { Result.ok a => ResultT.run (f a), Result.err e => Monad.pure (Result.err e) }pub instance [Monad M] Monad (ResultT E M) { def pure (a : A) : ResultT E M A := ResultT.mk (Monad.pure (Result.ok a)) def bind (ma : ResultT E M A) (f : A -> ResultT E M B) : ResultT E M B := ResultT.mk (Monad.bind (ResultT.run ma) (ResultT.bind_step f))}/// Option transformer: `OptionT M A = M (Option A)` short-circuits on/// `Option.none`, the `ResultT` shape with no error payload to carry.pub type OptionT (M : Type -> Type) (A : Type) { mk (run : M (Option A))}pub def OptionT.run (m : OptionT M A) : M (Option A) := match m { OptionT.mk r => r }/// Lift an underlying computation that always produces a value.pub def OptionT.lift [Monad M] {A : Type} (m : M A) : OptionT M A := OptionT.mk (Monad.bind m (fn a => Monad.pure (Option.some a)))def OptionT.bind_step [Monad M] {A : Type} {B : Type} (f : A -> OptionT M B) (o : Option A) : M (Option B) := match o { Option.some a => OptionT.run (f a), Option.none => Monad.pure Option.none }pub instance [Monad M] Monad (OptionT M) { def pure (a : A) : OptionT M A := OptionT.mk (Monad.pure (Option.some a)) def bind (ma : OptionT M A) (f : A -> OptionT M B) : OptionT M B := OptionT.mk (Monad.bind (OptionT.run ma) (OptionT.bind_step f))}