-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy paththesis-proposal.html
4536 lines (4029 loc) · 340 KB
/
thesis-proposal.html
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
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<!-- 2019-08-20 Tue 07:51 -->
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>The Next 700 Module Systems</title>
<meta name="generator" content="Org mode" />
<meta name="author" content="Musa Al-hassy" />
<style type="text/css">
<!--/*--><![CDATA[/*><!--*/
.title { text-align: center;
margin-bottom: .2em; }
.subtitle { text-align: center;
font-size: medium;
font-weight: bold;
margin-top:0; }
.todo { font-family: monospace; color: red; }
.done { font-family: monospace; color: green; }
.priority { font-family: monospace; color: orange; }
.tag { background-color: #eee; font-family: monospace;
padding: 2px; font-size: 80%; font-weight: normal; }
.timestamp { color: #bebebe; }
.timestamp-kwd { color: #5f9ea0; }
.org-right { margin-left: auto; margin-right: 0px; text-align: right; }
.org-left { margin-left: 0px; margin-right: auto; text-align: left; }
.org-center { margin-left: auto; margin-right: auto; text-align: center; }
.underline { text-decoration: underline; }
#postamble p, #preamble p { font-size: 90%; margin: .2em; }
p.verse { margin-left: 3%; }
pre {
border: 1px solid #ccc;
box-shadow: 3px 3px 3px #eee;
padding: 8pt;
font-family: monospace;
overflow: auto;
margin: 1.2em;
}
pre.src {
position: relative;
overflow: visible;
padding-top: 1.2em;
}
pre.src:before {
display: none;
position: absolute;
background-color: white;
top: -10px;
right: 10px;
padding: 3px;
border: 1px solid black;
}
pre.src:hover:before { display: inline;}
/* Languages per Org manual */
pre.src-asymptote:before { content: 'Asymptote'; }
pre.src-awk:before { content: 'Awk'; }
pre.src-C:before { content: 'C'; }
/* pre.src-C++ doesn't work in CSS */
pre.src-clojure:before { content: 'Clojure'; }
pre.src-css:before { content: 'CSS'; }
pre.src-D:before { content: 'D'; }
pre.src-ditaa:before { content: 'ditaa'; }
pre.src-dot:before { content: 'Graphviz'; }
pre.src-calc:before { content: 'Emacs Calc'; }
pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
pre.src-fortran:before { content: 'Fortran'; }
pre.src-gnuplot:before { content: 'gnuplot'; }
pre.src-haskell:before { content: 'Haskell'; }
pre.src-hledger:before { content: 'hledger'; }
pre.src-java:before { content: 'Java'; }
pre.src-js:before { content: 'Javascript'; }
pre.src-latex:before { content: 'LaTeX'; }
pre.src-ledger:before { content: 'Ledger'; }
pre.src-lisp:before { content: 'Lisp'; }
pre.src-lilypond:before { content: 'Lilypond'; }
pre.src-lua:before { content: 'Lua'; }
pre.src-matlab:before { content: 'MATLAB'; }
pre.src-mscgen:before { content: 'Mscgen'; }
pre.src-ocaml:before { content: 'Objective Caml'; }
pre.src-octave:before { content: 'Octave'; }
pre.src-org:before { content: 'Org mode'; }
pre.src-oz:before { content: 'OZ'; }
pre.src-plantuml:before { content: 'Plantuml'; }
pre.src-processing:before { content: 'Processing.js'; }
pre.src-python:before { content: 'Python'; }
pre.src-R:before { content: 'R'; }
pre.src-ruby:before { content: 'Ruby'; }
pre.src-sass:before { content: 'Sass'; }
pre.src-scheme:before { content: 'Scheme'; }
pre.src-screen:before { content: 'Gnu Screen'; }
pre.src-sed:before { content: 'Sed'; }
pre.src-sh:before { content: 'shell'; }
pre.src-sql:before { content: 'SQL'; }
pre.src-sqlite:before { content: 'SQLite'; }
/* additional languages in org.el's org-babel-load-languages alist */
pre.src-forth:before { content: 'Forth'; }
pre.src-io:before { content: 'IO'; }
pre.src-J:before { content: 'J'; }
pre.src-makefile:before { content: 'Makefile'; }
pre.src-maxima:before { content: 'Maxima'; }
pre.src-perl:before { content: 'Perl'; }
pre.src-picolisp:before { content: 'Pico Lisp'; }
pre.src-scala:before { content: 'Scala'; }
pre.src-shell:before { content: 'Shell Script'; }
pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
/* additional language identifiers per "defun org-babel-execute"
in ob-*.el */
pre.src-cpp:before { content: 'C++'; }
pre.src-abc:before { content: 'ABC'; }
pre.src-coq:before { content: 'Coq'; }
pre.src-groovy:before { content: 'Groovy'; }
/* additional language identifiers from org-babel-shell-names in
ob-shell.el: ob-shell is the only babel language using a lambda to put
the execution function name together. */
pre.src-bash:before { content: 'bash'; }
pre.src-csh:before { content: 'csh'; }
pre.src-ash:before { content: 'ash'; }
pre.src-dash:before { content: 'dash'; }
pre.src-ksh:before { content: 'ksh'; }
pre.src-mksh:before { content: 'mksh'; }
pre.src-posh:before { content: 'posh'; }
/* Additional Emacs modes also supported by the LaTeX listings package */
pre.src-ada:before { content: 'Ada'; }
pre.src-asm:before { content: 'Assembler'; }
pre.src-caml:before { content: 'Caml'; }
pre.src-delphi:before { content: 'Delphi'; }
pre.src-html:before { content: 'HTML'; }
pre.src-idl:before { content: 'IDL'; }
pre.src-mercury:before { content: 'Mercury'; }
pre.src-metapost:before { content: 'MetaPost'; }
pre.src-modula-2:before { content: 'Modula-2'; }
pre.src-pascal:before { content: 'Pascal'; }
pre.src-ps:before { content: 'PostScript'; }
pre.src-prolog:before { content: 'Prolog'; }
pre.src-simula:before { content: 'Simula'; }
pre.src-tcl:before { content: 'tcl'; }
pre.src-tex:before { content: 'TeX'; }
pre.src-plain-tex:before { content: 'Plain TeX'; }
pre.src-verilog:before { content: 'Verilog'; }
pre.src-vhdl:before { content: 'VHDL'; }
pre.src-xml:before { content: 'XML'; }
pre.src-nxml:before { content: 'XML'; }
/* add a generic configuration mode; LaTeX export needs an additional
(add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
pre.src-conf:before { content: 'Configuration File'; }
table { border-collapse:collapse; }
caption.t-above { caption-side: top; }
caption.t-bottom { caption-side: bottom; }
td, th { vertical-align:top; }
th.org-right { text-align: center; }
th.org-left { text-align: center; }
th.org-center { text-align: center; }
td.org-right { text-align: right; }
td.org-left { text-align: left; }
td.org-center { text-align: center; }
dt { font-weight: bold; }
.footpara { display: inline; }
.footdef { margin-bottom: 1em; }
.figure { padding: 1em; }
.figure p { text-align: center; }
.equation-container {
display: table;
text-align: center;
width: 100%;
}
.equation {
vertical-align: middle;
}
.equation-label {
display: table-cell;
text-align: right;
vertical-align: middle;
}
.inlinetask {
padding: 10px;
border: 2px solid gray;
margin: 10px;
background: #ffffcc;
}
#org-div-home-and-up
{ text-align: right; font-size: 70%; white-space: nowrap; }
textarea { overflow-x: auto; }
.linenr { font-size: smaller }
.code-highlighted { background-color: #ffff00; }
.org-info-js_info-navigation { border-style: none; }
#org-info-js_console-label
{ font-size: 10px; font-weight: bold; white-space: nowrap; }
.org-info-js_search-highlight
{ background-color: #ffff00; color: #000000; font-weight: bold; }
.org-svg { width: 90%; }
/*]]>*/-->
</style>
<script type="text/javascript" src="https://orgmode.org/org-info.js">
/**
*
* @source: https://orgmode.org/org-info.js
*
* @licstart The following is the entire license notice for the
* JavaScript code in https://orgmode.org/org-info.js.
*
* Copyright (C) 2012-2019 Free Software Foundation, Inc.
*
*
* The JavaScript code in this tag is free software: you can
* redistribute it and/or modify it under the terms of the GNU
* General Public License (GNU GPL) as published by the Free Software
* Foundation, either version 3 of the License, or (at your option)
* any later version. The code is distributed WITHOUT ANY WARRANTY;
* without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU GPL for more details.
*
* As additional permission under GNU GPL version 3 section 7, you
* may distribute non-source (e.g., minimized or compacted) forms of
* that code without the copy of the GNU GPL normally required by
* section 4, provided you include this license notice and a URL
* through which recipients can access the Corresponding Source.
*
* @licend The above is the entire license notice
* for the JavaScript code in https://orgmode.org/org-info.js.
*
*/
</script>
<script type="text/javascript">
/*
@licstart The following is the entire license notice for the
JavaScript code in this tag.
Copyright (C) 2012-2019 Free Software Foundation, Inc.
The JavaScript code in this tag is free software: you can
redistribute it and/or modify it under the terms of the GNU
General Public License (GNU GPL) as published by the Free Software
Foundation, either version 3 of the License, or (at your option)
any later version. The code is distributed WITHOUT ANY WARRANTY;
without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU GPL for more details.
As additional permission under GNU GPL version 3 section 7, you
may distribute non-source (e.g., minimized or compacted) forms of
that code without the copy of the GNU GPL normally required by
section 4, provided you include this license notice and a URL
through which recipients can access the Corresponding Source.
@licend The above is the entire license notice
for the JavaScript code in this tag.
*/
<!--/*--><![CDATA[/*><!--*/
org_html_manager.set("TOC_DEPTH", "3");
org_html_manager.set("LINK_HOME", "");
org_html_manager.set("LINK_UP", "");
org_html_manager.set("LOCAL_TOC", "1");
org_html_manager.set("VIEW_BUTTONS", "1");
org_html_manager.set("MOUSE_HINT", "underline");
org_html_manager.set("FIXED_TOC", "0");
org_html_manager.set("TOC", "1");
org_html_manager.set("VIEW", "info");
org_html_manager.setup(); // activate after the parameters are set
/*]]>*///-->
</script>
<script type="text/javascript">
/*
@licstart The following is the entire license notice for the
JavaScript code in this tag.
Copyright (C) 2012-2019 Free Software Foundation, Inc.
The JavaScript code in this tag is free software: you can
redistribute it and/or modify it under the terms of the GNU
General Public License (GNU GPL) as published by the Free Software
Foundation, either version 3 of the License, or (at your option)
any later version. The code is distributed WITHOUT ANY WARRANTY;
without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU GPL for more details.
As additional permission under GNU GPL version 3 section 7, you
may distribute non-source (e.g., minimized or compacted) forms of
that code without the copy of the GNU GPL normally required by
section 4, provided you include this license notice and a URL
through which recipients can access the Corresponding Source.
@licend The above is the entire license notice
for the JavaScript code in this tag.
*/
<!--/*--><![CDATA[/*><!--*/
function CodeHighlightOn(elem, id)
{
var target = document.getElementById(id);
if(null != target) {
elem.cacheClassElem = elem.className;
elem.cacheClassTarget = target.className;
target.className = "code-highlighted";
elem.className = "code-highlighted";
}
}
function CodeHighlightOff(elem, id)
{
var target = document.getElementById(id);
if(elem.cacheClassElem)
elem.className = elem.cacheClassElem;
if(elem.cacheClassTarget)
target.className = elem.cacheClassTarget;
}
/*]]>*///-->
</script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
displayAlign: "center",
displayIndent: "0em",
"HTML-CSS": { scale: 100,
linebreaks: { automatic: "false" },
webFont: "TeX"
},
SVG: {scale: 100,
linebreaks: { automatic: "false" },
font: "TeX"},
NativeMML: {scale: 100},
TeX: { equationNumbers: {autoNumber: "AMS"},
MultLineWidth: "85%",
TagSide: "right",
TagIndent: ".8em"
}
});
</script>
<script type="text/javascript"
src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-AMS_HTML"></script>
</head>
<body>
<div id="content">
<h1 class="title">The Next 700 Module Systems
<br />
<span class="subtitle">Extending Dependently-Typed Languages to Implement Module System Features In The Core Language</span>
</h1>
<div id="table-of-contents">
<h2>Table of Contents</h2>
<div id="text-table-of-contents">
<ul>
<li><a href="#introduction">1. Introduction —The Proposal's “Story”</a>
<ul>
<li><a href="#orgee7102e">1.1. A Language Has Many Tongues</a></li>
<li><a href="#org9c23220">1.2. Needless Distinctions for Containers</a></li>
<li><a href="#org2dc0ee4">1.3. Proposed Contributions</a></li>
<li><a href="#org738d3e2">1.4. Overview of the Remaining Chapters</a></li>
</ul>
</li>
<li><a href="#current_approaches">2. Current Approaches</a>
<ul>
<li><a href="#orgba88b50">2.1. Expectations of Module Systems</a></li>
<li><a href="#org292fa11">2.2. Ad hoc Grouping Mechanisms</a></li>
<li><a href="#org69e5635">2.3. Existing Systems</a></li>
<li><a href="#orgc7d32fc">2.4. Facets of Structuring Mechanisms: An Agda Rendition</a></li>
<li><a href="#org6a2de21">2.5. Theory Presentations: A Structuring Mechanism</a></li>
</ul>
</li>
<li><a href="#solution_requirements">3. Solution Requirements</a>
<ul>
<li><a href="#orga008de9">3.1. Missing Features</a></li>
<li><a href="#org0517160">3.2. Desirable Features</a></li>
<li><a href="#orgdc946aa">3.3. One-Item Checklist for a Candidate Solution</a></li>
<li><a href="#org59b062f">3.4. Preliminary Research</a>
<ul>
<li><a href="#org3f2710b">3.4.1. First Observation: Syntactic Similarity for Containers</a></li>
<li><a href="#org8fd714c">3.4.2. Second Observation: Computing Similarity for Containers</a></li>
<li><a href="#org3d88793">3.4.3. Next Steps</a></li>
</ul>
</li>
</ul>
</li>
<li><a href="#approach_and_timeline">4. Approach and Timeline</a>
<ul>
<li><a href="#org714c72e">4.1. Implementation Matter</a></li>
<li><a href="#org71ce4c8">4.2. Next Steps</a></li>
<li><a href="#orga5744ee">4.3. Timeline</a>
<ul>
<li><a href="#org8ab14fb">4.3.1. The First Pass: May-October 2019</a></li>
<li><a href="#org8db9a3b">4.3.2. The Middle Pass: November 2019 - February 2020</a></li>
<li><a href="#org86aa35f">4.3.3. The Final Pass: March - April 2020</a></li>
<li><a href="#orgae7bf04">4.3.4. Concluding Phase</a></li>
</ul>
</li>
</ul>
</li>
<li><a href="#conclusion">5. Conclusion</a></li>
</ul>
</div>
</div>
<div id="outline-container-orgb2bff6f" class="outline-2">
<h2 id="introduction"><span class="section-number-2">1</span> Introduction —The Proposal's “Story”</h2>
<div class="outline-text-2" id="text-introduction">
<p>
In this chapter we aim to present the narrative that demonstrates the distinction between
what can currently be accomplished and what is desired when working with composition of software
units. We arrive at the observation that packaging concepts differ only in their use –for example,
a typeclass and a record are both sequences of declarations that only differ in the former used
for polymorphism with instance search whereas the latter is used as a structure grouping related items together.
In turn, we are led to propose that the various packaging concepts ought to have a uniform syntax.
Moreover, since records are a particular notion of packaging, the commitment to syntactic similarity
gives rise to a <a href="https://en.wikipedia.org/wiki/Homoiconicity">homoiconic</a> nature to the host language.
</p>
<p>
Within this work we refer to a <i>simple type theory</i> as a language that contains typed lambda terms
for terms and formuale; if in addition it contains typed lambda terms for ‘proofs’
—which are members of types that could be interpreted as propositions—
then we say it is
a <i>dependently-typed language</i>, or ‘DTL’ for short. More precisely, if type formation is indexed,
i.e., types may depend on a context, then we have a DTL.
With the exception of declarations and ephemeral
notions, nearly everything in a DTL is a typed lambda term.
Just as Lisp's homoiconic nature blurs data and code leaving it not as a language with primitives
but rather a language with meta-primitives,
so too the lack of distinction between term and type lends itself to generic and uniform concepts in DTLs
thereby leaving no syntactic distinction between a constructive proof and an algorithm.
</p>
<p>
Proofs are not a necessary ingredient for dependent types
(and are anyways only a matter of intent, as you yourself also
emphasised in the last meeting).
</p>
<p>
The sections below explore our primary observation, which is discussed further
later on in chapter 3 as preliminary research.
Section 1 demonstrates the variety of languages present in a single system
which are conflated in a DTL,
section 2 discusses that such conflation should by necessity apply to notions of packaging,
and section 3 concludes with proposed work to ensure that happens.
</p>
<ul class="org-ul">
<li>In the introduction to section 1, you discuss "the variety of languages present in a single system". I feel this makes sense after reading "A coding language is actually many languages working together" below, but I found it confusing on first read. Maybe put languages in quotes and change system to language?</li>
</ul>
</div>
<div id="outline-container-orgee7102e" class="outline-3">
<h3 id="orgee7102e"><span class="section-number-3">1.1</span> A Language Has Many Tongues</h3>
<div class="outline-text-3" id="text-1-1">
<p>
A programming language is actually many languages working together.
</p>
<p>
The most basic of imperative languages comes with a notion of ‘statement’ that is executed
by the computer to alter ‘state’ and a notion of ‘value’ that can be assigned to memory locations.
Statements may be sequenced or looped, whereas values may be added or multiplied, for example.
In general, the operations on one linguistic category cannot be applied to the other.
Unfortunately, a rigid separation between the two sub-languages means that binary choice, for example,
conventionally invites two notations with identical semantics —e.g.; in <code>C</code> one writes <code>if (cond) clause₁ else clause₂</code>
for statements but must use the notation <code>cond?term₁:term₂</code> for values.
Hence, there are value and statement languages.
</p>
<p>
Let us continue using the <code>C</code> language for our examples since it is so ubiquitous
and has influenced many languages. Such a choice has the benefit of referring to
a concrete language, rather than speaking in vague generalities.
Besides Agda –a language mentioned throughout the proposal–
we shall also refer to Haskell as a representative of the functional
side of programming. For example, in Haskell there is no distinction between values and statements
—the latter being a particular instance of the former— and so it uses the same notation <code>if_then_else_</code> for both.
However, in practice, statements in Haskell are more pragmatically used as a body of a <code>do</code> block for which
the rules of conditionals and local variables change –hence, Haskell is not as uniform as it initially appears.
</p>
<p>
In <code>C</code>, one declares an integer value by <code>int x;</code> but a value of a user-defined type <code>T</code>
is declared <code>struct T x;</code> since, for simplicity, one may think of <code>C</code> having an array named <code>struct</code>
that contains the definitions of user-defined types <code>T</code> and the notation <code>struct T</code> acts as an array access.
Since this is a clunky notation, we can provide an alias using the declaration <code>typedef existing-name new-name;</code>.
Unfortunately, the existing name must necessarily be a type, such as <code>struct T</code> or <code>int</code>, and cannot be an arbitrary
term. One must use <code>#define</code> to produce term aliases, which are handled by the <code>C</code> preprocessor,
which also provides <code>#include</code> to import existing libraries.
Hence, the type language is distinct from the libraries language, which is part of the preprocessor language.
</p>
<p>
In contrast, Haskell has a pragma language for enabling certain features of the compiler. Unlike <code>C</code>, it
has an interface language using <code>typeclass</code>-es which differs from its <code>module</code> language
\parencite{haskell_modules_formally, haskell_in_haskell, classic_haskell_genericity}
since the former's names
may be qualified by the names of the latter but not the other way around. In turn, <code>typeclass</code> names may be used
as constraints on types, but not so with <code>module</code> names. It may be argued that this interface language is part
of the type language, but it is sufficiently different that it could be thought of as its own language \parencite{modular_modules}
—for example, it comes with keywords <code>class, instance, =></code> that can only appear in special phrases.
In addition, by default, variable declarations are the same for built-in and user-defined types –whereas <code>C</code> requires using <code>typedef</code> to mimic such behaviour.
However, Haskell distinguishes between term and type aliases.
In contrast, Agda treats aliasing as nothing more than a normal definition.
</p>
<p>
Certain application domains require high degrees of confidence in the correctness of software.
Such program verification settings may thus have an additional specification language.
For <code>C</code>, perhaps the most popular is the ANSI C Specification Language, ACSL \parencite{acsl}.
Besides the <code>C</code> types, ACSL provides a type <code>integer</code> for specifications referring to unbounded integers
as well as numerous other notions and notations not part of the <code>C</code> language. Hence, the specification language
generally differs from the implementation language. In contrast, Haskell's specification are generally \parencite{programatica} in comments
but its relative Agda allows specifications to occur at the type level.
</p>
<p>
Whether programs actually meet their specifications ultimately requires a proof language.
For example, using the Frama-C tool \parencite{frama_c}, ACSL specifications can be supported
by Isabelle or Coq proofs. In contrast, being dependently-typed, Agda allows us to use the implementation
language also as a proof language ---<i>the only distinction is a shift in our perspective; the syntax is the same.</i>
Tools such as Idris and Coq come with ‘tactics’ —algorithms which one may invoke to produce proofs—
and may combine them using specific operations that only act on tactics, whence yet another tongue.
</p>
<p>
Hence, even the simplest of programming languages contain the first three of the following
sub-languages –types may be treated at runtime.
</p>
<ol class="org-ol">
<li>Expression language;</li>
<li>Statement, or control flow, language;</li>
<li>Type language;</li>
<li>Specification language;</li>
<li>Proof language;</li>
<li>Module language;</li>
<li>Meta-programming languages —including Coq tactics, C preprocessor, Haskell pragmas, Template Haskell's various quotation brackets <code>[x| ... ]</code>, Idris directives, etc.</li>
</ol>
<p>
As briefly discussed, the first five languages telescope down into one uniform language
within the dependently-typed language Agda. So why not the module language?
</p>
</div>
</div>
<div id="outline-container-org9c23220" class="outline-3">
<h3 id="org9c23220"><span class="section-number-3">1.2</span> Needless Distinctions for Containers</h3>
<div class="outline-text-3" id="text-1-2">
<p>
Computing is compositionality.
Large mind-bending software developments are formed by composing smaller,
much more manageable, pieces together.
How? In the previous section we outlined a number of languages
equipped with term constructors, yet we did not indicate which were
more primitive and which could be derived.
</p>
<p>
The methods currently utilised are ‘ad hoc’,
e.g., “dump the contents of packages into a new \"uber package”.
What about when the packages contain conflicting names?
“Make an uber package with field names for each package's contents”.
What about viewing the new uber package as a hierarchy of its packages?
“Make conversion methods between the two representations.”
─This <i>should be</i> mechanically derivable.
</p>
<p>
In general, there are special-purpose constructs specifically for working
with packages of “usual”, or “day-to-day” expression- or statement-level code.
That is, a language for working with containers whose contents live in another language.
This forces the users to think of these constructs as rare notions that
are rarely needed —since they belong to an ephemeral language.
They are only useful when connecting packages together
and otherwise need not be learned.
</p>
<p>
When working with mutually dependent modules, a simple workaround to cyclic
typechecking and loading is to create an interface file containing the
declarations that dependents require. To mitigate such error-prone duplication of
declarations, one may utilise literate programming to tangle the declarations to
multiple files —the actual parent module and the interface module.
This was the situation with Haskell before its recent module signature
mechanism \parencite{haskell_backpack}.
Being a purely functional language, it is unsurprising that Haskell treats
nested record field updates awkwardly: Where a C-like language may have \newline
<code>a.b.c := d</code>, Haskell requires <code>a { b = b a {c = d}}</code> which necessarily has
field names <code>b, c</code> polluting the global function namespace as field projections.
Since a record is a possibly deeply nested list of declarations,
it is trivial to flatten such a list to mechanically generate the names
<code>“a-b-c”</code> —since the dot is reserved— unfortunately this is not possible
in the core language thereby forcing users to employ ‘lenses’ to generate such
accessors by compile-time meta-programming.
In the setting of DTLs, records in the form of nested Σ-types
tend to have tremendously poor performance
—in existing implementations of Coq \parencite{coq_cat_experiences} and Agda \parencite{perna},
the culprit generally being projections.
More generally,
what if we wanted to do something with packages that the host language does not
support? “Use a pre-processor, approximate packaging at a different language level,
or simply settle with what you have.”
</p>
<p>
<b>Main Observation</b> Packages, modules, theories, contexts, traits, typeclasses, interfaces, what have you
all boil down to dependent records at the end of the day and <i>really differ</i> in <i>how</i>
they are used or implemented. At the end of section 3 we demonstrate various distinct
presentations of such notions of packaging arising from a single package declaration.
</p>
</div>
</div>
<div id="outline-container-org2dc0ee4" class="outline-3">
<h3 id="org2dc0ee4"><span class="section-number-3">1.3</span> Proposed Contributions</h3>
<div class="outline-text-3" id="text-1-3">
<p>
The proposed thesis investigates the current state of the art of grouping
mechanisms \newline —sometimes referred to as modules or packages—,
their shortcomings, and a route to implementing candidate solutions
based upon a dependently-typed language.
</p>
<p>
The introduction of first-class structuring mechanisms drastically changes the situation
by allowing the composition and manipulation of structuring mechanisms within the language itself.
Granted, languages providing combinators for structuring mechanisms are not new;
e.g., such notions already exist for Full Maude \parencite{maude_module_algebra}
and B \parencite{B_reuse}. The former is closer in spirit to our work, but
it differs from ours in that it is based on a <i>reflective logic</i>: A logic where
certain aspects of its metatheory can be faithfully represented within the logic itself.
It may well be that the meta-theory of our effort may involve reflection,
yet our distinction is that our aim is to form powerful module system features
for Dependently-Typed Languages (DTLs).
</p>
<p>
To the uninitiated, the shift to DTLs may not appear useful, or at least would
not differ much from existing approaches. We believe otherwise; indeed,
in programming and, more generally, in mathematics, there are three
—below: 1, 2a, 2b— essentially
equivalent perspectives to understanding a concept. Even though they
are equivalent, each
perspective has prompted numerous programming languages; as such, the equivalence
does not make the selection of a perspective irrelevant. The perspectives are
as follows:
</p>
<ol class="org-ol">
<li><p>
“Point-wise” or “Constituent-Based”:
A concept is understood by studying the concepts it is “made out of”.
Common examples include:
</p>
<ul class="org-ul">
<li>A mathematical set is determined by the elements it contains.</li>
<li>A method is determined by the sequence
of statements or expressions it is composed from.</li>
<li>A package —such as a record or data declaration— is determined by
its components, which may be <i>thought of</i> as fields or constructors.</li>
</ul>
<p>
Object-oriented programming is based on the notion of inheritance
which informs us of “has a” and “is a” relationships.
</p></li>
<li><p>
“Point-free” or Relationship Based:
A concept is understood by its relationship to other concepts in the domain
of discourse. This approach comes into two sub-classifications:
</p>
<ol class="org-ol">
<li><p>
“First Class Citizen” or “Concept as Data”:
The concept is treated as a static entity and is
identified by applying operations <i>onto it</i> in order to observe its nature.
Common examples include:
</p>
<ul class="org-ul">
<li>A singleton set is a set whose cardinality is 1.</li>
<li>A method, in any coding language, is a value with the ability</li>
</ul>
<p>
to act on other values of a particular type.
</p>
<ul class="org-ul">
<li>A renaming scheme to provide different names for a given package;</li>
</ul>
<p>
more generally, applicative modules.
</p></li>
<li><p>
“Second Class Citizen” or “Concept as Method”:
The concept is treated as a dynamic entity that
is fed input stimuli and is understood by its emitted observational output.
Common examples include:
</p>
<ul class="org-ul">
<li>A singleton set is a set for which there is a unique mapping to it</li>
</ul>
<p>
from any other set. Input any set, obtain a map from it to the singleton set.
</p>
<ul class="org-ul">
<li>A method, in any coding language, is unique up to observational equality:</li>
</ul>
<p>
Feed it arguments, check its behaviour. Realistically, one may want to
also consider efficiency matters.
</p>
<ul class="org-ul">
<li>Generative modules as in the <code>new</code> keyword from Object oriented programming:</li>
</ul>
<p>
Basic construction arguments are provided and a container object is produced.
</p></li>
</ol>
<p>
Observing such a sub-classification as distinct led to traditional structural
programming languages, whereas blurring the distinction somewhat led to functional programming.
</p></li>
</ol>
<p>
A simple selection of equivalent perspectives leads to wholly distinct paradigms
of thought. It is with this idea that we propose an implementation of
first-class grouping mechanisms in a dependently typed language
—theories have been proposed, on paper, but as just discussed
actual design decisions may have challenging impacts on the overall
system. Most importantly, this is a
<i>requirements driven</i> approach to coherent modularisation constructs in
dependently typed languages.
</p>
<p>
Later on,
we shall demonstrate that
with a sufficiently expressive type system, a number of
traditional programming notions regarding ‘packaging up data’ become conflated
—in particular: Records and modules; which for the most
part can all be thought of as ``dependent products with named components''.
Languages without such expressive type systems necessitate certain constraints
on these concepts according to their intended usage
—e.g., no multiple inheritance for Java's classes and only one instance for
Haskell's typeclasses.
It is not clear whether such constraints have been brought to more expressive
languages out of necessity, convention, or convenience.
Hence we propose a systematic exploration of the structuring-mechanism
design space for DTLs as a starting point for the design of an appropriate
dependently-typed module system. Along the way, we intend to provide a set
of atomic combinators that suffice as building blocks for generally desirable
features of grouping mechanisms, and moreover we intend to provide an analyses
of their interactions.
</p>
<p>
That is, we want to look at the edge cases of the design space for structuring-mechanism
<i>systems</i>, not only what is considered `convenient' or `conventional'.
Along the way, we will undoubtedly encounter `useless' or non-feasible approaches.
The systems we intend to consider would account for, say, module structures with intrinsic types
—hence treating them as first class concepts— so that
our examination is based on sound principles.
</p>
<p>
Understandably, some of the traditional constraints have to do with
implementations. For example, a Haskell typeclass is generally implemented as a dictionary
that can, for the most part, be inlined whereas a record is, in some languages, a contiguous memory
block: They can be identified in a DTL, but their uses force different implementation
methodologies and consequently they are segregated under different names.
</p>
<p>
In summary,
the proposed research is to build upon the existing state of module
systems \parencite{types_for_modules} in a dependently-typed setting \parencite{dtls_give_modules} which is substantiated by developing
an extension to a compiler.
The intended outcomes include:
</p>
<ol class="org-ol">
<li>A clean module system for DTLs that treats modules uniformly as any other value type.</li>
<li>A variety of use-cases contrasting the resulting system with previous
approaches.</li>
<li>A module system that enables rather than inhibits efficiency.</li>
<li>Demonstrate that module features traditionally handled using meta-programming can be brought
to the data-value level; thereby not actually requiring the
immense power and complexity of meta-programming.</li>
</ol>
<p>
Most importantly, we intend to implement our theory to obtain
validation that it ‘works’.
</p>
</div>
</div>
<div id="outline-container-org738d3e2" class="outline-3">
<h3 id="org738d3e2"><span class="section-number-3">1.4</span> Overview of the Remaining Chapters</h3>
<div class="outline-text-3" id="text-1-4">
<p>
When a programming languages does not provide sufficiently expressive
primitives for a concept —such as typeclass derivation \parencite{deriving_via}—
users use some form of pre-processing to accomplish their tasks.
In our case, the insufficient primitives are regarding the creation and manipulation
of theories —i.e., records, classes, packages, modules. In section 3, we will demonstrate
an undisciplined prototype that clarified the requirements of our envisioned system.
Even though the prototype appears to be metaprogramming, the aim is not to force users
interested in manipulating packages to worry about the intricacies of representations;
that is, the end goal is to avoid metaprogramming —which is an over-glorified form
of preprocessing. The goal is to <i>use a dependently-typed language to implement</i>
<i>the ‘missing’ module system features directly inside the language.</i>
</p>
<p>
The remainder of the thesis proposal is organised as follows.
</p>
<ul class="org-ul">
<li>Chapter II discusses what is expected of modularisation mechanisms,
how they could be simulated, their interdefinability in Agda, and
discuss a theoretical basis for modularisation.</li>
<li>Chapter III outlines missing features from current modularisation systems,
their use cases, and provides a checklist for a candidate module
system for DTLs.</li>
<li>Chapter IV discusses issues regarding implementation matter and the next steps
in this research, along with a proposed timeline.</li>
<li>Chapter V outlines the intended outcomes of this research effort.</li>
</ul>
<p>
An important design decision is whether the resulting development is intended
to be reasoned about or not. If reasoning is important, then a language that
better supports it is ideal. That is why we are using Agda
–using a simpler language and maintaining data invariants eventually becomes
much harder \parencite{hasochism}.
</p>
<p>
Let us conclude by attempting to justify the title of this thesis proposal.
</p>
<p>
Landin's <i>The Next 700 Programming Languages</i> \parencite{seven_hundred_langs}
inspired a number of works, including
\parencite{seven_hundred_tt_models,seven_hundred_provers, seven_hundred_hoas,seven_hundred_libraries, seven_hundred_data}
and more.
The intended aim of the thesis is a requirements driven approach to coherent
modularisation constructs in DTLs. In particular, we wish to extend Agda
to be powerful enough to implement the module system features, in the core language,
that people actually want and currently mimic by-hand or using third-party preprocessors.
An eager fix would be to provide metaprogramming features,
but unless one is altering the syntax or producing efficient code, this is
glorified pre-processing —it is a means to fake missing abstraction features.
Moreover, metaprogramming would be a hammer too big for the nail we are interested in;
so big that its introduction might ruin the soundness of the DTLs
—e.g., two terms may be ill-typed and ill-formed, such as <code>x +</code> and <code>5 = 3</code>, but
are meaningful when joined together, as in <code>x + 5 = 3</code>.
Our aim is to provide just the right level of abstraction so that, if anything,
users can write a type of container or method upon it then derive ‘700’ simple
alternate views of the same container and method.
</p>
<p>
To be clear, consider a semi-ring —or any simple record of 17 different kinds of
data.
A semi-ring consists of two monoids —each consisting of a total of 7 items
of data and proof matter— where one of them is commutative and there are two
distributivity axioms. Hence, a semi-ring consists of 17 items.
If we wanted to expose, say, 3 such items —for example, the shared carrier and the
identities of each monoid— then there are a total of \(\binom{17}{3} = 680\) ways,
and if we jump to 4 items we have \(\binom{17}{4} = 2380\) possible forms.
Of course these numbers are only upper bounds when record fields depend on earlier items.
In section 3, we provide explicit examples of different structural presentations of
packages.
</p>
<p>
Usually, library designers provide one or two views, along with conversion functions,
and commit to those; instead we want to liberate them to choose whatever presentation
is convenient for the tasks at hand and to work comfortably with the guarantee that
all the presentations are isomorphic. Humans should be left to tackle difficult and
interesting problems; machines should derive the tedious and uninteresting
—even if it's simple, it saves time, is less error-prone, and clearly communicates
the underlying principle.
</p>
<p>
If anything, our aim is practical —to save developers from ad hoc copy-paste
preprocessing hacks.
</p>
</div>
</div>
</div>
<div id="outline-container-org0994771" class="outline-2">
<h2 id="current_approaches"><span class="section-number-2">2</span> Current Approaches</h2>
<div class="outline-text-2" id="text-current_approaches">
<p>
Structuring mechanisms for proof assistants are seen as tools providing
administrative support for large mechanisation developments
\parencite{LF_practical_module_system}, with support for them usually
being conservative: Support for structuring-mechanisms elaborates, or rewrites,
into the language of the ambient system's logic. Conservative extensions
are reasonable to avoid bootstrapping new foundations altogether but they
come at the cost of limiting expressiveness to the existing foundations;
thereby possibly producing awkward or unusual uses of linguistic phrases
of the ambient language.
</p>
<p>
We may use the term ‘module’ below due to its familiarity, however some of the
issues addressed also apply to other instances of grouping mechanisms
—such as records, code blocks, methods, files, families of files, and namespaces.
</p>
<p>
In section 2.1 we define modularisation; in section 2.2 we discuss how to
simulate it, and in section 2.3 we review what current systems can and cannot do;
then in section 2.4 we provide legitimate examples of the interdefinability of
different grouping mechanisms within Agda. We conclude in section 2.5 by
taking a look at an implementation-agnostic representation of grouping mechanisms
that is sufficiently abstract to ignore any differences between a record and
an interface but is otherwise sufficiently useful to encapsulate what is expected of
module systems.
Moreover, besides looking at the current solutions, we also briefly discuss their flaws.
</p>
</div>
<div id="outline-container-orgba88b50" class="outline-3">
<h3 id="orgba88b50"><span class="section-number-3">2.1</span> Expectations of Module Systems</h3>
<div class="outline-text-3" id="text-2-1">
<p>
Packaging systems are not so esoteric that we need to dwell on their uses;
yet we recall primary use cases to set the stage for the rest of our discussions.
</p>
<dl class="org-dl">
<dt>Namespacing</dt><dd><p>
Modules provide new unique local scopes for identifiers thereby permitting de-coupling.
</p>
<p>
The ability to have multiple files contribute to the same namespace is also desirable
for de-coupled developments. This necessitates an independence of module names from
the names of physical files —such de-conflation permits recursive modules.
</p></dd>
<dt>Information Hiding</dt><dd>Modules ought to provide the ability to enforce content <i>not</i> to be accessible,
or alterable, from outside of the module to enforce that users cannot depend on implementation design decisions.</dd>
<dt>Citizenship</dt><dd><p>
Grouping mechanisms need not be treated any more special than record types.
As such, one ought to be able to operate on them and manipulate them
like any first-class citizen.
</p>
<p>
In particular, packages themselves have types which happen to be packages.
This is the case with universal algebra, and OCaml, where
‘structures’ are typed by ‘signatures’
—note that OCaml's approach is within the same language, whereas, for example,
Haskell's recent retrofitting \parencite{haskell_backpack},
of its weak module system to allow such interfacing, is not
entirely in the core language since, for example, instantiating happens
by the package manager rather than by a core language declaration.
</p></dd>
<dt>Polymorphism</dt><dd><p>
Grouping mechanisms should group all kinds of things without prejudice.
</p>
<p>
This includes ‘nested datatypes’: Local types introduced for implementation
purposes, where only certain functionality is exposed. E.g., in an Agda record
declaration, it may be nice to declare a local type where the record fields refer to it.
This approach naturally leads into hierarchical modules as well.
</p>
<p>
Interestingly, such nesting is expressible in <a href="http://fsl.cs.illinois.edu/images/5/5e/Cayenne.pdf">Cayenne</a>, a long-gone predecessor
of Agda. The language lived for about 7 years and it is unclear why it is no longer
maintained. Speculation would be that dependent types were poorly understood by
the academics let alone the coders —moreover, it had essentially one maintainer
who has since moved on to other projects.
</p>
<p>
With the metaprogramming inspired approach we are proposing, it is only reasonable that, for example,
one be able to mechanically transform a package with a local type declaration into
a package with the local declaration removed and a new component added to abstract it.
That is, a particular implementation is no longer static, but dynamic.
</p></dd>
</dl>
<p>
It would not be unreasonable to consider adding to this enumeration:
</p>
<dl class="org-dl">
<dt>Sharing</dt><dd>The computation performed for a module parameter should be
shared across its constituents, rather than inefficiently being recomputed