Note: This channel on freenode is currently not being logged anymore. The logs are reproduced here for posterity.

2020-09-16 20:45:35 +0200 <tomsmeding> also there were lots of header tabs that were commented out, having a look at those
2020-09-16 20:46:20 +0200cole-h(~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 258 seconds)
2020-09-16 20:46:35 +0200elliott_(~elliott_@pool-71-114-77-65.washdc.fios.verizon.net)
2020-09-16 20:47:24 +0200 <tomsmeding> footer has been fixed, and the header links seem to work sm[m]
2020-09-16 20:47:44 +0200tomsmedingwonders why that stuff was commented out? was it disabled explicitly at some point?
2020-09-16 20:47:53 +0200__Joker(~Joker@180.151.106.108)
2020-09-16 20:48:44 +0200Ranhir(~Ranhir@157.97.53.139) (Read error: Connection reset by peer)
2020-09-16 20:50:27 +0200LKoen(~LKoen@81.255.219.130) (Remote host closed the connection)
2020-09-16 20:51:29 +0200 <sm[m]> tomsmeding++
2020-09-16 20:52:19 +0200__Joker(~Joker@180.151.106.108) (Ping timeout: 246 seconds)
2020-09-16 20:52:35 +0200 <sm[m]> woohoo, now a chance to fix some things that always bugged me, like the page size selector :)
2020-09-16 20:53:00 +0200 <tomsmeding> lol
2020-09-16 20:53:07 +0200 <tomsmeding> there's literally a list of page sizes
2020-09-16 20:53:14 +0200 <tomsmeding> so changing that is trivial
2020-09-16 20:54:33 +0200sm[m]tries to decipher the timestamps
2020-09-16 20:55:11 +0200Ranhir(~Ranhir@157.97.53.139)
2020-09-16 20:57:59 +0200 <sm[m]> I think the timezone is 2 or 3 hours off
2020-09-16 20:59:08 +0200Volt_(~Volt_@c-73-145-164-70.hsd1.mi.comcast.net) (Quit: )
2020-09-16 20:59:46 +0200 <sm[m]> I think it used to update quite often, which could be handy when you got disconnected or didn't trust your chat client
2020-09-16 20:59:54 +0200twopoint718(~cjw@fsf/member/twopoint718)
2020-09-16 21:00:21 +0200nineonine(~nineonine@216-19-190-182.dyn.novuscom.net) (Remote host closed the connection)
2020-09-16 21:03:10 +0200alp_(~alp@2a01:e0a:58b:4920:d89c:57f0:2993:7c47)
2020-09-16 21:03:23 +0200juuandyy(~juuandyy@90.166.144.65) (Ping timeout: 260 seconds)
2020-09-16 21:05:39 +0200shafox(~shafox@106.51.234.111) (Remote host closed the connection)
2020-09-16 21:05:50 +0200 <tomsmeding> ah right server is in UTC but receives stuff from the irc server in GMT+2 which is the timezone where the server is located
2020-09-16 21:06:22 +0200lembot(~lembot@168.196.201.63)
2020-09-16 21:06:38 +0200mariatsji(~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) (Remote host closed the connection)
2020-09-16 21:06:40 +0200wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-09-16 21:06:50 +0200 <tomsmeding> interesting that it does show shifted-correct timestamps for you, who are nowhere near europe in terms of timezones
2020-09-16 21:07:05 +0200kritzefitz(~kritzefit@212.86.56.80)
2020-09-16 21:07:13 +0200 <tomsmeding> does ircbrowse actively adjust timestamps according to the timezone of the client browser?
2020-09-16 21:09:00 +0200 <tomsmeding> oh right I didn't realise it's lazy and just writes +0000
2020-09-16 21:10:06 +0200nineonine(~nineonine@216.81.48.202)
2020-09-16 21:10:14 +0200 <geekosaur> fwiw I show 2 hours forward from my current timezone (UTC-4) which suggests UTC-2
2020-09-16 21:10:30 +0200 <geekosaur> that is, something timestamped 14:57 locally is 16:57 in ircbrowse
2020-09-16 21:10:33 +0200Rudd0(~Rudd0@185.189.115.108) (Ping timeout: 272 seconds)
2020-09-16 21:11:01 +0200gestone(~gestone@c-73-97-137-216.hsd1.wa.comcast.net)
2020-09-16 21:11:11 +0200lembot(~lembot@168.196.201.63) (Ping timeout: 272 seconds)
2020-09-16 21:11:47 +0200wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds)
2020-09-16 21:12:42 +0200lembot(~lembot@45.232.32.247)
2020-09-16 21:13:10 +0200Axman6(~Axman6@pdpc/supporter/student/Axman6) (Ping timeout: 258 seconds)
2020-09-16 21:13:24 +0200Axman6(~Axman6@pdpc/supporter/student/Axman6)
2020-09-16 21:14:10 +0200 <sm[m]> does anyone know a way to copy the current file path and/or line number in vs code ?
2020-09-16 21:15:03 +0200 <sm[m]> tomsmeding: I'm looking at upstream/snap-app/src/Snap/App/Controller.hs:91 and wondering if that's where the default page size of 35 comes from
2020-09-16 21:15:53 +0200 <sm[m]> and what happens if the page sizes at Controllers.hs:147 don't include that number
2020-09-16 21:16:08 +0200 <sm[m]> I'd test, but the build plan looks too hairy right now
2020-09-16 21:16:13 +0200 <tomsmeding> geekosaur: my brain is operating at reduced capacity; for me ircbrowse reports everything in UTC, but two hours earlier than the event actually happened; is that consistent with what you see?
2020-09-16 21:16:15 +0200gestone(~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 272 seconds)
2020-09-16 21:16:26 +0200 <tomsmeding> building is actually no harder than 'stack build'
2020-09-16 21:16:37 +0200 <tomsmeding> well, and waiting
2020-09-16 21:16:54 +0200tsrt^(tsrt@ip98-184-89-2.mc.at.cox.net)
2020-09-16 21:16:54 +0200 <sm[m]> that's hard when it's lts-3 and you have a mac with no spare disk space :)
2020-09-16 21:16:57 +0200 <geekosaur> it claims +0000 but 2 hours ahead of me or 2 hours behind UTC
2020-09-16 21:17:43 +0200 <geekosaur> >> that is, something timestamped 14:57 locally is 16:57 in ircbrowse
2020-09-16 21:18:10 +0200 <geekosaur> 14:57 being UTC-4, EDT
2020-09-16 21:18:45 +0200andreas303(~andreas@gateway/tor-sasl/andreas303) (Remote host closed the connection)
2020-09-16 21:18:49 +0200ViCi(daniel@10PLM.ro) (Ping timeout: 264 seconds)
2020-09-16 21:42:01 +0200ircbrowse_tom(~ircbrowse@64.225.78.177)
2020-09-16 21:42:02 +0200Server+CLnt
2020-09-16 21:42:13 +0200 <rustisafungus> so what is a type, and is there any practical phenomenon which creates a reasonable upper bound on the number of distinct types, or which limits the "growth" of types?
2020-09-16 21:43:58 +0200 <tomsmeding> sm[m]: geekosaur: I believe the timezone setting of ircbrowse is correct now
2020-09-16 21:44:43 +0200ChaiTRex(~ChaiTRex@gateway/tor-sasl/chaitrex) (Ping timeout: 240 seconds)
2020-09-16 21:45:12 +0200 <geekosaur> looks right to me, yes
2020-09-16 21:45:12 +0200 <Cale> rustisafungus: One way to think about them is that types are properties of programs for which the program itself can be interpreted as a proof.
2020-09-16 21:45:53 +0200 <Cale> rustisafungus: (and checked by a machine)
2020-09-16 21:46:51 +0200nfd(~nfd9001@c-67-183-38-33.hsd1.wa.comcast.net)
2020-09-16 21:47:10 +0200ChaiTRex(~ChaiTRex@gateway/tor-sasl/chaitrex)
2020-09-16 21:47:14 +0200 <rustisafungus> this question will make you laugh, but is there any way to think about the question of "how many types are there?"
2020-09-16 21:47:28 +0200hackagelti13 0.1.2.0 - Core functionality for LTI 1.3. https://hackage.haskell.org/package/lti13-0.1.2.0 (jade)
2020-09-16 21:47:40 +0200 <dolio> Infinitely many.
2020-09-16 21:47:40 +0200 <Cale> I mean, unless the answer is 1, usually it's infinitely many.
2020-09-16 21:47:54 +0200 <sm[m]> tomsmeding: what would you think about hiding all the connect/disconnects
2020-09-16 21:47:59 +0200 <Cale> It obviously depends on which type system we're talking about
2020-09-16 21:48:05 +0200 <tomsmeding> sm[m]: yes
2020-09-16 21:48:22 +0200 <tomsmeding> will require some finicking with the pagination though
2020-09-16 21:48:26 +0200 <Cale> It's like asking how many mathematical statements there are
2020-09-16 21:48:26 +0200 <rustisafungus> right but that's a boring answer. for example we could say that there are infinitely many physical units, when in fact there are just a few fundamental physical units from which all physical units are derived using simple operations
2020-09-16 21:48:27 +0200 <monochrom> "what is" questions are usually not worth answering.
2020-09-16 21:48:28 +0200hackageyesod-auth-lti13 0.1.2.0 - A yesod-auth plugin for LTI 1.3 https://hackage.haskell.org/package/yesod-auth-lti13-0.1.2.0 (jade)
2020-09-16 21:49:06 +0200 <monochrom> "how many types" is also a useless question in the first place.
2020-09-16 21:49:33 +0200 <rustisafungus> i don't agree, because Cale's answer says that if your program has more types, then it has more proven constraints imposed/checked by the compiler
2020-09-16 21:49:42 +0200 <monochrom> "what are the rules of making type expressions" is a much more useful question. Now it reveals structure.
2020-09-16 21:49:48 +0200 <Cale> If the answer were not infinity and were instead 100 billion, what would you do with that information?
2020-09-16 21:50:53 +0200Guest86335(~zv@2600:8801:c300:3160:725:f34a:154c:cdd0) (Quit: WeeChat 2.8)
2020-09-16 21:50:58 +0200nfd9001(~nfd9001@c-67-183-38-33.hsd1.wa.comcast.net) (Ping timeout: 260 seconds)
2020-09-16 21:51:06 +0200 <geekosaur> rustisafungus, you can meaningfully ask how many types a given program makes use of, but less so how many types there are globally
2020-09-16 21:51:15 +0200 <monochrom> Likewise, "how many binary trees?" "infinitely many" is useless. "how to define/generate binary trees by structural induction" is the useful one.
2020-09-16 21:52:09 +0200merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2020-09-16 21:52:16 +0200 <monochrom> We can also set up pathological type systems in which infinitely many types express no invariant at all so the counterpoint is moot.
2020-09-16 21:52:22 +0200 <rustisafungus> so is there a small collection of laws for defining "all possible" types?
2020-09-16 21:52:41 +0200gestone(~gestone@c-73-97-137-216.hsd1.wa.comcast.net)
2020-09-16 21:52:45 +0200 <Cale> In essentially any practical type system, yeah
2020-09-16 21:53:15 +0200 <rustisafungus> right but i am thinking in the sense of the fact that there was a one page probabilistic proof of fermat's last theorem while the mathematicians took forever to produce a lengthy and incomprehensible proof,... that is to say i am fine with heuristic/empirical/semi-empirical arguments
2020-09-16 21:53:28 +0200 <rustisafungus> Cale: so where do i find those laws?
2020-09-16 21:53:38 +0200 <Cale> For which type theory?
2020-09-16 21:53:42 +0200faker(bd0f81a2@189.15.129.162)
2020-09-16 21:53:53 +0200 <rustisafungus> i don't know,... i don't even know what a type theory is or what distinguishes one from another
2020-09-16 21:54:39 +0200 <geekosaur> maybe that's the wrong angle. start with standard Haskell ADTs
2020-09-16 21:55:03 +0200 <Cale> Yeah, I guess I should make sure you're not just asking about Haskell
2020-09-16 21:55:23 +0200 <rustisafungus> no i am asking more broadly