106 lines
3.0 KiB
Markdown
106 lines
3.0 KiB
Markdown
## Table
|
|
| Topic | Description | Confidence |
|
|
|-------|-------------|------------|
|
|
| Signatures | Checking whether the expression types are correct | 😐 |
|
|
| Programming | Writing code to solve an algorithmic problem | 😐 |
|
|
| Higher order functions | Demonstrate understanding of higher order functions, usually by chaining them | 😊 |
|
|
| List comprehensions | Demonstrate understanding of list comprehensions | 😊 |
|
|
| Recursion/infinite lists | Infinitely generating lists, usually by recursion and/or list comprehensions | 😐 |
|
|
| ADTs | Algebraic Data Types, usually defining a data type and writing functions that operate on it | 😕 |
|
|
| Proof on lists | Proving properties of functions that operate on lists | 😕 |
|
|
| Proof on trees/ADTs | Proving properties of functions that operate on trees or ADTs | 😕 |
|
|
|
|
|
|
## Deducing types systematically
|
|
|
|
### (:).(:)
|
|
```hs
|
|
expr = (:) . (:)
|
|
|
|
(:) :: a -> [a] -> [a]
|
|
(.) :: (c -> d) -> (b -> c) -> b -> d
|
|
|
|
=>
|
|
|
|
a -> ([a] -> [a]) = b -> c
|
|
|
|
b = a
|
|
c = [a] -> [a]
|
|
|
|
---
|
|
|
|
a' -> [a'] -> [a'] = c -> d
|
|
a -> [a] -> [a] = b -> c
|
|
|
|
b = a
|
|
c = [a] -> [a]
|
|
|
|
a' = [a] -> [a]
|
|
[[a] -> [a]] -> [[a] -> [a]] = d
|
|
|
|
|
|
expr :: b -> d
|
|
=>
|
|
expr :: a -> [[a] -> [a]] -> [[a] -> [a]]
|
|
```
|
|
|
|
|
|
### `f = \x y -> x (x (x y))` [^1]
|
|
|
|
```hs
|
|
f = \x y -> x (x (x y))
|
|
```
|
|
|
|
## Questions
|
|
> CLI is functional?
|
|
Not really. It fits the functional mindset.
|
|
Commands are:
|
|
- pure, input leads to output
|
|
- composable with the pipe, kinda like `(.)`
|
|
- They can be composed like higher order functions, i.e. one command can be the input to another command
|
|
|
|
In reality though, they are not functional. Their main goal is to interact with the system (a.k.a. a mutable state), which obviously breaks the functional paradigm.
|
|
|
|
> Y combinator?
|
|
A function, which allows us to define recursive functions without giving them a name. It gives us a fixed point of a function, i.e. a function that doesn't change when you apply it to itself.
|
|
|
|
In other words, finds a value $x$ such that $f(x) = x$.
|
|
|
|
```hs
|
|
y f = f (y f) -- this is the Y combinator
|
|
```
|
|
|
|
Example:
|
|
```hs
|
|
fact = \f n -> if n == 0 then 1 else n * f (n-1) -- n! = f(n) = n * f(n-1) = n * (n-1) * f(n-2) = ...
|
|
```
|
|
|
|
If we were to not use the Y combinator, we would have to define the function as:
|
|
```hs
|
|
fact = \n -> if n == 0 then 1 else n * fact (n-1)
|
|
```
|
|
|
|
> In which cases would it be impossible to not use the Y combinator?
|
|
Whenever we are working with a system that has no named functions, but we still want recursion.
|
|
|
|
In the context of Haskell, using the Y combinator (in the classical lambda calculus way) is elegant, yet not necessary.
|
|
Rewriting our factorial function using `where`:
|
|
|
|
```hs
|
|
fact :: Int -> Int
|
|
fact n = f n
|
|
where
|
|
f 0 = 1
|
|
f n = n * f (n-1)
|
|
```
|
|
|
|
is way more readable and intuitive.
|
|
|
|
|
|
|
|
## Resources
|
|
- [course](https://www.cis.upenn.edu/~cis1940/spring15/lectures.html)
|
|
- [standard list](https://hackage.haskell.org/package/base-4.21.0.0/docs/Data-List.html)
|
|
|
|
[^1]: need to find the actual rigorous way of doing this
|
|
[^2]: Referential transparency |