2025/04/28

Newest at the top

2025-04-28 11:03:02 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 11:02:42 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-04-28 11:02:41 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 248 seconds)
2025-04-28 11:01:56 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-28 11:01:29 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2025-04-28 11:00:01 +0200prdak(~Thunderbi@user/prdak) (Ping timeout: 248 seconds)
2025-04-28 10:54:05 +0200xff0x(~xff0x@2409:251:9040:2c00:c640:4db6:d630:f639)
2025-04-28 10:50:23 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 10:47:28 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2025-04-28 10:44:47 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 10:44:31 +0200comerijn(~merijn@77.242.116.146) merijn
2025-04-28 10:43:14 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
2025-04-28 10:39:26 +0200pabs3(~pabs3@user/pabs3) pabs3
2025-04-28 10:29:58 +0200lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-04-28 10:16:13 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-28 10:06:46 +0200gmg(~user@user/gehmehgeh) gehmehgeh
2025-04-28 09:59:30 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 09:59:15 +0200Googulator47(~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 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-04-28 09:53:35 +0200merijn(~merijn@77.242.116.146) merijn
2025-04-28 09:52:53 +0200prdak(~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 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-04-28 09:45:33 +0200xelxebar(~xelxebar@wilsonb.com) xelxebar
2025-04-28 09:44:36 +0200emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2025-04-28 09:43:58 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 09:43:41 +0200Googulator47(~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 +0200xelxebar(~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 +0200emmanuelux_(~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 +0200prdak(~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 +0200prdak(~Thunderbi@user/prdak) (Quit: prdak)
2025-04-28 09:33:05 +0200img(~img@user/img) img
2025-04-28 09:32:53 +0200akegalj(~akegalj@144-188.dsl.iskon.hr)
2025-04-28 09:31:45 +0200img(~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
2025-04-28 09:28:55 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 09:23:12 +0200akegalj(~akegalj@83-131-242-128.adsl.net.t-com.hr) (Ping timeout: 252 seconds)
2025-04-28 09:23:05 +0200Lord_of_Life_Lord_of_Life
2025-04-28 09:22:43 +0200harveypwca(~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving)
2025-04-28 09:22:34 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds)
2025-04-28 09:22:08 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)