-
Notifications
You must be signed in to change notification settings - Fork 0
/
lists.tex
1137 lines (958 loc) · 50.6 KB
/
lists.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
%!TEX root = reference.tex
\chapter{Sequences and Collections}
\label{lists}
\label{listExpressions}
\index{list expression}
\index{expressions!list}
There are many primary contracts that together relate to collections and sequences:
\begin{description}
\item[\q{concatenate}] defines what it means to concatenate two collections.
\item[\q{explosion}] defines the twin functions of explode and implode. Typically used to inspect and pack scalar entities.
\item[\q{foldable}] is a contract that defines the classic `fold' functions of leftFold, rightFold, leftFold1 and rightFold1.
\item[\q{indexable} and \q{sliceable}] are functions that define random access within a collection.
\item[\q{iterable} and \q{indexed\_iterable}] define processing a collection with a client function -- used for iterations and queries.
\item[\q{reversible}] defines the \q{reverse} function.
\item[\q{sequence}] is a core set of patterns and functions that defines what it means to process and/or build a collection sequentially.
\item[\q{sets}] define the set-oriented functions of intersection, union and complement.
\item[\q{sizeable}] is a pair of functions that define the size of a collection and whether the collection is empty or not.
\item[\q{sorting}] defines the sort function.
\item[\q{updateable}] is a set of functions that define the updating of collections by adding to a collection, merging collections, updating based on patterns and so on.
\end{description}
Many of these contracts are associated with special syntactic forms.
\begin{aside}
The term `collection' is used informally here. Not all types need implement all the contracts defined here. However, for a type to be considered a collection, it should implement all four contracts.
\end{aside}
In addition to the standard collection contracts, there are several standard types, \q{list} and \q{cons} that represent basic forms of sequence.
\section{Sequence Notation}
\label{sequenceNotation}
The \q{sequence} contract has additional syntactic support in the form of specific sequence notation for expressions (see Section~\vref{sequenceExpression}) and patterns (see Section~\vref{sequencePattern}).
An expression of the form:
\begin{lstlisting}[escapechar=|]
[E|\sub1\sequence{,}|E|\subn|]
\end{lstlisting}
is equivalent to the expression:
\begin{lstlisting}[escapechar=|]
_cons(E|\sub1|,|\sequence{}|_cons(E|\subn|,_nil())|\sequence{}|)
\end{lstlisting}
Similarly, the pattern:
\begin{lstlisting}[escapechar=|]
[P|\sub1\sequence{,}|P|\subn|]
\end{lstlisting}is equivalent to the expanded pattern:
\begin{lstlisting}[escapechar=|]
_pair(P|\sub1,\sequence{}|_pair(P|\subn|,_empty())|\sequence{}|)
\end{lstlisting}
This notation makes literals involving the \q{sequence} contract easier to write.
\subsection{The \q{sequence} Contract}
\label{sequenceContract}
\index{sequence contract@\q{sequence} contract}
The \q{sequence} contract defines the equivalent of an abstract type that is `about' sequences. It is defined in Program~\vref{sequenceContractDef}. The elements of the \q{sequence} contract are sufficient to allow abstract sequential processing of sequences.
\begin{program}[hbtp]
\begin{lstlisting}
contract sequence over s determines e is {
_empty has type ()<=s;
_pair has type (e,s)<=s;
_cons has type (e,s)=>s;
_apnd has type (s,e)=>s;
_back has type (s,e)<=s;
_nil has type ()=>s;
}
\end{lstlisting}
\caption{The Standard \q{sequence} Contract}\label{sequenceContractDef}
\end{program}
\noindent
For example, the \q{reverse} function in Program~\vref{reverseProgram} is defined for any form of sequence; i.e., for any type that implements the \q{sequence} contract.
\begin{program}[hbtp]
\begin{lstlisting}
reverse has type for all e,t such that (t)=>t where
sequence over t determines e
fun reverse(S) is let{
fun rev(_empty(),R) is R
| rev(_pair(H,T),R) is rev(T,_cons(H,R))
} in rev(S,_nil());
\end{lstlisting}
\caption{A \q{sequence} Reversal Function}\label{reverseProgram}
\end{program}
\begin{aside}
The \q{sequence} contract has a \emph{functional dependency} -- see Section~\vref{ContractFunctionalDependency}. This captures the intuition that sequences are about an element type; but the actual type of each element depends on the particular implementation of the \q{sequence}.
\end{aside}
\subsection{\q{\_empty} -- Empty Sequence Pattern}
\label{emptyPattern}
\index{sequence contract@\q{sequence} contract!empty@\q{empty}}
\begin{lstlisting}
_empty has type for all e,t such that ()<=t
where sequence over t determines e
\end{lstlisting}
The \q{\_empty} pattern is satisfied when matching an empty sequence.
\begin{aside}
The use of pattern abstractions is a normal feature of contracts that are aimed at defining an abstract type.
\end{aside}
\subsection{\q{\_pair} -- Non-Empty Sequence Pattern}
\label{nonEmptyPattern}
\index{sequence contract@\q{sequence} contract!pair@\q{pair}}
\begin{lstlisting}
_pair has type type for all e,t such that (e,t)<=t
where sequence over t determines e
\end{lstlisting}
The \q{\_pair} pattern is satisfied when matching an non-empty sequence. A successful match results in the head and tail part of the sequence also being match.
\subsection{\q{\_cons} -- Add to Front of Sequence}
\label{consFunction}
\index{sequence contract@\q{sequence} contract!cons@\q{cons}}
\begin{lstlisting}
_cons has type type for all e,t such that (e,t)=>t
where sequence over t determines e
\end{lstlisting}
The \q{\_cons} function is used to `cons' an element to the front of a \q{sequence} -- returning a new sequence with the new element at the front.
\subsection{\q{\_apnd} -- Add to End of Sequence}
\label{appendFunction}
\index{sequence contract@\q{sequence} contract!apnd@\q{apnd}}
\begin{lstlisting}
_apnd has type type for all e,t such that (t,e)=>t
where sequence over t determines e
\end{lstlisting}
The \q{\_apnd} function is used to append an element to the end of a \q{sequence}. I.e., a subsequent match against the \q{sequence} using the \q{\_pair} pattern will 'pick up' the newly appended element only after all existing elements have been removed.
\begin{aside}
Depending on the implementation type that backs a particular \q{sequence}, the performance of the \q{\_cons} and \q{\_apnd} functions may be radically different.
\end{aside}
\subsection{\q{\_back} -- Non-Empty Sequence Pattern}
\label{backPattern}
\index{sequence contract@\q{sequence} contract!back@\q{back}}
\begin{lstlisting}
_back has type type for all e,t such that (t,e)<=t
where sequence over t determines e
\end{lstlisting}
Like the \q{\_pair} pattern, the \q{\_back} pattern is satisfied when matching an non-empty sequence. A successful match results in the last element of the sequence being matched -- as well as the front portion of the sequence.
\begin{aside}
Depending on the implementation type that backs a particular \q{sequence}, the performance of the \q{\_pair} and \q{\_back} patterns may be radically different.
\end{aside}
\subsection{\q{\_nil} -- Construct Empty Sequence}
\label{newFunction}
\index{sequence contract@\q{sequence} contract!cons@\q{cons}}
\begin{lstlisting}
_nil has type type for all e,t such that ()=>t
where sequence over t determines e
\end{lstlisting}
The \q{\_nil} function is used to construct an empty instance of the sequence.
\section{Collection Notation}
Like the sequence notation, the collection notation is intended to allow collections that are not known to be sequences to be represented concisely in a type-independent way.
\section{The \q{concatenate} Contract}
\label{concatenateContract}
\index{concatenate contract@\q{concatenate} contract}
The \q{concatenate} contract defines a single function that implements the `concatenation' of two values together.
\begin{program}[H]
\begin{lstlisting}
contract concatenate over s is {
(++) has type (s,s)=>s;
}
\end{lstlisting}
\caption{The Standard \q{concatenate} Contract}\label{concatenateContractDef}
\end{program}
\noindent
\subsection{\q{++} -- Concatenate Sequences}
\label{concatFunction}
\index{concatenate contract@\q{concatenate} contract!++@\q{++}}
\index{concatenate sequences}
\begin{lstlisting}
(++) has type for all s such that (s,s)=>s where concatenate over s
\end{lstlisting}
The meaning of \q{S++T} is a new sequence where the elements of \q{S} come `first' and the elements of \q{T} come `next'.
\section{The \q{reversible} Contract}
\label{reversibleContract}
\index{reversible contract@\q{reversible} contract}
The \q{reversible} contract defines a single function that implements the `reverse' of function.
\begin{program}[H]
\begin{lstlisting}
contract reversible over s is {
reverse has type (s)=>s;
}
\end{lstlisting}
\caption{The Standard \q{reversible} Contract}\label{reversibleContractDef}
\end{program}
\noindent
\subsection{\q{reverse} -- Reverse Sequences}
\label{reverseFunction}
\index{reversible contract@\q{reversible} contract!reverse\q{reverse}}
\index{reverse sequences}
\begin{lstlisting}
reverse has type for all s such that (s)=>s where reversible over s
\end{lstlisting}
The meaning of \q{reverse(S)} is a new sequence where the elements of \q{S} are reversed.
\begin{aside}
The \q{reversible} contract is implemented for \q{list}s, \q{cons} lists and \q{string}s.
\end{aside}
\section{The \q{sets} Contract}
\label{setsContract}
The standard \q{sets} contract defines set operations over collections.
\index{sets contract@\q{sets} contract}
\begin{program}[hbtp]
\begin{lstlisting}
contract sets over s is {
union has type (s,s)=>s;
intersect has type (s,s)=>s;
complement has type (s,s)=>s;
}
\end{lstlisting}
\caption{The Standard \q{sets} Contract}\label{setContractDef}
\end{program}
\noindent
\subsection{\q{union} -- Union}
\label{unionFunction}
\index{sets contract@\q{sets} contract!union@\q{union}}
\index{union sequences}
\begin{lstlisting}
union has type for all s such that (s,s)=>s where sets over s
\end{lstlisting}
The meaning of \q{union(S,T)} is a new sequence consisting of elements of \q{S} merged with elements of \q{T}. Duplicate elements -- elements that appear in both \q{S} and \q{T} will not be duplicated in the result.
\begin{aside}
Although duplicates are eliminated as noted, if either of \q{S} or \q{T} already contains duplicates, then there may be duplicates in the result.
\end{aside}
\begin{aside}
There is no guarantee that the order of elements in the result reflects the order of elements in either of the sources of the \q{union} -- unless the type implementing the \q{sets} contract is already ordered.
\end{aside}
\subsection{\q{intersect} -- Intersection}
\label{intersectFunction}
\index{sets contract@\q{sets} contract!intersect@\q{intersect}}
\index{intersect sequences}
\begin{lstlisting}
intersect has type for all s such that (s,s)=>s where sets over s
\end{lstlisting}
The meaning of \q{intersect(S,T)} is a new sequence consisting of elements of \q{S} intersected with elements of \q{T}. Only elements that appear in both \q{S} and \q{T} will appear in the result.
\begin{aside}
There is no guarantee as to the order of elements in the result of \q{intersect}.
\end{aside}
\subsection{\q{complement} -- Complement}
\label{complementFunction}
\index{sets contract@\q{sets} contract!complement@\q{complement}}
\index{complement sequences}
\begin{lstlisting}
complement has type for all s such that (s,s)=>s where sets over s
\end{lstlisting}
The meaning of \q{complement(S,T)} is a new sequence consisting of elements of \q{S} which \emph{do not} occur within \q{T}.
\begin{aside}
There is no guarantee as to the order of elements in the result of \q{complement}.
\end{aside}
\section{The \q{sorting} Contract}
\label{sortingContract}
The \q{sorting} contract defines what it means to `sort' a collection. The contract itself is defined in Program~\vref{sortContractProg}.
\begin{program}[H]
\begin{lstlisting}
contract sorting over coll determines el is {
sort has type
(coll,(el,el)=>boolean) => coll;
}
\end{lstlisting}
\caption{The \q{sorting} Contract\label{sortContractProg}}
\end{program}
\subsection{\q{sort} -- Sort a Collection}
\label{sortFunction}
\index{sorting contract@\q{sorting} contract!sort\q{sort}}
\index{sort a collection}
\begin{lstlisting}
sort has type for all el, coll such that
(coll,(el,el)=>boolean) => coll where
sorting over coll determines el
\end{lstlisting}
The \q{sort} function sorts a function -- using a supplied comparator function to compare elements. The comparator function should return true if the second argument is greater than or equal to the first.
\begin{aside}
The actual sort algorithm used is not represented here.
\end{aside}
The \q{sorting} contract is implemented for the \q{list} type and the \q{cons} list type.
\section{The \q{sizeable} Contract}
\label{sizeableContract}
The standard \q{sizeable} contract is defined for those collections that have a concept of size associated with them.
\index{type!contracts! sizeable@\q{sizeable}}
\index{sizeable contract@\q{sizeable} contract}
The \q{sizeable} contract -- which is defined in Program~\vref{sizeableContractProg} -- defines the functions \q{size} and \q{isEmpty}.
\begin{program}
\begin{lstlisting}
contract sizeable of t is {
size has type (t) => integer;
isEmpty has type (t) => boolean;
}
\end{lstlisting}
\caption{The Standard \q{sizeable} Contract\label{sizeableContractProg}}
\end{program}
\subsection{\q{size} -- Size of a \q{sizeable} Collection}
\label{sizeFunction}
\index{sizeable contract@\q{sizeable} contract!size@\q{size}}
\begin{lstlisting}
size has type for all t such that (t)=>integer where sizeable over t
\end{lstlisting}
The \q{size} function returns the number of elements of a \q{sizeable} collection. The precise meaning of the \q{size} function is likely to be type-specific; for example, for \q{string}s, the \q{size} of a \q{string} is the number of characters in the string.
\subsection{\q{isEmpty} -- Is a \q{sizeable} Collection Empty}
\label{isEmptyFunction}
\index{sizeable contract@\q{sizeable} contract!isEmpty@\q{isEmpty}}
\begin{lstlisting}
isEmpty has type for all t such that (t)=>boolean where sizeable over t
\end{lstlisting}
The \q{isEmpty} function returns \q{true} if the collection has no elements.
\section{The \q{indexable} Contract}
\label{indexableContract}
The \q{indexable} contract defines the functions that relate to the `indexable' expressions.
\begin{program}
\begin{lstlisting}
contract indexable over s determines (k,v) is {
_index has type (s,k)=>option of v;
_set_indexed has type (s,k,v)=>s;
_delete_indexed has type (s,k)=>s;
}
\end{lstlisting}
\caption{The Standard \q{indexable} Contract}\label{indexableContractDef}
\end{program}
The \q{indexable} contract defines what it means to access an element of a collection by index, and how such collections may be updated. The contract is parameterized both over the collection type and the index type -- a fact made use of to allow \q{dictionary} values to also be indexed.
\begin{aside}
Note that special notation supports high-level access to the \q{indexable} and \q{sliceable} contracts, as can be seen in Section~\vref{indexNotation} and Section~\vref{sequenceUpdate}.
\end{aside}
\subsection{\q{\_index} -- Index Element}
\label{indexFunction}
\index{indexable contract@\q{indexable} contract!_index@\q{\_index}}
\begin{lstlisting}
_index has type for all s,k,v such that (s,k)=>option of v
where indexable over s determines (k,v)
\end{lstlisting}
\begin{aside}
The type of the index depends on the implementation of the contract. In the case of \q{list}s, the index is \q{integer}; and the first index is zero.
\end{aside}
\begin{aside}
If the index is not valid, for example if the index into a list is longer than the list, then \q{none} is returned.
\end{aside}
\subsection{\q{\_set\_indexed} -- Replace Element}
\label{indexReplaceFunction}
\index{indexable contract@\q{indexable} contract!_set_indexed@\q{\_set\_indexed}}
\index{replace element in collection}
\begin{lstlisting}
_set_indexed has type for all s,k,v such that (s,k,v)=>s
where indexable over s determines (k,v)
\end{lstlisting}
The \q{\_set\_indexed} function is used to represent the result of replacing an indexed element of a collection with a new value. The value returned is a new collection with every element identical to the original except that the ix\super{th} element is replaced.
If the index is out of range, i.e., if there is no element in the collection that corresponds to the requested index, then an error exception will be raised.
\subsection{\q{\_delete\_indexed} -- Remove Element}
\label{indexDeleteFunction}
\index{indexable contract@\q{indexable} contract!_delete_indexed@\q{\_delete\_indexed}}
\index{remove element from collection}
\begin{alltt}
_delete_indexed has type for all s,k,v such that (s,k)=>s
where indexable over s determines (k,v)
\end{alltt}
The \q{\_delete\_indexed} function is used to remove an element from a collection. The \q{\_delete\_indexed} function returns a collection with the identified element removed. The element to delete is identified by its key, not by the kay/value pair.
\begin{aside}
If the index is out of range, i.e., if there is no element in the collection that corresponds to the requested index, then an error exception may be raised -- depending on the implementation of the contract.
\end{aside}
\section{The \q{sliceable} Contract}
\label{sliceableContract}
The \q{sliceable} contract defines what it means to extract and update sub-sequences of collections. The contract -- defined in Program~\vref{sliceableContractProg} -- contains functions that extract a subsequence and replace a subsequence.
\begin{program}[htb]
\begin{lstlisting}
contract sliceable over t is {
_slice has type (t,integer,integer)=>t;
_splice has type (t,integer,integer,t)=>t;
}
\end{lstlisting}
\caption{The \q{sliceable} Contract\label{sliceableContractProg}}
\end{program}
As detailed below, the \q{sliceable} contract is supported by a `slice' notation that is based on the square bracket notation used to support indexing elements of collections.
\subsection{\q{\_slice} -- Extract Subsequence}
\label{sliceFunction}
\index{sliceable contract@\q{sliceable} contract!_slice@\q{\_slice}}
\index{extract subsequence of sequence}
\begin{lstlisting}
_slice has type for all t such that (t,integer,integer)=>t
where sliceable over t
\end{lstlisting}
The meaning of \q{\_slice(S,Fr,To)} is that a subset of the sequence in \q{S} is extracted, starting with index position \q{Fr} up to -- but not including -- the index position \q{To}. The first index of the sequence is assumed to be zero.
If \q{To} is smaller than the length of the sequence then then the result will be shortened accordingly.
The \q{\_slice} function has a special syntax which is similar to that used for list indexing:
\begin{lstlisting}
C[Fr:To]
\end{lstlisting}
is equivalent to the expression
\begin{lstlisting}
_slice(C,Fr,To)
\end{lstlisting}
\begin{aside}
The contract signature, and the type signature for \q{\_slice} do not mention the type of the elements of the sequence.
\end{aside}
\begin{aside}
For any sequence \q{S}, for any positive integers \q{F} $\ge0$ and \q{T}$\ge$\q{F}, the following identity is expected to hold for implementations of \q{\_slice}:
\begin{lstlisting}
S[F:T]++S[T:size(S)] = S
\end{lstlisting}
Note, in particular if \q{F} is greater than or equal to the \q{size} of the sequence then the result of \q{\_slice} will be an empty sequence. This is different to the behavior for \q{\_index} where an exception is \q{raise}d when the index is not present in the sequence.
\end{aside}
\begin{aside}
In addition to being implemented for \q{list}s, and \q{cons} lists, the \q{sliceable} contract is also implemented for \q{string}s. In the latter case, the \q{sliceable} contract defines the equivalent of sub-string and string-replace.
\end{aside}
\subsection{\q{\_splice} -- Replace Subsequence}
\label{spliceFunction}
\index{sliceable contract@\q{sliceable} contract!_splice@\q{\_splice}}
\index{replace subsequence of sequence}
\begin{lstlisting}
_splice has type for all t such that (t,integer,integer,t)=>t
where sliceable over t
\end{lstlisting}
The meaning of \q{\_splice(S,Fr,To,R)} is that a subsequence of \q{S} is replace with \q{R}. Starting with index position \q{Fr}, the elements up until -- but not including -- the position \q{To} are replaced by \q{R}. The first index of the sequence is assumed to be zero.
If \q{To} is greater than or equal to the \q{size} of the sequence then the result will be to replace the remaining of the sequence with the new elements.
The \q{\_splice} function has a special syntax which is similar to that used for updating list elements:
\begin{lstlisting}
C[Fr:To] := S
\end{lstlisting}
is equivalent to the action
\begin{lstlisting}
C := _splice(C,Fr,To,S)
\end{lstlisting}
\section{The \q{iterable} Contract}
\label{iterableContract}
The \q{iterable} contract defines what it means to `iterate' over a collection. The contract itself is defined in Program~\vref{iterateContractProg} and it makes use of the standard \q{IterState} type.
\begin{program}[H]
\begin{lstlisting}
contract iterable over coll determines el is {
_iterate has type
for all r such that
(coll,(el,IterState of r)=>IterState of r,IterState of r) =>
IterState of r;
}
type IterState of t is NoneFound or NoMore(t) or ContinueWith(t);
\end{lstlisting}
\caption{The \q{iterable} Contract\label{iterateContractProg}}
\end{program}
The \q{iterable} contract defines a single function -- \q{\_iterate} -- which is used to `iterate' over a collection applying a client function to each element of the collection.
\subsection{\q{\_iterate} -- Iterate over collection}
\label{iterateFunction}
\index{iterable contract@\q{iterable} contract!\_iterate@\q{\_iterate}}
\index{iterate over collection}
\begin{lstlisting}
_iterate has type
for all coll, el, r such that
(coll,(el,IterState of r)=>IterState of r,IterState of r) =>
IterState of r
where iterable over coll determines el
\end{lstlisting}
The \q{\_iterate} function traverses a collection -- in an order that is `natural' to teh type of the collection -- applying a `client function' to each element.
The client function has the type:
\begin{lstlisting}
(el,IterState of r)=>IterState of r
\end{lstlisting}
where \q{El} is an element of the collection and \q{State} and \q{NewState} represent the `state' of the iteration and are of the type \q{IterState}.
\begin{aside}
The idea is that the client function `processes' the candidate in the context of previous invocations of the client function and returns a new state that reflects the result.
\end{aside}
\begin{description}
\item[\q{NoneFound}] The \q{NoneFound} enumerated symbol denotes an empty state. The client may return a \q{NoneFound} result if the state represents a null situation.
\begin{aside}
The \q{\_iterate} function should not interpret \q{NoneFound} as a signal to terminate the iteration.
\end{aside}
\item[\q{ContinueWith}]
The \q{ContinueWith} constructor is used to denote a partially completed state. The client function returns a \q{ContinueWith} when the denoted state may be augmented by further processing of elements of the collection.
\item[\q{NoMore}]
The \q{NoMore} constructor is used to denote a completed state. The client function returns a \q{NoMore} value when it intends to signal that no further processing of the collection by the \q{\_iterate} function should be performed.
The \q{\_iterate} function should terminate processing the collection if the client function returns an \q{NoMore} value.
\end{description}
For example, to find positive integer values in a collection this client function could be used:
\begin{lstlisting}
fun findPositive(X, ContinueWith(L)) where X>=0 is
ContinueWith(cons(X,L))
| findPositive(_,S) default is S;
\end{lstlisting}
\begin{aside}
The \q{\_iterate} function is used automatically for \ntRef{SearchCondition}s; however, the programmer is also free to explicitly use the \q{\_iterate} function.
\end{aside}
\begin{aside}
The precise form of the declaration of \q{\_iterate} within the \q{iterable} contract bears some additional explanation -- since it takes the form of an explicitly quantified type.
The \q{\_iterate} function is somewhat independent of the nature of the client function -- it applies the client function and terminates when the client function indicates that it is `done'. However, the precise state information that the client function is collecting is not relevant to the \q{\_iterate} function. In effect, the \q{\_iterate} function needs its client function to be generic.
In addition, since the semantics of the \q{\_iterate} function does not depend on the generic state that the client function collects it would not be correct to incorporate \q{r} as an additional type argument to the contract itself.
Hence the formulation of \q{\_iterate} as an explicitly universally quantified function \emph{within} the contract.
\end{aside}
\section{The \q{indexed\_iterable} Contract}
\label{indexedIterableContract}
The \q{indexed\_iterable} contract defines what it means to `iterate' over a sequence where elements have a location within the sequence. The contract itself is defined in Program~\vref{indexedIterateContractProg} and it also makes use of the standard \q{IterState} type seen in Program~\vref{iterateContractProg}.
\begin{program}[H]
\begin{lstlisting}
contract indexed_iterable over s determines (k,v) is {
_ixiterate has type
for all r such that
(s,(k,v,IterState of r)=>IterState of r,IterState of r) =>
IterState of r;
}
\end{lstlisting}
\caption{The \q{indexed\_iterable} Contract\label{indexedIterateContractProg}}
\end{program}
The \q{indexed\_iterable} contract defines a single function -- \q{\_ixiterate} -- which is used to `iterate' over a sequence applying a client function to each element of the collection whilst keeping track of the index of the element within the collection that is being processed.
\subsection{\q{\_ixiterate} -- Iterate over collection}
\label{indexIterateFunction}
\index{indexed\_iterable contract@\q{indexed\_iterable} contract!\_ixiterate@\q{\_ixiterate}}
\index{iterate over collection}
\begin{lstlisting}
_ixiterate has type
for all coll,k,v,r such that
(coll,(k,v,IterState of r)=>IterState of r,IterState of r) =>
IterState of r
where indexed\_iterable over coll determines (k,v)
\end{lstlisting}
The \q{\_ixiterate} function traverses a collection -- in an order that is `natural' to the type of the collection -- applying a `client function' to each element. As it traverses the collection \q{\_ixiterate} keeps track of the index of the element within the collection.
The client function takes the form:
\begin{lstlisting}
fun client(Ix,El,State) is NewState
\end{lstlisting}
where \q{Ix} is a value that denotes the `position' of the element within the collection, \q{El} is an element of the collection and \q{State} and \q{NewState} represent the `state' of the iteration and are of the type \q{IterState}.
The interpretation of the \q{State} is the same as for the \q{iterable} contract.
For example, to find the location within a \q{cons} list of an element that is greater than zero we can use the client function:
\begin{lstlisting}
fun indexOfPositive(Ix,X, ContinueWith(L)) where X>=0 is
ContinueWith(cons(Ix,L))
| indexOfPositive(_,_,S) default is S;
\end{lstlisting}
\begin{aside}
The \q{\_ixiterate} function is used automatically in \ntRef{IndexedSearch} conditions; however, the programmer is also free to explicitly use the \q{indexed\_iterable} contract.
\end{aside}
\section{The \q{mappable} Contract}
\label{mappableContract}
The \q{mappable} contract defines what it means to be able to apply a function over a collection. It contains a single \q{map} function:
\begin{program}[H]
\begin{lstlisting}
contract mappable over c is {
map has type for all e,f such that ((e)=>f,c of e) => c of f;
}
\end{lstlisting}
\caption{The \q{mappable} Contract\label{mapContractProg}}
\end{program}
\subsection{\q{map} -- Apply a transformation to a collection}
\label{mapFunction}
The \q{map} function applies a function to a collection to produce a new collection. Its type is given by:
\begin{lstlisting}
map has type for all e,f such that ((e)=>f,c of e) => c of f where
mappable over c
\end{lstlisting}
For example, we can use \q{map} to construct a list of \q{string} representations of \q{integer} values by mapping \q{display} (see \vref{displayFunction}):
\begin{lstlisting}
map(list of [1,2,3,4],display)
\end{lstlisting}
the value of which is the \q{list}:
\begin{lstlisting}
list of ["1","2","3","4"]
\end{lstlisting}
Note the slightly unusual quantification over the collection type. The \q{map} function must be able to accept a generic function as its transformation function.
\section{The \q{filterable} Contract}
\label{filterableContract}
The \q{filterable} contract contains a single function -- \q{filter} -- that can be used to filter elements from a collection.
\begin{program}[H]
\begin{lstlisting}
contract filterable over t determines e is {
filter has type ((e)=>boolean,t) => t
}
\end{lstlisting}
\caption{The \q{filterable} Contract\label{filterContractProg}}
\end{program}
\subsection{\q{filter} -- Apply a predicate to a collection}
\label{filterFunction}
The \q{filter} function applies a predicate to a collection to produce a new collection -- containing only elements that satisfy the predicate. Its type is given by:
\begin{lstlisting}
filter has type for all e,t such that ((e)=>boolean,t) => t where
filterable over t determines e
\end{lstlisting}
For example, we can use \q{filter} to eliminate odd numbers from a list of \q{integer}s:
\begin{lstlisting}
filter(list of [1,2,3,4,5,6],(X)=>X%2=0)
\end{lstlisting}
which has value:
\begin{lstlisting}
list of [2,4,6]
\end{lstlisting}
\section{The \q{foldable} Contract}
\label{foldableContract}
The \q{foldable} contract defines another variant of iterating over collections while aggregating. The \q{foldable} contract defines two functions: \q{leftFold} and \q{rightFold}.
\begin{program}[H]
\begin{lstlisting}
contract foldable over c determines e is {
leftFold has type for all st such that ((st,e)=>st,st,c)=>st;
leftFold1 has type ((e,e)=>e,c) => e;
rightFold has type for all st such that ((e,st)=>st,st,c)=>st;
rightFold1 has type ((e,e)=>e,c)=>e;
}
\end{lstlisting}
\caption{The \q{foldable} Contract\label{foldableContractProg}}
\end{program}
For example, to add together a collection of \q{integer}s, one can use a \q{leftFold} (or equivalently a \q{rightFold}) expression:
\begin{lstlisting}
leftFold((+),0,list of [1, 2, 3, 4])
\end{lstlisting}
which has value \q{10}.
\begin{aside}
The appropriateness of using \q{leftFold} or \q{rightFold} depends on whether the function being applied is left associative or right associative. If the function is left associative, it is normally better (in the sense of being closer to what one might expect) to use \q{leftFold}.
The \q{leftFold1} and \q{rightFold1} variants are used in cases where there is no natural `zero' for the function being applied.
Some functions are commutative -- like \q{(+)} -- in which case the value returned by \q{leftFold} is equal to the value returned by \q{rightFold}.
\end{aside}
\subsection{\q{leftFold} -- Aggregate from the Left}
\label{leftFold}
The \q{leftFold} function reduces a sequence by successively applying a function from the beginning of the sequence.
\begin{lstlisting}
leftFold has type for all e,c,s such that
((s,e)=>s,s,c) => s where foldable over c determines e
\end{lstlisting}
The client function takes the form:
\begin{lstlisting}[escapechar=|]
fun leftClient(|\emph{Acc}|,|\emph{El}|) is |\emph{Acc'}|
\end{lstlisting}
where \q{\emph{Acc}} is the accumulated result so far, \q{\emph{El}} is successive elements of the collection and \q{\emph{Acc'}} is the result of applying the client function to the element.
\subsection{\q{leftFold1} -- Non-zero Aggregate from the Left}
\label{leftFold1}
The \q{leftFold1} function reduces a sequence by successively applying a function from the beginning of the sequence. The first element of the sequence is used as the initial `state':
\begin{lstlisting}
leftFold1 has type for all e,c such that
((e,e)=>e,c) => c where foldable over c determines e
\end{lstlisting}
The client function takes the form:
\begin{lstlisting}[escapechar=|]
fun leftClient(|\emph{Acc}|,|\emph{El}|) is |\emph{Acc'}|
\end{lstlisting}
where \q{\emph{Acc}} is the accumulated result so far, \q{\emph{El}} is successive elements of the collection and \q{\emph{Acc'}} is the result of applying the client function to the element.
\begin{aside}
The client function has a simpler form of type than that for \q{leftFold}. In particular, the types of both arguments and the result are identical. This is because \q{leftFold1} uses the first element of the sequence as the initial seed of the computation -- as opposed to an externally provided zero.
\end{aside}
\begin{aside}
If the sequence is empty then \q{leftFold1} will raise an exception.
\end{aside}
\begin{aside}
The standard contract for \q{foldable} includes a \emph{default} implementation of \q{leftFold1}. This default implementation is used in cases where a concrete implementation does not include a definition for \q{leftFold1}.
\end{aside}
\subsection{\q{rightFold} -- Aggregate from the Right}
\label{rightFold}
The \q{rightFold} function reduces a sequence by successively applying a function from the end of the sequence.
\begin{lstlisting}
rightFold has type for all e,c,s such that
((e,s)=>s,s,c) => s where foldable over c determines e
\end{lstlisting}
The client function takes the form:
\begin{lstlisting}[escapechar=|]
fun rightClient(|\emph{El}|,|\emph{Acc}|) is |\emph{Acc'}|
\end{lstlisting}
where \q{\emph{Acc}} is the accumulated result so far, \q{\emph{El}} is succesive elements of the collection and \q{\emph{Acc'}} is the result of applying the client function to the element.
\begin{aside}
Note that the order of the arguments in the left client and the right client is different: the right client function has the `element' argument first whereas the left client has the element argument second.
This reflects the difference in expected associativity of the clients.
\end{aside}
\subsection{\q{rightFold1} -- Non-zero Aggregate from the Right}
\label{rightFold1}
The \q{rightFold1} function reduces a sequence by successively applying a function from the end of the sequence. The last element of the sequence is used as the initial `state':
\begin{lstlisting}
rightFold1 has type for all e,c such that
((e,e)=>e,c) => c where foldable over c determines e
\end{lstlisting}
\begin{aside}
The client function has the same form as that for \q{leftFold1}; in particular its type is the same. However, the order of arguments is different: in particular, the client function should take the form:
\begin{lstlisting}[escapechar=|]
fun rightClient(|\emph{El}|,|\emph{Acc}|) is |\emph{Acc'}|
\end{lstlisting}
with successive elements being passed in to the first argument and the accumulated state in the second.
\end{aside}
\begin{aside}
If the sequence is empty then \q{rightFold1} will raise an exception.
\end{aside}
\begin{aside}
The standard contract for \q{foldable} includes a \emph{default} implementation of \q{rightFold1} -- which is based on the non-default implementation of \q{rightFold}.
\end{aside}
%\section{The \q{iotaC} Sequence Generation Contract}
%\label{iotaContract}
%
%The \q{iota} function -- defined in the \q{iotaC} contract -- is used to generate sequences typically based on numbers.
%
%\begin{program}[H]
%\begin{alltt}
%contract iotaC over (r,t) is \{
% iota has type (t,t,t) => r of t
%\}
%\end{alltt}
%\caption{The \q{iotaC} Contract}\label{iotaContractProg}
%\end{program}
%The \q{iotaC} contract has two type parameters -- the first is actually a \ntRef{TypeConstructor}: the name of a generic type. The second type is typically a numeric type that defines the type of the elements in the generated sequence.
%
%\subsection{\q{iota} -- Sequence Generation}
%\begin{alltt}
%iota has type iota has type for all r,t (t,t,t) => r of t
% where iotaC over (r, t)
%\end{alltt}
%
%A call to \q{iota} of the form:
%\begin{alltt}
%iota(\emph{F},\emph{T},\emph{S})
%\end{alltt}
%returns a sequence, starting at \emph{F}, incrementing by \emph{S} and ending when the next number in the sequence would be `past' \emph{T}.
%
%If the range is ascending, if \emph{S} is positive, then the sequence is terminated by the first number that is larger than \emph{T}. Conversely, for descending sequences, when \emph{S} is negative, the sequence is terminated by the last number that is larger than \emph{T}.
%
%For example, the call
%\begin{alltt}
%iota(1,12,3)
%\end{alltt}
%returns the \q{list}
%\begin{alltt}
%list of [1, 4, 7, 10]
%\end{alltt}
%(since the next number in the sequence -- 13 -- is larger than 12) and the call
%\begin{alltt}
%iota(10.0,0.0,-1.0)
%\end{alltt}
%returns the \q{list}
%\begin{alltt}
%list of [10.0, 9.0, 8.0, 7.0, 6.0, 5.0, 4.0, 3.0, 2.0, 1.0, 0.0]
%\end{alltt}
%
%
\section{The \q{updateable} Contract}
\label{updateableContract}
\index{updateable contract@\q{updateable} contract}
\index{modifying collections}
\index{contract!updateable@\q{updateable}}
The \q{updateable} contract captures some key functions involved in updating collections. The contract -- which is defined in Program~\vref{updateableContractProg} -- contains definitions for adding elements to a collection, merging two collections, updating a collection and deleting elements from the collection.
\begin{program}[H]
\begin{lstlisting}
contract updateable over r determines t is {
_extend has type (r,t)=>r;
_merge has type (r, r) => r;
_delete has type (r, ()<=t) => r;
_update has type (r, ()<=t, (t)=>t) => r;
}
\end{lstlisting}
\caption{The \q{updateable} Contract}\label{updateableContractProg}
\end{program}
The \q{updateable} contract is implemented for all the standard collection types: \q{cons}, \q{list}, \q{queue} and \q{dictionary}.
\subsection{Syntax for Updating Collections}
\label{updateSyntax}
Along with the contract, there is a standard notation for describing the updating of collections. This syntax is defined in Figure~\vref{updateSyntaxFig}.
\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{UpdateAction}&\arrow&\q{extend}\ \ntRef{Target}\ \q{with}\ \ntRef{Expression}\\
&\choice&\q{merge}\ \ntRef{Target}\ \q{with}\ \ntRef{Expression}\\
&\choice&\q{update}\ \ntRef{Pattern}\ \q{in}\ \ntRef{Target}\ \q{with}\ \ntRef{Expression}\\
&\choice&\q{delete}\ \ntRef{Pattern}\ \q{in}\ \ntRef{Target}
\end{eqnarray*}
\caption{Notation for updating collections}\label{updateSyntaxFig}
\end{figure}
The first `argument' of many of these actions is a \ntRef{Target}, i.e., they have the same semantics as the left hand side of an assignment action -- see Section~\vref{assignment}. In fact, one of the requirements of an \ntRef{UpdateAction} is that the collection being modified is in a re-assignable variable or field.
\subsection{\q{\_extend} a Collection}
\label{extend}
The \q{\_extend} function is used to `add' an element to a collection:
\begin{lstlisting}
_extend has type for all r,t such that (r,t)=>r
where updateable over r determines t
\end{lstlisting}
As an example of the use of \q{\_extend}, consider the \ntRef{Action}:
\begin{lstlisting}
extend R with ("fred",23)
\end{lstlisting}
assuming that \q{R} was defined as a list:
\begin{lstlisting}
var R := list of [ ("peter",20) ]
\end{lstlisting}
then after the \q{extend}, \q{R} will contain two tuples:
\begin{lstlisting}
list of [ ("fred", 23), ("peter",20) ]
\end{lstlisting}
\begin{aside}
Note that there is no implied commitment to preserve order of insertion into a collection. I.e., a sequence of \q{\_extend}s into a collection may not be visible when the collection is iterated over or searched.
\end{aside}
The relationship between the \q{extend} action and the \q{\_extend} function is captured in the macro rule:
\begin{lstlisting}
#extend ?Tgt with ?Exp ==> Tgt := _extend(Tgt,Exp)
\end{lstlisting}
\subsection{\q{\_merge} a Collection}
\label{merge}
The \q{\_merge} function is used to merge a collection with another one.
\begin{lstlisting}
_merge has type for all r,t such that (r,r)=>r
where updateable over r determines t
\end{lstlisting}
\begin{aside}
Technically a \q{\_merge} is equivalent to a sequence of \q{\_extend}s. However, for situations where many elements may be added simultaneously, using \q{\_merge} offer opportunities for more optimal implementations.
\end{aside}
As an example of the use of \q{\_merge}, consider the \ntRef{Action}:
\begin{lstlisting}
merge R with list of [("john",2), ("alfred",10)]
\end{lstlisting}
then, assuming the same \q{R} as above, after the \q{merge}, \q{R} will contain:
\begin{lstlisting}
list of [("fred", 23), ("john",2), ("alfred",10), ("peter",20)]
\end{lstlisting}
The relationship between the \q{merge} action and the \q{\_merge} function is captured in the macro rule:
\begin{lstlisting}
#merge ?Tgt with ?Rel ==> Tgt := _merge(Tgt,Rel)
\end{lstlisting}
\begin{aside}
One constraint of the \q{\_merge} function is that the type of the two collections must be the same. This is not necessary if an iteration is hand-coded using separate \q{\_extend} calls.
\end{aside}
\subsection{\q{\_update} a Collection}
\label{update}
The \q{\_update} function is used to update one or more elements in a collection simultaneously.
\begin{lstlisting}
_update has type for all r,t such that (r, ()<=t, (t)=>t) => r
where updateable over r determines t
\end{lstlisting}
This function takes three arguments: the collection to be updated, a \ntRef{Pattern} to identify which elements of the collection to update and a \ntRef{Function} to transform selected elements.
\begin{aside}
The \ntRef{UpdateAction} notation for \q{update} hides the existence of the pattern and function by automatically constructing the necessary programs.
\end{aside}
The \q{\_update} function `tests' each element of the collection to see if it should be updated. If an element is to be updated, then the transform function performs the change.
For example, to double all entries in \q{R} then we can use the action:
\begin{lstlisting}
update (N,X) in R with (N,X+X)
\end{lstlisting}
If we wanted to constrain the update to entries whose first element was less than \q{"fred"} we could use:
\begin{lstlisting}
update ((N,X) where N<"fred") in R with (N,2*X)
\end{lstlisting}
This last action would change \q{R} to:
\begin{lstlisting}
list of [ ("fred", 23), ("john",2), ("alfred",20), ("peter",20) ]
\end{lstlisting}
(since only \q{"alfred"} is less than \q{"fred"} in the standard lexicographical ordering).
The macro that defines the \q{update} notation in terms of \q{\_update} is:
\begin{lstlisting}
#update ?Ptn in ?Tgt with ?Exp ==> Tgt :=
_update(Tgt,(() from Ptn), (Ptn) => Exp)
\end{lstlisting}
\subsection{\q{\_delete} Elements from a Collection}
\label{delete}
The \q{\_delete} function is used to remove selected elements from a collection.
\begin{lstlisting}
_delete has type for all r,t such that (r, ()<=t) => r
where updateable over r determines t
\end{lstlisting}
This function takes two arguments: the collection to be updated and a \ntRef{Pattern} to identify which elements of the collection to remove.
\begin{aside}
The \ntRef{UpdateAction} notation for \q{delete} hides the explicit existence of the pattern abstraction.
\end{aside}
The \q{\_delete} function `tests' each element of the collection to see if it should be deleted.
For example, to delete all entries in \q{R} whose second element is less than 10 we can use the action:
\begin{lstlisting}
delete ((N,X) where X<10) in R
\end{lstlisting}
This last action would change \q{R} to:
\begin{lstlisting}
list of [("fred", 23), ("alfred",20), ("peter",20)]
\end{lstlisting}
The macro that defines the \q{delete} notation in terms of \q{\_delete} is:
\begin{lstlisting}
#delete ?Ptn in ?Tgt with ?Exp ==> Tgt := _delete(Tgt,(() from Ptn))
\end{lstlisting}
\section{The \q{explosion} Contract}
\label{explosionContract}
The \q{explosion} contract defines what it means to `pack' or 'unpack' a collection. Many sequences have a dual nature: for example \q{string}s can be viewed as compact entities that are effectively atomic, or as sequences of characters.
When exploding a \q{string}, the result is a sequence of \q{integer}s -- each representing a separate \emph{code point} in the string. This form is useful when the contents of the \q{string} needs to be processed and the former is useful when \q{string}s are processed as a whole.
\begin{aside}
Exploding a string into code points does not guarantee a unique decomposition. Some unicode characters have multiple representations as codepoints. However, alternate decompositions are guaranteed to be semantically equivalent.
\end{aside}
The explosion contract is defined in Program~\vref{explosionContractProg}.
\begin{program}[H]
\begin{lstlisting}