Prism: An Impure Functional Language With Typed Effects
7 days ago
- #algebraic effects
- #type systems
- #functional programming
- Prism是一种函数式编程语言，它使用受OCaml 5、Haskell和Koka启发的现代类型系统来建模效果，强调类型化和可组合的效果。
- 效果通过代数效果处理器来处理，允许定义和管理如yield、choose和reject等操作，并使用类型化行实现组合，从而无需单子变换器。
- 该语言通过效果行将多种语言特性（异常、生成器、透镜、可变状态、失败处理）统一在一个机制下，通过证据传递和Perceus引用计数提供零成本抽象。
- Prism支持现代类型特性，包括高阶多态性、带有类型类的临时多态性（Lean风格实例）以及效果的行多态性，实现了对效果的多态函数。
- 它编译为LLVM IR和MLIR，带有微小的C运行时，使用确定性引用计数进行内存管理，并包含一个用于形式验证和可重放执行的Lean 4模型。
- Prism通过WASM包含一个基于Web的游乐场，支持交互式实验，其设计是一个概念验证，优先考虑类型化效果和编译器优化，而非纯粹性。