git.iko.soy/Idris-dev
on master help sign in
Add some docstrings
f73d721David Raymond Christiansen
libs/base/Control/Isomorphism.idr+28−3
compare with master
unifiedsplit
@@ -4,7 +4,7 @@ import Syntax.PreorderReasoning
4
4
5%default total
5%default total
6
6
7−-- An isomorphism between two types
7+||| An isomorphism between two types
8data Iso : Type -> Type -> Type where
8data Iso : Type -> Type -> Type where
9 MkIso : (to : a -> b) ->
9 MkIso : (to : a -> b) ->
10 (from : b -> a) ->
10 (from : b -> a) ->
@@ -14,9 +14,11 @@ data Iso : Type -> Type -> Type where
14
14
15-- Isomorphism properties
15-- Isomorphism properties
16
16
17+||| Isomorphism is reflexive
17isoRefl : Iso a a
18isoRefl : Iso a a
18isoRefl = MkIso id id (\x => refl) (\x => refl)
19isoRefl = MkIso id id (\x => refl) (\x => refl)
19
20
21+||| Isomorphism is transitive
20isoTrans : Iso a b -> Iso b c -> Iso a c
22isoTrans : Iso a b -> Iso b c -> Iso a c
21isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
23isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
22 MkIso (\x => to' (to x))
24 MkIso (\x => to' (to x))
@@ -28,11 +30,13 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
28 (from (to x)) ={ fromTo x }=
30 (from (to x)) ={ fromTo x }=
29 x QED)
31 x QED)
30
32
33+||| Isomorphism is symmetric
31isoSym : Iso a b -> Iso b a
34isoSym : Iso a b -> Iso b a
32isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
35isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
33
36
34-- Isomorphisms over sums
37-- Isomorphisms over sums
35
38
39+||| Disjunction is commutative
36eitherComm : Iso (Either a b) (Either b a)
40eitherComm : Iso (Either a b) (Either b a)
37eitherComm = MkIso swap swap swapSwap swapSwap
41eitherComm = MkIso swap swap swapSwap swapSwap
38 where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!
42 where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!
@@ -42,6 +46,7 @@ eitherComm = MkIso swap swap swapSwap swapSwap
42 swapSwap (Left x) = refl
46 swapSwap (Left x) = refl
43 swapSwap (Right x) = refl
47 swapSwap (Right x) = refl
44
48
49+||| Disjunction is associative
45eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
50eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
46eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
51eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
47 where eitherAssoc1 : Either (Either a b) c -> Either a (Either b c)
52 where eitherAssoc1 : Either (Either a b) c -> Either a (Either b c)
@@ -64,6 +69,7 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
64 ok2 (Left (Right x)) = refl
69 ok2 (Left (Right x)) = refl
65 ok2 (Right x) = refl
70 ok2 (Right x) = refl
66
71
72+||| Disjunction with false is a no-op
67eitherBotLeft : Iso (Either _|_ a) a
73eitherBotLeft : Iso (Either _|_ a) a
68eitherBotLeft = MkIso to from ok1 ok2
74eitherBotLeft = MkIso to from ok1 ok2
69 where to : Either _|_ a -> a
75 where to : Either _|_ a -> a
@@ -77,10 +83,11 @@ eitherBotLeft = MkIso to from ok1 ok2
77 ok2 (Left x) = FalseElim x
83 ok2 (Left x) = FalseElim x
78 ok2 (Right x) = refl
84 ok2 (Right x) = refl
79
85
86+||| Disjunction with false is a no-op
80eitherBotRight : Iso (Either a _|_) a
87eitherBotRight : Iso (Either a _|_) a
81eitherBotRight = isoTrans eitherComm eitherBotLeft
88eitherBotRight = isoTrans eitherComm eitherBotLeft
82
89
83−
90+||| Isomorphism is a congruence with regards to disjunction
84eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
91eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
85eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
92eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
86 (MkIso to from toFrom fromTo)
93 (MkIso to from toFrom fromTo)
@@ -96,21 +103,25 @@ eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
96 ok2 (Left x) = cong (fromTo x)
103 ok2 (Left x) = cong (fromTo x)
97 ok2 (Right x) = cong (fromTo' x)
104 ok2 (Right x) = cong (fromTo' x)
98
105
106+||| Isomorphism is a congruence with regards to disjunction on the left
99eitherCongLeft : Iso a a' -> Iso (Either a b) (Either a' b)
107eitherCongLeft : Iso a a' -> Iso (Either a b) (Either a' b)
100eitherCongLeft i = eitherCong i isoRefl
108eitherCongLeft i = eitherCong i isoRefl
101
109
110+||| Isomorphism is a congruence with regards to disjunction on the right
102eitherCongRight : Iso b b' -> Iso (Either a b) (Either a b')
111eitherCongRight : Iso b b' -> Iso (Either a b) (Either a b')
103eitherCongRight i = eitherCong isoRefl i
112eitherCongRight i = eitherCong isoRefl i
104
113
105-- Isomorphisms over products
114-- Isomorphisms over products
115+||| Conjunction is commutative
106pairComm : Iso (a, b) (b, a)
116pairComm : Iso (a, b) (b, a)
107pairComm = MkIso swap swap swapSwap swapSwap
117pairComm = MkIso swap swap swapSwap swapSwap
108 where swap : (a', b') -> (b', a')
118 where swap : (a', b') -> (b', a')
109 swap (x, y) = (y, x)
119 swap (x, y) = (y, x)
110−
120+
111 swapSwap : (x : (a', b')) -> swap (swap x) = x
121 swapSwap : (x : (a', b')) -> swap (swap x) = x
112 swapSwap (x, y) = refl
122 swapSwap (x, y) = refl
113
123
124+||| Conjunction is associative
114pairAssoc : Iso (a, (b, c)) ((a, b), c)
125pairAssoc : Iso (a, (b, c)) ((a, b), c)
115pairAssoc = MkIso to from ok1 ok2
126pairAssoc = MkIso to from ok1 ok2
116 where
127 where
@@ -123,20 +134,25 @@ pairAssoc = MkIso to from ok1 ok2
123 ok2 : (x : (a, (b, c))) -> from (to x) = x
134 ok2 : (x : (a, (b, c))) -> from (to x) = x
124 ok2 (x, (y, z)) = refl
135 ok2 (x, (y, z)) = refl
125
136
137+||| Conjunction with truth is a no-op
126pairUnitRight : Iso (a, ()) a
138pairUnitRight : Iso (a, ()) a
127pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok
139pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok
128 where ok : (x : (a, ())) -> (fst x, ()) = x
140 where ok : (x : (a, ())) -> (fst x, ()) = x
129 ok (x, ()) = refl
141 ok (x, ()) = refl
130
142
143+||| Conjunction with truth is a no-op
131pairUnitLeft : Iso ((), a) a
144pairUnitLeft : Iso ((), a) a
132pairUnitLeft = isoTrans pairComm pairUnitRight
145pairUnitLeft = isoTrans pairComm pairUnitRight
133
146
147+||| Conjunction preserves falsehood
134pairBotLeft : Iso (_|_, a) _|_
148pairBotLeft : Iso (_|_, a) _|_
135pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
149pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
136
150
151+||| Conjunction preserves falsehood
137pairBotRight : Iso (a, _|_) _|_
152pairBotRight : Iso (a, _|_) _|_
138pairBotRight = isoTrans pairComm pairBotLeft
153pairBotRight = isoTrans pairComm pairBotLeft
139
154
155+||| Isomorphism is a congruence with regards to conjunction
140pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
156pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
141pairCong {a = a} {a' = a'} {b = b} {b' = b'}
157pairCong {a = a} {a' = a'} {b = b} {b' = b'}
142 (MkIso to from toFrom fromTo)
158 (MkIso to from toFrom fromTo)
@@ -155,13 +171,16 @@ pairCong {a = a} {a' = a'} {b = b} {b' = b'}
155 rewrite fromTo' y in
171 rewrite fromTo' y in
156 refl
172 refl
157
173
174+||| Isomorphism is a congruence with regards to conjunction on the left
158pairCongLeft : Iso a a' -> Iso (a, b) (a', b)
175pairCongLeft : Iso a a' -> Iso (a, b) (a', b)
159pairCongLeft i = pairCong i isoRefl
176pairCongLeft i = pairCong i isoRefl
160
177
178+||| Isomorphism is a congruence with regards to conjunction on the right
161pairCongRight : Iso b b' -> Iso (a, b) (a, b')
179pairCongRight : Iso b b' -> Iso (a, b) (a, b')
162pairCongRight = pairCong isoRefl
180pairCongRight = pairCong isoRefl
163
181
164-- Distributivity of products over sums
182-- Distributivity of products over sums
183+||| Products distribute over sums
165distribLeft : Iso (Either a b, c) (Either (a, c) (b, c))
184distribLeft : Iso (Either a b, c) (Either (a, c) (b, c))
166distribLeft = MkIso to from toFrom fromTo
185distribLeft = MkIso to from toFrom fromTo
167 where to : (Either a b, c) -> Either (a, c) (b, c)
186 where to : (Either a b, c) -> Either (a, c) (b, c)
@@ -177,20 +196,24 @@ distribLeft = MkIso to from toFrom fromTo
177 fromTo (Left x, y) = refl
196 fromTo (Left x, y) = refl
178 fromTo (Right x, y) = refl
197 fromTo (Right x, y) = refl
179
198
199+||| Products distribute over sums
180distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
200distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
181distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
201distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
182
202
183
203
184-- Enable preorder reasoning syntax over isomorphisms
204-- Enable preorder reasoning syntax over isomorphisms
205+||| Used for preorder reasoning syntax. Not intended for direct use.
185qed : (a : Type) -> Iso a a
206qed : (a : Type) -> Iso a a
186qed a = isoRefl
207qed a = isoRefl
187
208
209+||| Used for preorder reasoning syntax. Not intended for direct use.
188step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
210step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
189step a iso1 iso2 = isoTrans iso1 iso2
211step a iso1 iso2 = isoTrans iso1 iso2
190
212
191
213
192
214
193-- Isomorphisms over Maybe
215-- Isomorphisms over Maybe
216+||| Isomorphism is a congruence with respect to Maybe
194maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
217maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
195maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
218maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
196 where ok1 : (y : Maybe b) -> map to (map from y) = y
219 where ok1 : (y : Maybe b) -> map to (map from y) = y
@@ -200,6 +223,7 @@ maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1
200 ok2 Nothing = refl
223 ok2 Nothing = refl
201 ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
224 ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
202
225
226+||| `Maybe a` is the same as `Either a ()`
203maybeEither : Iso (Maybe a) (Either a ())
227maybeEither : Iso (Maybe a) (Either a ())
204maybeEither = MkIso to from iso1 iso2
228maybeEither = MkIso to from iso1 iso2
205 where to : Maybe a -> Either a ()
229 where to : Maybe a -> Either a ()
@@ -215,6 +239,7 @@ maybeEither = MkIso to from iso1 iso2
215 iso2 Nothing = refl
239 iso2 Nothing = refl
216 iso2 (Just x) = refl
240 iso2 (Just x) = refl
217
241
242+||| Maybe of void is just unit
218maybeVoidUnit : Iso (Maybe _|_) ()
243maybeVoidUnit : Iso (Maybe _|_) ()
219maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
244maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
220 (Either _|_ ()) ={ eitherBotLeft }=
245 (Either _|_ ()) ={ eitherBotLeft }=
libs/prelude/IO.idr+10−1
@@ -4,8 +4,10 @@ import Prelude.List
4
4
5%access public
5%access public
6
6
7+||| Idris's primitive IO, for building abstractions on top of
7abstract data PrimIO a = prim__IO a
8abstract data PrimIO a = prim__IO a
8
9
10+||| A token representing the world, for use in `IO`
9abstract data World = TheWorld
11abstract data World = TheWorld
10
12
11abstract WorldRes : Type -> Type
13abstract WorldRes : Type -> Type
@@ -26,7 +28,10 @@ abstract
26prim_io_return : a -> PrimIO a
28prim_io_return : a -> PrimIO a
27prim_io_return x = prim__IO x
29prim_io_return x = prim__IO x
28
30
31+||| Descriptions of the various sorts of Ints that Idris supports
29data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
32data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64 | IT8x16 | IT16x8 | IT32x4 | IT64x2
33+
34+||| Types available for foreign function calls
30data FTy = FIntT IntTy
35data FTy = FIntT IntTy
31 | FFunction FTy FTy
36 | FFunction FTy FTy
32 | FFloat
37 | FFloat
@@ -75,6 +80,7 @@ FBits32x4 = FIntT IT32x4
75FBits64x2 : FTy
80FBits64x2 : FTy
76FBits64x2 = FIntT IT64x2
81FBits64x2 = FIntT IT64x2
77
82
83+||| Interpret an FFI type as the type of the Idris function that it will become
78interpFTy : FTy -> Type
84interpFTy : FTy -> Type
79interpFTy (FIntT ITNative) = Int
85interpFTy (FIntT ITNative) = Int
80interpFTy (FIntT ITChar) = Char
86interpFTy (FIntT ITChar) = Char
@@ -95,7 +101,10 @@ interpFTy FUnit = ()
95
101
96interpFTy (FFunction a b) = interpFTy a -> interpFTy b
102interpFTy (FFunction a b) = interpFTy a -> interpFTy b
97
103
104+||| Type signatures for foreign functions
105+||| @ xs the argument types
106+||| @ t the return type
98−ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
107+ForeignTy : (xs : List FTy) -> (t : FTy) -> Type
99ForeignTy Nil rt = World -> PrimIO (interpFTy rt)
108ForeignTy Nil rt = World -> PrimIO (interpFTy rt)
100ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
109ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
101
110
libs/prelude/Prelude/Either.idr+11−1
@@ -16,10 +16,12 @@ data Either a b =
16-- Syntactic tests
16-- Syntactic tests
17--------------------------------------------------------------------------------
17--------------------------------------------------------------------------------
18
18
19+||| True if the argument is Left, False otherwise
19isLeft : Either a b -> Bool
20isLeft : Either a b -> Bool
20isLeft (Left l) = True
21isLeft (Left l) = True
21isLeft (Right r) = False
22isLeft (Right r) = False
22
23
24+||| True if the argument is Right, False otherwise
23isRight : Either a b -> Bool
25isRight : Either a b -> Bool
24isRight (Left l) = False
26isRight (Left l) = False
25isRight (Right r) = True
27isRight (Right r) = True
@@ -41,6 +43,7 @@ either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c
41either l r (Left x) = l x
43either l r (Left x) = l x
42either l r (Right x) = r x
44either l r (Right x) = r x
43
45
46+||| Keep the payloads of all Left constructors in a list of Eithers
44lefts : List (Either a b) -> List a
47lefts : List (Either a b) -> List a
45lefts [] = []
48lefts [] = []
46lefts (x::xs) =
49lefts (x::xs) =
@@ -48,6 +51,7 @@ lefts (x::xs) =
48 Left l => l :: lefts xs
51 Left l => l :: lefts xs
49 Right r => lefts xs
52 Right r => lefts xs
50
53
54+||| Keep the payloads of all Right constructors in a list of Eithers
51rights : List (Either a b) -> List b
55rights : List (Either a b) -> List b
52rights [] = []
56rights [] = []
53rights (x::xs) =
57rights (x::xs) =
@@ -55,9 +59,11 @@ rights (x::xs) =
55 Left l => rights xs
59 Left l => rights xs
56 Right r => r :: rights xs
60 Right r => r :: rights xs
57
61
62+||| Split a list of Eithers into a list of the left elements and a list of the right elements
58partitionEithers : List (Either a b) -> (List a, List b)
63partitionEithers : List (Either a b) -> (List a, List b)
59partitionEithers l = (lefts l, rights l)
64partitionEithers l = (lefts l, rights l)
60
65
66+||| Remove a "useless" Either by collapsing the case distinction
61fromEither : Either a a -> a
67fromEither : Either a a -> a
62fromEither (Left l) = l
68fromEither (Left l) = l
63fromEither (Right r) = r
69fromEither (Right r) = r
@@ -66,7 +72,9 @@ fromEither (Right r) = r
66-- Conversions
72-- Conversions
67--------------------------------------------------------------------------------
73--------------------------------------------------------------------------------
68
74
75+||| Convert a Maybe to an Either by using a default value in case of Nothing
76+||| @ e the default value
69−maybeToEither : e -> Maybe a -> Either e a
77+maybeToEither : (def : e) -> Maybe a -> Either e a
70maybeToEither def (Just j) = Right j
78maybeToEither def (Just j) = Right j
71maybeToEither def Nothing = Left def
79maybeToEither def Nothing = Left def
72
80
@@ -86,10 +94,12 @@ instance (Eq a, Eq b) => Eq (Either a b) where
86-- Injectivity of constructors
94-- Injectivity of constructors
87--------------------------------------------------------------------------------
95--------------------------------------------------------------------------------
88
96
97+||| Left is injective
89total leftInjective : {b : Type} -> {x : a} -> {y : a}
98total leftInjective : {b : Type} -> {x : a} -> {y : a}
90 -> (Left {b = b} x = Left {b = b} y) -> (x = y)
99 -> (Left {b = b} x = Left {b = b} y) -> (x = y)
91leftInjective refl = refl
100leftInjective refl = refl
92
101
102+||| Right is injective
93total rightInjective : {a : Type} -> {x : b} -> {y : b}
103total rightInjective : {a : Type} -> {x : b} -> {y : b}
94 -> (Right {a = a} x = Right {a = a} y) -> (x = y)
104 -> (Right {a = a} x = Right {a = a} y) -> (x = y)
95rightInjective refl = refl
105rightInjective refl = refl
libs/prelude/Prelude/Monad.idr+4−1
@@ -13,8 +13,11 @@ infixl 5 >>=
13class Applicative m => Monad (m : Type -> Type) where
13class Applicative m => Monad (m : Type -> Type) where
14 (>>=) : m a -> (a -> m b) -> m b
14 (>>=) : m a -> (a -> m b) -> m b
15
15
16+||| Also called `join` or mu
16flatten : Monad m => m (m a) -> m a
17flatten : Monad m => m (m a) -> m a
17flatten a = a >>= id
18flatten a = a >>= id
18
19
20+||| For compatibility with Haskell. Note that monads are **not** free to
21+||| define `return` and `pure` differently!
19return : Monad m => a -> m a
22return : Monad m => a -> m a
20−return = pure
23+return = pure