Home liberachat/#haskell: Logs Calendar

Logs on 2023-11-10 (liberachat/#haskell)

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

All times are in UTC on 2023-11-10.