You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<p>What’s the relation between these? A <em>quantity</em> has a <em>dimension</em>. The number describing the distance between Stockholm and Gothenburg is of the type length. A <em>quantity</em> also has a <em>unit</em> that relates the number to a known definite distance. The unit of a quantity must describe the dimension of the quantity. It’s not possible to describe a distance with joule. However, describing a distance is possible with both metres and inches. Those are two different units describing a quantity of the same dimension.</p>
31
31
<p>The dimension of a quantity is often implicitly understood given its unit. If I have a rope of 1 metre, you know it’s a length I’m talking about.</p>
32
32
<p>There are 7 <em>base dimensions</em>, each with a corresponding SI-unit.</p>
33
+
<figure>
34
+
<imgsrc="Base_dimensions.png" alt="The 7 base dimensions" class="float-img-right" /><figcaption>The 7 base dimensions</figcaption>
<p>We will now implement <em>type-level</em> dimensions. What is type-level? When one usually programs (in Haskell), one operatates (e.g. adds) on values (e.g. <code>1</code> and <code>2</code>). This is on <em>value-level</em>. Now we’ll do the same thing but on <em>type-level</em>, that is, perform operations on types.</p>
24
24
<p>What’s the purpose of type-level dimensions? It’s so we’ll notice as soon as compile-time if we’ve written something incorrect. E.g. adding a length and an area is not allowed since they have different dimensions.</p>
25
+
<figure>
26
+
<imgsrc="Lengths_and_area.png" alt="Adding lengths is OK. Adding lengths and areas is not OK." /><figcaption>Adding lengths is OK. Adding lengths and areas is not OK.</figcaption>
27
+
</figure>
25
28
<p>This implemention is very similar to the value-level one. It would be possible to only have one implementation by using <code>Data.Proxy</code>. But it would be trickier. This way is lengthier but easier to understand.</p>
26
29
<p>To be able to do type-level programming, we’ll need a nice stash of GHC-extensions.</p>
27
30
<divclass="sourceCode" id="cb1"><preclass="sourceCode literate haskell"><codeclass="sourceCode haskell"><aclass="sourceLine" id="cb1-1" data-line-number="1"><spanclass="ot">{-# LANGUAGE DataKinds #-}</span></a>
<p>We’ll need to be able to operate on integers on type-level. Instead of implementing it ourselves, we will just import the machinery so we can focus on the physics-part.</p>
51
+
<p>We’ll need to be able to operate on integers on the type-level. Instead of implementing it ourselves, we will just import the machinery so we can focus on the physics-part.</p>
<p>We make a <em>kind</em> for dimensions, just like we in the previous section made <em>type</em> for dimensions. On value-level we made a <em>type</em> with <em>values</em>. Now we make a <em>kind</em> with <em>types</em>. The meaning is exactly the same, except we have moved “one step up”.</p>
<aclass="sourceLine" id="cb7-5" data-line-number="5"><spanclass="kw">type</span><spanclass="dt">Temperature</span><spanclass="fu">=</span><spanclass="ch">'Dim Zero Zero Zero Zero Pos1 Zero Zero</span></a>
84
87
<aclass="sourceLine" id="cb7-6" data-line-number="6"><spanclass="kw">type</span><spanclass="dt">Substance</span><spanclass="fu">=</span><spanclass="ch">'Dim Zero Zero Zero Zero Zero Pos1 Zero</span></a>
85
88
<aclass="sourceLine" id="cb7-7" data-line-number="7"><spanclass="kw">type</span><spanclass="dt">Luminosity</span><spanclass="fu">=</span><spanclass="ch">'Dim Zero Zero Zero Zero Zero Zero Pos1</span></a></code></pre></div>
89
+
<p><code>'Dim</code> is used to distinguish between the <em>type</em><code>Dim</code> (left-hand-side of the <code>data Dim</code> definition) and the <em>type constructor</em><code>Dim</code> (right-hand-side of the <code>data Dim</code> definition, with <code>DataKinds</code>-perspective). <code>'Dim</code> refers to the type constructor. Both are created when using <code>DataKinds</code>.</p>
90
+
<p><code>Pos1</code>, <code>Neg1</code> and so on corresponds to <code>1</code> and <code>-1</code> in the imported package, which operates on type-level integers.</p>
91
+
<p><strong>Exercise.</strong> Create types for velocity, acceleration and the scalar.</p>
92
+
<p><strong>Solution.</strong></p>
86
93
<divclass="sourceCode" id="cb8"><preclass="sourceCode literate haskell"><codeclass="sourceCode haskell"><aclass="sourceLine" id="cb8-1" data-line-number="1"><spanclass="kw">type</span><spanclass="dt">Velocity</span><spanclass="fu">=</span><spanclass="ch">'Dim Pos1 Zero Neg1 Zero Zero Zero Zero</span></a>
87
94
<aclass="sourceLine" id="cb8-2" data-line-number="2"><spanclass="kw">type</span><spanclass="dt">Acceleration</span><spanclass="fu">=</span><spanclass="ch">'Dim Pos1 Zero Neg2 Zero Zero Zero Zero</span></a></code></pre></div>
88
95
<divclass="sourceCode" id="cb9"><preclass="sourceCode literate haskell"><codeclass="sourceCode haskell"><aclass="sourceLine" id="cb9-1" data-line-number="1"><spanclass="kw">type</span><spanclass="dt">One</span><spanclass="fu">=</span><spanclass="ch">'Dim Zero Zero Zero Zero Zero Zero Zero</span></a></code></pre></div>
89
-
<p><code>'Dim</code> is used to distinguish between the <em>type</em><code>Dim</code> (left-hand-side of the <code>data Dim</code> definition) and the <em>type constructor</em><code>Dim</code> (right-hand-side of the <code>data Dim</code> definition, with <code>DataKinds</code>-perspective). <code>'Dim</code> refers to the type constructor. Both are created when using <code>DataKinds</code>.</p>
90
-
<p><code>Pos1</code>, <code>Neg1</code> and so on corresponds to <code>1</code> and <code>-1</code> in the imported package, which operates on type-level integers.</p>
91
96
<h2id="multiplication-and-division">Multiplication and division</h2>
92
97
<p>Let’s implement multiplication and division on type-level. After such an operation a new dimension is created. And from the previous section we already know what the dimension should look like. To translate to Haskell-language: “after such an operation a new <em>type</em> is created”. How does one implement that? With <code>type family</code>! <code>type family</code> can easiest be thought of as a function on the type-level.</p>
<p>Perhaps not very exiting so far. But just wait ’til we create a data type for quantities. Then the strenghts of type-level dimensions will be clearer.</p>
115
128
116
129
</main>
117
130
118
131
<footer>
132
+
<nav>
133
+
<span>Previous: <ahref="../Dimensions/Testing of value-level dimensions.html">Testing of value-level dimensions</a></span>
0 commit comments