Newest at the top
| 2024-12-24 03:50:08 +0100 | <haskellbridge> | <thirdofmay18081814goya> the right statement is, if we interpret "Gamma |- A" holds and we interpret it as: "the sequence-dependent/ordered FRP-circuit "Gamma" propagates to "A"/produces a value of type "A"", then we can infer "[] Gamma |- A", that is, the sequence-independent/unordered total output of "Gamma" is enough to know that "A" will be propagated to/produced |
| 2024-12-24 03:46:02 +0100 | <haskellbridge> | <thirdofmay18081814goya> it was slightly wrongly formulated |
| 2024-12-24 03:45:40 +0100 | <ski> | thirdofmay18081814goya : hm, not sure i follow that FRP interpretation |
| 2024-12-24 03:40:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:36:08 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Ping timeout: 252 seconds) |
| 2024-12-24 03:34:44 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-12-24 03:33:03 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 03:31:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:22:35 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 260 seconds) |
| 2024-12-24 03:20:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-24 03:19:17 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 03:18:21 +0100 | rekahsoft | (~rekahsoft@76.69.85.220) rekahsoft |
| 2024-12-24 03:17:40 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 03:17:20 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2024-12-24 03:16:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:13:36 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2024-12-24 03:12:46 +0100 | nadja | (~dequbed@banana-new.kilobyte22.de) dequbed |
| 2024-12-24 03:12:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2024-12-24 03:11:59 +0100 | nadja | (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 265 seconds) |
| 2024-12-24 03:10:04 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection) |
| 2024-12-24 03:06:03 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-12-24 03:05:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:01:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:00:01 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 02:52:50 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 260 seconds) |
| 2024-12-24 02:49:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 02:45:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:43:09 +0100 | califax | (~califax@user/califx) califx |
| 2024-12-24 02:40:53 +0100 | <loonycyborg> | Basically I want to make a typesafe variant of system environment, and other structures that are inspired by it in some buildsystems :P |
| 2024-12-24 02:40:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> do note that the string-indexing of a type here is not doing any "work" so to say |
| 2024-12-24 02:39:53 +0100 | ft | (~ft@i59F4F055.versanet.de) ft |
| 2024-12-24 02:38:09 +0100 | ft | (~ft@i59F4F0F5.versanet.de) (Ping timeout: 265 seconds) |
| 2024-12-24 02:38:01 +0100 | <loonycyborg> | then total size would be known and indices could be assigned |
| 2024-12-24 02:37:44 +0100 | <loonycyborg> | ye list size would be most definitely finite, app and modules will have to define variables they want to see as string->value mappings and they will have to be merged into single mapping |
| 2024-12-24 02:35:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> * subtype of "TypeFrom String" that you're looking for |
| 2024-12-24 02:35:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 02:33:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> quite literally: you will not be able to do a thing with the "TypeFrom String" that you can't do with the finite type counting the number of modules/apps |
| 2024-12-24 02:32:21 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e. the finite type whose size is the number of modules/apps will be equivalent to the type you seek |
| 2024-12-24 02:32:16 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-12-24 02:31:37 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-24 02:31:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> loonycyborg: that type is actually equivalent to the finite type counting the number of modules/app |
| 2024-12-24 02:31:31 +0100 | <EvanR> | it's not like shovelware apps that get kicked off the app store if the dev doesn't change *something* every month |
| 2024-12-24 02:31:15 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 2024-12-24 02:30:53 +0100 | <EvanR> | loonycyborg, a lot of those libraries do exactly what they intended and have no need to keep updating |
| 2024-12-24 02:30:51 +0100 | <loonycyborg> | but actual values could be got from command line and other places |
| 2024-12-24 02:30:34 +0100 | <loonycyborg> | each string has own type specified by app or module |
| 2024-12-24 02:30:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:30:14 +0100 | <haskellbridge> | <thirdofmay18081814goya> loonycyborg: and what is the target type? |
| 2024-12-24 02:29:50 +0100 | <Leary> | loonycyborg: There are also packages on hackage for vector/array backed extensible records. As for version numbers, being <1 doesn't mean anything. |
| 2024-12-24 02:29:36 +0100 | <loonycyborg> | strings are determined by app or modules so it's pretty specific |