2024/12/24

Newest at the top

2024-12-24 02:26:43 +0100 <loonycyborg> current idea is to make mapping of strings to types at compile time then make some kind of structure that can be looked up by that string to get value of appropriate type
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 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2024-12-24 02:19:35 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-12-24 02:19:01 +0100j1n37(~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 +0100j1n37(~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 +0100merijn(~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 +0100acidjnk_new(~acidjnk@p200300d6e7283f25e9e9d221c37061e3.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
2024-12-24 02:13:53 +0100son0p(~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 +0100ljdarj(~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 +0100poscat(~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 +0100acidjnk_new3(~acidjnk@p200300d6e7283f41b013a429fe4b7686.dip0.t-ipconnect.de)
2024-12-24 02:08:51 +0100poscat0x04(~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 +0100Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2024-12-24 02:08:09 +0100tnt1(~Thunderbi@user/tnt1) tnt1
2024-12-24 02:07:55 +0100Feuermagier(~Feuermagi@user/feuermagier) (Read error: Connection reset by peer)
2024-12-24 02:07:45 +0100tnt1(~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 +0100merijn(~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 +0100Feuermagier_Feuermagier
2024-12-24 02:00:42 +0100Guest7514(~Feuermagi@user/feuermagier) (Killed (zirconium.libera.chat (Nickname regained by services)))
2024-12-24 02:00:42 +0100Feuermagier_(~Feuermagi@user/feuermagier) Feuermagier
2024-12-24 02:00:42 +0100FeuermagierGuest7514
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