Add exercise set 5

info/exercises/src/ex-05/ex/check.tex

+
+% do type checking for some simple terms
+
+\pagebreak
+\begin{exercise}{}
+  For each of the following term-type pairs \((t, \tau)\), check whether the
+  term can be ascribed with the given type, i.e., whether there exists a
+  derivation of \(\Gamma \vdash t: \tau\) for some typing context \(\Gamma\) in
+  the given system. If not, briefly argue why.
+
+  \begin{enumerate}
+    \item \(\lstinline|x|, \abool\)
+    \item \(\lstinline|x| + 1, \aint\)
+    \item \(\lstinline|(x && y)  ==  (x <=  0)|, \abool\)
+    \item \(\lstinline|f| ~\ato~ \lstinline|x| ~\ato~ \lstinline|y| ~\ato~ \lstinline|f((x, y))|\): 
+    
+    \lstinline|((List[Int], Bool) => Int) => List[Int] => Bool => Int|
+    \item \lstinline|Cons(x, x)| : \lstinline|List[List[Int]]|
+  \end{enumerate}
+
+  \begin{solution}
+    \begin{enumerate}
+      \item \lstinline|x, Bool|. Derivation, assume \lstinline|x| is a boolean:
+      \begin{equation*}
+        \AxiomC{\((\lstinline|x|, \abool) \in \{(\lstinline|x|, \abool)\}\)}
+        \UnaryInfC{\(\{(\lstinline|x|, \abool)\} \vdash \lstinline|x: Bool|\)}
+        \DisplayProof
+      \end{equation*}
+      Note that this would work with any type, as there are no constraints.
+      \item \(\lstinline|x| + 1, \aint\). Derivation, assume \lstinline|x| is an
+      integer:
+      \begin{equation*}
+        \AxiomC{\((\lstinline|x|, \aint) \in \{(\lstinline|x|, \aint)\}\)}
+        \UnaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|x: Int|\)}
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|1: Int|\)}
+        \BinaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|x + 1: Int|\)}
+        \DisplayProof
+      \end{equation*}
+      Due to addition constraining the type of \lstinline|x|, other possible
+      types would not work.
+      \item \(\lstinline|(x && y)  ==  (x <=  0)|, \abool\). Not well-typed.
+      From the left-hand side, we would enforce that \lstinline|x: Bool|, but on
+      the right, we find \lstinline|x: Int|. Due to this conflict, there is no
+      valid derivation for this term.
+      \item \lstinline|f => x => y => f((x, y))|: this is the currying function.
+      Note that it will conform to \lstinline|((a, b) => c) => a => b => c| for any choice 
+      of \lstinline|a|, \lstinline|b|, and \lstinline|c|. (check)
+      \item \lstinline|Cons(x, x)| : \lstinline|List[List[Int]]|. Not
+      well-typed. The \(cons\) rule tells us that the second argument must have
+      the same type as the result, so \lstinline|x: List[List[Int]]|, but the first
+      argument enforces the type to be \lstinline|List[Int]| (again, due to result
+      type). As \(\aint \neq \alist{\aint}\), this is not well-typed.
+
+      Note that the singular assignment of \lstinline|x| to \lstinline|Nil()|
+      can make a well typed term here, but the typing must hold for \emph{all}
+      possible values of \lstinline|x|.
+    \end{enumerate}
+  \end{solution}
+  
+\end{exercise}

info/exercises/src/ex-05/ex/map.tex

