Home liberachat/#haskell: Logs Calendar

Logs on 2025-04-09 (liberachat/#haskell)

00:00:25 <emojelly> Like if I write a fib function... then it will return a thunk (for discussion's sake). Now that thunk might get evaluated somewhere else entirely, but usually at least time profiling will still tell me that fib is the function to which the work is attributed, no?
00:00:47 <emojelly> At least that's how I understood it to work. The documentation literally says it's saving away the *call* stack, not the evaluation stack (if that's the right word).
00:02:23 <geekosaur> right, which means it ought to attribute things to where they're generated, not where they're forced
00:02:36 <emojelly> And the kicker is that the entire combineTestSignals' only merges two Coroutines together, which means replacing the continuation with a new continuation that calls the continuations of both coroutines and pastes them together.
00:02:42 <emojelly> Apart from that it's a whole lot of wrapping and unwrapping.
00:03:33 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
00:03:33 × jespada quits (~jespada@r179-25-248-190.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds)
00:03:41 <emojelly> geekosaur: exactly, which makes this case so weird, because: a) nothing gets forced in "combineTestSignals' (,)" itself, I think, but b) even if it would it certainly didn't come from that expression
00:08:01 sprout joins (~sprout@2a02-a448-3a80-0-c61c-b515-5509-58e7.fixed6.kpn.net)
00:09:00 <haskellbridge> <Bowuigi> emojelly did you disable optimization for the profiling build? That shouldn't allocate too much
00:09:14 <haskellbridge> <Bowuigi> Either that or it's weird CAF shenanigans
00:09:31 hgolden_ joins (~hgolden@syn-172-251-233-141.res.spectrum.com)
00:09:58 × potatoespotatoes quits (~quassel@user/potatoespotatoes) ()
00:10:07 × hgolden_ quits (~hgolden@syn-172-251-233-141.res.spectrum.com) (Remote host closed the connection)
00:11:37 <haskellbridge> <Bowuigi> If you don't want to disable optimization, make sure that GHC doesn't inline combineTestSignals'
00:11:38 <geekosaur> with prof-late optimization shouldn't matter
00:12:00 × hgolden quits (~hgolden@2603:8000:9d00:3ed1:d5a9:8f67:3cb9:6399) (Ping timeout: 246 seconds)
00:12:20 <statusbot> Maintenance update: hackage is going down for migration. -- http://status.haskell.org/pages/maintenance/537c07b0cf1fad5830000093/67f5bb13d9e59f092626b642
00:12:52 potatoespotatoes joins (~quassel@130.44.147.204)
00:12:52 × potatoespotatoes quits (~quassel@130.44.147.204) (Changing host)
00:12:52 potatoespotatoes joins (~quassel@user/potatoespotatoes)
00:12:59 × potatoespotatoes quits (~quassel@user/potatoespotatoes) (Client Quit)
00:13:24 potatoespotatoes joins (~quassel@130.44.147.204)
00:13:24 × potatoespotatoes quits (~quassel@130.44.147.204) (Changing host)
00:13:24 potatoespotatoes joins (~quassel@user/potatoespotatoes)
00:13:31 × potatoespotatoes quits (~quassel@user/potatoespotatoes) (Client Quit)
00:13:56 potatoespotatoes joins (~quassel@user/potatoespotatoes)
00:14:43 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
00:16:11 <emojelly> haskellbridge: I tried everything. Disabling optimization, enabling optimization, various profiling settings, switching between GHC 9.8 and 9.10...
00:16:47 <emojelly> it is entirely possible that the problem is maybe in Clash, which I have practically no insight into, but if, profiling is just not telling me anything.
00:17:02 × ystael quits (~ystael@user/ystael) (Ping timeout: 244 seconds)
00:17:20 <emojelly> (system process sampling and looking up the funky generated symbol name in the Core code seems to rather suggest it's in my code at first glance, though.)
00:18:00 <emojelly> have to run.
00:19:57 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
00:19:58 × inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 245 seconds)
00:20:53 inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net)
00:22:17 Inst joins (~Inst@user/Inst)
00:26:44 × inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
00:27:11 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
00:30:30 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
00:32:43 × califax quits (~califax@user/califx) (Remote host closed the connection)
00:34:25 califax joins (~califax@user/califx)
00:34:48 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
00:37:13 × gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 268 seconds)
00:39:09 gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk)
00:40:11 inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net)
00:43:09 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 246 seconds)
00:45:53 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
00:50:18 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
00:51:01 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
00:54:34 <EvanR> dude why are you talking to a bridge
00:55:43 <geekosaur> because many IRC clients autocomplete to the last speaker on a bare tab, which will get the bridge
00:55:45 × xff0x quits (~xff0x@2405:6580:b080:900:c071:5032:6468:f840) (Ping timeout: 248 seconds)
00:57:26 <emojelly> Ah, no. Because my irc client front end has a bug right now that swallows stuff in angle brackets, brackets included. I didn’t realize there was a name there…
00:57:54 <EvanR> oof
00:57:55 <emojelly> I *did* wonder, but I figured maybe this bridge is only used by a single user. :’)
00:58:52 <haskellbridge> <Liamzee> geekosaur maintains a bridge between some haskell rooms and matrix
00:58:57 <geekosaur> I want to move the bridge to something that does puppeting, but I need to get it off my personal box and that's waiting on the HF
00:59:22 × otto_s quits (~user@p5b044d5e.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
00:59:44 <geekosaur> (it works best with IPv6 but my provider's in the 20th century still)
01:01:19 otto_s joins (~user@p4ff27c58.dip0.t-ipconnect.de)
01:01:41 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:03:02 cptaffe joins (~cptaffe@user/cptaffe)
01:06:41 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
01:06:47 <EvanR> I dunno, this IPv6 stuff is probably just a fad
01:06:52 <EvanR> like unicode
01:07:13 <jackdk> emojelly: some kind of HTML sanitising?
01:07:38 <EvanR> third rate back alley HTML sanitizing
01:07:58 <haskellbridge> <Bowuigi> That shouldn't remove tags, just replace them with their &-codes
01:09:15 <geekosaur> that's certainly how I've always done it
01:11:49 <mauke> Bowuigi: that would be HTML escaping, not sanitizing
01:12:49 <geekosaur> .oO{ so you're saying sanitizing isn't sane? )
01:13:47 <mauke> exactly
01:14:17 <haskellbridge> <Bowuigi> It should just remove stuff on a blocklist and escape the unknowns
01:14:22 <mauke> "sanitizing" = mangling your inputs to remove all the "harmful" parts
01:14:49 <haskellbridge> <Bowuigi> That's the sanest option, given it removes possibly harmful stuff and keeps the rest
01:15:37 <haskellbridge> <Bowuigi> Unless my alias is potentially harmful, which it might be for my career but not for anyone else
01:17:27 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:19:37 <EvanR> sanitize :: String -> String
01:19:41 <EvanR> sanitize _ = ""
01:20:42 weary-traveler joins (~user@user/user363627)
01:21:57 <jackdk> No output, no vulnerability
01:22:09 <jackdk> And with lazy evaluation it doesn't even consider the input!
01:22:28 × XZDX quits (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Remote host closed the connection)
01:22:28 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
01:28:54 <haskellbridge> <Liamzee> the empty string is technically output
01:29:49 <haskellbridge> <Liamzee> i wonder what the safety of outputting bottom would be, though
01:33:16 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:33:31 prolic_ joins (~sasa@181.122.135.9)
01:36:02 <EvanR> perfectly safe. Just ignore the existence of bottom
01:37:53 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
01:44:32 xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
01:49:03 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:52:51 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
01:53:51 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
01:59:12 <statusbot> Maintenance update: hackage server is operational again! -- http://status.haskell.org/pages/maintenance/537c07b0cf1fad5830000093/67f5bb13d9e59f092626b642
01:59:18 <haskellbridge> <Liamzee> yay
01:59:27 <haskellbridge> <Liamzee> thanks @sclv etc
01:59:38 Garbanzo joins (~Garbanzo@2602:304:6eac:dc10::2e)
01:59:46 × notdabs quits (~Owner@2600:1700:69cf:9000:1d8b:380b:ab0b:1fbd) (Read error: Connection reset by peer)
02:02:57 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds)
02:03:37 qyrhx joins (~qyrhx@user/qyrhx)
02:04:51 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:05:04 × jmcantrell quits (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0)
02:05:05 jmcantrell_ is now known as jmcantrell
02:08:06 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
02:08:47 __jmcantrell__ joins (~weechat@user/jmcantrell)
02:08:49 × qyrhx quits (~qyrhx@user/qyrhx) (Quit: WeeChat 4.6.0)
02:09:36 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
02:10:28 × jmcantrell quits (644f1bed9a@user/jmcantrell) (Killed (tungsten.libera.chat (Nickname regained by services)))
02:10:28 __jmcantrell__ is now known as jmcantrell
02:10:37 jmcantrell_ joins (644f1bed9a@user/jmcantrell)
02:15:40 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer)
02:16:13 ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
02:17:26 ezzieygu1wuf joins (~Unknown@user/ezzieyguywuf)
02:17:58 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer)
02:20:38 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:23:41 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
02:24:50 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
02:26:59 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds)
02:27:22 j1n37 joins (~j1n37@user/j1n37)
02:28:34 × euphores quits (~SASL_euph@user/euphores) (Ping timeout: 244 seconds)
02:33:36 × bramh quits (~bramh@user/bramh) (Quit: Ping timeout (120 seconds))
02:33:50 bramh joins (~bramh@user/bramh)
02:36:00 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:36:26 euphores joins (~SASL_euph@user/euphores)
02:36:37 × Inst quits (~Inst@user/Inst) (Ping timeout: 248 seconds)
02:36:49 <emojelly> jackdk: I think it’s HTML sanitizing gone wrong, because I didn’t have this problem with an earlier version of the front end.
02:37:59 <monochrom> Moar general: sanitize :: a -> [b]; sanitize _ = []
02:38:52 <monochrom> Or maybe you prefer this other generalization direction? sanitize :: Istring b => a -> b; sanitize _ = ""
02:40:27 × prolic_ quits (~sasa@181.122.135.9) (Ping timeout: 244 seconds)
02:40:48 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
02:40:56 <EvanR> give me the most general generalization
02:42:10 <geekosaur> const []
02:42:18 <monochrom> sanitize :: forall a b c. IsString c => a -> ([b], c); sanitize _ = ([], "")
02:46:41 <haskellbridge> <Bowuigi> sanitize _ = mempty
02:47:19 <haskellbridge> <Bowuigi> Pointed sets would be more general, but it has to have this meaning of "nothing but something"
02:49:02 <monochrom> Like this? sanitize :: a -> Maybe b; sanitize _ = Nothing
02:51:10 <monochrom> OK mempty is nicer.
02:51:44 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:52:16 × EvanR quits (~EvanR@user/evanr) (Ping timeout: 268 seconds)
02:55:42 bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
02:56:39 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
02:57:20 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Max SendQ exceeded)
02:57:43 <mauke> sanitize :: a -> ()
02:58:02 <monochrom> :)
02:58:54 <monochrom> That's brilliant. The terminal object ought to be the most general. :)
03:00:07 bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
03:01:19 EvanR joins (~EvanR@user/evanr)
03:04:44 <jackdk> What they don't tell you is that `sanitise` uses `acme-smuggler` under the hood
03:07:33 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:09:17 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:10:04 <haskellbridge> <Liamzee> is everything okay with your issue, emojelly? I probably can't be of help, but just hoping you fixed your problem
03:10:50 <haskellbridge> <Liamzee> and sorry for the jokes (but you might actually want to shift the sanitize function to () and see how the profiler goes)
03:13:15 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
03:21:18 Square2 joins (~Square@user/square)
03:23:17 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:25:18 × Square quits (~Square4@user/square) (Ping timeout: 252 seconds)
03:27:12 × spew quits (~spew@135.233.119.40) (Remote host closed the connection)
03:27:58 spew joins (~spew@135.233.119.40)
03:28:21 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
03:28:41 × spew quits (~spew@135.233.119.40) (Remote host closed the connection)
03:29:04 spew joins (~spew@135.233.119.40)
03:32:05 segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
03:39:05 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:43:45 michalz joins (~michalz@185.246.207.200)
03:44:00 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
03:49:25 JuanDaugherty joins (~juan@user/JuanDaugherty)
03:54:49 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:59:49 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
04:10:37 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:16:18 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
04:22:01 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:25:10 j1n37 joins (~j1n37@user/j1n37)
04:26:24 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:26:51 tavare joins (~tavare@150.129.88.189)
04:26:51 × tavare quits (~tavare@150.129.88.189) (Changing host)
04:26:51 tavare joins (~tavare@user/tavare)
04:29:28 × Square2 quits (~Square@user/square) (Ping timeout: 244 seconds)
04:31:17 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
04:41:51 thuna` joins (~thuna`@user/thuna/x-1480069)
04:42:11 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:42:50 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:46:00 j1n37 joins (~j1n37@user/j1n37)
04:47:29 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
04:57:56 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:58:03 harveypwca joins (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c)
05:01:19 JuanDaugherty is now known as ColinRobinson
05:02:28 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
05:05:38 × amadaluzia quits (~amadaluzi@user/amadaluzia) (Quit: Hi, this is Paul Allen. I'm being called away to London for a few days. Meredith, I'll call you when I get back. Hasta la vista, baby.)
05:06:37 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:11:33 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
05:11:50 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
05:11:59 esph joins (~weechat@user/esph)
05:12:26 sayurc joins (~sayurc@169.150.203.34)
05:12:48 × segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 265 seconds)
05:19:58 j1n37- joins (~j1n37@user/j1n37)
05:20:00 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 246 seconds)
05:22:27 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:24:33 × thuna` quits (~thuna`@user/thuna/x-1480069) (Ping timeout: 246 seconds)
05:27:13 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
05:28:40 Inst joins (~Inst@user/Inst)
05:29:57 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:34:33 × tavare quits (~tavare@user/tavare) (Remote host closed the connection)
05:34:39 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
05:46:01 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
05:50:45 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
05:53:59 × Natch quits (~natch@c-92-34-7-158.bbcust.telenor.se) (Ping timeout: 260 seconds)
05:54:14 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
05:55:23 Natch joins (~natch@c-92-34-7-158.bbcust.telenor.se)
06:01:24 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:06:15 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
06:06:25 thuna` joins (~thuna`@user/thuna/x-1480069)
06:06:57 × jmcantrell quits (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0)
06:06:57 jmcantrell_ is now known as jmcantrell
06:18:06 × Garbanzo quits (~Garbanzo@2602:304:6eac:dc10::2e) (Remote host closed the connection)
06:29:19 × harveypwca quits (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving)
06:29:57 ColinRobinson is now known as JuanDaugherty
06:32:59 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:38:04 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
06:40:03 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
06:42:22 × ft quits (~ft@p508db463.dip0.t-ipconnect.de) (Quit: leaving)
06:48:21 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
06:51:56 fp joins (~Thunderbi@2001:708:20:1406::1370)
06:53:06 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
06:57:54 × fantom quits (~fantom@2.219.56.221) (Quit: Connection error?!)
06:58:21 × sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!)
07:00:01 × caconym quits (~caconym@user/caconym) (Quit: bye)
07:00:57 caconym joins (~caconym@user/caconym)
07:01:50 CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
07:03:07 JuanDaugherty is now known as ColinRobinson
07:03:22 fantom joins (~fantom@2.219.56.221)
07:03:40 polyphem joins (~rod@p4fc2cdf8.dip0.t-ipconnect.de)
07:04:08 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
07:06:54 sord937 joins (~sord937@gateway/tor-sasl/sord937)
07:08:58 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
07:17:06 jco joins (~jco@78-70-217-44-no600.tbcn.telia.com)
07:18:00 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds)
07:18:12 lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
07:18:45 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
07:18:50 Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915)
07:25:51 <[exa]> is there any good way to build stuff with accelerate-llvm-native without stack now? I was trying to somewhat revive the docker container but it fails (llvm 15 not available etc)
07:26:18 × emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir)
07:34:49 acidjnk_new3 joins (~acidjnk@p200300d6e71c4f99589ab59c7ee4b7ea.dip0.t-ipconnect.de)
07:37:08 __monty__ joins (~toonn@user/toonn)
07:37:12 × califax quits (~califax@user/califx) (Quit: ZNC 1.8.2 - https://znc.in)
07:37:27 califax joins (~califax@user/califx)
07:38:05 a_fantom joins (~fantom@2.219.56.221)
07:41:09 × fantom quits (~fantom@2.219.56.221) (Ping timeout: 244 seconds)
07:41:37 chele joins (~chele@user/chele)
07:45:57 merijn joins (~merijn@77.242.116.146)
07:51:40 Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
07:55:47 × ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
07:57:06 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
07:59:17 fantom joins (~fantom@2.219.56.221)
08:01:49 × a_fantom quits (~fantom@2.219.56.221) (Ping timeout: 244 seconds)
08:05:54 × Inst quits (~Inst@user/Inst) (Remote host closed the connection)
08:07:48 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:14:12 × Googulator quits (~Googulato@2a01-036d-0106-211a-f46d-c0c9-579b-1a24.pool6.digikabel.hu) (Quit: Client closed)
08:38:51 lxsameer joins (~lxsameer@Serene/lxsameer)
08:39:27 × j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 268 seconds)
08:41:48 j1n37 joins (~j1n37@user/j1n37)
08:48:48 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 252 seconds)
08:56:33 × poxel quits (~lennart@user/poxel) (Quit: WeeChat 4.6.0)
09:00:05 × fp quits (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 248 seconds)
09:03:47 fp joins (~Thunderbi@2001:708:150:10::1d80)
09:13:02 lortabac joins (~lortabac@2a0d:e487:132f:be52:3a12:65c4:6cf:efd7)
09:13:50 × Katarushisu quits (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: The Lounge - https://thelounge.chat)
09:14:42 Katarushisu joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net)
09:16:46 ljdarj joins (~Thunderbi@user/ljdarj)
09:24:55 forell_ joins (~forell@host-178-216-90-220.sta.tvknaszapraca.pl)
09:25:00 × forell quits (~forell@user/forell) (Ping timeout: 252 seconds)
09:26:25 vanishingideal joins (~vanishing@user/vanishingideal)
09:27:10 × vanishingideal quits (~vanishing@user/vanishingideal) (Remote host closed the connection)
09:37:06 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
09:40:57 × Katarushisu quits (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: The Lounge - https://thelounge.chat)
09:41:08 tabaqui joins (~tabaqui@167.71.80.236)
09:41:14 Katarushisu joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net)
09:41:42 j1n37 joins (~j1n37@user/j1n37)
09:47:56 × EvanR quits (~EvanR@user/evanr) (Read error: Connection reset by peer)
09:48:03 EvanR_ joins (~EvanR@user/evanr)
09:53:09 × lortabac quits (~lortabac@2a0d:e487:132f:be52:3a12:65c4:6cf:efd7) (Ping timeout: 252 seconds)
09:59:12 justin joins (~justin@136.158.10.171)
09:59:12 justin is now known as Guest6600
10:01:05 × Guest6600 quits (~justin@136.158.10.171) (Client Quit)
10:03:08 × xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
10:05:40 segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
10:10:53 alp joins (~alp@2001:861:8ca0:4940:93b8:dd2d:3845:3995)
10:19:15 × fantom quits (~fantom@2.219.56.221) (Ping timeout: 244 seconds)
10:24:39 × segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds)
10:28:01 <haskellbridge> <Morj> Hello Joe, do you like functional programming?
11:02:00 jespada joins (~jespada@r179-25-248-190.dialup.adsl.anteldata.net.uy)
11:02:49 lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
11:05:42 xff0x joins (~xff0x@2405:6580:b080:900:b50:e5e9:27c3:86)
11:13:40 <Digit> every time i'm configuring a program in something other than haskell, i feel like i'm wasting time that could be better spent better learning haskell... how far can one go, in replacing all the things with haskell programs? ... e.g. is there a terminal emulator written in haskell? yi for text editor, what else? can "everything" be covered?
11:15:37 <dmoerner> although there are exceptions (suckless, e.g.) i don't find that most programs written in language X need to be configured in language X
11:16:20 <dmoerner> instead for good reason they often use a specific language for configuration, like toml
11:22:24 <dutchie> there's xmonad for window management that immediately comes to mind
11:22:50 <dutchie> you could always generate program X's config by writing a Haskell program
11:26:10 <Leary> @hackage termonad
11:26:10 <lambdabot> https://hackage.haskell.org/package/termonad
11:26:14 <Leary> Digit: ^
11:27:04 <int-e> . o O ( what a name, but "termonador" would be better )
11:28:57 <merijn> Digit: There's also vty
11:29:39 <merijn> Although, tbh I doubt using yi would be a worthwhile investment :p
11:31:35 × euphores quits (~SASL_euph@user/euphores) (Ping timeout: 244 seconds)
11:34:10 sprotte24 joins (~sprotte24@p200300d16f0bc1000c82a6b41033ea55.dip0.t-ipconnect.de)
11:45:41 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 268 seconds)
11:48:35 × hsw quits (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) (Remote host closed the connection)
11:48:54 hsw joins (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw)
11:52:49 × jespada quits (~jespada@r179-25-248-190.dialup.adsl.anteldata.net.uy) (Ping timeout: 248 seconds)
11:55:15 × TheCoffeMaker_ quits (~TheCoffeM@186.136.173.186) (Ping timeout: 252 seconds)
11:55:46 jespada joins (~jespada@r190-133-30-51.dialup.adsl.anteldata.net.uy)
11:55:59 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
11:56:23 × YoungFrog quits (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Ping timeout: 265 seconds)
11:57:45 ljdarj joins (~Thunderbi@user/ljdarj)
12:01:13 JuanDaugherty joins (~juan@user/JuanDaugherty)
12:06:48 notdabs joins (~Owner@2600:1700:69cf:9000:19b2:995a:60d5:3b93)
12:07:03 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 246 seconds)
12:16:31 × zfnmxt quits (~zfnmxt@user/zfnmxt) (Remote host closed the connection)
12:17:32 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds)
12:17:34 × TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 244 seconds)
12:18:00 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
12:20:50 zfnmxt joins (~zfnmxt@user/zfnmxt)
12:27:49 JuanDaugherty is now known as ColinRobinson
12:30:33 as_ joins (~as@2800:a4:298:ee00:7661:9c1d:e20c:62d8)
12:30:52 comerijn joins (~merijn@77.242.116.146)
12:30:54 × thuna` quits (~thuna`@user/thuna/x-1480069) (Ping timeout: 252 seconds)
12:33:36 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds)
12:36:26 ljdarj joins (~Thunderbi@user/ljdarj)
12:36:38 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
12:43:59 michalz_ joins (~michalz@185.246.207.203)
12:44:33 × michalz quits (~michalz@185.246.207.200) (Ping timeout: 245 seconds)
12:54:56 × 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)
12:55:32 troydm joins (~troydm@user/troydm)
12:59:04 × fp quits (~Thunderbi@2001:708:150:10::1d80) (Ping timeout: 268 seconds)
13:26:53 fp joins (~Thunderbi@2001:708:20:1406::1370)
13:34:32 × TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Remote host closed the connection)
13:34:55 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
13:35:35 segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
13:40:02 tromp joins (~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf)
13:42:22 Square joins (~Square4@user/square)
13:52:11 ystael joins (~ystael@user/ystael)
14:12:52 × ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
14:14:52 <[exa]> Digit: unix clearly dictates that there's no silver bullet
14:14:57 CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
14:15:35 <[exa]> (otoh any time spent trying to sensibly port stuff to haskell is certainly not wasted)
14:16:11 amadaluzia joins (~amadaluzi@2a00:23c7:ed8b:6701:58aa:f4c7:c90:674e)
14:17:48 <[exa]> btw, is there any modern replacement for Ivory? I see the website is somehow dead today
14:19:48 × TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 252 seconds)
14:20:35 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
14:30:23 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 245 seconds)
14:32:00 j1n37 joins (~j1n37@user/j1n37)
14:33:25 × acidjnk_new3 quits (~acidjnk@p200300d6e71c4f99589ab59c7ee4b7ea.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
14:36:13 × segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 245 seconds)
14:37:44 × fp quits (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 268 seconds)
14:54:44 Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
14:56:02 EvanR_ is now known as EvanR
14:57:10 __jmcantrell__ joins (~weechat@user/jmcantrell)
14:57:27 jmcantrell is now known as Guest4549
14:57:27 × Guest4549 quits (644f1bed9a@user/jmcantrell) (Killed (zirconium.libera.chat (Nickname regained by services)))
14:57:27 __jmcantrell__ is now known as jmcantrell
14:57:35 jmcantrell_ joins (644f1bed9a@user/jmcantrell)
15:07:16 × tromp quits (~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf) (Quit: My iMac has gone to sleep. ZZZzzz…)
15:10:25 acidjnk_new3 joins (~acidjnk@p200300d6e71c4f995d166d77a499a203.dip0.t-ipconnect.de)
15:18:50 × as_ quits (~as@2800:a4:298:ee00:7661:9c1d:e20c:62d8) (Quit: as_)
15:20:38 × rembo10 quits (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in)
15:20:50 euphores joins (~SASL_euph@user/euphores)
15:21:23 as_ joins (~as@2800:a4:298:ee00:7661:9c1d:e20c:62d8)
15:22:06 rembo10 joins (~rembo10@main.remulis.com)
15:25:25 × alp quits (~alp@2001:861:8ca0:4940:93b8:dd2d:3845:3995) (Ping timeout: 252 seconds)
15:28:48 <hellwolf> There is no (!!) for linear arrays: you need to split it, dup it to (it', it'') then use it' and assemble the original list back with it''.
15:28:53 <hellwolf> pain
15:31:56 tromp joins (~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf)
15:32:02 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 248 seconds)
15:33:38 <EvanR> !! is lookup
15:33:43 zmt00 joins (~zmt00@user/zmt00)
15:33:45 <EvanR> the operation is usually ! for arrays
15:33:49 <EvanR> operator*
15:34:07 <EvanR> > [1,2,3,4,5] !! 3
15:34:08 <lambdabot> 4
15:34:29 <int-e> I don't think it matters for the linear type trouble
15:34:41 <EvanR> oh, linear
15:35:26 <int-e> though you could still have a function that replaces an array element and returns the old one
15:35:54 <EvanR> get :: HasCallStack => Int -> Vector a %1 -> (Ur a, Vector a)
15:36:59 <int-e> EvanR: more precisely, the problem would occur if the elements have a linear type
15:37:11 int-e shrugs
15:38:02 <EvanR> example?
15:39:34 <EvanR> a vector of linear functions?
15:40:13 × biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer)
15:42:12 <int-e> I'm trying to understand where the unrestricted a in your signature comes from. That would mean the elements of the vectors are also unrestricted when they are put in, wouldn't it?
15:42:48 <EvanR> let me find the constructor
15:43:18 <EvanR> fromList :: (HasCallStack, Movable b) => [a] -> (Vector a %1 -> b) %1 -> b
15:43:24 <EvanR> no
15:43:30 <EvanR> yes
15:44:45 <EvanR> so that's what Data.Vector.Mutable.Linear does
15:48:03 ft joins (~ft@p508db463.dip0.t-ipconnect.de)
15:49:15 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 252 seconds)
15:51:44 × comerijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds)
15:54:26 × califax quits (~califax@user/califx) (Remote host closed the connection)
15:54:26 × Chai-T-Rex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
15:54:55 ChaiTRex joins (~ChaiTRex@user/chaitrex)
15:54:55 califax joins (~califax@user/califx)
15:58:54 as_ parts (~as@2800:a4:298:ee00:7661:9c1d:e20c:62d8) (Adiós)
16:06:13 × acidjnk_new3 quits (~acidjnk@p200300d6e71c4f995d166d77a499a203.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
16:13:21 CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
16:14:55 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
16:15:29 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
16:18:21 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 265 seconds)
16:28:04 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds)
16:30:32 sayurc joins (~sayurc@169.150.203.34)
16:35:24 stef204 joins (~stef204@user/stef204)
16:36:43 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
16:44:46 alp joins (~alp@2001:861:8ca0:4940:408a:bf2b:1297:8090)
16:46:44 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds)
16:48:46 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
16:52:15 × L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 276 seconds)
16:53:42 wootehfoot joins (~wootehfoo@user/wootehfoot)
16:54:18 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
17:02:53 <EvanR> does the W in algorithm W stand for anything in particular
17:03:57 <spew> wadler
17:04:35 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
17:07:00 <EvanR> it's from Milner 1978, at which time wadler had just completed their bachelors in mathematics
17:07:06 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
17:07:56 <EvanR> A Theory of Type Polymorphism in Programming
17:08:11 × tromp quits (~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:08:48 × chele quits (~chele@user/chele) (Remote host closed the connection)
17:09:34 × sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!)
17:12:00 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
17:13:07 <spew> they were future seers
17:15:31 tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
17:16:06 euphores joins (~SASL_euph@user/euphores)
17:16:25 sayurc joins (~sayurc@169.150.203.34)
17:17:04 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
17:18:04 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
17:20:06 <haskellbridge> <Bowuigi> Milner was just using gen Z language because the algorithm was ahead of its time
17:20:12 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds)
17:20:59 j1n37 joins (~j1n37@user/j1n37)
17:22:34 tromp joins (~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf)
17:22:37 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
17:23:14 <Leary> EvanR: Probably 'well-typing'.
17:24:35 × amadaluzia quits (~amadaluzi@2a00:23c7:ed8b:6701:58aa:f4c7:c90:674e) (Changing host)
17:24:35 amadaluzia joins (~amadaluzi@user/amadaluzia)
17:27:16 segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
17:27:17 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
17:32:56 × alp quits (~alp@2001:861:8ca0:4940:408a:bf2b:1297:8090) (Ping timeout: 272 seconds)
17:34:48 × segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Quit: segfaultfizzbuzz)
17:35:00 acidjnk_new3 joins (~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de)
17:36:24 <EvanR> wikipedia states: Formally, in HM, a type σ' is more general than σ, formally σ' ⊑ σ, if ...
17:36:34 <EvanR> struggling to justify that choice of operator for that xD
17:36:47 <EvanR> since it looks like subset of
17:37:14 <EvanR> or less than
17:37:17 <EvanR> not more than
17:38:04 <int-e> well a more general type has fewer inhabitants; consider the extreme case forall a. a
17:38:26 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
17:39:56 <EvanR> in general that's not necessarily true
17:40:46 <int-e> are you sure about that
17:40:54 <EvanR> give or take I still don't know how to count such inhabitants
17:41:25 <int-e> any inhabitant of sigma' can be used at type sigma
17:42:17 <EvanR> more information about the types may let you do other things, but not less things
17:42:24 <EvanR> ok
17:43:21 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
17:47:56 atwm joins (~andrew@19-193-28-81.ftth.cust.kwaoo.net)
17:48:07 × sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!)
17:48:10 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
17:52:39 × atwm quits (~andrew@19-193-28-81.ftth.cust.kwaoo.net) (Client Quit)
17:52:53 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
17:54:59 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
18:03:56 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
18:03:59 <monochrom> So "more general" means "less information".
18:05:34 <monochrom> To be sure, that sounds wrong until I show the intermediate steps: more general = more abstract = less detail = less information
18:07:24 <monochrom> You can remember this example: \x -> x could be Int->Int or it could also be forall a. a->a. Int->Int is a larger space, forall a. a->a is a smaller space.
18:08:49 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
18:10:12 <int-e> monochrom: so by making things more general you strive to convey as little information as possible
18:10:14 <[exa]> EvanR: I'm usually reading that operator as "less specialized" but the choice still sucks
18:10:20 sayurc joins (~sayurc@169.150.203.34)
18:10:29 <EvanR> "less specialized" didn't help xD
18:10:47 <EvanR> since I guess I just flipped the confusion around mentally to still be there
18:10:52 <[exa]> at least it sounds properly like the "less than" for me
18:11:06 <[exa]> yeah
18:11:15 <int-e> in the end the choice of direction is completely arbitrary
18:11:27 <EvanR> sure
18:11:29 <[exa]> maybe we could just go and edit the wiki? where did they get the boxy lessthan anyway?
18:11:42 [exa] wants to see some radical model theory
18:11:44 <int-e> from unicode?
18:11:52 int-e runs
18:11:58 [exa] throws a stone
18:12:08 <monochrom> Yeah my favourite tease is saying that half of the fundamental theorem of Galois theory is just lattice theory, to show how little information it has/needs. >:)
18:12:40 <monochrom> (Also, that half is just 5-10 lines of proof.)
18:12:41 <int-e> I suspect that this direction is standard in the relevant fragment of the literature and you'd confuse people if you flipped the direction
18:13:26 <EvanR> you can say "σ' is more general than σ, formally σ ⊒ σ'"
18:13:31 <EvanR> totally arbitrary xD
18:13:49 <int-e> ⊑ is a standard symbol for partial orders that aren't comparisons or subsets
18:14:00 <int-e> EvanR: I see what you did there and I don't disapprove.
18:14:14 <EvanR> yeah I think of it as "less than"
18:14:24 <EvanR> and forall a . a is at the bottom
18:15:21 <EvanR> "lines of proof" (LOP)
18:17:24 <monochrom> Speaking of which, you do have an inverse relationship between number of statements satisfied vs number of elements.
18:18:20 <[exa]> kinda wondering, doesn't the declarative rule system they have there actually give a slightly different typesystem than what they show with algorithm W later?
18:19:03 <EvanR> they describe 4 different rule systems
18:19:12 <EvanR> for reasons, I presume
18:19:14 × ft quits (~ft@p508db463.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
18:19:25 <[exa]> as in, the Inst rule with ⊒ allows partial instantiation as opposed to the explicit instantiate() later below
18:19:44 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
18:19:45 <EvanR> if you get to they very end of that story, they kind of leave you on a cliffhanger
18:20:00 <EvanR> (proof obligations)
18:20:27 <int-e> (execises to the reader)
18:20:30 <int-e> +r
18:21:12 ft joins (~ft@p508db594.dip0.t-ipconnect.de)
18:21:47 [exa] imagines an episode of Dallas ending with JR saying to unseen person "I know who put ⊒ there!"
18:22:27 <haskellbridge> <Bowuigi> I just use bidirectional/contextual typing and call it a day. Still waiting for the polymorphism inference paper for contextual typing tho
18:23:25 <EvanR> do you have a paper for that
18:23:50 <haskellbridge> <Bowuigi> For the first two things yes, the last one does not exist yet
18:24:59 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
18:25:55 <haskellbridge> <Bowuigi> https://dl.acm.org/doi/10.1145/3450952 bidirectional typing https://dl.acm.org/doi/10.1145/3674655 contextual typing
18:26:33 <haskellbridge> <Bowuigi> The respective talks on both explain the concepts better
18:27:28 <haskellbridge> <Bowuigi> Polymorphism inference with bidirectional typing is reasonably well studied. Kovacs' algorithm is pretty fast and good enough for a lot of use cases
18:28:01 <haskellbridge> <Bowuigi> Polymorphism inference with contextual typing is likely going to be faster and more powerful, but it has to exist first
18:29:33 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
18:30:43 target_i joins (~target_i@user/target-i/x-6023099)
18:30:52 gmg joins (~user@user/gehmehgeh)
18:30:56 <EvanR> if it exists, then it is fast
18:31:11 <EvanR> like tachyons
18:33:32 <haskellbridge> <Bowuigi> Yes, except that tachyons have to be discovered rather than thought about and problem solve'd into existence
18:34:23 <int-e> EvanR: I always admire people who have the energy to make a full trip around the Sun every single year.
18:35:31 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
18:36:05 × __monty__ quits (~toonn@user/toonn) (Ping timeout: 248 seconds)
18:40:42 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
18:41:21 <EvanR> :thonk:
18:42:00 __monty__ joins (~toonn@user/toonn)
18:42:03 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
18:42:44 gmg joins (~user@user/gehmehgeh)
18:47:01 × jco quits (~jco@78-70-217-44-no600.tbcn.telia.com) (Quit: leaving)
18:49:10 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
18:52:58 × img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
18:54:17 img joins (~img@user/img)
18:55:55 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
18:59:18 Guest51 joins (~Guest17@2001:1c00:a01:bc00:d043:d46d:298e:ed82)
19:00:05 × caconym quits (~caconym@user/caconym) (Quit: bye)
19:00:11 × Guest51 quits (~Guest17@2001:1c00:a01:bc00:d043:d46d:298e:ed82) (Client Quit)
19:00:48 caconym joins (~caconym@user/caconym)
19:03:06 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
19:05:23 × tabaqui quits (~tabaqui@167.71.80.236) (Ping timeout: 245 seconds)
19:06:18 <haskellbridge> <sm> most of us hitch a ride :)
19:06:46 Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
19:07:13 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:08:04 fp joins (~Thunderbi@hof1.kyla.fi)
19:08:11 × Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
19:08:28 Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
19:08:46 L29Ah joins (~L29Ah@wikipedia/L29Ah)
19:12:22 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
19:14:54 lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
19:15:08 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Client Quit)
19:23:00 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:23:20 <monochrom> hee hee
19:26:51 × forell_ quits (~forell@host-178-216-90-220.sta.tvknaszapraca.pl) (Ping timeout: 265 seconds)
19:27:42 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
19:36:39 forell joins (~forell@user/forell)
19:38:49 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:40:00 ljdarj joins (~Thunderbi@user/ljdarj)
19:41:05 <EvanR> the unit type (()) (oof) is called the "unit type". Do we have a proper name for the one inhabitant of the unit type, other than, annoyingly "unit"
19:41:56 ljdarj1 joins (~Thunderbi@user/ljdarj)
19:43:34 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
19:44:36 <monochrom> It is usually the other way round, the type is named after the values. E.g., why do we say "integer" for values of the Integer type?
19:44:39 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds)
19:44:39 ljdarj1 is now known as ljdarj
19:45:55 wroathe_ joins (~wroathe@static-68-235-46-107.cust.tzulo.com)
19:47:09 <EvanR> well types have come after values in history
19:47:21 rvalue- joins (~rvalue@user/rvalue)
19:47:55 <ski> "empty tuple"
19:48:14 <EvanR> ok then the value is more properly named ()
19:48:31 <ski> of course
19:48:45 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 260 seconds)
19:48:48 <EvanR> like (a,b) and the types A x B and ...
19:49:00 <EvanR> Unit
19:49:11 <ski> "product type","sum type","exponential type" -- not being named after values
19:49:40 ski doesn't really like the term "unit", in any case
19:50:10 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:50:54 ski was pondering, the other day, whether it would be nicer to say "type product"
19:52:17 rvalue- is now known as rvalue
19:52:24 wroathe_ parts (~wroathe@static-68-235-46-107.cust.tzulo.com) ()
19:55:09 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
19:59:41 × fp quits (~Thunderbi@hof1.kyla.fi) (Ping timeout: 244 seconds)
20:02:37 <monochrom> type product type >:)
20:05:33 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:09:04 AlexNoo_ joins (~AlexNoo@178.34.160.239)
20:09:31 × michalz_ quits (~michalz@185.246.207.203) (Remote host closed the connection)
20:10:29 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
20:11:52 × AlexZenon quits (~alzenon@178.34.162.245) (Ping timeout: 244 seconds)
20:12:46 × AlexNoo quits (~AlexNoo@178.34.162.245) (Ping timeout: 265 seconds)
20:12:53 × ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj)
20:13:22 AlexNoo_ is now known as AlexNoo
20:21:21 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:25:03 AlexZenon joins (~alzenon@178.34.160.239)
20:26:18 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
20:37:09 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:43:54 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
20:51:12 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:55:47 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
20:59:06 × tessier quits (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 244 seconds)
21:00:18 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds)
21:00:27 × Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
21:00:41 Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
21:01:18 tessier joins (~tessier@ip68-8-117-219.sd.sd.cox.net)
21:02:20 × koz quits (~koz@121.99.240.58) (Quit: ZNC 1.8.2 - https://znc.in)
21:04:38 koz joins (~koz@121.99.240.58)
21:05:18 × mcfrdy quits (~mcfrdy@user/mcfrdy) (Quit: quit)
21:05:33 rembo10_ joins (~rembo10@main.remulis.com)
21:05:37 mcfrdy joins (~mcfrdy@user/mcfrdy)
21:06:18 × rembo10 quits (~rembo10@main.remulis.com) (Read error: Connection reset by peer)
21:06:59 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:07:23 ljdarj joins (~Thunderbi@user/ljdarj)
21:12:04 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
21:16:17 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
21:22:29 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:26:44 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
21:27:28 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
21:30:39 <__monty__> But it works so similarly to an algebraic unit with sum and product types : /
21:38:15 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:40:07 <EvanR> I beg to differ after trying to implement the meaning of A * B * C * D
21:43:47 × krjst quits (~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
21:46:02 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
21:47:13 × Pixi quits (~Pixi@user/pixi) (Read error: Connection reset by peer)
21:47:21 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
21:47:44 Pixi joins (~Pixi@user/pixi)
21:55:09 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds)
21:58:16 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:01:13 × weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!)
22:01:30 weary-traveler joins (~user@user/user363627)
22:02:35 × tromp quits (~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf) (Quit: My iMac has gone to sleep. ZZZzzz…)
22:02:53 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
22:08:05 krjst joins (~krjst@2604:a880:800:c1::16b:8001)
22:08:10 × tv quits (~tv@user/tv) (Read error: Connection reset by peer)
22:14:03 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:15:20 ljdarj1 joins (~Thunderbi@user/ljdarj)
22:16:52 × krjst quits (~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
22:18:26 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
22:18:26 ljdarj1 is now known as ljdarj
22:20:20 <__monty__> Can you elaborate?
22:21:20 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
22:21:39 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:23:00 × chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds)
22:23:47 chiselfuse joins (~chiselfus@user/chiselfuse)
22:32:06 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:33:09 <EvanR> supposedly A * B * C * D = A * (B * C) * D = (A * B) * C * C
22:33:14 <EvanR> D
22:33:23 <EvanR> but not really xD
22:33:33 <EvanR> when you get down to brass tacks
22:33:59 <EvanR> (or ML)
22:37:09 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
22:43:40 tv joins (~tv@user/tv)
22:43:48 krjst joins (~krjst@2604:a880:800:c1::16b:8001)
22:47:52 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:52:48 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
22:53:31 Sgeo joins (~Sgeo@user/sgeo)
23:00:16 × krjst quits (~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
23:03:40 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:04:10 × ystael quits (~ystael@user/ystael) (Ping timeout: 272 seconds)
23:06:30 krjst joins (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48)
23:07:28 × krjst quits (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Client Quit)
23:08:09 krjst joins (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48)
23:08:42 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
23:09:25 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:11:44 × inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
23:14:30 × krjst quits (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye)
23:14:59 krjst joins (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48)
23:19:17 × Square quits (~Square4@user/square) (Ping timeout: 248 seconds)
23:19:28 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:19:42 inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net)
23:21:44 × polykernel quits (~polykerne@user/polykernel) (Ping timeout: 252 seconds)
23:23:46 polykernel joins (~polykerne@user/polykernel)
23:24:04 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
23:25:09 × inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
23:28:02 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
23:29:29 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
23:31:04 inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net)
23:31:53 Square2 joins (~Square@user/square)
23:33:45 × sprotte24 quits (~sprotte24@p200300d16f0bc1000c82a6b41033ea55.dip0.t-ipconnect.de) (Quit: Leaving)
23:35:15 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:35:49 × inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 248 seconds)
23:39:34 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
23:39:58 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
23:48:53 inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net)
23:51:04 merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:56:12 × inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
23:56:49 XZDX joins (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e)
23:57:02 inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net)
23:57:31 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
23:59:05 × XZDX quits (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Changing host)
23:59:05 XZDX joins (~xzdx@user/XZDX)

All times are in UTC on 2025-04-09.