Logs on 2024-12-24 (liberachat/#haskell)
| 00:00:02 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 00:01:03 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 00:03:06 | Lears | is now known as Leary |
| 00:03:11 | <haskellbridge> | <thirdofmay18081814goya> ski: these comments have suddenly made sense to me, thank you very much again! |
| 00:03:17 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 00:04:21 | → | weary-traveler joins (~user@user/user363627) |
| 00:05:59 | <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" |
| 00:07:36 | <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 |
| 00:07:45 | <haskellbridge> | <thirdofmay18081814goya> * anyways" |
| 00:08:02 | <haskellbridge> | <thirdofmay18081814goya> of the context*, don't know why I said of the secret |
| 00:10:17 | × | loonycyborg_ quits (loonycybor@chantal.wesnoth.org) (Quit: ZNC - http://znc.sourceforge.net) |
| 00:10:29 | → | loonycyborg joins (loonycybor@wesnoth/developer/loonycyborg) |
| 00:10:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:12:36 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 00:14:44 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 00:14:53 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 00:22:31 | → | rvalue joins (~rvalue@user/rvalue) |
| 00:26:02 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:30:58 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 00:31:44 | × | simplystuart quits (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection) |
| 00:33:18 | × | statusbot quits (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Read error: Connection reset by peer) |
| 00:33:24 | → | statusbot8 joins (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) |
| 00:34:59 | × | PotatoGim quits (sid99505@id-99505.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 00:35:04 | <loonycyborg> | what would be the best way currently to make a compile-time mapping from strings to types? |
| 00:35:49 | × | snek quits (sid280155@id-280155.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 00:35:49 | × | cbarrett quits (uid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 245 seconds) |
| 00:35:49 | × | rubin55 quits (sid666177@id-666177.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 00:35:49 | × | jonrh quits (sid5185@id-5185.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 00:37:20 | <loonycyborg> | seems use case I have in mind mostly asks for "extensible records", but I don't care about order at all |
| 00:38:41 | → | cbarrett joins (uid192934@id-192934.helmsley.irccloud.com) |
| 00:38:43 | → | snek joins (sid280155@id-280155.lymington.irccloud.com) |
| 00:38:46 | → | rubin55 joins (sid666177@id-666177.lymington.irccloud.com) |
| 00:38:54 | → | PotatoGim joins (sid99505@id-99505.lymington.irccloud.com) |
| 00:39:00 | → | jonrh joins (sid5185@id-5185.ilkley.irccloud.com) |
| 00:41:25 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:41:41 | × | sprotte24 quits (~sprotte24@p200300d16f2af800514f7155ca1159f4.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 00:45:46 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:47:33 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 272 seconds) |
| 00:50:40 | → | rvalue joins (~rvalue@user/rvalue) |
| 00:56:50 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:57:02 | × | Guest78 quits (~Guest78@2a02:8084:1:6500::db) (Quit: Client closed) |
| 00:57:02 | <monochrom> | GHC has type-level string literals. |
| 00:57:12 | → | Feuermagier_ joins (~Feuermagi@user/feuermagier) |
| 00:57:12 | Feuermagier | is now known as Guest5199 |
| 00:57:12 | × | Guest5199 quits (~Feuermagi@user/feuermagier) (Killed (lead.libera.chat (Nickname regained by services))) |
| 00:57:12 | Feuermagier_ | is now known as Feuermagier |
| 00:59:24 | <EvanR> | yes the string itself is a type of kind Symbol |
| 01:00:31 | <EvanR> | there's "I don't care about order" and "we need the types to enforce nobody not even god can care about order" |
| 01:00:42 | Feuermagier | is now known as Guest7514 |
| 01:00:42 | → | Feuermagier_ joins (~Feuermagi@user/feuermagier) |
| 01:00:42 | × | Guest7514 quits (~Feuermagi@user/feuermagier) (Killed (zirconium.libera.chat (Nickname regained by services))) |
| 01:00:42 | Feuermagier_ | is now known as Feuermagier |
| 01:00:50 | <EvanR> | the first ones easier |
| 01:03:19 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 01:03:23 | <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 |
| 01:06:09 | <loonycyborg> | Seems I can use string literals at compile time with -XDataKinds and -XTypeFamilies but not sure if it's best way currently |
| 01:06:24 | <loonycyborg> | or how I can extract things back to runtime when needed |
| 01:07:45 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 01:07:55 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Read error: Connection reset by peer) |
| 01:08:09 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 01:08:11 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 01:08:11 | <loonycyborg> | this really reminds me of C++ template magic though |
| 01:08:51 | × | poscat0x04 quits (~poscat@user/poscat) (Quit: Bye) |
| 01:10:37 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7283f41b013a429fe4b7686.dip0.t-ipconnect.de) |
| 01:11:03 | <geekosaur> | KnownSymbol and singletons (blech) |
| 01:11:27 | <geekosaur> | you really want Idris or Agda; Haskell doesn't have a real dependent types story as yet |
| 01:11:58 | <geekosaur> | ("dependent types" = types that depend on runtime values, not just the other way around) |
| 01:12:11 | → | poscat joins (~poscat@user/poscat) |
| 01:13:13 | <EvanR> | KnownSymbol lets you have the corresponding String at runtime |
| 01:13:19 | <geekosaur> | also Haskell's type system isn't really up to things like hashmaps; the best it can do is linked lists |
| 01:13:20 | <EvanR> | similar to KnownNat |
| 01:13:30 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 01:13:53 | <loonycyborg> | I was thinking to use array at runtime and calculate indices for it at runtime |
| 01:13:53 | → | son0p joins (~ff@186.121.100.67) |
| 01:13:56 | × | acidjnk_new quits (~acidjnk@p200300d6e7283f25e9e9d221c37061e3.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 01:14:03 | <loonycyborg> | at *compile time |
| 01:14:07 | <EvanR> | if you're feeling nuts you might have success implementing a binary tree in the type system which serves the same purpose |
| 01:14:21 | <EvanR> | but a list is probably the most realistic |
| 01:14:52 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:14:57 | <EvanR> | if you literally don't care about order, then a list still works |
| 01:15:55 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 01:15:57 | <loonycyborg> | ye but avoiding traversal of whole list would be nice |
| 01:16:09 | <loonycyborg> | at least at runtime |
| 01:16:26 | <EvanR> | it's not at runtime |
| 01:16:37 | <EvanR> | or so I thought |
| 01:18:24 | <loonycyborg> | ye I want to build mapping at compile time but make runtime structures based on it |
| 01:19:01 | → | j1n37 joins (~j1n37@user/j1n37) |
| 01:19:35 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 01:21:51 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 01:23:24 | × | __monty__ quits (~toonn@user/toonn) (Quit: Lost terminal) |
| 01:24:34 | <EvanR> | and (before all that) verify what you plan to do at runtime makes any damn sense, which is where it gets complicated |
| 01:24:59 | <EvanR> | any reasoning pattern you use must be reflected in the type system |
| 01:25:34 | <EvanR> | or reasoning metapattern |
| 01:25:36 | <geekosaur> | can you do something like reflecting a type level list into a runtime Vector? |
| 01:25:52 | <geekosaur> | you'll need to think through what exactly you're doing to make that decision |
| 01:26:43 | <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 |
| 01:27:05 | <EvanR> | Symbols are already types and look like strings |
| 01:27:23 | geekosaur | wonders if this is just a dependent map |
| 01:27:31 | <haskellbridge> | <thirdofmay18081814goya> how many constructors does your type have? |
| 01:27:32 | <geekosaur> | there's packages on Hackage for that already |
| 01:27:39 | <EvanR> | was going to suggest looking at how dependent map works, which is already a library |
| 01:27:48 | <EvanR> | but was too slow |
| 01:28:03 | <loonycyborg> | HList seems to mostly fit |
| 01:28:31 | <loonycyborg> | but they all seem to be abandoned by devs with version numbers before 1.0 |
| 01:28:41 | <haskellbridge> | <thirdofmay18081814goya> are these any strings or a specific set of strings? |
| 01:29:36 | <loonycyborg> | strings are determined by app or modules so it's pretty specific |
| 01:29:50 | <Leary> | loonycyborg: There are also packages on hackage for vector/array backed extensible records. As for version numbers, being <1 doesn't mean anything. |
| 01:30:14 | <haskellbridge> | <thirdofmay18081814goya> loonycyborg: and what is the target type? |
| 01:30:15 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:30:34 | <loonycyborg> | each string has own type specified by app or module |
| 01:30:51 | <loonycyborg> | but actual values could be got from command line and other places |
| 01:30:53 | <EvanR> | loonycyborg, a lot of those libraries do exactly what they intended and have no need to keep updating |
| 01:31:15 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 01:31:31 | <EvanR> | it's not like shovelware apps that get kicked off the app store if the dev doesn't change *something* every month |
| 01:31:35 | <haskellbridge> | <thirdofmay18081814goya> loonycyborg: that type is actually equivalent to the finite type counting the number of modules/app |
| 01:31:37 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 01:32:16 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 01:32:21 | <haskellbridge> | <thirdofmay18081814goya> i.e. the finite type whose size is the number of modules/apps will be equivalent to the type you seek |
| 01:33:55 | <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 |
| 01:35:01 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:35:34 | <haskellbridge> | <thirdofmay18081814goya> * subtype of "TypeFrom String" that you're looking for |
| 01:37:44 | <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 |
| 01:38:01 | <loonycyborg> | then total size would be known and indices could be assigned |
| 01:38:09 | × | ft quits (~ft@i59F4F0F5.versanet.de) (Ping timeout: 265 seconds) |
| 01:39:53 | → | ft joins (~ft@i59F4F055.versanet.de) |
| 01:40:34 | <haskellbridge> | <thirdofmay18081814goya> do note that the string-indexing of a type here is not doing any "work" so to say |
| 01:40:53 | <loonycyborg> | Basically I want to make a typesafe variant of system environment, and other structures that are inspired by it in some buildsystems :P |
| 01:43:09 | → | califax joins (~califax@user/califx) |
| 01:45:38 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:49:57 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 01:52:50 | × | dsrt^ quits (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 260 seconds) |
| 02:00:01 | → | dsrt^ joins (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 02:01:02 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:05:42 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 02:06:03 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 02:10:04 | × | rekahsoft quits (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection) |
| 02:11:59 | × | nadja quits (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 265 seconds) |
| 02:12:12 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 02:12:46 | → | nadja joins (~dequbed@banana-new.kilobyte22.de) |
| 02:13:36 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:16:24 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:17:20 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 02:17:40 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 02:18:21 | → | rekahsoft joins (~rekahsoft@76.69.85.220) |
| 02:19:17 | → | emmanuelux_ joins (~emmanuelu@user/emmanuelux) |
| 02:20:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 02:22:35 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Ping timeout: 260 seconds) |
| 02:31:47 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:33:03 | → | _leo___ joins (~emmanuelu@user/emmanuelux) |
| 02:34:44 | → | weary-traveler joins (~user@user/user363627) |
| 02:36:08 | × | emmanuelux_ quits (~emmanuelu@user/emmanuelux) (Ping timeout: 252 seconds) |
| 02:40:59 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 02:45:40 | <ski> | thirdofmay18081814goya : hm, not sure i follow that FRP interpretation |
| 02:46:02 | <haskellbridge> | <thirdofmay18081814goya> it was slightly wrongly formulated |
| 02:50:08 | <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 |
| 02:51:29 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:53:05 | <haskellbridge> | <thirdofmay18081814goya> "[] Gamma" contains significantly less information than "Gamma" |
| 02:54:31 | <haskellbridge> | <thirdofmay18081814goya> but realizes an equivalence relation on (some) permutations of the chains in the partial order given by "Gamma" |
| 02:54:55 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 02:55:32 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 02:56:27 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 02:59:06 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:00:57 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 03:01:54 | <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 ->... |
| 03:02:00 | <haskellbridge> | ... CurrentViewport -> (ScreenCoordinates -> Color)" |
| 03:03:38 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:04:15 | <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",... |
| 03:04:20 | <haskellbridge> | ... "CurrentViewport". we only need their output signal |
| 03:07:04 | × | dsrt^ quits (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 245 seconds) |
| 03:07:11 | <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 |
| 03:08:06 | <haskellbridge> | <thirdofmay18081814goya> so your comments were very opportune heheh |
| 03:13:12 | × | _leo___ quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 03:14:24 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:14:51 | → | dsrt^ joins (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 03:19:10 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 03:20:54 | <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' ? |
| 03:21:03 | <ski> | er |
| 03:21:06 | <ski> | thirdofmay18081814goya ^ |
| 03:24:17 | 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> ) |
| 03:24:58 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 03:26:18 | × | CrunchyFlakes quits (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 03:28:26 | <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)') |
| 03:28:46 | → | CrunchyFlakes joins (~CrunchyFl@31.19.233.78) |
| 03:29:49 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:34:18 | <ski> | (also not sure if i should interpret `ButtonStates >-> ComponentStates >-> IndexedLayout >-> CurrentViewport -> (ScreenCoordinates -> Color) |
| 03:34:44 | <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 ?) |
| 03:34:48 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:35:03 | <ski> | (but i'm probably not following the FRP context here that well ..) |
| 03:40:46 | <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... |
| 03:40:52 | <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 |
| 03:41:21 | × | rekahsoft quits (~rekahsoft@76.69.85.220) (Remote host closed the connection) |
| 03:41:30 | × | td_ quits (~td@i53870924.versanet.de) (Ping timeout: 252 seconds) |
| 03:41:48 | <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]" |
| 03:42:04 | <haskellbridge> | <thirdofmay18081814goya> uh sorry the right-hand-side term |
| 03:42:08 | × | terrorjack4 quits (~terrorjac@2a01:4f8:c17:dc9f::) (Quit: The Lounge - https://thelounge.chat) |
| 03:43:08 | → | td_ joins (~td@i53870930.versanet.de) |
| 03:43:10 | → | rekahsoft joins (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) |
| 03:43:51 | → | terrorjack4 joins (~terrorjac@2a01:4f8:c17:dc9f::) |
| 03:45:34 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:45:43 | <haskellbridge> | <thirdofmay18081814goya> whoops, mistake on second interpretation equation, is wrong "lengthOf ([] Gamma) = lengthOf (Gamma |-)", it is instead "lengthOf ([] Gamma) = lengthOf $ removeIdenticalTerms (Gamma |-)" |
| 03:49:59 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 03:50:15 | <haskellbridge> | <thirdofmay18081814goya> a valid inference however would be something like "[] Gamma |- e : Exists (x :: [Chain]). [] x = [] Gamma" |
| 03:51:35 | <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" |
| 03:56:33 | <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 |
| 04:00:28 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 04:00:55 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:01:11 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Read error: Connection reset by peer) |
| 04:01:22 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 04:02:30 | <haskellbridge> | <Bowuigi> Which logic is this one? It looks interesting |
| 04:03:37 | × | rekahsoft quits (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection) |
| 04:05:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 04:07:59 | <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 |
| 04:09:02 | → | rekahsoft joins (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) |
| 04:10:10 | <haskellbridge> | <thirdofmay18081814goya> maybe (probably not) "GADTs" and something something "[]" |
| 04:10:51 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Ping timeout: 272 seconds) |
| 04:16:18 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:23:12 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 04:24:17 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 04:24:52 | → | aforemny joins (~aforemny@i59F4C727.versanet.de) |
| 04:25:54 | × | aforemny_ quits (~aforemny@2001:9e8:6cf3:d200:ed4d:2a81:f273:8171) (Ping timeout: 276 seconds) |
| 04:28:43 | <haskellbridge> | <Bowuigi> What's this "[]" operator? I'd assume it isn't "List" |
| 04:32:09 | <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 |
| 04:32:33 | <haskellbridge> | <thirdofmay18081814goya> ski helpfully suggests it can be interpreted generally as "necessity" or "it is necessary" |
| 04:34:21 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:35:48 | × | dsrt^ quits (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 244 seconds) |
| 04:37:13 | <EvanR> | so [] is the square modality |
| 04:37:26 | <EvanR> | not brackets |
| 04:37:34 | <haskellbridge> | <thirdofmay18081814goya> yeah sorry |
| 04:39:24 | <haskellbridge> | <Bowuigi> Oh it's modal logic in sequent-ish syntax |
| 04:40:21 | <haskellbridge> | <Bowuigi> "Unordered sequence of past effects" seems interesting |
| 04:41:25 | <haskellbridge> | <Bowuigi> Also is no modality a sort of middleground between "<>" and "[]"? Or is it a sort of modality polymorphism |
| 04:41:54 | <haskellbridge> | <thirdofmay18081814goya> i am not sure of this I am trying to find an answer |
| 04:42:00 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 04:43:34 | <haskellbridge> | <Bowuigi> Also how relevant is https://www.researchgate.net/publication/334752231_Implementing_a_modal_dependent_type_theory |
| 04:44:09 | → | invariadic joins (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) |
| 04:45:17 | <haskellbridge> | <Bowuigi> Or more generally, http://www.danielgratzer.com/papers/multimodal-dependent-type-theory.pdf |
| 04:45:41 | × | rekahsoft quits (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Ping timeout: 265 seconds) |
| 04:48:10 | × | invariadic quits (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) (Client Quit) |
| 04:49:20 | → | invariadic joins (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) |
| 04:49:33 | <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,... |
| 04:49:38 | <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. |
| 04:50:56 | <haskellbridge> | <thirdofmay18081814goya> or some variation of these themes |
| 04:51:36 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: interesting! I will read these articles |
| 04:51:40 | <haskellbridge> | <Bowuigi> That's pretty cool |
| 04:52:17 | <haskellbridge> | <Bowuigi> Never saw circuits as "possibly empty types depending on time" |
| 04:52:30 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:55:35 | <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" |
| 04:56:15 | <haskellbridge> | <Bowuigi> t is the time here, F is the possibly empty type |
| 04:56:53 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 05:04:36 | <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 |
| 05:05:14 | <haskellbridge> | <Bowuigi> Notions of "past" and "future" imply this anyways |
| 05:07:52 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:12:20 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:14:01 | → | robobub joins (uid248673@id-248673.uxbridge.irccloud.com) |
| 05:17:41 | → | xff0x joins (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) |
| 05:23:14 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:27:27 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 05:27:57 | → | dsrt^ joins (dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 05:33:55 | × | gorignak quits (~gorignak@user/gorignak) (Quit: quit) |
| 05:38:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:42:58 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 05:43:43 | → | esph joins (~weechat@user/esph) |
| 05:51:06 | <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... |
| 05:51:12 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/PBvgtawxtXnBJKOpEuWithmU/8CDgsIaqPKY (4 lines) |
| 05:53:43 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:58:18 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 06:07:03 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 06:07:17 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 06:08:15 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 06:09:06 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:16:04 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 06:21:24 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:27:19 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:27:59 | <haskellbridge> | <thirdofmay18081814goya> messed up. need to distinguish the stream and circuit types (lhs of "data ... := ...") from their constructors (rhs of "data ... := ...") |
| 06:31:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 06:35:10 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: am trying to realize this |
| 06:39:21 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:39:48 | × | invariadic quits (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) (Remote host closed the connection) |
| 06:44:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 06:45:33 | × | xff0x quits (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds) |
| 06:54:42 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:59:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 07:00:19 | → | Guest78 joins (~Guest78@2a02:8084:1:6500::db) |
| 07:06:12 | → | xff0x joins (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) |
| 07:10:05 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:15:02 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 07:25:29 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:29:41 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:29:59 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 07:40:06 | × | l_k quits (~student@46.61.242.35) (Ping timeout: 246 seconds) |
| 07:40:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:41:16 | → | l_k joins (~student@85.172.110.180) |
| 07:47:01 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 07:49:01 | → | CiaoSen joins (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) |
| 07:56:24 | × | CiaoSen quits (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) (Quit: CiaoSen) |
| 07:58:22 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:59:31 | <iqubic> | Is there a good way to get the nth bit from an integer in Haskell? |
| 08:00:01 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 08:00:34 | → | CiaoSen joins (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) |
| 08:00:37 | → | caconym joins (~caconym@user/caconym) |
| 08:03:22 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 08:05:28 | × | dsrt^ quits (dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 08:07:25 | → | irfan joins (~irfan@user/irfan) |
| 08:13:45 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:15:17 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 08:18:36 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 08:22:52 | × | irfan quits (~irfan@user/irfan) (Quit: leaving) |
| 08:29:08 | → | housemate joins (~housemate@pa49-185-180-187.pa.vic.optusnet.com.au) |
| 08:29:08 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:33:49 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 08:41:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:45:02 | <davean> | iqubic: Bits |
| 08:45:31 | <davean> | iqubic: https://hackage.haskell.org/package/base-4.21.0.0/docs/Data-Bits.html#v:testBit |
| 08:45:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 08:46:08 | <iqubic> | Yeah, I want something like that, but I want to have it return either a 1 or a 0 instead of a Bool. |
| 08:46:30 | <davean> | I mean then shift and mask. |
| 08:46:45 | <iqubic> | Is there a better way of doing it than just `\x n -> if testBit x n then 1 else 0`? |
| 08:47:07 | <davean> | depends on your definition of better, but shift and masking if you want it non-conditionally |
| 08:47:13 | <iqubic> | I see. |
| 08:47:21 | <iqubic> | Thanks for the help |
| 08:47:54 | <davean> | (a `shiftR` n) .&. 0x1 |
| 08:48:12 | <davean> | *assuming* that represents 1 in your type |
| 08:48:26 | <davean> | Which there *is no reason to assume* |
| 08:49:06 | <davean> | shift and mask is likely faster though, depending on a ton of factors. |
| 08:49:58 | <iqubic> | Thanks! |
| 08:51:40 | × | Guest78 quits (~Guest78@2a02:8084:1:6500::db) (Ping timeout: 240 seconds) |
| 08:56:43 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:59:41 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 09:01:14 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 09:02:49 | × | xff0x quits (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds) |
| 09:04:24 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 264 seconds) |
| 09:06:08 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 09:12:04 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 09:16:04 | → | billchenchina joins (~billchenc@103.152.35.21) |
| 09:16:09 | × | billchenchina quits (~billchenc@103.152.35.21) (Remote host closed the connection) |
| 09:16:32 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 09:20:03 | → | alexherbo2 joins (~alexherbo@2a02-8440-3504-8ae4-a87d-f91c-a611-29c0.rev.sfr.net) |
| 09:26:21 | × | CiaoSen quits (~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds) |
| 09:27:15 | × | housemate quits (~housemate@pa49-185-180-187.pa.vic.optusnet.com.au) (Ping timeout: 260 seconds) |
| 09:27:27 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 09:28:15 | × | alexherbo2 quits (~alexherbo@2a02-8440-3504-8ae4-a87d-f91c-a611-29c0.rev.sfr.net) (Remote host closed the connection) |
| 09:29:40 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds) |
| 09:32:35 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 09:42:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 09:46:50 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 09:52:01 | → | mari-estel joins (~mari-este@user/mari-estel) |
| 09:54:34 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 09:56:28 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 09:56:28 | tnt2 | is now known as tnt1 |
| 10:00:38 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 10:04:56 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 10:05:13 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 10:06:08 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 10:11:02 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 10:16:01 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 10:16:46 | → | ash3en joins (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) |
| 10:19:11 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 10:19:47 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 10:20:38 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 10:20:58 | × | ash3en quits (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit) |
| 10:23:53 | → | gentauro joins (~gentauro@user/gentauro) |
| 10:30:15 | × | gentauro quits (~gentauro@user/gentauro) (Ping timeout: 260 seconds) |
| 10:30:29 | → | xff0x joins (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) |
| 10:31:24 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 10:36:36 | → | gentauro joins (~gentauro@user/gentauro) |
| 10:38:11 | → | __monty__ joins (~toonn@user/toonn) |
| 10:38:31 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 10:41:37 | → | gentauro_ joins (~gentauro@cgn-cgn11-185-107-12-141.static.kviknet.net) |
| 10:41:54 | × | gentauro quits (~gentauro@user/gentauro) (Ping timeout: 265 seconds) |
| 10:43:21 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 10:47:35 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 10:47:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 10:58:42 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 10:59:01 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 11:03:39 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 11:12:02 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 11:15:51 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 11:16:44 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 11:16:53 | → | kuribas joins (~user@ptr-17d51enqg53ahlm81u8.18120a2.ip6.access.telenet.be) |
| 11:17:31 | × | AlexZenon quits (~alzenon@5.139.233.146) (Ping timeout: 252 seconds) |
| 11:23:25 | × | kuribas quits (~user@ptr-17d51enqg53ahlm81u8.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 11:27:24 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 11:27:27 | → | AlexZenon joins (~alzenon@5.139.233.146) |
| 11:31:43 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 11:33:07 | → | ash3en joins (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) |
| 11:33:09 | × | ash3en quits (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit) |
| 11:42:48 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 11:48:49 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 11:48:58 | → | sprotte24 joins (~sprotte24@p200300d16f32ae00e0f28665918683b3.dip0.t-ipconnect.de) |
| 11:59:30 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 12:00:05 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 12:03:55 | → | caconym joins (~caconym@user/caconym) |
| 12:04:00 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 12:14:53 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 12:18:11 | <hellwolf> | who is also using lsp in emacs; how can I enable hlint plugin properly |
| 12:18:28 | <hellwolf> | it doesn't seem to have code lens warnings coming from hlint |
| 12:20:39 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 12:21:57 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 12:24:51 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 12:28:21 | × | mari-estel quits (~mari-este@user/mari-estel) (Quit: nelli xmas) |
| 12:32:56 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 12:37:28 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 12:42:26 | × | tnt1 quits (~Thunderbi@user/tnt1) (Remote host closed the connection) |
| 12:43:01 | × | eL_Bart0 quits (eL_Bart0@dietunichtguten.org) (Ping timeout: 244 seconds) |
| 12:45:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 12:49:51 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 12:53:35 | × | CrunchyFlakes quits (~CrunchyFl@31.19.233.78) (Read error: Connection reset by peer) |
| 12:56:01 | → | CrunchyFlakes joins (~CrunchyFl@31.19.233.78) |
| 13:00:42 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 13:04:59 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 13:05:47 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 13:16:04 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 13:18:07 | → | ash3en joins (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) |
| 13:20:18 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 13:20:35 | × | ash3en quits (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit) |
| 13:25:15 | → | Nixkernal joins (~Nixkernal@90.74.198.178.dynamic.cust.swisscom.net) |
| 13:31:27 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 13:32:43 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 13:35:46 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 13:35:48 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 13:36:09 | → | gorignak joins (~gorignak@user/gorignak) |
| 13:36:32 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 13:36:50 | → | califax joins (~califax@user/califx) |
| 13:45:24 | → | korrykatti joins (~korrykatt@user/korrykatti) |
| 13:45:26 | × | korrykatti quits (~korrykatt@user/korrykatti) (Remote host closed the connection) |
| 13:46:19 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 13:49:41 | → | itaipu joins (~itaipu@168.121.98.246) |
| 13:52:46 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 14:04:23 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 14:06:30 | → | ubert joins (~Thunderbi@p200300ecdf117cf78af43359d271b243.dip0.t-ipconnect.de) |
| 14:09:03 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 14:19:44 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 14:21:04 | → | hseg joins (~gesh@46.120.21.36) |
| 14:24:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 14:30:21 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 14:35:08 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 14:37:24 | <hseg> | Weirdly enough, I'm getting a type error building chs-cabal, but only on non-windows systems and on ghc 8.10.7? https://0x0.st/8rJU.txt |
| 14:40:22 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 14:40:48 | × | toch quits (toch@user/toch) (Ping timeout: 276 seconds) |
| 14:42:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 14:44:22 | <int-e> | Looks like Cabal-3.14 is too new for this. |
| 14:44:30 | → | toch joins (~toch@user/toch) |
| 14:44:48 | <int-e> | for reference, GHC 8.10.7 shipped with Cabal-3.2.1 |
| 14:45:25 | <int-e> | (well, 3.2.1.0) |
| 14:48:08 | → | toch_ joins (toch@user/toch) |
| 14:48:16 | <hseg> | Odd that cabal tried to build chs-cabal-0.1.1.2 with Cabal-3.14.0.0 -- that is specifically listed as out-of-range on hackage |
| 14:48:48 | <int-e> | it's not a library dependency though, it's a build tool dependency |
| 14:49:14 | × | toch quits (~toch@user/toch) (Ping timeout: 272 seconds) |
| 14:49:17 | <hseg> | https://hackage.haskell.org/package/chs-cabal-0.1.1.2/dependencies no? it _is_ a library dep |
| 14:49:46 | <int-e> | Oh, looking at the wrong package |
| 14:50:06 | <hseg> | this build run comes from https://github.com/haskell/ghcup-hs/pull/1182 |
| 14:50:06 | <int-e> | but (evidently) that still doesn't prevent building Setup.{l}hs with Cabal>=3.14 |
| 14:51:21 | <int-e> | And that generates a somethingPathsomething file that use that new SymbolicPath abstraction. |
| 14:51:47 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 14:52:12 | <int-e> | IIUC |
| 14:52:35 | <int-e> | My reasoning is very much guided by actually having that error. |
| 14:52:45 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Ping timeout: 260 seconds) |
| 14:53:19 | <hseg> | hrm. who should I prod about this? |
| 14:53:24 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 14:54:33 | <hseg> | also, why would this not cause trouble with windows? |
| 14:55:39 | <hseg> | ah, I see - for some reason, cabal there decided to build with Cabal-3.12.1.0 |
| 14:56:09 | <hseg> | .. actually, I see multiple Cabals there? |
| 14:56:21 | <hseg> | it also builds Cabal-3.10.3.0 |
| 14:56:28 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 14:57:43 | <hseg> | hrm. it seems all the builds build Cabal-3.10.3.0, but windows/nonwindows differ on which newer cabal to build in addition -- 3.12.1.0 (windows, which works) or 3.14.0.0 (nonwindows, which breaks) |
| 15:02:02 | <hseg> | ahh -- the problem is the version of the cabal-install package these are built with, I think |
| 15:02:30 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 15:04:24 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 15:05:10 | × | ubert quits (~Thunderbi@p200300ecdf117cf78af43359d271b243.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 15:06:00 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 15:07:19 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 15:09:11 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 15:15:25 | <int-e> | I think what chs-cabal needs is an upper bound on its cabal-version field |
| 15:16:05 | <int-e> | well, for 0.1.1.2 at least |
| 15:16:51 | <int-e> | there's a 0.1.1.4 that works with Cabal-3.14? |
| 15:17:52 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 15:19:28 | <hseg> | https://hackage.haskell.org/package/chs-cabal-0.1.1.2/src/chs-cabal.cabal sets cabal-version to 1.18, so I don't _think_ that's the right place to blame? |
| 15:20:47 | <hseg> | indeed, https://hackage.haskell.org/package/chs-cabal-0.1.1.2/revisions/ seems to have deliberately introduced that upper bound? |
| 15:21:29 | <int-e> | hrm |
| 15:22:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 15:22:15 | <int-e> | https://cabal.readthedocs.io/en/3.4/cabal-package.html#pkg-field-cabal-version ...okay I'm confused. There used to be a lower bound syntax here but that's discontinued. |
| 15:24:39 | <int-e> | I guess 3.14 should conservatively refuse to work with any package that doesn't specify cabal-version: 3.14 or later? ("refuse" - it can still build Setup executable with an older Cabal version) |
| 15:25:14 | <int-e> | Oh I hate the fact that DDG found docs for version 3.4. |
| 15:25:45 | × | Natch quits (~natch@c-92-34-7-158.bbcust.telenor.se) (Ping timeout: 252 seconds) |
| 15:26:39 | <hseg> | note that cabal-version is the version of the .cabal format |
| 15:26:43 | <hseg> | not of the build tool |
| 15:28:03 | <int-e> | Yes but my understanding is that the build tool semantics are not supposed to change either. |
| 15:28:30 | <int-e> | So if a generated file isn't backwards compatible... that's very murky. |
| 15:29:01 | <int-e> | Anyway, the real issue I have is that there's no way I can see to *express* that Cabal-3.14 is unfit for building that package. |
| 15:29:48 | <int-e> | I can live with a breaking change that only affects a few packages (using those Path modules is not too common) |
| 15:30:32 | <hseg> | should I perhaps post this to the cabal-install github? |
| 15:33:15 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 15:35:07 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:35:46 | × | xff0x quits (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds) |
| 15:40:07 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 15:45:58 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 15:48:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 15:52:50 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 15:58:36 | → | sayurc joins (~sayurc@169.150.203.34) |
| 16:03:42 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 16:08:21 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 16:11:09 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 16:19:05 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 16:19:59 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 16:22:46 | → | pavonia joins (~user@user/siracusa) |
| 16:23:34 | × | CrunchyFlakes quits (~CrunchyFl@31.19.233.78) (Read error: Connection reset by peer) |
| 16:23:37 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 16:26:01 | → | CrunchyFlakes joins (~CrunchyFl@31.19.233.78) |
| 16:30:52 | × | notzmv quits (~umar@user/notzmv) (Ping timeout: 265 seconds) |
| 16:31:54 | → | ubert joins (~Thunderbi@p200300ecdf117cf7bdcd23ba5c3b89f8.dip0.t-ipconnect.de) |
| 16:34:28 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 16:37:34 | <geekosaur> | if you think you have a bug, yes. At worst someone will tell you how it's supposed to work |
| 16:37:48 | → | prasad joins (~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net) |
| 16:38:45 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 16:45:16 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 16:49:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 16:52:43 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 16:53:36 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 16:58:42 | → | notzmv joins (~umar@user/notzmv) |
| 17:03:34 | × | ridcully quits (~ridcully@p57b52ec2.dip0.t-ipconnect.de) (Quit: WeeChat 4.4.2) |
| 17:03:52 | → | ridcully joins (~ridcully@p57b52ec2.dip0.t-ipconnect.de) |
| 17:04:42 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 17:09:41 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:10:47 | zero | is now known as zzz |
| 17:11:28 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 17:12:13 | → | euphores joins (~SASL_euph@user/euphores) |
| 17:19:21 | × | sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
| 17:20:54 | → | sayurc joins (~sayurc@169.150.203.34) |
| 17:22:45 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 17:27:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 17:29:58 | × | robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:38:07 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 17:42:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 17:46:45 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 17:53:12 | × | ensyde quits (~ensyde@c-73-147-64-74.hsd1.va.comcast.net) (Ping timeout: 276 seconds) |
| 17:53:29 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 17:55:20 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 17:58:21 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 18:04:27 | → | weary-traveler joins (~user@user/user363627) |
| 18:05:57 | <hseg> | it appears to have been a false alarm -- the freezefile ghcup was using is dated to two days prior to the hackage revision that put the upper bound on Cabal for chs-cabal |
| 18:06:27 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 18:06:50 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 18:08:52 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:13:10 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 18:13:30 | × | prasad quits (~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net) (Remote host closed the connection) |
| 18:13:46 | → | prasad joins (~Thunderbi@2601:243:c001:3f07::e5) |
| 18:16:38 | × | mesaoptimizer quits (~mesa@user/PapuaHardyNet) (Ping timeout: 252 seconds) |
| 18:18:48 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 18:21:11 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 18:21:57 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 18:22:13 | <hololeap> | is there a way to search hackage/hoogle for instances? e.g. I want to see if there's a package out there that defines an Arbitrary instance for HashMap |
| 18:22:33 | Lord_of_Life_ | is now known as Lord_of_Life |
| 18:23:54 | <EvanR> | orphaned instances |
| 18:24:05 | <EvanR> | :scream: |
| 18:24:14 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:25:06 | <hololeap> | I did find this, but only because the package name gave it away: https://hackage.haskell.org/package/quickcheck-instances-0.3.32/docs/Test-QuickCheck-Instances-UnorderedContainers.html |
| 18:28:48 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 18:35:59 | × | hseg quits (~gesh@46.120.21.36) (Ping timeout: 260 seconds) |
| 18:39:36 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:39:57 | <hololeap> | I guess since orphan instances are supposed to be really loudly advertised, searching hackage for "orphans" or "instances" is a good way to do it |
| 18:40:39 | <monochrom> | heh yeah |
| 18:41:00 | <hololeap> | I wanted to see how other people are defining 'shrink' for HashMap since I don't really understand that function |
| 18:43:38 | <loonycyborg> | what is haskellbridge connected with? Matrix, discord something else? |
| 18:43:54 | <monochrom> | Matrix. |
| 18:44:45 | <loonycyborg> | I can join there too. What's the link to matrix room? |
| 18:45:40 | <monochrom> | I don't know. |
| 18:46:41 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 18:48:38 | <int-e> | /whois haskellbridge has a link to more info |
| 18:57:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:59:41 | → | mesaoptimizer joins (~mesa@user/PapuaHardyNet) |
| 19:02:38 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 19:04:14 | <haskellbridge> | <loonycyborg> found it |
| 19:13:02 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:16:31 | → | Natch joins (~natch@c-92-34-7-158.bbcust.telenor.se) |
| 19:17:49 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 19:18:07 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 19:22:16 | × | Natch quits (~natch@c-92-34-7-158.bbcust.telenor.se) (Ping timeout: 252 seconds) |
| 19:22:23 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 19:22:55 | × | prasad quits (~Thunderbi@2601:243:c001:3f07::e5) (Ping timeout: 264 seconds) |
| 19:23:16 | → | Natch joins (~natch@c-92-34-7-158.bbcust.telenor.se) |
| 19:25:02 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:25:48 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 19:29:20 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 19:34:51 | → | prasad joins (~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net) |
| 19:35:05 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:35:25 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 19:38:18 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 246 seconds) |
| 19:40:24 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:45:00 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 19:53:52 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 19:55:46 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:00:01 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 20:00:24 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:00:38 | → | caconym joins (~caconym@user/caconym) |
| 20:11:10 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:15:01 | × | tinjamin4 quits (~tinjamin@banshee.h4x0r.space) (Quit: The Lounge - https://thelounge.chat) |
| 20:15:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:16:31 | → | tinjamin4 joins (~tinjamin@banshee.h4x0r.space) |
| 20:16:36 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 20:23:21 | × | CrunchyFlakes quits (~CrunchyFl@31.19.233.78) (Read error: Connection reset by peer) |
| 20:25:34 | → | CrunchyFlakes joins (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) |
| 20:26:31 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:32:32 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 20:33:57 | × | coldtom quits (~coldtom@coldrick.cc) (Ping timeout: 248 seconds) |
| 20:34:51 | × | mhatta_ quits (~mhatta@www21123ui.sakura.ne.jp) (Ping timeout: 252 seconds) |
| 20:36:33 | → | mhatta joins (~mhatta@www21123ui.sakura.ne.jp) |
| 20:38:13 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 248 seconds) |
| 20:39:33 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 20:39:40 | → | Guest31 joins (~Guest31@2405:201:e054:d01c:8f8f:fa81:ee08:421) |
| 20:39:56 | <Guest31> | hi guys! |
| 20:43:39 | <Guest31> | ugh alright. bye guys!!! |
| 20:43:48 | × | Guest31 quits (~Guest31@2405:201:e054:d01c:8f8f:fa81:ee08:421) (Client Quit) |
| 20:43:56 | <yushyin> | ? |
| 20:44:42 | <darkling> | You didn't answer within 3m43s. Far too slow... |
| 20:46:45 | × | edwtjo quits (~edwtjo@fsf/member/edwtjo) (Ping timeout: 248 seconds) |
| 20:47:03 | → | edwtjo joins (~edwtjo@fsf/member/edwtjo) |
| 20:48:03 | <Rembane> | Well the guest didn't say anything of substance so I think we're all forgiven. |
| 20:48:28 | <monochrom> | "dinner calls" |
| 20:50:57 | × | forell quits (~forell@user/forell) (Ping timeout: 248 seconds) |
| 20:51:29 | <Rembane> | Call of the Dinner, the less famous book by Jack London |
| 20:52:21 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 21:03:49 | × | cptaffe quits (~cptaffe@user/cptaffe) (Ping timeout: 252 seconds) |
| 21:04:08 | → | cptaffe joins (~cptaffe@user/cptaffe) |
| 21:13:47 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:17:08 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 21:18:44 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 21:29:17 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:30:54 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:34:07 | <haskellbridge> | <geekosaur> loonycyborg, you might also be interested in #haskell:matrix.org (https://matrix.to/#/%23haskell%3Amatrix.org) (which is separate by their request) |
| 21:35:49 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 21:38:16 | × | prasad quits (~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net) (Ping timeout: 265 seconds) |
| 21:41:24 | → | robobub joins (uid248673@id-248673.uxbridge.irccloud.com) |
| 21:46:14 | → | Guest65 joins (~Guest65@2402:e280:3d29:67b:c89:46c4:c0e1:a8be) |
| 21:47:15 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:47:59 | × | Guest65 quits (~Guest65@2402:e280:3d29:67b:c89:46c4:c0e1:a8be) (Client Quit) |
| 21:51:36 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 21:52:57 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 22:15:44 | × | Patternmaster quits (~georg@user/Patternmaster) (Ping timeout: 272 seconds) |
| 22:16:17 | → | Patternmaster joins (~georg@vmi1645272.contaboserver.net) |
| 22:16:17 | × | Patternmaster quits (~georg@vmi1645272.contaboserver.net) (Changing host) |
| 22:16:17 | → | Patternmaster joins (~georg@user/Patternmaster) |
| 22:17:59 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:22:44 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 22:28:23 | → | forell joins (~forell@user/forell) |
| 22:28:51 | → | Everything joins (~Everythin@195.138.86.118) |
| 22:33:22 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:36:22 | → | superstar64 joins (~superstar@2600:1700:ed80:50a0::41) |
| 22:37:10 | → | ash3en joins (~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) |
| 22:38:15 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 22:40:49 | × | Raito_Bezarius quits (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 245 seconds) |
| 22:42:14 | → | Raito_Bezarius joins (~Raito@wireguard/tunneler/raito-bezarius) |
| 22:47:54 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Quit: leaving) |
| 22:48:47 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:50:42 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 22:53:00 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 22:53:05 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 22:56:16 | → | j1n37 joins (~j1n37@user/j1n37) |
| 22:57:27 | × | tt12310978324354 quits (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 246 seconds) |
| 22:58:42 | × | j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 22:59:32 | × | sayurc quits (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
| 22:59:48 | → | sayurc joins (~sayurc@169.150.203.34) |
| 23:04:10 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:07:26 | → | j1n37 joins (~j1n37@user/j1n37) |
| 23:10:42 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:18:43 | × | sprotte24 quits (~sprotte24@p200300d16f32ae00e0f28665918683b3.dip0.t-ipconnect.de) (Quit: Leaving) |
| 23:19:51 | × | ubert quits (~Thunderbi@p200300ecdf117cf7bdcd23ba5c3b89f8.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 23:20:01 | → | ubert1 joins (~Thunderbi@p200300ecdf117c0013c0076e2e9d6026.dip0.t-ipconnect.de) |
| 23:22:12 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:22:26 | ubert1 | is now known as ubert |
| 23:27:16 | → | cuteguest joins (~cuteguest@2601:602:680:2280::5d66) |
| 23:27:19 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 23:31:05 | <cuteguest> | hmm hmm im still stuck on the same problem as b4.. i hav a type class that relates a type to two GADTs like this (class Elmo a where type Bert :: a -> Type, type Ernie :: a -> Type).. is there a way to hav a type class like this that ensures each value of a has only 1 corresponding type? like, is there a way to show that these GADTs have only 1 |
| 23:31:05 | <cuteguest> | constructor for each value of a? |
| 23:32:54 | <cuteguest> | id like it so that if i had a function from Bert a to Ernie a that i could pattern match on the results if i knew the input type |
| 23:37:34 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:40:20 | <cuteguest> | ar we allowed to post pastebins in here? that might make it easier to read.. |
| 23:41:44 | <cuteguest> | ooh wait i see the thing up top.. hold on |
| 23:42:13 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 23:43:16 | <cuteguest> | hmm mayb christmas eve is the wrong time to ask questions :3 |
| 23:45:23 | <cuteguest> | im gonna post the full link.. i hope its ok >_< |
| 23:45:35 | <darkling> | If you have a pastebin, that's a good way of showing people your code. Go for it. |
| 23:45:41 | <cuteguest> | https://paste.tomsmeding.com/99l00Nhb |
| 23:45:59 | <darkling> | (I'm unlikely to be able to help directly; that's about as much as I can do here). |
| 23:46:06 | <cuteguest> | <33 |
| 23:46:57 | <cuteguest> | i appreciate your response at the v least |
| 23:52:56 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:55:20 | <geekosaur> | the only thing I can think of is this sounds slightly like a pattern synonym, otherwise it sounds "backwards" because typeclasses don't do that kind of thing, GADTs do |
| 23:56:38 | <cuteguest> | pattern synonym.. interesting.. thankyou |
| 23:57:15 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
All times are in UTC on 2024-12-24.