Home liberachat/#haskell: Logs Calendar

Logs on 2025-01-14 (liberachat/#haskell)

00:00:48 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
00:07:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
00:18:52 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
00:23:07 × rini quits (~rini@user/rini) (Ping timeout: 252 seconds)
00:23:08 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
00:24:29 × sprotte24 quits (~sprotte24@p200300d16f245c002d65884199a66258.dip0.t-ipconnect.de) (Quit: Leaving)
00:31:17 × acidjnk_new quits (~acidjnk@p200300d6e7283f35081469c6fc5c461d.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
00:33:58 rini joins (~rini@user/rini)
00:39:00 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 252 seconds)
00:42:11 Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-134-103.cust.tzulo.com)
00:42:27 × Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-134-103.cust.tzulo.com) (Remote host closed the connection)
00:42:52 Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-134-103.cust.tzulo.com)
00:45:07 swistak joins (~swistak@185.21.216.141)
00:49:36 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
00:50:25 × xff0x quits (~xff0x@2405:6580:b080:900:39df:db2a:91b7:da54) (Ping timeout: 248 seconds)
00:52:13 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
00:52:29 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
00:54:16 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
00:55:12 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
00:55:38 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
00:55:47 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
00:56:06 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
01:04:59 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:05:46 × stiell quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
01:06:34 stiell joins (~stiell@gateway/tor-sasl/stiell)
01:08:46 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
01:09:48 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
01:13:29 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
01:20:21 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:23:31 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
01:24:30 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
01:24:50 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
01:29:11 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
01:35:22 × otto_s quits (~user@p5de2fe2f.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
01:35:45 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:37:02 otto_s joins (~user@p4ff272c8.dip0.t-ipconnect.de)
01:40:39 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds)
01:42:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
01:48:03 xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
01:51:54 JamesMowery4395 joins (~JamesMowe@ip68-228-212-232.ph.ph.cox.net)
01:53:33 × JamesMowery439 quits (~JamesMowe@ip68-228-212-232.ph.ph.cox.net) (Ping timeout: 244 seconds)
01:53:33 JamesMowery4395 is now known as JamesMowery439
01:53:48 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:58:13 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
02:00:09 ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com)
02:01:29 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
02:09:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
02:13:29 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
02:22:18 × vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds)
02:23:55 × Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-134-103.cust.tzulo.com) (Quit: Leaving)
02:24:13 vanishingideal joins (~vanishing@user/vanishingideal)
02:24:33 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
02:29:12 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
02:29:57 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
02:30:18 potatoespotatoes joins (~quassel@130.44.147.204)
02:30:28 rvalue joins (~rvalue@user/rvalue)
02:33:18 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 245 seconds)
02:37:34 dmwit joins (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net)
02:39:09 <dmwit> I have foo.c. I'd like cabal to be in charge of creating foo.so and making foo.so available, perhaps through the Paths_mypackagename mechanism. Can I convince it to do that somehow? (Directly linking with foo.o or foo.a isn't enough, as I am going to fork a separate program that wants this .so to be available.)
02:41:39 × vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 260 seconds)
02:42:01 weary-traveler joins (~user@user/user363627)
02:43:15 vanishingideal joins (~vanishing@user/vanishingideal)
02:45:45 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
02:46:21 × potatoespotatoes quits (~quassel@130.44.147.204) (Changing host)
02:46:21 potatoespotatoes joins (~quassel@user/potatoespotatoes)
02:47:02 × potatoespotatoes quits (~quassel@user/potatoespotatoes) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
02:47:11 <geekosaur> https://cabal.readthedocs.io/en/stable/cabal-package-description-file.html#foreign-libraries with an empty list of Haskell modules?
02:47:16 potatoespotatoes joins (~quassel@130.44.147.204)
02:48:07 × potatoespotatoes quits (~quassel@130.44.147.204) (Changing host)
02:48:07 potatoespotatoes joins (~quassel@user/potatoespotatoes)
02:50:27 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
02:51:39 × potatoespotatoes quits (~quassel@user/potatoespotatoes) (Client Quit)
02:51:57 potatoespotatoes joins (~quassel@user/potatoespotatoes)
02:54:49 <dmwit> Interesting. That will probably add in a linker dependency on the Haskell runtime but that might not be a problem. Let me play with it, thanks for the suggestion.
02:58:23 Guest5 joins (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net)
03:01:07 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:02:37 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
03:03:33 <Guest5> Hi, I’ve messed up my setup, which means no xmonad and no GUI. While updating, the Haskell packages didn’t want to update so I uninstalled them to reinstall them, but now they all fail (other than GHC) with “cannot satisfy -package gtk2hs-buildtools“. I tried “emerge —oneshot —nodeps gtk2hs-buildtools” but that failed with the same
03:03:34 <Guest5> error. I’d send a paste but I don’t have xmonad so I don’t have a GUI anymore
03:04:06 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 272 seconds)
03:05:32 <dmwit> What tool are you using to install/uninstall packages? What does ghc-pkg list gtk2hs-buildtools say?
03:05:37 <Guest5> Of course haskell-updater didn’t work, I’m pretty sure it didn’t even try to build any packages
03:06:24 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
03:07:06 <Guest5> ghc-pkg list gtk2hs-buildtools says “no packages”, with the conf file being inside ~/.ghcup, which I didn’t know I had installed (maybe stack did that)
03:07:16 × potatoespotatoes quits (~quassel@user/potatoespotatoes) ()
03:07:44 <Guest5> And to install packages system wide I use emerge, and I use stack or cabal per-project
03:08:14 <dmwit> Is it possible that emerge and stack/cabal are choosing different GHC versions/installations?
03:08:30 potatoespotatoes joins (~quassel@130.44.147.204)
03:08:30 × potatoespotatoes quits (~quassel@130.44.147.204) (Changing host)
03:08:30 potatoespotatoes joins (~quassel@user/potatoespotatoes)
03:09:24 <Guest5> It is, I will uninstall GHC with emerge and see if there’s another system-wide one for Cabal hiding somewhere
03:09:49 <dmwit> ghcup tui will show you what's happening in ~/.ghcup for what it's worth
03:09:57 × Guest5 quits (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net) (Quit: Client closed)
03:10:01 × vanishingideal quits (~vanishing@user/vanishingideal) (*.net *.split)
03:10:01 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (*.net *.split)
03:10:01 × Sgeo quits (~Sgeo@user/sgeo) (*.net *.split)
03:10:01 × notzmv quits (~umar@user/notzmv) (*.net *.split)
03:10:01 × avidseeker quits (av@user/avidseeker) (*.net *.split)
03:10:01 × OftenFaded quits (~OftenFade@user/tisktisk) (*.net *.split)
03:10:01 × Sciencentistguy quits (~sciencent@hacksoc/ordinary-member) (*.net *.split)
03:10:02 × terrorjack45 quits (~terrorjac@2a01:4f8:c17:a66e::) (*.net *.split)
03:10:02 × img quits (~img@user/img) (*.net *.split)
03:10:02 × op_4 quits (~tslil@user/op-4/x-9116473) (*.net *.split)
03:10:02 × petrichor quits (~znc-user@user/petrichor) (*.net *.split)
03:10:02 × L29Ah quits (~L29Ah@wikipedia/L29Ah) (*.net *.split)
03:10:02 × Me-me quits (~me-me@user/me-me) (*.net *.split)
03:10:02 × tomboy64 quits (~tomboy64@user/tomboy64) (*.net *.split)
03:10:02 × YuutaW quits (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (*.net *.split)
03:10:02 × haritz quits (~hrtz@user/haritz) (*.net *.split)
03:10:02 × zero quits (~z@user/zero) (*.net *.split)
03:10:02 × migas9778 quits (~migas@static.140.65.63.178.clients.your-server.de) (*.net *.split)
03:10:02 × jrm quits (~jrm@user/jrm) (*.net *.split)
03:10:03 × tessier quits (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (*.net *.split)
03:10:03 × stilgart quits (~Christoph@chezlefab.net) (*.net *.split)
03:10:03 × GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (*.net *.split)
03:10:03 × nshepperd2 quits (~nshepperd@2a01:4f9:3b:4cc9::2) (*.net *.split)
03:10:03 × nadja quits (~dequbed@banana-new.kilobyte22.de) (*.net *.split)
03:10:03 × foul_owl quits (~kerry@185.203.219.80) (*.net *.split)
03:10:03 × nurupo quits (~nurupo.ga@user/nurupo) (*.net *.split)
03:10:03 × meinside quits (uid24933@id-24933.helmsley.irccloud.com) (*.net *.split)
03:10:03 × _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (*.net *.split)
03:10:03 × zlqrvx quits (~zlqrvx@user/zlqrvx) (*.net *.split)
03:10:03 × ycp quits (~znc@user/dragestil) (*.net *.split)
03:10:03 × jathan quits (~jathan@69.61.93.38) (*.net *.split)
03:10:03 × sprout quits (~sprout@84-80-106-227.fixed.kpn.net) (*.net *.split)
03:10:03 × Ekho quits (~Ekho@user/ekho) (*.net *.split)
03:10:04 × Ranhir quits (~Ranhir@157.97.53.139) (*.net *.split)
03:10:04 × bliminse quits (~bliminse@user/bliminse) (*.net *.split)
03:10:04 × tdammers quits (~tdammers@110-136-178-143.ftth.glasoperator.nl) (*.net *.split)
03:10:04 × mzg quits (mzg@abusers.hu) (*.net *.split)
03:10:04 × Goodbye_Vincent1 quits (cyvahl@freakshells.net) (*.net *.split)
03:14:33 Guest57 joins (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net)
03:15:03 vanishingideal joins (~vanishing@user/vanishingideal)
03:15:03 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
03:15:03 Sgeo joins (~Sgeo@user/sgeo)
03:15:03 notzmv joins (~umar@user/notzmv)
03:15:03 avidseeker joins (av@user/avidseeker)
03:15:03 OftenFaded joins (~OftenFade@user/tisktisk)
03:15:03 Sciencentistguy joins (~sciencent@hacksoc/ordinary-member)
03:15:03 terrorjack45 joins (~terrorjac@2a01:4f8:c17:a66e::)
03:15:03 img joins (~img@user/img)
03:15:03 op_4 joins (~tslil@user/op-4/x-9116473)
03:15:03 petrichor joins (~znc-user@user/petrichor)
03:15:03 L29Ah joins (~L29Ah@wikipedia/L29Ah)
03:15:03 Me-me joins (~me-me@user/me-me)
03:15:03 tomboy64 joins (~tomboy64@user/tomboy64)
03:15:03 YuutaW joins (~YuutaW@2404:f4c0:f9c3:502::100:17b7)
03:15:03 haritz joins (~hrtz@user/haritz)
03:15:03 zero joins (~z@user/zero)
03:15:03 migas9778 joins (~migas@static.140.65.63.178.clients.your-server.de)
03:15:03 jrm joins (~jrm@user/jrm)
03:15:03 tessier joins (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com)
03:15:03 stilgart joins (~Christoph@chezlefab.net)
03:15:03 GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano)
03:15:03 nshepperd2 joins (~nshepperd@2a01:4f9:3b:4cc9::2)
03:15:03 nadja joins (~dequbed@banana-new.kilobyte22.de)
03:15:03 foul_owl joins (~kerry@185.203.219.80)
03:15:03 nurupo joins (~nurupo.ga@user/nurupo)
03:15:03 meinside joins (uid24933@id-24933.helmsley.irccloud.com)
03:15:03 _d0t joins (~{-d0t-}@user/-d0t-/x-7915216)
03:15:03 zlqrvx joins (~zlqrvx@user/zlqrvx)
03:15:03 ycp joins (~znc@user/dragestil)
03:15:03 jathan joins (~jathan@69.61.93.38)
03:15:03 sprout joins (~sprout@84-80-106-227.fixed.kpn.net)
03:15:03 Ekho joins (~Ekho@user/ekho)
03:15:03 Ranhir joins (~Ranhir@157.97.53.139)
03:15:03 bliminse joins (~bliminse@user/bliminse)
03:15:03 tdammers joins (~tdammers@110-136-178-143.ftth.glasoperator.nl)
03:15:03 mzg joins (mzg@abusers.hu)
03:15:03 Goodbye_Vincent1 joins (cyvahl@freakshells.net)
03:15:04 × img quits (~img@user/img) (Max SendQ exceeded)
03:15:18 <Guest57> I got disconnected, did anyone say anything after 14:09? I am Guest5
03:15:18 img joins (~img@user/img)
03:16:36 <Guest57> Well, [current-hour]:09
03:17:11 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:20:05 <geekosaur> nope
03:22:57 <dmwit> I told you that ghcup tui would tell you about what ghcup knows.
03:23:07 <dmwit> Not sure whether that was after :09 or not.
03:24:14 <dmwit> geekosaur: So I can see that foreign-library results in a library being built into dist-newstyle, but I'm not sure how I'm meant to access that library('s directory) from within my application. At the very least cabal hasn't added the directory to any environment variables.
03:24:19 swistak joins (~swistak@185.21.216.141)
03:24:22 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
03:24:38 <Guest57> ghcup tui says I have an install of stack, cabal, and 10 GHC versions
03:25:00 <dmwit> scary =P
03:25:17 <geekosaur> does it actually say they're installed, or just available?
03:25:46 <Guest57> Systemwide version is 9.8.2 and ghcup version is 9.4.8. I tried downgrading but didn’t work
03:26:01 <Guest57> Well, they don’t say anything, they’re just green
03:26:39 <geekosaur> ghcup won't know about the system-wide version, and having both will lead to confusion at best and brokenness at worst
03:26:42 <geekosaur> pick one
03:27:00 <Guest57> If two greens mean installed, then only GHC 9.4.8 is installed, along with stack and cabal
03:27:22 <geekosaur> two green checkmarks means it's the default
03:27:28 <dmwit> Two green checks means default, one means installed, zero means available.
03:27:33 × Everything quits (~Everythin@195.138.86.118) (Ping timeout: 252 seconds)
03:28:07 <geekosaur> dmwit, I don't really know what happens after it's built, that's probably a #hackage question
03:28:21 <Guest57> Well, my problem is emerge failures, I don’t see how ghcup will affect those when I merge under root, which doesn’t have any of my local ghcup stuff in its path
03:28:32 <dmwit> Wow. That is not a channel I would have guessed. Okay, thanks.
03:28:43 <geekosaur> if you have a different ghc in your $PATH when you run emerge then things will get mixed up
03:29:01 <geekosaur> decide whether you are using emerge or ghcup, and get rid of the one you're not using
03:29:13 <dmwit> I wouldn't be too surprised if you have multiple versions installed even without considering what ghcup's done in $HOME
03:29:13 <haskellbridge> <maerwald> I don't think so
03:29:43 <haskellbridge> <maerwald> I'm pretty sure there's environment sanitization when emerge is run
03:29:54 <haskellbridge> <maerwald> Especially since it's not run as the user
03:31:26 × Guest57 quits (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net) (Quit: Client closed)
03:33:47 × hueso quits (~root@user/hueso) (Ping timeout: 244 seconds)
03:34:59 Guest38 joins (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net)
03:35:13 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:36:35 hueso joins (~root@user/hueso)
03:38:48 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:38:49 <dmwit> I mean I guess I don't really know what's going wrong. Perhaps you can find out a bit more about what emerge is doing with a --verbose or something?
03:39:33 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
03:42:34 <Guest38> All the logs say the same thing, that is, gtk2hs-buildtools couldn’t be found by the inner cabal that emerge uses. Of course, because it isn’t installed yet. I reinstalled cabal to see if that would change anything, but no luck
03:45:14 <dmwit> If you can find out what exact cabal command it's running, that might help explain why it believes it needs gtk2hs-buildtools.
03:45:36 <dmwit> That's a very unusual dependency, it should only be needed when installing things that depend on gtk2hs, which are bindings to a GUI library.
03:46:26 <dmwit> ...although if emerge and your shell are choosing different GHC versions, then the ghc-pkg command I suggested earlier will need to be tweaked. Can you try it again as root? ghc-pkg list gtk2hs-buildtools
03:46:54 <dmwit> (One hypothesis is that GHC's package database is broken; if it were, this might reveal that.)
03:47:44 <dmwit> (root or whatever user emerge runs as, I guess)
03:50:35 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:55:19 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
03:57:01 avidseeker parts (av@user/avidseeker) ()
03:59:45 avidseeker joins (av@user/avidseeker)
04:01:15 <Guest38> ‘ghc-pkg list’ with no package argument gives what looks like standard libraries such as base, binary, template-Haskell, parsec, mtl, and Cabal. There are more but I am on my phone so don’t want to type them out
04:02:35 <dmwit> If none of them say "broken" afterwards then that hypothesis is out.
04:02:47 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:03:17 <dmwit> At this point without the exact cabal command I don't think there's much folks here can do for you.
04:03:50 <Guest38> The command turned out to not be cabal, it was just ghc -hide-all-packages -package Cabal -package array … -package xhtml -package gtk2hs-buildtools —make …
04:04:43 <Guest38> The only packages listed here not in my ghc-pkg list are gtk2hs-buildtools and xhtml
04:04:57 <dmwit> Okay. What tool crafted this command line?
04:05:31 <Guest38> Never mind, xhtml is in the command line
04:05:47 saulosilva joins (~saulosilv@2804:14c:b525:8032:5d21:a3da:d197:21e9)
04:06:34 <Guest38> Probably cabal. I’m seeing this in the emerge build.log after “Using cabal-3.8.2.0” inside “configuring source…”
04:06:50 <Guest38> It’s making Setup.lhs
04:07:03 <dmwit> ...so like I said: we need the exact cabal command.
04:07:45 <saulosilva> Hello
04:07:52 × Guest38 quits (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net) (Quit: Client closed)
04:08:32 <saulosilva> What resources should i check out first regarding functional paradigm?
04:08:33 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
04:10:25 Guest79 joins (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net)
04:10:55 <dmwit> The Haskell wiki has a long list of tutorials, and some guidance on how to pick one.
04:11:14 <dmwit> https://wiki.haskell.org/index.php?title=Tutorials
04:11:16 <Guest79> Ah, I just realized I’m in #haskell rather than #haskell-gentoo. No wonder things weren’t adding up. Sorry dmwit and all, I’ll move this over there
04:13:17 × Guest79 quits (~Guest29@2403-5805-c700-0-f01e-fad9-5333-2933.ip6.aussiebb.net) (Client Quit)
04:13:30 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 276 seconds)
04:19:27 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:19:57 bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
04:24:02 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
04:31:14 <Axman6> I think the System-F FP course does a good job of introducing functional programming in general (particularly strongly typed, pure functional), but I may be a bit biased
04:34:49 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:40:14 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
04:44:14 dysthesis joins (~dysthesis@user/dysthesis)
04:51:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:58:08 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
05:03:24 swistak joins (~swistak@185.21.216.141)
05:09:15 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
05:13:53 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
05:14:20 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
05:20:17 dontdieych2 joins (~quassel@user/dontdieych2)
05:24:35 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
05:28:51 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
05:36:27 × tnt1 quits (~Thunderbi@user/tnt1) (Remote host closed the connection)
05:39:58 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
05:41:03 tnt1 joins (~Thunderbi@user/tnt1)
05:43:14 michalz joins (~michalz@185.246.207.197)
05:44:49 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
05:53:56 × ft quits (~ft@p4fc2a354.dip0.t-ipconnect.de) (Quit: leaving)
05:55:20 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
05:59:49 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
06:03:46 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
06:03:47 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:07:07 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds)
06:08:07 euleritian joins (~euleritia@dynamic-176-006-128-096.176.6.pool.telefonica.de)
06:08:21 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
06:10:17 × euleritian quits (~euleritia@dynamic-176-006-128-096.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
06:10:37 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
06:16:50 Square2 joins (~Square4@user/square)
06:19:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:20:09 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 244 seconds)
06:21:00 × Square quits (~Square@user/square) (Ping timeout: 252 seconds)
06:22:48 takuan joins (~takuan@178-116-218-225.access.telenet.be)
06:23:46 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
06:28:42 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
06:29:37 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds)
06:32:06 euleritian joins (~euleritia@dynamic-176-001-018-193.176.1.pool.telefonica.de)
06:34:31 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:39:15 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
06:39:51 × ryanbooker quits (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
06:47:37 × doyougnu quits (~doyougnu@syn-045-046-170-068.res.spectrum.com) (Quit: ZNC 1.8.2 - https://znc.in)
06:50:03 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:51:54 doyougnu joins (~doyougnu@syn-045-046-170-068.res.spectrum.com)
06:54:21 CiaoSen joins (~Jura@2a05:5800:2eb:a800:ca4b:d6ff:fec1:99da)
06:54:38 JuanDaugherty joins (~juan@user/JuanDaugherty)
06:55:16 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
06:55:29 swistak joins (~swistak@185.21.216.141)
06:58:20 tnt2 joins (~Thunderbi@user/tnt1)
06:59:08 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds)
06:59:08 tnt2 is now known as tnt1
07:04:46 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:09:43 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
07:10:24 × dysthesis quits (~dysthesis@user/dysthesis) (Ping timeout: 264 seconds)
07:11:17 acidjnk_new joins (~acidjnk@p200300d6e7283f533582140b26ca98c6.dip0.t-ipconnect.de)
07:12:40 × saulosilva quits (~saulosilv@2804:14c:b525:8032:5d21:a3da:d197:21e9) (Ping timeout: 240 seconds)
07:13:16 rvalue- joins (~rvalue@user/rvalue)
07:13:57 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 248 seconds)
07:16:48 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
07:19:42 rvalue- is now known as rvalue
07:20:11 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:24:56 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
07:25:40 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 272 seconds)
07:26:00 saulosilva joins (~saulosilv@2804:14c:b525:8032:2178:624d:5387:e840)
07:26:16 swistak joins (~swistak@185.21.216.141)
07:29:09 × euleritian quits (~euleritia@dynamic-176-001-018-193.176.1.pool.telefonica.de) (Ping timeout: 276 seconds)
07:29:10 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty)
07:29:48 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
07:30:30 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
07:35:34 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:36:03 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 265 seconds)
07:38:52 sawilagar joins (~sawilagar@user/sawilagar)
07:42:39 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
07:50:58 lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
07:51:31 alecs joins (~alecs@nat16.software.imdea.org)
07:53:05 swistak joins (~swistak@185.21.216.141)
07:53:38 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:56:35 sord937 joins (~sord937@gateway/tor-sasl/sord937)
07:58:09 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
07:59:03 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds)
08:00:01 × caconym quits (~caconym@user/caconym) (Quit: bye)
08:00:39 caconym joins (~caconym@user/caconym)
08:03:11 × saulosilva quits (~saulosilv@2804:14c:b525:8032:2178:624d:5387:e840) (Quit: Client closed)
08:04:27 akegalj joins (~akegalj@89-172-71-66.adsl.net.t-com.hr)
08:05:51 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
08:10:12 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
08:11:24 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 276 seconds)
08:13:15 hawer joins (~newyear@2.219.56.221)
08:18:37 swistak joins (~swistak@185.21.216.141)
08:24:07 × acidjnk_new quits (~acidjnk@p200300d6e7283f533582140b26ca98c6.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
08:25:09 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
08:30:21 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds)
08:30:59 tnt1 joins (~Thunderbi@user/tnt1)
08:31:27 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
08:32:01 acidjnk_new joins (~acidjnk@p200300d6e7283f533582140b26ca98c6.dip0.t-ipconnect.de)
08:32:36 euleritian joins (~euleritia@dynamic-176-006-136-008.176.6.pool.telefonica.de)
08:33:14 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:41:21 kuribas joins (~user@2a02:1808:80:3b72:47fa:cf83:67e6:7339)
08:41:53 eL_Bart0 joins (eL_Bart0@dietunichtguten.org)
08:44:06 <kuribas> It is possible to represent a lambda using ski combinators. Could you use this to represent a polytype (forall a. ...)?
08:44:58 <kuribas> This way you could avoid variable substitution.
08:48:00 <kuribas> "forall a.a" would be I, "forall a. a -> a" would be "S (->) I"
08:48:20 chele joins (~chele@user/chele)
08:49:28 <haskellbridge> <Bowuigi> Those definitions wouldn't work
08:49:54 × CiaoSen quits (~Jura@2a05:5800:2eb:a800:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds)
08:50:21 <haskellbridge> <Bowuigi> But type level SKI with (->) and a forall function definitely would (tho you need type lambdas)
08:50:59 merijn joins (~merijn@77.242.116.146)
08:51:51 <haskellbridge> <Bowuigi> This forall function, of kind "(k -> *) -> *", would be used like "forall (\a -> a -> a)"
08:51:58 <probie> Isn't "forall" the type level lambda?
08:52:39 <haskellbridge> <Bowuigi> No, forall is a quantifier, not a lambda
08:53:15 <haskellbridge> <Bowuigi> It can't be applied at the type level, but rather at the term level with a type application
08:54:45 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 248 seconds)
08:54:46 <haskellbridge> <Bowuigi> Either way, this type-level SKI system is somewhat impractical, so nowadays it's better to use Normalization-by-Evaluation instead, which is likely faster
08:54:52 <kuribas> forall is kind of a type level lambda
08:55:46 <kuribas> It's just applied implicitly when using HM inference.
08:56:54 <haskellbridge> <Bowuigi> It's a binder, like a lambda, but it can't be applied at the type level like a type lambda
08:57:28 <haskellbridge> <Bowuigi> Here, binder means "brings a new variable into scope"
08:59:28 <haskellbridge> <Bowuigi> HM can infer type applications, which occur at the term level and instance foralls at the type level. Type level application works directly at the type level, no terms are involved
09:00:03 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
09:00:49 <probie> I think Bowuigi is right. If I have a function `Λα.λ(x:α).x` it has type `forall α. α -> α`. The `forall` isn't any kind of lambda, it just "lines up" with them. If it was a lambda, you'd be able to apply it, but I can't say `(forall a . Maybe a) Int` to mean `Maybe Int`
09:01:02 swistak joins (~swistak@185.21.216.141)
09:01:18 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds)
09:01:18 × kuribas quits (~user@2a02:1808:80:3b72:47fa:cf83:67e6:7339) (Ping timeout: 272 seconds)
09:01:39 <tomsmeding> I think kuribas (who left) was talking about applying them on the type level, not on the value level
09:02:15 <tomsmeding> and you can, to a certain extent -- only if the forall is on a newtype
09:02:22 <tomsmeding> % type I = forall a. a -> a
09:02:22 <yahb2> <no output>
09:02:29 <tomsmeding> % :k I @Int
09:02:29 <yahb2> <interactive>:1:1: error: [GHC-20967] ; • Cannot apply function of kind ‘*’ ; to visible kind argument ‘Int’ ; • In the type ‘I @Int’
09:03:12 <haskellbridge> <Bowuigi> Yeah mixing foralls and type level lambdas happens sometimes
09:03:39 <tomsmeding> well sometimes it looks like you _can_ apply them with TypeApplications
09:03:43 <tomsmeding> just not in enough cases for this to work
09:03:57 × gorignak quits (~gorignak@user/gorignak) (Read error: Connection reset by peer)
09:04:26 <tomsmeding> % :t map
09:04:26 <yahb2> map :: forall a b. (a -> b) -> [a] -> [b]
09:04:31 <tomsmeding> % :t map @Int
09:04:31 <yahb2> map @Int :: forall b. (Int -> b) -> [Int] -> [b]
09:04:36 <tomsmeding> I just applied a forall
09:04:41 <tomsmeding> kinda
09:04:41 <haskellbridge> <Bowuigi> "type I = forall (a :: k). ()" should work tho, because you are instancing the k
09:05:02 gorignak joins (~gorignak@user/gorignak)
09:05:03 <tomsmeding> % type I = forall (a :: k). ()
09:05:03 <yahb2> <interactive>:19:23: error: [GHC-76037] ; Not in scope: type variable ‘k’
09:05:06 <tomsmeding> % :set -XPolyKinds
09:05:06 <yahb2> <no output>
09:05:08 <tomsmeding> % type I = forall (a :: k). ()
09:05:08 <yahb2> <interactive>:23:23: error: [GHC-76037] ; Not in scope: type variable ‘k’
09:05:13 <tomsmeding> % type I = forall k (a :: k). ()
09:05:13 <yahb2> <no output>
09:05:15 <tomsmeding> and then?
09:05:22 <tomsmeding> % :k I @Int
09:05:22 <yahb2> <interactive>:1:1: error: [GHC-20967] ; • Cannot apply function of kind ‘*’ ; to visible kind argument ‘Int’ ; • In the type ‘I @Int’
09:05:28 × acidjnk_new quits (~acidjnk@p200300d6e7283f533582140b26ca98c6.dip0.t-ipconnect.de) (Remote host closed the connection)
09:05:47 acidjnk_new joins (~acidjnk@p200300d6e7283f539c942177b6544d5d.dip0.t-ipconnect.de)
09:06:08 <haskellbridge> <Bowuigi> Uhhh what
09:06:54 <tomsmeding> is this TypeInType biting us?
09:07:14 <haskellbridge> <Bowuigi> Oh I'm dumb, you need kind annotations
09:07:23 <haskellbridge> <Bowuigi> The forall for k goes there
09:07:24 <tomsmeding> right
09:07:35 <tomsmeding> so really foralls are _not_ lambdas :)
09:07:41 <tomsmeding> you can "apply" foralls from the level below
09:07:46 <tomsmeding> not from inside the same level
09:07:57 <haskellbridge> <Bowuigi> "type I :: forall k. *; type I = ()"
09:08:35 <haskellbridge> <Bowuigi> Yeah that's what I was trying to say
09:09:04 <tomsmeding> @tell kuribas foralls are not lambdas: you can "apply" foralls from the level below (i.e. type foralls using TypeApplications on a value; kind foralls by applying a type function), but not from inside the same level
09:09:04 <lambdabot> Consider it noted.
09:09:16 <haskellbridge> <Bowuigi> Strictly speaking you don't "apply" foralls, but rather type lambdas. Foralls are "instanced". This terminology can help distinguishing them I guess
09:09:44 <tomsmeding> instance or instantiate?
09:10:09 <haskellbridge> <Bowuigi> Wait is there a difference? I englishn't
09:10:27 <tomsmeding> is there a difference between flammable and inflammable?
09:10:36 <tomsmeding> words are different only if we assign a different meaning to them :p
09:11:10 <haskellbridge> <magic_rb> Whats the difference, cause purely from a english standpoint theyre similar.
09:11:39 <tomsmeding> (flammable and inflammable look like they should be opposites, but they mean the same thing)
09:11:45 merijn joins (~merijn@77.242.116.146)
09:11:59 <tomsmeding> (same as exclamation and inclamation, except the latter is archaic so you don't really see this one in practice)
09:12:12 <haskellbridge> <magic_rb> Wait what
09:12:21 <haskellbridge> <magic_rb> Inflammable isnt an opposite to flammable?
09:12:37 <haskellbridge> <magic_rb> Wha
09:12:42 <tomsmeding> inflammable. adjective. 1. Easily ignited and capable of burning rapidly; flammable.
09:12:52 × euleritian quits (~euleritia@dynamic-176-006-136-008.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
09:12:53 <Leary> I would only say `instantiate` here. `instance` as a verb I've only heard in (casual) coding contexts, probably from "create an instance of".
09:13:04 tomsmeding agrees with Leary
09:14:15 <tomsmeding> or perhaps in a graphics context, duplicating an object many times using rendering tricks?
09:14:38 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
09:15:20 <haskellbridge> <Bowuigi> I vaguely remember seeing both to refer to the same thing on different contexts, but instantiate sounds cooler
09:15:31 <tomsmeding> good enough reason
09:15:37 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 265 seconds)
09:15:57 <haskellbridge> <Bowuigi> Also the opposite of flammable/inflammable is fireproof, which also sounds cooler
09:16:39 <tomsmeding> or incombustible
09:17:09 <tomsmeding> more latin -> cooler?
09:17:49 <probie> more latin -> less cool
09:19:06 <haskellbridge> <Bowuigi> Objection, spanish is more latin and it's word for fireproof is ignifugo, which is cooler
09:19:09 <Hecate> in French we have "ignifugé" for fireproof
09:19:18 <Hecate> "igni" -> fire, (ignition)
09:19:23 <tomsmeding> Latinate languages unite?
09:19:42 <Hecate> "fugé" -> fugere, that which flees
09:19:49 <Hecate> makes the fire flee
09:19:56 <tomsmeding> that's cool
09:20:01 swistak joins (~swistak@185.21.216.141)
09:20:10 jespada joins (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4)
09:20:16 a0v7a9 joins (~ava079@90.156.161.73)
09:21:49 kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
09:22:14 <mauke> feuerfest
09:22:37 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Client Quit)
09:22:42 <tomsmeding> fire party
09:23:30 <mauke> please party your seatbelts
09:25:59 <c_wraith> do fireproofs end with Quod Erat Flamma?
09:28:36 × m5zs7k quits (aquares@web10.mydevil.net) (Ping timeout: 246 seconds)
09:28:53 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 248 seconds)
09:29:43 kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
09:29:53 swistak joins (~swistak@185.21.216.141)
09:31:06 <haskellbridge> <Bowuigi> Yeah, they start with "proof" too
09:33:24 <kuribas> haskellbridge: I don't care about performance, only correctness.
09:34:58 × ol0ck quits (~quassel@user/ol0ck) (Ping timeout: 245 seconds)
09:35:14 <kuribas> tomsmeding: from a dependent types viewpoint, foralls are just lambdas. In idris "forall a. ... " is the same as "{O a : _} -> ...".
09:35:53 <kuribas> It's a lambda with an erased value.
09:36:04 <tomsmeding> in a dependent type system, yes. :P
09:36:09 <tomsmeding> Haskell is not dependently-typed
09:36:15 <tomsmeding> hence foralls are _not_ just lambdas here
09:36:33 <kuribas> Sure, I mean more theoretically.
09:37:24 <tomsmeding> you're going to run into needing impredicativity, though
09:37:24 <kuribas> As in, I could represent a forall as a lambda in the underlying system
09:37:33 <tomsmeding> if you set `I = forall a. a`, then you'll want to apply I to some other combinator expression
09:37:40 <tomsmeding> so what's the universe level of that a?
09:37:47 ol0ck joins (~quassel@user/ol0ck)
09:37:57 <tomsmeding> I : Set<?> -> Set<?>
09:38:02 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds)
09:38:38 <tomsmeding> (are the universe levels called Set1, Set2, etc. in Idris too?)
09:39:14 <kuribas> idris2 doesn't have universe levels yet...
09:39:16 <kuribas> It's all Type.
09:39:24 <tomsmeding> so idris2 is inconsistent?
09:39:28 <kuribas> yeah
09:39:35 <tomsmeding> interesting
09:39:45 <tomsmeding> so idris2 has Type : Type?
09:39:53 <tomsmeding> in that case you could perhaps do this
09:40:04 <tomsmeding> but you'll only be able to write non-dependent function types this way, I think
09:40:15 <tomsmeding> ah no, that's false
09:41:21 <kuribas> It's implied that the Type of Type is Type <2>
09:41:27 <kuribas> But idris2 doesn't implement it yet.
09:43:34 <kuribas> tomsmeding: well, the forall would need to accept any kind.
09:44:08 <tomsmeding> which is precisely possible only if Type : Type
09:44:09 <tomsmeding> (iirc)
09:44:09 × swistak quits (~swistak@185.21.216.141) (Ping timeout: 260 seconds)
09:44:20 <kuribas> no: I : {a:Type} -> a -> a
09:45:01 <kuribas> tomsmeding: still not sure if using combinators or lambdas to represent foralls in an advantage though...
09:45:26 <tomsmeding> oh I see, so I would be a universe-polymorphic function
09:45:26 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2)
09:45:35 <tomsmeding> I think it isn't at all :p
09:45:42 <tomsmeding> but a fun exercise perhaps
09:45:49 <kuribas> idk, how does that work in agda?
09:46:02 <kuribas> If you have an implicit, does it work in all universes?
09:46:10 <tomsmeding> I : (l : Level) -> (a : Set l) -> a -> a
09:46:13 <tomsmeding> iirc
09:46:33 <kuribas> Doesn't idris1 have an inferred universe level?
09:46:47 <tomsmeding> agda certainly also has implicit inferred universe levels
09:47:11 m5zs7k joins (aquares@web10.mydevil.net)
09:47:23 <tomsmeding> but the question is: shouldn't it be "I : (l : Level) -> (a : Set l) -> Set ; I l a = a -> a"
09:47:59 <tomsmeding> hm, "-> Set l", perhaps
09:49:10 <kuribas> yeah, I haven't worked with universes yet...
09:49:20 <kuribas> But in my case, level 1 would just work.
09:50:19 <tomsmeding> is I "a -> a"? or is I just "a"?
09:50:22 <tomsmeding> what is S?
09:50:42 <kuribas> a -> a
09:50:50 merijn joins (~merijn@77.242.116.146)
09:50:59 <tomsmeding> but then you aren't actually applying types, are you? What is S?
09:51:04 __monty__ joins (~toonn@user/toonn)
09:52:07 <kuribas> tomsmeding: not in the implementing language.
09:52:28 <tomsmeding> wasn't the premise that you can write types using combinators instead of foralls?
09:53:29 <kuribas> Yeah, in the implementing language. Like HOAS.
09:53:39 <kuribas> polymorphic types.
09:54:15 <tomsmeding> so then how are you going to write the type "(f : Type -> Type) -> (a : Type) -> f a"?
09:54:45 <tomsmeding> never mind that this type doesn't have a sensible implementation, but more complicated such examples do
09:56:57 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds)
09:57:19 <kuribas> tomsmeding: not exactly sure, I'll need to work it out...
09:58:06 <kuribas> gotto do my day job now :)
09:58:23 <kuribas> Python and clojure :(
09:58:34 <tomsmeding> :D
10:01:22 × xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
10:09:50 <smiesner> *laughs in java and js* (pls free me)
10:10:13 merijn joins (~merijn@77.242.116.146)
10:14:32 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds)
10:24:39 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 252 seconds)
10:27:55 merijn joins (~merijn@77.242.116.146)
10:32:28 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds)
10:33:06 merijn joins (~merijn@77.242.116.146)
10:35:05 × jespada quits (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Quit: My Mac has gone to sleep. ZZZzzz…)
10:37:08 sprotte24 joins (~sprotte24@p200300d16f2d390001157685e299ee37.dip0.t-ipconnect.de)
10:37:10 × sprotte24 quits (~sprotte24@p200300d16f2d390001157685e299ee37.dip0.t-ipconnect.de) (Client Quit)
10:37:19 × vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds)
10:38:45 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds)
10:38:46 vanishingideal joins (~vanishing@user/vanishingideal)
10:39:12 merijn joins (~merijn@77.242.116.146)
10:45:12 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds)
10:49:36 merijn joins (~merijn@77.242.116.146)
10:51:25 kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
10:59:03 × Miroboru quits (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal)
10:59:34 × mange quits (~user@user/mange) (Quit: Zzz...)
11:07:46 Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
11:08:19 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3))
11:08:55 kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
11:09:25 Miroboru joins (~myrvoll@178-164-114.82.3p.ntebredband.no)
11:10:04 × akegalj quits (~akegalj@89-172-71-66.adsl.net.t-com.hr) (Ping timeout: 244 seconds)
11:10:04 <kuribas> tomsmeding: I was just considering this: https://en.wikipedia.org/wiki/Higher-order_abstract_syntax
11:10:06 <tomsmeding> is HOAS not more about representing an AST?
11:13:29 xff0x joins (~xff0x@2405:6580:b080:900:5599:62cc:9825:4e0a)
11:13:59 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds)
11:16:23 Smiles joins (uid551636@id-551636.lymington.irccloud.com)
11:24:13 dysthesis joins (~dysthesis@user/dysthesis)
11:26:22 merijn joins (~merijn@77.242.116.146)
11:33:38 jespada joins (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4)
11:36:06 alexherbo2 joins (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net)
11:36:51 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
11:37:43 × dmwit quits (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net) (Quit: Client closed)
11:42:32 × alexherbo2 quits (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection)
11:43:05 alexherbo2 joins (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net)
11:47:31 × haskellbridge quits (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection)
11:48:33 haskellbridge joins (~hackager@syn-024-093-192-219.res.spectrum.com)
11:48:33 ChanServ sets mode +v haskellbridge
11:49:53 × alecs quits (~alecs@nat16.software.imdea.org) (Ping timeout: 252 seconds)
11:50:13 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds)
11:50:21 euleritian joins (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de)
11:52:48 × euphores quits (~SASL_euph@user/euphores) (Ping timeout: 246 seconds)
11:53:32 JuanDaugherty joins (~juan@user/JuanDaugherty)
11:55:07 lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
11:57:12 × dysthesis quits (~dysthesis@user/dysthesis) (Remote host closed the connection)
11:57:51 × euleritian quits (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
11:58:09 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
11:59:59 euphores joins (~SASL_euph@user/euphores)
12:00:04 × caconym quits (~caconym@user/caconym) (Quit: bye)
12:00:59 AlexNoo_ joins (~AlexNoo@178.34.163.23)
12:03:03 caconym joins (~caconym@user/caconym)
12:04:14 × AlexZenon quits (~alzenon@178.34.160.135) (Ping timeout: 244 seconds)
12:04:14 × AlexNoo quits (~AlexNoo@178.34.160.135) (Ping timeout: 252 seconds)
12:05:59 alecs joins (~alecs@nat16.software.imdea.org)
12:11:16 AlexZenon joins (~alzenon@178.34.163.23)
12:16:36 akegalj_ joins (~akegalj@89-172-71-66.adsl.net.t-com.hr)
12:17:59 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
12:26:06 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
12:28:41 __monty__ joins (~toonn@user/toonn)
12:30:18 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds)
12:30:22 AlexNoo_ is now known as AlexNoo
12:32:01 <kuribas> tomsmeding: a type is part of an AST, no?
12:34:06 <ncf> kuribas: implicits make no difference to universe levels
12:35:18 <kuribas> ncf: can I not write {n:Nat} -> {a:Type n} -> a -> a ?
12:35:19 <ncf> in Agda? you can if you replace Nat with Level
12:36:03 <ncf> this means the exact same thing as (l : Level) → (a : Type l) → a → a except you don't have to write the arguments explicitly
12:38:35 × ephemient quits (uid407513@user/ephemient) (Quit: Connection closed for inactivity)
12:38:37 <kuribas> https://docs.idris-lang.org/en/latest/faq/faq.html#does-idris-have-universe-polymorphism-what-is-the-type-of-type
12:40:53 <ncf> idris 2 has Type : Type. you don't need universe polymorphism if there's only one universe!
12:41:46 <kuribas> ncf: not by design. I think universes are simply not yet implemented.
12:41:46 merijn joins (~merijn@77.242.116.146)
12:49:55 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 264 seconds)
12:50:30 × Putonlalla quits (~Putonlall@it-cyan.it.jyu.fi) (Ping timeout: 252 seconds)
12:59:00 × tv quits (~tv@user/tv) (Read error: Connection reset by peer)
12:59:36 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty)
13:00:27 <tomsmeding> kuribas: a type is part of an AST, yes, but then you're talking about describing types in an embedded language, not in the host language. :p
13:00:41 <tomsmeding> and then the question is, how strong is the type system of your embedded language
13:01:19 merijn joins (~merijn@77.242.116.146)
13:03:43 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
13:05:06 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
13:07:09 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds)
13:12:56 <kuribas> tomsmeding: yeah, maybe this doesn't make sense outside logic languages like twelf.
13:13:11 <kuribas> tomsmeding: My goal is to make a type checker in clojure, but I wanted to verify it in idris/agda first.
13:19:43 tv joins (~tv@user/tv)
13:21:02 merijn joins (~merijn@77.242.116.146)
13:23:15 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
13:25:52 Putonlalla joins (~Putonlall@it-cyan.it.jyu.fi)
13:26:49 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
13:28:54 × Fischmiep quits (~Fischmiep@user/Fischmiep) (Quit: ZNC - https://znc.in)
13:29:13 merijn joins (~merijn@77.242.116.146)
13:29:26 Fischmiep joins (~Fischmiep@user/Fischmiep)
13:33:23 <hellwolf> ls
13:33:23 <hellwolf> (sorry, wrong window)
13:34:49 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds)
13:37:53 × tjbc quits (~tjbc@user/fliife) (Quit: ZNC - https://znc.in)
13:39:01 tjbc joins (~tjbc@user/fliife)
13:44:23 <kuribas> hello_hellwolf.com helmsucks.yaml solves_halting_problem.hs get_rich_with_blockchain.rs
13:45:51 <Hecate> haha
13:46:44 × akegalj_ quits (~akegalj@89-172-71-66.adsl.net.t-com.hr) (Ping timeout: 248 seconds)
13:46:58 merijn joins (~merijn@77.242.116.146)
13:49:58 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
13:55:27 × alexherbo2 quits (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection)
13:55:47 alexherbo2 joins (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net)
13:56:10 weary-traveler joins (~user@user/user363627)
13:56:16 × michalz quits (~michalz@185.246.207.197) (Read error: Connection reset by peer)
13:56:18 michalz_ joins (~michalz@185.246.207.203)
13:59:38 TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
13:59:55 <hellwolf> yea yea, next time sudo with password
14:03:06 × ThePenguin quits (~ThePengui@cust-95-80-24-166.csbnet.se) (Remote host closed the connection)
14:05:47 ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:28c7:5c1b:9c00:9e1b)
14:08:00 ThePenguin joins (~ThePengui@cust-95-80-24-166.csbnet.se)
14:08:46 × vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds)
14:11:16 vanishingideal joins (~vanishing@user/vanishingideal)
14:11:44 <kuribas> hellwolf: did you finally find a way to use diagrams from a shell command?
14:11:51 <kuribas> To make a work cloud?
14:13:07 × vanishingideal quits (~vanishing@user/vanishingideal) (Client Quit)
14:13:40 <hellwolf> am I expected to such an endeavor, ever?
14:14:01 <hellwolf> btw, you name looks familiar, by my memory failing me :D
14:15:28 <kuribas> hellwolf: you were working on it on munihac :)
14:17:36 <hellwolf> ah, now I remember you! No, I haven't gone back to THSH to publish it yet!
14:19:23 <kuribas> I see. It was a nice project.
14:19:44 × ThePenguin quits (~ThePengui@cust-95-80-24-166.csbnet.se) (Remote host closed the connection)
14:21:10 <hellwolf> just a small pause; I will use THSH in my main project, so I have a reason to maintain it.
14:21:16 <hellwolf> I hope your SQL DSL working out though.
14:21:24 <kuribas> I haven't worked on it either.
14:21:34 <kuribas> I gave a talk at FP dag though :)
14:21:57 <hellwolf> FP dag in Munich?
14:21:57 <kuribas> I wanted to work this holiday, but I could a bad flu.
14:21:58 <kuribas> No, FP dag in Leuven, Belgium.?
14:22:20 <kuribas> Where I finally met tomsmeding in person :)
14:22:23 <hellwolf> okay, just a guess of mine, I didn't know of it. And I assumed "dag" means "day".
14:22:37 <kuribas> Yeah, it's the "dutch FP day" or something.
14:22:51 <hellwolf> small world. I hope we all meet at ZuriHac again
14:23:00 <kuribas> We might be!
14:23:06 <hellwolf> you know they ahve the page ready, but not announced. I had a sneak peak at it.
14:23:17 <kuribas> I learned there are only two companies doing haskell in Belgium...
14:23:48 <hellwolf> plural is qualitatively different than sigular!
14:23:51 <hellwolf> in the sense of NonEmpty list in Haskell... too
14:24:05 <hellwolf> (to keep on-topic)
14:24:07 <hellwolf> :D
14:24:12 <kuribas> I did a script in haskell here, but it will be rewritten in clojure and Python...
14:24:36 <__monty__> kuribas: Which two? I know about WD in Gent.
14:25:21 <hellwolf> people don't want good things for them, it's too painful.
14:25:39 <kuribas> __monty__: central app, by Ashesh Ambasta, and pieSync
14:25:44 <kuribas> hellwolf: it feels that way.
14:25:48 <hellwolf> "it will be", but that day may never come: as you as you can keep the "if it works, don't touch it or ask you"
14:26:16 <kuribas> I am struggling with the Python debugger in vscode, I would expect more quality from a product used by millions.
14:26:46 <kuribas> __monty__: Western Digital?
14:27:22 <__monty__> Yeah, they used to come to the HUG in Leuven.
14:27:30 ThePenguin joins (~ThePengui@cust-95-80-24-166.csbnet.se)
14:29:44 <hellwolf> what do you want from a debugger, is the breakpoint working for you?
14:29:44 <hellwolf> (python debugger)
14:29:45 <kuribas> hellwolf: sometimes
14:29:45 <hellwolf> huh?
14:29:56 <hellwolf> dependently debuggable
14:30:01 <kuribas> We have code with a lot of dataframes, I find it hard to keep the right fields in my head.
14:30:12 <kuribas> So I trace through it find the problem.
14:30:36 <kuribas> For that reason, I prefer dataclasses, they can be typechecked.
14:31:25 <kuribas> I put a breakpoint in the code, but sometimes the debugger just hangs, sometimes it doesn't stop at the breakpoint, etc...
14:34:23 <hellwolf> sounds incredulous, there must be an explanation if your colleague also using it.
14:34:23 <kuribas> On a positive note, I do think functional programming is more and more adopted in other languages.
14:34:30 <kuribas> hellwolf: they use pycharm...
14:36:22 <hellwolf> sounds like it should be a charming experience.
14:36:32 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
14:39:31 rekahsoft joins (~rekahsoft@70.51.99.237)
14:42:58 × SlackCoder quits (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving)
14:44:04 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
14:49:16 j1n37 joins (~j1n37@user/j1n37)
14:50:55 dmwit joins (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net)
14:54:40 <kuribas> I am not charmed yet, but maybe I should be...
14:56:13 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds)
14:57:49 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds)
14:59:27 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
15:06:13 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds)
15:06:40 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
15:07:17 euleritian joins (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de)
15:08:02 <kuribas> Are there other FP languages that are popular in Belgium?
15:08:13 <kuribas> Ocaml, F#, scala, ...
15:08:16 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
15:08:46 <kuribas> I suppose scala is a bit more popular.
15:09:25 × _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 265 seconds)
15:09:25 merijn joins (~merijn@77.242.116.146)
15:09:25 × ystael quits (~ystael@user/ystael) (Read error: Connection reset by peer)
15:10:28 ystael joins (~ystael@user/ystael)
15:11:11 <haskellbridge> <Morj> Coq/rocq? But I'm saying this because of proximity to france
15:11:14 <hellwolf> do people count rust as FP? Unironically, FPCompete completes itself with rust
15:11:19 _d0t joins (~{-d0t-}@user/-d0t-/x-7915216)
15:11:24 <hellwolf> (not from belgium, sorry, just ranting)
15:11:54 <haskellbridge> <Morj> I was looking for ocaml positions in France recently, and they were all secretly for coq
15:11:56 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2)
15:12:32 <[exa]> I read some memes that Coq got renamed, is that true? (didn't really check)
15:13:54 × xdminsy quits (~xdminsy@117.147.71.200) (Ping timeout: 272 seconds)
15:13:54 <[exa]> __monty__: there are any bugger haskell user groups in benelux? are there any links/sites? (I failed googling that)
15:13:54 <[exa]> *bIgger
15:13:54 <[exa]> ayay.
15:14:33 <haskellbridge> <Morj> > Coq got renamedThe website is still coq.inria.fr
15:15:33 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds)
15:15:33 <[exa]> oh I see: The Coq team has decided that Coq will be renamed into 'The Rocq Prover'.
15:17:26 <hellwolf> https://coq.discourse.group/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001#renaming-coq-8
15:17:41 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
15:17:57 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
15:18:23 <hellwolf> It doesn't seem to have been actioned!
15:20:11 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
15:22:00 × chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
15:23:20 chexum joins (~quassel@gateway/tor-sasl/chexum)
15:25:36 merijn joins (~merijn@77.242.116.146)
15:27:36 <kuribas> haskellbridge: They were secretly using coq instead?
15:27:43 <kuribas> Maybe I should find a job in France...
15:31:21 <kuribas> coq compiles to ocaml, doesn't it?
15:31:25 ft joins (~ft@p4fc2a354.dip0.t-ipconnect.de)
15:34:14 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
15:34:24 <haskellbridge> <Morj> Coq can extract programs to multiple languages, including ocaml and haskell. Coq itself is writte in ocaml
15:35:10 × turlando quits (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.)
15:35:58 × alexherbo2 quits (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection)
15:36:26 turlando joins (~turlando@user/turlando)
15:38:14 weary-traveler joins (~user@user/user363627)
15:40:11 <__monty__> [exa]: I think the Leuven HUG kinda stopped meeting? And if people were coming from Gent to Leuven I kinda feel like the answer is no, at least for Flanders. I don't know about the NeLux part of that though, Merijn and tomsmeding might know for NL?
15:41:03 <__monty__> Either way, my info dates back 7-ish years. So I don't have current info.
15:41:06 × Digit quits (~user@user/digit) (Remote host closed the connection)
15:41:43 <merijn> I don't really go to more frequent things than NL-FP :p
15:44:32 inedia joins (~irc@2600:3c00:e000:287::1)
15:52:41 JuanDaugherty joins (~juan@user/JuanDaugherty)
15:56:40 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
15:59:24 × jespada quits (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Quit: My Mac has gone to sleep. ZZZzzz…)
16:00:34 merijn joins (~merijn@77.242.116.146)
16:04:16 × euleritian quits (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
16:04:34 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
16:10:07 Digit joins (~user@user/digit)
16:15:12 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty)
16:19:46 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
16:20:16 <haskellbridge> <Bowuigi> kuribas re:dependent-type-forall even from a dependent type viewpoint, foralls are not lambdas, but it unifies type lambdas and term lambdas (both term level constructs) into one
16:20:26 euleritian joins (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de)
16:20:45 <haskellbridge> <Bowuigi> The note on erasure is correct tho IIRC
16:21:14 × Square2 quits (~Square4@user/square) (Ping timeout: 248 seconds)
16:21:34 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
16:22:37 × euleritian quits (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
16:22:50 euleritian joins (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de)
16:27:20 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
16:27:47 × euleritian quits (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
16:27:50 rvalue joins (~rvalue@user/rvalue)
16:28:05 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
16:30:32 <haskellbridge> <Bowuigi> The type level combinator system ypu proposed simply wouldn't work. Lemme show you why: Suppose we want to know the type that "I I" expands to. Unfolding everything, using the definition you gave for I ("forall a. a -> a") leaves you with "(forall a. a -> a) (forall a. a -> a)". This term is not well kinded, as you are trying to apply a type of term * to another of term *
16:34:22 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 252 seconds)
16:35:41 <haskellbridge> <Bowuigi> Instead, combinators should be defined in the usual way but at the type level, using type level lambdas. To get arrows and forall you just add them as combinators, same for pairs, sums, pi types, sigma types, propositional equality types, constraints (the arrow is a "Constraint -> * -> *" operator), etc
16:36:48 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds)
16:37:30 euleritian joins (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de)
16:41:53 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
16:43:34 × EvanR quits (~EvanR@user/evanr) (Remote host closed the connection)
16:43:54 EvanR joins (~EvanR@user/evanr)
16:49:06 jespada joins (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4)
16:50:44 vanishingideal joins (~vanishing@user/vanishingideal)
16:56:08 <dolio> There are some papers on making lambda and pi the same. But they seem misguided to me.
16:56:58 <dolio> Since Π is not the only quantifier when you start getting into such things.
16:57:36 lbseale joins (~quassel@user/ep1ctetus)
17:05:16 × dmwit quits (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net) (Quit: Client closed)
17:11:48 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
17:11:49 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
17:16:40 <kuribas> haskellbridge: but they are in idris2
17:17:06 <kuribas> AFAIK "forall a.A" is sugar for "{0 a} -> A".
17:17:24 <kuribas> Which is a Pi type.
17:19:27 <kuribas> haskellbridge: "forall a. a -> a" has term "* -> *", but the first argument is implicit, so inferred by the compiler.
17:20:44 <kuribas> haskellbridge: oh, and I is (forall a . a).
17:21:34 ljdarj joins (~Thunderbi@user/ljdarj)
17:21:34 × euleritian quits (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
17:21:34 <kuribas> Or {0 a} -> a
17:21:47 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
17:24:54 target_i joins (~target_i@user/target-i/x-6023099)
17:26:36 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
17:28:18 euleritian joins (~euleritia@dynamic-176-004-140-090.176.4.pool.telefonica.de)
17:28:45 <geekosaur> why are you talking to the bridge instead of the person on the other side of it?
17:29:46 <kuribas> geekosaur: TIL :)
17:29:59 <int-e> geekosaur: tab-completion actually works for the bridge ;)
17:30:00 <geekosaur> (the person on the other side of the bridge has no idea what "haskellbridge" is, it only shows on IRC)
17:30:06 <geekosaur> yeh
17:30:23 r-sta joins (~r-sta@sgyl-37-b2-v4wan-168528-cust2421.vm6.cable.virginm.net)
17:30:34 <geekosaur> I'm considering switching to matrix-appservice-irc so users are puppeted on both sides instead of just the matrix side
17:31:24 <r-sta> so im still stuck trying to find out how to debug this <<loop>> in my program
17:31:24 <r-sta> i saw some kind of tree representation or something with -prof
17:31:28 kuribas GTG
17:31:31 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3))
17:31:35 <r-sta> i tried using breaks and stepping but it didnt work at all! it didnt even make it *to* the <<loop>>
17:32:23 <r-sta> i was concerned that any kind of diagram would need a fully compiling thing
17:32:33 <geekosaur> you might want `-fbreak-on-error` instead; some things use exceptions internally and usually you don't want ghci stopping in that case
17:33:03 <geekosaur> (`-fbreak-on-error` only breaks on unhandled exceptions)
17:33:03 <r-sta> i used that but it broke on another error that it didnt have when not using -fbreak-on-error
17:33:08 <r-sta> so it didnt make it to the <<loop>>
17:33:19 × euleritian quits (~euleritia@dynamic-176-004-140-090.176.4.pool.telefonica.de) (Read error: Connection reset by peer)
17:33:27 <r-sta> and that other error was not present when not using -fbreak-on-exception
17:33:42 <r-sta> error*
17:34:06 <r-sta> wait what. are these different things?
17:34:08 <r-sta> hmm
17:34:39 <c_wraith> Remember, <<loop>> is what ghc prints. it's not the error itself.
17:34:53 <r-sta> can i just turn that off?
17:34:59 <r-sta> like, just have it do the loop
17:35:01 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
17:35:14 <geekosaur> no, because it's by definition infinite
17:35:33 <geekosaur> <<loop>> means that when STG tries to evaluate a thunk, it immediately re-evaluates itself
17:35:40 <c_wraith> it's not just infinite, it's circular.
17:36:17 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
17:36:17 <geekosaur> and yes, break-on-exception and break-on-error are two different things
17:36:17 <c_wraith> Like, the result depends on itself, not on some other infinite calculation
17:36:18 euleritian joins (~euleritia@dynamic-176-004-140-090.176.4.pool.telefonica.de)
17:36:18 <geekosaur> -exception is all exceptions, -error is exceptions nto caught by a handler
17:36:18 × euleritian quits (~euleritia@dynamic-176-004-140-090.176.4.pool.telefonica.de) (Read error: Connection reset by peer)
17:36:34 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
17:36:35 <r-sta> i cant see if i might have been using break-on-exception
17:36:40 <r-sta> hopefully its an easy fix
17:37:55 <c_wraith> fwiw, my experience is that <<loop>>-causing issues are best found by simple inspection. The form of code that can cause them is pretty limited.
17:38:38 <geekosaur> that's why I raised `let x = x + 1` yesterday, that's a classic <<loop>>
17:39:03 <geekosaur> because the first thing `x` does is evaluate `x`
17:39:35 <c_wraith> though i guess the first step is compiling with -Wall and looking for shadowing warnings.
17:40:23 <r-sta> so, break-on-error crashes ghci so i cant step through it or do :list
17:40:33 <r-sta> Access violation in generated code when executing data at 0x7ff79a7ce1a0
17:40:33 <r-sta>  Attempting to reconstruct a stack trace...
17:40:34 <r-sta>    Frame Code address
17:40:34 <r-sta>  * 0x4ed0afd880 0x7ff79a7ce1a0
17:40:38 <r-sta> it just puts this garbage
17:41:17 <r-sta> "shadowing warnings" hmm
17:42:50 <c_wraith> One common cause of <<loop>> is let x = x + 1 types of bindings where you think the inner `x' refers to a previously bound value. Shadowing warnings will catch all of those.
17:42:50 <r-sta> I KNOW
17:43:03 <r-sta> sry
17:43:09 <r-sta> i just dont know where it is!
17:43:27 <geekosaur> "break-on-error crashes ghci" -- file a GHC bug please
17:43:35 <r-sta> derp
17:43:45 <r-sta> its complaining about lapack and hmatrix
17:44:24 <r-sta> there is a flag in my cabal file that tells it to use like hopenblas or smt
17:44:24 <r-sta> it creates an error when ghci is opened from the comand line
17:44:27 <r-sta> i think it *might* be similar
17:44:39 <r-sta> if its some *insane* linker thing from blas ill cry
17:44:52 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
17:45:33 <r-sta> package hmatrix
17:45:33 <r-sta>   flags: +openblas
17:46:03 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
17:46:03 × paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 252 seconds)
17:46:11 <r-sta> typing ghci at cmd results in;
17:46:12 <r-sta> ghc-9.4.8.exe: Could not load `libopenblas.dll'. Reason: addDLL: libopenblas.dll or dependencies not loaded. (Win32 error 126)
17:46:12 <r-sta> panic! (the 'impossible' happened)
17:46:13 <r-sta>   GHC version 9.4.8:
17:46:13 <r-sta>         loadArchive "C:\\ghcup\\msys64\\mingw64\\lib\\libopenblas.dll.a": failed
17:46:24 <r-sta> i have to use the cabal proj with the +openblas flag
17:46:41 <r-sta> now its going crazy about some error that i cant figure out at all
17:46:53 <r-sta> break-on-error points to hmatrix
17:47:35 × haritz quits (~hrtz@user/haritz) (Read error: Connection reset by peer)
17:48:40 haritz joins (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737)
17:48:43 × haritz quits (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) (Changing host)
17:48:43 haritz joins (~hrtz@user/haritz)
17:51:38 × sam113101 quits (~sam@modemcable220.199-203-24.mc.videotron.ca) (Quit: WeeChat 4.4.4)
17:51:56 <r-sta> Access violation in generated code when executing data at 0x7ff79a7ce1a0
17:52:24 <r-sta>  Attempting to reconstruct a stack trace...
17:52:25 <r-sta>    Frame Code address
17:52:25 <r-sta>  * 0x71107fda50 0x7ff79a7ce1a0
17:52:25 <r-sta>  * 0x71107fda58 0x7ff792d524ca C:\cabal\store\ghc-9.4.8\hmatrix-0.20.2-4cdbde37f45231e81ec073ef0dcbf107a90a6d6b\lib\libHShmatrix-0.20.2-4cdbde37f45231e81ec073ef0dcbf107a90a6d6b.a(#28:lapack-aux.o)+0x24ba
17:52:32 <r-sta> lapack this, hmatrix that
17:53:04 <r-sta> its a crazy error iv never seen before, i just thought it was typical result for break-on-error
17:53:17 <r-sta> but when i use break-on-exception it gives me a well behaved repl still
17:53:25 <r-sta> and i can use :list
17:53:30 <geekosaur> no, that's usually FFI going wrong and the program crashing at the OS level
17:54:03 <r-sta> balls
17:54:03 <r-sta> right well at least i know im not going to fix that
17:54:08 <geekosaur> the loadArchive error is probably hopenblas needing `library-for-ghci: true`
17:54:33 <r-sta> can i put this in my cabal.proj?
17:54:57 econo_ joins (uid147250@id-147250.tinside.irccloud.com)
17:56:25 sam113101 joins (~sam@modemcable220.199-203-24.mc.videotron.ca)
17:56:34 <r-sta> anyway its a nasty bug
17:56:46 <r-sta> i could put the whole proj for it to be reproducable
17:57:17 <r-sta> but its like, idk, kinda a lot of work that i might not want to share cf competition
17:57:39 <r-sta> id put a link on a private chat that isnt logged to someone with a common name from the forum
17:57:57 <r-sta> if there was a "want to do the bugfix" perogative
17:58:55 <geekosaur> https://paste.tomsmeding.com/eeUPJWNF project file fragment
18:00:35 <r-sta> first attempt fails
18:00:36 <r-sta> going to fully recompile to see if that makes a difference
18:00:40 <r-sta> but just adding that to the cabal file does not change the result at all
18:02:09 <r-sta> i mean, like, rather than putting the full project in a repo
18:02:20 <r-sta> id rather like, elect modules to put on hackage and find people to help maintain them
18:02:43 <r-sta> there is a really strong hypervarience model which i think is practically impossible to outperform locally
18:02:59 <r-sta> would be great to get the comunity into using tools like that
18:03:08 srazkvt joins (~sarah@user/srazkvt)
18:03:55 <r-sta> if there was some chance of people helping actually like, branch the project (fork?) then i could put the thing in a repo, and see if anyone else can have better luck profiling or finding this damn <<loop>> which must be technically possible...
18:04:12 <r-sta> but its releasing a lot of IP onto the unliscenced webs
18:04:34 <r-sta> depends on colaboration viability
18:05:21 <r-sta> idk if thats something i can choose on your behalf and just put the project, so ill wait for feedback
18:06:23 × srazkvt quits (~sarah@user/srazkvt) (Client Quit)
18:09:05 <r-sta> ...
18:09:08 <r-sta> ok ill put the repo
18:09:30 <r-sta> you know what this is like, when youv been waiting for a bus for ages and you get loads of errors in like every system
18:11:47 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
18:12:47 <r-sta> lol, i mean, im realeasing something that does nothing except give the most difficult to reproduce error!
18:12:59 <r-sta> but the theory under the hood is redicuous
18:13:31 saulosilva joins (~saulosilv@181.216.220.107)
18:15:06 <r-sta> https://github.com/munston/starship
18:15:06 <r-sta> ok. now its larger than the github drag and drop allows so iv had to zip it
18:15:11 <r-sta> but i mean, it can be maintained better...
18:15:44 × dontdieych2 quits (~quassel@user/dontdieych2) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
18:16:01 dontdieych2 joins (~quassel@user/dontdieych2)
18:16:45 <r-sta> the good bit is the aliens learning method. peace out
18:16:47 × r-sta quits (~r-sta@sgyl-37-b2-v4wan-168528-cust2421.vm6.cable.virginm.net) (Quit: Client closed)
18:19:11 Guest37 joins (~Guest37@2a02:ff0:332a:649b:3817:74af:208c:aa2c)
18:19:22 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
18:19:28 × Guest37 quits (~Guest37@2a02:ff0:332a:649b:3817:74af:208c:aa2c) (Client Quit)
18:20:34 × jespada quits (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Quit: My Mac has gone to sleep. ZZZzzz…)
18:24:21 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
18:27:00 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
18:35:08 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
18:36:55 × chele quits (~chele@user/chele) (Remote host closed the connection)
18:38:20 Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
18:39:39 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 272 seconds)
18:39:58 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
18:40:39 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
18:41:53 Lord_of_Life_ is now known as Lord_of_Life
18:41:53 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
18:41:53 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
18:42:02 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
18:48:54 × bionade24 quits (~quassel@2a03:4000:33:45b::1) (Quit: Apocalypse Incoming!)
18:49:05 bionade24 joins (~quassel@2a03:4000:33:45b::1)
18:49:55 lxsameer joins (~lxsameer@Serene/lxsameer)
18:50:07 × nicole quits (ilbelkyr@libera/staff/ilbelkyr) (Quit: Lost terminal)
18:50:35 nicole joins (ilbelkyr@libera/staff/ilbelkyr)
18:53:20 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
18:55:08 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 265 seconds)
18:55:34 pavonia joins (~user@user/siracusa)
18:57:28 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
18:57:43 × saulosilva quits (~saulosilv@181.216.220.107) (Quit: Client closed)
19:05:28 × Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
19:07:27 paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt)
19:08:35 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
19:11:01 tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
19:15:31 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
19:17:09 jespada joins (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4)
19:18:51 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en)
19:21:11 × jespada quits (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Client Quit)
19:26:09 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
19:26:35 × dtman34 quits (~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) (Ping timeout: 252 seconds)
19:28:23 × bliminse quits (~bliminse@user/bliminse) (Quit: leaving)
19:30:26 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
19:30:26 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
19:32:18 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
19:36:33 JuanDaugherty joins (~juan@user/JuanDaugherty)
19:45:21 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
19:46:30 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
19:47:30 Square2 joins (~Square4@user/square)
19:50:33 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
19:50:50 sprotte24 joins (~sprotte24@p200300d16f2d39009dedd0cca2feaedd.dip0.t-ipconnect.de)
19:53:03 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
19:55:30 ljdarj1 joins (~Thunderbi@user/ljdarj)
19:59:21 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 264 seconds)
19:59:21 ljdarj1 is now known as ljdarj
19:59:21 dtman34 joins (~dtman34@2601:447:d080:1a3c:e8b1:d264:a50b:db46)
20:00:02 × caconym quits (~caconym@user/caconym) (Quit: bye)
20:00:55 caconym joins (~caconym@user/caconym)
20:01:43 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:02:51 bliminse joins (~bliminse@user/bliminse)
20:03:07 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
20:08:48 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
20:08:59 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
20:10:18 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
20:10:59 <tomsmeding> __monty__: there is an attempt to have a haskell meetup in Utrecht once in a while, but it's somewhat infrequent
20:11:19 <tomsmeding> there's not too much of a "social" haskell scene in that sense, as far as I know
20:12:20 × xdej_ quits (~xdej@quatramaran.salle-s.org) (Remote host closed the connection)
20:12:24 <[exa]> __monty__: ah ok, I see
20:13:35 × int-e quits (~noone@int-e.eu) (Remote host closed the connection)
20:14:13 int-e joins (~noone@int-e.eu)
20:14:50 × lambdabot quits (~lambdabot@haskell/bot/lambdabot) (Remote host closed the connection)
20:15:19 lambdabot joins (~lambdabot@haskell/bot/lambdabot)
20:15:19 ChanServ sets mode +v lambdabot
20:18:08 Midjak joins (~MarciZ@82.66.147.146)
20:18:27 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
20:19:37 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:19:37 × paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 276 seconds)
20:24:15 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
20:24:15 xdminsy joins (~xdminsy@117.147.71.200)
20:26:29 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
20:27:37 × a0v7a9 quits (~ava079@90.156.161.73) (Quit: Leaving)
20:28:13 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
20:28:16 <haskellbridge> <magic_rb> Im always down for another utrecht haskell meet
20:28:52 <haskellbridge> <magic_rb> Someone just needs to tell me when and where and ill be there
20:28:55 <tomsmeding> magic_rb: if you're a member of the meetup group then in principle you should get notification emails when one is scheduler
20:28:58 <tomsmeding> *scheduled
20:29:11 <haskellbridge> <magic_rb> I do and i am
20:29:39 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
20:30:40 paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt)
20:35:27 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds)
20:37:21 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:39:50 × paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 276 seconds)
20:41:56 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
20:52:42 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:56:52 × hsw_ quits (~hsw@112-104-8-145.adsl.dynamic.seed.net.tw) (Remote host closed the connection)
20:57:07 hsw_ joins (~hsw@112-104-8-145.adsl.dynamic.seed.net.tw)
20:57:25 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
20:57:51 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en)
20:59:13 × dtman34 quits (~dtman34@2601:447:d080:1a3c:e8b1:d264:a50b:db46) (Ping timeout: 244 seconds)
21:00:00 × jle` quits (~jle`@2603:8001:3b02:84d4:68b0:c2d1:4ed0:1ad6) (Ping timeout: 252 seconds)
21:01:00 jle` joins (~jle`@2603:8001:3b02:84d4:90eb:bd2f:bbf5:f0d8)
21:02:28 × euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
21:03:09 euleritian joins (~euleritia@dynamic-176-006-128-233.176.6.pool.telefonica.de)
21:08:03 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
21:09:27 dtman34 joins (~dtman34@c-76-156-64-77.hsd1.mn.comcast.net)
21:14:36 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
21:15:13 × paul_j quits (~user@8.190.187.81.in-addr.arpa) (Remote host closed the connection)
21:25:22 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
21:29:20 × michalz_ quits (~michalz@185.246.207.203) (Remote host closed the connection)
21:30:10 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
21:31:45 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
21:35:59 × dtman34 quits (~dtman34@c-76-156-64-77.hsd1.mn.comcast.net) (Read error: Connection reset by peer)
21:36:09 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
21:40:44 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
21:43:55 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty)
21:44:59 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
21:47:45 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
21:47:49 dtman34 joins (~dtman34@c-76-156-64-77.hsd1.mn.comcast.net)
21:52:38 × xdminsy quits (~xdminsy@117.147.71.200) (Read error: Connection reset by peer)
21:54:08 xdminsy joins (~xdminsy@117.147.71.200)
21:55:45 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
21:56:08 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:00:42 × xdminsy quits (~xdminsy@117.147.71.200) (Read error: Connection reset by peer)
22:01:20 xdminsy joins (~xdminsy@117.147.71.200)
22:01:27 mange joins (~user@user/mange)
22:02:51 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
22:06:00 tnt2 joins (~Thunderbi@user/tnt1)
22:07:19 paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt)
22:07:44 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds)
22:08:55 tnt1 joins (~Thunderbi@user/tnt1)
22:09:23 Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
22:10:12 × tnt2 quits (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds)
22:14:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:15:48 × paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 245 seconds)
22:17:42 paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt)
22:18:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
22:22:13 × paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 248 seconds)
22:29:28 g00gler joins (uid125351@id-125351.uxbridge.irccloud.com)
22:29:32 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:32:46 lisbeths joins (uid135845@id-135845.lymington.irccloud.com)
22:34:27 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
22:35:21 dysthesis joins (~dysthesis@user/dysthesis)
22:39:17 ljdarj1 joins (~Thunderbi@user/ljdarj)
22:42:47 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
22:42:47 ljdarj1 is now known as ljdarj
22:44:55 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:49:00 Sgeo joins (~Sgeo@user/sgeo)
22:49:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
22:53:44 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:57:10 weary-traveler joins (~user@user/user363627)
22:58:34 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
22:59:20 × YuutaW quits (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (Quit: ZNC 1.9.1 - https://znc.in)
23:01:22 × weary-traveler quits (~user@user/user363627) (Client Quit)
23:02:00 YuutaW joins (~YuutaW@2404:f4c0:f9c3:502::100:17b7)
23:07:37 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
23:09:06 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
23:10:15 × dontdieych2 quits (~quassel@user/dontdieych2) (Ping timeout: 248 seconds)
23:10:37 paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt)
23:11:56 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
23:15:55 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
23:18:03 × paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 252 seconds)
23:24:14 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
23:24:19 sayurc joins (~sayurc@169.150.203.34)
23:25:38 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds)
23:26:40 paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt)
23:27:07 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
23:29:00 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:30:24 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
23:31:07 × paotsaq quits (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 244 seconds)
23:31:52 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
23:34:33 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
23:36:57 ec joins (~ec@gateway/tor-sasl/ec)
23:42:31 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
23:49:08 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
23:50:40 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
23:52:53 × xdminsy quits (~xdminsy@117.147.71.200) (Read error: Connection reset by peer)
23:53:47 xdminsy joins (~xdminsy@117.147.71.200)
23:54:04 × euleritian quits (~euleritia@dynamic-176-006-128-233.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
23:54:28 × remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
23:54:28 euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
23:54:33 gmg joins (~user@user/gehmehgeh)
23:55:16 remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz)
23:55:34 × Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep)

All times are in UTC on 2025-01-14.