On Sun, Nov 17, 2013 at 02:10:17PM -0800, Darren Duncan wrote: > I recall reading that at least in certain math/logic papers that a > programming language type system can be defined logically in terms > of pure sets, making it essentially self-defined without needing to > rely on external definitions of for example what a number is.
Well, it's true. But there's a more natural way for programming languages. Church's theory of types defines everything using functions as the primitive. While mathematics as a field has mostly settled on set theory as its basis, type theory is equally expressive and is usually preferred in language design. > Does Haskell at least conceptually work in terms like I described? > I seem to recall reading that how it logically thinks about string > values is towards that direction. Haskell, like most vaguely modern languages with a grounding in type theory and a strict type system, is based on functions as primitives. For a thorough primer on the subject, I recommend "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" for the theory, and Ben Pierce's spectacular "Types and Programming Languages" for the practical applications. http://gtps.math.cmu.edu/tttp.html http://www.cis.upenn.edu/~bcpierce/tapl/ Most of the newly created programming languages (and all the ones that aren't an embarrassment - Java, I'm looking at you) draw from these ideas to some extent. If you want to look at one that takes the concept out to the cutting edge of what is possible, I'd suggest Coq - not very practical, but interesting.
