Containers, monads and induction recursion

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

Full description

Saved in:
Bibliographic Details
Published in:Mathematical structures in computer science 2016-01, Vol.26 (1), p.89-113
Main Authors: GHANI, NEIL, HANCOCK, PETER
Format: Article
Language:English
Subjects:
Cleaning
Computer programming
Computer science
Containers
Decoding
Mathematical analysis
Mathematical models
Programming
Recursion
Recursion theory
Universe
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0960-1295
1469-8072
DOI:10.1017/S0960129514000127