Prism: An Impure Functional Language With Typed Effects
6 hours ago
- #algebraic effects
- #type systems
- #functional programming
- Prism is a functional programming language that models effects using modern type systems inspired by OCaml 5, Haskell, and Koka, emphasizing typed and composable effects.
- Effects are handled via algebraic effect handlers, allowing operations like yield, choose, and reject to be defined and managed with typed rows, enabling composition without monad transformers.
- The language unifies multiple language features (exceptions, generators, lenses, mutable state, failure handling) under one mechanism using effect rows, providing zero-cost abstractions via evidence passing and Perceus reference counting.
- Prism supports modern type features including higher-rank polymorphism, ad-hoc polymorphism with type classes (Lean-style instances), and row polymorphism for effects, enabling polymorphic functions over effects.
- It compiles to LLVM IR and MLIR with a tiny C runtime, uses deterministic reference counting for memory management, and includes a Lean 4 model for formal verification and replayable execution.
- Prism includes a web-based playground via WASM, allowing interactive experimentation, and is designed as a proof-of-concept that prioritizes typed effects and compiler optimizations over purity.