Newest at the top
| 2025-01-17 23:59:00 +0100 | <EvanR> | constructible or countable? |
| 2025-01-17 23:58:40 +0100 | <haskellbridge> | <thirdofmay18081814goya> a countable universe |
| 2025-01-17 23:58:27 +0100 | <haskellbridge> | <thirdofmay18081814goya> EvanR: oh ok well, the statement is that terms/values of a polymorphic function type are indexable by the indexability of a constructible universe |
| 2025-01-17 23:58:24 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-01-17 23:57:03 +0100 | <c_wraith> | Also, there are only countably many Haskell values for practical reasons like programs being countable and the total amount of input a program can receive being countable. |
| 2025-01-17 23:56:20 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-01-17 23:54:24 +0100 | <EvanR> | when you said "this one" there was nothing posted before you then said "this is not necessarily the case" maybe the bridge lost it |
| 2025-01-17 23:54:14 +0100 | <c_wraith> | It's secretly useful! |
| 2025-01-17 23:54:09 +0100 | <c_wraith> | have fun with that one. |
| 2025-01-17 23:54:03 +0100 | <c_wraith> | newtype Hyper a b = H (Hyper b a -> b) |
| 2025-01-17 23:53:43 +0100 | <EvanR> | how do you traverse a function value with or without finite time |
| 2025-01-17 23:53:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> this is not necessarily the case for e.g. values of coinductive types |
| 2025-01-17 23:53:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-17 23:53:28 +0100 | tnt2 | tnt1 |
| 2025-01-17 23:53:28 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 272 seconds) |
| 2025-01-17 23:53:28 +0100 | <EvanR> | "traversability of a value" is a bit weird |
| 2025-01-17 23:53:20 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-17 23:53:16 +0100 | <haskellbridge> | <thirdofmay18081814goya> this one |
| 2025-01-17 23:52:50 +0100 | <haskellbridge> | <thirdofmay18081814goya> so there might be infinitely possible values, but as long as any given value is traversable in finite time, it is a datatype |
| 2025-01-17 23:52:49 +0100 | <EvanR> | what statement |
| 2025-01-17 23:52:30 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm right but the statement specifically targets types whose terms are finitely traversable |
| 2025-01-17 23:51:50 +0100 | <EvanR> | infinite data might have non-countable possible values, for some value of possible |
| 2025-01-17 23:51:25 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-17 23:51:13 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2025-01-17 23:50:46 +0100 | <EvanR> | limiting yourself to finite data i haskell is a bit limiting goya |
| 2025-01-17 23:47:32 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-01-17 23:46:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 23:44:18 +0100 | symdrome | (~user@2804:1e78:2201:58b0::416) symdrome |
| 2025-01-17 23:35:46 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-01-17 23:35:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-17 23:31:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 23:27:53 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-17 23:25:24 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 260 seconds) |
| 2025-01-17 23:24:26 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-17 23:24:03 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-17 23:23:20 +0100 | michalz | (~michalz@185.246.207.215) (Remote host closed the connection) |
| 2025-01-17 23:20:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-17 23:18:16 +0100 | mixfix41 | (~tbmur@user/mixfix41) mixfix41 |
| 2025-01-17 23:18:03 +0100 | tnt2 | tnt1 |
| 2025-01-17 23:18:03 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-01-17 23:17:16 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-17 23:15:50 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 23:13:40 +0100 | tnt2 | tnt1 |
| 2025-01-17 23:13:40 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-01-17 23:13:21 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-17 23:07:03 +0100 | tnt2 | tnt1 |
| 2025-01-17 23:07:03 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-01-17 23:05:39 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-17 23:04:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-17 23:02:46 +0100 | ephilalethes | (~noumenon@182.0.203.121) (Quit: Leaving) |