Twisol

> It's like saying "I though canine were dangerous?" (yes for big cats, no so much for your average French bulldog).

Big cats are not canines :(

> You're the second person to link the exact same paper I did in my first response.

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.

> 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.

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.

The alternative not making sense doesn't automatically make this solution make sense :( It just highlights how many corners C++ has backed its design into.

I think it was a joke about compilers removing code by reasoning about undefined behavior.

"Pointwise squaring on an interval x" is just a weird way of describing the usual function f(x) = x^2 with domain restricted to an interval. It's pointwise because that's how functions f : R -> R are defined: given a point, or value, of the domain, give me a new point in the codomain.

If you think of `x` as a whole interval unto itself, and not just a single point, then I think the options become more interesting. The most natural product on two sets is indeed the cross product; but for intervals, I can imagine defining a common parameterization over both intervals and then multiplying pointwise up to that parameterization.

I think the key ingredient you're looking for is mutability. If you take advantage of the ability to implicitly modify state, your declared interfaces reduce in size because you don't need to model the threading of state through the interface. Since mutability means that your method signatures are less restrictive then they appear to be, it makes sense that this research (focusing on dependent types, and especially on dependently-typed proofs) would prefer a setting without implicit mutability. (Mutation is orthogonal to OOP vs. FP, anyway -- you can have pure OOP interfaces and also mutable FP interfaces.)

The Java stream interface also has a lot of methods that can technically be implemented in terms of other methods on the interface, but are present so that implementers can provide more efficient implementations depending on the capabilities of their model of streams. It makes sense that the present research would only consider the bare essentials of streams, and not things that could be layered on top at the cost of some optimization opportunities.

As a Java programmer, the essence of an OOP stream seems to be captured by the following interface:

    interface Stream<T> {
      T next();
    }

If we make mutation explicit, this evolves into:

    interface Stream<T> {
      Pair<T, Stream<T>> next();
    }

And then we can split this into two methods, providing each of the two components of the original `Pair`:

    interface Stream<T> {
      T head();
      Stream<T> tail();
    }

This is exactly what the paper shows on page 2, up to syntactic differences (like explicit type parameters to the methods).

You might be surprised how many people would exclude languages like HTML on the basis that they don't describe computations. (I am more of a PL maximalist: any syntax that allows you to describe and manipulate some class of semantic objects in a machine-processable manner can reasonably be called a programming language.)

> substitute error with whatever type you want there - null, Error, or your own thing

And if I want `error` to be `string` so I can just provide an error message? Proper disjoint sum types let me keep the two sides disjoint, even if they happen to be the same type. Union types will collapse on any overlap, so if I happen to instantiate `error` at `string` then I can no longer tell my error case from my data case.

> You should use a `Result` or `Either` type for that like everyone does.

You have missed the thread context, which is whether `Either a a` (also written `a + a`) has any merits over simply `a` (which is identical to `a | a`). If you're on the `Either` train already, we are arguing over imaginary beef.

> No disrespect, but that still sounds entirely useless to me.

It is disrespectful to say something "makes zero sense", regardless of anything you might say to the contrary. You've misrepresented my point: nobody wants to model something as `String | String`.

If you have, say, an `Int | Bool`, and you pass both sides through some kind of stringification function, you're naturally going to get `String | String` without ever having written that type down yourself. You wouldn't necessarily want to collapse that to `String`, however, because you may -- for instance -- want to give strings and ints different decorations around them before finally flattening them. You might write such a function as something like

    (ib) => ib
      .mapBoth(showInt, showBool)
      .visit(prepend("int: "), prepend("bool: "));

You couldn't run this if the result of the `mapBoth` had type `String | String`: that type is indistinguishable from `String`, and since you can't tell which case you're in, you wouldn't know which tag to prepend.

You could write the same function without passing through `String | String`:

    (ib) => ib.visit(
      sequence(showInt, prepend("int: ")),
      sequence(showBool, prepend("bool: ")));

And yes, in this especially contrived example, perhaps you may find that to make more sense anyway. But in longer pipelines, sometimes separated over multiple functions, often involving generic code, it becomes much harder to simply always fuse steps in this manner. This is why we say sum types (e.g. `String + String`) compose better: they don't behave any differently depending on whether the two sides are the same or not. You have explicit control over when the two sides rejoin.

Big-O notation is a famous example where = is some flavor of (asymptotic) proportionality, and it catches a lot of people out when they first learn about it.

No, it isn't "completely useless".

If you have a function that will normally return a string, but can sometimes fail due to reasons, you may wish to yield an error message in the latter case. So you're going to be returning a string, or a string.

It's not what the content of the data is; it's how you're supposed to interpret it. You have two cases, success and failure, and control will flow differently depending on that, not based strictly on the type of data at hand. We just model those cases in a type.

I suspect you'd notice simply because scrolling to the top of your history isn't sufficient anymore to find the first error. (Assuming one clears their shell history before compilation, which is very nearly required in this context...)

"Tengen Toppa Gurren Lagann", from upthread; the GL is for "Gurren Lagann", which is how it's usually known.

Sometimes you'll have nested Options just because you're mapping a fallible operation over a fallible input. You don't want the resulting `Option<Option<T>>` to immediately collapse; then you wouldn't know which upstream operation failed. It's true that `Option<Option<T>>` is very generic (i.e. it doesn't inherently tell you what each None means), but flattening Options removes more information; it isn't a solution to the problem you're posing. At least you can post-process an `Option<Option<T>>` into a multi-variant, self-documenting result type before you pass the value off to some other consumer.

