Containers, monads and induction recursion

Neil Ghani, Peter Hancock

Research output: Contribution to journalSpecial issuepeer-review

2 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)89-113
Number of pages25
JournalMathematical Structures in Computer Science
Issue numberSpecial Issue 01
Early online date20 Nov 2014
Publication statusPublished - 1 Jan 2016


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


Dive into the research topics of 'Containers, monads and induction recursion'. Together they form a unique fingerprint.

Cite this