Skip to content

Commit b200865

Browse files
MesablooMesabloo
committed
remove 'by-ref' operator and pointers in favor of references
1 parent d9cfc5c commit b200865

File tree

2 files changed

+56
-51
lines changed

2 files changed

+56
-51
lines changed

‎namespaces.tex‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,7 @@
192192
\newcommand*\Eunsigned[1]{\ensuremath{\mathsf{\Ifmt u{#1}}}}
193193
\newcommand*\Esigned[1]{\ensuremath{\mathsf{\Ifmt s{#1}}}}
194194
\newcommand*\Echar{\ensuremath{\mathsf{\Ifmt char}}}
195-
\newcommand*\Eptr[1]{\ensuremath{\operatorname{\mathsf{\Ifmt ptr}}{#1}}}
195+
\newcommand*\Eref[2]{\ensuremath{\operatorname{\mathsf{\Ifmt ref}}{#1}\;\mathsf{\Ifmt @}\;{#2}}}
196196
\newcommand*\Eletin[5]{\ensuremath{\mathsf{\Ifmt let}\ {#2}\ {#1}\ \mathsf{\Ifmt :}\ {#3}\mathrel{\mathsf{\Ifmt \coloneqq}}{#4}\mathrel{\mathsf{\Ifmt ;}}{#5}}}
197197
\newcommand*\Erecin[5]{\ensuremath{\mathsf{\Ifmt rec}\ {#2}\ {#1}\ \mathsf{\Ifmt :}\ {#3}\mathrel{\mathsf{\Ifmt \coloneqq}}{#4}\mathrel{\mathsf{\Ifmt ;}}{#5}}}
198198
\newcommand*\Ediv{\ensuremath{\mathsf{\Ifmt div}}}
@@ -201,8 +201,9 @@
201201
\newcommand*\Ewithhnd[6]{\ensuremath{\mathsf{\Ifmt with}\ {#1}\ \mathsf{\Ifmt let}\ {#2}\ {#3}{#4}\mathrel{\mathsf{\Ifmt \coloneqq}}{#5}\mathrel{\mathsf{\Ifmt ;}}{#6}}}
202202
\newcommand*\Ewith[2]{\ensuremath{\mathsf{\Ifmt with}\ {#1}\mathrel{\mathsf{\Ifmt ;}}{#2}}}
203203
\newcommand*\Eresume{\ensuremath{\mathsf{\Ifmt resume}}}
204-
\newcommand*\Ederef[1]{\ensuremath{{}^\mathsf{\Ifmt \ast}{#1}}}
205-
\newcommand*\Emkptr[1]{\ensuremath{\mathsf{\Ifmt !}{#1}}}
204+
\newcommand*\Ederef[1]{\ensuremath{\mathsf{\Ifmt !}{#1}}}
205+
\newcommand*\Emkref[1]{\ensuremath{\mathsf{\Ifmt \&}{#1}}}
206+
\newcommand*\Eregion{\ensuremath{\mathsf{\Ifmt region}}}
206207

207208
\newcommand*\surface[1]{\ensuremath{{\color{Fuchsia}\mathsf{#1}}}}
208209
\newcommand*\core[1]{\ensuremath{{\color{WildStrawberry}\mathsf{#1}}}}

‎part1-zilch.tex‎

Lines changed: 52 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -362,25 +362,27 @@ \subsection{Variables, typed holes and literals}\label{subsec:zilch-grammar-expr
362362
\label{fig:zilch-grammar-expressions-atom-grammar}
363363
\end{figure}
364364

365-
The by-ref operator \texttt{\&id} is only allowed if it appears within the top-most application in a \texttt{let} local binding.
366-
For example, these uses of the by-ref operator are valid:
367-
\begin{listing}[H]
368-
\inputminted{\zilchlexer}{examples/correct-byref.zc}
369-
370-
\captionsetup{style=invisible}
371-
\caption{Correct usage of by-ref operator.}
372-
\end{listing}
373-
\vspace*{-\baselineskip}
374-
375-
Hoewver, these uses are invalid:
376-
\begin{listing}[H]
377-
\inputminted{\zilchlexer}{examples/incorrect-byref.zc}
378-
379-
\captionsetup{style=invisible}
380-
\caption{Incorrect usage of by-ref operator.}
381-
\end{listing}
382-
\vspace*{-\baselineskip}
383-
In \texttt{test2}, the by-ref operator is in fact used in the application of \texttt{+} (recall that \texttt{a + b} is \texttt{\_+\_(a, b)}), which is not the top-most application in this local binding.
365+
% NOTE: &x now denotes making a reference
366+
%
367+
% The by-ref operator \texttt{\&id} is only allowed if it appears within the top-most application in a \texttt{let} local binding.
368+
% For example, these uses of the by-ref operator are valid:
369+
% \begin{listing}[H]
370+
% \inputminted{\zilchlexer}{examples/correct-byref.zc}
371+
372+
% \captionsetup{style=invisible}
373+
% \caption{Correct usage of by-ref operator.}
374+
% \end{listing}
375+
% \vspace*{-\baselineskip}
376+
377+
% Hoewver, these uses are invalid:
378+
% \begin{listing}[H]
379+
% \inputminted{\zilchlexer}{examples/incorrect-byref.zc}
380+
381+
% \captionsetup{style=invisible}
382+
% \caption{Incorrect usage of by-ref operator.}
383+
% \end{listing}
384+
% \vspace*{-\baselineskip}
385+
% In \texttt{test2}, the by-ref operator is in fact used in the application of \texttt{+} (recall that \texttt{a + b} is \texttt{\_+\_(a, b)}), which is not the top-most application in this local binding.
384386

385387
\subsection{Additive and multiplicative pairs}\label{subsec:zilch-grammar-expressions-pairs}
386388

@@ -1007,7 +1009,7 @@ \subsection{Local bindings and effect handling}\label{subsec:zilch-staticsem-exp
10071009
It is important because we disallow erasing function calls which cannot be guaranteed to always terminate (to prevent from making the type-checker loop indefinitely).
10081010
In the case of non-erased terms, we use termination checking to put the builtin $\Ediv$\ effect on functions which may not terminate (which are not \textit{total}).
10091011

1010-
The predicate $\Eterminates{x}$ is left undefined as it is an implementation detail\footnote{There are many ways to detect termination, either through termination metrics as in ATS, or structural recursion as in Coq or Agda, or just never allow recursion, etc.}.
1012+
The predicate $\Eterminates{x}$ is left undefined as it is an implementation detail\footnote{There are many ways to detect termination, either through termination metrics as in ATS, or structural recursion as in Coq or Agda, or just never allow recursion, etc. There are many ways to handle this and none is objectively better than all others.}.
10111013
However it must be present to ensure consistency and non-looping static behaviors.
10121014

10131015
\begin{figure}[H]
@@ -1309,22 +1311,23 @@ \subsection{Atomic expressions}\label{subsec:zilch-staticsem-exprs-atoms}
13091311

13101312
\begin{prooftree}
13111313
\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype{\ell}}{\Etotal}}
1312-
\infer1[\textsc{[Ptr-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Eptr{A}}{0}{\Etype{\ell}}{\Etotal}}
1314+
\hypo{\TypeSequent{\scale{0}{\Gamma}}{\rho}{0}{\Eregion}{\Etotal}}
1315+
\infer2[\textsc{[Ref-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Eref{A}{\rho}}{0}{\Etype{\ell}}{\Etotal}}
13131316
\end{prooftree}
13141317
\hspace{1.5em}
13151318
\begin{prooftree}
1316-
\hypo{\TypeSequent{\Gamma}{p}{\pi}{\Eptr{A}}{\epsilon}}
1317-
\infer1[\textsc{[Ptr-E]}]{\TypeSequent{\Gamma}{\Ederef{p}}{\pi}{A}{\epsilon}}
1319+
\hypo{\TypeSequent{\Gamma}{p}{\pi}{\Eref{A}{\rho}}{\epsilon}}
1320+
\infer1[\textsc{[Ref-E]}]{\TypeSequent{\Gamma}{\Ederef{p}}{\pi}{A}{\epsilon}}
13181321
\end{prooftree}
13191322
\\\vspace*{\baselineskip}
13201323
\begin{prooftree}
13211324
\hypo{\TypeSequent{\Gamma}{e}{\pi}{A}{\epsilon}}
1322-
\infer1[\textsc{[Ptr-I]}]{\TypeSequent{\Gamma}{\Emkptr{e}}{\pi}{\Eptr{A}}{\epsilon}}
1323-
\end{prooftree} % do we really want to allow this?
1325+
\infer1[\textsc{[Ref-I]}]{\TypeSequent{\Gamma}{\Emkref{e}}{\pi}{\Eref{A}{\rho}}{\epsilon}}
1326+
\end{prooftree}
13241327
}
13251328
}
13261329

1327-
\caption{Type inference rules for pointers.}
1330+
\caption{Type inference rules for references.}
13281331
\label{fig:zilch-staticsem-exprs-atoms-ptr-typerules}
13291332
\end{figure}
13301333

@@ -1374,32 +1377,33 @@ \section{A few notes}\label{sec:zilch-staticsem-notes}
13741377
\begin{description}[itemindent=0pt,left=0pt]
13751378
\item[For expressions]
13761379
\begin{align*}
1377-
\D{\lambda() \Rightarrow e} & \equiv \core{\D{\lambda(\omega\ \_ : \mathbf{1}) \Rightarrow e}} \\
1378-
\D{\lambda(\vec{\rho\ x : A}) \Rightarrow e} & \equiv \core{\lambda(\rho_0\ x_0 : \D{A_0}) \Rightarrow \ldots \Rightarrow \lambda(\rho_n\ x_n : \D{A_n}) \Rightarrow \D{e}} \\
1379-
\D{f(\vec{x})} & \equiv \core{\D{f}(\D{x_0})(\ldots)(\D{x_n})} \\
1380-
\D{() \to e} & \equiv \core{\D{(\omega\ \_ : \mathbf{1}) \to e}} \\
1381-
\D{(\vec{\rho\ x : A}) \to e} & \equiv \core{(\rho_0\ x_0 : \D{A_0}) \to \ldots \to (\rho_n\ x_n : \D{A_n}) \to \D{e}} \\
1382-
\D{if\ c\ then\ t\ else\ e} & \equiv \core{if\ \D{c}\ then\ \D{t}\ else\ \D{e}} \\
1383-
\D{(\vec{\rho\ x : A}) \otimes B} & \equiv \core{(\rho_0\ x_0 : \D{A_0}) \otimes \ldots \otimes (\rho_n\ x_n : \D{A_n}) \otimes \D{B}} \\
1384-
\D{()} & \equiv \core{()} \\
1385-
\D{(e)} & \equiv \core{\D{e}} \\
1386-
\D{(x_0, x_1, \ldots, x_n)} & \equiv \core{(\D{x_0}, (\D{x_1}, (\ldots, (\D{x_{n-1}}, \D{x_n})\ldots))} \\
1387-
\D{let\ (\vec{x}) \coloneqq e; f} & \equiv \core{let\ (x_0, \__0) \coloneqq \D{e};\ldots; let\ (x_{n-1},x_n) \coloneqq \__{n-1}; \D{f}} \\
1388-
\D{(\vec{x : A}) \mathbin{\&} B} & \equiv \core{(x_0 : \D{A_0}) \mathbin{\&} \ldots \mathbin{\&} (x_n : \D{A_n}) \mathbin{\&} \D{B}} \\
1389-
\D{\langle\rangle} & \equiv \core{\langle\rangle} \\
1390-
\D{\langle e\rangle} & \equiv \core{\D{e}} \\
1391-
\D{\langle x_0, x_1, \ldots, x_n\rangle} & \equiv \core{\langle\D{x_0}, \langle\D{x_1}, \langle\ldots, \langle\D{x_{n-1}}, \D{x_n}\rangle\ldots\rangle\rangle} \\
1392-
\D{let\ \rho\ f(\vec{\sigma\ x : A}) : \epsilon\ B \coloneqq e; g} & \equiv \core{let\ \rho\ f : \D{(\vec{\sigma\ x : A}) \to \epsilon\ B} \coloneqq \D{\lambda(\vec{\sigma\ x : A}) \Rightarrow e}; \D{g}} \\
1393-
\D{rec\ \rho\ f(\vec{\sigma\ x : A}) : \epsilon\ B \coloneqq e; g} & \equiv \core{rec\ \rho\ f : \D{(\vec{\sigma\ x : A}) \to \epsilon\ B} \coloneqq \D{\lambda(\vec{\sigma\ x : A}) \Rightarrow e}; \D{g}} \\
1394-
\D{let\ \rho\ x \coloneqq f(\vec{x}, \&a, \vec{y}); e} & \equiv \core{\D{let\ \rho\ (a, x) \coloneqq f(\vec{x}, a, \vec{y}); e}} \\
1395-
\D{e} & \equiv \core{e} \\
1380+
\D{\lambda() \Rightarrow e} & \equiv \core{\D{\lambda(\omega\ \_ : \mathbf{1}) \Rightarrow e}} \\
1381+
\D{\lambda(\overline{\rho\ x : A}) \Rightarrow e} & \equiv \core{\lambda(\rho_0\ x_0 : \D{A_0}) \Rightarrow \ldots \Rightarrow \lambda(\rho_n\ x_n : \D{A_n}) \Rightarrow \D{e}} \\
1382+
\D{f(\overline{x})} & \equiv \core{\D{f}(\D{x_0})(\ldots)(\D{x_n})} \\
1383+
\D{() \to e} & \equiv \core{\D{(\omega\ \_ : \mathbf{1}) \to e}} \\
1384+
\D{(\overline{\rho\ x : A}) \to e} & \equiv \core{(\rho_0\ x_0 : \D{A_0}) \to \ldots \to (\rho_n\ x_n : \D{A_n}) \to \D{e}} \\
1385+
\D{if\ c\ then\ t\ else\ e} & \equiv \core{if\ \D{c}\ then\ \D{t}\ else\ \D{e}} \\
1386+
\D{(\overline{\rho\ x : A}) \otimes B} & \equiv \core{(\rho_0\ x_0 : \D{A_0}) \otimes \ldots \otimes (\rho_n\ x_n : \D{A_n}) \otimes \D{B}} \\
1387+
\D{()} & \equiv \core{()} \\
1388+
\D{(e)} & \equiv \core{\D{e}} \\
1389+
\D{(x_0, x_1, \ldots, x_n)} & \equiv \core{(\D{x_0}, (\D{x_1}, (\ldots, (\D{x_{n-1}}, \D{x_n})\ldots))} \\
1390+
\D{let\ (\overline{x}) \coloneqq e; f} & \equiv \core{let\ (x_0, \__0) \coloneqq \D{e};\ldots; let\ (x_{n-1},x_n) \coloneqq \__{n-1}; \D{f}} \\
1391+
\D{(\overline{x : A}) \mathbin{\&} B} & \equiv \core{(x_0 : \D{A_0}) \mathbin{\&} \ldots \mathbin{\&} (x_n : \D{A_n}) \mathbin{\&} \D{B}} \\
1392+
\D{\langle\rangle} & \equiv \core{\langle\rangle} \\
1393+
\D{\langle e\rangle} & \equiv \core{\D{e}} \\
1394+
\D{\langle x_0, x_1, \ldots, x_n\rangle} & \equiv \core{\langle\D{x_0}, \langle\D{x_1}, \langle\ldots, \langle\D{x_{n-1}}, \D{x_n}\rangle\ldots\rangle\rangle} \\
1395+
\D{let\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e; g} & \equiv \core{let\ \rho\ f : \D{(\overline{\sigma\ x : A}) \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}; \D{g}} \\
1396+
\D{rec\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e; g} & \equiv \core{rec\ \rho\ f : \D{(\overline{\sigma\ x : A}) \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}; \D{g}} \\
1397+
% \D{let\ \rho\ x \coloneqq f(\overline{x}, \&a, \overline{y}); e} & \equiv \core{\D{let\ \rho\ (a, x) \coloneqq f(\overline{x}, a, \overline{y}); e}} \\
1398+
% TODO: change \& to something else
1399+
\D{e} & \equiv \core{e} \\
13961400
\end{align*}
13971401

13981402
\item[For the top-level]
13991403
\begin{align*}
1400-
\D{let\ \rho\ f(\vec{\sigma\ x : A}) : \epsilon\ B \coloneqq e} & \equiv \core{let\ \rho\ f : \D{\vec{(\sigma\ x : A)} \to \epsilon\ B} \coloneqq \D{\lambda(\vec{\sigma\ x : A}) \Rightarrow e}} \\
1401-
\D{rec\ \rho\ f(\vec{\sigma\ x : A}) : \epsilon\ B \coloneqq e} & \equiv \core{rec\ \rho\ f : \D{\vec{(\sigma\ x : A)} \to \epsilon\ B} \coloneqq \D{\lambda(\vec{\sigma\ x : A}) \Rightarrow e}} \\
1402-
\D{val\ \rho\ f(\vec{\sigma\ x : A}) : \epsilon\ B} & \equiv \core{val\ \rho\ f : (\sigma_0\ x_0 : \D{A_0}) \to \ldots \to (\sigma_n\ x_n : \D{A_n}) \to \epsilon\ \D{B}} \\
1404+
\D{let\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e} & \equiv \core{let\ \rho\ f : \D{\overline{(\sigma\ x : A)} \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}} \\
1405+
\D{rec\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e} & \equiv \core{rec\ \rho\ f : \D{\overline{(\sigma\ x : A)} \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}} \\
1406+
\D{val\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B} & \equiv \core{val\ \rho\ f : (\sigma_0\ x_0 : \D{A_0}) \to \ldots \to (\sigma_n\ x_n : \D{A_n}) \to \epsilon\ \D{B}} \\
14031407
\end{align*}
14041408
\end{description}
14051409

0 commit comments

Comments
 (0)