IRCBrowse

2022/03/08

2022-03-08 00:01:08 +0100zeenk(~zeenk@2a02:2f04:a30d:1300:51a3:bcfc:6cda:9fc5) (Quit: Konversation terminated!)
2022-03-08 00:03:35 +0100 <anon04088520> ok
2022-03-08 00:04:17 +0100InstX1_(~Liam@2601:6c4:4080:3f80:b5e9:14a0:500e:3e39)
2022-03-08 00:06:01 +0100burnsidesLlama(~burnsides@rrcs-76-81-82-250.west.biz.rr.com)
2022-03-08 00:07:04 +0100Topsi(~Tobias@dyndsl-095-033-017-136.ewe-ip-backbone.de) (Read error: Connection reset by peer)
2022-03-08 00:08:00 +0100mreh(~mreh@2a00:23c7:2803:ef00:d01b:c280:b64b:b893)
2022-03-08 00:09:19 +0100mrehmreh_
2022-03-08 00:10:14 +0100 <mreh_> What is there difference between the types in this error message?
2022-03-08 00:10:15 +0100 <mreh_> Couldn't match type ‘[S.PhotoT (QExpr Postgres s0)]’
2022-03-08 00:10:15 +0100 <mreh_>                      with ‘forall s'. [S.PhotoT (QExpr Postgres s')]’
2022-03-08 00:10:57 +0100 <hpc> rank
2022-03-08 00:10:59 +0100 <mreh_> Is the s not the same in all the elements in the list?
2022-03-08 00:11:44 +0100 <hpc> s0 is part of a larger scope than s'
2022-03-08 00:12:10 +0100 <hpc> s' is introduced right at the list, and s0 is introduced somewhere further out that's not communicated in that error
2022-03-08 00:15:18 +0100CiaoSen(~Jura@p200300c95737a2002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2022-03-08 00:15:59 +0100 <mreh_> I can't work out where s' is introduced, all the functions I'm using to construct values of S.PhotoT... all have forall s. in their type.
2022-03-08 00:16:26 +0100motherfsck(~motherfsc@user/motherfsck) (Quit: quit)
2022-03-08 00:18:20 +0100 <hpc> s' is introduced by that forall right there in the error
2022-03-08 00:18:30 +0100 <hpc> :P
2022-03-08 00:20:33 +0100daemonises(uid545329@id-545329.uxbridge.irccloud.com)
2022-03-08 00:23:39 +0100acidjnk(~acidjnk@p200300d0c7049f37592e4ec9ecef3fab.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
2022-03-08 00:31:15 +0100mreh_(~mreh@2a00:23c7:2803:ef00:d01b:c280:b64b:b893) (Ping timeout: 256 seconds)
2022-03-08 00:32:32 +0100stefan-_(~cri@42dots.de) (Ping timeout: 240 seconds)
2022-03-08 00:36:57 +0100stefan-_(~cri@42dots.de)
2022-03-08 00:39:01 +0100anon04088520(~anon04088@host-92-19-97-204.as13285.net) (Remote host closed the connection)
2022-03-08 00:39:19 +0100anon04088520(~anon04088@host-92-19-97-204.as13285.net)
2022-03-08 00:40:58 +0100justsomeguy(~justsomeg@user/justsomeguy) (Quit: WeeChat 3.4)
2022-03-08 00:43:43 +0100anon04088520(~anon04088@host-92-19-97-204.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 00:44:51 +0100fluxit(~fluxit@techsmix.net) (Quit: Bye!)
2022-03-08 00:45:38 +0100anon04088520(~anon04088@host-92-19-97-204.as13285.net)
2022-03-08 00:49:35 +0100texasmynsted(~texasmyns@99.96.221.112) (WeeChat 3.4)
2022-03-08 00:49:57 +0100anon04088520(~anon04088@host-92-19-97-204.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 00:50:51 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net)
2022-03-08 00:52:09 +0100chenqisu1(~chenqisu1@183.217.201.47)
2022-03-08 00:53:47 +0100 <worldhelloworld> Really struggling to conceptualize folds when traversing a list - could barely define a takeWhile in terms of foldr, but can't for the life of me, conceptualize a dropWhile in terms of fold :(
2022-03-08 00:55:25 +0100 <dminuoso> Can you share your version of takeWhile perhaps?
2022-03-08 00:55:32 +0100shailangsa(~shailangs@host86-186-133-59.range86-186.btcentralplus.com)
2022-03-08 00:55:32 +0100 <worldhelloworld> Sure
2022-03-08 00:55:50 +0100 <worldhelloworld> `takeWhile'' f = foldr (\x acc -> if f x then x:acc else []) []`
2022-03-08 00:57:27 +0100vorpuni(~pvorp@2001:861:3881:c690:a396:9946:d0cf:5cc0) (Remote host closed the connection)
2022-03-08 01:01:31 +0100 <worldhelloworld> scanr helped a bit with coming up with the definition, but for dropWhile finding it difficult .... been 3 days now lol
2022-03-08 01:02:20 +0100liz_(~liz@2a00:23c5:9680:501:b62e:99ff:fee4:47fa)
2022-03-08 01:04:59 +0100 <Axman6> worldhelloworld: so, acc can be a function, it doesn't have to be another list, so you can pass arguments to it. if you could pass in whether you've finished dropping and then not drop any more that might work
2022-03-08 01:05:27 +0100 <Axman6> (this isn't a function I've written myself, at least not for a very long time so not too sure about that)
2022-03-08 01:07:04 +0100 <worldhelloworld> @Axman6 `acc` is the accumulator - the one which holds the result after successive operations in fold ..... it's already inside the anonymous function .... not sure what you mean
2022-03-08 01:07:04 +0100 <lambdabot> Unknown command, try @list
2022-03-08 01:07:30 +0100worldhelloworld1(uid543174@id-543174.helmsley.irccloud.com)
2022-03-08 01:07:43 +0100 <geekosaur> try not thinking of it as an accumulator but as a state which sometimes gets used as an accumulator
2022-03-08 01:08:46 +0100 <Axman6> yes, acc can have any type you want
2022-03-08 01:08:55 +0100 <liz_> :t foldr
2022-03-08 01:08:56 +0100 <lambdabot> Foldable t => (a -> b -> b) -> b -> t a -> b
2022-03-08 01:09:11 +0100 <Axman6> % :t foldr @[]
2022-03-08 01:09:11 +0100 <yahb> Axman6: (a -> b -> b) -> b -> [a] -> b
2022-03-08 01:09:47 +0100 <liz_> so b can be any type you like, including a function
2022-03-08 01:10:37 +0100machinedgod(~machinedg@24.105.81.50) (Ping timeout: 240 seconds)
2022-03-08 01:12:56 +0100 <geekosaur> it can also for example be a tuple, if you need to carry around moe than one thing
2022-03-08 01:13:09 +0100 <geekosaur> *more
2022-03-08 01:13:50 +0100 <liz_> i sometimes use tuples for simple state which is then discarded by whatever function is using the fold
2022-03-08 01:16:30 +0100 <liz_> i had an [Int] -> [Int] fold that used a tuple, bin2int = fst $ foldr (\b (n,pow) -> (n+b*pow,2*pow)) (0,1)
2022-03-08 01:18:28 +0100 <worldhelloworld> I am not sure how to think of it in terms of state tbh - I don't think the hutton book has such examples that I can remember
2022-03-08 01:20:51 +0100 <worldhelloworld> but if one were to think in terms of accumulators, just for curiosity, is the dropWhile easy to grasp? Or am I struggling more than normal? Just trying to gauge my understanding
2022-03-08 01:20:54 +0100lavaman(~lavaman@98.38.249.169)
2022-03-08 01:21:44 +0100 <janus> what are people's opinions on upgrading packages in anticipation of the release of a dependency? for example, does it make sense to make a package compatible with ghc 9.2 even though it relies on cryptonite?
2022-03-08 01:22:08 +0100 <janus> i could appreciate the argument that since it hasn't actaully been run, one shouldn't claim compatibility
2022-03-08 01:23:20 +0100 <hpc> if you think only in terms of the semantics of the version numbers, it's a valid thing to do
2022-03-08 01:23:27 +0100 <hpc> i personally wouldn't do it, for the very reason you mention
2022-03-08 01:23:59 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 01:24:02 +0100 <janus> for cryptonite, there are PRs open that patch cryptonite to make it compatible. but when i see people overriding dependencies in comitted code, it makes me cringe
2022-03-08 01:24:33 +0100InstX1_(~Liam@2601:6c4:4080:3f80:b5e9:14a0:500e:3e39) (Ping timeout: 250 seconds)
2022-03-08 01:24:34 +0100 <hpc> maybe you can test against those PRs?
2022-03-08 01:24:36 +0100 <janus> i don't like comitting references to "replaced" dependencies because that code becomes stale as soon as the "real" upgrade happens
2022-03-08 01:25:08 +0100 <hpc> if the PRs would be a minor version bump i think you're in the clear
2022-03-08 01:25:26 +0100 <janus> hpc: what do you mean by testing? i am referring to stuff like this https://github.com/aesiniath/http-streams/pull/130/files
2022-03-08 01:25:31 +0100 <hpc> and if it breaks after you can make your own updates to fix it
2022-03-08 01:26:05 +0100 <hpc> build it yourself with those PRs merged in, and test against that
2022-03-08 01:26:12 +0100 <hpc> however you test your package
2022-03-08 01:26:42 +0100 <janus> right, i also think that it is a useful compromise to test with source-repository-package, but *not* commit that override
2022-03-08 01:26:43 +0100 <hpc> a "what-if" build of the dependencies, as it were
2022-03-08 01:27:18 +0100 <janus> my problem is that the PR description then becomes more complicated, since you have to explain to the repo owner how to 'override' the dependency and the anticipation and so on...
2022-03-08 01:27:43 +0100 <hpc> only if they want to use those PRs
2022-03-08 01:28:09 +0100 <hpc> otherwise the constraints of the released cryptonite package prevent using 9.2 anyway i assume?
2022-03-08 01:28:49 +0100 <hpc> so pre-loosening the constraints doesn't break things in the now
2022-03-08 01:28:51 +0100 <janus> yeah, the currently released cryptonite is unbuildable on 9.2 due to it's dependency on memory/foundation
2022-03-08 01:28:56 +0100 <hpc> and this testing is just to prove it won't break things in the future
2022-03-08 01:29:26 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net) (Read error: Connection reset by peer)
2022-03-08 01:29:35 +0100 <janus> it becomes even more involved with CI integration, because i speculate that some people don't want to merge code that isn't being exercised in CI
2022-03-08 01:29:39 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net)
2022-03-08 01:29:53 +0100 <janus> so they wouldn't merge a bytestring bump that allows 0.11 until 9.2 is exercised on CI...
2022-03-08 01:32:26 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net)
2022-03-08 01:33:02 +0100 <janus> hpc: what do you mean by "only if they want to use those PRs"? let's say the PR allows bytestring 0.11. would 'using the PR' mean compiling with GHC 9.2? and you're saying it could be allowed by the bounds even though overriden dependencies are not committed?
2022-03-08 01:34:10 +0100 <worldhelloworld> The way that book describes fold is in two ways 1) Replacing the cons operator by the function 2) The accumulator value method , taking the head and processing recursively ....... Is there another way to think about folds?
2022-03-08 01:34:30 +0100unyu(~pyon@user/pyon) (Quit: WeeChat 3.4)
2022-03-08 01:34:33 +0100 <hpc> janus: it would mean they did the same thing you did
2022-03-08 01:34:50 +0100 <hpc> doing their own build of that dependency with some stuff changed from what's on hackage
2022-03-08 01:35:24 +0100alMalsamolumberjack123
2022-03-08 01:36:08 +0100 <hpc> (which you don't need to support in your package, they're taking on the making-it-work burden themselves when they do that)
2022-03-08 01:37:18 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net) (Ping timeout: 272 seconds)
2022-03-08 01:37:23 +0100tommd(~tommd@97-120-41-123.ptld.qwest.net)
2022-03-08 01:38:23 +0100 <monochrom> There is no other way. In fact the second way is just a lousier way to say the first.
2022-03-08 01:39:04 +0100 <hpc> worldhelloworld: the first way generalizes way better too
2022-03-08 01:39:06 +0100 <hpc> :t maybe
2022-03-08 01:39:07 +0100 <lambdabot> b -> (a -> b) -> Maybe a -> b
2022-03-08 01:39:19 +0100 <hpc> worldhelloworld: maybe is just "replacing the Just" and "replacing the Nothing"
2022-03-08 01:39:25 +0100 <hpc> :t either
2022-03-08 01:39:26 +0100 <lambdabot> (a -> c) -> (b -> c) -> Either a b -> c
2022-03-08 01:39:28 +0100 <hpc> etc
2022-03-08 01:39:40 +0100 <monochrom> The first way though still has the problem of leaving it ambiguous what happens to infinite list.
2022-03-08 01:40:18 +0100 <hpc> it's not ambiguous
2022-03-08 01:40:39 +0100 <hpc> it just does whatever an infinite chain of that function would do
2022-03-08 01:40:45 +0100 <monochrom> Well, I was being charitable.
2022-03-08 01:40:53 +0100 <hpc> :P
2022-03-08 01:41:03 +0100 <Axman6> worldhelloworld: is this homework?
2022-03-08 01:41:07 +0100ishutin(~ishutin@92-249-150-139.static.digikabel.hu) (Ping timeout: 272 seconds)
2022-03-08 01:41:20 +0100 <Axman6> the dropWhile thing
2022-03-08 01:41:33 +0100 <monochrom> Read literally, it implies that if you have infinitely many cons, then there is infinitely much work to be done.
2022-03-08 01:41:37 +0100 <worldhelloworld> @axman6 - no trying to solve it for myself, got done with Uni way back
2022-03-08 01:41:37 +0100 <lambdabot> Unknown command, try @list
2022-03-08 01:41:52 +0100 <Axman6> ok, great, means we can be a bit more helpful
2022-03-08 01:42:13 +0100 <monochrom> which is incompatible with how things unfold (pun!) in Haskell
2022-03-08 01:42:17 +0100ishutin(~ishutin@92-249-193-65.pool.digikabel.hu)
2022-03-08 01:43:09 +0100 <hpc> monochrom: that is only the case strictly speaking (more pun!)
2022-03-08 01:43:33 +0100 <worldhelloworld> the problem I have trying to conceptualise fold with replacing cons (:) operator is how does one know which side of the cons operator goes where in ... say an anonymous function (\a b -> do something)
2022-03-08 01:43:57 +0100 <hpc> worldhelloworld: give that lambda a name - say, f
2022-03-08 01:44:10 +0100 <hpc> worldhelloworld: now you have your list, a : (b : c)
2022-03-08 01:44:11 +0100 <Axman6> @msg lambdabot > let everySecond xs = (foldr (\a acc keep -> if keep then a : acc (not keep) else acc (not keep)) (\_keep -> []) xs) True in everySecond [1..10]
2022-03-08 01:44:12 +0100 <lambdabot> Not enough privileges
2022-03-08 01:44:14 +0100 <Axman6> uh
2022-03-08 01:44:23 +0100 <monochrom> x:xs = (:) x xs. Replace that (:) there. Not ambiguous.
2022-03-08 01:44:29 +0100 <hpc> worldhelloworld: after you fold, it becomes a `f` (b `f` c)
2022-03-08 01:44:38 +0100 <Axman6> Well good thing I got that right on the first try!
2022-03-08 01:44:45 +0100 <Axman6> > let everySecond xs = (foldr (\a acc keep -> if keep then a : acc (not keep) else acc (not keep)) (\_keep -> []) xs) True in everySecond [1..10]
2022-03-08 01:44:46 +0100 <lambdabot> [1,3,5,7,9]
2022-03-08 01:44:53 +0100 <monochrom> Therefore, after replacement, (\a b -> do something) x xs. You do the math.
2022-03-08 01:45:11 +0100unyu(~pyon@user/pyon)
2022-03-08 01:45:23 +0100 <Axman6> worldhelloworld: here's an example of using foldr where acc is a function
2022-03-08 01:45:49 +0100 <Axman6> :t foldr `asAppliedTo` (\a acc keep -> if keep then a : acc (not keep) else acc (not keep))
2022-03-08 01:45:50 +0100 <lambdabot> Foldable t => (a -> (Bool -> [a]) -> Bool -> [a]) -> (Bool -> [a]) -> t a -> Bool -> [a]
2022-03-08 01:46:11 +0100 <monochrom> Err "x:xs" is a bad example.
2022-03-08 01:46:12 +0100 <Axman6> % :t foldr @[] `asAppliedTo` (\a acc keep -> if keep then a : acc (not keep) else acc (not keep)) -- to make the type a little simpler
2022-03-08 01:46:12 +0100 <yahb> Axman6: ; <interactive>:1:11: error: Variable not in scope: asAppliedTo :: ((a0 -> b0 -> b0) -> b0 -> [a0] -> b0) -> (a1 -> (Bool -> [a1]) -> Bool -> [a1]) -> t
2022-03-08 01:46:42 +0100 <monochrom> x : y : z : [] = (:) x ((:) y ((:) z [])). Replace all those (:)s there.
2022-03-08 01:47:02 +0100 <Axman6> urgh - mniip can we get asAppliedTo, asTypeOf etc added to yahb? they're so useful in here
2022-03-08 01:47:39 +0100 <monochrom> (\a b -> do something) x ((\a b -> do something) y ((\a b -> do something) z ???))...) where ??? is whatever replaces [].
2022-03-08 01:48:31 +0100 <dibblego> (:) is right-associative, add parens if it helps
2022-03-08 01:48:43 +0100 <hpc> worldhelloworld: by the way, take all of these examples and put them into a file and format it
2022-03-08 01:49:02 +0100 <hpc> irc is not an ideal medium for these sorts of code snippets
2022-03-08 01:49:26 +0100GIngeh(~GIngeh@203.62.28.64)
2022-03-08 01:49:27 +0100 <hpc> (formatting will probably include breaking out parts of it and giving them names)
2022-03-08 01:49:28 +0100 <worldhelloworld> good idea ... my brain is unable to process it right now
2022-03-08 01:49:44 +0100 <hpc> (names make all code better, even if they're just a b c)
2022-03-08 01:50:59 +0100 <worldhelloworld> yea, easier to understand for the mental model
2022-03-08 01:51:02 +0100 <GIngeh> @pl (\target -> listToMaybe . map (\[x,y] -> (x,y)) . filter (\x -> sum x == target) . combinations 2)
2022-03-08 01:51:02 +0100 <lambdabot> (line 1, column 33):
2022-03-08 01:51:02 +0100 <lambdabot> unexpected "["
2022-03-08 01:51:02 +0100 <lambdabot> expecting pattern
2022-03-08 01:52:16 +0100 <GIngeh> @pl \target -> listToMaybe . map (\ [x,y] -> (x,y)) . filter (\x -> sum x == target) . combinations 2
2022-03-08 01:52:16 +0100 <lambdabot> (line 1, column 33):
2022-03-08 01:52:16 +0100 <lambdabot> unexpected "["
2022-03-08 01:52:16 +0100 <lambdabot> expecting pattern
2022-03-08 01:52:49 +0100cynomys(~cynomys@user/cynomys)
2022-03-08 01:53:25 +0100cynomys(~cynomys@user/cynomys) (Client Quit)
2022-03-08 01:53:36 +0100 <geekosaur> you can't really make that part pointfree
2022-03-08 01:53:37 +0100 <Axman6> > let everySecond xs = (foldr (\a acc keep -> if keep then a : acc (not keep) else acc (not keep)) (\_keep -> []) {- <- this is acc -} xs {- <- this provedes each a -}) True {- <- this is the inital keep -} in everySecond [1..10] -- worldhelloworldthis might be useful to study, with comments added now
2022-03-08 01:53:39 +0100 <lambdabot> [1,3,5,7,9]
2022-03-08 01:54:10 +0100 <worldhelloworld> It's funny because i picked up the recursive cases really fast, but folds just got to me
2022-03-08 01:54:19 +0100 <worldhelloworld> hmm will note it down
2022-03-08 01:54:31 +0100 <Axman6> @pl \target -> listToMaybe . map (\ xs -> (xs!!0,xs!!1)) . filter (\x -> sum x == target) . combinations 2 -- hack for pl?
2022-03-08 01:54:31 +0100 <lambdabot> ((listToMaybe . map (liftM2 (,) (!! 0) (!! 1))) .) . (. combinations 2) . filter . (. sum) . (==)
2022-03-08 01:55:03 +0100vysn(~vysn@user/vysn)
2022-03-08 01:55:04 +0100 <geekosaur> maybe hork instead of hack :þ
2022-03-08 01:55:12 +0100 <liz_> lambdabot can do eta reduction? :o
2022-03-08 01:55:20 +0100 <geekosaur> then again hat describes most of pl's output
2022-03-08 01:56:04 +0100 <Axman6> worldhelloworld: the thing to take note of is the function we give to foldr here is taking three things: the current value in the list, what to do next, and some state that is uses, and passes on, to decide what to do with this particular a
2022-03-08 01:56:09 +0100 <monochrom> If you understand recursion, you can understand foldr by using recursion to reinvent it yourself.
2022-03-08 01:56:39 +0100 <hpc> to some extent, foldr /is/ recursion for lists
2022-03-08 01:56:43 +0100 <Axman6> liz_: pl is short for pointless, a pun on making things pointfree, because it often doesn't improve code at all
2022-03-08 01:57:02 +0100 <GIngeh> oh lord
2022-03-08 01:57:04 +0100 <hpc> but that's a whole other thing ;)
2022-03-08 01:57:06 +0100 <GIngeh> yeah I'm not gonna bother trying to use that
2022-03-08 01:57:08 +0100 <Axman6> hpc: to some extent, or it is univeral?
2022-03-08 01:57:11 +0100 <dibblego> > foldr (++) [] [[1,2,3], [4,5,6]] -- insert (++) in every (:) and [] in []
2022-03-08 01:57:12 +0100 <lambdabot> [1,2,3,4,5,6]
2022-03-08 01:57:22 +0100 <worldhelloworld> @monochrom thanks for making me feel I don't even understand recursion :P
2022-03-08 01:57:22 +0100 <lambdabot> Unknown command, try @list
2022-03-08 01:57:23 +0100 <hpc> Axman6: to the entire extent :P
2022-03-08 01:57:29 +0100 <Axman6> :)
2022-03-08 01:57:50 +0100GIngehGingeh
2022-03-08 01:57:59 +0100Gingeh(~GIngeh@203.62.28.64) (Quit: Client closed)
2022-03-08 01:58:22 +0100 <geekosaur> we call it "pl" ("pointless") for a reason :)
2022-03-08 01:58:32 +0100 <hpc> worldhelloworld: if it makes you feel better, the entire field of math doesn't even understand real numbers
2022-03-08 01:58:34 +0100 <geekosaur> and even so that's one of ts cleaner outputs
2022-03-08 01:58:41 +0100 <geekosaur> *its
2022-03-08 01:58:51 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds)
2022-03-08 01:58:54 +0100 <geekosaur> oh they left already
2022-03-08 01:59:00 +0100meinside(uid24933@id-24933.helmsley.irccloud.com)
2022-03-08 01:59:17 +0100 <liz_> it sounds very funny then
2022-03-08 01:59:22 +0100alp(~alp@user/alp)
2022-03-08 01:59:31 +0100 <hpc> you're further in the weeds here than hardly any programmer ever gets
2022-03-08 01:59:43 +0100 <hpc> but they're really cool weeds
2022-03-08 01:59:50 +0100 <monochrom> Hell I think most people understand recursion less than they think.
2022-03-08 02:00:04 +0100 <jackdk> I understand recursion as much as I understand recursion
2022-03-08 02:00:23 +0100 <monochrom> I recently proved that well-founded induction justifies well-founded recursive definitions.
2022-03-08 02:00:29 +0100cynomys(~cynomys@user/cynomys)
2022-03-08 02:00:34 +0100 <worldhelloworld> hpc not sure what that means about real numbers, but I presume it must be something fancy
2022-03-08 02:01:09 +0100 <monochrom> I think I found out that no matter how you dice it, some kind of choice axiom is needed.
2022-03-08 02:01:13 +0100 <worldhelloworld> monochrom am I a case in point?
2022-03-08 02:01:14 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 02:01:14 +0100machinedgod(~machinedg@24.105.81.50)
2022-03-08 02:01:47 +0100 <geekosaur> you have more justification than "most people", I suspect
2022-03-08 02:01:50 +0100 <hpc> worldhelloworld: just that fundamental math is deceptively tricky
2022-03-08 02:02:01 +0100cynomys(~cynomys@user/cynomys) (Client Quit)
2022-03-08 02:02:06 +0100 <Axman6> > let takeEnd n0 xs = fst $ foldr (\a (ys,n) -> if n <= 0 then (ys, n) else (a:ys, n-1)) ([],n0) xs in takeEnd 3 [1..10]
2022-03-08 02:02:09 +0100 <lambdabot> [8,9,10]
2022-03-08 02:02:09 +0100 <worldhelloworld> fair enough
2022-03-08 02:02:10 +0100Tuplanolla(~Tuplanoll@91-159-69-98.elisa-laajakaista.fi) (Quit: Leaving.)
2022-03-08 02:02:12 +0100 <monochrom> I checked a set theory textbook, it handwaved away the involvement of choice, as in, it avoided saying that choice is needed.
2022-03-08 02:02:20 +0100burnsidesLlama(~burnsides@rrcs-76-81-82-250.west.biz.rr.com) (Remote host closed the connection)
2022-03-08 02:02:28 +0100 <monochrom> I feel like the authors were not aware.
2022-03-08 02:02:43 +0100 <liz_> in my experience, the axiom of choice only comes up in extremely rigorous texts
2022-03-08 02:02:57 +0100 <monochrom> By extension, if certain authors of a certain set theory textbook were not aware, perhaps a lot of mathematicians neither.
2022-03-08 02:03:03 +0100cynomys(~cynomys@user/cynomys) (Client Quit)
2022-03-08 02:03:18 +0100 <hpc> worldhelloworld: there's a joke that real analysis should be called complex analysis due to how difficult it is and how many problems aren't solvable
2022-03-08 02:03:30 +0100cynomys(~cynomys@user/cynomys)
2022-03-08 02:03:39 +0100 <hpc> worldhelloworld: and complex numbers should be called rational numbers because they have so many fewer edge cases
2022-03-08 02:03:42 +0100 <hpc> etc etc
2022-03-08 02:03:52 +0100 <hpc> (the whole numeric hierarchy gets renamed)
2022-03-08 02:03:53 +0100 <worldhelloworld> haha that sounds funny, even though I'm unable to understand the depths of it
2022-03-08 02:04:00 +0100 <liz_> complex analysis is no cakewalk either though x_x
2022-03-08 02:04:27 +0100 <hpc> heh, yeah
2022-03-08 02:04:33 +0100cynomys(~cynomys@user/cynomys) (Client Quit)
2022-03-08 02:04:52 +0100 <Axman6> hypercomplex analysis
2022-03-08 02:05:15 +0100 <hpc> my formal learning ended just before linear algebra
2022-03-08 02:05:31 +0100 <hpc> partially due to bad teachers and partially due to bad teaching
2022-03-08 02:05:48 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
2022-03-08 02:05:49 +0100 <worldhelloworld> how did you manage to be self taught as much?
2022-03-08 02:06:02 +0100 <hpc> i wasn't able to independently figure out what the actual fundamental stuff was, and all the classes ever did was drill how to solve eigenvectors and such
2022-03-08 02:06:12 +0100 <liz_> i have a masters degree in maths and i still struggle with real/complex analysis a lot
2022-03-08 02:06:34 +0100 <hpc> worldhelloworld: when i started college i tried learning python after being stuck with java all through HS
2022-03-08 02:06:44 +0100 <hpc> quickly realized i was too stupid for python, and learned haskell instead
2022-03-08 02:06:55 +0100 <hpc> it was way easier, ghc does a lot of thinking for me
2022-03-08 02:07:01 +0100 <geekosaur> this sounds like me :þ
2022-03-08 02:07:02 +0100 <hpc> then i just followed the concepts
2022-03-08 02:07:20 +0100 <hpc> people say things here, i google them, follow wikipedia links, mess with them in ghci, and ask questions
2022-03-08 02:07:41 +0100 <worldhelloworld> I, unfortunately, learned python a bit, now I am trying to unlearn it to learn haskell - it's more difficult
2022-03-08 02:07:59 +0100 <hpc> yeah, try unlearning java sometime, it's even harder
2022-03-08 02:08:12 +0100mvk(~mvk@2607:fea8:5cc3:7e00::45ee)
2022-03-08 02:08:15 +0100 <worldhelloworld> :)
2022-03-08 02:08:19 +0100 <hpc> it took me a month to get to an irc bot that could echo back what i sent it
2022-03-08 02:08:20 +0100 <geekosaur> except I have some baggage like never quite trusting myself at math because of some horrific early "schooling"
2022-03-08 02:08:47 +0100 <liz_> this is interesting to hear about, because my introduction to haskell was quite formal; a professor recommended it to me while we were discussing semigroup theory
2022-03-08 02:09:08 +0100 <hpc> and then it barely worked at that, i think the early versions could only run for a few days at a time before getting memory-killed
2022-03-08 02:09:42 +0100Sgeo_(~Sgeo@user/sgeo)
2022-03-08 02:10:10 +0100 <monochrom> I recommend "Linear Algebra Done Right" for a non-computational, putting-the-algebra-back-into-linear-algebra explanation of linear algebra.
2022-03-08 02:10:36 +0100 <hpc> 3b1b was what finally got linear algebra's concepts in my head
2022-03-08 02:10:43 +0100 <hpc> but by then it was too late to feel like anything but work
2022-03-08 02:10:47 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
2022-03-08 02:10:48 +0100ProfSimm(~ProfSimm@87.227.196.109) (Remote host closed the connection)
2022-03-08 02:10:53 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net) (Ping timeout: 272 seconds)
2022-03-08 02:11:04 +0100 <worldhelloworld> monochrom - how approachable is it for someone out of touch with academics?
2022-03-08 02:11:35 +0100 <worldhelloworld> hpc whats 3b1b?
2022-03-08 02:11:48 +0100 <hpc> https://www.youtube.com/c/3blue1brown
2022-03-08 02:11:57 +0100 <monochrom> For example, transpose is really defined by an adjunction. <T v, w> = <v, (transpose T) w>
2022-03-08 02:11:57 +0100 <worldhelloworld> oh that channel - got it
2022-03-08 02:12:12 +0100Sgeo(~Sgeo@user/sgeo) (Ping timeout: 240 seconds)
2022-03-08 02:12:40 +0100 <monochrom> It also has a no-matrix proof that eigenthings exist.
2022-03-08 02:12:51 +0100 <monochrom> Hell, no-determinant too.
2022-03-08 02:13:11 +0100 <hpc> ooh, nice
2022-03-08 02:13:17 +0100 <hpc> i hated calculating those
2022-03-08 02:13:24 +0100 <hpc> even computers hate calculating thoses
2022-03-08 02:13:44 +0100da39a3ee5e6b4b0d(~textual@171.5.29.46)
2022-03-08 02:13:56 +0100 <hpc> it's like the math version doing lines on the chalkboarad for detention
2022-03-08 02:14:48 +0100 <worldhelloworld> I'm afraid I havent read as much as you guys, couldn't even read Gilbert Strang .... but someday
2022-03-08 02:15:00 +0100 <hpc> i haven't read gilbert strang :P
2022-03-08 02:15:36 +0100 <worldhelloworld> I assumed it's a good book so many/most must have
2022-03-08 02:16:49 +0100 <liz_> if you ever wanted to dip your toes in more formal theory, then
2022-03-08 02:16:53 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8)
2022-03-08 02:16:54 +0100 <liz_> whoops, mispressed enter
2022-03-08 02:17:26 +0100 <liz_> I. N. Herstein's "Topics in Algebra" has good sections on vector spaces and linear transformations
2022-03-08 02:18:37 +0100 <worldhelloworld> Interesting .... I am too rusty, that sounds like something rigourous, hopefully in due time
2022-03-08 02:18:41 +0100 <worldhelloworld> thanks though
2022-03-08 02:22:17 +0100machinedgod(~machinedg@24.105.81.50) (Ping timeout: 240 seconds)
2022-03-08 02:25:07 +0100alp(~alp@user/alp) (Remote host closed the connection)
2022-03-08 02:25:29 +0100alp(~alp@user/alp)
2022-03-08 02:28:08 +0100 <romesrf> night everyone
2022-03-08 02:28:12 +0100romesrf(~romes@44.190.189.46.rev.vodafone.pt) (Quit: WeeChat 3.4)
2022-03-08 02:29:02 +0100 <worldhelloworld> nighty
2022-03-08 02:29:37 +0100kimjetwav(~user@2607:fea8:2363:8f00:3065:9fc7:d58e:fc3e) (Quit: ERC 5.4.1 (IRC client for GNU Emacs 29.0.50))
2022-03-08 02:30:04 +0100kimjetwav(~user@2607:fea8:2363:8f00:3065:9fc7:d58e:fc3e)
2022-03-08 02:30:44 +0100DNH(~DNH@2a02:8108:1100:16d8:598a:8b0b:9405:6e26) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 02:34:01 +0100da39a3ee5e6b4b0d(~textual@171.5.29.46) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 02:35:35 +0100alp(~alp@user/alp) (Ping timeout: 268 seconds)
2022-03-08 02:45:16 +0100img(~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
2022-03-08 02:45:33 +0100img(~img@user/img)
2022-03-08 02:46:07 +0100tommd(~tommd@97-120-41-123.ptld.qwest.net) (Ping timeout: 256 seconds)
2022-03-08 03:00:45 +0100unyu(~pyon@user/pyon) (Quit: brb)
2022-03-08 03:01:10 +0100gentauro(~gentauro@user/gentauro) (Ping timeout: 256 seconds)
2022-03-08 03:01:54 +0100kimjetwav(~user@2607:fea8:2363:8f00:3065:9fc7:d58e:fc3e) (Quit: ERC 5.4.1 (IRC client for GNU Emacs 29.0.50))
2022-03-08 03:02:29 +0100kimjetwav(~user@2607:fea8:2363:8f00:3065:9fc7:d58e:fc3e)
2022-03-08 03:03:22 +0100unyu(~pyon@user/pyon)
2022-03-08 03:03:48 +0100justsomeguy(~justsomeg@user/justsomeguy)
2022-03-08 03:07:30 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e)
2022-03-08 03:07:45 +0100gentauro(~gentauro@user/gentauro)
2022-03-08 03:17:16 +0100vicfred(~vicfred@user/vicfred) (Quit: Leaving)
2022-03-08 03:18:36 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Remote host closed the connection)
2022-03-08 03:21:50 +0100hughjfchen(~hughjfche@vmi556545.contaboserver.net) (Quit: WeeChat 2.8)
2022-03-08 03:23:44 +0100wroathe(~wroathe@206-55-188-8.fttp.usinternet.com)
2022-03-08 03:23:44 +0100wroathe(~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host)
2022-03-08 03:23:44 +0100wroathe(~wroathe@user/wroathe)
2022-03-08 03:25:12 +0100hughjfchen(~hughjfche@vmi556545.contaboserver.net)
2022-03-08 03:34:02 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net) (Ping timeout: 256 seconds)
2022-03-08 03:34:20 +0100x_kuru(~xkuru@user/xkuru)
2022-03-08 03:35:19 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net)
2022-03-08 03:37:06 +0100caildddddt^(~cailddddd@50.232.121.75)
2022-03-08 03:37:30 +0100cheater1__(~Username@user/cheater)
2022-03-08 03:37:34 +0100little_mac(~little_ma@2601:410:4300:3ce0:4154:7a97:7f52:6596) (Remote host closed the connection)
2022-03-08 03:37:39 +0100xkuru(~xkuru@user/xkuru) (Ping timeout: 272 seconds)
2022-03-08 03:37:39 +0100cheater(~Username@user/cheater) (Ping timeout: 272 seconds)
2022-03-08 03:37:45 +0100cheater1__cheater
2022-03-08 03:37:51 +0100little_mac(~little_ma@2601:410:4300:3ce0:8cff:8f3a:46d8:f6ed)
2022-03-08 03:38:34 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 256 seconds)
2022-03-08 03:41:06 +0100liz(~liz@2a00:23c5:9680:501:f2d5:bfff:fe6a:5af4) (Remote host closed the connection)
2022-03-08 03:41:42 +0100justsomeguy(~justsomeg@user/justsomeguy) (Quit: WeeChat 3.4)
2022-03-08 03:41:58 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net) (Ping timeout: 256 seconds)
2022-03-08 03:48:03 +0100aeka`(~aeka@pool-100-4-208-71.albyny.fios.verizon.net)
2022-03-08 03:48:06 +0100aeka(~aeka@user/hiruji) (Ping timeout: 260 seconds)
2022-03-08 03:49:00 +0100neurocyte0917090(~neurocyte@user/neurocyte) (Ping timeout: 252 seconds)
2022-03-08 03:51:57 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
2022-03-08 03:52:11 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 03:55:53 +0100merijn(~merijn@c-001-002-007.client.esciencecenter.eduvpn.nl)
2022-03-08 03:57:54 +0100aeka`(~aeka@pool-100-4-208-71.albyny.fios.verizon.net) (Ping timeout: 260 seconds)
2022-03-08 04:04:44 +0100Unicorn_Princess(~Unicorn_P@46-54-248-191.static.kate-wing.si) (Remote host closed the connection)
2022-03-08 04:08:07 +0100kimjetwav(~user@2607:fea8:2363:8f00:3065:9fc7:d58e:fc3e) (Quit: ERC 5.4.1 (IRC client for GNU Emacs 29.0.50))
2022-03-08 04:08:17 +0100jonathanx_(~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 256 seconds)
2022-03-08 04:08:22 +0100mjs2600(~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in)
2022-03-08 04:09:46 +0100mjs2600(~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net)
2022-03-08 04:25:06 +0100geekosaur(~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
2022-03-08 04:28:08 +0100geekosaur(~geekosaur@xmonad/geekosaur)
2022-03-08 04:28:26 +0100merijn(~merijn@c-001-002-007.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
2022-03-08 04:34:20 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Remote host closed the connection)
2022-03-08 04:34:37 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 04:41:37 +0100waleee(~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 240 seconds)
2022-03-08 04:42:53 +0100terrorjack(~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat)
2022-03-08 04:44:05 +0100terrorjack(~terrorjac@2a01:4f8:1c1e:509a::1)
2022-03-08 04:48:50 +0100Erutuon(~Erutuon@user/erutuon) (Ping timeout: 256 seconds)
2022-03-08 04:51:37 +0100[_](~itchyjunk@user/itchyjunk/x-7353470)
2022-03-08 04:52:25 +0100emf(~emf@c-73-97-137-43.hsd1.wa.comcast.net)
2022-03-08 04:53:02 +0100emf(~emf@c-73-97-137-43.hsd1.wa.comcast.net) (Client Quit)
2022-03-08 04:54:41 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Remote host closed the connection)
2022-03-08 04:55:00 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 04:55:01 +0100emf(~emf@c-73-97-137-43.hsd1.wa.comcast.net)
2022-03-08 04:55:18 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds)
2022-03-08 04:55:36 +0100geekosaur(~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
2022-03-08 04:59:17 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 04:59:46 +0100emf_(~emf@2620:10d:c090:400::5:8ba5)
2022-03-08 05:01:28 +0100emf(~emf@c-73-97-137-43.hsd1.wa.comcast.net) (Ping timeout: 250 seconds)
2022-03-08 05:02:27 +0100adanwan(~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection)
2022-03-08 05:02:44 +0100adanwan(~adanwan@gateway/tor-sasl/adanwan)
2022-03-08 05:02:59 +0100cjb(~cjb@user/cjb) (Quit: rcirc on GNU Emacs 29.0.50)
2022-03-08 05:05:56 +0100geekosaur(~geekosaur@xmonad/geekosaur)
2022-03-08 05:10:02 +0100Erutuon(~Erutuon@user/erutuon)
2022-03-08 05:11:55 +0100mbuf(~Shakthi@122.174.51.86)
2022-03-08 05:17:46 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 05:20:07 +0100liz_(~liz@2a00:23c5:9680:501:b62e:99ff:fee4:47fa) (Quit: Leaving)
2022-03-08 05:20:16 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net)
2022-03-08 05:24:52 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net) (Ping timeout: 250 seconds)
2022-03-08 05:25:17 +0100mvk(~mvk@2607:fea8:5cc3:7e00::45ee) (Ping timeout: 240 seconds)
2022-03-08 05:28:36 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 05:29:04 +0100kayvank(~user@52-119-115-185.PUBLIC.monkeybrains.net) (Ping timeout: 256 seconds)
2022-03-08 05:33:17 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 05:35:13 +0100caildddddt^(~cailddddd@50.232.121.75) (Remote host closed the connection)
2022-03-08 05:36:13 +0100wroathe(~wroathe@user/wroathe) (Quit: leaving)
2022-03-08 05:36:51 +0100wroathe(~wroathe@206-55-188-8.fttp.usinternet.com)
2022-03-08 05:36:51 +0100wroathe(~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host)
2022-03-08 05:36:51 +0100wroathe(~wroathe@user/wroathe)
2022-03-08 05:43:47 +0100kayvank(~user@52-119-115-185.PUBLIC.monkeybrains.net)
2022-03-08 05:46:39 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 05:53:45 +0100worldhelloworld1(uid543174@id-543174.helmsley.irccloud.com) (Quit: Connection closed for inactivity)
2022-03-08 05:59:40 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 256 seconds)
2022-03-08 06:00:02 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e)
2022-03-08 06:10:10 +0100dschrempf(~dominik@070-207.dynamic.dsl.fonira.net)
2022-03-08 06:12:37 +0100aweinstock(~aweinstoc@cpe-67-248-65-250.nycap.res.rr.com) (Ping timeout: 240 seconds)
2022-03-08 06:13:26 +0100fryguybob(~fryguybob@cpe-74-67-169-145.rochester.res.rr.com) (Ping timeout: 272 seconds)
2022-03-08 06:14:34 +0100fryguybob(~fryguybob@cpe-74-67-169-145.rochester.res.rr.com)
2022-03-08 06:14:42 +0100aweinstock(~aweinstoc@cpe-67-248-65-250.nycap.res.rr.com)
2022-03-08 06:23:35 +0100kaph(~kaph@net-109-116-124-149.cust.vodafonedsl.it) (Ping timeout: 272 seconds)
2022-03-08 06:25:10 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 06:28:35 +0100dschrempf(~dominik@070-207.dynamic.dsl.fonira.net) (Quit: WeeChat 3.3)
2022-03-08 06:33:56 +0100bahamas(~lucian@84.232.140.52)
2022-03-08 06:35:40 +0100jonathanx(~jonathan@h-178-174-176-109.A357.priv.bahnhof.se)
2022-03-08 06:40:34 +0100ajb(~ajb@cupid.whatbox.ca) (Quit: bye)
2022-03-08 06:41:26 +0100res0nat0r08(~Fletch@dia.whatbox.ca) (Quit: The Lounge - https://thelounge.chat)
2022-03-08 06:41:48 +0100coot(~coot@213.134.190.95)
2022-03-08 06:45:39 +0100jpds(~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection)
2022-03-08 06:45:47 +0100kaph(~kaph@151.47.91.217)
2022-03-08 06:46:02 +0100jpds(~jpds@gateway/tor-sasl/jpds)
2022-03-08 06:49:47 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 06:52:25 +0100azimut_(~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection)
2022-03-08 06:52:53 +0100azimut(~azimut@gateway/tor-sasl/azimut)
2022-03-08 06:53:15 +0100nattiestnate(~nate@202.138.250.13)
2022-03-08 06:59:24 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds)
2022-03-08 07:01:02 +0100nattiestnate(~nate@202.138.250.13) (Quit: WeeChat 3.4)
2022-03-08 07:01:12 +0100emf_(~emf@2620:10d:c090:400::5:8ba5) (Quit: emf_)
2022-03-08 07:02:43 +0100zincy_(~zincy@host86-160-236-152.range86-160.btcentralplus.com)
2022-03-08 07:02:48 +0100kaph_(~kaph@151.47.91.217)
2022-03-08 07:03:33 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 07:03:38 +0100kaph(~kaph@151.47.91.217) (Read error: Connection reset by peer)
2022-03-08 07:07:21 +0100zincy_(~zincy@host86-160-236-152.range86-160.btcentralplus.com) (Ping timeout: 256 seconds)
2022-03-08 07:09:14 +0100takuan(~takuan@178-116-218-225.access.telenet.be)
2022-03-08 07:13:20 +0100bahamas(~lucian@84.232.140.52) (Ping timeout: 256 seconds)
2022-03-08 07:13:26 +0100azimut(~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection)
2022-03-08 07:13:45 +0100azimut(~azimut@gateway/tor-sasl/azimut)
2022-03-08 07:15:26 +0100deadmarshal_(~deadmarsh@95.38.114.14)
2022-03-08 07:19:40 +0100kaph__(~kaph@151.35.204.82)
2022-03-08 07:22:25 +0100kaph__(~kaph@151.35.204.82) (Read error: Connection reset by peer)
2022-03-08 07:22:29 +0100kaph_(~kaph@151.47.91.217) (Ping timeout: 272 seconds)
2022-03-08 07:30:24 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Remote host closed the connection)
2022-03-08 07:30:42 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 07:32:37 +0100[_](~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer)
2022-03-08 07:35:00 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Remote host closed the connection)
2022-03-08 07:35:17 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 07:39:07 +0100zebrag(~chris@user/zebrag) (Remote host closed the connection)
2022-03-08 07:43:55 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Remote host closed the connection)
2022-03-08 07:44:13 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 07:58:42 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net)
2022-03-08 07:59:11 +0100deadmarshal_(~deadmarsh@95.38.114.14) (Quit: ZNC 1.8.2 - https://znc.in)
2022-03-08 07:59:34 +0100deadmarshal_(~deadmarsh@95.38.114.14)
2022-03-08 08:00:23 +0100res0nat0r08(~Fletch@dia.whatbox.ca)
2022-03-08 08:03:27 +0100niekvandepas(~niekvande@77-161-122-185.fixed.kpn.net) (Ping timeout: 256 seconds)
2022-03-08 08:06:51 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 08:09:24 +0100akurilin_(uid322841@id-322841.ilkley.irccloud.com) (Quit: Connection closed for inactivity)
2022-03-08 08:17:03 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 08:18:05 +0100beka(~beka@104.193.170.240) (Remote host closed the connection)
2022-03-08 08:18:33 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2022-03-08 08:18:43 +0100beka(~beka@104.193.170.240)
2022-03-08 08:18:46 +0100FragByte(~christian@user/fragbyte) (Quit: Quit)
2022-03-08 08:19:24 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2022-03-08 08:20:45 +0100FragByte(~christian@user/fragbyte)
2022-03-08 08:21:36 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 08:22:28 +0100gehmehgeh(~user@user/gehmehgeh)
2022-03-08 08:23:11 +0100fendor(~fendor@178.115.53.79.wireless.dyn.drei.com)
2022-03-08 08:23:51 +0100jakalx(~jakalx@base.jakalx.net) ()
2022-03-08 08:30:22 +0100mbuf(~Shakthi@122.174.51.86) (Quit: Leaving)
2022-03-08 08:30:34 +0100jakalx(~jakalx@base.jakalx.net)
2022-03-08 08:32:04 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 08:32:59 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 08:41:11 +0100alp(~alp@user/alp)
2022-03-08 08:44:39 +0100x_kuru(~xkuru@user/xkuru) (Read error: Connection reset by peer)
2022-03-08 08:47:50 +0100michalz(~michalz@185.246.204.93)
2022-03-08 08:55:03 +0100mncheck(~mncheck@193.224.205.254)
2022-03-08 08:56:28 +0100deadmarshal_(~deadmarsh@95.38.114.14) (Ping timeout: 256 seconds)
2022-03-08 09:00:47 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 09:00:48 +0100acidjnk(~acidjnk@p200300d0c7049f27690562e0ba62f824.dip0.t-ipconnect.de)
2022-03-08 09:02:44 +0100deadmarshal_(~deadmarsh@95.38.114.14)
2022-03-08 09:03:39 +0100zeenk(~zeenk@2a02:2f04:a30d:1300:51a3:bcfc:6cda:9fc5)
2022-03-08 09:18:27 +0100jespada(~jespada@85.255.234.169)
2022-03-08 09:19:57 +0100mncheck(~mncheck@193.224.205.254) (Quit: Leaving)
2022-03-08 09:20:40 +0100mncheck(~mncheck@193.224.205.254)
2022-03-08 09:25:15 +0100drdo(~drdo@roach0.drdo.eu) (Quit: Ping timeout (120 seconds))
2022-03-08 09:25:28 +0100drdo(~drdo@roach0.drdo.eu)
2022-03-08 09:29:43 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:3240:c699:b7eb:e5b0)
2022-03-08 09:30:25 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds)
2022-03-08 09:31:35 +0100little_mac(~little_ma@2601:410:4300:3ce0:8cff:8f3a:46d8:f6ed) (Remote host closed the connection)
2022-03-08 09:34:28 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 250 seconds)
2022-03-08 09:35:12 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 09:35:52 +0100lumberjack123(~alMalsamo@gateway/tor-sasl/almalsamo) (Remote host closed the connection)
2022-03-08 09:36:09 +0100lumberjack123(~alMalsamo@gateway/tor-sasl/almalsamo)
2022-03-08 09:36:24 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 09:37:23 +0100Sgeo_(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2022-03-08 09:45:28 +0100pranshukhandal(pranshukha@envs.net) (Quit: the lounge - https://webirc.envs.net)
2022-03-08 09:45:28 +0100sus(zero@user/zeromomentum) (Quit: the lounge - https://webirc.envs.net)
2022-03-08 09:46:03 +0100Topsi(~Tobias@dyndsl-095-033-088-239.ewe-ip-backbone.de)
2022-03-08 09:48:06 +0100machinedgod(~machinedg@24.105.81.50)
2022-03-08 09:48:23 +0100sus(zero@user/zeromomentum)
2022-03-08 09:48:24 +0100pranshukhandal(~ghost@envs.net)
2022-03-08 09:49:38 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 09:50:17 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net)
2022-03-08 09:53:58 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 09:58:01 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
2022-03-08 10:00:06 +0100kadoban(~kadoban@user/kadoban) (Quit: You have been kicked for being idle)
2022-03-08 10:00:31 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 10:00:33 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2022-03-08 10:01:00 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643)
2022-03-08 10:03:28 +0100krappix(~krappix@nat-eduroam-76-gw-01-lne.lille.inria.fr)
2022-03-08 10:06:07 +0100lavaman(~lavaman@98.38.249.169) (Remote host closed the connection)
2022-03-08 10:09:35 +0100ptrcmd(~ptrcmd@user/ptrcmd) (Remote host closed the connection)
2022-03-08 10:11:05 +0100ptrcmd(~ptrcmd@user/ptrcmd)
2022-03-08 10:11:34 +0100ccntrq(~Thunderbi@2a01:c22:9102:c100:80c3:8f62:e3ae:6455)
2022-03-08 10:12:47 +0100DNH(~DNH@2a02:8108:1100:16d8:598a:8b0b:9405:6e26)
2022-03-08 10:18:10 +0100econo(uid147250@user/econo) (Quit: Connection closed for inactivity)
2022-03-08 10:19:11 +0100ishutin(~ishutin@92-249-193-65.pool.digikabel.hu) (Ping timeout: 272 seconds)
2022-03-08 10:20:14 +0100ishutin(~ishutin@87-97-30-219.pool.digikabel.hu)
2022-03-08 10:21:28 +0100kuribas(~user@ptr-25vy0i8r77cynr1cb5v.18120a2.ip6.access.telenet.be)
2022-03-08 10:21:32 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 10:22:11 +0100 <kuribas> Does correctness and simplicity even go together?
2022-03-08 10:22:54 +0100 <kuribas> I have been looking to solve this problem: in lisp (clojure) we can put a specification in data, then create the functionality by interpreting the data (for example a specification of an API).
2022-03-08 10:22:58 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 10:23:23 +0100 <kuribas> Doing this in haskell is easy. The problem is proving consistency.
2022-03-08 10:23:53 +0100 <kuribas> You'll end up with something like servant, which is hardly simple...
2022-03-08 10:24:23 +0100 <kuribas> Or you need to use GADTs to have stronger consistency garantees.
2022-03-08 10:24:36 +0100 <kuribas> And hashmaps are easy to work with in clojure, records in haskell aren't very flexible.
2022-03-08 10:26:51 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e)
2022-03-08 10:27:05 +0100 <kuribas> The thing is, doing these things is all possible, but doing it with "simple" haskell seems nearly impossible.
2022-03-08 10:31:50 +0100 <kuribas> Or maybe better to not "prove" consistency, but write a lot of tests?
2022-03-08 10:32:31 +0100 <kuribas> probably "not consistent haskell" is still better than clojure.
2022-03-08 10:33:30 +0100jespada(~jespada@85.255.234.169) (Ping timeout: 268 seconds)
2022-03-08 10:38:13 +0100 <kuribas> I found two solutions: higher kinded records, manipulating them using generic "magic".
2022-03-08 10:38:34 +0100 <kuribas> Or going to idris, where types can be data, and data can be types. That makes manipulating types much easier.
2022-03-08 10:42:57 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab) (Remote host closed the connection)
2022-03-08 10:43:46 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Remote host closed the connection)
2022-03-08 10:44:07 +0100romesrf(~romes@44.190.189.46.rev.vodafone.pt)
2022-03-08 10:45:25 +0100 <romesrf> good morning
2022-03-08 10:47:04 +0100cosimone(~user@93-47-229-38.ip115.fastwebnet.it)
2022-03-08 10:47:13 +0100krappix(~krappix@nat-eduroam-76-gw-01-lne.lille.inria.fr) (Ping timeout: 256 seconds)
2022-03-08 10:47:24 +0100 <kuribas> morning
2022-03-08 10:48:32 +0100dhouthoo(~dhouthoo@178-117-36-167.access.telenet.be)
2022-03-08 10:48:39 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 10:51:40 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net)
2022-03-08 10:52:46 +0100jespada(~jespada@148.252.132.235)
2022-03-08 10:53:42 +0100ehammarstrom_(~ehammarst@62-20-203-39-no182.tbcn.telia.com)
2022-03-08 10:53:47 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
2022-03-08 10:54:01 +0100ehammarstrom(~ehammarst@62-20-203-39-no182.tbcn.telia.com) (Ping timeout: 256 seconds)
2022-03-08 10:54:03 +0100tzh(~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz)
2022-03-08 10:56:57 +0100alt-romes(~romes@44.190.189.46.rev.vodafone.pt)
2022-03-08 10:58:27 +0100kaph(~kaph@151.37.169.201)
2022-03-08 10:59:38 +0100romesrf(~romes@44.190.189.46.rev.vodafone.pt) (Ping timeout: 252 seconds)
2022-03-08 11:00:01 +0100agumonkey(~user@88.163.231.79)
2022-03-08 11:01:24 +0100mncheck(~mncheck@193.224.205.254) (Remote host closed the connection)
2022-03-08 11:03:57 +0100phma(phma@2001:5b0:210b:8f48:791b:849d:7db1:84dd)
2022-03-08 11:05:07 +0100kaph(~kaph@151.37.169.201) (Ping timeout: 256 seconds)
2022-03-08 11:05:44 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 11:10:44 +0100mncheck(~mncheck@193.224.205.254)
2022-03-08 11:13:15 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 11:14:37 +0100ProfSimm(~ProfSimm@87.227.196.109)
2022-03-08 11:14:41 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e)
2022-03-08 11:16:13 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e) (Client Quit)
2022-03-08 11:16:45 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e)
2022-03-08 11:18:25 +0100szkl(uid110435@id-110435.uxbridge.irccloud.com)
2022-03-08 11:20:24 +0100Erutuon(~Erutuon@user/erutuon) (Ping timeout: 256 seconds)
2022-03-08 11:25:11 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 11:26:11 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 245 seconds)
2022-03-08 11:27:10 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Remote host closed the connection)
2022-03-08 11:30:27 +0100__monty__(~toonn@user/toonn)
2022-03-08 11:30:51 +0100jespada(~jespada@148.252.132.235) (Ping timeout: 268 seconds)
2022-03-08 11:32:55 +0100Erutuon(~Erutuon@user/erutuon)
2022-03-08 11:33:02 +0100Unicorn_Princess(~Unicorn_P@46-54-248-191.static.kate-wing.si)
2022-03-08 11:34:19 +0100jespada(~jespada@148.252.132.235)
2022-03-08 11:36:28 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 11:36:50 +0100vglfr(~vglfr@coupling.penchant.volia.net) (Ping timeout: 256 seconds)
2022-03-08 11:41:22 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
2022-03-08 11:43:21 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab)
2022-03-08 11:44:49 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 11:47:24 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab) (Ping timeout: 240 seconds)
2022-03-08 11:51:01 +0100agumonkey(~user@88.163.231.79) (Ping timeout: 256 seconds)
2022-03-08 11:52:56 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 11:55:56 +0100DNH(~DNH@2a02:8108:1100:16d8:598a:8b0b:9405:6e26) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 11:56:34 +0100rembo10(~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in)
2022-03-08 11:57:24 +0100DNH(~DNH@2a02:8108:1100:16d8:598a:8b0b:9405:6e26)
2022-03-08 11:57:28 +0100rembo10(~rembo10@main.remulis.com)
2022-03-08 11:57:30 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 11:58:51 +0100worldhelloworld1(uid543174@id-543174.helmsley.irccloud.com)
2022-03-08 11:58:53 +0100alt-romes(~romes@44.190.189.46.rev.vodafone.pt) (Quit: WeeChat 3.4)
2022-03-08 11:59:12 +0100romesrf(~romes@44.190.189.46.rev.vodafone.pt)
2022-03-08 11:59:36 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net) (Quit: Leaving)
2022-03-08 11:59:50 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net)
2022-03-08 12:01:56 +0100adanwan(~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 240 seconds)
2022-03-08 12:01:56 +0100adanwan_(~adanwan@gateway/tor-sasl/adanwan)
2022-03-08 12:04:30 +0100dsamperi(~dsamperi@2603-7000-3b42-5400-bdd9-2653-5498-c104.res6.spectrum.com)
2022-03-08 12:05:13 +0100dsamperi(~dsamperi@2603-7000-3b42-5400-bdd9-2653-5498-c104.res6.spectrum.com) (Client Quit)
2022-03-08 12:06:51 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net) (Ping timeout: 272 seconds)
2022-03-08 12:08:35 +0100mc47(~mc47@xmonad/TheMC47)
2022-03-08 12:10:28 +0100mc47(~mc47@xmonad/TheMC47) (Remote host closed the connection)
2022-03-08 12:10:32 +0100srk(~sorki@user/srk)
2022-03-08 12:10:42 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 12:12:57 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 12:13:56 +0100yauhsien(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Remote host closed the connection)
2022-03-08 12:14:45 +0100 <tomsmeding_> kuribas: proving correctness is always hard
2022-03-08 12:14:50 +0100tomsmeding_tomsmeding
2022-03-08 12:15:06 +0100 <tomsmeding> or at least, nobody has found a way yet to easily prove correctness of nontrivial programs
2022-03-08 12:15:26 +0100 <kuribas> perhaps correctness is a vague name
2022-03-08 12:15:33 +0100 <kuribas> I prefer "consistency".
2022-03-08 12:15:43 +0100 <tomsmeding> s/correctness/any nontrivial behavioural property/
2022-03-08 12:15:58 +0100 <kuribas> As in, I have a (API) specification, and I want to ensure the program implements this specification.
2022-03-08 12:16:05 +0100 <tomsmeding> same thing
2022-03-08 12:16:23 +0100 <kuribas> Or a database schema, and the SQL is correct WRT to that schema.
2022-03-08 12:16:38 +0100 <tomsmeding> that is easier, because sql is a more limited language than haskell
2022-03-08 12:17:20 +0100 <kuribas> It's subtly different, because I don't prove the program implements the business logic correctly.
2022-03-08 12:17:26 +0100 <kuribas> I just prove it is consisten with itself.
2022-03-08 12:17:32 +0100 <kuribas> Though possible wrong.
2022-03-08 12:17:52 +0100fendor_(~fendor@178.165.181.170.wireless.dyn.drei.com)
2022-03-08 12:17:56 +0100 <tomsmeding> it's still a nontrivial property about the behaviour of the program
2022-03-08 12:18:04 +0100 <kuribas> yeah
2022-03-08 12:18:19 +0100 <tomsmeding> "In computability theory, Rice's theorem states that all non-trivial semantic properties of programs are undecidable."
2022-03-08 12:18:38 +0100 <tomsmeding> it's hard, and humans have the impressive ability to write proofs for some of those properties
2022-03-08 12:18:43 +0100 <tomsmeding> but we haven't found a way yet to make that much easier
2022-03-08 12:18:55 +0100 <kuribas> Still, is it so hard to prove, this server implements this API specification?
2022-03-08 12:19:04 +0100 <kuribas> servant does it, but clumsily.
2022-03-08 12:19:20 +0100 <tomsmeding> in general, yes; if your program has specific structure that you can exploit (e.g. in the types), then that helps
2022-03-08 12:19:55 +0100 <tomsmeding> in particular, with a strong enough type system, you can encode the proof in the types, so that any total program that has that type does the right thing
2022-03-08 12:20:15 +0100 <tomsmeding> which is a fairly extreme case of "if your program has specific structure, it's easier"
2022-03-08 12:20:28 +0100fendor(~fendor@178.115.53.79.wireless.dyn.drei.com) (Ping timeout: 256 seconds)
2022-03-08 12:20:34 +0100 <tomsmeding> PL people very much like the approach, but it's not the only approach
2022-03-08 12:20:58 +0100 <kuribas> What I like to aim for is not "correct" business logic, but transparent and consistent business logic.
2022-03-08 12:21:24 +0100 <kuribas> In a sense that what business logic the program implements is easy to see from the code.
2022-03-08 12:21:29 +0100 <tomsmeding> you also have stuff like Why3, where you (write the program in their dialect of ocaml and) annotate pre- and post-conditions and loop invariants, and it tries to use an SMT solver to prove stuff
2022-03-08 12:21:31 +0100vglfr(~vglfr@88.155.96.35)
2022-03-08 12:21:50 +0100 <tomsmeding> true, maybe "correct" is a too-loaded term for this
2022-03-08 12:22:02 +0100 <tomsmeding> but for me, what you say falls into the same bucket
2022-03-08 12:22:15 +0100 <kuribas> Right, but that's "after the fact" proving.
2022-03-08 12:22:24 +0100 <tomsmeding> whether the specification is external, or if it's another part of your program, same thing
2022-03-08 12:22:24 +0100 <kuribas> You write some code or algorithm, then you prove it correct.
2022-03-08 12:22:28 +0100 <tomsmeding> yes
2022-03-08 12:22:42 +0100 <kuribas> It seems easier to make something correct by construction.
2022-03-08 12:22:46 +0100 <tomsmeding> as distinct from the dependent-types encode-the-proof-in-the-type-system approach
2022-03-08 12:24:09 +0100 <kuribas> Technically haskell is a subset of dependent-types.
2022-03-08 12:24:12 +0100 <tomsmeding> my point is, your observation that it's hard is not surprising :p
2022-03-08 12:24:12 +0100 <tomsmeding> yes
2022-03-08 12:24:13 +0100 <Hecate> hohai
2022-03-08 12:24:42 +0100 <kuribas> "Integer" is just a proposition that the value behaves like a mathematical integer
2022-03-08 12:24:56 +0100 <tomsmeding> Hecate: hi :)
2022-03-08 12:26:03 +0100aeka(~aeka@pool-100-4-208-71.albyny.fios.verizon.net)
2022-03-08 12:26:10 +0100 <kuribas> And the HM inference engine just proofs that it does.
2022-03-08 12:26:26 +0100 <kuribas> tomsmeding: yeah, I guess it's non-trivial.
2022-03-08 12:26:30 +0100 <Hecate> are we on the propositions as types / programs as proof discussion?
2022-03-08 12:26:36 +0100 <Hecate> tomsmeding: hello you :)
2022-03-08 12:26:51 +0100 <kuribas> tomsmeding: it's just, clojure doesn't feel very satisfying, though there good ideas in there.
2022-03-08 12:27:51 +0100 <tomsmeding> Hecate: this started the discussion https://ircbrowse.tomsmeding.com/day/lchaskell/today?id=463224#trid463224
2022-03-08 12:28:02 +0100 <Hecate> > Does correctness and simplicity even go together?
2022-03-08 12:28:04 +0100 <lambdabot> <hint>:1:50: error:
2022-03-08 12:28:04 +0100 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
2022-03-08 12:28:05 +0100 <Hecate> oh oh oh
2022-03-08 12:28:07 +0100 <Hecate> good question
2022-03-08 12:28:10 +0100 <Hecate> I have a short answer
2022-03-08 12:28:13 +0100 <Hecate> no and yes
2022-03-08 12:28:38 +0100 <Hecate> no: Being correct implies that you need to forgo a simplistic world view and take care of the sharp edges of your model
2022-03-08 12:29:05 +0100 <Hecate> yes: Having correct foundations mean that you have to do less work in your program to maintain correctness
2022-03-08 12:29:27 +0100 <Hecate> also read: Complexity has to live somewhere: https://ferd.ca/complexity-has-to-live-somewhere.html
2022-03-08 12:29:47 +0100Rembanebuilds house for complexity
2022-03-08 12:30:18 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net) (Ping timeout: 260 seconds)
2022-03-08 12:30:39 +0100 <Hecate> following this aphorism, we can indeed state that correctness is complex to nail, but having it live in your compiler rather than as an external library or, worse, to be manually verified by the user, makes thing simpler for downstream users
2022-03-08 12:31:09 +0100 <Hecate> now if you truly want a yes XOR no answer, you need to ask the question of costs and benefits
2022-03-08 12:31:27 +0100 <Hecate> at which scale of users is it more economic to have correctness upstreamed?
2022-03-08 12:31:45 +0100 <Hecate> if you're five cave dwellers using a lisp interpreter written in Forth, maybe not
2022-03-08 12:32:07 +0100 <Hecate> if you're 200k people around the globe and your language promotes correctness of thinking and implementation, then yeah sure
2022-03-08 12:32:51 +0100 <Hecate> any question? :p
2022-03-08 12:33:28 +0100 <maerwald> I never had the impression that Haskell promotes correctness. Correctness is usually something rather low-level that only in a few domains coincides with the type system.
2022-03-08 12:33:58 +0100 <maerwald> So not only is "simplicity" underspecified, but so is "correctness"
2022-03-08 12:34:41 +0100 <maerwald> what promotes correctness is usually the compiler, not the language, or the base libraries
2022-03-08 12:34:41 +0100 <Hecate> maerwald: on my side, I'd say that the expressivity of Haskell and some of its type-level feature enable you to achieve more correctness when representing a business domain
2022-03-08 12:35:06 +0100 <Hecate> for example, the ability to have Word16 for port numbers instead of Integer
2022-03-08 12:35:06 +0100 <Hecate> :)
2022-03-08 12:35:20 +0100 <Franciman> Hecate: maybe you can subsume your no, yes answer by talking about correctness with respect to a model
2022-03-08 12:35:28 +0100 <maerwald> Hecate: expressivity introduces complexity, too
2022-03-08 12:35:43 +0100 <Franciman> now if the model is to be accurate of reality, then it is going to probably be very wild and hard
2022-03-08 12:36:02 +0100 <Hecate> Franciman: ah well, the best questions attract the best answers, and general questions usually attract "it depends" as an answer :)
2022-03-08 12:36:04 +0100 <maerwald> so the most correct way to build something is usually not a turing complete language
2022-03-08 12:36:11 +0100 <maerwald> but the *most* restrictive way
2022-03-08 12:36:17 +0100 <Hecate> maerwald: everything introduces complexity, see https://ferd.ca/complexity-has-to-live-somewhere.html
2022-03-08 12:36:32 +0100 <Hecate> I don't think this is a valid deterrent :p
2022-03-08 12:36:52 +0100 <maerwald> the more you constrain expressivity, the less ways of expressing the wrong thing you have
2022-03-08 12:37:15 +0100 <Hecate> but then you deport complexity elsewhere, downstream
2022-03-08 12:37:19 +0100 <maerwald> but that means you want your primitives to express something meaningful, but not have many of those primitives
2022-03-08 12:37:31 +0100 <maerwald> so you could say horizontal vs vertical complexity
2022-03-08 12:37:37 +0100 <c_wraith> the solution must be as complex as the problem, yes. But that puts a lower bound on complexity that little software approaches.
2022-03-08 12:37:48 +0100 <Hecate> that's why I don't like the argument of building "simple", "minimal" language. It just means a tonne of boilerplate downstream while the compiler authors are wanking over their LoC count
2022-03-08 12:37:59 +0100 <c_wraith> Most software has a lot of complexity it doesn't need to
2022-03-08 12:38:37 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net)
2022-03-08 12:38:50 +0100 <maerwald> There are only two ways to build correct systems: 1. DSL that carry proofs, 2. everything else with manual proofs
2022-03-08 12:39:05 +0100 <maerwald> both things exist
2022-03-08 12:39:27 +0100 <maerwald> and Haskell is only used in the first and to a lesser degree
2022-03-08 12:40:54 +0100 <Hecate> yeah I'm not saying Haskell produces correct programs by construction
2022-03-08 12:41:01 +0100 <Hecate> it's not a prover
2022-03-08 12:41:03 +0100 <Hecate> but it help
2022-03-08 12:41:04 +0100yauhsien(~Yau-Hsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 12:41:05 +0100 <Hecate> *helps
2022-03-08 12:41:09 +0100 <kuribas> maerwald: correctness automatically implies less "wiggle room".
2022-03-08 12:41:19 +0100 <kuribas> I guess that's why a lot of people don't like it.
2022-03-08 12:41:55 +0100 <maerwald> Hecate: depends on the domain
2022-03-08 12:42:04 +0100 <kuribas> It gives you the feeling you have less flexibility.
2022-03-08 12:42:14 +0100 <kuribas> But I think the flexibility is just different, not less.
2022-03-08 12:42:21 +0100 <maerwald> I have more confidence in rust, when doing low-level stuff with posix APIs
2022-03-08 12:42:54 +0100 <maerwald> but rust is so verbose, my fingers hurt afterwards
2022-03-08 12:44:13 +0100vglfr(~vglfr@88.155.96.35) (Ping timeout: 272 seconds)
2022-03-08 12:44:18 +0100 <maerwald> Haskell is just more pleasure to code
2022-03-08 12:44:28 +0100 <maerwald> and pleasure is more important than correctness to me
2022-03-08 12:44:52 +0100 <maerwald> pleasure also affects productivity
2022-03-08 12:45:16 +0100lumberjack123(~alMalsamo@gateway/tor-sasl/almalsamo) (Ping timeout: 240 seconds)
2022-03-08 12:45:48 +0100 <tomsmeding> maerwald: s/correctness/proven correctness/ ?
2022-03-08 12:47:14 +0100 <maerwald> tomsmeding: hmm...
2022-03-08 12:47:22 +0100Erutuon(~Erutuon@user/erutuon) (Ping timeout: 272 seconds)
2022-03-08 12:47:39 +0100 <maerwald> I mean, typescripts type system isn't really *correct*, yet it's pleasure (unless you hit those few corner cases)
2022-03-08 12:49:10 +0100glguy(x@libera/staff/glguy) (Read error: Connection reset by peer)
2022-03-08 12:49:13 +0100 <maerwald> I rarely need proven correctness
2022-03-08 12:49:29 +0100glguy(x@libera/staff/glguy)
2022-03-08 12:50:31 +0100 <tomsmeding> isn't typescript's type system more like "as long as you don't do x,y,z dumb thing, it's type-safe"?
2022-03-08 12:50:36 +0100 <maerwald> yeah
2022-03-08 12:50:48 +0100 <maerwald> which is fine most of the time
2022-03-08 12:50:49 +0100 <tomsmeding> it's a partial correctness proof then
2022-03-08 12:50:50 +0100 <tomsmeding> yeah
2022-03-08 12:51:17 +0100 <tomsmeding> as long as you don't use unsafeCoerce and friends, Haskell is also pretty strong
2022-03-08 12:51:58 +0100 <tomsmeding> the existence of ways to still make bugs doesn't make measures to prevent lots of bugs bad
2022-03-08 12:52:42 +0100 <maerwald> I'm not satisfied with IO stuff in Haskell. It's either naive (most of base), has odd custom abstractions (process package) or incomplete bindings (unix package)
2022-03-08 12:53:20 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
2022-03-08 12:54:14 +0100 <maerwald> other languages have more thoughtful stdlibs
2022-03-08 12:54:49 +0100 <maerwald> that's the "correctness" I care about
2022-03-08 12:55:20 +0100 <tomsmeding> because your non-IO code is clear enough that you don't need any extra assurance?
2022-03-08 12:55:35 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 12:57:59 +0100 <maerwald> IO is the hardest
2022-03-08 12:58:06 +0100 <tomsmeding> in your application domain
2022-03-08 12:58:21 +0100 <maerwald> I've not yet seen a domain where it isn't
2022-03-08 12:58:26 +0100 <tomsmeding> compilers?
2022-03-08 12:58:34 +0100 <tomsmeding> I know, unimaginative example
2022-03-08 12:59:02 +0100 <tomsmeding> a compiler doesn't do a lot of interesting IO, barring TH handling in GHC I guess
2022-03-08 12:59:47 +0100 <maerwald> tomsmeding: What happens when you compile a file?
2022-03-08 13:00:07 +0100 <tomsmeding> you read the file, read some more files, and write an output file
2022-03-08 13:00:08 +0100 <maerwald> first you read it, then you produce artifacts, what if you ctrl+c during that... will the object file be deleted?
2022-03-08 13:00:10 +0100 <maerwald> etc. etc.
2022-03-08 13:00:25 +0100 <maerwald> you see this happening with cabal breaking it's dist-newstyle/ dir
2022-03-08 13:00:42 +0100 <tomsmeding> true, there is more stuff than a simple programmer would see at first glance
2022-03-08 13:01:00 +0100 <tomsmeding> but I think it's less complex than ghc's simplification engine
2022-03-08 13:01:40 +0100 <tomsmeding> and producing broken compilation artifacts if someone ^C's the compilation is annoying, but not as destructive as quiet miscompilation
2022-03-08 13:05:23 +0100 <tomsmeding> (but of course, I'm biased)
2022-03-08 13:05:57 +0100lambdabot(~lambdabot@haskell/bot/lambdabot) (Remote host closed the connection)
2022-03-08 13:06:23 +0100lambdabot(~lambdabot@silicon.int-e.eu)
2022-03-08 13:06:23 +0100lambdabot(~lambdabot@silicon.int-e.eu) (Changing host)
2022-03-08 13:06:23 +0100lambdabot(~lambdabot@haskell/bot/lambdabot)
2022-03-08 13:07:48 +0100int-e(~noone@int-e.eu) (Remote host closed the connection)
2022-03-08 13:08:28 +0100 <maerwald> the RTS is all IO, allocation, primops, ...
2022-03-08 13:09:15 +0100int-e(~noone@int-e.eu)
2022-03-08 13:13:15 +0100 <tomsmeding> also true, so there's both
2022-03-08 13:13:21 +0100jinsun__(~jinsun@user/jinsun) (Ping timeout: 272 seconds)
2022-03-08 13:13:49 +0100bontaq(~user@ool-45779fe5.dyn.optonline.net)
2022-03-08 13:13:59 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 13:16:00 +0100 <maerwald> another example... if you look at the ouroboros consensus protocol of cardano, it's all very heavy type level Haskell code. But what's really difficult is that all this blockchain foo is distributed IO actions
2022-03-08 13:16:27 +0100 <maerwald> and very few people can reason about it
2022-03-08 13:21:21 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
2022-03-08 13:21:36 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 13:23:03 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 13:25:54 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) (Ping timeout: 256 seconds)
2022-03-08 13:25:54 +0100jespada(~jespada@148.252.132.235) (Read error: Connection reset by peer)
2022-03-08 13:27:13 +0100LiaoTao_(~LiaoTao@gateway/tor-sasl/liaotao)
2022-03-08 13:27:29 +0100agumonkey(~user@88.163.231.79)
2022-03-08 13:27:36 +0100LiaoTao(~LiaoTao@gateway/tor-sasl/liaotao) (Ping timeout: 240 seconds)
2022-03-08 13:33:00 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
2022-03-08 13:33:59 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 13:34:40 +0100thevishy(~Nishant@49.37.242.151)
2022-03-08 13:38:35 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net)
2022-03-08 13:45:32 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab)
2022-03-08 13:47:59 +0100bahamas(~lucian@84.232.140.52)
2022-03-08 13:49:37 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab) (Ping timeout: 240 seconds)
2022-03-08 13:50:00 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
2022-03-08 13:50:20 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 13:52:36 +0100CiaoSen(~Jura@p200300c95737a2002a3a4dfffe84dbd5.dip0.t-ipconnect.de)
2022-03-08 13:55:35 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2022-03-08 13:56:27 +0100Kaipi(~Kaiepi@156.34.47.253) (Remote host closed the connection)
2022-03-08 13:59:23 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net)
2022-03-08 13:59:29 +0100Kaipi(~Kaiepi@156.34.47.253)
2022-03-08 13:59:46 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
2022-03-08 14:02:25 +0100Inst(~Liam@2601:6c4:4080:3f80:112d:add3:9747:500f)
2022-03-08 14:05:25 +0100anon04088520(~anon04088@host-92-19-98-150.as13285.net) ()
2022-03-08 14:06:00 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2022-03-08 14:09:13 +0100 <ProfSimm> FP is flawed because immutability of a piece of state or code is an assumption that's always wrong in the long term.
2022-03-08 14:10:21 +0100bahamas(~lucian@84.232.140.52) (Ping timeout: 272 seconds)
2022-03-08 14:12:11 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Remote host closed the connection)
2022-03-08 14:14:00 +0100 <hpc> that's like saying types are flawed because in the long term everything's a string
2022-03-08 14:14:49 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 14:14:54 +0100jao(~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net)
2022-03-08 14:15:16 +0100jinsun(~jinsun@user/jinsun)
2022-03-08 14:15:28 +0100 <ProfSimm> hpc: yes. Except I wouldn't say string.
2022-03-08 14:15:47 +0100 <ProfSimm> hpc: in the long term everything's an actor.
2022-03-08 14:16:23 +0100 <hpc> and all the world's a staging environment? :D
2022-03-08 14:17:48 +0100 <maerwald> everything's an actor suspiciously sounds like Java
2022-03-08 14:18:12 +0100 <hpc> actors are more a smalltalk thing
2022-03-08 14:18:18 +0100 <hpc> in java everything's a bean
2022-03-08 14:18:23 +0100 <hpc> and in erlang everything's a process
2022-03-08 14:19:34 +0100gnyeki(~gnyeki@user/gnyeki) (Quit: leaving)
2022-03-08 14:20:28 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
2022-03-08 14:20:42 +0100 <ProfSimm> hpc: I'd say Erlang's the most apt implementation of actors we have so far.
2022-03-08 14:20:50 +0100 <ProfSimm> Process = actor.
2022-03-08 14:21:05 +0100 <hpc> probably yeah
2022-03-08 14:21:16 +0100 <ProfSimm> That said Erlang processes are internally functional
2022-03-08 14:21:28 +0100 <ProfSimm> But they're small so it's kinda manageable
2022-03-08 14:22:45 +0100gnyeki(~gnyeki@user/gnyeki)
2022-03-08 14:23:00 +0100 <ProfSimm> Something I don't understand
2022-03-08 14:23:10 +0100 <ProfSimm> Functional programming often uses CSP in compilers
2022-03-08 14:23:19 +0100 <ProfSimm> But how does functional reduction work in CPS
2022-03-08 14:23:23 +0100 <ProfSimm> CPS sorry not CSP
2022-03-08 14:23:42 +0100 <ProfSimm> If CPS is all about calling things, what are we "reducing"
2022-03-08 14:24:44 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e)
2022-03-08 14:26:50 +0100 <kuribas> ProfSimm: you change the state, but don't mutate it.
2022-03-08 14:27:07 +0100 <kuribas> ProfSimm: you just update it.
2022-03-08 14:27:15 +0100 <kuribas> ProfSimm: it's the same result, but without mutation.
2022-03-08 14:31:26 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
2022-03-08 14:34:02 +0100ChaiTRex(~ChaiTRex@user/chaitrex)
2022-03-08 14:35:47 +0100chenqisu1(~chenqisu1@183.217.201.47) (Ping timeout: 252 seconds)
2022-03-08 14:35:56 +0100soxen(~bob@pool-173-54-217-168.nwrknj.fios.verizon.net)
2022-03-08 14:36:16 +0100boborygmy(~bob@pool-173-54-217-168.nwrknj.fios.verizon.net)
2022-03-08 14:37:34 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 272 seconds)
2022-03-08 14:37:45 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 14:38:11 +0100 <ProfSimm> kuribas: change and mutate mean the same thing
2022-03-08 14:38:36 +0100Pickchea(~private@user/pickchea)
2022-03-08 14:41:18 +0100 <kuribas> ProfSimm: change by replacing it.
2022-03-08 14:41:31 +0100 <kuribas> Using a state monad or IORef.
2022-03-08 14:41:36 +0100 <kuribas> But you don't mutate the contents.
2022-03-08 14:41:52 +0100 <kuribas> It actually make concurrency much easier.
2022-03-08 14:42:43 +0100acidjnk(~acidjnk@p200300d0c7049f27690562e0ba62f824.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
2022-03-08 14:42:59 +0100jespada(~jespada@148.252.132.235)
2022-03-08 14:44:50 +0100 <ProfSimm> kuribas: replacing it implies you're taking something from a place, and putting something else in its place
2022-03-08 14:44:55 +0100 <ProfSimm> kuribas: you mutated the place
2022-03-08 14:45:34 +0100 <kuribas> For IORef yes.
2022-03-08 14:45:38 +0100 <kuribas> For State, no.
2022-03-08 14:45:54 +0100 <kuribas> The effect is the same though.
2022-03-08 14:46:31 +0100 <kuribas> Especially in a concurrent setting, not mutating the content is an important distinction.
2022-03-08 14:47:05 +0100 <ProfSimm> kuribas: creating a copy with a change is not the same as changing.
2022-03-08 14:47:23 +0100 <ProfSimm> kuribas: also in concurrent setting you can still mutate, just use linear types
2022-03-08 14:47:39 +0100 <kuribas> linear types are overrated.
2022-03-08 14:47:41 +0100 <ProfSimm> kuribas: the abstractions Haskell provides is a bit like a way to avoid implementing linear types
2022-03-08 14:48:01 +0100 <kuribas> at least when I tried them in idris.
2022-03-08 14:48:40 +0100 <ProfSimm> kuribas: are they. a linear typeis mutable. If you have a continuous block of memory of 2MB and you want one byte changed in it, you just change it. How you do that in Haskell
2022-03-08 14:49:05 +0100 <kuribas> you don't.
2022-03-08 14:49:11 +0100 <ProfSimm> Great
2022-03-08 14:49:29 +0100 <ProfSimm> Well in that case linear types are not overrated :)
2022-03-08 14:49:42 +0100 <kuribas> Or use a vector with ST.
2022-03-08 14:49:51 +0100 <kuribas> Or whatever suits the problem.
2022-03-08 14:49:54 +0100 <ProfSimm> Doesn't match the requirements
2022-03-08 14:50:06 +0100 <ProfSimm> Rust uses linear types, and it's both concurrently safe, and can write kernel code.
2022-03-08 14:50:11 +0100 <kuribas> I don't know your requirements.
2022-03-08 14:50:25 +0100 <ProfSimm> kuribas: well it was: block of 2MB memory, change a byte
2022-03-08 14:50:35 +0100 <kuribas> I know that on a SSD, changing one byte will copy 4MBs of data.
2022-03-08 14:50:53 +0100 <ProfSimm> I think you mean 4k
2022-03-08 14:50:55 +0100 <kuribas> ProfSimm: that's an impementation detail, not a requirement.
2022-03-08 14:51:00 +0100 <merijn> I mean, you just use "Ptr Word8" and IO
2022-03-08 14:51:02 +0100 <ProfSimm> That's because storage devices are block devices
2022-03-08 14:51:05 +0100 <kuribas> right, 4k.
2022-03-08 14:51:41 +0100 <merijn> ProfSimm: I mean, you can literally just use the same approach as C and allocate a pointer to 2MB of bytes and update any arbitrary byte
2022-03-08 14:51:45 +0100 <kuribas> ProfSimm: change one byte in 2MB of memory is not a requirement, it's one possible solution for some problems.
2022-03-08 14:51:54 +0100 <ProfSimm> kuribas: however SSD doesn't map its contents linearly, it's about locality
2022-03-08 14:52:29 +0100 <kuribas> So first, I'd like to know what problem you need to solve. And as merijn says, if needed you can just use IO.
2022-03-08 14:52:33 +0100 <ProfSimm> kuribas: the problem is locality in general
2022-03-08 14:53:01 +0100 <ProfSimm> Replacing Earth when you have to turn on the light is not pragmatic. Even if you reuse most parts
2022-03-08 14:53:33 +0100 <kuribas> I'd say, the problem in general if making programs which are easy to reason about, easy to maintain, etc...
2022-03-08 14:54:02 +0100 <ProfSimm> Working with Lenses is not easy to reason about.
2022-03-08 14:54:05 +0100 <kuribas> So if you need to optimize for performance, I'd first look for architectural and algorithmic changes.
2022-03-08 14:54:36 +0100 <kuribas> Optimizing cache locality is onely a late change.
2022-03-08 14:55:09 +0100 <kuribas> However, speaking generally. For some problems (matrix operations, linear algebra) it could be important.
2022-03-08 14:55:25 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net) (Ping timeout: 256 seconds)
2022-03-08 14:56:57 +0100 <kuribas> ProfSimm: I'd go for immutability by default, only if it is really not possible, use mutation.
2022-03-08 14:57:07 +0100xff0x(~xff0x@dslb-094-222-029-254.094.222.pools.vodafone-ip.de) (Ping timeout: 256 seconds)
2022-03-08 14:57:47 +0100 <kuribas> Just responding to your "FP is flawed" argument, I don't mean immutable works for every problem.
2022-03-08 14:57:54 +0100 <ProfSimm> kuribas: sure
2022-03-08 14:58:08 +0100 <kuribas> But often we make immutable abstractions which actually mutate "under the hood", like bytestrings.
2022-03-08 14:58:13 +0100 <kuribas> or bytestring builders.
2022-03-08 14:58:30 +0100 <kuribas> You use them as if they are immutable, but under the hood they just fill buffers mutably.
2022-03-08 14:58:33 +0100 <ProfSimm> kuribas: I think immutability is a "local assumption" that's wrong in a wider scale. So a language should basically allow this recursive approach to immutability.
2022-03-08 14:59:28 +0100 <ProfSimm> kuribas: i.e. "in this moment right now, x y z are immutable" then you get out of this context, they're linear and mutable, but a b c are immutable. You get out in a wider context, a b c are linear and mutable.
2022-03-08 14:59:36 +0100 <ProfSimm> kuribas: so you can kinda work at the right level
2022-03-08 15:00:18 +0100 <ProfSimm> Haskell implements half of that
2022-03-08 15:00:29 +0100 <ProfSimm> Hides the other half in the runtime, and IO and what not
2022-03-08 15:00:40 +0100 <ProfSimm> If it make it explicit, I think it'd be even more powerful
2022-03-08 15:01:39 +0100 <kuribas> I don't know, I have yet to see the advantage of linear types. But I heared they work well in rust, which is on my list of languages to learn :)
2022-03-08 15:01:56 +0100 <kuribas> I guess affine types they are called?
2022-03-08 15:02:56 +0100off^(~off@50.232.121.75)
2022-03-08 15:02:59 +0100 <kuribas> however rust is not haskell, haskell is not rust
2022-03-08 15:03:10 +0100kadoban(~kadoban@user/kadoban)
2022-03-08 15:03:21 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 15:03:28 +0100 <ProfSimm> kuribas: yes affine means used at most once, linear exactly once. But it's the same idea.
2022-03-08 15:03:54 +0100 <ProfSimm> kuribas: in Rust you can make a single mutable borrow, OR multiple immutable borrows. The latter half is kinda like Haskell
2022-03-08 15:04:00 +0100ystael(~ystael@user/ystael)
2022-03-08 15:04:14 +0100 <ProfSimm> kuribas: but if you get back your immutable borrows, now you can mutate the thing, before you reshare it immutably.
2022-03-08 15:04:23 +0100 <ProfSimm> kuribas: it's kinda like State/IO if you squint
2022-03-08 15:04:25 +0100 <kuribas> right
2022-03-08 15:04:26 +0100 <ProfSimm> But made explicit
2022-03-08 15:07:22 +0100neurocyte0917090(~neurocyte@IP-045014190241.dynamic.medianet-world.de)
2022-03-08 15:07:22 +0100neurocyte0917090(~neurocyte@IP-045014190241.dynamic.medianet-world.de) (Changing host)
2022-03-08 15:07:22 +0100neurocyte0917090(~neurocyte@user/neurocyte)
2022-03-08 15:07:58 +0100worldhelloworld(~c1utt4r@vmi275462.contaboserver.net) (Ping timeout: 272 seconds)
2022-03-08 15:09:15 +0100xff0x(~xff0x@dslb-094-222-029-254.094.222.pools.vodafone-ip.de)
2022-03-08 15:11:32 +0100 <ProfSimm> kuribas: rust is not haskell, and rust does a lot of things i wish Haskell doesn't, but I feel there's core idea that could scale from the kernel to math proofs to scripting. If we get it right, we won't need 1000 languages
2022-03-08 15:12:41 +0100bahamas(~lucian@84.232.140.52)
2022-03-08 15:13:24 +0100jespada(~jespada@148.252.132.235) (Read error: Connection reset by peer)
2022-03-08 15:15:12 +0100jespada(~jespada@148.252.132.235)
2022-03-08 15:17:17 +0100bahamas(~lucian@84.232.140.52) (Ping timeout: 256 seconds)
2022-03-08 15:18:17 +0100 <geekosaur> uh
2022-03-08 15:18:40 +0100 <geekosaur> ob https://xkcd.com/927/
2022-03-08 15:19:54 +0100 <maerwald> that's the most prominent fallacy of programmers talking about programming languages... they only talk about technical properties
2022-03-08 15:20:29 +0100 <geekosaur> and in any case different languages often make meeting specific requirements easier while making others harder. for example, Ive worked with real time control languages, they workvery wellfor that but areless than idea for generalcomputation
2022-03-08 15:21:10 +0100 <geekosaur> something like matlab or octave is very good for matrix related math but lousy for anything else
2022-03-08 15:21:31 +0100 <geekosaur> similarly r/s and plotting/charts/data relationships
2022-03-08 15:22:18 +0100 <geekosaur> sql's a great database access language but worthless for anything else; conversely anything other than just packaging up an sql query to access a databaseis painful in other languages
2022-03-08 15:23:04 +0100lbseale(~ep1ctetus@user/ep1ctetus) (Read error: Connection reset by peer)
2022-03-08 15:23:29 +0100 <maerwald> it's like saying english is the best language, because it has the most words
2022-03-08 15:24:23 +0100 <geekosaur> pl/I tried to be a do-everything language. it was less than successful
2022-03-08 15:24:27 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
2022-03-08 15:25:43 +0100neurocyte0917090(~neurocyte@user/neurocyte) (Ping timeout: 272 seconds)
2022-03-08 15:26:57 +0100 <kuribas> geekosaur: well, hasure thinks SQL is great for graphql APIs
2022-03-08 15:27:44 +0100 <maerwald> I think we should accept that even programming languages have cultural context and that personal preferences of ergonomics and pleasure may be far more important than technical properties
2022-03-08 15:27:52 +0100 <geekosaur> ^
2022-03-08 15:28:17 +0100 <geekosaur> and corporate preferences and contexts
2022-03-08 15:28:58 +0100 <ProfSimm> maerwald: I'd be fine if English became the only language
2022-03-08 15:29:08 +0100 <ProfSimm> maerwald: in fact, I strongly would prefer it
2022-03-08 15:29:24 +0100 <geekosaur> lotsof others would disagree
2022-03-08 15:29:30 +0100 <ProfSimm> They're wrong.
2022-03-08 15:30:30 +0100 <ProfSimm> geekosaur: a good language would permit DSLs for specific purposes.
2022-03-08 15:30:45 +0100 <kuribas> ProfSimm: Ik geef de voorkeur aan nederlands :)
2022-03-08 15:31:10 +0100 <ProfSimm> geekosaur: imagine the world if you could only write libraries in C, because only C supports the C ABI
2022-03-08 15:31:15 +0100 <geekosaur> that was PL/I-think
2022-03-08 15:31:17 +0100 <geekosaur> it failed
2022-03-08 15:31:37 +0100 <geekosaur> hey, that was largely true for a couple decades
2022-03-08 15:31:48 +0100off^(~off@50.232.121.75) (Remote host closed the connection)
2022-03-08 15:32:01 +0100 <ProfSimm> geekosaur: so we're happy now when many languages use the same ABI right
2022-03-08 15:32:20 +0100 <ProfSimm> geekosaur: I wanna move the bar up. Everyone uses the same basic language, and everything is a DSL in it
2022-03-08 15:32:28 +0100 <geekosaur> because of the historical accident that C compilers were for a while moe readily available to programmers than expensive then-"mainstream" languages
2022-03-08 15:32:49 +0100 <geekosaur> again, that was PL/I-think
2022-03-08 15:33:28 +0100 <geekosaur> you end up with a huge ungainly language that's nearly impossible to compile and get reasonable performance out of
2022-03-08 15:33:41 +0100 <geekosaur> (this might even sound familiar to some people…)
2022-03-08 15:34:25 +0100kongsheng(~kongsheng@71.28.228.142)
2022-03-08 15:36:12 +0100 <kongsheng> Hello. I have a mathematical model which consists of a semigroup (or magma). It's a set with a binary operation defined by a table. What kind of background reading do I need to code this in haskell? I know absolutely nothing about programming computers.
2022-03-08 15:36:37 +0100euandreh(~euandreh@2804:14c:33:9fe5:7f03:8b0:a81c:56d7) (Ping timeout: 240 seconds)
2022-03-08 15:36:43 +0100jinsun__(~jinsun@user/jinsun)
2022-03-08 15:37:06 +0100 <romesrf> how can I ask for a function type here?
2022-03-08 15:39:24 +0100jinsun(~jinsun@user/jinsun) (Ping timeout: 240 seconds)
2022-03-08 15:42:13 +0100 <romesrf> auto reply: geekosaur answered elsewhere, it's just :t
2022-03-08 15:42:15 +0100 <romesrf> :t id
2022-03-08 15:42:16 +0100 <lambdabot> a -> a
2022-03-08 15:44:08 +0100jespada(~jespada@148.252.132.235) (Read error: Connection reset by peer)
2022-03-08 15:47:18 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab)
2022-03-08 15:47:31 +0100jespada(~jespada@148.252.132.235)
2022-03-08 15:51:24 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab) (Ping timeout: 240 seconds)
2022-03-08 15:52:44 +0100bahamas(~lucian@84.232.140.52)
2022-03-08 15:54:25 +0100shailangsa(~shailangs@host86-186-133-59.range86-186.btcentralplus.com) (Remote host closed the connection)
2022-03-08 15:57:00 +0100bahamas(~lucian@84.232.140.52) (Ping timeout: 240 seconds)
2022-03-08 16:00:21 +0100 <siers> what are some cool uses of bijections/invertible functions? I suppose you could compose a bunch of them together to achieve something quite magical
2022-03-08 16:02:30 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Remote host closed the connection)
2022-03-08 16:03:02 +0100alp(~alp@user/alp) (Ping timeout: 240 seconds)
2022-03-08 16:03:08 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 16:03:48 +0100ishutin(~ishutin@87-97-30-219.pool.digikabel.hu) (Ping timeout: 252 seconds)
2022-03-08 16:04:03 +0100 <siers> % :t (1, "x", [()]) -- I think this should work, romesrf
2022-03-08 16:04:03 +0100 <yahb> siers: Num a => (a, String, [()])
2022-03-08 16:04:45 +0100 <siers> if you meant in IRC, specifically
2022-03-08 16:05:27 +0100ishutin(~ishutin@87-97-82-131.pool.digikabel.hu)
2022-03-08 16:05:54 +0100CiaoSen(~Jura@p200300c95737a2002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2022-03-08 16:07:24 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 240 seconds)
2022-03-08 16:07:42 +0100 <kuribas> kongsheng: the interesting question is, what do you want to do with it?
2022-03-08 16:07:57 +0100 <kuribas> why do you want to code it?
2022-03-08 16:09:20 +0100 <kuribas> haskell has a Semigroup typeclass
2022-03-08 16:10:38 +0100 <kongsheng> kuribas: I want to start with a set {x,y} as well as a binary operation that is defined by a table. The binary operation is not associative by nature. I want to code it because the semigroup represents a thing in the real world, and I need a framework for testing whether the abstract mathematics works physically.
2022-03-08 16:11:41 +0100 <kuribas> isn't a semigroup supposed to be associative?
2022-03-08 16:12:30 +0100 <kongsheng> OH! Sorry! I am actually starting with something called a Magma instead of a semigroup.
2022-03-08 16:12:39 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2022-03-08 16:12:41 +0100 <kongsheng> Dang.
2022-03-08 16:12:47 +0100[_](~itchyjunk@user/itchyjunk/x-7353470)
2022-03-08 16:14:00 +0100[_](~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection)
2022-03-08 16:17:30 +0100 <kongsheng> Basically, what I want to do is start with a set {x,y} and this binary operation. I need an operator * to represent the binary operation. So I can symbolically do things like x*y*x*x etc. I am building a second function which depends on the first. The third function depends on the first two. The operators are ~ and +. So then I can build
2022-03-08 16:17:31 +0100 <kongsheng> expressions like x*y + ~x*y + ~x*~y. Given one of these expressions. I want to instantiate an object where the set {x,y} has been made more concrete with {0,1}. Then I need to build expressions i.e. ~(x*y + ~x*~*y) but have an option to evaluate them with the instantiated, concrete set.
2022-03-08 16:18:51 +0100 <kongsheng> But the problem is that I know nothing about haskell or programming, and my initial set with binary operation is non-associative.
2022-03-08 16:18:52 +0100 <sclv> so a magma has no laws to verify
2022-03-08 16:19:25 +0100 <kongsheng> The only law is that the operation remained closed, I think. That must be checked.
2022-03-08 16:19:27 +0100 <sclv> the rest is straightforward if you know haskell, but i don't think its something that you can learn how to do if you don't really learn the language first
2022-03-08 16:19:44 +0100nisstyre(~wes@user/nisstyre) (Quit: WeeChat 3.2.1)
2022-03-08 16:20:11 +0100 <sclv> if you encode your magma as a datatype (rather than just associating it to some subset of the naturals) then it will be definitionally closed
2022-03-08 16:20:32 +0100 <sclv> and even otherwise, its easy enough to read off by hand from the "multiplication table" if it is
2022-03-08 16:20:43 +0100 <kongsheng> Cool. I can probably do it in Mathematica but I don't have the money and would rather keep this study as Haskell as possible since it has theoretical underpinnings to Computer Science.
2022-03-08 16:21:36 +0100 <siers> sclv, what do you mean by "associating it to some subset of the naturals"?
2022-03-08 16:21:51 +0100 <kongsheng> Yea I see what  you mean. I kind of want to build a skeleton Magma and then build a particular Magma with my binary operation and set.
2022-03-08 16:22:01 +0100 <kongsheng> But hey thanks for giving me some ideas.
2022-03-08 16:22:19 +0100 <sclv> so the most straightforward thing in haskell is to not do that, but to define a specific datatype for each particular magma
2022-03-08 16:22:28 +0100 <sclv> or semigroup, or monoid
2022-03-08 16:22:33 +0100 <sclv> and again -- doing it for a magma seems pointless
2022-03-08 16:22:34 +0100 <siers> Wouldn't a typeclass for the magma be appropriate? I assume not, otherwise you (sclv) would've suggested it.
2022-03-08 16:22:56 +0100 <kongsheng> Ok. So use datatype logic instead of Object Oriented logic?
2022-03-08 16:23:21 +0100 <sclv> then, as siers suggested, you can make that datatype an instance of the appropriate typeclass
2022-03-08 16:23:51 +0100 <sclv> then you auto-derive some insteances and can use something like https://hackage.haskell.org/package/quickcheck-classes-0.6.5.0/docs/Test-QuickCheck-Classes.html to generate and run testcases for the properties you want
2022-03-08 16:24:06 +0100 <kongsheng> Hmm, maybe I don't need a skeleton framework at all, since like you said, all I have to do is check closure by the mult table.
2022-03-08 16:24:18 +0100 <sclv> but again, doing things this way requires knowing some haskell, otherwise you will get confused very quickly
2022-03-08 16:24:51 +0100 <kongsheng> Cool. I will do some reading and some more headwork.
2022-03-08 16:26:30 +0100 <kongsheng> The mathematics is more primitive than Boolean algebra and Logic, but my research group is trying to find out if we can start with this particular Magma and reach a turing complete device.
2022-03-08 16:26:47 +0100 <sclv> this isn't working with a general AST of your expressions btw, just letting you evaluate them directly
2022-03-08 16:27:46 +0100 <sclv> if you want to build an expression syntax tree to programmatically manipulate them, then you can do that too. there are lots of examples of this. the first i found on a google (idk if its good or not, just the first i found on a google) is something like https://john.cs.olemiss.edu/~hcc/csci450/ELIFP/Ch42/42_Abstract_Syntax.html
2022-03-08 16:28:02 +0100 <shapr> > let ones = 1 : ones in take 5 ones
2022-03-08 16:28:03 +0100 <lambdabot> [1,1,1,1,1]
2022-03-08 16:28:05 +0100 <kongsheng> ok thank you. I am writing all this down by the way.
2022-03-08 16:31:06 +0100 <kuribas> kongsheng: you can try macsyma, which is a free mathematica alternative.
2022-03-08 16:31:30 +0100 <kuribas> kongsheng: if you want to prove mathematical things, a dependently typed language could be better, like agda or idris.
2022-03-08 16:32:17 +0100Inst(~Liam@2601:6c4:4080:3f80:112d:add3:9747:500f) (Ping timeout: 240 seconds)
2022-03-08 16:33:28 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds)
2022-03-08 16:33:58 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 16:34:25 +0100bahamas(~lucian@84.232.140.52)
2022-03-08 16:35:17 +0100jz99_(~jz99@pa49-186-65-17.pa.vic.optusnet.com.au)
2022-03-08 16:35:18 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2022-03-08 16:35:42 +0100Inst(~Liam@2601:6c4:4080:3f80:8c26:e871:cea5:bbc0)
2022-03-08 16:36:40 +0100shapr(~user@pool-173-73-44-186.washdc.fios.verizon.net) (Read error: Connection reset by peer)
2022-03-08 16:36:47 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 252 seconds)
2022-03-08 16:37:09 +0100jz99_(~jz99@pa49-186-65-17.pa.vic.optusnet.com.au) (Remote host closed the connection)
2022-03-08 16:37:42 +0100 <sclv> if they don't even know haskell yet, sending them down the road to a dependently typed language is Not Good Advice
2022-03-08 16:37:54 +0100shapr(~user@pool-173-73-44-186.washdc.fios.verizon.net)
2022-03-08 16:38:18 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
2022-03-08 16:38:31 +0100 <kuribas> sclv: why not? There is a lot of DT teaching material which is self contained.
2022-03-08 16:38:44 +0100 <kuribas> Do DT languages assume haskell knowledge?
2022-03-08 16:38:47 +0100 <sclv> i won't argue. i'll just say that it requires a lot more ramp up
2022-03-08 16:38:57 +0100 <sclv> this person said they had virtually no programming background full stop
2022-03-08 16:39:17 +0100 <sclv> and they were looking to do computational checks not proofs
2022-03-08 16:39:32 +0100 <kuribas> I don't disagree, but I thought that idris or agda are more mathy...
2022-03-08 16:40:28 +0100 <sclv> they're suited for being proof assistants. doing symbolic computation and generated verification is very much in the haskell wheelhouse
2022-03-08 16:40:43 +0100 <sclv> not all maths is formal theorem proving!!!
2022-03-08 16:41:23 +0100 <juri_> not all math is formal theorem proving.. yet.
2022-03-08 16:41:39 +0100notzmv(~zmv@user/notzmv) (Ping timeout: 268 seconds)
2022-03-08 16:41:58 +0100 <siers> what kind of symbolic computation is haskell good at? how does that work even
2022-03-08 16:42:04 +0100 <siers> or what is meant by that
2022-03-08 16:42:41 +0100 <geekosaur> > foldr (*) z [a,b,c] -- looks symbolic to me :þ
2022-03-08 16:42:42 +0100 <lambdabot> a * (b * (c * z))
2022-03-08 16:42:46 +0100 <sclv> i mean that haskell is an excellent language for creating and manipulating ASTs -- what is commonly known as "computer algebra"
2022-03-08 16:44:57 +0100 <siers> geekosaur, hm
2022-03-08 16:45:06 +0100 <kuribas> surprising no CAS are written in haskell.
2022-03-08 16:45:41 +0100 <geekosaur> @hackage simple-reflect -- siers
2022-03-08 16:45:41 +0100 <lambdabot> https://hackage.haskell.org/package/simple-reflect -- siers
2022-03-08 16:46:12 +0100 <siers> nice
2022-03-08 16:46:24 +0100 <kuribas> that cannot even rewrite or simplify expressions.
2022-03-08 16:47:12 +0100 <geekosaur> true, but it shows the possibilities. and I'd suspect something more capable could be written. I have no idea why it hasn't yet, unlessit's just that it already exists elsewhere
2022-03-08 16:47:17 +0100 <siers> how was 1+2*(3+4) captured?
2022-03-08 16:47:28 +0100 <siers> yeah, the examples within illustrate what was meant by symbolic computation
2022-03-08 16:48:00 +0100 <polyphem> geekosaur: is that term rewriting (foldr example) possible also in ghci or is it a lambdabot feature ?
2022-03-08 16:48:17 +0100ec_(~ec@gateway/tor-sasl/ec) (Quit: ec_)
2022-03-08 16:48:23 +0100 <kuribas> polyphem: it's just a library
2022-03-08 16:48:31 +0100 <geekosaur> see the hackage library I pointed to
2022-03-08 16:48:45 +0100 <geekosaur> \you could install it, import Debug.SimpleReflect into ghci, and go nuts
2022-03-08 16:49:03 +0100 <geekosaur> you do need to use a few tricks to keep it from getting confused though
2022-03-08 16:49:16 +0100 <geekosaur> > foldr (*) (0::Expr) [a,b,c,d]
2022-03-08 16:49:17 +0100 <lambdabot> a * (b * (c * (d * 0)))
2022-03-08 16:49:29 +0100 <siers> what's Expr?
2022-03-08 16:49:31 +0100 <geekosaur> well I should have used 1 but then (*) is a placeholder
2022-03-08 16:49:35 +0100 <geekosaur> it just looks nicer infix
2022-03-08 16:49:40 +0100 <siers> ah, just some data type that implements Num?
2022-03-08 16:49:48 +0100 <geekosaur> Expr is the type simple-reflect uses internally to do this
2022-03-08 16:49:59 +0100 <geekosaur> it implenments Num and a number of other typeclasses
2022-03-08 16:50:01 +0100 <siers> how does it load 0 into Expr?
2022-03-08 16:50:14 +0100 <siers> by some function by implementing Num?
2022-03-08 16:50:23 +0100 <geekosaur> that just means it has a Num instance, so fromInteger works
2022-03-08 16:50:32 +0100 <polyphem> how does it not freak out , with all those free (undefined) variables
2022-03-08 16:50:46 +0100 <siers> that's probably lambdabot magic
2022-03-08 16:50:47 +0100 <polyphem> s/variables/bindings/ :)
2022-03-08 16:51:00 +0100 <geekosaur> (remember that any literal number has `fromInteger` or `fromRational` wrapped around it automatically to allow it to be any Num or Fractional instance as appropriate
2022-03-08 16:51:11 +0100doyougnu(~doyougnu@cpe-67-249-83-190.twcny.res.rr.com)
2022-03-08 16:51:19 +0100 <geekosaur> there's no lambdabot magic there, just the Expr type
2022-03-08 16:51:43 +0100 <geekosaur> and the library binding all the single letter names to Expr or related types
2022-03-08 16:51:46 +0100 <geekosaur> :t a
2022-03-08 16:51:47 +0100 <lambdabot> Expr
2022-03-08 16:51:47 +0100 <siers> geekosaur, I knew what implementing Num means :P but right, obviously it's fromInteger
2022-03-08 16:51:50 +0100 <geekosaur> :t f
2022-03-08 16:51:51 +0100 <lambdabot> FromExpr a => a
2022-03-08 16:51:52 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2022-03-08 16:52:00 +0100 <siers> I just thought there's more to it, but no
2022-03-08 16:52:16 +0100 <geekosaur> nothing else to it, just abusing Num a lot :)
2022-03-08 16:53:27 +0100 <geekosaur> and Show instances
2022-03-08 16:55:02 +0100euandreh(~euandreh@2804:14c:33:9fe5:e5ea:1ffe:3a64:8fa7)
2022-03-08 16:55:09 +0100 <polyphem> i see , thanks
2022-03-08 16:56:41 +0100 <siers> I read TAPL a bit and I remember seeing the semantical rules to compute a value from a term... kind of eye opening to see them written out
2022-03-08 16:57:07 +0100Pickchea(~private@user/pickchea) (Quit: Leaving)
2022-03-08 17:00:29 +0100 <siers> and those rules immediately spring into mind upon seeing the reduction example in simple-reflect
2022-03-08 17:00:59 +0100euandreh(~euandreh@2804:14c:33:9fe5:e5ea:1ffe:3a64:8fa7) (Ping timeout: 250 seconds)
2022-03-08 17:01:05 +0100nisstyre(wes@user/nisstyre)
2022-03-08 17:07:00 +0100agumonkey(~user@88.163.231.79) (Ping timeout: 240 seconds)
2022-03-08 17:10:12 +0100vysn(~vysn@user/vysn) (Ping timeout: 240 seconds)
2022-03-08 17:12:39 +0100ProfSimm(~ProfSimm@87.227.196.109) (Remote host closed the connection)
2022-03-08 17:14:43 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2022-03-08 17:15:45 +0100briandaed(~root@109.95.142.93.r.toneticgroup.pl)
2022-03-08 17:15:56 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2022-03-08 17:16:57 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2022-03-08 17:17:06 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:3240:c699:b7eb:e5b0) (Quit: WeeChat 2.8)
2022-03-08 17:17:12 +0100Vajb(~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813)
2022-03-08 17:20:36 +0100 <briandaed> quick question regarding Hackage/Stackage, I see that all LTSes from 16.31 to 18.27 use network-3.1.1.1 which is deprecated - why?
2022-03-08 17:21:34 +0100Sgeo(~Sgeo@user/sgeo)
2022-03-08 17:21:38 +0100worldhelloworld1(uid543174@id-543174.helmsley.irccloud.com) (Quit: Connection closed for inactivity)
2022-03-08 17:22:39 +0100 <merijn> Presumably because not everything in the snapshots was updated to work with newer versions of network yet?
2022-03-08 17:24:53 +0100 <briandaed> ok, sounds reasonably
2022-03-08 17:26:19 +0100waleee(~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
2022-03-08 17:26:43 +0100pooryorick(~pooryoric@87-119-174-173.tll.elisa.ee) (Ping timeout: 256 seconds)
2022-03-08 17:27:26 +0100 <geekosaur> I don't think they update snapshots actually, they just release new ones
2022-03-08 17:28:43 +0100 <jneira[m]> iirc it was deprecated due to a bug affecting cabal and msys with a relatively new version of autoconf
2022-03-08 17:29:06 +0100 <jneira[m]> they released a patched version 3.1.1.2 and deprecated .1
2022-03-08 17:29:38 +0100 <jneira[m]> but it is not affecting stack it seems so 🤷
2022-03-08 17:30:09 +0100 <jneira[m]> but I guess the lts would work with 3.1.1.2
2022-03-08 17:31:14 +0100waleee(~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 252 seconds)
2022-03-08 17:31:18 +0100 <geekosaur> stack controls its version of msys so presumably can avoid the issue
2022-03-08 17:32:17 +0100pooryorick(~pooryoric@87-119-174-173.tll.elisa.ee)
2022-03-08 17:32:19 +0100 <briandaed> next is 3.1.2.0 and looks a lot happened there https://hackage.haskell.org/package/network-3.1.2.0/changelog
2022-03-08 17:32:51 +0100incertia(~incertia@207.98.163.88) (Quit: ZNC 1.7.5 - https://znc.in)
2022-03-08 17:33:49 +0100 <geekosaur> and immutability of LTSes is important for reproducible builds, which is one of stack's "selling points"
2022-03-08 17:34:17 +0100gehmehgeh(~user@user/gehmehgeh) (Quit: Leaving)
2022-03-08 17:35:00 +0100waleee(~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
2022-03-08 17:35:14 +0100 <geekosaur> (to be clear the scare quotes are only because you're "selling" something that's for free, not because I'm casting aspersions on it)
2022-03-08 17:35:23 +0100 <briandaed> again sounds reasonably, but if there is a bug in compiler or library, the only way to fix it is to use newer LTS or use some hacked version provieded in extra-deps...
2022-03-08 17:35:53 +0100 <kuribas> couldn't you implement unlift EitherT using exceptions?
2022-03-08 17:36:12 +0100incertia(~incertia@207.98.163.88)
2022-03-08 17:36:25 +0100 <geekosaur> true, but they do a lot of testing to avoid that. at some point it may let something slipthrough though, in which case they may need a way to deprecate resolvers
2022-03-08 17:36:42 +0100zer0bitz(~zer0bitz@2001:2003:f74d:b800:7859:22cf:713c:fe6e)
2022-03-08 17:37:08 +0100ec(~ec@gateway/tor-sasl/ec)
2022-03-08 17:39:28 +0100 <briandaed> then I'm cursed, one week and I encountered https://github.com/haskell-crypto/cryptonite/issues/329 and then https://github.com/haskell/network/issues/438 , LTS-16.31, pity there is no summary which LTSes are used most frequently by commercial projects, similarly to some android version - market share stats
2022-03-08 17:47:05 +0100coot(~coot@213.134.190.95) (Quit: coot)
2022-03-08 17:47:14 +0100_ht(~quassel@231-169-21-31.ftth.glasoperator.nl)
2022-03-08 17:48:09 +0100Katarushisu(~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net) (Quit: The Lounge - https://thelounge.chat)
2022-03-08 17:48:09 +0100zer0bitz_(~zer0bitz@2001:2003:f74d:b800:7859:22cf:713c:fe6e)
2022-03-08 17:48:47 +0100Katarushisu(~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net)
2022-03-08 17:48:47 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab)
2022-03-08 17:50:36 +0100ec(~ec@gateway/tor-sasl/ec) (Ping timeout: 240 seconds)
2022-03-08 17:50:46 +0100zer0bitz(~zer0bitz@2001:2003:f74d:b800:7859:22cf:713c:fe6e) (Ping timeout: 245 seconds)
2022-03-08 17:51:27 +0100Midjak(~Midjak@82.66.147.146) (Quit: This computer has gone to sleep)
2022-03-08 17:51:30 +0100Cheery(~cheery@7-239-179-185.static.tentacle.fi) (Ping timeout: 250 seconds)
2022-03-08 17:51:40 +0100Cheery(~cheery@7-239-179-185.static.tentacle.fi)
2022-03-08 17:52:05 +0100ec(~ec@gateway/tor-sasl/ec)
2022-03-08 17:52:31 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab) (Remote host closed the connection)
2022-03-08 17:52:36 +0100Katarushisu(~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net) (Client Quit)
2022-03-08 17:52:46 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2022-03-08 17:53:43 +0100Katarushisu(~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net)
2022-03-08 17:55:22 +0100raym(~raym@user/raym) (Ping timeout: 256 seconds)
2022-03-08 17:56:00 +0100waleee(~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 252 seconds)
2022-03-08 17:56:17 +0100raym(~raym@user/raym)
2022-03-08 17:56:37 +0100jinsun__(~jinsun@user/jinsun) (Ping timeout: 240 seconds)
2022-03-08 17:57:44 +0100tzh(~tzh@c-24-21-73-154.hsd1.or.comcast.net)
2022-03-08 18:01:41 +0100nisstyre(wes@user/nisstyre) (Quit: WeeChat 3.4)
2022-03-08 18:01:41 +0100DNH(~DNH@2a02:8108:1100:16d8:598a:8b0b:9405:6e26) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 18:02:01 +0100nisstyre(wes@user/nisstyre)
2022-03-08 18:05:15 +0100agumonkey(~user@2a01:e0a:8f9:d3e0:b117:81a8:33f6:93e7)
2022-03-08 18:05:54 +0100doyougnu(~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) (Ping timeout: 252 seconds)
2022-03-08 18:05:56 +0100lbseale(~ep1ctetus@user/ep1ctetus)
2022-03-08 18:06:08 +0100ishutin(~ishutin@87-97-82-131.pool.digikabel.hu) (Ping timeout: 256 seconds)
2022-03-08 18:06:28 +0100doyougnu(~doyougnu@cpe-67-249-83-190.twcny.res.rr.com)
2022-03-08 18:07:58 +0100ishutin(~ishutin@84-236-21-25.pool.digikabel.hu)
2022-03-08 18:08:55 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 18:09:06 +0100mmhat(~mmh@55d49be1.access.ecotel.net)
2022-03-08 18:12:18 +0100toulene_(~toulene@user/toulene)
2022-03-08 18:13:55 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2022-03-08 18:14:48 +0100toulene_(~toulene@user/toulene) (Remote host closed the connection)
2022-03-08 18:15:33 +0100jinsun(~jinsun@user/jinsun)
2022-03-08 18:16:45 +0100Arsen(arsen@managarm/dev/Arsen) (Quit: Quit.)
2022-03-08 18:17:24 +0100Arsen(arsen@managarm/dev/Arsen)
2022-03-08 18:19:04 +0100ccntrq(~Thunderbi@2a01:c22:9102:c100:80c3:8f62:e3ae:6455) (Remote host closed the connection)
2022-03-08 18:21:05 +0100coot(~coot@213.134.190.95)
2022-03-08 18:22:00 +0100bjobjo(~bjobjo@user/bjobjo) (Quit: leaving)
2022-03-08 18:27:04 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab)
2022-03-08 18:27:52 +0100szkl(uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2022-03-08 18:28:29 +0100gdown(~gavin@h69-11-149-231.kndrid.broadband.dynamic.tds.net)
2022-03-08 18:28:36 +0100bjobjo(~bjobjo@user/bjobjo)
2022-03-08 18:30:55 +0100 <maerwald> don't use cryptonite
2022-03-08 18:31:56 +0100 <briandaed> hard to avoid that, a lot of libraries use it already
2022-03-08 18:32:42 +0100 <maerwald> well, then use different libraries
2022-03-08 18:33:26 +0100 <maerwald> wrt the network issue, it seems no one opened a ticket on the warp issue tracker
2022-03-08 18:34:12 +0100 <maerwald> but yeah... just today we were talking about correctness and haskell, which is rather confusing given that so many libraries use sloppy and unverified cryptolibraries
2022-03-08 18:34:12 +0100 <briandaed> yeah, also checked that
2022-03-08 18:34:38 +0100 <maerwald> not even audited
2022-03-08 18:38:33 +0100 <janus> maerwald: why would someone open a ticket on the warp issue tracker? doesn't seem like it forbids 3.1.2.0? what is the issue with warp?
2022-03-08 18:39:01 +0100 <janus> kazu says that warp 3.3.5 has fixed the gracefulClose issue
2022-03-08 18:40:19 +0100econo(uid147250@user/econo)
2022-03-08 18:40:46 +0100 <maerwald> janus: because of https://github.com/haskell/network/issues/438#issuecomment-784771757
2022-03-08 18:41:08 +0100analognoise(~analognoi@185.229.59.233)
2022-03-08 18:44:58 +0100jespada(~jespada@148.252.132.235) (Read error: Connection reset by peer)
2022-03-08 18:48:54 +0100 <Hecate> briandaed: it is indeed hard to avoid. Fortunately there are alternatives that are emerging, if you have a direct need for cryptography primitives. You can always ask questions on #haskell-cryptography about this. :)
2022-03-08 18:51:28 +0100notzmv(~zmv@user/notzmv)
2022-03-08 18:52:17 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Remote host closed the connection)
2022-03-08 18:54:13 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 18:54:25 +0100DNH(~DNH@2a02:8108:1100:16d8:598a:8b0b:9405:6e26)
2022-03-08 18:54:51 +0100Vajb(~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813) (Read error: Connection reset by peer)
2022-03-08 18:55:06 +0100bontaq`(~user@165.1.205.23)
2022-03-08 18:56:01 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2022-03-08 18:56:35 +0100bontaq(~user@ool-45779fe5.dyn.optonline.net) (Ping timeout: 256 seconds)
2022-03-08 18:57:36 +0100unyu(~pyon@user/pyon) (Quit: brb)
2022-03-08 18:57:48 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 250 seconds)
2022-03-08 18:58:02 +0100waleee(~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340)
2022-03-08 18:58:56 +0100jpds(~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
2022-03-08 18:59:14 +0100 <briandaed> Hecate: thx, joined
2022-03-08 19:00:21 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 19:00:48 +0100bontaq``(~user@ool-45779fe5.dyn.optonline.net)
2022-03-08 19:01:37 +0100jpds(~jpds@gateway/tor-sasl/jpds)
2022-03-08 19:02:24 +0100toulene(~toulene@user/toulene)
2022-03-08 19:02:49 +0100bontaq`(~user@165.1.205.23) (Ping timeout: 256 seconds)
2022-03-08 19:05:38 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
2022-03-08 19:07:56 +0100xkuru(~xkuru@user/xkuru)
2022-03-08 19:09:00 +0100raym(~raym@user/raym) (Remote host closed the connection)
2022-03-08 19:09:17 +0100ishutin(~ishutin@84-236-21-25.pool.digikabel.hu) (Ping timeout: 272 seconds)
2022-03-08 19:10:17 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2022-03-08 19:10:27 +0100ishutin(~ishutin@87-97-88-220.pool.digikabel.hu)
2022-03-08 19:11:00 +0100Vajb(~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813)
2022-03-08 19:11:18 +0100unyu(~pyon@user/pyon)
2022-03-08 19:11:44 +0100lavaman(~lavaman@98.38.249.169)
2022-03-08 19:12:10 +0100raym(~raym@user/raym)
2022-03-08 19:12:46 +0100kongsheng(~kongsheng@71.28.228.142) (Quit: Client closed)
2022-03-08 19:13:12 +0100jgeerds(~jgeerds@55d4548e.access.ecotel.net)
2022-03-08 19:13:35 +0100kongsheng(~kongsheng@71.28.228.142)
2022-03-08 19:16:03 +0100alp(~alp@user/alp)
2022-03-08 19:17:55 +0100euandreh(~euandreh@2804:14c:33:9fe5:49fc:dd14:62fe:1d6f)
2022-03-08 19:19:06 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:3d9b:7fc7:6af0:b7ab) (Remote host closed the connection)
2022-03-08 19:19:46 +0100emf(~emf@2620:10d:c090:400::5:33d6)
2022-03-08 19:23:04 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Remote host closed the connection)
2022-03-08 19:25:22 +0100coot(~coot@213.134.190.95) (Quit: coot)
2022-03-08 19:30:20 +0100kuribas(~user@ptr-25vy0i8r77cynr1cb5v.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3))
2022-03-08 19:32:02 +0100bontaq```(~user@165.1.205.23)
2022-03-08 19:32:50 +0100bontaq``(~user@ool-45779fe5.dyn.optonline.net) (Ping timeout: 256 seconds)
2022-03-08 19:37:44 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:8852:a14c:a420:3fd8)
2022-03-08 19:37:48 +0100bontaq(~user@ool-45779fe5.dyn.optonline.net)
2022-03-08 19:39:41 +0100bontaq```(~user@165.1.205.23) (Ping timeout: 272 seconds)
2022-03-08 19:41:15 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 19:46:25 +0100lambdabot(~lambdabot@haskell/bot/lambdabot) (Remote host closed the connection)
2022-03-08 19:46:33 +0100lambdabot(~lambdabot@silicon.int-e.eu)
2022-03-08 19:46:33 +0100lambdabot(~lambdabot@silicon.int-e.eu) (Changing host)
2022-03-08 19:46:33 +0100lambdabot(~lambdabot@haskell/bot/lambdabot)
2022-03-08 19:46:38 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds)
2022-03-08 19:57:16 +0100ec(~ec@gateway/tor-sasl/ec) (Ping timeout: 240 seconds)
2022-03-08 19:57:43 +0100Erutuon(~Erutuon@user/erutuon)
2022-03-08 20:00:10 +0100loonycyborg(loonycybor@wesnoth/developer/loonycyborg) (Quit: ZNC - http://znc.sourceforge.net)
2022-03-08 20:00:26 +0100loonycyborg(loonycybor@wesnoth/developer/loonycyborg)
2022-03-08 20:00:43 +0100jakalx(~jakalx@base.jakalx.net) ()
2022-03-08 20:02:37 +0100Erutuon(~Erutuon@user/erutuon) (Ping timeout: 240 seconds)
2022-03-08 20:02:53 +0100dsrt^(~dsrt@50.232.121.75)
2022-03-08 20:03:26 +0100jakalx(~jakalx@base.jakalx.net)
2022-03-08 20:05:32 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
2022-03-08 20:05:57 +0100Erutuon(~Erutuon@user/erutuon)
2022-03-08 20:06:57 +0100alMalsamo(~alMalsamo@gateway/tor-sasl/almalsamo)
2022-03-08 20:09:19 +0100Vajb(~Vajb@2001:999:62:aa00:7f5a:4f10:c894:3813) (Read error: Connection reset by peer)
2022-03-08 20:09:34 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2022-03-08 20:09:39 +0100zincy_(~zincy@2a00:23c8:970c:4801:d43:5e37:69e3:551c)
2022-03-08 20:12:31 +0100dhouthoo(~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.4)
2022-03-08 20:17:45 +0100 <Unicorn_Princess> is there an easy way to get ghcup to upgrade all the things to the latest version? ghcup install ghc 9.2.2 for each is tedious
2022-03-08 20:18:02 +0100desantra(~skykanin@user/skykanin)
2022-03-08 20:18:14 +0100vicfred(~vicfred@user/vicfred)
2022-03-08 20:18:55 +0100 <geekosaur> I don't think it has an "all" option. I just use ghcup tui and hit "i" on the things I want to install
2022-03-08 20:20:02 +0100 <Unicorn_Princess> then i guess i will suffer
2022-03-08 20:20:13 +0100deadmarshal_(~deadmarsh@95.38.114.14) (Ping timeout: 272 seconds)
2022-03-08 20:20:25 +0100 <janus> Unicorn_Princess: what do you mean with "for each"? the ghc version is independent of the other versions
2022-03-08 20:20:43 +0100Tuplanolla(~Tuplanoll@91-159-69-98.elisa-laajakaista.fi)
2022-03-08 20:20:51 +0100 <geekosaur> I presume that means ghc, cabal, stack, etc.
2022-03-08 20:20:56 +0100 <Unicorn_Princess> i mean ghcup handles ghc, cabal, stack, the lsp..
2022-03-08 20:22:41 +0100coot(~coot@213.134.190.95)
2022-03-08 20:22:44 +0100vicfred(~vicfred@user/vicfred) (Ping timeout: 250 seconds)
2022-03-08 20:24:46 +0100ProfSimm(~ProfSimm@87.227.196.109)
2022-03-08 20:28:26 +0100Akiva(~Akiva@user/Akiva)
2022-03-08 20:29:39 +0100 <monochrom> "ghcup install" understands the "latest" tag.
2022-03-08 20:30:13 +0100 <monochrom> The default is "recommended" this is why the default is not "latest".
2022-03-08 20:30:21 +0100doyougnu(~doyougnu@cpe-67-249-83-190.twcny.res.rr.com) (Ping timeout: 272 seconds)
2022-03-08 20:30:52 +0100 <geekosaur> for thing in ghcup ghc stack cabal; do ghcup install $thing latest; done # hls is installed with ghc
2022-03-08 20:32:49 +0100 <geekosaur> oh I'm wrong, so add hls to the list
2022-03-08 20:32:52 +0100 <geekosaur> sorry
2022-03-08 20:33:06 +0100 <geekosaur> wsd thinking of the hls-powered epithet
2022-03-08 20:33:07 +0100 <monochrom> :)
2022-03-08 20:34:08 +0100sceptttre(~sceptttre@2603-6011-df05-84ab-dcd9-3721-0281-3545.res6.spectrum.com)
2022-03-08 20:34:43 +0100sceptttre(~sceptttre@2603-6011-df05-84ab-dcd9-3721-0281-3545.res6.spectrum.com) (Quit: Client closed)
2022-03-08 20:34:47 +0100 <geekosaur> qactually I wonder if ghcup install works for itselfor if you have to use upgrade
2022-03-08 20:34:52 +0100agumonke`(~user@88.163.231.79)
2022-03-08 20:35:07 +0100 <monochrom> Defaulting to "recommended" not "latest" works great for me and my students. It is the prudent thing to do and it is not tedious, my students and I do not suffer.
2022-03-08 20:35:22 +0100zincy_(~zincy@2a00:23c8:970c:4801:d43:5e37:69e3:551c) (Remote host closed the connection)
2022-03-08 20:35:39 +0100 <geekosaur> in particular there is no hls yet for ghc 9.2.2
2022-03-08 20:35:57 +0100zincy_(~zincy@host86-160-236-152.range86-160.btcentralplus.com)
2022-03-08 20:35:57 +0100Unicorn_Princess(~Unicorn_P@46-54-248-191.static.kate-wing.si) (Remote host closed the connection)
2022-03-08 20:36:12 +0100 <geekosaur> and unless you need some new feature, 8.10.7 works fine
2022-03-08 20:36:17 +0100agumonkey(~user@2a01:e0a:8f9:d3e0:b117:81a8:33f6:93e7) (Ping timeout: 240 seconds)
2022-03-08 20:37:10 +0100 <monochrom> "ghcup install ghcup" shows an error message that suggests that ghcup is confused. :)
2022-03-08 20:37:57 +0100 <monochrom> The error messages and warnings says something along the line of "to install ghc, say ghcup install ghc"
2022-03-08 20:38:27 +0100 <geekosaur> just saw that :)
2022-03-08 20:38:43 +0100 <monochrom> So yeah it has to be "ghcup upgrade".
2022-03-08 20:38:48 +0100Unicorn_Princess(~Unicorn_P@46-54-248-191.static.kate-wing.si)
2022-03-08 20:39:04 +0100 <geekosaur> ghcup upgrade; for thing in hls ghc stack cabal; do ghcup install $thing latest; done
2022-03-08 20:39:48 +0100 <monochrom> ghcup installs those who don't install themselves >:)
2022-03-08 20:40:12 +0100 <monochrom> (Sorry I have been hairsplitting set theory lately!)
2022-03-08 20:40:25 +0100 <geekosaur> hm, could use ghcup list to extract the list of things to install, but it includes ghcup…
2022-03-08 20:40:54 +0100 <Unicorn_Princess> ghcup tui is very pleasant, thanks geekosaur
2022-03-08 20:41:31 +0100 <monochrom> It may be more robust to extract from "ghcup install --help" instead, under the "available commands" heading.
2022-03-08 20:42:19 +0100 <monochrom> or "ghcup list --help" and look for the "[-t|--tool <ghc|cabal|hls|stack>]"
2022-03-08 20:42:21 +0100 <geekosaur> but harder to sewd/awk :þ
2022-03-08 20:42:31 +0100 <geekosaur> *sed
2022-03-08 20:42:46 +0100 <monochrom> sewk and awek :)
2022-03-08 20:44:17 +0100kilolympus(~kilolympu@31.205.200.235)
2022-03-08 20:45:28 +0100zincy_(~zincy@host86-160-236-152.range86-160.btcentralplus.com) (Remote host closed the connection)
2022-03-08 20:46:40 +0100briandaed(~root@109.95.142.93.r.toneticgroup.pl) (Quit: leaving)
2022-03-08 20:47:59 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2022-03-08 20:53:52 +0100unyu(~pyon@user/pyon) (Quit: brb)
2022-03-08 20:54:39 +0100worldhelloworld(~c1utt4r@164.68.96.37)
2022-03-08 20:55:29 +0100DNH(~DNH@2a02:8108:1100:16d8:598a:8b0b:9405:6e26) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 20:55:37 +0100Lord_of_Life_(~Lord@user/lord-of-life/x-2819915)
2022-03-08 20:56:57 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds)
2022-03-08 20:57:21 +0100 <maerwald> `ghcup install ghcup` will end up trying to install a GHC with the version 'ghcup'
2022-03-08 20:57:34 +0100 <monochrom> Oh heh
2022-03-08 20:57:40 +0100 <maerwald> becaus `ghcup install <ver>` is the legacy form of installing GHC
2022-03-08 20:57:45 +0100DNH(~DNH@2a02:8108:1100:16d8:1c1a:3fa2:4926:7c5a)
2022-03-08 20:57:55 +0100 <maerwald> which is kept for compatibility
2022-03-08 20:57:58 +0100 <geekosaur> figured it was something like that
2022-03-08 20:58:13 +0100 <monochrom> Yeah I forgot that the parser could be trying "since ghcup is not a 'command' it must be a 'version/tag'"
2022-03-08 20:58:23 +0100Lord_of_Life_Lord_of_Life
2022-03-08 20:58:50 +0100 <worldhelloworld> unrelated question - what free irc client is there that has a history of conversations even when you are disconnected? there is so much to learn from this group .... I tried irccloud, but that's paid ... any free versions?
2022-03-08 20:58:52 +0100 <monochrom> as opposed to "parse error: ghcup is not a valid command"
2022-03-08 20:59:37 +0100 <maerwald> much more confusing is this: `ghcup install lol-8.10.7`
2022-03-08 20:59:56 +0100 <monochrom> See the /topic line for a volunteer's log website.
2022-03-08 21:00:13 +0100 <Unicorn_Princess> worldhelloworld, what do you mean history when disconnected? like, that you can access your logs from when you were connected, even if you're not currently connected?
2022-03-08 21:00:15 +0100 <maerwald> it will parse 'lol' as an arch-triple, because we support compiling cross-ghc, but it's ignored for install commands
2022-03-08 21:00:37 +0100 <monochrom> If you really want to do your own recording, consider an "irc bouncer" so you have a background process that connects 24/7
2022-03-08 21:00:41 +0100 <Unicorn_Princess> or do you mean that will show you channel chat history even for times when you weren't connected?
2022-03-08 21:01:16 +0100 <monochrom> (and the background process also serves as a proxy for your IRC client"
2022-03-08 21:01:35 +0100 <worldhelloworld> Unicorn_Princess ... yes something like that - irccloud used to have a history of missed cconversations, current one i'm trying , hexchat, doesn't
2022-03-08 21:02:14 +0100 <Unicorn_Princess> is there any reason i shouldn't stick OverloadedRecordDot and DuplicateRecordFields in .cabal's default-extensions and pretend haskell is sane?
2022-03-08 21:02:27 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 252 seconds)
2022-03-08 21:02:43 +0100 <sclv> for a given project? no. have fun with them!
2022-03-08 21:02:47 +0100 <monochrom> OverloadedRecordDot is not sane.
2022-03-08 21:03:02 +0100bahamas(~lucian@84.232.140.52) (Ping timeout: 240 seconds)
2022-03-08 21:03:07 +0100 <sclv> i mean i don't like it either, but if you do, just use it freely and see how it goes
2022-03-08 21:03:21 +0100 <Unicorn_Princess> worldhelloworld, alas, as monochrom said, you will need something to connect to the channel in your stead and maintain a history. irc does not support offline history syncing
2022-03-08 21:03:53 +0100 <monochrom> IRC servers don't record for you because they don't serve ads.
2022-03-08 21:03:54 +0100 <Unicorn_Princess> that something is called an "irc bouncer" in the lingo
2022-03-08 21:04:12 +0100 <sclv> the ircbrowse link in the channel description still maintains up to date logs
2022-03-08 21:04:15 +0100 <monochrom> (or sell your credit card number to strangers)
2022-03-08 21:04:15 +0100 <Unicorn_Princess> (and that's where my knowledge ends)
2022-03-08 21:04:18 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2022-03-08 21:04:22 +0100 <sclv> so you can just browse those too
2022-03-08 21:04:23 +0100 <worldhelloworld> Hmmm yes, the logs are one way, unfortunately not very interactive
2022-03-08 21:04:29 +0100 <Unicorn_Princess> monochrom, what's not sane about overloadedrecorddot?
2022-03-08 21:05:00 +0100 <monochrom> Cargo culting C, C++, and Java syntax is not sane.
2022-03-08 21:05:25 +0100 <monochrom> I guess it was Algol syntax.
2022-03-08 21:05:56 +0100 <Unicorn_Princess> i'll leave you to your personId, cowId, catId, dogId, etcId then :P
2022-03-08 21:06:23 +0100 <sclv> ugh... that's terrible. Now, on the other hand, id_person, id_cow, id_cat, now that's great!
2022-03-08 21:06:24 +0100 <monochrom> No I'm OK with for example SML's choice which is # IIRC.
2022-03-08 21:06:24 +0100 <worldhelloworld> Pardon my ignorance, but what does the term "cargo culting" mean? Or is it some dismissive reference to a rusty language monochrom ?
2022-03-08 21:06:55 +0100 <monochrom> Blindly mimicking things.
2022-03-08 21:07:13 +0100 <geekosaur> see the pacific island cargo cults post-ww2
2022-03-08 21:07:26 +0100 <worldhelloworld> ok, thanks - googling now
2022-03-08 21:07:40 +0100ec(~ec@gateway/tor-sasl/ec)
2022-03-08 21:07:40 +0100 <geekosaur> there are IRC clients like quassel which involve a bouncer component which stays connected, but that assumes you have some way for them to stay connected
2022-03-08 21:07:40 +0100 <monochrom> For example "I saw other people doing pair programming, I must do the same! I don't ask why. I don't ask suitability to my context."
2022-03-08 21:07:53 +0100 <geekosaur> otherwise, yes, you'd have to pay to have someone stay connected for you
2022-03-08 21:08:25 +0100 <geekosaur> there's also matrix but I don't know if that's free either
2022-03-08 21:08:55 +0100 <worldhelloworld> geekosaur , so if I have a cloud machine - is it easy to stay connected and then read it on another machine? I'd imagine it sounds a bit complicated to configure
2022-03-08 21:09:13 +0100 <geekosaur> quassel would configure it for you
2022-03-08 21:09:26 +0100 <geekosaur> otherwise you'd have to set up something like znc manually
2022-03-08 21:09:28 +0100 <worldhelloworld> thats true monochrom - follow the herd :)
2022-03-08 21:09:37 +0100ishutin(~ishutin@87-97-88-220.pool.digikabel.hu) (Ping timeout: 272 seconds)
2022-03-08 21:10:02 +0100 <worldhelloworld> ok will read if quassel fits my needs, configuring manually is a pain
2022-03-08 21:10:02 +0100 <sclv> i believe i first became familiar with cargo cults from the classic Niven sci fi novel Dream Park
2022-03-08 21:10:15 +0100 <monochrom> Unicorn_Princess, there are several sane choices. Use . for function composition, choose some other symbol for record selection. Or, use . for record selection, choose some other symbol for function composition. Using the same symbol for both is the insane one.
2022-03-08 21:10:40 +0100 <geekosaur> dot does too many things already and it shows
2022-03-08 21:10:46 +0100 <monochrom> FWIW SML chooses o for function composition, # for record selection.
2022-03-08 21:10:51 +0100 <geekosaur> > [False..True] -- nope
2022-03-08 21:10:52 +0100ishutin(~ishutin@84-236-40-230.pool.digikabel.hu)
2022-03-08 21:10:52 +0100 <lambdabot> error:
2022-03-08 21:10:52 +0100 <lambdabot> Not in scope: ‘False..’
2022-03-08 21:10:52 +0100 <lambdabot> No module named ‘False’ is imported.error:
2022-03-08 21:11:14 +0100 <Hecate> pity not everyone has easy access to ∘ on their keyboard
2022-03-08 21:11:47 +0100 <monochrom> And SML was defined long before unicode existed.
2022-03-08 21:12:15 +0100coot(~coot@213.134.190.95) (Quit: coot)
2022-03-08 21:12:24 +0100 <ski> SML's `#foo' also nicely differentiates between the field name, and the field accessor function
2022-03-08 21:12:27 +0100 <Hecate> that being said I'd have also (|>) and (<|)
2022-03-08 21:12:34 +0100worldhelloworld2(~quassel@vmi275462.contaboserver.net)
2022-03-08 21:12:38 +0100 <monochrom> But we can still debate which one is more nighmarish, "g o h" or "g `o` h" :)
2022-03-08 21:12:40 +0100 <Hecate> ski: don't we have that with overloaded labels nowadays?
2022-03-08 21:12:52 +0100 <Hecate> monochrom: the second one has a funny face though
2022-03-08 21:13:10 +0100 <Hecate> ( `o`) .oO(hello)
2022-03-08 21:15:50 +0100simendsjo(~user@84.211.91.241)
2022-03-08 21:17:27 +0100 <monochrom> SML has the nice uniformity that tuples are records too, (x,y,z) is the record {1=x, 2=y, 3=z} using 1, 2, 3 as field names.
2022-03-08 21:17:51 +0100 <ski> Hecate : well, you'd need `NoFieldSelectors', too
2022-03-08 21:17:51 +0100 <monochrom> So #2 works for all of: (x,y), (x,y,z), (x,y,z,t), ...
2022-03-08 21:19:00 +0100agumonke`(~user@88.163.231.79) (Remote host closed the connection)
2022-03-08 21:19:37 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net)
2022-03-08 21:22:46 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:8852:a14c:a420:3fd8) (Remote host closed the connection)
2022-03-08 21:22:59 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:8852:a14c:a420:3fd8)
2022-03-08 21:24:11 +0100yauhsien_(~yauhsien@61-231-43-120.dynamic-ip.hinet.net) (Ping timeout: 272 seconds)
2022-03-08 21:24:30 +0100unyu(~pyon@user/pyon)
2022-03-08 21:25:04 +0100desantra(~skykanin@user/skykanin) (Quit: WeeChat 3.3)
2022-03-08 21:27:52 +0100zincy_(~zincy@host86-160-236-152.range86-160.btcentralplus.com)
2022-03-08 21:28:46 +0100 <Hecate> ski: I think NoFieldSelectors is good
2022-03-08 21:30:29 +0100zincy_(~zincy@host86-160-236-152.range86-160.btcentralplus.com) (Remote host closed the connection)
2022-03-08 21:33:01 +0100zincy_(~zincy@2a00:23c8:970c:4801:d43:5e37:69e3:551c)
2022-03-08 21:35:32 +0100zer0bitz(~zer0bitz@2001:2003:f74d:b800:1d57:8085:a2ac:6196)
2022-03-08 21:37:39 +0100deadmarshal_(~deadmarsh@95.38.114.14)
2022-03-08 21:39:04 +0100agumonkey(~user@2a01:e0a:8f9:d3e0:b117:81a8:33f6:93e7)
2022-03-08 21:39:06 +0100zer0bitz_(~zer0bitz@2001:2003:f74d:b800:7859:22cf:713c:fe6e) (Ping timeout: 260 seconds)
2022-03-08 21:39:50 +0100_ht(~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection)
2022-03-08 21:40:22 +0100JimL(~quassel@89-162-2-132.fiber.signal.no)
2022-03-08 21:41:17 +0100zincy_(~zincy@2a00:23c8:970c:4801:d43:5e37:69e3:551c) (Remote host closed the connection)
2022-03-08 21:41:31 +0100zincy_(~zincy@2a00:23c8:970c:4801:d43:5e37:69e3:551c)
2022-03-08 21:42:33 +0100deadmarshal_(~deadmarsh@95.38.114.14) (Ping timeout: 272 seconds)
2022-03-08 21:45:25 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 21:46:14 +0100lavaman(~lavaman@98.38.249.169) (Remote host closed the connection)
2022-03-08 21:46:21 +0100dcoutts__(~duncan@host86-144-78-249.range86-144.btcentralplus.com) (Ping timeout: 272 seconds)
2022-03-08 21:47:18 +0100neurocyte0917090(~neurocyte@IP-045014190241.dynamic.medianet-world.de)
2022-03-08 21:47:18 +0100neurocyte0917090(~neurocyte@IP-045014190241.dynamic.medianet-world.de) (Changing host)
2022-03-08 21:47:18 +0100neurocyte0917090(~neurocyte@user/neurocyte)
2022-03-08 21:47:48 +0100Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 240 seconds)
2022-03-08 21:48:51 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291)
2022-03-08 21:49:36 +0100mastarija(~mastarija@2a05:4f46:e04:6000:509f:97b6:34da:4a)
2022-03-08 21:49:51 +0100JimL(~quassel@89-162-2-132.fiber.signal.no) (Remote host closed the connection)
2022-03-08 21:50:07 +0100 <mastarija> I'm wondering, is there an alternative to the `network` package?
2022-03-08 21:50:42 +0100 <Hecate> not sure
2022-03-08 21:50:49 +0100 <geekosaur> I think there might be higher level interfaces, but network is the loest level interface and would still be there underneath
2022-03-08 21:50:53 +0100 <geekosaur> *lowest
2022-03-08 21:51:06 +0100 <Hecate> hmm
2022-03-08 21:51:08 +0100 <Hecate> https://hackage.haskell.org/package/network-bsd ?
2022-03-08 21:51:09 +0100 <Hecate> maybe?
2022-03-08 21:51:20 +0100 <[exa]> it would be pretty hard to write a really different alternative to the sockets API
2022-03-08 21:51:24 +0100 <mastarija> I was just wondering if someone tried to do something else with low level networking
2022-03-08 21:51:55 +0100 <[exa]> the BSD subpackage is about netdb name resolution
2022-03-08 21:52:02 +0100acidjnk(~acidjnk@p200300d0c7049f27690562e0ba62f824.dip0.t-ipconnect.de)
2022-03-08 21:52:15 +0100 <geekosaur> yeh
2022-03-08 21:52:42 +0100 <geekosaur> network-bsd is name resolution, network is sockets, the docs for network point to some higher level interfaces
2022-03-08 21:52:46 +0100 <[exa]> mastarija: not really, berkeley sockets are kinda everywhere
2022-03-08 21:53:01 +0100 <geekosaur> "Other packages provide higher level interfaces:
2022-03-08 21:53:01 +0100 <geekosaur> connection
2022-03-08 21:53:01 +0100 <geekosaur> hookup
2022-03-08 21:53:01 +0100 <geekosaur> network-simple"
2022-03-08 21:53:08 +0100 <[exa]> mastarija: as geekosaur said, there's plenty of middleware that adds abstractions/goodies (0mq etc)
2022-03-08 21:53:27 +0100 <mastarija> yes I saw that
2022-03-08 21:53:34 +0100lavaman(~lavaman@98.38.249.169)
2022-03-08 21:53:59 +0100 <[exa]> is there even an OS that uses a non-socketish API for networking?
2022-03-08 21:54:06 +0100 <mastarija> but since there are usually 50 different takes on something in haskell I was surprised there's nothing for networking :D
2022-03-08 21:54:33 +0100 <geekosaur> there used to be some that used alternatives, but de facto sockets have won
2022-03-08 21:54:56 +0100 <mastarija> [exa], I'm not really looking for nonsocket networking, but maybe a different "wrapper" around the C library
2022-03-08 21:55:23 +0100 <geekosaur> the problem here is that network itself shows how difficult writing such wrappers is
2022-03-08 21:55:29 +0100 <[exa]> mastarija: for any specific purpose?
2022-03-08 21:55:34 +0100 <geekosaur> it'skinda notoriously difficult to keep wprking
2022-03-08 21:55:36 +0100 <mastarija> I was just interested if there's something out there
2022-03-08 21:55:46 +0100 <mastarija> Like looking at weird animals in the zoo
2022-03-08 21:55:50 +0100 <mastarija> nothing in particular :D
2022-03-08 21:56:26 +0100 <geekosaur> especially on windows
2022-03-08 21:56:29 +0100 <mastarija> geekosaur, yes I have problems on windows on occasions
2022-03-08 21:56:30 +0100 <[exa]> mastarija: I tend to take all sockets and wrap them with the haskell handles and then pretend the world is a happy place with only handles and IO
2022-03-08 21:56:44 +0100 <mastarija> xD
2022-03-08 21:57:13 +0100 <[exa]> ah, windows
2022-03-08 21:57:20 +0100 <monochrom> There are usually 50 different takes on something high-level.
2022-03-08 21:59:55 +0100Maxdamantus(~Maxdamant@user/maxdamantus)
2022-03-08 22:00:50 +0100TQuid(~TQuid@2604:3d08:6e7e:9700:9106:2a95:ca3a:5770)
2022-03-08 22:02:07 +0100alMalsamolumberjack123
2022-03-08 22:02:15 +0100TQuidregister
2022-03-08 22:02:20 +0100registerTQuid
2022-03-08 22:02:44 +0100 <janus> mastarija: i have made uring/iocp api compatible bindings for chez (used via idris), something similar should be possible with haskell (except i don't know how the haskell rts works).
2022-03-08 22:03:31 +0100 <janus> mastarija: https://git.sr.ht/~janus/
2022-03-08 22:03:48 +0100 <geekosaur> I think there might be some work on uring support in the rts
2022-03-08 22:04:05 +0100 <geekosaur> not inany released version, and still early
2022-03-08 22:04:16 +0100ec(~ec@gateway/tor-sasl/ec) (Ping timeout: 240 seconds)
2022-03-08 22:05:37 +0100zer0bitz(~zer0bitz@2001:2003:f74d:b800:1d57:8085:a2ac:6196) (Ping timeout: 250 seconds)
2022-03-08 22:06:57 +0100ec(~ec@gateway/tor-sasl/ec)
2022-03-08 22:07:59 +0100 <mastarija> janus, never heard of uring
2022-03-08 22:08:20 +0100 <mastarija> gonna check that out, thanks :)
2022-03-08 22:08:24 +0100 <janus> mastarija: there are some good articles on lwn
2022-03-08 22:10:03 +0100simendsjo(~user@84.211.91.241) (Ping timeout: 256 seconds)
2022-03-08 22:12:40 +0100gehmehgeh(~user@user/gehmehgeh)
2022-03-08 22:12:47 +0100 <mastarija> janus, thx, found one : https://lwn.net/Articles/810414/
2022-03-08 22:13:42 +0100zincy_(~zincy@2a00:23c8:970c:4801:d43:5e37:69e3:551c) (Remote host closed the connection)
2022-03-08 22:14:27 +0100lavaman(~lavaman@98.38.249.169) (Remote host closed the connection)
2022-03-08 22:15:24 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 240 seconds)
2022-03-08 22:17:17 +0100pavonia(~user@user/siracusa)
2022-03-08 22:18:28 +0100shailangsa(~shailangs@host86-186-133-59.range86-186.btcentralplus.com)
2022-03-08 22:19:08 +0100JimL(~quassel@89-162-2-132.fiber.signal.no)
2022-03-08 22:19:24 +0100coot(~coot@213.134.190.95)
2022-03-08 22:20:50 +0100dcoutts__(~duncan@host86-144-78-249.range86-144.btcentralplus.com)
2022-03-08 22:24:41 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:8852:a14c:a420:3fd8) (Remote host closed the connection)
2022-03-08 22:25:29 +0100cosimone(~user@93-47-229-38.ip115.fastwebnet.it) (Quit: ERC (IRC client for Emacs 27.1))
2022-03-08 22:26:23 +0100 <TQuid> Anyone here had success setting up a Haskell environment on an M1 mac?
2022-03-08 22:27:35 +0100 <geekosaur> ghc 8.10.7 should work fine
2022-03-08 22:27:43 +0100 <geekosaur> 9.2.2 apparently has a signing problem
2022-03-08 22:28:03 +0100 <geekosaur> but mostly people still use 8.10.7 so I wouldn't be in much hurry to upgrade anyway
2022-03-08 22:28:19 +0100 <TQuid> Yeah, when I try to install that from the bindist, "make install" results in every single library giving a security exception ("cannot scan for malicious software"). I don't relish re-running make for every one of those
2022-03-08 22:28:51 +0100 <TQuid> I have not found any way to tell the idiot OS to give a pass to a whole directory
2022-03-08 22:29:01 +0100kongsheng(~kongsheng@71.28.228.142) (Quit: Client closed)
2022-03-08 22:29:25 +0100AlexZenon(~alzenon@178.34.160.24) (Read error: Connection reset by peer)
2022-03-08 22:29:26 +0100Alex_test(~al_test@178.34.160.24) (Read error: Connection reset by peer)
2022-03-08 22:29:26 +0100AlexNoo(~AlexNoo@178.34.160.24) (Read error: Connection reset by peer)
2022-03-08 22:30:40 +0100ubert(~Thunderbi@p548c8d84.dip0.t-ipconnect.de) (Quit: ubert)
2022-03-08 22:30:43 +0100 <mastarija> geekosaur, I just tried setting up 9.2.2 on windows and it's broken it seems
2022-03-08 22:30:59 +0100 <maerwald> mastarija: yes
2022-03-08 22:31:03 +0100 <maerwald> see https://gitlab.haskell.org/ghc/ghc/-/issues/21196
2022-03-08 22:31:22 +0100 <mastarija> :D
2022-03-08 22:31:52 +0100romesrf(~romes@44.190.189.46.rev.vodafone.pt) (Ping timeout: 250 seconds)
2022-03-08 22:32:58 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:8852:a14c:a420:3fd8)
2022-03-08 22:33:00 +0100romesrf(~romes@44.190.189.46.rev.vodafone.pt)
2022-03-08 22:33:32 +0100 <maerwald> you can try putting yur msys2 into PATH
2022-03-08 22:33:54 +0100 <maerwald> but that can cause all sorts of other problems
2022-03-08 22:34:22 +0100 <maerwald> since windows uses PATH to look for dynamic libraries too
2022-03-08 22:34:58 +0100AlexNoo(~AlexNoo@178.34.160.24)
2022-03-08 22:35:33 +0100Alex_test(~al_test@178.34.160.24)
2022-03-08 22:36:05 +0100AlexZenon(~alzenon@178.34.160.24)
2022-03-08 22:37:52 +0100 <mastarija> maerwald, I have msys2 in my path (parts of it) it works nicely and I quite like the experience. When I need a package, just pacman -S and it's on!
2022-03-08 22:39:09 +0100ubert(~Thunderbi@p200300ecdf3be9b38bc0692fc3914e47.dip0.t-ipconnect.de)
2022-03-08 22:39:16 +0100dsrt^(~dsrt@50.232.121.75) (Remote host closed the connection)
2022-03-08 22:39:47 +0100mastarija(~mastarija@2a05:4f46:e04:6000:509f:97b6:34da:4a) (Quit: Leaving)
2022-03-08 22:41:56 +0100wyrd(~wyrd@gateway/tor-sasl/wyrd) (Ping timeout: 240 seconds)
2022-03-08 22:42:20 +0100 <janus> maybe the msys2 equivalent of /usr/lib needs to be on the path for libgcc_s.dll to be found (i am guessing the file name)
2022-03-08 22:42:39 +0100TQuid(~TQuid@2604:3d08:6e7e:9700:9106:2a95:ca3a:5770) (Remote host closed the connection)
2022-03-08 22:42:52 +0100Topsi(~Tobias@dyndsl-095-033-088-239.ewe-ip-backbone.de) (Read error: Connection reset by peer)
2022-03-08 22:43:00 +0100 <maerwald> it's absolutely not recommended
2022-03-08 22:43:08 +0100 <maerwald> weird things will happen
2022-03-08 22:43:35 +0100shapr(~user@pool-173-73-44-186.washdc.fios.verizon.net) (Remote host closed the connection)
2022-03-08 22:47:46 +0100coot(~coot@213.134.190.95) (Quit: coot)
2022-03-08 22:48:51 +0100wyrd(~wyrd@gateway/tor-sasl/wyrd)
2022-03-08 22:50:50 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl)
2022-03-08 22:51:57 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2022-03-08 22:53:07 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2022-03-08 22:53:45 +0100 <monochrom> Yikes, I was hoping that 9.2.2 would solve all platform-related problems. Apparently, it has caused more.
2022-03-08 22:54:04 +0100 <monochrom> OK, "caused" is unfair. suffered.
2022-03-08 22:54:25 +0100 <maerwald> msys2 maintainers also managed to break GHC: https://github.com/msys2/MINGW-packages/issues/10837
2022-03-08 22:54:30 +0100 <maerwald> so you get hit from all angles
2022-03-08 22:54:31 +0100 <geekosaur> 9.2.2 hasso far been abit of a cursedrelease. starting with "is not released"
2022-03-08 22:54:51 +0100 <monochrom> (Someone on the mailing list reported a signature-checking error on intel mac.)
2022-03-08 22:54:59 +0100 <geekosaur> yep
2022-03-08 22:55:42 +0100merijn(~merijn@c-001-001-005.client.esciencecenter.eduvpn.nl) (Ping timeout: 256 seconds)
2022-03-08 22:56:03 +0100 <monochrom> Though, the silver lining is that all the issues seem to be just packaging rather than fundamental eg code generator broken. :)
2022-03-08 22:56:11 +0100 <monochrom> So, much easily fixable.
2022-03-08 22:56:36 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
2022-03-08 22:56:53 +0100 <monochrom> OK, I guess from the POV of the GHC devs, it is packaging that's the hard part. :)
2022-03-08 22:56:57 +0100 <geekosaur> yeh, but imagine being poor bgamari right now
2022-03-08 22:57:34 +0100 <monochrom> They're probably like "code optimization based on abstract interpretation is trivial" :)
2022-03-08 22:59:31 +0100Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 245 seconds)
2022-03-08 23:01:08 +0100 <sm> releasing is hard
2022-03-08 23:01:18 +0100 <sm> sorry to hear 9.2.2 is continuing the tradition .. :/
2022-03-08 23:03:58 +0100biberu(~biberu@user/biberu) (Read error: Connection reset by peer)
2022-03-08 23:05:02 +0100 <romesrf> hahaah
2022-03-08 23:05:27 +0100 <romesrf> it is indeed unfortunate that so much work is required for that all to work
2022-03-08 23:06:10 +0100Maxdamantus(~Maxdamant@user/maxdamantus)
2022-03-08 23:06:43 +0100 <maerwald> well, first of all: supporting windows is hard anyway
2022-03-08 23:07:11 +0100 <romesrf> :') *windows* is hard
2022-03-08 23:07:17 +0100 <maerwald> then supporting mac is hard
2022-03-08 23:07:24 +0100 <maerwald> M1 even harder
2022-03-08 23:07:32 +0100 <maerwald> then FreeBSD is a nightmare at times
2022-03-08 23:07:51 +0100 <maerwald> alpine linux also causes issues
2022-03-08 23:07:54 +0100 <maerwald> and the list goes on
2022-03-08 23:08:02 +0100 <romesrf> it does seem like a chore
2022-03-08 23:08:05 +0100 <sm> bgamari needs help
2022-03-08 23:08:13 +0100 <romesrf> sm: how can we help?
2022-03-08 23:08:31 +0100 <maerwald> clone em
2022-03-08 23:08:41 +0100 <sm> get hired as a full time engineer with the GHC team
2022-03-08 23:08:46 +0100 <romesrf> sm: dream job?
2022-03-08 23:08:56 +0100takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2022-03-08 23:09:01 +0100 <sm> hehe maybe ask bgamari
2022-03-08 23:09:12 +0100 <sm> yes and no :)
2022-03-08 23:09:17 +0100 <sm> I imagine
2022-03-08 23:09:28 +0100Maxdaman1us(~Maxdamant@user/maxdamantus)
2022-03-08 23:09:30 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:8852:a14c:a420:3fd8) (Remote host closed the connection)
2022-03-08 23:09:34 +0100 <romesrf> "OK everyone 9.2.2 is out everyone get back on code optimization"
2022-03-08 23:09:44 +0100 <romesrf> *everyone is happy for a month*
2022-03-08 23:09:51 +0100 <romesrf> OK everyone 9.2.3 let's go
2022-03-08 23:09:57 +0100 <romesrf> 3 months of hell?
2022-03-08 23:09:59 +0100 <romesrf> :)
2022-03-08 23:10:12 +0100 <Unicorn_Princess> hm. project-name.cabal other-modules and default-extensions lists are newline-separated, but build-depends needs commas between items. what gives?
2022-03-08 23:10:56 +0100 <romesrf> sm: unfortunately full time isn't on the table for me, the thesis comes first
2022-03-08 23:10:58 +0100 <maerwald> Unicorn_Princess: because you already have optional whitespace between dependency name and version range
2022-03-08 23:11:08 +0100 <sm> picture how Debian supports multiple architectures. It's an army of maintainers all working together. (Actually it's probably a much smaller number of hard-working folks. But in principle, it's definitely not expected to all be handled by 1-2 people)
2022-03-08 23:11:13 +0100 <romesrf> but "where" is bgamari working?
2022-03-08 23:11:31 +0100 <Unicorn_Princess> maerwald, aaah, ugly, but makes sense, thanks
2022-03-08 23:11:47 +0100 <monochrom> If the job is just to pick one single platform and support it, it could be a dream job. If the job is to support multiple platforms, that's a nightmare job.
2022-03-08 23:11:51 +0100 <janus> Unicorn_Princess: you can avoid the commas by having multiple build-depends
2022-03-08 23:11:54 +0100 <maerwald> sm: a distro like debian probably has 50 active volunteers and easily up to 200 devs in total
2022-03-08 23:12:00 +0100 <sm> I think he and maybe others like mpickering are employees of Well-Typed and part/full time funded to work on GHC
2022-03-08 23:12:04 +0100 <romesrf> monochrom: I can see that :)
2022-03-08 23:12:05 +0100 <monochrom> Ugh wait a second! nightmare is a special case of dream... >:)
2022-03-08 23:12:12 +0100 <Unicorn_Princess> lol
2022-03-08 23:12:22 +0100 <romesrf> monochrom: LOL
2022-03-08 23:12:26 +0100Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 260 seconds)
2022-03-08 23:12:34 +0100 <romesrf> instance Dreamable Nightmare
2022-03-08 23:13:56 +0100biberu(~biberu@user/biberu)
2022-03-08 23:14:18 +0100 <romesrf> perhaps you know impurepics.com, they have some really funny images
2022-03-08 23:14:23 +0100 <romesrf> this one always comes to mind: https://impurepics.com/posts/2018-07-29-names-dont-matter.html
2022-03-08 23:14:25 +0100Maxdamantus(~Maxdamant@user/maxdamantus)
2022-03-08 23:14:42 +0100 <monochrom> Haha rosable.
2022-03-08 23:16:10 +0100kimjetwav(~user@2607:fea8:2363:8f00:9e8a:8fa1:6b4e:dd92)
2022-03-08 23:17:34 +0100Maxdaman1us(~Maxdamant@user/maxdamantus) (Ping timeout: 260 seconds)
2022-03-08 23:17:58 +0100kimjetwav(~user@2607:fea8:2363:8f00:9e8a:8fa1:6b4e:dd92) (Client Quit)
2022-03-08 23:19:17 +0100lavaman(~lavaman@98.38.249.169)
2022-03-08 23:21:59 +0100Guest14(~Guest14@185.249.168.124)
2022-03-08 23:22:31 +0100Guest14(~Guest14@185.249.168.124) (Client Quit)
2022-03-08 23:22:34 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:8852:a14c:a420:3fd8)
2022-03-08 23:26:49 +0100jz99(~jz99@pa49-186-65-17.pa.vic.optusnet.com.au)
2022-03-08 23:27:08 +0100jz99(~jz99@pa49-186-65-17.pa.vic.optusnet.com.au) (Remote host closed the connection)
2022-03-08 23:27:09 +0100euouae(~euouae@user/euouae)
2022-03-08 23:27:25 +0100 <euouae> Hello does anyone else have two entries of ~/.cabal/bin and ~/.gchup/bin in their $PATH?
2022-03-08 23:27:36 +0100jz99(~jz99@pa49-186-65-17.pa.vic.optusnet.com.au)
2022-03-08 23:28:07 +0100jz99(~jz99@pa49-186-65-17.pa.vic.optusnet.com.au) (Remote host closed the connection)
2022-03-08 23:28:09 +0100 <monochrom> I think most people do.
2022-03-08 23:28:22 +0100 <euouae> why is that monochrom, shouldn't there be a single entry instead?
2022-03-08 23:28:25 +0100 <geekosaur> I think they might mean two of each?
2022-03-08 23:28:29 +0100 <euouae> ah yeah, two of each
2022-03-08 23:28:38 +0100kaph(~kaph@151.35.10.65)
2022-03-08 23:28:48 +0100 <geekosaur> ideally there'd be only one. you might have to check your shell dotfiles for duplication
2022-03-08 23:29:04 +0100 <euouae> I can't even figure out where it is that it gets added
2022-03-08 23:29:09 +0100 <monochrom> I don't, but that's because I set up my ~/.cabal/config to have a non-default setting about installdir so I have ~/bin instead of ~/.cabal/bin
2022-03-08 23:29:18 +0100 <euouae> I don't see it under my .bashrc or .profile nor my corresponding /etc files
2022-03-08 23:30:11 +0100 <geekosaur> look for a line which sources ~/.ghcup/env
2022-03-08 23:30:22 +0100 <geekosaur> or possibly two such lines
2022-03-08 23:30:42 +0100 <euouae> aha, thanks. I will investigate. that does bring up results
2022-03-08 23:30:53 +0100shapr(~user@pool-173-73-44-186.washdc.fios.verizon.net)
2022-03-08 23:31:31 +0100 <euouae> in ~/.bashrc there's [ -f "/home/fox/.ghcup/env" ] && source "/home/fox/.ghcup/env"
2022-03-08 23:31:39 +0100fendor_(~fendor@178.165.181.170.wireless.dyn.drei.com) (Remote host closed the connection)
2022-03-08 23:31:44 +0100 <euouae> that one should be fine, as -f only tests for existence I believe, so ... hmm...
2022-03-08 23:31:48 +0100 <geekosaur> yes
2022-03-08 23:32:12 +0100 <monochrom> What if something runs .bashrc twice?
2022-03-08 23:33:09 +0100 <euouae> That's probably it
2022-03-08 23:33:16 +0100 <geekosaur> .bashrc is run with every shell, .profile only by a login shell. if you start a second shell under the first it'll add them to $PATH again
2022-03-08 23:33:47 +0100 <euouae> but who added that line to my .bashrc? Was it me?
2022-03-08 23:34:23 +0100 <euouae> It's not automatically done by ghcup, right? I must've mistakenly modified my .bashrc instead of .profile
2022-03-08 23:34:45 +0100 <monochrom> The "curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh" thing does. Although, it did ask you.
2022-03-08 23:35:02 +0100 <maerwald> euouae: that has been fixed
2022-03-08 23:35:03 +0100 <geekosaur> shouldn't it have added it to .profile though?
2022-03-08 23:35:10 +0100 <geekosaur> oh
2022-03-08 23:35:21 +0100 <maerwald> https://gitlab.haskell.org/haskell/ghcup-hs/-/merge_requests/229
2022-03-08 23:35:24 +0100 <euouae> aha, okay. thanks again for all the clarifications and the unix lesson :D
2022-03-08 23:35:50 +0100 <maerwald> 2 months ago, so if you re-run the ghcup installer, it will fix ~/.ghcup/env
2022-03-08 23:35:54 +0100kaph(~kaph@151.35.10.65) (Remote host closed the connection)
2022-03-08 23:36:16 +0100jpds(~jpds@gateway/tor-sasl/jpds) (Ping timeout: 240 seconds)
2022-03-08 23:36:22 +0100kaph(~kaph@151.35.10.65)
2022-03-08 23:37:04 +0100gehmehgeh(~user@user/gehmehgeh) (Remote host closed the connection)
2022-03-08 23:37:37 +0100 <monochrom> neat trick :)
2022-03-08 23:37:38 +0100mcgroin(~mcgroin@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 256 seconds)
2022-03-08 23:37:48 +0100 <euouae> maerwald https://www.haskell.org/ghcup/install/#manual-install the website could also be fixed
2022-03-08 23:38:06 +0100 <euouae> Because it seems that it's still suggesting the old thing?
2022-03-08 23:38:22 +0100jpds(~jpds@gateway/tor-sasl/jpds)
2022-03-08 23:38:53 +0100 <euouae> won't re-running ghcup also re-download everything?
2022-03-08 23:39:03 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2022-03-08 23:39:03 +0100 <maerwald> not much
2022-03-08 23:39:37 +0100 <maerwald> You can also: curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | BOOTSTRAP_HASKELL_MINIMAL=1 sh
2022-03-08 23:40:46 +0100 <euouae> I'm going to write my own hack that detects .cabal/bin presence in $PATH for now
2022-03-08 23:41:17 +0100 <maerwald> euouae: the link I gave you shows how to do it
2022-03-08 23:41:36 +0100haskellnoob(~haskellno@181.122.131.227)
2022-03-08 23:42:57 +0100 <haskellnoob> hello all, it's me again with another noob question where I am stuck
2022-03-08 23:43:01 +0100 <haskellnoob> https://pastebin.com/RSTJEZnb
2022-03-08 23:43:47 +0100 <haskellnoob> basically I have a newtype wrapped around a bytestring that gets hex-encoded, but I cannot implement the FromJSON instance, I'm just not smart enough to figure it out
2022-03-08 23:44:15 +0100 <euouae> maerwald in that commit, right? yup, but I'm going with the simpler $PATH =~ "cabal/.bin"
2022-03-08 23:45:16 +0100 <geekosaur> https://github.com/geekosaur/dotty/blob/master/.bsa-common#L21-L53 for those who like their minds blown :þ
2022-03-08 23:47:10 +0100ubert(~Thunderbi@p200300ecdf3be9b38bc0692fc3914e47.dip0.t-ipconnect.de) (Quit: ubert)
2022-03-08 23:47:23 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e)
2022-03-08 23:47:32 +0100Guest|40(~Guest|40@dsl-94-229-145-149.pool.bitel.net)
2022-03-08 23:47:50 +0100ubert(~Thunderbi@p200300ecdf3be9b34516931a7c3fe14b.dip0.t-ipconnect.de)
2022-03-08 23:47:56 +0100Guest|40(~Guest|40@dsl-94-229-145-149.pool.bitel.net) ()
2022-03-08 23:48:33 +0100whatsupdoc(uid509081@id-509081.hampstead.irccloud.com)
2022-03-08 23:49:30 +0100 <[exa]> haskellnoob: I guess it's missing a simple conversion back into the bytestring. do you have a function that converts the hex back?
2022-03-08 23:49:32 +0100 <euouae> cool trick with IFS
2022-03-08 23:51:07 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Quit: Leaving)
2022-03-08 23:51:16 +0100ec(~ec@gateway/tor-sasl/ec) (Ping timeout: 240 seconds)
2022-03-08 23:51:49 +0100 <bgamari> geekosaur, heh, life isn't so bad for me
2022-03-08 23:51:56 +0100 <bgamari> romesrf, I'm in New Hampshire
2022-03-08 23:52:10 +0100kaph_(~kaph@93-39-148-20.ip76.fastwebnet.it)
2022-03-08 23:52:11 +0100 <bgamari> geekosaur, it is indeed a tad annoying that we have to do yet another release
2022-03-08 23:52:36 +0100 <bgamari> but as you say, this is a problem that we know how to fix
2022-03-08 23:52:49 +0100da39a3ee5e6b4b0d(~textual@2403:6200:8876:d2a9:6da2:b132:dfcb:fb0e) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2022-03-08 23:52:51 +0100 <bgamari> things could be much worse and we are certainly converging
2022-03-08 23:53:15 +0100 <bgamari> the "not" mistake on the other hand I was quite annoyed by :)
2022-03-08 23:53:35 +0100da39a3ee5e6b4b0d(~textual@mx-ll-171.5.29-46.dynamic.3bb.co.th)
2022-03-08 23:54:55 +0100kaph(~kaph@151.35.10.65) (Ping timeout: 272 seconds)
2022-03-08 23:55:33 +0100dsrt^(~dsrt@50.232.121.75)
2022-03-08 23:55:59 +0100 <haskellnoob> exa, I now have this, at least compiling: https://pastebin.com/n9HViRdP - but I think the usage of "fromJust" is wrong here
2022-03-08 23:57:48 +0100 <maerwald> haskellnoob: you can case match on it and use `fail "blah"` for Nothing
2022-03-08 23:58:03 +0100 <maerwald> https://hackage.haskell.org/package/aeson-2.0.3.0/docs/Data-Aeson-Types.html#t:Parser has a MonadFail instance
2022-03-08 23:58:37 +0100 <haskellnoob> that works, nice !!
2022-03-08 23:58:46 +0100 <haskellnoob> thanks a lot guys, you're my heros