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.

Articles

1. Type Alchemy (2017, Aug 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, Mar 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, Mar 14)
   

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