[Haskell-cafe] Type-Level Programming

[wren ng thornton]

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