Refining inductive types

Robert Atkey, Patricia Johann, Neil Ghani

Research output: Contribution to journalArticle

10 Citations (Scopus)

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.
LanguageEnglish
Article number9
Number of pages30
JournalLogical Methods in Computer Science
Volume8
Issue number2
DOIs
Publication statusPublished - 4 Jun 2012

Fingerprint

Refining
Refinement
Computer programming languages
Programming
Type Systems
Programming Languages
Reasoning

Keywords

  • programming language
  • programme developers
  • data

Cite this

@article{8f9e9db5dc734e9eacebc2fc416fada2,
title = "Refining inductive types",
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.",
keywords = "programming language, programme developers, data",
author = "Robert Atkey and Patricia Johann and Neil Ghani",
year = "2012",
month = "6",
day = "4",
doi = "10.2168/LMCS-8(2:9)2012",
language = "English",
volume = "8",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
number = "2",

}

Refining inductive types. / Atkey, Robert; Johann, Patricia; Ghani, Neil.

In: Logical Methods in Computer Science, Vol. 8, No. 2, 9, 04.06.2012.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Refining inductive types

AU - Atkey, Robert

AU - Johann, Patricia

AU - Ghani, Neil

PY - 2012/6/4

Y1 - 2012/6/4

N2 - 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.

AB - 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.

KW - programming language

KW - programme developers

KW - data

U2 - 10.2168/LMCS-8(2:9)2012

DO - 10.2168/LMCS-8(2:9)2012

M3 - Article

VL - 8

JO - Logical Methods in Computer Science

T2 - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 9

ER -