Freezing Bidirectional Typing (Extended Abstract)
summary
Frost implements bidirectional information flow between function and argument types, using skeletons with ghosts to pass partial type shapes both ways; a freezing operator locks a term’s type so context cannot override it, resolving ambiguous flows. It infers where to introduce and instantiate quantifiers for first‑class polymorphism, supports implicit type abstraction, and is implemented in an ML‑like language with modal effect types. The authors conjecture a simple sound and complete inference algorithm and report that freezing is rarely required.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:23First-class polymorphism motivation
- 3:12Effect types and key observation
- 4:58Frost approach
- 8:38Type information flow directions
- 10:53Bidirectional flow importance
- 12:39Skeletons for partial types
- 18:28Default skeleton limits
- 20:14Freezing operator for inference
- 22:29Comparison with existing methods
- 23:13Color-based representation
- 25:26Future work and implementation
- 25:47Takeaways and conclusion
- 26:09Question and answer session
related talks
27mTowards Type Debugging using Partial Evaluation
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
01h 05mAll the Languages Together
21mPolymorphic Type Inference for Dynamic Languages
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
19mIll-Typed Programs Don't Evaluate
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
16mPolymorphic Types and Effects with Boolean Unification