| 2024-12-24 00:05:25 +0100 | son0p | (~ff@186.121.98.118) (Ping timeout: 252 seconds) |
| 2024-12-24 00:05:55 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-12-24 00:05:56 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-12-24 00:06:01 +0100 | califax | (~califax@user/califx) (Read error: Connection reset by peer) |
| 2024-12-24 00:06:11 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2024-12-24 00:06:18 +0100 | califax | (~califax@user/califx) califx |
| 2024-12-24 00:06:25 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2024-12-24 00:06:37 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 00:09:20 +0100 | esph | (~weechat@user/esph) (Ping timeout: 252 seconds) |
| 2024-12-24 00:10:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 00:11:40 +0100 | <hellwolf> | ski, show instance is actually "correct", I am sticking a weird domain where U256 means 256 bits. |
| 2024-12-24 00:11:40 +0100 | <hellwolf> | and thanks for your hint using case of, the TH code is actually quite easy, I have it done: https://play.haskell.org/saved/Hdf3hnIp |
| 2024-12-24 00:12:41 +0100 | <hellwolf> | still feel herculean, but now that I wrote couple of big TH code, it feels rather mechanical |
| 2024-12-24 00:22:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 00:28:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 00:29:38 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-24 00:39:02 +0100 | gorignak | (~gorignak@user/gorignak) (Ping timeout: 252 seconds) |
| 2024-12-24 00:39:39 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-12-24 00:40:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 00:43:07 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-12-24 00:45:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 00:46:15 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 2024-12-24 00:50:24 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 00:50:49 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 244 seconds) |
| 2024-12-24 00:55:17 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:00:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 01:01:03 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-12-24 01:03:06 +0100 | Lears | Leary |
| 2024-12-24 01:03:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> ski: these comments have suddenly made sense to me, thank you very much again! |
| 2024-12-24 01:03:17 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-24 01:04:21 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-12-24 01:05:59 +0100 | <haskellbridge> | <thirdofmay18081814goya> it suddenly made sense because as I was thinking about FRP, I realized, under the interpretation you give "[] Gamma |- A -> [] Gamma |- [] A" encodes that "[] Gamma" is sequence-independent in allowing the circuit to propagate to the next term, "A" |
| 2024-12-24 01:07:36 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e., that implication provides the semantics for: "it doesn't matter the order in which you evaluate/propagate through this part of the secret, it will yield "A" anyways |
| 2024-12-24 01:07:45 +0100 | <haskellbridge> | <thirdofmay18081814goya> * anyways" |
| 2024-12-24 01:08:02 +0100 | <haskellbridge> | <thirdofmay18081814goya> of the context*, don't know why I said of the secret |
| 2024-12-24 01:10:17 +0100 | loonycyborg_ | (loonycybor@chantal.wesnoth.org) (Quit: ZNC - http://znc.sourceforge.net) |
| 2024-12-24 01:10:29 +0100 | loonycyborg | (loonycybor@wesnoth/developer/loonycyborg) loonycyborg |
| 2024-12-24 01:10:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:12:36 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-12-24 01:14:44 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2024-12-24 01:14:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 01:22:31 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-12-24 01:26:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:30:58 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 01:31:44 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection) |
| 2024-12-24 01:33:18 +0100 | statusbot | (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Read error: Connection reset by peer) |
| 2024-12-24 01:33:24 +0100 | statusbot8 | (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) statusbot |
| 2024-12-24 01:34:59 +0100 | PotatoGim | (sid99505@id-99505.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:04 +0100 | <loonycyborg> | what would be the best way currently to make a compile-time mapping from strings to types? |
| 2024-12-24 01:35:49 +0100 | snek | (sid280155@id-280155.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:49 +0100 | cbarrett | (uid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:49 +0100 | rubin55 | (sid666177@id-666177.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:49 +0100 | jonrh | (sid5185@id-5185.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:37:20 +0100 | <loonycyborg> | seems use case I have in mind mostly asks for "extensible records", but I don't care about order at all |
| 2024-12-24 01:38:41 +0100 | cbarrett | (uid192934@id-192934.helmsley.irccloud.com) cbarrett |
| 2024-12-24 01:38:43 +0100 | snek | (sid280155@id-280155.lymington.irccloud.com) snek |
| 2024-12-24 01:38:46 +0100 | rubin55 | (sid666177@id-666177.lymington.irccloud.com) rubin55 |
| 2024-12-24 01:38:54 +0100 | PotatoGim | (sid99505@id-99505.lymington.irccloud.com) PotatoGim |
| 2024-12-24 01:39:00 +0100 | jonrh | (sid5185@id-5185.ilkley.irccloud.com) jonrh |
| 2024-12-24 01:41:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:41:41 +0100 | sprotte24 | (~sprotte24@p200300d16f2af800514f7155ca1159f4.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2024-12-24 01:45:46 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 01:47:33 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 272 seconds) |
| 2024-12-24 01:50:40 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-12-24 01:56:50 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:57:02 +0100 | Guest78 | (~Guest78@2a02:8084:1:6500::db) (Quit: Client closed) |
| 2024-12-24 01:57:02 +0100 | <monochrom> | GHC has type-level string literals. |
| 2024-12-24 01:57:12 +0100 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 01:57:12 +0100 | Feuermagier | Guest5199 |
| 2024-12-24 01:57:12 +0100 | Guest5199 | (~Feuermagi@user/feuermagier) (Killed (lead.libera.chat (Nickname regained by services))) |
| 2024-12-24 01:57:12 +0100 | Feuermagier_ | Feuermagier |
| 2024-12-24 01:59:24 +0100 | <EvanR> | yes the string itself is a type of kind Symbol |
| 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 02:00:42 +0100 | Feuermagier | Guest7514 |
| 2024-12-24 02:00:42 +0100 | Feuermagier_ | (~Feuermagi@user/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_ | Feuermagier |
| 2024-12-24 02:00:50 +0100 | <EvanR> | the first ones easier |
| 2024-12-24 02:03:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 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: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:06:24 +0100 | <loonycyborg> | or how I can extract things back to runtime when needed |
| 2024-12-24 02:07:45 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 2024-12-24 02:07:55 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Read error: Connection reset by peer) |
| 2024-12-24 02:08:09 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-24 02:08:11 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 02:08:11 +0100 | <loonycyborg> | this really reminds me of C++ template magic though |
| 2024-12-24 02:08:51 +0100 | poscat0x04 | (~poscat@user/poscat) (Quit: Bye) |
| 2024-12-24 02:10:37 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f41b013a429fe4b7686.dip0.t-ipconnect.de) |
| 2024-12-24 02:11:03 +0100 | <geekosaur> | KnownSymbol and singletons (blech) |
| 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:58 +0100 | <geekosaur> | ("dependent types" = types that depend on runtime values, not just the other way around) |
| 2024-12-24 02:12:11 +0100 | poscat | (~poscat@user/poscat) poscat |
| 2024-12-24 02:13:13 +0100 | <EvanR> | KnownSymbol lets you have the corresponding String at runtime |
| 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:20 +0100 | <EvanR> | similar to KnownNat |
| 2024-12-24 02:13:30 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 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:53 +0100 | son0p | (~ff@186.121.100.67) son0p |
| 2024-12-24 02:13:56 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f25e9e9d221c37061e3.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2024-12-24 02:14:03 +0100 | <loonycyborg> | at *compile time |
| 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:21 +0100 | <EvanR> | but a list is probably the most realistic |
| 2024-12-24 02:14:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 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:15:55 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2024-12-24 02:15:57 +0100 | <loonycyborg> | ye but avoiding traversal of whole list would be nice |
| 2024-12-24 02:16:09 +0100 | <loonycyborg> | at least at runtime |
| 2024-12-24 02:16:26 +0100 | <EvanR> | it's not at runtime |
| 2024-12-24 02:16:37 +0100 | <EvanR> | or so I thought |
| 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:19:01 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2024-12-24 02:19:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-24 02:21:51 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-12-24 02:23:24 +0100 | __monty__ | (~toonn@user/toonn) (Quit: Lost terminal) |
| 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:24:59 +0100 | <EvanR> | any reasoning pattern you use must be reflected in the type system |
| 2024-12-24 02:25:34 +0100 | <EvanR> | or reasoning metapattern |
| 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:52 +0100 | <geekosaur> | you'll need to think through what exactly you're doing to make that decision |
| 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:27:05 +0100 | <EvanR> | Symbols are already types and look like strings |
| 2024-12-24 02:27:23 +0100 | geekosaur | wonders if this is just a dependent map |
| 2024-12-24 02:27:31 +0100 | <haskellbridge> | <thirdofmay18081814goya> how many constructors does your type have? |
| 2024-12-24 02:27:32 +0100 | <geekosaur> | there's packages on Hackage for that already |
| 2024-12-24 02:27:39 +0100 | <EvanR> | was going to suggest looking at how dependent map works, which is already a library |
| 2024-12-24 02:27:48 +0100 | <EvanR> | but was too slow |
| 2024-12-24 02:28:03 +0100 | <loonycyborg> | HList seems to mostly fit |
| 2024-12-24 02:28:31 +0100 | <loonycyborg> | but they all seem to be abandoned by devs with version numbers before 1.0 |
| 2024-12-24 02:28:41 +0100 | <haskellbridge> | <thirdofmay18081814goya> are these any strings or a specific set of strings? |
| 2024-12-24 02:29:36 +0100 | <loonycyborg> | strings are determined by app or modules so it's pretty specific |
| 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:30:14 +0100 | <haskellbridge> | <thirdofmay18081814goya> loonycyborg: and what is the target type? |
| 2024-12-24 02:30:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:30:34 +0100 | <loonycyborg> | each string has own type specified by app or module |
| 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: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:31:15 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 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: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:37 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-24 02:32:16 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 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: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:35:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 02:35:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> * subtype of "TypeFrom String" that you're looking for |
| 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:38:01 +0100 | <loonycyborg> | then total size would be known and indices could be assigned |
| 2024-12-24 02:38:09 +0100 | ft | (~ft@i59F4F0F5.versanet.de) (Ping timeout: 265 seconds) |
| 2024-12-24 02:39:53 +0100 | ft | (~ft@i59F4F055.versanet.de) ft |
| 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: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:43:09 +0100 | califax | (~califax@user/califx) califx |
| 2024-12-24 02:45:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:49:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 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 03:00:01 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 03:01:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:05:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:06:03 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 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:11:59 +0100 | nadja | (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 265 seconds) |
| 2024-12-24 03:12:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2024-12-24 03:12:46 +0100 | nadja | (~dequbed@banana-new.kilobyte22.de) dequbed |
| 2024-12-24 03:13:36 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2024-12-24 03:16:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:17:20 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2024-12-24 03:17:40 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 03:18:21 +0100 | rekahsoft | (~rekahsoft@76.69.85.220) rekahsoft |
| 2024-12-24 03:19:17 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 03:20:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-24 03:22:35 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 260 seconds) |
| 2024-12-24 03:31:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:33:03 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 03:34:44 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-12-24 03:36:08 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Ping timeout: 252 seconds) |
| 2024-12-24 03:40:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:45:40 +0100 | <ski> | thirdofmay18081814goya : hm, not sure i follow that FRP interpretation |
| 2024-12-24 03:46:02 +0100 | <haskellbridge> | <thirdofmay18081814goya> it was slightly wrongly formulated |
| 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:51:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:53:05 +0100 | <haskellbridge> | <thirdofmay18081814goya> "[] Gamma" contains significantly less information than "Gamma" |
| 2024-12-24 03:54:31 +0100 | <haskellbridge> | <thirdofmay18081814goya> but realizes an equivalence relation on (some) permutations of the chains in the partial order given by "Gamma" |
| 2024-12-24 03:54:55 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2024-12-24 03:55:32 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 03:56:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:59:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:00:57 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 2024-12-24 04:01:54 +0100 | <haskellbridge> | <thirdofmay18081814goya> i accidentally stumbled on this while trying to model an frp circuit and realized it has an extremely practical application: i was interested in having my circuit produce an "A" (more specifically, "ScreenCoordinates -> Color"), and realized that it could be constructed from a particular sequence of signals that looked something like "ButtonStates -> ComponentStates -> IndexedLayout ->... |
| 2024-12-24 04:02:00 +0100 | <haskellbridge> | ... CurrentViewport -> (ScreenCoordinates -> Color)" |
| 2024-12-24 04:03:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 04:04:15 +0100 | <haskellbridge> | <thirdofmay18081814goya> then I worried a bit about whether this was a good implementation or a good network configuration or the unique way to obtain that particular function. but if this function is 100% reactive, then we can correctly infer "[] Gamma |- A", i.e., the reactive semantics of this configuration are not affected by the exact order of the signal functions "ButtonStates", "ComponentStates", "IndexedLayout",... |
| 2024-12-24 04:04:20 +0100 | <haskellbridge> | ... "CurrentViewport". we only need their output signal |
| 2024-12-24 04:07:04 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 245 seconds) |
| 2024-12-24 04:07:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> and this is in fact so: if "CurrentViewport" consumes a signal from "IndexedLayout", there is nothing that prevents us from duplicating that signal and also sending it forward in the circuit |
| 2024-12-24 04:08:06 +0100 | <haskellbridge> | <thirdofmay18081814goya> so your comments were very opportune heheh |
| 2024-12-24 04:13:12 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-12-24 04:14:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:14:51 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 04:19:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 04:20:54 +0100 | <ski> | haskellbridge : hm, but wouldn't `[] Gamma |- Gamma' also hold (if `[]' is a "neccesary"-type modality) (this is not true in provability logic, a modal logic explored by George Boolos in "The Logic of Provability", related to stuff like Gödel's incompleteness theorems, and Löb/Curry's theorem), so how can `[] Gamma' then be weaker than `Gamma' ? |
| 2024-12-24 04:21:03 +0100 | <ski> | er |
| 2024-12-24 04:21:06 +0100 | <ski> | thirdofmay18081814goya ^ |
| 2024-12-24 04:24:17 +0100 | ski | . o O ( <https://en.wikipedia.org/wiki/L%C3%B6b's_theorem>,<https://en.wikipedia.org/wiki/Curry%27s_paradox>,<https://en.wikipedia.org/wiki/Provability_logic>,<https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems> ) |
| 2024-12-24 04:24:58 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2024-12-24 04:26:18 +0100 | CrunchyFlakes | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-12-24 04:28:26 +0100 | <ski> | ("there is nothing that prevents us from duplicating that signal and also sending it forward in the circuit" -- sounds like comonadic preservation of context, if `[] A |- B', then `[] A |- [] B', `Comonad w => (w a -> b) -> (w a -> w b)') |
| 2024-12-24 04:28:46 +0100 | CrunchyFlakes | (~CrunchyFl@31.19.233.78) |
| 2024-12-24 04:29:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:34:18 +0100 | <ski> | (also not sure if i should interpret `ButtonStates >-> ComponentStates >-> IndexedLayout >-> CurrentViewport -> (ScreenCoordinates -> Color) |
| 2024-12-24 04:34:44 +0100 | <ski> | (also not sure if i should interpret `ButtonStates >-> ComponentStates >-> IndexedLayout >-> CurrentViewport >-> (ScreenCoordinates -> Color)' as a sequence/graph with five nodes, the last of which is a function type ?) |
| 2024-12-24 04:34:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 04:35:03 +0100 | <ski> | (but i'm probably not following the FRP context here that well ..) |
| 2024-12-24 04:40:46 +0100 | <haskellbridge> | <thirdofmay18081814goya> ski: I don't think so! it seems to me that "Gamma" is a syntactic abbreviation and not a term, so "|- Gamma" is not well defined, but we can attempt to give it two macro-expansions into a well-formed term. A first possibility is "Gamma :: Finite (lengthOf ([] Gamma)) -> Type", which associates the (lengthOf ([] Gamma) 'th pair in "macroExpand ([] Gamma)" or "removeIdenticalTerms $ macroExpand (Gamma... |
| 2024-12-24 04:40:52 +0100 | <haskellbridge> | ... |-)" to a type (effectively a projection function with extracts the type from the pair. But this is just a product type which does not carry any meaningful network configuration information! The second possible interpretation is "Gamma :: (varSymbol, Type) -> varSymbol, Type -> ..." which is a "lengthOf ([] Gamma) = lengthOf (Gamma |-)" function which can only encode a singular, totally ordered sequence of signals |
| 2024-12-24 04:41:21 +0100 | rekahsoft | (~rekahsoft@76.69.85.220) (Remote host closed the connection) |
| 2024-12-24 04:41:30 +0100 | td_ | (~td@i53870924.versanet.de) (Ping timeout: 252 seconds) |
| 2024-12-24 04:41:48 +0100 | <haskellbridge> | <thirdofmay18081814goya> to truly recapture our original context, the left-hand-side term "Gamma" in "[] Gamma |- Gamma" must in fact specify a partial order, which has type "[Chain]" |
| 2024-12-24 04:42:04 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh sorry the right-hand-side term |
| 2024-12-24 04:42:08 +0100 | terrorjack4 | (~terrorjac@2a01:4f8:c17:dc9f::) (Quit: The Lounge - https://thelounge.chat) |
| 2024-12-24 04:43:08 +0100 | td_ | (~td@i53870930.versanet.de) td_ |
| 2024-12-24 04:43:10 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) rekahsoft |
| 2024-12-24 04:43:51 +0100 | terrorjack4 | (~terrorjac@2a01:4f8:c17:dc9f::) terrorjack |
| 2024-12-24 04:45:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:45:43 +0100 | <haskellbridge> | <thirdofmay18081814goya> whoops, mistake on second interpretation equation, is wrong "lengthOf ([] Gamma) = lengthOf (Gamma |-)", it is instead "lengthOf ([] Gamma) = lengthOf $ removeIdenticalTerms (Gamma |-)" |
| 2024-12-24 04:49:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 04:50:15 +0100 | <haskellbridge> | <thirdofmay18081814goya> a valid inference however would be something like "[] Gamma |- e : Exists (x :: [Chain]). [] x = [] Gamma" |
| 2024-12-24 04:51:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh not sure if that notation encodes it very well, but from "[] Gamma" we can infer that there exists a "frpCircuit :: [Chain]" that has "(\x -> [] x) frpCircuit = [] Gamma" |
| 2024-12-24 04:56:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e., what we know from "[] Gamma" is that there is an frp circuit that will produce it, but we don't know the exact network configuration info that tells us which circuit precisely it is that will produce it |
| 2024-12-24 05:00:28 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2024-12-24 05:00:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:01:11 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Read error: Connection reset by peer) |
| 2024-12-24 05:01:22 +0100 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2024-12-24 05:02:30 +0100 | <haskellbridge> | <Bowuigi> Which logic is this one? It looks interesting |
| 2024-12-24 05:03:37 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection) |
| 2024-12-24 05:05:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 05:07:59 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm the above syntax could be interpreted in a dependently-typed type theory extended with only "[] : Type -> Type" or some form of higher order intuitionistic logic with a "[]" operator |
| 2024-12-24 05:09:02 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) rekahsoft |
| 2024-12-24 05:10:10 +0100 | <haskellbridge> | <thirdofmay18081814goya> maybe (probably not) "GADTs" and something something "[]" |
| 2024-12-24 05:10:51 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 272 seconds) |
| 2024-12-24 05:16:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:23:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 05:24:17 +0100 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2024-12-24 05:24:52 +0100 | aforemny | (~aforemny@i59F4C727.versanet.de) aforemny |
| 2024-12-24 05:25:54 +0100 | aforemny_ | (~aforemny@2001:9e8:6cf3:d200:ed4d:2a81:f273:8171) (Ping timeout: 276 seconds) |
| 2024-12-24 05:28:43 +0100 | <haskellbridge> | <Bowuigi> What's this "[]" operator? I'd assume it isn't "List" |
| 2024-12-24 05:32:09 +0100 | <haskellbridge> | <thirdofmay18081814goya> it has no objective meaning (can be given multiple meanings, see the ski comment I quote) but in the syntax above it encodes either an unordered sequence of past effects. the quoted comment itself quotes where ski gives the comonadic laws it satisfies |
| 2024-12-24 05:32:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> ski helpfully suggests it can be interpreted generally as "necessity" or "it is necessary" |
| 2024-12-24 05:34:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:35:48 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 244 seconds) |
| 2024-12-24 05:37:13 +0100 | <EvanR> | so [] is the square modality |
| 2024-12-24 05:37:26 +0100 | <EvanR> | not brackets |
| 2024-12-24 05:37:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> yeah sorry |
| 2024-12-24 05:39:24 +0100 | <haskellbridge> | <Bowuigi> Oh it's modal logic in sequent-ish syntax |
| 2024-12-24 05:40:21 +0100 | <haskellbridge> | <Bowuigi> "Unordered sequence of past effects" seems interesting |
| 2024-12-24 05:41:25 +0100 | <haskellbridge> | <Bowuigi> Also is no modality a sort of middleground between "<>" and "[]"? Or is it a sort of modality polymorphism |
| 2024-12-24 05:41:54 +0100 | <haskellbridge> | <thirdofmay18081814goya> i am not sure of this I am trying to find an answer |
| 2024-12-24 05:42:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-24 05:43:34 +0100 | <haskellbridge> | <Bowuigi> Also how relevant is https://www.researchgate.net/publication/334752231_Implementing_a_modal_dependent_type_theory |
| 2024-12-24 05:44:09 +0100 | invariadic | (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) |
| 2024-12-24 05:45:17 +0100 | <haskellbridge> | <Bowuigi> Or more generally, http://www.danielgratzer.com/papers/multimodal-dependent-type-theory.pdf |
| 2024-12-24 05:45:41 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Ping timeout: 265 seconds) |
| 2024-12-24 05:48:10 +0100 | invariadic | (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) (Client Quit) |
| 2024-12-24 05:49:20 +0100 | invariadic | (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) |
| 2024-12-24 05:49:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> in the frp context above the following is one possible interpretation. generally " (T : Type) |- term : T" can be interpreted as the statement that "T" is a nonempty type, but in an frp circuit whose context is on a timeline it could be interpreted as: at the moment, "T" is a nonempty type. then, "term :: box T" could mean: since the beginning and until the end, "T" is a nonempty type. finally,... |
| 2024-12-24 05:49:38 +0100 | <haskellbridge> | ... "term :: diamond T" could mean: T is an empty type at the moment but there exists a point in time in the future where it is not empty. |
| 2024-12-24 05:50:56 +0100 | <haskellbridge> | <thirdofmay18081814goya> or some variation of these themes |
| 2024-12-24 05:51:36 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: interesting! I will read these articles |
| 2024-12-24 05:51:40 +0100 | <haskellbridge> | <Bowuigi> That's pretty cool |
| 2024-12-24 05:52:17 +0100 | <haskellbridge> | <Bowuigi> Never saw circuits as "possibly empty types depending on time" |
| 2024-12-24 05:52:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:55:35 +0100 | <haskellbridge> | <Bowuigi> I guess one can translate each type in this fashion into a type family indexed by time, with Box being "forall t. F t" and Diamond being "exists t, t>Now. F t" given some definition for "Now" |
| 2024-12-24 05:56:15 +0100 | <haskellbridge> | <Bowuigi> t is the time here, F is the possibly empty type |
| 2024-12-24 05:56:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-24 06:04:36 +0100 | <haskellbridge> | <Bowuigi> Note that this induces an ordering in time, but since it doesn't imply Peano-like axioms, you can have booleans as time if you wanted |
| 2024-12-24 06:05:14 +0100 | <haskellbridge> | <Bowuigi> Notions of "past" and "future" imply this anyways |
| 2024-12-24 06:07:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:12:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 06:14:01 +0100 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) robobub |
| 2024-12-24 06:17:41 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) |
| 2024-12-24 06:23:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:27:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-24 06:27:57 +0100 | dsrt^ | (dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 06:33:55 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-12-24 06:38:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:42:58 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 06:43:43 +0100 | esph | (~weechat@user/esph) esph |
| 2024-12-24 06:51:06 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: i have just discovered myself that it is possible to do this. in a non-modal frp setting, we can posit the context "Gamma = (mkStream : Type -> Type), (n : Nat), (worldVector abbrev wvec : Finite n -> Exists (T : Type). mkStream T), (worldClosure : (T : Type) -> mkStream T -> Exists (fin : Finite n). leftProjection (wvec fin) = T)" where "Exists ... : ... -> (..., ...)" is the dependent... |
| 2024-12-24 06:51:12 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/PBvgtawxtXnBJKOpEuWithmU/8CDgsIaqPKY (4 lines) |
| 2024-12-24 06:53:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:58:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 07:07:03 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-12-24 07:07:17 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2024-12-24 07:08:15 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-24 07:09:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 07:16:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 07:21:24 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-12-24 07:27:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 07:27:59 +0100 | <haskellbridge> | <thirdofmay18081814goya> messed up. need to distinguish the stream and circuit types (lhs of "data ... := ...") from their constructors (rhs of "data ... := ...") |
| 2024-12-24 07:31:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 07:35:10 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: am trying to realize this |
| 2024-12-24 07:39:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 07:39:48 +0100 | invariadic | (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) (Remote host closed the connection) |
| 2024-12-24 07:44:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 07:45:33 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds) |
| 2024-12-24 07:54:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 07:59:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 08:00:19 +0100 | Guest78 | (~Guest78@2a02:8084:1:6500::db) |
| 2024-12-24 08:06:12 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) |
| 2024-12-24 08:10:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 08:15:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 08:25:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 08:29:41 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-12-24 08:29:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 08:40:06 +0100 | l_k | (~student@46.61.242.35) (Ping timeout: 246 seconds) |
| 2024-12-24 08:40:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 08:41:16 +0100 | l_k | (~student@85.172.110.180) |
| 2024-12-24 08:47:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-24 08:49:01 +0100 | CiaoSen | (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-12-24 08:56:24 +0100 | CiaoSen | (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) (Quit: CiaoSen) |
| 2024-12-24 08:58:22 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 08:59:31 +0100 | <iqubic> | Is there a good way to get the nth bit from an integer in Haskell? |
| 2024-12-24 09:00:01 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-12-24 09:00:34 +0100 | CiaoSen | (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-12-24 09:00:37 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2024-12-24 09:03:22 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 09:05:28 +0100 | dsrt^ | (dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 2024-12-24 09:07:25 +0100 | irfan | (~irfan@user/irfan) irfan |
| 2024-12-24 09:13:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 09:15:17 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2024-12-24 09:18:36 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-12-24 09:22:52 +0100 | irfan | (~irfan@user/irfan) (Quit: leaving) |
| 2024-12-24 09:29:08 +0100 | housemate | (~housemate@pa49-185-180-187.pa.vic.optusnet.com.au) housemate |
| 2024-12-24 09:29:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 09:33:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 09:41:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 09:45:02 +0100 | <davean> | iqubic: Bits |
| 2024-12-24 09:45:31 +0100 | <davean> | iqubic: https://hackage.haskell.org/package/base-4.21.0.0/docs/Data-Bits.html#v:testBit |
| 2024-12-24 09:45:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 09:46:08 +0100 | <iqubic> | Yeah, I want something like that, but I want to have it return either a 1 or a 0 instead of a Bool. |
| 2024-12-24 09:46:30 +0100 | <davean> | I mean then shift and mask. |
| 2024-12-24 09:46:45 +0100 | <iqubic> | Is there a better way of doing it than just `\x n -> if testBit x n then 1 else 0`? |
| 2024-12-24 09:47:07 +0100 | <davean> | depends on your definition of better, but shift and masking if you want it non-conditionally |
| 2024-12-24 09:47:13 +0100 | <iqubic> | I see. |
| 2024-12-24 09:47:21 +0100 | <iqubic> | Thanks for the help |
| 2024-12-24 09:47:54 +0100 | <davean> | (a `shiftR` n) .&. 0x1 |
| 2024-12-24 09:48:12 +0100 | <davean> | *assuming* that represents 1 in your type |
| 2024-12-24 09:48:26 +0100 | <davean> | Which there *is no reason to assume* |
| 2024-12-24 09:49:06 +0100 | <davean> | shift and mask is likely faster though, depending on a ton of factors. |
| 2024-12-24 09:49:58 +0100 | <iqubic> | Thanks! |
| 2024-12-24 09:51:40 +0100 | Guest78 | (~Guest78@2a02:8084:1:6500::db) (Ping timeout: 240 seconds) |
| 2024-12-24 09:56:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 09:59:41 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-12-24 10:01:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 10:02:49 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds) |
| 2024-12-24 10:04:24 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 264 seconds) |
| 2024-12-24 10:06:08 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2024-12-24 10:12:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 10:16:04 +0100 | billchenchina | (~billchenc@103.152.35.21) billchenchina |
| 2024-12-24 10:16:09 +0100 | billchenchina | (~billchenc@103.152.35.21) (Remote host closed the connection) |
| 2024-12-24 10:16:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 10:20:03 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3504-8ae4-a87d-f91c-a611-29c0.rev.sfr.net) alexherbo2 |
| 2024-12-24 10:26:21 +0100 | CiaoSen | (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds) |
| 2024-12-24 10:27:15 +0100 | housemate | (~housemate@pa49-185-180-187.pa.vic.optusnet.com.au) (Ping timeout: 260 seconds) |
| 2024-12-24 10:27:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 10:28:15 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3504-8ae4-a87d-f91c-a611-29c0.rev.sfr.net) (Remote host closed the connection) |
| 2024-12-24 10:29:40 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds) |
| 2024-12-24 10:32:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-12-24 10:42:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 10:46:50 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 10:52:01 +0100 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2024-12-24 10:54:34 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-24 10:56:28 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2024-12-24 10:56:28 +0100 | tnt2 | tnt1 |
| 2024-12-24 11:00:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 11:04:56 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 11:05:13 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-12-24 11:06:08 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2024-12-24 11:11:02 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-12-24 11:16:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 11:16:46 +0100 | ash3en | (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) ash3en |
| 2024-12-24 11:19:11 +0100 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2024-12-24 11:19:47 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2024-12-24 11:20:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 11:20:58 +0100 | ash3en | (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit) |
| 2024-12-24 11:23:53 +0100 | gentauro | (~gentauro@user/gentauro) gentauro |
| 2024-12-24 11:30:15 +0100 | gentauro | (~gentauro@user/gentauro) (Ping timeout: 260 seconds) |
| 2024-12-24 11:30:29 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) |
| 2024-12-24 11:31:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 11:36:36 +0100 | gentauro | (~gentauro@user/gentauro) gentauro |
| 2024-12-24 11:38:11 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2024-12-24 11:38:31 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 11:41:37 +0100 | gentauro_ | (~gentauro@cgn-cgn11-185-107-12-141.static.kviknet.net) |
| 2024-12-24 11:41:54 +0100 | gentauro | (~gentauro@user/gentauro) (Ping timeout: 265 seconds) |
| 2024-12-24 11:43:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 11:47:35 +0100 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
| 2024-12-24 11:47:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 11:58:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 11:59:01 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-12-24 12:03:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 12:12:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 12:15:51 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-12-24 12:16:44 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-24 12:16:53 +0100 | kuribas | (~user@ptr-17d51enqg53ahlm81u8.18120a2.ip6.access.telenet.be) kuribas |
| 2024-12-24 12:17:31 +0100 | AlexZenon | (~alzenon@5.139.233.146) (Ping timeout: 252 seconds) |
| 2024-12-24 12:23:25 +0100 | kuribas | (~user@ptr-17d51enqg53ahlm81u8.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2024-12-24 12:27:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 12:27:27 +0100 | AlexZenon | (~alzenon@5.139.233.146) |
| 2024-12-24 12:31:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 12:33:07 +0100 | ash3en | (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) ash3en |
| 2024-12-24 12:33:09 +0100 | ash3en | (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit) |
| 2024-12-24 12:42:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 12:48:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 12:48:58 +0100 | sprotte24 | (~sprotte24@p200300d16f32ae00e0f28665918683b3.dip0.t-ipconnect.de) |
| 2024-12-24 12:59:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 13:00:05 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-12-24 13:03:55 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2024-12-24 13:04:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-24 13:14:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 13:18:11 +0100 | <hellwolf> | who is also using lsp in emacs; how can I enable hlint plugin properly |
| 2024-12-24 13:18:28 +0100 | <hellwolf> | it doesn't seem to have code lens warnings coming from hlint |
| 2024-12-24 13:20:39 +0100 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-12-24 13:21:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |