Home
Schedule
Abstract Template
Masters Attendance
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" &ndash; 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 &ndash;                                                  
  fictitious, but plausible enough to be executable already &ndash; 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, &hellip;" presentation.                                  




-- Main.AndresLoeh - 08 Jan 2009