When Is a Type Refinement an Inductive Type?

DOI10.1007/978-3-642-19805-2_6zbMATH Open1326.68066arXiv1205.2492OpenAlexW1594164162MaRDI QIDQ3000600FDOQ3000600

Authors: Robert Atkey, Patricia Johann, Neil Ghani

Publication date: 19 May 2011

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Abstract: Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the N-indexed type of vectors refines lists by their lengths. Other data types may be refined in similar ways, but programmers must produce purpose-specific refinements on an ad hoc basis, developers must anticipate which refinements to include in libraries, and implementations must often store redundant information about data and their refinements. In this paper we show how to generically derive inductive characterisations of refinements of inductive types, and argue that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. Our characterisations also ensure that standard techniques for programming with and reasoning about inductive types are applicable to refinements, and that refinements can themselves be further refined.

Full work available at URL: https://arxiv.org/abs/1205.2492

Recommendations

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Cited In (2)

This page was built for publication: When Is a Type Refinement an Inductive Type?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000600)