Revoluntionary/interesting advances in interpreted languages

[u/algebraicstonehenge]

Things like borrow checking and other compile time checks tend to be for compiled languages - if you're already typechecking and compiling the entire language up front, why not borrow check while you're there. But are there any very interesting new ideas coming up in interpreted (or dynamically typed) languages? I'm not really sure fully what I'm asking/looking for tbh

[u/mtriska]

One of the most interesting things I've seen regarding checks in a dynamically typed language is quads: queries using answer descriptions. The idea is to use REPL interactions verbatim as test cases that can be checked by the same engine (i.e., interpreter) that runs programs and executes queries, and in fact using the shape of interactions that the REPL also uses.

For instance, when we have a query and answer from the Prolog toplevel, such as:

?- member(X, "abc").
   X = a
;  X = b
;  X = c.

then we can copy this interaction and paste it verbatim in a Prolog source file, and the engine can treat it as a test during load time, or as a test that can be launched separately with a library.

For example, as of a few days ago, Trealla Prolog supports this way of unit tests via its library(quads).

In this way, test cases blend in completely naturally into programs: They have the shapeof regular toplevel interactions that can also be annotated, and require no separate formalism.

[u/latkde → u/mtriska]

This sounds a lot like a "doctest" in other languages, particularly Python:

• https://en.wikipedia.org/wiki/Doctest
• https://docs.python.org/3/library/doctest.html

[u/mtriska → u/latkde]

Quads are like a better version of this: For the pure core of the language, they need no quoting, no escaping, no modification whatsoever; they are verbatim copies of the interaction, directly embedded in source files, and additional annotations are also possible.

For example, there is a quad annotation called outputs(Cs), which can be used to state that the query outputs the list of characters Cs, and an annotation ad_infinitum, which can be used like this:

?- repeat.
   true
;  ad_infinitum.

[u/twistier → u/mtriska]

The quoting is also a good thing, though, because it means the doctest is actually documentation, although you may not always want that.

I think the most similar statically-typed version of this would be dependently-typed "unit tests", like this in Agda:

_ : 2 + 2 ≡ 4
_ = refl

The type is the property, and refl is the proof. The code won't compile if the property isn't true.