Newest at the top
| 2025-04-28 10:29:58 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-28 10:16:13 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-28 10:06:46 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-28 09:59:30 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 09:59:15 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 09:54:24 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/ZXmHzkdBFkCbuBgjCCIfldSk/hI24ncMuDu0 (3 lines) |
| 2025-04-28 09:54:24 +0200 | <haskellbridge> | <hellwolf> amazing. |
| 2025-04-28 09:53:35 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-28 09:53:35 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-04-28 09:52:53 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 252 seconds) |
| 2025-04-28 09:46:45 +0200 | <Leary> | Cute fact about that `dfoldr`: just like with regular `foldr` on lists, you can rearrange it to get the church encoding `Vec n a` ~ `forall f. (forall m. a -> f m -> f (S m)) -> f Z -> f n`. Rare to see these for GADTs. |
| 2025-04-28 09:46:19 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-04-28 09:45:33 +0200 | xelxebar | (~xelxebar@wilsonb.com) xelxebar |
| 2025-04-28 09:44:36 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 2025-04-28 09:43:58 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 09:43:41 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 09:39:50 +0200 | <haskellbridge> | <hellwolf> something like that, depending the use case |
| 2025-04-28 09:39:34 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/nUqJifIEojXapRsqcNyBxQyG/SZSeSOaoePA (3 lines) |
| 2025-04-28 09:39:32 +0200 | <haskellbridge> | <hellwolf> though, I could think " filter" differently, it is a fold that adding a boolean to the original vector |
| 2025-04-28 09:37:53 +0200 | xelxebar | (~xelxebar@wilsonb.com) (Ping timeout: 248 seconds) |
| 2025-04-28 09:37:32 +0200 | <haskellbridge> | <hellwolf> but I can see the problem of filtering. |
| 2025-04-28 09:37:12 +0200 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2025-04-28 09:36:47 +0200 | <haskellbridge> | beautiful interface :p |
| 2025-04-28 09:36:47 +0200 | <haskellbridge> | <hellwolf> > dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n |
| 2025-04-28 09:35:12 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 09:34:57 +0200 | <haskellbridge> | I am checking this... which one is painful? I am asking unironically. |
| 2025-04-28 09:34:57 +0200 | <haskellbridge> | <hellwolf> https://hackage.haskell.org/package/vec-0.5.1/docs/Data-Vec-Lazy.html#g:5 |
| 2025-04-28 09:34:53 +0200 | prdak | (~Thunderbi@user/prdak) (Quit: prdak) |
| 2025-04-28 09:33:05 +0200 | img | (~img@user/img) img |
| 2025-04-28 09:32:53 +0200 | akegalj | (~akegalj@144-188.dsl.iskon.hr) |
| 2025-04-28 09:31:45 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-04-28 09:28:55 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-04-28 09:23:12 +0200 | akegalj | (~akegalj@83-131-242-128.adsl.net.t-com.hr) (Ping timeout: 252 seconds) |
| 2025-04-28 09:23:05 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-04-28 09:22:43 +0200 | harveypwca | (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving) |
| 2025-04-28 09:22:34 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 2025-04-28 09:22:08 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 09:21:51 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 09:21:42 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-04-28 09:19:10 +0200 | <c_wraith> | length-indexed vectors are very easy to understand, but actually quite awkward to use. Like... filter can have a ton of different types, and it turns out all of them are a pain to work with. |
| 2025-04-28 09:17:29 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 245 seconds) |
| 2025-04-28 09:11:51 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) |
| 2025-04-28 09:09:07 +0200 | <haskellbridge> | <hellwolf> Also, I think length-indexed vector is the most practical everyday stuff DT should sell hard. Like selling ADT and pattern matching to mainstream languages. |
| 2025-04-28 09:07:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 09:07:34 +0200 | <haskellbridge> | <hellwolf> But rust also shows that some technique of better managing runtime system behaviour can be appreciated. Do you consider DT and LinearTypes are orthogonal to each other as researches? |
| 2025-04-28 09:07:33 +0200 | <haskellbridge> | <geekosaur> oh, they weren't, you were just catching up while the bot was down (system upgrade) |
| 2025-04-28 09:07:29 +0200 | akegalj | (~akegalj@83-131-242-128.adsl.net.t-com.hr) akegalj |
| 2025-04-28 09:05:40 +0200 | <haskellbridge> | <hellwolf> Heh, yea, selling DT is hard because people are lazy and handwave the proofs a way by doing it on paper or simply yolo |
| 2025-04-28 09:04:21 +0200 | geekosaur | wonders how long those were queued |
| 2025-04-28 09:04:18 +0200 | <haskellbridge> | <Bowuigi> "Everyone's bad at code" and "I like having a good mental health" are probably why we still have PL research lol |