<story><title>The Little Typer (2018)</title><url>https://thelittletyper.com/</url></story><parent_chain></parent_chain><comment><author>ekidd</author><text>This is one of my two favorite books in &lt;i&gt;The Little &amp;lt;X&amp;gt;er&lt;/i&gt; series. The other is &lt;i&gt;The Reasoned Schemer&lt;/i&gt;.&lt;p&gt;&lt;i&gt;The Little Typer&lt;/i&gt; provides an introduction to dependent types. These can by used to guarantee things like &amp;quot;applying &amp;#x27;concat&amp;#x27; to a list of length X and list of length Y returns a list of X+Y&amp;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:&lt;p&gt;- Idris. This is basically &amp;quot;Haskell plus dependent types (and minus lazy evaluation)&amp;quot;: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.idris-lang.org&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.idris-lang.org&amp;#x2F;&lt;/a&gt;&lt;p&gt;- ATS. This is a complex systems-level language with dependent types: &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;www.ats-lang.org&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;www.ats-lang.org&amp;#x2F;&lt;/a&gt; This fills a niche (vaguely) similar to Rust and Ada Spark, with a focus on speed and safety.&lt;p&gt;&lt;i&gt;The Reasoned Schemer&lt;/i&gt; 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.)&lt;p&gt;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&amp;#x27;t expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they&amp;#x27;re still fascinating.</text></comment>
<story><title>The Little Typer (2018)</title><url>https://thelittletyper.com/</url></story><parent_chain></parent_chain><comment><author>adamgordonbell</author><text>A very mind-blowing and challenging book about Types.&lt;p&gt;The strange loop talk and my own interview of the authors might give some sense of what it&amp;#x27;s all about. There is also some interesting work online showing how the language used in the book can be created.&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.youtube.com&amp;#x2F;watch?v=VxINoKFm-S4&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.youtube.com&amp;#x2F;watch?v=VxINoKFm-S4&lt;/a&gt;&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;corecursive.com&amp;#x2F;023-little-typer-and-pie-language&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;corecursive.com&amp;#x2F;023-little-typer-and-pie-language&amp;#x2F;&lt;/a&gt;&lt;p&gt;&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;davidchristiansen.dk&amp;#x2F;tutorials&amp;#x2F;nbe&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;davidchristiansen.dk&amp;#x2F;tutorials&amp;#x2F;nbe&amp;#x2F;&lt;/a&gt;</text></comment>