Newest at the top
| 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 +0100 | merijn | (~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 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-30 21:08:26 +0100 | michalz_ | (~michalz@185.246.207.222) (Remote host closed the connection) |
| 2024-12-30 21:07:39 +0100 | JuanDaugherty | (~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 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2024-12-30 21:00:00 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-12-30 20:58:17 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-30 20:54:09 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2024-12-30 20:49:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-30 20:48:26 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) |
| 2024-12-30 20:43:31 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-30 20:42:47 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) |
| 2024-12-30 20:40:10 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-30 20:38:46 +0100 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) |
| 2024-12-30 20:37:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-30 20:37:48 +0100 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) (Quit: β reduced) |
| 2024-12-30 20:35:26 +0100 | smtt | (smt@user/smtt) smtt |
| 2024-12-30 20:34:57 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) |
| 2024-12-30 20:34:10 +0100 | mreh | (~matthew@host86-146-25-121.range86-146.btcentralplus.com) (Quit: Lost terminal) |
| 2024-12-30 20:33:59 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-30 20:33:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-30 20:32:26 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) |
| 2024-12-30 20:30:48 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2024-12-30 20:26:01 +0100 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) |
| 2024-12-30 20:25:16 +0100 | CrunchyFlakes | (~CrunchyFl@77.20.155.95) (Ping timeout: 252 seconds) |
| 2024-12-30 20:25:06 +0100 | rachelambda8 | (~rachelamb@cust-95-80-25-71.csbnet.se) (Quit: β reduced) |
| 2024-12-30 20:24:54 +0100 | CrunchyFlakes_ | (~CrunchyFl@ip4d14127c.dynamic.kabel-deutschland.de) |
| 2024-12-30 20:21:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-30 20:18:40 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2024-12-30 20:16:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-30 20:14:47 +0100 | CrunchyFlakes_ | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2024-12-30 20:13:47 +0100 | CrunchyFlakes | (~CrunchyFl@77.20.155.95) |
| 2024-12-30 20:13:40 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2024-12-30 20:09:54 +0100 | euleritian | (~euleritia@dynamic-176-001-202-129.176.1.pool.telefonica.de) |
| 2024-12-30 20:04:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |