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 |