When is a type refinement an inductive type

Robert Atkey, Patricia Johann, Neil Ghani

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

8 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 ℕ-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 often store redundant information about data and their refinements. This paper shows how to generically derive inductive characterisations of refinements of inductive types, and argues that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. These 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
Title of host publicationFoundations of Software Science and Computational Structures
Subtitle of host publication14th International Conference, FOSSACS 2011
EditorsMartin Hofmann
PublisherSpringer
Pages72-87
Number of pages16
ISBN (Print)978-3-642-19804-5
DOIs
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6604
ISSN (Print)0302-9743

Fingerprint

Computer programming languages

Keywords

  • programming language
  • typed programming
  • data types

Cite this

Atkey, R., Johann, P., & Ghani, N. (2011). When is a type refinement an inductive type. In M. Hofmann (Ed.), Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011 (pp. 72-87). (Lecture Notes in Computer Science ; Vol. 6604). Springer. https://doi.org/10.1007/978-3-642-19805-2_6
Atkey, Robert ; Johann, Patricia ; Ghani, Neil. / When is a type refinement an inductive type. Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011. editor / Martin Hofmann. Springer, 2011. pp. 72-87 (Lecture Notes in Computer Science ).
@inproceedings{a7d220a9c8e547f9b1cfe98c96c29488,
title = "When is a type refinement an inductive type",
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 ℕ-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 often store redundant information about data and their refinements. This paper shows how to generically derive inductive characterisations of refinements of inductive types, and argues that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. These 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, typed programming, data types",
author = "Robert Atkey and Patricia Johann and Neil Ghani",
year = "2011",
doi = "10.1007/978-3-642-19805-2_6",
language = "English",
isbn = "978-3-642-19804-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "72--87",
editor = "Martin Hofmann",
booktitle = "Foundations of Software Science and Computational Structures",

}

Atkey, R, Johann, P & Ghani, N 2011, When is a type refinement an inductive type. in M Hofmann (ed.), Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011. Lecture Notes in Computer Science , vol. 6604, Springer, pp. 72-87. https://doi.org/10.1007/978-3-642-19805-2_6

When is a type refinement an inductive type. / Atkey, Robert; Johann, Patricia; Ghani, Neil.

Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011. ed. / Martin Hofmann. Springer, 2011. p. 72-87 (Lecture Notes in Computer Science ; Vol. 6604).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - When is a type refinement an inductive type

AU - Atkey, Robert

AU - Johann, Patricia

AU - Ghani, Neil

PY - 2011

Y1 - 2011

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 ℕ-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 often store redundant information about data and their refinements. This paper shows how to generically derive inductive characterisations of refinements of inductive types, and argues that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. These 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 ℕ-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 often store redundant information about data and their refinements. This paper shows how to generically derive inductive characterisations of refinements of inductive types, and argues that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. These 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 - typed programming

KW - data types

U2 - 10.1007/978-3-642-19805-2_6

DO - 10.1007/978-3-642-19805-2_6

M3 - Conference contribution book

SN - 978-3-642-19804-5

T3 - Lecture Notes in Computer Science

SP - 72

EP - 87

BT - Foundations of Software Science and Computational Structures

A2 - Hofmann, Martin

PB - Springer

ER -

Atkey R, Johann P, Ghani N. When is a type refinement an inductive type. In Hofmann M, editor, Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011. Springer. 2011. p. 72-87. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-642-19805-2_6