OK, I think I have a plan. I’m gonna
- hack in Bool and W directly, leaving ‘data’ alone for the moment
- add the relevant extra eliminators for equations (dom, cod, sym)
- make coe go into functions, pairs and trees
- add a constructor for extensionality
If that works out, it’s time to rethink data, then remove Bool and W. I’ll keep youse posted.
I’ve done the first three of these; I’ve added two and two with the W-type representation of Nat; some useful stuff works. But I’ve also hit some gremlins…
I had a bit of a nightmare with some of the diagnostics, which were quoting terms containing de Bruijn levels, resulting in negative de Bruijn indices. I’ve also hit the more serious issue that levels (introduced only by quote, as it happens) are untyped. Recall that quote is typeless quotation of beta-normal forms. That don’t work no mo, because computation relies on equality testing, which is typed: you need to produce typed refs when you go under a binder, so you need to know the type of a lambda, ya da ya da ya da.
If we can get by with typed quotation, we’re out of dodge on this one.
If you check out tests/WCoe.suit, you’ll find lists constructed from W-types, and you’ll also find a hypothetical q : List X = List Y pushing through a little List X, leaving a little List Y with coerced elements. If you run the thing, you’ll see that the equality proof being pushed has a tendency to grow…
Still, it goes. Ext coming up!
We have extensionality in the form
prf : all x0:S0 => all x1:S1 => all xq:(x0:S0)=(x1:S1) => (f0 x0 : T0) = (f1 x1 : T1)
—–
ext {(f0 : all x0:S0 => T0) = (f1 : all x1:S1 => T1)} prf :
(f0 : all x0:S0 => T0) = (f1 : all x1:S1 => T1)
That’s a synth form (it needs to be, because it can grow a spine), but I should also add the corresponding and less noisy check form.
I’ve proved the induction principle for Nat (aka W Two So), which relies crucially on proving that two functions from Zero are equal.
Which isn’t much of a test, I grant you, but there’ll be more in a bit.