The Little Typer (2018)
This is one of my two favorite books in <i>The Little &lt;X&gt;er</i> series. The other is <i>The Reasoned Schemer</i>.<p><i>The Little Typer</i> provides an introduction to dependent types. These can by used to guarantee things like &quot;applying &#x27;concat&#x27; to a list of length X and list of length Y returns a list of X+Y&quot;. It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Two interesting languages using dependent types are:<p>- Idris. This is basically &quot;Haskell plus dependent types (and minus lazy evaluation)&quot;: <a href="https:&#x2F;&#x2F;www.idris-lang.org&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.idris-lang.org&#x2F;</a><p>- ATS. This is a complex systems-level language with dependent types: <a href="http:&#x2F;&#x2F;www.ats-lang.org&#x2F;" rel="nofollow">http:&#x2F;&#x2F;www.ats-lang.org&#x2F;</a> This fills a niche (vaguely) similar to Rust and Ada Spark, with a focus on speed and safety.<p><i>The Reasoned Schemer</i> 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. (Unification is a powerful technique that shows up in other places, including type checkers.)<p>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&#x27;t expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they&#x27;re still fascinating.