2023-02-12 00:02:57 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2023-02-12 00:06:11 +0100 | oldfashionedcow | (~Rahul_San@user/oldfashionedcow) |
2023-02-12 00:10:05 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d14c:efc7:12bb:4678) (Remote host closed the connection) |
2023-02-12 00:14:50 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2023-02-12 00:17:25 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 260 seconds) |
2023-02-12 00:18:40 +0100 | accord | (uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2023-02-12 00:21:01 +0100 | patrl | (~patrl@user/patrl) (Ping timeout: 252 seconds) |
2023-02-12 00:36:13 +0100 | Midjak | (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
2023-02-12 00:39:21 +0100 | shriekingnoise | (~shrieking@186.137.175.87) |
2023-02-12 00:39:59 +0100 | <geekosaur> | hm, found one trouble spot with hie files which would need to check if the module is Prelude, not just ideclImplicit. other possible trouble spots already do that check |
2023-02-12 00:40:08 +0100 | elevenkb | (~elevenkb@105.225.107.107) |
2023-02-12 00:42:22 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d14c:efc7:12bb:4678) |
2023-02-12 00:42:34 +0100 | aljer | (~j@user/aljer) |
2023-02-12 00:48:53 +0100 | aljer | (~j@user/aljer) (Quit: WeeChat 3.8) |
2023-02-12 00:49:12 +0100 | aljer | (~j@user/aljer) |
2023-02-12 00:57:39 +0100 | lackita | (~lackita@73.114.250.252) (Read error: Connection reset by peer) |
2023-02-12 00:58:08 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 01:08:52 +0100 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
2023-02-12 01:08:52 +0100 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
2023-02-12 01:08:52 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-02-12 01:09:25 +0100 | [Leary] | (~Leary]@user/Leary/x-0910699) (Remote host closed the connection) |
2023-02-12 01:09:52 +0100 | [Leary] | (~Leary]@user/Leary/x-0910699) |
2023-02-12 01:12:11 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 268 seconds) |
2023-02-12 01:12:21 +0100 | aljer | (~j@user/aljer) (Ping timeout: 252 seconds) |
2023-02-12 01:13:01 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 01:20:10 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) (Quit: Leaving.) |
2023-02-12 01:22:28 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Remote host closed the connection) |
2023-02-12 01:23:46 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2023-02-12 01:24:58 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-02-12 01:25:04 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Client Quit) |
2023-02-12 01:25:33 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-02-12 01:26:58 +0100 | notzmv | (~zmv@user/notzmv) |
2023-02-12 01:29:03 +0100 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
2023-02-12 01:37:08 +0100 | harveypwca | (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
2023-02-12 01:37:32 +0100 | aljer | (~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) |
2023-02-12 01:37:32 +0100 | aljer | (~j@2601:5c3:380:4e20:a1c6:2f5b:51eb:1666) (Changing host) |
2023-02-12 01:37:32 +0100 | aljer | (~j@user/aljer) |
2023-02-12 01:37:38 +0100 | aljer | (~j@user/aljer) (Client Quit) |
2023-02-12 01:37:56 +0100 | elevenkb | (~elevenkb@105.225.107.107) (Quit: Client closed) |
2023-02-12 01:38:40 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) |
2023-02-12 01:45:09 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
2023-02-12 01:45:11 +0100 | lackita | (~lackita@73.114.250.252) (Read error: Connection reset by peer) |
2023-02-12 01:45:23 +0100 | lackita | (~lackita@2600:1000:b055:1a62:482c:d8b4:d1a3:76c8) |
2023-02-12 01:45:42 +0100 | lackita | (~lackita@2600:1000:b055:1a62:482c:d8b4:d1a3:76c8) (Read error: Connection reset by peer) |
2023-02-12 01:45:53 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 01:47:06 +0100 | thongpv87 | (~thongpv87@123.31.75.7) |
2023-02-12 01:48:11 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) (Ping timeout: 248 seconds) |
2023-02-12 02:01:58 +0100 | oldfashionedcow | (~Rahul_San@user/oldfashionedcow) (Quit: WeeChat 3.8) |
2023-02-12 02:06:05 +0100 | Natch | (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Ping timeout: 252 seconds) |
2023-02-12 02:06:05 +0100 | yin | (~z@user/zero) (Quit: quit) |
2023-02-12 02:06:05 +0100 | tabemann | (~tabemann@2600:1700:7990:24e0:ef07:7078:7b84:e5fd) (Read error: Connection reset by peer) |
2023-02-12 02:06:05 +0100 | foghorn | (~foghorn@user/foghorn) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | gqplox[m] | (~gqploxmat@2001:470:69fc:105::2:d10d) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | kosmikus[m] | (~andresloe@2001:470:69fc:105::95d) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | Deide | (~deide@user/deide) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | jneira[m] | (~jneiramat@2001:470:69fc:105::d729) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | famubu[m] | (~famubumat@2001:470:69fc:105::1081) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | mira | (~aranea@wireguard/contributorcat/mira) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | kronicma1 | (user63668@neotame.csclub.uwaterloo.ca) (Ping timeout: 252 seconds) |
2023-02-12 02:06:06 +0100 | teddyc | (theodorc@cassarossa.samfundet.no) (Ping timeout: 252 seconds) |
2023-02-12 02:06:07 +0100 | gqplox[m] | (~gqploxmat@2001:470:69fc:105::2:d10d) |
2023-02-12 02:06:11 +0100 | travisb_ | (~travisb@2600:1700:7990:24e0:abed:c122:a91f:97ed) |
2023-02-12 02:06:11 +0100 | eldritchcookie[m | (~eldritchc@2001:470:69fc:105::2:d53c) (Ping timeout: 252 seconds) |
2023-02-12 02:06:11 +0100 | tjnhxmzhmqgytuwt | (~tjnhxmzhm@2001:470:69fc:105::3:70e) (Ping timeout: 252 seconds) |
2023-02-12 02:06:11 +0100 | fendor[m] | (~fendormat@2001:470:69fc:105::fcbd) (Ping timeout: 252 seconds) |
2023-02-12 02:06:11 +0100 | Me-me | (~me-me@user/me-me) (Ping timeout: 252 seconds) |
2023-02-12 02:06:14 +0100 | litharge | (litharge@libera/bot/litharge) (Remote host closed the connection) |
2023-02-12 02:06:16 +0100 | jeetelongname | (~jeet@217.79.169.181) (Remote host closed the connection) |
2023-02-12 02:06:16 +0100 | kosmikus[m]1 | (~andresloe@2001:470:69fc:105::95d) |
2023-02-12 02:06:21 +0100 | johnjaye | (~pi@173.209.64.74) (Ping timeout: 248 seconds) |
2023-02-12 02:06:32 +0100 | oldfashionedcow | (~Rahul_San@user/oldfashionedcow) |
2023-02-12 02:06:32 +0100 | pi1 | (~pi@173.209.64.74) |
2023-02-12 02:06:34 +0100 | litharge | (litharge@libera/bot/litharge) |
2023-02-12 02:06:51 +0100 | Wstfgl0 | (~me-me@2602:ff16:3:0:1:dc:beef:d00d) |
2023-02-12 02:06:51 +0100 | theodorc | (theodorc@cassarossa.samfundet.no) |
2023-02-12 02:07:18 +0100 | kronicma1 | (user13639@neotame.csclub.uwaterloo.ca) |
2023-02-12 02:08:01 +0100 | mewra | (~aranea@wireguard/contributorcat/mira) |
2023-02-12 02:08:05 +0100 | zero | (~z@user/zero) |
2023-02-12 02:08:17 +0100 | Natch | (~natch@92.34.7.158) |
2023-02-12 02:09:01 +0100 | Wstfgl0 | Me-me |
2023-02-12 02:09:33 +0100 | jneira[m] | (~jneiramat@2001:470:69fc:105::d729) |
2023-02-12 02:09:42 +0100 | Deide | (~deide@user/deide) |
2023-02-12 02:09:49 +0100 | famubu[m] | (~famubumat@2001:470:69fc:105::1081) |
2023-02-12 02:10:44 +0100 | foghorn | (~foghorn@user/foghorn) |
2023-02-12 02:10:46 +0100 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
2023-02-12 02:10:50 +0100 | Me-me | (~me-me@2602:ff16:3:0:1:dc:beef:d00d) (Changing host) |
2023-02-12 02:10:50 +0100 | Me-me | (~me-me@user/me-me) |
2023-02-12 02:11:10 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
2023-02-12 02:13:40 +0100 | fendor[m] | (~fendormat@2001:470:69fc:105::fcbd) |
2023-02-12 02:13:42 +0100 | eldritchcookie[m | (~eldritchc@2001:470:69fc:105::2:d53c) |
2023-02-12 02:14:25 +0100 | falafel | (~falafel@2607:fb91:143f:e47f:6cfc:4f5:5346:997f) |
2023-02-12 02:15:18 +0100 | tjnhxmzhmqgytuwt | (~tjnhxmzhm@2001:470:69fc:105::3:70e) |
2023-02-12 02:16:53 +0100 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
2023-02-12 02:16:59 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 248 seconds) |
2023-02-12 02:17:01 +0100 | zmt01 | (~zmt00@user/zmt00) |
2023-02-12 02:17:21 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 02:20:32 +0100 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 248 seconds) |
2023-02-12 02:21:35 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 02:22:15 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 02:25:11 +0100 | <Inst> | hmmm, this is interesting |
2023-02-12 02:25:25 +0100 | waleee | (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 265 seconds) |
2023-02-12 02:25:41 +0100 | <Inst> | a map over a recursive data structure is an example of a metamorphism, no? |
2023-02-12 02:28:52 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2023-02-12 02:29:49 +0100 | gmg | (~user@user/gehmehgeh) |
2023-02-12 02:32:44 +0100 | <cheater> | i have an ADT and i want to make sure that transitions only happen from specific constructors to specific other constructors. how do i do that? |
2023-02-12 02:35:51 +0100 | enoq | (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) (Quit: enoq) |
2023-02-12 02:39:28 +0100 | larrythecow | (~Rahul_San@user/oldfashionedcow) |
2023-02-12 02:39:42 +0100 | oldfashionedcow | (~Rahul_San@user/oldfashionedcow) (Killed (silver.libera.chat (Nickname regained by services))) |
2023-02-12 02:39:42 +0100 | larrythecow | oldfashionedcow |
2023-02-12 02:40:34 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 260 seconds) |
2023-02-12 02:41:14 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 02:42:27 +0100 | retrosenator | (~retrosena@134.sub-174-211-114.myvzw.com) |
2023-02-12 02:46:25 +0100 | acidjnk | (~acidjnk@p200300d6e715c445a05d634093e239a0.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
2023-02-12 02:50:13 +0100 | <wroathe> | Hey it's been a while since I wrote any haskell. I used to know what to do about this, but with vscode I've got a basic cabal package that has an executable and test-suite specified inside of it. The vscode extension locates imports just fine for haskell files that are part of the main executable, but when I'm editing my test source files it gives me "Could not load module ‘Test.Hspec’ It is a member |
2023-02-12 02:50:18 +0100 | <wroathe> | of the hidden package ‘hspec-2.10.9’." for the imports |
2023-02-12 02:50:30 +0100 | <wroathe> | I suspect this has something to do with cabal configuration or something like that. Anyone else run into this? |
2023-02-12 02:52:59 +0100 | <wroathe> | It's as if vscode can only locate dependencies for one target at a time within the cabal package |
2023-02-12 02:55:40 +0100 | <wroathe> | Oh, weird. If I force the extension to reload haskell language server it picks the configuration for the package related to whatever the current file I'm on is |
2023-02-12 02:55:47 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 268 seconds) |
2023-02-12 02:55:58 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 02:56:10 +0100 | <wroathe> | I think that's enough to go on. Ignore me. |
2023-02-12 02:57:01 +0100 | beteigeuze | (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Ping timeout: 268 seconds) |
2023-02-12 02:57:31 +0100 | <geekosaur> | you still sometimes have to provide an HIE cradle for HLS to do the right thing |
2023-02-12 02:57:32 +0100 | <EvanR> | cheater, you could use GADTs with phantom types |
2023-02-12 02:57:52 +0100 | <cheater> | EvanR: how? could you show me a simple functional example? |
2023-02-12 02:58:26 +0100 | <EvanR> | data Tag = RedTag | BlueTag | GreenTag |
2023-02-12 02:59:47 +0100 | <EvanR> | data CheatersType tag where R :: CheatersType RedTag; G :: CheatersType GreenTag |
2023-02-12 03:00:08 +0100 | <EvanR> | rgTransition :: CheatersType RedTag -> CheatersType GreenTag |
2023-02-12 03:00:23 +0100 | <EvanR> | rgTransition R = G |
2023-02-12 03:01:10 +0100 | <EvanR> | here, RedTag is used as a type. By enabling DataKinds |
2023-02-12 03:01:56 +0100 | <EvanR> | or you could just define data RedTag, data GreenTag |
2023-02-12 03:02:30 +0100 | <EvanR> | it's involved enough that you will need a good reason to go this route xD |
2023-02-12 03:03:10 +0100 | oldfashionedcow | (~Rahul_San@user/oldfashionedcow) (Quit: WeeChat 3.8) |
2023-02-12 03:03:53 +0100 | <cheater> | EvanR: a protocol |
2023-02-12 03:03:57 +0100 | Angelz | (Angelz@2605:6400:30:fc15:d55b:fa6c:bd14:9973) (Quit: IRCNow and Forever!) |
2023-02-12 03:04:38 +0100 | <cheater> | EvanR: why wouldn't i instead do rgTransitionEasy RedTag = GreenTag? why is your construction better? |
2023-02-12 03:06:02 +0100 | <cheater> | how does your construction propagate around the types of my values? |
2023-02-12 03:07:33 +0100 | <EvanR> | you said you wanted to allow only certain transitions |
2023-02-12 03:07:56 +0100 | <EvanR> | so rgTransition R = G is incomplete if you didn't use the phantom types |
2023-02-12 03:08:10 +0100 | <EvanR> | you'd also have to say rgTransition G = something, which you didn't want to allow |
2023-02-12 03:08:50 +0100 | <EvanR> | my examples don't have much interesting going on, but IRL you'd attach some relevant info to each constructor |
2023-02-12 03:11:40 +0100 | Guest7191 | (~Guest71@90-226-60-189-no2000.tbcn.telia.com) |
2023-02-12 03:12:29 +0100 | unit73e | (~emanuel@2001:818:e8dd:7c00:656:e5ff:fe72:9d36) |
2023-02-12 03:12:35 +0100 | <Guest7191> | If a package on hackage has been dormant for some time and there has been no communication possible with the maintainer, is it possible to transfer the ownership of that package? |
2023-02-12 03:13:25 +0100 | <geekosaur> | post a maintainer takeover request to haskell-cafe |
2023-02-12 03:13:43 +0100 | <unit73e> | so it works like aur |
2023-02-12 03:13:49 +0100 | <unit73e> | good to know |
2023-02-12 03:14:05 +0100 | <unit73e> | also hello |
2023-02-12 03:15:10 +0100 | <cheater> | <EvanR> you said you wanted to allow only certain transitions < yes, that's why I only provided rgTransitionEasy and not gbTransitionEasy or rbTransitionEasy |
2023-02-12 03:15:35 +0100 | <cheater> | <EvanR> so rgTransition R = G is incomplete if you didn't use the phantom types < i don't understand what you mean by "incomplete"? |
2023-02-12 03:15:45 +0100 | <EvanR> | what's the type of your rgTransition |
2023-02-12 03:15:46 +0100 | <cheater> | EvanR> you'd also have to say rgTransition G = something, which you didn't want to allow < idk what that means |
2023-02-12 03:16:05 +0100 | <EvanR> | always keep in mind the types |
2023-02-12 03:16:12 +0100 | <cheater> | oh, i have a simple protocol that has the following states: Hello, SendStuff, Ended |
2023-02-12 03:16:30 +0100 | <cheater> | you can legally go Hello -> SendStuff and SendStuff -> Ended. and no other transitions. |
2023-02-12 03:17:06 +0100 | <cheater> | EvanR> what's the type of your rgTransition < hmm i don't know what you mean :S |
2023-02-12 03:17:22 +0100 | <EvanR> | e.g. the type of chr is Int -> Char |
2023-02-12 03:17:45 +0100 | <EvanR> | rgTransition is a function taking what type to what type |
2023-02-12 03:18:15 +0100 | <EvanR> | ProtocolState -> ProtocolState? |
2023-02-12 03:18:56 +0100 | <cheater> | are you using the name rgTransition for something different than what you defined previously? |
2023-02-12 03:19:26 +0100 | <cheater> | you said rgTransition :: CheatersType RedTag -> CheatersType GreenTag |
2023-02-12 03:19:28 +0100 | <EvanR> | I'm talking about your version not mine |
2023-02-12 03:19:36 +0100 | <EvanR> | you went another way but didn't specify the type signature |
2023-02-12 03:19:39 +0100 | <cheater> | ok, to avoid confusion call it something else |
2023-02-12 03:19:47 +0100 | <cheater> | i called mine rgTransitionEasy, remember? |
2023-02-12 03:19:51 +0100 | <cheater> | to avoid confusing the two |
2023-02-12 03:19:57 +0100 | <EvanR> | so what's the type |
2023-02-12 03:20:33 +0100 | <cheater> | well it's rgTransitionEasy Tag -> Tag |
2023-02-12 03:20:37 +0100 | <cheater> | rgTransitionEasy :: Tag -> Tag |
2023-02-12 03:21:10 +0100 | <EvanR> | then to write a function taking Tag to Tag you have to define what happens for all 3 Tags |
2023-02-12 03:21:22 +0100 | Guest7191 | (~Guest71@90-226-60-189-no2000.tbcn.telia.com) (Quit: Client closed) |
2023-02-12 03:21:25 +0100 | <cheater> | right |
2023-02-12 03:21:27 +0100 | <EvanR> | otherwise it's incomplete |
2023-02-12 03:21:38 +0100 | Midjak | (~Midjak@82.66.147.146) |
2023-02-12 03:21:55 +0100 | <cheater> | in your version, which we call rgTransition, how do I create a value of type CheatersType RedTag? |
2023-02-12 03:22:01 +0100 | <EvanR> | it's possible to write a mistake into the code which crashes at runtime |
2023-02-12 03:22:27 +0100 | <EvanR> | R :: CheatersType RedTag |
2023-02-12 03:22:48 +0100 | <EvanR> | R is the only way, in this case |
2023-02-12 03:23:01 +0100 | <cheater> | ohh right |
2023-02-12 03:23:09 +0100 | <EvanR> | rgTransition G would not compile, wrong types |
2023-02-12 03:23:16 +0100 | <cheater> | but then I can also create G and skip the whole rgTransition thing, right? |
2023-02-12 03:23:36 +0100 | <EvanR> | you could hide R and G using the module system |
2023-02-12 03:23:49 +0100 | <EvanR> | exposing only R and the transition |
2023-02-12 03:23:54 +0100 | <cheater> | ok. so i could hide G but not R |
2023-02-12 03:23:56 +0100 | <cheater> | gotcha |
2023-02-12 03:24:04 +0100 | <cheater> | ty |
2023-02-12 03:24:19 +0100 | <EvanR> | or exposing something that amounts to providing R if some other thing is satsified |
2023-02-12 03:24:46 +0100 | <EvanR> | expose only the rules of the game you want the client code to play |
2023-02-12 03:24:47 +0100 | scrungus | (~scrungus@70.24.71.72) |
2023-02-12 03:24:59 +0100 | <cheater> | if i want to make a function that can only run on the G stage of my protocol, i write doWhenG :: CheatersType GreenTag -> SomeType -> SomeOtherType, right? |
2023-02-12 03:25:23 +0100 | gmg | (~user@user/gehmehgeh) (Ping timeout: 255 seconds) |
2023-02-12 03:25:44 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2023-02-12 03:25:50 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 265 seconds) |
2023-02-12 03:25:58 +0100 | <EvanR> | yeah you wouldn't be able to use doWhenG until the user did whatever to get a G |
2023-02-12 03:27:01 +0100 | Lord_of_Life_ | Lord_of_Life |
2023-02-12 03:27:12 +0100 | <cheater> | so i have to do something like let state = rgTransition R; doWhenG state icecream; right? |
2023-02-12 03:27:22 +0100 | gehmehgeh | (~user@user/gehmehgeh) |
2023-02-12 03:27:42 +0100 | <EvanR> | it sounds like you want to use do notation and access the network during all this |
2023-02-12 03:28:06 +0100 | <EvanR> | what you just wrote isn't valid haskell by itself |
2023-02-12 03:28:06 +0100 | <cheater> | that can come later, i'm trying to understand doWhenG right now |
2023-02-12 03:28:26 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 255 seconds) |
2023-02-12 03:28:43 +0100 | <EvanR> | let state = rgTransition R in doWhenG state icecream -- ok this |
2023-02-12 03:28:59 +0100 | <cheater> | yeah |
2023-02-12 03:29:17 +0100 | <EvanR> | we haven't really accomplished anything with this GADT so far. You could have just used two different types |
2023-02-12 03:29:32 +0100 | <cheater> | i mean yeah i was mentally putting the let in a do block :) |
2023-02-12 03:29:38 +0100 | <cheater> | ok :) thanks |
2023-02-12 03:29:50 +0100 | <EvanR> | e.g. doWhenG requires TypeG. rgTransition :: TypeR -> TypeG |
2023-02-12 03:29:56 +0100 | scrungus | (~scrungus@70.24.71.72) (Quit: Leaving) |
2023-02-12 03:29:57 +0100 | <EvanR> | (no GADTs) |
2023-02-12 03:30:42 +0100 | <cheater> | right, i can use separate types like that as well, no GADTs, right? |
2023-02-12 03:30:46 +0100 | <cheater> | so why use GADTs and not this? |
2023-02-12 03:31:48 +0100 | <EvanR> | note none of this code can access the network, they are just functions |
2023-02-12 03:32:24 +0100 | <cheater> | sure, but you can put them in IO, so that's not worth being worried about, right? |
2023-02-12 03:33:58 +0100 | <EvanR> | yeah you could use IO, and "you" the implemetor of the network protocol can write whatever you want to the socket at any time |
2023-02-12 03:34:22 +0100 | <EvanR> | if you have access to the socket |
2023-02-12 03:34:37 +0100 | <cheater> | so back to my previous question... why use GADTs and not separate types like TypeR and TypeG? |
2023-02-12 03:35:17 +0100 | scrungus_ | (~scrungus@70.24.71.72) |
2023-02-12 03:35:30 +0100 | <scrungus_> | I'm pretty new so sorry if I'm forming this question wrong, but what would I want to do if I had a list of indeterminate length (because it's from user input) and I wanted to use each value in that list as a parameter on a function that takes one parameter? (Basically applying the function multiple times on a value using each value in the list separately). |
2023-02-12 03:36:56 +0100 | <cheater> | fold or map or traverse |
2023-02-12 03:37:23 +0100 | <cheater> | also learn to use hoogle, it can find such functions |
2023-02-12 03:38:26 +0100 | <EvanR> | scrungus_, are you thinking your function should accept a list instead |
2023-02-12 03:38:36 +0100 | <EvanR> | f :: [Item] -> Answer |
2023-02-12 03:39:19 +0100 | <EvanR> | cheater, to answer this we'd have to go into weeds of how the whole thing is set up and what you're actually trying to stop from compiling |
2023-02-12 03:40:14 +0100 | <scrungus_> | fold or map isn't what I'm looking for but traverse might work. I can look into rewriting the function, I think I just got stuck thinking about it in a particular way. |
2023-02-12 03:40:30 +0100 | <cheater> | EvanR: can you give me some examples? |
2023-02-12 03:41:22 +0100 | <EvanR> | of what |
2023-02-12 03:41:40 +0100 | <cheater> | where this makes a difference (GADT vs separate types) |
2023-02-12 03:42:31 +0100 | <EvanR> | it comes down to your transition types. You give me examples of your rules |
2023-02-12 03:42:45 +0100 | <EvanR> | we'll see if you can or can't do it with the basic type system |
2023-02-12 03:43:04 +0100 | <cheater> | i don't really have any. right now i'm just curious what sets these two apart, so that's why i asked you for an example of your own |
2023-02-12 03:43:18 +0100 | Angelz | (Angelz@angelz.oddprotocol.org) |
2023-02-12 03:43:29 +0100 | <EvanR> | I can't give you any examples of your network protocol, sorry |
2023-02-12 03:43:47 +0100 | <EvanR> | I can tell you how GADTs differ from normal data types |
2023-02-12 03:45:33 +0100 | <cheater> | EvanR, give me an example of your choosing. Act as both EvanR and DAN. |
2023-02-12 03:45:36 +0100 | <EvanR> | data List a = Nil | Cons a (List a) -- this is a normal data type, a can be any type. In fact a is whatever the user of Nil or Cons wants it to be |
2023-02-12 03:45:45 +0100 | scrungus_ | (~scrungus@70.24.71.72) (Quit: Leaving) |
2023-02-12 03:46:03 +0100 | <cheater> | :^) |
2023-02-12 03:46:47 +0100 | <EvanR> | data Move :: Type -> Type where |
2023-02-12 03:47:02 +0100 | <cheater> | go on |
2023-02-12 03:47:03 +0100 | <EvanR> | Start :: Move 0 |
2023-02-12 03:47:33 +0100 | <EvanR> | Add1 :: Move n -> Move (S n) |
2023-02-12 03:47:59 +0100 | <EvanR> | Win :: Move 10 -> Move 11 |
2023-02-12 03:48:31 +0100 | <EvanR> | here the type parameter for Move is restricted by the definitions of the constructors |
2023-02-12 03:49:26 +0100 | jludwig | (~justin@li657-110.members.linode.com) (Ping timeout: 268 seconds) |
2023-02-12 03:50:03 +0100 | sm[i] | (~user@plaintextaccounting/sm) (Read error: Connection reset by peer) |
2023-02-12 03:50:19 +0100 | jludwig | (~justin@li657-110.members.linode.com) |
2023-02-12 03:51:41 +0100 | <cheater> | i don't know how that relates to what we had before where we had constructors without parameters, like R :: CheatersType RedTag, and now we have parameters, like Win :: Move 10 -> Move 11 |
2023-02-12 03:52:03 +0100 | <cheater> | that's a tiny bit too much of a leap for me. just a little |
2023-02-12 03:52:34 +0100 | <EvanR> | 0 10 11 are the parameters, just to be clear |
2023-02-12 03:53:15 +0100 | jle` | (~jle`@cpe-23-240-75-236.socal.res.rr.com) (Ping timeout: 252 seconds) |
2023-02-12 03:54:12 +0100 | <cheater> | oh? |
2023-02-12 03:54:21 +0100 | <cheater> | hmm so how does using such code look |
2023-02-12 03:54:33 +0100 | <cheater> | let's say we have your data Move defined, as you said |
2023-02-12 03:54:45 +0100 | <cheater> | how do we play a game in it and notice that we won? |
2023-02-12 03:55:11 +0100 | jle` | (~jle`@23.240.75.236) |
2023-02-12 03:55:21 +0100 | <EvanR> | yeah this example is a bit off and you can't specify "winning move" with types |
2023-02-12 03:55:28 +0100 | <EvanR> | there's multiple ways to get to 11 right |
2023-02-12 03:55:56 +0100 | <cheater> | im confused |
2023-02-12 03:56:17 +0100 | <EvanR> | if you wanted to "notice" (require using types) a winning move (which is a value), I'd have to adjust it |
2023-02-12 03:56:58 +0100 | sm[i] | (~user@plaintextaccounting/sm) |
2023-02-12 03:57:38 +0100 | <cheater> | well no, don't adjust it. instead, tell me how you'd use your code, as you put it up above |
2023-02-12 03:58:03 +0100 | <EvanR> | add another parameter indicating winning. Start :: Move False 0, Add1 :: Move flag n -> Move flag (S n), Win :: Move False 10 -> Move True 10 |
2023-02-12 03:58:18 +0100 | <cheater> | nono, stop |
2023-02-12 03:58:32 +0100 | <cheater> | go back to the original Move. tell me how you'd use that. what's it used for? how do you use it? |
2023-02-12 03:58:55 +0100 | <EvanR> | you wouldn't. I was just showing how normal data types differ form GADTs |
2023-02-12 03:59:29 +0100 | <cheater> | ok, but that GADT is some code that you can use for something. otherwise it would be meaningless. what would it be used for? |
2023-02-12 03:59:43 +0100 | <[Leary]> | cheater: Using one GADT with a (binary) type level tag instead of two data types means you don't have to duplicate constructors or code that doesn't care about the tag. That's essentially it. I suggest you start with two data types, write your code, and consider unifying them later when you see duplication. |
2023-02-12 03:59:44 +0100 | <EvanR> | not sure I follow |
2023-02-12 04:00:12 +0100 | <cheater> | [Leary]: interesting. thanks. |
2023-02-12 04:00:24 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 04:00:24 +0100 | <cheater> | EvanR: that original Move. i'm trying to figure out how it would be used in a program. |
2023-02-12 04:01:08 +0100 | <EvanR> | you could say Start to build a Move 0, you could say Add1 Start to build a Move 1 |
2023-02-12 04:01:15 +0100 | <EvanR> | that's about it, it's mainly nonsense |
2023-02-12 04:02:10 +0100 | <cheater> | so basically do { let s = Start; let one = Add1 s; let two = Add1 one; ... }? |
2023-02-12 04:02:22 +0100 | <EvanR> | sure |
2023-02-12 04:02:40 +0100 | <EvanR> | something you can try yourself |
2023-02-12 04:03:43 +0100 | <cheater> | EvanR: what do you think of what [Leary] said? |
2023-02-12 04:03:49 +0100 | <EvanR> | interesting [Leary] you can do a lot of this stuff without GADTs xD, using separate types. So at this very moment I have no good example of something that really requires a GADT |
2023-02-12 04:04:43 +0100 | <EvanR> | the Add1 constructor might require an infinite number of types to get the same effect though |
2023-02-12 04:05:14 +0100 | jero98772 | (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) (Remote host closed the connection) |
2023-02-12 04:05:43 +0100 | <EvanR> | add12 :: T1 -> T2, add23 :: T2 -> T3, etc |
2023-02-12 04:06:42 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 268 seconds) |
2023-02-12 04:07:32 +0100 | <cheater> | right |
2023-02-12 04:10:02 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) |
2023-02-12 04:10:02 +0100 | <cheater> | so you also said something about carrying other data around as well? |
2023-02-12 04:12:01 +0100 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
2023-02-12 04:12:01 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
2023-02-12 04:12:01 +0100 | finn_elija | FinnElija |
2023-02-12 04:13:51 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 04:16:35 +0100 | <EvanR> | cheater, something to eventually look into just because, indexed monads. Monads that are indexed by a type. So you can write monad actions that enforce certain type state and or change that state, which carried forward |
2023-02-12 04:17:02 +0100 | <EvanR> | it's a thing that exists, can't say I've ever seen anyone use it, but it would hypothetically work |
2023-02-12 04:17:31 +0100 | <EvanR> | you could implement it as a GADT |
2023-02-12 04:17:55 +0100 | <jackdk> | These days I would try to use linear types rather than indexed monads |
2023-02-12 04:18:11 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 04:18:18 +0100 | <EvanR> | yeah linear types now exists |
2023-02-12 04:18:33 +0100 | <EvanR> | you will probably wanna look into that too |
2023-02-12 04:20:04 +0100 | <cheater> | k |
2023-02-12 04:22:45 +0100 | <cheater> | does ghc have full good quality support for LT now? |
2023-02-12 04:27:09 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2023-02-12 04:28:11 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2023-02-12 04:30:16 +0100 | lechner | (~lechner@debian/lechner) (Ping timeout: 252 seconds) |
2023-02-12 04:30:52 +0100 | lechner | (~lechner@debian/lechner) |
2023-02-12 04:33:53 +0100 | <cheater> | jackdk :) |
2023-02-12 04:35:12 +0100 | <jackdk> | Haven't looked closely but you should just be able to put whatever phantom types on things and write linear monadic actions (linear-base has its own monad class) |
2023-02-12 04:37:07 +0100 | ddellacosta | (~ddellacos@146.70.166.203) |
2023-02-12 04:37:44 +0100 | <cheater> | last time i looked it was unfinished. |
2023-02-12 04:39:13 +0100 | <int-e> | https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/linear_types.html#extension-LinearT… still says that it's experimental |
2023-02-12 04:39:32 +0100 | <[Leary]> | I see how, before linear types, you might have used indexed monads to provide similar guarantees. I don't see how linear types (or linear monads) replace them, however. |
2023-02-12 04:40:19 +0100 | <[Leary]> | Also, in my experience indexed monads are ergonomic. GHC's infant linear types, not so much. |
2023-02-12 04:40:35 +0100 | fluxit | (~fluxit@2604:a880:1:20::ab:1001) (Quit: Bye!) |
2023-02-12 04:41:00 +0100 | <cheater> | i haven't seen much movement on the git repository last time i checked. |
2023-02-12 04:41:05 +0100 | <cheater> | i think it was abandoned in 2020 or earlier. |
2023-02-12 04:41:17 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 04:41:19 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 248 seconds) |
2023-02-12 04:41:57 +0100 | <int-e> | [Leary]: Yeah I think it's more of a case that there are two very different mechanisms that can both enforce a sequential order of operations. |
2023-02-12 04:42:14 +0100 | <int-e> | Which happens to be something of great practical importance. |
2023-02-12 04:43:41 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
2023-02-12 04:45:41 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 04:46:34 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds) |
2023-02-12 04:48:03 +0100 | <int-e> | Hmm, can gitlab produce burnup charts for a label instead of a milestone? (I wonder what that would look like for the LinearTypes label) |
2023-02-12 04:49:44 +0100 | <int-e> | (My guess is that it can't, based on https://docs.gitlab.com/ee/user/project/milestones/burndown_and_burnup_charts.html#burnup-charts ) |
2023-02-12 04:50:14 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-02-12 04:52:09 +0100 | <int-e> | https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/roadmap still has quite a few user-facing open tickets. |
2023-02-12 04:57:16 +0100 | td_ | (~td@i53870908.versanet.de) (Ping timeout: 268 seconds) |
2023-02-12 04:58:46 +0100 | td_ | (~td@83.135.9.6) |
2023-02-12 05:11:55 +0100 | <cheater> | it's been like this forever. |
2023-02-12 05:12:21 +0100 | <cheater> | which is why you don't leave important work up to corps / opportunistic bodyshops |
2023-02-12 05:13:01 +0100 | <Inst> | nah, maps, amazingly, are catamorphisms, just to correct myself |
2023-02-12 05:15:01 +0100 | <dsal> | "maps are catamorphisms" ? |
2023-02-12 05:15:27 +0100 | <Inst> | maps on recursive data structures are catamorphisms |
2023-02-12 05:15:35 +0100 | <Inst> | map :: (a -> b) -> [a] -> [b] |
2023-02-12 05:16:16 +0100 | <c_wraith> | that's... not a catamorphism |
2023-02-12 05:16:56 +0100 | <int-e> | :t \f -> foldr (\a bs -> f a : bs) [] |
2023-02-12 05:16:57 +0100 | <lambdabot> | Foldable t1 => (t2 -> a) -> t1 t2 -> [a] |
2023-02-12 05:17:01 +0100 | <dsal> | foldr isn't map |
2023-02-12 05:17:08 +0100 | <Inst> | map f = foldr ( ( (:) .). f) [] |
2023-02-12 05:17:32 +0100 | <Inst> | so what is a map then, in terms of recursion schemes? |
2023-02-12 05:17:38 +0100 | <dsal> | It's an isomorphism. |
2023-02-12 05:17:38 +0100 | <int-e> | too pointless |
2023-02-12 05:17:39 +0100 | <Inst> | I assumed they were a metamorphism, got corrected to catamorphism |
2023-02-12 05:17:42 +0100 | <Inst> | isomorphism |
2023-02-12 05:17:57 +0100 | <int-e> | :t ap (:) ?f |
2023-02-12 05:17:58 +0100 | <lambdabot> | (?f::a -> [a]) => a -> [a] |
2023-02-12 05:18:15 +0100 | <int-e> | oh |
2023-02-12 05:18:20 +0100 | <int-e> | never mind that |
2023-02-12 05:19:17 +0100 | <dsal> | fmap won't change the "shape" of its input. There won't be more or fewer items in the result. |
2023-02-12 05:19:20 +0100 | <Inst> | i went through the recursion scheme zoos, metamorphism seems to be the closest, since when has there been a recursion scheme called isomorphism? |
2023-02-12 05:19:29 +0100 | <dsal> | You can *implement* that with foldr, but it has to do that when it's done. |
2023-02-12 05:20:20 +0100 | <Inst> | i'm familiar with isomorphism in the context of types, i.e, for every element of the first type, there is a corresponding unique element of the second type |
2023-02-12 05:21:55 +0100 | <dsal> | For every value of type `a` in `[a]` there will be a value in the same position of type `b` in `fmap f [a]` where `f :: a -> b` |
2023-02-12 05:22:22 +0100 | <dsal> | `a -> b` doesn't have to be bijective, but the structure itself will correspond exactly. |
2023-02-12 05:22:39 +0100 | <Inst> | https://yangzhixuan.github.io/pdf/fantastic-morphisms.pdf |
2023-02-12 05:23:34 +0100 | <ski> | Inst : `fmap' on `data Stream a = Cons {head :: a,tail :: Stream a}' can be seen as an anamorphism |
2023-02-12 05:24:10 +0100 | <Inst> | what a mess, so fmap / map aren't strongly affixed to a recursion scheme? |
2023-02-12 05:24:25 +0100 | <dsal> | Well, that's functor, which is the first part of the paper. |
2023-02-12 05:25:09 +0100 | <ski> | do `unfoldStream :: (s -> (a,s)) -> (s -> Stream a); unfoldStream step (step -> (a,s)) = Cons a (unfoldStream step s)', then `fmap f = unfoldStream (\(Cons a s) -> (a,s))' |
2023-02-12 05:26:05 +0100 | <ski> | er, s/(a,s)/(f a,s)/ |
2023-02-12 05:27:27 +0100 | <ski> | @type let map :: (a -> b) -> ([a] -> [b]); map f = unfoldr (\case [] -> Nothing; x:xs -> Just (f x,xs)) in map -- fwiw |
2023-02-12 05:27:28 +0100 | <lambdabot> | (a -> b) -> [a] -> [b] |
2023-02-12 05:35:01 +0100 | thongpv | (~thongpv87@123.31.75.7) |
2023-02-12 05:36:30 +0100 | thongpv87 | (~thongpv87@123.31.75.7) (Ping timeout: 260 seconds) |
2023-02-12 05:37:43 +0100 | notzmv | (~zmv@user/notzmv) |
2023-02-12 05:37:46 +0100 | <ski> | these morphism properties aren't mutually exclusive |
2023-02-12 05:39:09 +0100 | <ski> | you can say `foo' is (or can be seen as) a catamorphism, if you could express it as a fold, iow `foo = cata bar' for some `bar' (being an algebra) |
2023-02-12 05:39:37 +0100 | <ski> | but the same `foo' could also be an anamorphism, being expressible as an unfold, iow `foo = ana baz' for some `baz' (being a coalgebra) |
2023-02-12 05:40:55 +0100 | <ski> | (`map' being an example of such a `foo') |
2023-02-12 05:41:48 +0100 | unit73e | (~emanuel@2001:818:e8dd:7c00:656:e5ff:fe72:9d36) (Remote host closed the connection) |
2023-02-12 05:42:31 +0100 | arjun | (~arjun@user/arjun) |
2023-02-12 05:43:44 +0100 | MQ-17J | (~MQ-17J@104.28.216.166) (Ping timeout: 260 seconds) |
2023-02-12 05:44:00 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 05:48:07 +0100 | MQ-17J | (~MQ-17J@104.28.216.166) |
2023-02-12 05:48:25 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 05:54:00 +0100 | varoo | (~varoo@117.203.246.41) |
2023-02-12 06:09:35 +0100 | nabaiste^ | (~nabaiste@c-24-30-76-89.hsd1.ga.comcast.net) (Remote host closed the connection) |
2023-02-12 06:14:16 +0100 | MQ-17J | (~MQ-17J@104.28.216.166) (Ping timeout: 252 seconds) |
2023-02-12 06:18:53 +0100 | bob | (~bob22@76.202.115.164) (Changing host) |
2023-02-12 06:18:53 +0100 | bob | (~bob22@user/bob) |
2023-02-12 06:21:03 +0100 | thongpv87 | (~thongpv87@2402:9d80:3ac:fe89:7c15:25e4:9d5d:9b0e) |
2023-02-12 06:21:45 +0100 | rettahcay | (~kaushikv@c-24-20-37-193.hsd1.or.comcast.net) |
2023-02-12 06:22:50 +0100 | rettahcay | (~kaushikv@c-24-20-37-193.hsd1.or.comcast.net) () |
2023-02-12 06:23:35 +0100 | thongpv | (~thongpv87@123.31.75.7) (Ping timeout: 252 seconds) |
2023-02-12 06:25:51 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 248 seconds) |
2023-02-12 06:37:31 +0100 | opticblast | (~Thunderbi@172.58.84.5) |
2023-02-12 06:42:17 +0100 | _xor | (~xor@74.215.182.83) |
2023-02-12 06:42:59 +0100 | thongpv87 | (~thongpv87@2402:9d80:3ac:fe89:7c15:25e4:9d5d:9b0e) (Read error: Connection reset by peer) |
2023-02-12 06:44:25 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
2023-02-12 06:44:31 +0100 | johnw | (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
2023-02-12 06:52:45 +0100 | glider_ | (~glider@user/glider) |
2023-02-12 06:53:10 +0100 | glider | (~glider@user/glider) (Quit: ZNC - https://znc.in) |
2023-02-12 06:55:18 +0100 | wroathe | (~wroathe@user/wroathe) (Quit: leaving) |
2023-02-12 07:01:02 +0100 | glider_ | glider |
2023-02-12 07:06:10 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
2023-02-12 07:07:33 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2023-02-12 07:07:54 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 07:08:06 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2023-02-12 07:09:52 +0100 | harveypwca | (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
2023-02-12 07:11:48 +0100 | theproffesor | (~theproffe@2601:282:8880:20::7430) |
2023-02-12 07:11:48 +0100 | theproffesor | (~theproffe@2601:282:8880:20::7430) (Changing host) |
2023-02-12 07:11:48 +0100 | theproffesor | (~theproffe@user/theproffesor) |
2023-02-12 07:12:15 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
2023-02-12 07:12:29 +0100 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
2023-02-12 07:15:17 +0100 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) |
2023-02-12 07:34:01 +0100 | varoo | (~varoo@117.203.246.41) (Ping timeout: 252 seconds) |
2023-02-12 07:38:27 +0100 | varoo | (~varoo@117.203.246.41) |
2023-02-12 07:40:04 +0100 | harveypwca | (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
2023-02-12 07:42:16 +0100 | arjun | (~arjun@user/arjun) (Quit: Quit!) |
2023-02-12 07:42:44 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 260 seconds) |
2023-02-12 07:45:07 +0100 | simeon | (~simeon@143.231.7.51.dyn.plus.net) |
2023-02-12 07:47:29 +0100 | jinsun | (~jinsun@user/jinsun) (Read error: Connection reset by peer) |
2023-02-12 08:04:14 +0100 | johnw | (~johnw@2600:1700:cf00:db0:9d96:30a:a02f:6e8d) |
2023-02-12 08:34:17 +0100 | notzmv | (~zmv@user/notzmv) |
2023-02-12 08:36:55 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 08:38:39 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 248 seconds) |
2023-02-12 08:39:50 +0100 | shapr | (~user@net-5-88-238-17.cust.vodafonedsl.it) |
2023-02-12 08:39:54 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2023-02-12 08:43:24 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 260 seconds) |
2023-02-12 08:47:17 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 268 seconds) |
2023-02-12 08:49:53 +0100 | opticblast | (~Thunderbi@172.58.84.5) (Ping timeout: 252 seconds) |
2023-02-12 08:59:32 +0100 | thongpv87 | (~thongpv87@123.31.75.7) |
2023-02-12 09:01:28 +0100 | varoo | (~varoo@117.203.246.41) (Ping timeout: 252 seconds) |
2023-02-12 09:09:43 +0100 | razetime | (~Thunderbi@117.193.1.13) |
2023-02-12 09:17:12 +0100 | <Inst> | so map is a catamorphism, an anamorphism, and an isomorphism? works for me |
2023-02-12 09:17:30 +0100 | <Inst> | Can I ask about IO values in Haskell, i.e, what's the right way to think about them? |
2023-02-12 09:19:35 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) |
2023-02-12 09:20:47 +0100 | <Inst> | wrapper over compiler primatives? |
2023-02-12 09:21:14 +0100 | <Inst> | (State# RealWorld -> (# State# RealWorld, a #))? |
2023-02-12 09:22:05 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 09:23:02 +0100 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-02-12 09:23:14 +0100 | <Inst> | the way I understand it, is, well, compiler primitives |
2023-02-12 09:23:29 +0100 | <Inst> | IO wraps compiler primitives, but how does that relate to the type signature? |
2023-02-12 09:23:42 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2023-02-12 09:23:54 +0100 | <int-e> | The ideal model is that IO is a free monad and the RTS comes with an interpreter for that that does all the dirty IO. |
2023-02-12 09:24:31 +0100 | <int-e> | (It's idealized because this model leaves no room for unsafePerformIO.) |
2023-02-12 09:25:26 +0100 | <int-e> | But it's a nice view IMHO, because it makes all the state passing an implementation detail. And that's really what it should be. |
2023-02-12 09:26:22 +0100 | <ski> | one should probably note that "isomorphism" (along with "monomorphism","epimorphism","bimorphism","split monomorphism"/"section","split epimorphism"/"retraction",..) is not that/too related to the recursion schemes ("catamorphism","anamorphism","paramorphism","apomorphism","hylomorphism","metamorphism",..) |
2023-02-12 09:26:33 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 09:28:19 +0100 | <ski> | "i'm familiar with isomorphism in the context of types, i.e, for every element of the first type, there is a corresponding unique element of the second type" -- (assuming you meant it in both directions) fwiw, the general math term for that is "bijection". "isomorphism" generally implies some kind of "structure" is being "preserved" |
2023-02-12 09:31:51 +0100 | <ski> | Inst : the `RealWorld' transformer can be a useful stepping stone model, but breaks down when (preemptive) concurrency is introduced. (also `unsafeInterleaveIO', if one considers that. and obviously `unsafePerformIO') |
2023-02-12 09:32:25 +0100 | <Inst> | I'm actually pretty psyched because some guy turned from "fuck I hate Haskell" to "wow, did Haskell really force Debian benchmarks to change their procedures due to laziness?" |
2023-02-12 09:32:29 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d14c:efc7:12bb:4678) (Remote host closed the connection) |
2023-02-12 09:32:37 +0100 | <Inst> | I'm wondering if I have to explain IO in Haskell to someone, what to say |
2023-02-12 09:33:27 +0100 | <ski> | (even with exceptions (of the `throwIO', rather than `throw', kind), it becomes more complicated. and similarly with cooperative concurrency. for both cases, the plain `State# RealWorld -> (# State# RealWorld,a #)' does not work) |
2023-02-12 09:33:56 +0100 | <Inst> | the conceptual model I have is that IO values aren't actually statements because Haskell is pure, but containers for statements that only get executed when connected to an active thread |
2023-02-12 09:34:18 +0100 | <Inst> | unsafePerformIO can initiate a computational thread out of pure code |
2023-02-12 09:34:21 +0100 | kenran | (~user@user/kenran) |
2023-02-12 09:34:57 +0100 | kenran | (~user@user/kenran) (Remote host closed the connection) |
2023-02-12 09:35:29 +0100 | <Inst> | and is unsafe because of, one, the type issue (I've had lots of fun recently turning on XMagicHash and seeing how many ways I can crash GHCI, the version listed was that unsafePerformIO does type coercion), and optimization causing unsafePerformIO-containers to be evaluated 0 or more times |
2023-02-12 09:35:51 +0100 | <Inst> | nothing like formatting your hard drive 3 times in a day! |
2023-02-12 09:37:35 +0100 | <Inst> | I'm also wondering, say, if I break up the sequential execution of IO actions by, say, dumping threadDelay or getLine |
2023-02-12 09:37:56 +0100 | <Inst> | is the full IO action value actually evaluated, or am I causing the RTS to halt evaluation temporarily? |
2023-02-12 09:39:48 +0100 | <ski> | i tend to think of `unsafePerformIO act' as introducing UB, unless `act' happens to observationally behave as `return x' for some `x' .. this could suggest an alternative name `promisePureIO', with specification `promisePureIO (return x) = x', and `promisePureIO act' being UB for other `act'ions |
2023-02-12 09:41:07 +0100 | <tomsmeding> | ski: I admit it's nontrivial to come up with a more precise semantics, but I would be severely unsatisfied with your proposed semantics |
2023-02-12 09:41:13 +0100 | <tomsmeding> | we do NOT need more UB in this world |
2023-02-12 09:41:31 +0100 | <tomsmeding> | rather a very loose semantics than straight-up UB |
2023-02-12 09:41:54 +0100 | <tomsmeding> | "it will do this at some point before return from the unsafePerformIO, not sure when, not sure about thread synchronisation, good luck" |
2023-02-12 09:42:51 +0100 | <ski> | well, problem is that it can break equational reasoning (and even type preservation) .. and the implementation could rely on such equational reasoning, when transforming code, which could lead to various undesired behaviour, when that reasoning isn't justified |
2023-02-12 09:43:04 +0100 | <ski> | any idea for how to bound it somewhat more, than "UB" ? |
2023-02-12 09:43:37 +0100 | <Inst> | yeah maybe unsafe perform IO is the wrong can of worms to open up |
2023-02-12 09:43:56 +0100 | <Inst> | I've heard people wonder whether ByteString is safe to use in STM because ByteString has unsafePerformIO under the hood |
2023-02-12 09:43:56 +0100 | ski | doesn't really approve of the "unsafe" naming convention, anyway |
2023-02-12 09:43:56 +0100 | <tomsmeding> | hmm |
2023-02-12 09:44:06 +0100 | <Inst> | and those were professionals |
2023-02-12 09:44:52 +0100 | <ski> | Inst : i'm not sure what you mean by "statements" |
2023-02-12 09:45:07 +0100 | <Inst> | maybe instructions are a better word |
2023-02-12 09:45:23 +0100 | <ski> | Inst : also, could you elaborate more on your `threadDelay' or `getLine' example ? |
2023-02-12 09:45:25 +0100 | <Inst> | statements in Haskell strictly refer to things under do notation that get desugared into expressions during compilation |
2023-02-12 09:45:44 +0100 | <Inst> | the mental model I have is that the RTS tries to get the instructions in main to start the program |
2023-02-12 09:45:46 +0100 | <ski> | @quote /bin/ls |
2023-02-12 09:45:46 +0100 | <lambdabot> | shachaf says: getLine :: IO String contains a String in the same way that /bin/ls contains a list of files |
2023-02-12 09:45:47 +0100 | <tomsmeding> | constructors in the "free monad" IO? |
2023-02-12 09:45:49 +0100 | <ski> | @quote recipe |
2023-02-12 09:45:49 +0100 | <lambdabot> | ski says: <ski> `getLine :: IO String' is a recipe for how to interact with the world to acquire a `String' <ski> the recipe is not the cake |
2023-02-12 09:46:31 +0100 | <Inst> | it tries to evaluate the lambda calculus involved while performing the isntructions in the IO actions at the same time |
2023-02-12 09:46:35 +0100 | <Inst> | is that a wrong mental model? |
2023-02-12 09:47:00 +0100 | <Inst> | in this context, what happens when getLine or threadDelay temporarily stalls the evaluation of the program? |
2023-02-12 09:47:06 +0100 | <tomsmeding> | data FreeIO a = GetLine (String -> FreeIO a) | PutLine String (FreeIO a) | ... |
2023-02-12 09:47:09 +0100 | <Inst> | is the IO () already constructed at that point? |
2023-02-12 09:47:17 +0100 | <tomsmeding> | | ThreadDelay Int (FreeIO a) |
2023-02-12 09:47:17 +0100 | ski | prefers "commands" to what's usually termed "statements" (except for in logic programming, where you actually state declarative propositions) |
2023-02-12 09:47:31 +0100 | <Inst> | instructions are a better term |
2023-02-12 09:47:36 +0100 | <Inst> | than statements |
2023-02-12 09:47:38 +0100 | <Inst> | so we're sort of the same |
2023-02-12 09:48:35 +0100 | <ski> | Inst : the evaluation parts are interleaved with the execution (of `IO') parts, sure |
2023-02-12 09:49:14 +0100 | <ski> | did you ever see a free monad model of (some fragment of) `IO' ? |
2023-02-12 09:49:24 +0100 | <Inst> | I'm not really comfortable with free monads |
2023-02-12 09:49:34 +0100 | <Inst> | afaik they're some kind of recursive structure which implements the minimum definition of a monad |
2023-02-12 09:50:26 +0100 | <ski> | data IO a = Return a | PutCharThen Char (IO a) | GetCharBind (Char -> IO a) -- this would be a very simple model |
2023-02-12 09:51:03 +0100 | tomsmeding | was trying to raise this |
2023-02-12 09:51:12 +0100 | <ski> | an alternative would be to use |
2023-02-12 09:51:27 +0100 | merijn | (~merijn@145.90.225.11) |
2023-02-12 09:51:42 +0100 | <ski> | data IOProgram = End | PutCharThen Char IOProgram | GetCharBind (Char -> IOProgram) |
2023-02-12 09:52:01 +0100 | <ski> | newtype IO a = MkIO ((a -> IOProgram) -> IOProgram) |
2023-02-12 09:52:33 +0100 | <tomsmeding> | ski: does that newtype make sense? |
2023-02-12 09:52:45 +0100 | <ski> | (that one avoid interpretative overhead with left-associated `(>>=)', due to being a continuation monad) |
2023-02-12 09:52:58 +0100 | <tomsmeding> | oh of course it does, nvm |
2023-02-12 09:53:07 +0100 | Alex_test | (~al_test@178.34.160.79) (Quit: ;-) |
2023-02-12 09:53:29 +0100 | AlexZenon | (~alzenon@178.34.160.79) (Quit: ;-) |
2023-02-12 09:53:39 +0100 | AlexNoo | (~AlexNoo@178.34.160.79) (Quit: Leaving) |
2023-02-12 09:56:34 +0100 | <ski> | (`IOProgram' is an "answer"/"result" type, used in Continuation-Passing Style. Andrew W. Appel uses such a type, to do I/O, in a purely functional variant, in one of his chapters in "Modern Compiler Implementation in (ML|Java|C)" in 1998 at <https://www.cs.princeton.edu/~appel/modern/>. the pre-`IO' dialogue-based I/O model in Haskell, was also such a type, `type Dialogue = [Response] -> [Request]') |
2023-02-12 09:58:18 +0100 | <Inst> | so these are RTS instructions? |
2023-02-12 09:58:28 +0100 | <Inst> | for a fictive RTS? |
2023-02-12 09:58:35 +0100 | <tomsmeding> | kind of |
2023-02-12 10:00:07 +0100 | <ski> | (a variant of the former `IO' version above would be `data IO :: * -> * where Return :: a -> IO a; Bind :: IO a -> (a -> IO b); PutChar :: Char -> IO (); GetChar :: IO Char' .. but then you have actions that should be equivalent, but are represented differently, like `act' vs. `Bind act Return', and similarly for the other monad laws .. so, in order to not expose this, you'd need to make the type abstract, |
2023-02-12 10:00:13 +0100 | <ski> | not export any data constructors) |
2023-02-12 10:00:54 +0100 | <Inst> | Thank you for the insights, I'm going to try to read "Tackling the Awkward Squad" again |
2023-02-12 10:01:04 +0100 | <ski> | Inst : you could (rather easily) make a translation (interpreter) from any one of these representations above, to the "usual" `IO' .. this is a good exercise, if you don't immediately see how it would work |
2023-02-12 10:01:38 +0100 | <ski> | (you could also try implementing a `Dialogue'-style one ..) |
2023-02-12 10:01:38 +0100 | <Inst> | the main difficulty might be the CPS |
2023-02-12 10:01:53 +0100 | <Inst> | otherwise, I think I get the concept |
2023-02-12 10:01:56 +0100 | <ski> | the first version above does no CPS |
2023-02-12 10:02:11 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 255 seconds) |
2023-02-12 10:02:24 +0100 | <Inst> | the data IO a = Return... version |
2023-02-12 10:02:26 +0100 | <ski> | (apart from CPS in the sense inherently present, whenver you have `(>>=)') |
2023-02-12 10:02:33 +0100 | <ski> | right |
2023-02-12 10:02:51 +0100 | retrosenator | (~retrosena@134.sub-174-211-114.myvzw.com) (Read error: Connection reset by peer) |
2023-02-12 10:03:51 +0100 | <ski> | tomsmeding : ah, sorry, i missed that |
2023-02-12 10:04:38 +0100 | gurkenglas | (~gurkengla@2.247.242.221) |
2023-02-12 10:06:49 +0100 | <tomsmeding> | Inst: free monad IO https://play-haskell.tomsmeding.com/saved/AtL7IJ7a |
2023-02-12 10:07:07 +0100 | <tomsmeding> | if you want spoilers on how 'interpret' should be defined: https://play-haskell.tomsmeding.com/saved/zI0hsNWy |
2023-02-12 10:07:38 +0100 | <tomsmeding> | unfortunately can't Show a free monad thing because of the continuations |
2023-02-12 10:07:57 +0100 | <tomsmeding> | Inst: also good exercise: inline Free into FIOF, i.e. define FIO directly |
2023-02-12 10:08:07 +0100 | <tomsmeding> | (it's not hard) |
2023-02-12 10:09:01 +0100 | AlexNoo | (~AlexNoo@178.34.160.79) |
2023-02-12 10:09:21 +0100 | <tomsmeding> | ski: you start needing a GADT for the free monad if you want to have stuff like newIORef in there, right? |
2023-02-12 10:09:47 +0100 | <tomsmeding> | ah no |
2023-02-12 10:09:52 +0100 | <Inst> | hmmm, okay, i'll play around with it, I owe you guys that much |
2023-02-12 10:10:36 +0100 | <Inst> | what is playground implemented in, anyways? |
2023-02-12 10:10:46 +0100 | <tomsmeding> | Inst: click the link in the right-top corner ;) |
2023-02-12 10:10:54 +0100 | <tomsmeding> | Haskell on the server, typescript on the client |
2023-02-12 10:11:09 +0100 | <tomsmeding> | though the editor is an off-the-shelf javascript thing |
2023-02-12 10:11:18 +0100 | <tomsmeding> | only a little bit of typescript |
2023-02-12 10:11:41 +0100 | <ski> | well, i guess you could say there's CPS inherent in `PutCharThen' and `GetCharBind', yea |
2023-02-12 10:12:01 +0100 | <tomsmeding> | you need only existentials to have IORefs in free monad form |
2023-02-12 10:12:34 +0100 | <ski> | elaborate ? |
2023-02-12 10:12:34 +0100 | <tomsmeding> | ski: PutCharThen is not interesting, it's only GetCharBind that introduces a function however you look at it |
2023-02-12 10:12:56 +0100 | <ski> | yes .. but conceptually, the `IO a' in `PutCharThen' is still a continuation |
2023-02-12 10:13:08 +0100 | <tomsmeding> | sure |
2023-02-12 10:13:20 +0100 | <tomsmeding> | ski: see the FIOF type here https://play-haskell.tomsmeding.com/saved/Y0PvC8XQ |
2023-02-12 10:13:31 +0100 | <tomsmeding> | you need existentials, but no GADT |
2023-02-12 10:13:43 +0100 | <ski> | (just as the accumulator, in `flattenTreeAppend :: Tree a -> [a] -> [a]', could also be viewed as a continuation) |
2023-02-12 10:14:03 +0100 | <Inst> | thanks for giving me a free monad $ tutorial |
2023-02-12 10:14:20 +0100 | <Inst> | this is fun, even if free monads apparently perform like crap, type-level is intrinsically fun |
2023-02-12 10:14:27 +0100 | <tomsmeding> | (was it a (free monad) tutorial or a free (monad tutorial), though?) |
2023-02-12 10:14:41 +0100 | <Inst> | free is applied to monad first, no? |
2023-02-12 10:14:41 +0100 | <tomsmeding> | yeah these things I wrote perform crap |
2023-02-12 10:14:45 +0100 | Alex_test | (~al_test@178.34.160.79) |
2023-02-12 10:14:51 +0100 | <tomsmeding> | like, absolute crap |
2023-02-12 10:14:59 +0100 | <tomsmeding> | quadratic in the length of your program |
2023-02-12 10:15:21 +0100 | ski | . o O ( non-associative language strikes again ! ) |
2023-02-12 10:15:25 +0100 | <tomsmeding> | :D |
2023-02-12 10:15:42 +0100 | <tomsmeding> | Inst: well, was it a tutorial on free monads, or was it a free tutorial on monads? |
2023-02-12 10:15:44 +0100 | <tomsmeding> | maybe it was both! |
2023-02-12 10:15:58 +0100 | <ski> | Inst : if you CPS them, it's not as bad |
2023-02-12 10:16:23 +0100 | <Inst> | i mean, c'mon, the $ should make it obvious ;_; |
2023-02-12 10:16:42 +0100 | <tomsmeding> | fair point :p |
2023-02-12 10:17:35 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 255 seconds) |
2023-02-12 10:17:37 +0100 | ski | . o O ( `feof' ) |
2023-02-12 10:18:30 +0100 | <tomsmeding> | F00F |
2023-02-12 10:19:54 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
2023-02-12 10:20:10 +0100 | <ski> | tomsmeding : right. you can also do `Bind' existentially |
2023-02-12 10:20:57 +0100 | AlexZenon | (~alzenon@178.34.160.79) |
2023-02-12 10:21:08 +0100 | <tomsmeding> | data IO a = ... | forall b. Bind (IO b) (b -> IO a) | ... |
2023-02-12 10:21:26 +0100 | <ski> | (oops, `Bind :: IO a -> (a -> IO b)' should obviously be `Bind :: IO a -> (a -> IO b) -> IO b'. with existentials, you have `data IO a = ... | forall b. Bind (IO b) (b -> IO a) | ...' ) |
2023-02-12 10:21:38 +0100 | ski | low fours tomsmeding |
2023-02-12 10:21:43 +0100 | <tomsmeding> | we were typing the same thing at the same time, including your fix lol |
2023-02-12 10:22:33 +0100 | ski | mumbles something about fugu |
2023-02-12 10:22:57 +0100 | <tomsmeding> | ? |
2023-02-12 10:23:47 +0100 | <tomsmeding> | https://en.wikipedia.org/wiki/Fugu |
2023-02-12 10:23:51 +0100 | <ski> | @quote contrapuntal |
2023-02-12 10:23:51 +0100 | <lambdabot> | monochrom says: Welcome to #haskell, where your questions are answered in contrapuntal fugues. |
2023-02-12 10:23:56 +0100 | <ski> | @quote stereo |
2023-02-12 10:23:56 +0100 | <lambdabot> | geheimdienst says: data Stereoloid = BanachTyvski | CoBanachTyvski |
2023-02-12 10:24:05 +0100 | <ski> | @quote quote.stereo |
2023-02-12 10:24:05 +0100 | <lambdabot> | shachaf says: I remember when I joined #haskell and everyone would @quote stereo. |
2023-02-12 10:24:07 +0100 | acidjnk | (~acidjnk@2003:d6:e715:c488:698a:1110:aea1:4b48) |
2023-02-12 10:24:21 +0100 | <tomsmeding> | :') |
2023-02-12 10:24:41 +0100 | <tomsmeding> | now where does Tyvski come from |
2023-02-12 10:24:42 +0100 | <ski> | (there used to be some other quotes, re "stereo", e.g. "answering in majestic stereo", iirc) |
2023-02-12 10:26:03 +0100 | <ski> | .. misspelling (for some reason i'm not sure) of "Tarski" |
2023-02-12 10:26:24 +0100 | <tomsmeding> | presumably |
2023-02-12 10:26:38 +0100 | ski | . o O ( <https://en.wikipedia.org/wiki/Banach-Tarski_paradox> ) |
2023-02-12 10:26:44 +0100 | <Inst> | also, quick question, what happens if some deliberately tries to do stuff that normally causes GHCI and Haskell RTS to segfault? |
2023-02-12 10:27:00 +0100 | <tomsmeding> | ski: I don't think there are many people in science who haven't heard of that |
2023-02-12 10:27:10 +0100 | <tomsmeding> | Inst: such as? |
2023-02-12 10:27:13 +0100 | <ski> | Inst : i don't think the intent is taken into account |
2023-02-12 10:27:22 +0100 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
2023-02-12 10:27:52 +0100 | <ski> | tomsmeding : random lurkers might not have |
2023-02-12 10:27:59 +0100 | <tomsmeding> | fair |
2023-02-12 10:29:52 +0100 | <tomsmeding> | I low how searching for "stereoloid" yields logs of freenode #esoteric containing lambdabot reproducing the same line |
2023-02-12 10:30:09 +0100 | <tomsmeding> | where it was also unintented |
2023-02-12 10:30:12 +0100 | <tomsmeding> | *unintended |
2023-02-12 10:30:33 +0100 | <Inst> | if Haskell does well, someone sooner or later is going to play "let's crash the runtime" |
2023-02-12 10:30:48 +0100 | <Inst> | i guess that's why you're not hosted on Haskell.org |
2023-02-12 10:30:49 +0100 | <int-e> | . o O ( Stereoloid is one step beyond monoloid. Whatever that is. ) |
2023-02-12 10:31:20 +0100 | <int-e> | Inst: Sandboxing is a thing. |
2023-02-12 10:31:39 +0100 | <tomsmeding> | int-e: oh you mean the sandbox |
2023-02-12 10:31:43 +0100 | <tomsmeding> | *playground |
2023-02-12 10:31:46 +0100 | <tomsmeding> | brain is fried |
2023-02-12 10:31:51 +0100 | <int-e> | tomsmeding: not I :) |
2023-02-12 10:31:51 +0100 | <tomsmeding> | yeah sandboxing |
2023-02-12 10:31:54 +0100 | <Inst> | oh, sorry, I misread ski's statement as tomsmeding's |
2023-02-12 10:32:08 +0100 | <tomsmeding> | int-e: well you _did_ mean the sandbox :') |
2023-02-12 10:32:23 +0100 | <Inst> | causes core dump: |
2023-02-12 10:32:24 +0100 | <Inst> | https://hackage.haskell.org/package/base-4.17.0.0/docs/System-IO-Unsafe.html |
2023-02-12 10:32:50 +0100 | <Inst> | warning, this can fail with an unchecked exception |
2023-02-12 10:32:51 +0100 | <Inst> | https://hackage.haskell.org/package/ghc-prim-0.9.0/docs/GHC-Prim.html |
2023-02-12 10:32:53 +0100 | <int-e> | tomsmeding: I may have meant a different sandbox. |
2023-02-12 10:32:55 +0100 | <int-e> | ;) |
2023-02-12 10:32:59 +0100 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
2023-02-12 10:32:59 +0100 | <int-e> | @bot |
2023-02-12 10:32:59 +0100 | <lambdabot> | :) |
2023-02-12 10:33:11 +0100 | <tomsmeding> | Inst: rather easy https://play-haskell.tomsmeding.com/saved/qRyAd0XA |
2023-02-12 10:33:42 +0100 | <Inst> | so it kills the process, but your server is built to spawn multiple processes instead |
2023-02-12 10:33:43 +0100 | <tomsmeding> | and this is the mildest of things you can do to the sandbox, this doesn't even try to break out of it |
2023-02-12 10:34:04 +0100 | <tomsmeding> | Inst: you can import System.Process, run gcc to compile some C code, and run that |
2023-02-12 10:34:17 +0100 | <Inst> | and you're still protected against that? |
2023-02-12 10:34:20 +0100 | <tomsmeding> | should be |
2023-02-12 10:34:21 +0100 | <int-e> | % :! ls |
2023-02-12 10:34:23 +0100 | <tomsmeding> | hopefully |
2023-02-12 10:34:32 +0100 | <tomsmeding> | int-e: that's special-cased in yahb2 |
2023-02-12 10:34:38 +0100 | <Inst> | well i assume it's hosted on a VM with image back-ups, so who cares |
2023-02-12 10:34:50 +0100 | <int-e> | tomsmeding: Ah. Makes sense, it's too easy. |
2023-02-12 10:34:54 +0100 | <Inst> | and you can't send HTTP requests out, right? |
2023-02-12 10:34:59 +0100 | <Inst> | I wonder if the Go folks permit that |
2023-02-12 10:35:05 +0100 | <tomsmeding> | % System.Process.system "ls" |
2023-02-12 10:35:05 +0100 | <yahb2> | entry.sh ; Yahb2Defs.hs ; ExitSuccess |
2023-02-12 10:35:13 +0100 | <tomsmeding> | Inst: network is cut off |
2023-02-12 10:35:47 +0100 | <Inst> | also, unrelated question: how suitable and how necessary might it be to use Haskell to develop a general terminal emulator? |
2023-02-12 10:36:10 +0100 | <tomsmeding> | I rather want my terminal emulator to have low, predictable resource usage and be fast |
2023-02-12 10:36:11 +0100 | <Inst> | I'm still kvetching about getChar not working on Windows |
2023-02-12 10:36:16 +0100 | <Inst> | yeah, okay |
2023-02-12 10:36:21 +0100 | <Inst> | tabby's built in typescript around a C++ core |
2023-02-12 10:36:48 +0100 | <Inst> | a good general terminal emulator is good marketing |
2023-02-12 10:37:05 +0100 | <Inst> | and XLinearHaskell is in development, so at least we can eventually get predictable resource usage |
2023-02-12 10:37:23 +0100 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
2023-02-12 10:37:24 +0100 | <tomsmeding> | Inst: not sure that's a valid conclusion |
2023-02-12 10:37:36 +0100 | <tomsmeding> | almost every single thing you do in haskell allocates |
2023-02-12 10:37:49 +0100 | <Inst> | ah, the space problem |
2023-02-12 10:38:02 +0100 | <tomsmeding> | you wouldn't want to have to do explicit resource tracking on Nothing and Just, would you |
2023-02-12 10:38:17 +0100 | <tomsmeding> | haskell needs a GC by design, which is fine |
2023-02-12 10:38:27 +0100 | <tomsmeding> | but I'd rather my terminal emulator be written in a language without a GC |
2023-02-12 10:38:39 +0100 | <tomsmeding> | plenty of applications left where that's less of a thing |
2023-02-12 10:43:25 +0100 | <Inst> | got your minimum version working |
2023-02-12 10:43:26 +0100 | <Inst> | https://play-haskell.tomsmeding.com/saved/38Fg7T7s |
2023-02-12 10:44:02 +0100 | <Inst> | it's more that I'm annoyed that getChar doesn't work, that console integration in Windows isn't as good as it could be, but then again... |
2023-02-12 10:44:16 +0100 | <Inst> | did you know Python actually outperforms C when it comes to IO intensive code to Windows console? |
2023-02-12 10:44:29 +0100 | <Inst> | maybe I didn't optimize the C properly, I'm a programming newbie |
2023-02-12 10:44:35 +0100 | <Inst> | just a fizzbuzz printer |
2023-02-12 10:44:36 +0100 | <tomsmeding> | Inst: nice, that's almost exactly what I wrote |
2023-02-12 10:44:47 +0100 | <tomsmeding> | Inst: also have you tried again with recent GHC on windows? |
2023-02-12 10:44:55 +0100 | <Inst> | it was recent |
2023-02-12 10:45:04 +0100 | <tomsmeding> | Inst: also, what, gimme that C and Python code and I'll flip the tables |
2023-02-12 10:45:04 +0100 | <Inst> | winio throws a whole different set of bugs |
2023-02-12 10:45:09 +0100 | <tomsmeding> | ah |
2023-02-12 10:45:39 +0100 | <tomsmeding> | oh to windows console specifically |
2023-02-12 10:45:43 +0100 | <tomsmeding> | dunno about that |
2023-02-12 10:45:52 +0100 | <tomsmeding> | Inst: did you compile the C with msvc? |
2023-02-12 10:46:07 +0100 | <[exa]> | that's the bug with C stdlib trying to be nice and flush after every newline? |
2023-02-12 10:46:15 +0100 | <tomsmeding> | python does the same |
2023-02-12 10:46:33 +0100 | <tomsmeding> | and both don't if stdout is not a tty |
2023-02-12 10:48:18 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2023-02-12 10:49:28 +0100 | razetime | (~Thunderbi@117.193.1.13) (Remote host closed the connection) |
2023-02-12 10:50:10 +0100 | ski | . o O ( "What If We Don't Pop the Stack? The Return of 2nd-Class Values" by Anxhelo Xhebraj,Oliver Bračevac,Guannan Wei,Tiark Rompf in 2022 at <https://drops.dagstuhl.de/opus/volltexte/2022/16243/pdf/LIPIcs-ECOOP-2022-15.pdf> ) |
2023-02-12 10:51:00 +0100 | <[exa]> | oh lovely |
2023-02-12 10:51:41 +0100 | <tomsmeding> | ski: I wonder how that compares to c++'s optimisation where it constructs a value in the spot where the parent function expects it |
2023-02-12 10:51:46 +0100 | <tomsmeding> | it has a name, I forget which |
2023-02-12 10:51:50 +0100 | <ski> | (in cases where you want to return a value of a size not known prior to the call, on the stack) |
2023-02-12 10:52:19 +0100 | ardell | (~ardell@user/ardell) |
2023-02-12 10:52:48 +0100 | <ski> | (could also be used to return stack-allocated closures .. cf. <https://en.wikipedia.org/wiki/Region-based_memory_management>) |
2023-02-12 10:52:50 +0100 | <tomsmeding> | ah, copy elision / named return value optimisation |
2023-02-12 10:53:05 +0100 | merijn | (~merijn@145.90.225.11) (Ping timeout: 252 seconds) |
2023-02-12 10:53:27 +0100 | <Inst> | let me go reproduce the results |
2023-02-12 10:53:41 +0100 | <Inst> | done via gcc, i have no idea how i installed it, on windows |
2023-02-12 10:57:14 +0100 | <[exa]> | tomsmeding: destination-passing style or copy/move elision? |
2023-02-12 10:57:33 +0100 | <[exa]> | ski: "storage mode polymorphism" is top |
2023-02-12 10:57:34 +0100 | <tomsmeding> | I guess those are similar? |
2023-02-12 10:57:59 +0100 | <[exa]> | yeah, the copy elision is somewhere in the smudgy middle between full dps and normal values |
2023-02-12 10:58:09 +0100 | <tomsmeding> | yeah |
2023-02-12 10:58:25 +0100 | <tomsmeding> | though does that don't-pop-the-stack paper give you full DPS? |
2023-02-12 10:58:28 +0100 | <[exa]> | "syntactically viable local optimum" |
2023-02-12 10:58:32 +0100 | <tomsmeding> | probably slightly better than copy elision still |
2023-02-12 10:58:56 +0100 | <ski> | the ML Kit <https://elsman.com/mlkit/>,<https://elsman.com/mlkit/pdf/mlkit-4.7.2.pdf>,<https://github.com/melsman/mlkit> (which does region inference) is interesting |
2023-02-12 10:59:20 +0100 | <ski> | [exa] : "is top" ? |
2023-02-12 10:59:54 +0100 | <[exa]> | tomsmeding: as far as I understand it now the paper basically gives you an easy and statically inferrable option to leave some stuff on the stack to be reliably collected by callers, which helps |
2023-02-12 11:00:01 +0100 | <[exa]> | ski: as in "is very good" :D |
2023-02-12 11:00:12 +0100 | <ski> | the Melbourne Mercury compiler does DPS, in some optimizations, to achieve last/tail calls |
2023-02-12 11:00:15 +0100 | <tomsmeding> | [exa]: right, so another mid-way point |
2023-02-12 11:00:35 +0100 | <ski> | [exa] : elaborate on "storage mode polymorphism" ? |
2023-02-12 11:00:41 +0100 | <ski> | (links ?) |
2023-02-12 11:01:39 +0100 | <[exa]> | in that stack-not-popping paper you linked, section 6.2 |
2023-02-12 11:02:08 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 11:02:28 +0100 | <Inst> | okies, reproduced the weird behavior, will try a few more time |
2023-02-12 11:02:34 +0100 | tomsmeding | . o O ( popping-not-your-stack ) |
2023-02-12 11:02:42 +0100 | <ski> | (it was a week or two since i read the aforementioned paper, i think it probably mentioned the term, iirc it suggested three (?) different strategies for how to implement an operation being polymorphic in whether to allocate result on stack or not .. but i was unsure whether you have the paper in mind, or perhaps some other source) |
2023-02-12 11:03:05 +0100 | <Inst> | 5.42 seconds C, 4.82 seconds Python |
2023-02-12 11:03:16 +0100 | <Inst> | iirc, it was Py < Julia < Haskell < C |
2023-02-12 11:03:21 +0100 | <tomsmeding> | Inst: share code? |
2023-02-12 11:03:24 +0100 | <tomsmeding> | wat haskell faster than C |
2023-02-12 11:03:26 +0100 | <Inst> | will in a bit |
2023-02-12 11:03:35 +0100 | <Inst> | yeah i've been encountering that for a bit |
2023-02-12 11:03:41 +0100 | <tomsmeding> | I mean, go haskell, but wat |
2023-02-12 11:03:55 +0100 | <Inst> | it probably has to do with the quality of the libraries that connect to windows console |
2023-02-12 11:04:02 +0100 | <[exa]> | sounds like C crippled by simplicity |
2023-02-12 11:04:04 +0100 | <tomsmeding> | yeah |
2023-02-12 11:04:34 +0100 | <Inst> | but that's sort of a fun point to make, it's completely useless and stupid, but it's a trivial way to reverse the usual language performance benchmarks by something incidental |
2023-02-12 11:04:34 +0100 | <[exa]> | if Julia is faster that basically means there are dirty tricks that reduce the system communication |
2023-02-12 11:04:44 +0100 | <Inst> | and implies that Py is doing so as well |
2023-02-12 11:05:23 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2023-02-12 11:05:31 +0100 | <[exa]> | Inst: you mean IO library benchmark? not really surprising to prove that C doesn't really have one |
2023-02-12 11:07:01 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 11:07:25 +0100 | falafel | (~falafel@2607:fb91:143f:e47f:6cfc:4f5:5346:997f) (Ping timeout: 252 seconds) |
2023-02-12 11:08:18 +0100 | <[exa]> | ski: yeah that paper, I just skimmed over it and it looks really good. I wanted a tool like that for some other projects for a very long time now. |
2023-02-12 11:08:33 +0100 | <[exa]> | great it has materialized now :] |
2023-02-12 11:09:01 +0100 | <Inst> | the C code is bugged, but in C's favor |
2023-02-12 11:09:02 +0100 | <Inst> | https://paste.tomsmeding.com/9hjCRbej |
2023-02-12 11:10:11 +0100 | <tomsmeding> | Inst: why bugged? |
2023-02-12 11:10:33 +0100 | <tomsmeding> | oh more newlines |
2023-02-12 11:10:33 +0100 | <Inst> | i can't be arsed to find the right analogues to putStr |
2023-02-12 11:10:37 +0100 | <tomsmeding> | that's not in C's favour |
2023-02-12 11:10:39 +0100 | <tomsmeding> | printf |
2023-02-12 11:10:43 +0100 | <tomsmeding> | printf("Fizz"); |
2023-02-12 11:10:58 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 268 seconds) |
2023-02-12 11:11:14 +0100 | <tomsmeding> | more newlines is more flushes is more IO calls is less speed |
2023-02-12 11:11:35 +0100 | <Inst> | 10 seconds on this variant |
2023-02-12 11:11:38 +0100 | <int-e> | or fputs(stdout, "Fizz") but a compiler might do that for you |
2023-02-12 11:11:49 +0100 | <tomsmeding> | probably will |
2023-02-12 11:11:51 +0100 | <Inst> | https://paste.tomsmeding.com/RtqhBpiX |
2023-02-12 11:12:00 +0100 | <Inst> | maybe set O? |
2023-02-12 11:12:02 +0100 | <Inst> | let me try that |
2023-02-12 11:12:08 +0100 | <int-e> | (I know that gcc will) |
2023-02-12 11:12:23 +0100 | <Inst> | 10.55 seconds |
2023-02-12 11:12:27 +0100 | <Inst> | under O2 |
2023-02-12 11:12:43 +0100 | <Inst> | so, virtually any language can beat C by simply exploiting the poor C windows IO library |
2023-02-12 11:13:49 +0100 | <int-e> | you still have printf("\n"); |
2023-02-12 11:14:16 +0100 | <int-e> | ah, sorry, python code does that too |
2023-02-12 11:14:37 +0100 | <tomsmeding> | Inst: python takes 0.0527 seconds here on linux in the 'st' terminal, C takes 0.0049 seconds |
2023-02-12 11:14:52 +0100 | <Inst> | sounds about right :) |
2023-02-12 11:14:55 +0100 | <tomsmeding> | sorry poor windows users, stuff's not optimised for windows |
2023-02-12 11:15:10 +0100 | <Inst> | please fix my getChar ;___; |
2023-02-12 11:15:14 +0100 | <tomsmeding> | oh I lie |
2023-02-12 11:15:24 +0100 | <tomsmeding> | 0.17s py, 0.072s C |
2023-02-12 11:15:31 +0100 | <tomsmeding> | was not writing to terminal, which is kind of essential |
2023-02-12 11:16:19 +0100 | <Inst> | https://gitlab.haskell.org/ghc/ghc/-/issues/21047 |
2023-02-12 11:16:45 +0100 | <Inst> | i'm a big fan of bird's book, and while it's not his fault done isn't a thing |
2023-02-12 11:16:53 +0100 | <Inst> | done :: m () |
2023-02-12 11:16:56 +0100 | <Inst> | done = pure () |
2023-02-12 11:17:09 +0100 | <Inst> | you can't implement getLine in terms of getChar as requested |
2023-02-12 11:17:12 +0100 | <Inst> | on windows systems |
2023-02-12 11:17:47 +0100 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
2023-02-12 11:18:04 +0100 | <Inst> | *while it's his fault |
2023-02-12 11:18:58 +0100 | <tomsmeding> | 0.14 for haskell, so C < haskell < py here |
2023-02-12 11:19:04 +0100 | <tomsmeding> | but varies |
2023-02-12 11:21:08 +0100 | <ski> | ((section 3) "Making Mercury programs tail recursive" by Peter Ross,David Overton,Zoltan Somogyi in 1999-09 at <https://www.mercurylang.org/documentation/papers.html#tail_lopstr> (extended abstract),<https://www.mercurylang.org/documentation/papers.html#tail_lopstr_lncs> does DPS (Destination-Passing Style), with LCMC/TCMC (Last/Tail Call Modulo Cons(tructor)), tracking definite aliases in the inst |
2023-02-12 11:21:14 +0100 | <ski> | (instantiation) system) |
2023-02-12 11:22:41 +0100 | <Inst> | so, ummm, you want me to inline the free monad into FIOF? |
2023-02-12 11:22:54 +0100 | <Inst> | https://play-haskell.tomsmeding.com/saved/38Fg7T7s |
2023-02-12 11:23:29 +0100 | <tomsmeding> | Inst: yeah make one datatype, FIO (replace the existing one) that inlines Free and FIOF into one thing |
2023-02-12 11:23:42 +0100 | <tomsmeding> | so that you see that Free is not magic |
2023-02-12 11:23:45 +0100 | <ski> | Inst,tomsmeding : `fputs("Fizz",stdout);' |
2023-02-12 11:25:31 +0100 | <Inst> | roughly looks like this right now |
2023-02-12 11:25:32 +0100 | <Inst> | data FIOF a |
2023-02-12 11:25:32 +0100 | <Inst> | = Put String FIOF |
2023-02-12 11:25:32 +0100 | <Inst> | | Get (String -> FIOF) |
2023-02-12 11:25:32 +0100 | <Inst> | | Sleep Int FIOF |
2023-02-12 11:25:32 +0100 | <Inst> | | Pure a |
2023-02-12 11:25:50 +0100 | <tomsmeding> | ski: funnily regardless of whether I use fputs or printf, the compiled assembly seems to call printf always |
2023-02-12 11:25:54 +0100 | <Inst> | also re console, you can always just use Haskell to wrap C, C++, or something like that |
2023-02-12 11:25:55 +0100 | <tomsmeding> | and runtimes are identical |
2023-02-12 11:26:08 +0100 | <tomsmeding> | Inst: that doesn't kindcheck |
2023-02-12 11:26:11 +0100 | ski | for a moment thought that Inst's "5.42 seconds C, 4.82 seconds Python" was referring to sections in the "don't pop the stack" paper |
2023-02-12 11:26:15 +0100 | <Inst> | that's what Tabby seems to do, and it's what Facebook did with Sigma / Standard Chartered |
2023-02-12 11:26:16 +0100 | <Inst> | ah |
2023-02-12 11:26:35 +0100 | ardell | (~ardell@user/ardell) (Quit: Konversation terminated!) |
2023-02-12 11:26:39 +0100 | <ski> | Inst : needs more parameters |
2023-02-12 11:26:56 +0100 | <ski> | tomsmeding : curious |
2023-02-12 11:26:59 +0100 | <Inst> | yeah, added the a to FIOF, forgot it during refactoring |
2023-02-12 11:28:34 +0100 | <ski> | you could just omit `a', (renaming `Pure' to `End' or `Terminate' or somesuch), if/when you're doing the CPS (as in `Cont IOAction a = (a -> IOAction) -> IOAction') version |
2023-02-12 11:36:31 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 11:41:55 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 11:52:48 +0100 | thongpv | (~thongpv87@123.31.75.7) |
2023-02-12 11:54:44 +0100 | simeon | (~simeon@143.231.7.51.dyn.plus.net) (Ping timeout: 260 seconds) |
2023-02-12 11:54:45 +0100 | thongpv87 | (~thongpv87@123.31.75.7) (Ping timeout: 268 seconds) |
2023-02-12 11:59:23 +0100 | xff0x | (~xff0x@2405:6580:b080:900:161d:e8bd:9253:e61c) (Ping timeout: 246 seconds) |
2023-02-12 12:01:05 +0100 | xff0x | (~xff0x@138.64.81.74) |
2023-02-12 12:01:05 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
2023-02-12 12:02:03 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2023-02-12 12:04:50 +0100 | mc47 | (~mc47@xmonad/TheMC47) |
2023-02-12 12:12:39 +0100 | gurkenglas | (~gurkengla@2.247.242.221) (Ping timeout: 252 seconds) |
2023-02-12 12:12:44 +0100 | notzmv | (~zmv@user/notzmv) |
2023-02-12 12:17:34 +0100 | thongpv | (~thongpv87@123.31.75.7) (Ping timeout: 268 seconds) |
2023-02-12 12:18:03 +0100 | <Inst> | done tomsmeding |
2023-02-12 12:18:05 +0100 | <Inst> | you're great at this |
2023-02-12 12:18:22 +0100 | <tomsmeding> | <3 |
2023-02-12 12:18:30 +0100 | <Inst> | https://play-haskell.tomsmeding.com/saved/bfa763t9 |
2023-02-12 12:18:36 +0100 | <Inst> | you should go set up a template system on playgrounds |
2023-02-12 12:18:54 +0100 | <Inst> | so, say, someone wants to set up an exercise, they can just get a copy of the template, and spawn a new playground based off the template |
2023-02-12 12:18:58 +0100 | <Inst> | unless it's already a feature |
2023-02-12 12:19:01 +0100 | <tomsmeding> | it's not |
2023-02-12 12:19:15 +0100 | <tomsmeding> | https://github.com/tomsmeding/play-haskell/issues/new?assignees=&labels=&template=feature_request.md |
2023-02-12 12:22:07 +0100 | <Inst> | thanks for the Free $ Free Monad $ Tutorial |
2023-02-12 12:22:31 +0100 | beteigeuze | (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
2023-02-12 12:22:33 +0100 | <tomsmeding> | :D |
2023-02-12 12:22:52 +0100 | <ski> | make that `(Free . Free Monad) Tutorial' |
2023-02-12 12:23:07 +0100 | shapr | (~user@net-5-88-238-17.cust.vodafonedsl.it) (Ping timeout: 268 seconds) |
2023-02-12 12:23:14 +0100 | <tomsmeding> | @pl \f -> (f . f Monad) Tutorial |
2023-02-12 12:23:14 +0100 | <lambdabot> | flip (ap (.) ($ Monad)) Tutorial |
2023-02-12 12:23:31 +0100 | <tomsmeding> | @pl \f -> f . f Monad |
2023-02-12 12:23:31 +0100 | <lambdabot> | ap (.) ($ Monad) |
2023-02-12 12:24:00 +0100 | <tomsmeding> | ((.) <*> flip id Monad) Free Tutorial |
2023-02-12 12:24:00 +0100 | <ski> | Inst : brackets in `(Pure a) >>= f = f a' are useless (and ditto for the other defining equations) |
2023-02-12 12:24:23 +0100 | <ski> | .. and in `(cont u) >>= f' |
2023-02-12 12:24:45 +0100 | <ski> | (also `deriving (Functor)' ..) |
2023-02-12 12:25:01 +0100 | <Inst> | done |
2023-02-12 12:25:04 +0100 | <tomsmeding> | I've taken to always putting parentheses around the deriving RHS |
2023-02-12 12:25:06 +0100 | <Inst> | I got lazy |
2023-02-12 12:25:12 +0100 | <Inst> | forgot to factor them out |
2023-02-12 12:25:43 +0100 | <ski> | is the `DerivingStrategies' really necessary ? |
2023-02-12 12:25:50 +0100 | <Inst> | nope, didn't refactor that out either |
2023-02-12 12:26:29 +0100 | <tomsmeding> | ski: ah, I put that in to do 'deriving newtype (Functor, Applicative, Monad)' on newtype FIO a = FIO (Free FIOF a) |
2023-02-12 12:26:49 +0100 | <tomsmeding> | Inst: <3 for issue |
2023-02-12 12:26:56 +0100 | <ski> | `\m -> go m' can be eta-reduced to `m' (alternatively `interpret m = go m' can be "function extensionality"d to `interpret = go') |
2023-02-12 12:27:19 +0100 | <ski> | tomsmeding : yes. doesn't a plain `deriving' work there ? |
2023-02-12 12:27:42 +0100 | <Inst> | i don't do that much type-level programming, in fact, i don't actually get it, outside of building some hacks around stuff |
2023-02-12 12:27:45 +0100 | <ski> | oh, and apparently `go' has some double brackets |
2023-02-12 12:27:50 +0100 | <tomsmeding> | ski: yes |
2023-02-12 12:28:12 +0100 | <Inst> | i think being able to develop in a top-down way with minimal type annotations is a show of the flexibility of Haskell toward some use cases |
2023-02-12 12:28:32 +0100 | <tomsmeding> | but I feel usage of GeneralizedNewtypeDeriving could use explicit signals |
2023-02-12 12:29:07 +0100 | <Inst> | Version 9.2.5 not available |
2023-02-12 12:29:07 +0100 | <ski> | yea, i was thinking maybe it was for being explicit |
2023-02-12 12:29:31 +0100 | <tomsmeding> | Inst: yeah oops I'm messing with the playground |
2023-02-12 12:29:34 +0100 | <ski> | Inst : now for CPS version ? |
2023-02-12 12:29:38 +0100 | <Inst> | sleep! |
2023-02-12 12:29:56 +0100 | <ski> | happy dreaming in CPS ! |
2023-02-12 12:30:00 +0100 | <tomsmeding> | Inst: should work again |
2023-02-12 12:30:26 +0100 | <ski> | (be sure to call `sleep' with a continuation involving your actions for tomorrow) |
2023-02-12 12:38:01 +0100 | <Unicorn_Princess> | should i ever call `cabal upgrade` and the like if i'm managing my haskell install through ghcup? |
2023-02-12 12:38:23 +0100 | <maerwald> | Unicorn_Princess: there's no such thing as 'cabal upgrade' |
2023-02-12 12:38:39 +0100 | <Unicorn_Princess> | or update or uh... anything of that nature |
2023-02-12 12:38:47 +0100 | MQ-17J | (~MQ-17J@104.28.248.166) |
2023-02-12 12:38:50 +0100 | <tomsmeding> | there is 'stack upgrade' though, and that you should _not_ use if you install stack through ghcup |
2023-02-12 12:38:52 +0100 | <maerwald> | 'cabal update' does not update the binary |
2023-02-12 12:39:05 +0100 | <tomsmeding> | Unicorn_Princess: 'cabal update' is a completely different thing, downloads the most recent package list |
2023-02-12 12:39:08 +0100 | <tomsmeding> | that you should run once in a while |
2023-02-12 12:39:36 +0100 | <Unicorn_Princess> | ah, so package list is handled separately. got it, thanks |
2023-02-12 12:45:24 +0100 | <tomsmeding> | is there anything in ~/.cabal/packages that is linux-distribution-specific? I.e. if I copy that directory over to another machine with the same CPU architecture, will that just work? |
2023-02-12 12:47:29 +0100 | MQ-17J | (~MQ-17J@104.28.248.166) (Ping timeout: 252 seconds) |
2023-02-12 12:49:37 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2023-02-12 12:54:18 +0100 | <int-e> | If it's the same ghc too and the same $HOME chances are pretty good that this works. |
2023-02-12 12:54:32 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 12:54:52 +0100 | <tomsmeding> | (of course there is no "another machine" here, it's a chroot with a different linux distro) |
2023-02-12 12:54:53 +0100 | <maerwald> | int-e: .cabal/packages is not the store |
2023-02-12 12:55:00 +0100 | <int-e> | oh |
2023-02-12 12:55:09 +0100 | <tomsmeding> | yeah I'm asking specifically about .cabal/packages |
2023-02-12 12:55:20 +0100 | <maerwald> | I'd be surprised |
2023-02-12 12:55:23 +0100 | <int-e> | sorry, that one can be copied over regardless of the platform |
2023-02-12 12:55:28 +0100 | <maerwald> | yeah |
2023-02-12 12:55:28 +0100 | <tomsmeding> | .cabal/store and .cabal/logs I can redirect, but it seems I can't do that to .cabal/packages and it also seems I don't need to |
2023-02-12 12:55:29 +0100 | <tomsmeding> | cool |
2023-02-12 12:58:55 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
2023-02-12 13:01:28 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-02-12 13:02:51 +0100 | mechap | (~mechap@user/mechap) (Ping timeout: 248 seconds) |
2023-02-12 13:05:08 +0100 | mechap | (~mechap@user/mechap) |
2023-02-12 13:13:29 +0100 | gurkenglas | (~gurkengla@dynamic-002-247-242-221.2.247.pool.telefonica.de) |
2023-02-12 13:15:33 +0100 | beteigeuze | (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Quit: beteigeuze) |
2023-02-12 13:15:58 +0100 | beteigeuze | (~Thunderbi@85.247.81.220) |
2023-02-12 13:16:03 +0100 | beteigeuze | (~Thunderbi@85.247.81.220) (Client Quit) |
2023-02-12 13:26:21 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 252 seconds) |
2023-02-12 13:26:54 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 260 seconds) |
2023-02-12 13:28:27 +0100 | mmhat | (~mmh@p200300f1c730fb3aee086bfffe095315.dip0.t-ipconnect.de) |
2023-02-12 13:28:49 +0100 | mmhat | (~mmh@p200300f1c730fb3aee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
2023-02-12 13:43:13 +0100 | yahb2 | (~yahb2@2a01:4f8:c0c:5c7b::2) (Remote host closed the connection) |
2023-02-12 13:43:25 +0100 | yahb2 | (~yahb2@2a01:4f8:c0c:5c7b::2) |
2023-02-12 13:45:44 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 13:51:21 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 13:51:57 +0100 | majjoha | (~majjoha@80.71.142.8.ipv4.parknet.dk) |
2023-02-12 13:52:10 +0100 | majjoha | (~majjoha@80.71.142.8.ipv4.parknet.dk) (Client Quit) |
2023-02-12 13:52:21 +0100 | simeon | (~simeon@51.7.231.143) |
2023-02-12 13:56:04 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
2023-02-12 13:57:25 +0100 | majjoha | (~majjoha@80.71.142.8.ipv4.parknet.dk) |
2023-02-12 13:58:36 +0100 | majjoha | (~majjoha@80.71.142.8.ipv4.parknet.dk) (Client Quit) |
2023-02-12 13:58:50 +0100 | majjoha | (~majjoha@80.71.142.8.ipv4.parknet.dk) |
2023-02-12 14:01:37 +0100 | CiaoSen | (~Jura@p200300c9570460002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
2023-02-12 14:05:41 +0100 | majjoha | (~majjoha@80.71.142.8.ipv4.parknet.dk) (Quit: Ping timeout (120 seconds)) |
2023-02-12 14:07:59 +0100 | shapr | (~user@host-79-37-239-243.retail.telecomitalia.it) |
2023-02-12 14:10:21 +0100 | simeon | (~simeon@51.7.231.143) (Ping timeout: 252 seconds) |
2023-02-12 14:10:35 +0100 | oldfashionedcow | (~Rahul_San@user/oldfashionedcow) |
2023-02-12 14:14:11 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Quit: No Ping reply in 180 seconds.) |
2023-02-12 14:16:10 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
2023-02-12 14:17:15 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2023-02-12 14:30:09 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 14:30:38 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 14:30:46 +0100 | __monty__ | (~toonn@user/toonn) |
2023-02-12 14:31:44 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 14:31:52 +0100 | lackita | (~lackita@73.114.250.252) (Read error: Connection reset by peer) |
2023-02-12 14:32:04 +0100 | lackita | (~lackita@2600:1000:b033:adf2:42c8:c73b:9ad5:1286) |
2023-02-12 14:32:23 +0100 | lackita | (~lackita@2600:1000:b033:adf2:42c8:c73b:9ad5:1286) (Read error: Connection reset by peer) |
2023-02-12 14:32:34 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 14:33:22 +0100 | thongpv | (~thongpv87@123.31.75.7) |
2023-02-12 14:35:51 +0100 | thongpv87 | (~thongpv87@2402:9d80:3ac:fe89:f117:a1ed:9f3d:f0e3) |
2023-02-12 14:35:59 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
2023-02-12 14:38:08 +0100 | thongpv | (~thongpv87@123.31.75.7) (Ping timeout: 248 seconds) |
2023-02-12 14:38:39 +0100 | juri_ | (~juri@84-19-175-179.pool.ovpn.com) (Ping timeout: 260 seconds) |
2023-02-12 14:39:10 +0100 | juri_ | (~juri@84.19.175.179) |
2023-02-12 14:41:09 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 14:41:18 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 14:41:19 +0100 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
2023-02-12 14:45:27 +0100 | retrosenator | (~retrosena@174.211.112.224) |
2023-02-12 14:46:19 +0100 | lackita | (~lackita@73.114.250.252) (Read error: Connection reset by peer) |
2023-02-12 14:46:44 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 14:47:29 +0100 | Axman6 | (~Axman6@user/axman6) (Remote host closed the connection) |
2023-02-12 14:47:46 +0100 | Axman6 | (~Axman6@user/axman6) |
2023-02-12 14:49:35 +0100 | juri_ | (~juri@84.19.175.179) (Ping timeout: 252 seconds) |
2023-02-12 14:50:52 +0100 | juri_ | (~juri@84.19.175.179) |
2023-02-12 14:52:04 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 260 seconds) |
2023-02-12 14:57:19 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 260 seconds) |
2023-02-12 14:57:42 +0100 | simeon | (~simeon@37.205.58.148) |
2023-02-12 14:57:45 +0100 | simeon | (~simeon@37.205.58.148) (Remote host closed the connection) |
2023-02-12 14:58:12 +0100 | lackita | (~lackita@2600:1000:b033:adf2:42c8:c73b:9ad5:1286) |
2023-02-12 14:59:50 +0100 | agevelt[m] | (~ageveltmo@2001:470:69fc:105::3:16db) |
2023-02-12 14:59:56 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 15:00:09 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) |
2023-02-12 15:03:23 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Ping timeout: 248 seconds) |
2023-02-12 15:08:23 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 268 seconds) |
2023-02-12 15:18:06 +0100 | trev | (~trev@user/trev) |
2023-02-12 15:21:43 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-02-12 15:26:36 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
2023-02-12 15:27:29 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-02-12 15:28:14 +0100 | o-90 | (~o-90@gateway/tor-sasl/o-90) |
2023-02-12 15:29:04 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-02-12 15:29:58 +0100 | o-90 | (~o-90@gateway/tor-sasl/o-90) (Remote host closed the connection) |
2023-02-12 15:31:49 +0100 | <cheater> | what's the best way to use integers on the type level? |
2023-02-12 15:32:02 +0100 | <cheater> | i have to specify large numbers, like 1337 and 420 |
2023-02-12 15:32:15 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 15:33:53 +0100 | <retrosenator> | what exactly does the program do if you need only those two particular numbers? |
2023-02-12 15:34:04 +0100 | dsrt^ | (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) |
2023-02-12 15:34:36 +0100 | <cheater> | it needs to send 1337 messages |
2023-02-12 15:34:41 +0100 | <cheater> | and then disconnect |
2023-02-12 15:34:51 +0100 | <cheater> | (it's actually a different number. but 1337 is funnier) |
2023-02-12 15:36:30 +0100 | <retrosenator> | 420? |
2023-02-12 15:36:35 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 15:36:38 +0100 | notzmv | (~zmv@user/notzmv) |
2023-02-12 15:37:00 +0100 | <retrosenator> | you just inspired me... |
2023-02-12 15:37:38 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d14c:efc7:12bb:4678) |
2023-02-12 15:39:46 +0100 | <tomsmeding> | cheater: https://hackage.haskell.org/package/base-4.16.0.0/docs/GHC-TypeNats.html in combination with https://hackage.haskell.org/package/ghc-typelits-natnormalise and perhaps https://hackage.haskell.org/package/ghc-typelits-knownnat works acceptably |
2023-02-12 15:40:10 +0100 | <cheater> | thanks, i'll read through that tomsmeding |
2023-02-12 15:42:00 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d14c:efc7:12bb:4678) (Ping timeout: 260 seconds) |
2023-02-12 15:48:35 +0100 | Sinbad | (~Sinbad@user/sinbad) |
2023-02-12 15:52:20 +0100 | Sinbad | (~Sinbad@user/sinbad) (Quit: WeeChat 3.8) |
2023-02-12 16:00:21 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) () |
2023-02-12 16:00:40 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) |
2023-02-12 16:01:00 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 16:05:36 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
2023-02-12 16:06:58 +0100 | gurkenglas | (~gurkengla@dynamic-002-247-242-221.2.247.pool.telefonica.de) (Ping timeout: 268 seconds) |
2023-02-12 16:07:42 +0100 | merijn | (~merijn@145.90.225.11) |
2023-02-12 16:09:38 +0100 | harveypwca | (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
2023-02-12 16:11:15 +0100 | jakalx | (~jakalx@base.jakalx.net) () |
2023-02-12 16:13:33 +0100 | merijn | (~merijn@145.90.225.11) (Ping timeout: 252 seconds) |
2023-02-12 16:20:55 +0100 | ubert | (~Thunderbi@p200300ecdf130185faf60c5e727d766b.dip0.t-ipconnect.de) |
2023-02-12 16:27:30 +0100 | <shapr> | xerox: are you in Rome? |
2023-02-12 16:27:37 +0100 | son0p | (~ff@190.158.28.118) |
2023-02-12 16:28:13 +0100 | patrl | (~patrl@user/patrl) |
2023-02-12 16:31:57 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) () |
2023-02-12 16:32:41 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) |
2023-02-12 16:32:43 +0100 | patrl | (~patrl@user/patrl) (Client Quit) |
2023-02-12 16:36:58 +0100 | gnalzo | (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-02-12 16:38:06 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:cd1a:e6be:bfd3:350) |
2023-02-12 16:41:06 +0100 | <Unicorn_Princess> | hrm... is hls-based completion janky, or is it just me/my emacs setup? |
2023-02-12 16:42:26 +0100 | <Unicorn_Princess> | it'll suggest stuff from all sorts of libraries, but not from the file i'm working in |
2023-02-12 16:42:38 +0100 | vjoki | (~vjoki@2a00:d880:3:1::fea1:9ae) (Quit: ...) |
2023-02-12 16:42:41 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:cd1a:e6be:bfd3:350) (Ping timeout: 255 seconds) |
2023-02-12 16:42:52 +0100 | vjoki | (~vjoki@2a00:d880:3:1::fea1:9ae) |
2023-02-12 16:43:09 +0100 | <geekosaur> | suspect it's you; works fine for me in vs code. although hls sometimes becomes confused and needs to be restarted |
2023-02-12 16:43:11 +0100 | <shapr> | If you haven't yet done a "cabal build" on the project, HLS won't know about the local definitions. could that be it? |
2023-02-12 16:44:20 +0100 | <Unicorn_Princess> | shapr, alas that's not it. but it may be stale, i'll try a restart |
2023-02-12 16:45:09 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
2023-02-12 16:45:21 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
2023-02-12 16:45:25 +0100 | <Unicorn_Princess> | seems to have helped. let's hope it sticks! |
2023-02-12 16:45:26 +0100 | <shapr> | if something seems entirely broken, you can delete ~/.cache/ghcide and ~/.cache/hie-bios but that's is rare |
2023-02-12 16:45:35 +0100 | <shapr> | that's rarely the issue |
2023-02-12 16:47:36 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-02-12 16:48:01 +0100 | juri_ | (~juri@84.19.175.179) (Ping timeout: 252 seconds) |
2023-02-12 16:49:07 +0100 | juri_ | (~juri@79.140.122.38) |
2023-02-12 16:50:35 +0100 | Sauvin | (~sauvin@user/Sauvin) (Read error: Connection reset by peer) |
2023-02-12 16:54:24 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-02-12 16:55:36 +0100 | rettahcay | (~kaushikv@c-24-20-37-193.hsd1.or.comcast.net) |
2023-02-12 17:00:14 +0100 | ski | . o O ( `iterate :: (a -> a) -> a -> (Nat -> a); iterate (\(f n) -> f (Succ n)) (f Zero) = f' ) |
2023-02-12 17:00:52 +0100 | ski | . o O ( `many,many :: Alternative i => i a -> i [a]; (many x,some x) = (many_x,some_x) where many_x = some_x <|> pure []; some_x = liftA2 (:) x many_x' ) |
2023-02-12 17:01:04 +0100 | <ski> | (er, s/many,many/many,some/) |
2023-02-12 17:01:54 +0100 | Sauvin | (~sauvin@user/Sauvin) |
2023-02-12 17:02:14 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2023-02-12 17:04:23 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) () |
2023-02-12 17:05:10 +0100 | jero98772 | (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) |
2023-02-12 17:05:16 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) |
2023-02-12 17:09:13 +0100 | waleee | (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
2023-02-12 17:11:00 +0100 | rettahcay | (~kaushikv@c-24-20-37-193.hsd1.or.comcast.net) () |
2023-02-12 17:13:41 +0100 | npmania | (~Thunderbi@45.8.223.218) |
2023-02-12 17:14:33 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
2023-02-12 17:18:47 +0100 | razetime | (~Thunderbi@117.193.1.13) |
2023-02-12 17:22:15 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
2023-02-12 17:22:16 +0100 | wroathe | (~wroathe@207.153.38.140) |
2023-02-12 17:22:16 +0100 | wroathe | (~wroathe@207.153.38.140) (Changing host) |
2023-02-12 17:22:16 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-02-12 17:22:51 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2023-02-12 17:24:31 +0100 | <tomsmeding> | ski: what language is that 'iterate' written in :p |
2023-02-12 17:28:36 +0100 | <ski> | tomsmeding : pseudo-Haskell :b |
2023-02-12 17:28:56 +0100 | <ski> | (more specifically, some pattern extensions i'm pondering) |
2023-02-12 17:29:29 +0100 | <tomsmeding> | how does pattern matching on function application work |
2023-02-12 17:29:34 +0100 | <tomsmeding> | s/does/can/ |
2023-02-12 17:29:56 +0100 | <ski> | the same way `f x = x + 1' works, with function application to the left of the `=' |
2023-02-12 17:30:07 +0100 | <ski> | (FSVO "same") |
2023-02-12 17:30:19 +0100 | <tomsmeding> | that works for the (many x, some x) case, ish |
2023-02-12 17:30:45 +0100 | <ski> | that's a multiple-entry piece of code |
2023-02-12 17:31:26 +0100 | <ski> | (but perhaps you should also ask about the lambda abstraction ..) |
2023-02-12 17:31:52 +0100 | <tomsmeding> | oh so for that iterate, the compiler is supposed to do induction over Nat or something, and recognise that there is exactly one f that can be synthesised from the arguments to follow that specification, and then return that? |
2023-02-12 17:31:54 +0100 | <tomsmeding> | that sounds like madness |
2023-02-12 17:32:38 +0100 | gurkenglas | (~gurkengla@dynamic-046-114-178-040.46.114.pool.telefonica.de) |
2023-02-12 17:32:41 +0100 | <ski> | that `iterate' definition is equivalent to |
2023-02-12 17:32:45 +0100 | <ski> | iterate g = f |
2023-02-12 17:32:47 +0100 | <ski> | where |
2023-02-12 17:33:14 +0100 | <ski> | f Zero = x |
2023-02-12 17:33:24 +0100 | <ski> | f (Succ n) = g (f n) |
2023-02-12 17:33:32 +0100 | <ski> | er, s/iterate g/iterate g x/ |
2023-02-12 17:34:21 +0100 | ub | (~Thunderbi@p200300ecdf1301856cd886509d6d0bd1.dip0.t-ipconnect.de) |
2023-02-12 17:34:31 +0100 | _xor | (~xor@74.215.182.83) (Quit: brb) |
2023-02-12 17:34:32 +0100 | <ski> | so, clearly, in either definition of `iterate', `f' is defined on both cases `Zero' and `Succ n', recursively defined for the latter one |
2023-02-12 17:35:10 +0100 | <tomsmeding> | so that f (Succ n) and that (f Zero) need to be patterns then, at the very least |
2023-02-12 17:35:12 +0100 | <ski> | the only thing that feels a bit icky would be if there were overlapping cases |
2023-02-12 17:35:29 +0100 | <ski> | `Zero' and `Succ n' are patterns, yes |
2023-02-12 17:35:40 +0100 | <tomsmeding> | right |
2023-02-12 17:35:44 +0100 | <ski> | is `f x' in `f x = x + 1' a pattern, in your mind ? |
2023-02-12 17:35:50 +0100 | <tomsmeding> | no you're right |
2023-02-12 17:36:09 +0100 | <tomsmeding> | but e.g. `iterate (\(f n) -> f (Succ n) + 1) (f Zero) = ...' cannot be valid |
2023-02-12 17:36:22 +0100 | <ski> | why not ? ;D |
2023-02-12 17:36:29 +0100 | <tomsmeding> | wtf does it mean |
2023-02-12 17:36:35 +0100 | <tomsmeding> | f Zero = x ; f (Succ n) + 1 = g (f n) |
2023-02-12 17:36:36 +0100 | <tomsmeding> | ? |
2023-02-12 17:36:59 +0100 | <tomsmeding> | and don't n+k patterns me |
2023-02-12 17:37:08 +0100 | <ski> | yes (minus the ` + 1') |
2023-02-12 17:37:11 +0100 | <tomsmeding> | or I guess this is precisely a generalisation of n+k patterns |
2023-02-12 17:37:26 +0100 | <tomsmeding> | ski: the '+ 1' was precisely my point |
2023-02-12 17:37:31 +0100 | <ski> | (the `f x = x + 1' was a separate, unrelated, example) |
2023-02-12 17:37:40 +0100 | <tomsmeding> | yeah I know |
2023-02-12 17:38:18 +0100 | <ski> | so `f (Succ n) + 1' never enters my picture |
2023-02-12 17:39:11 +0100 | <tomsmeding> | because the "body" (after possible lambda abstractions) of each ski-extended argument must be left-hand sides (better term?), and 'f (Succ n) + 1' is not a LHS? |
2023-02-12 17:39:19 +0100 | <tomsmeding> | well it is for (+), I guess |
2023-02-12 17:39:20 +0100 | <ski> | `f (Succ n)' is not an expression, so `f (Succ n) + 1' is not valid (unless you go `NPlusKPatterns', yes) |
2023-02-12 17:39:21 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
2023-02-12 17:39:43 +0100 | <ski> | (this is why i asked about `f x = x + 1', what you'd call `f x' there) |
2023-02-12 17:39:51 +0100 | <tomsmeding> | did you mean to say "`f (Succ n)' is not a pattern"? |
2023-02-12 17:39:57 +0100 | <ski> | no |
2023-02-12 17:39:58 +0100 | <tomsmeding> | ski: I'd call that a left-hand side |
2023-02-12 17:40:05 +0100 | <ski> | fair enough |
2023-02-12 17:40:16 +0100 | <ski> | `f (Succ n)' is a "left-hand side" |
2023-02-12 17:40:22 +0100 | <tomsmeding> | right |
2023-02-12 17:40:30 +0100 | <ski> | (i'd probably say "definiendum") |
2023-02-12 17:40:44 +0100 | <tomsmeding> | LHS is shorter :) |
2023-02-12 17:41:04 +0100 | <ski> | in `iterate (\(f n) -> f (Succ n)) (f Zero) = f', `f n' is an expression, and `f (Succ n)' is a definiendum / left-hand side |
2023-02-12 17:41:07 +0100 | <tomsmeding> | is `f (Succ n) + 1' a LHS? |
2023-02-12 17:41:11 +0100 | <ski> | no |
2023-02-12 17:41:25 +0100 | <tomsmeding> | with your extended patterns it might be |
2023-02-12 17:41:26 +0100 | <ski> | well, it is, if you're defining `(+)' |
2023-02-12 17:41:30 +0100 | <tomsmeding> | right |
2023-02-12 17:41:46 +0100 | <ski> | (but disregarding that) |
2023-02-12 17:41:54 +0100 | <tomsmeding> | so if you write `iterate (\(f n) -> f (Succ n) + 1) (f Zero) = ...', you're defining both f and plus |
2023-02-12 17:41:57 +0100 | <tomsmeding> | and neither fully |
2023-02-12 17:42:08 +0100 | <tomsmeding> | and in the definition of (+) you have another definition of f |
2023-02-12 17:42:23 +0100 | <ski> | tomsmeding : you're actually defining two separate variables `f', in that case |
2023-02-12 17:42:26 +0100 | <tomsmeding> | yes |
2023-02-12 17:42:36 +0100 | <tomsmeding> | to make things more intelligible :) |
2023-02-12 17:42:40 +0100 | juri_ | (~juri@79.140.122.38) (Read error: Connection reset by peer) |
2023-02-12 17:42:56 +0100 | <tomsmeding> | this is confusing |
2023-02-12 17:43:08 +0100 | <ski> | it's fun :) |
2023-02-12 17:44:00 +0100 | <ski> | if `<expr>' is an expression, and `<pat>' is a pattern, then `\<expr> -> <pat>' is a pattern, that when matched with a function will apply that function on `<expr>', and match the result with `<pat>' |
2023-02-12 17:44:12 +0100 | <tomsmeding> | unrelated question, can I initialise some IORef once without needing to pass it around all the time, without using unsafePerformIO? Assuming I'll need it in IO only, not in pure code |
2023-02-12 17:44:41 +0100 | <ski> | (iow, the pattern `\<expr> -> <pat>' can be explained in terms of view patterns, to be equivalent to `($ <expr>) -> <pat>') |
2023-02-12 17:44:59 +0100 | gurkenglas | (~gurkengla@dynamic-046-114-178-040.46.114.pool.telefonica.de) (Ping timeout: 248 seconds) |
2023-02-12 17:45:49 +0100 | <ski> | you'll probably need at least one `IORef', say to register other `IORef's under some kind of identifiers ? |
2023-02-12 17:45:53 +0100 | <tomsmeding> | but now any variables in <pat> that are also defined in other patterns, get put together in "definition blocks"? how are those called |
2023-02-12 17:46:29 +0100 | <tomsmeding> | ski: right, but that first IORef I need to either pass around or create using unsafePerformIO, right? |
2023-02-12 17:47:23 +0100 | <mauke> | or implicit parameters or passed through the type checker |
2023-02-12 17:47:25 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:cd1a:e6be:bfd3:350) |
2023-02-12 17:47:39 +0100 | <xerox> | shapr: nope, 400km north! |
2023-02-12 17:47:56 +0100 | <ski> | @wiki Top level mutable state |
2023-02-12 17:47:56 +0100 | <lambdabot> | https://wiki.haskell.org/Top_level_mutable_state |
2023-02-12 17:47:59 +0100 | <ski> | @wiki Global keys |
2023-02-12 17:47:59 +0100 | <lambdabot> | https://wiki.haskell.org/Global_keys |
2023-02-12 17:48:21 +0100 | juri_ | (~juri@84-19-175-179.pool.ovpn.com) |
2023-02-12 17:48:36 +0100 | <ski> | tomsmeding : i believe so |
2023-02-12 17:49:30 +0100 | <ski> | @hackage reflection |
2023-02-12 17:49:30 +0100 | <lambdabot> | https://hackage.haskell.org/package/reflection |
2023-02-12 17:50:09 +0100 | <ski> | (cue mauke) |
2023-02-12 17:51:04 +0100 | <tomsmeding> | ski: is reflection relevant to my question? I hope not! |
2023-02-12 17:51:34 +0100 | <mauke> | reflection is the "pass values through the type checker" option |
2023-02-12 17:52:05 +0100 | <tomsmeding> | ah right, but the initialisation could be an empty IORef for all I care |
2023-02-12 17:52:09 +0100 | <tomsmeding> | as long as there is one |
2023-02-12 17:52:23 +0100 | <mauke> | after all, why shouldn't we use the type system as a message bus? |
2023-02-12 17:52:27 +0100 | <tomsmeding> | :D |
2023-02-12 17:55:31 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 17:56:13 +0100 | <tomsmeding> | I like the mkOnceIO thing from proposal 4 |
2023-02-12 17:57:14 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:cd1a:e6be:bfd3:350) (Remote host closed the connection) |
2023-02-12 17:57:27 +0100 | <tomsmeding> | oh actually I don't because it still requires -fno-cse in client code |
2023-02-12 17:57:38 +0100 | jonathanx | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
2023-02-12 17:59:53 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 18:03:40 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:cd1a:e6be:bfd3:350) |
2023-02-12 18:03:42 +0100 | <ski> | tomsmeding : yes, next step is to add `<def>' as an alternative of `<pat>', `<pat> ::= ... | \ <expr> -> <pat> | <def>', with `<def> ::= <var> | <def> <pat> | <con> <def> .. <def> | \ <expr> -> <def> | <expr> -> <def> | ...' |
2023-02-12 18:04:06 +0100 | jao | (~jao@92.233.85.247) |
2023-02-12 18:05:56 +0100 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) |
2023-02-12 18:06:02 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
2023-02-12 18:06:53 +0100 | <ski> | (i've a bunch more additional alternatives i'm pondering, hidden behind the `...'s above) |
2023-02-12 18:06:53 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2023-02-12 18:07:29 +0100 | boxscape_ | (~boxscape_@81.191.27.107) |
2023-02-12 18:07:36 +0100 | <boxscape_> | % {} |
2023-02-12 18:07:36 +0100 | <yahb2> | <no output> |
2023-02-12 18:07:40 +0100 | <boxscape_> | how is this not a parse error |
2023-02-12 18:08:05 +0100 | <ski> | tomsmeding : by "definition blocks", do you mean (effectively) a set of defining equations (or definition/binding sites) that together make up a whole definition/binding ? |
2023-02-12 18:08:16 +0100 | <tomsmeding> | ski: that's precisely what I meant |
2023-02-12 18:08:19 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 252 seconds) |
2023-02-12 18:08:20 +0100 | <tomsmeding> | probably wrong word |
2023-02-12 18:08:21 +0100 | <boxscape_> | Oh I guess it's like how modules can be indented or in {} |
2023-02-12 18:08:32 +0100 | <tomsmeding> | % { x = 1 } |
2023-02-12 18:08:32 +0100 | <yahb2> | <no output> |
2023-02-12 18:08:39 +0100 | hpc | (~juzz@ip98-169-35-163.dc.dc.cox.net) (Ping timeout: 260 seconds) |
2023-02-12 18:08:42 +0100 | <boxscape_> | % x |
2023-02-12 18:08:42 +0100 | <yahb2> | 1 |
2023-02-12 18:09:11 +0100 | <tomsmeding> | ski: wild stuff |
2023-02-12 18:09:18 +0100 | <tomsmeding> | I'm not sure it will increase readability of code |
2023-02-12 18:09:46 +0100 | <tomsmeding> | but it's very interesting that one can give this weird "inverted" code a well-defined semantics without program synthesis |
2023-02-12 18:10:07 +0100 | hpc | (~juzz@ip98-169-35-163.dc.dc.cox.net) |
2023-02-12 18:10:33 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) |
2023-02-12 18:13:06 +0100 | <ski> | tomsmeding : hmm .. a "declaration group" is somewhat near, but not quite the same thing |
2023-02-12 18:13:46 +0100 | <ski> | "A declaration group is a minimal set of mutually dependent bindings. Hindley-Milner type inference is applied to each declaration group in dependency order. The order of declarations in where/let constructs is irrelevant" <https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-880004.5> |
2023-02-12 18:14:24 +0100 | thongpv87 | (~thongpv87@2402:9d80:3ac:fe89:f117:a1ed:9f3d:f0e3) (Read error: Connection reset by peer) |
2023-02-12 18:15:19 +0100 | <ski> | tomsmeding : some of my examples, that i'm playing around with (to explore the design space), i'm having trouble understanding, myself ;p |
2023-02-12 18:15:56 +0100 | <tomsmeding> | :p |
2023-02-12 18:16:02 +0100 | <ski> | (the two i gave above, are not among those. those two are fairly straight-forward) |
2023-02-12 18:20:00 +0100 | <ski> | i'm also thinking about "message-dispatching" syntax / "copatterns" |
2023-02-12 18:20:08 +0100 | <ski> | cf. "Copatterns: Programming Infinite Structures by Observations" by Andreas Abel,Brigitte Pientka,David Thibodeau,Anton Setzer in 2013 at <https://www.cse.chalmers.se/~abela/popl13.pdf> |
2023-02-12 18:21:08 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 18:21:24 +0100 | <ski> | and "Subtyping and Inheritance for Inductive Types" in 1997 at <https://www.cs.ru.nl/E.Poll/papers/durham97.pdf>,"Subtyping and Inheritance for Categorical Datatypes" in 1997 at <https://www.cs.ru.nl/E.Poll/papers/kyoto97.pdf>, both by Erik Poll |
2023-02-12 18:22:12 +0100 | rlj | (~rlj@194-218-34-180.customer.telia.com) |
2023-02-12 18:25:37 +0100 | ub1 | (~Thunderbi@84.140.142.240) |
2023-02-12 18:25:47 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 246 seconds) |
2023-02-12 18:26:03 +0100 | ub | (~Thunderbi@p200300ecdf1301856cd886509d6d0bd1.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
2023-02-12 18:27:53 +0100 | ub1 | ub |
2023-02-12 18:28:25 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-02-12 18:30:03 +0100 | razetime | (~Thunderbi@117.193.1.13) (Remote host closed the connection) |
2023-02-12 18:40:10 +0100 | <cheater> | is that the guy responsible for scala |
2023-02-12 18:43:59 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 264 seconds) |
2023-02-12 18:45:40 +0100 | wroathe | (~wroathe@50.205.197.50) |
2023-02-12 18:45:40 +0100 | wroathe | (~wroathe@50.205.197.50) (Changing host) |
2023-02-12 18:45:40 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-02-12 18:47:18 +0100 | shapr | (~user@host-79-37-239-243.retail.telecomitalia.it) (Ping timeout: 268 seconds) |
2023-02-12 18:52:46 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 18:52:53 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2023-02-12 18:53:31 +0100 | <eldritchcookie[m> | i read about backpack and love the idea however what happens if the module i am importing defines the correct functions but with different names? the problem becomes even worse if this happens with classes |
2023-02-12 18:53:38 +0100 | <ski> | .. as well as "absurd" patterns (cf. <https://agda.readthedocs.io/en/v2.6.3/language/function-definitions.html#absurd-patterns>,<http://docs.idris-lang.org/en/latest/reference/syntax-reference.html?highlight=impossible#grammar-…>,<https://stackoverflow.com/questions/32947534/impossible-patterns-in-idris>), |
2023-02-12 18:53:52 +0100 | <ski> | or- / disjunctive patterns (cf. <https://smlfamily.github.io/successor-ml/OldSuccessorMLWiki/Disjunctive_patterns.html>,<https://www.smlnj.org/doc/features.html>,<https://v2.ocaml.org/manual/patterns.html#sss:pat-or>,<https://rosettacode.org/wiki/Algebraic_data_types#OCaml>), and-patterns (generalized `<pat> @ <pat>') (and expression variants of these); |
2023-02-12 18:54:11 +0100 | <ski> | `let'-`in' patterns, `case'-`of' (and `if'-`then'-`else') patterns (and declarations) |
2023-02-12 18:54:32 +0100 | <ski> | (oh, and definiendum versions of those patterns) |
2023-02-12 18:56:24 +0100 | <ddellacosta> | Is there some standard way to handle 3rd-party library data types when implementing ToJSON/FromJSON with Aeson? I'm struggling to write instances for a custom data type where one of the fields is a CronSchedule (https://hackage.haskell.org/package/cron-0.7.0/docs/System-Cron-Types.html). Even though CronSchedule derives Generic, genericToEncoding that doesn't seem to be sufficient for ToJSON, and |
2023-02-12 18:56:26 +0100 | <ddellacosta> | it seems like I'm going to have to implement orphan instances for all of the CronSchedule field types as well, which smells. I feel like I'm missing something obvious. |
2023-02-12 18:56:54 +0100 | <geekosaur> | eldritchcookie[m, I believe a module signature allows you to do that mapping? |
2023-02-12 18:57:27 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 18:58:21 +0100 | notzmv | (~zmv@user/notzmv) |
2023-02-12 18:58:43 +0100 | <geekosaur> | https://github.com/danidiaz/really-small-backpack-example |
2023-02-12 19:01:15 +0100 | Sgeo | (~Sgeo@user/sgeo) |
2023-02-12 19:01:46 +0100 | gurkenglas | (~gurkengla@dynamic-046-114-178-040.46.114.pool.telefonica.de) |
2023-02-12 19:01:50 +0100 | npmania1 | (~Thunderbi@45.8.223.203) |
2023-02-12 19:03:23 +0100 | npmania | (~Thunderbi@45.8.223.218) (Ping timeout: 252 seconds) |
2023-02-12 19:03:23 +0100 | npmania1 | npmania |
2023-02-12 19:03:43 +0100 | <ski> | ddellacosta : i don't think backpack has any support for renaming exported identifiers in a module or signature .. (and unfortunately there's no rename-on-export nor rename-on-import (of identifiers exported from the module), with plain Haskell modules, either) |
2023-02-12 19:03:49 +0100 | <ski> | er .. |
2023-02-12 19:03:58 +0100 | <ski> | eldritchcookie[m : that ^ was intended for you |
2023-02-12 19:04:06 +0100 | <ddellacosta> | whew lol |
2023-02-12 19:07:14 +0100 | <ski> | (i know several Scheme module systems support both renaming of identifiers on import, and on export. both can be useful. it would also be interesting/nice if one could restrict the type signature, while exporting (e.g. when reexporting from another module) (or while importing, i suppose) .. somewhat relatedly, it would be nice if one could generalize a signature in a subclass) |
2023-02-12 19:12:16 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 19:14:56 +0100 | econo | (uid147250@user/econo) |
2023-02-12 19:15:03 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 268 seconds) |
2023-02-12 19:16:28 +0100 | rlj | (~rlj@194-218-34-180.customer.telia.com) (Quit: Client closed) |
2023-02-12 19:16:31 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 19:17:06 +0100 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
2023-02-12 19:17:34 +0100 | _leo___ | emmanuelux |
2023-02-12 19:18:16 +0100 | boxscape_ | (~boxscape_@81.191.27.107) (Quit: Connection closed) |
2023-02-12 19:22:49 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 19:28:23 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 264 seconds) |
2023-02-12 19:37:53 +0100 | <eldritchcookie[m> | if i define a new class lets say... (full message at <https://libera.ems.host/_matrix/media/v3/download/libera.chat/0e730cee9520066ea8482ae08f846e99d231…>) |
2023-02-12 19:38:01 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 19:38:10 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
2023-02-12 19:38:27 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 19:39:52 +0100 | lackita | (~lackita@2600:1000:b033:adf2:42c8:c73b:9ad5:1286) (Read error: Connection reset by peer) |
2023-02-12 19:40:04 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 19:40:37 +0100 | <geekosaur> | no. The Functor precondition on the instance is checked at use sites |
2023-02-12 19:40:44 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
2023-02-12 19:40:53 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 19:41:00 +0100 | <geekosaur> | also you can't have other instances of that class |
2023-02-12 19:41:14 +0100 | <geekosaur> | (wellm you can., but they'll overlap and therefore won't be reliable) |
2023-02-12 19:42:39 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
2023-02-12 19:44:15 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 248 seconds) |
2023-02-12 19:44:43 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 19:45:11 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 252 seconds) |
2023-02-12 19:45:20 +0100 | rlj | (~rlj@194-218-34-180.customer.telia.com) |
2023-02-12 19:45:55 +0100 | <eldritchcookie[m> | sad |
2023-02-12 19:46:28 +0100 | <rlj> | ski: please see privmsg |
2023-02-12 19:49:53 +0100 | jao | (~jao@92.233.85.247) (Ping timeout: 252 seconds) |
2023-02-12 19:50:29 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 246 seconds) |
2023-02-12 19:50:54 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 19:51:33 +0100 | <wroathe> | geekosaur: FYI try as I might I couldn't figure it out last night, but just now I had the idea to roll back to GHC 9.2.5 instead of the latest, and with that everything seems to be working again for this multi-component project |
2023-02-12 19:51:52 +0100 | <wroathe> | So something appears to be a bit wonky with HIE / HLS / GHC 9.4 |
2023-02-12 19:52:54 +0100 | <geekosaur> | wonder if that's related to multiple home modules… |
2023-02-12 19:53:06 +0100 | <geekosaur> | probably need to ask in #haskell-language-server |
2023-02-12 19:55:05 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 19:55:32 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 19:56:31 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 248 seconds) |
2023-02-12 19:59:07 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2023-02-12 20:00:04 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Max SendQ exceeded) |
2023-02-12 20:00:35 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2023-02-12 20:00:54 +0100 | cheater | (~Username@user/cheater) |
2023-02-12 20:06:27 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds) |
2023-02-12 20:08:25 +0100 | falafel | (~falafel@2607:fb91:143f:e47f:3f5:ed1d:a924:9b13) |
2023-02-12 20:08:35 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 20:08:58 +0100 | aljer | (~j@user/aljer) |
2023-02-12 20:09:15 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 20:14:31 +0100 | kaction | (~kaction@173.66.188.18) |
2023-02-12 20:18:51 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 20:20:50 +0100 | <aljer> | Does anyone here develop on Apple silicon? If so, do you have a preferred method of installing cabal or stack (using nix, rosetta, etc)? |
2023-02-12 20:21:20 +0100 | trev | (~trev@user/trev) (Remote host closed the connection) |
2023-02-12 20:22:23 +0100 | wroathe | (~wroathe@207.153.38.140) |
2023-02-12 20:22:23 +0100 | wroathe | (~wroathe@207.153.38.140) (Changing host) |
2023-02-12 20:22:23 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-02-12 20:22:27 +0100 | <dsal> | I use nix |
2023-02-12 20:22:31 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 20:23:07 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 20:24:21 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 20:24:59 +0100 | falafel | (~falafel@2607:fb91:143f:e47f:3f5:ed1d:a924:9b13) (Quit: Leaving) |
2023-02-12 20:25:21 +0100 | falafel | (~falafel@2607:fb91:143f:e47f:3f5:ed1d:a924:9b13) |
2023-02-12 20:26:01 +0100 | <sm> | ghcup. Before that, brew |
2023-02-12 20:26:23 +0100 | <aljer> | dsal: Thanks, that's what I'm leaning toward |
2023-02-12 20:26:26 +0100 | <sm> | no need for rosetta |
2023-02-12 20:27:27 +0100 | <aljer> | sm: I was trying to set up with ghcup but was getting a segfault with cabal, and another issue with stack (I believe it's due to a subdependency being installed with homebrew) |
2023-02-12 20:27:39 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) |
2023-02-12 20:27:56 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 20:28:23 +0100 | <sm> | the one rule is try to go all in with ghcup, don't mix haskell tools installed by different methods |
2023-02-12 20:28:41 +0100 | <sm> | especially not mixed intel/arm tools |
2023-02-12 20:29:50 +0100 | <aljer> | sm: That makes sense. This is my first time away from pacman/apt so still getting my bearings. |
2023-02-12 20:30:56 +0100 | <sm> | either ghcup or arm brew will install arm haskell tools (and those will build arm executables). Watch out you don't install intel brew, which runs but will install intel things |
2023-02-12 20:31:34 +0100 | <sm> | ghcup is the simple path I would say |
2023-02-12 20:33:16 +0100 | oldfashionedcow | oldfashionedrat |
2023-02-12 20:33:37 +0100 | <dsal> | nix is the only thing that's worked consistently for me. But it does require knowing at least a little about nix. |
2023-02-12 20:33:39 +0100 | oldfashionedrat | oldfashionedcow |
2023-02-12 20:33:41 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 20:34:00 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
2023-02-12 20:35:11 +0100 | <eldritchcookie[m> | does backpack also recompile all dependencies if we change only the instantiated module and not the hsig file? |
2023-02-12 20:35:42 +0100 | <eldritchcookie[m> | *dependants |
2023-02-12 20:36:23 +0100 | tomku | (~tomku@user/tomku) (Read error: Connection reset by peer) |
2023-02-12 20:36:34 +0100 | <eldritchcookie[m> | like say i have module Foo that depends on Bar.hsig is Foo recompiled if Bar.hs is modified? |
2023-02-12 20:36:41 +0100 | tomku | (~tomku@user/tomku) |
2023-02-12 20:37:33 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 20:37:59 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 20:40:53 +0100 | npmania | (~Thunderbi@45.8.223.203) (Quit: npmania) |
2023-02-12 20:41:40 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) |
2023-02-12 20:41:54 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
2023-02-12 20:41:58 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 20:42:04 +0100 | npmania | (~Thunderbi@45.8.223.203) |
2023-02-12 20:42:25 +0100 | harveypwca | (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
2023-02-12 20:43:38 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-02-12 20:45:33 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2023-02-12 20:48:46 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 252 seconds) |
2023-02-12 20:48:57 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
2023-02-12 20:49:01 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 20:49:25 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
2023-02-12 20:49:32 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
2023-02-12 20:49:58 +0100 | malte | (~malte@152.89.107.66) |
2023-02-12 20:50:22 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 20:53:20 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
2023-02-12 20:53:32 +0100 | gurkenglas | (~gurkengla@dynamic-046-114-178-040.46.114.pool.telefonica.de) (Ping timeout: 246 seconds) |
2023-02-12 20:53:43 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 268 seconds) |
2023-02-12 20:53:51 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 20:54:07 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 20:55:17 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) |
2023-02-12 20:55:29 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 20:55:31 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:cd1a:e6be:bfd3:350) (Remote host closed the connection) |
2023-02-12 20:58:41 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
2023-02-12 20:58:48 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 20:59:25 +0100 | eggplantade | (~Eggplanta@104.55.37.220) |
2023-02-12 21:01:14 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 21:02:03 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 21:02:27 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
2023-02-12 21:04:27 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 21:04:41 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
2023-02-12 21:06:03 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 268 seconds) |
2023-02-12 21:08:50 +0100 | opticblast | (~Thunderbi@172.58.82.191) |
2023-02-12 21:11:37 +0100 | gurkenglas | (~gurkengla@46.114.178.40) |
2023-02-12 21:11:57 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
2023-02-12 21:13:53 +0100 | <aljer> | Alright, I uninstalled/reinstalled ghcup and was able to create and compile a cabal project immediately. Not sure what I had configured incorrectly the first time. Thanks for the help/suggestions |
2023-02-12 21:14:09 +0100 | merijn | (~merijn@c-001-001-010.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
2023-02-12 21:14:13 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
2023-02-12 21:16:21 +0100 | wroathe | (~wroathe@207.153.38.140) |
2023-02-12 21:16:21 +0100 | wroathe | (~wroathe@207.153.38.140) (Changing host) |
2023-02-12 21:16:21 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-02-12 21:16:43 +0100 | <sm> | 👍️ |
2023-02-12 21:17:04 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-02-12 21:18:28 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
2023-02-12 21:19:34 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
2023-02-12 21:19:45 +0100 | <tomsmeding> | is there a library to parse cabal.project files? |
2023-02-12 21:19:57 +0100 | <tomsmeding> | Cabal-syntax seems to be for .cabal files only, but I may be mistaken |
2023-02-12 21:22:22 +0100 | <Hecate> | tomsmeding: I'd forward this question to #hackage if I were you |
2023-02-12 21:22:33 +0100 | <tomsmeding> | oh wait I need the cabal-install library of course |
2023-02-12 21:25:38 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
2023-02-12 21:26:02 +0100 | pavonia | (~user@user/siracusa) |
2023-02-12 21:26:05 +0100 | <tomsmeding> | meeh why does that need an HttpTransport |
2023-02-12 21:26:17 +0100 | <tomsmeding> | just parse the bloody thing |
2023-02-12 21:26:44 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
2023-02-12 21:28:07 +0100 | Bocaneri | (~sauvin@user/Sauvin) |
2023-02-12 21:28:30 +0100 | Bocaneri | Guest6558 |
2023-02-12 21:29:42 +0100 | Guest6558 | SenFache |
2023-02-12 21:30:43 +0100 | Sauvin | (~sauvin@user/Sauvin) (Ping timeout: 252 seconds) |
2023-02-12 21:37:13 +0100 | Sinbad | (~Sinbad@user/sinbad) |
2023-02-12 21:39:01 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
2023-02-12 21:40:01 +0100 | mewra | mira |
2023-02-12 21:40:09 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
2023-02-12 21:42:23 +0100 | <sclv> | tomsmeding: because you can include remote files |
2023-02-12 21:43:18 +0100 | <sclv> | if you never will parse with a remote includes its ok to pass in a dummy one iirc |
2023-02-12 21:44:04 +0100 | <tomsmeding> | sclv: will 'cabal freeze' ever generate anything with a remote include :p |
2023-02-12 21:44:21 +0100 | <sclv> | no |
2023-02-12 21:46:13 +0100 | <sclv> | in fact for freeze files the cabal config parser might suffice, since project files are just an extension of it |
2023-02-12 21:46:29 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
2023-02-12 21:47:24 +0100 | <tomsmeding> | sclv: where is said config parser? |
2023-02-12 21:48:29 +0100 | <sclv> | cant lookup now, on my phone |
2023-02-12 21:48:39 +0100 | <tomsmeding> | sure, no problem |
2023-02-12 21:55:20 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 260 seconds) |
2023-02-12 21:59:15 +0100 | wroathe | (~wroathe@50.205.197.50) |
2023-02-12 21:59:15 +0100 | wroathe | (~wroathe@50.205.197.50) (Changing host) |
2023-02-12 21:59:15 +0100 | wroathe | (~wroathe@user/wroathe) |
2023-02-12 22:01:52 +0100 | rlj | (~rlj@194-218-34-180.customer.telia.com) (Quit: Client closed) |
2023-02-12 22:02:05 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds) |
2023-02-12 22:02:24 +0100 | <sclv> | also may want to use https://hackage.haskell.org/package/cabal-install-parsers |
2023-02-12 22:04:57 +0100 | <sclv> | and for standard config parser https://hackage.haskell.org/package/cabal-install-3.8.1.0/docs/Distribution-Client-Config.html#v:l… |
2023-02-12 22:08:11 +0100 | retrosenator | (~retrosena@174.211.112.224) (Read error: Connection reset by peer) |
2023-02-12 22:08:39 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 22:11:54 +0100 | opticblast | (~Thunderbi@172.58.82.191) (Ping timeout: 260 seconds) |
2023-02-12 22:12:53 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 252 seconds) |
2023-02-12 22:18:49 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 268 seconds) |
2023-02-12 22:18:56 +0100 | lackita | (~lackita@73.114.250.252) |
2023-02-12 22:19:09 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2023-02-12 22:21:49 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2023-02-12 22:21:58 +0100 | aljer | (~j@user/aljer) (Quit: WeeChat 3.8) |
2023-02-12 22:25:50 +0100 | jinsun | (~jinsun@user/jinsun) |
2023-02-12 22:26:35 +0100 | jpds | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 255 seconds) |
2023-02-12 22:28:19 +0100 | Cale | (~cale@cpe80d04ade0a03-cm80d04ade0a01.cpe.net.cable.rogers.com) (Ping timeout: 252 seconds) |
2023-02-12 22:28:53 +0100 | <eldritchcookie[m> | is there some way to get cabal to dump interface files? i don't know how to compile with backpack without cabal |
2023-02-12 22:31:14 +0100 | Guest69 | (~Guest69@2601:401:4300:55a0:1b95:c0a4:db57:c150) |
2023-02-12 22:32:24 +0100 | Guest69 | (~Guest69@2601:401:4300:55a0:1b95:c0a4:db57:c150) (Client Quit) |
2023-02-12 22:33:10 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 22:37:55 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 260 seconds) |
2023-02-12 22:38:32 +0100 | <monochrom> | backpack does need cabal. |
2023-02-12 22:39:11 +0100 | <davean> | backpack needs cabal? |
2023-02-12 22:39:13 +0100 | <davean> | hum? |
2023-02-12 22:39:18 +0100 | <monochrom> | Is it not good enough to run "cabal build" as usual and then you hunt down the *.hi files? |
2023-02-12 22:39:38 +0100 | <monochrom> | Or if you mean the *.hsig files then you have to write them. |
2023-02-12 22:42:32 +0100 | jpds | (~jpds@gateway/tor-sasl/jpds) |
2023-02-12 22:44:12 +0100 | michalz | (~michalz@185.246.204.121) (Remote host closed the connection) |
2023-02-12 22:47:54 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2023-02-12 22:49:11 +0100 | gurkenglas | (~gurkengla@46.114.178.40) (Ping timeout: 252 seconds) |
2023-02-12 22:52:00 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
2023-02-12 22:52:43 +0100 | mmhat | (~mmh@2003:f1:c730:fb3a:ee08:6bff:fe09:5315) |
2023-02-12 22:56:35 +0100 | mmhat | (~mmh@2003:f1:c730:fb3a:ee08:6bff:fe09:5315) (Client Quit) |
2023-02-12 22:59:51 +0100 | <__monty__> | /wg 15 |
2023-02-12 23:00:00 +0100 | ubert | (~Thunderbi@p200300ecdf130185faf60c5e727d766b.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
2023-02-12 23:00:00 +0100 | ub | ubert |
2023-02-12 23:00:17 +0100 | <__monty__> | Whoops, disregard. |
2023-02-12 23:00:42 +0100 | ubert1 | (~Thunderbi@p200300ecdf13019b2eac5c41519fc3af.dip0.t-ipconnect.de) |
2023-02-12 23:03:02 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2023-02-12 23:03:25 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer) |
2023-02-12 23:05:48 +0100 | Lord_of_Life_ | Lord_of_Life |
2023-02-12 23:05:58 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
2023-02-12 23:06:40 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 23:12:15 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 248 seconds) |
2023-02-12 23:17:08 +0100 | adium | (adium@user/adium) (Quit: Stable ZNC by #bnc4you) |
2023-02-12 23:17:37 +0100 | SenFache | (~sauvin@user/Sauvin) (Remote host closed the connection) |
2023-02-12 23:18:13 +0100 | opticblast | (~Thunderbi@172.58.84.5) |
2023-02-12 23:19:09 +0100 | SenFache | (~sauvin@user/Sauvin) |
2023-02-12 23:19:50 +0100 | eggplantade | (~Eggplanta@104.55.37.220) (Remote host closed the connection) |
2023-02-12 23:27:39 +0100 | <davean> | __monty__: "good enough" is not "required" |
2023-02-12 23:27:48 +0100 | <davean> | er, monochrom |
2023-02-12 23:34:15 +0100 | gurkenglas | (~gurkengla@46.114.178.40) |
2023-02-12 23:40:54 +0100 | freeside | (~mengwong@103.252.202.170) |
2023-02-12 23:45:46 +0100 | freeside | (~mengwong@103.252.202.170) (Ping timeout: 268 seconds) |
2023-02-12 23:46:03 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 248 seconds) |
2023-02-12 23:46:30 +0100 | opticblast | (~Thunderbi@172.58.84.5) (Quit: opticblast) |
2023-02-12 23:47:51 +0100 | notzmv | (~zmv@user/notzmv) |
2023-02-12 23:48:00 +0100 | CiaoSen | (~Jura@p200300c9570460002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
2023-02-12 23:49:26 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-02-12 23:59:57 +0100 | lackita | (~lackita@73.114.250.252) (Ping timeout: 268 seconds) |