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.
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.
Data Structure Punning
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.
An exploration of how programs assign meaning to patterns of data, and the theories behind that behavior.