| 2023-11-10 00:01:07 +0100 | mechap | (~mechap@user/mechap) (Ping timeout: 264 seconds) |
| 2023-11-10 00:03:54 +0100 | koala_man | (~vidar@157.146.251.23.bc.googleusercontent.com) (Server closed connection) |
| 2023-11-10 00:04:05 +0100 | koala_man | (~vidar@157.146.251.23.bc.googleusercontent.com) |
| 2023-11-10 00:09:01 +0100 | fendor | (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) |
| 2023-11-10 00:12:07 +0100 | zer0bitz | (~zer0bitz@user/zer0bitz) |
| 2023-11-10 00:12:46 +0100 | <Unicorn_Princess> | https://hackage.haskell.org/package/unix says the maintainer is three dudes, but https://hackage.haskell.org/package/unix-2.8.3.0/docs/System-Posix.html says it's libraries@haskell.org. what's going on? and how can i tell which packages on hackage are "official", and which come from random blokes? |
| 2023-11-10 00:17:46 +0100 | fendor | (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Remote host closed the connection) |
| 2023-11-10 00:18:20 +0100 | accord | (uid568320@id-568320.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2023-11-10 00:18:55 +0100 | <monochrom> | In this case, fortunately, unix comes with GHC so I just stick to that. :) |
| 2023-11-10 00:19:49 +0100 | <yushyin> | the first link fetches the info from the cabal file, the second link from the source file, i guess. |
| 2023-11-10 00:20:43 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds) |
| 2023-11-10 00:22:55 +0100 | <Unicorn_Princess> | hm. how can i tell what comes with ghc, and whether i'm using the (local?) ghc version, or fetching something from hackage? |
| 2023-11-10 00:24:51 +0100 | remedan | (~remedan@ip-94-112-0-18.bb.vodafone.cz) |
| 2023-11-10 00:25:35 +0100 | <geekosaur> | ghc-pkg list --global |
| 2023-11-10 00:26:35 +0100 | <geekosaur> | (unless you get your ghc from OS packages in which case the global db probably has a lot of other gunk in it) |
| 2023-11-10 00:27:19 +0100 | <monochrom> | Or a lot fewer! Some linux distros like to split hair. |
| 2023-11-10 00:27:29 +0100 | <geekosaur> | and in that case https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-history is the best you'll do |
| 2023-11-10 00:28:10 +0100 | <Unicorn_Princess> | hmm, thanks |
| 2023-11-10 00:29:49 +0100 | <geekosaur> | as for the maintainers, libraries@ has responsibility but the actual work is generally done by the people listed in the cabal file (and the hackage page) |
| 2023-11-10 00:30:01 +0100 | neptun | (neptun@2607:5300:60:5910:dcad:beff:feef:5bc) (Server closed connection) |
| 2023-11-10 00:30:13 +0100 | neptun | (neptun@2607:5300:60:5910:dcad:beff:feef:5bc) |
| 2023-11-10 00:30:26 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2023-11-10 00:30:58 +0100 | <geekosaur> | so they're not really "random people", they're working under the purview of libraries@ |
| 2023-11-10 00:33:08 +0100 | <geekosaur> | @where versions |
| 2023-11-10 00:33:08 +0100 | <lambdabot> | I know nothing about versions. |
| 2023-11-10 00:33:15 +0100 | <geekosaur> | @where+ versions https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-history |
| 2023-11-10 00:33:15 +0100 | <lambdabot> | I will never forget. |
| 2023-11-10 00:33:41 +0100 | wroathe | (~wroathe@user/wroathe) (Ping timeout: 240 seconds) |
| 2023-11-10 00:35:22 +0100 | Buliarous | (~gypsydang@46.232.210.139) |
| 2023-11-10 00:37:56 +0100 | Jackneill | (~Jackneill@20014C4E1E058A009B5587F4C6A9FB36.dsl.pool.telekom.hu) (Ping timeout: 252 seconds) |
| 2023-11-10 00:39:40 +0100 | Adeon | (sid143283@id-418992.lymington.irccloud.com) (Server closed connection) |
| 2023-11-10 00:39:49 +0100 | Adeon | (sid418992@id-418992.lymington.irccloud.com) |
| 2023-11-10 00:39:54 +0100 | lhpitn_ | (~tn@mail.lebenshilfe-pi.de) |
| 2023-11-10 00:41:02 +0100 | shoggouth | (uid607148@user/shoggouth) (Quit: Connection closed for inactivity) |
| 2023-11-10 00:43:37 +0100 | lhpitn | (~tn@mail.lebenshilfe-pi.de) (Ping timeout: 258 seconds) |
| 2023-11-10 00:52:19 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2023-11-10 00:56:16 +0100 | jappiejappie | (~jappiejap@186-011-158-163.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2023-11-10 00:56:42 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
| 2023-11-10 01:05:40 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 01:19:07 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Ping timeout: 264 seconds) |
| 2023-11-10 01:24:42 +0100 | NemesisD | (sid24071@id-24071.lymington.irccloud.com) (Server closed connection) |
| 2023-11-10 01:24:46 +0100 | ouroboros | (~ouroboros@user/ouroboros) (Ping timeout: 255 seconds) |
| 2023-11-10 01:24:56 +0100 | NemesisD | (sid24071@id-24071.lymington.irccloud.com) |
| 2023-11-10 01:25:48 +0100 | A_Dragon | (A_D@libera/staff/dragon) |
| 2023-11-10 01:26:02 +0100 | ouroboros | (~ouroboros@user/ouroboros) |
| 2023-11-10 01:26:21 +0100 | <Axman6> | geekosaur: <3 Now I just need to remember that's how to find it! |
| 2023-11-10 01:26:34 +0100 | bah | (~bah@l1.tel) (Ping timeout: 255 seconds) |
| 2023-11-10 01:27:19 +0100 | DemonDerg | Guest745 |
| 2023-11-10 01:27:19 +0100 | Guest745 | (A_D@libera/staff/dragon) (Killed (cadmium.libera.chat (Nickname regained by services))) |
| 2023-11-10 01:27:19 +0100 | A_Dragon | DemonDerg |
| 2023-11-10 01:28:39 +0100 | <geekosaur> | So you need a where for the where? |
| 2023-11-10 01:28:55 +0100 | <Axman6> | yeah, but inside my brain |
| 2023-11-10 01:29:21 +0100 | <geekosaur> | Actually sm has a searchable website for lambdabot |
| 2023-11-10 01:29:46 +0100 | <geekosaur> | Haskell-links.org |
| 2023-11-10 01:31:41 +0100 | bah | (~bah@l1.tel) |
| 2023-11-10 01:31:43 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 2023-11-10 01:32:52 +0100 | euleritian | (~euleritia@dynamic-046-114-206-202.46.114.pool.telefonica.de) |
| 2023-11-10 01:33:24 +0100 | <monochrom> | There is a Hong Kong idiom for this issue with key-value stores. OK, the idiom was originally for something else, but this issue is a modern special case. |
| 2023-11-10 01:33:41 +0100 | <monochrom> | The safe with the key lost. |
| 2023-11-10 01:34:41 +0100 | <Axman6> | feels apt |
| 2023-11-10 01:34:56 +0100 | <monochrom> | Likewise for /etc/passwd- but you forgot all the passwords. >:) |
| 2023-11-10 01:35:21 +0100 | <Axman6> | and now we've got an apt update |
| 2023-11-10 01:35:27 +0100 | <Axman6> | or is that an apt upgrade |
| 2023-11-10 01:44:01 +0100 | lhpitn_ | (~tn@mail.lebenshilfe-pi.de) (Ping timeout: 240 seconds) |
| 2023-11-10 01:47:01 +0100 | <haskellbridge> | 06<sm> /me |
| 2023-11-10 01:47:01 +0100 | <haskellbridge> | 06<sm> checks out versions page.. wow that must be fun to edit |
| 2023-11-10 01:51:02 +0100 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 2023-11-10 01:51:02 +0100 | wroathe | (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 2023-11-10 01:51:02 +0100 | wroathe | (~wroathe@user/wroathe) |
| 2023-11-10 01:51:19 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 245 seconds) |
| 2023-11-10 01:52:27 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2023-11-10 01:54:09 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 258 seconds) |
| 2023-11-10 01:59:08 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 258 seconds) |
| 2023-11-10 01:59:49 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2023-11-10 02:02:56 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2023-11-10 02:04:02 +0100 | califax | (~califax@user/califx) |
| 2023-11-10 02:15:05 +0100 | wroathe | (~wroathe@user/wroathe) (Quit: leaving) |
| 2023-11-10 02:23:13 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 02:27:18 +0100 | ddellacosta | (~ddellacos@ool-44c738de.dyn.optonline.net) |
| 2023-11-10 02:28:04 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
| 2023-11-10 02:30:33 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 2023-11-10 02:38:55 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 264 seconds) |
| 2023-11-10 02:40:22 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2023-11-10 02:43:49 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 02:44:55 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 264 seconds) |
| 2023-11-10 02:46:42 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2023-11-10 02:47:57 +0100 | woffs | (3cd46299b2@woffs.de) (Server closed connection) |
| 2023-11-10 02:50:46 +0100 | _xor | (~xor@72.49.195.41) |
| 2023-11-10 02:51:35 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 2023-11-10 02:57:04 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 2023-11-10 03:00:50 +0100 | masterbuilder | (uid626153@user/masterbuilder) (Quit: Connection closed for inactivity) |
| 2023-11-10 03:03:55 +0100 | xff0x | (~xff0x@2405:6580:b080:900:ed3e:a41c:2d9d:c531) (Ping timeout: 258 seconds) |
| 2023-11-10 03:19:22 +0100 | otto_s | (~user@p5de2fe1e.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 2023-11-10 03:21:06 +0100 | otto_s | (~user@p5de2fb17.dip0.t-ipconnect.de) |
| 2023-11-10 03:24:05 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Ping timeout: 240 seconds) |
| 2023-11-10 03:25:31 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 03:30:00 +0100 | tabemann | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Read error: Connection reset by peer) |
| 2023-11-10 03:33:48 +0100 | arkeet | (arkeet@moriya.ca) (Ping timeout: 240 seconds) |
| 2023-11-10 03:34:29 +0100 | arkeet | (arkeet@moriya.ca) |
| 2023-11-10 03:36:35 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 2023-11-10 03:37:49 +0100 | tabemann | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 2023-11-10 03:42:59 +0100 | thegeekinside | (~thegeekin@189.141.80.123) (Ping timeout: 245 seconds) |
| 2023-11-10 03:44:49 +0100 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2023-11-10 03:55:43 +0100 | kimiamania46 | (~b4f4a2ab@user/kimiamania) (Quit: Ping timeout (120 seconds)) |
| 2023-11-10 03:56:02 +0100 | kimiamania46 | (~b4f4a2ab@user/kimiamania) |
| 2023-11-10 03:57:15 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2023-11-10 04:04:28 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 2023-11-10 04:04:28 +0100 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
| 2023-11-10 04:04:28 +0100 | finn_elija | FinnElija |
| 2023-11-10 04:17:36 +0100 | euleritian | (~euleritia@dynamic-046-114-206-202.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2023-11-10 04:17:54 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2023-11-10 04:19:14 +0100 | hgolden_ | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 2023-11-10 04:20:02 +0100 | ystael | (~ystael@user/ystael) (Server closed connection) |
| 2023-11-10 04:20:17 +0100 | ystael | (~ystael@user/ystael) |
| 2023-11-10 04:22:09 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2023-11-10 04:23:15 +0100 | Shock_ | (~shOkEy@77-234-80-134.pool.digikabel.hu) (Server closed connection) |
| 2023-11-10 04:23:22 +0100 | Shock_ | (~shOkEy@77-234-80-134.pool.digikabel.hu) |
| 2023-11-10 04:28:23 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 04:28:56 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
| 2023-11-10 04:36:43 +0100 | edr | (~edr@user/edr) (Quit: Leaving) |
| 2023-11-10 04:42:07 +0100 | iteratee | (~kyle@162.218.222.207) (Remote host closed the connection) |
| 2023-11-10 04:46:05 +0100 | td_ | (~td@i53870905.versanet.de) (Ping timeout: 240 seconds) |
| 2023-11-10 04:47:55 +0100 | td_ | (~td@i5387093F.versanet.de) |
| 2023-11-10 04:52:14 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 2023-11-10 05:00:42 +0100 | fiddlerwoaroof | (~fiddlerwo@user/fiddlerwoaroof) (Server closed connection) |
| 2023-11-10 05:01:19 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2023-11-10 05:01:36 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 05:02:34 +0100 | fiddlerwoaroof | (~fiddlerwo@user/fiddlerwoaroof) |
| 2023-11-10 05:06:13 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 2023-11-10 05:07:08 +0100 | Jon | (jon@dow.land) (Server closed connection) |
| 2023-11-10 05:07:42 +0100 | Jon | (jon@dow.land) |
| 2023-11-10 05:16:19 +0100 | aforemny_ | (~aforemny@2001:9e8:6ccb:5b00:f896:13f1:97ad:eaff) (Ping timeout: 245 seconds) |
| 2023-11-10 05:16:39 +0100 | aforemny | (~aforemny@2001:9e8:6cf3:9f00:3f53:5505:c25d:bb07) |
| 2023-11-10 05:27:15 +0100 | _xor | (~xor@72.49.195.41) (Read error: Connection reset by peer) |
| 2023-11-10 05:28:03 +0100 | _xor | (~xor@72.49.195.41) |
| 2023-11-10 05:31:55 +0100 | thegeekinside | (~thegeekin@189.141.80.123) |
| 2023-11-10 05:35:24 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 05:36:35 +0100 | thegeekinside | (~thegeekin@189.141.80.123) (Ping timeout: 252 seconds) |
| 2023-11-10 05:38:02 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) (Read error: Connection reset by peer) |
| 2023-11-10 05:40:26 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
| 2023-11-10 05:46:10 +0100 | trev | (~trev@user/trev) |
| 2023-11-10 05:47:19 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 2023-11-10 06:08:15 +0100 | sphynx | (~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288) (Server closed connection) |
| 2023-11-10 06:08:28 +0100 | sphynx | (~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288) |
| 2023-11-10 06:09:56 +0100 | apache2 | (apache2@anubis.0x90.dk) (Ping timeout: 272 seconds) |
| 2023-11-10 06:18:14 +0100 | <phma> | How do I find the number of OS threads Haskell is using (the number in +RTS -N)? |
| 2023-11-10 06:19:40 +0100 | iteratee | (~kyle@162.218.222.207) |
| 2023-11-10 06:20:05 +0100 | <monochrom> | GHC.Conc.numCapabilities. See also get/setNumCapabilities. |
| 2023-11-10 06:32:30 +0100 | qqq | (~qqq@92.43.167.61) (Remote host closed the connection) |
| 2023-11-10 06:46:19 +0100 | michalz | (~michalz@185.246.207.205) |
| 2023-11-10 06:57:31 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 264 seconds) |
| 2023-11-10 06:58:41 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2023-11-10 06:59:15 +0100 | euleritian | (~euleritia@dynamic-046-114-206-003.46.114.pool.telefonica.de) |
| 2023-11-10 07:02:34 +0100 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) |
| 2023-11-10 07:03:10 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2023-11-10 07:06:16 +0100 | iteratee | (~kyle@162.218.222.207) (Ping timeout: 246 seconds) |
| 2023-11-10 07:21:22 +0100 | hays | (rootvegeta@fsf/member/hays) (Server closed connection) |
| 2023-11-10 07:21:40 +0100 | euleritian | (~euleritia@dynamic-046-114-206-003.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2023-11-10 07:21:58 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2023-11-10 07:23:18 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2023-11-10 07:30:39 +0100 | haritz | (~hrtz@user/haritz) (Ping timeout: 240 seconds) |
| 2023-11-10 07:31:24 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2023-11-10 07:32:04 +0100 | Lycurgus | (~georg@user/Lycurgus) |
| 2023-11-10 07:33:24 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 258 seconds) |
| 2023-11-10 07:34:22 +0100 | euleritian | (~euleritia@dynamic-046-114-206-003.46.114.pool.telefonica.de) |
| 2023-11-10 07:42:34 +0100 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving) |
| 2023-11-10 07:44:46 +0100 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 246 seconds) |
| 2023-11-10 07:47:19 +0100 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2023-11-10 07:55:54 +0100 | CO2 | (CO2@gateway/vpn/protonvpn/co2) (Ping timeout: 245 seconds) |
| 2023-11-10 07:56:45 +0100 | kosmikus | (~kosmikus@nullzig.kosmikus.org) (Server closed connection) |
| 2023-11-10 07:56:57 +0100 | kosmikus | (~kosmikus@nullzig.kosmikus.org) |
| 2023-11-10 07:59:23 +0100 | acidjnk | (~acidjnk@p200300d6e72b9362d88f3ae5d7ed9705.dip0.t-ipconnect.de) |
| 2023-11-10 08:00:55 +0100 | <albet70> | what's the effect of Select monad? |
| 2023-11-10 08:12:22 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2023-11-10 08:18:33 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 08:22:12 +0100 | euleritian | (~euleritia@dynamic-046-114-206-003.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2023-11-10 08:22:30 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2023-11-10 08:23:16 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
| 2023-11-10 08:26:21 +0100 | phma | (~phma@host-67-44-208-186.hnremote.net) (Read error: Connection reset by peer) |
| 2023-11-10 08:27:23 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2023-11-10 08:27:40 +0100 | yosef` | (~yosef`@user/yosef/x-2947716) |
| 2023-11-10 08:32:21 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2023-11-10 08:36:41 +0100 | kuribas | (~user@2a02:1808:81:9f8d:1b5c:670d:e5d:4fa3) |
| 2023-11-10 08:40:33 +0100 | lortabac | (~lorenzo@2a01:e0a:541:b8f0:504f:9bc8:bd3:5975) |
| 2023-11-10 08:42:21 +0100 | tomku | (~tomku@user/tomku) (Ping timeout: 240 seconds) |
| 2023-11-10 08:44:30 +0100 | tomku | (~tomku@user/tomku) |
| 2023-11-10 08:48:33 +0100 | iteratee | (~kyle@162.218.222.207) |
| 2023-11-10 08:53:37 +0100 | iteratee_ | (~kyle@162.218.222.207) |
| 2023-11-10 08:54:36 +0100 | <[exa]> | albet70: for some kind of backtracking search, but don't ask me how, the referenced papers are way beyond my intuition |
| 2023-11-10 08:54:40 +0100 | iteratee | (~kyle@162.218.222.207) (Ping timeout: 258 seconds) |
| 2023-11-10 08:55:49 +0100 | kuribas | (~user@2a02:1808:81:9f8d:1b5c:670d:e5d:4fa3) (Ping timeout: 246 seconds) |
| 2023-11-10 08:57:15 +0100 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 2023-11-10 08:57:30 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 2023-11-10 09:04:08 +0100 | misterfish | (~misterfis@g250100.upc-g.chello.nl) |
| 2023-11-10 09:05:25 +0100 | notzmv | (~zmv@user/notzmv) |
| 2023-11-10 09:08:39 +0100 | kuribas | (~user@2a02:1808:81:9f8d:2942:2d4:2d9c:91f3) |
| 2023-11-10 09:11:21 +0100 | kuribas` | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2023-11-10 09:12:20 +0100 | kuribas` | (~user@ip-188-118-57-242.reverse.destiny.be) (Read error: Connection reset by peer) |
| 2023-11-10 09:13:07 +0100 | drdo | (~drdo@bl14-14-49.dsl.telepac.pt) (Ping timeout: 264 seconds) |
| 2023-11-10 09:13:17 +0100 | kuribas | (~user@2a02:1808:81:9f8d:2942:2d4:2d9c:91f3) (Ping timeout: 255 seconds) |
| 2023-11-10 09:14:19 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2023-11-10 09:18:49 +0100 | iteratee_ | (~kyle@162.218.222.207) (Ping timeout: 258 seconds) |
| 2023-11-10 09:23:46 +0100 | fendor | (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) |
| 2023-11-10 09:27:41 +0100 | <ncf> | Select is fun. i'd recommend looking at https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ and https://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/ as a starting point |
| 2023-11-10 09:34:17 +0100 | chele | (~chele@user/chele) |
| 2023-11-10 09:41:04 +0100 | zetef | (~quassel@95.77.17.251) |
| 2023-11-10 09:44:47 +0100 | __monty__ | (~toonn@user/toonn) |
| 2023-11-10 09:45:28 +0100 | zetef | (~quassel@95.77.17.251) (Ping timeout: 255 seconds) |
| 2023-11-10 09:51:06 +0100 | zetef | (~quassel@95.77.17.251) |
| 2023-11-10 09:53:33 +0100 | danza | (~francesco@151.43.119.7) |
| 2023-11-10 09:54:18 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 2023-11-10 09:57:22 +0100 | lhpitn_ | (~tn@mail.lebenshilfe-pi.de) |
| 2023-11-10 09:58:32 +0100 | danza | (~francesco@151.43.119.7) (Read error: Connection reset by peer) |
| 2023-11-10 09:59:43 +0100 | drdo | (~drdo@bl14-14-49.dsl.telepac.pt) |
| 2023-11-10 10:02:03 +0100 | alp | (~alp@2001:861:5e02:eff0:ef2c:b8ea:2a7c:3673) |
| 2023-11-10 10:02:17 +0100 | alp | (~alp@2001:861:5e02:eff0:ef2c:b8ea:2a7c:3673) (Changing host) |
| 2023-11-10 10:02:17 +0100 | alp | (~alp@user/alp) |
| 2023-11-10 10:05:19 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2023-11-10 10:05:22 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2023-11-10 10:08:26 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2023-11-10 10:12:43 +0100 | cayley5_ | (~42cayley@user/phileasfogg) (Server closed connection) |
| 2023-11-10 10:13:03 +0100 | cayley42 | (~cayley5@user/phileasfogg) |
| 2023-11-10 10:16:37 +0100 | _xor | (~xor@72.49.195.41) (Read error: Connection reset by peer) |
| 2023-11-10 10:18:56 +0100 | _xor | (~xor@72.49.195.41) |
| 2023-11-10 10:19:45 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Remote host closed the connection) |
| 2023-11-10 10:25:26 +0100 | danse-nr3 | (~danse@151.37.100.136) |
| 2023-11-10 10:25:45 +0100 | zetef | (~quassel@95.77.17.251) (Remote host closed the connection) |
| 2023-11-10 10:29:30 +0100 | mc47 | (~mc47@xmonad/TheMC47) |
| 2023-11-10 10:30:24 +0100 | yosef` | (~yosef`@user/yosef/x-2947716) (Ping timeout: 250 seconds) |
| 2023-11-10 10:32:48 +0100 | Jackneill | (~Jackneill@20014C4E1E058A00D02EFDF46D150C42.dsl.pool.telekom.hu) |
| 2023-11-10 10:34:43 +0100 | ft | (~ft@p4fc2a529.dip0.t-ipconnect.de) (Quit: leaving) |
| 2023-11-10 10:34:52 +0100 | misterfish | (~misterfis@g250100.upc-g.chello.nl) (Ping timeout: 246 seconds) |
| 2023-11-10 10:41:29 +0100 | misterfish | (~misterfis@87.215.131.102) |
| 2023-11-10 10:41:36 +0100 | fendor | (~fendor@2a02:8388:1640:be00:cb6e:46f6:2fe6:1728) (Remote host closed the connection) |
| 2023-11-10 10:41:55 +0100 | fendor | (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) |
| 2023-11-10 10:43:45 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
| 2023-11-10 10:45:25 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 2023-11-10 10:46:11 +0100 | kiriakos | (~kiriakos@p5b03e4a6.dip0.t-ipconnect.de) |
| 2023-11-10 10:47:15 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 10:52:01 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 2023-11-10 10:54:22 +0100 | mechap | (~mechap@user/mechap) |
| 2023-11-10 10:56:12 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 10:56:42 +0100 | troydm | (~troydm@user/troydm) (Ping timeout: 255 seconds) |
| 2023-11-10 10:57:22 +0100 | troydm | (~troydm@user/troydm) |
| 2023-11-10 11:00:08 +0100 | <kuribas> | I couldn't prove (n + 1 = m + 1) -> n = m with just recursion. |
| 2023-11-10 11:00:20 +0100 | <kuribas> | But I can trivially prove succAdd : (n : Nat) -> n + 1 = S n |
| 2023-11-10 11:00:29 +0100 | <kuribas> | Then eqSucc : {m, n : Nat} -> (n + 1 = m + 1) -> n = m; eqSucc prf = inj S $ rewrite (sym $ succAdd n) in rewrite (sym $ succAdd m) in prf |
| 2023-11-10 11:03:46 +0100 | <ncf> | should be doable by induction: the zero case is refl; assume p : n + 1 = m + 1, then inj S p : S (n + 1) = S (m + 1), and this computes to the same thing as S n + 1 = S m + 1 |
| 2023-11-10 11:03:55 +0100 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 246 seconds) |
| 2023-11-10 11:06:09 +0100 | <ncf> | oh, and i guess you need to handle the case where m = 0, n = S n' and vice-versa |
| 2023-11-10 11:06:42 +0100 | _xor | (~xor@72.49.195.41) (Read error: Connection reset by peer) |
| 2023-11-10 11:10:31 +0100 | _xor | (~xor@72.49.195.41) |
| 2023-11-10 11:10:34 +0100 | <ncf> | can idris eliminate absurd clauses where you try to unify 0 against S n ? |
| 2023-11-10 11:13:48 +0100 | <kuribas> | I don't think so, I tried it, but I could not prove eqSucc with only recursion. |
| 2023-11-10 11:13:55 +0100 | <kuribas> | I would need a secondary proof. |
| 2023-11-10 11:14:15 +0100 | <kuribas> | Sure, "0 = S n" is impossible |
| 2023-11-10 11:14:43 +0100 | <kuribas> | You can prove the unprovable with absurd |
| 2023-11-10 11:14:51 +0100 | <kuribas> | Prelude.absurd : Uninhabited t => t -> a |
| 2023-11-10 11:15:29 +0100 | <ncf> | so it can infer Uninhabited (0 = S n) ? |
| 2023-11-10 11:15:30 +0100 | <kuribas> | or if the input is uninhabited, I can just use "impossible" |
| 2023-11-10 11:15:52 +0100 | <kuribas> | ncf: if that's an input, then it is uninhabited. |
| 2023-11-10 11:16:01 +0100 | <kuribas> | You can use the keyword "impossible". |
| 2023-11-10 11:16:08 +0100 | <ncf> | nice |
| 2023-11-10 11:18:32 +0100 | <kuribas> | ncf: your type for inj S p is wrong. |
| 2023-11-10 11:19:09 +0100 | <ncf> | oh uh |
| 2023-11-10 11:19:10 +0100 | <ncf> | i meant cong |
| 2023-11-10 11:20:11 +0100 | <kuribas> | cong S p : 1 + (n + 1) = 1 + (m + 1) |
| 2023-11-10 11:20:31 +0100 | <ncf> | should also be the type of the goal |
| 2023-11-10 11:20:49 +0100 | <ncf> | S n + 1 ≡ S (n + 1) ≡ 1 + (n + 1) |
| 2023-11-10 11:22:23 +0100 | <tomsmeding> | #idris is spilling over |
| 2023-11-10 11:24:20 +0100 | <Rembane> | I'm all for the overflow |
| 2023-11-10 11:24:35 +0100 | <Hecate> | I need named typeclass instances!!! |
| 2023-11-10 11:24:39 +0100 | <Hecate> | I need them!!!! |
| 2023-11-10 11:26:49 +0100 | <ski> | for ? |
| 2023-11-10 11:27:52 +0100 | <Hecate> | servant uses FromHttpApiData, server and client alike |
| 2023-11-10 11:28:31 +0100 | <kuribas> | Hecate: you could use newtypes? |
| 2023-11-10 11:28:40 +0100 | <Hecate> | however "receiving" a certain value on the server is not the same as "receiving" this value from the client |
| 2023-11-10 11:29:56 +0100 | <Hecate> | my main problem is that FromJSON is the place where we do some validation |
| 2023-11-10 11:30:09 +0100 | <Hecate> | receiving data on the server -> yes, good, validate! |
| 2023-11-10 11:30:40 +0100 | <Hecate> | but the server doesn't necessarily send the exact same data, because it erases some fields upon (soft) deleting an entity |
| 2023-11-10 11:30:41 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Ping timeout: 258 seconds) |
| 2023-11-10 11:30:59 +0100 | <Hecate> | so, an empty field in the request payload is bad, but acceptable when sending back data |
| 2023-11-10 11:31:23 +0100 | <Hecate> | there might be a way to replace this empty field with a value that conveys the same intent |
| 2023-11-10 11:33:11 +0100 | <kuribas> | Hecate: use two datatypes for this data, then convert? |
| 2023-11-10 11:38:16 +0100 | <kuribas> | like InFoo and OutFoo. |
| 2023-11-10 11:40:15 +0100 | lhpitn_ | lhpitn |
| 2023-11-10 11:44:15 +0100 | rosco | (~rosco@yp-150-69.tm.net.my) |
| 2023-11-10 11:46:26 +0100 | <Hecate> | yeah I'm going to do some conversion in the client I guess |
| 2023-11-10 11:51:52 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 2023-11-10 11:53:58 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 246 seconds) |
| 2023-11-10 11:54:12 +0100 | tabemann_ | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 2023-11-10 11:55:22 +0100 | tabemann | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Ping timeout: 246 seconds) |
| 2023-11-10 11:57:24 +0100 | woffs | (3cd46299b2@woffs.de) |
| 2023-11-10 12:16:05 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
| 2023-11-10 12:22:03 +0100 | mechap | (~mechap@user/mechap) (Ping timeout: 258 seconds) |
| 2023-11-10 12:28:52 +0100 | mechap | (~mechap@user/mechap) |
| 2023-11-10 12:29:15 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2023-11-10 12:29:37 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2023-11-10 12:40:31 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2023-11-10 12:41:01 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2023-11-10 12:46:17 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2023-11-10 12:47:57 +0100 | rosco | (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal) |
| 2023-11-10 12:49:01 +0100 | mechap | (~mechap@user/mechap) (Ping timeout: 240 seconds) |
| 2023-11-10 13:01:27 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2023-11-10 13:01:54 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2023-11-10 13:03:54 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2023-11-10 13:04:47 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2023-11-10 13:14:11 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 2023-11-10 13:16:31 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2023-11-10 13:21:27 +0100 | _xor | (~xor@72.49.195.41) (Quit: Ping timeout (120 seconds)) |
| 2023-11-10 13:23:53 +0100 | xff0x | (~xff0x@2405:6580:b080:900:451:c5fa:806e:352e) |
| 2023-11-10 13:24:19 +0100 | CO2 | (CO2@gateway/vpn/protonvpn/co2) |
| 2023-11-10 13:26:07 +0100 | fendor | (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) (Remote host closed the connection) |
| 2023-11-10 13:28:41 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 13:28:49 +0100 | danse-nr3 | (~danse@151.37.100.136) (Ping timeout: 246 seconds) |
| 2023-11-10 13:31:22 +0100 | todi | (~todi@p4fd1a3e6.dip0.t-ipconnect.de) |
| 2023-11-10 13:33:09 +0100 | haritz | (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 2023-11-10 13:33:12 +0100 | haritz | (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 2023-11-10 13:33:12 +0100 | haritz | (~hrtz@user/haritz) |
| 2023-11-10 13:53:48 +0100 | vjoki | (~vjoki@2a00:d880:3:1::fea1:9ae) (Server closed connection) |
| 2023-11-10 13:55:02 +0100 | vjoki | (~vjoki@2a00:d880:3:1::fea1:9ae) |
| 2023-11-10 14:03:27 +0100 | nisstyre | (wes@user/nisstyre) (Server closed connection) |
| 2023-11-10 14:03:47 +0100 | nisstyre | (wes@user/nisstyre) |
| 2023-11-10 14:04:50 +0100 | edr | (~edr@user/edr) |
| 2023-11-10 14:05:07 +0100 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2023-11-10 14:05:30 +0100 | alp | (~alp@2001:861:5e02:eff0:2735:1b6e:45d6:b156) |
| 2023-11-10 14:07:04 +0100 | danse-nr3 | (~danse@151.37.96.125) |
| 2023-11-10 14:08:50 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2023-11-10 14:09:13 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2023-11-10 14:13:06 +0100 | tinwood | (~tinwood@canonical/tinwood) (Server closed connection) |
| 2023-11-10 14:13:18 +0100 | tinwood | (~tinwood@general.default.akavanagh.uk0.bigv.io) |
| 2023-11-10 14:13:18 +0100 | tinwood | (~tinwood@general.default.akavanagh.uk0.bigv.io) (Changing host) |
| 2023-11-10 14:13:18 +0100 | tinwood | (~tinwood@canonical/tinwood) |
| 2023-11-10 14:17:11 +0100 | jonrh | (sid5185@id-5185.ilkley.irccloud.com) (Server closed connection) |
| 2023-11-10 14:17:20 +0100 | jonrh | (sid5185@id-5185.ilkley.irccloud.com) |
| 2023-11-10 14:21:49 +0100 | <dminuoso> | 11:30:59 Hecate │ so, an empty field in the request payload is bad, but acceptable when sending back data |
| 2023-11-10 14:21:53 +0100 | <dminuoso> | It really sounds like you want separate types. |
| 2023-11-10 14:22:07 +0100 | <dminuoso> | Taking two different things and trying to give it the same name is.. a bad idea. |
| 2023-11-10 14:22:45 +0100 | dfordvm | (~dfordivam@160.16.87.223.v6.sakura.ne.jp) (Server closed connection) |
| 2023-11-10 14:23:16 +0100 | dfordvm | (~dfordivam@160.16.87.223.v6.sakura.ne.jp) |
| 2023-11-10 14:27:13 +0100 | akegalj | (~akegalj@195.29.107.235) |
| 2023-11-10 14:30:21 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2023-11-10 14:30:38 +0100 | <Hecate> | yep |
| 2023-11-10 14:31:01 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2023-11-10 14:31:53 +0100 | califax | (~califax@user/califx) |
| 2023-11-10 14:35:46 +0100 | doyougnu- | (~doyougnu@45.46.170.68) |
| 2023-11-10 14:36:21 +0100 | doyougnu | (~doyougnu@45.46.170.68) (Ping timeout: 240 seconds) |
| 2023-11-10 14:39:10 +0100 | phma | (phma@2001:5b0:210b:a318:44a0:81b9:3949:19d6) |
| 2023-11-10 14:39:19 +0100 | ubert | (~Thunderbi@178.165.207.175.wireless.dyn.drei.com) (Ping timeout: 255 seconds) |
| 2023-11-10 14:39:21 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 2023-11-10 14:43:24 +0100 | <kuribas> | Or you could make a newtype Out and a newtype In, then make different parsers for each type. |
| 2023-11-10 14:43:24 +0100 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.0.5) |
| 2023-11-10 14:43:40 +0100 | <kuribas> | instance FromJSON (In Foo)... |
| 2023-11-10 14:44:04 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Ping timeout: 246 seconds) |
| 2023-11-10 14:44:05 +0100 | <kuribas> | If you don't mind that a mandatory field can have a Maybe... |
| 2023-11-10 14:44:45 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 14:45:48 +0100 | <exarkun> | you could parameterize on `* -> *` and instantiate with Identity or Maybe |
| 2023-11-10 14:46:16 +0100 | <kuribas> | That's not granular to specific fields. |
| 2023-11-10 14:46:40 +0100 | <exarkun> | I mean, then use the parameter in the fields. |
| 2023-11-10 14:46:43 +0100 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) |
| 2023-11-10 14:46:44 +0100 | <dminuoso> | exarkun: In practice HKDs are horrible for this. |
| 2023-11-10 14:46:53 +0100 | <kuribas> | in haskell |
| 2023-11-10 14:47:15 +0100 | <exarkun> | In what way? |
| 2023-11-10 14:47:43 +0100 | <kuribas> | It adds more complexity that it solves a problem. |
| 2023-11-10 14:48:25 +0100 | <dminuoso> | You suddenly need -1 instances for everything, which not everything has. |
| 2023-11-10 14:48:59 +0100 | <dminuoso> | And its an awkward place to communicate things in. |
| 2023-11-10 14:49:16 +0100 | <dminuoso> | That is, if you read `FooTy Maybe` - it's not clear at all what that even means. |
| 2023-11-10 14:49:21 +0100 | idnar | (sid12240@debian/mithrandi) (Server closed connection) |
| 2023-11-10 14:49:23 +0100 | <dminuoso> | It's an incredibly leaky abstraction |
| 2023-11-10 14:49:30 +0100 | idnar | (sid12240@debian/mithrandi) |
| 2023-11-10 14:49:40 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
| 2023-11-10 14:50:58 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2023-11-10 14:51:23 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2023-11-10 14:51:45 +0100 | <exarkun> | Okay, plausible. Thanks. The solution space in haskell is so large, it's challenging to know which way to go sometimes. |
| 2023-11-10 14:52:48 +0100 | <kuribas> | It's not always necessary to go fully type safe. |
| 2023-11-10 14:53:08 +0100 | <exarkun> | Hey, I wrote Python for 20 years. |
| 2023-11-10 14:53:41 +0100 | <exarkun> | I have some damage to repair. |
| 2023-11-10 14:53:46 +0100 | <kuribas> | Python types are broken for many popular packages, like pandas. |
| 2023-11-10 14:53:51 +0100 | <kuribas> | They should try to type everything. |
| 2023-11-10 14:54:21 +0100 | <exarkun> | Once you realize the type of everything is object, it all works out. |
| 2023-11-10 14:54:38 +0100 | <kuribas> | and everything is a partial function |
| 2023-11-10 14:55:22 +0100 | <exarkun> | so total functions work for all of their inputs, partial functions work for some of their inputs. is there a word for a function that works for none of its inputs? |
| 2023-11-10 14:55:34 +0100 | <kuribas> | uninhabited? |
| 2023-11-10 14:59:11 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2023-11-10 15:00:26 +0100 | <exarkun> | Feels close. I have some dissonance trying to unify "uninhabited" which the idea that the function does exist ... but if it cannot produce any results, does it actually exist? |
| 2023-11-10 15:00:54 +0100 | <kuribas> | it's domain is empty |
| 2023-11-10 15:01:06 +0100 | <kuribas> | I'd say it doesn't exist. |
| 2023-11-10 15:01:38 +0100 | <kuribas> | Or it has one value, bottom? |
| 2023-11-10 15:02:05 +0100 | chomwitt | (~chomwitt@2a02:587:7a1a:4300:1ac0:4dff:fedb:a3f1) |
| 2023-11-10 15:02:18 +0100 | <kuribas> | exarkun: how did you survive python? I am not doing python, _with types_, and it's still hard. |
| 2023-11-10 15:03:06 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2023-11-10 15:03:20 +0100 | <exarkun> | I don't know, advanced myopia maybe. |
| 2023-11-10 15:03:30 +0100 | <kuribas> | s/not/now |
| 2023-11-10 15:03:47 +0100 | <exarkun> | Haskell has definitely decimated my ability to work with Python. |
| 2023-11-10 15:04:01 +0100 | <kuribas> | what is hard is the crazy stuff people do in Python... |
| 2023-11-10 15:04:25 +0100 | <kuribas> | Creating many layers that do nothing, just pass values around and make the whole flow hard to understand. |
| 2023-11-10 15:05:25 +0100 | <exarkun> | A big difference between Python and Haskell that jumps out at me is that in Python you will frequently just re-invent and re-implement basic abstractions and patterns whereas in Haskell you will re-use them. |
| 2023-11-10 15:05:26 +0100 | cbarrett | (sid192934@id-192934.helmsley.irccloud.com) (Server closed connection) |
| 2023-11-10 15:05:35 +0100 | cbarrett | (sid192934@id-192934.helmsley.irccloud.com) |
| 2023-11-10 15:05:50 +0100 | <exarkun> | So, yes, there's lots and lots of code that, looking back on it now, is just redundant. |
| 2023-11-10 15:06:01 +0100 | <exarkun> | (Plus OO silliness) |
| 2023-11-10 15:06:19 +0100 | <exarkun> | I remember feeling very proud, at the time, about some of the crazy tricks I figured out how to play in Python |
| 2023-11-10 15:07:18 +0100 | <exarkun> | But also you are constantly surrounded by the same kind of thing, and trying to fight it is largely futile |
| 2023-11-10 15:07:34 +0100 | <Inst> | today I learned |
| 2023-11-10 15:07:49 +0100 | <exarkun> | All the libraries you want to use are insane, all the programmers you work with don't want to hear you say "functor", etc. |
| 2023-11-10 15:07:57 +0100 | <kuribas> | I hate crazy tricks in Python |
| 2023-11-10 15:08:02 +0100 | <kuribas> | Best python is dumb python |
| 2023-11-10 15:08:11 +0100 | <Inst> | oh, sorry, i'll wait, it's just that I've been playing around with monad comprehensions and I have to find them hilarious |
| 2023-11-10 15:09:05 +0100 | <kuribas> | exarkun: yeah, I have "None if foo is None else f(foo)" all over the place |
| 2023-11-10 15:18:31 +0100 | <Inst> | is there a valid way to abuse monad comprehensions? |
| 2023-11-10 15:19:12 +0100 | fendor | (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) |
| 2023-11-10 15:22:00 +0100 | thegeekinside | (~thegeekin@189.141.80.123) |
| 2023-11-10 15:25:19 +0100 | <kuribas> | I never found a reason for them, I just use do notation. |
| 2023-11-10 15:38:52 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 2023-11-10 15:40:03 +0100 | euleritian | (~euleritia@dynamic-046-114-201-197.46.114.pool.telefonica.de) |
| 2023-11-10 15:43:34 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2023-11-10 15:45:11 +0100 | dexter2 | (dexter@2a01:7e00::f03c:91ff:fe86:59ec) (Server closed connection) |
| 2023-11-10 15:45:40 +0100 | dexter2 | (dexter@2a01:7e00::f03c:91ff:fe86:59ec) |
| 2023-11-10 16:02:28 +0100 | SethTisue | (sid14912@id-14912.ilkley.irccloud.com) (Server closed connection) |
| 2023-11-10 16:02:36 +0100 | SethTisue | (sid14912@id-14912.ilkley.irccloud.com) |
| 2023-11-10 16:15:34 +0100 | Sgeo | (~Sgeo@user/sgeo) |
| 2023-11-10 16:18:26 +0100 | <geekosaur> | afaik they only (re)exist because early Haskell had them |
| 2023-11-10 16:25:51 +0100 | hongminhee | (sid295@id-295.tinside.irccloud.com) (Server closed connection) |
| 2023-11-10 16:26:00 +0100 | hongminhee | (sid295@id-295.tinside.irccloud.com) |
| 2023-11-10 16:30:26 +0100 | <sclv> | valid use for monad comprehensions is arguably sql-like functional queries over sets afaik |
| 2023-11-10 16:31:19 +0100 | <sclv> | like imagine a list comprehension syntax but so it works for things that are “general tuple stores” |
| 2023-11-10 16:35:29 +0100 | Lycurgus | (~georg@user/Lycurgus) |
| 2023-11-10 16:38:07 +0100 | <c_wraith> | the monad comprehension work added a lot of stuff besides generalizing them to work on more types. |
| 2023-11-10 16:38:59 +0100 | <geekosaur> | oh, the sql-like stuff went in at the same time? |
| 2023-11-10 16:39:14 +0100 | <c_wraith> | yeah |
| 2023-11-10 16:39:24 +0100 | <geekosaur> | not that that gets used much either, aside from one weird example from monochrom I've never seen it in the wild |
| 2023-11-10 16:40:56 +0100 | <c_wraith> | I really don't even use list comprehensions |
| 2023-11-10 16:41:09 +0100 | <c_wraith> | So I'm not one to judge their value |
| 2023-11-10 16:42:26 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 16:43:59 +0100 | danse-nr3 | (~danse@151.37.96.125) (Read error: Connection reset by peer) |
| 2023-11-10 16:44:06 +0100 | CiaoSen | (~Jura@2a05:5800:282:c200:2a3a:4dff:fe84:dbd5) |
| 2023-11-10 16:44:19 +0100 | chomwitt | (~chomwitt@2a02:587:7a1a:4300:1ac0:4dff:fedb:a3f1) (Ping timeout: 264 seconds) |
| 2023-11-10 16:44:49 +0100 | alp | (~alp@2001:861:5e02:eff0:2735:1b6e:45d6:b156) (Ping timeout: 246 seconds) |
| 2023-11-10 16:44:56 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2023-11-10 16:50:43 +0100 | astra | (sid289983@id-289983.hampstead.irccloud.com) (Server closed connection) |
| 2023-11-10 16:51:04 +0100 | astra | (sid289983@id-289983.hampstead.irccloud.com) |
| 2023-11-10 16:52:23 +0100 | danse-nr3 | (~danse@151.43.103.201) |
| 2023-11-10 16:53:05 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2023-11-10 16:55:46 +0100 | jrm | (~jrm@user/jrm) (Quit: ciao) |
| 2023-11-10 16:56:20 +0100 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 255 seconds) |
| 2023-11-10 16:57:07 +0100 | jrm | (~jrm@user/jrm) |
| 2023-11-10 16:57:16 +0100 | dsrt^ | (~cd@76.145.193.217) (Remote host closed the connection) |
| 2023-11-10 16:57:33 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 2023-11-10 16:58:34 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2023-11-10 16:59:46 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2023-11-10 17:05:22 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2023-11-10 17:09:02 +0100 | oo_miguel | (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) (Ping timeout: 252 seconds) |
| 2023-11-10 17:15:52 +0100 | themc47 | (~mc47@xmonad/TheMC47) |
| 2023-11-10 17:16:39 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Ping timeout: 240 seconds) |
| 2023-11-10 17:20:27 +0100 | <haskellbridge> | 12<Celestial> what's the "RealWorld" state that something like `putStr` returns inside it's IO behind the scenes? |
| 2023-11-10 17:20:48 +0100 | <haskellbridge> | 12<Celestial> I tried digging through the actual code but it's too many handles and delegations to see through |
| 2023-11-10 17:21:00 +0100 | <haskellbridge> | 12<Celestial> does it do "magic" and just return a "new" state? |
| 2023-11-10 17:21:20 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2023-11-10 17:22:02 +0100 | <haskellbridge> | 12<Celestial> and in what way is the old real world state used if at all |
| 2023-11-10 17:22:20 +0100 | alp | (~alp@2001:861:5e02:eff0:2a62:8087:a14f:a450) |
| 2023-11-10 17:22:24 +0100 | <geekosaur> | actually it's nonexistent |
| 2023-11-10 17:22:54 +0100 | <geekosaur> | it's a zero-width token that exists solely to keep I/O actions from being reordered by being passed to and returned from all IO actions |
| 2023-11-10 17:23:09 +0100 | <geekosaur> | in what amounts to an unboxed State monad |
| 2023-11-10 17:23:39 +0100 | <haskellbridge> | 12<Celestial> so it's only used in the types and disappears completely at runtime? |
| 2023-11-10 17:23:47 +0100 | <geekosaur> | after it's done its job of keeping things from being reordered, it goes away because it has no runtime representation |
| 2023-11-10 17:24:11 +0100 | <haskellbridge> | 12<Celestial> thanks! |
| 2023-11-10 17:24:34 +0100 | <geekosaur> | it lasts a little longer than the types because Core-to-Core transformations can reorder things. it's in the early stages of code generation that it's recognized as having no runtime rep and is removed |
| 2023-11-10 17:25:39 +0100 | CiaoSen | (~Jura@2a05:5800:282:c200:2a3a:4dff:fe84:dbd5) (Ping timeout: 258 seconds) |
| 2023-11-10 17:26:01 +0100 | <EvanR> | ncf, yeah you can do f Z (S _) impossible as one of the 'equations' |
| 2023-11-10 17:27:05 +0100 | ft | (~ft@p4fc2a529.dip0.t-ipconnect.de) |
| 2023-11-10 17:29:58 +0100 | akegalj | (~akegalj@195.29.107.235) (Ping timeout: 246 seconds) |
| 2023-11-10 17:31:21 +0100 | <monochrom> | My one weird comprehension trick: https://mail.haskell.org/pipermail/haskell-cafe/2018-February/128607.html >:) |
| 2023-11-10 17:31:59 +0100 | <monochrom> | I don't understand it either! I was just exploring madness. Consider it trololo. :) |
| 2023-11-10 17:32:21 +0100 | danse-nr3 | is jealous of monochrom's super-effective information retrieval system |
| 2023-11-10 17:32:46 +0100 | chomwitt | (~chomwitt@ppp-94-68-252-18.home.otenet.gr) |
| 2023-11-10 17:32:54 +0100 | <danse-nr3> | also yesterday i think you fished a mail from > 5 years ago |
| 2023-11-10 17:32:56 +0100 | <monochrom> | Err, I'm afraid it's ego instead. I bookmark my own posts. >:) |
| 2023-11-10 17:33:34 +0100 | <monochrom> | Remember "I quote myself all the time, it adds spice to my conversations"? |
| 2023-11-10 17:33:57 +0100 | <int-e> | mono "monochrom" chrom |
| 2023-11-10 17:34:05 +0100 | <EvanR> | 1 out of 1 Dr. T's (Mr. T) recommend it |
| 2023-11-10 17:34:10 +0100 | <monochrom> | BTW I changed that to "I talk to myself all the time, it adds sparks to my monologues" >:) |
| 2023-11-10 17:34:32 +0100 | <int-e> | A good way to have an intelligent conversation. |
| 2023-11-10 17:35:23 +0100 | jpds | (~jpds@gateway/tor-sasl/jpds) |
| 2023-11-10 17:36:08 +0100 | hamess | (~hamess@user/hamess) (Server closed connection) |
| 2023-11-10 17:36:28 +0100 | hamess | (~hamess@user/hamess) |
| 2023-11-10 17:37:28 +0100 | <danse-nr3> | interesting, it has something. I also find sometimes i learn better by what i express about, but can't find a rule for taking notes that does not feel cluttering |
| 2023-11-10 17:41:45 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Ping timeout: 258 seconds) |
| 2023-11-10 17:51:48 +0100 | <monochrom> | onoes haha 9.4.8 |
| 2023-11-10 17:52:07 +0100 | <monochrom> | I started using 9.4.7 just a few weeks ago! |
| 2023-11-10 17:52:42 +0100 | ell | (~ellie@user/ellie) (Server closed connection) |
| 2023-11-10 17:53:04 +0100 | ell | (~ellie@user/ellie) |
| 2023-11-10 17:53:14 +0100 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 2023-11-10 17:54:49 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) |
| 2023-11-10 17:57:22 +0100 | alp_ | (~alp@2001:861:5e02:eff0:aeff:dd51:6947:85fd) |
| 2023-11-10 18:00:46 +0100 | alp | (~alp@2001:861:5e02:eff0:2a62:8087:a14f:a450) (Ping timeout: 246 seconds) |
| 2023-11-10 18:01:08 +0100 | iteratee | (~kyle@162.218.222.207) |
| 2023-11-10 18:01:45 +0100 | lortabac | (~lorenzo@2a01:e0a:541:b8f0:504f:9bc8:bd3:5975) (Quit: WeeChat 3.5) |
| 2023-11-10 18:02:21 +0100 | Aleksejs | (~Aleksejs@107.170.21.106) (Server closed connection) |
| 2023-11-10 18:03:01 +0100 | Aleksejs | (~Aleksejs@107.170.21.106) |
| 2023-11-10 18:03:30 +0100 | Raito_Bezarius | (~Raito@82-65-118-1.subs.proxad.net) (Server closed connection) |
| 2023-11-10 18:03:41 +0100 | euleritian | (~euleritia@dynamic-046-114-201-197.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2023-11-10 18:04:00 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2023-11-10 18:04:42 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) |
| 2023-11-10 18:06:17 +0100 | eggplantade | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2023-11-10 18:06:19 +0100 | CiaoSen | (~Jura@2a05:5800:282:c200:2a3a:4dff:fe84:dbd5) |
| 2023-11-10 18:06:42 +0100 | <EvanR> | SPJ: RealWorld is deeply magical. geekosaur: RealWorld is nonexistent |
| 2023-11-10 18:07:04 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 246 seconds) |
| 2023-11-10 18:07:21 +0100 | <EvanR> | start to question the naming of this object xD |
| 2023-11-10 18:07:23 +0100 | <geekosaur> | maybe it was at one point. these days the magic is in `runRW#` and `RealWorld` itself is normal |
| 2023-11-10 18:07:23 +0100 | <EvanR> | starting* |
| 2023-11-10 18:07:38 +0100 | <danse-nr3> | i thought geekosaur talked about a nonexistent token? That is still mysterious anyways |
| 2023-11-10 18:08:35 +0100 | <EvanR> | is () a zero-width token that also doesn't exist? |
| 2023-11-10 18:09:16 +0100 | <geekosaur> | it's lifted. (# #) is the doesn't-exist one |
| 2023-11-10 18:09:31 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 18:09:37 +0100 | <int-e> | People confuse `RealWorld` and `State# RealWorld` which is IO's instance of `State# s` and that's the thing that doesn't exist. |
| 2023-11-10 18:09:52 +0100 | Earnestly | (~earnest@user/earnestly) |
| 2023-11-10 18:10:02 +0100 | <geekosaur> | also (# foo #) because the unboxed 1-tuple literally doesn't exist in the code generator (has no difference whatsoever from just foo) |
| 2023-11-10 18:15:10 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2023-11-10 18:17:02 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2023-11-10 18:23:11 +0100 | <absence> | If I have a value of a sum type, and due to the program flow I know which constructur it contains, is there an unsafe "trust me I know what I'm doing" mechanism that lets me access the contents of that constructor without doing a pattern match? |
| 2023-11-10 18:24:19 +0100 | <danse-nr3> | usually such a program flow would reflect what is happening in its types, so that the variety of values in the sum is reduced |
| 2023-11-10 18:24:19 +0100 | <EvanR> | yes but it would be better if you find a way to express that which is type safe |
| 2023-11-10 18:24:20 +0100 | <ncf> | which part of "doing a pattern match" do you want to avoid? |
| 2023-11-10 18:24:32 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 2023-11-10 18:24:34 +0100 | <ncf> | if it's strictness, then "lazy patterns" should be the answer |
| 2023-11-10 18:25:18 +0100 | <EvanR> | f :: Either A B -> C -- and f "knows" the argument is Left. So Take A instead of Either? |
| 2023-11-10 18:27:02 +0100 | <absence> | I know it would be better to express it with types, but it's not always practical. For example, how do you express a Data.Sequence.Seq that is not empty? |
| 2023-11-10 18:28:01 +0100 | <EvanR> | practically, not sure. But technically you can type it as (a, Seq a) |
| 2023-11-10 18:28:15 +0100 | chomwitt | (~chomwitt@ppp-94-68-252-18.home.otenet.gr) (Ping timeout: 240 seconds) |
| 2023-11-10 18:28:41 +0100 | <EvanR> | splitting off the first element proves it's not empty |
| 2023-11-10 18:28:49 +0100 | <danse-nr3> | i think that the sum case is easier to handle anyways |
| 2023-11-10 18:30:19 +0100 | <EvanR> | which is basically how NonEmpty works, but that's a list |
| 2023-11-10 18:30:32 +0100 | <absence> | EvanR: Sure, but the functions in Data.Sequence don't operate on (a, Seq a), so you have to reimplement whatever functions you need. |
| 2023-11-10 18:31:06 +0100 | <geekosaur> | absence, Either has a runtime representation, so you still need the pattern match to extract the Left even if you know it's always Left |
| 2023-11-10 18:31:38 +0100 | <geekosaur> | the tag (Left/Right) is there and has to be skipped, which is part of what the pattern match does |
| 2023-11-10 18:32:16 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2023-11-10 18:32:17 +0100 | <absence> | geekosaur: That makes sense. Can it be skipped without being checked though? |
| 2023-11-10 18:32:36 +0100 | <geekosaur> | unsafeCoerce might work |
| 2023-11-10 18:33:03 +0100 | <EvanR> | if you want to be unsafe, you can pattern match and leave off the "impossible" cases. Seq also has a similar mechanism, ViewL, ViewR to match against. You could ignore the Empty case |
| 2023-11-10 18:33:55 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 2023-11-10 18:34:26 +0100 | <geekosaur> | wait, I'm wrong. unsafeCoerce reinterprets the tag, it does not remove it |
| 2023-11-10 18:34:36 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 2023-11-10 18:35:03 +0100 | <EvanR> | % unsafeCoerce (Left 'a') :: Char |
| 2023-11-10 18:35:03 +0100 | <yahb2> | '\283741641161' |
| 2023-11-10 18:35:15 +0100 | <EvanR> | ewwww |
| 2023-11-10 18:35:22 +0100 | <EvanR> | also wtf |
| 2023-11-10 18:35:35 +0100 | <geekosaur> | that's probably the info table pointer for `Left` |
| 2023-11-10 18:35:49 +0100 | <geekosaur> | which is the "tag" that's in the way |
| 2023-11-10 18:35:50 +0100 | <EvanR> | I've never heard of that unicode character xD |
| 2023-11-10 18:35:58 +0100 | <danse-nr3> | i hope my next codebase will not be written thinking "haskell is guiding me, but i am smarter than that" |
| 2023-11-10 18:36:00 +0100 | <geekosaur> | Show doesn't validate |
| 2023-11-10 18:36:51 +0100 | fendor | (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) (Remote host closed the connection) |
| 2023-11-10 18:37:59 +0100 | <absence> | geekosaur: I guess it would be hard to get past that, unless I start following pointers manually, which is a bit too unsafe for my taste. :) |
| 2023-11-10 18:38:14 +0100 | <geekosaur> | yeh |
| 2023-11-10 18:38:27 +0100 | <EvanR> | what about this |
| 2023-11-10 18:38:45 +0100 | <geekosaur> | think you'd have to use Foreign ad hope a gc doesn't happen |
| 2023-11-10 18:39:24 +0100 | <EvanR> | % fst ((unsafeCoerce (Left 'a')) :: (Char,Char)) |
| 2023-11-10 18:39:24 +0100 | <yahb2> | 'a' |
| 2023-11-10 18:39:35 +0100 | <EvanR> | lol |
| 2023-11-10 18:40:03 +0100 | <absence> | Haha! |
| 2023-11-10 18:41:00 +0100 | <absence> | % snd ((unsafeCoerce (Left 'a')) :: (Char,Char)) |
| 2023-11-10 18:41:01 +0100 | <yahb2> | /workdir/entry.sh: line 6: 4 Segmentation fault (core dumped) ghcup --offline run -- ghci Yahb2Defs.hs 2>&1 |
| 2023-11-10 18:41:24 +0100 | <EvanR> | I was about to try that first, but consulted the oracle of delphi first |
| 2023-11-10 18:41:32 +0100 | <EvanR> | who said use fst |
| 2023-11-10 18:42:15 +0100 | <absence> | Good advice. Why a tuple though? |
| 2023-11-10 18:42:32 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds) |
| 2023-11-10 18:42:47 +0100 | <EvanR> | % runIdentity (unsafeCoerce (Left 'a') :: Identity Char) |
| 2023-11-10 18:42:47 +0100 | <yahb2> | Oops, something went wrong |
| 2023-11-10 18:42:50 +0100 | notzmv | (~zmv@user/notzmv) (Read error: Connection reset by peer) |
| 2023-11-10 18:43:00 +0100 | <absence> | % Solo 'a' |
| 2023-11-10 18:43:01 +0100 | <yahb2> | <interactive>:5:1: error: ; Data constructor not in scope: Solo :: Char -> t |
| 2023-11-10 18:43:40 +0100 | <absence> | % Data.Tuple.Solo 'a' |
| 2023-11-10 18:43:40 +0100 | <yahb2> | Solo 'a' |
| 2023-11-10 18:44:34 +0100 | <absence> | % (unsafecoerce (Left 'a')) :: Data.Tuple.Solo Char |
| 2023-11-10 18:44:34 +0100 | <yahb2> | <interactive>:9:2: error: ; Variable not in scope: unsafecoerce :: Either Char b0 -> Solo Char |
| 2023-11-10 18:44:45 +0100 | <absence> | % (unsafeCoerce (Left 'a')) :: Data.Tuple.Solo Char |
| 2023-11-10 18:44:45 +0100 | <yahb2> | <interactive>:11:2: error: ; Variable not in scope: unsafeCoerce :: Either Char b0 -> Solo Char |
| 2023-11-10 18:44:56 +0100 | <absence> | gah, I'll shut up now and do this locally. :D |
| 2023-11-10 18:45:17 +0100 | <EvanR> | I'd be curious to see how helpful this is to performance |
| 2023-11-10 18:46:15 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 18:46:16 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2023-11-10 18:46:46 +0100 | <absence> | Hey, that actually worked! |
| 2023-11-10 18:51:00 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
| 2023-11-10 18:51:38 +0100 | <EvanR> | the council is concerned about your interest in the dark ways |
| 2023-11-10 18:53:32 +0100 | danse-nr3 | (~danse@151.43.103.201) (Ping timeout: 252 seconds) |
| 2023-11-10 18:57:29 +0100 | <absence> | I discovered the nonempty-containers package. Balance is restored, for now.... |
| 2023-11-10 19:01:26 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 255 seconds) |
| 2023-11-10 19:02:29 +0100 | <absence> | But thanks for the help, it's really interesting to learn more about what goes on under the hood. |
| 2023-11-10 19:03:22 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2023-11-10 19:06:20 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2023-11-10 19:06:40 +0100 | finsternis | (~X@23.226.237.192) |
| 2023-11-10 19:20:18 +0100 | alp_ | (~alp@2001:861:5e02:eff0:aeff:dd51:6947:85fd) (Remote host closed the connection) |
| 2023-11-10 19:20:41 +0100 | alp_ | (~alp@2001:861:5e02:eff0:fcd9:3351:9e5:f09) |
| 2023-11-10 19:23:19 +0100 | shapr | (~user@2600:1700:c640:3100:9af4:b6dd:227b:75bc) (Ping timeout: 264 seconds) |
| 2023-11-10 19:25:28 +0100 | alp_ | (~alp@2001:861:5e02:eff0:fcd9:3351:9e5:f09) (Ping timeout: 246 seconds) |
| 2023-11-10 19:27:33 +0100 | iteratee | (~kyle@162.218.222.207) (Ping timeout: 258 seconds) |
| 2023-11-10 19:28:20 +0100 | kronicma1 | (user76110@neotame.csclub.uwaterloo.ca) (Server closed connection) |
| 2023-11-10 19:28:37 +0100 | kronicma1 | (user24323@neotame.csclub.uwaterloo.ca) |
| 2023-11-10 19:39:10 +0100 | ludat | (~ludat@190.210.223.66) |
| 2023-11-10 19:40:02 +0100 | neceve | (~neceve@user/neceve) |
| 2023-11-10 19:46:46 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2023-11-10 19:49:39 +0100 | iteratee | (~kyle@162.218.222.207) |
| 2023-11-10 19:49:44 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
| 2023-11-10 19:55:48 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2023-11-10 19:58:09 +0100 | SoF | (~skius@user/skius) (Server closed connection) |
| 2023-11-10 19:58:36 +0100 | iteratee | (~kyle@162.218.222.207) (Ping timeout: 258 seconds) |
| 2023-11-10 19:58:39 +0100 | SoF | (~skius@user/skius) |
| 2023-11-10 20:00:51 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Remote host closed the connection) |
| 2023-11-10 20:03:40 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds) |
| 2023-11-10 20:06:59 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2023-11-10 20:08:01 +0100 | danza | (~francesco@151.43.103.201) |
| 2023-11-10 20:10:32 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2023-11-10 20:20:40 +0100 | cln_ | (cln@wtf.cx) (Server closed connection) |
| 2023-11-10 20:20:57 +0100 | cln_ | (cln@wtf.cx) |
| 2023-11-10 20:22:42 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2023-11-10 20:28:15 +0100 | dcoutts | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 2023-11-10 20:30:21 +0100 | alp_ | (~alp@2001:861:5e02:eff0:50fb:33d8:6b1b:f0dc) |
| 2023-11-10 20:31:30 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 20:33:32 +0100 | systemfault | (sid267009@about/typescript/member/systemfault) (Server closed connection) |
| 2023-11-10 20:33:41 +0100 | systemfault | (sid267009@about/typescript/member/systemfault) |
| 2023-11-10 20:37:16 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
| 2023-11-10 20:37:41 +0100 | chiselfu1e | (~chiselfus@user/chiselfuse) |
| 2023-11-10 20:37:44 +0100 | CiaoSen | (~Jura@2a05:5800:282:c200:2a3a:4dff:fe84:dbd5) (Ping timeout: 255 seconds) |
| 2023-11-10 20:38:30 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 2023-11-10 20:42:01 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 2023-11-10 20:42:45 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2023-11-10 20:44:02 +0100 | danza | (~francesco@151.43.103.201) (Read error: Connection reset by peer) |
| 2023-11-10 20:47:43 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 246 seconds) |
| 2023-11-10 20:51:41 +0100 | <monochrom> | EvanR: Belated but you know how "real numbers" are unrealistic and "imaginary numbers" are not fiction either. :) |
| 2023-11-10 20:54:02 +0100 | <EvanR> | hold on how are they unrealistic |
| 2023-11-10 20:54:24 +0100 | trev | (~trev@user/trev) (Quit: trev) |
| 2023-11-10 21:00:58 +0100 | iteratee | (~kyle@162.218.222.207) |
| 2023-11-10 21:02:07 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) |
| 2023-11-10 21:03:10 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 255 seconds) |
| 2023-11-10 21:03:28 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2023-11-10 21:05:55 +0100 | iteratee | (~kyle@162.218.222.207) (Ping timeout: 264 seconds) |
| 2023-11-10 21:07:30 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Remote host closed the connection) |
| 2023-11-10 21:12:36 +0100 | ludat | (~ludat@190.210.223.66) (Ping timeout: 250 seconds) |
| 2023-11-10 21:16:58 +0100 | <monochrom> | There are uncomputability issues, for example. And for a model of space and/or time, the idea of a continuum may deviate from reality when you zoom in enough. |
| 2023-11-10 21:17:46 +0100 | <duncan> | I think you could model space and time with a Tardis monad. |
| 2023-11-10 21:19:41 +0100 | <monochrom> | Unpopular opinion: newtype IO a = IO (DisneyWorld -> (# a, DisneyWorld #)). >:) |
| 2023-11-10 21:20:27 +0100 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) |
| 2023-11-10 21:20:57 +0100 | iteratee | (~kyle@162.218.222.207) |
| 2023-11-10 21:21:18 +0100 | <EvanR> | at least real numbers are well defined, unlike reality |
| 2023-11-10 21:29:23 +0100 | CO2 | (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1) |
| 2023-11-10 21:32:32 +0100 | <ncf> | spoken like a true classical mathematician |
| 2023-11-10 21:33:22 +0100 | <EvanR> | D: |
| 2023-11-10 21:34:22 +0100 | <monochrom> | hee hee |
| 2023-11-10 21:34:55 +0100 | <monochrom> | I am a true or not true classical mathematician. >:) |
| 2023-11-10 21:35:06 +0100 | <EvanR> | also idea of continuums is more general than real numbers |
| 2023-11-10 21:46:55 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) |
| 2023-11-10 21:47:51 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 258 seconds) |
| 2023-11-10 21:49:06 +0100 | euleritian | (~euleritia@dynamic-046-114-206-043.46.114.pool.telefonica.de) |
| 2023-11-10 21:49:40 +0100 | alp_ | (~alp@2001:861:5e02:eff0:50fb:33d8:6b1b:f0dc) (Ping timeout: 246 seconds) |
| 2023-11-10 21:55:08 +0100 | chomwitt | (~chomwitt@2a02:587:7a12:2d00:1ac0:4dff:fedb:a3f1) |
| 2023-11-10 22:00:02 +0100 | <energizer> | does haskell ecosystem have a type like `missing` where `3 + missing` evaluates to `missing` and `3 < missing` is neither true nor false? |
| 2023-11-10 22:00:40 +0100 | <EvanR> | maybe acme-php |
| 2023-11-10 22:00:55 +0100 | Earnestly | (~earnest@user/earnestly) (WeeChat 4.1.1) |
| 2023-11-10 22:01:09 +0100 | <energizer> | is that a joke (idk anything about php) |
| 2023-11-10 22:01:18 +0100 | <EvanR> | it's a real haskell package! |
| 2023-11-10 22:01:40 +0100 | <EvanR> | providing some of the um, behavior of PHP's data types |
| 2023-11-10 22:02:36 +0100 | <nullie> | is it like NaN? |
| 2023-11-10 22:02:36 +0100 | <energizer> | i'm basically looking for something that's ultra fancy for inspiration on how to do this properly, not the opposite |
| 2023-11-10 22:02:40 +0100 | <EvanR> | 3 < missing not being a Bool is hard to pull off though because Ord |
| 2023-11-10 22:02:55 +0100 | <EvanR> | you'd need an alternative Prelude |
| 2023-11-10 22:04:04 +0100 | <geekosaur> | I could argue that undefined fits the description. perhaps not in the way energizer hopes, though 🙂 |
| 2023-11-10 22:04:14 +0100 | <monochrom> | "3 + missing" requires "missing" to have a term not a type. |
| 2023-11-10 22:04:28 +0100 | <monochrom> | err, to be a term not a type. |
| 2023-11-10 22:04:51 +0100 | <energizer> | sure i meant "a type whose value `missing` ..." |
| 2023-11-10 22:04:54 +0100 | <EvanR> | > let missing = 0/0 in 3 + missing |
| 2023-11-10 22:04:55 +0100 | <lambdabot> | NaN |
| 2023-11-10 22:05:13 +0100 | <monochrom> | OK, next is "3 + missing" requires missing to have the same type as 3's. |
| 2023-11-10 22:05:18 +0100 | <EvanR> | > let missing = 0/0 in 3 < missing |
| 2023-11-10 22:05:19 +0100 | <lambdabot> | False |
| 2023-11-10 22:05:37 +0100 | <EvanR> | :t (<) |
| 2023-11-10 22:05:38 +0100 | <lambdabot> | Ord a => a -> a -> Bool |
| 2023-11-10 22:05:40 +0100 | <monochrom> | (+) requires both operands to be the very same type. |
| 2023-11-10 22:06:09 +0100 | <monochrom> | At some point I will start asking "what's the real question?" |
| 2023-11-10 22:06:36 +0100 | <EvanR> | oh |
| 2023-11-10 22:06:37 +0100 | <monochrom> | But I'm OK with armchair type theory too. |
| 2023-11-10 22:06:41 +0100 | <EvanR> | geekosaur is totally right |
| 2023-11-10 22:07:00 +0100 | <geekosaur> | (but what I think they really want is SQL NULL) |
| 2023-11-10 22:07:21 +0100 | <monochrom> | Then go Maybe and have liftA2 (+) (pure 3) Nothing? |
| 2023-11-10 22:07:29 +0100 | <energizer> | haskell has abstract interpreters that can give `x < 3` -> OneOf(true,false) or some other ambiguous type like that, right? |
| 2023-11-10 22:07:48 +0100 | <monochrom> | No. |
| 2023-11-10 22:07:50 +0100 | <geekosaur> | that sounds like raku |
| 2023-11-10 22:07:57 +0100 | <monochrom> | Mathematica yes. Haskell no. |
| 2023-11-10 22:08:12 +0100 | <monochrom> | Mathematica is a CAS. Haskell is just a programming language. |
| 2023-11-10 22:09:09 +0100 | <monochrom> | Haskell can't even do [ x | x <- [0 .. ], x < 0 ] = []. |
| 2023-11-10 22:10:28 +0100 | <monochrom> | OO people look at Haskell's resemblance to OO syntax (even down to the reserved word "class"!) and assume OO semantics and get very disappointed. |
| 2023-11-10 22:10:56 +0100 | <monochrom> | Math people look at Haskell's resemblance to math syntax and assume math semantics and also get very disappointed. |
| 2023-11-10 22:11:03 +0100 | <monochrom> | This is the fault of Haskell, supposedly. |
| 2023-11-10 22:12:00 +0100 | iteratee_ | (~kyle@162.218.222.207) |
| 2023-11-10 22:13:34 +0100 | <EvanR> | a data structure is just a dumb programming language |
| 2023-11-10 22:13:39 +0100 | <EvanR> | haskell is just a programming language |
| 2023-11-10 22:13:49 +0100 | <energizer> | just to be clear, i dont mean normal haskell has this, but there's probably some dissertation out there that could support it -- or no? |
| 2023-11-10 22:14:05 +0100 | <monochrom> | Oh and APL people look at Haskell's resemblance to APL syntax but also get very disappointed that Haskell doesn't go the full way. >:) |
| 2023-11-10 22:14:43 +0100 | iteratee | (~kyle@162.218.222.207) (Ping timeout: 255 seconds) |
| 2023-11-10 22:15:39 +0100 | <exarkun> | energizer: is "true" in your example meant to be the true from logic or from haskell? |
| 2023-11-10 22:16:31 +0100 | Inst | (~Inst@120.244.192.250) (Ping timeout: 255 seconds) |
| 2023-11-10 22:16:36 +0100 | <geekosaur> | energizer, not at all easily, you'd have to start from RebindableSyntax and rebuild the whole language to get the boolean behavior you want. it'd be far easier to start with something that supports that semantics to begin with, like Mathematica or Raku |
| 2023-11-10 22:17:11 +0100 | <geekosaur> | and I doubt RebindableSyntax is well enough tested that this would work without compiler crashes |
| 2023-11-10 22:18:15 +0100 | <energizer> | exarkun: either one. i'm just looking for somebody who's tried to design "propagating unknown value" semantics properly, in contrast to all the data systems like SQL that do it in unprincipled ways. and haskell community seems oriented to doing semantics properly so i figure if somebody's done it then #haskell might know |
| 2023-11-10 22:18:59 +0100 | <geekosaur> | you want raku, really |
| 2023-11-10 22:19:18 +0100 | <monochrom> | You can accept undefined aka bottom, ⊥. Then Haskell has it since the beginning. |
| 2023-11-10 22:19:47 +0100 | <energizer> | geekosaur: i'm sure i don't want raku. it undoubtedly has support for crazy operators, but i'm really looking for something designed by a type theory practitioner. |
| 2023-11-10 22:19:58 +0100 | <monochrom> | (+) is strict in most cases so x+⊥ = ⊥ so it spreads. |
| 2023-11-10 22:20:24 +0100 | <EvanR> | > 3 < undefined |
| 2023-11-10 22:20:25 +0100 | <exarkun> | energizer: Is it very important that the operators are `+` and `<` and not, say, a lifted form? |
| 2023-11-10 22:20:26 +0100 | <lambdabot> | *Exception: Prelude.undefined |
| 2023-11-10 22:20:49 +0100 | <geekosaur> | monochrom: that's why I suggested undefined early on |
| 2023-11-10 22:20:55 +0100 | <monochrom> | Yeah. |
| 2023-11-10 22:21:08 +0100 | <monochrom> | Sorry! |
| 2023-11-10 22:21:15 +0100 | <EvanR> | thou shall not catch undefined. Unless you want to solve this specific problem very easily xD |
| 2023-11-10 22:21:16 +0100 | <exarkun> | It seems like Maybe (or an homomorphic type with Functor/Applicative) would be the principled way to do it. |
| 2023-11-10 22:21:18 +0100 | <geekosaur> | 3 < undefined is also undefined, therefore a value that is neither True nor False |
| 2023-11-10 22:21:21 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2023-11-10 22:21:38 +0100 | <EvanR> | Maybe won't let you use < because it has to return a Bool |
| 2023-11-10 22:21:39 +0100 | <exarkun> | `Just x` is a known value, `Nothing` is an unknown value |
| 2023-11-10 22:21:40 +0100 | <energizer> | exarkun: that is, making it a monad? |
| 2023-11-10 22:21:51 +0100 | <geekosaur> | it's just not _usefully_ such a value |
| 2023-11-10 22:21:59 +0100 | <exarkun> | EvanR: Right, so `liftA2 (<)` |
| 2023-11-10 22:22:08 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 2023-11-10 22:22:13 +0100 | <EvanR> | hmm ok |
| 2023-11-10 22:22:26 +0100 | <monochrom> | If you also require x:⊥ = ⊥, then go back all the way to SML or even before, they are strict languages so they have it since the 1980s. |
| 2023-11-10 22:22:27 +0100 | <exarkun> | energizer: I don't know if you even need Monad. |
| 2023-11-10 22:22:52 +0100 | <exarkun> | energizer: liftA2 (<) (Just 3) Nothing -> Nothing |
| 2023-11-10 22:23:28 +0100 | <exarkun> | Actually maybe you don't even need Applicative? |
| 2023-11-10 22:23:41 +0100 | michalz | (~michalz@185.246.207.205) (Remote host closed the connection) |
| 2023-11-10 22:23:43 +0100 | <monochrom> | With binary operators you need Applicative :) |
| 2023-11-10 22:23:57 +0100 | <monochrom> | With just unary operators then yeah Functor is good enough. |
| 2023-11-10 22:24:18 +0100 | <exarkun> | All operators are unary right: fmap (uncurry (<)) (Just 3, Nothing) |
| 2023-11-10 22:24:18 +0100 | <EvanR> | > liftA2 (:) (Just 'x') Nothing |
| 2023-11-10 22:24:19 +0100 | <lambdabot> | Nothing |
| 2023-11-10 22:24:22 +0100 | <EvanR> | check |
| 2023-11-10 22:24:34 +0100 | <exarkun> | (uh wait no that's nonsense sorry) |
| 2023-11-10 22:24:35 +0100 | <monochrom> | Well until you desire a way to say "missing + missing". |
| 2023-11-10 22:25:13 +0100 | <monochrom> | I know what you mean. fmap (3 +) Nothing needs just fmap. |
| 2023-11-10 22:25:55 +0100 | <energizer> | exarkun: all the data analysis languages (sql, r, pandas, julia, ...) do it without lifting: `3 + missing` is `missing`. so i think it's probably something more like `undefined` |
| 2023-11-10 22:26:10 +0100 | <EvanR> | they have the Maybe built-in |
| 2023-11-10 22:26:16 +0100 | <EvanR> | undefined throws an exception |
| 2023-11-10 22:26:20 +0100 | <monochrom> | I wouldn't call sql analysis. |
| 2023-11-10 22:26:21 +0100 | <exarkun> | energizer: Maybe! Or maybe they're all unprincipled? |
| 2023-11-10 22:27:06 +0100 | <exarkun> | `undefined` breaks Curry-Howard correspondence right? |
| 2023-11-10 22:27:10 +0100 | <monochrom> | But OK people even say "devop engineer" so all is inflated. |
| 2023-11-10 22:27:20 +0100 | <EvanR> | Maybe (Maybe Char), you got your present present, your present missing, and your missing missing |
| 2023-11-10 22:27:34 +0100 | <monochrom> | If you so much as count the number of rows, it's "analysis" already. |
| 2023-11-10 22:27:39 +0100 | <energizer> | exarkun: all those languages are unprincipled, that's why i'm here looking for, apparently, `undefined` |
| 2023-11-10 22:27:58 +0100 | <exarkun> | energizer: Yea. But I think I'll argue that Maybe/lifting is more principled than undefined. |
| 2023-11-10 22:28:07 +0100 | <EvanR> | > head (x : undefined) |
| 2023-11-10 22:28:09 +0100 | <lambdabot> | x |
| 2023-11-10 22:28:18 +0100 | <EvanR> | should be missing right, it's not |
| 2023-11-10 22:28:42 +0100 | <exarkun> | I could be more precise: There is a denotation for Maybe. There is no denotation for undefined (is there?) |
| 2023-11-10 22:28:56 +0100 | <monochrom> | There is. |
| 2023-11-10 22:28:59 +0100 | <exarkun> | crud |
| 2023-11-10 22:28:59 +0100 | <EvanR> | denotation of undefined is bottom |
| 2023-11-10 22:29:23 +0100 | <energizer> | > undefined + 3 |
| 2023-11-10 22:29:24 +0100 | <lambdabot> | *Exception: Prelude.undefined |
| 2023-11-10 22:29:30 +0100 | <monochrom> | https://en.wikibooks.org/wiki/Haskell/Denotational_semantics |
| 2023-11-10 22:29:32 +0100 | <energizer> | eh that's not very nice |
| 2023-11-10 22:29:40 +0100 | <EvanR> | > 3 : undefined |
| 2023-11-10 22:29:42 +0100 | <lambdabot> | [3*Exception: Prelude.undefined |
| 2023-11-10 22:29:49 +0100 | <monochrom> | Or my course notes https://www.cs.utoronto.ca/~trebla/CSCC24-2023-Summer/partial-order-recursion.html |
| 2023-11-10 22:30:20 +0100 | <monochrom> | lambdabot can only show you operational semantics. It's an interpreter, evaluator. |
| 2023-11-10 22:30:20 +0100 | <exarkun> | energizer: That's only because you let it reach the repl |
| 2023-11-10 22:30:35 +0100 | Franciman | reads 50 shades of and instantly closes |
| 2023-11-10 22:31:45 +0100 | <exarkun> | monochrom: ty for the links |
| 2023-11-10 22:32:00 +0100 | <exarkun> | I'm out |
| 2023-11-10 22:32:06 +0100 | iteratee_ | (~kyle@162.218.222.207) (Read error: Connection reset by peer) |
| 2023-11-10 22:32:28 +0100 | iteratee | (~kyle@162.218.222.207) |
| 2023-11-10 22:38:27 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 258 seconds) |
| 2023-11-10 22:43:22 +0100 | <EvanR> | bottom is correct, but let x = x in x is effectively missing too, and can't be caught. Problematic |
| 2023-11-10 22:43:53 +0100 | Pickchea | (~private@user/pickchea) |
| 2023-11-10 22:44:12 +0100 | <EvanR> | > let x = x in x -- except it can! |
| 2023-11-10 22:44:14 +0100 | <lambdabot> | *Exception: <<loop>> |
| 2023-11-10 22:44:50 +0100 | <monochrom> | "We don't talk about their difference here." :) |
| 2023-11-10 22:45:32 +0100 | td_ | (~td@i5387093F.versanet.de) (Ping timeout: 272 seconds) |
| 2023-11-10 22:46:34 +0100 | <EvanR> | does reality need ⊥ added to account for what's on the other side of an event horizon |
| 2023-11-10 22:46:43 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 2023-11-10 22:46:43 +0100 | <c_wraith> | sometimes it's surprisingly hard to get <<loop>> to be thrown |
| 2023-11-10 22:46:44 +0100 | td_ | (~td@i53870938.versanet.de) |
| 2023-11-10 22:47:47 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 2023-11-10 22:47:55 +0100 | <monochrom> | That's the Heisenbug nondeterminism principle. >:) |
| 2023-11-10 22:48:03 +0100 | <c_wraith> | like, it's only detected on a major GC, and sometimes GHC will decide "I don't need to do a major GC here", no matter how you try to convince it |
| 2023-11-10 22:49:49 +0100 | dcoutts | (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 2023-11-10 22:51:24 +0100 | <monochrom> | Hawking proved that combining denotational bottom and operation heisenbug nondeterminism gives you GHC panics emitted thermodynamically. >:) |
| 2023-11-10 22:51:44 +0100 | <c_wraith> | huh. How do I log those? |
| 2023-11-10 22:52:15 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 2023-11-10 22:53:27 +0100 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 240 seconds) |
| 2023-11-10 22:54:35 +0100 | koz | (~koz@121.99.240.58) (Server closed connection) |
| 2023-11-10 22:55:22 +0100 | koz | (~koz@121.99.240.58) |
| 2023-11-10 23:03:54 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:f92b:a41d:1acd:a4f6) (Ping timeout: 272 seconds) |
| 2023-11-10 23:08:23 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2023-11-10 23:08:46 +0100 | califax | (~califax@user/califx) |
| 2023-11-10 23:09:44 +0100 | alp_ | (~alp@2001:861:5e02:eff0:7ec6:459:f36f:4240) |
| 2023-11-10 23:12:12 +0100 | <EvanR> | the log is entropy |
| 2023-11-10 23:13:53 +0100 | <monochrom> | :) |
| 2023-11-10 23:14:39 +0100 | <c_wraith> | oh yeah. according to this album I've been listening to, I'm supposed to be embracing that. |
| 2023-11-10 23:16:00 +0100 | <monochrom> | Would that be "quantum computing on acid"? :) |
| 2023-11-10 23:17:24 +0100 | <c_wraith> | No, but that sounds fun too. :) |
| 2023-11-10 23:21:21 +0100 | Phlebas | (~Ozymandia@2605:59c8:1051:9710:f8a8:d14:29cd:af13) |
| 2023-11-10 23:27:30 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 2023-11-10 23:27:57 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2023-11-10 23:43:27 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2023-11-10 23:44:26 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2023-11-10 23:44:30 +0100 | woffs | (3cd46299b2@woffs.de) (Quit: Gateway shutdown) |
| 2023-11-10 23:45:31 +0100 | Phlebas | (~Ozymandia@2605:59c8:1051:9710:f8a8:d14:29cd:af13) (Ping timeout: 246 seconds) |
| 2023-11-10 23:48:02 +0100 | woffs | (3cd46299b2@woffs.de) |
| 2023-11-10 23:50:46 +0100 | thegeekinside | (~thegeekin@189.141.80.123) (Ping timeout: 272 seconds) |
| 2023-11-10 23:50:47 +0100 | Jackneill | (~Jackneill@20014C4E1E058A00D02EFDF46D150C42.dsl.pool.telekom.hu) (Ping timeout: 255 seconds) |
| 2023-11-10 23:52:35 +0100 | Phlebas | (~Ozymandia@2605:59c8:1051:9710:d740:c10b:741:3ce) |
| 2023-11-10 23:52:50 +0100 | Phlebas | (~Ozymandia@2605:59c8:1051:9710:d740:c10b:741:3ce) (Client Quit) |
| 2023-11-10 23:57:07 +0100 | ggVGc | (~ggVGc@a.lowtech.earth) |
| 2023-11-10 23:57:46 +0100 | acidjnk | (~acidjnk@p200300d6e72b9362d88f3ae5d7ed9705.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2023-11-10 23:58:15 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |