tag:blogger.com,1999:blog-1777990983847811806.post8137932186432001110..comments2021-04-13T23:13:49.853-07:00Comments on Haskell for all: The visitor pattern is essentially the same thing as Church encodingGabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comBlogger10125tag:blogger.com,1999:blog-1777990983847811806.post-17899123460283026462021-02-05T01:32:48.595-08:002021-02-05T01:32:48.595-08:00Actually...in the "Course-of-Value Induction ...Actually...in the "Course-of-Value Induction in Cedille" paper they show that you can pattern match on more than one level even with the Böhm-Berarducci encoding by a technique called "tupling".Albert ten Napelhttps://www.blogger.com/profile/15506912779641451902noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-67024751175451625552021-02-04T08:43:58.790-08:002021-02-04T08:43:58.790-08:00My intended audience is just Haskell programmers ,...My intended audience is just Haskell programmers , but all my posts have a Creative Commons so people can freely translate them to use examples in other programming languages.Gabriel Gonzalezhttps://www.blogger.com/profile/01917800488530923694noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-38755935968419138772021-02-04T08:22:39.709-08:002021-02-04T08:22:39.709-08:00Would be helpful to have an example in some more m...Would be helpful to have an example in some more mainstream language for those of us not versed in Haskell.Guyren G Howehttps://www.blogger.com/profile/18004538540256202068noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-53406450867696597492021-02-04T03:34:19.924-08:002021-02-04T03:34:19.924-08:00If I recall correctly, if you want to pattern matc...If I recall correctly, if you want to pattern match on more than one level the Church-encoding (or Böhm-Berarducci) is not enough. You need course-of-value recusion aka histomorphism, see the paper "Course-of-Value Induction in Cedille".Albert ten Napelhttps://www.blogger.com/profile/15506912779641451902noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-69698515005837968032021-02-04T03:28:24.621-08:002021-02-04T03:28:24.621-08:00We can write the pattern functor for Tree:
type T...We can write the pattern functor for Tree:<br /><br />type TreeF t = forall r. (Int -> t -> t -> r) -> r -> r<br /><br />Then we can write the Church-style Fixpoint of functor:<br /><br />type Fix f = forall t. (f t -> t) -> t<br /><br />And (Fix TreeF) should be isomorphic to Tree, but I am unable to prove it.<br />Albert ten Napelhttps://www.blogger.com/profile/15506912779641451902noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-73829687281571492742021-02-04T03:14:52.490-08:002021-02-04T03:14:52.490-08:00I think:
type Tree = forall t . (Int -> Tree -...I think:<br /><br />type Tree = forall t . (Int -> Tree -> Tree -> t) -> t -> t<br /><br />Is actually the Scott encoding (the case match). The Parigot encoding would be:<br /><br />type Tree = forall t . (Int -> Tree -> Tree -> t -> t -> t) -> t -> t<br /><br />So that you have access to both the sub-trees and the results of the recursive calls of the sub-trees.<br /><br />Another interesting encoding is the Mendler-encoding:<br /><br />type Tree = forall t . (forall r. (r -> t) -> Int -> r -> r -> t) -> t -> t<br /><br />Here you get to decide if you want to perform the recursive call or not. This is not very interesting for a lazy language, but for a strict language it will matter.<br /><br />You can also modify the Mendler encoding to allow for unrestricted recursion:<br /><br />type Tree = forall t . ((Tree -> t) -> Int -> Tree -> Tree -> t) -> t -> t<br /><br />Basically the Scott encoding with access to the recursive call.Albert ten Napelhttps://www.blogger.com/profile/15506912779641451902noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-11611833944135420062021-01-08T08:57:28.647-08:002021-01-08T08:57:28.647-08:00I had exactly the same feeling, but I might be bia...I had exactly the same feeling, but I might be biased because I just spent a week studying recursion-schemes and I know see them everywhere.<br /><br />To add to this: Gabriel noted that the preorder function never recursively calls itself. If I understand correctly, that's because the construction of trees actually bakes in that its constituent parts are provided with the same 'handlers' for each constructor, much like an F-algebra would do for the Base functor?<br /><br />I'm wondering what implications this would have when we want to write minmax evaluation over these same trees, so without introducing a tag/constructor in the datatype signaling whether a node is a max or a min node.<br /><br />With a traditional (tagged initial?) datatype encoding, we could write 'minmax' by pattern matching on up to two levels of nesting at once, and then recursively call 'minmax' again.<br />I'm not so sure how this would translate for the Böhm-Berarducci approach, whether it is possible and how.. I'm might need to do some experimenting this evening!mvanderhallenhttps://www.blogger.com/profile/17078182565592575952noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-83822157203387396292021-01-07T08:32:13.054-08:002021-01-07T08:32:13.054-08:00As well as the Church/Böhm-Berarducci encoding, th...As well as the Church/Böhm-Berarducci encoding, there's a Parigot encoding. For the former, binary trees are expressed by<br /><br /> type Tree = forall t . (Int -> t -> t -> t) -> t -> t<br /><br />so the type is not recursive, but the constructors have to be recursive; this corresponds to what GOF call "internal visitors", where it is the visitor that controls the order of traversal. Whereas for the latter the type is<br /><br /> type Tree = forall t . (Int -> Tree -> Tree -> t) -> t -> t<br /><br />which is recursive, but now the constructors need not be; this corresponds to GOF's "external visitors", where it is the client that controls the order of traversal. <br /><br />For more detail, see this paper from OOPSLA 2008, mostly by my former student Bruno Oliveira:<br /><br /> http://www.cs.ox.ac.uk/publications/publication1398-abstract.html<br />Jeremy Gibbonshttps://www.blogger.com/profile/04633943586802588755noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-77532843154203159452021-01-04T16:52:28.949-08:002021-01-04T16:52:28.949-08:00Great post!
Minor typo:
-- Evaluate the anonymous...Great post!<br /><br />Minor typo:<br />-- Evaluate the anonymous function<br />= pi * 4.6 ^ 2<br /><br /><br />-= pi * 4.6 ^ 2<br />Markhttps://www.blogger.com/profile/09877119195514564181noreply@blogger.comtag:blogger.com,1999:blog-1777990983847811806.post-60796570234453879192021-01-04T14:34:59.068-08:002021-01-04T14:34:59.068-08:00Thanks for this insightful write up. I'm sensi...Thanks for this insightful write up. I'm sensing a strong relation of the Böhm-Berarducci encoding of Trees to F-Algebras and catamorphisms: <br /><br />preorder :: Tree -> [Int]<br /><br />pretty much looks like the F-Algebra of the Tree functor to me. I can't pinpoint this more precisely though for now. <br />Unknownhttps://www.blogger.com/profile/13587552231095691885noreply@blogger.com