Containers, monads and induction recursion

Neil Ghani, Peter Hancock

Research output: Contribution to journalSpecial issue

1 Citation (Scopus)

Abstract

Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a set U of codes and a decoding function T : U → D which assigns to every code u : U, a value T, u of some type D, e.g. the large type Set of small types or sets. The name induction recursion refers to the build-up of codes in U using inductive clauses, simultaneously with the definition of the function T, by structural recursion on codes.
Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation – in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.
LanguageEnglish
Pages89-113
Number of pages25
JournalMathematical Structures in Computer Science
Volume26
Issue numberSpecial Issue 01
Early online date20 Nov 2014
DOIs
Publication statusPublished - 1 Jan 2016

Fingerprint

Monads
Container
Recursion
Containers
Proof by induction
Functional programming
Computer programming languages
Decoding
Functional Programming
Algebraic Structure
Type Systems
Programming Languages
Assign

Keywords

  • codes (symbols)
  • computational linguistics
  • containers
  • algebraic structures
  • dependently typed programming
  • meta language
  • recursions
  • structural recursion
  • type systems
  • functional programming

Cite this

Ghani, Neil ; Hancock, Peter. / Containers, monads and induction recursion. In: Mathematical Structures in Computer Science. 2016 ; Vol. 26, No. Special Issue 01. pp. 89-113.
@article{89e3b0a2981e4cf1a6fefc5f1cc2aa9e,
title = "Containers, monads and induction recursion",
abstract = "Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a set U of codes and a decoding function T : U → D which assigns to every code u : U, a value T, u of some type D, e.g. the large type Set of small types or sets. The name induction recursion refers to the build-up of codes in U using inductive clauses, simultaneously with the definition of the function T, by structural recursion on codes.Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation – in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.",
keywords = "codes (symbols), computational linguistics, containers, algebraic structures, dependently typed programming, meta language, recursions, structural recursion, type systems, functional programming",
author = "Neil Ghani and Peter Hancock",
year = "2016",
month = "1",
day = "1",
doi = "10.1017/S0960129514000127",
language = "English",
volume = "26",
pages = "89--113",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
number = "Special Issue 01",

}

Containers, monads and induction recursion. / Ghani, Neil; Hancock, Peter.

In: Mathematical Structures in Computer Science, Vol. 26, No. Special Issue 01, 01.01.2016, p. 89-113.

Research output: Contribution to journalSpecial issue

TY - JOUR

T1 - Containers, monads and induction recursion

AU - Ghani, Neil

AU - Hancock, Peter

PY - 2016/1/1

Y1 - 2016/1/1

N2 - Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a set U of codes and a decoding function T : U → D which assigns to every code u : U, a value T, u of some type D, e.g. the large type Set of small types or sets. The name induction recursion refers to the build-up of codes in U using inductive clauses, simultaneously with the definition of the function T, by structural recursion on codes.Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation – in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.

AB - Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a set U of codes and a decoding function T : U → D which assigns to every code u : U, a value T, u of some type D, e.g. the large type Set of small types or sets. The name induction recursion refers to the build-up of codes in U using inductive clauses, simultaneously with the definition of the function T, by structural recursion on codes.Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation – in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.

KW - codes (symbols)

KW - computational linguistics

KW - containers

KW - algebraic structures

KW - dependently typed programming

KW - meta language

KW - recursions

KW - structural recursion

KW - type systems

KW - functional programming

UR - http://journals.cambridge.org/action/displayJournal?jid=MSC

U2 - 10.1017/S0960129514000127

DO - 10.1017/S0960129514000127

M3 - Special issue

VL - 26

SP - 89

EP - 113

JO - Mathematical Structures in Computer Science

T2 - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - Special Issue 01

ER -