Logs on 2024-04-24 (liberachat/#haskell)
| 00:07:25 | × | tv quits (~tv@user/tv) (Ping timeout: 245 seconds) |
| 00:07:43 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 246 seconds) |
| 00:07:48 | → | tv joins (~tv@user/tv) |
| 00:18:37 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
| 00:21:29 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 00:24:15 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 272 seconds) |
| 00:34:55 | × | zwrv quits (~yin@user/zero) (Ping timeout: 245 seconds) |
| 00:36:57 | → | zwrv joins (~yin@user/zero) |
| 00:49:42 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:51:20 | <cheater> | i would like to make it impossible to export a type from my module and i would like to add some checking that will error out if that happens. how can i do this? |
| 00:51:49 | <cheater> | it's a newtype |
| 00:52:04 | <cheater> | i want it usable outside the module using only values i exported which are smart constructors |
| 00:52:33 | <c_wraith> | You need some form of testing for "does not compile" |
| 00:53:04 | <c_wraith> | I know of a package that tests for type errors using -fdefer-type-errors, but there's no equivalent for name errors. Which is what you're really looking for. |
| 00:53:53 | <cheater> | it's mostly to make sure my coworkers don't do something stupid |
| 00:54:08 | <cheater> | which, you know, given that this is an unusual way to use modules, is warranted |
| 00:54:27 | <c_wraith> | not exporting constructors is a pretty common way to use modules... |
| 00:54:46 | <cheater> | yes, but forbidding the exporting is a less common thing |
| 00:55:01 | <cheater> | there isn't really a specific way to say in haskell "these things shall not be exported" |
| 00:55:16 | <cheater> | there's only the negative statement of "these things have not been exported" |
| 00:55:22 | <cheater> | but it's not like an active "do not export these" |
| 00:56:16 | <c_wraith> | Oh! You can use template haskell. |
| 00:56:26 | <cheater> | in what way |
| 00:56:57 | <c_wraith> | > runQ [| Bin |] --> UnboundVarE Bin |
| 00:56:58 | <lambdabot> | <hint>:1:7: error: parse error on input ‘|’ |
| 00:57:06 | <c_wraith> | whoops, didn't mean to prefix that with > |
| 00:57:07 | <c_wraith> | anyway |
| 00:57:24 | <cheater> | i don't get it |
| 00:57:29 | <cheater> | can you explain what it does? |
| 00:57:42 | <c_wraith> | If you runQ a quote containing the name of the constructor, you will get UnboundVarE if the constructor isn't in scope |
| 00:58:16 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 00:58:17 | <cheater> | ok but how does that help me? i would have to do this in every *other* module |
| 00:58:31 | → | madeleine-sydney joins (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 00:58:52 | <c_wraith> | Does every other module import a different version of the module containing the hidden constructors? |
| 00:59:58 | <c_wraith> | Someone would have to work really hard to break such a test - moving the constructors to a different module, or renaming them |
| 01:00:12 | <c_wraith> | At that point, they should get the point that they're doing something unapproved |
| 01:01:29 | <cheater> | i don't understand. why are you talking about different versions of module exports? |
| 01:01:42 | <c_wraith> | why are you talking about testing in every other module? |
| 01:01:48 | <c_wraith> | Modules have exactly one export list |
| 01:02:00 | <c_wraith> | You test the export list, not how it's imported in other modules |
| 01:02:12 | <cheater> | well if i have module Foo where would i put that test? |
| 01:02:18 | <c_wraith> | In a test |
| 01:02:21 | <cheater> | if i put it in module Foo then obviously the constructors will be there |
| 01:02:26 | <cheater> | so what, like another module? |
| 01:02:27 | <c_wraith> | No, of course not |
| 01:02:34 | <c_wraith> | Some other module, like all testts |
| 01:02:53 | <cheater> | hmm... |
| 01:03:07 | <cheater> | makes sense |
| 01:03:24 | <geekosaur> | if you try to put your test in the module where you're trying to prevent exports, which might be possible with some evil TH, what would stop someone from deleting your test? |
| 01:03:31 | <geekosaur> | it belongs in the test suite |
| 01:03:35 | × | zwrv quits (~yin@user/zero) (Ping timeout: 264 seconds) |
| 01:03:53 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (Ping timeout: 268 seconds) |
| 01:05:07 | × | mima quits (~mmh@aftr-62-216-211-1.dynamic.mnet-online.de) (Ping timeout: 268 seconds) |
| 01:05:32 | <monochrom> | It is a test case. I have such test cases in a C course. I teach students what not to put in a *.h file. So my test case is a C file that #include's it and tries to use what should be forbidden. If my file compiles, the student gets 0 marks. |
| 01:05:56 | <monochrom> | Very simple to write a shell script "if ! gcc foo.c ; then ..." for that. |
| 01:06:39 | <c_wraith> | Sadly, you can't use reify with runQ. I... don't know why not. |
| 01:09:11 | → | pointlessslippe1 joins (~pointless@212.82.82.3) |
| 01:12:23 | <cheater> | geekosaur: it's not about stopping someone from deleting the test |
| 01:12:31 | <cheater> | geekosaur: you misunderstood the thing i said earlier |
| 01:12:40 | <cheater> | [02:53:31] <cheater> there isn't really a specific way to say in haskell "these things shall not be exported" |
| 01:12:40 | <cheater> | [02:53:46] <cheater> there's only the negative statement of "these things have not been exported" |
| 01:13:26 | <cheater> | if someone tries to export the constructors, and then finds out the thing doesn't build, and the error comes from a line with the comment "do not export these, blah blah blah see ticket FU-69420" then they'll know not to export it |
| 01:13:34 | <cheater> | it's not about *preventing* someone from exporting the thing |
| 01:13:49 | <cheater> | it's to prevent them from (exporting it because they didn't know better) |
| 01:17:15 | <probie> | So the goal is to preventing some well-meaning agent of chaos from breaking everything? Very low effort, slightly messy, high success chance: Add the constructor the export list yourself, and then comment it out and stick a comment above it saying why it can't be exported |
| 01:17:24 | <probie> | That way if they go to export it, they'll see it |
| 01:20:32 | <jackdk> | can you put constraints on pattern synonyms? If so, you could stick a `TypeError (...) =>` on it and export that in place of the actual ctor |
| 01:20:42 | <geekosaur> | yeh, you were making it sound like active maliciousness which requires something more clever |
| 01:26:19 | × | xff0x quits (~xff0x@ai082039.d.east.v6connect.net) (Ping timeout: 272 seconds) |
| 01:27:43 | <cheater> | probie: that's practical... not the best solution but it might be the simplest useful solution |
| 01:28:00 | <cheater> | jackdk: i want those types to actually be used. |
| 01:28:34 | <cheater> | just via my own functions |
| 01:28:38 | <cheater> | and not via the types being instantiated. |
| 01:33:24 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 01:35:51 | × | random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 260 seconds) |
| 01:36:45 | × | otto_s quits (~user@p5b044a05.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 01:37:56 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 01:38:15 | → | otto_s joins (~user@p5b0445f5.dip0.t-ipconnect.de) |
| 01:38:15 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 245 seconds) |
| 01:57:43 | <Axman6> | So do you want users to be able to pattern match on the type but not use the constructor for creating the type? |
| 01:58:06 | → | trqt joins (~trqt@user/trqt) |
| 01:58:06 | <Axman6> | that feels doable with pattern synonyms |
| 02:02:20 | × | cipherrot quits (~znc-user@user/petrichor) (Read error: Connection reset by peer) |
| 02:02:40 | → | petrichor joins (~znc-user@user/petrichor) |
| 02:04:57 | × | hueso quits (~root@user/hueso) (Quit: hueso) |
| 02:08:53 | → | hueso joins (~root@user/hueso) |
| 02:09:55 | × | nschoe quits (~nschoe@2a01:e0a:8e:a190:f3a1:c501:e8bd:2571) (Ping timeout: 245 seconds) |
| 02:09:59 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:10:10 | → | tt123109 joins (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) |
| 02:10:16 | → | tabemann_ joins (~tabemann@2600:1700:7990:24e0:42f1:a891:a658:f99d) |
| 02:10:17 | → | Luj3 joins (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) |
| 02:10:20 | × | FragByte quits (~christian@user/fragbyte) (Ping timeout: 245 seconds) |
| 02:10:23 | × | Benzi-Junior quits (~BenziJuni@232-148-209-31.dynamic.hringdu.is) (Quit: ZNC 1.8.2 - https://znc.in) |
| 02:10:31 | → | ubert1 joins (~Thunderbi@2a02:8109:ab8a:5a00:a472:8995:2c6:603d) |
| 02:10:38 | × | Natch quits (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Read error: Connection reset by peer) |
| 02:10:39 | → | Benzi-Junior joins (~BenziJuni@232-148-209-31.dynamic.hringdu.is) |
| 02:10:41 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:a472:8995:2c6:603d) (Remote host closed the connection) |
| 02:10:41 | ubert1 | is now known as ubert |
| 02:10:44 | × | tabemann quits (~tabemann@2600:1700:7990:24e0:2a56:ddeb:a57a:6071) (Read error: Connection reset by peer) |
| 02:10:51 | → | pavonia_ joins (~user@user/siracusa) |
| 02:10:58 | × | Luj quits (~Luj@2a01:e0a:5f9:9681:1b36:b307:9c84:5d03) (Read error: Connection reset by peer) |
| 02:10:58 | Luj3 | is now known as Luj |
| 02:11:00 | → | tzh_ joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 02:11:07 | × | xal quits (~xal@mx1.xal.systems) (Quit: No Ping reply in 180 seconds.) |
| 02:11:07 | → | nschoe joins (~nschoe@2a01:e0a:8e:a190:f3a1:c501:e8bd:2571) |
| 02:11:12 | → | FragByte joins (~christian@user/fragbyte) |
| 02:11:19 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (Quit: ZNC - http://znc.in) |
| 02:11:25 | → | tcard_ joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 02:11:35 | × | tt12310 quits (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 245 seconds) |
| 02:11:35 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Ping timeout: 245 seconds) |
| 02:11:35 | tt123109 | is now known as tt12310 |
| 02:11:46 | × | driib quits (~driib@vmi931078.contaboserver.net) (Quit: Ping timeout (120 seconds)) |
| 02:11:50 | × | JamesMowery quits (~JamesMowe@ip98-171-80-211.ph.ph.cox.net) (Quit: Ping timeout (120 seconds)) |
| 02:11:59 | → | pointlessslippe1 joins (~pointless@212.82.82.3) |
| 02:12:09 | → | JamesMowery joins (~JamesMowe@ip98-171-80-211.ph.ph.cox.net) |
| 02:12:17 | × | SteelBlueSilk quits (~SteelBlue@user/SteelBlueSilk) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 02:12:18 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 02:12:18 | × | bcksl quits (~bcksl@user/bcksl) (Quit: \) |
| 02:12:22 | × | Ram-Z quits (~Ram-Z@li1814-254.members.linode.com) (Remote host closed the connection) |
| 02:12:22 | → | xal joins (~xal@mx1.xal.systems) |
| 02:12:24 | × | end quits (~end@user/end/x-0094621) (Quit: end) |
| 02:12:25 | × | son0p quits (~ff@191.104.18.195) (Ping timeout: 245 seconds) |
| 02:12:45 | → | Ram-Z joins (~Ram-Z@li1814-254.members.linode.com) |
| 02:13:05 | → | SteelBlueSilk joins (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) |
| 02:13:05 | × | SteelBlueSilk quits (~SteelBlue@c-98-42-249-36.hsd1.ca.comcast.net) (Changing host) |
| 02:13:05 | → | SteelBlueSilk joins (~SteelBlue@user/SteelBlueSilk) |
| 02:13:15 | × | td_ quits (~td@i5387090C.versanet.de) (Ping timeout: 245 seconds) |
| 02:13:18 | × | Catty quits (~catties@user/meow/catties) (Quit: n_n) |
| 02:13:38 | → | catties joins (~catties@user/meow/catties) |
| 02:13:40 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 245 seconds) |
| 02:14:05 | × | pavonia quits (~user@user/siracusa) (Ping timeout: 245 seconds) |
| 02:14:05 | × | tolt quits (~weechat-h@li219-154.members.linode.com) (Ping timeout: 245 seconds) |
| 02:14:05 | × | _________ quits (~nobody@user/noodly) (Ping timeout: 245 seconds) |
| 02:14:09 | → | td_ joins (~td@i5387090C.versanet.de) |
| 02:14:33 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 02:14:34 | pavonia_ | is now known as pavonia |
| 02:14:55 | × | tzh quits (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Ping timeout: 245 seconds) |
| 02:14:55 | × | Patternmaster quits (~georg@user/Patternmaster) (Ping timeout: 245 seconds) |
| 02:14:55 | × | hughjfchen quits (~hughjfche@vmi556545.contaboserver.net) (Ping timeout: 245 seconds) |
| 02:14:59 | → | _________ joins (~nobody@user/noodly) |
| 02:15:08 | → | tolt joins (~weechat-h@li219-154.members.linode.com) |
| 02:15:46 | → | Patternmaster joins (~georg@user/Patternmaster) |
| 02:15:56 | → | Natch joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
| 02:15:59 | → | hughjfchen joins (~hughjfche@vmi556545.contaboserver.net) |
| 02:18:03 | <glguy> | https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html search for "unidirectional" |
| 02:18:06 | × | trqt quits (~trqt@user/trqt) (Quit: Using Circe, the loveliest of all IRC clients) |
| 02:20:28 | → | bcksl joins (~bcksl@user/bcksl) |
| 02:22:30 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 02:23:01 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:23:27 | × | xdminsy quits (~xdminsy@117.147.70.233) (Ping timeout: 260 seconds) |
| 02:24:54 | → | end joins (~end@user/end/x-0094621) |
| 02:34:11 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 264 seconds) |
| 02:35:39 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:35:59 | × | td_ quits (~td@i5387090C.versanet.de) (Ping timeout: 272 seconds) |
| 02:37:28 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 02:37:40 | → | td_ joins (~td@i5387093D.versanet.de) |
| 02:49:10 | <jackdk> | Or through the provision of `Traversal'`s |
| 02:57:14 | <Inst> | is there any way to simplify this? |
| 02:58:00 | <Inst> | uncurry (<$) . (id &&& tryPutMVar handle.discordHandleLibraryError) |
| 02:58:39 | × | madeleine-sydney quits (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 03:01:40 | <mauke> | add points? |
| 03:03:17 | <Inst> | msg <$ tryPutMVar handle.DiscordHandleLibraryError msg |
| 03:03:26 | <Inst> | I probably don't understand Control.Arrow well enough |
| 03:05:08 | <Inst> | there has to be a combinator wherein you can run a monadic / applicative action on the target, but have the bind value be the target |
| 03:08:02 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds) |
| 03:09:53 | <mauke> | @pl \msg -> msg <$ tryPutMVar handle.DiscordHandleLibraryError msg |
| 03:09:53 | <lambdabot> | ap (<$) ((tryPutMVar handle .) . DiscordHandleLibraryError) |
| 03:11:27 | <mauke> | @pl \msg -> msg <$ tryPutMVar handle_discordHandleLibraryError msg |
| 03:11:27 | <lambdabot> | ap (<$) (tryPutMVar handle_discordHandleLibraryError) |
| 03:11:29 | <jackdk> | Hoogling for `a -> (a -> m b) -> m a` gives two instances of this function |
| 03:13:59 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds) |
| 03:15:13 | → | zmt00 joins (~zmt00@user/zmt00) |
| 03:16:17 | <jackdk> | If you strengthen the type signature from `IfElse`'s `Monad m => (a -> m b) -> (a -> m a)` to `Functor f => (a -> f b) -> a -> f a`, is it then the case that it has only one real implementation? Because the only way to get a `f anything` is to apply the function argument, then you have to `<$` the `a` back into it. Also, it makes it look like a `Lens a a a b`, which might be interesting |
| 03:16:33 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:a472:8995:2c6:603d) (Ping timeout: 256 seconds) |
| 03:19:13 | <Inst> | oof |
| 03:19:16 | <Inst> | thanks mauke, so pointless |
| 03:21:06 | <Inst> | (<$) <*> foo is the most toxic code ever, though |
| 03:24:20 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:28:26 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 03:28:40 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 03:31:01 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:31:58 | → | aforemny_ joins (~aforemny@2001:9e8:6cea:cb00:f739:9bdb:c465:7132) |
| 03:31:58 | × | aforemny quits (~aforemny@2001:9e8:6cc5:7800:397f:89d3:8c7e:e3e5) (Ping timeout: 255 seconds) |
| 03:51:10 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 245 seconds) |
| 03:54:16 | × | qqq quits (~qqq@92.43.167.61) (Remote host closed the connection) |
| 04:00:16 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
| 04:02:35 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 04:05:36 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 04:06:28 | → | sroso joins (~sroso@user/SrOso) |
| 04:06:55 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:22:04 | → | oneeyedalien joins (~oneeyedal@user/oneeyedalien) |
| 04:22:20 | → | madeleine-sydney joins (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) |
| 04:23:11 | → | son0p joins (~ff@191.104.18.195) |
| 04:24:26 | × | oneeyedalien quits (~oneeyedal@user/oneeyedalien) (Remote host closed the connection) |
| 04:27:28 | → | danza_ joins (~francesco@151.57.237.5) |
| 04:29:24 | → | average joins (uid473595@user/average) |
| 04:33:40 | × | danza_ quits (~francesco@151.57.237.5) (Ping timeout: 245 seconds) |
| 04:39:22 | → | michalz joins (~michalz@185.246.207.203) |
| 04:51:56 | × | rdcdr quits (~rdcdr@user/rdcdr) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 04:53:48 | → | benkard joins (~mulk@p5b112e4a.dip0.t-ipconnect.de) |
| 04:54:13 | → | rdcdr joins (~rdcdr@user/rdcdr) |
| 04:54:31 | × | mulk quits (~mulk@p5b2dc97e.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 04:54:32 | benkard | is now known as mulk |
| 05:01:36 | → | rosco joins (~rosco@yp-146-6.tm.net.my) |
| 05:13:53 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 05:17:20 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:30:07 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:31:03 | → | zetef joins (~quassel@5.2.182.98) |
| 05:31:44 | × | madeleine-sydney quits (~madeleine@c-76-155-235-153.hsd1.co.comcast.net) (Quit: Konversation terminated!) |
| 05:37:06 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 05:37:53 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 05:41:37 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 05:43:14 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 05:43:30 | → | euleritian joins (~euleritia@dynamic-176-001-023-202.176.1.pool.telefonica.de) |
| 05:43:48 | × | zetef quits (~quassel@5.2.182.98) (Ping timeout: 255 seconds) |
| 05:46:45 | <energizer> | i guess cartesianProduct distributes over zipWith? |
| 05:53:43 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 268 seconds) |
| 05:55:31 | → | jinsun_ joins (~jinsun@user/jinsun) |
| 05:55:31 | jinsun | is now known as Guest225 |
| 05:55:31 | × | Guest225 quits (~jinsun@user/jinsun) (Killed (cadmium.libera.chat (Nickname regained by services))) |
| 05:55:31 | jinsun_ | is now known as jinsun |
| 05:57:57 | → | acidjnk joins (~acidjnk@p200300d6e714dc53c081e76fe6dc232d.dip0.t-ipconnect.de) |
| 06:07:11 | × | trev quits (~trev@user/trev) (Ping timeout: 264 seconds) |
| 06:20:48 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:36:35 | → | mima joins (~mmh@aftr-62-216-211-228.dynamic.mnet-online.de) |
| 06:39:08 | × | average quits (uid473595@user/average) (Quit: Connection closed for inactivity) |
| 06:41:47 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:56:56 | × | euleritian quits (~euleritia@dynamic-176-001-023-202.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 06:57:20 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:04:15 | → | Guest95 joins (~Guest95@217.7.130.9) |
| 07:08:00 | → | danza_ joins (~francesco@151.57.237.5) |
| 07:18:51 | × | mima quits (~mmh@aftr-62-216-211-228.dynamic.mnet-online.de) (Ping timeout: 252 seconds) |
| 07:32:04 | → | oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 07:34:53 | → | gfundler joins (~user@p5b0f39a4.dip0.t-ipconnect.de) |
| 07:36:20 | × | ft quits (~ft@p4fc2a20e.dip0.t-ipconnect.de) (Quit: leaving) |
| 07:36:57 | → | Square joins (~Square@user/square) |
| 07:39:33 | <Inst> | wait |
| 07:39:40 | <Inst> | https://hackage.haskell.org/package/base-4.19.1.0/docs/src/Control.Arrow.html#Kleisli |
| 07:39:47 | <Inst> | This... is incorrectly documented isn't it? |
| 07:39:53 | <Inst> | It's not a monad, it's simply a parameterized type |
| 07:39:55 | <Inst> | there's no monad constraint here |
| 07:41:15 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds) |
| 07:41:53 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 07:42:01 | → | trev joins (~trev@user/trev) |
| 07:45:01 | <Inst> | the constraints are put in from instances, welp |
| 07:45:28 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 07:48:08 | <Inst> | hmmm, could you treat the kleisli arrows as applicative? |
| 07:49:28 | <Inst> | yeah, you only need pure and fmap to do it |
| 07:55:59 | <Inst> | ah, i understand, applicative kleisli can't be categories, so they can't be arrows |
| 07:57:51 | <probie> | Yeah, you need (sans the Kleisli new type) `(.) :: (b -> m c) -> (a -> m b) -> (a -> m c)`, which is going to require monad |
| 07:58:22 | <probie> | with only `fmap` and `pure`, the best you can do is `(b -> m c) -> (a -> m b) -> (a -> m (m c))` |
| 08:06:08 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 08:08:04 | × | tzh_ quits (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 08:09:01 | × | danza_ quits (~francesco@151.57.237.5) (Read error: Connection reset by peer) |
| 08:18:15 | × | sroso quits (~sroso@user/SrOso) (Read error: Connection reset by peer) |
| 08:19:52 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 08:20:28 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 08:22:29 | → | sroso joins (~sroso@user/SrOso) |
| 08:24:22 | → | lol_ joins (~lol@2603:3016:1e01:b940:500c:2d35:d29f:521d) |
| 08:25:44 | × | philopsos quits (~caecilius@user/philopsos) (Ping timeout: 268 seconds) |
| 08:28:30 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b940:bc60:e296:86fe:18c4) (Ping timeout: 268 seconds) |
| 08:33:44 | → | philopsos joins (~caecilius@user/philopsos) |
| 08:36:34 | → | danse-nr3 joins (~danse-nr3@151.43.249.70) |
| 08:39:16 | <jackdk> | the constraint is on the instance |
| 08:40:13 | × | philopsos quits (~caecilius@user/philopsos) (Ping timeout: 255 seconds) |
| 08:44:46 | → | __monty__ joins (~toonn@user/toonn) |
| 08:50:40 | × | Guest95 quits (~Guest95@217.7.130.9) (Quit: Client closed) |
| 08:54:07 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 08:54:53 | → | euleritian joins (~euleritia@77.22.252.56) |
| 09:00:46 | → | titibandit joins (~titibandi@user/titibandit) |
| 09:06:35 | × | gfundler quits (~user@p5b0f39a4.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 09:19:35 | → | zetef joins (~quassel@5.2.182.98) |
| 09:22:36 | × | zetef quits (~quassel@5.2.182.98) (Remote host closed the connection) |
| 09:25:39 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 09:32:33 | → | xdminsy joins (~xdminsy@117.147.70.233) |
| 09:32:54 | → | mima joins (~mmh@138.246.3.254) |
| 09:34:05 | × | Raito_Bezarius quits (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 240 seconds) |
| 09:34:31 | × | Luj quits (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) (Ping timeout: 256 seconds) |
| 09:35:47 | × | demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 252 seconds) |
| 09:36:54 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
| 09:37:01 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:42:08 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 09:43:32 | → | chele joins (~chele@user/chele) |
| 09:50:44 | → | Luj joins (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) |
| 09:53:18 | → | zetef joins (~quassel@5.2.182.99) |
| 10:05:36 | × | Luj quits (~Luj@2a01:e0a:5f9:9681:5880:c9ff:fe9f:3dfb) (Ping timeout: 256 seconds) |
| 10:09:01 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds) |
| 10:11:07 | gehmehgeh | is now known as gmg |
| 10:13:43 | → | yin joins (~yin@user/zero) |
| 10:15:02 | <haskellbridge> | <irregularsphere> here's something I think would be nice to share (though has some clear issues): https://play.haskell.org/saved/oO6x9Ycd |
| 10:15:09 | yin | is now known as zwrv |
| 10:17:35 | × | Me-me quits (~me-me@2602:ff16:3:0:1:dc:beef:d00d) (Changing host) |
| 10:17:35 | → | Me-me joins (~me-me@user/me-me) |
| 10:20:40 | <ncf> | is that your attempt at exofunctors |
| 10:21:21 | <Inst> | gahhh, streamly |
| 10:21:25 | <haskellbridge> | <irregularsphere> at what? |
| 10:21:28 | <Inst> | i realize i'll probably fall in love with streamly |
| 10:21:36 | <Inst> | do you know what a functor is in category theory? |
| 10:21:51 | <haskellbridge> | <irregularsphere> yes? |
| 10:22:06 | <ncf> | https://dorchard.wordpress.com/2011/10/18/subcategories-in-haskell-exofunctors/ |
| 10:22:35 | × | actioninja quits (~actioninj@user/actioninja) (Ping timeout: 268 seconds) |
| 10:22:46 | <Inst> | streamly honestly is the best library ever; a bunch of Indian guys decide to build a whole new language on top of Haskell with a library and a GHC plugin |
| 10:22:46 | <haskellbridge> | <irregularsphere> oh, I wasn't even the first to think of this |
| 10:24:11 | <danse-nr3> | what matters whether they were indian or not? |
| 10:24:22 | → | yeitrafferin joins (~user@2a04:4540:7213:3800:bf5b:caaa:b515:ed1a) |
| 10:24:53 | <Inst> | it matters insofar as if they open up a donation box, and you give them money, they'll get more work done than if you give money to any other Haskell organization |
| 10:29:28 | <haskellbridge> | <irregularsphere> ...and i was off by a margin of _thirteen_ years |
| 10:30:13 | <danse-nr3> | well that's what we do all the times, but by sharing you found out early |
| 10:30:53 | → | demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 10:31:38 | <haskellbridge> | <irregularsphere> wdym "early" |
| 10:32:56 | <haskellbridge> | <irregularsphere> ncf: thanks for the link by the way |
| 10:40:28 | × | Inst quits (~Inst@user/Inst) (Ping timeout: 268 seconds) |
| 10:45:53 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 10:46:38 | × | Square quits (~Square@user/square) (Ping timeout: 268 seconds) |
| 10:47:12 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 10:48:45 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:48:59 | → | Inst joins (~Inst@user/Inst) |
| 10:50:14 | <Inst> | I've told the Streamly folks (ComposeWell) they really should set up a Haskell consultancy, I guess it's probably their dream or something; they can undercut Serokell and Tweag like crazy |
| 10:50:27 | <Inst> | rather, I told them, they should open up a donation box |
| 10:50:51 | <Inst> | but if they opened up a Haskell consultancy they'd make a ton of money, if they could keep their employees from getting sniped off by Well-Typed / Serokell / Tweag |
| 10:52:57 | <danse-nr3> | haskell openings are not usually driven by low wages though |
| 10:53:32 | <Inst> | usually someone idealistic or willing to give a niche language a shot |
| 10:53:53 | <Inst> | still, the idea of having really cheap Haskell consultants would help move the needle on the business end |
| 10:54:17 | <danse-nr3> | i mean before spending weeks or months on developing a library or something irregularsphere |
| 10:56:30 | <danse-nr3> | haskellers *are* cheap nonetheless, 'cause the market is solid (to mean the opposite of a liquid market). But a cheap wage does not provide much of an edge from what i see in job offers |
| 10:57:40 | <Inst> | I mean that they could open up a consultancy to attempt to compete with Well-Typed / Serokell / Tweag / Galois |
| 11:01:03 | × | zetef quits (~quassel@5.2.182.99) (Remote host closed the connection) |
| 11:02:58 | → | xff0x joins (~xff0x@2405:6580:b080:900:a709:5227:95bf:dd51) |
| 11:03:53 | <Inst> | also TBH, while educated Indians usually know English, you tend to have substantial cultural differences compared to a European or American mainstream, so idioms, choices in API design, values in library construction, can differ |
| 11:09:01 | × | sroso quits (~sroso@user/SrOso) (Quit: Leaving :)) |
| 11:10:10 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 256 seconds) |
| 11:15:54 | × | danse-nr3 quits (~danse-nr3@151.43.249.70) (Ping timeout: 255 seconds) |
| 11:17:00 | × | aforemny_ quits (~aforemny@2001:9e8:6cea:cb00:f739:9bdb:c465:7132) (Ping timeout: 245 seconds) |
| 11:17:46 | → | ph88 joins (~ph88@91.64.63.48) |
| 11:19:01 | → | aforemny joins (~aforemny@2001:9e8:6cf1:5c00:5feb:9e42:c858:fd24) |
| 11:19:44 | → | rvalue joins (~rvalue@user/rvalue) |
| 11:20:24 | × | zwrv quits (~yin@user/zero) (Ping timeout: 255 seconds) |
| 11:22:22 | → | zwrv joins (~yin@user/zero) |
| 11:25:15 | → | Square joins (~Square@user/square) |
| 11:26:39 | <Inst> | speaking of that |
| 11:26:53 | <Inst> | I heard a while back that Warp is bitrotted, I mean, it still works, but it's seriously slow by modern standards |
| 11:27:10 | <Inst> | i was looking at Discord-Haskell and thinking about updating it |
| 11:28:17 | <Inst> | that's what led me back to streamly, and streamly doesn't have an interface for its network connection |
| 11:29:02 | <ph88> | How can i see the instance implementation of Show :+: ? -ddump-deriv doesn't work because the base library is not recompiled https://hackage.haskell.org/package/base-4.19.1.0/docs/GHC-Generics.html#t:Data |
| 11:29:28 | → | destituion joins (~destituio@85.221.111.174) |
| 11:29:50 | <ph88> | i want to override the default somehow and i don't know how to write the instance |
| 11:33:42 | <dminuoso> | Inst: Im not sure that hearsay about the quality of warp is helpful. We use warp in a bunch of different places and we have done profiling. Never was warp a significant hotspot in our profile data. |
| 11:34:33 | → | zetef joins (~quassel@5.2.182.99) |
| 11:34:34 | → | mreh joins (~mreh@2a00:23c7:2803:ef01:8104:39a6:ada6:ece) |
| 11:34:46 | <Inst> | warp got ripped off techempower benchmarks, but back when it was on, it was benchmarking 25-33% of fastest Rust frameworks, and 67% of nginx |
| 11:34:56 | <mreh> | @seen limmeh |
| 11:34:56 | <lambdabot> | I haven't seen limmeh. |
| 11:35:09 | <mreh> | @seen lemmih |
| 11:35:10 | <lambdabot> | I haven't seen lemmih. |
| 11:35:20 | <mreh> | huh |
| 11:35:34 | <mreh> | I guess he doesn't come on here any more |
| 11:35:50 | <mreh> | I was hoping to chat to someone about hgeometry |
| 11:36:02 | <Inst> | just saying, if Haskell performance experts were to give warp / wai etc a makeover, would at least bring haskell back in the running |
| 11:37:33 | <dminuoso> | A straight-up comparison of warp against rust is going to be difficult, and probably not helpful either. If the HTTP server implementation itself is a relevant hotspot you either have an atypical web application that, for some reason, is not doing any IO or CPU time in the request processing, or you have scaled to a point where even a small percentage improvement will translate into huge cost |
| 11:37:36 | <dminuoso> | savings. |
| 11:38:57 | <dminuoso> | And just blanket performance comparisons between "X in language A" and "X in language B" easily introcues the risk of doing something non-idiomatic in one language, or having some requirement orthogonal to the server implementation, and rather about the language itself. |
| 11:40:59 | <dminuoso> | I would expect a careful thorough analysis with code examples. |
| 11:41:04 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:42:01 | × | euphores quits (~SASL_euph@user/euphores) (Read error: Connection reset by peer) |
| 11:42:02 | <dminuoso> | All I can say is: This is the first time I've ever heard warp being called slow. All our bottlenecks were in request processing (usually space leaks, or doing inefficient database processing like converting fields through text formats) |
| 11:42:24 | <dminuoso> | I really have a hard time imagining warp being a *relevant* bottleneck. |
| 11:42:33 | <Inst> | the issue wasn't that it was a straight benchmark vs Rust, beating Rust is difficult if not impossible, but it was also a comparison against frameworks written in Java, Go, C#, etc... Warp was apparently losing to all of them |
| 11:42:45 | <dminuoso> | Warp is not a framework. |
| 11:42:48 | <dminuoso> | Warp is just a WAI server. |
| 11:42:58 | <dminuoso> | That's where the issue here is. |
| 11:43:18 | <dminuoso> | It sounds like you or they were comparing a HTTP interface server implementation with some framework. |
| 11:43:53 | <dminuoso> | It's like you're comparing FastCGI to Express.js. Apples and oranges. |
| 11:44:29 | <Inst> | i mean Yesod was listed, as was Servant, Servant + Postgresql iirc was rating 17% or so |
| 11:45:01 | <dminuoso> | See, this is why random hearsay is not useful. You are not only comparing apples and oranges, you are comparing fruit salad with oranges. |
| 11:45:22 | <dminuoso> | Servant has very little overhead (well other than compile-time overhead) |
| 11:46:12 | <dminuoso> | With postgresql, were they using hasql? or postgresql-simple? persistent? |
| 11:46:33 | <dminuoso> | Were the queries written by hand? What types were they serialized in? By what code? |
| 11:46:42 | × | mreh quits (~mreh@2a00:23c7:2803:ef01:8104:39a6:ada6:ece) (Quit: Client closed) |
| 11:47:02 | <Inst> | gotta go |
| 11:48:42 | <ph88> | Inst, 25-33% in range or rust? that can't be right |
| 11:48:44 | <dminuoso> | This is why you should publish not just "25-33%" number, but a full analysis, code involved, a comparison why two implementations should be equivalent (and say not doing some silly space leak in Haskell due to using foldl instead of foldl'), and full statistical data. |
| 11:49:04 | <Inst> | i'm going to try to get the techempower benchmarks |
| 11:49:18 | <ph88> | let me get them for you |
| 11:49:21 | <dminuoso> | If you use postgresql-simple and have lots of row processing, you will probably be paying a hefty peformance penalty because postgresql-simple uses the text interface of libpq |
| 11:49:41 | <dminuoso> | Switching that to hasql can potentially increase the performance up to a factor 8x on raw de-/serialization time. |
| 11:50:46 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 11:51:53 | → | euphores joins (~SASL_euph@user/euphores) |
| 11:53:19 | <ph88> | snap 416888 requests/s max https://tfb-status.techempower.com/unzip/results.2018-02-04-00-49-39-094.zip/home/techempower/FrameworkBenchmarks/results/20180131110755/snap/plaintext/raw.txt |
| 11:53:34 | <ph88> | actix 2616147 requests/s max https://tfb-status.techempower.com/unzip/results.2018-02-04-00-49-39-094.zip/home/techempower/FrameworkBenchmarks/results/20180131110755/actix/plaintext/raw.txt |
| 11:54:19 | <ph88> | haskell snap 16% performance of actix 100% |
| 11:54:24 | × | zwrv quits (~yin@user/zero) (Ping timeout: 252 seconds) |
| 11:54:25 | <dminuoso> | This has no profile data and shows no code. |
| 11:54:30 | <dminuoso> | Who knows why that is. |
| 11:54:43 | <ph88> | code is on github as usual, you can profile it |
| 11:54:52 | <dminuoso> | Not my job, honestly. |
| 11:55:06 | <ph88> | this is the latest result from techempower before snap got pulled out https://github.com/TechEmpower/FrameworkBenchmarks/blob/2d9b618c99ba0b0073eb49ffdb9e884bf640be1a/frameworks/Haskell/snap/benchmark_config.json#L24 |
| 11:56:09 | <dminuoso> | ph88: But really, if you do take a quick peek, this is highly synthetic and in no way representative of real code: https://github.com/TechEmpower/FrameworkBenchmarks/blob/master/frameworks/Haskell/snap/bench/src/Main.hs |
| 11:56:27 | → | zwrv joins (~yin@user/zero) |
| 11:56:49 | <dminuoso> | And it mixes in a bunch of libraries to the point that its impossible to say why this is slow. |
| 11:57:37 | <ph88> | on real world code you add in more libraries and IO, if we want to compare the webserver part only plaintext is the best benchmark to test routing and simple responses |
| 11:58:04 | <ph88> | somebody put up that snap benchmark code as best effort at the time |
| 11:58:16 | <dminuoso> | If http and routing performance is ever relevant to you, you will either have reached global scaling or have a very exotic use case. |
| 11:58:34 | <dminuoso> | ph88: The snap code does more, it also does database interaction |
| 11:58:36 | <dminuoso> | With mysql-simple. |
| 11:58:42 | <ph88> | all parts combined are relevant and http and routing is part of the total latency |
| 11:58:57 | <ph88> | if you want to add in additional parts there are also benchmarks with json formatting and postgresql access |
| 11:59:07 | <Inst> | https://www.techempower.com/benchmarks/#section=data-r22&hw=ph&test=json |
| 11:59:28 | → | rvalue joins (~rvalue@user/rvalue) |
| 11:59:31 | <dminuoso> | In my HTTP code, about half the time is spend in database IO, and the other is spend in crunching on millions of tree nodes. |
| 11:59:40 | <ph88> | it's one codebase for about 5 different benchmarks, it's been this way for many years |
| 11:59:40 | <dminuoso> | The HTTP overhead? Completely negligable. |
| 11:59:51 | <dminuoso> | Routing overhead? Probably microseconds? |
| 12:00:19 | <dminuoso> | ph88: Ah fiar enough. |
| 12:00:22 | <ph88> | ye that's of course up to you if you want to crunch millions of tree nodes in a blocking way |
| 12:00:28 | <Inst> | IHP is doing much better these days |
| 12:01:06 | <dminuoso> | ph88: Performance is best measured in your specific problem domain, because chances are the bottlenecks will things you dont think about. |
| 12:01:14 | <dminuoso> | Especially for libraries. |
| 12:01:21 | <Inst> | considering its baseline was garbage, of course :3 |
| 12:01:40 | <ph88> | but ecosystem optimization is best measured by libraries commonly used shared between many real world apps |
| 12:02:41 | <dminuoso> | ph88: Dunno, so if you look at snap, there shouldnt even be a database handler in there because snap does not have database interaction. |
| 12:02:59 | <dminuoso> | You're suddenly conflating snap with mysql-simple |
| 12:03:23 | <dminuoso> | Just using what you imagine would probably be used is a silly thing to do. |
| 12:03:29 | <ph88> | the mysql handler should not be hit on the route that serves plaintext |
| 12:03:40 | <dminuoso> | ph88: There should not be a db handler to begin with! |
| 12:03:42 | <dminuoso> | That's what Im saying. |
| 12:03:58 | <dminuoso> | And there should also not be a JSON handler |
| 12:04:05 | <dminuoso> | Because snap has neither JSON nor database interaction. |
| 12:04:13 | <ph88> | it's part of the benchmark requirements so that all implementations have some kind of database handler inside. That doesn't mean that that code gets executed for all benchmarks |
| 12:04:21 | <dminuoso> | You can do JSON and database interaction with *different* libraries and get different results. |
| 12:04:58 | <dminuoso> | That's a silly requirement, then. |
| 12:05:10 | <dminuoso> | It introduces the notion that modular frameworks cant exist. |
| 12:05:15 | <ph88> | It's an end to end test for 5 different uses cases in 1 codebase for each implementation. The implementations are then compared to each other |
| 12:05:53 | <ph88> | You can click on the buttons below "Test types" https://www.techempower.com/benchmarks/ it was already like that when the haskell frameworks where still on the charts |
| 12:06:51 | × | p3n quits (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (Quit: ZNC 1.8.2 - https://znc.in) |
| 12:07:42 | <ph88> | code loaded in RAM/cache but not executed is not going to make a significant difference in the benchmark results with so many iterations |
| 12:10:12 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 12:10:35 | → | akegalj joins (~akegalj@78-1-52-121.adsl.net.t-com.hr) |
| 12:13:46 | × | rosco quits (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 12:18:16 | → | rvalue joins (~rvalue@user/rvalue) |
| 12:18:25 | → | danse-nr3 joins (~danse-nr3@151.19.252.50) |
| 12:19:52 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:30:35 | × | koz quits (~koz@121.99.240.58) (Ping timeout: 260 seconds) |
| 12:32:22 | → | koz joins (~koz@121.99.240.58) |
| 12:34:58 | × | Inst quits (~Inst@user/Inst) (Ping timeout: 246 seconds) |
| 12:52:07 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:57:32 | <ph88> | how can i denote that something is of kind type ? |
| 13:03:57 | → | ystael joins (~ystael@user/ystael) |
| 13:10:25 | <ncf> | :: Type |
| 13:11:06 | <akegalj> | (from GHC.Types) |
| 13:12:07 | × | akegalj quits (~akegalj@78-1-52-121.adsl.net.t-com.hr) (Quit: leaving) |
| 13:13:46 | <ncf> | or Data.Kind |
| 13:14:48 | <dminuoso> | ph88: *of type Type |
| 13:15:27 | <dminuoso> | TypeInType is already the default, the extension merely removes the veil that massages all the diagnostics so it looks like we still have a kind system. |
| 13:15:52 | <dminuoso> | (And it removes some of the rather arbitrary restrictions to let you think TypeInType was not on) |
| 13:16:53 | × | Buggys quits (~Buggys@Buggy.shelltalk.net) (Ping timeout: 240 seconds) |
| 13:17:26 | <ph88> | we don't have a kind system? :> |
| 13:17:57 | <dminuoso> | No, we dont really anymore. |
| 13:18:02 | <dminuoso> | It's TypeInType. |
| 13:18:05 | <dminuoso> | Type :: Type |
| 13:18:18 | <dminuoso> | GHC is just lying to you every time it mentions the word kind. |
| 13:18:42 | <ph88> | do you have TypeInType on by default ? |
| 13:19:06 | <dminuoso> | ph88: Like I said, internally its already doing TypeInType. |
| 13:19:28 | <dminuoso> | The extension merely lifts some restrictions |
| 13:20:14 | <dminuoso> | https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/poly_kinds.html |
| 13:20:21 | <dminuoso> | "The extension TypeInType is now deprecated: its sole effect is to switch on PolyKinds (and hence KindSignatures) and DataKinds." |
| 13:20:59 | <dminuoso> | So no, we do not have a kind system anymore in GHC Haskell. |
| 13:22:38 | <dminuoso> | It's somewhat confusing that the word `kind` is still used all over the place in the manuals and diagnostics. |
| 13:23:09 | <ph88> | yes that's very confusing |
| 13:23:16 | <dminuoso> | But if we understand `kind` to mean the type of a type, I guess its alright. |
| 13:23:19 | <haskellbridge> | <irregularsphere> there was a kind system? |
| 13:23:22 | <Hecate> | ph88: Kind = Type :D |
| 13:23:47 | <dminuoso> | irregularsphere |
| 13:23:48 | <dminuoso> | irregularsphere: Yes. |
| 13:24:04 | <dminuoso> | We used to have a finite tower: Value -> Type -> Kind -> Sort |
| 13:24:11 | → | Buggys joins (Buggys@shelltalk.net) |
| 13:25:23 | <dminuoso> | At that time, there was only one Sort called BOX, so it used to be that `* :: BOX` and `(* -> *) :: BOX`, etc |
| 13:26:45 | <haskellbridge> | <irregularsphere> let me guess, it had no use? |
| 13:27:57 | <dminuoso> | I dont have experience from the time, but Im sure it was useful to denote that a particular thing is a kind. |
| 13:28:11 | <dminuoso> | i.e. `type family F (k :: BOX) ...` |
| 13:28:25 | <dminuoso> | Maybe it was even necessary for some interaction with other exdtensions |
| 13:29:19 | <danse-nr3> | so is that only Value -> Type now? |
| 13:29:36 | <dminuoso> | No, its Value -> Type -> Type -> Type -> Type -> ... |
| 13:29:55 | <danse-nr3> | oh |
| 13:29:58 | <dminuoso> | Compare with Agda's infinite tower `Bool : Set : Set1 : Set2 : Set3 : ...` |
| 13:30:36 | <dminuoso> | danse-nr3: Its why the most concise description of TypeInType is `Type :: Type` |
| 13:30:48 | <haskellbridge> | <irregularsphere> sounds like an improvement over the finite tower though |
| 13:31:19 | → | erty joins (~user@user/aeroplane) |
| 13:31:23 | <dminuoso> | irregularsphere: Well, it's a very important step for dependently typed haskell. |
| 13:31:32 | <danse-nr3> | interesting, had a very different mental model, i also thought it was Value -> Type -> Kind -> YouDontWannaKnow |
| 13:31:42 | ncf | . o O ( Bool : repeat Type ) |
| 13:32:14 | <dminuoso> | Yeah that YouDontWannaKnow was called Sort at the time. |
| 13:32:39 | <danse-nr3> | an infinite tower feels more freeing i guess (: |
| 13:34:01 | <ncf> | agda also uses "sort" to talk about types of types (so, what haskell used to call kinds and sorts) |
| 13:34:24 | <dminuoso> | So allowing for `Type :: Type` is a double edged swords. On one hand it acts as a simplification in the underlying type system, but it comes at the cost of allowing non-termination in the type system. |
| 13:34:58 | <dminuoso> | But it was swiftly argued that we have plenty of mechanisms (e.g. tyfams) to do that anyway, so we already paid for that. |
| 13:35:31 | <dminuoso> | https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf is a really nice paper to read |
| 13:36:42 | <dminuoso> | ncf: The infinite tower is a requirement I believe if you want termination in a dependently typed language. |
| 13:36:56 | <dminuoso> | Termination in the type system, that is. |
| 13:37:00 | <dminuoso> | Or in type checking, rather. |
| 13:37:03 | <ncf> | termination at all |
| 13:37:50 | <ncf> | you can do russell's (or girard's) paradox and get a nonterminating term |
| 13:38:47 | <dminuoso> | Ah I guess there's no difference since in a fully dependently typed language there no longer is a difference between expression and types? |
| 13:44:09 | <ncf> | yeah, the type checker has to evaluate terms sometimes |
| 13:46:43 | × | notzmv quits (~daniel@user/notzmv) (Read error: Connection reset by peer) |
| 13:49:23 | × | xff0x quits (~xff0x@2405:6580:b080:900:a709:5227:95bf:dd51) (Ping timeout: 256 seconds) |
| 13:54:30 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 245 seconds) |
| 13:54:48 | → | euleritian joins (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) |
| 13:58:10 | × | hueso quits (~root@user/hueso) (Quit: hueso) |
| 13:59:37 | <zwrv> | if i write a medium sized project in both simple, idiomatic haskell and simple, idiomatic chez scheme, which one would you bet to perform the best speedwise? |
| 14:02:02 | <ph88> | is haskell on the way to be dependently typed ? |
| 14:02:03 | → | hueso joins (~root@user/hueso) |
| 14:02:37 | <__monty__> | zwrv: I wouldn't take anyone's word for it for one thing. |
| 14:03:21 | <zwrv> | __monty__: i know i know |
| 14:06:43 | <EvanR> | a dependently typed system doesn't necessarily need an infinite hierarchy of Type, it could provide like 5 levels and say screw you if you end up needing more. Similar to GHC's tuple sizes |
| 14:09:02 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 14:09:30 | <haskellbridge> | <irregularsphere> EvanR: yes, but I guess it's better to live off an already infinite tower |
| 14:09:39 | <haskellbridge> | <irregularsphere> s/yes/sure |
| 14:10:30 | <EvanR> | you can also ignore the issue and do Type : Type, if stuff like girard's paradox doesn't bother you |
| 14:10:45 | → | xff0x joins (~xff0x@2405:6580:b080:900:a709:5227:95bf:dd51) |
| 14:10:50 | <EvanR> | which is what dependent haskell does |
| 14:13:52 | → | notzmv joins (~daniel@user/notzmv) |
| 14:17:19 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 14:17:38 | → | gmg joins (~user@user/gehmehgeh) |
| 14:20:36 | × | zwrv quits (~yin@user/zero) (Ping timeout: 256 seconds) |
| 14:22:14 | → | zwrv joins (~yin@user/zero) |
| 14:22:58 | <zwrv> | dependent haskell makes the type system inconsistent? |
| 14:23:36 | <ncf> | :t undefined |
| 14:23:37 | <lambdabot> | a |
| 14:23:44 | <ncf> | :t undefined :: Void |
| 14:23:45 | <lambdabot> | Void |
| 14:23:51 | <ncf> | looks pretty inconsistent to me already |
| 14:25:32 | <EvanR> | type system is already inconsistent, but I vaguely recall additional separate reasoning about it |
| 14:26:59 | <danse-nr3> | i don't get your example ncf. undefined is any type, therefore also Void |
| 14:27:21 | <danse-nr3> | oh i see, void is supposed to be void ... |
| 14:27:44 | <danse-nr3> | :/ |
| 14:30:26 | <EvanR> | Void is a type with no values. Yet we found one anyway xD |
| 14:30:30 | <EvanR> | contradiction |
| 14:30:56 | <EvanR> | never a good sign |
| 14:31:39 | × | cods quits (~fred@tuxee.net) (Ping timeout: 272 seconds) |
| 14:41:02 | → | Raito_Bezarius joins (~Raito@wireguard/tunneler/raito-bezarius) |
| 14:46:48 | × | euleritian quits (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 14:47:16 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 14:49:05 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 14:50:36 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Client Quit) |
| 14:55:37 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 14:58:39 | × | shapr quits (~user@c-24-218-186-89.hsd1.ma.comcast.net) (Ping timeout: 252 seconds) |
| 14:59:10 | → | average joins (uid473595@user/average) |
| 14:59:55 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 245 seconds) |
| 15:05:26 | → | Guest13 joins (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) |
| 15:06:52 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 15:07:20 | → | euleritian joins (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) |
| 15:09:05 | <zwrv> | undefined is not proper Haskell |
| 15:09:22 | <EvanR> | it's in the Report |
| 15:09:32 | → | p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 15:09:53 | <zwrv> | the Report is not proper Haskell |
| 15:10:06 | <danse-nr3> | well... |
| 15:10:15 | zwrv | hides |
| 15:12:07 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:13:06 | × | euleritian quits (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:13:13 | → | Piedro joins (~Piedro@213.226.141.81) |
| 15:13:25 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:14:55 | × | destituion quits (~destituio@85.221.111.174) (Read error: Connection reset by peer) |
| 15:17:05 | → | destituion joins (~destituio@85.221.111.174) |
| 15:17:58 | × | titibandit quits (~titibandi@user/titibandit) (Ping timeout: 268 seconds) |
| 15:26:16 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
| 15:30:32 | × | destituion quits (~destituio@85.221.111.174) (Ping timeout: 252 seconds) |
| 15:32:46 | → | destituion joins (~destituio@2a02:2121:340:2456:fffe:d0f:7737:dd1) |
| 15:39:03 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 15:46:00 | → | philopsos joins (~caecilius@user/philopsos) |
| 15:46:34 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 15:47:34 | → | gmg joins (~user@user/gehmehgeh) |
| 15:52:17 | → | tzh joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 15:54:45 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 15:54:53 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:55:28 | → | euleritian joins (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) |
| 16:04:06 | × | euleritian quits (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 16:09:22 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 16:13:54 | × | danse-nr3 quits (~danse-nr3@151.19.252.50) (Read error: Connection reset by peer) |
| 16:14:04 | → | danse-nr3 joins (~danse-nr3@151.35.248.91) |
| 16:14:16 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 16:15:44 | → | noumenon joins (~noumenon@113.51-175-156.customer.lyse.net) |
| 16:18:45 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 16:19:38 | <c_wraith> | given that nontermination exists, undefined doesn't allow anything new. it's just an optimized form of nontermination |
| 16:20:42 | <EvanR> | you can't experimentally prove non termination exists |
| 16:20:52 | <EvanR> | :P |
| 16:22:50 | <c_wraith> | all programs terminate when the hardware they're running on fails! |
| 16:26:40 | <EvanR> | > 2 + 2 |
| 16:26:42 | <lambdabot> | 4 |
| 16:26:46 | <EvanR> | termination exists |
| 16:27:20 | → | titibandit joins (~titibandi@user/titibandit) |
| 16:27:50 | <c_wraith> | see Schwarzenegger (1984) |
| 16:27:52 | × | aforemny quits (~aforemny@2001:9e8:6cf1:5c00:5feb:9e42:c858:fd24) (Ping timeout: 260 seconds) |
| 16:28:09 | → | aforemny joins (~aforemny@i59F516CB.versanet.de) |
| 16:28:10 | <enikar> | :D |
| 16:32:28 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:33:26 | × | Guest13 quits (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) (Ping timeout: 250 seconds) |
| 16:37:06 | × | aforemny quits (~aforemny@i59F516CB.versanet.de) (Ping timeout: 252 seconds) |
| 16:42:10 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:43:39 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:46:10 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 16:46:29 | → | aforemny joins (~aforemny@i59F516C4.versanet.de) |
| 16:46:29 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:47:18 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 16:49:51 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 268 seconds) |
| 16:52:50 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 16:53:23 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:54:51 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:54:56 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 17:02:51 | × | danse-nr3 quits (~danse-nr3@151.35.248.91) (Ping timeout: 255 seconds) |
| 17:20:05 | → | aforemny_ joins (~aforemny@i59F516D2.versanet.de) |
| 17:20:56 | × | zetef quits (~quassel@5.2.182.99) (Remote host closed the connection) |
| 17:21:06 | × | aforemny quits (~aforemny@i59F516C4.versanet.de) (Ping timeout: 252 seconds) |
| 17:24:28 | → | aforemny joins (~aforemny@i59F516CD.versanet.de) |
| 17:24:30 | × | aforemny_ quits (~aforemny@i59F516D2.versanet.de) (Ping timeout: 245 seconds) |
| 17:29:50 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 17:31:47 | × | aforemny quits (~aforemny@i59F516CD.versanet.de) (Ping timeout: 264 seconds) |
| 17:32:12 | → | aforemny joins (~aforemny@i59F516F4.versanet.de) |
| 17:34:27 | → | ft joins (~ft@p4fc2a20e.dip0.t-ipconnect.de) |
| 17:35:50 | → | aforemny_ joins (~aforemny@2001:9e8:6cf4:bd00:73c6:e367:95b1:7b24) |
| 17:36:29 | × | erty quits (~user@user/aeroplane) (Ping timeout: 252 seconds) |
| 17:36:35 | × | aforemny quits (~aforemny@i59F516F4.versanet.de) (Ping timeout: 245 seconds) |
| 17:38:51 | × | average quits (uid473595@user/average) (Quit: Connection closed for inactivity) |
| 17:45:11 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 17:51:35 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:52:33 | × | Piedro quits (~Piedro@213.226.141.81) (Remote host closed the connection) |
| 17:52:55 | × | xdminsy quits (~xdminsy@117.147.70.233) (Read error: Connection reset by peer) |
| 17:53:40 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 245 seconds) |
| 17:53:40 | → | xdminsy joins (~xdminsy@117.147.70.233) |
| 17:54:25 | → | zetef joins (~quassel@5.2.182.99) |
| 17:56:02 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 17:56:17 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Quit: BRB) |
| 18:00:44 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 18:02:59 | × | mima quits (~mmh@138.246.3.254) (Ping timeout: 264 seconds) |
| 18:12:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:13:31 | × | aforemny_ quits (~aforemny@2001:9e8:6cf4:bd00:73c6:e367:95b1:7b24) (Ping timeout: 255 seconds) |
| 18:14:51 | → | aforemny joins (~aforemny@2001:9e8:6cf5:700:8293:43c4:5a8e:1e5d) |
| 18:18:28 | <mauke> | I have solved the halting problem ... with an axe |
| 18:23:59 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 18:26:32 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 256 seconds) |
| 18:30:24 | × | zwrv quits (~yin@user/zero) (Ping timeout: 252 seconds) |
| 18:32:00 | → | zwrv joins (~yin@user/zero) |
| 18:36:20 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 18:37:51 | → | rvalue- joins (~rvalue@user/rvalue) |
| 18:39:05 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 256 seconds) |
| 18:39:39 | × | zetef quits (~quassel@5.2.182.99) (Read error: Connection reset by peer) |
| 18:41:10 | × | causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1) |
| 18:44:07 | rvalue- | is now known as rvalue |
| 18:54:00 | → | wroathe joins (~wroathe@50.205.197.50) |
| 18:54:00 | × | wroathe quits (~wroathe@50.205.197.50) (Changing host) |
| 18:54:00 | → | wroathe joins (~wroathe@user/wroathe) |
| 18:57:09 | × | foul_owl quits (~kerry@157.97.134.165) (Ping timeout: 255 seconds) |
| 19:01:39 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 255 seconds) |
| 19:09:15 | → | mima joins (~mmh@aftr-62-216-211-51.dynamic.mnet-online.de) |
| 19:11:23 | × | aforemny quits (~aforemny@2001:9e8:6cf5:700:8293:43c4:5a8e:1e5d) (Ping timeout: 268 seconds) |
| 19:11:38 | → | aforemny_ joins (~aforemny@2001:9e8:6cf5:7900:78ba:d909:e114:a6ce) |
| 19:14:55 | × | Square quits (~Square@user/square) (Ping timeout: 245 seconds) |
| 19:17:25 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:21:15 | <energizer> | what's the haskell version of NamedTuple? a record type created on the fly, modifiable on the fly |
| 19:21:35 | × | aforemny_ quits (~aforemny@2001:9e8:6cf5:7900:78ba:d909:e114:a6ce) (Ping timeout: 245 seconds) |
| 19:21:44 | <EvanR> | extensible record? |
| 19:21:54 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 19:22:23 | → | aforemny joins (~aforemny@2001:9e8:6cf5:9300:d93f:3d17:cef0:4b79) |
| 19:22:31 | <EvanR> | see also dependent map |
| 19:22:32 | <ncf> | wdym modifiable |
| 19:24:18 | <energizer> | eg if you have a record you can make another record by dropping a field |
| 19:24:53 | <energizer> | i looked up extensible records and found an old paper with this syntax {a = True, b = "Hello", c = 12::Int} but it doesnt seem to work in my ghci |
| 19:25:22 | <EvanR> | there's are more than one library implementing it in haskell, but I haven't see any which are particularly easy to use |
| 19:25:52 | <EvanR> | on the subject of dropping fields, there's more or less complex logic you can encode into the types to say what you want, because this is haskell!!! |
| 19:26:23 | <EvanR> | some extensible records implementations support dropping of fields, some don't |
| 19:26:45 | → | foul_owl joins (~kerry@185.216.231.182) |
| 19:28:17 | <EvanR> | https://hackage.haskell.org/package/vinyl |
| 19:28:32 | <ski> | energizer : cf. <https://www.haskell.org/hugs/pages/hugsman/exts.html#trex> |
| 19:35:05 | <energizer> | ski: can i use that in normal haskell or do i need a special environment? |
| 19:36:09 | → | ec_ joins (~ec@gateway/tor-sasl/ec) |
| 19:36:18 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 260 seconds) |
| 19:39:31 | <ncf> | well you need hugs |
| 19:42:31 | <ski> | energizer : as far as you consider Hugs as "normal Haskell", sure. it is a Hugs extension, of course, just like there's GHC extensions, and also some extensions that are shared |
| 19:42:49 | <energizer> | i think that's a no |
| 19:43:03 | <ski> | (but Hugs hasn't been updated in a long time, and doesn't support libraries making heavy use of extensions. it still works, though) |
| 19:43:52 | <ski> | in any case, the main point of linking to it is to give some idea of one take on how it could look, as a language feature/extension (rather than encoding in some way, in a library, using existing features) |
| 19:44:22 | × | aforemny quits (~aforemny@2001:9e8:6cf5:9300:d93f:3d17:cef0:4b79) (Ping timeout: 268 seconds) |
| 19:44:32 | → | aforemny_ joins (~aforemny@i59f516e0.versanet.de) |
| 19:47:37 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 19:48:05 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 19:49:22 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:50:58 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:52:45 | × | wroathe quits (~wroathe@user/wroathe) (Quit: leaving) |
| 19:53:34 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 260 seconds) |
| 19:54:30 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 19:54:46 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 19:55:15 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 19:55:20 | × | philopsos quits (~caecilius@user/philopsos) (Ping timeout: 245 seconds) |
| 19:56:28 | × | yeitrafferin quits (~user@2a04:4540:7213:3800:bf5b:caaa:b515:ed1a) (Remote host closed the connection) |
| 19:59:10 | × | califax quits (~califax@user/califx) (Ping timeout: 260 seconds) |
| 20:00:35 | → | califax joins (~califax@user/califx) |
| 20:01:38 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 20:08:08 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 20:10:32 | → | mei joins (~mei@user/mei) |
| 20:10:53 | × | zwrv quits (~yin@user/zero) (Ping timeout: 268 seconds) |
| 20:11:26 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:15:32 | → | Luj joins (~Luj@2a01:e0a:5f9:9681:627d:73c1:73b3:2561) |
| 20:17:15 | → | zwrv joins (~yin@user/zero) |
| 20:19:34 | <dminuoso> | 16:22:49 c_wraith │ all programs terminate when the hardware they're running on fails! |
| 20:19:42 | arthurvl | is now known as earthy |
| 20:20:29 | <dminuoso> | Under the assumption of accelerated cosmic expansion, you will eventually fail on heat death of the observable universe. |
| 20:20:31 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 20:29:28 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 20:31:08 | <monochrom> | Yeah computers fails under heat death too. |
| 20:31:43 | <EvanR> | reversible computer not affected |
| 20:32:44 | <EvanR> | it just continues to compute and uncompute the results forever |
| 20:33:10 | <EvanR> | make the question it's answering a good one |
| 20:38:29 | <monochrom> | :) |
| 20:41:26 | × | titibandit quits (~titibandi@user/titibandit) (Read error: Connection reset by peer) |
| 20:45:20 | <geekosaur> | INSUFFICIENT DATA FOR MEANINGFUL ANSWER |
| 20:46:56 | <c_wraith> | but the computer eventually figured that one out. |
| 20:55:30 | <c_wraith> | amusingly, the solution the computer came up with had a lot in common with Penrose's Conformal Cyclic Cosmology |
| 20:56:27 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 20:58:29 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 21:04:24 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 252 seconds) |
| 21:05:09 | × | zwrv quits (~yin@user/zero) (Ping timeout: 268 seconds) |
| 21:11:42 | → | zwrv joins (~yin@user/zero) |
| 21:12:32 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 21:14:01 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 21:16:17 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:18:38 | × | michalz quits (~michalz@185.246.207.203) (Quit: ZNC 1.8.2 - https://znc.in) |
| 21:20:10 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:22:06 | × | ec_ quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 21:22:41 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 21:24:16 | × | acidjnk quits (~acidjnk@p200300d6e714dc53c081e76fe6dc232d.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 21:25:30 | → | pavonia joins (~user@user/siracusa) |
| 21:27:26 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:28:57 | → | waldo joins (~waldo@user/waldo) |
| 21:50:18 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 21:53:31 | × | bollu quits (~bollu@159.65.151.13) (Quit: The Lounge - https://thelounge.chat) |
| 21:53:58 | → | bollu joins (~bollu@159.65.151.13) |
| 21:59:26 | → | chiselfu1e joins (~chiselfus@user/chiselfuse) |
| 22:00:34 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 22:03:12 | <haskellbridge> | <irregularsphere> (continuning discussion about exofunctors) by the way, I realized my code snippet's problem is at `<*>` because that does not appear in the traditional definition of a lax monoidal functor, rather only on Haskell (with their `id f a = f a`) |
| 22:03:32 | <haskellbridge> | <irregularsphere> could have realized this sooner, I know |
| 22:04:31 | <haskellbridge> | <irregularsphere> also, I found freelude which is interesting too |
| 22:04:59 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 22:05:08 | <ncf> | what problem? |
| 22:06:27 | <ncf> | haskell's definition is something like a lax closed functor, which are equivalent to lax monoidal functors between monoidal closed categories |
| 22:07:04 | × | Lears quits (~Leary]@user/Leary/x-0910699) (Ping timeout: 255 seconds) |
| 22:08:01 | <ncf> | but yes it looks like constraining x -> y is a bit random |
| 22:08:46 | <ncf> | i guess you need that because of the precondition thing on FuncOf? |
| 22:12:23 | → | peterbecich joins (~Thunderbi@47.229.123.186) |
| 22:15:04 | <ncf> | i guess the issue here is that Eq is not a *closed* subcategory of Hask |
| 22:15:30 | <ncf> | so you can get away with ConsMonoidal but not ConsApplicative |
| 22:18:29 | <haskellbridge> | <irregularsphere> ncf: constraints asking for too much, e.g. `a (x -> y)` |
| 22:18:48 | <haskellbridge> | <irregularsphere> I need the precondition because of `(<*>) = liftA2 id` |
| 22:19:14 | <haskellbridge> | <irregularsphere> and `liftA2 f a = (<*>) fmapC (f a)` |
| 22:20:23 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 268 seconds) |
| 22:20:39 | <haskellbridge> | <irregularsphere> `liftA2 f a = (<*> (fmapC f a))*` |
| 22:21:32 | <haskellbridge> | <irregularsphere> since `f :: x -> y -> z` then `fmapC` implies `a x, a (y -> z)`, thus `(<*>) fs as = liftA2 id` and `id :: (x -> y) -> x -> y` implies `a (x -> y)` |
| 22:23:04 | <haskellbridge> | <irregularsphere> and yes haskell's Applicative is that (I don't know what a lax closed functor is specifically) but after constraining you don't see `a (x -> y)` that much |
| 22:23:23 | × | cyphase quits (~cyphase@user/cyphase) (Quit: cyphase.com) |
| 22:24:32 | <haskellbridge> | <irregularsphere> I realized `<*>`'s type signature is `f (x -> y) -> f x- > f y`, since `f` is assumed to work on values of `a` then `f (x -> y)` does not make much sense either |
| 22:24:38 | <ncf> | https://ncatlab.org/nlab/show/closed+functor |
| 22:25:30 | <haskellbridge> | <irregularsphere> ah |
| 22:25:49 | <haskellbridge> | <irregularsphere> so my code snippet only works on closed subcategories |
| 22:27:29 | <haskellbridge> | <irregularsphere> well then I guess it being specifically a closed subcategory is not good! imagine `Eq (x -> y)` |
| 22:29:35 | → | cyphase joins (~cyphase@user/cyphase) |
| 22:31:56 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:37:02 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:37:06 | × | Pixi__ quits (~Pixi@user/pixi) (Quit: Leaving) |
| 22:37:53 | → | Pixi joins (~Pixi@user/pixi) |
| 22:39:13 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 256 seconds) |
| 22:45:40 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 268 seconds) |
| 22:45:45 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 22:46:31 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:46:46 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds) |
| 22:51:10 | → | waldo joins (~waldo@user/waldo) |
| 22:51:55 | → | sroso joins (~sroso@user/SrOso) |
| 22:52:22 | × | sroso quits (~sroso@user/SrOso) (Max SendQ exceeded) |
| 22:56:10 | → | phma_ joins (~phma@2001:5b0:210f:7f28:c0a7:813e:87a3:391e) |
| 22:56:38 | × | phma quits (phma@2001:5b0:2172:c758:72f8:9d6a:4a7b:7a0f) (Read error: Connection reset by peer) |
| 22:57:48 | × | waldo quits (~waldo@user/waldo) (Quit: waldo) |
| 22:58:02 | → | waldo joins (~waldo@user/waldo) |
| 22:58:10 | → | sroso joins (~sroso@user/SrOso) |
| 23:04:28 | → | y04nn joins (~username@2a03:1b20:8:f011::e10d) |
| 23:07:25 | × | zwrv quits (~yin@user/zero) (Ping timeout: 246 seconds) |
| 23:13:29 | × | ph88 quits (~ph88@91.64.63.48) (Remote host closed the connection) |
| 23:13:30 | × | chiselfu1e quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 23:14:17 | → | zwrv joins (~yin@user/zero) |
| 23:14:28 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 23:19:57 | × | peterbecich quits (~Thunderbi@47.229.123.186) (Ping timeout: 255 seconds) |
| 23:24:00 | × | mima quits (~mmh@aftr-62-216-211-51.dynamic.mnet-online.de) (Ping timeout: 255 seconds) |
| 23:40:11 | → | philopsos joins (~caecilius@user/philopsos) |
| 23:49:48 | × | trev quits (~trev@user/trev) (Ping timeout: 268 seconds) |
| 23:51:08 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:51:24 | → | trev joins (~trev@user/trev) |
| 23:55:40 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 23:58:00 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out) |
All times are in UTC on 2024-04-24.