main.tex

\documentclass[a4paper,10pt]{article}
%\usepackage[style=numeric]{biblatex}
%\addbibresource{main.bib}
\usepackage[T1]{fontenc}
%\usepackage{ebgaramond}
\usepackage{subfig}
\usepackage{mathpartir}
\usepackage{amsmath}
\author{Aghilas Y. Boussaa}
\sloppy
\newcommand{\kw}[1]{%
  \,\text{\textbf{#1}}\,
}
\newcommand{\pipe}{%
\; | \;
}
\begin{document}
\section{Module types}
To specify a module type, programmers would use the syntax of
figure~\ref{behaviour-surface}. It maps to the EBNF description given in
figure~\ref{behaviour-formal1}, where $X$ denotes an identifier, $t$ a type and
$\overline{X}$ a list of identifiers (more generally for all symbol $A$,
$\overline{A}$ will denote a list of $A$). This formal syntax is translated to
the one given in figure~\ref{behaviour-formal2} by the inductive rules given in
figure~\ref{behaviour-formal1to2}. This second syntax separates \texttt{param}
declarations from the others\footnote{The translation to the core language will
show how \texttt{param} declarations differ from the others.} and puts them at
the beginning of the module type definition.
\begin{figure}[h]
\begin{verbatim}
defmoduletype B do
  [ $param X(X1, ..., Xn)
  | $opaque X(X1, ..., Xn)
  | $type X(X1, ..., Xn) = t
  | callback X : t
  ]*
end
\end{verbatim}
\caption{Surface syntax proposal for module types}\label{behaviour-surface}
\end{figure}
\begin{figure}[h]
  \begin{align*}D_B^S ::=& \kw{param} X \overline{X} \pipe \kw{type} X
    \overline{X} = T \pipe \kw{opaque} X \overline{X} \pipe \kw{callback} X:T \\
    |&\, D_B^S ; D_B^S \pipe \epsilon \\
    B^S ::=& \kw{defmoduletype} X \kw{do} D_B^S \kw{end}
  \end{align*}
  \caption{A first formal syntax for module types}\label{behaviour-formal1}
\end{figure}
\begin{figure}[h]
  \begin{align*}D_B &::= \kw{type} X \overline{X} = T \pipe \kw{opaque} X
  \overline{X} \pipe \kw{callback} X:T \pipe D_B ; D_B \pipe \epsilon \\
  B &::= \kw{param} \overline{X \overline{X}}; D_B
  \end{align*}
  \caption{A second formal syntax for module types}\label{behaviour-formal2}
\end{figure}
\begin{figure}[h]
  \begin{mathpar}
    \inferrule{D\hookrightarrow_B \kw{param} \overline{X\overline{Y}};D_M\\
      D'\hookrightarrow_B \kw{param} \overline{X'\overline{Y'}};
      D_M'\\X\cap X' = \emptyset}{
      D;D'\hookrightarrow_B \kw{param}
      \overline{X\overline{Y}},\overline{X'\overline{Y'}};(D_M;D_M')}\\
    \inferrule{\\}{\kw{param} X \overline{Y} \hookrightarrow_B
      \kw{param} X \overline{Y};\epsilon}\hfill
    \inferrule{D\neq \kw{param} X \overline{Y}\\D\neq D_B^S;D_B^S}
              {D \hookrightarrow_B \kw{param} \emptyset;D}\\
  \end{mathpar}
  \caption{Translation rules between the two formal
    syntaxes for module types}\label{behaviour-formal1to2}
\end{figure}
\section{Modules}
Like with module types, we give a surface syntax for modules
(figure~\ref{module-surface}), two formal syntaxes (figure~\ref{module-formal1}
and figure~\ref{module-formal2}) and the translation rules between them
(figure~\ref{module-1to2}). The \texttt{param} keyword allows modules to depend
on types (the first kind of declaration) and to specify the arguments of
module types (the second one).
\begin{figure}[h]
\begin{verbatim}
defmodule M do
  [ $param X(X1, ..., Xn)
  | $param X(X1, ..., Xn)=t
  | $type X(X1, ..., Xn)=t
  | $opaque X(X1, ..., Xn)=t
  | @behaviour B
  | def f(X1 : t1, ..., Xn : tn) : t = e
  | defp f(X1 : t1, ..., Xn : tn) : t = e
  ]*
end
\end{verbatim}
\caption{Surface syntax proposal for modules}\label{module-surface}
\end{figure}
\begin{figure}[h]
  \begin{align*}
    D_M^S ::=& \kw{param} X \overline{X} \pipe \kw{param} X \overline{X} = T
    \pipe (\kw{type}|\kw{opaque}) X \overline{X} = T \\
    |&\kw{behaviour} X \pipe\kw{def(p)} X(\overline{X : T}) : T = E
    \pipe D_M^S; D_M^S \pipe \epsilon \\
    M^S ::=& \kw{defmodule} X \kw{do} D_M^S \kw{end}
  \end{align*}
  \caption{A first formal syntax for modules}\label{module-formal1}
\end{figure}

In the second syntax the parameters are put at the beginning, followed by
module types declarations and function and type declarations. Module types are
declared by a partial function from identifiers to records. For the translation
rules we define the union of two such functions $b$ and $b'$ by the following
equation:
\[
(b \cup b')(X) = \begin{cases} b(X) & \text{if } X  \notin \text{dom}(b'),\\
  b'(X) & \text{if } X  \notin \text{dom}(b),\\
  \{\overline{X=T};\overline{X'=T'}\}& \text{if }
  b(X)=\{\overline{X=T}\} \wedge b'(X)=\{\overline{X'=T'}\},
\end{cases}
\]
and is undefined otherwise. When using this kind of union, we make sure that the
tags $\overline{X_i}$ and $\overline{X'_i}$ are disjoint. The inductive rules of
figure~\ref{module-1to2} define jugements of the form $\Gamma,\mathcal{B}\vdash
D_M^S\hookrightarrow_M D_M$, meaning $D_M^S$ can be translated to $M$ knowing it
should implement the module types in the set $\mathcal{B}$ and the possible
module types, with their list of parameters, are given by $\Gamma$.

\begin{figure}[h]
  \begin{align*}
    D_M ::=& \,(\kw{type}|\kw{opaque})X \overline{X}=T
    \pipe \kw{def(p)} X(\overline{X : T}) : T = E
    \pipe D_M; D_M \pipe \epsilon \\
    M ::=& \kw{param} \overline{X\overline{X}};
    \kw{behaviour} X\mapsto\{\overline{X=T}\}; D_M
  \end{align*}
  \caption{A second formal syntax for modules}\label{module-formal2}
\end{figure}
\begin{figure}[h]
  \begin{mathpar}
    \inferrule{X\in\text{dom}(\Gamma)}{\Gamma,\mathcal{B}\vdash
      \kw{behaviour} X\hookrightarrow_M
      \kw{param}\emptyset;\kw{behaviour} X \mapsto \{\}; \epsilon}\\
    \inferrule{}
     {\Gamma,\mathcal{B}\vdash\kw{param} X\hookrightarrow_M
      \kw{param} X;\kw{behaviour} \emptyset; \epsilon}\\
    \inferrule{\Gamma,\mathcal{B} \vdash D \hookrightarrow_M
      \kw{param} P;\kw{behaviour} b;D_M\\
      \Gamma,\mathcal{B} \cup \text{dom}(b) \vdash D' \hookrightarrow_M
      \kw{param} P';\kw{behaviour} b';D_M'\\
      P\cap P' = \emptyset\\
      \forall X\in \text{dom}(b)\cap \text{dom}(b').
      \text{tags}(b(X))\cap \text{tags}(b'(X))=\emptyset
    }{\mathcal{B}\vdash D;D'\hookrightarrow_M \kw{param} P P';
      \kw{behaviour} b \cup b'; (D_M;D'_M)}\\
    \inferrule{\exists! B\in\mathcal{B}. X\in \Gamma(B)}
     {\Gamma,\mathcal{B}\vdash \kw{param} X=t\hookrightarrow_M
          \kw{param} \emptyset; \kw{behaviour} B\mapsto \{X=t\};\kw{type} X = t}\\
    \inferrule{D\neq \kw{param} X\\ D\neq \kw{param} X = t\\
      D\neq D^S_M;D^S_M}
     {\Gamma,\mathcal{B}\vdash D\hookrightarrow_M \kw{param} \emptyset;
      \kw{behaviour} \emptyset; D}
  \end{mathpar}
  \caption{Translation rules between the two formal syntaxes for
    modules}\label{module-1to2}
\end{figure}
\section{Programs}
We can, now, define a program as a sequence of module types and module
declarations, as done in figure~\ref{program-formal}. The translation rules are
given in figure~\ref{program-1to2}. They use the two preceding sets of rules
while maintaining a context of module types.
\begin{figure}[h]
  \begin{align*}
    P^S::=&\, B^S; P^S \pipe M^S; P^S \pipe \epsilon\\
    P::=&\, X = B \pipe X = M \pipe P;P \pipe \epsilon
  \end{align*}
  \caption{Two formal syntaxes for programs}\label{program-formal}
\end{figure}
\begin{figure}[h]
  \begin{mathpar}
    \inferrule{D^S_B\hookrightarrow_B \kw{param} \overline{X}; D\\
      \Gamma \cup (B\mapsto \overline{X})\vdash P^S\hookrightarrow_P P}{
      \Gamma\vdash\kw{defmoduletype} B \kw{do} D^S_B \kw{end}; P^S
      \hookrightarrow_P (B = \kw{param} \overline{X}; D); P
    }\\
    \inferrule{\Gamma, \emptyset\vdash D^S_M\hookrightarrow_M M\\
      \Gamma\vdash P^S\hookrightarrow_P P}{
      \Gamma\vdash\kw{defmodule} X\kw{do} D^S_M\kw{end}; P^S
      \hookrightarrow_P X = M; P
    }
  \end{mathpar}
  \caption{Translation rules between the two formal syntaxes for
    programs}\label{program-1to2}
\end{figure}
\section{Core language}
We translate the desugared syntaxes of the previous sections to 1ML's core
language without \texttt{include} nor \texttt{where} and
augmented with intersection types. The syntax of this language is given in
figure~\ref{core-syntax}.
\begin{figure}[h]
  \begin{align*}
    T ::=&\, E \pipe \kw{bool()} \pipe \{D\} \pipe (X:T)\Rightarrow T \pipe
    (X:T)\rightarrow T \\\
    |&\kw{type} \pipe =E \pipe T \cap T \pipe :X\\
    D ::=&\,X:T \pipe D;D\pipe \epsilon \\
    E ::=&\, X \pipe \kw{true} \pipe \kw{false} \pipe \kw{if} E
    \kw{then} E \kw{else} E \pipe \{N\} \pipe E.X\\
    |&\kw{fun} (X:T)\Rightarrow E \pipe
    X X \pipe \kw{type} T \pipe E :> T \pipe :X\\
    N ::=&\, X=E \pipe N ; N \pipe \epsilon
  \end{align*}
  \caption{Syntax of the core language}\label{core-syntax}
\end{figure}

Programs of the preceding section are translated to sequence of bindings. The
module types are translated to functions from types to types, and modules are
mapped to functions from types to records. The rules are given in
figure~\ref{core-trans}.

\begin{figure}[h]
  \begin{mathpar}
    \textbf{\emph{Behaviours}}\\
    \inferrule{\\}{\kw{type} X \overline{Y} = T
      \hookrightarrow_1^B X: \overline{(Y:\kw{type})\Rightarrow}[=\kw{type}T]}\\
    \inferrule{\\}{\kw{opaque} X \overline{Y}
      \hookrightarrow_1^B X: \overline{(Y:\kw{type})\Rightarrow}\kw{type}}\\
    \inferrule{\\}{\kw{callback} X: T\hookrightarrow_1^B X: T}\hfill
    \inferrule{\\}{\epsilon\hookrightarrow_1^B \epsilon}\hfill
    \inferrule{D_B\hookrightarrow_1^B D\\ D_B'\hookrightarrow_1^B D'}
      {D_B;D_B'\hookrightarrow_1^B D;D'}
  \end{mathpar}
  \caption{Translation rules to the core language}\label{core-trans}
      \end{figure}
  \begin{figure}[h]\ContinuedFloat
    \begin{mathpar}
    \textbf{\emph{Modules}}\\
    \inferrule{\\}{\kw{def} X (\overline{Y:T}): T' = E\hookrightarrow_1^M
      \left(X=\overline{\kw{fun} Y : T\Rightarrow}{E}\right):
      \left(X:\overline{(Y:T)\rightarrow}T'\right)}\\
    \inferrule{\\}{\kw{defp} X (\overline{Y:T}): T' = E\hookrightarrow_1^M
      \left(X=\overline{\kw{fun} Y : T\Rightarrow}{E}:>\overline{(Y:T)\rightarrow}T'\right):\epsilon}\\

    \inferrule{\\}{{\begin{aligned}
        \kw{type} X \overline{Y} = T\hookrightarrow_1^M&
      X=\overline{\kw{fun} Y : \kw{type}\Rightarrow}\kw{type}T:\\
      &X:\overline{(Y : \kw{type})\Rightarrow} [=\kw{type} T]
    \end{aligned}}\\\vspace{-\baselineskip}}\\
\inferrule{\\}{{\begin{aligned}
        \kw{opaque} X \overline{Y} = T\hookrightarrow_1^M&
      X=\overline{\kw{fun} Y : \kw{type}\Rightarrow}\kw{type}T:\\
      &X:\overline{(Y : \kw{type})\Rightarrow} \kw{type}
    \end{aligned}}\\\vspace{-\baselineskip}}\\
    \inferrule{\\}{\epsilon\hookrightarrow_1^M \epsilon : \epsilon}\hfill
    \inferrule{D_M\hookrightarrow_1^M N:D\\ D_M'\hookrightarrow_1^M N':D'}
      {D_B;D_B'\hookrightarrow_1^M B;B'}
      \end{mathpar}
  \caption{Translation rules to the core language}\label{core-trans}
      \end{figure}
  \begin{figure}[h]\ContinuedFloat
    \begin{mathpar}
    \textbf{\emph{Programs}}\\
    \inferrule{\\}{\epsilon\hookrightarrow_{1} \epsilon}\\
    \inferrule{D_B\hookrightarrow_{1}^B D}
              {{\begin{aligned}B=\kw{param}\overline{X\overline{Y}};D_B
                    \hookrightarrow_{1}^P B=\kw{fun} &
                    (p: \{\overline{X:\overline{(Y:\kw{type})\Rightarrow}\kw{type}}\})
                    \Rightarrow\\&\kw{type}\{\overline{X:[=p.X]};D\}\end{aligned}}\\}
              \\\vspace{-\baselineskip}
    \inferrule{P= (M=\kw{param}\overline{X};\kw{behaviour}
      \overline{B\mapsto\{\overline{X_B=T_B}\}};D_M)\\
      D_M\hookrightarrow_{1}^M N:D\\
      \overline{T'_B=T_B[\overline{X\leftarrow p.X}]}
    }{{\begin{aligned}P\hookrightarrow_{1}^P
      M= &\kw{fun} (p: \{\overline{X:\kw{type}}\})
         \Rightarrow\{\overline{X=p.X};N\}:>\\
         & (p: \{\overline{X:\kw{type}}\})\Rightarrow
         \{\overline{X:[=p.X]};D\}\cap
         \bigcap\overline{B(\{\overline{X_B=\kw{type}T'_B}\})}
% latex hack, to fix I guess
      \end{aligned}}\\\vspace{-\baselineskip}}
  \end{mathpar}
  \caption{Translation rules to the core language}\label{core-trans}
\end{figure}
  We add sealings to \texttt{defp} declarations in order to have their return
  type is checked. Thus \texttt{m.s} can't be replaced by \texttt{list(int)} in
  the tests of the \texttt{stack\_sharing.ex} example.

%\printbibliography
\end{document}