Minutes of Meetings of the Algebra of Programming Research Group in 1999

Michaelmas Term 1999 (all Fridays)

• 3rd December
• 26th November
• 19th November
• 12th November
• 5th November
• 29th October
• 22nd October
• 15th October

Friday, 3rd December 1999

Mike described his shallow embedding of Prolog programs into Haskell. He explained that a graft operation on search trees and the Prolog features of success, failure, conjunction and disjunction could be modelled using a monoid and a monad. Then he gave two Haskell functions to interpret Prolog programs with depth-first and breath-first strategies. The proof that breadth-first search respects graft is very complicated. The group did not meet after lunch.

Friday, 26th November 1999

Before lunch, Ross (visiting for the day) discussed the properties of three functions that Mike Spivey had written for streams. Richard explained how to use Huffman trees to merge lists together. Ross summarised a paper by Hinze which defines generalised folds polytypically. Clare showed the group her alternative way of doing the same thing.

After lunch, Ross introduced his proposed syntax for arrows in Haskell. Ian gave a candidate membership relation for nested types. Finally, Richard explained the Hugh-Tucker algorithm for alphabetic trees.

Friday, 19th November 1999

Before lunch, Ian explained how Hoogendijk proved that his candidate zips on regular types were half zips. However, it seemed difficult to do the same thing for nested types, particularly because the new candidate zip could not be expressed clearly. Richard suggested he should use Clare's alternative definition of folds. Then Richard proved a theorem about optimum ordered trees.

After lunch, Shin showed that the greedy theorem could be applied to the problem of building trees of minimum height. The resulting program then needs to be simplified.

Friday, 12th November 1999

Before lunch, Clare explained how she could define generalised folds by induction on the grammar of functors. However, the fold functions produced are the same as those in Richard's paper. Richard took the higher-order nested datatype of bottom-up lists and expressed it in a convenient form previously used only for first-order nested datatypes. The form was needed in the paper to ease the definition of generalised folds. The group did not meet after lunch.

Friday, 5th November 1999

Before lunch, Jeremy said he wanted to prove the approx lemma, a generic version of the take lemma. This is not difficult to do if you use the universal property of folds but Jeremy wanted to avoid all mention of category theory for aesthetic reasons. Shin then talked about applying the greedy theorem to Richard's paper on building trees with minimum height.

After lunch, Ian gave an alternative presentation of Richard's generalised folds paper which was intended to be clearer.

Friday, 29th October 1999

Before lunch, Ian summarised the four properties that candidate zips must have according to Hoogendijk's thesis. He explained how zips were defined for regular datatypes and then extended the treatment to nested datatypes. Unfortunately, although zips on nested datatypes are natural transformations, one must define them as generalised folds rather than as simple folds.

After lunch, Shin talked for a quarter of an hour about Huffman encoding again.

Friday, 22nd October 1999

Before lunch, the group continued last week's discussion on research topics. Then Shin and Richard described how to represent Huffman encoding as an optimisation problem. Various improvements to the obvious algorithm were discussed informally without calculation.

After lunch, Clare described how to give semantics to higher-order nested datatypes. Although no folds have yet been written for them, it seemed possible to work them out from the initial algebras. The category she used was complicated but we all agreed that it had to be. After Clare left, Richard summarised the morning's discussion for Geraint.

Friday, 15th October 1999

The group made a list of aims for the new academic year:

• cata in = id (how to prove it without using universal property of folds)
• saving space using strictness (with respect to a letter frequency counter that ran out of space after 1000 characters)
• prove that colimits exist with co-continuous functors
• semantics of higher-order nested datatypes
• zips for nested datatypes
• A paper of Oege's derives a polytypic definition of repmin and turns it into a logic problem by changing the category. What happens when we do the same thing to other functions?

Ian talked about zips to motivate a discussion on how to generalise nested functors to nested relators. He then explained how to use type classes to enforce constraints on programs. We then talked about Hinze's comments on the technique.

In the afternoon we discussed the Hamming problem. Delicate handling of lazy evaluation was needed to cope with infinite lists of infinite lists. Shin presented a working solution. The problem is very similar to that of generating the sentences of an arbitrary grammar, which was studied by Mackenzie.