Newest at the top
| 2024-10-13 05:24:08 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 05:22:03 +0200 | <Inst> | also, it implies that any function whose signature ends in an unconstrained type variable, is equivalent to trying to produce a value of type Void |
| 2024-10-13 05:21:14 +0200 | <Inst> | geekosaur: but a -> Void is defined, on the term level, exactly the same as a -> b |
| 2024-10-13 05:21:11 +0200 | Inst_ | Inst |
| 2024-10-13 05:21:08 +0200 | Inst | (~Inst@user/Inst) (Killed (NickServ (GHOST command used by Inst_))) |
| 2024-10-13 05:20:55 +0200 | Inst_ | (~Inst@user/Inst) Inst |
| 2024-10-13 05:15:30 +0200 | ephilalethes | (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 2024-10-13 05:14:45 +0200 | <geekosaur> | sorry, I mean the only value possible of type `b` |
| 2024-10-13 05:14:41 +0200 | <Lears> | All isomorphic. |
| 2024-10-13 05:14:38 +0200 | <Lears> | `forall a b. a -> b` ~ `forall a. a -> forall b. b` ~ `forall a. a -> Void` ~ `(exists a. a) -> Void` ~ `() -> Void` ~ `Void` |
| 2024-10-13 05:13:59 +0200 | <geekosaur> | in the same way that a -> a must be `id` |
| 2024-10-13 05:13:46 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-13 05:13:45 +0200 | <geekosaur> | it's not a -> Void, it's a -> b. the trick being that it must be `undefined` |
| 2024-10-13 05:12:27 +0200 | <Inst> | which gets me thinking to a -> b must be unfulfillable, as well as the possible inhabitants of [a] -> [a] |
| 2024-10-13 05:12:00 +0200 | <Inst> | "a -> a doesn't tell you anything", ummm, it tells you it's id |
| 2024-10-13 05:11:47 +0200 | <Inst> | i was reading Eric Normand complaining about the meaninglessness of type signatures |
| 2024-10-13 05:11:34 +0200 | <Inst> | "essentially the same", which is just as ambiguously useless as equivalent |
| 2024-10-13 05:11:02 +0200 | <probie> | Inst: can you define "equivalent"? It has the same number of inhabitants |
| 2024-10-13 05:10:00 +0200 | <Inst> | a function with a type, without any typeclass constraints, of a -> b is equivalent to a -> Void, right? |
| 2024-10-13 05:09:34 +0200 | Inst | (~Inst@user/Inst) Inst |
| 2024-10-13 05:07:14 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 05:01:23 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-13 04:56:10 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-13 04:51:25 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 04:50:18 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-10-13 04:40:21 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-10-13 04:35:38 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 04:34:29 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-10-13 04:29:28 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 04:23:41 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 255 seconds) |
| 2024-10-13 04:20:35 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Read error: Connection reset by peer) |
| 2024-10-13 04:20:35 +0200 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2024-10-13 04:18:24 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-13 04:14:05 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 04:11:12 +0200 | nadja | (~dequbed@banana-new.kilobyte22.de) dequbed |
| 2024-10-13 04:09:53 +0200 | nadja | (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 248 seconds) |
| 2024-10-13 04:09:08 +0200 | td_ | (~td@i5387090D.versanet.de) |
| 2024-10-13 04:09:08 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-13 04:07:29 +0200 | td_ | (~td@i5387092F.versanet.de) (Ping timeout: 255 seconds) |
| 2024-10-13 04:05:32 +0200 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2024-10-13 04:05:03 +0200 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2024-10-13 04:04:23 +0200 | ephilalethes | (~noumenon@113.51-175-156.customer.lyse.net) noumenon |
| 2024-10-13 04:02:16 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-13 03:57:19 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 03:46:20 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-10-13 03:44:28 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-10-13 03:41:32 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 03:30:06 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-13 03:29:35 +0200 | jinsun | (~jinsun@user/jinsun) () |
| 2024-10-13 03:27:43 +0200 | alp_ | (~alp@2001:861:e3d6:8f80:8cd6:c1b4:e0be:1fe8) (Ping timeout: 264 seconds) |