Skip to content

Commit 67fa5a8

Browse files
zhaojj2209zhaojj2209
authored
Modify Source Typed specs (#1366)
1 parent 86ea8df commit 67fa5a8

7 files changed

+356
-196
lines changed

‎docs/specs/source_1_typed_bnf.tex

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1+
\allowdisplaybreaks[1]
12
\begin{alignat*}{9}
2-
&& \textit{program} &&\quad ::= &\quad && \textit{import-directive} ... \ \textit{statement} ...
3+
&& \textit{program} &&\quad ::= &\quad && \textit{import-directive} ... \ \textit{type-alias} ... \ \textit{statement} ...
34
&& \textrm{\href{https://sourceacademy.org/sicpjs/3.1.1\#p6}{program}} \\[1mm]
45
&& \textit{import-directive} &&\quad ::= &\quad && \textbf{\texttt{import}}\ \textbf{\texttt{\{}}\ \textit{import-names} \ \textbf{\texttt{\}}}\ \textbf{\texttt{from}}\ \textit{string} \ \textbf{\texttt{;}} \quad
56
&& \textrm{import directive} \\[1mm]
@@ -8,14 +9,14 @@
89
&& \textrm{import name list} \\[1mm]
910
&& \textit{import-name} && ::= &\quad && \textit{name}\ | \ \textit{name} \ \textbf{\texttt{as}}\ \textit{name}
1011
&& \textrm{import name} \\[1mm]
12+
&& \textit{type-alias} && ::= &\quad && \textbf{\texttt{type}}\ \textit{name}[<\textit{name}\ (\ \textbf{\texttt{,}} \ \textit{name}\ ) ...>] \
13+
\textbf{\texttt{=}}\ \textit{alias-type} \textbf{\texttt{;}} && \textrm{type alias declaration}\\
1114
&& \textit{statement} &&\quad ::= &\quad && \textbf{\texttt{const}}\ \textit{name}[\texttt{:}\ \textit{type}] \
1215
\textbf{\texttt{=}}\ \textit{expression} \ \textbf{\texttt{;}}
1316
&& \textrm{\href{https://sourceacademy.org/sicpjs/1.1.2\#p2}{constant declaration}} \\
1417
&& && | &\quad && \textbf{\texttt{function}}\ \textit{name} \
1518
\textbf{\texttt{(}}\ \textit{names} \ \textbf{\texttt{)}}[\texttt{:}\ \textit{type}]\ \textit{block} \quad
1619
&& \textrm{\href{https://sourceacademy.org/sicpjs/1.1.4\#p4}{function declaration}}\\
17-
&& && | &\quad && \textbf{\texttt{type}}\ \textit{name}[<\textit{name}\ (\ \textbf{\texttt{,}} \ \textit{name}\ ) ...>] \
18-
\textbf{\texttt{=}}\ \textit{alias-type} \textbf{\texttt{;}} && \textrm{type alias declaration}\\
1920
&& && | &\quad && \textbf{\texttt{return}}\ \textit{expression} \ \textbf{\texttt{;}}
2021
&& \textrm{\href{https://sourceacademy.org/sicpjs/1.1.4\#p4}{return statement}}\\
2122
&& && | &\quad && \textit{if-statement} \quad
@@ -42,9 +43,6 @@
4243
&& \textrm{\href{https://sourceacademy.org/sicpjs/1.3.2\#p12}{conditional statement}} \\[1mm]
4344
&& \textit{block} && ::= & && \textbf{\texttt{\{}}\ \textit{statement} ... \ \textbf{\texttt{\}}} \quad
4445
&& \textrm{\href{https://sourceacademy.org/sicpjs/1.1.8\#p14}{block statement}}\\[1mm]
45-
\end{alignat*}
46-
47-
\begin{alignat*}{9}
4846
&& \textit{expression} && ::= &\quad && \textit{number} && \textrm{\href{https://sourceacademy.org/sicpjs/1.1.1\#p3}{primitive number expression}}\\
4947
&& && | &\quad && \textbf{\texttt{true}}\ |\ \textbf{\texttt{false}}
5048
&& \textrm{\href{https://sourceacademy.org/sicpjs/1.1.6\#p1}{primitive boolean expression}}\\

‎docs/specs/source_1_typed_typing.tex

Lines changed: 81 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -224,12 +224,12 @@ \subsubsection{Typing Relations on Expressions}
224224
\noindent
225225
\[
226226
\Rule{\Gamma, \Gamma_{alias} \vdash E_0 : (t_1, \ldots, t_n) \rightarrow t \quad \Gamma, \Gamma_{alias} \vdash E_1 : t'_1, \ldots, \Gamma, \Gamma_{alias} \vdash E_n : t'_n
227-
\quad (\forall 1 \leq i \leq n)(t'_i \wedge t_i \neq \emptyset)}{\Gamma, \Gamma_{alias} \vdash (E_0\ \Lp \ E_1, \ldots, E_n\ \Rp) : t}
227+
\quad (\forall 1 \leq i \leq n)(t'_i \wedge t_i \neq \emptyset)}{\Gamma, \Gamma_{alias} \vdash E_0\ \Lp \ E_1, \ldots, E_n\ \Rp : t}
228228
\]
229229
\noindent
230230
\[
231231
\Rule{\Gamma, \Gamma_{alias} \vdash E_0 : \Any \quad \Gamma, \Gamma_{alias} \vdash E_1 : t'_1, \ldots, \Gamma, \Gamma_{alias} \vdash E_n : t'_n
232-
}{\Gamma, \Gamma_{alias} \vdash (E_0\ \Lp \ E_1, \ldots, E_n\ \Rp) : \Any}
232+
}{\Gamma, \Gamma_{alias} \vdash E_0\ \Lp \ E_1, \ldots, E_n\ \Rp : \Any}
233233
\]
234234
\noindent
235235

@@ -251,7 +251,7 @@ \subsubsection{Typing Relations on Expressions}
251251

252252
For the \texttt{+} operator, the following rules are applied, in order of priority:
253253

254-
\begin{itemize}
254+
\begin{enumerate}
255255
\item{If the expression on the left side is a subset of type $\Number$,
256256
check that the other expression is a success type of $\Number$. The return type is $\Number$.}
257257
\item{If the expression on the left side is a subset of type $\String$,
@@ -262,7 +262,7 @@ \subsubsection{Typing Relations on Expressions}
262262
check that the other expression is a success type of $\String$. The return type is $\String$.}
263263
\item{If the expression on the left side cannot be narrowed to a subset of either $\Number$ or $\String$, check that both sides are success types of
264264
$\Number\ |\ \String$. The return type is $\Number\ |\ \String$.}
265-
\end{itemize}
265+
\end{enumerate}
266266

267267
\noindent
268268
\[
@@ -291,15 +291,15 @@ \subsubsection{Typing Relations on Expressions}
291291
\]
292292
\noindent
293293

294-
For lambda expressions, we extend $\Gamma$ with the declared types of all the function parameters,
294+
For lambda expressions, we temporarily extend $\Gamma$ with the declared types of all the function parameters,
295295
and check the type of the function body against the declared return type.
296296
As type syntax is optional, if type annotations are absent for any of the arguments or the return type, the type is assumed to be $\Any$.
297297
The type of the lambda expression is then the function type with the declared types of the parameters and the return type.
298298

299299
\noindent
300300
\[
301-
\Rule{\Gamma [x_1 \leftarrow t_1] \cdots [x_n \leftarrow t_n] \Gamma' \quad \Gamma' \vdash S : t' \quad t' \wedge t \neq \emptyset}{
302-
\Gamma, \Gamma_{alias} \vdash ( \Lp x_1:\ t_1, \ldots, x_n:\ t_n \Rp :\ t\ \texttt{=>}\ \Lc\ S\ \Rc) : (t_1, \ldots, t_n) \rightarrow t}
301+
\Rule{\Gamma [x_1 \leftarrow t_1] \cdots [x_n \leftarrow t_n] \vdash S : t' \quad t' \wedge t \neq \emptyset}{
302+
\Gamma, \Gamma_{alias} \vdash (x_1:\ t_1, \ldots, x_n:\ t_n) :\ t\ \texttt{=>}\ S : (t_1, \ldots, t_n) \rightarrow t}
303303
\]
304304
\noindent
305305

@@ -309,93 +309,133 @@ \subsubsection{Typing Relations on Expressions}
309309
\noindent
310310
\[
311311
\Rule{\Gamma, \Gamma_{alias} \vdash E_{pred} : t_{pred} \quad \Gamma, \Gamma_{alias} \vdash E_{cons} : t_{cons} \quad \Gamma, \Gamma_{alias} \vdash E_{alt} : t_{alt}
312-
\quad t_{pred} \wedge \Bool \neq \emptyset}{\Gamma, \Gamma_{alias} \vdash (E_{pred}\ \texttt{?}\ E_{cons} : E_{alt}) : t_{cons}\ |\ t_{alt}}
312+
\quad t_{pred} \wedge \Bool \neq \emptyset}{\Gamma, \Gamma_{alias} \vdash E_{pred}\ \texttt{?}\ E_{cons} : E_{alt} : t_{cons}\ |\ t_{alt}}
313313
\]
314314
\noindent
315315

316316
For as expressions, the type to cast the expression to must be a success type of the type of the expression.
317317

318318
\noindent
319319
\[
320-
\Rule{\Gamma, \Gamma_{alias} \vdash E : t' \quad t \wedge t' \neq \emptyset}{\Gamma, \Gamma_{alias} \vdash (E\ \texttt{as}\ t) : t}
320+
\Rule{\Gamma, \Gamma_{alias} \vdash E : t' \quad t \wedge t' \neq \emptyset}{\Gamma, \Gamma_{alias} \vdash E\ \texttt{as}\ t : t}
321321
\]
322322
\noindent
323323

324324
\subsubsection{Typing Relations on Statements}
325325

326-
For type alias declarations, the declared type $t$ for name $x$ is first checked against the type environments.
326+
Sequences in the top level are handled using the following steps:
327+
328+
\begin{enumerate}
329+
\item{Type alias declarations are evaluated, which adds type aliases to $\Gamma_{alias}$ to construct $\Gamma'_{alias}$.}
330+
\item{The declared types of constant declarations are added to $\Gamma$ to construct $\Gamma'$.
331+
Note that the declaration statements themselves are yet to be checked.}
332+
\item{All statements are checked using $\Gamma'$ and $\Gamma'_{alias}$.}
333+
\item{The type of the sequence is the type of the last value-producing statement.}
334+
\end{enumerate}
335+
336+
In the below rule, $D_n$ denotes constant declarations of the form $\texttt{const}\ x_n \texttt{:}\ t_n = E_n\texttt{;}$.
337+
If the type annotation for $x_n$ is absent, the declared type $t_n$ is assumed to be $\Any$.
338+
339+
\[
340+
\Rule{\begin{minipage}{140mm}
341+
$\Gamma_{alias} \vdash A_1 : \Gamma_{alias1}, \ldots, \Gamma_{aliasm-1} \vdash A_m : \Gamma'_{alias} \quad
342+
\Gamma [x_1 \leftarrow t_1] \cdots [x_n \leftarrow t_n] \Gamma'$ \\
343+
$\Gamma', \Gamma'_{alias} \vdash D_1 : t_1, \ldots, \Gamma', \Gamma'_{alias} \vdash D_n : t_n \quad
344+
\Gamma', \Gamma'_{alias} \vdash S_1 : t'_1, \ldots, \Gamma', \Gamma'_{alias} \vdash S_p : t'_p$\\
345+
\end{minipage}}{
346+
\Gamma, \Gamma_{alias} \vdash \{ A_1, \ldots, A_m, D_1, \ldots, D_n, S_1, \ldots, S_p \} : t'_p, \Gamma', \Gamma'_{alias}}
347+
\]
348+
349+
For type alias declarations, the declared type $t$ for type alias name $T$ is first checked against the type environments.
327350
Any type parameters declared are temporarily added to the type alias environment when checking the type of $t$
328351
to ensure that the type parameters are only used within $t$ itself.
329-
Then, the binding of name $x$ to type function $<T_1, \ldots, T_n> \rightarrow t$ is added to the type alias environment.
352+
Then, the binding of $T$ to type function $<T_1, \ldots, T_n> \rightarrow t$ is added to the type alias environment.
330353
If no type parameters are given, the type function is assumed to take in 0 type arguments.
331354

332355
\noindent
333356
\[
334-
\Rule{\Gamma, \Gamma_{alias} \vdash t : t \quad \Gamma_{alias} [x \leftarrow <> \rightarrow t] \Gamma_{alias}'
335-
}{\Gamma, \Gamma_{alias} \vdash (\texttt{type}\ x = t \texttt{;}) : \Undefined}
357+
\Rule{\Gamma, \Gamma_{alias} \vdash t : t \quad \Gamma_{alias} [T \leftarrow <> \rightarrow t] \Gamma'_{alias}
358+
}{\Gamma, \Gamma_{alias} \vdash \texttt{type}\ T = t \texttt{;} : \Undefined, \Gamma'_{alias}}
336359
\]
337360
\noindent
338361
\[
339362
\Rule{\Gamma, \Gamma_{alias}[T_1 \leftarrow T_1]\ldots[T_n \leftarrow T_n] \vdash t : t \quad
340-
\Gamma_{alias} [x \leftarrow <T_1, \ldots, T_n> \rightarrow T] \Gamma_{alias}'
341-
}{\Gamma, \Gamma_{alias} \vdash (\texttt{type}\ x<T_1, \ldots, T_n> = t \texttt{;}) : \Undefined}
363+
\Gamma_{alias} [T \leftarrow <T_1, \ldots, T_n> \rightarrow t] \Gamma'_{alias}
364+
}{\Gamma, \Gamma_{alias} \vdash \texttt{type}\ T<T_1, \ldots, T_n> = t \texttt{;} : \Undefined, \Gamma'_{alias}}
342365
\]
343366
\noindent
344367

345-
For constant declarations, the declared type of $x$, $t$, is added to the type environment.
346-
If the type annotation for $x$ is absent, the declared type $t$ is assumed to be $\Any$.
347-
348-
If the type annotation is a type reference to a type alias with name $T$,
349-
$t$ is first derived by applying the type arguments $t_1, \ldots, t_n$ to the type function for $T$,
368+
For constant declarations, the declared type $t$ is retrieved from the type environment.
369+
If the declared type is a type reference to a type alias with name $T$,
370+
$t$ is obtained by applying the type arguments $t_1, \ldots, t_n$ to the type function for $T$,
350371
replacing all instances of type variables $T_1, \ldots, T_n$ in $t$ with $t_1, \ldots, t_n$ respectively.
351372

352373
The derived type of the expression $E$, $t_E$, must be a success type of $t$.
353374
The type of the statement itself is $\Undefined$.
354375

355376
\noindent
356377
\[
357-
\Rule{\Gamma [x \leftarrow t] \Gamma' \quad \Gamma' \vdash E : t_E \quad t_E \wedge t \neq \emptyset}{
358-
\Gamma, \Gamma_{alias} \vdash (\texttt{const}\ x \texttt{:}\ t = E\texttt{;}) : \Undefined}
378+
\Rule{\Gamma \vdash E : t_E \quad t_E \wedge t \neq \emptyset}{
379+
\Gamma, \Gamma_{alias} \vdash \texttt{const}\ x \texttt{:}\ t = E\texttt{;} : \Undefined}
359380
\]
360381
\noindent
361382
\[
362-
\Rule{\Gamma_{alias}(T)<t_1, \ldots, t_n> = t \quad \Gamma [x \leftarrow t] \Gamma' \quad \Gamma' \vdash E : t_E \quad
363-
t_E \wedge t \neq \emptyset}{\Gamma, \Gamma_{alias} \vdash (\texttt{const}\ x \texttt{:}\ T<t_1, \ldots, t_n> = E\texttt{;}) : \Undefined}
383+
\Rule{\Gamma_{alias}(T)<t_1, \ldots, t_n> = t \quad \Gamma \vdash E : t_E \quad t_E \wedge t \neq \emptyset
384+
}{\Gamma, \Gamma_{alias} \vdash \texttt{const}\ x \texttt{:}\ T<t_1, \ldots, t_n> = E\texttt{;} : \Undefined}
364385
\]
365386
\noindent
366387

367388
The type of return statements and expression statements is the type of the expression in the statement.
368389

369390
\noindent
370391
\[
371-
\Rule{\Gamma, \Gamma_{alias} \vdash E : t}{\Gamma, \Gamma_{alias} \vdash (\texttt{return}\ E\texttt{;}) : t}
392+
\Rule{\Gamma, \Gamma_{alias} \vdash E : t}{\Gamma, \Gamma_{alias} \vdash \texttt{return}\ E\texttt{;} : t}
372393
\quad
373-
\Rule{\Gamma, \Gamma_{alias} \vdash E : t}{\Gamma, \Gamma_{alias} \vdash (E\texttt{;}) : t}
394+
\Rule{\Gamma, \Gamma_{alias} \vdash E : t}{\Gamma, \Gamma_{alias} \vdash E\texttt{;} : t}
374395
\]
375396
\noindent
376397

377-
For blocks, $\Gamma$ is first extended to include the types of names declared in the block.
398+
For blocks, $\Gamma$ is first extended temporarily to include the types of names declared in the block.
378399
Then, the component statements are checked against the extended type environment.
379400

380-
We assume that whenever there is a return statement or a conditional statement with a return statement within a
381-
block, it is the last statement in the block. (One could consider a ``dead code'' error otherwise.)
401+
For function body blocks and if statement blocks, we assume that whenever there is a return statement
402+
or a conditional statement with a return statement within a block, it is the last statement in the block.
403+
(One could consider a ``dead code'' error otherwise.)
382404

383-
The type of a function body block is the type of the return statement in the block.
384-
If the block does not contain any return statements, the type is $\Undefined$.
405+
The type of a function body or if statement block is the type of the return statement in the block.
406+
If the block does not contain any return statements, the type is $\Void$,
407+
which is a special type that is used to denote the return type of a function that does not return anything,
408+
and changes to $\Undefined$ if unioned with another type that is not $\Void$.
409+
410+
In the below rule, $D_n$ denotes constant declarations of the form $\texttt{const}\ x_n \texttt{:}\ t_n = E_n\texttt{;}$.
411+
If the type annotation for $x_n$ is absent, the declared type $t_n$ is assumed to be $\Any$.
385412

386413
\noindent
387414
\[
388-
\Rule{\Gamma [x_1 \leftarrow t_1] \cdots [x_n \leftarrow t_n] \Gamma' \quad
389-
\Gamma' \vdash S_1 : t'_1, \ldots, \Gamma' \vdash S_n : t'_n \quad S_n\ \textit{is a return statement}}{
390-
\Gamma, \Gamma_{alias} \vdash \{ (\texttt{const}\ x_1 \texttt{:}\ t_1 = E_1\texttt{;}) \ldots (\texttt{const}\ x_1 \texttt{:}\ t_1 = E_1\texttt{;})\
391-
S_1, \ldots, S_n\} : t'_n}
415+
\Rule{\Gamma [x_1 \leftarrow t_1] \cdots [x_m \leftarrow t_m] \Gamma_{temp} \quad
416+
\Gamma_{temp} \vdash D_1 : t_1, \ldots, \Gamma_{temp} \vdash D_m : t_m \quad
417+
\Gamma_{temp} \vdash S_1 : t'_1, \ldots, \Gamma_{temp} \vdash S_n : t'_n
418+
}{\Gamma, \Gamma_{alias} \vdash \{ D_1, \ldots, D_m, S_1, \ldots, S_n\} :
419+
\begin{cases}
420+
t'_n & S_n\ \textit{is a return statement} \\
421+
\Void & S_n\ \textit{is not a return statement}
422+
\end{cases}
423+
}
392424
\]
425+
\noindent
426+
427+
The type of a block that is not a function body or if statement block is the type of last value-producing statement in the block.
428+
429+
In the below rule, $D_n$ denotes constant declarations of the form $\texttt{const}\ x_n \texttt{:}\ t_n = E_n\texttt{;}$.
430+
If the type annotation for $x_n$ is absent, the declared type $t_n$ is assumed to be $\Any$.
431+
We also assume that $S_k$ is the last value-producing statement in the block.
432+
393433
\noindent
394434
\[
395-
\Rule{\Gamma [x_1 \leftarrow t_1] \cdots [x_n \leftarrow t_n] \Gamma' \quad
396-
\Gamma' \vdash S_1 : t'_1, \ldots, \Gamma' \vdash S_n : t'_n \quad S_n\ \textit{is not a return statement}}{
397-
\Gamma, \Gamma_{alias} \vdash \{ (\texttt{const}\ x_1 \texttt{:}\ t_1 = E_1\texttt{;}) \ldots (\texttt{const}\ x_1 \texttt{:}\ t_1 = E_1\texttt{;})\
398-
S_1, \ldots, S_n\} : \Undefined}
435+
\Rule{\Gamma [x_1 \leftarrow t_1] \cdots [x_m \leftarrow t_m] \Gamma_{temp} \quad
436+
\Gamma_{temp} \vdash D_1 : t_1, \ldots, \Gamma_{temp} \vdash D_m : t_m \quad
437+
\Gamma_{temp} \vdash S_1 : t'_1, \ldots, \Gamma_{temp} \vdash S_n : t'_n
438+
}{\Gamma, \Gamma_{alias} \vdash \{ D_1, \ldots, D_m, S_1, \ldots, S_n\} : t'_k}
399439
\]
400440
\noindent
401441

@@ -405,7 +445,7 @@ \subsubsection{Typing Relations on Statements}
405445
\noindent
406446
\[
407447
\Rule{\Gamma, \Gamma_{alias} \vdash S_{pred} : t_{pred} \quad \Gamma, \Gamma_{alias} \vdash S_{cons} : t_{cons} \quad \Gamma, \Gamma_{alias} \vdash S_{alt} : t_{alt}
408-
\quad t_{pred} \wedge \Bool \neq \emptyset}{\Gamma, \Gamma_{alias} \vdash (\texttt{if}\ (S_{pred})\ \{\ S_{cons}\ \}\
409-
\texttt{else}\ \{\ S_{alt}\ \}) : t_{cons}\ |\ t_{alt}}
448+
\quad t_{pred} \wedge \Bool \neq \emptyset}{\Gamma, \Gamma_{alias} \vdash \texttt{if}\ (S_{pred})\ S_{cons}\
449+
\texttt{else}\ S_{alt} : t_{cons}\ |\ t_{alt}}
410450
\]
411451
\noindent

0 commit comments

Comments
 (0)