+
+\begin{exercise}{}
+  Consider the following term \(t\):
+  %
+  \begin{center}
+    \(t = \) \lstinline{l =>  map(l, x =>  fst(x)(snd(x))  + snd(x))}
+    % t = \lstinline|l| ~\ato~ \lstinline|map|(\lstinline|l|, \lstinline|x| ~\ato~ \afst{\lstinline|x|}(\asnd{\lstinline|x|}) + \asnd{\lstinline|x|})
+  \end{center}
+
+  where \lstinline|map| is a function with type \(\forall \tau, \pi.\;
+  \alist{\tau} ~\ato~ (\tau ~\ato~ \pi) ~\ato~ \alist{\pi}\).
+
+  \begin{enumerate}
+    \item Label and assign type variables to each subterm of \(t\).
+    \item Generate the constraints on the type variables, assuming \(t\) is
+    well-typed, to infer the type of \(t\).
+    \item Solve the constraints via unification to deduce the type of \(t\).
+  \end{enumerate}
+  
+  \begin{solution}
+    \begin{enumerate}
+      \item We can label the subterms in the following way:
+      \begin{gather}
+        t: \tau = \lstinline|l =>  map(l, x =>  fst(x)(snd(x))  + snd(x))| \\
+        t_1: \tau_1 = \lstinline|map(l, x =>  fst(x)(snd(x))  + snd(x))| \\
+        t_2: \tau_2 = \lstinline|x =>  fst(x)(snd(x))  + snd(x)| \\
+        t_3: \tau_3 = \lstinline|fst(x)(snd(x)) + snd(x)| \\
+        t_4: \tau_4 = \lstinline|fst(x)(snd(x))| \\
+        t_5: \tau_5 = \lstinline|snd(x)| \\
+        t_6: \tau_6 = \lstinline|fst(x)| \\
+        \lstinline|l|: \tau_7 = \lstinline|l| \\
+        \lstinline|x|: \tau_8 = \lstinline|x| \\
+        \lstinline|map|: \tau_9 = \lstinline|map|
+      \end{gather}
+      We can choose to separately label \lstinline|x|, \lstinline|l|, and
+      \lstinline|map|, but it does not make any difference to the result.
+
+      \item
+      Inserting the type of \lstinline|map| (thus removing \(\tau_9\)), and
+      adding constraints by looking at the top-level of each subterm, we can get
+      the set of initial constraints, labelled by the subterm equation above
+      they come from:
+      \begin{gather*}
+        \tau = \tau_7 ~\ato~ \tau_1 \tag{1} \\
+        \tau_1 = \alist{\tau_3} \tag{2, 4} \\
+        \tau_7 = \alist{\tau_8} \tag{2, 9} \\
+        \tau_2 = \tau_8 ~\ato~ \tau_3 \tag{3} \\
+        \tau_3 = \aint \tag{4} \\
+        \tau_4 = \aint \tag{4} \\
+        \tau_5 = \aint \tag{4} \\
+        \tau_6 = \tau_5 ~\ato~ \tau_4 \tag{5} \\
+        \tau_8 = (\tau_5', \tau_5) \tag{6} \\
+        \tau_8 = (\tau_6, \tau_6') \tag{7}
+      \end{gather*}
+      for fresh type variables \(\tau_5'\) and \(\tau_6'\) arising from the rule
+      for pairs.
+
+      \item 
+      The constraints can be solved step-by-step (major steps shown):
+      \begin{enumerate}
+        \item Eliminating known types (\(\tau_3, \tau_4, \tau_5\)):
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \tau_1  \\
+          \tau_1 = \alist{\aint} \\
+          \tau_7 = \alist{\tau_8} \\
+          \tau_2 = \tau_8 ~\ato~ \aint  \\
+          \tau_6 = \aint ~\ato~ \aint \\
+          \tau_8 = (\tau_5', \aint) \\
+          \tau_8 = (\tau_6, \tau_6')
+        \end{gather*}
+        \item Eliminating \(\tau_1, \tau_6\):
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{\tau_8} \\
+          \tau_2 = \tau_8 ~\ato~ \aint  \\
+          \tau_8 = (\tau_5', \aint) \\
+          \tau_8 = (\aint ~\ato~ \aint, \tau_6')
+        \end{gather*}
+        \item Eliminating \(\tau_8\) using either of its equations:
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{(\tau_5', \aint)} \\
+          \tau_2 = (\tau_5', \aint) ~\ato~ \aint  \\
+          (\tau_5', \aint) = (\aint ~\ato~ \aint, \tau_6')
+        \end{gather*}
+        \item Performing unification of the pair type:
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{(\tau_5', \aint)} \\
+          \tau_2 = (\tau_5', \aint) ~\ato~ \aint  \\
+          \tau_5' = \aint ~\ato~ \aint \\
+          \aint  = \tau_6'
+        \end{gather*}
+        \item Eliminating \(\tau_5'\) and \(\tau_6'\):
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{(\aint ~\ato~ \aint, \aint)} \\
+          \tau_2 = (\aint ~\ato~ \aint, \aint) ~\ato~ \aint
+        \end{gather*}
+        \item Eliminating \(\tau_2, \tau_7\):
+        \begin{gather*}
+          \tau = \alist{(\aint ~\ato~ \aint, \aint)} ~\ato~ \alist{\aint}
+        \end{gather*}
+        \item Finally, all type variables are assigned, as we eliminate \(\tau\):
+        \begin{gather*}
+          \emptyset \text{ (no constraints left)}
+        \end{gather*}
+      \end{enumerate}
+
+      The type of \(t\) as discovered by the unification process is:
+      \begin{gather*}
+        \tau = \alist{(\aint ~\ato~ \aint, \aint)} ~\ato~ \alist{\aint}
+      \end{gather*}
+    \end{enumerate}
+  \end{solution}
+
+\end{exercise}

info/exercises/src/ex-05/ex/program.tex

+
+\begin{exercise}{}
+
+  A \emph{program} is a top-level expression \(t\) accompanied by a set of
+  user-provided function definitions. The program is well-typed if each of the
+  function bodies conform to the type of the function, and the top-level
+  expression is well-typed in the context of the function definitions.
+
+  For each of the following function definitions, check whether the function
+  body is well-typed:
+  %
+  \begin{enumerate}
+    \item \lstinline|def f(x: Int, y: Int): Bool =  x <= y|
+    \item \lstinline|def rec(x: Int): Int =  rec(x)|
+    \item \lstinline|def fib(n: Int): Int = if n <=  1 then 1 else (fib(n - 1)  + fib(n - 2))|
+  \end{enumerate}
+
+  \begin{solution}
+    \begin{enumerate}
+      \item Well-typed, apply rule \(Leq\).
+      \item Well-typed. We need to check if the body conforms to the output
+      type, if we know the function and its parameters have their ascribed type.
+      So, under the context \lstinline|rec: Int => Int, x: Int|, we need to
+      prove that \lstinline|rec(x): Int|. This follows from the \(app\) rule.
+
+      So, if we allow recursion and do not check for termination, we can prove
+      unexpected things using the non-terminating programs.
+      \item Well-typed. We need to produce a derivation of the following:
+      \begin{equation*}
+        \lstinline|fib: Int => Int|, \lstinline|n: Int| \vdash \lstinline|if n <=  1 then 1 else (fib(n - 1)  + fib(n - 2)): Int|
+      \end{equation*} 
+      i.e., given that \lstinline|fib| inductively has type \lstinline|Int => Int| and
+      the parameter \lstinline|n| has type \lstinline|Int|, we need to prove that the
+      body of the function has the ascribed type \lstinline|Int|.
+       
+      The derivation can be constructed by following the structure of the term
+      on the right-hand side, the body. We set \(\Gamma = 
+      %
+      \lstinline|fib: Int => Int|, \lstinline|n: Int|\) for brevity. The \lstinline|n-2|
+      branch is skipped due to space and being the same as the \lstinline|n-1| branch.
+      \begin{equation*}
+        \hspace*{-4cm}
+        \AxiomC{\((\lstinline|n|, \aint) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|n: Int|\)}
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+        \BinaryInfC{\(\Gamma \vdash \lstinline|n <= 1: Bool|\)}
+        %
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+        %
+        \AxiomC{\((\lstinline|fib, Int => Int|) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|fib: Int => Int|\)}
+        \AxiomC{\((\lstinline|n|, \aint) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|n: Int|\)}
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+        \BinaryInfC{\(\Gamma \vdash \lstinline|(n - 1): Int|\)}
+        \BinaryInfC{\(\Gamma \vdash \lstinline|fib(n - 1): Int|\)}
+        %
+        \AxiomC{\ldots}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|fib(n - 2): Int|\)}
+        %
+        \BinaryInfC{\(\Gamma \vdash \lstinline|fib(n - 1) + fib(n - 2): Int|\)}
+        %
+        \TrinaryInfC{\(\Gamma \vdash \lstinline|if n <=  1 then 1 else (fib(n - 1)  + fib(n - 2)): Int|\)}
+        \DisplayProof
+      \end{equation*}
+    \end{enumerate}
+    
+  \end{solution}
+  
+\end{exercise}

info/exercises/src/ex-05/ex/rec-inf.tex

+
+
+\pagebreak
+\begin{exercise}{}
+
+  Consider the following definition for a recursive function \(g\):
+
+  \begin{equation*}
+    \lstinline|def g(n, x)  = if n <=  2 then (x, x)  else (x, g(n - 1, x))|
+  \end{equation*}
+
+  \begin{enumerate}
+    \item Evaluate \(g(3, 1)\) and \(g(4, 2)\) using the definition of \(g\).
+      Suggest a type for the function \(g\) based on your observations.
+    \item Label and assign type variables to the definition parameters, body,
+      and its subterms.
+    \item Generate the constraints on the type variables, assuming the
+      definition of \(g\) is well-typed.
+    \item Attempt to solve the generated constraints via unification. Argue how
+    the result correlates to your observations from evaluating \(g\).
+  \end{enumerate}
+  
+  \begin{solution}
+    \begin{enumerate}
+      \item \lstinline|g(3, 1)| evaluates to \lstinline|(1, (1, 1))| and
+      \lstinline|g(4, 2)| evaluates to \lstinline|(2, (2, (2, 2)))|. Notably,
+      these two come from disjoint types. This suggests that the function \(g\)
+      is not well-typed.
+      \item We can label the parameters, subterms, and assign a type to the
+      function:
+      \setcounter{equation}{0}
+      \begin{gather}
+        \lstinline|g|: \tau \\
+        \lstinline|n|: \tau_n \\
+        \lstinline|x|: \tau_x \\
+        body: \tau_1 = \lstinline|if n <=  2 then (x, x)  else (x, g(n - 1, x))| \\
+        t_1: \tau_2 = \lstinline|n <=  2| \\
+        t_2: \tau_3 = \lstinline|(x, x)| \\
+        t_3: \tau_4 = \lstinline|(x, g(n - 1, x))| \\
+        t_4: \tau_5 = \lstinline|g(n - 1, x)| \\
+        t_5: \tau_6 = \lstinline|n - 1|
+      \end{gather}
+      \item We can generate the constraints by looking at the top-level of each
+      subterm equation:
+      \begin{gather*}
+        \tau = \tau_n ~\ato~ \tau_x ~\ato~ \tau_1 \tag{1, def} \\
+        \tau_1 = \tau_3 \tag{4} \\
+        \tau_1 = \tau_4 \tag{4} \\
+        \tau_2 = \abool \tag{4} \\
+        \tau_n = \aint \tag{5} \\
+        \tau_3 = (\tau_x, \tau_x) \tag{6} \\
+        \tau_4 = (\tau_x, \tau_5) \tag{6} \\
+        \tau_5 = \tau_1 \tag{7, def} \\
+        \tau_6 = \aint \tag{9}
+      \end{gather*}
+      \item The constraints can be solved (eliminating \(\tau_4, \tau_5\)) to
+      reach a set of constraints containing the recursive constraint \(\tau_1 =
+      (\tau_x, \tau_1)\). There is no type \(\tau_1\) (the output type of
+      \lstinline|g|!) satisfying this. 
+
+      This matches our previous observation where \lstinline|g| produced two
+      different sized tuples as its output. 
+    \end{enumerate}
+  \end{solution}
+  
+\end{exercise}
\ No newline at end of file

info/exercises/src/ex-05/ex/system.tex

+
+% we want lists, pairs
+% both parametric
+% we want some functions, as well as function definitions
+% we want to be able to define and typecheck recursive functions
+
+Consider a type system for a simple functional language, consisting of integers,
+booleans, parametric pairs, and lists. The rest of the exercises will revolve
+around this system.
+
+% language components
+\newcommand{\aint}{\lstinline|int|}
+\newcommand{\abool}{\lstinline|bool|}
+\newcommand{\aif}{\lstinline|if|}
+\newcommand{\athen}{\lstinline|then|}
+\newcommand{\aelse}{\lstinline|else|}
+\newcommand{\apair}[2]{(#1, #2)}
+\newcommand{\afst}[1]{\lstinline|fst|(#1)}
+\newcommand{\asnd}[1]{\lstinline|snd|(#1)}
+\newcommand{\alist}[1]{\lstinline|List[|#1\lstinline|]|}
+\newcommand{\anil}{\lstinline|Nil()|}
+\newcommand{\acons}[2]{\lstinline|Cons(|#1, #2\lstinline|)|}
+\newcommand{\ato}{\lstinline|=>|}
+
+%%% Actual type system
+\begin{gather*}
+  % variables
+  \AxiomC{\((x, \tau) \in \Gamma\)}
+  \RightLabel{(var)}
+  \UnaryInfC{\(\Gamma \vdash x : \tau\)}
+  \DisplayProof \\
+  % integers
+  \AxiomC{\(n\) is an integer value}
+  \RightLabel{(int)}
+  \UnaryInfC{\(\Gamma \vdash \num(n) : \aint\)}
+  \DisplayProof \\
+  % + -
+  \AxiomC{\(e_1 : \aint\)}
+  \AxiomC{\(e_2 : \aint\)}
+  \RightLabel{(+)}
+  \BinaryInfC{\(\Gamma \vdash e_1 + e_2 : \aint\)}
+  \DisplayProof \qquad
+  \AxiomC{\(e_1 : \aint\)}
+  \AxiomC{\(e_2 : \aint\)}
+  \RightLabel{(-)}
+  \BinaryInfC{\(\Gamma \vdash e_1 - e_2 : \aint\)}
+  \DisplayProof \\
+  % booleans
+  \AxiomC{\(b\) is a boolean value}
+  \RightLabel{(bool)}
+  \UnaryInfC{\(\Gamma \vdash \abool(b) : \abool\)}
+  \DisplayProof \\
+  % props
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \abool\)}
+  \RightLabel{(and)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \land e_2 : \abool\)}
+  \DisplayProof \qquad
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \abool\)}
+  \RightLabel{(or)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \lor e_2 : \abool\)}
+  \DisplayProof \\
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \RightLabel{(not)}
+  \UnaryInfC{\(\Gamma \vdash \neg e_1 : \abool\)}
+  \DisplayProof \\
+  % ite
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \tau\)}
+  \AxiomC{\(\Gamma \vdash e_3 : \tau\)}
+  \RightLabel{(ite)}
+  \TrinaryInfC{\(\Gamma \vdash \aif \, e_1 \, \athen \, e_2 \, \aelse \, e_3 : \tau\)}
+  \DisplayProof \\
+  % pairs
+  \AxiomC{\(\Gamma \vdash e_1 : \tau_1\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \tau_2\)}
+  \RightLabel{(pair)}
+  \BinaryInfC{\(\Gamma \vdash \apair{e_1}{e_2} : \apair{\tau_1}{\tau_2}\)}
+  \DisplayProof \\
+  % fst
+  \AxiomC{\(\Gamma \vdash e : \apair{\tau_1}{\tau_2}\)}
+  \RightLabel{(fst)}
+  \UnaryInfC{\(\Gamma \vdash \afst{e} : \tau_1\)}
+  \DisplayProof \qquad
+  % snd
+  \AxiomC{\(\Gamma \vdash e : \apair{\tau_1}{\tau_2}\)}
+  \RightLabel{(snd)}
+  \UnaryInfC{\(\Gamma \vdash \asnd{e} : \tau_2\)}
+  \DisplayProof \\
+  % lists
+  \AxiomC{\phantom{\(e \in \alist{\tau}\)}}
+  \RightLabel{(nil)}
+  \UnaryInfC{\(\Gamma \vdash \anil : \alist{\tau}\)}
+  \DisplayProof \qquad
+  \AxiomC{\(\Gamma \vdash e_1 : \tau\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \alist{\tau}\)}
+  \RightLabel{(cons)}
+  \BinaryInfC{\(\Gamma \vdash \acons{e_1}{e_2} : \alist{\tau}\)}
+  \DisplayProof \\
+  % functions
+  \AxiomC{\(\Gamma, x : \tau_1 \vdash e : \tau_2\)}
+  \RightLabel{(fun)}
+  \UnaryInfC{\(\Gamma \vdash \lambda x : \tau_1 ~\ato~ e : \tau_1 ~\ato~ \tau_2\)}
+  \DisplayProof \qquad
+  % application
+  \AxiomC{\(\Gamma \vdash e_1 : \tau_1 ~\ato~ \tau_2\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \tau_1\)}
+  \RightLabel{(app)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \, e_2 : \tau_2\)}
+  \DisplayProof \\
+\end{gather*}

info/exercises/src/ex-05/main.tex

+\documentclass[a4paper]{article}
+
+\input{../macro}
+
+\ifdefined\ANSWERS
+  \if\ANSWERS1
+    \printanswers
+  \fi
+\fi
+
+\DeclareMathOperator{\half}{half}
+\newcommand{\num}{\ensuremath{\mathbf{num}}}
+
+\title{CS 320 \\ Computer Language Processing\\Exercise Set 5}
+\author{}
+\date{April 02, 2025}
+
+\begin{document}
+\maketitle
+
+% type system
+% do some type checking
+% some unification
+% some inference
+\input{ex/system}
+
+\input{ex/check}
+
+\input{ex/program}
+
+\input{ex/map}
+
+\input{ex/rec-inf}
+
+\end{document}