lptk

Genuine question, as I'm not up to date with C#'s recent developments: can C# do 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.

Or this variation:

      ...
      Lit(value)
        and Map.find_opt(value) is Some(result)
        and computation(result) is
          Left(a)  then ...
          Right(b) then ...
      ...

It's currently badly outdated. There's one specifically for the UCS at https://ucs.mlscript.dev/

PS: there's another point being made on Reddit about cond's right-shift problem: https://www.reddit.com/r/ProgrammingLanguages/comments/1g127...

Also check out my other answer here: https://news.ycombinator.com/item?id=41901573

Just check out the paper's Motivaton section (2).

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.

As mentioned in a response to a sibling comment, we plan to support `or`, which should address the problem you mention. (If not, would you have an example of what you mean?)

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

We definitely want to get into that! Unfortunately it's not completely straightforward. A simple desugaring doesn't work due to our support for intermediate bindings and computations, which we don't want to recompute.

Here the `Allocate` effect is just a syntactically-lightweight way of doing dependency injection, right? Similar to a Haskell type class. I don't see why you'd need to make it an algebraic effect, as it does not need to mess with control flow AFAIK.

That's obviously nonsense.

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

Your idea of what FP means is completely nonstandard.

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.

They almost certainly run into these issues, but like most of the community, they probably think the cost is well worth bearing, given the advantages the language gives you.

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.

Worth noting that the presenter of this talk has done a complete 180 on subtyping as he's now using subtyping and variance in the core of his flagship library ZIO. He realized it was sometimes better to use the language's strengths rather than denigrate them for "ideological" reasons.

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.

(I'm not the person you were asking, but:)

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.

> but parallelism is also a base fact of many problem domains, where you have multiple agents (up to and including humans) collaborating and interacting simultaneously.

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.

> the functional perl approach here I also find confusing so there is no attempt to distill the essence of what's going on

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!

> It would be difficult to just stumble on a system like Simple-sub without that guidance

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!

Hi, author here. Just wanted to say that you should read the paper rather than the blog post, as the paper is more recent. It's in open access (and CC-BY license) here: https://infoscience.epfl.ch/record/278576

I think it's safe to say that the inspiration for Java lambda almost certainly did not come from the "FP zeitgeist" you're describing, but simply from other JVM languages like Scala and Clojure, which showed how useful they were and how they could be done nicely on the JVM.

> building for papers and PhDs rather than real customers

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

If by "all constructions wiht HKTs", you mean what can be done with HKTs in Haskell, then I'd say yes. It is well-known that ML modules provide a very advanced level of expressiveness, especially since OCaml's introduction of first-class modules. Also, Scala took this idea further and provides principled recursive first-class modules (which Scala calls dependent object types).

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.

> The first example disproved ionforce's claim that default values cannot be constructed dynamically.

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

What does this have to do with the original assertion that "one of Odersky's motives in creating Scala was bringing the power of Haskell into the JVM world"?

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.

> Haskell's key innovation over ML was HKTs

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.

Your example of nested functions with default arguments does not correspond to what derived implicits do. As a result of implicit resolution, an expression with an arbitrary number of subexpressions may be synthesized, the shape of which depends on the types involves. Default parameters simply cannot do that.

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.