Newest at the top
| 2024-12-29 06:37:58 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 06:24:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-29 06:23:26 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) Raito_Bezarius |
| 2024-12-29 06:18:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 06:08:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-29 06:06:46 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Max SendQ exceeded) |
| 2024-12-29 06:05:04 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) Raito_Bezarius |
| 2024-12-29 06:04:16 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Ping timeout: 265 seconds) |
| 2024-12-29 06:03:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 05:51:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-29 05:51:01 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 248 seconds) |
| 2024-12-29 05:47:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 05:35:51 +0100 | <haskellbridge> | <Bowuigi> Dedekind/Cauchy reals don't seem to require infinite alphabets |
| 2024-12-29 05:33:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 05:32:09 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: this is probably taken care of if the alphabet is assumed to be countable. cannot have uncountably-many terms arising from countable alphabet |
| 2024-12-29 05:30:48 +0100 | <haskellbridge> | <Bowuigi> Tho Nat may not be enough, unsure if larger infinities can be represented without dependent types |
| 2024-12-29 05:29:24 +0100 | <haskellbridge> | <Bowuigi> That makes sense I guess |
| 2024-12-29 05:29:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 05:17:56 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 05:14:26 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) euandreh |
| 2024-12-29 05:13:23 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 05:08:41 +0100 | euandreh | (~Thunderbi@2804:d59:8929:cc00:c70d:53a7:f44e:6c64) (Ping timeout: 265 seconds) |
| 2024-12-29 05:01:22 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 04:59:16 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 04:56:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:51:31 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 04:51:06 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 04:48:13 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 04:47:46 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 04:46:49 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-12-29 04:46:08 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) |
| 2024-12-29 04:46:01 +0100 | <haskellbridge> | <thirdofmay18081814goya> so that means the only "value" or only "worth" of "IndexType" is how many ways it can be different, i.e., its cardinality |
| 2024-12-29 04:43:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-29 04:41:38 +0100 | Typedfern | (~Typedfern@106.red-83-37-34.dynamicip.rima-tde.net) typedfern |
| 2024-12-29 04:39:04 +0100 | typedfern_ | (~Typedfern@106.red-83-37-34.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2024-12-29 04:39:04 +0100 | Typedfern | (~Typedfern@106.red-83-37-34.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2024-12-29 04:39:01 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-29 04:38:09 +0100 | <haskellbridge> | <thirdofmay18081814goya> because of non-dependent types |
| 2024-12-29 04:37:52 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e. we use the fact that "choiceFunction :: IndexType -> Type" applied to "index :: IndexType" will produce a term "resultingTerm :: Type" which has no subterms like "someSubterm :: IndexType" |
| 2024-12-29 04:36:43 +0100 | td_ | (~td@i5387092B.versanet.de) td_ |
| 2024-12-29 04:36:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:35:22 +0100 | <haskellbridge> | <thirdofmay18081814goya> not sure if the same argument could be used for dependent types. for non-dependent types I think it is enough |
| 2024-12-29 04:35:02 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-12-29 04:34:35 +0100 | td_ | (~td@i5387093F.versanet.de) (Ping timeout: 244 seconds) |
| 2024-12-29 04:31:21 +0100 | euleritian | (~euleritia@dynamic-176-006-135-074.176.6.pool.telefonica.de) (Ping timeout: 276 seconds) |
| 2024-12-29 04:30:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> these differences* |
| 2024-12-29 04:30:28 +0100 | <haskellbridge> | <thirdofmay18081814goya> so if you have "someTerm :: Type", it has at most finitely many differences with "anotherTerm :: Type", which means these can be indexed by a function on the naturals |
| 2024-12-29 04:29:25 +0100 | <haskellbridge> | <thirdofmay18081814goya> the argument also follows from considering that any term (e.g. in System F) has finitely many symbols and therefore can only have finitely many differences with any other term |
| 2024-12-29 04:28:58 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: well, there is nothing in "IndexType :: Type" that can be used to make a value of "Type". so it can only allow you to choose a value. i.e., the term that will result from applying "choiceFunction :: IndexType -> Type" will not contain any term from "IndexType" |
| 2024-12-29 04:25:11 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |