2024/05/18

2024-05-18 00:11:08 +0200AlexNoo_(~AlexNoo@5.139.232.131)
2024-05-18 00:13:08 +0200kadir(~kadir@88.251.51.100) (Quit: WeeChat 4.2.2)
2024-05-18 00:14:28 +0200AlexZenon(~alzenon@178.34.162.221) (Ping timeout: 268 seconds)
2024-05-18 00:14:49 +0200AlexNoo(~AlexNoo@178.34.162.221) (Ping timeout: 256 seconds)
2024-05-18 00:15:19 +0200zetef(~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
2024-05-18 00:21:11 +0200ystael(~ystael@user/ystael) (Ping timeout: 256 seconds)
2024-05-18 00:22:47 +0200AlexZenon(~alzenon@5.139.232.131)
2024-05-18 00:26:10 +0200__monty__(~toonn@user/toonn) (Quit: leaving)
2024-05-18 00:26:25 +0200sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 255 seconds)
2024-05-18 00:31:07 +0200jmdaemon(~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds)
2024-05-18 00:46:03 +0200talismanick(~user@2601:644:937c:ed10::ae5)
2024-05-18 00:47:23 +0200m257(~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca)
2024-05-18 00:48:29 +0200 <talismanick> typeclass laws let us make intuitive assumptions about the behavior of any instance satisfying them, but you do have to prove it
2024-05-18 00:48:31 +0200 <talismanick> but, in math, figuring out how to prove something is a big part of understanding it
2024-05-18 00:49:03 +0200 <talismanick> just writing out the proofs for Reader, Writer, and State, I don't feel like I understand anything more for doing so
2024-05-18 00:58:08 +0200yin(~yin@user/zero) (Remote host closed the connection)
2024-05-18 01:01:01 +0200 <monochrom> I would not take "prove implies understanding" religiously. When it works, it works. When it doesn't, it doesn't, or at most maybe look for another proof approach that brings understanding.
2024-05-18 01:02:36 +0200 <monochrom> Hell, in fact, we know in math of a lot of elementary proofs that only achieve being elementary, not furthering understanding, precisely because they avoid "advanced" structures that bring understanding.
2024-05-18 01:07:07 +0200 <talismanick> what are some instances with nontrivial proofs?
2024-05-18 01:08:04 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-05-18 01:09:52 +0200ski. o O ( "Mathematics, morally" by Eugenia Cheng in 2004-01 at <https://eugeniacheng.com/wp-content/uploads/2017/02/cheng-morality.pdf> )
2024-05-18 01:15:58 +0200acidjnk_new(~acidjnk@p200300d6e714dc64113083a2457f0359.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
2024-05-18 01:17:08 +0200zetef(~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Remote host closed the connection)
2024-05-18 01:17:58 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex)
2024-05-18 01:18:54 +0200 <dolio> I've been reading a book with some people, and it seems like most of the proofs are less believable than the facts they state.
2024-05-18 01:21:31 +0200Lycurgus(~georg@user/Lycurgus)
2024-05-18 01:21:47 +0200 <Lycurgus> 'understanding' - that's a feel innit?
2024-05-18 01:22:41 +0200 <Lycurgus> a feel of cognition
2024-05-18 01:24:24 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer)
2024-05-18 01:24:37 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf)
2024-05-18 01:25:08 +0200 <Lycurgus> feel, qualia, obscure thing
2024-05-18 01:26:05 +0200 <Lycurgus> without qualification that is; demonstrated understanding brings you back
2024-05-18 01:27:00 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-05-18 01:40:05 +0200 <Hecate> tomsmeding: eyo, do you want a PR to enable linear-base for GHC 9.10 on the playground?
2024-05-18 01:40:31 +0200Lycurgus(~georg@user/Lycurgus) (Quit: leaving)
2024-05-18 01:42:17 +0200 <ski> presumably understanding is objective insofar as it allows someone to better predict, diagnose, design
2024-05-18 01:54:55 +0200internatetional(~nate@2001:448a:20a3:c2e5:9ba2:a48e:b934:7d97) (Quit: WeeChat 4.2.2)
2024-05-18 01:55:43 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2024-05-18 02:00:25 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
2024-05-18 02:13:18 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds)
2024-05-18 02:14:50 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex)
2024-05-18 02:49:47 +0200m257(~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) (Ping timeout: 252 seconds)
2024-05-18 02:58:35 +0200y04nn(~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds)
2024-05-18 03:06:34 +0200otto_s(~user@p5b0448c7.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
2024-05-18 03:08:24 +0200otto_s(~user@p5b044b71.dip0.t-ipconnect.de)
2024-05-18 03:14:35 +0200Ranhir(~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/)
2024-05-18 03:14:37 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds)
2024-05-18 03:15:40 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:cfe3:13e2:96f6:9d2c) (Quit: Leaving)
2024-05-18 03:35:59 +0200addfb3(~dante@user/addfb3) (Ping timeout: 256 seconds)
2024-05-18 03:40:46 +0200Ranhir(~Ranhir@157.97.53.139)
2024-05-18 04:00:02 +0200fliife(~fliife@user/fliife) (Quit: ZNC 1.8.2+deb2build5 - https://znc.in)
2024-05-18 04:00:50 +0200fliife(~fliife@user/fliife)
2024-05-18 04:05:43 +0200m257(~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca)
2024-05-18 04:05:57 +0200dyniec(~dyniec@dybiec.info) (Quit: WeeChat 4.1.1)
2024-05-18 04:09:34 +0200td_(~td@i53870915.versanet.de) (Ping timeout: 246 seconds)
2024-05-18 04:11:28 +0200td_(~td@i53870939.versanet.de)
2024-05-18 04:12:28 +0200tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving)
2024-05-18 04:14:16 +0200tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303)
2024-05-18 04:18:03 +0200cjb(~cjb@user/cjb)
2024-05-18 04:21:45 +0200ringo___(~ringo@157.230.117.128) (Ping timeout: 268 seconds)
2024-05-18 04:22:22 +0200Athas(athas@sigkill.dk) (Ping timeout: 268 seconds)
2024-05-18 04:22:34 +0200Athas(athas@2a01:7c8:aaac:1cf:3ae1:f43a:30e:d1d8)
2024-05-18 04:23:32 +0200ringo___(~ringo@157.230.117.128)
2024-05-18 04:24:08 +0200kimiamania(~76637481@user/kimiamania) (Quit: Ping timeout (120 seconds))
2024-05-18 04:24:31 +0200kimiamania(~76637481@user/kimiamania)
2024-05-18 04:28:32 +0200bwe(~bwe@2a01:4f8:1c1c:4878::2) (Ping timeout: 268 seconds)
2024-05-18 04:28:32 +0200mesaoptimizer(~mesaoptim@user/PapuaHardyNet) (Ping timeout: 268 seconds)
2024-05-18 04:28:40 +0200bwe(~bwe@2a01:4f8:1c1c:4878::2)
2024-05-18 04:40:52 +0200 <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
2024-05-18 04:41:03 +0200 <talismanick> exercise*
2024-05-18 04:44:03 +0200Axman6(~Axman6@user/axman6) (Ping timeout: 264 seconds)
2024-05-18 04:49:33 +0200 <talismanick> I guess it's natural for typeclass law proofs to be impervious to intuition because metaproofs are apt to be like that?
2024-05-18 04:50:35 +0200cheater_(~Username@user/cheater)
2024-05-18 04:51:52 +0200ridcully_(~ridcully@p508ac2b4.dip0.t-ipconnect.de)
2024-05-18 04:52:53 +0200connrs(~connrs@user/connrs) (Ping timeout: 268 seconds)
2024-05-18 04:52:56 +0200hexeme_(~hexeme@user/hexeme)
2024-05-18 04:53:05 +0200fiddlerw-(~fiddlerwo@user/fiddlerwoaroof)
2024-05-18 04:53:59 +0200lbseale_(~quassel@user/ep1ctetus)
2024-05-18 04:54:08 +0200swistak-(~swistak@185.21.216.141)
2024-05-18 04:54:11 +0200gawen_(~gawen@user/gawen)
2024-05-18 04:54:17 +0200johnw_(~johnw@69.62.242.138)
2024-05-18 04:54:39 +0200ocra8_(ocra8@user/ocra8)
2024-05-18 04:54:57 +0200tessier(~treed@ec2-184-72-149-67.compute-1.amazonaws.com)
2024-05-18 04:55:15 +0200kmein_(~weechat@user/kmein)
2024-05-18 04:55:20 +0200defanor_(~defanor@tart.uberspace.net)
2024-05-18 04:55:20 +0200weechat(~weechat@user/dminuoso)
2024-05-18 04:55:43 +0200tolt_(~weechat-h@li219-154.members.linode.com)
2024-05-18 04:56:24 +0200todi1(~todi@p57803331.dip0.t-ipconnect.de)
2024-05-18 04:56:30 +0200Eoco(~ian@128.101.131.218)
2024-05-18 04:56:33 +0200deriamis_(deriamis@ec2-54-187-167-69.us-west-2.compute.amazonaws.com)
2024-05-18 04:56:39 +0200zlqrvx_(~zlqrvx@101.175.150.247)
2024-05-18 04:57:28 +0200CodeKiwi(~kiwi@137.184.156.191)
2024-05-18 04:58:43 +0200flounders_(~flounders@24.246.176.178)
2024-05-18 04:59:00 +0200teqwve-(teqwve@static.141.38.201.195.clients.your-server.de)
2024-05-18 04:59:08 +0200sand-witch_(~m-mzmz6l@vmi833741.contaboserver.net)
2024-05-18 05:00:45 +0200johnw(~johnw@69.62.242.138) (*.net *.split)
2024-05-18 05:00:45 +0200ocra8(ocra8@user/ocra8) (*.net *.split)
2024-05-18 05:00:45 +0200todi(~todi@p57803331.dip0.t-ipconnect.de) (*.net *.split)
2024-05-18 05:00:45 +0200deriamis(deriamis@ec2-54-187-167-69.us-west-2.compute.amazonaws.com) (*.net *.split)
2024-05-18 05:00:45 +0200gawen(~gawen@user/gawen) (*.net *.split)
2024-05-18 05:00:45 +0200foul_owl(~kerry@185.219.141.164) (*.net *.split)
2024-05-18 05:00:46 +0200DigitalKiwi(~kiwi@137.184.156.191) (*.net *.split)
2024-05-18 05:00:46 +0200cheater(~Username@user/cheater) (*.net *.split)
2024-05-18 05:00:46 +0200acarrico(~acarrico@dhcp-68-142-49-163.greenmountainaccess.net) (*.net *.split)
2024-05-18 05:00:46 +0200tessier_(~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (*.net *.split)
2024-05-18 05:00:46 +0200Eoco_(~ian@128.101.131.218) (*.net *.split)
2024-05-18 05:00:46 +0200tolt(~weechat-h@li219-154.members.linode.com) (*.net *.split)
2024-05-18 05:00:46 +0200flounders(~flounders@24.246.176.178) (*.net *.split)
2024-05-18 05:00:46 +0200sand-witch(~m-mzmz6l@vmi833741.contaboserver.net) (*.net *.split)
2024-05-18 05:00:46 +0200fiddlerwoaroof(~fiddlerwo@user/fiddlerwoaroof) (*.net *.split)
2024-05-18 05:00:46 +0200kmein(~weechat@user/kmein) (*.net *.split)
2024-05-18 05:00:46 +0200teqwve(teqwve@static.141.38.201.195.clients.your-server.de) (*.net *.split)
2024-05-18 05:00:46 +0200zlqrvx(~zlqrvx@user/zlqrvx) (*.net *.split)
2024-05-18 05:00:46 +0200ridcully(~ridcully@p508ac2b4.dip0.t-ipconnect.de) (*.net *.split)
2024-05-18 05:00:46 +0200swistak(~swistak@185.21.216.141) (*.net *.split)
2024-05-18 05:00:46 +0200df(~ben@justworks.xyz) (*.net *.split)
2024-05-18 05:00:46 +0200lbseale(~quassel@user/ep1ctetus) (*.net *.split)
2024-05-18 05:00:46 +0200defanor-(~defanor@tart.uberspace.net) (*.net *.split)
2024-05-18 05:00:46 +0200dminuoso(~weechat@user/dminuoso) (*.net *.split)
2024-05-18 05:00:46 +0200hexeme(~hexeme@user/hexeme) (*.net *.split)
2024-05-18 05:00:54 +0200cheater_cheater
2024-05-18 05:03:59 +0200 <dolio> No, propositions are types.
2024-05-18 05:04:01 +0200sand-witch_sand-witch
2024-05-18 05:04:13 +0200 <dolio> It's better if you don't read it the opposite way.
2024-05-18 05:04:45 +0200df(~ben@justworks.xyz)
2024-05-18 05:10:02 +0200m257(~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) (Ping timeout: 252 seconds)
2024-05-18 05:10:19 +0200foul_owl(~kerry@71.212.149.206)
2024-05-18 05:10:49 +0200acarrico(~acarrico@dhcp-68-142-49-163.greenmountainaccess.net)
2024-05-18 05:23:53 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-05-18 05:27:55 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-05-18 05:38:06 +0200Pixi__(~Pixi@user/pixi)
2024-05-18 05:39:03 +0200cpli_(77fc530071@2a03:6000:1812:100::252)
2024-05-18 05:39:13 +0200bw______(sid2730@id-2730.ilkley.irccloud.com)
2024-05-18 05:40:06 +0200cpli(77fc530071@2a03:6000:1812:100::252) (Ping timeout: 240 seconds)
2024-05-18 05:40:06 +0200bw_____(sid2730@id-2730.ilkley.irccloud.com) (Ping timeout: 240 seconds)
2024-05-18 05:40:12 +0200lukec_(9dfd4d094e@2a03:6000:1812:100::10e)
2024-05-18 05:40:18 +0200cpli_cpli
2024-05-18 05:40:18 +0200dy_(sid3438@user/dy)
2024-05-18 05:40:42 +0200davetapley_(sid666@id-666.uxbridge.irccloud.com)
2024-05-18 05:41:31 +0200Goodbye_Vincent1(cyvahl@freakshells.net)
2024-05-18 05:41:46 +0200fluffyballoon_(45ce440a48@2a03:6000:1812:100::e2)
2024-05-18 05:41:51 +0200shreyasminocha_(51fdc93eda@user/shreyasminocha)
2024-05-18 05:41:53 +0200sgarcia(sgarcia@swarm.znchost.com)
2024-05-18 05:42:08 +0200integral_(sid296274@user/integral)
2024-05-18 05:42:13 +0200systemfault_(sid267009@about/typescript/member/systemfault)
2024-05-18 05:42:25 +0200ell6(~ellie@user/ellie)
2024-05-18 05:42:56 +0200coldtom4(~coldtom@coldrick.cc)
2024-05-18 05:43:09 +0200filwisher_(2e6936c793@2a03:6000:1812:100::170)
2024-05-18 05:43:21 +0200gaze___(sid387101@id-387101.helmsley.irccloud.com)
2024-05-18 05:43:28 +0200aspen_(sid449115@id-449115.helmsley.irccloud.com)
2024-05-18 05:43:46 +0200chessai_(sid225296@id-225296.lymington.irccloud.com)
2024-05-18 05:44:02 +0200amir_(sid22336@user/amir)
2024-05-18 05:44:10 +0200scav_(sid309693@user/scav)
2024-05-18 05:44:17 +0200piele_(~piele@tbonesteak.creativeserver.net)
2024-05-18 05:44:27 +0200kuruczgy_(55b66dd3ae@2a03:6000:1812:100::127f)
2024-05-18 05:44:30 +0200dy(sid3438@user/dy) (Ping timeout: 240 seconds)
2024-05-18 05:44:30 +0200lukec(9dfd4d094e@2a03:6000:1812:100::10e) (Ping timeout: 240 seconds)
2024-05-18 05:44:30 +0200fluffyballoon(45ce440a48@2a03:6000:1812:100::e2) (Ping timeout: 240 seconds)
2024-05-18 05:44:30 +0200davetapley(sid666@id-666.uxbridge.irccloud.com) (Ping timeout: 240 seconds)
2024-05-18 05:44:30 +0200dy_dy
2024-05-18 05:44:30 +0200lukec_lukec
2024-05-18 05:44:30 +0200fluffyballoon_fluffyballoon
2024-05-18 05:44:31 +0200davetapley_davetapley
2024-05-18 05:44:40 +0200jleightcap_(7bc4014b62@user/jleightcap)
2024-05-18 05:44:51 +0200Ankhers_(e99e97ef8e@2a03:6000:1812:100::2a2)
2024-05-18 05:44:56 +0200jmcantrell_(644f1bed9a@user/jmcantrell)
2024-05-18 05:44:57 +0200remexre_(~remexre@user/remexre)
2024-05-18 05:45:01 +0200Vq_(~vq@81-231-76-8-no600.tbcn.telia.com)
2024-05-18 05:45:03 +0200pounce_(~pounce@user/cute/pounce)
2024-05-18 05:45:04 +0200fgaz__(1ff9197ed6@2a03:6000:1812:100::11ea)
2024-05-18 05:45:18 +0200constxqt(~constxd@user/constxd)
2024-05-18 05:45:22 +0200Taneb0(~Taneb@runciman.hacksoc.org)
2024-05-18 05:45:22 +0200alanz_(sid110616@id-110616.uxbridge.irccloud.com)
2024-05-18 05:45:28 +0200chaitlatte0_(ea29c0bb16@2a03:6000:1812:100::1124)
2024-05-18 05:45:43 +0200arcadewise_(52968ed80d@2a03:6000:1812:100::3df)
2024-05-18 05:45:56 +0200eso_(a0662dfd5e@2a03:6000:1812:100::1266)
2024-05-18 05:45:57 +0200hiredman_(~hiredman@frontier1.downey.family)
2024-05-18 05:46:18 +0200fn_lumi_(3d621153a5@2a03:6000:1812:100::df7)
2024-05-18 05:46:30 +0200bsima1_(9d7e39c8ad@2a03:6000:1812:100::dd)
2024-05-18 05:46:41 +0200ncf_(~n@monade.li)
2024-05-18 05:46:43 +0200ursa-major_(114efe6c39@2a03:6000:1812:100::11f3)
2024-05-18 05:46:48 +0200aniketd_(32aa4844cd@2a03:6000:1812:100::dcb)
2024-05-18 05:46:52 +0200poscat0x04(~poscat@user/poscat)
2024-05-18 05:47:10 +0200whereiseveryone_(206ba86c98@2a03:6000:1812:100::2e4)
2024-05-18 05:47:16 +0200pikajude-(~jude@2001:19f0:ac01:373:5400:2ff:fe86:3274)
2024-05-18 05:47:16 +0200darrik(~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se)
2024-05-18 05:47:17 +0200beaky_(~beaky@2a03:b0c0:0:1010::1e:a001)
2024-05-18 05:47:19 +0200brettgilio_(a35ba67324@2a03:6000:1812:100::260)
2024-05-18 05:47:24 +0200jjhoo_(jahakala@user/jjhoo)
2024-05-18 05:47:28 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf) (Ping timeout: 268 seconds)
2024-05-18 05:47:28 +0200probie_(cc0b34050a@user/probie)
2024-05-18 05:47:37 +0200rselim_(ce261f06ff@user/milesrout)
2024-05-18 05:47:42 +0200shachaf_(~shachaf@li227-219.members.linode.com)
2024-05-18 05:48:21 +0200henrytill_(e0180937c3@2a03:6000:1812:100::e8c)
2024-05-18 05:48:31 +0200markasoftware_(~quassel@107.161.26.124)
2024-05-18 05:48:45 +0200caubert_(~caubert@user/caubert)
2024-05-18 05:49:00 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf)
2024-05-18 05:49:05 +0200Boarders_____(sid425905@id-425905.lymington.irccloud.com)
2024-05-18 05:49:22 +0200nefercheprure(tma@twin.jikos.cz)
2024-05-18 05:49:39 +0200h2t(~h2t@user/h2t)
2024-05-18 05:49:41 +0200Hobbyboy|BNC(Hobbyboy@hobbyboy.co.uk)
2024-05-18 05:49:58 +0200mustafa_(sid502723@rockylinux/releng/mustafa)
2024-05-18 05:50:07 +0200xigua_(~xigua@user/xigua)
2024-05-18 05:50:15 +0200davean1(~davean@davean.sciesnet.net)
2024-05-18 05:50:27 +0200hueso_(~root@user/hueso)
2024-05-18 05:50:35 +0200meinside(uid24933@id-24933.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2024-05-18 05:50:35 +0200constxd(~constxd@user/constxd) (Ping timeout: 260 seconds)
2024-05-18 05:51:14 +0200mht-(~mht@2a03:b0c0:3:e0::1e2:c001)
2024-05-18 05:51:17 +0200WzC(~Frank@77-162-168-71.fixed.kpn.net)
2024-05-18 05:51:27 +0200quintasan_(~quassel@quintasan.pl)
2024-05-18 05:51:35 +0200Buggys-(Buggys@shelltalk.net)
2024-05-18 05:51:37 +0200aforemny(~aforemny@2001:9e8:6cdc:cf00:2044:2ce0:424e:adbd)
2024-05-18 05:51:46 +0200aforemny_(~aforemny@2001:9e8:6cfa:400:979c:514d:c315:798d) (Ping timeout: 246 seconds)