HackerPapers

arXiv:2010.07763cs.PL

Refinement Types: A Tutorial

Ranjit Jhala, Niki Vazou

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code. In this article, we distill the ideas developed in the substantial literature on refinement types into a unified tutorial that explains the key ingredients of modern refinement type systems. In particular, we show how to implement a refinement type checker via a progression of languages that incrementally add features to the language or type system.

arXiv comments
Journal reference
DOI
Subjects
cs.PLProgramming Languages cs.LOLogic in Computer Science cs.SESoftware Engineering

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Jan 2024 to Jan 2024. Found in 2 HN submissions from Oct 2020 to Oct 2020. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Cold showers on overhyped topics (2017) 1 comment

    • If I'm understanding correctly, refinement types[1] solve this by allowing you to constrain a type into a smaller set of values. Think set notation: ``` type Temperature<min: number, max: number> = { x: number | x >= min && x <= max } ``` [1]…

      potsandpansView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.