lptk
if e is
...
Lit(value)
and Map.find_opt(value) is Some(result)
then Some(result)
...
where the `...` may include many cases and may contain other Lit cases.Or this variation:
...
Lit(value)
and Map.find_opt(value) is Some(result)
and computation(result) is
Left(a) then ...
Right(b) then ...
...In ML you can't write something like this:
if e is
...
Lit(value)
and Map.find_opt(value) is Some(result)
then Some(result)
...
where the `...` may include many cases and may contain other Lit cases, so that you would need to refactor the whole expression.Haskell's pattern guards can do this, but they can't "split" control-flow in the middle of a case, as in:
Lit(value)
and Map.find_opt(value) is Some(result)
and computation(result) is
Left(a) then ...
Right(b) then ...
but these all fall out completely naturally in the UCS.Also, exhaustiveness Just Works without the need of any type annotation. The system is actually type system agnostic.
> I worry that the semantics around exhaustiveness and mutable values may be confusing, though I guess OCaml already has that problem
Indeed, and it was until very recently a source of unsoundness: https://icfp24.sigplan.org/details/mlworkshop-2024-papers/8/...
Java, one pair of parens:
int x = 1;
int y = x + 1;
System.out.println(y);
Clojure, six pairs of brackets: (let [x 1 y (+ x 1)] ((. (. System out) println) y))For the record, there is not one accepted definition, but we can get close by saying that FP languages are those based on lambda calculus as their semantics core. And the primary mechanism in lambda calculus is variable capture (as done in closures).
C is based on the Von-Neumann model and has absolutely nothing to do with the lambda calculus. No reasonable PL expert considers it functional.
Once you're used to the way it works, and if you're using well-maintained libraries, I find that it's really not such a big deal. Though it's always awkward to have transitive dependency conflicts, and those are best avoided if possible.
Also worth noting that Scala is not a "very big" language in any sense that I know of. It has a lot fewer features than C#, for instance. And probably a comparable amount to TypeScript.
The power of Haskell's type classes comes from two things:
* Implicit composition of instances: you can write `show [True, False]`, which will automatically/implicitly compose the `Show` instances of lists and booleans. With modules or interfaces, you'd have to build and use a "BoolListShow" manually.
* Higher-kinded types, to abstract over type constructors. This enables the use of abstractions like monads.
Rust only has the first of these two.
Scala uses OOP interfaces instead, but by augmenting them with both capabilities (implicit composition and higher-kinded types), it achieves the same expressiveness as Haskell.
I don't think parallelism is the word for that. More like concurrency
Parallel computing is closely related to concurrent computing—they are frequently used together, and often conflated, though the two are distinct: it is possible to have parallelism without concurrency (such as bit-level parallelism), and concurrency without parallelism (such as multitasking by time-sharing on a single-core CPU).[5][6] In parallel computing, a computational task is typically broken down into several, often many, very similar sub-tasks that can be processed independently and whose results are combined afterwards, upon completion. In contrast, in concurrent computing, the various processes often do not address related tasks; when they do, as is typical in distributed computing, the separate tasks may have a varied nature and often require some inter-process communication during execution.
https://en.wikipedia.org/wiki/Parallel_computing
What you're describing sounds like it would be solved by primitives such as the actor model, not by Haskell-style FP.
Sorry to hear that! I guess it depends on your preferences. Personally, I have a pretty "operational" mindset, so I'll find an algorithm easier to understand than its specification in terms of abstract algebra.
The whole thing started when I tried reimplementing MLsub at an MSR hackathon, and found it unnecessarily difficult — all the operational insights had to be painstakingly extracted from the thesis and barely-documented OCaml implementation (like others, I found the paper insufficient to reimplement the approach satisfyingly, for instance see http://gallium.inria.fr/blog/safely-typing-algebraic-effects...). I wrote this paper so other type system implementers wouldn't have to go through it again!
Actually, I'm not sure it would be that hard (Simple-sub author here). If you look at the core of the algorithm closely, you'll see it's really not special: you create type variables, add constraints on them, propagate the constraints, and that's mostly it. In fact, it's perfectly in line all previous work on subtyping inference, going back at least to Pottier's 1998 thesis — that thesis already had many ingredients of MLsub. The three big things MLsub brought to the table, in my opinion, were: 1. the idea to coalesce constraint graphs into compact type expressions, which are easier to read and understand; 2. using the algebraic insight to develop an elegant and simple principality proof (but I'm not sure it's really worth it; AFAIK the proof sketch I provided would also work); and 3. to provide a simpler subsumption checking algorithm. Specifically in terms of pure type inference (so, ignoring points 2 and 3), it's possible to imagine making the leap to compact types without the algebra insight. But this is just speculation, and it's of course impossible to tell a posteriori.
> If you want to add subtyping to a language with a more sophisticated type system, or add new features to a language that already has subtyping
In that case I think Simple-sub is a good place to start, as it does not presuppose all the algebraic structure that MLsub does; Simple-sub shows that principal type inference really doesn't need much at all form the type system. Now, you're free to add more structure to your subtyping lattice if you want to be able to simplify types more, and if you want to make checking subsumption easier, but the choice is in your hands.
> you should probably take a long hard look at it from an algebraic point of view to make sure they interact the way you want
That's still definitely true!
> the community takes a good hard look at itself to see what it can improve
This has already been happening for a while. FYI, the Scala center is entirely dedicated to improving Scala usage and its tooling, which JDG somehow forgets to mention (along with many other positive things happening in the community).
In fact, it turned out in discussions on reddit that JDG is kind of living in his own bubble, not really aware of a lot of things happening outside of it, and thinks he is the only one to see some problems that have in fact been worked on for years. For example, tooling with the Scala center, and the Scala2/Scala3 transition which has been a _central_ consideration in the design and implementation of Dotty since the inception of the project!
The problem is that modules in ML have a verbose syntax and are clunky to use compared to type classes. OCaml's modular implicits aim to make this better (see https://arxiv.org/abs/1512.01895), taking inspiration from Sala's implicits.
But I don't think that is what they meant. I think they meant something along the lines of what I said above:
> an expression with an arbitrary number of subexpressions may be synthesized, the shape of which depends on the types involves
AFAIK, Odersky doesn't particularly like people trying to replicate Haskell patterns in Scala. For example, he thinks using monads for most effects is inappropriate.
In fact, ML modules have had higher-kinded types [1] since before Haskell even existed. I guess Haskell's main innovation in this domain is really its very convenient higher-kinded parametric polymorphism with type classes.
[1] MacQueen, D B (1984). Modules for Standard ML. Conference Record of the 1984 ACM Symposium on LISP and Functional Programming Languages. 198-207.
The example you give to justify "recursion is quite restricted" is not a restriction on recursion at all, it's an ambiguity problem. Define `a` as `y` to shadow the function parameter, and it compiles.