Dear Pl Wonks,

Today we have Abhishek presenting Stephanie Weirich and Chris Casinghino's
work on generic programming.
Details follow.

Roshan


Title:
Arity-generic datatype-generic programming
by Stephanie Weirich and Chris Casinghino

Speaker:
Abhishek Kulkarni

When and Where:
LH115, Fri 4:00pm, Apr 16th

Abstract:
Some programs are doubly-generic. For example, map is
datatype-generic in that many different data structures support a
mapping operation. A generic programming language like Generic
Haskell can use a single definition to generate map for each
type. However, map is also arity-generic because it belongs to a
family of related operations that differ in the number of
arguments. For lists, this family includes repeat, map, zipWith,
zipWith3, zipWith4, etc. With dependent types or clever
programming, one can unify all of these functions together in a
single definition.

However, no one has explored the combination of these two forms
of genericity. These two axes are not orthogonal because the idea
of arity appears in Generic Haskell: datatype-generic versions of
repeat, map and zipWith have different arities of kind-indexed
types. In this paper, we define arity-generic datatype-generic
programs by building a framework for Generic Haskell-style
generic programming in the dependently-typed programming language
Agda 2.

http://www.seas.upenn.edu/~sweirich/papers/aritygen.pdf