Logs on 2024-11-07 (liberachat/#haskell)
| 00:00:26 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:04:51 | → | hueso joins (~root@user/hueso) |
| 00:05:05 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 00:06:18 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 00:12:02 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 00:14:10 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 00:14:10 | ljdarj1 | is now known as ljdarj |
| 00:14:57 | × | supercode quits (~supercode@user/supercode) (Quit: Client closed) |
| 00:15:32 | × | sprotte24 quits (~sprotte24@p200300d16f45f60044d2f8c33ad18940.dip0.t-ipconnect.de) (Quit: Leaving) |
| 00:15:47 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:20:23 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 00:22:12 | × | xff0x quits (~xff0x@2405:6580:b080:900:3e16:56e8:fa8f:748e) (Ping timeout: 276 seconds) |
| 00:23:04 | <monochrom> | Haha so there is opportunity for saying "Lean 88"?! :) |
| 00:27:25 | <monochrom> | But I disagree with Oleg in thinking of () as world state. Instead, it is more honest without sacrificing pragmatics to adopt that in "() -> Codomain" the -> is a Kleisli arrow. |
| 00:28:38 | × | TonyStone quits (~TonyStone@user/TonyStone) (Quit: Leaving) |
| 00:28:54 | → | TonyStone joins (~TonyStone@user/TonyStone) |
| 00:31:11 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:33:10 | <haskellbridge> | <zwro> would we be better off without undefined and error and other bottoms? could we guarantee totality (modulo termination)? |
| 00:34:07 | <geekosaur> | no, because there are other ways to get bottoms any time there are external inputs |
| 00:35:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:36:06 | <geekosaur> | too many bottoms, thanks to whoever thought it was a brilliant idea to throw an exception (which is a bottom) on file not found etc. |
| 00:39:46 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 00:43:16 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:46:34 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:51:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 00:51:44 | → | troojg joins (~troojg@user/troojg) |
| 00:56:23 | × | alexherbo2 quits (~alexherbo@2a02-8440-341a-456e-a8d1-f94d-35c3-2d26.rev.sfr.net) (Remote host closed the connection) |
| 01:00:18 | <haskellbridge> | <zwro> can't those exceptions be "caught" with something like `readFile :: IO (Either Exception FileContents)` ? |
| 01:00:56 | <haskellbridge> | <zwro> (pseudocode) |
| 01:01:54 | → | LainExperiments joins (~LainExper@user/LainExperiments) |
| 01:02:24 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:07:14 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 01:09:42 | × | KaitoDaumoto quits (~Unity3D@user/kaitodaumoto) (Remote host closed the connection) |
| 01:09:58 | <haskellbridge> | <zwro> maybe i want to explore liquid haskell? |
| 01:14:08 | → | jero98772 joins (~jero98772@2800:484:1d7c:cc00::3) |
| 01:14:13 | × | jero98772 quits (~jero98772@2800:484:1d7c:cc00::3) (Client Quit) |
| 01:15:05 | → | notzmv joins (~daniel@user/notzmv) |
| 01:15:09 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 01:16:08 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 01:17:47 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:20:06 | <geekosaur> | no, they're actual exceptions that must be caught in `IO` with `catch` or `handle` etc. |
| 01:21:01 | <dolio> | Well, you could restructure everything to return explicit failures. However, the problem is that that isn't necessarily a good idea. |
| 01:22:40 | <geekosaur> | as long as exceptions are a trainwreck, I can't see it being worse |
| 01:23:48 | <dolio> | That's very naive. |
| 01:24:54 | <geekosaur> | https://mail.haskell.org/pipermail/libraries/2014-September/023675.html |
| 01:25:09 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 01:25:11 | <geekosaur> | you're likely to leak with any exception |
| 01:25:25 | <geekosaur> | synchronous exceptions were a fundamental mistake |
| 01:26:35 | × | LainExperiments quits (~LainExper@user/LainExperiments) (Quit: Client closed) |
| 01:29:41 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 01:29:46 | → | LainExperiments joins (~LainExper@user/LainExperiments) |
| 01:35:50 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:38:52 | <dolio> | If you mean asynchronous exceptions, then you are unnecessarily conflating that with other aspects of the exception API. |
| 01:39:52 | <dolio> | E.G. if you don't want to locally handle an explicit `Either` result, then you need to use a monad transformer or something. |
| 01:40:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 01:42:02 | <dolio> | Which is possible, but then you probably have a lot of lifting and lowering to do. And also, the transformer will probably have abysmal performance characteristics, because it will repeatedly be building and inspecting Either values for the expected common case of not having an exception. |
| 01:46:40 | <dolio> | For scenarios where exceptions are actually exceptional, you want an alternate implementation, like continuations for algebraic effects, so that you just install a handler once and you only jump out to it when there actually is an exception. It's technically the same 'type,' but one implementation is far superior for how it will likely be used. |
| 01:49:39 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 01:49:58 | → | euleritian joins (~euleritia@77.22.252.56) |
| 01:51:12 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:54:18 | <Leary> | We could (and imo should) have unchecked panics (anywhere) and statically checked exceptions (IO/ST only) with `IO/ST :: [Exception] -> Type -> Type` uniting exception sets in `<*>`/`>>=` while `try`/`catch` delete one and `main :: IO [] (); runST :: (forall s. ST [] a) -> a`. Interruptible operations would necessarily include async exceptions in the type-level list of exceptions they might throw. The actual implementation would be essentially unchanged |
| 01:54:18 | <Leary> | , the interface would just be more strongly typed. |
| 01:55:39 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:02:03 | × | LainExperiments quits (~LainExper@user/LainExperiments) (Ping timeout: 256 seconds) |
| 02:02:30 | → | califax_ joins (~califax@user/califx) |
| 02:03:01 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 02:03:14 | × | TonyStone quits (~TonyStone@user/TonyStone) (Ping timeout: 260 seconds) |
| 02:03:36 | × | califax quits (~califax@user/califx) (Ping timeout: 260 seconds) |
| 02:03:36 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds) |
| 02:03:50 | califax_ | is now known as califax |
| 02:05:11 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 02:05:27 | → | gmg joins (~user@user/gehmehgeh) |
| 02:06:36 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:10:48 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 02:12:01 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 02:14:40 | × | spew quits (~spew@201.141.99.170) (Quit: spew) |
| 02:18:08 | → | TonyStone joins (~TonyStone@user/TonyStone) |
| 02:21:59 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:23:46 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 02:26:59 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:32:31 | → | ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com) |
| 02:35:29 | × | troojg quits (~troojg@user/troojg) (Ping timeout: 248 seconds) |
| 02:37:20 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:39:26 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 02:42:19 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:48:50 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:54:24 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:01:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:10:48 | × | weary-traveler quits (~user@user/user363627) (Ping timeout: 245 seconds) |
| 03:12:29 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:12:45 | → | blover joins (~arthur@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) |
| 03:13:50 | → | weary-traveler joins (~user@user/user363627) |
| 03:17:05 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 03:20:03 | × | blover quits (~arthur@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) (Remote host closed the connection) |
| 03:20:38 | → | blover joins (~blover@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) |
| 03:27:51 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:32:32 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 03:33:29 | × | TimWolla quits (~timwolla@2a01:4f8:150:6153:beef::6667) (Ping timeout: 260 seconds) |
| 03:40:10 | <Axman6> | I wrote something to do that years ago, which used indexed monads to list the possible expections, and handlers would remove them from the list |
| 03:40:52 | × | blover quits (~blover@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) (*.net *.split) |
| 03:40:52 | × | gmg quits (~user@user/gehmehgeh) (*.net *.split) |
| 03:40:52 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (*.net *.split) |
| 03:40:52 | × | califax quits (~califax@user/califx) (*.net *.split) |
| 03:40:52 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (*.net *.split) |
| 03:40:52 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (*.net *.split) |
| 03:40:52 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (*.net *.split) |
| 03:42:59 | <Axman6> | https://gist.github.com/axman6/19adc08a809d919a2efb |
| 03:43:13 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:43:25 | <Axman6> | (From back in the day when we didn't have most of those type level functions on lists defined for us) |
| 03:46:33 | → | califax joins (~califax@user/califx) |
| 03:46:34 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 03:46:36 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 03:47:39 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 03:50:15 | → | TimWolla joins (~timwolla@2a01:4f8:150:6153:beef::6667) |
| 03:50:50 | → | Inst_ joins (~Inst@user/Inst) |
| 03:50:51 | × | td_ quits (~td@i53870906.versanet.de) (Ping timeout: 276 seconds) |
| 03:51:02 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 03:51:19 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 03:52:23 | → | td_ joins (~td@i5387092D.versanet.de) |
| 03:53:21 | × | Inst quits (~Inst@user/Inst) (Ping timeout: 248 seconds) |
| 03:54:23 | → | gmg joins (~user@user/gehmehgeh) |
| 04:01:13 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:05:52 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 04:11:24 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 04:12:16 | <Leary> | Axman6: The Atkey parameterised monad isn't ideal for this; you want a graded(?) monad: `class Graded (m :: k -> Type -> Type) where { type E m :: k; type Ap m (g1 :: k) (g2 :: k) :: k; pure :: a -> m (E m) a; (>>=) :: m g1 a -> (a -> m g2 b) -> m (Ap m g1 g2) b }`, with the obvious monoidal properties at both levels. |
| 04:16:36 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:17:46 | <Axman6> | Not sure I follow how that works, I thik I'd need to see the instances |
| 04:21:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 04:31:59 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:37:49 | × | Inst_ quits (~Inst@user/Inst) (Ping timeout: 260 seconds) |
| 04:38:00 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 04:38:43 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 04:42:19 | <jackdk> | Does anyone have a favourite rank2classes-style library that provides a class for HKD representables? I'm specifically looking for a class to associate a record with a GADT namings its fields (like a total DMap) and a FRepresentable sounds like it would fit the bill. I don't need a rank-2 tabulate, if that makes the search easier. The FIndexable in Ed's distributive library looks right but never made it from GitHub to Hackage. |
| 04:45:38 | → | aforemny_ joins (~aforemny@i59F4C67C.versanet.de) |
| 04:46:34 | × | aforemny quits (~aforemny@i577B13E8.versanet.de) (Ping timeout: 260 seconds) |
| 04:50:02 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:55:46 | × | Square quits (~Square4@user/square) (Ping timeout: 252 seconds) |
| 04:58:31 | <Leary> | Axman6: https://gist.github.com/LSLeary/4484fb6bc4d96e59092d48592c162b9f |
| 05:00:24 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 05:07:57 | → | famubu joins (~famubu@user/famubu) |
| 05:09:26 | <famubu> | Hi. I was trying to do the example shown in the FRACTRAN wikipedia article: https://en.wikipedia.org/wiki/FRACTRAN |
| 05:09:36 | <famubu> | This is what I did: https://bpa.st/2FVCW |
| 05:09:51 | <famubu> | It gets the first few numbers right, but then goes wrong. |
| 05:09:57 | <famubu> | Any idea how to fix it? |
| 05:10:08 | <famubu> | This is my first time using Data.Ratio |
| 05:10:47 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:11:37 | <famubu> | Could be the `isInt` function? |
| 05:11:51 | <monochrom> | Is it actually safe to use Int and Ratio Int for this? Will you get integers too big for Int? |
| 05:13:15 | <famubu> | I was doing it under the assumption that it won't go beyond Int. Maybe I should change it? |
| 05:14:05 | <famubu> | Doing Int instead of Integer made it necessary to convert between Int and Integer too. |
| 05:14:26 | <Leary> | Axman6: (refresh to see improvements, if you already opened that link) |
| 05:15:00 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 05:18:41 | <famubu> | Made a version using Integer instead of Int: https://bpa.st/WT4TU |
| 05:18:51 | <famubu> | Result is still incorrect though.. |
| 05:19:09 | <famubu> | It's giving [2,15,825,725,1925,2275,425,25 |
| 05:19:23 | <famubu> | should've been [2,15,825,725,1925,2275,425,390, |
| 05:25:55 | <probie> | Why are you roundtripping via `Float`? Surely `isInt` could be more easily defined as `isInt x = denominator x == 1`. With that (and removing `fromRational`) I get correct answers with your code |
| 05:26:08 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:28:29 | <EvanR> | was just musing with this bog standard python code for 36028797018963968 `div` 5... which is apparently int(36028797018963968 / 5), which round trips through float and gets the wrong answer xD |
| 05:29:02 | <EvanR> | there is a // operator for integer division but it is doing the equivalent of `quot` instead of div |
| 05:29:45 | <EvanR> | floats... so alluring... so deadly |
| 05:30:42 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:32:17 | <famubu> | probie: Oh yeah.. Thanks! |
| 05:32:23 | <famubu> | Modified it to https://bpa.st/HQC4O |
| 05:32:26 | <famubu> | It works. |
| 05:34:06 | <famubu> | The `foo` function feels a bit messy. Any suggestions to make it better? More readable? |
| 05:39:09 | <Axman6> | Leary: nice, definitely simpler than the index monad version |
| 05:40:57 | <probie> | fambu: Perhaps something like https://paste.tomsmeding.com/oA1DYLzQ |
| 05:41:33 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:42:03 | <Axman6> | famubu: you can make multiple definitions inside a let block: let mfn = ...\n bs = ...\n bb = ...\nin |
| 05:44:53 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 05:45:34 | <famubu> | probie: Thanks. :) |
| 05:45:53 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 05:46:26 | <famubu> | Axman6: Oh.. didn't know that. Will keep that in mind. |
| 05:49:39 | <Axman6> | famubu: some things worth noting from probie's code, functions like null, head, tail etc. are often better replaced by case statements which allow you to perform the check (null) and also name the values you want (the head of the list) in one, efficient statement |
| 05:51:31 | × | ryanbooker quits (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 05:51:32 | <Axman6> | not sure how I feel about the use of round, I feel like it's likely to be doing more than just numerator would, which we know is the right value |
| 05:51:38 | × | pavonia quits (~user@user/siracusa) (Read error: Connection reset by peer) |
| 05:51:53 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 05:51:57 | → | pavonia joins (~user@user/siracusa) |
| 05:52:16 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 05:52:43 | → | michalz joins (~michalz@185.246.207.221) |
| 05:56:36 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:57:10 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 05:57:27 | → | califax joins (~califax@user/califx) |
| 05:58:06 | <famubu> | Axman6: +1 |
| 06:00:19 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 06:01:02 | → | gmg joins (~user@user/gehmehgeh) |
| 06:01:14 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 06:09:05 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 06:09:41 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 06:12:00 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:15:45 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Read error: Connection reset by peer) |
| 06:16:03 | → | longlongdouble joins (~longlongd@169.150.196.103) |
| 06:17:21 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 06:17:56 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:25:14 | × | longlongdouble quits (~longlongd@169.150.196.103) (Ping timeout: 252 seconds) |
| 06:26:08 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 06:28:04 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:31:38 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 255 seconds) |
| 06:31:48 | → | euleritian joins (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) |
| 06:33:21 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 06:43:26 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:43:28 | × | euleritian quits (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 06:44:36 | → | euleritian joins (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) |
| 06:48:38 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 06:55:11 | → | acidjnk joins (~acidjnk@p200300d6e7283f9509f155732eb456c8.dip0.t-ipconnect.de) |
| 06:57:38 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:02:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 07:07:39 | → | jco joins (~jco@78-70-217-44-no600.tbcn.telia.com) |
| 07:07:46 | → | alp joins (~alp@2001:861:e3d6:8f80:4549:4578:5f94:9afe) |
| 07:10:31 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 07:13:01 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:13:51 | → | gmg joins (~user@user/gehmehgeh) |
| 07:15:12 | × | dolio quits (~dolio@130.44.140.168) (Ping timeout: 252 seconds) |
| 07:17:32 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 07:18:16 | → | dolio joins (~dolio@130.44.140.168) |
| 07:22:34 | × | jco quits (~jco@78-70-217-44-no600.tbcn.telia.com) (Quit: leaving) |
| 07:28:34 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:33:49 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 07:34:13 | → | longlongdouble joins (~longlongd@169.150.196.103) |
| 07:38:27 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:44:14 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:47:25 | × | ft quits (~ft@p4fc2a216.dip0.t-ipconnect.de) (Quit: leaving) |
| 07:48:12 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 07:48:39 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 07:50:14 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 07:51:10 | → | briandaed joins (~root@185.234.210.211) |
| 07:51:11 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:51:27 | → | misterfish joins (~misterfis@h239071.upc-h.chello.nl) |
| 07:52:27 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 07:55:11 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:00:01 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 08:00:39 | → | caconym joins (~caconym@user/caconym) |
| 08:03:09 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 08:11:19 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 260 seconds) |
| 08:13:24 | → | cyphase joins (~cyphase@user/cyphase) |
| 08:15:35 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:18:09 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 260 seconds) |
| 08:19:18 | × | longlongdouble quits (~longlongd@169.150.196.103) (Ping timeout: 276 seconds) |
| 08:19:29 | → | sourcetarius joins (~sourcetar@user/sourcetarius) |
| 08:20:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 08:20:42 | → | longlongdouble joins (~longlongd@169.150.196.103) |
| 08:29:19 | → | cyphase joins (~cyphase@user/cyphase) |
| 08:31:39 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 08:33:36 | × | notzmv quits (~daniel@user/notzmv) (Ping timeout: 276 seconds) |
| 08:35:20 | → | rvalue- joins (~rvalue@user/rvalue) |
| 08:35:33 | × | euleritian quits (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) (Ping timeout: 248 seconds) |
| 08:36:09 | → | euleritian joins (~euleritia@77.22.252.56) |
| 08:36:17 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 255 seconds) |
| 08:41:11 | rvalue- | is now known as rvalue |
| 08:43:54 | → | turlando joins (~turlando@user/turlando) |
| 08:44:42 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:44:55 | × | longlongdouble quits (~longlongd@169.150.196.103) (Ping timeout: 252 seconds) |
| 08:46:28 | → | longlongdouble joins (~longlongd@169.150.196.103) |
| 08:54:50 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 08:56:09 | → | petrichor joins (~znc-user@user/petrichor) |
| 08:57:57 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 08:59:06 | × | longlongdouble quits (~longlongd@169.150.196.103) (Ping timeout: 272 seconds) |
| 09:00:26 | → | longlongdouble joins (~longlongd@169.150.196.103) |
| 09:01:25 | → | merijn joins (~merijn@77.242.116.146) |
| 09:03:31 | → | supercode joins (~supercode@user/supercode) |
| 09:03:58 | → | ubert joins (~Thunderbi@77.119.163.56.wireless.dyn.drei.com) |
| 09:05:18 | × | longlongdouble quits (~longlongd@169.150.196.103) (Ping timeout: 246 seconds) |
| 09:06:05 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 09:16:49 | → | hgolden__ joins (~hgolden@146.70.173.229) |
| 09:19:24 | × | hgolden_ quits (~hgolden@169.150.203.10) (Ping timeout: 252 seconds) |
| 09:21:15 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 09:21:53 | × | misterfish quits (~misterfis@h239071.upc-h.chello.nl) (Ping timeout: 248 seconds) |
| 09:28:55 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 09:31:37 | → | comerijn joins (~merijn@77.242.116.146) |
| 09:31:49 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 09:32:42 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 09:37:26 | <kuribas> | Which proof assistants have good automation? |
| 09:37:56 | <kuribas> | Is it true that dependently typed proof assistants (agda, coq, idris) have worse automation than HOL based (isabella)? |
| 09:38:48 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 09:40:10 | <tomsmeding> | Coq has fairly good automation, not familiar with HOL; Agda has ~absent automation |
| 09:40:30 | <tomsmeding> | but contrary to Coq, Agda has readable syntax |
| 09:41:11 | × | supercode quits (~supercode@user/supercode) (Quit: Client closed) |
| 09:46:24 | × | Versality quits (~Versality@user/Versality) (Remote host closed the connection) |
| 09:46:37 | → | Versality joins (~Versality@user/Versality) |
| 09:49:47 | → | alexherbo2 joins (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) |
| 09:51:18 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 09:55:40 | → | misterfish joins (~misterfis@31-161-39-137.biz.kpn.net) |
| 09:58:38 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 10:00:32 | × | alexherbo2 quits (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 10:00:52 | → | alexherbo2 joins (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) |
| 10:01:48 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 10:05:50 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Ping timeout: 255 seconds) |
| 10:09:03 | → | SlackCoder joins (~SlackCode@64-94-63-8.ip.weststar.net.ky) |
| 10:13:06 | → | merijn joins (~merijn@77.242.116.146) |
| 10:13:38 | → | xdminsy joins (~xdminsy@117.147.71.147) |
| 10:16:59 | → | sroso joins (~sroso@user/SrOso) |
| 10:18:04 | × | xdminsy quits (~xdminsy@117.147.71.147) (Client Quit) |
| 10:19:39 | <kuribas> | tomsmeding: what about this? https://agda.readthedocs.io/en/latest/tools/auto.html |
| 10:20:39 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 260 seconds) |
| 10:23:00 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:24:21 | → | xdminsy joins (~xdminsy@117.147.71.147) |
| 10:26:27 | <kuribas> | tomsmeding: did you mean there is no automation, or that "absent" is an automation feature? |
| 10:28:43 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 10:29:36 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 10:32:16 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 10:32:45 | → | kritzefitz joins (~kritzefit@debian/kritzefitz) |
| 10:39:42 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Ping timeout: 276 seconds) |
| 10:43:09 | → | notzmv joins (~daniel@user/notzmv) |
| 10:43:16 | <tomsmeding> | kuribas: I meant "no automation", but that's indeed not strictly true. 'auto' is useful for constructing simple lambda calculus terms, but it's multiple leagues below e.g. coq's 'omega' which just solves integer arithmetic stuff for you |
| 10:43:53 | <tomsmeding> | and 'omega' is not considered "fancy" in coq world |
| 10:44:42 | <kuribas> | ah right :) |
| 10:44:49 | <tomsmeding> | there is an integer _equality_ solver in agda-stdlib, but you have to explicitly write out the equality that you want it to solve |
| 10:44:58 | <tomsmeding> | and for inequalities, well, you're on your own with the basic lemmas |
| 10:45:23 | <tomsmeding> | agda-presburger can do it but it's doubly-exponential so it runs out of memory once you have 8 variables in your formula |
| 10:46:17 | <kuribas> | idris has a proof search algorithm, but it's also fragile. |
| 10:46:28 | tomsmeding | doesn't know much about idris |
| 10:49:56 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 10:52:06 | → | merijn joins (~merijn@77.242.116.146) |
| 10:53:02 | × | mulk quits (~mulk@pd95146e9.dip0.t-ipconnect.de) (Quit: ZNC - http://znc.in) |
| 10:53:24 | → | mulk joins (~mulk@pd95146e9.dip0.t-ipconnect.de) |
| 10:57:31 | → | Digitteknohippie joins (~user@user/digit) |
| 10:57:35 | × | Digit quits (~user@user/digit) (Ping timeout: 255 seconds) |
| 11:00:42 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 11:05:04 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 11:10:02 | × | alexherbo2 quits (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 11:11:28 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 11:13:11 | → | xff0x joins (~xff0x@2405:6580:b080:900:759a:e3d6:c0c3:b78a) |
| 11:20:53 | Digitteknohippie | is now known as Digit |
| 11:23:47 | → | merijn joins (~merijn@77.242.116.146) |
| 11:25:58 | × | sroso quits (~sroso@user/SrOso) (Quit: Leaving :)) |
| 11:27:21 | → | alexherbo2 joins (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) |
| 11:30:53 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 11:31:22 | × | pavonia quits (~user@user/siracusa) (Read error: Connection reset by peer) |
| 11:32:05 | → | pavonia joins (~user@user/siracusa) |
| 11:37:07 | × | youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 11:38:53 | → | youthlic joins (~Thunderbi@user/youthlic) |
| 11:42:38 | → | merijn joins (~merijn@77.242.116.146) |
| 11:47:12 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 11:52:11 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 260 seconds) |
| 11:52:21 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 11:52:21 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:54:50 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 11:56:24 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:59:40 | → | merijn joins (~merijn@77.242.116.146) |
| 12:00:04 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 12:01:37 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 12:02:11 | → | caconym joins (~caconym@user/caconym) |
| 12:04:43 | → | longlongdouble joins (~longlongd@117.234.149.253) |
| 12:17:17 | → | Inst joins (~Inst@user/Inst) |
| 12:17:23 | <Inst> | don't ask to ask, applicative laws? |
| 12:17:27 | × | longlongdouble quits (~longlongd@117.234.149.253) (Read error: Connection reset by peer) |
| 12:18:06 | <Inst> | composition -> associativity of monoids, other three laws = identity quality of pure |
| 12:18:33 | → | longlongdouble joins (~longlongd@2409:40d4:4052:dbab:1989:242:cab1:419a) |
| 12:24:39 | → | CoolMa7 joins (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) |
| 12:27:59 | × | longlongdouble quits (~longlongd@2409:40d4:4052:dbab:1989:242:cab1:419a) (Ping timeout: 260 seconds) |
| 12:29:23 | → | longlongdouble joins (~longlongd@117.234.149.253) |
| 12:30:26 | <Leary> | Inst: Identity === /left/ identity; Interchange === /symmetry/ of identity (hence /right/ identity). Homomorphism is redundant, following from parametricity. |
| 12:31:14 | <Inst> | thanks leary |
| 12:31:28 | <Inst> | didn't figure out on my own to compartmentalize them into left and right identity |
| 12:32:01 | <Inst> | just a strong lax monoidal functor, what's the problem? ツ |
| 12:39:12 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:42:21 | <kuribas> | tomsmeding: you mean coq has the best proof solving among dependently typed proof systems? |
| 12:42:34 | <kuribas> | tomsmeding: But the tactics are separate from the language, right? |
| 12:43:09 | × | famubu quits (~famubu@user/famubu) (Ping timeout: 260 seconds) |
| 12:48:35 | <haskellbridge> | <zwro> i'm playing around with the ghcitui and haskeline packages. i wonder if it's impossible to stream the output of, say, `let a = 1 : a in a` instead of waiting (in vain) for it to complete |
| 12:50:05 | <geekosaur> | _if_ ghci is being run in a pty and buffering is disabled, streaming should work |
| 12:50:54 | <geekosaur> | without the former, you get output in (I think 8kb on Linux) chunks; without the latter you get line buffering, but it's all one line so you again end up getting chunks when the line overflows the buffer |
| 12:52:31 | <Inst> | leary: is this the best intro to parametricity? |
| 12:52:33 | <Inst> | https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf |
| 12:52:49 | × | hgolden__ quits (~hgolden@146.70.173.229) (Ping timeout: 244 seconds) |
| 12:52:51 | × | alexherbo2 quits (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 12:53:10 | → | alexherbo2 joins (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) |
| 12:53:44 | <geekosaur> | (note that, if it's not in a pty, you would have to rewrite ghci to disable output buffering; GNU stdbuf only works with GNU libc's stdio, not Haskell's) |
| 12:54:35 | <geekosaur> | hm, that may mean you still can't get it to stream because in a pty it'll use `LineBuffering` and you can't tell it otherwise) |
| 12:54:54 | <geekosaur> | so yeh, custom ghci build would be needed |
| 12:55:03 | <haskellbridge> | <zwro> geekosaur: strangely, if i don't hFlush or i disable buffering, the process explodes and consumes all my cpu+memory |
| 12:55:29 | <geekosaur> | that sounds like a ghcitui problem |
| 12:55:39 | <haskellbridge> | <zwro> yes |
| 12:55:43 | <geekosaur> | presumably you'd have to rewrite it to stream instead of reading the output all at once |
| 12:56:00 | <geekosaur> | not impossible, just requires some work |
| 12:56:22 | <geekosaur> | (getting it all as a single chunk is the lazy-programmer way 🙂 ) |
| 12:58:12 | <geekosaur> | also I suspect you will run into the problems I described f you do change ghcitui to stream instead of trying to read it all at once |
| 12:58:13 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 13:01:33 | <Leary> | Inst: That's the most notable paper on the subject, but try <http://www.vex.net/~trebla/haskell/abs-type-param.html> first. |
| 13:01:43 | → | hgolden joins (~hgolden@23.162.40.28) |
| 13:01:56 | <Inst> | i hope monochrom doesn't have vex.net/~trebla on highlight? |
| 13:03:04 | <geekosaur> | at most the last part, I suspect, but I have this feeling it would be egoboo 😛 |
| 13:03:54 | × | CoolMa7 quits (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 13:04:20 | → | CoolMa7 joins (~CoolMa7@95.91.137.87) |
| 13:05:24 | → | housemate joins (~housemate@146.70.66.228) |
| 13:07:36 | → | comerijn joins (~merijn@77.242.116.146) |
| 13:11:09 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 13:11:44 | → | pavonia_ joins (~user@user/siracusa) |
| 13:13:04 | × | CoolMa7 quits (~CoolMa7@95.91.137.87) (Ping timeout: 272 seconds) |
| 13:13:22 | <Inst> | well it's deserved, his article's good |
| 13:14:02 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 13:14:27 | × | SlackCoder quits (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 13:15:49 | × | longlongdouble quits (~longlongd@117.234.149.253) (Ping timeout: 260 seconds) |
| 13:15:49 | × | pavonia quits (~user@user/siracusa) (Ping timeout: 260 seconds) |
| 13:15:54 | pavonia_ | is now known as pavonia |
| 13:15:57 | → | longlongdouble joins (~longlongd@117.234.146.164) |
| 13:16:11 | × | housemate quits (~housemate@146.70.66.228) (Read error: Connection reset by peer) |
| 13:24:56 | → | housemate joins (~housemate@146.70.66.228) |
| 13:30:17 | → | CoolMa7 joins (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) |
| 13:30:18 | × | sudden quits (~cat@user/sudden) (Ping timeout: 252 seconds) |
| 13:31:18 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 13:36:30 | × | longlongdouble quits (~longlongd@117.234.146.164) (Ping timeout: 272 seconds) |
| 13:37:58 | → | longlongdouble joins (~longlongd@117.225.100.25) |
| 13:38:50 | → | merijn joins (~merijn@77.242.116.146) |
| 13:39:13 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 13:41:27 | <Inst> | tbh what's the deal with O(ln n) for Haskell sets and maps? |
| 13:41:43 | <Inst> | afaik in other languages you can O(1) access objects |
| 13:41:58 | <kuribas> | Inst: O(ln n) is not much different from O(1). |
| 13:42:02 | → | sudden joins (~cat@user/sudden) |
| 13:42:07 | <kuribas> | Inst: it mostly depends on constant factors. |
| 13:42:20 | <kuribas> | Inst: in any case, it's what you get with immutable structures. |
| 13:42:53 | <kuribas> | most languages depend on mutability to get O(1). Which is itself a lie, since memory access in a CPU is not O(1). |
| 13:43:17 | <Inst> | how do you use mutability to get O(1) access? |
| 13:43:38 | <kuribas> | hashtables use mutation to insert elements. |
| 13:45:12 | <kuribas> | binary trees, which is are usually used in pure datatypes, have log n operations. |
| 13:47:30 | <[exa]> | tbh there are efficient hashy sets and maps even in haskell in https://hackage.haskell.org/package/unordered-containers |
| 13:48:02 | <[exa]> | but don't, the O(1) for hashmaps is a lie |
| 13:48:40 | × | ocra8 quits (ocra8@user/ocra8) (Quit: WeeChat 4.3.4) |
| 13:49:41 | → | weary-traveler joins (~user@user/user363627) |
| 13:50:24 | <kuribas> | Isn't the O(1) for a hashtable also a lie? |
| 13:50:46 | <kuribas> | It's only if the number of buckets is large enough? |
| 13:51:05 | × | housemate quits (~housemate@146.70.66.228) (Ping timeout: 252 seconds) |
| 13:51:26 | <[exa]> | yes it only holds for a completely immutable container prepared with a perfect hash |
| 13:51:34 | <[exa]> | at which point everyone should just use an array and integer index |
| 13:52:49 | × | longlongdouble quits (~longlongd@117.225.100.25) (Ping timeout: 248 seconds) |
| 13:53:17 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 13:53:21 | <[exa]> | for all kinds of mutable hashmaps you usually end up at something like O(log n/loglog n) with an uncanny constant factor and absolutely no chance to get any benefit from the usual computers' caching layers |
| 13:55:31 | <[exa]> | +- the usual consideration of "sometimes it just rehashes in O(n)" |
| 13:57:36 | × | CoolMa7 quits (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 14:02:34 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 14:02:54 | <[exa]> | Inst: anyway re mutability, each hashtable change requires changing a single element in a (potentially big) array. Normally with computers that's very efficient so people can reach the "amortized hashy O(1)" aka O(log/loglog). In haskell it's absolutely not easy unless you either unsafePerformIO or force the user to pull ST or IO through each operation. So people kinda fall back to trees which are |
| 14:02:56 | <[exa]> | usually doing most operations in O(log n). |
| 14:05:22 | <geekosaur> | (historical note: `containers` used to include an `IO`-based hash table. it was removed because its performance was pretty bad. but someone resuscitated it and mostly fixed the performance issues, and now it's in the `hashtables` package IIRC) |
| 14:05:59 | <geekosaur> | (this was long before `unordered-containers`) |
| 14:06:24 | × | notzmv quits (~daniel@user/notzmv) (Ping timeout: 276 seconds) |
| 14:06:33 | → | housemate joins (~housemate@146.70.66.228) |
| 14:07:17 | <geekosaur> | https://downloads.haskell.org/~ghc/6.6.1/docs/html/libraries/base/Data-HashTable.html |
| 14:07:28 | <geekosaur> | wasn't even in `containers`, that didn't exist yet |
| 14:07:56 | <[exa]> | whew cool, they actually did cuckoo hashing |
| 14:09:19 | × | sam113101 quits (~sam@modemcable220.199-203-24.mc.videotron.ca) (Ping timeout: 260 seconds) |
| 14:12:53 | × | housemate quits (~housemate@146.70.66.228) (Ping timeout: 245 seconds) |
| 14:14:24 | → | blover joins (~blover@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) |
| 14:16:34 | → | housemate joins (~housemate@146.70.66.228) |
| 14:19:54 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Read error: Connection reset by peer) |
| 14:21:06 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 14:22:44 | → | Square joins (~Square4@user/square) |
| 14:28:56 | → | CoolMa7 joins (~CoolMa7@95.91.137.87) |
| 14:30:11 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 14:31:06 | → | CoolMa7_ joins (~CoolMa7@128.90.145.4) |
| 14:33:59 | × | CoolMa7 quits (~CoolMa7@95.91.137.87) (Ping timeout: 252 seconds) |
| 14:34:58 | → | CoolMa7 joins (~CoolMa7@128.90.170.13) |
| 14:36:09 | × | CoolMa7_ quits (~CoolMa7@128.90.145.4) (Ping timeout: 260 seconds) |
| 14:38:13 | × | housemate quits (~housemate@146.70.66.228) (Ping timeout: 244 seconds) |
| 14:39:29 | × | CoolMa7 quits (~CoolMa7@128.90.170.13) (Ping timeout: 252 seconds) |
| 14:41:02 | → | CoolMa7 joins (~CoolMa7@128.90.175.3) |
| 14:43:43 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 245 seconds) |
| 14:44:09 | → | euleritian joins (~euleritia@dynamic-176-006-131-038.176.6.pool.telefonica.de) |
| 14:44:42 | → | housemate joins (~housemate@146.70.66.228) |
| 14:49:50 | → | housemate_ joins (~housemate@146.70.66.228) |
| 14:50:54 | × | housemate quits (~housemate@146.70.66.228) (Ping timeout: 260 seconds) |
| 14:54:44 | → | housemate joins (~housemate@146.70.66.228) |
| 14:56:06 | × | housemate_ quits (~housemate@146.70.66.228) (Ping timeout: 252 seconds) |
| 14:56:36 | × | cyphase quits (~cyphase@user/cyphase) (Read error: Connection reset by peer) |
| 14:57:36 | → | cyphase joins (~cyphase@user/cyphase) |
| 14:59:00 | → | housemate_ joins (~housemate@146.70.66.228) |
| 14:59:52 | × | housemate_ quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:00:39 | → | housemate_ joins (~housemate@146.70.66.228) |
| 15:01:39 | × | housemate quits (~housemate@146.70.66.228) (Ping timeout: 276 seconds) |
| 15:02:48 | × | housemate_ quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:03:39 | → | housemate_ joins (~housemate@146.70.66.228) |
| 15:05:27 | <EvanR> | the O(1) O(log n) etc is always subject to a degree of handwaving when applied to real life, where you ignore enough real details so, abstraction activates, and your curve fits |
| 15:06:00 | × | housemate_ quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:06:12 | <EvanR> | like you ignore n so large that you exit the actual ram and enter into cloud storage |
| 15:07:09 | → | housemate_ joins (~housemate@146.70.66.228) |
| 15:07:29 | <EvanR> | godot game engine uses umteen hashtables per second for every little thing and while it's "fast enough" you have to wonder about the cost of all that hashing |
| 15:09:38 | × | housemate_ quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:10:39 | → | housemate_ joins (~housemate@146.70.66.228) |
| 15:11:13 | × | housemate_ quits (~housemate@146.70.66.228) (Remote host closed the connection) |
| 15:11:32 | → | housemate joins (~housemate@146.70.66.228) |
| 15:12:24 | × | housemate quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:12:44 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 15:12:52 | → | housemate joins (~housemate@146.70.66.228) |
| 15:13:09 | × | euleritian quits (~euleritia@dynamic-176-006-131-038.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:13:33 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:13:46 | → | AlexNoo_ joins (~AlexNoo@178.34.160.231) |
| 15:15:14 | × | housemate quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:15:42 | → | housemate joins (~housemate@146.70.66.228) |
| 15:16:13 | × | gentauro quits (~gentauro@user/gentauro) (Ping timeout: 245 seconds) |
| 15:17:00 | × | AlexZenon quits (~alzenon@178.34.150.252) (Ping timeout: 252 seconds) |
| 15:17:33 | × | AlexNoo quits (~AlexNoo@178.34.150.252) (Ping timeout: 252 seconds) |
| 15:18:18 | × | housemate quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:18:18 | → | gentauro joins (~gentauro@user/gentauro) |
| 15:19:00 | → | housemate joins (~housemate@146.70.66.228) |
| 15:19:19 | → | famubu joins (~famubu@14.139.174.50) |
| 15:19:52 | × | housemate quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:20:20 | → | housemate joins (~housemate@146.70.66.228) |
| 15:21:15 | × | housemate quits (~housemate@146.70.66.228) (Remote host closed the connection) |
| 15:23:00 | AlexNoo_ | is now known as AlexNoo |
| 15:23:34 | × | CoolMa7 quits (~CoolMa7@128.90.175.3) (Ping timeout: 260 seconds) |
| 15:26:02 | → | CoolMa7 joins (~CoolMa7@95.91.137.87) |
| 15:26:59 | × | CoolMa7 quits (~CoolMa7@95.91.137.87) (Client Quit) |
| 15:28:11 | → | AlexZenon joins (~alzenon@178.34.160.231) |
| 15:30:58 | × | ubert quits (~Thunderbi@77.119.163.56.wireless.dyn.drei.com) (Ping timeout: 248 seconds) |
| 15:31:04 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 15:31:27 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:36:10 | → | housemate joins (~housemate@146.70.66.228) |
| 15:37:02 | × | housemate quits (~housemate@146.70.66.228) (Max SendQ exceeded) |
| 15:37:32 | → | housemate joins (~housemate@146.70.66.228) |
| 15:39:29 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 15:39:41 | → | euleritian joins (~euleritia@dynamic-176-006-131-038.176.6.pool.telefonica.de) |
| 15:41:44 | → | housemate_ joins (~housemate@146.70.66.228) |
| 15:42:23 | <c_wraith> | hash tables have more assumptions going into those O(1) claims than most data structures. In fact, those assumptions add up to having a bounded key space, in which case you claim any lookup strategy is O(1) |
| 15:42:33 | × | alp quits (~alp@2001:861:e3d6:8f80:4549:4578:5f94:9afe) (Ping timeout: 252 seconds) |
| 15:42:53 | × | housemate quits (~housemate@146.70.66.228) (Ping timeout: 255 seconds) |
| 15:43:34 | → | skylord5816 joins (~skylord58@user/skylord5816) |
| 15:43:57 | × | euleritian quits (~euleritia@dynamic-176-006-131-038.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 15:44:32 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 15:45:15 | → | euleritian joins (~euleritia@dynamic-176-006-128-136.176.6.pool.telefonica.de) |
| 15:48:06 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 15:48:54 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:50:02 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 16:00:30 | → | euphores joins (~SASL_euph@user/euphores) |
| 16:07:29 | × | son0p quits (~ff@186.119.84.155) (Ping timeout: 252 seconds) |
| 16:16:36 | × | housemate_ quits (~housemate@146.70.66.228) (Quit: "I saw it in a tiktok video and thought that it was the most smartest answer ever." ~ AnonOps Radio [some time some place] | I AM THE DERIVATIVE I AM GOING TANGENT TO THE CURVE!) |
| 16:17:28 | → | notzmv joins (~daniel@user/notzmv) |
| 16:17:59 | × | misterfish quits (~misterfis@31-161-39-137.biz.kpn.net) (Ping timeout: 255 seconds) |
| 16:18:05 | → | housemate joins (~housemate@146.70.66.228) |
| 16:19:43 | → | Digitteknohippie joins (~user@user/digit) |
| 16:20:32 | × | Digit quits (~user@user/digit) (Ping timeout: 272 seconds) |
| 16:23:59 | × | poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 252 seconds) |
| 16:24:33 | → | poscat joins (~poscat@user/poscat) |
| 16:34:58 | → | housemate_ joins (~housemate@146.70.66.228) |
| 16:37:05 | × | housemate quits (~housemate@146.70.66.228) (Ping timeout: 248 seconds) |
| 16:38:15 | × | alexherbo2 quits (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 16:38:16 | × | JamesMowery43 quits (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Ping timeout: 272 seconds) |
| 16:39:51 | <merijn> | hashtables are the most overrated datastructure IMHO |
| 16:40:05 | Digitteknohippie | is now known as Digit |
| 16:41:02 | <merijn> | Inst: Bit late, but there's also the issue of 1) memory complexity and 2) avg case vs worst case complexity |
| 16:41:35 | <merijn> | Inst: Haskell's immutable maps use storage linear in number of elements and are O(log n) average *AND* worst case complexity |
| 16:42:28 | <merijn> | Meanwhile hashmaps are O(1) (with sufficient handwaving) average case and O(n) worst case complexity. And you need a pretty decent amount of memory bloat to avoid hitting the O(n) case |
| 16:44:28 | <merijn> | Most people handwave/ignore the cost of computing a hash of the key, handwave the possibility of complexity degradation due to collisions |
| 16:45:50 | → | JamesMowery43 joins (~JamesMowe@ip68-228-212-232.ph.ph.cox.net) |
| 16:46:04 | <Inst> | tbh at O(ln n) and below, I suspect you can easily have performance dominated by constant factors? |
| 16:46:21 | <Inst> | like, seq is more efficient than list asymptotically, but benchmarks show that in many practical case list pulls ahead |
| 16:46:57 | <c_wraith> | The funniest counter-argument I heard to "hashing isn't O(1)" was "it is if you cache it." |
| 16:48:03 | <c_wraith> | Ah. Well. Solving the halting problem is also trivial is you just start with a table of all the answers. |
| 16:50:01 | × | merijn quits (~merijn@77.242.116.146) (Quit: Reconnecting) |
| 16:50:16 | → | merijn joins (~merijn@77.242.116.146) |
| 16:50:49 | <merijn> | Inst: I've used the Haskell map's with 10 thousands of entries in relatively tight loops and the performance was just fine |
| 16:51:14 | <merijn> | Which makes sense, since O(log n) scales insanely well with input size |
| 16:51:51 | <merijn> | Most people really overthink it and there's also a tendency of "I'm used to python/javascript/ruby/whatevr and they use hashmaps for everything, so they must be the best thing you can use!" |
| 16:52:25 | <merijn> | Not to mention that tree based maps like containers come with a bunch of other niceties you don't get with hashmaps |
| 16:52:46 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:53:18 | <merijn> | Like the ability to query "the key closest to X", easy queries for lowest/highest key value, stable and predictable traversal orders (containers guarantees traversal order from least to greatest key/element) |
| 16:58:43 | × | housemate_ quits (~housemate@146.70.66.228) (Remote host closed the connection) |
| 16:59:07 | → | housemate_ joins (~housemate@146.70.66.228) |
| 17:06:08 | × | housemate_ quits (~housemate@146.70.66.228) (Ping timeout: 272 seconds) |
| 17:06:08 | → | housemate joins (~housemate@146.70.66.228) |
| 17:11:05 | <monochrom> | Haha the irony in using caching for hashing. |
| 17:11:09 | → | toch joins (~toch@user/toch) |
| 17:11:26 | <monochrom> | or rather, using caching to speed up hashing |
| 17:14:48 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:15:19 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 17:16:01 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 17:17:21 | × | toch quits (~toch@user/toch) (Ping timeout: 244 seconds) |
| 17:18:17 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 17:32:26 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 17:33:41 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:37:12 | × | housemate quits (~housemate@146.70.66.228) (Quit: "I saw it in a tiktok video and thought that it was the most smartest answer ever." ~ AnonOps Radio [some time some place] | I AM THE DERIVATIVE I AM GOING TANGENT TO THE CURVE!) |
| 17:37:32 | → | CoolMa7 joins (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) |
| 17:40:08 | → | CoolMa7_ joins (~CoolMa7@128.90.175.5) |
| 17:41:54 | × | CoolMa7 quits (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 17:43:18 | → | alp joins (~alp@2001:861:e3d6:8f80:6393:3939:65f3:74c5) |
| 17:49:03 | × | JamesMowery43 quits (~JamesMowe@ip68-228-212-232.ph.ph.cox.net) (Ping timeout: 252 seconds) |
| 17:50:39 | × | blover quits (~blover@2804:7f0:6780:f864:2d9e:2c7d:cab0:69d2) (Ping timeout: 256 seconds) |
| 17:52:20 | → | JamesMowery43 joins (~JamesMowe@ip68-228-212-232.ph.ph.cox.net) |
| 17:53:29 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 17:57:41 | <probie> | Hashmaps also have a great feature where if the hashing algorithm is known, "bad" data can be generated to force the linear time lookup behaviour |
| 18:00:48 | × | CoolMa7_ quits (~CoolMa7@128.90.175.5) (Ping timeout: 246 seconds) |
| 18:05:29 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 18:07:03 | → | caconym joins (~caconym@user/caconym) |
| 18:09:44 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 18:11:44 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:16:55 | → | hgolden_ joins (~hgolden@23.162.40.69) |
| 18:17:44 | <haskellbridge> | <Bowuigi> c_wraith funny enough, cache retrieval is likely not O(1) either |
| 18:18:14 | → | son0p joins (~ff@152.202.37.255) |
| 18:19:08 | × | hgolden quits (~hgolden@23.162.40.28) (Ping timeout: 245 seconds) |
| 18:20:12 | → | housemate joins (~housemate@146.70.66.228) |
| 18:20:13 | <haskellbridge> | <Bowuigi> Perfect hash tables are great, but I wouldn't (ab)use the normal ones |
| 18:21:17 | → | ih1d joins (~ih1d@24.139.109.18) |
| 18:22:47 | × | ih1d quits (~ih1d@24.139.109.18) (Client Quit) |
| 18:23:27 | × | xdminsy quits (~xdminsy@117.147.71.147) (Ping timeout: 252 seconds) |
| 18:24:34 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) |
| 18:24:57 | → | hgolden__ joins (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) |
| 18:25:25 | × | hgolden_ quits (~hgolden@23.162.40.69) (Ping timeout: 248 seconds) |
| 18:25:35 | × | hgolden quits (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) (Remote host closed the connection) |
| 18:25:35 | × | hgolden__ quits (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) (Remote host closed the connection) |
| 18:26:45 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:29:46 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:6c70:1ac0:d127:74dd) |
| 18:32:29 | → | misterfish joins (~misterfis@31-161-39-137.biz.kpn.net) |
| 18:33:13 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:35:06 | → | Square2 joins (~Square@user/square) |
| 18:39:24 | × | Square quits (~Square4@user/square) (Ping timeout: 260 seconds) |
| 18:40:43 | → | benkard joins (~mulk@pd95146e9.dip0.t-ipconnect.de) |
| 18:42:09 | → | spew joins (~spew@135.233.119.40) |
| 18:42:24 | × | mulk quits (~mulk@pd95146e9.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 18:42:24 | benkard | is now known as mulk |
| 18:44:06 | × | spew quits (~spew@135.233.119.40) (Remote host closed the connection) |
| 18:44:21 | → | spew joins (~spew@135.233.119.40) |
| 18:44:56 | → | ih1d joins (~ih1d@24.139.109.18) |
| 18:45:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 18:53:10 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 18:54:10 | <mauke> | probie: not if you put a balanced tree under each bucket! |
| 18:56:59 | × | longlongdouble quits (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 19:01:49 | × | spew quits (~spew@135.233.119.40) (Remote host closed the connection) |
| 19:02:14 | × | son0p quits (~ff@152.202.37.255) (Ping timeout: 255 seconds) |
| 19:03:43 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:05:02 | → | longlongdouble joins (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 19:08:32 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 19:08:39 | × | housemate quits (~housemate@146.70.66.228) (Quit: "I saw it in a tiktok video and thought that it was the most smartest answer ever." ~ AnonOps Radio [some time some place] | I AM THE DERIVATIVE I AM GOING TANGENT TO THE CURVE!) |
| 19:10:38 | <dolio> | Does anyone use the sort of hash tables where you don't put linked lists in each bucket? I was required to learn about those at some point. |
| 19:10:59 | <dolio> | (Or, multiple values in a bucket in general.) |
| 19:11:11 | <c_wraith> | see the earlier note about Cuckoo hashing |
| 19:11:46 | <dolio> | Oh. I've never heard it called that. |
| 19:11:56 | <c_wraith> | well, that's one specific strategy |
| 19:11:58 | <c_wraith> | There are other. |
| 19:12:07 | <c_wraith> | open probing, linear probing, etc |
| 19:12:35 | → | ephilalethes joins (~noumenon@113.51-175-156.customer.lyse.net) |
| 19:12:43 | <tomsmeding> | @tell kuribas tactics are separate from the language, to be sure, but they're written _in_ the language, and you can't "just" use tactics written for coq in agda. In fact, I've never heard of anyone even trying anything in that direction. |
| 19:12:43 | <lambdabot> | Consider it noted. |
| 19:12:50 | → | spew joins (~spew@135.233.119.40) |
| 19:13:07 | → | housemate joins (~housemate@146.70.66.228) |
| 19:13:34 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:13:44 | <dolio> | I see. Cuckoo optimizes for looking up the most recently inserted, basically? |
| 19:13:54 | <dolio> | Instead of first-inserted. |
| 19:16:14 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 19:18:26 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 19:19:54 | → | emfrom joins (~emfrom@37.168.27.131) |
| 19:20:39 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:20:46 | → | ft joins (~ft@p4fc2a216.dip0.t-ipconnect.de) |
| 19:21:34 | × | absence quits (torgeihe@hildring.pvv.ntnu.no) (Ping timeout: 260 seconds) |
| 19:23:25 | → | absence joins (torgeihe@hildring.pvv.ntnu.no) |
| 19:26:14 | × | misterfish quits (~misterfis@31-161-39-137.biz.kpn.net) (Ping timeout: 260 seconds) |
| 19:28:51 | → | CoolMa7 joins (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) |
| 19:29:16 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:29:57 | × | euleritian quits (~euleritia@dynamic-176-006-128-136.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 19:30:15 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 19:34:09 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 19:44:45 | × | notzmv quits (~daniel@user/notzmv) (Read error: Connection reset by peer) |
| 19:45:03 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 19:45:19 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 19:47:11 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 19:47:11 | ljdarj1 | is now known as ljdarj |
| 19:49:41 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 19:51:26 | <ih1d> | anybody know why wiki.haskell.org is down? |
| 19:53:10 | <int-e> | https://status.haskell.org/ says a system upgrade went awry |
| 19:53:20 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 19:53:44 | <tomsmeding> | it's been like that since monday, I think |
| 19:55:25 | <geekosaur> | yes, a mediawiki upgrade blew up, that's the latest I've heard |
| 19:59:35 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 20:00:00 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 20:00:37 | → | caconym joins (~caconym@user/caconym) |
| 20:01:31 | → | tyzef joins (~tyzef@user/tyzef) |
| 20:02:45 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:05:25 | × | tmr quits (~tamer@5.2.74.82) (Changing host) |
| 20:05:25 | → | tmr joins (~tamer@user/tamer) |
| 20:07:24 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:08:47 | → | weary-traveler joins (~user@user/user363627) |
| 20:13:48 | × | tyzef quits (~tyzef@user/tyzef) (Quit: WeeChat 3.8) |
| 20:17:30 | → | tremon joins (~tremon@83.80.159.219) |
| 20:18:08 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:19:46 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 20:19:57 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit) |
| 20:23:14 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 20:27:28 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 20:27:33 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 20:35:39 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 20:36:43 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:43:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 20:46:58 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 20:47:02 | → | Sgeo__ joins (~Sgeo@user/sgeo) |
| 20:47:26 | × | Sgeo_ quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 20:51:49 | × | briandaed quits (~root@185.234.210.211) (Ping timeout: 260 seconds) |
| 20:54:47 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 20:58:59 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 20:59:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 21:03:18 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:05:18 | → | Square joins (~Square4@user/square) |
| 21:06:08 | × | emfrom quits (~emfrom@37.168.27.131) (Remote host closed the connection) |
| 21:08:11 | × | benjaminl quits (~benjaminl@user/benjaminl) (Read error: Connection reset by peer) |
| 21:08:26 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 21:08:50 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 21:08:54 | × | Square2 quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 21:12:06 | × | ephilalethes quits (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 21:12:32 | → | sprotte24 joins (~sprotte24@p200300d16f05e000c862cdd7b290d75c.dip0.t-ipconnect.de) |
| 21:12:59 | → | son0p joins (~ff@186.121.30.70) |
| 21:13:08 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:18:00 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 21:18:39 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 21:20:52 | × | tremon quits (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 21:21:09 | × | son0p quits (~ff@186.121.30.70) (Ping timeout: 260 seconds) |
| 21:21:21 | × | famubu quits (~famubu@14.139.174.50) (Ping timeout: 248 seconds) |
| 21:28:31 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:37:12 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 21:43:34 | <monochrom> | Derp. I am taking a look at free applicative functors (e.g. https://hackage.haskell.org/package/free-5.2/docs/Control-Applicative-Free.html), I try to implement <*> myself, get stuck, look at the answer, it is obvious (it is the same trick as fmap, and I could do fmap). |
| 21:44:06 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 21:44:10 | × | infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 272 seconds) |
| 21:45:21 | → | rvalue- joins (~rvalue@user/rvalue) |
| 21:46:21 | <tomsmeding> | monochrom: is there a good reason the first field of that Ap doesn't have an Ap around it? |
| 21:46:36 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 276 seconds) |
| 21:47:00 | <monochrom> | I don't know! I'm just learning. :) |
| 21:47:39 | <monochrom> | Supposedly f has to be actually relevant somewhere rather than being a phantom type. |
| 21:48:00 | <monochrom> | and it can't be in Pure so it may as well be in the recursive case. |
| 21:48:30 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 21:49:33 | <tomsmeding> | monochrom: if you wanna laugh, look at the implementation of runAp -- and in particular the naming of the fields of Ap |
| 21:50:08 | <tomsmeding> | f :: f a ; x :: Ap f (a -> b) |
| 21:50:15 | <monochrom> | Oh I think I see it. It is trying to have a list like [x0 :: f A0, x1 :: f (A0 -> A1), x2 :: f (A1 -> A2)]. |
| 21:51:08 | <monochrom> | Haha. "Let e be a group, H be its identity element, phi be a subgroup of e, G be a group homomorphism from e to f" |
| 21:51:13 | rvalue- | is now known as rvalue |
| 21:51:20 | <tomsmeding> | :D |
| 21:51:37 | <tomsmeding> | I mean, I kind of get it -- we have a value in a functor (call it f), and we have a value of our data type (call it x) |
| 21:51:47 | <tomsmeding> | it's just that juxtaposing the two makes it kind of funny |
| 21:52:26 | <monochrom> | I thought up my own field names "Ap f_secret cont", where f_secret :: f s, cont :: Ap f (s -> a). |
| 21:52:29 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:53:24 | <tomsmeding> | monochrom: the remark about the "list" is quite apt |
| 21:53:39 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 21:54:22 | <monochrom> | Your question inspired me to actually think about it. :) |
| 21:54:25 | <tomsmeding> | and that makes sense: a free monad also normalises out the association order of binds, so analogously, a free applicative should also normalise out the association order of (<*>) |
| 21:54:54 | → | Everything joins (~Everythin@178-133-1-121.mobile.vf-ua.net) |
| 21:55:15 | tomsmeding | . o O ( this module actually has an informative Portability metadata field ) |
| 21:55:51 | <monochrom> | Yeah, free monad tries to have f (f (f ... (f (Pure x)...) |
| 21:56:53 | <monochrom> | which is just waiting to be interpreted/collapsed by a custom-made join :: f (f a) -> f a |
| 21:57:23 | <tomsmeding> | where the top-level `f` computation computes a result, which is already applied to its continuation to produce the computation to run next |
| 21:57:56 | <tomsmeding> | s/which is already applied to/to which is already applied/ |
| 21:58:12 | <tomsmeding> | can't "apply" be commutative -.- |
| 21:58:38 | <monochrom> | Like f x = x f ? >:) |
| 21:58:43 | <tomsmeding> | :D |
| 21:58:45 | <tomsmeding> | yes |
| 22:02:32 | <tomsmeding> | monochrom: that list is not quite what's happening though. It's rather Ap f z ~= [f a, f b, f c, c -> b -> a -> z] |
| 22:02:53 | <monochrom> | Oh oops, yeah. |
| 22:02:53 | <tomsmeding> | (when carefully expanding the data type) |
| 22:03:13 | <tomsmeding> | and that makes more sense: it's just liftA n! |
| 22:03:44 | <tomsmeding> | then it's also clear how this "just" normalises out the (<*>) association order |
| 22:03:51 | <monochrom> | Oh there is the variadic liftAn my students are looking for! |
| 22:04:15 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:04:19 | <tomsmeding> | point them to Control.Applicative.Free next time >:) |
| 22:04:25 | <tomsmeding> | they'll sure be thankful |
| 22:04:38 | <monochrom> | "but it requires you to learn GADTs" >:) |
| 22:04:53 | → | infinity0 joins (~infinity0@pwned.gg) |
| 22:05:02 | <tomsmeding> | now you know what would be nice? If this listy interpretation was there in the documentation. |
| 22:05:15 | <tomsmeding> | it makes the whole thing obvious all at once |
| 22:06:01 | <tomsmeding> | (there's likely some alternative interpretation of this particular formulation of Ap that corresponds with some mathematical perspective on applicative functors) |
| 22:06:07 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:06:32 | <monochrom> | Nah the documentation is like "we are high brow, this is obvious from working out the left adjoint of the forgetful functor" |
| 22:08:06 | <tomsmeding> | it would also help if Ap was just flipped |
| 22:08:32 | <tomsmeding> | I mean, I get the parallel with (>>=), but come on, you're working in Haskell, and in Haskell, (<*>) is flipped |
| 22:08:55 | <tomsmeding> | I feel like I would have spotted the "this is liftAn" faster then too |
| 22:09:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 22:09:37 | <tomsmeding> | hm, perhaps not |
| 22:10:36 | <tomsmeding> | yes, because then it looks like a symbolic function applied to an argument inside f |
| 22:10:46 | × | alp quits (~alp@2001:861:e3d6:8f80:6393:3939:65f3:74c5) (Remote host closed the connection) |
| 22:10:49 | <tomsmeding> | but you still have to do the mental induction, I guess |
| 22:12:25 | <tomsmeding> | so actually "Ap f x" are good variable names, just for `flip Ap`, not for `Ap` :D |
| 22:13:23 | <tomsmeding> | yes, clearly Ed was wrong. |
| 22:13:43 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 22:13:49 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 22:20:03 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:21:50 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 22:22:03 | → | jero98772 joins (~jero98772@2800:484:1d7c:cc00::1) |
| 22:22:11 | × | michalz quits (~michalz@185.246.207.221) (Remote host closed the connection) |
| 22:24:24 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 22:27:04 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 22:31:47 | <monochrom> | Haha this is probably a consequence of quicklook impredicativity. I have "foo :: (forall x. ...) -> ()" for example (in general a rank-2+ type sig), then I can't have "foo = undefined" if I want a TODO stub, I have to write at least "foo _ = undefined". |
| 22:32:37 | <tomsmeding> | monochrom: is "foo = undefined" accepted if you turn on -XImpredicativeTypes? |
| 22:33:06 | <monochrom> | I haven't tried. I only have GADTs and GHC2021 (I think it includes RankNTypes). |
| 22:33:29 | <tomsmeding> | (I would rather expect it the other round: instantiating 'undefined' with a type containing foralls could be _permissible due to_ quicklook) |
| 22:33:35 | <tomsmeding> | it certainly was disallowed before :) |
| 22:33:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:33:46 | <monochrom> | Oh wait, it's shallow vs deep subsumption. |
| 22:34:06 | <geekosaur> | -XDeepSubsumption if your ghc is new enough |
| 22:34:42 | <tomsmeding> | -XImpredicativeTypes also works :> |
| 22:35:02 | <tomsmeding> | and -XDeepSubsumption does not! |
| 22:35:10 | <tomsmeding> | https://play.haskell.org/saved/Qtf5WYqV |
| 22:35:42 | <monochrom> | Right yeah. |
| 22:35:53 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 22:35:53 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Read error: Connection reset by peer) |
| 22:35:53 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 22:36:16 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 22:36:19 | → | califax joins (~califax@user/califx) |
| 22:36:35 | → | gmg joins (~user@user/gehmehgeh) |
| 22:38:07 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:43:42 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 22:44:50 | × | Leary quits (~Leary@user/Leary/x-0910699) (Remote host closed the connection) |
| 22:46:13 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 22:53:54 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:54:24 | → | famubu joins (~famubu@14.139.174.50) |
| 22:58:04 | × | Everything quits (~Everythin@178-133-1-121.mobile.vf-ua.net) (Remote host closed the connection) |
| 22:58:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:00:45 | → | notzmv joins (~daniel@user/notzmv) |
| 23:04:34 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 23:04:38 | → | pnotequalnp joins (~pnotequal@user/pnotequalnp) |
| 23:06:47 | <yin> | this is fun!: i have a bidirectional pattern synonym and try to use record update syntax like `MyPattern { x = ... }` i can get the error `constructor MyPattern does not have field 'x'` |
| 23:07:10 | <yin> | the solution: `(MyPattern) { x = ... }` |
| 23:07:46 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 23:07:47 | ljdarj1 | is now known as ljdarj |
| 23:08:19 | × | xff0x quits (~xff0x@2405:6580:b080:900:759a:e3d6:c0c3:b78a) (Ping timeout: 260 seconds) |
| 23:08:24 | <yin> | this feels kind of lispy |
| 23:09:42 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:10:51 | <yin> | also feels like PatternSynonyms could be patched to allow the former |
| 23:11:07 | → | pnotequalnp44 joins (~pnotequal@user/pnotequalnp) |
| 23:11:57 | × | pnotequalnp quits (~pnotequal@user/pnotequalnp) (Ping timeout: 256 seconds) |
| 23:13:02 | → | pavonia joins (~user@user/siracusa) |
| 23:13:49 | × | pnotequalnp44 quits (~pnotequal@user/pnotequalnp) (Client Quit) |
| 23:15:00 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 23:21:07 | → | xff0x joins (~xff0x@2405:6580:b080:900:759a:e3d6:c0c3:b78a) |
| 23:21:18 | → | supercode joins (~supercode@user/supercode) |
| 23:23:29 | × | CoolMa7 quits (~CoolMa7@ip5f5b8957.dynamic.kabel-deutschland.de) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 23:23:46 | × | supercode quits (~supercode@user/supercode) (Client Quit) |
| 23:25:29 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:30:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 23:31:59 | → | son0p joins (~ff@186.121.30.70) |
| 23:32:34 | <c_wraith> | that definitely sounds like a feature it should have. |
| 23:32:54 | <c_wraith> | If it allows you to create a record pattern, it should use the same syntax as a record pattern... |
| 23:33:05 | <monochrom> | To me it feels like kind of CPP. "#define add(x,y) ((x)+(y))" :) |
| 23:33:49 | <monochrom> | PPP = pattern pre-processor >:) |
| 23:36:51 | <geekosaur> | record update syntax is a bit weird |
| 23:37:38 | <c_wraith> | like at the parser level? |
| 23:37:41 | <monochrom> | It's probably a simple oversight in the parser. |
| 23:38:00 | → | Leary joins (~Leary@user/Leary/x-0910699) |
| 23:39:37 | <geekosaur> | yeh, it's probably missing a case for patsyns so it makes you fall into the parenthesized expression case |
| 23:42:09 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:44:33 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 23:44:34 | <geekosaur> | they left |
| 23:44:38 | <geekosaur> | whoops |
| 23:47:13 | <geekosaur> | anyway it sounds like someone should file a bug on gitlab |
| 23:50:57 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:57:10 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
All times are in UTC on 2024-11-07.