Home
Schedule
Abstract Template
Masters Attendance
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
Slicing It:IndexedContainersInHaskell
Stc
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