2025-02-09 00:07:56 +0100 | <peutri> | tomsmeding: (followup) currently going with sizeOf (fix id :: a), which is somehow worse-than-partial yet doesn't warn |
2025-02-09 00:08:06 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) sixfourtwelve |
2025-02-09 00:08:38 +0100 | <monochrom> | Interesting. Did "undefined :: a" cause a warning? |
2025-02-09 00:08:44 +0100 | <peutri> | but is by far the minimal project disruption I found |
2025-02-09 00:08:57 +0100 | <peutri> | yes (because Relude) |
2025-02-09 00:09:15 +0100 | <monochrom> | God, totality police. |
2025-02-09 00:09:23 +0100 | <peutri> | ikr |
2025-02-09 00:09:35 +0100 | <monochrom> | May I be facetious and say "totalitarian" >:) |
2025-02-09 00:09:37 +0100 | <peutri> | and I'm voluntarily signing up for it |
2025-02-09 00:11:08 +0100 | <peutri> | I'm also noticing now `fix id` is shorter than `undefined`, and considering… mmmm… no, better forget that |
2025-02-09 00:11:26 +0100 | <monochrom> | @type fix fix |
2025-02-09 00:11:27 +0100 | <lambdabot> | error: |
2025-02-09 00:11:27 +0100 | <lambdabot> | • Occurs check: cannot construct the infinite type: a ~ a -> a |
2025-02-09 00:11:27 +0100 | <lambdabot> | Expected type: a -> a |
2025-02-09 00:12:17 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Ping timeout: 248 seconds) |
2025-02-09 00:12:38 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
2025-02-09 00:13:28 +0100 | <monochrom> | More fairly, on the scale of safety, static error message > runtime error message > no error message |
2025-02-09 00:14:14 +0100 | <monochrom> | So a warning system that simply pushes users away from runtime error (undefined) to no error (fix id) is... You know, the road to hell is paved with well intentions. |
2025-02-09 00:17:44 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 00:22:35 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
2025-02-09 00:28:24 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:2961:287b:51c1:b384) |
2025-02-09 00:29:12 +0100 | Catty | kitties |
2025-02-09 00:29:40 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) sixfourtwelve |
2025-02-09 00:30:58 +0100 | hiredman | (~hiredman@frontier1.downey.family) (Quit: Lost terminal) |
2025-02-09 00:31:34 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:2961:287b:51c1:b384) (Client Quit) |
2025-02-09 00:31:53 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:2961:287b:51c1:b384) |
2025-02-09 00:31:58 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:2961:287b:51c1:b384) (Remote host closed the connection) |
2025-02-09 00:33:58 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Ping timeout: 252 seconds) |
2025-02-09 00:38:33 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
2025-02-09 00:39:22 +0100 | <Leary> | If you don't care to heed a warning, you're supposed to ignore or disable it---it is just a /warning/, after all, not an error. Let's not blame x-partial for /wacky dodging/. |
2025-02-09 00:42:20 +0100 | hiredman | (~hiredman@frontier1.downey.family) hiredman |
2025-02-09 00:43:19 +0100 | <monochrom> | That would be a much better stance than mine, if not for the same totalitarian police also instituting "no warning by the time you commit" or even -Wall -Werror. |
2025-02-09 00:44:08 +0100 | <monochrom> | So it just means I should be complaining about the policing system rather than the warning system. |
2025-02-09 00:50:05 +0100 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 265 seconds) |
2025-02-09 00:51:34 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) sixfourtwelve |
2025-02-09 00:51:55 +0100 | philopsos | (~caecilius@user/philopsos) philopsos |
2025-02-09 00:56:45 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Ping timeout: 276 seconds) |
2025-02-09 00:57:15 +0100 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
2025-02-09 00:59:58 +0100 | <Leary> | Right. I actually understand if people with too much code to review want strict CI to make their life easier, but it should diff with a checked-in record of known/accepted warnings for flexibility. |
2025-02-09 01:06:02 +0100 | mesaoptimizer0 | (~mesaoptim@user/PapuaHardyNet) (Ping timeout: 265 seconds) |
2025-02-09 01:06:02 +0100 | jathan | (~jathan@69.61.93.38) (Ping timeout: 265 seconds) |
2025-02-09 01:06:09 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 01:10:28 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
2025-02-09 01:13:34 +0100 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 244 seconds) |
2025-02-09 01:16:53 +0100 | TMA | (tma@twin.jikos.cz) (Ping timeout: 248 seconds) |
2025-02-09 01:17:38 +0100 | mulk | (~mulk@pd95141d7.dip0.t-ipconnect.de) (Ping timeout: 265 seconds) |
2025-02-09 01:18:05 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
2025-02-09 01:18:07 +0100 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 265 seconds) |
2025-02-09 01:19:49 +0100 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
2025-02-09 01:20:09 +0100 | mulk | (~mulk@pd95141d7.dip0.t-ipconnect.de) mulk |
2025-02-09 01:20:15 +0100 | otbergsten | (~otbergste@user/otbergsten) () |
2025-02-09 01:20:20 +0100 | Maxdamantus | (~Maxdamant@user/maxdamantus) Maxdamantus |
2025-02-09 01:20:33 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 268 seconds) |
2025-02-09 01:21:15 +0100 | jathan | (~jathan@2607:1a00:0:19::2:1dc) jathan |
2025-02-09 01:25:14 +0100 | TMA | (tma@twin.jikos.cz) TMA |
2025-02-09 01:36:05 +0100 | zero | zwro |
2025-02-09 01:37:29 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
2025-02-09 01:40:00 +0100 | alx741 | (~alx741@186.33.188.229) |
2025-02-09 01:43:56 +0100 | yegorc | (~yegorc@user/yegorc) yegorc |
2025-02-09 01:44:24 +0100 | aaronv | (~aaronv@user/aaronv) aaronv |
2025-02-09 01:44:32 +0100 | Square2 | (~Square@user/square) Square |
2025-02-09 01:44:34 +0100 | Square3 | (~Square@user/square) Square |
2025-02-09 01:47:00 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds) |
2025-02-09 01:47:24 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
2025-02-09 01:47:53 +0100 | sprotte24 | (~sprotte24@p200300d16f1e3a00501959556750eb7a.dip0.t-ipconnect.de) (Quit: Leaving) |
2025-02-09 01:49:58 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) stiell |
2025-02-09 01:50:19 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
2025-02-09 01:50:19 +0100 | ljdarj1 | ljdarj |
2025-02-09 01:54:53 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 01:57:47 +0100 | migas97787 | (~migas@static.140.65.63.178.clients.your-server.de) migas |
2025-02-09 01:59:15 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) |
2025-02-09 01:59:16 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Client Quit) |
2025-02-09 01:59:24 +0100 | migas9778 | (~migas@static.140.65.63.178.clients.your-server.de) (Read error: Connection reset by peer) |
2025-02-09 01:59:24 +0100 | migas97787 | migas9778 |
2025-02-09 01:59:33 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) |
2025-02-09 01:59:41 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
2025-02-09 02:05:05 +0100 | alx741 | (~alx741@186.33.188.229) (Quit: alx741) |
2025-02-09 02:21:31 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Quit: leaving) |
2025-02-09 02:21:40 +0100 | Guest46 | (~Guest46@149.40.58.147) |
2025-02-09 02:25:03 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-02-09 02:25:18 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f0584678bbe6a824f58.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
2025-02-09 02:31:17 +0100 | Guest46 | (~Guest46@149.40.58.147) (Quit: Client closed) |
2025-02-09 02:35:28 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
2025-02-09 02:36:15 +0100 | califax | (~califax@user/califx) califx |
2025-02-09 02:43:37 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 02:43:59 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
2025-02-09 02:48:07 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
2025-02-09 03:14:18 +0100 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 252 seconds) |
2025-02-09 03:18:59 +0100 | Jeanne-Kamikaze | (~Jeanne-Ka@79.127.217.43) Jeanne-Kamikaze |
2025-02-09 03:23:35 +0100 | aaronv | (~aaronv@user/aaronv) aaronv |
2025-02-09 03:28:07 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-02-09 03:29:14 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
2025-02-09 03:32:00 +0100 | gmg | (~user@user/gehmehgeh) (Ping timeout: 264 seconds) |
2025-02-09 03:32:02 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 03:32:10 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
2025-02-09 03:36:50 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
2025-02-09 03:53:33 +0100 | tavare | (~tavare@150.129.88.189) |
2025-02-09 03:53:33 +0100 | tavare | (~tavare@150.129.88.189) (Changing host) |
2025-02-09 03:53:33 +0100 | tavare | (~tavare@user/tavare) tavare |
2025-02-09 04:05:04 +0100 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
2025-02-09 04:05:35 +0100 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
2025-02-09 04:20:26 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 04:23:03 +0100 | Jeanne-Kamikaze | (~Jeanne-Ka@79.127.217.43) (Quit: Leaving) |
2025-02-09 04:24:36 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 04:47:14 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-02-09 04:59:25 +0100 | jle` | (~jle`@2603:8001:3b02:84d4:6618:6c83:b259:edfc) (Ping timeout: 252 seconds) |
2025-02-09 05:02:18 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
2025-02-09 05:03:48 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
2025-02-09 05:04:31 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) (Ping timeout: 244 seconds) |
2025-02-09 05:08:19 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-02-09 05:08:50 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 05:13:54 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 272 seconds) |
2025-02-09 05:17:57 +0100 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 248 seconds) |
2025-02-09 05:22:21 +0100 | aaronv | (~aaronv@user/aaronv) aaronv |
2025-02-09 05:32:59 +0100 | jle` | (~jle`@syn-023-240-067-073.res.spectrum.com) jle` |
2025-02-09 05:34:54 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 05:35:53 +0100 | <tri> | hi, why is this not working please? |
2025-02-09 05:35:55 +0100 | <tri> | https://paste.tomsmeding.com/jV6JdsBd |
2025-02-09 05:36:48 +0100 | <tri> | it has something to do with 2 parameters passing into zip, but I can't really explain |
2025-02-09 05:39:51 +0100 | dtman34 | (~dtman34@c-75-72-179-251.hsd1.mn.comcast.net) dtman34 |
2025-02-09 05:43:45 +0100 | <tri> | seems like I can only compose 1 input function... |
2025-02-09 05:44:02 +0100 | <monochrom> | Do you accept: getTotalDistance xs ys = sum (zipWith (\(left, right) -> abs $ left -right) xs ys) |
2025-02-09 05:45:48 +0100 | <tri> | yea that works, I'm just trying to make it work using function composition. I forgot what concept force me to use 1 input function to compose, I have to look it up |
2025-02-09 05:47:13 +0100 | yegorc | (~yegorc@user/yegorc) (Quit: Leaving) |
2025-02-09 05:47:30 +0100 | <tri> | btw I've just come back to Haskell after a long break, and still seeing you here helping people out. Thank you |
2025-02-09 05:51:33 +0100 | encyde | (~ensyde@2601:5c6:c200:6dc0::16fe) |
2025-02-09 05:54:10 +0100 | aforemny_ | (~aforemny@2001:9e8:6cdf:f800:9bf4:7ea7:4c6a:c80f) aforemny |
2025-02-09 05:55:19 +0100 | aforemny | (~aforemny@2001:9e8:6cc0:9f00:f26a:4821:630d:3b0c) (Ping timeout: 260 seconds) |
2025-02-09 05:56:34 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 05:57:26 +0100 | <tri> | oh the (.) is actually a function, which takes two 1-input functions |
2025-02-09 05:57:46 +0100 | <tri> | so that's why zip was failing because it is a 2-input function |
2025-02-09 06:01:02 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 06:01:09 +0100 | <monochrom> | Now to probe the boundary of your understanding, "g xs ys = sum (zipWith f xs ys)" can still be simplified with (.), but only as: g xs = sum . zipWith f xs |
2025-02-09 06:06:27 +0100 | <tri> | hmm ok |
2025-02-09 06:07:41 +0100 | jle` | (~jle`@syn-023-240-067-073.res.spectrum.com) (Quit: WeeChat 4.5.1) |
2025-02-09 06:14:10 +0100 | jle` | (~jle`@2603:8001:3b00:11:8cd8:7ce2:93ee:a30) jle` |
2025-02-09 06:18:58 +0100 | Loshki | (~Loshki@c-98-42-126-198.hsd1.ca.comcast.net) |
2025-02-09 06:19:02 +0100 | Loshki | (~Loshki@c-98-42-126-198.hsd1.ca.comcast.net) (Leaving) |
2025-02-09 06:27:17 +0100 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) lisbeths |
2025-02-09 06:28:07 +0100 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
2025-02-09 06:34:52 +0100 | weary-traveler | (~user@user/user363627) user363627 |
2025-02-09 06:35:00 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
2025-02-09 06:41:06 +0100 | <tri> | https://paste.tomsmeding.com/XPlMpEUw |
2025-02-09 06:42:09 +0100 | <tri> | Cannot apply expression of type ‘m0 a0’ |
2025-02-09 06:42:09 +0100 | <tri> | to a visible type argument ‘[Int] |
2025-02-09 06:42:20 +0100 | <tri> | how could I fix this please? I don't understand the error message, especially m0 and a0 |
2025-02-09 06:42:32 +0100 | <c_wraith> | Add parens |
2025-02-09 06:42:36 +0100 | <c_wraith> | return (...) |
2025-02-09 06:42:47 +0100 | <int-e> | :t return read |
2025-02-09 06:42:48 +0100 | <lambdabot> | (Monad m, Read a) => m (String -> a) |
2025-02-09 06:43:01 +0100 | <int-e> | that's the m0 a0, more or less |
2025-02-09 06:43:18 +0100 | <int-e> | the "expression of type ‘m0 a0’" I mean |
2025-02-09 06:43:44 +0100 | <int-e> | you can drop the @[Int], but you still need parentheses |
2025-02-09 06:44:14 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
2025-02-09 06:44:21 +0100 | <int-e> | (the type will then be taken from the type signature or `readList`) |
2025-02-09 06:44:29 +0100 | <int-e> | s/or/of/ |
2025-02-09 06:44:38 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 06:45:36 +0100 | <int-e> | tri: keep in mind that in Haskell `return` is a function, not syntax. |
2025-02-09 06:46:09 +0100 | <monochrom> | Conversely, I see people writing in C "return(x+y)" all the time. :) |
2025-02-09 06:47:55 +0100 | <tri> | ah! thank you. It's been a long time since I last used Haskell :) |
2025-02-09 06:49:14 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
2025-02-09 06:56:45 +0100 | <ski> | @type readLn -- tri |
2025-02-09 06:56:45 +0100 | <lambdabot> | Read a => IO a |
2025-02-09 06:57:23 +0100 | <ski> | better to use that, rather than `getLine' & `read' |
2025-02-09 06:58:18 +0100 | <ski> | (if there's parse-error, that will raise the error while the action is executed, as opposed to when the result is forced) |
2025-02-09 07:01:12 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
2025-02-09 07:01:49 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
2025-02-09 07:06:39 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-02-09 07:08:29 +0100 | <tri> | thank you |
2025-02-09 07:13:17 +0100 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 268 seconds) |
2025-02-09 07:14:23 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 07:14:49 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
2025-02-09 07:14:49 +0100 | tnt2 | tnt1 |
2025-02-09 07:16:13 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2025-02-09 07:16:58 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
2025-02-09 07:18:08 +0100 | aaronv | (~aaronv@user/aaronv) aaronv |
2025-02-09 07:20:00 +0100 | Square2 | (~Square@user/square) (Quit: Leaving) |
2025-02-09 07:25:01 +0100 | Square3 | Square2 |
2025-02-09 07:27:44 +0100 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
2025-02-09 07:29:05 +0100 | img | (~img@user/img) img |
2025-02-09 07:29:22 +0100 | tri | (~tri@2601:182:780:720::55a0) (Remote host closed the connection) |
2025-02-09 07:32:43 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 07:34:02 +0100 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
2025-02-09 07:34:48 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
2025-02-09 07:35:21 +0100 | img | (~img@user/img) img |
2025-02-09 07:37:05 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 07:37:59 +0100 | forell | (~forell@user/forell) (Ping timeout: 260 seconds) |
2025-02-09 07:43:13 +0100 | jjhoo_ | (jahakala@user/jjhoo) (Remote host closed the connection) |
2025-02-09 07:44:35 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
2025-02-09 07:45:10 +0100 | causal | (~eric@50.35.84.231) causal |
2025-02-09 07:54:56 +0100 | causal | (~eric@50.35.84.231) (Quit: WeeChat 4.5.1) |
2025-02-09 07:55:09 +0100 | jjhoo | (jahakala@user/jjhoo) jjhoo |
2025-02-09 08:20:28 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 08:25:10 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 272 seconds) |
2025-02-09 08:43:07 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) |
2025-02-09 08:47:30 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) (Ping timeout: 252 seconds) |
2025-02-09 08:47:51 +0100 | r-sta | (~r-sta@sgyl-37-b2-v4wan-168528-cust2421.vm6.cable.virginm.net) |
2025-02-09 08:47:53 +0100 | <r-sta> | why dont we have numbers at type level? |
2025-02-09 08:48:27 +0100 | <r-sta> | is it because the class system does not work at type level? |
2025-02-09 08:48:35 +0100 | <r-sta> | can i use associated type families? |
2025-02-09 08:48:53 +0100 | <r-sta> | i should be able to have a binary encoding be just as good as Nats |
2025-02-09 08:49:19 +0100 | <r-sta> | esp because when its supposed to recurse over nat parametric instances... |
2025-02-09 08:49:25 +0100 | <r-sta> | and it has to prove constraints |
2025-02-09 08:49:51 +0100 | <r-sta> | its always saying things like "idk if 1+(x-1) = x" and stuff |
2025-02-09 08:50:40 +0100 | <r-sta> | maybe im being mistaken to think that an abstract representation for numbers would solve anything |
2025-02-09 08:51:13 +0100 | <r-sta> | infact, i always opt for the represtanttion that does basically tail recursion by being a piano natural |
2025-02-09 08:51:24 +0100 | r-sta | (~r-sta@sgyl-37-b2-v4wan-168528-cust2421.vm6.cable.virginm.net) (Client Quit) |
2025-02-09 09:00:00 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
2025-02-09 09:00:07 +0100 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: The Lounge - https://thelounge.chat) |
2025-02-09 09:00:58 +0100 | caconym | (~caconym@user/caconym) caconym |
2025-02-09 09:04:15 +0100 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) tt1231 |
2025-02-09 09:08:53 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 09:10:45 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f26657989b577b132fd.dip0.t-ipconnect.de) acidjnk |
2025-02-09 09:12:04 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
2025-02-09 09:12:39 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
2025-02-09 09:13:02 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
2025-02-09 09:14:31 +0100 | tabaqui1 | (~root@87.200.129.102) tabaqui |
2025-02-09 09:16:20 +0100 | kenran | (~kenran@user/kenran) kenran |
2025-02-09 09:26:13 +0100 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 245 seconds) |
2025-02-09 09:26:21 +0100 | monochrom | (trebla@216.138.220.146) (Quit: ZNC 1.9.1+deb1 - https://znc.in) |
2025-02-09 09:33:30 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 09:33:42 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
2025-02-09 09:33:42 +0100 | tnt2 | tnt1 |
2025-02-09 09:33:42 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
2025-02-09 09:35:45 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-02-09 09:37:53 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 245 seconds) |
2025-02-09 09:38:23 +0100 | monochrom | (trebla@216.138.220.146) |
2025-02-09 09:38:29 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 09:40:52 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2025-02-09 09:41:21 +0100 | euphores | (~SASL_euph@user/euphores) (Read error: Connection reset by peer) |
2025-02-09 09:41:26 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 09:42:48 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
2025-02-09 09:42:57 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
2025-02-09 09:42:58 +0100 | tnt2 | tnt1 |
2025-02-09 09:44:26 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
2025-02-09 09:46:57 +0100 | __monty__ | (~toonn@user/toonn) toonn |
2025-02-09 09:48:38 +0100 | <tomsmeding> | peutri: that's hilarious. |
2025-02-09 09:48:41 +0100 | kenran | (~kenran@user/kenran) (Ping timeout: 268 seconds) |
2025-02-09 09:48:59 +0100 | <tomsmeding> | you can even read it as "fix it" with a bit of imagination. |
2025-02-09 09:49:17 +0100 | <tomsmeding> | :t fix error |
2025-02-09 09:49:18 +0100 | <lambdabot> | [Char] |
2025-02-09 09:49:22 +0100 | <tomsmeding> | ah too bad |
2025-02-09 09:50:35 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
2025-02-09 09:53:13 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) |
2025-02-09 09:53:43 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
2025-02-09 09:55:41 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-02-09 09:56:37 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 10:00:50 +0100 | dsrt^ | (~dsrt@108.192.66.114) (Ping timeout: 252 seconds) |
2025-02-09 10:01:05 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
2025-02-09 10:01:34 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
2025-02-09 10:20:20 +0100 | <mauke> | fix id ~ undefined |
2025-02-09 10:20:38 +0100 | <mauke> | Void ~ newtype V = MkV V |
2025-02-09 10:24:15 +0100 | kenran | (~kenran@user/kenran) kenran |
2025-02-09 10:25:04 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 10:29:30 +0100 | tri | (~tri@2601:182:780:720::55a0) (Ping timeout: 246 seconds) |
2025-02-09 10:44:30 +0100 | dsrt^ | (~dsrt@108.192.66.114) |
2025-02-09 10:45:01 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 10:49:14 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 10:51:26 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
2025-02-09 10:52:12 +0100 | mniip_ | mniip |
2025-02-09 10:58:14 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-02-09 11:02:24 +0100 | otbergsten | (~otbergste@user/otbergsten) otbergsten |
2025-02-09 11:13:08 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
2025-02-09 11:13:09 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
2025-02-09 11:21:29 +0100 | Square2 | (~Square@user/square) (Remote host closed the connection) |
2025-02-09 11:23:07 +0100 | Square2 | (~Square@user/square) Square |
2025-02-09 11:27:36 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
2025-02-09 11:28:15 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 11:31:10 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:ab56:7ab1:bb07:5d4e) dhil |
2025-02-09 11:33:05 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 11:33:06 +0100 | tri | (~tri@2601:182:780:720::55a0) (Ping timeout: 276 seconds) |
2025-02-09 11:33:18 +0100 | misterfish | (~misterfis@84.53.85.146) misterfish |
2025-02-09 11:37:45 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
2025-02-09 11:43:44 +0100 | Square2 | (~Square@user/square) (Ping timeout: 260 seconds) |
2025-02-09 11:44:56 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
2025-02-09 11:56:37 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
2025-02-09 12:07:43 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:ab56:7ab1:bb07:5d4e) (Ping timeout: 265 seconds) |
2025-02-09 12:10:24 +0100 | sprotte24 | (~sprotte24@p200300d16f25850039a3b2714e26a8e3.dip0.t-ipconnect.de) |
2025-02-09 12:21:29 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 12:22:16 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) |
2025-02-09 12:25:41 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
2025-02-09 12:26:45 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) (Ping timeout: 248 seconds) |
2025-02-09 12:28:54 +0100 | ss4 | (~wootehfoo@user/wootehfoot) wootehfoot |
2025-02-09 12:29:28 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 12:34:19 +0100 | tri | (~tri@2601:182:780:720::55a0) (Ping timeout: 260 seconds) |
2025-02-09 12:43:00 +0100 | famubu | (~julinuser@14.139.174.50) |
2025-02-09 12:43:00 +0100 | famubu | (~julinuser@14.139.174.50) (Changing host) |
2025-02-09 12:43:00 +0100 | famubu | (~julinuser@user/famubu) famubu |
2025-02-09 12:43:49 +0100 | <famubu> | How can we get a function to decrement an integer like we can increment with `(+1)`? I tried `(-1)` but it is same as `-1`. |
2025-02-09 12:44:40 +0100 | <famubu> | `(-1) 4` doesn't decrement, but `(1-) 4` does. |
2025-02-09 12:45:36 +0100 | <tomsmeding> | :t subtract 1 |
2025-02-09 12:45:37 +0100 | <lambdabot> | Num a => a -> a |
2025-02-09 12:46:03 +0100 | <tomsmeding> | or set LexicalNegation and use (- 1) :p |
2025-02-09 12:46:29 +0100 | <tomsmeding> | famubu: ^ |
2025-02-09 12:51:30 +0100 | <mauke> | > map (\f -> f 4) [subtract 1, pred, (+(-1))] |
2025-02-09 12:51:31 +0100 | <lambdabot> | [3,3,3] |
2025-02-09 12:52:14 +0100 | <mauke> | > map (\f -> f 4) [subtract 1, pred, (+(-1)), flip (-) 1] |
2025-02-09 12:52:16 +0100 | <lambdabot> | [3,3,3,3] |
2025-02-09 12:53:00 +0100 | <tomsmeding> | mind that one of those is not like the others |
2025-02-09 12:53:13 +0100 | <mauke> | oh, it's about to get wrose |
2025-02-09 12:53:24 +0100 | <tomsmeding> | > map (\f -> f (minBound :: Int)) [subtract 1, (+(-1)), flip (-) 1, pred] |
2025-02-09 12:53:25 +0100 | <lambdabot> | [9223372036854775807,9223372036854775807,9223372036854775807,*Exception: Pre... |
2025-02-09 12:53:42 +0100 | <tomsmeding> | > succ (maxBound :: Int) -- similarly |
2025-02-09 12:53:43 +0100 | <lambdabot> | *Exception: Prelude.Enum.succ{Int}: tried to take `succ' of maxBound |
2025-02-09 12:54:12 +0100 | <mauke> | > map (\f -> f 4) [subtract 1, pred, (+(-1)), flip (-) 1, complement . negate] |
2025-02-09 12:54:14 +0100 | <lambdabot> | [3,3,3,3,3] |
2025-02-09 13:00:54 +0100 | mrmr155334346318 | (~mrmr@user/mrmr) (Quit: Bye, See ya later!) |
2025-02-09 13:02:15 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
2025-02-09 13:02:30 +0100 | <int-e> | :t (-1+) |
2025-02-09 13:02:30 +0100 | <lambdabot> | Num a => a -> a |
2025-02-09 13:02:57 +0100 | <tomsmeding> | wait why is that a thing without LexicalNegation |
2025-02-09 13:03:24 +0100 | <int-e> | I don't know. It's a thing that GHC and Hugs used to disagree on. Hugs wanted (+ -1) instead. |
2025-02-09 13:04:08 +0100 | <int-e> | the precedence of unary minus agrees with the default ones of - and + (what's that, 5? No, it's 6. |
2025-02-09 13:04:24 +0100 | bcksl | (~bcksl@user/bcksl) (Quit: \) |
2025-02-09 13:04:24 +0100 | end | (~end@user/end/x-0094621) (Quit: end) |
2025-02-09 13:09:06 +0100 | <mauke> | pickup_artist = complement . negate |
2025-02-09 13:09:53 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 13:09:58 +0100 | <tomsmeding> | map ($ 4) [complement <$> negate, complement <&> negate] |
2025-02-09 13:10:00 +0100 | <tomsmeding> | > map ($ 4) [complement <$> negate, complement <&> negate] |
2025-02-09 13:10:02 +0100 | <lambdabot> | [3,5] |
2025-02-09 13:12:18 +0100 | mrmr155334346318 | (~mrmr@user/mrmr) mrmr |
2025-02-09 13:13:25 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 268 seconds) |
2025-02-09 13:14:19 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
2025-02-09 13:14:34 +0100 | <int-e> | the mother of all bit hacks |
2025-02-09 13:17:43 +0100 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 252 seconds) |
2025-02-09 13:21:23 +0100 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
2025-02-09 13:22:23 +0100 | bcksl | (~bcksl@user/bcksl) bcksl |
2025-02-09 13:23:29 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) sixfourtwelve |
2025-02-09 13:23:38 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) |
2025-02-09 13:24:18 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2025-02-09 13:25:17 +0100 | Digitteknohippie | (~user@user/digit) Digit |
2025-02-09 13:25:48 +0100 | Digit | (~user@user/digit) (Ping timeout: 245 seconds) |
2025-02-09 13:32:24 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) (Ping timeout: 252 seconds) |
2025-02-09 13:32:41 +0100 | end | (~end@user/end/x-0094621) end^ |
2025-02-09 13:34:23 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) (Quit: No Ping reply in 180 seconds.) |
2025-02-09 13:35:14 +0100 | Guest75 | (~Guest63@2405:201:e02d:9053:c861:d50c:f158:db37) |
2025-02-09 13:35:33 +0100 | Guest75 | (~Guest63@2405:201:e02d:9053:c861:d50c:f158:db37) (Client Quit) |
2025-02-09 13:35:42 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) __ |
2025-02-09 13:37:14 +0100 | ash3en1 | (~Thunderbi@146.70.124.222) ash3en |
2025-02-09 13:37:47 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
2025-02-09 13:37:48 +0100 | ash3en1 | ash3en |
2025-02-09 13:40:58 +0100 | misterfish | (~misterfis@84.53.85.146) misterfish |
2025-02-09 13:47:05 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
2025-02-09 13:49:33 +0100 | kenran | (~kenran@user/kenran) (Remote host closed the connection) |
2025-02-09 13:51:16 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:e1f7:3d09:6349:4c17) dhil |
2025-02-09 13:54:10 +0100 | Square2 | (~Square@user/square) Square |
2025-02-09 13:59:57 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 14:00:54 +0100 | yegorc | (~yegorc@user/yegorc) yegorc |
2025-02-09 14:01:48 +0100 | xff0x_ | (~xff0x@2405:6580:b080:900:a75:2366:4e5c:4ce9) |
2025-02-09 14:02:45 +0100 | xff0x | (~xff0x@2405:6580:b080:900:a44a:d727:8d11:d274) (Ping timeout: 268 seconds) |
2025-02-09 14:04:03 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
2025-02-09 14:06:36 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:2b04:9d3:4ad9:6811) |
2025-02-09 14:07:38 +0100 | Digitteknohippie | Digit |
2025-02-09 14:07:39 +0100 | ash3en | (~Thunderbi@146.70.124.222) (Quit: ash3en) |
2025-02-09 14:10:32 +0100 | m5zs7k | (aquares@web10.mydevil.net) (Ping timeout: 252 seconds) |
2025-02-09 14:11:04 +0100 | ss4 | wootehfoot |
2025-02-09 14:13:04 +0100 | xff0x_ | xff0x |
2025-02-09 14:14:30 +0100 | euouae | (~euouae@user/euouae) euouae |
2025-02-09 14:14:47 +0100 | <euouae> | Does anyone else find lsp-haskell to be finicky on emacs? |
2025-02-09 14:15:31 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 14:15:57 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Quit: leaving) |
2025-02-09 14:16:01 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
2025-02-09 14:18:43 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 14:19:49 +0100 | tnt2 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
2025-02-09 14:23:14 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:2b04:9d3:4ad9:6811) (Quit: benjamin) |
2025-02-09 14:23:24 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:8b55:ff55:7658:babe) |
2025-02-09 14:28:29 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:8b55:ff55:7658:babe) (Quit: benjamin) |
2025-02-09 14:28:39 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:8b55:ff55:7658:babe) |
2025-02-09 14:30:46 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:8b55:ff55:7658:babe) (Client Quit) |
2025-02-09 14:30:54 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:8b55:ff55:7658:babe) |
2025-02-09 14:32:04 +0100 | m5zs7k | (aquares@web10.mydevil.net) m5zs7k |
2025-02-09 14:32:30 +0100 | ft | (~ft@p3e9bcd97.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
2025-02-09 14:33:51 +0100 | ft | (~ft@p4fc2a610.dip0.t-ipconnect.de) ft |
2025-02-09 14:34:31 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
2025-02-09 14:35:36 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:8b55:ff55:7658:babe) (Ping timeout: 265 seconds) |
2025-02-09 14:41:21 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:c43:857b:f09b:159d) |
2025-02-09 14:41:38 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 14:42:07 +0100 | JuanDaugherty | ColinRobinson |
2025-02-09 14:42:13 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
2025-02-09 14:42:13 +0100 | tnt2 | tnt1 |
2025-02-09 14:45:08 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 14:46:28 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
2025-02-09 14:48:21 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 14:48:43 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 14:50:03 +0100 | tnt2 | (~Thunderbi@user/tnt1) (Ping timeout: 276 seconds) |
2025-02-09 14:52:42 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 14:59:41 +0100 | benjamin | (~benjamin@2a03:4b80:a720:6e10:c43:857b:f09b:159d) (Quit: benjamin) |
2025-02-09 15:01:52 +0100 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 252 seconds) |
2025-02-09 15:04:04 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
2025-02-09 15:05:47 +0100 | igemnace | (~igemnace@user/igemnace) (Quit: ZNC 1.9.0+deb2build3 - https://znc.in) |
2025-02-09 15:08:07 +0100 | encyde | (~ensyde@2601:5c6:c200:6dc0::16fe) (Ping timeout: 268 seconds) |
2025-02-09 15:08:39 +0100 | igemnace | (~igemnace@user/igemnace) igemnace |
2025-02-09 15:10:57 +0100 | otbergsten | (~otbergste@user/otbergsten) (Remote host closed the connection) |
2025-02-09 15:11:04 +0100 | euouae | (~euouae@user/euouae) () |
2025-02-09 15:13:04 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 15:15:56 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
2025-02-09 15:17:16 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
2025-02-09 15:17:16 +0100 | tnt2 | tnt1 |
2025-02-09 15:17:34 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 15:21:07 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:e1f7:3d09:6349:4c17) (Ping timeout: 244 seconds) |
2025-02-09 15:21:57 +0100 | paul_j | (~user@8.190.187.81.in-addr.arpa) |
2025-02-09 15:22:19 +0100 | tri | (~tri@2601:182:780:720::55a0) (Ping timeout: 260 seconds) |
2025-02-09 15:22:52 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 15:23:04 +0100 | yegorc | (~yegorc@user/yegorc) (Quit: Leaving) |
2025-02-09 15:23:15 +0100 | <kaol> | > take 5 [1..5] :: [NominalDiffTime] |
2025-02-09 15:23:16 +0100 | <lambdabot> | error: |
2025-02-09 15:23:17 +0100 | <lambdabot> | Not in scope: type constructor or class ‘NominalDiffTime’ |
2025-02-09 15:23:30 +0100 | yegorc | (~yegorc@user/yegorc) yegorc |
2025-02-09 15:31:44 +0100 | tri | (~tri@2601:182:780:720::55a0) (Remote host closed the connection) |
2025-02-09 15:32:02 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) |
2025-02-09 15:37:05 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 15:40:06 +0100 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
2025-02-09 15:40:19 +0100 | todi | (~todi@p57803331.dip0.t-ipconnect.de) todi |
2025-02-09 15:40:23 +0100 | erdem | (~erdem@user/erdem) (Quit: ZNC 1.9.1 - https://znc.in) |
2025-02-09 15:42:02 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
2025-02-09 15:44:24 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
2025-02-09 16:03:05 +0100 | haritz | saimazoon |
2025-02-09 16:04:12 +0100 | paul_j | (~user@8.190.187.81.in-addr.arpa) (Read error: Connection reset by peer) |
2025-02-09 16:04:56 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
2025-02-09 16:07:06 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
2025-02-09 16:10:12 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) (Remote host closed the connection) |
2025-02-09 16:18:51 +0100 | piele | (~piele@eiseth.creativeserver.net) |
2025-02-09 16:21:56 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
2025-02-09 16:25:11 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 16:26:39 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-02-09 16:29:30 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 16:32:18 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
2025-02-09 16:33:03 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit) |
2025-02-09 16:49:07 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) |
2025-02-09 16:49:20 +0100 | erdem | (~erdem@user/erdem) erdem |
2025-02-09 16:54:08 +0100 | erdem | (~erdem@user/erdem) (WeeChat 3.8) |
2025-02-09 16:54:26 +0100 | kenran | (~kenran@user/kenran) kenran |
2025-02-09 16:56:19 +0100 | <EvanR> | % take 5 [1..5] :: [NominalDiffTime] |
2025-02-09 16:56:19 +0100 | <yahb2> | <interactive>:115:19: error: [GHC-76037] ; Not in scope: type constructor or class ‘NominalDiffTime’ |
2025-02-09 16:57:01 +0100 | <EvanR> | the bots inhabit a dimension without time like that entity at the end of dr strange |
2025-02-09 16:57:22 +0100 | tri | (~tri@c-73-186-227-171.hsd1.ct.comcast.net) (Ping timeout: 252 seconds) |
2025-02-09 16:59:26 +0100 | <ski> | % import Data.Time.Clock |
2025-02-09 16:59:26 +0100 | <yahb2> | <no output> |
2025-02-09 16:59:28 +0100 | <ski> | % take 5 [1..5] :: [NominalDiffTime] |
2025-02-09 16:59:28 +0100 | <yahb2> | [1s,1.000000000001s,1.000000000002s,1.000000000003s,1.000000000004s] |
2025-02-09 17:00:04 +0100 | ski | notes a bad `Show' instance |
2025-02-09 17:00:38 +0100 | <EvanR> | what the actual F though |
2025-02-09 17:00:56 +0100 | <EvanR> | NominalDiffTime is implemented as a Pico |
2025-02-09 17:01:03 +0100 | <ski> | % (read . show) (take 5 [1..5]) :: [NominalDiffTime] |
2025-02-09 17:01:03 +0100 | <yahb2> | *** Exception: Prelude.read: no parse |
2025-02-09 17:01:07 +0100 | <EvanR> | how did we get 1.0000000004 |
2025-02-09 17:01:27 +0100 | <EvanR> | oooh |
2025-02-09 17:01:44 +0100 | <EvanR> | wait |
2025-02-09 17:01:47 +0100 | <EvanR> | wtf |
2025-02-09 17:02:23 +0100 | <EvanR> | % take 5 (enumFrom [2..]) :: [NominalDiffTime] |
2025-02-09 17:02:23 +0100 | <yahb2> | <interactive>:129:18: error: [GHC-83865] ; • Couldn't match expected type ‘NominalDiffTime’ ; with actual type ‘[a0]’ ; • In the first argument of ‘enumFrom’, namely ‘[2 .... |
2025-02-09 17:02:35 +0100 | <EvanR> | % take 5 (enumFrom 2) :: [NominalDiffTime] |
2025-02-09 17:02:35 +0100 | <yahb2> | [2s,2.000000000001s,2.000000000002s,2.000000000003s,2.000000000004s] |
2025-02-09 17:03:06 +0100 | <EvanR> | I was so used to the Enum instance of floats |
2025-02-09 17:04:10 +0100 | <EvanR> | floats and NominalDiffTime are like bargin bin real numbers so I dunno if Enum makes sense |
2025-02-09 17:04:58 +0100 | j1n37- | (~j1n37@user/j1n37) j1n37 |
2025-02-09 17:05:48 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
2025-02-09 17:14:15 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 17:17:07 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 17:18:38 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 17:19:06 +0100 | manwithluck` | (~manwithlu@2a09:bac1:5be0:20::49:de) manwithluck |
2025-02-09 17:22:09 +0100 | manwithluck | (~manwithlu@194.177.28.164) (Ping timeout: 276 seconds) |
2025-02-09 17:24:49 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Ping timeout: 248 seconds) |
2025-02-09 17:34:46 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
2025-02-09 17:35:30 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
2025-02-09 17:36:55 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:6cf:adc3:4aba:323f) dhil |
2025-02-09 17:40:56 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) justsomeguy |
2025-02-09 17:41:36 +0100 | <justsomeguy> | What is lifting in functional programming? I've read a few definitions, but it doesn't make sense to me right now. |
2025-02-09 17:42:07 +0100 | <EvanR> | there's a few things referred to as lifting |
2025-02-09 17:42:33 +0100 | <EvanR> | unrelated things |
2025-02-09 17:43:16 +0100 | rvalue- | rvalue |
2025-02-09 17:43:47 +0100 | <EvanR> | any function of type A -> B can be lifted to a function on F a, where F is a Functor, using fmap |
2025-02-09 17:44:29 +0100 | <mauke> | lift0 :: a -> F a; lift1 :: (a -> b) -> (F a -> F b); lift2 :: (a -> b -> c) -> (F a -> F b -> F c) |
2025-02-09 17:44:39 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2025-02-09 17:44:50 +0100 | <EvanR> | any monadic action m a can be lifted to an action in t m a where t is monad transformer, with lift |
2025-02-09 17:44:51 +0100 | <ncf> | it's a terrible word used all over the place by people trying to sound mathy |
2025-02-09 17:45:17 +0100 | <EvanR> | a lifted type is an type with an additional semantics bottom |
2025-02-09 17:45:36 +0100 | <EvanR> | like Int has a bottom while Int# doesn't |
2025-02-09 17:46:01 +0100 | <mauke> | isn't that a boxed type? |
2025-02-09 17:46:05 +0100 | <monochrom> | Yeah, disregard the "intuitive" word "lifting". Learn each of Functor's fmap, Applicative's liftA2, MonadTrans's lift on its own terms. |
2025-02-09 17:46:08 +0100 | <EvanR> | it's also boxed |
2025-02-09 17:47:03 +0100 | <EvanR> | Only Int where data Only a = MkOnly a is lifted a second time |
2025-02-09 17:47:11 +0100 | <mauke> | and here I thought lifting and boxing made you sound jocky, not nerdy |
2025-02-09 17:47:12 +0100 | <monochrom> | In general, learn everything on its own terms, disregard "meaningful" names. |
2025-02-09 17:47:17 +0100 | <EvanR> | lol |
2025-02-09 17:47:41 +0100 | <monochrom> | GHC does the heavy-lifting. |
2025-02-09 17:48:06 +0100 | <monochrom> | GHC does the heavy-lifting, but you have to think outside the box. |
2025-02-09 17:48:42 +0100 | <EvanR> | RealWorld is deeply magical. It is primitive, but it is not unlifted. |
2025-02-09 17:49:45 +0100 | <monochrom> | lifted types have bottoms, boxed types take heap space. For example array types are unlifted but boxed. |
2025-02-09 17:50:33 +0100 | <monochrom> | But that's about the only exception to the lifted-boxed correlation. :) |
2025-02-09 17:50:44 +0100 | <mauke> | magical realism |
2025-02-09 17:50:57 +0100 | <EvanR> | RealWorld is "not unlifted" |
2025-02-09 17:51:10 +0100 | <EvanR> | smh so british |
2025-02-09 17:51:39 +0100 | <monochrom> | Speaking of which, "heap" is another great example of having multiple unrelated meanings. |
2025-02-09 17:53:03 +0100 | <mauke> | why do we have stacks and heaps, but no piles? |
2025-02-09 17:53:29 +0100 | <monochrom> | After a while you ought to realize that there are fewer "intuition"s than there are mutually unrelated concepts. That should inform you how "helpful" "intuition"s are. |
2025-02-09 17:53:39 +0100 | <EvanR> | https://en.wikipedia.org/wiki/Pile_(abstract_data_type) |
2025-02-09 17:54:01 +0100 | <monochrom> | https://www.smbc-comics.com/comic/precise |
2025-02-09 17:54:40 +0100 | <justsomeguy> | I'll admit that the only part of your explanation I understood was the first bit (a -> b) -> (f a -> f b), which can work on multiple arities of functions. |
2025-02-09 17:54:48 +0100 | tri | (~tri@2601:182:780:720::55a0) (Remote host closed the connection) |
2025-02-09 17:55:01 +0100 | <justsomeguy> | I haven't gotten to monad transformers yet, and don't really understand what an action is. |
2025-02-09 17:55:14 +0100 | <EvanR> | like, getChar :: IO Char |
2025-02-09 17:55:17 +0100 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2025-02-09 17:55:17 +0100 | <EvanR> | it's an IO action |
2025-02-09 17:55:27 +0100 | <mauke> | ignore things that don't make sense yet |
2025-02-09 17:56:14 +0100 | <monochrom> | Sure. Learn what you're ready to or interested in. Just disbelieve meaningful names and essay "explanation"s. |
2025-02-09 17:56:23 +0100 | <mauke> | but I'll mention that Functor provides (a -> b) -> (f a -> f b), and Applicative provides all other arities |
2025-02-09 17:56:29 +0100 | <mniip> | I like how "hence ptrArg" refers to nothing anymore |
2025-02-09 17:57:07 +0100 | <mauke> | :t pure |
2025-02-09 17:57:08 +0100 | <lambdabot> | Applicative f => a -> f a |
2025-02-09 17:57:12 +0100 | <mauke> | :t liftA2 |
2025-02-09 17:57:13 +0100 | <lambdabot> | Applicative f => (a -> b -> c) -> f a -> f b -> f c |
2025-02-09 17:59:32 +0100 | <EvanR> | then hoist had the decency to use a different word for something unrelated |
2025-02-09 18:02:16 +0100 | <mauke> | :t hoist lift |
2025-02-09 18:02:17 +0100 | <lambdabot> | error: |
2025-02-09 18:02:17 +0100 | <lambdabot> | Variable not in scope: hoist :: (m0 a0 -> t0 m0 a0) -> t |
2025-02-09 18:02:59 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 18:03:36 +0100 | <mauke> | EvanR: that wp article sucks |
2025-02-09 18:04:24 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
2025-02-09 18:05:00 +0100 | <haskellbridge> | <Bowuigi> The intuition for lift is mostly "put this thing inside this other thing that's higher up", where "thing", "higher up", "inside" and "put" are context specific. Usually liftings are sort of "free", as in, they don't add more properties than the ones implied by the other context |
2025-02-09 18:05:42 +0100 | <mauke> | "put this thing inside this other thing" => embed |
2025-02-09 18:07:05 +0100 | <justsomeguy> | An unwrapper wrapper function? |
2025-02-09 18:07:16 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
2025-02-09 18:09:13 +0100 | <haskellbridge> | <Bowuigi> It can sometimes wrap functions but it isn't a wrapper function |
2025-02-09 18:09:35 +0100 | <haskellbridge> | <Bowuigi> mauke the "higher up" is what turns embed into lift I guess |
2025-02-09 18:11:52 +0100 | <haskellbridge> | <Bowuigi> For example, liftFree lifts a Functor "f" into a Monad "Free f" |
2025-02-09 18:13:23 +0100 | <EvanR> | mauke, ikr |
2025-02-09 18:14:47 +0100 | <haskellbridge> | <Bowuigi> Usually "inverses" to lift, pure and embed are prefixed with run, un and lower, and folds and traversals with fold, traverse, elim, cata, mcata, for |
2025-02-09 18:15:29 +0100 | <haskellbridge> | <Bowuigi> Maps are usually prefixed with map or on |
2025-02-09 18:16:22 +0100 | aaronv | (~aaronv@user/aaronv) aaronv |
2025-02-09 18:16:27 +0100 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 248 seconds) |
2025-02-09 18:17:25 +0100 | <haskellbridge> | <Bowuigi> Which word to use depends on the context. Stuff that represents wrappers tends to use wrap/embed and un, stuff that represents computations pure and run, categorical stuff lift and lower, etc |
2025-02-09 18:21:05 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
2025-02-09 18:25:58 +0100 | kenran | (~kenran@user/kenran) (Remote host closed the connection) |
2025-02-09 18:32:01 +0100 | kenran | (~kenran@user/kenran) kenran |
2025-02-09 18:32:43 +0100 | gutszu | (~gutszu@187.85.204.144) (Quit: Client closed) |
2025-02-09 18:42:36 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 18:43:26 +0100 | tri | (~tri@2601:182:780:720::55a0) (Remote host closed the connection) |
2025-02-09 18:43:38 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 18:50:44 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:6cf:adc3:4aba:323f) (Ping timeout: 268 seconds) |
2025-02-09 18:51:44 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 18:54:06 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
2025-02-09 18:56:09 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 19:02:36 +0100 | AkechiShiro | (~licht@user/akechishiro) (Ping timeout: 246 seconds) |
2025-02-09 19:02:56 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 272 seconds) |
2025-02-09 19:04:46 +0100 | AkechiShiro | (~licht@user/akechishiro) AkechiShiro |
2025-02-09 19:05:05 +0100 | <tri> | https://paste.tomsmeding.com/kY0jmKNs |
2025-02-09 19:05:33 +0100 | <tri> | I would like to keep the type variable a instead of changing it to a concrete type like Int, which will be compilable |
2025-02-09 19:05:55 +0100 | <tomsmeding> | :t read |
2025-02-09 19:05:56 +0100 | <lambdabot> | Read a => String -> a |
2025-02-09 19:06:11 +0100 | <tomsmeding> | tri: mind that `Read a` constraint |
2025-02-09 19:06:11 +0100 | <tri> | I *understand* that keeping just at a will not compile, because read will not know what to parse to |
2025-02-09 19:06:12 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) Raito_Bezarius |
2025-02-09 19:06:19 +0100 | <tomsmeding> | no, that's not the problem |
2025-02-09 19:06:29 +0100 | <tomsmeding> | `read` knows damn well what to parse to: it's `a` |
2025-02-09 19:06:34 +0100 | <tomsmeding> | it just doesn't know _how_ |
2025-02-09 19:06:42 +0100 | <tomsmeding> | the `Read a` constraint contains information that tells it how |
2025-02-09 19:06:55 +0100 | <tri> | yea Tom, so I tried to use the type Num a => String -> IO a, in hope that read can parse to a Num |
2025-02-09 19:06:57 +0100 | <tri> | but it still fail |
2025-02-09 19:07:09 +0100 | <tomsmeding> | try Read a instead of Num a ;) |
2025-02-09 19:07:17 +0100 | <tomsmeding> | Num and Read are unrelated |
2025-02-09 19:07:38 +0100 | <tri> | ah ok let me read it a bit more to understand |
2025-02-09 19:07:40 +0100 | <tri> | thank you |
2025-02-09 19:07:47 +0100 | yegorc | (~yegorc@user/yegorc) (Leaving) |
2025-02-09 19:08:05 +0100 | <tomsmeding> | `Num` tells you how (+), (-), (*), negate, abas, signum and fromInteger are defined |
2025-02-09 19:08:23 +0100 | <tomsmeding> | there's also, of course, a bunch more functions that can work using just those few, and those work on any Num type too |
2025-02-09 19:08:40 +0100 | <tomsmeding> | `Read` tells you how `read` is defined, essentially |
2025-02-09 19:09:01 +0100 | <tomsmeding> | tri: in fact, at runtime, that `Read a` constraint on your function becomes an actual function _argument_ |
2025-02-09 19:09:28 +0100 | <tomsmeding> | at runtime, it's a record with a few fields, one for each method in the type class |
2025-02-09 19:09:43 +0100 | <tomsmeding> | so if you have `myFoo :: Num a => a -> a -> a`, then myFoo takes _three_ arguments at runtime |
2025-02-09 19:10:07 +0100 | <tomsmeding> | and the first one of those contains 7 values: the definition of (+) for `a`, the definition of (-) for `a`, ..., the definition of `fromInteger` for `a` |
2025-02-09 19:10:19 +0100 | <tomsmeding> | `Read a` gives you the definition of `read` for `a`. :) |
2025-02-09 19:10:43 +0100 | <tomsmeding> | (Actually it gives you the definition of `readsPrec`, and `read` is implemented in terms of `readsPrec`. But that's mostly beside the point.) |
2025-02-09 19:10:53 +0100 | <tri> | thank you |
2025-02-09 19:11:00 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Max SendQ exceeded) |
2025-02-09 19:11:07 +0100 | tri | (~tri@2601:182:780:720::55a0) (Remote host closed the connection) |
2025-02-09 19:11:34 +0100 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 260 seconds) |
2025-02-09 19:11:35 +0100 | <haskellbridge> | <Bowuigi> Oh, this is a case where you learn more about a concepts when you understand how it is compiled |
2025-02-09 19:11:59 +0100 | <tomsmeding> | some people may disagree, but I think so |
2025-02-09 19:12:02 +0100 | <tomsmeding> | in this case |
2025-02-09 19:12:15 +0100 | <tomsmeding> | you can specify how type classes work just fine without talking about how they're compiled |
2025-02-09 19:12:51 +0100 | <tomsmeding> | but then it becomes an abstract, rather algebraic specification that only people who are already familiar with PL concepts will be able to work with |
2025-02-09 19:13:31 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
2025-02-09 19:14:14 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) Raito_Bezarius |
2025-02-09 19:18:22 +0100 | <monochrom> | I use algebra because everyone has acquired algebra skills. |
2025-02-09 19:18:47 +0100 | <monochrom> | from public mandatory education |
2025-02-09 19:20:03 +0100 | <tomsmeding> | I'm not talking about high-school algebra, I'm talking about abstract algebra that one learns either in an advanced FP / introductory PL course, or in a maths bachelor :p |
2025-02-09 19:20:24 +0100 | <monochrom> | Yeah I don't use that on other people. Don't worry! |
2025-02-09 19:20:57 +0100 | <tomsmeding> | if someone comes here with a question of what constraint to put on their function to make `read` work, I'm not going to assume they understand abstract algebra |
2025-02-09 19:21:15 +0100 | <tomsmeding> | if they had that kind of mental pathways already developed, they would have intuited the answer already ;) |
2025-02-09 19:23:52 +0100 | <monochrom> | This is how I teach classes and what the constraints are doing there: https://www.cs.utoronto.ca/~trebla/CSCC24-2024-Summer/04-haskell-types-2.html |
2025-02-09 19:24:15 +0100 | Square2 | (~Square@user/square) (Ping timeout: 244 seconds) |
2025-02-09 19:26:11 +0100 | <monochrom> | It does not use advanced math, but it does not use dictionaries either. For C++ compiler has already proved that there is another way. |
2025-02-09 19:27:06 +0100 | <monochrom> | (Meanwhile, people complain that GHC exes are already too big haha) |
2025-02-09 19:28:56 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
2025-02-09 19:29:49 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
2025-02-09 19:30:26 +0100 | Lord_of_Life_ | Lord_of_Life |
2025-02-09 19:31:08 +0100 | <tomsmeding> | monochrom: nice, I like |
2025-02-09 19:31:26 +0100 | <tomsmeding> | now I just have to remember where this lives when someone asks about type classes |
2025-02-09 19:32:08 +0100 | <monochrom> | It disappears soon. Namely, the "2024" part in the URL keeps changing, for obvious reasons. |
2025-02-09 19:32:42 +0100 | <monochrom> | Hrm I could easily make a "latest" alias! |
2025-02-09 19:32:48 +0100 | <tomsmeding> | 2023 is still up, it looks like |
2025-02-09 19:33:11 +0100 | <monochrom> | Ah I forgot to delete that haha |
2025-02-09 19:33:30 +0100 | <monochrom> | Usually in year N I keep both N and N-1. |
2025-02-09 19:33:58 +0100 | <tomsmeding> | given that not all directories are readable I assume you're aware that requesting /~trebla/ just gives a listing :) |
2025-02-09 19:34:24 +0100 | <tomsmeding> | but this will make it easier to find this stuff if I even remember to look for it, thanks |
2025-02-09 19:37:08 +0100 | <monochrom> | Yeah I am too lazy to make index.html so I just enable "just list everything" |
2025-02-09 19:37:48 +0100 | <tomsmeding> | when people do put an index.html in, they often forget to remove stuff from the directory that shouldn't be public any more in the first place |
2025-02-09 19:38:08 +0100 | <tomsmeding> | and then while they're kind of hidden then, they're still available if you know the URL |
2025-02-09 19:38:16 +0100 | <monochrom> | OK https://www.cs.utoronto.ca/~trebla/CSCC24-latest/ should be pretty reliable now! |
2025-02-09 19:38:27 +0100 | <tomsmeding> | sweet! |
2025-02-09 19:39:48 +0100 | <monochrom> | I wonder whether they forget or they simply have the wrong mental model. |
2025-02-09 19:40:07 +0100 | <tomsmeding> | probably first the latter, then later the former |
2025-02-09 19:40:47 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-02-09 19:41:53 +0100 | tri | (~tri@2601:182:780:720::55a0) |
2025-02-09 19:47:06 +0100 | tri | (~tri@2601:182:780:720::55a0) (Ping timeout: 276 seconds) |
2025-02-09 19:54:15 +0100 | aaronv | (~aaronv@user/aaronv) aaronv |
2025-02-09 19:58:29 +0100 | kenran | (~kenran@user/kenran) (Remote host closed the connection) |
2025-02-09 19:59:49 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 20:04:00 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 20:04:10 +0100 | aaronv | (~aaronv@user/aaronv) (Remote host closed the connection) |
2025-02-09 20:04:33 +0100 | Googulator | (~Googulato@2a01-036d-0106-4074-758c-12a1-cbb4-05eb.pool6.digikabel.hu) (Quit: Client closed) |
2025-02-09 20:04:49 +0100 | Googulator | (~Googulato@2a01-036d-0106-4074-758c-12a1-cbb4-05eb.pool6.digikabel.hu) |
2025-02-09 20:08:59 +0100 | yegorc | (~yegorc@user/yegorc) yegorc |
2025-02-09 20:09:51 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
2025-02-09 20:11:03 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
2025-02-09 20:12:18 +0100 | misterfish | (~misterfis@84.53.85.146) misterfish |
2025-02-09 20:12:54 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-02-09 20:19:24 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
2025-02-09 20:25:26 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
2025-02-09 20:27:22 +0100 | Anushka | (~Anushka@101.0.63.173) |
2025-02-09 20:27:29 +0100 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 265 seconds) |
2025-02-09 20:28:20 +0100 | Anushka | (~Anushka@101.0.63.173) (Client Quit) |
2025-02-09 20:28:59 +0100 | misterfish | (~misterfis@84.53.85.146) misterfish |
2025-02-09 20:29:22 +0100 | weary-traveler | (~user@user/user363627) user363627 |
2025-02-09 20:31:28 +0100 | yegorc | (~yegorc@user/yegorc) (Leaving) |
2025-02-09 20:36:35 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
2025-02-09 20:39:15 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
2025-02-09 20:42:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
2025-02-09 20:44:17 +0100 | lunitur | (~halloy485@2a00:1bb8:11c:a9a5:5d31:a95b:66b2:d7f4) |
2025-02-09 20:46:13 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
2025-02-09 20:49:34 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 20:51:06 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f26657989b577b132fd.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
2025-02-09 20:53:52 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 20:54:38 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
2025-02-09 20:55:02 +0100 | <EvanR> | :t negate . read |
2025-02-09 20:55:04 +0100 | <lambdabot> | (Num c, Read c) => String -> c |
2025-02-09 20:55:36 +0100 | <EvanR> | parses into a Num insofar as that makes any sense |
2025-02-09 20:56:20 +0100 | <EvanR> | not sure what happened to 'a' and 'b' there xD |
2025-02-09 20:57:42 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:d34b:be83:5f4c:606f) dhil |
2025-02-09 21:00:04 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
2025-02-09 21:00:42 +0100 | caconym | (~caconym@user/caconym) caconym |
2025-02-09 21:03:19 +0100 | michalz | (~michalz@185.246.207.203) |
2025-02-09 21:05:10 +0100 | dhil | (~dhil@2a0c:b381:5bf:3500:d34b:be83:5f4c:606f) (Ping timeout: 268 seconds) |
2025-02-09 21:09:38 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
2025-02-09 21:11:29 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
2025-02-09 21:12:46 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
2025-02-09 21:14:04 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
2025-02-09 21:15:06 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Client Quit) |
2025-02-09 21:16:49 +0100 | <lunitur> | Hi guys, I was thinking about making a GHC plugin for synthatic sugar that would make handling of monadic expressions easier, like !-notation or Monadic comprehensions in Idris. I would greatly appreciate if I could get some pointers. |
2025-02-09 21:16:53 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Ping timeout: 244 seconds) |
2025-02-09 21:18:03 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
2025-02-09 21:18:33 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
2025-02-09 21:19:37 +0100 | weary-traveler | (~user@user/user363627) user363627 |
2025-02-09 21:20:41 +0100 | otbergsten | (~otbergste@user/otbergsten) otbergsten |
2025-02-09 21:21:20 +0100 | Guest0 | (~Guest0@101.0.63.173) |
2025-02-09 21:21:28 +0100 | Guest0 | (~Guest0@101.0.63.173) (Client Quit) |
2025-02-09 21:21:37 +0100 | pavonia | (~user@user/siracusa) siracusa |
2025-02-09 21:24:21 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Ping timeout: 248 seconds) |
2025-02-09 21:25:00 +0100 | zaz | (~zaz@cmbg-18-b2-v4wan-168328-cust3861.vm17.cable.virginm.net) |
2025-02-09 21:25:31 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
2025-02-09 21:26:26 +0100 | zaz | Zaz_ |
2025-02-09 21:27:15 +0100 | <EvanR> | it's funny that in web world they want you to not do that and put individual side effecting code on its own line and store the result to a temporary |
2025-02-09 21:27:59 +0100 | <EvanR> | instead of making a more complex expression with multiple side effects |
2025-02-09 21:28:12 +0100 | <EvanR> | maybe they are just cargo culting haskell though |
2025-02-09 21:30:48 +0100 | Guest0 | (~Guest0@101.0.63.173) |
2025-02-09 21:31:07 +0100 | Guest0 | (~Guest0@101.0.63.173) (Client Quit) |
2025-02-09 21:34:33 +0100 | <geekosaur> | you might want to read https://www.reddit.com/r/haskell/comments/106opzn/ann_monadic_bang_a_plugin_for_more_concise/ |
2025-02-09 21:35:19 +0100 | <geekosaur> | also I've seen a discussion somewhere pitching something similar and a number of responses asking about various corner cases that come up in Haskell |
2025-02-09 21:35:46 +0100 | <geekosaur> | (I thought there was a ghc proposal at one point but I can't find it) |
2025-02-09 21:37:38 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 21:38:18 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
2025-02-09 21:41:54 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 21:44:45 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Ping timeout: 252 seconds) |
2025-02-09 21:46:35 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
2025-02-09 21:47:02 +0100 | talismanick | (~user@2601:644:937c:ed10::ae5) talismanick |
2025-02-09 21:51:48 +0100 | zfnmxt | (~zfnmxt@user/zfnmxt) zfnmxt |
2025-02-09 21:52:04 +0100 | <talismanick> | for `newtype RMonoid m = RMonoid (Monoid m => m -> m)`, is there a way to communicate the constraint when writing a Functor instance? |
2025-02-09 21:52:51 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
2025-02-09 21:53:20 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
2025-02-09 21:54:13 +0100 | prasad | (~Thunderbi@2601:243:c001:3f07::d1) |
2025-02-09 21:54:40 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
2025-02-09 21:55:15 +0100 | <lunitur> | thanks, i'm happy to see this exists but kinda bummed out because i really wanted to do some ghc related project |
2025-02-09 21:57:44 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 272 seconds) |
2025-02-09 21:59:50 +0100 | zaz | (~zaz@109.224.141.163) |
2025-02-09 22:01:15 +0100 | <ncf> | talismanick: what do you mean? that's not functorial in m |
2025-02-09 22:01:40 +0100 | Zaz_ | (~zaz@cmbg-18-b2-v4wan-168328-cust3861.vm17.cable.virginm.net) (Ping timeout: 240 seconds) |
2025-02-09 22:03:49 +0100 | <talismanick> | wait, you're right |
2025-02-09 22:03:56 +0100 | <talismanick> | what was I thinking? |
2025-02-09 22:04:35 +0100 | <ncf> | i don't know! |
2025-02-09 22:04:43 +0100 | <ncf> | forall m. RMonoid m is isomorphic to ℕ though |
2025-02-09 22:05:02 +0100 | <ncf> | (unrelatedly) |
2025-02-09 22:05:45 +0100 | <talismanick> | oh right, I was trying to write down a general rule for difference list style optimizations |
2025-02-09 22:06:17 +0100 | <talismanick> | (I just came back to this code after months and saw a halfwritten Functor instance with a type error) |
2025-02-09 22:06:41 +0100 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!) |
2025-02-09 22:07:13 +0100 | <talismanick> | maybe isomorphism to the naturals is part of what I was missing... |
2025-02-09 22:07:23 +0100 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan |
2025-02-09 22:13:00 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
2025-02-09 22:16:08 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
2025-02-09 22:17:39 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
2025-02-09 22:18:12 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Ping timeout: 252 seconds) |
2025-02-09 22:20:00 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
2025-02-09 22:20:34 +0100 | <zaz> | Hello! I'm interested in doing a deep dive over the coming months on bijective programming and in particular bijective parsing. I've skimmed a bunch of academic papers and am planning on learning more category theory, but what's the best way to get my hands dirty playing around with these ideas? Are there any bijective libraries out there that are |
2025-02-09 22:20:34 +0100 | <zaz> | relatively beginner-friendly? |
2025-02-09 22:20:35 +0100 | <zaz> | Also, why is bijectivity not built in? For example, why is there no way to do `invert(span isLower)`? It would seem like a really handy feature that if you compose a function out of a bunch of bijective functions that you could automatically invert it. |
2025-02-09 22:21:15 +0100 | <tomsmeding> | talismanick: the typical generalisation of difference lists is simply Endo |
2025-02-09 22:21:22 +0100 | <tomsmeding> | also known as Cayley transform |
2025-02-09 22:21:30 +0100 | <tomsmeding> | (when done to a monoid) |
2025-02-09 22:24:56 +0100 | <tomsmeding> | zaz: I can only reply to your last point (y no builtin), I'll leave the rest to others: there are very few expressions in practical code that are, in fact, bijective -- and if they are, then their subexpressions often are not. Indeed, `span` is not bijective, but `span isLower` suddenly is. `a * b` is not bijective, but `(a, a * b)` suddenly is. It would be a feature with rather significant (and |
2025-02-09 22:24:58 +0100 | <tomsmeding> | research-y!) implementation effort in GHC, with only very limited practical application |
2025-02-09 22:26:29 +0100 | <ncf> | span isLower is not bijective (it just has a left inverse) |
2025-02-09 22:27:28 +0100 | <talismanick> | tomsmeding: yes, what I had in mind was "automating" the Endo optimization |
2025-02-09 22:27:42 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 22:27:45 +0100 | <ncf> | anyway if you're willing to ignore that and work with lenses you could have span :: (a → Bool) → Iso [a] ([a], [a]) |
2025-02-09 22:29:54 +0100 | sp1ff | (~user@c-67-160-173-55.hsd1.wa.comcast.net) (Ping timeout: 248 seconds) |
2025-02-09 22:30:01 +0100 | <talismanick> | because you, the programmer, know `((([] ++ [a]) ++ [b]) ++ [c]) ++ [d]` is quadratic and `[a] ++ ([b] ++ ([c] ++ ([d] ++ [])))` is linear by inspection of `(++)`'s definition (traverse LHS to end, set its pointer to RHS's head) |
2025-02-09 22:31:29 +0100 | michalz | (~michalz@185.246.207.203) (Remote host closed the connection) |
2025-02-09 22:32:07 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
2025-02-09 22:32:32 +0100 | <talismanick> | which seems like something that could be automated "by hypothesis" (symbolic substitution by expanding definitions) because associativity guarantees safe local rearrangement (no sudden nontermination, etc) |
2025-02-09 22:33:19 +0100 | <talismanick> | except there's arbitrary parenthetical lookahead, and iso to ℕ means it's additionally streamlike |
2025-02-09 22:33:47 +0100 | <tomsmeding> | talismanick: automatic in what way? A compiler optimisation or a compiler plugin? Or something else? |
2025-02-09 22:33:56 +0100 | <talismanick> | compiler optimization |
2025-02-09 22:34:06 +0100 | <tomsmeding> | GHC doesn't know that (++) is associative |
2025-02-09 22:34:58 +0100 | <talismanick> | is it not allowed to assume associativity when told `[a]` has a Semigroup instance? |
2025-02-09 22:35:25 +0100 | <tomsmeding> | no, typeclass laws are not actually laws in haskell, you're allowed (by the language semantics) to break them |
2025-02-09 22:35:34 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f26c4dbaee3a15423f1.dip0.t-ipconnect.de) acidjnk |
2025-02-09 22:35:36 +0100 | <tomsmeding> | you're quite _expected_ not to |
2025-02-09 22:36:04 +0100 | <talismanick> | no fun allowed :( |
2025-02-09 22:36:28 +0100 | <tomsmeding> | usual caveat for built-in classes like WithDict that have GHC magic associated to them, where if you break the preconditions in the documentation you get nasal demons |
2025-02-09 22:36:55 +0100 | <tomsmeding> | or perhaps the new WithDict is safer than what was there before, I don't recall precisely |
2025-02-09 22:37:14 +0100 | <talismanick> | what if I /want/ -O3 to summon nasal demons? all those back and forths on C2 about a sufficiently smart compiler - I want to see what it can do lol |
2025-02-09 22:37:39 +0100 | <tomsmeding> | fork microHs? :p |
2025-02-09 22:37:45 +0100 | <monochrom> | Just hire a grad student. |
2025-02-09 22:37:46 +0100 | <tomsmeding> | or ghc if you dare |
2025-02-09 22:37:56 +0100 | <tomsmeding> | that costs money (usually) |
2025-02-09 22:38:04 +0100 | <tomsmeding> | not very much in some countries |
2025-02-09 22:38:16 +0100 | <monochrom> | Yeah but cheaper than industry :) |
2025-02-09 22:38:39 +0100 | <monochrom> | in some cases one slice of cheap pizza is all you need |
2025-02-09 22:39:00 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
2025-02-09 22:39:10 +0100 | zaz | (~zaz@109.224.141.163) (Ping timeout: 240 seconds) |
2025-02-09 22:39:27 +0100 | tomsmeding | . o O ( -ffast-math ) |
2025-02-09 22:39:34 +0100 | <monochrom> | :) |
2025-02-09 22:44:27 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Ping timeout: 268 seconds) |
2025-02-09 22:45:19 +0100 | <haskellbridge> | <Bowuigi> talismanick look into the Cayley monoid |
2025-02-09 22:45:44 +0100 | <haskellbridge> | <Bowuigi> More generally, the Cayley theorem, but that's a categorical thing |
2025-02-09 22:49:10 +0100 | <haskellbridge> | <Bowuigi> You can just define "lit = (<>)", "render m = m mempty", note that functions that directly act on the monoid are also allowed, so on strings you can do "tail . lit "a" . lit "b"" to get "lit "b"" |
2025-02-09 22:49:32 +0100 | <tomsmeding> | https://en.wikipedia.org/wiki/Transformation_semigroup |
2025-02-09 22:49:49 +0100 | <tomsmeding> | that's what wikipedia calls it, apparently |
2025-02-09 22:50:33 +0100 | <tomsmeding> | (it even mentions difference lists) |
2025-02-09 22:51:35 +0100 | <haskellbridge> | <Bowuigi> I also like to define "litC = (:)" for strings. Note that "tail . litC x = id" (mempty on the Cayley monoids) |
2025-02-09 22:54:24 +0100 | <haskellbridge> | <Bowuigi> I call it the Cayley monoid (technically "Cayley monoid of a monoid M", or just "Cayley monoid of M") because of that one theorem |
2025-02-09 22:54:50 +0100 | <talismanick> | yes, I was thinking about how best to automate that process |
2025-02-09 22:55:27 +0100 | <haskellbridge> | <Bowuigi> Just use the definitions above, doesn't require wrappers or anything like that |
2025-02-09 22:56:03 +0100 | <tomsmeding> | it's tricky, because rendering is not O(1), so if you render, you want to continue computation with the rendered value, not the composition you had before |
2025-02-09 22:56:38 +0100 | <tomsmeding> | i.e. if you `let x = lit "abc" . lit "def" . lit "ghi" in f (render x) (render x)` then you're doing work twice |
2025-02-09 22:56:55 +0100 | <haskellbridge> | <Bowuigi> Yeah, tho I'd recommend not rendering unless absolutely necessary |
2025-02-09 22:57:06 +0100 | <tomsmeding> | right, but you're going to auto-transform, you'll have to render sometimes |
2025-02-09 22:57:26 +0100 | <haskellbridge> | <Bowuigi> You can modify the composition directly, as I've shown before |
2025-02-09 22:57:52 +0100 | <tomsmeding> | talismanick: also this is only beneficial for monoids where the wrong associativity is actually slow; doing Cayley to `Sum Int` will only make everything slow |
2025-02-09 22:58:20 +0100 | <tomsmeding> | Bowuigi: what if the original program passed the String to `putStrLn`? You'll have to render it at that point. |
2025-02-09 22:58:22 +0100 | <haskellbridge> | <Bowuigi> Indeed, the same can be said for the other Cayley transformations |
2025-02-09 22:59:04 +0100 | <tomsmeding> | or what if the original program put the String in a `case`? Can't evaluate that `case` without rendering |
2025-02-09 23:00:56 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
2025-02-09 23:00:57 +0100 | <haskellbridge> | <Bowuigi> The case can be incorporated into the pipeline by just composing that function with the unrendered value in most cases. As for IO, that's what I mean by "absolutely necessary" |
2025-02-09 23:01:43 +0100 | <tomsmeding> | depends on what exactly is returned from the `case`, but yes, sometimes that works |
2025-02-09 23:01:50 +0100 | <haskellbridge> | <Bowuigi> Obviously this means that rendering is no longer O(n) but it allows you to keep adding stuff to the monoid afterwards |
2025-02-09 23:03:00 +0100 | <haskellbridge> | <Bowuigi> And if the entire pipeline is exposed to GHC, it can do its magic, as usual |
2025-02-09 23:03:41 +0100 | <tomsmeding> | you also have to render whenever the original program _shares_ a monoid value: with `let x = ... ; f y = y ++ y in putStrLn (f x x)`, if you don't take care, you're going to compute x twice (whereas this program as written only computes x once) |
2025-02-09 23:04:19 +0100 | <tomsmeding> | anyway we're doing talismanick's grad student's research for them :) |
2025-02-09 23:04:50 +0100 | <haskellbridge> | <Bowuigi> True lol |
2025-02-09 23:05:14 +0100 | <haskellbridge> | <Bowuigi> Gotta continue with my not-grad-student research then lol |
2025-02-09 23:07:58 +0100 | tabaqui1 | (~root@87.200.129.102) (Ping timeout: 244 seconds) |
2025-02-09 23:21:06 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
2025-02-09 23:25:18 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
2025-02-09 23:38:01 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
2025-02-09 23:39:36 +0100 | <haskellbridge> | <Bowuigi> Related, which syntax for visible and invisible foralls is preferred nowadays? |
2025-02-09 23:39:58 +0100 | <haskellbridge> | <Bowuigi> In general I mean, not just in Haskell |
2025-02-09 23:42:26 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) (Ping timeout: 248 seconds) |
2025-02-09 23:46:00 +0100 | <haskellbridge> | <Bowuigi> Currently I have "func : {a b : *} (f : * -> *) a -> f b = ...", where a and b are invisibly quantified (AKA their applications are inferred) and f is visibly quantified (AKA you must apply it as if it was a term), with "func @A @B F" as the application syntax |
2025-02-09 23:46:19 +0100 | myxos | (~myxos@syn-065-028-251-121.res.spectrum.com) (Ping timeout: 260 seconds) |
2025-02-09 23:46:56 +0100 | tri | (~tri@ool-44c70bcb.dyn.optonline.net) |
2025-02-09 23:48:01 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) sixfourtwelve |
2025-02-09 23:48:02 +0100 | <haskellbridge> | <Bowuigi> Sorry, "(x : k) -> t" is visible quantification, "{x : k} t" is invisible |
2025-02-09 23:48:04 +0100 | mange | (~user@user/mange) mange |
2025-02-09 23:48:09 +0100 | sixfourtwelve | (~ethanmorg@82.18.82.103) (Client Quit) |
2025-02-09 23:53:43 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2025-02-09 23:59:39 +0100 | lunitur | (~halloy485@2a00:1bb8:11c:a9a5:5d31:a95b:66b2:d7f4) (Ping timeout: 265 seconds) |