diff --git a/info/exercises/ex-05-sol.pdf b/info/exercises/ex-05-sol.pdf index 5b47aca822f60a4d2f4c7b321f48f3cf0134e080..29547edfa18155f1338f4250393965761aeb524f 100644 Binary files a/info/exercises/ex-05-sol.pdf and b/info/exercises/ex-05-sol.pdf differ diff --git a/info/exercises/ex-05.pdf b/info/exercises/ex-05.pdf index 355627556465d0f4378f51da10258130bb6b96ed..a02b25a98d7fddfa38dcf3d9b2b3370ab920c5a8 100644 Binary files a/info/exercises/ex-05.pdf and b/info/exercises/ex-05.pdf differ diff --git a/info/exercises/src/ex-05/ex/map.tex b/info/exercises/src/ex-05/ex/map.tex index 7c487fc7b7c117eea6831e637ab486a33e6c6aa2..2bcd54711077a5e8bfcb6c37b3a63e893416d39e 100644 --- a/info/exercises/src/ex-05/ex/map.tex +++ b/info/exercises/src/ex-05/ex/map.tex @@ -3,7 +3,7 @@ Consider the following term \(t\): % \begin{center} - \(t = \) \lstinline{l => map(l, x => fst(x)(snd(x)) + snd(x))} + \(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} @@ -21,8 +21,8 @@ \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: \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))| \\ diff --git a/info/exercises/src/ex-05/ex/program.tex b/info/exercises/src/ex-05/ex/program.tex index 137669d10e938a4c7dec1f329cc90fe36953acc2..da325c633a7fcc39d88dbaa26c48be1aba890371 100644 --- a/info/exercises/src/ex-05/ex/program.tex +++ b/info/exercises/src/ex-05/ex/program.tex @@ -10,7 +10,7 @@ body is well-typed: % \begin{enumerate} - \item \lstinline|def f(x: Int, y: Int): Bool = x <= y| + \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} diff --git a/info/exercises/src/ex-05/ex/rec-inf.tex b/info/exercises/src/ex-05/ex/rec-inf.tex index c5364bbf63032dbcf9f172761def4e9fe958fe00..9f2523a10fcf203e88f2af676d574b35b01102cd 100644 --- a/info/exercises/src/ex-05/ex/rec-inf.tex +++ b/info/exercises/src/ex-05/ex/rec-inf.tex @@ -6,11 +6,11 @@ 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))| + \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\). + \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. @@ -22,8 +22,8 @@ \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, + \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 @@ -33,11 +33,11 @@ \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))| \\ + 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_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