tag:blogger.com,1999:blog-11295132.post1814777119392201914..comments2016-09-24T21:29:58.885-07:00Comments on A Neighborhood of Infinity: The Categorification of the NaturalsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger10125tag:blogger.com,1999:blog-11295132.post-88538621199935634382010-03-26T09:15:36.882-07:002010-03-26T09:15:36.882-07:00g,
Powers had crossed my mind, but it never enter...g,<br /><br />Powers had crossed my mind, but it never entered my head that this gave a nice way to convert from binary to 'unary'. Awesome!sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-72488911686170301972010-03-26T09:01:34.489-07:002010-03-26T09:01:34.489-07:00I changed type families to functional dependencies...I changed type families to functional dependencies and added exponentiation. Exponentiation is "positional notation" because a function like Three -> Two is encoding a three-digit binary number.<br /><br />http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24391#a24391<br /><br />I tried removing Plussable and Timesable, but no luck because these two declarations <br /><br />> instance (Canonicable a Void, Canonicable b y) => Canonicable (Either a b) y where<br />> instance (Canonicable a (Maybe x), Canonicable b y, Canonicable (Either x y) c) => Canonicable (Either a b) (Maybe c) where<br /><br />cause a conflict and even canonical :: Either Void Void -> Void doesn't work.<br /><br />There must be strong connections between this categorification and combinatorial species. The antidiagonal (http://blog.sigfpe.com/2007/09/type-of-distinct-pairs.html) is a categorified version of n(n-1) and also combinatorial species.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-85440280151402083832010-02-15T14:36:54.478-08:002010-02-15T14:36:54.478-08:00Cool! Now Categorify Conway Games! ;-)Cool! Now Categorify Conway Games! ;-)leithaushttp://www.blogger.com/profile/01069099703796397027noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-63118717412892539112010-02-12T02:10:49.408-08:002010-02-12T02:10:49.408-08:00A few days after I've read the article I happe...A few days after I've read the article I happened to need the addition isomorphism[1] to prove that the union of finite sets is finite.<br /><br />Nice coincidence :)<br /><br />[1] http://code.haskell.org/~Saizan/Agda/NatCat.htmlSaizanhttp://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-31010236530611560132010-02-11T00:24:32.346-08:002010-02-11T00:24:32.346-08:00A quibble: you don't need induction to have ad...A quibble: you don't need induction to have addition and multiplication be the usual functions: if you drop induction from Peano arithmetic, the other Peano axioms still have that addition and multiplication are defined and have the usual results for all closed terms (i.e., natural numbers). You do need induction to prove that these functions are total, commutative, associative, &c.stewarthttp://openid.textproof.com/stewartnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-79958284282714746782010-02-09T11:34:20.926-08:002010-02-09T11:34:20.926-08:00For "Void", I tend to use this:
> vo...For "Void", I tend to use this:<br /><br />> void_elim :: Void -> a<br />> void_elim x = x `seq` error "You broke the type system!"<br /><br />Then you can eliminate all use of "undefined" and partial pattern matching; for example, in the case of Plussable Void b:<br /><br />> plus (Left v) = void_elim v<br />> plus (Right a) = a<br /><br />And in Timesable:<br /><br />> times (v,_) = void_elim vryanihttp://ryani.livejournal.com/noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-56951979249553207102010-02-08T09:04:24.625-08:002010-02-08T09:04:24.625-08:00i'd love to see a coq version of thisi'd love to see a coq version of thiszghost123http://www.blogger.com/profile/12592217260370508702noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-35440912271756770272010-02-07T15:53:41.108-08:002010-02-07T15:53:41.108-08:00Thanks to Paczesiowa for spotting the hopelessly s...Thanks to Paczesiowa for spotting the hopelessly silly typo I previously had in the first axiom.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-90326391659288853182010-02-06T17:41:43.780-08:002010-02-06T17:41:43.780-08:00The names starting with upper case are the types. ...The names starting with upper case are the types. The names starting with lower case are the elements of the types. I'm using the names zero, one, two, ... to label the elements of Void, One, Two, ...<br /><br />For example, the three elements of Three are {zero, one, two}.<br /><br />Zero has no elements, but One and above all contain zero (with lower case).<br /><br />Make more sense?sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-38985645893626348562010-02-06T17:31:42.132-08:002010-02-06T17:31:42.132-08:00You said that Void is representing zero, however d...You said that Void is representing zero, however defined <br /><br />zero :: Maybe a<br />zero = Nothing<br /><br />Hmmm... I didn't get this bit :).<br /><br />Nice post, by the way.metefichahttp://www.blogger.com/profile/15462135710203643022noreply@blogger.com