00:00:34 GEB is what happens when a smart person has some kind of mental blockage that makes them consider recursion amazing. 00:00:51 elliott: and Penrose 00:00:52 elliott, it's like whoa. 00:01:05 j-invariant: Penrose should just be ... forced to shut up forever? 00:01:10 LOL 00:01:10 j-invariant: like a restraining order 00:01:14 he can't publish any books any more 00:01:17 Penrose is crazy too? 00:01:20 elliott: the problem with Penrose is he's a really smart guy 00:01:33 he just has this one absolutely idiotic idea that he talks about sometimes 00:01:39 Phantom_Hoover: he thinks that intelligent life is immortal because the universe's maximum state of entropy has all information or something 00:01:44 ??? I don't know, I can't explain crazy people 00:01:45 I think Hofstader also knows his stuff 00:01:45 j-invariant: yeah 00:01:53 j-invariant: the smarter someone gets, I think, the more likely they are to have one really stupid idea 00:01:59 and be unable to see how stupid it is 00:02:03 yeah 00:02:05 like einstein 00:02:16 coppro, which crazy idea did he have? 00:02:19 oh yeah einstein with that stupid "relativity" stuff 00:02:20 coppro: yeah what was that fucker thinking with realtivity 00:02:22 *relativity 00:02:25 j-invariant: *high5* 00:02:27 :D 00:02:40 Phantom_Hoover: spooky action at a distance 00:03:04 that's my favourite name of anyhting really 00:03:05 isn't the non-existence of action at a distance a direct consequence of relativity? 00:03:10 spooky action at a distance 00:03:15 it's just ... the best name 00:03:15 j-invariant: well, you'd think 00:03:32 http://en.wikipedia.org/wiki/Action_at_a_distance_(physics) i bet this was renamed from the proper name by wikilamers 00:03:36 j-invariant: but Einstein also developed the first inklings of quantum theory 00:03:46 GOTT DOST NOT PLAY DIECE 00:03:49 exactly 00:04:10 he hated quantum theory because of its implications 00:04:17 he was too hung up on dumb concepts 00:04:30 despite having given the insight which led to the 00:04:31 *them 00:05:23 gödel's really stupid idea was that he was being poisoned, but that one resolved itself quite quickly :D 00:05:25 aww that was an awful thing to say 00:05:28 i'm such a bad person 00:05:57 GÖDEL'S GHOST FROWNS ON YOU 00:06:08 MAY ALL YOUR THEOREMS BE UNDECIDABLE 00:06:09 gödel's skeletal ghost 00:07:04 Vorpal: OS X — 96 gigs; Ubuntu — 56 gigs; Shared — 96 gigs 00:07:10 Vorpal: dunno whether those are decimal are binary gbs but who cares 00:07:13 does this look reasonable? 00:07:26 my school has a course that includes undecidability 00:07:30 I've heard it's kind of boring :( 00:07:40 I can resize the OS X one at any time really, but 00:08:18 elliott, no it doesn't 00:08:24 elliott, too much of OS X :P 00:08:34 Vorpal: aside from zealotry. 00:08:37 w/in 25 00:08:38 but since you can resize it again, sure 00:08:40 OS X takes up more space, simple fact 00:08:46 Vorpal: yeah but i'd have to get rid of ubuntu/shared 00:08:55 elliott, what? 00:09:01 Vorpal: because this takes up the whole disk 00:09:05 elliott, couldn't you add shared-2 00:09:06 or such 00:09:12 Vorpal: you mean shrink OS X? 00:09:15 elliott, yes 00:09:17 I doubt i'll want to give less to OS X 00:09:20 elliott, ah 00:09:25 considering there's only 50 gigs free on there as it stands 00:09:33 elliott, aren't there shrinkable linux file systems? 00:09:35 56 gigs for ubuntu might be too little? probably not 00:09:41 Vorpal: probably. i'm just going to go with ubuntu default 00:09:58 elliott, not sure how much ubuntu need 00:10:03 du -sh /usr might take a while 00:10:12 Vorpal: well as fizzie said his ubuntu install only uses about 10 gigs. 00:10:16 on my arch system: 00:10:18 $ df -h /usr/ 00:10:18 Filesystem Size Used Avail Use% Mounted on 00:10:18 /dev/mapper/array-usr 00:10:18 20G 8,5G 11G 46% /usr 00:10:21 Vorpal: but there's /home in these too, just things like music will go on shared 00:10:24 and also probably code? 00:10:34 elliott, well my /home : 00:10:41 Filesystem Size Used Avail Use% Mounted on 00:10:41 /dev/mapper/array-home 00:10:41 69G 59G 7,4G 89% /home 00:10:48 89% !? 00:10:50 lol 00:10:54 I guess I'll have to grow it 00:10:55 again 00:11:01 long live LVM! 00:11:01 yes, yes, I /am/ planning to buy my big desktop system. 00:11:19 elliott, you here see the wonder of LVM! 00:11:19 Vorpal: I'd like it if there was some kind of standard thing like a slimmed down LVM ... with saner nomenclature and tools. 00:11:30 Vorpal: and if all filesystems supported resizing. online resizing. 00:11:43 elliott, well actually jfs supports on line growing 00:11:46 Vorpal: but, uh, LVM has the wondrous feature of interoperating with NOTHING 00:11:55 want to just LOOK at your files in another OS? SORYYYYY 00:11:58 elliott, so does ext4 iirc 00:12:08 Vorpal: yeah. well. i'm not making my shared partition ext4 00:12:10 elliott, lvm for fuse? DO IT NOW! 00:12:16 fuck no 00:12:25 elliott, I think ext3 supports resizing too 00:12:28 online I mean 00:12:52 elliott, anyway I doubt I will change from linux on my destop 00:12:55 Fuck it, I'm resizing. If I decide it's all wrong I'll trash ubuntu & shared and redo it. 00:12:55 desktop* 00:13:07 elliott, what about swap 00:13:07 Vorpal: um hello @? (okay so @ won't interact with anything else either :-)) 00:13:14 Vorpal: I don't need swap, I have four gigabytes of RAM 00:13:22 elliott, you can't suspend to disk then 00:13:27 Vorpal: Sure you can with a swap file. 00:13:32 ... right 00:13:52 Vorpal: OK, fine, I'll make room for a six gig swap. 00:13:54 elliott, it's a blood drop 00:13:54 elliott, separate /boot I guess? 00:13:56 -!- wareya has joined. 00:14:03 elliott, needs to be 60 MB or less 00:14:16 (well it could be larger) 00:14:17 * Sgeo finished Braid 00:14:24 (would be a waste though) 00:14:29 Vorpal: why separate /boot. 00:14:43 elliott, well depends on if your bootloader can handle the main fs 00:15:18 elliott, I guess you need to install bootloader into partition rather than into mbr on that computer 00:15:20 elliott, no? 00:15:34 $ du -sh /usr/ 00:15:34 7,6G /usr/ 00:15:36 from thinkpad 00:16:09 /var contains a few chroots 00:16:13 so pointless to check 00:16:23 -!- elliott has quit (Remote host closed the connection). 00:16:58 -!- elliott has joined. 00:17:00 Wow. 00:17:03 That resize was quick. 00:17:06 Wonder why LimeChat crashed. 00:17:12 (Resize and partition, no less.) 00:17:24 OK, now I need to put GRUB on the shared partition. 00:17:40 You can install GRUB from OS X right? ...right? 00:18:05 hmm 00:18:11 can you download "GRUB 2 images" or something? 00:18:16 I wouldn't count on it: :) 00:18:51 oh come on, i have to :P 00:19:56 -!- variable has quit (Read error: Operation timed out). 00:20:55 configure: error: objconv not found which is required when building with apple compiler 00:21:02 olsner: grub can build on os x apparently? 00:21:43 -!- variable has joined. 00:22:01 sure, but isn't it heaps easier to do this from ubuntu once you install it? :) 00:22:08 00:21 < c_wraith> (I have goldbach's conjecture in formal logic as a tattoo) 00:22:10 olsner: i need grub to install it. 00:22:19 j-invariant: lol. 00:22:30 goldbach's conjecture is beautiful now? 00:22:33 right, due to not having an optical drive? 00:22:35 in logic notation? 00:22:42 olsner: i'm going to boot from hd with grub :p 00:22:47 so you're going to install the installer and boot it with grub? 00:22:49 olsner: I could just fish out a usb stick but this is the moar funz 00:22:50 yes 00:22:52 yes i am 00:22:54 install by copying 00:22:57 I approve :D 00:23:33 GRUB2 will be compiled with following components: 00:23:33 Platform: i386-efi 00:23:37 hmm 00:23:40 oh wait grub doesn't do 64-bit 00:23:40 right 00:23:43 don't want efi though 00:24:12 can it even boot without efi support on a mac? 00:24:20 olsner: well. yes. with bios emulation. 00:24:26 although probably it hands over control as bios? 00:24:33 i'm just scared that it'll be grub-efi 00:24:35 which I do nooooot want 00:24:42 olsner: see http://grub.enbug.org/TestingOnMacbook 00:24:47 erm 00:24:47 wrong page 00:24:57 oh no wait 00:24:59 olsner: that's the page 00:25:02 olsner: see drawbacks 00:25:05 no virtual terminals :-) 00:25:08 But Grub-EFI is so modern! 00:25:27 is it actually possible to force a bios build??? 00:25:43 aha 00:25:49 --with-platform=pc should do it 00:26:05 (is that "ok" to do? who knows let's find out) 00:27:48 In file included from kern/err.c:23: 00:27:48 ./include/grub/i18n.h:28:5: error: "ENABLE_NLS" is not defined 00:27:48 make: *** [kernel_img-kern_err.o] Error 1 00:27:49 make: *** Waiting for unfinished jobs.... 00:27:51 In file included from kern/misc.c:26: 00:27:53 ./include/grub/i18n.h:28:5: error: "ENABLE_NLS" is not defined 00:27:55 lol. 00:31:27 ok seriously. even a grub 1 image would do 00:31:41 i'll try a grub floppy. who knows 00:31:44 it just might work 00:32:47 let's see if that worked 00:32:48 refit time 00:33:07 http://en.wikipedia.org/wiki/Alexa_Ray_Joel 00:33:23 [[On December 5, 2009 Joel ingested a quantity of Traumeel, a homeopathic alternative to ibuprofen.]] 00:33:31 Worst. Suicide attempt. EVER. 00:33:34 That's WikiNotable! 00:33:42 And HILARIOUS. 00:33:42 Oh, I thought it was ... without context. 00:33:48 On December 6, 2009 Joel ate breakfast. 00:37:31 This is a perfect demonstration of the way that selection pressures in our culture are working against intelligence. 00:37:33 I wouldn't call that a suicide attempt 00:38:13 People clever enough to realise that you should use evidence-based suicide do not go on to reproduce, while those who opt for complementary and alternative suicide live. 00:38:29 j-invariant, well "attempt" is certainly relevant. 00:38:41 Note: that thing about selection is tongue in cheek. 00:38:43 [[Within a month after her Traumeel incident, on December 31, 2009 Joel publicly posted[51] that she wanted to help young girls deal with what she termed "heartbreak-related depression,"[52] which term, it was noted, "does not currently exist as a clinically diagnosable form of depression."]] 00:38:58 elliott, like CWC and his date ed classes. 00:39:22 she's just an idiot, now she goes on to make depression even less respectable as a serious mental healht problem 00:39:47 -!- elliott has quit (Remote host closed the connection). 00:40:47 They had that public mass-suicide-by-homeopathy thing, http://www.1023.org.uk/the-1023-overdose-event.php 00:41:15 -!- FireFly has quit (Quit: swatted to death). 00:41:17 has that had much of an effect? 00:41:45 -!- elliott has joined. 00:41:53 Didn't work. 00:42:07 Wait, I have another idea. 00:42:07 all these fucking "cuts" everyone complains about, but the NHS still prescibes homepathy and ancient chinese "stick needles in the guy to heal him" 00:42:22 yeah nhs support of homeopathy is fucked 00:42:38 Great idea: aquapuncture - combination of the ancient chinese art (?) and homeopathy! 00:42:47 I'll make a forture^H^H^H help lots of people! 00:42:52 :D 00:42:52 I thought the government basically said "no, it doesn't work, but we're still going to use it." 00:43:01 -!- elliott has quit (Remote host closed the connection). 00:43:10 Take a needle. Dilute it 10^60 times. 00:43:15 XD 00:43:19 Stick it into the patient. 00:43:47 Iridopuncture, aka needles-to-the-eye. 00:43:50 Although that would probably cure you of pins and needles, not anything else. 00:44:10 Like-cures-like is applicable to EVERYTHING. 00:44:25 Shot? Dilute a bullet 10^60 times! 00:44:56 Minecraft homeopathy. 00:45:13 Phantom_Hoover: Broken foot? Dissolve someone else's foot in acid, then start diluting that. 00:45:26 (Remember to break it first, though.) 00:46:41 Defend yourself against creepers! Bucket + gunpowder, then repeat 100 times! 00:53:50 -!- variable has quit (Read error: Operation timed out). 00:55:48 -!- variable has joined. 00:56:49 -!- elliott has joined. 00:56:57 I've had a sudden burst of reasonableness and found a USB stick 00:58:50 Phantom_Hoover: Can the world float? 00:59:04 elliott, not sure. 00:59:09 CAN IT FLOAT ON PIN 01:03:09 Phantom_Hoover: Who was the hippocampus? 01:03:29 John. 01:03:38 That explains it. 01:08:07 -!- coppro has quit (Quit: Changing server). 01:19:26 -!- elliott has quit (Remote host closed the connection). 01:25:54 -!- elliott has joined. 01:29:15 "One of the arguments for functional programming is better modular design. By analyzing publications advocating this approach, in particular through the example of a framework for financial contracts, we assess is strengths and weaknesses, and compare it with object-oriented design. The overall conclusion is that object- oriented design, especially in a modern form supporting high-level routine objects or “agents”, subsumes the fu 01:29:15 nctional approach, retaining its benefits while providing higher-level abstractions more supportive of extension and reuse." 01:29:18 --Bertrand Meyer ... 01:29:21 I disagree :-P 01:29:23 One of the arguments for functional programming is better modular design. By analyzing publications advocating this approach, in particular through the example of a framework for financial contracts, we assess is strengths and weaknesses, and compare it with object-oriented design. The overall conclusion is that object- oriented design, especially in a modern form supporting high-level routine objects or “agents”, subsumes the fun 01:29:23 ctional approach, retaining its benefits while providing higher-level abstractions more supportive of extension and reuse. 01:29:24 erm 01:29:25 http://se.ethz.ch/~meyer/publications/functional/meyer_functional_oo.pdf 01:30:04 "(We share the reader’s alarm at the unappetizing nature of the examples, especially coming from a Paris- based author. The sympathetic explanation is that the presentation was directed to a foreign audience of which it assumed, along with unfamiliarity with the metric system, barbaric culinary habits. The present discussion relies on the assumption that bad taste in desserts is not a sufficient predictor of bad taste in language an 01:30:05 d architecture paradigms.)" 01:31:31 -!- elliott has quit (Remote host closed the connection). 01:37:51 -!- j-invariant has quit (Quit: leaving). 01:42:19 -!- rderos has joined. 01:42:23 -!- rderos has left (?). 01:43:40 -!- elliott has joined. 01:48:42 [[When people want to emphasize how pathetically far we are from proving P≠NP, they often use the following argument: for godsakes, we can’t even prove that NEXP-complete problems aren’t solvable by depth-3, polynomial-size circuits consisting entirely of mod 6 gates! 01:48:42 But no more.]] 01:52:28 * oerjan wonders who "they" are :D 01:53:41 oerjan: the set {Scott Aaronson} :D 01:54:24 so he uses the royal "then", i take? 01:54:30 *"they" 01:54:34 oerjan: clearly :D 01:55:24 a subtle megalomania mixing the styles of queen victoria and julius caesar 01:57:12 bleh ... it seems you have to have a gpt thing to do usb w/ macbook air 01:57:18 wonder if fedora's stuff would do it 01:58:10 * oerjan looks at the actual blog post and detects _possibly_ a tiny tinge of sarcasm there... 01:58:16 oerjan: no shit :P 01:59:45 elliott: I feel slightly wrong writing in a functional style in K&R C 01:59:59 ais523: Er, wow. What. 02:00:01 purely for the purpose of making a "record this, do something, put it back to the original value" wrapper nest easily 02:00:02 ais523, cool! 02:00:08 ais523: Why are you ... 02:00:25 ais523: I mean, K&R? And ... 02:00:25 and as for K&R C, I was writing a hacked version of NetHack for RNG manipulation purposes 02:00:29 and NetHack's written in K&R C 02:00:37 ais523: protoize that shit for AceHack :P 02:00:39 (it predates C89, so you can hardly blame it for that) 02:00:54 any reason not to? 02:01:00 I haven't done things like reindenting or protoizing so existing patches apply wel 02:01:02 *well 02:01:10 boring :) 02:01:20 the indentation style's currently a mix of my two-space, and NetHack's four spaces for one level, tab for two levels 02:01:42 ais523: ...see, um 02:01:51 ais523: not following an existing codebase's indentation style 02:01:58 ais523: I'm afraid I'm going to have to kill you for the benefit of everyone. 02:02:00 elliott: means I end up not mixing tabs and sapces? 02:02:05 you can't have things both ways round 02:02:15 ais523: at least keep the same indentation width 02:02:23 (4, since they probably assume tab=8) 02:02:28 yep, in some cases I've been interspersing eight spaces for two levels 02:02:47 ais523: but don't do any two-spacing 02:02:51 mostly because telling the editor to save mixed-tab-and-space, while entirely possible, would mean repeatedly changing it there and back 02:03:01 time to try out this ubuntu usb stick again 02:03:11 ais523: erm emacs can condition on the path of the file 02:03:20 -!- elliott has quit (Remote host closed the connection). 02:03:48 (for the logs) I know, but that would be a pain to set up 02:03:58 -!- elliott has joined. 02:04:00 -!- elliott has quit (Changing host). 02:04:00 -!- elliott has joined. 02:04:01 grrrrrrrrrrrrrr 02:04:02 as I have far too many NetHack source trees, in all sorts of places 02:04:05 -!- coppro has joined. 02:04:06 GRR 02:04:09 GRRRGRGRGRGGRGR 02:04:14 -!- coppro has quit (Client Quit). 02:04:35 elliott: what? 02:04:40 ais523: stupid mac 02:05:04 hmm, why do places like BBC News always credit YouTube or Wikipedia rather than the actual author of the content? 02:05:07 ais523: basically, as far as i can tell, the only way to boto from a usb stick is to have it gpt-partitioned 02:05:09 *boot 02:05:12 ouch 02:05:16 "Booting Windows or Linux from an external disk is not well-supported by Apple’s firmware. It may work for you, but if it does not work, there is nothing rEFIt can do about it." 02:05:17 ais523: which can be done ... with a fedora specific, linux-only, RPM package 02:05:20 (Just saw that on a page.) 02:05:26 so basically 02:05:28 my options are 02:05:34 - see if i can get that working here (endless unpredictable pain) 02:05:35 or 02:05:39 you need a Linux-based program in order to install Linux? 02:05:41 - £60 on external SuperDrive 02:05:55 ais523: clearly! ubuntu has instructions for setting up a usb stick on a mac but they don't work and from what i'm reading, cannot possibly work 02:06:02 hmm, what about running Fedora in a VM, and using that to reformat the stick? 02:06:14 -!- Phantom_Hoover has quit (Remote host closed the connection). 02:06:24 ais523: that... sounds like it could rapidly become more than £60 worth of pain 02:06:26 Can't you partition it with just gdisk? 02:06:39 fizzie: partitioning is easy -- getting the files on there and making it bootable, I have no idea ho 02:06:40 w 02:06:45 apparently it has to be HFS-partitioned too 02:06:51 -!- coppro has joined. 02:06:54 so regular bootloaders won't work? 02:07:05 fizzie: Feel like making a USB stick image for me? :-P 02:07:07 oops 02:07:12 that was totally my fault 02:07:17 All it'll require is alien, an Ubuntu ISO, and PATIENCE! 02:07:26 -!- augur has quit (Ping timeout: 240 seconds). 02:07:29 I think I'll instead sleep on it. :p 02:07:45 ais523: You're far too loyal not to help out, right? 02:09:19 ais523: THAT IS NOT THE SOUND OF REASSURANCE 02:10:25 ais523: re youtube/wikipedia 02:10:37 ais523: because those seem like real, respectable businesses 02:10:42 ais523: real sources 02:10:46 Coolguy1272 doesn't 02:12:11 [[Steve Wozniak is an out and out self proclaimed geek. As the co-founder of Apple, he has given the world products aimed at making our life easier and more fun.]] 02:12:17 I ... don't think Woz stayed on for very long, BBC 02:13:05 bleARGH 02:13:07 *bleargh 02:14:20 ok seriously 02:14:25 it's got to be possible to do this 02:14:35 elliott, is the last ep of season 1 good? 02:14:43 Sgeo: Does it matter? You can't skip any. 02:14:49 ais523: I don't suppose I can convince you to try and install one package and try out a command ...? 02:18:34 Well, most of the good episodes were near the end of the season 02:20:31 coppro: what about YOU, I can depend on you can't I 02:23:51 -!- augur has joined. 02:24:45 elliott: What assistance do ou need, citizen? 02:25:08 coppro: one (1) .rpm converted to .deb and installed by you with the help of ``Alien'' conversion tool; 02:25:19 coppro: and one (1) Ubuntu Live CD ISO downloaded; 02:25:29 coppro: and one (1) conversion of this ISO to a disk image using that Linux-only tool 02:26:02 knowledge of RED Hat is above your Clearance, citizen. 02:26:12 Report for termination immediately. 02:26:15 Thank you, and enjoy your day. 02:26:21 coppro: p 02:26:25 *alien -i foo.rpm 02:26:27 coppro: DAMMIT I'MA GO INSANE 02:26:34 sdfghjk, 02:26:36 nm, 02:26:37 zxcvbnm, 02:26:43 can't even bother with references INSTALL THE PACKAGE ;_; 02:26:50 why do you need your ISO converted? 02:26:58 coppro: to install ubuntu. 02:27:05 to what though 02:27:10 coppro: this. 02:27:38 what is this 02:27:44 coppro: um, a computing machine? 02:27:52 oh wait it's a usb stick image? 02:28:01 coppro: no it's a live cd that you can turn into a usb stick image 02:28:02 lol just stick a partition table in front of it 02:28:08 coppro: yeah um it needs to be gpt 02:28:10 and hfs-formatted 02:28:15 gpt? 02:28:15 and i have no idea what bootloader it installs 02:28:17 and hfs? 02:28:18 coppro: apple shit 02:28:32 lol not happening 02:28:37 (maily cos I'm lazy) 02:28:45 coppro: there _is_ a reason I mentioned the .rpm, you know 02:28:49 but also because you wouldn't do it for me 02:29:00 i would actually if yelled at enough 02:29:03 how much do i have to tell 02:29:20 "livecd-iso-to-disk --mactel --reset-mbr foo.iso blah" NAG NAG NAG 02:29:29 NAG NAG NAG NAG NAG NAG NAG 02:29:33 fffff 02:36:38 -!- augur has quit (Ping timeout: 240 seconds). 02:38:52 -!- augur has joined. 02:42:22 -!- augur has quit (Remote host closed the connection). 02:42:46 -!- augur has joined. 02:43:17 -!- augur has quit (Read error: Connection reset by peer). 02:43:34 -!- augur has joined. 02:48:56 augur: stop it 02:49:33 elliott: sorry. ive been trying to fix my mbp screen 02:49:36 i broke the glass :( 02:49:44 augur: pray to steve jobs 02:49:46 and yet i followed the professional instructions! 02:50:18 augur: steve jobs. 02:50:30 :P 02:51:18 elliott: surely you have another computer with linux 02:51:27 (that was a statement) 02:51:54 coppro: I do, yes, but uh ... hmm. 02:51:58 Why amn't I doing taht. 02:52:00 oh well 02:52:03 getting a friend to do it instead 02:56:07 hmm, has thedailywtf's forum actually been patched to allow only haikus? 02:56:14 as opposed to a mod doing it manually? 02:56:21 (the sidebar forum, not the replies on the articles) 02:56:38 ais523: er, wow 02:56:41 well, not only haikus, but posts of approximate haiku length 02:56:56 you can write a short plaintext sentence which has a similar length 02:57:09 http://forums.thedailywtf.com/forums/t/21032.aspx 02:57:10 not very haikuy 02:57:20 From henceforth, all messages posted that are not in the form of a Haiku will be deleted. 02:57:20 You have been warned. Have a nice day. 02:57:21 -!- poiuy_qwert has joined. 02:57:29 :D 02:57:34 ais523: seems like it's some kind of bug 02:57:36 maybe 02:57:38 ah 02:57:46 ais523: and then it was turned into a haiku rule 02:57:56 oh, I see 02:58:09 CS has decided only to allow very short posts due to being broken 02:58:31 and the mod's response was, instead of fixing the forum, to institute a "haiku rule" to patch around it 02:59:06 now if there was only some website I could post on to report curious perversions in information technology... 02:59:10 ais523: the REAL wtf... 02:59:12 :D 02:59:15 because that definitely qualifies 02:59:56 ais523: http://forums.thedailywtf.com/forums/p/21032/241597.aspx#241597 03:00:29 You can now type more text into the subject line (255 UTF-16 characters by the looks of it) than you can in a post (~180 was it?) 03:00:41 elliott: saw it already 03:01:09 CS? 03:01:14 community server 03:01:16 community server 03:01:18 ah 03:01:21 a horrible asp.net abomination 03:01:22 a much-maligned forum that somehow got even worse 03:01:26 the real wtf is the daily wtf 03:01:35 seriously, why did it have to be alex that started it? 03:01:39 he's so close to being the wtf himself 03:03:35 ais523: is Username a mod? 03:03:42 he has rather ...suspicious... stats 03:03:45 he/she 03:14:39 -!- oerjan has quit (Quit: Good night). 03:28:05 -!- elliott has quit (Remote host closed the connection). 03:32:47 ais523, have you determined the exact allowable length yet? 03:52:26 According to Star Trek, all aliens want human girls 03:52:35 Or, human-looking girls 03:56:00 -!- zzo38 has joined. 03:58:30 I want to make up the new URI scheme for IRC, to get rid of problems with "IRC" scheme. The new one can be "IRCP" (for "Internet Relay Chat Protocol") and it accepts the username and password field, host, port, and so on. For example the URL for this channel would be: ircp://irc.freenode.net:6667/join?%23esoteric 04:01:31 yuck 04:02:56 To represent the registration of this channel: ircp://irc.freenode.net:6667/cs/info?%23esoteric 04:04:10 coppro: We don't sell that. 04:06:51 Why would you have a password in a URI? 04:07:28 Sgeo: You probably wouldn't, but you could if you needed to. (Other URI schemes do support username/password) You might also include just the username. 04:10:54 ircp:// URIs shall be case-insensitive (except the password) 04:11:49 it would make far more sense to call this channel ircp://irc.freenode.net:6667/%23esoteric 04:12:32 and for instance, its info would be ircp://irc.freenode.net:6667/%esoteric?info 04:12:58 coppro: I understand, but I don't like that much. 04:13:25 it's certainly better than putting something dumb like chanserv in there 04:13:46 coppro: But it is the chanserv info, isn't it?? 04:13:56 but that info might not be provided by chanserv 04:14:13 also you're making "cs" be a magic string there 04:14:27 coppro: But then the servers do not have a standard way of retrieving it, and it won't work. 04:14:36 zzo38: yes, that's a difficulty 04:14:51 zzo38: but you don't have a standard way of asking for "cs" info 04:15:55 coppro: Yes; the URL for the channel info would be secondary level specification, not a primary level; primary levels are the more standard ones. Secondary levels are used when the primary ones are insufficient. 04:16:33 (As if they are two separate RFCs or two separate chapters in one RFC, for example.) 04:18:12 Also, the channel type symbol (#&!+) must be URL encoded using % and hex code, except for ! which can be written as either "!" or "%21". The # & + MUST be written using "%23", "%26", "%2b", respectively. 04:32:18 -!- BeholdMyGlory has quit (Remote host closed the connection). 04:41:24 There is a command on this IRC server I didn't know, the CHANTRACE command. 04:43:13 Just put ChanServ in the URI 04:43:33 Hmm, no, that sucks 04:43:43 ChanServ might not be the only thing gthat varies 04:43:50 gVaries, now using glib 04:46:50 Sgeo: It is why I have specified that there is "primary level" and "secondary level". 05:21:45 What is a algorithm for calculating standard deviation (using integers only)? 05:37:58 that sounds difficult, considering the average of integers is not necessarily an integer... 05:38:37 quintopia: I could also just calculating fixed point using integers 06:15:26 -!- hagb4rd has quit (Ping timeout: 240 seconds). 06:57:58 -!- zzo38 has quit (Remote host closed the connection). 07:04:36 * Sgeo wants combat rations 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:08:25 * chantrace :Outputs a list of members in #channel in ETRACE format, with the classname 08:08:25 * chantrace :replaced by the server the users are on. 08:08:29 @ zzo 08:12:01 Sgeo, you have a cloak on - right? 08:12:19 variable, why? 08:12:24 -!- Wamanuz3 has joined. 08:12:38 Sgeo, because I think I just found your IP 08:12:46 *gasp* 08:12:55 Sgeo, not a major issue 08:13:03 but I want to know if cloaks actually work 08:13:24 variable, well, try finding the IP of someone who's cloaked. 08:13:43 Sgeo, your not? 08:14:04 Unless it's possible to be cloaked without one's knowledge, I am not. 08:14:08 What made you think I was? 08:14:28 Sgeo, misreading my /whois 08:14:31 sorry 08:14:50 * Sgeo shrugs 08:15:00 cloaks work if you identify before joining a channel 08:15:14 I had one for a while myself 08:15:24 coppro, I know how it works - I misread something 08:15:25 but now I have a hostname I'm not interested in cloaking 08:15:34 -!- Wamanuz2 has quit (Ping timeout: 276 seconds). 08:15:50 heh 08:16:01 hrm 08:16:16 damn you, grad courses 08:16:34 coppro, what courses? 08:17:39 variable: there's a course on logic next term I may sit in on 08:18:05 it's called "logic for comp. sci." by the registrar 08:18:10 coppro, cool 08:18:11 which leaves me guessing as to what it actually is 08:18:35 my favorite subject is logic :-} 08:19:11 but if it's anything like the previous logic course taught by the same prof (Advanced Logic in Computer Science) 5 terms ago, then it may be worth trying to maneuver my way around the dumb undergrad course 08:23:01 I'm not sure how far above my head it starts 08:23:22 but if it isn't too far, I would definitely love to take a real logic course rather than the blargh undergrad one 08:23:46 (provided, also, that I can convince necessary people that it is a good idea for me to replace the mandatory undergrad course with the grad one) 08:24:17 coppro, worst case just audit the class 08:29:26 variable: if I can find the time, sure 08:29:38 and/or if I can follow along 08:33:37 `/win 3 08:34:06 No output. 08:39:54 -!- Wamanuz4 has joined. 08:43:22 -!- Wamanuz3 has quit (Ping timeout: 276 seconds). 08:50:08 -!- sftp has quit (Remote host closed the connection). 08:58:31 -!- Wamanuz5 has joined. 09:01:10 -!- Wamanuz4 has quit (Ping timeout: 265 seconds). 09:36:45 -!- Wamanuz has joined. 09:39:00 -!- Wamanuz5 has quit (Ping timeout: 246 seconds). 09:54:01 -!- Wamanuz2 has joined. 09:56:52 -!- Wamanuz has quit (Ping timeout: 260 seconds). 10:19:20 ais523: that... sounds like it could rapidly become more than £60 worth of pain <-- (for logs): why £60 specifically? 10:39:03 My parents insist that I never stopped talking since I was nine months old, but this video tape of me at my first birthday has a distinctive lack of any meaningful vocalizations :P 11:01:07 -!- Wamanuz3 has joined. 11:04:17 -!- Wamanuz2 has quit (Ping timeout: 255 seconds). 11:13:41 -!- Wamanuz3 has quit (Read error: Connection reset by peer). 11:16:43 -!- Wamanuz4 has joined. 11:31:20 -!- MigoMipo has joined. 12:10:49 Gregor, :D 12:18:41 -!- augur has changed nick to mauna. 12:18:49 -!- mauna has changed nick to augur. 12:21:23 -!- Phantom_Hoover has joined. 12:21:23 -!- Phantom_Hoover has quit (Changing host). 12:21:23 -!- Phantom_Hoover has joined. 12:24:06 -!- wareya has left (?). 12:37:11 -!- oerjan has joined. 12:42:52 oerjan! 12:42:54 WAR! 12:43:48 -!- WAR has joined. 12:44:07 That would have been a lot better if it hadn't had my name in the whois. 12:44:56 -!- zzo38 has joined. 12:45:24 I wanted to make the "plain.cards" file and "texnicard_format.tex" file also available in the book, so I wrote a program in AWK. 12:45:38 -!- WAR has quit (Client Quit). 12:45:47 I don't think I have written a program in AWK before. 12:47:16 It works; but maybe I have done something 'improper' by not knowing programming with AWK, before. I don't know. 12:49:06 -!- zzo38 has set topic: nice stuff at http://esolangs.org/wiki/Main_Page | retards at voxelperfect.net have expired | historical documents at http://tunes.org/~nef/logs/esoteric/?C=M;O=D or via hg at http://codu.org/projects/esotericlogs/hg/. 12:49:54 -!- Phantom_Hoover has set topic: turds at http://esolangs.org/wiki/Main_Page | turds at voxelperfect.net have expired | historical turds at http://tunes.org/~nef/logs/esoteric/?C=M;O=D or via hg at http://codu.org/projects/esotericlogs/hg/. 12:49:58 TURDS 12:50:32 -!- zzo38 has set topic: TURDS at http://esolangs.org/wiki/Main_Page | TURDS at voxelperfect.net have expired | historical TURDS at http://tunes.org/~nef/logs/esoteric/?C=M;O=D or via hg at http://codu.org/projects/esotericlogs/hg/. 12:51:11 Good enough. 12:54:15 Is this considered a 'proper' program in AWK, or is there some things which I have done badly and could be improvement? http://sprunge.us/eLcc 13:02:50 why is SPARC system programming is soo undocumented 13:03:13 nooga: I don't know. Are you trying to write a program? 13:04:01 OS 13:15:37 beh 13:33:11 nooga, hm, how does SPARC deal with the register window thing when it comes to running out of registers. That is: what happens when call stack gets too deep? 13:33:41 i don't know because i can't find the goddamn docs 13:33:45 ah 13:33:57 something like intel's manual 13:34:37 I was wondering if it was handled by the hardware itself or if it invoked an exception handler which had to deal with it 13:40:29 -!- ais523 has quit (Remote host closed the connection). 13:40:45 going to reboot for kernel upgrade on the computer running this irc bouncer 13:40:47 bbl 13:40:56 -!- Vorpal has quit (Quit: ZNC - http://znc.sourceforge.net). 13:49:27 * Sgeo wonders if it may be worth it to wipe out Ubuntu and just use Tinycore for his Linux needs 13:53:27 IIRC running out of register window "depth" generates an exception, and then an OS exception handler will do some stack-pushery. 13:54:48 nooga: http://developers.sun.com/solaris/articles/sparcv9.pdf not good enough for your purposes? 14:05:54 -!- sftp has joined. 14:06:52 fizzie: lol, i'm stupid 14:07:04 i found that earlier and forgot that i have it :G 14:22:03 -!- Vorpal has joined. 14:43:45 Vorpal: "An overflow [of the register windows] causes a spill trap that allows privileged software [read: the OS] to save the occupied register window in memory, thereby making it available for use." 14:50:17 What are algorithms for calculating such things as standard deviation, etc? 14:54:56 zzo38: http://en.wikipedia.org/wiki/Standard_deviation#Rapid_calculation_methods 14:58:04 That's a bit of a misleading title there, since it seems more about doing a running standard deviation; for the std of a particular n-point data set, I don't think there's typically anything much more cleverer than the straight-forward O(n) just-you-know-calculate-it thing. 14:59:32 The algorithm described there should work. 15:00:07 How large do you expect $s_2$ to become in case of a large set of cards? 15:01:17 fizzie: well the clever thing about it afaik is that you can calculate it in one pass... 15:01:51 zzo38: well it should be less than N times the square of your maximal value... 15:02:02 oerjan: Well, yes, that is what I was alluding to with the "running" part. 15:02:13 (this is of course rather trivial) 15:02:27 fizzie: mhm 15:03:14 Anyhoo, quite often doing two passes is not a problem either. 15:03:34 The see-also "computing variance" article is a bit more comprehensive. 15:13:51 fizzie, ah 15:14:50 fizzie, presumably there is some trap when going the other way too? (In order to unspill when required) 15:15:11 Yes, there's a "window underflow" trap too. 15:17:12 (And there are some complications because the OS needs to make sure one process can't manage to peek into the register windows of another process.) 15:17:22 fizzie: you seem to know SPARCs pretty well 15:18:25 fizzie, hm... You mean like, store/restore windows on context switch? 15:19:05 if so, not sure how much it differs from normal storing/restoring of registers on other platforms (such as x86) 15:19:08 Vorpal: It doesn't need to, because there are separate registers to mark some register windows belonging to "current process" and others to "other", and separate traps for those. 15:19:40 nooga: Not really, I've just read a bit back when doing our compiler course, which had a sparc backend. 15:19:52 fizzie, but what if you have three processes? 15:20:17 Then you'd have to manually keep track, but there's still some windows "owned" by the current one, and some by the others. 15:21:38 fizzie, so the OS will spill/unspill as required then? 15:22:34 fizzie, how much does this enforce a specific calling convention btw? I remember reading that (on x86/x86-64 at least) GHC uses a custom calling convention. 15:22:41 Something like that. As far as I can determine, the idea is that if the current process only uses K register windows, you don't need to spill/fill the N-K unused ones. 15:23:32 fizzie, right, but if it uses all N then this would mean more switches to kernel mode? 15:23:43 which are usually slow on most architectures 15:25:03 I don't know about the tradeoffs, but there probably is one, yes. You could even have the OS maintain some sort of a per-process guesswork as to how many "clean" register windows it's going to prepare in advance on a context switch. 15:25:04 Is there an algorithm that works better to calculate it if the sample values are already sorted low to high? 15:25:32 -!- BeholdMyGlory has joined. 15:26:20 fizzie, btw did I mention that mcmap bug? If you place a torch high up (about altitude 120 or above) you get a garbled mess on the map in a block around that area. Garbled both on normal map and on topo map. 15:26:25 (I don't think there is, but if you know of it, tell me) 15:26:52 zzo38, better than what? 15:27:02 Vorpal: Yes, I saw that, though I already managed to forget it. 15:27:08 zzo38, and to calculate what? 15:27:50 Standard deviation, I assume. 15:27:58 fizzie, well, if you happen to have time to test it... 15:28:06 fizzie, ah 15:28:58 See, if you had written this in the github issue list, I wouldn't have managed to forget it. I'll try to take a look at some point. It's probably related to the "max-alt trees cause flickering map-garbage" thing I saw on my local server tests. 15:29:56 I know since it is sorted, it can easily calculate minimum, maximum, median. 15:33:07 Which other statistics would be useful for a set of cards (such as for Magic: the Gathering and similar games)? 15:35:13 Histograms of different categorizations? (I seem to recall MtG cards can be grouped into lands/creatures/instants/whatevers.) 15:36:06 fizzie: Yes, the category by card type. 15:36:57 I can do like that, I already have grouping. 15:37:49 Another question, about notation: if $Q_2$ is median, does $Q_0$ mean the minimum? 15:38:15 I /think/ so, but Q_0 is not normally defined. 15:38:46 From Wikipedia: "The 25th percentile is also known as the first quartile (Q1); the 50th percentile as the median or second quartile (Q2); the 75th percentile as the third quartile (Q3)." 15:39:21 It doesn't mention $Q_0$ or $Q_4$ (or $Q_5$, but that doesn't make sense). 15:39:43 Yes, so Q_0 and Q_4 could easily be read as the maxima and minima, but they're never actually defined. 15:40:05 Well, "maximum and minimum", I suppose. 15:41:00 I could just add a note next to the equation that explains this notation. 15:42:41 -!- elliott has joined. 15:42:43 Vorpal: Based on a quick source-glance, I don't seem to be verifying the y values in world.c:block_change, and an overflow there could possibly ruin both the heightmap and the surface map. I'll take a closer look later. 15:43:00 (I want to see what sort of numbers the server sends before blindly fixing that.) 15:43:23 http://en.wikipedia.org/wiki/Second_derivative_test 15:44:30 More tales of my adventures in the maths class: when I pointed out that the teacher's proclamation that f''(x)=0 at a point said nothing about its nature, I was told to shut up. 15:45:12 The class being taught this were then informed that such a function would never come up, even after I pointed out that x^4 is clearly an example. 15:46:44 Phantom_Hoover: you must be SO POPULAR 15:47:37 elliott, I am actually banned from setting foot in the maths department. 15:48:03 You might mess up the dangerous maths experiments. 15:49:24 Mathemagical monsters: http://deltafunktio.animeunioni.org/dft_eka_osa.gif (Disclaimer: you... uh, might have to be able to read Finnish to understand any of that.) 15:49:31 "Safety: the natural logarithm is an irritant and should be washed away if it comes into contact with the skin." 15:50:30 fizzie: I think it's better without. 15:51:28 "INTEGRAALI" 15:55:10 fizzie, are the Finnish words for "oxygen" and "vulva" really only a letter apart? 15:55:35 Both are required breathing for continued existence. 15:58:57 Phantom_Hoover: I don't think so. But the words for "vulva" and "cone" (as in "pine cone", not as in "geometric shape") are. 15:59:19 That's even BETTER. 15:59:31 stop being a cont 16:00:01 Phantom_Hoover: As are the words for "oxygen" and a very colloquial term for the penis. 16:00:10 s/$/inuation!!/ 16:01:21 ("häpy", "käpy" and "happi", "heppi", respecitvely.) 16:01:54 fizzie, all similar! 16:02:06 i take it finns are fond of happiness 16:02:13 There's more than a single-letter difference between häpy/happi, though. 16:02:24 They *are* quite close, I guess. 16:02:38 Häpy heppi, heppi käppy. Käppy happi, happi häpy. 16:02:43 Erm. 16:02:50 Häpy heppi, heppi käpy. Käpy happi, happi häpy. 16:04:00 Sharing consonants does not two words alike make. 16:04:01 no?? 16:04:06 Deewiant: does 16:04:13 shut up finnish l|_|z3r 16:04:35 Deewiant, consonants and similar phonetic properties if you don't know Finnish orthography! 16:04:52 We have several words where the double-consonant (or a double-wovel) makes a semantic difference. Like "taka" → "takka" → "taakka"; "back" (mostly as a prefix, like "takapuoli" = "backside") → "fireplace" → "burden". 16:05:16 How do you pronounce double 'k's? 16:05:30 takka on takataakka 16:05:39 Well, it's a stop consonant, only longer-duration one. 16:05:56 fizzie, you can have duration for a consonant? 16:05:58 [k:] 16:06:25 Phantom_Hoover: Why couldn't you? 16:06:41 http://en.wikipedia.org/wiki/Stop_consonant#Length 16:06:45 english has a few double-consonants too 16:06:50 bork 16:06:54 fizzie, OK, a voiceless plosive consonant. 16:06:58 fizzie: Can you prove that Finnish isn't just a gigantic prank on the rest of the world? 16:07:10 Can you prove that English isn't? 16:07:18 Or C++! 16:07:32 Deewiant: Maybe it is, but if it is, it's a lot less funny than Finnish 16:07:34 *Finnish. 16:07:45 More sad. 16:08:00 Deewiant, it's more what you get when you take about 3 languages and mush them together without thinking. 16:08:10 English is like "A man walks into a bar. He is an alcoholic and it's destroying his family." 16:08:44 `translatefromto en fi A man walks into a bar. He is an alcoholic and it's destroying his family. 16:08:53 http://www.youtube.com/watch?v=yL21sCWfnbE&t=1m8s "tuki" vs "tukki" 16:09:01 Mies kävelee baariin. Hän on alkoholisti ja se tuhoaa hänen perheensä. 16:09:30 (Disclaimer: I don't know if the guy knows what he's talking about, I just searched for an example) 16:11:32 The mode in Wikipedia is different from TeX; it has some commands that TeX doesn't and TeX has many commands that Wikipedia doesn't. Most equations probably works, though. 16:11:32 Wait, is a long stop just one in which you wait for a bit before removing the obstruction from the airway? 16:11:50 zzo38, this is because it is, in fact, LaTeX, 16:12:01 *EVILBLOATeX 16:12:02 Something like that, yes. 16:12:49 Phantom_Hoover: Does LaTeX not have any \def command? 16:13:19 elliott, so LaTeX is A Bad Thing as *well*? 16:13:29 IS THERE NOTHING THAT DOESN'T SUCK IN YOUR WORLD 16:13:31 Phantom_Hoover: No -- zzo38 just hates it. 16:13:35 Phantom_Hoover: I think LaTeX is great. 16:13:40 elliott, oh, right. 16:13:57 Well, there *is* nothing that doesn't suck in zzo's world, unless he made it himself. 16:14:54 Phantom_Hoover: Isn't that just what the Wikipedia link I pointed at says: "In a geminate or long stop, the occlusion lasts longer than in normal stops. In languages where stops are only distinguished by length (e.g. Arabic, Ilwana, Icelandic), the long stops may last up to three times as long as the short stops." 16:15:15 fizzie, that is indeed where I got it from. 16:15:41 Oh, I thought you were trying to describe what Deewiant's video was like. 16:15:46 But phonetic language confuses me, not least because "stop" and "plosive" both seem to mean the same thing for no readily apparent reason. 16:16:03 (I find Plain TeX easier to understand and use; but there are some things I don't like in TeX and some things which I think are missing. In general it is good, though.) 16:16:11 That guy was going on about glottal stops, so I suspect he may have no idea what he's talking about. 16:16:15 However, "ex-stop" and "explosive" are a very different thing. 16:16:25 elliott, Swedish has double consonants too. With different effects on the pronunciation than for Finnish though. And sometimes with semantic differences. (For example sil = sieve, sill = herring) 16:17:12 Vorpal: What kind of effect, do you have to pronounce it longer? 16:17:21 Or, louder? 16:17:31 zzo38, it modifies the preceding vowel. 16:18:02 Vorpal: OK. 16:18:40 `wl sv en sil 16:18:41 For Finnish it'd just be mostly a lenghtening. Compare "hila" (wicket/grate/grid) and "hilla" (cloudberry). 16:18:43 Sieve 16:19:07 elliott, as I said yes 16:19:18 You are probably not lying entirely! 16:19:29 Our phonology is a bit on the simplistic side. 16:19:38 Unlike EVERYTHING ELSE. 16:20:08 Ooh, Wikipedia has examples, I don't need to invent any: 16:20:09 tuli = fire, tuuli = wind, tulli = customs 16:20:09 muta = mud, muuta = other (partitive sg.), mutta = but, muuttaa = to change or to move 16:20:12 http://en.wikipedia.org/wiki/Finnish_phonology#Length 16:20:42 in Swedish the word "hade" (meaning "had") is pronounced as if it had been written like "hadde" btw. 16:20:55 english has a few double-consonants too ← not any with syntactic meaning AFAIK. 16:21:28 tuli = fire, tuuli = wind, tulli = customs <-- the last meaning I wound suspect is imported from Swedish, since sv:tull = en:customs. Either that or a common source for both. 16:21:42 well, not meaning. Word 16:22:17 Phantom_Hoover: I mean double consonants that are pronounced longer 16:22:55 I think it's mostly when combining a word that ends with the same consonant the other word starts with 16:23:44 and then Swedish has the fun word pairs like tomten/tomten, anden/anden and so on. (Same spelling, different pronunciation for different meanings. VERY subtle differences.) 16:24:14 (isn't it just a change in stress or whatever it is called?) 16:24:20 Yes. 16:24:45 in those examples, it's tonal differences rather than stress 16:24:49 olsner, ah 16:25:20 olsner, are there such examples with change of stress then? 16:25:59 -!- elliott has quit (Remote host closed the connection). 16:26:25 -!- elliott has joined. 16:27:54 [Of Finnish:] "Thus, omenanani "as my apple" contains light syllables only, and has primary stress on the first syllable and secondary on the third, as expected. In omenanamme "as our apple", on the other hand, the third syllable (na) is light and the fourth heavy (nam), thus secondary stress falls on the fourth syllable. --" Nice example words there. 16:28:35 Vorpal: I think stress is what happens with our double consonants 16:28:52 olsner, ah, but no cases with same spelling then? 16:29:00 Also, "omenanamme" = "as our apple", "omenan amme" = "apple's bathtub". 16:29:14 Vorpal: not that I can think of, but there probably are 16:32:21 fizzie, hah 16:32:28 Here's (in Finnish) two words that are spelled identically, but the stress differs: "-- for example the compound puunaama, meaning "wooden face" (from puu "tree" and naama "face"), is pronounced [ˈpuː-ˌnɑː-mɑ] but puunaama, meaning "which was cleaned" (...preceded by an agent in genitive, "by someone"), is pronounced [ˈpuː-nɑː-mɑ]." 16:33:11 fizzie, "[...](...preceded by an agent in genitive, "by someone")[...]" <-- a cleaning agent? 16:33:18 ;) 16:33:52 Unfortunately the stress-indicating bold font parts got lost. 16:33:58 ah 16:34:06 fizzie, well the channels filter bold I think 16:34:12 channel* 16:34:16 ls 16:34:19 err wrong window 16:34:31 That should've been [*ˈpuː-ˌnɑː*-mɑ] vs. [*ˈpuː*-nɑː-mɑ]. 16:38:02 fizzie, not as bad as the English words which are spelt identically but pronounced differently. 16:39:17 Phantom_Hoover, such as? 16:39:28 I can't think of any example atl 16:39:29 atm* 16:39:30 Read and read. 16:39:37 Tear and tear. 16:39:51 ah 16:40:06 Which are both because "ea" can be pronounced 'eh' or 'ee'. 16:41:20 hm, Does any other language have the sje-sound of Swedish? I seem to remember reading it was unique 16:41:49 well, Finland-Swedish (or whatever the English name of it is) has it obviously 16:41:59 Hmm... I wonder if fan #3 in this computer just doesn't have speed measurements available or why does lm-sensors say "0 RPM ALARM" about it... 16:42:47 Ilari, open case to check. I know that in my computer it is due to not having a case fan. (only CPU fan, PSU fan and GPU fan, and sensors only report about the CPU fan) 16:42:53 Vorpal: does it though? some dialects has it as sh, seem to recall finland-swedish doing that too 16:43:11 olsner, they have a different variant of it, that's true. 16:44:55 olsner, hm arguably the sje-sound in kjol and stjärna are slightly different. At least in whatever dialectal mix I speak. 16:45:13 kjol doesn't have a sje-sound 16:45:23 olsner, what do you call that sound then? 16:46:50 Today I learned AWK programming. 16:47:02 -!- cheater99 has quit (Ping timeout: 240 seconds). 16:47:09 Vorpal: http://en.wikipedia.org/wiki/Sje-sound#Colognian 16:48:15 Deewiant: "Whether or not there is a relation between the Swedish /ɧ/, and the Kölsch /ɧ/, is not known. While none seems to have been established, comments (e.g. on page 18 in [3]) suggest that, the choice of ‹ɧ› might well have been based upon a misunderstanding." 16:48:21 Deewiant, does that text say they are different or the same. It seems to discuss that but I'm not good at linguistics. 16:48:33 (basically I got lost in the jargon) 16:48:37 Deewiant: This is what you get when you let languages go all natural. 16:48:54 fizzie: I know, I didn't say that it was in another language, I just linked it 16:49:01 And yes, that's what you get 16:50:05 Vorpal: I would call it http://en.wikipedia.org/wiki/Voiceless_postalveolar_fricative but wikipedia claims swedish kjol has a different sound 16:50:14 hm 16:50:42 namely, this one: http://en.wikipedia.org/wiki/Voiceless_alveolo-palatal_fricative 16:51:24 olsner, also stjärna vs. sju. A quick experiment seems to indicate the position in the mouth of the sje-sound in those two words is somewhat different. 16:51:27 As a speech recognition guy, I think I'll petition the World Government (in our inevitable dystopic future) to instigate a "designed to be phonologically as simple as possible to distinguish" language instead. Maybe with just two (or very few) as-spectrally-different-as-possible sounds, and then all words are simple concatenations of those with none of this context-sensitive crap. 16:52:27 fizzie: I propose mindlinks. 16:52:28 Vorpal: yeah, it merges with the vowel a bit, dunno if it's enough of a difference to call it different sounds 16:52:35 olsner, hm 16:58:14 I've heard in a few places that this is the ugliest Finnish sentence(-pair) evar: "Älä rääkkää sitä kääkkää! En rääkkääkään!". (Translated, vaguely like: Don't torture that old guy! I'm not!) 16:58:26 -!- elliott has quit (Remote host closed the connection). 16:58:44 -!- LORD_NIETZSCHE has joined. 16:59:13 -!- elliott has joined. 16:59:54 -!- cheater99 has joined. 17:00:06 fizzie, hah 17:00:16 elliott, you seem to have connection problems today? 17:00:17 yeah 17:00:28 Vorpal: um i think i've gone offline exactly twice? 17:00:30 who is LORD_NIETZSCH 17:00:31 who is LORD_NIETZSCHE 17:00:35 no clue 17:00:38 it's me 17:00:44 can his nick stop shouting 17:01:21 MOSFET 17:01:58 -!- LORD_NIETZSCHE has left (?). 17:07:05 -!- cheater99 has quit (Read error: Connection reset by peer). 17:07:26 Who was Lord Nietzche? 17:07:30 What's updog? 17:07:30 What's updog? 17:09:36 http://userweb.kernel.org/~warthog9/april1/2010/ please tell me kernel.org actually looked like this on apr 1 17:11:36 -!- j-invariant has joined. 17:15:54 -!- cheater99 has joined. 17:24:08 elliott, the upside-down K is the height of stupidity. 17:24:24 It is rather silly. 17:26:05 http://www.complexitygraphics.com/#708027/-About-Contact <3 17:27:49 [[Graduated from Moscow State University in Social Psychology, and then studied in High Academic School of Graphic Design. ]] 17:27:51 Pfff. 17:28:01 INFERIOR SUBJECTS. 17:28:03 indeed 17:28:09 her knees are too angular anyway! 17:28:23 elliott, wha? 17:28:26 Phantom_Hoover: Meme. 17:28:52 elliott, wha? 17:28:55 wha? 17:29:14 Wow, I never realised that the Oolite theme gets way better if you wait a bit. 17:29:40 Phantom_Hoover: Define theme. 17:29:45 Oh, the tune. 17:29:46 Yes. 17:29:46 Indeed. 17:31:30 Phantom_Hoover: guy in #anagol just said php is better than haskell 17:32:05 This I must see. 17:32:16 Phantom_Hoover: nothing else was said 17:32:31 elliott, well at least tell them that they're an idiot! 17:33:02 Phantom_Hoover: http://sprunge.us/YTNc 17:33:24 17:31 Endres: um, but I think for me it is so 17:33:24 17:32 Endres: maybe not better, but... easier maybe? 17:33:35 not even gonna bother arguing ... 'specially since obvs not a native 17:33:47 easier? lol 17:33:56 Wait, wasn't *your* first language PHP? 17:34:21 Phantom_Hoover: i think it was technically basic that i never tried to understand and just copied from a book 17:34:26 PHP should be evaporated together with every dedicated PHP programmer 17:34:31 but um, pretty much php, yeah 17:34:33 :/ 17:34:37 to be fair i was 8 ok? 17:34:48 elliott, oh, so it was child abuse by someone. 17:34:57 no, i chose to learn it myself 17:35:01 i was 10 when i tried Pascal, don't worry elliott 17:35:07 after learning that $favourite_website was written in PHP 17:35:21 Phantom_Hoover: i used odbc to communicate with an Access database in PHP 17:35:23 I'm not kidding 17:35:38 man 17:35:42 I need some alcohol to forget that now 17:35:47 elliott, wait, so you were using Windows as well? 17:35:59 Phantom_Hoover: this was before ubuntu even existed 17:36:00 nooga, Pascal was my first language soon! 17:36:04 *too 17:36:06 Phantom_Hoover: also we had a winmodem 17:36:09 so linux is like ... no 17:36:23 Followed soon by Python, then about a week later by CL. 17:36:54 Phantom_Hoover: You are the luckiest bastard. Seriously. 17:37:02 elliott, naaa. 17:37:07 soon ... "F 17:37:09 :F 17:37:13 what's CL? 17:37:15 Phantom_Hoover: OK, Pascal is kind of shit, but it's not a /hideous/ language. 17:37:23 Phantom_Hoover: Python is lame but really, it's not _that_ bad. 17:37:29 Phantom_Hoover: And then Common Lisp which is pretty damn good. 17:37:31 j-invariant: common lisp 17:37:39 Phantom_Hoover: I stayed with PHP for about _two years_. 17:37:51 Do you have *any* idea how warped my grey matter became? 17:37:55 elliott, it was when you were asked to conceive and implement a sort algorithm by yourself. 17:38:16 Phantom_Hoover: Hm? 17:38:21 With a teacher who as far as I know was a Latin teacher who later became the computing teacher. 17:38:23 I had no idea why you would ever abstract anything. No idea how to modularise code. 17:38:32 No idea that mixing code and, you know, output was in any way sub-optimal. 17:38:44 I rarely used functions. 17:38:50 I was _awful_. 17:38:53 Two years. 17:38:54 elliott, that is indicative of bad PHP coding - not necc. the language itself 17:38:57 Or so. 17:39:06 although I will say that most PHP examples are HORRIBLE 17:39:10 variable: Perhaps. But PHP certainly lends itself to bad coding style. 17:39:11 elliott: don't worry 17:39:14 variable, yes, but when the language is definitely not conducive to that style... 17:39:14 elliott, agreed 17:39:18 variable: And even when it's coded perfectly, it's still a horrible language. 17:39:36 elliott, it is not horrible for its purpose 17:39:40 Yes. It is. 17:39:58 uhmit is horrrible for every purpose 17:39:59 trust me 17:40:05 variable: what purpose 17:40:11 i code php for *cough* money 17:40:16 As someone who stayed in the awful confines of web development for too many years, let me say that yes, it is. Absolutely horrible. 17:40:18 FWIW, I actually got my self-conceived sort algorithm off the ground when I used CL. 17:40:29 elliott is right 17:40:30 Hell, if you want to, I don't know, put the current date and time on a page. Even Perl is better. 17:40:51 But I gave up on doing it in Pascal when noöne could work out how the hell you got a function to return an array. 17:41:00 Phantom_Hoover: I don't think you can even do that 17:41:10 elliott, nor did the teacher. 17:41:29 variable: http://catseye.tc/about/php.html 17:41:46 The fourth paragraph of that is perhaps my favourite thing ever. 17:41:54 He basically told me to either use globals or alter the array passed to it. 17:42:05 Already Phantom_Hoover knew the putrid stench of mutability! 17:43:05 Yes, at that point I thought "forget that", then did it in Python and then CL. Of course, I mutated the array passed for those programs, too, but I was what, 13? 17:43:31 The algorithm was O(n^2), as well! 17:43:36 I like how you're apologising for not being a rabid functional weenie by 13. 17:43:39 i feel that i need to design a language that is extendable and elastic like scheme, concise like ruby or something and has a compiler that generates fast machine code 17:43:42 and then 17:43:47 i will code only in this language 17:43:55 nooga: And is purely functional? 17:43:57 Naw, thought not. 17:44:08 useless then 17:44:09 elliott: not Haskell 17:44:17 nooga: There are purely-functional languages that are not Haskell. 17:44:22 Haskell isn't too extensible, either. 17:44:26 i don't like them 17:44:40 i like mixed paradigm languages, like ruby 17:44:43 Well, not in the same sense that Scheme is. 17:44:57 nooga: Irrelevant; answer the question: mutable data? 17:45:34 immutable = useless 17:45:39 nooga: Ha ha ha. 17:45:42 Your language sucks. 17:45:53 I LIKE to mess with arrays in-place 17:46:08 It amazes me how people still think, in 2010, that they should create a language that practically actively works against a programmer. 17:46:23 Apparently the world has not yet learned that you don't put in "features" merely because they're easy to implement at the lower level. 17:46:30 Otherwise you throw away abstraction. 17:46:44 look 17:47:17 i know haskell is awesome and it's compiler is a piece of art 17:47:27 art LOL 17:47:36 lol 17:47:38 I would have claled it something else 17:47:39 clearly you have never seen ghc code 17:47:44 nobody gives a shit what the compiler looks like 17:47:55 * Phantom_Hoover shivers at GHC 17:47:55 anyway i don't even like haskell all that much, it has many flaws, but that's irrelevant 17:48:03 the fact is that mutability is a serious, crippling design flaw 17:48:07 elliott, what flaws? 17:48:13 I can't use haskell :/ 17:48:21 And "it's not Epigram" does not count. 17:48:27 Phantom_Hoover: It's not Epigram. 17:48:55 Phantom_Hoover: Typeclasses are restricted in probably-unavoidable ways but I don't like them anyway; no module system (a la ML, with functors (not that kind of functor); this is VERY important for abstraction and reuse) 17:49:00 and i like to have more expressive C with poorman's, basic oo, closures and ability to mess with the language itself 17:49:01 Some syntax quibbles 17:49:05 Phantom_Hoover: and the fact that I don't like the IO monad 17:49:11 also, records with named fields are handled badly 17:49:12 etc ... 17:49:19 elliott, what's wrong with the IO monad? 17:49:32 Phantom_Hoover: it's imperative. 17:49:35 and impure. 17:49:40 ehh 17:49:51 Phantom_Hoover: If you disagree, see http://conal.net/blog/posts/the-c-language-is-purely-functional/ 17:50:11 it's funny that ppl try to make languages that work AGAINST common sense and our machines architecture 17:50:33 nooga: Programs are for humans first; machines second. P.S. That machines are imperative is a mistake of history. 17:50:38 See http://www.cs.york.ac.uk/fp/reduceron/. 17:50:48 i know i know 17:50:55 nooga: And "common sense" is a term people use when they wish to portray an opinion as immediately obvious, without giving any logical reasoning to this. 17:50:59 if we had purely functional machines it would be sooo cooool 17:51:03 We do. 17:51:12 yeah... like 17:51:28 MIPS, x86, eeee, SPARC.... eee 17:51:35 none of them 17:51:41 nooga: http://www.cs.york.ac.uk/fp/reduceron/ 17:51:51 but nobody uses it! 17:51:55 nooga: if we had OS X and Linux it would be soo cooool 17:51:58 elliott, so what way of doing IO would you prefer? 17:52:01 nooga: but we don't, because 90% of people use Windows! 17:52:03 drat! 17:52:06 too bad OS X and Linux don't exist 17:52:09 go home everyone 17:52:11 Phantom_Hoover: FRP 17:52:29 Phantom_Hoover: (but that question isn't really relevant; you do not have to suggest something better to hold the opinion that something is bad) 17:52:52 17:50 < elliott> nooga: Programs are for humans first; machines second. P.S. 17:53:00 elliott: hmmmm 17:53:09 j-invariant: almost direct sicp quote :) or was it R5RS... whatever 17:53:13 it's true wherever it came from 17:53:14 elliott, but the fact that there seems to be no viable alternative makes complaining rather pointless. 17:53:18 Phantom_Hoover: FRP 17:53:29 I know. 17:53:44 Phantom_Hoover: and that's sort of like dismissing the inventors of ${first purely functional language} because "Well, you haven't offered any replacements for ALGOL constructs like 'while'!" 17:54:15 It _is_ relevant to complain that an existing solution is bad; innovation has to handle the rest. 17:54:22 elliott: Ideas for a better "haskell"CCC? 17:54:31 j-invariant: are those Cs typo? 17:54:37 yes 17:55:54 j-invariant: Some syntax tweaks. Make named fields in records be handled much better (make them proper accessor objects, there are a bunch of things on hackage that do good-looking things for this); ditch IO monad replace with FRP integrate into my perfect OS :-P (you can't really do any of this perfectly in an imperative OS); get rid of typeclasses, replace them, and the "module" system, with a proper ML-style module system with modu 17:55:54 le functors and the like -- also maybe some ideas from Ur in this area -- ... 17:55:57 j-invariant: make it epigram ... 17:56:04 j-invariant: ... and then make it epigram some more 17:58:19 bah 17:58:20 j-invariant: also: redo the whole stdlib 17:58:31 j-invariant: proper numeric typeclasses (except, module signatures now, not typeclasses!) 17:58:34 I'm a fan of not having an stdlib 17:58:43 yeah 17:58:47 j-invariant: maybe if you don't want a useful language :) 17:58:51 j-invariant: fine in Coq, not for Haskell ... 17:59:18 The first thing I do in Coq is turn off the massive stdlib and bootstrap my own tools :P 17:59:29 same with haskell 17:59:32 j-invariant: that's just because coq's stdlib is really shitty 17:59:37 me and stdlibs... we don't get along 17:59:40 j-invariant: and also because you presumably don't write actually useful Haskell programs ;) no offence 17:59:42 yes that's the point 17:59:42 HOW AM I SUPPOSED TO WRITE ANYTHING WITHOUT IO THAT CAN BE SYNCED WITH OTHER SYSTEMS 17:59:47 they tend to be shitty 17:59:55 nooga: i don't give a shit about your needs/wants :) 18:00:04 in @ it all works out perfectly of course. 18:00:14 how do you imagine purely functional OS 18:00:25 @ 18:00:27 elliott: I mean you should still be able to do "import Numbers" or whatever it is you want 18:00:30 also see Urbit 18:00:43 elliott: but all this e.g. "Num" crap shouldn't be imported to all programs automatically 18:00:45 j-invariant: I think it's useful to have a decent base built in... no point starting with a lot of useless import declarations 18:00:50 j-invariant: Num is crap, but if it were better designed ... 18:00:52 elliott: what @ 18:00:54 nooga: @ 18:01:02 :@ 18:01:07 elliott: I don't think language designers are capable of making a good stdlib 18:01:28 j-invariant: as a language designer I think they are :) but i guess you could call me a language designer and a library designer 18:01:35 also the evolution of the language is at a different pace than that of the stdlib 18:01:43 not in @ :) 18:01:58 @ updates are almost as likely to update the language as the core stdlib, I'd say 18:02:12 @? 18:02:17 @. 18:02:25 Pronounced "@". 18:02:37 @ is a macro expanding to whatever the final name of @ has. 18:02:38 *is. 18:03:14 oh great 18:03:26 does it have a homepage? 18:03:37 no, it has no need of one. 18:03:41 the channel logs are an okay start. 18:04:05 nonexistant, useless 18:04:23 nooga: I don't care about your needs/wants. 18:04:48 elliott, but tonnes of the discussion was in private queries! 18:05:18 hmm, @ has the deficiency of being hard to grep 18:05:41 10.09.19:07:41:54 alise: start writing aliseOS plz 18:05:45 But I thought it was *useless*. 18:08:55 Phantom_Hoover: i hire you to work on it 18:09:09 elliott, no dice! 18:09:15 Phantom_Hoover: why 18:09:54 elliott, because dice killed my family. 18:10:01 Phantom_Hoover: don't use dice then 18:10:13 elliott, I CAN'T 18:10:15 * Phantom_Hoover sobs 18:12:20 -!- BeholdMyGlory has quit (Remote host closed the connection). 18:13:53 elliott: what about Idirs http://www.cs.st-andrews.ac.uk/~eb/ 18:14:06 closer to epigram than haskell 18:14:22 j-invariant: i know of idris yeah it seems kinda cool but i'm not convinced that full dependent types are a good thing in practice 18:14:44 huh? TRAITOR! 18:14:47 j-invariant: something like Ur/Web where you could write the /Web part yourself (i.e. code in all those static checks) -- that might be good -- it seems to have like 75% of what you'd want of dependent types in practice 18:14:54 but is more, you know, decidable :) 18:14:58 j-invariant: nonono i love dependent types 18:15:01 cough 18:15:04 j-invariant: for theorem proving and formal verification and shit 18:15:17 j-invariant: i just think a 75% + stuff solution might be best for everything else 18:15:33 elliott: even to use something as simple as quotient types, I think you need full blown theorem proving 18:15:46 j-invariant: are quotient types that useful outside of theorem proving? 18:15:48 serious question 18:17:18 either j-invariant is having a worldview breakdown or has shunned me 18:20:15 actually you killed the whole channel *sputter, argh* 18:20:35 * Phantom_Hoover swatpans oerjan's courpse. 18:20:38 *corpse 18:20:48 He was too good for this sinful earth. 18:21:00 BRAINS. 18:21:13 MY GOD 18:21:20 MY SWATPAN IS MAGICAL 18:21:31 ...if you say so. 18:27:17 elliott: how does this work?: 18:27:25 j-invariant: ? 18:27:44 module Z (inject, (+), (*)) where type Z = (N,N) ; inject :: N -> Z ... 18:28:01 j-invariant: what's that from 18:28:02 j-invariant, is that... Agda? 18:28:11 nah doesn't look like it 18:28:19 elliott, yes it does. 18:28:23 no, it looks like haskell 18:28:26 uh it was meant to be haskell but now that I write it i'm not sure if it means what I wanted it to 18:28:27 i hate 2011 18:28:31 Although with less Unicode and underscores. 18:28:38 j-invariant: are you trying to demonstrate ML modules or? 18:28:39 http://wronki.pl has AD 2011 bug :F 18:28:41 or are you just asking a really vague question 18:28:43 no nevermind 18:28:43 nooga, yeah, it's so BORING. 18:28:48 j-invariant: nono i want to understand 18:28:53 forget that code Ill start again 18:28:57 and i did it ;f 18:28:58 ok 18:29:07 elliott: you can define integers as a quotient on pairs of natural numbers (you know that?) 18:29:16 just as a simple example 18:29:21 ifeq ($(shell expr "$(uname_R)" : '[15678]\.'),2) 18:29:21 OLD_ICONV = UnfortunatelyYes 18:29:21 endif 18:29:24 --git Makefile 18:29:25 j-invariant: yep 18:29:42 j-invariant: well the Works But Kind Of Horrible solution here is obvious 18:29:42 elliott: so in haskell you might well use this approach, not exporting the definition of Z but exporting functions to work with it 18:29:45 j-invariant: just define your own (==) 18:29:45 yep 18:29:59 then MyModule imports that, uses the functions with Z to its hearts content and all is well 18:30:03 yep 18:30:47 by all is well, I mean that every function MyModule can define respects the equivalence relation 18:31:17 yes 18:31:23 you can't prove this in Coq 18:31:29 indeed 18:31:56 this makes no sense 18:32:29 j-invariant: what doesn't 18:32:38 well Coq's knowledge of modules is limited i think 18:32:53 oh wait a second, it might be possible to prove this in Coq 18:33:22 if you implement a non-quotient version of Z and make a map between that and the quotient version 18:34:34 I need to try this out 18:34:55 nooo nooo nooo 18:35:00 boring boring boring 18:35:03 i can't work 18:36:34 -!- zzo38 has quit (Quit: All the letters on one side OK). 18:38:37 j-invariant: have you ever looked at Clean? 18:44:07 fizzie, what does this mean? 18:56:48 [DIED] world.c: 108: broken decompressed chunk length: 49 != 50 18:44:30 chunk was meant to be X long, it was Y. i would presume. 18:44:37 hm 18:44:47 elliott, Vorpal, fizzie, Deewiant, has anything actually been done on the MC server? 18:44:50 elliott: no 18:44:54 Phantom_Hoover: since when 18:45:00 j-invariant: ok 18:45:03 elliott, lately? 18:45:07 The last week or so? 18:46:37 fizzie: can i rewrite mcmap in ML or something 18:50:16 elliott, won't that have a lot of overhead if your system is already having some problem with running both minecraft and mcmap at once? 18:50:28 Vorpal: not if I compiled it with MLton :) 18:50:37 elliott, oh? 18:50:55 elliott, what is MLton? 18:50:58 jfgi 18:51:30 elliott, hm is it really that good? 18:51:46 good enough 18:52:06 not like mcmap is hugely resource-intensive or hugely speed-needing 18:52:49 elliott, true, I was thinking of memory overhead 18:53:04 elliott, which is the problem for me with minecraft alone 18:53:23 well, these sorts of compilers usually try and unbox everything. 18:53:36 try to yes 18:53:56 -!- Zuu has joined. 18:54:00 -!- Zuu has quit (Changing host). 18:54:01 -!- Zuu has joined. 18:54:13 how well does it manage though 18:54:47 It's not like unboxing is hard. 18:55:00 * Zuu unboxes elliott 18:57:21 FWIW, I think we should try proper survival multiplayer. 18:57:51 elliott killing Vorpal every 10 seconds by "accident" would be rather amusing. 18:58:14 Phantom_Hoover: When the SMP server was up, I killed ineiros and got 64 mob spawners 18:58:17 Alas, they spawned only pigs. 18:58:36 elliott, there *was* an SMP server up? 18:58:41 Phantom_Hoover: Yes, for something like a day. 18:58:52 Phantom_Hoover: Vorpal is too pussy to go on though. He'd just sit on IRC crying about his house. 18:59:00 (Side note - if we do - it must be on the same map.) 19:02:31 Vorpal: It means the zlib truncation bug I tweeted (but Notch ignored) has actually resulted in an incomplete chunk update. 19:02:59 fizzie: Notch, fix actual bugs? 19:03:04 Hahahahahahahahaahahahahahahhahahahahahahahahaha 19:03:17 Too busy getting internet fellatio from Twitter. 19:03:46 I may fix it to ignore those too, as long as the truncation affects only the light values, which I ignore. 19:03:53 Vorpal: It means the zlib truncation bug I tweeted (but Notch ignored) has actually resulted in an incomplete chunk update. ← what are you responding to? 19:04:05 Phantom_Hoover: fizzie, what does this mean? 18:56:48 [DIED] world.c: 108: broken decompressed chunk length: 49 != 50 19:04:06 Phantom_Hoover, to me 19:04:14 and I'm not a what 19:04:15 Vorpal, WELL DUH 19:05:58 Yes you are. 19:06:22 Notch can't code 19:06:53 nooga, we know that better than you. 19:07:18 j-invariant: have you finished epigram yet 19:07:40 For instance, there's a bug which will crash any server whatsoever and can be done with effectively no privileges. 19:08:01 No, I'm not saying what it is, and noöne else who knows should either. 19:08:34 Phantom_Hoover killed a server with 1,000 people on it permanently once with that bug. True story!* 19:08:35 *False story 19:09:03 true for very false values of 'true' 19:16:05 solution 19:16:07 : 19:16:15 reimplement minecraft 19:16:46 nooga: NETCRAFT 19:16:48 coppro: NETCRAFT 19:16:50 confirms it 19:19:11 -!- Zuu has quit (Ping timeout: 260 seconds). 19:19:22 where 19:20:21 elliott: I don't work on epigram 19:20:27 j-invariant: well get crackin'! 19:20:30 :) 19:20:32 -!- Zuu has joined. 19:20:35 elliott: parametrized modules 19:20:56 elliott: if I have an isomorphism between M and M', then why don't I have an isomorphism between F(M) and F(M')? 19:21:00 Coq is stupid. 19:21:12 j-invariant: Because Coq is stupid. 19:21:15 does epigram have this? 19:21:25 j-invariant: Epigram has everything! Including kittens! Nah, I don't actaully know. 19:21:26 *actually 19:21:41 elliott: if I could get an isomorphism between F(M) and F(M') I could have something like useful quotients 19:22:08 j-invariant: Doesn't every Coq story starting with "So I had this idea to implement quotient sets..." end with "...and it didn't work"? 19:22:19 maybe I should apply that mu- thing to a language with modules 19:22:26 XD 19:22:38 mu- thing? 19:22:54 it's smoe magic way to turn a programming language into a dependently typed one 19:23:25 they did it to a sort of haskell liek language and got a simple version of agda out 19:23:42 j-invariant: what happens when you apply it to C 19:23:46 if we throw modules in maybe we'll get quotients out 19:23:48 does it kill you and your family? 19:23:50 elliott: well it has to be a lambda calculus 19:23:53 j-invariant: LAME 19:23:58 the C calculus :D 19:24:15 who does NETCRAFT 19:24:32 coppro (coppro is the entire u/waterloo) 19:24:44 is it open? 19:24:54 it's NETTTTTTULATORY 19:24:56 OF HTHE THWEOITH IOEDFJHDFGMLKDFGNHDKL;FGH 19:24:59 check their website for opening hours 19:25:03 elliott: excerice, prove the theorem http://pastebin.com/6P2ydkcU 19:25:03 ;) 19:25:37 Vorpal: ... 19:25:49 j-invariant: for your homework, prove goldbach's conjecture 19:25:56 elliott, well oerjan seemed afk 19:25:59 well,* 19:26:25 j-invariant: hmm 19:26:39 um 19:26:41 j-invariant: (+,N):Z :: (*,Z):Q :: (^,Q):?? 19:27:02 netcraft is an internet services company based in england 19:27:17 nooga doesn't know who netcraft are lol 19:27:23 nooga is young netcraft confirms it 19:27:25 heh 19:27:40 ^ isn't QxQ -> Q though 19:27:41 j-invariant: what's ?? :) 19:27:45 j-invariant: oh indeed 19:27:46 j-invariant: darn 19:27:54 j-invariant: (+,N):Z :: (*,Z):Q :: (^,Z):?? 19:28:22 j-invariant: it's easy to show that you can define an inverse-making-quotient operation given an operator and a set obeying a few rules and that f(+,N)=Z and f(*,Z)=Q... this much is obvious 19:28:32 j-invariant: just wonder what happens when you put in (^,Z) 19:28:32 hmm 19:28:33 well 19:28:38 (a,b) represents a-b or a/b 19:28:38 so 19:28:48 we were talking about minecraft reimplementation, not a company with rainbow logo 19:28:50 (a,b) represents a((^)^-1)b 19:29:08 so is it just log_a(b)? 19:29:59 well 19:30:03 I think so 19:30:11 (1/x,e) = x 19:30:13 er no 19:30:19 j-invariant: you work out what comes out :P 19:31:07 well obviously (x,x^n) = n 19:31:11 hm 19:31:24 waiit 19:31:38 it's actually (x^n,x) = n 19:31:40 obviously 19:31:45 j-invariant: halp 19:31:52 confusion 19:31:57 right okay 19:32:00 (x^n, x) = n 19:32:07 obviously it's log_b(a) 19:32:11 for (a,b)... 19:32:30 hm 19:32:34 is it closed 19:32:45 WHO KNOWS 19:32:57 j-invariant: i think it's just Q with log to be honest... but then Q is just Z with divide 19:34:44 -!- elliott has quit (Remote host closed the connection). 19:34:52 -!- elliott has joined. 19:35:03 j-invariant: does the mu thing have to be a lambda calculus strictly? 19:35:07 or can any similar-ish structure do 19:35:13 I'd love to see a dependent-typed term rewriting language 19:37:04 elliott: Realizability and Parametricity in Pure Type Systems 19:37:25 j-invariant: that'd require actual thought!!!! 19:38:58 We describe a systematic method to build a logic from any 19:38:58 programming language described as a Pure Type System (PTS). The 19:38:58 formulas of this logic express properties about programs. We define a 19:38:58 parametricity theory about programs and a realizability theory for the 19:38:58 logic. The logic is expressive enough to internalize both theories. Thanks 19:39:00 to the PTS setting, we abstract most idiosyncrasies specific to particular 19:39:03 type theories. This confers generality to the results, and reveals parallels 19:39:05 between parametricity and realizability. 19:39:08 awesome 19:39:38 and it cites View from the Left 19:39:45 therefore its' MEGAawesome 19:40:09 j-invariant: i wish i was cool enough to have my own dependent language :p 19:40:27 you can! 19:40:32 j-invariant: o rly 19:40:40 just pick some esoteric PTS nobody cares about and apply this paper to it 19:41:01 j-invariant: bah -- i still want a language based on dual-intuitionistic logic 19:41:05 j-invariant: paraconsistent type system, how cool is that? 19:41:13 function arrow replaced with "butnot" 19:41:23 -!- BeholdMyGlory has joined. 19:41:59 j-invariant: hmm maybe i will try hacking up a dependent language 19:42:01 it sounds like fun 19:42:22 elliott: one with delimited continuations? 19:42:31 you can prove stuff that Coq and Agda can't prove if you do that 19:42:31 j-invariant: you can implement them on top of a language can't you? 19:42:35 huh 19:42:47 j-invariant: i don't wanna start doing tactics and shit so maybe proving isn't what i should focus on for now :) 19:42:49 but that sounds fun 19:42:52 there's this paper about it I don't really get it but an implementation would be interesting 19:42:52 * elliott waits for ghc to finish compiling 19:43:01 I just mean typing out lambda terms to prove things 19:43:07 right 19:43:50 j-invariant: maybe i can write a lazy specialiser for it and i will have succeeded in creating the Best Language :) 19:45:20 j-invariant: I wish Scheme was a better language because Ponzi Scheme is an awesome name 19:45:30 heh 19:45:42 i mean i have to write it 19:45:45 even though i don't really want to 19:46:03 ok so scheme is actually pretty nice 19:46:13 http://esolangs.org/wiki/Brainfuck/w/index.php%3Ftitle%3DTalk:Brainfuck/index.php#Implementation i'm proud of this code, for all the awful shit it does it's pretty 19:46:58 -!- pikhq has joined. 19:47:11 Grawr.\ 19:47:33 pikhq: I found out how to use stow with packages that refuse to even give you the time of day if you change the prefix. 19:48:06 elliott: Oh? 19:48:59 pikhq: ./configure --prefix=/usr/local && make && make install DESTDIR=root && mkdir /stow/foo && cp root/usr/local/* /stow/foo 19:49:10 Just about everything supports DESTDIR so this works great. 19:49:17 (Even Python's setup.py does.) 19:50:34 pikhq: Do I win a prize? 19:53:55 j-invariant: you know that de-bruijn-for-bound-stuff-names-for-unbound-stuff? 19:54:10 huh 19:54:14 j-invariant: that the epigram people do 19:54:23 I am not a number, I am a free variable 19:54:25 or something 19:54:34 what about it 19:54:36 j-invariant: am i weird if i think we should just get rid of all non-local variables and just rewrite everything as a single lambda application 19:54:38 i.e. 19:54:41 x=y;foo=bar 19:54:43 should just be 19:54:47 yes LOL 19:54:52 (\x->(\foo->...)bar)y 19:54:57 j-invariant: not as in, the actual code we write! 19:55:01 but i think compilers should do it like that 19:55:04 so i'm weird right 19:55:18 i mean an assignment like that is basically a let around the whole program 19:55:20 if everything is a lambda, then you can't step inside an abstraction cayou? 19:55:25 and let x=y in z is just (\x->z)y 19:55:28 j-invariant: why not 19:55:38 because it's just another lambda in side? 19:55:47 j-invariant: that isn't really what i mean 19:55:51 j-invariant: i don't mean every object should be a lambda 19:56:09 j-invariant: I just mean that there should be no assignment or anything, it should just be lambda application to a constant :p 19:56:19 and have everything be de bruijn 19:56:26 it's simpler to process :D 19:56:58 if you can get away with it, do it! 19:57:13 "I'd like to thank this /r/programming thread http://bit.ly/eNygOX for helping me adjust to senescence." --pigworker 19:57:20 guess what thread it is 19:57:24 I can guess :P 19:58:18 j-invariant: one issue with doing bindings in this way is that the order you choose is totally arbitrary ... and everything that passes some parameters to a module, if you add something to that module, all those break because the order changes 19:58:21 BUT THAT'S BORING PRACTICAL PROBLEMS 19:58:42 obviously we just redo every single piece of code every time a single byte changes 20:03:49 j-invariant: quick, what should i put in my silly language 20:04:10 quotients 20:04:25 j-invariant: that sounds really painful to do :> 20:05:16 j-invariant: (is it?) 20:05:22 no it shouldn't be difficult 20:05:34 j-invariant: can i add them after everything else or should i really do them first 20:05:45 it just needs to be done early 20:05:48 hmm 20:08:59 j-invariant: i am getting slightly disillusioned with all the provers :-. 20:09:01 *:-/ 20:09:16 elliott: so am I but I try to hide it 20:09:22 haha 20:09:39 j-invariant: let's go back to ridiculously dynamically typed, late-bound languages and write unit tests 20:09:48 unit tests? HAH 20:09:53 I don't /test/ 20:09:58 j-invariant: Unit tests prove goldbach!!!!!! 20:10:02 i ran 10^30 of them 20:10:04 all passed 20:10:17 j-invariant: (if I keep this up I'll turn into Zeilberger) 20:10:20 that's such a weird thought 20:10:21 * pikhq is still completely blown away by the recent PS3 hack... 20:10:29 or Chaitin... "Add an axiom!" 20:10:49 what PS3 hack? 20:11:15 Phantom_Hoover: http://i.imgur.com/rwmHO.png The PAXEL 20:11:18 elliott: oen of my concerns is how large scale programming can work 20:11:35 j-invariant: The hack by fail0verflow, which contains all of Team Twiizers, detailed at 27C3 recently. 20:11:39 elliott: category theory may be the solution to it 20:11:40 j-invariant: this is why i was talking about a 75% solution for all the not-just-pure-proving work 20:11:42 j-invariant: Well, rather, the *set* of hacks. 20:11:56 j-invariant: like, I don't look at Idris or Ur and think "will this scale to bigger things..." 20:11:58 j-invariant: The most hilarious one is that they have the signing key now. 20:12:18 wow 20:12:52 You see, Sony signs things using ECDSA, which requires, as part of the algorithm, a cryptographically secure random number. 20:12:59 Sony, however, uses a *constant* instead. 20:13:10 haha 20:13:14 Which allows you to get the private key using simple algebra. 20:13:49 "Sony seem to have just randomly sprinkled crypto on the PS3 as magical pixie dust. Wackier crypto usage MUST be more secure, right? Right?" 20:13:52 So, the PS3 is as hacked as it is possible to be. 20:15:14 that is incredible 20:15:19 They also discovered a handful of buffer overflows in un-reflashable code that would allow one to make a mod chip that Sony couldn't do anything about, but that kinda pales in comparison to it being *literally impossible* for Sony to do anything about everyone being able to sign anything. 20:15:22 Phantom_Hoover: http://i.imgur.com/rwmHO.png The PAXEL ← WANT 20:15:36 pikhq: I guess the PS3 devs grew up writing websites that don't santies SQL inputs 20:16:15 Phantom_Hoover: there's actually a mod for it lol 20:16:18 except it looks slightly less silly 20:16:28 elliott, WE MUST INSTALL IT 20:16:29 j-invariant: obviously we can solve that with DEPENDENT TYPES 20:16:32 Phantom_Hoover: client only 20:16:50 elliott, NOOOO 20:17:01 It is, in fact, more hacked than the Wii now. 20:19:55 Phantom_Hoover: http://dl.dropbox.com/u/14765180/AnimalCrafting/screenshots/animalcrafting16.png WORST TEXTURE PACK 20:20:34 elliott, what is that stuff meant to be? 20:20:42 Phantom_Hoover: Gravel. Seriously. 20:20:54 http://i.imgur.com/1Z1Bw.jpg omg that reminds me i need to install ambient occlusion. and painterly. 20:21:28 That animalcrafting16.png reminds me of one of the early 3D Sonics, for some reason. 20:21:44 it's animal crossing methinks 20:22:01 Phantom_Hoover: lol the reddit thread is filled with OMG WHAT TEXTURE PACK 20:22:04 it's painterly you idiots 20:26:03 wut 20:26:18 what 20:26:40 so what;s with this reimplementation 20:27:09 nooga: what reimplementation 20:28:22 Phantom_Hoover: On CMOS in Minecraft: "This is the best idea in the history of minecraft. Or at least slightly behind the idea of the character being able to pee, I think that is important also." 20:28:34 CMOS? 20:28:43 http://www.minecraftforum.net/viewtopic.php?f=1&t=45590 20:30:13 fizzie: Phantom_Hoover: http://getsatisfaction.com/mojang/topics/will_here_be_dragons_or_other_flying_mobsters_in_the_air_in_the_berworld#reply_4040443 20:30:17 Oh god I cannot stop laughing 20:30:25 elliott: reimplementation of minecraft 20:30:53 elliott, that is the best dragon ever. 20:31:02 Phantom_Hoover: He is so happy. Unintentionally. 20:31:03 it's funny how everyone left digg for reddit, now people rae leaving reddit 20:31:08 j-invariant: For what :p 20:31:17 Phantom_Hoover: Also nothing like a dragon at all which is just amazing. 20:31:19 there doesn't seem to be anything 20:31:25 Phantom_Hoover: ahahahaha oh god i just saw his eyes 20:31:27 http://blog.tmorris.net/bye-reddit/ 20:31:29 Phantom_Hoover: I thought the eyes were the nostrils 20:31:31 at the front 20:31:47 j-invariant: that was the guy who said he was going to kill himself in all the irc channels he was in a few years ago. 20:31:59 j-invariant: that's what I know him for :-P 20:32:04 * elliott reads post 20:32:35 hehe 20:32:45 :D 20:33:01 j-invariant: i wonder why because of quad's post ... it's supremely idiotic but isn't it obvious that nobody actually agrees with him? 20:34:04 heh ... just checked hacker news 20:34:08 that idiot kroc camen is at #1 20:34:12 IS NOWHERE SAFE 20:35:03 kroc camen? 20:35:07 Phantom_Hoover: this idiot. 20:35:08 Cabal-1.10.0.0-8b2e042500a42b47b6b121795bb9262f is unusable due to missing or recursive dependencies: 20:35:09 process-1.0.1.4-2a42745dbb9dd3c8087608f127411124 20:35:22 ?? 20:35:47 j-invariant: what 20:40:00 elliott, which idiot? 20:40:06 an idiot 20:44:29 elliott, that's quite possibly the least specific identifier EVER. 20:44:45 Phantom_Hoover: an entity 20:45:06 *non-obviously-flippant 20:45:41 i flip ants 20:46:03 Phantom_Hoover: please please please get Ubuntu working on this. 20:46:29 elliott, no. 20:46:57 Phantom_Hoover: why 20:47:20 elliott, you betrayed Debian in a Sgeoesque display of infidelity! 20:47:27 Phantom_Hoover: BAH 20:47:30 *Sgesque 20:53:27 elliott, also, you are a stooge of SHUTTLEWORTH 20:53:28 Yay, got that AONT code written (uses AES and SHA-256)... 20:53:35 Phantom_Hoover: *WORTHY SHUTTLE 20:53:56 elliott, YOUR TIME AT HOOVER HEAVY INDUSTRIES IS AT AN END 20:54:04 Phantom_Hoover: OK. Can I still steal TNT? 20:54:04 Ilari, you can be his replacement! 20:54:24 elliott, you can't use company TNT unless you concede that Shuttleworth is EVIL. 20:54:45 Phantom_Hoover: Of course he is. http://geekz.co.uk/lovesraymond/archive/cancomical-lynchpad 20:55:03 elliott, welcome back to HHI! 20:55:17 Phantom_Hoover: I don't want to join until you read every Everybody Loves Eric Raymond comic ever. 20:55:35 elliott, I've read most of them, if not all. 20:55:56 I wonder if there will ever be a new one. 20:56:14 "December 21, 2012 – A new ELER strip is published. 20:56:14 Sometime after, millions of *nix administrators die of a shock induced heart attack, and critical infrastructure is left unmaintained. Major companies go bankrupt as their servers succumb to threats normally mitigated by vigilant admins. The economies of the United States and the European Union collapse. Major military powers blame the incident on Chinese cyberwarfare, and invade the nation. Nuclear war ensues." 20:56:20 I... that... is actually plausible. 20:56:22 Certainly, all the links are purple. 20:56:29 ACTUALLY PLAUSIBLE. 20:57:04 "Checked ELER for update, as friend asked me had I seen latest post. Friend is now on a certain list. Oh yes…." 20:57:28 Phantom_Hoover: http://esr.ibiblio.org/?p=2575#comment-279450 "while arguably, I *am* in fact a world-changing figure" --esr 20:59:22 ESR SO CRAZY 20:59:37 The fact that the man is allowed anywhere near a gun is something I will never understand. 21:00:13 [[His highly respectable work and expertise in computer technology has been all but overshadowed by his batshit insane wingnut tendencies in the wake of 9/11]] — RW on ESR 21:00:19 Highly respectable HAHAHAHAHAHA 21:00:46 -!- poiuy_qwert has quit (Quit: This computer has gone to sleep). 21:02:11 * elliott corrects 21:02:48 Pleasepleaseplease do that. 21:03:05 Phantom_Hoover: http://rationalwiki.org/w/index.php?title=Eric_S._Raymond&diff=707432&oldid=695156 21:03:10 Phantom_Hoover: ADD A NEW REVISION ON TOP BEFORE HUMAN REVERTS ME 21:03:39 "The worst part of all is that he blames Alan Turing for his judicial punishment and suicide, even though Raymond, like every other computer programmer, owes Turing his career." 21:03:42 He does? Ha 21:03:47 Phantom_Hoover: AD DA REVISION ADD A REVISION QUIIIICK 21:03:50 IT WON'T LAST LONG 21:03:55 what the hell? 21:04:02 el 21:04:05 elliott, http://rationalwiki.org/wiki/Talk:Eric_S._Raymond#Utter_madness 21:04:12 he doesn't owe Turing anything 21:04:18 what an absurd statement 21:04:24 j-invariant: it's rationalwiki it can't be right 21:04:25 Note David Gerard's statement. 21:04:26 or sane or reasonable or 21:04:51 elliott, OTOH, he was saying that "Turing was asking for it", which is appalling beyond words. 21:05:01 Phantom_Hoover: Who cares — the article is already crap anyway. 21:05:04 [[Um, no. INTERCAL is one of the things that is ESR working in his sphere of powerful competence.]] 21:05:04 "His highly respectable work and expertise ..." ~~> "His questionable work and expertise in computer technology ..." hahahaha 21:05:09 lol 21:05:19 Phantom_Hoover: Add a damned revision to the article already so mine doesn't get reverted. 21:05:24 Just tweak the formatting of my edit :P 21:05:25 HE MERGED SOME GIT HUBS SO POWERFULLY COMPETENT 21:05:33 Phantom_Hoover: ^^^^ 21:05:33 Er, s/HUBS/THINGS/ 21:05:49 Phantom_Hoover: Also TO BE FAIR he did originally write C-INTERCAL, but the code wasn't very ... good. 21:06:56 pikhq: So, is there any actual obstacle to using stow? 21:07:17 elliott, done. 21:07:21 Phantom_Hoover: yay 21:07:36 Phantom_Hoover: Hey, you removed the amusing bit. 21:07:40 Oh, just footnoted it. 21:09:35 elliott, [[I do not like this article because it does not sufficiently acknowledge what ESR is good at and famous for. He wrote large chunks of libgif and libpng - without him your web browser would be a much sadder place. He has code in every Linux-based gadget you use - if his contributions disappeared, your broadband modem and even your television would be bricks.]] 21:09:43 — David Gerard 21:09:49 Phantom_Hoover: Seen, yes. What of it? 21:09:58 elliott, is this complete crap? 21:10:21 Phantom_Hoover: I think it's factually correct (probably), but it doesn't really matter much. 21:10:29 Parsing GIFs and PNGs is not some huge innovation. 21:10:49 Phantom_Hoover: Also it doesn't invalidate my footnote which states that it's /hard/ to find such a list which is true. 21:11:15 I have some kind of negative thought linked to David Gerard's name in my head but I don't know why. 21:12:48 j-invariant: maybe i'll use my crazy Transaction type in this lang 21:13:56 Fun stuff with AONT: Pad messages to fixed size and do AONT on each. Pick HMAC key for each message, chunk messages and compute HMACs for chunks and append the MACs to chunks. Then perform random in-order merge of chunks. If there are enough chunks per message and at least 2 messages, that's difficult to untangle without HMAC keys. 21:14:34 elliott, David Gerard has been... not trolling, but being a pain at Less Wrong. 21:14:51 For extra fun, couple chunks containing random data can be added... 21:14:52 elliott: Uh, other than symlinks sucking, no. 21:15:06 Phantom_Hoover: Howso? 21:15:14 pikhq: I wonder how the GNU System guys didn't think of using DESTDIR. 21:15:27 elliott: They do. 21:15:35 elliott, not sure. Look at the RW LW articles: he wrote a great deal of them. 21:16:05 Phantom_Hoover: You mean [[Less Wrong]] on RationalWiki? 21:16:07 Basically, that allows making data undecode multiple ways with possibilty of junk that just doesn't undecode. 21:16:12 elliott, yes. 21:16:24 Phantom_Hoover: Scared to do that — Reddit Atheists react explosively when confronted with people who are actually rigorous about it. 21:16:33 elliott, he's also part of the Wikipedian Bureaucracy. 21:16:39 Found that by Googling. 21:16:46 -!- Sasha2 has quit (Read error: Connection reset by peer). 21:17:28 -!- Sasha2 has joined. 21:17:44 Phantom_Hoover: '"rationalists"'. 21:17:49 Oh scare quotes. 21:17:55 pikhq: Then ... why is it blocking a release? 21:18:24 Phantom_Hoover: Aren't you an admin? 21:18:43 Phantom_Hoover: Oh wait, I forgot, RW goes by the Wikipedia Administration model, where admins are given endless powers but actually using them is taboo. 21:18:45 elliott, at RW? Sure, but the criteria for that are more or less the same as for autoconfirmation. 21:18:47 /troll 21:19:13 elliott: A) They don't *want* to use stow. B) stowfs does not work yet. 21:19:17 http://rationalwiki.org/w/index.php?title=Special%3AListUsers&username=&group=sysop&limit=50 21:19:20 Phantom_Hoover: Dear god how many are there. 21:19:26 elliott, a few hundred. 21:19:36 Phantom_Hoover: Over 500. 21:19:38 FWIW, I'm also a bureaucrat for reasons unclear to me. 21:19:43 Phantom_Hoover: Do they realise that they have almost as many sysops as Wikipedia? 21:19:46 Or maybe even as many? 21:19:51 elliott: C) That's not actually a major blocker; a major blocker is that HARDLY ANYTHING ACTUALLY HAPPENS WITH IT AT ALL. 21:20:05 pikhq: From using stow I actually kinda like it... 21:20:14 elliott, you fail to understand that a significant driving force behind RW's policy is being the opposite of Conservapedia. 21:20:23 Phantom_Hoover: RATIONALWIKI PREDATES CONSERVAPEDIA (iirc) 21:20:35 Yeah, the symlink thing is the only really *bad* thing about stow, and it's not *that* bad... 21:20:37 elliott, erm... no it doesn't. 21:20:46 Phantom_Hoover: It doesn't? Well that explains ... a lot. 21:21:13 Phantom_Hoover: I guess nobody realised that the opposite of Conservapedia is LiberalUnjustifiedNutjobPedia. 21:21:33 elliott, naw, that exists too, it's just *profoundly* unfunny. 21:21:47 http://liberapedia.wikia.com/wiki/Main_Page 21:21:52 Phantom_Hoover: It exists and it's called RW. Also isn't that Lumenos' thing? 21:22:10 Imagine a female zzo. Then imagine her attempting to be funny. 21:22:11 If you say "but RW is humorous", well ... I can't bring myself to take Conservapedia seriously either. :P 21:22:33 Phantom_Hoover: "Libertarians aren't keen on illegal immigration, but liberals always sort them out." Err? 21:22:46 elliott, don't let it trouble you. 21:22:54 Phantom_Hoover: It just ... ist hat meant to be funny? 21:22:55 I don't get it 21:23:07 elliott, again, it was written by zzo's distaff counterpart. 21:23:21 Phantom_Hoover: Too man contractions 21:23:58 zzo? zzo38? 21:24:30 *many 21:24:33 Phantom_Hoover: I know. 21:24:35 Phantom_Hoover: I meant in the text. 21:24:37 Of Liberapedia. 21:24:44 Phantom_Hoover: [[If you indicate your disagreement with the local belief clusters without at least using their jargon, someone may helpfully suggest that "you should try reading the sequences" before you attempt to talk to them. The "sequences"[6] are several collated series of Yudkowsky's blog posts, and there are eighteen sequences in all. The indexes for just the four "core sequences"[7] are somewhere north of 10,000 words. Those 21:24:44 link to over a hundred and fifty 2,000-3,000-word blog posts. That's about 300,000-450,000 words for those four. For comparison, Lord Of The Rings is 454,000 words.[8] As such, "You should try reading the sequences" is LessWrong for "Godspeed" "fuck you."]] 21:24:49 Phantom_Hoover: tl;dr "Reading is hard"? 21:25:28 elliott, well, saying "read this hefty tome" in an argument isn't a very good idea. 21:26:08 Phantom_Hoover: It's sort of like expecting you to have read the Bible on a Christian debate forum ... (I know, I know, that choice of analogy is just giving ammo but I don't care.) 21:26:11 Phantom_Hoover: As bad as RationalWiki is the Richard Dawkins forum is worse. :p 21:26:54 elliott, of course. RW is at least /ostensibly/ without any opinion on religion. 21:27:32 Phantom_Hoover: In attempting to interpret that sentence of yours, my brain stumbled upon a world where the definition of "ostensibly" is "not". 21:27:41 Phantom_Hoover: Disturbingly that seems to be the real world. 21:28:38 elliott, well, there are quite a few theists, and they get along fairly well. 21:28:47 Phantom_Hoover: O god, the RW article mentions the Amanda Knox case. 21:29:14 Hmm? 21:29:21 Murder of Meredith Ketcher. 21:29:34 Phantom_Hoover: As far as I can tell the entire Richard Dawkins forum is united in considering Amanda Knox 100% guilty without actually presenting any evidence at all or... anything; the courts agree. Less Wrong is of the opposite opinion. 21:30:03 I can't actually understand _why_ the RD forum agrees except that Reddit Atheists have this strange tendency to put undue trust in authority, presumably because they also believe all the most popular scientific theories without actually looking into them themselves. 21:30:11 Such a strange world. 21:30:18 (And by that I mean the whole world.) 21:30:48 elliott, trusting the prevailing scientific theories is just the only way to get by in the world. 21:30:55 Phantom_Hoover: Certainly. 21:31:01 Phantom_Hoover: But it doesn't mean you should generalise that to "trust authority". 21:31:34 Phantom_Hoover: I don't have any /evidence/ that Reddatheists think this, but it's the only theory I can come up with for things like their absolute unwavering trust in, e.g. courts. 21:32:09 elliott, particularly odd, given that Dawkins himself is no fan of the legal system. 21:32:34 Phantom_Hoover: I love Dawkins. It's his fans I'm not too keen on. 21:34:16 Phantom_Hoover: BTW, the Amanda Knox thing is http://lesswrong.com/lw/1ir/you_be_the_jury_survey_on_a_current_event/ http://lesswrong.com/lw/1j7/the_amanda_knox_test_how_an_hour_on_the_internet/; those posts have links to the Richard Dawkins forum, but if you replace "Don't be stupid, everyone can see that Amanda Knox is insanely guilty" mentally that's pretty much the exact content of the RD threads. 21:39:28 It still irks me that they ask for probabilities. 21:42:38 Phantom_Hoover: The LW-consensus is that an aversion to giving numeric probabilities is basically an artefact of human wetware. 21:43:09 elliott, but... I mean, do they have calculations for it or what? 21:43:19 Phantom_Hoover: "Your probability *estimate*". 21:43:46 Phantom_Hoover: It's meant to be rough, just like any guesswork. Numbers aren't inherently "precise". Note: I am giving my perception of the LW consensus, not supporting it or agreeing with it. 21:45:18 eat 21:46:07 Hmm... Returning to that fan problem... At least CPU fan and main case fan both work... 21:46:37 (dunno about PSU fan) 21:46:41 elliott, incidentally, Ilari is now your subordinate at HHI. 21:46:52 Also, GPU fan appears to work... 21:46:56 HHI? 21:46:56 Ilari: Do whatever. The paychecks will come at regular intervals. 21:47:05 Phantom_Hoover: Is it bad to try and establish a utopia of laziness with my position? 21:47:17 Ilari: Hoover Heavy Industries, the most fake corporation of fakeness. 21:47:32 elliott, I'm still not sure what kind of entity it is. 21:47:46 Phantom_Hoover: It's a militacountrypany! 21:47:59 elliott, OMG HHI in Oolite. 21:48:14 Phantom_Hoover: OH GOD 21:48:15 *Oh god 21:48:36 Phantom_Hoover: I would really play an Oolite MMO... I realise it's a non-trivial problem but I would honestly subscribe to a pay-monthly Oolite MMO I think. 21:48:44 Phantom_Hoover: EVE is just so boring and hard to get into. 21:48:48 elliott, yeah, but even then. 21:49:01 Phantom_Hoover: Even then what. 21:49:12 Even in a world of Platonically ideal computers, Braben would sue the hell out of the people running the MMO. 21:49:45 He's hardly easy-going about the rights to Elite. 21:49:46 Phantom_Hoover: Even if the ship names were changed? Presumably it'd take place in a new world anyway. 21:49:55 Phantom_Hoover: You can't copyright gameplay itself. 21:50:07 Change the names, make new designs, redo the UI. 21:50:09 elliott, by this point you can always just look at Infinity and sigh. 21:50:20 Phantom_Hoover: Who cares about landing on planets. 21:50:34 elliott, there is actually an OXP that lets you do that... 21:50:43 Heh. 21:52:06 Although it basically just consists of flying into the planet and getting a docking effect. 21:52:59 What's there? 21:53:52 [[Go to your preferences, select monobook as your default skin and never again worry about the horrible new crap mediawiki wants to inflict on you. That's what I did, anyway. --JeevesMkII The gentleman's gentleman at the other site 15:18, 30 December 2010 (UTC) 21:53:53 :That's the right conservative attitude. --Idiot numbre 188 (talk) 16:26, 30 December 2010 (UTC)]] 21:53:56 I should stop reading RW, it's bad for me. 21:54:01 I even /like/ Vector but COME ON. 21:54:43 Well, Vector does have the font size problem. 21:55:00 "Font size problem"? 21:55:42 What is it with people and No True Scotsman. I see No True Scotsman misused more than I see actual No True Scotsman. 21:55:43 It is well-documented that the text is far far far smaller than Monobook's on many computers. 21:56:19 If Dawkins announced that he was a Christian, and then kept doing EXACTLY THE SAME THINGS HE DID BEFORE FOREVER, and someone said then RD wasn't actually Christian, someone would bring out No True Scotsman. 21:56:38 Just because he publishes books and speaks in public about how all religion is false doesn't make him not a Christian! SCOTSMAAAAAN 21:56:41 Phantom_Hoover: Really? 21:56:45 Phantom_Hoover: s/computers/browsers/. Probably. 21:56:50 I've never seen that. 21:57:17 I did when WP started using it. 21:58:08 Oh god I forgot how amazing http://www.youtube.com/watch?v=ZW2qxFkcLM0 is. 21:58:11 Admittedly, Vector has a smaller font size anyway, but it was more pronounced. 21:59:00 LOL 21:59:25 j-invariant: lol at the trailer? or 21:59:28 yes 21:59:31 this is hilarious 21:59:32 it's amazing :D 21:59:35 i would so have gone and seen it 21:59:45 it's a parody of a real film no? 21:59:56 j-invariant: it's the trailer to "2012", recut with bongos 21:59:59 and 70s 22:00:00 :D 22:00:16 Also stupid scrolling text. 22:02:49 Phantom_Hoover: *awesome 22:02:49 elliott, agreeing with you: that is a horrible misuse of No True Scotsman. It has a very particular syllogistic form that I've almost never actually seen used 22:03:22 the flaw has nothing to do whether someone or something is or isn't in a group :-\ 22:03:26 [[ Hamish is shocked and declares that "No Scotsman would do such a thing." [Brighton is not part of Scotland.] ]] — Antony Flew (before he got old and crazy) 22:03:29 Best [] note ever. 22:03:37 elliott, true 22:03:49 Oh, he died. 22:04:29 elliott, Antony Flew? 22:04:36 Phantom_Hoover: He did indeed. 22:04:54 Phantom_Hoover: (The populariser of No True Scotsman and famous atheist who later got old and was convinced to agree that God does actually exist.) 22:04:59 (Then he died.) 22:05:02 the pure logical form is: (a) All members of the set of A lack the trait T. (b) X is a member of A (objection) X has trait T (c) X is not a True A 22:05:03 * Phantom_Hoover swatpans elliott to within an inch of his life --==\#/ 22:05:15 Phantom_Hoover: Do you remember when almost all the examples of forms of argumentation on Wikipedia were between Father and (precocious) Daughter? 22:05:19 That was hilarious. 22:05:26 elliott, ...no. 22:05:31 Phantom_Hoover: It was amazing. 22:05:51 SHOW ME 22:05:57 elliott, one thing I'm *really* good at is logic :-} 22:06:00 Phantom_Hoover: In one of them the father argued for tolerance of all beliefs, then the daughter went "Well, you CAN'T say that because you have to be tolerant of the belief that it's BAD to be tolerant!" and oh god 22:06:10 I'll try and find it. 22:06:48 Can't. 22:07:10 j-invariant: I wonder whether I should do this with she. 22:07:43 {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes, TypeFamilies, FlexibleContexts, NoMonomorphismRestriction #-} 22:07:45 I think I will 22:07:46 {-# OPTIONS_GHC -F -pgmF she #-} 22:07:50 j-invariant: I call that "Tuesday" 22:08:50 * elliott edits keyboard layout, changes £ to # 22:08:55 nobody talks about money and I need my hash 22:09:18 elliott, have you ever actually seen NTS used correctly? 22:09:24 variable: not that I know of 22:09:25 elliott, HAHAHA YOU HAVE A CRAPPY MAC KEYBOARD LAYOUT 22:09:31 it appears to be a vanishingly rare fallacy in practice. 22:09:46 mostly because there are easier-to-make, more convincing ones. 22:10:03 elliott, yep 22:10:17 "To open kluchrtoxml, you need to install Rosetta. Would you like to install it now?" 22:10:18 Lol, powerpc 22:10:34 stupid VLC and mplayer can't play my DVD 22:10:58 mplayer plays everything, you did something wrong 22:11:24 elliott, it should be mplayer dvd:// -dvd-device /dev/acd0 22:11:25 right? 22:11:30 I dunno :D 22:14:48 elliott: SHE can't do 22:14:48 j-invariant: I wish Type:Type was consistent 22:14:48 data (:/:) (r :: *) :: {Poly r} -> * where Q :: r -> r :/: p 22:14:49 type Gauss = Integer :/: {x^2 + 1} 22:15:01 j-invariant: Indeed, I doubt it can :P 22:15:05 It's not a full language, man! 22:15:23 j-invariant: That's cool though. 22:15:26 But I doubt it's possible :P 22:16:41 j-invariant: nicer than plain haskell though 22:16:43 -!- Behold has joined. 22:20:01 -!- BeholdMyGlory has quit (Ping timeout: 260 seconds). 22:22:19 how does urxvt NOT have unicode support.... 22:22:22 * variable is really confused 22:23:11 variable: it does 22:23:20 j-invariant: :( she can't have types which are dependent on themselves 22:23:27 j-invariant: i.e. a constructor of type T takes a dependent T 22:24:15 elliott, any unicode character shows up as ? 22:24:23 variable: you set encodings wrong 22:24:34 what should I change? 22:24:41 variable: depends :) 22:24:48 elliott: I don't see what you mean 22:24:55 j-invariant: hm i think i did it wrong 22:25:03 Sigma :: {a:Type} -> Term {Pi (TypeI Z) (TypeI Z)} -> Type 22:25:11 the output for that tries to use : as a type operator and stuff so no it's not that 22:25:13 oh does it have to be :: 22:25:14 of course 22:25:15 does that work though 22:25:29 nope doesn't 22:25:30 so how do you do it 22:25:38 elliott, which language are you guys messing around with this time? 22:26:09 nm got it working 22:26:11 Phantom_Hoover: Haskell+she 22:26:43 elliott, what does this "she" do? 22:26:51 Vorpal: she does many things. 22:26:55 elliott, any ideas for what to look for? 22:26:58 elliott, that's what SHE said! 22:27:06 pseudo-dependent types, Pi, pattern synonyms, pseudo-aspect-oriented programming, and IDIOM BRAKKETZ 22:27:10 variable: LC_ALL etc 22:27:15 variable: what program is outputting them? 22:27:17 have you tried "cat" 22:27:17 :p 22:27:48 run locale 22:27:52 that outputs the relevant variables 22:28:00 elliott, when I attempt to copy from xchat to the shell (so I guess its zsh) 22:28:01 and also shows which is in effect for those not set 22:28:06 LC_ALL is empty 22:28:16 they are all ="C" 22:28:18 variable, then there is LANG, LC_CTYPE and so on. 22:28:24 yeah you need to set them to en_foo.UTF8 22:28:27 variable, well of course unicode doesn't work then 22:28:38 Vorpal, I'm new to unicode in the terminall.... 22:28:58 I should set them to en_US.UTF8 ? 22:29:11 variable, set LANG=en_US.UTF-8 22:29:13 I think it is 22:29:27 then all the unset ones default to LANG 22:29:32 so you only need to set LANG 22:29:39 (and LC_ALL overrides all on top of that) 22:29:51 urxvt: default locale unavailable, check LC_* and LANG variables. Continuing. 22:30:08 uh 22:30:09 what 22:30:23 export LANG="en_US.UTF8"; urxvt 22:30:34 btw, you might want to change LC_COLLATE to C again. since the non-C locales often sorts case insensitively. 22:30:38 oh wait - missing a 0 22:30:40 a - 22:30:56 or another alternative: maybe the locale was not generated 22:31:02 I think how varies between distros 22:31:27 nope: adding a "-" works 22:31:32 ah 22:31:35 it seems 22:32:40 j-invariant: aw man 22:32:44 i just messed this up 22:32:52 data Term :: {Nat} -> {Type} -> * where 22:32:52 Star :: {n} -> Term l {TypeI (S n)} 22:32:52 Var :: Fin {n} -> Term {n} ??? 22:33:03 j-invariant: am i going to have to carry around the whole environment of types or something? : 22:33:04 :/ 22:34:28 obviously 22:34:54 j-invariant: in the /type system/? 22:34:58 j-invariant: I'm not Oleg! 22:35:06 but okay 22:35:09 it's just a list 22:35:22 Not Found 22:35:23 The requested URL /~conor/pub/she/examples/ShePrelude.lhs was not found on this server. 22:35:23 Apache Server at personal.cis.strath.ac.uk Port 80 22:36:11 -!- Sasha2_ has joined. 22:37:16 -!- MigoMipo_ has joined. 22:37:18 -!- BMG has joined. 22:38:39 -!- BMG has quit (Changing host). 22:38:39 -!- BMG has joined. 22:38:43 -!- BMG has changed nick to BeholdMyGlory. 22:40:04 -!- Sasha2 has quit (Ping timeout: 276 seconds). 22:40:43 -!- MigoMipo has quit (Ping timeout: 276 seconds). 22:40:50 -!- Behold has quit (Ping timeout: 272 seconds). 22:40:56 elliott, my next language design goal is to make a language that takes an extremely long time to *compile* but NOT based on the time of day or have any arbitrary time requirments 22:41:30 variable: We have that, it's called C++. 22:41:33 variable: Or Haskell. 22:42:03 elliott, isn't haskell faster than C++ at least? 22:42:07 (at compiling) 22:42:15 basically - make the language itself require algorithms that are Θ(2^n) 22:42:43 variable, why not O(n!) 22:42:45 Vorpal: Well. We're working on that. 22:43:12 variable: better -- have a language with, e.g., 2^128 types exactly. have the only possible method of type checking be brute forcing 22:43:14 variable: in fact 22:43:20 variable: just store programs as SHA-512 hashes of an actual program 22:43:25 compilation takes place by brute-forcing the actual program 22:43:27 and then compiling that 22:43:44 variable: just store programs as SHA-512 hashes of an actual program <-- didn't gregor do this already? 22:44:00 Probably. 22:44:03 elliott: this sucks 22:44:06 I think there is such a language on the wiki. 22:44:07 j-invariant: What does? 22:44:16 elliott, no because that is not deterministic 22:44:36 and I don't just want O(n!) I want Θ(n!) 22:44:39 variable: yes it is deterministic 22:44:46 hm 22:44:51 there are hash collisions, but who cares :) 22:44:56 elliott, no - because there could be multiple programs that result in the same sha hash 22:45:00 variable: specify the order in which strings are brute-forced duh 22:45:04 then it's deterministic 22:45:10 if it fails to compile, just search for a collision 22:45:16 Vorpal: :D 22:45:22 -!- pikhq has quit (*.net *.split). 22:45:30 -!- augur has quit (*.net *.split). 22:45:32 -!- Sgeo has quit (*.net *.split). 22:45:36 -!- sebbu has quit (*.net *.split). 22:45:56 elliott, but then its not turing complete - not all programs could be represented 22:45:57 run the program 22:45:57 until you manage to find a program that compiles 22:45:57 ask the user if it's what they want 22:46:01 -!- coppro has quit (*.net *.split). 22:46:05 -!- dbc has quit (*.net *.split). 22:46:08 if it's not, keep going 22:46:09 ËÌÍÎË‚·∏Ø!:L 22:46:09 Was this correct? [y/n] 22:46:10 elliott, well that works if every possible string is a valid program 22:46:10 Vorpal: No, you just completely skip the non-compiling ones. 22:46:10 elliott, well true 22:46:10 variable: That's not a requirement for turing completeness... 22:46:29 -!- pikhq has joined. 22:46:29 -!- augur has joined. 22:46:29 -!- Sgeo has joined. 22:46:29 -!- sebbu has joined. 22:46:37 variable: You take the original language, remove a bunch of programs (those which come after a valid program in brute-force-order), and that's the "real" language. 22:47:08 The hashes are just a facade over that. 22:47:08 -!- pikhq has quit (Excess Flood). 22:47:09 elliott, anyway, I'm pretty sure that every hash can yeild a program that outputs a given output, assuming a good hash function. 22:47:10 Vorpal: You could finetune a hash function for it. 22:47:10 *yield btw. 22:47:11 -!- pikhq has joined. 22:47:11 Vorpal: But that isn't true. 22:47:12 Vorpal: Consider outputs bigger than the hash size. 22:47:22 j-invariant, Φ = lower bound O = upper bound Θ is when O == Φ IIRC 22:47:22 elliott, well, there are infinitely many strings that result in the same hash 22:47:22 Vorpal: Specifically, uncompressable outputs bigger than the hash size. 22:47:29 -!- coppro has joined. 22:47:29 -!- dbc has joined. 22:47:35 Vorpal: Well, yes. 22:47:37 Vorpal: The pigeonholes are very crowded. 22:47:49 variable: did j-invariant ask? 22:47:49 -!- pikhq has quit (Excess Flood). 22:47:49 elliott, meh - I want to invent the language myself 22:47:49 :-} 22:48:05 elliott, I thought he did when he said hm 22:48:08 ah 22:48:10 elliott, if the hash function is good, then it will "look" random. Thus we won't get that anything starting with, say, an "y" can't have this hash 22:48:11 -!- pikhq has joined. 22:48:41 if that would happen, then it wouldn't be a good hash function 22:49:00 elliott, am I right? I always forget the lowerbound symbol - the rest I know are correct 22:49:08 variable: I... think so. 22:49:12 elliott, thus, we should be able to find a program for any given hash that gives a specific output. Though it may be a /very/ long program. 22:49:14 elliott, right? 22:49:21 Vorpal: Let's just say yes and not think about it! 22:49:34 elliott, do you think I'm not right? 22:49:35 Var :: {Fin n} -> Term {t:ts} t 22:49:37 j-invariant: can't believe that actually works 22:49:40 :/ 22:49:41 Vorpal: I don't know :-) 22:49:45 It's probably right. 22:49:51 elliott ah I have another idea for a language 22:50:00 elliott, well, who would be the expert on this? 22:50:06 Vorpal: Your mo^W^Wsomeone. 22:50:16 Vorpal: It sounds like something very hard to prove. 22:50:19 For a given hash function. 22:50:27 elliott, for any /real/ hash function yes 22:50:33 you program the language by defining all legal inputs and the resulting outputs. The compiler bruteforces the shortest program that would result in those inputs/outputs :-} 22:50:33 elliott, but for a theoretical perfect one 22:50:49 variable: Reminds me of Clue. 22:51:00 Vorpal: Well, let's consider the hash function : String -> 1. 22:51:15 Vorpal: There is only one such function, f(s) = (). 22:51:24 right 22:51:32 Vorpal: Every program has the hash (), and the hash () has every program. 22:51:38 Vorpal: What is your hypothesis again? 22:52:04 j-invariant: what do you think of HOAS? 22:52:46 elliott, well, for every value in the co-domain of the hash function it will be possible to find a program in the domain that gives the specific output (assuming a language where the program isn't the same as the output, I suspect the language need to be brainfuck-IO-complete) 22:53:00 (or at least output, I don't think input matters) 22:53:00 Vorpal: Consider 22:53:16 f : String -> 2; f('x':...) = A; f(s) = B 22:53:22 elliott, what language is this 22:53:24 i.e. x followed by anything is A, everything else is B. 22:53:27 Vorpal: Pseudo. 22:53:29 ah 22:53:36 Vorpal: Now consider a language where no valid program starts with x. 22:53:43 All programs hash to B; A has no program. 22:53:53 Vorpal: Of course this is pathological ... but it demonstrates that it is not universally true. 22:53:55 elliott, hm true. 22:54:04 Vorpal: I think the problem is that while hash functions "appear" random they are not _actually_ perfectly uniform. 22:54:09 elliott: HOAS is stupid 22:54:14 j-invariant: why 22:54:18 elliott, that is not a good hash in the way I said above though. 22:54:24 elliott: it's just completely impossible to use for anything nontrivial 22:54:26 elliott: elliott, if the hash function is good, then it will "look" random. Thus we won't get that anything starting with, say, an "y" can't have this hash 22:54:26 Vorpal: I don't think a good hash in that sense exists then. 22:54:28 j-invariant: well eys :P 22:54:29 *yes 22:54:39 elliott, true, I suppose even sha512 has some bias 22:54:53 elliott, but something like sha512 or similar should come close at least 22:55:18 -!- jix has quit (*.net *.split). 22:55:29 -!- coppro has quit (*.net *.split). 22:55:33 -!- dbc has quit (*.net *.split). 22:55:35 Vorpal: Close doesn't make a theorem. Infinity is against you; close times infinity equals infinitely far. :p 22:55:36 elliott: obvious being able to write syntax using lambda terms is nice, but using it internally for algorithms doesn't seem possible 22:55:36 elliott, of course. 22:55:36 j-invariant: agreed 22:55:45 Vorpal, good hash functions are not defined by looking random 22:55:45 * elliott parameterises Type 22:55:48 (on the level...) 22:55:58 j-invariant: is there any way out of an infinite hierarchy of Type-s again? 22:56:02 good hash functions are defined by small changes in the source result in large changes in the output 22:56:03 or is it all just machinery to hide it 22:56:10 variable: yes. we are aware 22:56:17 he was defining his own notion 22:57:04 elliott, but theoretically perfectly unbiased hash functions are often used in discussing algorithms using hash function. Proving something secure with that is easier than with any given real hash, so I seem to remember that often crypto things are proven secure given an unbiased hash function first. 22:57:16 variable, indeed 22:58:04 Vorpal, actually my definition isn't complete 22:58:04 variable, which will as a result look pretty random. I was not being very strict in my wording when I said "looking random" 22:58:04 because then theoretically multiplying all the bytes together should be a "good" hash function 22:58:22 Vorpal: is an unbiased function even theoretically possible? 22:58:26 * variable is away 22:58:28 I'm not sure such a functoin would be computable 22:58:29 *function 22:58:46 elliott, define theoretically. 22:58:55 -!- jix has joined. 22:59:41 Vorpal: Is there a computable unbiased hash function? 22:59:43 elliott, you can discuss things using an oracle in articles. They are presumably not possible for an UTM. 22:59:50 So not computable then. 23:00:02 elliott, I don't know if it has been proven if one could exist or not 23:00:10 elliott, I'm pretty sure none is known though. 23:00:26 data Term :: {[Type]} -> {Type n} -> * where 23:00:26 Star :: {n} -> Term {ts} {TypeI (S n)} 23:00:26 Var :: {Fin n} -> Term {t:ts} {t} 23:00:28 Fun :: {t} -> Term {t:ts} {s} -> Term {ts} {Pi t s} 23:00:30 App :: Term {ts} {Pi t s} -> Term {ts} {t} -> Term {ts} {s} 23:00:35 j-invariant: what's the hot way of describing data structures nowadays 23:00:40 W fell out of favour I know that :) 23:01:00 elliott, W? 23:01:13 Vorpal: W. 23:01:22 W 23:01:24 dot. 23:01:33 elliott, yes not very googable 23:01:52 elliott, even with the dot 23:01:54 THINGS I HATE: people who equate the web to "www". 23:01:55 Vorpal: The birth ceremony http://www.cs.nott.ac.uk/~txa/publ/icalp04.pdf and obituary http://www.e-pig.org/epilogue/?p=324 23:02:13 Vorpal: Just skip straight to the obituary. 23:02:59 "In Epigram 2, we don’t take W-types as the primitive source of inductive structure. Instead, we supply a universe of inductive types, giving first-order data a first-order representation. We’ve just written a paper about it: The Gentle Art of Levitation." 23:03:01 Vorpal, elliott: HASHFUCK IS PATENTED 23:03:05 but i think that might be overblown for what i want 23:03:19 Gregor: YOUR MOERMYORI TJOP FDJ ODGPDNG IODFJG IODJG IODFJG KOFDJGOIFDJH0DZJSVOI HIOSI ]EWSE0R 9J90E4JYS0SJ TAWR -K5 -K[RS';T/XHC;LGKO[N]PLJK 23:03:21 elliott, ah 23:03:33 Vorpal: you read the whole post and understood it in that time? 23:03:34 Hashfuck? 23:03:35 don't lie 23:03:37 elliott, no 23:03:39 elliott, I didn't 23:03:40 WELL THEN 23:03:41 get to it 23:03:42 elliott, I never claimed I did 23:03:48 *ShaFuck rather 23:03:49 I WONDER WHY 23:03:59 j-invariant: I should probably have a type for terms and values 23:04:10 -!- coppro has joined. 23:04:10 -!- dbc has joined. 23:04:38 -!- Phantom_Hoover has quit (Quit: Rebooting). 23:06:37 elliott: you mean both? 23:06:57 -!- Phantom_Hoover has joined. 23:06:58 j-invariant: as in, two individual ones 23:07:05 rather than just reducing Terms down to more value-y terms 23:07:06 ok 23:08:26 ugh, this utterly sucks 23:08:57 I have Maybe all over the place because I can't parametrize haskell modules by values 23:09:08 but it's not clear whether they get turned to Just's in time 23:09:19 elliott, well too long to read, but the general issue he mentions is a recurring theme. Too flexible, too hard to work with in computers. 23:09:20 data Term :: {[forall n. Type n]} -> {Type n} -> * where 23:09:21 TermWrap :: Thing Term {ts} {s} -> Term {ts} {s} 23:09:21 App :: me {ts} {Pi t s} -> me {ts} {t} -> Term {ts} {s} 23:09:22 instance Thingy Term where wrap = TermWrap 23:09:24 SUCH FUN 23:09:45 Vorpal: well there's more important stuff near the bottom where he demonstrates theoretical problems too. 23:09:53 23:08 j-invariant: I have Maybe all over the place because I can't parametrize haskell modules by values 23:09:57 j-invariant: this is why we need an ML-style module system! 23:10:01 yeah 23:10:03 or really Ur-style 23:10:03 :) 23:10:10 I don't know much about module systems really 23:10:21 elliott, the bit about canonical representation? 23:10:21 I want a language expressive enough to define them in 23:10:28 Vorpal: the bit about tt = ff. 23:10:31 or ff = tt. around there. 23:10:32 ah 23:11:29 elliott, should I learn OCaml? 23:11:32 I think I tried once 23:11:41 elliott, ah... it is inconsistent, right? 23:11:43 Sgeo: Learn Standard ML instead. Probably. 23:11:47 Vorpal: It's more subtle than that :-P 23:12:24 j-invariant: so what's your favourite way of defining recursive types in the value language! 23:12:26 The reason I started with Racket in the first place is because I heard good things about the module system. I was lied to. 23:12:30 Sgeo: LIED 23:12:39 Sgeo: the ML module system is nothing like what you think it is. 23:12:49 j-invariant: i.e. combinators resulting in Types. 23:12:52 elliott, ...? 23:15:01 j-invariant: can you look at what i have so far? http://sprunge.us/UiXi 23:15:07 j-invariant: specifically the XXX: comments ... I'm a bit confused 23:15:18 erm that App signature at the bottom is all wrong 23:15:20 it hosuld say Term, not me 23:15:21 *should 23:15:33 also star should be gone 23:15:44 also i have a bug 23:15:45 ffff 23:15:47 elliott, any reasons for Standard ML over OCaml? 23:15:57 Sgeo: ocaml sucks. sml sucks less. 23:16:14 elliott: just use Agda already :P 23:16:24 j-invariant: but agda is 'orrible 23:16:34 this IS agda code 23:16:55 j-invariant: LET ME LIVE IN MY ILLUSION 23:17:12 btw 23:17:20 you can't really use lists for a context of types 23:17:25 Not in scope: type constructor or class `SheTyType' 23:17:26 what is this even. 23:17:27 j-invariant: why not 23:17:29 since later types might depend on the earlier ones.. 23:17:35 this makes things difficult 23:17:43 j-invariant: oh god you're right 23:17:46 j-invariant: asdfghj that is awful 23:17:53 j-invariant: i need like 23:17:54 dependent lists 23:17:59 is that something that exists 23:18:31 elliott, what are you trying to do? 23:18:39 Vorpal: things. 23:18:53 elliott, okay, if you don't want to tell... 23:19:13 Vorpal: i explained above. 23:19:36 elliott, approx where? 23:19:46 dunno 23:19:51 it's a dependent lang 23:20:07 elliott, that you are writing (or do you mean what she is?) 23:20:25 former 23:20:30 elliott, cool 23:20:39 it is not going well 23:21:04 elliott, haskell should add such an extension already 23:21:11 aha! 23:21:20 solved 23:21:30 Vorpal: um that would require a complete restructuring of GHC 23:21:38 and would be difficult to integrate with large swathes of haskell 23:22:27 elliott, hm true 23:22:36 Ambiguous type variable `thing' in the constraint: 23:22:36 `Thingy thing' 23:22:46 j-invariant: apparently "thing" is ambiguous, who knew? 23:22:54 elliott, what good general purpose dependently typed languages are there? 23:22:56 any? 23:23:04 Vorpal: Epigram 23:23:10 elliott, 1 or 2? 23:23:13 2 23:23:23 elliott, which isn't usable yet iirc 23:23:24 so... 23:23:30 Are computers? 23:23:34 none that is usable as of today? 23:23:38 elliott, well, that depends 23:25:04 elliott, was it epigram that allowed you to declare a data structure using RFC notation? Or was that another language (which one?)? 23:26:04 Vorpal: That was Cola/whateveryouwanttocallit, completely unrelated, that one's more similar to Smalltalk — don't tell Sgeo, or I'll have to add another regexp to shutup. 23:26:34 elliott, dude you just highlighted him 23:26:35 -!- MigoMipo_ has quit (Read error: Connection reset by peer). 23:26:44 Vorpal: INDEED 23:27:09 elliott, so this Cola, was it any good? 23:27:21 Vorpal: It's a VPRI project. It's pretty coo'. 23:27:38 ah... 23:28:14 -!- augur has quit (*.net *.split). 23:28:16 -!- Sgeo has quit (*.net *.split). 23:28:20 -!- sebbu has quit (*.net *.split). 23:28:51 -!- Leonidas has quit (*.net *.split). 23:28:54 Vorpal: they are not general purpose 23:28:55 elliott, maybe I should try to learn Epigram? 23:28:55 j-invariant, which ones? epigram? 23:28:55 Vorpal: none of them 23:28:55 j-invariant, would you call haskell general purpose? 23:29:06 yes 23:29:06 ah well 23:29:06 j-invariant: Epigram is close enough :P 23:29:11 j-invariant, in what way is epigram not general purpose then? 23:29:16 Vorpal: You can't learn Epigram 2 because nothing actually runs Epigram 2. 23:29:22 elliott, hm true 23:29:39 Vorpal: There's an interactive-in-a-user-hostile-kind-of-way theorem prover that can define things in the Epigram system, but the actual language is completely unimplemented and utterly unfinished. 23:29:52 -!- Leonidas has joined. 23:29:52 -!- augur has joined. 23:29:52 -!- Sgeo has joined. 23:29:52 -!- sebbu has joined. 23:30:42 elliott: *Polynomial> let w = (one - Quot (mon 1, Just eisenstein))*(one + Quot (mon 1, Just eisenstein)) 23:30:42 elliott, right. Is it moving forward fast or? 23:30:42 *Polynomial> printPolynomial names ((inj w * x + y)^7) 23:30:42 "y^{7} + (14 + 7\\zeta)x y^{6} + (63 + 63\\zeta)x^{2} y^{5} + (105 + 210\\zeta)x^{3} y^{4} + (315\\zeta)x^{4} y^{3} + (-189 + 189\\zeta)x^{5} y^{2} + (-189)x^{6} y + (-54 + -27\\zeta)x^{7}" 23:30:57 Vorpal: It's been in progress since 2005, so no; but Conor likes throwing out gigantic swathes of the underlying system, so yes. 23:30:58 j-invariant: N I C E 23:30:58 elliott, hah 23:30:58 j-invariant: did you write this?!?! 23:31:06 Vorpal: *system on a regular basis, 23:31:11 yes 23:31:56 printPolynomial 23:31:56 :: (SheChecks Nat n, Ring r, Eq r, Show r) => 23:31:56 Vec n String -> MonoidRing r (Vec n Integer) -> String 23:34:10 j-invariant: i approve. i approve very hard 23:34:42 j-invariant: so do quotient sets work yet >:) 23:37:41 /Users/ehird/Code/tabby/first.hs:52:26: 23:37:41 Could not deduce (Show (me (t1 :$#$#$#: ts) s)) 23:37:42 from the context (t ~ SheTyPi t1 s) 23:37:43 arising from a use of `show' 23:37:45 at /Users/ehird/Code/tabby/first.hs:52:26-31 23:37:47 Possible fix: 23:37:49 add (Show (me (t1 :$#$#$#: ts) s)) to the context of 23:37:51 the constructor `Fun' 23:37:54 import ShePrelud 23:37:55 e 23:38:40 "For any logical system, T, with an algorithm to decide what is and is not a proof in T (aka a decidable set of axioms) such that each axiom of Robinson Aritmetic (which is a very weak theory of arithmetic) is provable in T, there is some formula G, such if T proves G or if T proves ¬G, then T proves 0=1." 23:38:40 j-invariant: already have yo 23:38:46 hasn't helped 23:39:00 i think i see the problem though MAYBE 23:39:10 flexible contexts -- ALWAYS A MISTAKE ??? 23:39:38 j-invariant: indeed 23:39:44 j-invariant: any reason for quoting that? :p 23:42:03 "the incompleteness and undecidability of PA cannot be blamed on the only aspect of PA differentiating it from Q, namely the axiom schema of induction." 23:42:50 haha "For Christmas I received the book Gödel, Escher, Bach: An Eternal Golden Braid (or GEB) and I have been pretty deeply troubled regarding Gödel's incompleteness theorems since." 23:44:02 "troubled"? 23:44:14 j-invariant: where's that from btw 23:46:24 Phantom_Hoover: http://i.imgur.com/1LCv6.png I think dome3 is smaller than the Cube. 23:46:37 Phantom_Hoover: Note how they have tons of people working on it and even they haven't gone for bedrock. 23:48:29 elliott, dome3? 23:48:40 Vorpal: see image. on the reddit creative server. 23:48:56 elliott, I see the image. But what is it supposed to be? 23:49:01 A dome. 23:49:03 WIP. 23:49:06 just a dome? 23:49:36 yes. 23:49:52 elliott, how does one get to dome 3? 23:50:06 Phantom_Hoover: /warp dome3. 23:50:11 Phantom_Hoover: Try not to crash the server. 23:50:45 elliott, such suspicion! 23:50:55 Phantom_Hoover: I'M ON TO YOU 23:51:12 elliott: I don't understand haskell types 23:51:15 what are they for 23:51:19 j-invariant: to type things 23:51:26 which things? 23:51:38 j-invariant: typed things 23:51:59 j-invariant, it is useless when he is in this mood 23:52:05 haha 23:52:31 Vorpal: actually i was joking along with j-invariant. 23:52:38 p. sure j-invariant knows what haskell types are 23:52:39 ah 23:52:49 j-invariant: TYPES IN HASKELL ARE LIKE BURRITOS TO YOUR MONADS 23:55:28 -!- elliott has quit (Remote host closed the connection). 23:55:50 X) 23:56:05 -!- elliott has joined. 23:56:47 If I became obsessed with Haskell, would shutup be configured to yell at me for mentioning Haskell? 23:57:26 Sgeo: Only if you say stupid things. 23:57:27 elliott, the dome is quite astounding. 23:57:38 Phantom_Hoover: Yes. Yet it is, afaik, smaller than the Cube and also more shallow. 23:57:45 Phantom_Hoover: How the fuck is the Cube ever going to get completed? 23:57:49 j-invariant: is that polynomial thing up anywhere? 23:57:52 Well, it definitely does go down to bedrock. 23:57:54 -!- j-invariant has quit (Quit: leaving). 23:57:55 I'd help if I could 23:58:01 Sgeo: Buy Minecraft. 23:58:10 elliott, it will get completed because we are HHI and we do not have restrictions on TNT. 23:58:17 HHI? 23:58:20 Phantom_Hoover: Do we have the TNT kit yet? 23:58:26 TNT kit? 23:58:33 -!- j-invariant has joined. 23:58:37 Sgeo: a kit to get tnt 23:58:40 j-invariant: is the polynomial source open? 23:58:45 elliott, you have a script to tell him to shut up? 23:58:48 elliott, why not just ignore 23:59:18 Vorpal, if I say Racket, Newspeak, Smalltalk, Factor, AW, Active Worlds, or ActiveWorlds, I get PMed a message teling me to shut up 23:59:29 Used to say it in the channel, but oerjan got ticked off 23:59:48 I am excellent at obeying the letter but not the spirit of any judgement. 23:59:49 Sgeo, just filter such /msg from elliott! 23:59:53 elliott: what do you want to see? 23:59:56 Vorpal: It doesn't come from me. 23:59:59 it's 5 files