Our great sponsors
-
pie
The Pie language, which accompanies The Little Typer by Friedman and Christiansen (by the-little-typer)
-
This is one of my two favorite books in The Little ...er series. The other is The Rational Schemer. These are two of the most advanced books in the series.
The Little Typer provides an introduction to dependent types. These can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Two interesting languages using dependent types are:
- Idris. This is basically "strict Haskell plus dependent types": https://www.idris-lang.org/)
- ATS. This is a complex systems-level language with dependent types: http://www.ats-lang.org/
The Rational Schemer shows how to build a Prolog-like logic language as a Scheme library. This is a very good introduction to logic programming and the implementation of backtracking and unification is fascinating.
This is an excellent series overall, but these two books are especially good for people who are interested in unusual programming language designs. I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they're still fascinating.
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
And here is a gist that demonstrates how simple it is to implement such a type-safe printf function:
https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr
-
Internally, the Idris2 compiler uses deBruijn numbering for its terms, which is tricky to get right once you start trying to manipulate terms. To help with this, it keeps a list of the names corresponding to the deBruijn indices at the type level. The type checker catches mistakes as you write code to manipulate them (inserting names, removing names, or renaming things).
I ran through some exercises teaching this technique[1]. My take-away as a beginner was that it was a pain to make the compiler happy and my code that the compiler didn't like was actually wrong.
I remember reading someone had written a functional red-black tree (with proof of correctness leveraging dependent types) and said the delete algorithm naturally followed from the types. That has was not my experience (delete wasn't immediately obvious to me), but I need to find some time to give it another go.
The Idris2 docs have an example of a lambda expression interpreter[2] whose terms have a vector of the types in the environment as a type parameter (erased at runtime), to ensure everything is type safe in the resulting interpreter.
Typescript has added some bits of dependent typing. For example, asserting a function returns true if the argument has type X, that a function throws if the argument is falsy, and I think type level string manipulation. They are fairly pragmatic, it's not a research language, so I presume that specific functionality is useful to a lot of people. I've used it a little bit of it to help the type checker infer non-null after my assert function was called.
All of that said, I think people are still exploring how dependent types can be used in practice.
[1]: https://github.com/edwinb/SPLV20/blob/master/Code/Lecture2/E...
