Decomposable Type Highlighting for Bidirectional Type and Cast Systems
summary
Defines a formal, decomposable highlighting method that computes synthesis slice and analysis slice answers for bidirectional typing, attaches those slices to types so they flow through dynamic casts, and exposes them in a prototype web UI for the gradually typed Hazel language. Implementation runs sliced Hazel programs so highlighted pieces still typecheck and execute, locates the minimal typing context that caused an error, and currently handles bidirectional cases with a partial prototype and hand proofs that the author plans to mechanize.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:28What is Hazel and bidirectional typing
- 3:31Bidirectional typing modes
- 4:34Term slices and precision
- 6:00Interactive type exploration
- 7:49Formal semantics for type analysis
- 10:00Decomposable type highlighting foundations
- 11:29Synthesis and analysis slices
- 13:35Minimally scoped checking contexts
- 15:24Dynamic casts and type debugging
- 16:30Future work and UI improvements
- 18:57Q&A
related talks
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
19mFlexible Structure Editing of Well-Typed Expressions
19mA Dependently Typed Language with Dynamic Equality
20mStatically Contextualizing Large Language Models with Typed Holes
15mTaming Type Annotations in Gradual Typing
02h 50mIntro to Type Systems and Operational Semantics
27mTowards Type Debugging using Partial Evaluation
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)