I was reading "Upwards and downwards accumulations on trees" by Jeremy Gibbons, and it's written in the Bird-Meertens formalism (a.k.a. Squiggol) of yesteryear. Not that I have anything against people who can write and understand this stuff (in fact, I have a lot of respect for them), but for me, the inconsistent and seemingly arbitrary notation leaves something to be desired. In an attempt to understand what was actually being done, I translated most of the equations to Haskell code. If you plan on reading this paper, here's hoping I could jump-start your comprehension with this contribution.
The only real issue that I ran into while performing this translation is in the function s_fork_sl2
. The second component of the catamorphism, ((⊙ ↟ ≪) ∘ ≪²), does not have the expected type (b, b) -> a -> (b, b) -> (b, b)
. After attempting to puzzle through how to unify the two, I eventually gave up and just came up with a function that seemed to do what I thought it should do, pairs g (x, _) _ (y, _) = (g x y, x)
where g :: b -> b -> b
is ⊙. But I'm not sure whether there's a bug in the definition in the paper or the one in my code. The code seems to work for a few tests. If you've already read this paper or you're at all interested in debugging Squiggol, I would be happy to learn how this works.
Sorry I'm such a late-comer, but no one's said anything, and I just found your blog - wonderful stuff, by the way.
ReplyDeleteI guess the big issue is how do you interpret the equivalents of 'fst' and 'snd' on a triple.
Because the trees used here are triples, it doesn't quite fit the form. Thank you for going through it and working on it beforehand.
I'm not sure I understand you. Can you give some context?
ReplyDeleteWell, the way in which the middle component of a triple gets "absorbed" by the operator is suggested, but is not specified very formally; it seems as if readerd (users?) are just supposed to "get it" by osmosis. It seems to me that it complicates how that "((⊙ ↟ ≪) ∘ ≪²)" part is supposed to obtain the subscript from the tree, and treat the other two parts as a pair. I am guessing that one is supposed to just ignore the middle part, and treat the two branch results as a pair. Since the examples in the paper only do this with operators and not with entire function expressions, it seems like the "crash course" in the notation is more like a "crash-and-burn" course.
ReplyDeleteAh yes. I think I see what you're saying. I had forgotten about the notation and the subscript approach to ┴.
ReplyDeleteNo to mention how (to my perspective, anyway) the operators tend to take currying as a matter of course, treating arguments as a pair, or as two separate values, with no warning, or notice. That makes it all the tougher to interpret.
ReplyDelete