| 2024-09-10 00:00:20 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 00:00:27 +0200 | <ski> | in Mercury, there's type inference, for that clause, yes |
| 2024-09-10 00:00:48 +0200 | <ski> | in Prolog .. well, it's not statically typed, so neither type inference nor type checking |
| 2024-09-10 00:00:59 +0200 | <tomsmeding> | hm |
| 2024-09-10 00:01:23 +0200 | <tomsmeding> | monochrom: you said that "type" isn't even rigorously defined, did you have a good "weird language" in mind here :p |
| 2024-09-10 00:01:40 +0200 | <haskellbridge> | <thirdofmay18081814goya> tomsmeding: i think a formal statement that resolves this would be: "\x:T -> x" is not a typing judgment and can only be type-checked by being such a typing judgment, so the only possibility for producing a well-typed program must be to first run type inference to produce "{} |- \x:T -> x : T -> T" |
| 2024-09-10 00:01:45 +0200 | <haskellbridge> | <thirdofmay18081814goya> no? |
| 2024-09-10 00:01:50 +0200 | <monochrom> | Does COBOL count? >:) |
| 2024-09-10 00:01:54 +0200 | <ski> | the interpretation of that clause, in Prolog (borrowing Mercury syntax to explicate the implicit quantification), is |
| 2024-09-10 00:02:11 +0200 | <ski> | all [X,Y] ( f(X) :- X = Y,Y = foo ). |
| 2024-09-10 00:02:18 +0200 | <ski> | while, in Mercury, it would be |
| 2024-09-10 00:02:24 +0200 | <monochrom> | I haven't seen a weird language. People have a surprisingly good and uncontrovserial consensus. |
| 2024-09-10 00:02:32 +0200 | <tomsmeding> | thirdofmay: '\x:T -> x' is a _term_, and a term is not the same as a judgement, indeed |
| 2024-09-10 00:02:34 +0200 | <ski> | all [X] ( f(X) :- some [Y] ( X = Y,Y = foo ) ). |
| 2024-09-10 00:02:51 +0200 | <ski> | which is of course logically equivalent to the former |
| 2024-09-10 00:02:57 +0200 | <sprout> | type has a lot of competing possible meanings. abstract label as in type theory, a set as in set theory, a catagory, or something corresponding to something in the operational semantics |
| 2024-09-10 00:03:05 +0200 | <ski> | .. but this difference sometimes matters |
| 2024-09-10 00:03:12 +0200 | <monochrom> | OK, one more try. Does set theory count? >:D |
| 2024-09-10 00:03:20 +0200 | <sprout> | and that are only 4 of the top of my head |
| 2024-09-10 00:03:40 +0200 | CiaoSen | (~Jura@2a05:5800:206:9700:ca4b:d6ff:fec1:99da) |
| 2024-09-10 00:03:49 +0200 | <ski> | (.. although, in some cases, Prolog behaves as if it does the latter. but this is outside of the core theory of plain Horn clauses) |
| 2024-09-10 00:03:58 +0200 | <sprout> | ah, logical proposition too. let's not foget curry howard |
| 2024-09-10 00:04:07 +0200 | <sprout> | *forget |
| 2024-09-10 00:04:23 +0200 | <haskellbridge> | <thirdofmay18081814goya> tomsmeding: hm but then where is the problem? |
| 2024-09-10 00:04:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 00:05:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> if we want a program that takes a partially annotated context and produces a well-typed context or the proposition that it can't be typed, we have all we need no? |
| 2024-09-10 00:05:13 +0200 | <sprout> | hmm, don't lay in an awkward position on the couch maybe |
| 2024-09-10 00:05:15 +0200 | <tomsmeding> | thirdofmay: at this point you'd first have to specify exactly what the inputs to, and outputs of, your type checking/inference algorithms are |
| 2024-09-10 00:05:25 +0200 | sprout | sits up |
| 2024-09-10 00:05:41 +0200 | <tomsmeding> | and at that point we're talking more about particular algorithms than about the overarching theory |
| 2024-09-10 00:06:09 +0200 | <tomsmeding> | can the algorithm handle open terms? If so, does it take a list of variables with Maybe Type annotations, or something else? |
| 2024-09-10 00:06:25 +0200 | <tomsmeding> | there's not a _whole_ lot of possible variations here |
| 2024-09-10 00:06:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> tomsmeding: a partially annotated context, so an ordered set containing either typing judgments or terms |
| 2024-09-10 00:06:47 +0200 | <tomsmeding> | not typing jugements, pairs of a name and a type |
| 2024-09-10 00:07:00 +0200 | <ski> | tomsmeding : Mercury borrows quite heavily from Haskell (and the MLs), in the type system |
| 2024-09-10 00:07:00 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah that works better |
| 2024-09-10 00:07:08 +0200 | <ski> | (it even has type classes ..) |
| 2024-09-10 00:07:29 +0200 | <tomsmeding> | ok people I dunno right |
| 2024-09-10 00:07:54 +0200 | <tomsmeding> | if you want to get this technical, write the definitions down rigorously in mathematical language, instead of in English |
| 2024-09-10 00:08:03 +0200 | <tomsmeding> | then we can talk about technicalities |
| 2024-09-10 00:08:17 +0200 | <tomsmeding> | also it's past midnight here, so I'm off to bed |
| 2024-09-10 00:08:33 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 00:08:49 +0200 | <haskellbridge> | <thirdofmay18081814goya> ty for help |
| 2024-09-10 00:09:14 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 00:09:23 +0200 | ski | . o O ( hypothetical judgements, parameterized judgments -- "Judgements as Types correspondence", a la LF (Twelf implementation) ) |
| 2024-09-10 00:10:59 +0200 | <Rembane> | This twelf? https://twelf.org/ |
| 2024-09-10 00:12:06 +0200 | <ski> | yes |
| 2024-09-10 00:12:46 +0200 | <ski> | ("LF" stands for "Logical Framework") |
| 2024-09-10 00:12:58 +0200 | <Rembane> | Thank you! |
| 2024-09-10 00:13:27 +0200 | CiaoSen | (~Jura@2a05:5800:206:9700:ca4b:d6ff:fec1:99da) (Ping timeout: 265 seconds) |
| 2024-09-10 00:13:46 +0200 | <ski> | (Twelf is a dependently typed logic programming language) |
| 2024-09-10 00:15:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 00:15:14 +0200 | <Rembane> | That seems incredibly powerful. Its syntax doesn't look too horrible too! |
| 2024-09-10 00:16:05 +0200 | <ski> | it's for sure an interesting system |
| 2024-09-10 00:16:23 +0200 | <haskellbridge> | <thirdofmay18081814goya> what would be some good use cases? |
| 2024-09-10 00:16:34 +0200 | <haskellbridge> | <thirdofmay18081814goya> type checker for one |
| 2024-09-10 00:18:45 +0200 | <ski> | focus on applications have more been on the side of specifying logical systems, or inference systems relating to programming languages (type systems, operational semantics), and then to prove theorems about these systems. but one can also write programs to compute things, (more or less) in the style of usual logic programming |
| 2024-09-10 00:19:09 +0200 | meygerjos | (~meygerjos@user/meygerjos) |
| 2024-09-10 00:19:43 +0200 | <haskellbridge> | <thirdofmay18081814goya> neat |
| 2024-09-10 00:19:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 00:20:17 +0200 | <ski> | lambdaProlog is a related system, sharing quite a bit of the background. it's not dependently typed, though, and it has (some) more facilities for more traditional programming |
| 2024-09-10 00:20:56 +0200 | <ski> | it's especially nice for doing HOAS (Higher-Order Abstract Syntax) |
| 2024-09-10 00:22:12 +0200 | <meygerjos> | i'm offering lessons in category theory https://meygerjos.com/ - also this is my first time on irc so lmk if i'm doing self-promotion in an inappropriate way |
| 2024-09-10 00:22:25 +0200 | <ski> | the main features of it, over traditional Prolog (and not considering it being statically typed), are (a) lambda terms (with unification); (b0) implication goals; and (b1) universal quantification goals |
| 2024-09-10 00:22:52 +0200 | <haskellbridge> | <thirdofmay18081814goya> ski: lambda terms is all i need |
| 2024-09-10 00:23:05 +0200 | <haskellbridge> | <thirdofmay18081814goya> and "fix" |
| 2024-09-10 00:23:06 +0200 | <ski> | even without (a), (b0) and (b1) can sometimes be quite nice, in logic programming. however, only (a) without (b0) and (b1) tends to be cumbersome |
| 2024-09-10 00:26:13 +0200 | <ski> | (one could also argue that (b1) naturally calls for (a) in cases, and perhaps also that (b0) is less useful without (b1). with (b0) you can introduce local clauses, but to get lexical scoping, hiding a local definition, you also need (b1)) |
| 2024-09-10 00:27:45 +0200 | <ski> | (.. of course, one could always introduce an "ad hoc" construction for lexical scoping of loca definitions .. but it's quite nicer for these to naturally fall out of already traditionally accepted logical connectives) |
| 2024-09-10 00:28:41 +0200 | <ski> | oh .. and Twelf also have these (a),(b0),(b1) |
| 2024-09-10 00:29:38 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 00:29:53 +0200 | Squared | (~Square@user/square) |
| 2024-09-10 00:30:20 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 00:30:41 +0200 | <ski> | thirdofmay18081814goya : however, the lambda terms they have are restricted, can't perform arbitrary computation (but you do get beta- and eta- conversion) in that there is e.g. no `case' construction on sum types. to compute stuff, you use predicates, as in Prolog |
| 2024-09-10 00:30:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 00:31:46 +0200 | <ski> | (Mercury does have general computing functions .. but it doesn't have unification of functions, apart from the trivial cases when one or both sides are unconstrained variables) |
| 2024-09-10 00:33:17 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 00:33:45 +0200 | <ski> | (oh, no `fix' in lambdaProlog,Twelf, either. (well-typed) lambda terms have terminating reduction) |
| 2024-09-10 00:33:58 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 00:35:58 +0200 | Me-me | (~me-me@kc.randomserver.name) (Changing host) |
| 2024-09-10 00:35:58 +0200 | Me-me | (~me-me@user/me-me) |
| 2024-09-10 00:35:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-10 00:36:04 +0200 | tv | (~tv@user/tv) (Ping timeout: 260 seconds) |
| 2024-09-10 00:36:34 +0200 | oo_miguel | (~Thunderbi@78.10.207.45) (Ping timeout: 252 seconds) |
| 2024-09-10 00:37:12 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 00:37:54 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 00:43:17 +0200 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2024-09-10 00:44:15 +0200 | EvanR | (~EvanR@user/evanr) (Quit: Leaving) |
| 2024-09-10 00:46:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 00:48:55 +0200 | gentauro | (~gentauro@user/gentauro) |
| 2024-09-10 00:50:49 +0200 | <haskellbridge> | <thirdofmay18081814goya> i'm definitely looking at logic programming the second i have a chance |
| 2024-09-10 00:50:51 +0200 | <haskellbridge> | <thirdofmay18081814goya> am very curious |
| 2024-09-10 00:51:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 00:51:15 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb21181cd9b506c11910.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-09-10 00:52:33 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 00:53:15 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 00:56:09 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds) |
| 2024-09-10 00:56:13 +0200 | meygerjos | (~meygerjos@user/meygerjos) (Ping timeout: 245 seconds) |
| 2024-09-10 00:59:18 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-10 00:59:58 +0200 | hgolden_ | (~hgolden@static-198-44-129-51.cust.tzulo.com) |
| 2024-09-10 01:02:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 01:02:45 +0200 | hgolden | (~hgolden@169.150.203.10) (Ping timeout: 265 seconds) |
| 2024-09-10 01:03:23 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-09-10 01:03:30 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 01:04:41 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-09-10 01:05:29 +0200 | k_hachig_ | (~k_hachig@2607:fea8:351d:ef0:f026:cab8:26a0:8d01) |
| 2024-09-10 01:06:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 01:13:38 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 01:14:20 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 01:15:40 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-09-10 01:16:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-10 01:17:16 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 01:17:59 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 01:21:14 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 01:21:55 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 01:22:17 +0200 | k_hachig_ | k_hachig |
| 2024-09-10 01:25:27 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-09-10 01:27:39 +0200 | k_hachig | (~k_hachig@2607:fea8:351d:ef0:f026:cab8:26a0:8d01) (Ping timeout: 246 seconds) |
| 2024-09-10 01:33:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 01:36:28 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 01:37:10 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 01:39:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-10 01:40:51 +0200 | pavonia | (~user@user/siracusa) |
| 2024-09-10 01:43:59 +0200 | hgolden__ | (~hgolden@23.162.40.28) |
| 2024-09-10 01:44:31 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Ping timeout: 264 seconds) |
| 2024-09-10 01:46:12 +0200 | hgolden_ | (~hgolden@static-198-44-129-51.cust.tzulo.com) (Ping timeout: 246 seconds) |
| 2024-09-10 01:49:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 01:50:30 +0200 | EvanR | (~EvanR@user/evanr) |
| 2024-09-10 01:50:38 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 01:52:05 +0200 | <haskellbridge> | <thirdofmay18081814goya> huh, lean4 typeclass resolution is the result of logic programming research |
| 2024-09-10 01:53:14 +0200 | <geekosaur> | I could see that, yes |
| 2024-09-10 01:53:17 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 2024-09-10 01:54:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 01:55:55 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2024-09-10 01:57:33 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 01:58:01 +0200 | <geekosaur> | I'm pretty sure I could describe GHC's constraint resolution (and certain I could describe standard Haskell's typeclass resolution) in Prolog, but the state of the art in logic programming has changed a bit since the last time I did anything with Prolog |
| 2024-09-10 01:58:15 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 02:01:10 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 02:01:51 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 02:03:48 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-09-10 02:03:50 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Remote host closed the connection) |
| 2024-09-10 02:04:13 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 02:05:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 02:05:13 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 02:05:55 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 02:12:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-10 02:13:11 +0200 | pavonia_ | (~user@user/siracusa) |
| 2024-09-10 02:13:21 +0200 | pavonia | (~user@user/siracusa) (Ping timeout: 252 seconds) |
| 2024-09-10 02:13:47 +0200 | pavonia_ | pavonia |
| 2024-09-10 02:20:54 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 02:21:34 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 02:22:39 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) |
| 2024-09-10 02:22:48 +0200 | k_hachig_ | (~k_hachig@2607:fea8:351d:ef0:f026:cab8:26a0:8d01) |
| 2024-09-10 02:23:16 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) (Changing host) |
| 2024-09-10 02:23:16 +0200 | vincent42 | (uid574193@user/vincent42) |
| 2024-09-10 02:23:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 02:24:34 +0200 | xff0x | (~xff0x@2405:6580:b080:900:979f:5e3e:76e8:a33b) (Ping timeout: 260 seconds) |
| 2024-09-10 02:27:01 +0200 | k_hachig_ | (~k_hachig@2607:fea8:351d:ef0:f026:cab8:26a0:8d01) (Ping timeout: 248 seconds) |
| 2024-09-10 02:28:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-10 02:33:40 +0200 | califax_ | (~califax@user/califx) |
| 2024-09-10 02:33:51 +0200 | califax | (~califax@user/califx) (Ping timeout: 260 seconds) |
| 2024-09-10 02:34:16 +0200 | hgolden__ | (~hgolden@23.162.40.28) (Read error: Connection reset by peer) |
| 2024-09-10 02:34:59 +0200 | califax_ | califax |
| 2024-09-10 02:36:04 +0200 | k_hachig_ | (~k_hachig@2607:fea8:351d:ef0:f026:cab8:26a0:8d01) |
| 2024-09-10 02:36:15 +0200 | k_hachig_ | k_hachig |
| 2024-09-10 02:39:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 02:40:49 +0200 | hook54321 | (sid149355@user/hook54321) (Ping timeout: 245 seconds) |
| 2024-09-10 02:40:49 +0200 | systemfault | (sid267009@about/typescript/member/systemfault) (Ping timeout: 245 seconds) |
| 2024-09-10 02:41:38 +0200 | SethTisue | (sid14912@id-14912.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-09-10 02:41:51 +0200 | systemfault | (sid267009@about/typescript/member/systemfault) |
| 2024-09-10 02:41:59 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 02:42:41 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 02:44:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 02:44:09 +0200 | tapas | (sid467876@id-467876.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-09-10 02:44:09 +0200 | spew | (~spew@201.141.99.170) (Ping timeout: 252 seconds) |
| 2024-09-10 02:44:48 +0200 | SethTisue | (sid14912@id-14912.ilkley.irccloud.com) |
| 2024-09-10 02:45:36 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 02:46:18 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 02:46:53 +0200 | hook54321 | (sid149355@user/hook54321) |
| 2024-09-10 02:47:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-09-10 02:47:22 +0200 | tapas | (sid467876@id-467876.ilkley.irccloud.com) |
| 2024-09-10 02:49:31 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 02:50:13 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 02:52:52 +0200 | spew | (~spew@201.141.99.170) |
| 2024-09-10 02:55:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 03:00:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-10 03:01:24 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 276 seconds) |
| 2024-09-10 03:04:54 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 03:05:35 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 03:11:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 03:12:57 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) |
| 2024-09-10 03:16:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 03:16:29 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-10 03:18:20 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-09-10 03:23:02 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Client Quit) |
| 2024-09-10 03:24:09 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-09-10 03:25:59 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 03:26:39 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 03:26:44 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Client Quit) |
| 2024-09-10 03:26:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 03:28:45 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 246 seconds) |
| 2024-09-10 03:29:35 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 03:30:17 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 03:31:07 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2024-09-10 03:31:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 03:33:33 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 03:34:14 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 03:38:43 +0200 | tv | (~tv@user/tv) |
| 2024-09-10 03:41:00 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-10 03:42:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 03:43:52 +0200 | hgolden | (~hgolden@static-198-44-129-115.cust.tzulo.com) |
| 2024-09-10 03:47:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 03:47:44 +0200 | Square | (~Square@user/square) |
| 2024-09-10 03:47:49 +0200 | Square | (~Square@user/square) (Remote host closed the connection) |
| 2024-09-10 03:48:59 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Remote host closed the connection) |
| 2024-09-10 03:49:40 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) |
| 2024-09-10 03:54:53 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (K-Lined) |
| 2024-09-10 03:56:58 +0200 | troojg | (~troojg@user/troojg) |
| 2024-09-10 03:58:23 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 04:03:26 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-10 04:03:35 +0200 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-09-10 04:03:54 +0200 | petrichor | (~znc-user@user/petrichor) |
| 2024-09-10 04:08:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 04:11:35 +0200 | Square | (~Square@user/square) |
| 2024-09-10 04:11:35 +0200 | Square | (~Square@user/square) (Remote host closed the connection) |
| 2024-09-10 04:11:57 +0200 | Square | (~Square@user/square) |
| 2024-09-10 04:12:47 +0200 | sp1ff | (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
| 2024-09-10 04:12:53 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 252 seconds) |
| 2024-09-10 04:14:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-10 04:14:24 +0200 | Axma10625 | (~Axman6@user/axman6) |
| 2024-09-10 04:16:28 +0200 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 246 seconds) |
| 2024-09-10 04:21:57 +0200 | Square | (~Square@user/square) (Ping timeout: 246 seconds) |
| 2024-09-10 04:24:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 04:26:09 +0200 | hgolden_ | (~hgolden@23.162.40.69) |
| 2024-09-10 04:28:40 +0200 | hgolden | (~hgolden@static-198-44-129-115.cust.tzulo.com) (Ping timeout: 252 seconds) |
| 2024-09-10 04:29:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 04:31:09 +0200 | hgolden_ | (~hgolden@23.162.40.69) (Ping timeout: 260 seconds) |
| 2024-09-10 04:31:25 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
| 2024-09-10 04:31:53 +0200 | Axma10625 | Axman6 |
| 2024-09-10 04:32:09 +0200 | vincent42 | (uid574193@user/vincent42) (Quit: Connection closed for inactivity) |
| 2024-09-10 04:33:26 +0200 | hgolden_ | (~hgolden@169.150.203.36) |
| 2024-09-10 04:35:40 +0200 | hgolden_ | (~hgolden@169.150.203.36) (Remote host closed the connection) |
| 2024-09-10 04:36:09 +0200 | hgolden_ | (~hgolden@169.150.203.36) |
| 2024-09-10 04:37:08 +0200 | hgolden_ | (~hgolden@169.150.203.36) (Remote host closed the connection) |
| 2024-09-10 04:37:33 +0200 | hgolden_ | (~hgolden@169.150.203.36) |
| 2024-09-10 04:40:26 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 04:42:13 +0200 | terrorjack4 | (~terrorjac@2a01:4f8:c17:dc9f::) (Quit: The Lounge - https://thelounge.chat) |
| 2024-09-10 04:42:57 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-09-10 04:43:46 +0200 | terrorjack4 | (~terrorjac@2a01:4f8:c17:dc9f::) |
| 2024-09-10 04:45:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 04:47:19 +0200 | john2 | (~john@2406:5a00:241a:5600:f0eb:f825:2ac6:1387) (Read error: Connection reset by peer) |
| 2024-09-10 04:48:08 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-09-10 04:48:18 +0200 | sa1 | (sid7690@id-7690.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-09-10 04:48:22 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-09-10 04:48:23 +0200 | john2 | (~john@2406:5a00:241a:5600:31b8:c267:49dc:2202) |
| 2024-09-10 04:48:26 +0200 | td_ | (~td@i5387092B.versanet.de) (Ping timeout: 255 seconds) |
| 2024-09-10 04:50:24 +0200 | td_ | (~td@i5387093D.versanet.de) |
| 2024-09-10 04:52:58 +0200 | sa1 | (sid7690@id-7690.ilkley.irccloud.com) |
| 2024-09-10 04:55:51 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: zzz) |
| 2024-09-10 04:56:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 04:57:59 +0200 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-09-10 05:01:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 05:12:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 05:17:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 05:25:01 +0200 | arahael_ | (~arahael@user/arahael) |
| 2024-09-10 05:27:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 05:30:10 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2024-09-10 05:30:33 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2024-09-10 05:31:35 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2024-09-10 05:32:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 05:42:28 +0200 | idnar | (sid12240@debian/mithrandi) (Ping timeout: 245 seconds) |
| 2024-09-10 05:43:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 05:46:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's the difference between the sld inference rule and the general resolution inference rule? |
| 2024-09-10 05:46:38 +0200 | idnar | (sid12240@debian/mithrandi) |
| 2024-09-10 05:48:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 05:51:24 +0200 | aforemny_ | (~aforemny@2001:9e8:6cc0:b200:2811:dbcb:ebeb:5aed) |
| 2024-09-10 05:51:54 +0200 | aforemny | (~aforemny@2001:9e8:6ce5:1500:20e4:f28d:e540:f289) (Ping timeout: 246 seconds) |
| 2024-09-10 05:53:43 +0200 | <jle`> | there's still no way to uncons a type-level Symbol? |
| 2024-09-10 05:53:58 +0200 | <jle`> | besides using that library what does the hacky CmpNat usage |
| 2024-09-10 05:59:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 06:01:20 +0200 | Squared | (~Square@user/square) (Ping timeout: 255 seconds) |
| 2024-09-10 06:04:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 06:04:36 +0200 | <Axman6> | There definitely is, let me see if I can find it |
| 2024-09-10 06:06:35 +0200 | <Axman6> | https://github.com/raehik/symparsec is built on top of https://hackage.haskell.org/package/base-4.16.1.0/docs/GHC-TypeLits.html#t:UnconsSymbol IIRC |
| 2024-09-10 06:07:50 +0200 | <jle`> | whoa :O |
| 2024-09-10 06:08:02 +0200 | <jle`> | i was staring at the docs for a while and didn't see UnconsSymbol |
| 2024-09-10 06:08:31 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-09-10 06:09:30 +0200 | <jle`> | thanks! |
| 2024-09-10 06:09:35 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-09-10 06:14:51 +0200 | <haskellbridge> | <thirdofmay18081814goya> geekosaur: if you have time at some point, would you mind giving me a general idea of how you would do this? just informally |
| 2024-09-10 06:15:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 06:19:13 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) |
| 2024-09-10 06:20:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 06:20:32 +0200 | <Axman6> | I've been resisting the urge to use symparsec as a way to define configuration for IP in Clash for a while now. Trying to define everything in the type system is kinda painful (though there are libraries that make it a little nicer) |
| 2024-09-10 06:20:57 +0200 | caconym | (~caconym@user/caconym) |
| 2024-09-10 06:23:18 +0200 | arahael_ | (~arahael@user/arahael) (Read error: Connection reset by peer) |
| 2024-09-10 06:24:19 +0200 | <jle`> | i'm trying to update my type level printf library after almost 5 years |
| 2024-09-10 06:24:31 +0200 | <Axman6> | <3 |
| 2024-09-10 06:24:47 +0200 | <jle`> | i was using the symbols library which basically checked against every Ascii character to see if it was the first character or not |
| 2024-09-10 06:24:48 +0200 | <geekosaur> | thirdofmay, I'm heading to bed. But typeclasses in Haskell can be thought of as having two components: an operational one involving passing dictionaries of functions around, and a type resolution one involving solving constraints. This amounts to asserting types and typeclass instances thereof, and then asking for a solution to a proposition constructed from typeclass constraints. |
| 2024-09-10 06:25:01 +0200 | <Axman6> | I wonder how hard it would be to support printf's %n$ syntax at the type level... |
| 2024-09-10 06:25:01 +0200 | <jle`> | and it was slow as doodoo |
| 2024-09-10 06:25:21 +0200 | caconym | (~caconym@user/caconym) (Client Quit) |
| 2024-09-10 06:25:35 +0200 | <jle`> | Axman6: that's what https://hackage.haskell.org/package/typelits-printf was supposed to do |
| 2024-09-10 06:25:37 +0200 | <jle`> | but it was super slow |
| 2024-09-10 06:25:43 +0200 | caconym | (~caconym@user/caconym) |
| 2024-09-10 06:25:43 +0200 | <Axman6> | Was that Csongor Kiss' library? |
| 2024-09-10 06:25:45 +0200 | <jle`> | but i wonder if i use symparsec it'd be usable |
| 2024-09-10 06:25:47 +0200 | <geekosaur> | I can't quite think clearly enough right now to dust off my Prolog from the 1990s and try to construct it right now. |
| 2024-09-10 06:25:58 +0200 | <jle`> | yeah it used kiss's library under the hood |
| 2024-09-10 06:26:27 +0200 | <jle`> | i tried using it myself for a while but the compile times were pretty infeasible |
| 2024-09-10 06:26:40 +0200 | <Axman6> | I remember the... ICFP? talk on that, I came away from it with very mixed feelings |
| 2024-09-10 06:27:03 +0200 | <jle`> | it was definitely a thing that existed, befure UnconsSymbol :) |
| 2024-09-10 06:27:17 +0200 | <Axman6> | Like, it was brilliant, but it was a brilliant solution to a problem that should be solved elsewhere (hence UnconsSymbol I guess) |
| 2024-09-10 06:27:44 +0200 | <jle`> | functionality wise the printf i built on top of it worked and i was happy with it, except for it added like 30 seconds per printf at compiletime |
| 2024-09-10 06:28:18 +0200 | <Axman6> | "You can use this library, but only once. Choose wisely" |
| 2024-09-10 06:29:41 +0200 | <Axman6> | Would it be difficult to make things extensible so users can add their own FormatTypes? ... is that already possible? |
| 2024-09-10 06:30:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 06:31:03 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-09-10 06:31:20 +0200 | <jle`> | i forgot how i did it haha we'll see once i properly dust it off |
| 2024-09-10 06:34:12 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-09-10 06:35:38 +0200 | <Axman6> | We have a C++ library at work which wraps cpprintf (iirc) and adds a %@ formatter for things which aren't supported and calls some toString'ish method |
| 2024-09-10 06:35:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 06:36:55 +0200 | <Axman6> | I'd love to see an instance for Show a => FormatType "@" a (or whatever character the bikeshed should be coloured with) |
| 2024-09-10 06:37:44 +0200 | hgolden_ | (~hgolden@169.150.203.36) (Ping timeout: 260 seconds) |
| 2024-09-10 06:37:58 +0200 | <Axman6> | I'm sure there's good reasons why that can't be done though |
| 2024-09-10 06:38:24 +0200 | michalz | (~michalz@185.246.207.215) |
| 2024-09-10 06:39:33 +0200 | aforemny_ | (~aforemny@2001:9e8:6cc0:b200:2811:dbcb:ebeb:5aed) (Ping timeout: 245 seconds) |
| 2024-09-10 06:39:44 +0200 | Square2 | (~Square4@user/square) |
| 2024-09-10 06:41:59 +0200 | jove | (~AdminUser@82-69-8-157.dsl.in-addr.zen.co.uk) |
| 2024-09-10 06:44:18 +0200 | <jle`> | i think you can add them but they're going to be orphan instances |
| 2024-09-10 06:44:34 +0200 | <jle`> | so not really great unless it's for an end application |
| 2024-09-10 06:44:49 +0200 | <jle`> | oh you mean a generic "Show" |
| 2024-09-10 06:45:24 +0200 | <jle`> | yeah i'm not sure if that head will overlap with everything else |
| 2024-09-10 06:45:51 +0200 | <jle`> | but it sounds useful |
| 2024-09-10 06:46:00 +0200 | jove | (~AdminUser@82-69-8-157.dsl.in-addr.zen.co.uk) (Changing host) |
| 2024-09-10 06:46:00 +0200 | jove | (~AdminUser@user/jove) |
| 2024-09-10 06:46:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 06:47:44 +0200 | <jle`> | yeah it looks like you're supposed to be able to add FormatType for your own custom types, but having it work with all Showable's might cause problems with overlapping instances |
| 2024-09-10 06:47:48 +0200 | <jle`> | i can investigate further |
| 2024-09-10 06:51:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 06:52:22 +0200 | jove | (~AdminUser@user/jove) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-09-10 06:52:29 +0200 | <Axman6> | yeah I was half expecting to see a fundep or something but it doesn't really make sense in either direction. Is there a nice way to say that there will only be one instance of a class where one of the parameters is a concrete type? |
| 2024-09-10 06:52:59 +0200 | jove | (~quassel@user/jove) |
| 2024-09-10 07:02:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 07:07:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-10 07:12:49 +0200 | hgolden | (~hgolden@syn-172-251-233-141.res.spectrum.com) |
| 2024-09-10 07:13:20 +0200 | <jle`> | yeah this kind of stuff i'm always just guessing and checking heh |
| 2024-09-10 07:15:38 +0200 | hgolden_ | (~hgolden@146.70.173.229) |
| 2024-09-10 07:16:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-10 07:18:13 +0200 | hgolden | (~hgolden@syn-172-251-233-141.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2024-09-10 07:18:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 07:19:46 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 272 seconds) |
| 2024-09-10 07:23:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 07:25:08 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-09-10 07:27:29 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-09-10 07:30:02 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-09-10 07:30:51 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb1871be317632822bda.dip0.t-ipconnect.de) |
| 2024-09-10 07:31:24 +0200 | euleritian | (~euleritia@dynamic-176-002-134-239.176.2.pool.telefonica.de) |
| 2024-09-10 07:34:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 07:34:51 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-09-10 07:36:54 +0200 | kuribas | (~user@ptr-17d51epau2xs89jopnb.18120a2.ip6.access.telenet.be) (Ping timeout: 246 seconds) |
| 2024-09-10 07:39:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-10 07:46:18 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) |
| 2024-09-10 07:47:59 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 07:49:16 +0200 | hiecaq` | (~hiecaq@user/hiecaq) |
| 2024-09-10 07:49:20 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Ping timeout: 255 seconds) |
| 2024-09-10 07:49:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 07:51:24 +0200 | harveypwca | (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) |
| 2024-09-10 07:54:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-10 07:56:55 +0200 | euleritian | (~euleritia@dynamic-176-002-134-239.176.2.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2024-09-10 07:58:30 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 07:59:53 +0200 | oo_miguel | (~Thunderbi@78.10.207.45) |
| 2024-09-10 08:01:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 08:04:29 +0200 | euleritian | (~euleritia@dynamic-176-002-139-084.176.2.pool.telefonica.de) |
| 2024-09-10 08:06:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 08:08:40 +0200 | euleritian | (~euleritia@dynamic-176-002-139-084.176.2.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2024-09-10 08:08:40 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-10 08:09:56 +0200 | euleritian | (~euleritia@dynamic-176-007-163-183.176.7.pool.telefonica.de) |
| 2024-09-10 08:12:42 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-09-10 08:17:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 08:22:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 08:26:01 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2024-09-10 08:26:31 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-10 08:33:02 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 08:33:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 08:34:39 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) (Ping timeout: 246 seconds) |
| 2024-09-10 08:35:54 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-10 08:37:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 08:38:17 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) |
| 2024-09-10 08:40:46 +0200 | harveypwca | (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) (Quit: Leaving) |
| 2024-09-10 08:47:10 +0200 | euleritian | (~euleritia@dynamic-176-007-163-183.176.7.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2024-09-10 08:48:25 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-10 08:48:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 08:53:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 08:55:10 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-09-10 08:57:09 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-09-10 09:00:01 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-09-10 09:00:40 +0200 | caconym | (~caconym@user/caconym) |
| 2024-09-10 09:02:16 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) (Quit: ash3en) |
| 2024-09-10 09:04:16 +0200 | k_hachig | (~k_hachig@2607:fea8:351d:ef0:f026:cab8:26a0:8d01) (Ping timeout: 272 seconds) |
| 2024-09-10 09:04:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 09:05:30 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) |
| 2024-09-10 09:05:53 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) (Changing host) |
| 2024-09-10 09:05:53 +0200 | vincent42 | (uid574193@user/vincent42) |
| 2024-09-10 09:06:39 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 09:09:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 09:15:59 +0200 | hololeap | (~quassel@user/hololeap) (Ping timeout: 260 seconds) |
| 2024-09-10 09:16:05 +0200 | markasoftware_ | (~quassel@107.161.26.124) (Ping timeout: 248 seconds) |
| 2024-09-10 09:20:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 09:23:24 +0200 | <[exa]> | mornin' all |
| 2024-09-10 09:24:10 +0200 | <[exa]> | is there some kind of "streaming" version of aeson "decode" which could handle the (potentially infinite) json object streams? Such as the ones that are used for batch processing with elasticsearch. |
| 2024-09-10 09:24:42 +0200 | <[exa]> | (example: `{"a":"b"} {"c":"d"}` decodes to some kind of streamy list of 2 objects) |
| 2024-09-10 09:25:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 09:25:35 +0200 | hololeap | (~quassel@user/hololeap) |
| 2024-09-10 09:27:41 +0200 | markasoftware | (~quassel@107.161.26.124) |
| 2024-09-10 09:31:00 +0200 | <[exa]> | ah ok Data.Aeson.Extra.Stream has something that I could probably remix into usable form |
| 2024-09-10 09:36:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 09:37:50 +0200 | akegalj | (~akegalj@89-164-127-178.dsl.iskon.hr) |
| 2024-09-10 09:39:27 +0200 | markasoftware | (~quassel@107.161.26.124) (Quit: No Ping reply in 180 seconds.) |
| 2024-09-10 09:40:56 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-10 09:41:13 +0200 | hololeap | (~quassel@user/hololeap) (Quit: No Ping reply in 180 seconds.) |
| 2024-09-10 09:41:41 +0200 | markasoftware | (~quassel@107.161.26.124) |
| 2024-09-10 09:42:38 +0200 | hololeap | (~quassel@user/hololeap) |
| 2024-09-10 09:43:22 +0200 | <jackdk> | I used https://hackage.haskell.org/package/aeson-2.2.1.0/docs/Data-Aeson-Decoding-Tokens.html once when I really needed to care about the order of fields and such |
| 2024-09-10 09:50:59 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-09-10 09:51:42 +0200 | chele | (~chele@user/chele) |
| 2024-09-10 09:51:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 09:53:42 +0200 | <[exa]> | jackdk: yeah that seems to be the way; the Data.Aeson.Extra.Stream kinda assumes it will be a finite array |
| 2024-09-10 09:54:58 +0200 | <[exa]> | is there a way to attoparsecly feed the aeson tokenizer with more stuff to parse? (like, `ByteString -> (Tokens, ByteString)`) Or am I just not seeing it in the docs? :D |
| 2024-09-10 09:55:44 +0200 | CiaoSen | (~Jura@2a05:5800:45a:da00:ca4b:d6ff:fec1:99da) |
| 2024-09-10 09:56:28 +0200 | <[exa]> | looks like the `k` type would be the leftover here https://hackage.haskell.org/package/aeson-2.2.1.0/docs/Data-Aeson-Decoding.html#v:toEitherValue ..but how.? |
| 2024-09-10 09:57:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-10 09:57:30 +0200 | <[exa]> | ah yes and bsToTokens returns precisely this with bytestring as a leftover, good, I see |
| 2024-09-10 09:57:32 +0200 | <[exa]> | thanks! |
| 2024-09-10 10:02:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 10:03:52 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-10 10:07:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-10 10:09:33 +0200 | yosef` | (~yosef`@user/yosef/x-2947716) |
| 2024-09-10 10:10:58 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-09-10 10:13:47 +0200 | dextaa | (~DV@user/dextaa) |
| 2024-09-10 10:15:09 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) |
| 2024-09-10 10:18:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 10:19:23 +0200 | yosef` | (~yosef`@user/yosef/x-2947716) (Remote host closed the connection) |
| 2024-09-10 10:19:34 +0200 | yosef` | (~yosef`@user/yosef/x-2947716) |
| 2024-09-10 10:23:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 10:23:19 +0200 | yosef` | (~yosef`@user/yosef/x-2947716) (Remote host closed the connection) |
| 2024-09-10 10:26:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 10:28:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Read error: Connection reset by peer) |
| 2024-09-10 10:43:20 +0200 | Noir | (~Noir@37.17.4.91) |
| 2024-09-10 10:43:31 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-09-10 10:45:20 +0200 | Noir | (~Noir@37.17.4.91) (Killed (ozone (No Spam))) |
| 2024-09-10 10:51:02 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-09-10 10:52:31 +0200 | arahael_ | (~arahael@user/arahael) |
| 2024-09-10 10:52:56 +0200 | arahael | (~arahael@user/arahael) (Quit: leaving) |
| 2024-09-10 10:53:56 +0200 | arahael_ | arahael |
| 2024-09-10 10:58:07 +0200 | ubert | (~Thunderbi@77.119.170.88.wireless.dyn.drei.com) |
| 2024-09-10 11:01:51 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-10 11:04:45 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 2024-09-10 11:08:40 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-10 11:10:24 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-09-10 11:11:30 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-09-10 11:14:50 +0200 | vincent42 | (uid574193@user/vincent42) (Quit: Connection closed for inactivity) |
| 2024-09-10 11:21:32 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-09-10 11:23:55 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 11:24:40 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 11:52:45 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 11:53:49 +0200 | misterfish | (~misterfis@87.215.131.102) |
| 2024-09-10 11:58:26 +0200 | CiaoSen | (~Jura@2a05:5800:45a:da00:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 2024-09-10 12:00:12 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-09-10 12:05:23 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 245 seconds) |
| 2024-09-10 12:07:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 12:11:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-10 12:16:08 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) |
| 2024-09-10 12:20:48 +0200 | p3n | (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-09-10 12:22:22 +0200 | p3n | (~p3n@217.198.124.246) |
| 2024-09-10 12:22:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 12:22:46 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-09-10 12:25:46 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 12:26:03 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 252 seconds) |
| 2024-09-10 12:26:44 +0200 | m5zs7k | (aquares@web10.mydevil.net) (Quit: m5zs7k) |
| 2024-09-10 12:27:08 +0200 | m5zs7k | (aquares@web10.mydevil.net) |
| 2024-09-10 12:27:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-10 12:31:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 12:34:15 +0200 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2024-09-10 12:34:32 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2024-09-10 12:35:35 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-09-10 12:36:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 12:37:26 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Quit: Leaving) |
| 2024-09-10 12:41:33 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-10 12:43:54 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Client Quit) |
| 2024-09-10 12:47:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 12:51:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 12:52:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 12:56:47 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 12:57:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-10 12:58:30 +0200 | <haskellbridge> | <mauke> [exa]: https://hackage.haskell.org/package/json-stream-0.4.5.3/docs/Data-JsonStream-Parser.html |
| 2024-09-10 13:00:05 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-09-10 13:00:44 +0200 | <haskellbridge> | <mauke> Wait, this is IRC. Just https://hackage.haskell.org/package/json-stream-0.4.5.3/docs/Data-JsonStream-Parser.html then; no replies |
| 2024-09-10 13:02:10 +0200 | gustavn | (~gustavn@user/gustavn) |
| 2024-09-10 13:02:21 +0200 | gustavn | (~gustavn@user/gustavn) () |
| 2024-09-10 13:04:27 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-10 13:04:28 +0200 | john2 | (~john@2406:5a00:241a:5600:31b8:c267:49dc:2202) (Read error: Connection reset by peer) |
| 2024-09-10 13:06:04 +0200 | john2 | (~john@2406:5a00:241a:5600:31b8:c267:49dc:2202) |
| 2024-09-10 13:08:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 13:13:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-10 13:17:47 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-10 13:17:50 +0200 | CiaoSen | (~Jura@2a05:5800:45a:da00:ca4b:d6ff:fec1:99da) |
| 2024-09-10 13:19:00 +0200 | benjaminl | (~benjaminl@user/benjaminl) |
| 2024-09-10 13:19:54 +0200 | benjaminl_ | (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) (Ping timeout: 246 seconds) |
| 2024-09-10 13:22:20 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 13:24:23 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 13:24:56 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 13:29:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 13:31:52 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-10 13:32:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 13:33:08 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-09-10 13:37:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 13:41:35 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 252 seconds) |
| 2024-09-10 13:42:45 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-10 13:45:54 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) |
| 2024-09-10 13:48:33 +0200 | srazkvt | (~sarah@user/srazkvt) (Ping timeout: 244 seconds) |
| 2024-09-10 13:48:37 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2024-09-10 13:54:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 13:55:54 +0200 | euleritian | (~euleritia@dynamic-176-006-144-128.176.6.pool.telefonica.de) |
| 2024-09-10 13:56:21 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 2024-09-10 13:57:30 +0200 | tomboy65 | (~tomboy64@user/tomboy64) (Ping timeout: 272 seconds) |
| 2024-09-10 13:59:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 14:00:26 +0200 | wei2912 | (~wei2912@116.88.52.77) |
| 2024-09-10 14:00:32 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) |
| 2024-09-10 14:00:46 +0200 | vincent42 | (uid574193@id-574193.hampstead.irccloud.com) (Changing host) |
| 2024-09-10 14:00:46 +0200 | vincent42 | (uid574193@user/vincent42) |
| 2024-09-10 14:00:54 +0200 | wei2912 | (~wei2912@116.88.52.77) (Client Quit) |
| 2024-09-10 14:01:09 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) (Read error: Connection reset by peer) |
| 2024-09-10 14:01:28 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) |
| 2024-09-10 14:01:47 +0200 | <vincent42> | > take 2 [1..] |
| 2024-09-10 14:01:49 +0200 | <lambdabot> | [1,2] |
| 2024-09-10 14:01:53 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-09-10 14:05:11 +0200 | <vincent42> | @hoogle [a] -> [a] |
| 2024-09-10 14:05:12 +0200 | <lambdabot> | Prelude tail :: [a] -> [a] |
| 2024-09-10 14:05:12 +0200 | <lambdabot> | Prelude init :: [a] -> [a] |
| 2024-09-10 14:05:12 +0200 | <lambdabot> | Prelude reverse :: [a] -> [a] |
| 2024-09-10 14:06:11 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) |
| 2024-09-10 14:08:19 +0200 | xff0x | (~xff0x@2405:6580:b080:900:6b3:40cb:7f8c:5b02) |
| 2024-09-10 14:09:25 +0200 | ubert | (~Thunderbi@77.119.170.88.wireless.dyn.drei.com) (Ping timeout: 248 seconds) |
| 2024-09-10 14:10:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 14:10:57 +0200 | tomboy64 | (~tomboy64@user/tomboy64) |
| 2024-09-10 14:14:16 +0200 | youthlic | (~Thunderbi@user/youthlic) |
| 2024-09-10 14:14:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 14:17:57 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-09-10 14:23:05 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 14:25:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 14:26:57 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 14:28:56 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) (Quit: ash3en) |
| 2024-09-10 14:38:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 14:49:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 14:51:33 +0200 | euleritian | (~euleritia@dynamic-176-006-144-128.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-10 14:51:51 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-10 14:54:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-10 14:58:56 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-10 15:04:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 15:09:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 15:13:59 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-10f7-8253-2258-2ec1.rev.sfr.net) |
| 2024-09-10 15:17:09 +0200 | hgolden__ | (~hgolden@146.70.173.165) |
| 2024-09-10 15:18:58 +0200 | <fr33domlover> | o/ Is there a function :: Double -> Maybe Float? |
| 2024-09-10 15:19:17 +0200 | <fr33domlover> | I see there's realToFrac but it doesn't check bounds |
| 2024-09-10 15:19:35 +0200 | <geekosaur> | I don't think so, and given how IEEE works there are questions as to how viable it would be |
| 2024-09-10 15:19:50 +0200 | hgolden_ | (~hgolden@146.70.173.229) (Ping timeout: 272 seconds) |
| 2024-09-10 15:20:18 +0200 | <geekosaur> | checking range of integrals is easy, Double -> Float also requires you to check loss of precision, but that's almost guaranteed |
| 2024-09-10 15:20:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 15:23:26 +0200 | <haskellbridge> | <mauke> . |
| 2024-09-10 15:23:26 +0200 | <haskellbridge> | :t \x -> let y = realToFrac x in if realToFrac y == x then Just y else Nothing |
| 2024-09-10 15:23:27 +0200 | <lambdabot> | (Real a1, Real a2, Fractional a2, Fractional a1) => a1 -> Maybe a2 |
| 2024-09-10 15:25:12 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-10f7-8253-2258-2ec1.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-10 15:25:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-10 15:26:23 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-0d31-59bb-894f-1b3a.rev.sfr.net) |
| 2024-09-10 15:27:38 +0200 | hgolden_ | (~hgolden@169.150.203.36) |
| 2024-09-10 15:29:49 +0200 | hgolden__ | (~hgolden@146.70.173.165) (Ping timeout: 244 seconds) |
| 2024-09-10 15:29:55 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-0d31-59bb-894f-1b3a.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-10 15:32:42 +0200 | fsbot` | (~user@2a01cb0403294f003a9b42233b797197.ipv6.abo.wanadoo.fr) |
| 2024-09-10 15:32:50 +0200 | <geekosaur> | right, but that's usually going to fail because of loss of precision vs. wacky base-2 mantissas |
| 2024-09-10 15:34:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 15:35:44 +0200 | fsbot` | (~user@2a01cb0403294f003a9b42233b797197.ipv6.abo.wanadoo.fr) (Client Quit) |
| 2024-09-10 15:36:22 +0200 | fsbot` | (~user@2a01cb0403294f003a9b42233b797197.ipv6.abo.wanadoo.fr) |
| 2024-09-10 15:37:47 +0200 | ubert | (~Thunderbi@178.165.190.245.wireless.dyn.drei.com) |
| 2024-09-10 15:39:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-10 15:43:06 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2024-09-10 15:43:32 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-09-10 15:49:03 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2024-09-10 15:50:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 15:52:57 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2024-09-10 15:54:27 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 15:55:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-10 15:56:38 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 245 seconds) |
| 2024-09-10 16:00:49 +0200 | CiaoSen | (~Jura@2a05:5800:45a:da00:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 2024-09-10 16:01:47 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) |
| 2024-09-10 16:04:23 +0200 | platao | (~mirc-rc@177.100.68.254) |
| 2024-09-10 16:04:36 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-09-10 16:05:44 +0200 | ubert1 | (~Thunderbi@178.115.52.77.wireless.dyn.drei.com) |
| 2024-09-10 16:05:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 16:07:13 +0200 | st_aldini | (~Thunderbi@136.48.22.91) |
| 2024-09-10 16:07:42 +0200 | talukara | (~talukara@user/talukara) |
| 2024-09-10 16:07:58 +0200 | ubert | (~Thunderbi@178.165.190.245.wireless.dyn.drei.com) (Ping timeout: 272 seconds) |
| 2024-09-10 16:07:58 +0200 | ubert1 | ubert |
| 2024-09-10 16:09:50 +0200 | fsbot` | (~user@2a01cb0403294f003a9b42233b797197.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 2024-09-10 16:10:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 16:14:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 16:15:19 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 16:17:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> any community where i could ask logic programming questions |
| 2024-09-10 16:17:10 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 260 seconds) |
| 2024-09-10 16:17:33 +0200 | <Franciman> | hi yes |
| 2024-09-10 16:17:38 +0200 | <Franciman> | #prolog and #scryer come to mind |
| 2024-09-10 16:17:46 +0200 | <Franciman> | #scryer is more like #ghc |
| 2024-09-10 16:17:48 +0200 | <haskellbridge> | <thirdofmay18081814goya> nice ty! |
| 2024-09-10 16:18:50 +0200 | <geekosaur> | hm, do mercury and curry have online communities somewhere? (well, I'm sure they do, but where?) |
| 2024-09-10 16:19:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 16:19:50 +0200 | user4561 | (~user4561@190.16.167.62) |
| 2024-09-10 16:19:50 +0200 | <ski> | it's ##prolog |
| 2024-09-10 16:20:13 +0200 | vincent42 | (uid574193@user/vincent42) (Quit: Connection closed for inactivity) |
| 2024-09-10 16:25:46 +0200 | user89 | (~user4561@190.16.167.62) |
| 2024-09-10 16:26:23 +0200 | EvanR | (~EvanR@user/evanr) (Quit: Leaving) |
| 2024-09-10 16:29:03 +0200 | user4561 | (~user4561@190.16.167.62) (Ping timeout: 256 seconds) |
| 2024-09-10 16:30:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 16:31:22 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 16:39:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-10 16:42:21 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Ping timeout: 252 seconds) |
| 2024-09-10 16:44:55 +0200 | user89 | (~user4561@190.16.167.62) (Ping timeout: 256 seconds) |
| 2024-09-10 16:45:35 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) |
| 2024-09-10 16:47:09 +0200 | EvanR | (~EvanR@user/evanr) |
| 2024-09-10 16:48:53 +0200 | turlando | (~turlando@user/turlando) (Ping timeout: 248 seconds) |
| 2024-09-10 16:52:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 16:55:55 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-09-10 16:56:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 16:57:09 +0200 | Guest5257 | (~Guest52@d108-172-198-192.bchsia.telus.net) |
| 2024-09-10 17:00:46 +0200 | user4561 | (~user4561@190.16.167.62) |
| 2024-09-10 17:01:55 +0200 | dhil | (~dhil@2001:8e0:2014:3100:ad3b:d0dd:4a3b:1c29) |
| 2024-09-10 17:05:11 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 17:07:20 +0200 | meygerjos | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-09-10 17:08:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 17:08:19 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 260 seconds) |
| 2024-09-10 17:10:49 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 260 seconds) |
| 2024-09-10 17:11:15 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-09-10 17:11:57 +0200 | turlando | (~turlando@user/turlando) |
| 2024-09-10 17:12:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 17:17:13 +0200 | user4561 | (~user4561@190.16.167.62) (Ping timeout: 256 seconds) |
| 2024-09-10 17:17:53 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 17:17:59 +0200 | caconym | (~caconym@user/caconym) |
| 2024-09-10 17:22:18 +0200 | user4561 | (~user4561@190.16.167.62) |
| 2024-09-10 17:23:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 17:25:55 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-09-10 17:28:03 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-10 17:28:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-10 17:29:42 +0200 | misterfish | (~misterfis@178.225.184.56) |
| 2024-09-10 17:33:16 +0200 | meygerjos | (~meygerjos@64.18.11.0) |
| 2024-09-10 17:33:25 +0200 | phantomlee | (~phantomle@2607:fb91:e03:d762:a4cd:359d:8804:8da6) |
| 2024-09-10 17:35:10 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-10 17:35:41 +0200 | meygerjos_ | (~meygerjos@2607:fb91:21ed:a2a:3ff6:cdaa:b720:639e) |
| 2024-09-10 17:36:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 17:36:29 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 265 seconds) |
| 2024-09-10 17:37:29 +0200 | misterfish | (~misterfis@178.225.184.56) (Ping timeout: 260 seconds) |
| 2024-09-10 17:38:12 +0200 | meygerjos | (~meygerjos@64.18.11.0) (Ping timeout: 246 seconds) |
| 2024-09-10 17:39:02 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-09-10 17:40:05 +0200 | turlando | (~turlando@user/turlando) (Ping timeout: 248 seconds) |
| 2024-09-10 17:41:23 +0200 | turlando | (~turlando@user/turlando) |
| 2024-09-10 17:41:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 17:49:10 +0200 | Katarushisu1 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: The Lounge - https://thelounge.chat) |
| 2024-09-10 17:49:27 +0200 | Katarushisu1 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 2024-09-10 17:50:22 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2024-09-10 17:52:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 17:53:44 +0200 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2024-09-10 17:53:49 +0200 | phantomlee | (~phantomle@2607:fb91:e03:d762:a4cd:359d:8804:8da6) (Leaving) |
| 2024-09-10 17:55:25 +0200 | Katarushisu1 | Katarushisu |
| 2024-09-10 17:57:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-10 17:57:26 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 18:00:13 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) |
| 2024-09-10 18:01:56 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-09-10 18:03:11 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-09-10 18:07:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 18:12:03 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2024-09-10 18:14:27 +0200 | user4561 | (~user4561@190.16.167.62) (Ping timeout: 256 seconds) |
| 2024-09-10 18:15:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 18:15:54 +0200 | <haskellbridge> | <Bowuigi> monochrom re:no-type-def I thought a definition of Type was made before Cubical TT, "the interval is not a type" they say |
| 2024-09-10 18:17:54 +0200 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya for a more rigorous version of "type checking" and "type inference" check out bidirectional type checking which more cleanly separates the two in modes |
| 2024-09-10 18:18:26 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-09-10 18:18:48 +0200 | <haskellbridge> | <Bowuigi> There's even a tutorial paper showing how to convert a syntax-directed (the usual one) type system into a bidirectional one using the Pfenning recipe |
| 2024-09-10 18:20:42 +0200 | <haskellbridge> | <Bowuigi> I think it also works with non-syntax-directed ones (like the algorithms for Hindley-Milner), not sure tho |
| 2024-09-10 18:21:37 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 18:22:27 +0200 | <haskellbridge> | <Bowuigi> Bidirectional type systems are easier to implement in general, as they don't have the "guessing" part involved in declarative (aka syntax-directed or non-syntax-directed). In a sense they are like the algorithmic ones (usually non-syntax-directed, like the HM algorithms) but less "unify this" |
| 2024-09-10 18:22:35 +0200 | spew | (~spew@201.141.99.170) |
| 2024-09-10 18:23:44 +0200 | <haskellbridge> | <Bowuigi> In fact, implementations usually mirror the bidirectional type rules, modulo type errors ofc |
| 2024-09-10 18:25:51 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: very neat! thank you for the references! |
| 2024-09-10 18:25:58 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-10 18:26:20 +0200 | <jle`> | fr33domlover: don't both Double and Float range from negative infinity to infinity? |
| 2024-09-10 18:27:15 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 18:32:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2024-09-10 18:34:19 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2024-09-10 18:35:17 +0200 | akegalj | (~akegalj@89-164-127-178.dsl.iskon.hr) (Quit: leaving) |
| 2024-09-10 18:36:35 +0200 | <geekosaur> | not exactly |
| 2024-09-10 18:37:05 +0200 | <geekosaur> | both have limits beyond which the value is considered "infinity" |
| 2024-09-10 18:37:29 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2024-09-10 18:37:36 +0200 | <EvanR> | it's like a function whose range is -inf to +inf xD |
| 2024-09-10 18:37:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 18:37:44 +0200 | <EvanR> | not all values get hit by it |
| 2024-09-10 18:38:25 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 18:38:35 +0200 | <geekosaur> | https://www.tutorialspoint.com/c_standard_library/float_h.htm |
| 2024-09-10 18:41:18 +0200 | <sprout> | in other news: Germany closes borders, Dutch want to follow suit |
| 2024-09-10 18:41:56 +0200 | <sprout> | oh, wrong channel |
| 2024-09-10 18:42:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-10 18:43:52 +0200 | <haskellbridge> | <thirdofmay18081814goya> wow crazy |
| 2024-09-10 18:47:38 +0200 | <EvanR> | haskell without borders |
| 2024-09-10 18:47:56 +0200 | <haskellbridge> | <thirdofmay18081814goya> ski: how come twelf development halted? |
| 2024-09-10 18:50:48 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2024-09-10 18:53:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 18:54:51 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-09-10 18:57:17 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 252 seconds) |
| 2024-09-10 18:57:30 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-51ab-df85-c3dc-d572.rev.sfr.net) |
| 2024-09-10 18:58:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 19:04:12 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-10 19:04:18 +0200 | meygerjos_ | (~meygerjos@2607:fb91:21ed:a2a:3ff6:cdaa:b720:639e) (Ping timeout: 246 seconds) |
| 2024-09-10 19:08:14 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-51ab-df85-c3dc-d572.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-10 19:08:25 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-51ab-df85-c3dc-d572.rev.sfr.net) |
| 2024-09-10 19:13:13 +0200 | <Inst> | i hope you don't mind |
| 2024-09-10 19:13:26 +0200 | <Inst> | but how does the Alternative instance for Maybe work? |
| 2024-09-10 19:13:36 +0200 | <Inst> | on GHCI some (Just 3) hangs |
| 2024-09-10 19:13:48 +0200 | <Inst> | and if you look at the implementation it seems as though there's missing implementations for some and many |
| 2024-09-10 19:14:01 +0200 | <monochrom> | Oh, that. some and many are meant to bottom out on many instances. |
| 2024-09-10 19:14:36 +0200 | <monochrom> | But with parsers for example, they terminate and give meaningful results. |
| 2024-09-10 19:16:13 +0200 | <Inst> | applicative = lax monoidal functor, alternative = ? |
| 2024-09-10 19:16:48 +0200 | <EvanR> | alternative = a made up one-off |
| 2024-09-10 19:16:57 +0200 | <ncf> | depends what laws you consider |
| 2024-09-10 19:17:18 +0200 | <ncf> | the simplest version can also be described as a lax monoidal functor but from the cocartesian monoidal structure instead of the monoidal one |
| 2024-09-10 19:18:01 +0200 | <monochrom> | What you need is that calling p multiple times, you don't always get "success", one of the calls gives "failure". That's when many/some terminates. |
| 2024-09-10 19:18:08 +0200 | <ncf> | or equivalently as monoids in the usual category of endofunctors equipped with the "pointwise" monoidal structure |
| 2024-09-10 19:18:21 +0200 | <ncf> | see https://mathoverflow.net/questions/259120/what-is-the-mathematical-name-for-haskells-alternative-f… |
| 2024-09-10 19:18:28 +0200 | <monochrom> | But the mutual recursion between many and some is exactly right. There is no missing logic. |
| 2024-09-10 19:18:48 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 19:19:06 +0200 | <monochrom> | many (Just foo) is a problem because, only because, (Just foo) refuses to fail. |
| 2024-09-10 19:19:25 +0200 | <ncf> | instead of the cartesian* monoidal one |
| 2024-09-10 19:19:31 +0200 | <Leary> | `some` and `many` really don't need to bottom out as often as they do, though. There's an interesting discussion about this on discourse: https://discourse.haskell.org/t/should-optional-be-a-member-of-alternative |
| 2024-09-10 19:19:38 +0200 | <monochrom> | But a parser given a finite string will eventually fail, so many/some works. |
| 2024-09-10 19:22:57 +0200 | <monochrom> | Hrm that is too long-winded. Is this the gist? many (Just ()) could have been Just (repeat ()). |
| 2024-09-10 19:23:25 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-09-10 19:23:30 +0200 | <geekosaur> | many (Just ()) ~~ repeat (Just ()) |
| 2024-09-10 19:23:39 +0200 | <monochrom> | Err yeah that. |
| 2024-09-10 19:24:02 +0200 | <monochrom> | (One more data point for Dijkstra. A formula is worth a thousand pictures.) |
| 2024-09-10 19:24:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 19:25:48 +0200 | <Leary> | monochrom: That's right in this case, though there are some broader points in there too. |
| 2024-09-10 19:26:37 +0200 | <geekosaur> | right, as mentioned earlier, if you replace Just () with a parser which eventually must fail, many will produce a meaningful result |
| 2024-09-10 19:26:58 +0200 | <Inst> | okay, so Alternative is a painpoint that's still included in base because of its centrality to parsers |
| 2024-09-10 19:27:12 +0200 | <geekosaur> | I keep wondering if this means some and many should be moved out of Alternative into a "sub"class |
| 2024-09-10 19:27:39 +0200 | <geekosaur> | …unfortunately, typeclasses don't really work that way so the answer is probably "no" from a practical standpoint |
| 2024-09-10 19:27:48 +0200 | <Inst> | it should, but, ummm, FAM proposal and the huge amount of breaking code? |
| 2024-09-10 19:28:19 +0200 | <geekosaur> | FAM /per se/ wouldn't be relevant, breaking code sadly would be |
| 2024-09-10 19:29:19 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) |
| 2024-09-10 19:29:23 +0200 | <geekosaur> | I do wonder how much cod would actuallyu break, though, as the vast majority of consumers use them indirectly via some parsing package |
| 2024-09-10 19:29:41 +0200 | <geekosaur> | *code |
| 2024-09-10 19:29:56 +0200 | <Inst> | i mean FAM proposal broke a lot of code |
| 2024-09-10 19:30:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-10 19:30:17 +0200 | <Inst> | "languages that people complain about and languages that no one uses" |
| 2024-09-10 19:30:43 +0200 | <Inst> | le sigh fmap (fmap only exists because it broke a lot of list code iirc if map were changed to fmap) |
| 2024-09-10 19:32:24 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 19:33:33 +0200 | <EvanR> | I support map being what it is and fmap being what it is |
| 2024-09-10 19:34:34 +0200 | <EvanR> | lets use established words and not break everything |
| 2024-09-10 19:35:11 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 19:36:57 +0200 | <Inst> | the difference between some and many, is that |
| 2024-09-10 19:37:21 +0200 | <Inst> | total failure on some occurs on the monad, and on many, it's represented by [], right? |
| 2024-09-10 19:37:29 +0200 | <Inst> | erm, applicative, not monad |
| 2024-09-10 19:38:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 19:39:52 +0200 | <geekosaur> | some is regex +, many is regex * |
| 2024-09-10 19:40:23 +0200 | <geekosaur> | put otherwise, some requires its parameter to succeed at least once, many doesn't |
| 2024-09-10 19:40:48 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2024-09-10 19:41:28 +0200 | <dolio> | Is there some 'law' that prevents many/some for Maybe from doing something productive? |
| 2024-09-10 19:42:37 +0200 | <dolio> | Oh yeah, it says 'least solution.' |
| 2024-09-10 19:42:53 +0200 | jinsun | (~jinsun@user/jinsun) |
| 2024-09-10 19:43:02 +0200 | <Inst> | curious, does anyone ever use the IO instance for Alternative? |
| 2024-09-10 19:43:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 19:43:10 +0200 | <Inst> | some foo = fun infinite loop? |
| 2024-09-10 19:44:12 +0200 | <mauke> | some p = (:) <$> p <*> many p; many p = some p <|> pure [] |
| 2024-09-10 19:44:48 +0200 | <Inst> | tbh many is probably more useful |
| 2024-09-10 19:45:11 +0200 | <mauke> | P+ = PP*; P* = P+| |
| 2024-09-10 19:45:12 +0200 | <monochrom> | "some getChar" takes a lot of memory, but it is fairly OK. >:) |
| 2024-09-10 19:46:03 +0200 | ash3en | (~Thunderbi@2a01:c23:90c8:7900:d8fc:8363:43ac:598e) (Quit: ash3en) |
| 2024-09-10 19:46:07 +0200 | <monochrom> | I think in reality I have seen <|> used for IO, but it's pretty rare, and that's it, no one really uses many/some for IO. |
| 2024-09-10 19:49:54 +0200 | <Inst> | u = error "welp"; u <|> putStrLn "derp" |
| 2024-09-10 19:50:02 +0200 | <Inst> | <|> isn't catching |
| 2024-09-10 19:50:25 +0200 | simendsjo | (~user@84.211.91.108) |
| 2024-09-10 19:50:51 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-09-10 19:52:27 +0200 | <mauke> | sure it is |
| 2024-09-10 19:53:06 +0200 | <mauke> | but only errors thrown in IO, not IO actions that *are* errors |
| 2024-09-10 19:54:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 19:55:30 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 19:57:27 +0200 | smalltalkman | (uid545680@2a03:5180:f:4::8:5390) (Quit: Connection closed for inactivity) |
| 2024-09-10 19:59:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-10 19:59:33 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-09-10 20:07:37 +0200 | <Inst> | some / many fails for IO because it'll accumulate the list of results and thus leak |
| 2024-09-10 20:08:48 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-10 20:08:56 +0200 | <EvanR> | mapM for IO already accumulates list of results |
| 2024-09-10 20:08:57 +0200 | <monochrom> | I have trouble changing the meaning of "fail" to include that. By that standard, some/many also fails for parsers. |
| 2024-09-10 20:09:51 +0200 | <monochrom> | In fact, since no one really uses many/some for IO in production, it has never manifested as a real problem. |
| 2024-09-10 20:10:30 +0200 | <monochrom> | Whereas, everyone uses many/some for parsing, and parsing 500MB files, at which point everyone gets OOM. In production code. In reality. |
| 2024-09-10 20:10:38 +0200 | <EvanR> | demand breakage |
| 2024-09-10 20:10:44 +0200 | <EvanR> | it's only broken if anyone tries to use it |
| 2024-09-10 20:10:50 +0200 | <monochrom> | haha |
| 2024-09-10 20:12:32 +0200 | dhil | (~dhil@2001:8e0:2014:3100:ad3b:d0dd:4a3b:1c29) (Quit: Leaving) |
| 2024-09-10 20:14:10 +0200 | <monochrom> | I also have trouble calling that "leak". But that's a hot take unpopular opinion for another day. |
| 2024-09-10 20:25:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 20:26:38 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 2024-09-10 20:30:23 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 20:31:53 +0200 | meygerjos_ | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 20:34:58 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-10 20:35:00 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-10 20:35:21 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-09-10 20:39:08 +0200 | paddymahoney | (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) (Ping timeout: 264 seconds) |
| 2024-09-10 20:39:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 20:45:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-10 20:48:21 +0200 | paddymahoney | (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) |
| 2024-09-10 20:50:36 +0200 | meygerjos_ | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Remote host closed the connection) |
| 2024-09-10 20:51:00 +0200 | meygerjos_ | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 20:54:09 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2024-09-10 20:56:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 20:59:23 +0200 | neuroevolutus | (~neuroevol@146.70.211.88) |
| 2024-09-10 21:00:02 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2024-09-10 21:00:39 +0200 | caconym | (~caconym@user/caconym) |
| 2024-09-10 21:00:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 21:11:08 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-10 21:11:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 21:16:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 21:16:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 21:19:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 21:21:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 21:23:20 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 21:26:13 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 248 seconds) |
| 2024-09-10 21:26:37 +0200 | <haskellbridge> | <thirdofmay18081814goya> any worthwhile approach in semantics to distinguishing between pure and non-pure functions? |
| 2024-09-10 21:27:24 +0200 | <EvanR> | the semantics of a pure function is... a function xD |
| 2024-09-10 21:28:23 +0200 | <EvanR> | to capture whatever a non-pure function is doing you have to come up with something else, or at least add something to the domain and codomain |
| 2024-09-10 21:29:11 +0200 | <monochrom> | Actually, to a large extent, most denotational semantics simply convert impure programs to more complicated pure functions. |
| 2024-09-10 21:30:13 +0200 | <monochrom> | So you will not have a formalize definition of "impure", only a subjective judgment of "this is a very complicated function space, so it must be modelling impure programs". |
| 2024-09-10 21:31:27 +0200 | <monochrom> | OK OK, there can be one, I bet it's so easy that no one ever bothered writing it down. |
| 2024-09-10 21:32:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 21:33:03 +0200 | <monochrom> | Iff "S->T" in the target language is not simply mapped to "[ [[S]] -> [[T]] ]" in the denotational semantics, then "clearly" the target language's "S->T" is impure. |
| 2024-09-10 21:34:07 +0200 | <monochrom> | where [[S]] is the semantic domain for S, and [foo -> bar] is the space of continuous functions from foo to bar. |
| 2024-09-10 21:34:42 +0200 | <EvanR> | change the name of impure functions to subroutines and you don't have to come up with distinguishing semantics |
| 2024-09-10 21:35:05 +0200 | <monochrom> | yeah! |
| 2024-09-10 21:35:11 +0200 | <EvanR> | you have to come up with semantics for functions on one hand and subroutines on another |
| 2024-09-10 21:35:45 +0200 | <monochrom> | Hoare made a billion-dollar mistake and a million-dollar mistake. |
| 2024-09-10 21:35:56 +0200 | <monochrom> | The former is what he admitted about null pointers. |
| 2024-09-10 21:36:09 +0200 | <monochrom> | The latter is "impure function". |
| 2024-09-10 21:36:44 +0200 | <monochrom> | I don't mean you shouldn't have subroutines. You should. But you shouldn't call it "function" just because it has a return value. |
| 2024-09-10 21:37:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 21:38:56 +0200 | <mauke> | Yeah, you should call it "function" because it is built into the language! </perl4> |
| 2024-09-10 21:39:10 +0200 | <monochrom> | :( XD |
| 2024-09-10 21:39:12 +0200 | target_i | (~target_i@user/target-i/x-6023099) |
| 2024-09-10 21:39:19 +0200 | <Franciman> | perl > haskell |
| 2024-09-10 21:39:34 +0200 | <monochrom> | Also BASIC |
| 2024-09-10 21:39:38 +0200 | <Franciman> | :) |
| 2024-09-10 21:39:54 +0200 | <Franciman> | what about vb.net? |
| 2024-09-10 21:40:13 +0200 | <monochrom> | I just mean very old BASIC. |
| 2024-09-10 21:41:11 +0200 | <ski> | `GOSUB' and `DEF FN' |
| 2024-09-10 21:41:53 +0200 | <mauke> | GOSUB & LEAVELIKE |
| 2024-09-10 21:41:54 +0200 | <monochrom> | I had some very basic BASIC that didn't have DEF FN. |
| 2024-09-10 21:42:24 +0200 | <ski> | expressions were impoverished, so you couldn't do much with `DEF FN' anyway |
| 2024-09-10 21:44:01 +0200 | <EvanR> | visual basic 6 > vb.net |
| 2024-09-10 21:45:42 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-10 21:48:26 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 21:50:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-10 21:51:31 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-09-10 21:52:28 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 245 seconds) |
| 2024-09-10 21:53:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-10 21:53:41 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 2024-09-10 21:56:04 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-10 21:57:14 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-10 22:04:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 22:05:36 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-09-10 22:09:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-10 22:13:47 +0200 | athan | (~athan@2600:382:2c2b:64d3:2527:5e01:ddb7:9181) |
| 2024-09-10 22:15:28 +0200 | <[exa]> | DEF FN is rust syntax no? |
| 2024-09-10 22:15:30 +0200 | [exa] | ducks |
| 2024-09-10 22:15:50 +0200 | <monochrom> | haha |
| 2024-09-10 22:16:39 +0200 | <int-e> | . o O ( PLEASE ABSTAIN FROM DEF FNING ) |
| 2024-09-10 22:19:33 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-10 22:20:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 22:20:24 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2024-09-10 22:23:10 +0200 | <[exa]> | monochrom: btw the $1B mistake was when he admitted the pointers to algol or when he admitted they are an issue? |
| 2024-09-10 22:23:18 +0200 | <[exa]> | (I vote for the 2nd) |
| 2024-09-10 22:23:38 +0200 | <monochrom> | hahaha |
| 2024-09-10 22:23:45 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 22:23:53 +0200 | <monochrom> | when he added null pointers to algol. |
| 2024-09-10 22:23:53 +0200 | hal | (~hal@209.35.83.180) |
| 2024-09-10 22:24:04 +0200 | <hal> | i have to find a library for multivariate lagrange interpolation |
| 2024-09-10 22:24:05 +0200 | <hal> | https://hackage.haskell.org/package/polynomial-algebra-0.1.0.1 |
| 2024-09-10 22:24:11 +0200 | <hal> | i find this which has the univariate case |
| 2024-09-10 22:24:20 +0200 | <hal> | does anyone know one for the polynomial case |
| 2024-09-10 22:24:34 +0200 | <hal> | i can find papers with formulae such as |
| 2024-09-10 22:24:35 +0200 | <hal> | https://www.ams.org/journals/mcom/1995-64-211/S0025-5718-1995-1297477-5/S0025-5718-1995-1297477-5.… |
| 2024-09-10 22:24:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-09-10 22:26:44 +0200 | <[exa]> | monochrom: awww :( |
| 2024-09-10 22:29:56 +0200 | prolic_ | (~sasa@181.122.138.24) |
| 2024-09-10 22:30:47 +0200 | <prolic_> | hello there. |
| 2024-09-10 22:31:11 +0200 | <prolic_> | I have some troubles using effectful with a websocket client, would someone be able to explain this to me? |
| 2024-09-10 22:33:28 +0200 | <hal> | could you give a more detailed description of the problem, im sure we can help |
| 2024-09-10 22:33:33 +0200 | <[exa]> | hal: wow I'm seeing multivariate lagrange for the first time |
| 2024-09-10 22:33:41 +0200 | <hal> | i know, its rough |
| 2024-09-10 22:33:44 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3409-a159-51ab-df85-c3dc-d572.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-10 22:34:01 +0200 | <hal> | the paper gives some algorithms, but i dont think there are any in libraries |
| 2024-09-10 22:34:05 +0200 | <[exa]> | prolic_: best if you had some code sample and exact error that's happening |
| 2024-09-10 22:34:16 +0200 | <hal> | would anyone be up for putting together a library with me based on one of these papers? |
| 2024-09-10 22:34:35 +0200 | meygerjos_ | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-09-10 22:34:41 +0200 | <hal> | im not used to working with polynomials, maybe someone could suggest their favourite library as a starting point |
| 2024-09-10 22:34:42 +0200 | <prolic_> | wait, let me paste the code |
| 2024-09-10 22:34:59 +0200 | simendsjo | (~user@84.211.91.108) (Ping timeout: 260 seconds) |
| 2024-09-10 22:35:11 +0200 | <prolic_> | https://paste.tomsmeding.com/AJXyUeZX |
| 2024-09-10 22:35:13 +0200 | <[exa]> | hal: the paper states "It is well known that there are essential difficulties" --- complete redflag tbh :D |
| 2024-09-10 22:35:23 +0200 | <[exa]> | hal: what do you need it for? (just curious) |
| 2024-09-10 22:35:24 +0200 | <prolic_> | my problem starts on line 111, with "liftIO $ startClient $ \conn -> do" |
| 2024-09-10 22:35:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 22:36:34 +0200 | <prolic_> | runClient return IO a, but I want to do some effects instead. |
| 2024-09-10 22:37:05 +0200 | <prolic_> | so I tried runEff, but lost all interpreters, I am kind of stuck now, haha |
| 2024-09-10 22:37:27 +0200 | <hal> | [exa] its a version of a local interpolation... difficult to describe. like, im doing local gradient discovery. i have a plane and it oscilates to lower the error to local trial points. there are many of these and and average is taken. occasionally they are reset to a zero plane, and the "temperature" added each itteration again lowers the error to |
| 2024-09-10 22:37:27 +0200 | <hal> | the local fit. there is a version that is a *global* interpolation, where instead of planes that are reset to flat for local slopes that are then heated to lower error of points added on the fly, it is the same except its reset to be the simple lagrange interpolation. "simple" only in 1d... |
| 2024-09-10 22:38:47 +0200 | <hal> | the local version is parametric in "far field influence" where if a sampler proposes samples that are miles off, then it doesnt much contribute to the local fit. the global version has no such locality restriction |
| 2024-09-10 22:39:04 +0200 | <hal> | i mean. i could just not do the global version and avoid all this lagrange polynomial stuff i suppose |
| 2024-09-10 22:39:24 +0200 | <hal> | but if anyone was up for helping put together one of these algorithms it would be cool |
| 2024-09-10 22:39:33 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2024-09-10 22:39:39 +0200 | <hal> | im guessing the numerical instability considerations as a red flag is a fair point |
| 2024-09-10 22:40:23 +0200 | <[exa]> | hal: yeah if you start fitting lagrange stuff then you create scary minima and maxima all around the place which will definitely _not_ help any gradient descent |
| 2024-09-10 22:40:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 22:40:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 22:41:01 +0200 | <[exa]> | (try a lagrange interpolation of like more than 20 points in 1D, there you are ultra lucky if it doesn't diverge like crazy) |
| 2024-09-10 22:41:10 +0200 | <hal> | as new points are queried, the heat adjusts the parameters to lower the error |
| 2024-09-10 22:41:21 +0200 | <[exa]> | hal: ever heard about radial basis functions? these provide really good interpolations |
| 2024-09-10 22:41:43 +0200 | <hal> | sure, i remember those from QM undergrad |
| 2024-09-10 22:42:47 +0200 | <hal> | i can find papers like this |
| 2024-09-10 22:42:47 +0200 | <hal> | https://core.ac.uk/download/pdf/37320748.pdf |
| 2024-09-10 22:43:29 +0200 | <[exa]> | prolic_: if I get it right, you might want unliftIO |
| 2024-09-10 22:43:37 +0200 | neuroevolutus | (~neuroevol@146.70.211.88) (Ping timeout: 256 seconds) |
| 2024-09-10 22:44:17 +0200 | <[exa]> | prolic_: but it's meant for "usual" transformish monad stack, not very sure about Effectful |
| 2024-09-10 22:44:28 +0200 | <hal> | hmm, they end up doing convex optimisation using CG! |
| 2024-09-10 22:44:39 +0200 | <[exa]> | prolic_: but even in the worst case, something like that shouldn't be complex to hack in |
| 2024-09-10 22:44:51 +0200 | <hal> | this is what i was doing, except i wanted polynomial terms in eg lagrange form |
| 2024-09-10 22:45:07 +0200 | <hal> | like i kind of simple initialisation case |
| 2024-09-10 22:45:14 +0200 | <hal> | looks like thats a broken idea |
| 2024-09-10 22:45:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 22:45:59 +0200 | <hal> | i thought because there was a closed form expression for the 1d case that i could just do that for the n=0 itteration and then do stochastic methods to fit extra points gradually |
| 2024-09-10 22:46:54 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds) |
| 2024-09-10 22:46:58 +0200 | <prolic_> | [exa]: where can I import the unliftIO function from? can't find it. |
| 2024-09-10 22:47:18 +0200 | <hal> | prolic_ did you try hoogle? |
| 2024-09-10 22:47:39 +0200 | <hal> | https://hoogle.haskell.org/?hoogle=unliftIO+&scope=set%3Astackage |
| 2024-09-10 22:47:48 +0200 | <prolic_> | thanks, let me try |
| 2024-09-10 22:48:28 +0200 | <[exa]> | ah actually there seems to be some effectful support for this |
| 2024-09-10 22:48:30 +0200 | <[exa]> | https://hackage.haskell.org/package/effectful-core-2.3.1.0/docs/Effectful-Internal-Unlift.html |
| 2024-09-10 22:49:51 +0200 | <[exa]> | they even claim some compatibility with unliftio-core, so maybe it's just hidden somewhere in them docs |
| 2024-09-10 22:50:38 +0200 | <hal> | ew, what a horrible library |
| 2024-09-10 22:50:51 +0200 | <prolic_> | I tried using unliftIO, just get a nice compile error |
| 2024-09-10 22:51:21 +0200 | <prolic_> | https://paste.tomsmeding.com/W3G1uzKY |
| 2024-09-10 22:51:23 +0200 | <[exa]> | likely not gonna be super straightforward but there should be a way prepared |
| 2024-09-10 22:51:48 +0200 | meygerjos_ | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 22:52:10 +0200 | <hal> | yeah, your lifting the IO version into EFF |
| 2024-09-10 22:52:29 +0200 | <hal> | i kind of dont see what your doing with this unlifting? |
| 2024-09-10 22:52:57 +0200 | <[exa]> | hal: there's a function which cannot take the Eff effects through and can only do IO, the task is to somehow smuggle the Eff into that one |
| 2024-09-10 22:53:02 +0200 | <[exa]> | so that it can do nicely |
| 2024-09-10 22:54:19 +0200 | <hal> | i just mean thats what the type error seems to say? |
| 2024-09-10 22:54:29 +0200 | athan_ | (~athan@2600:382:2c2b:64d3:2527:5e01:ddb7:9181) |
| 2024-09-10 22:54:58 +0200 | athan | (~athan@2600:382:2c2b:64d3:2527:5e01:ddb7:9181) (Ping timeout: 245 seconds) |
| 2024-09-10 22:55:05 +0200 | <hal> | did you just try to put unlift around the do block like where it has lift previously? cos thats not gona work |
| 2024-09-10 22:55:17 +0200 | <hal> | the overall type returns it in Eff |
| 2024-09-10 22:55:44 +0200 | <hal> | [exa] i think im not going to do the global interpolant case |
| 2024-09-10 22:55:51 +0200 | <hal> | thanks for the direction |
| 2024-09-10 22:55:52 +0200 | <hal> | peace |
| 2024-09-10 22:55:53 +0200 | hal | (~hal@209.35.83.180) (Quit: Connection closed) |
| 2024-09-10 22:56:10 +0200 | <[exa]> | hal: btw with your interpolation, I recall I used inverse-distance weighted things somewhere (interpolation = sum_i (value_i * 1/distance_i) / sum (1/distance_i)) |
| 2024-09-10 22:56:18 +0200 | <[exa]> | ah ok |
| 2024-09-10 22:56:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 22:58:12 +0200 | <[exa]> | prolic_: anyway the scheme for doing that stuff should be generally: `withRunInIO $ \toIo -> theProblematicIOFunction toIo effectfulStuffHere` |
| 2024-09-10 22:59:54 +0200 | <[exa]> | and this one should work even with concurrent stuff: https://hackage.haskell.org/package/effectful-core-2.3.1.0/docs/Effectful.html#v:withEffToIO |
| 2024-09-10 23:00:46 +0200 | <prolic_> | let me try |
| 2024-09-10 23:03:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-10 23:05:48 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: pillow time) |
| 2024-09-10 23:07:39 +0200 | <prolic_> | https://paste.tomsmeding.com/RMOPwjaB |
| 2024-09-10 23:08:02 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-09-10 23:08:03 +0200 | <prolic_> | seems I'm too stupid |
| 2024-09-10 23:08:11 +0200 | Guest5257 | (~Guest52@d108-172-198-192.bchsia.telus.net) (Quit: Connection closed) |
| 2024-09-10 23:08:12 +0200 | <[exa]> | you don't need liftIO |
| 2024-09-10 23:08:47 +0200 | lambdaRule | (~lambdaRul@node-1w7jr9phpv012678fhwoq5x7q.ipv6.telus.net) |
| 2024-09-10 23:09:02 +0200 | lambdaRule | (~lambdaRul@node-1w7jr9phpv012678fhwoq5x7q.ipv6.telus.net) (Client Quit) |
| 2024-09-10 23:10:12 +0200 | <[exa]> | just: withEfftoIo ConcurrentUnlift $ \runE -> startClient $ \conn -> runE $ do |
| 2024-09-10 23:10:17 +0200 | <[exa]> | prolic_: ^ |
| 2024-09-10 23:10:30 +0200 | <[exa]> | the EfftoIo should do the lift for you btw |
| 2024-09-10 23:11:51 +0200 | <[exa]> | AFAIK internally it literally captures the thing that represents your Eff state, then it smuggles it around the IO function as an IORef or something (which is carried by the runE), and runE just restores the thing in the intter Eff |
| 2024-09-10 23:13:29 +0200 | <geekosaur> | sounds moderately risky to me |
| 2024-09-10 23:14:11 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-09-10 23:14:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 23:14:40 +0200 | michalz | (~michalz@185.246.207.215) (Remote host closed the connection) |
| 2024-09-10 23:14:48 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 23:16:07 +0200 | <prolic_> | https://paste.tomsmeding.com/ngekXPDG |
| 2024-09-10 23:16:15 +0200 | <prolic_> | again compile errors |
| 2024-09-10 23:16:52 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-09-10 23:17:08 +0200 | <[exa]> | prolic_: you might need liftIO inside of that startClient function now |
| 2024-09-10 23:17:13 +0200 | <[exa]> | because you un-IOd it |
| 2024-09-10 23:18:11 +0200 | <prolic_> | [exa]: nope, doesn't work either |
| 2024-09-10 23:18:46 +0200 | <[exa]> | also no runEff or so, just async$... and logDebug$... |
| 2024-09-10 23:19:03 +0200 | <[exa]> | anyway if that fails I might be out of ideas |
| 2024-09-10 23:19:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 23:19:12 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-09-10 23:19:43 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-09-10 23:23:06 +0200 | <prolic_> | wow, this seems to work: withEffToIO SeqUnlift $ \runE -> startClient $ \conn -> liftIO $ runE $ do |
| 2024-09-10 23:23:57 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-10 23:24:11 +0200 | <[exa]> | ah I assumed the startClient is an IO, it's an Eff? |
| 2024-09-10 23:25:20 +0200 | <prolic_> | startClient by default is IO a, correct |
| 2024-09-10 23:25:21 +0200 | <prolic_> | withEffToIO (ConcUnlift Ephemeral Unlimited) $ \runE -> startClient $ \conn -> liftIO $ runE $ do |
| 2024-09-10 23:25:23 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2024-09-10 23:25:24 +0200 | <prolic_> | this works, too |
| 2024-09-10 23:25:31 +0200 | <prolic_> | which strategy should I use? |
| 2024-09-10 23:26:38 +0200 | <prolic_> | last error I have is this: msg <- Exception.try $ WS.receiveData conn :: IO (Either WS.ConnectionException BSL.ByteString) - but I think effectful has exception handling build-in. do you know how to use it by accident? |
| 2024-09-10 23:27:20 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-09-10 23:27:21 +0200 | <[exa]> | and the inner monad in startClient is IO too? |
| 2024-09-10 23:27:31 +0200 | <[exa]> | 'inner' as in the parameter action |
| 2024-09-10 23:27:44 +0200 | meygerjos_ | (~meygerjos@syn-024-090-143-083.res.spectrum.com) (Remote host closed the connection) |
| 2024-09-10 23:27:55 +0200 | <[exa]> | I don't see why it would require liftIO |
| 2024-09-10 23:28:03 +0200 | meygerjos_ | (~meygerjos@syn-024-090-143-083.res.spectrum.com) |
| 2024-09-10 23:28:12 +0200 | <prolic_> | ah, you mean this: withEffToIO (ConcUnlift Ephemeral Unlimited) $ \runE -> startClient $ \conn -> runE $ do |
| 2024-09-10 23:28:17 +0200 | <prolic_> | yes, that works |
| 2024-09-10 23:30:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 23:31:18 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-09-10 23:33:19 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-09-10 23:34:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-10 23:38:04 +0200 | <[exa]> | ah ok great |
| 2024-09-10 23:39:09 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-09-10 23:39:32 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2024-09-10 23:41:28 +0200 | astroanax | (~astroanax@cosmic.voyage) (Ping timeout: 252 seconds) |
| 2024-09-10 23:41:28 +0200 | df | (~ben@justworks.xyz) (Ping timeout: 252 seconds) |
| 2024-09-10 23:41:42 +0200 | df | (~ben@justworks.xyz) |
| 2024-09-10 23:41:52 +0200 | astroanax | (~astroanax@2001:19f0:7402:f82:5400:1ff:fec4:f7d7) |
| 2024-09-10 23:45:28 +0200 | <prolic_> | I tried to get tryError running |
| 2024-09-10 23:45:56 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-10 23:46:41 +0200 | <prolic_> | I thought this looks good: https://paste.tomsmeding.com/lP4478HX |
| 2024-09-10 23:47:32 +0200 | <prolic_> | but instead I have tons of compile errors, like Could not deduce (Logging :> es1) arising from a use of ‘logDebug’. |
| 2024-09-10 23:50:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-10 23:51:30 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2024-09-10 23:51:35 +0200 | ubert | (~Thunderbi@178.115.52.77.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 2024-09-10 23:52:55 +0200 | pavonia | (~user@user/siracusa) |
| 2024-09-10 23:55:34 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-10 23:57:31 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |