Logs on 2023-04-11 (liberachat/#haskell)
| 00:00:06 | → | mauke_ joins (~mauke@user/mauke) |
| 00:02:22 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 00:02:25 | × | mauke quits (~mauke@user/mauke) (Ping timeout: 268 seconds) |
| 00:02:25 | mauke_ | is now known as mauke |
| 00:06:10 | <hololeap> | whatsupdoc: is that the one kmett has been working on? |
| 00:07:18 | × | zeenk quits (~zeenk@2a02:2f04:a307:2300::7fe) (Quit: Konversation terminated!) |
| 00:11:36 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Quit: Lost terminal) |
| 00:17:02 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 00:22:34 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 276 seconds) |
| 00:41:38 | → | chanceyan joins (~chanceyan@user/chanceyan) |
| 01:00:35 | <Nosrep> | elixir the language? |
| 01:00:47 | <Nosrep> | ekmett doesn't have any elixir repos in his github and there's 299 repos |
| 01:07:11 | <Axman6> | hololeap: are you thinking about guanxi? |
| 01:07:26 | <Axman6> | elixir's the rubified erlang |
| 01:08:48 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 01:09:42 | <hololeap> | I'm not sure, but I remember kmett saying something about working on a different language |
| 01:10:25 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:10:42 | <hololeap> | I think it runs on jvm |
| 01:11:03 | <hololeap> | rubified erlang sounds cool, honestly |
| 01:13:18 | × | opticblast quits (~Thunderbi@172.58.85.126) (Read error: Connection reset by peer) |
| 01:13:37 | → | opticblast joins (~Thunderbi@172.58.85.126) |
| 01:14:06 | <hololeap> | edwardk_: what was the other language you have been working on, or am I totally off base |
| 01:14:24 | × | opticblast quits (~Thunderbi@172.58.85.126) (Client Quit) |
| 01:16:32 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:18:25 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 01:20:23 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 01:20:25 | <monochrom> | I heard of "Turbo Haskell" :) |
| 01:21:36 | <c_wraith> | hololeap: the Haskell-like that runs on the JVM was ermine. But I don't think edwardk has worked at the place developing that in a long time |
| 01:22:01 | <c_wraith> | well. the haskell-like that runs on the jvm that he was working on |
| 01:22:07 | <hololeap> | but he _did_? this was a random convo on IRC and yeah it was at least a couple years ago |
| 01:22:32 | <c_wraith> | yes. Probably more than 10 years ago, now |
| 01:22:41 | <hololeap> | oh, well not that long ago |
| 01:23:02 | <c_wraith> | it easily can come up in conversation more recently |
| 01:23:21 | <hololeap> | my impression was that it was current work |
| 01:24:29 | → | nunggu joins (~q@user/nunggu) |
| 01:24:31 | <monochrom> | Every car was once a new car. Every work was once current work. >:D |
| 01:25:10 | <monochrom> | http://www.vex.net/~trebla/humour/tautologies.html #13 |
| 01:25:57 | <c_wraith> | I feel like if I really looked, I could find some cars that were built old. :P |
| 01:27:34 | <monochrom> | Fortunately I happened to not talk of violins. Some people make intially-old violins to fake Strads. >:D |
| 01:27:55 | × | leah2 quits (~leah@vuxu.org) (Ping timeout: 252 seconds) |
| 01:27:56 | <hololeap> | oldsmobile QED |
| 01:28:11 | <monochrom> | hahaha |
| 01:29:53 | <hololeap> | I saw something that was saying Stradivarius violins have a unique sound because they were made from trees that grew in the little ice age, which made the wood more dense |
| 01:30:29 | × | nunggu quits (~q@user/nunggu) (Remote host closed the connection) |
| 01:33:52 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 248 seconds) |
| 01:38:43 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
| 01:43:01 | × | czy quits (~user@host-140-25.ilcub310.champaign.il.us.clients.pavlovmedia.net) (Remote host closed the connection) |
| 01:43:17 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 01:51:07 | × | xff0x quits (~xff0x@ai098135.d.east.v6connect.net) (Ping timeout: 248 seconds) |
| 01:52:11 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 01:52:33 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 01:53:24 | → | nate1 joins (~nate@98.45.169.16) |
| 01:55:23 | <Nosrep> | step 1. refrigerated greenhouse 2. ??? 3. profit |
| 01:58:21 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 268 seconds) |
| 01:59:28 | → | zq joins (~zq@xorshift.org) |
| 01:59:30 | <zq> | hello |
| 01:59:43 | <zq> | ml module functor == haskell typeclass functor? |
| 02:00:25 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 02:01:33 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 02:05:01 | → | leah2 joins (~leah@vuxu.org) |
| 02:10:20 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 265 seconds) |
| 02:11:17 | → | nunggu joins (~q@user/nunggu) |
| 02:12:58 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 02:16:37 | <probie> | zq: not at all |
| 02:16:51 | × | td_ quits (~td@i53870914.versanet.de) (Ping timeout: 268 seconds) |
| 02:17:35 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Ping timeout: 260 seconds) |
| 02:18:21 | → | td_ joins (~td@i5387091F.versanet.de) |
| 02:18:44 | → | nate1 joins (~nate@98.45.169.16) |
| 02:27:03 | × | jumpnbrownweasel quits (~jumpnbrow@2603-800c-240f-1c55-8db8-2c23-1ffe-bf07.res6.spectrum.com) (Quit: Leaving) |
| 02:31:32 | <ryantrinkle> | any recommendation on how to emit a warning or error if someone uses a particular library/module *without* using a particular compiler plugin? |
| 02:31:56 | <ryantrinkle> | i just wrote a lib where users will suffer an enormous performance penalty if they forget to use the plugin |
| 02:32:36 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 02:33:44 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 02:33:59 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:35:39 | → | jwiegley_ joins (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
| 02:36:18 | × | jwiegley quits (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Read error: Connection reset by peer) |
| 02:38:25 | → | pieguy128_ joins (~pieguy128@bras-base-mtrlpq5031w-grc-50-65-93-192-141.dsl.bell.ca) |
| 02:38:33 | <probie> | ryantrinkle: Do you also control the compiler plugin? Definitely a hack, but if so you can add a type checker plugin to it that can solve a specific constraint, and then add that otherwise unsolvable constraint to your library |
| 02:38:55 | × | pieguy128 quits (~pieguy128@bas8-montreal02-65-93-194-11.dsl.bell.ca) (Ping timeout: 260 seconds) |
| 02:43:18 | <probie> | e.g. `class UsingCompilerPluginFoo a where` and then somewhere in your library have a useless dummy function `usingCompilerPlugin :: UsingCompilerPluginFoo () => ()` to block compilation unless the plugin is being used |
| 02:46:28 | <jackdk> | probie: `-XMultiParamTypeClasses` allows nullary type classes; can you use that here? Also, you could put such a type class on the library functions that require the plugin, instead of a magic binding |
| 02:48:35 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 02:53:51 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 268 seconds) |
| 02:54:23 | → | opticblast joins (~Thunderbi@172.58.85.126) |
| 02:55:32 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 02:59:24 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:59:24 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:59:24 | finn_elija | is now known as FinnElija |
| 03:01:17 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 03:01:25 | <probie> | jackdk: does ghc promise to erase "empty" type classes, or is there a risk it's going to rewrite `C => T` to `() -> T` instead of `T`? |
| 03:03:34 | <jackdk> | I dunno. I jut remember seeing it in the doc for that extension. If it rewrites it to a silly function, that's easily fixable with the plugin anyway |
| 03:06:11 | × | Vq quits (~vq@90-227-192-206-no77.tbcn.telia.com) (Ping timeout: 268 seconds) |
| 03:07:57 | → | Vq joins (~vq@90-227-192-206-no77.tbcn.telia.com) |
| 03:10:38 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 03:14:52 | × | jero98772 quits (~jero98772@2800:484:1d84:9000::2) (Remote host closed the connection) |
| 03:19:01 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 240 seconds) |
| 03:33:48 | × | opticblast quits (~Thunderbi@172.58.85.126) (Ping timeout: 255 seconds) |
| 03:36:13 | → | opticblast joins (~Thunderbi@172.58.85.126) |
| 03:37:18 | → | czy joins (~user@host-140-25.ilcub310.champaign.il.us.clients.pavlovmedia.net) |
| 03:38:11 | → | pyook joins (~puke@user/puke) |
| 03:44:17 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 03:45:39 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 03:49:13 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Client Quit) |
| 03:49:57 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 03:50:01 | × | matthews quits (~matthews@gentoo/developer/matthew) (Quit: ZNC 1.8.2+deb2+b1 - https://znc.in) |
| 03:50:29 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 03:56:51 | × | opticblast quits (~Thunderbi@172.58.85.126) (Ping timeout: 260 seconds) |
| 04:20:31 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 240 seconds) |
| 04:23:16 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 04:23:17 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 04:23:17 | → | wroathe joins (~wroathe@user/wroathe) |
| 04:24:12 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 04:30:03 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 255 seconds) |
| 04:30:32 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 04:30:40 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds) |
| 04:32:22 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 04:41:15 | → | mbuf joins (~Shakthi@49.207.178.186) |
| 04:44:54 | → | trev joins (~trev@user/trev) |
| 04:59:10 | → | Feuermagier_ joins (~Feuermagi@user/feuermagier) |
| 05:00:13 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Read error: Connection reset by peer) |
| 05:00:26 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 05:01:13 | × | Feuermagier_ quits (~Feuermagi@user/feuermagier) (Client Quit) |
| 05:08:54 | → | cheater_ joins (~Username@user/cheater) |
| 05:10:29 | × | cheater quits (~Username@user/cheater) (Ping timeout: 250 seconds) |
| 05:10:38 | cheater_ | is now known as cheater |
| 05:20:10 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 05:26:03 | → | bgs joins (~bgs@212-85-160-171.dynamic.telemach.net) |
| 05:27:03 | → | freeside joins (~mengwong@50.216.111.242) |
| 05:30:48 | × | mikess quits (~sam@user/mikess) (Ping timeout: 264 seconds) |
| 05:31:30 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:40:11 | → | hopelessness[m] joins (~hopelessn@2001:470:69fc:105::3:4043) |
| 05:43:30 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 260 seconds) |
| 05:46:21 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 05:46:29 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 05:50:55 | × | cheater quits (~Username@user/cheater) (Read error: Connection reset by peer) |
| 05:51:54 | → | cheater joins (~Username@user/cheater) |
| 05:54:19 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 06:00:53 | → | michalz joins (~michalz@185.246.204.101) |
| 06:04:12 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 06:05:26 | × | nunggu quits (~q@user/nunggu) (Ping timeout: 255 seconds) |
| 06:11:06 | → | harveypwca joins (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
| 06:11:29 | → | MajorBiscuit joins (~MajorBisc@31-23-159.netrun.cytanet.com.cy) |
| 06:15:19 | → | kenran joins (~user@user/kenran) |
| 06:20:59 | × | chanceyan quits (~chanceyan@user/chanceyan) (Quit: Client closed) |
| 06:23:58 | × | _leo___ quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 06:24:47 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 260 seconds) |
| 06:38:48 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 06:39:13 | → | gurkenglas joins (~gurkengla@dynamic-046-114-181-068.46.114.pool.telefonica.de) |
| 06:40:51 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 06:50:42 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 06:53:36 | × | ddellacosta quits (~ddellacos@146.70.171.100) (Ping timeout: 264 seconds) |
| 06:55:00 | → | Guest99 joins (~Guest99@host-im9myvj.static.zeelandnet.nl) |
| 06:58:57 | → | vglfr joins (~vglfr@88.155.17.187) |
| 07:06:09 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:807f:2761:46c9:9711) |
| 07:07:16 | → | zeenk joins (~zeenk@2a02:2f04:a307:2300::7fe) |
| 07:08:08 | × | zaquest quits (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 07:11:14 | → | acidjnk joins (~acidjnk@p200300d6e715c407d4f5be9b40c24016.dip0.t-ipconnect.de) |
| 07:15:35 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 07:15:47 | → | ddellacosta joins (~ddellacos@146.70.185.100) |
| 07:17:35 | → | zaquest joins (~notzaques@5.130.79.72) |
| 07:19:40 | → | chanceyan joins (~chanceyan@user/chanceyan) |
| 07:20:32 | → | kuribas joins (~user@188.189.245.25) |
| 07:25:00 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 07:25:45 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 07:32:50 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 07:39:09 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:39:42 | → | mastarija joins (~mastarija@2a05:4f46:e03:6000:95dc:f9bd:1c2a:3be8) |
| 07:40:20 | × | zeenk quits (~zeenk@2a02:2f04:a307:2300::7fe) (Remote host closed the connection) |
| 07:40:42 | → | zeenk joins (~zeenk@2a02:2f04:a307:2300::fba) |
| 07:41:19 | <JensPetersen[m]> | I have a space character operator ("ab" +-+ "cd == "ab " +-+ " cd" = ), but now I can't decide what it should do for an empty string: "ab" +-+ "", hmm |
| 07:42:34 | <hopelessness[m]> | according to the first example I would think that `"ab "` and `"ab"` would be equally valid |
| 07:42:51 | <hopelessness[m]> | imo `"ab"` would make more sense on the context I'm inferring |
| 07:47:44 | × | freeside quits (~mengwong@50.216.111.242) (Ping timeout: 248 seconds) |
| 07:50:23 | × | harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
| 07:52:09 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 07:53:51 | <mauke> | > ab" +-+ "cd == "ab " +-+ " cd" = |
| 07:53:53 | <lambdabot> | <hint>:1:32: error: parse error on input ‘=’ |
| 07:54:40 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:55:50 | × | chanceyan quits (~chanceyan@user/chanceyan) (Quit: Client closed) |
| 07:56:24 | × | ddellacosta quits (~ddellacos@146.70.185.100) (Ping timeout: 265 seconds) |
| 07:57:05 | → | ddellacosta joins (~ddellacos@146.70.171.100) |
| 07:58:35 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 08:02:52 | <tomsmeding> | JensPetersen[m]: spec seems to be to concatenate while removing any spaces in between, right? In which case indeed "ab" +-+ "" == "ab" |
| 08:03:42 | <JensPetersen[m]> | tomsmeding: Yeah I feel that is right - maybe I just want an append space operator too :) |
| 08:03:48 | × | drdo quits (~drdo@bl7-76-103.dsl.telepac.pt) (Ping timeout: 255 seconds) |
| 08:05:46 | <tomsmeding> | @let a +␠+ b = a ++ " " ++ b |
| 08:05:47 | <lambdabot> | Defined. |
| 08:07:58 | × | Guest99 quits (~Guest99@host-im9myvj.static.zeelandnet.nl) (Quit: Client closed) |
| 08:09:27 | <mauke> | > let a +??+ b = unwords (words a ++ words b) in "ab " +??+ " cd" |
| 08:09:29 | <lambdabot> | "ab cd" |
| 08:10:06 | × | kuribas quits (~user@188.189.245.25) (Ping timeout: 255 seconds) |
| 08:10:19 | → | freeside joins (~mengwong@50.216.111.242) |
| 08:13:02 | <JensPetersen[m]> | aha |
| 08:13:29 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 08:13:57 | <JensPetersen[m]> | Yeah that is a simple implementation indeed |
| 08:16:39 | → | mmhat joins (~mmh@p200300f1c7106e86ee086bfffe095315.dip0.t-ipconnect.de) |
| 08:17:42 | × | mmhat quits (~mmh@p200300f1c7106e86ee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 08:18:14 | → | Rembane joins (~Rembane@li346-36.members.linode.com) |
| 08:19:52 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 08:20:35 | × | ubert quits (~Thunderbi@p548c84d6.dip0.t-ipconnect.de) (Quit: ubert) |
| 08:23:45 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 08:24:20 | × | winny quits (~weechat@user/winny) (Quit: kernel) |
| 08:25:01 | → | winny joins (~weechat@user/winny) |
| 08:39:45 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 08:43:05 | <ncf> | zq: no, and it also has nothing to do with what C++ calls a functor, or what Prolog calls a functor (all four are different concepts 🙃) |
| 08:58:24 | <Hecate> | ahah yes the famous OCaml/Haskell/C++/Prolog dichotomy |
| 09:00:07 | × | pareto-optimal-d quits (~pareto-op@2001:470:69fc:105::1:b61f) (Quit: You have been kicked for being idle) |
| 09:00:07 | × | ikervagyok[m] quits (~ikervagyo@2001:470:69fc:105::2:f119) (Quit: You have been kicked for being idle) |
| 09:01:21 | <hopelessness[m]> | that seems more like a quartotomy :p |
| 09:01:27 | → | __monty__ joins (~toonn@user/toonn) |
| 09:01:38 | <hopelessness[m]> | s/quartotomy/quarchotomy/ |
| 09:02:54 | → | Guest66 joins (~Guest66@140.124.184.119) |
| 09:04:06 | → | chanceyan joins (~chanceyan@user/chanceyan) |
| 09:05:07 | <hopelessness[m]> | wiktionary doesn't list it as a word, even though it acknowledges [trichotomy](https://en.m.wiktionary.org/wiki/trichotomy#English) as analog to [dichotomy](https://en.m.wiktionary.org/wiki/dichotomy#English) |
| 09:05:09 | <merijn> | Hecate: Wouldn't that be a tetrachotomy? |
| 09:05:20 | <merijn> | hopelessness[m]: Wrong language prefix ;) |
| 09:05:36 | <Hecate> | merijn: yes that would be the greek word indeed |
| 09:05:41 | <hopelessness[m]> | ahhhh heck |
| 09:05:42 | <hopelessness[m]> | out-nerded |
| 09:05:51 | <hopelessness[m]> | * wiktionary doesn't list it as a word, even though it acknowledges [trichotomy](https://en.m.wiktionary.org/wiki/trichotomy#English) as analog to [dichotomy](https://en.m.wiktionary.org/wiki/dichotomy#English) |
| 09:06:15 | <merijn> | hopelessness[m]: I'm just extrapolating from di/tri/tetra in chemistry |
| 09:07:26 | <hopelessness[m]> | I was never good in chemistry 😆 |
| 09:08:23 | → | ubert joins (~Thunderbi@2a02:8109:abc0:6434:81f3:78d3:e012:2761) |
| 09:22:44 | × | mastarija quits (~mastarija@2a05:4f46:e03:6000:95dc:f9bd:1c2a:3be8) (Quit: WeeChat 3.7.1) |
| 09:36:50 | → | NiceBird joins (~NiceBird@185.133.111.196) |
| 09:38:17 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Remote host closed the connection) |
| 09:44:43 | × | ft quits (~ft@p4fc2a88b.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:46:16 | × | chanceyan quits (~chanceyan@user/chanceyan) (Quit: Client closed) |
| 09:49:55 | × | Guest66 quits (~Guest66@140.124.184.119) (Quit: Client closed) |
| 09:51:20 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:807f:2761:46c9:9711) (Ping timeout: 246 seconds) |
| 09:51:37 | → | gensyst joins (~gensyst@user/gensyst) |
| 09:53:45 | <gensyst> | Have you worked yet with "nixpkgs support for incremental Haskell builds" ? |
| 09:53:52 | <gensyst> | Is this already done? |
| 09:54:24 | <gensyst> | It's GHC 9.4 or later only supposedly, because only >= GHC 9.4 has file hashing to detect changes. |
| 09:57:45 | × | vglfr quits (~vglfr@88.155.17.187) (Ping timeout: 265 seconds) |
| 10:09:54 | × | gurkenglas quits (~gurkengla@dynamic-046-114-181-068.46.114.pool.telefonica.de) (Quit: leaving) |
| 10:10:17 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 265 seconds) |
| 10:15:51 | <fendor[m]> | I may have asked before, but is it typeclasses or type classes? or is either fine? |
| 10:16:43 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 10:16:54 | <merijn> | fendor[m]: I think the report uses the latter? |
| 10:17:44 | <fendor[m]> | realworldhaskell and lyah use the former, wikipedia uses the latter |
| 10:18:47 | <fendor[m]> | but yeah, the report uses the latter, going to use that as my source of truth, thanks! |
| 10:19:08 | → | mei joins (~mei@user/mei) |
| 10:19:56 | → | gurkenglas joins (~gurkengla@dynamic-046-114-181-068.46.114.pool.telefonica.de) |
| 10:31:01 | → | vglfr joins (~vglfr@88.155.17.187) |
| 10:38:46 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 10:39:45 | → | saolof joins (~saolof@2001:2002:5ae4:c319:4108:8be0:bf78:a848) |
| 10:44:30 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Ping timeout: 260 seconds) |
| 10:46:17 | × | zeenk quits (~zeenk@2a02:2f04:a307:2300::fba) (Quit: Konversation terminated!) |
| 10:51:05 | × | forell quits (~forell@user/forell) (Ping timeout: 250 seconds) |
| 10:53:02 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 10:54:19 | → | forell joins (~forell@user/forell) |
| 10:56:52 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 10:58:09 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 10:58:30 | → | xff0x joins (~xff0x@ai098135.d.east.v6connect.net) |
| 11:03:08 | → | kenran` joins (~user@user/kenran) |
| 11:04:31 | × | kenran quits (~user@user/kenran) (Ping timeout: 240 seconds) |
| 11:09:25 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:c066:a6a4:43b5:25e) |
| 11:19:49 | × | gurkenglas quits (~gurkengla@dynamic-046-114-181-068.46.114.pool.telefonica.de) (Remote host closed the connection) |
| 11:21:33 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 11:21:46 | → | gurkenglas joins (~gurkengla@dynamic-046-114-181-068.46.114.pool.telefonica.de) |
| 11:28:49 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 276 seconds) |
| 11:30:55 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.8) |
| 11:35:23 | × | pyook quits (~puke@user/puke) (Read error: Connection reset by peer) |
| 11:35:36 | → | pyook joins (~puke@user/puke) |
| 11:43:28 | × | vglfr quits (~vglfr@88.155.17.187) (Ping timeout: 248 seconds) |
| 11:43:32 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 11:43:40 | → | vglfr joins (~vglfr@88.155.17.187) |
| 11:46:40 | × | anpad quits (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 11:47:01 | → | anpad joins (~pandeyan@user/anpad) |
| 11:50:06 | → | enoq joins (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) |
| 11:50:58 | × | vglfr quits (~vglfr@88.155.17.187) (Ping timeout: 268 seconds) |
| 11:52:08 | → | vglfr joins (~vglfr@88.155.17.187) |
| 11:58:46 | × | vglfr quits (~vglfr@88.155.17.187) (Ping timeout: 252 seconds) |
| 12:03:56 | → | vglfr joins (~vglfr@88.155.17.187) |
| 12:08:38 | → | paulpaul1076 joins (~textual@95-29-5-208.broadband.corbina.ru) |
| 12:09:48 | → | akadude[m] joins (~akadudema@2001:470:69fc:105::2:5bf7) |
| 12:11:45 | × | Vq quits (~vq@90-227-192-206-no77.tbcn.telia.com) (Ping timeout: 255 seconds) |
| 12:13:43 | → | Vq joins (~vq@90-227-192-206-no77.tbcn.telia.com) |
| 12:24:29 | × | Katarushisu quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Quit: The Lounge - https://thelounge.chat) |
| 12:25:40 | → | Katarushisu joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 12:28:06 | <chreekat> | <fendor[m]> "realworldhaskell and lyah use..." <- oh damn is that what's going on |
| 12:28:26 | <chreekat> | I had asked myself the same question and came to the same conclusion (follow the report), but wasn't sure why I was confused in the first place |
| 12:28:28 | <chreekat> | database, data base |
| 12:28:47 | <chreekat> | i think I still prefer typeclass though |
| 12:33:14 | <fendor[m]> | I also feel like typeclass reads slightly more natural, but couldn't give an argument why |
| 12:34:19 | <int-e> | exposure |
| 12:34:47 | <fendor[m]> | yeah I guess that's it |
| 12:34:47 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:35:06 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:9da2:60aa:4250:a867) |
| 12:35:16 | edwardk_ | is now known as edwardk |
| 12:35:38 | <int-e> | (As a data point, I prefer "type class" and I have not read either of those books... but I do prefer "database" and the only reason I see for that is that that's what everybody else uses.) |
| 12:39:41 | <kenran`> | "user name" vs. "username" is the same for me |
| 12:39:54 | <kenran`> | I guess as German it's only natural for the concatenated variant to feel more natural to me though |
| 12:40:28 | kenran` | is now known as kenran |
| 12:42:17 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 12:50:06 | <hopelessness[m]> | haha yeah |
| 12:50:17 | <hopelessness[m]> | I often concatenate even when it's not possible |
| 12:50:37 | <int-e> | . o O ( overconcatenation ) |
| 12:51:05 | <[exa]> | might deserve a hyphen. :D |
| 12:51:19 | <int-e> | [exa]: that would destroy the joke |
| 12:51:33 | <hopelessness[m]> | hyphen-deserving |
| 12:51:37 | <hopelessness[m]> | hyphendeserving |
| 12:51:39 | <yin> | i feel like there's a subtle difference like in 'log in' vs 'login' |
| 12:52:05 | <hopelessness[m]> | mhm |
| 12:52:07 | <ncf> | verb vs noun |
| 12:52:15 | <kenran> | yeah, like verb vs. noun. clean up vs cleanup |
| 12:52:32 | <hopelessness[m]> | ncf: I thought so at first, but both can be used for both, right ... ? |
| 12:52:41 | <hopelessness[m]> | Like there's a clear preferences but I think both work |
| 12:52:53 | <kenran> | I don't think so tbh, but yeah, not a native speaker either |
| 12:53:27 | <kenran> | "The log in was successful" just looks wrong to me, or a commit message like "Cleanup some stuff" |
| 12:53:51 | <hopelessness[m]> | hmm |
| 12:54:06 | <int-e> | You log in with your login (was that spelled "log-in" at some point in the past?) credentials... |
| 12:54:09 | <ncf> | if you're not allergic to prescriptivism, http://www.notaverb.com/login |
| 12:55:37 | <int-e> | (I feel that often these compound terms start out hyphenated and then at some point the hyphen gets dropped for convenience, but I don't know whether this is actually true.) |
| 12:55:53 | <hopelessness[m]> | that seems right, yeah |
| 12:55:55 | <[Leary]> | 'Typeclass' is immediately recognisable as the specific jargon, not any other meaning that could arise from the combination of 'type' and 'class'. 'Database' and 'username' probably arose and persisted for the same reason: they clarify. |
| 12:56:37 | → | yoneda joins (~mike@193.206.102.122) |
| 12:57:08 | <int-e> | . o O ( We didn't learn that in type class. ) |
| 12:57:33 | <ncf> | my favourite dehyphenation is "reëxports" (to stay vaguely on-topic :p) |
| 12:58:23 | <ncf> | (https://hackage.haskell.org/package/composition-prelude-3.0.0.2/docs/Control-Composition.html#g:12) |
| 12:59:04 | <yin> | i have always wondered who needed to come up with "initialize" |
| 13:00:45 | <int-e> | "bootstrap" |
| 13:01:13 | <int-e> | "endianness" (those last two both come from fictional stories) |
| 13:01:46 | <yin> | did they? |
| 13:02:03 | <kenran> | Wait, bootstrap? you mean the usage as verb specifically? |
| 13:03:10 | <int-e> | At least as far as I know. Bootstrapping is Münchhausen (pulling himself out of a swamp by his bootstraps) and "endianness" alludes to the war in Gulliver's Travels about which side to open an egg from. |
| 13:03:21 | <Rembane> | And then war ensues |
| 13:04:37 | <int-e> | Cf. https://www.rfc-editor.org/ien/ien137.txt for endianness. |
| 13:05:28 | <kenran> | int-e: ah, got it. I somehow read that as "the word bootstrap comes from a fictional story", which sounded strange :D |
| 13:06:25 | <int-e> | "Words are failing me to express how eloquent I'm feeling today." |
| 13:07:48 | <merijn> | kenran: It does |
| 13:08:46 | jpds4 | is now known as jpds |
| 13:11:31 | × | kenran quits (~user@user/kenran) (Ping timeout: 276 seconds) |
| 13:14:13 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 13:15:10 | <yin> | int-e: the "Who's on first? Zero or One ??" chapter in your link reminded me on how ridiculous it is that we've abbreviated "prima minuta" to "minute" and "seconda minuta" to "second". |
| 13:15:33 | <yin> | more specifically "pars minuta prima" and "pars minuta seconda" |
| 13:15:53 | <yin> | *secunda apparently |
| 13:16:38 | → | mei joins (~mei@user/mei) |
| 13:17:56 | <merijn> | I love how Amazon's generated example code is just...wrong |
| 13:18:01 | <merijn> | such fune |
| 13:18:07 | <merijn> | I love my life >.< |
| 13:23:29 | × | gensyst quits (~gensyst@user/gensyst) (Quit: Leaving) |
| 13:26:35 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 248 seconds) |
| 13:34:39 | → | mikess joins (~sam@user/mikess) |
| 13:42:20 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 13:42:21 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 13:42:21 | → | wroathe joins (~wroathe@user/wroathe) |
| 13:44:30 | → | tlaxkit joins (~hexchat@170.253.32.109) |
| 13:47:23 | <kuribas> | int-e: doesn't it come from puss in boots? |
| 13:48:16 | <ryantrinkle> | probie: yes, I do; awesome suggestion, thanks! |
| 13:58:24 | → | jero98772 joins (~jero98772@2800:484:1d84:9000::5) |
| 14:00:43 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 260 seconds) |
| 14:03:31 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 276 seconds) |
| 14:04:44 | → | kenran joins (~user@user/kenran) |
| 14:08:18 | → | cfricke joins (~cfricke@user/cfricke) |
| 14:19:12 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 14:23:51 | → | zeenk joins (~zeenk@2a02:2f04:a307:2300::fba) |
| 14:28:14 | → | marinelli joins (~marinelli@gateway/tor-sasl/marinelli) |
| 14:29:15 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:29:42 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 14:29:50 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:33:12 | → | Square joins (~Square4@user/square) |
| 14:38:37 | × | freeside quits (~mengwong@50.216.111.242) (Ping timeout: 276 seconds) |
| 14:39:13 | → | Albina_Pavlovna joins (~Albina_Pa@2603-7000-76f0-76e0-491d-4022-58a1-d85a.res6.spectrum.com) |
| 14:45:13 | × | marinelli quits (~marinelli@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 14:56:09 | → | freeside joins (~mengwong@50.216.111.242) |
| 14:59:55 | → | olle joins (~olle@h-155-4-129-160.NA.cust.bahnhof.se) |
| 15:00:21 | <olle> | Let's say I have an effectful read inside a function that depends on logic. Is there a way to move it out so I don't have to use IO there? |
| 15:00:36 | <olle> | One (ugly?) way could be to simply preload it. |
| 15:00:58 | <hopelessness[m]> | you mean reading a file? |
| 15:01:11 | <olle> | Reading anything - db, file, url, ... |
| 15:02:00 | → | MatthiasG joins (~MatthiasG@202.133.199.92) |
| 15:02:23 | <hopelessness[m]> | you could either pass the data to the function and then `effectfulRead >>= f` where `f` is the processing function, or you make your function return an `IO` action as well |
| 15:02:39 | <hopelessness[m]> | In theory theres `performUnsafeIO` but ... don't use that |
| 15:02:57 | <olle> | Hm |
| 15:03:13 | <olle> | No algebraic effects in haskell, right? |
| 15:03:14 | <hopelessness[m]> | s/performUnsafeIO/unsafePerformIO/ |
| 15:03:30 | <TheMatten[m]> | olle: There're libraries for that |
| 15:03:39 | <hopelessness[m]> | what do you want to do in the first place? |
| 15:03:42 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 15:05:13 | <olle> | Looking for strategies to extend the "functional core" of a system. I don't work in Haskell tho, just thought I'd ask here too. :) |
| 15:05:40 | <hopelessness[m]> | hm ok |
| 15:06:05 | <hopelessness[m]> | do you have an example in mind? I have a hard time understanding what you mean, I think 😅 |
| 15:06:26 | <olle> | Not currently. :( I need one. |
| 15:06:53 | <hopelessness[m]> | ok, let me give a setup maybe |
| 15:09:13 | × | freeside quits (~mengwong@50.216.111.242) (Read error: Connection reset by peer) |
| 15:09:29 | <hopelessness[m]> | (unlines . reverse . lines) <$> readFile "foo.txt" |
| 15:09:58 | <hopelessness[m]> | this is just a basic example of reading a file and then reversing the order of all lines |
| 15:10:06 | <hopelessness[m]> | What would be a "better" way to do that? |
| 15:10:27 | <olle> | No, the issue is when the read depends on business logic somehow. |
| 15:10:42 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 15:10:44 | <hopelessness[m]> | hm |
| 15:10:47 | <olle> | So the read happens _sometimes_ but not always :) |
| 15:11:12 | <hopelessness[m]> | ah, |
| 15:11:13 | <hopelessness[m]> | * ah |
| 15:16:37 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 15:17:20 | × | isekaijin quits (~isekaijin@user/isekaijin) (Read error: Connection reset by peer) |
| 15:17:51 | → | fryguybob joins (~fryguybob@cpe-24-94-50-22.stny.res.rr.com) |
| 15:18:49 | × | saolof quits (~saolof@2001:2002:5ae4:c319:4108:8be0:bf78:a848) (Remote host closed the connection) |
| 15:20:00 | → | saolof joins (~saolof@2001:2002:5ae4:c319:4108:8be0:bf78:a848) |
| 15:21:56 | × | saolof quits (~saolof@2001:2002:5ae4:c319:4108:8be0:bf78:a848) (Remote host closed the connection) |
| 15:23:44 | × | aweinstock quits (~aweinstoc@cpe-74-76-189-75.nycap.res.rr.com) (Ping timeout: 248 seconds) |
| 15:31:58 | <ncf> | first thing that comes to mind is the free monad over Reader Text, or something |
| 15:32:48 | × | yoneda quits (~mike@193.206.102.122) (Quit: leaving) |
| 15:34:42 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:c066:a6a4:43b5:25e) (Ping timeout: 246 seconds) |
| 15:36:31 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:9da2:60aa:4250:a867) (Remote host closed the connection) |
| 15:36:50 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 15:37:09 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 15:37:51 | × | enoq quits (~enoq@2a05:1141:1f5:5600:b9c9:721a:599:bfe7) (Quit: enoq) |
| 15:37:57 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 15:41:06 | → | econo joins (uid147250@user/econo) |
| 15:41:38 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 246 seconds) |
| 15:42:03 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 15:44:10 | <olle> | I'd need to read up on that :d |
| 15:44:17 | <olle> | Free monad, freer monad, ... |
| 15:49:13 | → | hugo- joins (znc@verdigris.lysator.liu.se) |
| 15:54:03 | × | hugo- quits (znc@verdigris.lysator.liu.se) (Ping timeout: 255 seconds) |
| 16:04:43 | <ncf> | olle: super basic example: https://f.monade.li/sUQK1S.hs |
| 16:05:03 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 16:05:19 | <ncf> | this is a monad that allows you to read something at most once (not technically a free monad, but maybe a "free idempotent monad" if you like) |
| 16:05:54 | → | fen46 joins (~fen@250.79-105-213.static.virginmediabusiness.co.uk) |
| 16:06:11 | <fen46> | hi, re haskell as *not* a dependently typed language |
| 16:06:21 | <fen46> | given the type system is complete, whats the problem? |
| 16:06:56 | <fen46> | like, what we have at term level thats important is a completeness that the type system also has |
| 16:07:57 | <fen46> | where, by complete, i mean that since the top level function implementations can be recursive and so form a function graph... |
| 16:08:09 | <fen46> | graph like what a turing machine implements |
| 16:08:10 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 16:08:13 | <fen46> | so complete |
| 16:09:06 | <fen46> | the only thing i can think of is the problem of defunctionalisation |
| 16:09:16 | <fen46> | but thats just an inconvineice |
| 16:09:25 | × | MatthiasG quits (~MatthiasG@202.133.199.92) (Ping timeout: 260 seconds) |
| 16:09:39 | → | MatthiasG joins (~MatthiasG@119.56.103.127) |
| 16:09:52 | <fen46> | trying to think what a language extension that would satisfy the dependent programming problem |
| 16:10:05 | <fen46> | is it impossible to solve defunctionalisation using a language extension? |
| 16:11:03 | <fen46> | and can anyone think of anything else apart from that? |
| 16:11:22 | <fen46> | that would be required for the dependent typing problem to be considered solved |
| 16:11:24 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 16:14:47 | <ncf> | er, "free pointed endofunctor", not free idempotent monad. |
| 16:15:10 | <ncf> | basically a functor-level Maybe |
| 16:15:11 | → | hugo- joins (znc@verdigris.lysator.liu.se) |
| 16:18:09 | × | MatthiasG quits (~MatthiasG@119.56.103.127) (Read error: Connection reset by peer) |
| 16:18:13 | <ncf> | with this, you can define `ask` as `Read id`, and then write computations just as in Reader r |
| 16:18:31 | → | MatthiasG joins (~MatthiasG@202.133.199.92) |
| 16:18:55 | <c_wraith> | fen46: Haskell can emulate a lot of what dependently-typed languages do, but it's verbose, indirect, and has some awful gaps like an utter lack of floating-point values at the type level. |
| 16:21:17 | <fen46> | can we do things like traversaable at type level? |
| 16:21:52 | <fen46> | a had a problem with scanning a hetrogenous list with a convolutional opperator |
| 16:22:31 | <fen46> | i think its quite an undertaking... but possible? |
| 16:23:16 | <fen46> | i have it written at term level, maybe someone could help me write it at type level? |
| 16:23:27 | <c_wraith> | It's probably possible to represent the aspects you care about. But that doesn't mean it's pleasant. Or even worth doing. |
| 16:23:29 | <fen46> | help me by writing it at type level* |
| 16:23:43 | <fen46> | c_wraith: its just a requirement |
| 16:23:59 | <fen46> | so its more like "can you avoid having to do it" |
| 16:24:22 | <fen46> | so, yeah, not doing convolutional scannings on hetrogenous lists... |
| 16:24:43 | → | Guest|18 joins (~Guest|18@31.111.125.187) |
| 16:24:45 | <fen46> | im sure there are other uses |
| 16:24:50 | <fen46> | thats just the kind of test case |
| 16:25:57 | <olle> | ncf: right, and you combine the read with a lambda for a successful read? |
| 16:26:01 | <fen46> | eg if i wanted to zipWith (/), the lengthed lists in a hetrogenous list, and have to work out the resulting length |
| 16:26:18 | <fen46> | the adjacent antries of* |
| 16:26:21 | <fen46> | entries* |
| 16:26:58 | <fen46> | so then you have to do the same kind of scanning with adjacency convolution at type level with the length returning opperation |
| 16:27:08 | <fen46> | seems like a pretty general pattern |
| 16:27:18 | <c_wraith> | I strongly recommend not doing that |
| 16:27:25 | <c_wraith> | (In Haskell) |
| 16:27:29 | <fen46> | start hitting things like that pretty quickly when you start length annotating things |
| 16:27:43 | <ncf> | olle: not sure i understand the question |
| 16:27:51 | <fen46> | and yeah, basically have to if you want to do any fancy thing like passing around graphs with specified shapes |
| 16:27:57 | <c_wraith> | Even if you can make it work, it won't be worth using. |
| 16:28:01 | <fen46> | and then the levity recursion on that seems like it might kill you |
| 16:29:07 | <fen46> | c_wriath: i cant prove you wrong on that, but it seems pessimistic |
| 16:29:34 | <fen46> | but yeah, with the current state of defunctionalisation i would tend to agree out of sheer lacitude |
| 16:29:59 | <fen46> | and am constantly checking back in to see if theres any progress with the dependant typing language extension |
| 16:30:37 | <fen46> | lets just assume im thriftier than i actually am, and both need to and am able to wrangle these type level graph convolutions |
| 16:30:45 | <fen46> | and just am lacking the syntax |
| 16:32:06 | <fen46> | and yeah, i can think of a case, which is literally just the implementation of a graph, where you need to do basically an adjacency matrix exponentiation at type level |
| 16:32:35 | <fen46> | its not like its "unnecessary", its like the fundamentals of even being able to write the types of graphs |
| 16:33:32 | <fen46> | and, they are always hetrogenous, because they are supposed to be able to support representing programs |
| 16:34:05 | <fen46> | and there is some (truly ungodly) issue about the monad instance, of subgraphs, and the consequent hetroginaity |
| 16:35:05 | <fen46> | i mean, maybe its fine to have no type level representation of the way the program is structured |
| 16:35:20 | <fen46> | but it seems to kill everything at the levity recursion stage |
| 16:35:32 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Remote host closed the connection) |
| 16:36:08 | <fen46> | i guess i might be suspecting that its actually writing the traversable machinery at type level, such that would allow to handle these hetrogenous convolutions, that would "solve all our problems" |
| 16:36:31 | × | MajorBiscuit quits (~MajorBisc@31-23-159.netrun.cytanet.com.cy) (Ping timeout: 252 seconds) |
| 16:36:38 | <fen46> | eg. by doing something like allowing for program representation using the graph representation it would support |
| 16:36:48 | × | Square quits (~Square4@user/square) (Ping timeout: 248 seconds) |
| 16:36:58 | <fen46> | and then somehow because thats available be able to act as a compiler or whatever you would need at type level thats apparently missing |
| 16:37:11 | <fen46> | pretty vague i know, sorry |
| 16:37:54 | <fen46> | like, what i think im saying is "people on about dependent types just want map to work out the box at type level" |
| 16:38:09 | <fen46> | and that actually wouldnt be that far from the point |
| 16:38:48 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 16:38:57 | <fen46> | obvs using tail recursion to derive the traversable and listlike alternative, monad and comonadic zipper opperations |
| 16:39:33 | <fen46> | like, dont forget i think being able to do map somehow extends to giving you pointers by suspended traversal since your just pattern matching on the head basically |
| 16:39:47 | <fen46> | traversable things flattening to lists modulo some shape data |
| 16:40:07 | → | drdo joins (~drdo@bl7-76-103.dsl.telepac.pt) |
| 16:40:18 | × | Albina_Pavlovna quits (~Albina_Pa@2603-7000-76f0-76e0-491d-4022-58a1-d85a.res6.spectrum.com) (Quit: ZZZzzz…) |
| 16:40:24 | <fen46> | "if only type level lists worket properly" |
| 16:40:47 | <fen46> | and then its like, well why dont they!? |
| 16:41:22 | <fen46> | where most of the list opperations are from prelude |
| 16:41:38 | × | ubert quits (~Thunderbi@2a02:8109:abc0:6434:81f3:78d3:e012:2761) (Remote host closed the connection) |
| 16:41:57 | <fen46> | so when i ask, can someone help me put the traversable etc. (through to comonadic pointer) opperations at type level |
| 16:42:17 | <fen46> | i imagine it is basically towards the effort of satisfying whats missing in terms of dependet types |
| 16:42:31 | <fen46> | and wonder why people just say things like "ooh, i wouldnt bother with that, sounds difficult" |
| 16:43:01 | <fen46> | instead of being like "omg, thats the best idea iv ever heard, now all i want to do is levity proof convolutions" |
| 16:44:16 | × | drdo quits (~drdo@bl7-76-103.dsl.telepac.pt) (Remote host closed the connection) |
| 16:44:35 | → | drdo joins (~drdo@bl7-76-103.dsl.telepac.pt) |
| 16:44:55 | <fen46> | like, i literally did something like a PHD on this, the dissuasion seems almost impertinent, given the technology has already been presented |
| 16:46:39 | → | elevenkb joins (~elevenkb@105.225.53.253) |
| 16:47:41 | × | Guest|18 quits (~Guest|18@31.111.125.187) (Quit: Connection closed) |
| 16:48:25 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 16:51:47 | → | opticblast joins (~Thunderbi@172.58.85.126) |
| 16:55:00 | → | razetime joins (~Thunderbi@117.193.7.1) |
| 16:57:56 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 16:59:14 | × | MatthiasG quits (~MatthiasG@202.133.199.92) (Read error: Connection reset by peer) |
| 16:59:49 | → | MatthiasG joins (~MatthiasG@202.133.199.92) |
| 17:00:09 | → | notzmv joins (~zmv@user/notzmv) |
| 17:01:07 | × | opticblast quits (~Thunderbi@172.58.85.126) (Ping timeout: 265 seconds) |
| 17:02:14 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Remote host closed the connection) |
| 17:06:56 | <fen46> | the bit i cant do is understanding how it would work |
| 17:07:07 | <fen46> | like, if it were to be a language extension, or a module or something |
| 17:07:53 | <fen46> | to envisage what "does what it says on the tin" actually means for haskell and as close as it might become on its path *towards* dependent types |
| 17:08:15 | <fen46> | i think what i say could almost sound convincing that what you actually want is type level seti |
| 17:08:42 | <fen46> | is kind of what im trying to say, rather than "i really actually waant to have to write the program graphs" |
| 17:09:17 | <fen46> | like, we have recursive datatypes, so the main mechanism is present |
| 17:09:25 | <fen46> | which is why i basically think its complete i guess |
| 17:09:43 | <fen46> | so then the question is whats actually missing? |
| 17:09:49 | × | mbuf quits (~Shakthi@49.207.178.186) (Quit: Leaving) |
| 17:10:09 | <fen46> | and i can get pretty far with seti, and its as far as the prelude does, in offering the ground level haskell environment |
| 17:10:42 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:10:54 | <fen46> | i guess maybe i could use some kind of deriving instances in data families or what i cant even understand... |
| 17:11:25 | <fen46> | some kind of type level default instances or something is missing? i cant figure it out |
| 17:11:58 | <fen46> | basically wanting something like foldMapDefault |
| 17:12:10 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 17:12:11 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 264 seconds) |
| 17:12:24 | <fen46> | big complicated hierarchy of defaults from geti+seti instances |
| 17:12:41 | <fen46> | at Type Level... |
| 17:12:55 | <fen46> | and if thats literally all thats missing... |
| 17:13:04 | <fen46> | to give the absent type level prelude |
| 17:13:25 | <fen46> | and that with it, then dependent types isnt done, but haskell is more tooled up for type level programing |
| 17:13:37 | <fen46> | much more to the point where its usable |
| 17:13:48 | <fen46> | since traversable basically covers so much |
| 17:14:29 | <fen46> | so maybe my question is, would type level seti be a satesfactory standin for full dependent types |
| 17:14:38 | <fen46> | and if so, can i get some hands on!? |
| 17:14:58 | → | jtza8 joins (~user@165.255.63.78) |
| 17:16:06 | <fen46> | like, if you think about how mental type level lenses in the style of ed kmett would be, and that the canonical version presented by geti+seti seems like feasable implementation in comparison and would at least allow for lists to have the usual higher order functions over them |
| 17:16:56 | <fen46> | given thats basically "where its at" for haskell at term level, seems like this would be natural way to go towards type level land |
| 17:17:24 | <fen46> | since dependant languages exist and haskell will not likely join them |
| 17:17:41 | <fen46> | that this would be basically the best place for haskell to get developed |
| 17:18:23 | <fen46> | the actual instances are really simple, geti and seti that is, to mimic at type level alongside term level implementations |
| 17:18:24 | <monochrom> | I think at some point you need to recall that if no one is interested in your discussion then you should stop. |
| 17:18:44 | <fen46> | i wasnt even sure anyone was reading it |
| 17:18:53 | <monochrom> | Or at least switch to Facebook or Twitter. |
| 17:19:09 | <fen46> | so i shouldnt try and message you? |
| 17:19:46 | <fen46> | someone could weigh in with a comment on the subject material i guess |
| 17:19:53 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.8) |
| 17:19:57 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 17:20:06 | <int-e> | tl;dr |
| 17:20:46 | <darkling> | I think monochrom's point was that if nobody has by now, you're probably not going to get one... |
| 17:20:48 | <fen46> | tl;dr: i think i can convince you to write type level seti for me and add it to the language because its the best thing to do |
| 17:21:00 | <monochrom> | I personally start my discussion with one or maybe at most five lines. Then I suspend until someone shows interest. Otherwise let it go. |
| 17:21:39 | <fen46> | then im confused about the, it being the best thing ever and people, as you seem to imply not being interested |
| 17:21:52 | <monochrom> | But if that's against your philosophy, you can always go to Twitter, and no one will complain there. |
| 17:21:59 | <fen46> | it does seem accurate to be fair |
| 17:22:18 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 17:22:34 | <fen46> | i guess im *not* convinced people arent interested, you just set the tone |
| 17:23:24 | <monochrom> | No, I spoke what other people were too polite to speak. |
| 17:23:32 | <fen46> | oh right, your just complaining about the messages. yeah, im not too stoked on doing stuff either |
| 17:23:33 | × | vglfr quits (~vglfr@88.155.17.187) (Ping timeout: 256 seconds) |
| 17:23:39 | <fen46> | oh, ok the flood. my bad. |
| 17:23:43 | <fen46> | im dumb like that |
| 17:23:49 | <fen46> | i didnt realise people were online. |
| 17:24:23 | <fen46> | sorry ill shut up. but any input would still be appreciated if thats where a discussion could lead |
| 17:24:31 | <monochrom> | My said technique of "at most 5 lines then suspend" can be learned. |
| 17:24:41 | → | vglfr joins (~vglfr@88.155.17.187) |
| 17:24:51 | <fen46> | im wondering if my subject material can be... |
| 17:24:52 | <monochrom> | Or else switching to a suitable social media platform can be easily done. |
| 17:25:07 | <fen46> | i was yet to be aware of these fantastic techniques |
| 17:25:24 | <fen46> | im still keen on input |
| 17:25:55 | × | tlaxkit quits (~hexchat@170.253.32.109) (Quit: Saliendo...) |
| 17:25:58 | <fen46> | so my one question. if seti could help haskell at type level, would you be interested? |
| 17:26:18 | <fen46> | since i guess everything rests on that |
| 17:26:45 | × | razetime quits (~Thunderbi@117.193.7.1) (Remote host closed the connection) |
| 17:34:15 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 17:34:17 | → | Albina_Pavlovna joins (~Albina_Pa@2603-7000-76f0-76e0-491d-4022-58a1-d85a.res6.spectrum.com) |
| 17:35:01 | → | Guest87 joins (~Guest87@047-224-137-232.res.spectrum.com) |
| 17:40:37 | × | MatthiasG quits (~MatthiasG@202.133.199.92) (Ping timeout: 268 seconds) |
| 17:40:45 | → | MatthiasG joins (~MatthiasG@202.133.199.92) |
| 17:41:03 | × | MatthiasG quits (~MatthiasG@202.133.199.92) (Read error: Connection reset by peer) |
| 17:42:51 | <Guest87> | @pl \x -> f x + g x |
| 17:42:51 | <lambdabot> | liftM2 (+) f g |
| 17:44:12 | <Guest87> | @pl \x -> x +x |
| 17:44:12 | <lambdabot> | join (+) |
| 17:45:06 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 17:47:00 | × | Guest87 quits (~Guest87@047-224-137-232.res.spectrum.com) (Quit: Client closed) |
| 17:53:52 | × | [exa] quits (~exa@srv3n.blesmrt.net) (Changing host) |
| 17:53:52 | → | [exa] joins (~exa@user/exa/x-3587197) |
| 17:55:32 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Remote host closed the connection) |
| 17:55:33 | → | mechap joins (~mechap@user/mechap) |
| 18:00:14 | × | jtza8 quits (~user@165.255.63.78) (Remote host closed the connection) |
| 18:00:18 | <ncf> | to whom it may interest: the construction i was trying to describe earlier is analogous to the "free monoid on a semigroup", i.e. the left adjoint to the forgetful functor from monoids to semigroups |
| 18:01:00 | <ncf> | so, it's a "functorification" of the instance Semigroup a => Monoid (Maybe a) (https://hackage.haskell.org/package/base-4.18.0.0/docs/src/GHC.Base.html#line-489) |
| 18:09:16 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 18:09:20 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 18:12:18 | → | coot_ joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 18:14:56 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Ping timeout: 246 seconds) |
| 18:14:56 | coot_ | is now known as coot |
| 18:15:28 | → | kenran joins (~user@user/kenran) |
| 18:16:41 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 255 seconds) |
| 18:17:42 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 18:20:18 | <fen46> | (geti,set) :: (Geti f i => f a -> ((a,i),f a),Seti f i => ((a,i),f a) -> f a) |
| 18:31:55 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 18:34:53 | × | fen46 quits (~fen@250.79-105-213.static.virginmediabusiness.co.uk) (Ping timeout: 265 seconds) |
| 18:41:53 | × | jero98772 quits (~jero98772@2800:484:1d84:9000::5) (Ping timeout: 246 seconds) |
| 18:43:01 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 276 seconds) |
| 18:43:57 | → | pwug joins (~pwug@user/pwug) |
| 18:52:04 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 18:53:36 | → | jero98772 joins (~jero98772@2800:484:1d84:9000::5) |
| 19:13:22 | → | BOO joins (~BOO@220-129-34-70.dynamic-ip.hinet.net) |
| 19:25:22 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 19:28:44 | → | MajorBiscuit joins (~MajorBisc@31-23-159.netrun.cytanet.com.cy) |
| 19:29:54 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
| 19:33:42 | → | ix joins (~ix@2a02:8012:281f:0:d65d:64ff:fe52:5efe) |
| 19:34:55 | × | eggplantade quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 19:49:57 | → | vglfr_ joins (~vglfr@88.155.17.187) |
| 19:50:56 | × | haritz quits (~hrtz@user/haritz) (Ping timeout: 248 seconds) |
| 19:51:16 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Remote host closed the connection) |
| 19:52:15 | × | jero98772 quits (~jero98772@2800:484:1d84:9000::5) (Ping timeout: 265 seconds) |
| 19:53:14 | × | BOO quits (~BOO@220-129-34-70.dynamic-ip.hinet.net) (Quit: Client closed) |
| 19:53:41 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 19:53:50 | → | jerg joins (~jerg@2001:a61:6134:5201:5df3:da85:9419:73e) |
| 19:55:03 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 19:55:26 | → | ft joins (~ft@p4fc2a88b.dip0.t-ipconnect.de) |
| 19:57:01 | → | heraldo joins (~heraldo@user/heraldo) |
| 19:57:23 | × | vglfr_ quits (~vglfr@88.155.17.187) (Quit: leaving) |
| 19:58:11 | → | Square joins (~Square@user/square) |
| 20:01:54 | → | auiee joins (~vglfr@88.155.17.187) |
| 20:03:42 | × | auiee quits (~vglfr@88.155.17.187) (Client Quit) |
| 20:03:48 | → | Sciencentistguy1 joins (~sciencent@hacksoc/ordinary-member) |
| 20:05:30 | → | jero98772 joins (~jero98772@2800:484:1d84:9000::5) |
| 20:05:52 | × | Sciencentistguy quits (~sciencent@hacksoc/ordinary-member) (Ping timeout: 248 seconds) |
| 20:05:52 | Sciencentistguy1 | is now known as Sciencentistguy |
| 20:06:59 | → | auiee joins (~vglfr@88.155.17.187) |
| 20:08:49 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 20:08:52 | × | auiee quits (~vglfr@88.155.17.187) (Client Quit) |
| 20:10:59 | → | Square2 joins (~Square4@user/square) |
| 20:12:56 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 246 seconds) |
| 20:13:14 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 255 seconds) |
| 20:13:24 | × | troydm quits (~troydm@user/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 20:13:43 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 20:14:09 | × | Square quits (~Square@user/square) (Ping timeout: 255 seconds) |
| 20:14:14 | → | troydm joins (~troydm@user/troydm) |
| 20:14:33 | Square2 | is now known as Square |
| 20:23:33 | × | elevenkb quits (~elevenkb@105.225.53.253) (Quit: Client closed) |
| 20:25:22 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 20:27:47 | → | mei joins (~mei@user/mei) |
| 20:33:21 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:33:49 | → | pavonia joins (~user@user/siracusa) |
| 20:35:14 | × | michalz quits (~michalz@185.246.204.101) (Remote host closed the connection) |
| 20:35:24 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) |
| 20:39:18 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 20:39:59 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:ad1e:c088:4c6f:8ed8) (Ping timeout: 250 seconds) |
| 20:43:02 | × | MajorBiscuit quits (~MajorBisc@31-23-159.netrun.cytanet.com.cy) (Quit: WeeChat 3.6) |
| 20:49:28 | → | Batzy_ joins (~quassel@user/batzy) |
| 20:52:16 | × | Batzy quits (~quassel@user/batzy) (Ping timeout: 248 seconds) |
| 20:53:33 | → | haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
| 20:53:33 | × | haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
| 20:53:33 | → | haritz joins (~hrtz@user/haritz) |
| 20:57:51 | → | Batzy joins (~quassel@user/batzy) |
| 21:01:05 | × | Batzy_ quits (~quassel@user/batzy) (Ping timeout: 260 seconds) |
| 21:02:01 | × | jero98772 quits (~jero98772@2800:484:1d84:9000::5) (Ping timeout: 240 seconds) |
| 21:07:11 | <olle> | In terms of design by contract, would you say an IO write is more complex than an IO read? |
| 21:09:02 | × | sammelweis quits (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
| 21:10:49 | → | sammelweis joins (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
| 21:13:21 | <Hecate> | I've never done DbC |
| 21:13:33 | → | jero98772 joins (~jero98772@2800:484:1d84:9000::5) |
| 21:13:54 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 265 seconds) |
| 21:25:04 | × | Albina_Pavlovna quits (~Albina_Pa@2603-7000-76f0-76e0-491d-4022-58a1-d85a.res6.spectrum.com) (Quit: ZZZzzz…) |
| 21:25:50 | <olle> | Fair enough |
| 21:27:48 | <sm> | olle: what's an example of applying design by contract here ? |
| 21:28:31 | <sm> | is it another way of saying, is the specification of one more complex than the other ? |
| 21:29:47 | <zq> | just read the backpack paper and have questions, any recommendations on a good place to ask? |
| 21:32:25 | <olle> | sm: I'm thinking of pre- and post-conditions, and how their complexity are affected by a function reading or writing to stuff |
| 21:32:33 | <monochrom> | I may still recall a little bit of backpack stuff. |
| 21:32:54 | <sm> | aha |
| 21:34:21 | <olle> | For example, if you have a company that _only_ reads from file, the order of the functions probably won't matter (much?). But if one function also writes to file, order might become important. |
| 21:34:43 | <olle> | company/function/s |
| 21:34:44 | <olle> | >< |
| 21:34:54 | <hpc> | alternatively, if you only write to a file, do you even have to do anything at all? |
| 21:34:59 | <monochrom> | IMO pre/post conditions are utterly useless for I/O R/W unless you make the totally ancient (Apple-DOS era) assumption that you are the only one accessing the file system and so the file system is just one huge but unshared mutable variable. |
| 21:36:03 | <monochrom> | In this The Year 2023 of Our Lord, the file system is emphatically shared and multi-user. You are better off with at the very least automata or any concurrency theory. |
| 21:37:13 | <monochrom> | (If you haven't heard of Apple DOS, then try CP/M.) |
| 21:38:09 | <olle> | I'm assuming atomic access to file system here |
| 21:38:53 | <monochrom> | I was not even bringing up non-atomicity in the real world. |
| 21:39:12 | <olle> | Well |
| 21:39:25 | <olle> | In any case, my question is how to compare the complexity of one contract to another :) |
| 21:39:40 | <hpc> | once you get small enough, every operation is atomic |
| 21:39:45 | <monochrom> | I was, merely, pointing out that even with atomicity, you even cannot assume "read that location; 5 seconds later, read that location again" is idempotent. |
| 21:40:19 | <hpc> | just keep subdividing the non-atomic operations |
| 21:41:02 | <hpc> | olle: this class of problem (especially on the filesystem) is called time-of-call/time-of-use |
| 21:41:31 | <monochrom> | I have a feeling that, as usual, comparing two contracts is undecidable. |
| 21:41:32 | <hpc> | between stating a file and opening it, something else deleted it |
| 21:41:39 | <olle> | hpc: still unrelated ^^ |
| 21:41:56 | <monochrom> | Right? Even "merely" comparing two CFGs is already undecidable. |
| 21:42:10 | → | koolazer joins (~koo@user/koolazer) |
| 21:43:26 | <olle> | To take an example, imagine you have function F that reads 3 times and writes 2 times, and function G that reads 2 times and writes 3 times. Does it make sense to compare their contracts from such a perspective? |
| 21:43:39 | <hpc> | olle: i guess the answer to the question as stated then is, neither operation has a consistent "complexity" value by measures that make sense |
| 21:43:53 | <hpc> | imagine you have a function H that reads 100 times, and a funcgion I that writes 100 times |
| 21:44:03 | <olle> | Maybe not |
| 21:44:04 | <hpc> | in the case of H, it's equivalent to reading once |
| 21:44:09 | <hpc> | in I, it's equivalent to doing nothing at all |
| 21:44:14 | <hpc> | because you never read |
| 21:44:41 | <monochrom> | But that's for very private local vars that no one else can observe. |
| 21:44:44 | <hpc> | (or if I is part of a larger system, I is equivalent to writing once) |
| 21:44:51 | <olle> | I mean, some other function can read. :) |
| 21:45:21 | <olle> | Read/write to/from file, that is |
| 21:45:38 | <hpc> | you'd need to come up with some way of analyzing F/G such that you can say F has 15 complexity points and G has 12 |
| 21:45:59 | <hpc> | maybe that means how many ways you can reorder the read/write calls and get funny results, or something like that |
| 21:46:28 | <monochrom> | Although, entropy and information theory says that writing generates more waste heat than reading. |
| 21:46:29 | <olle> | Yeah, the crucial point is how the reads/writes depend on each other. |
| 21:47:35 | <monochrom> | Or maybe not. If you read to somewhere, that also means writing to that somewhere. meh. |
| 21:48:17 | <olle> | hpc: Sounds like some type of graph analysis |
| 21:48:31 | <olle> | What depends on what in which order |
| 21:48:50 | <olle> | Where independent reads/writes could be considered less complex [for the human brain] |
| 21:49:31 | <hpc> | actually, that reordering idea doesn't quite make sense, you'd basically be measuring concurrency issues instead |
| 21:49:32 | monochrom | on next year's April 1st will go to the linux kernel and swap read() and write(), rationale being that the original "read"() writes to memory, and the original "write"() reads from memory. >:D |
| 21:50:42 | <olle> | hpc: No, I think it has some merit. Imagine copy a file and delete the original. Not good if you delete the original first. ^^' |
| 21:53:51 | <hpc> | sure, but that doesn't say which operation to attribute that misbehavior to |
| 21:54:43 | <olle> | The post-condition breaks if you re-order the reads/writes? |
| 21:55:02 | <monochrom> | Um, you always attribute misbehaviours to the programmer! |
| 21:55:07 | <hpc> | yeah, but which was it, read or write? |
| 21:55:22 | <hpc> | you have to say one of them contributed more to the problem than the other, otherwise you can't get that "X is more complex than Y" metric |
| 21:55:48 | <olle> | hpc: Does it matter? It should be compared to another function that also has one read and one write where a re-order does _not_ cause a bug. |
| 21:55:57 | <olle> | Wait |
| 21:56:14 | <mauke> | monochrom: https://www.ioccc.org/1984/anonymous/anonymous.c |
| 21:56:24 | <olle> | I'm confusing semantics with syntax or something |
| 21:57:17 | <olle> | Wait, is the conclusion that cp is less complex than mv? |
| 21:57:53 | <monochrom> | Wait a second, '-'-'-' is now a file descriptor... haha |
| 21:58:08 | <monochrom> | OK I am now too scared to run that program. |
| 21:58:11 | <olle> | Well cp is read-write and mv is read-write-write (second write is the delete) |
| 21:59:02 | <geekosaur> | unless it's on the same filesystem in whoich case it's write-write (link, unlink) |
| 21:59:15 | <olle> | Obviously you couldn't implement cp as write-read either :d |
| 22:00:01 | <hpc> | geekosaur: it's even better than that, according to strace it's renameat2() |
| 22:00:15 | <geekosaur> | true, I ignored that part |
| 22:00:40 | <monochrom> | There is no information you can gain from "read-write is more complex than read-write-write". |
| 22:00:47 | <hpc> | jeez, this is actually a lot |
| 22:00:57 | <monochrom> | err, s/more/less/ |
| 22:01:14 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 255 seconds) |
| 22:01:15 | <hpc> | it has to know what the filesystem states are, to know if it can do renameat2 in the first place |
| 22:01:30 | <hpc> | which... is reading from a file that isn't even a file |
| 22:01:41 | <hpc> | because it's /proc :D |
| 22:02:14 | <olle> | Need to sleep, but thanks for feedback, the graph/reorder idea was interesting |
| 22:02:15 | <olle> | \o |
| 22:02:31 | <mauke> | '-'-'-' is a perfectly cromulent file descriptor |
| 22:03:25 | <monochrom> | OOOHHHH haha I forgot that the middle - just means subtraction. |
| 22:04:04 | <monochrom> | You have just certified that I can't even parse C grammar. :) |
| 22:05:16 | <monochrom> | My excuse is that I'm studying linear algebra right now, C is on swap. |
| 22:07:07 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:07:29 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 22:07:45 | <hpc> | ppsh, "linear" means it's easy |
| 22:08:24 | <monochrom> | As with musical instruments, someone will find ways to make it difficult. |
| 22:08:48 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 22:09:44 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 22:12:47 | × | gurkenglas quits (~gurkengla@dynamic-046-114-181-068.46.114.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 22:12:52 | → | zmt01 joins (~zmt00@user/zmt00) |
| 22:13:23 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 22:13:55 | → | gurkenglas joins (~gurkengla@dynamic-046-114-183-049.46.114.pool.telefonica.de) |
| 22:14:31 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 240 seconds) |
| 22:14:44 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 246 seconds) |
| 22:32:20 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 22:34:33 | × | urdh quits (~urdh@user/urdh) (Ping timeout: 255 seconds) |
| 22:35:48 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 22:40:23 | → | urdh joins (~urdh@user/urdh) |
| 22:46:57 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:49:07 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 250 seconds) |
| 22:49:55 | <juri_> | monochrom: has anyone exposed you to projective geometric algebra? |
| 22:50:06 | <juri_> | linear algebra is dead. ;) |
| 22:52:32 | <monochrom> | I think yes. |
| 22:53:00 | <monochrom> | Is that something about bivectors, Clifford algebra, etc.? |
| 22:53:45 | <monochrom> | linear algebra may be dead but still highly relevant and useful, like Fortran. :) |
| 22:57:25 | <juri_> | ok. your pain. ;) |
| 22:57:39 | <juri_> | i have written a haskell library for this, covering many of the 2D cases. |
| 22:58:41 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 22:58:49 | <monochrom> | Oh, I'm studing linear algebra because of the prospect of using the following as Num instance homework next time I teach Haskell in a course. |
| 22:59:25 | <juri_> | Oh! then stay far away from what i've done. its pure madness! :) |
| 22:59:42 | <monochrom> | The nxn matrices form a ring, so most of the Num methods are accounted for. Except what to do about signum and abs. |
| 23:00:48 | <juri_> | https://github.com/Haskell-Things/HSlice/blob/master/Graphics/Slicer/Math/PGAPrimitives.hs <-- in case you want to twist your brain. ;) |
| 23:00:49 | <monochrom> | I have just recalled learning that every square matrix is factorable into (some unitary matrix) * (positive square root of M* times M). |
| 23:01:37 | <monochrom> | That sounds like a great candidate for M = signum M * abs M. I'm investigating how to compute them. |
| 23:02:09 | → | gry joins (st@botters/gry) |
| 23:02:14 | <juri_> | you lost me completely. my last linear algebra was in high school, and it probably shows in my code. |
| 23:02:15 | <monochrom> | "ORMOLU_DISABLE" haha |
| 23:02:44 | <juri_> | me and ormolu don't agree on much. ;) |
| 23:02:53 | → | dextaa1 joins (~DV@user/dextaa) |
| 23:03:16 | <monochrom> | Oh I have a feeling that learning C : learning Haskell :: learning linear algebra : learning geometric algebra |
| 23:03:34 | <monochrom> | Namely being a clean slate may make your life easier! |
| 23:03:42 | <hpc> | this is why i learned linear geometry |
| 23:03:47 | <monochrom> | haha |
| 23:04:01 | <juri_> | this is why i spent 25 years writing C. |
| 23:04:07 | <juri_> | *hides* |
| 23:04:11 | × | dextaa quits (~DV@user/dextaa) (Ping timeout: 248 seconds) |
| 23:04:11 | dextaa1 | is now known as dextaa |
| 23:07:09 | → | maxwarrior joins (~maxwarrio@2803:9800:98c1:795a:fc63:5ff3:390c:c0a0) |
| 23:07:33 | <maxwarrior> | Hi everybody! |
| 23:08:18 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 255 seconds) |
| 23:10:32 | × | zeenk quits (~zeenk@2a02:2f04:a307:2300::fba) (Quit: Konversation terminated!) |
| 23:10:54 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 23:11:02 | × | maxwarrior quits (~maxwarrio@2803:9800:98c1:795a:fc63:5ff3:390c:c0a0) (Remote host closed the connection) |
| 23:16:12 | × | pwug quits (~pwug@user/pwug) (Quit: Leaving) |
| 23:22:28 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 23:24:06 | × | gurkenglas quits (~gurkengla@dynamic-046-114-183-049.46.114.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 23:25:07 | × | jerg quits (~jerg@2001:a61:6134:5201:5df3:da85:9419:73e) (Quit: Leaving) |
| 23:29:50 | × | codaraxis quits (~codaraxis@user/codaraxis) (Ping timeout: 260 seconds) |
| 23:33:01 | × | acidjnk quits (~acidjnk@p200300d6e715c407d4f5be9b40c24016.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 23:34:37 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:36:52 | → | harveypwca joins (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
| 23:41:13 | × | ell quits (~ellie@user/ellie) (Quit: Ping timeout (120 seconds)) |
| 23:41:32 | → | ell joins (~ellie@user/ellie) |
| 23:42:03 | × | NiceBird quits (~NiceBird@185.133.111.196) (Ping timeout: 255 seconds) |
| 23:45:41 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 268 seconds) |
All times are in UTC on 2023-04-11.