Minutes of 2006 Meetings of the Algebra of Programming Research Group

Trinity Term 2006 (all Fridays)

• 23rd Jun
• 9th Jun
• 26th May
• 12th May
• 5th May
• 28th April
• 21st April

Hilary Term 2006 (all Fridays)

We did meet, but everybody was too busy to take notes.

Friday, 23rd Jun 2006

We (Jeremy, Sharon, Ian, Bruno) returned to the problem of handling insertions into red-black trees represented as a GADT:

data R  -- colours: red and black
data B

data Z  -- naturals
data S n

data RBTree a c h where  -- element type, root colour, black height
  Empty :: RBTree a B Z
  Red   :: RBTree a B n -> a -> RBTree a B n -> RBTree a R n
  Black :: RBTree a c1 n -> a -> RBTree a c2 n -> RBTree a B (S n)

The standard algorithms break the invariants in complicated ways, then subsequently reestablish them, and we haven't yet figured out precisely how to capture the breaks and repairs.

One approach, modelled on Hongwei Xi's implementation in Dependent ML, allows a single violation of the invariant at the root:

data OK  -- booleans
data Bad

data RBTree a c h v where  -- elements, colour, height, violations
  Empty :: RBTree a B Z OK
  Red   :: TwoBlacks c1 c2 v -> 
           RBTree a c1 n OK -> a -> RBTree a c2 n OK -> RBTree a R n v
  Black :: RBTree a c1 n OK -> a -> RBTree a c2 n OK -> RBTree a B (S n) OK

data TwoBlacks c1 c2 v where
  BB :: Or B B OK
  RB :: Or R B Bad
  BR :: Or B R Bad

Bruno suggested an alternative, adding a constructor Cast for coercing a red tree to black. Either way, we still didn't manage to complete the definition of insertion.

(Addendum: Ross Paterson wrote the following implementation:

  data Tree a n
          = BTree (RBTree a B n)
          | RTree (RBTree a R n)

  insert :: Ord a => a -> RBTree a c n -> Either (Tree a n) (RBTree a B (S n))
  insert x t = case insertRB x t of
          SameHeight t' -> Left t'
          Overflow a b c d e -> Right (Black a b (Red c d e))

  data InsertResult a n
          = SameHeight (Tree a n)
          | Overflow (RBTree a B n) a (RBTree a B n) a (RBTree a B n)

  -- only red nodes can overflow

  insertRB :: Ord a => a -> RBTree a c n -> InsertResult a n
  insertRB x t@Empty = SameHeight (insertB x t)
  insertRB x (Red l k r)
    | x == k = SameHeight (RTree (Red l x r))
    | x <  k = case insertB x l of
          BTree l' -> SameHeight (RTree (Red l' k r))
          RTree (Red ll lk lr) -> Overflow ll lk lr k r
    | x >  k = case insertB x r of
          BTree r' -> SameHeight (RTree (Red l k r'))
          RTree (Red rl rk rr) -> Overflow l k rl rk rr
  insertRB x t@(Black l k r) = SameHeight (insertB x t)

  insertB :: Ord a => a -> RBTree a B n -> Tree a n
  insertB x Empty = RTree (Red Empty x Empty)
  insertB x (Black l k r)
    | x == k = BTree (Black l x r)
    | x <  k = case insertRB x l of
          SameHeight (BTree l') -> BTree (Black l' k r)
          SameHeight (RTree l') -> BTree (Black l' k r)
          Overflow a b c d e -> RTree (Red (Black a b c) d (Black e k r))
    | x >  k = case insertRB x r of
          SameHeight (BTree r') -> BTree (Black l k r')
          SameHeight (RTree r') -> BTree (Black l k r')
          Overflow a b c d e -> RTree (Red (Black l k a) b (Black c d e))

using the above definitions of colours, naturals, and (the original) RBTree. Also, Conor McBride showed Jeremy an Epigram implementation, which Jeremy subsequently translated into Haskell using GADTs.)

Friday, 9th June 2006

There are certain rules governing how you can make cross stitches on Aida fabric, which has an open weave resulting in a square grid arrangement of holes on the fabric. Squares are sized 1 unit by 1 unit.

A cross stitch is made on a square from two straight stitches: a \ stitch followed by a / stitch. The \ stitch can be made in either the NW->SE direction or SE->NW direction. The / stitch can likewise be made in either the SW->NE or NE->SW direction. There can elapse many other stitches in between the making of the \ and the /, so long as the \ is first and sometime later the / occurs, the constraint is satisfied.

The cross-stitch theorem says that you never need to use more thread than you have to, in order to sew cross stitches to fill a contiguous region of colour. "Contiguous" means that it is one connected component only, where any square must share at least one boundary with another square in the region (i.e. no squares just touching at the corner). More formally, the cross-stitch theorem says that in order to sew a contiguous patch with n squares, you need only the amount of thread

enough leading thread to start with
+ 2n*sqrt(2) + 2n-1
+ enough thread to finish off securely

This means that you don't ever need to see any little diagonal lines behind the back of the fabric, each "underneath stitch" goes from down through one hole to up through another hole one unit away.

It was pretty easy to demonstrate convincingly, but informally, that this theorem is indeed true, but proving it formally turned out to be harder than it looks. We tried an inductive proof, but couldn't get all the cases to come out.

(Addendum: Sharon says she and Richard proved the theorem while at MPC in Kuressaare.)

Friday, 26th May 2006

Jeremy reminded the group about various approaches to modelling stateful web interactions in terms of continuations, such as Peter Thiemann's WASH, and work by Christian Queinnec and Felleisen. We spent some time reconstructing continuation-passing style, then contemplated briefly how to represent continuations as hidden fields in HTML forms. (Felleisen et al show that lambda lifting and defunctionalization are the two steps needed in addition to the CPS transform.)

Friday, 12th May 2006

Jeremy presented some aspects of a paper Swapping Argument and Results of Recursive Functions by Akimasa Morihata and others from Tokyo, to appear at MPC. The paper describes a technique for rearranging a program that assembles a value in its arguments (as an accumulating parameter) into a cyclic program that assembles the value in its results, which might be more amenable to fusion. In particular, the central theorems relate traditional and IO-swapped versions of foldl and a higher-order foldr. The proofs are rather operational, and we tried (with only moderate success) to deduce declarative proofs by equational reasoning, by reconstructing invariants for the cyclic programs.

Friday, 5th May 2006

Jeremy talked about using GADTs to do static dimensional analysis (eg of programs dealing in time, distance and velocity, guaranteeing appropriate dimensions of all quantities, and preventing adding a time to a distance).

Friday, 28th April 2006

Richard spoke about modelling brains as collections of neurons, inspired by Les Valiant's Circuits of the Mind.

Friday, 21st April 2006

Jeremy spoke about using Conor McBride's idioms, and in particular the traverse operator, to capture the essence of imperative iterations. What laws should traverse satisfy? There appear to be some higher-order naturality properties here, of the kind studied by Hoogendijk in the context of generic zips (which in retrospect isn't so surprising, because there is already a connection between idioms and zips).

See The Essence of the Iterator Pattern, and also the forthcoming chapter Datatype-Generic Programming of the SSDGP lecture notes.