HN user
Your map was very formative for me when I was exploring metal, thanks a lot !
I would love for this Map to be expanded to modern subgenres. There are lot's of subgenres that completely changed in the last decades (notably, the *cores and the tech* ...)
And it's definitely missing Thall (https://www.youtube.com/watch?v=AtV9pcHh8vM). :D
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.
https://regex-generate.github.io/regenerate/ (I'm one of the authors) enumerates all the matching (and non-matching) strings, which incidentally answers the question, but doesn't terminate in the infinite case.
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-re[1] uses a derivative-style construction to lazily build a DFA. The general idea is to use something similar to Owens et al's DFA construction, but doing it inline with some caching, to compile lazily (and building a thomson-like automaton, for group capture). In practice, it is fairly fast, although not as optimized as the Rust crate. :) Derivatives supports several match semantics very easily (ocaml-re does longest, shortest, greedy, non-greedy, first). It indeed doesn't handle unicode matching though (it's possible, there is a prototype implem, but nobody took the time to push it through). Note that it's not difficult to (lazily or not) build a NFA using derivatives as well (with Antimirov's construction).
`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 would encourage you not to use DOIs for software. They are not made for this, and have limitations which are not appropriate.
Instead, use Software Heritage https://www.softwareheritage.org/ , it provides unique identifiers and actually understand repositories, versioning, history, etc. It also allows you to cite the software and even give proper, durable links to point to the code.
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. :)
My understanding is that the difference between fuzz testing and property testing is how the input is crafted. Both can be viewed as a pair of things: a function to generate series of bits as input, and a way to turn these bits into the appropriate data under test.
Property testing generates these bits using a specified distribution, and that's about it. Fuzz testing generates these bits by looking at how the program is executed, and uses a black box to try to explore all paths in the program.
Most libraries for property testing comes with very convenient ways to craft the "input to data" part. Fuzz tools come with an almost magically effective way to craft interesting inputs. The two combines very well (and have been combined in several libraries).
I disagree with the sibling comments: regular expressions should still be about regular languages. It's not because Larry Wall committed yet another atrocity that we should all follow him off the cliff. Perl can keep its monster.
However, that doesn't mean we shouldn't strive for richer feature (within the confine of regularity), or that a parsing library automatically does the job better.
For instance: intersection and complement are regular operators that works very well in regular expressions. lookahead is a regular operator (lookbehind and backreferences are not), etc. Those operators do not necessarily work at all in richer parsing libraries. When added to regular expressions, they should be well handled and optimized by regex engines (which is is currently not the case). There's still work to do, features to add, which require appropriate testing techniques.
That is very limited in practice. In my experience, it doesn't scale to more complex features.
Creating strings that match a regex can be very useful for testing too, as it allows you to fuzz a regex engine without using another regex engine as oracle.
It is indeed quite subtle to be "productive" (that's how we say we will explore both "+"). I wrote a paper about how to do it well a few years ago, with quite a few tricks: https://regex-generate.github.io/regenerate/
Hi steve, since you are around: is there a (formal?) description of how this "niche" layout optimization behaves on ADTs in general, or any documented work on the topic?
Amusingly, I was precisely working today on extra-nice error messages for module type errors in OCaml. :)
My reaction to the title was "But they are not exotic, I use them every day!"
It's definitely the feature I miss the most every time I work in other languages, even presumable "advanced" ones, like Haskell. One notable attempt to add them elsewhere is "modular C"[1].
In france, and in particular in Paris, https://www.geovelo.fr/ is very very good. It knows about various Parisian specialties (going the wrong way on residential street is allowed, temporary bike paths, mixed pedestrian/bike paths, etc) that other apps don't really understand. It also gives multiple paths depending on various criterion.
OsmAnd is also decent. Google map is terribly bad.
Unfortunately, this is not the case as soon as you add grouping! To properly express regular expression with grouping, finite state automatons are not sufficient and you need the theory of transducers which does not admit the same properties (in particular regarding to determinisation).
In french, "la petite reine" (i.e., "the little queen") is a fancy literary idiom for a bicycle. Also, "bicyclette" is a feminine noun.
There is a really easy solution to this: write regexes with combinators.
star (range 'a' 'z')
For instance, this is real code to build a regex parsing URLs (translated in a JS-ish syntax):
let cset = chars => compl(set(chars));
let prefix = (head, tail) => char(head) ++ rep(tail);
let scheme = rep(cset("/:?#")) ++ str("://");
let host = rep(cset("/:?#"));
let port = prefix(':', digit);
let path = rep(prefix('/', cset("/?#")));
let query = prefix('?', cset("#"));
let fragment = prefix('#', any);
let url = scheme ++ host ++ opt(port) ++ path ++ opt(query) ++ opt(fragment);
I'm surprised they chose that algorithm, it's fairly limited and not that efficient.
If your nodes have width, you should read "Improving Walker's Algorithm to Run in Linear Time" (I have an implementation here: https://github.com/Drup/tree_layout)
If your nodes have width and height, you need to read "Drawing Non-layered Tidy Trees in Linear Time"
If you want to go bananas visualizing n-ary trees: https://treevis.net/ :D
A self-contained type-system is called "a logic". There are plenty of logics, many of which are not related to set algebra. Furthermore, many type systems are not directly related to set algebra (for instance, Rust's ownership). There are also more profound reasons (what is the type of a type, cf the notion of impredicativity and questions about decidability), but those are usually of little practical consequences for "mainstream" languages.
With only a logic, you can't show properties about the language. In particular, we like to show that programs that are well typed avoid some errors (like segfaults), or that if an expression ( `log2(length(s))`) has a type (`int`), when you evaluate it to a value, the value (`4`) has the same type. If you want to consider such (nice!) properties, you need to consider the type system and the language together.
For a little bit of context, Robert Lang is what you could call a "modern master" of Origami. He's one of the author who promoted a "whole vision" approach to model design, using lot's of circle/square packing and a very scientific methodology. He's also the author of several books (and some software!) to explain how to design your own models using his techniques.
One of the reason the last model is a new scale of complexity might be that it somehow use "old school" techniques: There is now collapse, no circle packing, it's just straight traditional (hard!) folding from start to finish. Creating such complex models from the traditional tools is usually really hard. It also has a certain elegance to it that is often very pleasing.
For the type system aspects, there are two steps:
1. Learn the theory. Yes, you need to. On this matter, the book "Types and Programming Languages" (or TAPL for short) is the bible: https://www.cis.upenn.edu/~bcpierce/tapl/
2. Implement toy type systems. There are several resources for this, but personally, I like this one: http://plzoo.andrej.com/
This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.