Logs on 2022-10-11 (liberachat/#haskell)
| 00:01:24 | × | causal quits (~user@50.35.83.177) (Quit: WeeChat 3.6) |
| 00:02:40 | → | causal joins (~user@50.35.83.177) |
| 00:02:59 | × | beteigeuze quits (~Thunderbi@89.187.168.50) (Remote host closed the connection) |
| 00:03:18 | → | beteigeuze joins (~Thunderbi@89.187.168.50) |
| 00:12:44 | → | arkeet joins (arkeet@moriya.ca) |
| 00:18:24 | × | raym quits (~aritra@user/raym) (Ping timeout: 264 seconds) |
| 00:23:45 | → | raym joins (~aritra@user/raym) |
| 00:29:27 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 00:31:02 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Quit: WeeChat 3.6) |
| 00:32:03 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 248 seconds) |
| 00:32:35 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 00:33:51 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 244 seconds) |
| 00:40:03 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 244 seconds) |
| 00:42:45 | → | rockystone joins (~rocky@user/rockymarine) |
| 00:45:08 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
| 00:47:36 | → | nate1 joins (~nate@98.45.169.16) |
| 00:48:50 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 00:48:51 | <Clinton[m]> | Is there a function like this (or a generalisation):... (full message at <https://libera.ems.host/_matrix/media/r0/download/libera.chat/6209b5251f695d948d8bcf677b32e7c7832a83e5>) |
| 00:50:36 | <EvanR> | taking an Either a b as an input, weird |
| 00:50:53 | <Clinton[m]> | * -> d))`, as |
| 00:52:12 | <Clinton[m]> | In my particular case I've got an `EitherT SomeError m (Maybe Good)` and I want to transform this into `EitherT ABiggerErrorType m Good`. |
| 00:52:27 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 244 seconds) |
| 00:52:58 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Ping timeout: 244 seconds) |
| 00:53:20 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 265 seconds) |
| 00:53:35 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 00:54:40 | <Clinton[m]> | like:... (full message at <https://libera.ems.host/_matrix/media/r0/download/libera.chat/0240ecca2d280e5e937b9cb4cfd6f211408140b8>) |
| 00:54:58 | <Clinton[m]> | * like:... (full message at <https://libera.ems.host/_matrix/media/r0/download/libera.chat/1498984f3fd3e6f6077d5b5db03fc8b0a51e13d6>) |
| 00:58:07 | <EvanR> | error hierarchy |
| 00:58:22 | → | lottaquestions_ joins (~nick@2607:fa49:503e:7100:a9a5:f580:1f2d:9d23) |
| 01:01:39 | <ski> | pure (\x y -> x ++ '.' : y) <$> many1' digit <* char '>' <*> many1' digit -- argento |
| 01:02:59 | <ski> | DrScheme^WDrRacket does have "language levels", where you only introduce a simplified fragment of the system, at a time. Helium did a simplified Haskell, for beginners (more attention to diagnostics, skipping type classes, ..) |
| 01:03:55 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
| 01:04:37 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 01:06:02 | <ski> | @type Control.Monad.Except.mapExceptT . fmap -- Clinton[m] |
| 01:06:04 | <lambdabot> | Functor n => (Either e a -> Either e' b) -> ExceptT e n a -> ExceptT e' n b |
| 01:07:04 | <johnjaye> | idk. i would think those types of things would be meaningless unless they come with the base product, as dr. scheme does |
| 01:07:15 | × | Franciman quits (~Franciman@mx1.fracta.dev) (Read error: Connection reset by peer) |
| 01:07:18 | <johnjaye> | something like, the default is baby mode and then you have to enter a command to enable advanced mode. |
| 01:07:57 | <ski> | language extensions are something like that, except starting from the "default full language", tacking more on |
| 01:08:29 | <ski> | .. so, maybe we need "language restrictions" ? |
| 01:09:50 | <ski> | gqplox : error actually tells you that it expected a function but found a list |
| 01:11:58 | <johnjaye> | like i'm learning haskell and i had no idea what that is |
| 01:12:02 | <johnjaye> | nor do i really have the motivation to try it |
| 01:12:06 | <EvanR> | {-# UNLANGUAGE NoPolymorphism #-} |
| 01:12:36 | <EvanR> | {-# LANGUAGE NoSyntaxSugar #-} |
| 01:12:42 | <monochrom> | Wait that's double-negative. :) |
| 01:12:48 | <johnjaye> | ski: the logic would be that advanced users would know to pass some option like -abc to get the full language, where a beginner just types 'ghci' say |
| 01:13:08 | <monochrom> | {-# ain't no GADTs #-} |
| 01:13:26 | <EvanR> | in the spirit of use more words and less configuration options, have two different ghci commands |
| 01:13:46 | <EvanR> | ghci vs noobci or something |
| 01:13:51 | <jackdk> | Isn't that exactly what language extensions do? |
| 01:14:15 | <EvanR> | yeah it's pretty annoying too xD |
| 01:14:37 | <EvanR> | first, a page of extensions activated in every file for stuff I consider "should be in the base game" |
| 01:14:41 | <monochrom> | Well there is also the issue with Prelude being too large and you need a smaller one to go with a smaller language. |
| 01:15:19 | <ski> | johnjaye : "i had no idea what that is" -- "that" being ? |
| 01:16:00 | <ski> | johnjaye : yea. or perhaps beginners could use `ghci -basic' or something |
| 01:16:30 | <ski> | monochrom : "yea, sure." |
| 01:16:56 | <ski> | (re some linguist claiming that affirmative was never used to mean "no") |
| 01:17:33 | <ski> | (oh, actually, i think it was "yea, yea.", doubling affirmative, now that i think about it) |
| 01:17:43 | <johnjaye> | ski: beginning users are unlikely to do that. but i'm not try to be dogmatic. |
| 01:17:55 | <monochrom> | I think "yea yea" is sarcasm and so it applies to "no" too. |
| 01:18:12 | <EvanR> | some stuff extensions are commonly used for are... pretty common |
| 01:18:15 | <gqplox> | ski: yep I was being dumb oops, thanks for that |
| 01:18:16 | <johnjaye> | in general i think most stuff in computing is not geared around educating newcomers except maybe scheme. but scheme is basically purely academic and hard to write real programs with |
| 01:18:19 | <johnjaye> | so you see the problem |
| 01:18:22 | <ski> | johnjaye : an instructor or tutorial/book could tell them to supply that, to begin with .. but then not everone goes through that route |
| 01:18:29 | → | Franciman joins (~Franciman@mx1.fracta.dev) |
| 01:18:53 | <johnjaye> | now that i think about it i'm not sure which of these links i have is the official haskell tutorial. i have 4 or 5 bookmarks |
| 01:19:02 | <gqplox> | Although I was trying an example after where where it said something like "probably incorrect no of arguments supplied, got one expected two" or something |
| 01:19:09 | <EvanR> | haskell.org/tutorial \o/ |
| 01:19:12 | <johnjaye> | one is learn you a haskell. the other says haskell 98 intro. learn haskell in x minutes |
| 01:19:22 | <EvanR> | vintage tutorial |
| 01:20:00 | <monochrom> | Every educational language fails to get traction. |
| 01:20:11 | <EvanR> | learn you a haskell isn't the official tutorial, but it crazy how much inertia it has |
| 01:20:13 | <ski> | gqplox : point is to learn what to look for first (mismatch) in error messages, see if that gives a clue for the source of the problem in the source, before trying to more carefully parse the error message |
| 01:21:04 | <johnjaye> | monochrom: well that's the catch-22. it seems like you have to be an educational language to really be newbie-friendly. but then that's all you do. |
| 01:21:20 | <johnjaye> | anyway. i'm learning a lot of haskell and it's pretty fun. i saw a strange loop talk about it. a couple actually |
| 01:21:45 | → | rekahsoft joins (~rekahsoft@142.189.68.220) |
| 01:22:20 | <johnjaye> | i think i saw hoogle as well but couldn't tell if it was official or not |
| 01:22:34 | × | rekahsoft quits (~rekahsoft@142.189.68.220) (Remote host closed the connection) |
| 01:22:37 | <gqplox> | Yes I agree, I felt kind of bad asking because I'm that beginner asking "why doesn't this work, it gives this error" and the error explains exactly what the problem is, so sorry for that. |
| 01:23:08 | → | rekahsoft joins (~rekahsoft@142.189.68.220) |
| 01:23:26 | <monochrom> | The human brain naturally petrifies upon seeing things marked as error messages. |
| 01:23:54 | <monochrom> | If I say "please press enter" you will press enter. |
| 01:24:28 | <monochrom> | If I say "an error has occurred, but it can be auto-fixed if you press enter" you freeze and you don't know what to do. |
| 01:24:43 | <EvanR> | especially in case it says, "Keyboard not detected. Press F1 to continue" |
| 01:24:50 | <monochrom> | haha |
| 01:24:56 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 01:24:58 | <johnjaye> | i've just accepted that error messages are part of the learning process. |
| 01:25:07 | <gqplox> | Haha true, I've improved a bit but I still have a long way to go :) |
| 01:25:15 | <johnjaye> | meaning. you should be actively trying to cause errors and determining what in the code you typed that caused that error. |
| 01:25:25 | <gqplox> | I remember I saw my fried using terminal for the first time, I thought ls and cat were like black magic haha |
| 01:25:32 | <gqplox> | friend* |
| 01:25:45 | <johnjaye> | well they are |
| 01:25:58 | <johnjaye> | how many coreutil commands do you know outside of those 'magic' commands like cat, ls, grep? i bet not a lot |
| 01:26:56 | <johnjaye> | and if you do then you're yottachad and don't need me to tell you that |
| 01:27:37 | × | xff0x quits (~xff0x@ai071162.d.east.v6connect.net) (Ping timeout: 252 seconds) |
| 01:27:55 | <EvanR> | unless you're on one of these new fangled systems with everything compiled into the kernel or something, you can even look in /bin or /usr/bin to see all the commands xD |
| 01:28:10 | <EvanR> | and wonder wtf they are. And then read the manual |
| 01:28:40 | <johnjaye> | with learning it's always a chicken and egg problem though. as video game designers will tell you |
| 01:28:47 | <johnjaye> | how do you communicate that to the player without just telling them |
| 01:29:26 | <johnjaye> | i remember trying to figure out how printf could print hex characters on bsd. the man page then said This program deliberately does not convert hexadeximal codes. |
| 01:29:31 | <ski> | gqplox : error messages are known to take a while to get used to, to learn what to focus on most / at first, and learning the most common reasons for particular kinds of errors |
| 01:29:33 | <johnjaye> | so... that was helpful to know! |
| 01:29:37 | <ski> | gqplox : <https://pics.me.me/an-engineer-helping-a-designer-whoa-youre-a-hacker-no-43162553.png> |
| 01:29:50 | <EvanR> | there will be a side quest on disc 3 which leads them to /usr/bin with the promise of loot, and they will wonder how the hell they got this far without knowing |
| 01:29:52 | <johnjaye> | but it's a bit weird to just out and out tell you that |
| 01:30:04 | <gqplox> | Hahah true |
| 01:30:48 | <EvanR> | I vaguely remember a "unix tutorial" telling me to type `where ls' or something to see where the program is located |
| 01:31:09 | <EvanR> | so at least that's worth mentioning |
| 01:31:10 | <gqplox> | Well I'll keep trying and come back here when I inevitably get stuck again ;) Hopefully for a better reason though |
| 01:31:11 | <ski> | johnjaye : istr HL2 had some nice unobtrusive tutorial stuff (barrel is in the way (you can whack or shoot barrels to turn them on fire), crate is in the way (you can get goods from these crates), ..) |
| 01:31:36 | <gqplox> | Yeah I found which useful a few times when I had some issues with homebrew |
| 01:31:41 | <johnjaye> | EvanR: that's some unix tutorial since 'where' is a windows command... |
| 01:31:58 | <monochrom> | Soon, if you know about files and folders, you will be a hacker too. Because there is a new generation of young people who have only used phones and tablets, not even Windows or Mac. |
| 01:32:05 | → | frost joins (~frost@user/frost) |
| 01:32:11 | <EvanR> | so windows stole the where command eh |
| 01:32:17 | <EvanR> | embrace extend and so on |
| 01:32:44 | <ski> | johnjaye : "stuff in computing is not geared around educating newcomers" -- you might enjoy "Re: Mercury in academic teaching?" by Richard A. O'Keefe in 2006-10-(09,10) at <https://www.mercurylang.org/list-archives/users/2006-October/004000.html>,<https://www.mercurylang.org/list-archives/users/2006-October/004011.html> |
| 01:33:02 | <ski> | "Mercury has a much steeper learning curve, but in many cases the compiler tells you when your program is not going to do what you thought it would." |
| 01:33:12 | <ski> | "That's not a \"but\", it's really a \"because\".","Mercury has a much steeper learning curve, BECAUSE in many cases the compiler tells you when your program is not going to do what you thought it would, and you never get to find out what would have happened, so you don't understand what the compiler is trying to tell you." |
| 01:33:32 | <ski> | "Over the years, one of the top complaints that I have heard from people who have taken programming courses and found them very hard going is \"I could never make sense of the compiler error messages.\"" |
| 01:33:43 | <ski> | "Come to think of it, one of the things that drives me up the wall is 3rd year students handing in C programs with obvious problems that the C compiler DID tell them about, but they weren't EXPECTING to understand anything the compiler said, so they didn't bother looking at what it did say or even the particular lines it was talking about." |
| 01:33:51 | <ski> | "What I am saying here has been said before, at greater length, with a wealth of supporting evidence, by my elders and betters: A programming system meant to be used by people learning a new kind of programming language had better have really good error reports." |
| 01:34:17 | <gqplox> | I heard that the rust compiler has really nice error messages |
| 01:35:59 | <ski> | generally, people often have an unhealthy attitude towards errors, want to brush them off (e.g. to run-time). or having a system "helpfully" correct a mistake you did (especially if without telling you), decreasing the utility of negative feedback, lowering edit distance to an accepted program that does something unintended |
| 01:36:22 | × | beteigeuze quits (~Thunderbi@89.187.168.50) (Ping timeout: 244 seconds) |
| 01:36:33 | <ski> | (correct, or guess .. often the same thing, i suppose) |
| 01:36:45 | <johnjaye> | well. c compiler error messages are terrible |
| 01:37:00 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 268 seconds) |
| 01:37:02 | <monochrom> | Generally, people are greedy. |
| 01:37:03 | <johnjaye> | i would expect students to be told this and to learn to understand them as much as the preprocessor or linker |
| 01:37:26 | <ski> | ("oh, this input doesn't make sense. let me just return a nonsensical result you probably won't detect, rather that complaining loudly about the issue") |
| 01:37:55 | <ski> | johnjaye : true. but they're still better than nothing |
| 01:38:26 | <johnjaye> | i think it hits on the larger issue also of reasoning about code. haskell is kind of the opposite of c in that respect from what i can tell |
| 01:38:39 | <johnjaye> | c has all these arcane rules about when something might get converted to something else or when this operation will affect this other one. |
| 01:38:48 | <johnjaye> | whereas haskell is very mathematical and composable |
| 01:38:59 | <monochrom> | Is that why I don't find GHC error messages terrible? I had got used to GCC error messages. :) |
| 01:39:09 | <EvanR> | PHP's white screen effect. No error messages, no problem xD |
| 01:39:14 | <EvanR> | and no website. It's great |
| 01:39:19 | <johnjaye> | the most bizarre one is that literal constants get placed into unsigned, signed, unsigned, signed types depending on size. the smallest one first |
| 01:39:26 | <johnjaye> | how are you supposed to reason about that |
| 01:40:26 | → | cyphase joins (~cyphase@user/cyphase) |
| 01:40:32 | <EvanR> | I mainly pretend number constants are just integers (math) until the very last minute, and hope it doesn't matter xD |
| 01:41:08 | <ski> | EvanR : TCsh has `where' (and `which') as builtins |
| 01:41:39 | <EvanR> | oh dang the command is which |
| 01:43:53 | <EvanR> | in the spirit of ask forgiveness instead of permission, my C implementation uses infinite precision integers. Until it doesn't |
| 01:44:11 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 260 seconds) |
| 01:44:46 | <EvanR> | unfortunately you don't usually get an error message when it doesn't work! |
| 01:45:14 | <ski> | johnjaye : "the larger issue also of reasoning about code" -- i would be happy if the larger programming "community" (such as it is ..), could start to acknowledge and talk about reasonability ("predictive power", including refactoring ease) more comparably to expressivity ("cavalier power" .. this and that language feature) |
| 01:45:35 | <EvanR> | but in particular problems, if you can't / don't observe finite precision, it effectively doesn't exist |
| 01:45:39 | <ski> | .. someone should build the DeathStation 9000 |
| 01:45:54 | <johnjaye> | heh. well c is unique. reading it is like reading a commentary on the constitution with 50 volume set |
| 01:46:09 | <johnjaye> | i was studying this for example today: https://port70.net/~nsz/c/c11/n1570.html#6.5.6p9 |
| 01:46:23 | <ski> | ah, you mean reading the standard |
| 01:46:30 | <johnjaye> | now imagine saying something like that about haskell. |
| 01:46:39 | <EvanR> | johnjaye, join me in reviewing documents on B instead. It's like going back to original D&D |
| 01:46:50 | <EvanR> | a breath of fresh air |
| 01:46:51 | <johnjaye> | 'the two integers in haskell shall be subtracte but if ONE of them is larger than the other and the other one is smaller by 2 than the former THEN the result is defined as..." |
| 01:47:11 | <johnjaye> | haha. isn't there a B port somewhere. i think wikipedia had a link |
| 01:47:34 | <EvanR> | just the documentation is the topic at the moment heh |
| 01:47:43 | <EvanR> | or what's left of it |
| 01:47:54 | <johnjaye> | yeah i heard about it but didn't read it |
| 01:47:57 | <johnjaye> | is it interesting |
| 01:48:09 | <EvanR> | just short and to the point |
| 01:49:03 | <EvanR> | https://www.bell-labs.com/usr/dmr/www/kbman.pdf |
| 01:49:08 | <ski> | EvanR : before 3rd ed. ? |
| 01:49:32 | <EvanR> | lol 3rd edition |
| 01:49:45 | <EvanR> | you hurt my soul |
| 01:54:27 | <monochrom> | w00t, McIlroy |
| 01:55:03 | → | leungbk joins (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) |
| 01:56:43 | × | leungbk quits (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) (Client Quit) |
| 01:57:23 | → | leungbk joins (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) |
| 01:57:51 | <ski> | EvanR : ah, that's nice. B has block-less functions |
| 01:58:27 | × | mr_mxyzptlk quits (~Srain@2806:266:48a:240:a579:dfff:fd47:c997) (Remote host closed the connection) |
| 01:59:21 | × | jmorris quits (uid537181@id-537181.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 01:59:41 | ski | . o O ( "The character set used in B is ANSCII." ) |
| 02:00:55 | <EvanR> | yeah that was funny at first now I can't stop finding various spellings of ascii |
| 02:01:11 | <ski> | escape sequences doubled as digraphs ? |
| 02:01:11 | <EvanR> | which was basically brand new at that time |
| 02:01:30 | ski | 's seen "PETSCII" |
| 02:02:12 | <EvanR> | no digraphs in that document, though it's pretty old and B went on to get tweaks at each site |
| 02:02:34 | → | ubert1 joins (~Thunderbi@77.119.164.69.wireless.dyn.drei.com) |
| 02:02:56 | × | ubert quits (~Thunderbi@77.119.192.27.wireless.dyn.drei.com) (Ping timeout: 268 seconds) |
| 02:02:57 | <ski> | yea, i was wondering why `*(' and `*)' would expand to `{' and `}', if not also outside string and character literals |
| 02:02:57 | ubert1 | is now known as ubert |
| 02:03:36 | × | leungbk quits (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) (Quit: ERC 5.4 (IRC client for GNU Emacs 28.2)) |
| 02:04:04 | <EvanR> | maybe your keyboard didn't have those keys but they still needed to process them, since they are in ascii |
| 02:04:23 | → | leungbk joins (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) |
| 02:04:32 | <EvanR> | but then how do you write code |
| 02:04:41 | → | yuzhao_ joins (~yuzhao@36.112.45.72) |
| 02:04:48 | <EvanR> | well, maybe they were digraphs after all |
| 02:05:00 | <ski> | ("ANSCII" sounds like emphasizing that it came from ANSI .. or maybe it's just a confusion/misspelling) |
| 02:06:29 | × | yuzhao quits (~yuzhao@36.112.45.72) (Ping timeout: 252 seconds) |
| 02:06:53 | → | rockystone joins (~rocky@user/rockymarine) |
| 02:07:42 | <EvanR> | you can still find references to the American National Standard Code for Information Interchange https://www.ibm.com/docs/en/zvse/6.2?topic=SSB27H_6.2.0/fa2mr_app_b_ascii.html |
| 02:09:21 | zzz | is now known as zzz[m] |
| 02:09:26 | [_] | is now known as [itchyjunk] |
| 02:09:55 | zzz[m] | is now known as zzz |
| 02:11:36 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 260 seconds) |
| 02:11:37 | <Clinton[m]> | <ski> "@type Control.Monad.Except...." <- Thanks ski that's close enough! |
| 02:11:50 | <Clinton[m]> | > <@ski:libera.chat> @type Control.Monad.Except.mapExceptT . fmap -- Clinton |
| 02:11:51 | <Clinton[m]> | * Thanks ski that'll do the job! |
| 02:11:52 | <lambdabot> | <hint>:1:1: error: parse error on input ‘<@’ |
| 02:13:07 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 02:13:24 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:15:09 | → | extratail joins (~archie@2804:214:82be:8ae9:99a:eac4:866e:815c) |
| 02:16:06 | <extratail> | Hello. There's a directory called `.stack` in my $HOME_DIR . It has a sort of big size. What happens if I delete it? |
| 02:18:40 | <jackdk> | I haven't used stack for years, but I think you'll just have to redownload GHCs and packages if you run stack again. There might also be "global project" settings in there I think |
| 02:19:16 | × | gqplox quits (~textual@97e654ef.skybroadband.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 02:20:15 | <ski> | (fwiw, CC64 (non-cross C compiler, written in ultraFORTH^WvolksFORTH) for Commodore 64, by Philip Zembrod (who semi-recently took the project up again), |
| 02:20:18 | <ski> | <https://github.com/pzembrod/cc64>,<https://sourceforge.net/projects/cc64/>,<https://telarity.com/~dan/cbm/languages.html#C>,<http://www.csbruce.com/cbm/ftp/c64/programming/cc64v0[34].(zip|txt)>(,<https://www.lyonlabs.org/commodore/onrequest/collections.html>) patched PETSCII charset, to include characters `\^_{|}~', rather than using digraphs) |
| 02:20:26 | <ski> | Clinton[m] : you can still do it by hand, if you want to .. |
| 02:20:54 | × | leungbk quits (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) (Quit: ERC 5.4 (IRC client for GNU Emacs 28.2)) |
| 02:20:57 | <ski> | @type (ExceptT .) . (. runExceptT) . fmap |
| 02:20:58 | <lambdabot> | Functor m => (Either e1 a1 -> Either e2 a2) -> ExceptT e1 m a1 -> ExceptT e2 m a2 |
| 02:21:38 | → | leungbk joins (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) |
| 02:23:59 | <extratail> | jackdk, Stack is not a recommended tool anymore? What's the standard now? Just Cabal? |
| 02:24:51 | <jackdk> | I have personally had no major problems with cabal for many years. Stack still appears to be developed and I think had a release recently |
| 02:25:53 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 02:26:58 | <jackdk> | I think also it still doesn't support backpack or named internal libraries, which has slowed adoption of such things. Is that still true? |
| 02:27:47 | × | jero98772 quits (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) (Remote host closed the connection) |
| 02:28:50 | → | andreabedini joins (~andreabed@8s8kj681vht2qj3xkwc5.ip6.superloop.com) |
| 02:35:53 | <EvanR> | Oh, I heard backpack is dead in the water |
| 02:36:37 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 02:36:37 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:36:37 | finn_elija | is now known as FinnElija |
| 02:41:35 | × | leungbk quits (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) (Quit: ERC 5.4 (IRC client for GNU Emacs 28.2)) |
| 02:41:49 | ski | . o O ( "C compiler written in Forth" in 2020-12-18 at <https://www.youtube.com/watch?v=u4_gSYVh87c>,"cc64 - a Small C compiler written in Forth" in 2020-12-29 at <https://www.youtube.com/watch?v=X7kJiuD_PFM> by Philip Zembrod ) |
| 02:42:49 | <ski> | extratail : "The Cabal/Stack Disambiguation Guide" in 2019-07-03 at <https://gist.github.com/merijn/8152d561fb8b011f9313c48d876ceb07> might be interesting |
| 02:43:04 | → | leungbk joins (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) |
| 02:43:16 | × | leungbk quits (~user@2603-8000-1201-2dd2-5d38-428e-02cf-32d2.res6.spectrum.com) (Remote host closed the connection) |
| 02:44:18 | <EvanR> | they really cut down on the C |
| 02:44:20 | → | rockystone joins (~rocky@user/rockymarine) |
| 02:44:26 | <EvanR> | probably for the better |
| 02:45:42 | <ski> | "Supported subset of the C language cc64 is based on the old K&R standard. No ANSI, sorry. There are, however, some restrictions. Only int and char as basic data types are supported. No structs, no unions, only one level of pointer (nothing like char **p). No type casts. No goto. #define can only give a numeric value to a macro. No proper text substitution. No macros with parameters. No #undef. No |
| 02:45:48 | <ski> | #ifdef/#ifndef. No typedef, no enum. That's it, I think." |
| 02:47:01 | <ski> | "C extensions There are two non-standard declaration forms in cc64. They both include an operator, /= and *=. With /= an explicit value is assigned to a symbol, e.g. extern int i /= 0x9ffe ; extern char fgetc() /= 0xa02 ; They usually are not used explicitly in programs but appear in library header files (see below)." |
| 02:47:24 | × | Typedfern quits (~Typedfern@216.red-83-37-34.dynamicip.rima-tde.net) (Ping timeout: 265 seconds) |
| 02:47:53 | <ski> | "cc64 supports a special kind of functions. They only take one argument and can be called very fast without any software stack manipulation, just with the parameter in a/x. They will normally be written in assembler and are declared with *=, e.g. extern char getchar() *= 0xffcf ;" |
| 02:49:24 | → | tgi joins (~thegeekin@189.180.118.117) |
| 02:51:21 | ski | idly wonders in which environments `HOME_DIR' is set |
| 02:54:51 | × | causal quits (~user@50.35.83.177) (Quit: WeeChat 3.6) |
| 02:55:56 | × | thegeekinside quits (~thegeekin@189.180.118.117) (Ping timeout: 244 seconds) |
| 02:56:14 | → | thegeekinside joins (~thegeekin@189.180.118.117) |
| 02:56:36 | <EvanR> | paraphrase "you know what would be really cool, if you take your parser for C and make it output forth code" xD |
| 02:56:42 | → | nate1 joins (~nate@98.45.169.16) |
| 02:57:10 | <EvanR> | (instead of machine code) |
| 02:57:27 | × | thegeekinside quits (~thegeekin@189.180.118.117) (Remote host closed the connection) |
| 02:57:35 | × | tgi quits (~thegeekin@189.180.118.117) (Remote host closed the connection) |
| 02:57:49 | × | td_ quits (~td@muedsl-82-207-238-191.citykom.de) (Ping timeout: 252 seconds) |
| 02:57:51 | <probie> | Is backpack dead, or simply not seeing much use, because of a lack of support from things like haddock? |
| 02:58:32 | <probie> | (or alternatively, dead because of a lack of convincing use cases) |
| 02:59:43 | → | td_ joins (~td@94.134.91.197) |
| 03:00:25 | → | thegeekinside joins (~thegeekin@189.180.118.117) |
| 03:02:05 | × | frost quits (~frost@user/frost) (Quit: Client closed) |
| 03:06:50 | <sm> | dead or dormant because it doesn't help haskell users and tool devs already overloaded by complexity |
| 03:11:46 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Remote host closed the connection) |
| 03:12:59 | × | ddellacosta quits (~ddellacos@86.106.143.227) (Ping timeout: 244 seconds) |
| 03:13:20 | → | leungbk joins (~user@2603-8000-1201-2dd2-4bcb-8ea7-10ea-7a7c.res6.spectrum.com) |
| 03:15:37 | → | razetime joins (~quassel@117.193.4.181) |
| 03:18:11 | × | jbayardo quits (~jbayardo@20.83.116.49) (Remote host closed the connection) |
| 03:21:14 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 03:21:40 | <probie> | That's fair. When I first heard about it, I thought it might have seen use as a way of handling orphan instances. I think I've only heard it mentioned once in recent memory, and that was edward kmett giving a talk about https://github.com/ekmett/unboxed |
| 03:23:50 | → | loras joins (~loras@c-73-139-125-125.hsd1.fl.comcast.net) |
| 03:27:17 | → | jbayardo joins (~jbayardo@20.83.116.49) |
| 03:30:56 | × | jbayardo quits (~jbayardo@20.83.116.49) (Remote host closed the connection) |
| 03:33:22 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 03:33:24 | <Clinton[m]> | Is there any extension that allows this:... (full message at <https://libera.ems.host/_matrix/media/r0/download/libera.chat/91ac1d0c2ad75361dbfcca7b682fa9704436b0bb>) |
| 03:33:39 | → | img joins (~img@user/img) |
| 03:34:05 | → | talismanick joins (~talismani@2601:200:c100:c9e0::1b0b) |
| 03:34:22 | <EvanR> | is that some form of pattern eta reduction xD |
| 03:39:15 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
| 03:42:24 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 03:43:28 | <zzz> | Clinton[m]: no, because the left hand side is a pattern match |
| 03:44:41 | <zzz> | and Blah1 is applied to x, not an argument to your function |
| 03:46:34 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Ping timeout: 244 seconds) |
| 03:46:34 | × | Vajb quits (~Vajb@2001:999:504:1841:9e47:1ec7:a52e:1d57) (Read error: Connection reset by peer) |
| 03:47:17 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) |
| 03:47:26 | <zzz> | if you had `f (Blah1 x) = g x` you can't reduce it to `f Blah1 = g` |
| 03:52:49 | → | jmorris joins (uid537181@id-537181.uxbridge.irccloud.com) |
| 04:00:17 | → | DDR joins (~DDR@2604:3d08:4c7f:8250:e38c:e536:e3ca:1a0f) |
| 04:02:47 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a5-27.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 04:06:43 | <ski> | f . Blah1 = g -- unfortunately pseudo-Haskell |
| 04:06:44 | → | nate1 joins (~nate@98.45.169.16) |
| 04:07:01 | → | mbuf joins (~Shakthi@49.204.112.116) |
| 04:07:15 | → | Buliarous joins (~gypsydang@46.232.210.139) |
| 04:08:03 | <ski> | actually, i've wanted a `case' branch (e.g.) `Just -> Just' (or maybe just `Just', "punning") .. |
| 04:08:33 | → | Vajb joins (~Vajb@2001:999:504:1841:9e47:1ec7:a52e:1d57) |
| 04:09:18 | <ski> | (.. there would be a slight difference of meaning, corresponding to not eta-expanding the resulting (alternative) continuation) |
| 04:10:35 | <ski> | Clinton[m] : if you define a `caseFoo' (or `foldFoo'/`cataFoo'), you could say `caseFoo f g' |
| 04:11:22 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 244 seconds) |
| 04:11:59 | × | inversed quits (~inversed@90.209.137.56) (Ping timeout: 265 seconds) |
| 04:12:03 | <ski> | @src bool |
| 04:12:04 | <lambdabot> | bool f _ False = f |
| 04:12:04 | <lambdabot> | bool _ t True = t |
| 04:12:10 | <ski> | @pl \b t e -> if b then t else e |
| 04:12:10 | <lambdabot> | if' |
| 04:12:14 | <ski> | @src maybe |
| 04:12:15 | <lambdabot> | maybe n _ Nothing = n |
| 04:12:15 | <lambdabot> | maybe _ f (Just x) = f x |
| 04:12:19 | <ski> | @src either |
| 04:12:20 | <lambdabot> | either f _ (Left x) = f x |
| 04:12:20 | <lambdabot> | either _ g (Right y) = g y |
| 04:12:24 | <c_wraith> | catamorphisms everywhere! |
| 04:12:25 | <ski> | @src foldr |
| 04:12:26 | <lambdabot> | foldr f z [] = z |
| 04:12:26 | <lambdabot> | foldr f z (x:xs) = f x (foldr f z xs) |
| 04:12:58 | <EvanR> | the catamorphening |
| 04:13:39 | <ski> | @hoogle r -> (a -> [a] -> r) -> [a] -> r |
| 04:13:41 | <lambdabot> | Data.List.Extra list :: b -> (a -> [a] -> b) -> [a] -> b |
| 04:13:41 | <lambdabot> | Extra list :: b -> (a -> [a] -> b) -> [a] -> b |
| 04:13:41 | <lambdabot> | Data.List.HT switchL :: b -> (a -> [a] -> b) -> [a] -> b |
| 04:14:28 | × | leungbk quits (~user@2603-8000-1201-2dd2-4bcb-8ea7-10ea-7a7c.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 04:15:01 | <ski> | @hoogle (rho -> Bool) -> (rho -> a) -> (rho -> a) -> (rho -> a) |
| 04:15:03 | <lambdabot> | Control.Conditional select :: ToBool bool => (a -> bool) -> (a -> b) -> (a -> b) -> (a -> b) |
| 04:15:32 | <ski> | (i've seen that called `cond') |
| 04:16:47 | <EvanR> | is `list' just foldr |
| 04:16:52 | <ski> | no |
| 04:16:58 | <ski> | it's `caseList' |
| 04:17:08 | EvanR | thonks |
| 04:17:43 | <EvanR> | ok so it's not recursive |
| 04:18:10 | <EvanR> | in of itself |
| 04:18:23 | <ski> | Church encoding vs. Scott encoding |
| 04:19:02 | <ski> | (there's also `r -> (a -> [a] -> r -> r) -> ([a] -> r)', which is primitive recursion) |
| 04:19:48 | <EvanR> | :t foldr |
| 04:19:50 | <lambdabot> | Foldable t => (a -> b -> b) -> b -> t a -> b |
| 04:19:57 | → | inversed joins (~inversed@90.209.137.56) |
| 04:20:40 | × | lambdap237 quits (~lambdap@static.167.190.119.168.clients.your-server.de) (Quit: lambdap237) |
| 04:21:15 | → | lambdap237 joins (~lambdap@static.167.190.119.168.clients.your-server.de) |
| 04:22:54 | × | dsrt^ quits (~dsrt@c-76-17-6-165.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 04:23:08 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Remote host closed the connection) |
| 04:25:14 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection) |
| 04:25:48 | <ski> | @quote sound.of |
| 04:25:49 | <lambdabot> | kfish says: a quiet pond / a frog jumps in / the sound of type inference |
| 04:26:42 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 258 seconds) |
| 04:27:08 | <ski> | @quote snow.falls |
| 04:27:08 | <lambdabot> | shapr says: < shapr> the snow falls slowly / the lambdas are lifting - / weak head normal form. |
| 04:34:12 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 04:35:00 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 04:36:59 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 04:41:05 | → | nate1 joins (~nate@98.45.169.16) |
| 04:41:28 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 04:41:31 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 04:43:33 | <ski> | @quote circular.list |
| 04:43:33 | <lambdabot> | gwern says: there are no beginnings or ends to the circular list; but a cons cell thunked in Amador... |
| 04:44:31 | → | titibandit joins (~titibandi@xdsl-89-0-65-2.nc.de) |
| 04:45:37 | <ski> | @quote deep.thought |
| 04:45:37 | <lambdabot> | ski says: <ski> How does a Haskeller in deep thought sound? <ski> *thunk* *thunk* *thunk* |
| 04:45:55 | × | Franciman quits (~Franciman@mx1.fracta.dev) (Read error: Connection reset by peer) |
| 04:45:59 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 244 seconds) |
| 04:46:09 | → | biberu joins (~biberu@user/biberu) |
| 04:49:08 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 04:49:09 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 04:49:09 | → | wroathe joins (~wroathe@user/wroathe) |
| 04:55:17 | × | talismanick quits (~talismani@2601:200:c100:c9e0::1b0b) (Ping timeout: 244 seconds) |
| 04:56:50 | × | mvk quits (~mvk@2607:fea8:5ce3:8500::a80f) (Ping timeout: 244 seconds) |
| 05:00:09 | → | Franciman joins (~Franciman@mx1.fracta.dev) |
| 05:02:00 | × | rekahsoft quits (~rekahsoft@142.189.68.220) (Ping timeout: 244 seconds) |
| 05:03:45 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 05:09:59 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: Exeunt juan@acm.org) |
| 05:10:45 | → | yvan-sraka joins (~yvan-srak@46.183.103.8) |
| 05:11:59 | → | yuzhao joins (~yuzhao@36.112.45.72) |
| 05:13:36 | × | yuzhao_ quits (~yuzhao@36.112.45.72) (Ping timeout: 260 seconds) |
| 05:13:50 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 05:15:24 | × | titibandit quits (~titibandi@xdsl-89-0-65-2.nc.de) (Quit: Leaving.) |
| 05:19:55 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 246 seconds) |
| 05:25:44 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
| 05:29:34 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 05:31:00 | → | jonathanx_ joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
| 05:31:41 | × | freeside quits (~mengwong@103.252.202.193) (Ping timeout: 260 seconds) |
| 05:31:54 | → | wroathe joins (~wroathe@206-55-188-8.fttp.usinternet.com) |
| 05:31:54 | × | wroathe quits (~wroathe@206-55-188-8.fttp.usinternet.com) (Changing host) |
| 05:31:54 | → | wroathe joins (~wroathe@user/wroathe) |
| 05:32:26 | × | argento quits (~argent0@191.81.194.124) (Remote host closed the connection) |
| 05:32:49 | → | chomwitt joins (~chomwitt@2a02:587:dc0c:c200:9e04:2be9:6643:df78) |
| 05:32:52 | × | extratail quits (~archie@2804:214:82be:8ae9:99a:eac4:866e:815c) (Ping timeout: 246 seconds) |
| 05:33:24 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 05:33:27 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 05:34:30 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 05:34:33 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 244 seconds) |
| 05:35:55 | → | rockystone joins (~rocky@user/rockymarine) |
| 05:38:39 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:39:46 | → | califax joins (~califax@user/califx) |
| 05:43:14 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection) |
| 05:45:46 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 05:47:59 | × | DDR quits (~DDR@2604:3d08:4c7f:8250:e38c:e536:e3ca:1a0f) (Ping timeout: 244 seconds) |
| 05:52:18 | → | titibandit joins (~titibandi@xdsl-89-0-65-2.nc.de) |
| 05:53:43 | × | yvan-sraka quits (~yvan-srak@46.183.103.8) (Remote host closed the connection) |
| 05:55:13 | → | tcard joins (~tcard@2400:4051:5801:7500:19ce:ed82:2ab7:90f9) |
| 05:55:37 | × | tcard_ quits (~tcard@2400:4051:5801:7500:19ce:ed82:2ab7:90f9) (Ping timeout: 246 seconds) |
| 05:57:23 | × | tcard quits (~tcard@2400:4051:5801:7500:19ce:ed82:2ab7:90f9) (Read error: Connection reset by peer) |
| 05:57:37 | → | tcard joins (~tcard@2400:4051:5801:7500:19ce:ed82:2ab7:90f9) |
| 05:59:41 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:00:21 | × | jao quits (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 268 seconds) |
| 06:00:40 | → | nate1 joins (~nate@98.45.169.16) |
| 06:01:51 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 06:02:37 | × | jmorris quits (uid537181@id-537181.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 06:03:41 | × | califax quits (~califax@user/califx) (Ping timeout: 258 seconds) |
| 06:04:34 | × | tcard quits (~tcard@2400:4051:5801:7500:19ce:ed82:2ab7:90f9) (Read error: Connection reset by peer) |
| 06:04:40 | → | tcard_ joins (~tcard@2400:4051:5801:7500:19ce:ed82:2ab7:90f9) |
| 06:04:43 | → | califax joins (~califax@user/califx) |
| 06:05:33 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 244 seconds) |
| 06:09:37 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 06:10:43 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 244 seconds) |
| 06:11:34 | → | skrider joins (~skrider@2607:f140:6000:29:3621:a5cd:d0ee:a46) |
| 06:12:19 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 248 seconds) |
| 06:13:13 | × | skrider quits (~skrider@2607:f140:6000:29:3621:a5cd:d0ee:a46) (Client Quit) |
| 06:13:54 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:17:48 | × | jargon quits (~jargon@184.101.208.112) (Remote host closed the connection) |
| 06:20:15 | × | andreabedini quits (~andreabed@8s8kj681vht2qj3xkwc5.ip6.superloop.com) (Quit: WeeChat 3.6) |
| 06:29:30 | → | gurkenglas joins (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
| 06:30:38 | × | titibandit quits (~titibandi@xdsl-89-0-65-2.nc.de) (Remote host closed the connection) |
| 06:30:56 | → | rockystone joins (~rocky@user/rockymarine) |
| 06:31:11 | → | kenran joins (~user@user/kenran) |
| 06:32:56 | × | thegeekinside quits (~thegeekin@189.180.118.117) (Ping timeout: 244 seconds) |
| 06:34:06 | <sm> | I like these haskell haikus ! |
| 06:36:05 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 06:39:23 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 06:40:34 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 06:40:57 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:41:48 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 06:42:59 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 06:44:04 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 06:46:05 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 06:47:40 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 06:48:35 | × | jonathanx_ quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 248 seconds) |
| 06:49:23 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 06:50:29 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 06:51:00 | → | acidjnk joins (~acidjnk@p200300d6e7137a344db4216ce866c9cc.dip0.t-ipconnect.de) |
| 06:51:11 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 06:51:29 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 06:51:59 | → | zeenk joins (~zeenk@2a02:2f04:a20a:3e00:5712:52b0:ca1d:bc63) |
| 06:52:36 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 264 seconds) |
| 06:52:52 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 06:53:08 | → | rockystone joins (~rocky@user/rockymarine) |
| 06:54:17 | → | mncheck joins (~mncheck@193.224.205.254) |
| 06:54:41 | → | yvan-sraka joins (~yvan-srak@46.183.103.17) |
| 06:57:25 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 06:57:54 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 06:58:01 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:4408:559f:5dea:dc65) |
| 06:59:42 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 06:59:52 | → | jonathanx joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 07:03:46 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 07:04:03 | × | mbuf quits (~Shakthi@49.204.112.116) (Quit: Leaving) |
| 07:04:03 | → | kuribas joins (~user@silversquare.silversquare.eu) |
| 07:05:18 | → | MajorBiscuit joins (~MajorBisc@c-001-009-031.client.tudelft.eduvpn.nl) |
| 07:06:08 | → | darkstardev13 joins (~darkstard@50.126.124.156) |
| 07:06:18 | × | natechan quits (~nate@98.45.169.16) (Ping timeout: 268 seconds) |
| 07:07:36 | × | rosalind quits (rosalind@id-194105.uxbridge.irccloud.com) (Quit: Updating details, brb) |
| 07:07:42 | → | n8chan joins (~nate@98.45.169.16) |
| 07:07:46 | → | rosalind joins (rosalind@id-194105.uxbridge.irccloud.com) |
| 07:08:16 | × | darkstardev13 quits (~darkstard@50.126.124.156) (Max SendQ exceeded) |
| 07:08:48 | × | gurkenglas quits (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 07:08:57 | × | Ristovski quits (~Ristovski@hellomouse/perf/ristovski) (Ping timeout: 250 seconds) |
| 07:09:43 | → | briandaed joins (~briandaed@185.234.210.211.r.toneticgroup.pl) |
| 07:11:55 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 07:14:24 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:16:40 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 07:20:17 | → | Ristovski joins (~Ristovski@hellomouse/perf/ristovski) |
| 07:21:00 | <tomsmeding> | delightful quotes! |
| 07:21:09 | → | darkstardevx joins (~darkstard@50.126.124.156) |
| 07:23:21 | × | darkstardevx quits (~darkstard@50.126.124.156) (Remote host closed the connection) |
| 07:23:29 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 07:23:46 | → | darkstardevx joins (~darkstard@50.126.124.156) |
| 07:32:37 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 07:38:46 | → | thyriaen joins (~thyriaen@2a01:aea0:dd4:463c:6245:cbff:fe9f:48b1) |
| 07:45:16 | × | ph88 quits (~ph88@2a02:8109:9e00:71d0:7166:ab0e:b806:c76c) (Ping timeout: 260 seconds) |
| 07:46:49 | × | jonathanx quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 244 seconds) |
| 07:47:45 | → | Typedfern joins (~Typedfern@221.red-83-37-36.dynamicip.rima-tde.net) |
| 07:48:14 | → | CiaoSen joins (~Jura@p200300c95700eb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 07:50:11 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 07:53:54 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 07:55:00 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 264 seconds) |
| 08:00:34 | → | frost joins (~frost@user/frost) |
| 08:01:29 | → | nate1 joins (~nate@98.45.169.16) |
| 08:02:18 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 08:04:20 | → | nschoe joins (~q@2a01:e0a:8e:a190:6cde:f540:4aad:1d22) |
| 08:06:24 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 265 seconds) |
| 08:06:52 | → | jonathanx joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 08:13:59 | → | fserucas joins (~fserucas@2001:818:e376:a400:fb92:70c1:dd88:c7d7) |
| 08:17:18 | × | Ristovski quits (~Ristovski@hellomouse/perf/ristovski) (Ping timeout: 244 seconds) |
| 08:19:30 | × | yvan-sraka quits (~yvan-srak@46.183.103.17) (Remote host closed the connection) |
| 08:22:30 | → | chele joins (~chele@user/chele) |
| 08:22:52 | → | yvan-sraka joins (~yvan-srak@46.183.103.17) |
| 08:23:11 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 260 seconds) |
| 08:23:28 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 08:24:27 | × | yvan-sraka quits (~yvan-srak@46.183.103.17) (Remote host closed the connection) |
| 08:27:02 | → | rockystone joins (~rocky@user/rockymarine) |
| 08:27:38 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 244 seconds) |
| 08:29:38 | × | shriekingnoise quits (~shrieking@186.137.167.202) (Quit: Quit) |
| 08:30:28 | → | yvan-sraka joins (~yvan-srak@46.183.103.17) |
| 08:31:33 | → | leungbk joins (~user@cpe-142-129-149-172.socal.res.rr.com) |
| 08:39:27 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 268 seconds) |
| 08:42:37 | × | razetime quits (~quassel@117.193.4.181) (Ping timeout: 244 seconds) |
| 08:43:37 | → | teo joins (~teo@user/teo) |
| 08:44:32 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Remote host closed the connection) |
| 08:44:58 | × | loras quits (~loras@c-73-139-125-125.hsd1.fl.comcast.net) (Ping timeout: 268 seconds) |
| 08:45:04 | × | johnjaye quits (~pi@173.209.64.74) (Ping timeout: 265 seconds) |
| 08:45:24 | × | mcglk quits (~mcglk@131.191.49.120) (Read error: Connection reset by peer) |
| 08:46:42 | → | johnjaye joins (~pi@173.209.64.74) |
| 08:46:45 | <dr_merijn> | lambdabot is full of amazing quotes, it's underused :p |
| 08:46:46 | <dr_merijn> | @quote |
| 08:46:47 | <lambdabot> | Lemmih says: "I don't understand why my code acts weird when I use unsafePerformIO" is not a bug. |
| 08:46:51 | <dr_merijn> | Hah |
| 08:46:53 | <dr_merijn> | I love that one |
| 08:47:55 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 08:48:30 | <spivak> | yeah |
| 08:49:31 | → | __monty__ joins (~toonn@user/toonn) |
| 08:50:20 | → | mcglk joins (~mcglk@131.191.49.120) |
| 08:51:43 | → | rockystone joins (~rocky@user/rockymarine) |
| 08:53:59 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 244 seconds) |
| 08:54:17 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 08:55:14 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-44.cgn.res.adslplus.ch) |
| 08:57:18 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 268 seconds) |
| 08:57:23 | ← | rosalind parts (rosalind@id-194105.uxbridge.irccloud.com) () |
| 08:58:10 | → | razetime joins (~quassel@117.193.4.181) |
| 08:58:52 | × | jonathanx quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Remote host closed the connection) |
| 08:59:04 | → | jonathanx joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 09:00:05 | × | losfair[m] quits (~losfairma@2001:470:69fc:105::2:7ca3) (Quit: You have been kicked for being idle) |
| 09:01:16 | × | yvan-sraka quits (~yvan-srak@46.183.103.17) (Remote host closed the connection) |
| 09:01:19 | → | gmg joins (~user@user/gehmehgeh) |
| 09:09:36 | → | rockystone joins (~rocky@user/rockymarine) |
| 09:12:25 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 09:14:30 | × | leungbk quits (~user@cpe-142-129-149-172.socal.res.rr.com) (Ping timeout: 268 seconds) |
| 09:19:18 | × | freeside quits (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 244 seconds) |
| 09:23:45 | → | leungbk joins (~user@cpe-142-129-149-172.socal.res.rr.com) |
| 09:25:41 | → | zoelea joins (~zoelea@202.91.42.6) |
| 09:27:58 | ← | zoelea parts (~zoelea@202.91.42.6) () |
| 09:29:40 | × | frost quits (~frost@user/frost) (Quit: Client closed) |
| 09:30:09 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 09:30:20 | <fendor[m]> | Good morning, I am slightly confused about Types, Kinds, etc... I have this code example: https://paste.tomsmeding.com/fVVyfYQg basically I wonder why the declaration `data Set (n :: [k])` leads to the shown error. |
| 09:30:44 | <fendor[m]> | In my understanding, 'k' is a Kind, while 'n' is a type |
| 09:31:25 | <fendor[m]> | I guess, I kind of get why e is inferred to be a kind |
| 09:35:30 | → | freeside joins (~mengwong@bb115-66-48-84.singnet.com.sg) |
| 09:35:50 | × | briandaed quits (~briandaed@185.234.210.211.r.toneticgroup.pl) (Ping timeout: 244 seconds) |
| 09:35:58 | <jackdk> | in Haskell kinds classify types just as types classify values |
| 09:36:03 | <kuribas> | fendor[m]: don't you want Set (n :: [Type])? |
| 09:37:15 | <dr_merijn> | fendor[m]: You want: "data Set (n :: [*])" |
| 09:37:34 | <dr_merijn> | Or, well, "data Set (n :: [Type])" if you're a TypeInType heretic |
| 09:37:35 | <fendor[m]> | * and Type are the same thing, right? |
| 09:37:36 | <kuribas> | Ext takes a value, so it `e` must be a Type. |
| 09:37:36 | <jackdk> | kuribas: fendor[m] probably does, but GHC 9.0.1 and 9.0.2 accept it. I think if `n` is of any other kind it only allows the `Empty` ctor to have a value |
| 09:37:40 | <dr_merijn> | fendor[m]: Yeah |
| 09:37:44 | <fendor[m]> | Or only with the StarIsType Extension? |
| 09:37:50 | <dr_merijn> | fendor[m]: The problem is that k is *any* kind |
| 09:38:01 | <dr_merijn> | fendor[m]: But constructors can only accept arguments that have type * |
| 09:38:35 | <fendor[m]> | What why? I could have a list of [* -> *] right, or am I misunderstanding your point? |
| 09:38:38 | <dr_merijn> | fendor[m]: So "Ext :: e -> Set s -> Set (e ': s)" infers that 'e :: *' (and therefore 'Set :: [*] -> *') |
| 09:39:09 | <dr_merijn> | fendor[m]: Because values always have types with kind * and the first argument to Ext is a value |
| 09:39:46 | <dr_merijn> | Therefore 'e :: *' and 'Set :: [*] -> *' (as opposed to 'Set :: [k] -> *' which your initial version does) |
| 09:39:46 | <kuribas> | fendor[m]: that will be uninhabited. |
| 09:39:58 | <kuribas> | well, only Empty. |
| 09:40:32 | <dr_merijn> | fendor[m]: You could have a list of [* -> *], but "* -> *" can't be the kind of 'e' in Ext's signature |
| 09:41:10 | <dr_merijn> | because 's :: [k]' according to your definition |
| 09:41:33 | <dr_merijn> | and appending 'e :: *' to 's :: [k]' is a kind error |
| 09:41:59 | <fendor[m]> | because * /= k, since k can be more? |
| 09:42:39 | → | madnight joins (~madnight@static.59.103.201.195.clients.your-server.de) |
| 09:42:56 | <fendor[m]> | like, k can be an arbitrary kind? |
| 09:43:09 | <dr_merijn> | fendor[m]: k is "whatever the second argument you use for 'Ext' has" |
| 09:43:57 | <dr_merijn> | Pressumably it'd also work if you change the signature of Ext to "Ext :: e -> Set (s :: [*]) -> Set (e ': s)" |
| 09:44:06 | <dr_merijn> | But at that point, you might as well just change the first line |
| 09:44:58 | <dr_merijn> | Because, theoretically, you could indeed have 's :: [* -> *]' |
| 09:45:02 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 09:45:07 | <dr_merijn> | But then that doesn't typecheck with the prepend of e |
| 09:45:45 | → | yvan-sraka joins (~yvan-srak@46.183.103.8) |
| 09:46:00 | × | ft quits (~ft@p3e9bc57b.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:46:23 | <fendor[m]> | ok, great, then I think I got it, thank you very much! (s :: [*]) doesnt work in combination with the rest of the code (curious type error) but Ill try to debug it with my new knowledge |
| 09:46:37 | <dr_merijn> | fendor[m]: Then you need to rethink Ext |
| 09:46:59 | <dr_merijn> | fendor[m]: Perhaps you meant: "Ext :: proxy e -> Set s -> Set (e' : s)"? |
| 09:47:16 | <dr_merijn> | eh, s/' / '/ |
| 09:47:37 | <fendor[m]> | just to be clear 'data Set (n :: [*]) where' does work, but 'Ext :: e -> Set (s :: [*]) -> Set E : s)' doesn't |
| 09:48:01 | <dr_merijn> | fendor[m]: Your problem is, essentially, that you are promising a value of type 'e' as first argument to Ext, restricting type 'e' to have kind '*' |
| 09:48:25 | <dr_merijn> | Using "proxy e" (or "Proxy e"), frees 'e' from that limiation |
| 09:48:54 | <fendor[m]> | yeah, but I would lose the value in that case |
| 09:49:16 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Ping timeout: 244 seconds) |
| 09:49:51 | <dr_merijn> | Yes, but value and "types other than *" are contradictory |
| 09:49:53 | <dr_merijn> | You gotta pick |
| 09:51:19 | × | spivak quits (uid398348@user/spivak) (K-Lined) |
| 09:51:46 | <fendor[m]> | yeah, the proposal of 'data Set (n :: [*])' works perfectly fine for me, just trying to understand what's going on. |
| 09:51:59 | <fendor[m]> | For reference, that's the code where https://paste.tomsmeding.com/CWKuyhId Set (s :: [*]) doesn't work |
| 09:52:19 | <fendor[m]> | but it works with 'data Set (n :: [*])' |
| 09:52:22 | × | jonathanx quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 244 seconds) |
| 09:52:36 | → | jonathanx joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 09:53:20 | <fendor[m]> | but it feels to me like this is exactly the same issue, just manifests when you actively want to use it. |
| 09:53:55 | <fendor[m]> | since 'Split s ('[] :: * -> *) s' would be a valid kind inference? |
| 09:56:30 | → | michalz joins (~michalz@185.246.207.218) |
| 09:57:00 | <dminuoso> | Is there a cabal variant of runghc where I could just say `cabal run ./foo --build-depends some-lib`? |
| 09:57:29 | <dminuoso> | The closest alternative I can see is to use `cabal repl`, which might sort of work for me, but its cumbersome |
| 09:59:11 | → | mbuf joins (~Shakthi@49.204.135.6) |
| 10:00:42 | <fendor[m]> | cabal script feature is too slow/unpractical? |
| 10:09:56 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 260 seconds) |
| 10:11:18 | × | raym quits (~aritra@user/raym) (Ping timeout: 268 seconds) |
| 10:12:55 | → | mvxkz joins (~mvxkz@119.30.46.32) |
| 10:13:42 | <mvxkz> | About μ and η on a monoid making no sense, since they essentially transform two of an object (same, thus equal) included in their definition into said object (μ) or a specific object included in their definition into itself (η) |
| 10:13:56 | <mvxkz> | Essentially they for example transform the identity functor into the selected object iirc, or two of the selected objects into the selected object |
| 10:14:09 | <mvxkz> | Like this makes sense from a programming PoV, but not mathematical |
| 10:16:40 | → | raym joins (~aritra@user/raym) |
| 10:17:41 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 244 seconds) |
| 10:19:28 | <mvxkz> | anyone? |
| 10:21:04 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 10:25:02 | → | rockystone joins (~rocky@user/rockymarine) |
| 10:33:25 | × | ii8 quits (~ii8@45.63.97.131) (Quit: ii8) |
| 10:34:26 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 260 seconds) |
| 10:35:46 | × | CiaoSen quits (~Jura@p200300c95700eb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 10:35:54 | <lyxia> | What's the context of this question? Who said "μ and η on a monoid make no sense"? |
| 10:36:46 | → | beteigeuze joins (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) |
| 10:39:05 | <byorgey> | mu doesn't "transform two of an object into said object", that's a confusion of levels. It is a *morphism* from M x M -> M. As a Haskell example, if f :: (Int, Int) -> Int, you don't say "f transforms two copies of Int into Int". |
| 10:40:23 | → | rockystone joins (~rocky@user/rockymarine) |
| 10:40:59 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 10:41:13 | <byorgey> | In general, morphisms in a category don't transform one object into another. The objects are more like the *type* of the morphism. |
| 10:43:49 | → | alex` joins (~user@171.red-83-36-41.dynamicip.rima-tde.net) |
| 10:46:06 | × | cfricke quits (~cfricke@user/cfricke) (Ping timeout: 244 seconds) |
| 10:49:10 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 10:49:12 | × | raym quits (~aritra@user/raym) (Ping timeout: 244 seconds) |
| 10:49:51 | <dminuoso> | mvxkz: Also what do you mean by "same, thus equal"? |
| 10:51:35 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 10:54:02 | <dminuoso> | mvxkz: Let me give you a different, more programmer friendly perspective on what this is about: https://gist.github.com/dminuoso/d5ab4ba5d8a5142dde9f4d4c736e3ecb |
| 10:55:19 | <dminuoso> | Here `return/pure` takes the role of η, and `join` takes the role of μ |
| 10:55:38 | <dminuoso> | Observe, that these look very similar to the categorical diagrams: |
| 10:55:49 | <dminuoso> | https://ncatlab.org/nlab/show/monoid+in+a+monoidal+category in 2. Definition |
| 10:56:55 | <dminuoso> | This gets more complicated when mapping to Haskell, because we should start defining what categories we have. |
| 10:56:57 | → | CiaoSen joins (~Jura@p200300c95700eb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 10:57:48 | × | shailangsa quits (~shailangs@host86-159-49-5.range86-159.btcentralplus.com) (Remote host closed the connection) |
| 10:58:14 | <dminuoso> | There's Hask, in which objects are types and morphisms are functions between those types. We can even make a monoidal category of Hask, by equipping it with a tensor like (,) or Either (feel free to do that construction and demonstrate that it satisfies the monoidal category diagrams) |
| 10:58:34 | → | xff0x joins (~xff0x@2405:6580:b080:900:3beb:3a95:af78:4788) |
| 10:58:39 | <dminuoso> | But we have endofunctors, that is functors Hask -> Hask, like IO or Identity |
| 10:58:55 | <dminuoso> | And we can have a category of suchs endofunctor, where IO is an object itself, or Identity |
| 10:58:58 | × | yvan-sraka quits (~yvan-srak@46.183.103.8) (Remote host closed the connection) |
| 10:59:03 | × | thyriaen quits (~thyriaen@2a01:aea0:dd4:463c:6245:cbff:fe9f:48b1) (Remote host closed the connection) |
| 10:59:05 | <dminuoso> | Morphisms are natural transformations between these endofunctors |
| 10:59:38 | <dminuoso> | Every natural transformation in haskell is representable by `type l ~> r = forall a. l a -> l r` |
| 11:00:01 | <dminuoso> | So if `S` is a functor, and `T` is a functor, then every function `S a -> T a` happens to be a natural transformation from S to T. |
| 11:00:10 | <probie> | s/l r/r a/ |
| 11:00:15 | <dminuoso> | Thanks |
| 11:00:33 | <dminuoso> | This is in fact a free theorem, and in the absence of bottom, holds true as long as its implementation type checks. |
| 11:01:03 | → | raym joins (~aritra@user/raym) |
| 11:01:12 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-44.cgn.res.adslplus.ch) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 11:01:18 | <dminuoso> | Here's some examples of natural transformations in Haskell: |
| 11:01:24 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 11:01:24 | <dminuoso> | :t maybeToList |
| 11:01:26 | <lambdabot> | Maybe a -> [a] |
| 11:01:36 | <dminuoso> | Note that both `Maybe` and `[]` are endofunctors |
| 11:01:57 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 11:02:06 | <dminuoso> | And because of what I said above about `if `S` is a functor, and `T` is a functor, then every function `S a -> T a` happens to be a natural transformation from S to T`, therefore `maybeToList` is a natural transformation |
| 11:02:20 | <dminuoso> | (Note the requirement that S and T be endofunctors here) |
| 11:03:02 | <dminuoso> | We could write such functions, using the type alias `type l ~> r = forall a. l a -> r a` as: |
| 11:03:10 | <dminuoso> | maybeToList :: Maybe ~> [] |
| 11:03:20 | → | Midjak joins (~Midjak@82.66.147.146) |
| 11:03:37 | <dminuoso> | setOfTree :: Tree ~> Set |
| 11:03:43 | <dminuoso> | Oh wait, that is a bad example. |
| 11:03:53 | <dminuoso> | vectorOfTree :: Tree ~> Vector |
| 11:04:01 | <dminuoso> | At any rate |
| 11:04:15 | <dminuoso> | It turns out, that the composition of two endofunctors itself is an endofunctor too. |
| 11:04:24 | <dminuoso> | So (Maybe :.: IO) itself too is an endofunctor. |
| 11:04:48 | <dminuoso> | Or if you compose it with itself, so `Maybe :.: Maybe` too is an endofunctor |
| 11:05:01 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-44.cgn.res.adslplus.ch) |
| 11:05:10 | <dminuoso> | Then observe that: join :: (Maybe :.: Maybe) ~> Maybe |
| 11:07:17 | <mvxkz> | hmm |
| 11:09:19 | <dminuoso> | And similarly: |
| 11:09:32 | <dminuoso> | return :: Identity ~> Maybe (with a bit of squinting) |
| 11:14:42 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 11:15:30 | → | zer0bitz joins (~zer0bitz@2001:2003:f748:2000:8093:1499:1d37:f588) |
| 11:16:06 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
| 11:17:33 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 11:21:33 | × | beteigeuze quits (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) (Quit: beteigeuze) |
| 11:22:01 | × | leungbk quits (~user@cpe-142-129-149-172.socal.res.rr.com) (Remote host closed the connection) |
| 11:22:17 | <zzz> | can you give an example of something thatbis *not* an endofunctor? |
| 11:23:16 | <dminuoso> | Heh this is going to be a funny pun: |
| 11:23:26 | <dminuoso> | https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-Monoid.html#t:Endo |
| 11:24:04 | <int-e> | contra variance |
| 11:25:13 | <int-e> | (you have to break the "functor" part of "endofunctor") |
| 11:25:17 | <dminuoso> | Though to be fair, every function `S a -> T a` for contravariant functor is also a natural transformation. |
| 11:25:37 | → | leungbk joins (~user@2603-8000-1201-2dd2-ed4f-5e28-791d-2486.res6.spectrum.com) |
| 11:25:40 | <dminuoso> | (So the statement holds for contra and covariant functors alike) |
| 11:26:07 | <int-e> | But Endo is invariant, so there's not much to transform. |
| 11:26:29 | <int-e> | The space between "contra" and "variance" was deliberate btw. :P |
| 11:27:04 | × | leungbk quits (~user@2603-8000-1201-2dd2-ed4f-5e28-791d-2486.res6.spectrum.com) (Client Quit) |
| 11:27:18 | <dminuoso> | Ah. :) |
| 11:28:02 | → | leungbk joins (~user@2603-8000-1201-2dd2-ed4f-5e28-791d-2486.res6.spectrum.com) |
| 11:28:15 | <zzz> | none of that was confusing at all |
| 11:29:12 | × | xff0x quits (~xff0x@2405:6580:b080:900:3beb:3a95:af78:4788) (Ping timeout: 264 seconds) |
| 11:29:47 | <dminuoso> | mvxkz: And to finalize the circle, in that category of endofunctors, we can equip it with a tensor too (where in the case of Hask there are (,) or Either to make it a monoidal category), in this category we have two prominent tensors: (:.:) and Day |
| 11:29:51 | × | razetime quits (~quassel@117.193.4.181) (Ping timeout: 260 seconds) |
| 11:30:52 | → | xff0x joins (~xff0x@ai071162.d.east.v6connect.net) |
| 11:31:01 | × | leungbk quits (~user@2603-8000-1201-2dd2-ed4f-5e28-791d-2486.res6.spectrum.com) (Client Quit) |
| 11:31:17 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-44.cgn.res.adslplus.ch) (Quit: Textual IRC Client: www.textualapp.com) |
| 11:32:25 | <dminuoso> | But we choose (:.:). Now, in this setting we have a bunch of endofunctors, which a bunch of morphisms going around. Some of these objects (endofunctors) are monoids (=monads). And it is precisely each such object, that is requipped with two particular morphisms (natural transformations), satisfying the diagrams shown above. |
| 11:32:36 | → | leungbk joins (~user@2603-8000-1201-2dd2-ed4f-5e28-791d-2486.res6.spectrum.com) |
| 11:32:39 | <dminuoso> | (Note I skipped that the monoidal category construnction has some additional laws) |
| 11:40:24 | → | razetime joins (~quassel@117.193.4.181) |
| 11:43:10 | → | extratail joins (~archie@2804:214:82c9:273b:11b:69f9:589e:dd5a) |
| 11:45:50 | → | yvan-sraka joins (~yvan-srak@46.183.103.8) |
| 11:46:09 | × | MajorBiscuit quits (~MajorBisc@c-001-009-031.client.tudelft.eduvpn.nl) (Quit: WeeChat 3.5) |
| 11:47:48 | → | lyle joins (~lyle@104.246.145.85) |
| 11:50:52 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 11:51:14 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 11:53:36 | × | yvan-sraka quits (~yvan-srak@46.183.103.8) (Remote host closed the connection) |
| 11:53:54 | → | yvan-sraka joins (~yvan-srak@37.173.21.3) |
| 11:54:15 | × | lyle quits (~lyle@104.246.145.85) (Ping timeout: 252 seconds) |
| 11:54:17 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 268 seconds) |
| 11:59:42 | × | yvan-sraka quits (~yvan-srak@37.173.21.3) (Remote host closed the connection) |
| 12:00:16 | <mvxkz> | ty for the infos |
| 12:01:28 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 12:02:58 | → | nate1 joins (~nate@98.45.169.16) |
| 12:05:31 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 12:07:36 | × | leungbk quits (~user@2603-8000-1201-2dd2-ed4f-5e28-791d-2486.res6.spectrum.com) (Ping timeout: 264 seconds) |
| 12:07:44 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 244 seconds) |
| 12:09:03 | → | rockystone joins (~rocky@user/rockymarine) |
| 12:15:15 | × | Putonlalla quits (~Putonlall@it-cyan.it.jyu.fi) (Remote host closed the connection) |
| 12:15:32 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 12:16:09 | → | shailangsa joins (~shailangs@host86-182-139-4.range86-182.btcentralplus.com) |
| 12:20:29 | → | Ristovski joins (~Ristovski@hellomouse/perf/ristovski) |
| 12:23:44 | ← | tdmm parts (1c9b9145fc@2604:bf00:561:2000::1c8) () |
| 12:26:07 | → | yvan-sraka joins (~yvan-srak@37.173.21.3) |
| 12:26:14 | × | yvan-sraka quits (~yvan-srak@37.173.21.3) (Remote host closed the connection) |
| 12:27:20 | → | yvan-sraka joins (~yvan-srak@37.173.21.3) |
| 12:30:21 | × | yvan-sraka quits (~yvan-srak@37.173.21.3) (Remote host closed the connection) |
| 12:32:47 | × | mvxkz quits (~mvxkz@119.30.46.32) (Remote host closed the connection) |
| 12:33:55 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 258 seconds) |
| 12:34:46 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 12:43:03 | → | famubu joins (~famubu@14.139.174.50) |
| 12:43:03 | × | famubu quits (~famubu@14.139.174.50) (Changing host) |
| 12:43:03 | → | famubu joins (~famubu@user/famubu) |
| 12:43:57 | <famubu> | Hi. I was trying to install the latest version of pandoc from cabal while still having an older pandoc that I installed from my linux distro's package manager. How can that be done? |
| 12:44:28 | <dr_merijn> | Trivially? :p |
| 12:44:34 | <famubu> | I tried using cabal to make a new project like `cabal init -i` with pandoc as a build dependency. And the build finished all right. But I am still at a loss as to how to use the newer pandoc.. |
| 12:44:43 | <dr_merijn> | famubu: Do you mean the library or the executable? |
| 12:44:49 | <famubu> | executable. |
| 12:45:15 | <famubu> | I didn't know how to do it, so just tried cabal. |
| 12:45:20 | <dr_merijn> | For executables just use "cabal install --install-method=copy pandoc" |
| 12:45:37 | <dr_merijn> | Then the executable should be in ~/.cabal/bin |
| 12:47:08 | <famubu> | dr_merijn: That worked. Thanks! |
| 12:50:43 | → | frost joins (~frost@user/frost) |
| 13:00:52 | × | acidjnk quits (~acidjnk@p200300d6e7137a344db4216ce866c9cc.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 13:02:39 | → | burnsidesLlama joins (~burnsides@client-8-70.eduroam.oxuni.org.uk) |
| 13:03:34 | → | Guest17 joins (~Guest17@217.64.164.1) |
| 13:08:09 | → | Tuplanolla joins (~Tuplanoll@91-159-69-34.elisa-laajakaista.fi) |
| 13:10:26 | × | razetime quits (~quassel@117.193.4.181) (Remote host closed the connection) |
| 13:10:27 | → | thegeekinside joins (~thegeekin@189.180.118.117) |
| 13:12:02 | <Guest17> | Is there an example somewhere how to convert the encoding of a lens from either the Profunctor- or vanLaarhoven-encoding to the existential encoding? |
| 13:12:16 | <dminuoso> | Guest17: Yes, look at `optics` it has transformations in both directions |
| 13:12:44 | <dminuoso> | https://hackage.haskell.org/package/optics-0.4.2/docs/Optics-Lens.html#v:lensVL |
| 13:12:46 | <dminuoso> | https://hackage.haskell.org/package/optics-0.4.2/docs/Optics-Lens.html#v:toLensVL |
| 13:12:48 | <dminuoso> | For instance |
| 13:12:55 | <dminuoso> | Each optics type has its own variants, whenever applicable. |
| 13:13:00 | <dminuoso> | In its respective module |
| 13:13:08 | × | burnsidesLlama quits (~burnsides@client-8-70.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 13:14:34 | <Guest17> | Doesn't that convert between the VL and Profunctor encoding? |
| 13:14:48 | <dminuoso> | Ah I misread the question, pardon me. |
| 13:15:04 | <dminuoso> | There was a linebreak right after vanLaarhoven-encoding. |
| 13:18:31 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 244 seconds) |
| 13:20:08 | → | acidjnk joins (~acidjnk@p200300d6e7137a344db4216ce866c9cc.dip0.t-ipconnect.de) |
| 13:21:20 | → | tgi joins (~thegeekin@189.180.54.50) |
| 13:22:26 | × | thegeekinside quits (~thegeekin@189.180.118.117) (Ping timeout: 260 seconds) |
| 13:22:44 | <Guest17> | I have found a conversion from the existential encoding to VL, but I need a to the existential encoding, not from it. |
| 13:22:46 | <Guest17> | https://hackage.haskell.org/package/generic-lens-2.2.1.0/docs/src/Data.Generics.Internal.VL.Lens.html#lens2lensvl |
| 13:23:11 | × | frost quits (~frost@user/frost) (Quit: Client closed) |
| 13:23:16 | <Guest17> | I need a conversion to the existential encoding* |
| 13:25:00 | → | jero98772 joins (~jero98772@2800:484:1d80:d8ce:3490:26c5:1782:da8c) |
| 13:28:29 | × | dolio quits (~dolio@130.44.130.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 13:30:25 | → | dolio joins (~dolio@130.44.130.54) |
| 13:31:35 | → | rockystone joins (~rocky@user/rockymarine) |
| 13:33:24 | × | dolio quits (~dolio@130.44.130.54) (Client Quit) |
| 13:33:31 | × | famubu quits (~famubu@user/famubu) (Ping timeout: 268 seconds) |
| 13:34:13 | × | jero98772 quits (~jero98772@2800:484:1d80:d8ce:3490:26c5:1782:da8c) (Ping timeout: 268 seconds) |
| 13:34:37 | → | dolio joins (~dolio@130.44.130.54) |
| 13:34:57 | → | alecs joins (~alecs@bo-18-159-115.service.infuturo.it) |
| 13:37:00 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 265 seconds) |
| 13:42:20 | → | Surobaki joins (~surobaki@user/surobaki) |
| 13:45:50 | × | Surobaki quits (~surobaki@user/surobaki) (Remote host closed the connection) |
| 13:46:02 | → | Surobaki joins (~surobaki@137.44.222.70) |
| 13:47:16 | → | jero98772 joins (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) |
| 13:47:25 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 13:47:55 | × | kuribas quits (~user@silversquare.silversquare.eu) (Ping timeout: 252 seconds) |
| 13:48:06 | <Surobaki> | Hi, I´m learning about the type system and I´m trying to understand why this doesn´t work: foo :: (a, a); foo = (True, False) |
| 13:48:15 | <Surobaki> | Any help would be great, thanks! |
| 13:48:19 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 13:48:36 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 13:49:18 | → | rockystone joins (~rocky@user/rockymarine) |
| 13:49:26 | <Surobaki> | In other words, why can´t I instantiate a type variable tuple with actual objects of the same type |
| 13:49:32 | → | wroathe joins (~wroathe@user/wroathe) |
| 13:50:26 | <Guest17> | does it work if you change the signature to foo :: (Bool, Bool)? |
| 13:51:46 | <Guest17> | because True and False are values of type Bool. The type variables cannot vary. They are fixed to Bool. |
| 13:51:46 | × | ubert quits (~Thunderbi@77.119.164.69.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 13:51:59 | <lortabac> | Surobaki: 'a' does not mean "any type", it means "all the types" |
| 13:52:05 | → | ubert joins (~Thunderbi@77.119.164.69.wireless.dyn.drei.com) |
| 13:52:37 | × | eggplantade quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 244 seconds) |
| 13:52:41 | <lortabac> | it means that the function should work whatever 'a' is |
| 13:53:57 | <geekosaur> | more specifically: it says that the consumer of foo gets to specify `a`. you don't get to pick one yourself |
| 13:54:42 | <Surobaki> | Thanks guys! That sheds some light on it |
| 13:56:10 | → | causal joins (~user@2001:470:ea0f:3:329c:23ff:fe3f:1e0e) |
| 13:56:13 | × | Franciman quits (~Franciman@mx1.fracta.dev) (Read error: Connection reset by peer) |
| 13:56:29 | <geekosaur> | (and as such, the only value you can specify is `(undefined, undefined)` since you can't know what `a` the consumer/caller wanted) |
| 13:56:56 | <dr_merijn> | geekosaur[m]: pfft, I can come up with *at least* one more :p |
| 13:57:27 | × | alecs quits (~alecs@bo-18-159-115.service.infuturo.it) (Ping timeout: 252 seconds) |
| 13:57:29 | <geekosaur> | `undefined` presumably? |
| 13:57:37 | <geekosaur> | there is that I guess |
| 13:58:34 | → | jonathanx_ joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 13:58:51 | × | jonathanx quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Read error: Connection reset by peer) |
| 13:59:25 | → | alecs joins (~alecs@bo-18-159-115.service.infuturo.it) |
| 14:01:11 | <dr_merijn> | Technically correct = best kinda correct :p |
| 14:01:48 | → | jonathanx joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 14:02:57 | × | jonathanx_ quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 252 seconds) |
| 14:03:37 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 14:03:38 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 14:03:38 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 14:03:38 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 14:03:38 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 14:03:38 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 14:03:38 | × | califax quits (~califax@user/califx) (Write error: Connection reset by peer) |
| 14:05:01 | × | Surobaki quits (~surobaki@137.44.222.70) (Ping timeout: 244 seconds) |
| 14:05:03 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 14:05:05 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 14:05:13 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 14:05:24 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 14:05:37 | → | califax joins (~califax@user/califx) |
| 14:05:54 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 14:05:57 | → | shriekingnoise joins (~shrieking@186.137.167.202) |
| 14:10:26 | → | MajorBiscuit joins (~MajorBisc@c-001-009-031.client.tudelft.eduvpn.nl) |
| 14:10:31 | × | alecs quits (~alecs@bo-18-159-115.service.infuturo.it) (Ping timeout: 246 seconds) |
| 14:12:00 | → | alecs joins (~alecs@bo-18-159-115.service.infuturo.it) |
| 14:18:27 | → | Franciman joins (~Franciman@mx1.fracta.dev) |
| 14:19:32 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 265 seconds) |
| 14:29:03 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 14:34:11 | → | azimut_ joins (~azimut@gateway/tor-sasl/azimut) |
| 14:34:17 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
| 14:34:56 | → | beteigeuze joins (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) |
| 14:45:24 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 258 seconds) |
| 14:49:28 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 14:51:26 | × | alecs quits (~alecs@bo-18-159-115.service.infuturo.it) (Ping timeout: 265 seconds) |
| 14:52:50 | → | mvk joins (~mvk@2607:fea8:5ce3:8500::a80f) |
| 14:53:03 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 14:53:49 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 14:53:53 | × | Franciman quits (~Franciman@mx1.fracta.dev) (Read error: Connection reset by peer) |
| 14:54:25 | → | razetime joins (~quassel@117.193.4.181) |
| 14:55:57 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 14:58:09 | <johnjaye> | is this output normal when building with cabal? |
| 14:58:12 | × | dr_merijn quits (~dr_merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 265 seconds) |
| 14:58:15 | <johnjaye> | https://dpaste.com/2FMDEEVER |
| 14:58:25 | <johnjaye> | expected might be a better term. i recently installed ghc |
| 14:59:37 | → | zebrag joins (~chris@user/zebrag) |
| 14:59:57 | → | loras joins (~bc@c-73-139-125-125.hsd1.fl.comcast.net) |
| 15:00:00 | <nek0> | johnjaye: seems reasonable |
| 15:00:01 | → | bc_ joins (~bc@c-73-139-125-125.hsd1.fl.comcast.net) |
| 15:00:13 | × | bc_ quits (~bc@c-73-139-125-125.hsd1.fl.comcast.net) (Remote host closed the connection) |
| 15:00:34 | × | jonathanx quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 15:04:00 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 265 seconds) |
| 15:07:05 | → | Feuermagier_ joins (~Feuermagi@213.149.82.60) |
| 15:07:57 | × | Guest17 quits (~Guest17@217.64.164.1) (Ping timeout: 244 seconds) |
| 15:08:47 | × | azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 258 seconds) |
| 15:09:10 | <davean> | johnjaye: yes? What else would you expect? |
| 15:09:15 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 15:09:48 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Ping timeout: 265 seconds) |
| 15:10:34 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 15:11:22 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:4408:559f:5dea:dc65) (Quit: WeeChat 2.8) |
| 15:12:48 | → | vorpuni joins (~pvorp@2001:861:3881:c690:c993:5fdd:bfff:f466) |
| 15:15:08 | → | Guest17 joins (~Guest17@217.64.164.1) |
| 15:15:16 | → | rockystone joins (~rocky@user/rockymarine) |
| 15:16:00 | → | jonathanx joins (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) |
| 15:18:24 | × | CiaoSen quits (~Jura@p200300c95700eb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 15:20:17 | → | Franciman joins (~Franciman@mx1.fracta.dev) |
| 15:22:06 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 15:22:36 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 264 seconds) |
| 15:24:24 | → | dr_merijn joins (~dr_merijn@86-86-29-250.fixed.kpn.net) |
| 15:25:10 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 15:25:26 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 15:27:24 | × | jonathanx quits (~jonathan@h-98-128-168-222.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 15:30:26 | <johnjaye> | i don't know. that's the problem. |
| 15:31:08 | <johnjaye> | ah i guess it built everything. it's compiling the actual thing now |
| 15:31:23 | <johnjaye> | i guess this is a 'first time building on cabal' thing? |
| 15:31:31 | <johnjaye> | i.e. it needs a ton of common packages |
| 15:31:32 | <davean> | Ok, usually people ask questions because there is a reason they think things are not exactly as they expect or there is something specific they're trying to understand. |
| 15:31:49 | <davean> | johnjaye: it said exactly what packages it needed and why - thats what you sent us? |
| 15:32:25 | <johnjaye> | right. so according to your reaction that's normal for building with cabal. |
| 15:32:27 | <davean> | As you said, you just installed GHC, so it'll only have 'base' |
| 15:32:39 | <davean> | Thats litterly its job? |
| 15:33:05 | <davean> | Its doing what you use it for and saying that explicitely |
| 15:35:05 | <davean> | It seems you're having a miss match of expectations but I can't help you if I don't know what you expected |
| 15:38:49 | <johnjaye> | well i could try to speculate on my mental state and why i didn't expect it. but i don't think it would be very useful. |
| 15:39:14 | <johnjaye> | there's a one-to-many relationship in that there's a single way something works, but many ways people can not understand how it works. |
| 15:39:52 | <johnjaye> | for example against me you could show quicklisp and how it does something similar, download a dozen packages just to load something you got from github say |
| 15:40:37 | <davean> | I mean litterly any dependency management tool basicly |
| 15:40:53 | <davean> | Thats its primary job |
| 15:40:54 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 15:41:03 | <davean> | so I guess I don't know why you executed cabal |
| 15:41:15 | <davean> | Maybe this is pointless but I'd like to answer the reason for your question |
| 15:41:26 | → | rockystone joins (~rocky@user/rockymarine) |
| 15:42:39 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 15:43:01 | × | Feuermagier_ quits (~Feuermagi@213.149.82.60) (Ping timeout: 260 seconds) |
| 15:45:15 | × | beteigeuze quits (~Thunderbi@a79-169-109-107.cpe.netcabo.pt) (Ping timeout: 244 seconds) |
| 15:45:21 | × | teo quits (~teo@user/teo) (Ping timeout: 260 seconds) |
| 15:45:27 | → | nate1 joins (~nate@98.45.169.16) |
| 15:45:58 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
| 16:02:04 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Remote host closed the connection) |
| 16:04:41 | × | nschoe quits (~q@2a01:e0a:8e:a190:6cde:f540:4aad:1d22) (Ping timeout: 268 seconds) |
| 16:07:08 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Remote host closed the connection) |
| 16:09:18 | → | shapr joins (~user@68.54.166.125) |
| 16:12:48 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 16:13:15 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 16:13:53 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 16:14:53 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 16:16:41 | × | alex` quits (~user@171.red-83-36-41.dynamicip.rima-tde.net) (Ping timeout: 250 seconds) |
| 16:16:51 | × | MajorBiscuit quits (~MajorBisc@c-001-009-031.client.tudelft.eduvpn.nl) (Ping timeout: 260 seconds) |
| 16:17:32 | → | talismanick joins (~talismani@2601:200:c100:c9e0::1b0b) |
| 16:17:32 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 16:18:45 | → | MajorBiscuit joins (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) |
| 16:19:21 | × | johnjaye quits (~pi@173.209.64.74) (Ping timeout: 252 seconds) |
| 16:20:09 | → | beteigeuze joins (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
| 16:20:42 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 16:22:27 | × | mvk quits (~mvk@2607:fea8:5ce3:8500::a80f) (Ping timeout: 244 seconds) |
| 16:23:22 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 16:27:47 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Ping timeout: 248 seconds) |
| 16:34:11 | × | Franciman quits (~Franciman@mx1.fracta.dev) (Ping timeout: 248 seconds) |
| 16:35:38 | × | MajorBiscuit quits (~MajorBisc@2a02-a461-129d-1-193d-75d8-745d-e91e.fixed6.kpn.net) (Ping timeout: 268 seconds) |
| 16:43:36 | → | econo joins (uid147250@user/econo) |
| 16:45:46 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 258 seconds) |
| 16:46:03 | × | abrantesasf quits (~abrantesa@187.64.158.2) (Read error: Connection reset by peer) |
| 16:48:43 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 246 seconds) |
| 16:49:04 | × | fserucas quits (~fserucas@2001:818:e376:a400:fb92:70c1:dd88:c7d7) (Ping timeout: 246 seconds) |
| 16:51:37 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 16:53:15 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 16:57:16 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 16:58:26 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 17:01:16 | → | thyriaen joins (~thyriaen@2a01:aea0:dd4:463c:6245:cbff:fe9f:48b1) |
| 17:01:52 | <dminuoso> | Guest17: What is the existential encoding by the way? |
| 17:05:36 | → | leungbk joins (~user@cpe-142-129-149-172.socal.res.rr.com) |
| 17:08:51 | → | Henson joins (~kvirc@207.136.101.195) |
| 17:10:02 | <Henson> | it seems as though the convention in Lens is to name lenses with an underscore. I have encountered MANY times when this has been a problem because VSCode thinks it's a type hole and doesn't give me a warning that it's something that is not in scope. Is there an alternative convention for naming lenses that doesn't confuse them with type holes? |
| 17:10:52 | <Guest17> | dminuoso: https://www.tweag.io/blog/2022-05-05-existential-optics/ |
| 17:11:17 | × | leungbk quits (~user@cpe-142-129-149-172.socal.res.rr.com) (Ping timeout: 250 seconds) |
| 17:12:49 | <dminuoso> | Guest17: Ah cool, thjanks. |
| 17:12:56 | → | Topsi joins (~Topsi@dyndsl-095-033-025-008.ewe-ip-backbone.de) |
| 17:13:16 | <dminuoso> | Henson: The convention merely stems from various TH helpers, by default, generating lenses for every field that starts with an underscore. |
| 17:14:08 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 17:14:44 | <geekosaur> | you can use whatever prefix you want as long as you replace `makeLenses` with the appropriate call specifying that prefix |
| 17:14:55 | <geekosaur> | I misremember how you do that right now |
| 17:14:57 | <dminuoso> | Henson: But you can use a custom lensRules with the field _fieldToDef swapped with a suitable function. So you could - in a separate file - write `makeLenses = makeLensesWith (lensRules { _fieldDef = yourFunction })` |
| 17:15:04 | <dminuoso> | And use that instead. |
| 17:15:09 | <geekosaur> | right, that |
| 17:15:46 | <dminuoso> | Henson: It could be some trivial _fieldDef that just selects *every* field. |
| 17:16:15 | <dminuoso> | Or maybe soem `makeLenses pref = ...` such that `makeLenses "foo_"` would generate lenses for every field starting with foo_. |
| 17:16:18 | <dminuoso> | The sky is the limit. |
| 17:16:45 | <dminuoso> | (Note that _fieldDef not just selects, but also renames - so it controls both whether or not a field is used, and also what the generated lens name is) |
| 17:17:26 | <dminuoso> | Henson: Take also note of `lensRulesFor`, `lookingupNamer` and `mappingNamer` |
| 17:17:48 | → | Franciman joins (~Franciman@mx1.fracta.dev) |
| 17:18:53 | → | alecs joins (~alecs@host-62-211-49-5.pool62211.interbusiness.it) |
| 17:21:33 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 17:22:46 | → | jbayardo joins (~jbayardo@20.83.116.49) |
| 17:23:02 | → | thegeekinside joins (~thegeekin@189.180.7.159) |
| 17:24:12 | × | tgi quits (~thegeekin@189.180.54.50) (Ping timeout: 268 seconds) |
| 17:27:04 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Ping timeout: 265 seconds) |
| 17:27:52 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Remote host closed the connection) |
| 17:29:51 | → | gurkenglas joins (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
| 17:30:48 | → | tgi joins (~thegeekin@189.180.7.159) |
| 17:32:12 | × | jbayardo quits (~jbayardo@20.83.116.49) (Ping timeout: 244 seconds) |
| 17:32:50 | × | thegeekinside quits (~thegeekin@189.180.7.159) (Ping timeout: 268 seconds) |
| 17:33:51 | × | raym quits (~aritra@user/raym) (Ping timeout: 260 seconds) |
| 17:36:49 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:39:19 | → | raym joins (~aritra@user/raym) |
| 17:39:26 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 258 seconds) |
| 17:40:17 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 17:40:33 | <Henson> | I just write my Lenses by hand, so I don't need to fit into a TH mould, I'm just trying to stick to a convention, if one exists. |
| 17:41:28 | × | razetime quits (~quassel@117.193.4.181) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 17:41:47 | <dminuoso> | The _ convention is just for when you want TH generated lenses. |
| 17:42:52 | <Henson> | ok |
| 17:44:03 | <geekosaur> | yeh, I wouldn't worry about conventions if you';re not using TH |
| 17:44:45 | <Henson> | ok, thank you for the tips |
| 17:45:04 | × | acidjnk quits (~acidjnk@p200300d6e7137a344db4216ce866c9cc.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 17:48:07 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Quit: Leaving) |
| 17:48:38 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 17:49:44 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 17:52:12 | → | jbayardo joins (~jbayardo@20.83.116.49) |
| 17:52:26 | × | mbuf quits (~Shakthi@49.204.135.6) (Quit: Leaving) |
| 17:53:44 | <Guest17> | I found the conversion function I was looking for |
| 17:53:52 | <Guest17> | it's elens in this post |
| 17:53:54 | <Guest17> | https://www.reddit.com/r/haskell/comments/ujmjx0/comment/i7sayy4/?utm_source=reddit&utm_medium=web2x&context=3 |
| 17:54:37 | × | alecs quits (~alecs@host-62-211-49-5.pool62211.interbusiness.it) (Ping timeout: 265 seconds) |
| 17:56:21 | → | alecs joins (~alecs@151.36.35.186) |
| 17:58:35 | × | Guest17 quits (~Guest17@217.64.164.1) (Quit: Client closed) |
| 17:59:53 | → | acidjnk joins (~acidjnk@p200300d6e7137a811112d37158fd9527.dip0.t-ipconnect.de) |
| 18:00:17 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 18:02:26 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 18:03:32 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 18:09:35 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 18:14:00 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Quit: Leaving) |
| 18:14:36 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 18:15:12 | → | titibandit joins (~titibandi@xdsl-89-0-65-2.nc.de) |
| 18:15:53 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 18:20:38 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Remote host closed the connection) |
| 18:23:03 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 18:23:31 | × | extratail quits (~archie@2804:214:82c9:273b:11b:69f9:589e:dd5a) (Ping timeout: 248 seconds) |
| 18:24:49 | → | AlexNoo_ joins (~AlexNoo@178.34.161.92) |
| 18:24:50 | → | c209e6dc-4d76-47 joins (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) |
| 18:25:34 | <c209e6dc-4d76-47> | I'm trying to build something using cabal on a server over ssh but the home directory has only 4GB quota, I do have another location with more storage, but how do I change the cabal home path from ~/.cabal? |
| 18:26:02 | × | hrberg quits (~quassel@171.79-160-161.customer.lyse.net) (Ping timeout: 265 seconds) |
| 18:27:06 | × | Alex_test quits (~al_test@94.233.240.222) (Ping timeout: 268 seconds) |
| 18:27:06 | × | AlexZenon quits (~alzenon@94.233.240.222) (Ping timeout: 268 seconds) |
| 18:28:41 | × | AlexNoo quits (~AlexNoo@94.233.240.222) (Ping timeout: 260 seconds) |
| 18:29:03 | → | hrberg joins (~quassel@171.79-160-161.customer.lyse.net) |
| 18:29:11 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 18:29:47 | <monochrom> | Yes there is an environment variable for that. Let me find it... |
| 18:30:03 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 18:31:57 | → | AlexZenon joins (~alzenon@178.34.161.92) |
| 18:32:14 | → | Alex_test joins (~al_test@178.34.161.92) |
| 18:32:31 | <monochrom> | CABAL_CONFIG |
| 18:32:56 | <monochrom> | Err no, CABAL_DIR |
| 18:33:43 | AlexNoo_ | is now known as AlexNoo |
| 18:34:08 | <c209e6dc-4d76-47> | I see, thanks |
| 18:34:30 | <c209e6dc-4d76-47> | so I can look into doing cabal clean to remove files from ~/.cabal first or just do rm -rf ~/.cabal safely? |
| 18:35:43 | <c209e6dc-4d76-47> | latter seems to have worked |
| 18:36:11 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 18:39:08 | × | c209e6dc-4d76-47 quits (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) (Quit: Konversation terminated!) |
| 18:39:30 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 18:41:24 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 18:41:29 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 18:42:44 | × | tgi quits (~thegeekin@189.180.7.159) (Remote host closed the connection) |
| 18:45:03 | × | raym quits (~aritra@user/raym) (Ping timeout: 244 seconds) |
| 18:46:12 | → | raym joins (~aritra@user/raym) |
| 18:52:48 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 244 seconds) |
| 18:53:23 | × | raym quits (~aritra@user/raym) (Ping timeout: 248 seconds) |
| 18:54:20 | → | raym joins (~aritra@user/raym) |
| 18:56:50 | → | rockystone joins (~rocky@user/rockymarine) |
| 18:58:00 | → | c209e6dc-4d76-47 joins (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) |
| 19:01:09 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 19:03:31 | × | Natch quits (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Ping timeout: 250 seconds) |
| 19:06:03 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 19:06:45 | → | Natch joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
| 19:09:13 | → | CiaoSen joins (~Jura@p200300c95700eb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 19:12:03 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 19:12:46 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 19:16:51 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Remote host closed the connection) |
| 19:17:34 | → | leungbk joins (~user@cpe-142-129-149-172.socal.res.rr.com) |
| 19:17:45 | → | mvk joins (~mvk@2607:fea8:5ce3:8500::a80f) |
| 19:19:08 | → | ft joins (~ft@p3e9bc57b.dip0.t-ipconnect.de) |
| 19:20:20 | <FlaminWalrus> | Any ideas on how to make this small program more memory efficient? I run it on a ~300Mb text file containing Fortran-formatted floats, and the program just eats 15GB of RAM and spins. Not even sure if it should be more strict or more lazy; tried both to little avail. https://paste.tomsmeding.com/7n9G7jrl |
| 19:23:57 | <tomsmeding> | FlaminWalrus: replacing the `point` list by an Array (or Vector) should already help, but there's probably other things too (deferring to the rest of the crowd here) |
| 19:24:50 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 19:25:20 | <EvanR> | I don't see anything wrong with reading the data in into a TimeSeries (list of (complex) doubles), but I am highly suspicious of sending such a list into an FFT |
| 19:25:48 | <tomsmeding> | (performance may be gained by reading the file as a strict ByteString and parsing the floats using the bytestring-lexing package; `read` on Doubles is veeeery slow) |
| 19:25:58 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 265 seconds) |
| 19:27:24 | <tomsmeding> | EvanR: an array will at least remove _quite_ a couple of pointers from that representation; if you move to a fully unboxed array, you'll have 16 bytes per element instead of the current at least 8(Complex) + 2*(8(Double) + 8(Double#)) + 8(pointer to next cons cell) = 40 bytes |
| 19:27:33 | <EvanR> | yeah there's a constant factor increase in cost reading in a String and using read |
| 19:28:32 | <dolio> | Doing !! repeatedly in a giant list is not going to be good, either. |
| 19:29:00 | <EvanR> | the fft is treating the list as an array, so that's... yeah |
| 19:29:08 | <tomsmeding> | lol yes |
| 19:34:40 | <dolio> | I think the algorithm is O(n²) just from the list element accesses. |
| 19:35:35 | <tomsmeding> | _mosT_ algorithms that are supposed to be subquadratic time and use !! are in fact at least quadratic |
| 19:35:35 | <dminuoso> | I would start by profiling. |
| 19:35:43 | <dminuoso> | So we dont have to guess. |
| 19:36:11 | <tomsmeding> | to be fair, profiling memory usage in haskell is nontrivial, especially for someone who hasn't yet realised that using Array/Vector here instead of (!!) might be a good idea |
| 19:37:44 | <dminuoso> | It's even less trivial to guess based on this non-trivial code. |
| 19:38:00 | <dminuoso> | There could be some lingering lazyness problem solvable by a single bang. |
| 19:38:26 | <tomsmeding> | fair |
| 19:38:28 | <Square> | Is there any agreement on what is best for readability choosing between "let..in" and "where" syntax? I just discovered "where" makes me structure things better. |
| 19:38:32 | <dolio> | No, come on. |
| 19:40:02 | <dminuoso> | Square: If its just a single binding needed for understanding what an expression does, I would use let-in (as it forces the reader to read or skip to get to the relevant expression), otherwise I would prefer where. |
| 19:40:03 | <EvanR> | a single bang which makes fft using lists fast xD |
| 19:40:13 | <EvanR> | that's a bang alright |
| 19:40:15 | → | rockystone joins (~rocky@user/rockymarine) |
| 19:40:21 | <tomsmeding> | EvanR: fast no, using less memory maybe |
| 19:40:43 | <EvanR> | solving the obvious problems first xD |
| 19:40:45 | <monochrom> | The agreement is use what you like. |
| 19:40:58 | <dminuoso> | I mean I see sum after map for example. foldl' is likely a better choice. |
| 19:41:01 | <Square> | dminuoso, sounds like a fair rule. |
| 19:41:08 | <EvanR> | a faster way to convert String to Double is like icing on the cake |
| 19:41:55 | <monochrom> | tomsmeding: I think EvanR was speaking hypothetically to set up a joke/pun. :) |
| 19:41:59 | → | biberu joins (~biberu@user/biberu) |
| 19:42:01 | <dminuoso> | FlaminWalrus: Yeah, each time you do a `sum $ map`, consider foldl' instead. |
| 19:42:05 | → | teo joins (~teo@user/teo) |
| 19:42:16 | → | kenran joins (~user@user/kenran) |
| 19:43:14 | <dminuoso> | (Though I wonder whether perhaps there's a RULES for that) |
| 19:43:31 | <tomsmeding> | isn't that precisely what `build` is for |
| 19:43:40 | <EvanR> | I didn't notice the list being recursive split into smaller and smaller chunks, but if it is, that is a big source of memory um sink of memory |
| 19:43:56 | <dminuoso> | tomsmeding: build is for foldr fusion. |
| 19:44:06 | → | extratail joins (~archie@2804:214:82c9:273b:11b:69f9:589e:dd5a) |
| 19:44:20 | × | Topsi quits (~Topsi@dyndsl-095-033-025-008.ewe-ip-backbone.de) (Ping timeout: 265 seconds) |
| 19:44:35 | <dminuoso> | But that wouldnt apply here |
| 19:44:45 | <tomsmeding> | dminuoso: https://play-haskell.tomsmeding.com/saved/xeYGufTp seems to (press Core) |
| 19:44:48 | × | alecs quits (~alecs@151.36.35.186) (Ping timeout: 264 seconds) |
| 19:44:50 | <dolio> | Make sure you optimize your list functions before you completely stop using lists. |
| 19:44:51 | <dminuoso> | mmm |
| 19:45:09 | <EvanR> | FlaminWalrus, taking subslices of an array is much more efficient than the equivalent operation on lists |
| 19:45:45 | <dminuoso> | tomsmeding: give me a moment to analyze the core here, I always find it difficult to read. |
| 19:45:53 | <EvanR> | not to mention the !! to ! improvement |
| 19:46:23 | <tomsmeding> | dminuoso: I feel you, I was mostly going by `ghc -O -ddump-rule-rewrites a.hs` printing `fold/build` twice |
| 19:46:27 | → | zxrom joins (~zxrom@mm-232-14-212-37.vitebsk.dynamic.pppoe.byfly.by) |
| 19:46:39 | <tomsmeding> | and then checking the core to make sure it wasn't a fluke |
| 19:47:21 | → | pavonia joins (~user@user/siracusa) |
| 19:47:25 | <dminuoso> | tomsmeding: Okay, but this will only work if the list producer actually uses `build`. |
| 19:47:37 | <dminuoso> | Otherwise you should foldl'. |
| 19:47:45 | <tomsmeding> | right, but we're talking about `map` here |
| 19:47:48 | <monochrom> | FFT is better off with an array instead of a list or a bunch of lists. |
| 19:48:08 | <tomsmeding> | monochrom: that's too obvious, we're having fun with the less obvious things |
| 19:48:17 | <monochrom> | OK! |
| 19:48:30 | <dminuoso> | tomsmeding: uh, so? |
| 19:48:32 | <EvanR> | the twist never gets old |
| 19:48:43 | <EvanR> | arrays are actually trees in ram xD |
| 19:49:07 | <EvanR> | why didn't they just use an array of ram |
| 19:49:16 | <dminuoso> | tomsmeding: map does not use build, what's your point? |
| 19:49:26 | <tomsmeding> | dminuoso: that ghc -ddump-rule-rewrites command also prints this https://paste.tomsmeding.com/tWtG5yZ4 |
| 19:49:31 | <tomsmeding> | more RULEs |
| 19:49:50 | <monochrom> | Then let's consider an improvement based on defining your own data-strict spine-nonstrict list type "data L a = N | C !a (L a)" and furthermore your own strict complex number type "data C = !Double :+ !Double" ... |
| 19:49:51 | <dminuoso> | tomsmeding: can you make the module names disappear please? |
| 19:50:06 | <dolio> | map gets rewritten to use build. |
| 19:50:07 | <monochrom> | In fact, let's unbox some of those fields, too... |
| 19:50:17 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 19:50:19 | <dminuoso> | dolio: Oh okay, that's good to know. |
| 19:50:44 | <monochrom> | EvanR: I think the hardware does think in terms of an array of RAM areas. |
| 19:50:44 | <EvanR> | Complex already has strict fields at least |
| 19:51:02 | <tomsmeding> | dminuoso: https://paste.tomsmeding.com/jV3VuWAe better? |
| 19:51:03 | <monochrom> | Oh cool. |
| 19:51:14 | <dminuoso> | Ah yes, thanks :) |
| 19:52:02 | <EvanR> | when I come back tomorrow, I expect to see a fast FFT using lists |
| 19:52:23 | <tomsmeding> | EvanR: written by you |
| 19:52:31 | <EvanR> | I'm not smart enough |
| 19:52:32 | → | alecs joins (~alecs@151.34.71.118) |
| 19:52:54 | <monochrom> | fast FFT? ATM machine? >:) |
| 19:52:57 | → | kenran joins (~user@user/kenran) |
| 19:53:11 | <dminuoso> | So why would there be a rewrite rule rewriting map, when you could just hardwire that implementation in? |
| 19:53:22 | × | Sauvin quits (~colere@about/linux/staff/sauvin) (Quit: Leaving) |
| 19:53:23 | <dminuoso> | Or wait, there's a map/build kind of rule? |
| 19:53:33 | <EvanR> | yes because lists are slow for the operations required, so it cancels one of the Fs out of the FFT to make an FT |
| 19:53:46 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 19:53:47 | <EvanR> | so you need to add fast back in |
| 19:54:00 | <monochrom> | I wonder if one can make FFT fast with FIFOs. |
| 19:54:04 | <dminuoso> | Found it: |
| 19:54:06 | <dminuoso> | "map" [~1] forall f xs. map f xs = build (\c n -> foldr (mapFB c f) n xs) |
| 19:54:11 | <dolio> | Because if it doesn't fuse, you want to rewrite it back to the recursive implementation, which is better. |
| 19:54:19 | <tomsmeding> | dminuoso: presumably yes; I think all the build stuff is just in rules |
| 19:54:29 | → | kenran joins (~user@user/kenran) |
| 19:54:37 | <dminuoso> | tomsmeding: and no, its not. |
| 19:55:32 | <dminuoso> | Oh also nice to know there is a RULES `map coerce = coerce` |
| 19:55:44 | <tomsmeding> | TIL I love it |
| 19:56:12 | <monochrom> | They really have thought of everything. :) |
| 19:56:13 | <dolio> | sum for lists is also defined using foldl', from what I can see. |
| 19:57:16 | <tomsmeding> | dolio: only since base-4.16, before that it was, well, https://hackage.haskell.org/package/base-4.15.1.0/docs/src/GHC.List.html#sum |
| 19:57:30 | <tomsmeding> | slightly embarassing |
| 19:57:43 | <tomsmeding> | s/r/rr/ |
| 19:58:02 | <dminuoso> | Thats 9.0.2 |
| 19:58:04 | <EvanR> | i was told for years that foldl would be automagically optimized |
| 19:58:14 | <dminuoso> | So only since 9.2.1 heh |
| 19:58:15 | <tomsmeding> | I mean, probably, but still |
| 19:58:51 | → | Colere joins (~colere@about/linux/staff/sauvin) |
| 19:58:59 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 268 seconds) |
| 19:59:01 | <EvanR> | I guess the '-crowd won xD |
| 19:59:18 | <monochrom> | Well I was told for years that 2010 was when we could send astronauts to Jupiter, too. |
| 19:59:33 | <dolio> | It's not really that embarassing, because for lots of cases, GHC doesn't need you to write foldl', I think. |
| 19:59:48 | <dolio> | When you're operating on a concrete type, like in this case. |
| 20:00:24 | <dminuoso> | Why is that not embarrassing in that case? |
| 20:00:43 | <dolio> | Because it's already doing what you want. |
| 20:00:58 | <EvanR> | I'd agree if the slow code made into something that mattered for some amount of time, would be embarrassing |
| 20:01:07 | <dminuoso> | Naively I would have thought foldl would cost me thunk allocations |
| 20:01:22 | → | ph88 joins (~ph88@2a02:8109:9e00:71d0:5ba:5f3b:8b59:3371) |
| 20:02:04 | <dminuoso> | `foldl' (+) 0 [1..100000000]` will compute, but `foldl (+) 0 [1..100000000]` will stackoverflow for me |
| 20:02:42 | <dminuoso> | dolio: this seems to not do what I want. |
| 20:02:47 | <EvanR> | in ghci? |
| 20:03:02 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 20:03:14 | <tomsmeding> | works fine with ghc -O |
| 20:03:28 | <EvanR> | that you get different results in general in ghci is a larger issue |
| 20:03:39 | <dminuoso> | Mmm |
| 20:03:46 | <tomsmeding> | nah ghci just doesn't do any optimisations, and strictness analysis is a nontrivial optimisation |
| 20:04:16 | <dminuoso> | But honestly, if you *rely* on a particular RULES to fire, or an optimization to kick in, you should really consider writing it optimized yourself. |
| 20:04:29 | <EvanR> | optimizations make working things work better... if it means broken or not broken we need a different word xD |
| 20:04:44 | <dminuoso> | Unless you use something like inspection-testing |
| 20:05:20 | <EvanR> | which is why TCO is annoying |
| 20:06:05 | <EvanR> | TCNB (tail calls not broken) |
| 20:07:23 | <FlaminWalrus> | Thanks for the suggestions; this is my first Haskell program outside one or two Advent of Code problems a year or so ago. The obvious isn't obvious to me quite yet ☺ |
| 20:07:58 | <tomsmeding> | FlaminWalrus: please forgive us all for our use of language :) |
| 20:08:39 | → | rockystone joins (~rocky@user/rockymarine) |
| 20:08:54 | <FlaminWalrus> | It's all good, I've got enough math and computational physics background to guess what it all means |
| 20:11:50 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 20:12:10 | → | burnsidesLlama joins (~burnsides@client-8-86.eduroam.oxuni.org.uk) |
| 20:13:35 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 20:13:51 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 20:14:29 | × | loras quits (~bc@c-73-139-125-125.hsd1.fl.comcast.net) (Quit: Leaving) |
| 20:15:31 | × | vorpuni quits (~pvorp@2001:861:3881:c690:c993:5fdd:bfff:f466) (Ping timeout: 248 seconds) |
| 20:16:12 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:17:22 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) |
| 20:18:17 | → | codaraxis__ joins (~codaraxis@user/codaraxis) |
| 20:18:34 | × | burnsidesLlama quits (~burnsides@client-8-86.eduroam.oxuni.org.uk) (Ping timeout: 244 seconds) |
| 20:21:40 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:9960:b0f8:561f:a74b) (Ping timeout: 244 seconds) |
| 20:21:48 | × | teo quits (~teo@user/teo) (Ping timeout: 268 seconds) |
| 20:22:02 | × | codaraxis___ quits (~codaraxis@user/codaraxis) (Ping timeout: 265 seconds) |
| 20:24:08 | → | jonathanx joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
| 20:25:25 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
| 20:26:32 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 20:31:29 | × | jonathanx quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 244 seconds) |
| 20:34:14 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 258 seconds) |
| 20:46:20 | → | nate1 joins (~nate@98.45.169.16) |
| 20:48:29 | → | teo joins (~teo@user/teo) |
| 20:49:56 | → | vorpuni joins (~pvorp@2001:861:3881:c690:6a24:2212:7415:f659) |
| 20:50:48 | × | CiaoSen quits (~Jura@p200300c95700eb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 20:51:21 | × | nate1 quits (~nate@98.45.169.16) (Ping timeout: 268 seconds) |
| 20:54:10 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 20:54:10 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 20:54:13 | allbery_b | is now known as geekosaur |
| 21:01:48 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 21:02:00 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Remote host closed the connection) |
| 21:02:11 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 21:07:23 | × | zer0bitz quits (~zer0bitz@2001:2003:f748:2000:8093:1499:1d37:f588) (Ping timeout: 268 seconds) |
| 21:09:53 | × | leungbk quits (~user@cpe-142-129-149-172.socal.res.rr.com) (Ping timeout: 265 seconds) |
| 21:10:11 | <monochrom> | Oh! ghcup is now recommending GHC 9.2.4. |
| 21:10:19 | <monochrom> | "This recompiles everything." |
| 21:11:05 | × | teo quits (~teo@user/teo) (Ping timeout: 268 seconds) |
| 21:13:04 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 21:16:26 | <drlkf> | does anyone have an idea how to make a json parser similar to the (.:) operator, but with array nth ? |
| 21:18:12 | → | biberu joins (~biberu@user/biberu) |
| 21:20:25 | × | phma quits (~phma@2001:5b0:210f:49a8:1266:723e:2abd:17a6) (Read error: Connection reset by peer) |
| 21:20:52 | → | phma joins (~phma@host-67-44-208-113.hnremote.net) |
| 21:23:00 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 21:29:06 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 21:29:07 | × | zeenk quits (~zeenk@2a02:2f04:a20a:3e00:5712:52b0:ca1d:bc63) (Quit: Konversation terminated!) |
| 21:31:56 | → | libertyprime joins (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) |
| 21:36:55 | × | Henson quits (~kvirc@207.136.101.195) (Ping timeout: 250 seconds) |
| 21:39:27 | × | ubert quits (~Thunderbi@77.119.164.69.wireless.dyn.drei.com) (Ping timeout: 252 seconds) |
| 21:42:52 | × | c209e6dc-4d76-47 quits (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) (Quit: Konversation terminated!) |
| 21:51:44 | × | michalz quits (~michalz@185.246.207.218) (Remote host closed the connection) |
| 21:52:01 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 21:55:37 | × | jinsun quits (~jinsun@user/jinsun) (Read error: Connection reset by peer) |
| 21:56:00 | → | jinsun joins (~jinsun@user/jinsun) |
| 21:59:09 | → | ubert joins (~Thunderbi@77.119.214.60.wireless.dyn.drei.com) |
| 21:59:51 | × | mncheck quits (~mncheck@193.224.205.254) (Ping timeout: 260 seconds) |
| 22:02:04 | → | yvan-sraka joins (~yvan-srak@2a01:c22:ac1f:9c00:1306:3abb:2386:5c1b) |
| 22:05:09 | <Axman6> | EvanR: fast FFT using lists: https://hackage.haskell.org/package/pure-fft-0.2.0/docs/Numeric-FFT.html |
| 22:05:33 | <Axman6> | well, FFT using lists anyway, no idea if it's fast |
| 22:07:02 | <hpc> | fast just means what algorithm it is |
| 22:07:13 | <hpc> | like quicksort |
| 22:07:35 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 244 seconds) |
| 22:08:41 | → | leungbk joins (~user@cpe-142-129-149-172.socal.res.rr.com) |
| 22:11:31 | × | ph88 quits (~ph88@2a02:8109:9e00:71d0:5ba:5f3b:8b59:3371) (Ping timeout: 260 seconds) |
| 22:12:16 | × | infinity0 quits (~infinity0@185.112.146.113) (Remote host closed the connection) |
| 22:15:29 | → | infinity0 joins (~infinity0@185.112.146.113) |
| 22:16:05 | → | rockystone joins (~rocky@user/rockymarine) |
| 22:16:37 | × | titibandit quits (~titibandi@xdsl-89-0-65-2.nc.de) (Remote host closed the connection) |
| 22:17:09 | × | infinity0 quits (~infinity0@185.112.146.113) (Remote host closed the connection) |
| 22:18:18 | × | yvan-sraka quits (~yvan-srak@2a01:c22:ac1f:9c00:1306:3abb:2386:5c1b) (Remote host closed the connection) |
| 22:18:32 | × | vorpuni quits (~pvorp@2001:861:3881:c690:6a24:2212:7415:f659) (Remote host closed the connection) |
| 22:19:03 | → | infinity0 joins (~infinity0@185.112.146.113) |
| 22:19:52 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 22:22:30 | → | yvan-sraka joins (~yvan-srak@2a01:c22:ac1f:9c00:1306:3abb:2386:5c1b) |
| 22:23:34 | <janus> | drlkf: could you post an example of the output with a sample of expected input, and their types |
| 22:24:38 | <janus> | drlkf: you can make a function that takes an aeson Parser of a list and extracts the n'th value, i think |
| 22:24:55 | <janus> | drlkf: should be a one-liner |
| 22:26:06 | × | alecs quits (~alecs@151.34.71.118) (Ping timeout: 260 seconds) |
| 22:27:46 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 22:36:26 | × | yvan-sraka quits (~yvan-srak@2a01:c22:ac1f:9c00:1306:3abb:2386:5c1b) (Remote host closed the connection) |
| 22:37:25 | × | chomwitt quits (~chomwitt@2a02:587:dc0c:c200:9e04:2be9:6643:df78) (Ping timeout: 268 seconds) |
| 22:37:56 | × | thyriaen quits (~thyriaen@2a01:aea0:dd4:463c:6245:cbff:fe9f:48b1) (Remote host closed the connection) |
| 22:38:33 | <monochrom> | immutable list quicksort : "is that really quicksort?" :: list fft : "is that really fft?" >:) |
| 22:40:23 | <FlaminWalrus> | hpc: apparently, List and Array have vastly different algorithmics for ordered container operations, so it's not unreasonable to expect it to affect things |
| 22:43:21 | <hpc> | speaking of, i was looking at the lagrange transform over the weekend and that's some crazy stuff |
| 22:43:23 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 22:43:55 | <FlaminWalrus> | Laplace? Legendre? |
| 22:44:03 | <hpc> | er, laplace |
| 22:45:05 | <FlaminWalrus> | Gotcha, yeah it's easy to think of it as substituting an imaginary variable $s$ for $i\omega$ in the FT, where $\omega$ is usually real |
| 22:45:05 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 22:45:17 | <FlaminWalrus> | Has similar mathematical advantages, transforming calculus to algebra and all that |
| 22:45:59 | <FlaminWalrus> | At the same time, not as nice for high-level functional analysis as the FT |
| 22:46:06 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 22:46:23 | <hpc> | the part that sold me on it was how it helps with differential equations |
| 22:46:40 | <FlaminWalrus> | Used a lot in circuit analysis where you have a very large problem of a very specific type; it can be faster numerically |
| 22:47:02 | <hpc> | since exponentials and sines both have themselves in their derivatives, and those are the real/imaginary axes of the laplace transform |
| 22:47:36 | × | Franciman quits (~Franciman@mx1.fracta.dev) (Read error: Connection reset by peer) |
| 22:48:45 | <FlaminWalrus> | This could be cool or mean absolutely nothing to you, but an old professor told me about a construction of _field_ isomorphisms between integer-indexed sequences, meromorphic functions, and a direct limit of Banach spaces of real-valued functions |
| 22:48:49 | <hpc> | so you can use it to characterize something governed by differential equations the same way you would use fourier transform to analyze a sound wave |
| 22:48:50 | <EvanR> | Axman6, we already had "fft using list", FlaminWalrus posted one which started the whole discussion xD |
| 22:49:04 | <EvanR> | a discussion on how to make it fast |
| 22:49:31 | <FlaminWalrus> | The last isomorphism is an asymptotic version of the Laplace transform, that allows you to use it when the integrals don't converge |
| 22:49:38 | <EvanR> | ok the issue was memory |
| 22:49:48 | <FlaminWalrus> | (it also wasn't fast lol) |
| 22:49:56 | <hpc> | heh |
| 22:50:23 | <FlaminWalrus> | Took about 30sec to compute a PSD estimate on 400 numbers |
| 22:50:32 | <FlaminWalrus> | s/400/4000 |
| 22:51:56 | <FlaminWalrus> | Another cool thing about transforms: the uncertainty principle in quantum mechanics is a _special case_ of the uncertainty principle for (discrete) Fourier transforms, where there's a tradeoff between resolution in frequency and amplitude |
| 22:52:09 | <FlaminWalrus> | Position and momentum are Fourier-conjugate quantities |
| 22:52:34 | <monochrom> | Tip for Laplace transforms: Do not find the Laplace transforms of sin and cos separately, do a BOGO deal: find the Laplace transform of exp(i*t) then the real part is for cos and the imag part is for sin. |
| 22:54:00 | <FlaminWalrus> | Is there some sort of functor instance to lift List functions through Array? |
| 22:55:14 | <monochrom> | No. But if you use the vector library package, it has a lot of list-inspired functions. |
| 22:55:26 | <dolio> | The one Axman6 linked doesn't appear to fall into the same trap. |
| 22:56:18 | <EvanR> | Vector and Array i are Functors |
| 22:56:26 | × | waleee quits (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 260 seconds) |
| 22:56:43 | <EvanR> | though Vector seems to have more utility functions |
| 22:56:49 | <EvanR> | beyond mapping |
| 22:57:19 | → | waleee joins (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 22:57:42 | <Axman6> | I remember being amazed by the pure-fft implementation years ago, then realising I could make it faster.. I forgot how, I may have submitted a PR, but the author has disappeared a long time ago :( |
| 22:57:48 | <dolio> | I.E. it is zipping lists, not doing nested loops that index into a large list. |
| 22:58:20 | <EvanR> | Vector and Array i are also Foldable, so mapping and folding are covered at least |
| 22:58:43 | <FlaminWalrus> | EvanR: *literally everything* is a functor apparently, if you think about it hard enough. Continuity is a functor from Top to Poset |
| 22:58:43 | <FlaminWalrus> | |
| 22:59:34 | <FlaminWalrus> | These guys are committed to that crusade: https://ncatlab.org/nlab/show/HomePage |
| 23:03:32 | <monochrom> | Wait is that just a forgetful functor that forgets the points and retains only how a lattice of open sets is a poset? |
| 23:04:01 | × | gurkenglas quits (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 23:06:22 | <FlaminWalrus> | Continuity means preimage of open sets is open; it's contravariant, and maps f: X → Y between topological spaces to the induced map of the lattice of the topologies of Y and X under open set inclusion f': Y → X that maps open sets of Y to their (open) preimages |
| 23:06:40 | → | mikoto-chan joins (~mikoto-ch@193.185.223.3) |
| 23:06:42 | <FlaminWalrus> | Friend told me that one as a joke once |
| 23:07:31 | × | libertyprime quits (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) (Ping timeout: 260 seconds) |
| 23:07:40 | <FlaminWalrus> | (I think it does essentially forget the points, but the topological information about f is encoded in f') |
| 23:07:49 | × | Tuplanolla quits (~Tuplanoll@91-159-69-34.elisa-laajakaista.fi) (Ping timeout: 252 seconds) |
| 23:09:02 | × | sayola quits (~sayola@dslb-088-064-186-217.088.064.pools.vodafone-ip.de) (Read error: Connection reset by peer) |
| 23:09:38 | <dolio> | That one is particularly trivial in some settings. You define the algebras that are open sets, and what kind of maps between them are valid, and then the spaces are just the opposite category. |
| 23:09:39 | × | acidjnk quits (~acidjnk@p200300d6e7137a811112d37158fd9527.dip0.t-ipconnect.de) (Ping timeout: 250 seconds) |
| 23:09:47 | → | jmorris joins (uid537181@id-537181.uxbridge.irccloud.com) |
| 23:11:34 | <dolio> | Axman6: Was your trick to not re-calculate the length over and over? |
| 23:13:26 | <Axman6> | possibly - and I think it was doing too much work to interleve/deinterleve the lists, but I haven;t looked at the code for avery long time... |
| 23:14:58 | <FlaminWalrus> | dolio: it's basically a circular definition—arrows in Top are continuous _a priori,_ so trying to define continuity using them is sure to end in disaster |
| 23:15:07 | <FlaminWalrus> | Hence the "joke" |
| 23:16:15 | × | inversed quits (~inversed@90.209.137.56) (Ping timeout: 252 seconds) |
| 23:17:50 | → | Franciman joins (~Franciman@mx1.fracta.dev) |
| 23:19:34 | → | libertyprime joins (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) |
| 23:19:48 | <dolio> | In locale theory, you start by defining "frames," which are complete, distributive lattices. Then you say what a frame homomorphism is, which I think is just the obvious homomorphism for such lattices. Then the category of locales is the opposite of the category of frames. So, every frame gives a locale, and a continuous map from local X to locale Y is a frame homomorphism from Y to X. |
| 23:20:58 | → | c209e6dc-4d76-47 joins (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) |
| 23:21:46 | <EvanR> | continuity is really a placeholder for "what we care about here" |
| 23:23:00 | × | c209e6dc-4d76-47 quits (~aditya@2601:249:4300:1296:195:dac6:592c:a55a) (Client Quit) |
| 23:23:12 | × | mvk quits (~mvk@2607:fea8:5ce3:8500::a80f) (Ping timeout: 264 seconds) |
| 23:23:13 | <dolio> | I think you are encouraged to think of the frame as the opens of the locale, though, rather than them being exactly the same thing. |
| 23:24:39 | <dolio> | Then points are a derived notion, and there are some non-trivial locales without any (global) points. |
| 23:26:25 | → | inversed joins (~inversed@90.209.137.56) |
| 23:27:31 | <FlaminWalrus> | Since we're talking categories, I thought I'd drop this: https://arxiv.org/abs/cs/0404056 is a really cool paper that showcases the utility of the point of view; researchers noticed an isomorphism between the categorical description of quantum information and the categorical description of linear logic, allowing them to translate almost directly the lambda calculi in use for studying the latter |
| 23:28:19 | <FlaminWalrus> | Thinking of quantum advantage in terms of O(1) linear term pruning is a really nice perspective |
| 23:29:11 | <EvanR> | so you want to write quantum hello world. Let me first introduce you to some category theory |
| 23:29:48 | <Axman6> | https://hackage.haskell.org/package/QIO relevant? |
| 23:30:06 | <FlaminWalrus> | Is this #haskell or not? I'd think that's what Jones and the gang tried to do with classical computation :) |
| 23:30:38 | <EvanR> | what is going on with that fonts capital Q |
| 23:31:06 | <EvanR> | that's hipster as hell |
| 23:31:16 | <monochrom> | Indeed sometimes I enjoy pointfree topology, yes. :) |
| 23:31:19 | <Axman6> | This is Haskell, we _are_ hipster as hell |
| 23:31:29 | <EvanR> | haskster |
| 23:34:07 | <Axman6> | > enumFrom () |
| 23:34:09 | <lambdabot> | [()] |
| 23:34:23 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 244 seconds) |
| 23:36:30 | <EvanR> | does QIO require IO... |
| 23:36:39 | <Axman6> | maybe |
| 23:36:39 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 23:37:34 | <EvanR> | ah no, you can run it in a probability monad |
| 23:37:46 | <FlaminWalrus> | newtype UniverseSplitter deriving Monad... |
| 23:37:48 | <Axman6> | perhaps |
| 23:37:54 | <EvanR> | oh I see what you did there |
| 23:39:09 | → | rockystone joins (~rocky@user/rockymarine) |
| 23:42:44 | → | gentauro joins (~gentauro@user/gentauro) |
| 23:43:34 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 23:43:34 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 23:43:37 | allbery_b | is now known as geekosaur |
| 23:44:07 | × | rockystone quits (~rocky@user/rockymarine) (Ping timeout: 252 seconds) |
| 23:54:05 | → | johnjaye joins (~pi@173.209.64.74) |
| 23:54:36 | → | rockystone joins (~rocky@user/rockymarine) |
| 23:56:44 | <hpc> | FlaminWalrus: finally i can bake an apple pie |
All times are in UTC on 2022-10-11.