Newest at the top
| 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" |
| 2024-12-29 04:18:13 +0100 | <Leary> | I don't see what an ordering on the index kind has to do with anything. |
| 2024-12-29 04:17:05 +0100 | <haskellbridge> | <Bowuigi> Wait how? |
| 2024-12-29 04:16:00 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2024-12-29 04:14:23 +0100 | <haskellbridge> | <thirdofmay18081814goya> pattern matching, that is |
| 2024-12-29 04:13:37 +0100 | <haskellbridge> | <thirdofmay18081814goya> simply because the work of an indexing type is delimited simply by how many ways you can pattern match on it. i.e. this completely specifies the extent of the work an indexing type can do |