2025/04/10

2025-04-10 00:01:13 +0200weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-04-10 00:01:30 +0200weary-traveler(~user@user/user363627) user363627
2025-04-10 00:02:35 +0200tromp(~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-10 00:02:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 00:08:05 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) krjst
2025-04-10 00:08:10 +0200tv(~tv@user/tv) (Read error: Connection reset by peer)
2025-04-10 00:14:03 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 00:15:20 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-04-10 00:16:52 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
2025-04-10 00:18:26 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-04-10 00:18:26 +0200ljdarj1ljdarj
2025-04-10 00:20:20 +0200 <__monty__> Can you elaborate?
2025-04-10 00:21:20 +0200merijn(~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 +0200chiselfuse(~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds)
2025-04-10 00:23:47 +0200chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-04-10 00:32:06 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 00:43:40 +0200tv(~tv@user/tv) tv
2025-04-10 00:43:48 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) krjst
2025-04-10 00:47:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 00:52:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-04-10 00:53:31 +0200Sgeo(~Sgeo@user/sgeo) Sgeo
2025-04-10 01:00:16 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
2025-04-10 01:03:40 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:04:10 +0200ystael(~ystael@user/ystael) (Ping timeout: 272 seconds)
2025-04-10 01:06:30 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 01:07:28 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Client Quit)
2025-04-10 01:08:09 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 01:08:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-10 01:09:25 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 01:11:44 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
2025-04-10 01:14:30 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye)
2025-04-10 01:14:59 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 01:19:17 +0200Square(~Square4@user/square) (Ping timeout: 248 seconds)
2025-04-10 01:19:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:19:42 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:21:44 +0200polykernel(~polykerne@user/polykernel) (Ping timeout: 252 seconds)
2025-04-10 01:23:46 +0200polykernel(~polykerne@user/polykernel) polykernel
2025-04-10 01:24:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-10 01:25:09 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
2025-04-10 01:28:02 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
2025-04-10 01:29:29 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-04-10 01:31:04 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:31:53 +0200Square2(~Square@user/square) Square
2025-04-10 01:33:45 +0200sprotte24(~sprotte24@p200300d16f0bc1000c82a6b41033ea55.dip0.t-ipconnect.de) (Quit: Leaving)
2025-04-10 01:35:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:35:49 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 248 seconds)
2025-04-10 01:39:34 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-04-10 01:39:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 01:48:53 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:51:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:56:12 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
2025-04-10 01:56:49 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e)
2025-04-10 01:57:02 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:57:31 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-10 01:59:05 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Changing host)
2025-04-10 01:59:05 +0200XZDX(~xzdx@user/XZDX) XZDX
2025-04-10 02:03:10 +0200jespada(~jespada@r190-133-30-51.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds)
2025-04-10 02:08:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:11:52 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye)
2025-04-10 02:12:13 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 02:13:05 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-04-10 02:21:38 +0200acidjnk_new3(~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Remote host closed the connection)
2025-04-10 02:22:22 +0200acidjnk_new3(~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de)
2025-04-10 02:23:55 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 02:23:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:25:18 +0200poscat0x04(~poscat@user/poscat) (Ping timeout: 276 seconds)
2025-04-10 02:26:16 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
2025-04-10 02:28:37 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 02:31:02 +0200polyphem(~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 +0200poscat(~poscat@user/poscat) poscat
2025-04-10 02:39:25 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 02:39:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:45:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-10 02:45:35 +0200notdabs(~Owner@2600:1700:69cf:9000:19b2:995a:60d5:3b93) (Quit: Leaving)
2025-04-10 02:53:09 +0200xff0x(~xff0x@2405:6580:b080:900:b50:e5e9:27c3:86) (Ping timeout: 248 seconds)
2025-04-10 02:55:31 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:55:49 +0200foul_owl(~kerry@94.156.149.99) (Ping timeout: 248 seconds)
2025-04-10 02:58:09 +0200otto_s(~user@p4ff27c58.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2025-04-10 03:00:05 +0200otto_s(~user@p4ff278a2.dip0.t-ipconnect.de)
2025-04-10 03:01:03 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-10 03:03:56 +0200acidjnk_new(~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de)
2025-04-10 03:05:53 +0200acidjnk_new3(~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-04-10 03:06:42 +0200foul_owl(~kerry@174-21-146-90.tukw.qwest.net) foul_owl
2025-04-10 03:08:43 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds)
2025-04-10 03:13:42 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-10 03:13:56 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-10 03:21:07 +0200tavare(~tavare@150.129.88.189) tavare
2025-04-10 03:21:07 +0200tavare(~tavare@150.129.88.189) (Changing host)
2025-04-10 03:21:07 +0200tavare(~tavare@user/tavare) tavare
2025-04-10 03:25:05 +0200acidjnk_new(~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2025-04-10 03:26:27 +0200foul_owl(~kerry@174-21-146-90.tukw.qwest.net) (Ping timeout: 265 seconds)
2025-04-10 03:27:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 03:28:54 +0200ezzieygu1wuf(~Unknown@user/ezzieyguywuf) (Ping timeout: 246 seconds)
2025-04-10 03:30:39 +0200aforemny_(~aforemny@i59F4C56B.versanet.de) (Ping timeout: 244 seconds)
2025-04-10 03:31:24 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2025-04-10 03:32:00 +0200merijn(~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 +0200Square(~Square4@user/square) Square
2025-04-10 03:37:13 +0200weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-04-10 03:37:29 +0200weary-traveler(~user@user/user363627) user363627
2025-04-10 03:39:08 +0200Square2(~Square@user/square) (Ping timeout: 245 seconds)
2025-04-10 03:40:19 +0200foul_owl(~kerry@94.156.149.91) foul_owl
2025-04-10 03:42:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 03:47:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 03:50:08 +0200aforemny(~aforemny@i59F4C778.versanet.de) aforemny
2025-04-10 03:50:13 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-04-10 03:58:42 +0200merijn(~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 +0200merijn(~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 +0200tessier(~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 +0200tessier(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 04:16:32 +0200slack1256(~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) slack1256
2025-04-10 04:16:48 +0200tavare(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 04:21:00 +0200ryanbooker(uid4340@id-4340.hampstead.irccloud.com) ryanbooker
2025-04-10 04:24:54 +0200TheCoffeMaker(~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 +0200TheCoffeMaker(~TheCoffeM@user/thecoffemaker) TheCoffeMaker
2025-04-10 04:29:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 04:29:57 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-10 04:31:13 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 265 seconds)
2025-04-10 04:34:06 +0200stef204(~stef204@user/stef204) (Quit: WeeChat 4.2.1)
2025-04-10 04:35:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-04-10 04:37:02 +0200slack1256(~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) (Remote host closed the connection)
2025-04-10 04:45:34 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 04:46:14 +0200hattckory(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 05:01:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 05:06:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 05:17:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 05:18:10 +0200tamer(~tamer@user/tamer) (Read error: Connection reset by peer)
2025-04-10 05:22:24 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-10 05:32:23 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 05:32:53 +0200merijn(~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 +0200tamer(~tamer@5.2.74.82)
2025-04-10 05:37:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 05:41:02 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 05:48:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 05:50:14 +0200zlqrvx_(~zlqrvx@101.175.150.247)
2025-04-10 05:51:15 +0200zlqrvx(~zlqrvx@101.175.150.247) (Read error: Connection reset by peer)
2025-04-10 05:54:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-10 05:57:56 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 06:01:16 +0200bitdex_(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 06:01:24 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-04-10 06:04:03 +0200whez(uid470288@id-470288.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2025-04-10 06:04:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 06:09:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 06:09:14 +0200peterbecich(~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 +0200michalz(~michalz@185.246.207.201)
2025-04-10 06:20:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 06:23:05 +0200bitdex_(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-04-10 06:23:28 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 06:25:18 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-04-10 06:31:13 +0200sayurc(~sayurc@169.150.203.34) (Quit: Konversation terminated!)
2025-04-10 06:36:01 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 06:38:41 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds)
2025-04-10 06:41:14 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-10 06:43:29 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 06:49:12 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-10 06:58:47 +0200hattckory(~hattckory@70.27.118.207)
2025-04-10 06:59:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 07:03:54 +0200hattckory(~hattckory@70.27.118.207) (Ping timeout: 260 seconds)
2025-04-10 07:04:29 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-10 07:10:35 +0200Square2(~Square@user/square) Square
2025-04-10 07:12:42 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 07:14:34 +0200Square(~Square4@user/square) (Ping timeout: 260 seconds)
2025-04-10 07:15:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 07:15:42 +0200sayurc(~sayurc@169.150.203.34) sayurc
2025-04-10 07:17:16 +0200amadaluzia(~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 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 07:19:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 07:20:47 +0200ryanbooker(uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2025-04-10 07:23:29 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds)
2025-04-10 07:26:45 +0200amadaluzia(~amadaluzi@user/amadaluzia) amadaluzia
2025-04-10 07:30:50 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 07:33:48 +0200michalz(~michalz@185.246.207.201) (Quit: ZNC 1.9.1 - https://znc.in)
2025-04-10 07:34:06 +0200michalz(~michalz@185.246.207.201)
2025-04-10 07:36:12 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-04-10 07:37:11 +0200michalz(~michalz@185.246.207.201) (Client Quit)
2025-04-10 07:37:34 +0200michalz(~michalz@185.246.207.221)
2025-04-10 07:38:18 +0200peterbecich(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 07:51:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 07:59:47 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 08:05:15 +0200hattckory(~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 +0200peterbecich(~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 +0200Square2(~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 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 08:16:55 +0200foul_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 +0200weary-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 +0200jmcantrell(~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0)
2025-04-10 08:22:33 +0200jmcantrell_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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 08:28:51 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
2025-04-10 08:31:00 +0200foul_owl(~kerry@94.156.149.97) foul_owl
2025-04-10 08:32:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 08:37:57 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 246 seconds)
2025-04-10 08:42:58 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 08:43:29 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 08:47:44 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds)
2025-04-10 08:48:07 +0200ft(~ft@p508db594.dip0.t-ipconnect.de) (Quit: leaving)
2025-04-10 08:48:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 08:50:37 +0200tromp(~textual@2001:1c00:3487:1b00:44ed:cdbe:8e8e:71c5)
2025-04-10 08:51:52 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 08:57:11 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 244 seconds)
2025-04-10 08:57:16 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-04-10 08:59:14 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 09:00:04 +0200caconym(~caconym@user/caconym) (Quit: bye)
2025-04-10 09:01:03 +0200caconym(~caconym@user/caconym) caconym
2025-04-10 09:03:09 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 09:04:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-04-10 09:05:20 +0200inca(~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 +0200remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) (Ping timeout: 252 seconds)
2025-04-10 09:15:44 +0200TMA(tma@twin.jikos.cz) (Ping timeout: 260 seconds)
2025-04-10 09:18:18 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds)
2025-04-10 09:18:26 +0200Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-04-10 09:19:12 +0200vpan(~vpan@212.117.1.172)
2025-04-10 09:19:50 +0200Lord_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 +0200remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan
2025-04-10 09:29:41 +0200chele(~chele@user/chele) chele
2025-04-10 09:35:37 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-04-10 09:36:43 +0200acidjnk(~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) acidjnk
2025-04-10 09:39:43 +0200XZDX(~xzdx@user/XZDX) (Remote host closed the connection)
2025-04-10 09:40:00 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e)
2025-04-10 09:41:08 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-04-10 09:45:38 +0200lisbeths(uid135845@id-135845.lymington.irccloud.com) lisbeths
2025-04-10 09:49:38 +0200merijn(~merijn@77.242.116.146) merijn
2025-04-10 09:53:30 +0200fp(~Thunderbi@2001:708:20:1406::1370) fp
2025-04-10 09:53:45 +0200ski. o O ( "Interview with Vibe Coder in 2025" <https://www.youtube.com/watch?v=JeNS1ZNHQs8> )
2025-04-10 09:57:30 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-04-10 10:04:33 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds)
2025-04-10 10:19:15 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 10:20:12 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Remote host closed the connection)
2025-04-10 10:25:23 +0200forell(~forell@user/forell) (Quit: ZNC - https://znc.in)
2025-04-10 10:26:40 +0200forell(~forell@user/forell) forell
2025-04-10 10:37:58 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds)
2025-04-10 10:45:12 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-04-10 10:48:21 +0200sprotte24(~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de)
2025-04-10 10:48:53 +0200sprotte24(~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) (Client Quit)
2025-04-10 10:53:51 +0200sayurc(~sayurc@169.150.203.34) (Quit: Konversation terminated!)
2025-04-10 10:56:50 +0200alp(~alp@2001:861:8ca0:4940:e00c:8d19:d96b:e8b0)
2025-04-10 10:59:35 +0200poxel(~lennart@user/poxel) poxel
2025-04-10 11:02:20 +0200poxel(~lennart@user/poxel) (Client Quit)
2025-04-10 11:02:24 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
2025-04-10 11:02:39 +0200poxel(~poxel@user/poxel) poxel
2025-04-10 11:02:44 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
2025-04-10 11:08:04 +0200olivial(~benjaminl@user/benjaminl) (Read error: Connection reset by peer)
2025-04-10 11:08:20 +0200olivial(~benjaminl@user/benjaminl) benjaminl
2025-04-10 11:11:16 +0200lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-04-10 11:17:09 +0200Guest71(~Guest75@37.204.222.118)
2025-04-10 11:19:58 +0200poxel(~poxel@user/poxel) (Quit: WeeChat 4.6.0)
2025-04-10 11:20:18 +0200poxel(~poxel@user/poxel) poxel
2025-04-10 11:31:42 +0200Guest71(~Guest75@37.204.222.118) (Ping timeout: 240 seconds)
2025-04-10 11:34:52 +0200fp(~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 +0200hsw(~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) (Ping timeout: 246 seconds)
2025-04-10 11:45:32 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 11:46:30 +0200hsw(~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) hsw
2025-04-10 11:46:36 +0200sprotte24(~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de)
2025-04-10 11:56:46 +0200lambdap2371(~lambdap@static.167.190.119.168.clients.your-server.de) (Quit: Ping timeout (120 seconds))
2025-04-10 11:57:01 +0200lambdap2371(~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 +0200pavonia(~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 +0200lortabac(~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 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds)
2025-04-10 12:31:09 +0200poxel(~poxel@user/poxel) (Quit: WeeChat 4.6.0)
2025-04-10 12:31:29 +0200poxel(~weechat@user/poxel) poxel
2025-04-10 12:32:04 +0200poxel(~weechat@user/poxel) (Client Quit)
2025-04-10 12:32:23 +0200poxel(~poxel@user/poxel) poxel
2025-04-10 12:37:18 +0200 <yin> separating ghc.base from base
2025-04-10 12:49:53 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds)
2025-04-10 12:55:39 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess
2025-04-10 12:56:36 +0200JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-04-10 13:00:04 +0200caconym(~caconym@user/caconym) (Quit: bye)
2025-04-10 13:00:27 +0200acidjnk(~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
2025-04-10 13:02:12 +0200caconym(~caconym@user/caconym) caconym
2025-04-10 13:02:14 +0200jespada(~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) jespada
2025-04-10 13:04:42 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 13:07:38 +0200TMA(tma@twin.jikos.cz) TMA
2025-04-10 13:08:12 +0200jacopovalanzano(~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net)
2025-04-10 13:09:59 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-04-10 13:11:59 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds)
2025-04-10 13:15:31 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-10 13:15:40 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 272 seconds)
2025-04-10 13:23:40 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 13:25:13 +0200xff0x(~xff0x@2405:6580:b080:900:1c0d:6c97:349e:6228)
2025-04-10 13:30:09 +0200tabaqui(~tabaqui@167.71.80.236) tabaqui
2025-04-10 13:34:09 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds)
2025-04-10 13:34:51 +0200amadaluzia(~amadaluzi@user/amadaluzia) (Remote host closed the connection)
2025-04-10 13:35:33 +0200JuanDaugherty(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-04-10 13:57:33 +0200walt(~ggVGc@a.lowtech.earth) (Ping timeout: 276 seconds)
2025-04-10 13:57:55 +0200walt(~ggVGc@a.lowtech.earth)
2025-04-10 14:03:34 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 14:09:52 +0200bcksl(~bcksl@user/bcksl) (Quit: \)
2025-04-10 14:09:52 +0200end(~end@user/end/x-0094621) (Quit: end)
2025-04-10 14:13:58 +0200jespada(~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) (Ping timeout: 268 seconds)
2025-04-10 14:14:33 +0200acidjnk(~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) acidjnk
2025-04-10 14:16:29 +0200jespada(~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) jespada
2025-04-10 14:20:23 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
2025-04-10 14:20:43 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
2025-04-10 14:41:18 +0200jacopovalanzano(~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Ping timeout: 240 seconds)
2025-04-10 14:43:44 +0200zlqrvx_(~zlqrvx@101.175.150.247) (Ping timeout: 260 seconds)
2025-04-10 14:44:39 +0200bcksl(~bcksl@user/bcksl) bcksl
2025-04-10 14:45:13 +0200zlqrvx(~zlqrvx@2001:8003:8c8b:e00:374a:bdcb:457c:d1e3)
2025-04-10 14:49:13 +0200end(~end@user/end/x-0094621) end^
2025-04-10 14:53:12 +0200vpan(~vpan@212.117.1.172) (Quit: Leaving.)
2025-04-10 15:00:36 +0200cstml(~Thunderbi@user/cstml) cstml
2025-04-10 15:01:39 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds)
2025-04-10 15:05:09 +0200hattckory(~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 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2025-04-10 15:14:04 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-10 15:15:22 +0200j1n37(~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 +0200fp(~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 +0200notdabs(~Owner@2600:1700:69cf:9000:3895:739f:4247:f37f)
2025-04-10 15:30:39 +0200sprotte24_(~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de)
2025-04-10 15:31:03 +0200fp(~Thunderbi@2001:708:150:10::1d80) (Ping timeout: 268 seconds)
2025-04-10 15:32:13 +0200shreyasminocha_(51fdc93eda@user/shreyasminocha) shreyasminocha
2025-04-10 15:32:15 +0200ggb_(a62ffbaf4f@2a03:6000:1812:100::3ac)
2025-04-10 15:32:15 +0200smiesner_(b0cf5acf8c@2a03:6000:1812:100::13b9)
2025-04-10 15:32:15 +0200sm2n_(ae95cb1267@user/sm2n) sm2n
2025-04-10 15:32:15 +0200raghavgururajan_(ea769b8000@user/raghavgururajan) raghavgururajan
2025-04-10 15:32:16 +0200simendsjo_(34b0550437@2a03:6000:1812:100::1441) simendsjo
2025-04-10 15:32:16 +0200arcadewise_(52968ed80d@2a03:6000:1812:100::3df) l3gacyb3ta
2025-04-10 15:32:16 +0200probie_(cc0b34050a@user/probie) probie
2025-04-10 15:32:16 +0200ymherklotz_(cb2c9cfbdd@2a03:6000:1812:100::29a) ymherklotz
2025-04-10 15:32:16 +0200ursa-major_(114efe6c39@2a03:6000:1812:100::11f3) ursa-major
2025-04-10 15:32:17 +0200duncan__(c6181279e3@user/meow/duncan) duncan
2025-04-10 15:32:18 +0200op_4_(~tslil@2a01:4f8:c0c:7952::1)
2025-04-10 15:32:18 +0200samhh__(7569f027cf@2a03:6000:1812:100::e4) samhh
2025-04-10 15:32:19 +0200sefidel_(~sefidel@user/sefidel) sefidel
2025-04-10 15:32:19 +0200j0lol_(~j0lol@132.145.17.236) j0lol
2025-04-10 15:32:19 +0200saolsen_(sid26430@id-26430.lymington.irccloud.com) saolsen
2025-04-10 15:32:44 +0200hamishmack_(sid389057@id-389057.hampstead.irccloud.com) hamishmack
2025-04-10 15:32:51 +0200bgamari_(~bgamari@64.223.225.174)
2025-04-10 15:32:54 +0200cptaffe`(~cptaffe@user/cptaffe) cptaffe
2025-04-10 15:33:02 +0200vgtw_(~vgtw@user/vgtw) vgtw
2025-04-10 15:33:59 +0200cstml(~Thunderbi@user/cstml) (Quit: cstml)
2025-04-10 15:35:17 +0200milan2(~milan@88.212.61.169)
2025-04-10 15:35:29 +0200inedia_(~irc@2600:3c00:e000:287::1)
2025-04-10 15:35:34 +0200kst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 15:35:41 +0200mima_(~mmh@user/mima) mima
2025-04-10 15:35:46 +0200_[_________]_(~oos95GWG@user/oos95GWG) oos95GWG
2025-04-10 15:36:22 +0200abrar_(~abrar@static-96-245-187-163.phlapa.fios.verizon.net)
2025-04-10 15:36:31 +0200aforemny_(~aforemny@2001:9e8:6cd3:ed00:7f35:da5a:93ab:c3e3) aforemny
2025-04-10 15:37:02 +0200mal1(~mal@ns2.wyrd.be) lieven
2025-04-10 15:37:14 +0200darrik(~natch@c-92-34-7-158.bbcust.telenor.se)
2025-04-10 15:37:28 +0200ystael(~ystael@user/ystael) ystael
2025-04-10 15:40:08 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (*.net *.split)
2025-04-10 15:40:08 +0200TMA(tma@twin.jikos.cz) (*.net *.split)
2025-04-10 15:40:08 +0200sprotte24(~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) (*.net *.split)
2025-04-10 15:40:09 +0200aforemny(~aforemny@i59F4C778.versanet.de) (*.net *.split)
2025-04-10 15:40:09 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (*.net *.split)
2025-04-10 15:40:09 +0200Natch(~natch@c-92-34-7-158.bbcust.telenor.se) (*.net *.split)
2025-04-10 15:40:09 +0200cptaffe(~cptaffe@user/cptaffe) (*.net *.split)
2025-04-10 15:40:09 +0200rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-15-174-95-4-83.dsl.bell.ca) (*.net *.split)
2025-04-10 15:40:09 +0200milan(~milan@88.212.61.169) (*.net *.split)
2025-04-10 15:40:09 +0200op_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 +0200samhh_(7569f027cf@2a03:6000:1812:100::e4) (*.net *.split)
2025-04-10 15:40:09 +0200raghavgururajan(ea769b8000@user/raghavgururajan) (*.net *.split)
2025-04-10 15:40:10 +0200duncan(c6181279e3@user/meow/duncan) (*.net *.split)
2025-04-10 15:40:10 +0200ursa-major(114efe6c39@2a03:6000:1812:100::11f3) (*.net *.split)
2025-04-10 15:40:10 +0200sm2n(ae95cb1267@user/sm2n) (*.net *.split)
2025-04-10 15:40:10 +0200probie(cc0b34050a@user/probie) (*.net *.split)
2025-04-10 15:40:10 +0200shreyasminocha(51fdc93eda@user/shreyasminocha) (*.net *.split)
2025-04-10 15:40:11 +0200simendsjo(34b0550437@2a03:6000:1812:100::1441) (*.net *.split)
2025-04-10 15:40:11 +0200arcadewise(52968ed80d@2a03:6000:1812:100::3df) (*.net *.split)
2025-04-10 15:40:11 +0200exfalsoquodlibet(a7085e0f71@2a03:6000:1812:100::13a3) (*.net *.split)
2025-04-10 15:40:11 +0200ymherklotz(cb2c9cfbdd@2a03:6000:1812:100::29a) (*.net *.split)
2025-04-10 15:40:11 +0200smiesner(b0cf5acf8c@user/smiesner) (*.net *.split)
2025-04-10 15:40:11 +0200ggb(a62ffbaf4f@2a03:6000:1812:100::3ac) (*.net *.split)
2025-04-10 15:40:11 +0200abrar(~abrar@static-96-245-187-163.phlapa.fios.verizon.net) (*.net *.split)
2025-04-10 15:40:11 +0200vgtw(~vgtw@user/vgtw) (*.net *.split)
2025-04-10 15:40:11 +0200j0lol(~j0lol@132.145.17.236) (*.net *.split)
2025-04-10 15:40:12 +0200acidsys(~crameleon@openSUSE/member/crameleon) (*.net *.split)
2025-04-10 15:40:12 +0200saolsen(sid26430@id-26430.lymington.irccloud.com) (*.net *.split)
2025-04-10 15:40:12 +0200hammond(proscan@gateway04.insomnia247.nl) (*.net *.split)
2025-04-10 15:40:12 +0200bgamari(~bgamari@64.223.225.174) (*.net *.split)
2025-04-10 15:40:12 +0200inedia(~irc@2600:3c00:e000:287::1) (*.net *.split)
2025-04-10 15:40:12 +0200sefidel(~sefidel@user/sefidel) (*.net *.split)
2025-04-10 15:40:12 +0200_koolazer(~koo@user/koolazer) (*.net *.split)
2025-04-10 15:40:13 +0200bastelfreak(bastelfrea@libera/staff/VoxPupuli.bastelfreak) (*.net *.split)
2025-04-10 15:40:13 +0200lieven(~mal@ns2.wyrd.be) (*.net *.split)
2025-04-10 15:40:13 +0200mima(~mmh@user/mima) (*.net *.split)
2025-04-10 15:40:13 +0200hamishmack(sid389057@id-389057.hampstead.irccloud.com) (*.net *.split)
2025-04-10 15:40:13 +0200duncan__duncan
2025-04-10 15:40:13 +0200ggb_ggb
2025-04-10 15:40:13 +0200hamishmack_hamishmack
2025-04-10 15:40:13 +0200shreyasminocha_shreyasminocha
2025-04-10 15:40:13 +0200darrikNatch
2025-04-10 15:40:13 +0200cptaffe`cptaffe
2025-04-10 15:40:14 +0200smiesner_smiesner
2025-04-10 15:40:14 +0200ymherklotz_ymherklotz
2025-04-10 15:40:14 +0200arcadewise_arcadewise
2025-04-10 15:40:14 +0200simendsjo_simendsjo
2025-04-10 15:40:14 +0200probie_probie
2025-04-10 15:40:14 +0200saolsen_saolsen
2025-04-10 15:40:14 +0200op_4_op_4
2025-04-10 15:40:14 +0200sefidel_sefidel
2025-04-10 15:40:14 +0200raghavgururajan_raghavgururajan
2025-04-10 15:40:14 +0200sm2n_sm2n
2025-04-10 15:40:14 +0200ursa-major_ursa-major
2025-04-10 15:40:15 +0200j0lol_j0lol
2025-04-10 15:40:37 +0200lortabac(~lortabac@88-125-6-227.subs.proxad.net) lortabac
2025-04-10 15:42:55 +0200tavare(~tavare@user/tavare) tavare
2025-04-10 15:42:58 +0200tavare(~tavare@user/tavare) (Remote host closed the connection)
2025-04-10 15:43:54 +0200TMA(tma@twin.jikos.cz) TMA
2025-04-10 15:45:51 +0200koolazer(~koo@user/koolazer) koolazer
2025-04-10 15:46:26 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 15:46:38 +0200bastelfreak(bastelfrea@libera/staff/VoxPupuli.bastelfreak) bastelfreak
2025-04-10 15:47:02 +0200acidsys(~crameleon@openSUSE/member/crameleon) crameleon
2025-04-10 15:47:53 +0200exfalsoquodlibet(a7085e0f71@2a03:6000:1812:100::13a3)
2025-04-10 15:51:14 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds)
2025-04-10 15:54:56 +0200lisbeths(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 +0200weary-traveler(~user@user/user363627) user363627
2025-04-10 16:25:17 +0200amadaluzia(~amadaluzi@user/amadaluzia) amadaluzia
2025-04-10 16:27:33 +0200Square(~Square4@user/square) Square
2025-04-10 16:33:43 +0200Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2025-04-10 16:34:13 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
2025-04-10 16:34:45 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
2025-04-10 16:38:25 +0200hattckory(~hattckory@70.27.118.207)
2025-04-10 16:43:09 +0200hattckory(~hattckory@70.27.118.207) (Ping timeout: 260 seconds)
2025-04-10 16:44:44 +0200notdabs(~Owner@2600:1700:69cf:9000:3895:739f:4247:f37f) (Read error: Connection reset by peer)
2025-04-10 16:48:08 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-10 16:48:38 +0200notdabs(~Owner@2600:1700:69cf:9000:a504:86ce:5139:ec16)
2025-04-10 16:49:18 +0200milan2(~milan@88.212.61.169) (Quit: WeeChat 4.4.3)
2025-04-10 16:50:05 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 16:50:56 +0200Feuermagier(~Feuermagi@user/feuermagier) (Quit: Leaving)
2025-04-10 16:52:47 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-10 16:56:09 +0200Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2025-04-10 17:02:15 +0200Feuermagier(~Feuermagi@user/feuermagier) (Quit: Leaving)
2025-04-10 17:07:36 +0200lortabac(~lortabac@88-125-6-227.subs.proxad.net) (Quit: WeeChat 4.5.2)
2025-04-10 17:11:21 +0200Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2025-04-10 17:13:51 +0200ColinRobinson(~juan@user/JuanDaugherty) JuanDaugherty
2025-04-10 17:20:12 +0200marinelli(~weechat@gateway/tor-sasl/marinelli) marinelli
2025-04-10 17:20:49 +0200acidjnk(~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2025-04-10 17:30:03 +0200hammond(proscan@gateway04.insomnia247.nl)
2025-04-10 17:34:08 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 17:46:29 +0200ColinRobinsonJuanDaugherty
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 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-04-10 17:54:25 +0200chele(~chele@user/chele) (Remote host closed the connection)
2025-04-10 17:55:24 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-10 17:55:54 +0200amadaluzia_(~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012)
2025-04-10 17:57:15 +0200JuanDaughertyColinRobinson
2025-04-10 18:00:31 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2025-04-10 18:01:01 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-10 18:05:37 +0200ColinRobinsonJuanDaugherty
2025-04-10 18:08:35 +0200GdeVolpiano(~GdeVolpia@user/GdeVolpiano) (Ping timeout: 252 seconds)
2025-04-10 18:09:30 +0200GdeVolpiano(~GdeVolpia@user/GdeVolpiano) GdeVolpiano
2025-04-10 18:23:32 +0200JuanDaughertyColinRobinson
2025-04-10 18:26:20 +0200ft(~ft@p508db594.dip0.t-ipconnect.de) ft
2025-04-10 18:36:16 +0200sayurc(~sayurc@169.150.203.34) sayurc
2025-04-10 18:38:02 +0200acidjnk(~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 +0200Feuermagier(~Feuermagi@user/feuermagier) (Quit: Leaving)
2025-04-10 18:51:11 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-04-10 18:52:49 +0200Sgeo(~Sgeo@user/sgeo) Sgeo
2025-04-10 18:54:45 +0200L29Ah(~L29Ah@wikipedia/L29Ah) (Ping timeout: 248 seconds)
2025-04-10 18:57:08 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh
2025-04-10 18:57:27 +0200Square2(~Square@user/square) Square
2025-04-10 19:01:30 +0200Square(~Square4@user/square) (Ping timeout: 252 seconds)
2025-04-10 19:01:30 +0200amadaluzia(~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds)
2025-04-10 19:01:37 +0200merijn(~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 +0200tabaqui(~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 +0200pavonia(~user@user/siracusa) siracusa
2025-04-10 19:09:16 +0200Feuermagier(~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 +0200kimiamania9(~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 +0200kimiamania(~65804703@user/kimiamania) (Read error: Connection reset by peer)
2025-04-10 19:13:04 +0200kimiamania9kimiamania
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 +0200acidjnk(~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 +0200ColinRobinson(~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 +0200merijn(~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 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 19:21:44 +0200ski. 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 +0200YoungFrog(~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 +0200sayurc(~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 +0200merijn(~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 +0200acidjnk(~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 +0200merijn(~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 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
2025-04-10 19:39:52 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
2025-04-10 19:40:23 +0200peterbecich(~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 +0200sayurc(~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 +0200merijn(~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 +0200Flow(~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 +0200merijn(~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 +0200ski. 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 +0200merijn(~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 +0200merijn(~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 +0200fantom(~fantom@2.219.56.221)
2025-04-10 20:16:21 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-10 20:16:42 +0200ski. 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 +0200ski. 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 +0200ski. 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 +0200target_i(~target_i@user/target-i/x-6023099) target_i
2025-04-10 20:20:02 +0200j1n37(~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 +0200merijn(~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 +0200gmg(~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 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855)
2025-04-10 20:25:34 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) (Changing host)
2025-04-10 20:25:34 +0200XZDX(~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 +0200merijn(~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 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-04-10 20:31:26 +0200ski. 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 +0200bsima(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 20:37:37 +0200frosthaern(~frosthaer@2406:7400:116:ac19:3f62:4a05:5a1d:7cdc)
2025-04-10 20:37:45 +0200ski. 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 +0200frosthaern(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-10 20:43:11 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
2025-04-10 20:43:27 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
2025-04-10 20:45:40 +0200monochromwould 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 +0200weary-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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 20:57:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 21:00:02 +0200caconym(~caconym@user/caconym) (Quit: bye)
2025-04-10 21:00:45 +0200caconym(~caconym@user/caconym) caconym
2025-04-10 21:03:52 +0200michalz(~michalz@185.246.207.221) (Remote host closed the connection)
2025-04-10 21:08:01 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2025-04-10 21:09:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 21:12:06 +0200cheater(~Username@user/cheater) (Ping timeout: 244 seconds)
2025-04-10 21:14:48 +0200chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2025-04-10 21:15:17 +0200cheater(~Username@user/cheater) cheater
2025-04-10 21:15:24 +0200chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-04-10 21:16:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 21:17:41 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 21:18:10 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds)
2025-04-10 21:19:22 +0200feetwind(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-10 21:22:45 +0200XZDX(~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 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-10 21:27:20 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-10 21:33:28 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-04-10 21:39:20 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-04-10 21:41:26 +0200sabathan2(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-04-10 21:44:47 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-04-10 21:45:43 +0200rbdr(~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de)
2025-04-10 21:49:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 21:51:20 +0200Feuermagier(~Feuermagi@user/feuermagier) (Quit: Leaving)
2025-04-10 21:51:20 +0200peterbecich(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 21:55:16 +0200notdabs(~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 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 21:58:41 +0200weary-traveler(~user@user/user363627) user363627
2025-04-10 21:59:59 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855)
2025-04-10 22:00:21 +0200alp(~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 +0200rbdr(~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) (Quit: rbdr)
2025-04-10 22:03:33 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) (Changing host)
2025-04-10 22:03:33 +0200XZDX(~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 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds)
2025-04-10 22:10:33 +0200rbdr(~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 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-04-10 22:12:56 +0200Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2025-04-10 22:14:03 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Quit: Leaving)
2025-04-10 22:14:06 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-04-10 22:14:08 +0200gmg(~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 +0200hattckory(~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 +0200merijn(~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 +0200merijn(~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 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
2025-04-10 22:28:17 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
2025-04-10 22:28:18 +0200biberu(~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 +0200bliminse(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 22:34:05 +0200amadaluzia_(~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) (Changing host)
2025-04-10 22:34:05 +0200amadaluzia_(~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 +0200bliminse(~bliminse@user/bliminse) bliminse
2025-04-10 22:35:04 +0200CiaoSen(~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 +0200merijn(~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 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed)
2025-04-10 22:40:31 +0200Googulator(~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu)
2025-04-10 22:42:29 +0200tromp(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 22:47:54 +0200myme(~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 +0200myme(~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 +0200merijn(~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 +0200amadaluzia_(~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 +0200amadaluzia(~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 +0200amadaluzia(~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) (Remote host closed the connection)
2025-04-10 22:53:52 +0200amadaluzia(~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 +0200Guest87(~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 +0200merijn(~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 +0200amadaluzia(~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 +0200inca(~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 +0200amadaluzia(~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 +0200enoq(~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 +0200merijn(~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 +0200amadaluzia(~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 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 23:11:33 +0200 <enoq> like applicativeMap instead of <*>
2025-04-10 23:11:42 +0200 <EvanR> it's not a map
2025-04-10 23:11:48 +0200 <enoq> or just applicative
2025-04-10 23:11:53 +0200 <__monty__> `ap` no?
2025-04-10 23:11:58 +0200 <haskellbridge> <loonycyborg> can just put functions in `` and use them as operators
2025-04-10 23:11:58 +0200 <EvanR> ap exists
2025-04-10 23:12:14 +0200 <haskellbridge> <loonycyborg> "asTypeOf" etc :P
2025-04-10 23:12:15 +0200 <monochrom> I don't get why people want English/words for coding. But that's none of my business. My business though is to remind them that they can always go back to COBOL.
2025-04-10 23:12:55 +0200 <enoq> no need to pick either extreme
2025-04-10 23:13:14 +0200 <EvanR> but pure f `ap` x `ap` y `ap` z has the issue of annoying people who read it, which might be the real issue
2025-04-10 23:13:28 +0200 <EvanR> also in cobol
2025-04-10 23:13:35 +0200 <int-e> monochrom: isn't the lesson that we've learned from COBOL that learning a programming language's syntax does not get easier when it uses words
2025-04-10 23:13:36 +0200 <monochrom> Haskell is already neither extreme.
2025-04-10 23:14:12 +0200 <int-e> and the programs don't become more readable either
2025-04-10 23:14:16 +0200 <enoq> yeah, I guess you could say APL is even worse
2025-04-10 23:14:40 +0200 <monochrom> We are like "mod 5 3" which is even more wordy than C.
2025-04-10 23:14:59 +0200 <EvanR> (other than maybe lens) and library might introduce an operator, and then "don't use this library because there is someone who doesn't know this operator" would mean you can't use most programming languages
2025-04-10 23:15:03 +0200 <haskellbridge> <loonycyborg> one most unusual choice is use of space for function application instead of more common (x,y..)
2025-04-10 23:15:04 +0200 <int-e> or 5 `mod` 3
2025-04-10 23:15:08 +0200 <Guest87> int-e Oh I guess that's true. But let's say that's intentional but I want `extendEnv "v" 1 (extendEnv "v" 2 makeEnv)` to be indistinguishable from `extendEnv "v" ` makeEnv`. Is there an easy way to do that?
2025-04-10 23:15:14 +0200 <EvanR> but that issue exists for non-operators
2025-04-10 23:15:21 +0200 <__monty__> 5 `mod` 3 is arguably more readable IMO.