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/Quantity/Test.lhs
+23-25Lines changed: 23 additions & 25 deletions
Original file line number
Diff line number
Diff line change
@@ -2,6 +2,8 @@
2
2
Testing of Quantity
3
3
===================
4
4
5
+
\ignore{
6
+
5
7
> {-# LANGUAGE DataKinds #-}
6
8
> {-# LANGUAGE GADTs #-}
7
9
> {-# LANGUAGE KindSignatures #-}
@@ -11,11 +13,23 @@ Testing of Quantity
11
13
> {-# LANGUAGE FlexibleInstances #-}
12
14
> {-# LANGUAGE TypeSynonymInstances #-}
13
15
16
+
}
17
+
14
18
> moduleDimensions.Quantity.Test
15
19
> ( runTests
16
20
> )
17
21
>where
18
22
23
+
24
+
< {-# LANGUAGE DataKinds #-}
25
+
< {-# LANGUAGE GADTs #-}
26
+
< {-# LANGUAGE KindSignatures #-}
27
+
< {-# LANGUAGE TypeFamilies #-}
28
+
< {-# LANGUAGE UndecidableInstances #-}
29
+
< {-# LANGUAGE TypeOperators #-}
30
+
< {-# LANGUAGE FlexibleInstances #-}
31
+
< {-# LANGUAGE TypeSynonymInstances #-}
32
+
19
33
> importPreludehiding (length, div)
20
34
> importTest.QuickCheck
21
35
@@ -36,9 +50,9 @@ First we need an `Arbitrary` instance for `Quantity d val`. For `d` we'll mostly
36
50
A generator for an arbitrary dimension.
37
51
38
52
> genQuantity::QuantitydDouble->Gen (Qd)
39
-
> genQuantity sugar=do
53
+
> genQuantity quantity=do
40
54
> value <- arbitrary
41
-
>return (value #sugar)
55
+
>return (value #quantity)
42
56
43
57
And now we make `Arbitrary` instances of arbitrary selected dimensions in the `Quantity`s.
44
58
@@ -57,7 +71,7 @@ And now we make `Arbitrary` instances of arbitrary selected dimensions in the `Q
57
71
Testing arithmetic properties
58
72
-----------------------------
59
73
60
-
One regular numbers, and hence too on quantites with their dimensions, a bunch of properties should hold. The things we test here are
74
+
On regular numbers, and hence too on quantites with their dimensions, a bunch of properties should hold. The things we test here are
61
75
62
76
- Addition commutative
63
77
- Addition associative
@@ -69,20 +83,14 @@ One regular numbers, and hence too on quantites with their dimensions, a bunch o
69
83
- Subtraction and addition cancel each other out
70
84
- Division and multiplication cancel each other out
71
85
- Pythagoran trigonometric identity
72
-
- The sugar doesn't care about input value
73
86
74
87
Let's start!
75
88
76
89
We could write the type signatures in a general way like
77
90
78
91
< prop_addCom::Qd->Qd->Bool
79
92
80
-
But we won't do that for two reasons.
81
-
82
-
1. QuickCheck needs concrete types in order to work. So we would have to do a bunch of specialization anyway. And even if we begin with a general signature, we can't cover all cases since there are infinitly many dimensions.
83
-
2. TODO: Går inte för vissa fall, t.ex.
84
-
85
-
<Couldn't match type `Mul d (Mul d d)' with `Mul (Mul d d) d'
93
+
But we won't do that since QuickCheck needs concrete types in order to work. So we would have to do a bunch of specialization anyway. And even if we begin with a general signature, we can't cover all cases since there are infinitly many dimensions.
86
94
87
95
Instead we'll pick some arbitrary dimensions that have an `Arbitrary` instance.
88
96
@@ -98,7 +106,6 @@ Instead we'll pick some arbitrary dimensions that have an `Arbitrary` instance.
98
106
> prop_addId::QTime->Bool
99
107
> prop_addId a = zero +# a ~= a
100
108
>where
101
-
> -- `zero` will, thanks to the versatile suger, have > -- the same dimension as `a`.
102
109
> zero =0# a
103
110
104
111
>-- a * b = b * a
@@ -133,33 +140,24 @@ Instead we'll pick some arbitrary dimensions that have an `Arbitrary` instance.
Copy file name to clipboardExpand all lines: Physics/src/Dimensions/TypeLevel.lhs
+33-22Lines changed: 33 additions & 22 deletions
Original file line number
Diff line number
Diff line change
@@ -2,15 +2,7 @@
2
2
Type-level dimensions
3
3
=====================
4
4
5
-
We will now implement *type-level* dimensions. What is type-level? Programs (in Haskell) normally operatate on (e.g. add) values (e.g. `1` and `2`). This is on *value-level*. Now we'll do the same thing but on *type-level*, that is, perform operations on types.
6
-
7
-
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.
8
-
9
-
10
-
11
-
This implemention is very similar to the value-level one. It would be possible to only have one implementation by using `Data.Proxy`. But it would be trickier. This way is lengthier but easier to understand.
12
-
13
-
To be able to do type-level programming, we'll need a nice stash of GHC-extensions.
5
+
\ignore{
14
6
15
7
> {-# LANGUAGE DataKinds #-}
16
8
> {-# LANGUAGE GADTs #-}
@@ -19,7 +11,7 @@ To be able to do type-level programming, we'll need a nice stash of GHC-extensio
19
11
> {-# LANGUAGE UndecidableInstances #-}
20
12
> {-# LANGUAGE TypeOperators #-}
21
13
22
-
See the end of the next chapter to read what they do.
14
+
}
23
15
24
16
> moduleDimensions.TypeLevel
25
17
> ( Dim(..)
@@ -35,6 +27,25 @@ See the end of the next chapter to read what they do.
35
27
> , One
36
28
> ) where
37
29
30
+
We will now implement *type-level* dimensions. What is type-level? Programs (in Haskell) normally operatate on (e.g. add) values (e.g. `1` and `2`). This is on *value-level*. Now we'll do the same thing but on *type-level*, that is, perform operations on types.
31
+
32
+
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.
33
+
34
+
{.img-center}
35
+
36
+
This implemention is very similar to the value-level one. It would be possible to only have one implementation by using `Data.Proxy`. But it would be trickier. This way is lengthier but easier to understand.
37
+
38
+
To be able to do type-level programming, we'll need a nice stash of GHC-extensions.
39
+
40
+
< {-# LANGUAGE DataKinds #-}
41
+
< {-# LANGUAGE GADTs #-}
42
+
< {-# LANGUAGE KindSignatures #-}
43
+
< {-# LANGUAGE TypeFamilies #-}
44
+
< {-# LANGUAGE UndecidableInstances #-}
45
+
< {-# LANGUAGE TypeOperators #-}
46
+
47
+
See the end of the next chapter to read what they do.
48
+
38
49
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.
39
50
40
51
> importNumeric.NumType.DK.Integers
@@ -87,7 +98,7 @@ This may sound confusing, but the point of this will become clear over time. Let
87
98
88
99
`Pos1`, `Neg1` and so on corresponds to `1` and `-1` in the imported package, which operates on type-level integers.
89
100
90
-
**Exercise.** Create types for velocity, acceleration and the scalar.
101
+
**Exercise** Create types for velocity, acceleration and the scalar.
91
102
92
103
<details>
93
104
<summary>**Solution**</summary>
@@ -98,8 +109,8 @@ This may sound confusing, but the point of this will become clear over time. Let
98
109
99
110
> typeOne= 'Dim ZeroZeroZeroZeroZeroZeroZero
100
111
101
-
</div>
102
-
</details>
112
+
</div>
113
+
</details>
103
114
104
115
Multiplication and division
105
116
---------------------------
@@ -116,7 +127,7 @@ Let's implement multiplication and division on the type-level. After such an ope
116
127
- `Mul` is the name of the function.
117
128
- `d1 :: Dim` is read as "the *type* `d1` has *kind* `Dim`".
118
129
119
-
**Exercise.** As you would suspect, division is very similar, so why don't you try 'n implement it yourself?
130
+
**Exercise** As you would suspect, division is very similar, so why don't you try 'n implement it yourself?
120
131
121
132
<details>
122
133
<summary>**Solution**</summary>
@@ -128,10 +139,10 @@ Let's implement multiplication and division on the type-level. After such an ope
128
139
> 'Dim (le1-le2) (ma1-ma2) (ti1-ti2) (cu1-cu2)
129
140
> (te1-te2) (su1-su2) (lu1-lu2)
130
141
131
-
</div>
132
-
</details>
142
+
</div>
143
+
</details>
133
144
134
-
**Exercise.** Implement a type-level function for raising a dimension to the power of some integer.
145
+
**Exercise** Implement a type-level function for raising a dimension to the power of some integer.
135
146
136
147
<details>
137
148
<summary>**Solution**</summary>
@@ -141,12 +152,12 @@ Let's implement multiplication and division on the type-level. After such an ope
0 commit comments