Talk Invitation: Idiomatic Traversals (29/8)

[Tom Schrijvers]

Stefan Mehner will give a talk on lawful Traversable instances this Thursday August 29 at 10:30 in lecture room V1 of building S9 (campus De Sterre) to which you are kindly invited.

See http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.6.0.1/Data-Traversable.html.

Understanding Idiomatic Traversals Backwards and Forwards

Stefan Mehner, Universitaet Bonn

We present new ways of reasoning about a particular class of effectful Haskell

programs, namely those expressed as idiomatic traversals. Starting out with a

specific problem about labelling and unlabelling binary trees, we extract a

general inversion law, applicable to any monad, relating a traversal over the

elements of an arbitrary traversable type to a traversal that goes in the

opposite direction. This law can be invoked to show that, in a suitable sense,

unlabelling is the inverse of labelling. The inversion law, as well as a number

of other properties of idiomatic traversals, is a corollary of a more general

theorem characterising traversable functors as finitary containers: an

arbitrary traversable object can be decomposed uniquely into shape and

contents, and traversal be understood in terms of those.  Proof of the theorem

involves the properties of traversal in a special idiom related to the free

applicative functor.

--
prof. dr. ir. Tom Schrijvers

Programming Languages Group
Department of Applied Mathematics and Computer Science
University of Ghent

Krijgslaan 281 S9
9000 Gent
Belgium
Phone: +32 9 264 4805
http://users.ugent.be/~tschrijv/