Skip to content

Commit 9ad0434

Browse files
author
Oskar Lundström
committed
Sista putsande på Quantity! Åtminstone just nu...
1 parent 934c9e0 commit 9ad0434

File tree

4 files changed

+35
-32
lines changed

4 files changed

+35
-32
lines changed

Physics/src/Dimensions/Mole.png

4.07 KB
Loading

Physics/src/Dimensions/Quantity.lhs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Quantities
1717
> ( Quantity
1818
> , length, mass, time, current, temperature, substance, luminosity, one
1919
> , velocity, acceleration, force, momentum
20+
> , meter, kilogram, second, ampere, kelvin, mole, candela, unitless
2021
> , (~=)
2122
> , isZero
2223
> , (#)
@@ -465,8 +466,6 @@ To solve these two problems we'll introduce some syntactic sugar. First some pre
465466

466467
And now the sugar.
467468

468-
TODO: Please multiply the values instead of throwing them away. I'm pretty sure (#) should behave as "scale" of a vector space. So that (x#(y#z)) == ((x*y)#z).
469-
470469
> (#) :: (Num v) => v -> Quantity d v -> Quantity d v
471470
> v # (ValQuantity d bv) = ValQuantity d (v*bv)
472471

@@ -490,6 +489,8 @@ But let's not stop there. It would be prettier if you could actually write `mete
490489

491490
**Exercise** Make it so that one can write the SI-units instead of the base dimensions when one uses the sugar. Then show how to write $4$ seconds.
492491

492+
![](Mole.png "A different kind of mole..."){.float-img-right}
493+
493494
<details>
494495
<summary>**Solution**</summary>
495496
<div>
@@ -501,7 +502,7 @@ But let's not stop there. It would be prettier if you could actually write `mete
501502
> kelvin = temperature
502503
> mole = substance
503504
> candela = luminosity
504-
> unitless =
505+
> unitless = one
505506

506507
> fourSeconds = 4 # second
507508

Physics/src/Dimensions/Quantity/Test.lhs

Lines changed: 23 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
Testing of Quantity
33
===================
44

5+
\ignore{
6+
57
> {-# LANGUAGE DataKinds #-}
68
> {-# LANGUAGE GADTs #-}
79
> {-# LANGUAGE KindSignatures #-}
@@ -11,11 +13,23 @@ Testing of Quantity
1113
> {-# LANGUAGE FlexibleInstances #-}
1214
> {-# LANGUAGE TypeSynonymInstances #-}
1315

16+
}
17+
1418
> module Dimensions.Quantity.Test
1519
> ( runTests
1620
> )
1721
> where
1822

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+
1933
> import Prelude hiding (length, div)
2034
> import Test.QuickCheck
2135

@@ -36,9 +50,9 @@ First we need an `Arbitrary` instance for `Quantity d val`. For `d` we'll mostly
3650
A generator for an arbitrary dimension.
3751

3852
> genQuantity :: Quantity d Double -> Gen (Q d)
39-
> genQuantity sugar = do
53+
> genQuantity quantity = do
4054
> value <- arbitrary
41-
> return (value # sugar)
55+
> return (value # quantity)
4256

4357
And now we make `Arbitrary` instances of arbitrary selected dimensions in the `Quantity`s.
4458

@@ -57,7 +71,7 @@ And now we make `Arbitrary` instances of arbitrary selected dimensions in the `Q
5771
Testing arithmetic properties
5872
-----------------------------
5973

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
6175

6276
- Addition commutative
6377
- Addition associative
@@ -69,20 +83,14 @@ One regular numbers, and hence too on quantites with their dimensions, a bunch o
6983
- Subtraction and addition cancel each other out
7084
- Division and multiplication cancel each other out
7185
- Pythagoran trigonometric identity
72-
- The sugar doesn't care about input value
7386

7487
Let's start!
7588

7689
We could write the type signatures in a general way like
7790

7891
< prop_addCom :: Q d -> Q d -> Bool
7992

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.
8694

8795
Instead we'll pick some arbitrary dimensions that have an `Arbitrary` instance.
8896

@@ -98,7 +106,6 @@ Instead we'll pick some arbitrary dimensions that have an `Arbitrary` instance.
98106
> prop_addId :: Q Time -> Bool
99107
> prop_addId a = zero +# a ~= a
100108
> where
101-
> -- `zero` will, thanks to the versatile suger, have > -- the same dimension as `a`.
102109
> zero = 0 # a
103110

104111
> -- a * b = b * a
@@ -133,33 +140,24 @@ Instead we'll pick some arbitrary dimensions that have an `Arbitrary` instance.
133140
> prop_pythagoranIdentity a = sinq a *# sinq a +#
134141
> cosq a *# cosq a ~= (1 # one)
135142

136-
> prop_sugar :: Double -> Q Length -> Q Length -> Bool
137-
> prop_sugar v a b = v # a ~= v # b
143+
144+
\ignore{
138145

139146
Integrating tests with Stack
140147
----------------------------
141148

142149
> runTests :: IO ()
143150
> runTests = do
144-
> putStrLn "Dimensions quantity: Addition commutative"
145151
> quickCheck prop_addCom
146-
> putStrLn "Dimensions quantity: Addition associative"
147152
> quickCheck prop_addAss
148-
> putStrLn "Dimensions quantity: Zero is identity for addition"
149153
> quickCheck prop_addId
150-
> putStrLn "Dimensions quantity: Multiplication commutative"
151154
> quickCheck prop_mulCom
152-
> putStrLn "Dimensions quantity: Multiplication associative"
153155
> quickCheck prop_mulAss
154-
> putStrLn "Dimensions quantity: One is identity for multiplication"
155156
> quickCheck prop_mulId
156-
> putStrLn "Dimensions quantity: Addition distributes over multiplication"
157157
> quickCheck prop_addDistOverMul
158-
> putStrLn "Dimensions quantity: Subtraction and addition cancel each other out"
159158
> quickCheck prop_addSubCancel
160-
> putStrLn "Dimensions quantity: Division and multiplication cancel each other out"
161159
> quickCheck prop_mulDivCancel
162-
> putStrLn "Dimensions quantity: Pythagoran trigonometric identity"
163160
> quickCheck prop_pythagoranIdentity
164-
> putStrLn "Dimensions quantity: Sugar is correct"
165-
> quickCheck prop_sugar
161+
> putStrLn "Dimensions Quantity tests passed!"
162+
163+
}

Physics/src/Dimensions/Usage.lhs

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,16 +2,22 @@
22
Usage
33
=====
44

5-
In this module we'll show how to use value-level dimensions, type-level dimensions and `Quantity` in an "actual" progam.
5+
\ignore{
66

77
> {-# LANGUAGE TypeOperators #-}
88

9+
}
10+
911
> module Dimensions.Usage
1012
> (
1113
> )
1214
> where
1315

14-
Let's first import the things we have created.
16+
In this module we'll show how to use value-level dimensions, type-level dimensions and `Quantity` in an "actual" progam. Let's first use this fancy GHC-extension
17+
18+
< {-# LANGUAGE TypeOperators #-}
19+
20+
and then import the things we have created.
1521

1622
> import Dimensions.TypeLevel
1723
> import Dimensions.Quantity
@@ -24,8 +30,6 @@ Values and types
2430

2531
Let's create a length, time and mass, in the way hinted in the previous chapter.
2632

27-
TODO: Av okända skäl så blir de nedanstående av typ `Integer` om ej en decimal tas med. Man vill nog ha dom som `Double`. Idealt skulle de ha typ `(Num v) => v` men jag har inte fått till det så bra.
28-
2933
< myLength = 10.0 # length
3034
< myTime = 20.0 # time
3135
< myMass = 30.0 # mass

0 commit comments

Comments
 (0)