3 ms·

They define paramorphisms more rigorously on pages 4–5.

by bradrn 2y ago

almostgotcaught 2y ago
That's not at all what they define in that section. They define their chosen combinator that is called "para" which is as close to what they're alluding to as a bicycle is to a semi truck.
- trealira 2y ago
  They didn't coin the term paramorphism. Lambert Marteens did in 1992 [0]. It's an extension of the concept of catamorphisms. These terms were invented by people knowledgeable about category theory [1]. 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_Paramorphisms https://www.researchgate.net/publication/256269748_Paramorph... [1]: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/tutorial-on-the-universality-and-expressiveness-of-fold/CDBAA53C7120E23CBBBE206FD47FDBAA https://www.cambridge.org/core/journals/journal-of-functiona...
  - almostgotcaught 2y ago
    > They didn't coin the term paramorphism. Lambert Marteens did in 1992 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.
    - trealira 2y ago
      > I literally linked that paper. 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.
    - Twisol 2y ago
      > they're alluding to math[1] but they're not doing math. 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.
- Twisol 2y ago
  You're correct that they aren't defining the concept of paramorphisms in that section -- but that's because paramorphisms have been present in the literature for a long time: > 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.
  - almostgotcaught 2y ago
    > present in the literature for a long time: 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.
    - 2y ago
- gergo_barany 2y ago
  What they're "alluding to" is a standard combinator that has existed under the name "paramorphism" for a long time. Here is Jeremy Gibbons's "Origami programming" https://www.cs.ox.ac.uk/jeremy.gibbons/publications/origami.pdf https://www.cs.ox.ac.uk/jeremy.gibbons/publications/origami.... from 2003: [...] 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 don't know of an older source for this particular syntactic presentation, though apparently if you put in the work to translate Squiggol to Haskell, you can read this concrete syntax out of Meijer et al.'s Bananas paper from 1991. 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".

They define paramorphisms more rigorously on pages 4–5.

by bradrn 2y ago

They define paramorphisms more rigorously on pages 4–5.

That's not at all what they define in that section. They define their chosen combinator that is called "para" which is as close to what they're alluding to as a bicycle is to a semi truck.

trealira 2y ago
They didn't coin the term paramorphism. Lambert Marteens did in 1992 [0]. It's an extension of the concept of catamorphisms. These terms were invented by people knowledgeable about category theory [1]. 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_Paramorphisms https://www.researchgate.net/publication/256269748_Paramorph... [1]: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/tutorial-on-the-universality-and-expressiveness-of-fold/CDBAA53C7120E23CBBBE206FD47FDBAA https://www.cambridge.org/core/journals/journal-of-functiona...
- almostgotcaught 2y ago
  > They didn't coin the term paramorphism. Lambert Marteens did in 1992 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.
  - trealira 2y ago
    > I literally linked that paper. 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.
  - Twisol 2y ago
    > they're alluding to math[1] but they're not doing math. 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.
Twisol 2y ago
You're correct that they aren't defining the concept of paramorphisms in that section -- but that's because paramorphisms have been present in the literature for a long time: > 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.
- almostgotcaught 2y ago
  > present in the literature for a long time: 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.
  - 2y ago
gergo_barany 2y ago
What they're "alluding to" is a standard combinator that has existed under the name "paramorphism" for a long time. Here is Jeremy Gibbons's "Origami programming" https://www.cs.ox.ac.uk/jeremy.gibbons/publications/origami.pdf https://www.cs.ox.ac.uk/jeremy.gibbons/publications/origami.... from 2003: [...] 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 don't know of an older source for this particular syntactic presentation, though apparently if you put in the work to translate Squiggol to Haskell, you can read this concrete syntax out of Meijer et al.'s Bananas paper from 1991. 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".