2025-04-10 00:01:13 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
2025-04-10 00:01:30 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-04-10 00:02:35 +0200 | tromp | (~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2025-04-10 00:02:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-10 00:08:05 +0200 | krjst | (~krjst@2604:a880:800:c1::16b:8001) krjst |
2025-04-10 00:08:10 +0200 | tv | (~tv@user/tv) (Read error: Connection reset by peer) |
2025-04-10 00:14:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 00:15:20 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
2025-04-10 00:16:52 +0200 | krjst | (~krjst@2604:a880:800:c1::16b:8001) (Quit: bye) |
2025-04-10 00:18:26 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
2025-04-10 00:18:26 +0200 | ljdarj1 | ljdarj |
2025-04-10 00:20:20 +0200 | <__monty__> | Can you elaborate? |
2025-04-10 00:21:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
2025-04-10 00:21:39 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2025-04-10 00:23:00 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
2025-04-10 00:23:47 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
2025-04-10 00:32:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 00:33:09 +0200 | <EvanR> | supposedly A * B * C * D = A * (B * C) * D = (A * B) * C * C |
2025-04-10 00:33:14 +0200 | <EvanR> | D |
2025-04-10 00:33:23 +0200 | <EvanR> | but not really xD |
2025-04-10 00:33:33 +0200 | <EvanR> | when you get down to brass tacks |
2025-04-10 00:33:59 +0200 | <EvanR> | (or ML) |
2025-04-10 00:37:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-10 00:43:40 +0200 | tv | (~tv@user/tv) tv |
2025-04-10 00:43:48 +0200 | krjst | (~krjst@2604:a880:800:c1::16b:8001) krjst |
2025-04-10 00:47:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 00:52:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
2025-04-10 00:53:31 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
2025-04-10 01:00:16 +0200 | krjst | (~krjst@2604:a880:800:c1::16b:8001) (Quit: bye) |
2025-04-10 01:03:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 01:04:10 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 272 seconds) |
2025-04-10 01:06:30 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst |
2025-04-10 01:07:28 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Client Quit) |
2025-04-10 01:08:09 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst |
2025-04-10 01:08:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
2025-04-10 01:09:25 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 01:11:44 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
2025-04-10 01:14:30 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye) |
2025-04-10 01:14:59 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst |
2025-04-10 01:19:17 +0200 | Square | (~Square4@user/square) (Ping timeout: 248 seconds) |
2025-04-10 01:19:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 01:19:42 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
2025-04-10 01:21:44 +0200 | polykernel | (~polykerne@user/polykernel) (Ping timeout: 252 seconds) |
2025-04-10 01:23:46 +0200 | polykernel | (~polykerne@user/polykernel) polykernel |
2025-04-10 01:24:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-10 01:25:09 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
2025-04-10 01:28:02 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
2025-04-10 01:29:29 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
2025-04-10 01:31:04 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
2025-04-10 01:31:53 +0200 | Square2 | (~Square@user/square) Square |
2025-04-10 01:33:45 +0200 | sprotte24 | (~sprotte24@p200300d16f0bc1000c82a6b41033ea55.dip0.t-ipconnect.de) (Quit: Leaving) |
2025-04-10 01:35:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 01:35:49 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 248 seconds) |
2025-04-10 01:39:34 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
2025-04-10 01:39:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-10 01:48:53 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
2025-04-10 01:51:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 01:56:12 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 252 seconds) |
2025-04-10 01:56:49 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) |
2025-04-10 01:57:02 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
2025-04-10 01:57:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
2025-04-10 01:59:05 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Changing host) |
2025-04-10 01:59:05 +0200 | XZDX | (~xzdx@user/XZDX) XZDX |
2025-04-10 02:03:10 +0200 | jespada | (~jespada@r190-133-30-51.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
2025-04-10 02:08:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 02:11:52 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye) |
2025-04-10 02:12:13 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst |
2025-04-10 02:13:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-10 02:21:38 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Remote host closed the connection) |
2025-04-10 02:22:22 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) |
2025-04-10 02:23:55 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-04-10 02:23:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 02:25:18 +0200 | poscat0x04 | (~poscat@user/poscat) (Ping timeout: 276 seconds) |
2025-04-10 02:26:16 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
2025-04-10 02:28:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-10 02:31:02 +0200 | polyphem | (~rod@p4fc2cdf8.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
2025-04-10 02:31:05 +0200 | <EvanR> | Frege observed, as we did above, that in the study of functions it is sufficient to focus on unary functions (i.e., functions that take exactly one argument). |
2025-04-10 02:31:22 +0200 | <EvanR> | (The procedure of viewing a multiple-arity operation as a sequence of abstractions that yield an equivalent unary operation is called currying the operation. |
2025-04-10 02:31:29 +0200 | <EvanR> | Perhaps it would be more historically accurate to call the operation fregeing, but there are often miscarriages of justice in the appellation of mathematical ideas.) |
2025-04-10 02:31:45 +0200 | <EvanR> | lol |
2025-04-10 02:32:29 +0200 | <haskellbridge> | <Morj> There's a quote you can find that someone who invented the thing is less powerful than the one who named this thing |
2025-04-10 02:32:32 +0200 | <haskellbridge> | <Morj> I call it Morj's law |
2025-04-10 02:38:01 +0200 | poscat | (~poscat@user/poscat) poscat |
2025-04-10 02:39:25 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 02:39:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 02:45:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-04-10 02:45:35 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:19b2:995a:60d5:3b93) (Quit: Leaving) |
2025-04-10 02:53:09 +0200 | xff0x | (~xff0x@2405:6580:b080:900:b50:e5e9:27c3:86) (Ping timeout: 248 seconds) |
2025-04-10 02:55:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 02:55:49 +0200 | foul_owl | (~kerry@94.156.149.99) (Ping timeout: 248 seconds) |
2025-04-10 02:58:09 +0200 | otto_s | (~user@p4ff27c58.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
2025-04-10 03:00:05 +0200 | otto_s | (~user@p4ff278a2.dip0.t-ipconnect.de) |
2025-04-10 03:01:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-04-10 03:03:56 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de) |
2025-04-10 03:05:53 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
2025-04-10 03:06:42 +0200 | foul_owl | (~kerry@174-21-146-90.tukw.qwest.net) foul_owl |
2025-04-10 03:08:43 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
2025-04-10 03:13:42 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
2025-04-10 03:13:56 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
2025-04-10 03:21:07 +0200 | tavare | (~tavare@150.129.88.189) tavare |
2025-04-10 03:21:07 +0200 | tavare | (~tavare@150.129.88.189) (Changing host) |
2025-04-10 03:21:07 +0200 | tavare | (~tavare@user/tavare) tavare |
2025-04-10 03:25:05 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
2025-04-10 03:26:27 +0200 | foul_owl | (~kerry@174-21-146-90.tukw.qwest.net) (Ping timeout: 265 seconds) |
2025-04-10 03:27:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 03:28:54 +0200 | ezzieygu1wuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 246 seconds) |
2025-04-10 03:30:39 +0200 | aforemny_ | (~aforemny@i59F4C56B.versanet.de) (Ping timeout: 244 seconds) |
2025-04-10 03:31:24 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
2025-04-10 03:32:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 03:32:37 +0200 | <EvanR> | in the law: if x == y then f x == f y, (congruence), would you say "== preserves function application" or "function application preserves ==" and/or what is the congruence, == or function application |
2025-04-10 03:36:18 +0200 | Square | (~Square4@user/square) Square |
2025-04-10 03:37:13 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
2025-04-10 03:37:29 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-04-10 03:39:08 +0200 | Square2 | (~Square@user/square) (Ping timeout: 245 seconds) |
2025-04-10 03:40:19 +0200 | foul_owl | (~kerry@94.156.149.91) foul_owl |
2025-04-10 03:42:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 03:47:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 03:50:08 +0200 | aforemny | (~aforemny@i59F4C778.versanet.de) aforemny |
2025-04-10 03:50:13 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
2025-04-10 03:58:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 04:03:27 +0200 | <haskellbridge> | <Bowuigi> EvanR in HoTT the unit type is denoted as mathbb{1} and its inhabitant is denoted * (or with a star) |
2025-04-10 04:03:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-10 04:04:28 +0200 | <haskellbridge> | <Bowuigi> If you want something convention independent just ask for the limit/adjunction version of those constructs |
2025-04-10 04:05:18 +0200 | tessier | (~tessier@ip68-8-117-219.sd.sd.cox.net) (Ping timeout: 272 seconds) |
2025-04-10 04:05:30 +0200 | <EvanR> | yes I saw that in HoTT |
2025-04-10 04:06:26 +0200 | tessier | (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) tessier |
2025-04-10 04:06:47 +0200 | <haskellbridge> | <Bowuigi> Also the product type is only associative up to isomorphism, members of (AxB)xC and members of Ax(BxC) are not equal, just equivalent (except under univalence) |
2025-04-10 04:06:55 +0200 | <EvanR> | 𝟙 |
2025-04-10 04:08:13 +0200 | <haskellbridge> | <Bowuigi> Yes, the boolean type is mathbb{2} and in general any type with exactly N elements is denoted mathbb{N} |
2025-04-10 04:14:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 04:16:32 +0200 | slack1256 | (~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) slack1256 |
2025-04-10 04:16:48 +0200 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
2025-04-10 04:17:51 +0200 | <slack1256> | Has anyone used tsvector in persistent ? |
2025-04-10 04:17:58 +0200 | <slack1256> | How do you declare in as a datatype? |
2025-04-10 04:18:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 04:21:00 +0200 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) ryanbooker |
2025-04-10 04:24:54 +0200 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) (Ping timeout: 276 seconds) |
2025-04-10 04:26:49 +0200 | <monochrom> | EvanR: Interesting, I have always thought of it as == preserves function application, but the other round is just as valid. |
2025-04-10 04:26:54 +0200 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) TheCoffeMaker |
2025-04-10 04:29:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 04:29:57 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-04-10 04:31:13 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
2025-04-10 04:34:06 +0200 | stef204 | (~stef204@user/stef204) (Quit: WeeChat 4.2.1) |
2025-04-10 04:35:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-10 04:37:02 +0200 | slack1256 | (~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) (Remote host closed the connection) |
2025-04-10 04:45:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 04:46:14 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-10 04:47:39 +0200 | <EvanR> | I got that off stanford.edu on the topic of lambda calculus |
2025-04-10 04:48:03 +0200 | <EvanR> | where it describes eta conversion as "= preserving application and abstraction" |
2025-04-10 04:50:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-10 05:01:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 05:06:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 05:17:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 05:18:10 +0200 | tamer | (~tamer@user/tamer) (Read error: Connection reset by peer) |
2025-04-10 05:22:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-04-10 05:32:23 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 05:32:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 05:34:23 +0200 | <haskellbridge> | <Liamzee> curious, have people built a linear lens system for vector yet? IIRC, there was something about that on Bartosz Milewski's site |
2025-04-10 05:34:25 +0200 | <haskellbridge> | <Liamzee> https://bartoszmilewski.com/2024/02/07/linear-lenses-in-haskell/ |
2025-04-10 05:34:29 +0200 | tamer | (~tamer@5.2.74.82) |
2025-04-10 05:37:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-10 05:41:02 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-04-10 05:48:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 05:50:14 +0200 | zlqrvx_ | (~zlqrvx@101.175.150.247) |
2025-04-10 05:51:15 +0200 | zlqrvx | (~zlqrvx@101.175.150.247) (Read error: Connection reset by peer) |
2025-04-10 05:54:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-04-10 05:57:56 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 06:01:16 +0200 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-04-10 06:01:24 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2025-04-10 06:04:03 +0200 | whez | (uid470288@id-470288.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2025-04-10 06:04:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 06:09:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-10 06:09:14 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
2025-04-10 06:10:50 +0200 | <ski> | EvanR : "`f' preserves equality" (i'd say `=', unless you specifically mean decidable equality) (and it's not "function application" but "(function appliation of) `f'"). `(==)' would be the congruence relation (wrt `f') here |
2025-04-10 06:12:26 +0200 | michalz | (~michalz@185.246.207.201) |
2025-04-10 06:20:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 06:23:05 +0200 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2025-04-10 06:23:28 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-04-10 06:25:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-10 06:31:13 +0200 | sayurc | (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
2025-04-10 06:36:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 06:38:41 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-10 06:41:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
2025-04-10 06:43:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 06:49:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-04-10 06:58:47 +0200 | hattckory | (~hattckory@70.27.118.207) |
2025-04-10 06:59:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 07:03:54 +0200 | hattckory | (~hattckory@70.27.118.207) (Ping timeout: 260 seconds) |
2025-04-10 07:04:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-04-10 07:10:35 +0200 | Square2 | (~Square@user/square) Square |
2025-04-10 07:12:42 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 07:14:34 +0200 | Square | (~Square4@user/square) (Ping timeout: 260 seconds) |
2025-04-10 07:15:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 07:15:42 +0200 | sayurc | (~sayurc@169.150.203.34) sayurc |
2025-04-10 07:17:16 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Quit: Hi, this is Paul Allen. I'm being called away to London for a few days. Meredith, I'll call you when I get back. Hasta la vista, baby.) |
2025-04-10 07:19:15 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 07:19:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-10 07:20:47 +0200 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
2025-04-10 07:23:29 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-10 07:26:45 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
2025-04-10 07:30:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 07:33:48 +0200 | michalz | (~michalz@185.246.207.201) (Quit: ZNC 1.9.1 - https://znc.in) |
2025-04-10 07:34:06 +0200 | michalz | (~michalz@185.246.207.201) |
2025-04-10 07:36:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-10 07:37:11 +0200 | michalz | (~michalz@185.246.207.201) (Client Quit) |
2025-04-10 07:37:34 +0200 | michalz | (~michalz@185.246.207.221) |
2025-04-10 07:38:18 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
2025-04-10 07:46:08 +0200 | <haskellbridge> | <hellwolf> why did i not know this is a valid syntax |
2025-04-10 07:46:08 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/wUEaSQWmEwGlroXOCJYXuzhL/7ofVWvhpwhM (3 lines) |
2025-04-10 07:46:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 07:51:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-10 07:59:47 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 08:05:15 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
2025-04-10 08:05:28 +0200 | <Leary> | hellwolf: https://play.haskell.org/saved/bRThmTVI |
2025-04-10 08:05:56 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 08:07:08 +0200 | <haskellbridge> | <hellwolf> what about that? |
2025-04-10 08:07:31 +0200 | <Leary> | Also: https://play.haskell.org/saved/ObeWDdIa |
2025-04-10 08:07:58 +0200 | <Leary> | If you try to run these, you'll see they don't work, and the errors tell you where the syntax comes from and its limitations. |
2025-04-10 08:08:49 +0200 | Square2 | (~Square@user/square) (Ping timeout: 260 seconds) |
2025-04-10 08:11:15 +0200 | <haskellbridge> | <hellwolf> your first one can still work without any extension. but perhaps because it was enabled by default in ghc2021. |
2025-04-10 08:11:16 +0200 | <haskellbridge> | the second one is interesting |
2025-04-10 08:12:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 08:12:27 +0200 | <mauke> | fucking playground |
2025-04-10 08:12:37 +0200 | <mauke> | how do I get it top stop hijacking Ctrl-L? |
2025-04-10 08:13:53 +0200 | <haskellbridge> | <hellwolf> vibe code and send PR to tom :p |
2025-04-10 08:16:16 +0200 | <haskellbridge> | <hellwolf> But I honestly don't understand why the 2nd example doesn't work and what ghc is complaining about. Baffling syntax rule here, and I wonder why this syntax is even allowed if it doesn't work as expected at times. No intuition works here for me. |
2025-04-10 08:16:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 08:16:55 +0200 | foul_owl | (~kerry@94.156.149.91) (Ping timeout: 268 seconds) |
2025-04-10 08:17:35 +0200 | <mauke> | https://www.haskell.org/hugs/pages/users_guide/type-annotations.html |
2025-04-10 08:20:14 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-04-10 08:21:12 +0200 | <Leary> | hellwolf: It's part of STV; the /expectation/ is for it to successfully bind type variables for use in the body, as in: https://play.haskell.org/saved/OYapfbVm |
2025-04-10 08:22:18 +0200 | <haskellbridge> | <hellwolf> what is STV? |
2025-04-10 08:22:33 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0) |
2025-04-10 08:22:33 +0200 | jmcantrell_ | jmcantrell |
2025-04-10 08:22:49 +0200 | <Leary> | ScopedTypeVariables. It simply isn't intended to replace top-level type signatures. |
2025-04-10 08:23:22 +0200 | <haskellbridge> | <hellwolf> now it starts to make sense, it's a pattern matching. |
2025-04-10 08:23:22 +0200 | <haskellbridge> | So if I run it through the TH, it would show the right syntax constructor and makes sense. |
2025-04-10 08:24:04 +0200 | <haskellbridge> | <hellwolf> it was an illusion that it looked like a type declaration |
2025-04-10 08:24:13 +0200 | <haskellbridge> | <hellwolf> but it had nothing to do with it. |
2025-04-10 08:24:19 +0200 | <haskellbridge> | <hellwolf> i get it now. thanks for explaining. |
2025-04-10 08:27:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 08:28:51 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
2025-04-10 08:31:00 +0200 | foul_owl | (~kerry@94.156.149.97) foul_owl |
2025-04-10 08:32:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-10 08:37:57 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 246 seconds) |
2025-04-10 08:42:58 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 08:43:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 08:47:44 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-10 08:48:07 +0200 | ft | (~ft@p508db594.dip0.t-ipconnect.de) (Quit: leaving) |
2025-04-10 08:48:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-10 08:50:37 +0200 | tromp | (~textual@2001:1c00:3487:1b00:44ed:cdbe:8e8e:71c5) |
2025-04-10 08:51:52 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
2025-04-10 08:57:11 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 244 seconds) |
2025-04-10 08:57:16 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
2025-04-10 08:59:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 09:00:04 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
2025-04-10 09:01:03 +0200 | caconym | (~caconym@user/caconym) caconym |
2025-04-10 09:03:09 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 09:04:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-10 09:05:20 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
2025-04-10 09:08:33 +0200 | <[exa]> | Is there any good way how to debug assertion failure in C++ code that get somehow (no idea how) triggered from usual ghc compilation? |
2025-04-10 09:08:48 +0200 | <[exa]> | In particular I've got this thing here with accelerate-llvm: https://paste.tomsmeding.com/GbdNItS1 |
2025-04-10 09:09:02 +0200 | <[exa]> | somehow I can't even trace how ghc comes to executing the C source |
2025-04-10 09:15:06 +0200 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Ping timeout: 252 seconds) |
2025-04-10 09:15:44 +0200 | TMA | (tma@twin.jikos.cz) (Ping timeout: 260 seconds) |
2025-04-10 09:18:18 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds) |
2025-04-10 09:18:26 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
2025-04-10 09:19:12 +0200 | vpan | (~vpan@212.117.1.172) |
2025-04-10 09:19:50 +0200 | Lord_of_Life_ | Lord_of_Life |
2025-04-10 09:23:03 +0200 | <[exa]> | (nvm, opened an issue here if someone's interested in poking in that https://github.com/AccelerateHS/accelerate-llvm/issues/102 ) |
2025-04-10 09:23:53 +0200 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan |
2025-04-10 09:29:41 +0200 | chele | (~chele@user/chele) chele |
2025-04-10 09:35:37 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
2025-04-10 09:36:43 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) acidjnk |
2025-04-10 09:39:43 +0200 | XZDX | (~xzdx@user/XZDX) (Remote host closed the connection) |
2025-04-10 09:40:00 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) |
2025-04-10 09:41:08 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2025-04-10 09:45:38 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) lisbeths |
2025-04-10 09:49:38 +0200 | merijn | (~merijn@77.242.116.146) merijn |
2025-04-10 09:53:30 +0200 | fp | (~Thunderbi@2001:708:20:1406::1370) fp |
2025-04-10 09:53:45 +0200 | ski | . o O ( "Interview with Vibe Coder in 2025" <https://www.youtube.com/watch?v=JeNS1ZNHQs8> ) |
2025-04-10 09:57:30 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
2025-04-10 10:04:33 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-10 10:19:15 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 10:20:12 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Remote host closed the connection) |
2025-04-10 10:25:23 +0200 | forell | (~forell@user/forell) (Quit: ZNC - https://znc.in) |
2025-04-10 10:26:40 +0200 | forell | (~forell@user/forell) forell |
2025-04-10 10:37:58 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds) |
2025-04-10 10:45:12 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2025-04-10 10:48:21 +0200 | sprotte24 | (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) |
2025-04-10 10:48:53 +0200 | sprotte24 | (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) (Client Quit) |
2025-04-10 10:53:51 +0200 | sayurc | (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
2025-04-10 10:56:50 +0200 | alp | (~alp@2001:861:8ca0:4940:e00c:8d19:d96b:e8b0) |
2025-04-10 10:59:35 +0200 | poxel | (~lennart@user/poxel) poxel |
2025-04-10 11:02:20 +0200 | poxel | (~lennart@user/poxel) (Client Quit) |
2025-04-10 11:02:24 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
2025-04-10 11:02:39 +0200 | poxel | (~poxel@user/poxel) poxel |
2025-04-10 11:02:44 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
2025-04-10 11:08:04 +0200 | olivial | (~benjaminl@user/benjaminl) (Read error: Connection reset by peer) |
2025-04-10 11:08:20 +0200 | olivial | (~benjaminl@user/benjaminl) benjaminl |
2025-04-10 11:11:16 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
2025-04-10 11:17:09 +0200 | Guest71 | (~Guest75@37.204.222.118) |
2025-04-10 11:19:58 +0200 | poxel | (~poxel@user/poxel) (Quit: WeeChat 4.6.0) |
2025-04-10 11:20:18 +0200 | poxel | (~poxel@user/poxel) poxel |
2025-04-10 11:31:42 +0200 | Guest71 | (~Guest75@37.204.222.118) (Ping timeout: 240 seconds) |
2025-04-10 11:34:52 +0200 | fp | (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 268 seconds) |
2025-04-10 11:36:28 +0200 | <yin> | any news on the plan to make base versions independent from ghc versions? |
2025-04-10 11:39:57 +0200 | hsw | (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) (Ping timeout: 246 seconds) |
2025-04-10 11:45:32 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 11:46:30 +0200 | hsw | (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) hsw |
2025-04-10 11:46:36 +0200 | sprotte24 | (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) |
2025-04-10 11:56:46 +0200 | lambdap2371 | (~lambdap@static.167.190.119.168.clients.your-server.de) (Quit: Ping timeout (120 seconds)) |
2025-04-10 11:57:01 +0200 | lambdap2371 | (~lambdap@static.167.190.119.168.clients.your-server.de) |
2025-04-10 12:00:31 +0200 | <kqr> | I am calling a function that gives me back its own special Result type, and I'd like to do the equivalent of `fromMaybe` on it. Is there anything about e.g. I'm guessing the right place to start thinking would be its Foldable instance, right? ( |
2025-04-10 12:00:39 +0200 | <int-e> | yin: is that what ghc-internal is about? |
2025-04-10 12:03:55 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2025-04-10 12:04:38 +0200 | __monty__ | (~toonn@user/toonn) toonn |
2025-04-10 12:05:01 +0200 | <kqr> | Update on result type: indeed, foldr const defaultValue does what I need. |
2025-04-10 12:08:59 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 260 seconds) |
2025-04-10 12:12:43 +0200 | <yin> | int-e: not sure. i recall having that conversation here but details elude me |
2025-04-10 12:13:58 +0200 | <yin> | maybe something discussed here https://discourse.haskell.org/t/a-different-approach-to-emancipating-base/5695/6 |
2025-04-10 12:24:45 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds) |
2025-04-10 12:31:09 +0200 | poxel | (~poxel@user/poxel) (Quit: WeeChat 4.6.0) |
2025-04-10 12:31:29 +0200 | poxel | (~weechat@user/poxel) poxel |
2025-04-10 12:32:04 +0200 | poxel | (~weechat@user/poxel) (Client Quit) |
2025-04-10 12:32:23 +0200 | poxel | (~poxel@user/poxel) poxel |
2025-04-10 12:37:18 +0200 | <yin> | separating ghc.base from base |
2025-04-10 12:49:53 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-10 12:55:39 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
2025-04-10 12:56:36 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
2025-04-10 13:00:04 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
2025-04-10 13:00:27 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
2025-04-10 13:02:12 +0200 | caconym | (~caconym@user/caconym) caconym |
2025-04-10 13:02:14 +0200 | jespada | (~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) jespada |
2025-04-10 13:04:42 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 13:07:38 +0200 | TMA | (tma@twin.jikos.cz) TMA |
2025-04-10 13:08:12 +0200 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) |
2025-04-10 13:09:59 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
2025-04-10 13:11:59 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-10 13:15:31 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
2025-04-10 13:15:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 272 seconds) |
2025-04-10 13:23:40 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 13:25:13 +0200 | xff0x | (~xff0x@2405:6580:b080:900:1c0d:6c97:349e:6228) |
2025-04-10 13:30:09 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
2025-04-10 13:34:09 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
2025-04-10 13:34:51 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Remote host closed the connection) |
2025-04-10 13:35:33 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
2025-04-10 13:57:33 +0200 | walt | (~ggVGc@a.lowtech.earth) (Ping timeout: 276 seconds) |
2025-04-10 13:57:55 +0200 | walt | (~ggVGc@a.lowtech.earth) |
2025-04-10 14:03:34 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 14:09:52 +0200 | bcksl | (~bcksl@user/bcksl) (Quit: \) |
2025-04-10 14:09:52 +0200 | end | (~end@user/end/x-0094621) (Quit: end) |
2025-04-10 14:13:58 +0200 | jespada | (~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) (Ping timeout: 268 seconds) |
2025-04-10 14:14:33 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) acidjnk |
2025-04-10 14:16:29 +0200 | jespada | (~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) jespada |
2025-04-10 14:20:23 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
2025-04-10 14:20:43 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
2025-04-10 14:41:18 +0200 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Ping timeout: 240 seconds) |
2025-04-10 14:43:44 +0200 | zlqrvx_ | (~zlqrvx@101.175.150.247) (Ping timeout: 260 seconds) |
2025-04-10 14:44:39 +0200 | bcksl | (~bcksl@user/bcksl) bcksl |
2025-04-10 14:45:13 +0200 | zlqrvx | (~zlqrvx@2001:8003:8c8b:e00:374a:bdcb:457c:d1e3) |
2025-04-10 14:49:13 +0200 | end | (~end@user/end/x-0094621) end^ |
2025-04-10 14:53:12 +0200 | vpan | (~vpan@212.117.1.172) (Quit: Leaving.) |
2025-04-10 15:00:36 +0200 | cstml | (~Thunderbi@user/cstml) cstml |
2025-04-10 15:01:39 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds) |
2025-04-10 15:05:09 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
2025-04-10 15:07:30 +0200 | <hellwolf> | is there a Nat/SNat case analysis utility, such that you can split into cases which carries a Dict for each case handling function? |
2025-04-10 15:07:47 +0200 | <hellwolf> | E.g. split it into Dict @(n == 0) and Dict @(1 <= n) |
2025-04-10 15:08:14 +0200 | <hellwolf> | I could write myself, use unsafeAxiom, but I am wondering if this is common enough of a utility to appear somewhere. |
2025-04-10 15:11:19 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
2025-04-10 15:14:04 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
2025-04-10 15:15:22 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-04-10 15:19:43 +0200 | <merijn> | yin: It hasn't happened in the past decade, so I wouldn't hold my breath ;) |
2025-04-10 15:20:12 +0200 | <merijn> | int-e: I think yin is mostly referring to make base installable |
2025-04-10 15:20:29 +0200 | <merijn> | So you could, for example, install a newer base on an older GHC and vice versa |
2025-04-10 15:21:20 +0200 | <int-e> | Yeah I got the question. |
2025-04-10 15:21:51 +0200 | fp | (~Thunderbi@2001:708:150:10::1d80) fp |
2025-04-10 15:22:38 +0200 | <int-e> | I just stumbled across ghc-internal recently and wondered whether splitting that off might be related. I didn't check any links or timeline. |
2025-04-10 15:30:24 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:3895:739f:4247:f37f) |
2025-04-10 15:30:39 +0200 | sprotte24_ | (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) |
2025-04-10 15:31:03 +0200 | fp | (~Thunderbi@2001:708:150:10::1d80) (Ping timeout: 268 seconds) |
2025-04-10 15:32:13 +0200 | shreyasminocha_ | (51fdc93eda@user/shreyasminocha) shreyasminocha |
2025-04-10 15:32:15 +0200 | ggb_ | (a62ffbaf4f@2a03:6000:1812:100::3ac) |
2025-04-10 15:32:15 +0200 | smiesner_ | (b0cf5acf8c@2a03:6000:1812:100::13b9) |
2025-04-10 15:32:15 +0200 | sm2n_ | (ae95cb1267@user/sm2n) sm2n |
2025-04-10 15:32:15 +0200 | raghavgururajan_ | (ea769b8000@user/raghavgururajan) raghavgururajan |
2025-04-10 15:32:16 +0200 | simendsjo_ | (34b0550437@2a03:6000:1812:100::1441) simendsjo |
2025-04-10 15:32:16 +0200 | arcadewise_ | (52968ed80d@2a03:6000:1812:100::3df) l3gacyb3ta |
2025-04-10 15:32:16 +0200 | probie_ | (cc0b34050a@user/probie) probie |
2025-04-10 15:32:16 +0200 | ymherklotz_ | (cb2c9cfbdd@2a03:6000:1812:100::29a) ymherklotz |
2025-04-10 15:32:16 +0200 | ursa-major_ | (114efe6c39@2a03:6000:1812:100::11f3) ursa-major |
2025-04-10 15:32:17 +0200 | duncan__ | (c6181279e3@user/meow/duncan) duncan |
2025-04-10 15:32:18 +0200 | op_4_ | (~tslil@2a01:4f8:c0c:7952::1) |
2025-04-10 15:32:18 +0200 | samhh__ | (7569f027cf@2a03:6000:1812:100::e4) samhh |
2025-04-10 15:32:19 +0200 | sefidel_ | (~sefidel@user/sefidel) sefidel |
2025-04-10 15:32:19 +0200 | j0lol_ | (~j0lol@132.145.17.236) j0lol |
2025-04-10 15:32:19 +0200 | saolsen_ | (sid26430@id-26430.lymington.irccloud.com) saolsen |
2025-04-10 15:32:44 +0200 | hamishmack_ | (sid389057@id-389057.hampstead.irccloud.com) hamishmack |
2025-04-10 15:32:51 +0200 | bgamari_ | (~bgamari@64.223.225.174) |
2025-04-10 15:32:54 +0200 | cptaffe` | (~cptaffe@user/cptaffe) cptaffe |
2025-04-10 15:33:02 +0200 | vgtw_ | (~vgtw@user/vgtw) vgtw |
2025-04-10 15:33:59 +0200 | cstml | (~Thunderbi@user/cstml) (Quit: cstml) |
2025-04-10 15:35:17 +0200 | milan2 | (~milan@88.212.61.169) |
2025-04-10 15:35:29 +0200 | inedia_ | (~irc@2600:3c00:e000:287::1) |
2025-04-10 15:35:34 +0200 | kst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst |
2025-04-10 15:35:41 +0200 | mima_ | (~mmh@user/mima) mima |
2025-04-10 15:35:46 +0200 | _[_________]_ | (~oos95GWG@user/oos95GWG) oos95GWG |
2025-04-10 15:36:22 +0200 | abrar_ | (~abrar@static-96-245-187-163.phlapa.fios.verizon.net) |
2025-04-10 15:36:31 +0200 | aforemny_ | (~aforemny@2001:9e8:6cd3:ed00:7f35:da5a:93ab:c3e3) aforemny |
2025-04-10 15:37:02 +0200 | mal1 | (~mal@ns2.wyrd.be) lieven |
2025-04-10 15:37:14 +0200 | darrik | (~natch@c-92-34-7-158.bbcust.telenor.se) |
2025-04-10 15:37:28 +0200 | ystael | (~ystael@user/ystael) ystael |
2025-04-10 15:40:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (*.net *.split) |
2025-04-10 15:40:08 +0200 | TMA | (tma@twin.jikos.cz) (*.net *.split) |
2025-04-10 15:40:08 +0200 | sprotte24 | (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) (*.net *.split) |
2025-04-10 15:40:09 +0200 | aforemny | (~aforemny@i59F4C778.versanet.de) (*.net *.split) |
2025-04-10 15:40:09 +0200 | krjst | (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (*.net *.split) |
2025-04-10 15:40:09 +0200 | Natch | (~natch@c-92-34-7-158.bbcust.telenor.se) (*.net *.split) |
2025-04-10 15:40:09 +0200 | cptaffe | (~cptaffe@user/cptaffe) (*.net *.split) |
2025-04-10 15:40:09 +0200 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-15-174-95-4-83.dsl.bell.ca) (*.net *.split) |
2025-04-10 15:40:09 +0200 | milan | (~milan@88.212.61.169) (*.net *.split) |
2025-04-10 15:40:09 +0200 | op_4 | (~tslil@user/op-4/x-9116473) (*.net *.split) |
2025-04-10 15:40:09 +0200 | [_________] | (~oos95GWG@user/oos95GWG) (*.net *.split) |
2025-04-10 15:40:09 +0200 | samhh_ | (7569f027cf@2a03:6000:1812:100::e4) (*.net *.split) |
2025-04-10 15:40:09 +0200 | raghavgururajan | (ea769b8000@user/raghavgururajan) (*.net *.split) |
2025-04-10 15:40:10 +0200 | duncan | (c6181279e3@user/meow/duncan) (*.net *.split) |
2025-04-10 15:40:10 +0200 | ursa-major | (114efe6c39@2a03:6000:1812:100::11f3) (*.net *.split) |
2025-04-10 15:40:10 +0200 | sm2n | (ae95cb1267@user/sm2n) (*.net *.split) |
2025-04-10 15:40:10 +0200 | probie | (cc0b34050a@user/probie) (*.net *.split) |
2025-04-10 15:40:10 +0200 | shreyasminocha | (51fdc93eda@user/shreyasminocha) (*.net *.split) |
2025-04-10 15:40:11 +0200 | simendsjo | (34b0550437@2a03:6000:1812:100::1441) (*.net *.split) |
2025-04-10 15:40:11 +0200 | arcadewise | (52968ed80d@2a03:6000:1812:100::3df) (*.net *.split) |
2025-04-10 15:40:11 +0200 | exfalsoquodlibet | (a7085e0f71@2a03:6000:1812:100::13a3) (*.net *.split) |
2025-04-10 15:40:11 +0200 | ymherklotz | (cb2c9cfbdd@2a03:6000:1812:100::29a) (*.net *.split) |
2025-04-10 15:40:11 +0200 | smiesner | (b0cf5acf8c@user/smiesner) (*.net *.split) |
2025-04-10 15:40:11 +0200 | ggb | (a62ffbaf4f@2a03:6000:1812:100::3ac) (*.net *.split) |
2025-04-10 15:40:11 +0200 | abrar | (~abrar@static-96-245-187-163.phlapa.fios.verizon.net) (*.net *.split) |
2025-04-10 15:40:11 +0200 | vgtw | (~vgtw@user/vgtw) (*.net *.split) |
2025-04-10 15:40:11 +0200 | j0lol | (~j0lol@132.145.17.236) (*.net *.split) |
2025-04-10 15:40:12 +0200 | acidsys | (~crameleon@openSUSE/member/crameleon) (*.net *.split) |
2025-04-10 15:40:12 +0200 | saolsen | (sid26430@id-26430.lymington.irccloud.com) (*.net *.split) |
2025-04-10 15:40:12 +0200 | hammond | (proscan@gateway04.insomnia247.nl) (*.net *.split) |
2025-04-10 15:40:12 +0200 | bgamari | (~bgamari@64.223.225.174) (*.net *.split) |
2025-04-10 15:40:12 +0200 | inedia | (~irc@2600:3c00:e000:287::1) (*.net *.split) |
2025-04-10 15:40:12 +0200 | sefidel | (~sefidel@user/sefidel) (*.net *.split) |
2025-04-10 15:40:12 +0200 | _koolazer | (~koo@user/koolazer) (*.net *.split) |
2025-04-10 15:40:13 +0200 | bastelfreak | (bastelfrea@libera/staff/VoxPupuli.bastelfreak) (*.net *.split) |
2025-04-10 15:40:13 +0200 | lieven | (~mal@ns2.wyrd.be) (*.net *.split) |
2025-04-10 15:40:13 +0200 | mima | (~mmh@user/mima) (*.net *.split) |
2025-04-10 15:40:13 +0200 | hamishmack | (sid389057@id-389057.hampstead.irccloud.com) (*.net *.split) |
2025-04-10 15:40:13 +0200 | duncan__ | duncan |
2025-04-10 15:40:13 +0200 | ggb_ | ggb |
2025-04-10 15:40:13 +0200 | hamishmack_ | hamishmack |
2025-04-10 15:40:13 +0200 | shreyasminocha_ | shreyasminocha |
2025-04-10 15:40:13 +0200 | darrik | Natch |
2025-04-10 15:40:13 +0200 | cptaffe` | cptaffe |
2025-04-10 15:40:14 +0200 | smiesner_ | smiesner |
2025-04-10 15:40:14 +0200 | ymherklotz_ | ymherklotz |
2025-04-10 15:40:14 +0200 | arcadewise_ | arcadewise |
2025-04-10 15:40:14 +0200 | simendsjo_ | simendsjo |
2025-04-10 15:40:14 +0200 | probie_ | probie |
2025-04-10 15:40:14 +0200 | saolsen_ | saolsen |
2025-04-10 15:40:14 +0200 | op_4_ | op_4 |
2025-04-10 15:40:14 +0200 | sefidel_ | sefidel |
2025-04-10 15:40:14 +0200 | raghavgururajan_ | raghavgururajan |
2025-04-10 15:40:14 +0200 | sm2n_ | sm2n |
2025-04-10 15:40:14 +0200 | ursa-major_ | ursa-major |
2025-04-10 15:40:15 +0200 | j0lol_ | j0lol |
2025-04-10 15:40:37 +0200 | lortabac | (~lortabac@88-125-6-227.subs.proxad.net) lortabac |
2025-04-10 15:42:55 +0200 | tavare | (~tavare@user/tavare) tavare |
2025-04-10 15:42:58 +0200 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
2025-04-10 15:43:54 +0200 | TMA | (tma@twin.jikos.cz) TMA |
2025-04-10 15:45:51 +0200 | koolazer | (~koo@user/koolazer) koolazer |
2025-04-10 15:46:26 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 15:46:38 +0200 | bastelfreak | (bastelfrea@libera/staff/VoxPupuli.bastelfreak) bastelfreak |
2025-04-10 15:47:02 +0200 | acidsys | (~crameleon@openSUSE/member/crameleon) crameleon |
2025-04-10 15:47:53 +0200 | exfalsoquodlibet | (a7085e0f71@2a03:6000:1812:100::13a3) |
2025-04-10 15:51:14 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-10 15:54:56 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2025-04-10 16:11:50 +0200 | _[_________]_ | (~oos95GWG@user/oos95GWG) (Quit: _[_________]_) |
2025-04-10 16:11:58 +0200 | [_________] | (~oos95GWG@user/oos95GWG) oos95GWG |
2025-04-10 16:16:34 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-04-10 16:25:17 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
2025-04-10 16:27:33 +0200 | Square | (~Square4@user/square) Square |
2025-04-10 16:33:43 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
2025-04-10 16:34:13 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
2025-04-10 16:34:45 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
2025-04-10 16:38:25 +0200 | hattckory | (~hattckory@70.27.118.207) |
2025-04-10 16:43:09 +0200 | hattckory | (~hattckory@70.27.118.207) (Ping timeout: 260 seconds) |
2025-04-10 16:44:44 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:3895:739f:4247:f37f) (Read error: Connection reset by peer) |
2025-04-10 16:48:08 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
2025-04-10 16:48:38 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:a504:86ce:5139:ec16) |
2025-04-10 16:49:18 +0200 | milan2 | (~milan@88.212.61.169) (Quit: WeeChat 4.4.3) |
2025-04-10 16:50:05 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 16:50:56 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
2025-04-10 16:52:47 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-04-10 16:56:09 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
2025-04-10 17:02:15 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
2025-04-10 17:07:36 +0200 | lortabac | (~lortabac@88-125-6-227.subs.proxad.net) (Quit: WeeChat 4.5.2) |
2025-04-10 17:11:21 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
2025-04-10 17:13:51 +0200 | ColinRobinson | (~juan@user/JuanDaugherty) JuanDaugherty |
2025-04-10 17:20:12 +0200 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
2025-04-10 17:20:49 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
2025-04-10 17:30:03 +0200 | hammond | (proscan@gateway04.insomnia247.nl) |
2025-04-10 17:34:08 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 17:46:29 +0200 | ColinRobinson | JuanDaugherty |
2025-04-10 17:47:35 +0200 | <hellwolf> | answering my own question: https://play.haskell.org/saved/tVbw1IsX did a case_non_zero_nat as exercise |
2025-04-10 17:53:56 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
2025-04-10 17:54:25 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
2025-04-10 17:55:24 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
2025-04-10 17:55:54 +0200 | amadaluzia_ | (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) |
2025-04-10 17:57:15 +0200 | JuanDaugherty | ColinRobinson |
2025-04-10 18:00:31 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
2025-04-10 18:01:01 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-04-10 18:05:37 +0200 | ColinRobinson | JuanDaugherty |
2025-04-10 18:08:35 +0200 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 252 seconds) |
2025-04-10 18:09:30 +0200 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) GdeVolpiano |
2025-04-10 18:23:32 +0200 | JuanDaugherty | ColinRobinson |
2025-04-10 18:26:20 +0200 | ft | (~ft@p508db594.dip0.t-ipconnect.de) ft |
2025-04-10 18:36:16 +0200 | sayurc | (~sayurc@169.150.203.34) sayurc |
2025-04-10 18:38:02 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) acidjnk |
2025-04-10 18:38:57 +0200 | <EvanR> | ski, this law (whatever symbol is used for the equality) goes for all f, not some f |
2025-04-10 18:39:07 +0200 | <EvanR> | forall x y and f |
2025-04-10 18:40:44 +0200 | <EvanR> | which is followed in set theory for =, or hypothetically === in elixir (== fails in elixir to follow the law) |
2025-04-10 18:42:37 +0200 | <EvanR> | seems to be a law in agda for = |
2025-04-10 18:42:48 +0200 | <EvanR> | whence the cong tool |
2025-04-10 18:49:32 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
2025-04-10 18:51:11 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
2025-04-10 18:52:49 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
2025-04-10 18:54:45 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 248 seconds) |
2025-04-10 18:57:08 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
2025-04-10 18:57:27 +0200 | Square2 | (~Square@user/square) Square |
2025-04-10 19:01:30 +0200 | Square | (~Square4@user/square) (Ping timeout: 252 seconds) |
2025-04-10 19:01:30 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
2025-04-10 19:01:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 19:03:28 +0200 | <ski> | EvanR : doesn't matter. then it's "`f' preserves equality, for all `f'". to be "function application preserves equality", it would have to say that if `f == g' and `a == b', then `f(a) == g(b)' |
2025-04-10 19:04:26 +0200 | <ski> | (that (latter) rule itself is often simply called "congruence", btw, taking it for granted that we're talking about function application) |
2025-04-10 19:05:04 +0200 | <EvanR> | alright congruence is basically talking about both things together |
2025-04-10 19:05:37 +0200 | <ski> | if you want to spell it out, "`==' is a congruence relation wrt function application" |
2025-04-10 19:06:05 +0200 | <EvanR> | on what preserves what, I see this article with an extension to equality of lambda calculus terms called the ξ rule |
2025-04-10 19:07:28 +0200 | <EvanR> | if M = N then \x.M = \x.N |
2025-04-10 19:07:33 +0200 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
2025-04-10 19:07:42 +0200 | <ski> | yea, that's also congruence |
2025-04-10 19:07:43 +0200 | <EvanR> | and it remarks "it means = preserves abstract" |
2025-04-10 19:07:49 +0200 | <ski> | (in this case of lambda abstraction) |
2025-04-10 19:07:54 +0200 | <EvanR> | abstraction |
2025-04-10 19:09:01 +0200 | pavonia | (~user@user/siracusa) siracusa |
2025-04-10 19:09:16 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
2025-04-10 19:11:25 +0200 | <EvanR> | it's actually three rules... if M=N then AM = AN, if M=N then MA = NA, if M=N then \x.M = \x.N (no mention of whether x may or must not appear free) and the remark is "it (=) preserves application and abstraction" |
2025-04-10 19:11:51 +0200 | kimiamania9 | (~65804703@user/kimiamania) kimiamania |
2025-04-10 19:12:44 +0200 | <EvanR> | maybe they're all mutually preserving each other |
2025-04-10 19:13:04 +0200 | kimiamania | (~65804703@user/kimiamania) (Read error: Connection reset by peer) |
2025-04-10 19:13:04 +0200 | kimiamania9 | kimiamania |
2025-04-10 19:13:33 +0200 | <ski> | a function `f : A -> A' is said to preserve a property `P' on `A', whenever `P(x)' implies `P(f(x))', for all `x' in `A'. `f' is said to reflect the property `P' whenever `P(f(x))' implies `P(x)', for all `x' in `A' |
2025-04-10 19:16:09 +0200 | <ski> | if you take `A' to be lambda expressions, and `f' the operation of "lambda-abstracting over the variable `x'", and generalize `P' from a unary relation on `A' to a binary one, specifically the `=' one, then you get "if M = N then \x.M = \x.N" above, from "`f' preserves `P'" |
2025-04-10 19:16:59 +0200 | <EvanR> | well that makes the remark backwards |
2025-04-10 19:17:03 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
2025-04-10 19:17:28 +0200 | <ski> | "no mention of whether x may or must not appear free" -- it may |
2025-04-10 19:18:12 +0200 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
2025-04-10 19:19:21 +0200 | <ski> | but yea, i guess people often are a bit loose with which is the "preserver" and which is the "preservee" |
2025-04-10 19:20:03 +0200 | <ski> | (reminds me i've seen people phrase `f(3)' as "`3' is being applied to the function `f'" ..) |
2025-04-10 19:20:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 19:20:39 +0200 | <EvanR> | that's like 3[array] = *(3 + array) |
2025-04-10 19:20:46 +0200 | <ski> | ayup |
2025-04-10 19:21:40 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 19:21:44 +0200 | ski | . o O ( <https://ncatlab.org/nlab/show/reflected+limit> (example of "reflect" in the above sense, although in a highly abstract context) ) |
2025-04-10 19:27:07 +0200 | <ski> | .. btw, in congruence/modular arithmetic, the congruence relation (the ".. = .. (mod m)" thing) is a congruence wrt the ring operations (being zero, one, addition, negation, multiplication) |
2025-04-10 19:28:29 +0200 | YoungFrog | (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) youngfrog |
2025-04-10 19:29:38 +0200 | <EvanR> | if a = b (mod m) then -a = -b (mod m) |
2025-04-10 19:29:47 +0200 | <ski> | yep (for negation) |
2025-04-10 19:30:24 +0200 | <EvanR> | what about in geometry, congruent triangles |
2025-04-10 19:30:50 +0200 | <EvanR> | is that another topic or an instance of congruence above |
2025-04-10 19:30:55 +0200 | sayurc | (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
2025-04-10 19:32:01 +0200 | <ski> | the operations are translations, rotations, reflections, and all possible compositions of those |
2025-04-10 19:32:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 19:32:23 +0200 | <ski> | if we also allow scalings, then the congruence relation is called "similarity", rather than "congruent" |
2025-04-10 19:32:37 +0200 | <EvanR> | ehm |
2025-04-10 19:33:04 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f7444aa95b6f7c7abd1.dip0.t-ipconnect.de) acidjnk |
2025-04-10 19:33:13 +0200 | <ski> | "In geometry, two figures or objects are congruent if they have the same shape and size, or if one has the same shape and size as the mirror image of the other." <https://en.wikipedia.org/wiki/Congruence_(geometry)> |
2025-04-10 19:33:31 +0200 | <EvanR> | if ABC is congruent to DEF then T ABC is congruent to T DEF (T is a translation) |
2025-04-10 19:33:58 +0200 | <EvanR> | a law satisfied by the relation |
2025-04-10 19:34:12 +0200 | <EvanR> | though it doesn't explain what "is congruent" means |
2025-04-10 19:34:16 +0200 | <ski> | yea. instead of "figures" we can say "generalized points", or "open expressions" |
2025-04-10 19:35:16 +0200 | <ski> | a circle is (e.g.) given by an expression whose type is "point", and which has a free variable which expresses the angle parameter |
2025-04-10 19:36:15 +0200 | <ski> | but for these operations, we don't need to consider the whole figure, we can consider each possible point value of it, for each possible value of the parameters / free variables, one at a time |
2025-04-10 19:36:40 +0200 | <ski> | (we translate a collection of points by translating each point in the collection, separately) |
2025-04-10 19:36:42 +0200 | <EvanR> | ... set of points ... |
2025-04-10 19:37:07 +0200 | <ski> | well. "indexed family" would be more accurate than "set" here, really |
2025-04-10 19:39:01 +0200 | <ski> | you can have `t : Real |- (0,0,0) : Real^3', the "line that doesn't move" (dimension one). this is distinct from `|- (0,0,0) : Real^3' (a closed expression, no free variables) (dimension zero) |
2025-04-10 19:39:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
2025-04-10 19:39:30 +0200 | <ski> | the former is "non-injective", is "singular" (in matrix algebra terminology). the latter isn't |
2025-04-10 19:39:35 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
2025-04-10 19:39:52 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
2025-04-10 19:40:23 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
2025-04-10 19:40:35 +0200 | <ski> | even though both of those, extensionally, determine the same set of points |
2025-04-10 19:41:09 +0200 | <EvanR> | that looks more like vector math, linear algebra |
2025-04-10 19:41:36 +0200 | <ski> | (can you have a triangle with all side lengths zero ? if you consider a triangle to be a set of points, it doesn't seem to make much sense. if you consider it as an index family, a function for a parameterizing set, then it does) |
2025-04-10 19:42:03 +0200 | <EvanR> | ok good, "set of points" has more problems than I thought xD |
2025-04-10 19:42:04 +0200 | <ski> | (s/for a/from a/) |
2025-04-10 19:42:07 +0200 | sayurc | (~sayurc@169.150.203.34) sayurc |
2025-04-10 19:43:20 +0200 | <EvanR> | I think it would be tricky to construct a triangle with side lengths zero since the sides would be defined using two points that are distinct |
2025-04-10 19:43:53 +0200 | <ski> | heron's formula for area works fine |
2025-04-10 19:44:13 +0200 | <ski> | figuring out angles .. doesn't work out |
2025-04-10 19:44:22 +0200 | <EvanR> | not a very good triangle |
2025-04-10 19:44:55 +0200 | <ski> | or, if you want to, you could say that you should specify the angles, separately, that would work |
2025-04-10 19:45:19 +0200 | <ski> | two angles being zero, the third being half a turn, e.g. |
2025-04-10 19:45:43 +0200 | <ski> | (or some other configuration, that makes the angles sum up to a half turn) |
2025-04-10 19:46:00 +0200 | <EvanR> | you could specify it and then confirming that those angles are correct would be impossible according to definition of angle given by birkhoff and beatley , which I've been reading |
2025-04-10 19:46:07 +0200 | <ski> | you can already consider a triangle with non-zero side lengths, but two angles being zero, so .. |
2025-04-10 19:46:29 +0200 | <EvanR> | that would work |
2025-04-10 19:48:48 +0200 | <EvanR> | alright, I'm wrong, you could confirm those angles are right, though the directions of the sides would not be defined |
2025-04-10 19:49:09 +0200 | <EvanR> | you couldn't extend the sides into a half line or full line |
2025-04-10 19:49:39 +0200 | <EvanR> | which could be fixed by also specifying that (in which case you didn't have to specify the angles) |
2025-04-10 19:50:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 19:50:34 +0200 | <ski> | situation seems a bit similar to specifying a complex number by magnitude (absolute value), and argument (angle) .. if magnitude is zero, then argument is ambiguous/arbitrary/non-well-defined |
2025-04-10 19:51:22 +0200 | <ski> | would you prefer to have different "complex zeros", one for each possible direction ? (kinda like floating-point numbers have both positive and negative zero ..), or just one of them ? |
2025-04-10 19:51:48 +0200 | <EvanR> | the "reciprocal" of complex infinities |
2025-04-10 19:52:01 +0200 | <ski> | mm |
2025-04-10 19:52:25 +0200 | <EvanR> | but a single direction might not be enough, or so I recall from 3D calculus |
2025-04-10 19:52:41 +0200 | <EvanR> | approaching weird functions along different curves gets different results |
2025-04-10 19:52:46 +0200 | <ski> | this kinda points towards projective space |
2025-04-10 19:52:55 +0200 | Flow | (~none@gentoo/developer/flow) flow |
2025-04-10 19:53:00 +0200 | <EvanR> | approaching zero of weird functions |
2025-04-10 19:53:27 +0200 | <ski> | yep, you can have a curve which doesn't have an asymptote line, as it approachex complex infinity |
2025-04-10 19:55:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
2025-04-10 19:55:15 +0200 | <ski> | mm, you're thinking of existence of all partial derivatives doesn't imply differentiability |
2025-04-10 19:56:04 +0200 | <EvanR> | the details are foggy but since then I chalked it up to caring about bad functions xD |
2025-04-10 19:57:10 +0200 | <EvanR> | I also have real analysis a constructive approach through interval arithmetic |
2025-04-10 19:57:47 +0200 | <ski> | might want to take a peek at say first chapter of Anders Kock's book, too |
2025-04-10 19:59:08 +0200 | <EvanR> | synthetic differential geometry |
2025-04-10 19:59:14 +0200 | ski | . o O ( "Synthetic Differential Geometry" (2nd ed.) by Anders Kock in 2006-03 at <https://users-math.au.dk/kock/sdg99.pdf> ) |
2025-04-10 19:59:17 +0200 | <ski> | yep |
2025-04-10 19:59:48 +0200 | <EvanR> | analytic vs synthetic |
2025-04-10 19:59:53 +0200 | <ski> | there's also the classic Errett Bishop book of Constructive Analysis |
2025-04-10 20:00:07 +0200 | <ski> | (with Douglas Bridges, in later edition) |
2025-04-10 20:00:33 +0200 | <EvanR> | the pdf on SDG on read really was cool |
2025-04-10 20:00:37 +0200 | <EvanR> | I read* |
2025-04-10 20:00:56 +0200 | <EvanR> | it seemed to really apply when trying to do geometry for computer games |
2025-04-10 20:01:16 +0200 | <EvanR> | by thinking about edge cases in terms of what some highly zoomed in version of the geometry would be |
2025-04-10 20:01:22 +0200 | <ski> | Kock proceeds by postulating an axiom, which would be inconsistent, if we used classical logic, but which is fine, using constructive logic |
2025-04-10 20:01:52 +0200 | <ski> | basically that the subset of all reals whose square is zero, has dimension one, rather than zero |
2025-04-10 20:02:23 +0200 | <EvanR> | a circle intersects a tangent line in not necessarily one point |
2025-04-10 20:02:30 +0200 | <ski> | it's an "infinitesimal line segment". long enough that we can talk about slopes, but not long enough that we can talk about it bending (stuff having non-zero second derivatives) |
2025-04-10 20:02:34 +0200 | <ski> | yep |
2025-04-10 20:04:56 +0200 | <EvanR> | I speculate that that setting would be good for having zero size triangles but with all the proper data in tact |
2025-04-10 20:05:17 +0200 | <ski> | if `f : |D -> |R' is a function from `|D = { x : |R | x^2 = 0 }' to reals, then `f' is determined by two real numbers, `f(0)' (the "abscissa-intercept"), and `D(f)(0)' (the first derivative, giving the slope) |
2025-04-10 20:05:45 +0200 | <ski> | hm, could be interesting to investigate |
2025-04-10 20:05:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 20:06:44 +0200 | <ski> | and we get a "infinitesimal cancellation" law. if `d * a = d * b', for *all* `d' in `|D', then `a = b' |
2025-04-10 20:10:37 +0200 | <ski> | this allows us to e.g. compute, using `f(x) = x^2', we get `f(x + d) - f(x) = (x + d)^2 - x^2 = x^2 + 2*d*x + d^2 - x^2 = 2*d*x + d^2 = 2*d*x' (using that square of `d' is zero in last step) |
2025-04-10 20:10:44 +0200 | <ski> | and so, if we want `D(f)(x) * ((x + d) - x) = D(f)(x) * d = f(x + d) - f(x)' (suggestive of `D(f)(x) = (f(x + d) - f(x)) / ((x + d) - x)'), then this means `D(f)(x) * d = 2*d*x', and therefore `D(f)(x) = 2*x' |
2025-04-10 20:11:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-04-10 20:11:39 +0200 | <ski> | so you calculate with infinitesimals as "quantities so small that their square is zero", like physicists have done, all along |
2025-04-10 20:13:23 +0200 | <EvanR> | I thought physicists discard quantities that are too infinite xD |
2025-04-10 20:13:51 +0200 | <ski> | heh, i guess occasionally, too :b |
2025-04-10 20:15:52 +0200 | fantom | (~fantom@2.219.56.221) |
2025-04-10 20:16:21 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
2025-04-10 20:16:42 +0200 | ski | . o O ( "Intuitionistic mathematics for physics" by Andrej Bauer in 2008-08-13 at <https://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/> ) |
2025-04-10 20:16:49 +0200 | ski | . o O ( "How can one do calculus with (nilpotent) infinitesimals): An Introduction to Smooth Infinitesimal Analysis" by MKOConnor in 2008-08-11 at <https://xorshammer.com/2008/08/11/smooth-infinitesimal-analysis/> ) |
2025-04-10 20:16:54 +0200 | ski | . o O ( "Multivariate Calculus with Nilpotent Infinitesimals: More Smooth Infinitesimal Analysis" by MKOConnor in 2008-08-16 at <https://xorshammer.com/2008/08/16/smooth-infinitesimal-analysis2/> ) |
2025-04-10 20:18:35 +0200 | <EvanR> | nlab draws a contrast between analysis and "synthesis", now we have SDG and smooth infinitesimal analysis, which are talking about the same thing? |
2025-04-10 20:19:54 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
2025-04-10 20:20:02 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
2025-04-10 20:20:07 +0200 | <ski> | "synthetic" here refers to introducing the basic properties we want to consider, by axioms. as opposed to "analysis" referring to defining/implementing/constructing structures, with the properties we'd like, out of "simpler material" |
2025-04-10 20:21:29 +0200 | <EvanR> | in analysis, nlab goes back to the roots of the word which is greek for unraveling, which, is the literal name of a proof exercise in this interval analysis based real analysis book |
2025-04-10 20:21:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 20:21:46 +0200 | <ski> | however, "analysis" on its own tends to stand for systems talking about limits (or maybe infinitesimals), and derivatives, integrals, and the like. and i suppose MKOConnor is using the term here for such a system, even though it's synthetically rather than analytically conceived |
2025-04-10 20:21:50 +0200 | <EvanR> | which would make it the opposite of constructing or building |
2025-04-10 20:22:04 +0200 | <ski> | yes |
2025-04-10 20:22:34 +0200 | <ski> | reverse-engineering our vague intuitions, in order to build a concrete implementation |
2025-04-10 20:23:05 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
2025-04-10 20:24:29 +0200 | <ski> | e.g. how Descartes reduced geometry to numbers, by the coordinate system. giving a concrete way one can realize/implement e.g. a plane, as a set of points which each are pairs of real number (rather than being some kind of abstract geometric points, conceived of without a priori having a coordinate system) |
2025-04-10 20:25:02 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) |
2025-04-10 20:25:34 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) (Changing host) |
2025-04-10 20:25:34 +0200 | XZDX | (~xzdx@user/XZDX) XZDX |
2025-04-10 20:26:00 +0200 | <ski> | (Descartes also apparently claimed that he got the idea for this (the coordinate system), as a method of gaining knowledge/power over the elements, from an angel in a dream ..) |
2025-04-10 20:26:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-04-10 20:26:53 +0200 | <EvanR> | in the plato.stanford article on descartes I was surprised to learn a lot of unrelated-to-coordinate-planes stuff about his career |
2025-04-10 20:27:20 +0200 | <ski> | mhm ? |
2025-04-10 20:27:39 +0200 | <EvanR> | it was a time when people were arguing about whether this or that curve was sufficiently geometric |
2025-04-10 20:27:58 +0200 | <EvanR> | and there was work on connecting algebraic formulas and curves |
2025-04-10 20:28:27 +0200 | <ski> | yep |
2025-04-10 20:28:27 +0200 | <EvanR> | stuff like conic sections were tentatively geometric at the time because you could construct it by cutting off a piece of cone |
2025-04-10 20:28:46 +0200 | <EvanR> | but cubic curves being geometric was like blasphemy |
2025-04-10 20:29:15 +0200 | <ski> | (i don't recall whether i read/skimmed those Stanford encyclopaedia articles, though. i'v read a bunch of others) |
2025-04-10 20:29:52 +0200 | <ski> | mm. because of the restriction to unmarked ruler, and compass, in the constructions in Euclid's Elementa |
2025-04-10 20:30:11 +0200 | <EvanR> | I'm not sure if that was the strict criteria anymore |
2025-04-10 20:30:31 +0200 | <EvanR> | but "any random curve you can dream up" was certainly not necessarily a proper geometric curve |
2025-04-10 20:30:55 +0200 | <EvanR> | this is the shit descartes was dealing with xD |
2025-04-10 20:31:16 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
2025-04-10 20:31:26 +0200 | ski | . o O ( "Quod Erat Faciendum" ("Which was to be constructed") -- the Elementa has both theorems, and constructions, but modern formulations of logic tends to awkwardly phrase the latter as existential theorems. type theory makes theorems special cases of constructions ) |
2025-04-10 20:32:27 +0200 | <ski> | istr hearing about various mechanical devices, for drawing cubic curves |
2025-04-10 20:33:00 +0200 | <EvanR> | yeah the had more devices |
2025-04-10 20:33:01 +0200 | <haskellbridge> | <Bowuigi> Is geometric algebra related to anything here? It has "geometric" on the name |
2025-04-10 20:33:22 +0200 | <ski> | (<https://plato.stanford.edu/entries/descartes/>,<https://plato.stanford.edu/entries/descartes-works/> being "those articles", in this case) |
2025-04-10 20:34:18 +0200 | <ski> | i haven't really looked much into it. afaiui, it builds geometric objects out of other ones, with a basic set of combinators, so it's basically a DSL |
2025-04-10 20:34:32 +0200 | <EvanR> | hilbert in referring to a hypothetical machine or effective method to decide geometry referred to "constructible using only compass, straight edge, and segment transferer" |
2025-04-10 20:34:43 +0200 | bsima | (~bsima@2604:a880:400:d0::19f1:7001) (So long, and thanks for all the fish.) |
2025-04-10 20:34:45 +0200 | <ski> | i'd assume that it's synthetic in nature, but perhaps it has both synthetic and analytic aspects |
2025-04-10 20:37:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 20:37:37 +0200 | frosthaern | (~frosthaer@2406:7400:116:ac19:3f62:4a05:5a1d:7cdc) |
2025-04-10 20:37:45 +0200 | ski | . o O ( "Analytic and algebraic topology of locally Euclidean metrization of infinitely differentiable Riemannian manifold" -- "(The Great) Lobachevsky" by Tom Lehrer in 1953 at <https://www.youtube.com/watch?v=gXlfXirQF3A> ) |
2025-04-10 20:37:58 +0200 | frosthaern | (~frosthaer@2406:7400:116:ac19:3f62:4a05:5a1d:7cdc) (Client Quit) |
2025-04-10 20:40:26 +0200 | <EvanR> | I found the part which uses the literal word unraveling. Proposition 1.3.12 Let F be any family of intervals, and [a,b] a rational interval. Then a <= F <= b if and only if [a,b] intersects each interval of F. |
2025-04-10 20:40:50 +0200 | <EvanR> | The proof is left as an exercise in "unravelling" that everyone should do |
2025-04-10 20:41:05 +0200 | <EvanR> | (some notational context is missing to make sense of that proposition) |
2025-04-10 20:41:59 +0200 | <EvanR> | the jargon might just be coincidence |
2025-04-10 20:43:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-04-10 20:43:11 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
2025-04-10 20:43:27 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
2025-04-10 20:45:40 +0200 | monochrom | would not analyse too much the choice of the word "analysis". >:) |
2025-04-10 20:46:00 +0200 | <EvanR> | wikipedia suggests geometric algebra is related to exterior product |
2025-04-10 20:46:31 +0200 | <EvanR> | monochrom, it's a nonce placeholder for a subject name! |
2025-04-10 20:47:02 +0200 | <mauke> | nonce = child molester |
2025-04-10 20:48:10 +0200 | <EvanR> | who put that in the dictionary |
2025-04-10 20:48:24 +0200 | <monochrom> | Right, there is no such thing as "meaningful name". |
2025-04-10 20:50:00 +0200 | <ski> | that's one of two meanings of "nonce" |
2025-04-10 20:50:52 +0200 | <ski> | is `x + 1' a "name" ? |
2025-04-10 20:51:40 +0200 | <mauke> | maybe. is its father called elon? |
2025-04-10 20:51:48 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-04-10 20:52:01 +0200 | <ski> | (mathematicians would sometimes refer to it as such. programmers would probably say "expression" instead) |
2025-04-10 20:53:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 20:57:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
2025-04-10 21:00:02 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
2025-04-10 21:00:45 +0200 | caconym | (~caconym@user/caconym) caconym |
2025-04-10 21:03:52 +0200 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
2025-04-10 21:08:01 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
2025-04-10 21:09:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 21:12:06 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 244 seconds) |
2025-04-10 21:14:48 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
2025-04-10 21:15:17 +0200 | cheater | (~Username@user/cheater) cheater |
2025-04-10 21:15:24 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
2025-04-10 21:16:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 21:17:41 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 21:18:10 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
2025-04-10 21:19:22 +0200 | feetwind | (~mike@user/feetwind) feetwind |
2025-04-10 21:22:19 +0200 | <feetwind> | anyone remember the tool ghc-core? it would pretty print ghc core for you. i swear there was a more modern equivalent of it out there though, like a browser based tool you could interactively collapse/expand parts of the core with, but struggling to find it |
2025-04-10 21:22:35 +0200 | <feetwind> | maybe it was just a dream |
2025-04-10 21:22:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-10 21:22:45 +0200 | XZDX | (~xzdx@user/XZDX) (Ping timeout: 260 seconds) |
2025-04-10 21:25:46 +0200 | <geekosaur> | https://flora.pm/packages/@hackage/dump-core maybe? |
2025-04-10 21:26:53 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
2025-04-10 21:27:20 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
2025-04-10 21:33:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 21:34:48 +0200 | <feetwind> | yes surely, thx :) |
2025-04-10 21:38:35 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
2025-04-10 21:39:20 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
2025-04-10 21:41:26 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
2025-04-10 21:44:47 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
2025-04-10 21:45:43 +0200 | rbdr | (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) |
2025-04-10 21:49:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 21:51:20 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
2025-04-10 21:51:20 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-04-10 21:53:18 +0200 | <hellwolf> | https://play.haskell.org/saved/JaGKxO4E this is just weirld. (need to use L11 instead of L10) |
2025-04-10 21:53:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
2025-04-10 21:55:16 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:a504:86ce:5139:ec16) (Read error: Connection reset by peer) |
2025-04-10 21:57:13 +0200 | <int-e> | you can use a2 x = A2 x |
2025-04-10 21:57:51 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
2025-04-10 21:58:41 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-04-10 21:59:59 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) |
2025-04-10 22:00:21 +0200 | alp | (~alp@2001:861:8ca0:4940:e00c:8d19:d96b:e8b0) (Ping timeout: 248 seconds) |
2025-04-10 22:01:28 +0200 | <int-e> | And then a2 :: a -> A a will work |
2025-04-10 22:02:48 +0200 | rbdr | (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) (Quit: rbdr) |
2025-04-10 22:03:33 +0200 | XZDX | (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) (Changing host) |
2025-04-10 22:03:33 +0200 | XZDX | (~xzdx@user/XZDX) XZDX |
2025-04-10 22:06:55 +0200 | <hellwolf> | interesting, more weird. |
2025-04-10 22:07:57 +0200 | <int-e> | The mental model I have for this is that GHC can implicitly change some types, adding, shuffling or removing constraints, but it will only do that for visible variables. |
2025-04-10 22:08:15 +0200 | <int-e> | So by naming `x`, x :: a can be used as x :: Show a => a as required by A2 |
2025-04-10 22:08:45 +0200 | <int-e> | (I'm assuming that you do understand that the types of A1 and A2 are different) |
2025-04-10 22:09:21 +0200 | <hellwolf> | I understand the rankN part |
2025-04-10 22:10:29 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
2025-04-10 22:10:33 +0200 | rbdr | (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) rbdr |
2025-04-10 22:12:14 +0200 | <int-e> | Without naming x GHC will try to match the whole Show a => a -> A a against (Show a => a) -> A a and that fails because Show a => a and a are different types (incidentally with different representations) |
2025-04-10 22:12:23 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
2025-04-10 22:12:56 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
2025-04-10 22:14:03 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
2025-04-10 22:14:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
2025-04-10 22:14:08 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
2025-04-10 22:14:14 +0200 | <EvanR> | (Show a => a) -> A a is a thing? Is it rank 2 |
2025-04-10 22:14:48 +0200 | hattckory | (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
2025-04-10 22:15:58 +0200 | <int-e> | Well I omitted the forall. that goes with it |
2025-04-10 22:16:34 +0200 | <int-e> | But yeah it's a rank 2 type. Also... probably more useful with other classes that actually provide functions that return an a. |
2025-04-10 22:16:53 +0200 | <hellwolf> | yea, I extracted from my code. it's a bit contrived. |
2025-04-10 22:16:59 +0200 | <hellwolf> | with Show. |
2025-04-10 22:17:32 +0200 | <EvanR> | (forall a . Show a => a) -> A a -- different a? |
2025-04-10 22:18:26 +0200 | <int-e> | EvanR: No, it's literally an empty forall. |
2025-04-10 22:18:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 22:18:56 +0200 | <int-e> | EvanR: there was a link: https://play.haskell.org/saved/JaGKxO4E |
2025-04-10 22:19:54 +0200 | <EvanR> | wtf |
2025-04-10 22:20:32 +0200 | <EvanR> | I saw an "bindless lambda" yesterday like \whatever |
2025-04-10 22:20:41 +0200 | <EvanR> | but now I've seen everything |
2025-04-10 22:22:22 +0200 | <int-e> | :t \ -> () |
2025-04-10 22:22:23 +0200 | <lambdabot> | error: parse error on input ‘->’ |
2025-04-10 22:22:25 +0200 | <int-e> | ;-) |
2025-04-10 22:22:50 +0200 | <hellwolf> | I have a feeling this won't be the last one |
2025-04-10 22:23:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-04-10 22:24:05 +0200 | <int-e> | FWIW, that forall. is not actually needed. |
2025-04-10 22:24:58 +0200 | <hellwolf> | I like to write "forall." explicitly sometimes, so that no typo will create a type variable by accident. |
2025-04-10 22:25:33 +0200 | <EvanR> | need a type system for the type signatures to keep it straight |
2025-04-10 22:25:53 +0200 | <int-e> | hellwolf: It's fairly common to need a few eta-expansions when working with higher rank types in GHC. |
2025-04-10 22:26:05 +0200 | <int-e> | EvanR: let me tell you about kinds |
2025-04-10 22:26:43 +0200 | <hellwolf> | I have noticed also with linear arrows sometimes. |
2025-04-10 22:28:01 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
2025-04-10 22:28:17 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
2025-04-10 22:28:18 +0200 | biberu | (~biberu@user/biberu) biberu |
2025-04-10 22:28:28 +0200 | <int-e> | hellwolf: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/rank_polymorphism.html#subsumption has some details about this particular facet of RankNTypes |
2025-04-10 22:29:29 +0200 | bliminse | (~bliminse@user/bliminse) (Quit: leaving) |
2025-04-10 22:30:43 +0200 | <int-e> | Oh there's a DeepSubsumption extension for this? I never knew. |
2025-04-10 22:30:58 +0200 | <int-e> | Indeed that makes a2 = A2 compile. |
2025-04-10 22:31:33 +0200 | <geekosaur> | it's pretty recent and documented as ephemeral (that is, it's inteended only as a porting aid and expected to go away) |
2025-04-10 22:31:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 22:34:05 +0200 | amadaluzia_ | (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) (Changing host) |
2025-04-10 22:34:05 +0200 | amadaluzia_ | (~amadaluzi@user/amadaluzia) amadaluzia |
2025-04-10 22:34:39 +0200 | <int-e> | So... DeepSubsumption enables some functionality that GHC never had, but is scheduled to be removed. That's fun. |
2025-04-10 22:35:00 +0200 | bliminse | (~bliminse@user/bliminse) bliminse |
2025-04-10 22:35:04 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds) |
2025-04-10 22:36:00 +0200 | <hellwolf> | I remember it caused a huge disturbance in the universe |
2025-04-10 22:36:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
2025-04-10 22:36:35 +0200 | <mauke> | 42 :: exists. Int |
2025-04-10 22:37:38 +0200 | <hellwolf> | foo :: exists a. a ~ Void => a |
2025-04-10 22:39:41 +0200 | <int-e> | Oh. I'm wrong; GHC 8.2 to 8.10 do accept a2 = A2. GHC 8.0 and 9.0 do not. And 9.2 is the first version to support DeepSubsumption. |
2025-04-10 22:40:05 +0200 | <int-e> | I don't have any pre-8.0 versions to test. |
2025-04-10 22:40:14 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
2025-04-10 22:40:31 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
2025-04-10 22:42:29 +0200 | tromp | (~textual@2001:1c00:3487:1b00:44ed:cdbe:8e8e:71c5) (Ping timeout: 248 seconds) |
2025-04-10 22:44:09 +0200 | <hellwolf> | I think this belongs to one of more GHC terms that the utterance of the word means absolute nothing to most of non-type-theory people |
2025-04-10 22:46:18 +0200 | <monochrom> | DeepSubsumption is a backward-compatibility flag for newer GHCs that provide quicklook impredicativity. |
2025-04-10 22:46:20 +0200 | <int-e> | ironically I learned about RankNTypes before 8.2 so this need for eta-expansion did not surprise me. |
2025-04-10 22:47:05 +0200 | <hellwolf> | oh impredicativetypes is that other magic spell word |
2025-04-10 22:47:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 22:47:54 +0200 | myme | (~myme@2a01:799:d5e:5f00:8f18:9cf4:29f5:943f) (Ping timeout: 265 seconds) |
2025-04-10 22:48:18 +0200 | <monochrom> | In more detail, in those newer GHCs, even if you don't ask for impredicativity, you still get the modified type inference algorithm. |
2025-04-10 22:48:47 +0200 | myme | (~myme@2a01:799:d5e:5f00:2d74:af8d:2498:f0a8) myme |
2025-04-10 22:49:40 +0200 | <geekosaur> | yes. there's a discussion in 9.0.1's release notes iirc |
2025-04-10 22:50:24 +0200 | <int-e> | I guess both terms have their origin in logic. Subsumption translates to one type being more general than another. Impredicativity... tbh I still don't quite know what that really is, never mind how it got that name. |
2025-04-10 22:51:20 +0200 | <EvanR> | it's literally the negation of something |
2025-04-10 22:51:30 +0200 | <int-e> | I get *that* |
2025-04-10 22:51:38 +0200 | <EvanR> | so not a great way to get at what it positively is |
2025-04-10 22:51:53 +0200 | <EvanR> | like non-linear |
2025-04-10 22:52:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
2025-04-10 22:52:07 +0200 | <int-e> | EvanR: stop |
2025-04-10 22:52:15 +0200 | <int-e> | (you're not helping) |
2025-04-10 22:52:33 +0200 | <hellwolf> | impredatory language |
2025-04-10 22:52:39 +0200 | <EvanR> | stop agreeing with me |
2025-04-10 22:52:42 +0200 | amadaluzia_ | (~amadaluzi@user/amadaluzia) (Quit: Hi, this is Paul Allen. I'm being called away to London for a few days. Meredith, I'll call you when I get back. Hasta la vista, baby.) |
2025-04-10 22:52:42 +0200 | <hellwolf> | aka. javascript |
2025-04-10 22:52:43 +0200 | <int-e> | (and frankly I didn't ask for an explanation) |
2025-04-10 22:53:04 +0200 | amadaluzia | (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) |
2025-04-10 22:53:06 +0200 | <hellwolf> | predatory language. aka Haskell |
2025-04-10 22:53:21 +0200 | <hellwolf> | or the other way around, depending on the user. |
2025-04-10 22:53:30 +0200 | amadaluzia | (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) (Remote host closed the connection) |
2025-04-10 22:53:52 +0200 | amadaluzia | (~amadaluzi@host217-43-236-22.range217-43.btcentralplus.com) |
2025-04-10 22:54:54 +0200 | <EvanR> | otoh I can ask what impredicativity means |
2025-04-10 22:55:16 +0200 | <EvanR> | in this context |
2025-04-10 22:55:38 +0200 | <hellwolf> | [forall a. a -> String] |
2025-04-10 22:55:45 +0200 | <hellwolf> | is this impredicative type or rankn |
2025-04-10 22:55:49 +0200 | <monochrom> | It means that for example "Maybe (forall a. a->a)" is acceptable, you don't have to make your own newtype wrapper for the "forall a. a->a" part. |
2025-04-10 22:55:57 +0200 | <monochrom> | Impredicative. |
2025-04-10 22:56:02 +0200 | Guest87 | (~Guest87@2620:72:0:1f18:7d2a:62e7:7a20:d79f) |
2025-04-10 22:56:54 +0200 | <monochrom> | Impredicative implies rank-n so it's also rank-n :) |
2025-04-10 22:56:57 +0200 | <hellwolf> | so (forall a. a -> String) -> String is rankn |
2025-04-10 22:57:10 +0200 | <hellwolf> | but [forall a. a -> String] -> Srring is impredicativetypes |
2025-04-10 22:57:39 +0200 | <hellwolf> | ah, so it is generalization |
2025-04-10 22:57:40 +0200 | <hellwolf> | ? |
2025-04-10 22:58:11 +0200 | <EvanR> | when you go to substitute a type into forall a . a -> a, instanciate the type, is yet another "forall a . a -> a" a valid substitution |
2025-04-10 22:58:50 +0200 | <monochrom> | Yes you can have id (id :: forall a. a -> a) |
2025-04-10 22:59:31 +0200 | <monochrom> | You can have [id :: forall a. a->a] |
2025-04-10 23:00:13 +0200 | <EvanR> | :t id (id :: forall a . a -> a) |
2025-04-10 23:00:14 +0200 | <lambdabot> | a -> a |
2025-04-10 23:00:25 +0200 | <monochrom> | lambdabot doesn't do impredicative. |
2025-04-10 23:00:44 +0200 | <hellwolf> | :t id id id id id id id id |
2025-04-10 23:00:45 +0200 | <lambdabot> | a -> a |
2025-04-10 23:01:54 +0200 | <hellwolf> | %import Data.Void |
2025-04-10 23:02:04 +0200 | <ncf> | :t fmap fmap fmap fmap id id id id |
2025-04-10 23:02:05 +0200 | <lambdabot> | a -> a |
2025-04-10 23:02:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-04-10 23:03:08 +0200 | <Guest87> | Hey folks. I have a fp problem that I am curious if it can be solved without a list, but haven't been able to figure out an easy/obvious solution |
2025-04-10 23:03:08 +0200 | <Guest87> | Suppose I want to represent an a mapping of variables to values. Can be done with a list, or with the following functions: |
2025-04-10 23:03:09 +0200 | <Guest87> | ``` |
2025-04-10 23:03:09 +0200 | <Guest87> | makeEnv = \a -> undefined |
2025-04-10 23:03:10 +0200 | <Guest87> | extendEnv var val env = \y -> if y == var then val else (env y) |
2025-04-10 23:03:10 +0200 | <Guest87> | ``` |
2025-04-10 23:03:38 +0200 | <Guest87> | But say I want the oldest variable binding to be in the front instead of in the back. This can easily be done with a list, but is it possible to do it with functions? :) |
2025-04-10 23:03:40 +0200 | <monochrom> | You can do that. You can also use Data.Map. |
2025-04-10 23:04:35 +0200 | <monochrom> | Functions will not be very good at that, especially if you use undefined. |
2025-04-10 23:04:39 +0200 | amadaluzia | (~amadaluzi@host217-43-236-22.range217-43.btcentralplus.com) (Quit: Hi, this is Paul Allen. I'm being called away to London for a few days. Meredith, I'll call you when I get back. Hasta la vista, baby.) |
2025-04-10 23:04:58 +0200 | <Guest87> | I totally could, but this problem is a simpler representation of a problem I am trying to solve in a different language. |
2025-04-10 23:05:18 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 272 seconds) |
2025-04-10 23:05:28 +0200 | <monochrom> | I thought lists were more available than functions in a different language. |
2025-04-10 23:05:40 +0200 | <monochrom> | Unless that other language is System F. |
2025-04-10 23:05:55 +0200 | <Guest87> | They are haha, but I am being stubborn and trying to do it the cool way |
2025-04-10 23:06:13 +0200 | <EvanR> | you can represent the list data type using lambdas |
2025-04-10 23:06:26 +0200 | <EvanR> | I dunno if that's cool enough though |
2025-04-10 23:06:45 +0200 | <Guest87> | I will most likely have to do the list implementation for "maintability", but very curious to see if there's a a way to define this "reverse mapping" |
2025-04-10 23:06:47 +0200 | amadaluzia | (~amadaluzi@host217-43-236-22.range217-43.btcentralplus.com) |
2025-04-10 23:06:57 +0200 | <monochrom> | Representing list use lambda also requires either impredicativity or untyped. |
2025-04-10 23:07:59 +0200 | <int-e> | Guest87: with the definitions you've given, extendEnv "v" 2 (extendEnv "v" 1 makeEnv) is indistinguishable from extendEnv "v" 2 makeEnv; they're the same function. |
2025-04-10 23:08:21 +0200 | enoq | (~enoq@2a05:1141:1e6:3b00:6d50:57a3:cc97:7b04) enoq |
2025-04-10 23:09:06 +0200 | <enoq> | sorry for the provocative question: I like a lot of the concepts but I find the symbol soup worse than Perl, is there a similar language that uses words? |
2025-04-10 23:09:08 +0200 | <int-e> | So the shadowed values (here "v" -> 1) are completely inaccessible. |
2025-04-10 23:09:37 +0200 | <EvanR> | "too many operators" is usually a reaction to not knowing what <$> or <*> means |
2025-04-10 23:09:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
2025-04-10 23:09:46 +0200 | <enoq> | am I looking for something like Scala? |
2025-04-10 23:09:55 +0200 | <EvanR> | my list of "all (default) haskell operators" is most consisting of operators available in "normal" languages |
2025-04-10 23:10:01 +0200 | <EvanR> | mostly |
2025-04-10 23:10:16 +0200 | <EvanR> | probably a better idea to just look up what <$> and <*> are |
2025-04-10 23:10:27 +0200 | <monochrom> | You are fundamentally specifying: If var is already in env, don't extend, else extend. If you use Nothing/Just instead of undefined, that will be very easy to do. |
2025-04-10 23:10:28 +0200 | <EvanR> | (they're useful) |
2025-04-10 23:10:37 +0200 | <int-e> | EvanR: Who knows, maybe they're dealing with lens |
2025-04-10 23:10:52 +0200 | amadaluzia | (~amadaluzi@host217-43-236-22.range217-43.btcentralplus.com) (Client Quit) |
2025-04-10 23:10:52 +0200 | <monochrom> | COBOL uses words. |
2025-04-10 23:11:12 +0200 | <enoq> | a hell of a lot of those yeah xD |
2025-04-10 23:11:13 +0200 | <monochrom> | You literally have to write "MULTIPLY X BY Y INTO Z" |
2025-04-10 23:11:13 +0200 | inca | (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
2025-04-10 23:11:33 +0200 | <enoq> | like applicativeMap instead of <*> |
2025-04-10 23:11:42 +0200 | <EvanR> | it's not a map |
2025-04-10 23:11:48 +0200 | <enoq> | or just applicative |
2025-04-10 23:11:53 +0200 | <__monty__> | `ap` no? |
2025-04-10 23:11:58 +0200 | <haskellbridge> | <loonycyborg> can just put functions in `` and use them as operators |
2025-04-10 23:11:58 +0200 | <EvanR> | ap exists |
2025-04-10 23:12:14 +0200 | <haskellbridge> | <loonycyborg> "asTypeOf" etc :P |
2025-04-10 23:12:15 +0200 | <monochrom> | I don't get why people want English/words for coding. But that's none of my business. My business though is to remind them that they can always go back to COBOL. |
2025-04-10 23:12:55 +0200 | <enoq> | no need to pick either extreme |
2025-04-10 23:13:14 +0200 | <EvanR> | but pure f `ap` x `ap` y `ap` z has the issue of annoying people who read it, which might be the real issue |
2025-04-10 23:13:28 +0200 | <EvanR> | also in cobol |
2025-04-10 23:13:35 +0200 | <int-e> | monochrom: isn't the lesson that we've learned from COBOL that learning a programming language's syntax does not get easier when it uses words |
2025-04-10 23:13:36 +0200 | <monochrom> | Haskell is already neither extreme. |
2025-04-10 23:14:12 +0200 | <int-e> | and the programs don't become more readable either |
2025-04-10 23:14:16 +0200 | <enoq> | yeah, I guess you could say APL is even worse |
2025-04-10 23:14:40 +0200 | <monochrom> | We are like "mod 5 3" which is even more wordy than C. |
2025-04-10 23:14:59 +0200 | <EvanR> | (other than maybe lens) and library might introduce an operator, and then "don't use this library because there is someone who doesn't know this operator" would mean you can't use most programming languages |
2025-04-10 23:15:03 +0200 | <haskellbridge> | <loonycyborg> one most unusual choice is use of space for function application instead of more common (x,y..) |
2025-04-10 23:15:04 +0200 | <int-e> | or 5 `mod` 3 |
2025-04-10 23:15:08 +0200 | <Guest87> | int-e Oh I guess that's true. But let's say that's intentional but I want `extendEnv "v" 1 (extendEnv "v" 2 makeEnv)` to be indistinguishable from `extendEnv "v" ` makeEnv`. Is there an easy way to do that? |
2025-04-10 23:15:14 +0200 | <EvanR> | but that issue exists for non-operators |
2025-04-10 23:15:21 +0200 | <__monty__> | 5 `mod` 3 is arguably more readable IMO. |