Danel Ahman: Directed Containers (or monoids, actions, dependent types, and more)

Date of publication: 8. 10. 2018
Mathematics and theoretical computing seminar
Četrtek, 11. 10. 2018, od 11h do 13h, učilnica 3.07, Jadranska 21
Abstract: In this talk I am going to give an overview of a neat specialisation of container datatypes, called directed containers, which I have been working on with James Chapman and Tarmo Uustalu, and discuss their various applications in computer science. I will begin by recalling their basic type-theoretic definition, their use for modelling datastructures where each data-node naturally determines a compatible
sub-datastructure, and discuss why they are a canonical such structure. I will also outline their more fibrational definition and make some interesting observations about it. I will then show you that they also have useful applications in effectful (think state) and bidirectional (think lenses) programming. Finally, I will discuss a slightly different characterisation of them, which also leads us back to the interesting observations I will have made earlier in the talk.