00:47:47 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 00:48:16 -!- Lord_of_Life_ has joined. 00:50:26 -!- Lord_of_Life has quit (Ping timeout: 250 seconds). 00:50:42 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 01:17:01 -!- Essadon has quit (Quit: Qutting). 01:23:48 -!- arseniiv has quit (Ping timeout: 245 seconds). 01:33:27 -!- sprocklem has quit (Quit: brb). 01:35:13 -!- sprocklem has joined. 01:46:08 -!- doesthis has joined. 01:48:38 hi peeps, so where can I learn about category theory? 01:50:03 because today I met someone who said that they like types because of the commuting diagram of fold, and I want to be able to understand what they have in mind 02:56:59 doesthis: Well, what kind of background do you have? Usually what I recommend generically is Steve Awodey's book "Category Theory", but while it has almost no prerequisites mathematically, it's definitely written in a style that might be uncomfortable if you're not used to reading mathematics. 02:58:01 I'm not sure which commuting diagram that person would have been referring to, but there are some category theoretical approaches to discussing what folds are, via so-called "F-algebras" 02:59:14 F algebras look like the kind he had in mind 02:59:35 (More precisely, that's a formulation of what "catamorphisms" are -- despite the name, that's a term from computer science and not category theory originally) 03:00:26 There are a bunch of things programmers might refer to as folds which are not quite catamorphisms, and a bunch of things which are catamorphisms that most programmers might shy away from calling a fold at first. 03:00:27 -!- pikhq has quit (Quit: Packing up computer stuff for moving). 03:01:01 "catamorphism" is a pointless term, just say "fold" hth 03:01:18 haha, fair enough 03:01:18 I have great difficulty understanding abstractions unless I can keep in mind a particular instantiation of it 03:01:37 What languages are you familiar with? Can I write some Haskell examples? 03:01:45 That one theorem that every initial F-algebra is an isomorphism is pretty good. 03:01:48 Haskell is fine 03:01:59 Okay, so suppose we have a type like this: 03:02:29 data Nature a = Rock | Stream a (Nature a) | Bush (Nature a) (Nature a) 03:03:00 (It's intentionally a bit weird just to give some different cases :) 03:03:42 So, one of the most common patterns that comes up in programming with algebraic data types is to just replace each constructor throughout with another specified value 03:04:05 So for example, we might usefully provide: 03:04:18 foldNature rock stream bush = f 03:04:22 where 03:04:28 f Rock = rock 03:04:43 f (Stream x n) = stream x (f n) 03:05:01 f (Bush n n') = bush (f n) (f n') 03:05:42 i.e. the resulting function f will go through a Nature value and replace each occurrence of Rock with rock, Stream with stream, and Bush with bush 03:06:05 If we do this thing for lists, that's a (right) fold 03:06:49 It replaces each cons in the list with some specified function, and the empty list at the end (if any) with a specified value 03:07:35 that sounds like fold 03:07:40 yeah 03:08:33 These functions, which are uniquely determined by the type in some sense that can be made more precise, are called catamorphisms (or perhaps just folds) 03:09:00 But note that this doesn't get us the left fold on the list type, that one is something less natural. 03:09:45 and in general, it doesn't immediately get us a way to sequentialise the elements of a type, like some generalised notions people have called "fold" would 03:09:58 It's just about substituting structure 03:11:50 One idea for getting at this in a more general way is to make the recursion in the data type more explicit 03:12:08 We could start with some type which was abstracted over the places where we were going to be recursive: 03:12:30 data Nature a n = Rock | Stream a n | Bush n n 03:12:46 and then write a type-level fixed point: 03:13:10 newtype Fix f = In (f (Fix f)) 03:13:28 out :: Fix f -> f (Fix f) 03:13:33 out (In x) = x 03:13:59 So that now Fix (Nature a) becomes equivalent to our original type 03:14:12 (with a lot of noisy In's) 03:15:40 Now, think about a function of type Nature a b -> b 03:16:10 Such a function is kind of like the specification of our three arguments in the above thing, rock, stream, and bush 03:16:41 In particular, if we have some h :: Nature a b -> b 03:17:45 Well, let's say it the other way, if we wanted to specify such a function h, we could do it as follows: 03:17:51 h Rock = rock 03:18:29 h (Stream x n) = stream x n -- no recursion now 03:18:39 h (Bush n n') = bush n n' 03:19:00 Choosing such a rock, stream, and bush will uniquely determine which function h is. 03:19:12 since these generically handle all the cases 03:19:45 that makes sense but I'm going to have to spend time on understanding Fix 03:19:55 So a single function of type (Nature a b -> b), using this non-recursive version of Nature is a way of capturing all the arguments we would have given to the fold 03:21:03 and then there's a way to generically write a fold which will work on types that are expressed in this way (so long as it turns out that the type we're taking the fixed point of is a Functor) 03:21:24 Right, let's look at Fix a bit more carefully 03:21:57 So, before, we might've written some value like Bush (Stream 1 (Stream 2 Rock)) (Stream 3 Rock) 03:22:55 With the Fix version, each "In" gets us another level deeper, basically, so with that approach, the corresponding value would look like: 03:23:33 In (Bush (In (Stream 1 (In (Stream 2 (In Rock))))) (In (Stream 3 (In Rock)))) 03:24:10 :: Fix (Nature Integer) 03:24:30 (sorry for not naming them differently, I didn't feel like writing primes everywhere today) 03:25:26 In :: Nature a (Fix (Nature a)) -> Fix (Nature a) 03:25:35 or more generally 03:25:41 In :: f (Fix f) -> Fix f 03:26:16 So it's possible to write: 03:26:28 cata :: Functor f => (f a -> a) -> Fix f -> a 03:27:05 nyancata 03:27:19 cata h (In x) = h (fmap (cata h) x) 03:27:29 or slightly more fancily 03:27:43 cata h = h . fmap (cata h) . out 03:28:18 So this Functor bit is the category theory creeping its way in a little 03:29:27 From a programmer's perspective, the (Functor f) just expresses the constraint that we need a way to take any function, say of type a -> b, and some value of type f a, and obtain a value of type f b 03:29:38 i.e. we can turn functions of type a -> b into functions of type f a -> f b 03:30:29 You pick any such type f, and then its fixed point has some notion of fold, given by that 'cata' thing 03:30:52 ok 03:32:24 There's a bit more going on there that you can tease out, but that's really the gist of it 03:32:37 thank you 03:33:16 Usually when I actually use this stuff, I much prefer the definitions like foldNature to the fully generic thing 03:33:36 But having such a function is very often useful 03:33:57 (especially when the type is actually recursive, but sometimes even when it's not!) 03:39:13 -!- doesthis has quit (Ping timeout: 256 seconds). 03:39:15 [[User:YamTokTpaFa/sandbox]] https://esolangs.org/w/index.php?diff=60912&oldid=60909 * YamTokTpaFa * (+301) /* Specifications */ 03:39:30 [[User:YamTokTpaFa/sandbox]] https://esolangs.org/w/index.php?diff=60913&oldid=60912 * YamTokTpaFa * (+1) /* = Operating content of file */ 03:54:39 -!- FreeFull has quit. 03:58:26 -!- sprocklem has quit (Quit: Lost terminal). 03:59:17 -!- sprocklem has joined. 08:34:50 -!- AnotherTest has joined. 08:40:52 -!- LKoen has joined. 09:08:38 -!- LKoen has quit (Remote host closed the connection). 09:11:30 -!- b_jonas has joined. 09:17:57 -!- orbitaldecay has joined. 09:20:52 -!- orbitaldecay_ has quit (Ping timeout: 245 seconds). 09:30:25 -!- LKoen has joined. 09:30:50 -!- LKoen has quit (Read error: Connection reset by peer). 11:04:42 `? banana 11:04:43 Bananananananana BATMAN! 11:04:45 `? lens 11:04:47 A lens is just a store comonad coalgebra. 11:26:46 -!- xkapastel has joined. 11:32:58 -!- AnotherTest has quit (Ping timeout: 245 seconds). 12:25:34 -!- arseniiv has joined. 12:50:06 -!- Essadon has joined. 12:50:24 -!- Essadon has quit (Max SendQ exceeded). 12:51:25 -!- Lord_of_Life_ has joined. 12:51:59 -!- Lord_of_Life has quit (Ping timeout: 258 seconds). 12:52:33 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 13:05:37 -!- FreeFull has joined. 13:36:31 -!- xkapastel has quit (Quit: Connection closed for inactivity). 15:09:20 -!- zzo38 has joined. 15:24:05 -!- xkapastel has joined. 16:01:34 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)). 16:54:51 -!- tromp_ has quit (Remote host closed the connection). 17:20:18 -!- MDude has joined. 17:30:57 -!- tromp has joined. 17:35:22 -!- tromp has quit (Ping timeout: 246 seconds). 17:41:17 -!- tromp has joined. 17:43:48 shachaf: erghea bs fpravp cbaq was quite good. (I had the right idea for the raqtnzr very soon, but arranging the required bireynl took quite some effort) 18:00:28 -!- Phantom_Hoover has joined. 18:09:42 -!- tromp has quit (Remote host closed the connection). 18:19:57 -!- nfd has joined. 18:22:37 -!- nfd9001 has quit (Ping timeout: 268 seconds). 18:29:54 -!- tromp has joined. 18:32:51 Hello 18:35:41 hi 18:39:30 Do you like Digi-RGB and IMIDI? 18:42:34 no 18:42:39 i dont work with anything like that 18:44:10 -!- tromp has quit (Remote host closed the connection). 18:47:55 A format could also be made up for transmitting IMIDI messages with infrared signals; in this way the signal is one way (wired IMIDI is two ways), but the infrared can also include a device number, maybe three bits device number. 18:53:39 what is IMIDI and Digi-RGB 19:00:01 -!- AnotherTest has joined. 19:13:38 -!- j-bot has joined. 19:20:32 It is something I invented; Digi-RGB is a video signal (one way only), having several balanced pairs, which is clock, vsync, red, green, blue; at first I had four of each red/green/blue so that there are two clock cycles per pixel, but someone suggested making it more serialized to have less pins and more clock cycles per pixel. 19:21:55 -!- tromp has joined. 19:21:56 IMIDI is a kind of two way MIDI, and is not only for music it can be used for many kind of stuff including television. Most commands are like MIDI, although the format of SysEx payloads is different (the framing is the same though), and a few other commands for device selection (a device address is a sequence of 7-bit numbers) 19:22:07 -!- economicsbat has quit (Ping timeout: 245 seconds). 19:23:44 -!- economicsbat has joined. 20:19:43 -!- FreeFull has quit (Read error: Connection reset by peer). 20:20:06 -!- FreeFull has joined. 20:29:02 int-e: It wa pretty clear that you had to use the cevfba trick, but the fact that you had to use it twice (with grkg vf qrsrng) was sneaky. 20:30:28 How many clock cycles per pixel do you think should be in Digi-RGB? The more clock cycles per pixel, the slower frame rate it can handle and the more complicated the protocol becomes, but it also makes the cable simpler because it needs less pins. 20:31:43 shachaf: I think I only used it once in the end. 20:32:13 * int-e is looking at the tnyyrel now. 20:33:11 Oh, maybe it was a different solution. 20:33:51 shachaf: grkg vf qrsrng was definitely involved 20:34:45 Hmm, maybe I only used it once too. 20:36:28 No, I don't think so. I'm not sure what your solution is. 20:38:08 shachaf: https://int-e.eu/~bf3/tmp/baba-critical{,2}.png is the critical moment (spoiler alert, obviously) 20:39:24 Those both look like screenshots of the beginning of the level. 20:39:40 huh. that's strange. let me try that again 20:40:15 there, fixed. 20:41:06 I'd call that a use of the cevfba trick. 20:41:16 yeah but it's the only one 20:41:24 Oh, huh. 20:41:47 (as usualy you may be counting things differently) 20:41:51 ... usual 20:41:53 You didn't do onon vf sybng? 20:42:02 I get it. 20:42:05 no. 20:42:40 I had convinced myself that was impossible. 20:42:49 Wait, no. How do you get past the skull? 20:44:01 V chfu xrxr ba gbc bs gur fxhyy, juvpu perngrf obgu xrxr naq onon va gung cynpr; V pna zbir bar hcjneqf gb chfu gur synt qbja naq gur bgure bar fgenvtug gb gur evtug. 20:47:50 That's quite different from using the float. 20:52:33 -!- economicsbat has quit (Ping timeout: 250 seconds). 20:52:49 Yeah. As I said, I couldn't make that work. Still can't, for that matter. 20:54:57 -!- economicsbat has joined. 21:03:36 shachaf: The thing is, destroying the 'is' on the right is the only way I see to get enough material for setting up any kind of overlay in the first place. 21:03:39 ... 21:03:59 (I meant to rot13 that) 21:04:19 -!- AnotherTest has quit (Ping timeout: 246 seconds). 21:07:59 I think the trick there is gb chfu nyy gur grkg gb gur evtug, arkg gb gur jnyy. 21:08:22 I should finish this game, I still have some levels left. 21:14:16 I have 220/11/3 now. (The /3 has a spoiler in the changelog) 21:14:32 I'm missing something in zrgn, apparently. 21:18:44 -!- orbitaldecay_ has joined. 21:22:06 -!- orbitaldecay has quit (Ping timeout: 264 seconds). 21:31:07 shachaf: ah. got it. tricky solution :) 21:31:55 ("it" being your kind of solution for erghea bs fpravp cbaq) 21:33:50 -!- xkapastel has quit (Quit: Connection closed for inactivity). 21:42:32 -!- MDude has quit (Ping timeout: 245 seconds). 21:46:17 -!- xkapastel has joined. 21:58:40 wow, just have seen a textbook on logic where the author names variables V|V, V||V, V|||V and so on (though no VV—why?..). I guess they wasn’t pleased with more or less standard v, v′, v′′, v′′′… but I think the result is unjustly rough on the reader 21:58:42 `? master disco 21:58:44 master disco? ¯\(°​_o)/¯ 21:59:44 -!- moei has joined. 21:59:48 I guess they wanted no variable name contained in any other name, though I don’t see how it will make sufficiently many things sufficiently easier 22:00:54 that's not enough though if you want full Incident rules 22:01:36 I could stand string languages for logic textbooks, but this is too much. One should teach that terms and formulas are trees, and that we aren’t interested in the set of allowed variable names any more than it is recursive enumerable 22:02:41 b_jonas: that's not enough though if you want full Incident rules => maybe the reasons are ever less sesible, I didn’t read that book far. This was pretty enough 22:10:59 -!- arseniiv has quit (Ping timeout: 250 seconds). 22:40:11 I followed a link on a webpage and got this: {"message":"Content not available.","code":"404","raw":"{\"message\":\"Content doesn't exist\",\"code\":404}"} What is the purpose of the raw copy included? 22:44:11 (Except the raw isn't quoting 404, and the message is different too, and those thing is seem strange to me) 22:45:40 > fix (\m -> "{\"message\":\"Content not available.\",\"code\":\"404\",\"raw\":" ++ show m ++ "}") 22:45:42 "{\"message\":\"Content not available.\",\"code\":\"404\",\"raw\":\"{\\\"mes... 22:45:52 > var $ fix (\m -> "{\"message\":\"Content not available.\",\"code\":\"404\",\"raw\":" ++ show m ++ "}") 22:45:54 {"message":"Content not available.","code":"404","raw":"{\"message\":\"Conte... 22:49:07 `perl -e sub w{q/{"message":"Content not available.","code":"404","raw":"/.$_[0]=~s/([\"\\])/\\$1/gr.q/"}/}; $s="";$s=w($s) for 0..8; print$s,"\n"; 22:49:07 ​{"message":"Content not available.","code":"404","raw":"{\"message\":\"Content not available.\",\"code\":\"404\",\"raw\":\"{\\\"message\\\":\\\"Content not available.\\\",\\\"code\\\":\\\"404\\\",\\\"raw\\\":\\\"{\\\\\\\"message\\\\\\\":\\\\\\\"Content not available.\\\\\\\",\\\\\\\"code\\\\\\\":\\\\\\\"404\\\\\\\",\\\\\\\"raw\\\\\\\":\\\\\\\"{\\\\\\\\\\\\\\\"message\\\\\\\\\\\\\\\":\\\\\\\\\\\\\\\"Content not available.\\\\\\\\\\\\\\\",\\\\\\\\\\\\\\\ 22:50:11 `perl -e sub w{q/{"message":"Content not available.","code":"404","raw":"/.$_[0]=~s/"/\\"/gr=~s/\\/\\x5C/gr.q/"}/}; $s="";$s=w($s) for 0..8; print$s,"\n"; 22:50:12 ​{"message":"Content not available.","code":"404","raw":"{\x5C"message\x5C":\x5C"Content not available.\x5C",\x5C"code\x5C":\x5C"404\x5C",\x5C"raw\x5C":\x5C"{\x5Cx5C\x5C"message\x5Cx5C\x5C":\x5Cx5C\x5C"Content not available.\x5Cx5C\x5C",\x5Cx5C\x5C"code\x5Cx5C\x5C":\x5Cx5C\x5C"404\x5Cx5C\x5C",\x5Cx5C\x5C"raw\x5Cx5C\x5C":\x5Cx5C\x5C"{\x5Cx5Cx5C\x5Cx5C\x5C"message\x5Cx5Cx5C\x5Cx5C\x5C":\x5Cx5Cx5C\x5Cx5C\x5C"Content not available.\x5Cx5Cx5C\x5Cx5C\x5C",\x5 23:04:00 -!- Sgeo__ has joined. 23:07:07 -!- Sgeo_ has quit (Ping timeout: 245 seconds). 23:07:19 -!- b_jonas has quit (Quit: leaving). 23:13:31 is everyone excited for the GPS week field rollover in ~47 minutes? 23:13:46 midnite UTC 23:24:51 what's the worst that could happen, hmm 23:27:33 Oh there's an article in the news warning that old car GPS systems may fail. That's something. 23:35:12 -!- oerjan has joined. 23:44:31 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 23:53:50 -!- xkapastel has quit (Quit: Connection closed for inactivity). 23:59:54 ONE MINUTE TILL MIDNIGHT