Logs on 2023-08-23 (liberachat/#haskell)
| 00:03:16 | <Inst> | type families maybe? |
| 00:05:14 | × | ulysses4ever quits (~artem@c-73-103-90-145.hsd1.in.comcast.net) (Read error: Connection reset by peer) |
| 00:05:25 | → | ulysses4ever joins (~artem@2601:249:4380:8950:f474:e3f8:9806:671) |
| 00:07:02 | <EvanR> | GADTs can hold a type class dictionary by putting a context on the ctor |
| 00:07:30 | <EvanR> | a newtype can only have 1 component |
| 00:09:02 | <Inst> | ah, so it's an implementation problem? Probably I should just stop procrastinating by trying to play around with fancy types and actually build stuff instead |
| 00:09:22 | → | abrantesasf joins (~abrantesa@177.137.232.92) |
| 00:12:13 | → | sm joins (~sm@plaintextaccounting/sm) |
| 00:12:50 | <geekosaur> | datatype contexts apply when building a value but you can't recover the information when you use the value. GADTs include a dictionary so the information can be recovered |
| 00:14:44 | <Inst> | i maen i should focus on features instead, instead of this fancy type nonsense |
| 00:15:11 | <Inst> | i just got besotted by someone on Discourse who was abusing monadic do with writer |
| 00:15:24 | <Inst> | i thought it'd be cool to replace a 2D list with a do block |
| 00:15:41 | ski | . o O ( `newtype Dict cxt = cxt => WrapDict -- one component' ) |
| 00:16:37 | × | sm quits (~sm@plaintextaccounting/sm) (Ping timeout: 245 seconds) |
| 00:18:57 | <EvanR> | nice |
| 00:19:28 | → | bopqod joins (~ubuntu@user/bopqod) |
| 00:23:28 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 00:24:35 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:25:02 | <[Leary]> | In reality, you probably have to settle for `newtype Dict cxt = Dict{ withDict :: forall r. (cxt => r) -> r }`. |
| 00:26:05 | <[Leary]> | Not sure if that saves you anything over the `data` version. |
| 00:30:29 | × | NewtonTrendy quits (uid282092@user/bopqod) () |
| 00:31:38 | bopqod | is now known as NewtonTrendy |
| 00:38:04 | × | ski quits (~ski@129.16.31.191) (Ping timeout: 248 seconds) |
| 00:43:44 | × | libertyprime quits (~libertypr@203.96.203.44) (Quit: Lost terminal) |
| 00:45:30 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 245 seconds) |
| 00:47:44 | × | mima quits (~mmh@aftr-62-216-211-141.dynamic.mnet-online.de) (Ping timeout: 256 seconds) |
| 00:49:28 | × | Square2 quits (~Square4@user/square) (Ping timeout: 250 seconds) |
| 00:53:21 | × | falafel quits (~falafel@216.68.6.51.dyn.plus.net) (Ping timeout: 246 seconds) |
| 00:54:09 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 00:59:43 | → | sm joins (~sm@plaintextaccounting/sm) |
| 01:02:16 | → | artem joins (~artem@73.145.241.118) |
| 01:03:24 | × | troydm quits (~troydm@user/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 01:04:12 | × | sm quits (~sm@plaintextaccounting/sm) (Ping timeout: 260 seconds) |
| 01:04:28 | → | troydm joins (~troydm@user/troydm) |
| 01:04:57 | × | ulysses4ever quits (~artem@2601:249:4380:8950:f474:e3f8:9806:671) (Ping timeout: 245 seconds) |
| 01:06:20 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 245 seconds) |
| 01:07:24 | × | Inst quits (~liamzy@2601:6c4:4085:6d50::d547) (Remote host closed the connection) |
| 01:07:42 | → | Inst joins (~liamzy@2601:6c4:4085:6d50::7d) |
| 01:10:38 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:11:48 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 01:13:46 | <EvanR> | Inst, you're glossing, like, using gloss to visualize types? cool |
| 01:15:23 | → | re101-eel-85 joins (~re101-eel@2606:40:48:6841::1064:304e) |
| 01:16:45 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:18:02 | → | danza_ joins (~francesco@an-19-166-29.service.infuturo.it) |
| 01:20:36 | × | danza__ quits (~francesco@151.43.215.52) (Ping timeout: 256 seconds) |
| 01:21:33 | × | abrantesasf quits (~abrantesa@177.137.232.92) (Remote host closed the connection) |
| 01:21:43 | <Inst> | no no no |
| 01:21:54 | <Inst> | i'm working on some side project, i.e, a joke library |
| 01:23:21 | <Inst> | abusing template haskell, and part of the joke was to stuff all the dumb stuff in |
| 01:23:30 | <Inst> | like, make it overly complicated in the backend |
| 01:24:00 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 246 seconds) |
| 01:24:32 | × | re101-eel-85 quits (~re101-eel@2606:40:48:6841::1064:304e) (Ping timeout: 246 seconds) |
| 01:28:54 | → | razetime joins (~quassel@117.254.37.57) |
| 01:30:12 | → | ulysses4ever joins (~artem@c-73-103-90-145.hsd1.in.comcast.net) |
| 01:31:19 | <Inst> | i'm trying to make a lib, my first ever, that extends file embed, lets you deploy files from your executable, produce hashes from them, check them against hashes, and grab them from online, it's a joke lib, very trivial functionality |
| 01:31:52 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 01:31:52 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 01:32:10 | × | artem quits (~artem@73.145.241.118) (Ping timeout: 245 seconds) |
| 01:32:16 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 01:32:52 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 01:33:39 | <Hooloovoo> | it doesn't sound like a very funny joke |
| 01:37:24 | <Inst> | i'm looking for help to try to make it into a fizzbuzz enterprise edition |
| 01:37:44 | <Inst> | i.e, stuff it with dependent types, everything weird and experimental |
| 01:42:10 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 01:47:58 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-fc05-5499-f77c-fbe5.res6.spectrum.com) (Remote host closed the connection) |
| 01:51:28 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-fc05-5499-f77c-fbe5.res6.spectrum.com) |
| 01:51:54 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-fc05-5499-f77c-fbe5.res6.spectrum.com) (Remote host closed the connection) |
| 01:52:20 | × | td_ quits (~td@i5387091D.versanet.de) (Ping timeout: 256 seconds) |
| 01:53:59 | → | td_ joins (~td@i53870917.versanet.de) |
| 01:54:01 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-fc05-5499-f77c-fbe5.res6.spectrum.com) |
| 01:54:01 | → | sm joins (~sm@plaintextaccounting/sm) |
| 01:58:27 | × | sm quits (~sm@plaintextaccounting/sm) (Ping timeout: 246 seconds) |
| 01:58:33 | → | jabuxas joins (~jabuxas@user/jabuxas) |
| 02:06:12 | × | xff0x quits (~xff0x@2405:6580:b080:900:a30:2bd2:51c4:52fd) (Ping timeout: 245 seconds) |
| 02:07:22 | × | jabuxas quits (~jabuxas@user/jabuxas) (Quit: Leaving.) |
| 02:07:31 | → | jabuxas joins (~jabuxas@user/jabuxas) |
| 02:08:06 | × | mvk quits (~mvk@2607:fea8:5c9a:a600::1c6d) (Ping timeout: 246 seconds) |
| 02:11:54 | → | artem joins (~artem@c-73-103-90-145.hsd1.in.comcast.net) |
| 02:11:55 | × | ulysses4ever quits (~artem@c-73-103-90-145.hsd1.in.comcast.net) (Read error: Connection reset by peer) |
| 02:11:55 | × | jabuxas quits (~jabuxas@user/jabuxas) (Client Quit) |
| 02:15:48 | → | nate2 joins (~nate@98.45.169.16) |
| 02:16:58 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 244 seconds) |
| 02:21:02 | × | gatekempt quits (~gatekempt@user/gatekempt) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 02:22:44 | × | td_ quits (~td@i53870917.versanet.de) (Ping timeout: 246 seconds) |
| 02:24:22 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) |
| 02:24:36 | → | td_ joins (~td@i5387090D.versanet.de) |
| 02:27:49 | × | AlexZenon quits (~alzenon@178.34.150.48) (Ping timeout: 244 seconds) |
| 02:27:53 | <justsomeguy> | You should define a DSL that generates your real program. |
| 02:28:16 | <justsomeguy> | That will up the complexity... |
| 02:28:36 | × | Alex_test quits (~al_test@178.34.150.48) (Ping timeout: 256 seconds) |
| 02:33:21 | → | AlexZenon joins (~alzenon@178.34.150.48) |
| 02:33:31 | <Inst> | already working the TH, and bashing my head in because it's giving me not in scope errors |
| 02:33:41 | <Inst> | maybe that's why snoyman never expanded file embed to support traversables |
| 02:34:20 | → | Alex_test joins (~al_test@178.34.150.48) |
| 02:34:51 | → | ft joins (~ft@p508db17b.dip0.t-ipconnect.de) |
| 02:36:31 | → | sm joins (~sm@plaintextaccounting/sm) |
| 02:39:03 | × | ddellacosta quits (~ddellacos@146.70.168.136) (Ping timeout: 246 seconds) |
| 02:41:04 | × | sm quits (~sm@plaintextaccounting/sm) (Ping timeout: 256 seconds) |
| 02:41:22 | → | ddellacosta joins (~ddellacos@146.70.165.10) |
| 02:41:28 | <monochrom> | You're running into what the Scheme people call "hygienic macros" vs variable capture. |
| 02:42:30 | <monochrom> | If you desire variable capture but you actually have a hygienic macro, that will be an unexpected var-not-found. |
| 02:43:11 | <monochrom> | Conversely, if you desire no variable capture but you actually have a non-hygienic (variable-capturing) macro, that will be an unexpected unsoundness. |
| 02:50:57 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:50:57 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:50:57 | finn_elija | is now known as FinnElija |
| 02:53:21 | × | Achylles quits (~Achylles_@45.182.57.81) (Quit: Leaving) |
| 02:55:37 | <dolio> | Everyone who's thinking clearly want hygienic macros, though. |
| 02:56:08 | <monochrom> | I agree, hence unsoundness :) |
| 02:56:35 | <dolio> | Manually avoiding variable capture is so much harder to get right than using some extra feature for the times you actually want variable capture. |
| 02:59:30 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 03:05:07 | → | myyo joins (~myyo@75-166-145-203.hlrn.qwest.net) |
| 03:06:18 | → | powderhorn joins (~powderhor@207-153-12-54.static.fttp.usinternet.com) |
| 03:07:27 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 245 seconds) |
| 03:07:54 | × | Inst quits (~liamzy@2601:6c4:4085:6d50::7d) (Remote host closed the connection) |
| 03:08:34 | → | Inst joins (~liamzy@2601:6c4:4085:6d50::d547) |
| 03:10:08 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 03:10:59 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 03:11:08 | × | hugo quits (znc@2001:6b0:17:f0a0::17) (Ping timeout: 248 seconds) |
| 03:11:28 | <Inst> | monochrome: the actual issue was that I was playing type tetris because I wanted to use traverse, and somehow created two separate calls to newName |
| 03:12:19 | <monochrom> | OK, so hashwashing OCD :) |
| 03:12:27 | <Inst> | georgeClooney_a2Jg :: ByteString |
| 03:12:27 | <Inst> | georgeClooney_a2Jh |
| 03:12:27 | <Inst> | = |
| 03:12:34 | <Inst> | didn't notice it |
| 03:15:40 | × | myyo quits (~myyo@75-166-145-203.hlrn.qwest.net) (Read error: Connection reset by peer) |
| 03:15:41 | → | myyo_ joins (~myyo@75-166-145-203.hlrn.qwest.net) |
| 03:16:36 | → | myyo joins (~myyo@75-166-145-203.hlrn.qwest.net) |
| 03:16:36 | × | myyo_ quits (~myyo@75-166-145-203.hlrn.qwest.net) (Read error: Connection reset by peer) |
| 03:16:59 | <EvanR> | encode messages in your variables names by spelling everything backwards |
| 03:17:03 | <EvanR> | you know you want to |
| 03:18:57 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 03:19:08 | × | nate2 quits (~nate@98.45.169.16) (Ping timeout: 248 seconds) |
| 03:22:00 | × | elkcl quits (~elkcl@broadband-95-84-226-240.ip.moscow.rt.ru) (Ping timeout: 250 seconds) |
| 03:24:48 | → | zmt01 joins (~zmt00@user/zmt00) |
| 03:25:44 | → | hgolden_ joins (~hgolden@2603-8000-9d00-3ed1-fc05-5499-f77c-fbe5.res6.spectrum.com) |
| 03:26:05 | × | flukiluke quits (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Ping timeout: 246 seconds) |
| 03:26:24 | → | flukiluke joins (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
| 03:27:50 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 246 seconds) |
| 03:28:11 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-fc05-5499-f77c-fbe5.res6.spectrum.com) (Ping timeout: 246 seconds) |
| 03:28:35 | × | bilegeek quits (~bilegeek@2600:1008:b084:26e1:642d:15c:b0a8:d815) (Quit: Leaving) |
| 03:28:53 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 03:33:32 | × | Inst quits (~liamzy@2601:6c4:4085:6d50::d547) (Remote host closed the connection) |
| 03:33:49 | → | Inst joins (~liamzy@2601:6c4:4085:6d50::d547) |
| 03:40:09 | × | jmcantrell quits (~weechat@user/jmcantrell) (Quit: WeeChat 4.0.3) |
| 03:40:41 | → | elkcl joins (~elkcl@broadband-95-84-226-240.ip.moscow.rt.ru) |
| 03:44:00 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 03:45:37 | × | myyo quits (~myyo@75-166-145-203.hlrn.qwest.net) () |
| 03:48:57 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 04:01:14 | → | aforemny_ joins (~aforemny@2001:9e8:6cf2:c700:b41f:8d5e:8e07:ee66) |
| 04:02:06 | × | aforemny quits (~aforemny@i59F516F9.versanet.de) (Ping timeout: 245 seconds) |
| 04:07:05 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 04:09:09 | × | smalltalkman quits (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:11:20 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 04:12:01 | × | g quits (g@libera/staff-emeritus/glguy) (Remote host closed the connection) |
| 04:12:09 | → | g joins (g@libera/staff-emeritus/glguy) |
| 04:16:12 | × | razetime quits (~quassel@117.254.37.57) (Ping timeout: 248 seconds) |
| 04:17:52 | × | thegeekinside quits (~thegeekin@189.180.79.225) (Ping timeout: 260 seconds) |
| 04:17:52 | × | artem quits (~artem@c-73-103-90-145.hsd1.in.comcast.net) (Read error: Connection reset by peer) |
| 04:17:52 | → | ulysses4ever joins (~artem@c-73-103-90-145.hsd1.in.comcast.net) |
| 04:21:37 | × | g quits (g@libera/staff-emeritus/glguy) (Remote host closed the connection) |
| 04:21:45 | → | g joins (g@libera/staff-emeritus/glguy) |
| 04:51:45 | × | g quits (g@libera/staff-emeritus/glguy) (Remote host closed the connection) |
| 04:51:53 | → | g joins (g@libera/staff-emeritus/glguy) |
| 05:01:39 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 246 seconds) |
| 05:02:40 | → | razetime joins (~quassel@117.254.37.57) |
| 05:03:26 | <dsal> | People are pretty weird about readability and identifier names. I had someone recently say that `x` should have a more detailed (expanded? I don't remember the exact word) name in case maybeSomething of; Just x -> doSomethingWith x; Nothing -> doNothing |
| 05:04:16 | <dsal> | Like, do you need to call this "something"? Because I can look up more easily than I can do long string character matches in my head. |
| 05:06:08 | <c_wraith> | you should call it "theThingIDon'tCareAbout" |
| 05:06:17 | <c_wraith> | fortunately, apostrophes are allowed in identifiers |
| 05:07:23 | <c_wraith> | Though if someone complained about that to me, I'd replace the whole case with a call to maybe |
| 05:11:31 | × | shapr quits (~user@2600:1700:c640:3100:944:4982:f0a2:9b14) (Ping timeout: 246 seconds) |
| 05:14:20 | <mauke> | hey, I just met you |
| 05:15:02 | <Axman6> | dsal: the better name is none at all, maybe doNothing doSomethingWith maybeSomething |
| 05:15:49 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 05:16:34 | <Axman6> | (and a style I sometimes use is maybeSomething & maybe doNothing doSomethingWith, which can make it clearer what the subject of the code is) |
| 05:17:44 | × | danza_ quits (~francesco@an-19-166-29.service.infuturo.it) (Read error: Connection reset by peer) |
| 05:17:50 | <mauke> | case maybeSomething of Just (doSomethingWith -> y) -> y; Nothing -> doNothing |
| 05:18:03 | → | danza_ joins (~francesco@151.47.200.141) |
| 05:18:27 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 246 seconds) |
| 05:19:01 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 05:19:23 | <monochrom> | Programmers are generally fanatic about superficial coding guides like that. |
| 05:20:26 | <monochrom> | "meaningful names (no exception), at most 60 lines per function (no exception), at most N columns per line (no exception), indentation must be ..." etc etc |
| 05:20:32 | <dsal> | Axman6: That's the direction I usually go. |
| 05:21:05 | <mauke> | a pattern I've seen in real code: case ... of thing@(isCromulent -> True) -> doStuff thing; ... |
| 05:22:22 | × | Inst quits (~liamzy@2601:6c4:4085:6d50::d547) (Ping timeout: 246 seconds) |
| 05:23:03 | <monochrom> | Programmers are incapable of unalgorithm it-depends value judgment (that's why they chose algorithmic programming, no?), that is why their coding style guides are simple mechanical checks that mean nothing. |
| 05:24:16 | <monochrom> | One style guide is going to be "never pointfree" and another is going to be "always pointfree". There is not going to be a reasonable style guide that says "pointfree when it makes sense, pointful when it makes sense". |
| 05:25:14 | <mauke> | I thought that was what the perl style guide was about :-) |
| 05:25:40 | → | johnw joins (~johnw@69.62.242.138) |
| 05:26:11 | <mauke> | "there's more than one way to do it, so choose the way that makes the most sense / is clearest for your particular situation" |
| 05:26:25 | → | Inst joins (~liamzy@2601:6c4:4085:6d50::725c) |
| 05:27:34 | <dsal> | Drives me insane when people equate longer names to more readable code. It's less readable to me personally, and I worked in a setting where we had people whose job was to study and understand readability and the consensus was that arbitrarily long identifier names don't help much. |
| 05:27:48 | <probie> | monochrom: Rigid, sometimes silly rules make for a few days of "wtf" but months of freedom from irrelevant decisions. It is optimising for employee mental health, and (hopefully) by extension, productivity |
| 05:28:08 | <dsal> | Though length proportional to scope is a handy rule of thumb. The same code that needed something longer than an `x` for the `Just` case had a parameter named `t` on a function that was like, a page long. That was OK, I guess. |
| 05:28:58 | <mauke> | also, identifier huffmanization |
| 05:29:10 | <dsal> | probie: That's true unless the rules are overly prescriptive and make it harder for the people to maintain a codebase to understand the codebase in favor of hypothetical people who aren't familiar with it and have no access to people who are. |
| 05:29:42 | <mauke> | names that you use all the time should be shorter than names you don't (or at least shouldn't) use often |
| 05:29:54 | <dsal> | Yeah, soft rules like that are helpful. |
| 05:30:04 | × | ddellacosta quits (~ddellacos@146.70.165.10) (Ping timeout: 246 seconds) |
| 05:30:07 | <mauke> | (cf. unsafePerformIO) |
| 05:30:21 | <dsal> | But also, a thing you use just one to move one line down doesn't need to be self-documenting when it's actually obvious. |
| 05:30:53 | <monochrom> | probie: Do you have data that shows that silly rules improve mental health? |
| 05:30:59 | <probie> | dsal: I don't inherently disagree, but every place I've worked with super prescriptive rules has been a pleasure to work at, and every place that was "just go for it", was a mediocre experience at best |
| 05:31:44 | <dsal> | I see people doing stuff like `let aThing = mkAThing in useAThing aThing` and like, why is that easier to read than `useAThing mkAThing` ? |
| 05:31:52 | <probie> | monochrom: no, only myself as a data point, but I'm also on the autism spectrum, so that probably ruins even that |
| 05:32:22 | → | ddellacosta joins (~ddellacos@146.70.166.100) |
| 05:32:45 | <monochrom> | Oh if we're only talking about personal experience, my personal experience is that disallowing myself to just use "foo" is the single most source of stress. |
| 05:33:22 | <monochrom> | And when I allow myself to just use "foo" and move on, my productivity increases by 500% instantly. |
| 05:33:27 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 05:33:46 | <monochrom> | To be sure, I don't abuse "foo", I use it when it really doesn't matter. |
| 05:33:49 | <mauke> | foo', foo'', foo''', foo'''' |
| 05:34:17 | <dsal> | There was some discussion around some coding style stuff in the codebase and a couple of my snippets ended up in the discussion, written a couple different ways. Luckily, I can't remember the details, but they'd be equivalents where I might do something like `something <$> fun1 <*> fun2` and people would be like, do you like that or `do; x <- fun1; y <- fun2; something x y` |
| 05:34:38 | <dsal> | One of them literally used `x` and `y` in one of those situations where the names meant absolutely nothing, but now I've got names and bindings and stuff to consider instead of just like, a simple applicative. |
| 05:34:49 | <mauke> | also, to reduce pointless arguments over names, all types should be called T, all classes C, and all functions f |
| 05:35:03 | <mauke> | if there's a conflict, make a new module |
| 05:35:31 | <dsal> | But the frustrating part is that this will be a helper in a where clause in a function that's got an incredibly robust test suite, but nobody would ever see. vs. the entire API surface of the application which is just a disaster. |
| 05:35:43 | <glguy> | Put f::a in your class C so you can reuse it a bunch |
| 05:36:24 | <glguy> | Easier to remember the name that way |
| 05:37:08 | <dsal> | mauke: I suggested that we not release a reusable framework `Thing` with all of the exported identifiers starting with `thing` (e.g., `thingThing` and `thingThingResultSuccess` and got pointed to a module that named a type `T` as an example of why that's bad or something. |
| 05:37:49 | → | michalz joins (~michalz@185.246.207.203) |
| 05:40:06 | <dsal> | It's hard for me to understand some people's concerns, to be honest. Person didn't want to export a symbol called `Success` because it conflicts with other thing. But that's like, only if you make a giant module importing a bunch of different unqualified modules that export `Success` and want to distinguish them. So like, don't do that. |
| 05:40:22 | <monochrom> | Consider using theDarkLordWhoMustNotBeName next time :) |
| 05:40:34 | <monochrom> | err, theDarkLordWhoMustNotBeNamed |
| 05:40:54 | → | sm joins (~sm@plaintextaccounting/sm) |
| 05:41:38 | <dsal> | I had someone complain *madly* when I suggested he didn't need a ~7 word identifier that was used once on the line below its definition. Told me he absolutely couldn't read the code unless it contained all the words. |
| 05:41:51 | × | sm quits (~sm@plaintextaccounting/sm) (Client Quit) |
| 05:42:35 | <dsal> | Something like `someValueFromSomeActionThatDoesAthing <- getSomeValueFromSomeActionThatDoesAthing; doSomeOtherActionWithThisThingIGot someValueFromSomeActionThatDoesAthing` |
| 05:44:08 | <dsal> | Our coding convention strongly recommended not doing that. Management got involved. The guy apparently had some neurodivergence that made it impossible to read code if every symbol didn't have its entire commit history in it. Which makes it pretty hard to work in a codebase where people don't do that. |
| 05:47:37 | <monochrom> | Style guides are written by the victors. |
| 05:47:54 | <monochrom> | History and style guides and "recipes" for success. |
| 05:49:01 | × | Guest3051 quits (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 248 seconds) |
| 05:49:10 | → | briandaed joins (~briandaed@185.234.210.211) |
| 05:52:33 | → | Guest3051 joins (sid1055@id-1055.tinside.irccloud.com) |
| 05:58:37 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 05:59:10 | → | acidjnk joins (~acidjnk@p200300d6e7072f05045f4aa7d8e8f055.dip0.t-ipconnect.de) |
| 06:05:22 | <dsal> | People like make rules about things that are easy to make rules about even if they don't have much impact. The things that have a lot of impact are a lot harder to codify, so we'll just leave those as an exercise for the maintainer. |
| 06:09:51 | → | CiaoSen joins (~Jura@2a05:5800:29f:f100:664b:f0ff:fe37:9ef) |
| 06:13:53 | <Axman6> | @quote+ monochrom Style guides are written by the victors. |
| 06:13:53 | <lambdabot> | No quotes match. BOB says: You seem to have forgotten your passwd, enter another! |
| 06:14:19 | <glguy> | Remember |
| 06:14:31 | <dsal> | lambdabot: my password is x |
| 06:15:16 | <Axman6> | @remember monochrom Style guides are written by the victors. |
| 06:15:16 | <lambdabot> | Done. |
| 06:15:40 | <Axman6> | Thanks - took me much longer than I hoped to find that via PM with lambdabot |
| 06:26:14 | → | sm joins (~sm@plaintextaccounting/sm) |
| 06:26:59 | × | sm quits (~sm@plaintextaccounting/sm) (Client Quit) |
| 06:29:54 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) (Remote host closed the connection) |
| 06:35:05 | × | ircbrowse_tom quits (~ircbrowse@static.162.49.55.162.clients.your-server.de) (ZNC 1.8.2+deb2build5 - https://znc.in) |
| 06:35:21 | → | ircbrowse_tom_ joins (~ircbrowse@static.162.49.55.162.clients.your-server.de) |
| 06:35:29 | Server | sets mode +Cnt |
| 06:35:44 | → | sympt3 joins (~sympt@user/sympt) |
| 06:35:53 | → | tired- joins (~tired@user/tired) |
| 06:35:57 | → | SheRejoined joins (haveident@libera/staff/she/her) |
| 06:36:00 | → | jackdk_ joins (sid373013@cssa/jackdk) |
| 06:36:03 | → | leeb- joins (~leeb@tk2-243-31079.vs.sakura.ne.jp) |
| 06:36:04 | → | xelxebar_ joins (~xelxebar@wilsonb.com) |
| 06:36:05 | → | stefan-__ joins (~cri@42dots.de) |
| 06:36:50 | → | fiddlerwoaroof joins (~fiddlerwo@user/fiddlerwoaroof) |
| 06:36:53 | → | natto17 joins (~natto@129.154.243.159) |
| 06:37:04 | → | Simikando joins (~Simikando@adsl-dyn1.91-127-51.t-com.sk) |
| 06:37:26 | → | raoul1 joins (~raoul@95.179.203.88) |
| 06:37:34 | → | pie__ joins (~pie_bnc@user/pie/x-2818909) |
| 06:38:03 | → | kjak_ joins (~kjak@pool-108-28-157-148.washdc.fios.verizon.net) |
| 06:38:03 | → | cln_ joins (cln@wtf.cx) |
| 06:38:05 | → | Hecate_ joins (~mariposa@user/hecate) |
| 06:38:11 | → | barrucad1 joins (~barrucadu@carcosa.barrucadu.co.uk) |
| 06:38:15 | → | gnyeki_ joins (~gnyeki@li578-216.members.linode.com) |
| 06:38:16 | × | gnyeki_ quits (~gnyeki@li578-216.members.linode.com) (Changing host) |
| 06:38:16 | → | gnyeki_ joins (~gnyeki@user/gnyeki) |
| 06:38:17 | → | root joins (~root@user/institor) |
| 06:38:21 | → | adium_ joins (adium@user/adium) |
| 06:38:39 | → | user2 joins (~user@162.255.84.96) |
| 06:38:42 | root | is now known as Guest7973 |
| 06:38:46 | → | sweater1 joins (~sweater@206.81.18.26) |
| 06:38:53 | → | kaol_ joins (~kaol@94-237-42-30.nl-ams1.upcloud.host) |
| 06:38:53 | → | dontdieych_ joins (~alarm@132.226.169.184) |
| 06:38:55 | × | institor quits (~root@user/institor) (Killed (NickServ (GHOST command used by Guest7973))) |
| 06:39:04 | Guest7973 | is now known as institor |
| 06:39:19 | × | She quits (haveident@libera/staff/she/her) (*.net *.split) |
| 06:39:19 | × | kjak quits (~kjak@pool-108-28-157-148.washdc.fios.verizon.net) (*.net *.split) |
| 06:39:19 | × | natto quits (~natto@129.154.243.159) (*.net *.split) |
| 06:39:19 | × | lambdap237 quits (~lambdap@static.167.190.119.168.clients.your-server.de) (*.net *.split) |
| 06:39:19 | × | SoF quits (~skius@user/skius) (*.net *.split) |
| 06:39:19 | × | sympt quits (~sympt@user/sympt) (*.net *.split) |
| 06:39:19 | × | tired quits (~tired@user/tired) (*.net *.split) |
| 06:39:19 | × | dontdieych quits (~alarm@132.226.169.184) (*.net *.split) |
| 06:39:19 | × | xelxebar quits (~xelxebar@wilsonb.com) (*.net *.split) |
| 06:39:19 | × | jackdk quits (sid373013@cssa/jackdk) (*.net *.split) |
| 06:39:19 | × | gnyeki quits (~gnyeki@user/gnyeki) (*.net *.split) |
| 06:39:19 | × | polux quits (~polux@51-15-169-172.rev.poneytelecom.eu) (*.net *.split) |
| 06:39:19 | × | barrucadu quits (~barrucadu@carcosa.barrucadu.co.uk) (*.net *.split) |
| 06:39:19 | × | fiddlerw- quits (~fiddlerwo@user/fiddlerwoaroof) (*.net *.split) |
| 06:39:19 | × | user1 quits (~user@162.255.84.96) (*.net *.split) |
| 06:39:19 | × | sweater quits (~sweater@206.81.18.26) (*.net *.split) |
| 06:39:19 | × | aku quits (~aku@65.108.245.241) (*.net *.split) |
| 06:39:19 | × | pie_ quits (~pie_bnc@user/pie/x-2818909) (*.net *.split) |
| 06:39:21 | × | adium quits (adium@user/adium) (*.net *.split) |
| 06:39:21 | × | raoul quits (~raoul@95.179.203.88) (*.net *.split) |
| 06:39:21 | × | ircbrowse_tom quits (~ircbrowse@static.162.49.55.162.clients.your-server.de) (*.net *.split) |
| 06:39:21 | × | Hecate quits (~mariposa@user/hecate) (*.net *.split) |
| 06:39:21 | × | cln quits (~cln@wtf.cx) (*.net *.split) |
| 06:39:21 | × | leeb quits (~leeb@tk2-243-31079.vs.sakura.ne.jp) (*.net *.split) |
| 06:39:21 | × | kaol quits (~kaol@94-237-42-30.nl-ams1.upcloud.host) (*.net *.split) |
| 06:39:21 | × | stefan-_ quits (~cri@42dots.de) (*.net *.split) |
| 06:39:21 | × | tdammers quits (~tdammers@219-131-178-143.ftth.glasoperator.nl) (*.net *.split) |
| 06:39:21 | SheRejoined | is now known as She |
| 06:39:21 | SoF1 | is now known as SoF |
| 06:39:21 | raoul1 | is now known as raoul |
| 06:39:21 | sympt3 | is now known as sympt |
| 06:39:21 | polux8 | is now known as polux |
| 06:39:21 | jackdk_ | is now known as jackdk |
| 06:39:21 | lambdap2371 | is now known as lambdap237 |
| 06:39:22 | leeb- | is now known as leeb |
| 06:43:31 | → | aku joins (~aku@65.108.245.241) |
| 06:45:39 | × | Simikando quits (~Simikando@adsl-dyn1.91-127-51.t-com.sk) (Quit: Leaving) |
| 06:51:15 | → | tdammers joins (~tdammers@219-131-178-143.ftth.glasoperator.nl) |
| 06:53:54 | → | fendor joins (~fendor@2a02:8388:1640:be00:b586:6c06:a58:19a3) |
| 06:56:53 | → | andrei_n joins (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) |
| 07:01:25 | → | jonathan__ joins (~jonathan@193.203.13.93) |
| 07:02:09 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:f1a1:7919:4ffc:e710) |
| 07:04:20 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:13:52 | → | oo_miguel joins (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) |
| 07:16:19 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 07:17:50 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 246 seconds) |
| 07:19:15 | × | razetime quits (~quassel@117.254.37.57) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 07:19:16 | → | ccapndave joins (~ccapndave@mob-194-230-146-105.cgn.sunrise.net) |
| 07:21:00 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 256 seconds) |
| 07:21:01 | xelxebar_ | is now known as xelxebar |
| 07:22:55 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 07:22:55 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 07:22:55 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 07:23:48 | → | mmhat joins (~mmh@p200300f1c7042784ee086bfffe095315.dip0.t-ipconnect.de) |
| 07:25:50 | → | mima joins (~mmh@aftr-62-216-211-216.dynamic.mnet-online.de) |
| 07:27:37 | → | sm joins (~sm@plaintextaccounting/sm) |
| 07:30:26 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) |
| 07:33:09 | <Axman6> | Type level records, is this a thing that can be easily done? I could possibly use a type class with associated types, but it would be nice to be able to take a record that exists and chance one value. |
| 07:33:16 | <mmhat> | -quit |
| 07:33:22 | × | mmhat quits (~mmh@p200300f1c7042784ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.0.4) |
| 07:36:04 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) (Ping timeout: 246 seconds) |
| 07:38:38 | × | ccapndave quits (~ccapndave@mob-194-230-146-105.cgn.sunrise.net) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 07:43:11 | × | bonz060 quits (~quassel@2001:bc8:640:f07::1) (Quit: No Ping reply in 180 seconds.) |
| 07:47:47 | <dminuoso> | Axman6: Well records are really just some superficial syntax sugar. With a tyfam and a multi-parameter type you can get the same effect. |
| 07:48:21 | <dminuoso> | It's just not as convenient, as you have to write the accessor/update tyfams explicitly. But I suppose you could cook up some TH to take the boilerplate off your hands. |
| 07:49:02 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:50:21 | × | fendor quits (~fendor@2a02:8388:1640:be00:b586:6c06:a58:19a3) (Remote host closed the connection) |
| 07:53:32 | <tdammers> | I believe singletons-th can do that for you, but it comes at a price... |
| 07:54:24 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:55:36 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 07:58:29 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 244 seconds) |
| 07:59:55 | aforemny_ | is now known as aforemny |
| 08:00:23 | × | powderhorn quits (~powderhor@207-153-12-54.static.fttp.usinternet.com) (Ping timeout: 246 seconds) |
| 08:02:22 | → | vglfr joins (~vglfr@cli-188-239-201-89.bbn.slav.dn.ua) |
| 08:02:30 | × | vglfr quits (~vglfr@cli-188-239-201-89.bbn.slav.dn.ua) (Remote host closed the connection) |
| 08:03:09 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 08:03:10 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 08:03:10 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 08:03:45 | → | SegmentationFaul joins (~Segmentat@185.151.84.54) |
| 08:06:21 | → | vglfr joins (~vglfr@cli-188-239-201-89.bbn.slav.dn.ua) |
| 08:07:18 | → | ccapndave joins (~ccapndave@mob-194-230-146-105.cgn.sunrise.net) |
| 08:07:30 | × | ccapndave quits (~ccapndave@mob-194-230-146-105.cgn.sunrise.net) (Client Quit) |
| 08:08:33 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 08:09:26 | → | kmein joins (~weechat@user/kmein) |
| 08:09:31 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 08:10:25 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 08:10:57 | <albet70> | when Data.List.Split would merge into Data.List? |
| 08:11:25 | × | danza_ quits (~francesco@151.47.200.141) (Ping timeout: 246 seconds) |
| 08:12:25 | <albet70> | Data.List lack some base methods to do with strings, Data.Text has those methods |
| 08:13:06 | → | bonz060 joins (~quassel@2001:bc8:640:f07::1) |
| 08:15:58 | × | cfricke quits (~cfricke@user/cfricke) (Ping timeout: 256 seconds) |
| 08:16:42 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 08:16:53 | <dminuoso> | albet70: I am not aware of any RFC to do this. |
| 08:19:28 | → | cfricke joins (~cfricke@user/cfricke) |
| 08:24:41 | × | bonz060 quits (~quassel@2001:bc8:640:f07::1) (Quit: No Ping reply in 180 seconds.) |
| 08:25:45 | × | andrei_n quits (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) (Remote host closed the connection) |
| 08:26:25 | → | andrei_n joins (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) |
| 08:26:45 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 08:26:51 | <lisbeths> | What about a version of currying where the beta normal form of the last computation is the input to the next function in the input stream. |
| 08:29:45 | × | andrei_n quits (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) (Remote host closed the connection) |
| 08:30:02 | → | andrei_n joins (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) |
| 08:30:19 | → | ubert joins (~Thunderbi@178.115.53.153.wireless.dyn.drei.com) |
| 08:32:58 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 256 seconds) |
| 08:33:35 | → | mechap joins (~mechap@user/mechap) |
| 08:34:27 | × | ubert quits (~Thunderbi@178.115.53.153.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 08:38:18 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 08:38:18 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 08:38:18 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 08:39:06 | × | infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 245 seconds) |
| 08:42:21 | → | infinity0 joins (~infinity0@pwned.gg) |
| 08:44:37 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:46:02 | → | danse-nr3 joins (~francesco@151.47.200.141) |
| 08:50:32 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 08:55:59 | → | logothesia joins (~logothesi@user/logothesia) |
| 08:56:45 | × | andrei_n quits (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) (Remote host closed the connection) |
| 08:57:03 | → | andrei_n joins (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) |
| 08:58:25 | × | jonathan__ quits (~jonathan@193.203.13.93) (Ping timeout: 245 seconds) |
| 08:59:49 | → | jonathan joins (~jonathan@193.203.13.97) |
| 09:02:55 | → | __monty__ joins (~toonn@user/toonn) |
| 09:04:12 | × | deviance quits (~deviance@bcdcac82.skybroadband.com) (Ping timeout: 248 seconds) |
| 09:09:06 | × | acidjnk quits (~acidjnk@p200300d6e7072f05045f4aa7d8e8f055.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 09:09:09 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 09:12:20 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:12:26 | × | mima quits (~mmh@aftr-62-216-211-216.dynamic.mnet-online.de) (Ping timeout: 260 seconds) |
| 09:12:55 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 09:16:49 | × | andrei_n quits (~andrei.n@2a02:a03f:c0bc:8400:2ce4:55ac:9234:c3d) (Quit: Leaving) |
| 09:18:11 | → | danse-nr3_ joins (~francesco@151.47.178.6) |
| 09:20:06 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 252 seconds) |
| 09:20:39 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:21:11 | × | danse-nr3 quits (~francesco@151.47.200.141) (Ping timeout: 260 seconds) |
| 09:24:19 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 09:24:19 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 09:24:19 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 09:25:44 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 09:26:19 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 09:26:49 | × | danse-nr3_ quits (~francesco@151.47.178.6) (Remote host closed the connection) |
| 09:27:11 | → | danse-nr3_ joins (~francesco@151.47.178.6) |
| 09:28:30 | × | jonathan quits (~jonathan@193.203.13.97) (Ping timeout: 256 seconds) |
| 09:28:36 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:29:38 | → | jonathan joins (~jonathan@193.203.13.91) |
| 09:30:58 | × | sm quits (~sm@plaintextaccounting/sm) (Quit: sm) |
| 09:33:03 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) |
| 09:34:20 | kaol_ | is now known as kaol |
| 09:35:45 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:f1a1:7919:4ffc:e710) (Quit: WeeChat 2.8) |
| 09:37:31 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) (Ping timeout: 246 seconds) |
| 09:42:17 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.0.2) |
| 09:43:30 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:43:42 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 09:43:44 | × | ft quits (~ft@p508db17b.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:48:13 | → | smalltalkman joins (uid545680@id-545680.hampstead.irccloud.com) |
| 09:51:28 | → | Pickchea joins (~private@user/pickchea) |
| 09:58:27 | → | fweht joins (uid404746@id-404746.lymington.irccloud.com) |
| 09:59:21 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 10:04:24 | × | mc47 quits (~mc47@xmonad/TheMC47) (Quit: Leaving) |
| 10:06:32 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 246 seconds) |
| 10:06:41 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 260 seconds) |
| 10:07:11 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 10:09:47 | → | sm joins (~sm@plaintextaccounting/sm) |
| 10:11:48 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 252 seconds) |
| 10:25:43 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 10:26:54 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 10:29:14 | → | acidjnk joins (~acidjnk@p200300d6e7072f05d52b79b26b7060d5.dip0.t-ipconnect.de) |
| 10:32:17 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 10:37:00 | → | andrei_n joins (~andrei.n@2a02:a03f:c0bc:8400:789e:e88f:e465:7978) |
| 10:43:26 | × | hdggxin quits (~hdggxin@122.175.41.19) (Ping timeout: 260 seconds) |
| 10:44:47 | → | hdggxin joins (~hdggxin@122.175.41.19) |
| 10:48:54 | × | danse-nr3_ quits (~francesco@151.47.178.6) (Ping timeout: 258 seconds) |
| 10:56:39 | barrucad1 | is now known as barrucadu |
| 10:58:11 | → | akegalj joins (~akegalj@36-180.dsl.iskon.hr) |
| 10:59:50 | × | CiaoSen quits (~Jura@2a05:5800:29f:f100:664b:f0ff:fe37:9ef) (Ping timeout: 244 seconds) |
| 11:01:20 | → | bitdex_ joins (~bitdex@gateway/tor-sasl/bitdex) |
| 11:02:09 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 246 seconds) |
| 11:05:49 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 11:07:40 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 11:07:58 | → | danse-nr3_ joins (~francesco@151.47.178.6) |
| 11:08:41 | × | hdggxin quits (~hdggxin@122.175.41.19) (Ping timeout: 250 seconds) |
| 11:08:43 | → | xff0x joins (~xff0x@2405:6580:b080:900:ac2a:af6b:2973:1b48) |
| 11:13:27 | → | hdggxin joins (~hdggxin@122.175.41.19) |
| 11:14:01 | → | thyriaen joins (~thyriaen@2a01:aea0:dd4:6c62:6245:cbff:fe9f:48b1) |
| 11:15:10 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 11:18:04 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 11:20:33 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 252 seconds) |
| 11:21:16 | × | nyc quits (~nyc@2603-7000-a106-2fb5-0000-0000-0000-1f21.res6.spectrum.com) (Ping timeout: 256 seconds) |
| 11:22:51 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 11:23:33 | × | Pickchea quits (~private@user/pickchea) (Ping timeout: 246 seconds) |
| 11:24:18 | → | lortabac joins (~lortabac@37.97.111.147) |
| 11:26:22 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 11:27:39 | × | sm quits (~sm@plaintextaccounting/sm) (Quit: sm) |
| 11:28:59 | → | kmein joins (~weechat@user/kmein) |
| 11:30:14 | → | mima joins (~mmh@dhcp-138-246-3-237.dynamic.eduroam.mwn.de) |
| 11:34:11 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 245 seconds) |
| 11:34:53 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) |
| 11:37:38 | → | CiaoSen joins (~Jura@2a05:5800:29f:f100:664b:f0ff:fe37:9ef) |
| 11:39:30 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:4c38:8910:beb8:9cb7) (Ping timeout: 258 seconds) |
| 11:43:08 | × | hdggxin quits (~hdggxin@122.175.41.19) (Ping timeout: 246 seconds) |
| 11:45:34 | → | hseg joins (~gesh@77.137.68.75) |
| 11:45:51 | × | danse-nr3_ quits (~francesco@151.47.178.6) (Ping timeout: 252 seconds) |
| 11:46:42 | <hseg> | Hi - stack isn't picking up the latest versions of packages, even when listed in extra-deps. eg have dep on tls-1.8.0, but stack complains it can't find it on hackage |
| 11:46:50 | <hseg> | anybody else have this? |
| 11:47:39 | <hseg> | also, just saw play.haskell.org has been added, it's appreciated! |
| 11:48:21 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 11:48:21 | × | bitdex_ quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 11:48:52 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 11:49:19 | → | bitdex_ joins (~bitdex@gateway/tor-sasl/bitdex) |
| 11:49:38 | → | ripspin joins (~chatzilla@1.145.132.147) |
| 11:49:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 11:53:10 | × | ripspin quits (~chatzilla@1.145.132.147) (Remote host closed the connection) |
| 11:58:02 | × | andrei_n quits (~andrei.n@2a02:a03f:c0bc:8400:789e:e88f:e465:7978) (Remote host closed the connection) |
| 11:58:20 | → | andrei_n joins (~andrei.n@2a02:a03f:c0bc:8400:789e:e88f:e465:7978) |
| 12:00:00 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 12:02:27 | → | danse-nr3_ joins (~francesco@151.47.178.6) |
| 12:03:35 | → | Square2 joins (~Square4@user/square) |
| 12:04:43 | × | andrei_n quits (~andrei.n@2a02:a03f:c0bc:8400:789e:e88f:e465:7978) (Quit: Leaving) |
| 12:09:22 | × | SegmentationFaul quits (~Segmentat@185.151.84.54) (Quit: Client closed) |
| 12:10:11 | → | notzmv joins (~zmv@user/notzmv) |
| 12:14:23 | stefan-__ | is now known as stefan-_ |
| 12:19:21 | × | acidjnk quits (~acidjnk@p200300d6e7072f05d52b79b26b7060d5.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 12:23:41 | × | td_ quits (~td@i5387090D.versanet.de) (Ping timeout: 245 seconds) |
| 12:25:36 | → | td_ joins (~td@i5387092B.versanet.de) |
| 12:35:37 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:4421:6684:8924:105c) |
| 12:38:07 | <hseg> | ping? anyone else notice stack not picking up latest versions of packages that exist in hackage? |
| 12:39:15 | → | hdggxin joins (~hdggxin@122.175.41.19) |
| 12:39:56 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:4421:6684:8924:105c) (Ping timeout: 245 seconds) |
| 12:47:16 | <danse-nr3_> | did not happen to me but it would be a rather fundamental issue. I would rather guess that your environment is affecting this |
| 12:47:33 | × | bitdex_ quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 12:48:35 | <hseg> | hrm. nuked the stack cache, seems to have solved it. _shrugs_ |
| 12:48:41 | → | bitdex_ joins (~bitdex@gateway/tor-sasl/bitdex) |
| 12:49:02 | <hseg> | and yeah, it was extremely surprising to me |
| 12:50:49 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:50:59 | <hseg> | for this precise reason |
| 12:54:33 | → | SegmentationFaul joins (~Segmentat@185.151.84.54) |
| 12:57:18 | × | akegalj quits (~akegalj@36-180.dsl.iskon.hr) (Quit: leaving) |
| 12:58:00 | <danse-nr3_> | strange |
| 12:58:24 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 12:58:43 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 12:59:15 | <danse-nr3_> | oh, i overlooked your original question |
| 12:59:18 | <danse-nr3_> | hseg, pong |
| 12:59:22 | <danse-nr3_> | sorry for the latency |
| 13:00:00 | <hseg> | :) |
| 13:00:34 | <hseg> | you answered my original question - negatively, prompting my nuke |
| 13:02:07 | → | acidjnk joins (~acidjnk@p200300d6e7072f05f88db541a99f62e2.dip0.t-ipconnect.de) |
| 13:09:27 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.0.2) |
| 13:12:51 | <danse-nr3_> | yeah but the ping was left unacked |
| 13:15:31 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 13:15:51 | × | ulysses4ever quits (~artem@c-73-103-90-145.hsd1.in.comcast.net) (Read error: Connection reset by peer) |
| 13:16:03 | → | ulysses4ever joins (~artem@c-73-103-90-145.hsd1.in.comcast.net) |
| 13:17:48 | → | sm joins (~sm@plaintextaccounting/sm) |
| 13:18:11 | → | danse-nr3__ joins (~francesco@151.47.130.197) |
| 13:18:46 | × | sm quits (~sm@plaintextaccounting/sm) (Client Quit) |
| 13:19:04 | → | nyc joins (~nyc@2603-7000-a106-2fb5-0000-0000-0000-1f21.res6.spectrum.com) |
| 13:20:01 | × | AlexZenon quits (~alzenon@178.34.150.48) (Ping timeout: 245 seconds) |
| 13:20:02 | × | AlexNoo quits (~AlexNoo@178.34.150.48) (Ping timeout: 246 seconds) |
| 13:20:26 | × | Alex_test quits (~al_test@178.34.150.48) (Ping timeout: 245 seconds) |
| 13:20:28 | × | hseg quits (~gesh@77.137.68.75) (Quit: WeeChat 4.0.4) |
| 13:21:00 | × | danse-nr3_ quits (~francesco@151.47.178.6) (Ping timeout: 252 seconds) |
| 13:23:54 | × | ulysses4ever quits (~artem@c-73-103-90-145.hsd1.in.comcast.net) (Read error: Connection reset by peer) |
| 13:24:28 | → | ulysses4ever joins (~artem@73.103.90.145) |
| 13:24:30 | × | thyriaen quits (~thyriaen@2a01:aea0:dd4:6c62:6245:cbff:fe9f:48b1) (Remote host closed the connection) |
| 13:26:39 | Hecate_ | is now known as Hecate |
| 13:29:17 | → | fendor joins (~fendor@2a02:8388:1640:be00:b586:6c06:a58:19a3) |
| 13:29:29 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 13:30:11 | → | gatekempt joins (~gatekempt@user/gatekempt) |
| 13:31:22 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 264 seconds) |
| 13:33:00 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 246 seconds) |
| 13:34:12 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 252 seconds) |
| 13:34:40 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 13:34:47 | × | hgolden_ quits (~hgolden@2603-8000-9d00-3ed1-fc05-5499-f77c-fbe5.res6.spectrum.com) (Remote host closed the connection) |
| 13:36:42 | × | CiaoSen quits (~Jura@2a05:5800:29f:f100:664b:f0ff:fe37:9ef) (Ping timeout: 246 seconds) |
| 13:40:34 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 13:43:00 | → | artem joins (~artem@2601:249:4380:8950:f474:e3f8:9806:671) |
| 13:43:02 | × | ulysses4ever quits (~artem@73.103.90.145) (Read error: Connection reset by peer) |
| 13:45:46 | → | ulysses4ever joins (~artem@c-73-103-90-145.hsd1.in.comcast.net) |
| 13:45:47 | × | artem quits (~artem@2601:249:4380:8950:f474:e3f8:9806:671) (Read error: Connection reset by peer) |
| 13:50:07 | → | ystael joins (~ystael@user/ystael) |
| 13:53:16 | → | artem joins (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) |
| 13:54:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:54:50 | × | ulysses4ever quits (~artem@c-73-103-90-145.hsd1.in.comcast.net) (Ping timeout: 256 seconds) |
| 13:54:52 | × | artem quits (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) (Read error: Connection reset by peer) |
| 13:55:49 | → | ulysses4ever joins (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) |
| 13:57:02 | → | artem joins (~artem@73.145.240.82) |
| 13:59:01 | × | artem quits (~artem@73.145.240.82) (Read error: Connection reset by peer) |
| 13:59:01 | × | ulysses4ever quits (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) (Read error: Connection reset by peer) |
| 13:59:43 | → | ulysses4ever joins (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) |
| 14:03:50 | × | ulysses4ever quits (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) (Ping timeout: 246 seconds) |
| 14:04:31 | → | ulysses4ever joins (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) |
| 14:04:53 | → | AlexNoo joins (~AlexNoo@178.34.150.48) |
| 14:05:38 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 14:06:14 | → | Alex_test joins (~al_test@178.34.150.48) |
| 14:13:29 | × | SegmentationFaul quits (~Segmentat@185.151.84.54) (Quit: Ping timeout (120 seconds)) |
| 14:14:05 | → | Simikando joins (~Simikando@adsl-dyn1.91-127-51.t-com.sk) |
| 14:14:10 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 14:14:44 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 14:15:30 | × | lortabac quits (~lortabac@37.97.111.147) (Ping timeout: 245 seconds) |
| 14:16:01 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 14:17:23 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 14:19:19 | → | Pickchea joins (~private@user/pickchea) |
| 14:19:51 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 252 seconds) |
| 14:22:44 | → | thegeekinside joins (~thegeekin@189.180.79.225) |
| 14:31:20 | → | nyr joins (~nyr@user/nyr) |
| 14:35:21 | × | briandaed quits (~briandaed@185.234.210.211) (Remote host closed the connection) |
| 14:37:09 | → | lortabac joins (~lortabac@37.97.111.147) |
| 14:39:32 | × | ulysses4ever quits (~artem@2601:408:c405:16e8:f474:e3f8:9806:671) (Ping timeout: 246 seconds) |
| 14:39:33 | × | Simikando quits (~Simikando@adsl-dyn1.91-127-51.t-com.sk) (Quit: Leaving) |
| 14:43:20 | → | ulysses4ever joins (~artem@73.145.240.82) |
| 14:43:34 | → | shapr joins (~user@2600:1700:c640:3100:a991:ffa8:c9bc:d5d1) |
| 14:43:44 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 14:43:59 | → | SegmentationFaul joins (~Segmentat@185.151.84.54) |
| 14:45:07 | × | lortabac quits (~lortabac@37.97.111.147) (Quit: WeeChat 2.8) |
| 14:45:24 | × | ulysses4ever quits (~artem@73.145.240.82) (Read error: Connection reset by peer) |
| 14:47:18 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 14:48:30 | → | AlexZenon joins (~alzenon@178.34.150.48) |
| 14:48:58 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 14:49:57 | × | mc47 quits (~mc47@xmonad/TheMC47) (Quit: Leaving) |
| 14:51:33 | → | ulysses4ever joins (~artem@2601:40d:509:64:f474:e3f8:9806:671) |
| 14:53:19 | → | abrantesasf joins (~abrantesa@177.137.232.92) |
| 14:53:28 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 258 seconds) |
| 14:53:31 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 14:56:02 | × | ulysses4ever quits (~artem@2601:40d:509:64:f474:e3f8:9806:671) (Ping timeout: 256 seconds) |
| 14:56:09 | × | g quits (g@libera/staff-emeritus/glguy) (Remote host closed the connection) |
| 14:56:17 | → | g joins (g@libera/staff-emeritus/glguy) |
| 14:56:43 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 14:58:16 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 14:58:16 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 14:58:16 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 14:59:28 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 15:00:37 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.0.3) |
| 15:03:33 | → | powderhorn joins (~powderhor@207-153-12-54.static.fttp.usinternet.com) |
| 15:05:18 | → | ripspin joins (~chatzilla@1.145.177.195) |
| 15:06:38 | → | ulysses4ever joins (~artem@hilton-nomadix.wintek.com) |
| 15:08:20 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 15:08:28 | × | nyr quits (~nyr@user/nyr) (Ping timeout: 248 seconds) |
| 15:08:37 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:4421:6684:8924:105c) |
| 15:10:43 | × | ulysses4ever quits (~artem@hilton-nomadix.wintek.com) (Ping timeout: 246 seconds) |
| 15:11:03 | → | ulysses4ever joins (~artem@2601:408:c405:4964:f474:e3f8:9806:671) |
| 15:13:29 | × | ulysses4ever quits (~artem@2601:408:c405:4964:f474:e3f8:9806:671) (Read error: Connection reset by peer) |
| 15:13:33 | → | artem joins (~artem@2601:408:c405:4964:f474:e3f8:9806:671) |
| 15:15:23 | <exarkun> | I tried to use module "thinning" (https://ghc.gitlab.haskell.org/ghc/doc/users_guide/packages.html#thinning-and-renaming-modules) by adding `{-# OPTIONS_GHC -package "base64-bytestring (Data.ByteString.Base64)" #-}` to one of my source files but `cabal build` gives me `unknown flag in {-# OPTIONS_GHC #-} pragma: -package`. How should I do this? |
| 15:19:48 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 15:24:45 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
| 15:25:24 | × | artem quits (~artem@2601:408:c405:4964:f474:e3f8:9806:671) (Ping timeout: 244 seconds) |
| 15:28:23 | × | SegmentationFaul quits (~Segmentat@185.151.84.54) (Ping timeout: 246 seconds) |
| 15:28:45 | → | jabuxas joins (~jabuxas@user/jabuxas) |
| 15:29:16 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 260 seconds) |
| 15:29:54 | → | mechap joins (~mechap@user/mechap) |
| 15:35:47 | <danse-nr3__> | i searched a bit but i did not find any documentation that would hint to that syntax being wrong. I guess most thinning users choose command line flags |
| 15:36:51 | <fendor> | I might be wrong, but maybe OPTIONS_GHC is only allowed for interactive flags? `-package` is not an interactive flag, e.g. you can't specify it in ghci |
| 15:37:08 | ← | Minnozz parts (~minnozz@salix.minnozz.com) (WeeChat 3.8) |
| 15:37:14 | <fendor> | * in a ghci session to load another package |
| 15:39:37 | <exarkun> | hm. https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using.html#source-file-options says that only "Dynamic" flags can be used with OPTIONS_GHC (although I am not sure if the intent here is that _all_ "Dynamic" flags can be used with it) |
| 15:39:53 | → | ulysses4ever joins (~artem@2607:fb91:174a:9d2c:92a6:7fd7:d49d:f507) |
| 15:39:56 | <exarkun> | https://ghc.gitlab.haskell.org/ghc/doc/users_guide/flags.html#flag-reference does say that "-package" is "Dynamic" |
| 15:40:26 | <exarkun> | I can use the `PackageImports` language extension instead... but docs told me it's fragile and I should prefer thinning. |
| 15:41:04 | → | Simikando joins (~Simikando@adsl-dyn1.91-127-51.t-com.sk) |
| 15:44:49 | × | abrantesasf quits (~abrantesa@177.137.232.92) (Remote host closed the connection) |
| 15:47:37 | → | dhil joins (~dhil@78.45.150.83.ewm.ftth.as8758.net) |
| 15:48:13 | × | Simikando quits (~Simikando@adsl-dyn1.91-127-51.t-com.sk) (Quit: Leaving) |
| 15:48:26 | <c_wraith> | exarkun: if you're using cabal, use mixins |
| 15:48:26 | × | ulysses4ever quits (~artem@2607:fb91:174a:9d2c:92a6:7fd7:d49d:f507) (Read error: Connection reset by peer) |
| 15:48:36 | → | ulysses4ever joins (~artem@192.31.0.5) |
| 15:48:48 | × | gehmehgeh quits (~user@user/gehmehgeh) (Ping timeout: 246 seconds) |
| 15:49:04 | <c_wraith> | exarkun: https://cabal.readthedocs.io/en/stable/cabal-package.html#pkg-field-mixins |
| 15:49:55 | × | acidjnk quits (~acidjnk@p200300d6e7072f05f88db541a99f62e2.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 15:50:06 | × | jabuxas quits (~jabuxas@user/jabuxas) (Quit: Leaving.) |
| 15:50:54 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 15:51:07 | × | thegeekinside quits (~thegeekin@189.180.79.225) (Remote host closed the connection) |
| 15:51:18 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 15:53:46 | <exarkun> | c_wraith: Okay, didn't know about those. It looks like they aren't per-module though? |
| 15:54:06 | <c_wraith> | they aren't. but on the plus side, they work. :) |
| 15:54:49 | <exarkun> | in my specific case, I need to specify per-module, so I guess PackageImports for now |
| 15:55:15 | <exarkun> | thanks for the pointer about mixins |
| 15:57:26 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 15:59:26 | <justsomeguy> | Is it possible to write a test that proves whether something is a data constructor or type constructor? I'm trying to unit test my homework. When I try to evaluate the type constructor "Doggies" I get the following exception "Illegal term-level use of the type constructor ‘Doggies’". So maybe I can use hspec's `shouldThrow`? |
| 16:00:34 | <justsomeguy> | Until now, I've been writing expect scripts that run GHCi interactively and do string matching for my tests, but I thought it would be nicer to write hspec unit tests, instead. |
| 16:01:05 | <geekosaur> | "throw" is runtime, you are getting a compile time error |
| 16:01:18 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 16:01:34 | <c_wraith> | I don't see much value in testing something that just won't compile if code is using it incorrectly |
| 16:02:21 | <c_wraith> | It's like writing a test that integers aren't functions. |
| 16:02:55 | <EvanR> | tests test your running program. Or are you testing GHC itself |
| 16:04:24 | <justsomeguy> | I have a list of questions like "what is the type of x", "what is the kind of x". They're really reading comprehension questions about Haskell syntax. But I've been forcing myself to write test for everything so far in the hopes I can use it as a checklist so when I forget where I left off in the project I can just run all of the tests to find out. |
| 16:04:52 | <justsomeguy> | Maybe I should keep a literal checklist instead. |
| 16:05:12 | <EvanR> | what is the _ of x, type or kind xD |
| 16:06:29 | <EvanR> | term, type, or kind |
| 16:06:32 | <EvanR> | or sort |
| 16:06:40 | <justsomeguy> | I'm just overcomplicating things. It sucks to re-start a big book an lose your place :D. |
| 16:08:53 | <[Leary]> | You can write `x :: <type>` then `type t :: <kind>`, etc rather than tests? If it compiles, the "tests" pass without needing to do anything at runtime. |
| 16:09:30 | <c_wraith> | You can only write positive tests like that... trivially, anyway. |
| 16:10:09 | <c_wraith> | There is a package that lets you write negative tests for that sort of thing if you use -fdefer-type-errors, but it only works for type errors |
| 16:11:02 | <justsomeguy> | I hadn't thought of that [Leary]. That makes sense for some of these questions. |
| 16:11:36 | <danse-nr3__> | are you studying out of a book? |
| 16:12:27 | <justsomeguy> | Yes, I'm studying from Haskell Programming from First Principles. You can see my notes here: hpfp.readthedocs.io. I've been working on it off-and-on for a few years now. |
| 16:12:43 | <justsomeguy> | (And keep on getting stuck.) |
| 16:14:35 | <danse-nr3__> | nice that you are publishing your notes |
| 16:15:01 | <justsomeguy> | It helps me out. Easier to ask questions this way. |
| 16:17:38 | <justsomeguy> | For something like this I have a text-based question and answer https://github.com/kingparra/hpfp/blob/cd44ae4ad68800375168b6b5966599d81be0ae6f/11_-_algebraic_datatypes/exercises/11.5.1_-_dog_types.rst and an expect script that I've been using in lui of actual tests |
| 16:17:40 | <justsomeguy> | https://github.com/kingparra/hpfp/blob/cd44ae4ad68800375168b6b5966599d81be0ae6f/11_-_algebraic_datatypes/exercises/11.5.1_-_dog_types.rst.d/dogtypes.expect ... |
| 16:18:13 | <danse-nr3__> | oh i recall when that book came out. Christopher Allen attacked me on twitter because he did not like my comment |
| 16:19:21 | <erisco> | justsomeguy, I just have a file that I keep appending to as I encounter exercises, so I've left off at the bottom |
| 16:20:16 | <justsomeguy> | erisco: How do you know if you got one wrong? |
| 16:20:52 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 258 seconds) |
| 16:21:04 | <erisco> | the compiler will tell me, if it can be determined by static analysis |
| 16:21:09 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 16:22:25 | <erisco> | otherwise, I'm not that worried about it for small problems, I just run a few inputs by hand |
| 16:24:13 | <erisco> | if there are dark areas of my solution, I need to retry the problem, and I need to keep doing that until my internal, informal static analyser is convinced... then I run a few inputs by hand to doublecheck I am not kidding myself |
| 16:24:22 | <exarkun> | Your unit tests are a program you run to tell you about some behavior of your program (runtime behavior - since they're a thing you run) |
| 16:24:56 | <exarkun> | The compiler is a program you run to tell you things about some possible source code you have (it's runtime for the compiler! but that's a special time we call compile time). |
| 16:25:09 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 16:25:14 | <exarkun> | Among the things the compiler can tell you are ... is this Haskell (as the compiler understands it) source code or not |
| 16:25:23 | <exarkun> | (and if not, often some details about why it thinks so) |
| 16:25:35 | <erisco> | which is a practice that would make a TDD enjoyer's hair stand on end :P |
| 16:26:12 | <exarkun> | A sufficiently enlightened TDDer can accept that the compiler might have valuable input to supply :) |
| 16:26:43 | <exarkun> | I think it's really the very dynamic language mindset which has trouble with the idea that some properties of a program might not be its _runtime_ properties. |
| 16:27:02 | <c_wraith> | you could theoretically accept that "compiles" is an implicit test on its own. |
| 16:27:02 | <exarkun> | (so you have Python programs that include unit tests for what happens if you call a 2 argument function with 3 arguments, etc) |
| 16:27:06 | <erisco> | a TDDer is concerned about the behavioural ie extrinsic properties of a program, whereas a static analyser is concerned about the intentional ie intrinsic properties of a program |
| 16:27:48 | <EvanR> | all programs compile and run. HTML had it right |
| 16:27:58 | <EvanR> | get straight to the debugging |
| 16:28:24 | <erisco> | a TDDer is satisfied if a black box passes all tests... another approach, and I do not have a name for it, is to build understanding and correctness compositionally, so you know you have the right result at every step of construction |
| 16:28:26 | <EvanR> | all text files I mean, are programs |
| 16:28:39 | <exarkun> | erisco: Well, I speak as a reformed dynamic language TDDer, so I think there's at least some variability in the group :) |
| 16:29:02 | <justsomeguy> | erisco: Well, a single big file makes remembering where you left off simpler, for sure. I'm about ready to ditch my old efforts and try a straight run-through of the book in one go. Maybe I'll go with a few big files. |
| 16:29:40 | <exarkun> | If you programming language has no intentional properties (programs don't mean anything, they just do stuff) then it's pretty reasonable to largely ignore intentions. |
| 16:30:10 | <exarkun> | But we can still write useful tests for Haskell code, and we can even do so TDD if we want. |
| 16:31:13 | <danse-nr3__> | of course, test-driven dev has little to do with compiling distinctions |
| 16:31:56 | <erisco> | When all tests pass, and assuming the tests cover all practical cases, that's great. I think the difference reveals itself when tests are not passing and now someone has to do something about it. As programmers, we're pretty interested in intention :) |
| 16:32:44 | × | fendor quits (~fendor@2a02:8388:1640:be00:b586:6c06:a58:19a3) (Remote host closed the connection) |
| 16:33:33 | <erisco> | if you've ever had to modify a test so the program passed, because it is too hard to fix the reason it fails this year, then you know what I mean :P |
| 16:38:03 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 16:38:11 | × | ddellacosta quits (~ddellacos@146.70.166.100) (Ping timeout: 246 seconds) |
| 16:38:35 | → | ddellacosta joins (~ddellacos@146.70.166.100) |
| 16:40:16 | <EvanR> | program to compute pi is failing the test, just change the test |
| 16:42:45 | → | thegeekinside joins (~thegeekin@189.180.79.225) |
| 16:43:27 | × | p3n quits (~p3n@217.198.124.246) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:44:58 | × | ddellacosta quits (~ddellacos@146.70.166.100) (Ping timeout: 244 seconds) |
| 16:45:41 | × | ripspin quits (~chatzilla@1.145.177.195) (Remote host closed the connection) |
| 16:46:55 | → | ddellacosta joins (~ddellacos@146.70.185.100) |
| 16:47:08 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 4.0.3) |
| 16:47:19 | <erisco> | we explained the future risk for interfacing with other systems, but the business decided that we'll just explain to external stakeholders that, in the way we like to do things, pi = 22/7 |
| 16:47:38 | × | danse-nr3__ quits (~francesco@151.47.130.197) (Ping timeout: 246 seconds) |
| 16:48:45 | <geekosaur> | https://en.wikipedia.org/wiki/Indiana_Pi_Bill |
| 16:51:13 | → | danza joins (~francesco@151.47.130.197) |
| 16:52:36 | <erisco> | now that's a rich piece of history |
| 16:53:03 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 246 seconds) |
| 16:57:15 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 16:58:06 | <shapr> | @quote haskell |
| 16:58:06 | <lambdabot> | haskell says: Haskell binaries are made of 100% win. That is why they are so big. |
| 17:00:37 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:fc05:5499:f77c:fbe5) |
| 17:01:50 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 256 seconds) |
| 17:03:50 | <carter> | thats a good one` |
| 17:06:07 | → | hugo- joins (znc@130.236.254.23) |
| 17:07:02 | × | perrierjouet quits (~perrierjo@modemcable048.127-56-74.mc.videotron.ca) (Quit: WeeChat 4.0.3) |
| 17:07:11 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:07:58 | → | jabuxas joins (~jabuxas@user/jabuxas) |
| 17:13:02 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 17:16:00 | × | Square2 quits (~Square4@user/square) (Ping timeout: 256 seconds) |
| 17:17:30 | × | ddellacosta quits (~ddellacos@146.70.185.100) (Ping timeout: 252 seconds) |
| 17:18:02 | → | danza_ joins (~francesco@151.46.217.116) |
| 17:20:32 | × | danza quits (~francesco@151.47.130.197) (Ping timeout: 256 seconds) |
| 17:21:22 | → | ddellacosta joins (~ddellacos@146.70.168.100) |
| 17:21:28 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 17:22:17 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 17:23:41 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Read error: Connection reset by peer) |
| 17:25:57 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 17:26:51 | × | danza_ quits (~francesco@151.46.217.116) (Ping timeout: 252 seconds) |
| 17:27:03 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 17:27:45 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 17:31:28 | <EvanR> | and from then on geometry was added to US schools |
| 17:31:33 | × | g quits (g@libera/staff-emeritus/glguy) (Remote host closed the connection) |
| 17:31:40 | → | g joins (g@libera/staff-emeritus/glguy) |
| 17:32:08 | <EvanR> | reading, writing, and arithmetic only gets you so far |
| 17:35:42 | → | Inst joins (~liamzy@2601:6c4:4085:6d50::725c) |
| 17:37:07 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:37:41 | × | logothesia quits (~logothesi@user/logothesia) (Ping timeout: 246 seconds) |
| 17:38:46 | × | jabuxas quits (~jabuxas@user/jabuxas) (Quit: Leaving.) |
| 17:39:41 | → | acidjnk joins (~acidjnk@p200300d6e7072f05a8abaa2c9ff73443.dip0.t-ipconnect.de) |
| 17:40:06 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 246 seconds) |
| 17:48:42 | → | artem joins (~artem@192.31.0.5) |
| 17:48:44 | × | ulysses4ever quits (~artem@192.31.0.5) (Read error: Connection reset by peer) |
| 17:49:34 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 17:49:53 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 17:50:21 | → | ulysses4ever joins (~artem@192.31.0.5) |
| 17:53:00 | × | artem quits (~artem@192.31.0.5) (Ping timeout: 245 seconds) |
| 17:53:49 | → | EvanR_ joins (~EvanR@user/evanr) |
| 17:54:33 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:55:40 | → | shapr` joins (~user@2600:1700:c640:3100:a991:ffa8:c9bc:d5d1) |
| 17:55:53 | × | shapr quits (~user@2600:1700:c640:3100:a991:ffa8:c9bc:d5d1) (Ping timeout: 246 seconds) |
| 17:55:55 | × | EvanR quits (~EvanR@user/evanr) (Ping timeout: 245 seconds) |
| 17:59:56 | × | Inst quits (~liamzy@2601:6c4:4085:6d50::725c) (Ping timeout: 245 seconds) |
| 18:01:19 | × | myxos quits (~myxos@cpe-65-28-251-121.cinci.res.rr.com) (Quit: myxos) |
| 18:04:33 | <erisco> | EvanR_, I was rather disappointed by geometry. Forget the geometry, Euclid's work was groundbreaking for mathematical foundations. I think I spent all my time in school wondering where the hell this math stuff came from |
| 18:05:25 | EvanR_ | is now known as EvanR |
| 18:05:34 | <EvanR> | euclid is great |
| 18:06:19 | <dolio> | Geometry is the algebra of rationals + square roots, right? :þ |
| 18:07:32 | <erisco> | I thought geometry was about actually using the little lines on your straight edge, and then having a debate about whether that was real math or not |
| 18:08:13 | × | fweht quits (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 18:09:15 | × | mima quits (~mmh@dhcp-138-246-3-237.dynamic.eduroam.mwn.de) (Ping timeout: 245 seconds) |
| 18:09:24 | → | Volt_ joins (~Volt_@c-73-47-181-152.hsd1.ma.comcast.net) |
| 18:09:35 | <erisco> | incidentally, if someone could explain limits to me without showing me pictures of secants turning into tangents, or showing me a lim x -> 0 and then throwing a bunch of identities at me, would appreciate it |
| 18:09:44 | → | deviance joins (~deviance@bcdcac82.skybroadband.com) |
| 18:09:48 | → | artem joins (~artem@192.31.0.5) |
| 18:10:06 | <shapr`> | erisco: have you looked at infinitesimals? |
| 18:10:07 | <dolio> | Explain what about them? |
| 18:10:13 | shapr` | is now known as shapr |
| 18:12:00 | <erisco> | shapr`, years ago, though I didn't look at them for too long. Worth it? I have just never got much into numbers because working with them feels like working with poorly documented code and searching SO for the answers |
| 18:12:35 | × | ulysses4ever quits (~artem@192.31.0.5) (Ping timeout: 245 seconds) |
| 18:12:36 | <erisco> | z, s z, s (s z), and I'm following, but we get into limits and I lose the plot |
| 18:12:57 | <dolio> | I think the nice thing about infinitessimals is that you can do calculus-like stuff without talking about limits at all. |
| 18:13:02 | <shapr> | Infinitesimals were what calculus used before it got limits |
| 18:13:22 | <shapr> | Yeah, what dolio said |
| 18:13:26 | <dolio> | And if you go the SDG route, it forces you to use intuitionistic logic, which is morally correct. |
| 18:13:33 | <erisco> | I was taught limits as here's the notation, here's a bunch of rules for what the limit of this over that is |
| 18:13:58 | <shapr> | erisco: also, the "losing the plot" phrase was good after talking about pictures of secants |
| 18:14:11 | <ncf> | were you taught a definition? that's the most important thing |
| 18:14:13 | <exarkun> | erisco: https://www.maa.org/sites/default/files/pdf/devlin/LockhartsLament.pdf (thanks shapr ) |
| 18:14:29 | <shapr> | exarkun: I love that document :-) |
| 18:14:54 | <shapr> | I'm giving a surprise talk on Friday noon Pacific time on a different research paper |
| 18:15:29 | <shapr> | erisco: infinitesimals are specifically "calculus without limits" and I didn't realize how punny that might sound until I wrote it :-| |
| 18:16:11 | <erisco> | the tragedy is that, now that we have generations of human calculators, when schools try to teach mathematics from a "lets think and understand" foundation, parents are outraged |
| 18:16:31 | <shapr> | dolio: what's the SDG route? |
| 18:16:45 | <shapr> | what does SDG stand for? |
| 18:16:55 | <dolio> | Synthetic Differential Geometry, instead of non-standard analysis. |
| 18:17:02 | <shapr> | oh, thank you! |
| 18:17:20 | → | ski joins (~ski@83.248.72.178) |
| 18:17:29 | <shapr> | exarkun: did you make it to my talk on Lockhart's Lament? |
| 18:17:36 | <exarkun> | shapr: I don't think so |
| 18:18:18 | <shapr> | It was fun. I talked about reading that document in a waiting room, getting inspired and finding an exciting math problem in my pocket. |
| 18:18:38 | <shapr> | Specifically, I'd purchased ako dice where the faces look like https://cofree.coffee/~shapr/ako-dice.jpg |
| 18:18:40 | <erisco> | anyways, if anyone has resources to explain limits / reals to the constructivist-minded, would appreciate |
| 18:21:33 | <ddellacosta> | interesting, I thought that the reason limits are used vs. infinitesmals is because the latter isn't sufficiently formalized, but apparently that was done in the 20th century |
| 18:21:58 | <shapr> | I thought that too |
| 18:22:14 | <EvanR> | erisco, you defined integers. You can define the limit of a sequence, or whatever flavor of limit |
| 18:22:17 | <ski> | shapr : oh, you talked on his paper ? or the book ? |
| 18:22:19 | <EvanR> | just definitions |
| 18:22:28 | <shapr> | ski: I gave a talk about Lockhart's Lament, yes |
| 18:22:45 | <shapr> | ski: I'm doing random talks about once every two weeks, want me to invite you? |
| 18:23:14 | <dolio> | erisco: Limits essentially come from the usual 'real numbers' actually being objects that let you query for approximations to some precision. Two methods of approximation give the same real number if they are close enough at every approximation precision. |
| 18:24:05 | <erisco> | sounds very computational of you |
| 18:24:17 | <EvanR> | a limit of a sequence of rationals can be defined without mentioning reals, so starting with "I don't get reals" is jumping the gun. In the traditional ordering of things |
| 18:24:49 | <erisco> | EvanR, and you'd define this limit axiomatically? with quantifiers? |
| 18:24:53 | <dolio> | So, given an appropriate sequence or set of such approximation objects, you can fold them into a single approximation that is the object the whole set was approximating. |
| 18:25:17 | <EvanR> | a definition and an axiom are two different things |
| 18:25:27 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 18:25:42 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 252 seconds) |
| 18:25:46 | <EvanR> | x = 3 is a definition, there exists a square root of two is an axiom |
| 18:25:56 | <mauke> | from what I recall from uni, one of the axioms of the real numbers was that every strictly increasing sequence of real numbers that is bounded above has a least upper bound, which is also a real number |
| 18:27:07 | <ski> | erisco : hmm .. well, i'm reminded of "Constructive Analysis" by Errett Bishop & Douglas Bridges. also Martin Escardo has some interesting papers regarding convergent sequences (and the "generic convergent sequence" (the "one-point compactification of the natural numbers"), classically being the natural numbers with an additional infinity point. think `data Nat = Zero | Succ Nat' including `inf = Succ inf') |
| 18:27:07 | <EvanR> | erisco, in the classic course, you "construct the reals with limits" and then you can prove that it corresponds to the axiomatic reals |
| 18:27:12 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 18:27:13 | <ski> | .. but i think possibly his papers wouldn't be a good intro |
| 18:27:22 | <EvanR> | it requires classical logic |
| 18:27:39 | <EvanR> | but see the section of constructive reals in homotopy type theory |
| 18:28:16 | <erisco> | repeating theme here is sequences, so I'll think more about sequences, thanks |
| 18:28:31 | <EvanR> | sequences are great, you can use haskell to generate them! |
| 18:28:54 | <EvanR> | make a list of rationals whose limit is the square root of two |
| 18:30:59 | <erisco> | off hand, I am not quite sure how you translate from lim h -> 0 (f (x + h) - f x) / h = f' x to a sequence |
| 18:31:23 | <EvanR> | that's a different kind of limit |
| 18:31:26 | <EvanR> | different definition |
| 18:31:48 | <erisco> | there is more than one kind of limit? |
| 18:31:51 | <EvanR> | yes |
| 18:31:55 | <ncf> | they're all similar |
| 18:31:59 | <erisco> | where were you in grade 11 |
| 18:32:26 | <EvanR> | that's what university is for, high school damage control |
| 18:32:39 | <ncf> | you could interpret that to mean "the limit of the sequence of approximations ((f(x + 1/n) - f x)/(1/n)) for n : ℕ" |
| 18:32:45 | <erisco> | where were you in calc I or II |
| 18:33:00 | <erisco> | all I was doing then is learning trig identities lol |
| 18:33:40 | <ski> | ddellacosta : hm, are you aware of Anders Kock's "Synthetic Differential Geometry" (book, 2nd ed.) in 2006 at <http://home.imf.au.dk/kock/sdg99.pdf> ? it formalizes some "naïve" reasoning with infinitesimals, crucially reasoning in an intuitionistic logic. .. also i'm reminded of Paul Taylor's "Abstract Stone Duality" <https://paultaylor.eu/ASD/>, which is a project to make a computable lambda-calculus for |
| 18:33:42 | → | bratwurst joins (~blaadsfa@S010610561191f5d6.lb.shawcable.net) |
| 18:33:46 | <ski> | dedekind cuts |
| 18:33:50 | <erisco> | ncf, there's an idea, thanks |
| 18:35:09 | <EvanR> | yeah, that gets you the same result as the definition. Which involves allowing you to approach 0 (from above in this case) however you want |
| 18:36:27 | <EvanR> | badly behaved expressions could converge to different things depending on the sequence taken, i.e. don't converge |
| 18:37:17 | <EvanR> | like when you get stock predictions that cherry pick their historical samples! |
| 18:37:25 | <erisco> | That's the trouble with axiomatic descriptions though isn't it. Doesn't tell you what, if anything, actually satisfies |
| 18:37:54 | <EvanR> | axiomatic? or do you mean the choice of sequence |
| 18:38:25 | <erisco> | I am imagining you are going to give an axiomatic meaning (what I was calling "definition") to limits on sequences |
| 18:38:54 | <EvanR> | go look at the definition of limit of a sequence (of rationals or whatever elements of a metric space) |
| 18:39:02 | <EvanR> | it's not an axiom |
| 18:39:08 | <erisco> | then you're left with trying to prove for a particular sequence what the limit is |
| 18:39:15 | <EvanR> | what it means it up to you, that's semantics |
| 18:39:30 | <dolio> | One of the definitions of reals (based on sets) would more naturally incorporate the ->0 example. |
| 18:39:53 | <EvanR> | you prove things by among other things abbreviating things with defintions |
| 18:40:05 | <dolio> | Because it would involve whole sets of reals getting close to 0, rather than a sequence. |
| 18:40:40 | <EvanR> | yeah there are multiple ways to define real numbers |
| 18:40:49 | <erisco> | EvanR, wikipedia is saying "x is the limit of the sequence s iff forall ..." |
| 18:40:56 | <erisco> | if this is not axiomatic I don't know what is |
| 18:41:30 | <dolio> | However, if you dig into the details, there is additional information required about the sets that is analogous to particular sequences. |
| 18:41:31 | <mauke> | a definition? |
| 18:41:33 | <EvanR> | take everything on the right side of iff, and any time you have that, you can call that information "a limit" |
| 18:41:44 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 244 seconds) |
| 18:41:58 | <EvanR> | it's like defining a function in haskell, so you can reuse the code without repeating it |
| 18:42:13 | <EvanR> | axioms are like new laws of logic that give you things out of the blue |
| 18:43:10 | <EvanR> | or like defining an ADT |
| 18:43:26 | <erisco> | okay, I just don't see the terminology the same way, but that's besides the point |
| 18:44:44 | <ncf> | definitions are not axioms; axioms are precisely statements without definitions (under the proofs-as-programs paradigm) |
| 18:46:28 | <ski> | ddellacosta : perhaps "" by Andrej Bauer in 2008-08-13 at <https://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/> and "The Arithmetic Hierarchy" by XOR's Hammer in 2016-05-14 at <https://xorshammer.com/2016/05/14/the-arithmetic-hierarchy-meets-the-real-world/> could be interesting |
| 18:46:39 | <EvanR> | as an example, I defined integers as either Z or, given any integer n, S n. Ok. And then I can add an axiom: there exists an infinite integer. But don't tell you how to get it |
| 18:46:51 | <ski> | ("Practical Foundations of Mathematics" by Paul Taylor in 1999 at <https://paultaylor.eu/~pt/prafm/> is also an interesting book ..) |
| 18:47:32 | <ski> | shapr : where did you give the talk ? is there any recording ? |
| 18:47:44 | <erisco> | when I say "definition" I just mean the expression of the meaning for a particular term, so the definition of "limit" is whatever expresses the meaning of the term "limit" |
| 18:48:16 | <EvanR> | well, that's annoying because limits are defined as something. Not what you're saying, the deep meaning or anything |
| 18:48:27 | <erisco> | if that expression is a quantified logical proposition, a statement about what must hold for an object to be considered a limit, I am going to say that is an axiomatic definition for limits |
| 18:48:47 | <ncf> | mathematicians like to give words meaning using "iff" |
| 18:48:48 | <erisco> | and if someone hates my use of terminology, I don't apologise :P |
| 18:48:58 | <EvanR> | it helps to be on the same page |
| 18:49:03 | <ncf> | you should interpret that iff as an equal sign, and then interpret that equal sign as a := |
| 18:49:15 | <EvanR> | redefining terminology, of definition no doubt, isn't helping anyone |
| 18:49:19 | <EvanR> | noless |
| 18:49:21 | <dolio> | Well, sometimes it's not the definition, too. :) |
| 18:49:53 | <EvanR> | but as long as we get to the same destination, redefine things as you will |
| 18:52:16 | <EvanR> | the definition of limit of a sequence (of things with metric space powers) is a definition is the same sense as haskell when you use let. The RHS of the = can be substituted wherever the short name is used elsewhere |
| 18:52:29 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 248 seconds) |
| 18:52:36 | <EvanR> | or vice versa |
| 18:52:56 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 18:53:10 | <ski> | EvanR : another view of axioms are that they are interfaces. starting from group axioms, you can prove things. then, if anyone can instantiate the group axioms with a constructed model (aka a group), then the proved things holds for it |
| 18:53:22 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 18:54:09 | <EvanR> | oh yeah, that is how they present the axiomatic reals. Here is the interface. Watch as we construct an example implementation |
| 18:55:45 | <EvanR> | something they struggle to do with axiomatic quantum field theory, according to nlab |
| 18:55:47 | <ski> | ncf : "mathematicians like to give words meaning using \"iff\"" .. unfortunately, they also like writing "if" in definitions, when they mean "if and only if". (this can be seen as an inductive definition (or a definition of a predicate in Prolog) .. anything that can *not* be derived about the concept, using the "if" statement, is assumed to not hold (least model)) |
| 18:56:20 | ski | 's not fond of using `:=', really .. |
| 18:57:16 | <erisco> | ski, yes, that is basically the translation between how I prefer to think about it... I'd be saying "assume l is a limit" and proceeding. Would then "assume l is a limit" be the axiom, otherwise speaking? |
| 18:58:21 | <EvanR> | you're trying to make it more mysterious than it is, you can always unpack the definition of l-is-the-limit-of-s |
| 18:58:47 | <erisco> | nah I think "axiom" is made more mysterious than it is :P |
| 18:58:53 | <EvanR> | where the interface version would be opaque at best |
| 18:59:03 | <EvanR> | you can only access what's in the interface |
| 19:01:22 | × | vglfr quits (~vglfr@cli-188-239-201-89.bbn.slav.dn.ua) (Read error: Connection reset by peer) |
| 19:02:18 | → | vglfr joins (~vglfr@cli-188-239-201-89.bbn.slav.dn.ua) |
| 19:04:02 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-212.fiber.dynamic.sonic.net) (Quit: segfaultfizzbuzz) |
| 19:05:31 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 19:06:33 | <erisco> | so anyways, you've got some condition, you have to prove it holds, and that raises the question of how you do that |
| 19:07:14 | <erisco> | so feels to me like you've punted the problem to one of proof methods... now how do you prove something is the limit of a sequence? then you get taught all these strategies based on how the sequence is defined |
| 19:07:17 | <ski> | there's more or less two different senses of "axiom". the original is "self-evident truth". related is "postulate" which is regarded as not as self-evident, but still needed as a basic building block to reason. the model here is "Elementa" by Euclid. then there's the more modern view of "axiom" in which you start to develop a theory (not historically, but in how you conceptually present it) by starting from |
| 19:07:23 | <ski> | a number of "undefined symbols" (like constants, functions, relations), and a number of "unproved propositions", the "axioms" (basic statements involving the undefined symbols, relating them to each other. ideally, there would be exactly one interpretation/model of the symbols which make the axioms true. but commonly there's more than one, iow we have some unintended interpretations. sometimes the |
| 19:07:29 | <ski> | multiplicity of interpretations is the point, e.g group theory, ring theory, lattices, ...) |
| 19:08:09 | <ski> | in this latter sense, "axiom" is more or less the same as "hypothesis" or "assumption", with the only practical different that the scope of it is rather broad, rather than only scoping over a small segment |
| 19:10:02 | <EvanR> | erisco, i take it you get the definition of limit of a sequence now. If not the definition of a definition |
| 19:10:12 | <EvanR> | it's a pretty neat definition |
| 19:10:16 | <shapr> | ski: I think solomon made a recording, I'm not sure if it was uploaded anywhere |
| 19:11:51 | <ski> | (btw, you can see an implementation of programming language as an "intended model", and you can view other analyzers, e.g. cross-referencers (e.g. building a dependency graph for modules or functions/procedures/predicates), linters, doc-extracters, &c. as "unintended interpretations" .. leaving the possibility for "unintended interpretations" can be very useful. this is also related to "shallow vs. deep |
| 19:11:57 | <ski> | embedding" of EDSLs .. if you implement a mini-language as a data-structure, you can interpret that tree and extract other information from it than just "running" it in the usual way (i always mix up which is which of deep and shallow, though .. they correspond to inductive vs. coinductive, more or less)) |
| 19:12:19 | <ski> | shapr : ah. would be interested to see it |
| 19:13:10 | ski | has to leave in a moment, would otherwise like to engage more in the conversation |
| 19:16:40 | <erisco> | for me it is just, in general conversation, there is a fungibility between axioms, hypotheses, conditions, yadda, yadda, though I recognise they can be ontologically distinct and relevantly so when being particular about a certain formal system |
| 19:20:30 | → | p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 19:20:44 | × | ski quits (~ski@83.248.72.178) (Ping timeout: 248 seconds) |
| 19:21:01 | <EvanR> | it's just hard to get anywhere if you can't make definitions along the way, without them being construed as something more |
| 19:21:37 | <EvanR> | have you ever seen a student or someone disagree with an argument because they say the definition "is wrong" xD |
| 19:21:46 | <EvanR> | before you even get to the point |
| 19:22:04 | <erisco> | What I am trying to grok about limits, and derivatives, is something like grokking integers versus evenness. I can construct the integers. In the mind they feel like a tangible thing. Evenness, on the other hand, is a property an integer can have. Turns out I can construct exactly the even integers too, but nonetheless, evenness itself sits in the mind like a property of a thing |
| 19:22:56 | <EvanR> | are you even integers just respellings of the first thing |
| 19:22:58 | <EvanR> | your |
| 19:23:23 | <EvanR> | without any other definitions they're equivalent |
| 19:23:28 | <erisco> | are you hinting at a bijection? yes sure |
| 19:33:18 | <erisco> | So I think where I am at, for this sequence perspective, the question starts at what is meant by sequence. Only from there can you then make sense of limits |
| 19:33:38 | <EvanR> | sure, ok, check the definition of sequence |
| 19:33:54 | <EvanR> | or pick one to your liking |
| 19:34:03 | <erisco> | there are many, is my point |
| 19:34:18 | <dolio> | It's a function from the natural numbers. |
| 19:34:22 | <mauke> | isn't a sequence basically just a mapping from ... that |
| 19:34:24 | <EvanR> | do they deviate from one another in any meaningful way |
| 19:34:51 | <erisco> | I should think so, yes |
| 19:34:57 | <dolio> | It's actually nicer for real numbers if you say it's a function from the rationals to an approximation with a radius given by that rational. |
| 19:36:00 | <dolio> | But it still works if you say it's a function from the naturals to an approximation with radius 1/2^n or something. |
| 19:36:17 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.0.2) |
| 19:36:21 | → | mima joins (~mmh@62.216.211.151) |
| 19:37:11 | <EvanR> | if alice's definition of sequence is function from the naturals, and bob's definition is a haskell data structure, and you can map losslessly between them, then cool we can move on xD |
| 19:44:31 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 245 seconds) |
| 19:48:41 | → | fweht joins (uid404746@id-404746.lymington.irccloud.com) |
| 19:51:01 | <dolio> | Yeah, you can also define them as streams of approximants, like `data Stream = Cons Q Stream`. |
| 19:54:37 | → | ft joins (~ft@p508db658.dip0.t-ipconnect.de) |
| 20:00:55 | → | Square2 joins (~Square4@user/square) |
| 20:02:53 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 20:03:11 | <dsal> | I don't know how to use cabal. How do I get a repl with the test suite in scope? |
| 20:03:56 | → | gdown joins (~gavin@h69-11-148-248.kndrid.broadband.dynamic.tds.net) |
| 20:05:09 | × | bratwurst quits (~blaadsfa@S010610561191f5d6.lb.shawcable.net) (Ping timeout: 250 seconds) |
| 20:07:45 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 20:09:32 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 20:10:08 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 20:10:57 | <geekosaur> | cabal repl test:testname? |
| 20:11:43 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 246 seconds) |
| 20:16:21 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 20:16:22 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 20:16:22 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 20:24:19 | <dsal> | Oh, it was :spec not :test-suite |
| 20:27:24 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 20:31:41 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:36:50 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 20:37:54 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:37:58 | → | pavonia joins (~user@user/siracusa) |
| 20:42:50 | → | Pickchea joins (~private@user/pickchea) |
| 20:54:57 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 258 seconds) |
| 20:57:44 | <justsomeguy> | What do I have to do to use this package with stack? Do I need to build it, or can I just pull it from stackage? https://github.com/brendanhay/amazonka |
| 20:58:00 | → | sm joins (~sm@plaintextaccounting/sm) |
| 20:58:20 | <geekosaur> | you would be building it either way; stack doesn't have binary provisioning or cache |
| 20:58:31 | <geekosaur> | I expect you have to put it in extra-deps |
| 20:58:50 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 20:59:35 | <geekosaur> | either via hackage (it was recently released) or via git commit references; I'd go with hackage extra-deps before trying to use git |
| 21:00:53 | <geekosaur> | oh, its hackage page claims stackage has it, but I don't know if it's in the latest LTS |
| 21:02:19 | <geekosaur> | not in the LTS, but is in https://www.stackage.org/nightly-2023-08-23 which is on ghc 9.6 |
| 21:04:20 | × | sm quits (~sm@plaintextaccounting/sm) (Quit: sm) |
| 21:10:15 | <justsomeguy> | Ok, so I have to build it from source, and then I can add the resulting tarball to extra-deps? |
| 21:10:47 | <justsomeguy> | Maybe this is a bad idea. |
| 21:11:26 | × | jonathan quits (~jonathan@193.203.13.91) (Ping timeout: 258 seconds) |
| 21:11:33 | <geekosaur> | no? |
| 21:11:46 | <geekosaur> | just add it to extra-deps, stack will handle fetching and building |
| 21:11:54 | → | finsternis joins (~X@23.226.237.192) |
| 21:12:02 | <geekosaur> | or use the nightly LTS and that way you don't need to add it to extra-deps |
| 21:12:24 | <justsomeguy> | Ahh, ok, that's much simpler. |
| 21:12:38 | justsomeguy | was dreading setting up nix and cabal to build this library |
| 21:13:15 | → | ulysses4ever joins (~artem@192.31.0.5) |
| 21:13:53 | × | artem quits (~artem@192.31.0.5) (Read error: Connection reset by peer) |
| 21:14:22 | <geekosaur> | the whole point of stack and modern cabal is to manage this stuff for you |
| 21:14:31 | × | ulysses4ever quits (~artem@192.31.0.5) (Read error: Connection reset by peer) |
| 21:14:43 | → | ulysses4ever joins (~artem@192.31.0.5) |
| 21:14:43 | <geekosaur> | so you just say "I need this library" somewhere and they fetch and build it |
| 21:19:08 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-212.fiber.dynamic.sonic.net) |
| 21:19:26 | <justsomeguy> | When I saw nix in the readme it wasn't clear to me that I can use it from stack or cabal alone. |
| 21:20:26 | × | gdown quits (~gavin@h69-11-148-248.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 21:21:49 | <geekosaur> | once it was released on hackage that version should work without nix |
| 21:22:00 | <geekosaur> | no promises about using it from git |
| 21:22:17 | → | nate2 joins (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
| 21:26:06 | × | dhil quits (~dhil@78.45.150.83.ewm.ftth.as8758.net) (Ping timeout: 252 seconds) |
| 21:27:10 | × | nate2 quits (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 21:31:36 | × | ulysses4ever quits (~artem@192.31.0.5) (Ping timeout: 245 seconds) |
| 21:32:50 | → | ulysses4ever joins (~artem@73.145.242.113) |
| 21:33:01 | → | sm joins (~sm@plaintextaccounting/sm) |
| 21:33:13 | × | sm quits (~sm@plaintextaccounting/sm) (Client Quit) |
| 21:34:27 | <justsomeguy> | Does this look right to you? https://github.com/kingparra/aws-for-jobs/tree/master/03_-_ec2_basics/deploy-an-instance/deploy-hs |
| 21:36:26 | → | jinsun_ joins (~jinsun@user/jinsun) |
| 21:36:27 | jinsun | is now known as Guest9199 |
| 21:36:27 | × | Guest9199 quits (~jinsun@user/jinsun) (Killed (silver.libera.chat (Nickname regained by services))) |
| 21:36:27 | jinsun_ | is now known as jinsun |
| 21:36:33 | × | ulysses4ever quits (~artem@73.145.242.113) (Read error: Connection reset by peer) |
| 21:38:10 | <justsomeguy> | Aha, I think that now stack is able to retrieve the package, but I'm getting build errors since I'm missing things like gcc-c++ and friends. |
| 21:38:26 | <justsomeguy> | Progress, at least. I can track down the dependencies. |
| 21:38:50 | → | ulysses4ever joins (~artem@192.31.0.5) |
| 21:40:10 | <justsomeguy> | Thanks for answering my dumb questions. I'm still figuring out the basics of stack, cabal, and nix. |
| 21:40:25 | <Rembane> | shapr: That sounds a bit disappointing. VPS hosts should just be good. I know I have high expectations. I got stuff to work though. Not running on unstable is a good start. |
| 21:40:38 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 256 seconds) |
| 21:41:15 | → | artem joins (~artem@73.145.242.113) |
| 21:41:40 | × | artem quits (~artem@73.145.242.113) (Read error: Connection reset by peer) |
| 21:42:17 | → | sm joins (~sm@plaintextaccounting/sm) |
| 21:42:22 | → | caryhartline joins (~caryhartl@168.182.58.169) |
| 21:42:33 | → | artem joins (~artem@2601:408:c405:79c5:f474:e3f8:9806:671) |
| 21:43:28 | × | ulysses4ever quits (~artem@192.31.0.5) (Ping timeout: 256 seconds) |
| 21:43:40 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:45:50 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 21:45:50 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 21:45:50 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 21:45:50 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds) |
| 21:47:42 | → | ulysses4ever joins (~artem@c-73-103-90-145.hsd1.in.comcast.net) |
| 21:47:58 | × | sm quits (~sm@plaintextaccounting/sm) (Quit: sm) |
| 21:49:43 | × | ulysses4ever quits (~artem@c-73-103-90-145.hsd1.in.comcast.net) (Read error: Connection reset by peer) |
| 21:50:00 | × | artem quits (~artem@2601:408:c405:79c5:f474:e3f8:9806:671) (Read error: Connection reset by peer) |
| 21:50:25 | → | ulysses4ever joins (~artem@73.145.242.113) |
| 21:52:23 | × | ulysses4ever quits (~artem@73.145.242.113) (Read error: Connection reset by peer) |
| 21:52:27 | → | artem joins (~artem@73.145.242.113) |
| 21:56:36 | × | artem quits (~artem@73.145.242.113) (Ping timeout: 245 seconds) |
| 21:56:40 | → | ulysses4ever joins (~artem@73.145.242.113) |
| 21:56:55 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 21:57:07 | × | ulysses4ever quits (~artem@73.145.242.113) (Read error: Connection reset by peer) |
| 21:57:12 | → | artem joins (~artem@73.145.242.113) |
| 21:57:38 | × | acidjnk quits (~acidjnk@p200300d6e7072f05a8abaa2c9ff73443.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 22:01:20 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 246 seconds) |
| 22:01:36 | × | artem quits (~artem@73.145.242.113) (Read error: Connection reset by peer) |
| 22:02:10 | → | ph88 joins (~ph88@ip5b403cd4.dynamic.kabel-deutschland.de) |
| 22:03:01 | → | ulysses4ever joins (~artem@73.145.242.113) |
| 22:03:28 | <ph88> | is there a nice way to make a "double" foldM ? foldM2 :: (Foldable t, Monad m) => (c -> b -> a -> m b) -> c -> t b -> t a -> m c |
| 22:03:55 | → | sm joins (~sm@plaintextaccounting/sm) |
| 22:04:03 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 252 seconds) |
| 22:04:38 | <EvanR> | would that do like a cross join |
| 22:05:08 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 22:05:27 | <EvanR> | also -> m c) ? |
| 22:08:48 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 22:09:04 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 22:09:04 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 22:09:04 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 22:11:20 | → | arahael joins (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) |
| 22:14:04 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 256 seconds) |
| 22:15:24 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:15:33 | → | dibblego joins (~dibblego@116.255.1.151) |
| 22:15:33 | × | dibblego quits (~dibblego@116.255.1.151) (Changing host) |
| 22:15:33 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 22:15:46 | × | arahael quits (~arahael@119-18-1-27.771201.syd.nbn.aussiebb.net) (Ping timeout: 256 seconds) |
| 22:16:45 | × | michalz quits (~michalz@185.246.207.203) (Remote host closed the connection) |
| 22:17:57 | → | jabuxas joins (~jabuxas@user/jabuxas) |
| 22:20:45 | <int-e> | aww, I can't have newtype X b where X :: (a, b) -> X b |
| 22:22:10 | × | dibblego quits (~dibblego@haskell/developer/dibblego) (Ping timeout: 245 seconds) |
| 22:22:34 | <int-e> | (that particular type isn't useful; it's a bit oversimplified) |
| 22:24:33 | <erisco> | ph88, Applicative gives t a -> t b -> t (a, b) which you can then fold |
| 22:26:09 | <erisco> | int-e, you can quantify a but you'll be challenged to construct an X |
| 22:26:36 | → | dibblego joins (~dibblego@116-255-1-151.ip4.superloop.au) |
| 22:26:36 | × | dibblego quits (~dibblego@116-255-1-151.ip4.superloop.au) (Changing host) |
| 22:26:36 | → | dibblego joins (~dibblego@haskell/developer/dibblego) |
| 22:27:26 | <int-e> | erisco: It's supposed to be existentially quantified. And I don't have a plain `a` but something with actual operations (an MVar, specifically.) |
| 22:28:04 | × | gatekempt quits (~gatekempt@user/gatekempt) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 22:28:08 | <ph88> | foldM2 :: (Foldable t, Monad m) => (c -> b -> a -> m c) -> c -> t b -> t a -> m c typo* |
| 22:28:11 | <int-e> | erisco: It would ultimately make sense as a newtype at runtime, when types are erased. But GHC doesn't like it. |
| 22:28:57 | <ph88> | erisco, where is t a -> t b -> t (a, b) ? |
| 22:29:12 | <erisco> | mm I see, so you want newtype especially, not data |
| 22:30:08 | <erisco> | you can make a separate data type, but I am guessing that isn't helping you |
| 22:31:34 | <int-e> | Sure, I can. It's really no big deal, it would just feel nice to have. |
| 22:32:20 | × | ulysses4ever quits (~artem@73.145.242.113) (Read error: Connection reset by peer) |
| 22:33:48 | → | ulysses4ever joins (~artem@73.145.242.113) |
| 22:35:16 | <erisco> | ph88, (<*>) . fmap (,) |
| 22:38:04 | × | ulysses4ever quits (~artem@73.145.242.113) (Read error: Connection reset by peer) |
| 22:39:44 | <ph88> | > :t (<*>) . fmap (,) |
| 22:39:45 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
| 22:39:56 | <geekosaur> | no "> " |
| 22:40:29 | <geekosaur> | :t (<*>) . fmap (,) |
| 22:40:30 | <lambdabot> | Applicative f => f a1 -> f a2 -> f (a1, a2) |
| 22:41:05 | → | falafel joins (~falafel@216.68.6.51.dyn.plus.net) |
| 22:41:52 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 22:42:43 | <geekosaur> | :t \a b -> (,) <$> a <*> b |
| 22:42:44 | <lambdabot> | Applicative f => f a1 -> f a2 -> f (a1, a2) |
| 22:42:48 | <geekosaur> | same thing |
| 22:44:38 | <geekosaur> | or `liftA2 (,)` |
| 22:45:31 | × | hyvoid quits (~hyenavoid@222-0-178-69.static.gci.net) (Remote host closed the connection) |
| 22:46:01 | → | wroathe joins (~wroathe@user/wroathe) |
| 22:47:05 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 22:48:56 | <[Leary]> | :t \f -> foldMap . foldMap f |
| 22:48:57 | <lambdabot> | (Monoid m, Foldable t1, Foldable t2) => (a1 -> a2 -> m) -> t2 a1 -> t1 a2 -> m |
| 22:49:26 | <geekosaur> | not quite what they asked for |
| 22:49:55 | <int-e> | erisco: in case you're interested in context: https://github.com/int-e/ivar-simple/issues/1#issuecomment-1690744097 |
| 22:50:28 | <[Leary]> | geekosaur: Should be if you use with `newtype EndoM m a = EndoM (a -> m a)`. |
| 22:50:38 | <[Leary]> | For the Monoid. |
| 22:51:00 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 22:51:01 | <[Leary]> | Though it's not clear if they want zippy or cartesion behaviour. |
| 22:51:38 | <[Leary]> | ph88: ^ |
| 22:53:22 | <ph88> | [Leary], cartesian |
| 22:55:46 | <[Leary]> | > (\f -> foldMap . foldMap f) (\a b -> [(a, b)]) "Hello" "world" |
| 22:55:48 | <lambdabot> | [('H','w'),('e','w'),('l','w'),('l','w'),('o','w'),('H','o'),('e','o'),('l',... |
| 22:56:16 | <[Leary]> | Yep, cartesian. |
| 22:58:46 | × | sm quits (~sm@plaintextaccounting/sm) (Quit: sm) |
| 22:59:37 | <ph88> | [Leary], i need foldM behavior with an accumulator and monadic action. Not all elemens of the two foldables should end up being used |
| 23:01:30 | <ph88> | :t \f a b -> foldM f c ((,) <$> a <*> b) |
| 23:01:31 | <lambdabot> | (Foldable t, Monad m, Applicative t) => (Expr -> (a1, a2) -> m Expr) -> t a1 -> t a2 -> m Expr |
| 23:02:02 | <ph88> | maybe this is the best which can be done |
| 23:02:12 | <[Leary]> | Did you see the `EndoM` monoid I wrote above? It should get you there. |
| 23:02:39 | <ph88> | with newtype ? |
| 23:02:45 | <[Leary]> | Yes. |
| 23:08:26 | <[Leary]> | :t \f t1 t2 -> appEndoM $ (foldMap . foldMap (\a b -> EndoM (f a b))) t1 t2 |
| 23:08:27 | <lambdabot> | (Monad m, Foldable t1, Foldable t2) => (t3 -> a1 -> a2 -> m a2) -> t2 t3 -> t1 a1 -> a2 -> m a2 |
| 23:09:38 | <[Leary]> | :t \f t1 t2 -> appEndoM . getDual $ (foldMap . foldMap (\a b -> Dual (EndoM (f a b)))) t1 t2 |
| 23:09:40 | <lambdabot> | (Monad m, Foldable t1, Foldable t2) => (t3 -> a1 -> a2 -> m a2) -> t2 t3 -> t1 a1 -> a2 -> m a2 |
| 23:10:10 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 256 seconds) |
| 23:13:29 | <ph88> | interesting solution, i have never seen EndoM |
| 23:15:49 | <ddellacosta> | ski: thanks, didn't know about any of those resources |
| 23:18:00 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 245 seconds) |
| 23:18:43 | <[Leary]> | It's essentially just `Kleisli` with the input and output forced to unify. A slightly broader construction would be `newtype Cat c a = Cat{ appCat :: c a a }; instance Category c => Semigroup (Cat c a) where Cat c1 <> Cat c2 = Cat (c1 . c2); instance Category c => Monoid (Cat c a) where mempty = Cat id`. Then `Endo` ~ `Cat (->)` and `EndoM` ~ `Cat Kleisli`, etc. |
| 23:21:35 | <[Leary]> | Err, `EndoM m` ~ `Cat (Kleisli m)`. |
| 23:25:37 | × | mud quits (~mud@user/kadoban) (Quit: quit) |
| 23:34:03 | → | drewjose5 joins (~drewjose@223.178.84.241) |
| 23:34:45 | × | bitdex_ quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 23:34:51 | × | drewjose quits (~drewjose@223.178.80.68) (Ping timeout: 246 seconds) |
| 23:34:51 | drewjose5 | is now known as drewjose |
| 23:35:48 | → | Pixi joins (~Pixi@user/pixi) |
| 23:35:54 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 246 seconds) |
| 23:44:44 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds) |
| 23:45:10 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 23:46:03 | × | bratwurst quits (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) (Ping timeout: 244 seconds) |
| 23:48:01 | → | ulysses4ever joins (~artem@2601:408:c405:84e:f474:e3f8:9806:671) |
| 23:48:44 | → | bratwurst joins (~blaadsfa@2604:3d09:207f:f650:216:3eff:fe5a:a1f8) |
| 23:54:24 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 23:54:24 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 23:54:24 | → | wroathe joins (~wroathe@user/wroathe) |
All times are in UTC on 2023-08-23.