Logs on 2023-12-06 (liberachat/#haskell)
| 00:02:05 | <Rembane> | darchitect: No worries! Also, we're here if you have any questions. |
| 00:25:48 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 00:26:32 | → | Square2 joins (~Square4@user/square) |
| 00:29:12 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 00:30:07 | × | Square quits (~Square@user/square) (Ping timeout: 276 seconds) |
| 00:43:19 | × | tomith quits (tomith@user/tomith) (Quit: tomith) |
| 00:43:50 | × | xff0x quits (~xff0x@2405:6580:b080:900:7175:c6a6:e4c5:7fc9) (Ping timeout: 256 seconds) |
| 00:45:19 | → | xff0x joins (~xff0x@2405:6580:b080:900:f141:53b1:8840:95f3) |
| 00:48:29 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 00:48:41 | × | xff0x quits (~xff0x@2405:6580:b080:900:f141:53b1:8840:95f3) (Client Quit) |
| 00:50:07 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 00:51:24 | → | xff0x joins (~xff0x@2405:6580:b080:900:3547:f7c0:e559:ee75) |
| 00:52:50 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Remote host closed the connection) |
| 00:55:15 | × | jespada_ quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 260 seconds) |
| 00:55:15 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 00:55:23 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 00:58:07 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 01:09:23 | × | Pixi` quits (~Pixi@user/pixi) (Ping timeout: 268 seconds) |
| 01:20:27 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 01:22:28 | × | myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Quit: myxos) |
| 01:36:29 | <jackdk> | Which "rank 2 functor/traversable/etc" package is most recommended these days? barbies/conkin/hkd/rank2classes/something else I've missed? |
| 01:36:40 | → | Pixi joins (~Pixi@user/pixi) |
| 01:49:12 | → | myxos joins (~myxos@065-028-251-121.inf.spectrum.com) |
| 01:52:56 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 01:56:08 | → | Xyloes joins (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) |
| 01:57:43 | × | thegeekinside quits (~thegeekin@189.141.65.247) (Remote host closed the connection) |
| 02:04:20 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (Ping timeout: 256 seconds) |
| 02:06:02 | → | pointlessslippe1 joins (~pointless@212.82.82.3) |
| 02:14:07 | × | talismanick quits (~user@2601:204:ef00:bb0::f34e) (Ping timeout: 260 seconds) |
| 02:23:19 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 02:26:15 | → | thegeekinside joins (~thegeekin@189.141.65.247) |
| 02:26:22 | × | Square2 quits (~Square4@user/square) (Ping timeout: 260 seconds) |
| 02:27:20 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Remote host closed the connection) |
| 02:28:11 | → | Katarushisu19 joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 02:28:19 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 268 seconds) |
| 02:28:58 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 255 seconds) |
| 02:29:48 | → | dcoutts_ joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 02:29:59 | × | Katarushisu1 quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Ping timeout: 264 seconds) |
| 02:29:59 | Katarushisu19 | is now known as Katarushisu1 |
| 02:33:03 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 02:40:02 | × | xff0x quits (~xff0x@2405:6580:b080:900:3547:f7c0:e559:ee75) (Ping timeout: 256 seconds) |
| 02:40:25 | × | ec quits (~ec@gateway/tor-sasl/ec) (Read error: Connection reset by peer) |
| 02:40:25 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 02:40:48 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 02:41:31 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:46:42 | × | benjaminl quits (~benjaminl@user/benjaminl) (Remote host closed the connection) |
| 02:47:43 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 02:51:48 | → | docelif^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 03:01:03 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:16:11 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 03:18:41 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 245 seconds) |
| 03:20:47 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 03:23:48 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 03:31:07 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:97d:c646:7189:b78d) (Remote host closed the connection) |
| 03:31:22 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 03:39:10 | × | foul_owl quits (~kerry@157.97.134.165) (Ping timeout: 255 seconds) |
| 03:47:23 | × | td_ quits (~td@i5387092A.versanet.de) (Ping timeout: 264 seconds) |
| 03:49:04 | → | td_ joins (~td@i53870917.versanet.de) |
| 03:50:46 | × | Katarushisu1 quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 03:51:06 | → | Katarushisu1 joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 03:53:39 | → | foul_owl joins (~kerry@157.97.134.165) |
| 03:54:05 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:54:05 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:54:05 | finn_elija | is now known as FinnElija |
| 04:08:35 | → | Buliarous joins (~gypsydang@46.232.210.139) |
| 04:10:30 | → | ania123 joins (~ania123@94-43-231-47.dsl.utg.ge) |
| 04:18:35 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 04:40:08 | × | YuutaW quits (~YuutaW@mail.yuuta.moe) (Ping timeout: 256 seconds) |
| 04:44:58 | → | aforemny_ joins (~aforemny@2001:9e8:6cde:cb00:5605:e8df:30a7:a7a3) |
| 04:46:22 | × | aforemny quits (~aforemny@2001:9e8:6cfa:3700:318d:661c:fcd5:6731) (Ping timeout: 260 seconds) |
| 04:47:04 | × | gentauro quits (~gentauro@user/gentauro) (Ping timeout: 268 seconds) |
| 05:04:54 | × | ania123 quits (~ania123@94-43-231-47.dsl.utg.ge) (Quit: Client closed) |
| 05:10:31 | × | thegeekinside quits (~thegeekin@189.141.65.247) (Ping timeout: 255 seconds) |
| 05:17:25 | → | kmein joins (~weechat@user/kmein) |
| 05:19:08 | × | abrar_ quits (~abrar@pool-108-52-90-30.phlapa.fios.verizon.net) (Ping timeout: 268 seconds) |
| 05:20:49 | → | abrar_ joins (~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) |
| 05:29:19 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 05:29:59 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 05:31:46 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 05:31:55 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 05:45:36 | → | igemnace joins (~ian@user/igemnace) |
| 05:57:43 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 05:58:02 | → | newsham joins (~newsham@2603-800c-2c01-6825-e926-a2cb-be50-5432.res6.spectrum.com) |
| 05:58:26 | → | euleritian joins (~euleritia@dynamic-002-247-248-016.2.247.pool.telefonica.de) |
| 05:59:19 | <newsham> | if (in CT) a monoid has one object, and the morphisms are (for instance) integers and composition is (for instance) multiplication, and identity is (eg) "1". What is the object itself? |
| 06:00:08 | <EvanR> | the set of integers is the one object |
| 06:00:55 | <EvanR> | er |
| 06:01:00 | <int-e> | newsham: If you describe it like that, the object can be totally abstract. Or you can do the arrow-only CT thing where the object is the identity morphism |
| 06:01:05 | <newsham> | why is a morphism "3" an arrow from the set of integers to itself? |
| 06:01:31 | <int-e> | newsham: it becomes a function if you interpret it as (*3) |
| 06:01:32 | <EvanR> | I'm wrong, each arrow is an integer, and the object is whatever, "*" |
| 06:01:35 | <EvanR> | unit |
| 06:01:57 | <newsham> | ok.. i guess thats easier to grok. morphism is (*3), and composition is just normal func composition |
| 06:02:03 | <newsham> | and object is set of ints. |
| 06:02:05 | <EvanR> | morphisms don't need to be functions |
| 06:02:18 | <newsham> | right, thats why i was trying to not assume the morphism was a func |
| 06:02:30 | <newsham> | but having a hard time grokking what the object was then |
| 06:02:44 | <EvanR> | the more important part there is that there is only one object |
| 06:02:46 | <int-e> | newsham: it could literally be anything |
| 06:02:55 | <EvanR> | it doesn't do anything else |
| 06:03:05 | <int-e> | the only role of the object is to serve as source and target of your morphisms |
| 06:03:25 | <newsham> | i still have a hard time wrapping my head around the construction though.. what justification do i have to say that "3" is a morphism from "abstract thing" to itself? |
| 06:03:49 | <int-e> | you just define the source and target of 3 to be that object |
| 06:04:01 | <EvanR> | you didn't construct it, you just looked at that monoid through ct beer goggles |
| 06:04:37 | <newsham> | when looking at monoid through the goggles, my eyes only see "set of integers" as an object. |
| 06:04:50 | <int-e> | There's really no further required meaning to it. You can compose f and g if the target of g is the source of f. |
| 06:05:02 | <newsham> | but i think the treating numbers as functions and the ojbect as ints and composition as func composition works well enough for me. its a valid construction |
| 06:05:16 | <int-e> | You take the definition of a category and check all the properties. |
| 06:05:22 | <EvanR> | you could make an inspirational diagram of that category: it would have 1 object and an infinite number of arrows coming out of it and going back in, one for each integer |
| 06:05:33 | <EvanR> | the definition of morphism composition is multiplication of corresponding integers |
| 06:05:38 | <newsham> | it seems really arbitrary to me that I would out of thin air delcare that "3" goes from "a" to "a" without saying what "a" is. like.. cant i just do that in other contexts where it would lead to nonsense? |
| 06:05:39 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 06:06:02 | <EvanR> | like when you draw a diagram in geometry, you put a point called A, it's just a point, it's nothing more |
| 06:06:17 | <EvanR> | it serves to end line segments or draw lines through |
| 06:06:21 | <EvanR> | or center a circle |
| 06:06:28 | <int-e> | newsham: welcome to abstract nonsense I suppose |
| 06:06:58 | <EvanR> | we make up meaningless things all the time in haskell |
| 06:07:07 | <EvanR> | data () = (), what is ()? doesn't matter |
| 06:07:11 | <newsham> | well i guess my concrete question here, which i dont have enough depth to know the answer to, is literally "could I do the same construction in another context where it doesnt make sense and result in nonsense" |
| 06:07:12 | <int-e> | > fix id |
| 06:07:14 | <lambdabot> | *Exception: <<loop>> |
| 06:07:21 | <newsham> | I have no problem with unit :) |
| 06:07:33 | <EvanR> | why is unit not objectionable on the same grounds |
| 06:07:34 | <newsham> | I have no problem with bottom (if its in your code, not mine) |
| 06:07:59 | <int-e> | newsham: you can define a structure that has all the operations of a category but violates its laws. |
| 06:08:01 | → | todi1 joins (~todi@pd9571076.dip0.t-ipconnect.de) |
| 06:08:05 | <newsham> | i'm not against having abstract things.. like I said, it boils down to that one question above. |
| 06:08:06 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 06:08:09 | × | todi quits (~todi@pd9571327.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 06:08:25 | <int-e> | like if you have one object *, integers as morphisms, but you use subtraction for composition |
| 06:08:27 | <newsham> | perhaps i just need to go deeper and revisit my question later. |
| 06:08:31 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 06:08:31 | <EvanR> | you could also look at the category structure (or monoid structure for that matter) as an interface |
| 06:08:38 | <int-e> | which... isn't a monoid. |
| 06:08:52 | → | zetef joins (~quassel@95.77.17.251) |
| 06:09:09 | <int-e> | and it turns out that with a single object, categories correspond exactly to usual monoids from abstract algebra. |
| 06:09:29 | <newsham> | yes thats what i'm exploring. |
| 06:09:54 | <newsham> | i mostly get it except this question. ok.. well, back into the breach. thanks for the conversation |
| 06:10:06 | <int-e> | You just have that extra "object" thing around. Which goes away if you identify objects and their identity morphisms, as already mentioned. |
| 06:10:31 | <EvanR> | conflating different things as being the same should make it more confusing usually xD |
| 06:10:59 | <int-e> | newsham: this is similar to what EvanR said... what's the meaning of "x"? :-) |
| 06:11:05 | <EvanR> | which is why "correspond" is probably easier than "is really" when talking about monoids being categories |
| 06:12:00 | <int-e> | once you've internalized the correspondence the difference vanishes ;-) |
| 06:12:24 | <EvanR> | unless you use homotopy type theory |
| 06:13:02 | <EvanR> | which puts my suggestion of draw diagrams into overdrive |
| 06:13:04 | <int-e> | I ... don't. |
| 06:13:26 | <int-e> | I barely use category theory ;) |
| 06:15:29 | <EvanR> | different points in the space "are equal" if you have a path between them, and if there is only 1 connected component to the space, everything is equal. But there could be non trivial spatial structure, so equivalences aren't equal. In which case you couldn't collapse the entire space into a single point unfortunately for the reductionist! |
| 06:15:31 | → | acidjnk_new joins (~acidjnk@p200300d6e72b933411fabc01fd6787da.dip0.t-ipconnect.de) |
| 06:16:33 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:20:39 | × | benjaminl quits (~benjaminl@user/benjaminl) (Remote host closed the connection) |
| 06:21:58 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 06:22:44 | × | snek quits (sid280155@id-280155.lymington.irccloud.com) (Ping timeout: 256 seconds) |
| 06:23:01 | → | snek joins (sid280155@id-280155.lymington.irccloud.com) |
| 06:28:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:35:35 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 06:36:18 | → | chomwitt joins (~chomwitt@2a02:587:7a09:c300:1ac0:4dff:fedb:a3f1) |
| 06:40:44 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:47:17 | → | trev joins (~trev@user/trev) |
| 06:53:17 | → | igemnace joins (~ian@user/igemnace) |
| 06:55:32 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:02:59 | × | analoq quits (~yashi@user/dies) (Ping timeout: 264 seconds) |
| 07:04:18 | → | analoq joins (~yashi@user/dies) |
| 07:05:49 | → | ubert1 joins (~Thunderbi@178.165.165.175.wireless.dyn.drei.com) |
| 07:05:58 | × | ubert quits (~Thunderbi@91.141.79.49.wireless.dyn.drei.com) (Ping timeout: 276 seconds) |
| 07:05:58 | ubert1 | is now known as ubert |
| 07:07:40 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 268 seconds) |
| 07:11:52 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:12:05 | × | ft quits (~ft@p4fc2a395.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 07:14:13 | → | ft joins (~ft@p3e9bc784.dip0.t-ipconnect.de) |
| 07:15:02 | → | kenran joins (~user@user/kenran) |
| 07:19:08 | × | newsham quits (~newsham@2603-800c-2c01-6825-e926-a2cb-be50-5432.res6.spectrum.com) (Quit: Client closed) |
| 07:24:13 | → | alp_ joins (~alp@2001:861:e3d6:8f80:4f0:3b3:6172:8f1e) |
| 07:25:52 | × | docelif^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 07:27:25 | × | Igloo quits (~ian@matrix.chaos.earth.li) (Ping timeout: 260 seconds) |
| 07:30:26 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:35:22 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:37:06 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:39:16 | → | chele joins (~chele@user/chele) |
| 07:42:54 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 07:45:08 | → | Igloo joins (~ian@2001:8b0:645c::210) |
| 07:51:43 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 07:59:30 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 07:59:59 | → | Guest16 joins (~Guest16@136.169.59.60) |
| 08:00:04 | × | euleritian quits (~euleritia@dynamic-002-247-248-016.2.247.pool.telefonica.de) (Read error: Connection reset by peer) |
| 08:00:10 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 08:00:22 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 08:02:23 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 264 seconds) |
| 08:04:20 | → | rosco joins (~rosco@175.136.158.171) |
| 08:25:54 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 08:27:46 | × | benjaminl quits (~benjaminl@user/benjaminl) (Remote host closed the connection) |
| 08:28:40 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 08:32:23 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 264 seconds) |
| 08:34:16 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 08:39:12 | → | zetef joins (~quassel@95.77.17.251) |
| 08:44:56 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 08:47:43 | → | CiaoSen joins (~Jura@2a05:5800:281:b200:ca4b:d6ff:fec1:99da) |
| 08:50:05 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:51:40 | → | swamp_ joins (~zmt00@user/zmt00) |
| 08:52:14 | × | swamp_ quits (~zmt00@user/zmt00) (Max SendQ exceeded) |
| 08:53:01 | → | swamp_ joins (~zmt00@user/zmt00) |
| 08:54:31 | × | zmt01 quits (~zmt00@user/zmt00) (Ping timeout: 245 seconds) |
| 08:58:11 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:58:40 | × | tessier quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 268 seconds) |
| 09:01:30 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 09:07:06 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Remote host closed the connection) |
| 09:14:16 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 09:15:04 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 09:18:22 | → | notzmv joins (~zmv@user/notzmv) |
| 09:18:51 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:22:26 | → | aforemny joins (~aforemny@i59F516FF.versanet.de) |
| 09:22:27 | × | aforemny_ quits (~aforemny@2001:9e8:6cde:cb00:5605:e8df:30a7:a7a3) (Ping timeout: 256 seconds) |
| 09:23:23 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:26:25 | → | qqq joins (~qqq@92.43.167.61) |
| 09:26:39 | → | mmhat joins (~mmh@p200300f1c726935cee086bfffe095315.dip0.t-ipconnect.de) |
| 09:27:01 | [_] | is now known as [itchyjunk] |
| 09:27:34 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 09:28:00 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 256 seconds) |
| 09:31:13 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 246 seconds) |
| 09:32:24 | × | Xyloes quits (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) (Quit: Konversation terminated!) |
| 09:36:40 | → | Xyloes joins (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) |
| 09:38:19 | × | Xyloes quits (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) (Client Quit) |
| 09:40:01 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 09:40:01 | → | tessier joins (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 09:43:09 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 09:44:29 | → | Xyloes joins (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) |
| 09:44:31 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Ping timeout: 245 seconds) |
| 09:44:31 | → | chele joins (~chele@user/chele) |
| 09:46:16 | × | tessier quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 255 seconds) |
| 09:47:19 | × | Xyloes quits (~wyx@2400:dd01:103a:1012:5923:33ce:7857:fc04) (Client Quit) |
| 09:49:16 | → | zetef joins (~quassel@95.77.17.251) |
| 09:51:37 | <phma> | I've been working on a library in Haskell and Rust (two implementations in one repo, with a shell script that runs both and compares them). The Rust version starts at 0.1.0 and the Haskell version |
| 09:52:00 | <phma> | starts at 0.1.0.0. How should I handle correspondence between the version numbers? |
| 09:53:23 | × | gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 09:53:48 | <haskellbridge> | 06<sm> why not make them the same ? |
| 09:54:08 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:54:18 | <phma> | because they use different formats of version numbers |
| 09:54:34 | <haskellbridge> | 06<sm> why ? |
| 09:55:18 | <haskellbridge> | 06<sm> haskell doesn't require a particular number of version number components AFAIK |
| 09:56:00 | <phma> | https://stackoverflow.com/questions/37201431/why-does-haskell-versioning-policy-have-two-places-for-major-version-not-one-li |
| 09:56:14 | <c_wraith> | haskell doesn't but there is a convention |
| 09:56:33 | <[exa]> | oh whoops I always thought that it's 3 semver numbers + 1 for maintainer uploads |
| 09:56:35 | <c_wraith> | but there's no reason you can't make the haskell version the rust version with a "0." in front of it |
| 09:56:50 | <haskellbridge> | 06<sm> 0.1 is a perfectly fine haskell package version |
| 09:56:54 | <phma> | https://pvp.haskell.org/ |
| 09:56:57 | → | __monty__ joins (~toonn@user/toonn) |
| 09:57:08 | <c_wraith> | sm: you're sort of missing the point, which is to not be like stack |
| 09:57:40 | haskellbridge | 06<sm> gets back to work |
| 09:58:05 | <c_wraith> | phma: why do they start at those? |
| 09:58:12 | × | chomwitt quits (~chomwitt@2a02:587:7a09:c300:1ac0:4dff:fedb:a3f1) (Remote host closed the connection) |
| 09:58:42 | <c_wraith> | phma: why not start at, for instance, 0.1.0 and 0.0.1.0? |
| 09:58:57 | <phma> | c_wraith: I don't know, that's the starting version number when creating a project |
| 09:59:34 | <phma> | I could do that, I suppose, since I haven't tagged anything yet |
| 09:59:53 | <phma> | or used the library in anything else |
| 10:00:50 | <phma> | also, is there a tool that, given two versions of a library, tells what needs to be bumped in the version number? |
| 10:01:12 | <c_wraith> | I think someone has made something like that, but I can't remember any details at all |
| 10:01:24 | <phma> | afk — kitchen time |
| 10:01:33 | × | rosco quits (~rosco@175.136.158.171) (Quit: Lost terminal) |
| 10:01:39 | → | danse-nr3 joins (~danse@rm-19-20-84.service.infuturo.it) |
| 10:03:19 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 10:04:02 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 10:15:35 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 264 seconds) |
| 10:16:36 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds) |
| 10:16:39 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 10:17:26 | → | tessier joins (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 10:17:51 | × | danse-nr3 quits (~danse@rm-19-20-84.service.infuturo.it) (Ping timeout: 256 seconds) |
| 10:19:40 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:21:07 | → | danse-nr3 joins (~danse@rm-19-20-84.service.infuturo.it) |
| 10:22:06 | × | myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection) |
| 10:22:45 | <trev> | how do I understand this line: `map f >>> foldr (>>>) id`? |
| 10:23:39 | × | cods quits (~fred@tuxee.net) (Ping timeout: 256 seconds) |
| 10:23:43 | <trev> | where the inputs are `List -> Int` |
| 10:23:54 | <danse-nr3> | huh i think the parenthesis are useless there |
| 10:24:06 | <danse-nr3> | % :t (>>>) |
| 10:24:06 | <yahb2> | <interactive>:1:1: error: ; • Variable not in scope: >>> ; • Perhaps you meant one of these: ; ‘>>’ (imported from Prelude), ‘>>=’ (imported from Prelude), ; ‘>=>’ (imported... |
| 10:24:08 | × | Guest16 quits (~Guest16@136.169.59.60) (Ping timeout: 250 seconds) |
| 10:24:16 | <danse-nr3> | @hoogle >>> |
| 10:24:16 | <lambdabot> | Control.Arrow (>>>) :: Category cat => cat a b -> cat b c -> cat a c |
| 10:24:16 | <lambdabot> | Control.Category (>>>) :: Category cat => cat a b -> cat b c -> cat a c |
| 10:24:16 | <lambdabot> | GHC.Desugar (>>>) :: forall arr . Arrow arr => forall a b c . arr a b -> arr b c -> arr a c |
| 10:24:32 | <[exa]> | >>> is the arrow composition, IMO it's valid with the parentheses there |
| 10:24:58 | <danse-nr3> | cool then |
| 10:25:15 | <trev> | can you re-write that without >>>? |
| 10:25:31 | <trev> | cause i don't really understand how the functions are composed |
| 10:25:46 | <danse-nr3> | > 1 (+) 1 |
| 10:25:47 | <lambdabot> | error: |
| 10:25:47 | <lambdabot> | • Could not deduce (Num a0) |
| 10:25:47 | <lambdabot> | from the context: (Num a, Num t, Num ((a -> a -> a) -> t -> t1)) |
| 10:26:19 | <danse-nr3> | i see |
| 10:26:49 | <danse-nr3> | > import Control.Arrow |
| 10:26:51 | <lambdabot> | <hint>:1:1: error: parse error on input ‘import’ |
| 10:26:56 | <[Leary]> | % :t \f -> map f >>> foldr (>>>) id |
| 10:26:56 | <yahb2> | \f -> map f >>> foldr (>>>) id :: (a -> b -> b) -> [a] -> b -> b |
| 10:27:03 | <[Leary]> | % :t \f -> foldr (flip (.)) id . map f |
| 10:27:03 | <yahb2> | \f -> foldr (flip (.)) id . map f :: (a -> c -> c) -> [a] -> c -> c |
| 10:27:18 | <[exa]> | +1 [Leary] ^^ |
| 10:27:33 | <danse-nr3> | maybe go step by step trev |
| 10:27:40 | <[exa]> | not that it would remove the function composition but it's hard to remove function composition from code that only does function composition right... |
| 10:27:42 | <danse-nr3> | % :t foldr (>>>) id |
| 10:27:42 | <yahb2> | foldr (>>>) id :: Foldable t => t (b -> b) -> b -> b |
| 10:28:52 | <danse-nr3> | % foldr (>>>) id [+1, +2] 0 |
| 10:28:52 | <yahb2> | <interactive>:81:17: error: ; A section must be enclosed in parentheses thus: (+ 1) ; ; <interactive>:81:21: error: ; A section must be enclosed in parentheses thus: (+ 2) |
| 10:29:06 | <danse-nr3> | % foldr (>>>) id [(+1), (+2)] 0 |
| 10:29:06 | <yahb2> | 3 |
| 10:31:33 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:32:32 | <trev> | so the foldr is being applied before the `map f` in my example? |
| 10:34:58 | <danse-nr3> | hmm i am not very familiar with arrows but i think we can test with functions to know the answer |
| 10:34:58 | → | cods joins (~fred@tuxee.net) |
| 10:35:24 | <[exa]> | trev: it should roughly correspond to: `foldr (>>>) id (map f ( ....something ...))` |
| 10:35:37 | <[exa]> | :t (>>>) |
| 10:35:37 | <lambdabot> | forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k). Category cat => cat a b -> cat b c -> cat a c |
| 10:36:01 | <[exa]> | (>>>) pipes from left to right, unlike (.) |
| 10:36:26 | <danse-nr3> | :t (<> "1") >>> (<> "2") |
| 10:36:27 | <lambdabot> | [Char] -> [Char] |
| 10:36:40 | <danse-nr3> | ((<> "1") >>> (<> "2")) "" |
| 10:36:48 | <danse-nr3> | % ((<> "1") >>> (<> "2")) "" |
| 10:36:48 | <yahb2> | "12" |
| 10:36:58 | <trev> | so there is no way to explain it by being extra verbose? like using intermediate values or something? |
| 10:37:27 | <trev> | or just in terms of simple things like `map` and `foldr` |
| 10:37:57 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds) |
| 10:39:47 | <danse-nr3> | there are no intermediate values i think. The functions or the two sides of the main >>> are composed as shown above, the other >>> is used to build a function with foldr |
| 10:40:37 | <danse-nr3> | if we consider that >>> is working as the opposite of . , maybe that answers your question about intermediate values |
| 10:41:11 | <danse-nr3> | i guess you can make it clear bu having specific variables with type annotation for each function and then a line with `f >>> g` |
| 10:41:21 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 10:41:22 | <danse-nr3> | *clearer and *by |
| 10:43:18 | × | danse-nr3 quits (~danse@rm-19-20-84.service.infuturo.it) (Read error: Connection reset by peer) |
| 10:43:22 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 10:44:22 | → | danse-nr3 joins (~danse@rm-19-55-63.service.infuturo.it) |
| 10:46:12 | <phma> | c_wraith: I changed it to 0.0.1.0, seems to be no problem |
| 10:48:30 | × | John_Ivan quits (~John_Ivan@user/john-ivan/x-1515935) (Ping timeout: 260 seconds) |
| 10:48:41 | → | Square2 joins (~Square4@user/square) |
| 10:54:03 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:58:47 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 264 seconds) |
| 10:59:00 | × | kronicma1 quits (user39425@neotame.csclub.uwaterloo.ca) (Quit: WeeChat 3.8) |
| 11:08:02 | → | tremon joins (~tremon@83.80.159.219) |
| 11:08:27 | → | coot_ joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 11:08:59 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Ping timeout: 264 seconds) |
| 11:09:23 | coot_ | is now known as coot |
| 11:16:05 | → | xff0x joins (~xff0x@2405:6580:b080:900:8e8f:f259:634:292d) |
| 11:32:40 | × | CiaoSen quits (~Jura@2a05:5800:281:b200:ca4b:d6ff:fec1:99da) (Ping timeout: 246 seconds) |
| 11:35:15 | → | rvalue joins (~rvalue@user/rvalue) |
| 11:35:38 | → | rito joins (~ritog@45.112.243.47) |
| 11:39:05 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 11:42:06 | todi1 | is now known as todi |
| 11:43:05 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 11:50:43 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 268 seconds) |
| 11:50:52 | × | duncan quits (~duncan@nat-server.ehlab.uk) (Quit: WeeChat 3.0) |
| 11:56:29 | → | Guest|79 joins (~Guest|79@78-73-145-35-no2661.tbcn.telia.com) |
| 11:56:43 | <Guest|79> | damn irc, that was many years ago |
| 12:01:41 | → | CiaoSen joins (~Jura@2a05:5800:281:b200:ca4b:d6ff:fec1:99da) |
| 12:03:33 | <jackdk> | still here, still going strong |
| 12:04:30 | <danse-nr3> | "strong" |
| 12:12:07 | × | lg188 quits (~lg188@82.18.98.230) (Ping timeout: 276 seconds) |
| 12:19:13 | → | duncan joins (~duncan@user/duncan) |
| 12:19:16 | × | xff0x quits (~xff0x@2405:6580:b080:900:8e8f:f259:634:292d) (Ping timeout: 276 seconds) |
| 12:20:31 | → | xff0x joins (~xff0x@ai096045.d.east.v6connect.net) |
| 12:20:38 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 12:22:35 | <Guest|79> | haha well theres 625 people online which is kind of insane to me |
| 12:23:03 | <trev> | "online" |
| 12:23:05 | <Guest|79> | at first before it loaded it said 0 people online which didn't chock me |
| 12:23:30 | <Guest|79> | at least 4 |
| 12:32:04 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:32:31 | × | alp_ quits (~alp@2001:861:e3d6:8f80:4f0:3b3:6172:8f1e) (Ping timeout: 246 seconds) |
| 12:35:24 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:35:47 | → | flounders joins (~flounders@24.246.176.178) |
| 12:43:12 | × | Guest|79 quits (~Guest|79@78-73-145-35-no2661.tbcn.telia.com) (Quit: Connection closed) |
| 12:43:40 | × | danse-nr3 quits (~danse@rm-19-55-63.service.infuturo.it) (Ping timeout: 255 seconds) |
| 12:44:17 | × | hgolden_ quits (~hgolden@cpe-172-251-233-141.socal.res.rr.com) (Remote host closed the connection) |
| 12:46:07 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
| 12:54:01 | → | cadro joins (~cadro@2a10:3781:647:1:5a5d:353f:fca3:987d) |
| 12:54:09 | × | cadro quits (~cadro@2a10:3781:647:1:5a5d:353f:fca3:987d) (Client Quit) |
| 12:57:33 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 12:59:19 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 12:59:55 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:10:59 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 13:16:04 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:18:04 | → | edr joins (~edr@user/edr) |
| 13:21:33 | → | danse-nr3 joins (~danse@rm-19-55-63.service.infuturo.it) |
| 13:36:32 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:41:07 | × | mikess quits (~sam@user/mikess) (Ping timeout: 246 seconds) |
| 13:43:58 | → | alp_ joins (~alp@2001:861:e3d6:8f80:9cca:35b8:68c7:62cd) |
| 13:43:58 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 13:44:08 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 13:45:23 | → | myxos joins (~myxos@065-028-251-121.inf.spectrum.com) |
| 13:48:49 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 13:49:12 | × | dcoutts_ quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Read error: Connection reset by peer) |
| 13:49:28 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 13:49:40 | → | euleritian joins (~euleritia@dynamic-002-247-248-090.2.247.pool.telefonica.de) |
| 13:51:49 | × | duncan quits (~duncan@user/duncan) (Quit: ZNC 1.8.2 - https://znc.in) |
| 13:54:16 | → | duncan joins (~duncan@user/duncan) |
| 13:55:17 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:02:41 | × | loonycyborg quits (~loonycybo@wesnoth/developer/loonycyborg) (Ping timeout: 268 seconds) |
| 14:17:10 | × | xigua quits (~xigua@user/xigua) (Remote host closed the connection) |
| 14:17:44 | → | xigua joins (~xigua@user/xigua) |
| 14:18:35 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 14:18:54 | → | ddellacosta joins (~ddellacos@ool-44c73d16.dyn.optonline.net) |
| 14:23:43 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 14:26:29 | → | thegeekinside joins (~thegeekin@189.141.65.247) |
| 14:28:56 | × | CiaoSen quits (~Jura@2a05:5800:281:b200:ca4b:d6ff:fec1:99da) (Ping timeout: 256 seconds) |
| 14:31:07 | × | ddellacosta quits (~ddellacos@ool-44c73d16.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 14:33:23 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 14:34:11 | × | misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 264 seconds) |
| 14:34:26 | × | myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Quit: myxos) |
| 14:34:53 | → | myxos joins (~myxos@065-028-251-121.inf.spectrum.com) |
| 14:41:32 | <dminuoso_> | Is there a deeper reason why GHC cannot automatically polymorphize let bindings? I just had a compiler error when something along the lines of `f = showT 'a' <> showT 1 where showT = T.pack . show` failed, and just staring at it it seems so obvious that if a monomorphized binding ends up with multiple types, it could just undo monomorphization. |
| 14:43:17 | <dminuoso_> | or well, when I say "automatically polymorphize" I really mean repolymorphize monomorphized bindings (when necessary) |
| 14:43:19 | × | danse-nr3 quits (~danse@rm-19-55-63.service.infuturo.it) (Read error: Connection reset by peer) |
| 14:43:41 | → | danse-nr3 joins (~danse@151.47.16.49) |
| 14:49:37 | → | sabino joins (~sabino@user/sabino) |
| 14:49:52 | → | igemnace joins (~ian@user/igemnace) |
| 14:50:20 | <kuribas> | dminuoso_: because it's not decidable? |
| 14:50:41 | <dminuoso_> | How is it not decidable? |
| 14:51:41 | <dminuoso_> | If you get any unification error on that binding, allow to polymorphize and try again. |
| 14:52:38 | <dminuoso_> | Include a warning that the binding is polymorphized and a quantified type signature should be included, as to nudge the programmer into avoiding that unnecessary round 1. |
| 14:56:30 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 14:56:51 | <ncf> | yes let's add more rules and exceptions, the monomorphism restriction isn't surprising enough as it is ;) |
| 14:57:12 | <dminuoso_> | This would, at best, make it less surprising. |
| 14:57:48 | <dminuoso_> | Type unification errors when MMR kicks in are strange and non-obvious. A dedicated warning can directly tell you what's happening. |
| 14:58:47 | × | raym quits (~ray@user/raym) (Ping timeout: 264 seconds) |
| 15:00:21 | <danse-nr3> | once a feature gets in, its impact slowly propagates to the code around it. It is unavoidable i guess, to make it work better with the rest |
| 15:00:41 | → | loonycyborg joins (loonycybor@wesnoth/developer/loonycyborg) |
| 15:01:37 | <dminuoso_> | `Cannot match Char with Int` vs "Ignoring monomorphism restriction on x (foo.hs:103) would allow compilation to succeed. The inferred type of x is: ..." |
| 15:01:44 | <dminuoso_> | Ultimately this could still be an error. |
| 15:04:04 | <dminuoso_> | But perhaps that would require a bit more sophisticated type error slicing to know which binding to even try to repolymorphize, and perhaps this would dramatically increase type checking time *when* errors occurs since there might be any number of bindings GHC could try to repolymorphize... |
| 15:04:07 | <dminuoso_> | Mmm |
| 15:04:54 | → | raym joins (~ray@user/raym) |
| 15:06:43 | × | darchitect quits (~darchitec@2a00:23c6:3584:df01:49b7:b837:bf00:38a1) (Quit: WeeChat 4.1.1) |
| 15:10:33 | ← | ricardo1 parts (~ricardo@84.16.179.218) () |
| 15:11:27 | × | Hooloovoo quits (~Hooloovoo@hax0rbana.org) (Ping timeout: 268 seconds) |
| 15:12:42 | → | zetef joins (~quassel@95.77.17.251) |
| 15:12:58 | → | Hooloovoo joins (~Hooloovoo@hax0rbana.org) |
| 15:21:09 | × | sefidel quits (~sefidel@user/sefidel) (Remote host closed the connection) |
| 15:21:43 | → | sefidel joins (~sefidel@user/sefidel) |
| 15:24:15 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:24:24 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.0.5) |
| 15:24:36 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 15:32:02 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Remote host closed the connection) |
| 15:32:17 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 15:32:30 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:40:17 | × | rito quits (~ritog@45.112.243.47) (Ping timeout: 256 seconds) |
| 15:40:32 | <glguy> | dminuoso_: the monomorphism restriction is a feature, not a limitation. It means things that look like simple values can perform like them. Complex rules for re polymorphism would make it much harder to be confident that you didn't accidentally create a performance mistake and would end up creating extra work where we would need to put even more type signatures on let bindings to avoid this new |
| 15:40:33 | <glguy> | pitfall |
| 15:40:45 | <kuribas> | dminuoso_: If I recall correctly, having polymorphic let with various extensions (GADTs, etc) is undecidable, or just very hard to implement. |
| 15:41:49 | <glguy> | You can already with with the restriction disabled via an extension pragma |
| 15:42:40 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 15:42:54 | × | Square2 quits (~Square4@user/square) (Ping timeout: 268 seconds) |
| 15:46:05 | → | John_Ivan joins (~John_Ivan@user/john-ivan/x-1515935) |
| 15:47:27 | × | John_Ivan quits (~John_Ivan@user/john-ivan/x-1515935) (Remote host closed the connection) |
| 15:52:53 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:53:09 | → | zincy joins (~tom@2a00:23c8:9705:9501:4425:940f:c2d:62c4) |
| 15:54:58 | <exarkun> | Did Network.Socket.close use to be named Network.Socket.sClose? |
| 15:56:54 | → | Square joins (~Square@user/square) |
| 15:58:47 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 264 seconds) |
| 16:02:14 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Remote host closed the connection) |
| 16:02:46 | → | John_Ivan joins (~John_Ivan@user/john-ivan/x-1515935) |
| 16:03:05 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 16:03:12 | <bwe> | dminuoso_: rolling my MaybeeState to grasp monad transformers: https://gist.github.com/benjaminweb/ea91583983f5eceb10549ed25db03ec4/revisions |
| 16:03:22 | × | mmhat quits (~mmh@p200300f1c726935cee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.1.2) |
| 16:04:19 | <bwe> | dminuoso_: I am stuck at line 350: Found hole: _ :: Maybe a -> MaybeeState s1 a1 |
| 16:04:56 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:05:24 | × | euleritian quits (~euleritia@dynamic-002-247-248-090.2.247.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:05:43 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:10:12 | <bwe> | f :: (a -> MaybeeState s b) -- so the only thing is how to get around the Maybe; fmap or case don't work |
| 16:12:23 | × | gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 16:13:07 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 16:16:03 | <ncf> | bwe: you should probably case split on maybee_a and wonder what should happen in each branch |
| 16:17:15 | ski | glances around |
| 16:19:50 | <bwe> | ncf: got it; I've compared Monad instances for Maybee and State to realise what I need to do. |
| 16:20:16 | <bwe> | https://gist.github.com/benjaminweb/ea91583983f5eceb10549ed25db03ec4#file-monadt-hs-L345-L352 |
| 16:21:29 | → | ricardo1 joins (~ricardo@84.16.179.218) |
| 16:22:19 | <ncf> | yup :) now check the monad laws |
| 16:23:33 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 16:23:36 | ski | was just about to say that |
| 16:24:19 | bwe | is afk, will do later. |
| 16:26:05 | × | danse-nr3 quits (~danse@151.47.16.49) (Ping timeout: 240 seconds) |
| 16:28:35 | × | gehmehgeh quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 16:29:17 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 16:36:15 | × | picnoir quits (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.1.1) |
| 16:36:54 | → | danse-nr3 joins (~danse@151.47.16.49) |
| 16:37:58 | → | chomwitt joins (~chomwitt@2a02:587:7a09:c300:1ac0:4dff:fedb:a3f1) |
| 16:38:43 | → | picnoir joins (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) |
| 16:46:07 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:46:49 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:51:14 | × | infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection) |
| 16:52:04 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.1.1) |
| 16:53:21 | → | infinity0 joins (~infinity0@pwned.gg) |
| 16:55:52 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 17:01:22 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 17:02:12 | → | mikess joins (~sam@user/mikess) |
| 17:02:46 | × | chele quits (~chele@user/chele) (Quit: Leaving) |
| 17:02:51 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:11:01 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Remote host closed the connection) |
| 17:13:11 | <bwe> | how do I check them? I'd start with them: https://wiki.haskell.org/Monad_laws |
| 17:16:41 | <idgaen> | by hand, I guess |
| 17:17:02 | <Rembane> | Or using Agda if you like dependently typed programming |
| 17:17:59 | <danse-nr3> | i also saw some rule checking automation. Maybe recently added to quickcheck but not sure, maybe was elsewhere |
| 17:19:30 | <duncan> | It is not as simple as putting the forumlae into haskell code |
| 17:19:38 | <duncan> | but you can do it easier with `join` |
| 17:19:44 | <duncan> | (at least associativity) |
| 17:20:19 | <duncan> | Most of the academic courses I saw which checked them provided students with a simple module which took care of it |
| 17:20:33 | <ncf> | it might also be easier if you straight up define a MaybeT transformer instead of the special case of MaybeT State |
| 17:20:59 | <duncan> | https://blog.ploeh.dk/2022/04/11/monad-laws/ |
| 17:21:20 | <geekosaur> | there's a QuickCheck-classes package which has helpers for testing typeclass instances, and QuickCheck-classes-base which uses it to test typeclasses in base (and presumably can be used as examples to test your own) |
| 17:22:09 | <ncf> | nice haiku on that wiki page |
| 17:22:16 | <ski> | bwe : "how do I check them?" -- start from both sides, simplify, see if you get the same thing |
| 17:22:54 | ski | 's kinda disappointed that wiki page doesn't mention the form of the laws, in terms `join' |
| 17:22:57 | <duncan> | One of the issues I had when I was implementing this stuff in R (don't ask) was lack of good examples even in Haskell |
| 17:23:32 | <duncan> | the blog posts just sort of assume, you can translate the categorical machinery into code |
| 17:23:52 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:23:55 | <ski> | ncf : well, `MaybeeState s' isn't exactly `MaybeT (State s)' (for two reasons) |
| 17:24:57 | <ski> | duncan : hm, would also be interesting to see the laws expressed in terms of LINQ |
| 17:25:19 | <ncf> | ski: up to a trivial isomorphism |
| 17:25:25 | <duncan> | LINQ ~ .net/F#? |
| 17:26:00 | <duncan> | Well, Seemann does all the catamorphism examples in F#/Haskell |
| 17:27:11 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 17:28:57 | <ski> | duncan : yes |
| 17:29:30 | <ski> | ncf : oh, you're right, i'm confusing the order |
| 17:30:01 | → | rito joins (~ritog@45.112.243.47) |
| 17:31:04 | <ski> | (still, `MaybeeState s' is failing a law) |
| 17:39:25 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Remote host closed the connection) |
| 17:46:57 | <ncf> | ski: is it? |
| 17:46:57 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 17:48:04 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:51:17 | × | chomwitt quits (~chomwitt@2a02:587:7a09:c300:1ac0:4dff:fedb:a3f1) (Ping timeout: 240 seconds) |
| 17:51:54 | <ski> | yes |
| 17:52:21 | <ski> | (not one of the three main monad laws, though) |
| 17:54:09 | <ncf> | oh yeah <*> has effects backwards |
| 17:54:39 | <ski> | quite |
| 17:57:42 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:58:50 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:00:24 | × | misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 252 seconds) |
| 18:00:29 | <bwe> | ski: so it's not failing left identity, right identity, nor associativity - is that what you mean? |
| 18:02:14 | → | misterfish joins (~misterfis@84-53-85-146.bbserv.nl) |
| 18:07:07 | <ski> | bwe : well, i didn't check those in detail |
| 18:07:12 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 18:07:13 | <ski> | (have you tried to check them ?) |
| 18:07:36 | <bwe> | no, I don't know where to start with |
| 18:07:49 | <bwe> | MkMaybeeState g >>= f = MkMaybeeState $ \s0 -> |
| 18:09:56 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 18:10:30 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 18:11:05 | <ski> | hm |
| 18:11:12 | → | euleritian joins (~euleritia@dynamic-002-247-248-090.2.247.pool.telefonica.de) |
| 18:12:40 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 18:12:43 | × | alp_ quits (~alp@2001:861:e3d6:8f80:9cca:35b8:68c7:62cd) (Ping timeout: 256 seconds) |
| 18:12:48 | <ski> | bwe : let's say you wanted to check the left neutral element law : |
| 18:13:01 | <ski> | return a >>= amb = amb a |
| 18:13:28 | <ski> | so, you'd start at one end |
| 18:13:37 | <ski> | return a >>= amb |
| 18:13:50 | <ski> | and then unfold/inline your definition `return' |
| 18:14:08 | <ski> | = MkMaybeeState (\z -> (Just a,z)) >>= amb |
| 18:14:14 | <bwe> | MkMaybeeState (\z s> (Just x, z)) >>= amb |
| 18:14:20 | <bwe> | oh :) |
| 18:14:23 | <ski> | yes |
| 18:14:36 | <ski> | and then you'd use your definition of `(>>=)' |
| 18:15:48 | <ski> | = MkMaybeeState $ \s0 -> case (\z -> (Just a,z)) s0 of (Just a,s1) -> let MkMaybeeState f' = amb a in f' s1; (Nothing,s1) -> (Nothing,s1) |
| 18:16:10 | <ski> | and then you can start simplifyig. i suggest starting with the `(\z -> (Just a,z)) s0' part |
| 18:17:03 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:17:51 | <ski> | (btw, if you turned on `{-# LANGUAGE BlockArguments #-}', at the top of the file, you could avoid those `$'s) |
| 18:17:55 | <bwe> | my definition excludes the variant Nothing |
| 18:18:28 | <bwe> | but let me work it through first |
| 18:18:32 | <ski> | well, can you do a simplification of the above expression, step by step, repeating each complete expression after each simplification step ? |
| 18:18:55 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Ping timeout: 255 seconds) |
| 18:19:17 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 18:21:17 | <bwe> | (\z -> (Just a,z)) s0 is equivalent to return x |
| 18:21:33 | <bwe> | so I am replacing that |
| 18:24:40 | × | rito quits (~ritog@45.112.243.47) (Ping timeout: 255 seconds) |
| 18:27:33 | × | danse-nr3 quits (~danse@151.47.16.49) (Ping timeout: 268 seconds) |
| 18:29:23 | <ski> | bwe : equivalent to `return a', but yes |
| 18:29:54 | <ski> | (i used `a' and `amb', not `x' and `f', in the original formulation of the law) |
| 18:30:01 | <bwe> | right |
| 18:30:13 | <ski> | (as mnemonics : `a :: a' and `amb :: a -> m b') |
| 18:30:31 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 18:33:01 | × | misterfish quits (~misterfis@84-53-85-146.bbserv.nl) (Ping timeout: 276 seconds) |
| 18:39:33 | → | chomwitt joins (~chomwitt@2a02:587:7a09:c300:1ac0:4dff:fedb:a3f1) |
| 18:41:09 | × | igemnace quits (~ian@user/igemnace) (Remote host closed the connection) |
| 18:41:16 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 18:41:48 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:42:11 | → | danza joins (~francesco@rm-19-62-121.service.infuturo.it) |
| 18:46:49 | → | petrolblue joins (~anon@2a02:908:1065:4340::1c45) |
| 18:48:10 | → | rito joins (~ritog@45.112.243.47) |
| 18:48:48 | × | danza quits (~francesco@rm-19-62-121.service.infuturo.it) (Ping timeout: 252 seconds) |
| 18:52:26 | × | benjaminl quits (~benjaminl@user/benjaminl) (Ping timeout: 256 seconds) |
| 18:53:15 | → | machinedgod joins (~machinedg@93-136-134-38.adsl.net.t-com.hr) |
| 18:55:26 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Remote host closed the connection) |
| 19:01:25 | × | euleritian quits (~euleritia@dynamic-002-247-248-090.2.247.pool.telefonica.de) (Read error: Connection reset by peer) |
| 19:01:43 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:05:32 | → | YuutaW joins (~YuutaW@mail.yuuta.moe) |
| 19:09:20 | <dminuoso_> | reallyUnsafeStateCoerce = unsafeCoerce# |
| 19:09:30 | <dminuoso_> | Today is the day I get to use this thing in production code. :) |
| 19:09:56 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 19:11:04 | <EvanR> | for a minute I thought we were talking about amb i.e. the opposite of unamb |
| 19:11:24 | <EvanR> | doesn't seem to come up much in haskell for some reason |
| 19:11:55 | × | bratwurst quits (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) (Ping timeout: 260 seconds) |
| 19:12:40 | → | pretty_dumm_guy joins (~trottel@2a02:810b:43bf:aba0:dc82:dff8:b6b:479) |
| 19:12:43 | <int-e> | dminuoso_: what could possibly go wrong? |
| 19:12:59 | × | gawen quits (~gawen@user/gawen) (Quit: cya) |
| 19:14:46 | <dminuoso_> | int-e: Pretty much nothing. I just freely coerce between ZeroBitType state tokens. |
| 19:15:13 | <bwe> | ski: do I work on both sides of = ? |
| 19:15:21 | <dminuoso_> | Roughly I have this thing parametric over arbitrary ZeroBitType state tokens (a kind of no-effect/ST/IO polymorphism), and I want to run IO inside (irrespective of whats outside) |
| 19:15:33 | <int-e> | dminuoso_: ah, boring! |
| 19:15:35 | <int-e> | ;) |
| 19:16:05 | × | cimento quits (CO2@gateway/vpn/protonvpn/cimento) (Quit: WeeChat 4.1.2) |
| 19:16:25 | <int-e> | (Well, so far. *If* this results in a bug that could become a fascinating anecdote. :) ) |
| 19:16:44 | → | cimento joins (CO2@gateway/vpn/protonvpn/cimento) |
| 19:17:45 | <ski> | bwe : start from one side, see how far you get. if needed, also start from the other side |
| 19:18:20 | <bwe> | ski: what's my aim? to make both sides stating the same? |
| 19:18:25 | <ski> | yes |
| 19:18:54 | <bwe> | now I have case (return a) s0 of on the right side |
| 19:24:13 | <ski> | unfold/inline `return' ? |
| 19:24:32 | → | gawen joins (~gawen@user/gawen) |
| 19:24:52 | <ski> | (also, are you sure you didn't miss some data constructor or field selector ?) |
| 19:25:52 | <ski> | @hoogle Word0 |
| 19:25:52 | <lambdabot> | System.Console.Repline Word0 :: WordCompleter m -> CompleterStyle m |
| 19:25:54 | × | glguy quits (g@libera/staff/glguy) (Quit: Quit) |
| 19:26:03 | <ski> | @hoogle Int0 |
| 19:26:03 | <lambdabot> | GHC.Fingerprint fingerprint0 :: Fingerprint |
| 19:26:04 | <lambdabot> | Fingerprint fingerprint0 :: Fingerprint |
| 19:26:04 | <lambdabot> | Text.Ginger.GVal toInt0 :: GVal m -> Int |
| 19:27:15 | → | glguy joins (g@libera/staff/glguy) |
| 19:27:34 | <bwe> | ski: https://gist.github.com/benjaminweb/bcaccecbdde765e05360a452c3d5a074 |
| 19:28:46 | <ski> | bwe : you should add the starting points (that i gave), to that sequence of rewritings, as well |
| 19:29:35 | <EvanR> | when you're playing with zero-size types whose only purpose is to affect the type system, and then you unsafeCoerce, what's the point xD |
| 19:29:40 | × | gawen quits (~gawen@user/gawen) (Quit: cya) |
| 19:29:56 | × | glguy quits (g@libera/staff/glguy) (Client Quit) |
| 19:29:58 | <EvanR> | I guess you can have a small "kernel of trust" module which is proved correct once |
| 19:30:01 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 255 seconds) |
| 19:30:10 | → | glguy joins (g@libera/staff/glguy) |
| 19:30:19 | <ski> | also, don't repeat the definition of `(>>=)' (specialized as per your particular call), especially not multiple times .. there's no reason to, here |
| 19:31:10 | <ski> | also, make up your mind. use `return a' or `return x', but not both |
| 19:31:19 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 240 seconds) |
| 19:31:51 | <ski> | (you say `MkMaybeeState (\z -> (Just x, z)) >>= amb = ...', with `x' there rather than `a', which suggests you started with `return x' (not `return a'), although you didn't show what you started with) |
| 19:33:23 | <ski> | bwe : oh, i see what you're (trying to) do. you went from `(\z -> (Just (a, z))) s0' to `(return a) s0' .. that's the wrong direction ! that's getting further away from computed results, not closer to them ! |
| 19:33:35 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 19:33:39 | bwe | sighs |
| 19:34:06 | <[exa]> | good evening all, how's your lambdas |
| 19:34:16 | <ski> | also, replacing `amb a' with `MkMaybeeState (\z -> (Just x, z))' is incorrect (since that's `return x', which you can't assume `amb a' to be equal to. `amb' is arbitrary) |
| 19:35:24 | <bwe> | ski: I am taking a break until tomorrow, can't think clearly |
| 19:35:24 | <ski> | bwe : hmm .. perhaps, as a warm-up, you could try to prove that `(++)' has `[]' as left and right neutral element, and that `(++)' is associative .. iow, proving that `[]' and `(++)' forms a monoid |
| 19:35:36 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 19:35:40 | <ski> | as a warm-up for proving laws, i mean |
| 19:35:54 | <bwe> | let me do that tomorrow |
| 19:36:17 | <bwe> | proving means I am simplifying one side step by step so it becomes the other side |
| 19:36:23 | <ski> | (since your `(>>=)' is relatively complicated, so it's easy to get lost in it, or confused about what one's trying to do) |
| 19:36:41 | <ski> | or simplifying both sides, until you've massaged them to look the same |
| 19:36:44 | <bwe> | ski: but anyways, I feel my return is flawed |
| 19:37:04 | <ski> | (there may also be some more creative steps than simplifying. but simpifying is a large part of it) |
| 19:37:27 | <ski> | why do you think so ? |
| 19:38:32 | → | gawen joins (~gawen@user/gawen) |
| 19:39:17 | <[exa]> | bwe: are you aiming for the (StateT s Maybe) or (MaybeT (State s)) semantics? (sorry might have missed that in the scrollback) |
| 19:39:52 | <ski> | [exa] : it's un[4~clear (they haven't started thinking about this yet, i think) |
| 19:40:26 | <monochrom> | Is this MaybeT State? You can prove that State satisfies laws, and prove MaybeT M satisfies laws if you know M satisfies laws. This will be much cleaner than confronting MaybeT State as a monolith. |
| 19:40:37 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) (Ping timeout: 276 seconds) |
| 19:41:19 | <monochrom> | As it happens, this goes deeps into why people think verifying 1M LOC is impossible and why they are wrong. |
| 19:41:50 | [exa] | . o O ( 1M LOC in Matlab ) |
| 19:42:21 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 19:42:21 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 19:42:21 | finn_elija | is now known as FinnElija |
| 19:42:54 | <[exa]> | ski: oic, thx |
| 19:44:35 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 19:46:30 | → | ericcodes joins (~ericcodes@pool-72-83-186-186.washdc.fios.verizon.net) |
| 19:48:12 | × | petrolblue quits (~anon@2a02:908:1065:4340::1c45) (Quit: petrolblue) |
| 19:49:26 | <EvanR> | metadiscussion: list, [], and ++ is said to form a monoid, and sometimes the especially fast and loose will said it *is a* monoid. And from the perspective of hardline dependent type environments, I would say you could package them up to be used as a monoid (which is some type serving as a uniform interface). How many other ways can we skin a cat and is there any difference... |
| 19:49:29 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 19:50:14 | <EvanR> | *is a* served the purposes fine back in abstract algebra 101 |
| 19:51:05 | <monochrom> | Two theorem provers, Isabel and Lean, have adopted the type class approach for this. |
| 19:51:58 | ericcodes | is now known as Guest3304 |
| 19:51:58 | × | Guest3304 quits (~ericcodes@pool-72-83-186-186.washdc.fios.verizon.net) (Killed (tantalum.libera.chat (Nickname regained by services))) |
| 19:52:20 | → | ericcodes joins (~user@pool-72-83-186-186.washdc.fios.verizon.net) |
| 19:53:45 | <monochrom> | But while we are at it, *ML (pun on "meta"!) use modules and module interfaces. |
| 19:54:28 | <bwe> | [exa]: I am trying to let scalpel's Scraper return errors instead of just a Maybe. For this, I am trying to grasp monad transformers. For this I rolled my own Maybe, State. ski helped me a ton with that. Now I am rolling a thing that does Maybe and State at once. Next up should be Reader and Maybe. Then IO + Maybe. To see the pattern to emerge. |
| 19:54:38 | <ski> | length : (++) >---> (+) -- while we're at it |
| 19:54:41 | → | bramhaag74 joins (~bramhaag@endeavour.server.bramh.me) |
| 19:55:02 | <monochrom> | haha nice |
| 19:55:09 | × | bramhaag7 quits (~bramhaag@endeavour.server.bramh.me) (Read error: Connection reset by peer) |
| 19:55:09 | bramhaag74 | is now known as bramhaag7 |
| 19:55:27 | <EvanR> | *and* and *+* work talking about monads might be misleading because those are commutative, but there's at least two ways to combine all those pairs of monads depending on what you want to happen |
| 19:55:35 | <EvanR> | s/work/when/ |
| 19:55:36 | <ski> | (cue universal algebra, and categories for those) |
| 19:55:39 | <bwe> | do you know any visual explanation with boxes of monad transformers (or in my case doing the State and Maybe thing)? I feel that this would help me significantly. |
| 19:56:16 | <EvanR> | or a gastronomic explanation with burritos |
| 19:56:25 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 19:56:47 | <[exa]> | bwe: ah so, good. Honestly I'd recommend starting with IO+Maybe, because 1] Maybe is easiest and 2] you can't take IO apart which will prevent you from reimplementing it like State |
| 19:56:54 | <monochrom> | I don't think boxes are the right visuals for Maybe or MaybeT. |
| 19:57:00 | × | ericcodes quits (~user@pool-72-83-186-186.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
| 19:57:57 | <ncf> | [exa]: what's wrong with "is a" monoid? |
| 19:58:01 | <ncf> | sorry, EvanR * |
| 19:58:13 | <ncf> | as long as you're not saying "[a] is a monoid" |
| 19:58:22 | <monochrom> | I think box/block diagrams can only help read the code for State's >>=. For example, it won't help seeing why it satisfies laws. |
| 19:59:25 | <bwe> | monochrom: no, not for satisfying the laws; I was more after the pattern that leads me to the transformer like MaybeT. |
| 19:59:34 | <monochrom> | The right visual for Maybe may be decision trees. |
| 20:07:28 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 20:10:17 | <EvanR> | *can be packaged as a*, industrial semantics. *forms a* natural semantics. *is a* platonic semantics? xD |
| 20:11:49 | <[exa]> | "is" is dangerous, it's like saying "we all know which kind of equivalence I meant here right" |
| 20:12:12 | × | abrar_ quits (~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) (Quit: WeeChat 3.8) |
| 20:12:34 | <monochrom> | industrial? business? :) |
| 20:12:46 | <monochrom> | public relations? >:) |
| 20:13:02 | <dminuoso_> | [exa]: This is getting into silly language lawyering territory, as this kind of "is" is (!) at the meta language of us describing mathematical facts. |
| 20:13:10 | <monochrom> | equivalence? isomorphism? |
| 20:13:27 | → | abrar joins (~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) |
| 20:13:51 | <monochrom> | Three most common words Haskellers use without actual understanding: isomorphism, thunk, strict. |
| 20:13:52 | <[exa]> | dminuoso_: yeah, I hate it since I saw actual ontology authors using `is` as a fully qualified term :D |
| 20:13:53 | <dminuoso_> | When I say "In category theory, a monoid is...", you get into just an endless circle of pointless journeys that roundtrip through homotopy type theory if you try and debate about "is" in that sentence. |
| 20:14:28 | <[exa]> | "we call ...blabla... a 'monoid' " |
| 20:14:40 | <dminuoso_> | I dont think Ive ever heard someone debate over "Set X equipped with a binary operation and ... is a monoid". |
| 20:15:02 | <monochrom> | call by name? >:) |
| 20:15:05 | <dminuoso_> | Whether you use "is", "is called", "forms" - this is all discussions about the natural language itself. |
| 20:15:09 | <ncf> | i mean, the "is a" in "([a], [], (++)) is a monoid" is clearly meant to be read as "has type" |
| 20:15:20 | <monochrom> | EvanR: What is natural semantics? |
| 20:16:03 | <EvanR> | I'm thinking it forms a monoid like molecular clouds form solar systems and caves form stalactites xD |
| 20:16:12 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:16:16 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 20:16:45 | <monochrom> | You know of the Niklaus Wirth (the Pascal guy, e.g) joke about call by name and call by value? |
| 20:17:08 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 20:17:40 | <EvanR> | nope |
| 20:17:57 | → | petrolblue joins (~petrolblu@ip-095-222-169-156.um34.pools.vodafone-ip.de) |
| 20:18:12 | <monochrom> | So he was giving a talk in the US. He began with "in Europe they call me <correct Swiss pronounciation of his name>, in the US you call me Nickel's Worth. So Europeans call by name and Americans call by value." |
| 20:18:29 | <EvanR> | lol |
| 20:19:11 | × | lottaquestions quits (~nick@2607:fa49:503d:b200:2d55:64ae:c120:e947) (Quit: Konversation terminated!) |
| 20:20:10 | × | petrolblue quits (~petrolblu@ip-095-222-169-156.um34.pools.vodafone-ip.de) (Client Quit) |
| 20:20:24 | <monochrom> | There is also "has the monoid trait" e.g. Scala. |
| 20:21:14 | <monochrom> | I think I like the trait idea or equivalent. For example the real numbers has many traits: field, metric space, vector space, ... |
| 20:21:26 | <EvanR> | ok that one might have a more obvious practical difference, i.e. you can probably do more with monoids in scala than in math |
| 20:21:58 | <EvanR> | like, test to see if it has that trait xD |
| 20:22:04 | <monochrom> | Wait that can't be true. Math can prove monoid theorems, Scala can't. |
| 20:22:49 | <monochrom> | Well no, you can only test to see if someone has declared that it has that trait. |
| 20:23:20 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 20:23:25 | <monochrom> | which is no better than math, in which you check to see if someone has proved stuff. |
| 20:24:05 | <EvanR> | in the sense that you check to see if a turing machine halts |
| 20:24:06 | <dminuoso_> | EvanR: In fact, "Is a monoid" is a perfectly reasonable description, since there's plenty of mathematical constructions where you consider that tuple as objects or some kind. |
| 20:24:30 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 20:24:41 | <monochrom> | No, Scala does not enable the computer to discover that lists are monoids. |
| 20:24:55 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:24:57 | <EvanR> | but it's much more reliable at determining if someone defined the trait |
| 20:25:00 | <monochrom> | Scala at best enables someone to declare it. |
| 20:25:36 | <monochrom> | For lists yes it's in the stdlib and comes out of the box. But in general, for an arbitrary type? |
| 20:26:33 | <monochrom> | Someone has defined a new data structure and uploaded it to the Scala community library repo. But they have not declared that it is a monoid. |
| 20:26:46 | <EvanR> | checking if someone somewhere ever proved a particular machine halts or not might stall xD |
| 20:27:10 | <EvanR> | but that would be a cool programming language feature |
| 20:27:21 | <monochrom> | Now you wonder whether someone else has figured it out and uploaded an update or a companion library package that makes it a monoid. |
| 20:27:33 | <monochrom> | So now you have to search the community library package repo. |
| 20:28:01 | <monochrom> | This is no better than a mathematician searching the literature for a known theorem and proof. |
| 20:28:11 | <EvanR> | anyway, I wasn't trying to get into the nitty gritty of programming monoids |
| 20:28:35 | <EvanR> | just the rhetoric of calling them out in public |
| 20:28:42 | <dminuoso_> | Haskell design question. I have whats called a Codec, which is a data structure containing serialization/deserialization information for various things for communication with clients. All of this makes heavy use of Dynamic for a bunch of reasons, so you do something like `encode codec "User-Name" (mkText "text")` where "User-Name" is looked up in the structure and encoded according to what it |
| 20:28:44 | <dminuoso_> | finds. |
| 20:29:20 | <dminuoso_> | Now, a select few things require an additional secret for crypto stuff, but each client I communicate with has a different secret. |
| 20:30:15 | <dminuoso_> | With an interface like `encode :: Codec -> AttributeName -> Dynamic -> IO ByteString`, how would I sensibly inject a secret that would probably not be needed, but maybe yes. |
| 20:30:20 | <dminuoso_> | Pass it all the time? That feels wrong, somehow. |
| 20:30:50 | <EvanR> | when you build the codec the cryptokeys can be closed over and hidden within it |
| 20:31:46 | <EvanR> | dunno if it would be good design |
| 20:31:48 | <dminuoso_> | EvanR: Well I suppose I could have a sort of PreCodec (sans secret), and upon a connection with a client lookup its secret, and build a `Codec {secret = "foo", ..}` |
| 20:31:56 | <dminuoso_> | Mmm |
| 20:32:44 | <EvanR> | you wouldn't need a separate type or a field, if any "methods" use the cryptokey, they would access it from the closure. But if you don't have the key at codec construction time, that's out |
| 20:33:31 | <EvanR> | unless you get it from the IVar in the closure... which might be jumping the shark into overengineering slightly |
| 20:33:40 | <dminuoso_> | What is an IVar? |
| 20:33:51 | <EvanR> | a write-once variable you can read in pure code |
| 20:34:09 | <EvanR> | some thread can set its value at a later date |
| 20:34:36 | <EvanR> | dependency injection! |
| 20:35:12 | <EvanR> | ... just pass the key in to the function that needs it xD |
| 20:35:54 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9ce:2c57:5542:dde4) |
| 20:39:36 | → | petrolblue joins (~petrolblu@2a02:908:1065:4340::1c45) |
| 20:41:27 | → | dwt_ joins (~dwt_@2601:2c6:8381:e5c:606f:34a3:7300:6f05) |
| 20:44:27 | × | dwt__ quits (~dwt_@2601:2c6:8381:e5c:e4bc:2ef0:3dfa:99ac) (Ping timeout: 268 seconds) |
| 20:44:47 | × | ubert quits (~Thunderbi@178.165.165.175.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 20:46:52 | → | ubert joins (~Thunderbi@178.165.165.175.wireless.dyn.drei.com) |
| 20:49:14 | × | petrolblue quits (~petrolblu@2a02:908:1065:4340::1c45) (Quit: petrolblue) |
| 20:51:30 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 20:52:10 | rito | is now known as ritog |
| 20:52:53 | × | ritog quits (~ritog@45.112.243.47) (Quit: Leaving) |
| 21:00:01 | <ncf> | bwe: one way to convince yourself that MaybeT m a = m (Maybe a) is the right definition is that, for any monad m, there is a *distributive law* l :: Maybe (m a) -> m (Maybe a) , but no distributive law in the other direction in general |
| 21:00:32 | <ncf> | so, exercise 1 (easy): define l |
| 21:00:44 | John_Ivan | is now known as Lim_Fao |
| 21:01:56 | <ncf> | exercise 2 (harder): determine exactly what conditions such a distributive law l :: n (m a) -> m (n a) should satisfy in order to be able to make m ∘ n a monad |
| 21:04:06 | <ncf> | exercise 3: find similar distributive laws for Writer and Reader (hint: they may not all go in the same direction, i.e. you might have to use m ∘ n instead of n ∘ m) and derive WriterT and ReaderT from them |
| 21:04:26 | Lim_Fao | is now known as Der_Dumm_Nemetzk |
| 21:04:35 | Der_Dumm_Nemetzk | is now known as DerDummNemetzkii |
| 21:06:52 | <ncf> | exercise 1.1: prove, or at least convince yourself, that there is no general distributive law m (Maybe a) -> Maybe (m a) |
| 21:10:17 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 21:10:31 | × | bratwurst quits (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) (Remote host closed the connection) |
| 21:10:55 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 21:11:34 | × | ubert quits (~Thunderbi@178.165.165.175.wireless.dyn.drei.com) (Quit: ubert) |
| 21:12:37 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 21:13:00 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Max SendQ exceeded) |
| 21:14:03 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 21:15:43 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Max SendQ exceeded) |
| 21:16:46 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 21:18:22 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Max SendQ exceeded) |
| 21:19:24 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 21:22:51 | × | bratwurst quits (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) (Ping timeout: 245 seconds) |
| 21:27:22 | × | doyougnu quits (~doyougnu@45.46.170.68) (Ping timeout: 255 seconds) |
| 21:27:46 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 21:31:11 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 245 seconds) |
| 21:31:50 | → | doyougnu joins (~doyougnu@045-046-170-068.res.spectrum.com) |
| 22:02:39 | → | Feuermagier_ joins (~Feuermagi@user/feuermagier) |
| 22:02:39 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Killed (zirconium.libera.chat (Nickname regained by services))) |
| 22:02:39 | Feuermagier_ | is now known as Feuermagier |
| 22:06:21 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:10:48 | → | bryanv joins (~quassel@2603:c028:4503:7500:45b7:933:ab17:bc10) |
| 22:11:13 | <ski> | bwe : "do you know any visual explanation with boxes of monad transformers (or in my case doing the State and Maybe thing)? I feel that this would help me significantly." -- well, not quite that, but perhaps still could be useful/interesting : |
| 22:11:26 | <ski> | "railroad diagrams" for `Maybe'/`Either' <https://www.youtube.com/watch?v=srQt1NAHYC0#t=40m53s>,<https://www.slideshare.net/ScottWlaschin/functional-design-patterns-devternity2018> (starting at slide 90) |
| 22:11:36 | <ski> | the "state boxen" in "Lazy Functional State Threads" by John Launchbury,Simon L. Peyton Jones in 1993-11-08 - 1994-04-10 at <https://www.microsoft.com/en-us/research/wp-content/uploads/1994/06/lazy-functional-state-threads.pdf> |
| 22:11:46 | <ski> | "Monads, a Field Guide" by dpiponi 2006-10-21 at <http://blog.sigfpe.com/2006/10/monads-field-guide.html> |
| 22:11:59 | <ski> | also, you should probably at some point check out |
| 22:12:04 | <ski> | @where invented-monads |
| 22:12:04 | <lambdabot> | "You Could Have Invented Monads! (And Maybe You Already Have.)" by dpiponi in 2006-08-07 at <http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html> |
| 22:12:13 | <ski> | "The right visual for Maybe may be decision trees." -- or railroad diagrams |
| 22:12:24 | <monochrom> | Yeah. |
| 22:12:46 | <geekosaur> | has monad transformers step by step been mentioned? |
| 22:12:56 | <monochrom> | At some point I would also like to rant against this obsession with visuals. But perhaps another day. |
| 22:13:01 | <ski> | not that i recall, geekosaur |
| 22:13:18 | <ski> | Typeclassopedia, and "All About Monads" have, though |
| 22:13:37 | <ski> | (about half a month ago, when i talked to bwe last about this, before today) |
| 22:14:40 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 22:16:31 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 22:20:59 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:21:52 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 22:26:38 | × | bratwurst quits (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) (Ping timeout: 256 seconds) |
| 22:32:55 | <np> | is there a variant on zip that keeps the /longest/ list? something like this: (zipDefault [1, 2, 3] [4, 5] 0) -> ([(1, 4), (2, 5), (3, 0)]) |
| 22:34:06 | <ncf> | np: https://hackage.haskell.org/package/semialign-1.3/docs/Data-Semialign.html |
| 22:34:28 | <np> | ncf: cheers |
| 22:35:51 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 22:36:51 | <ncf> | :t alignWith |
| 22:36:52 | <lambdabot> | error: Variable not in scope: alignWith |
| 22:37:02 | <ncf> | @let import Data.Align |
| 22:37:02 | <lambdabot> | /sandbox/tmp/.L.hs:66:1: error: |
| 22:37:03 | <lambdabot> | Could not find module ‘Data.Align’ |
| 22:37:03 | <lambdabot> | Use -v (or `:set -v` in ghci) to see a list of the files searched for. |
| 22:37:07 | <ncf> | :( |
| 22:41:16 | → | zetef joins (~quassel@95.77.17.251) |
| 22:42:42 | × | pretty_dumm_guy quits (~trottel@2a02:810b:43bf:aba0:dc82:dff8:b6b:479) (Quit: WeeChat 3.5) |
| 22:44:36 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 22:45:52 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 256 seconds) |
| 22:48:24 | × | bratwurst quits (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) (Ping timeout: 268 seconds) |
| 22:49:17 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 22:52:24 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 22:55:17 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 23:00:09 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 252 seconds) |
| 23:00:22 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 23:00:23 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 23:07:07 | × | haskellbridge quits (~haskellbr@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 23:09:55 | × | chomwitt quits (~chomwitt@2a02:587:7a09:c300:1ac0:4dff:fedb:a3f1) (Ping timeout: 260 seconds) |
| 23:11:59 | → | haskellbridge joins (~haskellbr@069-135-003-034.biz.spectrum.com) |
| 23:11:59 | ChanServ | sets mode +v haskellbridge |
| 23:12:40 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 246 seconds) |
| 23:13:03 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 23:14:22 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 23:17:13 | → | Square2 joins (~Square4@user/square) |
| 23:19:51 | × | acidjnk_new quits (~acidjnk@p200300d6e72b933411fabc01fd6787da.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 23:20:39 | × | Square quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 23:20:46 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:21:25 | × | sawilagar quits (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 23:21:49 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 23:26:33 | → | wroathe joins (~wroathe@50.205.197.50) |
| 23:26:33 | × | wroathe quits (~wroathe@50.205.197.50) (Changing host) |
| 23:26:33 | → | wroathe joins (~wroathe@user/wroathe) |
| 23:34:57 | × | xff0x quits (~xff0x@ai096045.d.east.v6connect.net) (Ping timeout: 268 seconds) |
| 23:35:59 | × | machinedgod quits (~machinedg@93-136-134-38.adsl.net.t-com.hr) (Ping timeout: 264 seconds) |
| 23:36:53 | → | xff0x joins (~xff0x@178.255.149.135) |
| 23:38:58 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 260 seconds) |
| 23:44:55 | × | myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection) |
| 23:44:58 | <monochrom> | Darn I am trumped by GHC strictness AI again. |
| 23:45:28 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 23:45:52 | <monochrom> | So I wanted to show what reverse looks like in STG, Cmm, and asm. "foo acc (x:xs) = foo (x:acc) xs; foo acc [] = acc". |
| 23:46:34 | <monochrom> | I was hoping that for simplicity I could omit the base case "foo acc [] = acc" in hope that the STG etc would be less clutter. |
| 23:47:31 | <monochrom> | But GHC sees that if xs is finite, the function will bottom out anyway; and if xs is infinite, no one will see the x:acc construction. |
| 23:47:57 | <monochrom> | So the optimized code becomes: "foo _ (_:xs) = foo xs" -_-; |
| 23:48:09 | <Lycurgus> | so from this, i'm inferreing that 'strictness AI' means the general complier without forcing strictness |
| 23:48:27 | <monochrom> | "If it diverges anyway, better to diverge in constant space..." |
| 23:51:02 | → | Sgeo joins (~Sgeo@user/sgeo) |
All times are in UTC on 2023-12-06.