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