Type Theory

While I have no formal education in the algebra behind type theory, I have just enough education in set theory and experience in typed languages that I have elected to risk making a fool of myself talking about it anyway.

I will be using examples from programming languages in which I actively work, so largely C and Rust. I don’t speak any languages with more intricate type systems, which is no doubt limiting what I’m able to express.

These are often drawn directly from my experience at work.

  1. Data Types (2017 March 14)

    An exploration of how programs assign meaning to patterns of data, and the theories behind that behavior.

  2. Data Structure Punning (2017 March 15)

    Complex data records are often only used as subsets of themselves. In languages such as C++, Java, and C♯, the class and interface systems are built in a way to allow this polymorphism using compile- or run- time typing systems, but this is often expensive or siloed within an artifact or language. This article talks about record composition and destructuring, and ways a language might aid the use of parts of a record in place of the whole.

  3. Type Alchemy (2017 August 18)

    We regularly work with data whose size is not fixed or known ahead-of-time – text, especially C strings, are a prominent example of this – and manipulating it safely requires effort. Part of my work involves using streams of structured, unsized, data, with as little indirection and discontinuity as possible.

  4. Type Solidity (2018 August 29)

    I have strong opinions about how generic type systems ought to work and only by writing them down in a fully specified manner can people who actually know type theory tell me why I’m wrong.