Logs: freenode/#haskell
| 2020-09-16 18:45:35 | <tomsmeding> | also there were lots of header tabs that were commented out, having a look at those |
| 2020-09-16 18:46:20 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 258 seconds) |
| 2020-09-16 18:46:35 | → | elliott_ joins (~elliott_@pool-71-114-77-65.washdc.fios.verizon.net) |
| 2020-09-16 18:47:24 | <tomsmeding> | footer has been fixed, and the header links seem to work sm[m] |
| 2020-09-16 18:47:44 | tomsmeding | wonders why that stuff was commented out? was it disabled explicitly at some point? |
| 2020-09-16 18:47:53 | → | __Joker joins (~Joker@180.151.106.108) |
| 2020-09-16 18:48:44 | × | Ranhir quits (~Ranhir@157.97.53.139) (Read error: Connection reset by peer) |
| 2020-09-16 18:50:27 | × | LKoen quits (~LKoen@81.255.219.130) (Remote host closed the connection) |
| 2020-09-16 18:51:29 | <sm[m]> | tomsmeding++ |
| 2020-09-16 18:52:19 | × | __Joker quits (~Joker@180.151.106.108) (Ping timeout: 246 seconds) |
| 2020-09-16 18:52:35 | <sm[m]> | woohoo, now a chance to fix some things that always bugged me, like the page size selector :) |
| 2020-09-16 18:53:00 | <tomsmeding> | lol |
| 2020-09-16 18:53:07 | <tomsmeding> | there's literally a list of page sizes |
| 2020-09-16 18:53:14 | <tomsmeding> | so changing that is trivial |
| 2020-09-16 18:54:33 | sm[m] | tries to decipher the timestamps |
| 2020-09-16 18:55:11 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 2020-09-16 18:57:59 | <sm[m]> | I think the timezone is 2 or 3 hours off |
| 2020-09-16 18:59:08 | × | Volt_ quits (~Volt_@c-73-145-164-70.hsd1.mi.comcast.net) (Quit: ) |
| 2020-09-16 18:59:46 | <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 18:59:54 | → | twopoint718 joins (~cjw@fsf/member/twopoint718) |
| 2020-09-16 19:00:21 | × | nineonine quits (~nineonine@216-19-190-182.dyn.novuscom.net) (Remote host closed the connection) |
| 2020-09-16 19:03:10 | → | alp_ joins (~alp@2a01:e0a:58b:4920:d89c:57f0:2993:7c47) |
| 2020-09-16 19:03:23 | × | juuandyy quits (~juuandyy@90.166.144.65) (Ping timeout: 260 seconds) |
| 2020-09-16 19:05:39 | × | shafox quits (~shafox@106.51.234.111) (Remote host closed the connection) |
| 2020-09-16 19:05:50 | <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 19:06:22 | → | lembot joins (~lembot@168.196.201.63) |
| 2020-09-16 19:06:38 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) (Remote host closed the connection) |
| 2020-09-16 19:06:40 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2020-09-16 19:06:50 | <tomsmeding> | interesting that it does show shifted-correct timestamps for you, who are nowhere near europe in terms of timezones |
| 2020-09-16 19:07:05 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 2020-09-16 19:07:13 | <tomsmeding> | does ircbrowse actively adjust timestamps according to the timezone of the client browser? |
| 2020-09-16 19:09:00 | <tomsmeding> | oh right I didn't realise it's lazy and just writes +0000 |
| 2020-09-16 19:10:06 | → | nineonine joins (~nineonine@216.81.48.202) |
| 2020-09-16 19:10:14 | <geekosaur> | fwiw I show 2 hours forward from my current timezone (UTC-4) which suggests UTC-2 |
| 2020-09-16 19:10:30 | <geekosaur> | that is, something timestamped 14:57 locally is 16:57 in ircbrowse |
| 2020-09-16 19:10:33 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 272 seconds) |
| 2020-09-16 19:11:01 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-16 19:11:11 | × | lembot quits (~lembot@168.196.201.63) (Ping timeout: 272 seconds) |
| 2020-09-16 19:11:47 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 2020-09-16 19:12:42 | → | lembot joins (~lembot@45.232.32.247) |
| 2020-09-16 19:13:10 | × | Axman6 quits (~Axman6@pdpc/supporter/student/Axman6) (Ping timeout: 258 seconds) |
| 2020-09-16 19:13:24 | → | Axman6 joins (~Axman6@pdpc/supporter/student/Axman6) |
| 2020-09-16 19:14:10 | <sm[m]> | does anyone know a way to copy the current file path and/or line number in vs code ? |
| 2020-09-16 19:15:03 | <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 19:15:53 | <sm[m]> | and what happens if the page sizes at Controllers.hs:147 don't include that number |
| 2020-09-16 19:16:08 | <sm[m]> | I'd test, but the build plan looks too hairy right now |
| 2020-09-16 19:16:13 | <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 19:16:15 | × | gestone quits (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) (Ping timeout: 272 seconds) |
| 2020-09-16 19:16:26 | <tomsmeding> | building is actually no harder than 'stack build' |
| 2020-09-16 19:16:37 | <tomsmeding> | well, and waiting |
| 2020-09-16 19:16:54 | → | tsrt^ joins (tsrt@ip98-184-89-2.mc.at.cox.net) |
| 2020-09-16 19:16:54 | <sm[m]> | that's hard when it's lts-3 and you have a mac with no spare disk space :) |
| 2020-09-16 19:16:57 | <geekosaur> | it claims +0000 but 2 hours ahead of me or 2 hours behind UTC |
| 2020-09-16 19:17:43 | <geekosaur> | >> that is, something timestamped 14:57 locally is 16:57 in ircbrowse |
| 2020-09-16 19:18:10 | <geekosaur> | 14:57 being UTC-4, EDT |
| 2020-09-16 19:18:45 | × | andreas303 quits (~andreas@gateway/tor-sasl/andreas303) (Remote host closed the connection) |
| 2020-09-16 19:18:49 | × | ViCi quits (daniel@10PLM.ro) (Ping timeout: 264 seconds) |
| 2020-09-16 19:42:01 | → | ircbrowse_tom joins (~ircbrowse@64.225.78.177) |
| 2020-09-16 19:42:02 | Server | sets mode +CLnt |
| 2020-09-16 19:42:13 | <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 19:43:58 | <tomsmeding> | sm[m]: geekosaur: I believe the timezone setting of ircbrowse is correct now |
| 2020-09-16 19:44:43 | × | ChaiTRex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Ping timeout: 240 seconds) |
| 2020-09-16 19:45:12 | <geekosaur> | looks right to me, yes |
| 2020-09-16 19:45:12 | <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 19:45:53 | <Cale> | rustisafungus: (and checked by a machine) |
| 2020-09-16 19:46:51 | → | nfd joins (~nfd9001@c-67-183-38-33.hsd1.wa.comcast.net) |
| 2020-09-16 19:47:10 | → | ChaiTRex joins (~ChaiTRex@gateway/tor-sasl/chaitrex) |
| 2020-09-16 19:47:14 | <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 19:47:28 | hackage | lti13 0.1.2.0 - Core functionality for LTI 1.3. https://hackage.haskell.org/package/lti13-0.1.2.0 (jade) |
| 2020-09-16 19:47:40 | <dolio> | Infinitely many. |
| 2020-09-16 19:47:40 | <Cale> | I mean, unless the answer is 1, usually it's infinitely many. |
| 2020-09-16 19:47:54 | <sm[m]> | tomsmeding: what would you think about hiding all the connect/disconnects |
| 2020-09-16 19:47:59 | <Cale> | It obviously depends on which type system we're talking about |
| 2020-09-16 19:48:05 | <tomsmeding> | sm[m]: yes |
| 2020-09-16 19:48:22 | <tomsmeding> | will require some finicking with the pagination though |
| 2020-09-16 19:48:26 | <Cale> | It's like asking how many mathematical statements there are |
| 2020-09-16 19:48:26 | <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 19:48:27 | <monochrom> | "what is" questions are usually not worth answering. |
| 2020-09-16 19:48:28 | hackage | yesod-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 19:49:06 | <monochrom> | "how many types" is also a useless question in the first place. |
| 2020-09-16 19:49:33 | <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 19:49:42 | <monochrom> | "what are the rules of making type expressions" is a much more useful question. Now it reveals structure. |
| 2020-09-16 19:49:48 | <Cale> | If the answer were not infinity and were instead 100 billion, what would you do with that information? |
| 2020-09-16 19:50:53 | × | Guest86335 quits (~zv@2600:8801:c300:3160:725:f34a:154c:cdd0) (Quit: WeeChat 2.8) |
| 2020-09-16 19:50:58 | × | nfd9001 quits (~nfd9001@c-67-183-38-33.hsd1.wa.comcast.net) (Ping timeout: 260 seconds) |
| 2020-09-16 19:51:06 | <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 19:51:15 | <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 19:52:09 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 2020-09-16 19:52:16 | <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 19:52:22 | <rustisafungus> | so is there a small collection of laws for defining "all possible" types? |
| 2020-09-16 19:52:41 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-16 19:52:45 | <Cale> | In essentially any practical type system, yeah |
| 2020-09-16 19:53:15 | <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 19:53:28 | <rustisafungus> | Cale: so where do i find those laws? |
| 2020-09-16 19:53:38 | <Cale> | For which type theory? |
| 2020-09-16 19:53:42 | → | faker joins (bd0f81a2@189.15.129.162) |
| 2020-09-16 19:53:53 | <rustisafungus> | i don't know,... i don't even know what a type theory is or what distinguishes one from another |
| 2020-09-16 19:54:39 | <geekosaur> | maybe that's the wrong angle. start with standard Haskell ADTs |
| 2020-09-16 19:55:03 | <Cale> | Yeah, I guess I should make sure you're not just asking about Haskell |
| 2020-09-16 19:55:23 | <rustisafungus> | no i am asking more broadly |
All times are in UTC.