Скачать или смотреть [Scheme'25] Sound Default-Typed Scheme (Position Paper)

Sound Default-Typed Scheme (Position Paper) (Video, Scheme 2025)
Jan-Paul Ramos-Davila
(Boston University)

Abstract: We propose a new approach to typing Scheme programs based on the observation that programmers often have strong beliefs about the “normal” behavior of their code. Rather than forcing a binary choice between static types and runtime checks, we introduce default typing, where each program point carries a plausibility-ranked set of types. The highest-ranked type (rank 0) represents what the programmer believes will “almost always” be true, while higher ranks capture increasingly exceptional cases. By leveraging Racket’s macro-extensible type system and SMT-based constraint solving, we can verify whether a program type-checks using only the default assumptions. Success yields efficient code with no runtime overhead; failure produces a counterexample showing which assumptions are violated. We provide a precise notion of conditional soundness: programs are guaranteed type-safe only when their default assumptions hold at runtime.


Presentation at the Scheme 2025 workshop, October 16, 2025, https://conf.researchr.org/home/icfp-...
Sponsored by ACM SIGPLAN.