Intensional Refinement Datatypes: With Application to Scalable Verification of Pattern-Match Safety

Eddie C Jones; Steven Ramsay

doi:10.1145/3445980

Intensional Refinement Datatypes: With Application to Scalable Verification of Pattern-Match Safety

Eddie C Jones, Steven Ramsay

Research output: Contribution to journal › Article (Academic Journal) › peer-review

71 Downloads (Pure)

Abstract

The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic data types by a limited form of structural subtyping and environment-level intersection. We describe a fully automatic, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds.

Original language	English
Article number	55
Number of pages	29
Journal	Proceedings of the ACM on Programming Languages
Volume	5
Issue number	POPL
DOIs	https://doi.org/10.1145/3445980
Publication status	Published - 4 Jan 2021

Structured keywords

Programming Languages

Access to Document

10.1145/3445980

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via Association for Computing Machinery at https://doi.org/10.1145/3434336. Please refer to any applicable terms of use of the publisher.
Final published version, 378 KBLicence: CC BY

https://arxiv.org/abs/2008.01452

Embargoed Document

Full-text PDF (author accepted manuscript)
Accepted author manuscript, 818 KB
Request copy

1 Active

8030 EPSRC EP/T006595/1 Higher-order Constrained Horn Clauses
Ramsay, S.
1/03/20 → 28/02/23
Project: Research

Cite this

@article{6f062454843d4f39a4341b935899ac96,

title = "Intensional Refinement Datatypes: With Application to Scalable Verification of Pattern-Match Safety",

abstract = "The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic data types by a limited form of structural subtyping and environment-level intersection. We describe a fully automatic, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds. ",

author = "Jones, {Eddie C} and Steven Ramsay",

year = "2021",

month = jan,

day = "4",

doi = "10.1145/3445980",

language = "English",

volume = "5",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "POPL",

}

TY - JOUR

T1 - Intensional Refinement Datatypes

T2 - With Application to Scalable Verification of Pattern-Match Safety

AU - Jones, Eddie C

AU - Ramsay, Steven

PY - 2021/1/4

Y1 - 2021/1/4

N2 - The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic data types by a limited form of structural subtyping and environment-level intersection. We describe a fully automatic, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds.

AB - The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic data types by a limited form of structural subtyping and environment-level intersection. We describe a fully automatic, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds.

U2 - 10.1145/3445980

DO - 10.1145/3445980

M3 - Article (Academic Journal)

VL - 5

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - POPL

M1 - 55

ER -

Intensional Refinement Datatypes: With Application to Scalable Verification of Pattern-Match Safety

Abstract

Structured keywords

Access to Document

Embargoed Document

Fingerprint

Projects

8030 EPSRC EP/T006595/1 Higher-order Constrained Horn Clauses

Cite this