Home liberachat/#haskell: Logs Calendar

Logs on 2024-05-18 (liberachat/#haskell)

00:00:25 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
00:13:18 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds)
00:14:50 bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
00:49:47 × m257 quits (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) (Ping timeout: 252 seconds)
00:58:35 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds)
01:06:34 × otto_s quits (~user@p5b0448c7.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
01:08:24 otto_s joins (~user@p5b044b71.dip0.t-ipconnect.de)
01:14:35 × Ranhir quits (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/)
01:14:37 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds)
01:15:40 × joeyadams quits (~joeyadams@2603:6010:5100:2ed:cfe3:13e2:96f6:9d2c) (Quit: Leaving)
01:35:59 × addfb3 quits (~dante@user/addfb3) (Ping timeout: 256 seconds)
01:40:46 Ranhir joins (~Ranhir@157.97.53.139)
02:00:02 × fliife quits (~fliife@user/fliife) (Quit: ZNC 1.8.2+deb2build5 - https://znc.in)
02:00:50 fliife joins (~fliife@user/fliife)
02:05:43 m257 joins (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca)
02:05:57 × dyniec quits (~dyniec@dybiec.info) (Quit: WeeChat 4.1.1)
02:09:34 × td_ quits (~td@i53870915.versanet.de) (Ping timeout: 246 seconds)
02:11:28 td_ joins (~td@i53870939.versanet.de)
02:12:28 × tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving)
02:14:16 tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303)
02:18:03 cjb joins (~cjb@user/cjb)
02:21:45 × ringo___ quits (~ringo@157.230.117.128) (Ping timeout: 268 seconds)
02:22:22 × Athas quits (athas@sigkill.dk) (Ping timeout: 268 seconds)
02:22:34 Athas joins (athas@2a01:7c8:aaac:1cf:3ae1:f43a:30e:d1d8)
02:23:32 ringo___ joins (~ringo@157.230.117.128)
02:24:08 × kimiamania quits (~76637481@user/kimiamania) (Quit: Ping timeout (120 seconds))
02:24:31 kimiamania joins (~76637481@user/kimiamania)
02:28:32 × bwe quits (~bwe@2a01:4f8:1c1c:4878::2) (Ping timeout: 268 seconds)
02:28:32 × mesaoptimizer quits (~mesaoptim@user/PapuaHardyNet) (Ping timeout: 268 seconds)
02:28:40 bwe joins (~bwe@2a01:4f8:1c1c:4878::2)
02:40:52 <talismanick> if types are propositions and programs are proofs, then mechanically the Monad instance for State is certainly an excersive in understanding through proof - it's basically dataflow through let-binding, as I see it
02:41:03 <talismanick> exercise*
02:44:03 × Axman6 quits (~Axman6@user/axman6) (Ping timeout: 264 seconds)
02:49:33 <talismanick> I guess it's natural for typeclass law proofs to be impervious to intuition because metaproofs are apt to be like that?
02:50:35 cheater_ joins (~Username@user/cheater)
02:51:52 ridcully_ joins (~ridcully@p508ac2b4.dip0.t-ipconnect.de)
02:52:53 × connrs quits (~connrs@user/connrs) (Ping timeout: 268 seconds)
02:52:56 hexeme_ joins (~hexeme@user/hexeme)
02:53:05 fiddlerw- joins (~fiddlerwo@user/fiddlerwoaroof)
02:53:59 lbseale_ joins (~quassel@user/ep1ctetus)
02:54:08 swistak- joins (~swistak@185.21.216.141)
02:54:11 gawen_ joins (~gawen@user/gawen)
02:54:17 johnw_ joins (~johnw@69.62.242.138)
02:54:39 ocra8_ joins (ocra8@user/ocra8)
02:54:57 tessier joins (~treed@ec2-184-72-149-67.compute-1.amazonaws.com)
02:55:15 kmein_ joins (~weechat@user/kmein)
02:55:20 defanor_ joins (~defanor@tart.uberspace.net)
02:55:20 weechat joins (~weechat@user/dminuoso)
02:55:43 tolt_ joins (~weechat-h@li219-154.members.linode.com)
02:56:24 todi1 joins (~todi@p57803331.dip0.t-ipconnect.de)
02:56:30 Eoco joins (~ian@128.101.131.218)
02:56:33 deriamis_ joins (deriamis@ec2-54-187-167-69.us-west-2.compute.amazonaws.com)
02:56:39 zlqrvx_ joins (~zlqrvx@101.175.150.247)
02:57:28 CodeKiwi joins (~kiwi@137.184.156.191)
02:58:43 flounders_ joins (~flounders@24.246.176.178)
02:59:00 teqwve- joins (teqwve@static.141.38.201.195.clients.your-server.de)
02:59:08 sand-witch_ joins (~m-mzmz6l@vmi833741.contaboserver.net)
03:00:45 × johnw quits (~johnw@69.62.242.138) (*.net *.split)
03:00:45 × ocra8 quits (ocra8@user/ocra8) (*.net *.split)
03:00:45 × todi quits (~todi@p57803331.dip0.t-ipconnect.de) (*.net *.split)
03:00:45 × deriamis quits (deriamis@ec2-54-187-167-69.us-west-2.compute.amazonaws.com) (*.net *.split)
03:00:45 × gawen quits (~gawen@user/gawen) (*.net *.split)
03:00:45 × foul_owl quits (~kerry@185.219.141.164) (*.net *.split)
03:00:46 × DigitalKiwi quits (~kiwi@137.184.156.191) (*.net *.split)
03:00:46 × cheater quits (~Username@user/cheater) (*.net *.split)
03:00:46 × acarrico quits (~acarrico@dhcp-68-142-49-163.greenmountainaccess.net) (*.net *.split)
03:00:46 × tessier_ quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (*.net *.split)
03:00:46 × Eoco_ quits (~ian@128.101.131.218) (*.net *.split)
03:00:46 × tolt quits (~weechat-h@li219-154.members.linode.com) (*.net *.split)
03:00:46 × flounders quits (~flounders@24.246.176.178) (*.net *.split)
03:00:46 × sand-witch quits (~m-mzmz6l@vmi833741.contaboserver.net) (*.net *.split)
03:00:46 × fiddlerwoaroof quits (~fiddlerwo@user/fiddlerwoaroof) (*.net *.split)
03:00:46 × kmein quits (~weechat@user/kmein) (*.net *.split)
03:00:46 × teqwve quits (teqwve@static.141.38.201.195.clients.your-server.de) (*.net *.split)
03:00:46 × zlqrvx quits (~zlqrvx@user/zlqrvx) (*.net *.split)
03:00:46 × ridcully quits (~ridcully@p508ac2b4.dip0.t-ipconnect.de) (*.net *.split)
03:00:46 × swistak quits (~swistak@185.21.216.141) (*.net *.split)
03:00:46 × df quits (~ben@justworks.xyz) (*.net *.split)
03:00:46 × lbseale quits (~quassel@user/ep1ctetus) (*.net *.split)
03:00:46 × defanor- quits (~defanor@tart.uberspace.net) (*.net *.split)
03:00:46 × dminuoso quits (~weechat@user/dminuoso) (*.net *.split)
03:00:46 × hexeme quits (~hexeme@user/hexeme) (*.net *.split)
03:00:54 cheater_ is now known as cheater
03:03:59 <dolio> No, propositions are types.
03:04:01 sand-witch_ is now known as sand-witch
03:04:13 <dolio> It's better if you don't read it the opposite way.
03:04:45 df joins (~ben@justworks.xyz)
03:10:02 × m257 quits (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) (Ping timeout: 252 seconds)
03:10:19 foul_owl joins (~kerry@71.212.149.206)
03:10:49 acarrico joins (~acarrico@dhcp-68-142-49-163.greenmountainaccess.net)
03:23:53 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:27:55 euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
03:38:06 Pixi__ joins (~Pixi@user/pixi)
03:39:03 cpli_ joins (77fc530071@2a03:6000:1812:100::252)
03:39:13 bw______ joins (sid2730@id-2730.ilkley.irccloud.com)
03:40:06 × cpli quits (77fc530071@2a03:6000:1812:100::252) (Ping timeout: 240 seconds)
03:40:06 × bw_____ quits (sid2730@id-2730.ilkley.irccloud.com) (Ping timeout: 240 seconds)
03:40:12 lukec_ joins (9dfd4d094e@2a03:6000:1812:100::10e)
03:40:18 cpli_ is now known as cpli
03:40:18 dy_ joins (sid3438@user/dy)
03:40:42 davetapley_ joins (sid666@id-666.uxbridge.irccloud.com)
03:41:31 Goodbye_Vincent1 joins (cyvahl@freakshells.net)
03:41:46 fluffyballoon_ joins (45ce440a48@2a03:6000:1812:100::e2)
03:41:51 shreyasminocha_ joins (51fdc93eda@user/shreyasminocha)
03:41:53 sgarcia joins (sgarcia@swarm.znchost.com)
03:42:08 integral_ joins (sid296274@user/integral)
03:42:13 systemfault_ joins (sid267009@about/typescript/member/systemfault)
03:42:25 ell6 joins (~ellie@user/ellie)
03:42:56 coldtom4 joins (~coldtom@coldrick.cc)
03:43:09 filwisher_ joins (2e6936c793@2a03:6000:1812:100::170)
03:43:21 gaze___ joins (sid387101@id-387101.helmsley.irccloud.com)
03:43:28 aspen_ joins (sid449115@id-449115.helmsley.irccloud.com)
03:43:46 chessai_ joins (sid225296@id-225296.lymington.irccloud.com)
03:44:02 amir_ joins (sid22336@user/amir)
03:44:10 scav_ joins (sid309693@user/scav)
03:44:17 piele_ joins (~piele@tbonesteak.creativeserver.net)
03:44:27 kuruczgy_ joins (55b66dd3ae@2a03:6000:1812:100::127f)
03:44:30 × dy quits (sid3438@user/dy) (Ping timeout: 240 seconds)
03:44:30 × lukec quits (9dfd4d094e@2a03:6000:1812:100::10e) (Ping timeout: 240 seconds)
03:44:30 × fluffyballoon quits (45ce440a48@2a03:6000:1812:100::e2) (Ping timeout: 240 seconds)
03:44:30 × davetapley quits (sid666@id-666.uxbridge.irccloud.com) (Ping timeout: 240 seconds)
03:44:30 dy_ is now known as dy
03:44:30 lukec_ is now known as lukec
03:44:30 fluffyballoon_ is now known as fluffyballoon
03:44:31 davetapley_ is now known as davetapley
03:44:40 jleightcap_ joins (7bc4014b62@user/jleightcap)
03:44:51 Ankhers_ joins (e99e97ef8e@2a03:6000:1812:100::2a2)
03:44:56 jmcantrell_ joins (644f1bed9a@user/jmcantrell)
03:44:57 remexre_ joins (~remexre@user/remexre)
03:45:01 Vq_ joins (~vq@81-231-76-8-no600.tbcn.telia.com)
03:45:03 pounce_ joins (~pounce@user/cute/pounce)
03:45:04 fgaz__ joins (1ff9197ed6@2a03:6000:1812:100::11ea)
03:45:18 constxqt joins (~constxd@user/constxd)
03:45:22 Taneb0 joins (~Taneb@runciman.hacksoc.org)
03:45:22 alanz_ joins (sid110616@id-110616.uxbridge.irccloud.com)
03:45:28 chaitlatte0_ joins (ea29c0bb16@2a03:6000:1812:100::1124)
03:45:43 arcadewise_ joins (52968ed80d@2a03:6000:1812:100::3df)
03:45:56 eso_ joins (a0662dfd5e@2a03:6000:1812:100::1266)
03:45:57 hiredman_ joins (~hiredman@frontier1.downey.family)
03:46:18 fn_lumi_ joins (3d621153a5@2a03:6000:1812:100::df7)
03:46:30 bsima1_ joins (9d7e39c8ad@2a03:6000:1812:100::dd)
03:46:41 ncf_ joins (~n@monade.li)
03:46:43 ursa-major_ joins (114efe6c39@2a03:6000:1812:100::11f3)
03:46:48 aniketd_ joins (32aa4844cd@2a03:6000:1812:100::dcb)
03:46:52 poscat0x04 joins (~poscat@user/poscat)
03:47:10 whereiseveryone_ joins (206ba86c98@2a03:6000:1812:100::2e4)
03:47:16 pikajude- joins (~jude@2001:19f0:ac01:373:5400:2ff:fe86:3274)
03:47:16 darrik joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se)
03:47:17 beaky_ joins (~beaky@2a03:b0c0:0:1010::1e:a001)
03:47:19 brettgilio_ joins (a35ba67324@2a03:6000:1812:100::260)
03:47:24 jjhoo_ joins (jahakala@user/jjhoo)
03:47:28 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 268 seconds)
03:47:28 probie_ joins (cc0b34050a@user/probie)
03:47:37 rselim_ joins (ce261f06ff@user/milesrout)
03:47:42 shachaf_ joins (~shachaf@li227-219.members.linode.com)
03:48:21 henrytill_ joins (e0180937c3@2a03:6000:1812:100::e8c)
03:48:31 markasoftware_ joins (~quassel@107.161.26.124)
03:48:45 caubert_ joins (~caubert@user/caubert)
03:49:00 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
03:49:05 Boarders_____ joins (sid425905@id-425905.lymington.irccloud.com)
03:49:22 nefercheprure joins (tma@twin.jikos.cz)
03:49:39 h2t joins (~h2t@user/h2t)
03:49:41 Hobbyboy|BNC joins (Hobbyboy@hobbyboy.co.uk)
03:49:58 mustafa_ joins (sid502723@rockylinux/releng/mustafa)
03:50:07 xigua_ joins (~xigua@user/xigua)
03:50:15 davean1 joins (~davean@davean.sciesnet.net)
03:50:27 hueso_ joins (~root@user/hueso)
03:50:35 × meinside quits (uid24933@id-24933.helmsley.irccloud.com) (Ping timeout: 260 seconds)
03:50:35 × constxd quits (~constxd@user/constxd) (Ping timeout: 260 seconds)
03:51:14 mht- joins (~mht@2a03:b0c0:3:e0::1e2:c001)
03:51:17 WzC joins (~Frank@77-162-168-71.fixed.kpn.net)
03:51:27 quintasan_ joins (~quassel@quintasan.pl)
03:51:35 Buggys- joins (Buggys@shelltalk.net)
03:51:37 aforemny joins (~aforemny@2001:9e8:6cdc:cf00:2044:2ce0:424e:adbd)
03:51:46 × aforemny_ quits (~aforemny@2001:9e8:6cfa:400:979c:514d:c315:798d) (Ping timeout: 246 seconds)
03:52:09 yandere__ joins (sid467876@id-467876.ilkley.irccloud.com)
03:53:00 mal1 joins (~mal@ns2.wyrd.be)
03:53:02 × acarrico quits (~acarrico@dhcp-68-142-49-163.greenmountainaccess.net) (*.net *.split)
03:53:02 × foul_owl quits (~kerry@71.212.149.206) (*.net *.split)
03:53:02 × df quits (~ben@justworks.xyz) (*.net *.split)
03:53:02 × hueso quits (~root@user/hueso) (*.net *.split)
03:53:02 × causal quits (~eric@50.35.88.207) (*.net *.split)
03:53:02 × xdminsy quits (~xdminsy@117.147.70.240) (*.net *.split)
03:53:02 × echoreply quits (~echoreply@45.32.163.16) (*.net *.split)
03:53:02 × cyphase quits (~cyphase@user/cyphase) (*.net *.split)
03:53:02 × hippoid quits (~hippoid@c-98-213-162-40.hsd1.il.comcast.net) (*.net *.split)
03:53:02 × [Leary] quits (~Leary]@user/Leary/x-0910699) (*.net *.split)
03:53:02 × op_4 quits (~tslil@user/op-4/x-9116473) (*.net *.split)
03:53:02 × dostoyevsky2 quits (~sck@user/dostoyevsky2) (*.net *.split)
03:53:02 × YuutaW quits (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (*.net *.split)
03:53:02 × esph quits (~weechat@user/esph) (*.net *.split)
03:53:02 × nurupo quits (~nurupo.ga@user/nurupo) (*.net *.split)
03:53:02 × TMA quits (tma@twin.jikos.cz) (*.net *.split)
03:53:02 × lambdabot quits (~lambdabot@haskell/bot/lambdabot) (*.net *.split)
03:53:02 × ncf quits (~n@monade.li) (*.net *.split)
03:53:02 × vgtw quits (~vgtw@user/vgtw) (*.net *.split)
03:53:02 × YoungFrog quits (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (*.net *.split)
03:53:02 × pieguy128 quits (~pieguy128@bras-base-mtrlpq5031w-grc-47-67-70-101-170.dsl.bell.ca) (*.net *.split)
03:53:02 × dibblego quits (~dibblego@haskell/developer/dibblego) (*.net *.split)
03:53:02 × tnks quits (sid412124@id-412124.helmsley.irccloud.com) (*.net *.split)
03:53:02 × bradparker quits (sid262931@id-262931.uxbridge.irccloud.com) (*.net *.split)
03:53:02 × jmct quits (sid160793@id-160793.tinside.irccloud.com) (*.net *.split)
03:53:02 × b20n quits (sid115913@id-115913.uxbridge.irccloud.com) (*.net *.split)
03:53:02 × kaol quits (~kaol@94-237-42-30.nl-ams1.upcloud.host) (*.net *.split)
03:53:02 × lieven quits (~mal@ns2.wyrd.be) (*.net *.split)
03:53:02 × Hobbyboy quits (Hobbyboy@hobbyboy.co.uk) (*.net *.split)
03:53:02 × davean quits (~davean@davean.sciesnet.net) (*.net *.split)
03:53:02 × tamer quits (~tamer@user/tamer) (*.net *.split)
03:53:02 × bastelfreak quits (bastelfrea@libera/staff/VoxPupuli.bastelfreak) (*.net *.split)
03:53:02 × mrmonday quits (~robert@what.i.hope.is.not.a.tabernaevagant.es) (*.net *.split)
03:53:02 × evertedsphere quits (sid434122@id-434122.hampstead.irccloud.com) (*.net *.split)
03:53:18 nurupo_ joins (~nurupo.ga@user/nurupo)
03:53:33 xdminsy joins (~xdminsy@117.147.70.240)
03:53:38 × APic quits (apic@apic.name) (*.net *.split)
03:53:38 × Noinia quits (~Frank@77-162-168-71.fixed.kpn.net) (*.net *.split)
03:53:38 × chaitlatte0 quits (ea29c0bb16@user/chaitlatte0) (*.net *.split)
03:53:38 × probie quits (cc0b34050a@user/probie) (*.net *.split)
03:53:38 × caubert quits (~caubert@user/caubert) (*.net *.split)
03:53:38 × henrytill quits (e0180937c3@2a03:6000:1812:100::e8c) (*.net *.split)
03:53:38 × kuruczgy quits (55b66dd3ae@2a03:6000:1812:100::127f) (*.net *.split)
03:53:38 × jmcantrell quits (644f1bed9a@user/jmcantrell) (*.net *.split)
03:53:38 × Ankhers quits (e99e97ef8e@2a03:6000:1812:100::2a2) (*.net *.split)
03:53:38 × rselim quits (ce261f06ff@user/milesrout) (*.net *.split)
03:53:38 × arcadewise quits (52968ed80d@2a03:6000:1812:100::3df) (*.net *.split)
03:53:38 × ursa-major quits (114efe6c39@2a03:6000:1812:100::11f3) (*.net *.split)
03:53:38 × whereiseveryone quits (206ba86c98@2a03:6000:1812:100::2e4) (*.net *.split)
03:53:38 × scav quits (sid309693@user/scav) (*.net *.split)
03:53:38 × mht-wtf quits (~mht@mht.wtf) (*.net *.split)
03:53:38 × Goodbye_Vincent quits (cyvahl@freakshells.net) (*.net *.split)
03:53:38 × coldtom quits (~coldtom@coldrick.cc) (*.net *.split)
03:53:38 × gaze__ quits (sid387101@id-387101.helmsley.irccloud.com) (*.net *.split)
03:53:38 × alanz quits (sid110616@id-110616.uxbridge.irccloud.com) (*.net *.split)
03:53:38 × yandere_ quits (sid467876@id-467876.ilkley.irccloud.com) (*.net *.split)
03:53:38 × h2t_ quits (~h2t@user/h2t) (*.net *.split)
03:53:38 × amir quits (sid22336@user/amir) (*.net *.split)
03:53:38 × integral quits (sid296274@user/integral) (*.net *.split)
03:53:38 × haritz quits (~hrtz@user/haritz) (*.net *.split)
03:53:38 × aspen quits (sid449115@id-449115.helmsley.irccloud.com) (*.net *.split)
03:53:38 × Boarders____ quits (sid425905@id-425905.lymington.irccloud.com) (*.net *.split)
03:53:38 × systemfault quits (sid267009@about/typescript/member/systemfault) (*.net *.split)
03:53:38 × chessai quits (sid225296@id-225296.lymington.irccloud.com) (*.net *.split)
03:53:38 × xigua quits (~xigua@user/xigua) (*.net *.split)
03:53:38 × jleightcap quits (7bc4014b62@user/jleightcap) (*.net *.split)
03:53:38 × brettgilio quits (a35ba67324@2a03:6000:1812:100::260) (*.net *.split)
03:53:38 × fn_lumi quits (3d621153a5@2a03:6000:1812:100::df7) (*.net *.split)
03:53:38 × shreyasminocha quits (51fdc93eda@user/shreyasminocha) (*.net *.split)
03:53:38 × aniketd quits (32aa4844cd@2a03:6000:1812:100::dcb) (*.net *.split)
03:53:38 × eso quits (a0662dfd5e@2a03:6000:1812:100::1266) (*.net *.split)
03:53:38 × fgaz_ quits (1ff9197ed6@2a03:6000:1812:100::11ea) (*.net *.split)
03:53:38 × filwisher quits (2e6936c793@2a03:6000:1812:100::170) (*.net *.split)
03:53:38 × bsima1 quits (9d7e39c8ad@2a03:6000:1812:100::dd) (*.net *.split)
03:53:38 × remexre quits (~remexre@user/remexre) (*.net *.split)
03:53:38 × beaky quits (~beaky@2a03:b0c0:0:1010::1e:a001) (*.net *.split)
03:53:38 × Riviera quits (Riviera@user/riviera) (*.net *.split)
03:53:38 × poscat quits (~poscat@user/poscat) (*.net *.split)
03:53:38 × Pixi` quits (~Pixi@user/pixi) (*.net *.split)
03:53:38 × tv quits (~tv@user/tv) (*.net *.split)
03:53:38 × hiredman quits (~hiredman@frontier1.downey.family) (*.net *.split)
03:53:38 × wz1000 quits (~zubin@static.11.113.47.78.clients.your-server.de) (*.net *.split)
03:53:38 × Taneb quits (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (*.net *.split)
03:53:38 × y-koj quits (~yk@2404:7a81:c840:5e00:e654:e8ff:fee1:ca92) (*.net *.split)
03:53:38 × Vq quits (~vq@81-231-76-8-no600.tbcn.telia.com) (*.net *.split)
03:53:38 × sgarcia_ quits (sgarcia@swarm.znchost.com) (*.net *.split)
03:53:38 × markasoftware quits (~quassel@107.161.26.124) (*.net *.split)
03:53:38 × Buggys quits (Buggys@shelltalk.net) (*.net *.split)
03:53:39 × Ekho quits (~Ekho@user/ekho) (*.net *.split)
03:53:39 × ell quits (~ellie@user/ellie) (*.net *.split)
03:53:39 × Aleksejs quits (~Aleksejs@107.170.21.106) (*.net *.split)
03:53:39 × bcksl quits (~bcksl@user/bcksl) (*.net *.split)
03:53:39 × Natch quits (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (*.net *.split)
03:53:39 × quintasan quits (~quassel@quintasan.pl) (*.net *.split)
03:53:39 × noctux quits (~noctux@user/noctux) (*.net *.split)
03:53:39 × jjhoo quits (~jahakala@user/jjhoo) (*.net *.split)
03:53:39 × pounce quits (~pounce@user/cute/pounce) (*.net *.split)
03:53:39 × mustafa quits (sid502723@rockylinux/releng/mustafa) (*.net *.split)
03:53:39 × shachaf quits (~shachaf@user/shachaf) (*.net *.split)
03:53:39 × spider quits (spider@tilde.cafe) (*.net *.split)
03:53:39 × albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (*.net *.split)
03:53:39 × pikajude quits (~jude@149.28.207.64) (*.net *.split)
03:53:39 × dragestil quits (~znc@user/dragestil) (*.net *.split)
03:53:39 × tstat_ quits (~tstat@user/tstat) (*.net *.split)
03:53:39 × dfordvm quits (~dfordivam@160.16.87.223.v6.sakura.ne.jp) (*.net *.split)
03:53:39 × piele quits (~piele@tbonesteak.creativeserver.net) (*.net *.split)
03:53:40 Ankhers_ is now known as Ankhers
03:53:40 kuruczgy_ is now known as kuruczgy
03:53:40 alanz_ is now known as alanz
03:53:40 systemfault_ is now known as systemfault
03:53:40 ell6 is now known as ell
03:53:40 pounce_ is now known as pounce
03:53:43 yandere__ is now known as yandere_
03:53:43 aniketd_ is now known as aniketd
03:53:44 henrytill_ is now known as henrytill
03:53:44 mustafa_ is now known as mustafa
03:53:44 rselim_ is now known as rselim
03:53:45 Goodbye_Vincent1 is now known as Goodbye_Vincent
03:53:45 scav_ is now known as scav
03:53:45 gaze___ is now known as gaze__
03:53:45 amir_ is now known as amir
03:53:45 remexre_ is now known as remexre
03:53:45 bsima1_ is now known as bsima1
03:53:45 probie_ is now known as probie
03:53:45 arcadewise_ is now known as arcadewise
03:53:45 xigua_ is now known as xigua
03:53:45 eso_ is now known as eso
03:53:46 chaitlatte0_ is now known as chaitlatte0
03:53:46 jmcantrell_ is now known as jmcantrell
03:53:46 coldtom4 is now known as coldtom
03:53:46 integral_ is now known as integral
03:53:46 chessai_ is now known as chessai
03:53:46 aspen_ is now known as aspen
03:53:47 fgaz__ is now known as fgaz_
03:53:47 shreyasminocha_ is now known as shreyasminocha
03:53:47 fn_lumi_ is now known as fn_lumi
03:53:47 brettgilio_ is now known as brettgilio
03:53:47 jleightcap_ is now known as jleightcap
03:53:48 ursa-major_ is now known as ursa-major
03:53:48 whereiseveryone_ is now known as whereiseveryone
03:53:59 yandere_ is now known as tapas
03:54:00 Hobbyboy|BNC is now known as Hobbyboy
03:54:05 tv joins (~tv@user/tv)
03:54:12 tstat joins (~tstat@user/tstat)
03:54:14 noctux joins (~noctux@user/noctux)
03:54:15 Aleksejs joins (~Aleksejs@107.170.21.106)
03:54:48 × AlexNoo_ quits (~AlexNoo@5.139.232.131) (Read error: Connection reset by peer)
03:55:15 UNREAALuo-ed joins (~UNREAALao@163.180.213.155)
03:55:21 AlexNoo_ joins (~AlexNoo@5.139.232.131)
03:55:32 UNREAALuo-ed parts (~UNREAALao@163.180.213.155) ()
03:55:37 meinside joins (uid24933@id-24933.helmsley.irccloud.com)
03:55:41 lambdabot joins (~lambdabot@silicon.int-e.eu)
03:55:41 × lambdabot quits (~lambdabot@silicon.int-e.eu) (Changing host)
03:55:41 lambdabot joins (~lambdabot@haskell/bot/lambdabot)
03:55:41 ChanServ sets mode +v lambdabot
03:55:59 acarrico joins (~acarrico@dhcp-68-142-49-163.greenmountainaccess.net)
03:55:59 df joins (~ben@justworks.xyz)
03:55:59 causal joins (~eric@50.35.88.207)
03:55:59 echoreply joins (~echoreply@45.32.163.16)
03:55:59 hippoid joins (~hippoid@c-98-213-162-40.hsd1.il.comcast.net)
03:55:59 [Leary] joins (~Leary]@user/Leary/x-0910699)
03:55:59 op_4 joins (~tslil@user/op-4/x-9116473)
03:55:59 dostoyevsky2 joins (~sck@user/dostoyevsky2)
03:55:59 YuutaW joins (~YuutaW@2404:f4c0:f9c3:502::100:17b7)
03:55:59 vgtw joins (~vgtw@user/vgtw)
03:55:59 YoungFrog joins (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be)
03:55:59 pieguy128 joins (~pieguy128@bras-base-mtrlpq5031w-grc-47-67-70-101-170.dsl.bell.ca)
03:55:59 b20n joins (sid115913@id-115913.uxbridge.irccloud.com)
03:55:59 kaol joins (~kaol@94-237-42-30.nl-ams1.upcloud.host)
03:55:59 tamer joins (~tamer@user/tamer)
03:55:59 bastelfreak joins (bastelfrea@libera/staff/VoxPupuli.bastelfreak)
03:55:59 mrmonday joins (~robert@what.i.hope.is.not.a.tabernaevagant.es)
03:55:59 evertedsphere joins (sid434122@id-434122.hampstead.irccloud.com)
03:56:11 Pegazusuo`_ joins (~Syzzopiu_@fixed-187-189-91-62.totalplay.net)
03:56:12 bradparker joins (sid262931@id-262931.uxbridge.irccloud.com)
03:56:18 <Pegazusuo`_> shachaf_ rselim probie jjhoo_ brettgilio beaky_ darrik pikajude- whereiseveryone poscat0x04 aniketd ursa-major ncf_ bsima1 fn_lumi hiredman_ eso arcadewise chaitlatte0 alanz Taneb0 constxqt fgaz_ pounce Vq_ remexre jmcantrell Ankhers jleightcap kuruczgy piele_ scav amir chessai aspen gaze__ filwisher_ coldtom ell systemfault integral sgarcia shreyasminocha fluffyballoon Goodbye_Vincent d
03:56:19 <Pegazusuo`_> avetapley dy lukec bw______ cpli Pixi__ euleritian peterbecich sand-witch teqwve- flounders_ CodeKiwi zlqrvx_ deriamis_ Eoco todi1 tolt_ weechat defanor_ kmein_ tessier ocra8_ johnw_ gawen_ swistak- lbseale_ fiddlerw- hexeme_ ridcully_ cheater bwe kimiamania ringo___ Athas cjb tcard td_ fliife Ranhir otto_s bitdex talismanick AlexZenon califax visilii_ pavonia emmanuelux euphores raym JimL n
03:56:20 <Pegazusuo`_> ullie mei tzh _xor billchenchina sp1ff EvanR Sgeo FinnElija patrl zer0bitz igemnace qqq xff0x ft rvalue Lord_of_Life L29Ah ChaiTRex driib3 mikko xal tinjamin doyougnu oo_miguel philopsos bollu B-J immae sudden bsima remmie landonf Dykam pierrot evanrelf cln_ JoelMcCracken mhatta samhh_ TheCoffeMaker joeyh akspecs riatre mauke _0xa fr33domlover lambdap2371 xstill_ Pozyomka xsarnik carter_
03:56:21 <Pegazusuo`_> PotatoGim_ dmj` Pent nek0 Fangs edwardk darkling hugo sprout puke dagi85299 jinsun MironZ xnyhps jcarpenter2 tomboy64 jrm destituion Maxdamantus koz famubu chexum pie_ ec m1dnight terrorjack aku SteelBlueSilk erisco phma Luj bliminse demon-cat p3n CrunchyFlakes JamesMowery hgolden laker monochrom michalz biberu pointlessslippe1 Moyst cayley5 ent infinity0 dtman34 img lockna rdcdr son0p Rodney_
03:56:22 <Pegazusuo`_> iteratee paddymahoney gentauro urdh drdo m5zs7k stefan-__ ames Raito_Bezarius [exa] Ram-Z mrmr1553343 tt1231097 _d0t mima benjaminl GoldsteinQ jle` arahael dolio szkl Hafydd inedia pja pandeyan motherfsck mulk sam113101 vulpine eugenrh forell chiselfuse mjrosenb andrea_r Me-me bionade24 zmt01 adium glguy nschoe tabemann ircbrowse_tom tomsmeding amjoseph nitrix bgamari orcus dispater mxs Angelz
03:56:23 <Pegazusuo`_> tomku masterbuilder fryguybob myxos sympt Rembane itaipu whatsupdoc endojelly rembo10 Teacup_ xelxebar_ kaskal- kritzefitz welterde leah2 migas97 Batzy malte arkeet paotsaq Xe juri_ thaumavorio byte ski Yumemi krei-se ACuriousMoose finsternis canta cjay kosmikus A_Dragon picnoir stefan-_ gabriel_sevecek kronicmage robobub opqdonut auri rncwnd emergence jocke-l hook54321 robertm tired statusbot
03:56:24 <Pegazusuo`_> wryish siers koala_man adamCS incertia lockywolf end meejah ario sweater aws seeg123456 leeb nshepperd2 carbolymer bryanv Typedfern enikar mzg haveo_ mqlnv down200 zfnmxt flukiluke She berberman danso hughjfchen Patternmaster _________ catties FragByte dunj3 tertek anon8697 hc sukbeom V peutri lyxia Arsen bairyn Fijxu tdammers int-e it_ s4msung sshine Philonous CATS RMSBach gabiruh Vajb delyan_
03:56:25 <Pegazusuo`_> Flow Franciman cross yaroot samhh jkoshy jakzale fvr sus sm2n ymherklotz duncan b0o pmk raghavgururajan ggb lane wagle sajith nonzen hamishmack flocks andjjj23 mniip_ barrucadu abrar MelMalik conjunctive sefidel myme earthy diagprov snek tritlo_ hololeap yahb2 hovsater Sciencentistguy sm sa jackdk T_S_____ Kamuela byorgey red-snail nisstyre turlando jakesyl_____ buhman Tisoxin liskin mrvdb pdw
03:56:26 <Pegazusuo`_> Fischmiep TimWolla heartbur1 ian_ Clint andreas808 smalltalkman geekosaur edmundnoble_ edwtjo tinwood SethTisue PHO`_ lally alinab mjacob lisq nadja hadronized tureba mcfrdy nshepperd lexi-lambda SanchayanMaity idnar bjs degraafk CalimeroTeknik Putonlalla dumptruckman [_________] polux dfg edm NemesisD sa1 rune_ taktoa[c] jonrh c_wraith tomjaguarpaw nckx xerox farn_ exarkun eL_Bart0- energizer
03:56:27 <Pegazusuo`_> gmc astra shawwwn mankyKitty caasih bah ouroboros disconnect3d acro davl litharge NiKaN apache Techcable sclv iphy ProofTechnique_ rubin55 natto aristid JSharp drlkf SoF hexology shane Hecate Jon loonycyborg noteness- laman1 xnbya2 SrPx acidsys rachelambda krasjet institor mira mmaruseacph2 yushyin cbarrett S11001001 dsal xacktm stilgart nrr_______ meooow chymera haasn Logio totbwf ChanServ
03:56:28 Pegazusuo`_ parts (~Syzzopiu_@fixed-187-189-91-62.totalplay.net) ()
03:56:42 × zmt01 quits (~zmt00@user/zmt00) (Quit: Leaving)
03:56:47 dibblego joins (~dibblego@116.255.1.119)
03:56:47 × dibblego quits (~dibblego@116.255.1.119) (Changing host)
03:56:47 dibblego joins (~dibblego@haskell/developer/dibblego)
03:56:57 cyphase joins (~cyphase@user/cyphase)
03:57:15 nurupo_ is now known as nurupo
03:57:19 Riviera joins (Riviera@user/riviera)
03:57:21 × df quits (~ben@justworks.xyz) (Remote host closed the connection)
03:57:24 × causal quits (~eric@50.35.88.207) (Ping timeout: 260 seconds)
03:57:24 × hippoid quits (~hippoid@c-98-213-162-40.hsd1.il.comcast.net) (Ping timeout: 260 seconds)
03:57:32 df joins (~ben@justworks.xyz)
03:57:33 × kaol quits (~kaol@94-237-42-30.nl-ams1.upcloud.host) (Ping timeout: 260 seconds)
03:57:33 × tamer quits (~tamer@user/tamer) (Quit: "")
03:57:35 kaol_ joins (~kaol@94-237-42-30.nl-ams1.upcloud.host)
03:57:48 tmr joins (~tamer@5.2.74.82)
03:58:20 causal joins (~eric@50.35.88.207)
03:58:22 hippoid joins (~hippoid@c-98-213-162-40.hsd1.il.comcast.net)
03:58:47 tnks joins (sid412124@id-412124.helmsley.irccloud.com)
03:58:48 × b20n quits (sid115913@id-115913.uxbridge.irccloud.com) (Ping timeout: 260 seconds)
03:58:49 ChanServ sets mode +o glguy
03:59:00 glguy sets mode +R
03:59:01 haritz joins (~hrtz@user/haritz)
03:59:01 y-koj joins (~yk@2404:7a81:c840:5e00:e654:e8ff:fee1:ca92)
03:59:01 dragestil joins (~znc@user/dragestil)
03:59:01 dfordvm joins (~dfordivam@160.16.87.223.v6.sakura.ne.jp)
03:59:46 b20n joins (sid115913@id-115913.uxbridge.irccloud.com)
04:01:53 Ekho joins (~Ekho@user/ekho)
04:02:02 APic joins (apic@apic.name)
04:02:11 bcksl joins (~bcksl@user/bcksl)
04:02:55 y-koj_ joins (~yk@2404:7a81:c840:5e00:e654:e8ff:fee1:ca92)
04:04:09 × y-koj quits (~yk@2404:7a81:c840:5e00:e654:e8ff:fee1:ca92) (Ping timeout: 240 seconds)
04:04:16 esph joins (~weechat@user/esph)
04:04:49 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 255 seconds)
04:06:49 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
04:07:29 albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8)
04:08:04 × pieguy128 quits (~pieguy128@bras-base-mtrlpq5031w-grc-47-67-70-101-170.dsl.bell.ca) (Max SendQ exceeded)
04:08:04 × vgtw quits (~vgtw@user/vgtw) (Max SendQ exceeded)
04:08:51 jmct joins (sid160793@id-160793.tinside.irccloud.com)
04:08:52 pieguy128 joins (~pieguy128@bas1-quebec14-67-70-101-170.dsl.bell.ca)
04:09:56 vgtw joins (~vgtw@user/vgtw)
04:10:23 foul_owl joins (~kerry@71.212.149.206)
04:12:36 hea_ed joins (~LRHio`y@80.69.63.28)
04:12:36 × hea_ed quits (~LRHio`y@80.69.63.28) (K-Lined)
04:28:28 spider joins (spider@tilde.cafe)
04:32:00 raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
04:36:47 wz1000 joins (~zubin@static.11.113.47.78.clients.your-server.de)
04:51:40 × Eoco quits (~ian@128.101.131.218) (Quit: WeeChat 4.1.1)
04:54:15 Eoco joins (~ian@128.101.131.218)
04:55:38 × Eoco quits (~ian@128.101.131.218) (Client Quit)
04:55:41 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 272 seconds)
04:56:50 Eoco joins (~ian@128.101.131.218)
04:57:07 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
04:57:55 × Eoco quits (~ian@128.101.131.218) (Client Quit)
04:58:15 Eoco joins (~ian@128.101.131.218)
04:58:43 × Eoco quits (~ian@128.101.131.218) (Client Quit)
04:59:02 Eoco joins (~ian@128.101.131.218)
05:00:08 y04nn joins (~username@2a03:1b20:8:f011::e10d)
05:03:45 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds)
05:08:24 zetef joins (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
05:17:04 takuan joins (~takuan@178-116-218-225.access.telenet.be)
05:28:22 connrs joins (~connrs@user/connrs)
05:36:35 × foul_owl quits (~kerry@71.212.149.206) (Ping timeout: 264 seconds)
05:44:35 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds)
05:47:19 Vq_ is now known as Vq
05:48:29 foul_owl joins (~kerry@157.97.134.168)
05:54:09 × philopsos quits (~caecilius@user/philopsos) (Quit: Lost terminal)
05:58:11 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
06:00:06 philopsos joins (~caecilius@user/philopsos)
06:02:45 × cjb quits (~cjb@user/cjb) (Quit: leaving)
06:07:32 cjb joins (813b6d8c75@user/cjb)
06:08:18 kadir joins (~kadir@88.251.51.100)
06:18:33 × connrs quits (~connrs@user/connrs) (Read error: Connection reset by peer)
06:22:12 acidjnk_new joins (~acidjnk@p200300d6e714dc996547f0aaefed2014.dip0.t-ipconnect.de)
06:22:32 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 260 seconds)
06:23:58 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
06:25:46 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
06:26:20 rvalue joins (~rvalue@user/rvalue)
06:30:34 × TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Excess Flood)
06:32:13 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
06:34:52 × AlexZenon quits (~alzenon@5.139.232.131) (Ping timeout: 246 seconds)
06:41:53 connrs joins (~connrs@user/connrs)
06:45:20 × gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Quit: WeeChat 4.2.2)
06:47:20 gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk)
06:49:32 AlexNoo_ is now known as AlexNoo
06:54:56 × jle` quits (~jle`@2603:8001:3b02:84d4:6e37:aef9:1702:5bd0) (Ping timeout: 268 seconds)
06:55:27 jle` joins (~jle`@2603:8001:3b02:84d4:f1eb:615d:e4c3:d09c)
06:56:05 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 240 seconds)
06:56:18 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
06:58:02 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
06:59:11 gmg joins (~user@user/gehmehgeh)
07:08:40 × billchenchina quits (~billchenc@103.152.35.21) (Remote host closed the connection)
07:09:57 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
07:10:59 sord937 joins (~sord937@gateway/tor-sasl/sord937)
07:17:51 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 255 seconds)
07:18:32 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
07:22:05 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 240 seconds)
07:27:17 × zetef quits (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Ping timeout: 240 seconds)
07:27:36 Nixkernal joins (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch)
07:28:59 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
07:33:22 × gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds)
07:34:05 gmg joins (~user@user/gehmehgeh)
07:37:11 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
07:38:16 superbil joins (~superbil@1-34-176-171.hinet-ip.hinet.net)
07:46:01 × superbil quits (~superbil@1-34-176-171.hinet-ip.hinet.net) (Quit: WeeChat 4.2.2)
07:48:45 libertyprime joins (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz)
07:54:08 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
07:55:30 bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
08:08:13 shachaf_ is now known as shachaf
08:08:36 × shachaf quits (~shachaf@li227-219.members.linode.com) (Changing host)
08:08:36 shachaf joins (~shachaf@user/shachaf)
08:11:17 Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
08:13:12 × libertyprime quits (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Quit: leaving)
08:16:38 superbil joins (~superbil@1-34-176-171.hinet-ip.hinet.net)
08:18:39 mesaoptimizer joins (~mesaoptim@user/PapuaHardyNet)
08:26:04 wootehfoot joins (~wootehfoo@user/wootehfoot)
08:27:11 × TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Excess Flood)
08:29:35 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
08:33:05 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
08:36:02 × TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Excess Flood)
08:38:21 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
08:43:43 wootehfoot joins (~wootehfoo@user/wootehfoot)
08:54:17 danza joins (~francesco@151.47.77.65)
08:54:25 danse-nr3 joins (~danse-nr3@151.47.77.65)
08:54:48 × danse-nr3 quits (~danse-nr3@151.47.77.65) (Remote host closed the connection)
08:55:12 danse-nr3 joins (~danse-nr3@151.47.77.65)
08:55:18 × danse-nr3 quits (~danse-nr3@151.47.77.65) (Client Quit)
09:08:22 siw5ohs0 joins (~aiw5ohs0@user/aiw5ohs0)
09:08:40 × danza quits (~francesco@151.47.77.65) (Ping timeout: 260 seconds)
09:09:20 siw5ohs0 parts (~aiw5ohs0@user/aiw5ohs0) (Leaving)
09:09:42 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
09:11:17 ncf_ is now known as ncf
09:21:54 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
09:24:15 wootehfoot joins (~wootehfoo@user/wootehfoot)
09:28:39 danza joins (~francesco@151.47.77.65)
09:30:41 todi1 is now known as todi
09:42:29 × causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1)
09:43:34 × califax quits (~califax@user/califx) (Ping timeout: 260 seconds)
09:44:52 califax joins (~califax@user/califx)
09:49:39 fendor joins (~fendor@2a02:8388:1605:ce00:24e2:c141:1f86:a346)
09:50:18 sukbeom parts (~sukbeom@121.172.255.83) (The Lounge - https://thelounge.chat)
10:01:11 × danza quits (~francesco@151.47.77.65) (Ping timeout: 264 seconds)
10:01:18 ChanServ sets mode +o ski
10:01:21 ski sets mode -Ro ski
10:04:05 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 240 seconds)
10:06:03 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
10:08:04 __monty__ joins (~toonn@user/toonn)
10:12:47 × califax quits (~califax@user/califx) (Remote host closed the connection)
10:13:33 califax joins (~califax@user/califx)
10:25:59 sawilagar joins (~sawilagar@user/sawilagar)
11:02:35 Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
11:02:47 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds)
11:03:56 Lord_of_Life_ is now known as Lord_of_Life
11:08:55 nefercheprure is now known as TMA
11:14:00 × patrl quits (~patrl@user/patrl) (Remote host closed the connection)
11:15:50 patrl joins (~patrl@user/patrl)
11:22:49 × FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
11:24:54 FinnElija joins (~finn_elij@user/finn-elija/x-0085643)
11:29:59 × Rodney_ quits (~Rodney@176.254.244.83) (Ping timeout: 252 seconds)
11:30:54 × Athas quits (athas@2a01:7c8:aaac:1cf:3ae1:f43a:30e:d1d8) (Quit: ZNC 1.8.2 - https://znc.in)
11:32:28 Athas joins (athas@2a01:7c8:aaac:1cf:3ae1:f43a:30e:d1d8)
11:43:00 Rodney_ joins (~Rodney@176.254.244.83)
11:59:06 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds)
12:02:44 euleritian joins (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de)
12:05:04 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 260 seconds)
12:06:30 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
12:06:45 × driib3 quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
12:07:47 driib3 joins (~driib@vmi931078.contaboserver.net)
12:18:36 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 260 seconds)
12:19:31 × driib3 quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
12:20:21 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
12:26:37 driib3 joins (~driib@vmi931078.contaboserver.net)
12:38:05 waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
12:40:05 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 240 seconds)
12:42:09 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
12:43:12 × driib3 quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
12:45:16 driib3 joins (~driib@vmi931078.contaboserver.net)
12:47:09 × superbil quits (~superbil@1-34-176-171.hinet-ip.hinet.net) (Ping timeout: 265 seconds)
12:47:56 × ft quits (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving)
13:00:33 superbil joins (~superbil@1-34-176-171.hinet-ip.hinet.net)
13:11:33 danza joins (~francesco@rm-19-59-215.service.infuturo.it)
13:15:14 ft joins (~ft@p508db8fc.dip0.t-ipconnect.de)
13:21:34 target_i joins (~target_i@user/target-i/x-6023099)
13:30:41 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
13:49:23 joeyadams joins (~joeyadams@2603:6010:5100:2ed:b273:9497:4ffe:5456)
13:51:35 × euleritian quits (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Ping timeout: 264 seconds)
13:51:41 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 240 seconds)
13:52:18 euleritian joins (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de)
13:59:54 × euleritian quits (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
14:00:11 euleritian joins (~euleritia@p200300d40f4af8000124b0e3dde43af2.dip0.t-ipconnect.de)
14:01:07 × sefidel quits (~sefidel@user/sefidel) (Remote host closed the connection)
14:02:00 sefidel joins (~sefidel@user/sefidel)
14:09:02 gmg joins (~user@user/gehmehgeh)
14:18:44 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
14:20:50 gmg joins (~user@user/gehmehgeh)
14:21:15 × xdminsy quits (~xdminsy@117.147.70.240) (Quit: Konversation terminated!)
14:21:41 xdminsy joins (~xdminsy@117.147.70.240)
14:21:47 × Athas quits (athas@2a01:7c8:aaac:1cf:3ae1:f43a:30e:d1d8) (Quit: ZNC 1.8.2 - https://znc.in)
14:21:57 Athas joins (athas@sigkill.dk)
14:33:41 × euleritian quits (~euleritia@p200300d40f4af8000124b0e3dde43af2.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
14:34:25 euleritian joins (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de)
14:46:53 waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
14:51:31 gensyst joins (~gensyst@user/gensyst)
14:53:15 × danza quits (~francesco@rm-19-59-215.service.infuturo.it) (Quit: Leaving)
14:59:55 × euleritian quits (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
15:00:10 euleritian joins (~euleritia@p200300d40f4af800405d8730c55eda43.dip0.t-ipconnect.de)
15:04:05 × euleritian quits (~euleritia@p200300d40f4af800405d8730c55eda43.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
15:08:57 euleritian joins (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de)
15:18:32 × euleritian quits (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
15:18:43 euleritian joins (~euleritia@p200300d40f4af80011ef9d47c01a966a.dip0.t-ipconnect.de)
15:25:50 random-jellyfish joins (~developer@user/random-jellyfish)
15:27:23 Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
15:27:28 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
15:34:45 × xdminsy quits (~xdminsy@117.147.70.240) (Read error: Connection reset by peer)
15:35:13 × random-jellyfish quits (~developer@user/random-jellyfish) (Quit: Leaving)
15:36:07 xdminsy joins (~xdminsy@117.147.70.240)
15:49:41 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 240 seconds)
16:00:16 × gensyst quits (~gensyst@user/gensyst) (Quit: Leaving)
16:00:25 econo_ joins (uid147250@id-147250.tinside.irccloud.com)
16:04:22 × gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds)
16:05:56 × superbil quits (~superbil@1-34-176-171.hinet-ip.hinet.net) (Read error: Connection reset by peer)
16:21:30 superbil joins (~superbil@1-34-176-171.hinet-ip.hinet.net)
16:24:02 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
16:24:05 × bollu quits (~bollu@159.65.151.13) (Quit: Ping timeout (120 seconds))
16:25:33 chiselfuse joins (~chiselfus@user/chiselfuse)
16:27:37 bollu joins (~bollu@159.65.151.13)
16:29:02 tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
16:33:34 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
16:42:19 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
16:42:55 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
16:46:15 petrichor joins (~znc-user@user/petrichor)
16:53:05 × L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer)
16:53:09 ph88 joins (~ph88@2a02:8109:9e26:c800:6411:ca4c:6107:b01c)
17:01:39 × fendor quits (~fendor@2a02:8388:1605:ce00:24e2:c141:1f86:a346) (Remote host closed the connection)
17:02:56 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:11:45 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
17:19:26 × joeyadams quits (~joeyadams@2603:6010:5100:2ed:b273:9497:4ffe:5456) (Quit: Leaving)
17:20:58 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:21:17 × ph88 quits (~ph88@2a02:8109:9e26:c800:6411:ca4c:6107:b01c) (Ping timeout: 240 seconds)
17:26:30 Square joins (~Square@user/square)
17:26:53 × euleritian quits (~euleritia@p200300d40f4af80011ef9d47c01a966a.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
17:31:06 euleritian joins (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de)
17:35:29 Sgeo joins (~Sgeo@user/sgeo)
17:37:47 mikess joins (~mikess@user/mikess)
17:42:15 visilii_ is now known as visilii
17:45:44 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
17:50:11 justsomeguy joins (~justsomeg@user/justsomeguy)
17:50:58 <justsomeguy> How do I use the Data.Array.IArray.ixmap function? I don't see any examples in the documentation.
17:52:19 <justsomeguy> I have an array a = array (0,2) [(0,'a'),(1,'b'),(2,'c')] :: Array Int Char and am trying to map (+1) to each index in the array.
17:52:37 <glguy> ixmap (0,2) (+1) a
17:52:50 <glguy> oh, I guess you'd want:
17:52:53 aryah joins (~aryah@52-123.dsl.iskon.hr)
17:52:55 <glguy> ixmap (1,3) (+1) a
17:53:05 <glguy> that is tricky
17:53:14 <ncf> nope
17:53:17 <glguy> otherway
17:53:18 <glguy> subtrace 1
17:53:20 <glguy> subtract 1
17:53:22 <ncf> ixmap (1, 3) (subtract 1) a
17:53:52 <ncf> :t ixmap
17:53:53 <lambdabot> (Ix i, Ix j) => (i, i) -> (i -> j) -> Array j e -> Array i e
17:54:09 <ncf> "what bounds do you want", "how do you get back to the old indices"
17:54:18 <mauke> justsomeguy: what do you mean by "map (+1) to each index"?
17:54:20 y04nn joins (~username@45.129.56.202)
17:55:49 <ncf> surprised there isn't a lens combinator that takes an Iso
17:55:56 <aryah> there's a contradiction in the 'extensions lifecycle' proposal (601). explaining experimental, it says "an Experimental extension must be Deprecated prior to removal", but then they recently expanded the section "transitions that are possible but left at the discretion of implementers..." with Experimental -> (does not exist)
17:56:09 <ncf> apply it backwards to the bounds to determine the new bounds, then forwards to get the elements
17:56:36 <justsomeguy> I was expecting to use ixmap (0,2) (+1) a to create a new Array like array (1,3) [(1,'a'),(2,'b'),(3,'c')]. But honestly I'm not sure what ixmap does and I'm just trying to go through each function in IArray and try them out on sample inputs.
17:56:37 <ncf> well i guess your Iso would need to be well-behaved
17:56:50 <aryah> soo, which is it? I guess the latter, but the text should surely be consistent before acceptence.
17:57:00 <ncf> justsomeguy: read the type carefully
17:57:02 <geekosaur> aryah, that might best be posted to the proposal issue?
17:57:18 <mauke> justsomeguy: ah, then what ncf said
17:57:39 <aryah> yeah, prob, I didn't want to need to dig up my github acc...
17:58:05 <geekosaur> I use a password manager to keep track of such things 🙂
17:58:34 <ncf> the function creates an array with the given bounds, then applies the function to each *new* index to get the element corresponding to that index from the old array
17:59:01 <aryah> hahah, yeah, well it was a bad accident with my credentials overall tbh.
17:59:12 <ncf> so if you want to apply some transformation f to the indices, you need to apply f to the bounds and give f⁻¹ as the mapping
18:03:20 <justsomeguy> I'm 100% lost.
18:04:08 <justsomeguy> So, the first argument is a range of indices supplied as a tulpe, right?
18:04:24 <justsomeguy> And they you provide a unary function to manipulate each index.
18:04:34 <justsomeguy> and the last argument is an Array.
18:04:43 <justsomeguy> (an IArray, sorry)
18:05:00 <justsomeguy> What is a bounds?
18:05:12 <ncf> first and last index
18:05:26 <ncf> (0, 2) in your `a`
18:11:15 <justsomeguy> So when I run b = ixmap (1,1) (+1) a I get array (1,1) [(1,'c')]. Now I have a = array (0,2) [(0,'a'),(1,'b'),(2,'c')] and b = array (1,1) [(1,'c')].
18:12:08 <ncf> as expected
18:13:25 <monochrom> (1,1) means an array of length 1, the only index being 1.
18:13:52 <justsomeguy> Oh man... I thought the first element of the tuple was the starting index, not the length.
18:14:01 <EvanR> justsomeguy, the resulting array effectively uses a function on the incoming index to get the value
18:14:02 <ncf> it is the starting index
18:14:08 <ncf> and the second one is the last index
18:14:12 <ncf> > [1..1]
18:14:14 <lambdabot> [1]
18:14:26 <monochrom> And I guess also b ! i = a ! (i+1) as you specified (+1).
18:14:53 <monochrom> Eh, if anything, I would expect length to be second, not first. :)
18:15:00 <EvanR> r[i] = a[f(i)]
18:15:16 <ncf> (length wouldn't make sense for higher-dimensional arrays)
18:17:27 <justsomeguy> So would I only use ixmap to get subranges of the input IArray? I don't see how else I could use it. I guess it depends on what type you chose as your index.
18:18:34 <ncf> <ncf> ixmap (1, 3) (subtract 1) a
18:18:38 <ncf> doesn't look like a subrange to me
18:22:13 <monochrom> There is no dedicated subrange function, so yeah ixmap with id is one solution. But you can also try array (3,5) [ (i, a ! i) | i <- [3..5] ]
18:25:50 × destituion quits (~destituio@2a02:2121:10b:62ca:10a5:f759:7fb5:9fb1) (Ping timeout: 256 seconds)
18:26:08 <mauke> ixmap can be used to give you a permutation of the input array
18:29:29 <ski> > fmap getSum (ximap (0,9) (^ 2) (L.tabulate (-3,3) (\i -> Sum (i^2))))
18:29:30 <lambdabot> array (0,9) [(0,0),(1,2),(2,0),(3,0),(4,8),(5,0),(6,0),(7,0),(8,0),(9,18)]
18:30:04 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds)
18:31:19 kaol_ is now known as kaol
18:31:39 <ncf> :t ximap
18:31:40 <lambdabot> (Ix i, Ix j, Monoid e) => (j, j) -> (i -> j) -> Array i e -> Array j e
18:32:16 <ncf> nice
18:33:01 <ski> covariant rather than contravariant, over map with finite support
18:33:56 <ncf> is this a Kan extension
18:36:26 <ski> > ixmap (-3,3) (^ 2) (L.tabulate (0,9) (\j -> 2*j)) -- not just subrange or selection, but also replication
18:36:28 <lambdabot> array (-3,3) [(-3,18),(-2,8),(-1,2),(0,0),(1,2),(2,8),(3,18)]
18:36:47 ski . o O ( <https://en.wikipedia.org/wiki/Monoid_ring> )
18:36:47 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
18:37:10 <justsomeguy> What do covariant and contravariant mean?
18:37:42 <ski> ncf : not sure
18:38:05 × euleritian quits (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Ping timeout: 240 seconds)
18:38:06 <ski> justsomeguy : covariant means "varies in the same direction", and contravariant means "varies in the opposite direction"
18:38:12 <mauke> ...
18:38:27 wootehfoot joins (~wootehfoo@user/wootehfoot)
18:39:07 <ncf> as with functors: covariant is fmap :: (a -> b) -> f a -> f b, contravariant is contramap :: (a -> b) -> f b -> f a
18:39:24 <ski> justsomeguy : for `fmap :: (a -> b) -> (Array i a -> Array i b)', we provide a function from `a' elements to `b' elements, and gets back a function from `a' arrays to `b' arrays .. so both functions, the element function, and the array function, go in the same direction
18:39:48 <ncf> in this case the functor under consideration is (`Array` e)
18:40:09 <ski> justsomeguy : ditto for my `ximap', you provide `i -> j' and get back `Array i e -> Array j e', so both are going in the same direction, still
18:40:54 <ski> justsomeguy : but for `ixmap', you provide `j -> i', getting back `Array i e -> Array j e', so here we're *reversing* direction ! hence, *contra*variant, in this case
18:43:59 <ski> justsomeguy : some kind of thing comes up in Object-orientation, with subtyping. you can have a method (in a subclass) that possibly returns an object that's a subtype of the return type of the object in the superclass. so in superclass `C' you can have `T foo(Blah blah);', and in subclass `D', you can, if you want, instead have `U foo(Blah blah);' as long as `U' is a subtype of `T'. because every object of
18:44:05 <ski> type `U' also has type `T'. this means that method return types are covariant
18:45:20 <EvanR> OOP. foo Blah blah
18:46:25 <ski> however, if we instead look at argument/parameter types, say we have `void bar(U obj);' in `C', then we could have `void bar(T obj);' in `D'. because a `D' is supposed to be a `C' (you can pass a `D' object to where a `C' object is expected), `bar' in `D' will always have to be prepared for people sending `U's to it, we can't replace `U' with a subtype of `U', in the subclass `D'. we *can* replace `U' with
18:46:31 <ski> a *supertype* `T', though, allowing `bar' in `D' to accept *more* types of objects than the original `bar' in `C'
18:46:58 <ski> so, this is contravariant
18:47:35 <ski> s/some kind/same kind/
18:49:51 <ski> btw, if you have mutable arrays, then `U[]' is neither a subtype nor a supertype of `T[]', when `U' is a subtype of `T'. this is because we can both read (output) from arrays (which is covariant), and write (input) to arrays (which is contravariant). so saying `Bike[]' is a subtype of `Vehicle[]' is wrong, if the array is mutable
18:50:22 <ski> for methods (and functions in general), the inputs (arguments/parameters) are contravariant, and the output (result) is covariant
18:51:06 <aryah> ski: ty, a very clear explanation, I wondered the same a few times
18:51:37 <ski> there are various other words that are also used. covariant : order-preserving, increasing, monotone, upper. contravariant : order-reversing, decreasing, antitone, lower
18:51:59 <ski> aryah : happy it made sense
18:53:18 <ski> oh, also "positive (position)" for covariant, and "negative (position)" for contravariant
18:53:36 <ski> (think about rules like "positive times positive is positive", "positive times negative is negative", ..)
18:54:14 <mauke> ArrayStoreException
18:54:34 <ski> in `a -> Maybe b', `b' is in positive (output/result/covariant) position, while `a' is in negative (input/argument/parameter/contravariant) position
18:55:58 <ski> and in `(a -> Bool) -> Bool', `a' is again in positive position. if you have `test :: (T -> Bool) -> Bool', then this function `test' in some sense "contains" a number of `T' values (they're "output", although only indirectly, from the function `test'. you can only "prod" at them by providing predicate callbacks)
18:56:05 × y04nn quits (~username@45.129.56.202) (Ping timeout: 240 seconds)
18:56:26 <ski> e.g. we could have `test p = p t0 && (p t1 || not (p t2))', for some `t0,t1,t2 :: T'
18:56:36 <mauke> if you're familiar with C, T *ptr automatically converts to const T *, but T **ptr does not convert to const T **
18:56:39 <mauke> this is because of reasons
18:56:43 <monochrom> The beauty is that neg times neg is pos too. For example in ((X -> Int) -> Int), X is at a positive covariant position, because it's neg of neg.
18:57:27 <ski> mauke : yea, Java messed this up
19:05:43 destituion joins (~destituio@2a02:2121:607:127a:483a:846b:b497:f738)
19:05:55 raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
19:09:03 y04nn joins (~username@2a03:1b20:8:f011::e10d)
19:11:43 <ski> (oh, and this about contra- and co- variance of inputs/arguments and outputs/results also relates to preconditions and postconditions. if you strengthen the postcondition (make it more demanding), you strengthen the whole contract. but if you strengthen the precondition (make it more demanding), you *weaken* the whole contract, because now you're allowing fewer things to be passed to the operation, you're
19:11:49 <ski> only considering fewer situations, so it's easier, not harder, to implement this overall weakened contract)
19:12:03 euleritian joins (~euleritia@p200300d40f4af8006c29977101d489e2.dip0.t-ipconnect.de)
19:14:34 <mauke> for example, it is very hard to prove "all naturals numbers are odd". but if you strengthen the precondition, like "all prime numbers are odd", it gets much easier to prove.
19:15:44 <int-e> mauke: ahem
19:15:49 <ncf> lol
19:16:01 <EvanR> all prime numbers worth their salt
19:16:15 <EvanR> all proper prime numbers
19:16:35 <int-e> (I'd like to say that I have two reasons speaking against that but it's really just one.)
19:16:51 <mauke> how odd
19:17:06 <ncf> so i guess any map f : A → M into a monoid can be extended along g : A → B as b ↦ sum(f(g⁻¹(b))) : B → M
19:17:23 <ncf> and ximap is just the restriction of that to maps with finite contiguous domains (arrays)
19:17:27 <ncf> i wonder if this construction has a name
19:17:30 <int-e> mauke: I guess you can try that defense. (That 2 is *the* odd prime.)
19:17:44 <ncf> it's not actually an "extension" proper because the composition doesn't recover f
19:17:53 <EvanR> there's 10 kinds of prime numbers
19:18:01 <EvanR> even and odd
19:18:32 <mauke> there's 10 kinds of people: binary and non-binary
19:21:16 <raehik> I need a `decSNat :: SNat n -> SNat (n-1)` (ignore n=0 case) but I can't incur KnownNat constraints. How do I write this?
19:21:26 <ski> i recall some mathematician saying that two is the oddest of the primes
19:21:52 <Rembane> That's a good quote
19:22:37 <ski> ncf : perhaps it would be nicer with commutative monoids .. but the indices had an order given by `Ix' in this case
19:23:05 <ncf> that's true
19:24:13 L29Ah joins (~L29Ah@wikipedia/L29Ah)
19:24:27 <ski> (like there's results where all odd primes are treated the same way, but you have to treat two differently. commonly this is, on some level, because there's only one (unique !) congruence class modulo two which doesn't contain zero)
19:24:30 <ncf> raehik: withKnownNat?
19:25:18 <ski> @hoogle withKnownNat
19:25:19 <lambdabot> Data.Singletons.TypeLits withKnownNat :: Sing n -> (KnownNat n => r) -> r
19:26:36 <ncf> hmm, i guess it's not clear how to proceed from there
19:26:36 <raehik> ncf: yeah I'm thinking withKnownNat and some unsafeCoerce ing...?
19:28:55 <ncf> could not deduce KnownNat (n - 1) from KnownNat n
19:29:00 <ncf> hmm... is this just GHC being bad
19:29:25 <geekosaur> yes. try the natnormalise plugin, I think?
19:29:59 <geekosaur> or its cousin that I can't recall ottomh
19:32:52 <raehik> geekosaur: I know of ghc-typelits-knownnat
19:33:07 <raehik> if possible I'd like to know how to do it manually too
19:33:11 <geekosaur> that might be it
19:33:24 <geekosaur> afaik it just adds constraints for obvious things like that
19:34:08 <geekosaur> the decision was made at some point that, rather than teach the typechecker things like that, it should be done with plugins (iirc)
19:34:14 <monochrom> Hot take: 3 is the oddest of odd primes.
19:34:51 <ncf> 3 is actually the least odd prime
19:34:58 <monochrom> hahaha
19:36:48 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 260 seconds)
19:37:12 <ncf> not to be confused with 2, the least-odd prime
19:37:46 <Rembane> I think 0 is the roundest of the hot take primes
19:39:05 machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
20:00:15 <raehik> geekosaur: even with that package I need to provide a proof that n >= 1... bleh
20:00:25 waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
20:10:32 × Pixi__ quits (~Pixi@user/pixi) (Quit: Leaving)
20:11:06 Pixi joins (~Pixi@user/pixi)
20:13:11 × Square quits (~Square@user/square) (Ping timeout: 264 seconds)
20:14:04 y04nn joins (~username@2a03:1b20:8:f011::e10d)
20:19:29 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
20:20:30 chiselfuse joins (~chiselfus@user/chiselfuse)
20:20:44 × phma quits (~phma@host-67-44-208-141.hnremote.net) (Read error: Connection reset by peer)
20:21:36 phma joins (~phma@2001:5b0:210d:fcc8:b4c9:7a8c:a02a:3e86)
20:23:41 × euleritian quits (~euleritia@p200300d40f4af8006c29977101d489e2.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
20:24:06 <raehik> geekosaur: turns out I can copy how singletons-base implements singled Natural subtraction, reifying->performing regular subtraction->unsafeCoercing the result
20:24:13 euleritian joins (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de)
20:24:44 <monochrom> >:)
20:27:35 pavonia joins (~user@user/siracusa)
20:27:39 fizbin__ joins (~fizbin@user/fizbin)
20:28:38 × bionade24 quits (~quassel@2a03:4000:33:45b::1) (Quit: Apocalypse Incoming!)
20:28:45 gmg joins (~user@user/gehmehgeh)
20:28:52 bionade24 joins (~quassel@2a03:4000:33:45b::1)
20:29:18 × euleritian quits (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
20:29:30 euleritian joins (~euleritia@p200300d40f4af8005abbe7e2e78f892d.dip0.t-ipconnect.de)
20:34:50 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
20:35:30 × gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds)
20:43:28 gmg joins (~user@user/gehmehgeh)
20:46:30 RedFlamingos joins (~RedFlamin@user/RedFlamingos)
20:46:51 sawilagar joins (~sawilagar@user/sawilagar)
20:47:16 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds)
20:50:40 × qqq quits (~qqq@92.43.167.61) (Remote host closed the connection)
20:52:04 zetef joins (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
20:56:02 × gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds)
21:04:00 × petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
21:07:20 × zetef quits (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Ping timeout: 260 seconds)
21:14:09 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
21:26:03 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
21:31:31 zetef joins (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
21:32:47 edrx joins (~Eduardo@179-191-223-123.static.sumicity.net.br)
21:33:53 <edrx> hi all! I am trying to translate my notes on this
21:33:59 <edrx> do a <- [0,1]; b <- [a+1,a+2]; guard (a+b < 4); return (a,b)
21:34:11 <edrx> to Lean...
21:34:32 × zetef quits (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Read error: Connection reset by peer)
21:34:35 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
21:35:05 <edrx> the translation of [0,1] is not immediate, but I guess that I can find if I find how [0,1] is expanded to f 0 1 for a certain f...
21:35:05 zetef joins (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
21:35:21 <edrx> anyone knows the name of that f?
21:35:31 <mauke> huh?
21:35:43 chiselfuse joins (~chiselfus@user/chiselfuse)
21:36:31 × fizbin__ quits (~fizbin@user/fizbin) (Ping timeout: 260 seconds)
21:36:44 <edrx> if I run seq 2 5 in a shell the output is 2 3 4 5
21:37:04 <edrx> [2,5] in Haskell is syntax sugar for something else
21:37:20 <mauke> yeah, technically it's 2 : (5 : [])
21:37:39 <edrx> I'm trying to find that something else in the source
21:37:43 <edrx> ooops, my fault!
21:37:52 <EvanR> and do notation is expanded to >>= and >> and let
21:38:16 <mauke> but [2,5] is just a two-element list
21:38:18 <mauke> it's not a range
21:38:21 <edrx> I forgot that [2,5] is a list with two elements and not something like 2,3,4,5
21:38:26 <edrx> (embarrased)
21:38:33 fizbin__ joins (~fizbin@user/fizbin)
21:38:33 <EvanR> > [2..5]
21:38:34 <lambdabot> [2,3,4,5]
21:38:42 <edrx> that!!!!
21:38:44 <mauke> > enumFromTo 2 5
21:38:46 <lambdabot> [2,3,4,5]
21:38:55 <edrx> perfect!!! thanks =)
21:39:30 <mauke> @undo do a <- [0,1]; b <- [a+1,a+2]; guard (a+b < 4); return (a,b)
21:39:30 <lambdabot> [0, 1] >>= \ a -> [a + 1, a + 2] >>= \ b -> guard (a + b < 4) >> return (a, b)
21:39:39 <mauke> @. pl undo do a <- [0,1]; b <- [a+1,a+2]; guard (a+b < 4); return (a,b)
21:39:40 <lambdabot> ap ((>>=) . liftM2 (:) (1 +) (return . (2 +))) (ap (ap . (((>>) . guard) .) . flip flip 4 . ((<) .) . (+)) ((return .) . (,))) =<< [0, 1]
21:39:48 <mauke> there. now it's art.
21:40:13 <EvanR> magnificent desolation
21:40:33 <edrx> that's super neat! when I learned that I had to do the translation by hand...
21:41:37 <edrx> is there an easy way to run that translation from a ghci repl?
21:42:20 <mauke> I don't think so
21:42:43 <ski> > (\a o -> [(a,b) | let b = a + o,a+b < 4]) <$> [0,1] <*>> [1,2]
21:42:45 <lambdabot> [(0,1),(0,2),(1,2)]
21:43:28 × zetef quits (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Read error: Connection reset by peer)
21:43:59 zetef joins (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
21:47:44 <ski> it's not to hard to run `undo' in your head
21:48:14 <edrx> when we have practice it is trivial
21:49:11 <geekosaur> you can run lambdabot locally, although installing it is a bit of a pain currently
21:49:20 <ski> you can check the "Translations" part of <https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-470003.14> (and <https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-420003.11> for list comprehensions)
21:49:27 <geekosaur> you can also talk to it in /query
21:50:07 <edrx> let me try
21:50:13 <edrx> ski: thanks =)
21:50:49 × michalz quits (~michalz@185.246.207.193) (Quit: ZNC 1.9.0 - https://znc.in)
21:52:23 × fizbin__ quits (~fizbin@user/fizbin) (Ping timeout: 261 seconds)
21:52:46 <EvanR> lambdabot is a living program, it must be preserved for future generations
21:53:24 michalz joins (~michalz@185.246.207.221)
21:53:29 × michalz quits (~michalz@185.246.207.221) (Remote host closed the connection)
21:53:39 <geekosaur> lambdabot itself is fine. one of its dependencies was never updated for Semigroup, iirc
21:56:17 <edrx> geekosaur: done! I'll have to clean up my script to talk to lambdabot someday, but the ugly prototype works =)
22:01:35 fizbin__ joins (~fizbin@user/fizbin)
22:01:57 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:02:38 × zetef quits (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Remote host closed the connection)
22:02:54 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
22:03:22 × kadir quits (~kadir@88.251.51.100) (Quit: WeeChat 4.2.2)
22:04:10 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
22:05:16 chiselfuse joins (~chiselfus@user/chiselfuse)
22:09:24 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds)
22:13:36 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds)
22:15:00 × aryah quits (~aryah@52-123.dsl.iskon.hr) (Ping timeout: 260 seconds)
22:15:55 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
22:16:52 notzmv joins (~daniel@user/notzmv)
22:29:27 × fizbin__ quits (~fizbin@user/fizbin) (Ping timeout: 256 seconds)
22:46:32 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Remote host closed the connection)
22:46:47 y04nn joins (~username@2a03:1b20:8:f011::e10d)
22:53:16 × euleritian quits (~euleritia@p200300d40f4af8005abbe7e2e78f892d.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
22:54:00 euleritian joins (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de)
23:01:03 × phma quits (~phma@2001:5b0:210d:fcc8:b4c9:7a8c:a02a:3e86) (Read error: Connection reset by peer)
23:01:31 phma joins (~phma@host-67-44-208-131.hnremote.net)
23:01:57 aryah joins (~aryah@141-138-36-145.dsl.iskon.hr)
23:04:01 chiselfu1e joins (~chiselfus@user/chiselfuse)
23:05:46 × chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds)
23:10:03 × acidjnk_new quits (~acidjnk@p200300d6e714dc996547f0aaefed2014.dip0.t-ipconnect.de) (Ping timeout: 255 seconds)
23:11:28 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Ping timeout: 260 seconds)
23:25:49 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
23:52:11 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
23:57:40 × chiselfu1e quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
23:58:44 chiselfuse joins (~chiselfus@user/chiselfuse)

All times are in UTC on 2024-05-18.