Logs: liberachat/#haskell
| 2021-07-14 20:14:37 | <dminuoso> | (It wouldn't even know if they are satisfied) |
| 2021-07-14 20:15:11 | <dminuoso> | However, there's tricks to tie GHCs hands and gain this optimization in a guaranteed manner |
| 2021-07-14 20:18:02 | × | norias quits (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) (Ping timeout: 245 seconds) |
| 2021-07-14 20:18:24 | × | Guest9 quits (~Guest9@43.250.157.35) (Quit: Connection closed) |
| 2021-07-14 20:19:03 | <burnsidesLlama> | Making GHC aware of class laws seems like something type-level programming can address. I can't think of how exactly yet. It is like embedding a proof assistant able to work with user-defined axioms into the compiler. |
| 2021-07-14 20:19:25 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Read error: Connection reset by peer) |
| 2021-07-14 20:19:42 | → | Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 2021-07-14 20:19:49 | → | Atum__ joins (IRC@user/atum/x-2392232) |
| 2021-07-14 20:19:50 | <Hecate> | burnsidesLlama: LiquidHaskell |
| 2021-07-14 20:19:56 | <Hecate> | (I think?) |
| 2021-07-14 20:20:09 | <dminuoso> | burnsidesLlama: Well, we can get away with something far more trivial in Haskell |
| 2021-07-14 20:20:17 | <Hecate> | Ryan Scott wrote a paper about it as well |
| 2021-07-14 20:20:50 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Quit: Lost terminal) |
| 2021-07-14 20:21:03 | <dminuoso> | % newtype F f a = F { runF :: forall b. (a -> b) -> f b } |
| 2021-07-14 20:21:04 | <yahb> | dminuoso: |
| 2021-07-14 20:21:05 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-07-14 20:21:50 | <dminuoso> | burnsidesLlama: ^- here. This is just a newtype wrapper where we represent a functor as partially applied to fmap, sort of how the argument to `build` is a foldr partially applied to something list like. |
| 2021-07-14 20:22:11 | × | Atum_ quits (IRC@user/atum/x-2392232) (Ping timeout: 265 seconds) |
| 2021-07-14 20:22:15 | <dminuoso> | % someList = F (`fmap` [1,2,3,4,5]) |
| 2021-07-14 20:22:15 | <yahb> | dminuoso: |
| 2021-07-14 20:22:43 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-14 20:22:44 | <dminuoso> | % instance Functor (F f) where fmap f m = F (\k -> runF m (k . f)) |
| 2021-07-14 20:22:44 | <yahb> | dminuoso: |
| 2021-07-14 20:22:49 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-07-14 20:22:52 | cheater1__ | is now known as cheater |
| 2021-07-14 20:23:43 | <dminuoso> | Here. So we can turn say a list into this `F` representation, then do a bunch of `fmap f . fmap g . fmap h . fmap i . fmap j` on it, and then go back again - and tadaa - its fused. |
| 2021-07-14 20:23:51 | <dminuoso> | It will go over the list only once |
| 2021-07-14 20:24:47 | <tomsmeding> | because the actual 'fmap' on the list is only executed once: when the original function (`fmap` [1,2,3,4,5]) is executed; all the other fmaps translate to function composition, of which ghc does know that it can fuse |
| 2021-07-14 20:24:52 | → | ptrcmd joins (~ptrcmd@user/ptrcmd) |
| 2021-07-14 20:25:45 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) (Remote host closed the connection) |
| 2021-07-14 20:25:58 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) |
| 2021-07-14 20:26:33 | <dminuoso> | % lowerF (F f) = f id |
| 2021-07-14 20:26:33 | <yahb> | dminuoso: |
| 2021-07-14 20:26:40 | <dminuoso> | % lowerF . fmap (+1) . fmap (*20) . fmap (/5) $ someList |
| 2021-07-14 20:26:40 | <yahb> | dminuoso: [5.0,9.0,13.0,17.0,21.0] |
| 2021-07-14 20:28:12 | <dminuoso> | We can then also write ourselves some: |
| 2021-07-14 20:28:36 | <dminuoso> | % liftF a = F (`fmap` a) |
| 2021-07-14 20:28:36 | <yahb> | dminuoso: |
| 2021-07-14 20:28:41 | <burnsidesLlama> | in the definition of F, is runF missing an argument? the call in the instance declaration to runF m (k . f) seems to need two arguments rather than one |
| 2021-07-14 20:28:47 | <dminuoso> | % lowerF . fmap (+1) . fmap (*20) . fmap (/5) .liftF $ [1,2,3,4,5,6] |
| 2021-07-14 20:28:47 | <yahb> | dminuoso: [5.0,9.0,13.0,17.0,21.0,25.0] |
| 2021-07-14 20:29:05 | <dminuoso> | Then all we have to do is wrap this large fmap composition between `lowerF` and `liftF`, and we get fusion for free. |
| 2021-07-14 20:29:23 | <dminuoso> | Nothing else even knows about this F representation! At runtime its even gone because its a newtype |
| 2021-07-14 20:29:51 | × | P1RATEZ quits (piratez@user/p1ratez) (Remote host closed the connection) |
| 2021-07-14 20:29:54 | <dminuoso> | burnsidesLlama: No. This is field-syntax for newtype |
| 2021-07-14 20:29:59 | <dminuoso> | % :t runF |
| 2021-07-14 20:29:59 | <yahb> | dminuoso: forall {f :: * -> *} {a}. F f a -> forall b. (a -> b) -> f b |
| 2021-07-14 20:30:27 | → | beka joins (~beka@104.193.170-244.PUBLIC.monkeybrains.net) |
| 2021-07-14 20:30:52 | <tomsmeding> | 'runF m' is the field, which has type (forall b. (a -> b) -> f b), of the record m |
| 2021-07-14 20:31:00 | <dminuoso> | Correkt |
| 2021-07-14 20:33:12 | <burnsidesLlama> | I'll need time to digest what's been said :), bye for now. |
| 2021-07-14 20:33:12 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-07-14 20:33:12 | × | amirouche quits (~amirouche@user/amirouche) (Read error: Connection reset by peer) |
| 2021-07-14 20:34:29 | × | chexum quits (~chexum@gateway/tor-sasl/chexum) (Quit: -) |
| 2021-07-14 20:34:42 | smichel17 | is now known as smichel |
| 2021-07-14 20:36:18 | → | chexum joins (~chexum@gateway/tor-sasl/chexum) |
| 2021-07-14 20:37:40 | → | analognoise joins (~analognoi@83.136.182.93) |
| 2021-07-14 20:38:02 | × | cheater quits (~Username@user/cheater) (Ping timeout: 245 seconds) |
| 2021-07-14 20:38:25 | → | cheater joins (~Username@user/cheater) |
| 2021-07-14 20:38:33 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 255 seconds) |
| 2021-07-14 20:38:44 | → | Guest239 joins (~Guest23@50.47.115.102) |
| 2021-07-14 20:38:55 | × | finsternis quits (~X@23.226.237.192) (Remote host closed the connection) |
| 2021-07-14 20:38:58 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-14 20:39:21 | → | amirouche joins (~amirouche@user/amirouche) |
| 2021-07-14 20:39:41 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-07-14 20:40:07 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-07-14 20:44:09 | <Guest239> | Does anyone know how to make autocompletion and automatic refactoring to work for Haskell in Spacemacs? |
| 2021-07-14 20:44:55 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Ping timeout: 268 seconds) |
| 2021-07-14 20:45:03 | → | Topsi joins (~Tobias@dyndsl-095-033-020-123.ewe-ip-backbone.de) |
| 2021-07-14 20:46:16 | × | beka quits (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 246 seconds) |
| 2021-07-14 20:47:03 | smichel | is now known as smichel17 |
| 2021-07-14 20:47:28 | × | silverwhitefish quits (~hidden@47.202.102.10) (Quit: One for all, all for One (2 Corinthians 5)) |
| 2021-07-14 20:48:54 | × | MidAutumnMoon9 quits (~MidAutumn@user/midautumnmoon) (Ping timeout: 255 seconds) |
| 2021-07-14 20:49:14 | × | amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 268 seconds) |
| 2021-07-14 20:50:35 | → | jess joins (~jess@libera/staff/jess) |
| 2021-07-14 20:50:54 | → | o1lo01ol1o joins (~o1lo01ol1@bl11-109-140.dsl.telepac.pt) |
| 2021-07-14 20:51:50 | × | jippiedoe quits (~david@77-171-152-62.fixed.kpn.net) (Quit: Leaving) |
| 2021-07-14 20:51:53 | → | jneira_ joins (~jneira_@28.red-80-28-169.staticip.rima-tde.net) |
| 2021-07-14 20:52:09 | <Guest239> | In spacemacs the Haskell layer is able to suggest refactorings but is unable to apply them with SPC m r r. How can I fix this? |
| 2021-07-14 20:56:01 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2021-07-14 20:56:05 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-07-14 20:56:08 | cheater1__ | is now known as cheater |
| 2021-07-14 20:56:20 | → | MidAutumnMoon9 joins (~MidAutumn@user/midautumnmoon) |
| 2021-07-14 20:58:32 | × | ph88^ quits (~ph88@2a02:8109:9e00:2b48:9925:18b1:79f7:f242) (Ping timeout: 255 seconds) |
| 2021-07-14 21:01:10 | → | DNH joins (~DNH@2a02:8108:1100:16d8:4c45:cc63:abad:ed54) |
| 2021-07-14 21:01:12 | × | DNH quits (~DNH@2a02:8108:1100:16d8:4c45:cc63:abad:ed54) (Client Quit) |
| 2021-07-14 21:01:20 | × | ec quits (~ec@gateway/tor-sasl/ec) (Quit: ec) |
| 2021-07-14 21:03:42 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 258 seconds) |
| 2021-07-14 21:04:14 | × | cheater quits (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 2021-07-14 21:04:34 | → | cheater joins (~Username@user/cheater) |
| 2021-07-14 21:05:15 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-07-14 21:05:51 | → | spruit11_ joins (~quassel@2a02:a467:ccd6:1:4852:6669:da0c:37fe) |
| 2021-07-14 21:06:42 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-14 21:09:20 | × | spruit11 quits (~quassel@2a02:a467:ccd6:1:f403:cf1e:97b5:1c9b) (Ping timeout: 255 seconds) |
| 2021-07-14 21:10:32 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-07-14 21:11:03 | → | zebrag joins (~chris@user/zebrag) |
| 2021-07-14 21:11:34 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-14 21:11:58 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 2021-07-14 21:13:12 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 2021-07-14 21:13:37 | → | Atum_ joins (IRC@user/atum/x-2392232) |
All times are in UTC.