Logs on 2024-09-08 (liberachat/#haskell)
| 00:00:03 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 00:00:16 | × | mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (Remote host closed the connection) |
| 00:02:06 | × | alexherbo2 quits (~alexherbo@2a02-8440-3114-792e-ddff-112f-809e-f52d.rev.sfr.net) (Remote host closed the connection) |
| 00:03:34 | → | mhatta joins (~mhatta@www21123ui.sakura.ne.jp) |
| 00:05:52 | × | acidjnk_new quits (~acidjnk@p200300d6e72cfb079527f265a4c52d61.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 00:11:06 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:15:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 00:21:01 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 00:21:53 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 00:22:18 | → | lambdaRule joins (~lambdaRul@node-1w7jr9phpv011s6crr0owcb3v.ipv6.telus.net) |
| 00:24:14 | <lambdaRule> | how to understand this list comprehension? |
| 00:24:14 | <lambdaRule> | arbitrary :: Arbitrary a => Gen a |
| 00:24:15 | <lambdaRule> | vector :: Arbitrary a => Int -> Gen [a] |
| 00:24:15 | <lambdaRule> | vector n = sequence [ arbitrary | i <- [1..n] ] |
| 00:24:29 | <lambdaRule> | what's the purpose of i? |
| 00:26:44 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 00:26:53 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:27:35 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:28:01 | → | sayola joins (~sayola@2a00:20:d307:80d8:cc05:636b:e7c8:3824) |
| 00:28:16 | <dmj`> | vector n = replicateM n arbitrary |
| 00:29:07 | <monochrom> | Yeah, i is "unused", but [1..n] causes the list to have length n. |
| 00:29:16 | <monochrom> | > [() | i <- [1..10]] |
| 00:29:18 | <lambdabot> | [(),(),(),(),(),(),(),(),(),()] |
| 00:30:22 | <geekosaur> | yeh, I'd've used replicateM instead of the list comprehension |
| 00:30:47 | <geekosaur> | > [() | _ <- [1..10]] |
| 00:30:49 | <lambdabot> | [(),(),(),(),(),(),(),(),(),()] |
| 00:30:51 | × | CiaoSen quits (~Jura@2a05:5800:459:6700:ca4b:d6ff:fec1:99da) (Ping timeout: 246 seconds) |
| 00:31:33 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 00:31:39 | <geekosaur> | @index replicateM |
| 00:31:39 | <lambdabot> | Control.Monad, Data.Sequence |
| 00:32:07 | <dmj`> | @src replicateM |
| 00:32:07 | <lambdabot> | replicateM n x = sequence (replicate n x) |
| 00:32:37 | <geekosaur> | I guess the only reason to use the list comp is to avoid the import. it doesn't even avoid a dependency, since Control.Monad is in base |
| 00:34:05 | <geekosaur> | also note that these examples are a little too oversimplified, since replicate is sufficient for them. but arbitrary requires replicateM, I think |
| 00:35:06 | <geekosaur> | (or sequence, as in your given code) |
| 00:36:25 | <geekosaur> | for that matter, it doesn't even avoid an import since they have to use sequence instead |
| 00:36:43 | <lambdaRule> | thanks for all the info. I searched list comprehension syntax but I haven't found anything. What should I have searched? |
| 00:37:15 | <lambdaRule> | this is some very old code that I |
| 00:37:25 | <lambdaRule> | reading, from QuickCheck |
| 00:37:29 | <geekosaur> | "Haskell list comprehension" (if you don't specify the language, you probably get Python's) |
| 00:40:49 | <geekosaur> | if you got a lot of "x for i in …" then you got Python's list comprehensions, which aren't quite as elaborate as Haskell's but do roughly the same thing |
| 00:42:41 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:43:24 | <dmj`> | :t enumFromTo |
| 00:43:25 | <lambdabot> | Enum a => a -> a -> [a] |
| 00:45:53 | → | spew joins (~spew@201.141.99.170) |
| 00:47:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 00:57:37 | → | troojg joins (~troojg@user/troojg) |
| 00:58:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:03:24 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 01:06:42 | × | jrm quits (~jrm@user/jrm) (Quit: ciao) |
| 01:08:12 | → | jrm joins (~jrm@user/jrm) |
| 01:08:40 | <justsomeguy> | Is there some trick for getting used to point-free syntax? It's been a few years and it still throws me off. |
| 01:09:09 | <EvanR> | if it makes no sense just don't do it |
| 01:09:21 | <justsomeguy> | I'm reading it in other peoples code. |
| 01:09:30 | <EvanR> | if it's more complicated than f 0 x . g "ok" . h, I'm out |
| 01:09:58 | × | abrar quits (~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) (Quit: WeeChat 4.2.2) |
| 01:10:06 | <justsomeguy> | Yeah, there are things like (sequence .) . fmap in this book I'm reading. |
| 01:10:11 | <EvanR> | gross |
| 01:10:22 | <geekosaur> | that's past the point where I throw in the towel, yeh |
| 01:10:30 | <EvanR> | @unpl (f .) . g |
| 01:10:30 | → | abrar joins (~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) |
| 01:10:30 | <lambdabot> | (\ x x0 -> f (g x x0)) |
| 01:10:33 | <geekosaur> | "too dotty" |
| 01:10:59 | <EvanR> | \x y -> sequence (fmap x y) |
| 01:11:04 | <justsomeguy> | I wonder if I can get that unpointfree in my IDE somehow. It's probably possible with the LSP. |
| 01:11:35 | <justsomeguy> | Hey, that rhymed! |
| 01:11:38 | <geekosaur> | someone would have to contribute a plugin based on the pointfree package |
| 01:12:10 | <geekosaur> | the main work is already done, just need to hook it in to HLS |
| 01:14:15 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:15:38 | <justsomeguy> | I'd like to look into writing that once I get out of the "can't code himself out of a wet paper bag" phase. |
| 01:19:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:23:58 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 01:27:19 | <EvanR> | :t (.).(.) |
| 01:27:19 | <lambdabot> | (b -> c) -> (a1 -> a2 -> b) -> a1 -> a2 -> c |
| 01:27:46 | <EvanR> | :t \f g x y -> (f .) . g |
| 01:27:46 | <lambdabot> | (b -> c) -> (a1 -> a2 -> b) -> p1 -> p2 -> a1 -> a2 -> c |
| 01:28:06 | <EvanR> | :t \x y f g -> (f .) . g |
| 01:28:06 | <lambdabot> | p1 -> p2 -> (b -> c) -> (a1 -> a2 -> b) -> a1 -> a2 -> c |
| 01:28:12 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 01:28:21 | <EvanR> | brain broke |
| 01:29:04 | <EvanR> | ok it's the same thing |
| 01:29:53 | × | yin quits (~z@user/zero) (Ping timeout: 248 seconds) |
| 01:30:02 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:30:13 | → | zero joins (~z@user/zero) |
| 01:34:58 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:44:40 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 01:45:14 | <morb> | hello |
| 01:45:49 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:49:24 | <geekosaur> | hello |
| 01:50:40 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 01:53:52 | × | ZharMeny quits (~ZharMeny@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
| 01:55:05 | × | lambdaRule quits (~lambdaRul@node-1w7jr9phpv011s6crr0owcb3v.ipv6.telus.net) (Quit: Client closed) |
| 02:01:37 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:02:05 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 02:02:32 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 02:02:33 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:02:34 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 02:03:32 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 02:03:50 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 02:05:04 | × | op_4 quits (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 02:05:34 | → | op_4 joins (~tslil@user/op-4/x-9116473) |
| 02:06:44 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:07:49 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 248 seconds) |
| 02:09:43 | × | troojg quits (~troojg@user/troojg) (Ping timeout: 264 seconds) |
| 02:17:23 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:22:16 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 02:25:24 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 02:31:59 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 02:33:11 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:33:42 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 02:37:54 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 02:48:19 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 02:48:57 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:50:08 | × | td_ quits (~td@i5387091F.versanet.de) (Ping timeout: 252 seconds) |
| 02:51:54 | → | td_ joins (~td@i53870918.versanet.de) |
| 02:53:34 | × | dpren_ quits (uid175126@id-175126.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:53:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:53:59 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 03:04:44 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:06:34 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 03:09:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 03:11:02 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 03:20:08 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:25:29 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 03:26:19 | × | sourcetarius quits (~sourcetar@user/sourcetarius) (Quit: zzz) |
| 03:28:16 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 03:28:32 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:29:35 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 03:33:18 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 03:34:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:35:35 | × | aforemny quits (~aforemny@2001:9e8:6cdd:cc00:e18:f1bd:8977:4cc7) (Ping timeout: 252 seconds) |
| 03:35:39 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 03:35:42 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 03:36:11 | → | aforemny joins (~aforemny@2001:9e8:6cfd:5300:79d5:7cd7:efda:1b62) |
| 03:36:21 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 03:37:35 | × | xff0x quits (~xff0x@2405:6580:b080:900:c1a4:8f81:9151:7c9c) (Ping timeout: 265 seconds) |
| 03:39:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 03:41:48 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 03:50:06 | → | xff0x joins (~xff0x@2405:6580:b080:900:c1a4:8f81:9151:7c9c) |
| 03:52:51 | → | Artea joins (~Lufia@artea.pt) |
| 03:52:51 | ← | Artea parts (~Lufia@artea.pt) () |
| 03:52:59 | → | Artea joins (~Lufia@artea.pt) |
| 03:53:00 | ← | Artea parts (~Lufia@artea.pt) () |
| 03:53:14 | → | Artea joins (~Lufia@artea.pt) |
| 03:53:14 | ← | Artea parts (~Lufia@artea.pt) () |
| 03:53:17 | → | Artea joins (~Lufia@artea.pt) |
| 03:53:17 | ← | Artea parts (~Lufia@artea.pt) () |
| 03:58:11 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 04:05:36 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:06:09 | → | weary-traveler joins (~user@user/user363627) |
| 04:10:15 | × | spew quits (~spew@201.141.99.170) (Quit: spew) |
| 04:10:20 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 04:16:02 | → | harveypwca joins (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) |
| 04:17:24 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 04:21:21 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:26:44 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 04:37:08 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:42:03 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 04:42:09 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 04:45:37 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 04:45:47 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 04:46:36 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 04:51:01 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 248 seconds) |
| 04:52:55 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:57:33 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 05:03:14 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 05:08:42 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:12:53 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 05:13:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 05:17:51 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 246 seconds) |
| 05:20:00 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 05:21:58 | × | harveypwca quits (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) (Quit: Leaving) |
| 05:24:30 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 05:24:31 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:31:42 | <probie> | I wouldn't use it outside of code golf, but `(f .) . g` isn't particularly scary. `(f .) . g` --> `\x -> (f .) (g x)` --> `\x -> f . g x` --> `\x y -> f (g x y)`. |
| 05:32:07 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 05:33:40 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:39:56 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:45:18 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:50:03 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 05:56:23 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 05:57:05 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:01:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 06:02:25 | × | sp1ff quits (~user@c-73-11-70-111.hsd1.wa.comcast.net) (Read error: Connection reset by peer) |
| 06:02:40 | → | sp1ff joins (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
| 06:05:27 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 06:11:49 | → | misterfish joins (~misterfis@84.53.85.146) |
| 06:12:38 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:12:52 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:17:40 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 06:19:00 | → | pharaoh joins (~Guest68@118-168-3-32.dynamic-ip.hinet.net) |
| 06:19:21 | <pharaoh> | Hello world |
| 06:19:49 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 06:21:06 | <pharaoh> | morb |
| 06:21:13 | <pharaoh> | you’re pinned down |
| 06:23:50 | <pharaoh> | morb |
| 06:23:58 | <pharaoh> | make you’re activatef |
| 06:24:08 | <pharaoh> | Activated |
| 06:27:56 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 06:28:39 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:30:39 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 246 seconds) |
| 06:30:40 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 06:35:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 06:35:21 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 276 seconds) |
| 06:39:38 | <pharaoh> | RMSBach |
| 06:39:42 | <pharaoh> | report you first |
| 06:39:45 | <pharaoh> | bsima- |
| 06:39:49 | <pharaoh> | report you the second |
| 06:39:52 | <pharaoh> | Batzy |
| 06:39:58 | <pharaoh> | you’re the third |
| 06:39:59 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:40:09 | <pharaoh> | you guys are blacklisted tromp |
| 06:40:23 | <pharaoh> | you are the fellow of Trump, aren’t you |
| 06:40:26 | <pharaoh> | tromp |
| 06:40:52 | <mauke> | @where ops |
| 06:40:52 | <lambdabot> | byorgey Cale conal copumpkin dcoutts dibblego dolio edwardk geekosaur glguy jmcarthur johnw mniip monochrom quicksilver shachaf shapr ski |
| 06:41:11 | <tromp> | Trump sucks |
| 06:41:21 | <pharaoh> | Then change your name |
| 06:41:32 | <pharaoh> | that’s not my or |
| 06:41:36 | <pharaoh> | problem |
| 06:41:49 | <pharaoh> | tromp response when received |
| 06:41:51 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 06:45:56 | <pharaoh> | tromp |
| 06:46:07 | <pharaoh> | She is against our ritual |
| 06:46:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:46:22 | <pharaoh> | face the consequences, poor merijn |
| 06:46:31 | <pharaoh> | you’re Japanese, ha? |
| 06:47:08 | <pharaoh> | merijn |
| 06:47:12 | <pharaoh> | are you literate? |
| 06:47:21 | × | pharaoh quits (~Guest68@118-168-3-32.dynamic-ip.hinet.net) (Quit: Client closed) |
| 06:47:37 | → | Guest68 joins (~Guest68@118-168-3-32.dynamic-ip.hinet.net) |
| 06:47:58 | <Guest68> | Ban you merijn |
| 06:48:03 | <Guest68> | bliminse |
| 06:48:05 | <Guest68> | bliminse |
| 06:48:08 | <Guest68> | Batzy |
| 06:48:13 | <Guest68> | bjs |
| 06:48:52 | × | Guest68 quits (~Guest68@118-168-3-32.dynamic-ip.hinet.net) (Client Quit) |
| 06:50:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 06:52:08 | × | sp1ff quits (~user@c-73-11-70-111.hsd1.wa.comcast.net) (Ping timeout: 252 seconds) |
| 06:54:47 | × | mesaoptimizer quits (~mesaoptim@user/PapuaHardyNet) (Ping timeout: 265 seconds) |
| 06:56:52 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 07:00:01 | × | tt123109783243 quits (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: The Lounge - https://thelounge.chat) |
| 07:02:04 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:02:13 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 248 seconds) |
| 07:03:12 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 07:03:18 | → | tt123109783243 joins (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) |
| 07:06:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 07:16:02 | → | mreh joins (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 07:17:51 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:18:36 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 07:22:56 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 07:23:05 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 244 seconds) |
| 07:27:39 | × | aljustiet quits (aljustiet@here.and.ready-to.party) (Changing host) |
| 07:27:39 | → | aljustiet joins (aljustiet@user/meow/aljustiet) |
| 07:31:27 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 07:31:30 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:36:30 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 07:36:53 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 255 seconds) |
| 07:47:17 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:50:13 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 07:52:16 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 07:56:40 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 08:01:01 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:03:05 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 08:06:12 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 08:07:56 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 08:11:13 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 08:11:35 | × | aljustiet quits (aljustiet@user/meow/aljustiet) (Quit: fBNC - https://bnc4free.com) |
| 08:15:08 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 08:15:39 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 08:18:54 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 08:23:42 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 08:25:37 | → | acidjnk_new joins (~acidjnk@p200300d6e72cfb75c990977c7caf1962.dip0.t-ipconnect.de) |
| 08:27:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:29:09 | × | youthlic quits (~Thunderbi@user/youthlic) (Ping timeout: 248 seconds) |
| 08:31:02 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 08:31:24 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 08:31:52 | → | mesaoptimizer joins (~mesaoptim@user/PapuaHardyNet) |
| 08:32:30 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 08:37:22 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 08:45:14 | × | Squared quits (~Square@user/square) (Ping timeout: 244 seconds) |
| 08:45:51 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 08:46:42 | → | euleritian joins (~euleritia@dynamic-176-006-133-246.176.6.pool.telefonica.de) |
| 08:47:41 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:48:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 08:52:03 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 245 seconds) |
| 08:53:26 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 08:58:45 | → | alexherbo2 joins (~alexherbo@2a02-8440-320a-9266-8566-4481-a134-9ff2.rev.sfr.net) |
| 09:00:46 | kitaleth | is now known as alethkit |
| 09:04:04 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 09:09:08 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 09:19:51 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 09:24:37 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 09:33:30 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 09:34:03 | × | youthlic quits (~Thunderbi@user/youthlic) (Ping timeout: 246 seconds) |
| 09:37:23 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:38:15 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 09:41:53 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 09:44:07 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 09:46:24 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 09:48:31 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 09:49:16 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 09:54:52 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 10:00:32 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 10:05:04 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 10:06:16 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 272 seconds) |
| 10:06:37 | × | euleritian quits (~euleritia@dynamic-176-006-133-246.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 10:06:55 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 10:10:07 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 10:13:08 | → | CiaoSen joins (~Jura@2a05:5800:459:c200:ca4b:d6ff:fec1:99da) |
| 10:15:28 | → | petrichor joins (~znc-user@user/petrichor) |
| 10:15:42 | × | petrichor quits (~znc-user@user/petrichor) (Remote host closed the connection) |
| 10:17:27 | × | CiaoSen quits (~Jura@2a05:5800:459:c200:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds) |
| 10:20:52 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 10:21:12 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 10:23:29 | <haskellbridge> | <thirdofmay18081814goya> what ordering can be given to the logics corresponding to the calculi in the lambda cube? |
| 10:25:32 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 10:26:04 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 10:31:58 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 10:35:44 | × | m1dnight quits (~christoph@d8D861908.access.telenet.be) (Quit: WeeChat 4.4.1) |
| 10:36:00 | → | m1dnight joins (~christoph@d8D861908.access.telenet.be) |
| 10:36:39 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 10:41:22 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 10:41:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 10:45:53 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 255 seconds) |
| 10:52:26 | → | mechap joins (~mechap@user/mechap) |
| 10:52:26 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 10:54:26 | <mechap> | I have just installed stack and all commands seem to run into that connection error http://0x0.st/XwnK.log |
| 10:55:07 | → | ash3en joins (~Thunderbi@2a01:c23:8d79:ee00:30a3:7625:9892:e350) |
| 10:55:33 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 10:57:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 11:01:19 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 264 seconds) |
| 11:04:05 | → | sourcetarius joins (~sourcetar@user/sourcetarius) |
| 11:07:05 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 265 seconds) |
| 11:08:13 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 11:09:36 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 11:12:02 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 11:12:15 | × | cheater quits (~Username@user/cheater) (Ping timeout: 276 seconds) |
| 11:13:12 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 11:16:15 | × | ash3en quits (~Thunderbi@2a01:c23:8d79:ee00:30a3:7625:9892:e350) (Ping timeout: 246 seconds) |
| 11:16:27 | → | ZharMeny joins (~ZharMeny@user/ZharMeny) |
| 11:24:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 11:28:32 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 11:29:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 11:33:13 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 11:33:54 | <haskellbridge> | <sm> Maybe report on #haskell-stack:matrix.org or check the issue tracker, I think there are some workarounds |
| 11:34:11 | × | crvs quits (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) (Read error: Connection reset by peer) |
| 11:37:21 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 11:39:53 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 255 seconds) |
| 11:52:08 | → | ash3en joins (~Thunderbi@2a01:c23:8d79:ee00:30a3:7625:9892:e350) |
| 11:55:19 | × | EvanR quits (~EvanR@user/evanr) (Ping timeout: 260 seconds) |
| 11:55:34 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 12:00:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 12:01:35 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 12:07:42 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 12:11:22 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 12:16:19 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 12:23:15 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:25:13 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 12:27:09 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 12:31:18 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 272 seconds) |
| 12:32:51 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 12:33:59 | × | ash3en quits (~Thunderbi@2a01:c23:8d79:ee00:30a3:7625:9892:e350) (Ping timeout: 260 seconds) |
| 12:37:15 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:42:57 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 12:43:59 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 12:47:53 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 12:48:50 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 12:49:55 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 12:51:13 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 245 seconds) |
| 13:03:54 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 13:04:15 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 13:08:15 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 13:10:44 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 13:11:08 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 13:14:31 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 13:19:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 13:19:40 | <haskellbridge> | <eldritchcookie> hello does anyone one know how pattern synonyms interacts with required type arguments? |
| 13:19:51 | × | ZharMeny quits (~ZharMeny@user/ZharMeny) (Remote host closed the connection) |
| 13:20:07 | <haskellbridge> | <eldritchcookie> i was unable to declare a pattern for proxy which requires a type argument |
| 13:24:27 | → | ZharMeny joins (~ZharMeny@user/ZharMeny) |
| 13:26:20 | <tomsmeding> | eldritchcookie: this seems to compile https://play.haskell.org/saved/4B5qc7k8 |
| 13:26:34 | <tomsmeding> | the bang pattern is of course unsatisfactory, but for Proxy it happens to be sufficient I think :p |
| 13:28:50 | <tomsmeding> | or I'm actually not sure -- the thing it's matching looks like a function |
| 13:28:55 | <tomsmeding> | anyway have to go, sorry |
| 13:30:18 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 13:31:19 | <haskellbridge> | <eldritchcookie> why does it accept if we have _ but not a constructor? |
| 13:33:15 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 13:34:39 | → | misterfish joins (~misterfis@84.53.85.146) |
| 13:35:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 13:37:01 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 13:38:37 | → | euleritian joins (~euleritia@dynamic-176-006-144-222.176.6.pool.telefonica.de) |
| 13:42:12 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 13:43:28 | × | tinwood quits (~tinwood@user/tinwood) (Remote host closed the connection) |
| 13:43:59 | → | divya joins (~user@202.170.201.47) |
| 13:44:42 | → | tinwood joins (~tinwood@general.default.akavanagh.uk0.bigv.io) |
| 13:44:42 | × | tinwood quits (~tinwood@general.default.akavanagh.uk0.bigv.io) (Changing host) |
| 13:44:42 | → | tinwood joins (~tinwood@user/tinwood) |
| 13:46:05 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 13:47:52 | → | cheater joins (~Username@user/cheater) |
| 13:48:18 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 13:50:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 13:55:10 | × | tinwood quits (~tinwood@user/tinwood) (Remote host closed the connection) |
| 13:55:31 | → | petrichor joins (~znc-user@user/petrichor) |
| 13:56:22 | → | tinwood joins (~tinwood@general.default.akavanagh.uk0.bigv.io) |
| 13:56:23 | × | tinwood quits (~tinwood@general.default.akavanagh.uk0.bigv.io) (Changing host) |
| 13:56:23 | → | tinwood joins (~tinwood@user/tinwood) |
| 14:01:52 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 14:03:21 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 14:05:44 | × | alexherbo2 quits (~alexherbo@2a02-8440-320a-9266-8566-4481-a134-9ff2.rev.sfr.net) (Remote host closed the connection) |
| 14:06:38 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 14:07:45 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 14:10:08 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 14:14:40 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 14:15:19 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 14:16:41 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:19:27 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 14:21:54 | → | EvanR joins (~EvanR@user/evanr) |
| 14:24:39 | <Leary> | eldritchcookie: GHC won't accept `data Req a where Req :: forall a -> Req a` either, so I rather doubt the pattern synonym equivalent is possible. |
| 14:24:49 | <Leary> | You may have to settle for `req :: forall k r. (forall (t :: k) -> r) -> (forall (t :: k). Proxy t -> r)`. |
| 14:25:53 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 14:26:15 | × | divya quits (~user@202.170.201.47) (Remote host closed the connection) |
| 14:30:49 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 14:33:34 | → | jinsun_ joins (~jinsun@user/jinsun) |
| 14:33:34 | × | jinsun quits (~jinsun@user/jinsun) (Killed (iridium.libera.chat (Nickname regained by services))) |
| 14:33:34 | jinsun_ | is now known as jinsun |
| 14:36:22 | → | ircbrowse_tom joins (~ircbrowse@user/tomsmeding/bot/ircbrowse-tom) |
| 14:36:24 | Server | sets mode +Cnt |
| 14:36:44 | × | tomsmeding quits (~tomsmedin@2a01:4f8:c0c:5e5e::2) (Quit: ZNC 1.9.1 - https://znc.in) |
| 14:37:23 | × | yahb2 quits (~yahb2@user/tomsmeding/bot/yahb2) (Remote host closed the connection) |
| 14:37:38 | → | weary-traveler joins (~user@user/user363627) |
| 14:37:48 | → | yahb2 joins (~yahb2@user/tomsmeding/bot/yahb2) |
| 14:37:48 | ChanServ | sets mode +v yahb2 |
| 14:37:53 | → | tomsmeding joins (~tomsmedin@2a01:4f8:c0c:5e5e::2) |
| 14:38:55 | → | ircbrowse_tom joins (~ircbrowse@user/tomsmeding/bot/ircbrowse-tom) |
| 14:38:57 | Server | sets mode +Cnt |
| 14:40:26 | → | AlexNoo joins (~AlexNoo@178.34.163.219) |
| 14:41:39 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 14:46:11 | × | sayola quits (~sayola@2a00:20:d307:80d8:cc05:636b:e7c8:3824) (Read error: Connection reset by peer) |
| 14:46:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 14:48:19 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 14:50:06 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 14:55:43 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 14:57:26 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 15:00:54 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 15:02:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 15:03:48 | → | briandaed joins (~root@185.234.210.211) |
| 15:12:18 | × | robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 15:12:26 | → | spew joins (~spew@201.141.99.170) |
| 15:13:13 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 15:18:30 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 15:18:30 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 15:21:22 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 15:27:03 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 15:27:12 | × | AlexZenon quits (~alzenon@178.34.163.219) (Ping timeout: 246 seconds) |
| 15:29:00 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 15:32:28 | → | AlexZenon joins (~alzenon@178.34.163.219) |
| 15:33:51 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 15:37:56 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 15:44:48 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 15:44:56 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 15:49:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 15:54:38 | → | alexherbo2 joins (~alexherbo@2a02-8440-320a-9266-699a-a628-8e15-b532.rev.sfr.net) |
| 15:58:27 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 16:00:35 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 16:05:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 16:16:23 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 16:17:07 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:19:54 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 244 seconds) |
| 16:20:45 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 16:25:20 | → | sayola joins (~sayola@2a00:20:d307:80d8:f1b7:2433:d516:6c1c) |
| 16:27:31 | × | sayola quits (~sayola@2a00:20:d307:80d8:f1b7:2433:d516:6c1c) (Client Quit) |
| 16:28:02 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 16:31:47 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 16:33:17 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 16:34:39 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:37:02 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 16:38:17 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 16:39:54 | × | mreh quits (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 252 seconds) |
| 16:40:51 | → | sam113102 joins (~sam@modemcable220.199-203-24.mc.videotron.ca) |
| 16:42:43 | × | sam113101 quits (~sam@modemcable220.199-203-24.mc.videotron.ca) (Ping timeout: 264 seconds) |
| 16:42:46 | sam113102 | is now known as sam113101 |
| 16:43:00 | → | simendsjo joins (~user@84.211.91.108) |
| 16:45:16 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 272 seconds) |
| 16:47:33 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 16:52:15 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 16:59:32 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 17:00:25 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:04:50 | × | simendsjo quits (~user@84.211.91.108) (Ping timeout: 252 seconds) |
| 17:06:33 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 17:09:49 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 17:10:48 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 17:11:09 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya STLC is propositional logic, system F is second-order intuitionistic logic, everything more powerful is higher order and above and the other ones are subsets |
| 17:12:10 | <dolio> | It's a sort of second order propositional logic which is not really widely studied. |
| 17:13:37 | <haskellbridge> | <Bowuigi> Yeah, I guess System Fω is somewhat similar to higher order logic given a similar kinding system |
| 17:13:52 | <haskellbridge> | <thirdofmay18081814goya> ty! |
| 17:14:13 | <haskellbridge> | <thirdofmay18081814goya> i do wonder why they call it second order propositional logic since it has no first order terms |
| 17:14:15 | <dolio> | Even Fω is not something that would be typically studied in logic. |
| 17:14:26 | <haskellbridge> | <thirdofmay18081814goya> first order quantification* |
| 17:15:11 | <Franciman> | becase you can quantify over subsets |
| 17:15:18 | <Franciman> | so you skip first order and directly go to second order |
| 17:15:25 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:15:30 | <Franciman> | but only have part of its power |
| 17:15:34 | <haskellbridge> | <Bowuigi> But the standard logics are Hilbert-style (axiomatic) proof systems. Everything lambda calculus related is Martin-Löf style (intuitionistic), everything lambda-mu calculus related is Gentzen-style (sequent) |
| 17:15:52 | <Franciman> | lambda-mu you mean fixpoints? |
| 17:15:59 | <Franciman> | and strategy logics? |
| 17:16:09 | <haskellbridge> | <Bowuigi> No, I mean the one with commands |
| 17:16:32 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: i think \lambda D is strictly more expressive than FOL from what i've read |
| 17:16:42 | <haskellbridge> | <thirdofmay18081814goya> I mean \lambda P |
| 17:17:00 | <haskellbridge> | <Bowuigi> Lambda-mu-mu tilde (λμμ̃) is slightly more popular I guess |
| 17:17:32 | <haskellbridge> | <thirdofmay18081814goya> Franciman: i.e. on a set-theoretic semantics? |
| 17:17:48 | <EvanR> | nice use of unicode there |
| 17:18:00 | <EvanR> | unicode is now vindicated |
| 17:18:04 | <haskellbridge> | <Bowuigi> https://www.pls-lab.org/en/Lambda_mu_calculus |
| 17:18:31 | × | euleritian quits (~euleritia@dynamic-176-006-144-222.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:18:48 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:19:14 | <Franciman> | ah okok nice |
| 17:20:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 17:21:00 | <dolio> | If you think about them as logics, then about the only interesting thing about System F is that you can define all the connectives properly in an intuitionistic logic from just implication and ∀. |
| 17:21:55 | <dolio> | Because you don't actually care about distinguishing all the distinct terms of each type, you only care about whether there is a term, more or less. |
| 17:23:24 | <dolio> | And if you're thinking classical logic, even that isn't interesting. |
| 17:23:36 | <haskellbridge> | <thirdofmay18081814goya> oh you can quantify over subsets, I get it now (semantics for \forall P where P is a relation symbol and a relation is a set of n-tuples) |
| 17:23:52 | × | arkeet quits (~arkeet@moriya.ca) (Quit: ZNC 1.8.2 - https://znc.in) |
| 17:29:15 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 17:29:34 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:31:00 | <monochrom> | Bowuigi: That is very interesting, thanks. (I once coded up lambda + callcc, but I conflated terms with commands, cont vars with lambda vars, i.e., I merely wrote a mini typed Scheme.) |
| 17:31:11 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:31:14 | → | arkeet joins (~arkeet@moriya.ca) |
| 17:32:06 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 17:34:29 | × | paddymahoney quits (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) (Ping timeout: 255 seconds) |
| 17:37:44 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 17:38:53 | → | mreh joins (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 17:39:43 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 17:40:54 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 246 seconds) |
| 17:43:19 | × | Inst quits (~Inst@user/Inst) (Read error: Connection reset by peer) |
| 17:43:22 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 17:44:30 | → | euphores joins (~SASL_euph@user/euphores) |
| 17:44:31 | → | paddymahoney joins (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) |
| 17:47:20 | → | Inst joins (~Inst@user/Inst) |
| 17:50:49 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:52:44 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 17:55:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 17:58:03 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 18:06:10 | × | alexherbo2 quits (~alexherbo@2a02-8440-320a-9266-699a-a628-8e15-b532.rev.sfr.net) (Remote host closed the connection) |
| 18:06:35 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:07:09 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 18:07:32 | → | alexherbo2 joins (~alexherbo@2a02-8440-320a-9266-cdc2-fc7e-a2a1-0b7e.rev.sfr.net) |
| 18:10:52 | × | alexherbo2 quits (~alexherbo@2a02-8440-320a-9266-cdc2-fc7e-a2a1-0b7e.rev.sfr.net) (Remote host closed the connection) |
| 18:11:56 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 18:12:23 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:12:28 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 245 seconds) |
| 18:13:01 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 18:18:21 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 18:22:24 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:23:21 | <dolio> | monochrom: You should read Compiling with Classical Connectives. |
| 18:24:47 | <monochrom> | I think I saw some Wadler talk doing that. |
| 18:27:20 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 18:37:18 | → | sp1ff joins (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
| 18:38:11 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:42:18 | <haskellbridge> | <thirdofmay18081814goya> https://kf8nh.com/_matrix/media/v3/download/matrix.org/QqQlQcBiTFxtPOXlThhqDrBp/image.png |
| 18:42:35 | <haskellbridge> | <thirdofmay18081814goya> do haskell type families satisfy this same definition from Martin-Lof dependent type theory? |
| 18:43:05 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 18:44:48 | <mauke> | doesn't this definition apply to all type constructors :: * -> *? |
| 18:45:20 | <mauke> | ah, no |
| 18:46:50 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 18:47:17 | <mauke> | this is more like B :: exists a. a -> * |
| 18:49:15 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 18:53:50 | <monochrom> | Haskell type families can do x::Type but not, for example, x::Int. |
| 18:53:58 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:55:03 | <monochrom> | OK people then start making "type-level Int", but that's just not the same. In dependent typing, the point is that x is a term-level Int. |
| 18:55:08 | → | troojg joins (~troojg@user/troojg) |
| 18:58:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 19:00:44 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 19:07:37 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 19:09:45 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:12:57 | × | oo_miguel quits (~Thunderbi@78.10.207.45) (Quit: oo_miguel) |
| 19:15:32 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 19:17:47 | <haskellbridge> | <Bowuigi> monochrom yeah the idea is similar but lambda-mu is more classical logic oriented |
| 19:19:41 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya only at the kind level (which is sort of dependent). At a type/value level that is dependent term abstraction (which haskell doesn't have, tho you can get close with singletons) |
| 19:20:13 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: ah I see! ty |
| 19:20:41 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 19:24:26 | <haskellbridge> | <Bowuigi> If A = Type then this corresponds to a type constructor, if A = Kind it corresponds to a kind abstraction (capital lambda at the type level). Dependent types just lift both of those restrictions (possibly adding an upper bound, eg. not allowing A to be larger than Kind) |
| 19:28:51 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 19:30:06 | → | Squared joins (~Square@user/square) |
| 19:32:12 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:33:51 | × | briandaed quits (~root@185.234.210.211) (Remote host closed the connection) |
| 19:33:57 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 19:37:18 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 19:47:54 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 19:47:59 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:49:09 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 19:52:03 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 245 seconds) |
| 19:52:47 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 19:52:53 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 19:55:30 | → | CiaoSen joins (~Jura@2a05:5800:459:c200:ca4b:d6ff:fec1:99da) |
| 20:00:04 | × | tabemann quits (~tabemann@2600:1700:7990:24e0:d4c9:6f74:4823:c124) (Remote host closed the connection) |
| 20:00:23 | → | tabemann joins (~tabemann@2600:1700:7990:24e0:f2d2:5bad:a45f:c15b) |
| 20:03:46 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:05:39 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 20:08:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 20:13:29 | → | hgolden_ joins (~hgolden@146.70.173.37) |
| 20:13:51 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 20:15:52 | × | hgolden quits (~hgolden@146.70.173.165) (Ping timeout: 252 seconds) |
| 20:16:21 | × | troojg quits (~troojg@user/troojg) (Ping timeout: 248 seconds) |
| 20:16:28 | AWizzArd_ | is now known as AWizzArd |
| 20:16:41 | × | AWizzArd quits (~code@gehrels.uberspace.de) (Changing host) |
| 20:16:41 | → | AWizzArd joins (~code@user/awizzard) |
| 20:28:49 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 20:30:11 | → | __monty__ joins (~toonn@user/toonn) |
| 20:32:45 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds) |
| 20:33:19 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 20:35:20 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:35:33 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 20:36:27 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 20:40:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 20:45:44 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 20:51:08 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:51:09 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 244 seconds) |
| 20:55:20 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:55:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 20:59:08 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:01:59 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 21:05:18 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 21:06:47 | → | Everything joins (~Everythin@109.162.122.37) |
| 21:06:55 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:08:28 | → | pavonia joins (~user@user/siracusa) |
| 21:11:49 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 21:11:58 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 21:12:28 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 21:12:31 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:15:35 | → | ash3en joins (~Thunderbi@146.70.124.222) |
| 21:16:37 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 248 seconds) |
| 21:17:18 | × | ash3en quits (~Thunderbi@146.70.124.222) (Client Quit) |
| 21:22:42 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:27:44 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 21:28:38 | → | mechap joins (~mechap@user/mechap) |
| 21:29:28 | <mechap> | could you please help me with stack ? http://0x0.st/XwFs.log |
| 21:31:33 | × | CiaoSen quits (~Jura@2a05:5800:459:c200:ca4b:d6ff:fec1:99da) (Ping timeout: 246 seconds) |
| 21:32:11 | <justsomeguy> | mechap: What stack resolver are you using? Maybe the snapshot no longer exists. |
| 21:32:47 | <justsomeguy> | (Since you're gettting a NoSuchBucket error.) |
| 21:34:09 | <mechap> | I deleted .stack and it seems to work now |
| 21:34:40 | <justsomeguy> | I think it was using a nightly snapshot, or some other snapshot that no longer exists. |
| 21:34:53 | <mechap> | that's possible |
| 21:38:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:43:38 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 21:43:57 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:45:24 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:46:27 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 21:46:28 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 21:49:33 | × | ZharMeny quits (~ZharMeny@user/ZharMeny) (Read error: Connection reset by peer) |
| 21:51:51 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 265 seconds) |
| 21:54:15 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:56:30 | <juri_> | is anyone actually using termonad? |
| 21:58:11 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:58:26 | <geekosaur> | I've heard of several people at least trying it out, but I personally never saw the point |
| 21:58:58 | <geekosaur> | there's already lots of VTE-based terminals out there, configuring one in Haskell doesn't seem to bring anything to the table IMO |
| 21:59:15 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 21:59:35 | <justsomeguy> | alacritty is the best terminal emulator |
| 21:59:49 | <EvanR> | fight fight fight |
| 22:00:13 | <EvanR> | xterm unfortunately can't be beaten |
| 22:00:24 | → | ZharMeny joins (~ZharMeny@user/ZharMeny) |
| 22:00:25 | <geekosaur> | urxvt 😛 |
| 22:00:38 | <EvanR> | urxvt is pretty good now |
| 22:00:41 | × | ZharMeny quits (~ZharMeny@user/ZharMeny) (Read error: Connection reset by peer) |
| 22:00:43 | × | mreh quits (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 264 seconds) |
| 22:00:45 | <geekosaur> | (that said, I actually use mate-terminal because I use mate) |
| 22:00:57 | → | ZharMeny joins (~ZharMeny@user/ZharMeny) |
| 22:01:52 | <juri_> | urxvt here too, but i'm looking at doing some ai .... stuff .... and am looking for a terminal emulator to add features to, so... |
| 22:04:10 | <EvanR> | AI in your terminal xD |
| 22:04:37 | <justsomeguy> | There are some experiments in that area, like https://www.warp.dev/ |
| 22:04:38 | <geekosaur> | ai yai yai |
| 22:04:42 | <EvanR> | make sure you have wireframe vector graphics support so you can draw an andros-like face |
| 22:05:10 | <justsomeguy> | Personally I would rather have a simple cli utility I can query for things with. |
| 22:07:05 | <justsomeguy> | What does lifting mean? I see it used in different contexts and find it confusing. |
| 22:08:02 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 22:08:09 | <juri_> | I'm doing something a bit different, but.. :D |
| 22:10:03 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:14:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 22:15:07 | <EvanR> | justsomeguy, have you seen fmap |
| 22:15:32 | <EvanR> | :: Functor f => (a -> b) -> (f a -> f b) |
| 22:16:03 | <EvanR> | it lifts any function to a corresponding function on f-things |
| 22:16:46 | <EvanR> | I've seen it in other contexts to means similar abstract structural moves |
| 22:17:03 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 22:17:35 | <monochrom> | Yes "lift" is an intuitive word, not a rigorous word. |
| 22:18:44 | <monochrom> | where intuition = without evident rational thought and inference. https://www.merriam-webster.com/dictionary/intuition |
| 22:18:47 | <justsomeguy> | So, in (=<<) :: Monad m => (a -> m b) -> m a -> m b, the a -> b is lifted to m a -> m b. What about the m b in (a -> m b? |
| 22:18:54 | <EvanR> | no |
| 22:19:06 | <EvanR> | I wouldn't call that lifting xD |
| 22:19:16 | <monochrom> | That one "lifts" a->mb to ma->mb. |
| 22:19:39 | <EvanR> | it's more like monad function application |
| 22:19:54 | <monochrom> | Or maybe it's demotion? Because contravariant something something? |
| 22:20:06 | <EvanR> | if anything gets actually applied to a function, all the cool words go out the window xD |
| 22:20:09 | <EvanR> | like composition |
| 22:20:23 | <EvanR> | you hear that elixir people! |
| 22:20:32 | <EvanR> | applying is not function composition |
| 22:21:00 | <monochrom> | Heh |
| 22:21:42 | → | ZharMeny` joins (~ZharMeny@user/ZharMeny) |
| 22:21:56 | <EvanR> | a "lifted type" is, unrelated it seems, a type with an additional bottom |
| 22:22:00 | <monochrom> | Remember how people look at the equivalent of "f . g $ x" and "f $ g $ x" and be like "so what is the difference between . and $" |
| 22:22:45 | <EvanR> | D: |
| 22:23:05 | <EvanR> | unboxed Int = ... -1 | 0 | 1 | 2 | 3 | ... |
| 22:23:05 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:23:10 | <EvanR> | Int = Int | bottom xD |
| 22:23:16 | <EvanR> | Int = unboxed Int | bottom xD |
| 22:23:24 | <EvanR> | lifted |
| 22:23:44 | × | ZharMeny quits (~ZharMeny@user/ZharMeny) (Ping timeout: 260 seconds) |
| 22:24:31 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 22:25:53 | <justsomeguy> | Does boxed mean there's a pointer involved, and unboxed mean there isn't? |
| 22:26:19 | <EvanR> | boxed means there's a box, which you access with a pointer |
| 22:26:27 | <EvanR> | you could access an unboxed value with a pointer to, if you want |
| 22:26:35 | <monochrom> | Yes but there is more. boxed is heap-allocated. |
| 22:27:23 | <EvanR> | unboxed values are scattered loose |
| 22:27:45 | <EvanR> | or confusingly, packed into an unboxed array |
| 22:27:53 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 22:28:20 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:30:48 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 245 seconds) |
| 22:32:47 | <monochrom> | More confusingly, that array itself is boxed (because heap) but unlifted (because no bottom). >:) |
| 22:33:11 | ZharMeny` | is now known as ZharMeny |
| 22:35:16 | <haskellbridge> | <thirdofmay18081814goya> anyone got good references about designing applications as a consequence of type-level reasoning? |
| 22:35:33 | <haskellbridge> | <thirdofmay18081814goya> algebra-driven design is about this, no? |
| 22:38:52 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:42:01 | <justsomeguy> | thirdofmay: I came across this book but haven't read it yet (it's over my head) https://thinkingwithtypes.com/ |
| 22:42:41 | <haskellbridge> | <thirdofmay18081814goya> nice! i'll give it a read, ty |
| 22:43:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 22:45:00 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 22:53:19 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 22:54:39 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:54:54 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 22:54:59 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 22:56:23 | <justsomeguy> | I have to admit that even though I like the idea of preventing more errors throught the type system I really dread the thought of working on a complicated code base that does type-level stuff. |
| 22:57:05 | <haskellbridge> | <thirdofmay18081814goya> imo it's less about safety and more about compositionality/modularity of design |
| 22:57:13 | <haskellbridge> | <thirdofmay18081814goya> although safety is nice too |
| 22:59:17 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 22:59:38 | <EvanR> | business requirements are not well-typed |
| 22:59:46 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Ping timeout: 252 seconds) |
| 22:59:51 | <justsomeguy> | The main issue for me is that it's a huge time investment to understand such a design well enough to contribute to it. |
| 23:00:14 | <justsomeguy> | But I'm also not an experienced programmer, more of a sysadmin, and I'm a little out of my element where Haskell is concerned. |
| 23:01:07 | <geekosaur> | you can get there |
| 23:01:23 | <geekosaur> | <-- ex-sysadmin (retired/disability) |
| 23:03:14 | × | xff0x quits (~xff0x@2405:6580:b080:900:c1a4:8f81:9151:7c9c) (Ping timeout: 260 seconds) |
| 23:05:04 | → | troojg joins (~troojg@user/troojg) |
| 23:05:56 | → | xff0x joins (~xff0x@2405:6580:b080:900:64f3:44bc:1e36:4a59) |
| 23:08:15 | <monochrom> | I don't use type-level design. I use Jackson Structured Design, which is type-driven but actually gets things done cleanly. It takes the view that a [abstract] type is specified by which operations you want it to support, so you ask yourself that question first, and not jump into implementation prematurely. |
| 23:10:13 | <haskellbridge> | <thirdofmay18081814goya> monochrom: https://en.wikipedia.org/wiki/Jackson_structured_programming this? |
| 23:10:22 | <monochrom> | There are some old FP papers actually doing that (without calling it that). For example the Wadler pretty-printing paper. They call it "algebra" instead, because if you have a [abstract] type and a bunch of operations, that's an algebra. |
| 23:10:26 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:13:14 | <justsomeguy> | monochrom: This one: https://en.wikipedia.org/wiki/Jackson_structured_programming ? |
| 23:13:24 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 23:13:30 | <justsomeguy> | lol, nevermind, definitely not that one |
| 23:15:01 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 248 seconds) |
| 23:15:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 23:15:11 | <monochrom> | Or maybe I have a beautified memory of it. |
| 23:17:06 | × | acidjnk_new quits (~acidjnk@p200300d6e72cfb75c990977c7caf1962.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 23:22:56 | → | morb joins (~morb@108.41.100.120) |
| 23:24:58 | <monochrom> | Maybe https://en.wikipedia.org/wiki/Jackson_system_development instead. I'll [mis]interpret "identifies the entities in the system, the actions they perform" as what I said above. >:) |
| 23:26:13 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:26:41 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 23:30:28 | × | tstat quits (~tstat@user/tstat) (Quit: ZNC 1.8.2 - https://znc.in) |
| 23:31:01 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 23:31:59 | × | morb quits (~morb@108.41.100.120) (Ping timeout: 260 seconds) |
| 23:37:25 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 248 seconds) |
| 23:42:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:47:04 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:47:10 | → | morb joins (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 23:50:24 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 23:51:33 | × | morb quits (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 246 seconds) |
| 23:56:48 | × | xff0x quits (~xff0x@2405:6580:b080:900:64f3:44bc:1e36:4a59) (Ping timeout: 246 seconds) |
| 23:57:46 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:57:57 | → | xff0x joins (~xff0x@2405:6580:b080:900:5825:9cdb:90f7:52b0) |
All times are in UTC on 2024-09-08.