It has been a little while since I posted anything. So here’s a general update about my work and other aspects of my life.

I’ve been passively thinking about Dana, but not doing very much significant. I have abandoned the RTS language on the grounds that it is too hard for my little mind right now. Hopefully I will come back to it, but it can be safely moved further down in the queue without hurting my progress.

That brings me back to the dependent typed core. I’ve switched directions and decided that it really ought to be total. In experimenting with how to bring back partiality to a total language, it finally sunk in how partiality is a monad in its essence. It is in the very same way Maybe is, though my practical ideas about the essence of nontermination prevented me from seeing that.

I’ve been fooling around with the semantics of system IG, and have gotten nowhere interesting. Whatever beautiful connection between application and typing there is, I haven’t seen it yet.

Since typechecking arbitrary terms in system IG is undecidable, I’ve been trying to write an “interactive typechecker”: essentially a library for typechecking. Various inference algorithms can be built on top, but their correctness follows from the underlying library. I am stuck on the representation of conversion proofs between lambda terms.

All of these are rather minor problems that can be worked through with a little thought. I’ve been distracted, however, because of a woman named Anna, with whom I’ve been having at least two hour conversations almost every night. I had forgotten what it meant to have good conversations about nontechnical things (it’s really nice). We seem to like each other, despite my friend’s warnings about her being insane or something :-). I’m interested to see where it goes.

Oh and I’m starting school again in the summer, to finish by Bachelors in mathematics. The intention being to go do a PhD program with Paul Hudak, if that can be arranged, or something similar.

More meat soon.


3 thoughts on “Update

  1. Shouldn’t one of Anna’s friends warn her about you instead? Dependent types, monads, nontermination, oh my!

  2. Whenever someone talks about a dependently-typed language, I’m always tempted to say “Why not just use Coq? All the infrastructure makes things easier, especially for proving things.”

  3. Robin: Well, it’s basically the same reason I argued for using PiSigma earlier. I like the flexibility of having my own implementation, to move things here and there, to modify the details as the semantic ideas crystalize. In implementing PiSigma, I learned a lot and cut out a lot of its cruft, got a firm understanding of boxes and their semantics, why the unboxing operator was a bad idea, etc.

    Besides, Coq is a pretty large system, not as simple and beautiful as I’d like. For example, the universe stratification constraints seem far too complicated, though I admit there may not be a better way. But it’s something I want to play with. I have a feeling there’s something to Girard’s impredicativity (not Type:Type, but ((A:Type) -> (A -> Type) -> Type) : Type, which is amazingly still consistent).

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s