Skip to main content

Research Repository

Advanced Search

Indexed containers

Altenkirch, Thorsten; Ghani, Neil; Hancock, Peter; McBride, Conor; Morris, Peter

Authors

Neil Ghani

Peter Hancock

Conor McBride

Peter Morris



Abstract

We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.

Citation

Altenkirch, T., Ghani, N., Hancock, P., McBride, C., & Morris, P. (2015). Indexed containers. Journal of Functional Programming, 25, 1-41. https://doi.org/10.1017/s095679681500009x

Journal Article Type Article
Acceptance Date Mar 18, 2015
Online Publication Date May 20, 2015
Publication Date 2015
Deposit Date Jan 13, 2021
Journal Journal of Functional Programming
Print ISSN 0956-7968
Electronic ISSN 1469-7653
Publisher Cambridge University Press (CUP)
Peer Reviewed Peer Reviewed
Volume 25
Article Number e5
Pages 1-41
DOI https://doi.org/10.1017/s095679681500009x
Public URL https://nottingham-repository.worktribe.com/output/5224778
Publisher URL https://www.cambridge.org/core/journals/journal-of-functional-programming/article/indexed-containers/FB9C7DC88A65E7529D39554379D9765F

You might also like



Downloadable Citations