You are here:
(02 Sep 2010,
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 <pre>map_F : all S, T. (S -> T) -> F S -> F T</pre> 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 <pre>map_G : all X, Y. (all i. X i -> Y i) -> (all o. G X o -> G Y o)</pre> 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. -- Main.AndresLoeh - 08 Jan 2009
ore topic actions
Topic revision: r2 - 02 Sep 2010,
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS?