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, Aug 18 at 00:00 )
   

   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 at 00:00 )
   

   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 at 00:00 )
   

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