| 2025-01-18 00:00:01 +0100 | <EvanR> | countable and constructible is certainly not the same thing |
| 2025-01-18 00:00:19 +0100 | <monochrom> | And on second thought, I am not even sure I can take credit. My purpose was to make a newtype to allow the like of (\x -> x x), and the error message literally inspires that definition! |
| 2025-01-18 00:00:41 +0100 | <EvanR> | formal languages come with grammar rules which limit you to a countable number of sentences |
| 2025-01-18 00:00:45 +0100 | <monochrom> | "I thank GHC for suggesting this newtype." |
| 2025-01-18 00:00:52 +0100 | <EvanR> | haskell being an example of one |
| 2025-01-18 00:01:18 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-18 00:01:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> right, e.g. a language with the judgment 'x is a value of type Real Number' does not have countably many statements I think |
| 2025-01-18 00:02:04 +0100 | <EvanR> | that's mixing concepts |
| 2025-01-18 00:02:23 +0100 | <EvanR> | jumping to another level of abstraction, beyond the syntax |
| 2025-01-18 00:02:29 +0100 | paul_j | (~user@8.190.187.81.in-addr.arpa) (Quit: Asta la vista) |
| 2025-01-18 00:02:47 +0100 | <monochrom> | We know of at least two theories (aka models) of programming, and they disagree on countability as well as other things. The moral is that you choose a theory to suit a purpose, not for Platonic "absolute" "truth". |
| 2025-01-18 00:02:56 +0100 | <EvanR> | as far as real numbers go it's a pretty nutty way to specify one xD |
| 2025-01-18 00:03:02 +0100 | <EvanR> | usually you need a language for that |
| 2025-01-18 00:03:19 +0100 | <haskellbridge> | <thirdofmay18081814goya> well if a theory is a set of axioms and derivable sentences, then we should admit such a language (the one having the judgment 'x is a value of type Real Number') |
| 2025-01-18 00:04:06 +0100 | <geekosaur> | there are countably many values of IEEE float or double, though. you're limited to some form of "computable reals" on any physical computer |
| 2025-01-18 00:04:12 +0100 | <EvanR> | is "x" there a metavariable or literally x |
| 2025-01-18 00:04:26 +0100 | <haskellbridge> | <thirdofmay18081814goya> geekosaur: the computable reals are embeddable in the naturals! |
| 2025-01-18 00:04:37 +0100 | <geekosaur> | yes |
| 2025-01-18 00:04:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:04:42 +0100 | <geekosaur> | hence are countable |
| 2025-01-18 00:04:43 +0100 | <monochrom> | And it is also related to the deal with real numbers, set theory, everything. There are countable models of ZFC, and yet there are also uncountable sets. |
| 2025-01-18 00:04:59 +0100 | <EvanR> | also there's a difference between computable real and algorithmic real |
| 2025-01-18 00:05:13 +0100 | <EvanR> | monochrom, yes that's what I was getting at |
| 2025-01-18 00:05:15 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 00:05:34 +0100 | <EvanR> | uncountable is necessarily semantic |
| 2025-01-18 00:05:55 +0100 | <monochrom> | You can choose a different level of abstraction (aka model) you get a different conclusion. This is supposed to be normal. |
| 2025-01-18 00:08:12 +0100 | <monochrom> | I think both are necessarily semantic. But then that's a tautology. You need to choose a semantic (aka model again) before you can argue anything. |
| 2025-01-18 00:08:49 +0100 | <EvanR> | sometimes something can be said about any possible semantics |
| 2025-01-18 00:08:56 +0100 | <EvanR> | because you're really talking about the syntax |
| 2025-01-18 00:09:12 +0100 | <EvanR> | or the logic of how you put the sentences together |
| 2025-01-18 00:09:22 +0100 | <EvanR> | and never really refer to any meaning |
| 2025-01-18 00:09:35 +0100 | <EvanR> | which happens in haskell sometimes |
| 2025-01-18 00:09:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2025-01-18 00:09:51 +0100 | <monochrom> | In particular if you think that you are using merely syntax trees for your argument, then you are choosing the Herbrand model, therefore it's a model, therefore it's also a semantics! There is no escape from arguing semantics |
| 2025-01-18 00:09:59 +0100 | <EvanR> | when you're dealing with raw data, no IO |
| 2025-01-18 00:10:24 +0100 | <EvanR> | Herbrand |
| 2025-01-18 00:10:37 +0100 | <EvanR> | I'll have to look that up and hope it's not ridiculously trivial lol |
| 2025-01-18 00:10:48 +0100 | <monochrom> | "It's semantics all the way down" >:) |
| 2025-01-18 00:11:08 +0100 | <monochrom> | It is fairly trivial. It's literally the set of ASTs. |
| 2025-01-18 00:11:52 +0100 | <monochrom> | So for example if you argue that programs are countable, you are just reminding us that the Herbrand model is countable. |
| 2025-01-18 00:12:16 +0100 | <monochrom> | ... and I guess that's one way to see why there are countable models for ZFC! |
| 2025-01-18 00:12:25 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-18 00:13:42 +0100 | <haskellbridge> | <thirdofmay18081814goya> i'll be back with a more rigorous statement |
| 2025-01-18 00:13:57 +0100 | <monochrom> | And whatever you do in model theory, you must respect that Herbrand models are here to stay, even if it may be an annoying silly oddball. |
| 2025-01-18 00:16:06 +0100 | agent314 | (~quassel@c-24-17-1-67.hsd1.wa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 00:16:30 +0100 | agent314 | (~quassel@37.19.210.25) agent314 |
| 2025-01-18 00:17:58 +0100 | <monochrom> | You may need more than spelling out a rigorous statement. You may end up also needing to spell out exactly which proof system you chose. Like I said, choosing a different one leads to the opposite result. |
| 2025-01-18 00:18:48 +0100 | <monochrom> | And just around the same time in #haskell-offtopic we were talking about how programs come ship with their own C++ libs to avoid DLL hell. |
| 2025-01-18 00:19:24 +0100 | <monochrom> | program : supporting libs :: true statement :: the proof system that proved it |
| 2025-01-18 00:19:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:20:45 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 00:21:20 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 272 seconds) |
| 2025-01-18 00:21:20 +0100 | tnt2 | tnt1 |
| 2025-01-18 00:21:41 +0100 | <monochrom> | Oh and... |
| 2025-01-18 00:21:50 +0100 | <monochrom> | @quote monochrom polymorphic |
| 2025-01-18 00:21:50 +0100 | <lambdabot> | monochrom says: All pointless debates can be settled by going polymorphic. |
| 2025-01-18 00:22:57 +0100 | <c_wraith> | does that also apply to pointfree debates? |
| 2025-01-18 00:23:13 +0100 | <monochrom> | haha, I haven't thought of that. |
| 2025-01-18 00:23:51 +0100 | igorantonow | (~igor@user/igorantonow) igorantonow |
| 2025-01-18 00:24:37 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 00:25:20 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 265 seconds) |
| 2025-01-18 00:31:06 +0100 | igorantonow | (~igor@user/igorantonow) (Remote host closed the connection) |
| 2025-01-18 00:33:57 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-01-18 00:35:53 +0100 | ss4 | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2025-01-18 00:37:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:40:47 +0100 | Everything | (~Everythin@195.138.86.118) (Quit: leaving) |
| 2025-01-18 00:42:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-18 00:42:44 +0100 | tallcatparade | (~tallcatpa@99-171-182-203.lightspeed.sndgca.sbcglobal.net) |
| 2025-01-18 00:43:44 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) alecs |
| 2025-01-18 00:47:48 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 244 seconds) |
| 2025-01-18 00:53:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 00:57:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 00:57:47 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-01-18 00:58:09 +0100 | tallcatparade | (~tallcatpa@99-171-182-203.lightspeed.sndgca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2025-01-18 00:58:55 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 01:03:18 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 01:08:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 01:13:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 01:13:45 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-18 01:15:31 +0100 | tallcatparade | (~tallcatpa@2600:8801:9801:d600::c83b) |
| 2025-01-18 01:16:07 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-01-18 01:18:30 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 01:24:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 01:24:21 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-01-18 01:30:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2025-01-18 01:33:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 01:38:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 01:42:38 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-01-18 01:48:49 +0100 | <homo> | trying to convert microhs's use of GHC.Types(Any) to Data.Dynamic(Dynamic) to make hugs happy is so hard that it seems impossible |
| 2025-01-18 01:49:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 01:49:22 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) (Ping timeout: 248 seconds) |
| 2025-01-18 01:51:49 +0100 | <homo> | the more I try the more I discover code that I have to rewrite |
| 2025-01-18 01:53:42 +0100 | sprotte24 | (~sprotte24@p200300d16f42e000280df7176889acea.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-01-18 01:55:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 01:55:41 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-01-18 02:03:57 +0100 | mixfix41 | (~tbmur@user/mixfix41) (Ping timeout: 265 seconds) |
| 2025-01-18 02:05:46 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 02:10:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 02:13:09 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-01-18 02:13:26 +0100 | euleritian | (~euleritia@77.23.250.232) |
| 2025-01-18 02:15:23 +0100 | acidjnk | (~acidjnk@p200300d6e7283f5200259c07642d77ab.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-01-18 02:16:37 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds) |
| 2025-01-18 02:19:34 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 2025-01-18 02:21:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 02:25:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 02:25:35 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-01-18 02:31:57 +0100 | otto_s | (~user@p5b044128.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-01-18 02:32:13 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 02:32:39 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 02:32:58 +0100 | otto_s | (~user@p4ff27ba5.dip0.t-ipconnect.de) |
| 2025-01-18 02:35:14 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 02:35:47 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-18 02:36:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 02:39:29 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds) |
| 2025-01-18 02:39:45 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-01-18 02:41:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 02:42:54 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 02:43:27 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 02:44:19 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 02:44:39 +0100 | euleritian | (~euleritia@77.23.250.232) (Remote host closed the connection) |
| 2025-01-18 02:44:51 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 02:45:31 +0100 | euleritian | (~euleritia@77.23.250.232) |
| 2025-01-18 02:49:04 +0100 | telser | (~quassel@user/telser) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2025-01-18 02:51:09 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-18 02:51:30 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-18 02:51:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 02:53:55 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-18 02:56:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 03:05:55 +0100 | ColinRobinson | JuanDaugherty |
| 2025-01-18 03:07:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 03:11:38 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 2025-01-18 03:13:31 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-18 03:14:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 03:15:18 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-01-18 03:15:18 +0100 | JuanDaugherty | ColinRobinson |
| 2025-01-18 03:15:52 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 03:17:14 +0100 | symdrome | (~user@2804:1e78:2201:58b0::416) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
| 2025-01-18 03:17:41 +0100 | jrm2 | (~jrm@user/jrm) jrm |
| 2025-01-18 03:17:48 +0100 | jrm | (~jrm@user/jrm) (Read error: Connection reset by peer) |
| 2025-01-18 03:19:17 +0100 | jrm2 | jrm |
| 2025-01-18 03:20:12 +0100 | Jeanne-Kamikaze | (~Jeanne-Ka@79.127.217.40) Jeanne-Kamikaze |
| 2025-01-18 03:24:20 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 03:25:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 03:25:38 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-01-18 03:25:38 +0100 | tnt2 | tnt1 |
| 2025-01-18 03:27:07 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 264 seconds) |
| 2025-01-18 03:27:56 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 03:28:24 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 03:29:31 +0100 | ColinRobinson | JuanDaugherty |
| 2025-01-18 03:29:31 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 03:31:11 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 03:32:28 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 03:32:53 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-01-18 03:32:53 +0100 | tnt2 | tnt1 |
| 2025-01-18 03:35:43 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-18 03:40:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 03:43:39 +0100 | JuanDaugherty | ColinRobinson |
| 2025-01-18 03:45:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 03:50:44 +0100 | ColinRobinson | JuanDaugherty |
| 2025-01-18 03:53:19 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-01-18 03:53:31 +0100 | alp | (~alp@2001:861:8ca0:4940:efc9:d30b:fc5e:f0f7) (Ping timeout: 264 seconds) |
| 2025-01-18 03:56:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 03:57:37 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 03:57:56 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-01-18 03:57:56 +0100 | tnt2 | tnt1 |
| 2025-01-18 04:00:23 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2025-01-18 04:01:10 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) TheCoffeMaker |
| 2025-01-18 04:02:13 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 04:02:29 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 2025-01-18 04:02:29 +0100 | tnt2 | tnt1 |
| 2025-01-18 04:02:35 +0100 | JuanDaugherty | ColinRobinson |
| 2025-01-18 04:10:50 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 04:10:51 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-01-18 04:10:51 +0100 | tnt2 | tnt1 |
| 2025-01-18 04:11:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 04:11:59 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: ColinRobinson) |
| 2025-01-18 04:13:57 +0100 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 248 seconds) |
| 2025-01-18 04:15:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 04:26:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 04:31:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 04:33:13 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 04:37:54 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 04:40:40 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-01-18 04:42:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 04:44:54 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-18 04:46:48 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-18 04:47:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 04:55:11 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 04:55:40 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 04:56:14 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 04:56:40 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 04:56:46 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 04:57:52 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 04:57:55 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 04:58:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 04:59:18 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 04:59:26 +0100 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2025-01-18 05:00:09 +0100 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) hackager |
| 2025-01-18 05:00:09 +0100 | ChanServ | +v haskellbridge |
| 2025-01-18 05:00:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-01-18 05:02:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 05:10:03 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-01-18 05:10:40 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-01-18 05:13:39 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-01-18 05:13:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 05:18:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-18 05:24:31 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 05:29:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 05:32:06 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 05:36:21 +0100 | Jeanne-Kamikaze | (~Jeanne-Ka@79.127.217.40) (Quit: Leaving) |
| 2025-01-18 05:36:37 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-18 05:45:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 05:50:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 05:50:25 +0100 | agent314 | (~quassel@37.19.210.25) (Ping timeout: 248 seconds) |
| 2025-01-18 05:50:59 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d98:5c1a:a689:d0b8) (Ping timeout: 260 seconds) |
| 2025-01-18 05:51:03 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-18 05:54:27 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-18 05:59:13 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 06:00:35 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 06:05:58 +0100 | euleritian | (~euleritia@77.23.250.232) (Remote host closed the connection) |
| 2025-01-18 06:06:14 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-18 06:07:34 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-01-18 06:08:23 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-18 06:12:23 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d98:5c1a:a689:d0b8) |
| 2025-01-18 06:16:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 06:18:23 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 06:19:44 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 06:21:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 06:32:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 06:32:26 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 06:36:58 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 06:37:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 06:47:16 +0100 | sroso | (~sroso@user/SrOso) SrOso |
| 2025-01-18 06:48:11 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 06:55:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 07:07:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 07:12:09 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 07:15:59 +0100 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2025-01-18 07:21:25 +0100 | greenflower | (~greenflow@2409:4080:ceba:f2ae:f192:933c:3880:ac13) greenflower |
| 2025-01-18 07:22:56 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 07:23:35 +0100 | greenflower | (~greenflow@2409:4080:ceba:f2ae:f192:933c:3880:ac13) (Client Quit) |
| 2025-01-18 07:23:55 +0100 | tessier | (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 265 seconds) |
| 2025-01-18 07:24:15 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2025-01-18 07:25:24 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-01-18 07:26:20 +0100 | pabs3 | (~pabs3@user/pabs3) (Remote host closed the connection) |
| 2025-01-18 07:26:49 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 2025-01-18 07:27:03 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-01-18 07:28:25 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-18 07:29:46 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 07:40:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 07:45:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 07:49:28 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 07:50:30 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-01-18 07:50:30 +0100 | tnt2 | tnt1 |
| 2025-01-18 07:52:01 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 07:56:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 07:56:17 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds) |
| 2025-01-18 07:56:59 +0100 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2025-01-18 07:59:36 +0100 | CiaoSen | (~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) CiaoSen |
| 2025-01-18 08:00:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 08:00:27 +0100 | JamesMowery439 | (~JamesMowe@ip68-228-212-232.ph.ph.cox.net) (Quit: Goodbye) |
| 2025-01-18 08:00:45 +0100 | JamesMowery4395 | (~JamesMowe@ip68-228-212-232.ph.ph.cox.net) JamesMowery |
| 2025-01-18 08:02:57 +0100 | mikess | (~mikess@user/mikess) mikess |
| 2025-01-18 08:06:53 +0100 | mikess | (~mikess@user/mikess) (Client Quit) |
| 2025-01-18 08:11:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 08:13:28 +0100 | Square | (~Square@user/square) Square |
| 2025-01-18 08:16:07 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 08:23:05 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:24:22 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:24:29 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:25:55 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:26:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 08:31:32 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:32:49 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:33:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 08:33:36 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:34:53 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:35:24 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-01-18 08:35:56 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:37:11 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:40:02 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:41:21 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:42:35 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:43:52 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:43:53 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:44:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 08:45:12 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:45:20 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 08:46:45 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 08:47:15 +0100 | harveypwca | (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) HarveyPwca |
| 2025-01-18 08:49:09 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 08:59:32 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-18 08:59:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 09:00:02 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-01-18 09:00:34 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 09:00:47 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-01-18 09:01:58 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:03:16 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:03:25 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:04:50 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-18 09:04:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 09:05:57 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:06:43 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:11:56 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:12:02 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:12:45 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-18 09:13:19 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:14:16 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-01-18 09:14:16 +0100 | tnt2 | tnt1 |
| 2025-01-18 09:14:21 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:15:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 09:15:37 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:20:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2025-01-18 09:23:58 +0100 | harveypwca | (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) (Quit: Leaving) |
| 2025-01-18 09:26:03 +0100 | <chiselfuse> | [ x | x /=13, x <- [10..20], x /= 15, x /= 19] |
| 2025-01-18 09:26:12 +0100 | <chiselfuse> | what happens here? why does it run forever? |
| 2025-01-18 09:26:28 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:27:28 +0100 | <tomsmeding> | > [ x | x /=13, x <- [10..20], x /= 15, x /= 19] |
| 2025-01-18 09:27:29 +0100 | <lambdabot> | [10,11,12,13,14,16,17,18,20] |
| 2025-01-18 09:27:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 09:27:34 +0100 | <tomsmeding> | O.o |
| 2025-01-18 09:27:36 +0100 | <tomsmeding> | % [ x | x /=13, x <- [10..20], x /= 15, x /= 19] |
| 2025-01-18 09:27:36 +0100 | <yahb2> | <interactive>:5:7: error: [GHC-88464] Variable not in scope: x |
| 2025-01-18 09:27:38 +0100 | <tomsmeding> | thank you |
| 2025-01-18 09:27:44 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:27:44 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-18 09:27:53 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:27:57 +0100 | <tomsmeding> | chiselfuse: you can't require that x /= 13 before you have some x in the first place |
| 2025-01-18 09:28:11 +0100 | <tomsmeding> | do you know python? |
| 2025-01-18 09:28:43 +0100 | <tomsmeding> | > x |
| 2025-01-18 09:28:44 +0100 | <lambdabot> | x |
| 2025-01-18 09:28:49 +0100 | <tomsmeding> | (lambdabot being too clever) |
| 2025-01-18 09:29:34 +0100 | homo | (~homo@user/homo) (Read error: Connection reset by peer) |
| 2025-01-18 09:30:02 +0100 | <chiselfuse> | tomsmeding: i know a little bit of python |
| 2025-01-18 09:30:05 +0100 | <chiselfuse> | > :version |
| 2025-01-18 09:30:06 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
| 2025-01-18 09:30:17 +0100 | <Angelz> | python? |
| 2025-01-18 09:30:19 +0100 | <tomsmeding> | chiselfuse: do you know python's list comprehension syntax? |
| 2025-01-18 09:30:20 +0100 | <chiselfuse> | what's '>' and what is '%' here? |
| 2025-01-18 09:30:24 +0100 | <Angelz> | i dunno |
| 2025-01-18 09:30:27 +0100 | <chiselfuse> | tomsmeding: no |
| 2025-01-18 09:30:29 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:30:44 +0100 | <tomsmeding> | it's rather like haskell's, so that would've been a shortcut for explaining what haskell does here :) |
| 2025-01-18 09:30:56 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-01-18 09:30:59 +0100 | <chiselfuse> | what's '>' and what is '%' here? |
| 2025-01-18 09:31:09 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:31:11 +0100 | <tomsmeding> | lambdabot and yahb2 are bothghci-ish; lambdabot responds to '>', yahb2 to '%' |
| 2025-01-18 09:31:23 +0100 | <tomsmeding> | yahb2 is ghci, lambdabot is some magic over ghci |
| 2025-01-18 09:31:27 +0100 | <chiselfuse> | how can we learn the ghci versions of othem? |
| 2025-01-18 09:31:33 +0100 | <tomsmeding> | % :version |
| 2025-01-18 09:31:33 +0100 | <yahb2> | 9.12.1 |
| 2025-01-18 09:31:38 +0100 | <chiselfuse> | > :version |
| 2025-01-18 09:31:39 +0100 | <lambdabot> | <hint>:1:1: error: parse error on input ‘:’ |
| 2025-01-18 09:31:40 +0100 | <tomsmeding> | lambdabot doesn't support such querying |
| 2025-01-18 09:32:01 +0100 | <chiselfuse> | mine is The Glorious Glasgow Haskell Compilation System, version 9.2.8 |
| 2025-01-18 09:32:03 +0100 | Angelz | (Angelz@Angelz.oddprotocol.org) (Changing host) |
| 2025-01-18 09:32:03 +0100 | Angelz | (Angelz@user/angelz) angelz |
| 2025-01-18 09:32:05 +0100 | <chiselfuse> | and it runs forever |
| 2025-01-18 09:32:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-18 09:32:15 +0100 | <tomsmeding> | what is 'x'? |
| 2025-01-18 09:32:25 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:32:29 +0100 | <Angelz> | cservice maybe. |
| 2025-01-18 09:32:41 +0100 | <tomsmeding> | chiselfuse: because this particular bit of code should _not_ run forever. |
| 2025-01-18 09:32:50 +0100 | <chiselfuse> | tomsmeding: but it evaluates fine on one of them. i want to know whether it's valid haskell or not (both semantically and syntactically) and how it gets evaluted on either of those |
| 2025-01-18 09:33:01 +0100 | <tomsmeding> | it is not valid haskell |
| 2025-01-18 09:33:06 +0100 | <tomsmeding> | because in the "x /= 13", x is out of scope |
| 2025-01-18 09:33:17 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:33:17 +0100 | <tomsmeding> | lambdabot has pre-defined magic values for 'a' through 'z' for reasons |
| 2025-01-18 09:33:24 +0100 | <tomsmeding> | so it doesn't quite raise an error here |
| 2025-01-18 09:33:30 +0100 | <chiselfuse> | but it's just a definition, i thought those didn't matter in fp |
| 2025-01-18 09:33:50 +0100 | acidjnk | (~acidjnk@p200300d6e7283f4400259c07642d77ab.dip0.t-ipconnect.de) acidjnk |
| 2025-01-18 09:33:53 +0100 | <tomsmeding> | in a list comprehension, the items to the right of the '|' get run "left-to-right" |
| 2025-01-18 09:34:04 +0100 | <chiselfuse> | sorry, i meant i thought order of definitions didn't matter |
| 2025-01-18 09:34:14 +0100 | <chiselfuse> | get run? |
| 2025-01-18 09:34:18 +0100 | <chiselfuse> | procedurally? |
| 2025-01-18 09:34:23 +0100 | <chiselfuse> | not so fp |
| 2025-01-18 09:34:24 +0100 | <tomsmeding> | % [(x,y) | x <- [1..3], y <- ['a'..'c']] |
| 2025-01-18 09:34:24 +0100 | <yahb2> | [(1,'a'),(1,'b'),(1,'c'),(2,'a'),(2,'b'),(2,'c'),(3,'a'),(3,'b'),(3,'c')] |
| 2025-01-18 09:34:32 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:34:35 +0100 | it_ | (~quassel@v2202212189510211193.supersrv.de) (Quit: ,o>) |
| 2025-01-18 09:34:38 +0100 | <tomsmeding> | % [(x,y) | x <- [1..3], x /= 2, y <- ['a'..'c']] |
| 2025-01-18 09:34:38 +0100 | <yahb2> | [(1,'a'),(1,'b'),(1,'c'),(3,'a'),(3,'b'),(3,'c')] |
| 2025-01-18 09:34:45 +0100 | <tomsmeding> | % [(x,y) | x <- [1..3], y <- ['a'..'c'], x /= 2] |
| 2025-01-18 09:34:45 +0100 | <yahb2> | [(1,'a'),(1,'b'),(1,'c'),(3,'a'),(3,'b'),(3,'c')] |
| 2025-01-18 09:34:51 +0100 | <tomsmeding> | % [(x,y) | x /= 2, x <- [1..3], y <- ['a'..'c']] |
| 2025-01-18 09:34:51 +0100 | <yahb2> | <interactive>:15:10: error: [GHC-88464] Variable not in scope: x |
| 2025-01-18 09:35:35 +0100 | <tomsmeding> | not quite procedurally, but you can think of it that way |
| 2025-01-18 09:35:43 +0100 | <tomsmeding> | a '<-' clause is a "for loop", a bare condition is an "if" |
| 2025-01-18 09:36:09 +0100 | <tomsmeding> | and at the bottom of the for/if nesting, the expression to the left of the '|' is generated |
| 2025-01-18 09:36:14 +0100 | <tomsmeding> | the results are put in a list |
| 2025-01-18 09:36:15 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:36:45 +0100 | <Leary> | @undo [ x | x /= 13, x <- [10..20], x /= 15 ] |
| 2025-01-18 09:36:45 +0100 | <lambdabot> | if x /= 13 then concatMap (\ x -> if x /= 15 then [x] else []) [10 .. 20] else [] |
| 2025-01-18 09:37:10 +0100 | <chiselfuse> | what's @undo? |
| 2025-01-18 09:37:27 +0100 | <tomsmeding> | converts a haskell expression into one using more basic syntax |
| 2025-01-18 09:37:27 +0100 | <Leary> | It desugars the list comprehension so you can see what it means. |
| 2025-01-18 09:37:30 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:37:41 +0100 | <Leary> | Here, you can see that `x` is used before it's brought into scope. |
| 2025-01-18 09:38:10 +0100 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
| 2025-01-18 09:38:40 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:38:47 +0100 | <chiselfuse> | @undo [ x | x <- [10..20], x /=13, x /= 15 ] |
| 2025-01-18 09:38:48 +0100 | <lambdabot> | concatMap (\ x -> if x /= 13 then if x /= 15 then [x] else [] else []) [10 .. 20] |
| 2025-01-18 09:38:55 +0100 | <chiselfuse> | can i use @undo on my computer |
| 2025-01-18 09:39:00 +0100 | it_ | (~quassel@game-crew.ch) K4su |
| 2025-01-18 09:39:07 +0100 | <tomsmeding> | you can open a private chat with lambdabot |
| 2025-01-18 09:39:22 +0100 | <chiselfuse> | @undo :version |
| 2025-01-18 09:39:22 +0100 | <lambdabot> | <unknown>.hs:1:1:Parse error: : |
| 2025-01-18 09:39:43 +0100 | <chiselfuse> | i want run code localloy |
| 2025-01-18 09:39:56 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:40:13 +0100 | <tomsmeding> | '@undo' is a plugin in lambdabot, so it's rather hard to run locally |
| 2025-01-18 09:40:34 +0100 | it_ | (~quassel@game-crew.ch) (Client Quit) |
| 2025-01-18 09:40:49 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:40:51 +0100 | it_ | (~quassel@game-crew.ch) K4su |
| 2025-01-18 09:42:08 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:42:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 09:43:08 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:44:20 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-18 09:44:31 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:44:51 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:46:08 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:48:51 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:50:17 +0100 | Guest9464 | (~v@anomalous.eu) |
| 2025-01-18 09:51:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 09:51:05 +0100 | Guest9464 | (~v@anomalous.eu) (Remote host closed the connection) |
| 2025-01-18 09:52:31 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:52:31 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:52:36 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-18 09:53:03 +0100 | <haskellbridge> | <Bowuigi> I guess you can just write the list comprehension in ghci and see if it works, along with the result |
| 2025-01-18 09:53:35 +0100 | <haskellbridge> | <Bowuigi> You can't see what it desugars to, but you can build an intuition of what it does anyway |
| 2025-01-18 09:53:53 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:54:21 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:55:45 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:55:57 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:57:14 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:57:24 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:58:50 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 09:59:02 +0100 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) robobub |
| 2025-01-18 09:59:21 +0100 | it_ | (~quassel@game-crew.ch) (Quit: ,o>) |
| 2025-01-18 09:59:29 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 09:59:54 +0100 | it_ | (~quassel@game-crew.ch) K4su |
| 2025-01-18 10:00:59 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:01:03 +0100 | it_ | (~quassel@game-crew.ch) (Client Quit) |
| 2025-01-18 10:01:35 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:02:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 10:03:02 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:03:43 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:03:45 +0100 | CiaoSen | (~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 2025-01-18 10:04:13 +0100 | it_ | (~quassel@game-crew.ch) K4su |
| 2025-01-18 10:04:57 +0100 | alp | (~alp@2001:861:8ca0:4940:a068:990b:3be7:3971) |
| 2025-01-18 10:04:58 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:05:06 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:06:23 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:06:37 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:07:53 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:08:32 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:09:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-18 10:09:34 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-18 10:09:48 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:10:35 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:11:51 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:12:43 +0100 | <chiselfuse> | are you sure that @undo is guaranteed to be correct in all cases? |
| 2025-01-18 10:13:07 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:14:02 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds) |
| 2025-01-18 10:14:48 +0100 | <tomsmeding> | the author of lambdabot tried their best |
| 2025-01-18 10:15:46 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:15:49 +0100 | <tomsmeding> | but in general that's what you're going to get from software -- even if you have formally proven software, that delegates the burden to the implementor of the proof tool, which is hopefully smaller and easier to check, but still to be checked manually |
| 2025-01-18 10:15:54 +0100 | <c_wraith> | the desugaring is part of the spec. The only thing lambdabot doesn't necessarily have is the definition of all the relevant data types |
| 2025-01-18 10:16:09 +0100 | <c_wraith> | So it doesn't know when a pattern match needs to introduce a fail case |
| 2025-01-18 10:17:04 +0100 | <c_wraith> | (a pattern match on the LHS of a <-, specifically) |
| 2025-01-18 10:17:56 +0100 | <tomsmeding> | @undo [x | Just x <- l] |
| 2025-01-18 10:17:56 +0100 | <lambdabot> | concatMap (\ a -> case a of { Just x -> [x]; _ -> []}) l |
| 2025-01-18 10:18:08 +0100 | <tomsmeding> | ah it just assumes there's other constructors |
| 2025-01-18 10:20:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 10:20:19 +0100 | <c_wraith> | That's a case I'd expect to have hardcoded |
| 2025-01-18 10:20:40 +0100 | <c_wraith> | @undo do { (a, b) <- foo ; pure $ a + b } |
| 2025-01-18 10:20:40 +0100 | <lambdabot> | foo >>= \ (a, b) -> pure $ a + b |
| 2025-01-18 10:20:56 +0100 | <c_wraith> | It knows that one only has one constructor |
| 2025-01-18 10:21:10 +0100 | it_ | (~quassel@game-crew.ch) (Quit: ,o>) |
| 2025-01-18 10:21:33 +0100 | <c_wraith> | I'd assume the @undo plugin has definitions for all the common types |
| 2025-01-18 10:22:09 +0100 | it_ | (~quassel@game-crew.ch) K4su |
| 2025-01-18 10:22:36 +0100 | <c_wraith> | @undo do { Foo a b <- foo ; pure $ a + b } |
| 2025-01-18 10:22:36 +0100 | <lambdabot> | foo >>= \ c -> case c of { Foo a b -> pure $ a + b; _ -> fail ""} |
| 2025-01-18 10:22:53 +0100 | <c_wraith> | and just assumes that things it doesn't know about have more constructors. |
| 2025-01-18 10:23:12 +0100 | <c_wraith> | whereas ghc knows if there are more constructors or not |
| 2025-01-18 10:24:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-18 10:28:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 10:29:33 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:30:56 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:30:57 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:32:14 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:32:16 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:32:18 +0100 | acidjnk | (~acidjnk@p200300d6e7283f4400259c07642d77ab.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-01-18 10:33:23 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-18 10:33:38 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:35:15 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:36:43 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:38:01 +0100 | euandreh1 | (~Thunderbi@191-217-172-66.user3p.v-tal.net.br) euandreh |
| 2025-01-18 10:39:24 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-01-18 10:39:28 +0100 | euandreh1 | (~Thunderbi@191-217-172-66.user3p.v-tal.net.br) (Client Quit) |
| 2025-01-18 10:39:38 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 2025-01-18 10:39:57 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-18 10:40:21 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Client Quit) |
| 2025-01-18 10:40:43 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-18 10:40:54 +0100 | euandreh | (~Thunderbi@189.6.105.228) (Ping timeout: 260 seconds) |
| 2025-01-18 10:42:30 +0100 | euandreh | (~Thunderbi@191-217-172-66.user3p.v-tal.net.br) euandreh |
| 2025-01-18 10:44:54 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:46:09 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:46:10 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:46:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-18 10:47:26 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:47:27 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:48:43 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-18 10:49:41 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection) |
| 2025-01-18 10:51:17 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-18 10:52:17 +0100 | Guest8686 | (~v@anomalous.eu) |
| 2025-01-18 10:52:49 +0100 | ubert | (~Thunderbi@p200300ecdf3b1a6b3fb62acbaa32cd66.dip0.t-ipconnect.de) ubert |
| 2025-01-18 10:52:56 +0100 | todi | (~todi@p57803331.dip0.t-ipconnect.de) todi |
| 2025-01-18 10:57:46 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |