Newest at the top
| 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) |
| 2024-12-29 04:22:24 +0100 | <haskellbridge> | <Bowuigi> I still don't understand how does that limit you to Nat/Fin |
| 2024-12-29 04:21:19 +0100 | dsrt^ | (dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-29 04:21:17 +0100 | <haskellbridge> | <thirdofmay18081814goya> Leary: not sure either, just threw that out there to make the problem more concrete |
| 2024-12-29 04:20:33 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-29 04:20:32 +0100 | <haskellbridge> | <thirdofmay18081814goya> "choiceFunction :: IndexType -> Type", where "IndexType :: Type" |
| 2024-12-29 04:20:08 +0100 | <haskellbridge> | <thirdofmay18081814goya> that's not the type it has, the choice function in which it serves as the indexing type has that type |
| 2024-12-29 04:19:18 +0100 | <haskellbridge> | <thirdofmay18081814goya> wait |
| 2024-12-29 04:19:15 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh |
| 2024-12-29 04:18:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: the extent of the work that can be done by an indexing type is that of specifying another type, so it has type "IndexType -> Type", where "IndexType : Type" |