curryhoward

You can inspect the styles with browser dev tools. It's IBM Plex Mono.

Ah, I think your clarification makes a lot more sense than your original phrasing, because Haskell's position is indeed that side effects are bad, not that effects are bad. The bad thing is "side", not "effects".

The suggestion is to use pure Haskell for the rules DSL only. The surrounding system that applies any side effects would presumably not be written in that language.

It's a good idea, and Facebook actually does something like this for their spam filtering rules: https://engineering.fb.com/2015/06/26/security/fighting-spam...

Citation needed on "well-established". I find myself often benefiting from Haskell's disciplined approach to effects.

For one, Rust's "trait" system, which is a foundational part of the language that enables a lot of Rust's expressivity, is a limited imitation of Haskell's "type classes". Rust would be a very different language without it.

The Y combinator is not the same as λ calculus. The Y combinator is an expression in λ calculus.

Even more beautiful than the y combinator

That's a bit of a strange statement. The Y combinator is an expression in λ calculus. It's like saying French is even more beautiful than the phrase "nouveau départ".

Comic Sans is perfect for setting children’s activity timetables that are displayed in a school playground. It’s perhaps not as appropriate for announcing scientific breakthroughs.

Simon Peyton Jones would beg to differ. :)

and why they are so absolutely lost when it comes to creating successful languages

They aren't lost—they're just more interested in actually good ideas than in popularity. Popular languages must appeal to all kinds of programmers with varying backgrounds, so they are heavily constrained. Your argument is basically that mathematicians don't know what they're doing because their most advanced theories aren't used by mechanical engineers.

Most of the functional programmers I know have a deeper understanding of OOP than the OOP programmers I know. For example, most of the OOP programmers I know do not understand covariance and contravariance (whereas just about every functional programmer I know has mastered them), even though those concepts frequently come up in the context of OOP. People who study programming language theory tend to gravitate toward the functional paradigm, but it's not because they don't understand OOP.

That's what (4) is for. Time out after some duration.

Code has limited CPU available as well - if it tries to use too many cycles it quits with an error

That's a pretty strange failure mode. Usually you'd just throttle the sandboxed application (e.g., give it a CFS quota with a CPU cgroup) or give it a limited number of vCPUs.

the implicit operator in a sequence of two expression without parentheses could be string concatenation rather than function application

You can design a language which uses `e1 e2` to represent any binary operation you like, but I'd argue that function application is more common than string concatenation, so it's more deserving of that syntax. Plus, it plays nicely with currying.

Is there a reason why you would make fn(1) and fn 1 equivalent?

For the same reason you'd make 1 + 2 the same as 1 + (2). Parentheses can be used to group arbitrary subexpressions.

Exactly. We should recognize that as the real contribution of Rust: not breaking new ground in what is theoretically possible, but making it practical for the masses.

Until about 5 years ago there was no safe, GC-free, practical systems programming language, and furthermore it was unknown how to build such a thing. Now we know.

It was known [1], but only by theorists, and theorists aren't the ones building compilers and implementing real programming languages.

Obviously the Rust community has achieved an impressive feat of engineering, and I'm extremely grateful for that. But using a substructural type system to avoid needing a garbage collector is not a new idea, just one that Rust has successfully popularized.

It takes a long time for ideas from the programming languages theory community to reach the mainstream.

[1] http://www.cs.ioc.ee/ewscs/2010/mycroft/linear-2up.pdf

You are correct in that there is a definition of idempotence that agrees with you, but you are wrong to correct the parent comment, because the most common mathematical definition of idempotence of functions agrees with them (and not you).

There are multiple definitions of idempotence, used even within computer science, and neither of you seem to be aware of the definition used by the other. The common mathematical definition of an idempotent function is that f(f(x)) = f(x) for all x. But in computer science there is another common definition which involves side effects not being repeated (that is, `f(); f();` is the same as `f();`).

Certain functional programmers corrupted this idea to somehow mean pure functions are free; that these functions can be executed one to infinity times and the result is the same.

I think you are conflating two things and attacking a strawperson. As someone who is very involved in the functional programming community, I've never heard anyone say that pure functions are "free", and if this has been said it's certainly not the majority perspective. The fact that a function gives you the same result given the same arguments is not meant to be some kind of encouragement to redundantly call a function many times. It's meant to give you a tool to better reason about the program logically. You don't have to worry about _when_ a pure function is called, because it doesn't depend on hidden state that may change over time, and it doesn't change anything about its environment.

In a sense, I think you seem to have been given the _opposite_ idea (not necessarily saying it was your misunderstanding vs. someone else poorly communicating to you); the fact that a function always gives you consistent results means that you never have to invoke it multiple times. In some sense, this viewpoint recognizes the cost of function execution even more than the zeitgeist.

I think a significant portion of programmers are very smart people who work hard at producing good, generalizable, understandable effective code.

To be clear, I don't disagree with this, but it's not relevant. You wouldn't expect a typical mechanical engineer to have research-level mastery of theoretical physics, even if they can build impressive, reliable machines. It's not an insult to the engineer.

I follow thousands of languages

What does this mean?

Regarding the need for evidence in programming languages research: maybe it's just my bias for theory, but I think of PL research as a branch of mathematics more than an experimental discipline. In mathematics, you don't cite evidence, you write proofs. Most of the papers in conferences like POPL deal with topics like domain theory, type theory, category theory, formal logic, semantics, models of computation, etc. Results in these fields are achieved on paper or in a proof assistant, not by taking a survey.