In other words, nested optionals might not be very readable, but they're a necessary product of having a highly modular, reusable toolkit, and you can always massage them into more informative, domain-specific types at whatever point that becomes appropriate.

Silence is not consent. As in many things, consent must be enthusiastic.

Ah, but now you've lost the asterisks in the transfer to HN! This art has been <gasp> defaced! /s

Yes, maybe I should have just posted it, but I'd rather people click through and actually read the OP. There's something worth your time on the other side of that link!

The best part is a ways down -- I'd quote it here but that would just be karma farming. Look for "With patch applied".

I have this issue on occasion with older mixed C/C++ codebases that use `.c` for C files and `.C` for C++ files. Maddening.

Right -- they happen in "screen space", not "world space", to use a graphics analogy.

Even in English, the term "lily-livered" is an insult (meaning "cowardly", apparently).

You've described something extraordinarily similar to my own mental topology for processing problems. I'm also autistic, although I think our sensitivities differ somewhat.

I also try to (and mostly succeed at) hold a whole problem in my head at once. This made me fairly successful at architecting software systems with many moving parts, but it's an incredible drain on my energy, and I would sometimes find myself so exhausted I would go to sleep for hours (i.e. not a simple nap) in the middle of the day. I credit this ability for my current burnout, honestly! It's deeply satisfying to do, but maintaining it week after week amidst all the other responsibilities of my previous job (especially the interpersonal ones) was crippling.

It would be kinder to assume that "I think about how to solve the problem" doesn't capture the nuances of actually doing that thinking to the satisfaction of the commenter, and this is their attempt to articulate it to match their experience. The process of "understand the starting point, the desired end point, and identify the path between them" closely matches the way I approach problems. If you don't feel inclined to meet someone where they're at, you can say so without condescension.

I don't think that term has been appropriate for a long time... Wikipedia seems to indicate similarly.

https://en.m.wikipedia.org/wiki/Mongolian_idiocy

I saw someone on Rocket League use that term as an insult. When I said it was a slur, they said it just meant "stupid", heh. No, buddy... there's a lot more to it than that.

From what I understand, a more direct analogue to "danger" is "abunai". The word "yabai" almost seems to be usable as a generic intensifier, like many English speakers might use the s-word. (I'm extremely far from fluent, though, so take my observations with a pile of salt.)

And Quiver itself exports to LaTeX that uses the `tikz-cd` package ("cd" for "commutative diagrams"), if you'd like to use that directly.

The OSS CAD Suite [0] is a good open-source toolchain for this stuff. You can then write hardware designs in the SytemVerilog language (VSCode has some plugins, I believe, but I've just been using a basic text editor) and use the build toolchain to compile ("synthesize") and program e.g. an FPGA with your designs.

(FWIW, I've only just taken a class on Verilog this past Spring, but we used oss-cad-suite and I found it pretty straightforward to use. The bundled version of Verilator had some issues on my Mac though, so I had to compile my own copy of Verilator.)

[0] https://github.com/YosysHQ/oss-cad-suite-build/

Alright, you've nerd-sniped me.

Our assumption is that the ratio of people with autism and ADHD to people with just autism is greater than the ratio of people with ADHD to people in general. Using your variables, that is: W / (W + X) > (W + Y) / (W + X + Y + Z). This simplifies out to the constraint that ZW > XY.

We want to show that the ratio of people with autism and ADHD to people with just ADHD is no greater than the ratio of people with just autism to people in general. This is: W / (W + Y) <= (W + X) / (W + X + Y + Z).

We can recognize that this is almost the same as our assumption, just exchanging the roles of X and Y. (I guess that's obvious from the problem statement.) That means our goal is to show that ZW <= YX, which is immediately just the negation of what we're assuming. That would be a contradiction.

So, indeed, this is mathematically impossible!

(EDIT: It's surprisingly hard to write these formulae down in English without getting confused.)

I think something that would be possible is that having ADHD if you have autism is more likely than having autism if you have ADHD. For instance, "being older than 20 if you're older than 30 is more likely than being older than 30 if you're older than 20" is just obviously true, because one entails the other.

Heh, and that subtitle is a link to a page that says:

> Meet Ayaha Hideri, the official anime mascot of Hysteria

I'm sure this would grate on many people, but honestly, I'm here for it.