Picture of smart phone in human hand

World leading smartphone and mobile technology research at Strathclyde...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by University of Strathclyde researchers, including by Strathclyde researchers from the Department of Computer & Information Sciences involved in researching exciting new applications for mobile and smartphone technology. But the transformative application of mobile technologies is also the focus of research within disciplines as diverse as Electronic & Electrical Engineering, Marketing, Human Resource Management and Biomedical Enginering, among others.

Explore Strathclyde's Open Access research on smartphone technology now...

Containers, monads and induction recursion

Ghani, Neil and Hancock, Peter (2016) Containers, monads and induction recursion. Mathematical Structures in Computer Science, 26 (Specia). pp. 89-113.

Full text not available in this repository. (Request a copy from the Strathclyde author)

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.