Re: Online Programming Lanugage Discussions
Posted: Sep 5, 2006 4:20 AM
> To help defeat them, I
> have been calling on the big guns at <b><a
> a-the-Ultimate.org</a></b>, a discussion site for
> programming language and type system theorists.
There's certainly a lot of very bright people, there. I've recently bought several books on computer science/programming language therory and type theory, myself, including the one you mention in your blog (as well as some maths books - such as books on lambda calculus and category theory), to be able to actually understand what they talk about in such discussions, and be able to participate. :)
The books I've bought (on programming languages and types), are:
- "Concepts, Techniques, and Models of Computer Programming"
- "Types and Programming Languages"
- "Advanced Topics in Types and Programming Languages"
However, I've not got around to read these, yet. It seems I'll have enough to read for a while. :)
Some maths books on interesting, and computer science-relevant topics, that I've also recently bought (which I haven't read, either):
- "Conceptual Mathematics: A First Introduction to Categories"
- "Basic Category Theory for Computer Scientists"
- "An Introduction to Lambda Calculi for Computer Scientists"
- "Introduction to Topology"
- "A Combinatorial Introduction to Topology"
- "Algebraic Topology"
I typically buy several books on topics, as they tend to complement each other, and it gives a better chance of getting one or a few that are really good. :)
> It is a good place to hang out for aspiring language designers.
Definitely. I was reading a very interesting thread there a few days ago: "Why type systems are interesting" (http://lambda-the-ultimate.org/node/100), and was thinking: "This is something Christopher Diggins should read" (I assumed it could be of interest to you, from knowing your interest in programming language design and type systems), but I see you're already well familiar with the site. :)
> What is happening right now with Cat is that I am trying
> to merge static type-checking and dynamic type-checking in
> a single language.
As you've seen from the thread you linked to, "dynamic typing" isn't really a term that is well accepted by type theorists, as they instead prefer to call dynamically typed languages "untyped languages"... :)
"Definitions of type system vary, but the following one due to Benjamin C. Pierce roughly corresponds to the current consensus in the programming language theory community:
[A type system is a] tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
In other words, the term "dynamic typing" appears to be something of a contradiction, in terms of classical type theory. Using the above conventional definition of "type", "dynamically typed languages" are basically "untyped" - all variables are of a "universal type" (variant).