It is best to think of Haskell functions as math functions, not as C or Python functions; likewise, Haskell variables as math variables (for unknowns and constants), not as C or Python variables (mutable state).
Because of this, you will hear me say “f(4) equals/gives 10” not “returns 10”, “codomain” not “return type”, “apply this function to that parameter” (plugging in) not “call this function”. Both angles are correct, you don't have to speak like me, but the algebra angle is better for beginners than the control-flow angle.
This example takes two integer parameters and gives an integer answer:
diffSq :: Integer -> Integer -> Integer diffSq x y = (x - y) * (x + y)in HaskellBasics.hs
How to use: diffSq 2 1
There is a bit more theory on types like X -> Y -> Z
in a later
lecture.
Two ways of local definitions:
diffSqV3a, diffSqV3b :: Integer -> Integer -> Integer diffSqV3a x y = let minus = x - y plus = x + y in minus * plus diffSqV3b x y = minus * plus where minus = x - y plus = x + yin HaskellBasics.hs
The difference:
“let
-in
” is an expression, can be used
wherever an expression is expected, e.g, 2 * (let x=5 in
x+1)
“where
” is not part of an expression, e.g., “2 * (x+1
where x=5)
” is illegal. It is part of a definition, e.g., “y =
... where x=5
” is legal. There is another place you can use
“where
”, shown in slowFib2
in the next section.
slowFactorial :: Integer -> Integer slowFactorial 0 = 1 slowFactorial n = n * slowFactorial (n - 1) -- Slow Fibonacci (yawn) to show you can have more patterns. slowFib :: Integer -> Integer slowFib 0 = 0 slowFib 1 = 1 slowFib n = slowFib (n-1) + slowFib (n-2) -- More fundamental form---using a "case-of" expression: slowFib2 :: Integer -> Integer slowFib2 x = case x of 0 -> 0 1 -> 1 n -> slowFib2 n1 + slowFib2 n2 where n1 = n - 1 n2 = n - 2 -- The other example of "where". This one is part of "n -> ...".in HaskellBasics.hs
Can you use if-then-else for these examples? Guards? Yes.
You will see something like this all the time:
f (x*2 + 1) :: Integer
This is notation for “the type of f (x*2 + 1)
is Integer
”. It is used in both actual code and explanation
prose.
Those two things are called:
f (x*2 + 1) :: Integer ^^^^^^^^^^^ ^^^^^^^ term type
One more example:
h . g :: Char -> Bool ^^^^^ ^^^^^^^^^^^^ term type
“term” is also widely known as “expression”. I like “term” because it is shorter, and because “type” is also called “type expression”.
What about “value”? Answer: 5+4
is a term; the result of
evaluating it, 9, is a value. But I am lax about this.
(How to create code vs how to run code.)
Everyone teaches how to run recursive code. That still doesn't help you with writing. (Probably impedes you actually --- hand-running recursive code is distracting.)
I teach you both. I show you that writing recursive code can be easier if you don't try to run it.
Synthesis view (how I write recursive code): Pretend induction = Use induction to prove something that still contains unknowns, ah but during the proof you find out how to solve for the unknowns!
How I coded up slowFactorial:
WTP: For all natural n: slowFactorial n = n!
Base case:
WTP: slowFactorial 0 = 0!
Notice 0! = 1, so if I code up
slowFactorial 0 = 1
I get slowFactorial 0 = 0!
Induction step:
Let natural n ≥ 1 be given.
Induction hypothesis: slowFactorial (n-1) = (n-1)!
WTP: slowFactorial n = n!
Notice
n! = n*(n-1)! = n * slowFactorial (n-1) by I.H.
So if I code up
slowFactorial n = n * slowFactorial (n-1)
I get slowFactorial n = n!
Comments:
The proof structure guides the code structure.
I refuse to imagine “what if I unfold slowFactorial (n-1) by hand?”. The I.H. already tells me the answer so I just use it. This helps me focus.
The catch: I need to make up my mind and carefully write down the specification — what answer my function should give. I need the I.H. to be clear, not muddy.
You get both code and correctness proof. Buy 1 get 1 free. Why don't people do this more?!
Evaluation view (how a computer or an enslaved student runs code): Plug and chug:
slowFactorial 3 → 3 * slowFactorial (3 - 1) → 3 * slowFactorial 2 → 3 * (2 * slowFactorial (2 - 1)) → 3 * (2 * slowFactorial 1) → 3 * (2 * (1 * slowFactorial (1 - 1))) → 3 * (2 * (1 * slowFactorial 0)) → 3 * (2 * (1 * 1)) → 3 * (2 * 1) → 3 * 2 → 6 -}
The next example shows recursion/induction on lists. Reminder of list syntax:
types: [Integer]
, [Bool]
, []
Integer
, [] Bool
, etc.
empty list: []
list literal: [4, 1, 6]
That's syntax sugar for: 4 : (1 : (6 : []))
Those parentheses are optional, like this: 4 : 1 : 6 : []
Formally (recursive definition as in CSCB36): a list is one of:
[]
These are singly-linked lists. To reach the nth item (or even just the nth node), you need to take Θ(n) time to go through all the nodes from the beginning. These are not arrays.
Insertion sort: Strategy: Have a helper function insert
:
Take element e and list xs. xs is assumed to have been sorted.
Put e into the “right place” in xs so the whole is still sorted. E.g.,
insert 4 [1,3,5,8,9,10] = [1,3,4,5,8,9,10]
But we're doing functional programming with immutable lists, can't change xs, but instead: produce a new list that's like xs but also with e at the right place. (Similarly for sorting, can't re-arrange the given list, but will produce a new, sorted list.)
insert :: Integer -> [Integer] -> [Integer] -- Structural induction on xs. -- Base case: xs is empty. Answer is [e] aka e:[] insert e [] = [e] -- e : [] -- Induction step: Suppose xs has the form x:xt (and xt is shorter than xs). -- E.g., xs = [1,3,5,8], x = 1, xt = [3,5,8]. -- Induction hypothesis: insert e xt = put e into the right place in xt. insert e xs@(x:xt) -- xs@(x:xt) is an "as-pattern", "xs as (x:xt)", -- so xs refers to the whole list, and it also matches x:xt -- -- If e <= x, then e should be put before x, in fact all of xs, and be done. -- E.g., insert 1 (10 : xs) = 1 : (10 : xs) | e <= x = e : xs -- Otherwise, the answer should go like: -- x, followed by whatever is putting e into the right place in xt. -- i.e., -- x, followed by insert e xt (because IH) -- E.g., insert 25 (10 : xt) = 10 : (insert 25 xt) | otherwise = x : insert e xtin HaskellBasics.hs
Exercise: Evaluate insert 15 (10 : 20 : []):
insert 15 (10 : 20 : []) →
Using insert
you can complete the sorting algorithm. Here are
two versions, reflecting two styles. Exercise: Your turn to use induction on
them.
Direct recursion version:
insertionSort :: [Integer] -> [Integer] insertionSort [] = [] insertionSort (x:xt) = insert x (insertionSort xt)in HaskellBasics.hs
This other version models a while-loop and an accumulator variable:
The go
helper function models a while-loop; its second parameter
acc
models an accumulater variable.
insertionSortAcc :: [Integer] -> [Integer] insertionSortAcc xs = go xs [] where -- Specification for go (when you prove go correct by induction): -- for all xs, for all acc: -- Assume acc is in sorted order (precondition). -- go xs acc = add elements of xs to acc but in sorted order go (x:xt) acc = let acc2 = insert x acc in go xt acc2 go [] acc = accin HaskellBasics.hs