Скачать или смотреть [TyDe'22] Structural Refinement Types

Structural Refinement Types (Video, TyDe 2022)
David Binder, Ingo Skupin, David Lawen, and Klaus Ostermann
(University of Tubingen, Germany; University of Tubingen, Germany; University of Tubingen, Germany; University of Tubingen, Germany)

Abstract: Static types are a great form of lightweight static analysis. But sometimes a type like List is too coarse; we would also like to work with its refinements like non-empty lists, or lists containing exactly 42 elements. Dependent types allow for this, but they impose a heavy proof burden on the programmer. We want the checking and inference of refinements to be fully automatic. In this article we present a simple refinement type system and inference algorithm which uses only variants of familiar concepts from constraint-based type inference. Concretely, we build on the algebraic subtyping approach and extend it with typing rules which combine properties of nominal and structural type systems in a novel way. Despite the simplicity of our approach, the resulting type system is very expressive and allows to specify and infer non-trivial properties of programs.

Article: https://doi.org/10.1145/3546196.3550163

ORCID: https://orcid.org/0000-0003-1272-0972, https://orcid.org/0000-0001-8320-8445, https://orcid.org/0000-0003-1276-9151, https://orcid.org/0000-0001-5294-5506

Video Tags: Structural Types, Nominal Types, Refinement Types, Algebraic Subtyping, icfpws22tydemain-p5-p, doi:10.1145/3546196.3550163, orcid:0000-0003-1272-0972, orcid:0000-0001-8320-8445, orcid:0000-0003-1276-9151, orcid:0000-0001-5294-5506

Presentation at the TyDe 2022 conference, September 11, 2022, https://icfp22.sigplan.org/home/tyde-...
Sponsored by ACM, ACM SIGPLAN, https://www.sigplan.org/