Epilogue

I thought I’d start writing a thing or two about the setup for the incarnation of Epigram we’re currently working on. At the heart of the thing is a Language Of Verifiable Evidence, which is all you need, really. You can stick a fancy syntax and lots of abbreviation mechanisms on top of it, and you can glue lots of erasure mechanisms and a compiler to the bottom of it, but in the middle, there’s this language whose (open) terms you can typecheck and evaluate, without any need for further elaboration, wishful thinking, or appeal to oracle. Is this a core language? I don’t know: that phrase has been used in so many ways.

The setup of this language is obsessively bidirectional, to the point of separating the syntactic categories for which types get pushed in and from which types are extracted.

Pushing types in: TYPE ∋ INTM
Extracting types: EXTM ∈ TYPE

We start with the rules for changing direction:

T ∋ s  if  s ∈ S  and  ⋆ ∋ S ≡ T
(s:S) ∈ S  if  ⋆ ∋ S  and  S ∋ s

I’m writing this in Greek just now: I’ll give the translation to ASCII in a bit. In Greek, I use underlining to show the embedding from EXTM to INTM, in aid of comprehension — it’s silent in ASCII. Embedding EXTM into INTM, two types for the same term collide, and we constrain them to be definitionally equal. If we want to turn an INTM into an EXTM, we have no choice but to provide a type annotation explicitly. Logically, the latter amounts to stating and proving a lemma as part of an indirect proof.

We’ll need sets, so here goes the usual cop-out.

⋆ ∋ ⋆

We’ll distinguish the layers of sets of sets when we have a good story about abstracting over layers. Something’s in the pipeline.

Here are functions. Note that S → T abbreviates Π S λ _ → T, making simple function types a special case of dependent function types. Also note that we replace the bound variable of the abstraction with a typed free variable for typechecking purposes: this will be handy in a moment.

⋆ ∋ Π S T  if  ⋆ ∋ S  and  S→⋆ ∋ T
Π S T ∋ λ v → t  if  for fresh p, T p^S ⇓ T’  and  T’ ∋ t[p^S/v]

Logically, the INTMs correspond to introduction rules. The EXTMs tell us how to use stuff in a way that lets you read off what you’ve got. Here are typed free variables (we never meet a bound variable) and application.

p^S ∈ S
f s ∈ T’  if  f ∈ Π S T  and  S ∋ s  and  s ⇓ s’  and  T s’ ⊳ T’

What’s that at the end? Once we’ve typechecked the argument s, we can evaluate it, yielding value s’, then compute the result of value application T s’. The types we push in and out are VALs, to a good approximation, the subset of INTM which has nowhere the indirect (s:S) construction. We say that the corresponding EXTM subset is that of NEUtral terms.

We have evaluation judgments INTM ⇓ VAL and EXTM ⇓ VAL which are mostly structural, except where type annotations are stripped and where computation happens. In the latter case, we appeal to the compuation judgment, VAL ELIM ⊳ VAL, where stuff actually happens.

(s:S) ⇓ s’  if  s ⇓ s’
s ⇓ s’  if  s ⇓ s’

⋆ ⇓ ⋆

Π S T ⇓ Π S’ T’  if  S ⇓ S’  and  T ⇓ T’
λ v → t ⇓ λ v → t

p^S ⇓ p^S
f s ⇓ t’  if  f ⇓ f’  and  s ⇓ s’  and  f’ s’ ⊳ t’

Computation for functions does β_v if it finds a λ, and produces a bigger neutral term if the function is neutral.

(λ v → t) s’ ⊳ t’  if  t[s'/v] ⇓ t’
f’ s’ ⊳ f’ s’

Something’s still missing. I haven’t told you what the definitional equality is. It amounts to rather more than being identified (up to α-conversion of bound variables) by evaluation: we do untyped evaluation, then typed quotation

T ∋ s ≡ t  if  s ⇓ s’  and  t ⇓ t’  and  T ∋ s’ ⇑ u  and  T ∋ t’ ⇑ u

Quotation standardises the result of evaluation, producing a unique normal form. In particular, it performs some η-expansion. We have type-directed quotation for values TYPE ∋ VAL ⇑ INTM and type-reconstructing quotation for neutrals NEU ⇑ EXTM ∈ TYPE. In the first instance, quotation is completely structural, following the typing rules, except at Π-types, where we have the following instead:

Π S T ∋ f ⇑ λ v → t[v/p^S]  if  for fresh p, T p^S ⇓ T’  and  f p^S ⇓ t’  and  T’ ∋ t’ ⇑ t

Isn’t that it? Nope. λ is not the ultimate: you can’t encode datatypes with dependent elimination impredicatively in an intensional setting. In a later post, I’ll show how to extend this machinery to some actual data.

[Edit: noticed some exterms weren't underlined!]

This entry was posted on Sunday, January 3rd, 2010 at 11:26 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.