2023-11-11 00:05:42 +0100 | arahael | (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) |
2023-11-11 00:08:02 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) |
2023-11-11 00:08:11 +0100 | tomjaguarpaw | (~tom@172.104.25.182) (Server closed connection) |
2023-11-11 00:08:25 +0100 | tomjaguarpaw | (~tom@172-104-25-182.ip.linodeusercontent.com) |
2023-11-11 00:09:40 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds) |
2023-11-11 00:15:41 +0100 | mc47 | (~mc47@xmonad/TheMC47) |
2023-11-11 00:16:40 +0100 | themc47 | (~mc47@xmonad/TheMC47) (Ping timeout: 246 seconds) |
2023-11-11 00:21:20 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2023-11-11 00:21:31 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 264 seconds) |
2023-11-11 00:22:42 +0100 | Lord_of_Life_ | Lord_of_Life |
2023-11-11 00:24:22 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) (Quit: Lost terminal) |
2023-11-11 00:33:04 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 258 seconds) |
2023-11-11 00:33:24 +0100 | arahael | (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) (Quit: Lost terminal) |
2023-11-11 00:36:57 +0100 | Square | (~Square@user/square) |
2023-11-11 00:37:25 +0100 | Natch| | (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
2023-11-11 00:37:43 +0100 | Natch | (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Ping timeout: 264 seconds) |
2023-11-11 00:37:57 +0100 | euleritian | (~euleritia@dynamic-046-114-206-043.46.114.pool.telefonica.de) (Ping timeout: 255 seconds) |
2023-11-11 00:38:49 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2023-11-11 00:40:34 +0100 | arahael | (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) |
2023-11-11 00:43:08 +0100 | <EvanR> | a non-integer number might be e.g. a number with a fractional part. A non-rational number e.g. has an irrational part. A non-real number has an imaginary part. Finally, and this terminology is apparently used in scheme docs, an implementation may support non-complex numbers xD |
2023-11-11 00:43:40 +0100 | <EvanR> | so in a galaxy brain meme, means simple numbers, i.e. nats xD |
2023-11-11 00:46:39 +0100 | <EvanR> | ok they're probably talking about quaternions but non-complex sounds funny |
2023-11-11 00:47:11 +0100 | geekosaur | hands EvanR some infinitesimals |
2023-11-11 00:48:32 +0100 | thegeekinside | (~thegeekin@189.141.80.123) |
2023-11-11 00:48:45 +0100 | <haskellbridge> | 12<Celestial> where in that order would complex numbers formed by the integers fit? Basically instead of {a + bi | a, b in R}, {a + bi | a, b in Z} |
2023-11-11 00:50:12 +0100 | <geekosaur> | nobody cares about the Gaussian integers 😞 |
2023-11-11 00:50:29 +0100 | <geekosaur> | (iirc the definition of Haskell's Complex excludes them) |
2023-11-11 00:50:36 +0100 | <geekosaur> | % :i Complex |
2023-11-11 00:50:36 +0100 | <yahb2> | <interactive>:1:1: error: Not in scope: ‘Complex’ |
2023-11-11 00:50:45 +0100 | <geekosaur> | % import Data.Complex |
2023-11-11 00:50:46 +0100 | <yahb2> | <no output> |
2023-11-11 00:50:47 +0100 | <geekosaur> | % :i Complex |
2023-11-11 00:50:48 +0100 | <yahb2> | type Complex :: * -> * ; data Complex a = !a :+ !a ; -- Defined in ‘Data.Complex’ ; instance Applicative Complex -- Defined in ‘Data.Complex’ ; instance Eq a => Eq (Complex a) -- Defined in ‘Dat... |
2023-11-11 00:51:15 +0100 | <haskellbridge> | 12<Celestial> you'd probably want to lookat its Num instance |
2023-11-11 00:51:20 +0100 | <geekosaur> | huh, wasn't there a Fractional constraint there at one point? |
2023-11-11 00:51:42 +0100 | <geekosaur> | wait, can't have thatr on `data` |
2023-11-11 00:51:43 +0100 | <haskellbridge> | 12<Celestial> in the type itself? |
2023-11-11 00:51:51 +0100 | <geekosaur> | not usefully at least |
2023-11-11 00:52:30 +0100 | <haskellbridge> | 12<Celestial> The num Instance of Complex has a `RealFrac` contraint |
2023-11-11 00:52:35 +0100 | <EvanR> | > (1:Int) :+ 2 |
2023-11-11 00:52:36 +0100 | <lambdabot> | error: |
2023-11-11 00:52:36 +0100 | <lambdabot> | • Data constructor not in scope: Int :: [a] |
2023-11-11 00:52:36 +0100 | <lambdabot> | • Perhaps you meant variable ‘int’ (imported from Text.PrettyPrint.Hughe... |
2023-11-11 00:52:37 +0100 | <haskellbridge> | 12<Celestial> RealFloat* |
2023-11-11 00:52:42 +0100 | <EvanR> | > (1::Int) :+ 2 |
2023-11-11 00:52:43 +0100 | <lambdabot> | 1 :+ 2 |
2023-11-11 00:52:46 +0100 | <EvanR> | yay |
2023-11-11 00:53:00 +0100 | <EvanR> | machine complex |
2023-11-11 00:53:08 +0100 | <geekosaur> | but the other methods have Floating or RealFloat, from the looks of it |
2023-11-11 00:53:40 +0100 | <EvanR> | > ((1::Int) :+ 2) + 9 |
2023-11-11 00:53:42 +0100 | <lambdabot> | error: |
2023-11-11 00:53:42 +0100 | <lambdabot> | • No instance for (RealFloat Int) arising from a use of ‘+’ |
2023-11-11 00:53:42 +0100 | <lambdabot> | • In the expression: ((1 :: Int) :+ 2) + 9 |
2023-11-11 00:53:50 +0100 | <EvanR> | wat |
2023-11-11 00:53:51 +0100 | <geekosaur> | which limits their usefulness |
2023-11-11 00:54:28 +0100 | <EvanR> | because abs requires sqrt |
2023-11-11 00:54:33 +0100 | <EvanR> | stupid Num class |
2023-11-11 00:55:21 +0100 | <haskellbridge> | 12<Celestial> bridge users can't use the bot right |
2023-11-11 00:55:44 +0100 | <EvanR> | someone here could set up a script to rely bot commands xD |
2023-11-11 00:56:04 +0100 | <EvanR> | relay |
2023-11-11 01:00:42 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
2023-11-11 01:03:38 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
2023-11-11 01:05:52 +0100 | <geekosaur> | probably for the best |
2023-11-11 01:05:54 +0100 | <geekosaur> | > (1 :+ 5) :+ (2 :+ 3) |
2023-11-11 01:05:55 +0100 | <lambdabot> | (1 :+ 5) :+ (2 :+ 3) |
2023-11-11 01:11:37 +0100 | alp_ | (~alp@2001:861:5e02:eff0:7ec6:459:f36f:4240) (Ping timeout: 246 seconds) |
2023-11-11 01:13:21 +0100 | neceve | (~neceve@user/neceve) (Ping timeout: 240 seconds) |
2023-11-11 01:13:35 +0100 | Pickchea | (~private@user/pickchea) (Quit: Leaving) |
2023-11-11 01:14:44 +0100 | pavonia | (~user@user/siracusa) |
2023-11-11 01:15:51 +0100 | thegeekinside | (~thegeekin@189.141.80.123) (Remote host closed the connection) |
2023-11-11 01:26:56 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800::302a) (Remote host closed the connection) |
2023-11-11 01:41:02 +0100 | arahael | (~arahael@119-18-2-212.771202.syd.nbn.aussiebb.net) (Ping timeout: 255 seconds) |
2023-11-11 01:41:57 +0100 | sansk | (~sansk@user/sansk) |
2023-11-11 01:51:31 +0100 | Square | (~Square@user/square) (Ping timeout: 246 seconds) |
2023-11-11 01:54:00 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2023-11-11 01:56:45 +0100 | derpyxdhs | (~Thunderbi@user/derpyxdhs) |
2023-11-11 01:57:01 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds) |
2023-11-11 02:02:19 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
2023-11-11 02:06:28 +0100 | ddellacosta | (~ddellacos@ool-44c738de.dyn.optonline.net) (Ping timeout: 255 seconds) |
2023-11-11 02:06:37 +0100 | sansk | (~sansk@user/sansk) (Quit: WeeChat 4.0.4) |
2023-11-11 02:10:14 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
2023-11-11 02:10:42 +0100 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
2023-11-11 02:12:58 +0100 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) |
2023-11-11 02:13:28 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
2023-11-11 02:14:27 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2023-11-11 02:14:38 +0100 | chomwitt | (~chomwitt@2a02:587:7a12:2d00:1ac0:4dff:fedb:a3f1) (Ping timeout: 252 seconds) |
2023-11-11 02:29:11 +0100 | hueso | (~root@user/hueso) (Ping timeout: 255 seconds) |
2023-11-11 02:29:12 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-11-11 02:30:09 +0100 | hueso | (~root@user/hueso) |
2023-11-11 02:33:03 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 258 seconds) |
2023-11-11 02:33:48 +0100 | Me-me | (~me-me@user/me-me) (Server closed connection) |
2023-11-11 02:35:32 +0100 | Me-me | (~me-me@2602:ff16:3:0:1:dc:beef:d00d) |
2023-11-11 02:44:12 +0100 | derpyxdhs | (~Thunderbi@user/derpyxdhs) (Quit: derpyxdhs) |
2023-11-11 02:46:45 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-11 02:51:22 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
2023-11-11 02:53:42 +0100 | ec_ | ec |
2023-11-11 02:59:32 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) (Server closed connection) |
2023-11-11 02:59:42 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) |
2023-11-11 03:15:58 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Ping timeout: 272 seconds) |
2023-11-11 03:18:09 +0100 | otto_s | (~user@p5de2fb17.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
2023-11-11 03:18:19 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-11 03:19:48 +0100 | otto_s | (~user@p5de2f676.dip0.t-ipconnect.de) |
2023-11-11 03:25:21 +0100 | glguy | (g@libera/staff/glguy) (*.net *.split) |
2023-11-11 03:25:35 +0100 | glguy | (g@libera/staff/glguy) |
2023-11-11 03:37:57 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) |
2023-11-11 03:49:57 +0100 | <monochrom> | w00t Complex (Complex a) |
2023-11-11 03:50:12 +0100 | <monochrom> | I think I heard that Complex is actually a Monad instance! |
2023-11-11 03:50:52 +0100 | <monochrom> | Haha yes, even better, MonadFix and MonadZip too. |
2023-11-11 03:51:18 +0100 | <monochrom> | "since base-4.15.0.0" |
2023-11-11 03:51:46 +0100 | <monochrom> | OK Functor Applicative Monad were since 4.9.0.0. |
2023-11-11 03:51:56 +0100 | <EvanR> | 🤔 |
2023-11-11 03:52:39 +0100 | <monochrom> | > join (1 :+ 5) :+ (2 :+ 3) |
2023-11-11 03:52:41 +0100 | <lambdabot> | (1.0 :+ 0.0) :+ (2.0 :+ 3.0) |
2023-11-11 03:52:45 +0100 | <monochrom> | :) |
2023-11-11 03:53:28 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
2023-11-11 03:53:51 +0100 | <EvanR> | shouldn't that be -2 :+ 7 |
2023-11-11 03:53:59 +0100 | <EvanR> | er |
2023-11-11 03:54:13 +0100 | <monochrom> | "It's complicated." :) |
2023-11-11 03:56:30 +0100 | <monochrom> | Yeah I was thinking 1 :+ 3 |
2023-11-11 03:56:47 +0100 | <EvanR> | lol |
2023-11-11 03:57:30 +0100 | <EvanR> | :t (1 :+ 5) :+ (2 :+ 3) |
2023-11-11 03:57:31 +0100 | <lambdabot> | Num a => Complex (Complex a) |
2023-11-11 03:57:39 +0100 | <EvanR> | :t join (1 :+ 5) :+ (2 :+ 3) |
2023-11-11 03:57:40 +0100 | <lambdabot> | RealFloat a => Complex (Complex a) |
2023-11-11 03:57:44 +0100 | <EvanR> | wtf |
2023-11-11 03:58:11 +0100 | <EvanR> | :t join ((1 :+ 5) :+ (2 :+ 3)) |
2023-11-11 03:58:12 +0100 | <lambdabot> | Num a => Complex a |
2023-11-11 03:58:29 +0100 | <monochrom> | Oh! Right, I blew the parentheses. |
2023-11-11 03:58:45 +0100 | <monochrom> | > join ((1 :+ 5) :+ (2 :+ 3)) |
2023-11-11 03:58:46 +0100 | <lambdabot> | 1 :+ 3 |
2023-11-11 03:58:47 +0100 | <geekosaur> | gutter quaternions? 😛 |
2023-11-11 03:58:51 +0100 | <monochrom> | better |
2023-11-11 03:59:44 +0100 | <EvanR> | a discarding monad |
2023-11-11 03:59:56 +0100 | <EvanR> | > return 7 :: Complex Double |
2023-11-11 03:59:58 +0100 | <lambdabot> | 7.0 :+ 7.0 |
2023-11-11 04:00:31 +0100 | <monochrom> | Generally if you have "data P a = P a a" then the only correct join is join (P (P x _) (P _ y)) = P x y. |
2023-11-11 04:01:05 +0100 | <EvanR> | taking the diagonal |
2023-11-11 04:01:15 +0100 | <monochrom> | It is discarding because you have an isomorphism with Bool->a |
2023-11-11 04:01:23 +0100 | <monochrom> | Or yeah, diagonal |
2023-11-11 04:02:04 +0100 | <EvanR> | MONADS. you can't explain that |
2023-11-11 04:02:38 +0100 | <EvanR> | must be a miracle 🤡 |
2023-11-11 04:04:17 +0100 | <EvanR> | so every representable functor is a monad in a unique way because function monad |
2023-11-11 04:04:21 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
2023-11-11 04:04:21 +0100 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
2023-11-11 04:04:21 +0100 | finn_elija | FinnElija |
2023-11-11 04:07:15 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-11-11 04:08:32 +0100 | edr | (~edr@user/edr) (Quit: Leaving) |
2023-11-11 04:16:33 +0100 | td_ | (~td@i53870938.versanet.de) (Ping timeout: 258 seconds) |
2023-11-11 04:18:19 +0100 | td_ | (~td@i53870937.versanet.de) |
2023-11-11 04:18:31 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
2023-11-11 04:20:22 +0100 | <catilina> | jackdk: following your and [exa]'s pointers, I've got the code to not fail upon running now in https://paste.tomsmeding.com/UUEr8bhj. It still breaks the workflow as the meta values are assigned (in line 5 and 6) before the filter in line 7. |
2023-11-11 04:21:07 +0100 | <catilina> | do you see how I can merge the 3 lines? |
2023-11-11 04:24:21 +0100 | ystael | (~ystael@user/ystael) (Ping timeout: 240 seconds) |
2023-11-11 04:25:13 +0100 | <jackdk> | catilina: move the `@(Pandoc meta _)` pattern match to the second binding of `pandoc <-`? |
2023-11-11 04:28:39 +0100 | <catilina> | Hmm, that seems to somewhat work: https://paste.tomsmeding.com/XLgzznfh |
2023-11-11 04:29:13 +0100 | <catilina> | but now there's an error in the type somewhere else, so not fully? |
2023-11-11 04:34:46 +0100 | <jackdk> | don't know, sorry. I have too much on this weekend to crack open the project and look at it, I hope someone else can help |
2023-11-11 04:36:42 +0100 | <catilina> | no worries - hope you have a good weekend! |
2023-11-11 04:42:25 +0100 | rosco | (~rosco@yp-150-69.tm.net.my) |
2023-11-11 04:47:40 +0100 | Inst | (~Inst@120.244.192.250) |
2023-11-11 04:51:15 +0100 | user2 | (~user@162.255.84.96) (Server closed connection) |
2023-11-11 04:51:37 +0100 | user2 | (~user@162.255.84.96) |
2023-11-11 04:57:59 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
2023-11-11 05:09:53 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
2023-11-11 05:10:56 +0100 | Xe | (~cadey@perl/impostor/xe) (Server closed connection) |
2023-11-11 05:11:23 +0100 | Xe | (~cadey@perl/impostor/xe) |
2023-11-11 05:12:54 +0100 | xff0x | (~xff0x@2405:6580:b080:900:451:c5fa:806e:352e) (Ping timeout: 258 seconds) |
2023-11-11 05:14:40 +0100 | xff0x | (~xff0x@178.255.149.135) |
2023-11-11 05:16:12 +0100 | aforemny_ | (~aforemny@2001:9e8:6cd8:e200:b35d:4788:701d:c1c7) |
2023-11-11 05:16:34 +0100 | mud | (~mud@user/kadoban) |
2023-11-11 05:17:30 +0100 | aforemny | (~aforemny@2001:9e8:6cf3:9f00:3f53:5505:c25d:bb07) (Ping timeout: 258 seconds) |
2023-11-11 05:21:05 +0100 | xff0x | (~xff0x@178.255.149.135) (Ping timeout: 252 seconds) |
2023-11-11 05:22:55 +0100 | xff0x | (~xff0x@2405:6580:b080:900:ad36:3751:9aba:5ce7) |
2023-11-11 05:24:32 +0100 | myme | (~myme@2a01:799:d60:e400:303:74c0:223b:e4a8) (Ping timeout: 272 seconds) |
2023-11-11 05:25:21 +0100 | myme | (~myme@2a01:799:d60:e400:8378:aee3:77de:c4de) |
2023-11-11 05:28:15 +0100 | YuutaW | (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (Ping timeout: 240 seconds) |
2023-11-11 05:29:54 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
2023-11-11 05:32:51 +0100 | zero | yin |
2023-11-11 05:35:19 +0100 | rosco | (~rosco@yp-150-69.tm.net.my) (Quit: Lost terminal) |
2023-11-11 05:47:35 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 05:49:09 +0100 | zups | (~meow@2a01:4f9:c010:6036::1) (Server closed connection) |
2023-11-11 05:49:27 +0100 | zups | (~meow@2a01:4f9:c010:6036::1) |
2023-11-11 05:55:43 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
2023-11-11 06:08:45 +0100 | qqq | (~qqq@92.43.167.61) |
2023-11-11 06:11:36 +0100 | trev | (~trev@user/trev) |
2023-11-11 06:22:50 +0100 | rosco | (~rosco@193.138.218.161) |
2023-11-11 06:40:58 +0100 | Inst | (~Inst@120.244.192.250) (Remote host closed the connection) |
2023-11-11 06:41:15 +0100 | Inst | (~Inst@120.244.192.250) |
2023-11-11 06:45:21 +0100 | rosco | (~rosco@193.138.218.161) (Ping timeout: 240 seconds) |
2023-11-11 06:47:35 +0100 | rosco | (~rosco@193.138.218.161) |
2023-11-11 06:51:01 +0100 | td_ | (~td@i53870937.versanet.de) (Ping timeout: 240 seconds) |
2023-11-11 06:51:41 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 240 seconds) |
2023-11-11 06:51:49 +0100 | <Inst> | I think it's possible to have an IO instance for traversable, but why isn't it in base? |
2023-11-11 06:52:58 +0100 | td_ | (~td@i53870901.versanet.de) |
2023-11-11 06:53:39 +0100 | <Inst> | I know about chshersh's IO as an instance of Num, you guys were making fun of me for a IsString instance of IO, but IO is still a Semigroup and Monoid, not sure why Traversable IO is a bad idea? |
2023-11-11 06:53:55 +0100 | rosco | (~rosco@193.138.218.161) (Ping timeout: 246 seconds) |
2023-11-11 06:54:28 +0100 | <Inst> | oh, Foldable |
2023-11-11 06:54:37 +0100 | <Inst> | Traversable requires Foldable, and Foldable IO -> unsafePerformIO |
2023-11-11 06:54:38 +0100 | <Inst> | doip |
2023-11-11 06:59:20 +0100 | <monochrom> | I think I speak for most regular when I say that I am mostly skeptical of most implicit type conversion puns. |
2023-11-11 06:59:38 +0100 | <monochrom> | s/regular/regulars/ |
2023-11-11 07:00:08 +0100 | <Inst> | Yeah, I know, I had it explained to me why throwing IsString around, especially with outside library types, is a bad idea. |
2023-11-11 07:00:08 +0100 | bilegeek | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
2023-11-11 07:00:15 +0100 | <monochrom> | Even IsString, I refuse to use it except for very specific scenerios. |
2023-11-11 07:00:18 +0100 | <Inst> | *base library types |
2023-11-11 07:00:26 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-11 07:00:32 +0100 | euleritian | (~euleritia@dynamic-046-114-206-043.46.114.pool.telefonica.de) |
2023-11-11 07:00:36 +0100 | <Inst> | I got around my problem by converting my string into a lambda, then fmap / <*> into the effects I wanted |
2023-11-11 07:00:55 +0100 | euleritian | (~euleritia@dynamic-046-114-206-043.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-11-11 07:01:12 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 07:01:15 +0100 | <Inst> | I have no objection to purity, and am willing to pay a reasonable price for it. |
2023-11-11 07:02:21 +0100 | <Inst> | Thanks for the response monochrom :) |
2023-11-11 07:02:24 +0100 | <monochrom> | Num IO and IsString IO cross the grey area and unambiguosly step into "why don't you just go with javascript and tcl and leave us alone" territory. |
2023-11-11 07:03:42 +0100 | <Inst> | ChShersh, btw, is now talking about how he likes Typescript and Python now :) |
2023-11-11 07:04:06 +0100 | <monochrom> | Equivalently I am not saying they are wrong, I am saying they are against the spirit of Haskell, they are shoehorning other languages into Haskell. javscript and tcl exist for a reason, for people or scenerios who need that. |
2023-11-11 07:04:53 +0100 | <Inst> | monochrom: as far as I understand, it's a matter of scale, you can do all sorts of weird tricks with Haskell to break it at small scales, but Haskell will have a nasty revenge once you scale up |
2023-11-11 07:05:11 +0100 | <Inst> | and all the inconveniences are there for a reason |
2023-11-11 07:06:00 +0100 | _xor | (~xor@72.49.195.41) |
2023-11-11 07:06:29 +0100 | <monochrom> | There is no way you can shoehorn all programming styles into one language. They conflict with each other. You must accept a trade off and give up something. |
2023-11-11 07:08:05 +0100 | <Inst> | I think looking at a certain legacied 132k SLOC codebase with varying code styles |
2023-11-11 07:08:19 +0100 | <Inst> | I used to not understand why people loved their monad transformers, effect systems, etc, so much |
2023-11-11 07:09:13 +0100 | <Inst> | now I understand, with very simple code, small programs, it doesn't really matter what you do, or what architectures you use, but working on larger programs / codebases, architecture, safety, all the ideological constraints of Haskell, make sense |
2023-11-11 07:11:26 +0100 | fweht | (uid404746@id-404746.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2023-11-11 07:12:47 +0100 | totbwf | (sid402332@id-402332.uxbridge.irccloud.com) (Server closed connection) |
2023-11-11 07:13:01 +0100 | totbwf | (sid402332@id-402332.uxbridge.irccloud.com) |
2023-11-11 07:21:58 +0100 | arahael | (~arahael@1.145.75.174) |
2023-11-11 07:22:19 +0100 | <hammond> | does increased modularity and granularity affect readability? |
2023-11-11 07:22:45 +0100 | <Hecate> | hammond: yes |
2023-11-11 07:22:51 +0100 | <monochrom> | Define readability, e.g., readable by 3yo? readable by educated people? |
2023-11-11 07:23:35 +0100 | <hammond> | should i make my objects bigger and coarser? to improve readability? aka use broader strokes? |
2023-11-11 07:23:40 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
2023-11-11 07:24:06 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
2023-11-11 07:24:11 +0100 | <Hecate> | monochrom: more like "readable by the same person with less headache" |
2023-11-11 07:24:11 +0100 | <hammond> | well readable would be something that takes an average human a reasonable amount of time to understand. |
2023-11-11 07:24:15 +0100 | <Inst> | Sorry if this is not helpful, or boring, but I can understand why people prefer abstractions, even at the small scale |
2023-11-11 07:24:45 +0100 | <monochrom> | The average human is not even programming-literate. |
2023-11-11 07:24:45 +0100 | <Hecate> | hammond: if you're looking to create abstractions, determine first if you will use them more than twice |
2023-11-11 07:25:10 +0100 | <Inst> | When you start with a language, you are working at the small scale, but you develop habits there. What might work for scripts won't work for larger programs, and you're going to end up taking your scripting habits up when working with larger programs, so it's better to start with good habits. |
2023-11-11 07:25:24 +0100 | <monochrom> | That may change in the near future but even 10 years from now it will only be, say, Swift-literate. |
2023-11-11 07:25:52 +0100 | <Hecate> | monochrom: I think hammond is talking about something else here |
2023-11-11 07:25:57 +0100 | <hammond> | hecate that's the thing. you make this ultra fine grained library and say you will reuse the code, and it kinda makes things harder. |
2023-11-11 07:26:00 +0100 | bilegeek_ | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
2023-11-11 07:26:37 +0100 | <monochrom> | s/talking/thinking/ |
2023-11-11 07:27:09 +0100 | <monochrom> | But I am not going to play telepathy. I can only work with the exact wording. |
2023-11-11 07:27:21 +0100 | <Hecate> | hammond: that's why we have refactorings. :) But it's better to have something that works first before generalising it |
2023-11-11 07:27:23 +0100 | <hammond> | monochrom: so you say readibility doesnt matter. |
2023-11-11 07:27:36 +0100 | <monochrom> | No, I say readability is undefined. |
2023-11-11 07:27:49 +0100 | <monochrom> | Or even better, moving goalpost. |
2023-11-11 07:27:50 +0100 | <hammond> | code should can be difficult, because we are supposed to be programmers. |
2023-11-11 07:27:51 +0100 | bilegeek | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Ping timeout: 240 seconds) |
2023-11-11 07:28:22 +0100 | harveypwca | (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) |
2023-11-11 07:28:25 +0100 | <Inst> | monochrom: can we define it as "readable by the end user", or "readable by probable collaborators"? Although, the latter seems trivial (i.e, if it's not readable, they won't collaborate). |
2023-11-11 07:29:40 +0100 | bilegeek_ | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Read error: Connection reset by peer) |
2023-11-11 07:29:57 +0100 | bilegeek_ | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
2023-11-11 07:31:17 +0100 | <hammond> | Hecate, the opposite of generalization is specialization. say i write a large function that only does one thing. I can probably break that function into smaller generalized pieces of code. by doing that i'm reducing readability. |
2023-11-11 07:31:30 +0100 | <hammond> | it's kinda like having a bunch of GOTOs. |
2023-11-11 07:32:42 +0100 | <monochrom> | It is always personal. It is always an echo chamber. You make your a library in a certain way, a certain style. Then it attracts people who understand it and repels people who don't. But you forget the selection bias echo chamber and jump from "this library is readable by people who like it this way" to "this library is readable, absolutely, unconditionally, universally, period, now why some other people don't get it?". It is always personal, it is |
2023-11-11 07:32:42 +0100 | <monochrom> | always an echo chamber. |
2023-11-11 07:32:53 +0100 | <Hecate> | hammond: I don't necessarily agree, taken individually these pieces become more readable because their dependencies are made more explicit |
2023-11-11 07:33:31 +0100 | <Inst> | Maybe that's a question of culture, i.e, some people might find a monolith more readable, others would have an easier time with smaller functions. |
2023-11-11 07:33:51 +0100 | <Inst> | It's weird, what attracted me to Haskell in the first place was how short and comprehensible the individual pieces of Haskell programs were. |
2023-11-11 07:34:01 +0100 | <Inst> | Now I'm more addicted to where clause abuse. |
2023-11-11 07:34:52 +0100 | bilegeek_ | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Ping timeout: 246 seconds) |
2023-11-11 07:37:16 +0100 | jpds | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 264 seconds) |
2023-11-11 07:38:04 +0100 | <hammond> | Hecate but you would have to jump from this file to another file and back again, just to understand a portion. code reuseability is great, and can still be done, but at a coarser level. this is horrible example, but think bash script. |
2023-11-11 07:39:52 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
2023-11-11 07:40:44 +0100 | califax | (~califax@user/califx) |
2023-11-11 07:46:08 +0100 | <Hecate> | hammond: yeah it's alright to jump files. Well first of all you can have two files open side by side, but also you should be taking notes when diving into a code base |
2023-11-11 07:46:18 +0100 | <hammond> | "The animal jumped on my desk and was playing with my keyboard." as opposed to "The cat jumped ... etc" by being specific you are more readible. Lisp is great, you can really abstract a lof of things, but it's incredibly unreadible. |
2023-11-11 07:46:30 +0100 | <hammond> | haha ok |
2023-11-11 07:54:25 +0100 | jpds | (~jpds@gateway/tor-sasl/jpds) |
2023-11-11 08:00:53 +0100 | danza | (~francesco@151.35.107.96) |
2023-11-11 08:07:08 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Read error: Connection reset by peer) |
2023-11-11 08:07:51 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2023-11-11 08:11:01 +0100 | danza | (~francesco@151.35.107.96) (Ping timeout: 240 seconds) |
2023-11-11 08:14:03 +0100 | zaquest | (~notzaques@5.130.79.72) |
2023-11-11 08:16:11 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-11 08:19:52 +0100 | thegman | (~thegman@072-239-207-086.res.spectrum.com) (Quit: leaving) |
2023-11-11 08:20:43 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
2023-11-11 08:22:50 +0100 | alp_ | (~alp@2001:861:5e02:eff0:40ee:54d5:8b84:9bc6) |
2023-11-11 08:26:15 +0100 | yoyofreeman | (~yoyofreem@176.97.76.178) |
2023-11-11 08:27:40 +0100 | califax | (~califax@user/califx) (Ping timeout: 264 seconds) |
2023-11-11 08:29:31 +0100 | califax | (~califax@user/califx) |
2023-11-11 08:40:51 +0100 | acidjnk | (~acidjnk@p200300d6e72b9351ac6f5a8b7958b98c.dip0.t-ipconnect.de) |
2023-11-11 08:45:16 +0100 | td_ | (~td@i53870901.versanet.de) (Ping timeout: 258 seconds) |
2023-11-11 08:45:22 +0100 | Square | (~Square@user/square) |
2023-11-11 08:50:42 +0100 | arahael | (~arahael@1.145.75.174) (Ping timeout: 255 seconds) |
2023-11-11 08:51:59 +0100 | td_ | (~td@i5387091C.versanet.de) |
2023-11-11 08:57:56 +0100 | misterfish | (~misterfis@84-53-85-146.bbserv.nl) |
2023-11-11 09:01:44 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-11 09:02:31 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 09:09:37 +0100 | harveypwca | (~harveypwc@2601:246:c280:7940:585a:99af:3e4c:209b) (Quit: Leaving) |
2023-11-11 09:11:14 +0100 | <Inst> | this is weird |
2023-11-11 09:11:22 +0100 | <Inst> | > u.moo = "Moo!" |
2023-11-11 09:11:24 +0100 | <lambdabot> | <hint>:1:7: error: parse error on input ‘=’ |
2023-11-11 09:11:36 +0100 | <Inst> | > uuoouo.moo = "Moo!" |
2023-11-11 09:11:37 +0100 | <lambdabot> | <hint>:1:12: error: parse error on input ‘=’ |
2023-11-11 09:11:44 +0100 | <Inst> | well, GHCI will accept this, however |
2023-11-11 09:11:51 +0100 | <Inst> | oh, it's accepting it as a definition of . |
2023-11-11 09:12:52 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
2023-11-11 09:13:50 +0100 | euleritian | (~euleritia@dynamic-046-114-203-139.46.114.pool.telefonica.de) |
2023-11-11 09:13:52 +0100 | ddellacosta | (~ddellacos@ool-44c738de.dyn.optonline.net) |
2023-11-11 09:16:42 +0100 | fendor | (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) |
2023-11-11 09:17:11 +0100 | bilegeek_ | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) |
2023-11-11 09:20:11 +0100 | YuutaW | (~YuutaW@mail.yuuta.moe) |
2023-11-11 09:23:54 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 09:24:07 +0100 | AlexZenon_2 | (~alzenon@94.233.241.129) |
2023-11-11 09:24:30 +0100 | Pickchea | (~private@user/pickchea) |
2023-11-11 09:25:40 +0100 | AlexZenon | (~alzenon@94.233.241.129) (Ping timeout: 255 seconds) |
2023-11-11 09:26:43 +0100 | kimiamania464 | (~b4f4a2ab@user/kimiamania) |
2023-11-11 09:27:01 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 255 seconds) |
2023-11-11 09:27:01 +0100 | bah | (~bah@l1.tel) (Ping timeout: 255 seconds) |
2023-11-11 09:27:10 +0100 | bah | (~bah@l1.tel) |
2023-11-11 09:28:22 +0100 | kimiamania46 | (~b4f4a2ab@user/kimiamania) (Ping timeout: 255 seconds) |
2023-11-11 09:28:22 +0100 | kimiamania464 | kimiamania46 |
2023-11-11 09:33:20 +0100 | CiaoSen | (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
2023-11-11 09:37:32 +0100 | joel135 | (sid136450@id-136450.hampstead.irccloud.com) (Server closed connection) |
2023-11-11 09:37:50 +0100 | joel135 | (sid136450@id-136450.hampstead.irccloud.com) |
2023-11-11 09:44:37 +0100 | danza | (~francesco@151.43.102.160) |
2023-11-11 09:48:00 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
2023-11-11 09:48:45 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
2023-11-11 09:49:50 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-11 09:50:34 +0100 | drlkf | (~drlkf@192.184.163.34.bc.googleusercontent.com) (Server closed connection) |
2023-11-11 09:51:00 +0100 | drlkf | (~drlkf@192.184.163.34.bc.googleusercontent.com) |
2023-11-11 09:52:44 +0100 | CiaoSen | (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) (Ping timeout: 258 seconds) |
2023-11-11 10:00:49 +0100 | alp_ | (~alp@2001:861:5e02:eff0:40ee:54d5:8b84:9bc6) (Ping timeout: 246 seconds) |
2023-11-11 10:03:57 +0100 | ss4 | (~wootehfoo@user/wootehfoot) |
2023-11-11 10:04:14 +0100 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) |
2023-11-11 10:05:17 +0100 | euleritian | (~euleritia@dynamic-046-114-203-139.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
2023-11-11 10:05:28 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 264 seconds) |
2023-11-11 10:05:35 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 10:08:52 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-11-11 10:12:44 +0100 | ss4 | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
2023-11-11 10:13:01 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2023-11-11 10:13:49 +0100 | yushyin | (9DYMgg4QG5@mail.karif.server-speed.net) (Server closed connection) |
2023-11-11 10:14:11 +0100 | yushyin | (lVHsxtO6yj@mail.karif.server-speed.net) |
2023-11-11 10:21:10 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-11 10:21:51 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 10:25:56 +0100 | CO2 | (CO2@gateway/vpn/protonvpn/co2) |
2023-11-11 10:27:11 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
2023-11-11 10:29:52 +0100 | caubert_ | (~caubert@user/caubert) (Server closed connection) |
2023-11-11 10:30:11 +0100 | caubert | (~caubert@user/caubert) |
2023-11-11 10:31:37 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
2023-11-11 10:32:18 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
2023-11-11 10:33:04 +0100 | gmg | (~user@user/gehmehgeh) |
2023-11-11 10:37:04 +0100 | codedmart | (~codedmart@li335-49.members.linode.com) (Server closed connection) |
2023-11-11 10:37:22 +0100 | codedmart | (~codedmart@li335-49.members.linode.com) |
2023-11-11 10:40:24 +0100 | davl_ | (~davl@207.154.228.18) |
2023-11-11 10:40:43 +0100 | kiriakos | (~kiriakos@p5b03e4a6.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
2023-11-11 10:40:58 +0100 | disconnect3d | (~disconnec@user/disconnect3d) (Ping timeout: 255 seconds) |
2023-11-11 10:40:58 +0100 | davl | (~davl@207.154.228.18) (Ping timeout: 255 seconds) |
2023-11-11 10:41:04 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-11-11 10:42:42 +0100 | disconnect3d | (~disconnec@user/disconnect3d) |
2023-11-11 10:42:55 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
2023-11-11 10:43:52 +0100 | jpds | (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 264 seconds) |
2023-11-11 10:44:52 +0100 | danza | (~francesco@151.43.102.160) (Ping timeout: 255 seconds) |
2023-11-11 10:46:41 +0100 | alp_ | (~alp@2001:861:5e02:eff0:59a7:a2ca:543c:6e8) |
2023-11-11 10:47:02 +0100 | Jackneill | (~Jackneill@20014C4E1E058A00ABC7937222D6C543.dsl.pool.telekom.hu) |
2023-11-11 10:47:55 +0100 | bjs | (sid190364@user/bjs) (Server closed connection) |
2023-11-11 10:48:06 +0100 | bjs | (sid190364@user/bjs) |
2023-11-11 10:48:58 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
2023-11-11 10:50:09 +0100 | jpds | (~jpds@gateway/tor-sasl/jpds) |
2023-11-11 10:52:21 +0100 | bilegeek_ | (~bilegeek@2600:1008:b05e:cbb0:f27c:224f:ff0f:39bd) (Quit: Leaving) |
2023-11-11 10:54:31 +0100 | Lycurgus | (~georg@user/Lycurgus) |
2023-11-11 10:56:03 +0100 | YuutaW | (~YuutaW@mail.yuuta.moe) (Ping timeout: 260 seconds) |
2023-11-11 10:58:52 +0100 | chiselfu1e | (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
2023-11-11 11:00:51 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
2023-11-11 11:04:14 +0100 | arahael | (~arahael@1.145.109.210) |
2023-11-11 11:05:33 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 11:07:37 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-11 11:12:28 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 255 seconds) |
2023-11-11 11:25:05 +0100 | tomboy64 | (~tomboy64@user/tomboy64) |
2023-11-11 11:27:46 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) |
2023-11-11 11:39:10 +0100 | acidjnk | (~acidjnk@p200300d6e72b9351ac6f5a8b7958b98c.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
2023-11-11 11:43:26 +0100 | arahael | (~arahael@1.145.109.210) (Quit: leaving) |
2023-11-11 11:49:34 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
2023-11-11 11:49:40 +0100 | arahael | (~arahael@21.127.96.58.static.exetel.com.au) |
2023-11-11 11:52:27 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
2023-11-11 11:53:33 +0100 | __monty__ | (~toonn@user/toonn) |
2023-11-11 11:59:56 +0100 | meooow | (~meooow@165.232.184.169) (Server closed connection) |
2023-11-11 12:00:11 +0100 | meooow | (~meooow@2400:6180:100:d0::ad9:e001) |
2023-11-11 12:10:12 +0100 | mc47 | (~mc47@xmonad/TheMC47) |
2023-11-11 12:17:41 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-11 12:20:42 +0100 | alp_ | (~alp@2001:861:5e02:eff0:59a7:a2ca:543c:6e8) (Ping timeout: 258 seconds) |
2023-11-11 12:22:51 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
2023-11-11 12:26:25 +0100 | catilina | (~user@49.235.216.139.sta.wbroadband.net.au) (Changing host) |
2023-11-11 12:26:25 +0100 | catilina | (~user@user/catilina) |
2023-11-11 12:28:53 +0100 | nonzen_ | (~nonzen@user/nonzen) (Server closed connection) |
2023-11-11 12:29:09 +0100 | nonzen | (~nonzen@user/nonzen) |
2023-11-11 12:31:22 +0100 | Pickchea | (~private@user/pickchea) (Quit: Leaving) |
2023-11-11 12:33:47 +0100 | alp_ | (~alp@2001:861:5e02:eff0:fda7:f942:c2a6:6612) |
2023-11-11 12:33:49 +0100 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2023-11-11 12:41:35 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-11-11 12:42:20 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Remote host closed the connection) |
2023-11-11 12:47:09 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-11-11 12:53:45 +0100 | duncan | (~duncan@nat-server.ehlab.uk) (Server closed connection) |
2023-11-11 12:54:01 +0100 | duncan | (~duncan@nat-server.ehlab.uk) |
2023-11-11 12:55:56 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-11 12:56:23 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 12:56:37 +0100 | Sgeo_ | (~Sgeo@user/sgeo) |
2023-11-11 12:57:45 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-11 12:59:41 +0100 | Sgeo | (~Sgeo@user/sgeo) (Ping timeout: 240 seconds) |
2023-11-11 13:00:23 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 13:06:25 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
2023-11-11 13:06:50 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-11-11 13:07:29 +0100 | Inst | (~Inst@120.244.192.250) (Read error: Connection reset by peer) |
2023-11-11 13:09:34 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
2023-11-11 13:09:49 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
2023-11-11 13:09:54 +0100 | Lycurgus | (~georg@li1192-118.members.linode.com) |
2023-11-11 13:09:54 +0100 | Lycurgus | (~georg@li1192-118.members.linode.com) (Changing host) |
2023-11-11 13:09:54 +0100 | Lycurgus | (~georg@user/Lycurgus) |
2023-11-11 13:15:56 +0100 | Inst | (~Inst@120.244.192.250) |
2023-11-11 13:17:08 +0100 | mankyKitty | (sid31287@id-31287.helmsley.irccloud.com) (Server closed connection) |
2023-11-11 13:17:16 +0100 | mankyKitty | (sid31287@id-31287.helmsley.irccloud.com) |
2023-11-11 13:27:34 +0100 | innegatives | (uid621315@id-621315.tinside.irccloud.com) (Server closed connection) |
2023-11-11 13:28:13 +0100 | innegatives | (sid621315@id-621315.tinside.irccloud.com) |
2023-11-11 13:35:01 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
2023-11-11 13:35:22 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 13:38:30 +0100 | CO2 | (CO2@gateway/vpn/protonvpn/co2) (Quit: WeeChat 4.1.1) |
2023-11-11 13:39:24 +0100 | neceve | (~neceve@user/neceve) |
2023-11-11 13:42:52 +0100 | amir | (sid22336@user/amir) (Server closed connection) |
2023-11-11 13:43:01 +0100 | amir | (sid22336@user/amir) |
2023-11-11 13:45:03 +0100 | alp_ | (~alp@2001:861:5e02:eff0:fda7:f942:c2a6:6612) (Ping timeout: 240 seconds) |
2023-11-11 13:45:13 +0100 | nckx | (~nckx@libera/staff/owl/nckx) (Server closed connection) |
2023-11-11 13:45:18 +0100 | zombiboo | (~user@2001:2042:3c78:ab00:ce0:e802:ba9d:f9d3) |
2023-11-11 13:46:29 +0100 | nckx | (~nckx@libera/staff/owl/nckx) |
2023-11-11 13:46:56 +0100 | fendor | (~fendor@2a02:8388:1640:be00:ca17:ceee:5bbe:1594) (Remote host closed the connection) |
2023-11-11 13:51:19 +0100 | target_i | (~target_i@217.175.14.39) |
2023-11-11 13:54:02 +0100 | zombiboo | (~user@2001:2042:3c78:ab00:ce0:e802:ba9d:f9d3) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.1)) |
2023-11-11 14:04:31 +0100 | Sgeo_ | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2023-11-11 14:11:07 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
2023-11-11 14:12:14 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
2023-11-11 14:12:35 +0100 | Umeaboy | (~Umeaboy@94-255-145-133.cust.bredband2.com) |
2023-11-11 14:13:40 +0100 | <Umeaboy> | Hi! To solve this issue I need to recompile the kernel right? https://pastebin.mozilla.org/1VssEDFs |
2023-11-11 14:20:44 +0100 | <exarkun> | I don't know, but I wouldn't guess that building ghc ever requires support for more deeply nested symbolic links than is standard. |
2023-11-11 14:21:26 +0100 | <tomsmeding> | "...../opt/lib/ghc-9.2.3/lib/package.conf.d/Cabal-3.6.3.0.conf" failed: mode 120777 broken symbolic link to ../../../../../opt/lib/ghc-9.2.3/lib/package.conf.d/Cabal-3.6.3.0.conf |
2023-11-11 14:21:30 +0100 | <tomsmeding> | that's a symbolic link to itself |
2023-11-11 14:21:39 +0100 | <tomsmeding> | you can count the number of ".." |
2023-11-11 14:21:48 +0100 | <tomsmeding> | so no, that's not suppose to happen |
2023-11-11 14:27:04 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2023-11-11 14:28:52 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-11 14:30:24 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-11-11 14:31:42 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Max SendQ exceeded) |
2023-11-11 14:32:10 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-11-11 14:32:46 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 246 seconds) |
2023-11-11 14:33:22 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
2023-11-11 14:35:24 +0100 | dunj3 | (~dunj3@kingdread.de) (Quit: ZNC 1.8.2+deb2+b1 - https://znc.in) |
2023-11-11 14:36:45 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Ping timeout: 255 seconds) |
2023-11-11 14:38:43 +0100 | arahael | (~arahael@21.127.96.58.static.exetel.com.au) (Ping timeout: 246 seconds) |
2023-11-11 14:42:23 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 260 seconds) |
2023-11-11 14:42:41 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 14:42:46 +0100 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) |
2023-11-11 14:42:50 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) |
2023-11-11 14:44:43 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-11 14:48:29 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-11 14:51:15 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
2023-11-11 14:52:39 +0100 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 240 seconds) |
2023-11-11 14:53:22 +0100 | infinity0 | (~infinity0@pwned.gg) |
2023-11-11 14:53:38 +0100 | aspen | (sid449115@id-449115.helmsley.irccloud.com) (Server closed connection) |
2023-11-11 14:53:47 +0100 | aspen | (sid449115@id-449115.helmsley.irccloud.com) |
2023-11-11 14:58:15 +0100 | <Umeaboy> | tomsmeding: So, what Can I do? |
2023-11-11 14:58:34 +0100 | <Umeaboy> | Try with a little older version? |
2023-11-11 14:59:10 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Quit: Restarting) |
2023-11-11 14:59:22 +0100 | AlexZenon_2 | AlexZenon |
2023-11-11 15:09:52 +0100 | flukiluke | (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Server closed connection) |
2023-11-11 15:10:12 +0100 | flukiluke | (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
2023-11-11 15:13:47 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 15:23:57 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
2023-11-11 15:25:02 +0100 | Lycurgus | (~georg@user/Lycurgus) |
2023-11-11 15:31:22 +0100 | michalz | (~michalz@185.246.207.203) |
2023-11-11 15:31:27 +0100 | neceve | (~neceve@user/neceve) (Ping timeout: 240 seconds) |
2023-11-11 15:31:55 +0100 | qqq | (~qqq@92.43.167.61) (Ping timeout: 246 seconds) |
2023-11-11 15:37:08 +0100 | qqq | (~qqq@92.43.167.61) |
2023-11-11 15:47:56 +0100 | mud | (~mud@user/kadoban) (Quit: quit) |
2023-11-11 16:02:22 +0100 | chomwitt | (~chomwitt@2a02:587:7a12:2d00:1ac0:4dff:fedb:a3f1) |
2023-11-11 16:06:39 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
2023-11-11 16:07:22 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
2023-11-11 16:14:55 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 264 seconds) |
2023-11-11 16:15:13 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 16:16:08 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-11 16:29:33 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) |
2023-11-11 16:31:27 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
2023-11-11 16:31:33 +0100 | mechap | (~mechap@user/mechap) |
2023-11-11 16:31:50 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 16:38:35 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
2023-11-11 16:38:57 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
2023-11-11 16:39:38 +0100 | acidjnk | (~acidjnk@p200300d6e72b9351ac6f5a8b7958b98c.dip0.t-ipconnect.de) |
2023-11-11 16:39:47 +0100 | sajith | (~sajith@user/sajith) (Server closed connection) |
2023-11-11 16:40:07 +0100 | sajith_ | (~sajith@user/sajith) |
2023-11-11 16:40:27 +0100 | alguem | (~alguem@45.163.64.23) |
2023-11-11 16:40:40 +0100 | <alguem> | test |
2023-11-11 16:41:22 +0100 | Guest65 | (~Guest65@45.163.64.23) |
2023-11-11 16:41:27 +0100 | <geekosaur> | pass |
2023-11-11 16:42:08 +0100 | <alguem> | it is my frist time using this "libera chat" is it like discord or what? |
2023-11-11 16:42:28 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-11 16:42:42 +0100 | <geekosaur> | not very |
2023-11-11 16:43:46 +0100 | <Clint> | depends on how you spin it |
2023-11-11 16:45:28 +0100 | <exarkun> | it's like N pieces of software sending small messages to M other pieces of software which then retransmits those messages largely in-tact to Q pieces of software |
2023-11-11 16:45:37 +0100 | <exarkun> | which I think is exactly identical to discord? |
2023-11-11 16:45:49 +0100 | <exarkun> | also, other things! |
2023-11-11 16:47:24 +0100 | <alguem> | it's like a text based chat protocol? |
2023-11-11 16:48:00 +0100 | <ski> | yes |
2023-11-11 16:48:18 +0100 | <geekosaur> | it just lacks a lot of modern amenities |
2023-11-11 16:48:36 +0100 | geekosaur | *poofs* — busy morning |
2023-11-11 16:48:57 +0100 | <c_wraith> | it's from.. the early 90s? |
2023-11-11 16:49:15 +0100 | <ski> | 1988 |
2023-11-11 16:49:26 +0100 | <ski> | by Jarkko Oikarinen |
2023-11-11 16:50:12 +0100 | <alguem> | it seems very cool, except that apparently it has no message historic, it seems |
2023-11-11 16:50:25 +0100 | <ski> | (i consider that a feature) |
2023-11-11 16:50:34 +0100 | <alguem> | and since I didn't gave any password in, i guess its less moderated? |
2023-11-11 16:50:40 +0100 | <alguem> | like |
2023-11-11 16:50:45 +0100 | <ski> | there's moderation |
2023-11-11 16:51:01 +0100 | <alguem> | how is that? |
2023-11-11 16:51:13 +0100 | <ski> | but you tend to be able to join channels, without necessarily making an account first, yea |
2023-11-11 16:51:14 +0100 | <exarkun> | in each channel, there are participants enabled to take certain actions |
2023-11-11 16:51:26 +0100 | <exarkun> | like mute a user, or kick them out |
2023-11-11 16:51:50 +0100 | <ski> | (some channels do require registration, though. either as a temporary measure, to say avoid spammers for a period. or more permanently) |
2023-11-11 16:51:51 +0100 | <exarkun> | also, this network _does_ have accounts and authentication, it's just optional most of the time |
2023-11-11 16:52:27 +0100 | <alguem> | I think that with an account, Ill be able to read old messages? |
2023-11-11 16:52:57 +0100 | <yushyin> | ircv3 has a chathistory extension, but it's only a draft and the libera network doesn't support it (yet) |
2023-11-11 16:52:57 +0100 | <alguem> | at least since when I joint ? |
2023-11-11 16:53:02 +0100 | <ski> | network staff for the most part stays away from getting involved in individual channel moderation, deals more with people being a problem with multiple channels |
2023-11-11 16:53:50 +0100 | <ski> | alguem : "I think that with an account, Ill be able to read old messages?" -- no. you'll be able to read (and send) MemoServ messages, though |
2023-11-11 16:54:12 +0100 | <alguem> | hmmm |
2023-11-11 16:54:21 +0100 | <alguem> | still interesting |
2023-11-11 16:55:14 +0100 | <ski> | (i see to remember seeing your nickname before, though .. perhaps from the Freenode days, maybe ? or maybe i'm confusing with someone else) |
2023-11-11 16:55:40 +0100 | <alguem> | wondering what kind of topics go here, I guess it's not meant for support with haskell? since it doesn't seem to allow images |
2023-11-11 16:55:52 +0100 | acro | (~acro@user/acro) (Server closed connection) |
2023-11-11 16:56:01 +0100 | <ski> | Haskell support and discussion goes here |
2023-11-11 16:56:07 +0100 | acro | (~acro@user/acro) |
2023-11-11 16:56:41 +0100 | <ski> | people tend to paste snippets of code on paste sites, and give the resulting links to the pastes in their messages here |
2023-11-11 16:57:32 +0100 | <ski> | (that also works for image paste sites .. although it's generally considered a bit rude to use that for code pastes, unless it's really necessary to use an image rather than text, to display the issue in question) |
2023-11-11 16:57:40 +0100 | <alguem> | Maybe you've seen, ski, "alguem" literally means "someone" in direct translation to English, so it wouldn't surprise me if someone before me used this nick, but it wasn't me, it's my first time using something like this chat |
2023-11-11 16:57:49 +0100 | <ski> | ah, that could be it :) |
2023-11-11 16:59:09 +0100 | <alguem> | I guess once I saw a guy from Youtube using something similar tho |
2023-11-11 16:59:56 +0100 | <EvanR> | alguem, IRC is like two cargo ships rendezvous in the middle of the ocean, no names no serial numbers no record the transaction takes place |
2023-11-11 17:00:10 +0100 | <alguem> | but it seemed to be complex to set up, he used it in terminal haha |
2023-11-11 17:00:31 +0100 | <EvanR> | https://www.youtube.com/watch?v=O2rGTXHvPCQ |
2023-11-11 17:00:54 +0100 | <ski> | oh, i guess i should mention .. a common mistake newbies make is thinking that noone's there, if noone appears to be responding directly within a few minutes (at best). people generally are commonly connected to IRC, while doing other things (working, eating, watching a film, and even going for a walk or sleeping) |
2023-11-11 17:02:12 +0100 | <ski> | so .. be patient, preferably wait at least half an hour after announcing your presence. also, of course, some times of day tend to be more active that others. also, people may be around, lurking or glancing at the channel, but not saying anything, until someone brings up an interesting topic |
2023-11-11 17:02:15 +0100 | <ncf> | the five human activities |
2023-11-11 17:03:27 +0100 | <EvanR> | libera has an easy to use web client |
2023-11-11 17:03:32 +0100 | <EvanR> | not complex |
2023-11-11 17:03:43 +0100 | <alguem> | i doubt that he was using libera |
2023-11-11 17:04:05 +0100 | <EvanR> | if you have your own client you can connect to any IRC network |
2023-11-11 17:04:24 +0100 | <alguem> | btw, thank you for the advice, ski :) |
2023-11-11 17:04:28 +0100 | <ski> | (also, it's not uncommon that people are a bit loathe to announce their presence, until they feel they know enough about your issue to have a chance of being able to contribute. moral : be upfront with the details of your problem. don't just say "anyone here ?" or "anyone know about X ?", since (only) saying something like that will lower your chances of getting a response. saying what you've already tried |
2023-11-11 17:04:34 +0100 | <ski> | also helps) |
2023-11-11 17:04:36 +0100 | <yushyin> | libera is one of the bigger irc networks |
2023-11-11 17:04:56 +0100 | <ski> | no problem, alguem :) |
2023-11-11 17:10:40 +0100 | <mauke> | re: message history, this channel specifically has public logs |
2023-11-11 17:11:33 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800::302a) |
2023-11-11 17:12:07 +0100 | <ski> | yea, check the topic. on Libera, it's policy that channels are supposed to mention in topic when there's publicly available logging |
2023-11-11 17:12:32 +0100 | <ph88> | does optparse-applicative support nested commands? like ./app command1 commandA --flag ? |
2023-11-11 17:14:07 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 246 seconds) |
2023-11-11 17:15:36 +0100 | Guest65 | (~Guest65@45.163.64.23) (Quit: Client closed) |
2023-11-11 17:18:38 +0100 | <ph88> | i think i found my answer here https://github.com/pcapriotti/optparse-applicative/issues/296#issuecomment-375837196 will try |
2023-11-11 17:20:37 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 17:21:24 +0100 | auri | (~auri@fsf/member/auri) () |
2023-11-11 17:24:04 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2023-11-11 17:24:38 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
2023-11-11 17:26:43 +0100 | xff0x | (~xff0x@2405:6580:b080:900:ad36:3751:9aba:5ce7) (Ping timeout: 246 seconds) |
2023-11-11 17:27:56 +0100 | xff0x | (~xff0x@2405:6580:b080:900:fcad:32c3:a424:90e2) |
2023-11-11 17:29:06 +0100 | <EvanR> | barendregt "lambda calculus with types" goes over many lambda calculi with types, one that is not mentioned in the lambda cube is "lambda-intersection" which is like simply typed lambda calculus with intersection types. Ok. Conspicuously missing is a lambda calculus with unions. Is it because that makes no sense? Or it makes sense but is too complicated? |
2023-11-11 17:30:17 +0100 | <ski> | it can make sense, if you have (labelled, light-weight) variant types |
2023-11-11 17:30:26 +0100 | ystael | (~ystael@user/ystael) |
2023-11-11 17:31:11 +0100 | auri | (~auri@fsf/member/auri) |
2023-11-11 17:31:40 +0100 | <EvanR> | so while lambda intersection has syntax for taking the union of types, and then parallel juxtaposition of terms to match the intersection types, union requires labeled variant syntax? |
2023-11-11 17:31:46 +0100 | <ski> | intersection of two record types could involve intersection of the field types, and if one field is a function type, that could in turn take union of corresponding argument types, i think ? |
2023-11-11 17:32:35 +0100 | <EvanR> | i meant to say, taking the intersection of types |
2023-11-11 17:32:39 +0100 | <ski> | i dunno, haven't seen this particular "lambda-intersection" system |
2023-11-11 17:32:54 +0100 | <EvanR> | it seems pretty funky |
2023-11-11 17:33:12 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 17:33:50 +0100 | <EvanR> | the gimmick being, term has type A and B both |
2023-11-11 17:34:50 +0100 | <EvanR> | 3|'a' : Int intersect Char, aiui |
2023-11-11 17:37:02 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
2023-11-11 17:37:07 +0100 | edmundnoble_ | (sid229620@id-229620.helmsley.irccloud.com) (Server closed connection) |
2023-11-11 17:37:16 +0100 | edmundnoble_ | (sid229620@id-229620.helmsley.irccloud.com) |
2023-11-11 17:38:31 +0100 | <ski> | ah, i guess i've not seen this `... | ...' |
2023-11-11 17:40:34 +0100 | CiaoSen | (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
2023-11-11 17:41:31 +0100 | <EvanR> | there's also a special type omega, and you can say any term : omega |
2023-11-11 17:42:01 +0100 | <EvanR> | I guess that stands for any |
2023-11-11 17:42:03 +0100 | <ski> | yea, the neutral element of intersection |
2023-11-11 17:45:19 +0100 | johnw | (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
2023-11-11 17:48:44 +0100 | <ncf> | wouldn't 3|'a' just be an element of a pair type |
2023-11-11 17:49:01 +0100 | <EvanR> | yeah I probably misunderstand something |
2023-11-11 17:50:22 +0100 | bliminse | (~bliminse@user/bliminse) (Ping timeout: 258 seconds) |
2023-11-11 17:50:49 +0100 | stiell | (~stiell@gateway/tor-sasl/stiell) |
2023-11-11 17:51:30 +0100 | <ph88> | how can i make a mutable integer? it's supposed to be 1 first time the function gets called and +1 after |
2023-11-11 17:52:08 +0100 | <ski> | `IORef Int' ? |
2023-11-11 17:52:15 +0100 | <ph88> | thanks ! |
2023-11-11 17:53:24 +0100 | <ph88> | ski, maybe something else? With IORef i have to pass in the ref to the function i think |
2023-11-11 17:53:27 +0100 | <ski> | i guess it would be commutative, ncf |
2023-11-11 17:53:34 +0100 | oo_miguel | (~Thunderbi@78-11-179-96.static.ip.netia.com.pl) |
2023-11-11 17:53:40 +0100 | <ski> | ph88 : not if the function is declared in a local scope |
2023-11-11 17:54:01 +0100 | <EvanR> | STRef Int ? |
2023-11-11 17:55:09 +0100 | alp_ | (~alp@2001:861:5e02:eff0:fc3a:5bf6:1b0e:f883) |
2023-11-11 17:55:22 +0100 | <ski> | @wiki Top level mutable state |
2023-11-11 17:55:22 +0100 | <lambdabot> | https://wiki.haskell.org/Top_level_mutable_state |
2023-11-11 17:55:27 +0100 | <ski> | might be interesting, ph88 ? |
2023-11-11 17:56:21 +0100 | <ph88> | looks good, thanks guys |
2023-11-11 17:56:39 +0100 | ski | would tend to opt for "Proposal 1: Don't do that", though |
2023-11-11 17:56:39 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
2023-11-11 17:57:02 +0100 | <EvanR> | what's wrong with taking IORef Int as an argument |
2023-11-11 17:57:33 +0100 | <EvanR> | or the application's entire context record |
2023-11-11 17:58:02 +0100 | CiaoSen | (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) (Ping timeout: 258 seconds) |
2023-11-11 17:59:06 +0100 | <EvanR> | ok I must have seen this pipe thing somewhere entirely else on a different subject, barendregt's lambda-intersection has no pipe thing |
2023-11-11 17:59:07 +0100 | mechap | (~mechap@user/mechap) (Ping timeout: 255 seconds) |
2023-11-11 18:14:44 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
2023-11-11 18:22:33 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
2023-11-11 18:31:15 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
2023-11-11 18:31:30 +0100 | tired | (~tired@user/tired) (Server closed connection) |
2023-11-11 18:31:32 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
2023-11-11 18:31:54 +0100 | tired | (~tired@user/tired) |
2023-11-11 18:39:02 +0100 | idgaen | (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
2023-11-11 18:45:43 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-11-11 18:45:46 +0100 | Lycurgus | (~georg@li1192-118.members.linode.com) |
2023-11-11 18:45:46 +0100 | Lycurgus | (~georg@li1192-118.members.linode.com) (Changing host) |
2023-11-11 18:45:46 +0100 | Lycurgus | (~georg@user/Lycurgus) |
2023-11-11 18:47:45 +0100 | dsrt^ | (~cd@76.145.193.217) |
2023-11-11 18:48:12 +0100 | Guest17 | (~Guest17@2401:4900:80a9:b778::243:ecc0) |
2023-11-11 18:48:23 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-11 18:48:29 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 252 seconds) |
2023-11-11 18:48:49 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) |
2023-11-11 18:48:50 +0100 | <Guest17> | A question about Haskell diagrams: can one change an attribute, like the colour, of a subdiagram, possibly by referring to its name? |
2023-11-11 18:52:38 +0100 | <tomsmeding> | Umeaboy: not sure, something in the ghc build process has gone wrong to make that symlink cycle. But it might also be due to incorrect configuration; I know little about custom ghc builds, but perhaps you entered some path in some configuration where you incorrectly interpreted what path ought to go there? (Or the documentation was inaccurate, of course.) |
2023-11-11 18:53:27 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
2023-11-11 18:53:27 +0100 | <ncf> | Guest17: what's a haskell diagram? |
2023-11-11 18:53:58 +0100 | <Guest17> | The Haskell Diagrams package |
2023-11-11 18:59:23 +0100 | <EvanR> | diagrams, it's great |
2023-11-11 18:59:35 +0100 | <EvanR> | SICP picture language on acid |
2023-11-11 19:00:03 +0100 | <EvanR> | well this is haskell so, on base |
2023-11-11 19:03:06 +0100 | marinelli | (~weechat@gateway/tor-sasl/marinelli) |
2023-11-11 19:03:52 +0100 | Guest17 | (~Guest17@2401:4900:80a9:b778::243:ecc0) (Ping timeout: 250 seconds) |
2023-11-11 19:05:26 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
2023-11-11 19:07:11 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 252 seconds) |
2023-11-11 19:08:25 +0100 | YuutaW | (~YuutaW@mail.yuuta.moe) |
2023-11-11 19:08:36 +0100 | MelanieMalik | (ellenor@callbox.trd.is) (Ping timeout: 240 seconds) |
2023-11-11 19:10:07 +0100 | SrPx | (sid108780@id-108780.uxbridge.irccloud.com) (Server closed connection) |
2023-11-11 19:10:51 +0100 | SrPx | (sid108780@id-108780.uxbridge.irccloud.com) |
2023-11-11 19:11:21 +0100 | Guest17 | (~Guest17@2401:4900:80a9:b778::243:ecc0) |
2023-11-11 19:11:40 +0100 | edm | (sid147314@id-147314.hampstead.irccloud.com) (Server closed connection) |
2023-11-11 19:12:10 +0100 | edm | (sid147314@id-147314.hampstead.irccloud.com) |
2023-11-11 19:13:42 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2023-11-11 19:13:53 +0100 | notzmv | (~zmv@user/notzmv) |
2023-11-11 19:16:55 +0100 | turlando | (~turlando@user/turlando) (Server closed connection) |
2023-11-11 19:17:11 +0100 | turlando | (~turlando@user/turlando) |
2023-11-11 19:17:15 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 260 seconds) |
2023-11-11 19:18:53 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-11 19:19:15 +0100 | <monochrom> | Neeeeaaat, 9.4.8 has -split-sections for Windows too. Finally! |
2023-11-11 19:20:39 +0100 | trev | (~trev@user/trev) (Quit: trev) |
2023-11-11 19:20:57 +0100 | trev | (~trev@user/trev) |
2023-11-11 19:21:58 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
2023-11-11 19:23:48 +0100 | Guest17 | (~Guest17@2401:4900:80a9:b778::243:ecc0) (Ping timeout: 250 seconds) |
2023-11-11 19:24:05 +0100 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
2023-11-11 19:24:26 +0100 | alp_ | (~alp@2001:861:5e02:eff0:fc3a:5bf6:1b0e:f883) (Remote host closed the connection) |
2023-11-11 19:24:31 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2023-11-11 19:24:44 +0100 | alp_ | (~alp@2001:861:5e02:eff0:d2d5:46e1:ee50:3986) |
2023-11-11 19:29:07 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
2023-11-11 19:29:27 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-11 19:30:11 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
2023-11-11 19:30:16 +0100 | edwardk | (sid47016@haskell/developer/edwardk) (Server closed connection) |
2023-11-11 19:30:26 +0100 | edwardk | (sid47016@haskell/developer/edwardk) |
2023-11-11 19:30:54 +0100 | <ph88> | how can i match on an entire record? i tried this syntax r@{..} |
2023-11-11 19:32:07 +0100 | <EvanR> | r@TheConstructor{} would match |
2023-11-11 19:33:15 +0100 | <EvanR> | to write .. you need RecordWildcards |
2023-11-11 19:33:19 +0100 | <ph88> | got it :D |
2023-11-11 19:33:54 +0100 | <EvanR> | which introduces things invisibly into scope... |
2023-11-11 19:34:44 +0100 | alp_ | (~alp@2001:861:5e02:eff0:d2d5:46e1:ee50:3986) (Ping timeout: 255 seconds) |
2023-11-11 19:37:00 +0100 | <EvanR> | if you use NamedFieldPuns instead, you can easily denote the fields you wanted to use |
2023-11-11 19:37:21 +0100 | CiaoSen | (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
2023-11-11 19:38:03 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 19:42:06 +0100 | <geekosaur> | if you don't need to specify the constructor, why not just: r |
2023-11-11 19:42:31 +0100 | <geekosaur> | unless you want some fields from it as well, in which case NamedFieldPuns is your friend |
2023-11-11 19:48:44 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-11 20:13:09 +0100 | <ph88> | real world haskell example uses json web token https://github.com/nodew/haskell-realworld-example/blob/master/src/Conduit/JWT.hs i have just a simple client-server setup should i use jwt to make things future proof or better to use some alternative ? |
2023-11-11 20:13:43 +0100 | <ph88> | geekosaur EvanR thanks was not up to date yet with NamedFieldPuns |
2023-11-11 20:18:02 +0100 | neceve | (~neceve@user/neceve) |
2023-11-11 20:19:03 +0100 | ania123 | (~ania123@wl-pool2-ont-004.uni-muenster.de) |
2023-11-11 20:21:46 +0100 | <ania123> | does anyone can me point a paper where this problem is studied: https://math.stackexchange.com/questions/42210/number-of-ways-of-partitioning-a-sum-into-ordered-n… |
2023-11-11 20:22:42 +0100 | <geekosaur> | sounds like a question for ##math to me? |
2023-11-11 20:24:29 +0100 | <ania123> | haskell community love math |
2023-11-11 20:24:46 +0100 | <geekosaur> | true, but not necessarily number theory which this sounds like |
2023-11-11 20:24:53 +0100 | <geekosaur> | there's a lot of kinds of math |
2023-11-11 20:26:23 +0100 | <monochrom> | I never understood that logic. Those who like to discuss math are already in ##math. Therefore, regardless of whether I love math, if I am not there then it clearly means I don't want to talk about it. Therefore, why are you disturbing my peace? |
2023-11-11 20:26:59 +0100 | <monochrom> | OK that's a rhetorical question. I know the answer of course. Because you think the world owes it to you. |
2023-11-11 20:27:33 +0100 | <int-e> | they did ask on ##math, FWIW |
2023-11-11 20:29:35 +0100 | kimiamania46 | (~b4f4a2ab@user/kimiamania) (Ping timeout: 260 seconds) |
2023-11-11 20:31:01 +0100 | <ph88> | how is one supposed to do cookie based authentication with servant these days? i found this package with a topic from 2018 where people ask to make it work with newer servant versions https://github.com/zohl/servant-auth-cookie/issues/48 |
2023-11-11 20:32:35 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 20:35:39 +0100 | euleritian | (~euleritia@dynamic-046-114-200-127.46.114.pool.telefonica.de) (Ping timeout: 260 seconds) |
2023-11-11 20:36:22 +0100 | <ddellacosta> | ph88: I'm looking at the docs here: https://docs.servant.dev/en/stable/tutorial/Authentication.html#generalized-authentication-in-action ...and while I haven't dug too deep, it seems like they implement a cookie-based authentication scheme without servant-auth-cookie, unless I'm missing something. Have you tried building on the approach laid out there? |
2023-11-11 20:36:55 +0100 | chymera | (~chymera@ns1000526.ip-51-81-46.us) (Server closed connection) |
2023-11-11 20:37:10 +0100 | chymera | (~chymera@ns1000526.ip-51-81-46.us) |
2023-11-11 20:38:50 +0100 | <ph88> | ddellacosta, it's just an example not a full implementation. I look for more batteries included like web frameworks in other languages |
2023-11-11 20:39:39 +0100 | fweht | (uid404746@id-404746.lymington.irccloud.com) |
2023-11-11 20:41:41 +0100 | <ph88> | for example https://symfony.com/doc/current/security.html it has all of the stuff you want out of the box |
2023-11-11 20:44:24 +0100 | <ph88> | maybe i should move from servant to another haskell framework which offers more, but which one ? |
2023-11-11 20:44:40 +0100 | <ddellacosta> | ph88: I see, in that case have you checked out IHP? https://ihp.digitallyinduced.com/ |
2023-11-11 20:45:02 +0100 | <ddellacosta> | I don't know enough about that or symfony to compare, but sounds more like what you're looking for |
2023-11-11 20:46:53 +0100 | <ddellacosta> | also fwiw, since I was poking at it already, there's a number of other examples of servant apps here: https://github.com/haskell-servant/servant/blob/master/doc/examples.md, with some more cookie examples like https://github.com/FlogFr/FlashCard/blob/master/src/Auth.hs |
2023-11-11 20:47:51 +0100 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Ping timeout: 240 seconds) |
2023-11-11 20:48:34 +0100 | Pickchea | (~private@user/pickchea) |
2023-11-11 20:49:47 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
2023-11-11 20:50:00 +0100 | <ph88> | ddellacosta, thanks ! |
2023-11-11 20:51:02 +0100 | <ddellacosta> | ph88: sure thing, I hope you find what you're looking for |
2023-11-11 20:51:07 +0100 | kimiamania46 | (~b4f4a2ab@user/kimiamania) |
2023-11-11 20:52:46 +0100 | <ddellacosta> | ph88: oh and I would be remiss to not mention yesod, which is older but more mature and similarly full featured: https://www.yesodweb.com/ |
2023-11-11 20:59:27 +0100 | Square | (~Square@user/square) (Ping timeout: 260 seconds) |
2023-11-11 21:01:03 +0100 | Batzy | (~quassel@user/batzy) (Quit: No Ping reply in 180 seconds.) |
2023-11-11 21:02:15 +0100 | <ph88> | it seems i should either use yesod or ihp |
2023-11-11 21:02:30 +0100 | Batzy | (~quassel@user/batzy) |
2023-11-11 21:06:21 +0100 | <monochrom> | yesod is s/batteries/kitchen sink/ |
2023-11-11 21:06:54 +0100 | Inst | (~Inst@120.244.192.250) (Ping timeout: 255 seconds) |
2023-11-11 21:08:11 +0100 | CiaoSen | (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) (Ping timeout: 252 seconds) |
2023-11-11 21:08:54 +0100 | Sgeo | (~Sgeo@user/sgeo) |
2023-11-11 21:10:50 +0100 | Ellenor | (~Ellenor@callbox.trd.is) |
2023-11-11 21:11:54 +0100 | trev | (~trev@user/trev) (Quit: trev) |
2023-11-11 21:14:07 +0100 | delyan_ | (sid523379@id-523379.hampstead.irccloud.com) (Server closed connection) |
2023-11-11 21:14:24 +0100 | delyan_ | (sid523379@id-523379.hampstead.irccloud.com) |
2023-11-11 21:15:56 +0100 | myxos | (~myxos@cpe-65-28-251-121.cinci.res.rr.com) (Server closed connection) |
2023-11-11 21:16:39 +0100 | myxos | (~myxos@cpe-65-28-251-121.cinci.res.rr.com) |
2023-11-11 21:20:19 +0100 | haasn | (sid579015@id-579015.hampstead.irccloud.com) (Server closed connection) |
2023-11-11 21:20:29 +0100 | haasn | (sid579015@id-579015.hampstead.irccloud.com) |
2023-11-11 21:22:51 +0100 | hiredman | (~hiredman@frontier1.downey.family) (Server closed connection) |
2023-11-11 21:23:02 +0100 | hiredman | (~hiredman@frontier1.downey.family) |
2023-11-11 21:28:31 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2023-11-11 21:32:59 +0100 | Ellenor | MelanieMalik |
2023-11-11 21:34:11 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2023-11-11 21:50:50 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
2023-11-11 21:55:35 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
2023-11-11 21:56:00 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-11-11 21:58:53 +0100 | <Unicorn_Princess> | when haddock documenting records, fourmolu keeps changing -- | to -- ^ and moving them, so the comment comes after, instead of before, the record. how can i get it to not do that? none of the options in https://fourmolu.github.io/config/ seem to be what i want |
2023-11-11 21:59:03 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
2023-11-11 21:59:22 +0100 | mc47 | (~mc47@xmonad/TheMC47) |
2023-11-11 22:01:49 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
2023-11-11 22:04:25 +0100 | <monochrom> | Fork again? fourmolu is already a fork from ormolu just to customize spacing. |
2023-11-11 22:09:04 +0100 | <yushyin> | 'We encourage any contributions which add further flexibility.' i guess this means, PRs welcome? :) |
2023-11-11 22:17:56 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
2023-11-11 22:20:48 +0100 | ania123 | (~ania123@wl-pool2-ont-004.uni-muenster.de) (Quit: Client closed) |
2023-11-11 22:20:50 +0100 | Katarushisu1 | (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
2023-11-11 22:22:28 +0100 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 260 seconds) |
2023-11-11 22:23:25 +0100 | Katarushisu1 | (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
2023-11-11 22:24:53 +0100 | rye|53 | (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) |
2023-11-11 22:24:58 +0100 | <monochrom> | To be sure, fork-then-PR is still nicer than just fork. :) |
2023-11-11 22:25:19 +0100 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
2023-11-11 22:25:50 +0100 | rye|5376 | (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) |
2023-11-11 22:25:52 +0100 | rye|5376 | (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) (Client Quit) |
2023-11-11 22:31:22 +0100 | Lycurgus | (~georg@user/Lycurgus) |
2023-11-11 22:31:38 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
2023-11-11 22:33:07 +0100 | <EvanR> | in the untyped lambda calculus, the question of whether some term has a beta normal form is undecidable. When that LC is equipped with a simple type system + intersection types but not an omega type, then a term can be typed if and only if it is strongly normalizing. Which means type inference in that case is undecidable |
2023-11-11 22:33:46 +0100 | <EvanR> | in the relevant subset of haskell, type inference is decidable. But haskell doesn't have the intersection types. |
2023-11-11 22:34:34 +0100 | rye|53 | (~rye|53@wsip-184-176-159-132.ph.ph.cox.net) (Quit: Connection closed) |
2023-11-11 22:34:51 +0100 | <EvanR> | weird! |
2023-11-11 22:35:43 +0100 | <monochrom> | With just a simple type system, type inference is decidable too. |
2023-11-11 22:37:14 +0100 | <monochrom> | I think simple type system + fix also has decidable type inference. |
2023-11-11 22:38:03 +0100 | <monochrom> | Haskell minus type classes (or SML) is when you have polymorphic type system + fix, and type inference is still decidable. |
2023-11-11 22:38:09 +0100 | <EvanR> | https://i.imgur.com/40ulrg8.png (simply type system + intersection - omega not shown, but M:? in that case is no) |
2023-11-11 22:38:48 +0100 | <monochrom> | Then again last time we discussed this, we reckoned that it is only a thin line between simply-typed and polymorphic. |
2023-11-11 22:39:17 +0100 | <EvanR> | my confusion on that was cleared up by this paper which makes a distinction between curry style and church style systems |
2023-11-11 22:40:09 +0100 | <monochrom> | Oh, that. |
2023-11-11 22:40:18 +0100 | <EvanR> | but anyway... the stated reasoning for simple + intersection - omega having undecidable type inference is because that would be equivalent to determining if an arbitrary term has a normal form |
2023-11-11 22:40:21 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
2023-11-11 22:40:34 +0100 | <EvanR> | because of a theorem not proven here |
2023-11-11 22:40:53 +0100 | <EvanR> | how does simple by itself avoid this fate, and get decidable type inference |
2023-11-11 22:40:55 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) (Server closed connection) |
2023-11-11 22:41:14 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) |
2023-11-11 22:41:44 +0100 | <int-e> | It's also decidable whether a term in the simply typed lambda calculus with fix has a normal form. "On the lambda Y calculus", R. Statman, Proc. 17th IEEE Symposium on Logic in Computer Science, 2002. |
2023-11-11 22:42:10 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
2023-11-11 22:42:42 +0100 | <EvanR> | STLC which usually has the type signature on the lambda variable right |
2023-11-11 22:42:57 +0100 | <EvanR> | (what barendregt calls church style) |
2023-11-11 22:43:05 +0100 | <monochrom> | I forgot which one is curry or church, but when answering beginner questions in #haskell, it is more useful to take the stance of "if your code doesn't type-check then we need not discuss its 'meaning' and consequent crackpot ideas". :) |
2023-11-11 22:43:38 +0100 | <int-e> | Hmm, it doesn't really matter whether it's Church style or Curry style... that's just syntax. |
2023-11-11 22:44:27 +0100 | <EvanR> | in curry style, you can write whatever (unannotated) lambda term you want and it's fine. Whether anyone can find a type in some type system is a separate problem, and it's a big difference |
2023-11-11 22:44:52 +0100 | <monochrom> | But I am OK with mature, learned discussions of terms that fail a certain type system because the participants are not crackpots. :) |
2023-11-11 22:44:55 +0100 | <EvanR> | and you can view haskell this way if you want |
2023-11-11 22:45:23 +0100 | <Lycurgus> | 'other crackpot ideas' refers to 'meaning'? |
2023-11-11 22:46:52 +0100 | <Lycurgus> | (understood to be a jest, just not how broad) |
2023-11-11 22:46:55 +0100 | <int-e> | EvanR: But it doesn't matter for the simply typed calculus, even if you add `fix`. |
2023-11-11 22:47:32 +0100 | <EvanR> | ... right, hence my question |
2023-11-11 22:47:55 +0100 | <monochrom> | Doesn't the omega type make sense only in the context of intersection types? |
2023-11-11 22:48:07 +0100 | <EvanR> | the premise is you don't have omega so it doesn't matter |
2023-11-11 22:48:15 +0100 | <monochrom> | Its sole purpose being to complete the type-level monoid. |
2023-11-11 22:48:21 +0100 | <int-e> | EvanR: Yeah but the answer is that there are two styles and it doesn't really matter which one you use. (And indeed I can't remember which one is which either.) |
2023-11-11 22:48:43 +0100 | <monochrom> | And I apologize for bringing up fix to muddle the issues. >:) |
2023-11-11 22:48:46 +0100 | <EvanR> | it doesn't, you can write haskell with no type annotations |
2023-11-11 22:48:52 +0100 | <EvanR> | somehow |
2023-11-11 22:49:13 +0100 | <monochrom> | Well let's say SML instead of Haskell. Type classes muddle the issues, too. |
2023-11-11 22:49:21 +0100 | <int-e> | As long as you stay in the mildly polymorphic Hindley Milner fragment... sure. |
2023-11-11 22:49:54 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) |
2023-11-11 22:50:17 +0100 | <int-e> | (And a bit of type classes doesn't hurt either. But it's not unconditional, as witnessed by rhe existence of UndecidableInstances) |
2023-11-11 22:51:00 +0100 | <EvanR> | on this hand, intersection (no omega) typability corresponds to normalization which is undecidable (in curry style!). On the other hand, haskell is decidably typable (ignoring type classes I guess) |
2023-11-11 22:51:13 +0100 | <EvanR> | (also curry style) |
2023-11-11 22:51:28 +0100 | arahael | (~arahael@21.127.96.58.static.exetel.com.au) |
2023-11-11 22:51:29 +0100 | monochrom | 's joke cube: Copenhagen vs multiple-world, Curry vs Church, big endian vs little endian. >:) |
2023-11-11 22:51:32 +0100 | <EvanR> | so where is the secret sauce disconnect |
2023-11-11 22:52:03 +0100 | ddb | (ddb@tilde.club) (Server closed connection) |
2023-11-11 22:52:22 +0100 | ddb | (ddb@tilde.club) |
2023-11-11 22:52:27 +0100 | <monochrom> | But Haskell lacks intersection types. |
2023-11-11 22:52:40 +0100 | <int-e> | EvanR: The question is what you mean by "Haskell", because that usually comes with many type system extensions that people use casually. |
2023-11-11 22:52:41 +0100 | <EvanR> | yes |
2023-11-11 22:53:01 +0100 | <EvanR> | obviously ignoring the haskell stuff that defeats type inference |
2023-11-11 22:53:07 +0100 | <int-e> | Many of which make type inference undecidable. |
2023-11-11 22:53:12 +0100 | <EvanR> | or none of what i said makes sense |
2023-11-11 22:53:37 +0100 | <int-e> | Sorry, as usual I don't know where this started. |
2023-11-11 22:54:02 +0100 | <monochrom> | The lambda cube. |
2023-11-11 22:54:16 +0100 | <monochrom> | Or maybe some lambda cube? |
2023-11-11 22:54:29 +0100 | <EvanR> | it's funny because this system isn't on the cube |
2023-11-11 22:54:36 +0100 | <Unicorn_Princess> | nvm fixed it |
2023-11-11 22:54:38 +0100 | <EvanR> | despite having this normalizing property |
2023-11-11 22:54:52 +0100 | yahb2 | (~yahb2@2a01:4f8:c0c:5c7b::2) (Server closed connection) |
2023-11-11 22:55:07 +0100 | nate3 | (~nate@c-98-45-169-16.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
2023-11-11 22:55:14 +0100 | yahb2 | (~yahb2@2a01:4f8:c0c:5c7b::2) |
2023-11-11 22:55:14 +0100 | ChanServ | +v yahb2 |
2023-11-11 22:55:31 +0100 | <EvanR> | anyway I guess my confusion is well-founded because a typability <=> normalizing property makes no sense in haskell because recursion |
2023-11-11 22:55:38 +0100 | <EvanR> | my confusiong isn't well-founded* |
2023-11-11 22:55:42 +0100 | <Unicorn_Princess> | (turns out -- |-style haddock on records is incompatible with leading comma style. setting it to trailing switched the haddock to --|-style automatically: https://fourmolu.github.io/config/comma-style/) |
2023-11-11 22:56:09 +0100 | <monochrom> | I confess that I did not study these normalizability and computability questions at all. Except ad-hoc-ly for the few systems I came across. |
2023-11-11 22:56:18 +0100 | <Unicorn_Princess> | (some github issues mentioned it, i think there's a reason it's not compatible, but here my investigation will cease) |
2023-11-11 22:57:21 +0100 | <geekosaur> | sounds like the sort of thing haddock would have opinions about |
2023-11-11 22:57:45 +0100 | <geekosaur> | -- | foo \n , foo :: X |
2023-11-11 22:58:06 +0100 | <geekosaur> | haddock probably sees the comma as separating the comment from the field |
2023-11-11 22:58:54 +0100 | <monochrom> | Yeah I think "-- |doc for the next thing" cannot make sense until after comma ends the previous thing. |
2023-11-11 22:59:31 +0100 | mht-wtf | (~mht@2a03:b0c0:3:e0::1e2:c001) (Server closed connection) |
2023-11-11 22:59:44 +0100 | mht-wtf | (~mht@mht.wtf) |
2023-11-11 22:59:44 +0100 | michalz | (~michalz@185.246.207.203) (Remote host closed the connection) |
2023-11-11 22:59:48 +0100 | <monochrom> | Then again in an ideal world comma neither ends or begins anything, it's just syntax. |
2023-11-11 22:59:48 +0100 | <int-e> | EvanR: Hmm that interesection logic claim isn't too useful anyway, because often we're not interested in the halting problem (program halts on a particular input) but in the universal halting problem instead. And I rather suspect that the proof works by extracting (potentially highly complicated) types from an actual reduction to normal form. |
2023-11-11 23:00:06 +0100 | Jackneill | (~Jackneill@20014C4E1E058A00ABC7937222D6C543.dsl.pool.telekom.hu) (Ping timeout: 258 seconds) |
2023-11-11 23:00:40 +0100 | <EvanR> | it goes both ways, so seems kind of interesting |
2023-11-11 23:01:19 +0100 | <int-e> | Oh there are plenty of interesting things that aren't very useful :-) |
2023-11-11 23:01:33 +0100 | <monochrom> | :( |
2023-11-11 23:01:40 +0100 | <EvanR> | let me see if I can put it in a form that is obviously confusing, and also obviously wrong to shrink the problem |
2023-11-11 23:01:55 +0100 | <Unicorn_Princess> | that makes sense, i am happy with this comma-explanation, thanks. i know i said investigation ceased, but it was gonna bug me |
2023-11-11 23:02:01 +0100 | arahael | (~arahael@21.127.96.58.static.exetel.com.au) (Ping timeout: 246 seconds) |
2023-11-11 23:02:07 +0100 | <monochrom> | Wait, you can't have both confusing and obviously wrong. |
2023-11-11 23:02:28 +0100 | <Unicorn_Princess> | perhaps it is only the wrongness that is obvious |
2023-11-11 23:02:40 +0100 | <int-e> | monochrom: Heh. "this is obviously wrong but I don't know why" |
2023-11-11 23:02:46 +0100 | <EvanR> | it will be confusing to me and obviously wrong to you! |
2023-11-11 23:02:56 +0100 | <monochrom> | OK I can buy that. |
2023-11-11 23:03:36 +0100 | <EvanR> | intersection no omega: has a type <=> strongly normalizing, undecidable. simple types: has a type <=> strongly normalizing, decidable |
2023-11-11 23:03:48 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
2023-11-11 23:04:37 +0100 | <monochrom> | OK that's obviously confusing but I think it's also obviously correct? :) |
2023-11-11 23:04:59 +0100 | <EvanR> | the justification for undecidable is the equivalence to checking for a normal form, which is true in both cases |
2023-11-11 23:05:18 +0100 | <EvanR> | but this justification doesn't work for simple types because it's decidable after all |
2023-11-11 23:06:24 +0100 | <EvanR> | so why would the justification ever work |
2023-11-11 23:06:51 +0100 | <int-e> | EvanR: where does "has a type <=> strongly normalizing" come from? |
2023-11-11 23:06:59 +0100 | <EvanR> | for intersection? |
2023-11-11 23:07:07 +0100 | <int-e> | No for simple types, where it's demonstrably false. |
2023-11-11 23:07:16 +0100 | urdh | (~urdh@user/urdh) (Server closed connection) |
2023-11-11 23:07:27 +0100 | <int-e> | That, or vacuously true. |
2023-11-11 23:07:28 +0100 | <EvanR> | is it? then that was the "obviously wrong" part |
2023-11-11 23:07:39 +0100 | <int-e> | s/vacuously/trivially/ |
2023-11-11 23:07:40 +0100 | urdh | (~urdh@user/urdh) |
2023-11-11 23:07:46 +0100 | <EvanR> | is it trivially true or trivially false? |
2023-11-11 23:08:16 +0100 | <int-e> | It depends on whether you start with terms of the simply typed lambda calculus, which all have a type and are all strongly normalizing |
2023-11-11 23:08:24 +0100 | <monochrom> | TIme to also introduce "obviously paradoxical" >:) |
2023-11-11 23:08:57 +0100 | <EvanR> | the table I showed shows that type inference for STLC (curry style) is decidable, but I thought the strongly normalizing property carried over, maybe not |
2023-11-11 23:09:11 +0100 | <EvanR> | could be the key |
2023-11-11 23:09:13 +0100 | <int-e> | Or whether you consider terms of the untyped lambda calculus, which can be strongly normalizing (undecidable) and/or typeable in the simply typed lambda calculus (which is decidable), and those two notions aren't the same. |
2023-11-11 23:09:54 +0100 | <EvanR> | i thought the result was if it could be ascribed a simply typed type it's normalizing to something |
2023-11-11 23:09:54 +0100 | <int-e> | You only have an implication (typeable implies strongly normalizing). |
2023-11-11 23:10:10 +0100 | <EvanR> | so you're saying it's one way not both ways |
2023-11-11 23:10:23 +0100 | <geekosaur> | are we talking about the same kind of normalizing? |
2023-11-11 23:10:24 +0100 | <int-e> | you can write down a normal form \x. x x which isn't typeable. |
2023-11-11 23:10:46 +0100 | <EvanR> | ok! |
2023-11-11 23:11:05 +0100 | xigua | (~xigua@user/xigua) (Remote host closed the connection) |
2023-11-11 23:11:09 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2023-11-11 23:11:23 +0100 | <int-e> | (aside, how does that type with intersection types?) |
2023-11-11 23:11:40 +0100 | xigua | (~xigua@user/xigua) |
2023-11-11 23:11:43 +0100 | <EvanR> | it has a type, I can tell you once I get an intersection symbol off unicode site |
2023-11-11 23:11:43 +0100 | int-e | doesn't know how intersection types work. |
2023-11-11 23:12:07 +0100 | <EvanR> | but, x has type tau -> sigma, and also type tau |
2023-11-11 23:12:12 +0100 | <EvanR> | intersect those |
2023-11-11 23:12:19 +0100 | <tomsmeding> | EvanR: https://tomsmeding.com/unicode#intersec |
2023-11-11 23:12:24 +0100 | <monochrom> | ∩ |
2023-11-11 23:12:36 +0100 | <tomsmeding> | or wait until monochrom turns up |
2023-11-11 23:13:07 +0100 | <EvanR> | \x . x x : ((a -> b) ∩ a) -> b |
2023-11-11 23:14:14 +0100 | <EvanR> | so x is a hyperfunction or something xD |
2023-11-11 23:14:15 +0100 | <int-e> | Oh so you kind of defer unification (including its potential to fail). |
2023-11-11 23:15:07 +0100 | <EvanR> | unification? type inference is undecidable as we saw earlier |
2023-11-11 23:16:18 +0100 | <EvanR> | the normal typing rule for function application combined with a rule that says x has type a and type a -> b lets you prove that typing |
2023-11-11 23:16:19 +0100 | <int-e> | I mean, where you have (a -> b) ∩ a, the simply typed lambda calculus would unify a -> b and a. |
2023-11-11 23:16:34 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Server closed connection) |
2023-11-11 23:16:51 +0100 | <tomsmeding> | EvanR: how do I construct a value of type (a -> b) ∩ a |
2023-11-11 23:16:55 +0100 | <EvanR> | hmm... I don't know about that. Maybe you're talking about HM |
2023-11-11 23:17:02 +0100 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) |
2023-11-11 23:17:02 +0100 | <int-e> | besides, you can ask about unifiers even when that problem isn't decidable. |
2023-11-11 23:17:16 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2023-11-11 23:17:42 +0100 | <EvanR> | a type that is both a and a -> b, well that's a ∩ (a -> b) |
2023-11-11 23:17:46 +0100 | <EvanR> | tomsmeding, in haskell? |
2023-11-11 23:18:05 +0100 | <tomsmeding> | well haskell doesn't have intersection types, but haskell syntax might be nice for understandability :p |
2023-11-11 23:18:20 +0100 | <EvanR> | cue the hyperfunction guru for an example |
2023-11-11 23:18:25 +0100 | <tomsmeding> | like, what is the typing rule that introduces ∩ |
2023-11-11 23:18:42 +0100 | <EvanR> | if x : t1 and x : t2, then you can have x : t1 ∩ t2 |
2023-11-11 23:18:51 +0100 | <tomsmeding> | I get how the typing rule for application looks into the arguments of ∩ to see if there's a function type in there somewhere |
2023-11-11 23:18:58 +0100 | <tomsmeding> | oh |
2023-11-11 23:18:59 +0100 | <tomsmeding> | right |
2023-11-11 23:19:12 +0100 | <tomsmeding> | ew |
2023-11-11 23:19:15 +0100 | <EvanR> | lol |
2023-11-11 23:19:33 +0100 | <EvanR> | apparently this stuff is all the rage in typescript |
2023-11-11 23:19:42 +0100 | tomsmeding | scurries back to more normal type systems |
2023-11-11 23:20:03 +0100 | <monochrom> | It is possible that you can justify that a second copy of (\x. x x) has type (a -> b) ∩ a. |
2023-11-11 23:20:47 +0100 | <tomsmeding> | yeah like how would that typing derivation even look |
2023-11-11 23:20:50 +0100 | <ski> | $ ocaml -rectypes |
2023-11-11 23:20:56 +0100 | <ski> | # fun x -> x x;; |
2023-11-11 23:21:01 +0100 | <ski> | - : ('a -> 'b as 'a) -> 'b = <fun> |
2023-11-11 23:21:14 +0100 | <geekosaur> | we're talking about lambda calculus, no? I thought little things like actually producing values weren't relevant? |
2023-11-11 23:21:15 +0100 | <monochrom> | Nevermind, non-normalizing terms cannot be typed. (\x. x x)(\x. x x) is supposed to be illegal. |
2023-11-11 23:21:22 +0100 | <EvanR> | tomsmeding, exercise for the reader, or check this paper out xD |
2023-11-11 23:21:27 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2023-11-11 23:22:13 +0100 | <monochrom> | OK, it is possible that no term has type (a -> b) ∩ a. This doesn't stop (\x. x x) from wanting such a parameter. |
2023-11-11 23:22:32 +0100 | <tomsmeding> | right |
2023-11-11 23:22:38 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
2023-11-11 23:22:43 +0100 | <EvanR> | tomsmeding, but when checking the inside of the lambda... you have x : (a -> b) ∩ a in context, then you can use another rule which says you get x : a -> b and x : a |
2023-11-11 23:22:59 +0100 | <int-e> | (\x. x x) (\x. x) would be legal though. So you'll derive (\x. x) : (a -> b) ∩ a for some a and b. a = b = c -> c works, right? |
2023-11-11 23:23:06 +0100 | <monochrom> | Humans suffer the same problem too. "I want fast and cheap and good" always happens. It is never fulfilled. :) |
2023-11-11 23:23:39 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) |
2023-11-11 23:24:15 +0100 | <tomsmeding> | EvanR: is that about type-checking (\x. x x) : ((a -> b) ∩ a) -> b ? I get that :p |
2023-11-11 23:24:21 +0100 | <tomsmeding> | it's how to produce anything with type (a -> b) ∩ a |
2023-11-11 23:24:30 +0100 | <int-e> | tomsmeding: see what I just wrote? |
2023-11-11 23:24:50 +0100 | <tomsmeding> | oh heh |
2023-11-11 23:24:52 +0100 | <tomsmeding> | yes |
2023-11-11 23:24:52 +0100 | <int-e> | it's not *that* type but it's an instance of that type. |
2023-11-11 23:25:28 +0100 | <tomsmeding> | "a function that you can apply to itself and get something (a 'b')" |
2023-11-11 23:25:37 +0100 | <tomsmeding> | an example of which is... id |
2023-11-11 23:25:46 +0100 | <tomsmeding> | this was not very enlightening |
2023-11-11 23:25:48 +0100 | <EvanR> | a couple days ago someone was doing hyperfunctions in here which I think is this |
2023-11-11 23:25:48 +0100 | <int-e> | :t const const |
2023-11-11 23:25:49 +0100 | <lambdabot> | b1 -> a -> b2 -> a |
2023-11-11 23:25:51 +0100 | <EvanR> | and a blog post to go with it |
2023-11-11 23:25:58 +0100 | <EvanR> | because "they're super useful" |
2023-11-11 23:26:21 +0100 | <EvanR> | https://doisinkidney.com/posts/2021-03-14-hyperfunctions.html |
2023-11-11 23:26:39 +0100 | <EvanR> | shoot no, they reverse the arguments |
2023-11-11 23:27:04 +0100 | <EvanR> | so a ∩ (b -> a) |
2023-11-11 23:27:12 +0100 | yoyofreeman | (~yoyofreem@176.97.76.178) (Remote host closed the connection) |
2023-11-11 23:27:30 +0100 | <EvanR> | no |
2023-11-11 23:27:44 +0100 | <int-e> | Sometimes people see a single use case that's important to them and a tool that they think would fit that use case, and suddenly that tool becomes "super useful". |
2023-11-11 23:27:44 +0100 | <EvanR> | yes |
2023-11-11 23:27:53 +0100 | yoyofreeman | (~yoyofreem@176.97.76.178) |
2023-11-11 23:27:54 +0100 | <EvanR> | also yes |
2023-11-11 23:28:35 +0100 | <int-e> | (Been there, done that. It's an easy trap to fall into.) |
2023-11-11 23:28:49 +0100 | <EvanR> | (a -> b) ∩ ((b -> a) -> b) |
2023-11-11 23:28:50 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2023-11-11 23:29:34 +0100 | <monochrom> | Oh may I introduce you to the Giry monad, it's super useful... https://www.cs.utoronto.ca/~trebla/cpm.pdf >:) |
2023-11-11 23:30:08 +0100 | <monochrom> | But generally, s/Sometimes/Always/ |
2023-11-11 23:30:32 +0100 | <monochrom> | But we can do worse. |
2023-11-11 23:30:48 +0100 | arahael | (~arahael@21.127.96.58.static.exetel.com.au) |
2023-11-11 23:31:09 +0100 | <exarkun> | typo in the citation, "probabaility" |
2023-11-11 23:31:16 +0100 | <monochrom> | Just last night, someone asked about readability, and it soon turned out that clearly they just want other people to say yes to "exclusively only my favourite style is readable". |
2023-11-11 23:31:22 +0100 | Pickchea | (~private@user/pickchea) (Quit: Leaving) |
2023-11-11 23:32:07 +0100 | <tomsmeding> | okay I proved (? with some imagined typing rules that seem reasonable) that (\x. x x) : ∀a b. ((a -> b) -> b) ∩ (a -> b) |
2023-11-11 23:32:32 +0100 | <monochrom> | exarkun: :( |
2023-11-11 23:32:57 +0100 | <tomsmeding> | if you start with (a -> b) ∩ a and try to apply typing rules you're forced to refine the type to this |
2023-11-11 23:33:18 +0100 | <EvanR> | oh you got forall now? xD |
2023-11-11 23:33:36 +0100 | <EvanR> | that's a whole nother thing |
2023-11-11 23:33:40 +0100 | gmg | (~user@user/gehmehgeh) (Ping timeout: 264 seconds) |
2023-11-11 23:33:42 +0100 | <tomsmeding> | just wanna be explicit :p |
2023-11-11 23:33:54 +0100 | <tomsmeding> | it's not like it doesn't mean the same thing if I remove the forall |
2023-11-11 23:34:05 +0100 | <tomsmeding> | yes, triple negation, deal with it |
2023-11-11 23:34:06 +0100 | <EvanR> | semantics! |
2023-11-11 23:34:43 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d0e6:54a3:ea5c:7672) (Remote host closed the connection) |
2023-11-11 23:35:07 +0100 | <monochrom> | Fortunately negation is self-adjoint so triple negation is simplifiable to single negation. |
2023-11-11 23:35:17 +0100 | <tomsmeding> | er no my proof is bonkers |
2023-11-11 23:35:26 +0100 | <tomsmeding> | scratch that |
2023-11-11 23:35:53 +0100 | <tomsmeding> | okay sorry my brain is not ready for this, I'm off to bed |
2023-11-11 23:36:09 +0100 | <monochrom> | Calculus of Constructions is so much simpler. :) |
2023-11-11 23:37:01 +0100 | <EvanR> | also if you're using the exact system barendregt says, you have this if x : t and t ≤ u, you can have x : u |
2023-11-11 23:37:11 +0100 | <EvanR> | which might let you simplify something |
2023-11-11 23:37:12 +0100 | <int-e> | EvanR: that post reminds me of this silly trick: https://paste.tomsmeding.com/VxiOKUN7 |
2023-11-11 23:38:04 +0100 | <monochrom> | That was what I brought up last time. :) |
2023-11-11 23:38:15 +0100 | <EvanR> | that looks like a ∩ (a -> b) if I ever seen one |
2023-11-11 23:38:18 +0100 | <int-e> | Oh no, am I becoming monochrom? |
2023-11-11 23:38:30 +0100 | <monochrom> | We are entangled! |
2023-11-11 23:38:57 +0100 | accord | (uid568320@id-568320.hampstead.irccloud.com) |
2023-11-11 23:39:18 +0100 | <monochrom> | I would say it is the simpler a ≅ a -> b. |
2023-11-11 23:39:40 +0100 | <EvanR> | yeah |
2023-11-11 23:40:31 +0100 | <EvanR> | this system comes with a subtyping preorder which is probably where the real complexity comes in |
2023-11-11 23:42:29 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
2023-11-11 23:43:00 +0100 | <monochrom> | No, my experience with lattice theory is that having ≤ is implied by having ∩, so any complexity traces back to ∩ itself. |
2023-11-11 23:44:35 +0100 | <monochrom> | For example, you can rephrase that rule as: if x : foo ∩ u, then x : u. |
2023-11-11 23:44:38 +0100 | <EvanR> | well there's only 6 total typing rules and like 8 axioms of the preorder |
2023-11-11 23:45:18 +0100 | <EvanR> | that's one of the typing rules |
2023-11-11 23:50:32 +0100 | <mauke> | real complexity is an oxymoron |
2023-11-11 23:51:00 +0100 | <EvanR> | otoh real ∩ complex makes total sense! |
2023-11-11 23:51:04 +0100 | <monochrom> | Why? |
2023-11-11 23:51:10 +0100 | neceve | (~neceve@user/neceve) (Remote host closed the connection) |
2023-11-11 23:53:04 +0100 | <monochrom> | In Haskell land, real ∩ complex is called Floating. >:) |
2023-11-11 23:54:11 +0100 | <EvanR> | yes somehow corporate languages which have intersection all over their brochures seem to be talking about (ad-hoc) polymorphism, I wonder if this is simply an instance of record subtypes |
2023-11-11 23:54:15 +0100 | <monochrom> | So I'm thinking that GADTs may be able to emulate intersection types. |
2023-11-11 23:54:20 +0100 | CiaoSen | (~Jura@2a05:5800:2b0:5500:2a3a:4dff:fe84:dbd5) |
2023-11-11 23:55:23 +0100 | <monochrom> | Or closed type families can. |
2023-11-11 23:56:21 +0100 | <int-e> | monochrom: Have you seen this before? slide 5 from https://latticehacks.cr.yp.to/ ...presenter said "this is not a lattice", and apologized to the live translation team |
2023-11-11 23:57:12 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
2023-11-11 23:57:31 +0100 | <int-e> | (of course it's about a different type of lattice) |
2023-11-11 23:57:35 +0100 | <monochrom> | Eh I recongize the name Natalie Wolchover from Quanta Magazine. |
2023-11-11 23:58:16 +0100 | <monochrom> | Haha lettuce. |
2023-11-11 23:59:05 +0100 | <mauke> | I knew exactly what I was going to find on that slide :-D |
2023-11-11 23:59:25 +0100 | arahael | (~arahael@21.127.96.58.static.exetel.com.au) (Ping timeout: 246 seconds) |