Logs on 2024-01-09 (liberachat/#haskell)
| 00:00:24 | → | res0nat0r0844909 joins (~Fletch@falcon.whatbox.ca) |
| 00:05:42 | → | steew_ joins (~steew@user/steew) |
| 00:07:13 | × | steew quits (~steew@user/steew) (Ping timeout: 255 seconds) |
| 00:07:14 | steew_ | is now known as steew |
| 00:11:38 | <Axman6> | That's a little scary... |
| 00:11:54 | <Axman6> | Luckily this isn't recursive |
| 00:14:23 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 264 seconds) |
| 00:15:50 | → | Jard joins (~igork@78.84.190.186) |
| 00:16:05 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 00:18:26 | × | Tuplanolla quits (~Tuplanoll@91-159-69-171.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:20:22 | <Axman6> | @type let f <$! l = f <$> view l in (<$!) |
| 00:20:23 | <lambdabot> | MonadReader s f => (a -> b) -> Getting a s a -> f b |
| 00:22:41 | <Axman6> | @type let f <$. l = f <$> view l; f <*. l = f <*> view l in flip (,) <$. _1 <*. _2 |
| 00:22:42 | <lambdabot> | (MonadReader s f, Field1 s s b1 b1, Field2 s s b2 b2) => f (b2, b1) |
| 00:22:49 | → | Square joins (~Square@user/square) |
| 00:41:22 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.1.2) |
| 00:43:37 | × | EvanR quits (~EvanR@user/evanr) (Quit: Leaving) |
| 00:49:03 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 00:50:23 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 264 seconds) |
| 00:51:32 | × | causal quits (~eric@50.35.85.7) (Quit: WeeChat 4.1.1) |
| 00:59:12 | → | pavonia joins (~user@user/siracusa) |
| 00:59:35 | → | astrolabe joins (~astrolabe@astrolabe.plus.com) |
| 01:00:53 | × | euleritian quits (~euleritia@dynamic-089-015-238-167.89.15.238.pool.telefonica.de) (Read error: Connection reset by peer) |
| 01:01:09 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 01:02:02 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 01:02:48 | → | lingprefix joins (~lingprefi@user/lingprefix) |
| 01:02:54 | → | uiop1234 joins (~uiop1234@202.220.233.220.static.exetel.com.au) |
| 01:03:13 | × | uiop1234 quits (~uiop1234@202.220.233.220.static.exetel.com.au) (Client Quit) |
| 01:04:26 | → | uiop1234 joins (~uiop1234@202.220.233.220.static.exetel.com.au) |
| 01:06:34 | ← | uiop1234 parts (~uiop1234@202.220.233.220.static.exetel.com.au) () |
| 01:12:48 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 01:22:16 | × | mmhat quits (~mmh@p200300f1c7428268ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.1.2) |
| 01:23:04 | → | EvanR joins (~EvanR@user/evanr) |
| 01:24:36 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 01:25:21 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 01:25:59 | Lord_of_Life_ | is now known as Lord_of_Life |
| 01:26:27 | → | meritamen joins (~meritamen@user/meritamen) |
| 01:30:51 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 01:35:12 | <c_wraith> | A few days ago, I found myself wishing base had a paramorphism for []. Does it have it someplace sneaky that I'm not looking? |
| 01:38:49 | → | xff0x joins (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) |
| 01:39:36 | <Axman6> | what's a paramorphism again? |
| 01:40:17 | <c_wraith> | ok, this is really funny. I just searched to see if google knew anything, and I found a reddit thread in which.. you asked that and I answered. :) |
| 01:40:49 | Axman6 | :highfive: |
| 01:41:03 | <c_wraith> | https://www.reddit.com/r/haskell/comments/u1t237/the_visitor_pattern_and_catamorphisms/i4hycyy/ |
| 01:42:23 | <Axman6> | <3 |
| 01:44:03 | <Axman6> | I have a feeling the answer is no, at least not that Ive ever seen (though it could be doable with foldr?) |
| 01:44:30 | <c_wraith> | it's awkward to do with foldr. Possible, but it loses efficiency. |
| 01:47:46 | <c_wraith> | It looks like I only wanted it in order to write that [a] -> [(a, [a])] function that everyone keeps rewriting over and over. I guess if that was in base, I wouldn't want list paramorphisms. |
| 01:47:57 | <c_wraith> | (this time) |
| 01:54:06 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 01:55:03 | <c_wraith> | But `para (\x xs r -> (x, xs) : map (fmap (x:)) r) []' is such a nicer implementation than the alternatives if I have to keep writing it over and over... |
| 02:04:45 | <jackdk> | What is that function? Turning a list into a list of heads and tails? Seems like it's almost Data.List.NonEmpty.tails but not quite |
| 02:05:33 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 02:05:38 | <c_wraith> | Not just heads. taking every element out of the list, and returning that element and the rest of the list |
| 02:10:40 | <c_wraith> | (that fmap is prepending the element to the rest of the returned lists, which is how you get everything back) |
| 02:17:22 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 02:17:22 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 02:22:31 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 276 seconds) |
| 02:25:59 | → | sroso joins (~sroso@user/SrOso) |
| 02:27:09 | × | sroso quits (~sroso@user/SrOso) (Remote host closed the connection) |
| 02:33:19 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 02:37:24 | → | sroso joins (~sroso@user/SrOso) |
| 02:37:57 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 252 seconds) |
| 02:38:09 | → | Guest62 joins (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) |
| 02:38:40 | → | irrgit__ joins (~irrgit@146.70.27.250) |
| 02:42:18 | × | irrgit_ quits (~irrgit@89.47.234.74) (Ping timeout: 256 seconds) |
| 02:45:18 | → | rosco joins (~rosco@175.136.156.77) |
| 02:45:35 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 264 seconds) |
| 02:46:20 | × | Guest62 quits (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) (Quit: Client closed) |
| 02:49:22 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 02:55:52 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 03:02:52 | × | petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 03:03:15 | × | xff0x quits (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) (Ping timeout: 252 seconds) |
| 03:04:13 | → | petrichor joins (~znc-user@user/petrichor) |
| 03:08:18 | <c_wraith> | lens has a function named "para" that says "technically a paramorphism" and the word "technically" is sure doing a lot of work.. |
| 03:09:44 | <c_wraith> | like, yes. It is technically a paramorphism, but... it's sure a weird expression of it. |
| 03:10:40 | <c_wraith> | > para (\ls rs -> case ls of [] -> [] ; (x:xs) -> case rs of [] -> [] ; (r:_) -> (x, xs): map (fmap (x:)) r) [1..5] |
| 03:10:42 | <lambdabot> | [(1,[2,3,4,5]),(2,[1,3,4,5]),(3,[1,2,4,5]),(4,[1,2,3,5]),(5,[1,2,3,4])] |
| 03:14:44 | → | jargon joins (~jargon@211.sub-174-205-225.myvzw.com) |
| 03:15:38 | → | jargon_ joins (~jargon@211.sub-174-205-225.myvzw.com) |
| 03:15:47 | → | Guest62 joins (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) |
| 03:16:11 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 03:16:42 | × | jargon_ quits (~jargon@211.sub-174-205-225.myvzw.com) (Killed (NickServ (GHOST command used by jargon))) |
| 03:16:55 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 03:17:17 | × | jargon quits (~jargon@211.sub-174-205-225.myvzw.com) (Remote host closed the connection) |
| 03:17:48 | → | jargon joins (~jargon@211.sub-174-205-225.myvzw.com) |
| 03:19:10 | × | Guest62 quits (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) (Client Quit) |
| 03:22:28 | × | meritamen quits (~meritamen@user/meritamen) (Remote host closed the connection) |
| 03:22:29 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:604b:dee:6683:e755) (Remote host closed the connection) |
| 03:22:44 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) |
| 03:25:39 | <c_wraith> | (ok, it's not actually weird. It's generalized to be correct for any type with a correct Plated instance. But it means you do a lot of stuff by hand.) |
| 03:32:44 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 03:33:31 | → | euleritian joins (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) |
| 03:34:33 | × | zeka quits (~zeka@2600:1700:2121:180:fc1e:e1df:c7a6:218c) (Ping timeout: 268 seconds) |
| 03:35:19 | → | zeka__ joins (~zeka@2600:1700:2121:180:9966:d187:1602:11f9) |
| 03:36:09 | × | astrolabe quits (~astrolabe@astrolabe.plus.com) (Quit: Client closed) |
| 03:47:17 | × | td_ quits (~td@i53870925.versanet.de) (Ping timeout: 240 seconds) |
| 03:47:19 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 03:49:22 | → | td_ joins (~td@i53870924.versanet.de) |
| 03:52:02 | <EvanR> | this is what happens when you used discovered stuff as opposed to invented xd |
| 03:52:26 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 245 seconds) |
| 03:54:59 | → | bilegeek joins (~bilegeek@2600:1008:b0a5:5faa:ea63:51d4:70a3:2023) |
| 03:56:28 | × | Jard quits (~igork@78.84.190.186) (Remote host closed the connection) |
| 03:58:13 | → | meritamen joins (~meritamen@user/meritamen) |
| 04:01:29 | × | phma quits (~phma@2001:5b0:210d:7708:c2d8:8831:303c:d8e2) (Read error: Connection reset by peer) |
| 04:01:57 | → | phma joins (~phma@2001:5b0:210d:7708:ef47:fe3e:a28b:a600) |
| 04:04:19 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 04:06:21 | → | aforemny_ joins (~aforemny@i59F516FD.versanet.de) |
| 04:07:30 | × | aforemny quits (~aforemny@i59F516EE.versanet.de) (Ping timeout: 260 seconds) |
| 04:10:53 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 252 seconds) |
| 04:12:01 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 04:22:35 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 04:33:27 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 268 seconds) |
| 04:33:49 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 04:45:09 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 04:47:13 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 04:51:06 | × | dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Read error: Connection reset by peer) |
| 04:52:17 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 04:52:43 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 05:00:45 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 05:02:53 | → | trev joins (~trev@user/trev) |
| 05:03:06 | × | foul_owl quits (~kerry@157.97.134.167) (Ping timeout: 260 seconds) |
| 05:03:20 | × | euleritian quits (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) (Read error: Connection reset by peer) |
| 05:03:38 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 05:04:14 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 05:05:07 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 255 seconds) |
| 05:08:39 | × | rosco quits (~rosco@175.136.156.77) (Quit: Lost terminal) |
| 05:11:23 | → | alp_ joins (~alp@2001:861:e3d6:8f80:f7ce:4acc:831e:1a6e) |
| 05:15:18 | → | phma_ joins (~phma@host-67-44-208-148.hnremote.net) |
| 05:15:20 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 05:15:21 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 05:15:21 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 05:15:51 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 05:15:52 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 05:16:15 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 05:18:42 | × | phma quits (~phma@2001:5b0:210d:7708:ef47:fe3e:a28b:a600) (Ping timeout: 256 seconds) |
| 05:21:32 | phma_ | is now known as phma |
| 05:22:25 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:31:18 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 05:31:55 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 05:34:07 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 05:38:28 | <Axman6> | c_wraith: I feel like I've needed that function many times, and would love to see it in Data.List, as something like `selections`, with all the appropriate laziness like you'd get with permutations |
| 05:39:12 | <Axman6> | it's also basically list zipper... so you could maybe do something fun with lens' zipper stuff |
| 05:40:48 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 05:57:07 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 06:03:34 | × | famubu quits (~julinuser@user/famubu) (Quit: leaving) |
| 06:06:11 | × | Katarushisu1 quits (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Ping timeout: 245 seconds) |
| 06:10:23 | → | xdminsy joins (~xdminsy@117.147.71.169) |
| 06:14:03 | → | Katarushisu1 joins (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 06:14:37 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:19:38 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 06:19:55 | → | euleritian joins (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) |
| 06:20:29 | <c_wraith> | what's funny is that if you put [a] -> [(a, [a])] into hackage, you get a bunch of implementations of exactly that function |
| 06:20:38 | <c_wraith> | Including one from the ghc package! |
| 06:21:32 | → | famubu joins (~julinuser@user/famubu) |
| 06:22:05 | <famubu> | Is it possible to have a function returning a type (as in 'Int', 'Bool', etc) in haskell? By means of an extension maybe? |
| 06:22:50 | <famubu> | Like: `foo :: Int -> Type` where `foo 2` returns `Bool` and `foo 1` returns `()`. |
| 06:23:13 | → | irrgit_ joins (~irrgit@89.47.234.74) |
| 06:25:49 | <famubu> | Or even TemplateHaskell? |
| 06:25:52 | <c_wraith> | famubu: no. |
| 06:25:59 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:26:05 | × | irrgit__ quits (~irrgit@146.70.27.250) (Ping timeout: 240 seconds) |
| 06:26:09 | <c_wraith> | famubu: you can return Either Int Bool |
| 06:26:26 | <c_wraith> | But types need to be checked without knowing their runtime values |
| 06:27:01 | <c_wraith> | types exist only at compile time |
| 06:27:52 | <famubu> | Oh.. |
| 06:35:22 | → | michalz joins (~michalz@185.246.207.221) |
| 06:35:59 | → | igemnace joins (~ian@user/igemnace) |
| 06:36:06 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds) |
| 06:37:45 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 06:38:20 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 06:43:07 | <jackdk> | Can I get a show of hands of how many people are using GHC 9.8 for stuff? Want to get a sense of how urgently I need to rush out an amazonka release |
| 06:46:27 | <haskellbridge> | 05<irregularsphere> c_wraith: sorry if I'm being pedantic, but I don't think hackage can search for types? rather hoogle |
| 06:46:54 | <c_wraith> | irregularsphere: you are completely correct. I just typed the wrong thing |
| 06:48:02 | <Axman6> | famubu: you could use a type family to do that though. You are getting very close to (well actually ast) dependent types |
| 06:48:07 | <Axman6> | as* |
| 06:50:12 | <jackdk> | You could also have a type family that turns a Nat into a Type |
| 06:50:30 | <jackdk> | And a singleton to reflect a value up into the type |
| 06:54:02 | <Axman6> | GADTs might also help |
| 06:54:12 | <Axman6> | So many options! |
| 06:54:50 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:55:47 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 264 seconds) |
| 06:55:50 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:56:59 | → | foul_owl joins (~kerry@174-21-148-34.tukw.qwest.net) |
| 07:03:50 | → | acidjnk joins (~acidjnk@2003:d6:e72b:9308:1c56:4b97:a161:31b) |
| 07:08:03 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 07:08:32 | × | hexology quits (~hexology@user/hexology) (Quit: hex on you ...) |
| 07:12:41 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 07:12:50 | <probie> | jackdk: I'm using GHC 9.8, but there's no particular feature in 9.8 that would stop me downgrading to 9.6 if that was the path of least resistance to be able to use a library that I needed. |
| 07:14:27 | <jackdk> | probie: thanks for the data point. i think 9.8 is still only in stackage nightlies, and while I don't really care about the stackverse it tells me there's not yet the pressure to rush out a release. (The actual fix is minor, and I have a PR up, but it means a new release of the 300+ service bindings and I would like to not spam hackage) |
| 07:14:57 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 07:19:06 | × | EvanR quits (~EvanR@user/evanr) (Ping timeout: 245 seconds) |
| 07:24:17 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 07:41:23 | → | xff0x joins (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) |
| 07:41:31 | → | Square2 joins (~Square4@user/square) |
| 07:42:02 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:42:55 | <haskellbridge> | 05<irregularsphere> What's a stackverse? |
| 07:44:34 | × | Square quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 07:45:06 | <int-e> | stack + stackage + community (the alternative would probably be cabal + hackage + community, and of course there's a huge overlap) |
| 07:48:37 | × | foul_owl quits (~kerry@174-21-148-34.tukw.qwest.net) (Ping timeout: 268 seconds) |
| 07:58:24 | × | puke quits (~puke@user/puke) (Read error: Connection reset by peer) |
| 07:59:16 | → | puke joins (~puke@user/puke) |
| 08:01:49 | → | foul_owl joins (~kerry@185.216.231.181) |
| 08:06:17 | → | CiaoSen joins (~Jura@2a05:5800:2c0:fb00:ca4b:d6ff:fec1:99da) |
| 08:06:21 | <tomsmeding> | jackdk: I'm using ghc HEAD (9.9?) for some wasm side project, but I have never yet touched AWS stuff so this is an unimportant data point :p |
| 08:07:49 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 08:09:31 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 08:11:46 | × | euleritian quits (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) (Read error: Connection reset by peer) |
| 08:12:05 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 08:19:55 | → | gmg joins (~user@user/gehmehgeh) |
| 08:27:19 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 08:27:45 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 252 seconds) |
| 08:28:07 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 08:30:52 | → | waldo joins (~waldo@user/waldo) |
| 08:35:20 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 256 seconds) |
| 08:39:26 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 08:41:52 | → | miguelnegrao joins (~miguelneg@2001:818:dc71:d100:e682:f5cd:9590:d961) |
| 08:42:28 | × | mikess quits (~mikess@user/mikess) (Ping timeout: 255 seconds) |
| 08:44:32 | <miguelnegrao> | Hi all. I'm working on a pet project which uses a type safe interface using dependent types. I'm using type level peano nats data Nat = Zero | Succ Nat and in the types I go as high as 8 * 4096 in Nat types. |
| 08:45:35 | <miguelnegrao> | When I try to compile my project with such high Nats first ghc aborts, and then If I set -freduction-depth=0 it uses all available memory and is sigkilled. |
| 08:45:36 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 08:46:12 | <miguelnegrao> | Is there no hope of using a Nat such as the one I have above for realist values we encounter in actual code ? |
| 08:46:48 | → | mikess joins (~mikess@user/mikess) |
| 08:47:35 | <lortabac> | miguelnegrao: depending on your use case, you may be able to use GHC's built-in Nat type |
| 08:47:42 | <tomsmeding> | miguelnegrao: I'm not surprised that GHC gives up on that, no. The built-in nats (GHC.TypeNats) should perform a lot better, but they're also less flexible (no proper inductive structure, though ghc-typelits-natnormalise can help) |
| 08:48:41 | × | a51 quits (a51@gateway/vpn/protonvpn/a51) (Ping timeout: 245 seconds) |
| 08:50:15 | <miguelnegrao> | I need to do proofs, as far as I'm aware, you can't do proofs in the usual way with built in GHC.TypeNats... |
| 08:51:30 | <tomsmeding> | you're mostly at the mercy of the plugins (in addition to the mentioned one there's also a constraint simplification plugin), yes |
| 08:52:50 | <miguelnegrao> | My whole point here was learning depedent types, building proofs in the same way as agda, lean, etc and using it in a language I'm familiar with. In that case in my toy file system I will need to keep numbers small ... |
| 08:53:35 | <tomsmeding> | I'm not sure haskell is the proper place for that :D |
| 08:53:38 | <tomsmeding> | try agda |
| 08:53:42 | <tomsmeding> | it's fairly haskell-like |
| 08:53:53 | <tomsmeding> | idris also fits the bill I believe, but I've never used idris |
| 08:53:58 | <int-e> | you could probably cook up a binary representation but you'll have to pay for that in the proofs |
| 08:53:58 | <miguelnegrao> | tomsmending: I know, I know... but I love haskell too much :-D |
| 08:54:09 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 08:54:18 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 268 seconds) |
| 08:54:19 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 08:55:10 | <miguelnegrao> | I actually haven't bumped with too many things that I cannot do. The only issue I had with singletons was with promoting GADTs to singletons, which is difficult/not possible in the normal singletons package. |
| 08:55:51 | <tomsmeding> | yeah if you go full-on singletons (whether generated or hand-written) you can do quite a lot |
| 08:56:24 | <tomsmeding> | but note that haskell is not consistent: 'undefined' is a proof of false, infinite recursion is, and also technically the fact that Type :: Type is a logical paradox |
| 08:56:34 | ← | albet70 parts (~xxx@2400:8902::f03c:92ff:fe60:98d8) () |
| 08:57:37 | <tomsmeding> | % :set -XNoTypeInType |
| 08:57:37 | <yahb2> | <no output> |
| 08:57:39 | <tomsmeding> | % :k Type |
| 08:57:40 | <yahb2> | Type :: Type |
| 08:57:51 | <tomsmeding> | and support for NoTypeInType is long gone :D |
| 08:58:26 | <miguelnegrao> | But in practice these can be overcome, right ? Search the project for undefined. If there is infinite recursion then i doesn't compile, right ? |
| 08:58:48 | <tomsmeding> | let myReallyNotUndefined = myReallyNotUndefined |
| 08:58:59 | <tomsmeding> | it will definitely compile |
| 08:59:21 | <miguelnegrao> | so it will loop at runtime, in that case. |
| 08:59:27 | <tomsmeding> | yeah |
| 08:59:36 | <miguelnegrao> | Then you know you've made a mistake. :-) |
| 08:59:53 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 09:00:00 | <miguelnegrao> | but I see your point, the whole ideia is to catch problems at compile time. |
| 09:00:13 | <miguelnegrao> | One has to be careful with that. |
| 09:00:17 | <tomsmeding> | hmm, perhaps, but if I remember correctly there was a way to have that code not run at runtime |
| 09:00:40 | <tomsmeding> | I mean, if it's you that is writing all the code, then you can impose upon yourself the requirement that you (manually, on paper) prove termination of all your functions |
| 09:00:46 | <tomsmeding> | :p |
| 09:00:52 | <haskellbridge> | 05<irregularsphere> miguelnegrao: if infinite recursion doesn't compile then the compiler solves the halting problem |
| 09:01:07 | <haskellbridge> | 05<irregularsphere> (provably impossible) |
| 09:02:06 | <miguelnegrao> | haskellbridge: yes, good point. |
| 09:02:25 | × | sroso quits (~sroso@user/SrOso) (Read error: Connection reset by peer) |
| 09:03:53 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 09:04:50 | <miguelnegrao> | In Richard's thesis he does adress these concerns. He points to the possibility of writing a totality checker for Haskell. Regarding the lack of termination of type level functions GHC already has a reduction step counter, which was the problem I was hitting first. |
| 09:05:44 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 09:05:46 | → | nschoe2 joins (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) |
| 09:05:51 | <miguelnegrao> | They are building dependent types into Haskell, so I suppose the consider the effort worth it somehow... |
| 09:06:05 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 240 seconds) |
| 09:06:11 | <miguelnegrao> | (possibly not for proofs...) |
| 09:06:31 | <c_wraith> | Eh. The compiler doesn't need to solve the halting problem to reject code that it can't prove terminates. |
| 09:06:50 | <c_wraith> | There are lots of languages with that feature. |
| 09:07:36 | <miguelnegrao> | Although you can't really almost do anything with for instance a Nat indexed Vec without proofs. |
| 09:08:10 | × | Square2 quits (~Square4@user/square) (Ping timeout: 256 seconds) |
| 09:08:14 | <miguelnegrao> | c_wraith: that's a termination checker, right ? |
| 09:08:24 | <c_wraith> | yes. |
| 09:10:06 | <c_wraith> | The halting problem says that you can't look at all programs and determine whether they halt or not. But you can still say "this is easy to prove termination for, that's easy to prove non-termination for, and for all the ones where the proof isn't easy, the programmer has to provide it" |
| 09:10:19 | <haskellbridge> | 05<irregularsphere> c_wraith: yeah i suppose we can't have a perfect one |
| 09:11:01 | → | Square2 joins (~Square4@user/square) |
| 09:11:15 | → | barak joins (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) |
| 09:12:30 | <c_wraith> | the plan I recall for a dependent typing extension to haskell was to turn inconsistent types into runtime bottoms, by compiling a residue of the proof into something that needed to be evaluated along with the expression |
| 09:13:29 | <c_wraith> | which is roughly equivalent to how haskell handles inconsistent types anyway |
| 09:14:34 | <c_wraith> | But last I heard, that entire project is sort of on standby due to GHC core being much harder to make dependently-typed than expected |
| 09:15:43 | <miguelnegrao> | c_wraith: I believe there is still progress happening: https://serokell.io/blog/ghc-dependent-types-in-haskell-2 this was from 22nd December. |
| 09:17:12 | <c_wraith> | Ok, not totally on standby, but now like 5 years behind the initial plan as the obstacles are very slowly smoothed out :) |
| 09:17:41 | <miguelnegrao> | Yeah, it's a hard problem... |
| 09:20:14 | × | Square2 quits (~Square4@user/square) (Ping timeout: 260 seconds) |
| 09:20:34 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 09:21:11 | <miguelnegrao> | Still, this issue with GHC.TypeLit vs inductive Nats and perfomance of inductive Nats seems unresolved... |
| 09:21:19 | <haskellbridge> | 05<irregularsphere> c_wraith: "...the programmer has to provide it" reminds me of the 3*n+1 conjecture |
| 09:22:14 | <c_wraith> | That's absolutely one a termination checker would say "that's up to you" about |
| 09:22:21 | <miguelnegrao> | https://lean-lang.org/lean4/doc/nat.html "However, the internal representation of Nat is optimized. Small natural numbers (i.e., < 2^63 in a 64-bit machine) are represented by a single machine word. Big numbers are implemented using GMP numbers. " |
| 09:24:12 | <haskellbridge> | 05<irregularsphere> c_wraith: ...The proof is left as an exercise to the programmer |
| 09:24:14 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 09:26:29 | <miguelnegrao> | "Well, I have a very nice proof of that, it just doesn't fit on the side of this page..." |
| 09:26:55 | <haskellbridge> | 05<irregularsphere> "It's trivial." |
| 09:29:17 | <c_wraith> | I just want pi types. I'm not especially concerned with proof systems or compile-time evaluation. I just want to be able to parameterize types with values and have those values be available at run time. |
| 09:30:28 | <c_wraith> | (without the pain of using singletons) |
| 09:31:57 | × | xff0x quits (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) (Ping timeout: 256 seconds) |
| 09:32:24 | <haskellbridge> | 05<irregularsphere> I was thinking of a () -> a, but I'm not sure if that's idiomatic |
| 09:32:26 | × | ubert quits (~Thunderbi@p200300ecdf2683a8da5ffe35771476c1.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 09:32:39 | <haskellbridge> | 05<irregularsphere> :t const |
| 09:32:52 | <haskellbridge> | 05<irregularsphere> > :t const |
| 09:33:04 | <haskellbridge> | 05<irregularsphere> const :: a -> b -> a |
| 09:33:18 | <c_wraith> | sorry, the bots don't recognize how the matrix bridge relays messages on the IRC side |
| 09:33:27 | <haskellbridge> | 05<irregularsphere> huh |
| 09:34:12 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:36:23 | <haskellbridge> | 05<irregularsphere> actually wait () -> a isn't a singleton |
| 09:36:26 | <haskellbridge> | 05<irregularsphere> it's isomorphic to a |
| 09:37:25 | × | nschoe2 quits (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) (Quit: WeeChat 4.1.2) |
| 09:37:56 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 09:41:02 | <miguelnegrao> | Do you mean Void -> a ? |
| 09:41:20 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 09:41:33 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 09:42:14 | <haskellbridge> | 05<irregularsphere> Void has no inhabitants |
| 09:42:33 | <haskellbridge> | 05<irregularsphere> hence why absurd (:: Void -> a) is called absurd |
| 09:43:44 | <haskellbridge> | 05<irregularsphere> meanwhile () has an inhabitant, called () |
| 09:44:23 | <haskellbridge> | 05<irregularsphere> and only () |
| 09:46:54 | <haskellbridge> | 05<irregularsphere> actually wait you have a good point |
| 09:46:56 | <ncf> | Void -> a is also a singleton |
| 09:47:03 | <haskellbridge> | 05<irregularsphere> Void -> a is a singleton yes |
| 09:47:05 | <haskellbridge> | 05<irregularsphere> but is it usable |
| 09:47:47 | <famubu> | What's the use of type roles? Does anyone know of a good resource preferably with examples where we can read about it? |
| 09:48:17 | <famubu> | And where is this room bridged to? is it some other public space? |
| 09:48:30 | <haskellbridge> | 05<irregularsphere> #haskell-irc:matrix.org |
| 09:48:37 | <famubu> | Ah.. |
| 09:49:27 | <famubu> | For understanding type roles, I tried reading some of this: https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/roles.html#:~:text=The%20role%20of%20a%20type,as%20T%20Int%20Bool%20c%20). |
| 09:49:53 | <famubu> | But I didn't get the example mentioned there. |
| 09:50:12 | → | waldo joins (~waldo@user/waldo) |
| 09:50:12 | <miguelnegrao> | Void -> a is ex falso quodlibet (EFQ) from False (Void) any proposition follows. And a -> Void is "not a". At least in Lean ... |
| 09:50:51 | <int-e> | famubu: The example would coerce Inspect Int (= Bool) to Inspect Age (= Int) |
| 09:51:46 | <famubu> | int-e: Is that coercion an example representational type role or of nominal? |
| 09:52:16 | <famubu> | I thought nominal needed exact same thing? it looked more like 'representational equivality' |
| 09:52:45 | × | miguelnegrao quits (~miguelneg@2001:818:dc71:d100:e682:f5cd:9590:d961) (Quit: miguelnegrao) |
| 09:52:54 | <famubu> | `data Complex a = MkComplex (F a)` is mentioned as example of nominal type role |
| 09:53:01 | <int-e> | famubu: Which breaks the type system (There is dark history here; for a while, GeneralizedNewtypeDeriving could *actually* be used to implement `unsafeCoerce`. This was fixed through equality constraints (a ~ b), coerce and Coercible, and type roles.). |
| 09:55:20 | <int-e> | famubu: Maybe a more natural motivating example is `Data.Map.Map k a`, where `k` is declared to be nominal. This prevents you from coercing a `Map k a` to `Map k' a` where k' is a newtype wrapper around k, which may come with a completely different Ord instance, breaking the integrity of the associative map. (It doesn't break type safety though, so the ghc manual uses a more abstract but... |
| 09:55:26 | <int-e> | ...ultimately more devastating example) |
| 09:56:18 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:56:40 | → | wheatengineer joins (~frederik@p200300f63f3a4600180a52eefcdcc2d6.dip0.t-ipconnect.de) |
| 09:59:51 | → | nschoe joins (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) |
| 10:02:19 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) |
| 10:02:54 | <famubu> | Okay, so one of the uses for type role nominal is to prevent coercions? |
| 10:03:31 | <famubu> | Phantom is like don't care, I guess. But then why bother writing it? Or is it that it's a default type role? |
| 10:03:53 | <famubu> | And where does representational come in handy? |
| 10:04:18 | <famubu> | Isn't coercion possible only when there representations of the two types are same? Or something like that? |
| 10:04:47 | <famubu> | Type role is for specific type parameter of a type, is it? |
| 10:05:01 | <famubu> | It's like 'the role of a parameter in the type' |
| 10:05:19 | <famubu> | When I first heard the name type role, I thought it was something related to the entire type as a whole. |
| 10:05:50 | × | xdminsy quits (~xdminsy@117.147.71.169) (Ping timeout: 268 seconds) |
| 10:06:09 | → | xdminsy joins (~xdminsy@117.147.71.169) |
| 10:06:50 | → | danse-nr3 joins (~danse@151.43.165.56) |
| 10:07:23 | × | phma quits (~phma@host-67-44-208-148.hnremote.net) (Read error: Connection reset by peer) |
| 10:08:17 | → | Tuplanolla joins (~Tuplanoll@91-159-69-171.elisa-laajakaista.fi) |
| 10:08:26 | → | phma joins (~phma@host-67-44-208-144.hnremote.net) |
| 10:09:24 | <famubu> | Is it that a type role is mentioned only for the last type argument of a type? |
| 10:12:23 | × | meritamen quits (~meritamen@user/meritamen) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 10:15:28 | <famubu> | No, type roles is for all arguments of type. |
| 10:16:42 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 10:18:12 | → | rosco joins (~rosco@175.136.156.77) |
| 10:18:26 | <int-e> | Yes, this is about restricting coercions. To coerce T a to T b, if the argument has a nominal role, a and be must be the same; if it's representational, then a and b must be coercible, and if it's a phantom argument, then you can coerce no matter what the types a and b are. |
| 10:18:43 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 10:18:49 | <famubu> | int-e: Thanks |
| 10:19:11 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 10:19:57 | <int-e> | These roles can be inferred (in data types you get only representational and phantom roles, but type families require nominal roles), but also manually adjusted to restrict coercions even further. |
| 10:21:36 | × | acidjnk quits (~acidjnk@2003:d6:e72b:9308:1c56:4b97:a161:31b) (Ping timeout: 245 seconds) |
| 10:24:19 | → | meritamen joins (~meritamen@user/meritamen) |
| 10:27:58 | → | not_reserved joins (~not_reser@185.153.177.191) |
| 10:29:41 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) (Remote host closed the connection) |
| 10:33:09 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 252 seconds) |
| 10:34:38 | → | igemnace joins (~ian@user/igemnace) |
| 10:36:04 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds) |
| 10:52:46 | → | chele joins (~chele@user/chele) |
| 11:04:18 | × | tertek quits (~tertek@user/tertek) (Ping timeout: 260 seconds) |
| 11:05:49 | × | meritamen quits (~meritamen@user/meritamen) (Remote host closed the connection) |
| 11:05:56 | → | tertek joins (~tertek@user/tertek) |
| 11:06:26 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) |
| 11:12:54 | <haskellbridge> | 05<irregularsphere> did haskell invent everything |
| 11:13:34 | <haskellbridge> | 05<irregularsphere> i was reading the singleton paper and right off the bat the citations are 2000s (especially since the paper is from 2012) |
| 11:14:40 | <haskellbridge> | 05<irregularsphere> amazing features btw |
| 11:21:09 | × | Luj quits (~Luj@2a01:e0a:5f9:9681:2ea5:d487:e077:51db) (Quit: Ping timeout (120 seconds)) |
| 11:21:28 | → | Luj joins (~Luj@2a01:e0a:5f9:9681:f715:669b:cfa9:834a) |
| 11:24:17 | → | AndreiDuma joins (~textual@95.76.23.32) |
| 11:25:53 | × | kmein quits (~weechat@user/kmein) (Quit: ciao kakao) |
| 11:26:24 | ← | AndreiDuma parts (~textual@95.76.23.32) () |
| 11:26:27 | → | AndreiDuma joins (~textual@95.76.23.32) |
| 11:27:04 | → | causal joins (~eric@50.35.85.7) |
| 11:36:11 | → | Square2 joins (~Square4@user/square) |
| 11:37:05 | → | kmein joins (~weechat@user/kmein) |
| 11:39:23 | × | bilegeek quits (~bilegeek@2600:1008:b0a5:5faa:ea63:51d4:70a3:2023) (Quit: Leaving) |
| 11:39:24 | → | xff0x joins (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) |
| 11:42:39 | × | mikess quits (~mikess@user/mikess) (Ping timeout: 268 seconds) |
| 11:42:46 | → | meritamen joins (~meritamen@user/meritamen) |
| 11:46:08 | → | mmhat joins (~mmh@p200300f1c7428268ee086bfffe095315.dip0.t-ipconnect.de) |
| 11:46:22 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:54:40 | × | puke quits (~puke@user/puke) (Ping timeout: 268 seconds) |
| 12:00:54 | × | danse-nr3 quits (~danse@151.43.165.56) (Read error: Connection reset by peer) |
| 12:22:22 | → | acidjnk joins (~acidjnk@p200300d6e72b930818892410b5265f00.dip0.t-ipconnect.de) |
| 12:22:53 | × | nschoe quits (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) (Ping timeout: 240 seconds) |
| 12:26:04 | × | lingprefix quits (~lingprefi@user/lingprefix) (Quit: leaving) |
| 12:28:32 | × | AndreiDuma quits (~textual@95.76.23.32) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 12:37:04 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 12:43:14 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 260 seconds) |
| 12:47:27 | × | vglfr quits (~vglfr@234.red-88-6-215.staticip.rima-tde.net) (Ping timeout: 256 seconds) |
| 12:48:37 | → | vglfr joins (~vglfr@90.167.190.99) |
| 12:49:11 | → | AndreiDuma joins (~textual@95.76.23.32) |
| 13:04:45 | × | vglfr quits (~vglfr@90.167.190.99) (Read error: Connection reset by peer) |
| 13:05:29 | → | vglfr joins (~vglfr@234.red-88-6-215.staticip.rima-tde.net) |
| 13:22:46 | → | mikess joins (~mikess@user/mikess) |
| 13:25:25 | → | ryantrinkle joins (~ryantrink@140.174.247.171) |
| 13:26:10 | <ryantrinkle> | is the external interpreter incredibly slow? i am trying it (for the first time) and it's just hanging at "GHCi, version 8.10.7: https://www.haskell.org/ghc/ :? for help" for 10 minutes |
| 13:26:30 | <ryantrinkle> | it's a somewhat large project (hundreds of modules, hundreds of deps), but it has not even started mentioning loading modules |
| 13:27:00 | <ryantrinkle> | ghc-iserv-prof has been at 100% CPU the whole time |
| 13:27:14 | <ryantrinkle> | (this is running with -fexternal-interpreter -prof) |
| 13:43:31 | → | alexherbo2 joins (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 14:01:51 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) (Remote host closed the connection) |
| 14:02:20 | ← | ryantrinkle parts (~ryantrink@140.174.247.171) () |
| 14:05:21 | × | CiaoSen quits (~Jura@2a05:5800:2c0:fb00:ca4b:d6ff:fec1:99da) (Ping timeout: 245 seconds) |
| 14:05:41 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) |
| 14:08:03 | → | danse-nr3 joins (~danse@151.43.184.127) |
| 14:08:55 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 14:10:37 | × | cfricke quits (~cfricke@user/cfricke) (Ping timeout: 246 seconds) |
| 14:12:36 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 14:13:37 | × | phma quits (~phma@host-67-44-208-144.hnremote.net) (Read error: Connection reset by peer) |
| 14:14:05 | → | phma joins (~phma@host-67-44-208-144.hnremote.net) |
| 14:27:02 | → | EvanR joins (~EvanR@user/evanr) |
| 14:27:29 | × | EvanR quits (~EvanR@user/evanr) (Remote host closed the connection) |
| 14:28:38 | → | EvanR joins (~EvanR@user/evanr) |
| 14:32:14 | → | ystael joins (~ystael@user/ystael) |
| 14:33:03 | × | jargon quits (~jargon@211.sub-174-205-225.myvzw.com) (Read error: Connection reset by peer) |
| 14:35:35 | → | ryantrinkle joins (~ryantrink@140.174.247.171) |
| 14:40:30 | → | eggplant_ joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 14:41:53 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) (Quit: ubert) |
| 14:42:04 | → | ubert1 joins (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) |
| 14:42:21 | × | ubert1 quits (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) (Client Quit) |
| 14:43:06 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) (Ping timeout: 260 seconds) |
| 14:43:35 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) |
| 14:44:23 | × | xff0x quits (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) (Ping timeout: 264 seconds) |
| 14:46:34 | <EvanR> | famubu, that kind of function is technically possible using dependent types, which haskell doesn't have but other languages do |
| 14:47:07 | <EvanR> | though that example is a bit contrived and not that motivating for such complexity |
| 14:48:21 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 14:48:36 | → | euleritian joins (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) |
| 15:03:08 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 15:04:51 | × | rosco quits (~rosco@175.136.156.77) (Quit: Lost terminal) |
| 15:06:21 | → | a51 joins (a51@gateway/vpn/protonvpn/a51) |
| 15:09:53 | × | AndreiDuma quits (~textual@95.76.23.32) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 15:16:52 | × | alexherbo2 quits (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 15:19:06 | × | mmhat quits (~mmh@p200300f1c7428268ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 15:19:28 | → | mmhat joins (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) |
| 15:21:52 | × | wheatengineer quits (~frederik@p200300f63f3a4600180a52eefcdcc2d6.dip0.t-ipconnect.de) (Quit: Leaving) |
| 15:25:19 | → | ph88 joins (~ph88@2a02:8109:9e26:c800:e199:9848:c5f0:b040) |
| 15:26:27 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 15:26:42 | × | Square2 quits (~Square4@user/square) (Ping timeout: 256 seconds) |
| 15:31:06 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.1.1) |
| 15:33:39 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 15:38:31 | → | alexherbo2 joins (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 15:48:03 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:52:47 | × | euleritian quits (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:53:00 | × | a51 quits (a51@gateway/vpn/protonvpn/a51) (Quit: WeeChat 4.1.2) |
| 15:53:06 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:57:39 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 15:58:38 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:03:12 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 16:04:02 | × | not_reserved quits (~not_reser@185.153.177.191) (Quit: Client closed) |
| 16:06:37 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:07:59 | × | ph88 quits (~ph88@2a02:8109:9e26:c800:e199:9848:c5f0:b040) (Quit: Leaving) |
| 16:10:04 | → | ph88 joins (~ph88@2a02:8109:9e26:c800:2698:eca0:c269:b854) |
| 16:11:35 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) (Ping timeout: 256 seconds) |
| 16:16:00 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 16:17:23 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 16:17:54 | → | euleritian joins (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) |
| 16:18:29 | → | not_reserved joins (~not_reser@185.153.177.191) |
| 16:20:39 | × | ph88 quits (~ph88@2a02:8109:9e26:c800:2698:eca0:c269:b854) (Ping timeout: 256 seconds) |
| 16:23:02 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 16:24:24 | × | meritamen quits (~meritamen@user/meritamen) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 16:25:01 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 16:29:17 | × | phma quits (~phma@host-67-44-208-144.hnremote.net) (Read error: Connection reset by peer) |
| 16:29:39 | → | a51 joins (a51@gateway/vpn/protonvpn/a51) |
| 16:36:03 | → | phma joins (~phma@2001:5b0:211f:6828:6be8:2d10:9148:6096) |
| 16:39:00 | × | not_reserved quits (~not_reser@185.153.177.191) (Quit: Client closed) |
| 16:44:03 | × | eggplant_ quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 16:44:19 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d504:f200:d614:49c6) |
| 16:46:43 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 16:49:06 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 260 seconds) |
| 16:50:33 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 16:55:08 | × | mmhat quits (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.1.2) |
| 16:57:56 | → | mmhat joins (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) |
| 16:59:50 | × | mmhat quits (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 16:59:55 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 17:01:58 | × | danse-nr3 quits (~danse@151.43.184.127) (Ping timeout: 276 seconds) |
| 17:03:10 | × | alp_ quits (~alp@2001:861:e3d6:8f80:f7ce:4acc:831e:1a6e) (Ping timeout: 246 seconds) |
| 17:06:50 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 17:08:46 | → | waldo joins (~waldo@user/waldo) |
| 17:11:05 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 17:15:37 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 17:19:42 | <cheater> | hi |
| 17:19:47 | <cheater> | anyone got a good monad tutorial? |
| 17:23:15 | → | not_reserved joins (~not_reser@185.153.177.191) |
| 17:24:51 | → | mechap joins (~mechap@user/mechap) |
| 17:25:34 | <duncan> | cheater: https://blog.ploeh.dk/2017/10/04/from-design-patterns-to-category-theory/ |
| 17:25:53 | <cheater> | nice |
| 17:26:41 | <EvanR> | lol https://wiki.haskell.org/Monad_tutorials_timeline |
| 17:29:38 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 17:31:46 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 17:33:50 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 17:34:26 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 260 seconds) |
| 17:34:42 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:35:27 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 17:36:18 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 17:38:47 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:42:29 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 240 seconds) |
| 17:43:10 | <tomsmeding> | it's even on the list! |
| 17:44:52 | × | barak quits (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) (Remote host closed the connection) |
| 17:46:10 | → | barak joins (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) |
| 17:46:51 | <duncan> | Seemann writes so well and that series is so comprehensive. Great stuff. |
| 17:47:09 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 17:47:29 | → | waldo joins (~waldo@user/waldo) |
| 17:47:40 | <EvanR> | there was a monad non-tutorial which was just a bunch of examples of common ways to use monads but written in ruby or something |
| 17:48:07 | <EvanR> | I mean, idiomatic block structured ruby code which is doing something that haskell files under "monads" |
| 17:50:34 | <EvanR> | that I cannot find or remember |
| 17:54:51 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 17:55:39 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 17:56:15 | × | xsarnik quits (xsarnik@lounge.fi.muni.cz) (Quit: Ping timeout (120 seconds)) |
| 17:56:44 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.1.2) |
| 17:56:59 | × | ricardo2 quits (~ricardo@84.16.179.218) (Ping timeout: 264 seconds) |
| 17:57:04 | × | eL_Bart0 quits (eL_Bart0@dietunichtguten.org) (Quit: Restarting) |
| 17:57:14 | → | michalz_ joins (~michalz@185.246.207.201) |
| 17:57:15 | → | ricardo1 joins (~ricardo@84.16.179.218) |
| 17:57:22 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 17:57:31 | → | eL_Bart0 joins (eL_Bart0@dietunichtguten.org) |
| 17:58:47 | × | michalz quits (~michalz@185.246.207.221) (Ping timeout: 264 seconds) |
| 18:01:37 | → | xsarnik joins (xsarnik@lounge.fi.muni.cz) |
| 18:02:15 | × | bah quits (~bah@l1.tel) (Ping timeout: 260 seconds) |
| 18:02:23 | → | bah joins (~bah@l1.tel) |
| 18:02:31 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 240 seconds) |
| 18:02:55 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 240 seconds) |
| 18:03:07 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 18:03:51 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 18:04:12 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 18:04:31 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 18:04:36 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 18:13:30 | × | alexherbo2 quits (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 18:16:05 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 268 seconds) |
| 18:17:07 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 255 seconds) |
| 18:19:19 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 18:19:31 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 256 seconds) |
| 18:20:40 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 18:21:32 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 18:24:02 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:25:35 | × | irrgit_ quits (~irrgit@89.47.234.74) (Read error: Connection reset by peer) |
| 18:27:39 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 18:33:44 | → | waldo joins (~waldo@user/waldo) |
| 18:36:40 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 18:37:11 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 18:38:28 | → | danza joins (~danza@151.43.143.81) |
| 18:42:52 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 18:43:19 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 18:44:35 | → | alexherbo2 joins (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 18:45:59 | → | AndreiDuma joins (~textual@95.76.23.32) |
| 18:46:18 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 260 seconds) |
| 18:48:18 | → | mechap joins (~mechap@user/mechap) |
| 18:53:52 | × | alexherbo2 quits (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 18:54:16 | → | alexherbo2 joins (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 18:54:16 | × | alexherbo2 quits (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 18:54:35 | → | alexherbo2 joins (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 18:59:06 | × | alexherbo2 quits (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Ping timeout: 250 seconds) |
| 18:59:18 | → | puke joins (~puke@user/puke) |
| 18:59:22 | × | euleritian quits (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:59:44 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:01:27 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 19:08:52 | × | vglfr quits (~vglfr@234.red-88-6-215.staticip.rima-tde.net) (Ping timeout: 255 seconds) |
| 19:11:08 | → | alexherbo2 joins (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 19:12:29 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 19:15:33 | → | target_i joins (~target_i@217.175.14.39) |
| 19:16:19 | × | Batzy_ quits (~quassel@user/batzy) (Ping timeout: 256 seconds) |
| 19:21:47 | → | kwii joins (~kwii@212.24.26.235) |
| 19:25:10 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 19:27:10 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 19:28:21 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 19:29:51 | → | vglfr joins (~vglfr@234.red-88-6-215.staticip.rima-tde.net) |
| 19:32:40 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 19:33:08 | → | euleritian joins (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) |
| 19:39:39 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 19:40:26 | → | sammburr joins (~sammburr@host-92-16-247-196.as13285.net) |
| 19:40:58 | ← | sammburr parts (~sammburr@host-92-16-247-196.as13285.net) () |
| 19:41:02 | × | euleritian quits (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) (Read error: Connection reset by peer) |
| 19:41:19 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:44:52 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 19:45:41 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:49:06 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 19:52:35 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 256 seconds) |
| 19:54:35 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds) |
| 19:56:37 | → | jmdaemon joins (~jmdaemon@user/jmdaemon) |
| 19:59:23 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 20:02:01 | × | jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 246 seconds) |
| 20:05:39 | × | alexherbo2 quits (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 20:07:51 | × | kwii quits (~kwii@212.24.26.235) (Read error: Connection reset by peer) |
| 20:07:59 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 20:08:14 | → | kwii joins (~kwii@212.24.26.235) |
| 20:08:23 | → | waldo joins (~waldo@user/waldo) |
| 20:14:56 | × | benjaminl quits (~benjaminl@user/benjaminl) (Ping timeout: 245 seconds) |
| 20:15:05 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 20:17:48 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 20:18:55 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 20:23:16 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 20:23:37 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 20:24:34 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 20:27:08 | × | kwii quits (~kwii@212.24.26.235) (Ping timeout: 252 seconds) |
| 20:27:48 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d504:f200:d614:49c6) (Remote host closed the connection) |
| 20:27:51 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 245 seconds) |
| 20:29:44 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 20:31:16 | × | danza quits (~danza@151.43.143.81) (Ping timeout: 276 seconds) |
| 20:33:40 | → | alexherbo2 joins (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 20:33:46 | <tomsmeding> | EvanR: I updated the graph (may need to force-reload the page for your browser to re-fetch it) https://wiki.haskell.org/Monad_tutorials_timeline |
| 20:34:32 | <EvanR> | yep I did have to force reload the page |
| 20:34:47 | <EvanR> | I think that's the first time I force reloaded a page in like 9 years |
| 20:35:18 | <EvanR> | caching is still hard! |
| 20:35:19 | <tomsmeding> | I sometimes force-reload MS Teams out of anger just to put more load on their servers when it broke again |
| 20:36:00 | <EvanR> | sadly or fortunately we have no monad tutorials for 2024 yet |
| 20:36:20 | → | nschoe joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 20:36:32 | <tomsmeding> | this is your chance! |
| 20:36:58 | <tomsmeding> | I sent this to a friend and they went like, "search for 'monad tutorial' on youtube and multiply these numbers by like 5" |
| 20:37:09 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 20:38:26 | <EvanR> | there are too many monad tutorials. Clearly the only solution is another one which explains it once and for all |
| 20:39:06 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 245 seconds) |
| 20:39:11 | × | AndreiDuma quits (~textual@95.76.23.32) (Quit: Textual IRC Client: www.textualapp.com) |
| 20:39:34 | → | AndreiDuma joins (~textual@95.76.23.32) |
| 20:41:57 | <haskellbridge> | 15<Jade> https://xkcd.com/927/ | sed 's/standard/monad tutorial/g' |
| 20:43:59 | <tomsmeding> | my immediate thought too |
| 20:44:26 | <tomsmeding> | the alt-text is funny because it's usb-c now |
| 20:45:41 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Remote host closed the connection) |
| 20:46:09 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 20:46:47 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 20:46:47 | <EvanR> | usb is an infinitely nested shrinking sequence of plugs |
| 20:47:11 | <EvanR> | but it's uncomputable so we're getting through the sequence quite slow |
| 20:50:43 | → | waldo joins (~waldo@user/waldo) |
| 20:59:52 | × | barak quits (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) (Ping timeout: 276 seconds) |
| 21:01:35 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a926:b546:474f:4cf4) |
| 21:04:33 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 21:06:35 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:a926:b546:474f:4cf4) (Ping timeout: 268 seconds) |
| 21:07:54 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 21:10:11 | × | mikess quits (~mikess@user/mikess) (Ping timeout: 264 seconds) |
| 21:12:14 | × | ricardo1 quits (~ricardo@84.16.179.218) (Read error: Connection reset by peer) |
| 21:14:41 | × | alexherbo2 quits (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 21:15:31 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 21:18:26 | → | hexology joins (~hexology@user/hexology) |
| 21:20:57 | → | mikess joins (~mikess@user/mikess) |
| 21:23:15 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 21:25:34 | → | nschoe2 joins (nschoe@gateway/vpn/protonvpn/nschoe) |
| 21:25:52 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 21:26:50 | × | nschoe quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 260 seconds) |
| 21:37:33 | × | waldo quits (~waldo@user/waldo) (Ping timeout: 252 seconds) |
| 21:43:56 | × | tomsmeding quits (~tomsmedin@2a01:4f8:c0c:5e5e::2) (Quit: ZNC 1.8.2 - https://znc.in) |
| 21:44:29 | → | tomsmeding joins (~tomsmedin@2a01:4f8:c0c:5e5e::2) |
| 21:47:17 | → | waldo joins (~waldo@user/waldo) |
| 21:47:22 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 21:47:42 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-a6e3-3ba3-0107-8cff.res6.spectrum.com) |
| 21:48:20 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 21:50:41 | → | ircbrowse_tom joins (~ircbrowse@2a01:4f8:1c1c:9319::1) |
| 21:50:47 | Server | sets mode +Cnt |
| 21:51:57 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:a926:b546:474f:4cf4) |
| 22:08:18 | × | michalz_ quits (~michalz@185.246.207.201) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:09:39 | × | AndreiDuma quits (~textual@95.76.23.32) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 22:11:00 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 22:15:15 | × | Bynbo7 quits (~Axman6@user/axman6) (Remote host closed the connection) |
| 22:16:06 | × | Axman6 quits (~Axman6@user/axman6) (Remote host closed the connection) |
| 22:17:13 | × | xdminsy quits (~xdminsy@117.147.71.169) (Ping timeout: 276 seconds) |
| 22:17:28 | → | xdminsy joins (~xdminsy@117.147.71.199) |
| 22:20:38 | × | Axman61 quits (~Axman6@user/axman6) (Ping timeout: 244 seconds) |
| 22:21:38 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 22:22:24 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 22:24:59 | × | Flow quits (~none@gentoo/developer/flow) (Ping timeout: 260 seconds) |
| 22:27:41 | × | target_i quits (~target_i@217.175.14.39) (Quit: leaving) |
| 22:28:08 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:29:28 | → | kwii joins (~kwii@212.24.26.235) |
| 22:35:29 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 22:48:01 | × | myme quits (~myme@2a01:799:d60:e400:40e3:f57:648e:522b) (Ping timeout: 255 seconds) |
| 22:48:53 | → | myme joins (~myme@2a01:799:d60:e400:a6b6:bec4:8c06:a0eb) |
| 22:49:25 | <haskellbridge> | 05<irregularsphere> "monad tutorial"? i look at Monad in the docs and go "oh, okay" |
| 22:52:29 | × | acidjnk quits (~acidjnk@p200300d6e72b930818892410b5265f00.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 23:02:08 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:08:56 | → | Flow joins (~none@gentoo/developer/flow) |
| 23:10:58 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 23:16:56 | → | barak joins (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) |
| 23:21:45 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 23:28:53 | → | Axman6 joins (~Axman6@user/axman6) |
| 23:29:55 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 245 seconds) |
| 23:31:47 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 23:33:16 | × | Axman6 quits (~Axman6@user/axman6) (Remote host closed the connection) |
| 23:34:08 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 252 seconds) |
| 23:38:13 | × | foul_owl quits (~kerry@185.216.231.181) (Quit: WeeChat 3.8) |
| 23:38:29 | → | foul_owl joins (~kerry@185.216.231.181) |
| 23:44:30 | × | not_reserved quits (~not_reser@185.153.177.191) (Quit: Client closed) |
| 23:44:57 | × | a51 quits (a51@gateway/vpn/protonvpn/a51) (Quit: WeeChat 4.1.2) |
| 23:46:01 | <EvanR> | pssh documentation is old hat |
| 23:46:20 | × | barak quits (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) (Remote host closed the connection) |
| 23:54:30 | × | nschoe2 quits (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 245 seconds) |
| 23:54:50 | → | Guest8 joins (~Guest93@155.33.133.42) |
| 23:55:50 | <Guest8> | @pl (\e a p -> a (f e p)) |
| 23:55:50 | <lambdabot> | flip (.) . f |
| 23:57:34 | <monochrom> | What would be really interesting is the number of monad videos on TikTok. >:) |
| 23:57:58 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 23:58:00 | × | kwii quits (~kwii@212.24.26.235) (Remote host closed the connection) |
| 23:58:46 | × | Guest8 quits (~Guest93@155.33.133.42) (Client Quit) |
| 23:58:50 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:59:07 | <EvanR> | resulting in everyone except montana understanding monads |
All times are in UTC on 2024-01-09.