tag:blogger.com,1999:blog-11295132.post115732611535122088..comments2017-03-14T08:49:33.474-07:00Comments on A Neighborhood of Infinity: Infinitesimal TypesDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-11295132.post-40089976135662519602014-09-11T11:36:41.296-07:002014-09-11T11:36:41.296-07:00Building on this: Consider a particular space x (w...Building on this: Consider a particular space x (which may have positive measure). Then a differential with respect to x should be a <i>finite set of points</i>. The sum x + dx is simply the union of the spaces, which preserves the measure of x. To carry out x/dx, you form an equivalence relation R so that the members of x/R have the same measure and |x/dx| = |dx|, and then identify each of the members with an element of dx.Kate Candyhttp://www.blogger.com/profile/14525055415849205916noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-34102596961642899792011-07-16T08:35:56.530-07:002011-07-16T08:35:56.530-07:00I also see a connection to the boundary operator o...I also see a connection to the boundary operator on chains in algebraic topology:<br />http://en.wikipedia.org/wiki/Chain_%28algebraic_topology%29Per Persson (md2perpe)http://www.blogger.com/profile/15762511809361135623noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-46340674132104381522011-07-16T08:31:14.526-07:002011-07-16T08:31:14.526-07:00The d^2 = 0 is also the case of the exterior deriv...The d^2 = 0 is also the case of the exterior derivative for differential forms:<br />http://en.wikipedia.org/wiki/Differential_form#Exterior_differential_complexPer Persson (md2perpe)http://www.blogger.com/profile/15762511809361135623noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-2455594326138291812011-03-17T13:35:29.449-07:002011-03-17T13:35:29.449-07:00Snorri,
I did eventually come up with an interpre...Snorri,<br /><br />I did eventually come up with an interpretation of D^2=0 for types. See <a href="http://blog.sigfpe.com/2010/08/constraining-types-with-regular.html" rel="nofollow">here</a>.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-72097962828564205062011-03-17T13:32:32.078-07:002011-03-17T13:32:32.078-07:00Hmm. Reminds me of monads in Haskell.Hmm. Reminds me of monads in Haskell.Snorri Agnarssonnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-48074270206609416832009-11-22T23:12:12.072-08:002009-11-22T23:12:12.072-08:00I don't suppose there's anything even rese...I don't suppose there's anything even resembling singleton types in Haskellâ€¦is there?Peter Davishttp://www.blogger.com/profile/10421999352110832388noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-27014891287701160982008-05-21T13:50:00.000-07:002008-05-21T13:50:00.000-07:00d^0 = 0 corresponds to "get rid of the constants"....d^0 = 0 corresponds to "get rid of the constants". Ideas are now forming in my brain but I don't know if they'll go anywhere.Roberthttp://www.blogger.com/profile/10746976399050925428noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-42088363355522341772008-05-21T02:38:00.000-07:002008-05-21T02:38:00.000-07:00Linear logic also bans contraction. This correspon...Linear logic also bans contraction. This corresponds to not being able to avoid using the hole. Or perhaps that corresponds to weakening. I forget whether I'm going forwards or backwards.<BR/>In any case, is it so that d^0 = 0 rather than 1?Roberthttp://www.blogger.com/profile/10746976399050925428noreply@blogger.com