22317
|
1 |
module Classes where {
|
|
2 |
|
|
3 |
import Nat;
|
|
4 |
import Integer;
|
|
5 |
|
|
6 |
class Semigroup a where {
|
|
7 |
mult :: a -> a -> a;
|
|
8 |
};
|
|
9 |
|
|
10 |
class (Semigroup a) => Monoidl a where {
|
|
11 |
neutral :: a;
|
|
12 |
};
|
|
13 |
|
|
14 |
class (Monoidl a) => Group a where {
|
|
15 |
inverse :: a -> a;
|
|
16 |
};
|
|
17 |
|
|
18 |
inverse_int :: Integer -> Integer;
|
|
19 |
inverse_int i = negate i;
|
|
20 |
|
|
21 |
neutral_int :: Integer;
|
|
22 |
neutral_int = 0;
|
|
23 |
|
|
24 |
mult_int :: Integer -> Integer -> Integer;
|
|
25 |
mult_int i j = i + j;
|
|
26 |
|
|
27 |
instance Semigroup Integer where {
|
|
28 |
mult = mult_int;
|
|
29 |
};
|
|
30 |
|
|
31 |
instance Monoidl Integer where {
|
|
32 |
neutral = neutral_int;
|
|
33 |
};
|
|
34 |
|
|
35 |
instance Group Integer where {
|
|
36 |
inverse = inverse_int;
|
|
37 |
};
|
|
38 |
|
|
39 |
pow_nat :: (Monoidl a) => Nat -> a -> a;
|
|
40 |
pow_nat (Suc n) x = mult x (pow_nat n x);
|
|
41 |
pow_nat Zero_nat x = neutral;
|
|
42 |
|
|
43 |
pow_int :: (Group a) => Integer -> a -> a;
|
|
44 |
pow_int k x =
|
|
45 |
(if 0 <= k then pow_nat (nat k) x
|
|
46 |
else inverse (pow_nat (nat (negate k)) x));
|
|
47 |
|
|
48 |
example :: Integer;
|
|
49 |
example = pow_int 10 (-2);
|
|
50 |
|
|
51 |
}
|