tag:blogger.com,1999:blog-1777990983847811806.post8137932186432001110..comments2021-07-31T08:38:15.743-07:00Comments on Haskell for all: The visitor pattern is essentially the same thing as Church encodingGabriel Gonzalezhttp://www.blogger.com/profile/01917800488530923694noreply@blogger.comBlogger11125tag:blogger.com,1999:blog-1777990983847811806.post-53478985503055460732021-07-30T10:37:49.933-07:002021-07-30T10:37:49.933-07:00Actually, you don't need parametric polymorphi...Actually, you don't need parametric polymorphism to encode a type-safe algebraic type. ADTs are existential types, and all you need are existential types. You have chosen to encode existentials using universals (presumably because universals are far more fundamental in ML-like languages), but you could have just as well used a Haskell type class or a ML module, which are existential (and then you'd get the so-called tagless final style encoding).<br /><br />In Go, however, existentials are fundamental and very much "in your face". They are called interfaces. Here is an encoding of an ADT in Go, using only interfaces and no generics: https://play.golang.org/p/IbwK3pKfpCS.<br /><br />Just like traditional ADTs, this is closed, type-safe, and the pattern matching is exhaustive.<br /><br />Now that we get generics in Go, we will be able to encode more than ADTs, we will be able to encode a lot of what GADTs can encode.Aram Hăvărneanuhttps://www.blogger.com/profile/00315944519075223213noreply@blogger.comtag: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