| 2022-08-04 00:01:26 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2022-08-04 00:01:55 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2022-08-04 00:04:46 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-08-04 00:05:57 +0200 | kalalele | (~kalalele@2a02-a446-aea7-1-e858-b948-ec55-5937.fixed6.kpn.net) (Read error: Connection reset by peer) |
| 2022-08-04 00:08:23 +0200 | fjmorazan | (~quassel@user/fjmorazan) () |
| 2022-08-04 00:09:04 +0200 | fjmorazan | (~quassel@user/fjmorazan) |
| 2022-08-04 00:09:05 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 2022-08-04 00:14:39 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 244 seconds) |
| 2022-08-04 00:15:04 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-231.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2022-08-04 00:16:38 +0200 | acidjnk | (~acidjnk@p200300d6e70586478c218a5601cf793a.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2022-08-04 00:18:21 +0200 | lambdabot | (~lambdabot@haskell/bot/lambdabot) (Remote host closed the connection) |
| 2022-08-04 00:19:23 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 00:20:25 +0200 | lambdabot | (~lambdabot@silicon.int-e.eu) |
| 2022-08-04 00:20:25 +0200 | lambdabot | (~lambdabot@silicon.int-e.eu) (Changing host) |
| 2022-08-04 00:20:25 +0200 | lambdabot | (~lambdabot@haskell/bot/lambdabot) |
| 2022-08-04 00:29:06 +0200 | blueagain | (~blueagain@user/blueagain) |
| 2022-08-04 00:36:58 +0200 | blueagain | (~blueagain@user/blueagain) () |
| 2022-08-04 00:39:32 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 00:42:22 +0200 | nek0 | (~nek0@2a01:4f8:222:2b41::12) (Quit: The Lounge - https://thelounge.chat) |
| 2022-08-04 00:44:07 +0200 | nek0 | (~nek0@2a01:4f8:222:2b41::12) |
| 2022-08-04 00:45:23 +0200 | gurkenglas | (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2022-08-04 00:45:27 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-08-04 00:47:27 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 00:50:34 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 2022-08-04 00:51:51 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-08-04 00:53:45 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-08-04 00:57:32 +0200 | JaredMohammed[m] | (~jaredmoha@2001:470:69fc:105::2:5b48) |
| 2022-08-04 00:58:35 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
| 2022-08-04 01:04:28 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 01:08:02 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 268 seconds) |
| 2022-08-04 01:11:08 +0200 | leeks | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Ping timeout: 255 seconds) |
| 2022-08-04 01:11:35 +0200 | codaraxis | (~codaraxis@user/codaraxis) |
| 2022-08-04 01:12:08 +0200 | leeks | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 2022-08-04 01:12:12 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2022-08-04 01:17:08 +0200 | talismanick | (~talismani@campus-100-192.ucdavis.edu) (Ping timeout: 268 seconds) |
| 2022-08-04 01:18:54 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-08-04 01:30:20 +0200 | yvan-sraka | (uid419690@id-419690.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-08-04 01:35:12 +0200 | Igloo | (~ian@matrix.chaos.earth.li) |
| 2022-08-04 01:41:54 +0200 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-08-04 01:42:02 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2022-08-04 01:42:30 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 268 seconds) |
| 2022-08-04 01:44:14 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 2022-08-04 01:44:58 +0200 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 2022-08-04 01:57:49 +0200 | JaredMohammed[m] | (~jaredmoha@2001:470:69fc:105::2:5b48) () |
| 2022-08-04 01:58:30 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Ping timeout: 244 seconds) |
| 2022-08-04 02:02:46 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) (Ping timeout: 268 seconds) |
| 2022-08-04 02:07:50 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 02:08:29 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::d5f2) |
| 2022-08-04 02:08:39 +0200 | yaroot_ | (~yaroot@p3374048-ipngn8502souka.saitama.ocn.ne.jp) |
| 2022-08-04 02:10:54 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 02:11:25 +0200 | yaroot | (~yaroot@2400:4052:ac0:d900:680e:dbff:fe1e:4953) (Ping timeout: 244 seconds) |
| 2022-08-04 02:11:25 +0200 | yaroot_ | yaroot |
| 2022-08-04 02:15:20 +0200 | fserucas_ | (~fserucas@83.223.235.72) |
| 2022-08-04 02:17:32 +0200 | fserucas | (~fserucas@83.223.235.72) (Ping timeout: 245 seconds) |
| 2022-08-04 02:18:15 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 02:20:57 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2022-08-04 02:22:20 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-08-04 02:22:24 +0200 | jargon | (~jargon@184.101.188.251) |
| 2022-08-04 02:22:46 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-08-04 02:26:14 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 2022-08-04 02:26:27 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) |
| 2022-08-04 02:26:41 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) |
| 2022-08-04 02:27:38 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 2022-08-04 02:27:38 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 2022-08-04 02:27:38 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2022-08-04 02:30:01 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 2022-08-04 02:30:53 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) |
| 2022-08-04 02:30:55 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) (Remote host closed the connection) |
| 2022-08-04 02:31:11 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) |
| 2022-08-04 02:32:08 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 2022-08-04 02:32:20 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) |
| 2022-08-04 02:40:25 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 02:42:07 +0200 | sandy_doo | (~sandydoo@185.209.196.136) (Ping timeout: 245 seconds) |
| 2022-08-04 02:43:00 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-08-04 02:45:28 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 268 seconds) |
| 2022-08-04 02:51:24 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 02:52:00 +0200 | Guest15 | (~Guest15@2601:643:897f:5f73:798:18eb:66c5:dd30) |
| 2022-08-04 02:53:25 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) (Remote host closed the connection) |
| 2022-08-04 02:54:18 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) |
| 2022-08-04 02:57:50 +0200 | xff0x | (~xff0x@2405:6580:b080:900:40d:d87e:58e3:1ef6) (Ping timeout: 240 seconds) |
| 2022-08-04 03:02:22 +0200 | frost | (~frost@user/frost) |
| 2022-08-04 03:03:44 +0200 | Guest15 | (~Guest15@2601:643:897f:5f73:798:18eb:66c5:dd30) (Quit: Client closed) |
| 2022-08-04 03:10:57 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 2022-08-04 03:11:14 +0200 | Midjak | (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 2022-08-04 03:17:06 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 2022-08-04 03:29:52 +0200 | vglfr | (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 2022-08-04 03:30:18 +0200 | burnsidesLlama | (~burnsides@119247164140.ctinets.com) () |
| 2022-08-04 03:30:23 +0200 | <albet70> | @free reverse :: [a] -> [a] |
| 2022-08-04 03:30:23 +0200 | <lambdabot> | $map f . reverse = reverse . $map f |
| 2022-08-04 03:30:44 +0200 | <albet70> | how lambdabot implement this 'free'? |
| 2022-08-04 03:30:54 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 03:31:12 +0200 | <Axman6> | its source code is https://github.com/lambdabot/lambdabot |
| 2022-08-04 03:31:39 +0200 | <Axman6> | https://github.com/lambdabot/lambdabot/tree/master/lambdabot-haskell-plugins/src/Lambdabot/Plugin/… |
| 2022-08-04 03:32:22 +0200 | <Axman6> | @free f :: (((a -> b) -> c) -> d) -> d |
| 2022-08-04 03:32:22 +0200 | <lambdabot> | (forall f2 f3. (forall f4 f5. h . f4 = f5 . g => k (f2 f4) = f3 f5) => p (q f2) = f1 f3) => p (f q) = f |
| 2022-08-04 03:32:22 +0200 | <lambdabot> | f1 |
| 2022-08-04 03:33:29 +0200 | <Axman6> | but I would guess the theorems for free paper would be more useful |
| 2022-08-04 03:35:24 +0200 | <qrpnxz1> | messing with with unboxed values pretty yucky in haskell :(( |
| 2022-08-04 03:35:37 +0200 | <Axman6> | what makes you say that? |
| 2022-08-04 03:36:32 +0200 | <EvanR> | unboxed literals can be a bit weird |
| 2022-08-04 03:36:49 +0200 | <EvanR> | general values are guaranteed to behave thanks to the kind system |
| 2022-08-04 03:36:56 +0200 | <qrpnxz1> | error messages when you don't have MagicHash and UnboxedTuples enabled are pretty bad. If i didn't know about the extensions before hand, and probably be out of luck. I have to pull in all these special GHC modules because they are basically second-class "implementation details" Math is just a mess |
| 2022-08-04 03:37:02 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2022-08-04 03:37:37 +0200 | <qrpnxz1> | i can get by, but it's just not nice |
| 2022-08-04 03:40:20 +0200 | mrmr1 | (~mrmr@user/mrmr) |
| 2022-08-04 03:42:07 +0200 | mrmr | (~mrmr@user/mrmr) (Ping timeout: 245 seconds) |
| 2022-08-04 03:42:08 +0200 | mrmr1 | mrmr |
| 2022-08-04 03:43:38 +0200 | geekosaur | is pretty sure it's not supposed to be nice |
| 2022-08-04 03:47:05 +0200 | <qrpnxz1> | it's disappointing but understandable |
| 2022-08-04 03:47:07 +0200 | vglfr | (~vglfr@194.9.14.33) (Ping timeout: 245 seconds) |
| 2022-08-04 03:47:13 +0200 | qrpnxz1 | qrpnxz |
| 2022-08-04 03:47:57 +0200 | <Axman6> | they literally are implementation details, after all |
| 2022-08-04 03:48:17 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 03:49:32 +0200 | <qrpnxz> | they shouldn't be though. Unboxed are important enough to get the same amount of attention as anything in the report. |
| 2022-08-04 03:50:12 +0200 | <qrpnxz> | well let me check first that they aren't in the report actually |
| 2022-08-04 03:50:43 +0200 | <qrpnxz> | looks like no |
| 2022-08-04 03:50:47 +0200 | <geekosaur> | they're not. and other haskell impls don't have them |
| 2022-08-04 03:50:52 +0200 | <EvanR> | the issue is with some syntax for unboxed literals |
| 2022-08-04 03:51:14 +0200 | <EvanR> | the kind of stuff we usually can't complain about because it's syntax and so bikeshedding xD |
| 2022-08-04 03:51:54 +0200 | <EvanR> | the issue about not knowing about extensions is kind of not an issue though |
| 2022-08-04 03:52:13 +0200 | <geekosaur> | they're specific to ghc. and I'd argue that if you need to care and aren't a ghc dev, you've made a wrong life choice somewhere. (rust?) |
| 2022-08-04 03:52:14 +0200 | <qrpnxz> | Syntax can be pretty important. I dont' mind the # thing actually, it's just the terrible messages when you do go to use it |
| 2022-08-04 03:52:41 +0200 | vglfr | (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 2022-08-04 03:52:49 +0200 | <geekosaur> | what's it to do? per the report # is a perfectly valid operator name, and i8n fact in use on hackage |
| 2022-08-04 03:52:50 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 03:53:14 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 268 seconds) |
| 2022-08-04 03:53:14 +0200 | <qrpnxz> | yeah, (#) is used in lens for example for reviewing |
| 2022-08-04 03:53:23 +0200 | <qrpnxz> | idk that that actually clashes with magichash |
| 2022-08-04 03:54:47 +0200 | <EvanR> | as long as space around operators is required it's easy |
| 2022-08-04 03:54:56 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 03:54:56 +0200 | <qrpnxz> | on a related note, not being able to mix symbols with letters in names in general is also a big sad |
| 2022-08-04 03:55:05 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2022-08-04 03:55:12 +0200 | <EvanR> | space around operators is not required though xD |
| 2022-08-04 03:55:19 +0200 | <EvanR> | making mixed names impossible |
| 2022-08-04 03:55:50 +0200 | <qrpnxz> | not so, there would just be a different interpretation based on if you had the space or not. |
| 2022-08-04 03:55:51 +0200 | <geekosaur> | I think that changed with OverloadedRecordDot |
| 2022-08-04 03:56:20 +0200 | <EvanR> | oh jeez... we are lost then |
| 2022-08-04 03:56:36 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 2022-08-04 03:57:29 +0200 | <qrpnxz> | i would love for example if functions that return Maybe could by convention end in ?. I'd celebrate that with a few drinks |
| 2022-08-04 03:57:31 +0200 | <geekosaur> | (actually the spaces around operators thing has been coming since BangPatterns, but only got rationalized with OverloadedRecordDot) |
| 2022-08-04 03:57:56 +0200 | <EvanR> | what if they return Maybe (Maybe Something), two question marks? xD |
| 2022-08-04 03:58:32 +0200 | <qrpnxz> | mmm, i'd say one mark :) but interesting case |
| 2022-08-04 03:58:48 +0200 | <geekosaur> | BangPatterns, TypeApplications, NegativeLiterals and friends, etc. all had special spacing rules that got combined together with OverloadedRecordDot |
| 2022-08-04 03:58:54 +0200 | <EvanR> | code in the maybe monad would probably get pretty noisy |
| 2022-08-04 03:59:11 +0200 | <qrpnxz> | isn't it the opposite of noise because i don't have to case match |
| 2022-08-04 03:59:23 +0200 | <EvanR> | there would just be a lot of ? |
| 2022-08-04 03:59:45 +0200 | <qrpnxz> | there's a lot of 'e' and 'a' too, pesky common letters |
| 2022-08-04 04:00:04 +0200 | <EvanR> | well, letters and punctuation marks aren't on equal footing |
| 2022-08-04 04:00:25 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-08-04 04:00:28 +0200 | <EvanR> | letters blend together to form words and entire sentences we can see at once, while strings of punctuation marks are just that |
| 2022-08-04 04:00:36 +0200 | <qrpnxz> | wecouldalsotypelikethis,butthespacesareworthit |
| 2022-08-04 04:00:57 +0200 | <EvanR> | perl exists |
| 2022-08-04 04:01:06 +0200 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 2022-08-04 04:01:28 +0200 | <qrpnxz> | idk enough about perl to have anything to reply to that :) |
| 2022-08-04 04:01:41 +0200 | hippoid | (~hippoid@c-98-220-13-8.hsd1.il.comcast.net) (Ping timeout: 255 seconds) |
| 2022-08-04 04:01:44 +0200 | <EvanR> | if you like code containing a lot of punctuation |
| 2022-08-04 04:02:12 +0200 | <qrpnxz> | oh yeah, the variable names in perl indicate type i think? or interpretation rather (?) |
| 2022-08-04 04:02:40 +0200 | <EvanR> | no that's bad C++ |
| 2022-08-04 04:02:40 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 04:03:16 +0200 | <qrpnxz> | then i could also do things like do { a? <- fallible; case a? of { Just a -> ... |
| 2022-08-04 04:04:52 +0200 | <geekosaur> | isn't that swift? |
| 2022-08-04 04:05:03 +0200 | zaquest | (~notzaques@5.130.79.72) |
| 2022-08-04 04:05:07 +0200 | <qrpnxz> | i think ? is an operator in swift |
| 2022-08-04 04:05:27 +0200 | <qrpnxz> | that does early return on optionals |
| 2022-08-04 04:05:53 +0200 | <geekosaur> | mm, I think there's a language that has that trailing ? (mis?)feature. ruby? |
| 2022-08-04 04:06:07 +0200 | <qrpnxz> | early return for Maybe comes free with laziness, but only if you re associate all your binds correctly |
| 2022-08-04 04:06:14 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 240 seconds) |
| 2022-08-04 04:06:21 +0200 | <qrpnxz> | geekosaur: as an operator or convention? |
| 2022-08-04 04:06:32 +0200 | <geekosaur> | convention |
| 2022-08-04 04:06:32 +0200 | <qrpnxz> | scheme has it as convention for predicates |
| 2022-08-04 04:06:39 +0200 | <qrpnxz> | which is also nice |
| 2022-08-04 04:06:41 +0200 | <geekosaur> | allowed at the end of names |
| 2022-08-04 04:06:54 +0200 | <qrpnxz> | even? |
| 2022-08-04 04:06:56 +0200 | <qrpnxz> | odd? |
| 2022-08-04 04:06:58 +0200 | <qrpnxz> | that's just nice |
| 2022-08-04 04:07:07 +0200 | <geekosaur> | in any case I should have gone to bed half an hour ago |
| 2022-08-04 04:07:21 +0200 | <qrpnxz> | 👋 |
| 2022-08-04 04:07:24 +0200 | <geekosaur> | (guess that's better than lisp's "p" suffix for predicates) |
| 2022-08-04 04:08:28 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 04:12:56 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 04:20:53 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 2022-08-04 04:20:53 +0200 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-08-04 04:20:53 +0200 | finn_elija | FinnElija |
| 2022-08-04 04:25:34 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 04:27:18 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-08-04 04:28:04 +0200 | Guest|26 | (~Guest|26@S0106020fb5669598.ed.shawcable.net) |
| 2022-08-04 04:28:25 +0200 | Guest|26 | (~Guest|26@S0106020fb5669598.ed.shawcable.net) (Client Quit) |
| 2022-08-04 04:28:54 +0200 | <monochrom> | Oh, so "lisp" is a predicate... :) |
| 2022-08-04 04:29:11 +0200 | <qrpnxz> | xd |
| 2022-08-04 04:29:25 +0200 | monochrom | writes in CV: I know lisp, scheme?, and isJava. |
| 2022-08-04 04:29:34 +0200 | <qrpnxz> | haha |
| 2022-08-04 04:34:35 +0200 | <instantaphex> | Is there a way to free form type over multiple lines in ghci? I know I can use :{ :} to enter multiple lines, but I find that typos are getting me down and I can't go back and fix them. |
| 2022-08-04 04:35:33 +0200 | <Axman6> | use a file |
| 2022-08-04 04:35:53 +0200 | <instantaphex> | You got me there |
| 2022-08-04 04:36:45 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 2022-08-04 04:37:02 +0200 | <monochrom> | ghci is not an IDE |
| 2022-08-04 04:37:50 +0200 | <monochrom> | I don't understand the obsession with hand-typing lengthy code at the REPL. |
| 2022-08-04 04:38:20 +0200 | <monochrom> | Some people cite Python but Python's REPL isn't a better editor than ghci either. |
| 2022-08-04 04:39:04 +0200 | <instantaphex> | I don't hand type lengthy code per se, but it would be nice to have sort of a scratch pad type repl type thing at times |
| 2022-08-04 04:39:12 +0200 | td_ | (~td@94.134.91.79) (Ping timeout: 245 seconds) |
| 2022-08-04 04:39:28 +0200 | <Axman6> | almost like... a file... in an editor... :P |
| 2022-08-04 04:39:29 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 2022-08-04 04:39:30 +0200 | <instantaphex> | Or a vim plugin that would let me highlight a block of code and run it |
| 2022-08-04 04:39:51 +0200 | <monochrom> | My recollection is that only Smalltalk came half-close to that dream, and no one alive has seen Smalltalk by now. |
| 2022-08-04 04:40:19 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 04:40:28 +0200 | <instantaphex> | I briefly looked at a smalltalk tutorial at one point out of curiosity. I noped out pretty fast |
| 2022-08-04 04:41:11 +0200 | <monochrom> | In this case I mean Smalltalk's IDE. |
| 2022-08-04 04:41:18 +0200 | td_ | (~td@94.134.91.223) |
| 2022-08-04 04:41:56 +0200 | <instantaphex> | I feel like the Clojure community is super into repling hard core. I guess not so much for haskell devs |
| 2022-08-04 04:42:39 +0200 | <monochrom> | Ah I forgot Clojure. Yeah it gets pretty close. |
| 2022-08-04 04:42:56 +0200 | <instantaphex> | I've seen them use terms like REPL driven development |
| 2022-08-04 04:43:08 +0200 | <instantaphex> | Never tried Clojure so I have no idea |
| 2022-08-04 04:45:09 +0200 | zebrag | (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 2022-08-04 04:45:12 +0200 | <monochrom> | Clojure is an extremely dynamic language. Hot-fixing code at the REPL is an option. |
| 2022-08-04 04:45:34 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 268 seconds) |
| 2022-08-04 04:46:10 +0200 | <monochrom> | (In principle you could do that to Scheme too, but it's the Clojure people who are serious about it.) |
| 2022-08-04 04:47:21 +0200 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2022-08-04 04:47:44 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-08-04 05:03:53 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
| 2022-08-04 05:10:11 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2022-08-04 05:10:33 +0200 | jero98772 | (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) (Remote host closed the connection) |
| 2022-08-04 05:11:11 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-08-04 05:16:22 +0200 | Guest55 | (~Guest55@c-71-198-235-211.hsd1.ca.comcast.net) |
| 2022-08-04 05:18:23 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 2022-08-04 05:21:54 +0200 | <sm> | I'm alive! Smalltalk is awesome and still here |
| 2022-08-04 05:23:20 +0200 | frost30 | (~frost@user/frost) |
| 2022-08-04 05:23:29 +0200 | frost | (~frost@user/frost) (Quit: Client closed) |
| 2022-08-04 05:23:34 +0200 | frost30 | (~frost@user/frost) (Client Quit) |
| 2022-08-04 05:28:14 +0200 | Vajb | (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) (Read error: Connection reset by peer) |
| 2022-08-04 05:28:22 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) |
| 2022-08-04 05:28:47 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 2022-08-04 05:35:23 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 05:36:19 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2022-08-04 05:38:06 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) |
| 2022-08-04 05:38:23 +0200 | tinwood_ | (~tinwood@general.default.akavanagh.uk0.bigv.io) (Quit: No Ping reply in 180 seconds.) |
| 2022-08-04 05:39:49 +0200 | tinwood | (~tinwood@general.default.akavanagh.uk0.bigv.io) |
| 2022-08-04 05:39:49 +0200 | tinwood | (~tinwood@general.default.akavanagh.uk0.bigv.io) (Changing host) |
| 2022-08-04 05:39:49 +0200 | tinwood | (~tinwood@canonical/tinwood) |
| 2022-08-04 05:44:38 +0200 | rekahsoft | (~rekahsoft@bras-base-wdston4533w-grc-02-142-113-160-8.dsl.bell.ca) (Ping timeout: 240 seconds) |
| 2022-08-04 05:45:39 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2022-08-04 05:45:48 +0200 | Vajb | (~Vajb@2001:999:70c:2b99:3e15:6929:5bc6:c014) |
| 2022-08-04 05:47:15 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 05:51:30 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-08-04 05:52:34 +0200 | vglfr | (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 2022-08-04 05:53:22 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 05:58:29 +0200 | mbuf | (~Shakthi@122.165.55.71) |
| 2022-08-04 06:03:14 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 06:03:39 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2022-08-04 06:06:15 +0200 | causal | (~user@50.35.83.177) (Quit: WeeChat 3.6) |
| 2022-08-04 06:10:53 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) () |
| 2022-08-04 06:11:50 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 240 seconds) |
| 2022-08-04 06:22:04 +0200 | <EvanR> | clojure repl was cool when I tried it, until you veer into the java |
| 2022-08-04 06:23:11 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 06:26:51 +0200 | vglfr | (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 2022-08-04 06:28:51 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 06:31:22 +0200 | vglfr | (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 2022-08-04 06:32:06 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 06:37:02 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 2022-08-04 06:39:33 +0200 | vglfr | (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 2022-08-04 06:40:52 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 06:43:22 +0200 | vglfr | (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 2022-08-04 06:43:50 +0200 | <Clinton[m]> | `GHC.Generic` has this function `to :: Rep a x -> a`. I'm trying to write a function that goes from `MyUntypedData -> Maybe (Rep a x)`. I can then just use `to` to create the actual type. |
| 2022-08-04 06:43:51 +0200 | <Clinton[m]> | But what is `x` here? I need to make it something because `Rep a` has type `Type -> Type` and hence can't be a return value of a function. But what should I make it? Or will anything do here (could I just make it `()` for example?) |
| 2022-08-04 06:54:29 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 2022-08-04 06:58:26 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) |
| 2022-08-04 06:58:38 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 240 seconds) |
| 2022-08-04 07:00:55 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-08-04 07:05:02 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
| 2022-08-04 07:10:27 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 07:10:38 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 2022-08-04 07:13:28 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 2022-08-04 07:13:39 +0200 | leeks | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 2022-08-04 07:15:50 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Client Quit) |
| 2022-08-04 07:17:17 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 2022-08-04 07:17:55 +0200 | gmg | (~user@user/gehmehgeh) |
| 2022-08-04 07:21:29 +0200 | <glguy> | Clinton[m]: the way to make a Rep a x is with from :: Generic a => a -> Rep a x |
| 2022-08-04 07:22:03 +0200 | <glguy> | the extra type parameter you're asking about only exists to support Generic1 |
| 2022-08-04 07:22:12 +0200 | <glguy> | you can just set it to whatever |
| 2022-08-04 07:22:35 +0200 | <glguy> | but it doesn't sound like the usecase you described makes much sense |
| 2022-08-04 07:23:28 +0200 | <Clinton[m]> | glguy: I think I've worked out that I can just leave the `x` open, I can still make a concrete value that represents it without restricting `x` so it doesn't matter |
| 2022-08-04 07:24:03 +0200 | euandreh | (~euandreh@179.214.113.107) |
| 2022-08-04 07:24:57 +0200 | <glguy> | right, it doesn't matter what you put there |
| 2022-08-04 07:26:17 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 2022-08-04 07:31:25 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 2022-08-04 07:33:54 +0200 | razetime | (~quassel@43.254.111.18) |
| 2022-08-04 07:35:41 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 252 seconds) |
| 2022-08-04 07:39:51 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 07:44:26 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 07:47:08 +0200 | jakalx | (~jakalx@base.jakalx.net) () |
| 2022-08-04 07:51:52 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-08-04 07:57:23 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 07:57:48 +0200 | coot | (~coot@213.134.190.95) |
| 2022-08-04 08:00:54 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 08:10:12 +0200 | <albet70> | @djinn join :: ((((a->r)->r)->r)->r)-> ((a->r)->r) |
| 2022-08-04 08:10:12 +0200 | <lambdabot> | Cannot parse command |
| 2022-08-04 08:10:35 +0200 | <albet70> | @djinn ((((a->r)->r)->r)->r)-> ((a->r)->r) |
| 2022-08-04 08:10:35 +0200 | <lambdabot> | f a b = a (\ c -> c b) |
| 2022-08-04 08:13:33 +0200 | <albet70> | f a b = a (\ c -> c b), is this f join when m is Cont? |
| 2022-08-04 08:14:44 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2022-08-04 08:15:19 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-08-04 08:16:34 +0200 | razetime | (~quassel@43.254.111.18) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2022-08-04 08:19:39 +0200 | misterfish | (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) |
| 2022-08-04 08:20:01 +0200 | PiDelport | (uid25146@id-25146.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-08-04 08:22:01 +0200 | <Axman6> | @unmtl Cont r a |
| 2022-08-04 08:22:01 +0200 | <lambdabot> | (a -> r) -> r |
| 2022-08-04 08:22:25 +0200 | <Axman6> | @unmtl ContT r (Cont r) a |
| 2022-08-04 08:22:25 +0200 | <lambdabot> | (a -> (r -> r) -> r) -> (r -> r) -> r |
| 2022-08-04 08:22:36 +0200 | <Axman6> | not sure if that's relevant |
| 2022-08-04 08:23:09 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Quit: ghn) |
| 2022-08-04 08:23:13 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) |
| 2022-08-04 08:23:28 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 2022-08-04 08:23:52 +0200 | <albet70> | @unmtl Cont r (Cont r) |
| 2022-08-04 08:23:52 +0200 | <lambdabot> | err: `Cont r' is not applied to enough arguments, giving `/\A. (A -> r) -> r' |
| 2022-08-04 08:25:44 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2022-08-04 08:26:13 +0200 | <albet70> | join :: Cont r (Cont r a) -> Cont r a, this is wrong? |
| 2022-08-04 08:28:52 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-08-04 08:28:57 +0200 | instantaphex | (~jb@c-73-171-252-84.hsd1.fl.comcast.net) (Ping timeout: 268 seconds) |
| 2022-08-04 08:32:53 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 252 seconds) |
| 2022-08-04 08:33:31 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 2022-08-04 08:34:42 +0200 | fef | (~thedawn@user/thedawn) |
| 2022-08-04 08:35:05 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 2022-08-04 08:35:10 +0200 | <albet70> | @djinn (a->)->((a->r)->r)->(b->r)->r |
| 2022-08-04 08:35:10 +0200 | <lambdabot> | Cannot parse command |
| 2022-08-04 08:35:26 +0200 | <albet70> | @djinn (a->r)->((a->r)->r)->(b->r)->r |
| 2022-08-04 08:35:26 +0200 | <lambdabot> | f a b _ = b a |
| 2022-08-04 08:41:02 +0200 | jargon | (~jargon@184.101.188.251) (Remote host closed the connection) |
| 2022-08-04 08:41:38 +0200 | chele | (~chele@user/chele) |
| 2022-08-04 08:41:44 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Quit: ghn) |
| 2022-08-04 08:42:02 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 2022-08-04 08:42:59 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) (Remote host closed the connection) |
| 2022-08-04 08:43:25 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:5f26:adbf:e619:7a29) |
| 2022-08-04 08:44:03 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-08-04 08:44:22 +0200 | vglfr | (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 2022-08-04 08:44:30 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 08:50:05 +0200 | acidjnk | (~acidjnk@p200300d6e7058699cc6cce398877ca6f.dip0.t-ipconnect.de) |
| 2022-08-04 08:55:56 +0200 | misterfish | (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) (Ping timeout: 268 seconds) |
| 2022-08-04 08:57:16 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 08:57:19 +0200 | <ski> | albet70 : yes, that's `join' |
| 2022-08-04 08:57:41 +0200 | <ski> | (eta-reduced, even) |
| 2022-08-04 08:58:02 +0200 | yvan-sraka | (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) |
| 2022-08-04 09:00:20 +0200 | ubert | (~Thunderbi@77.119.221.71.wireless.dyn.drei.com) |
| 2022-08-04 09:00:56 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 09:07:27 +0200 | irfan | (~irfan@user/irfan) |
| 2022-08-04 09:08:21 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 09:09:56 +0200 | <irfan> | hello, is there a way to use `TypeApplications` to replace type annotations for values like `x :: C a => a`? |
| 2022-08-04 09:10:31 +0200 | <ski> | do you mean `x :: forall a. C a => a' ? |
| 2022-08-04 09:11:13 +0200 | <irfan> | ski: yeah |
| 2022-08-04 09:11:55 +0200 | <ski> | then you should be able to use `x @T', for whatever `T' you want to use in place of `a', rather than using a type ascription like `x :: T' |
| 2022-08-04 09:12:53 +0200 | <irfan> | ski: but expressions like `2 @Int` don't seem to work, at least in GHCi? |
| 2022-08-04 09:12:57 +0200 | vglfr | (~vglfr@194.9.14.33) (Ping timeout: 245 seconds) |
| 2022-08-04 09:13:14 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Quit: ghn) |
| 2022-08-04 09:13:33 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) |
| 2022-08-04 09:13:38 +0200 | <[exa]> | irfan: try `fromInteger @Int 2` |
| 2022-08-04 09:14:07 +0200 | <[exa]> | (2 is not a function, but a syntactic sugar) |
| 2022-08-04 09:15:02 +0200 | <irfan> | [exa]: ah, so `TypeApplications` is only meant for being used by functions, correct? |
| 2022-08-04 09:15:11 +0200 | <ski> | (that `x' was also not a function) |
| 2022-08-04 09:15:17 +0200 | <ski> | irfan : no |
| 2022-08-04 09:15:25 +0200 | <irfan> | ski: no. |
| 2022-08-04 09:16:04 +0200 | <irfan> | ski: Cannot apply expression of type ‘t1’ |
| 2022-08-04 09:16:09 +0200 | <[exa]> | irfan: you can apply types to whatever accepts the type arguments, no problem with that |
| 2022-08-04 09:16:26 +0200 | <ski> | % maxBound @Int |
| 2022-08-04 09:16:26 +0200 | <yahb2> | 9223372036854775807 |
| 2022-08-04 09:16:35 +0200 | <ski> | @type maxBound |
| 2022-08-04 09:16:36 +0200 | <lambdabot> | Bounded a => a |
| 2022-08-04 09:16:43 +0200 | <ski> | `maxBound' is not a function |
| 2022-08-04 09:16:53 +0200 | <[exa]> | just that `2 @Int` desugars to `(fromInteger (Magical2Integer)) @Int`, which is not really what we wanted |
| 2022-08-04 09:17:05 +0200 | <[exa]> | irfan: ^ |
| 2022-08-04 09:17:45 +0200 | <ski> | (s/apply types to/apply to types/) |
| 2022-08-04 09:18:34 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 09:18:49 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) |
| 2022-08-04 09:18:50 +0200 | <ski> | it would make sense to me to have `2 @Int' working, though |
| 2022-08-04 09:19:31 +0200 | <irfan> | [exa]: ah, i see. i had not declared the type for the value i was applying it for. that's why it was not working. thanks for the clarification, ski, [exa]! |
| 2022-08-04 09:19:34 +0200 | <ski> | GHC authors might be convincable to make that work |
| 2022-08-04 09:19:46 +0200 | <irfan> | ski: agreed. |
| 2022-08-04 09:20:04 +0200 | gurkenglas | (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) |
| 2022-08-04 09:20:16 +0200 | <ski> | irfan : declared the type, how ? |
| 2022-08-04 09:22:51 +0200 | <irfan> | ski: explicitly declared for some type in question i had. from the docs, i think it's not supposed to work for inferred types. |
| 2022-08-04 09:24:21 +0200 | alternateved | (~user@staticline-31-183-149-36.toya.net.pl) |
| 2022-08-04 09:25:12 +0200 | <ski> | "it" referring to ? |
| 2022-08-04 09:25:22 +0200 | <irfan> | % view = show |
| 2022-08-04 09:25:22 +0200 | <yahb2> | <no output> |
| 2022-08-04 09:25:29 +0200 | <ski> | perhaps your `x' was actually monomorphic ? |
| 2022-08-04 09:25:34 +0200 | <irfan> | % view @Int $ 7 |
| 2022-08-04 09:26:11 +0200 | <irfan> | ski: no, i've got the restriction turned off. |
| 2022-08-04 09:27:34 +0200 | <irfan> | % let view :: Show a => a -> String; view = show |
| 2022-08-04 09:27:34 +0200 | <yahb2> | <no output> |
| 2022-08-04 09:27:40 +0200 | <irfan> | view @Int $ 7 |
| 2022-08-04 09:27:57 +0200 | <irfan> | % view @Int $ 7 |
| 2022-08-04 09:27:57 +0200 | <yahb2> | "7" |
| 2022-08-04 09:31:05 +0200 | <ski> | % let view = show |
| 2022-08-04 09:31:05 +0200 | <yahb2> | <no output> |
| 2022-08-04 09:31:09 +0200 | <ski> | % :t view |
| 2022-08-04 09:31:09 +0200 | <yahb2> | view :: Show a => a -> String |
| 2022-08-04 09:31:13 +0200 | <ski> | % view @Int 2 |
| 2022-08-04 09:31:13 +0200 | <yahb2> | <interactive>:128:1: error: ; • Cannot apply expression of type ‘a0 -> String’ ; to a visible type argument ‘Int’ ; • In the expression: view @Int 2 ; In an equation for ‘it’: i... |
| 2022-08-04 09:31:52 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 2022-08-04 09:32:28 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 09:35:47 +0200 | dos__^^ | (~user@user/dos/x-1723657) |
| 2022-08-04 09:36:42 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 2022-08-04 09:38:03 +0200 | zeenk | (~zeenk@2a02:2f04:a311:2d00:6865:d863:4c93:799f) |
| 2022-08-04 09:39:03 +0200 | tcard_ | (~tcard@p945242-ipngn9701hodogaya.kanagawa.ocn.ne.jp) |
| 2022-08-04 09:39:54 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 09:40:03 +0200 | dibblego | (~dibblego@haskell/developer/dibblego) (Read error: Connection reset by peer) |
| 2022-08-04 09:40:20 +0200 | dibblego | (~dibblego@122-199-1-30.ip4.superloop.com) |
| 2022-08-04 09:40:21 +0200 | dibblego | (~dibblego@122-199-1-30.ip4.superloop.com) (Changing host) |
| 2022-08-04 09:40:21 +0200 | dibblego | (~dibblego@haskell/developer/dibblego) |
| 2022-08-04 09:41:02 +0200 | Jonno_FTW | (~come@user/jonno-ftw/x-0835346) (Ping timeout: 255 seconds) |
| 2022-08-04 09:41:17 +0200 | son0p | (~ff@181.136.122.143) (Ping timeout: 245 seconds) |
| 2022-08-04 09:41:42 +0200 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 2022-08-04 09:41:42 +0200 | tcard | (~tcard@p945242-ipngn9701hodogaya.kanagawa.ocn.ne.jp) (Ping timeout: 245 seconds) |
| 2022-08-04 09:41:42 +0200 | ByronJohnson | (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) (Ping timeout: 245 seconds) |
| 2022-08-04 09:42:43 +0200 | Jonno_FTW | (~come@api.carswap.me) |
| 2022-08-04 09:42:43 +0200 | Jonno_FTW | (~come@api.carswap.me) (Changing host) |
| 2022-08-04 09:42:43 +0200 | Jonno_FTW | (~come@user/jonno-ftw/x-0835346) |
| 2022-08-04 09:43:25 +0200 | ByronJohnson | (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) |
| 2022-08-04 09:43:32 +0200 | werneta | (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 2022-08-04 09:49:26 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:5f26:adbf:e619:7a29) (Ping timeout: 240 seconds) |
| 2022-08-04 09:49:42 +0200 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2022-08-04 09:50:35 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:8097:2d55:dcdf:fe15) |
| 2022-08-04 09:51:11 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 09:52:44 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 2022-08-04 09:54:42 +0200 | Midjak | (~Midjak@82.66.147.146) |
| 2022-08-04 09:55:25 +0200 | yvan-sraka | (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2022-08-04 09:55:44 +0200 | yvan-sraka | (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) |
| 2022-08-04 09:56:03 +0200 | frost | (~frost@user/frost) |
| 2022-08-04 10:04:26 +0200 | kuribas | (~user@188.189.234.111) |
| 2022-08-04 10:04:42 +0200 | sandy_doo | (~sandydoo@185.209.196.136) |
| 2022-08-04 10:09:27 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 10:12:46 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) (Remote host closed the connection) |
| 2022-08-04 10:15:28 +0200 | sandydoo | (~sandydoo@194.87.95.71) |
| 2022-08-04 10:15:29 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-08-04 10:15:52 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 10:16:43 +0200 | VictorHugenay | (~jh@user/VictorHugenay) |
| 2022-08-04 10:17:20 +0200 | sandy_doo | (~sandydoo@185.209.196.136) (Ping timeout: 268 seconds) |
| 2022-08-04 10:19:53 +0200 | sandy_doo | (~sandydoo@146.70.117.210) |
| 2022-08-04 10:22:09 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 252 seconds) |
| 2022-08-04 10:22:16 +0200 | sandydoo | (~sandydoo@194.87.95.71) (Ping timeout: 268 seconds) |
| 2022-08-04 10:23:12 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 2022-08-04 10:23:30 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 10:28:33 +0200 | Techcable | (~Techcable@user/Techcable) (Remote host closed the connection) |
| 2022-08-04 10:30:06 +0200 | Techcable | (~Techcable@user/Techcable) |
| 2022-08-04 10:36:52 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2022-08-04 10:39:58 +0200 | Jade1 | (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) |
| 2022-08-04 10:40:39 +0200 | hsw | (~hsw@112-104-144-236.adsl.dynamic.seed.net.tw) |
| 2022-08-04 10:42:07 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 245 seconds) |
| 2022-08-04 10:43:15 +0200 | MajorBiscuit | (~MajorBisc@c-001-031-013.client.tudelft.eduvpn.nl) |
| 2022-08-04 10:45:11 +0200 | <kuribas> | When it comes to correctness, it looks to my like the Curry/Howard isomorphism is the only way to get there. |
| 2022-08-04 10:45:37 +0200 | <kuribas> | At least for formal correctness, not testing. |
| 2022-08-04 10:45:53 +0200 | <kuribas> | Most efforts seem to lead in that direction. |
| 2022-08-04 10:46:01 +0200 | <kuribas> | Haskell is become more and more dependently typed. |
| 2022-08-04 10:46:22 +0200 | <merijn> | That depends how you write Haskell... |
| 2022-08-04 10:47:47 +0200 | __monty__ | (~toonn@user/toonn) |
| 2022-08-04 10:51:11 +0200 | <kuribas> | I mean if you want to do metaprogramming and still have correctness. |
| 2022-08-04 10:51:28 +0200 | <kuribas> | Either you give up on correctness, or you end up with a lot of type level computations. |
| 2022-08-04 10:51:51 +0200 | <kuribas> | And Generics are a really ugly part of haskell. |
| 2022-08-04 10:54:47 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 10:57:10 +0200 | benin0 | (~benin@183.82.25.146) |
| 2022-08-04 10:57:19 +0200 | <merijn> | kuribas: Depends, you can do meta programming with TTH too |
| 2022-08-04 10:58:10 +0200 | <kuribas> | sure, but it is harder to get correct. |
| 2022-08-04 10:58:14 +0200 | zeenk | (~zeenk@2a02:2f04:a311:2d00:6865:d863:4c93:799f) (Quit: Konversation terminated!) |
| 2022-08-04 10:58:29 +0200 | <kuribas> | does TTH ensure the generated program is typesafe? |
| 2022-08-04 10:58:55 +0200 | <kuribas> | Well, it cannot crash at runtime, so that's something. |
| 2022-08-04 11:01:55 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-08-04 11:05:37 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 11:06:34 +0200 | <kuribas> | Still, I find using TH to generate types or constraints a lot more cumbersome that calculating a type in the same language. |
| 2022-08-04 11:06:42 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 245 seconds) |
| 2022-08-04 11:07:04 +0200 | Jade1 | (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) (Quit: Client closed) |
| 2022-08-04 11:07:16 +0200 | <merijn> | kuribas: TTH is type safe, yes |
| 2022-08-04 11:07:33 +0200 | <kuribas> | Can it deal with polymorphic functions and data? |
| 2022-08-04 11:07:35 +0200 | <merijn> | In that it only generates code that typechecks |
| 2022-08-04 11:07:52 +0200 | Jade1 | (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) |
| 2022-08-04 11:07:56 +0200 | <kuribas> | hmm, right |
| 2022-08-04 11:09:46 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-08-04 11:12:23 +0200 | ozkutuk | (~ozkutuk@176.240.173.153) (Ping timeout: 252 seconds) |
| 2022-08-04 11:13:07 +0200 | mbuf | (~Shakthi@122.165.55.71) (Ping timeout: 252 seconds) |
| 2022-08-04 11:13:50 +0200 | mbuf | (~Shakthi@122.165.55.71) |
| 2022-08-04 11:13:53 +0200 | ozkutuk | (~ozkutuk@176.240.173.153) |
| 2022-08-04 11:15:53 +0200 | Luj | (~Luj@2a01:e0a:5f9:9681:abed:9db1:6133:89ac) (Quit: Ping timeout (120 seconds)) |
| 2022-08-04 11:16:14 +0200 | Luj | (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) |
| 2022-08-04 11:19:36 +0200 | enemeth79 | (uid309041@id-309041.lymington.irccloud.com) |
| 2022-08-04 11:21:16 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 11:21:35 +0200 | mbuf | (~Shakthi@122.165.55.71) (Read error: Connection reset by peer) |
| 2022-08-04 11:21:47 +0200 | mbuf | (~Shakthi@122.165.55.71) |
| 2022-08-04 11:22:27 +0200 | shriekingnoise | (~shrieking@186.137.167.202) (Quit: Quit) |
| 2022-08-04 11:27:36 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 2022-08-04 11:27:43 +0200 | fef | (~thedawn@user/thedawn) (Ping timeout: 268 seconds) |
| 2022-08-04 11:28:27 +0200 | <ski> | ("TTH" as opposed to "TH" ?) |
| 2022-08-04 11:28:37 +0200 | <merijn> | yes |
| 2022-08-04 11:28:49 +0200 | <ski> | what does the former expand to ? |
| 2022-08-04 11:28:56 +0200 | Jade1 | (~Jade1@ip-178-201-128-039.um46.pools.vodafone-ip.de) (Quit: Client closed) |
| 2022-08-04 11:28:57 +0200 | <merijn> | Typed TH |
| 2022-08-04 11:29:03 +0200 | <ski> | ah, right |
| 2022-08-04 11:29:37 +0200 | ski | 's more familiar with MetaML (and to some extent MetaOCaml) |
| 2022-08-04 11:30:06 +0200 | <ski> | kuribas : still wondering how CH factors into it |
| 2022-08-04 11:30:40 +0200 | yvan-sraka | (~yvan-srak@209.red-2-139-126.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2022-08-04 11:31:11 +0200 | <ski> | (type systems for staged programming have been related to modal logics, mind) |
| 2022-08-04 11:32:35 +0200 | <ski> | kuribas : what's the difference between generation and calculation, there ? |
| 2022-08-04 11:32:37 +0200 | <kuribas> | ski: CH? |
| 2022-08-04 11:32:43 +0200 | <ski> | Curry-Howard |
| 2022-08-04 11:33:17 +0200 | EvanR_ | (~EvanR@user/evanr) |
| 2022-08-04 11:33:51 +0200 | <kuribas> | Well, thinking of types as proofs helps in modelling complex logic. |
| 2022-08-04 11:34:01 +0200 | <kuribas> | with GADTs, dependent types, etc... |
| 2022-08-04 11:34:15 +0200 | EvanR | (~EvanR@user/evanr) (Remote host closed the connection) |
| 2022-08-04 11:34:25 +0200 | <kuribas> | With dependent types I can make a type that contains arbitrary code to solve a constraint. |
| 2022-08-04 11:35:00 +0200 | <kuribas> | But without them I am forced to generate the Constraints or types using TH. |
| 2022-08-04 11:35:33 +0200 | <ski> | itym inhabitants of types as proofs |
| 2022-08-04 11:36:16 +0200 | <kuribas> | yes |
| 2022-08-04 11:36:23 +0200 | <ski> | well, you said "same language", which i took to be TH |
| 2022-08-04 11:36:57 +0200 | <kuribas> | well, TH is haskell, but it operates on a syntactic level. |
| 2022-08-04 11:37:22 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-08-04 11:37:23 +0200 | <kuribas> | Though dependent type checking does also... hmm... |
| 2022-08-04 11:37:28 +0200 | <merijn> | It operates at an AST level, though? |
| 2022-08-04 11:37:35 +0200 | <ski> | so what is the difference between generating a type, and calculating a type, in TH ? |
| 2022-08-04 11:37:39 +0200 | <merijn> | dependent types aren't syntactic? |
| 2022-08-04 11:37:40 +0200 | <kuribas> | merijn: right |
| 2022-08-04 11:37:48 +0200 | <ski> | (or did i misunderstand your statement) |
| 2022-08-04 11:37:59 +0200 | <kuribas> | merijn: dependent type checking works by normalisation of expressions. |
| 2022-08-04 11:38:10 +0200 | <kuribas> | merijn: equality is syntactic equality after type checking. |
| 2022-08-04 11:39:09 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 11:39:20 +0200 | <kuribas> | well, before type checking... |
| 2022-08-04 11:40:09 +0200 | <kuribas> | I just seem to be able to better solve hard type level stuff when thinking of types as propositions. |
| 2022-08-04 11:40:28 +0200 | <kuribas> | GADTs as carrying "proofs". |
| 2022-08-04 11:41:21 +0200 | <kuribas> | I don't mean to say that formal proofs are alway better than just writing tests. |
| 2022-08-04 11:41:42 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 2022-08-04 11:41:50 +0200 | <kuribas> | But when you go the way of formal correctness, it seems you end up with Curry/Howard. |
| 2022-08-04 11:42:04 +0200 | <merijn> | Not really |
| 2022-08-04 11:42:12 +0200 | <merijn> | At least, I don't see it |
| 2022-08-04 11:42:40 +0200 | <kuribas> | merijn: counterexample? |
| 2022-08-04 11:43:24 +0200 | kenran | (~kenran@p200300df770eae00d275524cc766554f.dip0.t-ipconnect.de) |
| 2022-08-04 11:43:46 +0200 | <ski> | Racket has an interesting higher-order contract system, which can interact usefully with Typed Racket |
| 2022-08-04 11:44:24 +0200 | <kuribas> | contracts sounds to me like runtime testing, no? |
| 2022-08-04 11:44:26 +0200 | sandy_doo | (~sandydoo@146.70.117.210) (Ping timeout: 268 seconds) |
| 2022-08-04 11:44:32 +0200 | <ski> | intuitionistic logic doesn't necessarily imply CH |
| 2022-08-04 11:44:36 +0200 | <ski> | kuribas : yes, indeed |
| 2022-08-04 11:45:04 +0200 | <merijn> | kuribas: A lot of formal methods verification stuff doesn't really interact with CH all that much |
| 2022-08-04 11:45:29 +0200 | <merijn> | kuribas: It's a lot more "designing state machines and proof certain transitions/states can never happen" |
| 2022-08-04 11:45:55 +0200 | <kuribas> | right. Maybe I am thinking more about "correct by construction". |
| 2022-08-04 11:46:10 +0200 | <kuribas> | Rather than, I have a program, now prove it correct. |
| 2022-08-04 11:46:14 +0200 | <ski> | like specifying that a higher-order function has some preconditions on its parameters, and some postcondition involving those and the result, and that the preconditions on the function parameters in turn can have pre- and post- conditions. and when a contract fails, you should properly distinguish between the higher-order function failing, and its callback failing, properly attributing blame either to the |
| 2022-08-04 11:46:20 +0200 | <ski> | callee or the caller |
| 2022-08-04 11:46:34 +0200 | <ski> | (i believe Wadler also wrote some paper about contracts) |
| 2022-08-04 11:46:48 +0200 | <kuribas> | ski: but if it is runtime, can you call it still formal verification? |
| 2022-08-04 11:47:01 +0200 | <ski> | i wouldn't |
| 2022-08-04 11:48:22 +0200 | <kuribas> | I think "correct by construction" is much more feasible. |
| 2022-08-04 11:48:24 +0200 | <ski> | (just mentioning it as an interesting case of "tests", one that can interact with types, iirc) |
| 2022-08-04 11:48:31 +0200 | <lortabac> | kuribas: "correct by construction" is not the only way to prove programs correct |
| 2022-08-04 11:48:47 +0200 | <lortabac> | you can have extrinsic proofs in the program itself |
| 2022-08-04 11:49:03 +0200 | <lortabac> | or you can have refinements à la Liquid Haskell |
| 2022-08-04 11:49:04 +0200 | <kuribas> | I just proving programs correct after writing the program very tedious and hard. |
| 2022-08-04 11:49:08 +0200 | ski | . o O ( AoC ) |
| 2022-08-04 11:49:42 +0200 | <ski> | i recently looked a bit at ATS .. quite interesting system |
| 2022-08-04 11:49:57 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2022-08-04 11:50:02 +0200 | <lortabac> | kuribas: it depends |
| 2022-08-04 11:50:35 +0200 | son0p | (~ff@181.136.122.143) |
| 2022-08-04 11:50:39 +0200 | <ski> | (being able to reason about system-level concepts like mutable locations, in a dependent setting) |
| 2022-08-04 11:51:23 +0200 | <lortabac> | for example "correct by construction" data types means you need a different type for each invariant |
| 2022-08-04 11:51:51 +0200 | ski | . o O ( McBride's ornaments ) |
| 2022-08-04 11:52:08 +0200 | <lortabac> | whereas you might use lists and add extrinsic proofs for the properties you want to check |
| 2022-08-04 11:53:08 +0200 | CiaoSen | (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 2022-08-04 11:54:44 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2022-08-04 11:58:00 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 2022-08-04 12:02:29 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 12:05:20 +0200 | sandy_doo | (~sandydoo@146.70.117.210) |
| 2022-08-04 12:14:21 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
| 2022-08-04 12:16:33 +0200 | sandy_doo | (~sandydoo@146.70.117.210) (Ping timeout: 252 seconds) |
| 2022-08-04 12:18:58 +0200 | <kuribas> | lortabac: also correct by construction functions, where you have to pass a constraint which proves some invariants. |
| 2022-08-04 12:19:15 +0200 | <kuribas> | "correct by constraints" maybe ? |
| 2022-08-04 12:34:31 +0200 | vglfr | (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 2022-08-04 12:35:38 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 12:42:02 +0200 | <kuribas> | ski: with dependent types you could make contracts as constraints on a passed value. |
| 2022-08-04 12:42:13 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) |
| 2022-08-04 12:42:56 +0200 | <kuribas> | ski: (foo:MyData) -> MeetConstraints foo FooConstraints => Result |
| 2022-08-04 12:43:06 +0200 | <kuribas> | (maybe offtopic because this is idris) |
| 2022-08-04 12:43:48 +0200 | <kuribas> | s/MeetConstraints/MeetContracts |
| 2022-08-04 12:44:51 +0200 | <kuribas> | but that mostly works if the contract is easily proven. |
| 2022-08-04 12:45:12 +0200 | <kuribas> | For complex stuff making tests is easier. |
| 2022-08-04 12:47:07 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 2022-08-04 12:47:11 +0200 | frost | (~frost@user/frost) (Quit: Client closed) |
| 2022-08-04 12:47:32 +0200 | frost | (~frost@user/frost) |
| 2022-08-04 12:50:07 +0200 | <lisbeths> | I want to take a second to admire haskell curry, probably one of the most syntactically successful programmers of all time. |
| 2022-08-04 12:50:43 +0200 | <lisbeths> | Without the notion of a lambda that takes an x that returns a lamba from moses shoenfinkel, and without currying, we wouldn't have the beauty of haskell. |
| 2022-08-04 12:50:52 +0200 | <lisbeths> | Thank you to these two brilliant men. |
| 2022-08-04 12:58:32 +0200 | sandy_doo | (~sandydoo@146.70.117.210) |
| 2022-08-04 13:06:24 +0200 | <kuribas> | is this a bot? |
| 2022-08-04 13:06:26 +0200 | <ski> | kuribas : hm, right. i was more thinking of executable contracts (e.g. a contract that a given function parameter only computes prime numbers) |
| 2022-08-04 13:06:32 +0200 | <ski> | no, kuribas |
| 2022-08-04 13:06:52 +0200 | <kuribas> | because that sounded like a random blurb of words. |
| 2022-08-04 13:06:54 +0200 | xff0x | (~xff0x@2405:6580:b080:900:13b:63d1:e32e:fe38) |
| 2022-08-04 13:08:02 +0200 | <ski> | (well, with LiquidHaskell you can also write stuff like `{foo :: MyData | ..foo..} -> Result') |
| 2022-08-04 13:08:12 +0200 | <kuribas> | right |
| 2022-08-04 13:10:17 +0200 | misterfish | (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) |
| 2022-08-04 13:17:08 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 13:17:34 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 2022-08-04 13:18:09 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 13:18:44 +0200 | <kuribas> | lisbeths: haskell curry wasn't a programmer |
| 2022-08-04 13:19:40 +0200 | <lisbeths> | the language police have arrived |
| 2022-08-04 13:20:06 +0200 | <kuribas> | semantics police maybe? |
| 2022-08-04 13:21:17 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 2022-08-04 13:21:52 +0200 | gurkenglas | (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2022-08-04 13:23:06 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 268 seconds) |
| 2022-08-04 13:26:16 +0200 | jean-paul[m] | (~jean-paul@2001:470:69fc:105::d1ab) |
| 2022-08-04 13:26:25 +0200 | exarkun | (~exarkun@user/exarkun) (WeeChat 3.5) |
| 2022-08-04 13:29:58 +0200 | <lisbeths> | you'll never get me copper |
| 2022-08-04 13:30:04 +0200 | lisbeths | runs |
| 2022-08-04 13:30:14 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 13:30:19 +0200 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 244 seconds) |
| 2022-08-04 13:30:25 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 13:31:03 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 2022-08-04 13:31:31 +0200 | <ski> | there used to be a SyntaxPolice in here |
| 2022-08-04 13:31:39 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 13:32:07 +0200 | <jackdk> | do you mean, "you'll never fetch me [some] copper", "you'll never take my copper", or "you [policeman] will never get me"? |
| 2022-08-04 13:32:27 +0200 | <ski> | @quote SyntaxNinja |
| 2022-08-04 13:32:27 +0200 | <lambdabot> | SyntaxNinja says: You'd be surprised how hard is to hire haskellers :( They're all like, "Yeah, I'll come work for you, and by 'come' I mean stay here and work remotely and by 'work for you' I mean |
| 2022-08-04 13:32:28 +0200 | <lambdabot> | I'll keep doing what I'm doing." ;) |
| 2022-08-04 13:32:32 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 245 seconds) |
| 2022-08-04 13:33:01 +0200 | <Hecate> | jackdk: 3rd one :) |
| 2022-08-04 13:34:32 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2022-08-04 13:36:07 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 252 seconds) |
| 2022-08-04 13:39:26 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-08-04 13:39:38 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 13:39:50 +0200 | <__monty__> | So critical of remote work. And I'm sure it's not as hard to find people willing to write non research-type Haskell nowadays. |
| 2022-08-04 13:42:53 +0200 | <ski> | that was some years ago, true |
| 2022-08-04 13:43:06 +0200 | <ski> | (possibly more than ten, i don't recall) |
| 2022-08-04 13:43:29 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2022-08-04 13:43:50 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2022-08-04 13:57:52 +0200 | <merijn> | I mean, that quote is referring to "we tried hire ekmett, dons, bos, simon marlow, etc." |
| 2022-08-04 13:58:17 +0200 | <merijn> | I mean, 90% of #haskell was people like that 10-15 years ago |
| 2022-08-04 13:58:30 +0200 | <merijn> | At least, the active portion :p |
| 2022-08-04 14:00:35 +0200 | <ski> | it was a fun time :b |
| 2022-08-04 14:01:23 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-08-04 14:06:49 +0200 | ozkutuk | (~ozkutuk@176.240.173.153) (Quit: The Lounge - https://thelounge.chat) |
| 2022-08-04 14:07:38 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-08-04 14:09:08 +0200 | enemeth79 | (uid309041@id-309041.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-08-04 14:09:18 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 14:19:37 +0200 | Pickchea | (~private@user/pickchea) (Ping timeout: 245 seconds) |
| 2022-08-04 14:24:15 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-08-04 14:24:32 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 14:25:38 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 14:29:39 +0200 | kuribas` | (~user@silversquare.silversquare.eu) |
| 2022-08-04 14:30:52 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 245 seconds) |
| 2022-08-04 14:31:33 +0200 | kuribas | (~user@188.189.234.111) (Ping timeout: 268 seconds) |
| 2022-08-04 14:31:39 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 14:33:56 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 14:38:11 +0200 | noteness | (~noteness@user/noteness) (Remote host closed the connection) |
| 2022-08-04 14:41:03 +0200 | noteness | (~noteness@user/noteness) |
| 2022-08-04 14:43:04 +0200 | <siers> | work they did not? |
| 2022-08-04 14:43:13 +0200 | <Axman6> | those were the days... |
| 2022-08-04 14:43:58 +0200 | <Axman6> | Here I am, writing Haskell* remotely for the man, doin my job. What a chump |
| 2022-08-04 14:44:21 +0200 | <siers> | what is the product about? |
| 2022-08-04 14:44:27 +0200 | <Axman6> | (* "Haskell" = Daml) |
| 2022-08-04 14:45:18 +0200 | <siers> | anyway, I have an actual question. I am looking at this recursion scheme tutorial (in scala, I'm sorry) and it is calling the fold function an "algebra" and the unfold function a "coalgebra". First, is this the correct terminology and second, why is it an algebra and is it the algebra kind of algebra — i.e. set of operations and laws on some set of elements? |
| 2022-08-04 14:45:51 +0200 | <siers> | I guess I'm thinking of an algebraic structure |
| 2022-08-04 14:46:38 +0200 | <ski> | the argument to the fold/unfold is the algebra/coalgebra |
| 2022-08-04 14:47:08 +0200 | <siers> | you're absolutely right and that's what I meant, sorry |
| 2022-08-04 14:47:15 +0200 | <siers> | fold function as in the function you pass to fold |
| 2022-08-04 14:47:20 +0200 | <ski> | cata :: Functor f => (f r -> r) -> (Mu f -> r) -- fold |
| 2022-08-04 14:47:32 +0200 | <siers> | mu is the fix operator? |
| 2022-08-04 14:47:39 +0200 | <ski> | ana :: Functor f => (s -> f s) -> (s -> Nu f) -- unfold |
| 2022-08-04 14:47:49 +0200 | <siers> | or I guess type |
| 2022-08-04 14:47:53 +0200 | <Axman6> | @hoogle Mu |
| 2022-08-04 14:47:53 +0200 | <lambdabot> | Data.Fix newtype Mu f |
| 2022-08-04 14:47:53 +0200 | <lambdabot> | Data.Fix Mu :: (forall a . (f a -> a) -> a) -> Mu f |
| 2022-08-04 14:47:53 +0200 | <lambdabot> | Data.ISO3166_CountryCodes MU :: CountryCode |
| 2022-08-04 14:47:58 +0200 | <ski> | `Mu f' is the least fixed point of `f', and `Nu f' is the greatest one |
| 2022-08-04 14:48:52 +0200 | <ski> | e.g. `Mu (Compose Maybe (a,))' is finite lists of `a's, while `Nu (Compose Maybe (a,))' is potentially finite streams of `a's |
| 2022-08-04 14:49:20 +0200 | <siers> | @hoogle Compose |
| 2022-08-04 14:49:21 +0200 | <lambdabot> | module Data.Functor.Compose |
| 2022-08-04 14:49:21 +0200 | <lambdabot> | Data.Functor.Compose newtype Compose f g a |
| 2022-08-04 14:49:21 +0200 | <lambdabot> | Data.Functor.Compose Compose :: f (g a) -> Compose f g a |
| 2022-08-04 14:49:28 +0200 | <siers> | ah, ok |
| 2022-08-04 14:49:39 +0200 | <siers> | suspected so |
| 2022-08-04 14:49:51 +0200 | <Axman6> | Is that Mu above the right one? |
| 2022-08-04 14:50:03 +0200 | <siers> | looks about right |
| 2022-08-04 14:50:09 +0200 | <ski> | `Mu Maybe' is natural numbers. `Nu Maybe' is natural numbers extended with an infinity element, `inf = Succ inf' (`Nu Maybe' is also sometimes known as the "generic convergent sequence", or the "one-point compactification of the naturals") |
| 2022-08-04 14:50:34 +0200 | <Axman6> | I think I was actually expecting to see Fix actually... newtype Fix f = Fix (f (fix f)) |
| 2022-08-04 14:50:43 +0200 | <Axman6> | Fix* |
| 2022-08-04 14:50:54 +0200 | <ski> | in Haskell, `Mu' and `Nu' are both expressed in the same way. but there's a conceptual distinction, when we ignore bottom elements |
| 2022-08-04 14:51:42 +0200 | <ski> | Axman6 : well, that `Mu' above is a different encoding .. |
| 2022-08-04 14:52:07 +0200 | misterfish | (~misterfis@ip214-130-173-82.adsl2.static.versatel.nl) (Ping timeout: 245 seconds) |
| 2022-08-04 14:52:18 +0200 | <ski> | newtype Mu f = In (f (Mu f)) -- is the encoding i was thinking of |
| 2022-08-04 14:53:08 +0200 | coot | (~coot@213.134.176.158) |
| 2022-08-04 14:53:23 +0200 | <Axman6> | yeah that's what I was thinking about |
| 2022-08-04 14:53:44 +0200 | <ski> | siers : anyway, consider a monoid, on a type `M'. you have a neutral element `mempty :: M', and a binary combination `mappend,(<>) :: M -> M -> M' .. you also have three laws involving these two operations |
| 2022-08-04 14:54:02 +0200 | <siers> | right |
| 2022-08-04 14:54:05 +0200 | coot | (~coot@213.134.176.158) (Client Quit) |
| 2022-08-04 14:54:35 +0200 | coot | (~coot@213.134.176.158) |
| 2022-08-04 14:56:06 +0200 | frost | (~frost@user/frost) (Ping timeout: 252 seconds) |
| 2022-08-04 14:56:52 +0200 | autophagian | (~mika@ip5f5bf3a3.dynamic.kabel-deutschland.de) |
| 2022-08-04 14:56:55 +0200 | <ski> | now .. given any set/type, you can form the "free monoid" on it, which is the "least restricted" set/type which includes all the elements of the former one, and also has the two monoid operations defined, such that expressions involving them and the elements are *only* considered equal if you can prove them to be equal by the laws |
| 2022-08-04 14:57:43 +0200 | <ski> | this free monoid is the monoid of (finite) lists over the type `a', with singleton map as the inclusion, and empty list and append as the monoid operations |
| 2022-08-04 14:59:11 +0200 | <siers> | I am not familiar with free monoids |
| 2022-08-04 14:59:22 +0200 | <siers> | should this explanation be enough to fully grasp them? :) |
| 2022-08-04 15:00:02 +0200 | <ski> | if the element type `a' is itself a monoid, you can "evaluate/interpret" the list of elements, by replacing empty list with `mempty :: M', and append with `mappend :: M -> M -> M' (it doesn't matter which way you associate, due to the laws) |
| 2022-08-04 15:00:17 +0200 | <ski> | @type Control.Lens.Fold.foldBy :: (m -> m -> m) -> m -> ([m] -> m) |
| 2022-08-04 15:00:19 +0200 | <lambdabot> | (m -> m -> m) -> m -> [m] -> m |
| 2022-08-04 15:00:25 +0200 | <ski> | @type fold :: Monoid m => [m] -> m |
| 2022-08-04 15:00:26 +0200 | <lambdabot> | Monoid m => [m] -> m |
| 2022-08-04 15:00:36 +0200 | gurkenglas | (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) |
| 2022-08-04 15:01:26 +0200 | <siers> | so you get a monoid for a list of elements and that's the free monoid? |
| 2022-08-04 15:02:49 +0200 | <ski> | (you can replace `[m]' with `t m', where `Foldable t' holds, since `Foldable', more or less, means "list-like". although see "Free Monoids in Haskell" <https://web.archive.org/web/20150222212709/http://comonad.com/reader/2015/free-monoids-in-haskell/>) |
| 2022-08-04 15:02:50 +0200 | <siers> | so in the free monoid, the items are both the elements of a and expressions with the monoid ops and "a"s? |
| 2022-08-04 15:03:21 +0200 | <ski> | the free monoid of `a' is `[a]' (if you ignore the infinite (and the partial) lists) |
| 2022-08-04 15:03:26 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-08-04 15:03:30 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 15:03:32 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-08-04 15:03:45 +0200 | <siers> | what's a partial list? are they in math? |
| 2022-08-04 15:04:02 +0200 | <ski> | (you take the free monoid of a type/set (the element *type*), not of an element, or a list of them) |
| 2022-08-04 15:04:10 +0200 | <ski> | > 0 : 1 : undefined |
| 2022-08-04 15:04:12 +0200 | <lambdabot> | [0,1*Exception: Prelude.undefined |
| 2022-08-04 15:04:24 +0200 | nek0 | (~nek0@2a01:4f8:222:2b41::12) (Quit: The Lounge - https://thelounge.chat) |
| 2022-08-04 15:04:29 +0200 | <ski> | in denotational semantics, written like `0 : 1 : _|_' |
| 2022-08-04 15:05:16 +0200 | <siers> | "¬ (0 : 1 : ⊥)" :) |
| 2022-08-04 15:05:47 +0200 | <ski> | anyway, consider the two arguments, of type `m -> m -> m' and `m', to `foldBy'. these describe the monoid operations that we've chosen to use, on `m' (the `foldBy' operation assumes that these actually satisfies the monoid laws, as a precondition) |
| 2022-08-04 15:06:01 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 244 seconds) |
| 2022-08-04 15:06:07 +0200 | <siers> | ski, oh, I understood that a is the type/set in one instance and an element in the other in my sentence. I am being imprecise, sorr.y |
| 2022-08-04 15:06:43 +0200 | <ski> | using "type algebra", we can reexpress these as `(m,m) -> m' and `() -> m'. or in more mathy notation, `m^2 -> m' and `1 -> m' (or `m^0 -> m', if you prefer) |
| 2022-08-04 15:07:08 +0200 | <ski> | so, `(m -> m -> m) -> m -> ([m] -> m) |
| 2022-08-04 15:07:09 +0200 | <siers> | m^0 — cute :) |
| 2022-08-04 15:07:21 +0200 | <siers> | I'll try to decode that bit about the foldBy |
| 2022-08-04 15:07:32 +0200 | Furor | (~colere@about/linux/staff/sauvin) (Ping timeout: 245 seconds) |
| 2022-08-04 15:08:06 +0200 | <ski> | so, `(m -> m -> m) -> m -> ([m] -> m)' becomes `((m,m) -> m) -> (() -> m) -> ([m] -> m)' becomes `(Either () (m,m) -> m) -> ([m] -> m)' (you could say `Maybe' instead of `Either ()') |
| 2022-08-04 15:08:12 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) |
| 2022-08-04 15:08:16 +0200 | Colere | (~colere@about/linux/staff/sauvin) |
| 2022-08-04 15:08:23 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2022-08-04 15:08:28 +0200 | <siers> | those look isomorphic :) |
| 2022-08-04 15:08:33 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 268 seconds) |
| 2022-08-04 15:08:33 +0200 | <siers> | maybe / either () |
| 2022-08-04 15:09:05 +0200 | <ski> | this `Either () (m,m) -> m' / `1 + m^2 -> m' / `m^0 + m^2 -> m' is the type of (monoid, in this case) algebras, on `m' (assuming the laws are satisfied) |
| 2022-08-04 15:09:21 +0200 | <ski> | it sums up all the operations of the algebra, in a single operation |
| 2022-08-04 15:09:37 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 2022-08-04 15:10:34 +0200 | Furor | (~colere@about/linux/staff/sauvin) |
| 2022-08-04 15:10:42 +0200 | <ski> | a Peano algebra on a set `p' consists of an element `zero :: p' and a function `succ :: p -> p'. in this case, there's no laws. e.g. `p' could be `Bool', `zero' could be `True', and `succ' could be `not' |
| 2022-08-04 15:11:31 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-08-04 15:12:22 +0200 | <siers> | ok, I got it all |
| 2022-08-04 15:12:48 +0200 | <ski> | natural numbers is the "initial" peano algebra. for any peano algebra `(p,zero,succ)', there is a function (specifically a peano algebra (homo)morphism) `fold_zero_succ :: Nat -> p'. in Haskell, we'd express this as parameterized over `zero' and `succ', as `fold :: p -> (p -> p) -> (Nat -> p)' |
| 2022-08-04 15:12:51 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 15:13:22 +0200 | Colere | (~colere@about/linux/staff/sauvin) (Ping timeout: 245 seconds) |
| 2022-08-04 15:14:09 +0200 | CiaoSen | (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2022-08-04 15:14:24 +0200 | <siers> | yeah, I can see why that fold is a homomorphism |
| 2022-08-04 15:14:32 +0200 | <ski> | anyway, the general pattern that seems to be emerging is that we can express the operations over the carrier / underlying set `a' as a single operation, in `F a -> a', for some functor `F' (often a polynomial one, like `F a = 1 + a^2' or `F a = 1 + a') |
| 2022-08-04 15:14:48 +0200 | <ski> | in such a case, we talk about an `F'-algebra (`F' being a functor) |
| 2022-08-04 15:16:11 +0200 | <ski> | (i'm not aware of how this is extended from the case of an algebra with no laws (an "anarchic algebra", like Peano, or directed multigraphs), to one with laws (like monoids, groups, rings, vector spaces, lattices, boolean algebras ..)) |
| 2022-08-04 15:16:14 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-08-04 15:17:25 +0200 | <ski> | anyway, for unfold, we typically have, instead of a "recursive result type" `r', that we combine `r -> r -> r', and generate at leaves `r', and then use those operations to crush a structure to a single result `r' |
| 2022-08-04 15:19:50 +0200 | <ski> | instead of that, we have a state type `s', some observations/properties, like `s -> C' for constants `C', and some state transitions, like `s -> s', or `s -> (P -> s)' (for some parameter `P'). anyway, given `unfold :: (s -> C) -> (s -> (P -> s)) -> (s -> Obj)', where `Obj' is the "OO-like" (or dynamical-system like) type we're unfolding into |
| 2022-08-04 15:20:35 +0200 | <ski> | we can reexpress that as `(s -> (C,P -> s)) -> (s -> Ob)'. which generalizes similarly to `(s -> f s) -> (s -> Nu s)', where `f' is again a functor |
| 2022-08-04 15:20:45 +0200 | <ski> | the input of type `s -> f s' here is the `f'-coalgebra |
| 2022-08-04 15:20:53 +0200 | hippoid | (~hippoid@d53-64-120-188.nap.wideopenwest.com) |
| 2022-08-04 15:23:51 +0200 | <ski> | "A Tutorial on (Co)Algebras and (Co)Induction" by Bart Jacobs,Jan Rutten in 1997 at <https://www.cs.ru.nl/B.Jacobs/PAPERS/JR.pdf> might perhaps be helpful |
| 2022-08-04 15:24:47 +0200 | <ski> | (apparently there's also a "A Tutorial on Co-induction and Functional Programming" in 1994 by Andrew D. Gordon at <https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3914>, but i haven't read this) |
| 2022-08-04 15:25:16 +0200 | superice | (~superice@2a01:7c8:aab9:48e:5054:ff:fe7b:347) |
| 2022-08-04 15:25:30 +0200 | <siers> | hm, wouldn't that Obj have to appear twice in unfold? I guess I misunderstood something |
| 2022-08-04 15:26:10 +0200 | <ski> | cata phi = phi . fmap (cata phi) . out |
| 2022-08-04 15:26:26 +0200 | <ski> | ana psi = In . fmap (ana psi) . psi |
| 2022-08-04 15:26:46 +0200 | <ski> | (also look up "recursion schemes", and, perhaps, "Squiggol") |
| 2022-08-04 15:28:04 +0200 | <ski> | (assuming `newtype Fix f = In {out :: f (Fix f)}' as encoding for both `Mu f' and `Nu f') |
| 2022-08-04 15:29:25 +0200 | <siers> | I read about F-algebras once, but that made less sense than what I heard from you now. |
| 2022-08-04 15:29:52 +0200 | zmt00 | (~zmt00@user/zmt00) |
| 2022-08-04 15:30:20 +0200 | <siers> | And I cannot believe you wrote out all of this for me (and for anyone else who's reading), that is amazing. I almost understand all of it, but I'm decoding the bit about the unfold. |
| 2022-08-04 15:31:45 +0200 | superice | (~superice@2a01:7c8:aab9:48e:5054:ff:fe7b:347) () |
| 2022-08-04 15:34:02 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-08-04 15:34:09 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 15:37:06 +0200 | ski | . o O ( "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" by Erik Meijer,Maarten Fokkinga,Ross Paterson in 1991-08-26 at <https://maartenfokkinga.github.io/utwente/mmf91m.pdf> ) |
| 2022-08-04 15:37:17 +0200 | ski | . o O ( "Bananas in Space: Extending Fold and Unfold to Exponential Types" by Erik Meijer,Graham Huttom in 1995 at <https://www.cs.nott.ac.uk/~pszgmh/bananas.pdf> ) |
| 2022-08-04 15:37:24 +0200 | ski | . o O ( "A tutorial on the universality and expressiveness of fold" by Graham Hutton in 1999-07 at <https://www.cs.nott.ac.uk/~pszgmh/bib.html#fold> ) |
| 2022-08-04 15:37:29 +0200 | <merijn> | That first paper is rough, though :p |
| 2022-08-04 15:38:17 +0200 | gdd1 | gdd |
| 2022-08-04 15:39:56 +0200 | <ski> | anyway, the other encoding of `Mu f' (roughly speaking) comes from taking `cata :: (f r -> r) -> (Mu f -> r)', `flip'ping it into `flip cata :: Mu f -> (forall r. (f r -> r) -> r)', and claiming that this is a bijection, electing to define `Mu f' to amount to `forall r. (f r -> r) -> r' |
| 2022-08-04 15:41:28 +0200 | <ski> | similarly, we can take `ana :: (s -> f s) -> (s -> Nu s)', and `uncurry' (and `flip', if we want to, which i do) it into `(exists s. (s,s -> f s)) -> Nu f', and similarly define `Nu f' as `exists s. (s,s -> f s)' |
| 2022-08-04 15:42:45 +0200 | <ski> | the former is related to the Church (or CPS) encoding of a data type. the latter to the (what i call) "State encoding" |
| 2022-08-04 15:43:38 +0200 | <ski> | @quote separation.of |
| 2022-08-04 15:43:39 +0200 | <lambdabot> | GuySteele says: Some people prefer not to commingle the functional, lambda-calculus part of a language with the parts that do side effects. It seems they believe in the separation of Church and |
| 2022-08-04 15:43:39 +0200 | <lambdabot> | state. |
| 2022-08-04 15:43:45 +0200 | <ski> | @quote are.dual |
| 2022-08-04 15:43:45 +0200 | <lambdabot> | ski says: I'd rather say that in Haskell, Church and State are dual |
| 2022-08-04 15:45:08 +0200 | <ski> | @hoogle Nu |
| 2022-08-04 15:45:09 +0200 | <lambdabot> | Data.Fix data Nu f |
| 2022-08-04 15:45:09 +0200 | <lambdabot> | Data.Fix Nu :: (a -> f a) -> a -> Nu f |
| 2022-08-04 15:45:09 +0200 | <lambdabot> | Data.ISO3166_CountryCodes NU :: CountryCode |
| 2022-08-04 15:49:29 +0200 | <ski> | (er, s/s -> Nu s/s -> Nu f/) |
| 2022-08-04 15:49:31 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 2022-08-04 15:49:54 +0200 | <siers> | an F-algebra is the "Mu f"? |
| 2022-08-04 15:49:54 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
| 2022-08-04 15:50:23 +0200 | <ski> | no, an `F'-algebra (over carrier `r') is a value of type `F r -> r' |
| 2022-08-04 15:50:33 +0200 | <siers> | alright |
| 2022-08-04 15:50:38 +0200 | <ski> | an `F'-coalgebra (over carrier `s') is a value of type `s -> F s' |
| 2022-08-04 15:50:54 +0200 | <ski> | type Algebra f r = f r -> r |
| 2022-08-04 15:51:04 +0200 | <ski> | type Coalgebra f s = s -> f s |
| 2022-08-04 15:51:06 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-08-04 15:51:11 +0200 | FurudeRika[m] | (~chitandae@user/FurudeRika) |
| 2022-08-04 15:51:16 +0200 | <ski> | (i've seen those type synonyms used, occasionally) |
| 2022-08-04 15:51:50 +0200 | <ski> | cata :: Functor f => Algebra f r -> (Mu r -> r) |
| 2022-08-04 15:52:05 +0200 | <ski> | er |
| 2022-08-04 15:52:08 +0200 | <ski> | cata :: Functor f => Algebra f r -> (Mu f -> r) |
| 2022-08-04 15:52:12 +0200 | <ski> | ana :: Functor f => Coalgebra f s -> (s -> Nu f) |
| 2022-08-04 15:53:48 +0200 | alternateved | (~user@staticline-31-183-149-36.toya.net.pl) (Remote host closed the connection) |
| 2022-08-04 15:56:07 +0200 | VictorHugenay | (~jh@user/VictorHugenay) (Quit: Konversation terminated!) |
| 2022-08-04 15:58:32 +0200 | Furor | Colere |
| 2022-08-04 16:04:27 +0200 | arjun | (~arjun@user/arjun) |
| 2022-08-04 16:10:44 +0200 | Nahra | (~user@static.161.95.99.88.clients.your-server.de) |
| 2022-08-04 16:16:11 +0200 | arjun | (~arjun@user/arjun) (Read error: Connection reset by peer) |
| 2022-08-04 16:16:19 +0200 | arjun_ | (~arjun@user/arjun) |
| 2022-08-04 16:19:00 +0200 | mc47 | (~mc47@xmonad/TheMC47) |
| 2022-08-04 16:20:05 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:8097:2d55:dcdf:fe15) (Ping timeout: 268 seconds) |
| 2022-08-04 16:21:53 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Quit: WeeChat 3.6) |
| 2022-08-04 16:22:01 +0200 | razetime | (~quassel@117.254.34.168) |
| 2022-08-04 16:26:11 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-08-04 16:27:17 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-08-04 16:27:37 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 16:29:00 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-08-04 16:29:10 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 16:37:42 +0200 | kenran | (~kenran@p200300df770eae00d275524cc766554f.dip0.t-ipconnect.de) (Quit: WeeChat info:version) |
| 2022-08-04 16:40:54 +0200 | gurkenglas | (~gurkengla@p57b8a60f.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2022-08-04 16:42:41 +0200 | yvan-sraka | (~yvan-srak@3.red-2-138-130.dynamicip.rima-tde.net) |
| 2022-08-04 16:44:14 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 240 seconds) |
| 2022-08-04 16:46:31 +0200 | zebrag | (~chris@user/zebrag) |
| 2022-08-04 16:46:42 +0200 | sandy_doo | (~sandydoo@146.70.117.210) (Ping timeout: 245 seconds) |
| 2022-08-04 16:50:38 +0200 | zmt00 | (~zmt00@user/zmt00) (Quit: Leaving) |
| 2022-08-04 16:51:18 +0200 | Guest55 | (~Guest55@c-71-198-235-211.hsd1.ca.comcast.net) (Quit: Client closed) |
| 2022-08-04 16:54:21 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 2022-08-04 16:54:21 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-08-04 16:54:21 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2022-08-04 16:54:21 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) (Write error: Connection reset by peer) |
| 2022-08-04 16:54:21 +0200 | noteness | (~noteness@user/noteness) (Write error: Connection reset by peer) |
| 2022-08-04 16:54:54 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2022-08-04 16:54:56 +0200 | noteness | (~noteness@user/noteness) |
| 2022-08-04 16:55:02 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 16:55:02 +0200 | ski | (~ski@ext-1-213.eduroam.chalmers.se) (Ping timeout: 245 seconds) |
| 2022-08-04 16:55:08 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
| 2022-08-04 16:55:11 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-08-04 16:55:39 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-08-04 17:02:24 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 2022-08-04 17:03:08 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 17:04:26 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 17:04:47 +0200 | zmt00 | (~zmt00@user/zmt00) |
| 2022-08-04 17:05:51 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-08-04 17:08:09 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 17:08:11 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Ping timeout: 268 seconds) |
| 2022-08-04 17:08:38 +0200 | Pickchea | (~private@user/pickchea) (Ping timeout: 240 seconds) |
| 2022-08-04 17:09:32 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-08-04 17:09:54 +0200 | pgib | (~textual@173.38.117.85) |
| 2022-08-04 17:12:30 +0200 | yvan-sraka | (~yvan-srak@3.red-2-138-130.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 2022-08-04 17:15:50 +0200 | acidjnk | (~acidjnk@p200300d6e7058699cc6cce398877ca6f.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2022-08-04 17:16:34 +0200 | jakalx | (~jakalx@base.jakalx.net) () |
| 2022-08-04 17:18:23 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 17:19:44 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-08-04 17:22:32 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 245 seconds) |
| 2022-08-04 17:27:32 +0200 | razetime | (~quassel@117.254.34.168) (Ping timeout: 245 seconds) |
| 2022-08-04 17:28:47 +0200 | kuribas` | (~user@silversquare.silversquare.eu) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2022-08-04 17:29:28 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 17:29:48 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 17:32:43 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Remote host closed the connection) |
| 2022-08-04 17:33:00 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) |
| 2022-08-04 17:33:18 +0200 | naso | (~naso@193-116-244-197.tpgi.com.au) (Client Quit) |
| 2022-08-04 17:36:58 +0200 | autophagian | (~mika@ip5f5bf3a3.dynamic.kabel-deutschland.de) (Quit: leaving) |
| 2022-08-04 17:38:23 +0200 | razetime | (~quassel@117.254.34.223) |
| 2022-08-04 17:39:20 +0200 | irfan | (~irfan@user/irfan) (Quit: leaving) |
| 2022-08-04 17:39:55 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-08-04 17:44:10 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2022-08-04 17:44:10 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-08-04 17:44:38 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 17:44:40 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-08-04 17:45:42 +0200 | gmg | (~user@user/gehmehgeh) |
| 2022-08-04 17:49:49 +0200 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 2022-08-04 17:52:03 +0200 | zmt00 | (~zmt00@user/zmt00) (Read error: Connection reset by peer) |
| 2022-08-04 17:59:44 +0200 | zxx7529 | (~Thunderbi@user/zxx7529) (Quit: zxx7529) |
| 2022-08-04 18:01:16 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2022-08-04 18:05:02 +0200 | vglfr | (~vglfr@194.9.14.33) (Ping timeout: 245 seconds) |
| 2022-08-04 18:08:19 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2022-08-04 18:08:49 +0200 | gmg | (~user@user/gehmehgeh) |
| 2022-08-04 18:11:49 +0200 | nek0 | (~nek0@2a01:4f8:222:2b41::12) |
| 2022-08-04 18:15:35 +0200 | razetime | (~quassel@117.254.34.223) (Remote host closed the connection) |
| 2022-08-04 18:23:25 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 18:24:16 +0200 | zmt00 | (~zmt00@user/zmt00) |
| 2022-08-04 18:24:43 +0200 | Inst | (~Inst@2601:6c4:4080:3f80:59d6:821b:713c:d1d9) |
| 2022-08-04 18:25:07 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2022-08-04 18:25:49 +0200 | <Inst> | also, re GHC, are there any fundamental issues with say, a language extensions adding ditto marks? i.e, two backticks unseparated indicate an argument that copies the argument on a top-level pattern match above it? |
| 2022-08-04 18:25:56 +0200 | <Inst> | ex: Fun arg arg2 |
| 2022-08-04 18:26:01 +0200 | <Inst> | fun `` `` |
| 2022-08-04 18:26:38 +0200 | <Inst> | what about subcasing? I.e, within a case expression, if I want to say, case x of.... then I can say pure of, then the second of triggers a subcase |
| 2022-08-04 18:26:58 +0200 | <Inst> | every result within the subcase now has a pure appended to its front |
| 2022-08-04 18:27:42 +0200 | <Inst> | alternatively, fun of Pattern, everything within the subcase now presumes the pattern as a prefix |
| 2022-08-04 18:27:57 +0200 | <Inst> | i guess it's very imperative, i.e, got a problem, add syntax |
| 2022-08-04 18:29:10 +0200 | acidjnk | (~acidjnk@p200300d6e705869994ba3201910e432a.dip0.t-ipconnect.de) |
| 2022-08-04 18:36:13 +0200 | ghn1 | (~Thunderbi@2603-6081-4900-4100-5031-9898-5d51-6f66.res6.spectrum.com) |
| 2022-08-04 18:36:42 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-08-04 18:39:47 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-a96a-49d4-1800-c7da.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 2022-08-04 18:39:48 +0200 | ghn1 | ghn |
| 2022-08-04 18:42:32 +0200 | MajorBiscuit | (~MajorBisc@c-001-031-013.client.tudelft.eduvpn.nl) (Ping timeout: 245 seconds) |
| 2022-08-04 18:43:37 +0200 | benin0 | (~benin@183.82.25.146) (Ping timeout: 268 seconds) |
| 2022-08-04 18:44:04 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 2022-08-04 18:44:29 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) |
| 2022-08-04 18:54:26 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) (Quit: Leaving.) |
| 2022-08-04 18:55:30 +0200 | obabo | (~obabo@2E8BF8F7.catv.pool.telekom.hu) (Quit: WeeChat 3.6) |
| 2022-08-04 19:00:39 +0200 | caubert_ | (~caubert@user/caubert) (Quit: WeeChat 3.5) |
| 2022-08-04 19:00:48 +0200 | caubert | (~caubert@user/caubert) |
| 2022-08-04 19:02:25 +0200 | <geekosaur[m]> | It's what everyone else seems to do (see MultiWayIf) |
| 2022-08-04 19:03:47 +0200 | surgeon | (~surge9nma@2001:470:69fc:105::f585) |
| 2022-08-04 19:04:45 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-08-04 19:04:58 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-08-04 19:05:59 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 19:08:05 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 19:09:26 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
| 2022-08-04 19:09:30 +0200 | euandreh | (~euandreh@179.214.113.107) (Quit: WeeChat 3.6) |
| 2022-08-04 19:10:41 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 19:12:32 +0200 | <geekosaur> | or RecordDotSyntax which I personally think was a mistake |
| 2022-08-04 19:19:21 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2022-08-04 19:23:47 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 2022-08-04 19:30:38 +0200 | Ram-Z | (~Ram-Z@li1814-254.members.linode.com) (Ping timeout: 268 seconds) |
| 2022-08-04 19:30:59 +0200 | AlexNoo_ | (~AlexNoo@94.233.241.233) |
| 2022-08-04 19:32:32 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 19:32:38 +0200 | AlexZenon | (~alzenon@178.34.150.131) (Ping timeout: 240 seconds) |
| 2022-08-04 19:34:38 +0200 | Alex_test | (~al_test@178.34.150.131) (Ping timeout: 240 seconds) |
| 2022-08-04 19:34:57 +0200 | AlexNoo | (~AlexNoo@178.34.150.131) (Ping timeout: 268 seconds) |
| 2022-08-04 19:35:27 +0200 | benin0 | (~benin@2401:4900:2323:8106:8928:2ec0:5649:e0a1) |
| 2022-08-04 19:36:20 +0200 | AlexNoo_ | AlexNoo |
| 2022-08-04 19:36:30 +0200 | AlexZenon | (~alzenon@94.233.241.233) |
| 2022-08-04 19:38:33 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 19:39:10 +0200 | vglfr | (~vglfr@194.9.14.33) (Read error: Connection reset by peer) |
| 2022-08-04 19:39:35 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 2022-08-04 19:39:52 +0200 | Alex_test | (~al_test@94.233.241.233) |
| 2022-08-04 19:40:46 +0200 | benin0 | (~benin@2401:4900:2323:8106:8928:2ec0:5649:e0a1) (Quit: The Lounge - https://thelounge.chat) |
| 2022-08-04 19:41:16 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) |
| 2022-08-04 19:42:51 +0200 | mbuf | (~Shakthi@122.165.55.71) (Quit: Leaving) |
| 2022-08-04 19:43:22 +0200 | shriekingnoise | (~shrieking@186.137.167.202) |
| 2022-08-04 19:43:52 +0200 | byorgey | (~byorgey@155.138.238.211) (Remote host closed the connection) |
| 2022-08-04 19:48:51 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 2022-08-04 19:48:51 +0200 | wroathe | (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 2022-08-04 19:48:51 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2022-08-04 19:48:51 +0200 | zero | (~z@user/zero) |
| 2022-08-04 19:49:23 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2022-08-04 19:49:47 +0200 | zero | yin |
| 2022-08-04 19:49:51 +0200 | fserucas_ | (~fserucas@83.223.235.72) (Quit: Leaving) |
| 2022-08-04 19:50:56 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 19:57:35 +0200 | stefan-_ | (~cri@42dots.de) (Ping timeout: 260 seconds) |
| 2022-08-04 19:58:50 +0200 | noteness | (~noteness@user/noteness) (Remote host closed the connection) |
| 2022-08-04 19:59:48 +0200 | noteness | (~noteness@user/noteness) |
| 2022-08-04 20:02:57 +0200 | Ram-Z | (~Ram-Z@li1814-254.members.linode.com) |
| 2022-08-04 20:05:02 +0200 | stefan-_ | (~cri@42dots.de) |
| 2022-08-04 20:05:26 +0200 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 2022-08-04 20:05:51 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2022-08-04 20:06:02 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2022-08-04 20:06:02 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 2022-08-04 20:06:02 +0200 | noteness | (~noteness@user/noteness) (Write error: Broken pipe) |
| 2022-08-04 20:06:02 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2022-08-04 20:06:02 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-08-04 20:06:24 +0200 | noteness | (~noteness@user/noteness) |
| 2022-08-04 20:06:33 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2022-08-04 20:06:37 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
| 2022-08-04 20:06:45 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 20:06:49 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2022-08-04 20:06:52 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 2022-08-04 20:07:06 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2022-08-04 20:10:32 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 255 seconds) |
| 2022-08-04 20:10:33 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-08-04 20:10:52 +0200 | noteness | (~noteness@user/noteness) (Remote host closed the connection) |
| 2022-08-04 20:11:16 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 20:11:38 +0200 | noteness | (~noteness@user/noteness) |
| 2022-08-04 20:13:25 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2022-08-04 20:17:10 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-08-04 20:18:37 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 20:20:26 +0200 | Kaiepi | (~Kaiepi@156.34.47.253) (Ping timeout: 268 seconds) |
| 2022-08-04 20:21:08 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2022-08-04 20:21:16 +0200 | coot | (~coot@213.134.176.158) (Quit: coot) |
| 2022-08-04 20:21:40 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2022-08-04 20:22:47 +0200 | coot | (~coot@213.134.176.158) |
| 2022-08-04 20:22:47 +0200 | coot | (~coot@213.134.176.158) (Remote host closed the connection) |
| 2022-08-04 20:22:48 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 2022-08-04 20:22:53 +0200 | arjun_ | (~arjun@user/arjun) (Remote host closed the connection) |
| 2022-08-04 20:23:29 +0200 | causal | (~user@50.35.83.177) |
| 2022-08-04 20:25:22 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 268 seconds) |
| 2022-08-04 20:27:20 +0200 | Guest55 | (~Guest55@c-71-198-235-211.hsd1.ca.comcast.net) |
| 2022-08-04 20:28:45 +0200 | econo | (uid147250@user/econo) |
| 2022-08-04 20:30:05 +0200 | foul_owl | (~kerry@23.82.194.108) (Ping timeout: 252 seconds) |
| 2022-08-04 20:39:57 +0200 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 2022-08-04 20:41:05 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 20:42:23 +0200 | Cale | (~cale@cpef48e38ee8583-cm30b7d4b3fc20.cpe.net.cable.rogers.com) (Read error: Connection reset by peer) |
| 2022-08-04 20:42:37 +0200 | Cale | (~cale@cpef48e38ee8583-cm30b7d4b3fc20.cpe.net.cable.rogers.com) |
| 2022-08-04 20:43:42 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-08-04 20:48:53 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 268 seconds) |
| 2022-08-04 20:49:16 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 20:49:56 +0200 | <qrpnxz> | i don't know why multiwayif exists |
| 2022-08-04 20:50:12 +0200 | <qrpnxz> | is it cheaper than case () of? |
| 2022-08-04 20:50:21 +0200 | <Cale> | no |
| 2022-08-04 20:50:32 +0200 | <geekosaur> | no, and iirc it's just sugar for that |
| 2022-08-04 20:51:07 +0200 | <qrpnxz> | well actually, if you use that other if extension dothenifmorewordsoup, then the advantage is you can remove nesting probably |
| 2022-08-04 20:51:22 +0200 | <qrpnxz> | otherwise case will do |
| 2022-08-04 20:51:30 +0200 | <Cale> | which one? |
| 2022-08-04 20:51:35 +0200 | <qrpnxz> | let me look |
| 2022-08-04 20:51:53 +0200 | <qrpnxz> | DoAndIfThenElse |
| 2022-08-04 20:52:13 +0200 | <Cale> | oh, that just... that one is gross, and turned on by default, but useless |
| 2022-08-04 20:52:59 +0200 | <qrpnxz> | very useful to me, i was confused as hell when i compiled something and it wasn't implicit |
| 2022-08-04 20:53:06 +0200 | <Cale> | It lets you put semicolons in the middle of your if expressions so that if you happened to indent them incorrectly inside a do-block, you won't get bitten for it |
| 2022-08-04 20:53:20 +0200 | <Cale> | If you indent them like: |
| 2022-08-04 20:53:23 +0200 | <Cale> | if condition |
| 2022-08-04 20:53:26 +0200 | <Cale> | then foo |
| 2022-08-04 20:53:29 +0200 | <Cale> | else bar |
| 2022-08-04 20:53:33 +0200 | <Cale> | then you don't need it |
| 2022-08-04 20:53:39 +0200 | <Cale> | and also your code is nicer |
| 2022-08-04 20:54:29 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 20:54:30 +0200 | <qrpnxz> | yeah, i legit had to guess that, but see that adds nesting, sometimes you want nesting, sometimes you don't. By removing the nesting i can write neat if cond then return _ else do |
| 2022-08-04 20:54:39 +0200 | <qrpnxz> | and then keep at the same nest level |
| 2022-08-04 20:54:50 +0200 | <Cale> | terrible :) |
| 2022-08-04 20:55:10 +0200 | <qrpnxz> | not terrible, that's rather common in imperative code |
| 2022-08-04 20:55:14 +0200 | <Cale> | They do that kind of thing in the GHC source code in various places, and it actually makes things hard to read |
| 2022-08-04 20:55:30 +0200 | <Cale> | Knowing that there's an early exit is important. |
| 2022-08-04 20:56:10 +0200 | <Cale> | Being able to visually tell that by looking at indentation is good, but once you start breaking that expectation, you have to scrutinize every do-block carefully |
| 2022-08-04 20:57:00 +0200 | <Cale> | Like, in a long function, I might not know that I'm in one branch of a conditional, and be trying to add behaviour that applies all the time |
| 2022-08-04 20:57:47 +0200 | <qrpnxz> | i think i get what you are getting at. Because in haskell return doesn't actually shortcut (indeed that then part may not even *say* return, it's just a monad expression), then the hint that it was returning is the "else do" bit rather than a "return" keyword |
| 2022-08-04 20:58:16 +0200 | <geekosaur> | yep, but that just makes it doubly confusing |
| 2022-08-04 20:58:26 +0200 | <qrpnxz> | but for me this is a minor difference. Different languages are different |
| 2022-08-04 20:58:31 +0200 | <Cale> | Yeah, because nothing otherwise can break out of a do-block before the end apart from an exception |
| 2022-08-04 20:58:48 +0200 | <geekosaur> | I agree with Cale, I want to see that the else leg is actually under a conditional |
| 2022-08-04 20:59:02 +0200 | <geekosaur> | and indentation would tell me that |
| 2022-08-04 20:59:04 +0200 | <Cale> | (or calling the function that callCC handed you, if you're in ContT or something, but you never are) |
| 2022-08-04 20:59:12 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 245 seconds) |
| 2022-08-04 20:59:45 +0200 | <Cale> | You get used to being able to see do-blocks as things that usually run to completion. |
| 2022-08-04 20:59:49 +0200 | <qrpnxz> | yeah in callCC then you can do `when cond (k _)` |
| 2022-08-04 21:02:59 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 2022-08-04 21:06:09 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 21:07:39 +0200 | _xor | (~xor@74.215.182.83) (Quit: WeeChat 3.0) |
| 2022-08-04 21:08:41 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2022-08-04 21:09:06 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 2022-08-04 21:09:44 +0200 | kenran | (~kenran@200116b82be9c900b06c95caadc7b21a.dip.versatel-1u1.de) |
| 2022-08-04 21:09:47 +0200 | sandy_doo | (~sandydoo@146.70.117.210) |
| 2022-08-04 21:12:21 +0200 | kenran | (~kenran@200116b82be9c900b06c95caadc7b21a.dip.versatel-1u1.de) (Client Quit) |
| 2022-08-04 21:23:25 +0200 | <qrpnxz> | i was thinking of how do i make a type of optic that will let me do effects as i traverse, and i just realized that profunctor optics already allow that!! |
| 2022-08-04 21:26:05 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-08-04 21:26:44 +0200 | ghn1 | (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) |
| 2022-08-04 21:27:16 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 21:28:07 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 21:28:50 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-5031-9898-5d51-6f66.res6.spectrum.com) (Ping timeout: 255 seconds) |
| 2022-08-04 21:28:55 +0200 | ghn1 | ghn |
| 2022-08-04 21:30:33 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 21:31:59 +0200 | <qrpnxz> | or maybe van laarhoven would have suffised for what i just tested with. I'm trying to work with mutable containers in a lensy way but it's not super great. I can make something like `(a -> ST s a) -> c -> ST s c`, which is useful, but i want to do other effects as i traverse, so i thought of doing something like it's polymorphic on the transformer `forall t. (MonadTrans t) => (a -> t (ST s) a) -> |
| 2022-08-04 21:32:01 +0200 | <qrpnxz> | c -> t (ST s) c` and that's pretty neat. Bit limited though because the last param can't be phantom, sinse `t m` is a Monad, so really maybe the optimal would be something that's an "Applicative transformer", but would that not just be: `forall f. Applicative f => (a -> Compose f (ST s) a) -> c -> Compose f (ST s) c`? that could work |
| 2022-08-04 21:32:21 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-08-04 21:35:03 +0200 | vglfr | (~vglfr@194.9.14.33) (Ping timeout: 268 seconds) |
| 2022-08-04 21:35:55 +0200 | ghn1 | (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) |
| 2022-08-04 21:36:16 +0200 | vglfr | (~vglfr@194.9.14.33) |
| 2022-08-04 21:37:07 +0200 | ghn1 | (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) (Client Quit) |
| 2022-08-04 21:37:31 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 2022-08-04 21:37:46 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 21:38:29 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) |
| 2022-08-04 21:39:25 +0200 | coot | (~coot@213.134.176.158) |
| 2022-08-04 21:44:31 +0200 | coot | (~coot@213.134.176.158) (Ping timeout: 252 seconds) |
| 2022-08-04 21:45:42 +0200 | <qrpnxz> | or actually i'm stuck in monad land because i need to pass the value from the editor to the write action. Hell, even just to pass the value from read to the editor i need bind I think. Switching order to Compose (ST s) f may be more workable |
| 2022-08-04 21:46:39 +0200 | <qrpnxz> | and actually that makes more sense, because the effect is on the value in the context of ST, not on the ST context itself |
| 2022-08-04 21:48:42 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) |
| 2022-08-04 21:50:32 +0200 | ghn1 | (~Thunderbi@2603-6081-4900-4100-a593-ff41-38de-2384.res6.spectrum.com) |
| 2022-08-04 21:50:51 +0200 | azimut_ | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 21:51:10 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 268 seconds) |
| 2022-08-04 21:53:01 +0200 | ghn | (~Thunderbi@2603-6081-4900-4100-d44c-313c-3d0d-87f2.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 2022-08-04 21:53:02 +0200 | ghn1 | ghn |
| 2022-08-04 22:01:32 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 22:01:44 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2022-08-04 22:03:05 +0200 | coot | (~coot@213.134.176.158) |
| 2022-08-04 22:04:49 +0200 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 2022-08-04 22:05:56 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-08-04 22:07:24 +0200 | Kaiepi | (~Kaiepi@156.34.47.253) |
| 2022-08-04 22:09:17 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2022-08-04 22:13:37 +0200 | FragByte | (~christian@user/fragbyte) (Quit: Quit) |
| 2022-08-04 22:13:47 +0200 | eggplantade | (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 245 seconds) |
| 2022-08-04 22:15:48 +0200 | FragByte | (~christian@user/fragbyte) |
| 2022-08-04 22:17:07 +0200 | sandy_doo | (~sandydoo@146.70.117.210) (Ping timeout: 245 seconds) |
| 2022-08-04 22:18:28 +0200 | zeenk | (~zeenk@2a02:2f04:a311:2d00:6865:d863:4c93:799f) |
| 2022-08-04 22:19:04 +0200 | pavonia | (~user@user/siracusa) |
| 2022-08-04 22:23:02 +0200 | <qrpnxz> | ah! if i create a new array in the process, then i get an honest to goodness traversal, with the only difference being that instead of taking an editor in (->) and returning one in (->), i take one in (Kleisli m) and return another one in (Kleisli m). So for example I can do `(a -> ST s (f b)) -> STArray i a -> ST s (f (Array i b))` :) |
| 2022-08-04 22:26:01 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 2022-08-04 22:26:11 +0200 | johnw | (~johnw@2600:1700:cf00:db0:4977:125:61ab:9934) |
| 2022-08-04 22:28:29 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 22:29:07 +0200 | jmd_ | (~jmdaemon@user/jmdaemon) |
| 2022-08-04 22:29:30 +0200 | <johnw> | is there a Haskell library that, via template Haskell or some such, can transform an ADT into its type of one-hole contexts? I.e., create the derivative of a data type? |
| 2022-08-04 22:29:59 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 252 seconds) |
| 2022-08-04 22:30:00 +0200 | <qrpnxz> | idk, but you can zip any structure you have a traversal to with https://hackage.haskell.org/package/zippers |
| 2022-08-04 22:30:18 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 22:30:41 +0200 | <qrpnxz> | see also https://hackage.haskell.org/package/lens-5.1.1/docs/Control-Lens-Plated.html and https://hackage.haskell.org/package/lens-5.1.1/docs/Control-Lens-Traversal.html#g:4 |
| 2022-08-04 22:31:08 +0200 | <qrpnxz> | johnw |
| 2022-08-04 22:32:13 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2022-08-04 22:32:31 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2022-08-04 22:34:59 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-08-04 22:36:11 +0200 | titibandit | (~titibandi@xdsl-78-35-214-18.nc.de) (Remote host closed the connection) |
| 2022-08-04 22:40:00 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 22:41:36 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) (Ping timeout: 244 seconds) |
| 2022-08-04 22:44:14 +0200 | zer0bitz | (~zer0bitz@2001:2003:f748:2000:f402:7db0:5697:8cad) (Ping timeout: 240 seconds) |
| 2022-08-04 22:48:22 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-08-04 22:49:27 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 22:50:18 +0200 | Milan | (~Milan@46.245.118.112) |
| 2022-08-04 22:51:25 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 244 seconds) |
| 2022-08-04 22:53:52 +0200 | <EvanR_> | johnw, that sounds like automatic differentiation, going just by the title |
| 2022-08-04 22:55:04 +0200 | <geekosaur> | different kind of differentiation, I think |
| 2022-08-04 22:55:28 +0200 | <geekosaur> | AD is value level, one-hole contexts is type level? |
| 2022-08-04 22:55:52 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) |
| 2022-08-04 22:56:17 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-231.elisa-laajakaista.fi) |
| 2022-08-04 22:56:44 +0200 | <EvanR_> | man that might explain why I never got differentiation xD |
| 2022-08-04 22:57:09 +0200 | EvanR_ | EvanR |
| 2022-08-04 23:00:52 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 23:02:22 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-08-04 23:06:28 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-08-04 23:07:26 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 244 seconds) |
| 2022-08-04 23:07:33 +0200 | ubert | (~Thunderbi@77.119.221.71.wireless.dyn.drei.com) (Ping timeout: 268 seconds) |
| 2022-08-04 23:07:53 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 2022-08-04 23:11:25 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
| 2022-08-04 23:14:38 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-08-04 23:17:50 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 240 seconds) |
| 2022-08-04 23:18:19 +0200 | jero98772 | (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) |
| 2022-08-04 23:18:57 +0200 | phma_ | (~phma@host-67-44-208-30.hnremote.net) |
| 2022-08-04 23:19:45 +0200 | phma | (phma@2001:5b0:211b:ae28:2ee:ca83:26d:80f2) (Read error: Connection reset by peer) |
| 2022-08-04 23:19:51 +0200 | <johnw> | the reason I'm wondering about this is because yesterday, I wanted the dual of a lens: a diffuser |
| 2022-08-04 23:20:02 +0200 | <johnw> | dual in a different sense than lens/prism |
| 2022-08-04 23:21:18 +0200 | <johnw> | if a Lens' s a is a "focus" into some structure 's' that lets you work with 'a', a Diffuser' s a is an "abstraction" from some structure 's' to its one-hole contexts around 'a'. Why would I want this? Because if I had a diffuser 'diff', I could do `x ^. diff == y ^. diff`, and be able to know very easily whether everything *but* the value at 'a' is equal. |
| 2022-08-04 23:23:54 +0200 | <geekosaur> | that almost sounds like a comonadic lens |
| 2022-08-04 23:23:55 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) |
| 2022-08-04 23:24:04 +0200 | <johnw> | actually, it really does |
| 2022-08-04 23:24:10 +0200 | <geekosaur> | and I note Control.Lens.Internal.Context appears to support that |
| 2022-08-04 23:25:13 +0200 | coot | (~coot@213.134.176.158) (Quit: coot) |
| 2022-08-04 23:28:38 +0200 | merijn | (~merijn@c-001-001-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds) |
| 2022-08-04 23:30:05 +0200 | <johnw> | a Context gets very close, but it doesn't yield the one-hole context that might actually be comparable. Instead, it encodes a functional variant of the one-hole context in the form of (a -> s) |
| 2022-08-04 23:30:32 +0200 | <johnw> | I suppose if I have an 'a' in hand, I can just use it on the two contexts and then compare |
| 2022-08-04 23:30:48 +0200 | <johnw> | but that doesn't work in cases where 'a' is incomparable but the rest of the context is |
| 2022-08-04 23:31:18 +0200 | Etxeberrialex[m] | (~etxeberri@2001:470:69fc:105::1:5ae6) |
| 2022-08-04 23:31:30 +0200 | Etxeberrialex[m] | (~etxeberri@2001:470:69fc:105::1:5ae6) () |
| 2022-08-04 23:32:30 +0200 | phma_ | phma |
| 2022-08-04 23:32:45 +0200 | Inst | (~Inst@2601:6c4:4080:3f80:59d6:821b:713c:d1d9) (Ping timeout: 244 seconds) |
| 2022-08-04 23:35:51 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-08-04 23:43:50 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Write error: Connection reset by peer) |
| 2022-08-04 23:43:50 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) (Write error: Broken pipe) |
| 2022-08-04 23:43:50 +0200 | noteness | (~noteness@user/noteness) (Read error: Connection reset by peer) |
| 2022-08-04 23:43:50 +0200 | azimut_ | (~azimut@gateway/tor-sasl/azimut) (Read error: Connection reset by peer) |
| 2022-08-04 23:43:50 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Read error: Connection reset by peer) |
| 2022-08-04 23:44:10 +0200 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
| 2022-08-04 23:44:14 +0200 | noteness | (~noteness@user/noteness) |
| 2022-08-04 23:44:27 +0200 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2022-08-04 23:44:27 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-08-04 23:44:32 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-08-04 23:45:56 +0200 | MajorBiscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 268 seconds) |
| 2022-08-04 23:47:44 +0200 | MajorBiscuit | (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 2022-08-04 23:57:53 +0200 | morrow | (~user@bzq-110-168-31-106.red.bezeqint.net) |