tag:blogger.com,1999:blog-11295132.post3902722215962593314..comments2017-05-19T20:38:17.775-07:00Comments on A Neighborhood of Infinity: The AntidiagonalDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-11295132.post-48854248967049663812013-05-17T13:28:53.359-07:002013-05-17T13:28:53.359-07:00"y = au+bv+uv" -- shouldn't this be ..."y = au+bv+uv" -- shouldn't this be "av+bu+uv"? Like this:<br /><br />(ab)² = y + ab<br />a²b² - ab = y<br />(u + a)(v + b) - ab = y<br />uv + ub + av = y<br />nooodlnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-83863279915340773842009-04-28T02:25:00.000-07:002009-04-28T02:25:00.000-07:00I'm wondering if the Blogger bug you are referring...I'm wondering if the Blogger bug you are referring to is the use of the less-than and greater-than symbols. You should be able to use the <A HREF="http://en.wikipedia.org/wiki/Character_encodings_in_HTML#XML_character_entity_references" REL="nofollow">character entity</A> &lt; to get < and &gt; to get >.Sean Leatherhttp://www.blogger.com/profile/02951502639017426632noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-37649638897884792212007-09-03T02:07:00.000-07:002007-09-03T02:07:00.000-07:00This is really interesting stuff. I'm looking forw...This is really interesting stuff. I'm looking forward to the next instalment. It's good see some interest in witnesses to inequality. In Epigram, we sometimes like to present the equality test as a view on two elements of a type: they must be obtained either by duplication, or by projection from what you're calling the antidiagonal. Good name, I think.<BR/><BR/>We've tended to chop things up a little differently, because we can. We're not exactly aiming for T-1, but rather T-{t} for a specific t:T. Just as category theory eventually stops being lattice theory, type theory eventually stops being combinatorics, more or less at the point where witnesses matter.<BR/><BR/>As for generic programming, it's not exactly Coq, but I should plug my friend Peter Morris's work on the generic construction of various things in a dependently typed setting, starting with equality decision (informative rather than Boolean). I should also recommend my friend Ulf Norell's new implementation of Agda, which I strongly suspect would be way more fun for this sort of thing than Coq (or Epigram 1, for that matter).<BR/><BR/>Meanwhile, us Epigram folks have been thinking real hard about how to set up a datatype system which comes with a built-in notion of generic programming. On paper, the operation you seek should jack up more or less directly from the fact that finite enumerations support element removal. (Note that you can't take 1 from 0, but you can remove any z:0 from 0. Of course, you can take 0 from 0*0.)<BR/><BR/>If A is splittable and (B a) is splittable for all a:A, then (Σa:A. B a) is splittable. Subtracting (a, b) gives you (A-a) + (B a - b). Note that you need an <I>informative</I> analysis method to see this. Suppose you have some (a', b') to compare with (a, b). It only makes sense to compare b' with b if you have identified a' with a.<BR/><BR/>We're hoping that eventually we'll have enough time to assemble a system from the various experiments we have on the slab. Dependently typed programming relies on informative testing, so 'witness structures' like the antidiagonal do start to show up. In 'The view from the left', James McKinna and I defined element removal for simple type expressions (expressing the pious hope that it might one day be generic), followed by antityped terms (terms with a leftmost type error).<BR/><BR/>So I should shut up and get on with Epigram 2. But thank you. It's really nice to read posts which I can point to and say 'we should make that stuff just work'. And so we shall.Conorhttp://www.cs.nott.ac.uk/~ctmnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-26923743967764256592007-09-02T22:03:00.000-07:002007-09-02T22:03:00.000-07:00Eelis,What I meant was what does Coq have to offer...Eelis,<BR/><BR/>What I meant was what does Coq have to offer in terms of generic programming (as in Generic Haskell or PolyP)? Any language that allows constraints on types makes it easy to define the type of distinct pairs. But what I'm really after is a cleaner way to construct the same thing *without* using constraints. For one thing, working out how to do this without constraints led to a general way to compactly represent pairs of structures that have equal substructures. That wouldn't have become apparent if I just used constraints.<BR/><BR/>Nonetheless, Coq does look interesting and I'll give myself a crash course soon.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-4466167550373788992007-09-02T20:58:00.000-07:002007-09-02T20:58:00.000-07:00"I wonder what Coq has to offer here."In Coq, the ..."I wonder what Coq has to offer here."<BR/><BR/>In Coq, the type family of distinct pairs can be defined simply as:<BR/><BR/> Definition DistinctPair (T: Set): Set := { x: T * T | fst x <> snd x }.<BR/><BR/>Inhabitants of instances of this family carry with them proofs that the first element is distinct from the second. For example, we can exhibit the inhabitant (1, 2) of the type (DistinctPair nat) as follows:<BR/><BR/> Definition p12: DistinctPair nat := exist _ (1, 2) (n_Sn 1).<BR/><BR/>n_Sn is a standard library lemma of type (forall n: nat, n <> S n), and so (n_Sn 1) is a proof that 1<>2.Eelisnoreply@blogger.com