Lambda the Ultimate

I agree, Hindley's book is rather dense. I managed to make it through the first chapter and a little ways into the second.

I'll second the recommendation for TaPL. You probably want to be exposed to structural induction beforehand, even though it's covered in the first chapter.

The Essentials of Programming Languages also has a bit on type systems, both object-oriented and hindley-milner. Type Theory and Functional Programming is freely available online, and emphasizes type theory as an extension of natural deduction.

My experience as somebody who is reasonably sophisticated mathematically, is that type theory is not an easy thing to teach yourself. Sadly, I've never really had anybody to explain it to me, and so, I feel like I'm way behind where I could be on this subject.

I'm pretty weak on proofs myself, and ended up skipping them more and more as I made my way through TaPL. But even without the proofs, the semi-formal description of different topics in PL was great light-ish reading. Though I plan to go through it again to try to absorb the more formal sections, I'd be perfectly satisfied with my purchase even without that stuff.

Also, some of the interspersed exercise questions are particularly good.

Definitely a good book.

When I was in your position, I also learned a lot from some of Luca Cardelli's papers. "Typeful programming" (Research Report 45, Digital SRC, 1994) is a surprisingly good as an introduction, in that it walks through a self-contained language that demonstrates pretty much all the interesting type features that were well-understood at the time (so no objects). It's split with a discursive description in the front with the type rules at the back to refer to, so you can get to grips with the concepts without being scared by the maths :-)

-- Simon

Shriram Krishnamurthi's book has some real potential. Though this isn't quite on topic, I do recommend the section on web programming with continuations. It's a great idea and this is the most accessible introduction to the topic that I've seen.

...Wonders whether we do a disservice of bundling the teaching of mathematical concepts/notation and applied programming concepts (PL, algorithms, etc...). For example, you don't expect the Physics and Chemistry departments to teach Differential Equations, but somehow we expect the CS department to convey Set Theory, Category Theory, Lambda Calculus, etc...

Best I can find for covering these topics as maths is under the umbrella of Discrete Mathematics, but I don't remember such a topic when I was at University many years ago (my coursework included Trig, Calc I-III, Differential Equations, Matrix Algebra, Stats and various other business related maths). Could it be I wasn't paying attention at the time.

There are many mathematical (or math-heavy) subjects which are taught in science/engineering departments that I can think of. (At least they were when and where I went to the university):

Among them:

* Linear system theory
* All manner of signal processing theory (both discrete-time and continuous-time)
* Numerous "CS" topics as mentioned above.
* Game theory

I'm not sure why this is. Of the various scientific displines, ones which probably contribute the most to mathematics (and are the most demanding consumers of mathematical theory) are CS, physics, and economics.

LC and CT are best left to the CS department, the way things are now.

My impression, however, is that CS programs don't teach these skills well enough, and most CS graduates wouldn't know how or when to apply them. But that's a different kind of problem...

From somebody who majored in mathematics and assisted with several discrete math classes, a couple of observations:

The material covered in Discrete Mathematics varies wildly, much more so than any other course. It's goals vary only somewhat less so. Usually, students will be expected to be familiar with reading and writing simple proofs, naive set theory, propositional logic, universal and existential quantifiers, and induction over the natural numbers.

I've never heard of the lambda calculus being taught in Discrete Math. (Though it probably has been, sometime, somewhere.) My gut feeling is that time spent on the lambda calculus would have poor returns on the goals stated above.

On the other hand, it is increasingly popular to use ML and Haskell in discrete math. In these courses, it has been my experience that:

1. Non-computer scientists write atrocious code that they foist upon their students. (and often think their code is thing greatest thing since sliced bread.)

2. Non-mathematicans don't do justice to the mathematical aspects of the course. (and instead of thinking they are doing a great job, they are simply oblivious)

3. At better institutions, I'd say that maybe a third to a half of the discrete profs are competent in both math and computer science.

4. Students often (usually?) don't like functional programming. Is it because these students have been selected by introductory programming courses in C++ or Java? Maybe, I don't know.

Of course, these are highly informal observations, so YMMV.

Back when the job market favored programmers, there was a substantial push from management types to remove mathematics from the computer science curriculum. Believe me, this movement is still there. There just hasn't been the motivation to push forward in recent years.

Educators are taking this to mean that they are doing a terrible job of teach *how* math is applicable to computer science. Traditionally, the subjects are taught in isolation from each other. I know of two efforts to remedy this:

The TeachScheme! project aims at teaching Scheme in high school algebra classes. As such, it largely focuses on applying computer science to mathematics and giving students a more concrete way to interact with algebra.

The Beseme Project aims to integrate Haskell and equational reasoning into discrete math. Again, the course requirements dictate that the focus is on the math, but secretly, it's trying to do more in the direction of applying math to computer science.

As for textbooks for discrete math, there is probably more discontent on this topic than for any other math course. I didn't keep my Discrete Math book, in fact, I don't even remember which one it was.

I haven't found a discrete math book I like yet. Maybe the Beseme Project will publish a book someday. :-)

Interesting comments, especially since I am about to teach a new first-year course in Discrete Mathematics aimed specifically at Computer Science.

I am a trained mathematician (all 3 degrees in Pure Math, but my undergrad was a joint CS-Math degree), but I also worked for 10 years as a professional programmer. Of course, I cheated, I was working for Maplesoft, although I did start out writing GUI code before I took over the Math Group (and then, shudder, even did some Web programming). As far as using a lot of mathematics in my daily programming work, I sure did a lot of that!

