Looking at data structures more algebraically, as abstract types characterized by their introduction and elimination forms is another topic that’s present in some standard CS sequences and can make one a better programmer. This breaks the habit of projecting intended interpretation of the data to its representation in computer memory, giving more freedom to design data structures for sparse data, that don’t look like the data (which is their interpretation), but play its role (for example, binary decision diagrams). This is related to the statement/model distinction in logic, but the point of view of type theory is intuitively closer to programming practice. (SICP goes some of the way in this direction, but not in sufficient detail.)
A standard treatment of (in particular) this aspect of type theory is [Pierce] or [Harper], which would go easier after something like [Girard, Lafont & Taylor]. Related intuitions can be developed by learning a language like Haskell [Lipovaca] and some category theory [Lawvere & Schanuel]. References:
Seconding the type theory recommendation. The formal CS education I had contained almost nothing about this, so it was all independent studying from textbooks for me anyway.
Looking at data structures more algebraically, as abstract types characterized by their introduction and elimination forms is another topic that’s present in some standard CS sequences and can make one a better programmer. This breaks the habit of projecting intended interpretation of the data to its representation in computer memory, giving more freedom to design data structures for sparse data, that don’t look like the data (which is their interpretation), but play its role (for example, binary decision diagrams). This is related to the statement/model distinction in logic, but the point of view of type theory is intuitively closer to programming practice. (SICP goes some of the way in this direction, but not in sufficient detail.)
A standard treatment of (in particular) this aspect of type theory is [Pierce] or [Harper], which would go easier after something like [Girard, Lafont & Taylor]. Related intuitions can be developed by learning a language like Haskell [Lipovaca] and some category theory [Lawvere & Schanuel]. References:
Benjamin C. Pierce, Types and Programming Languages
Robert Harper, Practical Foundations for Programming Languages
Jean-Yves Girard, Yves Lafont, Paul Taylor, Proofs and Types
Miran Lipovaca, Learn You a Haskell for Great Good!: A Beginner’s Guide
F. William Lawvere, Stephen H. Schanuel, Conceptual Mathematics: A First Introduction to Categories
Seconding the type theory recommendation. The formal CS education I had contained almost nothing about this, so it was all independent studying from textbooks for me anyway.