Epilogue

This post is in the garden path style. It’s literate Haskell. Preramble:

> import Control.Applicative  -- gosh!
> import Unsafe.Coerce        -- eek!

Suppose I give you an applicative functor

< instance Applicative De

I'm not going to tell you what it is, but I am going to give you this handy fixpoint operator. Of course, I'm going to get cross if you use other kinds of general recursion.

< fix :: (De x -> x) -> x

I’m also going to define two fixpoint type constructors, and relate one to the other:

> newtype Nu f = Con (f (Nu f))
> newtype NuDe f = ConDe (f (De (NuDe f)))

< splat :: NuDe f -> Nu f

What’s going on? ‘De’ is for ‘delay’ — by some conceptual unit of time. Imagine that lazily produced values are sliced up into the parts ready now, the parts that’ll be ready a wee bit later, those a bit after that, and so ad infinitum. De delays data, and ‘NuDe’ is a fixpoint giving co-trees with delayed children.

Correspondingly, the fixpoint operator is guarded: to make an x, you can have help from a De x: that means you don’t get any information with which to start making the x, but you can maybe get hold of some other useful data in time for the delayed parts. The ‘splat’ operator strips out the delays and gives you ‘ordinary’ codata.

Streams

Let’s see an example:

> type Str    x = Nu ((,) x)
> type StrDe  x = NuDe ((,) x)
>
> nats :: Str Int
> nats = splat (make 0) where
>   make :: Int -> StrDe Int
>   make = fix $ \ make n -> ConDe (n , make < *> pure (n + 1))

I made a thing for showing the first n layers of some stuff

*Main> upto 5 nats
“(Con (0, (Con (1, (Con (2, (Con (3, (Con (4, ?))))))))))”

Of course, we know that there’s a nicer definition of ‘nats’,
via map:

> mapS :: (a -> b) -> StrDe a -> StrDe b
> mapS = fix $ \ mapS f as -> case as of
>   ConDe (a, das) -> ConDe (f a, mapS < *> pure f < *> das)

> nats' :: Str Int
> nats' = splat . fix $ \ nats' -> ConDe (0, mapS (1 +) < $> nats')

I suppose I should ham it up a bit.

> hmerge :: StrDe Int -> StrDe Int -> StrDe Int
> hmerge = fix $ \ hmerge as bs -> case (as, bs) of
>   (as@(ConDe (a, das)), bs@(ConDe (b, dbs))) -> case compare a b of
>     LT -> ConDe (a, hmerge < *> das < *> pure bs)
>     EQ -> ConDe (a, hmerge < *> das < *> dbs)
>     GT -> ConDe (b, hmerge < *> pure as < *> dbs)
>
> hamming :: Str Int
> hamming = splat . fix $ \ hamming -> ConDe (1,
>   hmerge < $> (mapS (2 *) < $> hamming)
>          < *> (mapS (3 *) < $> hamming) )

*Main> upto 20 hamming
“(Con (1, (Con (2, (Con (3, (Con (4, (Con (6, (Con (8, (Con (9, (Con (12, (Con (16, (Con (18, (Con (24, (Con (27, (Con (32, (Con (36, (Con (48, (Con (54, (Con (64, (Con (72, (Con (81, (Con (96, ?))))))))))))))))))))))))))))))))))))))))”

Is this interesting? Well, it might provide some flexibility in total coprogramming languages. It’s a tricky business. Here’s a problem I learned about from Nils Anders Danielsson. Take the usual Haskell nats

> hNats :: [Int]
> hNats = 0 : map (+1) hNats

and replace map by the ‘extensionally equal’

> map2 :: (a -> b) -> [a] -> [b]
> map2 f []            = []
> map2 f [a]           = [f a]
> map2 f (a : a' : as) = f a : f a' : map2 f as
>
> hNats' :: [Int]
> hNats' = 0 : map2 (+1) hNats'

[Edit: Peter Gammie rightly points out that map and map2 can be persuaded to disagree conspicuously on (x : undefined). I consider map and map2 to agree on all values worth speaking of. After all, if we can write Haskell programs ignoring partiality effects, we can surely apply the same lifting to conversation...]

What happens when you run hNats’?

*Main> hNats’
[0 C-c C-cInterrupted.

A good start, followed by a long wait. So map and map2 are not interchangeable despite being equal. It seems to me that we gain by making a clearer separation between the description of processes to generate codata and the codata themselves. In effect, that’s what NuDe exposes. Can we write mapS2? Let’s see

< mapS2 :: (a -> b) -> StrDe a -> StrDe b
< mapS2 = fix $ \ mapS2 f as -> case as of
< ConDe (a, das) -> ????

I can’t do any further case analysis just now, because das has a delayed type: the value isn’t really there yet. I can do it later, with a bit of a clunky helper function:

> mapS2 :: (a -> b) -> NuDe ((,) a) -> NuDe ((,) b)
> mapS2 = fix $ \ mapS2 f as -> case as of
>   ConDe (a, das) ->
>     let help (ConDe (a', das')) = ConDe (f a', mapS2 < *> pure f < *> das')
>     in  ConDe (f a, help < $> das)
>
> nats2 :: Nu ((,) Int)
> nats2 = splat . fix $ \ nats2 -> ConDe (0, mapS2 (1 +) < $> nats2)

Whoops!

*Main> upto 5 nats2
“(Con (0, (Con (1, (Con (2, (Con (3, (Con (4, ?))))))))))”

I fixed it! The abstractness of De makes sure we can’t look at things which aren’t ready.

Breadth-First Labelling

Let’s go a bit wild now, and have a crack at breadth-first labelling in the style of Jeremy Gibbons and Geraint Jones. We’ll need trees built like these

> data TreeF a tree = L | N tree a tree
> type Tree   a = Nu (TreeF a)
> type TreeDe a = NuDe (TreeF a)

The challenge is to define a function

< label :: Tree () -> Str x -> Tree x

which decorates the nodes of an unlabelled tree with data drawn from a stream, but to do so in a breadth-first manner. There’s a notoriously short program which does this.

> aux :: (Str s -> (t, Str s)) -> s -> t
> aux f s = t where
>   (t, ss) = f (Con (s, ss))
>
> labelGJ :: Tree () -> Str x -> Tree x
> labelGJ = aux . layer where
>   layer (Con L) xss = (Con L, xss)
>   layer (Con (N l () r)) (Con (Con (x, xs), xss0)) =
>     let (l', xss1) = layer l xss0
>         (r', xss2) = layer r xss1
>     in  (Con (N l' x r'), Con (xs, xss2))

But what an outrageous function aux is! For one thing, it’s astonishingly circular, relying on laziness to feed a function its own output. For another thing, it’s only going to work for some pretty darn well-behaved functions f.

Let’s have a nice big tree — infinite, but with some leaves — to play with

> myTree :: Tree ()
> myTree = splat . fix $ \ myTree -> ConDe $ N
>   (pure (ConDe (N myTree () (pure (ConDe L))))) () myTree

Let’s label that.

*Main> upto 4 (labelGJ myTree nats)  -- I added the layout
"(Con (N (Con (N (Con (N (Con (N ? 6 ?))
                         3
                         (Con (N ? 7 ?))))
                 1
                 (Con L)))
         0
         (Con (N (Con (N (Con (N ? 8 ?))
                         4
                         (Con L)))
                 2
                 (Con (N (Con (N ? 9 ?))
                         5
                         (Con (N ? 10 ?))))))))"

