Home liberachat/#haskell: Logs Calendar

Logs on 2024-02-11 (liberachat/#haskell)

00:00:22 × motherfsck quits (~motherfsc@user/motherfsck) (Ping timeout: 276 seconds)
00:00:52 <energizer> (a,b) having length but (a,b,c) not having it makes me think (a,b) isnt quite the 2-tuple, it's really a separate Pair type
00:01:17 <ncf> Foldable is just the "getter" half of Traversable
00:01:34 <ski> a pair is a `2'-tuple
00:01:49 × gooba quits (~gooba@90-231-13-185-no3430.tbcn.telia.com) (Remote host closed the connection)
00:02:26 <energizer> why would a 2 tuple have length but a 3 tuple not. no i think (a,b) is Pair
00:02:58 → gooba joins (~gooba@90-231-13-185-no3430.tbcn.telia.com)
00:03:50 <energizer> which is more like a single element k-v map
00:04:08 <monochrom> Um is this the "Pair vs APair" debate again? >:)
00:04:09 <ski> it's just that further instances are not present
00:04:25 <yushyin> because no one bothered to implement the Foldable instance
00:05:17 <ncf> you could have instances for n-tuples applied to n - 1 type parameters, and they would all have length constantly 1
00:08:37 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds)
00:09:58 <ski> % length $(return (TupE [Just (LitE (IntegerL 42))]))
00:09:58 <yahb2> 1
00:10:36 <ncf> uh
00:10:40 <ncf> is that Solo?
00:10:43 <ski> yes
00:10:54 <ski> % :t $(return (TupE [Just (LitE (IntegerL 42))]))
00:10:54 <yahb2> $(return (TupE [Just (LitE (IntegerL 42))])) :: Num a => Solo a
00:11:02 <geekosaur> "it's really a separate Pair type" --- that's how tuples work in Haskell
00:11:09 <geekosaur> they are not funny-looking lists
00:11:13 × yoo quits (~yo0O0o@user/mobivme) (Ping timeout: 264 seconds)
00:12:12 <geekosaur> they are anonymous product types
00:12:25 <geekosaur> (or "record types" if you prefer)
00:13:19 <monochrom> I think there are people out there who insist "product types" because they make a big fuss about "record types" having field names. :)
00:13:32 × azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds)
00:13:53 <monochrom> I was very surprised but they totally said "they are different!"
00:14:02 → rvalue joins (~rvalue@user/rvalue)
00:15:23 <ski> record types are labelled product types. tuple types are positional product types
00:15:36 <energizer> `length (Person "alice" 25 "main")` doesnt work tho
00:15:59 <monochrom> OK I guess there is a natural way to give a subtyping system to record types and we don't do it to tuple types.
00:16:03 <ski> because there's no `Foldable' instance, for that type
00:16:09 <geekosaur> it could if you provided a Foldable instance for it; most people don't
00:17:01 <ncf> that doesn't look functorial
00:17:04 <ski> tuple types, in SML, are merely record types, whose field names/labels are all positive integers up to the number of components
00:18:29 <monochrom> You can always map (x,y,z) to ((x,y),z) and then you can enjoy Foldable methods.
00:21:03 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
00:21:52 × waleee quits (~waleee@176.10.144.38) (Ping timeout: 268 seconds)
00:23:48 → EvanR joins (~EvanR@user/evanr)
00:33:20 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds)
00:34:25 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
00:40:30 <EvanR> > print(x)
00:40:31 <lambdabot> <IO ()>
00:53:36 → bilegeek joins (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13)
00:57:01 × Square quits (~Square@user/square) (Ping timeout: 268 seconds)
01:01:11 <monochrom> You're pretty late for print(x). :)
01:13:35 <EvanR> figured
01:15:08 → mjs2600 joins (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net)
01:15:13 × mjs2600_ quits (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) (Read error: Connection reset by peer)
01:15:46 × tessier quits (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 276 seconds)
01:17:01 → tessier joins (~treed@ip72-220-57-194.sd.sd.cox.net)
01:22:02 × tessier quits (~treed@ip72-220-57-194.sd.sd.cox.net) (Ping timeout: 252 seconds)
01:23:15 → tessier joins (~treed@ec2-184-72-149-67.compute-1.amazonaws.com)
01:25:00 × Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving)
01:46:19 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds)
01:46:25 → Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
01:47:17 × pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds)
01:47:47 Lord_of_Life_ is now known as Lord_of_Life
01:53:53 → falafel joins (~falafel@141.156.241.57)
01:54:36 → [_] joins (~itchyjunk@user/itchyjunk/x-7353470)
01:58:01 × [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 264 seconds)
02:07:01 × Tuplanolla quits (~Tuplanoll@91-159-68-95.elisa-laajakaista.fi) (Quit: Leaving.)
02:12:38 × mulk quits (~mulk@pd9514242.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
02:13:47 → mulk joins (~mulk@p5b112899.dip0.t-ipconnect.de)
02:18:49 × otto_s quits (~user@p5b04400d.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
02:20:00 → otto_s joins (~user@p4ff27640.dip0.t-ipconnect.de)
02:22:35 → motherfsck joins (~motherfsc@user/motherfsck)
02:38:07 → Feuermagier joins (~Feuermagi@user/feuermagier)
02:47:38 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
02:50:16 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit)
03:05:03 × op_4 quits (~tslil@user/op-4/x-9116473) (Remote host closed the connection)
03:05:31 → op_4 joins (~tslil@user/op-4/x-9116473)
03:08:32 × mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.8.2+deb4+b2 - https://znc.in)
03:11:21 → mhatta joins (~mhatta@www21123ui.sakura.ne.jp)
03:16:11 × falafel quits (~falafel@141.156.241.57) (Ping timeout: 264 seconds)
03:33:29 × td_ quits (~td@i53870917.versanet.de) (Ping timeout: 252 seconds)
03:35:17 → td_ joins (~td@i5387093C.versanet.de)
03:45:18 × bilegeek quits (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13) (Quit: Leaving)
03:49:29 × jargon quits (~jargon@157.sub-174-205-162.myvzw.com) (Remote host closed the connection)
03:54:20 → falafel joins (~falafel@141.156.241.57)
04:08:49 × falafel quits (~falafel@141.156.241.57) (Ping timeout: 264 seconds)
04:21:35 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
04:39:52 → Guest30 joins (~Guest57@2405:201:12:3dae:f726:6f38:f016:3459)
04:40:07 <Guest30> @free fmap :: (a -> b) -> f a -> f b
04:40:07 <lambdabot> Extra stuff at end of line
04:40:55 <Guest30> @free fmap :: (a -> b) -> F a -> F b
04:40:55 <lambdabot> g . h = k . f => $map_F g . fmap h = fmap k . $map_F f
04:41:24 <Guest30> @free pure :: a -> F a
04:41:24 <lambdabot> $map_F f . pure = pure . f
04:42:00 <Guest30> @free bind :: F a -> (a -> F b) -> F b
04:42:00 <lambdabot> $map_F g . h = k . f => $map_F g (bind x h) = bind ($map_F f x) k
04:47:39 → aforemny_ joins (~aforemny@i59F516F6.versanet.de)
04:47:43 × aforemny quits (~aforemny@2001:9e8:6cfa:c300:ed38:1b4d:cf6e:9f22) (Ping timeout: 260 seconds)
05:01:54 → fansly joins (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e)
05:01:57 × fansly quits (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Client Quit)
05:02:07 → fansly joins (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e)
05:03:08 × mulk quits (~mulk@p5b112899.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
05:05:10 → mulk joins (~mulk@p5b2dcdd6.dip0.t-ipconnect.de)
05:05:54 → bilegeek joins (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13)
05:10:01 × JordiGH quits (~jordi@user/jordigh) (Ping timeout: 264 seconds)
05:12:04 → qqq joins (~qqq@92.43.167.61)
05:12:12 → azimut joins (~azimut@gateway/tor-sasl/azimut)
05:16:37 × fansly quits (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Ping timeout: 264 seconds)
05:18:35 → fansly joins (~fansly@103.3.221.176)
05:20:22 → szkl joins (uid110435@id-110435.uxbridge.irccloud.com)
05:35:54 × Guest30 quits (~Guest57@2405:201:12:3dae:f726:6f38:f016:3459) (Quit: Client closed)
05:38:36 × fansly quits (~fansly@103.3.221.176) (Read error: Connection reset by peer)
05:39:56 → fansly joins (~fansly@182.2.141.93)
05:43:00 × fansly quits (~fansly@182.2.141.93) (Read error: Connection reset by peer)
05:43:18 → fansly joins (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e)
05:58:43 → Guest67 joins (~Guest57@49.36.11.6)
05:59:06 <Guest67> @free filter :: (a -> Boolean) -> F a -> F a
05:59:06 <lambdabot> $map_F f . filter (g . f) = filter g . $map_F f
06:01:16 <Guest67> @free safeExtract :: a -> F a -> a
06:01:16 <lambdabot> f . safeExtract x = safeExtract (f x) . $map_F f
06:02:02 <Guest67> @free unsafeExtract :: f a -> a
06:02:02 <lambdabot> Extra stuff at end of line
06:02:09 <Guest67> @free unsafeExtract :: F a -> a
06:02:10 <lambdabot> f . unsafeExtract = unsafeExtract . $map_F f
06:03:07 <Guest67> @free toEither :: e -> F a -> G e a
06:03:08 <lambdabot> Plugin `free' failed with: Sorry, this type is too difficult for me.
06:03:08 <lambdabot> CallStack (from HasCallStack):
06:03:08 <lambdabot> error, called at src/Lambdabot/Plugin/Haskell/Free/FreeTheorem.hs:296:31 in lambdabot-haskell-plugins-5.3-KdjsqvMFsLeLZemJqobWap:Lambdabot.Plugin.Haskell.Free.FreeTheorem
06:03:40 <Guest67> @free toEither :: b -> F a -> F b a
06:03:41 <lambdabot> Plugin `free' failed with: Sorry, this type is too difficult for me.
06:03:41 <lambdabot> CallStack (from HasCallStack):
06:03:41 <lambdabot> error, called at src/Lambdabot/Plugin/Haskell/Free/FreeTheorem.hs:296:31 in lambdabot-haskell-plugins-5.3-KdjsqvMFsLeLZemJqobWap:Lambdabot.Plugin.Haskell.Free.FreeTheorem
06:03:56 <Guest67> @free toEither :: b -> F a -> G b a
06:03:56 <lambdabot> Plugin `free' failed with: Sorry, this type is too difficult for me.
06:03:57 <lambdabot> CallStack (from HasCallStack):
06:03:57 <lambdabot> error, called at src/Lambdabot/Plugin/Haskell/Free/FreeTheorem.hs:296:31 in lambdabot-haskell-plugins-5.3-KdjsqvMFsLeLZemJqobWap:Lambdabot.Plugin.Haskell.Free.FreeTheorem
06:04:17 ← Guest67 parts (~Guest57@49.36.11.6) ()
06:04:37 × mulk quits (~mulk@p5b2dcdd6.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
06:08:51 × johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in)
06:16:40 × fansly quits (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Quit: Quit)
06:20:51 → fansly joins (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e)
06:23:18 → bzm3r joins (~bzm3r@d205-250-253-229.bchsia.telus.net)
06:37:15 → mulk joins (~mulk@pd95144c1.dip0.t-ipconnect.de)
06:41:01 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
06:41:57 × fansly quits (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Remote host closed the connection)
06:42:22 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
06:44:52 → RaspbellySwirl joins (~Raspbelly@host-213-235-142-6.ip.topnet.cz)
06:45:22 → fansly joins (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e)
06:50:45 × fansly quits (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Read error: Connection reset by peer)
06:50:55 → fansly joins (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e)
06:52:59 × fansly quits (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Remote host closed the connection)
06:55:26 → coot joins (~coot@89-69-206-216.dynamic.chello.pl)
07:02:56 → CrunchyFlakes joins (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
07:08:31 → fansly joins (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e)
07:11:49 × coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Remote host closed the connection)
07:12:07 → peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com)
07:12:18 → coot joins (~coot@89-69-206-216.dynamic.chello.pl)
07:12:30 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
07:12:40 → euleritian joins (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de)
07:13:00 × euleritian quits (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) (Read error: Connection reset by peer)
07:13:18 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
07:19:46 → johnw joins (~johnw@69.62.242.138)
07:20:00 × johnw quits (~johnw@69.62.242.138) (Remote host closed the connection)
07:21:40 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
07:22:35 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
07:24:36 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
07:25:06 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
07:30:18 × coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot)
07:32:25 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
07:33:00 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
07:36:59 × qqq quits (~qqq@92.43.167.61) (Remote host closed the connection)
07:39:25 × peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
07:40:25 → johnw joins (~johnw@69.62.242.138)
07:44:24 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
07:44:53 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
07:44:58 → gcdsefhu^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net)
07:45:39 × L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 256 seconds)
07:49:51 → L29Ah joins (~L29Ah@wikipedia/L29Ah)
07:50:21 × trev quits (~trev@user/trev) (Ping timeout: 260 seconds)
07:52:07 → trev joins (~trev@109-252-43-67.nat.spd-mgts.ru)
07:55:08 × trev quits (~trev@109-252-43-67.nat.spd-mgts.ru) (Client Quit)
07:56:03 → trev joins (~trev@109-252-43-67.nat.spd-mgts.ru)
07:56:29 × trev quits (~trev@109-252-43-67.nat.spd-mgts.ru) (Changing host)
07:56:29 → trev joins (~trev@user/trev)
07:57:26 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
07:58:08 → euleritian joins (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de)
07:58:30 × euleritian quits (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) (Read error: Connection reset by peer)
07:58:55 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
08:00:07 × tt1231 quits (~tt123@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: The Lounge - https://thelounge.chat)
08:00:11 × Natch quits (~natch@92.34.7.158) (Remote host closed the connection)
08:00:14 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
08:00:37 × trev quits (~trev@user/trev) (Client Quit)
08:00:52 → trev joins (~trev@user/trev)
08:02:08 → tt1231 joins (~tt123@2603-6010-8700-4a81-219f-50d3-618a-a6ee.res6.spectrum.com)
08:02:41 × bilegeek quits (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13) (Quit: Leaving)
08:03:27 × gcdsefhu^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection)
08:05:29 → Natch joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se)
08:06:38 → acidjnk_new joins (~acidjnk@p200300d6e737e77464baf57332386b26.dip0.t-ipconnect.de)
08:35:49 × fansly quits (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Ping timeout: 264 seconds)
08:38:16 → fansly joins (~fansly@103.3.221.176)
08:38:49 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
08:39:19 → euleritian joins (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de)
08:41:03 → _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl)
08:41:46 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
08:52:04 × euleritian quits (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) (Ping timeout: 276 seconds)
08:52:57 → euleritian joins (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de)
08:55:48 → eb20 joins (~eb@41.189.245.59)
08:57:50 → rscastilho2024 joins (~rscastilh@189.61.140.215)
08:58:34 × fansly quits (~fansly@103.3.221.176) (Ping timeout: 276 seconds)
08:59:28 × rscastilho2024 quits (~rscastilh@189.61.140.215) (Remote host closed the connection)
08:59:47 <eb20> anyone her use hugs?
09:00:28 → fansly joins (~fansly@182.2.165.191)
09:10:01 <kaol> Yes. Recently, unlikely. I last did anything with it when ghc 6 was new.
09:10:29 × euleritian quits (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
09:10:46 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
09:16:46 × elkcl quits (~elkcl@broadband-95-84-226-240.ip.moscow.rt.ru) (Ping timeout: 276 seconds)
09:16:49 → pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
09:20:50 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
09:25:13 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds)
09:27:56 × fansly quits (~fansly@182.2.165.191) (Read error: Connection reset by peer)
09:29:57 → euleritian joins (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de)
09:31:26 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
09:31:48 → Tuplanolla joins (~Tuplanoll@91-159-68-95.elisa-laajakaista.fi)
09:32:41 × euleritian quits (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
09:32:59 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
09:33:32 <mauke> there was someone on matrix who still uses it
09:33:49 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
09:35:32 → gmg joins (~user@user/gehmehgeh)
09:37:16 × bzm3r quits (~bzm3r@d205-250-253-229.bchsia.telus.net) (Ping timeout: 250 seconds)
09:42:31 × todi quits (~todi@p4fd1aef3.dip0.t-ipconnect.de) (Quit: ZNC - https://znc.in)
09:52:29 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds)
09:52:34 → todi joins (~todi@p4fd1aef3.dip0.t-ipconnect.de)
09:52:54 → euleritian joins (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de)
09:54:12 × megaTherion quits (~therion@unix.io) (Quit: ZNC 1.8.2 - https://znc.in)
09:55:15 × szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
10:01:02 → megaTherion joins (~therion@unix.io)
10:01:47 × euleritian quits (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
10:02:05 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
10:02:53 × acidjnk_new quits (~acidjnk@p200300d6e737e77464baf57332386b26.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
10:06:06 × tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz)
10:09:56 → alexherbo2 joins (~alexherbo@33.134.22.93.rev.sfr.net)
10:15:55 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 276 seconds)
10:18:04 × megaTherion quits (~therion@unix.io) (Remote host closed the connection)
10:21:22 → megaTherion joins (~therion@unix.io)
10:23:45 → michalz joins (~michalz@185.246.207.205)
10:36:49 → coot joins (~coot@89-69-206-216.dynamic.chello.pl)
10:36:58 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
10:40:08 × alexherbo2 quits (~alexherbo@33.134.22.93.rev.sfr.net) (Remote host closed the connection)
10:40:29 → alexherbo2 joins (~alexherbo@2a02-8440-3340-93db-fd9e-1a08-c9e1-df21.rev.sfr.net)
10:58:57 → Lycurgus joins (~georg@user/Lycurgus)
11:18:39 → sroso joins (~sroso@user/SrOso)
11:20:59 → infinity0 joins (~infinity0@pwned.gg)
11:24:34 → infinity0_ joins (~infinity0@pwned.gg)
11:24:35 infinity0 is now known as Guest7389
11:24:35 infinity0_ is now known as infinity0
11:25:37 × Guest7389 quits (~infinity0@pwned.gg) (Ping timeout: 264 seconds)
11:27:20 × Axman6 quits (~Axman6@user/axman6) (Remote host closed the connection)
11:33:12 → mmhat joins (~mmh@p200300f1c740af4dee086bfffe095315.dip0.t-ipconnect.de)
11:38:06 × sroso quits (~sroso@user/SrOso) (Quit: Leaving :))
11:39:12 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
11:51:43 → yotta joins (~cha0s@14.191.144.106)
11:53:01 × mmhat quits (~mmh@p200300f1c740af4dee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.2.1)
11:56:23 → Square joins (~Square@user/square)
11:58:13 <yotta> When passing multiple MutableByteArray# to a C function, it is correct to use Array# MutableByteArray# or MutableArray# MutableByteArray# ? The C function writes to the bytearrays.
12:01:25 × mrmr155334 quits (~mrmr@user/mrmr) (Quit: Bye, See ya later!)
12:01:59 × azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection)
12:03:13 → azimut joins (~azimut@gateway/tor-sasl/azimut)
12:04:57 <int-e> yotta: oh https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/ffi.html actually has an example of this (look for sum_first)... you need to poke into RTS internals
12:05:36 → mrmr155334 joins (~mrmr@user/mrmr)
12:05:44 → qqq joins (~qqq@92.43.167.61)
12:08:34 <int-e> (For mutation, use Array# MutableByteArray#)
12:10:29 <yotta> thank
12:31:59 × Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving)
12:35:01 → yoo joins (~yo0O0o@130.105.162.162)
12:46:59 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
12:47:20 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
12:58:26 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
13:03:54 → Axman6 joins (~Axman6@user/axman6)
13:05:31 → fbytez_ joins (~uid@user/fbytez)
13:08:00 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
13:08:41 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
13:10:36 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
13:11:49 × EvanR quits (~EvanR@user/evanr) (Read error: Connection reset by peer)
13:11:59 → EvanR joins (~EvanR@user/evanr)
13:12:44 → Midjak joins (~MarciZ@82.66.147.146)
13:14:20 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
13:22:10 × eb20 quits (~eb@41.189.245.59) (Ping timeout: 250 seconds)
13:25:36 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
13:33:05 × alexherbo2 quits (~alexherbo@2a02-8440-3340-93db-fd9e-1a08-c9e1-df21.rev.sfr.net) (Remote host closed the connection)
13:48:04 → __monty__ joins (~toonn@user/toonn)
13:48:49 × average quits (uid473595@user/average) (Quit: Connection closed for inactivity)
13:54:41 → [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470)
13:54:56 → alexherbo2 joins (~alexherbo@2a02-8440-3341-cfe3-0966-2558-23d8-f964.rev.sfr.net)
13:58:20 × [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds)
14:04:00 <haskellbridge> <J​ade> I'm often seeing an idiom along the line of `length [ () | pat <- some_list ]` where the pattern match would be identical to an `==`. Would it not make sense to have something like `count :: Eq a => a -> [a] -> Int` for these?
14:04:08 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
14:04:09 <haskellbridge> <J​ade> in base specifically*
14:05:05 <haskellbridge> <J​ade> It could even be `count :: (a -> Bool) -> [a] -> Int`
14:05:32 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
14:06:14 → elkcl joins (~elkcl@broadband-95-84-226-240.ip.moscow.rt.ru)
14:06:27 <Axman6> the pattern match is likely to be more efficient, and that's not quite the same thing - the code you pasted counts how many items match a geven pattern, not what's equal to another value
14:07:04 <haskellbridge> <J​ade> yeah I saw a lot of those with strings and the "pattern" being a character literal
14:07:44 <haskellbridge> <J​ade> and it always takes a second or so to click, but with a `count 'x' list` that would be a lot easier
14:07:46 <ski> > replicateM 2 (Const (Sum 7))
14:07:48 <lambdabot> Const (Sum {getSum = 14})
14:07:53 <haskellbridge> <J​ade> s/list/string
14:08:09 <ski> > replicateM 2 (Const (Product 7))
14:08:11 <lambdabot> Const (Product {getProduct = 49})
14:08:11 <ski> i guess
14:09:18 <haskellbridge> <J​ade> wait why is that happening
14:09:31 <haskellbridge> <J​ade> Oh I see
14:09:53 <int-e> https://wiki.haskell.org/Fairbairn_threshold is a factor here
14:10:45 <haskellbridge> <J​ade> The Monad instances of these newtype wrappers for Monoids are the same as the identity monad
14:12:05 <ncf> Applicative, not Monad (Const k isn't a monad unless k is ())
14:12:14 <ncf> :t replicateM
14:12:15 <lambdabot> Applicative m => Int -> m a -> m [a]
14:13:15 × driib quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
14:14:04 <ncf> (and no, this isn't the identity applicative)
14:14:44 → JordiGH joins (~jordi@user/jordigh)
14:15:19 <ski> "No instance for (MonadFail (Const (Product Integer)))" :(
14:17:01 <ncf> can't MonadFail if it Fails to Monad
14:20:15 × Midjak quits (~MarciZ@82.66.147.146) (Read error: Connection reset by peer)
14:20:42 → MarciZ joins (~MarciZ@82.66.147.146)
14:21:42 <ski> exactly
14:26:37 <haskellbridge> <i​rregularsphere> ski: ...how exactly is it going to implement `String -> Product Integer` anyway
14:27:20 <haskellbridge> <i​rregularsphere> sorry, `fail :: forall a. String -> Const (Product Integer) a`
14:31:30 <haskellbridge> <i​rregularsphere> my best guess is to put a `Maybe` somewhere but I'm not sure
14:32:39 <haskellbridge> <i​rregularsphere> maybe `Compose Maybe (Const (Product Integer))`?
14:32:51 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
14:35:38 → driib joins (~driib@vmi931078.contaboserver.net)
14:38:05 <haskellbridge> <i​rregularsphere> nvm about the compose thing
14:40:27 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
14:42:04 → euleritian joins (~euleritia@77.22.252.56)
14:42:23 × euleritian quits (~euleritia@77.22.252.56) (Read error: Connection reset by peer)
14:43:02 → euleritian joins (~euleritia@77.22.252.56)
14:43:50 → acidjnk_new joins (~acidjnk@p5dd87f44.dip0.t-ipconnect.de)
14:45:14 <ncf> fail _ = Const mempty ?
14:45:18 <ncf> Fail isn't the problem, it's Monad
14:48:14 → Midjak joins (~MarciZ@82.66.147.146)
14:48:42 × MarciZ quits (~MarciZ@82.66.147.146) (Read error: Connection reset by peer)
14:50:59 <haskellbridge> <i​rregularsphere> Ah.
14:57:02 → fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c)
14:57:14 × JordiGH quits (~jordi@user/jordigh) (Ping timeout: 268 seconds)
15:01:01 × euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 264 seconds)
15:01:29 → euleritian joins (~euleritia@dynamic-176-006-191-101.176.6.pool.telefonica.de)
15:01:47 × pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 264 seconds)
15:03:33 → pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
15:13:34 × euleritian quits (~euleritia@dynamic-176-006-191-101.176.6.pool.telefonica.de) (Ping timeout: 268 seconds)
15:14:10 → euleritian joins (~euleritia@77.22.252.56)
15:18:49 × euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 276 seconds)
15:19:25 × Midjak quits (~MarciZ@82.66.147.146) (Read error: Connection reset by peer)
15:19:37 → euleritian joins (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de)
15:19:55 × euleritian quits (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
15:20:12 → euleritian joins (~euleritia@77.22.252.56)
15:20:29 → JordiGH joins (~jordi@user/jordigh)
15:21:04 <haskellbridge> <i​rregularsphere> If `Monad (Const (Product Integer))` were to ever happen, then `join`'s only expected behaviour is `id`, thus `xs >>= f = xs >>= (\x -> id (f x)) = xs >>= (\x -> return (f x) >>= id) = xs >>= (\x -> (return . f) x >>= id) = (xs >>= return . f) >>= id = (fmap f xs) >>= id = join (fmap f xs) = fmap f xs = xs`
15:21:09 → Midjak joins (~MarciZ@82.66.147.146)
15:23:18 <ncf> what?
15:23:19 <haskellbridge> <i​rregularsphere> (join's expected behaviour is id because join has type `Const (Product Integer) (Const (Product Integer) a) -> Const (Product Integer) a`, which is saying `\(Const x) -> ...`, in which it is most reasonable to be `\(Const x) -> Const x = id`
15:23:41 <haskellbridge> <i​rregularsphere> ncf: I fear that `xs >>= f = xs` for all `xs` and `f`.
15:24:08 <haskellbridge> <i​rregularsphere> ok gn
15:24:14 <ncf> "most reasonable" isn't a proof
15:25:01 <haskellbridge> <i​rregularsphere> fair
15:25:08 <ncf> you have to show that whatever you pick for join (which is a function m → m where m is a monoid), the laws can't be satisfied
15:26:00 <ncf> there are as many functions forall m. Monoid m => m → m as there are natural numbers, can you see why?
15:26:05 <haskellbridge> <i​rregularsphere> actually you can reverse define `xs >>= f = join (fmap f xs)` which all laws will automatically be satisfied
15:26:16 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
15:26:30 <haskellbridge> <i​rregularsphere> but `fmap f xs = xs` by definition
15:26:38 <haskellbridge> <i​rregularsphere> so `xs >>= f = join xs`
15:27:14 <ncf> yes, it's usually easier to reason about join than >>=
15:27:25 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
15:27:32 <haskellbridge> <i​rregularsphere> what i'm trying to point out is that
15:27:37 <haskellbridge> <i​rregularsphere> `f` is discarded
15:28:15 <ncf> sure
15:28:41 <haskellbridge> <i​rregularsphere> so with all definitions of `join`, `>>=` is already useless
15:29:20 <haskellbridge> <i​rregularsphere> yeah in my super long explanation you can omit last step
15:29:29 <haskellbridge> <i​rregularsphere> and apply `fmap f xs = xs`
15:29:40 <ski> irregularsphere : the point was to use refutable patterns, not `MonadFail' per se
15:30:06 <haskellbridge> <i​rregularsphere> (most of the blob of text is me proving `xs >>= f = join (fmap f xs)`)
15:30:10 × euleritian quits (~euleritia@77.22.252.56) (Read error: Connection reset by peer)
15:30:20 → euleritian joins (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de)
15:30:25 <ncf> that's the definition of >>=
15:30:40 × euleritian quits (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
15:30:41 <haskellbridge> <i​rregularsphere> ski: oh, huh
15:30:57 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
15:33:10 <haskellbridge> <i​rregularsphere> ncf: unfortunately it isn't like that in haskell source :( would like to push a pr though, but it's currently half past ten at night for me
15:33:20 × pastly quits (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 255 seconds)
15:33:24 <haskellbridge> <i​rregularsphere> gn everyone!
15:33:51 <ncf> ok if you take >>= as primitive and define join as _>>= id then you do have to prove that, but it should just be an application of naturality
15:34:15 <ncf> in particular there's no reason to involve return
15:34:25 → rscastilho2024 joins (~rscastilh@189.61.140.215)
15:34:45 <haskellbridge> <i​rregularsphere> `return` was simply part of my proof that `xs >>= f = join (fmap f xs)`
15:36:04 <ncf> i'm saying you don't need to mention return to prove that
15:36:12 × Midjak quits (~MarciZ@82.66.147.146) (Read error: Connection reset by peer)
15:36:45 → Midjak joins (~MarciZ@82.66.147.146)
15:36:46 <haskellbridge> <i​rregularsphere> different proofs same conclusion hehe
15:39:05 <haskellbridge> <i​rregularsphere> yea what i'm trying to detail is that no matter how hard you try while adhering to laws you'd always do `xs >>= f` = `xs >>= id` in some way or another
15:40:17 → pastly joins (~pastly@gateway/tor-sasl/pastly)
15:40:31 <haskellbridge> <i​rregularsphere> (the case for trying to define `Monad (Const a)` by the way)
15:41:27 <ski> i've before pondered having operations like `forall a b. m a -> (a -> n b) -> n b'. e.g. `m = State sr',`n = Reader sr', or `m = []',`n = Count' (`Const (Product Integer))' above)
15:41:52 <haskellbridge> <i​rregularsphere> *meanwhile me saying "gn" 11 minutes ago
15:42:29 <ski> btw, your `id' has type `(forall a. Const c a) -> (forall a. Const c a)'
15:42:41 <haskellbridge> <i​rregularsphere> yup
15:42:47 <haskellbridge> <i​rregularsphere> what's wrong about that
15:42:51 × Midjak quits (~MarciZ@82.66.147.146) (Read error: Connection reset by peer)
15:42:53 <ski> @src (>>=) Either
15:42:53 <lambdabot> Source not found. This mission is too important for me to allow you to jeopardize it.
15:43:05 <ski> @src Either (>>=)
15:43:05 <lambdabot> Left l >>= _ = Left l
15:43:05 <lambdabot> Right r >>= k = k r
15:43:08 <ncf> ski: isn't that just a left n-module?
15:43:27 <ncf> i.e. mn ~> n
15:43:27 <haskellbridge> <i​rregularsphere> (wait lambdabot can _do_ that?)
15:43:31 → Midjak joins (~MarciZ@82.66.147.146)
15:43:42 <ski> ncf : i was thinking about something like actions, or perhaps retract situations, yea
15:44:18 <ski> (i also had `forall a. n a -> m a', and some laws relating the operations)
15:44:20 <geekosaur> irregularsphere, it has a small database of sources which is sometimes inaccurate for ghc (it's mostly cribbed from the haskell 2010 report)
15:44:28 <ski> irregularsphere : do what ?
15:44:35 <geekosaur> it doesn't know how to search for actual source code, sadly
15:44:39 <haskellbridge> <i​rregularsphere> the @src command
15:44:46 <ski> anyway, imagine if it was defined like
15:45:07 <ski> Right a >>= k = k a
15:45:16 <ski> m >>= _ = m
15:45:49 <ski> and now imagine if this `m' had type `forall b. Either a b' (due to `m' not matching `Right a')
15:47:32 <ski> or, if you prefer
15:47:41 <ski> m@(Left _) >>= _ = m
15:47:49 × jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds)
15:49:31 → son0p joins (~ff@186.121.50.114)
15:50:50 <ski> irregularsphere : oh, and types are not inferred for higher-rank operations
15:51:03 <ski> (iow, that `id' won't be inferred)
16:09:10 → target_i joins (~target_i@217.175.14.39)
16:12:54 × fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection)
16:15:20 → wootehfoot joins (~wootehfoo@user/wootehfoot)
16:21:32 → Pixi` joins (~Pixi@user/pixi)
16:24:35 × Pixi quits (~Pixi@user/pixi) (Ping timeout: 252 seconds)
16:31:05 × coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot)
16:33:26 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds)
16:33:32 → euleritian joins (~euleritia@77.22.252.56)
16:34:58 → jargon joins (~jargon@157.sub-174-205-162.myvzw.com)
16:46:15 × AlexZenon quits (~alzenon@94.233.241.194) (Ping timeout: 256 seconds)
16:51:23 → AlexZenon joins (~alzenon@94.233.241.194)
17:06:04 → AstraGravityGirl joins (~astra@181.42.52.150)
17:08:16 × alexherbo2 quits (~alexherbo@2a02-8440-3341-cfe3-0966-2558-23d8-f964.rev.sfr.net) (Remote host closed the connection)
17:11:07 → alexherbo2 joins (~alexherbo@143.132.22.93.rev.sfr.net)
17:11:28 × pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5)
17:11:56 → pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
17:15:37 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
17:15:48 × alexherbo2 quits (~alexherbo@143.132.22.93.rev.sfr.net) (Remote host closed the connection)
17:15:53 → econo_ joins (uid147250@id-147250.tinside.irccloud.com)
17:17:16 × myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection)
17:28:11 × euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 256 seconds)
17:28:26 → euleritian joins (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de)
17:28:55 × yotta quits (~cha0s@14.191.144.106) (Quit: WeeChat 4.2.1)
17:29:49 <noumenon> what's a "rank"?
17:31:41 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 252 seconds)
17:33:40 <monochrom> https://wiki.haskell.org/Rank-N_types may help
17:36:02 → Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
17:36:15 → myxos joins (~myxos@065-028-251-121.inf.spectrum.com)
17:39:13 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 276 seconds)
17:40:11 × AstraGravityGirl quits (~astra@181.42.52.150) (Ping timeout: 264 seconds)
17:40:27 × euleritian quits (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) (Read error: Connection reset by peer)
17:40:34 × yoo quits (~yo0O0o@130.105.162.162) (Changing host)
17:40:34 → yoo joins (~yo0O0o@user/mobivme)
17:40:38 <ncf> rank(a -> b) = 1 + rank a; rank _ = 0
17:40:44 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
17:40:58 <ncf> er no
17:46:20 → AstraGravityGirl joins (~AstraGrav@181.42.52.150)
17:46:23 <ncf> i guess it's slightly tricky to define by induction on types. two mutually recursive functions should do it
17:46:30 <APic> Indeed.
17:46:56 × Midjak quits (~MarciZ@82.66.147.146) (Read error: Connection reset by peer)
17:47:30 → Midjak joins (~MarciZ@82.66.147.146)
17:47:56 → rvalue joins (~rvalue@user/rvalue)
17:51:55 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds)
17:52:35 → euleritian joins (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de)
17:55:26 × euleritian quits (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) (Read error: Connection reset by peer)
17:55:43 → euleritian joins (~euleritia@77.22.252.56)
18:01:01 × AstraGravityGirl quits (~AstraGrav@181.42.52.150) (Quit: AstraGravityGirl)
18:05:47 → tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net)
18:07:13 × Midjak quits (~MarciZ@82.66.147.146) (Ping timeout: 255 seconds)
18:13:35 → AstraGravityGirl joins (~AstraGrav@181.42.52.150)
18:15:04 → peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com)
18:15:47 × euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 256 seconds)
18:15:47 × AstraGravityGirl quits (~AstraGrav@181.42.52.150) (Client Quit)
18:18:32 → euleritian joins (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de)
18:25:40 <ski> noumenon : briefly, it's when a function take a polymorphic operation as *argument*, or when a function takes such a function as argument, &c.
18:26:07 <ski> so `(forall a. ..a..) -> ...' or `((forall a. ..a..) -> ...) -> ...' or ..
18:27:41 <ski> (some people say "higher-rank polymorphism", but i don't think the first of those examples is like polymorphism at all (more like existentials, cf. `... -> (exists a. ..a..)'. the next one is "kinda like polymorphism", though, so we alternate between "kinda existential" and "kinda universal")
18:30:10 <ski> (oh, and "higher-rank" means rank greater than one. rank one is plain polymorphism, values of type `forall a. ..a..'. sometimes people call (ordinary, without `forall' and `exists') monomorphic operations, "rank zero")
18:31:39 <ski> (and that issue with "non-ranked" operations is what ncf ran into above)
18:43:54 → coot joins (~coot@89.69.206.216)
18:47:02 → pyooque joins (~puke@user/puke)
18:47:02 puke is now known as Guest9035
18:47:02 × Guest9035 quits (~puke@user/puke) (Killed (tungsten.libera.chat (Nickname regained by services)))
18:47:02 pyooque is now known as puke
18:47:30 → alexherbo2 joins (~alexherbo@2a02-8440-3341-cfe3-f821-77e5-e4a1-a519.rev.sfr.net)
18:47:39 <noumenon> ski: so, can you rank ranks?
18:53:05 × euleritian quits (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) (Read error: Connection reset by peer)
18:53:22 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
18:56:34 × peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds)
18:57:11 → Midjak joins (~MarciZ@82.66.147.146)
18:57:59 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
18:59:42 → euleritian joins (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de)
19:00:09 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 272 seconds)
19:02:26 → Guest33 joins (~Guest33@2804:7f7:ddab:a8cd:9c91:258e:279f:d997)
19:03:59 × Guest33 quits (~Guest33@2804:7f7:ddab:a8cd:9c91:258e:279f:d997) (Client Quit)
19:06:49 × coot quits (~coot@89.69.206.216) (Quit: coot)
19:07:56 → ursa-major joins (~ursa-majo@c-174-63-24-92.hsd1.co.comcast.net)
19:08:11 → rvalue joins (~rvalue@user/rvalue)
19:10:44 × euleritian quits (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
19:11:02 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
19:12:34 <ski> noumenon : how do you mean ?
19:14:38 <noumenon> ski: oh, nvm, I was confusing it with "kind"
19:15:37 <noumenon> something about forming a fractal hierarchy
19:16:36 <noumenon> having sorts of kinds, and so on
19:17:04 <noumenon> species of sorts
19:17:09 <noumenon> varieties of species
19:17:33 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
19:17:39 <noumenon> I wonder if you can abstract even that fractal nesting somehow
19:19:23 <EvanR> you run out of jargon so fast, might as well call the type universes by number
19:19:39 <EvanR> Type 1 : Type 2 : Type 3, etc
19:20:52 → euleritian joins (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de)
19:21:03 <noumenon> sounds more reasonable
19:21:06 <ncf> it's called agda
19:24:55 × alexherbo2 quits (~alexherbo@2a02-8440-3341-cfe3-f821-77e5-e4a1-a519.rev.sfr.net) (Remote host closed the connection)
19:30:34 × rscastilho2024 quits (~rscastilh@189.61.140.215) (Remote host closed the connection)
19:31:02 × euleritian quits (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
19:31:24 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
19:35:10 → rscastilho2024 joins (~rscastilh@189.61.140.215)
19:37:52 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
19:39:37 → ld joins (~ld@2a01:4b00:8438:1700:eee4:f118:781d:97a0)
19:39:45 × ld quits (~ld@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection)
19:40:16 <noumenon> lol
19:40:18 <noumenon> https://iohk.io/en/research/library/papers/reasonable-agda-is-correct-haskell-writing-verified-haskell-using-agda2hs/
19:40:20 → euleritian joins (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de)
19:40:25 → azr4e1 joins (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0)
19:40:28 <noumenon> and just when I thought Haskell was the biggest shark in the water
19:40:52 <Rembane> noumenon: There are always bigger sharks. :)
19:41:13 × azr4e1 quits (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection)
19:41:56 → azr4e1 joins (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0)
19:41:59 × azr4e1 quits (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection)
19:42:31 <ncf> haskell is nothing
19:42:38 <ncf> -- bob harper, probably
19:42:42 <noumenon> Rembane: there has to be some ultimate language, one which perfectly abstracts anything; the biggest shark
19:43:12 <Rembane> noumenon: Maybe. Lambda calculus perhaps?
19:43:34 → Guest92 joins (~Guest92@97-120-50-87.ptld.qwest.net)
19:43:37 <noumenon> maybe that's what we should be programming with
19:44:33 <ncf> it's called agda (bis)
19:44:50 <ncf> cubical agda, even
19:45:14 × euleritian quits (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
19:45:16 <probie> Is cubical agda the hott extension to agda?
19:45:32 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
19:45:45 <noumenon> >open import Cubical.Core.Everything
19:45:55 <noumenon> well, that does sound like something you'd write before coding the universe
19:45:59 <ncf> the *computational* hott extension to agda
19:47:24 → azr4e1 joins (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0)
19:47:38 <geekosaur> noumenon: abstracts how? there are multiple kinds of abstraction
19:47:39 <ncf> (you don't need any extensions to do hott; in fact you need to *remove* an axiom (--without-K). but if you want your proofs to actually compute, then you need a metric shitton of complicated stuff)
19:48:39 <geekosaur> LC is one form of abstraction. the Ωmega language abstracts in a different way. etc.
19:50:22 <noumenon> geekosaur: something that abstracts abstraction itself, the ultimate abstraction, the Megalodon of languages
19:50:51 <noumenon> hopefully with intuitive syntax
19:51:02 <geekosaur> didn't Gödel have something to say about that?
19:51:34 <noumenon> until Gödel proves his theorems with Agda I don't believe them
19:53:22 → pmk joins (6afe4476a1@2a03:6000:1812:100::26d)
19:58:33 × Guest92 quits (~Guest92@97-120-50-87.ptld.qwest.net) (Quit: Client closed)
20:02:52 × azr4e1 quits (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection)
20:04:29 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
20:08:20 → azr4e1 joins (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0)
20:08:35 × azr4e1 quits (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection)
20:09:07 → finsternis joins (~X@23.226.237.192)
20:09:09 → bzm3r joins (~bzm3r@d205-250-253-229.bchsia.telus.net)
20:09:12 → azr4e1 joins (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0)
20:09:26 × azr4e1 quits (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection)
20:10:06 × rscastilho2024 quits (~rscastilh@189.61.140.215) (Remote host closed the connection)
20:16:07 → Achylles joins (~Achylles_@45.182.57.125)
20:20:21 <EvanR> noumenon, haskell is the gateway drug of advanced programming languages
20:20:44 <EvanR> you may never heard of what's out there until you do haskell and then people tell you that's nothing
20:22:02 → Sgeo joins (~Sgeo@user/sgeo)
20:23:15 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
20:41:11 × noumenon quits (~noumenon@113.51-175-156.customer.lyse.net) (Read error: Connection reset by peer)
20:48:45 → peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com)
20:52:06 × ricardo_1 quits (~ricardo@shabang.toppoint.de) (Read error: Connection reset by peer)
20:54:55 × michalz quits (~michalz@185.246.207.205) (Quit: ZNC 1.8.2 - https://znc.in)
20:55:17 → azr4e1 joins (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0)
20:55:31 × peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds)
20:56:45 → hamster joins (~ham@user/ham)
20:58:23 × Achylles quits (~Achylles_@45.182.57.125) (Quit: Leaving)
20:58:49 → Achylles joins (~Achylles_@45.182.57.125)
20:59:03 × Achylles quits (~Achylles_@45.182.57.125) (Max SendQ exceeded)
20:59:13 × ham2 quits (~ham@user/ham) (Ping timeout: 264 seconds)
21:01:16 <TMA> well, Gödel theorems are just the tip of the iceberg. if you happen to have a "nice" theory of first order logic [nice ~ consistent, complete] the axioms are not recursively enumerable
21:03:03 <TMA> there cannot be the biggest shark
21:05:23 × raoul quits (~raoul@95.179.203.88) (Quit: Ping timeout (120 seconds))
21:05:42 → raoul joins (~raoul@95.179.203.88)
21:07:26 × target_i quits (~target_i@217.175.14.39) (Quit: leaving)
21:08:13 <haskellbridge> <L​iamzee> hi noumenon, I'm phenomenon, how are you doing? :)
21:11:22 × Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 256 seconds)
21:11:57 → Maxdamantus joins (~Maxdamant@user/maxdamantus)
21:14:19 × RaspbellySwirl quits (~Raspbelly@host-213-235-142-6.ip.topnet.cz) (Ping timeout: 246 seconds)
21:16:33 × ursa-major quits (~ursa-majo@c-174-63-24-92.hsd1.co.comcast.net) (Quit: WeeChat 4.2.1)
21:17:11 × hololeap quits (~quassel@user/hololeap) (Quit: Bye)
21:18:17 → hololeap joins (~quassel@user/hololeap)
21:24:05 ski idly ponders time cubical agda
21:25:07 <ski> noumenon left, about half an hour ago
21:26:13 <EvanR> is that what dr gene ray used. Time is cubic: top bottom and two sides
21:28:20 → peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com)
21:33:51 ski . o O ( "The 4-equidistant time points can be considered as Time Square imprinted upon the circle of Earth. In a single rotation of the Earth sphere, each Time corner point rotates through the other 3-corner Time points, thus creating 16 corners, 96 hours and 4-simultaneous 24-hour Days within a single rotation of Earth – equated to a Higher Order of Life Time Cube." )
21:34:08 <ski> clearly this is talking about suspensions and stuff
21:34:30 <EvanR> you're somehow right
21:34:40 × azr4e1 quits (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Ping timeout: 255 seconds)
21:39:12 × _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht)
21:39:32 <ncf> suspensions of disbelief
21:43:35 × peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
21:56:11 <ncf> ski: surely "time cubical agda" would implement guarded cubical type theory (https://agda.readthedocs.io/en/latest/language/guarded.html)
22:00:03 <ski> hm, that's modal stuff, yes ?
22:00:38 ski 's reminded of Nanevski's "Contextual Modal Type Theory"
22:01:45 <ncf> there's a "later" modality, clock quantification...
22:02:25 <ski> .. i wonder how (if) this relates to MetaML/MetaOCaml stuff
22:02:47 → Miroboru joins (~myrvoll@178-164-114.82.3p.ntebredband.no)
22:03:43 <ski> "Application t u for t : (@tick x : A) → B is restricted so that t is typable in the prefix of the context that does not include any @tick variables in u." -- what's the type of `u', here ?
22:05:17 <ncf> A
22:07:55 × todi quits (~todi@p4fd1aef3.dip0.t-ipconnect.de) (Quit: ZNC - https://znc.in)
22:07:59 × dostoyevsky2 quits (~sck@user/dostoyevsky2) (Quit: leaving)
22:08:18 <haskellbridge> <i​rregularsphere> EvanR: i felt stupid searching up "gateway drug"
22:08:22 → dostoyevsky2 joins (~sck@user/dostoyevsky2)
22:09:34 <geekosaur> gotta be careful with those English idioms…
22:09:55 <EvanR> I just check urban dictionary to see if it would help. It does not
22:10:06 × puke quits (~puke@user/puke) (Quit: puke)
22:13:28 <haskellbridge> <i​rregularsphere> noumenon: wdym agda is a "bigger shark" than haskell
22:13:44 <haskellbridge> <i​rregularsphere> it just looks like haskell but the compiler proves it
22:13:51 <haskellbridge> <i​rregularsphere> either way agda2hs seems nice
22:14:50 <geekosaur> noumenon left some time ago
22:16:01 <geekosaur> (the bridge doesn't relay joins/parts and I Have no intention of enabling that)
22:17:24 <EvanR> you do join part reporting just fine
22:17:30 <EvanR> thanks
22:18:47 × ystael quits (~ystael@user/ystael) (Ping timeout: 252 seconds)
22:19:56 <haskellbridge> <i​rregularsphere> wait is haskell intrinsically not always type correct
22:20:00 <haskellbridge> <i​rregularsphere> i hate to see it
22:20:17 × dostoyevsky2 quits (~sck@user/dostoyevsky2) (Quit: leaving)
22:20:27 <geekosaur> it's type correct, but there are programs that are well typed that haskell's typechecker cannot so prove
22:20:28 <haskellbridge> <i​rregularsphere> ~~*meanwhile me putting up `undefined` in `Instance Num`~~
22:20:33 → dostoyevsky2 joins (~sck@user/dostoyevsky2)
22:20:44 <haskellbridge> <i​rregularsphere> type correct as in mathematically correct
22:20:44 <geekosaur> because it's relatively weak
22:20:45 <EvanR> well typed programs don't get stuck
22:21:15 → puke joins (~puke@user/puke)
22:21:34 <geekosaur> agda, idris, and coq among others have stronger type checkers
22:22:26 <geekosaur> and agda and idris can translate to haskell basically by doing the typechecking and then wrapping everything in unsafeCoerce aka "just trust me on this, okay?"
22:22:51 <haskellbridge> <i​rregularsphere> is unsafeCoerce basically "yeah i proved this myself"
22:22:57 <geekosaur> yes
22:23:07 <haskellbridge> <i​rregularsphere> oh so that's what it's for
22:23:59 <EvanR> there are programs that make sense that can't be type checked in haskell. And there are type checked programs in haskell that crash disgracefully
22:24:15 <haskellbridge> <i​rregularsphere> i wonder what unsafeCoerce# is up to
22:24:51 <haskellbridge> <i​rregularsphere> to be put up with such funny documentation
22:25:01 <haskellbridge> <i​rregularsphere> > Highly, terribly dangerous coercion from one representation type to another. Misuse of this function can invite the garbage collector to trounce upon your data and then laugh in your face. You don't want this function. Really.
22:26:10 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:27:11 <geekosaur> unsafeCoerce reinterprets one LiftedRep as a different LiftedRep. this is somewhat dangerous if the two aren't actually representationally compatible
22:28:06 <geekosaur> unsafeCoerce# reinteprets any TypeRep as a different TypeRep. this is a very good way to cause core dumps if you don't know exactly what you're doing
22:32:14 × chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
22:33:08 → chexum joins (~quassel@gateway/tor-sasl/chexum)
22:34:36 × mechap quits (~mechap@user/mechap) (Quit: WeeChat 4.2.1)
22:51:38 → azr4e1 joins (~azr4e1@137.220.68.193)
22:51:54 × azr4e1 quits (~azr4e1@137.220.68.193) (Remote host closed the connection)
22:53:55 × JordiGH quits (~jordi@user/jordigh) (Ping timeout: 268 seconds)
22:57:28 → random-jellyfish joins (~developer@user/random-jellyfish)
23:03:02 → causal joins (~eric@50.35.85.7)
23:06:19 → tri joins (~tri@ool-18bc2e74.dyn.optonline.net)
23:10:20 → jmdaemon joins (~jmdaemon@user/jmdaemon)
23:11:05 × tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 260 seconds)
23:24:33 × takuan quits (~takuan@178.116.218.225) (Remote host closed the connection)
23:29:08 → JordiGH joins (~jordi@user/jordigh)
23:29:52 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
23:35:01 × Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep)
23:40:21 <ski> hm, so it's not like `@tick A', then ?
23:45:01 × random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 256 seconds)
23:52:25 → tri joins (~tri@ool-18bc2e74.dyn.optonline.net)
23:56:50 × tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds)
23:57:04 × acidjnk_new quits (~acidjnk@p5dd87f44.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)

All times are in UTC on 2024-02-11.