Andrew Coppin wrote:
I think I looked at Coq (or was it Epigram?) and found it utterly incomprehensible. Whoever wrote the document I was reading was obviously very comfortable with advanced mathematical abstractions which I've never even heard of.
One of the things I've found when dealing with--- er, reading the documentation for languages like Coq, is that the class of problems which motivate the need to move to such powerful formalisms are often so abstract that it is hard to come up with simple practical examples of why anyone should care. There are examples everywhere, but complex machinery is only motivated by complex problems, so it's hard to find nice simple examples.
In particular, I've noticed that once you start *using* Coq (et al.) and trying to prove theorems about your programs, the subtle issues that motivate the complex machinery begin to make sense. For example, there's a lot of debate over whether Axiom K is a good thing or not. Just reading the literature doesn't shed any light on the real ramifications of having the axiom vs not; you really need to go about trying to prove definitional equalities and seeing the places where you can't proceed without it, before you can appreciate what all the hubbub is about.
It's a bit like trying to learn Prolog from somebody who thinks that the difference between first-order and second-order logic is somehow "common knowledge". (FWIW, I have absolutely no clue what that difference is.
First-order means you can only quantify over simple things. Second-order means you can also quantify over quantification, as it were.
For example, the type system of simply-typed lambda calculus is 1st-order intuitionistic propositional logic, and System F (i.e., STLC + rank-n polymorphism) is 2nd-order. (F_omega is higher-order, but that's one of those wormholes in the lambda cube.)
Though "higher-order" is a much abused term, which may cause some of the confusion. The higher-orderness discussed above has to do with quantification within types, which has to do with higher-orderness of the related logics. But we can also talk about a different sort of higher-orderness, namely what distinguishes System F from F_omega, or distinguishes LF from ITT. In STLC we add a simple language of types at a layer above the term layer, in order to make sure the term layer behaves itself. After hacking around we eventually decide it'd be cool to have functions at the type level. But how to we make sure that our types are well-formed? Well, we add a new layer of simple "types" on top of the type layer--- which gives us a second-order system. We could repeat the process again once we decide we want kind-level functions too.[1]
To take a different track, in cognitive science people talk about "theory of mind", i.e. the idea that we each theorize that other people have minds, desires, beliefs, etc. A first-order theory of mind is when we attribute a mind to other people. A second-order theory of mind is when we attribute a theory of mind to other people (i.e., we believe that they believe that we have a mind). Etc.
In epistemic/doxastic logics we can talk about first-order knowledge/beliefs, that is beliefs in simple propositions. But we can also talk about second-order beliefs, that is beliefs about beliefs. Etc.
[1] See Tim Sheard's Omega for the logical conclusion of this process. -- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
