00:02:02 <zzo38> 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 <elliott> Sgeo: Please tell me you feel a great surge of pride every day knowing you created {{purge}}.
00:05:15 <tswett> zzo38: that makes sense.
00:05:40 <zzo38> 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 <Sgeo> 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 <Sgeo> I also made http://en.wikipedia.org/wiki/Template:Wstress3d
00:11:23 <tswett> zzo38: oh, those files. I didn't look closely at them.
00:11:56 <tswett> Sgeo created Wikipedia's {{purge}}?
00:12:55 <Sgeo> I have as much claim to it as I have to Wikihack and Creatures Wiki
00:13:10 <zzo38> I created a page number template which was once used on Wikipedia, that template is now gone, however.
00:13:53 <zzo38> 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 <tswett> Most of my Wikipedia edits are removing commas.
00:14:29 -!- Sasha has quit (Ping timeout: 255 seconds).
00:15:03 <zzo38> 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 <zzo38> 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 <zzo38> [[User:Zzo38/Userboxes/cmdline]] seems to be the one used the most.
00:19:49 <Sgeo> If GoL scientists discovered the glider, would they assume that it has "phases" that it exists in
00:20:03 <Sgeo> Gliders in phase 1 react a certain way, gliders in phase 2 act differently
00:20:14 <Sgeo> Although presumably macro-level objects are mostly resistant
00:20:22 <Sgeo> Or self-repairing
00:22:29 <tswett> Sgeo: that's very likely. They might not even discover until the very end that the two things are both gliders.
00:24:18 <Sgeo> Well, they might discover that glider guns seem to produce one or the other or both seemingly at random
00:24:37 <Sgeo> (depending on how they position the target object, but they wouldn't know that)
00:25:56 <Sgeo> No, they'd... only see one at a time, they wouldn't see both eminating at once
00:27:33 <oerjan> 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 <oerjan> and if the cycle length is even, then the two phases of glider _would_ have different biological effects
00:29:26 <elliott> i wish GoL was the universe, it's cooler than this one
00:30:46 <Sgeo> "Out of phase" has more meaning in their universe than it does in ours
00:30:50 <oerjan> although they would probably still be capable of producing chaos in scientific experiments, assuming their universe contained some to start with
00:32:14 <Sgeo> What about the orientation of the glider?
00:32:50 <Sgeo> Erm, as in, it kind of has 4 phases, 2 of which are just reflections of the other 2
00:33:17 <oerjan> so they might see 4 different kinds
00:34:36 <oerjan> 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 <Sgeo> Hmm, didn't think of that
00:35:34 <Sgeo> That's.. interesting
00:35:42 <oerjan> they might need to do experiments with chaos in order to discover the simpler fundamental rules
00:36:26 <Vorpal> 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 <oerjan> life could have global symmetry phases both in position on the grid, timing, and direction
00:36:35 <Sgeo> 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 <elliott> Vorpal: very irrelevant to this hypothetical.
00:36:59 -!- zzo38 has quit (Remote host closed the connection).
00:37:13 <oerjan> Sgeo: except without chaos to investigate they might not even recognize building a glider gun in different places as the same operation
00:38:36 <oerjan> they might have to use entirely different methods to build them 1 place shifted
00:42:50 <Sgeo> Would they even get a correct value for c?
00:43:27 <Sgeo> Things in a vacuum have a maximum speed that's lower than c, right?
00:44:27 <oerjan> a long line still expands at c, but it gets shorter in the process
00:47:33 <pikhq> Sgeo: Max speed in a vacuum in Life is c/2, IIRC.
00:48:06 <Sgeo> 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 <Vorpal> elliott, wow, amazing lava + water cavern
00:57:43 <Sgeo> Are there items in GoL with a small number of parents?
00:58:09 <Sgeo> 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 <Sgeo> Said pattern has no parents other than reactions in which the pattern is part of the parent
00:58:56 <elliott> <Sgeo> Are there items in GoL with a small number of parents?
00:59:16 <Sgeo> I should have said non-zero
01:07:09 <elliott> Gregor: Okay, I love ELF now (since I got it working.)
01:07:17 <elliott> And it's even a pretty "istruc", too!
01:07:38 <pikhq> http://www.dslreports.com/r0/download/1606057~0c86508b26b11f6901e6989a7b4e327c/Soeed.JPG From a recent FCC survey on broadband in the US.
01:08:09 <elliott> Gregor: http://sprunge.us/TjZS true.s :P
01:08:31 <elliott> 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 <elliott> 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:59 <pikhq> Note that by the FCC's current standards on what "broadband" is, 58% of US broadband connections aren't.
01:09:25 <Gregor> Mine most assuredly is not.
01:09:28 <elliott> Gregor: Still, dude, 92 bytes! Not bad!
01:09:40 <pikhq> Gregor: 4 Mbps down and 1 Mbps up?
01:09:44 <Gregor> elliott: A shell script would be shorter ;)
01:09:48 <elliott> Now to go further in the Whirlwind page and pick the one that stays remotely sane :P
01:09:54 <elliott> Gregor: Not if you add /bin/sh's size :P
01:10:10 -!- Sasha has quit (Ping timeout: 240 seconds).
01:10:16 <elliott> 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 <Gregor> elliott: I'm assuming, based on my brilliance, that you have to include /bin/sh ANYWAY.
01:10:21 <pikhq> Gregor: But remember, "we're number one!".
01:10:37 <pikhq> elliott: That is actually how dynamic linking works.
01:10:40 <elliott> Gregor: Not if you don't need it!
01:10:42 <Gregor> 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 <pikhq> elliott: The dynamic linker is set as the interpreter.
01:10:50 <Sgeo> Say their biological cycle is a multiple of 4
01:10:59 <elliott> Gregor: But what if you wrote an ELF/esolang polyglot? :p
01:11:02 <Sgeo> They see gliders as 4 distinct particles, don't see the connect
01:11:03 <fizzie> elliott: Why not just "xor eax, eax" + "inc eax"? It's not any longer.
01:11:06 <elliott> Or /anylang, but I doubt most languages would accept such silly :P
01:11:10 <elliott> fizzie: It is? Oh, wonderful. :p
01:11:13 <Gregor> elliott: But yeah, it could be an invalid ELF otherwise, just enough to get passed into an interpreter :P
01:11:13 <Sgeo> What happens when they come across a 5... thingy item
01:11:23 <pikhq> Gregor: Yes, but the ld.so actually gets passed the file. :)
01:11:38 <Sgeo> Might they eventually deduce that the 4 particles are in fact the same, similar to the 5-phase item?
01:11:43 <elliott> 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 <pikhq> You could actually set your ELF files to load using qemu. :P
01:11:55 <elliott> Gregor: Mega kudos if it's a quine.
01:12:09 <elliott> pikhq: Only if you lied about architecture and the like :P
01:12:11 <pikhq> (well, it'd only really work if the file in question is statically linked.)
01:12:17 <Gregor> elliott: Should be possible with BF.
01:12:17 <elliott> pikhq: http://sprunge.us/TjZS true.s!
01:12:29 <elliott> Gregor: That's so close to cheating that I don't like it :P
01:12:47 <elliott> Gregor: Like polyglots where the other languages are all in comments.
01:12:52 <elliott> No, man, you gotta use dual meanings!
01:13:15 -!- Sasha has joined.
01:13:29 <elliott> I wonder why my version of true is two bytes larger than his 42...
01:13:42 <elliott> Perhaps nasm changed the instructions generated somehow, but I doubt it.
01:13:50 <elliott> (in the, what, 11 years since that article was written)
01:13:56 <fizzie> elliott: It is in fact one byte shorter with eax:
01:13:58 <fizzie> 00000000 30C0 xor al,al
01:13:58 <fizzie> 00000004 31C0 xor eax,eax
01:15:06 <elliott> [[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 <elliott> Some phrasings I just love.
01:16:33 <elliott> fizzie: OTOH "xor ebx, ebx" seems to be bigger than "xor bx, bx" here.
01:16:57 <fizzie> It shouldn't, in 32-bit mode.
01:17:26 <fizzie> One will require a prefix byte, but it should be the one that's not the "native" size.
01:17:46 <fizzie> (ndisasm defaults to -b 16 though.)
01:18:25 <Vorpal> fizzie, I found a VAST lava + water cavern
01:18:30 <Vorpal> got lost in it for half an hour
01:18:34 <Vorpal> before I found my way back
01:18:53 <Vorpal> fizzie, just 30 second walk from underground dock
01:19:15 * elliott decides that 93 bytes is acceptable for true
01:19:23 <elliott> I'm not going to interleave with the ELF header.
01:20:08 <fizzie> It's harder to interleave with the structs anyway. :p
01:20:24 <Vorpal> elliott, do you realise you will NEVER use less than min(page-size,disk-sector-size)
01:21:29 -!- Mathnerd314 has joined.
01:21:46 <elliott> if you, e.g., pack it all into one file
01:21:58 <elliott> fizzie: not really, well yes ehdr and phdr, but not putting the code into ehdr
01:22:04 <elliott> fizzie: since it's basically just macros :P
01:22:20 <elliott> Vorpal: anyway it's not about saving disk space, which I have in abundance
01:22:55 <fizzie> Also don't the filesystems do tail-packing nowadays anyway?
01:23:19 <elliott> Vorpal: it's more about coding asceticism, for fun and also to remind myself facilis descensus Averni.
01:23:32 <fizzie> (At least experimentally.)
01:23:34 <elliott> (Whereby Avernus I clearly mean bloated code.)
01:26:39 <elliott> elliott@dinky:~/code/crtls$ make; wc -c true
01:26:40 <elliott> make: Nothing to be done for `all'.
01:26:40 <elliott> elliott@dinky:~/code/crtls$ make; wc -c true
01:26:40 <elliott> nasm -f bin true.s -o true
01:26:48 <elliott> fizzie: I replaced "xor ebx, ebx" with "xor bx, bx".
01:27:15 <fizzie> Are you sure you're assembling with bits 32?
01:27:26 <fizzie> It's not the default with -f bin.
01:27:37 <fizzie> 00000007 31DB xor ebx,ebx
01:27:37 <fizzie> 00000009 6631DB xor bx,bx
01:27:37 <fizzie> 0000000C 30DB xor bl,bl
01:27:54 <fizzie> Those are the three variants with ndisasm -b 32.
01:28:05 <elliott> fizzie: Indeed I was not! Oops.
01:28:20 <elliott> Now my size matches Raiter's, too. Joy.
01:28:31 <elliott> fizzie: And the two variants are the same, as well, although ebx is probably "nicer".
01:29:00 <elliott> That's the fastest true I've ever seen!
01:30:42 <elliott> "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 <elliott> Methinks I will not rely on that. :p
01:31:14 <elliott> Without any code, my ELF spooge takes up 84 bytes. I think that is an acceptable smallest program size :P
01:33:03 <elliott> My eyes love me so much for this new theme.
01:38:55 <elliott> "VbeSignature should be set to 'VBE2' when function is called to indicate VBE3.0"
01:42:45 <elliott> Gregor: From the Plan 9 fortune file :P
01:43:50 -!- zzo38 has joined.
01:44:38 <elliott> "If emacs buffers were limited to the size of memory, it would not be possible to
01:44:45 <elliott> What a profound and yet utterly insane statement.
01:47:09 <zzo38> 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 <zzo38> elliott: It shouldn't make much sense to edit /dev/mem directly in emacs though!?
01:49:07 <elliott> What would be great is editing the part of Emacs' memory that pertains to the open /dev/mem buffer.
01:49:15 <elliott> It's Emacsen all the way down!
01:49:43 <zzo38> elliott: Figure out if you can do that.
01:50:15 <elliott> zzo38: No :P Thinking about Emacs makes my head hurt, I just use the thing and pretend it doesn't exist.
01:51:04 <zzo38> Then figure out if you know anything about making a computer game like I described.
01:51:45 <zzo38> How many computer games allow adjusting gravitational field strength?
01:52:14 <Sgeo> I'm going to see if I can watch the first ep of DS9
01:52:38 <zzo38> Sgeo: Then do watch the first ep of DS9
01:53:14 <oerjan> no no, he's just going to check if he _can_. for the principle of it.
01:53:43 <zzo38> OK, check if you can.
01:54:01 <Sgeo> oerjan, are there simple 5... thing spaceships?
01:54:17 <zzo38> 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:29 <Sgeo> Or at least, ones with an odd number of ... I want to call them phases
01:54:41 <zzo38> Sgeo: Next time see if you can watch DS999
01:55:18 <zzo38> Sgeo: No, you have to call them phones. Even if it is incorrect.
01:58:40 <elliott> Vorpal goes to bed about 5 times every night.
01:58:50 <elliott> he dilutes the usage of → to a hideous degree.
01:59:06 * Sgeo points a glider gun at Vorpal
01:59:27 <zzo38> elliott: Maybe he has the macro set up to do that, and he didn't bother to change it.
01:59:27 <oerjan> Vorpal is secretly a hamster
01:59:58 <elliott> oerjan: i approve of this theory
02:00:19 <Sgeo> 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 <Sgeo> As they lazily assume that that's the best observable distinguishing characteristic
02:01:49 -!- zzo38 has quit (Remote host closed the connection).
02:02:59 <Sgeo> 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 <Ilari> 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:28:18 <elliott> 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 <elliott> (And that's really the best you can hope for.)
02:29:23 <Ilari> Well, it is not incomplete specifications that are the problem... It is the "not implemented yet" and "broken in practice" stuff...
02:31:33 <Ilari> Oh, and then there's still that great IPv6 routing split (really really bad)...
02:34:42 <Sgeo> What's wrong with IPv6 implementations? Beside the fact that they're not used?
02:36:57 <Ilari> #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 <Ilari> Oh, and then there's DNS whitelisting. It just won't scale.
02:39:19 <Ilari> The complexity isn't linear, it is quadric, and the n is very large.
02:42:01 -!- donglongchao has joined.
02:42:03 <Sgeo> DNS. Whitelisting
02:42:36 <Sgeo> I don't know what that means, but please tell me it's more sane than it sounds
02:43:17 <Sgeo> Alsol, what's the great routing split?
02:44:50 -!- donglongchao has left (?).
02:47:14 <elliott> I didn't realise how badly I was treating my eyes before this.
02:49:04 <Sgeo> 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 <Sgeo> Or might not, I guess
02:49:26 <Sgeo> So they'd think there are 2 distinct particles instead of 4
02:49:40 <Sgeo> Why am I calling it a "particle"?
02:49:54 <Sgeo> Wait, I'm mistaken, aren't I?
02:50:36 <Gregor> <elliott> I didn't realise how badly I was treating my eyes before this.
02:51:02 <elliott> Gregor: I've upped all my font sizes and made my theme a bit nicer on the eyes :P
02:51:24 <elliott> 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 <Gregor> You should wear polarized computer-viewing glasses like meeeeeeeeeeeee :P
02:51:27 <elliott> But the point is it's big.
02:51:33 <elliott> Gregor: Do you... actually do that?
02:51:41 <Gregor> elliott: Have for years.
02:51:54 <elliott> 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:20 <Gregor> 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 <elliott> Gregor: What do they even change, anyway? Visually. :p
02:53:22 <elliott> 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 <Gregor> 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 <Gregor> I have great vision, my eyes just burn after staring at a computer for a while :P
02:53:46 <Ilari> Sgeo: Well, it probably isn't.
02:55:17 <elliott> Gregor: Everything looking yellow sounds "fun"
02:55:22 <elliott> Gregor: As in "no thanks" :P
02:57:57 <Gregor> elliott: You certainly lack faith in your mind's ability to adapt to scenarios w.r.t. vision.
02:58:39 <elliott> Gregor: But dude, all the porno would become ASIAN!
03:01:24 <Sgeo> I think I have no problem looking at a computer screen for 12+ hours at a time
03:01:31 <Sgeo> Well, actually, I do go eat sometimes
03:01:49 -!- rodgort has quit (Quit: Coyote finally caught me).
03:04:00 <Gregor> Sgeo: Your computer doesn't feed you? Ha.
03:33:29 <elliott> I's geng qui difficu o ype
03:34:08 <Gregor> I eat my cryptographic keys.
03:34:36 <Gregor> It's getting quite difficult to 0x8fd0113ab9c04e
03:55:55 <Sasha> okay the newest uTorrent is ugly as fuck
03:56:12 <Sasha> it makes me feel like they are making programs for retards
03:56:30 <Sasha> all big pictures and "lawl it's a search thing too"
03:56:45 * oerjan points out that _is_ a possibility
03:59:10 <quintopia> have there been any big surveys in the last couple of years about which terminal emulators people use?
04:00:07 <oerjan> there are enough people using terminal emulators for a big survey?
04:00:37 <quintopia> basically everything that can speak vt
04:00:38 <Sgeo> 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:45 <Sgeo> Not entirely sure if they'd make the right inference from that, but surely it would help
04:02:19 <oerjan> 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 <oerjan> or even something that emit precisely 3 of them...
04:07:12 <quintopia> http://www.linuxquestions.org/questions/linux-software-2/what-is-your-favorite-terminal-emulator-442024/
04:07:25 <quintopia> lame. why does konsole have such an overwhelming number of users?
04:07:44 <Sgeo> People like KDE?
04:07:48 <quintopia> (i know the answer...default kde and all that)
04:08:07 <Sgeo> What's with the Konsole hate?
04:08:32 <Gregor> I use konsole on XFCE.
04:08:37 <Gregor> konsole is the best terminal emulator there is.
04:08:52 <Gregor> It has nice bindings, tab support, scrollback, ...
04:09:26 <quintopia> it has lots of gui stuff that mostly just got on my nerves
04:09:45 <quintopia> but again: is aterm default for anyone?
04:09:52 <Gregor> quintopia: It has ... almost no GUI stuff, and what little it has is all disable-able, like most KDE stuff.
04:13:09 <quintopia> Gregor: perhaps it is that i am using a relatively slow computer and frequently at a very low resolution
04:13:28 <Gregor> That could be an issue :P
04:15:17 * Sgeo again ponders switching his Ubuntu install to Kubuntu
04:25:52 <elliott> <quintopia> have there been any big surveys in the last couple of years about which terminal emulators people use?
04:25:56 <elliott> um it's hardly a subject of holy wars
04:28:54 <quintopia> 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:51 <elliott> we're never going to see major innovations in vt100 emulation
04:35:27 <coppro> I have to agree with Gregor
04:35:32 <coppro> Konsole is the superior terminal emulator
04:35:47 <elliott> i don't really get what konsole does that gnome-terminal doesn't, to be honest
04:36:21 <coppro> copy-paste keyboard shortcuts
04:36:39 <elliott> coppro: gnome-terminal does urls.
04:36:42 <elliott> and copy-paste keyboard shortcuts.
04:37:32 <coppro> maybe some other term was running last time I used non-konsole then
04:37:37 <coppro> I sort of assumed it was gnome-term
04:38:04 <elliott> and gnome-terminal is actually pretty darn configurable
04:38:06 <elliott> unlike most gnome programs :)
04:40:10 <elliott> coppro: anyway copy-paste shortcuts are for noobs, learn to use selections
04:40:49 <elliott> they're the only thing X does for me that I like. :)
04:41:08 <elliott> "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 <coppro> I hate trying to remember what the last thing I selected is
04:41:15 <elliott> coppro: that's not how you do it...
04:41:25 <elliott> coppro: you select what you want, immediately move to where you want it, and press the middle button
04:41:42 <coppro> elliott: yes, and that last step is where I have trouble
04:41:54 <elliott> you have trouble pressing the middle button?
04:42:05 <coppro> the nothing in-between bit
04:42:28 <coppro> also, I hate my algebra prof
04:43:02 <coppro> the second half of the course to me was roughly equivalent to taking a pull-string doll
04:43:07 <coppro> that says "polynomials"
04:44:54 <coppro> oerjan: thankfully none of that
04:57:43 <Sgeo> 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 <Sgeo> Or maybe I'm confused
05:00:23 <oerjan> well for a start it's not clear that the _first_ law applies
05:01:45 <Sgeo> Does Second rely on First?
05:02:01 <Sgeo> It seems rather clear that the First law does NOT apply
05:02:20 <oerjan> 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 <oerjan> that is, you still have free energy
05:03:17 <Sgeo> You can go from an active state to a dead state, but not dead to active
05:03:30 <Sgeo> *completely dead
05:04:10 <Sgeo> I'm thinking that that's.. something
05:04:10 <oerjan> more importantly, you cannot increase the information content
05:04:24 <oerjan> whether or not you have active states
05:09:53 <Sgeo> O viously, I wore out my key
05:10:52 <Sgeo> What's the equivalent of heat in GoL?
05:11:02 <Sgeo> Err, closest equiv
05:13:37 <oerjan> i have no idea that is not essentially "looks lively"
05:17:05 <Sgeo> 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 <Sgeo> So that those otherwise immortal ****s can know mortality
05:18:31 <elliott> 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 <elliott> http://www.muppetlabs.com/~breadbox/software/tiny/true.asm.txt
05:19:56 <Gregor> 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 <elliott> Gregor: It only checks one byte near the end of argv[0], so "yes".
05:20:43 <Sgeo> Ok, with maybe one ancestor of F that contains 1 F, but that should be stilllifeish or something
05:21:09 <Gregor> Mmmmm, near the end ... clever, also impressive to keep it so small.
05:21:49 <elliott> Gregor: I'm too much of a wimp, and have complete ELF headers in my programs. :)
05:21:55 <elliott> Albeit far smaller ones than you'd expect.
05:22:15 <elliott> Gregor: Still, 91-byte true and false ain't bad :P
05:22:19 <elliott> 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 <elliott> (I copied large swathes of the ELF specification in there.)
05:22:46 <Sgeo> 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 <elliott> Gregor: Hopefully I can manage to write cat(1) without going insane.
05:24:26 <elliott> And next, why, mount(8)! Or, er, eventually.
05:24:41 <elliott> I pride myself in being A Slightly Better-Maintained asmutils With More Naffness.
05:24:48 <elliott> (My true and false are smaller though!!)
05:25:40 <elliott> I should make macros for these :P
05:25:49 <elliott> (These = standard ELF junk.)
05:32:57 <elliott> 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 <Sgeo> "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:02:02 <Sgeo> ^not an actual quote from anything
06:02:48 <Sgeo> Just what I'm imagining as possible incorrect knowledge in GoLverse
06:03:06 <coppro> and why is it so brainhurty
06:04:18 <Sgeo> Because we're speculating what a completely alien form of life might think about the universe around them
06:04:38 <Sgeo> And said universe has very, very little in common with ours
06:07:07 <coppro> there are more than 4 directions in Life
06:07:17 <Sgeo> Gliders can only travel in 4
06:07:45 <Sgeo> For some reason, I'm obsessed with gliders
06:07:51 <Sgeo> What they think of gliders
06:08:38 <Sgeo> 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 <Sgeo> 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 <Sgeo> 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 <Sgeo> oerjan, you awake/
06:31:01 <Sgeo> 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 <Sgeo> Well, 'deterministically placed' would need to be replaced with an algorihm, I mean
06:32:11 <oerjan> i guess that's something to measure, at least
06:32:45 <Ilari> 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 <Sgeo> 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 <Sgeo> Actually, then, a sufficiently dense immobile object doesn't have heat, even if there's a lot of internal activity :/
06:35:57 <Sgeo> External heat?
06:36:10 <Sgeo> Since it's certainly not causing things around it to move, seeing as it's immobile
06:36:34 <Sgeo> Erm, immobile and not giving stuff off
06:36:40 <oerjan> 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 <Sgeo> 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 <Sgeo> Although I'm sure they would have a deeper than us understanding of larger scale stuff
06:59:07 <Sgeo> What could we do to attempt to identify life? Intelligent life/
07:00:44 <Sgeo> ...also raising a question, what if WE are in a simulation, and our watchers have limited means to identify intelligent life?
07:00:55 <Sgeo> 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: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:37:16 <Phantom_Hoover> A changeable limit, but I suspect the ROU will slow things horrifically. I give up.
13:23:50 <Vorpal> <elliott> Vorpal: ping <-- pong
13:24:24 <Vorpal> <elliott> 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 <Vorpal> 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 <Phantom_Hoover> Is it only me who thinks that the lambda calculus page on WP should use <math> tags around expressions rather than <code>?
13:58:59 <augur> Phantom_Hoover: no
13:59:04 <augur> but luckily, WP is a W
13:59:28 <Phantom_Hoover> Yes, but doing things like that will tend to bring down the screaming hoardes of bureaucrats.
14:01:02 -!- wareya_ has joined.
14:04:02 -!- wareya has quit (Ping timeout: 245 seconds).
14:14:02 * Phantom_Hoover wonders if it's justifiable to be annoyed at people calling the lambda calculus "code".
14:16:25 <augur> Phantom_Hoover: depends. do you think LC is a programming language?
14:17:11 <Phantom_Hoover> 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 <augur> sounds like a job for a script!
14:18:06 <Phantom_Hoover> I can fix the various lexing errors etc., but spacing &stupidhtmlentities; have sapped my resolve.
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 <Phantom_Hoover> [[ 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 <Phantom_Hoover> I shall make this language, and write an absurdly incomprehensible licence for it.
15:03:09 -!- Mathnerd314 has joined.
15:04:03 <nooga> journalists are extremely ignorant in all fields
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 <elliott> 22:32:45 <Ilari> 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:09:12 <Ilari> And out of those, dane was IIRC annouced less than 48 hours ago...
16:09:27 <elliott> 23:00:44 <Sgeo> ...also raising a question, what if WE are in a simulation, and our watchers have limited means to identify intelligent life?
16:09:28 <elliott> 23:00:55 <Sgeo> Should we do something that might be recognizable somehow?
16:09:42 <elliott> there is no reason to believe they could recognise our actions at all.
16:09:49 <elliott> and there is also no reason to believe that they *want* sentient life.
16:11:36 <Ilari> Fun fact: The orignal name for 'dane' was rejected for being too similar to 'kitten' (which is existing working group).
16:13:31 <elliott> Ilari: do the names have any meaning? :P
16:14:35 <Phantom_Hoover> elliott, the formatting in the WP article on the lambda calculus is awful.
16:14:40 <elliott> Phantom_Hoover: I'm fixing it now.
16:14:53 <elliott> I fully expect to get reverted for daring to be an anonymous IP and making such a sweeping change of evil.
16:15:15 <elliott> [[The [[identity function]] <math>I(x) = x</math> takes a single input, ''x'', and immediately returns ''x'']]
16:15:20 <elliott> I like how they phrase it imperatively.
16:15:24 <elliott> But no, I am here to fix formatting alone.
16:15:54 <Ilari> Most of apparently acronyms...
16:16:09 <Phantom_Hoover> elliott, that section is not for the intelligent. It is for the kind of idiot who thinks of everything imperatively.
16:17:55 <Ilari> No doubt choosen for amusement potential...
16:18:35 <elliott> Phantom_Hoover: Amusingly, this actually looks uglier with the default math formatting (do it in HTML for simple stuff).
16:21:10 <Phantom_Hoover> elliott, use some terrible hack to force it into formatting with TeX always!
16:22:46 <elliott> 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 <elliott> (M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
16:23:07 <elliott> (λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y and y ∉ FV(N)
16:23:12 <elliott> ^ Only a shithead does that with monospaced text.
16:23:21 <Phantom_Hoover> elliott, we do not have the MW TeX thing on the esolang wiki.
16:23:38 <elliott> Phantom_Hoover: Well, I can prerender stuff. Or beg Graue for it.
16:23:39 <Phantom_Hoover> I asked graue, and he said it was effectively impossible with his hosting setup.
16:24:02 <elliott> Given two arguments, we have:<br />
16:24:02 <elliott> <tt>((x, y) ↦ x*x + y*y)(5, 2)</tt><br />
16:24:02 <elliott> <tt> = 5*5 + 2*2 = 29</tt>.<br />
16:24:02 <elliott> However, using currying, we have:<br />
16:24:36 <elliott> Phantom_Hoover: I'll do something or other, then.
16:25:03 <elliott> I could put something on there. :p
16:26:20 <Phantom_Hoover> 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:28:20 <elliott> Phantom_Hoover: Rutian is the server of yore.
16:28:28 <elliott> Born out of the ESO standards agency.
16:28:35 <elliott> Used for miscellaneous crap for three years or so.
16:28:40 <elliott> Well, two, it's beend ormant lately.
16:29:14 <Vorpal> elliott, was out gathering wood in the middle of nowhere. Found a lone obsidian block, no water or lava near.
16:29:20 <Vorpal> elliott, halfway up a mountain
16:29:40 <Vorpal> elliott, what genre are we talking about?
16:30:04 <Vorpal> elliott, oh I thought that was supposed to be scary music
16:30:19 <elliott> Vorpal: It was just your standard moving DUN DUN DUUUUUUUUUUUUN.
16:30:28 <elliott> http://www.youtube.com/watch?v=7g9WjcGdxuM
16:31:09 <Vorpal> 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 <elliott> The thing was the lone obsidian.
16:31:59 <Vorpal> elliott, hm. will watch in a sec
16:32:28 <elliott> 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 <elliott> Phantom_Hoover: NO SOUP FOR YOU
16:32:42 <Vorpal> elliott, that video says "not available in your area"
16:32:46 <Vorpal> elliott, so what is it
16:32:52 <elliott> Vorpal: It's just the DUN DUN DUUUUUUUUUUUUUUUUN.
16:33:08 <Vorpal> elliott, huh, it works when refreshing page
16:33:38 <Vorpal> elliott, ah, that sound. Is it a stock one or?
16:35:13 <elliott> Or else constantly reproduced perfectly.
16:35:41 * elliott forces Firefox to look at clog logs in utf8
16:35:51 <elliott> 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 <elliott> Vorpal: an example of super-simple sorta-orthogonal persistence
16:36:25 <Vorpal> elliott, too tired to read asm
16:36:25 <elliott> 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 <elliott> 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 <elliott> the page fault handler then pages it in from disk, and the jump succeeds
16:37:05 <Vorpal> elliott, what makes sure stuff gets written to disk then?
16:37:16 <elliott> Vorpal: It wasn't developed that far. :)
16:37:37 <elliott> Vorpal: It's the oiu system from memetech.com which is *still* down.
16:37:42 <elliott> The cap system got more development...
16:41:42 <elliott> Gregor: Should I switch to sid to get Firefox 3.6?
16:41:58 <elliott> WHAT, it's still 3.5 in sid.
16:42:02 <elliott> 3.6 is only in experimental.
16:42:10 <elliott> Fuck this, I'm installing the experimental package manualla.
16:43:10 <oerjan> manuel, the package from barcelona
16:46:40 <elliott> elliott@dinky:~$ sudo dpkg -i iceweasel_3.6.13-1_amd64.deb
16:46:48 <elliott> iceweasel depends on xulrunner-1.9.2 (>= 1.9.2.11); however:
16:46:49 <elliott> Package xulrunner-1.9.2 is not installed.
16:50:10 <elliott> I need: libmozjs3d, iceweasel-l10n-en-gb
16:54:06 <quintopia> 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 <elliott> 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:31 <elliott> you may want to look into mathjax (jsMath's successor) if you're willing to do some manual work.
16:56:38 <quintopia> could you pelase write me one that doesn't suck?
16:56:49 <elliott> no, it is basically impossible
16:56:54 <elliott> html doesn't work like that
16:57:05 <quintopia> i don't care about the math. i just want to preserve the non-math formatting
16:57:40 <quintopia> basically, where text and images are located, and laying out of bibliography, and anchoring citations
16:58:01 <elliott> 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 <Gregor> There's one that's OK.
16:58:19 <quintopia> i know a lot of it could be done approximately
16:59:28 <quintopia> and i'm willing to tolerate a lot of differences since they are fundamentally different paradigms
16:59:29 <Gregor> quintopia: http://www.tug.org/applications/tex4ht/ <-- good part: Works well. Bad part: Original creator is dead.
17:00:21 <quintopia> Gregor: so the continued development isn't as good as the original development?
17:00:46 <Gregor> It's not that it's not as good so much as that it's slowed to a crawl.
17:01:49 <Gregor> 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:03:13 <nooga> are there some papers on implementing UNIX-like systems?
17:03:37 <Gregor> nooga: Literally every advanced OS textbook in history? :P
17:04:36 <elliott> Gregor: Unix counts as advanced nowadays? Fuck.
17:04:55 <elliott> You know, the OS designed to be as simple as possible to implement and get working and be practical.
17:05:02 <elliott> In a multi-user, networked environment.
17:05:18 <Gregor> elliott: By "advanced" I mean "it covers topics lower than shells", not "it covers research in OS design"
17:05:37 <elliott> Gregor: There are OS design textbooks which... cover just shells? And not kernels?
17:05:47 <Gregor> Slight exaggeration :P
17:05:57 <elliott> Gregor: ^_________________^
17:06:01 <Gregor> The point is there are definitely OS textbooks you could read cover-to-cover without being able to write an OS.
17:06:16 <Gregor> s/being able to/learning to/
17:06:40 <elliott> 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:22 <elliott> Phantom_Hoover: Oh stop bugging me.
17:25:00 -!- oerjan has quit (Quit: leaving).
17:25:50 -!- Mathnerd314 has joined.
17:41:46 <elliott> Phantom_Hoover: I haven't read since ... I forget. Link me to the first
17:44:46 <elliott> 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 <elliott> 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 <elliott> Phantom_Hoover: Beta? With all the shitty bugs?
17:55:34 <Phantom_Hoover> I feel quite intensely nerdy for getting that reference.
18:02:49 <elliott> Phantom_Hoover: http://i.imgur.com/asrO9.jpg XD
18:04:48 <elliott> OK. That should be enough.
18:04:48 <elliott> On Monday: turns out it’s not enough."
18:04:52 <quintopia> elliott: http://i.imgur.com/LZZJx.gif
18:05:19 <elliott> Phantom_Hoover: Ha, the price is going up to 15 euros in beta.
18:06:18 <Phantom_Hoover> elliott, I still prefer his GCII playthroughs by a small margin, though.
18:06:38 <elliott> Phantom_Hoover: I haven't played GCII, so I probably wouldn't.
18:07:01 <elliott> Phantom_Hoover: OK, rephrase: I don't really like games like that.
18:07:31 <elliott> Phantom_Hoover: Oh fine, link me then.
18:07:37 <elliott> But I like the Minecraft ones partly because I know how silly he's being.
18:08:28 <Phantom_Hoover> http://www.computerandvideogames.com/article.php?id=161570&site=pcg
18:09:02 <quintopia> someone buy me a fast computer so i can play minecraft
18:09:35 <elliott> 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 <elliott> on Linux, no less, where the graphics performance isn't exactly stellar
18:09:56 <elliott> quintopia: rendering distance to short, graphics to fast, problem solved
18:10:38 <quintopia> it always ran ridiculously slow for me. i'll see about the settings.
18:10:53 <Phantom_Hoover> quintopia, and my mid-to-low end laptop runs it fine on normal rendering distance and fancy graphics.
18:10:56 <elliott> quintopia: Sometimes it does and you just have to restart it. You're not playing in-browser, right?
18:11:36 <quintopia> elliott: don't think so. haven't played in-browser since the very first demo.
18:11:55 <elliott> If you're not on Linux I can't even remotely help.
18:12:05 <elliott> 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 <elliott> It's actually pretty snappy.
18:13:00 <elliott> Phantom_Hoover: Price-wise, ignoring things that are stupidly overpriced because of a brand name (*cough* Sony *cough*)
18:13:04 <elliott> quintopia: what? you mean icedtea?
18:13:10 <elliott> that isn't a modification, that's a backport of openjdk to run java 6
18:13:22 <elliott> quintopia: uninstall the other javas and install the sun-java6-* packages on debian
18:15:00 <quintopia> pretty sure that's my default (or something close enough to it not to make a difference)
18:15:24 <elliott> quintopia: no, in fact, the difference /does/ matter
18:15:30 <elliott> openjdk, icedtea, etc. don't work or don't work as well
18:16:10 <quintopia> elliott: i'm talking about an experimental build that doesn't actually change the performance of sun's build at all
18:17:11 <elliott> quintopia: well, suit yourself
18:20:53 <Phantom_Hoover> [[So I did what I always do when I can't do anything good: I did something stupid.]]
18:21:04 <Phantom_Hoover> There's something unspeakably profound about that quote.
18:23:00 <elliott> Phantom_Hoover: Link me to the playthrough of GCII?
18:23:24 <Phantom_Hoover> <Phantom_Hoover> http://www.computerandvideogames.com/article.php?id=161570&site=pcg
18:26:00 <Phantom_Hoover> There's another one where he takes over the next size of galaxy through peaceful means.
18:30:39 <elliott> Phantom_Hoover: "Final Entry"?
18:30:41 <elliott> That doesn't look final to me.
18:30:46 <elliott> Also that site's font rendering is fucked up and hideous.
18:30:50 <elliott> Phantom_Hoover: Or rather: Where's First Entry.
18:34:27 <elliott> Phantom_Hoover: Greaaaat. And on a hideous site too.
18:34:54 <elliott> 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 <elliott> (computerandvideogames.com <-- what kind of domain name is that)
18:35:21 <Phantom_Hoover> I have a thing that guts horrible rendering on webpages and makes them vaguely readable, if that helps.
18:35:55 <Phantom_Hoover> 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:35 <elliott> Phantom_Hoover: I know, I know, Readability, yes.
18:36:42 <elliott> I can never get it looking nicely.
18:37:35 <elliott> 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:48 <elliott> Phantom_Hoover: I'm fussy.
18:38:24 <Phantom_Hoover> elliott, default layout or Readibility layout. Guess which is palatable?
18:41:53 <Vorpal> elliott, still in there?
18:42:11 <Phantom_Hoover> elliott, so can we expect Nicely Formatted Lambda Calculus soon?
18:43:20 <Vorpal> elliott, if you want me to show you the way out, that happens now, not in half a minute
18:43:32 <elliott> Phantom_Hoover: You're really irritating when you bug people. :p
18:43:43 <Vorpal> elliott, guess not then
18:52:02 <Phantom_Hoover> <elliott> 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 <elliott> Phantom_Hoover: http://upload.wikimedia.org/math/c/b/4/cb4c22a5b26892bebcca85d168d98566.png
18:52:22 <elliott> </mathisavariable, then < math >
19:00:47 <elliott> Phantom_Hoover: Sheesh, WP's LC raticle is just terrible.
19:01:16 <elliott> 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:02:12 <Phantom_Hoover> elliott, that is the problem with WP as a reference source...
19:02:39 <elliott> 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:43 <elliott> "doesn't (usually) matter"
19:02:45 <elliott> Real fucking helpful there.
19:03:41 <elliott> 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:56 -!- cheater99 has quit (Ping timeout: 250 seconds).
19:04:31 <Phantom_Hoover> I'll help in that case; I have a probably-autoconfirmed account handy.
19:04:50 <elliott> Phantom_Hoover: Undoubtedly a sockpuppet of me!
19:05:00 <elliott> Incidentally, Google Code redesigned and it's now harder to read and get information.
19:05:12 -!- pikhq has quit (Ping timeout: 265 seconds).
19:06:47 <elliott> Phantom_Hoover: Yes! Sinister.
19:07:35 * Phantom_Hoover shivers at the pure unadulterated awfulness of the design.
19:10:51 <elliott> Phantom_Hoover: Why are you even visiting those poseurs? http://adamcadre.ac/lyttle.html
19:11:09 <elliott> Congratulations, you won the Bulwer-Lytton -- you can write long sentences! Fuckfaces.
19:11:27 <elliott> Phantom_Hoover: (Presumably you already know of the Lytton Lytton, though.)
19:11:33 <elliott> (If not, READ ALL THE RESULTS NOW AND LAUGH)
19:14:18 <elliott> Phantom_Hoover: FWIW, I'm up to "Beta reduction" in the informal description.
19:14:33 -!- oerjan has joined.
19:17:09 <oerjan> 09:55:22 <Phantom_Hoover> http://www.mezzacotta.net/garfield/?comic=571
19:17:10 <oerjan> 09:55:34 <Phantom_Hoover> I feel quite intensely nerdy for getting that reference.
19:17:11 -!- cheater99 has joined.
19:18:02 <oerjan> hey i got it too, but i consider sandman to be on my _less_ nerdy side... :D
19:18:58 <oerjan> this may just be a further sign of my madness, i guess
19:23:25 <elliott> oerjan: you know the two "famous" LC encodings of data types, Church and Mogensen-Scott?
19:23:44 <oerjan> actually no. at least not the latter.
19:23:50 <elliott> oerjan: http://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding
19:26:52 <oerjan> ok the scott encoding looks like the one i consider "obvious"
19:27:50 <elliott> oerjan: presumably you know http://en.wikipedia.org/wiki/Church_encoding :p
19:28:03 <elliott> which ofc applies to more than just naturals
19:28:47 <elliott> 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:55 <elliott> cons x xs f g = g x (xs f g)
19:28:57 <elliott> and then we can define foldr
19:29:00 <elliott> foldr f z {cons x xs} = f x (xs z f)
19:29:04 <elliott> foldr f z {cons x xs} = f x (foldr f z xs)
19:29:21 <elliott> 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 <Phantom_Hoover> oerjan, wait, the Church encoding isn't the obvious one for you?
19:29:38 <elliott> Phantom_Hoover: mogensen-scott is pretty obvious for non-numeral-and-list types
19:29:45 <elliott> oerjan: and I'm just wondering how well this would work in general
19:29:57 <elliott> oerjan: hm you can define foldl with foldr right? (ignore efficiency right now :))
19:30:06 <oerjan> 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 <oerjan> but the boolean and pair examples on the Church encoding page are indeed what i'd consider obvious
19:30:57 <elliott> oerjan: how do you do that again? :p
19:31:55 <oerjan> in fact i'm wondering if that first page might have it wrong then?
19:32:33 <oerjan> true = \t f -> t, false = \t f -> f
19:32:52 <oerjan> cons x y = \f -> f x y
19:33:07 <elliott> might be so, now tell me how to define foldl with foldr :p
19:34:20 * oerjan is suddenly very hungry
19:34:25 <Phantom_Hoover> Hmm, so Mogensen-Scott for the unary naturals would be... 0 = \ c1 c2 -> c1, S = \ n c1 c2 -> c2 n?
19:34:28 <oerjan> i think you'd better as #haskell then
19:35:00 <Phantom_Hoover> I really need to find a better reference for the LC than WP...
19:36:45 <elliott> myFoldl f z xs = foldr step id xs z
19:36:45 <elliott> where step x g a = g (f a x)
19:36:51 <elliott> thanks RWH, that was so real-world of you :P
19:40:15 <elliott> Phantom_Hoover: I'm playing with this data encoding to figure out if it's a good representation of data.
19:40:30 <elliott> Phantom_Hoover: The Reduceron, for instance, represents data as functions, and doesn't use this encoding AFAIK.
19:40:50 <elliott> 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 <elliott> I'm wondering if this foldl expands to the "efficient" implementation.
19:41:53 <Phantom_Hoover> I get this steadily growing feeling that a Lazy K implementation in Haskell would be a good idea...
19:42:30 <elliott> Phantom_Hoover: Enjoy your possible space leak. :p
19:42:34 <elliott> Phantom_Hoover: But yeah, it would make things easier.
19:42:52 <Phantom_Hoover> elliott, it can't be worse than the one in the existing (C++) implementation.
19:43:07 <elliott> Phantom_Hoover: Lazy K is kinda rubbish, though; it's SKI calculus plus gimmick. :p
19:43:42 <Phantom_Hoover> elliott, well, it's SKI calculus + normal functional IO mechanism.
19:44:02 <elliott> Phantom_Hoover: Plus syntax gimmick.
19:46:07 <Phantom_Hoover> I still ponder the sanity of someone who thinks "SKI calculus implementation? C++ is the perfect language!".
19:50:18 <elliott> 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:51:38 <Phantom_Hoover> The worst part is that you cannot pronounce any of those names.
19:52:14 <elliott> Phantom_Hoover: I've renamed them to disambiguate :P
19:53:09 <elliott> 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 <elliott> So I can simplify these things step by step without making stupid mistakes.
19:53:44 <Phantom_Hoover> elliott, you mean handling code as code rather than text?
19:55:11 <elliott> foldl fl zl xsl = foldr (\xq gq aq -> gq (fl aq xq)) (\xi -> xi) xsl zl
19:55:13 <elliott> foldl f z {cons x xs} = foldl f (f z x) xs
19:55:42 <elliott> What I'm saying is: The right-fold data structure representation supports foldl perfectly well.
19:55:46 <elliott> (With a sufficiently smart CPU :P)
20:00:42 <elliott> Phantom_Hoover: I am not sure how this works with mutually-recursive data types and the like :(
20:01:59 <elliott> Phantom_Hoover: I guess I'll just go with the induction schemes.
20:03:28 <elliott> "TIL That Linus Torvalds also created Git, so much cooler now"
20:06:19 <elliott> Phantom_Hoover: That's on /r/programming's front page.
20:06:31 <elliott> It has finally ceased to be worthwhile even in the slightest.
20:07:47 <Phantom_Hoover> elliott, "What do Java developers think of Scala?" I sense the invisible hand of Sgeo!
20:08:21 <elliott> I remember when git was low-level and you had to use cogito to get anything done.
20:13:11 <elliott> Phantom_Hoover: Dude, it was 2006 :P
20:13:52 <Phantom_Hoover> Back then I could write Hello World in Pascal and that was IT!
20:18:02 <elliott> fun (T : Type) (P : Tree T -> Set) => Tree_rect T P
20:18:02 <elliott> : forall (T : Type) (P : Tree T -> Set),
20:18:02 <elliott> (forall t : T, P (Leaf T t)) ->
20:21:11 <elliott> Phantom_Hoover: No, I was just trying to get a tree's recursive induction scheme.
20:21:16 <elliott> Since Coq is :oohdependent:, it hasn't helped much.
20:24:03 <elliott> Branch x y f g = g (x f g) (y f g)
20:24:56 <elliott> mapTree f t = foldTree f Branch
20:25:23 <elliott> mapTree f t = foldTree f Branch t
20:25:54 <elliott> mapTree f t = foldTree (Leaf . f) Branch t
20:26:48 <elliott> mapTree f {Leaf x} = Leaf (f x)
20:26:49 <elliott> mapTree f {Branch x y} = Branch (mapTree f x) (mapTree f y)
20:31:11 <elliott> map f {cons x xs} = cons (f x) (map f xs)
20:31:16 <elliott> Phantom_Hoover: these things really expand properly!
20:40:39 <elliott> Phantom_Hoover: Have you looked at the Reduceron?
20:40:43 <elliott> It may restore your faith in electrons.
20:40:48 <elliott> Phantom_Hoover: http://www.cs.york.ac.uk/fp/reduceron/
20:41:10 <elliott> Phantom_Hoover: tl;dr purely functional, lazy graph rewriting on an FPGA.
20:41:29 <oerjan> electrons, traitorous little schemers
20:41:31 <elliott> Phantom_Hoover: Yes, it does have IO of some kind.
20:41:34 <elliott> Well, it has O. Dunno about I.
20:41:43 <elliott> It's irrelevant though, just gawp at the amazingness and read the lovely memos.
20:54:42 <elliott> Phantom_Hoover: Oops, I just realised my tree structure was (Leaf X | Branch Tree Tree), which is rather useless.
20:54:54 <elliott> It should be (Leaf | Branch X Tree Tree).
20:59:18 <elliott> mapTree f {Branch x t1 t2} = Branch (f x) (mapTree f t1) (mapTree f t2)
21:05:35 <Vorpal> elliott, idea: redstone message bus (think CAN)
21:05:52 <Vorpal> elliott, doable or not?
21:06:02 -!- hagb4rd has joined.
21:06:08 <Vorpal> well presumably doable considering the CPU
21:08:29 <Gregor> `addquote <Anti-X> 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 <HackEgo> 241) <Anti-X> 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 <Gregor> hagb4rd: "hi@all" isn't likely to elicit much of a reaction, except for elliott mistabbing you :P
21:10:59 <elliott> <HackEgo> 241) <Anti-X> 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:11:13 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.28706
21:11:20 <elliott> Gregor: I can't believe my new quote system isn't 17x as efficient as the old one :P
21:11:27 <elliott> Your bot spends SO MUCH TIME doing ABSOLUTELY NOTHING OF VALUE X-D
21:12:23 <elliott> 231) <elliott> Wow, that [ ! "$1" ] actually works.
21:12:26 <elliott> Why is that even in the database.
21:14:48 <oerjan> `addquote <elliott> ONLY GOOD QUOTES PLEASE! AND NO FAKE ONES EITHER!
21:14:49 <HackEgo> 241) <elliott> ONLY GOOD QUOTES PLEASE! AND NO FAKE ONES EITHER!
21:15:07 <Phantom_Hoover> HOLY CRAP MY PARENTS ARE WATCHING SELTZER AND FRIEDBERG AND LAUGHING I'M GOING TO UNIVERSITY NOW AND NEVER COMING BACK
21:15:32 <elliott> `addquote IN AN ALTERNATE UNIVERSE THAT IS THIS ONE: <oerjan> The mother of my children is a goat!
21:16:49 <Phantom_Hoover> elliott, AAAAAAAAAAAA ALL MY GENES ARE THEIRS AAAAAAAAAAAAAAAAAAAAAAAA
21:17:25 <Gregor> I think I need a fuse-hg.
21:17:31 <elliott> Phantom_Hoover: Don't worry! It is theoretically possible that every single gene you have mutated!
21:17:37 <elliott> You could share NO genes with them!
21:17:41 <Gregor> hg clone-ing a large repository is (sometimes) quite slow >_>
21:17:47 <HackEgo> 242) IN AN ALTERNATE UNIVERSE THAT IS THIS ONE: <oerjan> The mother of my children is a goat!
21:17:48 <Gregor> Or at least, inconsistent-speed.
21:18:05 <elliott> Gregor: Is "fuse-hg" meant to be something more interesting than a FUSE interface to hg?
21:22:03 <HackEgo> 129) <soupdragon> 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 <soupdragon> ^ I learned that trick from atheists
21:22:57 <elliott> it's vaguely irritating that fax was an interesting cool person and an utterly insane psycho in one
21:26:43 <elliott> hmph, what's foldl on a tree..
21:27:32 <oerjan> elliott: i'm not sure that makes sense
21:27:51 <elliott> oerjan: me neither, but i *want* it to make sense :)
21:27:56 <elliott> Deewiant: bad Deewiant *slaps*
21:28:15 <elliott> -- foldlTree f z (Branch x t1 t2) = foldlTree (f (foldlTree f z t1) x) t2
21:28:18 <elliott> oerjan: i think that *sort* of works
21:28:32 <oerjan> i mean a tree is basically a way to correct for a list's biased direction-ness...
21:28:39 <elliott> so really there's foldlTreeLeft and foldlTreeRight
21:28:47 <elliott> where you just swap t1 and t2 there
21:28:51 <elliott> Gregor: hm? were you saying yes to my definition?
21:29:28 <oerjan> note that for a list, a foldl is equivalent to a foldr of the reversed list
21:29:39 <Gregor> elliott: To fuse-hg :P
21:30:10 <oerjan> however if you reverse/mirror a tree, you still use the same fold
21:30:12 <elliott> Gregor: What would it be, then? (Suggest rename to hg-fuse, for consistency.)
21:30:13 <Gregor> 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 <oerjan> (with tweaked parameters)
21:30:42 <elliott> Gregor: I was saying: is it more interesting than FUSE? As in: did you mean "fuse" the verb?
21:30:46 <elliott> As in fuse two hg repositories together in some way?
21:30:48 <elliott> That would be interesting.
21:32:32 <elliott> oerjan: give me a tree operation other than fold and map, then :P
21:32:46 <oerjan> elliott: monad operations!
21:32:47 <elliott> to write in terms of foldr and expand back
21:32:55 <elliott> oerjan: oh gawd -- what are they on trees?
21:33:26 <oerjan> well return x is just Branch x Leaf Leaf i think
21:33:52 <elliott> 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 <oerjan> 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 <elliott> oerjan: eh? (Leaf X | Branch Tree Tree) you mean as the alternative?
21:38:33 <oerjan> what should join (Branch (Branch x t1 t2) t3 t4) be
21:38:37 <elliott> I had that at first, but then realised it doesn't model actual trees
21:38:44 <elliott> (Leaf X | Branch X Tree Tree)?
21:39:03 <oerjan> the former has an obvious monad instance, at least
21:39:22 <oerjan> the latter may not actually help in that respect
21:39:37 <Phantom_Hoover> Gyaaah, where's pikhq when you need him and his multimedia nerdery.
21:41:08 <elliott> Phantom_Hoover: I have some of it.
21:41:16 <elliott> oerjan: erm but how do you model an "actual" tree with the former?
21:42:31 <oerjan> elliott: oh forget that
21:42:47 <elliott> oerjan: but then it's hardly a tree structure, is it?
21:42:51 <elliott> oerjan: oh or do you mean, forget what i said
21:42:54 <elliott> Phantom_Hoover: no, I can help
21:43:05 <elliott> Phantom_Hoover: pretend i'm pikhq, i'm as much an encoding nerd as he is :)
21:43:26 <oerjan> elliott is in fact pikhq converted to big5
21:43:29 <Phantom_Hoover> elliott, http://torrentz.eu/search?f=futurama+season+3
21:43:36 <oerjan> or wait, that's the wrong way around
21:44:01 <Vorpal> elliott, I have an idea how to make that "clear" one work. Involves one SR-latch and two buttons
21:44:21 <elliott> Phantom_Hoover: http://torrentz.com/7f97cf9ea5ff10a01b56789c85ce32e3c8a24674 This is the best one out of the first few.
21:44:33 <elliott> Phantom_Hoover: 11 seeders, 10 peers. Should go quickly enough.
21:45:00 <elliott> Phantom_Hoover: There is a preferable 8 gig Matroska rip, but it is seederless.
21:45:42 <elliott> Phantom_Hoover: You can't tell without downloading.
21:46:03 <elliott> 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 <Phantom_Hoover> elliott, I mean in the sense of "what would be the kind of order of magnitude you'd expect"?
21:46:28 <elliott> Phantom_Hoover: A few hours if stuff is good.
21:47:24 <elliott> Phantom_Hoover: Did you add the trackers?
21:47:30 <elliott> Did you *wait* because this stuff takes time to propagate?
21:47:46 <elliott> Phantom_Hoover: No you didn't.
21:47:57 <elliott> Phantom_Hoover: You did add them with a blank line in between, yes?
21:48:18 <elliott> Phantom_Hoover: Give it some minutes.
21:48:38 <Phantom_Hoover> And I am looking at the tracker list right now and two of them have 1 peer listed each.
21:49:30 <elliott> Phantom_Hoover: OK, I realise you don't get how BitTorrent works, but stop looking at it and go back in five minutes.
21:53:10 <elliott> oerjan: so wait what's the preferable tree structure again :D
21:53:17 <oerjan> YOU NEED TO IMPROVE YOUR COOKING SKILLS
21:53:45 <oerjan> elliott: nothing wrong with your original, is there
21:53:56 <elliott> oerjan: you mean Tree = Leaf | Branch X Tree Tree?
21:54:05 <elliott> oerjan: right, so what's join :D
21:54:51 <elliott> oerjan: now i need to find the monad laws as phrased for join :p
21:55:11 <elliott> oerjan: now i need a winning lottery ticket
21:55:16 <elliott> (if it worked once, it's worth trying again!)
21:58:03 <elliott> oerjan: join . return == id
21:58:04 <elliott> join . join == join . fmap join
21:58:20 <elliott> oerjan: wait do you need fmap to do a monad? doesn't join/return suffice
21:59:00 <Phantom_Hoover> elliott, you need it in some capacity, since >>= can't be expressed in terms of join and return alone.
21:59:26 <elliott> ok well I have treeMap so that's sorted
21:59:37 <elliott> oerjan: ok so obviously "join (Branch x Leaf Leaf) = x" :)
22:01:30 <Phantom_Hoover> I wish cpressey was here so I could torment him with both monads AND pointfree style!
22:03:18 <oerjan> 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 <elliott> 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 <elliott> as in when someone says "oh yeah i solved this problem using a TREE", i can't imagine them using that
22:06:32 -!- Sasha has quit (Ping timeout: 245 seconds).
22:06:40 <elliott> oerjan: Initially, I thought this was going to be about even plainer binary
22:06:40 <elliott> data Tree a = Branch (Tree a) (Tree a) | Leaf a
22:06:50 <oerjan> 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 <elliott> lesson: #esoteric is unable to avoid itself
22:06:57 <elliott> <oerjan> 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:07:20 <oerjan> elliott: um clarkstone doesn't ring a bell
22:07:30 <elliott> oerjan: Simon Richard Clarkstone = SimonRC
22:07:33 -!- Sasha has joined.
22:07:40 <elliott> /whois if you want to check (also note present in #haskell too)
22:07:45 <elliott> also i remember his sig :)
22:07:51 <elliott> oerjan: so would you recommend I just go for the ultra-plain binary tree route for the sake of algorithmic purity :)
22:07:52 <Phantom_Hoover> * [SimonRC] (~sc@fof.durge.org): Simon Richard Clarkstone
22:08:10 <oerjan> weird, i thought his surname was something different
22:10:34 <oerjan> 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:28 <oerjan> the combined one above
22:11:55 <elliott> oerjan: wait since when does Tree have two type parameters
22:12:09 <oerjan> elliott: in the combined version it does
22:12:23 <elliott> oerjan: we're doing the (Leaf X | Branch Tree Tree) version now, I've decided :P
22:12:27 <oerjan> you allow different types for values in branches and in leaves
22:12:38 <oerjan> elliott: ok in that case just ignore the a's
22:14:37 <elliott> tree :: Tree (Tree a) -> Tree a
22:14:42 <elliott> oerjan: oh that's rather easy then isn't it
22:14:46 <elliott> oerjan: we just want to s/Leaf x/x/
22:15:02 <elliott> join (Leaf x) = x; join (Branch t1 t2) = Branch (join t1) (join t2)
22:15:47 <elliott> oerjan: and thus joinTree = foldTree Branch id
22:15:51 <Phantom_Hoover> Incidentally, I found out why Coq files have a .v suffix: it's short for "vernacular".
22:16:16 <elliott> Phantom_Hoover: Insert lewd reference to Coq's name and word beginning with V.
22:16:24 <elliott> Insert me being swatted by oerjan.
22:17:14 <oerjan> imagine if this subreddit actually were highly active http://www.reddit.com/r/correctionsdept/
22:17:34 <elliott> oerjan: "there doesn't seem to be anything here" - ha, ha, ha
22:18:00 <elliott> hm so wait how do you do bind in terms of fmap and join?
22:18:32 <oerjan> it's no fair to type my lines before me!
22:19:32 <oerjan> (btw it was linked from http://www.reddit.com/r/technology/comments/ek22q/reddit_now_creates_the_news_the_ciapsyteknet/)
22:22:36 <Phantom_Hoover> elliott, oerjan, I said that about 15 minutes before either of you.
22:23:28 <oerjan> Phantom_Hoover: well your time-traveling ways aren't fair either!
22:24:23 <oerjan> Phantom_Hoover: um no i don't think that's right
22:24:46 <elliott> progress so far simplifying bind:
22:24:47 <elliott> bindTree {Branch t1 t2} f = Branch (((mapTree f t1) (\x -> x) Branch)) (((mapTree f t2) (\x -> x) Branch))
22:25:45 <oerjan> (>>=) = flip $ (join .) . fmap
22:26:44 <oerjan> you were trying to use . with a two-argument function
22:26:44 <elliott> oerjan: go ask for lambdabot again :D
22:26:50 <elliott> Phantom_Hoover: *not* you, you're not nice and persuasive
22:26:55 <oerjan> elliott: i didn't do it the first time
22:27:03 <elliott> oerjan: which is why you're the best person to do it now!
22:27:08 <elliott> oerjan: nobody's sick of you yet
22:27:53 <elliott> Phantom_Hoover: Yes, but when you asked, it disappeared soon after.
22:28:00 <elliott> When I (IIRC) asked gwern it didn't.
22:28:08 <elliott> What I'm sayin' is: you're not sweet enough :P
22:28:42 <elliott> oerjan: just use puppy dog eyes
22:29:42 <oerjan> elliott: it probably disappears whenever lambdabot quits, regardless. sheesh.
22:30:05 <elliott> oerjan: it didn't last time, iirc it was added to the list :) i may be wrong though
22:30:22 <elliott> oerjan: anyway go ask! you can prolly use your haskell report credentials to make ridiculous demands or sth
22:30:25 <elliott> bindTree {Branch t1 t2} f = Branch (bindTree t1 f) (bindTree t2 f)
22:30:28 <oerjan> if it was added to the list why did it disappear again?
22:30:38 <elliott> Phantom_Hoover: It's just map.
22:30:42 <elliott> mapTree f {Leaf x} = Leaf (f x)
22:30:42 <elliott> mapTree f {Branch t1 t2} = Branch (mapTree f t1) (mapTree f t2)
22:30:45 <elliott> mapTree f t = foldTree Branch (Leaf . f)
22:30:49 <elliott> oerjan: who knows? I think it changed servers at one point or something
22:30:56 <elliott> oerjan: Lemmih is the current guy-to-bug.
22:33:05 <elliott> http://sprunge.us/UiAY here's my working out of all of this
22:33:10 <elliott> :: precedes a block that's equivalent
22:34:30 <olsner> foldl = xqgqaqgqflaqxqzl
22:34:32 <elliott> Phantom_Hoover: Read it like this:
22:34:47 <elliott> foldl f z xs = foldr (\x g a -> g (f a x)) (\x -> x) xs z
22:34:55 <elliott> The suffixes on the variables were added because I ran into alpha-renaming issues.
22:35:13 <elliott> This is why I need a manual-but-automated rewriter tool. :p
22:37:50 <elliott> Would anyone like a copy of my GLORIOUS EYE-CURING GNOME THEME?
22:44:29 <elliott> Phantom_Hoover: Generally, yes.
22:45:21 <Phantom_Hoover> 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 <elliott> Phantom_Hoover: The implicit argument system is nicer than Agda's, at least.
22:46:12 <elliott> Phantom_Hoover: Would you like my WONDERFUL GNOME THEME?
22:46:28 <Phantom_Hoover> WHY IS IT SO "£$%"£$%ING *HARD* TO MAKE ID A FUNCTION?
22:46:51 <elliott> Phantom_Hoover: Definition id x := x.
22:47:05 <elliott> Phantom_Hoover: Definition id {A} (x : A) := x.
22:47:20 <elliott> Coq < Definition id {A} (x : A) := x.
22:47:22 <elliott> Phantom_Hoover: Yes it is.
22:47:57 <elliott> [[Case expressions can be removed by defining data constructors as
22:47:58 <elliott> functions and transforming case expressions to function applications.]]
22:48:10 <elliott> hey they stole Church's and Mogensen's and Scott's and my idea :)
22:48:15 <elliott> Phantom_Hoover: And? How is id not a function?
22:48:35 <Phantom_Hoover> fmap [elided or not actually there depending on what's set] id is a type error.
22:49:03 <elliott> Phantom_Hoover: OK, please give me the full definition of fmap.
22:49:13 <elliott> Phantom_Hoover: OK, please give me the full definition of fmap.
22:49:36 <elliott> Phantom_Hoover: OK, please give me the full definition of fmap.
22:49:44 <elliott> I have done monads in Coq before.
22:50:00 <Phantom_Hoover> Fixpoint fmap (A B : Set) (f : A -> B) (t : tree A) : tree B := [elided].
22:50:21 <elliott> Phantom_Hoover: Definition of tree, please.
22:50:27 <elliott> I can just make it an axiom.
22:51:57 <Phantom_Hoover> Essentially, I'm told that fmap id is an error as id : ID rather than * -> *.
22:52:16 <elliott> Phantom_Hoover: Yes, because the values of A and B are not clear.
22:52:26 <elliott> Phantom_Hoover: You might want to try using {A B : Set} in fmap.
22:52:38 <elliott> Failing that... just give A as a parameter, and forall A in the scope you're in.
22:52:47 <elliott> <elliott> Failing that... just give A as a parameter, and forall A in the scope you're in.
22:53:40 <elliott> Coq < Axiom tree : Set -> Set.
22:53:40 <elliott> Coq < Axiom fmap : forall (A B : Set) (f : A -> B) (t : tree A), tree B.
22:53:40 <elliott> Coq < Definition id {A} (x : A) := x.
22:53:50 <elliott> : forall A : Set, tree A -> tree A
22:53:52 <elliott> Phantom_Hoover: You did something wrong, then.
22:54:11 <Phantom_Hoover> Right, so I have to actually *define my own id* because Coq's definition is idiotic?
22:54:46 <elliott> Phantom_Hoover: I forgot Coq has its own.
22:55:23 -!- zzo38 has joined.
22:55:33 <elliott> Coq < Definition fmap_id (A : Set) (t : tree A) : tree A := fmap A A (id (A:=A)) t.
22:55:42 <elliott> Phantom_Hoover: Was that so hard?
22:55:51 <elliott> If an implicit parameter can't be inferred, just specify it with (paramname:=val).
22:56:12 <elliott> How I found out what name to use:
22:56:16 <elliott> ID = forall A : Type, A -> A
22:57:31 <elliott> Phantom_Hoover: I refuse to believe it discriminates against you and refuses to execute the same code that works for me.
22:57:49 <elliott> 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 <Phantom_Hoover> elliott, well, sans the (A := A) which is the silly part I couldn't remember.
22:58:06 <zzo38> "also, for future reference, spambots, <http> 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 <elliott> Phantom_Hoover: The silly part? That's the important part.
22:58:34 <elliott> 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 <elliott> 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 <elliott> Phantom_Hoover: The reliable way to specify implicit type parameters is with (name:=val).
22:59:13 <elliott> 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 <elliott> It could be (A:=WhatARandomNameToGiveASet).
22:59:50 <Phantom_Hoover> 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 <elliott> Phantom_Hoover: Because in all the /other/ cases, it works fine.
23:00:37 <elliott> 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 <Phantom_Hoover> elliott, you mean those in which id is not being passed to other functions?
23:01:02 <elliott> Phantom_Hoover: No, you can pass id to other functions easily; just not to functions you're using polymorphically.
23:01:14 <elliott> (Or some condition roughly like that.)
23:01:22 <zzo38> 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 <elliott> 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 <zzo38> 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 <elliott> zzo38: That seems... interesting.
23:06:19 <elliott> An automatic bug-fixer? :p
23:06:23 <elliott> Phantom_Hoover: Would you like my GNOME THEME?!?!?1i19037248957yj
23:06:59 <Phantom_Hoover> elliott, does it shrilly scream about type errors constantly?
23:07:56 <elliott> Phantom_Hoover: NOPE! That's the best feature!
23:08:02 <zzo38> 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:14 <elliott> 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 <pikhq> Every video encoder sucks.
23:08:49 <elliott> 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 <pikhq> I cannot figure out *any* way to properly encode mixed framerate video.
23:09:37 <pikhq> 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 <elliott> Phantom_Hoover: http://filebin.ca/qkmtx/Kimono.zip
23:10:44 <pikhq> If I could perhaps write a timestamp-generating inverse telecine filter + deinterlacer, I could just barely get it going right.
23:10:47 <elliott> Phantom_Hoover: Install by selecting the zip in Appearance → Install...
23:11:02 <elliott> Phantom_Hoover: Fonts to set: Application font = Droid Sans, Document font = Sans,
23:11:14 <elliott> *Sans; Window title font = Droid Sans Bold
23:11:17 <elliott> Fixed width font = Droid Sans Mono
23:11:21 <elliott> All 10 except Window title, which should be 11.
23:11:35 <elliott> And set your DPI write in details, too. (http://members.ping.de/~sven/dpi.html to calculate)
23:11:43 <elliott> Well, okay, so the DPI thing is optional.
23:12:18 <elliott> 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 <elliott> 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 <elliott> Phantom_Hoover: wget it and dpkg -i it.
23:12:49 <elliott> Oh, and I apologise to pikhq for making a theme that isn't Grey Mist.
23:12:50 <pikhq> 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 <pikhq> elliott: Screenshot?
23:13:37 <zzo38> Or possibly if you suppress some error messages, even.
23:14:12 <Phantom_Hoover> elliott, erm, Appearance expects something called a theme file and complains about the zip.
23:14:25 <elliott> Phantom_Hoover: I'll reupload in a second.
23:14:26 <elliott> pikhq: http://imgur.com/GIKWc.png (Phantom_Hoover too)
23:14:33 <elliott> pikhq: (If you think the fonts are huge, consider that my display is 120 ppi.)
23:15:16 <elliott> It's Good, but it means fonts will look huge for people on less Good displays. :p
23:15:23 <elliott> (i.e. desktop displays or not-as-small laptops)
23:15:28 <elliott> Phantom_Hoover: Still want it after seeing THE HIDEOUS SCREENSHOT?
23:16:15 <pikhq> elliott: Insufficiently Grey. And insufficiently Mist.
23:16:17 <elliott> Now pikhq will yell at me for the fact that it has a gradient.
23:17:23 <elliott> pikhq: Looking at it, I guess it actually just shows that, deep down, I still like Bluecurve. :P
23:18:29 <Phantom_Hoover> Is there an easy way of expressing function composition in Coq?
23:19:16 <zzo38> I think another use of getting these message from compiler to automatically change things, might also include linker errors, if needed.
23:19:31 <elliott> Phantom_Hoover: http://coq.inria.fr/library/Coq.Program.Basics.html
23:19:34 <elliott> Notation " g ∘ f " := (compose g f)
23:19:35 <elliott> (at level 40, left associativity) : program_scope.
23:19:49 <elliott> Phantom_Hoover: You may want to define your own notation for it that is less Unicodey.
23:20:35 <Phantom_Hoover> Funnily enough, compose is not a defined object for me.
23:21:03 <elliott> Phantom_Hoover: "Library Coq.Program.Basics"
23:21:07 <elliott> Phantom_Hoover: Require Import Coq.Program.Basics.
23:21:31 <elliott> Phantom_Hoover: (Or Require Import Program.Basics or Require Import Basics.)
23:21:56 <elliott> Phantom_Hoover: What about it?
23:22:11 <elliott> 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 <elliott> Which, of course, is what you should do all the time when correcting things...
23:22:33 <elliott> C-c C-u to unevaluate the previous statement, I think ... but I've forgotten.
23:24:41 <Phantom_Hoover> elliott, so Require Import Foo.Bar. will evaluate as soon as I type the "." after Foo.
23:25:51 <elliott> Phantom_Hoover: Ohh, I see what you mean.
23:26:21 <elliott> "# See the Proof General Eclipse wiki for screenshots of Proof General in Eclipse."
23:31:02 <elliott> Phantom_Hoover: What are you writing in Coq?
23:31:58 <elliott> Phantom_Hoover: Which is intended to be?
23:33:05 <elliott> Phantom_Hoover: Oh, sprunge your code. :p
23:33:37 -!- MigoMipo has quit (Ping timeout: 260 seconds).
23:35:25 <elliott> Phantom_Hoover: I'd prefer to laugh at your Coq.
23:35:30 <elliott> Considering extraction removes all the interesting dependency.
23:35:37 <oerjan> the monad of incompetence
23:35:58 <oerjan> finally a good use for strict encapsulation
23:36:19 <Phantom_Hoover> 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 <Phantom_Hoover> With "type intros. Type induction and a variable name." stuck in for good measure.
23:40:16 <elliott> Phantom_Hoover: If rewrite is your most common tactic, ur doin it rong.
23:40:32 <elliott> Phantom_Hoover: BTW, Proof General can list all the tactics in the system (there's fewer than you think).
23:40:37 <elliott> Just TAB on that and pick a likely one. :p
23:41:41 <elliott> Phantom_Hoover: I'm just trying to help.
23:44:28 <Phantom_Hoover> But seriously; I've never had occasion to do anything interesting enough to invest time into properly learning Coq.
23:46:39 <elliott> Phantom_Hoover: Do what me and fax were trying to do, replace the standard library.
23:46:54 <elliott> Phantom_Hoover: (Try starting with category theory; there's a wonderful paper about embedding it into Coq, absolutely wonderful.)
23:47:04 <elliott> If you can't get the algebraic structures down, you lose.
23:47:07 <elliott> Phantom_Hoover: You sign up by doing it!
23:47:14 <elliott> Phantom_Hoover: Er, there's some option to Coq to tell it to forget the stdlib exists.
23:47:26 -!- Sasha2 has joined.
23:47:33 <elliott> i note that fax disappeared from the internet right after oerjan banned it
23:47:51 <elliott> *** coq-prog-args: ("-emacs-U" "-nois") ***
23:47:54 <oerjan> ...i've seen fax on freenode since then
23:47:59 <elliott> Phantom_Hoover: Put that at the end of your file... or the top, I forget.
23:48:05 <elliott> oerjan: Well, okay, stopped posting to reddit. And its blog.
23:48:07 <Phantom_Hoover> Also, I think you misunderestimate how weirdly uneven my understanding of things.
23:48:17 <elliott> Phantom_Hoover: Try the bottom. Yes, the bottom.
23:48:24 -!- Sasha has quit (Ping timeout: 240 seconds).
23:49:18 <elliott> Phantom_Hoover: http://sqig.math.ist.utl.pt/pub/CarvalhoA/98-C-DiplomaThesis/maintext.ps
23:49:21 <elliott> Phantom_Hoover: (One version of) the lovely paper.
23:49:45 <Phantom_Hoover> elliott, did I mention that I don't know any category theory?
23:49:54 <elliott> Phantom_Hoover: You don't really have to. :p
23:50:39 <elliott> 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 <elliott> Phantom_Hoover: Then you get to the cat of small cats -- sorry, category of small categories -- and shit goes crazy.
23:51:02 <elliott> I think oerjan can agree with the part of my explanation that involves shit going crazy.
23:51:19 <elliott> Phantom_Hoover: Also morphisms and monoids and monads.
23:52:02 <oerjan> and topoi. or so i hear.
23:52:20 <elliott> oerjan: i never got that far :D