Contents
1 Introduction
2 Useful GHCi Notes
3 Google? Hoogle!
4 Proofs
1 1 2
3
Tutorial 03
Jason Balaci January 29, 2021
4.1 InductiononN…………………………………….. 3 4.2 Onemoretime,forthelists!………………………………. 3 4.3 Lengths(fromTutorial02)! ………………………………. 3
5 Mathematical Expressions 5
5.1 Let’saddMonus!……………………………………. 5
6 More expressions! 6
1 Introduction
module Tutorial 03 where import Data.List (intersperse)
import Prelude hiding (length) main :: IO ()
main = putStrLn “Hello, world!”
2 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.
:type
1
3
:reload will reload your currently loaded modules
:help will show you list of commands available to you
:load
:quit will exit the GHCi
: will repeat the last command you executed
:!
Useful examples of :type
— 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!
Google? Hoogle!
Much like Google is a search engine to the internet, Hoogle is our Haskell API search engine.
We can search general things, like map, filter, id, const, ++, and more!
We can also search for things according to their types!
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 id!
The source code also has nice syntax highlighting and shows informative tooltips (including type
definitions, hyperlinks to definitions, and more!).
2
4 Proofs
4.1 Induction on N
ForanypredicateP :N→B,P(0)∧(∀k:N.P(k) =⇒ P(k+1)) =⇒ P(n) A general schema:
By induction on n : N:
Base case: Prove that P(0) holds!
Proof for P(0)
Induction Step: Assume P (n), and show that P (n) =⇒ P (n + 1)
Proof for P (n + 1), assuming induction hypothesis P (n) holds! ∴ P holds for all natural numbers!
4.2 One more time, for the lists!
For any predicate P : [a] → B, P ([]) ∧ (∀xs :[a].∀x : a.P (xs) =⇒ P ((x : xs)) =⇒ ∀xs :[a].P (xs) A general schema:
By induction on xs :[a]:
Base case: Prove that P([]) holds!
Proof for P([])
Induction Step: Assume P (xs), and show that P (xs) =⇒ P ((x : xs))
Proof for P ((x : xs)), assuming induction hypothesis P (xs) holds! ∴ P holds for all lists!
4.3 Lengths (from Tutorial 02)!
First, let us define length!
length :: [ a ] → Int
length [ ] = 0 — length.1 length (x : xs) = length xs + 1 — length.2
Let’s us also recall how ++ works! (From ’base’ source code)
(++) :: [a] -> [a] -> [a]
(++) [] ys = ys — ++.1
(++) (x:xs) ys = x : xs ++ ys — ++.2
How can we prove that ∀ xs, ys . length (xs ++ ys) = length xs + length ys?
3
Proof. ∀ xs, ys . length (xs ++ ys) = length xs + length ys We will use induction on xs.
Base Case: []
Our goal is length ([] ++ ys) = length [] + length ys.
length ([] ++ ys) = {++.1}
length ys
= { Identity of + }
0 + length ys = { length.1 }
length [] + length ys
∴ our base case holds! Now let’s check out our induction step! Induction Step: (x:xs)
Recall our induction hypothesis: ∀ xs, ys . length (xs ++ ys) = length xs + length ys Our goal is length ((x:xs) ++ ys) = length (x:xs) + length ys
LHS:
RHS:
= = =
= =
length ((x:xs) ++ ys) {++.2}
length (x:(xs ++ ys)) { length.2 }
length (xs ++ ys) + 1
{ ind. hyp. }
length xs + length ys + 1
length (x:xs) + length ys { length.2 }
length xs + 1 + length ys { commutativity }
length xs + length ys + 1
∴ we have shown LHS = RHS, and hence our inductive proof holds.
As such, we have shown that ∀ xs, ys . length (xs ++ ys) = length xs + length ys holds!
4
5
Mathematical Expressions
— 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
Let’s add Monus!
5.1
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 monus y where x < y, then x monus y = 0, otherwise, x monus y = x − y. Alternatively, x monus y = max(0, x − y)).
data Expr′ = Lit′ Integer
| Add′ Expr′ Expr′
| Sub′ Expr′ Expr′
| Monus′ Expr′ Expr′
eval ′ :: Expr ′ → Integer
eval′ (Lit′ i) = i
eval′ (Add′ a b) = eval′ a + eval′ b
eval′ (Sub′ a b) = eval′ a − eval′ b
eval′ (Monus′ a b) = max 0 (eval′ a − eval′ b)
-- *Tutorial_03> eval’ (Monus’ (Lit’ 10) (Lit’ 3))
— 7
— *Tutorial_03> eval’ (Monus’ (Lit’ 10) (Lit’ 10000)) — 0
Can we check if an expression contains a Monus’ operation? Yes!
hasMonus :: Expr ′ → Bool hasMonus (Lit′ i) = False
5
6
hasMonus (Add′ a b) = hasMonus a ∨ hasMonus b hasMonus (Sub′ a b) = hasMonus a ∨ hasMonus b hasMonus (Monus′ a b) = True
— *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
More expressions!
data Expr2 = Lit2 Integer | Add2 [Expr2 ]
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.
— Some useful functions for working with lists:
— * sum – sum of all values in a list
— (e.g., sum [1,2,3] = 6) —
— * 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]) —
— * filter – get only elements of a list according to some predicate rule
— (e.g., filter (\x -> x > 10) [1..13] = [11,12,13]) —
— * elem – ”contains”-like operation
— (e.g., elem 1 [2,3,4,1] = True) —
— * maximum – gets the maximum element of a list
— (e.g., maximum [3,2,10] = 10) —
— * minimum – gets the minimum element of a list
— (e.g., minimum [3,2,10] = 2) —
— * foldl and foldr – left/right associative folds of a structure into a single value (seen in class) —
— * concat – concatenates a list of lists into a single list
— (e.g., concat [“a”, “bcdefg”] = “abcdefg”) —
— * intersperse (imported from Data.List) – takes an element and a list,
— and “intersperses” the value between each value in the list
6
—
— Have a look at the Haskell documentation for Data.List!
— Note: you may need to import Data.List
— Finally, we can write our ”view” function!
view :: Expr2 → String
view (Lit2 a) = show a
view (Add2 ts) = concat (intersperse ” + ” (map (view) 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 []) — “”
7