| 2024-01-09 00:05:28 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-01-09 00:11:01 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-01-09 00:11:39 +0100 | euleritian | (~euleritia@dynamic-089-015-238-167.89.15.238.pool.telefonica.de) |
| 2024-01-09 00:21:10 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 276 seconds) |
| 2024-01-09 00:31:11 +0100 | <Axman6> | @hoogle (a -> f b) -> Maybe a -> f () |
| 2024-01-09 00:31:12 +0100 | <lambdabot> | Control.Concurrent.Async.Lifted mapConcurrently_ :: (Foldable t, MonadBaseControl IO m) => (a -> m b) -> t a -> m () |
| 2024-01-09 00:31:12 +0100 | <lambdabot> | Control.Concurrent.Async.Lifted.Safe mapConcurrently_ :: (Foldable t, MonadBaseControl IO m, Forall (Pure m)) => (a -> m b) -> t a -> m () |
| 2024-01-09 00:31:12 +0100 | <lambdabot> | Prelude mapM_ :: (Foldable t, Monad m) => (a -> m b) -> t a -> m () |
| 2024-01-09 00:33:55 +0100 | <Axman6> | thanks mapM_ <3 |
| 2024-01-09 00:39:15 +0100 | <jackdk> | Axman6: for_ |
| 2024-01-09 00:39:24 +0100 | <jackdk> | % :t Data.Foldable.for_ |
| 2024-01-09 00:39:24 +0100 | <yahb2> | Data.Foldable.for_ ; :: (Foldable t, Applicative f) => t a -> (a -> f b) -> f () |
| 2024-01-09 00:40:02 +0100 | <jackdk> | Axman6: also beware https://www.snoyman.com/blog/2017/01/foldable-mapm-maybe-and-recursive-functions/ |
| 2024-01-09 00:43:40 +0100 | duncan | (~duncan@user/duncan) (Ping timeout: 246 seconds) |
| 2024-01-09 00:49:41 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 240 seconds) |
| 2024-01-09 00:51:38 +0100 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-01-09 00:59:25 +0100 | duncan | (~duncan@user/duncan) |
| 2024-01-09 01:00:24 +0100 | res0nat0r0844909 | (~Fletch@falcon.whatbox.ca) |
| 2024-01-09 01:05:42 +0100 | steew_ | (~steew@user/steew) |
| 2024-01-09 01:07:13 +0100 | steew | (~steew@user/steew) (Ping timeout: 255 seconds) |
| 2024-01-09 01:07:14 +0100 | steew_ | steew |
| 2024-01-09 01:11:38 +0100 | <Axman6> | That's a little scary... |
| 2024-01-09 01:11:54 +0100 | <Axman6> | Luckily this isn't recursive |
| 2024-01-09 01:14:23 +0100 | mechap | (~mechap@user/mechap) (Ping timeout: 264 seconds) |
| 2024-01-09 01:15:50 +0100 | Jard | (~igork@78.84.190.186) |
| 2024-01-09 01:16:05 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-01-09 01:18:26 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-171.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-01-09 01:20:22 +0100 | <Axman6> | @type let f <$! l = f <$> view l in (<$!) |
| 2024-01-09 01:20:23 +0100 | <lambdabot> | MonadReader s f => (a -> b) -> Getting a s a -> f b |
| 2024-01-09 01:22:41 +0100 | <Axman6> | @type let f <$. l = f <$> view l; f <*. l = f <*> view l in flip (,) <$. _1 <*. _2 |
| 2024-01-09 01:22:42 +0100 | <lambdabot> | (MonadReader s f, Field1 s s b1 b1, Field2 s s b2 b2) => f (b2, b1) |
| 2024-01-09 01:22:49 +0100 | Square | (~Square@user/square) |
| 2024-01-09 01:41:22 +0100 | igemnace | (~ian@user/igemnace) (Quit: WeeChat 4.1.2) |
| 2024-01-09 01:43:37 +0100 | EvanR | (~EvanR@user/evanr) (Quit: Leaving) |
| 2024-01-09 01:49:03 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-01-09 01:50:23 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 264 seconds) |
| 2024-01-09 01:51:32 +0100 | causal | (~eric@50.35.85.7) (Quit: WeeChat 4.1.1) |
| 2024-01-09 01:59:12 +0100 | pavonia | (~user@user/siracusa) |
| 2024-01-09 01:59:35 +0100 | astrolabe | (~astrolabe@astrolabe.plus.com) |
| 2024-01-09 02:00:53 +0100 | euleritian | (~euleritia@dynamic-089-015-238-167.89.15.238.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-01-09 02:01:09 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 02:02:02 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 02:02:48 +0100 | lingprefix | (~lingprefi@user/lingprefix) |
| 2024-01-09 02:02:54 +0100 | uiop1234 | (~uiop1234@202.220.233.220.static.exetel.com.au) |
| 2024-01-09 02:03:13 +0100 | uiop1234 | (~uiop1234@202.220.233.220.static.exetel.com.au) (Client Quit) |
| 2024-01-09 02:04:26 +0100 | uiop1234 | (~uiop1234@202.220.233.220.static.exetel.com.au) |
| 2024-01-09 02:06:34 +0100 | uiop1234 | (~uiop1234@202.220.233.220.static.exetel.com.au) () |
| 2024-01-09 02:12:48 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
| 2024-01-09 02:22:16 +0100 | mmhat | (~mmh@p200300f1c7428268ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.1.2) |
| 2024-01-09 02:23:04 +0100 | EvanR | (~EvanR@user/evanr) |
| 2024-01-09 02:24:36 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2024-01-09 02:25:21 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2024-01-09 02:25:59 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2024-01-09 02:26:27 +0100 | meritamen | (~meritamen@user/meritamen) |
| 2024-01-09 02:30:51 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-01-09 02:35:12 +0100 | <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? |
| 2024-01-09 02:38:49 +0100 | xff0x | (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) |
| 2024-01-09 02:39:36 +0100 | <Axman6> | what's a paramorphism again? |
| 2024-01-09 02:40:17 +0100 | <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. :) |
| 2024-01-09 02:40:49 +0100 | Axman6 | :highfive: |
| 2024-01-09 02:41:03 +0100 | <c_wraith> | https://www.reddit.com/r/haskell/comments/u1t237/the_visitor_pattern_and_catamorphisms/i4hycyy/ |
| 2024-01-09 02:42:23 +0100 | <Axman6> | <3 |
| 2024-01-09 02:44:03 +0100 | <Axman6> | I have a feeling the answer is no, at least not that Ive ever seen (though it could be doable with foldr?) |
| 2024-01-09 02:44:30 +0100 | <c_wraith> | it's awkward to do with foldr. Possible, but it loses efficiency. |
| 2024-01-09 02:47:46 +0100 | <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. |
| 2024-01-09 02:47:57 +0100 | <c_wraith> | (this time) |
| 2024-01-09 02:54:06 +0100 | ystael | (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 2024-01-09 02:55:03 +0100 | <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... |
| 2024-01-09 03:04:45 +0100 | <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 |
| 2024-01-09 03:05:33 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 2024-01-09 03:05:38 +0100 | <c_wraith> | Not just heads. taking every element out of the list, and returning that element and the rest of the list |
| 2024-01-09 03:10:40 +0100 | <c_wraith> | (that fmap is prepending the element to the rest of the returned lists, which is how you get everything back) |
| 2024-01-09 03:17:22 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-01-09 03:17:22 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 03:22:31 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 276 seconds) |
| 2024-01-09 03:25:59 +0100 | sroso | (~sroso@user/SrOso) |
| 2024-01-09 03:27:09 +0100 | sroso | (~sroso@user/SrOso) (Remote host closed the connection) |
| 2024-01-09 03:33:19 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 03:37:24 +0100 | sroso | (~sroso@user/SrOso) |
| 2024-01-09 03:37:57 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 252 seconds) |
| 2024-01-09 03:38:09 +0100 | Guest62 | (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) |
| 2024-01-09 03:38:40 +0100 | irrgit__ | (~irrgit@146.70.27.250) |
| 2024-01-09 03:42:18 +0100 | irrgit_ | (~irrgit@89.47.234.74) (Ping timeout: 256 seconds) |
| 2024-01-09 03:45:18 +0100 | rosco | (~rosco@175.136.156.77) |
| 2024-01-09 03:45:35 +0100 | shriekingnoise | (~shrieking@186.137.175.87) (Ping timeout: 264 seconds) |
| 2024-01-09 03:46:20 +0100 | Guest62 | (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) (Quit: Client closed) |
| 2024-01-09 03:49:22 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 03:55:52 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 2024-01-09 04:02:52 +0100 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-01-09 04:03:15 +0100 | xff0x | (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) (Ping timeout: 252 seconds) |
| 2024-01-09 04:04:13 +0100 | petrichor | (~znc-user@user/petrichor) |
| 2024-01-09 04:08:18 +0100 | <c_wraith> | lens has a function named "para" that says "technically a paramorphism" and the word "technically" is sure doing a lot of work.. |
| 2024-01-09 04:09:44 +0100 | <c_wraith> | like, yes. It is technically a paramorphism, but... it's sure a weird expression of it. |
| 2024-01-09 04:10:40 +0100 | <c_wraith> | > para (\ls rs -> case ls of [] -> [] ; (x:xs) -> case rs of [] -> [] ; (r:_) -> (x, xs): map (fmap (x:)) r) [1..5] |
| 2024-01-09 04:10:42 +0100 | <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])] |
| 2024-01-09 04:14:44 +0100 | jargon | (~jargon@211.sub-174-205-225.myvzw.com) |
| 2024-01-09 04:15:38 +0100 | jargon_ | (~jargon@211.sub-174-205-225.myvzw.com) |
| 2024-01-09 04:15:47 +0100 | Guest62 | (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) |
| 2024-01-09 04:16:11 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 2024-01-09 04:16:42 +0100 | jargon_ | (~jargon@211.sub-174-205-225.myvzw.com) (Killed (NickServ (GHOST command used by jargon))) |
| 2024-01-09 04:16:55 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 2024-01-09 04:17:17 +0100 | jargon | (~jargon@211.sub-174-205-225.myvzw.com) (Remote host closed the connection) |
| 2024-01-09 04:17:48 +0100 | jargon | (~jargon@211.sub-174-205-225.myvzw.com) |
| 2024-01-09 04:19:10 +0100 | Guest62 | (~Guest62@2404:7a84:31e0:d000:54a2:d4cd:3a78:1976) (Client Quit) |
| 2024-01-09 04:22:28 +0100 | meritamen | (~meritamen@user/meritamen) (Remote host closed the connection) |
| 2024-01-09 04:22:29 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:604b:dee:6683:e755) (Remote host closed the connection) |
| 2024-01-09 04:22:44 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) |
| 2024-01-09 04:25:39 +0100 | <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.) |
| 2024-01-09 04:32:44 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-01-09 04:33:31 +0100 | euleritian | (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) |
| 2024-01-09 04:34:33 +0100 | zeka | (~zeka@2600:1700:2121:180:fc1e:e1df:c7a6:218c) (Ping timeout: 268 seconds) |
| 2024-01-09 04:35:19 +0100 | zeka__ | (~zeka@2600:1700:2121:180:9966:d187:1602:11f9) |
| 2024-01-09 04:36:09 +0100 | astrolabe | (~astrolabe@astrolabe.plus.com) (Quit: Client closed) |
| 2024-01-09 04:47:17 +0100 | td_ | (~td@i53870925.versanet.de) (Ping timeout: 240 seconds) |
| 2024-01-09 04:47:19 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-01-09 04:49:22 +0100 | td_ | (~td@i53870924.versanet.de) |
| 2024-01-09 04:52:02 +0100 | <EvanR> | this is what happens when you used discovered stuff as opposed to invented xd |
| 2024-01-09 04:52:26 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 245 seconds) |
| 2024-01-09 04:54:59 +0100 | bilegeek | (~bilegeek@2600:1008:b0a5:5faa:ea63:51d4:70a3:2023) |
| 2024-01-09 04:56:28 +0100 | Jard | (~igork@78.84.190.186) (Remote host closed the connection) |
| 2024-01-09 04:58:13 +0100 | meritamen | (~meritamen@user/meritamen) |
| 2024-01-09 05:01:29 +0100 | phma | (~phma@2001:5b0:210d:7708:c2d8:8831:303c:d8e2) (Read error: Connection reset by peer) |
| 2024-01-09 05:01:57 +0100 | phma | (~phma@2001:5b0:210d:7708:ef47:fe3e:a28b:a600) |
| 2024-01-09 05:04:19 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 05:06:21 +0100 | aforemny_ | (~aforemny@i59F516FD.versanet.de) |
| 2024-01-09 05:07:30 +0100 | aforemny | (~aforemny@i59F516EE.versanet.de) (Ping timeout: 260 seconds) |
| 2024-01-09 05:10:53 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 252 seconds) |
| 2024-01-09 05:12:01 +0100 | thegeekinside | (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 2024-01-09 05:22:35 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 05:33:27 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 268 seconds) |
| 2024-01-09 05:33:49 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-01-09 05:45:09 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 05:47:13 +0100 | thegeekinside | (~thegeekin@189.217.90.224) |
| 2024-01-09 05:51:06 +0100 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Read error: Connection reset by peer) |
| 2024-01-09 05:52:17 +0100 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-01-09 05:52:43 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 2024-01-09 06:00:45 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 06:02:53 +0100 | trev | (~trev@user/trev) |
| 2024-01-09 06:03:06 +0100 | foul_owl | (~kerry@157.97.134.167) (Ping timeout: 260 seconds) |
| 2024-01-09 06:03:20 +0100 | euleritian | (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-01-09 06:03:38 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 06:04:14 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2024-01-09 06:05:07 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 255 seconds) |
| 2024-01-09 06:08:39 +0100 | rosco | (~rosco@175.136.156.77) (Quit: Lost terminal) |
| 2024-01-09 06:11:23 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:f7ce:4acc:831e:1a6e) |
| 2024-01-09 06:15:18 +0100 | phma_ | (~phma@host-67-44-208-148.hnremote.net) |
| 2024-01-09 06:15:20 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-01-09 06:15:21 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-01-09 06:15:21 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-01-09 06:15:51 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-01-09 06:15:52 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-01-09 06:16:15 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-01-09 06:18:42 +0100 | phma | (~phma@2001:5b0:210d:7708:ef47:fe3e:a28b:a600) (Ping timeout: 256 seconds) |
| 2024-01-09 06:21:32 +0100 | phma_ | phma |
| 2024-01-09 06:22:25 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-01-09 06:31:18 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-01-09 06:31:55 +0100 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-01-09 06:34:07 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 06:38:28 +0100 | <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 |
| 2024-01-09 06:39:12 +0100 | <Axman6> | it's also basically list zipper... so you could maybe do something fun with lens' zipper stuff |
| 2024-01-09 06:40:48 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 2024-01-09 06:57:07 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 07:03:34 +0100 | famubu | (~julinuser@user/famubu) (Quit: leaving) |
| 2024-01-09 07:06:11 +0100 | Katarushisu1 | (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) (Ping timeout: 245 seconds) |
| 2024-01-09 07:10:23 +0100 | xdminsy | (~xdminsy@117.147.71.169) |
| 2024-01-09 07:14:03 +0100 | Katarushisu1 | (~Katarushi@cpc147790-finc20-2-0-cust502.4-2.cable.virginm.net) |
| 2024-01-09 07:14:37 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-01-09 07:19:38 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-01-09 07:19:55 +0100 | euleritian | (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) |
| 2024-01-09 07:20:29 +0100 | <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 |
| 2024-01-09 07:20:38 +0100 | <c_wraith> | Including one from the ghc package! |
| 2024-01-09 07:21:32 +0100 | famubu | (~julinuser@user/famubu) |
| 2024-01-09 07:22:05 +0100 | <famubu> | Is it possible to have a function returning a type (as in 'Int', 'Bool', etc) in haskell? By means of an extension maybe? |
| 2024-01-09 07:22:50 +0100 | <famubu> | Like: `foo :: Int -> Type` where `foo 2` returns `Bool` and `foo 1` returns `()`. |
| 2024-01-09 07:23:13 +0100 | irrgit_ | (~irrgit@89.47.234.74) |
| 2024-01-09 07:25:49 +0100 | <famubu> | Or even TemplateHaskell? |
| 2024-01-09 07:25:52 +0100 | <c_wraith> | famubu: no. |
| 2024-01-09 07:25:59 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-01-09 07:26:05 +0100 | irrgit__ | (~irrgit@146.70.27.250) (Ping timeout: 240 seconds) |
| 2024-01-09 07:26:09 +0100 | <c_wraith> | famubu: you can return Either Int Bool |
| 2024-01-09 07:26:26 +0100 | <c_wraith> | But types need to be checked without knowing their runtime values |
| 2024-01-09 07:27:01 +0100 | <c_wraith> | types exist only at compile time |
| 2024-01-09 07:27:52 +0100 | <famubu> | Oh.. |
| 2024-01-09 07:35:22 +0100 | michalz | (~michalz@185.246.207.221) |
| 2024-01-09 07:35:59 +0100 | igemnace | (~ian@user/igemnace) |
| 2024-01-09 07:36:06 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds) |
| 2024-01-09 07:37:45 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-01-09 07:38:20 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-01-09 07:43:07 +0100 | <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 |
| 2024-01-09 07:46:27 +0100 | <haskellbridge> | 05<irregularsphere> c_wraith: sorry if I'm being pedantic, but I don't think hackage can search for types? rather hoogle |
| 2024-01-09 07:46:54 +0100 | <c_wraith> | irregularsphere: you are completely correct. I just typed the wrong thing |
| 2024-01-09 07:48:02 +0100 | <Axman6> | famubu: you could use a type family to do that though. You are getting very close to (well actually ast) dependent types |
| 2024-01-09 07:48:07 +0100 | <Axman6> | as* |
| 2024-01-09 07:50:12 +0100 | <jackdk> | You could also have a type family that turns a Nat into a Type |
| 2024-01-09 07:50:30 +0100 | <jackdk> | And a singleton to reflect a value up into the type |
| 2024-01-09 07:54:02 +0100 | <Axman6> | GADTs might also help |
| 2024-01-09 07:54:12 +0100 | <Axman6> | So many options! |
| 2024-01-09 07:54:50 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-01-09 07:55:47 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 264 seconds) |
| 2024-01-09 07:55:50 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-01-09 07:56:59 +0100 | foul_owl | (~kerry@174-21-148-34.tukw.qwest.net) |
| 2024-01-09 08:03:50 +0100 | acidjnk | (~acidjnk@2003:d6:e72b:9308:1c56:4b97:a161:31b) |
| 2024-01-09 08:08:03 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 08:08:32 +0100 | hexology | (~hexology@user/hexology) (Quit: hex on you ...) |
| 2024-01-09 08:12:41 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 2024-01-09 08:12:50 +0100 | <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. |
| 2024-01-09 08:14:27 +0100 | <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) |
| 2024-01-09 08:14:57 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-01-09 08:19:06 +0100 | EvanR | (~EvanR@user/evanr) (Ping timeout: 245 seconds) |
| 2024-01-09 08:24:17 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 08:41:23 +0100 | xff0x | (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) |
| 2024-01-09 08:41:31 +0100 | Square2 | (~Square4@user/square) |
| 2024-01-09 08:42:02 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-01-09 08:42:55 +0100 | <haskellbridge> | 05<irregularsphere> What's a stackverse? |
| 2024-01-09 08:44:34 +0100 | Square | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2024-01-09 08:45:06 +0100 | <int-e> | stack + stackage + community (the alternative would probably be cabal + hackage + community, and of course there's a huge overlap) |
| 2024-01-09 08:48:37 +0100 | foul_owl | (~kerry@174-21-148-34.tukw.qwest.net) (Ping timeout: 268 seconds) |
| 2024-01-09 08:58:24 +0100 | puke | (~puke@user/puke) (Read error: Connection reset by peer) |
| 2024-01-09 08:59:16 +0100 | puke | (~puke@user/puke) |
| 2024-01-09 09:01:49 +0100 | foul_owl | (~kerry@185.216.231.181) |
| 2024-01-09 09:06:17 +0100 | CiaoSen | (~Jura@2a05:5800:2c0:fb00:ca4b:d6ff:fec1:99da) |
| 2024-01-09 09:06:21 +0100 | <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 |
| 2024-01-09 09:07:49 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-01-09 09:09:31 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 2024-01-09 09:11:46 +0100 | euleritian | (~euleritia@dynamic-089-015-239-142.89.15.239.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-01-09 09:12:05 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 09:19:55 +0100 | gmg | (~user@user/gehmehgeh) |
| 2024-01-09 09:27:19 +0100 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2024-01-09 09:27:45 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 252 seconds) |
| 2024-01-09 09:28:07 +0100 | ec | (~ec@gateway/tor-sasl/ec) |
| 2024-01-09 09:30:52 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 09:35:20 +0100 | waldo | (~waldo@user/waldo) (Ping timeout: 256 seconds) |
| 2024-01-09 09:39:26 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 09:41:52 +0100 | miguelnegrao | (~miguelneg@2001:818:dc71:d100:e682:f5cd:9590:d961) |
| 2024-01-09 09:42:28 +0100 | mikess | (~mikess@user/mikess) (Ping timeout: 255 seconds) |
| 2024-01-09 09:44:32 +0100 | <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. |
| 2024-01-09 09:45:35 +0100 | <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. |
| 2024-01-09 09:45:36 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2024-01-09 09:46:12 +0100 | <miguelnegrao> | Is there no hope of using a Nat such as the one I have above for realist values we encounter in actual code ? |
| 2024-01-09 09:46:48 +0100 | mikess | (~mikess@user/mikess) |
| 2024-01-09 09:47:35 +0100 | <lortabac> | miguelnegrao: depending on your use case, you may be able to use GHC's built-in Nat type |
| 2024-01-09 09:47:42 +0100 | <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) |
| 2024-01-09 09:48:41 +0100 | a51 | (a51@gateway/vpn/protonvpn/a51) (Ping timeout: 245 seconds) |
| 2024-01-09 09:50:15 +0100 | <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... |
| 2024-01-09 09:51:30 +0100 | <tomsmeding> | you're mostly at the mercy of the plugins (in addition to the mentioned one there's also a constraint simplification plugin), yes |
| 2024-01-09 09:52:50 +0100 | <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 ... |
| 2024-01-09 09:53:35 +0100 | <tomsmeding> | I'm not sure haskell is the proper place for that :D |
| 2024-01-09 09:53:38 +0100 | <tomsmeding> | try agda |
| 2024-01-09 09:53:42 +0100 | <tomsmeding> | it's fairly haskell-like |
| 2024-01-09 09:53:53 +0100 | <tomsmeding> | idris also fits the bill I believe, but I've never used idris |
| 2024-01-09 09:53:58 +0100 | <int-e> | you could probably cook up a binary representation but you'll have to pay for that in the proofs |
| 2024-01-09 09:53:58 +0100 | <miguelnegrao> | tomsmending: I know, I know... but I love haskell too much :-D |
| 2024-01-09 09:54:09 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 2024-01-09 09:54:18 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 268 seconds) |
| 2024-01-09 09:54:19 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
| 2024-01-09 09:55:10 +0100 | <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. |
| 2024-01-09 09:55:51 +0100 | <tomsmeding> | yeah if you go full-on singletons (whether generated or hand-written) you can do quite a lot |
| 2024-01-09 09:56:24 +0100 | <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 |
| 2024-01-09 09:56:34 +0100 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) () |
| 2024-01-09 09:57:37 +0100 | <tomsmeding> | % :set -XNoTypeInType |
| 2024-01-09 09:57:37 +0100 | <yahb2> | <no output> |
| 2024-01-09 09:57:39 +0100 | <tomsmeding> | % :k Type |
| 2024-01-09 09:57:40 +0100 | <yahb2> | Type :: Type |
| 2024-01-09 09:57:51 +0100 | <tomsmeding> | and support for NoTypeInType is long gone :D |
| 2024-01-09 09:58:26 +0100 | <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 ? |
| 2024-01-09 09:58:48 +0100 | <tomsmeding> | let myReallyNotUndefined = myReallyNotUndefined |
| 2024-01-09 09:58:59 +0100 | <tomsmeding> | it will definitely compile |
| 2024-01-09 09:59:21 +0100 | <miguelnegrao> | so it will loop at runtime, in that case. |
| 2024-01-09 09:59:27 +0100 | <tomsmeding> | yeah |
| 2024-01-09 09:59:36 +0100 | <miguelnegrao> | Then you know you've made a mistake. :-) |
| 2024-01-09 09:59:53 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 10:00:00 +0100 | <miguelnegrao> | but I see your point, the whole ideia is to catch problems at compile time. |
| 2024-01-09 10:00:13 +0100 | <miguelnegrao> | One has to be careful with that. |
| 2024-01-09 10:00:17 +0100 | <tomsmeding> | hmm, perhaps, but if I remember correctly there was a way to have that code not run at runtime |
| 2024-01-09 10:00:40 +0100 | <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 |
| 2024-01-09 10:00:46 +0100 | <tomsmeding> | :p |
| 2024-01-09 10:00:52 +0100 | <haskellbridge> | 05<irregularsphere> miguelnegrao: if infinite recursion doesn't compile then the compiler solves the halting problem |
| 2024-01-09 10:01:07 +0100 | <haskellbridge> | 05<irregularsphere> (provably impossible) |
| 2024-01-09 10:02:06 +0100 | <miguelnegrao> | haskellbridge: yes, good point. |
| 2024-01-09 10:02:25 +0100 | sroso | (~sroso@user/SrOso) (Read error: Connection reset by peer) |
| 2024-01-09 10:03:53 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2024-01-09 10:04:50 +0100 | <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. |
| 2024-01-09 10:05:44 +0100 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-01-09 10:05:46 +0100 | nschoe2 | (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) |
| 2024-01-09 10:05:51 +0100 | <miguelnegrao> | They are building dependent types into Haskell, so I suppose the consider the effort worth it somehow... |
| 2024-01-09 10:06:05 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 240 seconds) |
| 2024-01-09 10:06:11 +0100 | <miguelnegrao> | (possibly not for proofs...) |
| 2024-01-09 10:06:31 +0100 | <c_wraith> | Eh. The compiler doesn't need to solve the halting problem to reject code that it can't prove terminates. |
| 2024-01-09 10:06:50 +0100 | <c_wraith> | There are lots of languages with that feature. |
| 2024-01-09 10:07:36 +0100 | <miguelnegrao> | Although you can't really almost do anything with for instance a Nat indexed Vec without proofs. |
| 2024-01-09 10:08:10 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 256 seconds) |
| 2024-01-09 10:08:14 +0100 | <miguelnegrao> | c_wraith: that's a termination checker, right ? |
| 2024-01-09 10:08:24 +0100 | <c_wraith> | yes. |
| 2024-01-09 10:10:06 +0100 | <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" |
| 2024-01-09 10:10:19 +0100 | <haskellbridge> | 05<irregularsphere> c_wraith: yeah i suppose we can't have a perfect one |
| 2024-01-09 10:11:01 +0100 | Square2 | (~Square4@user/square) |
| 2024-01-09 10:11:15 +0100 | barak | (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) |
| 2024-01-09 10:12:30 +0100 | <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 |
| 2024-01-09 10:13:29 +0100 | <c_wraith> | which is roughly equivalent to how haskell handles inconsistent types anyway |
| 2024-01-09 10:14:34 +0100 | <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 |
| 2024-01-09 10:15:43 +0100 | <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. |
| 2024-01-09 10:17:12 +0100 | <c_wraith> | Ok, not totally on standby, but now like 5 years behind the initial plan as the obstacles are very slowly smoothed out :) |
| 2024-01-09 10:17:41 +0100 | <miguelnegrao> | Yeah, it's a hard problem... |
| 2024-01-09 10:20:14 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 260 seconds) |
| 2024-01-09 10:20:34 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-01-09 10:21:11 +0100 | <miguelnegrao> | Still, this issue with GHC.TypeLit vs inductive Nats and perfomance of inductive Nats seems unresolved... |
| 2024-01-09 10:21:19 +0100 | <haskellbridge> | 05<irregularsphere> c_wraith: "...the programmer has to provide it" reminds me of the 3*n+1 conjecture |
| 2024-01-09 10:22:14 +0100 | <c_wraith> | That's absolutely one a termination checker would say "that's up to you" about |
| 2024-01-09 10:22:21 +0100 | <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. " |
| 2024-01-09 10:24:12 +0100 | <haskellbridge> | 05<irregularsphere> c_wraith: ...The proof is left as an exercise to the programmer |
| 2024-01-09 10:24:14 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-01-09 10:26:29 +0100 | <miguelnegrao> | "Well, I have a very nice proof of that, it just doesn't fit on the side of this page..." |
| 2024-01-09 10:26:55 +0100 | <haskellbridge> | 05<irregularsphere> "It's trivial." |
| 2024-01-09 10:29:17 +0100 | <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. |
| 2024-01-09 10:30:28 +0100 | <c_wraith> | (without the pain of using singletons) |
| 2024-01-09 10:31:57 +0100 | xff0x | (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) (Ping timeout: 256 seconds) |
| 2024-01-09 10:32:24 +0100 | <haskellbridge> | 05<irregularsphere> I was thinking of a () -> a, but I'm not sure if that's idiomatic |
| 2024-01-09 10:32:26 +0100 | ubert | (~Thunderbi@p200300ecdf2683a8da5ffe35771476c1.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2024-01-09 10:32:39 +0100 | <haskellbridge> | 05<irregularsphere> :t const |
| 2024-01-09 10:32:52 +0100 | <haskellbridge> | 05<irregularsphere> > :t const |
| 2024-01-09 10:33:04 +0100 | <haskellbridge> | 05<irregularsphere> const :: a -> b -> a |
| 2024-01-09 10:33:18 +0100 | <c_wraith> | sorry, the bots don't recognize how the matrix bridge relays messages on the IRC side |
| 2024-01-09 10:33:27 +0100 | <haskellbridge> | 05<irregularsphere> huh |
| 2024-01-09 10:34:12 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-01-09 10:36:23 +0100 | <haskellbridge> | 05<irregularsphere> actually wait () -> a isn't a singleton |
| 2024-01-09 10:36:26 +0100 | <haskellbridge> | 05<irregularsphere> it's isomorphic to a |
| 2024-01-09 10:37:25 +0100 | nschoe2 | (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) (Quit: WeeChat 4.1.2) |
| 2024-01-09 10:37:56 +0100 | thegeekinside | (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 2024-01-09 10:41:02 +0100 | <miguelnegrao> | Do you mean Void -> a ? |
| 2024-01-09 10:41:20 +0100 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2024-01-09 10:41:33 +0100 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2024-01-09 10:42:14 +0100 | <haskellbridge> | 05<irregularsphere> Void has no inhabitants |
| 2024-01-09 10:42:33 +0100 | <haskellbridge> | 05<irregularsphere> hence why absurd (:: Void -> a) is called absurd |
| 2024-01-09 10:43:44 +0100 | <haskellbridge> | 05<irregularsphere> meanwhile () has an inhabitant, called () |
| 2024-01-09 10:44:23 +0100 | <haskellbridge> | 05<irregularsphere> and only () |
| 2024-01-09 10:46:54 +0100 | <haskellbridge> | 05<irregularsphere> actually wait you have a good point |
| 2024-01-09 10:46:56 +0100 | <ncf> | Void -> a is also a singleton |
| 2024-01-09 10:47:03 +0100 | <haskellbridge> | 05<irregularsphere> Void -> a is a singleton yes |
| 2024-01-09 10:47:05 +0100 | <haskellbridge> | 05<irregularsphere> but is it usable |
| 2024-01-09 10:47:47 +0100 | <famubu> | What's the use of type roles? Does anyone know of a good resource preferably with examples where we can read about it? |
| 2024-01-09 10:48:17 +0100 | <famubu> | And where is this room bridged to? is it some other public space? |
| 2024-01-09 10:48:30 +0100 | <haskellbridge> | 05<irregularsphere> #haskell-irc:matrix.org |
| 2024-01-09 10:48:37 +0100 | <famubu> | Ah.. |
| 2024-01-09 10:49:27 +0100 | <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%…). |
| 2024-01-09 10:49:53 +0100 | <famubu> | But I didn't get the example mentioned there. |
| 2024-01-09 10:50:12 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 10:50:12 +0100 | <miguelnegrao> | Void -> a is ex falso quodlibet (EFQ) from False (Void) any proposition follows. And a -> Void is "not a". At least in Lean ... |
| 2024-01-09 10:50:51 +0100 | <int-e> | famubu: The example would coerce Inspect Int (= Bool) to Inspect Age (= Int) |
| 2024-01-09 10:51:46 +0100 | <famubu> | int-e: Is that coercion an example representational type role or of nominal? |
| 2024-01-09 10:52:16 +0100 | <famubu> | I thought nominal needed exact same thing? it looked more like 'representational equivality' |
| 2024-01-09 10:52:45 +0100 | miguelnegrao | (~miguelneg@2001:818:dc71:d100:e682:f5cd:9590:d961) (Quit: miguelnegrao) |
| 2024-01-09 10:52:54 +0100 | <famubu> | `data Complex a = MkComplex (F a)` is mentioned as example of nominal type role |
| 2024-01-09 10:53:01 +0100 | <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.). |
| 2024-01-09 10:55:20 +0100 | <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... |
| 2024-01-09 10:55:26 +0100 | <int-e> | ...ultimately more devastating example) |
| 2024-01-09 10:56:18 +0100 | cfricke | (~cfricke@user/cfricke) |
| 2024-01-09 10:56:40 +0100 | wheatengineer | (~frederik@p200300f63f3a4600180a52eefcdcc2d6.dip0.t-ipconnect.de) |
| 2024-01-09 10:59:51 +0100 | nschoe | (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) |
| 2024-01-09 11:02:19 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) |
| 2024-01-09 11:02:54 +0100 | <famubu> | Okay, so one of the uses for type role nominal is to prevent coercions? |
| 2024-01-09 11:03:31 +0100 | <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? |
| 2024-01-09 11:03:53 +0100 | <famubu> | And where does representational come in handy? |
| 2024-01-09 11:04:18 +0100 | <famubu> | Isn't coercion possible only when there representations of the two types are same? Or something like that? |
| 2024-01-09 11:04:47 +0100 | <famubu> | Type role is for specific type parameter of a type, is it? |
| 2024-01-09 11:05:01 +0100 | <famubu> | It's like 'the role of a parameter in the type' |
| 2024-01-09 11:05:19 +0100 | <famubu> | When I first heard the name type role, I thought it was something related to the entire type as a whole. |
| 2024-01-09 11:05:50 +0100 | xdminsy | (~xdminsy@117.147.71.169) (Ping timeout: 268 seconds) |
| 2024-01-09 11:06:09 +0100 | xdminsy | (~xdminsy@117.147.71.169) |
| 2024-01-09 11:06:50 +0100 | danse-nr3 | (~danse@151.43.165.56) |
| 2024-01-09 11:07:23 +0100 | phma | (~phma@host-67-44-208-148.hnremote.net) (Read error: Connection reset by peer) |
| 2024-01-09 11:08:17 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-171.elisa-laajakaista.fi) |
| 2024-01-09 11:08:26 +0100 | phma | (~phma@host-67-44-208-144.hnremote.net) |
| 2024-01-09 11:09:24 +0100 | <famubu> | Is it that a type role is mentioned only for the last type argument of a type? |
| 2024-01-09 11:12:23 +0100 | meritamen | (~meritamen@user/meritamen) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-01-09 11:15:28 +0100 | <famubu> | No, type roles is for all arguments of type. |
| 2024-01-09 11:16:42 +0100 | igemnace | (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 2024-01-09 11:18:12 +0100 | rosco | (~rosco@175.136.156.77) |
| 2024-01-09 11:18:26 +0100 | <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. |
| 2024-01-09 11:18:43 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-01-09 11:18:49 +0100 | <famubu> | int-e: Thanks |
| 2024-01-09 11:19:11 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-01-09 11:19:57 +0100 | <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. |
| 2024-01-09 11:21:36 +0100 | acidjnk | (~acidjnk@2003:d6:e72b:9308:1c56:4b97:a161:31b) (Ping timeout: 245 seconds) |
| 2024-01-09 11:24:19 +0100 | meritamen | (~meritamen@user/meritamen) |
| 2024-01-09 11:27:58 +0100 | not_reserved | (~not_reser@185.153.177.191) |
| 2024-01-09 11:29:41 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) (Remote host closed the connection) |
| 2024-01-09 11:33:09 +0100 | waldo | (~waldo@user/waldo) (Ping timeout: 252 seconds) |
| 2024-01-09 11:34:38 +0100 | igemnace | (~ian@user/igemnace) |
| 2024-01-09 11:36:04 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds) |
| 2024-01-09 11:52:46 +0100 | chele | (~chele@user/chele) |
| 2024-01-09 12:04:18 +0100 | tertek | (~tertek@user/tertek) (Ping timeout: 260 seconds) |
| 2024-01-09 12:05:49 +0100 | meritamen | (~meritamen@user/meritamen) (Remote host closed the connection) |
| 2024-01-09 12:05:56 +0100 | tertek | (~tertek@user/tertek) |
| 2024-01-09 12:06:26 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) |
| 2024-01-09 12:12:54 +0100 | <haskellbridge> | 05<irregularsphere> did haskell invent everything |
| 2024-01-09 12:13:34 +0100 | <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) |
| 2024-01-09 12:14:40 +0100 | <haskellbridge> | 05<irregularsphere> amazing features btw |
| 2024-01-09 12:21:09 +0100 | Luj | (~Luj@2a01:e0a:5f9:9681:2ea5:d487:e077:51db) (Quit: Ping timeout (120 seconds)) |
| 2024-01-09 12:21:28 +0100 | Luj | (~Luj@2a01:e0a:5f9:9681:f715:669b:cfa9:834a) |
| 2024-01-09 12:24:17 +0100 | AndreiDuma | (~textual@95.76.23.32) |
| 2024-01-09 12:25:53 +0100 | kmein | (~weechat@user/kmein) (Quit: ciao kakao) |
| 2024-01-09 12:26:24 +0100 | AndreiDuma | (~textual@95.76.23.32) () |
| 2024-01-09 12:26:27 +0100 | AndreiDuma | (~textual@95.76.23.32) |
| 2024-01-09 12:27:04 +0100 | causal | (~eric@50.35.85.7) |
| 2024-01-09 12:36:11 +0100 | Square2 | (~Square4@user/square) |
| 2024-01-09 12:37:05 +0100 | kmein | (~weechat@user/kmein) |
| 2024-01-09 12:39:23 +0100 | bilegeek | (~bilegeek@2600:1008:b0a5:5faa:ea63:51d4:70a3:2023) (Quit: Leaving) |
| 2024-01-09 12:39:24 +0100 | xff0x | (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) |
| 2024-01-09 12:42:39 +0100 | mikess | (~mikess@user/mikess) (Ping timeout: 268 seconds) |
| 2024-01-09 12:42:46 +0100 | meritamen | (~meritamen@user/meritamen) |
| 2024-01-09 12:46:08 +0100 | mmhat | (~mmh@p200300f1c7428268ee086bfffe095315.dip0.t-ipconnect.de) |
| 2024-01-09 12:46:22 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-01-09 12:54:40 +0100 | puke | (~puke@user/puke) (Ping timeout: 268 seconds) |
| 2024-01-09 13:00:54 +0100 | danse-nr3 | (~danse@151.43.165.56) (Read error: Connection reset by peer) |
| 2024-01-09 13:22:22 +0100 | acidjnk | (~acidjnk@p200300d6e72b930818892410b5265f00.dip0.t-ipconnect.de) |
| 2024-01-09 13:22:53 +0100 | nschoe | (~nschoe@2a01:e0a:8e:a190:7977:996:497e:66b1) (Ping timeout: 240 seconds) |
| 2024-01-09 13:26:04 +0100 | lingprefix | (~lingprefi@user/lingprefix) (Quit: leaving) |
| 2024-01-09 13:28:32 +0100 | AndreiDuma | (~textual@95.76.23.32) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-01-09 13:37:04 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 13:43:14 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 260 seconds) |
| 2024-01-09 13:47:27 +0100 | vglfr | (~vglfr@234.red-88-6-215.staticip.rima-tde.net) (Ping timeout: 256 seconds) |
| 2024-01-09 13:48:37 +0100 | vglfr | (~vglfr@90.167.190.99) |
| 2024-01-09 13:49:11 +0100 | AndreiDuma | (~textual@95.76.23.32) |
| 2024-01-09 14:04:45 +0100 | vglfr | (~vglfr@90.167.190.99) (Read error: Connection reset by peer) |
| 2024-01-09 14:05:29 +0100 | vglfr | (~vglfr@234.red-88-6-215.staticip.rima-tde.net) |
| 2024-01-09 14:22:46 +0100 | mikess | (~mikess@user/mikess) |
| 2024-01-09 14:25:25 +0100 | ryantrinkle | (~ryantrink@140.174.247.171) |
| 2024-01-09 14:26:10 +0100 | <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 |
| 2024-01-09 14:26:30 +0100 | <ryantrinkle> | it's a somewhat large project (hundreds of modules, hundreds of deps), but it has not even started mentioning loading modules |
| 2024-01-09 14:27:00 +0100 | <ryantrinkle> | ghc-iserv-prof has been at 100% CPU the whole time |
| 2024-01-09 14:27:14 +0100 | <ryantrinkle> | (this is running with -fexternal-interpreter -prof) |
| 2024-01-09 14:43:31 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 2024-01-09 15:01:51 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) (Remote host closed the connection) |
| 2024-01-09 15:02:20 +0100 | ryantrinkle | (~ryantrink@140.174.247.171) () |
| 2024-01-09 15:05:21 +0100 | CiaoSen | (~Jura@2a05:5800:2c0:fb00:ca4b:d6ff:fec1:99da) (Ping timeout: 245 seconds) |
| 2024-01-09 15:05:41 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) |
| 2024-01-09 15:08:03 +0100 | danse-nr3 | (~danse@151.43.184.127) |
| 2024-01-09 15:08:55 +0100 | thegeekinside | (~thegeekin@189.217.90.224) |
| 2024-01-09 15:10:37 +0100 | cfricke | (~cfricke@user/cfricke) (Ping timeout: 246 seconds) |
| 2024-01-09 15:12:36 +0100 | shriekingnoise | (~shrieking@186.137.175.87) |
| 2024-01-09 15:13:37 +0100 | phma | (~phma@host-67-44-208-144.hnremote.net) (Read error: Connection reset by peer) |
| 2024-01-09 15:14:05 +0100 | phma | (~phma@host-67-44-208-144.hnremote.net) |
| 2024-01-09 15:27:02 +0100 | EvanR | (~EvanR@user/evanr) |
| 2024-01-09 15:27:29 +0100 | EvanR | (~EvanR@user/evanr) (Remote host closed the connection) |
| 2024-01-09 15:28:38 +0100 | EvanR | (~EvanR@user/evanr) |
| 2024-01-09 15:32:14 +0100 | ystael | (~ystael@user/ystael) |
| 2024-01-09 15:33:03 +0100 | jargon | (~jargon@211.sub-174-205-225.myvzw.com) (Read error: Connection reset by peer) |
| 2024-01-09 15:35:35 +0100 | ryantrinkle | (~ryantrink@140.174.247.171) |
| 2024-01-09 15:40:30 +0100 | eggplant_ | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 2024-01-09 15:41:53 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d0ca:3ec7:17:7000) (Quit: ubert) |
| 2024-01-09 15:42:04 +0100 | ubert1 | (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) |
| 2024-01-09 15:42:21 +0100 | ubert1 | (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) (Client Quit) |
| 2024-01-09 15:43:06 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:9c77:5ce5:f4fd:7eca) (Ping timeout: 260 seconds) |
| 2024-01-09 15:43:35 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) |
| 2024-01-09 15:44:23 +0100 | xff0x | (~xff0x@133-175-35-58.east.fdn.vectant.ne.jp) (Ping timeout: 264 seconds) |
| 2024-01-09 15:46:34 +0100 | <EvanR> | famubu, that kind of function is technically possible using dependent types, which haskell doesn't have but other languages do |
| 2024-01-09 15:47:07 +0100 | <EvanR> | though that example is a bit contrived and not that motivating for such complexity |
| 2024-01-09 15:48:21 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-01-09 15:48:36 +0100 | euleritian | (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) |
| 2024-01-09 16:03:08 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2024-01-09 16:04:51 +0100 | rosco | (~rosco@175.136.156.77) (Quit: Lost terminal) |
| 2024-01-09 16:06:21 +0100 | a51 | (a51@gateway/vpn/protonvpn/a51) |
| 2024-01-09 16:09:53 +0100 | AndreiDuma | (~textual@95.76.23.32) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-01-09 16:16:52 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2024-01-09 16:19:06 +0100 | mmhat | (~mmh@p200300f1c7428268ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2024-01-09 16:19:28 +0100 | mmhat | (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) |
| 2024-01-09 16:21:52 +0100 | wheatengineer | (~frederik@p200300f63f3a4600180a52eefcdcc2d6.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2024-01-09 16:25:19 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800:e199:9848:c5f0:b040) |
| 2024-01-09 16:26:27 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-01-09 16:26:42 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 256 seconds) |
| 2024-01-09 16:31:06 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.1.1) |
| 2024-01-09 16:33:39 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-01-09 16:38:31 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 2024-01-09 16:48:03 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-01-09 16:52:47 +0100 | euleritian | (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-01-09 16:53:00 +0100 | a51 | (a51@gateway/vpn/protonvpn/a51) (Quit: WeeChat 4.1.2) |
| 2024-01-09 16:53:06 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 16:57:39 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-01-09 16:58:38 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 17:03:12 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-01-09 17:04:02 +0100 | not_reserved | (~not_reser@185.153.177.191) (Quit: Client closed) |
| 2024-01-09 17:06:37 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-01-09 17:07:59 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800:e199:9848:c5f0:b040) (Quit: Leaving) |
| 2024-01-09 17:10:04 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800:2698:eca0:c269:b854) |
| 2024-01-09 17:11:35 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:ddbb:f550:1f2a:8658) (Ping timeout: 256 seconds) |
| 2024-01-09 17:16:00 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-01-09 17:17:23 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 2024-01-09 17:17:54 +0100 | euleritian | (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) |
| 2024-01-09 17:18:29 +0100 | not_reserved | (~not_reser@185.153.177.191) |
| 2024-01-09 17:20:39 +0100 | ph88 | (~ph88@2a02:8109:9e26:c800:2698:eca0:c269:b854) (Ping timeout: 256 seconds) |
| 2024-01-09 17:23:02 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 2024-01-09 17:24:24 +0100 | meritamen | (~meritamen@user/meritamen) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-01-09 17:25:01 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 2024-01-09 17:29:17 +0100 | phma | (~phma@host-67-44-208-144.hnremote.net) (Read error: Connection reset by peer) |
| 2024-01-09 17:29:39 +0100 | a51 | (a51@gateway/vpn/protonvpn/a51) |
| 2024-01-09 17:36:03 +0100 | phma | (~phma@2001:5b0:211f:6828:6be8:2d10:9148:6096) |
| 2024-01-09 17:39:00 +0100 | not_reserved | (~not_reser@185.153.177.191) (Quit: Client closed) |
| 2024-01-09 17:44:03 +0100 | eggplant_ | (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2024-01-09 17:44:19 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d504:f200:d614:49c6) |
| 2024-01-09 17:46:43 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 2024-01-09 17:49:06 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 260 seconds) |
| 2024-01-09 17:50:33 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2024-01-09 17:55:08 +0100 | mmhat | (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.1.2) |
| 2024-01-09 17:57:56 +0100 | mmhat | (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) |
| 2024-01-09 17:59:50 +0100 | mmhat | (~mmh@p200300f1c74282ceee086bfffe095315.dip0.t-ipconnect.de) (Client Quit) |
| 2024-01-09 17:59:55 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2024-01-09 18:01:58 +0100 | danse-nr3 | (~danse@151.43.184.127) (Ping timeout: 276 seconds) |
| 2024-01-09 18:03:10 +0100 | alp_ | (~alp@2001:861:e3d6:8f80:f7ce:4acc:831e:1a6e) (Ping timeout: 246 seconds) |
| 2024-01-09 18:06:50 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 2024-01-09 18:08:46 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 18:11:05 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 18:15:37 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 2024-01-09 18:19:42 +0100 | <cheater> | hi |
| 2024-01-09 18:19:47 +0100 | <cheater> | anyone got a good monad tutorial? |
| 2024-01-09 18:23:15 +0100 | not_reserved | (~not_reser@185.153.177.191) |
| 2024-01-09 18:24:51 +0100 | mechap | (~mechap@user/mechap) |
| 2024-01-09 18:25:34 +0100 | <duncan> | cheater: https://blog.ploeh.dk/2017/10/04/from-design-patterns-to-category-theory/ |
| 2024-01-09 18:25:53 +0100 | <cheater> | nice |
| 2024-01-09 18:26:41 +0100 | <EvanR> | lol https://wiki.haskell.org/Monad_tutorials_timeline |
| 2024-01-09 18:29:38 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 18:31:46 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
| 2024-01-09 18:33:50 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-01-09 18:34:26 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 260 seconds) |
| 2024-01-09 18:34:42 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-01-09 18:35:27 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 2024-01-09 18:36:18 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 2024-01-09 18:38:47 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-01-09 18:42:29 +0100 | waldo | (~waldo@user/waldo) (Ping timeout: 240 seconds) |
| 2024-01-09 18:43:10 +0100 | <tomsmeding> | it's even on the list! |
| 2024-01-09 18:44:52 +0100 | barak | (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) (Remote host closed the connection) |
| 2024-01-09 18:46:10 +0100 | barak | (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) |
| 2024-01-09 18:46:51 +0100 | <duncan> | Seemann writes so well and that series is so comprehensive. Great stuff. |
| 2024-01-09 18:47:09 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 18:47:29 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 18:47:40 +0100 | <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 |
| 2024-01-09 18:48:07 +0100 | <EvanR> | I mean, idiomatic block structured ruby code which is doing something that haskell files under "monads" |
| 2024-01-09 18:50:34 +0100 | <EvanR> | that I cannot find or remember |
| 2024-01-09 18:54:51 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-01-09 18:55:39 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-01-09 18:56:15 +0100 | xsarnik | (xsarnik@lounge.fi.muni.cz) (Quit: Ping timeout (120 seconds)) |
| 2024-01-09 18:56:44 +0100 | igemnace | (~ian@user/igemnace) (Quit: WeeChat 4.1.2) |
| 2024-01-09 18:56:59 +0100 | ricardo2 | (~ricardo@84.16.179.218) (Ping timeout: 264 seconds) |
| 2024-01-09 18:57:04 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Quit: Restarting) |
| 2024-01-09 18:57:14 +0100 | michalz_ | (~michalz@185.246.207.201) |
| 2024-01-09 18:57:15 +0100 | ricardo1 | (~ricardo@84.16.179.218) |
| 2024-01-09 18:57:22 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2024-01-09 18:57:31 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) |
| 2024-01-09 18:58:47 +0100 | michalz | (~michalz@185.246.207.221) (Ping timeout: 264 seconds) |
| 2024-01-09 19:01:37 +0100 | xsarnik | (xsarnik@lounge.fi.muni.cz) |
| 2024-01-09 19:02:15 +0100 | bah | (~bah@l1.tel) (Ping timeout: 260 seconds) |
| 2024-01-09 19:02:23 +0100 | bah | (~bah@l1.tel) |
| 2024-01-09 19:02:31 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 240 seconds) |
| 2024-01-09 19:02:55 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 240 seconds) |
| 2024-01-09 19:03:07 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-01-09 19:03:51 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-01-09 19:04:12 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-01-09 19:04:31 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
| 2024-01-09 19:04:36 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
| 2024-01-09 19:13:30 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2024-01-09 19:16:05 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 268 seconds) |
| 2024-01-09 19:17:07 +0100 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 255 seconds) |
| 2024-01-09 19:19:19 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 2024-01-09 19:19:31 +0100 | waldo | (~waldo@user/waldo) (Ping timeout: 256 seconds) |
| 2024-01-09 19:20:40 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 2024-01-09 19:21:32 +0100 | adanwan | (~adanwan@gateway/tor-sasl/adanwan) |
| 2024-01-09 19:24:02 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-01-09 19:25:35 +0100 | irrgit_ | (~irrgit@89.47.234.74) (Read error: Connection reset by peer) |
| 2024-01-09 19:27:39 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 19:33:44 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 19:36:40 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-01-09 19:37:11 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-01-09 19:38:28 +0100 | danza | (~danza@151.43.143.81) |
| 2024-01-09 19:42:52 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-01-09 19:43:19 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-01-09 19:44:35 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 2024-01-09 19:45:59 +0100 | AndreiDuma | (~textual@95.76.23.32) |
| 2024-01-09 19:46:18 +0100 | mechap | (~mechap@user/mechap) (Ping timeout: 260 seconds) |
| 2024-01-09 19:48:18 +0100 | mechap | (~mechap@user/mechap) |
| 2024-01-09 19:53:52 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2024-01-09 19:54:16 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 2024-01-09 19:54:16 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2024-01-09 19:54:35 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 2024-01-09 19:59:06 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Ping timeout: 250 seconds) |
| 2024-01-09 19:59:18 +0100 | puke | (~puke@user/puke) |
| 2024-01-09 19:59:22 +0100 | euleritian | (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-01-09 19:59:44 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 20:01:27 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 256 seconds) |
| 2024-01-09 20:08:52 +0100 | vglfr | (~vglfr@234.red-88-6-215.staticip.rima-tde.net) (Ping timeout: 255 seconds) |
| 2024-01-09 20:11:08 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 2024-01-09 20:12:29 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2024-01-09 20:15:33 +0100 | target_i | (~target_i@217.175.14.39) |
| 2024-01-09 20:16:19 +0100 | Batzy_ | (~quassel@user/batzy) (Ping timeout: 256 seconds) |
| 2024-01-09 20:21:47 +0100 | kwii | (~kwii@212.24.26.235) |
| 2024-01-09 20:25:10 +0100 | biberu | (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 2024-01-09 20:27:10 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
| 2024-01-09 20:28:21 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-01-09 20:29:51 +0100 | vglfr | (~vglfr@234.red-88-6-215.staticip.rima-tde.net) |
| 2024-01-09 20:32:40 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-01-09 20:33:08 +0100 | euleritian | (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) |
| 2024-01-09 20:39:39 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 2024-01-09 20:40:26 +0100 | sammburr | (~sammburr@host-92-16-247-196.as13285.net) |
| 2024-01-09 20:40:58 +0100 | sammburr | (~sammburr@host-92-16-247-196.as13285.net) () |
| 2024-01-09 20:41:02 +0100 | euleritian | (~euleritia@dynamic-089-015-237-163.89.15.237.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-01-09 20:41:19 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 20:44:52 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-01-09 20:45:41 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 20:49:06 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
| 2024-01-09 20:52:35 +0100 | waldo | (~waldo@user/waldo) (Ping timeout: 256 seconds) |
| 2024-01-09 20:54:35 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds) |
| 2024-01-09 20:56:37 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) |
| 2024-01-09 20:59:23 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-01-09 21:02:01 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 246 seconds) |
| 2024-01-09 21:05:39 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2024-01-09 21:07:51 +0100 | kwii | (~kwii@212.24.26.235) (Read error: Connection reset by peer) |
| 2024-01-09 21:07:59 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-01-09 21:08:14 +0100 | kwii | (~kwii@212.24.26.235) |
| 2024-01-09 21:08:23 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 21:14:56 +0100 | benjaminl | (~benjaminl@user/benjaminl) (Ping timeout: 245 seconds) |
| 2024-01-09 21:15:05 +0100 | benjaminl | (~benjaminl@user/benjaminl) |
| 2024-01-09 21:17:48 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2024-01-09 21:18:55 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2024-01-09 21:23:16 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2024-01-09 21:23:37 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2024-01-09 21:24:34 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2024-01-09 21:27:08 +0100 | kwii | (~kwii@212.24.26.235) (Ping timeout: 252 seconds) |
| 2024-01-09 21:27:48 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:d504:f200:d614:49c6) (Remote host closed the connection) |
| 2024-01-09 21:27:51 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 245 seconds) |
| 2024-01-09 21:29:44 +0100 | trev | (~trev@user/trev) (Quit: trev) |
| 2024-01-09 21:31:16 +0100 | danza | (~danza@151.43.143.81) (Ping timeout: 276 seconds) |
| 2024-01-09 21:33:40 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) |
| 2024-01-09 21:33:46 +0100 | <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 |
| 2024-01-09 21:34:32 +0100 | <EvanR> | yep I did have to force reload the page |
| 2024-01-09 21:34:47 +0100 | <EvanR> | I think that's the first time I force reloaded a page in like 9 years |
| 2024-01-09 21:35:18 +0100 | <EvanR> | caching is still hard! |
| 2024-01-09 21:35:19 +0100 | <tomsmeding> | I sometimes force-reload MS Teams out of anger just to put more load on their servers when it broke again |
| 2024-01-09 21:36:00 +0100 | <EvanR> | sadly or fortunately we have no monad tutorials for 2024 yet |
| 2024-01-09 21:36:20 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 21:36:32 +0100 | <tomsmeding> | this is your chance! |
| 2024-01-09 21:36:58 +0100 | <tomsmeding> | I sent this to a friend and they went like, "search for 'monad tutorial' on youtube and multiply these numbers by like 5" |
| 2024-01-09 21:37:09 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-01-09 21:38:26 +0100 | <EvanR> | there are too many monad tutorials. Clearly the only solution is another one which explains it once and for all |
| 2024-01-09 21:39:06 +0100 | waldo | (~waldo@user/waldo) (Ping timeout: 245 seconds) |
| 2024-01-09 21:39:11 +0100 | AndreiDuma | (~textual@95.76.23.32) (Quit: Textual IRC Client: www.textualapp.com) |
| 2024-01-09 21:39:34 +0100 | AndreiDuma | (~textual@95.76.23.32) |
| 2024-01-09 21:41:57 +0100 | <haskellbridge> | 15<Jade> https://xkcd.com/927/ | sed 's/standard/monad tutorial/g' |
| 2024-01-09 21:43:59 +0100 | <tomsmeding> | my immediate thought too |
| 2024-01-09 21:44:26 +0100 | <tomsmeding> | the alt-text is funny because it's usb-c now |
| 2024-01-09 21:45:41 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) (Remote host closed the connection) |
| 2024-01-09 21:46:09 +0100 | machinedgod | (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 2024-01-09 21:46:47 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 2024-01-09 21:46:47 +0100 | <EvanR> | usb is an infinitely nested shrinking sequence of plugs |
| 2024-01-09 21:47:11 +0100 | <EvanR> | but it's uncomputable so we're getting through the sequence quite slow |
| 2024-01-09 21:50:43 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 21:59:52 +0100 | barak | (~barak@2a0d:6fc2:68c1:2600:4270:3360:ac54:f834) (Ping timeout: 276 seconds) |
| 2024-01-09 22:01:35 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a926:b546:474f:4cf4) |
| 2024-01-09 22:04:33 +0100 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-01-09 22:06:35 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a926:b546:474f:4cf4) (Ping timeout: 268 seconds) |
| 2024-01-09 22:07:54 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-01-09 22:10:11 +0100 | mikess | (~mikess@user/mikess) (Ping timeout: 264 seconds) |
| 2024-01-09 22:12:14 +0100 | ricardo1 | (~ricardo@84.16.179.218) (Read error: Connection reset by peer) |
| 2024-01-09 22:14:41 +0100 | alexherbo2 | (~alexherbo@2a01cb0084fc5100fdd31218d0ca8c0c.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2024-01-09 22:15:31 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-01-09 22:18:26 +0100 | hexology | (~hexology@user/hexology) |
| 2024-01-09 22:20:57 +0100 | mikess | (~mikess@user/mikess) |
| 2024-01-09 22:23:15 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-01-09 22:25:34 +0100 | nschoe2 | (nschoe@gateway/vpn/protonvpn/nschoe) |
| 2024-01-09 22:25:52 +0100 | thegeekinside | (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 2024-01-09 22:26:50 +0100 | nschoe | (nschoe@gateway/vpn/protonvpn/nschoe) (Ping timeout: 260 seconds) |
| 2024-01-09 22:37:33 +0100 | waldo | (~waldo@user/waldo) (Ping timeout: 252 seconds) |
| 2024-01-09 22:43:56 +0100 | tomsmeding | (~tomsmedin@2a01:4f8:c0c:5e5e::2) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-01-09 22:44:29 +0100 | tomsmeding | (~tomsmedin@2a01:4f8:c0c:5e5e::2) |
| 2024-01-09 22:47:17 +0100 | waldo | (~waldo@user/waldo) |
| 2024-01-09 22:47:22 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 2024-01-09 22:47:42 +0100 | hgolden | (~hgolden@2603-8000-9d00-3ed1-a6e3-3ba3-0107-8cff.res6.spectrum.com) |
| 2024-01-09 22:48:20 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) |
| 2024-01-09 22:50:41 +0100 | ircbrowse_tom | (~ircbrowse@2a01:4f8:1c1c:9319::1) |
| 2024-01-09 22:50:47 +0100 | Server | +Cnt |
| 2024-01-09 22:51:57 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:a926:b546:474f:4cf4) |
| 2024-01-09 23:08:18 +0100 | michalz_ | (~michalz@185.246.207.201) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-01-09 23:09:39 +0100 | AndreiDuma | (~textual@95.76.23.32) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-01-09 23:11:00 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 2024-01-09 23:15:15 +0100 | Bynbo7 | (~Axman6@user/axman6) (Remote host closed the connection) |
| 2024-01-09 23:16:06 +0100 | Axman6 | (~Axman6@user/axman6) (Remote host closed the connection) |
| 2024-01-09 23:17:13 +0100 | xdminsy | (~xdminsy@117.147.71.169) (Ping timeout: 276 seconds) |
| 2024-01-09 23:17:28 +0100 | xdminsy | (~xdminsy@117.147.71.199) |
| 2024-01-09 23:20:38 +0100 | Axman61 | (~Axman6@user/axman6) (Ping timeout: 244 seconds) |
| 2024-01-09 23:21:38 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 2024-01-09 23:22:24 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) |
| 2024-01-09 23:24:59 +0100 | Flow | (~none@gentoo/developer/flow) (Ping timeout: 260 seconds) |
| 2024-01-09 23:27:41 +0100 | target_i | (~target_i@217.175.14.39) (Quit: leaving) |
| 2024-01-09 23:28:08 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-01-09 23:29:28 +0100 | kwii | (~kwii@212.24.26.235) |
| 2024-01-09 23:35:29 +0100 | johnw | (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 2024-01-09 23:48:01 +0100 | myme | (~myme@2a01:799:d60:e400:40e3:f57:648e:522b) (Ping timeout: 255 seconds) |
| 2024-01-09 23:48:53 +0100 | myme | (~myme@2a01:799:d60:e400:a6b6:bec4:8c06:a0eb) |
| 2024-01-09 23:49:25 +0100 | <haskellbridge> | 05<irregularsphere> "monad tutorial"? i look at Monad in the docs and go "oh, okay" |
| 2024-01-09 23:52:29 +0100 | acidjnk | (~acidjnk@p200300d6e72b930818892410b5265f00.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |