2024/12/30

Newest at the top

2024-12-30 21:36:41 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh
2024-12-30 21:36:27 +0100califax(~califax@user/califx) califx
2024-12-30 21:35:36 +0100califax(~califax@user/califx) (Ping timeout: 264 seconds)
2024-12-30 21:34:59 +0100prasad(~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net) (Ping timeout: 245 seconds)
2024-12-30 21:34:51 +0100AlexNoo_AlexNoo
2024-12-30 21:34:37 +0100kayvank(~user@52-119-115-185.PUBLIC.monkeybrains.net) (Remote host closed the connection)
2024-12-30 21:33:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-30 21:32:24 +0100gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-12-30 21:31:05 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2024-12-30 21:26:38 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-30 21:23:58 +0100 <int-e> Eh, I don't know. I'm probably wrong. It is interesting that this doesn't tie into Data.Typeable out of the box.
2024-12-30 21:23:37 +0100son0p(~ff@2800:e6:4001:6cc3:2e2c:4b4e:bc2a:6f17) son0p
2024-12-30 21:23:34 +0100kayvank(~user@52-119-115-185.PUBLIC.monkeybrains.net) kayvank
2024-12-30 21:19:17 +0100 <int-e> I guess `TestEquality` is meant for things that are compile time decidable
2024-12-30 21:18:30 +0100 <int-e> Yeah I didn't read enough context. `f` is the argument of the TestEquality class.
2024-12-30 21:17:58 +0100 <carbolymer> for some reason
2024-12-30 21:17:55 +0100 <int-e> ah
2024-12-30 21:17:50 +0100 <carbolymer> int-e: but there's no `TestEquality Proxy`
2024-12-30 21:16:21 +0100 <carbolymer> I'm tired
2024-12-30 21:16:18 +0100 <carbolymer> shit I
2024-12-30 21:16:16 +0100 <carbolymer> Data.Typeable I mean
2024-12-30 21:16:05 +0100 <carbolymer> thanks!
2024-12-30 21:15:57 +0100 <carbolymer> omg, I've read Data.Equality three times and I didn't notice eqT
2024-12-30 21:14:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2024-12-30 21:13:11 +0100 <int-e> testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
2024-12-30 21:13:03 +0100 <int-e> (taking f = Proxy)
2024-12-30 21:12:53 +0100 <int-e> huh isn't that exactly what testEquality is?
2024-12-30 21:10:47 +0100 <int-e> With Data.Typeable you can write f :: (Typeable a, Typeable b) => p a -> p b -> Maybe (a :~: b); f _ _ = eqT
2024-12-30 21:09:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-30 21:08:26 +0100michalz_(~michalz@185.246.207.222) (Remote host closed the connection)
2024-12-30 21:07:39 +0100JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2024-12-30 21:06:35 +0100 <carbolymer> how do I write a function `Proxy a -> Proxy b -> Maybe (a :~: b)` ? Basically, an instance `TestEquality Proxy`
2024-12-30 21:00:37 +0100caconym(~caconym@user/caconym) caconym
2024-12-30 21:00:00 +0100caconym(~caconym@user/caconym) (Quit: bye)
2024-12-30 20:58:17 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-30 20:54:09 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2024-12-30 20:49:39 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-30 20:48:26 +0100euleritian(~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de)
2024-12-30 20:43:31 +0100euleritian(~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-12-30 20:42:47 +0100euleritian(~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de)
2024-12-30 20:40:10 +0100euleritian(~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-12-30 20:38:46 +0100rachelambda8(~rachelamb@cust-95-80-25-71.csbnet.se)
2024-12-30 20:37:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-12-30 20:37:48 +0100rachelambda8(~rachelamb@cust-95-80-25-71.csbnet.se) (Quit: β reduced)
2024-12-30 20:35:26 +0100smtt(smt@user/smtt) smtt
2024-12-30 20:34:57 +0100euleritian(~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de)
2024-12-30 20:34:10 +0100mreh(~matthew@host86-146-25-121.range86-146.btcentralplus.com) (Quit: Lost terminal)
2024-12-30 20:33:59 +0100euleritian(~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-12-30 20:33:19 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-30 20:32:26 +0100euleritian(~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de)