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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118use std::test {}use lib::id {Id, Id.run}use lib::transformers {StateT, ResultT, OptionT}// StateT spike: the smallest shape that exercises everything the rest of// this module depends on -- a higher-kinded type parameter (`M : Type -> Type`)// on an inductive, a `[Monad M]`-constrained instance, and run-time recursive// dispatch of `Monad.pure`/`Monad.bind` on the underlying monad through the// instance body's variable `M` (concretized to `Id` at the call site).#[test]def test_statet_pure_run : Bool := let m : StateT I64 Id I64 := Monad.pure 42 in match Id.run (StateT.run m 0) { Pair.pair s a => (s == 0) && (a == 42) }// `test_statet_bind` was commented out here, blamed on `MatchTraversalMismatch`// triggered by `Monad.bind` immediately followed by a `Pair.pair` match in// the same `def`, and called "StateT-specific." That diagnosis was only half// right: splitting `Monad.bind`'s computation into its own top-level `def`// (the fix that resurrects `ResultT`/`OptionT`'s own bind tests below)// cleared the `MatchTraversalMismatch` here too. But it then exposed a// SECOND, separate failure: `eval error: value is not a constructor` at run// time, inside the `StateT` instance's own `bind`/`StateT.bind_step`// (`lib/transformers.mo`),// previously blamed on a real interpreter bug in `StateT`'s own `bind`.// That blame was wrong: the failure was the checker's dictionary-resolution// gap for instance calls whose `[Monad M]` dictionary argument resolves// from a partially-applied spine (`StateT I64 Id`), fixed by the// constraint-position work in `core_check_module.rs`/`core_check.rs` --// the split-`def` form below now passes.def statet_bind_result : StateT I64 Id I64 := let m : StateT I64 Id I64 := Monad.pure 10 in Monad.bind m (fn a => Monad.pure (a + 1))#[test]def test_statet_bind : Bool := match Id.run (StateT.run statet_bind_result 100) { Pair.pair s a => (s == 100) && (a == 11) }// ResultT/OptionT `bind`: a throwaway single-file probe (outside this mote,// its own tiny `#![mote {...}]`) run BEFORE writing these instances showed// `Monad.bind` dispatch followed immediately by a `Result.ok`/`err` or// `Option.some`/`none` match passing cleanly -- but that probe was// MISLEADING. Run for real, in THIS file (part of `init`'s own full// prelude context, much bigger than an isolated probe), the identical// `Monad.bind`-then-`match` shape reproduces the exact same// `MatchTraversalMismatch` StateT's own note describes. So the bug is not// "StateT-specific" as that note concluded -- it is sensitive to the// surrounding compilation context's size/shape, and a small standalone// probe is not a reliable predictor of the real target file. The fix that// *does* work, confirmed here: put `Monad.bind`'s own computation in its// own top-level `def`, so the `match` that reads the result is no longer// in the same `def` as the `bind` dispatch -- exactly the mitigation this// codebase already uses for Loom's indexed-monad do-blocks.def resultt_bind_result : ResultT String Id I64 := let m : ResultT String Id I64 := Monad.pure 10 in Monad.bind m (fn a => Monad.pure (a + 1))#[test]def test_resultt_pure_run : Bool := let m : ResultT String Id I64 := Monad.pure 42 in match Id.run (ResultT.run m) { Result.ok a => a == 42, Result.err _ => false }#[test]def test_resultt_bind : Bool := match Id.run (ResultT.run resultt_bind_result) { Result.ok a => a == 11, Result.err _ => false }def resultt_bind_short_circuit_result : ResultT String Id I64 := let m : ResultT String Id I64 := ResultT.mk (Id.id (Result.err "boom")) in Monad.bind m (fn a => Monad.pure (a + 1))#[test]def test_resultt_bind_short_circuits : Bool := match Id.run (ResultT.run resultt_bind_short_circuit_result) { Result.ok _ => false, Result.err e => String.beq e "boom" }#[test]def test_optiont_pure_run : Bool := let m : OptionT Id I64 := Monad.pure 42 in match Id.run (OptionT.run m) { Option.some a => a == 42, Option.none => false }def optiont_bind_result : OptionT Id I64 := let m : OptionT Id I64 := Monad.pure 10 in Monad.bind m (fn a => Monad.pure (a + 1))#[test]def test_optiont_bind : Bool := match Id.run (OptionT.run optiont_bind_result) { Option.some a => a == 11, Option.none => false }def optiont_bind_short_circuit_result : OptionT Id I64 := let m : OptionT Id I64 := OptionT.mk (Id.id Option.none) in Monad.bind m (fn a => Monad.pure (a + 1))#[test]def test_optiont_bind_short_circuits : Bool := match Id.run (OptionT.run optiont_bind_short_circuit_result) { Option.some _ => false, Option.none => true }