tag:blogger.com,1999:blog-11295132.post115047538773059338..comments2017-03-14T08:49:33.474-07:00Comments on A Neighborhood of Infinity: A Taylor Series for TypesDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-11295132.post-33671979617844858362008-02-06T05:31:00.000-08:002008-02-06T05:31:00.000-08:00This is probably nitpicking, but:>> If I only give...This is probably nitpicking, but:<BR/><BR/>>> If I only give you an unordered pair and a bit, you can't recover my original ordered pair. Unless, somehow, you know that was the very bit which was used to record the order when the pair was scrambled.<BR/><BR/>I think this argument is not right (although the conclusion is still correct). Forget about unordered pairs for the moment and consider 2*2 and 2+2. If I give you Left True, you can't recover the original pair, unless you know that Left was used to encode that the left bit was true and the value true was used to encode the right bit being true. Nevertheless, these types are isomorphic, and it's easy to show an isomorphism.<BR/><BR/>Although a positive answer to the question "If I give you an element of Y, can you recover the element of X I used to make it?" is sufficient to show that there is an isomorphism, a negative answer just shows that there's no _unique_ isomorphism. If you have a total order on X, you can try making an isomorphism using the bit to record the order. However, it can't be done because 2*X^2/2 has more elements than X^2. This is because (x,x) has only one representation in X^2, but two in 2*X^2/2 (specifically (false, {x,x}) and (true, {x,x})). So it's the presence of the diagonal, not the lack of knowledge about what the bit does that prevents the isomorphism.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-62694810387070706042007-04-11T15:54:00.000-07:002007-04-11T15:54:00.000-07:00It seems to me that X^2 is isomorphic to 2*X^2/2. ...It seems to me that X^2 <I>is</I> isomorphic to 2*X^2/2. The former is an ordered pair, and the latter is (depending upon which way you want to look at it) an unordered pair X^2/2 (i.e. also a bag) with a bit which then defines it to be an ordered pair.<BR/><BR/>Oh wait.<BR/><BR/>Now that I write that paragraph I see what you mean! :p Is it that you also need to know the encoding scheme used for the positioning of the two elements of the pair? ... how the bit actually tells you which way around they go?<BR/><BR/>It seems to me that if taken at "type level" then X^2 is still 'essentially' isomorphic to 2*X^2/2... if you have an unordered pair and a bit you have <B>the information to construct</B> an ordered pair. Granted you might not be able to recreate a <I>particular</I> pair, and hence my qualifier about "at type level" :)Porgeshttp://porg.es/blognoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-69535240564232375472006-11-12T04:11:00.000-08:002006-11-12T04:11:00.000-08:00This is certainly something I've been kicking arou...This is certainly something I've been kicking around for a few years, but it requires a little caution. As with Taylor series in analysis, you've got to worry about the remainder. The series summation translates to typespeak as ‘for some finite number of elements’, which means you don't get a Taylor series for Stream. If you require that each possible shape of F has finitely many positions, then you do get a Taylor series, or perhaps we should say a Taylor <i>species</i>.<br /><br />It's also quite weird trying to figure out how to work with these jumbled up data structures. There are lots of things which intuitively should make sense, eg these bags X^n/n!, or circles X^n/n (the derivative of an (n+1)-circles is an n-tuple). Finding a notation which seduces you into writing truths is harder. Eg, X^2 is not isomorphic to 2*X^2/2. If I only give you an unordered pair and a bit, you can't recover my original ordered pair. Unless, somehow, you know that was the very bit which was used to record the order when the pair was scrambled.<br /><br />So although it's a very attractive idea, it's been quite tricky getting the tools together to make it precise in the context of mucking about more generally with quotients. (By the way, Epigram 2 will support quotients: we're planning to hack up all of this stuff.)<br /><br />However, the same sort of story showed up when I was trying to characterise tail-recursive iteration over trees. There, the thing that pops out is a sort of ‘Remainder Theorem’ for types, giving rise to a power series construction by repeated division. It turns out that division means (wlog) ‘finding the context of the <i>leftmost</i> hole’. You would expect that finding <i>all</i> n holes left to right, then choosing a permutation is the same as finding n holes in any order, and so it is. The beginnings of an article about this misadventure may be found <a href="http://www.cs.nott.ac.uk/~ctm/Dissect.pdf">here</a>.<br /><br />But yeah, this stuff is a barrel of laughs. With a hole in it.Conorhttp://www.blogger.com/profile/16369842679510868375noreply@blogger.com