I am currently employed in department that offers both a Computer Science and a Software Engineering degree. About 2/3 of the faculty are actually ex-mathematicians of one flavour or another, it is actually quite pleasant, but the poor "systems" people feel pretty lonely!

In any case, since my own interests lie on the PL side, I intend to teach a bit more of the mathematics needed for understanding programs than is usual. While I will of course teach some of the the mathematics necessary for complexity analysis of data-structures and algorithms (though the best tool for that, namely the Mellin Transform, is not going to make it :-( ).

My current plan is to craft a course highly influenced by The Haskell Road. I may even sprinkle in some ideas from synthetic topology (though not by that name!), at least in the exercises.

The challenge I have set myself is the following: for every single piece of mathematics I teach in that course, I should be able to provide at least one example from Computer Science understandable by a first year student. If I can't, then I will not teach that bit of mathematics and move on.

Any and all comments, advice, etc are very welcome!

I am reminded of my 8th grader who keeps questioning why he needs to study algebra - since he says he'll never use it. I can't say that there's much way to show him the practical side, since he's got his whole life figured out (at least until the end of the day).

Me, I'm more interested in the discrete mathematics that transcends any particular programming language. Problem with many of the texts is that the notation of mathematical abstraction is overwhelmed with the notation of the programming language being used. I get the feeling that a lot of texts put some common mathematical notation at the beginning of the chapters, but don't dwell on it enough. The assumption being that you are either already familiar the notation or that a practical demonstration in the chosen PL will make matters clear.

On the notation front, I agree. That is why I was intending to use Maple to demonstrate some of the ideas, and Haskell for others. That way I hope to be able to keep the PL notation and the Math notation as close as possible to each other.

In most programming languages, it is true that the notation is so far from the mathematical notation that this obscures rather than re-inforces the point.

Have a look at my lecture notes at for inspiration. I believe I tried to flog them here before :-) Hope this doesn't look too desperate. I do plan to turn them into a book, if I find the time...

At least as far as I was concerned. Note that the link you gave in your post is broken.

I think you have the right spirit about it. Since you are using Haskell, you probably will find the Beseme Project useful. A conversation with Dr. Page would be very worthwhile, and there are lecture notes to draw inspiration from and problems to use.

Plus, the Beseme Project claims to have found a statistically significant result. Students that get an "A" or a "B" in the Beseme sections get better grades when they take Data Structures than students in traditional Discrete Math sections.

I should also point out that my observations are from within the United States, and non-American computer science tends to be less adverse to mathematics. Too bad I can't sit in on your course, it sounds interesting.

Personally, when I was a math major (at Northwestern), I never saw a "discrete math" course (and I took everything offered, except prob stats). Instead, I had set theory, algebra, topology, etc. When I recently started taking graduate CS courses, I found that there was a discrete math course required, but I had already covered the material.

Maybe "discrete math" courses were invented as catch-alls to meet the needs of CS, and that's why they sometimes get taught in CS departments?

...Wonders whether we do a disservice of bundling the teaching of mathematical concepts/notation and applied programming concepts (PL, algorithms, etc...).

Depends on what your aims are; and the manner in which you teach.

Often teachers try to fill buckets with their theory. I think you don't get a lot out of a student if you present Edmond's Blossom algorithm and than ask him/her to implement it, or teach some reduction trick, or to apply some master theorem. Most students will do that nicely, get through their exams, and most will forget all they learned within three weeks. Some buckets just have too many holes - but it's good for those students who do remember well.

Some teachers try to spark flames. I am still that young so I like to give students a book and a problem and then make them analyze, solve, and then implement the problem "hey, the problem reduces to finding disjoint sets in a bipartite graph; let's write that down and go Java." But this is hard work and students will certainly learn less theory, and, yeah, it's difficult sparking a flame in a wet towel - but it is good for those who are good problem solvers.

The biggest problems occur when "bucket fillers" try to be "flame sparkers" or vice versa; or when students are used to one kind of learning, and then get the other kind.

But the above is one big overgeneralization and, fortunately, in the end, it doesn't matter that much.
Bad students will always be bad students and the best students will always be the best despite of their studies.

Still haven't found a self-study text, so I went and applied for admission for a graduate course in Discrete Mathematics over at UTD. Will be interesting since I haven't seen the inside of classroom for some 24 years.

Have also been thinking of maybe trying to get a teaching gig at some point (since I'll likely have at least one kid in college for the next 12 years). Perhaps they can cut me a discount so I won't go totally broke (definite sticker shock going to the University bookstore today where the textbook for the class I want to take lists at $120).

It is a little frustrating to get lost in TAPL even though it is considered an introduction. I get the feeling topics in ATTPL are very interesting...too bad I can't make sense of them.

I was also thinking of taking a non-credit course at NYU or Columbia (or any other NYC/JC) school. Unfortunately they don't seem to offer classes in the evening. There should be seminars for working programmers who want to learn this stuff from a lecturer...hint hint to the LTU gurus ;)

Naive Computational Type Theory?

I skimmed this, and it looks neither as newbie friendly nor as concrete and broad in its coverage as TAPL.

YMMV, of course.

I notice that the word "Type Theory" means slightly different things depending on the context

Is this really different than any other branch of math? You have the pure theory and then the applications of that theory, and we frequently blur them together in casual usage.

For example, a book on pure domain theory will show how it can be applied to LC semantics, or a book on pure Category Theory will show how it can be applied to a problem from Topology. In these case, we generally don't make the distinction unless we need to.