Abstract
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 language | English |
|---|---|
| Pages (from-to) | 89-113 |
| Number of pages | 25 |
| Journal | Mathematical Structures in Computer Science |
| Volume | 26 |
| Issue number | Special Issue 01 |
| Early online date | 20 Nov 2014 |
| DOIs | |
| Publication status | Published - 1 Jan 2016 |
Fingerprint
Keywords
- codes (symbols)
- computational linguistics
- containers
- algebraic structures
- dependently typed programming
- meta language
- recursions
- structural recursion
- type systems
- functional programming
Cite this
}
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 journal › Special 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
JF - Mathematical Structures in Computer Science
SN - 0960-1295
IS - Special Issue 01
ER -