00:02:02 tswett: Please tell me whether or not any of this makes any sense to you. 00:02:27 -!- wareya has quit (Read error: Connection reset by peer). 00:03:33 -!- wareya has joined. 00:04:27 Sgeo: Please tell me you feel a great surge of pride every day knowing you created {{purge}}. 00:05:15 zzo38: that makes sense. 00:05:40 tswett: Does the files I linked makes sense to you? 00:05:58 * Sgeo isn't sure how serious elliott is, but I am somewhat glad I made some somewhat widely used contribution 00:07:20 Now, if I can figure out how it's used today, since I certainly don't see a purge link on http://en.wikipedia.org/wiki/Talk:Buffer_overflow 00:07:36 I also made http://en.wikipedia.org/wiki/Template:Wstress3d 00:11:23 zzo38: oh, those files. I didn't look closely at them. 00:11:56 Sgeo created Wikipedia's {{purge}}? 00:12:55 I have as much claim to it as I have to Wikihack and Creatures Wiki 00:13:10 I created a page number template which was once used on Wikipedia, that template is now gone, however. 00:13:53 Which is probably the most significant thing I ever posted on Wikipedia, except for a few userboxes I created, some of which (but only a few!) are used by other users too. 00:14:19 Most of my Wikipedia edits are removing commas. 00:14:29 -!- Sasha has quit (Ping timeout: 255 seconds). 00:15:03 I have done some minor changes like that too, but I think it was never removing commas, as far as I know. 00:16:28 If you want to see which userboxes that I have created are used by other user pages, go to edit on my user page, and then on the list of templates see things started with "User:Zzo38/Userboxes/" scrolled there, click on each one and select "What links here" to see what pages used that template. 00:17:09 -!- Sasha has joined. 00:17:21 [[User:Zzo38/Userboxes/cmdline]] seems to be the one used the most. 00:19:49 If GoL scientists discovered the glider, would they assume that it has "phases" that it exists in 00:20:03 Gliders in phase 1 react a certain way, gliders in phase 2 act differently 00:20:04 etc 00:20:14 Although presumably macro-level objects are mostly resistant 00:20:22 Or self-repairing 00:21:32 night → 00:21:36 Nigh 00:21:37 t 00:22:29 Sgeo: that's very likely. They might not even discover until the very end that the two things are both gliders. 00:24:18 Well, they might discover that glider guns seem to produce one or the other or both seemingly at random 00:24:37 (depending on how they position the target object, but they wouldn't know that) 00:25:56 No, they'd... only see one at a time, they wouldn't see both eminating at once 00:27:33 hm that's an interesting idea - if their life form has a consistent global phase with some large cycle number, like our own molecules have chirality... 00:28:03 and if the cycle length is even, then the two phases of glider _would_ have different biological effects 00:29:19 oerjan: :D 00:29:26 i wish GoL was the universe, it's cooler than this one 00:30:46 "Out of phase" has more meaning in their universe than it does in ours 00:30:50 although they would probably still be capable of producing chaos in scientific experiments, assuming their universe contained some to start with 00:32:14 What about the orientation of the glider? 00:32:50 Erm, as in, it kind of has 4 phases, 2 of which are just reflections of the other 2 00:33:09 oh right 00:33:17 so they might see 4 different kinds 00:34:36 also if their life form has parts that are always directed in the same way globally, then they might even find gliders traveling in different directions to be different 00:35:15 Hmm, didn't think of that 00:35:34 That's.. interesting 00:35:42 they might need to do experiments with chaos in order to discover the simpler fundamental rules 00:36:26 why does it have to take on such an existance. Why not a different form of life, more like a single sentient being? 00:36:27 life could have global symmetry phases both in position on the grid, timing, and direction 00:36:29 oerjan, Sgeo ^ 00:36:35 Depending how little/much their smallest movement is (if they can move), they'd notice that building a glider gun in different places results in different gliders? 00:36:37 Vorpal: very irrelevant to this hypothetical. 00:36:59 -!- zzo38 has quit (Remote host closed the connection). 00:37:02 elliott, oh? 00:37:13 Sgeo: except without chaos to investigate they might not even recognize building a glider gun in different places as the same operation 00:38:10 ...huh 00:38:36 they might have to use entirely different methods to build them 1 place shifted 00:42:50 Would they even get a correct value for c? 00:43:27 Things in a vacuum have a maximum speed that's lower than c, right? 00:44:05 periodic things, yes 00:44:27 a long line still expands at c, but it gets shorter in the process 00:47:33 Sgeo: Max speed in a vacuum in Life is c/2, IIRC. 00:48:06 I was thinking that we should make a simulation that lets us pretend to be GoL Scientists, but we don't know what good manipulatory .. manipulations are reasonable 00:53:31 elliott, wow, amazing lava + water cavern 00:57:43 Are there items in GoL with a small number of parents? 00:58:09 Perhaps some life might evolve with a finite resource, a pattern that is involved with some reaction that ends up returning just that pattern 00:58:30 Said pattern has no parents other than reactions in which the pattern is part of the parent 00:58:56 Are there items in GoL with a small number of parents? 00:59:00 there are items with 0. 00:59:16 I should have said non-zero 01:07:01 93 true 01:07:03 That is more f'n like it! 01:07:09 Gregor: Okay, I love ELF now (since I got it working.) 01:07:17 And it's even a pretty "istruc", too! 01:07:21 X-D 01:07:38 http://www.dslreports.com/r0/download/1606057~0c86508b26b11f6901e6989a7b4e327c/Soeed.JPG From a recent FCC survey on broadband in the US. 01:08:09 Gregor: http://sprunge.us/TjZS true.s :P 01:08:31 Gregor: (I am not at all sure "xor al, al inc al" works reliably if anything above the low byte of eax is set.) 01:08:41 Not sure how much the kernel looks at, for a syscall, or what guarantees there are on eax's initial value in Linux :P 01:08:44 lawl 01:08:59 Note that by the FCC's current standards on what "broadband" is, 58% of US broadband connections aren't. 01:09:25 Mine most assuredly is not. 01:09:28 Gregor: Still, dude, 92 bytes! Not bad! 01:09:40 Gregor: 4 Mbps down and 1 Mbps up? 01:09:44 elliott: A shell script would be shorter ;) 01:09:46 pikhq: Nope. 01:09:48 Now to go further in the Whirlwind page and pick the one that stays remotely sane :P 01:09:54 Gregor: Not if you add /bin/sh's size :P 01:10:10 -!- Sasha has quit (Ping timeout: 240 seconds). 01:10:16 Gregor: Thing I learned reading sco.com (lawl)'s copy of the ELF header specification thing: ELFs can set an interpreter. Seriously. 01:10:20 Who needs shebangs?! 01:10:20 elliott: I'm assuming, based on my brilliance, that you have to include /bin/sh ANYWAY. 01:10:21 Gregor: But remember, "we're number one!". 01:10:37 elliott: That is actually how dynamic linking works. 01:10:40 Gregor: Not if you don't need it! 01:10:42 elliott: Calling that an interpreter is a bit misleading, although that is the spec, that's where you put /lib/ld.so 01:10:44 elliott: The dynamic linker is set as the interpreter. 01:10:45 pikhq: Oh, indeed. 01:10:50 Say their biological cycle is a multiple of 4 01:10:59 Gregor: But what if you wrote an ELF/esolang polyglot? :p 01:11:02 They see gliders as 4 distinct particles, don't see the connect 01:11:03 elliott: Why not just "xor eax, eax" + "inc eax"? It's not any longer. 01:11:06 Or /anylang, but I doubt most languages would accept such silly :P 01:11:10 fizzie: It is? Oh, wonderful. :p 01:11:13 elliott: But yeah, it could be an invalid ELF otherwise, just enough to get passed into an interpreter :P 01:11:13 What happens when they come across a 5... thingy item 01:11:23 Gregor: Yes, but the ld.so actually gets passed the file. :) 01:11:38 Might they eventually deduce that the 4 particles are in fact the same, similar to the 5-phase item? 01:11:38 ... 01:11:43 Gregor: Kudos to the first person to write an ELF/something else polyglot with the something-else set as the interpreter :P 01:11:50 You could actually set your ELF files to load using qemu. :P 01:11:55 Gregor: Mega kudos if it's a quine. 01:12:09 pikhq: Only if you lied about architecture and the like :P 01:12:11 (well, it'd only really work if the file in question is statically linked.) 01:12:17 elliott: Should be possible with BF. 01:12:17 pikhq: http://sprunge.us/TjZS true.s! 01:12:29 Gregor: That's so close to cheating that I don't like it :P 01:12:34 elliott: :) 01:12:36 :P 01:12:47 Gregor: Like polyglots where the other languages are all in comments. 01:12:52 No, man, you gotta use dual meanings! 01:13:15 -!- Sasha has joined. 01:13:29 I wonder why my version of true is two bytes larger than his 42... 01:13:42 Perhaps nasm changed the instructions generated somehow, but I doubt it. 01:13:50 (in the, what, 11 years since that article was written) 01:13:56 elliott: It is in fact one byte shorter with eax: 01:13:58 00000000 30C0 xor al,al 01:13:58 00000002 FEC0 inc al 01:13:58 00000004 31C0 xor eax,eax 01:13:58 00000006 40 inc eax 01:14:03 fizzie: What luck. 01:15:06 [[Note that the last eight bytes in the ELF header bear a certain kind of resemblence to the first eight bytes in the program header table. A certain kind of resemblence that might be described as "identical".]] 01:15:10 Some phrasings I just love. 01:16:33 fizzie: OTOH "xor ebx, ebx" seems to be bigger than "xor bx, bx" here. 01:16:57 It shouldn't, in 32-bit mode. 01:17:26 One will require a prefix byte, but it should be the one that's not the "native" size. 01:17:46 (ndisasm defaults to -b 16 though.) 01:18:25 fizzie, I found a VAST lava + water cavern 01:18:30 got lost in it for half an hour 01:18:34 before I found my way back 01:18:38 elliott, fizzie ^ 01:18:53 fizzie, just 30 second walk from underground dock 01:19:15 * elliott decides that 93 bytes is acceptable for true 01:19:17 Shocking, I know. 01:19:23 I'm not going to interleave with the ELF header. 01:20:08 It's harder to interleave with the structs anyway. :p 01:20:24 elliott, do you realise you will NEVER use less than min(page-size,disk-sector-size) 01:21:29 -!- Mathnerd314 has joined. 01:21:40 Vorpal: untrue 01:21:46 if you, e.g., pack it all into one file 01:21:58 fizzie: not really, well yes ehdr and phdr, but not putting the code into ehdr 01:22:01 elliott, well okay 01:22:04 fizzie: since it's basically just macros :P 01:22:20 Vorpal: anyway it's not about saving disk space, which I have in abundance 01:22:55 Also don't the filesystems do tail-packing nowadays anyway? 01:23:19 Vorpal: it's more about coding asceticism, for fun and also to remind myself facilis descensus Averni. 01:23:32 (At least experimentally.) 01:23:34 (Whereby Avernus I clearly mean bloated code.) 01:26:39 elliott@dinky:~/code/crtls$ make; wc -c true 01:26:40 make: Nothing to be done for `all'. 01:26:40 94 true 01:26:40 elliott@dinky:~/code/crtls$ make; wc -c true 01:26:40 nasm -f bin true.s -o true 01:26:40 chmod +x true 01:26:42 93 true 01:26:48 fizzie: I replaced "xor ebx, ebx" with "xor bx, bx". 01:26:50 I swear, it's smaller. 01:27:03 bl is the same as bx. 01:27:15 Are you sure you're assembling with bits 32? 01:27:26 It's not the default with -f bin. 01:27:37 00000007 31DB xor ebx,ebx 01:27:37 00000009 6631DB xor bx,bx 01:27:37 0000000C 30DB xor bl,bl 01:27:54 Those are the three variants with ndisasm -b 32. 01:28:05 fizzie: Indeed I was not! Oops. 01:28:20 Now my size matches Raiter's, too. Joy. 01:28:31 fizzie: And the two variants are the same, as well, although ebx is probably "nicer". 01:28:56 real0m0.001s 01:28:57 (I sleeps now.) 01:29:00 That's the fastest true I've ever seen! 01:29:02 ASM POWER! 01:30:42 "When Linux starts up a new executable, one of the things it does is zero out the accumulator (as well as most of the other registers). Taking advantage of this fact would have allowed me to remove the xor, bringing the program down to five bytes. However, this behavior is certainly not documented, and there's no guarantee that it can be counted on to stay that way (other than the lack of any obvious reason to change it)." 01:30:48 Methinks I will not rely on that. :p 01:31:14 Without any code, my ELF spooge takes up 84 bytes. I think that is an acceptable smallest program size :P 01:33:03 My eyes love me so much for this new theme. 01:38:55 "VbeSignature should be set to 'VBE2' when function is called to indicate VBE3.0" 01:42:30 elliott: ... guh? 01:42:45 Gregor: From the Plan 9 fortune file :P 01:43:50 -!- zzo38 has joined. 01:44:38 "If emacs buffers were limited to the size of memory, it would not be possible to 01:44:38 edit /dev/mem." 01:44:45 What a profound and yet utterly insane statement. 01:47:09 What we need is the computer game allowing adjusting all the rules, including: days played, hours played per day, season, wind, gravitational field strength, match condition, players per team, wicket strength, field diameter, field eccentricity, pitch length, leg bye toggle, LBW toggle, time limits, etc. 01:48:34 elliott: It shouldn't make much sense to edit /dev/mem directly in emacs though!? 01:49:07 What would be great is editing the part of Emacs' memory that pertains to the open /dev/mem buffer. 01:49:15 It's Emacsen all the way down! 01:49:43 elliott: Figure out if you can do that. 01:50:15 zzo38: No :P Thinking about Emacs makes my head hurt, I just use the thing and pretend it doesn't exist. 01:51:04 Then figure out if you know anything about making a computer game like I described. 01:51:45 How many computer games allow adjusting gravitational field strength? 01:52:14 I'm going to see if I can watch the first ep of DS9 01:52:38 Sgeo: Then do watch the first ep of DS9 01:53:14 no no, he's just going to check if he _can_. for the principle of it. 01:53:43 OK, check if you can. 01:54:01 oerjan, are there simple 5... thing spaceships? 01:54:10 Sgeo: i have no idea 01:54:17 In the description I made, what other rules are needed adjustment, I think? 01:54:24 * nooga has got a new shell account on an OpenBSD box 01:54:27 * nooga likes 01:54:29 Or at least, ones with an odd number of ... I want to call them phases 01:54:41 Sgeo: Next time see if you can watch DS999 01:55:18 Sgeo: No, you have to call them phones. Even if it is incorrect. 01:56:40 night → 01:57:34 Again? 01:57:45 Again?? 01:58:40 Vorpal goes to bed about 5 times every night. 01:58:50 he dilutes the usage of → to a hideous degree. 01:59:06 * Sgeo points a glider gun at Vorpal 01:59:27 elliott: Maybe he has the macro set up to do that, and he didn't bother to change it. 01:59:27 Vorpal is secretly a hamster 01:59:58 oerjan: i approve of this theory 02:00:19 If they eventually work out that these four c/4 diagonally-moving particles that move in the same direction are one and the same, might they end up lumping in other spaceships that are also c/4 in the same direction? 02:00:47 As they lazily assume that that's the best observable distinguishing characteristic 02:01:45 day 02:01:49 -!- zzo38 has quit (Remote host closed the connection). 02:02:59 I mean, if they don't directly observe that the 4 phases are similar, but guess it from a 5-phase ship or something 02:26:19 Ugh... IPv6 in practice is just a one big Charlie Foxtrot. Well, if you take all the RFCs about it, it is a decent network-layer protocol, but the practical implementation is just CF. 02:27:56 Ilari: YAY PEOPLE 02:28:18 Ilari: This is why technical specifications must be flawless and completely-specified; then it'll only be a major clusterfuck, rather than a gigantic one! 02:28:26 (And that's really the best you can hope for.) 02:29:23 Well, it is not incomplete specifications that are the problem... It is the "not implemented yet" and "broken in practice" stuff... 02:31:33 Oh, and then there's still that great IPv6 routing split (really really bad)... 02:34:42 What's wrong with IPv6 implementations? Beside the fact that they're not used? 02:36:57 #1) The great routing split #2) Hosts that think they have IPv6 connectivity but don't #3) Last mile issues #4) Low adoption on client side. 02:37:29 -!- pikhq has quit (Ping timeout: 255 seconds). 02:38:00 -!- pikhq has joined. 02:38:43 Oh, and then there's DNS whitelisting. It just won't scale. 02:39:19 The complexity isn't linear, it is quadric, and the n is very large. 02:42:01 -!- donglongchao has joined. 02:42:03 DNS. Whitelisting 02:42:05 . 02:42:36 I don't know what that means, but please tell me it's more sane than it sounds 02:43:17 Alsol, what's the great routing split? 02:44:50 -!- donglongchao has left (?). 02:47:14 I didn't realise how badly I was treating my eyes before this. 02:49:04 If GoL life _doesn't_ have a NORTH or whatever, and can rotate, they might discover that 2 of the phases are just the other two upside down 02:49:11 Or might not, I guess 02:49:26 So they'd think there are 2 distinct particles instead of 4 02:49:40 Why am I calling it a "particle"? 02:49:54 Wait, I'm mistaken, aren't I? 02:50:07 elliott: ? 02:50:16 Yeah, n/ 02:50:17 m 02:50:23 Gregor: ? 02:50:36 I didn't realise how badly I was treating my eyes before this. 02:51:02 Gregor: I've upped all my font sizes and made my theme a bit nicer on the eyes :P 02:51:24 Gregor: Specifically everything's about 12pt now, although what I actually did was set my PPI properly, so it's still set at 10pt. 02:51:25 You should wear polarized computer-viewing glasses like meeeeeeeeeeeee :P 02:51:27 But the point is it's big. 02:51:33 Gregor: Do you... actually do that? 02:51:41 elliott: Have for years. 02:51:54 Anyway, the problem was that 10pt fonts when X thinks your display is 96 ppi and you actually have a 120 ppi laptop display that you sit away from = LOL PAIN 02:52:04 Gregor: But why. 02:52:20 elliott: Because after I sit in front of a computer without them for an hour or so, my eyes start to scream at me. 02:52:57 Gregor: What do they even change, anyway? Visually. :p 02:53:22 My eyes have adapted to staring at a computer screen for countless hours at a time. Surprisingly I don't need glasses and have better-than-average vision even after all these years... 02:53:29 elliott: Uhh, everything looks yellow? They reduce glare? I'm really not sure, but I know that they work, and believe their affect to be stronger than placebo. 02:53:44 I have great vision, my eyes just burn after staring at a computer for a while :P 02:53:46 Sgeo: Well, it probably isn't. 02:55:17 Gregor: Everything looking yellow sounds "fun" 02:55:22 Gregor: As in "no thanks" :P 02:57:57 elliott: You certainly lack faith in your mind's ability to adapt to scenarios w.r.t. vision. 02:58:39 Gregor: But dude, all the porno would become ASIAN! 02:58:46 ... 02:58:49 *clap clap* 03:01:24 I think I have no problem looking at a computer screen for 12+ hours at a time 03:01:31 Well, actually, I do go eat sometimes 03:01:49 -!- rodgort has quit (Quit: Coyote finally caught me). 03:04:00 Sgeo: Your computer doesn't feed you? Ha. 03:33:16 Gregor: I eat my keys. 03:33:29 I's geng qui difficu o ype 03:33:34 *ge||ing 03:34:08 I eat my cryptographic keys. 03:34:36 It's getting quite difficult to 0x8fd0113ab9c04e 03:36:08 Gregor: i eat chips 03:36:09 ... 03:36:11 computer chips 03:36:13 ha! ha! 03:36:14 ha! 03:36:16 ha! 03:37:13 Beep boop 03:55:55 okay the newest uTorrent is ugly as fuck 03:56:01 why is it so ugly 03:56:12 it makes me feel like they are making programs for retards 03:56:30 all big pictures and "lawl it's a search thing too" 03:56:45 * oerjan points out that _is_ a possibility 03:56:56 *that that 03:59:10 have there been any big surveys in the last couple of years about which terminal emulators people use? 04:00:07 there are enough people using terminal emulators for a big survey? 04:00:27 and/or virtual terminals 04:00:37 basically everything that can speak vt 04:00:38 If there are glider guns with odd periods, if they're constructed, the GoL scientists should see that some guns emit the 4 (what they think are distinct) while others only 1, right? 04:01:13 Sgeo: you'd think 04:01:45 Not entirely sure if they'd make the right inference from that, but surely it would help 04:02:19 although that doesn't really prove anything, you could be able to make something that emit the 4 without doing it in a periodic way 04:02:38 or even something that emit precisely 3 of them... 04:03:38 *emitted 04:07:12 http://www.linuxquestions.org/questions/linux-software-2/what-is-your-favorite-terminal-emulator-442024/ 04:07:25 lame. why does konsole have such an overwhelming number of users? 04:07:44 People like KDE? 04:07:48 (i know the answer...default kde and all that) 04:07:55 is aterm default on something? 04:08:07 What's with the Konsole hate? 04:08:32 I use konsole on XFCE. 04:08:33 i found it fat, slow and ugly? 04:08:37 konsole is the best terminal emulator there is. 04:08:52 It has nice bindings, tab support, scrollback, ... 04:09:26 it has lots of gui stuff that mostly just got on my nerves 04:09:45 but again: is aterm default for anyone? 04:09:52 quintopia: It has ... almost no GUI stuff, and what little it has is all disable-able, like most KDE stuff. 04:13:09 Gregor: perhaps it is that i am using a relatively slow computer and frequently at a very low resolution 04:13:28 That could be an issue :P 04:15:17 * Sgeo again ponders switching his Ubuntu install to Kubuntu 04:25:52 have there been any big surveys in the last couple of years about which terminal emulators people use? 04:25:56 um it's hardly a subject of holy wars 04:26:33 I use vimterm 04:28:54 yeah, i don't intend to start a major holy war. i just wanted to have my finger on the pulse of common preference 04:34:45 it's really irrelevant 04:34:51 we're never going to see major innovations in vt100 emulation 04:34:59 and that's undeniable 04:35:04 lol 04:35:27 I have to agree with Gregor 04:35:32 Konsole is the superior terminal emulator 04:35:47 i don't really get what konsole does that gnome-terminal doesn't, to be honest 04:36:08 urls 04:36:21 copy-paste keyboard shortcuts 04:36:39 coppro: gnome-terminal does urls. 04:36:42 and copy-paste keyboard shortcuts. 04:37:19 coppro: so/ 04:37:21 *so...? 04:37:22 elliott: hrm 04:37:32 maybe some other term was running last time I used non-konsole then 04:37:37 I sort of assumed it was gnome-term 04:37:39 probably xterm ... 04:38:04 and gnome-terminal is actually pretty darn configurable 04:38:06 unlike most gnome programs :) 04:40:10 coppro: anyway copy-paste shortcuts are for noobs, learn to use selections 04:40:33 elliott: fuck them 04:40:42 coppro: seriously? 04:40:49 they're the only thing X does for me that I like. :) 04:41:08 "The X server has to be the biggest program I've ever seen that doesn't do anything for you." --Ken Thompson 04:41:08 I hate trying to remember what the last thing I selected is 04:41:15 coppro: that's not how you do it... 04:41:25 coppro: you select what you want, immediately move to where you want it, and press the middle button 04:41:31 nothing in-between 04:41:42 elliott: yes, and that last step is where I have trouble 04:41:54 you have trouble pressing the middle button? 04:42:01 no 04:42:05 the nothing in-between bit 04:42:28 also, I hate my algebra prof 04:43:02 the second half of the course to me was roughly equivalent to taking a pull-string doll 04:43:07 that says "polynomials" 04:43:08 "root" 04:43:11 "irreducible" 04:43:14 "finite field" 04:43:17 "irreducible" 04:43:20 "polynomials" 04:44:47 galois galois galois 04:44:54 oerjan: thankfully none of that 04:57:43 Why wouldn't the Second Law of Thermodynamics apply in GoL? Isn't it a statistical thing, rather than a physical thing? 04:58:52 Or maybe I'm confused 05:00:23 well for a start it's not clear that the _first_ law applies 05:01:45 Does Second rely on First? 05:02:01 It seems rather clear that the First law does NOT apply 05:02:20 as for the second, there is probably some way to apply the informational interpretation of it to GoL, yes. but i think that without the first law and the link between them the consequences might not be as strong 05:03:05 that is, you still have free energy 05:03:11 *"energy" 05:03:17 You can go from an active state to a dead state, but not dead to active 05:03:30 *completely dead 05:04:10 I'm thinking that that's.. something 05:04:10 more importantly, you cannot increase the information content 05:04:24 whether or not you have active states 05:04:28 BRB 05:05:11 Vorpal: ping 05:09:15 ack 05:09:53 O viously, I wore out my key 05:10:52 What's the equivalent of heat in GoL? 05:11:02 Err, closest equiv 05:13:37 i have no idea that is not essentially "looks lively" 05:17:05 If we attempt to make GoL life via evolution, we should make sure that it's absolutely full of a pattern F such that all ancestors of F contain more than one copy of F in some generation 05:17:16 So that those otherwise immortal ****s can know mortality 05:18:31 Gregor: Wow -- Brian Raiter, dissatisfied with a 45-byte program returning 42, made a 45-byte program that acts as either true or false, depending on how you invoke it. 05:18:34 http://www.muppetlabs.com/~breadbox/software/tiny/true.asm.txt 05:18:36 Impressive. 05:19:56 elliott: Does it work if invoked as "/bin/true" instead of "true"? 05:20:15 -!- Sgeo has left (?). 05:20:19 -!- Sgeo has joined. 05:20:23 Gregor: It only checks one byte near the end of argv[0], so "yes". 05:20:43 Ok, with maybe one ancestor of F that contains 1 F, but that should be stilllifeish or something 05:21:09 Mmmmm, near the end ... clever, also impressive to keep it so small. 05:21:49 Gregor: I'm too much of a wimp, and have complete ELF headers in my programs. :) 05:21:55 Albeit far smaller ones than you'd expect. 05:22:06 Ahhh :P 05:22:15 Gregor: Still, 91-byte true and false ain't bad :P 05:22:19 I even use symbolic names for the fields and values! I want my money's worth out of elf.inc, it was a bitch to write. 05:22:26 (I copied large swathes of the ELF specification in there.) 05:22:46 Actually, earlier, I was thinking that something similar [but less brutal [all ancestors of F contain as much F as the child]] would help foster competition and assist in the evolution of intelligent life 05:24:18 Gregor: Hopefully I can manage to write cat(1) without going insane. 05:24:26 And next, why, mount(8)! Or, er, eventually. 05:24:41 I pride myself in being A Slightly Better-Maintained asmutils With More Naffness. 05:24:48 (My true and false are smaller though!!) 05:25:40 I should make macros for these :P 05:25:49 (These = standard ELF junk.) 05:32:57 ais523logread: http://www.muppetlabs.com/~breadbox/intercal/os2diff.txt does this still suffice for using c-intercal on os/2? 05:38:43 -!- elliott has quit (Quit: Leaving). 05:50:06 -!- pingveno has quit (Ping timeout: 260 seconds). 05:51:37 -!- pingveno has joined. 05:57:24 -!- rodgort has joined. 06:01:06 "These 16 particles [4 in each direction] cause damage to biological tissue. Fortunately, the damage is usually automatically repaired by our bodies. All 16 particles travel at the same speed." 06:01:31 wait what the hell? 06:02:02 ^not an actual quote from anything 06:02:07 coppro: BE AFRAID 06:02:48 Just what I'm imagining as possible incorrect knowledge in GoLverse 06:03:00 what is GoL? 06:03:06 and why is it so brainhurty 06:03:09 Game of Life 06:04:18 Because we're speculating what a completely alien form of life might think about the universe around them 06:04:38 And said universe has very, very little in common with ours 06:06:58 oh 06:07:07 there are more than 4 directions in Life 06:07:17 Gliders can only travel in 4 06:07:39 oh, I se 06:07:45 For some reason, I'm obsessed with gliders 06:07:51 What they think of gliders 06:08:38 oerjan suggested that if they have a universal-to-their-form-of-life UP, then they might not notice that a NW glider is the same thing as a NE glider 06:09:12 And if there's a biological ... clock thing that's a multiple of 4, the phases of a glider might be seen as distinct and unrelated particles 06:09:27 Although I guess that also assumes that they move at distances that are multiples of four 06:14:58 -!- rodgort has quit (Quit: Coyote finally caught me). 06:15:09 -!- rodgort has joined. 06:23:24 -!- Goosey has quit (Ping timeout: 276 seconds). 06:29:03 oerjan, you awake/ 06:31:01 How does "Amount of blocks destroyed when deterministically placed all at a certain distance from live cells after X amount of time" sound as a definition of heat/ 06:32:05 Well, 'deterministically placed' would need to be replaced with an algorihm, I mean 06:32:11 i guess that's something to measure, at least 06:32:45 Funky IETF working group names: 6lowpan, multimob, softwire, dime, grow, bliss, drinks, martini, mmusic, salud, splices, forces, dane, emu, hokey, kitten, ledbat and storm. 06:34:49 Blinkers shouldn't be considered to have heat, should they? (Given any distance above um, a very small number, used in the definition, they don't) 06:35:37 Actually, then, a sufficiently dense immobile object doesn't have heat, even if there's a lot of internal activity :/ 06:35:57 External heat? 06:36:10 Since it's certainly not causing things around it to move, seeing as it's immobile 06:36:34 Erm, immobile and not giving stuff off 06:36:40 that way to measure it is only going to be an approximation, anyhow, while waiting for their scientists to develop a deeper understanding 06:37:59 Just to clarify: Deeper than us? Or are we trying to think of what THEY'd use as a definition? I was being selfish 06:38:18 Although I'm sure they would have a deeper than us understanding of larger scale stuff 06:38:21 well both 06:59:07 What could we do to attempt to identify life? Intelligent life/ 07:00:44 ...also raising a question, what if WE are in a simulation, and our watchers have limited means to identify intelligent life? 07:00:55 Should we do something that might be recognizable somehow? 07:05:22 -!- oerjan has quit (Quit: Anyway, good night). 07:35:39 -!- kar8nga has joined. 07:49:15 -!- Sgeo has quit (Read error: Connection reset by peer). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:39:59 -!- andywang has joined. 08:40:38 -!- andywang has quit (Client Quit). 08:42:22 -!- Mathnerd314 has quit (Ping timeout: 245 seconds). 08:43:17 -!- kar8nga has quit (Remote host closed the connection). 08:48:09 -!- kar8nga has joined. 09:02:09 -!- kar8nga has quit (Remote host closed the connection). 09:03:23 -!- nopseudoidea has joined. 09:03:41 -!- nopseudoidea has quit (Client Quit). 09:05:34 -!- MigoMipo has joined. 09:53:46 -!- Macstheyjustsuck has joined. 09:54:17 -!- Macstheyjustsuck has left (?). 09:58:37 -!- Phantom_Hoover has joined. 10:26:32 -!- Phantom_Hoover has quit (Ping timeout: 245 seconds). 10:44:00 -!- kar8nga has joined. 10:53:32 -!- Phantom_Hoover has joined. 11:09:08 -!- Georgey has joined. 11:09:25 -!- Georgey has left (?). 11:48:53 -!- ishagua has joined. 11:49:12 -!- ishagua has left (?). 12:04:15 MoveCraft empties chests when used. How irksome. 12:12:39 -!- kfdsfdsafdsaf has joined. 12:14:16 -!- kfdsfdsafdsaf has quit (Remote host closed the connection). 12:25:55 -!- Phantom_Hoover has left (?). 12:26:01 -!- Phantom_Hoover has joined. 12:36:37 And it has a 1000 block limit. "$£%"£$%^ 12:37:16 A changeable limit, but I suspect the ROU will slow things horrifically. I give up. 13:23:50 Vorpal: ping <-- pong 13:24:24 he dilutes the usage of → to a hideous degree. <-- well in that case I had planned to go to bed before, but then forgot it 13:24:29 also it was exactly 2 times 13:48:01 -!- ppseeker has joined. 13:49:02 -!- ppseeker has quit (Quit: ~ Trillian Astra - www.trillian.im ~). 13:57:49 Is it only me who thinks that the lambda calculus page on WP should use tags around expressions rather than ? 13:58:59 Phantom_Hoover: no 13:59:04 but luckily, WP is a W 13:59:06 not merely a P 13:59:28 Yes, but doing things like that will tend to bring down the screaming hoardes of bureaucrats. 14:00:29 no it wont 14:00:41 Well, there's only one way to find out! 14:01:02 -!- wareya_ has joined. 14:02:39 Urgh, the tags aren't even ; they're . 14:04:02 -!- wareya has quit (Ping timeout: 245 seconds). 14:04:44 Previewing this will be fun... 14:07:20 What's the LaTeX macro thingy for ↦? 14:08:14 Ah, \mapsto 14:14:02 * Phantom_Hoover wonders if it's justifiable to be annoyed at people calling the lambda calculus "code". 14:16:21 Oh, forget it. That page is beyond easy repair. 14:16:25 Phantom_Hoover: depends. do you think LC is a programming language? 14:16:29 nooo dont stop! 14:16:36 I MUST 14:17:11 Seriously, I'm trying to convert horrific HTML formatting into nice LaTeX formatting on a huge article with lots of the former. 14:17:28 sounds like a job for a script! 14:18:06 I can fix the various lexing errors etc., but spacing &stupidhtmlentities; have sapped my resolve. 14:20:48 And I suck at scripting things. 14:36:55 -!- oerjan has joined. 14:46:48 -!- augur has quit (Remote host closed the connection). 14:47:13 -!- augur has joined. 14:51:45 -!- augur has quit (Ping timeout: 250 seconds). 14:57:17 [[ Many programmers have created and promoted the computer programming language known as "open source code" to be shared on public sites at no cost, but licensing issues are murky.]] — Reuters. 14:57:40 I shall make this language, and write an absurdly incomprehensible licence for it. 15:03:09 -!- Mathnerd314 has joined. 15:03:31 lol 15:04:03 journalists are extremely ignorant in all fields 15:08:11 Except journalism, naturally. 15:08:22 Which is not a particularly high endorsement. 15:08:37 -!- jack has joined. 15:08:54 -!- jack has changed nick to Jackoz. 15:32:01 * Phantom_Hoover is tempted to add ""Goths don't do anything bad in the UK," I say "They're a gentle and essentially middle-class subculture."" to the head of TV Tropes' article on goths. 15:33:55 -!- augur has joined. 15:49:24 -!- Jackoz has quit (Quit: Jackoz). 15:49:50 -!- Mathnerd314 has quit (Ping timeout: 240 seconds). 15:53:09 -!- FireFly has joined. 16:06:25 -!- elliott has joined. 16:08:38 22:32:45 Funky IETF working group names: 6lowpan, multimob, softwire, dime, grow, bliss, drinks, martini, mmusic, salud, splices, forces, dane, emu, hokey, kitten, ledbat and storm. 16:08:41 Ilari: wat :D 16:09:12 And out of those, dane was IIRC annouced less than 48 hours ago... 16:09:27 23:00:44 ...also raising a question, what if WE are in a simulation, and our watchers have limited means to identify intelligent life? 16:09:28 23:00:55 Should we do something that might be recognizable somehow? 16:09:42 there is no reason to believe they could recognise our actions at all. 16:09:49 and there is also no reason to believe that they *want* sentient life. 16:11:04 Vorpal: ping2 16:11:36 Fun fact: The orignal name for 'dane' was rejected for being too similar to 'kitten' (which is existing working group). 16:13:31 Ilari: do the names have any meaning? :P 16:14:35 elliott, the formatting in the WP article on the lambda calculus is awful. 16:14:40 Phantom_Hoover: I'm fixing it now. 16:14:53 I fully expect to get reverted for daring to be an anonymous IP and making such a sweeping change of evil. 16:15:10 Your soul must be greatly uncompressible. 16:15:15 [[The [[identity function]] I(x) = x takes a single input, ''x'', and immediately returns ''x'']] 16:15:17 Hahaahahaha. 16:15:20 I like how they phrase it imperatively. 16:15:24 But no, I am here to fix formatting alone. 16:15:54 Most of apparently acronyms... 16:16:09 elliott, that section is not for the intelligent. It is for the kind of idiot who thinks of everything imperatively. 16:17:55 No doubt choosen for amusement potential... 16:18:35 Phantom_Hoover: Amusingly, this actually looks uglier with the default math formatting (do it in HTML for simple stuff). 16:18:36 OH WELL! 16:21:10 elliott, use some terrible hack to force it into formatting with TeX always! 16:21:17 No :P 16:22:46 Phantom_Hoover: If this gets reverted I'll replace the λ-calculus article on Esolang (pretty sure we have one) with a merger of it and my revision of the Wikipedia page. 16:23:07 x[x := N] ≡ N 16:23:07 y[x := N] ≡ y, if x ≠ y 16:23:07 (M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N]) 16:23:07 (λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y and y ∉ FV(N) 16:23:12 ^ Only a shithead does that with monospaced text. 16:23:21 elliott, we do not have the MW TeX thing on the esolang wiki. 16:23:38 Phantom_Hoover: Well, I can prerender stuff. Or beg Graue for it. 16:23:39 I asked graue, and he said it was effectively impossible with his hosting setup. 16:24:02 Given two arguments, we have:
16:24:02 ((x, y) ↦ x*x + y*y)(5, 2)
16:24:02 = 5*5 + 2*2 = 29.
16:24:02 However, using currying, we have:
16:24:04 Thou art fucking with me. 16:24:36 Phantom_Hoover: I'll do something or other, then. 16:24:50 rutian is still alive. 16:24:54 After all these years. 16:24:56 And it has an IP. 16:25:03 I could put something on there. :p 16:26:20 You know what'd be funny? If the article had originally been done with LaTeX and some moronic bureaucracy had led to it being HTMLed. 16:27:12 Rutian? 16:28:20 Phantom_Hoover: Rutian is the server of yore. 16:28:28 Born out of the ESO standards agency. 16:28:35 Used for miscellaneous crap for three years or so. 16:28:40 Well, two, it's beend ormant lately. 16:29:14 elliott, was out gathering wood in the middle of nowhere. Found a lone obsidian block, no water or lava near. 16:29:20 elliott, halfway up a mountain 16:29:27 Vorpal: DUN DUN DUUUUN 16:29:40 elliott, what genre are we talking about? 16:29:47 Vorpal: what? 16:30:04 elliott, oh I thought that was supposed to be scary music 16:30:19 Vorpal: It was just your standard moving DUN DUN DUUUUUUUUUUUUN. 16:30:28 http://www.youtube.com/watch?v=7g9WjcGdxuM 16:31:09 elliott, ah, so not the music when the protagonist is carefully walking forward and you just *know* something will happen at any moment 16:31:24 The thing was the lone obsidian. 16:31:59 elliott, hm. will watch in a sec 16:32:28 Phantom_Hoover: Failed to parse (unknown function\begin): \begin{align*} ((x, y) \mapsto x*x + y*y)(5, 2) \\ &= 5*5 + 2*2 = 29. \end{align*} 16:32:32 Phantom_Hoover: NO SOUP FOR YOU 16:32:42 elliott, that video says "not available in your area" 16:32:46 elliott, so what is it 16:32:48 Vorpal: What X-D 16:32:52 Vorpal: It's just the DUN DUN DUUUUUUUUUUUUUUUUN. 16:32:52 elliott, indeed 16:33:08 elliott, huh, it works when refreshing page 16:33:38 elliott, ah, that sound. Is it a stock one or? 16:35:04 Vorpal: Presumably. 16:35:06 :P 16:35:13 Or else constantly reproduced perfectly. 16:35:41 * elliott forces Firefox to look at clog logs in utf8 16:35:51 Vorpal: anyway what i was pinging you for is this http://code.google.com/p/loper/source/browse/trunk/crap/example/oiuboot.asm?r=93 16:36:00 Vorpal: an example of super-simple sorta-orthogonal persistence 16:36:25 elliott, too tired to read asm 16:36:25 Vorpal: specifically, whenever it gets a page fault, it loads that address from disk into RAM and pages it into the virtual address, then returns 16:36:43 Vorpal: and it doesn't even load the kernel itself; it just sets up the page fault handler, and jumps into unloaded memory 16:36:53 the page fault handler then pages it in from disk, and the jump succeeds 16:36:58 heh 16:37:05 elliott, what makes sure stuff gets written to disk then? 16:37:16 Vorpal: It wasn't developed that far. :) 16:37:37 Vorpal: It's the oiu system from memetech.com which is *still* down. 16:37:42 The cap system got more development... 16:41:42 Gregor: Should I switch to sid to get Firefox 3.6? 16:41:58 WHAT, it's still 3.5 in sid. 16:42:02 3.6 is only in experimental. 16:42:10 Fuck this, I'm installing the experimental package manualla. 16:42:12 *manually. 16:43:10 manuel, the package from barcelona 16:44:15 elliott, did you give up on the LC rewrite? 16:45:49 Phantom_Hoover: Not yet. 16:46:40 elliott@dinky:~$ sudo dpkg -i iceweasel_3.6.13-1_amd64.deb 16:46:44 Bring on the instability! 16:46:48 iceweasel depends on xulrunner-1.9.2 (>= 1.9.2.11); however: 16:46:49 Package xulrunner-1.9.2 is not installed. 16:46:49 LOZL 16:50:10 I need: libmozjs3d, iceweasel-l10n-en-gb 16:54:06 speaking of tex articles being redone in html, is there a good tool for converting a tex file to an html file (getting as close an approximation to the formatting as html allows)? 16:56:11 no, there are tools but they all suck at it and i'll kill you if you use them because they're that bad. 16:56:29 damn 16:56:31 you may want to look into mathjax (jsMath's successor) if you're willing to do some manual work. 16:56:38 could you pelase write me one that doesn't suck? 16:56:49 no, it is basically impossible 16:56:54 html doesn't work like that 16:57:05 i don't care about the math. i just want to preserve the non-math formatting 16:57:40 basically, where text and images are located, and laying out of bibliography, and anchoring citations 16:58:01 not gonna happen. html doesn't work like that unless you force it to, and doing it from tex would just be near-impossible. 16:58:14 There's one that's OK. 16:58:17 One sec. 16:58:19 i know a lot of it could be done approximately 16:59:28 and i'm willing to tolerate a lot of differences since they are fundamentally different paradigms 16:59:29 quintopia: http://www.tug.org/applications/tex4ht/ <-- good part: Works well. Bad part: Original creator is dead. 16:59:39 lol 17:00:21 Gregor: so the continued development isn't as good as the original development? 17:00:46 It's not that it's not as good so much as that it's slowed to a crawl. 17:01:49 Anyway, if you have something that you want to convert to an HTML page that looks like it came from LaTeX but isn't just a PDF barfed into a web browser (e.g. a language spec), it's pretty good. 17:02:17 -!- Goosey has joined. 17:02:53 uh 17:03:13 are there some papers on implementing UNIX-like systems? 17:03:37 nooga: Literally every advanced OS textbook in history? :P 17:04:36 Gregor: Unix counts as advanced nowadays? Fuck. 17:04:55 You know, the OS designed to be as simple as possible to implement and get working and be practical. 17:05:02 In a multi-user, networked environment. 17:05:18 elliott: By "advanced" I mean "it covers topics lower than shells", not "it covers research in OS design" 17:05:37 Gregor: There are OS design textbooks which... cover just shells? And not kernels? 17:05:40 Are you being serious? 17:05:47 Slight exaggeration :P 17:05:57 Gregor: ^_________________^ 17:06:01 The point is there are definitely OS textbooks you could read cover-to-cover without being able to write an OS. 17:06:10 Gregor: Indeed... 17:06:16 s/being able to/learning to/ 17:06:40 I love how big my fonts are and how beige my background is! I'm OLD now! 17:08:04 -!- kar8nga has quit (Remote host closed the connection). 17:10:04 elliott, how goes the LaTeXification of WP? 17:10:22 Phantom_Hoover: Oh stop bugging me. 17:14:48 Wtf is up with cat. 17:25:00 -!- oerjan has quit (Quit: leaving). 17:25:50 -!- Mathnerd314 has joined. 17:27:07 elliott, how should we know? 17:27:14 magic 17:41:10 elliott, read MC Experiment day 12 yet? 17:41:46 Phantom_Hoover: I haven't read since ... I forget. Link me to the first 17:42:27 http://www.pcgamer.com/author/pentadact/ 17:42:36 Look back until you find the one you haven't read. 17:43:24 Hey, it goes to beta in 9 days. 17:44:46 I’m swept violently over the threshold, flung clear of the falling water, and left mid-air, sickeningly high over dry land. My only hope is if the water somehow hits the ground before me, spreads out into some kind of pool and… 17:44:47 It doesn’t. 17:44:47 A fountain of metal, stone, sand, torches and sticks explodes from me as I hit the ground, and the last thing I see in front of my dying face is the egg, still intact. 17:45:05 Phantom_Hoover: Beta? With all the shitty bugs? 17:45:58 I assume he's working like hell to ruin^W fix it. 17:55:22 http://www.mezzacotta.net/garfield/?comic=571 17:55:34 I feel quite intensely nerdy for getting that reference. 18:02:49 Phantom_Hoover: http://i.imgur.com/asrO9.jpg XD 18:02:57 Indeed. 18:04:48 "Oh my God. 18:04:48 OK. That should be enough. 18:04:48 On Monday: turns out it’s not enough." 18:04:52 elliott: http://i.imgur.com/LZZJx.gif 18:05:09 quintopia: what 18:05:19 Phantom_Hoover: Ha, the price is going up to 15 euros in beta. 18:05:25 More bugs cost more! 18:06:18 elliott, I still prefer his GCII playthroughs by a small margin, though. 18:06:26 (Tom Francis', that is.) 18:06:38 Phantom_Hoover: I haven't played GCII, so I probably wouldn't. 18:06:45 elliott, nor have I. 18:06:52 It's not written for people who have. 18:07:01 Phantom_Hoover: OK, rephrase: I don't really like games like that. 18:07:19 Nor I. 18:07:31 Phantom_Hoover: Oh fine, link me then. 18:07:37 But I like the Minecraft ones partly because I know how silly he's being. 18:08:28 http://www.computerandvideogames.com/article.php?id=161570&site=pcg 18:09:02 someone buy me a fast computer so i can play minecraft 18:09:19 quintopia: what? 18:09:35 quintopia: I play it on a 1.3 GHz Core 2 Duo laptop running at 1.2 GHz with an onboard Intel GPU 18:09:45 on Linux, no less, where the graphics performance isn't exactly stellar 18:09:56 quintopia: rendering distance to short, graphics to fast, problem solved 18:10:09 hmm 18:10:38 it always ran ridiculously slow for me. i'll see about the settings. 18:10:53 quintopia, and my mid-to-low end laptop runs it fine on normal rendering distance and fancy graphics. 18:10:56 quintopia: Sometimes it does and you just have to restart it. You're not playing in-browser, right? 18:11:36 elliott: don't think so. haven't played in-browser since the very first demo. 18:11:39 it ran okay then. 18:11:51 quintopia: Sun JRE or? 18:11:55 If you're not on Linux I can't even remotely help. 18:12:05 Phantom_Hoover: My laptop is actually on the high end of mid end; it's very sturdy, thin and lightweight, and has a long battery life; it's just that long battery life, lightweight and super-fast CPU don't really mix. :p 18:12:08 It's actually pretty snappy. 18:12:15 a modification of sun jvm i think 18:12:31 elliott, depends on how you define "end", then. 18:13:00 Phantom_Hoover: Price-wise, ignoring things that are stupidly overpriced because of a brand name (*cough* Sony *cough*) 18:13:04 quintopia: what? you mean icedtea? 18:13:10 that isn't a modification, that's a backport of openjdk to run java 6 18:13:22 quintopia: uninstall the other javas and install the sun-java6-* packages on debian 18:15:00 pretty sure that's my default (or something close enough to it not to make a difference) 18:15:24 quintopia: no, in fact, the difference /does/ matter 18:15:30 openjdk, icedtea, etc. don't work or don't work as well 18:16:10 elliott: i'm talking about an experimental build that doesn't actually change the performance of sun's build at all 18:17:11 quintopia: well, suit yourself 18:20:53 [[So I did what I always do when I can't do anything good: I did something stupid.]] 18:21:04 There's something unspeakably profound about that quote. 18:23:00 Phantom_Hoover: Link me to the playthrough of GCII? 18:23:24 http://www.computerandvideogames.com/article.php?id=161570&site=pcg 18:26:00 There's another one where he takes over the next size of galaxy through peaceful means. 18:26:08 Well, *"peaceful" 18:30:39 Phantom_Hoover: "Final Entry"? 18:30:41 That doesn't look final to me. 18:30:46 Also that site's font rendering is fucked up and hideous. 18:30:50 Phantom_Hoover: Or rather: Where's First Entry. 18:34:17 elliott, it must have been updated in place. 18:34:27 Phantom_Hoover: Greaaaat. And on a hideous site too. 18:34:31 The diary starts at Day 1 on that page. 18:34:37 It is rather, isn't it? 18:34:54 Phantom_Hoover: Especially since it fucks up Firefox's font rendering for me. I think I'll skip that playthrough for now. :p 18:35:08 (computerandvideogames.com <-- what kind of domain name is that) 18:35:21 I have a thing that guts horrible rendering on webpages and makes them vaguely readable, if that helps. 18:35:55 It also guts the screencaps, but that's a minor loss and you can use the popup thing if you're that desparate. 18:36:00 *desperate. 18:36:35 Phantom_Hoover: I know, I know, Readability, yes. 18:36:36 I don't like it. 18:36:42 I can never get it looking nicely. 18:37:06 Why not? 18:37:35 To force the formula to render as PNG, add \, (small space) at the end of the formula (where it is not rendered). This will force PNG if the user is in "HTML if simple" mode, but not for "HTML if possible" mode (math rendering settings in preferences). 18:37:36 Aha. 18:37:48 Phantom_Hoover: I'm fussy. 18:38:24 elliott, default layout or Readibility layout. Guess which is palatable? 18:38:35 Phantom_Hoover: Shaddap. 18:41:53 elliott, still in there? 18:42:11 elliott, so can we expect Nicely Formatted Lambda Calculus soon? 18:43:19 Vorpal: Yes. 18:43:20 elliott, if you want me to show you the way out, that happens now, not in half a minute 18:43:20 Phantom_Hoover: Maybe. 18:43:32 Phantom_Hoover: You're really irritating when you bug people. :p 18:43:43 elliott, guess not then 18:43:59 elliott, FEAR MY BUGGINESS. 18:52:02 Phantom_Hoover: Especially since it fucks up Firefox's font rendering for me. I think I'll skip that playthrough for now. :p ← what rendering would that be? 18:52:07 Phantom_Hoover: http://upload.wikimedia.org/math/c/b/4/cb4c22a5b26892bebcca85d168d98566.png 18:52:10 Phantom_Hoover: Whoops! 18:52:15 mathisavariable 18:52:22 19:00:47 Phantom_Hoover: Sheesh, WP's LC raticle is just terrible. 19:01:16 I'm tempted to write a treatment that doesn't both assume its readers are stupid and also use non-obvious mathematical terminology in the same sentence. 19:01:17 *article 19:02:12 elliott, that is the problem with WP as a reference source... 19:02:39 A basic form of equivalence, definable on lambda terms, is alpha equivalence. This states that the particular choice of bound variable, in a lambda abstraction, doesn't (usually) matter. For instance, λx.x and λy.y are alpha-equivalent lambda terms, representing the same identity function. Note that the terms x and y aren't alpha-equivalent, because they are not bound in a lambda abstraction. In many presentations, it is usual to identify alpha 19:02:40 -equivalent lambda terms. 19:02:43 "doesn't (usually) matter" 19:02:45 Real fucking helpful there. 19:03:41 Phantom_Hoover: Prediction: Being an IP, I'm going to get auto-reverted by a bot for making too many changes, left a threatening anti-vandalism message by it on my talk page, and will then have to contact the owner of the bot to stop it re-reverting if I do, at which point my edit will be reverted because fuck you. 19:03:44 (by a human) 19:03:56 -!- cheater99 has quit (Ping timeout: 250 seconds). 19:04:31 I'll help in that case; I have a probably-autoconfirmed account handy. 19:04:50 Phantom_Hoover: Undoubtedly a sockpuppet of me! 19:05:00 Incidentally, Google Code redesigned and it's now harder to read and get information. 19:05:10 More cluttered too. 19:05:12 -!- pikhq has quit (Ping timeout: 265 seconds). 19:05:16 A 2-year-old sockpuppet? 19:06:47 Phantom_Hoover: Yes! Sinister. 19:07:21 http://www.bulwer-lytton.com/ 19:07:35 * Phantom_Hoover shivers at the pure unadulterated awfulness of the design. 19:10:51 Phantom_Hoover: Why are you even visiting those poseurs? http://adamcadre.ac/lyttle.html 19:11:09 Congratulations, you won the Bulwer-Lytton -- you can write long sentences! Fuckfaces. 19:11:14 elliott, stumbled there from TV Tropes. 19:11:27 Phantom_Hoover: (Presumably you already know of the Lytton Lytton, though.) 19:11:33 (If not, READ ALL THE RESULTS NOW AND LAUGH) 19:11:58 elliott, I've seen it. 19:14:18 Phantom_Hoover: FWIW, I'm up to "Beta reduction" in the informal description. 19:14:33 -!- oerjan has joined. 19:17:09 09:55:22 http://www.mezzacotta.net/garfield/?comic=571 19:17:10 09:55:34 I feel quite intensely nerdy for getting that reference. 19:17:11 -!- cheater99 has joined. 19:18:02 hey i got it too, but i consider sandman to be on my _less_ nerdy side... :D 19:18:58 this may just be a further sign of my madness, i guess 19:23:25 oerjan: you know the two "famous" LC encodings of data types, Church and Mogensen-Scott? 19:23:44 actually no. at least not the latter. 19:23:50 oerjan: http://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding 19:26:52 ok the scott encoding looks like the one i consider "obvious" 19:27:50 oerjan: presumably you know http://en.wikipedia.org/wiki/Church_encoding :p 19:28:03 which ofc applies to more than just naturals 19:28:47 oerjan: anyway (as actually mentioned in that article at the bottom) i've been wondering about an encoding based on the induction combinator for a function... i.e. right fold 19:28:50 erm for a data type 19:28:53 so 19:28:55 nil f g = f 19:28:55 cons x xs f g = g x (xs f g) 19:28:57 and then we can define foldr 19:28:59 foldr f z xs = xs z f 19:29:00 :: 19:29:00 foldr f z {nil} = z 19:29:00 foldr f z {cons x xs} = f x (xs z f) 19:29:00 :: 19:29:02 foldr f z {nil} = z 19:29:04 foldr f z {cons x xs} = f x (foldr f z xs) 19:29:21 where the first :: there is expanding out the call tot he list, and the second one is replacing foldr's RHS (xs z f) with a call to foldr itself 19:29:24 oerjan, wait, the Church encoding isn't the obvious one for you? 19:29:38 Phantom_Hoover: mogensen-scott is pretty obvious for non-numeral-and-list types 19:29:45 oerjan: and I'm just wondering how well this would work in general 19:29:57 oerjan: hm you can define foldl with foldr right? (ignore efficiency right now :)) 19:29:59 I forget how 19:30:00 elliott, ah, you meant in general. 19:30:06 Phantom_Hoover: not what is listed as church encoding on the http://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding page 19:30:36 but the boolean and pair examples on the Church encoding page are indeed what i'd consider obvious 19:30:43 Yes, indeed. 19:30:57 oerjan: how do you do that again? :p 19:31:55 in fact i'm wondering if that first page might have it wrong then? 19:32:33 true = \t f -> t, false = \t f -> f 19:32:52 cons x y = \f -> f x y 19:33:07 might be so, now tell me how to define foldl with foldr :p 19:33:12 or i'll ASK #HASKELL 19:33:19 oh _that_ 19:34:20 * oerjan is suddenly very hungry 19:34:25 Hmm, so Mogensen-Scott for the unary naturals would be... 0 = \ c1 c2 -> c1, S = \ n c1 c2 -> c2 n? 19:34:28 i think you'd better as #haskell then 19:34:34 *ask 19:34:40 food -> 19:35:00 I really need to find a better reference for the LC than WP... 19:36:45 oerjan: 19:36:45 myFoldl f z xs = foldr step id xs z 19:36:45 where step x g a = g (f a x) 19:36:51 thanks RWH, that was so real-world of you :P 19:39:45 elliott, what do you seek to do? 19:40:15 Phantom_Hoover: I'm playing with this data encoding to figure out if it's a good representation of data. 19:40:30 Phantom_Hoover: The Reduceron, for instance, represents data as functions, and doesn't use this encoding AFAIK. 19:40:50 And they have notes writing about how their automatic CPU-level inlining optimisations and the like help inline data structures right into the code so that stuff is efficient. 19:40:57 I'm wondering if this foldl expands to the "efficient" implementation. 19:41:53 I get this steadily growing feeling that a Lazy K implementation in Haskell would be a good idea... 19:42:24 Ugh, I made a mistake. 19:42:30 Phantom_Hoover: Enjoy your possible space leak. :p 19:42:34 Phantom_Hoover: But yeah, it would make things easier. 19:42:52 elliott, it can't be worse than the one in the existing (C++) implementation. 19:42:58 Indeed. 19:43:07 Phantom_Hoover: Lazy K is kinda rubbish, though; it's SKI calculus plus gimmick. :p 19:43:42 elliott, well, it's SKI calculus + normal functional IO mechanism. 19:44:02 Phantom_Hoover: Plus syntax gimmick. 19:46:07 I still ponder the sanity of someone who thinks "SKI calculus implementation? C++ is the perfect language!". 19:50:18 foldl fl zl {cons xv xsv} = (\xq gq aq -> gq (fl aq xq)) xv (xsv (\xi -> xi) (\xq gq aq -> gq (fl aq xq))) zl 19:50:19 this is going well 19:51:38 The worst part is that you cannot pronounce any of those names. 19:52:14 Phantom_Hoover: I've renamed them to disambiguate :P 19:53:09 Phantom_Hoover: What I need is a program to let me do valid manipulations on lambda expressions manually, handling alpha conversion etc. itself. 19:53:18 So I can simplify these things step by step without making stupid mistakes. 19:53:44 elliott, you mean handling code as code rather than text? 19:54:48 Yes. 19:55:06 YES! 19:55:10 Simplified 19:55:11 foldl fl zl xsl = foldr (\xq gq aq -> gq (fl aq xq)) (\xi -> xi) xsl zl 19:55:11 to 19:55:13 foldl f z {nil} = z 19:55:13 foldl f z {cons x xs} = foldl f (f z x) xs 19:55:42 What I'm saying is: The right-fold data structure representation supports foldl perfectly well. 19:55:46 (With a sufficiently smart CPU :P) 20:00:42 Phantom_Hoover: I am not sure how this works with mutually-recursive data types and the like :( 20:01:59 Phantom_Hoover: I guess I'll just go with the induction schemes. 20:03:28 "TIL That Linus Torvalds also created Git, so much cooler now" 20:03:31 Fuck you /r/programming. 20:03:34 I'm going to Slashdot. 20:05:38 elliott, zuh? 20:06:19 Phantom_Hoover: That's on /r/programming's front page. 20:06:31 It has finally ceased to be worthwhile even in the slightest. 20:07:47 elliott, "What do Java developers think of Scala?" I sense the invisible hand of Sgeo! 20:08:21 I remember when git was low-level and you had to use cogito to get anything done. 20:12:47 You're OLD 20:13:11 Phantom_Hoover: Dude, it was 2006 :P 20:13:32 OLD 20:13:52 Back then I could write Hello World in Pascal and that was IT! 20:18:02 Tree_rec = 20:18:02 fun (T : Type) (P : Tree T -> Set) => Tree_rect T P 20:18:02 : forall (T : Type) (P : Tree T -> Set), 20:18:02 (forall t : T, P (Leaf T t)) -> 20:18:02 (forall t : Tree T, 20:20:45 Coqing, then? 20:21:11 Phantom_Hoover: No, I was just trying to get a tree's recursive induction scheme. 20:21:16 Since Coq is :oohdependent:, it hasn't helped much. 20:22:14 Oh, the whole rec and rect thing. 20:24:03 Leaf x f g = f x 20:24:03 Branch x y f g = g (x f g) (y f g) 20:24:05 beautiful 20:24:56 mapTree f t = foldTree f Branch 20:25:06 Wundervoll! 20:25:22 erm actaully 20:25:23 mapTree f t = foldTree f Branch t 20:25:30 *actually 20:25:50 oh, wait 20:25:54 mapTree f t = foldTree (Leaf . f) Branch t 20:26:48 mapTree f {Leaf x} = Leaf (f x) 20:26:49 mapTree f {Branch x y} = Branch (mapTree f x) (mapTree f y) 20:26:50 mission accomplished 20:31:11 map f {nil} = nil 20:31:11 map f {cons x xs} = cons (f x) (map f xs) 20:31:16 Phantom_Hoover: these things really expand properly! 20:31:18 this is awesome 20:40:39 Phantom_Hoover: Have you looked at the Reduceron? 20:40:43 It may restore your faith in electrons. 20:40:48 Phantom_Hoover: http://www.cs.york.ac.uk/fp/reduceron/ 20:40:54 The memos are great. 20:41:10 Phantom_Hoover: tl;dr purely functional, lazy graph rewriting on an FPGA. 20:41:21 IO? 20:41:29 electrons, traitorous little schemers 20:41:31 Phantom_Hoover: Yes, it does have IO of some kind. 20:41:34 Well, it has O. Dunno about I. 20:41:43 It's irrelevant though, just gawp at the amazingness and read the lovely memos. 20:54:42 Phantom_Hoover: Oops, I just realised my tree structure was (Leaf X | Branch Tree Tree), which is rather useless. 20:54:54 It should be (Leaf | Branch X Tree Tree). 20:59:18 mapTree f {Leaf} = Leaf 20:59:18 mapTree f {Branch x t1 t2} = Branch (f x) (mapTree f t1) (mapTree f t2) 20:59:20 w00tz. 21:05:35 elliott, idea: redstone message bus (think CAN) 21:05:52 elliott, doable or not? 21:06:02 -!- hagb4rd has joined. 21:06:08 well presumably doable considering the CPU 21:06:13 but... feasible? 21:06:22 hi@all 21:06:37 brb 21:07:54 Vorpal: Maybe. 21:07:59 HackEgo: hi. 21:08:29 `addquote i didn't like jquery, until i decided to use it because it made development faster. now i can't go back to women... 21:08:47 241) i didn't like jquery, until i decided to use it because it made development faster. now i can't go back to women... 21:10:37 hagb4rd: "hi@all" isn't likely to elicit much of a reaction, except for elliott mistabbing you :P 21:10:59 241) i didn't like jquery, until i decided to use it because it made development faster. now i can't go back to women... 21:10:59 wat 21:11:10 `pastequotes 21:11:13 http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.28706 21:11:20 Gregor: I can't believe my new quote system isn't 17x as efficient as the old one :P 21:11:27 Your bot spends SO MUCH TIME doing ABSOLUTELY NOTHING OF VALUE X-D 21:12:23 231) Wow, that [ ! "$1" ] actually works. 21:12:26 Why is that even in the database. 21:12:28 `delquote 231 21:12:41 *poof* 21:14:48 `addquote ONLY GOOD QUOTES PLEASE! AND NO FAKE ONES EITHER! 21:14:49 241) ONLY GOOD QUOTES PLEASE! AND NO FAKE ONES EITHER! 21:15:07 HOLY CRAP MY PARENTS ARE WATCHING SELTZER AND FRIEDBERG AND LAUGHING I'M GOING TO UNIVERSITY NOW AND NEVER COMING BACK 21:15:32 `addquote IN AN ALTERNATE UNIVERSE THAT IS THIS ONE: The mother of my children is a goat! 21:15:44 Phantom_Hoover: ;__; 21:16:49 elliott, AAAAAAAAAAAA ALL MY GENES ARE THEIRS AAAAAAAAAAAAAAAAAAAAAAAA 21:17:25 I think I need a fuse-hg. 21:17:31 Phantom_Hoover: Don't worry! It is theoretically possible that every single gene you have mutated! 21:17:37 You could share NO genes with them! 21:17:40 SCIENCE 21:17:41 elliott, yesyesyesyesyesyes 21:17:41 hg clone-ing a large repository is (sometimes) quite slow >_> 21:17:47 242) IN AN ALTERNATE UNIVERSE THAT IS THIS ONE: The mother of my children is a goat! 21:17:48 Or at least, inconsistent-speed. 21:18:05 Gregor: Is "fuse-hg" meant to be something more interesting than a FUSE interface to hg? 21:21:38 Gregor: y/n? 21:22:00 `quote 129 21:22:03 129) if you claim that the universe is more than 3D the burden of proof is on you to produce a klien bottle that doesn't self intersect ^ I learned that trick from atheists 21:22:16 Ah, the good old days. 21:22:57 it's vaguely irritating that fax was an interesting cool person and an utterly insane psycho in one 21:26:43 hmph, what's foldl on a tree.. 21:27:32 elliott: i'm not sure that makes sense 21:27:37 foldl . toList 21:27:51 oerjan: me neither, but i *want* it to make sense :) 21:27:56 Deewiant: bad Deewiant *slaps* 21:28:15 -- foldlTree f z Leaf = z 21:28:15 -- foldlTree f z (Branch x t1 t2) = foldlTree (f (foldlTree f z t1) x) t2 21:28:16 It typically is that 21:28:18 oerjan: i think that *sort* of works 21:28:28 elliott: Yes 21:28:32 i mean a tree is basically a way to correct for a list's biased direction-ness... 21:28:39 so really there's foldlTreeLeft and foldlTreeRight 21:28:41 if you get my meaning 21:28:47 where you just swap t1 and t2 there 21:28:51 Gregor: hm? were you saying yes to my definition? 21:29:28 note that for a list, a foldl is equivalent to a foldr of the reversed list 21:29:39 elliott: To fuse-hg :P 21:30:10 however if you reverse/mirror a tree, you still use the same fold 21:30:12 Gregor: What would it be, then? (Suggest rename to hg-fuse, for consistency.) 21:30:13 elliott: Basically, I want to be able to fuse-mount a particular revision, then when I unmount it commits a new revision with my changes. 21:30:21 (with tweaked parameters) 21:30:22 oerjan: right. 21:30:27 Gregor: Oh, so "no" then. 21:30:42 Gregor: I was saying: is it more interesting than FUSE? As in: did you mean "fuse" the verb? 21:30:46 As in fuse two hg repositories together in some way? 21:30:48 That would be interesting. 21:30:54 Oh :P 21:32:32 oerjan: give me a tree operation other than fold and map, then :P 21:32:46 elliott: monad operations! 21:32:47 to write in terms of foldr and expand back 21:32:55 oerjan: oh gawd -- what are they on trees? 21:33:26 well return x is just Branch x Leaf Leaf i think 21:33:52 oerjan: I'm doing this because I'm fairly sure that representing structures as their right fold (i.e. their induction-recursion combinator) is the best representation in LC; it's easy to convert pattern matching into it, and when inlining and expanding functions defined with the combinators, they tend to unroll to the obvious, efficient "direct" implementation 21:37:29 actually i'm not sure about monad operations on trees when the x'es are embedded straight into Branch rather than Leaf 21:38:30 oerjan: eh? (Leaf X | Branch Tree Tree) you mean as the alternative? 21:38:33 what should join (Branch (Branch x t1 t2) t3 t4) be 21:38:37 I had that at first, but then realised it doesn't model actual trees 21:38:39 or do you mean 21:38:44 (Leaf X | Branch X Tree Tree)? 21:39:03 the former has an obvious monad instance, at least 21:39:22 the latter may not actually help in that respect 21:39:37 Gyaaah, where's pikhq when you need him and his multimedia nerdery. 21:41:08 Phantom_Hoover: I have some of it. 21:41:16 oerjan: erm but how do you model an "actual" tree with the former? 21:41:24 * Phantom_Hoover just goes for the torrent with the most peers. 21:42:31 elliott: oh forget that 21:42:42 oerjan: what :D 21:42:47 oerjan: but then it's hardly a tree structure, is it? 21:42:50 it doesn't work 21:42:51 oerjan: oh or do you mean, forget what i said 21:42:54 Phantom_Hoover: no, I can help 21:42:55 yeah 21:43:05 Phantom_Hoover: pretend i'm pikhq, i'm as much an encoding nerd as he is :) 21:43:06 well, close 21:43:26 elliott is in fact pikhq converted to big5 21:43:29 elliott, http://torrentz.eu/search?f=futurama+season+3 21:43:36 or wait, that's the wrong way around 21:43:40 (obviously) 21:43:52 Pick one or find a better one. 21:44:01 elliott, I have an idea how to make that "clear" one work. Involves one SR-latch and two buttons 21:44:21 Phantom_Hoover: http://torrentz.com/7f97cf9ea5ff10a01b56789c85ce32e3c8a24674 This is the best one out of the first few. 21:44:33 Phantom_Hoover: 11 seeders, 10 peers. Should go quickly enough. 21:45:00 Phantom_Hoover: There is a preferable 8 gig Matroska rip, but it is seederless. 21:45:04 So go with that one. 21:45:31 elliott, define "quickly enough". 21:45:39 And I shall compare it with actual results. 21:45:42 Phantom_Hoover: You can't tell without downloading. 21:46:03 Phantom_Hoover: It depends on your connection, everyone else's connection, general swarm health... Start the torrent, add the trackers from torrentz, and give it some minutes to get going. 21:46:08 elliott, I mean in the sense of "what would be the kind of order of magnitude you'd expect"? 21:46:28 Phantom_Hoover: A few hours if stuff is good. 21:46:49 1 peer. 21:46:54 Stuff is not good. 21:47:15 1 peer *listed*, not connected. 21:47:24 Phantom_Hoover: Did you add the trackers? 21:47:30 Did you *wait* because this stuff takes time to propagate? 21:47:32 Yep. 21:47:46 There were 4, and one of them was already there. 21:47:46 Phantom_Hoover: No you didn't. 21:47:48 Wait a few minutes. 21:47:52 Phantom_Hoover: Wait. 21:47:57 Phantom_Hoover: You did add them with a blank line in between, yes? 21:48:04 Yes. 21:48:18 Phantom_Hoover: Give it some minutes. 21:48:38 And I am looking at the tracker list right now and two of them have 1 peer listed each. 21:49:30 Phantom_Hoover: OK, I realise you don't get how BitTorrent works, but stop looking at it and go back in five minutes. 21:49:32 Seriously. 21:50:03 I take your point. It's up to 29. 21:52:43 THERE IS EGG ON MY FACE 21:53:10 oerjan: so wait what's the preferable tree structure again :D 21:53:17 YOU NEED TO IMPROVE YOUR COOKING SKILLS 21:53:45 elliott: nothing wrong with your original, is there 21:53:56 oerjan: you mean Tree = Leaf | Branch X Tree Tree? 21:54:01 yes 21:54:05 oerjan: right, so what's join :D 21:54:24 I DON'T KNOW 21:54:36 if it even is a monad 21:54:51 oerjan: now i need to find the monad laws as phrased for join :p 21:54:57 * oerjan googles 21:55:11 oerjan: now i need a winning lottery ticket 21:55:16 (if it worked once, it's worth trying again!) 21:58:03 oerjan: join . return == id 21:58:04 join . fmap return == id 21:58:04 join . join == join . fmap join 21:58:20 oerjan: wait do you need fmap to do a monad? doesn't join/return suffice 21:59:00 elliott, you need it in some capacity, since >>= can't be expressed in terms of join and return alone. 21:59:10 hm indeed 21:59:26 ok well I have treeMap so that's sorted 21:59:37 oerjan: ok so obviously "join (Branch x Leaf Leaf) = x" :) 22:00:32 (>>= f) = join (fmap f), yes? 22:01:30 I wish cpressey was here so I could torment him with both monads AND pointfree style! 22:02:32 Erm, s/!/./ 22:02:52 What an overbearingly gregarious lapse. 22:03:18 elliott: the examples i find for tree monad all seem to assume something equivalent to the Leaf x | Branch (Tree x) (Tree x) version. although i found this one comment: http://www.rhinocerus.net/forum/lang-haskell/383058-good-old-tree-monad.html#post1814212 22:03:45 oerjan: well I mean I have no objection to "Leaf x | Branch (Tree x) (Tree x)" I just don't see how it's a *tree* 22:03:55 as in when someone says "oh yeah i solved this problem using a TREE", i can't imagine them using that 22:05:15 Wait, Tree is a monad now? 22:06:14 Phantom_Hoover: seemingly 22:06:30 oerjan: HA! 22:06:32 -!- Sasha has quit (Ping timeout: 245 seconds). 22:06:40 How are bind and return done? 22:06:40 oerjan: Initially, I thought this was going to be about even plainer binary 22:06:40 trees, like this: 22:06:40 data Tree a = Branch (Tree a) (Tree a) | Leaf a 22:06:40 -- 22:06:40 Simon Richard Clarkstone: 22:06:45 oerjan: = our SimonRC 22:06:50 you can combine it though, Tree a b = Leaf b | Branch a (Tree a b) (Tree a b), then Tree a is still a monad 22:06:52 lesson: #esoteric is unable to avoid itself 22:06:57 you can combine it though, Tree a b = Leaf b | Branch a (Tree a b) (Tree a b), then Tree a is still a monad 22:06:59 that's ugly though :) 22:07:00 Well, I assume return = Leaf. 22:07:20 elliott: um clarkstone doesn't ring a bell 22:07:30 oerjan: Simon Richard Clarkstone = SimonRC 22:07:33 -!- Sasha has joined. 22:07:40 /whois if you want to check (also note present in #haskell too) 22:07:43 oh /whois agrees 22:07:45 also i remember his sig :) 22:07:51 oerjan: so would you recommend I just go for the ultra-plain binary tree route for the sake of algorithmic purity :) 22:07:52 * [SimonRC] (~sc@fof.durge.org): Simon Richard Clarkstone 22:08:10 weird, i thought his surname was something different 22:10:34 Phantom_Hoover: for join, whenever you have t :: Tree a (Tree a b), you can conceptually get a Tree a b from that by replacing all Leaf x with x 22:11:00 (at the outer level) 22:11:11 oerjan, what's the structure of this tree? 22:11:28 the combined one above 22:11:55 oerjan: wait since when does Tree have two type parameters 22:12:09 elliott: in the combined version it does 22:12:23 Right. 22:12:23 oerjan: we're doing the (Leaf X | Branch Tree Tree) version now, I've decided :P 22:12:25 for simplicity 22:12:27 you allow different types for values in branches and in leaves 22:12:38 elliott: ok in that case just ignore the a's 22:14:32 so hm 22:14:37 tree :: Tree (Tree a) -> Tree a 22:14:42 oerjan: oh that's rather easy then isn't it 22:14:46 oerjan: we just want to s/Leaf x/x/ 22:14:53 no? 22:15:02 join (Leaf x) = x; join (Branch t1 t2) = Branch (join t1) (join t2) 22:15:37 yep 22:15:47 oerjan: and thus joinTree = foldTree Branch id 22:15:51 Incidentally, I found out why Coq files have a .v suffix: it's short for "vernacular". 22:16:16 Phantom_Hoover: Insert lewd reference to Coq's name and word beginning with V. 22:16:24 Insert me being swatted by oerjan. 22:16:33 * oerjan obliges -----### 22:17:14 imagine if this subreddit actually were highly active http://www.reddit.com/r/correctionsdept/ 22:17:34 oerjan: "there doesn't seem to be anything here" - ha, ha, ha 22:18:00 hm so wait how do you do bind in terms of fmap and join? 22:18:04 it's uh 22:18:10 x >>= f = join (fmap f x) 22:18:11 right? 22:18:16 indeed 22:18:32 it's no fair to type my lines before me! 22:19:32 (btw it was linked from http://www.reddit.com/r/technology/comments/ek22q/reddit_now_creates_the_news_the_ciapsyteknet/) 22:22:36 elliott, oerjan, I said that about 15 minutes before either of you. 22:23:26 Indeed, (>>=) = flip $ join . fmap 22:23:28 Phantom_Hoover: well your time-traveling ways aren't fair either! 22:24:23 Phantom_Hoover: um no i don't think that's right 22:24:42 oerjan, oh? 22:24:46 progress so far simplifying bind: 22:24:47 bindTree {Leaf v} f = f v 22:24:47 bindTree {Branch t1 t2} f = Branch (((mapTree f t1) (\x -> x) Branch)) (((mapTree f t2) (\x -> x) Branch)) 22:25:03 oerjan, operator precedence or...? 22:25:41 I wish we still had lambdabot... 22:25:45 (>>=) = flip $ (join .) . fmap 22:26:44 you were trying to use . with a two-argument function 22:26:44 oerjan: go ask for lambdabot again :D 22:26:50 Phantom_Hoover: *not* you, you're not nice and persuasive 22:26:55 elliott: i didn't do it the first time 22:27:03 bind = (join .) . flip fmap 22:27:03 oerjan: which is why you're the best person to do it now! 22:27:08 oerjan: nobody's sick of you yet 22:27:39 I doubt anyone remembers me from last time I asked... 22:27:53 Phantom_Hoover: Yes, but when you asked, it disappeared soon after. 22:28:00 When I (IIRC) asked gwern it didn't. 22:28:08 What I'm sayin' is: you're not sweet enough :P 22:28:18 argh 22:28:42 oerjan: just use puppy dog eyes 22:28:43 8.8 22:29:42 elliott: it probably disappears whenever lambdabot quits, regardless. sheesh. 22:30:05 oerjan: it didn't last time, iirc it was added to the list :) i may be wrong though 22:30:22 oerjan: anyway go ask! you can prolly use your haskell report credentials to make ridiculous demands or sth 22:30:25 bindTree {Leaf v} f = f v 22:30:25 bindTree {Branch t1 t2} f = Branch (bindTree t1 f) (bindTree t2 f) 22:30:26 elliott, how's fmap defined for Tree? 22:30:26 YES 22:30:28 if it was added to the list why did it disappear again? 22:30:28 IT FINALLY WORKS 22:30:38 Phantom_Hoover: It's just map. 22:30:42 mapTree f {Leaf x} = Leaf (f x) 22:30:42 mapTree f {Branch t1 t2} = Branch (mapTree f t1) (mapTree f t2) 22:30:43 or 22:30:45 mapTree f t = foldTree Branch (Leaf . f) 22:30:49 oerjan: who knows? I think it changed servers at one point or something 22:30:54 Oh, just map Leaf x => Leaf (f x). 22:30:56 oerjan: Lemmih is the current guy-to-bug. 22:33:05 http://sprunge.us/UiAY here's my working out of all of this 22:33:10 :: precedes a block that's equivalent 22:33:56 Dear god what is that at foldl aaaaa 22:34:30 foldl = xqgqaqgqflaqxqzl 22:34:32 Phantom_Hoover: Read it like this: 22:34:47 foldl f z xs = foldr (\x g a -> g (f a x)) (\x -> x) xs z 22:34:51 olsner: fthagn! 22:34:55 The suffixes on the variables were added because I ran into alpha-renaming issues. 22:35:13 This is why I need a manual-but-automated rewriter tool. :p 22:37:50 Would anyone like a copy of my GLORIOUS EYE-CURING GNOME THEME? 22:39:23 Wait, Coq curries things, doesn't it? 22:40:15 chicken and curry 22:44:29 Phantom_Hoover: Generally, yes. 22:45:21 My tormentor was in fact the byzantine implicit argument system masquerading in the garb of currying oddities. 22:45:54 * elliott notes http://www.cs.york.ac.uk/fp/reduceron/memos/Memo13.txt for reading in a minute 22:46:05 Phantom_Hoover: The implicit argument system is nicer than Agda's, at least. 22:46:12 Phantom_Hoover: Would you like my WONDERFUL GNOME THEME? 22:46:28 WHY IS IT SO "£$%"£$%ING *HARD* TO MAKE ID A FUNCTION? 22:46:32 PLEASE EXPLAIN. 22:46:32 What? 22:46:51 Phantom_Hoover: Definition id x := x. 22:46:59 Wait, no. 22:47:05 Phantom_Hoover: Definition id {A} (x : A) := x. 22:47:13 Anything wrong with that? 22:47:14 elliott, YOU'D THINK IT'D BE THAT SIMPLE BUT NOOOOO 22:47:20 Coq < Definition id {A} (x : A) := x. 22:47:20 id is defined 22:47:22 Phantom_Hoover: Yes it is. 22:47:27 You're doing it wrong. 22:47:29 YES THERE BLOODY WELL IS 22:47:36 Phantom_Hoover: What? 22:47:57 [[Case expressions can be removed by defining data constructors as 22:47:58 functions and transforming case expressions to function applications.]] 22:48:04 elliott, fmap (A B : Set) (f : A -> B). 22:48:10 hey they stole Church's and Mogensen's and Scott's and my idea :) 22:48:15 Phantom_Hoover: And? How is id not a function? 22:48:35 fmap [elided or not actually there depending on what's set] id is a type error. 22:48:51 Don't ask me why because I don't know. 22:49:03 Phantom_Hoover: OK, please give me the full definition of fmap. 22:49:09 id has type forall A : Type, A -> A. 22:49:13 Phantom_Hoover: OK, please give me the full definition of fmap. 22:49:28 NO BECAUSE IT IS EMBARRASSINGLY AWFUL 22:49:36 Phantom_Hoover: OK, please give me the full definition of fmap. 22:49:44 I have done monads in Coq before. 22:50:00 Fixpoint fmap (A B : Set) (f : A -> B) (t : tree A) : tree B := [elided]. 22:50:21 Phantom_Hoover: Definition of tree, please. 22:50:25 Actually, nevermind. 22:50:27 I can just make it an axiom. 22:51:57 Essentially, I'm told that fmap id is an error as id : ID rather than * -> *. 22:52:16 Phantom_Hoover: Yes, because the values of A and B are not clear. 22:52:18 Where ID = forall A : Type, A -> A. 22:52:26 Phantom_Hoover: You might want to try using {A B : Set} in fmap. 22:52:38 Failing that... just give A as a parameter, and forall A in the scope you're in. 22:52:41 elliott, just tried that. 22:52:45 Still an error. 22:52:47 Failing that... just give A as a parameter, and forall A in the scope you're in. 22:52:49 elliott, tried that. 22:52:52 Still an error. 22:53:40 Coq < Axiom tree : Set -> Set. 22:53:40 tree is assumed 22:53:40 Coq < Axiom fmap : forall (A B : Set) (f : A -> B) (t : tree A), tree B. 22:53:40 fmap is assumed 22:53:40 Coq < Definition id {A} (x : A) := x. 22:53:48 fmap_id 22:53:50 : forall A : Set, tree A -> tree A 22:53:52 Phantom_Hoover: You did something wrong, then. 22:54:11 Right, so I have to actually *define my own id* because Coq's definition is idiotic? 22:54:30 Phantom_Hoover: Nope: 22:54:41 elliott, well, you did. 22:54:46 Phantom_Hoover: I forgot Coq has its own. 22:54:56 elliott, then try it with that. 22:55:16 Certainly. 22:55:23 -!- zzo38 has joined. 22:55:33 Coq < Definition fmap_id (A : Set) (t : tree A) : tree A := fmap A A (id (A:=A)) t. 22:55:33 fmap_id is defined 22:55:42 Phantom_Hoover: Was that so hard? 22:55:51 If an implicit parameter can't be inferred, just specify it with (paramname:=val). 22:56:12 How I found out what name to use: 22:56:16 Coq < Check id. 22:56:16 id 22:56:16 : ID 22:56:16 Coq < Print ID. 22:56:16 ID = forall A : Type, A -> A 22:57:13 Exactly what I did. 22:57:31 Phantom_Hoover: I refuse to believe it discriminates against you and refuses to execute the same code that works for me. 22:57:33 You did something wrong. 22:57:49 oerjan: I've managed to convince myself that the only good representation of data as lambda-calculus functions is with their induction-recursion right folds. Yay. 22:58:03 elliott, well, sans the (A := A) which is the silly part I couldn't remember. 22:58:06 "also, for future reference, spambots, makes no sense as an XML-style tag in any markup system I know..." Apparently someone typed that in a spam message in esolang wiki? 22:58:16 Phantom_Hoover: The silly part? That's the important part. 22:58:34 Phantom_Hoover: When you say "fmap A A id t", it can't infer what the value of A is in id's type, (forall A, A -> A). 22:58:50 Phantom_Hoover: You can't say (id A), obviously, because we can easily infer that A:=Set and thus id is Set -> Set and thus (id A) = A. 22:59:02 Phantom_Hoover: The reliable way to specify implicit type parameters is with (name:=val). 22:59:13 Just because the name in id's type and the name in your code happen to coincide doesn't make it silly. 22:59:26 It could be (A:=WhatARandomNameToGiveASet). 22:59:50 elliott, that is not my problem; my problem is "why make the parameter implicit if you'll have to specify it explicitly anyway". 23:00:18 Phantom_Hoover: Because in all the /other/ cases, it works fine. 23:00:37 Implicit parameters are hugely convenient; the type inferrer just can't manage this one case; once you see the error and know what to do, it's trivial to fix. 23:00:43 elliott, you mean those in which id is not being passed to other functions? 23:01:02 Phantom_Hoover: No, you can pass id to other functions easily; just not to functions you're using polymorphically. 23:01:14 (Or some condition roughly like that.) 23:01:22 Do you think it is somehow possible to do some special things in C by a external program that looks at the error messages emitted by the compiler? 23:01:29 It's a compromise solution, sure; but then so is type inference, there's always going to be cases it can't handle. 23:05:56 So that you can insert compile-time error traps into the program, and then in case of specific errors, modify the program and resubmit it to the compiler to try again. 23:06:16 zzo38: That seems... interesting. 23:06:19 An automatic bug-fixer? :p 23:06:23 Phantom_Hoover: Would you like my GNOME THEME?!?!?1i19037248957yj 23:06:59 elliott, does it shrilly scream about type errors constantly? 23:07:56 Phantom_Hoover: NOPE! That's the best feature! 23:08:02 elliott: No, not quite an automatic bug-fixer. You would still have to enter manually what it changes in case of what error, so you might use it to change things in case something doesn't fit due to machine word size, or to allow "x.qqq" to be replaced by a macro if "x" is not a structure, and so on. 23:08:08 Then I shall have it! 23:08:14 Phantom_Hoover: BTW, I often find that it's actually easier to write functions with tactics first. 23:08:17 -!- pikhq has joined. 23:08:29 Every video encoder sucks. 23:08:38 X-D 23:08:49 Phantom_Hoover: Defining functions like that is a Bad Idea, but you can do it -- just end Definition with a dot. And you can even do some fixed-point stuff. Just remember to Show the code at the end and replace the tactics with it. 23:08:57 I cannot figure out *any* way to properly encode mixed framerate video. 23:09:37 Handbrake almost does it, (Windows-only) Avisynth can be hacked into doing it, x264's CLI can do it if you can somehow get a timestamp file for it, and nothing else even *makes the attempt*. 23:10:35 Phantom_Hoover: http://filebin.ca/qkmtx/Kimono.zip 23:10:44 If I could perhaps write a timestamp-generating inverse telecine filter + deinterlacer, I could just barely get it going right. 23:10:47 Phantom_Hoover: Install by selecting the zip in Appearance → Install... 23:11:02 Phantom_Hoover: Fonts to set: Application font = Droid Sans, Document font = Sans, 23:11:05 Desktop font = Droid Sand 23:11:14 *Sans; Window title font = Droid Sans Bold 23:11:17 Fixed width font = Droid Sans Mono 23:11:21 All 10 except Window title, which should be 11. 23:11:35 And set your DPI write in details, too. (http://members.ping.de/~sven/dpi.html to calculate) 23:11:43 Well, okay, so the DPI thing is optional. 23:11:45 But the fonts aren't. :p 23:12:08 Is Droid Sans preinstalled? 23:12:18 Oh, and the .deb for the Droid fonts: http://ubuntu.mirrors.pair.com/archive//pool/universe/t/ttf-droid/ttf-droid_1.00~b112+dfsg+1-0ubuntu1_all.deb 23:12:25 Phantom_Hoover: http://ubuntu.mirrors.pair.com/archive//pool/universe/t/ttf-droid/ttf-droid_1.00~b112+dfsg+1-0ubuntu1_all.deb 23:12:34 Phantom_Hoover: wget it and dpkg -i it. 23:12:49 Oh, and I apologise to pikhq for making a theme that isn't Grey Mist. 23:12:50 So. ATM I am encoding with a gigantic pipeline because I've gotten fed up with the limitations of all the tools out there. ALL OF THEM. 23:13:01 elliott: Screenshot? 23:13:37 Or possibly if you suppress some error messages, even. 23:13:45 pikhq: Sure. 23:14:12 elliott, erm, Appearance expects something called a theme file and complains about the zip. 23:14:21 Phantom_Hoover: Oh. 23:14:25 Phantom_Hoover: I'll reupload in a second. 23:14:26 pikhq: http://imgur.com/GIKWc.png (Phantom_Hoover too) 23:14:33 pikhq: (If you think the fonts are huge, consider that my display is 120 ppi.) 23:14:59 Is that Bad or Good? 23:15:16 It's Good, but it means fonts will look huge for people on less Good displays. :p 23:15:23 (i.e. desktop displays or not-as-small laptops) 23:15:28 Phantom_Hoover: Still want it after seeing THE HIDEOUS SCREENSHOT? 23:15:50 I must say my enthusiasm is dimmed somewhat. 23:16:01 YOUR LOSS 23:16:12 I mean, I actually *like* Mist. 23:16:15 elliott: Insufficiently Grey. And insufficiently Mist. 23:16:17 Now pikhq will yell at me for the fact that it has a gradient. 23:16:20 SEE I WAS RIGHT 23:17:23 pikhq: Looking at it, I guess it actually just shows that, deep down, I still like Bluecurve. :P 23:18:29 Is there an easy way of expressing function composition in Coq? 23:19:16 I think another use of getting these message from compiler to automatically change things, might also include linker errors, if needed. 23:19:31 Phantom_Hoover: http://coq.inria.fr/library/Coq.Program.Basics.html 23:19:34 Notation " g ∘ f " := (compose g f) 23:19:35 (at level 40, left associativity) : program_scope. 23:19:49 Phantom_Hoover: You may want to define your own notation for it that is less Unicodey. 23:20:35 Funnily enough, compose is not a defined object for me. 23:21:03 Phantom_Hoover: "Library Coq.Program.Basics" 23:21:07 Phantom_Hoover: Require Import Coq.Program.Basics. 23:21:31 Phantom_Hoover: (Or Require Import Program.Basics or Require Import Basics.) 23:21:37 Electric terminator, but anyway... 23:21:56 Phantom_Hoover: What about it? 23:22:11 Phantom_Hoover: You realise you can cause statements to become un-evaluated? And also unevaluate everything beyond a certain point in the document? 23:22:21 Which, of course, is what you should do all the time when correcting things... 23:22:33 C-c C-u to unevaluate the previous statement, I think ... but I've forgotten. 23:22:45 elliott, yes, but typing "." evaluates. 23:23:03 Phantom_Hoover: Yes; and? 23:23:32 eviluation 23:24:41 elliott, so Require Import Foo.Bar. will evaluate as soon as I type the "." after Foo. 23:24:53 Phantom_Hoover: And? 23:25:13 Hey, it takes care of that. 23:25:51 Phantom_Hoover: Ohh, I see what you mean. 23:25:52 Yes, it does. 23:26:00 Proof General is godly. 23:26:21 "# See the Proof General Eclipse wiki for screenshots of Proof General in Eclipse." 23:26:22 WHY DOES THAT EXIST 23:27:52 XD. 23:31:02 Phantom_Hoover: What are you writing in Coq? 23:31:49 elliott, incompetence personified. 23:31:58 Phantom_Hoover: Which is intended to be? 23:32:37 Something... monady... 23:33:05 Phantom_Hoover: Oh, sprunge your code. :p 23:33:37 -!- MigoMipo has quit (Ping timeout: 260 seconds). 23:34:06 Even better: I'll EXTRACT it! 23:35:25 Phantom_Hoover: I'd prefer to laugh at your Coq. 23:35:30 Considering extraction removes all the interesting dependency. 23:35:37 the monad of incompetence 23:35:58 finally a good use for strict encapsulation 23:36:19 NB: My method for proving things in Coq is "type simpl. Type rewrite and some relevant rule. Type unfold and a function name. Is proof finished? Repeat otherwise." 23:36:37 With "type intros. Type induction and a variable name." stuck in for good measure. 23:36:46 And the occasional reflexivity. 23:37:05 I know 6 tactics and that is enough! 23:40:16 Phantom_Hoover: If rewrite is your most common tactic, ur doin it rong. 23:40:28 Deeply. 23:40:32 Phantom_Hoover: BTW, Proof General can list all the tactics in the system (there's fewer than you think). 23:40:37 Just TAB on that and pick a likely one. :p 23:40:47 I don't pretend to know how to do it properly. 23:41:41 Phantom_Hoover: I'm just trying to help. 23:44:28 But seriously; I've never had occasion to do anything interesting enough to invest time into properly learning Coq. 23:46:39 Phantom_Hoover: Do what me and fax were trying to do, replace the standard library. 23:46:54 Phantom_Hoover: (Try starting with category theory; there's a wonderful paper about embedding it into Coq, absolutely wonderful.) 23:47:02 That actually seems worthwhile. How do I sign up? 23:47:04 If you can't get the algebraic structures down, you lose. 23:47:07 Phantom_Hoover: You sign up by doing it! 23:47:14 Phantom_Hoover: Er, there's some option to Coq to tell it to forget the stdlib exists. 23:47:15 Let me find it. 23:47:26 -!- Sasha2 has joined. 23:47:33 i note that fax disappeared from the internet right after oerjan banned it 23:47:50 Phantom_Hoover: 23:47:51 (* 23:47:51 *** Local Variables: *** 23:47:51 *** coq-prog-args: ("-emacs-U" "-nois") *** 23:47:51 *** End: *** 23:47:54 ...i've seen fax on freenode since then 23:47:59 Phantom_Hoover: Put that at the end of your file... or the top, I forget. 23:48:05 oerjan: Well, okay, stopped posting to reddit. And its blog. 23:48:07 Also, I think you misunderestimate how weirdly uneven my understanding of things. 23:48:11 *is 23:48:17 Phantom_Hoover: Try the bottom. Yes, the bottom. 23:48:24 -!- Sasha has quit (Ping timeout: 240 seconds). 23:49:18 Phantom_Hoover: http://sqig.math.ist.utl.pt/pub/CarvalhoA/98-C-DiplomaThesis/maintext.ps 23:49:21 Phantom_Hoover: (One version of) the lovely paper. 23:49:45 elliott, did I mention that I don't know any category theory? 23:49:54 Phantom_Hoover: You don't really have to. :p 23:50:13 Also that I'm tired? 23:50:20 It's not even midnight... 23:50:39 Phantom_Hoover: Categories are what happens when you decide to make entire mathematical foundations objects. For instance, in the Set category, objects are sets. In the Hask category (Haskell), objects are Haskell types. 23:50:54 Phantom_Hoover: Then you get to the cat of small cats -- sorry, category of small categories -- and shit goes crazy. 23:51:02 I think oerjan can agree with the part of my explanation that involves shit going crazy. 23:51:19 Phantom_Hoover: Also morphisms and monoids and monads. 23:52:02 and topoi. or so i hear. 23:52:20 oerjan: i never got that far :D 23:52:31 not really me either