[Haskell-cafe] Type-Level Programming
wren ng thornton
wren at freegeek.org
Sun Jun 27 00:46:22 EDT 2010
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.
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.
 See Tim Sheard's Omega for the logical conclusion of this process.
More information about the Haskell-Cafe