Newest at the top
| 2024-12-24 02:25:52 +0100 | <geekosaur> | you'll need to think through what exactly you're doing to make that decision |
| 2024-12-24 02:25:36 +0100 | <geekosaur> | can you do something like reflecting a type level list into a runtime Vector? |
| 2024-12-24 02:25:34 +0100 | <EvanR> | or reasoning metapattern |
| 2024-12-24 02:24:59 +0100 | <EvanR> | any reasoning pattern you use must be reflected in the type system |
| 2024-12-24 02:24:34 +0100 | <EvanR> | and (before all that) verify what you plan to do at runtime makes any damn sense, which is where it gets complicated |
| 2024-12-24 02:23:24 +0100 | __monty__ | (~toonn@user/toonn) (Quit: Lost terminal) |
| 2024-12-24 02:21:51 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-12-24 02:19:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-24 02:19:01 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2024-12-24 02:18:24 +0100 | <loonycyborg> | ye I want to build mapping at compile time but make runtime structures based on it |
| 2024-12-24 02:16:37 +0100 | <EvanR> | or so I thought |
| 2024-12-24 02:16:26 +0100 | <EvanR> | it's not at runtime |
| 2024-12-24 02:16:09 +0100 | <loonycyborg> | at least at runtime |
| 2024-12-24 02:15:57 +0100 | <loonycyborg> | ye but avoiding traversal of whole list would be nice |
| 2024-12-24 02:15:55 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2024-12-24 02:14:57 +0100 | <EvanR> | if you literally don't care about order, then a list still works |
| 2024-12-24 02:14:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:14:21 +0100 | <EvanR> | but a list is probably the most realistic |
| 2024-12-24 02:14:07 +0100 | <EvanR> | if you're feeling nuts you might have success implementing a binary tree in the type system which serves the same purpose |
| 2024-12-24 02:14:03 +0100 | <loonycyborg> | at *compile time |
| 2024-12-24 02:13:56 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f25e9e9d221c37061e3.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2024-12-24 02:13:53 +0100 | son0p | (~ff@186.121.100.67) son0p |
| 2024-12-24 02:13:53 +0100 | <loonycyborg> | I was thinking to use array at runtime and calculate indices for it at runtime |
| 2024-12-24 02:13:30 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2024-12-24 02:13:20 +0100 | <EvanR> | similar to KnownNat |
| 2024-12-24 02:13:19 +0100 | <geekosaur> | also Haskell's type system isn't really up to things like hashmaps; the best it can do is linked lists |
| 2024-12-24 02:13:13 +0100 | <EvanR> | KnownSymbol lets you have the corresponding String at runtime |
| 2024-12-24 02:12:11 +0100 | poscat | (~poscat@user/poscat) poscat |
| 2024-12-24 02:11:58 +0100 | <geekosaur> | ("dependent types" = types that depend on runtime values, not just the other way around) |
| 2024-12-24 02:11:27 +0100 | <geekosaur> | you really want Idris or Agda; Haskell doesn't have a real dependent types story as yet |
| 2024-12-24 02:11:03 +0100 | <geekosaur> | KnownSymbol and singletons (blech) |
| 2024-12-24 02:10:37 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f41b013a429fe4b7686.dip0.t-ipconnect.de) |
| 2024-12-24 02:08:51 +0100 | poscat0x04 | (~poscat@user/poscat) (Quit: Bye) |
| 2024-12-24 02:08:11 +0100 | <loonycyborg> | this really reminds me of C++ template magic though |
| 2024-12-24 02:08:11 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 02:08:09 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-24 02:07:55 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Read error: Connection reset by peer) |
| 2024-12-24 02:07:45 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 2024-12-24 02:06:24 +0100 | <loonycyborg> | or how I can extract things back to runtime when needed |
| 2024-12-24 02:06:09 +0100 | <loonycyborg> | Seems I can use string literals at compile time with -XDataKinds and -XTypeFamilies but not sure if it's best way currently |
| 2024-12-24 02:03:23 +0100 | <loonycyborg> | I was thinking more of " I don't care about order so I can do hashmap" but not sure how it applies to compile-time |
| 2024-12-24 02:03:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 02:00:50 +0100 | <EvanR> | the first ones easier |
| 2024-12-24 02:00:42 +0100 | Feuermagier_ | Feuermagier |
| 2024-12-24 02:00:42 +0100 | Guest7514 | (~Feuermagi@user/feuermagier) (Killed (zirconium.libera.chat (Nickname regained by services))) |
| 2024-12-24 02:00:42 +0100 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 02:00:42 +0100 | Feuermagier | Guest7514 |
| 2024-12-24 02:00:31 +0100 | <EvanR> | there's "I don't care about order" and "we need the types to enforce nobody not even god can care about order" |
| 2024-12-24 01:59:24 +0100 | <EvanR> | yes the string itself is a type of kind Symbol |
| 2024-12-24 01:57:12 +0100 | Feuermagier_ | Feuermagier |