A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F...
summary
Presents F⋈, a small core language that lets intersection types, union types and overloaded functions coexist with a deterministic merge operator by enforcing a dual pair of relations (mergeability and distinguishability) and performing systematic eta expansion of runtime values. Gives concrete typing rules, an operational semantics that wraps values to hide nonexposed fields, and formal proofs: progress, preservation and determinism for the calculus. Demonstrates encoding of extensible evaluators (integers + floats) without code duplication, and mechanized meta-theory.
AI-written summary · about
chapters (6)
- 0:00A Bowtie for a Beast
- 1:46The Merge Operator: Pitfalls
- 7:12Mergeability: Functions
- 8:59Disjointness & Duality
- 11:24Operational Semantics
- 17:59Example: Summary
related talks
26mTypes as First-Class Values in Fuzion (Extended Abstract)
18mThe Essence of Generalized Algebraic Data Types
15mQualified Types with Boolean Algebras
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
19mTowards Tagless Interpretation of Stratified System F (Extended Abstract)
19mExtensible Metatheory Mechanization via Family Polymorphism
46mThe Calculated Typer (Functional Pearl)
15mLiberating Merges via Apartness and Guarded Subtyping