See also pure type systems<p><a href="https://en.wikipedia.org/wiki/Pure_type_system" rel="nofollow">https://en.wikipedia.org/wiki/Pure_type_system</a>
Reminds me a bit of the "Commutative diagram of harmonic wave" from wikipedia<p><a href="https://commons.wikimedia.org/wiki/File:Commutative_diagram_of_harmonic_wave_properties.svg" rel="nofollow">https://commons.wikimedia.org/wiki/File:Commutative_diagram_...</a>
Can anyone recommend an <i>online course</i> for learning about the lambda calculus and the introductory type theory?<p>I've tried learning about them on my own using books, but I have trouble staying focused and motivated enough to get very far.
Language theory and lambda calculus classes were some of my favourite in college. I wonder how many serious bugs would be averted if programming languages came with more complete type systems.
"Each dimension of the cube corresponds to a new way of making objects depend on other objects"<p>Is it normal to refer to data structures as objects? Just to my knowledge most typed languages abhor the awesome potential of object-oriented programming, like the CLOS.