Date: 2009-01-16 (non-standard day!)
Room: BBL room 509 (non-standard room!)
Speaker: Conor McBride (Strathclyde University)
Title: Slicing it: indexed containers? in Haskell?
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.
F : Set -> Set
which behave like
collections of elements drawn from
. 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
of "input" kinds of element
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.
- 08 Jan 2009