tag:blogger.com,1999:blog-11295132.post6189536188959217455..comments2014-04-16T10:57:46.206-07:00Comments on A Neighborhood of Infinity: Memoizing Polymorphic Functions with High School Algebra and QuantifiersDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-11295132.post-68239686369582057462009-11-29T16:57:21.869-08:002009-11-29T16:57:21.869-08:00Dear Author blog.sigfpe.com !
It you have correct...Dear Author blog.sigfpe.com ! <br />It you have correctly told :)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-91894991700553989172009-11-09T10:46:52.940-08:002009-11-09T10:46:52.940-08:00This was great and challenging. I followed the lin...This was great and challenging. I followed the link back to your old post about data and codata and a few more lights turned on upstairs. Kind of like skiing a blue run after a black. Thanks for continuing this blog!T_S_http://www.blogger.com/profile/08087102167160417535noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-30608224836122443062009-11-09T10:34:41.672-08:002009-11-09T10:34:41.672-08:00ertai,
Thanks for that.
It makes me grumpy when ...ertai,<br /><br />Thanks for that.<br /><br />It makes me grumpy when the Haskell compiler forces me to implement a function of type voidElim ∷ Void → ∀ a· a when it seems obvious to me that a complete implementation should take zero lines of code. :-)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-82207367713688101012009-11-09T06:43:56.088-08:002009-11-09T06:43:56.088-08:00I also think that a n=0 version would help underst...I also think that a n=0 version would help understanding better the solution.<br /><br /><b><br />> type T0 f = T f Void <br /> <br />> voidElim ∷ Void → ∀ a· a <br />> voidElim _ = error "voidElim: impossible" <br /> <br />> memoize0 ∷ Functor f ⇒ (∀ a· [a] → f a) → T0 f <br />> memoize0 f = memoize (λ(_ , xs) → f xs) <br /> <br />> memoize0' ∷ Functor f ⇒ T0 f → ∀ a· [a] → f a <br />> memoize0' t xs = memoize' t (voidElim, xs)<br /></b>ertaihttp://www.blogger.com/profile/01280276982496105053noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-38839612122884871712009-11-08T13:10:01.101-08:002009-11-08T13:10:01.101-08:00Shin no Noir,
The constraint is missing only beca...Shin no Noir,<br /><br />The constraint is missing only because I could accidentally get away with it without the compiler complaining.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-74154822824970543302009-11-08T12:43:03.541-08:002009-11-08T12:43:03.541-08:00Is there a reason why you don't include the (F...Is there a reason why you don't include the (Functor f =>) constraint in the type of yoneda? It would make yoneda less general, but on the other hand would make it more symmetric with its inverse yoneda'.Shin no Noirhttp://www.blogger.com/profile/08974372500960094990noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-80596328439618765112009-11-08T07:11:57.793-08:002009-11-08T07:11:57.793-08:00Sjoerd,
Maybe I should have said ir more clearly,...Sjoerd,<br /><br />Maybe I should have said ir more clearly, but for n=0, (n->a,[a]) -> f a is the same as [a]. I could add a line to exhibit that isomorphism.<br /><br />Or maybe you meant the more philosophical question of "why when looking to memoize [a] -> f a are we led to a whole family of types?". Which I'm not sure how to answer.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-90707210852225513712009-11-08T02:47:20.949-08:002009-11-08T02:47:20.949-08:00What I don't understand is that you want to me...What I don't understand is that you want to memoize forall a. [a] -> f a, and end up with memoization for forall a. (n -> a, [a]) -> f aSjoerd Visscherhttp://www.blogger.com/profile/10698430967044536619noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-91188890650342170372009-11-08T01:36:28.414-08:002009-11-08T01:36:28.414-08:00Great work! I will still need some time to fully d...Great work! I will still need some time to fully digest this but...<br /><br />Just a quick remark, in your definition of Exists:<br /><br /><b><br />data Exists f a = forall a. Exists (f a)<br /></b><br /><br />The type parameter 'a' is useless and misleading since it is different<br />from the forall one. I suggest:<br /><br /><b><br />data Exists f = forall a. Exists (f a)<br /></b>ertaihttp://www.blogger.com/profile/01280276982496105053noreply@blogger.com