Fixing Twelf via indirection

One thing I've been thinking about a bit lately is whether it might be possible to smooth over quite a number of the problems with Twelf via essentially providing an additional meta-language. For example, something like a Haskell library that can interface with the Twelf server. It would be possible to essentially use the library to do things the way they are done now, but also use something like the parametricity trick from "Boxes Go Bananas" to programmatically construct some bits of proofs. I guess I'm kind of thinking of Delphin lite perhaps. But then it would be possible to write combinators for giving you "generic" sums and products and false elimination.

The primary problem is that while it would be possible to enforce that HOAS is used correctly, it would be difficult to ensure that only well-typed LF terms are manipulated. The other serious problem is that it would require building a considerable amount on intelligence into the system to be able to provide comprehensible error messages. As it is Twelf doesn't always provide particularly enlightening error messages, so it would perhaps even require adding heuristics to interrogate the twelf-server for additional information that most users don't know to consult.

However, perhaps after I've had more time to work with Coq this semester, I'll conclude that such effort is pointless.  Adam Chlipala was pushing programming entirely in Coq while I was at ICFP.  It is something I've certainly considered before, but I don't think I have any projects at the moment where I can really justify the learning curve for doing so.

Leave a Comment