All Outputs (2)

Indexed containers (2015)
Journal Article
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

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... Read More about Indexed containers.

Monads need not be endofunctors (2015)
Journal Article
Altenkirch, T., Chapman, J., & Uustalu, T. (2015). Monads need not be endofunctors. Logical Methods in Computer Science, 11(1), 1-40. https://doi.org/10.2168/LMCS-11%281%3A3%292015

We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed λ-calculus syntax and indexed containers. We show tha... Read More about Monads need not be endofunctors.