Slicing It:IndexedContainersInHaskell

Date: 2009-01-16 (non-standard day!)

Time: 11:00

Room: BBL room 509 (non-standard room!)

Speaker: Conor McBride (Strathclyde University)

Title: Slicing it: indexed containers? in Haskell?

Abstract

In this talk I shall attempt to explain the idea of "indexed containers" – a key foundational component of dependent data structures. Improbably, I shall seek to do this by developing the basic equipment for constructing and using them in a dialect – fictitious, but plausible enough to be executable already – of the dependently typed functional programming language, Haskell.

A container F : Set -> Set gives sets F X which behave like collections of elements drawn from X. We expect containers to be functorial, i.e. to support

map_F : all S, T. (S -> T) -> F S -> F T

and, moreover, to have least (greatest) fixpoints corresponding to (co-)inductively defined sets, equipped with (un-)fold operators and so on. Recursively defined containers may then be studied (in the style of Bird, de Moor et al.) by taking fixpoints of two-parameter containers with bifunctorial structure, and so on.

In the dependently typed setting, we can generalize to the notion of indexed container (Altenkirch, Ghani, Hancock, McBride, and Morris) G : (I -> Set) -> (O -> Set), for sets I of "input" kinds of element and O of "output" kinds of collection, with at least the functorial behaviour suggested by seeing each (X -> Set) as a slice category

map_G : all X, Y. (all i. X i -> Y i) -> (all o. G X o -> G Y o)

E.g., vectors are indexed containers in (1 -> Set) -> (Nat -> Set), with one kind of element, and collections distinguished by length; map for vectors transforms elements, preserving length. Conveniently, indexed containers are closed under fixpoints. Correspondingly, their "algebra of programming" is arguably rather more straightforward in principle than for the standard "set, functor, bifunctor, …" presentation.

-- AndresLoeh - 08 Jan 2009