Comments on: W-types: good news and bad news http://www.e-pig.org/epilogue/?p=324 for Epigram Sun, 6 Nov 2011 09:25:45 +0000 http://wordpress.org/?v=2.8.4 hourly 1 By: Adam http://www.e-pig.org/epilogue/?p=324&cpage=1#comment-71096 Adam Tue, 15 Jun 2010 07:48:31 +0000 http://www.e-pig.org/epilogue/?p=324#comment-71096 Of course all _propositional_ equalities hold under an absurd hypothesis, but I think Conor's point is rather that the _definitional_ (judgmental) equality also collapses if it identifies the different W-type implementations of zero. Definitional equality needs to make sense even on open terms, as otherwise computation on them can "go wrong" without a false hypothesis to blame. Of course all _propositional_ equalities hold under an absurd hypothesis, but I think Conor’s point is rather that the _definitional_ (judgmental) equality also collapses if it identifies the different W-type implementations of zero. Definitional equality needs to make sense even on open terms, as otherwise computation on them can “go wrong” without a false hypothesis to blame.

]]> By: Brandon http://www.e-pig.org/epilogue/?p=324&cpage=1#comment-71078 Brandon Sat, 12 Jun 2010 21:51:30 +0000 http://www.e-pig.org/epilogue/?p=324#comment-71078 I don't see how the last example is any worse than the issues that have already been dealt with in OTT. In a context with a hypothesis in 0 you will already be able to prove absurdities, but as long as these equalities over terms in the W-type are propositional you would still need to explicitly coerce by them, and if you are going to that trouble you can get up to worse mischief simply by induction on the hypothesis from 0. I don’t see how the last example is any worse than the issues that have already been dealt with in OTT. In a context with a hypothesis in 0 you will already be able to prove absurdities, but as long as these equalities over terms in the W-type are propositional you would still need to explicitly coerce by them, and if you are going to that trouble you can get up to worse mischief simply by induction on the hypothesis from 0.

]]> By: Conor http://www.e-pig.org/epilogue/?p=324&cpage=1#comment-70946 Conor Sun, 18 Apr 2010 10:12:28 +0000 http://www.e-pig.org/epilogue/?p=324#comment-70946 Sorry for slow response: I wonder if we can set this blog up so that pending comments get more attention. But anyhow, the impact of this observation about W-types (infinitely many implementations of zero, all provably equal but definitionally distinct), is just that we need a slightly larger base set of types from which to work. Whatever the base set, we apply the same technique to compute the meaning of equations. In Epigram 2, we don't take W-types as the primitive source of inductive structure. Instead, we supply a universe of inductive types, giving first-order data a first-order representation. We've just written a paper about it: <a href="http://personal.cis.strath.ac.uk/~dagand/levitation.pdf" rel="nofollow">The Gentle Art of Levitation.</a> Sorry for slow response: I wonder if we can set this blog up so that pending comments get more attention.

But anyhow, the impact of this observation about W-types (infinitely many implementations of zero, all provably equal but definitionally distinct), is just that we need a slightly larger base set of types from which to work. Whatever the base set, we apply the same technique to compute the meaning of equations.

In Epigram 2, we don’t take W-types as the primitive source of inductive structure. Instead, we supply a universe of inductive types, giving first-order data a first-order representation. We’ve just written a paper about it: The Gentle Art of Levitation.

]]> By: Rob Jellinghaus http://www.e-pig.org/epilogue/?p=324&cpage=1#comment-70942 Rob Jellinghaus Mon, 12 Apr 2010 22:26:50 +0000 http://www.e-pig.org/epilogue/?p=324#comment-70942 There seems to be a punchline missing, though. The "Observational Equality, Now!" paper bases its Agda 2 implementation on a W-set constructor for trees. Is it the case (I'm only barely familiarizing myself with dependent types) that the very extensionality of W-types is what OTT tries to overcome by using observable equality? Or does this W-type non-canonicity issue have bad implications for OTT itself? There seems to be a punchline missing, though. The “Observational Equality, Now!” paper bases its Agda 2 implementation on a W-set constructor for trees. Is it the case (I’m only barely familiarizing myself with dependent types) that the very extensionality of W-types is what OTT tries to overcome by using observable equality? Or does this W-type non-canonicity issue have bad implications for OTT itself?

]]> By: Luke Palmer http://www.e-pig.org/epilogue/?p=324&cpage=1#comment-70903 Luke Palmer Thu, 11 Mar 2010 11:03:18 +0000 http://www.e-pig.org/epilogue/?p=324#comment-70903 Interesting stuff, thanks for taking the time to write it down. It's a bit over my head, but I think I got most of the important bits. Interesting stuff, thanks for taking the time to write it down. It’s a bit over my head, but I think I got most of the important bits.

]]>