Why (Good) Type Systems are Great - HackMD

<style> .reveal { font-size: 32px; } </style> # Why Type Systems are Great ### <small>(when combined with a sufficiently powerful typechecker)</small>  slides: https://tinyurl.com/types-are-awesome code: https://github.com/sagnibak/types-are-awesome-demo --- In order to make the most of this talk, you must be able to appreciate formal mathematical proofs. <span>That is not a problem since you've all taken CS 70.</span> ---- ## Proof <span>In order to become a UPE member, you must be a CS major. </span><span>In order to be a CS major, you must have taken CS 70. </span><span>Therefore every UPE member must have taken CS 70.</span> ---- ## A Program ```python class UPEMember: csMajor: CSMajor class CSMajor: takenCS70: HasTakenCS70 class HasTakenCS70: sid: int def upeToCS70(upeMember: UPEMember) -> HasTakenCS70: return csMajorToCS70(upeMember.csMajor) def csMajorToCS70(csMajor: CSMajor) -> HasTakenCS70: return csMajor.takenCS70 ``` ----  Jay is a UPE member $\implies$ Jay has taken CS 70. ```python jay_monga = UPEMember(CSMajor(HasTakenCS70(3032323332))) also_jay: HasTakenCS70 = upeToCS70(jay_monga) ``` <span><tr> - All the code type-checks!</tr></span> <span><tr> - Proves that the set of UPE members is nonempty $\implies$ the set of students who have taken CS 70 is nonempty.</tr></span> --- ## The Curry-Howard Isomorphism Every proposition is isomorphic to a type. Every proof is isomorphic to a program. ---- | Logic | Python | C++ | Rust | Scala | Haskell | |-------|--------|------|------------|--------|-----------| | True | `None` | `void` | `()` | `Unit` | `()` | | False | `NoReturn` | `void` | `!`/`never` | `Nothing` | `bottom` | | $\land$ | `(a, b)` | `pair` | `(a, b)` | `(a, b)` | `(a, b)` | | $\lor$ | `Union` | tagged union | `enum` | `Either` | `Either` | | $\implies$ | `def` | function | `fn` | `def` | function | | $\forall$ | `Generic` | `<...>` | `<...>` | `[...]` | generics |  ...and a LOT more! ---- ### Negation \begin{align*} \neg P &\equiv \neg P \lor \text{False} \\ &\equiv (P \implies \text{False}) \end{align*} We can use this tautology to define the negation of a type. Python: ```python notP = Callable[[P], NoReturn] # this is a type alias ``` Rust: ```rust type Not<P> = fn(P) -> !; // type alias ``` ---- ### Distributive Law $(P \lor Q) \land R \implies (P \land R) \lor (Q \land R)$ Python: ```python def distribute(p_or_q: Union[P, Q], r: R) -> Union[Tuple[P, R], Tuple[Q, R]]: if isinstance(p_or_q, P): p: P = p_or_q return (p, r) else: q: Q = p_or_q return (q, r) ``` Rust: ```rust fn distribute(p_or_q: Either<P, Q>, r: R) -> Either<(P, R), (Q, R)> { match p_or_q { Either::Left(p) => Either::Left((p, r)), Either::Right(q) => Either::Right((q, r)), } } // defining a sum type enum Either<P, Q> { Left(P), Right(Q), } ``` ---- ### Function Application, Modus Ponens $((P \implies Q) \land P) \implies Q$ Python: ```python def apply(p_to_q: Callable[[P], Q], p: P) -> Q: return p_to_q(p) ``` Rust: ```rust fn apply(p_to_q: fn(P) -> Q, p: P) -> Q { p_to_q(p) } ``` <span>If I have a way to convert evidence for $P$ into evidence for $Q$ and I have evidence for $P$, then I can produce evidence for $Q$.</span> ---- ### Currying $((P \land Q) \implies R) \implies (P \implies (Q \implies R))$ ```python def curry(fn: Callable[[P, Q], R]) -> Callable[[P], Callable[[Q], R]]: def curried(p: P) -> Callable[[Q], R]: def inner(q: Q) -> R: return fn(p, q) return inner return curried ``` ---- ### Universal Quantification, Generics $(P \land Q) \implies (Q \land P) \; \forall P, Q$ ```rust fn and_commutes<P, Q>(p_and_q: (P, Q)) -> (Q, P) { (p_and_q.1, p_and_q.0) } ``` <span> We can actually make all the functions above generic by adding `<...>`, just like we can make the propositions true $\forall \ldots$ </span> <span> ```rust fn notP<P>(p: P) -> ! { loop {} // infinite looping is also valid } ```  ```rust fn distribute<P, Q, R>( p_or_q: Either<P, Q>, r: R ) -> Either<(P, R), (Q, R)> { match p_or_q { Either::Left(p) => Either::Left((p, r)), Either::Right(q) => Either::Right((q, r)), } } ```  </span> ---- ### Contraposition $(P \implies Q) \implies (\neg Q \implies \neg P)$ ```python NotP = Callable[[P], NoReturn] NotQ = Callable[[Q], NoReturn] def contraposition(p_to_q: Callable[[P], Q]) -> Callable[[NotQ], NotP]: def contrapositive(not_q: NotQ) -> NotP: def inner(p: P) -> NoReturn: return not_q(p_to_q(p)) return inner return contrapositive ``` ---- ### Double Negation Introduction \begin{align*} P &\implies \neg \neg P \\ \equiv P &\implies (\neg P \implies \text{False}) \\ \equiv P &\implies ((P \implies \text{False}) \implies \text{False}) \end{align*} ```python NotP = Callable[[P], NoReturn] NotNotP = Callable[[NotP], NoReturn] def double_negation_intro(p: P) -> NotNotP: def double_negation(not_p: NotP) -> NoReturn: return not_p(p) return double_negation ``` ---- ### Double Negation Elimination $\neg \neg P \implies P$ Impossible to prove! <span> You only have functions that return instances of `NoReturn`. They don't give you any way to produce evidence for $P$.</span> <span>You typically need language extensions (e.g., in Haskell) to add this as an axiom.</span> ---- ### Proof by Contradiction $(\neg P \implies \text{False}) \implies P$ Impossible to prove, since it implies (and is implied by) double negation in this framework of logic. ---- ### No law of the excluded middle $$ P \lor \neg P \not\Rightarrow \text{True} $$ <span> Equivalent to double negation elimination! \begin{align*} P \lor \neg P &\equiv \neg P \lor P \\ &\equiv \neg \neg P \implies P \end{align*} </span> <span>Topology has scenarios where the law of the excluded middle does not hold. Scroll down with caution.</span> ---- <span> - Consider the Sierpiński topological space, defined by the set $X:=\{0,1\}$ with topology (open sets) $\mathcal{T} := \{\varnothing, \{1\}, \{0,1\}\}$. Then the closed sets are $\{\varnothing, \{0\}, \{0,1\}\}$. </span> <span> - If we let $X$ be true, $\varnothing$ be false, $\cup$ be or, and $\cap$ be and, we get a system that obeys the axioms of intuitionistic logic. Every proposition is a set, and the **interior** of its complement is its negation. </span> <span> - LEM is equivalent to $U \cup \neg U = X\;\forall U\subseteq X$, but this does not hold for $U := \{1\}$, since $\neg U = \text{interior}(\{1\}^c) = \varnothing$. </span> ---- <span> - Consider $X = \mathbb{R}$ with the usual topology (open balls/open rectangles). </span> <span> - If we let $X$ be true, $\varnothing$ be false, $\cup$ be or, and $\cap$ be and, we get a system that obeys the axioms of intuitionistic logic. Every proposition is a set, and the **interior** of its complement is its negation. </span> <span> <span> - LEM is equivalent to $U \cup \neg U = X\;\forall U\subseteq X$, but this does not hold for $U := (p, q)$, since $\neg U = \text{interior}((-\infty, p] \cup [q, \infty)) = (-\infty, p) \cup (q, \infty)$. - $(p, q) \cup (-\infty, p) \cup (q, \infty) = \mathbb{R} \setminus \{p, q\} \ne \mathbb{R}$  </span> --- ## But Why Does It Matter? - More work at compile time means less work at runtime - Code that compiles usually works --- ## Example: `isinstance` <span> Without types:  ```python def csMajorToCS70(csMajor): if isinstance(csMajor, CSMajor): return csMajor.takenCS70 else: raise TypeError("csMajor must be a CSMajor!") ```  </span> <span> With types:  ```python def csMajorToCS70(csMajor: CSMajor) -> HasTakenCS70: return csMajor.takenCS70 ```  </span> ---- We need an `isinstance` check (runtime typechecking) when we don't have compile-time typechecking. This is bad because: <span><tr> - runtime typecheking happens every time the function is called, so it has a runtime overhead</tr></span> <span><tr> - our program can terminate without producing the correct output</tr></span> --- ## Example: Sometimes `None` <span> Consider:  ```python def sometimesNone() -> Optional[int]: return randint(1, 10) if random() > 0.2 else None ```  </span> <span> Without typechecking:  ```python def foo(a): return a * sometimesNone() ```  <span> With typechecking:  ```python def foo(a: int) -> int: if (b := sometimesNone()) is not None: return a * b else: return a ```  </span> ---- <span><tr> - Without typechecking you can merrily ignore the case when the result of `sometimesNone` is `None`, and get a `TypeError` at runtime. </tr></span> <span><tr> - With typechecking you are forced to do _something_ in that case. An alternative to the code presented above would be to pass through that `None`. <span><small>Smells like a monad.</small></span>  </tr></span> <span> ```python def foo(a: int) -> Optional[int]: if (b := sometimesNone()) is not None: return a * b else: return b ```  </span> --- ## No More Null Pointers Rust uses static typechecking to prevent - dereferencing null pointers - data races - double frees - etc. --- You can have multiple immutable pointers to a piece of memory: <span> ```rust= let arr = [1, 2, 3]; let ptr1 = &arr; let ptr2 = &arr; ```  </span> <span>But you can only have one mutable pointer to it: </span> <span> ```rust=2 let ptr3 = &mut arr; // this is okay let ptr4 = &arr; // not okay, ptr1 is live let ptr5 = &mut arr; // also not okay ptr1[2] = 4; // necessary to keep ptr1 live ```  </span> ---- How does the compiler keep track of what is mutable and what is not? Types! ```rust ptr1, ptr2, ptr4: &[i32]; ptr3, ptr5: &mut [i32]; ``` <span> The Rust type system is expressive enough to mark the mutability of variables.  </span> <span> In order to do the same in C++, you would need reference-counted pointers which add runtime overhead.  </span> --- ### What might go wrong <span> The following is legal C++, it compiles: ```cpp std::vector<int>* arr = new std::vector<int>({1, 2, 3}); std::vector<int>* ptr = arr; delete arr; std::cout << (*ptr)[0] << std::endl; ```  </span> <span> At runtime it causes 2020 to happen.  </span> <span> The equivalent Rust code does not compile:  </span> <span> ```rust=2 let mut arr = vec![1, 2, 3]; let ptr = &arr; Vec::drain(&mut arr, ..); println!("{:?}", ptr); ```  </span> ---- We create a reference `ptr` to `arr` on line 3, then we create a mutable reference on line 4, and then we try to use `ptr` again on line 5. That is a problem, since `ptr` is no longer pointing to valid memory. ![](https://i.imgur.com/PQIRWC9.png)     ---- - The `Vec<T>::drain` takes a mutable reference to a `Vec`, it has signature `drain(self: &mut Vec<T>, range: ...)`. </span> <span> - The compiler has an axiom that you can have either a single mutable reference or multiple immutable references to the same piece of memory. </span> <span> - But `ptr` is a live immutable reference to `arr` and `self` is a live mutable reference to `arr`, a contradiction. </span> ---- However, the following is valid ```rust=2 let mut arr: Vec<i32> = vec![1, 2, 3]; let ptr = &arr; drop(&mut arr); ``` since `ptr` gets optimized away by line 4 (it is not "live" at line 4). --- ## Optimizations Can Rust optimize the following code? ```rust fn compute(input: &u32, output: &mut u32) { if *input > 10 { *output = 1; } if *input > 5 { *output *= 2; } } ``` <span> Yes!  ```rust fn compute(input: &u32, output: &mut u32) { let cached = *input; // keep *input in a register if cached > 10 { *output = 2; // x > 10 implies x > 5, so double and exit } else if cached_input > 5 { *output *= 2; } } ```  </span> ---- What about this C++ function? ```cpp void compute(int* input, int* output) { if (*input > 10) { *output = 1; } if (*input > 5) { *output *= 2; } } ``` <span> No! Consider this driver code:  ```cpp const int a = 20; const int* input = &a, *output = &a; printf("Before -> *input: %d, *output: %d\n", *input, *output); compute(input, output); printf("After -> *input: %d, *output: %d\n", *input, *output); ```  </span> <span> ``` Before -> *input: 20, *output: 20 After -> *input: 1, *output: 1 ```  </span> ---- `const` __does not__ solves the problem in C++. Consider ```cpp void compute(const int* input, int* output) { if (*input > 10) { *output = 1; } if (*input > 5) { *output *= 2; } } ``` with driver code: ```cpp int a = 20; const int* input = &a; int* output = &a; // this is illegal in Rust printf("Before -> *input: %d, *output: %d\n", *input, *output); compute(input, output); printf("After -> *input: %d, *output: %d\n", *input, *output); ``` <span> ``` Before -> *input: 20, *output: 20 After -> *input: 1, *output: 1 ```  </span> --- ## Example: Compile-time Length The following is valid Python, it compiles: ```python a = np.zeros((2, 3)) b = np.zeros((4, 5)) _ = a.dot(b) ``` But it causes a shape-mismatch error at runtime, since you cannot multiply a 2×3 matrix by a 4×5 matrix. <span> The following equivalent Rust code fails to compile:  ```rust let a = Matrix<f32, U2, U3, MatrixArray<f32, U2, U3>>::zero(); let b = Matrix<f32, U4, U5, MatrixArray<f32, U4, U5>>::zero(); let _ = a * b; ```  </span> ---- Let's look at this closely. ```rust let a = Matrix<f32, U2, U3, MatrixArray<f32, U2, U3>>::zero(); ``` <span> - The `Matrix` and `MatrixArray` types are generic in their data type, number of rows, and number of columns. `Matrix` is also generic in its containter type, which is `MatrixArray<f32, U2, U3>` here.  </span> <span> - `U2`, `U3`, `U4`, and `U5` are type-level numbers. These numbers are evaluated at compile time, and get optimized away at runtime.  </span> ---- <span> This is the meat of the matrix multiplication implementation ([full](https://github.com/dimforge/nalgebra/blob/dev/src/base/ops.rs#L619)):  ```rust impl<...> Mul<Matrix<..., R2, C2, ...>> for Matrix<..., R1, C1, ...> where ShapeConstraint: AreMultipliable<R1, C1, R2, C2>, { type Output = MatrixMN<..., R1, C2>; fn mul(self, rhs: Matrix<..., R2, C2, ...>) -> Self::Output { &self * &rhs } } ```  - Type constraints appear after `where`. Specifically, the constraint `AreMultipliable` ensures that only matrices of appropriate dimensions get multiplied together.  - It is a proposition, expressed as a type, which the compiler tries to prove, by finding an appropriate implementation!  </span> ---- This is the meat of the `AreMultipliable` type ([full](https://github.com/dimforge/nalgebra/blob/dev/src/base/constraint.rs)): ```rust struct ShapeConstraint; pub trait AreMultipliable<R1: Dim, C1: Dim, R2: Dim, C2: Dim>: DimEq<C1, R2> {} impl<R1: Dim, C1: Dim, R2: Dim, C2: Dim> AreMultipliable<R1, C1, R2, C2> for ShapeConstraint where ShapeConstraint: DimEq<C1, R2> {} pub trait DimEq<D1: Dim, D2: Dim> {} impl<D: Dim> DimEq<D, D> for ShapeConstraint {} ``` <span> - The compiler can produce a `DimEq<C1, R2>` instance for `ShapeConstraint` only if `C1` and `R2` are the same type (here, the same number).  - The empty bodies `{}` mean that these types cannot do anything at runtime, they will get optimized away. (In the actual code some of the bodies contain associated types, which also get optimized away.)  </span> ---- # Demo --- ## References, Further Reading - [Sierpiński space](https://en.wikipedia.org/wiki/Sierpi%C5%84ski_space) - [Example of the Law of the Excluded Middle failing](https://math.stackexchange.com/a/1371237/783650) - [Curry-Howard isomorphism](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Related_proofs-as-programs_correspondences) - [Aliasing in Rust](https://doc.rust-lang.org/nomicon/aliasing.html) - [typenum.rs](https://github.com/paholg/typenum) - [peano.rs](https://github.com/paholg/peano) - [Nalgebra](https://nalgebra.org/) - [Type-level rust in detail](https://beachape.com/blog/2017/03/12/gentle-intro-to-type-level-recursion-in-Rust-from-zero-to-frunk-hlist-sculpting/) - [More useful version of ^ but less comprehensive](https://beachape.com/blog/2017/03/12/gentle-intro-to-type-level-recursion-in-Rust-from-zero-to-frunk-hlist-sculpting/) - [Curry-Howard Isomorphism in Haskell (talk)](https://www.youtube.com/watch?v=tfG7T54MhIU&ab_channel=LambdaConf)