Structural Refinement Types

on YouTube ↗13m

" summary

A lightweight refinement-type system and inference algorithm extends algebraic subtyping with rules from polymorphic variants to infer precise refinements (non-empty lists, exact-length lists, a predecessor function that rejects zero) with no annotations and no SMT solvers. Constraint generation produces subtyping constraints solved and simplified via automata-based simplification; higher-kinded refinements support per-spine or per-element list refinements. Implementation is small if the base algebraic-subtyping engine exists; limits: only regular-type properties (cannot express primality), metatheory and usability (verbose inferred types) remain to be completed.

AI-written summary · about

" chapters (6)

1. 0:00Problem statement
2. 1:36Structural refinement types
3. 2:38System design and inference
4. 4:31Typing rules
5. 7:25Handling parameterized types
6. 9:47Takeaways and future work