Logs on 2025-04-10 (liberachat/#haskell)
| 00:03:10 | × | jespada quits (~jespada@r190-133-30-51.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
| 00:08:08 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:11:52 | × | krjst quits (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye) |
| 00:12:13 | → | krjst joins (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) |
| 00:13:05 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 00:21:38 | × | acidjnk_new3 quits (~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 00:22:22 | → | acidjnk_new3 joins (~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) |
| 00:23:55 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 00:23:56 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:25:18 | × | poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 276 seconds) |
| 00:26:16 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 00:28:37 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 00:31:02 | × | polyphem quits (~rod@p4fc2cdf8.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 00:31:05 | <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). |
| 00:31:22 | <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. |
| 00:31:29 | <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.) |
| 00:31:45 | <EvanR> | lol |
| 00:32:29 | <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 |
| 00:32:32 | <haskellbridge> | <Morj> I call it Morj's law |
| 00:38:01 | → | poscat joins (~poscat@user/poscat) |
| 00:39:25 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 00:39:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:45:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 00:45:35 | × | notdabs quits (~Owner@2600:1700:69cf:9000:19b2:995a:60d5:3b93) (Quit: Leaving) |
| 00:53:09 | × | xff0x quits (~xff0x@2405:6580:b080:900:b50:e5e9:27c3:86) (Ping timeout: 248 seconds) |
| 00:55:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:55:49 | × | foul_owl quits (~kerry@94.156.149.99) (Ping timeout: 248 seconds) |
| 00:58:09 | × | otto_s quits (~user@p4ff27c58.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 01:00:05 | → | otto_s joins (~user@p4ff278a2.dip0.t-ipconnect.de) |
| 01:01:03 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 01:03:56 | → | acidjnk_new joins (~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de) |
| 01:05:53 | × | acidjnk_new3 quits (~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 01:06:42 | → | foul_owl joins (~kerry@174-21-146-90.tukw.qwest.net) |
| 01:08:43 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 01:13:42 | → | j1n37- joins (~j1n37@user/j1n37) |
| 01:13:56 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 01:21:07 | → | tavare joins (~tavare@150.129.88.189) |
| 01:21:07 | × | tavare quits (~tavare@150.129.88.189) (Changing host) |
| 01:21:07 | → | tavare joins (~tavare@user/tavare) |
| 01:25:05 | × | acidjnk_new quits (~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 01:26:27 | × | foul_owl quits (~kerry@174-21-146-90.tukw.qwest.net) (Ping timeout: 265 seconds) |
| 01:27:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:28:54 | × | ezzieygu1wuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 246 seconds) |
| 01:30:39 | × | aforemny_ quits (~aforemny@i59F4C56B.versanet.de) (Ping timeout: 244 seconds) |
| 01:31:24 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 01:32:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 01:32:37 | <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 |
| 01:36:18 | → | Square joins (~Square4@user/square) |
| 01:37:13 | × | weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!) |
| 01:37:29 | → | weary-traveler joins (~user@user/user363627) |
| 01:39:08 | × | Square2 quits (~Square@user/square) (Ping timeout: 245 seconds) |
| 01:40:19 | → | foul_owl joins (~kerry@94.156.149.91) |
| 01:42:54 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:47:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 01:50:08 | → | aforemny joins (~aforemny@i59F4C778.versanet.de) |
| 01:50:13 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 01:58:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:03:27 | <haskellbridge> | <Bowuigi> EvanR in HoTT the unit type is denoted as mathbb{1} and its inhabitant is denoted * (or with a star) |
| 02:03:43 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 02:04:28 | <haskellbridge> | <Bowuigi> If you want something convention independent just ask for the limit/adjunction version of those constructs |
| 02:05:18 | × | tessier quits (~tessier@ip68-8-117-219.sd.sd.cox.net) (Ping timeout: 272 seconds) |
| 02:05:30 | <EvanR> | yes I saw that in HoTT |
| 02:06:26 | → | tessier joins (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 02:06:47 | <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) |
| 02:06:55 | <EvanR> | 𝟙 |
| 02:08:13 | <haskellbridge> | <Bowuigi> Yes, the boolean type is mathbb{2} and in general any type with exactly N elements is denoted mathbb{N} |
| 02:14:26 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:16:32 | → | slack1256 joins (~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) |
| 02:16:48 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
| 02:17:51 | <slack1256> | Has anyone used tsvector in persistent ? |
| 02:17:58 | <slack1256> | How do you declare in as a datatype? |
| 02:18:50 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 02:21:00 | → | ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com) |
| 02:24:54 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 276 seconds) |
| 02:26:49 | <monochrom> | EvanR: Interesting, I have always thought of it as == preserves function application, but the other round is just as valid. |
| 02:26:54 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 02:29:48 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:29:57 | → | j1n37 joins (~j1n37@user/j1n37) |
| 02:31:13 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 02:34:06 | × | stef204 quits (~stef204@user/stef204) (Quit: WeeChat 4.2.1) |
| 02:35:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 02:37:02 | × | slack1256 quits (~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) (Remote host closed the connection) |
| 02:45:34 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:46:14 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
| 02:47:39 | <EvanR> | I got that off stanford.edu on the topic of lambda calculus |
| 02:48:03 | <EvanR> | where it describes eta conversion as "= preserving application and abstraction" |
| 02:50:29 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 03:01:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:06:07 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 03:17:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:18:10 | × | tamer quits (~tamer@user/tamer) (Read error: Connection reset by peer) |
| 03:22:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 03:32:23 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 03:32:53 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:34:23 | <haskellbridge> | <Liamzee> curious, have people built a linear lens system for vector yet? IIRC, there was something about that on Bartosz Milewski's site |
| 03:34:25 | <haskellbridge> | <Liamzee> https://bartoszmilewski.com/2024/02/07/linear-lenses-in-haskell/ |
| 03:34:29 | → | tamer joins (~tamer@5.2.74.82) |
| 03:37:53 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 03:41:02 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:48:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:50:14 | → | zlqrvx_ joins (~zlqrvx@101.175.150.247) |
| 03:51:15 | × | zlqrvx quits (~zlqrvx@101.175.150.247) (Read error: Connection reset by peer) |
| 03:54:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 03:57:56 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 04:01:16 | → | bitdex_ joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:01:24 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 04:04:03 | × | whez quits (uid470288@id-470288.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:04:27 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:09:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 04:09:14 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 04:10:50 | <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 |
| 04:12:26 | → | michalz joins (~michalz@185.246.207.201) |
| 04:20:15 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:23:05 | × | bitdex_ quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 04:23:28 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:25:18 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 04:31:13 | × | sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
| 04:36:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:38:41 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
| 04:41:14 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 04:43:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:49:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 04:58:47 | → | hattckory joins (~hattckory@70.27.118.207) |
| 04:59:16 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:03:54 | × | hattckory quits (~hattckory@70.27.118.207) (Ping timeout: 260 seconds) |
| 05:04:29 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 05:10:35 | → | Square2 joins (~Square@user/square) |
| 05:12:42 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:14:34 | × | Square quits (~Square4@user/square) (Ping timeout: 260 seconds) |
| 05:15:02 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:15:42 | → | sayurc joins (~sayurc@169.150.203.34) |
| 05:17:16 | × | amadaluzia quits (~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.) |
| 05:19:15 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 05:19:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 05:20:47 | × | ryanbooker quits (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 05:23:29 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
| 05:26:45 | → | amadaluzia joins (~amadaluzi@user/amadaluzia) |
| 05:30:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:33:48 | × | michalz quits (~michalz@185.246.207.201) (Quit: ZNC 1.9.1 - https://znc.in) |
| 05:34:06 | → | michalz joins (~michalz@185.246.207.201) |
| 05:36:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 05:37:11 | × | michalz quits (~michalz@185.246.207.201) (Client Quit) |
| 05:37:34 | → | michalz joins (~michalz@185.246.207.221) |
| 05:38:18 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 05:46:08 | <haskellbridge> | <hellwolf> why did i not know this is a valid syntax |
| 05:46:08 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/wUEaSQWmEwGlroXOCJYXuzhL/7ofVWvhpwhM (3 lines) |
| 05:46:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:51:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 05:59:47 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 06:05:15 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
| 06:05:28 | <Leary> | hellwolf: https://play.haskell.org/saved/bRThmTVI |
| 06:05:56 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 06:07:08 | <haskellbridge> | <hellwolf> what about that? |
| 06:07:31 | <Leary> | Also: https://play.haskell.org/saved/ObeWDdIa |
| 06:07:58 | <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. |
| 06:08:49 | × | Square2 quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 06:11:15 | <haskellbridge> | <hellwolf> your first one can still work without any extension. but perhaps because it was enabled by default in ghc2021. |
| 06:11:16 | <haskellbridge> | the second one is interesting |
| 06:12:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:12:27 | <mauke> | fucking playground |
| 06:12:37 | <mauke> | how do I get it top stop hijacking Ctrl-L? |
| 06:13:53 | <haskellbridge> | <hellwolf> vibe code and send PR to tom :p |
| 06:16:16 | <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. |
| 06:16:54 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 06:16:55 | × | foul_owl quits (~kerry@94.156.149.91) (Ping timeout: 268 seconds) |
| 06:17:35 | <mauke> | https://www.haskell.org/hugs/pages/users_guide/type-annotations.html |
| 06:20:14 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 06:21:12 | <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 |
| 06:22:18 | <haskellbridge> | <hellwolf> what is STV? |
| 06:22:33 | × | jmcantrell quits (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.0) |
| 06:22:33 | jmcantrell_ | is now known as jmcantrell |
| 06:22:49 | <Leary> | ScopedTypeVariables. It simply isn't intended to replace top-level type signatures. |
| 06:23:22 | <haskellbridge> | <hellwolf> now it starts to make sense, it's a pattern matching. |
| 06:23:22 | <haskellbridge> | So if I run it through the TH, it would show the right syntax constructor and makes sense. |
| 06:24:04 | <haskellbridge> | <hellwolf> it was an illusion that it looked like a type declaration |
| 06:24:13 | <haskellbridge> | <hellwolf> but it had nothing to do with it. |
| 06:24:19 | <haskellbridge> | <hellwolf> i get it now. thanks for explaining. |
| 06:27:39 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:28:51 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 06:31:00 | → | foul_owl joins (~kerry@94.156.149.97) |
| 06:32:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 06:37:57 | × | inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 246 seconds) |
| 06:42:58 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 06:43:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:47:44 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
| 06:48:07 | × | ft quits (~ft@p508db594.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:48:21 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 06:50:37 | → | tromp joins (~textual@2001:1c00:3487:1b00:44ed:cdbe:8e8e:71c5) |
| 06:51:52 | → | inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
| 06:57:11 | × | inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 244 seconds) |
| 06:57:16 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 06:59:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:00:04 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 07:01:03 | → | caconym joins (~caconym@user/caconym) |
| 07:03:09 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 07:04:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 07:05:20 | → | inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
| 07:08:33 | <[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? |
| 07:08:48 | <[exa]> | In particular I've got this thing here with accelerate-llvm: https://paste.tomsmeding.com/GbdNItS1 |
| 07:09:02 | <[exa]> | somehow I can't even trace how ghc comes to executing the C source |
| 07:15:06 | × | remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Ping timeout: 252 seconds) |
| 07:15:44 | × | TMA quits (tma@twin.jikos.cz) (Ping timeout: 260 seconds) |
| 07:18:18 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds) |
| 07:18:26 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 07:19:12 | → | vpan joins (~vpan@212.117.1.172) |
| 07:19:50 | Lord_of_Life_ | is now known as Lord_of_Life |
| 07:23:03 | <[exa]> | (nvm, opened an issue here if someone's interested in poking in that https://github.com/AccelerateHS/accelerate-llvm/issues/102 ) |
| 07:23:53 | → | remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz) |
| 07:29:41 | → | chele joins (~chele@user/chele) |
| 07:35:37 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:36:43 | → | acidjnk joins (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) |
| 07:39:43 | × | XZDX quits (~xzdx@user/XZDX) (Remote host closed the connection) |
| 07:40:00 | → | XZDX joins (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) |
| 07:41:08 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:45:38 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 07:49:38 | → | merijn joins (~merijn@77.242.116.146) |
| 07:53:30 | → | fp joins (~Thunderbi@2001:708:20:1406::1370) |
| 07:53:45 | ski | . o O ( "Interview with Vibe Coder in 2025" <https://www.youtube.com/watch?v=JeNS1ZNHQs8> ) |
| 07:57:30 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 08:04:33 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
| 08:19:15 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 08:20:12 | × | XZDX quits (~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Remote host closed the connection) |
| 08:25:23 | × | forell quits (~forell@user/forell) (Quit: ZNC - https://znc.in) |
| 08:26:40 | → | forell joins (~forell@user/forell) |
| 08:37:58 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds) |
| 08:45:12 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:48:21 | → | sprotte24 joins (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) |
| 08:48:53 | × | sprotte24 quits (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) (Client Quit) |
| 08:53:51 | × | sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
| 08:56:50 | → | alp joins (~alp@2001:861:8ca0:4940:e00c:8d19:d96b:e8b0) |
| 08:59:35 | → | poxel joins (~lennart@user/poxel) |
| 09:02:20 | × | poxel quits (~lennart@user/poxel) (Client Quit) |
| 09:02:24 | × | Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
| 09:02:39 | → | poxel joins (~poxel@user/poxel) |
| 09:02:44 | → | Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
| 09:08:04 | × | olivial quits (~benjaminl@user/benjaminl) (Read error: Connection reset by peer) |
| 09:08:20 | → | olivial joins (~benjaminl@user/benjaminl) |
| 09:11:16 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 09:17:09 | → | Guest71 joins (~Guest75@37.204.222.118) |
| 09:19:58 | × | poxel quits (~poxel@user/poxel) (Quit: WeeChat 4.6.0) |
| 09:20:18 | → | poxel joins (~poxel@user/poxel) |
| 09:31:42 | × | Guest71 quits (~Guest75@37.204.222.118) (Ping timeout: 240 seconds) |
| 09:34:52 | × | fp quits (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 268 seconds) |
| 09:36:28 | <yin> | any news on the plan to make base versions independent from ghc versions? |
| 09:39:57 | × | hsw quits (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) (Ping timeout: 246 seconds) |
| 09:45:32 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 09:46:30 | → | hsw joins (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) |
| 09:46:36 | → | sprotte24 joins (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) |
| 09:56:46 | × | lambdap2371 quits (~lambdap@static.167.190.119.168.clients.your-server.de) (Quit: Ping timeout (120 seconds)) |
| 09:57:01 | → | lambdap2371 joins (~lambdap@static.167.190.119.168.clients.your-server.de) |
| 10:00:31 | <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? ( |
| 10:00:39 | <int-e> | yin: is that what ghc-internal is about? |
| 10:03:55 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 10:04:38 | → | __monty__ joins (~toonn@user/toonn) |
| 10:05:01 | <kqr> | Update on result type: indeed, foldr const defaultValue does what I need. |
| 10:08:59 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 260 seconds) |
| 10:12:43 | <yin> | int-e: not sure. i recall having that conversation here but details elude me |
| 10:13:58 | <yin> | maybe something discussed here https://discourse.haskell.org/t/a-different-approach-to-emancipating-base/5695/6 |
| 10:24:45 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds) |
| 10:31:09 | × | poxel quits (~poxel@user/poxel) (Quit: WeeChat 4.6.0) |
| 10:31:29 | → | poxel joins (~weechat@user/poxel) |
| 10:32:04 | × | poxel quits (~weechat@user/poxel) (Client Quit) |
| 10:32:23 | → | poxel joins (~poxel@user/poxel) |
| 10:37:18 | <yin> | separating ghc.base from base |
| 10:49:53 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
| 10:55:39 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 10:56:36 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 11:00:04 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 11:00:27 | × | acidjnk quits (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 11:02:12 | → | caconym joins (~caconym@user/caconym) |
| 11:02:14 | → | jespada joins (~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) |
| 11:04:42 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 11:07:38 | → | TMA joins (tma@twin.jikos.cz) |
| 11:08:12 | → | jacopovalanzano joins (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) |
| 11:09:59 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:11:59 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
| 11:15:31 | → | j1n37- joins (~j1n37@user/j1n37) |
| 11:15:40 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 272 seconds) |
| 11:23:40 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 11:25:13 | → | xff0x joins (~xff0x@2405:6580:b080:900:1c0d:6c97:349e:6228) |
| 11:30:09 | → | tabaqui joins (~tabaqui@167.71.80.236) |
| 11:34:09 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
| 11:34:51 | × | amadaluzia quits (~amadaluzi@user/amadaluzia) (Remote host closed the connection) |
| 11:35:33 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 11:57:33 | × | walt quits (~ggVGc@a.lowtech.earth) (Ping timeout: 276 seconds) |
| 11:57:55 | → | walt joins (~ggVGc@a.lowtech.earth) |
| 12:03:34 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 12:09:52 | × | bcksl quits (~bcksl@user/bcksl) (Quit: \) |
| 12:09:52 | × | end quits (~end@user/end/x-0094621) (Quit: end) |
| 12:13:58 | × | jespada quits (~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) (Ping timeout: 268 seconds) |
| 12:14:33 | → | acidjnk joins (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) |
| 12:16:29 | → | jespada joins (~jespada@r179-25-43-11.dialup.adsl.anteldata.net.uy) |
| 12:20:23 | × | Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
| 12:20:43 | → | Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
| 12:41:18 | × | jacopovalanzano quits (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Ping timeout: 240 seconds) |
| 12:43:44 | × | zlqrvx_ quits (~zlqrvx@101.175.150.247) (Ping timeout: 260 seconds) |
| 12:44:39 | → | bcksl joins (~bcksl@user/bcksl) |
| 12:45:13 | → | zlqrvx joins (~zlqrvx@2001:8003:8c8b:e00:374a:bdcb:457c:d1e3) |
| 12:49:13 | → | end joins (~end@user/end/x-0094621) |
| 12:53:12 | × | vpan quits (~vpan@212.117.1.172) (Quit: Leaving.) |
| 13:00:36 | → | cstml joins (~Thunderbi@user/cstml) |
| 13:01:39 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds) |
| 13:05:09 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
| 13:07:30 | <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? |
| 13:07:47 | <hellwolf> | E.g. split it into Dict @(n == 0) and Dict @(1 <= n) |
| 13:08:14 | <hellwolf> | I could write myself, use unsafeAxiom, but I am wondering if this is common enough of a utility to appear somewhere. |
| 13:11:19 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:14:04 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 13:15:22 | → | j1n37 joins (~j1n37@user/j1n37) |
| 13:19:43 | <merijn> | yin: It hasn't happened in the past decade, so I wouldn't hold my breath ;) |
| 13:20:12 | <merijn> | int-e: I think yin is mostly referring to make base installable |
| 13:20:29 | <merijn> | So you could, for example, install a newer base on an older GHC and vice versa |
| 13:21:20 | <int-e> | Yeah I got the question. |
| 13:21:51 | → | fp joins (~Thunderbi@2001:708:150:10::1d80) |
| 13:22:38 | <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. |
| 13:30:24 | → | notdabs joins (~Owner@2600:1700:69cf:9000:3895:739f:4247:f37f) |
| 13:30:39 | → | sprotte24_ joins (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) |
| 13:31:03 | × | fp quits (~Thunderbi@2001:708:150:10::1d80) (Ping timeout: 268 seconds) |
| 13:32:13 | → | shreyasminocha_ joins (51fdc93eda@user/shreyasminocha) |
| 13:32:15 | → | ggb_ joins (a62ffbaf4f@2a03:6000:1812:100::3ac) |
| 13:32:15 | → | smiesner_ joins (b0cf5acf8c@2a03:6000:1812:100::13b9) |
| 13:32:15 | → | sm2n_ joins (ae95cb1267@user/sm2n) |
| 13:32:15 | → | raghavgururajan_ joins (ea769b8000@user/raghavgururajan) |
| 13:32:16 | → | simendsjo_ joins (34b0550437@2a03:6000:1812:100::1441) |
| 13:32:16 | → | arcadewise_ joins (52968ed80d@2a03:6000:1812:100::3df) |
| 13:32:16 | → | probie_ joins (cc0b34050a@user/probie) |
| 13:32:16 | → | ymherklotz_ joins (cb2c9cfbdd@2a03:6000:1812:100::29a) |
| 13:32:16 | → | ursa-major_ joins (114efe6c39@2a03:6000:1812:100::11f3) |
| 13:32:17 | → | duncan__ joins (c6181279e3@user/meow/duncan) |
| 13:32:18 | → | op_4_ joins (~tslil@2a01:4f8:c0c:7952::1) |
| 13:32:18 | → | samhh__ joins (7569f027cf@2a03:6000:1812:100::e4) |
| 13:32:19 | → | sefidel_ joins (~sefidel@user/sefidel) |
| 13:32:19 | → | j0lol_ joins (~j0lol@132.145.17.236) |
| 13:32:19 | → | saolsen_ joins (sid26430@id-26430.lymington.irccloud.com) |
| 13:32:44 | → | hamishmack_ joins (sid389057@id-389057.hampstead.irccloud.com) |
| 13:32:51 | → | bgamari_ joins (~bgamari@64.223.225.174) |
| 13:32:54 | → | cptaffe` joins (~cptaffe@user/cptaffe) |
| 13:33:02 | → | vgtw_ joins (~vgtw@user/vgtw) |
| 13:33:59 | × | cstml quits (~Thunderbi@user/cstml) (Quit: cstml) |
| 13:35:17 | → | milan2 joins (~milan@88.212.61.169) |
| 13:35:29 | → | inedia_ joins (~irc@2600:3c00:e000:287::1) |
| 13:35:34 | → | kst joins (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) |
| 13:35:41 | → | mima_ joins (~mmh@user/mima) |
| 13:35:46 | → | _[_________]_ joins (~oos95GWG@user/oos95GWG) |
| 13:36:22 | → | abrar_ joins (~abrar@static-96-245-187-163.phlapa.fios.verizon.net) |
| 13:36:31 | → | aforemny_ joins (~aforemny@2001:9e8:6cd3:ed00:7f35:da5a:93ab:c3e3) |
| 13:37:02 | → | mal1 joins (~mal@ns2.wyrd.be) |
| 13:37:14 | → | darrik joins (~natch@c-92-34-7-158.bbcust.telenor.se) |
| 13:37:28 | → | ystael joins (~ystael@user/ystael) |
| 13:40:08 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (*.net *.split) |
| 13:40:08 | × | TMA quits (tma@twin.jikos.cz) (*.net *.split) |
| 13:40:08 | × | sprotte24 quits (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) (*.net *.split) |
| 13:40:09 | × | aforemny quits (~aforemny@i59F4C778.versanet.de) (*.net *.split) |
| 13:40:09 | × | krjst quits (~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (*.net *.split) |
| 13:40:09 | × | Natch quits (~natch@c-92-34-7-158.bbcust.telenor.se) (*.net *.split) |
| 13:40:09 | × | cptaffe quits (~cptaffe@user/cptaffe) (*.net *.split) |
| 13:40:09 | × | rekahsoft quits (~rekahsoft@bras-base-orllon1103w-grc-15-174-95-4-83.dsl.bell.ca) (*.net *.split) |
| 13:40:09 | × | milan quits (~milan@88.212.61.169) (*.net *.split) |
| 13:40:09 | × | op_4 quits (~tslil@user/op-4/x-9116473) (*.net *.split) |
| 13:40:09 | × | [_________] quits (~oos95GWG@user/oos95GWG) (*.net *.split) |
| 13:40:09 | × | samhh_ quits (7569f027cf@2a03:6000:1812:100::e4) (*.net *.split) |
| 13:40:09 | × | raghavgururajan quits (ea769b8000@user/raghavgururajan) (*.net *.split) |
| 13:40:10 | × | duncan quits (c6181279e3@user/meow/duncan) (*.net *.split) |
| 13:40:10 | × | ursa-major quits (114efe6c39@2a03:6000:1812:100::11f3) (*.net *.split) |
| 13:40:10 | × | sm2n quits (ae95cb1267@user/sm2n) (*.net *.split) |
| 13:40:10 | × | probie quits (cc0b34050a@user/probie) (*.net *.split) |
| 13:40:10 | × | shreyasminocha quits (51fdc93eda@user/shreyasminocha) (*.net *.split) |
| 13:40:11 | × | simendsjo quits (34b0550437@2a03:6000:1812:100::1441) (*.net *.split) |
| 13:40:11 | × | arcadewise quits (52968ed80d@2a03:6000:1812:100::3df) (*.net *.split) |
| 13:40:11 | × | exfalsoquodlibet quits (a7085e0f71@2a03:6000:1812:100::13a3) (*.net *.split) |
| 13:40:11 | × | ymherklotz quits (cb2c9cfbdd@2a03:6000:1812:100::29a) (*.net *.split) |
| 13:40:11 | × | smiesner quits (b0cf5acf8c@user/smiesner) (*.net *.split) |
| 13:40:11 | × | ggb quits (a62ffbaf4f@2a03:6000:1812:100::3ac) (*.net *.split) |
| 13:40:11 | × | abrar quits (~abrar@static-96-245-187-163.phlapa.fios.verizon.net) (*.net *.split) |
| 13:40:11 | × | vgtw quits (~vgtw@user/vgtw) (*.net *.split) |
| 13:40:11 | × | j0lol quits (~j0lol@132.145.17.236) (*.net *.split) |
| 13:40:12 | × | acidsys quits (~crameleon@openSUSE/member/crameleon) (*.net *.split) |
| 13:40:12 | × | saolsen quits (sid26430@id-26430.lymington.irccloud.com) (*.net *.split) |
| 13:40:12 | × | hammond quits (proscan@gateway04.insomnia247.nl) (*.net *.split) |
| 13:40:12 | × | bgamari quits (~bgamari@64.223.225.174) (*.net *.split) |
| 13:40:12 | × | inedia quits (~irc@2600:3c00:e000:287::1) (*.net *.split) |
| 13:40:12 | × | sefidel quits (~sefidel@user/sefidel) (*.net *.split) |
| 13:40:12 | × | _koolazer quits (~koo@user/koolazer) (*.net *.split) |
| 13:40:13 | × | bastelfreak quits (bastelfrea@libera/staff/VoxPupuli.bastelfreak) (*.net *.split) |
| 13:40:13 | × | lieven quits (~mal@ns2.wyrd.be) (*.net *.split) |
| 13:40:13 | × | mima quits (~mmh@user/mima) (*.net *.split) |
| 13:40:13 | × | hamishmack quits (sid389057@id-389057.hampstead.irccloud.com) (*.net *.split) |
| 13:40:13 | duncan__ | is now known as duncan |
| 13:40:13 | ggb_ | is now known as ggb |
| 13:40:13 | hamishmack_ | is now known as hamishmack |
| 13:40:13 | shreyasminocha_ | is now known as shreyasminocha |
| 13:40:13 | darrik | is now known as Natch |
| 13:40:13 | cptaffe` | is now known as cptaffe |
| 13:40:14 | smiesner_ | is now known as smiesner |
| 13:40:14 | ymherklotz_ | is now known as ymherklotz |
| 13:40:14 | arcadewise_ | is now known as arcadewise |
| 13:40:14 | simendsjo_ | is now known as simendsjo |
| 13:40:14 | probie_ | is now known as probie |
| 13:40:14 | saolsen_ | is now known as saolsen |
| 13:40:14 | op_4_ | is now known as op_4 |
| 13:40:14 | sefidel_ | is now known as sefidel |
| 13:40:14 | raghavgururajan_ | is now known as raghavgururajan |
| 13:40:14 | sm2n_ | is now known as sm2n |
| 13:40:14 | ursa-major_ | is now known as ursa-major |
| 13:40:15 | j0lol_ | is now known as j0lol |
| 13:40:37 | → | lortabac joins (~lortabac@88-125-6-227.subs.proxad.net) |
| 13:42:55 | → | tavare joins (~tavare@user/tavare) |
| 13:42:58 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
| 13:43:54 | → | TMA joins (tma@twin.jikos.cz) |
| 13:45:51 | → | koolazer joins (~koo@user/koolazer) |
| 13:46:26 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 13:46:38 | → | bastelfreak joins (bastelfrea@libera/staff/VoxPupuli.bastelfreak) |
| 13:47:02 | → | acidsys joins (~crameleon@openSUSE/member/crameleon) |
| 13:47:53 | → | exfalsoquodlibet joins (a7085e0f71@2a03:6000:1812:100::13a3) |
| 13:51:14 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
| 13:54:56 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:11:50 | × | _[_________]_ quits (~oos95GWG@user/oos95GWG) (Quit: _[_________]_) |
| 14:11:58 | → | [_________] joins (~oos95GWG@user/oos95GWG) |
| 14:16:34 | → | weary-traveler joins (~user@user/user363627) |
| 14:25:17 | → | amadaluzia joins (~amadaluzi@user/amadaluzia) |
| 14:27:33 | → | Square joins (~Square4@user/square) |
| 14:33:43 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 14:34:13 | × | Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
| 14:34:45 | → | Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
| 14:38:25 | → | hattckory joins (~hattckory@70.27.118.207) |
| 14:43:09 | × | hattckory quits (~hattckory@70.27.118.207) (Ping timeout: 260 seconds) |
| 14:44:44 | × | notdabs quits (~Owner@2600:1700:69cf:9000:3895:739f:4247:f37f) (Read error: Connection reset by peer) |
| 14:48:08 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 14:48:38 | → | notdabs joins (~Owner@2600:1700:69cf:9000:a504:86ce:5139:ec16) |
| 14:49:18 | × | milan2 quits (~milan@88.212.61.169) (Quit: WeeChat 4.4.3) |
| 14:50:05 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 14:50:56 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 14:52:47 | → | j1n37 joins (~j1n37@user/j1n37) |
| 14:56:09 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 15:02:15 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 15:07:36 | × | lortabac quits (~lortabac@88-125-6-227.subs.proxad.net) (Quit: WeeChat 4.5.2) |
| 15:11:21 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 15:13:51 | → | ColinRobinson joins (~juan@user/JuanDaugherty) |
| 15:20:12 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 15:20:49 | × | acidjnk quits (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 15:30:03 | → | hammond joins (proscan@gateway04.insomnia247.nl) |
| 15:34:08 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 15:46:29 | ColinRobinson | is now known as JuanDaugherty |
| 15:47:35 | <hellwolf> | answering my own question: https://play.haskell.org/saved/tVbw1IsX did a case_non_zero_nat as exercise |
| 15:53:56 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 15:54:25 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 15:55:24 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 15:55:54 | → | amadaluzia_ joins (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) |
| 15:57:15 | JuanDaugherty | is now known as ColinRobinson |
| 16:00:31 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 16:01:01 | → | j1n37 joins (~j1n37@user/j1n37) |
| 16:05:37 | ColinRobinson | is now known as JuanDaugherty |
| 16:08:35 | × | GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 252 seconds) |
| 16:09:30 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 16:23:32 | JuanDaugherty | is now known as ColinRobinson |
| 16:26:20 | → | ft joins (~ft@p508db594.dip0.t-ipconnect.de) |
| 16:36:16 | → | sayurc joins (~sayurc@169.150.203.34) |
| 16:38:02 | → | acidjnk joins (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) |
| 16:38:57 | <EvanR> | ski, this law (whatever symbol is used for the equality) goes for all f, not some f |
| 16:39:07 | <EvanR> | forall x y and f |
| 16:40:44 | <EvanR> | which is followed in set theory for =, or hypothetically === in elixir (== fails in elixir to follow the law) |
| 16:42:37 | <EvanR> | seems to be a law in agda for = |
| 16:42:48 | <EvanR> | whence the cong tool |
| 16:49:32 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 16:51:11 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 16:52:49 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 16:54:45 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 248 seconds) |
| 16:57:08 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 16:57:27 | → | Square2 joins (~Square@user/square) |
| 17:01:30 | × | Square quits (~Square4@user/square) (Ping timeout: 252 seconds) |
| 17:01:30 | × | amadaluzia quits (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
| 17:01:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 17:03:28 | <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)' |
| 17:04:26 | <ski> | (that (latter) rule itself is often simply called "congruence", btw, taking it for granted that we're talking about function application) |
| 17:05:04 | <EvanR> | alright congruence is basically talking about both things together |
| 17:05:37 | <ski> | if you want to spell it out, "`==' is a congruence relation wrt function application" |
| 17:06:05 | <EvanR> | on what preserves what, I see this article with an extension to equality of lambda calculus terms called the ξ rule |
| 17:07:28 | <EvanR> | if M = N then \x.M = \x.N |
| 17:07:33 | × | tabaqui quits (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 17:07:42 | <ski> | yea, that's also congruence |
| 17:07:43 | <EvanR> | and it remarks "it means = preserves abstract" |
| 17:07:49 | <ski> | (in this case of lambda abstraction) |
| 17:07:54 | <EvanR> | abstraction |
| 17:09:01 | → | pavonia joins (~user@user/siracusa) |
| 17:09:16 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 17:11:25 | <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" |
| 17:11:51 | → | kimiamania9 joins (~65804703@user/kimiamania) |
| 17:12:44 | <EvanR> | maybe they're all mutually preserving each other |
| 17:13:04 | × | kimiamania quits (~65804703@user/kimiamania) (Read error: Connection reset by peer) |
| 17:13:04 | kimiamania9 | is now known as kimiamania |
| 17:13:33 | <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' |
| 17:16:09 | <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'" |
| 17:16:59 | <EvanR> | well that makes the remark backwards |
| 17:17:03 | × | acidjnk quits (~acidjnk@p200300d6e71c4f74c570287c99ce2cc6.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 17:17:28 | <ski> | "no mention of whether x may or must not appear free" -- it may |
| 17:18:12 | × | ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 17:19:21 | <ski> | but yea, i guess people often are a bit loose with which is the "preserver" and which is the "preservee" |
| 17:20:03 | <ski> | (reminds me i've seen people phrase `f(3)' as "`3' is being applied to the function `f'" ..) |
| 17:20:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 17:20:39 | <EvanR> | that's like 3[array] = *(3 + array) |
| 17:20:46 | <ski> | ayup |
| 17:21:40 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 17:21:44 | ski | . o O ( <https://ncatlab.org/nlab/show/reflected+limit> (example of "reflect" in the above sense, although in a highly abstract context) ) |
| 17:27:07 | <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) |
| 17:28:29 | → | YoungFrog joins (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) |
| 17:29:38 | <EvanR> | if a = b (mod m) then -a = -b (mod m) |
| 17:29:47 | <ski> | yep (for negation) |
| 17:30:24 | <EvanR> | what about in geometry, congruent triangles |
| 17:30:50 | <EvanR> | is that another topic or an instance of congruence above |
| 17:30:55 | × | sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
| 17:32:01 | <ski> | the operations are translations, rotations, reflections, and all possible compositions of those |
| 17:32:03 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 17:32:23 | <ski> | if we also allow scalings, then the congruence relation is called "similarity", rather than "congruent" |
| 17:32:37 | <EvanR> | ehm |
| 17:33:04 | → | acidjnk joins (~acidjnk@p200300d6e71c4f7444aa95b6f7c7abd1.dip0.t-ipconnect.de) |
| 17:33:13 | <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)> |
| 17:33:31 | <EvanR> | if ABC is congruent to DEF then T ABC is congruent to T DEF (T is a translation) |
| 17:33:58 | <EvanR> | a law satisfied by the relation |
| 17:34:12 | <EvanR> | though it doesn't explain what "is congruent" means |
| 17:34:16 | <ski> | yea. instead of "figures" we can say "generalized points", or "open expressions" |
| 17:35:16 | <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 |
| 17:36:15 | <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 |
| 17:36:40 | <ski> | (we translate a collection of points by translating each point in the collection, separately) |
| 17:36:42 | <EvanR> | ... set of points ... |
| 17:37:07 | <ski> | well. "indexed family" would be more accurate than "set" here, really |
| 17:39:01 | <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) |
| 17:39:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 17:39:30 | <ski> | the former is "non-injective", is "singular" (in matrix algebra terminology). the latter isn't |
| 17:39:35 | × | Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
| 17:39:52 | → | Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
| 17:40:23 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 17:40:35 | <ski> | even though both of those, extensionally, determine the same set of points |
| 17:41:09 | <EvanR> | that looks more like vector math, linear algebra |
| 17:41:36 | <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) |
| 17:42:03 | <EvanR> | ok good, "set of points" has more problems than I thought xD |
| 17:42:04 | <ski> | (s/for a/from a/) |
| 17:42:07 | → | sayurc joins (~sayurc@169.150.203.34) |
| 17:43:20 | <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 |
| 17:43:53 | <ski> | heron's formula for area works fine |
| 17:44:13 | <ski> | figuring out angles .. doesn't work out |
| 17:44:22 | <EvanR> | not a very good triangle |
| 17:44:55 | <ski> | or, if you want to, you could say that you should specify the angles, separately, that would work |
| 17:45:19 | <ski> | two angles being zero, the third being half a turn, e.g. |
| 17:45:43 | <ski> | (or some other configuration, that makes the angles sum up to a half turn) |
| 17:46:00 | <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 |
| 17:46:07 | <ski> | you can already consider a triangle with non-zero side lengths, but two angles being zero, so .. |
| 17:46:29 | <EvanR> | that would work |
| 17:48:48 | <EvanR> | alright, I'm wrong, you could confirm those angles are right, though the directions of the sides would not be defined |
| 17:49:09 | <EvanR> | you couldn't extend the sides into a half line or full line |
| 17:49:39 | <EvanR> | which could be fixed by also specifying that (in which case you didn't have to specify the angles) |
| 17:50:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 17:50:34 | <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 |
| 17:51:22 | <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 ? |
| 17:51:48 | <EvanR> | the "reciprocal" of complex infinities |
| 17:52:01 | <ski> | mm |
| 17:52:25 | <EvanR> | but a single direction might not be enough, or so I recall from 3D calculus |
| 17:52:41 | <EvanR> | approaching weird functions along different curves gets different results |
| 17:52:46 | <ski> | this kinda points towards projective space |
| 17:52:55 | → | Flow joins (~none@gentoo/developer/flow) |
| 17:53:00 | <EvanR> | approaching zero of weird functions |
| 17:53:27 | <ski> | yep, you can have a curve which doesn't have an asymptote line, as it approachex complex infinity |
| 17:55:14 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 17:55:15 | <ski> | mm, you're thinking of existence of all partial derivatives doesn't imply differentiability |
| 17:56:04 | <EvanR> | the details are foggy but since then I chalked it up to caring about bad functions xD |
| 17:57:10 | <EvanR> | I also have real analysis a constructive approach through interval arithmetic |
| 17:57:47 | <ski> | might want to take a peek at say first chapter of Anders Kock's book, too |
| 17:59:08 | <EvanR> | synthetic differential geometry |
| 17:59:14 | ski | . o O ( "Synthetic Differential Geometry" (2nd ed.) by Anders Kock in 2006-03 at <https://users-math.au.dk/kock/sdg99.pdf> ) |
| 17:59:17 | <ski> | yep |
| 17:59:48 | <EvanR> | analytic vs synthetic |
| 17:59:53 | <ski> | there's also the classic Errett Bishop book of Constructive Analysis |
| 18:00:07 | <ski> | (with Douglas Bridges, in later edition) |
| 18:00:33 | <EvanR> | the pdf on SDG on read really was cool |
| 18:00:37 | <EvanR> | I read* |
| 18:00:56 | <EvanR> | it seemed to really apply when trying to do geometry for computer games |
| 18:01:16 | <EvanR> | by thinking about edge cases in terms of what some highly zoomed in version of the geometry would be |
| 18:01:22 | <ski> | Kock proceeds by postulating an axiom, which would be inconsistent, if we used classical logic, but which is fine, using constructive logic |
| 18:01:52 | <ski> | basically that the subset of all reals whose square is zero, has dimension one, rather than zero |
| 18:02:23 | <EvanR> | a circle intersects a tangent line in not necessarily one point |
| 18:02:30 | <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) |
| 18:02:34 | <ski> | yep |
| 18:04:56 | <EvanR> | I speculate that that setting would be good for having zero size triangles but with all the proper data in tact |
| 18:05:17 | <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) |
| 18:05:45 | <ski> | hm, could be interesting to investigate |
| 18:05:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:06:44 | <ski> | and we get a "infinitesimal cancellation" law. if `d * a = d * b', for *all* `d' in `|D', then `a = b' |
| 18:10:37 | <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) |
| 18:10:44 | <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' |
| 18:11:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 18:11:39 | <ski> | so you calculate with infinitesimals as "quantities so small that their square is zero", like physicists have done, all along |
| 18:13:23 | <EvanR> | I thought physicists discard quantities that are too infinite xD |
| 18:13:51 | <ski> | heh, i guess occasionally, too :b |
| 18:15:52 | → | fantom joins (~fantom@2.219.56.221) |
| 18:16:21 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 18:16:42 | 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/> ) |
| 18:16:49 | 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/> ) |
| 18:16:54 | 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/> ) |
| 18:18:35 | <EvanR> | nlab draws a contrast between analysis and "synthesis", now we have SDG and smooth infinitesimal analysis, which are talking about the same thing? |
| 18:19:54 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 18:20:02 | → | j1n37 joins (~j1n37@user/j1n37) |
| 18:20:07 | <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" |
| 18:21:29 | <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 |
| 18:21:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:21:46 | <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 |
| 18:21:50 | <EvanR> | which would make it the opposite of constructing or building |
| 18:22:04 | <ski> | yes |
| 18:22:34 | <ski> | reverse-engineering our vague intuitions, in order to build a concrete implementation |
| 18:23:05 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 18:24:29 | <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) |
| 18:25:02 | → | XZDX joins (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) |
| 18:25:34 | × | XZDX quits (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) (Changing host) |
| 18:25:34 | → | XZDX joins (~xzdx@user/XZDX) |
| 18:26:00 | <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 ..) |
| 18:26:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 18:26:53 | <EvanR> | in the plato.stanford article on descartes I was surprised to learn a lot of unrelated-to-coordinate-planes stuff about his career |
| 18:27:20 | <ski> | mhm ? |
| 18:27:39 | <EvanR> | it was a time when people were arguing about whether this or that curve was sufficiently geometric |
| 18:27:58 | <EvanR> | and there was work on connecting algebraic formulas and curves |
| 18:28:27 | <ski> | yep |
| 18:28:27 | <EvanR> | stuff like conic sections were tentatively geometric at the time because you could construct it by cutting off a piece of cone |
| 18:28:46 | <EvanR> | but cubic curves being geometric was like blasphemy |
| 18:29:15 | <ski> | (i don't recall whether i read/skimmed those Stanford encyclopaedia articles, though. i'v read a bunch of others) |
| 18:29:52 | <ski> | mm. because of the restriction to unmarked ruler, and compass, in the constructions in Euclid's Elementa |
| 18:30:11 | <EvanR> | I'm not sure if that was the strict criteria anymore |
| 18:30:31 | <EvanR> | but "any random curve you can dream up" was certainly not necessarily a proper geometric curve |
| 18:30:55 | <EvanR> | this is the shit descartes was dealing with xD |
| 18:31:16 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 18:31:26 | 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 ) |
| 18:32:27 | <ski> | istr hearing about various mechanical devices, for drawing cubic curves |
| 18:33:00 | <EvanR> | yeah the had more devices |
| 18:33:01 | <haskellbridge> | <Bowuigi> Is geometric algebra related to anything here? It has "geometric" on the name |
| 18:33:22 | <ski> | (<https://plato.stanford.edu/entries/descartes/>,<https://plato.stanford.edu/entries/descartes-works/> being "those articles", in this case) |
| 18:34:18 | <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 |
| 18:34:32 | <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" |
| 18:34:43 | ← | bsima parts (~bsima@2604:a880:400:d0::19f1:7001) (So long, and thanks for all the fish.) |
| 18:34:45 | <ski> | i'd assume that it's synthetic in nature, but perhaps it has both synthetic and analytic aspects |
| 18:37:27 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:37:37 | → | frosthaern joins (~frosthaer@2406:7400:116:ac19:3f62:4a05:5a1d:7cdc) |
| 18:37:45 | 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> ) |
| 18:37:58 | × | frosthaern quits (~frosthaer@2406:7400:116:ac19:3f62:4a05:5a1d:7cdc) (Client Quit) |
| 18:40:26 | <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. |
| 18:40:50 | <EvanR> | The proof is left as an exercise in "unravelling" that everyone should do |
| 18:41:05 | <EvanR> | (some notational context is missing to make sense of that proposition) |
| 18:41:59 | <EvanR> | the jargon might just be coincidence |
| 18:43:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 18:43:11 | × | Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
| 18:43:27 | → | Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
| 18:45:40 | monochrom | would not analyse too much the choice of the word "analysis". >:) |
| 18:46:00 | <EvanR> | wikipedia suggests geometric algebra is related to exterior product |
| 18:46:31 | <EvanR> | monochrom, it's a nonce placeholder for a subject name! |
| 18:47:02 | <mauke> | nonce = child molester |
| 18:48:10 | <EvanR> | who put that in the dictionary |
| 18:48:24 | <monochrom> | Right, there is no such thing as "meaningful name". |
| 18:50:00 | <ski> | that's one of two meanings of "nonce" |
| 18:50:52 | <ski> | is `x + 1' a "name" ? |
| 18:51:40 | <mauke> | maybe. is its father called elon? |
| 18:51:48 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 18:52:01 | <ski> | (mathematicians would sometimes refer to it as such. programmers would probably say "expression" instead) |
| 18:53:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:57:53 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 19:00:02 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:45 | → | caconym joins (~caconym@user/caconym) |
| 19:03:52 | × | michalz quits (~michalz@185.246.207.221) (Remote host closed the connection) |
| 19:08:01 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 19:09:02 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:12:06 | × | cheater quits (~Username@user/cheater) (Ping timeout: 244 seconds) |
| 19:14:48 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 19:15:17 | → | cheater joins (~Username@user/cheater) |
| 19:15:24 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 19:16:15 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:17:41 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:18:10 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 248 seconds) |
| 19:19:22 | → | feetwind joins (~mike@user/feetwind) |
| 19:22:19 | <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 |
| 19:22:35 | <feetwind> | maybe it was just a dream |
| 19:22:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 19:22:45 | × | XZDX quits (~xzdx@user/XZDX) (Ping timeout: 260 seconds) |
| 19:25:46 | <geekosaur> | https://flora.pm/packages/@hackage/dump-core maybe? |
| 19:26:53 | → | j1n37- joins (~j1n37@user/j1n37) |
| 19:27:20 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 19:33:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:34:48 | <feetwind> | yes surely, thx :) |
| 19:38:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 19:39:20 | × | sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 19:41:26 | → | sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 19:44:47 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 19:45:43 | → | rbdr joins (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) |
| 19:49:16 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:51:20 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 19:51:20 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 19:53:18 | <hellwolf> | https://play.haskell.org/saved/JaGKxO4E this is just weirld. (need to use L11 instead of L10) |
| 19:53:57 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 19:55:16 | × | notdabs quits (~Owner@2600:1700:69cf:9000:a504:86ce:5139:ec16) (Read error: Connection reset by peer) |
| 19:57:13 | <int-e> | you can use a2 x = A2 x |
| 19:57:51 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 19:58:41 | → | weary-traveler joins (~user@user/user363627) |
| 19:59:59 | → | XZDX joins (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) |
| 20:00:21 | × | alp quits (~alp@2001:861:8ca0:4940:e00c:8d19:d96b:e8b0) (Ping timeout: 248 seconds) |
| 20:01:28 | <int-e> | And then a2 :: a -> A a will work |
| 20:02:48 | × | rbdr quits (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) (Quit: rbdr) |
| 20:03:33 | × | XZDX quits (~xzdx@2601:404:ce00:4e51:214:51ff:fe83:9855) (Changing host) |
| 20:03:33 | → | XZDX joins (~xzdx@user/XZDX) |
| 20:06:55 | <hellwolf> | interesting, more weird. |
| 20:07:57 | <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. |
| 20:08:15 | <int-e> | So by naming `x`, x :: a can be used as x :: Show a => a as required by A2 |
| 20:08:45 | <int-e> | (I'm assuming that you do understand that the types of A1 and A2 are different) |
| 20:09:21 | <hellwolf> | I understand the rankN part |
| 20:10:29 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 20:10:33 | → | rbdr joins (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) |
| 20:12:14 | <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) |
| 20:12:23 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 20:12:56 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 20:14:03 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 20:14:06 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 20:14:08 | → | gmg joins (~user@user/gehmehgeh) |
| 20:14:14 | <EvanR> | (Show a => a) -> A a is a thing? Is it rank 2 |
| 20:14:48 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
| 20:15:58 | <int-e> | Well I omitted the forall. that goes with it |
| 20:16:34 | <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. |
| 20:16:53 | <hellwolf> | yea, I extracted from my code. it's a bit contrived. |
| 20:16:59 | <hellwolf> | with Show. |
| 20:17:32 | <EvanR> | (forall a . Show a => a) -> A a -- different a? |
| 20:18:26 | <int-e> | EvanR: No, it's literally an empty forall. |
| 20:18:40 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:18:56 | <int-e> | EvanR: there was a link: https://play.haskell.org/saved/JaGKxO4E |
| 20:19:54 | <EvanR> | wtf |
| 20:20:32 | <EvanR> | I saw an "bindless lambda" yesterday like \whatever |
| 20:20:41 | <EvanR> | but now I've seen everything |
| 20:22:22 | <int-e> | :t \ -> () |
| 20:22:23 | <lambdabot> | error: parse error on input ‘->’ |
| 20:22:25 | <int-e> | ;-) |
| 20:22:50 | <hellwolf> | I have a feeling this won't be the last one |
| 20:23:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 20:24:05 | <int-e> | FWIW, that forall. is not actually needed. |
| 20:24:58 | <hellwolf> | I like to write "forall." explicitly sometimes, so that no typo will create a type variable by accident. |
| 20:25:33 | <EvanR> | need a type system for the type signatures to keep it straight |
| 20:25:53 | <int-e> | hellwolf: It's fairly common to need a few eta-expansions when working with higher rank types in GHC. |
| 20:26:05 | <int-e> | EvanR: let me tell you about kinds |
| 20:26:43 | <hellwolf> | I have noticed also with linear arrows sometimes. |
| 20:28:01 | × | Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
| 20:28:17 | → | Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
| 20:28:18 | → | biberu joins (~biberu@user/biberu) |
| 20:28:28 | <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 |
| 20:29:29 | × | bliminse quits (~bliminse@user/bliminse) (Quit: leaving) |
| 20:30:43 | <int-e> | Oh there's a DeepSubsumption extension for this? I never knew. |
| 20:30:58 | <int-e> | Indeed that makes a2 = A2 compile. |
| 20:31:33 | <geekosaur> | it's pretty recent and documented as ephemeral (that is, it's inteended only as a porting aid and expected to go away) |
| 20:31:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:34:05 | × | amadaluzia_ quits (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) (Changing host) |
| 20:34:05 | → | amadaluzia_ joins (~amadaluzi@user/amadaluzia) |
| 20:34:39 | <int-e> | So... DeepSubsumption enables some functionality that GHC never had, but is scheduled to be removed. That's fun. |
| 20:35:00 | → | bliminse joins (~bliminse@user/bliminse) |
| 20:35:04 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds) |
| 20:36:00 | <hellwolf> | I remember it caused a huge disturbance in the universe |
| 20:36:06 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 20:36:35 | <mauke> | 42 :: exists. Int |
| 20:37:38 | <hellwolf> | foo :: exists a. a ~ Void => a |
| 20:39:41 | <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. |
| 20:40:05 | <int-e> | I don't have any pre-8.0 versions to test. |
| 20:40:14 | × | Googulator quits (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) (Quit: Client closed) |
| 20:40:31 | → | Googulator joins (~Googulato@2a01-036d-0106-211a-98f9-54d1-cd01-d0d3.pool6.digikabel.hu) |
| 20:42:29 | × | tromp quits (~textual@2001:1c00:3487:1b00:44ed:cdbe:8e8e:71c5) (Ping timeout: 248 seconds) |
| 20:44:09 | <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 |
| 20:46:18 | <monochrom> | DeepSubsumption is a backward-compatibility flag for newer GHCs that provide quicklook impredicativity. |
| 20:46:20 | <int-e> | ironically I learned about RankNTypes before 8.2 so this need for eta-expansion did not surprise me. |
| 20:47:05 | <hellwolf> | oh impredicativetypes is that other magic spell word |
| 20:47:19 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:47:54 | × | myme quits (~myme@2a01:799:d5e:5f00:8f18:9cf4:29f5:943f) (Ping timeout: 265 seconds) |
| 20:48:18 | <monochrom> | In more detail, in those newer GHCs, even if you don't ask for impredicativity, you still get the modified type inference algorithm. |
| 20:48:47 | → | myme joins (~myme@2a01:799:d5e:5f00:2d74:af8d:2498:f0a8) |
| 20:49:40 | <geekosaur> | yes. there's a discussion in 9.0.1's release notes iirc |
| 20:50:24 | <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. |
| 20:51:20 | <EvanR> | it's literally the negation of something |
| 20:51:30 | <int-e> | I get *that* |
| 20:51:38 | <EvanR> | so not a great way to get at what it positively is |
| 20:51:53 | <EvanR> | like non-linear |
| 20:52:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 20:52:07 | <int-e> | EvanR: stop |
| 20:52:15 | <int-e> | (you're not helping) |
| 20:52:33 | <hellwolf> | impredatory language |
| 20:52:39 | <EvanR> | stop agreeing with me |
| 20:52:42 | × | amadaluzia_ quits (~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.) |
| 20:52:42 | <hellwolf> | aka. javascript |
| 20:52:43 | <int-e> | (and frankly I didn't ask for an explanation) |
| 20:53:04 | → | amadaluzia joins (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) |
| 20:53:06 | <hellwolf> | predatory language. aka Haskell |
| 20:53:21 | <hellwolf> | or the other way around, depending on the user. |
| 20:53:30 | × | amadaluzia quits (~amadaluzi@2a00:23c7:ed8b:6701:d3f5:8c4c:643c:d012) (Remote host closed the connection) |
| 20:53:52 | → | amadaluzia joins (~amadaluzi@host217-43-236-22.range217-43.btcentralplus.com) |
| 20:54:54 | <EvanR> | otoh I can ask what impredicativity means |
| 20:55:16 | <EvanR> | in this context |
| 20:55:38 | <hellwolf> | [forall a. a -> String] |
| 20:55:45 | <hellwolf> | is this impredicative type or rankn |
| 20:55:49 | <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. |
| 20:55:57 | <monochrom> | Impredicative. |
| 20:56:02 | → | Guest87 joins (~Guest87@2620:72:0:1f18:7d2a:62e7:7a20:d79f) |
| 20:56:54 | <monochrom> | Impredicative implies rank-n so it's also rank-n :) |
| 20:56:57 | <hellwolf> | so (forall a. a -> String) -> String is rankn |
| 20:57:10 | <hellwolf> | but [forall a. a -> String] -> Srring is impredicativetypes |
| 20:57:39 | <hellwolf> | ah, so it is generalization |
| 20:57:40 | <hellwolf> | ? |
| 20:58:11 | <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 |
| 20:58:50 | <monochrom> | Yes you can have id (id :: forall a. a -> a) |
| 20:59:31 | <monochrom> | You can have [id :: forall a. a->a] |
| 21:00:13 | <EvanR> | :t id (id :: forall a . a -> a) |
| 21:00:14 | <lambdabot> | a -> a |
| 21:00:25 | <monochrom> | lambdabot doesn't do impredicative. |
| 21:00:44 | <hellwolf> | :t id id id id id id id id |
| 21:00:45 | <lambdabot> | a -> a |
| 21:01:54 | <hellwolf> | %import Data.Void |
| 21:02:04 | <ncf> | :t fmap fmap fmap fmap id id id id |
| 21:02:05 | <lambdabot> | a -> a |
| 21:02:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:03:08 | <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 |
| 21:03:08 | <Guest87> | Suppose I want to represent an a mapping of variables to values. Can be done with a list, or with the following functions: |
| 21:03:09 | <Guest87> | ``` |
| 21:03:09 | <Guest87> | makeEnv = \a -> undefined |
| 21:03:10 | <Guest87> | extendEnv var val env = \y -> if y == var then val else (env y) |
| 21:03:10 | <Guest87> | ``` |
| 21:03:38 | <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? :) |
| 21:03:40 | <monochrom> | You can do that. You can also use Data.Map. |
| 21:04:35 | <monochrom> | Functions will not be very good at that, especially if you use undefined. |
| 21:04:39 | × | amadaluzia quits (~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.) |
| 21:04:58 | <Guest87> | I totally could, but this problem is a simpler representation of a problem I am trying to solve in a different language. |
| 21:05:18 | × | inca quits (~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 272 seconds) |
| 21:05:28 | <monochrom> | I thought lists were more available than functions in a different language. |
| 21:05:40 | <monochrom> | Unless that other language is System F. |
| 21:05:55 | <Guest87> | They are haha, but I am being stubborn and trying to do it the cool way |
| 21:06:13 | <EvanR> | you can represent the list data type using lambdas |
| 21:06:26 | <EvanR> | I dunno if that's cool enough though |
| 21:06:45 | <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" |
| 21:06:47 | → | amadaluzia joins (~amadaluzi@host217-43-236-22.range217-43.btcentralplus.com) |
| 21:06:57 | <monochrom> | Representing list use lambda also requires either impredicativity or untyped. |
| 21:07:59 | <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. |
| 21:08:21 | → | enoq joins (~enoq@2a05:1141:1e6:3b00:6d50:57a3:cc97:7b04) |
| 21:09:06 | <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? |
| 21:09:08 | <int-e> | So the shadowed values (here "v" -> 1) are completely inaccessible. |
| 21:09:37 | <EvanR> | "too many operators" is usually a reaction to not knowing what <$> or <*> means |
| 21:09:38 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 21:09:46 | <enoq> | am I looking for something like Scala? |
| 21:09:55 | <EvanR> | my list of "all (default) haskell operators" is most consisting of operators available in "normal" languages |
| 21:10:01 | <EvanR> | mostly |
| 21:10:16 | <EvanR> | probably a better idea to just look up what <$> and <*> are |
| 21:10:27 | <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. |
| 21:10:28 | <EvanR> | (they're useful) |
| 21:10:37 | <int-e> | EvanR: Who knows, maybe they're dealing with lens |
| 21:10:52 | × | amadaluzia quits (~amadaluzi@host217-43-236-22.range217-43.btcentralplus.com) (Client Quit) |
| 21:10:52 | <monochrom> | COBOL uses words. |
| 21:11:12 | <enoq> | a hell of a lot of those yeah xD |
| 21:11:13 | <monochrom> | You literally have to write "MULTIPLY X BY Y INTO Z" |
| 21:11:13 | → | inca joins (~inca@pool-96-255-212-224.washdc.fios.verizon.net) |
| 21:11:33 | <enoq> | like applicativeMap instead of <*> |
| 21:11:42 | <EvanR> | it's not a map |
| 21:11:48 | <enoq> | or just applicative |
| 21:11:53 | <__monty__> | `ap` no? |
| 21:11:58 | <haskellbridge> | <loonycyborg> can just put functions in `` and use them as operators |
| 21:11:58 | <EvanR> | ap exists |
| 21:12:14 | <haskellbridge> | <loonycyborg> "asTypeOf" etc :P |
| 21:12:15 | <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. |
| 21:12:55 | <enoq> | no need to pick either extreme |
| 21:13:14 | <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 |
| 21:13:28 | <EvanR> | also in cobol |
| 21:13:35 | <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 |
| 21:13:36 | <monochrom> | Haskell is already neither extreme. |
| 21:14:12 | <int-e> | and the programs don't become more readable either |
| 21:14:16 | <enoq> | yeah, I guess you could say APL is even worse |
| 21:14:40 | <monochrom> | We are like "mod 5 3" which is even more wordy than C. |
| 21:14:59 | <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 |
| 21:15:03 | <haskellbridge> | <loonycyborg> one most unusual choice is use of space for function application instead of more common (x,y..) |
| 21:15:04 | <int-e> | or 5 `mod` 3 |
| 21:15:08 | <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? |
| 21:15:14 | <EvanR> | but that issue exists for non-operators |
| 21:15:21 | <__monty__> | 5 `mod` 3 is arguably more readable IMO. |
| 21:15:53 | <Guest87> | `extend "v" 1`* |
| 21:16:10 | <haskellbridge> | <loonycyborg> I'm wondering if it was considered to use space for function composition instead |
| 21:16:19 | <EvanR> | many people would not understand % used for modulo, so it's probably a good idea to not use C at all |
| 21:16:20 | <int-e> | Guest87: you just swapped 1 and 2 in what I wrote |
| 21:16:22 | <haskellbridge> | <loonycyborg> and more conventional syntax for function calls |
| 21:16:34 | <__monty__> | loonycyborg: You can go further and use juxtaposition to mean composition, see Forth et al. |
| 21:16:42 | <EvanR> | conventional syntax for function calls as is would not work with currying |
| 21:16:48 | <EvanR> | unfortunately |
| 21:17:07 | <EvanR> | and would add a lot of noise |
| 21:17:12 | <monochrom> | I don't use space for function application. |
| 21:17:27 | <monochrom> | > fst(length,id)"abcd" |
| 21:17:29 | <lambdabot> | 4 |
| 21:17:29 | <haskellbridge> | <loonycyborg> __monty__: ye it's like in math |
| 21:17:30 | <int-e> | > id(42) |
| 21:17:32 | <lambdabot> | 42 |
| 21:17:33 | <monochrom> | No space. |
| 21:17:56 | <Guest87> | int-e Oh oops sorry. I want `extendEnv "v" 1 (extendEnv "v" 2 makeEnv)` to be indistinguishable from `extendEnv "v" 2 makeEnv` |
| 21:17:58 | → | amadaluzia joins (~amadaluzi@2a00:23c7:ed8b:6701:57da:5a07:1b87:60e1) |
| 21:18:00 | <haskellbridge> | <loonycyborg> I'm just wondering whether haskell was considering it too |
| 21:18:01 | <EvanR> | math has a hard time with currying, going for extraneous jargon to emphasize that a function might be higher order |
| 21:18:23 | <EvanR> | very confusing, instead of just having "function" and domain and range for them all |
| 21:19:01 | <monochrom> | But I can agree with Dijkstra in using explicit . for application, ∘ for composition, e.g. length."abcd" |
| 21:19:02 | <EvanR> | instead of function it's an operator, or a transform, or a functional (??) |
| 21:19:04 | <int-e> | Guest87: you'd have to change extendEnv to allow that; it would have to check whether "v" is already defined. So you have to change `makeEnv` too because there's no way to do anything useful with `undefined` |
| 21:19:22 | × | amadaluzia quits (~amadaluzi@2a00:23c7:ed8b:6701:57da:5a07:1b87:60e1) (Client Quit) |
| 21:19:43 | <int-e> | (and that will be true in any pure functional language) |
| 21:20:27 | <EvanR> | > let f(x,y) = x+y in f(3,7) |
| 21:20:28 | <lambdabot> | 10 |
| 21:20:34 | <EvanR> | noice |
| 21:20:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:20:54 | → | amadaluzia joins (~amadaluzi@2a00:23c7:ed8b:6701:6582:5675:67d:4956) |
| 21:21:18 | <monochrom> | If you like standard math/C notation, you can always write mod(5)(3). (Landin did that.) |
| 21:21:24 | <int-e> | > (+)`uncurry`(2,3) |
| 21:21:25 | <lambdabot> | 5 |
| 21:22:21 | <Guest87> | So if I was working with lists, `extendEnv var val env = env <> (var, val)` is all I would need to get the behavior that I am describing poorly |
| 21:22:23 | <int-e> | monochrom: If you ever try to write a functional program in Python you'll do that too. |
| 21:22:41 | <Guest87> | `env <> [(var, val)]` * |
| 21:22:48 | <EvanR> | so by using tuples you can write f(x,y,z,etc) in haskell, but you might annoy everybody reading the code again |
| 21:22:53 | <monochrom> | I suppose Landin was trying to write functional programs in Algol! :) |
| 21:23:58 | <monochrom> | But yeah the beauty is that it already works here and now, in Haskell JS Python. |
| 21:24:04 | <Guest87> | If `extendEnv` had to return a function, is there an easy way to express this "append to the end" behavior? |
| 21:24:43 | <EvanR> | if you have undefined at the end I think you can't do much of anything with this list, without knowing additional information about it (the length) |
| 21:25:01 | <EvanR> | which you probably don't want to track separately |
| 21:25:06 | <EvanR> | but you could |
| 21:25:37 | <monochrom> | There is no "append to end" for functions. It doesn't exist. But it's also an XY problem. |
| 21:25:46 | <Guest87> | Ok how about `makeEnv = \a -> "undefined"` |
| 21:25:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 21:26:38 | <EvanR> | it's a start |
| 21:26:40 | <monochrom> | The X problem is simply "add a key-value pair but not when key is already in the map" which is pretty easy to do. |
| 21:27:09 | <EvanR> | also if the goal was the just do it normally but backwards, you can do it normally then reverse the list for some reason |
| 21:27:11 | <monochrom> | Frankly even for the list version I wouldn't append to end for multiple reasons. |
| 21:27:15 | <int-e> | easy to do provided that you can check membership in the map |
| 21:27:29 | int-e | points to his messages from 8 minutes ago |
| 21:29:04 | × | rbdr quits (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 21:29:31 | <EvanR> | if you will never have the sentinel value "undefined" in your environment that would work |
| 21:29:56 | <EvanR> | I dunno if this counts as good or cool anymore though |
| 21:30:26 | <int-e> | In Haskell you could wrap values in a Maybe, starting with \x -> Nothing |
| 21:30:54 | <int-e> | But there's a lot of reasons to prefer Data.Map in almost all cases. |
| 21:30:56 | <monochrom> | May I pitch the System F solution? LOL |
| 21:31:13 | <monochrom> | Including both list and maybe in System F heh |
| 21:31:41 | <monochrom> | OK AVL trees in System F LOL |
| 21:31:59 | <int-e> | how hard could it be |
| 21:32:18 | <Guest87> | Will I get in "trouble" if I use code from a different language to show my problem? I am realizing my "simpler representation" is not really accurate |
| 21:32:20 | <monochrom> | "It will annoy the reader" :) |
| 21:32:44 | <monochrom> | As long as I understand the different language. |
| 21:33:12 | <Guest87> | Actually, I can still represent the actual problem in haskell gimme 1 sec |
| 21:33:14 | × | enoq quits (~enoq@2a05:1141:1e6:3b00:6d50:57a3:cc97:7b04) (Quit: Leaving) |
| 21:33:31 | <EvanR> | XY problem but X and Y are programming languages |
| 21:33:32 | <int-e> | monochrom: "It will annoy the reader" <-- why else would you be on IRK |
| 21:33:50 | <monochrom> | :) |
| 21:34:05 | <hellwolf> | how many of you use monadic bang? |
| 21:34:08 | <EvanR> | solve it in known language X but the task is to solve it in Y (unknown) |
| 21:34:16 | <monochrom> | What is monadic bang? |
| 21:35:21 | <hellwolf> | https://hackage.haskell.org/package/monadic-bang . TL;DR: to replace "a <- yourmon x; pure a" with "pure !(yourmon x)" |
| 21:36:04 | <EvanR> | even in web world that is frowned upon |
| 21:36:15 | <EvanR> | they want you to put each side effecting statement on its own line |
| 21:36:20 | <EvanR> | and use a temporary |
| 21:36:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:36:49 | <monochrom> | Is that supposed to be an acme package? As in a joke? Or was it April 1? Because you can always just write "yourmon x" with just standard Haskell. |
| 21:37:26 | <hellwolf> | my example was just an illustration. |
| 21:37:27 | <haskellbridge> | <loonycyborg> How easy it's to use plugins like that? Is it enough to add something to your cabal file? |
| 21:37:54 | <hellwolf> | {-# OPTIONS_GHC -fplugin=MonadicBang #-} |
| 21:38:52 | <haskellbridge> | <loonycyborg> and how to ensure plugin is actually installed? |
| 21:39:12 | <monochrom> | In that case, applicative/idiom notation/brackets already exist. |
| 21:39:30 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:39:54 | <haskellbridge> | <loonycyborg> hmm just add it to depends I guess |
| 21:39:58 | <monochrom> | OK, I don't know where to look for an implementation, but people have talked about it. The upside being you just need Applicative, you don't need Monad. |
| 21:40:47 | <monochrom> | The downside being the very reason I came to Haskell is precisely because I'm tired of that sh*t. |
| 21:41:23 | <hellwolf> | what are you exactly tired of? |
| 21:41:46 | <monochrom> | "sin(readNum()) + cos(random(0,1))" thanks but no tanks. |
| 21:41:48 | <hellwolf> | (not trying to argue, I am just curious whys and whynots) |
| 21:41:52 | <monochrom> | s/tanks/thanks/ |
| 21:41:59 | <EvanR> | stupid syntax tricks |
| 21:42:25 | <hellwolf> | is do notation as a syntax trick the sweet spot you are oaky with? |
| 21:42:40 | <hellwolf> | or would you think writing >>= everywhere is better? |
| 21:42:43 | <EvanR> | do notation is barely a trick, if you tried going with just >>= and lambda |
| 21:42:48 | <EvanR> | it's very similar code |
| 21:42:48 | <monochrom> | How does do-notation count as a syntax trick? |
| 21:43:10 | <hellwolf> | by definition it can be desugared |
| 21:43:22 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 21:43:34 | <monochrom> | If that is your definition, my objection is not about sugar vs desugar. |
| 21:43:49 | <monochrom> | My principle is that syntax should not hide semantics. |
| 21:43:53 | <hellwolf> | that monadic bang inline otherwise lines of monadic bind to a !(..) block, I am not sure if it makes things that much worse. |
| 21:44:28 | <hellwolf> | fair enough, monadic bang does have semantic ambigouity which !(..) block get bound first. |
| 21:44:39 | <monochrom> | do-notation does not hide the effectful and sequential semantics (of IO, say). "sin(readNum()) + cos(random(0,1))" does. If you're in C, you don't even know the effect order now. |
| 21:45:09 | <hellwolf> | you would assume so, but laziness can catch you off guard. |
| 21:45:16 | <EvanR> | that's one of the reasons it's not approved of in imperative code right now either |
| 21:45:23 | <EvanR> | ordering |
| 21:46:27 | <monochrom> | Why are people so hung up on syntax? |
| 21:47:02 | <monochrom> | "It's not English so I don't understand it." "It's not sin(cmd1()) so I don't understand it." |
| 21:47:27 | <EvanR> | in both cases it's "something I was familiar with already" |
| 21:47:31 | <int-e> | monochrom: you can complain about the syntax *before* you learn a language |
| 21:48:22 | <EvanR> | I'm guilty of doing this, going from haskell to PHP, ruby, javascript. Trying to make it do functional things |
| 21:48:27 | <EvanR> | and making a huge mess of it |
| 21:48:27 | <int-e> | (Am I answering a rhetorical question? Maybe.) |
| 21:48:40 | <monochrom> | Wait, no, that would mean complaints from outsiders. |
| 21:48:45 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 21:48:48 | <monochrom> | uninformed complaints from outsiders. |
| 21:49:07 | <hellwolf> | "how learn to stop worrying and love the boilerplates?" |
| 21:49:17 | <EvanR> | boilerplate? |
| 21:49:19 | <monochrom> | But I would be OK with *during*. It's fair to ask "why this syntax? what motivation? what's the big picture?" |
| 21:50:26 | <hellwolf> | different people have different level of trigger point when it comes to the amount of tolerable boilerplate, i guess |
| 21:50:35 | <EvanR> | boilerplate is when there is no way to reuse code except copy and paste a huge amount of it into the file |
| 21:50:44 | <EvanR> | in haskell you have functions |
| 21:51:03 | <hellwolf> | monadic bang is for people triggered by unnecessary one-time variable names |
| 21:51:26 | <haskellbridge> | <loonycyborg> for boilerplate there's always CPP :P |
| 21:51:39 | <EvanR> | action >>= followup |
| 21:51:56 | <EvanR> | if followup is point free no name |
| 21:52:30 | <EvanR> | but enough point free will annoy the reader! |
| 21:52:35 | <hellwolf> | so I guess I got the answer from you guys then: no one uses monadic bang! :) |
| 21:52:39 | <monochrom> | "(+) <*> fmap sin getNum <*> fmap cos (randomRIO (0,1))" does not have unnecessary one-time variable names. |
| 21:52:41 | <haskellbridge> | <loonycyborg> template haskell too but it has limitations |
| 21:52:51 | <haskellbridge> | <loonycyborg> like TH can't generate import statements |
| 21:52:59 | <EvanR> | probably for the best |
| 21:53:05 | <haskellbridge> | <loonycyborg> that would be useful for emulating conditional compilation |
| 21:53:10 | <monochrom> | Unless you then point to the "unnecessary" two-time "fmap"s. |
| 21:53:26 | <hellwolf> | monochrom: those may need necessary variable names! |
| 21:53:46 | <hellwolf> | even if they were one-time |
| 21:53:49 | <haskellbridge> | <loonycyborg> like how would you conditionally import a module depending on host platform/arch/os etc otherwise? |
| 21:54:00 | <hellwolf> | for readability; subjectivity be not damned |
| 21:54:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:54:33 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:54:35 | <monochrom> | loonycyborg: CPP is the current only way. |
| 21:55:11 | <haskellbridge> | <loonycyborg> there's just no getting rid of damned thing |
| 21:55:14 | <EvanR> | different cabal files xD |
| 21:55:24 | <EvanR> | one for linux one for windows |
| 21:56:13 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 21:57:54 | <hellwolf> | would you be okay with this boilerplate: |
| 21:57:56 | <hellwolf> | let (arr1, x) = read arr0 0 |
| 21:57:56 | <hellwolf> | (arr2, y) = read arr1 1 |
| 21:58:10 | <monochrom> | That would require a makefile to determine which cabal file to use. |
| 21:58:10 | <hellwolf> | the infamous linear-type threading of variable names. |
| 21:58:13 | <EvanR> | can we not call this boilerplate |
| 21:58:27 | <EvanR> | it's kind of like "what do you think of DSL disease" |
| 21:58:34 | <monochrom> | yeah we can call it toxic instead |
| 21:58:59 | <hellwolf> | what do we call it? |
| 21:59:01 | <monochrom> | or any of the latest most popular hyperboles |
| 21:59:20 | → | rbdr joins (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) |
| 21:59:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 21:59:43 | <EvanR> | threading of successive state variables |
| 21:59:59 | <EvanR> | which is a thing also in elixir (they have no such state monad or anything) |
| 22:00:24 | <EvanR> | though linear base does |
| 22:00:37 | <hellwolf> | thinking about it, isn't State monad a nice way of bypassing the need of that threading for that use case? |
| 22:01:23 | <monochrom> | But I defy your false dichotomy. I estimate which one is shorter and go with it: manual threading like that vs using State. |
| 22:02:31 | <monochrom> | You see, there are always some annoying people like me who always answers "it depends". |
| 22:03:06 | <monochrom> | Ruining any rule of thumb, style guide, doctrine, dogma, ideology. |
| 22:03:10 | <hellwolf> | today, I actually managed to implement a different threading-hiding solution for lineartypes. Though, the Ur pattern makes most of the problem going away anyways; mine is for something different. |
| 22:03:42 | <hellwolf> | I like it depends, as long as it's explained clearly. |
| 22:04:22 | <monochrom> | I guess except for the it-depends ideology. :) |
| 22:04:35 | <monochrom> | itdependism |
| 22:04:45 | <hellwolf> | changing-goal-post as a merit. |
| 22:04:56 | <Guest87> | int-e monochrom okay, I have a similar implementation ready for haskell, though i am doing it in a text editor so I apologize for any typos |
| 22:04:58 | <hellwolf> | principle as a sin. |
| 22:05:30 | <hellwolf> | (tongue-in-cheek here. personally, I much prefer principle first) |
| 22:05:49 | <Guest87> | data Task = Task {programToRun :: String, input :: String} |
| 22:05:49 | <Guest87> | data Pipeline = Pipeline {initialTask :: String, steps :: [String -> Task]} |
| 22:05:50 | <Guest87> | makePipeline task = Pipeline task [] |
| 22:05:50 | <Guest87> | addStep pipeline step = Pipeline (initialTask pipeline) (steps pipeline <> [step]) |
| 22:05:51 | <Guest87> | runTask :: Task -> IO (Either String Task) |
| 22:05:51 | <Guest87> | run pipeline = do |
| 22:05:52 | <Guest87> | case (steps pipeline) of |
| 22:05:52 | <Guest87> | [] -> putStrLn "done" |
| 22:05:53 | <Guest87> | [f:nxt] -> (beginRun nxt) . f . initialTask $ pipeline |
| 22:05:53 | <Guest87> | beginRun next task = do |
| 22:05:53 | <EvanR> | aaaaaaaa |
| 22:05:54 | <Guest87> | step <- runTask task |
| 22:05:54 | <Guest87> | case step of |
| 22:05:55 | <Guest87> | Left res -> case next of |
| 22:05:55 | <Guest87> | [] -> putStrLn "done" |
| 22:05:56 | <Guest87> | [f:nxt] -> beginRun nxt (f res) |
| 22:05:56 | <Guest87> | Right t -> beginRun next t |
| 22:05:59 | <hellwolf> | stooooop |
| 22:06:11 | <Guest87> | Ugh I should paste in a gist :( |
| 22:06:12 | <hellwolf> | https://paste.tomsmeding.com/ |
| 22:06:19 | <Guest87> | Or there, thank you hellwolf |
| 22:06:41 | <Guest87> | https://paste.tomsmeding.com/tggksoJO |
| 22:06:52 | <geekosaur> | IRC is absolutely terrible for code, and too old to support things like code blocks |
| 22:07:05 | <Guest87> | I am too used to discord and other chats I think |
| 22:07:18 | <EvanR> | IRC gets new features all the time |
| 22:07:22 | <EvanR> | soon... code blocks |
| 22:07:23 | <haskellbridge> | <maralorn> hellwolf: I will try to use monadic-bang I have been hoping for something like it for a long time and had kinda forgotten about the plugin. |
| 22:07:28 | <EvanR> | and animated premium emojis |
| 22:08:28 | <haskellbridge> | <maralorn> Is this an IRC nitro pro channel? |
| 22:08:29 | <Guest87> | So, the problem/annoyance I have is that I want to [String -> Task] to be somehow squashed into a single (String -> Task) |
| 22:09:26 | <EvanR> | Monoid m => Monoid (a -> m) |
| 22:09:38 | <hellwolf> | maralorn: nice! It seems actively maintained, which is a good sign. |
| 22:09:42 | <EvanR> | mconcat :: [a -> m] -> a -> m |
| 22:09:52 | <EvanR> | if Task were a Monoid |
| 22:10:12 | <haskellbridge> | <maralorn> Doesn't look like a monoid to me. |
| 22:10:30 | <monochrom> | [String -> Maybe Task] is much more squashable. |
| 22:11:01 | <haskellbridge> | <maralorn> Would String -> [Task] be an option that looks more feasible. |
| 22:11:07 | <monochrom> | which is still repeating what we said before --- undefined is not very workable with in the first place. Use Nothing. |
| 22:12:00 | <EvanR> | [Task] be a monoid |
| 22:12:16 | <monochrom> | Oh yeah Maybe Task is too. Same difference :) |
| 22:12:31 | <EvanR> | pick your squash |
| 22:12:37 | <monochrom> | Also there are First and Last for overriding or not overriding existing mappings. |
| 22:13:22 | <monochrom> | Also did you know that flip (++) is also a monoid operator :) |
| 22:14:18 | × | rbdr quits (~rbdr@dynamic-089-012-130-183.89.12.pool.telefonica.de) (Quit: WeeChat 4.6.0) |
| 22:14:51 | <Guest87> | My current solution does the following: |
| 22:14:52 | <Guest87> | https://paste.tomsmeding.com/8E9is43S |
| 22:15:38 | <Guest87> | It works well, but the only problem is that `n` `addCont` calls means I have to unwrap `n-1` layers to get to the actual next step |
| 22:16:33 | <EvanR> | well if you're always operating on only one end of this list |
| 22:16:49 | <EvanR> | better make that end the list beginning |
| 22:17:03 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 245 seconds) |
| 22:18:11 | <EvanR> | if you operate on both ends equally often, there is the functional queue ([Task],[Task]) where one list is backwards |
| 22:19:15 | <Guest87> | Always operating on one end |
| 22:20:19 | <EvanR> | that being said if "n" is not that much it probably doesn't matter either way |
| 22:20:50 | <Guest87> | I am worried some code reviewer will shoot this whole solution down regardless of what `n` is :/ |
| 22:21:16 | <EvanR> | boils down to annoying the reader again |
| 22:21:16 | <Guest87> | But also, I could just do the list implementation if that happens |
| 22:21:50 | <Guest87> | Realizing how different/poorly statement my original problem was |
| 22:22:21 | <Guest87> | Now that the context is here, the problem statement would be "Is there a way to do `addCont` without this unwrapping behavior?" |
| 22:22:30 | <EvanR> | step 1. understand the question |
| 22:22:35 | <EvanR> | step 0. write a proper question |
| 22:23:39 | <EvanR> | you are shadowing t twice in your code so it's hard to grok what is going on |
| 22:24:12 | → | Square joins (~Square4@user/square) |
| 22:24:25 | <haskellbridge> | <loonycyborg> you don't even have a list of tasks |
| 22:24:31 | <haskellbridge> | <loonycyborg> only a way to calculate them |
| 22:25:27 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:25:57 | <EvanR> | alright addCont takes what seems to be an error handler and a program name / input string. Then it calls continue but but continue doesn't return an Either as far as I can tell |
| 22:26:03 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:26:35 | <monochrom> | list of length n is just as inefficient as function chain of length n. |
| 22:27:17 | <EvanR> | but if fixed maybe this addCont produces a sort of recursive "object" as in OOP. But only a single one, not adding anything to anything |
| 22:27:27 | <monochrom> | If there is a code reviewer who does not treat both equally, well, I guess that's why you're paid to appease an arbitrary code reviewer. |
| 22:27:29 | × | Square2 quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 22:28:12 | <Guest87> | EvanR damn yea, the shadowing is real bad. Here is the full code without shadowing |
| 22:28:13 | <Guest87> | https://paste.tomsmeding.com/4T0PUPHR |
| 22:28:47 | <EvanR> | still, continue returns a Task, not a function to apply input to |
| 22:28:52 | <EvanR> | much less returning an Either |
| 22:29:15 | <EvanR> | though if you install GHC you would already know this |
| 22:29:54 | <haskellbridge> | <loonycyborg> honestly I'd recommend adding type annotations :P |
| 22:30:20 | <EvanR> | Right t2 seems to have a new string, but then you pass it into the recursive call where a function was supposed to be |
| 22:30:44 | <Guest87> | Ah crap, this is what I get for trying to port non-pure code without a type checker |
| 22:30:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 22:31:00 | <EvanR> | in addStep you use f but f is not introduced anywhere |
| 22:31:46 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 22:32:57 | <EvanR> | yeah a type signature for addCont and addStep ok all top level definitions here would go a long way |
| 22:33:52 | <Guest87> | Thank you for feedback, adding those |
| 22:40:31 | × | roconnor quits (~quassel@rocq/roconnor) (Ping timeout: 265 seconds) |
| 22:41:45 | → | roconnor joins (~quassel@rocq/roconnor) |
| 22:41:51 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:43:22 | <Guest87> | Holy shit haskell playground is a thing now |
| 22:46:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 22:47:44 | <EvanR> | > let tasks = [(++ "!"), (++ "world"), (++ " "), (++ "Hello")] in foldl (.) id tasks "" |
| 22:47:46 | <lambdabot> | "Hello world!" |
| 22:48:02 | <EvanR> | operating on the beginning of this list is operating on the "last task" |
| 22:48:11 | × | cheater quits (~Username@user/cheater) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 22:50:16 | <EvanR> | foldl (.) id combines them "first task" first |
| 22:52:00 | <EvanR> | the "" at the end is the initial input |
| 22:53:24 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 276 seconds) |
| 22:54:44 | <EvanR> | > foldl (.) id [t4, t3, t2, t1] initial |
| 22:54:45 | <lambdabot> | error: |
| 22:54:45 | <lambdabot> | • Variable not in scope: t4 :: c -> c |
| 22:54:45 | <lambdabot> | • Perhaps you meant one of these: |
| 22:55:11 | <EvanR> | > foldl (.) id [z, y, x, w] initial |
| 22:55:13 | <lambdabot> | error: Variable not in scope: initial |
| 22:55:16 | <EvanR> | > foldl (.) id [z, y, x, w] i |
| 22:55:17 | <lambdabot> | error: |
| 22:55:17 | <lambdabot> | • Couldn't match expected type ‘Expr -> Expr’ |
| 22:55:17 | <lambdabot> | with actual type ‘Expr’ |
| 22:56:14 | <EvanR> | > foldl (.) id [h, g, f] i |
| 22:56:16 | <lambdabot> | h (g (f i)) |
| 22:57:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:59:22 | <Guest87> | Okay, very sorry for the previous code. Here is it with ghc |
| 22:59:23 | <Guest87> | https://play.haskell.org/saved/RpqxGbLD |
| 23:01:34 | <haskellbridge> | <loonycyborg> you can turn [IO Task] into IO [Task] using "sequence" function |
| 23:03:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 23:03:39 | <haskellbridge> | <loonycyborg> probably clearer would be to build a list of them and then sequence it |
| 23:03:47 | <EvanR> | alright you have the issue that the meat of your post never happens since beginRun never gets around to it |
| 23:03:54 | <EvanR> | but yeah |
| 23:06:01 | <EvanR> | I presume you want the result of each task to be threaded into the next one |
| 23:06:54 | <Guest87> | +haskellbridge I think what you are describing is what I concluded to be the way to do this efficiently, but I also don't have an intuition for what "sequencing something" means, so I am not sure |
| 23:06:57 | <EvanR> | [String -> IO (Either String String)] |
| 23:07:24 | <EvanR> | this function stands for a Task without the explicit type for it |
| 23:07:37 | <EvanR> | the list can be combined using a fold |
| 23:08:13 | <EvanR> | to get a final String -> IO (Either String String) to run on the initial input |
| 23:08:29 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 23:09:00 | <emojelly> | Remember my performance drama, where profiling didn't help? I think I found at least part of the issue, through experimentation. |
| 23:09:15 | × | sprotte24_ quits (~sprotte24@p200300d16f15a4001c8bedf899879cb7.dip0.t-ipconnect.de) (Quit: Leaving) |
| 23:09:20 | <emojelly> | It seems to be related to how many Monad Transformers I layer. Partly also what those Monad Transformers are. |
| 23:09:24 | <Guest87> | EvanR correct. Running a single Task could require running more Task until the final result is obtained |
| 23:09:28 | <emojelly> | It seems to grow hyperlinearly with each transformer. |
| 23:10:35 | <emojelly> | I tried with an onion made of a few IdentityTs and Either, and it's enough to blow the runtime up massively. |
| 23:10:46 | <Guest87> | So having a list of Task is the correct thing to do here instead of "squashing it all up" into one Task? |
| 23:10:58 | <EvanR> | the list is there so you can edit it |
| 23:11:08 | <EvanR> | if it was a fixed sequence of tasks you wouldn't need it |
| 23:11:57 | <emojelly> | I'm now rewriting my Coroutine-code in Pipes, because that claims to be "fast", specifically also by internally weakening the monad transformer laws. |
| 23:12:20 | <Guest87> | EvanR: That's a good argument, I don't know why I am being so stubborn about not having a list |
| 23:12:33 | <Guest87> | Maybe I just miss working with functions |
| 23:13:04 | <Guest87> | Is there a proper name/term for the problem I am running into when I do it all with one Task? |
| 23:13:27 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:14:28 | <EvanR> | functions in haskell are blackboxes the only thing you do with them, other than pass them around, is apply them to an argument |
| 23:14:55 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 23:14:55 | <emojelly> | My Monad/Monad Transformer, mixed in with the one from the test framework (Hedgehog), is quite an impressive layer of Coroutine, ExceptT, ReaderT, WriterT, Maybe, IdentityT... I know WriterT has a problem, but even if I try a more minimal example consisting just of Coroutine, IdentityT, and Either, just adding an IdentityT can make things multiple times slower. |
| 23:15:01 | → | j1n37 joins (~j1n37@user/j1n37) |
| 23:16:16 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 23:16:34 | <emojelly> | This is a bit of a bummer, because I was stupidly assuming that Monad Transformers were mostly "free" in terms of performance, at least in terms of just being part of the type, without much actual usage. But that does not seem to be the case at all. Even an IdentityT can wreak havoc if you e.g. fmap through it (i.e. actually follow transformer laws). |
| 23:16:56 | <EvanR> | Guest87, question, what is the "empty list" of tasks supposed to do |
| 23:17:39 | <EvanR> | or is it never empty |
| 23:18:14 | <emojelly> | I guess this is part of why people use effectful these days? But my usage of Coroutine specifically precludes effectful, I think. |
| 23:18:24 | <Guest87> | Yea for now I am assuming I at least have (Task "identityProgram" startingInput (\t -> return Nothing)) |
| 23:18:39 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:18:48 | <EvanR> | Guest87, something like ... https://paste.tomsmeding.com/JF0HROx2 |
| 23:19:06 | <EvanR> | well you return Nothing so what goes on to the next program |
| 23:19:40 | × | xff0x quits (~xff0x@2405:6580:b080:900:1c0d:6c97:349e:6228) (Ping timeout: 265 seconds) |
| 23:19:59 | × | hattckory quits (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds) |
| 23:20:05 | <Guest87> | In `addCont`, Nothing is where I end up passing on the result to the next task |
| 23:20:12 | <Guest87> | Otherwise, Nothing means "nothing left to do" |
| 23:20:25 | <EvanR> | but there is no result |
| 23:20:56 | <EvanR> | but since the code never runs in your case, that question doesn't need to be answered |
| 23:21:16 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 23:23:26 | <EvanR> | in my paste, addCont would simply be prepending another Task to the list |
| 23:23:50 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 23:23:54 | → | xff0x joins (~xff0x@2405:6580:b080:900:1c0d:6c97:349e:6228) |
| 23:25:10 | <Guest87> | EvanR yup, this is easy to do with a list, I am just being a dummy and feel like using a list means I haven't figured out the elegant solution |
| 23:26:28 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 23:26:46 | <EvanR> | turning a non-empty [Task] into a Task using a Task -> Task -> Task... fairly "elegant" I'd say |
| 23:27:21 | <Guest87> | xD I am just making things hard for myself I guess |
| 23:28:14 | <Guest87> | Are there any haskell libraries that implement whatever I am dealing with here? At one point I was re-learning the Cont monad, but this doesn't feel like Cont exactly |
| 23:29:55 | <EvanR> | my paste is the entirety of the problem afaiui |
| 23:30:02 | <EvanR> | hardly needs a library |
| 23:30:26 | <EvanR> | but in general "Tasks" sounds like they'd be running concurrently and might need to communicate with each other, and the async library is pretty nice there |
| 23:31:19 | <EvanR> | :t foldl1 |
| 23:31:20 | <lambdabot> | Foldable t => (a -> a -> a) -> t a -> a |
| 23:31:30 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:32:19 | → | hattckory joins (~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) |
| 23:32:41 | <EvanR> | if it was just a bunch of IO actions in a list that needed to run, that's even less of a library, just sequence :: [IO a] -> IO [a] |
| 23:32:49 | ← | jleightcap parts (7bc4014b62@user/jleightcap) () |
| 23:34:05 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 23:34:16 | <EvanR> | and my posted code can probably be golfed with some pointfree compositions |
| 23:34:26 | <EvanR> | to get that a -> a -> a smaller |
| 23:35:48 | × | cipherrot quits (~znc-user@user/petrichor) (Ping timeout: 245 seconds) |
| 23:36:49 | <Guest87> | EvanR: I think your Task type needs to be `String -> IO (Either String Task)` (assuming recursive `type` worked) |
| 23:36:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 23:38:21 | <EvanR> | it does not |
| 23:38:44 | <EvanR> | I didn't see the point of the Task datatype as stated |
| 23:39:09 | → | sayurc_ joins (~sayurc@169.150.203.34) |
| 23:39:19 | × | sayurc quits (~sayurc@169.150.203.34) (Read error: Connection reset by peer) |
| 23:39:37 | <EvanR> | it amounted to a function returning a thing to pass to the next function, and a string to pass into that function |
| 23:40:45 | <Guest87> | The issue is that when I "run" a Task, it either gives a result, or gives me another Task to get the final result |
| 23:41:03 | <Guest87> | Kinda like a trampoline situation I think |
| 23:42:00 | → | petrichor joins (~znc-user@user/petrichor) |
| 23:42:40 | <EvanR> | not in my paste, the next task is next in the list that you maintained |
| 23:42:58 | <EvanR> | if the task itself is supposed to determine that, that's another problem |
| 23:43:14 | <EvanR> | then "adding" a task from outside doesn't make much sense |
| 23:44:59 | <EvanR> | if running the task is supposed to yield a new task and so on, that's more like free monads |
| 23:45:13 | <EvanR> | plus interpreter |
| 23:46:08 | <EvanR> | but if all you're doing is IO actions that sometimes fail early |
| 23:46:24 | <EvanR> | that would be a pretty simple free monad |
| 23:46:45 | <EvanR> | or you could just use IO exceptions to fail early, and catch that exception |
| 23:46:52 | <EvanR> | and write IO actions |
| 23:47:02 | <EvanR> | if you were actually using haskell |
| 23:47:03 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:50:00 | <EvanR> | in both cases you would not be able to outside force a task to suddenly be happening at the end |
| 23:50:21 | <Guest87> | Does "Free" in free monad mean "we get this for free", or does it mean something else? |
| 23:50:50 | <EvanR> | it sure does |
| 23:50:56 | <EvanR> | unless you get more specific |
| 23:52:01 | <EvanR> | but warning, just writing an IO program is already this "task runs and generates the next task to run until the final result" |
| 23:52:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 23:52:28 | <haskellbridge> | <Bowuigi> It means "we get monadic structure for free" (or rather, from a functor) |
| 23:52:39 | <EvanR> | and stitching is just (>>=) :: IO a -> (a -> IO b) -> IO b |
| 23:53:27 | <EvanR> | if a = b = String |
| 23:53:40 | <EvanR> | then your pipeline could be just an IO String |
| 23:54:02 | <EvanR> | and I lied you can tack more IO actions before and after |
| 23:55:45 | <Guest87> | I am reading the following: |
| 23:55:45 | <Guest87> | https://www.haskellforall.com/2012/06/you-could-have-invented-free-monads.html |
| 23:56:23 | <Guest87> | and it feels kinda similar to what I am dealing with |
| 23:58:16 | <Guest87> | The `catch` function feels similar to my `addCont` |
| 23:59:13 | <EvanR> | say you have the IO String |
| 23:59:27 | <EvanR> | and you want to put String -> IO String "at the end" (post process) |
| 23:59:35 | <EvanR> | that's just >>= |
All times are in UTC on 2025-04-10.