OK, it’s time to rumble. I’ll need a little gadget to split delayed pairs, and then we’re set.

> dePair :: De (s, t) -> (De s, De t)
> dePair dst = (fst < $> dst, snd < $> dst)

> myAux :: (StrDe s -> (t, StrDe s)) -> s -> t
> myAux f s = fst . fix $ \ tss -> f (ConDe (s, snd < $> tss))
>
> myLabel :: Tree () -> Str x -> Tree x
> myLabel t xs = splat (myAux (layer t) xs) where
>   layer = fix $ \ layer t xss -> case t of
>     Con L           -> (ConDe L, xss)
>     Con (N l () r)  -> case xss of
>       (ConDe (Con (x, xs), xss0)) ->
>         let (l', xss1) = dePair $ layer < *> pure l < *> xss0
>             (r', xss2) = dePair $ layer < *> pure r < *> xss1
>             in  (ConDe (N l' x r'), ConDe (xs, xss2))

See? Everything in the top layer happens now: everything below happens later. The type of myAux explains exactly the discipline required to make this work. Apart from idiomatic grot, it’s the same function. In fact, we could even retype myLabel to work on trees with delay — it’s breadth-first, after all.

Things To Do

Have you spotted the security hole? We need to make sure people don’t use splat in the middle of constructions to bring data forwards in time. I suspect that some runST-style voodoo would draw the boundary properly.

Given a fix to that problem, it remains to show that all the (co)programs which respect this interface and refrain from unauthorized recursion are suitably total. I’m working on a model in a total type theory and finally getting somewhere, after a lot of headbanging.

And then there’s the usual thing — we need to figure out how language can help us hide the applicative grot. It’d be nice just to mark the boundary between code executed now and code executed in the future, rather than all that noise.

Structure cops will note that De is another example of an applicative functor which is not a monad — join would bring things from the far future to the near future, and that had better not be possible. However, where applicative functors in general only pull through traversable functors (containers with finitely many elements), De pulls through all containers. So it’s a bit special. I wonder what it is.

Don’t Look!

OK, here’s the implementation. It’s a con.

> newtype De x = De x deriving Show -- ssh, don't tell!

> instance Functor De where
>   fmap f (De x) = De (f x)

> instance Applicative De where
>   pure = De
>   De f < *> De s = De (f s)

> fix :: (De x -> x) -> x
> fix f = f (De (fix f))

> splat :: NuDe f -> Nu f
> splat = unsafeCoerce

> class PShow f where
>   pshow :: (x -> String) -> f x -> String

> upto :: PShow f => Int -> Nu f -> String
> upto 0 _         = "?"
> upto n (Con fx)  = "(Con " ++ pshow (upto (n - 1)) fx ++")"

> instance Show a => PShow ((,) a) where
>   pshow sh (a, b) = "(" ++ show a ++ ", " ++ sh b ++ ")"

> instance Show a => PShow (TreeF a) where
>   pshow sh L = "L"
>   pshow sh (N s a t) = "(N " ++ sh s ++ " " ++ show a ++ " " ++ sh t ++ ")"

This entry was posted on Friday, June 26th, 2009 at 4:59 pm and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.