Epilogue

First up, have a butcher’s at TypedLambda.epi. If you look hard enough, you’ll see that all sorts of implicit syntax is holding this thing together. Not only implicit argument synthesis, but implicit argument abstraction—the sort of thing which shows up with rank-n polymorphism. Getting this to behave at all sensibly was quite a big deal at the time and it’s still a bit garbled, to be honest. So let me try to make a clearer plan for version 2.

Epigram has implicit quantifiers, ∀_ and ∃_, which are distinct from their explicit counterparts. (In Lego, the implicit and explicit ∀ were identified, and this inevitably resulted in lots of little mishaps.) Epigram provides both implicit and explicit means to use and to construct elements of implicitly quantified types.

In the underlying type theory, everything is explicit. Use: the postfix _ inhibits implicit usage and instead converts its operand to an explicit function or pair.

Construction: as you might expect, there’s a λ_; meanwhile, prefix _ overrides an implicit field in a tuple.

What about elaborating implicit usage and construction? Implicit usage, also known as completion is by argument synthesis for ∀_ and second projection for ∃_. Implicit construction is by implicit quantification for ∀_ and witness synthesis for ∃_. But how do these mechanisms kick in? We’d better take a closer look at how type information flows around in typechecking before we can figure that out. We can only perform implicit construction when we’re pushing type information downward; completion we can do anytime.

Let me do something like Pierce’s ‘local type inference’ thing, and have judgments representing types going down and coming up. Note that I use to stand only for non-implicitly quantified types.

The first represents the situation where a type (possibly implicit) is being pushed into the elaboration of a concrete term. The second indicates that a (possibly implicit) type can be inferred for a concrete term. The third explains how this type may be completed to an explicit type. I write for the conjunction of and , compressing inference-then-completion.

Here are the downward rules. I write for a term other than an explicit constructor for an implicit quantifier. If we’re pushing in an implicit quantifier, we adjust the problem accordingly. If we have an explicit constructor, we follow the underlying theory.

The funny bullet is an anonymous nonce. You can’t make explicit reference to the implicitly bound variable. Fortunately, you can make implicit reference to it.

For explicit quantifiers and constructors, we now get

For terms other than abstraction and pairing in non-implicit types, we just infer and complete the type, then check it’s the one we want.

Meanwhile, going the other way, the completion rules go like this:

And the upward rules (a selection thereof)…

This entry was posted on Sunday, June 19th, 2005 at 2:09 pm and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.