20260213033430

Reading Category Theory for Programmers by Bartosz Milewski on stream.

Previous reading: 20260205231424

Part 1, Section 2 - Types and Functions:

Who needs Types?
- The author seems to imply that strongly typed statically checked languages are better, because they prioritize the production of programs that are correct.
- I agree with this, but they don't say it outright so I'm not sure what point they are trying to make exactly.
Types are about composability
- I like the quote "The stronger the type system of the language, the better this match can be described and mechanically verified." because it can be read both ways: the type system not only helps the compiler produce correct programs, but it also helps us write programs.
- Milewski mentions how stronger type systems could prevent you from writing semantically correct programs, but that in these cases there are usually backdoors built into the language that allow you to write these programs anyway. This reminds me of unsafePerformIO and my favorite function of all time, accursedUnutterablePerformIO.
- Milewski's comment about productivity in Haskell reminds me of a research report I read once where the people reviewing the code didn't believe Haskell was a real programming language. The report is titled Haskell vs. Ada vs. Awk vs. ... An Experiment in Software Prototyping Productivity by Paul Hudak and Mark P. Jones, and was published in October 1994. https://www.cs.yale.edu/publications/techreports/tr1049.pdf
- I would argue strong typing can replace unit testing, though I do think that unit testing can still be a powerful tool.
What are types?
- Set is a category with the following properties:
  - An empty set has no elements.
  - There are special one-element sets.
  - Functions map elements of one set to elements of another set.
  - Functions can map two elements to one, but not one element to two.
  - An identity function maps each element of a set to itself.
- Milewski says the plan is to gradually forget all this information in favor of expressing all of these notions in purely categorical terms -- that is, in terms of objects and arrows.
- ⊥ (bottom) can be thought of a special value that is added to every type which corresponds to a non-terminating computation or one that returns a runtime error.
- Functions that return bottom are partial, while those that don't are called total.
- Total functions return a valid result for every possible argument.
- The category of Haskell types and functions is actually a Hask instead of a Set, but what a hask is will not be explained in this book.
- Operational semantics describes the mechanics of program execution
- Under Denotational Semantics, every programming construct is given a mathematical interpretation.
- A breakthrough in category theory by Eugenio Moggi showed that computational effects can be mapped to monads, giving us a way to have a denotational semantic reading of programs that previously could only be understood under the operational semantics lens.
Pure and Dirty Functions
- Pure functions are functions that always produce the same result given the same input and have no side effects.
- Pure functions are easier to give denotational semantics to, which makes them easier to model using category theory.
Examples of types
- Void in Haskell is a type that isn't inhabited by any value. That is, if a function requires Void as an argument, you cannot call it because you cannot produce a value of type Void
- Types and functions can be understood in terms of logic due to the Curry-Howard isomorphism.
- () (unit) in Haskell is a type inhabited by exactly one value.
- Functions from unit to any type A are in a one-to-one correspondence with elements in set A.
- Functions from type A to unit map every element in set A to unit.
  - Such a function can be defined as f :: a -> (), because no matter the type of a, it will always return unit. Functions that can be implemented the same way for any type like this are called parametrically polymorphic.

Challenges:

use std::collections::HashMap;
use std::cmp::Eq;
use std::hash::Hash;

fn main() {
    let mut add5 = memoize(|x| { x + 5 } );
    add5(10);
    add5(10);
    add5(10);
}

fn memoize<T: Copy + Eq + Hash, U: Copy>(f: fn(T) -> U) -> impl FnMut(T) -> U {
    let mut memo = HashMap::new();
    return move |a| {
        match memo.get(&a) {
            Some(result) => {
                println!("Remembered!");
                return *result;
            }
            None => {
                let result = f(a);
                memo.insert(a, result);
                println!("Memoized!");
                return result;
            }
        }
    };
}

No, it doesn't work because the function isn't pure.
Yes, because the function is pure now.
My example is in rust, BUT I think the answers would be as follows:
1. Yes
2. No
3. Kind of. Memoize would return the right value, but the print statement would no longer print on subsequent calls. The function isn't quite pure because it has a side effect.
4. No, this function has a side effect -- it depends on and mutates static state.
If we are only going to count pure functions, there's a finite number of them, and you can write them all (pseudocode). There four total functions and one partial one:
1. fn(_) -> return true
2. fn(_) -> return false
3. fn(a) -> return a
4. fn(a) -> return not a
5. fn(a) -> undefined
Void has no arrows, because it has no values. True and False both use the same function to point to Unit, Unit can point to either true or false, but these functions are different. I don't think any arrows point from Bool or Unit to Void, because I don't think Void includes bottom.

content

meta