Posts tagged "type-level" on abhinavsarkar.nethttps://abhinavsarkar.net/tags/type-level/feed.atom2021-01-04T00:00:00ZAbhinav Sarkarhttps://abhinavsarkar.net/about/abhinav@abhinavsarkar.nethttps://abhinavsarkar.net/images/favicon.ico© 2017–2023, Abhinav Sarkarhttps://abhinavsarkar.net/posts/type-level-haskell-aoc7/Solving Advent of Code “Handy Haversacks” in Type-level Haskell2021-01-04T00:00:00ZAbhinav Sarkarhttps://abhinavsarkar.net/about/abhinav@abhinavsarkar.net<p>I have been trying to use type-level programming in Haskell to solve interesting problems since I read <a href="https://thinkingwithtypes.com/" target="_blank" rel="noopener">Thinking with Types</a> by <a href="https://reasonablypolymorphic.com/" target="_blank" rel="noopener">Sandy Maguire</a>. Then I found myself solving the problems in <a href="https://adventofcode.com/2020" target="_blank" rel="noopener">Advent of Code 2020</a> and some of them seemed suitable to be solved with type-level programming. So I decided to give it a shot.</p>
<p><p>This post was originally published on <a href="https://abhinavsarkar.net/posts/type-level-haskell-aoc7/?mtm_campaign=feed">abhinavsarkar.net</a>.</p><!--more--></p>
<nav id="toc" class="right-toc"><h3>Contents</h3><ol><li><a href="#type-level-programming">Type-level Programming</a></li><li><a href="#handy-haversacks">Handy Haversacks</a></li><li><a href="#terms-types-and-kinds">Terms, Types, and Kinds</a></li><li><a href="#type-level-primitives">Type-level Primitives</a></li><li><a href="#type-families">Type Families</a></li><li><a href="#setup">Setup</a></li><li><a href="#consuming-strings-at-type-level">Consuming Strings at Type-level</a></li><li><a href="#parsing-at-type-level">Parsing at Type-level</a></li><li><a href="#how-many-bags">How Many Bags?</a></li></ol></nav>
<h2 data-track-content data-content-name="type-level-programming" data-content-piece="type-level-haskell-aoc7" id="type-level-programming">Type-level Programming</h2>
<p>Type-level programming (TLP) is, simply put, using the type system of a language to solve a problem, or a part of a problem. In a way, we already do TLP when we create the right types to represent our problems and solutions in code. The right types do a lot of work for us by making sure that wrong models and states do not compile, hence reducing the solution-space for us. But in some languages like <a href="https://www.haskell.org/" target="_blank" rel="noopener">Haskell</a> and <a href="https://www.idris-lang.org/" target="_blank" rel="noopener">Idris</a>, we can do much more than just crafting the right types. We can leverage the type-system itself for computation! Recent versions of Haskell have introduced superb support for various extensions and primitives to make TLP in Haskell easier than ever before<a href="#fn1" class="footnote-ref" id="fnref1" role="doc-noteref"><sup>1</sup></a>. Let’s use TLP to solve an interesting problem in this post.</p>
<h2 data-track-content data-content-name="handy-haversacks" data-content-piece="type-level-haskell-aoc7" id="handy-haversacks">Handy Haversacks</h2>
<p><a href="https://adventofcode.com/2020/day/7" target="_blank" rel="noopener">Handy Haversacks</a> is the problem for the day seven of Advent of Code 2020<a href="#fn2" class="footnote-ref" id="fnref2" role="doc-noteref"><sup>2</sup></a>. In this problem, our input is a set of rules about some bags. The bags have different colors and may contain zero or more bags of other colors. Here are the rules for the example problem:</p>
<pre class="plain"><code>light red bags contain 1 bright white bag, 2 muted yellow bags.
dark orange bags contain 3 bright white bags, 4 muted yellow bags.
bright white bags contain 1 shiny gold bag.
muted yellow bags contain 2 shiny gold bags, 9 faded blue bags.
shiny gold bags contain 1 dark olive bag, 2 vibrant plum bags.
dark olive bags contain 3 faded blue bags, 4 dotted black bags.
vibrant plum bags contain 5 faded blue bags, 6 dotted black bags.
faded blue bags contain no other bags.
dotted black bags contain no other bags.</code></pre>
<p>We are going to solve the part two of the problem: given the color of a bag, find out how many other bags in total that bag contains. Since the bags can contain more bags, this is a recursive problem. For the rules above, a <code>shiny gold</code> bag contains …</p>
<blockquote>
<p>1 dark olive bag (and the 7 bags within it) plus 2 vibrant plum bags (and the 11 bags within each of those): 1 + 1*7 + 2 + 2*11 = 32 bags!</p>
</blockquote>
<p>At this point, many of the readers would have already solved this problem in their heads: just parse the input to a lookup table and use it to recursively calculate the number of bags. Easy, isn’t it? But what if we want to solve it with type-level programming?</p>
<h2 data-track-content data-content-name="terms-types-and-kinds" data-content-piece="type-level-haskell-aoc7" id="terms-types-and-kinds">Terms, Types, and Kinds</h2>
<p>We are used to working in the world of <em>Terms</em>. Terms are “things” that programs manipulate at the runtime, for example, integers, strings, and user-defined data type instances. Terms have <em>Types</em> which are used by the compiler to prevent certain behaviors at compile-time, even before the programs are run. For example, it prevents you from adding a string to an integer.</p>
<p>The compiler works (or computes) with types instead of terms. This chain goes further. Like terms have types, types have <em>Kinds</em>. Kinds can be thought of as “the types of the Types”. The compiler uses kinds to prevent certain behaviors of the types at compile-time. Let’s use GHCi to explore terms, types, and kinds:</p>
<div class="sourceCode" id="cb2" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb2-1"><a href="#cb2-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">True</span> <span class="co">-- a term</span></span>
<span id="cb2-2"><a href="#cb2-2" aria-hidden="true" tabindex="-1"></a>True</span>
<span id="cb2-3"><a href="#cb2-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">True</span> <span class="co">-- and its type</span></span>
<span id="cb2-4"><a href="#cb2-4" aria-hidden="true" tabindex="-1"></a>True :: Bool</span>
<span id="cb2-5"><a href="#cb2-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Bool</span> <span class="co">-- and the kind of the Bool type</span></span>
<span id="cb2-6"><a href="#cb2-6" aria-hidden="true" tabindex="-1"></a>Bool :: *</span></code></pre></div>
<p>All terms have only one kind: <code class="sourceCode haskell"><span class="op">*</span></code>. That is, all types like <code class="sourceCode haskell"><span class="dt">Int</span></code>, <code class="sourceCode haskell"><span class="dt">String</span></code> and whatever data types we define ourselves, have the kind <code class="sourceCode haskell"><span class="op">*</span></code>.</p>
<p>It’s trivial to create new types in Haskell with <code>data</code> and <code>newtype</code> definitions. How do we go about creating new kinds? The <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-DataKinds" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">DataKinds</span></code></a> extension lets us do that:</p>
<div class="sourceCode" id="cb3" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb3-1"><a href="#cb3-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XDataKinds</span></span>
<span id="cb3-2"><a href="#cb3-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">data</span> <span class="dt">Allow</span> <span class="ot">=</span> <span class="dt">Yes</span> <span class="op">|</span> <span class="dt">No</span></span>
<span id="cb3-3"><a href="#cb3-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">Yes</span> <span class="co">-- Yes is data constructor with type Allow</span></span>
<span id="cb3-4"><a href="#cb3-4" aria-hidden="true" tabindex="-1"></a>Yes :: Allow</span>
<span id="cb3-5"><a href="#cb3-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Allow</span> <span class="co">-- Allow is a type with kind *</span></span>
<span id="cb3-6"><a href="#cb3-6" aria-hidden="true" tabindex="-1"></a>Allow :: *</span>
<span id="cb3-7"><a href="#cb3-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Yes</span> <span class="co">-- Yes is a type too. Its kind is Allow.</span></span>
<span id="cb3-8"><a href="#cb3-8" aria-hidden="true" tabindex="-1"></a>Yes :: Allow</span></code></pre></div>
<p>The <code class="sourceCode haskell"><span class="dt">DataKinds</span></code> extension promotes types to kinds, and data constructors of types to the types of corresponding kinds. In the example above, <code class="sourceCode haskell"><span class="dt">Yes</span></code> and <code class="sourceCode haskell"><span class="dt">No</span></code> are the promoted types of the promoted kind <code class="sourceCode haskell"><span class="dt">Allow</span></code>. Even though the constructors, types, and kinds may have same names, the compiler can tell apart from their context.</p>
<p>Now we know how to create our own kinds. What if we check for the promoted kinds of the built-in types?</p>
<div class="sourceCode" id="cb4" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb4-1"><a href="#cb4-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">True</span></span>
<span id="cb4-2"><a href="#cb4-2" aria-hidden="true" tabindex="-1"></a>True :: Bool</span>
<span id="cb4-3"><a href="#cb4-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dv">1</span><span class="ot"> ::</span> <span class="dt">Int</span></span>
<span id="cb4-4"><a href="#cb4-4" aria-hidden="true" tabindex="-1"></a>1 :: Int :: Int</span>
<span id="cb4-5"><a href="#cb4-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="st">"hello"</span></span>
<span id="cb4-6"><a href="#cb4-6" aria-hidden="true" tabindex="-1"></a>"hello" :: [Char]</span>
<span id="cb4-7"><a href="#cb4-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">True</span></span>
<span id="cb4-8"><a href="#cb4-8" aria-hidden="true" tabindex="-1"></a>True :: Bool</span>
<span id="cb4-9"><a href="#cb4-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dv">1</span></span>
<span id="cb4-10"><a href="#cb4-10" aria-hidden="true" tabindex="-1"></a>1 :: Nat</span>
<span id="cb4-11"><a href="#cb4-11" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="st">"hello"</span></span>
<span id="cb4-12"><a href="#cb4-12" aria-hidden="true" tabindex="-1"></a>"hello" :: Symbol</span></code></pre></div>
<p>As expected, the <code class="sourceCode haskell"><span class="dt">Bool</span></code> type is promoted to the <code class="sourceCode haskell"><span class="dt">Bool</span></code> kind. But numbers and strings have kinds <code class="sourceCode haskell"><span class="dt">Nat</span></code> and <code class="sourceCode haskell"><span class="dt">Symbol</span></code> respectively. What are these new kinds?</p>
<h2 data-track-content data-content-name="type-level-primitives" data-content-piece="type-level-haskell-aoc7" id="type-level-primitives">Type-level Primitives</h2>
<p>To be able to do useful computation at type-level, we need type-level numbers and strings. We can use <a href="https://wiki.haskell.org/Peano_numbers" target="_blank" rel="noopener">Peano numbers</a> to encode natural numbers as a type and use the <code class="sourceCode haskell"><span class="dt">DataKinds</span></code> extension to <a href="https://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html#data-kinds" target="_blank" rel="noopener">promote them to type-level</a>. With numbers as types now, we can use them for interesting things like <a href="https://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html#vectors" target="_blank" rel="noopener">sized vectors</a> with compile-time validation for index bound checks etc. But Peano numbers are awkward to work with because of their verbosity. Fortunately, GHC has built-in support for type-level natural numbers with the <a href="https://hackage.haskell.org/package/base-4.14.1.0/docs/GHC-TypeLits.html" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">GHC.TypeLits</span></code></a> package.</p>
<div class="sourceCode" id="cb5" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb5-1"><a href="#cb5-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dv">1</span> <span class="co">-- 1 is a type-level number here</span></span>
<span id="cb5-2"><a href="#cb5-2" aria-hidden="true" tabindex="-1"></a>1 :: Nat</span>
<span id="cb5-3"><a href="#cb5-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dv">10000</span> <span class="co">-- kind of all type-level numbers is GHC.TypeLits.Nat</span></span>
<span id="cb5-4"><a href="#cb5-4" aria-hidden="true" tabindex="-1"></a>10000 :: Nat</span></code></pre></div>
<p>GHC supports type-level strings as well through the same package. Unlike term-level strings which are lists of <code class="sourceCode haskell"><span class="dt">Char</span></code>s, type-level strings are defined as a primitive and their kind is <code class="sourceCode haskell"><span class="dt">Symbol</span></code><a href="#fn3" class="footnote-ref" id="fnref3" role="doc-noteref"><sup>3</sup></a>.</p>
<div class="sourceCode" id="cb6" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb6-1"><a href="#cb6-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="st">"hello at type-level"</span></span>
<span id="cb6-2"><a href="#cb6-2" aria-hidden="true" tabindex="-1"></a>"hello at type-level" :: Symbol</span></code></pre></div>
<p>GHC also supports type-level lists and tuples. Type-level lists can contain zero or more types of same kind, while type-level tuples can contain zero or more types of possibly different kinds.</p>
<div class="sourceCode" id="cb7" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb7-1"><a href="#cb7-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind [<span class="dv">1</span>, <span class="dv">2</span>, <span class="dv">3</span>]</span>
<span id="cb7-2"><a href="#cb7-2" aria-hidden="true" tabindex="-1"></a>[1, 2, 3] :: [Nat]</span>
<span id="cb7-3"><a href="#cb7-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind [<span class="st">"hello"</span>, <span class="st">"world"</span>]</span>
<span id="cb7-4"><a href="#cb7-4" aria-hidden="true" tabindex="-1"></a>["hello", "world"] :: [Symbol]</span>
<span id="cb7-5"><a href="#cb7-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="co">-- prefix the tuple with ' to disambiguate it as a type-level tuple</span></span>
<span id="cb7-6"><a href="#cb7-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind '(<span class="dv">1</span>, <span class="st">"one"</span>)</span>
<span id="cb7-7"><a href="#cb7-7" aria-hidden="true" tabindex="-1"></a>'(1, "one") :: (Nat, Symbol)</span></code></pre></div>
<p>Now we are familiar with the primitives for type-level computations. How exactly do we do these computations though?</p>
<h2 data-track-content data-content-name="type-families" data-content-piece="type-level-haskell-aoc7" id="type-families">Type Families</h2>
<p><em>Type families</em> can be thought of as functions that work at type-level. Just like we use functions to do computations at term-level, we use type families to do computations at type-level. Type families are enabled by the <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeFamilies" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">TypeFamilies</span></code></a> extension<a href="#fn4" class="footnote-ref" id="fnref4" role="doc-noteref"><sup>4</sup></a>.</p>
<p>Let’s write a simple type family to compute the logical conjunction of two type-level booleans:</p>
<div class="sourceCode" id="cb8" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb8-1"><a href="#cb8-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeFamilies</span></span>
<span id="cb8-2"><a href="#cb8-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">+</span>m</span>
<span id="cb8-3"><a href="#cb8-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">type</span> <span class="kw">family</span> <span class="dt">And</span> (<span class="ot">x ::</span> <span class="dt">Bool</span>) (<span class="ot">y ::</span> <span class="dt">Bool</span>)<span class="ot"> ::</span> <span class="dt">Bool</span> <span class="kw">where</span></span>
<span id="cb8-4"><a href="#cb8-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">And</span> <span class="dt">True</span> <span class="dt">True</span> <span class="ot">=</span> <span class="dt">True</span></span>
<span id="cb8-5"><a href="#cb8-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">And</span> _ _ <span class="ot">=</span> <span class="dt">False</span></span>
<span id="cb8-6"><a href="#cb8-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span></span>
<span id="cb8-7"><a href="#cb8-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">And</span></span>
<span id="cb8-8"><a href="#cb8-8" aria-hidden="true" tabindex="-1"></a>And :: Bool -> Bool -> Bool</span>
<span id="cb8-9"><a href="#cb8-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">And</span> <span class="dt">True</span> <span class="dt">False</span></span>
<span id="cb8-10"><a href="#cb8-10" aria-hidden="true" tabindex="-1"></a>And True False :: Bool</span>
<span id="cb8-11"><a href="#cb8-11" aria-hidden="true" tabindex="-1"></a>= 'False</span>
<span id="cb8-12"><a href="#cb8-12" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">And</span> <span class="dt">True</span> <span class="dt">True</span></span>
<span id="cb8-13"><a href="#cb8-13" aria-hidden="true" tabindex="-1"></a>And True True :: Bool</span>
<span id="cb8-14"><a href="#cb8-14" aria-hidden="true" tabindex="-1"></a>= 'True</span>
<span id="cb8-15"><a href="#cb8-15" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">And</span> <span class="dt">False</span> <span class="dt">True</span></span>
<span id="cb8-16"><a href="#cb8-16" aria-hidden="true" tabindex="-1"></a>And False True :: Bool</span>
<span id="cb8-17"><a href="#cb8-17" aria-hidden="true" tabindex="-1"></a>= 'False</span></code></pre></div>
<p>Kind of <code>And</code> shows that it is a function at type-level. We apply it using the <code>:kind!</code> command in GHCi to see that it indeed works as expected.</p>
<p>GHC comes with some useful type families to do computations on <code class="sourceCode haskell"><span class="dt">Nat</span></code>s and <code class="sourceCode haskell"><span class="dt">Symbol</span></code>s in the <code class="sourceCode haskell"><span class="dt">GHC.TypeLits</span></code> package. Let’s see them in action:</p>
<div class="sourceCode" id="cb9" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb9-1"><a href="#cb9-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">import</span> <span class="dt">GHC.TypeLits</span></span>
<span id="cb9-2"><a href="#cb9-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeOperators</span></span>
<span id="cb9-3"><a href="#cb9-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dv">1</span> <span class="op">+</span> <span class="dv">2</span> <span class="co">-- addition at type-level</span></span>
<span id="cb9-4"><a href="#cb9-4" aria-hidden="true" tabindex="-1"></a>1 + 2 :: Nat</span>
<span id="cb9-5"><a href="#cb9-5" aria-hidden="true" tabindex="-1"></a>= 3</span>
<span id="cb9-6"><a href="#cb9-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">CmpNat</span> <span class="dv">1</span> <span class="dv">2</span> <span class="co">-- comparison at type-level, return lifted Ordering</span></span>
<span id="cb9-7"><a href="#cb9-7" aria-hidden="true" tabindex="-1"></a>CmpNat 1 2 :: Ordering</span>
<span id="cb9-8"><a href="#cb9-8" aria-hidden="true" tabindex="-1"></a>= 'LT</span>
<span id="cb9-9"><a href="#cb9-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">AppendSymbol</span> <span class="st">"hello"</span> <span class="st">"world"</span> <span class="co">-- appending two symbols at type-level</span></span>
<span id="cb9-10"><a href="#cb9-10" aria-hidden="true" tabindex="-1"></a>AppendSymbol "hello" "world" :: Symbol</span>
<span id="cb9-11"><a href="#cb9-11" aria-hidden="true" tabindex="-1"></a>= "helloworld"</span></code></pre></div>
<p>The <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeOperators" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">TypeOperators</span></code></a> extension enables us to define and use type families with symbolic names.</p>
<p>We have learned the basics of TLP in Haskell. Next, we can proceed to solve the actual problem.</p>
<h2 data-track-content data-content-name="setup" data-content-piece="type-level-haskell-aoc7" id="setup">Setup</h2>
<p>This post is written in a literate programming style, meaning if you take all the code snippets from the post (excluding the GHCi examples) in the order they appear and put them in a file, you’ll have a real working program. First go the extensions and imports:</p>
<div class="sourceCode" id="cb10" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb10-1"><a href="#cb10-1" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE DataKinds, TypeFamilies #-}</span></span>
<span id="cb10-2"><a href="#cb10-2" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE TypeOperators, UndecidableInstances #-}</span></span>
<span id="cb10-3"><a href="#cb10-3" aria-hidden="true" tabindex="-1"></a><span class="kw">module</span> <span class="dt">AoC7</span> <span class="kw">where</span></span>
<span id="cb10-4"><a href="#cb10-4" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb10-5"><a href="#cb10-5" aria-hidden="true" tabindex="-1"></a><span class="kw">import</span> <span class="dt">Data.Proxy</span></span>
<span id="cb10-6"><a href="#cb10-6" aria-hidden="true" tabindex="-1"></a><span class="kw">import</span> <span class="dt">Data.Symbol.Ascii</span></span>
<span id="cb10-7"><a href="#cb10-7" aria-hidden="true" tabindex="-1"></a><span class="kw">import</span> <span class="dt">GHC.TypeLits</span></span>
<span id="cb10-8"><a href="#cb10-8" aria-hidden="true" tabindex="-1"></a><span class="kw">import</span> <span class="dt">Prelude</span> <span class="kw">hiding</span> (words, reverse)</span></code></pre></div>
<p>We have already encountered some of these extensions in the sections above. We’ll learn about the rest of them as we go along.</p>
<h2 data-track-content data-content-name="consuming-strings-at-type-level" data-content-piece="type-level-haskell-aoc7" id="consuming-strings-at-type-level">Consuming Strings at Type-level</h2>
<p>The first capability required for parsing is to consume the input string character-by-character. It’s easy to do that with term-level strings as they are simply lists of characters. But <code class="sourceCode haskell"><span class="dt">Symbol</span></code>s are built-in primitives and cannot be consumed character-by-character using the built-in functionalities. Therefore, the first thing we should do is to figure out how to break a symbol into its constituent characters. Fortunately for us, the <a href="https://hackage.haskell.org/package/symbols-0.3.0.0" target="_blank" rel="noopener"><code>symbols</code></a> library implements just that with the <a href="https://hackage.haskell.org/package/symbols-0.3.0.0/docs/Data-Symbol-Ascii.html#t:ToList" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">ToList</span></code></a> type family<a href="#fn5" class="footnote-ref" id="fnref5" role="doc-noteref"><sup>5</sup></a>. It also provide a few more utilities to work with symbols which we use later for solving our problem. Let’s see what <code>ToList</code> gives us:</p>
<div class="sourceCode" id="cb11" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb11-1"><a href="#cb11-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">import</span> <span class="dt">Data.Symbol.Ascii</span> (<span class="dt">ToList</span>)</span>
<span id="cb11-2"><a href="#cb11-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="st">"hello there"</span></span>
<span id="cb11-3"><a href="#cb11-3" aria-hidden="true" tabindex="-1"></a>"hello there" :: Symbol</span>
<span id="cb11-4"><a href="#cb11-4" aria-hidden="true" tabindex="-1"></a>= "hello there"</span>
<span id="cb11-5"><a href="#cb11-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">ToList</span> <span class="st">"hello there"</span></span>
<span id="cb11-6"><a href="#cb11-6" aria-hidden="true" tabindex="-1"></a>ToList "hello there" :: [Symbol]</span>
<span id="cb11-7"><a href="#cb11-7" aria-hidden="true" tabindex="-1"></a>= '["h", "e", "l", "l", "o", " ", "t", "h", "e", "r", "e"]</span></code></pre></div>
<p>It does what we want. However, for the purpose of parsing rules for this problem, it’s better to have the symbols broken as words. We already have the capability to break a symbol into a list of symbols of its characters. Now, we can combine the character symbols to create a list of word symbols.</p>
<p>We start with solving this problem with a term-level function. It is like the <a href="https://hackage.haskell.org/package/base-4.14.1.0/docs/Prelude.html#v:words" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="fu">words</span></code></a> function from the Prelude but of type <code class="sourceCode haskell">[<span class="dt">String</span>] <span class="ot">-></span> [<span class="dt">String</span>]</code> instead of <code class="sourceCode haskell"><span class="dt">String</span> <span class="ot">-></span> [<span class="dt">String</span>]</code>.</p>
<div class="sourceCode" id="cb12" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb12-1"><a href="#cb12-1" aria-hidden="true" tabindex="-1"></a><span class="fu">words</span><span class="ot"> ::</span> [<span class="dt">String</span>] <span class="ot">-></span> [<span class="dt">String</span>]</span>
<span id="cb12-2"><a href="#cb12-2" aria-hidden="true" tabindex="-1"></a><span class="fu">words</span> s <span class="ot">=</span> <span class="fu">reverse</span> <span class="op">$</span> words2 [] s</span>
<span id="cb12-3"><a href="#cb12-3" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb12-4"><a href="#cb12-4" aria-hidden="true" tabindex="-1"></a><span class="ot">words2 ::</span> [<span class="dt">String</span>] <span class="ot">-></span> [<span class="dt">String</span>] <span class="ot">-></span> [<span class="dt">String</span>]</span>
<span id="cb12-5"><a href="#cb12-5" aria-hidden="true" tabindex="-1"></a>words2 acc [] <span class="ot">=</span> acc</span>
<span id="cb12-6"><a href="#cb12-6" aria-hidden="true" tabindex="-1"></a>words2 [] (<span class="st">" "</span><span class="op">:</span>xs) <span class="ot">=</span> words2 [] xs</span>
<span id="cb12-7"><a href="#cb12-7" aria-hidden="true" tabindex="-1"></a>words2 [] (x<span class="op">:</span>xs) <span class="ot">=</span> words2 [x] xs</span>
<span id="cb12-8"><a href="#cb12-8" aria-hidden="true" tabindex="-1"></a>words2 acc (<span class="st">" "</span><span class="op">:</span>xs) <span class="ot">=</span> words2 (<span class="st">""</span><span class="op">:</span>acc) xs</span>
<span id="cb12-9"><a href="#cb12-9" aria-hidden="true" tabindex="-1"></a>words2 (a<span class="op">:</span>as) (x<span class="op">:</span>xs) <span class="ot">=</span> words2 ((a <span class="op">++</span> x)<span class="op">:</span>as) xs</span>
<span id="cb12-10"><a href="#cb12-10" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb12-11"><a href="#cb12-11" aria-hidden="true" tabindex="-1"></a><span class="fu">reverse</span><span class="ot"> ::</span> [a] <span class="ot">-></span> [a]</span>
<span id="cb12-12"><a href="#cb12-12" aria-hidden="true" tabindex="-1"></a><span class="fu">reverse</span> l <span class="ot">=</span> rev l []</span>
<span id="cb12-13"><a href="#cb12-13" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb12-14"><a href="#cb12-14" aria-hidden="true" tabindex="-1"></a><span class="ot">rev ::</span> [a] <span class="ot">-></span> [a] <span class="ot">-></span> [a]</span>
<span id="cb12-15"><a href="#cb12-15" aria-hidden="true" tabindex="-1"></a>rev [] a <span class="ot">=</span> a</span>
<span id="cb12-16"><a href="#cb12-16" aria-hidden="true" tabindex="-1"></a>rev (x<span class="op">:</span>xs) a <span class="ot">=</span> rev xs (x<span class="op">:</span>a)</span></code></pre></div>
<p>This code may look unidiomatic Haskell but it’s written this way because we have to translate it to the type families version and type families do not support <code class="sourceCode haskell"><span class="kw">let</span></code> or <code class="sourceCode haskell"><span class="kw">where</span></code> bindings and <code class="sourceCode haskell"><span class="kw">case</span></code> or <code class="sourceCode haskell"><span class="kw">if</span></code> constructs. They support only recursion and pattern matching.</p>
<p><code class="sourceCode haskell"><span class="fu">words</span></code> works as expected:</p>
<div class="sourceCode" id="cb13" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb13-1"><a href="#cb13-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="fu">words</span> [<span class="st">"h"</span>, <span class="st">"e"</span>, <span class="st">"l"</span>, <span class="st">"l"</span>, <span class="st">"o"</span>, <span class="st">" "</span>, <span class="st">"t"</span>, <span class="st">"h"</span>, <span class="st">"e"</span>, <span class="st">"r"</span>, <span class="st">"e"</span>]</span>
<span id="cb13-2"><a href="#cb13-2" aria-hidden="true" tabindex="-1"></a>["hello","there"]</span></code></pre></div>
<p>Translating <code>words</code> to type-level is almost mechanical. Starting with the last function above:</p>
<div class="sourceCode" id="cb14" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb14-1"><a href="#cb14-1" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span></span>
<span id="cb14-2"><a href="#cb14-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">Rev</span> (<span class="ot">acc ::</span> [<span class="dt">Symbol</span>]) (<span class="ot">chrs ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> [<span class="dt">Symbol</span>] <span class="kw">where</span></span>
<span id="cb14-3"><a href="#cb14-3" aria-hidden="true" tabindex="-1"></a> <span class="dt">Rev</span> '[] a <span class="ot">=</span> a</span>
<span id="cb14-4"><a href="#cb14-4" aria-hidden="true" tabindex="-1"></a> <span class="dt">Rev</span> (x <span class="op">:</span> xs) a <span class="ot">=</span> <span class="dt">Rev</span> xs (x <span class="op">:</span> a)</span>
<span id="cb14-5"><a href="#cb14-5" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb14-6"><a href="#cb14-6" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">Reverse</span> (<span class="ot">chrs ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> [<span class="dt">Symbol</span>] <span class="kw">where</span></span>
<span id="cb14-7"><a href="#cb14-7" aria-hidden="true" tabindex="-1"></a> <span class="dt">Reverse</span> l <span class="ot">=</span> <span class="dt">Rev</span> l '[]</span>
<span id="cb14-8"><a href="#cb14-8" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb14-9"><a href="#cb14-9" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">Words2</span> (<span class="ot">acc ::</span> [<span class="dt">Symbol</span>]) (<span class="ot">chrs ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> [<span class="dt">Symbol</span>] <span class="kw">where</span></span>
<span id="cb14-10"><a href="#cb14-10" aria-hidden="true" tabindex="-1"></a> <span class="dt">Words2</span> acc '[] <span class="ot">=</span> acc</span>
<span id="cb14-11"><a href="#cb14-11" aria-hidden="true" tabindex="-1"></a> <span class="dt">Words2</span> '[] (<span class="st">" "</span> <span class="op">:</span> xs) <span class="ot">=</span> <span class="dt">Words2</span> '[] xs</span>
<span id="cb14-12"><a href="#cb14-12" aria-hidden="true" tabindex="-1"></a> <span class="dt">Words2</span> '[] (x <span class="op">:</span> xs) <span class="ot">=</span> <span class="dt">Words2</span> '[x] xs</span>
<span id="cb14-13"><a href="#cb14-13" aria-hidden="true" tabindex="-1"></a> <span class="dt">Words2</span> acc (<span class="st">" "</span> <span class="op">:</span> xs) <span class="ot">=</span> <span class="dt">Words2</span> (<span class="st">""</span> <span class="op">:</span> acc) xs</span>
<span id="cb14-14"><a href="#cb14-14" aria-hidden="true" tabindex="-1"></a> <span class="dt">Words2</span> (a <span class="op">:</span> as) (x <span class="op">:</span> xs) <span class="ot">=</span> <span class="dt">Words2</span> (<span class="dt">AppendSymbol</span> a x <span class="op">:</span> as) xs</span>
<span id="cb14-15"><a href="#cb14-15" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb14-16"><a href="#cb14-16" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">Words</span> (<span class="ot">chrs ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> [<span class="dt">Symbol</span>] <span class="kw">where</span></span>
<span id="cb14-17"><a href="#cb14-17" aria-hidden="true" tabindex="-1"></a> <span class="dt">Words</span> s <span class="ot">=</span> <span class="dt">Reverse</span> (<span class="dt">Words2</span> '[] s)</span></code></pre></div>
<p>We need the <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#type-family-decidability" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">UndecidableInstances</span></code></a> extension to write these type families. This extension relaxes some rules that GHC places to make sure that type inference in the compiler terminates. In other words, this extension lets us write recursive code at type-level which may never terminate. Since GHC cannot prove that the recursion terminates, it’s up to us programmers to make sure that it does.</p>
<p>Let’s see if it works:</p>
<div class="sourceCode" id="cb15" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb15-1"><a href="#cb15-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">ToList</span> <span class="st">"hello there"</span></span>
<span id="cb15-2"><a href="#cb15-2" aria-hidden="true" tabindex="-1"></a>ToList "hello there" :: [Symbol]</span>
<span id="cb15-3"><a href="#cb15-3" aria-hidden="true" tabindex="-1"></a>= '["h", "e", "l", "l", "o", " ", "t", "h", "e", "r", "e"]</span>
<span id="cb15-4"><a href="#cb15-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">Words</span> (<span class="dt">ToList</span> <span class="st">"hello there"</span>)</span>
<span id="cb15-5"><a href="#cb15-5" aria-hidden="true" tabindex="-1"></a>Words (ToList "hello there") :: [Symbol]</span>
<span id="cb15-6"><a href="#cb15-6" aria-hidden="true" tabindex="-1"></a>= '["hello", "there"]</span></code></pre></div>
<p>Great! Now we can move on to the actual parsing of the rules.</p>
<h2 data-track-content data-content-name="parsing-at-type-level" data-content-piece="type-level-haskell-aoc7" id="parsing-at-type-level">Parsing at Type-level</h2>
<p>Here are the rules of the problem as a list of symbols:</p>
<div class="sourceCode" id="cb16" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb16-1"><a href="#cb16-1" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="dt">Rules</span> <span class="ot">=</span> [</span>
<span id="cb16-2"><a href="#cb16-2" aria-hidden="true" tabindex="-1"></a> <span class="st">"light red bags contain 1 bright white bag, 2 muted yellow bags."</span></span>
<span id="cb16-3"><a href="#cb16-3" aria-hidden="true" tabindex="-1"></a> , <span class="st">"dark orange bags contain 3 bright white bags, 4 muted yellow bags."</span></span>
<span id="cb16-4"><a href="#cb16-4" aria-hidden="true" tabindex="-1"></a> , <span class="st">"bright white bags contain 1 shiny gold bag."</span></span>
<span id="cb16-5"><a href="#cb16-5" aria-hidden="true" tabindex="-1"></a> , <span class="st">"muted yellow bags contain 2 shiny gold bags, 9 faded blue bags."</span></span>
<span id="cb16-6"><a href="#cb16-6" aria-hidden="true" tabindex="-1"></a> , <span class="st">"shiny gold bags contain 1 dark olive bag, 2 vibrant plum bags."</span></span>
<span id="cb16-7"><a href="#cb16-7" aria-hidden="true" tabindex="-1"></a> , <span class="st">"dark olive bags contain 3 faded blue bags, 4 dotted black bags."</span></span>
<span id="cb16-8"><a href="#cb16-8" aria-hidden="true" tabindex="-1"></a> , <span class="st">"vibrant plum bags contain 5 faded blue bags, 6 dotted black bags."</span></span>
<span id="cb16-9"><a href="#cb16-9" aria-hidden="true" tabindex="-1"></a> , <span class="st">"faded blue bags contain no other bags."</span></span>
<span id="cb16-10"><a href="#cb16-10" aria-hidden="true" tabindex="-1"></a> , <span class="st">"dotted black bags contain no other bags."</span></span>
<span id="cb16-11"><a href="#cb16-11" aria-hidden="true" tabindex="-1"></a> ]</span></code></pre></div>
<p>We can see that the rules always start with the color of the container bag. Then they go on to either say that such-and-such bags “contain no other bags.” or list out the counts of one or more contained colored bags. We capture this model in a new type (and kind!):</p>
<div class="sourceCode" id="cb17" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb17-1"><a href="#cb17-1" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">Bag</span> <span class="ot">=</span> <span class="dt">EmptyBag</span> <span class="dt">Symbol</span> <span class="op">|</span> <span class="dt">FilledBag</span> <span class="dt">Symbol</span> [(<span class="dt">Nat</span>, <span class="dt">Symbol</span>)]</span></code></pre></div>
<p>A <code class="sourceCode haskell"><span class="dt">Bag</span></code> is either an <code class="sourceCode haskell"><span class="dt">EmptyBag</span></code> with a color or a <code class="sourceCode haskell"><span class="dt">FilledBag</span></code> with a color and a list of tuples of count of contained bags along with their colors.</p>
<p>Next, we write the parsing logic at type-level which works on word symbols, directly as type families this time:</p>
<div class="sourceCode" id="cb18" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb18-1"><a href="#cb18-1" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">Parse</span> (<span class="ot">wrds ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> <span class="dt">Bag</span> <span class="kw">where</span></span>
<span id="cb18-2"><a href="#cb18-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">Parse</span> (color1 <span class="op">:</span> color2 <span class="op">:</span> <span class="st">"bags"</span> <span class="op">:</span> <span class="st">"contain"</span> <span class="op">:</span> rest) <span class="ot">=</span></span>
<span id="cb18-3"><a href="#cb18-3" aria-hidden="true" tabindex="-1"></a> <span class="dt">Parse2</span> (<span class="dt">AppendSymbol</span> color1 (<span class="dt">AppendSymbol</span> <span class="st">" "</span> color2)) rest</span>
<span id="cb18-4"><a href="#cb18-4" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb18-5"><a href="#cb18-5" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">Parse2</span> (<span class="ot">color ::</span> <span class="dt">Symbol</span>) (<span class="ot">wrds ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> <span class="dt">Bag</span> <span class="kw">where</span></span>
<span id="cb18-6"><a href="#cb18-6" aria-hidden="true" tabindex="-1"></a> <span class="dt">Parse2</span> color (<span class="st">"no"</span> <span class="op">:</span> _) <span class="ot">=</span> <span class="dt">EmptyBag</span> color</span>
<span id="cb18-7"><a href="#cb18-7" aria-hidden="true" tabindex="-1"></a> <span class="dt">Parse2</span> color rest <span class="ot">=</span> <span class="dt">FilledBag</span> color (<span class="dt">Parse3</span> rest)</span>
<span id="cb18-8"><a href="#cb18-8" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb18-9"><a href="#cb18-9" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">Parse3</span> (<span class="ot">wrds ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> [(<span class="dt">Nat</span>, <span class="dt">Symbol</span>)] <span class="kw">where</span></span>
<span id="cb18-10"><a href="#cb18-10" aria-hidden="true" tabindex="-1"></a> <span class="dt">Parse3</span> '[] <span class="ot">=</span> '[]</span>
<span id="cb18-11"><a href="#cb18-11" aria-hidden="true" tabindex="-1"></a> <span class="dt">Parse3</span> (count <span class="op">:</span> color1 <span class="op">:</span> color2 <span class="op">:</span> _ <span class="op">:</span> rest) <span class="ot">=</span></span>
<span id="cb18-12"><a href="#cb18-12" aria-hidden="true" tabindex="-1"></a> ('(<span class="dt">ReadNat</span> count, <span class="dt">AppendSymbol</span> color1 (<span class="dt">AppendSymbol</span> <span class="st">" "</span> color2)) <span class="op">:</span> <span class="dt">Parse3</span> rest)</span></code></pre></div>
<p>The <code class="sourceCode haskell"><span class="dt">Parse</span></code> type family parses a list of word symbols into the <code class="sourceCode haskell"><span class="dt">Bag</span></code> type. The logic is straightforward, if a little verbose compared to the equivalent term-level code. We use the <code class="sourceCode haskell"><span class="dt">AppendSymbol</span></code> type family to put word symbols together and the <a href="https://hackage.haskell.org/package/symbols-0.3.0.0/docs/Data-Symbol-Ascii.html#t:ReadNat" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">ReadNat</span></code></a> type family to convert a <code class="sourceCode haskell"><span class="dt">Symbol</span></code> into a <code class="sourceCode haskell"><span class="dt">Nat</span></code>. The rest is pattern matching and recursion. A quick test in GHCi reveals that it works:</p>
<div class="sourceCode" id="cb19" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb19-1"><a href="#cb19-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb19-2"><a href="#cb19-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">Parse</span></span>
<span id="cb19-3"><a href="#cb19-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> (<span class="dt">Words</span> (<span class="dt">ToList</span> <span class="st">"light red bags contain 1 bright white bag, 2 muted yellow bags."</span>))</span>
<span id="cb19-4"><a href="#cb19-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb19-5"><a href="#cb19-5" aria-hidden="true" tabindex="-1"></a>Parse (Words (ToList "light red bags contain 1 bright white bag, 2 muted yellow bags.")) :: Bag</span>
<span id="cb19-6"><a href="#cb19-6" aria-hidden="true" tabindex="-1"></a>= 'FilledBag</span>
<span id="cb19-7"><a href="#cb19-7" aria-hidden="true" tabindex="-1"></a> "light red" '[ '(1, "bright white"), '(2, "muted yellow")]</span>
<span id="cb19-8"><a href="#cb19-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">Parse</span> (<span class="dt">Words</span> (<span class="dt">ToList</span> <span class="st">"bright white bags contain 1 shiny gold bag."</span>))</span>
<span id="cb19-9"><a href="#cb19-9" aria-hidden="true" tabindex="-1"></a>Parse (Words (ToList "bright white bags contain 1 shiny gold bag.")) :: Bag</span>
<span id="cb19-10"><a href="#cb19-10" aria-hidden="true" tabindex="-1"></a>= 'FilledBag "bright white" '[ '(1, "shiny gold")]</span>
<span id="cb19-11"><a href="#cb19-11" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">Parse</span> (<span class="dt">Words</span> (<span class="dt">ToList</span> <span class="st">"faded blue bags contain no other bags."</span>))</span>
<span id="cb19-12"><a href="#cb19-12" aria-hidden="true" tabindex="-1"></a>Parse (Words (ToList "faded blue bags contain no other bags.")) :: Bag</span>
<span id="cb19-13"><a href="#cb19-13" aria-hidden="true" tabindex="-1"></a>= 'EmptyBag "faded blue"</span></code></pre></div>
<p>Finally, we parse all rules into a list of <code class="sourceCode haskell"><span class="dt">Bag</span></code>s:</p>
<div class="sourceCode" id="cb20" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb20-1"><a href="#cb20-1" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">ParseRules</span> (<span class="ot">rules ::</span> [<span class="dt">Symbol</span>])<span class="ot"> ::</span> [<span class="dt">Bag</span>] <span class="kw">where</span></span>
<span id="cb20-2"><a href="#cb20-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">ParseRules</span> '[] <span class="ot">=</span> '[]</span>
<span id="cb20-3"><a href="#cb20-3" aria-hidden="true" tabindex="-1"></a> <span class="dt">ParseRules</span> (rule <span class="op">:</span> rest) <span class="ot">=</span> (<span class="dt">Parse</span> (<span class="dt">Words</span> (<span class="dt">ToList</span> rule)) <span class="op">:</span> <span class="dt">ParseRules</span> rest)</span>
<span id="cb20-4"><a href="#cb20-4" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb20-5"><a href="#cb20-5" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="dt">Bags</span> <span class="ot">=</span> <span class="dt">ParseRules</span> <span class="dt">Rules</span></span></code></pre></div>
<p>And validate that it works:</p>
<div class="sourceCode" id="cb21" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb21-1"><a href="#cb21-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">Bags</span></span>
<span id="cb21-2"><a href="#cb21-2" aria-hidden="true" tabindex="-1"></a>Bags :: [Bag]</span>
<span id="cb21-3"><a href="#cb21-3" aria-hidden="true" tabindex="-1"></a>= '[ 'FilledBag</span>
<span id="cb21-4"><a href="#cb21-4" aria-hidden="true" tabindex="-1"></a> "light red" '[ '(1, "bright white"), '(2, "muted yellow")],</span>
<span id="cb21-5"><a href="#cb21-5" aria-hidden="true" tabindex="-1"></a> 'FilledBag</span>
<span id="cb21-6"><a href="#cb21-6" aria-hidden="true" tabindex="-1"></a> "dark orange" '[ '(3, "bright white"), '(4, "muted yellow")],</span>
<span id="cb21-7"><a href="#cb21-7" aria-hidden="true" tabindex="-1"></a> 'FilledBag "bright white" '[ '(1, "shiny gold")],</span>
<span id="cb21-8"><a href="#cb21-8" aria-hidden="true" tabindex="-1"></a> 'FilledBag</span>
<span id="cb21-9"><a href="#cb21-9" aria-hidden="true" tabindex="-1"></a> "muted yellow" '[ '(2, "shiny gold"), '(9, "faded blue")],</span>
<span id="cb21-10"><a href="#cb21-10" aria-hidden="true" tabindex="-1"></a> 'FilledBag</span>
<span id="cb21-11"><a href="#cb21-11" aria-hidden="true" tabindex="-1"></a> "shiny gold" '[ '(1, "dark olive"), '(2, "vibrant plum")],</span>
<span id="cb21-12"><a href="#cb21-12" aria-hidden="true" tabindex="-1"></a> 'FilledBag</span>
<span id="cb21-13"><a href="#cb21-13" aria-hidden="true" tabindex="-1"></a> "dark olive" '[ '(3, "faded blue"), '(4, "dotted black")],</span>
<span id="cb21-14"><a href="#cb21-14" aria-hidden="true" tabindex="-1"></a> 'FilledBag</span>
<span id="cb21-15"><a href="#cb21-15" aria-hidden="true" tabindex="-1"></a> "vibrant plum" '[ '(5, "faded blue"), '(6, "dotted black")],</span>
<span id="cb21-16"><a href="#cb21-16" aria-hidden="true" tabindex="-1"></a> 'EmptyBag "faded blue", 'EmptyBag "dotted black"]</span></code></pre></div>
<p>On to the final step of solving the problem: calculating the number of contained bags.</p>
<h2 data-track-content data-content-name="how-many-bags" data-content-piece="type-level-haskell-aoc7" id="how-many-bags">How Many Bags?</h2>
<p>We have the list of bags with us now. To calculate the total number of bags contained in a bag of a given color, we need to be able to lookup bags from this list by their colors. So, that’s the first thing we implement:</p>
<div class="sourceCode" id="cb22" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb22-1"><a href="#cb22-1" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span></span>
<span id="cb22-2"><a href="#cb22-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag</span> (<span class="ot">color ::</span> <span class="dt">Symbol</span>) (<span class="ot">bags ::</span> [<span class="dt">Bag</span>])<span class="ot"> ::</span> <span class="dt">Bag</span> <span class="kw">where</span></span>
<span id="cb22-3"><a href="#cb22-3" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag</span> color '[] <span class="ot">=</span> <span class="dt">TypeError</span> (<span class="dt">Text</span> <span class="st">"Unknown color: "</span> <span class="op">:<>:</span> <span class="dt">ShowType</span> color)</span>
<span id="cb22-4"><a href="#cb22-4" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag</span> color (<span class="dt">EmptyBag</span> color' <span class="op">:</span> rest) <span class="ot">=</span></span>
<span id="cb22-5"><a href="#cb22-5" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag2</span> color (<span class="dt">CmpSymbol</span> color color') (<span class="dt">EmptyBag</span> color') rest</span>
<span id="cb22-6"><a href="#cb22-6" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag</span> color (<span class="dt">FilledBag</span> color' contained <span class="op">:</span> rest) <span class="ot">=</span></span>
<span id="cb22-7"><a href="#cb22-7" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag2</span> color (<span class="dt">CmpSymbol</span> color color') (<span class="dt">FilledBag</span> color' contained) rest</span>
<span id="cb22-8"><a href="#cb22-8" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb22-9"><a href="#cb22-9" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">LookupBag2</span> (<span class="ot">color ::</span> <span class="dt">Symbol</span>)</span>
<span id="cb22-10"><a href="#cb22-10" aria-hidden="true" tabindex="-1"></a> (<span class="ot">order ::</span> <span class="dt">Ordering</span>)</span>
<span id="cb22-11"><a href="#cb22-11" aria-hidden="true" tabindex="-1"></a> (<span class="ot">bag ::</span> <span class="dt">Bag</span>)</span>
<span id="cb22-12"><a href="#cb22-12" aria-hidden="true" tabindex="-1"></a> (<span class="ot">rest ::</span> [<span class="dt">Bag</span>])<span class="ot"> ::</span> <span class="dt">Bag</span> <span class="kw">where</span></span>
<span id="cb22-13"><a href="#cb22-13" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag2</span> _ <span class="dt">EQ</span> bag _ <span class="ot">=</span> bag</span>
<span id="cb22-14"><a href="#cb22-14" aria-hidden="true" tabindex="-1"></a> <span class="dt">LookupBag2</span> color _ _ rest <span class="ot">=</span> <span class="dt">LookupBag</span> color rest</span></code></pre></div>
<p>The <code class="sourceCode haskell"><span class="dt">LookupBag</span></code> type family recursively walks through the list of <code class="sourceCode haskell"><span class="dt">Bag</span></code>s, matching each bag’s color to the given color using the <a href="https://hackage.haskell.org/package/base-4.14.1.0/docs/GHC-TypeLits.html#t:CmpSymbol" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">CmpSymbol</span></code></a> type family. Upon finding a match, it returns the matched bag. If no match is found, it returns a <code class="sourceCode haskell"><span class="dt">TypeError</span></code>. <a href="https://hackage.haskell.org/package/base-4.9.1.0/docs/GHC-TypeLits.html#t:TypeError" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">TypeError</span></code></a> is a type family much like the <a href="https://hackage.haskell.org/package/base-4.14.1.0/docs/Prelude.html#v:error" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="fu">error</span></code></a> function except it throws a compile time error instead of a runtime error.</p>
<p>Finally, we use <code class="sourceCode haskell"><span class="dt">LookupBag</span></code> to implement the <code class="sourceCode haskell"><span class="dt">BagCount</span></code> type family which does the actual calculation:</p>
<div class="sourceCode" id="cb23" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb23-1"><a href="#cb23-1" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">BagCount</span> (<span class="ot">color ::</span> <span class="dt">Symbol</span>)<span class="ot"> ::</span> <span class="dt">Nat</span> <span class="kw">where</span></span>
<span id="cb23-2"><a href="#cb23-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">BagCount</span> color <span class="ot">=</span> <span class="dt">BagCount2</span> (<span class="dt">LookupBag</span> color <span class="dt">Bags</span>)</span>
<span id="cb23-3"><a href="#cb23-3" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb23-4"><a href="#cb23-4" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">BagCount2</span> (<span class="ot">bag ::</span> <span class="dt">Bag</span>)<span class="ot"> ::</span> <span class="dt">Nat</span> <span class="kw">where</span></span>
<span id="cb23-5"><a href="#cb23-5" aria-hidden="true" tabindex="-1"></a> <span class="dt">BagCount2</span> (<span class="dt">EmptyBag</span> _) <span class="ot">=</span> <span class="dv">0</span></span>
<span id="cb23-6"><a href="#cb23-6" aria-hidden="true" tabindex="-1"></a> <span class="dt">BagCount2</span> (<span class="dt">FilledBag</span> _ bagCounts) <span class="ot">=</span> <span class="dt">BagCount3</span> bagCounts</span>
<span id="cb23-7"><a href="#cb23-7" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb23-8"><a href="#cb23-8" aria-hidden="true" tabindex="-1"></a><span class="kw">type</span> <span class="kw">family</span> <span class="dt">BagCount3</span> (<span class="ot">a ::</span> [(<span class="dt">Nat</span>, <span class="dt">Symbol</span>)])<span class="ot"> ::</span> <span class="dt">Nat</span> <span class="kw">where</span></span>
<span id="cb23-9"><a href="#cb23-9" aria-hidden="true" tabindex="-1"></a> <span class="dt">BagCount3</span> '[] <span class="ot">=</span> <span class="dv">0</span></span>
<span id="cb23-10"><a href="#cb23-10" aria-hidden="true" tabindex="-1"></a> <span class="dt">BagCount3</span> ( '(n, bag) <span class="op">:</span> as) <span class="ot">=</span></span>
<span id="cb23-11"><a href="#cb23-11" aria-hidden="true" tabindex="-1"></a> n <span class="op">+</span> n <span class="op">GHC.TypeLits.*</span> <span class="dt">BagCount2</span> (<span class="dt">LookupBag</span> bag <span class="dt">Bags</span>) <span class="op">+</span> <span class="dt">BagCount3</span> as</span></code></pre></div>
<p>We use the type-level operators <code class="sourceCode haskell"><span class="op">+</span></code> and <code class="sourceCode haskell"><span class="op">*</span></code> from the <code class="sourceCode haskell"><span class="dt">GHC.TypeLits</span></code> package to do the math on the <code class="sourceCode haskell"><span class="dt">Nat</span></code> numbers. The rest again, is just recursion and pattern matching.</p>
<p>Our work is finished. It’s time to put it all to test in GHCi:</p>
<div class="sourceCode" id="cb24" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb24-1"><a href="#cb24-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">BagCount</span> <span class="st">"shiny gold"</span></span>
<span id="cb24-2"><a href="#cb24-2" aria-hidden="true" tabindex="-1"></a>BagCount "shiny gold" :: Nat</span>
<span id="cb24-3"><a href="#cb24-3" aria-hidden="true" tabindex="-1"></a>= 32</span>
<span id="cb24-4"><a href="#cb24-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">BagCount</span> <span class="st">"light red"</span></span>
<span id="cb24-5"><a href="#cb24-5" aria-hidden="true" tabindex="-1"></a>BagCount "light red" :: Nat</span>
<span id="cb24-6"><a href="#cb24-6" aria-hidden="true" tabindex="-1"></a>= 186</span>
<span id="cb24-7"><a href="#cb24-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">BagCount</span> <span class="st">"faded blue"</span></span>
<span id="cb24-8"><a href="#cb24-8" aria-hidden="true" tabindex="-1"></a>BagCount "faded blue" :: Nat</span>
<span id="cb24-9"><a href="#cb24-9" aria-hidden="true" tabindex="-1"></a>= 0</span></code></pre></div>
<p>It works! We can also convert the type-level counts to term-level using the <a href="https://hackage.haskell.org/package/base-4.14.1.0/docs/GHC-TypeLits.html#v:natVal" target="_blank" rel="noopener"><code>natVal</code></a> function and the <a href="https://hackage.haskell.org/package/base-4.14.1.0/docs/Data-Proxy.html#t:Proxy" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">Proxy</span></code></a> type with the <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeApplications" target="_blank" rel="noopener"><code class="sourceCode haskell"><span class="dt">TypeApplications</span></code></a> extension. If we put an invalid color, we get a compilation error instead of a runtime error.</p>
<div class="sourceCode" id="cb25" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb25-1"><a href="#cb25-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeApplications</span></span>
<span id="cb25-2"><a href="#cb25-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> natVal <span class="op">$</span> <span class="dt">Proxy</span> <span class="op">@</span>(<span class="dt">BagCount</span> <span class="st">"shiny gold"</span>)</span>
<span id="cb25-3"><a href="#cb25-3" aria-hidden="true" tabindex="-1"></a>32</span>
<span id="cb25-4"><a href="#cb25-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> natVal <span class="op">$</span> <span class="dt">Proxy</span> <span class="op">@</span>(<span class="dt">BagCount</span> <span class="st">"shiny red"</span>)</span>
<span id="cb25-5"><a href="#cb25-5" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb25-6"><a href="#cb25-6" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">17</span><span class="op">:</span><span class="dv">1</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb25-7"><a href="#cb25-7" aria-hidden="true" tabindex="-1"></a> • Unknown color: "shiny red"</span>
<span id="cb25-8"><a href="#cb25-8" aria-hidden="true" tabindex="-1"></a> • In the expression: natVal $ Proxy @(BagCount "shiny red")</span>
<span id="cb25-9"><a href="#cb25-9" aria-hidden="true" tabindex="-1"></a> In an equation for ‘it’:</span>
<span id="cb25-10"><a href="#cb25-10" aria-hidden="true" tabindex="-1"></a> it = natVal $ Proxy @(BagCount "shiny red")</span></code></pre></div>
<hr></hr>
<p>This concludes our little fun experiment with type-level programming in Haskell<a href="#fn6" class="footnote-ref" id="fnref6" role="doc-noteref"><sup>6</sup></a>. Though our problem was an easy one, it demonstrated the power of TLP. I hope to see more useful applications of TLP in the Haskell ecosystem going forward.</p>
<p>You can find the complete code for this post <a href="https://abhinavsarkar.net/code/aoc7.html?mtm_campaign=feed">here</a>.</p>
<section id="footnotes" class="footnotes footnotes-end-of-document" role="doc-endnotes">
<hr></hr>
<ol>
<li id="fn1"><p>Many modern libraries are increasingly employing TLP for better type-safe APIs. Some examples:</p>
<ul>
<li><a href="http://hackage.haskell.org/package/servant" target="_blank" rel="noopener">servant</a>: Type-safe webservice APIs</li>
<li><a href="https://hackage.haskell.org/package/row-types" target="_blank" rel="noopener">row-types</a>: Type-safe open records</li>
<li><a href="https://hackage.haskell.org/package/polysemy" target="_blank" rel="noopener">polysemy</a>: Type-safe effect system</li>
<li><a href="https://hackage.haskell.org/package/type-of-html" target="_blank" rel="noopener">type-of-html</a>: Type driven HTML generation</li>
<li><a href="https://hackage.haskell.org/package/sized" target="_blank" rel="noopener">sized</a>: Type-safe sized sequence data-types</li>
<li><a href="https://hackage.haskell.org/package/dimensions" target="_blank" rel="noopener">dimensional</a>: Safe type-level dimensionality for multidimensional data</li>
</ul>
<a href="#fnref1" class="footnote-back" role="doc-backlink">↩︎</a></li>
<li id="fn2"><p>For the unfamiliar:</p>
<blockquote>
<p>Advent of Code is an Advent calendar of small programming puzzles for a variety of skill sets and skill levels that can be solved in any programming language you like. People use them as a speed contest, interview prep, company training, university coursework, practice problems, or to challenge each other.</p>
</blockquote>
<a href="#fnref2" class="footnote-back" role="doc-backlink">↩︎</a></li>
<li id="fn3"><p>Type-level strings have interesting usages like type-safe keys in <a href="https://hackage.haskell.org/package/row-types" target="_blank" rel="noopener">open records</a>.<a href="#fnref3" class="footnote-back" role="doc-backlink">↩︎</a></p></li>
<li id="fn4"><p>The type families we use in this post are technically <em>Top-level closed type families</em>. There are other ways of defining type families as described in the <a href="https://wiki.haskell.org/GHC/Type_families" target="_blank" rel="noopener">Haskell wiki</a>.<a href="#fnref4" class="footnote-back" role="doc-backlink">↩︎</a></p></li>
<li id="fn5"><p>The author of the <code>symbols</code> library <a href="https://kcsongor.github.io" target="_blank" rel="noopener">Csongor Kiss</a> has written <a href="https://web.archive.org/web/20201128084735/https://kcsongor.github.io/symbol-parsing-haskell/" target="_blank" rel="noopener">an excellent post</a> about how <code>ToList</code> is implemented.<a href="#fnref5" class="footnote-back" role="doc-backlink">↩︎</a></p></li>
<li id="fn6"><p>We solve only the example problem in this post but not the actual problem which has a much larger set of rules. This is because it’s just too slow to compile. I suspect it’s because we don’t have a built-in function to break a symbol into its constituent characters and have to resort to complicated type-level hacks for the same.<a href="#fnref6" class="footnote-back" role="doc-backlink">↩︎</a></p></li>
</ol>
</section><p>If you liked this post, please <a href="https://abhinavsarkar.net/posts/type-level-haskell-aoc7/?mtm_campaign=feed#syndications">leave a comment</a>.</p><img referrerpolicy="no-referrer-when-downgrade" src="https://anna.abhinavsarkar.net/matomo.php?idsite=1&rec=1" style="border:0" alt="" />2021-01-04T00:00:00Z<p>I have been trying to use type-level programming in Haskell to solve interesting problems since I read <a href="https://thinkingwithtypes.com/" target="_blank" rel="noopener">Thinking with Types</a> by <a href="https://reasonablypolymorphic.com/" target="_blank" rel="noopener">Sandy Maguire</a>. Then I found myself solving the problems in <a href="https://adventofcode.com/2020" target="_blank" rel="noopener">Advent of Code 2020</a> and some of them seemed suitable to be solved with type-level programming. So I decided to give it a shot.</p>
<p>https://abhinavsarkar.net/posts/twt-notes-1/Notes for ‘Thinking with Types: Type-level Programming in Haskell’, Chapters 1–52020-03-18T00:00:00ZAbhinav Sarkarhttps://abhinavsarkar.net/about/abhinav@abhinavsarkar.net<p><a href="https://www.haskell.org" target="_blank" rel="noopener">Haskell</a>—with its powerful type system—has a great support for type-level programming and it has gotten much better in the recent times with the new releases of the <a href="https://www.haskell.org/ghc/" target="_blank" rel="noopener">GHC</a> compiler. But type-level programming remains a daunting topic even with seasoned haskellers. <em><a href="https://thinkingwithtypes.com/" target="_blank" rel="noopener">Thinking with Types: Type-level Programming in Haskell</a></em> by <a href="https://sandymaguire.me/about/" target="_blank" rel="noopener">Sandy Maguire</a> is a book which attempts to fix that. I’ve taken some notes to summarize my understanding of the same.</p>
<p>This post was originally published on <a href="https://abhinavsarkar.net/posts/twt-notes-1/?mtm_campaign=feed">abhinavsarkar.net</a>.</p><!--more-->
<nav id="toc"><h3>Contents</h3><ol><li><a href="#introduction">Introduction</a></li><li><a href="#chapter-1.-the-algebra-behind-types">Chapter 1. The Algebra Behind Types</a><ol><li><a href="#isomorphisms-and-cardinalities">Isomorphisms and Cardinalities</a></li><li><a href="#sum-product-and-exponential-types">Sum, Product and Exponential Types</a></li><li><a href="#the-curry-howard-isomorphism">The Curry-Howard Isomorphism</a></li><li><a href="#canonical-representations">Canonical Representations</a></li></ol></li><li><a href="#chapter-2.-terms-types-and-kinds">Chapter 2. Terms, Types and Kinds</a><ol><li><a href="#the-kind-system">The Kind System</a></li><li><a href="#data-kinds">Data Kinds</a></li><li><a href="#promotion-of-built-in-types">Promotion of Built-In Types</a></li><li><a href="#type-level-functions">Type-level Functions</a></li></ol></li><li><a href="#chapter-3.-variance">Chapter 3. Variance</a></li><li><a href="#chapter-4.-working-with-types">Chapter 4. Working with Types</a></li><li><a href="#chapter-5.-constraints-and-gadts">Chapter 5. Constraints and GADTs</a><ol><li><a href="#constraints">Constraints</a></li><li><a href="#gadts">GADTs</a></li><li><a href="#heterogeneous-lists">Heterogeneous Lists</a></li><li><a href="#creating-new-constraints">Creating New Constraints</a></li></ol></li><li><a href="#conclusion">Conclusion</a></li></ol></nav>
<h2 data-track-content data-content-name="introduction" data-content-piece="twt-notes-1" id="introduction">Introduction</h2>
<ul>
<li>Type-level Programming (TLP) is writing programs that run at compile-time, unlike term-level programming which is writing programs that run at run-time.</li>
<li>TLP should be used in moderation.</li>
<li>TLP should be mostly used
<ul>
<li>for programs that are catastrophic to get wrong (finance, healthcare, etc).</li>
<li>when it simplifies the program API massively.</li>
<li>when power-to-weight ratio of adding TLP is high.</li>
</ul></li>
<li>Types are not a silver bullet for fixing all errors:
<ul>
<li>Correct programs can be not well-typed.</li>
<li>It can be hard to assign type for useful programs. e.g. <code>printf</code> from C.</li>
</ul></li>
<li>Types can turn possible runtime errors into compile-time errors.</li>
</ul>
<h2 data-track-content data-content-name="chapter-1.-the-algebra-behind-types" data-content-piece="twt-notes-1" id="chapter-1.-the-algebra-behind-types">Chapter 1. The Algebra Behind Types</h2>
<h3 id="isomorphisms-and-cardinalities">Isomorphisms and Cardinalities</h3>
<ul>
<li><em>Cardinality</em> of a type is the number of values it can have ignoring bottoms. The values of a type are also called the <em>inhabitants</em> of the type.</li>
</ul>
<div class="sourceCode" id="cb1" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb1-1"><a href="#cb1-1" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">Void</span></span>
<span id="cb1-2"><a href="#cb1-2" aria-hidden="true" tabindex="-1"></a> <span class="co">-- no possible values. cardinality: 0</span></span>
<span id="cb1-3"><a href="#cb1-3" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">Unit</span> <span class="ot">=</span> <span class="dt">Unit</span></span>
<span id="cb1-4"><a href="#cb1-4" aria-hidden="true" tabindex="-1"></a> <span class="co">-- only one possible value. cardinality: 1</span></span>
<span id="cb1-5"><a href="#cb1-5" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">Bool</span> <span class="ot">=</span> <span class="dt">True</span> <span class="op">|</span> <span class="dt">False</span></span>
<span id="cb1-6"><a href="#cb1-6" aria-hidden="true" tabindex="-1"></a> <span class="co">-- only two possible values. cardinality: 2</span></span></code></pre></div>
<ul>
<li>Cardinality is written using notation: <code>|Void| = 0</code></li>
<li>Two types are said to be <em>Isomorphic</em> if they have same cardinality.</li>
<li>An <em>isomorphism</em> between types <code>a</code> and <code>b</code> is a pair of functions <code>to</code> and <code>from</code> such that:</li>
</ul>
<div class="sourceCode" id="cb2" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb2-1"><a href="#cb2-1" aria-hidden="true" tabindex="-1"></a><span class="ot">to ::</span> a <span class="ot">-></span> b</span>
<span id="cb2-2"><a href="#cb2-2" aria-hidden="true" tabindex="-1"></a><span class="ot">from ::</span> b <span class="ot">-></span> a</span>
<span id="cb2-3"><a href="#cb2-3" aria-hidden="true" tabindex="-1"></a>to <span class="op">.</span> from <span class="ot">=</span> <span class="fu">id</span></span>
<span id="cb2-4"><a href="#cb2-4" aria-hidden="true" tabindex="-1"></a>from <span class="op">.</span> to <span class="ot">=</span> <span class="fu">id</span></span></code></pre></div>
<h3 id="sum-product-and-exponential-types">Sum, Product and Exponential Types</h3>
<ul>
<li><code class="sourceCode haskell"><span class="dt">Either</span> a b</code> is a <em>Sum</em> type. Its number of inhabitants is sum of the number of inhabitants of type <code>a</code> and <code>b</code> like so: <code>|a|</code> possible values with the <code class="sourceCode haskell"><span class="dt">Left</span></code> constructor and <code>|b|</code> possible values with the <code class="sourceCode haskell"><span class="dt">Right</span></code> constructor. Formally:</li>
</ul>
<pre class="plain"><code>|Either a b| = |a| + |b|</code></pre>
<ul>
<li><code>(a, b)</code> is a <em>Product</em> type. Its number of inhabitant is the product of the number of inhabitants of types <code>a</code> and <code>b</code>. Formally:</li>
</ul>
<pre class="plain"><code>|(a, b)| = |a| * |b|</code></pre>
<ul>
<li>Some more examples:</li>
</ul>
<pre class="plain"><code>|Maybe a| = |Nothing| + |Just a| = 1 + |a|
|[a]| = 1 + |a| + |a|^2 + |a|^3 + ...
|Either a Void| = |a| + 0 = |a|
|Either Void a| = 0 + |a| = |a|
|(a, Unit)| = |a| * 1 = |a|
|(Unit, a)| = 1 * |a| = |a|</code></pre>
<ul>
<li>Function types are exponentiation types.</li>
</ul>
<pre class="plain"><code>|a -> b| = |b|^|a|</code></pre>
<p>For every value in domain <code>a</code> there can be <code>|b|</code> possible values in the range <code>b</code>. And there are <code>|a|</code> possible values in domain <code>a</code>. So:</p>
<pre class="plain"><code>|a -> b|
= |b| * |b| * ... * |b| -- (|a| times)
= |b|^|a|</code></pre>
<ul>
<li>Data can be represented in many possible isomorphic types. Some of them are more useful than others. Example:</li>
</ul>
<div class="sourceCode" id="cb8" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb8-1"><a href="#cb8-1" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">TicTacToe1</span> a <span class="ot">=</span> <span class="dt">TicTacToe1</span></span>
<span id="cb8-2"><a href="#cb8-2" aria-hidden="true" tabindex="-1"></a> {<span class="ot"> topLeft ::</span> a</span>
<span id="cb8-3"><a href="#cb8-3" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> topCenter ::</span> a</span>
<span id="cb8-4"><a href="#cb8-4" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> topRight ::</span> a</span>
<span id="cb8-5"><a href="#cb8-5" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> middleLeft ::</span> a</span>
<span id="cb8-6"><a href="#cb8-6" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> middleCenter ::</span> a</span>
<span id="cb8-7"><a href="#cb8-7" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> middleRight ::</span> a</span>
<span id="cb8-8"><a href="#cb8-8" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> bottomLeft ::</span> a</span>
<span id="cb8-9"><a href="#cb8-9" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> bottomCenter ::</span> a</span>
<span id="cb8-10"><a href="#cb8-10" aria-hidden="true" tabindex="-1"></a> ,<span class="ot"> bottomRight ::</span> a</span>
<span id="cb8-11"><a href="#cb8-11" aria-hidden="true" tabindex="-1"></a> }</span>
<span id="cb8-12"><a href="#cb8-12" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb8-13"><a href="#cb8-13" aria-hidden="true" tabindex="-1"></a><span class="op">|</span><span class="dt">TicTacToe1</span> a<span class="op">|</span></span>
<span id="cb8-14"><a href="#cb8-14" aria-hidden="true" tabindex="-1"></a> <span class="ot">=</span> <span class="op">|</span>a<span class="op">|</span> <span class="op">*</span> <span class="op">|</span>a<span class="op">|</span> <span class="op">*</span> <span class="op">...</span> <span class="op">*</span> <span class="op">|</span>a<span class="op">|</span> <span class="co">-- 9 times</span></span>
<span id="cb8-15"><a href="#cb8-15" aria-hidden="true" tabindex="-1"></a> <span class="ot">=</span> <span class="op">|</span>a<span class="op">|^</span><span class="dv">9</span></span>
<span id="cb8-16"><a href="#cb8-16" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb8-17"><a href="#cb8-17" aria-hidden="true" tabindex="-1"></a><span class="ot">emptyBoard1 ::</span> <span class="dt">TicTacToe1</span> (<span class="dt">Maybe</span> <span class="dt">Bool</span>)</span>
<span id="cb8-18"><a href="#cb8-18" aria-hidden="true" tabindex="-1"></a>emptyBoard1 <span class="ot">=</span></span>
<span id="cb8-19"><a href="#cb8-19" aria-hidden="true" tabindex="-1"></a> <span class="dt">TicTacToe1</span> <span class="dt">Nothing</span> <span class="dt">Nothing</span> <span class="dt">Nothing</span></span>
<span id="cb8-20"><a href="#cb8-20" aria-hidden="true" tabindex="-1"></a> <span class="dt">Nothing</span> <span class="dt">Nothing</span> <span class="dt">Nothing</span></span>
<span id="cb8-21"><a href="#cb8-21" aria-hidden="true" tabindex="-1"></a> <span class="dt">Nothing</span> <span class="dt">Nothing</span> <span class="dt">Nothing</span></span>
<span id="cb8-22"><a href="#cb8-22" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb8-23"><a href="#cb8-23" aria-hidden="true" tabindex="-1"></a><span class="co">-- Alternatively</span></span>
<span id="cb8-24"><a href="#cb8-24" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb8-25"><a href="#cb8-25" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">Three</span> <span class="ot">=</span> <span class="dt">One</span> <span class="op">|</span> <span class="dt">Two</span> <span class="op">|</span> <span class="dt">Three</span></span>
<span id="cb8-26"><a href="#cb8-26" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">TicTacToe2</span> a <span class="ot">=</span></span>
<span id="cb8-27"><a href="#cb8-27" aria-hidden="true" tabindex="-1"></a> <span class="dt">TicTacToe2</span> (<span class="dt">Three</span> <span class="ot">-></span> <span class="dt">Three</span> <span class="ot">-></span> a)</span>
<span id="cb8-28"><a href="#cb8-28" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb8-29"><a href="#cb8-29" aria-hidden="true" tabindex="-1"></a><span class="op">|</span><span class="dt">TicTacToe2</span> a<span class="op">|</span> <span class="ot">=</span> <span class="op">|</span>a<span class="op">|^</span>(<span class="op">|</span><span class="dt">Three</span><span class="op">|</span> <span class="op">*</span> <span class="op">|</span><span class="dt">Three</span><span class="op">|</span>)</span>
<span id="cb8-30"><a href="#cb8-30" aria-hidden="true" tabindex="-1"></a> <span class="ot">=</span> <span class="op">|</span>a<span class="op">|^</span>(<span class="dv">3</span><span class="op">*</span><span class="dv">3</span>)</span>
<span id="cb8-31"><a href="#cb8-31" aria-hidden="true" tabindex="-1"></a> <span class="ot">=</span> <span class="op">|</span>a<span class="op">|^</span><span class="dv">9</span></span>
<span id="cb8-32"><a href="#cb8-32" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb8-33"><a href="#cb8-33" aria-hidden="true" tabindex="-1"></a><span class="ot">emptyBoard2 ::</span> <span class="dt">TicTacToe2</span> (<span class="dt">Maybe</span> <span class="dt">Bool</span>)</span>
<span id="cb8-34"><a href="#cb8-34" aria-hidden="true" tabindex="-1"></a>emptyBoard2 <span class="ot">=</span></span>
<span id="cb8-35"><a href="#cb8-35" aria-hidden="true" tabindex="-1"></a> <span class="dt">TicTacToe2</span> <span class="op">$</span> <span class="fu">const</span> <span class="op">$</span> <span class="fu">const</span> <span class="dt">Nothing</span></span></code></pre></div>
<h3 id="the-curry-howard-isomorphism">The Curry-Howard Isomorphism</h3>
<ul>
<li>Every logic statement can be expressed as an equivalent computer program.</li>
<li>Helps us analyze mathematical theorems through programming.</li>
</ul>
<h3 id="canonical-representations">Canonical Representations</h3>
<ul>
<li>Since multiple equivalent representations of a type are possible, the representation in form of sum of products is considered the canonical representation of the type. Example:</li>
</ul>
<div class="sourceCode" id="cb9" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb9-1"><a href="#cb9-1" aria-hidden="true" tabindex="-1"></a><span class="dt">Either</span> a (<span class="dt">Either</span> b (c, d)) <span class="co">-- canonical</span></span>
<span id="cb9-2"><a href="#cb9-2" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb9-3"><a href="#cb9-3" aria-hidden="true" tabindex="-1"></a>(a, <span class="dt">Bool</span>) <span class="co">-- not canonical</span></span>
<span id="cb9-4"><a href="#cb9-4" aria-hidden="true" tabindex="-1"></a><span class="dt">Either</span> a a</span>
<span id="cb9-5"><a href="#cb9-5" aria-hidden="true" tabindex="-1"></a><span class="co">-- same cardinality as above but canonical</span></span></code></pre></div>
<h2 data-track-content data-content-name="chapter-2.-terms-types-and-kinds" data-content-piece="twt-notes-1" id="chapter-2.-terms-types-and-kinds">Chapter 2. Terms, Types and Kinds</h2>
<h3 id="the-kind-system">The Kind System</h3>
<ul>
<li><em>Terms</em> are things manipulated at runtime. <em>Types</em> of terms are used by compiler to prove “things” about the terms.</li>
<li>Similarly, <em>Types</em> are things manipulated at compile-time. <em>Kinds</em> of types are used by the compiler to prove “things” about the types.</li>
<li>Kinds are “the types of the Types”.</li>
<li>Kind of things that can exist at runtime (terms) is <code class="sourceCode haskell"><span class="op">*</span></code>. That is, kind of <code class="sourceCode haskell"><span class="dt">Int</span></code>, <code class="sourceCode haskell"><span class="dt">String</span></code> etc is <code class="sourceCode haskell"><span class="op">*</span></code>.</li>
</ul>
<div class="sourceCode" id="cb10" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb10-1"><a href="#cb10-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">True</span></span>
<span id="cb10-2"><a href="#cb10-2" aria-hidden="true" tabindex="-1"></a>True :: Bool</span>
<span id="cb10-3"><a href="#cb10-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Bool</span></span>
<span id="cb10-4"><a href="#cb10-4" aria-hidden="true" tabindex="-1"></a>Bool :: *</span></code></pre></div>
<ul>
<li>There are kinds other than <code class="sourceCode haskell"><span class="op">*</span></code>. For example:</li>
</ul>
<div class="sourceCode" id="cb11" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb11-1"><a href="#cb11-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Show</span> <span class="dt">Int</span></span>
<span id="cb11-2"><a href="#cb11-2" aria-hidden="true" tabindex="-1"></a>Show Int :: Constraint</span></code></pre></div>
<ul>
<li>Higher-kinded types have <code class="sourceCode haskell">(<span class="ot">-></span>)</code> in their kind signature:</li>
</ul>
<div class="sourceCode" id="cb12" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb12-1"><a href="#cb12-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Maybe</span></span>
<span id="cb12-2"><a href="#cb12-2" aria-hidden="true" tabindex="-1"></a>Maybe :: * -> *</span>
<span id="cb12-3"><a href="#cb12-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Maybe</span> <span class="dt">Int</span></span>
<span id="cb12-4"><a href="#cb12-4" aria-hidden="true" tabindex="-1"></a>Maybe Int :: *</span>
<span id="cb12-5"><a href="#cb12-5" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb12-6"><a href="#cb12-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">Control.Monad.Trans.Maybe.MaybeT</span></span>
<span id="cb12-7"><a href="#cb12-7" aria-hidden="true" tabindex="-1"></a>Control.Monad.Trans.Maybe.MaybeT</span>
<span id="cb12-8"><a href="#cb12-8" aria-hidden="true" tabindex="-1"></a> :: m (Maybe a) -> Control.Monad.Trans.Maybe.MaybeT m a</span>
<span id="cb12-9"><a href="#cb12-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Control.Monad.Trans.Maybe.MaybeT</span></span>
<span id="cb12-10"><a href="#cb12-10" aria-hidden="true" tabindex="-1"></a>Control.Monad.Trans.Maybe.MaybeT :: (* -> *) -> * -> *</span>
<span id="cb12-11"><a href="#cb12-11" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Control.Monad.Trans.Maybe.MaybeT</span> <span class="dt">IO</span> <span class="dt">Int</span></span>
<span id="cb12-12"><a href="#cb12-12" aria-hidden="true" tabindex="-1"></a>Control.Monad.Trans.Maybe.MaybeT IO Int :: *</span></code></pre></div>
<h3 id="data-kinds">Data Kinds</h3>
<ul>
<li><a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-DataKinds" target="_blank" rel="noopener"><code>DataKinds</code></a> extension lets us create new kinds.</li>
<li>It lifts data constructors into type constructors and types into kinds.</li>
</ul>
<div class="sourceCode" id="cb13" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb13-1"><a href="#cb13-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XDataKinds</span></span>
<span id="cb13-2"><a href="#cb13-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">data</span> <span class="dt">Allow</span> <span class="ot">=</span> <span class="dt">Yes</span> <span class="op">|</span> <span class="dt">No</span></span>
<span id="cb13-3"><a href="#cb13-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">Yes</span> <span class="co">-- Yes is data constructor</span></span>
<span id="cb13-4"><a href="#cb13-4" aria-hidden="true" tabindex="-1"></a>Yes :: Allow</span>
<span id="cb13-5"><a href="#cb13-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">Allow</span> <span class="co">-- Allow is a type</span></span>
<span id="cb13-6"><a href="#cb13-6" aria-hidden="true" tabindex="-1"></a>Allow :: *</span>
<span id="cb13-7"><a href="#cb13-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">'Yes</span> <span class="co">-- 'Yes is a type too. Its kind is 'Allow.</span></span>
<span id="cb13-8"><a href="#cb13-8" aria-hidden="true" tabindex="-1"></a>'Yes :: Allow</span></code></pre></div>
<ul>
<li>Lifted constructors and types are written with a preceding <code>'</code> (called <em>tick</em>).</li>
</ul>
<h3 id="promotion-of-built-in-types">Promotion of Built-In Types</h3>
<ul>
<li><a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-DataKinds" target="_blank" rel="noopener"><code>DataKinds</code></a> extension promotes built-in types too.</li>
<li>Strings are promoted to the kind <code>Symbol</code>.</li>
<li>Natural numbers are promoted to the kind <code>Nat</code>.</li>
</ul>
<div class="sourceCode" id="cb14" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb14-1"><a href="#cb14-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="st">"hi"</span> <span class="co">-- "hi" is a type-level string</span></span>
<span id="cb14-2"><a href="#cb14-2" aria-hidden="true" tabindex="-1"></a>"hi" :: GHC.Types.Symbol</span>
<span id="cb14-3"><a href="#cb14-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dv">123</span> <span class="co">-- 123 is a type-level natural number</span></span>
<span id="cb14-4"><a href="#cb14-4" aria-hidden="true" tabindex="-1"></a>123 :: GHC.Types.Nat</span></code></pre></div>
<ul>
<li>We can do type level operations on <code class="sourceCode haskell"><span class="dt">Symbol</span></code>s and <code class="sourceCode haskell"><span class="dt">Nat</span></code>s.</li>
</ul>
<div class="sourceCode" id="cb15" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb15-1"><a href="#cb15-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>m <span class="op">+</span><span class="dt">GHC.TypeLits</span></span>
<span id="cb15-2"><a href="#cb15-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">AppendSymbol</span></span>
<span id="cb15-3"><a href="#cb15-3" aria-hidden="true" tabindex="-1"></a>AppendSymbol :: Symbol -> Symbol -> Symbol</span>
<span id="cb15-4"><a href="#cb15-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">AppendSymbol</span> <span class="st">"hello "</span> <span class="st">"there"</span></span>
<span id="cb15-5"><a href="#cb15-5" aria-hidden="true" tabindex="-1"></a>AppendSymbol "hello " "there" :: Symbol</span>
<span id="cb15-6"><a href="#cb15-6" aria-hidden="true" tabindex="-1"></a>= "hello there"</span>
<span id="cb15-7"><a href="#cb15-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeOperators</span></span>
<span id="cb15-8"><a href="#cb15-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> (<span class="dv">1</span> <span class="op">+</span> <span class="dv">2</span>) <span class="op">^</span> <span class="dv">7</span></span>
<span id="cb15-9"><a href="#cb15-9" aria-hidden="true" tabindex="-1"></a>(1 + 2) ^ 7 :: Nat</span>
<span id="cb15-10"><a href="#cb15-10" aria-hidden="true" tabindex="-1"></a>= 2187</span></code></pre></div>
<ul>
<li><a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeOperators" target="_blank" rel="noopener"><code>TypeOperators</code></a> extension is needed for applying type-level functions with symbolic identifiers.</li>
<li>There are type-level lists and tuples:</li>
</ul>
<div class="sourceCode" id="cb16" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb16-1"><a href="#cb16-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind '[ <span class="dt">'True</span> ]</span>
<span id="cb16-2"><a href="#cb16-2" aria-hidden="true" tabindex="-1"></a>'[ 'True ] :: [Bool]</span>
<span id="cb16-3"><a href="#cb16-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind '[<span class="dv">1</span>,<span class="dv">2</span>,<span class="dv">3</span>]</span>
<span id="cb16-4"><a href="#cb16-4" aria-hidden="true" tabindex="-1"></a>'[1,2,3] :: [Nat]</span>
<span id="cb16-5"><a href="#cb16-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind '[<span class="st">"abc"</span>]</span>
<span id="cb16-6"><a href="#cb16-6" aria-hidden="true" tabindex="-1"></a>'["abc"] :: [Symbol]</span>
<span id="cb16-7"><a href="#cb16-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">'False</span> '<span class="op">:</span> <span class="dt">'True</span> '<span class="op">:</span> '[]</span>
<span id="cb16-8"><a href="#cb16-8" aria-hidden="true" tabindex="-1"></a>'False ': 'True ': '[] :: [Bool]</span>
<span id="cb16-9"><a href="#cb16-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind '(<span class="dv">6</span>, <span class="st">"x"</span>, <span class="dt">'False</span>)</span>
<span id="cb16-10"><a href="#cb16-10" aria-hidden="true" tabindex="-1"></a>'(6, "x", 'False) :: (Nat, Symbol, Bool)</span></code></pre></div>
<h3 id="type-level-functions">Type-level Functions</h3>
<ul>
<li>With the <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeFamilies" target="_blank" rel="noopener"><code>TypeFamilies</code></a> extension, it’s possible to write new type-level functions as closed type families:</li>
</ul>
<div class="sourceCode" id="cb17" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb17-1"><a href="#cb17-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XDataKinds</span></span>
<span id="cb17-2"><a href="#cb17-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeFamilies</span></span>
<span id="cb17-3"><a href="#cb17-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb17-4"><a href="#cb17-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">type</span> <span class="kw">family</span> <span class="dt">And</span> (<span class="ot">x ::</span> <span class="dt">Bool</span>) (<span class="ot">y ::</span> <span class="dt">Bool</span>)<span class="ot"> ::</span> <span class="dt">Bool</span> <span class="kw">where</span></span>
<span id="cb17-5"><a href="#cb17-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">And</span> <span class="dt">'True</span> <span class="dt">'True</span> <span class="ot">=</span> <span class="dt">'True</span></span>
<span id="cb17-6"><a href="#cb17-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">And</span> _ _ <span class="ot">=</span> <span class="dt">'False</span></span>
<span id="cb17-7"><a href="#cb17-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb17-8"><a href="#cb17-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind <span class="dt">And</span></span>
<span id="cb17-9"><a href="#cb17-9" aria-hidden="true" tabindex="-1"></a>And :: Bool -> Bool -> Bool</span>
<span id="cb17-10"><a href="#cb17-10" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">And</span> <span class="dt">'True</span> <span class="dt">'False</span></span>
<span id="cb17-11"><a href="#cb17-11" aria-hidden="true" tabindex="-1"></a>And 'True 'False :: Bool</span>
<span id="cb17-12"><a href="#cb17-12" aria-hidden="true" tabindex="-1"></a>= 'False</span>
<span id="cb17-13"><a href="#cb17-13" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">And</span> <span class="dt">'True</span> <span class="dt">'True</span></span>
<span id="cb17-14"><a href="#cb17-14" aria-hidden="true" tabindex="-1"></a>And 'True 'True :: Bool</span>
<span id="cb17-15"><a href="#cb17-15" aria-hidden="true" tabindex="-1"></a>= 'True</span>
<span id="cb17-16"><a href="#cb17-16" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">And</span> <span class="dt">'False</span> <span class="dt">'True</span></span>
<span id="cb17-17"><a href="#cb17-17" aria-hidden="true" tabindex="-1"></a>And 'False 'True :: Bool</span>
<span id="cb17-18"><a href="#cb17-18" aria-hidden="true" tabindex="-1"></a>= 'False</span></code></pre></div>
<div class="page-break">
</div>
<h2 data-track-content data-content-name="chapter-3.-variance" data-content-piece="twt-notes-1" id="chapter-3.-variance">Chapter 3. Variance</h2>
<ul>
<li>There are three types of <em>Variance</em> (<code class="sourceCode haskell"><span class="dt">T</span></code> here a type of kind <code>* -> *</code>):
<ul>
<li>Covariant: any function of type <code class="sourceCode haskell">a <span class="ot">-></span> b</code> can be lifted into a function of type <code class="sourceCode haskell"><span class="dt">T</span> a <span class="ot">-></span> <span class="dt">T</span> b</code>. Covariant types are instances of the <a href="https://hackage.haskell.org/package/base/docs/Prelude.html#t:Functor" target="_blank" rel="noopener"><code>Functor</code></a> typeclass:</li>
</ul>
<div class="sourceCode" id="cb18" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb18-1"><a href="#cb18-1" aria-hidden="true" tabindex="-1"></a><span class="kw">class</span> <span class="dt">Functor</span> f <span class="kw">where</span></span>
<span id="cb18-2"><a href="#cb18-2" aria-hidden="true" tabindex="-1"></a><span class="ot"> fmap ::</span> (a <span class="ot">-></span> b) <span class="ot">-></span> f a <span class="ot">-></span> f b</span></code></pre></div>
<ul>
<li>Contravariant: any function of type <code class="sourceCode haskell">a <span class="ot">-></span> b</code> can be lifted into a function of type <code class="sourceCode haskell"><span class="dt">T</span> b <span class="ot">-></span> <span class="dt">T</span> a</code>. Contravariant functions are instances of the <a href="https://hackage.haskell.org/package/base/docs/Data-Functor-Contravariant.html" target="_blank" rel="noopener"><code>Contravariant</code></a> typeclass:</li>
</ul>
<div class="sourceCode" id="cb19" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb19-1"><a href="#cb19-1" aria-hidden="true" tabindex="-1"></a><span class="kw">class</span> <span class="dt">Contravariant</span> f <span class="kw">where</span></span>
<span id="cb19-2"><a href="#cb19-2" aria-hidden="true" tabindex="-1"></a><span class="ot"> contramap ::</span> (a <span class="ot">-></span> b) <span class="ot">-></span> f b <span class="ot">-></span> f a</span></code></pre></div>
<ul>
<li>Invariant: no function of type <code class="sourceCode haskell">a <span class="ot">-></span> b</code> can be lifted into a function of type <code class="sourceCode haskell"><span class="dt">T</span> a</code>. Invariant functions are instances of the <a href="https://hackage.haskell.org/package/invariant/docs/Data-Functor-Invariant.html#t:Invariant" target="_blank" rel="noopener"><code>Invariant</code></a> typeclass:</li>
</ul>
<div class="sourceCode" id="cb20" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb20-1"><a href="#cb20-1" aria-hidden="true" tabindex="-1"></a><span class="kw">class</span> <span class="dt">Invariant</span> f <span class="kw">where</span></span>
<span id="cb20-2"><a href="#cb20-2" aria-hidden="true" tabindex="-1"></a><span class="ot"> invmap ::</span> (a <span class="ot">-></span> b) <span class="ot">-></span> (b <span class="ot">-></span> a) <span class="ot">-></span> f a <span class="ot">-></span> f b</span></code></pre></div></li>
<li>Variance of a type <code class="sourceCode haskell"><span class="dt">T</span></code> is specified with respect to a particular type parameter. A type <code class="sourceCode haskell"><span class="dt">T</span></code> with two parameters <code>a</code> and <code>b</code> could be covariant wrt. <code>a</code> and contravariant wrt. <code>b</code>.</li>
<li>Variance of a type <code class="sourceCode haskell"><span class="dt">T</span></code> wrt. a particular type parameter is determined by whether the parameter appears in positive or negative <em>position</em>s.
<ul>
<li>If a type parameter appears on the left-hand side of a function, it is said to be in a negative position. Else it is said to be in a positive position.</li>
<li>If a type parameter appears only in positive positions then the type is covariant wrt. that parameter.</li>
<li>If a type parameter appears only in negative positions then the type is contravariant wrt. that parameter.</li>
<li>If a type parameter appears in both positive and negative positions then the type is invariant wrt. that parameter.</li>
<li>positions follow the laws of multiplication for their <em>signs</em>.</li>
</ul></li>
</ul>
<div class="scrollable-table">
<table>
<thead>
<tr class="header">
<th style="text-align: left;">a</th>
<th style="text-align: left;">b</th>
<th style="text-align: left;">a * b</th>
</tr>
</thead>
<tbody>
<tr class="odd">
<td style="text-align: left;">+</td>
<td style="text-align: left;">+</td>
<td style="text-align: left;">+</td>
</tr>
<tr class="even">
<td style="text-align: left;">+</td>
<td style="text-align: left;">-</td>
<td style="text-align: left;">-</td>
</tr>
<tr class="odd">
<td style="text-align: left;">-</td>
<td style="text-align: left;">+</td>
<td style="text-align: left;">-</td>
</tr>
<tr class="even">
<td style="text-align: left;">-</td>
<td style="text-align: left;">-</td>
<td style="text-align: left;">+</td>
</tr>
</tbody>
</table>
</div>
<ul>
<li>Examples:</li>
</ul>
<div class="sourceCode" id="cb21" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb21-1"><a href="#cb21-1" aria-hidden="true" tabindex="-1"></a><span class="kw">newtype</span> <span class="dt">T1</span> a <span class="ot">=</span> <span class="dt">T1</span> (<span class="dt">Int</span> <span class="ot">-></span> a)</span>
<span id="cb21-2"><a href="#cb21-2" aria-hidden="true" tabindex="-1"></a><span class="co">-- a is in +ve position, T1 is covariant wrt. a.</span></span>
<span id="cb21-3"><a href="#cb21-3" aria-hidden="true" tabindex="-1"></a><span class="kw">newtype</span> <span class="dt">T2</span> a <span class="ot">=</span> <span class="dt">T2</span> (a <span class="ot">-></span> <span class="dt">Int</span>)</span>
<span id="cb21-4"><a href="#cb21-4" aria-hidden="true" tabindex="-1"></a><span class="co">-- a is in -ve position, T2 is contravariant wrt. a.</span></span>
<span id="cb21-5"><a href="#cb21-5" aria-hidden="true" tabindex="-1"></a><span class="kw">newtype</span> <span class="dt">T3</span> a <span class="ot">=</span> <span class="dt">T3</span> (a <span class="ot">-></span> a)</span>
<span id="cb21-6"><a href="#cb21-6" aria-hidden="true" tabindex="-1"></a><span class="co">-- a is in both -ve and +ve position. T3 is invariant wrt. a.</span></span>
<span id="cb21-7"><a href="#cb21-7" aria-hidden="true" tabindex="-1"></a><span class="kw">newtype</span> <span class="dt">T4</span> a <span class="ot">=</span> <span class="dt">T4</span> ((<span class="dt">Int</span> <span class="ot">-></span> a) <span class="ot">-></span> <span class="dt">Int</span>)</span>
<span id="cb21-8"><a href="#cb21-8" aria-hidden="true" tabindex="-1"></a><span class="co">-- a is in +ve position but (Int -> a) is in -ve position.</span></span>
<span id="cb21-9"><a href="#cb21-9" aria-hidden="true" tabindex="-1"></a><span class="co">-- So a is in -ve position overall. T4 is contravariant wrt. a.</span></span>
<span id="cb21-10"><a href="#cb21-10" aria-hidden="true" tabindex="-1"></a><span class="kw">newtype</span> <span class="dt">T5</span> a <span class="ot">=</span> <span class="dt">T5</span> ((a <span class="ot">-></span> <span class="dt">Int</span>) <span class="ot">-></span> <span class="dt">Int</span>)</span>
<span id="cb21-11"><a href="#cb21-11" aria-hidden="true" tabindex="-1"></a><span class="co">-- a is in -ve position but (a -> Int) is in -ve position.</span></span>
<span id="cb21-12"><a href="#cb21-12" aria-hidden="true" tabindex="-1"></a><span class="co">-- So a is in +ve position overall. T5 is covariant wrt. a.</span></span></code></pre></div>
<ul>
<li>Covariant parameters are said to be <em>produced</em> or <em>owned</em> by the type.</li>
<li>Contravariant parameters are said to be <em>consumed</em> by the type.</li>
<li>A type that has two parameters and is covariant in both of them is an instance of <a href="https://hackage.haskell.org/package/base/docs/Data-Bifunctor.html#t:Bifunctor" target="_blank" rel="noopener"><code>BiFunctor</code></a>.</li>
<li>A type that has two parameters and is contravariant in first parameter and covariant in second parameter is an instance of <a href="https://hackage.haskell.org/package/profunctors/docs/Data-Profunctor.html#t:Profunctor" target="_blank" rel="noopener"><code>Profunctor</code></a>.</li>
</ul>
<h2 data-track-content data-content-name="chapter-4.-working-with-types" data-content-piece="twt-notes-1" id="chapter-4.-working-with-types">Chapter 4. Working with Types</h2>
<ul>
<li>Standard Haskell has no notion of scopes for types.</li>
<li><a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-ScopedTypeVariables" target="_blank" rel="noopener"><code>ScopedTypeVariables</code></a> extension lets us bind type variables to a scope. It requires an explicitly <code>forall</code> quantifier in type signatures.</li>
</ul>
<div class="sourceCode" id="cb22" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb22-1"><a href="#cb22-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="co">-- This does not compile.</span></span>
<span id="cb22-2"><a href="#cb22-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb22-3"><a href="#cb22-3" aria-hidden="true" tabindex="-1"></a><span class="ot">> comp ::</span> (a <span class="ot">-></span> b) <span class="ot">-></span> (b <span class="ot">-></span> c) <span class="ot">-></span> a <span class="ot">-></span> c</span>
<span id="cb22-4"><a href="#cb22-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> comp f g a <span class="ot">=</span> go f</span>
<span id="cb22-5"><a href="#cb22-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">where</span></span>
<span id="cb22-6"><a href="#cb22-6" aria-hidden="true" tabindex="-1"></a><span class="ot">> go ::</span> (a <span class="ot">-></span> b) <span class="ot">-></span> c</span>
<span id="cb22-7"><a href="#cb22-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> go f' <span class="ot">=</span> g (f' a)</span>
<span id="cb22-8"><a href="#cb22-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb22-9"><a href="#cb22-9" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb22-10"><a href="#cb22-10" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">11</span><span class="op">:</span><span class="dv">11</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb22-11"><a href="#cb22-11" aria-hidden="true" tabindex="-1"></a> • Couldn't match expected type ‘c1’ with actual type ‘c’</span>
<span id="cb22-12"><a href="#cb22-12" aria-hidden="true" tabindex="-1"></a> ‘c1’ is a rigid type variable bound by</span>
<span id="cb22-13"><a href="#cb22-13" aria-hidden="true" tabindex="-1"></a> the type signature for:</span>
<span id="cb22-14"><a href="#cb22-14" aria-hidden="true" tabindex="-1"></a> go :: forall a1 b1 c1. (a1 -> b1) -> c1</span>
<span id="cb22-15"><a href="#cb22-15" aria-hidden="true" tabindex="-1"></a> at <interactive>:10:3-21</span>
<span id="cb22-16"><a href="#cb22-16" aria-hidden="true" tabindex="-1"></a> ‘c’ is a rigid type variable bound by</span>
<span id="cb22-17"><a href="#cb22-17" aria-hidden="true" tabindex="-1"></a> the type signature for:</span>
<span id="cb22-18"><a href="#cb22-18" aria-hidden="true" tabindex="-1"></a> comp :: forall a b c. (a -> b) -> (b -> c) -> a -> c</span>
<span id="cb22-19"><a href="#cb22-19" aria-hidden="true" tabindex="-1"></a> at <interactive>:7:1-38</span>
<span id="cb22-20"><a href="#cb22-20" aria-hidden="true" tabindex="-1"></a> • In the expression: g (f' a)</span>
<span id="cb22-21"><a href="#cb22-21" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb22-22"><a href="#cb22-22" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">11</span><span class="op">:</span><span class="dv">14</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb22-23"><a href="#cb22-23" aria-hidden="true" tabindex="-1"></a> • Couldn't match expected type ‘b’ with actual type ‘b1’</span>
<span id="cb22-24"><a href="#cb22-24" aria-hidden="true" tabindex="-1"></a> ‘b1’ is a rigid type variable bound by</span>
<span id="cb22-25"><a href="#cb22-25" aria-hidden="true" tabindex="-1"></a> the type signature for:</span>
<span id="cb22-26"><a href="#cb22-26" aria-hidden="true" tabindex="-1"></a> go :: forall a1 b1 c1. (a1 -> b1) -> c1</span>
<span id="cb22-27"><a href="#cb22-27" aria-hidden="true" tabindex="-1"></a> at <interactive>:10:3-21</span>
<span id="cb22-28"><a href="#cb22-28" aria-hidden="true" tabindex="-1"></a> ‘b’ is a rigid type variable bound by</span>
<span id="cb22-29"><a href="#cb22-29" aria-hidden="true" tabindex="-1"></a> the type signature for:</span>
<span id="cb22-30"><a href="#cb22-30" aria-hidden="true" tabindex="-1"></a> comp :: forall a b c. (a -> b) -> (b -> c) -> a -> c</span>
<span id="cb22-31"><a href="#cb22-31" aria-hidden="true" tabindex="-1"></a> at <interactive>:7:1-38</span>
<span id="cb22-32"><a href="#cb22-32" aria-hidden="true" tabindex="-1"></a> • In the first argument of ‘g’, namely ‘(f' a)’</span>
<span id="cb22-33"><a href="#cb22-33" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb22-34"><a href="#cb22-34" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">11</span><span class="op">:</span><span class="dv">17</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb22-35"><a href="#cb22-35" aria-hidden="true" tabindex="-1"></a> • Couldn't match expected type ‘a1’ with actual type ‘a’</span>
<span id="cb22-36"><a href="#cb22-36" aria-hidden="true" tabindex="-1"></a> ‘a1’ is a rigid type variable bound by</span>
<span id="cb22-37"><a href="#cb22-37" aria-hidden="true" tabindex="-1"></a> the type signature for:</span>
<span id="cb22-38"><a href="#cb22-38" aria-hidden="true" tabindex="-1"></a> go :: forall a1 b1 c1. (a1 -> b1) -> c1</span>
<span id="cb22-39"><a href="#cb22-39" aria-hidden="true" tabindex="-1"></a> at <interactive>:10:3-21</span>
<span id="cb22-40"><a href="#cb22-40" aria-hidden="true" tabindex="-1"></a> ‘a’ is a rigid type variable bound by</span>
<span id="cb22-41"><a href="#cb22-41" aria-hidden="true" tabindex="-1"></a> the type signature for:</span>
<span id="cb22-42"><a href="#cb22-42" aria-hidden="true" tabindex="-1"></a> comp :: forall a b c. (a -> b) -> (b -> c) -> a -> c</span>
<span id="cb22-43"><a href="#cb22-43" aria-hidden="true" tabindex="-1"></a> at <interactive>:7:1-38</span>
<span id="cb22-44"><a href="#cb22-44" aria-hidden="true" tabindex="-1"></a> • In the first argument of ‘f'’, namely ‘a’</span>
<span id="cb22-45"><a href="#cb22-45" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb22-46"><a href="#cb22-46" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="co">-- But this does.</span></span>
<span id="cb22-47"><a href="#cb22-47" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XScopedTypeVariables</span></span>
<span id="cb22-48"><a href="#cb22-48" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb22-49"><a href="#cb22-49" aria-hidden="true" tabindex="-1"></a><span class="ot">> comp ::</span> <span class="kw">forall</span> a b c<span class="op">.</span> (a <span class="ot">-></span> b) <span class="ot">-></span> (b <span class="ot">-></span> c) <span class="ot">-></span> a <span class="ot">-></span> c</span>
<span id="cb22-50"><a href="#cb22-50" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> comp f g a <span class="ot">=</span> go f</span>
<span id="cb22-51"><a href="#cb22-51" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">where</span></span>
<span id="cb22-52"><a href="#cb22-52" aria-hidden="true" tabindex="-1"></a><span class="ot">> go ::</span> (a <span class="ot">-></span> b) <span class="ot">-></span> c</span>
<span id="cb22-53"><a href="#cb22-53" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> go f' <span class="ot">=</span> g (f' a)</span>
<span id="cb22-54"><a href="#cb22-54" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span></code></pre></div>
<ul>
<li><a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-TypeApplications" target="_blank" rel="noopener"><code>TypeApplications</code></a> extension lets us directly apply types to expressions:</li>
</ul>
<div class="sourceCode" id="cb23" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb23-1"><a href="#cb23-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeApplications</span></span>
<span id="cb23-2"><a href="#cb23-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="fu">traverse</span></span>
<span id="cb23-3"><a href="#cb23-3" aria-hidden="true" tabindex="-1"></a>traverse</span>
<span id="cb23-4"><a href="#cb23-4" aria-hidden="true" tabindex="-1"></a> :: (Traversable t, Applicative f) =></span>
<span id="cb23-5"><a href="#cb23-5" aria-hidden="true" tabindex="-1"></a> (a -> f b) -> t a -> f (t b)</span>
<span id="cb23-6"><a href="#cb23-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="fu">traverse</span> <span class="op">@</span><span class="dt">Maybe</span></span>
<span id="cb23-7"><a href="#cb23-7" aria-hidden="true" tabindex="-1"></a>traverse @Maybe</span>
<span id="cb23-8"><a href="#cb23-8" aria-hidden="true" tabindex="-1"></a> :: Applicative f =></span>
<span id="cb23-9"><a href="#cb23-9" aria-hidden="true" tabindex="-1"></a> (a -> f b) -> Maybe a -> f (Maybe b)</span>
<span id="cb23-10"><a href="#cb23-10" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="fu">traverse</span> <span class="op">@</span><span class="dt">Maybe</span> <span class="op">@</span>[]</span>
<span id="cb23-11"><a href="#cb23-11" aria-hidden="true" tabindex="-1"></a>traverse @Maybe @[]</span>
<span id="cb23-12"><a href="#cb23-12" aria-hidden="true" tabindex="-1"></a> :: (a -> [b]) -> Maybe a -> [Maybe b]</span>
<span id="cb23-13"><a href="#cb23-13" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="fu">traverse</span> <span class="op">@</span><span class="dt">Maybe</span> <span class="op">@</span>[] <span class="op">@</span><span class="dt">Int</span></span>
<span id="cb23-14"><a href="#cb23-14" aria-hidden="true" tabindex="-1"></a>traverse @Maybe @[] @Int</span>
<span id="cb23-15"><a href="#cb23-15" aria-hidden="true" tabindex="-1"></a> :: (Int -> [b]) -> Maybe Int -> [Maybe b]</span>
<span id="cb23-16"><a href="#cb23-16" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="fu">traverse</span> <span class="op">@</span><span class="dt">Maybe</span> <span class="op">@</span>[] <span class="op">@</span><span class="dt">Int</span> <span class="op">@</span><span class="dt">String</span></span>
<span id="cb23-17"><a href="#cb23-17" aria-hidden="true" tabindex="-1"></a>traverse @Maybe @[] @Int @String</span>
<span id="cb23-18"><a href="#cb23-18" aria-hidden="true" tabindex="-1"></a> :: (Int -> [String]) -> Maybe Int -> [Maybe String]</span></code></pre></div>
<ul>
<li>Types are applied in the order they appear in the type signature. It is possible to avoid applying types by using a type with an underscore: <code>@_</code></li>
</ul>
<div class="sourceCode" id="cb24" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb24-1"><a href="#cb24-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="fu">traverse</span> <span class="op">@</span><span class="dt">Maybe</span> <span class="op">@</span>_ <span class="op">@</span>_ <span class="op">@</span><span class="dt">String</span></span>
<span id="cb24-2"><a href="#cb24-2" aria-hidden="true" tabindex="-1"></a>traverse @Maybe @_ @_ @String</span>
<span id="cb24-3"><a href="#cb24-3" aria-hidden="true" tabindex="-1"></a> :: Applicative w1 =></span>
<span id="cb24-4"><a href="#cb24-4" aria-hidden="true" tabindex="-1"></a> (w2 -> w1 String) -> Maybe w2 -> w1 (Maybe String)</span></code></pre></div>
<ul>
<li>Sometimes the compiler cannot infer the type of an expression. <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-AllowAmbiguousTypes" target="_blank" rel="noopener"><code>AllowAmbiguousTypes</code></a> extension allow such programs to compile.</li>
</ul>
<div class="sourceCode" id="cb25" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb25-1"><a href="#cb25-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XScopedTypeVariables</span></span>
<span id="cb25-2"><a href="#cb25-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb25-3"><a href="#cb25-3" aria-hidden="true" tabindex="-1"></a><span class="ot">> f ::</span> <span class="kw">forall</span> a<span class="op">.</span> <span class="dt">Show</span> a <span class="ot">=></span> <span class="dt">Bool</span></span>
<span id="cb25-4"><a href="#cb25-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> f <span class="ot">=</span> <span class="dt">True</span></span>
<span id="cb25-5"><a href="#cb25-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb25-6"><a href="#cb25-6" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb25-7"><a href="#cb25-7" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">7</span><span class="op">:</span><span class="dv">6</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb25-8"><a href="#cb25-8" aria-hidden="true" tabindex="-1"></a> • Could not deduce (Show a0)</span>
<span id="cb25-9"><a href="#cb25-9" aria-hidden="true" tabindex="-1"></a> from the context: Show a</span>
<span id="cb25-10"><a href="#cb25-10" aria-hidden="true" tabindex="-1"></a> bound by the type signature for:</span>
<span id="cb25-11"><a href="#cb25-11" aria-hidden="true" tabindex="-1"></a> f :: forall a. Show a => Bool</span>
<span id="cb25-12"><a href="#cb25-12" aria-hidden="true" tabindex="-1"></a> at <interactive>:7:6-29</span>
<span id="cb25-13"><a href="#cb25-13" aria-hidden="true" tabindex="-1"></a> The type variable ‘a0’ is ambiguous</span>
<span id="cb25-14"><a href="#cb25-14" aria-hidden="true" tabindex="-1"></a> • In the ambiguity check for ‘f’</span>
<span id="cb25-15"><a href="#cb25-15" aria-hidden="true" tabindex="-1"></a> To defer the ambiguity check to use sites, enable AllowAmbiguousTypes</span>
<span id="cb25-16"><a href="#cb25-16" aria-hidden="true" tabindex="-1"></a> In the type signature: f :: forall a. Show a => Bool</span></code></pre></div>
<ul>
<li><code class="sourceCode haskell"><span class="dt">Proxy</span></code> is a type isomorphic to <code>()</code> except with a phantom type parameter:</li>
</ul>
<div class="sourceCode" id="cb26" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb26-1"><a href="#cb26-1" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">Proxy</span> a <span class="ot">=</span> <span class="dt">Proxy</span></span></code></pre></div>
<ul>
<li>With all the three extensions enabled, it is possible to get a term-level representation of types using the <a href="https://hackage.haskell.org/package/base/docs/Data-Typeable.html" target="_blank" rel="noopener"><code>Data.Typeable</code></a> module:</li>
</ul>
<div class="sourceCode" id="cb27" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb27-1"><a href="#cb27-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XScopedTypeVariables</span></span>
<span id="cb27-2"><a href="#cb27-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeApplications</span></span>
<span id="cb27-3"><a href="#cb27-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XAllowAmbiguousTypes</span></span>
<span id="cb27-4"><a href="#cb27-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>m <span class="op">+</span><span class="dt">Data.Typeable</span></span>
<span id="cb27-5"><a href="#cb27-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb27-6"><a href="#cb27-6" aria-hidden="true" tabindex="-1"></a><span class="ot">> typeName ::</span> <span class="kw">forall</span> a<span class="op">.</span> <span class="dt">Typeable</span> a <span class="ot">=></span> <span class="dt">String</span></span>
<span id="cb27-7"><a href="#cb27-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> typeName <span class="ot">=</span> <span class="fu">show</span> <span class="op">.</span> typeRep <span class="op">$</span> <span class="dt">Proxy</span> <span class="op">@</span>a</span>
<span id="cb27-8"><a href="#cb27-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb27-9"><a href="#cb27-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> typeName <span class="op">@</span><span class="dt">String</span></span>
<span id="cb27-10"><a href="#cb27-10" aria-hidden="true" tabindex="-1"></a>"[Char]"</span>
<span id="cb27-11"><a href="#cb27-11" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> typeName <span class="op">@</span>(<span class="dt">IO</span> <span class="dt">Int</span>)</span>
<span id="cb27-12"><a href="#cb27-12" aria-hidden="true" tabindex="-1"></a>"IO Int"</span></code></pre></div>
<h2 data-track-content data-content-name="chapter-5.-constraints-and-gadts" data-content-piece="twt-notes-1" id="chapter-5.-constraints-and-gadts">Chapter 5. Constraints and GADTs</h2>
<h3 id="constraints">Constraints</h3>
<ul>
<li><em>Constraints</em> are a kind different than the types (<code class="sourceCode haskell"><span class="op">*</span></code>).</li>
<li>Constraints are what appear on the left-hand side on the fat context arrow <code class="sourceCode haskell"><span class="ot">=></span></code>, like <code class="sourceCode haskell"><span class="dt">Show</span> a</code>.</li>
</ul>
<div class="sourceCode" id="cb28" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb28-1"><a href="#cb28-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>k <span class="dt">Show</span></span>
<span id="cb28-2"><a href="#cb28-2" aria-hidden="true" tabindex="-1"></a>Show :: * -> Constraint</span>
<span id="cb28-3"><a href="#cb28-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>k <span class="dt">Show</span> <span class="dt">Int</span></span>
<span id="cb28-4"><a href="#cb28-4" aria-hidden="true" tabindex="-1"></a>Show Int :: Constraint</span>
<span id="cb28-5"><a href="#cb28-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>k (<span class="dt">Show</span> <span class="dt">Int</span>, <span class="dt">Eq</span> <span class="dt">String</span>)</span>
<span id="cb28-6"><a href="#cb28-6" aria-hidden="true" tabindex="-1"></a>(Show Int, Eq String) :: Constraint</span></code></pre></div>
<ul>
<li>Type equalities <code class="sourceCode haskell">(<span class="dt">Int</span> <span class="op">~</span> a)</code> are another way of creating Constraints. <code class="sourceCode haskell">(<span class="dt">Int</span> <span class="op">~</span> a)</code> says <code>a</code> is same as <code class="sourceCode haskell"><span class="dt">Int</span></code>.</li>
<li>Type equalities are
<ul>
<li>reflexive: <code>a ~ a</code> always</li>
<li>symmetrical: <code>a ~ b</code> implies <code>b ~ a</code></li>
<li>transitive: <code>a ~ b</code> and <code>b ~ c</code> implies <code>a ~ c</code></li>
</ul></li>
</ul>
<h3 id="gadts">GADTs</h3>
<ul>
<li><em>GADTs</em> are Generalized Algebraic DataTypes. They allow writing explicit type signatures for data constructors. Here is the code for a length-typed list using GADTs:</li>
</ul>
<div class="sourceCode" id="cb29" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb29-1"><a href="#cb29-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XGADTs</span></span>
<span id="cb29-2"><a href="#cb29-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XKindSignatures</span></span>
<span id="cb29-3"><a href="#cb29-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeOperators</span></span>
<span id="cb29-4"><a href="#cb29-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XDataKinds</span></span>
<span id="cb29-5"><a href="#cb29-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>m <span class="op">+</span><span class="dt">GHC.TypeLits</span></span>
<span id="cb29-6"><a href="#cb29-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb29-7"><a href="#cb29-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">data</span> <span class="dt">List</span> (<span class="ot">a ::</span> <span class="op">*</span>) (<span class="ot">n ::</span> <span class="dt">Nat</span>) <span class="kw">where</span></span>
<span id="cb29-8"><a href="#cb29-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">Nil</span><span class="ot"> ::</span> <span class="dt">List</span> a <span class="dv">0</span></span>
<span id="cb29-9"><a href="#cb29-9" aria-hidden="true" tabindex="-1"></a><span class="ot">> (:~) ::</span> a <span class="ot">-></span> <span class="dt">List</span> a n <span class="ot">-></span> <span class="dt">List</span> a (n <span class="op">+</span> <span class="dv">1</span>)</span>
<span id="cb29-10"><a href="#cb29-10" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">infixr</span> <span class="dv">5</span> <span class="op">:~</span></span>
<span id="cb29-11"><a href="#cb29-11" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb29-12"><a href="#cb29-12" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">Nil</span></span>
<span id="cb29-13"><a href="#cb29-13" aria-hidden="true" tabindex="-1"></a>Nil :: List a 0</span>
<span id="cb29-14"><a href="#cb29-14" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="ch">'a'</span> <span class="op">:~</span> <span class="dt">Nil</span></span>
<span id="cb29-15"><a href="#cb29-15" aria-hidden="true" tabindex="-1"></a>'a' :~ Nil :: List Char 1</span>
<span id="cb29-16"><a href="#cb29-16" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="ch">'b'</span> <span class="op">:~</span> <span class="ch">'a'</span> <span class="op">:~</span> <span class="dt">Nil</span></span>
<span id="cb29-17"><a href="#cb29-17" aria-hidden="true" tabindex="-1"></a>'b' :~ 'a' :~ Nil :: List Char 2</span>
<span id="cb29-18"><a href="#cb29-18" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">True</span> <span class="op">:~</span> <span class="ch">'a'</span> <span class="op">:~</span> <span class="dt">Nil</span></span>
<span id="cb29-19"><a href="#cb29-19" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb29-20"><a href="#cb29-20" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">1</span><span class="op">:</span><span class="dv">9</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb29-21"><a href="#cb29-21" aria-hidden="true" tabindex="-1"></a> • Couldn't match type ‘Char’ with ‘Bool’</span>
<span id="cb29-22"><a href="#cb29-22" aria-hidden="true" tabindex="-1"></a> Expected type: List Bool 1</span>
<span id="cb29-23"><a href="#cb29-23" aria-hidden="true" tabindex="-1"></a> Actual type: List Char (0 + 1)</span>
<span id="cb29-24"><a href="#cb29-24" aria-hidden="true" tabindex="-1"></a> • In the second argument of ‘(:~)’, namely ‘'a' :~ Nil’</span>
<span id="cb29-25"><a href="#cb29-25" aria-hidden="true" tabindex="-1"></a> In the expression: True :~ 'a' :~ Nil</span></code></pre></div>
<ul>
<li>GADTs are just syntactic sugar for ADTs with type equalities. The above definition is equivalent to:</li>
</ul>
<div class="sourceCode" id="cb30" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb30-1"><a href="#cb30-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XGADTs</span></span>
<span id="cb30-2"><a href="#cb30-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XKindSignatures</span></span>
<span id="cb30-3"><a href="#cb30-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeOperators</span></span>
<span id="cb30-4"><a href="#cb30-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XDataKinds</span></span>
<span id="cb30-5"><a href="#cb30-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>m <span class="op">+</span><span class="dt">GHC.TypeLits</span></span>
<span id="cb30-6"><a href="#cb30-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb30-7"><a href="#cb30-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">data</span> <span class="dt">List</span> (<span class="ot">a ::</span> <span class="op">*</span>) (<span class="ot">n ::</span> <span class="dt">Nat</span>)</span>
<span id="cb30-8"><a href="#cb30-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="ot">=</span> (n <span class="op">~</span> <span class="dv">0</span>) <span class="ot">=></span> <span class="dt">Nil</span></span>
<span id="cb30-9"><a href="#cb30-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">|</span> a <span class="op">:~</span> <span class="dt">List</span> a (n <span class="op">-</span> <span class="dv">1</span>)</span>
<span id="cb30-10"><a href="#cb30-10" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">infixr</span> <span class="dv">5</span> <span class="op">:~</span></span>
<span id="cb30-11"><a href="#cb30-11" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb30-12"><a href="#cb30-12" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="ch">'a'</span> <span class="op">:~</span> <span class="dt">Nil</span></span>
<span id="cb30-13"><a href="#cb30-13" aria-hidden="true" tabindex="-1"></a>'a' :~ Nil :: List Char 1</span>
<span id="cb30-14"><a href="#cb30-14" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="ch">'b'</span> <span class="op">:~</span> <span class="ch">'a'</span> <span class="op">:~</span> <span class="dt">Nil</span></span>
<span id="cb30-15"><a href="#cb30-15" aria-hidden="true" tabindex="-1"></a>'b' :~ 'a' :~ Nil :: List Char 2</span></code></pre></div>
<ul>
<li>Type-safety of this list can be used to write a safe <code class="sourceCode haskell"><span class="fu">head</span></code> function which does not compile for an empty list:</li>
</ul>
<div class="sourceCode" id="cb31" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb31-1"><a href="#cb31-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb31-2"><a href="#cb31-2" aria-hidden="true" tabindex="-1"></a><span class="ot">> safeHead ::</span> <span class="dt">List</span> a (n <span class="op">+</span> <span class="dv">1</span>) <span class="ot">-></span> a</span>
<span id="cb31-3"><a href="#cb31-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> safeHead (x <span class="op">:~</span> _) <span class="ot">=</span> x</span>
<span id="cb31-4"><a href="#cb31-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb31-5"><a href="#cb31-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> safeHead (<span class="ch">'a'</span> <span class="op">:~</span> <span class="ch">'b'</span> <span class="op">:~</span> <span class="dt">Nil</span>)</span>
<span id="cb31-6"><a href="#cb31-6" aria-hidden="true" tabindex="-1"></a>'a'</span>
<span id="cb31-7"><a href="#cb31-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> safeHead <span class="dt">Nil</span></span>
<span id="cb31-8"><a href="#cb31-8" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb31-9"><a href="#cb31-9" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">21</span><span class="op">:</span><span class="dv">10</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb31-10"><a href="#cb31-10" aria-hidden="true" tabindex="-1"></a> • Couldn't match type ‘1’ with ‘0’</span>
<span id="cb31-11"><a href="#cb31-11" aria-hidden="true" tabindex="-1"></a> Expected type: List a (0 + 1)</span>
<span id="cb31-12"><a href="#cb31-12" aria-hidden="true" tabindex="-1"></a> Actual type: List a 0</span>
<span id="cb31-13"><a href="#cb31-13" aria-hidden="true" tabindex="-1"></a> • In the first argument of ‘safeHead’, namely ‘Nil’</span>
<span id="cb31-14"><a href="#cb31-14" aria-hidden="true" tabindex="-1"></a> In the expression: safeHead Nil</span>
<span id="cb31-15"><a href="#cb31-15" aria-hidden="true" tabindex="-1"></a> In an equation for ‘it’: it = safeHead Nil</span></code></pre></div>
<h3 id="heterogeneous-lists">Heterogeneous Lists</h3>
<p>We can use GADTs to build heterogeneous lists which can store values of different types and are type-safe to use.</p>
<p>First, the required extensions and imports:</p>
<div class="sourceCode" id="cb32" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb32-1"><a href="#cb32-1" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE KindSignatures #-}</span></span>
<span id="cb32-2"><a href="#cb32-2" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE DataKinds #-}</span></span>
<span id="cb32-3"><a href="#cb32-3" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE TypeOperators #-}</span></span>
<span id="cb32-4"><a href="#cb32-4" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE GADTs #-}</span></span>
<span id="cb32-5"><a href="#cb32-5" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE FlexibleInstances #-}</span></span>
<span id="cb32-6"><a href="#cb32-6" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE FlexibleContexts #-}</span></span>
<span id="cb32-7"><a href="#cb32-7" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE TypeApplications #-}</span></span>
<span id="cb32-8"><a href="#cb32-8" aria-hidden="true" tabindex="-1"></a><span class="ot">{-# LANGUAGE ScopedTypeVariables #-}</span></span>
<span id="cb32-9"><a href="#cb32-9" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb32-10"><a href="#cb32-10" aria-hidden="true" tabindex="-1"></a><span class="kw">module</span> <span class="dt">HList</span> <span class="kw">where</span></span>
<span id="cb32-11"><a href="#cb32-11" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb32-12"><a href="#cb32-12" aria-hidden="true" tabindex="-1"></a><span class="kw">import</span> <span class="dt">Data.Typeable</span></span></code></pre></div>
<p><code class="sourceCode haskell"><span class="dt">HList</span></code> is defined as a GADT:</p>
<div class="sourceCode" id="cb33" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb33-1"><a href="#cb33-1" aria-hidden="true" tabindex="-1"></a><span class="kw">data</span> <span class="dt">HList</span> (<span class="ot">ts ::</span> [<span class="op">*</span>]) <span class="kw">where</span></span>
<span id="cb33-2"><a href="#cb33-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">HNil</span><span class="ot"> ::</span> <span class="dt">HList</span> '[]</span>
<span id="cb33-3"><a href="#cb33-3" aria-hidden="true" tabindex="-1"></a><span class="ot"> (:#) ::</span> t <span class="ot">-></span> <span class="dt">HList</span> ts <span class="ot">-></span> <span class="dt">HList</span> (t '<span class="op">:</span> ts)</span>
<span id="cb33-4"><a href="#cb33-4" aria-hidden="true" tabindex="-1"></a><span class="kw">infixr</span> <span class="dv">5</span> <span class="op">:#</span></span></code></pre></div>
<p>Example usage:</p>
<div class="sourceCode" id="cb34" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb34-1"><a href="#cb34-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">HNil</span></span>
<span id="cb34-2"><a href="#cb34-2" aria-hidden="true" tabindex="-1"></a>HNil :: HList '[]</span>
<span id="cb34-3"><a href="#cb34-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb34-4"><a href="#cb34-4" aria-hidden="true" tabindex="-1"></a>'a' :# HNil :: HList '[Char]</span>
<span id="cb34-5"><a href="#cb34-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span><span class="kw">type</span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb34-6"><a href="#cb34-6" aria-hidden="true" tabindex="-1"></a>True :# 'a' :# HNil :: HList '[Bool, Char]</span></code></pre></div>
<p>We can write operations on <code class="sourceCode haskell"><span class="dt">HList</span></code>:</p>
<div class="sourceCode" id="cb35" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb35-1"><a href="#cb35-1" aria-hidden="true" tabindex="-1"></a><span class="ot">hLength ::</span> <span class="dt">HList</span> ts <span class="ot">-></span> <span class="dt">Int</span></span>
<span id="cb35-2"><a href="#cb35-2" aria-hidden="true" tabindex="-1"></a>hLength <span class="dt">HNil</span> <span class="ot">=</span> <span class="dv">0</span></span>
<span id="cb35-3"><a href="#cb35-3" aria-hidden="true" tabindex="-1"></a>hLength (x <span class="op">:#</span> xs) <span class="ot">=</span> <span class="dv">1</span> <span class="op">+</span> hLength xs</span>
<span id="cb35-4"><a href="#cb35-4" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb35-5"><a href="#cb35-5" aria-hidden="true" tabindex="-1"></a><span class="ot">hHead ::</span> <span class="dt">HList</span> (t '<span class="op">:</span> ts) <span class="ot">-></span> t</span>
<span id="cb35-6"><a href="#cb35-6" aria-hidden="true" tabindex="-1"></a>hHead (t <span class="op">:#</span> _) <span class="ot">=</span> t</span></code></pre></div>
<p>Example usage:</p>
<div class="sourceCode" id="cb36" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb36-1"><a href="#cb36-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> hLength <span class="op">$</span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb36-2"><a href="#cb36-2" aria-hidden="true" tabindex="-1"></a>2</span>
<span id="cb36-3"><a href="#cb36-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> hHead <span class="op">$</span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb36-4"><a href="#cb36-4" aria-hidden="true" tabindex="-1"></a>True</span>
<span id="cb36-5"><a href="#cb36-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> hHead <span class="dt">HNil</span></span>
<span id="cb36-6"><a href="#cb36-6" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb36-7"><a href="#cb36-7" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">7</span><span class="op">:</span><span class="dv">7</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb36-8"><a href="#cb36-8" aria-hidden="true" tabindex="-1"></a> • Couldn't match type ‘'[]’ with ‘t : ts0’</span>
<span id="cb36-9"><a href="#cb36-9" aria-hidden="true" tabindex="-1"></a> Expected type: HList (t : ts0)</span>
<span id="cb36-10"><a href="#cb36-10" aria-hidden="true" tabindex="-1"></a> Actual type: HList '[]</span>
<span id="cb36-11"><a href="#cb36-11" aria-hidden="true" tabindex="-1"></a> • In the first argument of ‘hHead’, namely ‘HNil’</span>
<span id="cb36-12"><a href="#cb36-12" aria-hidden="true" tabindex="-1"></a> In the expression: hHead HNil</span>
<span id="cb36-13"><a href="#cb36-13" aria-hidden="true" tabindex="-1"></a> In an equation for ‘it’: it = hHead HNil</span>
<span id="cb36-14"><a href="#cb36-14" aria-hidden="true" tabindex="-1"></a> • Relevant bindings include it :: t (bound at <interactive>:7:1)</span></code></pre></div>
<p>We need to define instances of typeclasses like <code class="sourceCode haskell"><span class="dt">Eq</span></code>, <code class="sourceCode haskell"><span class="dt">Ord</span></code> etc. for <code class="sourceCode haskell"><span class="dt">HList</span></code> because GHC cannot derive them automatically yet:</p>
<div class="sourceCode" id="cb37" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb37-1"><a href="#cb37-1" aria-hidden="true" tabindex="-1"></a><span class="kw">instance</span> <span class="dt">Eq</span> (<span class="dt">HList</span> '[]) <span class="kw">where</span></span>
<span id="cb37-2"><a href="#cb37-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">HNil</span> <span class="op">==</span> <span class="dt">HNil</span> <span class="ot">=</span> <span class="dt">True</span></span>
<span id="cb37-3"><a href="#cb37-3" aria-hidden="true" tabindex="-1"></a><span class="kw">instance</span> (<span class="dt">Eq</span> t, <span class="dt">Eq</span> (<span class="dt">HList</span> ts))</span>
<span id="cb37-4"><a href="#cb37-4" aria-hidden="true" tabindex="-1"></a> <span class="ot">=></span> <span class="dt">Eq</span> (<span class="dt">HList</span> (t '<span class="op">:</span> ts)) <span class="kw">where</span></span>
<span id="cb37-5"><a href="#cb37-5" aria-hidden="true" tabindex="-1"></a> (x <span class="op">:#</span> xs) <span class="op">==</span> (y <span class="op">:#</span> ys) <span class="ot">=</span></span>
<span id="cb37-6"><a href="#cb37-6" aria-hidden="true" tabindex="-1"></a> x <span class="op">==</span> y <span class="op">&&</span> xs <span class="op">==</span> ys</span>
<span id="cb37-7"><a href="#cb37-7" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb37-8"><a href="#cb37-8" aria-hidden="true" tabindex="-1"></a><span class="kw">instance</span> <span class="dt">Ord</span> (<span class="dt">HList</span> '[]) <span class="kw">where</span></span>
<span id="cb37-9"><a href="#cb37-9" aria-hidden="true" tabindex="-1"></a> <span class="dt">HNil</span> <span class="ot">`compare`</span> <span class="dt">HNil</span> <span class="ot">=</span> <span class="dt">EQ</span></span>
<span id="cb37-10"><a href="#cb37-10" aria-hidden="true" tabindex="-1"></a><span class="kw">instance</span> (<span class="dt">Ord</span> t, <span class="dt">Ord</span> (<span class="dt">HList</span> ts))</span>
<span id="cb37-11"><a href="#cb37-11" aria-hidden="true" tabindex="-1"></a> <span class="ot">=></span> <span class="dt">Ord</span> (<span class="dt">HList</span> (t '<span class="op">:</span> ts)) <span class="kw">where</span></span>
<span id="cb37-12"><a href="#cb37-12" aria-hidden="true" tabindex="-1"></a> (x <span class="op">:#</span> xs) <span class="ot">`compare`</span> (y <span class="op">:#</span> ys) <span class="ot">=</span></span>
<span id="cb37-13"><a href="#cb37-13" aria-hidden="true" tabindex="-1"></a> x <span class="ot">`compare`</span> y <span class="op"><></span> xs <span class="ot">`compare`</span> ys</span>
<span id="cb37-14"><a href="#cb37-14" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb37-15"><a href="#cb37-15" aria-hidden="true" tabindex="-1"></a><span class="kw">instance</span> <span class="dt">Show</span> (<span class="dt">HList</span> '[]) <span class="kw">where</span></span>
<span id="cb37-16"><a href="#cb37-16" aria-hidden="true" tabindex="-1"></a> <span class="fu">show</span> <span class="dt">HNil</span> <span class="ot">=</span> <span class="st">"[]"</span></span>
<span id="cb37-17"><a href="#cb37-17" aria-hidden="true" tabindex="-1"></a><span class="kw">instance</span> (<span class="dt">Typeable</span> t, <span class="dt">Show</span> t, <span class="dt">Show</span> (<span class="dt">HList</span> ts))</span>
<span id="cb37-18"><a href="#cb37-18" aria-hidden="true" tabindex="-1"></a> <span class="ot">=></span> <span class="dt">Show</span> (<span class="dt">HList</span> (t '<span class="op">:</span> ts)) <span class="kw">where</span></span>
<span id="cb37-19"><a href="#cb37-19" aria-hidden="true" tabindex="-1"></a> <span class="fu">show</span> (x <span class="op">:#</span> xs) <span class="ot">=</span></span>
<span id="cb37-20"><a href="#cb37-20" aria-hidden="true" tabindex="-1"></a> <span class="fu">show</span> x </span>
<span id="cb37-21"><a href="#cb37-21" aria-hidden="true" tabindex="-1"></a> <span class="op">++</span> <span class="st">"@"</span> <span class="op">++</span> <span class="fu">show</span> (typeRep (<span class="dt">Proxy</span> <span class="op">@</span>t))</span>
<span id="cb37-22"><a href="#cb37-22" aria-hidden="true" tabindex="-1"></a> <span class="op">++</span> <span class="st">" :# "</span> <span class="op">++</span> <span class="fu">show</span> xs</span></code></pre></div>
<p>The instances are defined recursively: one for the base case and one for the inductive case.</p>
<p>Example usage:</p>
<div class="sourceCode" id="cb38" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb38-1"><a href="#cb38-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span> <span class="op">==</span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb38-2"><a href="#cb38-2" aria-hidden="true" tabindex="-1"></a>True</span>
<span id="cb38-3"><a href="#cb38-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span> <span class="op">==</span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'b'</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb38-4"><a href="#cb38-4" aria-hidden="true" tabindex="-1"></a>False</span>
<span id="cb38-5"><a href="#cb38-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span> <span class="op">==</span> <span class="dt">True</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb38-6"><a href="#cb38-6" aria-hidden="true" tabindex="-1"></a></span>
<span id="cb38-7"><a href="#cb38-7" aria-hidden="true" tabindex="-1"></a><span class="ot"><</span>interactive<span class="op">>:</span><span class="dv">17</span><span class="op">:</span><span class="dv">24</span><span class="op">:</span> <span class="fu">error</span><span class="op">:</span></span>
<span id="cb38-8"><a href="#cb38-8" aria-hidden="true" tabindex="-1"></a> • Couldn't match type ‘'[]’ with ‘'[Char]’</span>
<span id="cb38-9"><a href="#cb38-9" aria-hidden="true" tabindex="-1"></a> Expected type: HList '[Bool, Char]</span>
<span id="cb38-10"><a href="#cb38-10" aria-hidden="true" tabindex="-1"></a> Actual type: HList '[Bool]</span>
<span id="cb38-11"><a href="#cb38-11" aria-hidden="true" tabindex="-1"></a> • In the second argument of ‘(==)’, namely ‘True :# HNil’</span>
<span id="cb38-12"><a href="#cb38-12" aria-hidden="true" tabindex="-1"></a> In the expression: True :# 'a' :# HNil == True :# HNil</span>
<span id="cb38-13"><a href="#cb38-13" aria-hidden="true" tabindex="-1"></a> In an equation for ‘it’: it = True :# 'a' :# HNil == True :# HNil</span>
<span id="cb38-14"><a href="#cb38-14" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="fu">show</span> <span class="op">$</span> <span class="dt">True</span> <span class="op">:#</span> <span class="ch">'a'</span> <span class="op">:#</span> <span class="dt">HNil</span></span>
<span id="cb38-15"><a href="#cb38-15" aria-hidden="true" tabindex="-1"></a>"True@Bool :# 'a'@Char :# []"</span></code></pre></div>
<h3 id="creating-new-constraints">Creating New Constraints</h3>
<ul>
<li>Type families can be used to create new Constraints:</li>
</ul>
<div class="sourceCode" id="cb39" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb39-1"><a href="#cb39-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XKindSignatures</span></span>
<span id="cb39-2"><a href="#cb39-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XDataKinds</span></span>
<span id="cb39-3"><a href="#cb39-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeOperators</span></span>
<span id="cb39-4"><a href="#cb39-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XTypeFamilies</span></span>
<span id="cb39-5"><a href="#cb39-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>m <span class="op">+</span><span class="dt">Data.Constraint</span></span>
<span id="cb39-6"><a href="#cb39-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb39-7"><a href="#cb39-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">type</span> <span class="kw">family</span> <span class="dt">AllEq</span> (<span class="ot">ts ::</span> [<span class="op">*</span>])<span class="ot"> ::</span> <span class="dt">Constraint</span> <span class="kw">where</span></span>
<span id="cb39-8"><a href="#cb39-8" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">AllEq</span> '[] <span class="ot">=</span> ()</span>
<span id="cb39-9"><a href="#cb39-9" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">AllEq</span> (t '<span class="op">:</span> ts) <span class="ot">=</span> (<span class="dt">Eq</span> t, <span class="dt">AllEq</span> ts)</span>
<span id="cb39-10"><a href="#cb39-10" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span>
<span id="cb39-11"><a href="#cb39-11" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>kind<span class="op">!</span> <span class="dt">AllEq</span> '[<span class="dt">Bool</span>, <span class="dt">Char</span>]</span>
<span id="cb39-12"><a href="#cb39-12" aria-hidden="true" tabindex="-1"></a>AllEq '[Bool, Char] :: Constraint</span>
<span id="cb39-13"><a href="#cb39-13" aria-hidden="true" tabindex="-1"></a>= (Eq Bool, (Eq Char, () :: Constraint))</span></code></pre></div>
<ul>
<li><code class="sourceCode haskell"><span class="dt">AllEq</span></code> is a type-level function from a list of types to a constraint.</li>
<li>With the <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-ConstraintKinds" target="_blank" rel="noopener"><code>ConstraintKinds</code></a> extension, <code class="sourceCode haskell"><span class="dt">AllEq</span></code> can be made polymorphic over all constraints instead of just <code class="sourceCode haskell"><span class="dt">Eq</span></code>:</li>
</ul>
<div class="sourceCode" id="cb40" data-lang="ghci"><pre class="sourceCode lhs numberSource"><code class="sourceCode literatehaskell"><span id="cb40-1"><a href="#cb40-1" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>set <span class="op">-</span><span class="dt">XConstraintKinds</span></span>
<span id="cb40-2"><a href="#cb40-2" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>{</span>
<span id="cb40-3"><a href="#cb40-3" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="kw">type</span> <span class="kw">family</span> <span class="dt">All</span> (<span class="ot">c ::</span> <span class="op">*</span> <span class="ot">-></span> <span class="dt">Constraint</span>)</span>
<span id="cb40-4"><a href="#cb40-4" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> (<span class="ot">ts ::</span> [<span class="op">*</span>])<span class="ot"> ::</span> <span class="dt">Constraint</span> <span class="kw">where</span></span>
<span id="cb40-5"><a href="#cb40-5" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">All</span> c '[] <span class="ot">=</span> ()</span>
<span id="cb40-6"><a href="#cb40-6" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="dt">All</span> c (t '<span class="op">:</span> ts) <span class="ot">=</span> (c t, <span class="dt">All</span> c ts)</span>
<span id="cb40-7"><a href="#cb40-7" aria-hidden="true" tabindex="-1"></a><span class="ot">></span> <span class="op">:</span>}</span></code></pre></div>
<ul>
<li>With <code class="sourceCode haskell"><span class="dt">All</span></code>, instances for <code class="sourceCode haskell"><span class="dt">HList</span></code> can be written non-recursively:</li>
</ul>
<div class="sourceCode" id="cb41" data-lang="haskell"><pre class="sourceCode numberSource haskell"><code class="sourceCode haskell"><span id="cb41-1"><a href="#cb41-1" aria-hidden="true" tabindex="-1"></a><span class="kw">instance</span> <span class="dt">All</span> <span class="dt">Eq</span> ts <span class="ot">=></span> <span class="dt">Eq</span> (<span class="dt">HList</span> ts) <span class="kw">where</span></span>
<span id="cb41-2"><a href="#cb41-2" aria-hidden="true" tabindex="-1"></a> <span class="dt">HNil</span> <span class="op">==</span> <span class="dt">HNil</span> <span class="ot">=</span> <span class="dt">True</span></span>
<span id="cb41-3"><a href="#cb41-3" aria-hidden="true" tabindex="-1"></a> (a <span class="op">:#</span> as) <span class="op">==</span> (b <span class="op">:#</span> bs) <span class="ot">=</span> a <span class="op">==</span> b <span class="op">&&</span> as <span class="op">==</span> bs</span></code></pre></div>
<h2 data-track-content data-content-name="conclusion" data-content-piece="twt-notes-1" id="conclusion">Conclusion</h2>
<p>I’m still in the process of reading the book and I’ll post the notes for the rest of the chapters in a later post. The complete code for <code>HList</code> can be found <a href="https://abhinavsarkar.net/code/hlist.html?mtm_campaign=feed">here</a>.</p><p>If you liked this post, please <a href="https://abhinavsarkar.net/posts/twt-notes-1/?mtm_campaign=feed#syndications">leave a comment</a>.</p><img referrerpolicy="no-referrer-when-downgrade" src="https://anna.abhinavsarkar.net/matomo.php?idsite=1&rec=1" style="border:0" alt="" />2020-03-18T00:00:00Z<p><a href="https://www.haskell.org" target="_blank" rel="noopener">Haskell</a>—with its powerful type system—has a great support for type-level programming and it has gotten much better in the recent times with the new releases of the <a href="https://www.haskell.org/ghc/" target="_blank" rel="noopener">GHC</a> compiler. But type-level programming remains a daunting topic even with seasoned haskellers. <em><a href="https://thinkingwithtypes.com/" target="_blank" rel="noopener">Thinking with Types: Type-level Programming in Haskell</a></em> by <a href="https://sandymaguire.me/about/" target="_blank" rel="noopener">Sandy Maguire</a> is a book which attempts to fix that. I’ve taken some notes to summarize my understanding of the same.</p>