You can inspect the styles with browser dev tools. It's IBM Plex Mono.
1,300 karma · joined January 17, 2015
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...
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".
Simon Peyton Jones would beg to differ. :)
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.
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.
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.
For the same reason you'd make 1 + 2 the same as 1 + (2). Parentheses can be used to group arbitrary subexpressions.
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.
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();`).
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.
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.
What does this mean?
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.
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.
(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.
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).
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.
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...
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.