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
|
\documentclass{article}
\usepackage{fullpage,amsmath,amssymb,proof}
\newcommand{\cd}[1]{\texttt{#1}}
\newcommand{\mt}[1]{\mathsf{#1}}
\newcommand{\rc}{+ \hspace{-.075in} + \;}
\newcommand{\rcut}{\; \texttt{--} \;}
\newcommand{\rcutM}{\; \texttt{---} \;}
\begin{document}
\title{The Ur/Web Manual}
\author{Adam Chlipala}
\maketitle
\section{Ur Syntax}
In this section, we describe the syntax of Ur, deferring to a later section discussion of most of the syntax specific to SQL and XML. The sole exceptions are the declaration forms for tables, sequences, and cookies.
\subsection{Lexical Conventions}
We give the Ur language definition in \LaTeX $\;$ math mode, since that is prettier than monospaced ASCII. The corresponding ASCII syntax can be read off directly. Here is the key for mapping math symbols to ASCII character sequences.
\begin{center}
\begin{tabular}{rl}
\textbf{\LaTeX} & \textbf{ASCII} \\
$\to$ & \cd{->} \\
$\times$ & \cd{*} \\
$\lambda$ & \cd{fn} \\
$\Rightarrow$ & \cd{=>} \\
$\neq$ & \cd{<>} \\
$\leq$ & \cd{<=} \\
$\geq$ & \cd{>=} \\
\\
$x$ & Normal textual identifier, not beginning with an uppercase letter \\
$X$ & Normal textual identifier, beginning with an uppercase letter \\
\end{tabular}
\end{center}
We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas. Another separator may be used in place of a comma. The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII.
We write $\ell$ for literals of the primitive types, for the most part following C conventions. There are $\mt{int}$, $\mt{float}$, and $\mt{string}$ literals.
This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
\subsection{Core Syntax}
\emph{Kinds} classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies.
$$\begin{array}{rrcll}
\textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
&&& \mt{Unit} & \textrm{the trivial constructor} \\
&&& \mt{Name} & \textrm{field names} \\
&&& \kappa \to \kappa & \textrm{type-level functions} \\
&&& \{\kappa\} & \textrm{type-level records} \\
&&& (\kappa\times^+) & \textrm{type-level tuples} \\
&&& \_\_ & \textrm{wildcard} \\
&&& (\kappa) & \textrm{explicit precedence} \\
\end{array}$$
Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
$$\begin{array}{rrcll}
\textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
&&& \; ::: & \textrm{implicit}
\end{array}$$
\emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
$$\begin{array}{rrcll}
\textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
&&& \hat{x} & \textrm{constructor variable} \\
\\
&&& \tau \to \tau & \textrm{function type} \\
&&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
&&& \$ c & \textrm{record type} \\
\\
&&& c \; c & \textrm{type-level function application} \\
&&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
\\
&&& () & \textrm{type-level unit} \\
&&& \#X & \textrm{field name} \\
\\
&&& [(c = c)^*] & \textrm{known-length type-level record} \\
&&& c \rc c & \textrm{type-level record concatenation} \\
&&& \mt{fold} & \textrm{type-level record fold} \\
\\
&&& (c^+) & \textrm{type-level tuple} \\
&&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
\\
&&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
\\
&&& \_ :: \kappa & \textrm{wildcard} \\
&&& (c) & \textrm{explicit precedence} \\
\\
\textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
&&& M.x & \textrm{projection from a module} \\
\end{array}$$
Modules of the module system are described by \emph{signatures}.
$$\begin{array}{rrcll}
\textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
&&& X & \textrm{variable} \\
&&& \mt{functor}(X : S) : S & \textrm{functor} \\
&&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
&&& M.X & \textrm{projection from a module} \\
\\
\textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
&&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
&&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
&&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
&&& \mt{val} \; x : \tau & \textrm{value} \\
&&& \mt{structure} \; X : S & \textrm{sub-module} \\
&&& \mt{signature} \; X = S & \textrm{sub-signature} \\
&&& \mt{include} \; S & \textrm{signature inclusion} \\
&&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
&&& \mt{class} \; x & \textrm{abstract type class} \\
&&& \mt{class} \; x = c & \textrm{concrete type class} \\
\\
\textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
&&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
\end{array}$$
\emph{Patterns} are used to describe structural conditions on expressions, such that expressions may be tested against patterns, generating assignments to pattern variables if successful.
$$\begin{array}{rrcll}
\textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
&&& x & \textrm{variable} \\
&&& \ell & \textrm{constant} \\
&&& \hat{X} & \textrm{nullary constructor} \\
&&& \hat{X} \; p & \textrm{unary constructor} \\
&&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
&&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
&&& (p) & \textrm{explicit precedence} \\
\\
\textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
&&& M.X & \textrm{projection from a module} \\
\end{array}$$
\emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
$$\begin{array}{rrcll}
\textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
&&& \hat{x} & \textrm{variable} \\
&&& \hat{X} & \textrm{datatype constructor} \\
&&& \ell & \textrm{constant} \\
\\
&&& e \; e & \textrm{function application} \\
&&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
&&& e [c] & \textrm{polymorphic function application} \\
&&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
\\
&&& \{(c = e,)^*\} & \textrm{known-length record} \\
&&& e.c & \textrm{record field projection} \\
&&& e \rc e & \textrm{record concatenation} \\
&&& e \rcut c & \textrm{removal of a single record field} \\
&&& e \rcutM c & \textrm{removal of multiple record fields} \\
&&& \mt{fold} & \textrm{fold over fields of a type-level record} \\
\\
&&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
\\
&&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
\\
&&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression} \\
\\
&&& \_ & \textrm{wildcard} \\
&&& (e) & \textrm{explicit precedence} \\
\\
\textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
&&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
\end{array}$$
\emph{Declarations} primarily bring new symbols into context.
$$\begin{array}{rrcll}
\textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
&&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
&&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
&&& \mt{val} \; x : \tau = e & \textrm{value} \\
&&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
&&& \mt{structure} \; X : S = M & \textrm{module definition} \\
&&& \mt{signature} \; X = S & \textrm{signature definition} \\
&&& \mt{open} \; M & \textrm{module inclusion} \\
&&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
&&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
&&& \mt{table} \; x : c & \textrm{SQL table} \\
&&& \mt{sequence} \; x & \textrm{SQL sequence} \\
&&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
&&& \mt{class} \; x = c & \textrm{concrete type class} \\
\\
\textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
&&& X & \textrm{variable} \\
&&& M.X & \textrm{projection} \\
&&& M(M) & \textrm{functor application} \\
&&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
\end{array}$$
There are two kinds of Ur files. A file named $M\texttt{.ur}$ is an \emph{implementation file}, and it should contain a sequence of declarations $d^*$. A file named $M\texttt{.urs}$ is an \emph{interface file}; it must always have a matching $M\texttt{.ur}$ and should contain a sequence of signature items $s^*$. When both files are present, the overall effect is the same as a monolithic declaration $\mt{structure} \; M : \mt{sig} \; s^* \; \mt{end} = \mt{struct} \; d^* \; \mt{end}$. When no interface file is included, the overall effect is similar, with a signature for module $M$ being inferred rather than just checked against an interface.
\subsection{Shorthands}
There are a variety of derived syntactic forms that elaborate into the core syntax from the last subsection. We will present the additional forms roughly following the order in which we presented the constructs that they elaborate into.
In many contexts where record fields are expected, like in a projection $e.c$, a constant field may be written as simply $X$, rather than $\#X$.
A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$. Positive natural numbers may be used in most places where field names would be allowed.
In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards. More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid [c \sim c]$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.
A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively.
A signature item or declaration $\mt{class} \; x = \lambda y :: \mt{Type} \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= x \mid (x : \tau) \mid (x \; ? \; \kappa) \mid [c \sim c]$. A lone variable $x$ as a binder stands for an expression variable of unspecified type.
A $\mt{val}$ or $\mt{val} \; \mt{rec}$ declaration may include expression binders before the equal sign, following the binder grammar from the last paragraph. Such declarations are elaborated into versions that add additional $\lambda$s to the fronts of the righthand sides, as appropriate. The keyword $\mt{fun}$ is a synonym for $\mt{val} \; \mt{rec}$.
A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$. A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$.
A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$
The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
The syntax $\mt{if} \; e \; \mt{then} \; e_1 \; \mt{else} \; e_2$ expands to $\mt{case} \; e \; \mt{of} \; \mt{Basis}.\mt{True} \Rightarrow e_1 \mid \mt{Basis}.\mt{False} \Rightarrow e_2$.
There are infix operator syntaxes for a number of functions defined in the $\mt{Basis}$ module. There is $=$ for $\mt{eq}$, $\neq$ for $\mt{neq}$, $-$ for $\mt{neg}$ (as a prefix operator) and $\mt{minus}$, $+$ for $\mt{plus}$, $\times$ for $\mt{times}$, $/$ for $\mt{div}$, $\%$ for $\mt{mod}$, $<$ for $\mt{lt}$, $\leq$ for $\mt{le}$, $>$ for $\mt{gt}$, and $\geq$ for $\mt{ge}$.
A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c$. $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$, and $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$.
\section{Static Semantics}
In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values.
Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed.
\begin{itemize}
\item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
\item $\Gamma \vdash c \sim c$ proves the disjointness of two record constructors; that is, that they share no field names. We overload the judgment to apply to pairs of field names as well.
\item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
\item $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors. This is often called a \emph{definitional equality} in the world of type theory.
\item $\Gamma \vdash e : \tau$ is a standard typing judgment.
\item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
\item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations, as well as to signature items and sequences of signature items.
\item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
\item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$.
\item $\Gamma \vdash M : S$ is the module signature checking judgment.
\item $\mt{proj}(M, \overline{s}, V)$ is a partial function for projecting a signature item from $\overline{s}$, given the module $M$ that we project from. $V$ may be $\mt{con} \; x$, $\mt{datatype} \; x$, $\mt{val} \; x$, $\mt{signature} \; X$, or $\mt{structure} \; X$. The parameter $M$ is needed because the projected signature item may refer to other items from $\overline{s}$.
\item $\mt{selfify}(M, \overline{s})$ adds information to signature items $\overline{s}$ to reflect the fact that we are concerned with the particular module $M$. This function is overloaded to work over individual signature items as well.
\end{itemize}
\subsection{Kinding}
$$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
\Gamma \vdash c :: \kappa
}
\quad \infer{\Gamma \vdash x :: \kappa}{
x :: \kappa \in \Gamma
}
\quad \infer{\Gamma \vdash x :: \kappa}{
x :: \kappa = c \in \Gamma
}$$
$$\infer{\Gamma \vdash M.x :: \kappa}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
}
\quad \infer{\Gamma \vdash M.x :: \kappa}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
}$$
$$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
\Gamma \vdash \tau_1 :: \mt{Type}
& \Gamma \vdash \tau_2 :: \mt{Type}
}
\quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
\Gamma, x :: \kappa \vdash \tau :: \mt{Type}
}
\quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
\Gamma \vdash c :: \{\mt{Type}\}
}$$
$$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
\Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
& \Gamma \vdash c_2 :: \kappa_1
}
\quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
\Gamma, x :: \kappa_1 \vdash c :: \kappa_2
}$$
$$\infer{\Gamma \vdash () :: \mt{Unit}}{}
\quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
$$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
\forall i: \Gamma \vdash c_i : \mt{Name}
& \Gamma \vdash c'_i :: \kappa
& \forall i \neq j: \Gamma \vdash c_i \sim c_j
}
\quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
\Gamma \vdash c_1 :: \{\kappa\}
& \Gamma \vdash c_2 :: \{\kappa\}
& \Gamma \vdash c_1 \sim c_2
}$$
$$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$
$$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
\forall i: \Gamma \vdash c_i :: k_i
}
\quad \infer{\Gamma \vdash c.i :: k_i}{
\Gamma \vdash c :: (k_1 \times \ldots \times k_n)
}$$
$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
\Gamma \vdash c_1 :: \{\kappa'\}
& \Gamma \vdash c_2 :: \{\kappa'\}
& \Gamma, c_1 \sim c_2 \vdash c :: \kappa
}$$
\subsection{Record Disjointness}
We will use a keyword $\mt{map}$ as a shorthand, such that, for $f$ of kind $\kappa \to \kappa'$, $\mt{map} \; f$ stands for $\mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) (x_3 :: \{\kappa'\}) \Rightarrow [x_1 = f \; x_2] \rc x_3) \; []$.
$$\infer{\Gamma \vdash c_1 \sim c_2}{
\Gamma \vdash c_1 \hookrightarrow c'_1
& \Gamma \vdash c_2 \hookrightarrow c'_2
& \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
}
\quad \infer{\Gamma \vdash X \sim X'}{
X \neq X'
}$$
$$\infer{\Gamma \vdash c_1 \sim c_2}{
c'_1 \sim c'_2 \in \Gamma
& \Gamma \vdash c'_1 \hookrightarrow c''_1
& \Gamma \vdash c'_2 \hookrightarrow c''_2
& c_1 \in c''_1
& c_2 \in c''_2
}$$
$$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
\quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
\quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
\Gamma \vdash c_1 \hookrightarrow C_1
& \Gamma \vdash c_2 \hookrightarrow C_2
}
\quad \infer{\Gamma \vdash c \hookrightarrow C}{
\Gamma \vdash c \equiv c'
& \Gamma \vdash c' \hookrightarrow C
}
\quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
\Gamma \vdash c \hookrightarrow C
}$$
\subsection{Definitional Equality}
We use $\mathcal C$ to stand for a one-hole context that, when filled, yields a constructor. The notation $\mathcal C[c]$ plugs $c$ into $\mathcal C$. We omit the standard definition of one-hole contexts. We write $[x \mapsto c_1]c_2$ for capture-avoiding substitution of $c_1$ for $x$ in $c_2$.
$$\infer{\Gamma \vdash c \equiv c}{}
\quad \infer{\Gamma \vdash c_1 \equiv c_2}{
\Gamma \vdash c_2 \equiv c_1
}
\quad \infer{\Gamma \vdash c_1 \equiv c_3}{
\Gamma \vdash c_1 \equiv c_2
& \Gamma \vdash c_2 \equiv c_3
}
\quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
\Gamma \vdash c_1 \equiv c_2
}$$
$$\infer{\Gamma \vdash x \equiv c}{
x :: \kappa = c \in \Gamma
}
\quad \infer{\Gamma \vdash M.x \equiv c}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
}
\quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
$$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
\quad \infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
\quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
$$\infer{\Gamma \vdash [] \rc c \equiv c}{}
\quad \infer{\Gamma \vdash [\overline{c_1 = c'_1}] \rc [\overline{c_2 = c'_2}] \equiv [\overline{c_1 = c'_1}, \overline{c_2 = c'_2}]}{}$$
$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c \equiv c}{
\Gamma \vdash c_1 \sim c_2
}
\quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; [] \equiv i}{}
\quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; ([c_1 = c_2] \rc c) \equiv f \; c_1 \; c_2 \; (\mt{fold} \; f \; i \; c)}{}$$
$$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
\quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c)
\equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$
$$\infer{\Gamma \vdash \mt{map} \; f \; (c_1 \rc c_2) \equiv \mt{map} \; f \; c_1 \rc \mt{map} \; f \; c_2}{}$$
\subsection{Expression Typing}
We assume the existence of a function $T$ assigning types to literal constants. It maps integer constants to $\mt{Basis}.\mt{int}$, float constants to $\mt{Basis}.\mt{float}$, and string constants to $\mt{Basis}.\mt{string}$.
We also refer to a function $\mathcal I$, such that $\mathcal I(\tau)$ ``uses an oracle'' to instantiate all constructor function arguments at the beginning of $\tau$ that are marked implicit; i.e., replace $x_1 ::: \kappa_1 \to \ldots \to x_n ::: \kappa_n \to \tau$ with $[x_1 \mapsto c_1]\ldots[x_n \mapsto c_n]\tau$, where the $c_i$s are inferred and $\tau$ does not start like $x ::: \kappa \to \tau'$.
$$\infer{\Gamma \vdash e : \tau : \tau}{
\Gamma \vdash e : \tau
}
\quad \infer{\Gamma \vdash e : \tau}{
\Gamma \vdash e : \tau'
& \Gamma \vdash \tau' \equiv \tau
}
\quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
$$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
x : \tau \in \Gamma
}
\quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
}
\quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
X : \tau \in \Gamma
}
\quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
}$$
$$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
\Gamma \vdash e_1 : \tau_1 \to \tau_2
& \Gamma \vdash e_2 : \tau_1
}
\quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
\Gamma, x : \tau_1 \vdash e : \tau_2
}$$
$$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
\Gamma \vdash e : x :: \kappa \to \tau
& \Gamma \vdash c :: \kappa
}
\quad \infer{\Gamma \vdash \lambda x \; ? \; \kappa \Rightarrow e : x \; ? \; \kappa \to \tau}{
\Gamma, x :: \kappa \vdash e : \tau
}$$
$$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
\forall i: \Gamma \vdash c_i :: \mt{Name}
& \Gamma \vdash e_i : \tau_i
& \forall i \neq j: \Gamma \vdash c_i \sim c_j
}
\quad \infer{\Gamma \vdash e.c : \tau}{
\Gamma \vdash e : \$([c = \tau] \rc c')
}
\quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
\Gamma \vdash e_1 : \$c_1
& \Gamma \vdash e_2 : \$c_2
}$$
$$\infer{\Gamma \vdash e \rcut c : \$c'}{
\Gamma \vdash e : \$([c = \tau] \rc c')
}
\quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
\Gamma \vdash e : \$(c \rc c')
}$$
$$\infer{\Gamma \vdash \mt{fold} : \begin{array}{c}
x_1 :: (\{\kappa\} \to \tau)
\to (x_2 :: \mt{Name} \to x_3 :: \kappa \to x_4 :: \{\kappa\} \to \lambda [[x_2] \sim x_4]
\Rightarrow x_1 \; x_4 \to x_1 \; ([x_2 = x_3] \rc x_4)) \\
\to x_1 \; [] \to x_5 :: \{\kappa\} \to x_1 \; x_5
\end{array}}{}$$
$$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
\Gamma \vdash \overline{ed} \leadsto \Gamma'
& \Gamma' \vdash e : \tau
}
\quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
\forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
& \Gamma_i \vdash e_i : \tau
}$$
$$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
\Gamma \vdash c_1 :: \{\kappa\}
& \Gamma \vdash c_2 :: \{\kappa\}
& \Gamma, c_1 \sim c_2 \vdash e : \tau
}$$
\subsection{Pattern Typing}
$$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
\quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
\quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
$$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
& \textrm{$\tau$ not a function type}
}
\quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
& \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
}$$
$$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
& \textrm{$\tau$ not a function type}
}$$
$$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
& \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
}$$
$$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
\Gamma_0 = \Gamma
& \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
}
\quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
\Gamma_0 = \Gamma
& \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
}$$
\subsection{Declaration Typing}
We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$.
This is the first judgment where we deal with type classes, for the $\mt{class}$ declaration form. We will omit their special handling in this formal specification. In the compiler, a set of available type classes and their instances is maintained, and these instances are used to fill in expression wildcards.
We presuppose the existence of a function $\mathcal O$, where $\mathcal(M, \overline{s})$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$. Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained. A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $S$.
We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$. We write $\mt{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables.
$$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
\quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
\Gamma \vdash d \leadsto \Gamma'
& \Gamma' \vdash \overline{d} \leadsto \Gamma''
}$$
$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
\Gamma \vdash c :: \kappa
}
\quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
\overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
}$$
$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
& \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
}$$
$$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
\Gamma \vdash e : \tau
}$$
$$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
\forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
& \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
}$$
$$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
\Gamma \vdash M : S
& \textrm{ ($M$ not a $\mt{struct} \; \ldots \; \mt{end}$)}
}
\quad \infer{\Gamma \vdash \mt{structure} \; X : S = \mt{struct} \; \overline{d} \; \mt{end} \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \overline{s} \; \mt{end}
}$$
$$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
\Gamma \vdash S
}$$
$$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
}$$
$$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
\Gamma \vdash c_1 :: \{\kappa\}
& \Gamma \vdash c_2 :: \{\kappa\}
& \Gamma \vdash c_1 \sim c_2
}
\quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
}$$
$$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{
\Gamma \vdash c :: \{\mt{Type}\}
}
\quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
$$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
\Gamma \vdash \tau :: \mt{Type}
}$$
$$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
\Gamma \vdash c :: \mt{Type} \to \mt{Type}
}$$
$$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
\quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
}
\quad \infer{\overline{y}; x; \Gamma \vdash X \; \mt{of} \; \tau \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to \tau \to x \; \overline{y}}{
\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
}$$
\subsection{Signature Item Typing}
We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
$$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
\quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
\Gamma \vdash s \leadsto \Gamma'
& \Gamma' \vdash \overline{s} \leadsto \Gamma''
}$$
$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
\Gamma \vdash c :: \kappa
}
\quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
\overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
}$$
$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
& \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
}$$
$$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
\Gamma \vdash \tau :: \mt{Type}
}$$
$$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
\Gamma \vdash S
}
\quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
\Gamma \vdash S
}$$
$$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
\Gamma \vdash S
& \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
}$$
$$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
\Gamma \vdash c_1 :: \{\kappa\}
& \Gamma \vdash c_2 :: \{\kappa\}
}$$
$$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
\Gamma \vdash c :: \mt{Type} \to \mt{Type}
}
\quad \infer{\Gamma \vdash \mt{class} \; x \leadsto \Gamma, x :: \mt{Type} \to \mt{Type}}{}$$
\subsection{Signature Compatibility}
To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including mmultiple bindings for the same identifier. This is in addition to the usual alpha-variation of locally-bound variables.
We rely on a judgment $\Gamma \vdash \overline{s} \leq s'$, which expresses the occurrence in signature items $\overline{s}$ of an item compatible with $s'$. We also use a judgment $\Gamma \vdash \overline{dc} \leq \overline{dc}$, which expresses compatibility of datatype definitions.
$$\infer{\Gamma \vdash S \equiv S}{}
\quad \infer{\Gamma \vdash S_1 \equiv S_2}{
\Gamma \vdash S_2 \equiv S_1
}
\quad \infer{\Gamma \vdash X \equiv S}{
X = S \in \Gamma
}
\quad \infer{\Gamma \vdash M.X \equiv S}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
}$$
$$\infer{\Gamma \vdash S \; \mt{where} \; \mt{con} \; x = c \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa = c \; \overline{s_2} \; \mt{end}}{
\Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
& \Gamma \vdash c :: \kappa
}
\quad \infer{\Gamma \vdash \mt{sig} \; \overline{s^1} \; \mt{include} \; S \; \overline{s^2} \; \mt{end} \equiv \mt{sig} \; \overline{s^1} \; \overline{s} \; \overline{s^2} \; \mt{end}}{
\Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
}$$
$$\infer{\Gamma \vdash S_1 \leq S_2}{
\Gamma \vdash S_1 \equiv S_2
}
\quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
\quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
\Gamma \vdash \overline{s} \leq s'
& \Gamma \vdash s' \leadsto \Gamma'
& \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
}$$
$$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
\Gamma \vdash s \leq s'
}
\quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
\Gamma \vdash s \leadsto \Gamma'
& \Gamma' \vdash \overline{s} \leq s'
}$$
$$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
\Gamma \vdash S'_1 \leq S_1
& \Gamma, X : S'_1 \vdash S_2 \leq S'_2
}$$
$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
\quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}}{}$$
$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
}$$
$$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}
\quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}$$
$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
\Gamma \vdash c_1 \equiv c_2
}
\quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{con} \; x :: \mt{Type} \to \mt{Type} = c_2}{
\Gamma \vdash c_1 \equiv c_2
}$$
$$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
\Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
}$$
$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
& \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
}$$
$$\infer{\Gamma \vdash \cdot \leq \cdot}{}
\quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
\Gamma \vdash \overline{dc} \leq \overline{dc'}
}
\quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
\Gamma \vdash \tau_1 \equiv \tau_2
& \Gamma \vdash \overline{dc} \leq \overline{dc'}
}$$
$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
\Gamma \vdash M.z \equiv M'.z'
}$$
$$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
\Gamma \vdash \tau_1 \equiv \tau_2
}
\quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
\Gamma \vdash S_1 \leq S_2
}
\quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
\Gamma \vdash S_1 \leq S_2
& \Gamma \vdash S_2 \leq S_1
}$$
$$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
\Gamma \vdash c_1 \equiv c'_1
& \Gamma \vdash c_2 \equiv c'_2
}$$
$$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{class} \; x}{}
\quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{class} \; x}{}
\quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{class} \; x = c_2}{
\Gamma \vdash c_1 \equiv c_2
}$$
\subsection{Module Typing}
We use a helper function $\mt{sigOf}$, which converts declarations and sequences of declarations into their principal signature items and sequences of signature items, respectively.
$$\infer{\Gamma \vdash M : S}{
\Gamma \vdash M : S'
& \Gamma \vdash S' \leq S
}
\quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
\Gamma \vdash \overline{d} \leadsto \Gamma'
}
\quad \infer{\Gamma \vdash X : S}{
X : S \in \Gamma
}$$
$$\infer{\Gamma \vdash M.X : S}{
\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
& \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
}$$
$$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
\Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
& \Gamma \vdash M_2 : S_1
}
\quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
\Gamma \vdash S_1
& \Gamma, X : S_1 \vdash S_2
& \Gamma, X : S_1 \vdash M : S_2
}$$
\begin{eqnarray*}
\mt{sigOf}(\cdot) &=& \cdot \\
\mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
\\
\mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
\mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
\mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
\mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
\mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
\mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
\mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
\mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
\mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
\mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
\mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
\mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
\mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
\mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\
\end{eqnarray*}
\begin{eqnarray*}
\mt{selfify}(M, \cdot) &=& \cdot \\
\mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, \sigma, s) \; \mt{selfify}(M, \overline{s'}) \\
\\
\mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
\mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
\mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
\mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
\mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
\mt{selfify}(M, \mt{structure} \; X : S) &=& \mt{structure} \; X : \mt{selfify}(M.X, \overline{s}) \textrm{ (where $\Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}$)} \\
\mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
\mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
\mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
\mt{selfify}(M, \mt{class} \; x) &=& \mt{class} \; x = M.x \\
\mt{selfify}(M, \mt{class} \; x = c) &=& \mt{class} \; x = c \\
\end{eqnarray*}
\end{document}
|