\documentclass{article}
\usepackage[left=1in,right=1in]{geometry}
\usepackage{scrextend}
\usepackage{color}
\usepackage{hyperref}
\usepackage{url}
\usepackage{amsfonts}
\usepackage{amsmath,amssymb}
\usepackage{amsthm}
%include polycode.fmt
%options ghci
%Credits to Musa Al-hassy for the below scripts!!!%
\def\stepWith#1#2{ \\ #1 & \quad \color{black}{\{\;\text{#2}\;\}} \\ & }
\def\step#1{ \stepWith{\equiv}{#1} }
\def\commentbegin{\quad\{\ }
\def\commentend{\}}
\def\stepEq#1{ \stepWith{=}{#1} }
\begin{document}
\title{Tutorial 03}
\author{Jason Balaci}
\date{\today}
\maketitle
\tableofcontents
\section{Introduction}
\begin{code}
module Tutorial_03 where
import Data.List ( intersperse )
import Prelude hiding ( length )
main :: IO ()
main = putStrLn “Hello, world!”
\end{code}
\section{Useful GHCi Notes}
With GHCi open in your terminal, we can do some neat things to make our development experience a little bit more comfortable.
\begin{itemize}
\item @:type
\item @:reload@ will reload your currently loaded modules
\item @:help@ will show you list of commands available to you
\item @:load
\item @:quit@ will exit the GHCi
\item @:@ will repeat the last command you executed
\item @:!
\end{itemize}
\textbf{Useful examples of} @:type@
\begin{code}
— What’s the type of sum ?
— You can check! Execute “:type sum” in your terminal!
—
— What’s the type of + ?
— You can check! Execute “:type (+)” in your terminal!
—
— What’s the type of ++ ?
— You can check! Execute “:type (++)” in your terminal!
—
— What’s the type of \&\& ?
— You can check! Execute “:type (\&\&)” in your terminal!
—
— While you can also also use Hoogle to examine things, at times Hoogle does not contain
— information about things. For example, it does not contain information about things
— that you constructed or of libraries that aren’t listen on Hackage!
—
— I wonder what other operators we can examine with this!
\end{code}
\section{Google? Hoogle!}
Much like Google is a search engine to the internet, \href{https://hoogle.haskell.org/}{Hoogle} is our Haskell API search engine.
\begin{itemize}
\item We can search general things, like
\href{https://hoogle.haskell.org/?hoogle=map}{\texttt{map}},
\href{https://hoogle.haskell.org/?hoogle=filter}{\texttt{filter}},
\href{https://hoogle.haskell.org/?hoogle=id}{@id@},
\href{https://hoogle.haskell.org/?hoogle=const}{\texttt{const}},
\href{https://hoogle.haskell.org/?hoogle=%2B%2B}{\texttt{++}}, and more!
\item We can also search for things according to their types!
\item We can also view the source code for many things by clicking specific Hackage links and then using the “source” links on the right hand side. Check out the source code for \href{https://hackage.haskell.org/package/base-4.14.1.0/docs/src/GHC.Base.html#id}{@id@}!
\item The source code also has nice syntax highlighting and shows informative tooltips (including type definitions, hyperlinks to definitions, and more!).
\end{itemize}
\section{Proofs}
\subsection{Induction on $\mathbb{N}$}
For any predicate $P : \mathbb{N} \rightarrow \mathbb{B}$, $P(0) \land (\forall k : \mathbb{N} . P(k) \implies P(k+1)) \implies P(n)$\\
A general schema:
\textbf{By induction on} $n : \mathbb{N}$:\\
\textbf{Base case}: Prove that $P(0)$ holds!
\textit{Proof for} $P(0)$\\
\textbf{Induction Step}: Assume $P(n)$, and show that $P(n) \implies P(n+1)$
\textit{Proof for $P(n+1)$, assuming induction hypothesis $P(n)$ holds!}\\
$\therefore P$ holds for all natural numbers!
\subsection{One more time, for the lists!}
For any predicate $P : [a] \rightarrow \mathbb{B}$, $P($@[]@$) \land (\forall xs : $@[a]@$ . \forall x : a . P(xs) \implies P((x:xs)) \implies \forall xs : $@[a]@$ . P(xs)$\\
A general schema:
\textbf{By induction on} $xs : $@[a]@:\\
\textbf{Base case}: Prove that $P($@[]@$)$ holds!
\textit{Proof for} $P($@[]@$)$\\
\textbf{Induction Step}: Assume $P(xs)$, and show that $P(xs) \implies P((x:xs))$
\textit{Proof for $P((x:xs))$, assuming induction hypothesis $P(xs)$ holds!}\\
$\therefore P$ holds for all lists!
\subsection{Lengths (from Tutorial 02)!}
First, let us define @length@!
\begin{code}
length :: [a] -> Int
length [] = 0 — length.1
length (x:xs) = length xs + 1 — length.2
\end{code}
Let’s us also recall how @++@ works! (From \href{https://hackage.haskell.org/package/base-4.8.0.0/docs/src/GHC-Base.html#%2B%2B}{‘base’ source code})\\
@(++) :: [a] -> [a] -> [a]@
@(++) [] ys = ys — ++.1@
@(++) (x:xs) ys = x : xs ++ ys — ++.2@\\
How can we prove that $\forall$ @xs, ys . length (xs ++ ys) = length xs + length ys@?\\
\begin{proof} $\forall$ @xs, ys . length (xs ++ ys) = length xs + length ys@\\
We will use induction on @xs@.\\
\textbf{Base Case}: @[]@
Our goal is @length ([] ++ ys) = length [] + length ys@.
\begin{align*}&
@length ([] ++ ys)@
\stepEq{@…@}
@…@
\stepEq{@…@}
@…@
\stepEq{@…@}
@…@
\end{align*}
$\therefore$ our base case holds! Now let’s check out our induction step!\\
\textbf{Induction Step}: @(x:xs)@
Recall our induction hypothesis: $\forall $ @xs, ys . length (xs ++ ys) = length xs + length ys@\\
Our goal is @length ((x:xs) ++ ys) = length (x:xs) + length ys@\\
LHS:
\begin{align*}&
@length ((x:xs) ++ ys)@
\stepEq{@…@}
@…@
\stepEq{@…@}
@…@
\stepEq{…}
@…@
\end{align*}
RHS:
\begin{align*}&
@length (x:xs) + length ys@
\stepEq{@…@}
@…@
\stepEq{@…@}
@…@
\end{align*}
$\therefore$ we have shown LHS = RHS, and hence our inductive proof holds.\\
As such, we have shown that $\forall$ @xs, ys . length (xs ++ ys) = length xs + length ys@ holds!
\end{proof}
\section{Mathematical Expressions}
\begin{code}
— Math expression langauge from Jan28.lhs
data Expr =
Lit Integer
| Expr :+: Expr
| Expr :-: Expr
deriving Show
eval :: Expr -> Integer
eval (Lit i) = i
eval (e1 :+: e2) = eval e1 + eval e2
eval (e1 :-: e2) = eval e1 – eval e2
ee1, ee2, ee3, ee4 :: Expr
ee1 = Lit 5 :+: (Lit 6 :-: Lit 12)
ee2 = (Lit 5 :+: Lit 6) :-: Lit 12
ee3 = (Lit 5 :+: Lit 6) :+: Lit 12
ee4 = (ee3 :+: ee3) :+: ee3
\end{code}
\subsection{Let’s add Monus!}
Let’s create a language @Expr’@ that has the same functionality as @Expr@
but does not use infix data structures.
Additionally, we would like to add the @Monus’@ operation where monus is
defined as subtraction of the natural numbers (same operation as on the
integers but no negative numbers exist, so if you’ve got an expression
$x$ \texttt{monus} $y$ where $x < y$, then $x$ \texttt{monus} $y = 0$, otherwise, $x$ \texttt{monus} $y = x - y$.
Alternatively, $x$ \texttt{monus} $y = max (0, x - y)$).
\begin{code}
data Expr' =
Lit' Integer
| Add' Expr' Expr'
| Sub' Expr' Expr'
| Monus' Expr' Expr'
-- Just like above, our evaluation function!
eval' :: Expr' -> Integer
eval’ (Lit’ i) = i
eval’ (Add’ a b) = eval’ a + eval’ b
eval’ (Sub’ a b) = eval’ a – eval’ b
— TODO!!!!
— eval’ (Monus’ a b) = …
— @*Tutorial_03> eval’ (Monus’ (Lit’ 10) (Lit’ 3))@
— @7@
— @*Tutorial_03> eval’ (Monus’ (Lit’ 10) (Lit’ 10000))@
— @0@
\end{code}
\textbf{Can we check if an expression contains a Monus’ operation? Yes!}
\begin{code}
— hasMonus :: Expr’ -> Bool
— hasMonus (Lit’ i) = …
— hasMonus (Add’ a b) = …
— hasMonus (Sub’ a b) = …
— hasMonus (Monus’ a b) = …
— @*Tutorial_03> hasMonus (Monus’ (Lit’ 10) (Lit’ 3))@
— @True@
— @*Tutorial_03> hasMonus (Add’ (Lit’ 1) (Monus’ (Lit’ 10) (Lit’ 3)))@
— @True@
— @*Tutorial_03> hasMonus (Add’ (Lit’ 1) (Sub’ (Lit’ 10) (Lit’ 3)))@
— @False@
\end{code}
\section{More expressions!}
\begin{code}
data Expr2 = Lit2 Integer | Add2 [Expr2]
\end{code}
\textbf{Can we view this Expr2 as a string? Yes!}
But we’re going to have to work with lists, so we might be interested in first learning about some of the standard Haskell library functions we can use.
\begin{code}
— Some useful functions for working with lists:
— * \textbf{sum} – sum of all values in a list
— (e.g., @sum [1,2,3] = 6@)
—
— * \textbf{map} – apply a function to all values of a list
— (e.g., @map (\x -> x * 2) [1,2,3,4,5] = [2,4,6,8,10]@)
—
— * \textbf{filter} – get only elements of a list according to some predicate rule
— (e.g., @filter (\x -> x > 10) [1..13] = [11,12,13]@)
—
— * \textbf{elem} – “contains”-like operation
— (e.g., @elem 1 [2,3,4,1] = True@)
—
— * \textbf{maximum} – gets the maximum element of a list
— (e.g., @maximum [3,2,10] = 10@)
—
— * \textbf{minimum} – gets the minimum element of a list
— (e.g., @minimum [3,2,10] = 2@)
—
— * \textbf{foldl} and \textbf{foldr} – left/right associative folds of a structure into a single value (seen in class)
—
— * \textbf{concat} – concatenates a list of lists into a single list
— (e.g., @concat [“a”, “bcdefg”] = “abcdefg”@)
—
— * \textbf{intersperse} (imported from Data.List) – takes an element and a list,
— and “intersperses” the value between each value in the list
—
— \href{https://hackage.haskell.org/package/base-4.14.1.0/docs/Data-List.html}{Have a look at the Haskell documentation for Data.List!}
— \textit{Note: you may need to import Data.List }
— Finally, we can write our “view” function!
— view :: Expr2 -> String
— view (Lit2 a) = …
— view (Add2 ts) = …
— @*Tutorial_03> a = Add2 [Lit2 1, Lit2 2, Lit2 3]@
— @*Tutorial_03> view a@
— @”1 + 2 + 3″@
— @*Tutorial_03> a = Add2 [Lit2 1, Lit2 2, Lit2 3, Add2 [Lit2 4, Lit2 5, Lit2 6]]@
— @*Tutorial_03> view a@
— @”1 + 2 + 3 + 4 + 5 + 6″@
— @*Tutorial_03> view (Add2 [])@
— @””@
\end{code}
\end{document}