Type Theory

I am not a type theoretician nor have I taken any courses in the science. What I do have, however, is an engineering background doing fun things with data layout and type-directed programming.


  1. Type Alchemy (2017-08-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.

  2. Data Structure Punning (2017-03-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. Data Types (2017-03-14)

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