Logs: freenode/#haskell
| 2020-10-08 21:36:59 | × | danvet_ quits (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) (Ping timeout: 246 seconds) |
| 2020-10-08 21:37:47 | × | snakemas1 quits (~snakemast@213.100.206.23) (Ping timeout: 240 seconds) |
| 2020-10-08 21:39:00 | → | zacts joins (~zacts@dragora/developer/zacts) |
| 2020-10-08 21:40:41 | → | kreetx joins (~markus@228-90-235-80.dyn.estpak.ee) |
| 2020-10-08 21:41:12 | × | radge quits (~dav@84.45.212.159) (Quit: WeeChat 2.9) |
| 2020-10-08 21:41:51 | × | raehik quits (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net) (Quit: WeeChat 2.8) |
| 2020-10-08 21:44:14 | × | LKoen quits (~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 2020-10-08 21:44:30 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 2020-10-08 21:46:23 | → | cosimone joins (~cosimone@93-47-228-249.ip115.fastwebnet.it) |
| 2020-10-08 21:46:51 | → | raehik joins (~raehik@cpc96984-rdng25-2-0-cust109.15-3.cable.virginm.net) |
| 2020-10-08 21:47:47 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 2020-10-08 21:50:29 | → | worc3131 joins (~quassel@2a02:c7f:c026:9500:7d0b:65d0:38a4:4786) |
| 2020-10-08 21:50:31 | → | proofofme joins (~proofofme@184-96-74-65.hlrn.qwest.net) |
| 2020-10-08 21:51:11 | → | thir joins (~thir@p200300f27f0fc60038c1b16891cbfa03.dip0.t-ipconnect.de) |
| 2020-10-08 21:53:38 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2020-10-08 21:53:46 | → | GyroW_ joins (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) |
| 2020-10-08 21:53:47 | × | GyroW_ quits (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) (Changing host) |
| 2020-10-08 21:53:47 | → | GyroW_ joins (~GyroW@unaffiliated/gyrow) |
| 2020-10-08 21:54:45 | → | oisdk joins (~oisdk@2001:bb6:3329:d100:7807:4c86:5073:949e) |
| 2020-10-08 21:54:53 | × | GyroW quits (~GyroW@unaffiliated/gyrow) (Ping timeout: 260 seconds) |
| 2020-10-08 21:55:16 | × | zacts quits (~zacts@dragora/developer/zacts) (Quit: leaving) |
| 2020-10-08 21:55:49 | → | zacts joins (~zacts@dragora/developer/zacts) |
| 2020-10-08 21:56:02 | × | thir quits (~thir@p200300f27f0fc60038c1b16891cbfa03.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2020-10-08 21:56:25 | → | frank001 joins (~frank001@178.162.212.214) |
| 2020-10-08 21:57:07 | <dolio> | (=<<) is good because it shows how homomorphisms of free algebras `m a -> m b` arise from maps `a -> m b`. |
| 2020-10-08 21:57:27 | × | st8less quits (~st8less@2603:a060:11fd:0:9c66:9b18:c21:60c) (Ping timeout: 240 seconds) |
| 2020-10-08 21:57:43 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-08 21:58:45 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Quit: leaving) |
| 2020-10-08 21:59:07 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 2020-10-08 22:01:21 | <dolio> | Of course, that only depends on `m a` being a free algebra. If you situate it in the category of all algebras, it's `(a -> r) -> m a -> r`, presuming `r` is an algebra. |
| 2020-10-08 22:03:28 | → | falafel joins (~falafel@2605:e000:1527:d491:1ccf:5c8d:7928:e9cc) |
| 2020-10-08 22:04:01 | × | ryansmccoy quits (~ryansmcco@156.96.151.132) (Ping timeout: 246 seconds) |
| 2020-10-08 22:04:36 | → | ryansmccoy joins (~ryansmcco@193.37.254.27) |
| 2020-10-08 22:04:36 | <dminuoso> | proofofme: Now to the next step. An applicative is simply a monoid in the category of endofunctors as well! |
| 2020-10-08 22:05:15 | × | fendor quits (~fendor@77.119.131.69.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2020-10-08 22:05:17 | <dminuoso> | But that category is equipped with a different tensor. In case of Monad it's endofunctor composition, and in case of Applicative it's Day convolution. :) |
| 2020-10-08 22:05:41 | monochrom | cries |
| 2020-10-08 22:05:46 | <dolio> | In that case it doesn't need to be an endofunctor, though. |
| 2020-10-08 22:06:35 | × | worc3131 quits (~quassel@2a02:c7f:c026:9500:7d0b:65d0:38a4:4786) (Ping timeout: 272 seconds) |
| 2020-10-08 22:07:34 | <proofofme> | interesting! I am referencing all this stuff right now |
| 2020-10-08 22:08:22 | <monochrom> | I now agree with St. Augustine that you math nerds are pure evil. :) |
| 2020-10-08 22:08:41 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2020-10-08 22:09:10 | <hpc> | we should make like pythagoras and throw them overboard |
| 2020-10-08 22:09:18 | <monochrom> | Programmers work very hard to code up things, then a math nerd comes along to point out that "it's just a special case of this conceptually simple thing" |
| 2020-10-08 22:09:19 | <dminuoso> | proofofme: As a fun excercise, try to think of other tensors and see whether you discover more such monoids. |
| 2020-10-08 22:09:46 | <dminuoso> | There's at least three more tensors that yield interesting results. |
| 2020-10-08 22:10:22 | <monochrom> | One time I was TAing in a computer graphics course. In terms of coding up ray tracing for example, intersection test for a ray with a sphere is very different from intersection test for a ray with a cube. |
| 2020-10-08 22:10:32 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-08 22:10:56 | <dminuoso> | tomsmeding: I managed a testcase btw: https://gitlab.haskell.org/ghc/ghc/-/issues/18822 |
| 2020-10-08 22:11:16 | <monochrom> | Then a math prof friend visited the graphics prof, we brought up that, and the math prof friend pointed out "but a cube is just a sphere under a different norm". |
| 2020-10-08 22:11:54 | <dolio> | Maybe programmers should have looked at what math people were doing decades before, so they wouldn't have to reinvent it. |
| 2020-10-08 22:12:14 | <dminuoso> | dolio: Heh. Or even at what programmers were doing decades before! |
| 2020-10-08 22:12:25 | <dminuoso> | Im looking at you, mongodb developers. |
| 2020-10-08 22:12:35 | <dolio> | Yeah, that too. |
| 2020-10-08 22:13:23 | <monochrom> | I am sympathetic to them, though in disagreement, because as a consequence of the victors writing history, the nosql people never knew that historically databases started out as nosql. |
| 2020-10-08 22:13:23 | × | jespada quits (~jespada@90.254.245.15) (Ping timeout: 246 seconds) |
| 2020-10-08 22:13:27 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 2020-10-08 22:13:58 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Remote host closed the connection) |
| 2020-10-08 22:14:12 | <dminuoso> | There's an influx of new programmers, completely oblivious about POSIX, relational algebra, interesting languages... |
| 2020-10-08 22:14:14 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 2020-10-08 22:14:35 | <monochrom> | If you tell them the old name "network database" they will totally misunderstand you because they don't know that "network" simply meant pointers back then. |
| 2020-10-08 22:14:58 | <monochrom> | (They will think you mean, like, cloud.) |
| 2020-10-08 22:14:59 | <dminuoso> | monochrom: If I stare at some of the early steps of MongoDB they are not just repeating it, but repeating it poorly. MongoDB will crash if you use more than 2GiB in your database on a 32 bit architecture. |
| 2020-10-08 22:15:00 | <dolio> | If you squint at the 'algebra' thing above, you see that Lawvere invented CPS for algebra 12 years before Steele and Sussman. :) |
| 2020-10-08 22:15:04 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-08 22:15:11 | <dminuoso> | I mean, for a database that's saying quite a lot. |
| 2020-10-08 22:15:20 | <dminuoso> | Or the complete lack of any properties of ACID early on |
| 2020-10-08 22:15:46 | <dminuoso> | It seemed to have been a "Lets see how hard a database can be, if we dont do any reading and just start writing" |
| 2020-10-08 22:16:58 | → | jespada joins (~jespada@90.254.245.15) |
| 2020-10-08 22:18:48 | <maralorn> | dolio: I say this as a mathematician. Normally people (like physicists, programmers) invent something and then after a few decads mathematicians are like "well what you did is btw. this really simple concept, that we invented motivated by what you did" |
| 2020-10-08 22:19:49 | <monochrom> | And while we're at it... I wish I could write "C because (because A, so B)" up there for that sentence that I ended up wording "C because as a consequence of A, B". |
| 2020-10-08 22:20:34 | <monochrom> | So the logical structure of what I was saying is: (A therefore B) therefore C. Marvel at the CPS structure! >:) |
| 2020-10-08 22:20:55 | → | mirrorbird joins (~psutcliff@2a00:801:3f8:10df:3fb2:3ec3:6676:3873) |
| 2020-10-08 22:21:38 | <dolio> | maralorn: If I were talking to mathematicians I'd be playing the opposite side. :) |
| 2020-10-08 22:21:58 | <maralorn> | ^^ |
| 2020-10-08 22:22:27 | <dolio> | They just stole our Martin-löf type theory. |
| 2020-10-08 22:22:39 | <maralorn> | It's not always like that. But in general I think both sides deserve a lot of credit. And in a world where people tend to idolize abstractness, rigor and brute intelligence. I try to nudge the world view into the direction of valuing intuition, motivation and experience. |
| 2020-10-08 22:22:40 | <monochrom> | heh |
| 2020-10-08 22:24:22 | <monochrom> | That is a minority world from what I saw. |
| 2020-10-08 22:24:51 | <monochrom> | The majority world idolize intuition, experience, and after-the-fact rationalization instead. |
| 2020-10-08 22:25:00 | <monochrom> | Just look at politics. |
| 2020-10-08 22:25:43 | × | spew quits (uid195861@gateway/web/irccloud.com/x-ypeilgetepuhkpyp) (Quit: Connection closed for inactivity) |
| 2020-10-08 22:26:12 | <dolio> | I mean, it wasn't long ago that I was talking in here about how mathematicians are all wrong when they tell physicists they 'aren't allowed to do' various stuff with derivatives because it doesn't work in classical analysis or whatever. |
| 2020-10-08 22:26:46 | <dolio> | Because they went off and studied something different than what physicists are actually doing, but decided the math was the real thing. |
| 2020-10-08 22:27:30 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2020-10-08 22:29:03 | → | conal joins (~conal@64.71.133.70) |
| 2020-10-08 22:29:13 | × | conal quits (~conal@64.71.133.70) (Client Quit) |
| 2020-10-08 22:30:28 | <proofofme> | So let's say that I have a field of type `Maybe [String]` and want to compare it to elements from input of type [String], and return the index of the first match, if it exists. Would I use mapM_ to accomplish this? |
| 2020-10-08 22:32:21 | <monochrom> | No. More like fmap. |
| 2020-10-08 22:32:57 | <monochrom> | What does "compare" mean to compare Nothing against ["hello", "hi"] ? |
| 2020-10-08 22:34:33 | <proofofme> | Just ["hello", "hi"], yeah? |
| 2020-10-08 22:34:38 | <proofofme> | is that what you mean? |
| 2020-10-08 22:34:49 | <dminuoso> | So, just out of curiosity proofofme |
| 2020-10-08 22:34:54 | <monochrom> | No. You wrote "compare Maybe [String] to [String]". |
| 2020-10-08 22:35:05 | <dminuoso> | You dabble in non-trivial category theory but seem to be stuck in the beginning steps of Haskell. |
| 2020-10-08 22:35:11 | <dminuoso> | What's your motivation behind learning CT? |
| 2020-10-08 22:35:17 | <monochrom> | So I compare Nothing :: Maybe [String] to ["hello", "hi"] :: [String] |
| 2020-10-08 22:35:31 | <maralorn> | I read up on the Monads are Monoids in the category of Endofunctors thing. A few years ago I was like "A now I get it.". Now I feel that's like saying "a bycicle is just two wheels with pedals." It's not really wrong but it's a really bad definition and I can think of contraptions that fit the name, that don‘t match at all. |
| 2020-10-08 22:36:29 | <proofofme> | My main motivation is personal fulfillment in learning this stuff, but also applying it professionally to write better code, whether it's Haskell or whatever else I'm using. |
| 2020-10-08 22:37:10 | <proofofme> | I'm really new at non-trivial Haskell |
All times are in UTC.