Comments on: Towards Observational Equality http://www.e-pig.org/epilogue/?p=102 for Epigram Sun, 6 Nov 2011 09:25:45 +0000 http://wordpress.org/?v=2.8.4 hourly 1 By: Conor http://www.e-pig.org/epilogue/?p=102&cpage=1#comment-4293 Conor Mon, 30 Jan 2006 16:00:32 +0000 http://www.e-pig.org/epilogue/?p=102#comment-4293 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. 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.

]]> By: Conor http://www.e-pig.org/epilogue/?p=102&cpage=1#comment-4292 Conor Mon, 30 Jan 2006 13:39:02 +0000 http://www.e-pig.org/epilogue/?p=102#comment-4292 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! 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!

]]> By: Conor http://www.e-pig.org/epilogue/?p=102&cpage=1#comment-4282 Conor Thu, 26 Jan 2006 23:41:22 +0000 http://www.e-pig.org/epilogue/?p=102#comment-4282 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. 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.

]]>