Drup

HM is not complex type inference. In fact, among all the approaches you cite, it leads to the simplest type system and the simplest implementation. Moreover, there are lot's of courses, reference implementations, and reasonable extensions for a wide array of features (structural subtyping, qualified types, etc). There are even type-system libraries to make it easy to implement (like Inferno).

When new programmer discover ML-family language, they are often stunned by how lightweight it feels, because you don't have to annotate anything. If your types are not structurally too complicated and you want something really easy to use, HM is still the nicest experience.

Naturally, it's all a tradeoff, and if you want specific features (chiefly: borrows, high-order types, overloading, or Typescript-like features), you will need to abandon complete inference (and use something like bidirectional, most likely).

I'm going to be contrarian: Yes, you should learn about type systems if you want to design a programming language, and decide in full conscience what you need. At the very least, it will give you a concrete idea of what safety means for a programming language.

It doesn't mean you have to use an advanced one, but your choice choose be based on knowledge, not ignorance.

A lot of harm; including the billion dollar mistake, has been done by badly designed type systems from the Java/C/C++ family.

You seem well versed into that corner. Do you have a good (and reasonably complete) introduction/exploration for these memory-efficient data-structure for computation ?

I've been working on memory representation of algebraic data types quite a bit, and I've always wondered if we could combine them with succinct data-structures.

That remark is actually more interesting than you think. As groundbreaking as it was, algorithm W iss far too slow for non-toy languages. All modern HM languages (that I know of) use some form of union-find trickeries, as pioneered by the one presented in the blog post (but also present in resolution-by-constraints approaches employed by Haskell and Scala).

So, in fact, it's actually never algorithm W in non-toy languages. ;)

Side note: this article is originally from 2013 and is considered a must-read by any would-be hackers trying to modify the OCaml typechecker (it's cited in the documentation).

Actually, there is a rather pervasive notion of "soundness" in programming language theory. It has many flavors (because, as you hint, programming languages are quite varied). One of the most simple way of stating it, often dubbed "progress and preservation" is: a well typed program can execute (i.e., it doesn't crash) and returns a value of the same type.

This obviously covers type safety, but also spatial memory safety, and can be extended to temporal memory safety, and even some concurrency aspects.

This has been proven for fairly large subsets of programming languages and even some full languages (like SML). Unfortunately, it doesn't hold for most mainstream ones, because programming language theory is often ... under-used ... among language designers.

Giuseppe Castagna is a very well known PL researcher, and very seasoned when it comes to gradual types and "structural" types (the static version of duck-typing), which seems like a great fit for Elixir.

Having a good quality and curated regex benchmarks would be quite useful! I hope you plan on having several features, and engines that can only have partial support. That would make for very interesting comparisons.

`ocaml-ctypes` currently supports "reverse-bindings" (making OCaml functions available from C) out-of-the-box and mostly takes care of the intersection you are talking about, so this already works quite well.

The only gain from emiting C code is portability to weird architecture that would be covered by C compilers but not the OCaml one; which is arguably a pretty niche use-case.

I'm the author if anyone has questions. :)

Sigbovik's jokes are of the kind where the premise is completely bonkers. The rest of the development is made with the utmost rigor to highlight said bonkersitude, Reductio ad absurdum.

To everyone in this subthread: sigbovik is a conference published every 1st of April.

This paper is an April's fool joke. I didn't think people could take that one seriously. I guess it's a good April's fool then. :)