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/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