a

haskell/README.md

@@ -16,6 +16,7 @@ This is the larger, more general README, which will house the main takeaways/rev
   - [ToC](#toc)
 - [Books and resources](#books-and-resources)
   - [13th of March - Introduction](#13th-of-march---introduction)
+  - [\[16th of March - Deriving types\]](#16th-of-march---deriving-types)
 
 # Books and resources
 - [Haskell Programming from first principles](http://haskellbook.com/)
@@ -41,6 +42,36 @@ The tree is simply too complex. Linked lists are easy.
 ## [16th of March - Deriving types]
 
 > How does one do this systematically?
+**Eyeball method:**
+Looking at the function definition:
+
+1. Each parameter - what is the type of each parameter?
+2. Return type - what is the type of the return value?
+3. If the function calls another function, look at the type of that function.
+4. Replace concrete types with type variables (a, b, c, etc.)
+  
+**Formal method[^2]:**
+(on paper)
+
+1. Write down the type of each argument and subexpression.
+2. Generate equations for how types relate to each other and apply transitivity (if needed).
+e.g.
+$$
+\begin{align*}
+f &:: a \to b \to c \\
+g &:: c \to e \\
+
+\implies f \circ g &:: a \to b \to e
+\end{align*}
+$$
+3. Solve the equations for the most general type.
+
+
 
 > Lazy and singly-linked lists, what's the relation?
+A lazy list doesn’t compute all elements at once; it only computes elements as you need them.
+A singly-linked list is naturally great for lazy, because each element points to the next, with the next being a thunk (actual fucking term, meaning a computation that hasn't been evaluated yet[^1]).
 
+
+[^1]: More generally, a thunk is a subroutine used to inject computation into another subroutine. They delay computation until it is needed. It canonically originates from the verb *think* lmao.
+[^2]: [Hindley–Milner type inference](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system)

haskell/sessions/16_03/notes.md

@@ -52,17 +52,55 @@ f = \x y -> x (x (x y))
 ```
 
 ## Questions
-> How does one do the equations?
-
 > 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
 
-> Lazy and singly-linked lists, what's the relation?
+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
+[^1]: need to find the actual rigorous way of doing this
+[^2]: Referential transparency 

haskell/sessions/23_03/notes.md

@@ -0,0 +1,17 @@
+
+## Lists
+
+```hs
+------------ !! mapAccumL 
+mapAccumL :: (s -> a -> (s, b)) -> s -> [a] -> (s, [b])
+------------
+```
+
+
+> Generics in C?
+
+> Implement Haskell lists in Python
+
+> Forall and exists in functional programming
+
+https://hackage.haskell.org/package/base-4.3.1.0/docs/src/Data-List.html

writeups/README.md

@@ -0,0 +1,21 @@
+The most significant (prioritized) writeups that I'm working on can be seen in the footer at [confest.im](https://confest.im/blog), but this folder includes every "technical" (and related to the languages described here) writeup I am working on.
+
+## Ideas and progress
+Tables concerning the idea, the description and progress of the writeups I am working on.
+Scale of progress:
+1. 💡 - Idea stage
+2. 🚧 - Structuring
+3. ✏️ - Writing
+4. ✅ - Finished
+5. ❌ - Abandoned
+
+---
+
+| Idea | Description | Progress |
+|------|-------------|----------|
+| Memory safety | Understanding memory safety from the perspective of a Python developer |  🚧 |
+
+---
+
+1. The intersection of functional programming and formal verification as an amateur in both
+## Miscellaneous ideas