Polymorphic Types and Effects with Boolean Unification
summary
Extends Hindley-Milner with Boolean unification to infer precise pure/impure effects, proven to compute principal types and soundly guarantee that terms typed pure produce no effects. Implementation in the Flix compiler handles ~30k lines and ~1k standard-library functions; Boolean unification is NP-hard but empirical results show about 1.4x type-inference overhead and roughly 1.1x end-to-end compilation slowdown. Examples include map/compose constraints that enforce at-most-one-impure argument and use MGUs modulo Boolean equivalence to solve effect constraints.
AI-written summary · about
chapters (11)
- 0:00Start
- 1:33Type and Effect System To Rule Out Nonsensical Programs
- 2:26Signature for Map
- 2:51Forward Function Composition
- 3:17Haskell
- 6:18Extend Unification to Boolean Unification
- 8:15Rule for Function Abstraction
- 10:11Principle Type Inference
- 13:25The Performance Cost of Effect Inference
- 14:19Performance Impact on End-to-End Compilation Time
- 15:24Summary
related talks
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
15mQualified Types with Boolean Algebras
23mLet Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)
21mPolymorphic Type Inference for Dynamic Languages
32mMLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
30mConstraint Typing with Boolean Algebra
19mAssociated Effects: Flexible Abstractions for Effectful Programming