For whatever reason, papers about programming languages that attempt to use data to make arguments about productivity, safety, etc. always seem unconvincing to me. Maybe it's because they usually aren't reproducible, or maybe it's just because the way most programmers write code doesn't matter to me, because most programmers aren't aware of what is possible on the frontier.

Google Cloud Run / AWS Fargate. You upload a Docker image and you instantly have a service with auto-scaling, load balancing, HTTPS, etc. It works with any programming language thanks to Docker.

Small plug: consider using Toast [1] to define your CI jobs. It's essentially Make + Docker. You define whatever targets you want (build, test, lint, etc.) and the dependencies between them in a YAML file, and Toast runs them in Docker containers. You can run your jobs on any machine that has Docker—including CI systems like Travis and GitHub Actions. You aren't locked into any CI system, and you can also run your jobs locally.

[1] https://github.com/stepchowfun/toast

A small plug: Toast (https://github.com/stepchowfun/toast) has already introduced a patch for this vulnerability (CVE-2020-15228), so arbitrary user code running inside Toast will not be able to trigger this vulnerability when run via a GitHub Action. I highly recommend using Toast for your CI jobs (with or without GitHub Actions), not just for this security fix but also because it also allows you to run your CI jobs locally. It just runs everything inside Docker containers, so it works the same in CI, on your laptop, on your coworker's machine, etc.

One important difference between algebraic effects and resumable exceptions is that with algebraic effects, the handler gets access to a reified version of the current continuation. The handler can then use that continuation to resume an arbitrary number of times, or not at all. For example, the handler could resume once for each item in a list, essentially using the continuation to map the list to a new list. The handler can even return the continuation to be invoked later, after the handler has finished. This is very unlike the restricted kind of resumable exceptions that you see in hardware.

Algebraic effects are a structured form of delimited continuations, for people who know about that concept. They give you nearly the full power of monads.

I like to think there is a nice pun here, that functional programming is "timeless" in two simultaneous ways:

(1) As mentioned in the article, values are immutable and side effects are reified so you do not have to reason about time. Instead, you can reason equationally, which unlocks some nice benefits related to refactoring, reasoning about correctness and concurrency, testing, reproducibility, etc.

(2) Functional programming is based on well-behaved mathematical foundations and so is more stable than the other programming paradigms. Object-oriented programming is a constantly moving target because it doesn't have a principled formal foundation (despite many attempts to establish one on an ex post facto basis), whereas functions are "timeless" in the sense that they're here to stay.

It's not without tradeoffs of course, but if you're willing to have an open mind about how computers should be programmed and forego some things that are so pervasive in traditional programming (e.g., unrestricted side effects), the payoff is huge.

it has canonicity, which I'd argue is necessary for a general-purpose programming language

MLTT, even without HoTT/CTT, already features canonicity, no? (At least for positive types.)

I thought the main advantage of HoTT is that you can define non-trivial equalities, and the advantage of CTT in particular is that univalence can be derived in it (rather than introducing it as a non-computational axiom).

My number one use case for comments is documenting invariants/preconditions/postconditions that are not enforced by any automated mechanism (e.g., a type system). I'm surprised no one else has mentioned this. To me these are exactly the things that MUST be commented. Of course, it's useful to have some mental heuristics around what other kinds of comments are helpful to readers, but unenforced assumptions/guarantees need to be documented so programmers in the future can see what they are.

One might argue that all invariants should be covered by tests, but tests (by themselves) cannot even ensure some the most basic properties about functions, such as that a function always returns a sorted list no matter what input it's given. Tests also cannot ensure that a function's preconditions are always satisfied at every call site, because new call sites can be added in the future without causing the existing tests to fail.

There is a recent paper called "Codata in action" [1] that I think gives a nice explanation of (part of) OOP in terms of codata types.

But that paper also finally clarified for me why OOP is so awkward and unnatural sometimes. Why should an entire program be composed only of codata types? One would think data types (which are traditionally seen more in functional languages than OOP languages) would be more natural for most problems.

The specific combination of late binding and equi-recursive codata types that is approximated by OOP only makes sense when you're solving a problem that is naturally expressed in terms of those features, but in my mind the majority of problems are not.

The other major problem I have with OOP is that it's not a straightforward manifestation of an underlying mathematical calculus, but rather a hodgepodge of (not universally agreed upon) programming ideas that are best applied on a more à la carte basis. These ideas should be used when appropriate rather than taken as an indivisible paradigm to be applied wholesale to every programming problem. That's why I prefer to think of OOP as a design pattern rather than a programming paradigm: useful in some situations, but not to be used for every situation.

[1] https://www.microsoft.com/en-us/research/uploads/prod/2020/0...

Union types are basically an anonymous form of sum types.

This is false on multiple levels. First, being a sum type has nothing to do with the type being named vs. anonymous. What makes a sum type a sum type is that it's a categorical coproduct, whether you give it a name or not. Second, sum types are synonymous with _disjoint_ (i.e., tagged) unions, not unions. Consider the union of boolean with itself. The result would be equivalent to boolean, because union is an idempotent operation. Disjoint union, or sum, would give you a type with 4 values instead of 2.

Technically enums (or more generally tagged unions, which is what Rust's enums are) is a superset of sum types as you can have multiple variants of the same type

That just how sum types work (have you ever wondered why they are called "sum" in the first place?). You're thinking of union types.