Skip to content

Commit 697593b

Browse files
viktorcsimmaviktorcsimma
committed
Writing an incomplete interface with postulates
1 parent 803878b commit 697593b

File tree

3 files changed

+205
-1
lines changed

3 files changed

+205
-1
lines changed

‎lib/Haskell/Data/Map.agda

+199
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
1+
-- An incomplete interface of
2+
-- Haskell's Data.Map.
3+
-- See https://hackage.haskell.org/package/containers-0.4.0.0/docs/src/Data-Map.html.
4+
5+
-- We don't actually implement maps;
6+
-- we only postulate an interface
7+
-- and some basic properties.
8+
9+
module Haskell.Data.Map where
10+
11+
open import Agda.Builtin.Unit
12+
open import Agda.Builtin.Bool
13+
open import Agda.Builtin.Nat hiding (_<_)
14+
open import Agda.Builtin.Int
15+
open import Agda.Builtin.List
16+
open import Haskell.Prim.Bool
17+
open import Haskell.Prim.Maybe
18+
open import Haskell.Prim.Monoid
19+
open import Haskell.Prim.Ord
20+
open import Haskell.Prim.Tuple
21+
import Haskell.Prim.String
22+
open import Haskell.Prim using (case_of_; _$_; _≡_; if_then_else_; ⊥; IsTrue; IsFalse)
23+
open import Haskell.Prelude using (error)
24+
25+
variable
26+
k v a b : Set
27+
28+
postulate
29+
Map : (k a : Set) -> Set
30+
31+
iMonoidMap : {k v : Set} {{ordk : Ord k}} -> Monoid (Map k v)
32+
33+
-- Constructs an empty map.
34+
empty : Map k a
35+
36+
-- | /O(1)/. Is the map empty?
37+
--
38+
-- > Data.Map.null (empty) == True
39+
-- > Data.Map.null (singleton 1 'a') == False
40+
null : Map k a -> Bool
41+
@0 emptyIsNull : ∀ {k a : Set} -> IsTrue (null (empty {k} {a}))
42+
43+
-- | /O(1)/. The number of elements in the map.
44+
--
45+
-- > size empty == 0
46+
-- > size (singleton 1 'a') == 1
47+
-- > size (fromList([(1,'a'), (2,'c'), (3,'b')])) == 3
48+
size : Map k a -> Nat -- should we use Nat or Int here?
49+
@0 nullHasSize0 : ∀ (map : Map k a) -> IsTrue (null map) -> size map ≡ 0
50+
51+
-- | /O(log n)/. Lookup the value at a key in the map.
52+
--
53+
-- The function will return the corresponding value as @('Just' value)@,
54+
-- or 'Nothing' if the key isn't in the map.
55+
lookup : {{ordk : Ord k}} -> k -> Map k a -> Maybe a
56+
57+
-- Same, but returns a tuple with the key and the value.
58+
lookupAssoc : {{ordk : Ord k}} -> Map k a -> Maybe (k × a)
59+
60+
-- | /O(log n)/. Is the key a member of the map? See also 'notMember'.
61+
--
62+
-- > member 5 (fromList [(5,'a'), (3,'b')]) == True
63+
-- > member 1 (fromList [(5,'a'), (3,'b')]) == False
64+
member : {{ordk : Ord k}} -> k -> Map k a -> Bool
65+
66+
notMember : {{ordk : Ord k}} -> k -> Map k a -> Bool
67+
notMember key map = not (member key map)
68+
69+
postulate
70+
@0 notMember↔Nothing : {{ordk : Ord k}} -> ∀ (key : k) (map : Map k a)
71+
-> IsFalse (member key map) ↔ lookup key map ≡ Nothing
72+
@0 nullHasNoMembers : {{ordk : Ord k}} -> ∀ (map : Map k a) -> IsTrue (null map)
73+
-> ∀ (key : k) -> IsFalse (member key map)
74+
75+
-- | /O(log n)/. Find the value at a key.
76+
-- Calls 'error' when the element can not be found.
77+
-- Consider using 'lookup' when elements may not be present.
78+
find : {{ordk : Ord k}} (key : k) (map : Map k a) -> @0 IsTrue (member key map)
79+
-> a
80+
@0 findSameAsLookup : {{ordk : Ord k}} (key : k) (map : Map k a) (@0 isMember : IsTrue (member key map))
81+
-> lookup key map ≡ Just (find key map isMember)
82+
83+
-- I think it's easier to write a definition here.
84+
findWithDefault : {{ordk : Ord k}} -> a -> k -> Map k a -> a
85+
findWithDefault def k m = case lookup k m of λ where
86+
Nothing -> def
87+
(Just x) -> x
88+
89+
postulate
90+
singleton : k -> a -> Map k a
91+
@0 singletonHasItsElement : {{ordk : Ord k}} -> ∀ (key : k) (val : a)
92+
-> lookup key (singleton key val) ≡ Just val
93+
94+
{--------------------------------------------------------------------
95+
Insertion
96+
--------------------------------------------------------------------}
97+
-- | /O(log n)/. Insert a new key and value in the map.
98+
-- If the key is already present in the map, the associated value is
99+
-- replaced with the supplied value. 'insert' is equivalent to
100+
-- @'insertWith' 'const'@.
101+
--
102+
-- > insert 5 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'x')]
103+
-- > insert 7 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'a'), (7, 'x')]
104+
-- > insert 5 'x' empty == singleton 5 'x'
105+
insert : {{ordk : Ord k}} -> k -> a -> Map k a -> Map k a
106+
@0 memberAfterInsertion : {{ordk : Ord k}} -> ∀ (key : k) (val : a) (map : Map k a)
107+
-> lookup key (insert key val map) ≡ Just val
108+
@0 sizeIncreasesAfterInsertion : {{ordk : Ord k}} -> ∀ (key : k) (val : a) (map : Map k a)
109+
-> @0 IsFalse (member key map)
110+
-> size (insert key val map) ≡ suc (size map)
111+
@0 sizeRemainsAfterInsertion : {{ordk : Ord k}} -> ∀ (key : k) (val : a) (map : Map k a)
112+
-> @0 IsTrue (member key map)
113+
-> size (insert key val map) ≡ size map
114+
115+
-- | /O(n*log n)/. Build a map from a list of key\/value pairs. See also 'fromAscList'.
116+
-- If the list contains more than one value for the same key, the last value
117+
-- for the key is retained.
118+
fromList : {{ordk : Ord k}} -> List (k × a) -> Map k a
119+
fromList [] = empty
120+
fromList ((key , val) ∷ xs) = insert key val (fromList xs)
121+
122+
postulate
123+
-- | /O(log n)/. Insert with a function, combining key, new value and old value.
124+
-- @'insertWithKey' f key value mp@
125+
-- will insert the pair (key, value) into @mp@ if key does
126+
-- not exist in the map. If the key does exist, the function will
127+
-- insert the pair @(key,f key new_value old_value)@.
128+
-- Note that the key passed to f is the same key passed to 'insertWithKey'.
129+
--
130+
-- > let f key new_value old_value = (show key) ++ ":" ++ new_value ++ "|" ++ old_value
131+
-- > insertWithKey f 5 "xxx" (fromList [(5,"a"), (3,"b")]) == fromList [(3, "b"), (5, "5:xxx|a")]
132+
-- > insertWithKey f 7 "xxx" (fromList [(5,"a"), (3,"b")]) == fromList [(3, "b"), (5, "a"), (7, "xxx")]
133+
-- > insertWithKey f 5 "xxx" empty == singleton 5 "xxx"
134+
135+
insertWithKey : {{ordk : Ord k}} -> (k -> a -> a -> a) -> k -> a -> Map k a -> Map k a
136+
@0 insertWithKeyIfMember : {{ordk : Ord k}}
137+
-> ∀ (f : k -> a -> a -> a) (key : k) (newval : a) (map : Map k a)
138+
-> (@0 isMember : IsTrue (member key map))
139+
-> insertWithKey f key newval map ≡ insert
140+
key
141+
(f key newval (find key map isMember))
142+
map
143+
@0 insertWithKeyIfNotMember : {{ordk : Ord k}}
144+
-> ∀ (f : k -> a -> a -> a) (key : k) (newval : a) (map : Map k a)
145+
-> (@0 isNotMember : IsFalse (member key map))
146+
-> insertWithKey f key newval map ≡ insert key newval map
147+
148+
-- | /O(log n)/. Insert with a function, combining new value and old value.
149+
-- @'insertWith' f key value mp@
150+
-- will insert the pair (key, value) into @mp@ if key does
151+
-- not exist in the map. If the key does exist, the function will
152+
-- insert the pair @(key, f new_value old_value)@.
153+
insertWith : {{ordk : Ord k}} -> (a -> a -> a) -> k -> a -> Map k a -> Map k a
154+
insertWith f key newval map = insertWithKey (λ _ new old -> f new old) key newval map
155+
156+
-- | /O(log n)/. Combines insert operation with old value retrieval.
157+
-- The expression (@'insertLookupWithKey' f k x map@)
158+
-- is a pair where the first element is equal to (@'lookup' k map@)
159+
-- and the second element equal to (@'insertWithKey' f k x map@).
160+
insertLookupWithKey : {{ordk : Ord k}} -> (k -> a -> a -> a) -> k -> a -> Map k a
161+
-> (Maybe a × Map k a)
162+
insertLookupWithKey f key newval map = lookup key map , insertWithKey f key newval map
163+
164+
postulate
165+
{--------------------------------------------------------------------
166+
Deletion
167+
[delete] is the inlined version of [deleteWith (\k x -> Nothing)]
168+
--------------------------------------------------------------------}
169+
-- | /O(log n)/. Delete a key and its value from the map. When the key is not
170+
-- a member of the map, the original map is returned.
171+
delete : {{ordk : Ord k}} -> k -> Map k a -> Map k a
172+
@0 notMemberAfterDeletion : {{ordk : Ord k}} -> ∀ (key : k) (map : Map k a)
173+
-> IsFalse (member key (delete key map))
174+
@0 sizeDecreasesAfterDeletion : {{ordk : Ord k}} -> ∀ (key : k) (map : Map k a)
175+
-> @0 IsTrue (member key map)
176+
-> size map ≡ suc (size (delete key map))
177+
{- This follows from the next one.
178+
@0 sizeRemainsAfterDeletion : {{ordk : Ord k}} -> ∀ (key : k) (map : Map k a)
179+
-> @0 IsFalse (member key map)
180+
-> size map ≡ size (delete key map)
181+
-}
182+
@0 deletingWhatThereIsNot : {{ordk : Ord k}} -> ∀ (key : k) (map : Map k a)
183+
-> @0 IsFalse (member key map)
184+
-> map ≡ delete key map
185+
186+
@0 insertAndDelete : {{ordk : Ord k}} -> ∀ (key : k) (val : a) (map : Map k a)
187+
-> @0 IsFalse (member key map)
188+
-> delete key (insert key val map) ≡ map
189+
@0 deleteAndInsert : {{ordk : Ord k}} -> ∀ (key : k) (map : Map k a)
190+
-> (@0 isMember : IsTrue (member key map))
191+
-> insert key (find key map isMember) (delete key map)
192+
≡ map
193+
194+
@0 insertNotChangingOthers : {{ordk : Ord k}} -> ∀ (key1 key2 : k) (val : a) (map : Map k a)
195+
-> lookup key1 (insert key2 val map) ≡ lookup key1 map
196+
@0 deleteNotChangingOthers : {{ordk : Ord k}} -> ∀ (key1 key2 : k) (map : Map k a)
197+
-> lookup key1 (delete key2 map) ≡ lookup key1 map
198+
199+
-- Done until delete.

‎lib/Haskell/Prim.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ data ⊥ : Set where
9999
magic : {A : Set} → ⊥ → A
100100
magic ()
101101

102-
--principle of explosion
102+
-- principle of explosion
103103
exFalso : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥
104104
exFalso {False} () b
105105
exFalso {True} a ()

‎lib/Haskell/Prim/Tuple.agda

+5
Original file line numberDiff line numberDiff line change
@@ -43,3 +43,8 @@ snd₃ (_ , y , _) = y
4343

4444
thd₃ : (a × b × c) → c
4545
thd₃ (_ , _ , z) = z
46+
47+
-- logical equivalence for proofs
48+
infix 3 _↔_
49+
_↔_ : (A : Set) (B : Set) -> Set
50+
A ↔ B = (A → B) × (B → A)

0 commit comments

Comments
 (0)