A Simpler Encoding of Indexed Types
summary
Presents a restricted indexed-type syntax that replaces general term unification with evaluable term pattern unification, claims simpler implementation and measurable performance via index erasure optimization, and proves a sound and complete translation from simpler indices into general index types. Implements the design in Arend and Aya (homotopy-type variants) and formalizes type checking in a dependently typed lambda calculus; limitations include inability to express some identity-type encodings unless a built-in path/identity type is provided.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:57Example applications
- 1:34Indices specify "constructor selection"
- 4:13New design
- 5:50Comparison with general indexed types
- 9:06Loss of expressivity
- 10:49The paper
- 11:16Implementation & application
related talks
19mIll-Typed Programs Don't Evaluate
14mA dependently typed calculus with pattern matching and erasure inference
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
28mEta conversion for the unit type (is still not that simple)
25mCubical Synthetic Homotopy Theory
25mShallowly embedding type theories
29mUnification Modulo Isomorphisms between Dependent Types for Type-based Library Search
18mThe Essence of Generalized Algebraic Data Types