gdritter repos pico-ml-old / 32d6462
Modified syntax slightly (using `rec` keyword) Getty Ritter 9 years ago
6 changed file(s) with 109 addition(s) and 95 deletion(s). Collapse all Expand all
+1
-0
.gitignore less more
1 *~
+19
-0
stdlib/Category.pml less more
1 exports
2 Category(..)
3 _>>>_
4 _<<<_
5 arrowCategory
6
7 record Category cat
8 .id (cat a a)
9 .compose (cat b c -> cat a b -> cat a c)
10
11 _>>>_ : implicit (Category cat) -> cat a b -> cat b c -> cat a c
12 c = flip c.compose
13
14 _<<<_ : implicit (Category cat) -> cat b c -> cat a b -> cat a c
15 c = c.compose
16
17 implicit arrowCategory : Category _->_ = rec
18 .id = id
19 .compose = compose
+12
-14
stdlib/Collections.pml less more
11 exports
2 ( HasLength(..)
3 , length
4 , null
5 , Sequence(..)
6 , Functor(..)
7 , map
8 )
2 Functor(..)
3 HasLength(..)
4 Sequence(..)
5 length
6 map
7 null
98
10 record HasLength f = { .length (f -> Nat) }
9 record HasLength f = .length (f -> Nat)
1110
1211 length : implicit (HasLength l) -> l -> Nat
13 (implicit l) = l.length
12 l = l.length
1413
1514 null : implicit (HasLength l) -> l -> Bool
16 (implicit l) ls = l.length ls == 0
15 l ls = l.length ls == 0
1716
1817 record Sequence f =
19 { .toList (f a -> List a)
20 , .fromList (List a -> f a)
21 }
18 .toList (f a -> List a)
19 .fromList (List a -> f a)
2220
23 record Functor f = { .map ((a -> b) -> f a -> f b) }
21 record Functor f = .map ((a -> b) -> f a -> f b)
2422
2523 map : implicit (Functor f) -> (a -> b) -> f a -> f b
2624 f = f.map
+25
-22
stdlib/List.pml less more
1 import list
2 import monoid
1 exports
2 listHasLength
3 listSequence
4 listFunctor
5 listMonoid
6 head
7 tail
38
4 implicit listHasLength : HasLength List =
5 { .length
6 Cons _ xs = 1 + length xs
7 Nil = 0
8 }
9 import Monoid
910
10 implicit listSequence : Sequence List =
11 { .toList = id
12 , .fromList = id
13 }
11 implicit listHasLength : HasLength List = rec
12 .length
13 Cons _ xs = 1 + length xs
14 Nil = 0
1415
15 implicit listFunctor : Functor List =
16 { .map
17 f (Cons x xs) = Cons (f x) xs
18 _ Nil = Nil
19 }
16 implicit listSequence : Sequence List = rec
17 .toList = id
18 .fromList = id
2019
21 implicit listMonoid : Monoid List =
22 { .empty = []
23 , .append
24 Nil ys = ys
25 (Cons x xs) ys = Cons x (append xs ys)
26 }
20 implicit listFunctor : Functor List = rec
21 .map
22 f (Cons x xs) = Cons (f x) xs
23 _ Nil = Nil
24
25 implicit listMonoid : Monoid List = rec
26 .empty = []
27 .append
28 Nil ys = ys
29 (Cons x xs) ys = Cons x (append xs ys)
2730
2831 head : List a -> a
2932 x :: _ = x
+37
-39
stdlib/Monoid.pml less more
11 exports
2 ( Monoid(..)
3 , empty
4 , _<>_
5 )
2 Monoid(..)
3 empty
4 _<>_
5 unitMonoid
6 additive
7 multiplicative
8 conjunctive
9 disjunctive
10 dual
11 endo
12 reader
13 pair
614
715 import Num
816
917 -- The Monoid type
1018
11 record Monoid m =
12 { .empty m
13 , .append (m -> m -> m)
14 }
19 record Monoid m
20 .empty m
21 .append (m -> m -> m)
1522
1623 -- implicit sugars for the Monoid operations
1724
2330
2431 -- some Monoid values
2532
26 implicit unitMonoid : Monoid () =
27 { .empty = ()
28 , .append _ _ = ()
29 }
33 implicit unitMonoid : Monoid () = rec
34 .empty = ()
35 .append _ _ = ()
3036
3137 additive : implicit (Add m) -> Monoid m
32 add = { .empty = add.zero
33 , .append = add.plus
34 }
38 add = rec .empty = add.zero
39 .append = add.plus
3540
3641 multiplicative : implicit (Mul m) -> Monoid m
37 mul = { .empty = mul.one
38 , .append = mul.times
39 }
42 mul = rec .empty = mul.one
43 .append = mul.times
4044
41 implicit conjunctive : Monoid Bool =
42 { .empty = False
43 , .append = _&&_
44 }
45 implicit conjunctive : Monoid Bool = rec
46 .empty = False
47 .append = _&&_
4548
46 disjunctive : Monoid Bool =
47 { .empty = True
48 , .append = _||_
49 }
49 disjunctive : Monoid Bool = rec
50 .empty = True
51 .append = _||_
5052
5153 dual : Monoid m -> Monoid m
52 m = { .empty = m.empty
53 , .append x y = m.append y x
54 }
54 m = rec .empty = m.empty
55 .append x y = m.append y x
5556
56 endo : Monoid (a -> a) =
57 { .empty = id
58 , .append x y = compose x y
59 }
57 endo : Monoid (a -> a) = rec
58 .empty = id
59 .append x y = compose x y
6060
6161 reader : implicit (Monoid b) -> Monoid (a -> b)
62 m = { .empty _ = m.empty
63 , .append x f g = m.append (f x) (g x)
64 }
62 m = rec .empty _ = m.empty
63 .append x f g = m.append (f x) (g x)
6564
6665 pair : implicit (Monoid l) -> implicit (Monoid r) -> Monoid (l * r)
67 l r = { .empty = (l.empty, r.empty)
68 , .append (x1, y1) (x2, y2) = (l.append x1 x2, r.append y1 y2)
69 }
66 l r = rec .empty = (l.empty, r.empty)
67 .append (x1, y1) (x2, y2) = (l.append x1 x2, r.append y1 y2)
+15
-20
stdlib/Num.pml less more
11 exports
2 ( Add(..)
3 , Mul(..)
4 , _+_
5 , _*_
6 )
2 Add(..)
3 Mul(..)
4 _+_
5 _*_
76
87 -- mathematical operations
98
10 record IsNumber n = { .fromInteger (Int -> n) }
9 record IsNumber n = .fromInteger (Int -> n)
1110
1211 record Add n =
13 { .zero n
14 , .plus (n -> n -> n)
15 }
12 .zero n
13 .plus (n -> n -> n)
1614
1715 record Mul n =
18 { .one n
19 , .times (n -> n -> n)
20 }
16 .one n
17 .times (n -> n -> n)
2118
2219 record Sub n =
23 { .pSubAdd (Add n)
24 , .sub (n -> n -> n)
25 }
20 .pSubAdd (Add n)
21 .sub (n -> n -> n)
2622
2723 record Div n =
28 { .pDivMul (Mul n)
29 , .div (n -> n -> n)
30 , .mod (n -> n -> n)
31 , .rem (n -> n -> n)
32 }
24 .pDivMul (Mul n)
25 .div (n -> n -> n)
26 .mod (n -> n -> n)
27 .rem (n -> n -> n)
3328
3429 -- some teaspoons for mathematical operations
3530