Logs: liberachat/#haskell
| 2021-07-14 19:48:15 | <dminuoso> | let x = \f z -> foldr f z t in ... |
| 2021-07-14 19:48:26 | <dminuoso> | burnsidesLlama: So this is just a foldr partially applied to some structure already |
| 2021-07-14 19:48:47 | × | qbt quits (~edun@user/edun) (Read error: Connection reset by peer) |
| 2021-07-14 19:48:56 | <dminuoso> | And `build` just finalizes such a partially applied foldr by providing (:) and [] to the remaining arguments. |
| 2021-07-14 19:49:10 | → | qbt joins (~edun@user/edun) |
| 2021-07-14 19:50:07 | <burnsidesLlama> | in the 'let x = ...' line, do you mean foldr for lists? Or a fold for possibly another kind of ADT |
| 2021-07-14 19:50:25 | × | qbt quits (~edun@user/edun) (Read error: Connection reset by peer) |
| 2021-07-14 19:50:25 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Read error: Connection reset by peer) |
| 2021-07-14 19:50:41 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-07-14 19:50:48 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Read error: Connection reset by peer) |
| 2021-07-14 19:51:04 | <dminuoso> | Maybe this is a red herring, mmm. |
| 2021-07-14 19:51:06 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-07-14 19:51:41 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 2021-07-14 19:51:49 | <dminuoso> | burnsidesLlama: Could be anything. |
| 2021-07-14 19:52:39 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-07-14 19:52:47 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-14 19:52:51 | → | qbt joins (~edun@user/edun) |
| 2021-07-14 19:52:52 | cheater1__ | is now known as cheater |
| 2021-07-14 19:53:22 | <burnsidesLlama> | are you saying we can make lists out of anything using build? this doesn't seem right |
| 2021-07-14 19:54:05 | × | qbt quits (~edun@user/edun) (Client Quit) |
| 2021-07-14 19:54:22 | → | qbt joins (~edun@user/edun) |
| 2021-07-14 19:54:23 | tomsmeding | . o O ( https://hackage.haskell.org/package/base-4.14.0.0/docs/src/Data.Foldable.html#toList ) |
| 2021-07-14 19:54:50 | <dminuoso> | burnsidesLlama: Let's for the sake of simplicity say it has to be a foldable at least. |
| 2021-07-14 19:55:16 | <dminuoso> | Or.. no. This really is a red herring |
| 2021-07-14 19:55:25 | <burnsidesLlama> | I'm not familiar with foldable, could we be even more concrete? E.g. by taking a binary tree type |
| 2021-07-14 19:56:36 | <dminuoso> | burnsidesLlama: The idea is roughly the same as church encoding a list. A list can be fully characterized by its fold. |
| 2021-07-14 19:56:42 | <dminuoso> | (its right fold) |
| 2021-07-14 19:57:03 | <dminuoso> | % :t foldr |
| 2021-07-14 19:57:03 | <yahb> | dminuoso: forall {t :: * -> *} {a} {b}. Foldable t => (a -> b -> b) -> b -> t a -> b |
| 2021-07-14 19:57:38 | <dminuoso> | burnsidesLlama: One way to understand Foldable, is that Foldable is anything that you can turn into a list. |
| 2021-07-14 19:57:51 | → | dunj3 joins (~dunj3@2001:16b8:30fc:7f00:fd96:42cd:9d60:7ae7) |
| 2021-07-14 19:58:20 | <dminuoso> | So if we partially apply foldr in its 3rd argument already to some foldable thing, then the remaining thing fully characterizes the list |
| 2021-07-14 19:58:21 | <burnsidesLlama> | And I imagine a Foldable instance must supply a canonical translation (which is injective?) into a list |
| 2021-07-14 19:58:24 | <dminuoso> | Consider: |
| 2021-07-14 19:58:32 | → | o1lo01ol1o joins (~o1lo01ol1@bl11-109-140.dsl.telepac.pt) |
| 2021-07-14 19:58:37 | <dminuoso> | % x = \f z -> foldr f z [1,2,3,4,5,6] |
| 2021-07-14 19:58:37 | <yahb> | dminuoso: |
| 2021-07-14 19:58:45 | <dminuoso> | % :t x |
| 2021-07-14 19:58:45 | <yahb> | dminuoso: forall {a} {b}. Num a => (a -> b -> b) -> b -> b |
| 2021-07-14 19:58:46 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-14 19:58:51 | <dminuoso> | Im going to claim that `x` is fully equivalent to [1,2,3,4,5,6] |
| 2021-07-14 19:59:11 | <dminuoso> | burnsidesLlama: Remember that question, we will get to it shortly |
| 2021-07-14 19:59:34 | <dminuoso> | burnsidesLlama: Let's test my claim these things are even isomorphic. |
| 2021-07-14 19:59:53 | × | qbt quits (~edun@user/edun) (Quit: WeeChat 3.2) |
| 2021-07-14 20:00:04 | <dminuoso> | Can we turn `x` back into a proper Haskell list? |
| 2021-07-14 20:00:06 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-14 20:00:12 | → | qbt joins (~edun@user/edun) |
| 2021-07-14 20:00:44 | <burnsidesLlama> | by doing build x |
| 2021-07-14 20:00:47 | <dminuoso> | heh |
| 2021-07-14 20:00:50 | <dminuoso> | Right. |
| 2021-07-14 20:00:56 | <dminuoso> | Or just manually doing `x (:) []` |
| 2021-07-14 20:00:58 | <dminuoso> | % x (:) [] |
| 2021-07-14 20:00:59 | <yahb> | dminuoso: [1,2,3,4,5,6] |
| 2021-07-14 20:01:41 | <dminuoso> | 21:58:21 burnsidesLlama | And I imagine a Foldable instance must supply a canonical translation (which is injective?) into a list |
| 2021-07-14 20:01:49 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 246 seconds) |
| 2021-07-14 20:02:06 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-07-14 20:02:10 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-07-14 20:02:19 | <dminuoso> | Yes and no. While strictly speaking we could allow for an instance author to write `toList` (and it would semantically be legit), instead we demand you supply an (equivalent) foldr or foldMap instead. |
| 2021-07-14 20:02:22 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-14 20:02:29 | cheater1__ | is now known as cheater |
| 2021-07-14 20:02:42 | <dminuoso> | foldr has the same power as toList, but its more flexible |
| 2021-07-14 20:03:03 | <dminuoso> | It's more flexible because you can - should you want - avoid the actual intermediate cons cells in the list |
| 2021-07-14 20:03:20 | <dminuoso> | So here comes the clue: |
| 2021-07-14 20:03:32 | <dminuoso> | `build` turns a foldr-encoded list into a proper list |
| 2021-07-14 20:03:36 | × | o1lo01ol1o quits (~o1lo01ol1@bl11-109-140.dsl.telepac.pt) (Ping timeout: 268 seconds) |
| 2021-07-14 20:03:54 | <dminuoso> | and foldr goes from a proper list to something else again |
| 2021-07-14 20:04:14 | <dminuoso> | build is equipped with special fusion rules that essentially say: |
| 2021-07-14 20:04:34 | <dminuoso> | With some luck: foldr k z (build g) = g k z |
| 2021-07-14 20:05:14 | → | jumper149 joins (~jumper149@80.240.31.34) |
| 2021-07-14 20:05:15 | × | juhp quits (~juhp@128.106.188.66) (Ping timeout: 255 seconds) |
| 2021-07-14 20:05:44 | <burnsidesLlama> | is it saying: "if we are building a list out of g, only to destroy it, then we can directly compute the result"? |
| 2021-07-14 20:05:50 | <dminuoso> | Yes. |
| 2021-07-14 20:05:52 | <dminuoso> | With some luck. |
| 2021-07-14 20:06:17 | <dminuoso> | You're still at the merci of the inliner and the magic whistles of the GHC simplifier - so there's no actual guarantee. |
| 2021-07-14 20:06:32 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-07-14 20:06:32 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-07-14 20:06:36 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 255 seconds) |
| 2021-07-14 20:07:05 | <burnsidesLlama> | that sounds mysterious and/or ominous |
| 2021-07-14 20:07:10 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 2021-07-14 20:07:13 | <burnsidesLlama> | one last question, then i need to go to sleep |
| 2021-07-14 20:07:42 | <burnsidesLlama> | how is this kind of 'deforestation' related to deforesting a function of the form 'fold . unfold'? |
| 2021-07-14 20:08:08 | → | juhp joins (~juhp@128.106.188.66) |
| 2021-07-14 20:09:25 | <dminuoso> | burnsidesLlama: https://www.cs.ox.ac.uk/ralf.hinze/publications/IFL10.pdf |
| 2021-07-14 20:09:50 | → | ph88^ joins (~ph88@2a02:8109:9e00:2b48:9925:18b1:79f7:f242) |
| 2021-07-14 20:10:07 | <dminuoso> | This optimization I described above is called foldr/build fusion in GHC slang. |
| 2021-07-14 20:10:14 | <dminuoso> | There's an equivalent dual optimizatoin called unfold/destroy |
| 2021-07-14 20:11:43 | <burnsidesLlama> | thank you! :) |
| 2021-07-14 20:12:12 | × | ph88 quits (~ph88@2a02:8109:9e00:7e5c:9925:18b1:79f7:f242) (Ping timeout: 245 seconds) |
| 2021-07-14 20:12:23 | <dminuoso> | % :t unfoldr |
| 2021-07-14 20:12:24 | <yahb> | dminuoso: forall {t} {a}. (t -> Maybe (a, t)) -> t -> [a] |
| 2021-07-14 20:12:25 | <dminuoso> | % :t destroy |
| 2021-07-14 20:12:25 | <yahb> | dminuoso: forall {a} {t1} {t2}. (([a] -> Maybe (a, [a])) -> t1 -> t2) -> t1 -> t2 |
| 2021-07-14 20:12:48 | <dminuoso> | % destroy unfoldr [1..5] |
| 2021-07-14 20:12:48 | <yahb> | dminuoso: [1,2,3,4,5] |
| 2021-07-14 20:13:14 | × | juhp quits (~juhp@128.106.188.66) (Quit: juhp) |
| 2021-07-14 20:13:23 | <dminuoso> | Please dont ask me why we have foldr/build fusion. I expect other folks to be more knowledgable here. |
| 2021-07-14 20:13:28 | → | juhp joins (~juhp@128.106.188.66) |
| 2021-07-14 20:13:50 | <dminuoso> | burnsidesLlama: By the way, as an interesting side note: |
| 2021-07-14 20:14:00 | <dminuoso> | Recall my example of: fmap f . fmap g = fmap (f . g) ? |
| 2021-07-14 20:14:29 | <dminuoso> | It would be nice if GHC could observe this law, and always transform the former into the latter. But it cant, GHC is not even aware of any class laws. |
All times are in UTC.