Calling HLists “collections” is misleading. In spite of their name, HLists are actually record types. The only actual list involved is a compile-time list of component types used to form a record type.
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.
In general, Haskell does not do parametric polymorphism through monomorphization. In particular, higher-rank polymorphism becomes unusable if polymorphism is implemented through monomorphization. On the other hand, if I recall correctly, Rust only supports higher-rank polymorphism for lifetimes, which neither have nor need a runtime representation. This is why monomorphization is a viable implementation strategy for Rust generics.
(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.
Two words: loop invariant. Implement a system that figures out the right loop invariant given a problem description (expressed however you want), and you will have made a lot of progress.
Optionals are a better alternative to null. They compose better (i.e., they nest) and play nicely with data abstraction (i.e., you can define an abstract type that hides the fact that its underlying representation is optional), unlike null.
Typed Racket is more ambitious than other attempts at adding types to an underlying untyped language. Namely, Typed Racket guarantees that typed code is never to blame for certain contract violations, and, if any such contract violation happens, it will be properly traced back to an offending piece of untyped code. This is what makes gradual types gradual (as opposed to merely optional), alas, it is also what has been found to have unacceptable overhead.
> It doesn't try to analyze and compare existing programming languages.
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”.
I don't understand in what sense programs can be called “differentiable”. Is the space of programs modulo observational equivalence a manifold to begin with? (I don't think it's Hausdorff or even T1, but I could be wrong.)
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.
You are badly conflating some issues here. How to implement automatic memory management is a runtime design issue. How to enforce proper non-memory resource management is a language design issue. Nothing forbids an implementation of a safe-Rust-like language with a garbage collector. Destructors would still be called deterministically, and destructed objects would still be unusable afterwards, as mandated by the language's semantics. But memory will only be reclaimed during the next garbage collection cycle.
There are other (better!) reasons against cross-language interoperability, though, such as the reduction in static guarantees to an unusable lowest common denominator.
> The problem is, functional programming languages are almost always harder to read than other languages. Haskell is the obvious example
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.
Not too long was it figured out how to reconcile subtyping with type inference. However, this requires doing subtyping in a very specific way, which most users of languages with subtyping will not find pleasing. In particular, the design of the type system must pay very close attention to issues of polarity and existence of certain universal objects in the categories of types. This work caters more to designers and users of ML-style languages who want to add subtyping, than to designers and users of more traditional languages who want to add type inference.
Lately, I am of the idea that the real problem with how we do concurrency is that we have yet to figure out a way to do it without first-class procedures. When we spawn a thread, even in a low language such as C, we use something to the effect of:
The trouble with this approach to concurrency is twofold:
(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.
> Java's semantics are pass-by-value only of you consider that the "values" that are being passed are pointers.
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?
> Your definitions of Ring and PolynomialRing are incomplete because neither specifies the appropriate set of axioms. Because you do not specify those axioms, your type signature is underspecified.
Indeed. Types are not for proving absolutely everything. The rest you have to prove on your own.
> Of course, there do exist type systems which fix this problem by allowing you to specify the axioms to which a Ring or CommutativeRing must conform.
There isn't much value in those. Types are for programming automation. The human brain is for general-purpose theorem proving. What is a real pity is that it is difficult to annotate programs with handwritten proofs.
> and of course now you have to do full-blown theorem proving.
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.