Recursive Program Synthesis using Paramorphisms [pdf]
theory.stanford.edu
theory.stanford.edu
> paramorphisms, a class of programs that includes the most common recursive programming patterns on algebraic data types
"most common ... patterns". ok.
they're alluding to math[1] but they're not doing math.
I also disagree with the notion that they aren't really doing math. It's very straightforward to derive programs by proving other properties of these recursive combinators. I would recommend reading A tutorial on the universality and expressiveness of fold [1] as an example of this; folds are catamorphisms, which is why I bring it up.
[0]: https://www.researchgate.net/publication/256269748_Paramorph...
[1]: https://www.cambridge.org/core/journals/journal-of-functiona...
I literally linked that paper.
> It's very straightforward to derive programs by proving other properties of these recursive combinators.
Cool they don't do that. There's a word for being obliquely related: allusion.
It's amazing how much benefit of the doubt CS people get. In math you either prove a theorem/lemma by writing it out in full or you... have nothing. In CS people tell nice stories, draw cool diagrams, write down random formulae and everyone is just hmm yes brilliant.
You did; I overlooked that. I don't know why you're implying the authors invented the term and made up the combinator just now, then.
> Cool they don't do that.
Their program is basically doing an automated version of what Graham Hutton did in that paper, except they rewrite functions using para instead of fold.
Edit:
> It's amazing how much benefit of the doubt CS people get. In math you either prove a theorem/lemma by writing it out in full or you... have nothing. In CS people tell nice stories, draw cool diagrams, write down random formulae and everyone is just hmm yes brilliant.
You seem to have a chip on your shoulder. I don't know why you're telling me this.
So they're applying the math somebody else already put together? It isn't clear what your opinion is. Are you saying it's not valid if it's not math?
Let's judge the paper by what they say they did in the abstract.
> We show that synthesizing recursive functional programs using a class of primitive recursive combinators is both simpler and solves more benchmarks from the literature than previously proposed approaches.
It sounds like their proposed metrics are subjective ("simpler") or data-oriented ("solves more ... than previously").
> Our method synthesizes paramorphisms, a class of programs that includes the most common recursive programming patterns on algebraic data types.
They're applying a pre-existing concept ("paramorphisms") to a problem domain where (it is implied) it either has not been applied before, or with a new spin.
> The crux of our approach is to split the synthesis problem into two parts: a multi-hole template that fixes the recursive structure, and a search for non-recursive program fragments to fill the template holes.
They give a novel (,it is implied) structural model for solving their problem using their chosen concept as their key contribution to the study of this problem. It is indirectly suggested that factoring the recursive and non-recursive parts apart allows them to be handled more effectively individually.
---
Regarding your specific complaints: I do not see any immediate need for new math. Nor are they inventing new words, at least in the title or abstract. You may have legitimate concerns about general academic practice, but if you're going to levy those criticisms at this paper, you could do your arguments better justice than with a drive-by.
> for a detailed review of paramorphisms from a formal perspective, see [Meertens 1992]
To your original point, the title of this paper is only using terms ("paramorphisms", "recursive", and "program synthesis") that are decidedly not novel.
For the benefit of other readers:
As to why "paramorphisms" are singled out as a concept worthy of having their own name, I recommend the 1991 paper "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" by Meijer, Fokkinga, and Paterson, which is much more readable than the referenced Meertens paper.
We all know what an "infinite loop" is; a natural question is whether there are any looping constructs that cannot get caught in an infinite loop. The "for-each" loop has become popular in imperative languages; the reason it works is because it does a kind of structural iteration over finite data which fits a regular pattern.
A "catamorphism" precisely captures this notion of structural iteration (really, structural recursion), for a vast family of data types (the "inductively defined" ones). But for any algorithm where you'd use an unbounded loop (or unbounded recursion), it's not always easy (or possible!) to implement that algorithm using catamorphic recursion instead -- and they're not always the most performant, either (e.g. you can't short-circuit the recursion).
So we've gone from something that is too powerful/expressive (unbounded recursion/iteration) to something that is not powerful/expressive enough (catamorphic recursion/iteration), with the dividing line of "allows infinite loops" somewhere in the middle. The study of general recursion schemes, which includes paramorphisms, is essentially the study of alternatives to unbounded recursion/iteration that are better than catamorphisms on one or more desiderata.
You're the second person to link the exact same paper I did in my first response.
> To your original point, the title of this paper is only using terms ("paramorphisms", "recursive", and "program synthesis") that are decidedly not novel.
They italicize paramorphism in the abstract. We all very well know that italics means novel usage. So again: let's drop the charade that everything is above board here.
Or, they're writing for an audience that isn't necessarily familiar with paramorphisms and other morphisms, but still is familiar with functional programming.
Yes; it sounds like you're suggesting they should be defining these concepts themselves instead of saying somebody else did them. But that would be academic dishonesty. So you must be alluding to something else.
> We all very well know that italics means novel usage.
You say that as though expecting everyone to agree. I do not. I personally use italics because several people I have spoken with, including my advisor, feel that boldface is shouty. Underline is rarely used for a similar reason. Italic font is the the only available form of typographic \emph{asis}; it is used (if sparingly) for key terms and ideas that the reader's attention should be drawn to, which include novel ideas, but can be much more than that.
OK. Since you're opposed to merely alluding to things (your italics, which I find funny), could you please state explicitly the misconduct you are alleging?
[...] capture this modified recursion pattern explicitly as a higher-order operator; in this case, the operator is known as a paramorphism [92]. In the case of lists, we could define
paraL :: (α → (List α, β) → β) → β → List α → β
paraL f e Nil = e
paraL f e (Cons x xs) = f x (xs, paraL f e xs)
I think what you're criticising is that the name "paramorphism" was adopted from category-theory-on-a-blackboard to functional-programming-that-actually-runs-on-a-computer. That ship sailed 30 years ago; this paper from 2024 is not what caused it to sail. I also think that you're incorrect to criticize this. Analogies are often very helpful.
You are right that the people who pointed you to Meertens's paper were not helpful in clearing up the confusion, since your confusion is exactly that Meertens's paper talks about the other meaning of the term "paramorphism".
Personally I'm fine with that - I have no issue with CS people borrowing terminology from category theory to describe stuff, so long as the analogy is reasonable. But I get where you're coming from - having learned some CT in (grad) school, I used to find Haskell wikis confusing as heck because they use CT terminology but nobody clarifies what category they're actually working in!
"Hask", the (almost) category where the objects are types and the morphisms from A to B is the type A -> B.
Edit: to be more specific, you need to specify what constitutes a type - all possible ADTs under all possible names? Are equivalent functions considered the same morphism? What about seq? Is there a privileged "IO" type, and if not how is it represented in the set of types? What about other monads hiding different side effects? What about bottom? Many of these choices will of course be equivalent in some sense, but technically speaking you don't have a category until you've nailed this stuff down.
Paramorphisms' section is at page 5. It refers to the 1990 paper by Lambert Meertens that your reference attributes to 1992.