BFPG Monthly Meetup (last one of 2018!)

Intro to Zippers - Tony Morris

The term zipper is a colloquial used to describe n-hole (most often, 1-hole) contexts. That is, a data structure that has a hole or pointer focused on a specific element with the ability to efficiently traverse to its neighbouring elements, providing an elegant solution for the need to efficiently traverse and modify immutable data structures.

In this talk, we will look at examples of zippers for canonical data structures such as lists and other products and sums. We will then define comonads and see the relationship between zippers and comonads.

Most of this talk will be spent on the practical application of zippers in everyday programming. We will solve some simple problems using zippers. We will then contrast why we might use a zipper, compared to a lens.

Finally, for a fun and interesting observation, we will look at the algebraic structure of products and sums, then compute the derivative of these structures. Turns out, a derivative of a data structure is its zipper ("McBride, Conor, et al (2005). ∂ for Data: Differentiating Data Structures").

Dependently Typed Zippers over Dependent-Data-Type-Embedded DSLs - Donovan Crichton

GADT (AKA Dependent-Data-Type) embedded DSLs have the advantage of being type-checked by the meta-language and are very easy to interpret. Unfortunately most people working with these DSLs know the difficulty involved when one wishes to transform part of the syntax tree. This talk proposes a method to address that issue through the introduction of a Huet Zipper implemented with dependent types. The talk will start by briefly introducing the concepts of dependent types (GADTs, pi types, and sigma types), along with a brief refresher on GADT-Embedded (HOAS) DSLs, before moving on to discuss the details of the zipper implementation proper in Idris. This talk aims to showcase how dependent types can be applied in interesting ways to tackle some otherwise difficult problems.