| 2024-09-30 00:01:03 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-30 00:01:10 +0200 | <andrewboltachev> | dolio: well, Set^3 is a category of triplets like (a, a', a'') |
| 2024-09-30 00:01:45 +0200 | <dolio> | A functor. |
| 2024-09-30 00:02:26 +0200 | <andrewboltachev> | ok F is a functor. that's how we make a functor from more than one set to one essentially |
| 2024-09-30 00:03:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 00:03:57 +0200 | <dolio> | Yes. But what you're talking about is assembling many different arities of functors into a single category. So that requires having some way of relating different arities to make any sense. |
| 2024-09-30 00:04:34 +0200 | <andrewboltachev> | Yes. thanks a lot for the idea! I'll research it |
| 2024-09-30 00:06:09 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-30 00:06:12 +0200 | <dolio> | Also, depending on what exactly you want to do, you might need not just numbers, but lists indicating whether the argument is covariant or contravariant, and so on. |
| 2024-09-30 00:06:40 +0200 | <dolio> | But all the examples were covariant functors. |
| 2024-09-30 00:08:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-30 00:09:22 +0200 | <andrewboltachev> | https://app.diagrams.net/#G1lKco0mv66sGjTyMSMU1g-ogSE5PIbdzc#%7B%22pageId%22%3A%22YBh8yTivGdvy1ecIg6Zf%22%7D |
| 2024-09-30 00:09:57 +0200 | <andrewboltachev> | dolio: Maybe coproduct will give rise for contravariant functors in the idea you've given |
| 2024-09-30 00:10:21 +0200 | <dolio> | No. Exponentials will. |
| 2024-09-30 00:10:25 +0200 | <andrewboltachev> | ah |
| 2024-09-30 00:10:30 +0200 | <dolio> | I.E. functions. |
| 2024-09-30 00:11:20 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2024-09-30 00:13:06 +0200 | <andrewboltachev> | coproducts (in ADTs) have been a problem (or main point of interest?) for me in this (bigger) idea that I research |
| 2024-09-30 00:13:51 +0200 | <andrewboltachev> | in, for example "Categorical Databases" by David Spivak et al they talk about a "Database instance" functor C -> Set |
| 2024-09-30 00:14:54 +0200 | <andrewboltachev> | but I believe it only works for them 'cause single "database table" is like a product of fields: (e.g. first_name, last_name, email, password etc) |
| 2024-09-30 00:15:47 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod |
| 2024-09-30 00:16:22 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-30 00:17:13 +0200 | <andrewboltachev> | if I generalize the idea (which I want) and the "generalized table" has also coproducts, e.g. either "pickup" or "delivery" (for a web store like Amazon perhaps) then how do they map coproduct onto Set |
| 2024-09-30 00:18:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 00:22:00 +0200 | <hololeap> | andrewboltachev: https://www.parsonsmatt.org/2019/03/19/sum_types_in_sql.html ? |
| 2024-09-30 00:23:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-30 00:24:13 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-09-30 00:24:30 +0200 | <andrewboltachev> | hololeap: well, this is for SQL, but I rather mention "Categorical Databases" :-) |
| 2024-09-30 00:24:35 +0200 | Eoco | (~ian@128.101.131.218) (Quit: WeeChat 4.1.1) |
| 2024-09-30 00:25:06 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2024-09-30 00:25:12 +0200 | <hololeap> | ok |
| 2024-09-30 00:25:16 +0200 | Eoco | (~ian@128.101.131.218) (Client Quit) |
| 2024-09-30 00:25:55 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2024-09-30 00:26:03 +0200 | <andrewboltachev> | hololeap: also, some ppl say that having extra constraints in SQL will make db perform slower. (some even say that Foreign keys make it slow) |
| 2024-09-30 00:26:08 +0200 | Eoco | (~ian@128.101.131.218) (Client Quit) |
| 2024-09-30 00:26:40 +0200 | <andrewboltachev> | so one approach is to have e.g. "type" column and then several nullable columns, where each subset is for particular type etc etc |
| 2024-09-30 00:27:06 +0200 | <geekosaur> | depends on the db, really. sqlite will be bad, postgresql should be reasonable |
| 2024-09-30 00:27:29 +0200 | <geekosaur> | mariadb is poor |
| 2024-09-30 00:28:25 +0200 | <hololeap> | the article mentions three different approaches, including nullable columns |
| 2024-09-30 00:28:26 +0200 | <andrewboltachev> | yes I worked with ppl who denied fks in Postgres in "pursuit" for performance |
| 2024-09-30 00:29:13 +0200 | <geekosaur> | postgres has this thing where it's slower than simpler dbs for small tables, but scales far better than other databases as they get larger and more joins are involved |
| 2024-09-30 00:29:14 +0200 | <andrewboltachev> | hololeap: thanks. sorry |
| 2024-09-30 00:30:20 +0200 | <hololeap> | it's cool I just threw it out because at first glance it seemed vaguely relevant to the backlog I bothered to read |
| 2024-09-30 00:30:31 +0200 | <hololeap> | lol |
| 2024-09-30 00:30:47 +0200 | alp | (~alp@2001:861:e3d6:8f80:9956:3934:6a0b:7b98) |
| 2024-09-30 00:30:50 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb46757e16ffb08be72b.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2024-09-30 00:30:59 +0200 | alp | (~alp@2001:861:e3d6:8f80:9956:3934:6a0b:7b98) (Changing host) |
| 2024-09-30 00:30:59 +0200 | alp | (~alp@user/alp) alp |
| 2024-09-30 00:31:03 +0200 | <andrewboltachev> | geekosaur: I believe there's a lot of science happening under the hood of Postgres :-) |
| 2024-09-30 00:31:18 +0200 | <monochrom> | Why is sqlite bad with foreign keys? If I create an index for the foreign key column, will it be much better? |
| 2024-09-30 00:31:23 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2024-09-30 00:31:37 +0200 | <geekosaur> | sqlite's just bad at jpining; it works best with single flat tables |
| 2024-09-30 00:31:47 +0200 | <geekosaur> | this is the price of being small and simple |
| 2024-09-30 00:31:50 +0200 | <andrewboltachev> | (didn't learn how to read output of EXPLAIN yet) |
| 2024-09-30 00:32:50 +0200 | <geekosaur> | basically it has no clue about query optimization, so where postgresql and even mariadb will optimize joins to at leats some extent, sqlite will keep brute-forcing them |
| 2024-09-30 00:33:26 +0200 | <geekosaur> | (for example it doesn't know how to use relative table sizes to determine when it's better to do the join from the other direction) |
| 2024-09-30 00:34:04 +0200 | <geekosaur> | and keeps no key statistics so it can't use those to similarly optimize how to do joins |
| 2024-09-30 00:34:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 00:34:43 +0200 | <geekosaur> | this kind of stuff means postgresql has higher overhead, but that overhead is fairly fixed so it becomes a smaller part of the cost as tables/indexes get larger |
| 2024-09-30 00:34:44 +0200 | <__monty__> | I'm skeptical working around the lack of foreign keys would usually be more performant than letting the DB engine do its thing. |
| 2024-09-30 00:35:29 +0200 | <geekosaur> | sounds like second generation nosql to me |
| 2024-09-30 00:35:42 +0200 | <andrewboltachev> | yes that team used JSONB |
| 2024-09-30 00:36:03 +0200 | <andrewboltachev> | i.e. two column tables — uuid and data (jsonb) |
| 2024-09-30 00:36:04 +0200 | <geekosaur> | unsurprisingly, nosql dbs are terrible at sqlish things |
| 2024-09-30 00:36:19 +0200 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2024-09-30 00:36:37 +0200 | <andrewboltachev> | but PostgreSQL is good at nosql (if you want it). Or is it? |
| 2024-09-30 00:37:12 +0200 | <geekosaur> | the higher overhead means it's usually not that great at them. tbh I'd use sqlite at that point |
| 2024-09-30 00:37:34 +0200 | <andrewboltachev> | ah |
| 2024-09-30 00:37:48 +0200 | Eoco | (~ian@128.101.131.218) (Quit: WeeChat 4.4.2) |
| 2024-09-30 00:37:52 +0200 | <geekosaur> | it's doing a lot of bookkeeping to optimize sql-style queries, if you do nosql with it that's all wasted |
| 2024-09-30 00:38:47 +0200 | <geekosaur> | (sorry, my inner db wonk is showing 🙂 ) |
| 2024-09-30 00:38:56 +0200 | Eoco | (~ian@128.101.131.218) Eoco |
| 2024-09-30 00:39:02 +0200 | <andrewboltachev> | geekosaur: I sometimes optimize ORM calls :D (e.g. call 1 time instead of N) |
| 2024-09-30 00:39:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-30 00:41:14 +0200 | <andrewboltachev> | geekosaur: do you use esqueleto or sth? |
| 2024-09-30 00:43:01 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 248 seconds) |
| 2024-09-30 00:43:02 +0200 | <andrewboltachev> | geekosaur: and have you seen "Categorical databases"? And if yes, do you think it brings anything useful |
| 2024-09-30 00:44:17 +0200 | <geekosaur> | I don't actually do databases any more (since 1996) |
| 2024-09-30 00:44:51 +0200 | <andrewboltachev> | wow |
| 2024-09-30 00:44:55 +0200 | <geekosaur> | but that was around when the open source community picked up postgres, ripped out the research-quality QUEL engine, and started building a production-quality SQL engine to replace it |
| 2024-09-30 00:45:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 00:46:38 +0200 | xsarnik | (xsarnik@lounge.fi.muni.cz) (The Lounge - https://thelounge.chat) |
| 2024-09-30 00:50:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-30 00:54:12 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 276 seconds) |
| 2024-09-30 01:00:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 01:01:28 +0200 | deepfire | (~user@80.92.100.69) (Remote host closed the connection) |
| 2024-09-30 01:06:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 01:10:53 +0200 | Typedfern | (~Typedfern@2a02:9130:9c34:14e4:99e7:1e2d:3a90:e394) (Ping timeout: 265 seconds) |
| 2024-09-30 01:16:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 01:19:24 +0200 | andrewboltachev | (~andrey@178.141.123.3) (Quit: Leaving.) |
| 2024-09-30 01:20:07 +0200 | <geekosaur> | (also, re "Categorical Databases", I'm a programmer/sysadmin who's picked up a very little bit of abstract mathematics from hanging out in here; I expect that paper would be gobbledygook to me) |
| 2024-09-30 01:20:13 +0200 | <geekosaur> | whoops, missed |
| 2024-09-30 01:21:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 01:27:10 +0200 | Typedfern | (~Typedfern@2a02:9130:9c34:14e4:d11e:8149:a19f:6793) |
| 2024-09-30 01:29:33 +0200 | dyniec | (~dyniec@dybiec.info) dyniec |
| 2024-09-30 01:32:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 01:37:25 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-30 01:41:18 +0200 | <monochrom> | :) |
| 2024-09-30 01:41:47 +0200 | <monochrom> | There is a chance David Spivak's writing can made sense to practical people. Afterall, he wrote like "CT for engineers". |
| 2024-09-30 01:48:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 01:53:25 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 02:03:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 02:04:15 +0200 | pavonia | (~user@user/siracusa) siracusa |
| 2024-09-30 02:06:53 +0200 | polyphem | (~rod@p3ee3f695.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 2024-09-30 02:07:20 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-09-30 02:08:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 02:09:06 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2024-09-30 02:09:32 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-09-30 02:12:39 +0200 | bh34e5 | (~bh34e5@user/bh34e5) bh34e5 |
| 2024-09-30 02:19:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 02:22:09 +0200 | xff0x | (~xff0x@2405:6580:b080:900:2db7:1968:c949:1e07) (Ping timeout: 260 seconds) |
| 2024-09-30 02:24:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-30 02:34:51 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-09-30 02:35:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 02:40:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 02:40:48 +0200 | synchromesh | (~john@2406:5a00:241a:5600:e176:3a40:8bde:547a) (Read error: Connection reset by peer) |
| 2024-09-30 02:41:15 +0200 | synchromesh | (~john@2406:5a00:241a:5600:e176:3a40:8bde:547a) synchromesh |
| 2024-09-30 02:45:44 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-30 02:46:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 02:46:03 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-09-30 02:49:06 +0200 | <Inst> | why does it need to make sense to practical people? |
| 2024-09-30 02:50:07 +0200 | <geekosaur> | context is someone asked me about it on finding I have practical/internals database experience |
| 2024-09-30 02:52:32 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2024-09-30 02:53:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-30 03:01:26 +0200 | <Inst> | ehhh |
| 2024-09-30 03:01:26 +0200 | <Inst> | https://www.categoricaldata.net/cql/Broad_SoftEng.pdf |
| 2024-09-30 03:04:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 03:10:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 03:11:19 +0200 | <JuanDaugherty> | when a thing not worth doing is done nicely |
| 2024-09-30 03:14:39 +0200 | troojg | (~troojg@user/troojg) troojg |
| 2024-09-30 03:17:53 +0200 | xff0x | (~xff0x@182.169.73.28) |
| 2024-09-30 03:20:07 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) athan |
| 2024-09-30 03:20:32 +0200 | <Inst> | it looks like CQL is a thing, which is probably relevant to you geekosaur |
| 2024-09-30 03:20:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 03:21:12 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-09-30 03:22:34 +0200 | troojg | (~troojg@user/troojg) (Remote host closed the connection) |
| 2024-09-30 03:22:55 +0200 | troojg | (~troojg@user/troojg) troojg |
| 2024-09-30 03:23:25 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 244 seconds) |
| 2024-09-30 03:25:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-30 03:29:50 +0200 | zero | (~z@user/zero) (Ping timeout: 252 seconds) |
| 2024-09-30 03:32:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 03:34:07 +0200 | zero | (~z@user/zero) zero |
| 2024-09-30 03:38:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-30 03:39:35 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 03:40:53 +0200 | <Inst> | was this why hoogle went down? |
| 2024-09-30 03:40:57 +0200 | <Inst> | https://blog.haskell.org/haskell-foundation-and-committee-merger/ |
| 2024-09-30 03:42:07 +0200 | <geekosaur> | no? hoogle's been unstable for a while now, I think it just got too big (hoogle v5 has some fairly strict database size limits) |
| 2024-09-30 03:45:24 +0200 | <Inst> | it was the first time i saw hoogle go down |
| 2024-09-30 03:46:10 +0200 | <geekosaur> | it's been over a month. I'm certain because I've reported it to #haskell-infrastructure multiple times |
| 2024-09-30 03:47:44 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 260 seconds) |
| 2024-09-30 03:48:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 03:56:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-30 03:56:45 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-09-30 03:58:07 +0200 | Typedfern | (~Typedfern@2a02:9130:9c34:14e4:d11e:8149:a19f:6793) (Ping timeout: 265 seconds) |
| 2024-09-30 03:58:59 +0200 | identity | (~identity@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
| 2024-09-30 03:59:55 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 04:01:19 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-09-30 04:02:52 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2024-09-30 04:03:10 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-09-30 04:04:14 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 04:07:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 04:12:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-30 04:16:16 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 260 seconds) |
| 2024-09-30 04:16:38 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2024-09-30 04:23:04 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-09-30 04:23:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 04:25:09 +0200 | Inst | (~Inst@user/Inst) (Remote host closed the connection) |
| 2024-09-30 04:25:34 +0200 | Inst | (~Inst@user/Inst) Inst |
| 2024-09-30 04:26:47 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 04:28:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 04:31:20 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-09-30 04:32:14 +0200 | bh34e5 | (~bh34e5@user/bh34e5) (Ping timeout: 255 seconds) |
| 2024-09-30 04:35:14 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 04:39:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 04:41:20 +0200 | td_ | (~td@i53870935.versanet.de) (Ping timeout: 252 seconds) |
| 2024-09-30 04:43:11 +0200 | td_ | (~td@i53870928.versanet.de) |
| 2024-09-30 04:44:14 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-09-30 04:44:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-30 04:48:34 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2024-09-30 04:50:30 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-30 04:51:36 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-09-30 04:52:12 +0200 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-09-30 04:55:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 05:00:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-30 05:05:55 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-09-30 05:06:23 +0200 | Typedfern | (~Typedfern@2a02:9130:9c34:14e4:3caf:37c0:2522:467b) |
| 2024-09-30 05:08:06 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-09-30 05:10:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 05:12:17 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-09-30 05:15:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-30 05:22:56 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-09-30 05:26:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 05:31:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 05:42:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 05:43:29 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 265 seconds) |
| 2024-09-30 05:44:35 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-09-30 05:45:32 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) athan |
| 2024-09-30 05:47:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-30 05:52:40 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 265 seconds) |
| 2024-09-30 05:53:22 +0200 | michalz | (~michalz@185.246.207.197) |
| 2024-09-30 05:57:57 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:4e01:3d77:727d:559b) (Ping timeout: 252 seconds) |
| 2024-09-30 05:58:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 05:58:57 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:467d:3e5f:31ca:9a0a) jle` |
| 2024-09-30 06:03:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-30 06:07:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 06:12:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 06:23:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 06:25:57 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-09-30 06:27:01 +0200 | youthlic | (~Thunderbi@user/youthlic) (Ping timeout: 248 seconds) |
| 2024-09-30 06:31:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-30 06:42:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 06:47:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 06:49:39 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) machinedgod |
| 2024-09-30 06:50:01 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-09-30 06:53:08 +0200 | Guest88 | (~Guest99@2806:2f0:1000:c843:4888:b302:2f13:2d52) |
| 2024-09-30 06:57:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 06:58:53 +0200 | Guest88 | Laverga |
| 2024-09-30 07:03:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-30 07:09:27 +0200 | <haskellbridge> | <thirdofmay18081814goya> is there some sort of useful mathematical representation of trees? maybe with some linear algebra? |
| 2024-09-30 07:09:29 +0200 | Vajb | (~Vajb@n7m8bu6eaitlx0eukg2-1.v6.elisa-mobile.fi) |
| 2024-09-30 07:10:01 +0200 | Laverga | (~Guest99@2806:2f0:1000:c843:4888:b302:2f13:2d52) (Ping timeout: 256 seconds) |
| 2024-09-30 07:11:05 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-09-30 07:11:58 +0200 | bliminse | (~bliminse@user/bliminse) (Quit: leaving) |
| 2024-09-30 07:13:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 07:15:02 +0200 | <Lears> | thirdofmay: I don't know what you're looking for---a tree is already a mathematical object. But as a graph its adjacency relation can be written as a matrix I suppose. |
| 2024-09-30 07:18:23 +0200 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2024-09-30 07:18:36 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm right, I was thinking what sort of mathematical representation would be useful for thinking about transformations on trees |
| 2024-09-30 07:18:52 +0200 | <haskellbridge> | <thirdofmay18081814goya> will look up how to express them wrt adjecency relation, ty |
| 2024-09-30 07:19:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-30 07:20:07 +0200 | alp | (~alp@2001:861:e3d6:8f80:8ed3:89ad:bffe:2596) |
| 2024-09-30 07:20:13 +0200 | alp | (~alp@2001:861:e3d6:8f80:8ed3:89ad:bffe:2596) (Changing host) |
| 2024-09-30 07:20:13 +0200 | alp | (~alp@user/alp) alp |
| 2024-09-30 07:23:04 +0200 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit) |
| 2024-09-30 07:29:02 +0200 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya which kinds of transformations on trees? Recursion schemes may help, specially cata. You get equational reasoning for free too |
| 2024-09-30 07:29:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 07:29:45 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm right |
| 2024-09-30 07:30:00 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah any tree is just some datatype defined through a fixpoint |
| 2024-09-30 07:30:07 +0200 | <haskellbridge> | <thirdofmay18081814goya> right |
| 2024-09-30 07:30:08 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-09-30 07:30:09 +0200 | <haskellbridge> | <thirdofmay18081814goya> this could work |
| 2024-09-30 07:31:01 +0200 | andrewboltachev | (~andrey@178.141.123.3) andrewboltachev |
| 2024-09-30 07:33:17 +0200 | <haskellbridge> | <Bowuigi> Yeah, you might even be able to skip over some cases by sort of unrolling loops and simplifying sums, like, "List a = 1 + (a * rec)" being expanded to "a * a * ... * 1", that is, "a^n". Might not happen on every tree but it can be useful |
| 2024-09-30 07:33:18 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 276 seconds) |
| 2024-09-30 07:33:35 +0200 | <haskellbridge> | <thirdofmay18081814goya> it's a good idea ty for recommendation! |
| 2024-09-30 07:34:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-30 07:35:17 +0200 | <haskellbridge> | <Bowuigi> Good luck and remember to Reason Isomorphically! |
| 2024-09-30 07:45:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 07:46:56 +0200 | gdown | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown |
| 2024-09-30 07:50:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-30 07:50:31 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-30 07:52:27 +0200 | gdown | floyza |
| 2024-09-30 07:53:36 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 2024-09-30 07:53:53 +0200 | gdown | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown |
| 2024-09-30 07:54:07 +0200 | <Axman6> | That just sounds like the reasoning I already have! |
| 2024-09-30 07:54:21 +0200 | acidjnk | (~acidjnk@p200300d6e72cfb276c1c454e32c34a99.dip0.t-ipconnect.de) acidjnk |
| 2024-09-30 07:54:25 +0200 | gdown | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 2024-09-30 07:54:42 +0200 | gdown | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown |
| 2024-09-30 07:54:57 +0200 | gdown | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 2024-09-30 07:55:15 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown |
| 2024-09-30 07:56:03 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 2024-09-30 08:01:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 08:03:33 +0200 | bliminse | (~bliminse@user/bliminse) bliminse |
| 2024-09-30 08:06:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-30 08:07:30 +0200 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2024-09-30 08:07:48 +0200 | alp | (~alp@2001:861:e3d6:8f80:5ec8:1cec:7a:413a) |
| 2024-09-30 08:07:50 +0200 | alp | (~alp@2001:861:e3d6:8f80:5ec8:1cec:7a:413a) (Changing host) |
| 2024-09-30 08:07:50 +0200 | alp | (~alp@user/alp) alp |
| 2024-09-30 08:10:37 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-09-30 08:13:07 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-09-30 08:16:04 +0200 | Xe | (~cadey@perl/impostor/xe) (Ping timeout: 260 seconds) |
| 2024-09-30 08:16:47 +0200 | <jackdk> | dohohoho |
| 2024-09-30 08:16:52 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 08:22:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-30 08:23:44 +0200 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-09-30 08:27:13 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-30 08:27:25 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2024-09-30 08:32:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 08:35:01 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2024-09-30 08:36:49 +0200 | <haskellbridge> | <Bowuigi> I was mostly referring to the paper of the same name by Hinze and James, but it works either way |
| 2024-09-30 08:37:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-30 08:39:34 +0200 | <haskellbridge> | <Bowuigi> Is there any formalization of System F with type operators but without type abstractions? In particular, with Haskell-style newtypes and taking built-in type operators into account |
| 2024-09-30 08:40:30 +0200 | <haskellbridge> | <Bowuigi> Outside of System FC, that is. That extension has way more than what I need |
| 2024-09-30 08:41:29 +0200 | poscat0x04 | (~poscat@user/poscat) poscat |
| 2024-09-30 08:41:54 +0200 | poscat | (~poscat@user/poscat) (Ping timeout: 260 seconds) |
| 2024-09-30 08:42:36 +0200 | <haskellbridge> | <Bowuigi> I could just grab the kinding from Leijen2004 (or any type system with type constructors) and call it a day, but if there are any better ways to do this I'm open to suggestions |
| 2024-09-30 08:43:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 08:44:40 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2024-09-30 08:48:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-30 08:50:46 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-09-30 08:54:25 +0200 | ft | (~ft@p4fc2acce.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-09-30 08:58:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-09-30 08:59:43 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-09-30 09:00:02 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-09-30 09:00:42 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2024-09-30 09:06:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-30 09:09:25 +0200 | misterfish | (~misterfis@87.215.131.102) misterfish |
| 2024-09-30 09:18:39 +0200 | cipherrot | (~znc-user@user/petrichor) petrichor |
| 2024-09-30 09:20:18 +0200 | petrichor | (~znc-user@user/petrichor) (Ping timeout: 272 seconds) |
| 2024-09-30 09:20:23 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-09-30 09:29:03 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-09-30 09:31:29 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-30 09:34:08 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-09-30 09:35:54 +0200 | CiaoSen | (~Jura@2a05:5800:2e8:8f00:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-09-30 09:36:56 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-30 09:41:55 +0200 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2024-09-30 09:42:35 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-09-30 09:43:33 +0200 | alp | (~alp@2001:861:e3d6:8f80:5ec8:1cec:7a:413a) |
| 2024-09-30 09:43:41 +0200 | alp | (~alp@2001:861:e3d6:8f80:5ec8:1cec:7a:413a) (Changing host) |
| 2024-09-30 09:43:41 +0200 | alp | (~alp@user/alp) alp |
| 2024-09-30 09:47:27 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) |
| 2024-09-30 09:47:43 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) (Changing host) |
| 2024-09-30 09:47:43 +0200 | vincent42 | (uid574193@user/vincent42) vincent42 |
| 2024-09-30 09:48:27 +0200 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2024-09-30 09:53:51 +0200 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 246 seconds) |
| 2024-09-30 09:55:28 +0200 | kritzefitz | (~kritzefit@debian/kritzefitz) kritzefitz |
| 2024-09-30 09:55:47 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 265 seconds) |
| 2024-09-30 09:58:20 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 09:58:22 +0200 | alp | (~alp@2001:861:e3d6:8f80:5ec8:1cec:7a:413a) |
| 2024-09-30 09:58:23 +0200 | alp | (~alp@2001:861:e3d6:8f80:5ec8:1cec:7a:413a) (Changing host) |
| 2024-09-30 09:58:23 +0200 | alp | (~alp@user/alp) alp |
| 2024-09-30 10:00:09 +0200 | kuribas | (~user@ptr-17d51emnflxb1h2uq90.18120a2.ip6.access.telenet.be) kuribas |
| 2024-09-30 10:07:39 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2024-09-30 10:11:07 +0200 | <haskellbridge> | <carbolymer`> @pl mconcat . map |
| 2024-09-30 10:11:16 +0200 | <haskellbridge> | <carbolymer`> how do I call lambdabot from matrix |
| 2024-09-30 10:11:44 +0200 | <geekosaur> | put a blank line first |
| 2024-09-30 10:12:12 +0200 | <haskellbridge> | <geekosaur> @pl mconcat . map |
| 2024-09-30 10:12:23 +0200 | <haskellbridge> | <geekosaur> m, my client didn't play along there |
| 2024-09-30 10:12:29 +0200 | <haskellbridge> | <carbolymer`> :D |
| 2024-09-30 10:12:37 +0200 | <haskellbridge> | <carbolymer`> @pl mconcat . map |
| 2024-09-30 10:12:38 +0200 | <haskellbridge> | <geekosaur> @b52 |
| 2024-09-30 10:12:39 +0200 | <haskellbridge> | <carbolymer`> no bueno |
| 2024-09-30 10:12:57 +0200 | <haskellbridge> | <geekosaur> I wonder if the latest update removes them. this used to work :( |
| 2024-09-30 10:14:11 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 10:14:36 +0200 | <haskellbridge> | <geekosaur> . |
| 2024-09-30 10:14:36 +0200 | <haskellbridge> | @pl mconcat . map |
| 2024-09-30 10:14:47 +0200 | <geekosaur> | it's also inserting spaces 😞 |
| 2024-09-30 10:16:05 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 265 seconds) |
| 2024-09-30 10:20:33 +0200 | chele | (~chele@user/chele) chele |
| 2024-09-30 10:22:36 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-30 10:23:30 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-09-30 10:26:59 +0200 | troydm | (~troydm@user/troydm) (Read error: Connection reset by peer) |
| 2024-09-30 10:34:21 +0200 | <lortabac> | in a multi-package project, is there a way to specify ghc-options for all the packages in cabal.project.local? |
| 2024-09-30 10:39:23 +0200 | <lortabac> | nevermind, I found it. You can start a stanza with 'package *' |
| 2024-09-30 10:44:23 +0200 | troydm | (~troydm@user/troydm) troydm |
| 2024-09-30 10:46:53 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 252 seconds) |
| 2024-09-30 10:52:20 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-09-30 10:57:04 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 260 seconds) |
| 2024-09-30 10:57:51 +0200 | synchromesh | (~john@2406:5a00:241a:5600:e176:3a40:8bde:547a) (Read error: Connection reset by peer) |
| 2024-09-30 10:58:53 +0200 | synchromesh | (~john@2406:5a00:241a:5600:a1ef:6d76:30da:3d0e) synchromesh |
| 2024-09-30 10:59:54 +0200 | polyphem | (~rod@pd9fbf2fe.dip0.t-ipconnect.de) polyphem |
| 2024-09-30 11:00:28 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-09-30 11:01:51 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-09-30 11:04:07 +0200 | Vengeance_ | (~Vengeance@2.219.56.221) (Ping timeout: 252 seconds) |
| 2024-09-30 11:04:08 +0200 | Xe | (~cadey@perl/impostor/xe) Xe |
| 2024-09-30 11:07:19 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2024-09-30 11:11:16 +0200 | misterfish | (~misterfis@178.229.145.184) misterfish |
| 2024-09-30 11:21:59 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-09-30 11:23:21 +0200 | vanced | (~Vengeance@2.219.56.221) |
| 2024-09-30 11:24:29 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-09-30 11:24:30 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-09-30 11:27:15 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-09-30 11:37:55 +0200 | <haskellbridge> | <carbolymer`> @pl |
| 2024-09-30 11:39:08 +0200 | <haskellbridge> | <carbolymer`> tbf @ is not a great choice for command character for a bot |
| 2024-09-30 11:40:12 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-09-30 11:42:53 +0200 | <tomsmeding> | carbolymer`: on irc there is no special behaviour for @ ;) |
| 2024-09-30 11:43:43 +0200 | <haskellbridge> | <carbolymer`> tomsmeding: yes, but it's used to mark OP in quite a lot of clients, so when you're writing to someone, sometimes @ gets copied |
| 2024-09-30 11:44:59 +0200 | <tomsmeding> | % putStrLn "@pl \x -> x" |
| 2024-09-30 11:44:59 +0200 | <yahb2> | <interactive>:17:17: error: [GHC-21231] ; lexical error in string/character literal at character ' ' |
| 2024-09-30 11:45:03 +0200 | <tomsmeding> | % putStrLn "@pl \\x -> x" |
| 2024-09-30 11:45:03 +0200 | <yahb2> | @pl \x -> x |
| 2024-09-30 11:45:10 +0200 | <tomsmeding> | ah, lambdabot ignores yahb2 |
| 2024-09-30 11:45:18 +0200 | <tomsmeding> | @botsnack |
| 2024-09-30 11:45:18 +0200 | <lambdabot> | :) |
| 2024-09-30 11:46:43 +0200 | briandaed | (~root@185.234.210.211) |
| 2024-09-30 11:51:22 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-30 11:54:37 +0200 | <Inst> | huh |
| 2024-09-30 11:54:58 +0200 | <Inst> | in Haskell, a :: Peano; a = S a is a valid value |
| 2024-09-30 11:55:57 +0200 | <tomsmeding> | > let ones = 1 : ones in ones |
| 2024-09-30 11:55:59 +0200 | <lambdabot> | [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1... |
| 2024-09-30 11:56:16 +0200 | <ncf> | the natural numbers and conatural numbers coincide in haskell |
| 2024-09-30 11:58:36 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2024-09-30 12:01:04 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
| 2024-09-30 12:01:27 +0200 | xff0x | (~xff0x@182.169.73.28) (Ping timeout: 265 seconds) |
| 2024-09-30 12:02:49 +0200 | <int-e> | are those the chosen ones |
| 2024-09-30 12:03:29 +0200 | <Inst> | by lambdabot, yes |
| 2024-09-30 12:03:49 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-09-30 12:06:25 +0200 | <ski> | afaik, IRC clients normally don't copy channel status like `@' or `+', when completing nicknames |
| 2024-09-30 12:07:33 +0200 | <ski> | (i also think `@' is a good choice, to subtly encourage people to not add `@' willynilly to nicknames when addressing them) |
| 2024-09-30 12:09:00 +0200 | <__monty__> | ski: They're using the haskellbridge. On the Matrix side you have to prefix names with @ to "mention" someone. |
| 2024-09-30 12:10:49 +0200 | <Inst> | monty: why are you a dunder method? |
| 2024-09-30 12:16:31 +0200 | <ski> | yea, i was talking about people on the IRC side, __monty__ |
| 2024-09-30 12:17:10 +0200 | vincent42 | (uid574193@user/vincent42) (Quit: Connection closed for inactivity) |
| 2024-09-30 12:18:26 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-09-30 12:22:41 +0200 | <Inst> | hmmm, I wonder what happens if |
| 2024-09-30 12:23:17 +0200 | <Inst> | > fmap (+1) [minBound .. maxBound] == fmap (+1) ([minBound .. maxBound] :: [Int]) |
| 2024-09-30 12:23:23 +0200 | <lambdabot> | mueval-core: Time limit exceeded |
| 2024-09-30 12:23:54 +0200 | <Inst> | i'm still waiting for haskell to show function equality on my ghci :( |
| 2024-09-30 12:24:04 +0200 | <Inst> | for the simple case |
| 2024-09-30 12:26:23 +0200 | <int-e> | why. you won't live to see that finish on a 64 bit system. |
| 2024-09-30 12:28:54 +0200 | <Inst> | ~10^19, yup :( |
| 2024-09-30 12:32:42 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 12:33:31 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-09-30 12:37:13 +0200 | <ncf> | 19? |
| 2024-09-30 12:37:30 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 2024-09-30 12:37:46 +0200 | <int-e> | > 64 * logBase 10 2 |
| 2024-09-30 12:37:48 +0200 | <lambdabot> | 19.265919722494793 |
| 2024-09-30 12:37:56 +0200 | <ncf> | ah |
| 2024-09-30 12:43:04 +0200 | <__monty__> | Inst: You've started on the road to a pun. |
| 2024-09-30 12:45:26 +0200 | misterfish | (~misterfis@178.229.145.184) (Ping timeout: 265 seconds) |
| 2024-09-30 12:48:13 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-30 12:58:17 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2024-09-30 13:06:50 +0200 | misterfish | (~misterfis@87.215.131.102) misterfish |
| 2024-09-30 13:07:11 +0200 | Typedfern | (~Typedfern@2a02:9130:9c34:14e4:3caf:37c0:2522:467b) (Ping timeout: 265 seconds) |
| 2024-09-30 13:10:45 +0200 | xff0x | (~xff0x@2405:6580:b080:900:4c01:617c:3138:9e79) |
| 2024-09-30 13:10:50 +0200 | CiaoSen | (~Jura@2a05:5800:2e8:8f00:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 2024-09-30 13:18:04 +0200 | comerijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 13:20:00 +0200 | Typedfern | (~Typedfern@2a02:9130:9c33:296c:4caa:2c3a:afbd:6119) |
| 2024-09-30 13:20:32 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2024-09-30 13:32:34 +0200 | Typedfern | (~Typedfern@2a02:9130:9c33:296c:4caa:2c3a:afbd:6119) (Ping timeout: 244 seconds) |
| 2024-09-30 13:33:05 +0200 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2024-09-30 13:43:18 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 13:44:13 +0200 | Typedfern | (~Typedfern@2a02:9130:9c33:296c:d6c0:1874:d2f5:c68c) |
| 2024-09-30 13:56:24 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds) |
| 2024-09-30 13:56:57 +0200 | <geekosaur> | Inst, https://hackage.haskell.org/package/universe-1.2.3/docs/Data-Universe-Instances-Reverse.html? |
| 2024-09-30 13:58:05 +0200 | <geekosaur> | (with, indeed, the problem of time; but that's your problem 😛 ) |
| 2024-09-30 13:59:34 +0200 | alp | (~alp@user/alp) (Remote host closed the connection) |
| 2024-09-30 14:05:37 +0200 | cipherrot | (~znc-user@user/petrichor) (Read error: Connection reset by peer) |
| 2024-09-30 14:08:21 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2024-09-30 14:08:56 +0200 | petrichor | (~znc-user@user/petrichor) petrichor |
| 2024-09-30 14:09:06 +0200 | petrichor | (~znc-user@user/petrichor) (Read error: Connection reset by peer) |
| 2024-09-30 14:14:50 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 14:19:41 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-09-30 14:24:35 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2024-09-30 14:24:56 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2024-09-30 14:25:49 +0200 | pointlessslippe1 | (~pointless@62.106.85.17) (Read error: Connection reset by peer) |
| 2024-09-30 14:31:10 +0200 | identity | (~identity@user/ZharMeny) identity |
| 2024-09-30 14:34:00 +0200 | pointlessslippe1 | (~pointless@62.106.85.17) pointlessslippe1 |
| 2024-09-30 14:34:10 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 14:35:17 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 14:38:38 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 2024-09-30 14:43:01 +0200 | xff0x | (~xff0x@2405:6580:b080:900:4c01:617c:3138:9e79) (Ping timeout: 252 seconds) |
| 2024-09-30 14:47:49 +0200 | CiaoSen | (~Jura@2a05:5800:2e8:8f00:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-09-30 14:55:52 +0200 | xff0x | (~xff0x@2405:6580:b080:900:4c01:617c:3138:9e79) |
| 2024-09-30 15:06:49 +0200 | synchromesh | (~john@2406:5a00:241a:5600:a1ef:6d76:30da:3d0e) (Read error: Connection reset by peer) |
| 2024-09-30 15:07:31 +0200 | synchromesh | (~john@2406:5a00:241a:5600:a1ef:6d76:30da:3d0e) synchromesh |
| 2024-09-30 15:11:57 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-30 15:16:43 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 265 seconds) |
| 2024-09-30 15:20:53 +0200 | Guest10 | (~Guest10@2400:56a0:3c1:6224:aab1:a164:91f6:1222) |
| 2024-09-30 15:21:32 +0200 | mzg | (mzg@abusers.hu) |
| 2024-09-30 15:22:13 +0200 | Guest10 | (~Guest10@2400:56a0:3c1:6224:aab1:a164:91f6:1222) (Client Quit) |
| 2024-09-30 15:22:16 +0200 | <cheater> | i honestly don't really understand what people are using universe for |
| 2024-09-30 15:22:32 +0200 | <cheater> | it seems like something that belongs in drupal |
| 2024-09-30 15:25:36 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-09-30 15:27:20 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-09-30 15:31:13 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-09-30 15:33:41 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-09-30 15:36:03 +0200 | CiaoSen | (~Jura@2a05:5800:2e8:8f00:ca4b:d6ff:fec1:99da) (Ping timeout: 244 seconds) |
| 2024-09-30 15:40:40 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 15:42:31 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-09-30 15:43:12 +0200 | codaraxis | (~codaraxis@user/codaraxis) Codaraxis |
| 2024-09-30 15:53:23 +0200 | Shires | (~Shires@81.170.22.200) |
| 2024-09-30 15:54:24 +0200 | Shires | (~Shires@81.170.22.200) () |
| 2024-09-30 15:58:11 +0200 | Yesman | (~Yesman@103.182.161.2) |
| 2024-09-30 15:59:52 +0200 | Yesman | (~Yesman@103.182.161.2) (Client Quit) |
| 2024-09-30 16:00:03 +0200 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
| 2024-09-30 16:00:22 +0200 | Guest9426 | (~User@103.182.161.2) |
| 2024-09-30 16:01:25 +0200 | spew | (~spew@201.141.99.170) spew |
| 2024-09-30 16:01:40 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 265 seconds) |
| 2024-09-30 16:02:05 +0200 | <Guest9426> | Can someone recommend a good learning resource to start learning haskell since there seems to be way too many to choose from and a lot of them might be outdated |
| 2024-09-30 16:02:43 +0200 | <ski> | @where CIS194 |
| 2024-09-30 16:02:43 +0200 | <lambdabot> | <https://github.com/byorgey/haskell-course>,<https://www.seas.upenn.edu/~cis194/spring13/lectures.html> |
| 2024-09-30 16:03:54 +0200 | <opqdonut> | Guest9426: https://haskell.mooc.fi is a fairly up-to-date course on the basics |
| 2024-09-30 16:05:09 +0200 | <Guest9426> | Aight cheers I'll go take a look |
| 2024-09-30 16:10:00 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-09-30 16:13:07 +0200 | Guest9426 | (~User@103.182.161.2) (Quit: Client closed) |
| 2024-09-30 16:20:31 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-09-30 16:21:16 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 16:28:49 +0200 | codaraxis__ | (~codaraxis@user/codaraxis) Codaraxis |
| 2024-09-30 16:32:17 +0200 | codaraxis | (~codaraxis@user/codaraxis) (Ping timeout: 252 seconds) |
| 2024-09-30 16:38:47 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-09-30 16:39:26 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2024-09-30 16:40:22 +0200 | aforemny_ | (~aforemny@2001:9e8:6cd4:700:eda4:904a:ed7b:86ce) aforemny |
| 2024-09-30 16:40:49 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2024-09-30 16:40:49 +0200 | aforemny | (~aforemny@i59F4C7BB.versanet.de) (Ping timeout: 265 seconds) |
| 2024-09-30 16:40:50 +0200 | ljdarj1 | ljdarj |
| 2024-09-30 16:45:00 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-09-30 17:07:15 +0200 | floyza | (~gavin@h69-11-148-150.kndrid.broadband.dynamic.tds.net) gdown |
| 2024-09-30 17:15:55 +0200 | misterfish | (~misterfis@84.53.85.146) misterfish |
| 2024-09-30 17:20:56 +0200 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 265 seconds) |
| 2024-09-30 17:21:22 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-09-30 17:21:30 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds) |
| 2024-09-30 17:23:54 +0200 | <Inst> | why doesn't Haskell accept this? |
| 2024-09-30 17:25:20 +0200 | <Inst> | https://paste.tomsmeding.com/ZFG0CItc |
| 2024-09-30 17:25:54 +0200 | <Inst> | should Haskell accept this? |
| 2024-09-30 17:26:07 +0200 | <ski> | you can't match on functions with data constructors |
| 2024-09-30 17:26:20 +0200 | <Rembane> | Inst: Try Left{} instead |
| 2024-09-30 17:26:52 +0200 | <ski> | each data constructor pattern must be a data constructor fully applied to patterns corresponding to all the component arguments of the data constructor |
| 2024-09-30 17:27:01 +0200 | <ncf> | your match isn't complete, if anything |
| 2024-09-30 17:27:15 +0200 | <ski> | yea, that too |
| 2024-09-30 17:27:17 +0200 | <ncf> | consider foo @Bool (bool (Left True) (Right False)) |
| 2024-09-30 17:27:30 +0200 | <Inst> | yeah I thought it was a weird exception that'd allow me to match on functions since data constructosr are functions |
| 2024-09-30 17:27:40 +0200 | <ski> | (and using `Left {}' doesn't help with this) |
| 2024-09-30 17:27:54 +0200 | <ski> | `False' is a data constructor that is not a function |
| 2024-09-30 17:28:39 +0200 | <Inst> | or in other words, haskell can only match on fully applied data constructors |
| 2024-09-30 17:28:58 +0200 | <ski> | yes |
| 2024-09-30 17:29:17 +0200 | <Inst> | or in other words, why? |
| 2024-09-30 17:29:43 +0200 | <Inst> | iirc function equality is a complete nightmare to deal with |
| 2024-09-30 17:30:07 +0200 | <Inst> | is that why, since if / case compiles to case foo of True; False in core |
| 2024-09-30 17:30:22 +0200 | <ski> | think of `Node :: a -> [Tree a] -> Tree a' as a function that takes an `a', returning a new function that takes a list of trees of `a's, and *then* constructs an aggregate compound that contains/holds these two items, for later retrieval |
| 2024-09-30 17:31:00 +0200 | <ski> | if you only applied it to an `a', getting a `[Tree a] -> Tree a' back, the container hasn't been created yet, so you can't match to extract things from it |
| 2024-09-30 17:31:25 +0200 | <Inst> | there's a hacky way to do it, though |
| 2024-09-30 17:31:26 +0200 | <ski> | function equality is not decidable, in general |
| 2024-09-30 17:31:46 +0200 | <Inst> | well, plain unsafe / unidiomatic |
| 2024-09-30 17:31:47 +0200 | <ski> | that's how an implementation would probably implement it |
| 2024-09-30 17:32:34 +0200 | <ski> | in OCaml, you can't even partially apply a data constructor, you must always spell it out fully applied. if you want the constructor function, you must type a lambda, like `fun x -> Some x', rather than just `Some' |
| 2024-09-30 17:33:02 +0200 | <ski> | in Haskell, think of (unapplied) `Left' as being shorthand for `\x -> Left x' |
| 2024-09-30 17:33:20 +0200 | <Inst> | https://paste.tomsmeding.com/VypZIobC |
| 2024-09-30 17:33:37 +0200 | <Inst> | sorry for the unintentional obscenity |
| 2024-09-30 17:34:05 +0200 | <ski> | Inst : now try `f (\x -> seq x (Left x))' |
| 2024-09-30 17:34:46 +0200 | <Inst> | hence why it's unsafe |
| 2024-09-30 17:34:47 +0200 | <ski> | or `f (\b -> if b then Left (not b) else Right 42)' |
| 2024-09-30 17:35:29 +0200 | <ski> | (the latter case, as well as ncf's example, shows why you're not exhausetive, not covering all cases) |
| 2024-09-30 17:36:34 +0200 | <ski> | (not all functions returning an `Either' decides to return a `Left', alternatively a `Right', *independently* of what the argument was) |
| 2024-09-30 17:37:18 +0200 | <Inst> | which i guess answers my question, for Haskell to accept this you'd have to give data constructors special types |
| 2024-09-30 17:43:44 +0200 | <monochrom> | Are you sure you do not want instead (forall a. a -> Either a a) -> String, which actually narrows down the possibilities? |
| 2024-09-30 17:44:17 +0200 | <Inst> | still doesn't get rid of seq |
| 2024-09-30 17:44:36 +0200 | <monochrom> | But then why not simplify it to Bool -> String? |
| 2024-09-30 17:45:10 +0200 | <Inst> | but thanks, monochrom, that fixes the unsafe code |
| 2024-09-30 17:46:09 +0200 | jimbob88 | (~jimbob88@shef-16-b2-v4wan-169443-cust2838.vm3.cable.virginm.net) |
| 2024-09-30 17:46:40 +0200 | <monochrom> | That may be my next exam question. :) Prove: If e :: forall a. a -> Either a a, then e = Left or e = Right. |
| 2024-09-30 17:48:15 +0200 | <monochrom> | But "foo e = case e () of Left _ -> x; Right _ -> y" does not need seq. |
| 2024-09-30 17:48:25 +0200 | anpad | (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-09-30 17:48:46 +0200 | <monochrom> | if foo is rank-2 so e is polymorphic so you can choose (). |
| 2024-09-30 17:49:05 +0200 | <Inst> | yeah, I used unit as well in the fixed code |
| 2024-09-30 17:51:05 +0200 | <Inst> | but we get a fun type error here |
| 2024-09-30 17:51:21 +0200 | <Inst> | let u = Left :: String -> Either String a |
| 2024-09-30 17:51:23 +0200 | jimbob88 | (~jimbob88@shef-16-b2-v4wan-169443-cust2838.vm3.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2024-09-30 17:52:02 +0200 | <ski> | need to actually pass a polymorphic argument |
| 2024-09-30 17:52:55 +0200 | <Inst> | i mean i know it'll produce a type error |
| 2024-09-30 17:53:38 +0200 | <monochrom> | String -> Either String a has more possibilities than Left. For example, Left . reverse. |
| 2024-09-30 17:55:09 +0200 | <monochrom> | And by the time you tell me "a" is not really a variable, just a secret, you really have String -> Either String Int, then "\x -> if null x then Left "hello" else Right (length x)" is also possible so it is not "always Left" or "always Right". |
| 2024-09-30 17:55:31 +0200 | <tomsmeding> | monochrom: that exam question sounds tricky. Is `e = undefined` Left or Right? |
| 2024-09-30 17:55:58 +0200 | <monochrom> | The extra polymorphism I added is important to ensure that the input cannot be arbitrary. |
| 2024-09-30 17:56:15 +0200 | <monochrom> | tomsmeding: For that topic, we ignore bottoms. :) |
| 2024-09-30 17:56:48 +0200 | <tomsmeding> | do you actually cover parametricity and the laws you can derive rigorously that way? |
| 2024-09-30 17:56:53 +0200 | <tomsmeding> | that's pretty advanced |
| 2024-09-30 17:56:55 +0200 | <monochrom> | It is not a grad course, so I won't be teaching a version of parametricity that respects bottoms. >:) |
| 2024-09-30 17:57:04 +0200 | <tomsmeding> | even ignoring bottoms |
| 2024-09-30 17:57:12 +0200 | tomsmeding | never got that |
| 2024-09-30 17:57:16 +0200 | <monochrom> | Yes :) https://www.cs.utoronto.ca/~trebla/CSCC24-2024-Summer/abs-type-param.html |
| 2024-09-30 17:57:16 +0200 | <Inst> | what do you call the fact that we're ignoring id? |
| 2024-09-30 17:57:26 +0200 | <monochrom> | I found a way to make it not advanced. |
| 2024-09-30 17:57:54 +0200 | <monochrom> | Type error is why id cannot be X -> Either X Y |
| 2024-09-30 17:58:19 +0200 | <monochrom> | or forall a. a -> Either a a |
| 2024-09-30 17:58:25 +0200 | <tomsmeding> | monochrom: found a typo: the `in` in polyUse should be `ins` |
| 2024-09-30 17:58:42 +0200 | <monochrom> | Ooohhhh I thought I caught all typos. |
| 2024-09-30 17:59:30 +0200 | <monochrom> | Fixed! |
| 2024-09-30 17:59:35 +0200 | <tomsmeding> | yay! |
| 2024-09-30 18:01:01 +0200 | <monochrom> | There is a second instance of the same typo. But a second upload fixed it. |
| 2024-09-30 18:02:26 +0200 | <monochrom> | Eventually you will find that my trick is to use dynamic scoping! >:) |
| 2024-09-30 18:04:46 +0200 | <Inst> | hmmm, but in theory, it makes sense that Haskell could match on data constructors and partially applied data constructors, no? |
| 2024-09-30 18:05:18 +0200 | <ski> | how ? |
| 2024-09-30 18:05:19 +0200 | <tomsmeding> | in haskell we like eta-reduction/eta-abstraction to not do anything semantically |
| 2024-09-30 18:05:31 +0200 | <tomsmeding> | i.e. we'd like "\x -> f x" and "f" to behave the same |
| 2024-09-30 18:06:05 +0200 | <__monty__> | I wonder why I always have the most trouble implementing <*> of all the Functor to Monad concepts. |
| 2024-09-30 18:06:09 +0200 | <tomsmeding> | if we'd allow matching on partially-applied data constructors, then somehow "C" would behave differently from "\x -> C x", which is not a partially-applied datacon but instead a function |
| 2024-09-30 18:06:24 +0200 | <tomsmeding> | and also, we want stuff like "you can match on this" to be determinable from types alonr |
| 2024-09-30 18:06:26 +0200 | <tomsmeding> | *alone |
| 2024-09-30 18:06:29 +0200 | <tomsmeding> | Inst: hence that won't work |
| 2024-09-30 18:06:35 +0200 | <tomsmeding> | __monty__: (<*>) = ap |
| 2024-09-30 18:06:36 +0200 | <ski> | __monty__ : `liftA2's simpler ? |
| 2024-09-30 18:06:36 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-09-30 18:08:39 +0200 | <Inst> | tomsmeding: i'm actually hard-pressed to imagine a case where being able to match on data constructosr would be useful |
| 2024-09-30 18:08:51 +0200 | <Inst> | data Foo = Bar Int | Baz Char |
| 2024-09-30 18:08:56 +0200 | <tomsmeding> | on a *partially applied data constructor, I guess you mean? |
| 2024-09-30 18:09:04 +0200 | <Inst> | in this case, though, it'd be a simple type violation, no? |
| 2024-09-30 18:09:16 +0200 | <tomsmeding> | what would you expect the syntax to even be |
| 2024-09-30 18:09:33 +0200 | <__monty__> | ski: Presuming <*>, yes. |
| 2024-09-30 18:10:08 +0200 | <tomsmeding> | and without <*>? :p |
| 2024-09-30 18:11:52 +0200 | <ski> | __monty__ : sometimes `join' is easier or clearer to write directly, rather than `(>>=)'. i was wondering what you similarly thought about `liftA2' vs. `(<*>)' |
| 2024-09-30 18:13:00 +0200 | <c_wraith> | > case Left "hello" of Left{} -> 1 ; Right{} -> 2 -- Inst |
| 2024-09-30 18:13:01 +0200 | <lambdabot> | 1 |
| 2024-09-30 18:13:26 +0200 | <Inst> | tomsmeding: something like just parensing a partially applied data constructor, but either case, Left / Right is like a special case, otherwise it's usually just begging for inconsistent types |
| 2024-09-30 18:13:34 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-09-30 18:13:42 +0200 | <Inst> | c_wraith: wait, do people actually use that syntax? |
| 2024-09-30 18:13:47 +0200 | <c_wraith> | sometimes. |
| 2024-09-30 18:14:00 +0200 | <tomsmeding> | sometimes, yes |
| 2024-09-30 18:14:10 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-09-30 18:14:21 +0200 | <tomsmeding> | still not sure where the inconsistent types come from or what you really mean :p |
| 2024-09-30 18:15:45 +0200 | <c_wraith> | It mostly depends on what kinds of changes you're expecting. Like, you'd never expect Either to change its definition, so it really doesn't matter. But if you have some domain type that might frequently change during development it can matter. |
| 2024-09-30 18:16:26 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-09-30 18:16:29 +0200 | <Inst> | if you're trying to top level pattern match on a constructor from Foo |
| 2024-09-30 18:16:32 +0200 | <c_wraith> | You'd use positional match syntax if you want to reconsider your definition when the type changes. You'd use record match syntax when you want to ignore changes to the definition. |
| 2024-09-30 18:16:38 +0200 | <Inst> | what is the type of your function? |
| 2024-09-30 18:16:55 +0200 | <Inst> | Bar :: Int -> Foo; Baz :: Char -> Foo |
| 2024-09-30 18:17:28 +0200 | <tomsmeding> | the {} syntax is just from record syntax; it just allows you to elide the actual fields |
| 2024-09-30 18:17:34 +0200 | <tomsmeding> | there's nothing "partially applied" going on here |
| 2024-09-30 18:17:53 +0200 | <Inst> | you asked "what would you expect the syntax to even be" |
| 2024-09-30 18:18:11 +0200 | <Inst> | i pointed out there's a possible syntax but it makes no sense in a statically typed language |
| 2024-09-30 18:18:20 +0200 | <tomsmeding> | `f Left = ...`? |
| 2024-09-30 18:18:33 +0200 | <Inst> | I mean data Foo = Bar Int | Baz Char |
| 2024-09-30 18:18:39 +0200 | <tomsmeding> | `f Bar = ...`? |
| 2024-09-30 18:18:59 +0200 | <tomsmeding> | that syntax is indeed free, but typing indeed presents a problem |
| 2024-09-30 18:19:03 +0200 | <Inst> | f Bar = ...; f Baz = ...; f :: ??? |
| 2024-09-30 18:19:09 +0200 | <Inst> | That said: |
| 2024-09-30 18:19:24 +0200 | <Inst> | f Left Bar works |
| 2024-09-30 18:19:25 +0200 | <tomsmeding> | but also the eta-expansion argument that I gave which tells you that even if you'd have a data type for which the types do line up, we still don't want this |
| 2024-09-30 18:19:40 +0200 | andrewboltachev | (~andrey@178.141.123.3) (Quit: Leaving.) |
| 2024-09-30 18:20:22 +0200 | <tomsmeding> | because if you'd have `data Foo = Bar Int | Baz Int`, then perhaps `f :: (Int -> Foo) -> _`, but from that type I should also be able to pass `\n -> if n == 0 then Bar 42 else Baz 100` to f |
| 2024-09-30 18:20:24 +0200 | <tomsmeding> | and that ain't going to work |
| 2024-09-30 18:20:31 +0200 | <__monty__> | ski: Haven't written enough liftA2s to have an opinion TBH. |
| 2024-09-30 18:21:06 +0200 | <Inst> | the if expression isn't well-typed |
| 2024-09-30 18:21:25 +0200 | <ski> | __monty__ : well, if you do, you can use `(<*>) = liftA2 ($)' |
| 2024-09-30 18:21:31 +0200 | <tomsmeding> | % data Foo = Bar Int | Baz Char |
| 2024-09-30 18:21:32 +0200 | <yahb2> | <no output> |
| 2024-09-30 18:21:42 +0200 | <tomsmeding> | % :t \n -> if n == 0 then Bar 42 else Baz 100 |
| 2024-09-30 18:21:42 +0200 | <yahb2> | <interactive>:1:38: error: [GHC-39999] ; • Could not deduce ‘Num Char’ arising from the literal ‘100’ ; from the context: (Eq a, Num a) ; bound by the inferred type of it :: (Eq a... |
| 2024-09-30 18:21:48 +0200 | <tomsmeding> | % data Foo = Bar Int | Baz Int |
| 2024-09-30 18:21:48 +0200 | <yahb2> | <no output> |
| 2024-09-30 18:21:50 +0200 | <tomsmeding> | % :t \n -> if n == 0 then Bar 42 else Baz 100 |
| 2024-09-30 18:21:50 +0200 | <yahb2> | \n -> if n == 0 then Bar 42 else Baz 100 ; :: (Eq a, Num a) => a -> Foo |
| 2024-09-30 18:21:56 +0200 | <tomsmeding> | sorry that's what I meant |