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
Copy file name to clipboardExpand all lines: Physics/src/Dimensions/ValueLevel.lhs
+25-23Lines changed: 25 additions & 23 deletions
Original file line number
Diff line number
Diff line change
@@ -2,15 +2,6 @@
2
2
Value-level dimensions
3
3
======================
4
4
5
-
From the introduction, two things became apparanent:
6
-
7
-
1. Given the unit of a quantity, its dimension is known implicitly.
8
-
2. If we only work with SI-units, there is a one-to-one correspondence between dimensions and units.
9
-
10
-
We'll use these facts when implementing dimensions. More precisely, "length" and "metre" will be interchangable, and so on.
11
-
12
-
What you see below is the [Haskell module syntax](http://learnyouahaskell.com/modules#making-our-own-modules). Why do we show it to you? Because we don't want to hide any code from you if you follow along this tutorial.
13
-
14
5
> moduleDimensions.ValueLevel
15
6
> ( Dim(..)
16
7
> , mul
@@ -24,10 +15,17 @@ What you see below is the [Haskell module syntax](http://learnyouahaskell.com/mo
24
15
> , luminosity
25
16
> , one
26
17
> ) where
27
-
18
+
>
28
19
> importPreludehiding (length, div)
29
20
30
-
A dimension can be seen as a product of the base dimensions, with an individual exponent on each base dimension. Since the 7 base dimensions are known in advance, we can design our data type using this fact.
21
+
From the introduction, two things became apparanent:
22
+
23
+
1. Given the unit of a quantity, its dimension is known implicitly.
24
+
2. If we only work with SI-units, there is a one-to-one correspondence between dimensions and units.
25
+
26
+
We'll use these facts when implementing dimensions. More precisely, "length" and "metre" will be interchangable, and so on.
27
+
28
+
A dimension can be seen as a product of the base dimensions, with an individual exponent on each base dimension. Because the 7 base dimensions are known in advance, we can design our data type using this fact.
31
29
32
30
> dataDim=DimInteger-- Length
33
31
>Integer-- Mass
@@ -64,8 +62,8 @@ Noticed how we used "m" (for metre) for implicitly refering to the dimension "le
64
62
> area =Dim2000000
65
63
> charge =Dim0011000
66
64
67
-
</div>
68
-
</details>
65
+
</div>
66
+
</details>
69
67
70
68
Multiplication and division
71
69
---------------------------
@@ -86,8 +84,8 @@ Dimensions can be multiplied and divided. Velocity is, as we just saw, a divisio
It's now possible to construct dimensions in the following fashion.
93
91
@@ -96,8 +94,6 @@ It's now possible to construct dimensions in the following fashion.
96
94
> force = mass `mul` acceleration
97
95
> momentum = force `mul` time
98
96
99
-
TODO: try to replace "since" by "because" (in many places) to avoid confusion with the meaning of "since" in the time-domain.
100
-
101
97
A dimension we so far haven't mentioned is the *scalar*, which shows up when working with, for example, coefficients of friction. It's dimensionless because it arises from division of two equal dimensions. The case of coefficients of friction looks like
102
98
103
99
\begin{align}
@@ -113,19 +109,21 @@ A dimension we so far haven't mentioned is the *scalar*, which shows up when wor
113
109
> one =Dim0000000
114
110
> one' = force `div` force
115
111
116
-
</div>
117
-
</details>
112
+
</div>
113
+
</details>
118
114
119
115
Pretty-printer
120
116
--------------
121
117
122
-
{.float-img-left}
118
+
{.float-img-left}
123
119
124
120
The purpose of value-level dimensions is to be able to print 'em nicely. The pretty printer should be function with the type
125
121
126
122
< showDim::Dim->String
127
123
128
-
meaning it shows a dimension as a string. How to actually implement this is not the interesting part in this tutorial, so you may with good conscience skip this implementation. However, if you're curios, you can still take a look at it.
124
+
meaning it shows a dimension as a string. But how to actually implement this is not the interesting part of this tutorial. Hence we skip it.
125
+
126
+
\ignore{
129
127
130
128
> showDim::Dim->String
131
129
> showDim (Dim le ma ti cu te su lu)
@@ -156,11 +154,15 @@ meaning it shows a dimension as a string. How to actually implement this is not
156
154
> len:: (Integraln) => [a] ->n
157
155
> len []=0
158
156
> len (a:as) =1+ len as
159
-
>
157
+
158
+
}
159
+
160
+
We use `showDim` to make `Dim` an instance of `Show`
{.float-img-left}
6
-
7
-
For operations on dimensions, there are a number of laws which should hold. We will here test that the value-level dimensions obey them. One way is to use `QuickCheck`, which produces lots o' random test cases.
8
-
9
5
> moduleDimensions.ValueLevel.Test
10
6
> ( runTests
11
7
> ) where
12
-
8
+
>
13
9
> importPreludehiding (length, div)
14
10
> importTest.QuickCheck
15
11
> importData.List
16
-
12
+
>
17
13
> importDimensions.ValueLevel
18
14
15
+
{.float-img-left}
16
+
17
+
For operations on dimensions, there are a number of laws which should hold. We will here test that the value-level dimensions obey them. One way is to use `QuickCheck`, which produces lots o' random test cases.
18
+
19
19
Generating arbitrary dimensions
20
20
-------------------------------
21
21
@@ -34,7 +34,7 @@ An arbitrary example of an `Arbitrary` instance (get it?) could look like
34
34
< instanceArbitraryIntPairwhere
35
35
< arbitrary = genIntPair
36
36
37
-
**Exercise.** Now try to implement an `Arbitrary` instance of `Dim`.
37
+
**Exercise** Now try to implement an `Arbitrary` instance of `Dim`.
38
38
39
39
<details>
40
40
<summary>**Solution**</summary>
@@ -56,8 +56,8 @@ Here's one way to do it.
56
56
> instanceArbitraryDimwhere
57
57
> arbitrary = genDim
58
58
59
-
</div>
60
-
</details>
59
+
</div>
60
+
</details>
61
61
62
62
Properties for operations on dimensions
63
63
---------------------------------------
@@ -71,7 +71,10 @@ The laws to test are
71
71
- `one` is a unit for multiplication
72
72
- Multiplication and division cancel each other out
73
73
- Dividing by `one` does nothing
74
-
- Dividing by a division brings up the lowest denominator [TODO: strange wording?? Perhaps use a formula instead. (and perhaps use `recip` to simplify?)]
74
+
- Dividing by a division brings up the lowest denominator
75
+
\begin{align}
76
+
\frac{x}{\frac{x}{y}} = y
77
+
\end{align}
75
78
- Multiplication by $x$ is the same as dividing by the inverse of $x$.
76
79
77
80
The implementation of the first law looks like
@@ -97,10 +100,6 @@ Here's what the rest could look like.
>-- Property: multiplication same as division by inverse
113
116
> prop_mulDivInv::Dim->Dim->Bool
114
117
> prop_mulDivInv d1 d2 = d1 `mul` d2 ==
115
118
> d1 `div` (one `div` d2)
116
119
117
-
</div>
118
-
</details>
119
-
120
-
Testing the pretty-printer
121
-
--------------------------
122
-
123
-
TODO: It is good that you test it, but I suggest you keep that out of the learning material [perhaps a link to "extra reading"].
124
-
125
-
We rely pretty heavily on the pretty-printer. Let's test it too! We won't get too ambitious in our testing of it. It'll be enough to check that if a dimension has a nonzero
126
-
127
-
TODO: Do something about the problem of m and mol.
128
-
129
-
-- Property: pretty-printed has correct of a dimension
130
-
prop_correctDim :: Integer -> Dim -> Bool
131
-
prop_correctDim i d = prop_correctDim' (i `mod` 7) d (show d)
132
-
133
-
prop_correctDim' :: Integer -> Dim -> String -> Bool
134
-
prop_correctDim' 0 (Dim le ma ti cu te su lu) str =
135
-
prop_correctDim'' le "m" str
136
-
prop_correctDim' 1 (Dim le ma ti cu te su lu) str =
137
-
prop_correctDim'' ma "kg" str
138
-
prop_correctDim' 2 (Dim le ma ti cu te su lu) str =
139
-
prop_correctDim'' ti "s" str
140
-
prop_correctDim' 3 (Dim le ma ti cu te su lu) str =
141
-
prop_correctDim'' cu "A" str
142
-
prop_correctDim' 4 (Dim le ma ti cu te su lu) str =
143
-
prop_correctDim'' te "K" str
144
-
prop_correctDim' 5 (Dim le ma ti cu te su lu) str =
145
-
prop_correctDim'' su "mol" str
146
-
prop_correctDim' 6 (Dim le ma ti cu te su lu) str =
-- kg^2 (eller dylikt) ska finns exakt en gång i rätt nivå
171
-
-- och inte finns alls i fel nivå.
172
-
173
-
-- Exatcly once. Not more or less
174
-
occursOnce :: (Eq a) => [a] -> [a] -> Bool
175
-
occursOnce a = (==1) . numOccurs a
176
-
177
-
occursNever :: (Eq a) => [a] -> [a] -> Bool
178
-
occursNever a = (==0) . numOccurs a
179
-
180
-
-- How many times the first list occurs in the second one
181
-
numOccurs :: (Eq a) => [a] -> [a] -> Int
182
-
numOccurs subList list = len $ filter (==subList) sg
183
-
where
184
-
sg = subGroups (len subList) list
185
-
186
-
-- Groups the list into lists of the specified length
187
-
subGroups :: Int -> [a] -> [[a]]
188
-
subGroups n _
189
-
| n < 1 = error "Groups must be at least 1 big"
190
-
subGroups _ [] = []
191
-
subGroups n list@(_:rest)
192
-
| n > len list = []
193
-
| otherwise = (take n list):(subGroups n rest)
194
-
195
-
-- Length of a list
196
-
len :: [a] -> Int
197
-
len [] = 0
198
-
len (x:xs) = 1 + len xs
199
-
200
-
Integrating tests with Stack
201
-
----------------------------
202
-
203
-
This project uses `Stack`. One part of `Stack` is continous testing, and for it to work on the tests we developed here, the following functions is needed.
120
+
</div>
121
+
</details>
122
+
123
+
We should also test the pretty-printer. But just like how that function itself is implemented isn't interesting, neither is the code testing it. We therefore leave it out.
124
+
125
+
From this module, we export a function `runTests`. That function runs all the tests implemented here and is used with Stack.
126
+
127
+
\ignore{
128
+
129
+
> prop_correctDim::Integer->Dim->Bool
130
+
> prop_correctDim i d = prop_correctDim' (i `mod`7) d (show d)
131
+
>
132
+
> prop_correctDim'::Integer->Dim->String->Bool
133
+
> prop_correctDim' 0 (Dim le ma ti cu te su lu) str =
134
+
> prop_correctDim'' le "m" str
135
+
> prop_correctDim' 1 (Dim le ma ti cu te su lu) str =
136
+
> prop_correctDim'' ma "kg" str
137
+
> prop_correctDim' 2 (Dim le ma ti cu te su lu) str =
138
+
> prop_correctDim'' ti "s" str
139
+
> prop_correctDim' 3 (Dim le ma ti cu te su lu) str =
140
+
> prop_correctDim'' cu "A" str
141
+
> prop_correctDim' 4 (Dim le ma ti cu te su lu) str =
142
+
> prop_correctDim'' te "K" str
143
+
> prop_correctDim' 5 (Dim le ma ti cu te su lu) str =
144
+
> prop_correctDim'' su "mol" str
145
+
> prop_correctDim' 6 (Dim le ma ti cu te su lu) str =
0 commit comments