To give a perhaps odious but relatable analogy, a form is a list of questions, but a filled form is not a list of answers - it is a record of answers to the questions in the form.

(Aside: Type checkers essentially see recursive function definitions as applications of a fixed point operator to non-recursive functions. If your function has a rank-1 type but uses polymorphic recursion, the type checker sees it as the application of a rank-2 fixed point operator to a non-recursive function. This is why I see polymorphic recursion as “morally higher-rank polymorphism”, even when the type signatures in your code are ostensibly rank-1 ones. Polymorphic recursion is widely used in Haskell.)

However, IMO, you only need rank-1 polymorphism 95% of the time anyway, so optimizing for the common use case is a good strategy. By far, the main use case for generics is implementing efficient and reasonably reusable data structures and algorithms in a reasonably type-safe way. For this use case, monomorphization and aggressive inlining of small functions are evidently the right things to do. Other uses of generics (say, streaming I/O frameworks) strike me as a lot more questionable.

Relevant paper and talk:

http://www.ccis.northeastern.edu/home/types/publications/gra...

https://www.youtube.com/watch?v=1u1JGwmW0IQ

It does. For example, this theory identifies when and how incorrectly designed programming languages fail to enforce abstractions, very much like how the theory of database normalization identifies when and how incorrectly designed database schemata fail to enforce data integrity constraints.

But perhaps what you mean is “it doesn't try to view existing programming languages under an unwarranted positive light”.

The examples given in the article are merely derivatives of ordinary mathematical functions defined by ordinary mathematical expressions - in particular, there are no sequencing, no conditionals and no loops. So why call them “differentiable programs” when you are actually dealing with ordinary differentiable functions from good old 19th century analysis? We need urgent improvements in the intellectual honesty department.

> Variables are immutable by default, globals are not allowed, functions are pure.

This is a huge non-sequitur.

There are other (better!) reasons against cross-language interoperability, though, such as the reduction in static guarantees to an unusable lowest common denominator.

There are many legitimate reasons to dislike Haskell, such as being hard to parse mechanically, but being hard to read is not one of them.

> F# and other languages ML-style syntax are probably the easiest to read.

The syntax of ML's module language is pretty complicated. You cannot look at those “where type” (SML) and “with type” (OCaml) clauses and tell me with a straight face that they were meant to be easy to read. This syntax makes translucent ascription harder to read than it ought to be. It is so bad that many[0] people work around it in various ways, like using the combination of generative datatypes and transparent ascription as a poor man's translucent ascription.

As for F#, I would not call it ML-style, precisely due to the inability to express modular abstraction.

[0] Relative to the size of the ML community, of course.

    datatype 'a tree = T of 'a * 'a tree list

https://news.ycombinator.com/item?id=13781467

    launch_thread(function, perhaps, some, initial, data);

(0) It forces a hierarchical structure where one continuation of the branching point is deemed the “parent” and the others are deemed the “children”. In particular, if the forking procedure was called by another, only the “parent” continuation may return to the caller. This is unnatural and unnecessarily limiting. Even if you have valid reasons to guarantee that only one continuation will yield control back to the caller (e.g., to enforce linear usage of the caller's resources), the responsibility to yield back to the caller is in itself as a resource like any other, whose usage can be “negotiated” between the continuations.

(1) It brings the complication of first-class procedures when it is often not needed. From a low-level, operational point of view, all you need is the ability to jump to two (or more) places at once, i.e., a multigoto. There is no reason to require each continuation to have a separate lexical scope, which, in my example above, one has to work around by passing “perhaps some local data” to `launch_Thread`. There is also no reason to make “children” continuations first-class objects. If you need to pass around the procedure used to launch a thread between very remote parts of your program, chances are your program's design is completely broken anyway. These things distract the programmer from the central problem in concurrent programming, namely, how to coordinate resource usage by continuations.

All values in Java are indeed either primitives or pointers. You cannot define your own values! How is anyone supposed to call this a high-level language?

So, um, like this?

    signature RING =
    sig
      type t
      val + : t * t -> t
      val * : t * t -> t
      val ~ : t -> t
    end

This is precisely why parametric polymorphism is superior to ad-hoc polymorphism as a way to enable programs to work in previously unanticipated situations. Don't work with concrete use cases, work with the minimum abstract requirements that allow your program to work!

> On the other hand, some mutations will be extremely valuable. For example, it is possible to extend arithmetic to symbolic quantities.

So, for example, like this?

    functor PolynomialRing (R : RING) : RING =
    struct
      type t = R.t list
      
      fun xs + nil = xs
        | nil + ys = ys
        | (x :: xs) + (y :: ys) = R.+ (x, y) :: xs + ys
      
      (* define multiplication and negation too... *)
    end

So I want a proper formal semantics, maybe not for all of Rust, but at least for a fragment interesting enough to express lifetime and mutability concerns. In particular, I want a formal account of interior mutability.

R is objectively a bad programming language. However, it is by no means inaccessible. I have no statistics background whatsoever, and I managed to learn enough R to be dangerous in a mere week. Other than the 1-based indexing and the utterly disgusting dynamic dispatch mechanism (you could simply not to use the latter), R is surprisingly pleasant to use. What I enjoyed the most is that vectors and matrices are first-class values, not objects that are referred to through pointers. It's probably copy-on-write under the hood, but I don't need to care. Hallelujah!