00:00:34 <elliott> GEB is what happens when a smart person has some kind of mental blockage that makes them consider recursion amazing.
00:01:05 <elliott> j-invariant: Penrose should just be ... forced to shut up forever?
00:01:10 <elliott> j-invariant: like a restraining order
00:01:14 <elliott> he can't publish any books any more
00:01:20 <j-invariant> elliott: the problem with Penrose is he's a really smart guy
00:01:33 <j-invariant> he just has this one absolutely idiotic idea that he talks about sometimes
00:01:39 <elliott> 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 <elliott> ??? I don't know, I can't explain crazy people
00:01:53 <elliott> j-invariant: the smarter someone gets, I think, the more likely they are to have one really stupid idea
00:01:59 <elliott> and be unable to see how stupid it is
00:02:19 <j-invariant> oh yeah einstein with that stupid "relativity" stuff
00:02:20 <elliott> coppro: yeah what was that fucker thinking with realtivity
00:02:40 <coppro> Phantom_Hoover: spooky action at a distance
00:03:04 <elliott> that's my favourite name of anyhting really
00:03:05 <j-invariant> isn't the non-existence of action at a distance a direct consequence of relativity?
00:03:10 <elliott> spooky action at a distance
00:03:15 <elliott> it's just ... the best name
00:03:15 <coppro> j-invariant: well, you'd think
00:03:32 <elliott> http://en.wikipedia.org/wiki/Action_at_a_distance_(physics) i bet this was renamed from the proper name by wikilamers
00:03:36 <coppro> j-invariant: but Einstein also developed the first inklings of quantum theory
00:04:10 <coppro> he hated quantum theory because of its implications
00:04:17 <coppro> he was too hung up on dumb concepts
00:04:30 <coppro> despite having given the insight which led to the
00:05:23 <elliott> gödel's really stupid idea was that he was being poisoned, but that one resolved itself quite quickly :D
00:05:25 <elliott> aww that was an awful thing to say
00:07:04 <elliott> Vorpal: OS X — 96 gigs; Ubuntu — 56 gigs; Shared — 96 gigs
00:07:10 <elliott> Vorpal: dunno whether those are decimal are binary gbs but who cares
00:07:13 <elliott> does this look reasonable?
00:07:26 <coppro> my school has a course that includes undecidability
00:07:30 <coppro> I've heard it's kind of boring :(
00:07:40 <elliott> I can resize the OS X one at any time really, but
00:08:18 <Vorpal> elliott, no it doesn't
00:08:24 <Vorpal> elliott, too much of OS X :P
00:08:34 <elliott> Vorpal: aside from zealotry.
00:08:38 <Vorpal> but since you can resize it again, sure
00:08:40 <elliott> OS X takes up more space, simple fact
00:08:46 <elliott> Vorpal: yeah but i'd have to get rid of ubuntu/shared
00:09:01 <elliott> Vorpal: because this takes up the whole disk
00:09:05 <Vorpal> elliott, couldn't you add shared-2
00:09:12 <elliott> Vorpal: you mean shrink OS X?
00:09:17 <elliott> I doubt i'll want to give less to OS X
00:09:25 <elliott> considering there's only 50 gigs free on there as it stands
00:09:33 <Vorpal> elliott, aren't there shrinkable linux file systems?
00:09:35 <elliott> 56 gigs for ubuntu might be too little? probably not
00:09:41 <elliott> Vorpal: probably. i'm just going to go with ubuntu default
00:09:58 <Vorpal> elliott, not sure how much ubuntu need
00:10:03 <Vorpal> du -sh /usr might take a while
00:10:12 <elliott> Vorpal: well as fizzie said his ubuntu install only uses about 10 gigs.
00:10:18 <Vorpal> Filesystem Size Used Avail Use% Mounted on
00:10:21 <elliott> Vorpal: but there's /home in these too, just things like music will go on shared
00:10:34 <Vorpal> elliott, well my /home :
00:10:41 <Vorpal> Filesystem Size Used Avail Use% Mounted on
00:10:41 <Vorpal> /dev/mapper/array-home
00:10:41 <Vorpal> 69G 59G 7,4G 89% /home
00:10:54 <Vorpal> I guess I'll have to grow it
00:11:01 <elliott> yes, yes, I /am/ planning to buy my big desktop system.
00:11:19 <Vorpal> elliott, you here see the wonder of LVM!
00:11:19 <elliott> 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 <elliott> Vorpal: and if all filesystems supported resizing. online resizing.
00:11:43 <Vorpal> elliott, well actually jfs supports on line growing
00:11:46 <elliott> Vorpal: but, uh, LVM has the wondrous feature of interoperating with NOTHING
00:11:55 <elliott> want to just LOOK at your files in another OS? SORYYYYY
00:11:58 <Vorpal> elliott, so does ext4 iirc
00:12:08 <elliott> Vorpal: yeah. well. i'm not making my shared partition ext4
00:12:10 <Vorpal> elliott, lvm for fuse? DO IT NOW!
00:12:25 <Vorpal> elliott, I think ext3 supports resizing too
00:12:52 <Vorpal> elliott, anyway I doubt I will change from linux on my destop
00:12:55 <elliott> Fuck it, I'm resizing. If I decide it's all wrong I'll trash ubuntu & shared and redo it.
00:13:07 <Vorpal> elliott, what about swap
00:13:07 <elliott> Vorpal: um hello @? (okay so @ won't interact with anything else either :-))
00:13:14 <elliott> Vorpal: I don't need swap, I have four gigabytes of RAM
00:13:22 <Vorpal> elliott, you can't suspend to disk then
00:13:27 <elliott> Vorpal: Sure you can with a swap file.
00:13:52 <elliott> Vorpal: OK, fine, I'll make room for a six gig swap.
00:13:54 <Sgeo> elliott, it's a blood drop
00:13:54 <Vorpal> elliott, separate /boot I guess?
00:13:56 -!- wareya has joined.
00:14:03 <Vorpal> elliott, needs to be 60 MB or less
00:14:16 <Vorpal> (well it could be larger)
00:14:17 * Sgeo finished Braid
00:14:24 <Vorpal> (would be a waste though)
00:14:29 <elliott> Vorpal: why separate /boot.
00:14:43 <Vorpal> elliott, well depends on if your bootloader can handle the main fs
00:15:18 <Vorpal> elliott, I guess you need to install bootloader into partition rather than into mbr on that computer
00:16:09 <Vorpal> /var contains a few chroots
00:16:23 -!- elliott has quit (Remote host closed the connection).
00:16:58 -!- elliott has joined.
00:17:06 <elliott> Wonder why LimeChat crashed.
00:17:12 <elliott> (Resize and partition, no less.)
00:17:24 <elliott> OK, now I need to put GRUB on the shared partition.
00:17:40 <elliott> You can install GRUB from OS X right? ...right?
00:18:11 <elliott> can you download "GRUB 2 images" or something?
00:18:16 <olsner> I wouldn't count on it: :)
00:19:56 -!- variable has quit (Read error: Operation timed out).
00:20:55 <elliott> configure: error: objconv not found which is required when building with apple compiler
00:21:02 <elliott> olsner: grub can build on os x apparently?
00:21:43 -!- variable has joined.
00:22:01 <olsner> sure, but isn't it heaps easier to do this from ubuntu once you install it? :)
00:22:08 <j-invariant> 00:21 < c_wraith> (I have goldbach's conjecture in formal logic as a tattoo)
00:22:10 <elliott> olsner: i need grub to install it.
00:22:30 <elliott> goldbach's conjecture is beautiful now?
00:22:33 <olsner> right, due to not having an optical drive?
00:22:42 <elliott> olsner: i'm going to boot from hd with grub :p
00:22:47 <olsner> so you're going to install the installer and boot it with grub?
00:22:49 <elliott> olsner: I could just fish out a usb stick but this is the moar funz
00:23:33 <elliott> GRUB2 will be compiled with following components:
00:23:40 <elliott> oh wait grub doesn't do 64-bit
00:24:12 <olsner> can it even boot without efi support on a mac?
00:24:20 <elliott> olsner: well. yes. with bios emulation.
00:24:26 <elliott> although probably it hands over control as bios?
00:24:33 <elliott> i'm just scared that it'll be grub-efi
00:24:42 <elliott> olsner: see http://grub.enbug.org/TestingOnMacbook
00:25:08 <fizzie> But Grub-EFI is so modern!
00:25:27 <elliott> is it actually possible to force a bios build???
00:25:49 <elliott> --with-platform=pc should do it
00:26:05 <elliott> (is that "ok" to do? who knows let's find out)
00:27:48 <elliott> In file included from kern/err.c:23:
00:27:48 <elliott> ./include/grub/i18n.h:28:5: error: "ENABLE_NLS" is not defined
00:27:48 <elliott> make: *** [kernel_img-kern_err.o] Error 1
00:27:49 <elliott> make: *** Waiting for unfinished jobs....
00:27:51 <elliott> In file included from kern/misc.c:26:
00:27:53 <elliott> ./include/grub/i18n.h:28:5: error: "ENABLE_NLS" is not defined
00:31:27 <elliott> ok seriously. even a grub 1 image would do
00:31:41 <elliott> i'll try a grub floppy. who knows
00:33:23 <Phantom_Hoover> [[On December 5, 2009 Joel ingested a quantity of Traumeel, a homeopathic alternative to ibuprofen.]]
00:33:42 <elliott> Oh, I thought it was ... without context.
00:33:48 <elliott> On December 6, 2009 Joel ate breakfast.
00:37:31 <Phantom_Hoover> This is a perfect demonstration of the way that selection pressures in our culture are working against intelligence.
00:38:13 <Phantom_Hoover> 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:43 <elliott> [[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:39:22 <j-invariant> 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 <fizzie> 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:45 -!- elliott has joined.
00:42:07 <elliott> Wait, I have another idea.
00:42:07 <j-invariant> 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 <elliott> yeah nhs support of homeopathy is fucked
00:42:38 <j-invariant> Great idea: aquapuncture - combination of the ancient chinese art (?) and homeopathy!
00:42:47 <j-invariant> I'll make a forture^H^H^H help lots of people!
00:42:52 <Phantom_Hoover> 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:47 <fizzie> Iridopuncture, aka needles-to-the-eye.
00:43:50 <Phantom_Hoover> Although that would probably cure you of pins and needles, not anything else.
00:45:13 <fizzie> Phantom_Hoover: Broken foot? Dissolve someone else's foot in acid, then start diluting that.
00:45:26 <fizzie> (Remember to break it first, though.)
00:46:41 <Phantom_Hoover> 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 <elliott> I've had a sudden burst of reasonableness and found a USB stick
00:58:50 <elliott> Phantom_Hoover: Can the world float?
01:03:09 <elliott> Phantom_Hoover: Who was the hippocampus?
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 <elliott> "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 <elliott> nctional approach, retaining its benefits while providing higher-level abstractions more supportive of extension and reuse."
01:29:23 <elliott> 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 <elliott> ctional approach, retaining its benefits while providing higher-level abstractions more supportive of extension and reuse.
01:29:25 <elliott> http://se.ethz.ch/~meyer/publications/functional/meyer_functional_oo.pdf
01:30:04 <elliott> "(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 <elliott> 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 <elliott> [[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:52:28 * oerjan wonders who "they" are :D
01:53:41 <elliott> oerjan: the set {Scott Aaronson} :D
01:54:24 <oerjan> so he uses the royal "then", i take?
01:55:24 <oerjan> a subtle megalomania mixing the styles of queen victoria and julius caesar
01:57:12 <elliott> bleh ... it seems you have to have a gpt thing to do usb w/ macbook air
01:57:18 <elliott> 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:59:45 <ais523> elliott: I feel slightly wrong writing in a functional style in K&R C
02:00:01 <ais523> purely for the purpose of making a "record this, do something, put it back to the original value" wrapper nest easily
02:00:25 <elliott> ais523: I mean, K&R? And ...
02:00:25 <ais523> and as for K&R C, I was writing a hacked version of NetHack for RNG manipulation purposes
02:00:29 <ais523> and NetHack's written in K&R C
02:00:37 <elliott> ais523: protoize that shit for AceHack :P
02:00:39 <ais523> (it predates C89, so you can hardly blame it for that)
02:01:00 <ais523> I haven't done things like reindenting or protoizing so existing patches apply wel
02:01:20 <ais523> 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:51 <elliott> ais523: not following an existing codebase's indentation style
02:01:58 <elliott> ais523: I'm afraid I'm going to have to kill you for the benefit of everyone.
02:02:00 <ais523> elliott: means I end up not mixing tabs and sapces?
02:02:05 <ais523> you can't have things both ways round
02:02:15 <elliott> ais523: at least keep the same indentation width
02:02:23 <elliott> (4, since they probably assume tab=8)
02:02:28 <ais523> yep, in some cases I've been interspersing eight spaces for two levels
02:02:47 <elliott> ais523: but don't do any two-spacing
02:02:51 <ais523> 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 <elliott> time to try out this ubuntu usb stick again
02:03:11 <elliott> 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 <ais523> (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:02 <ais523> as I have far too many NetHack source trees, in all sorts of places
02:04:05 -!- coppro has joined.
02:04:14 -!- coppro has quit (Client Quit).
02:05:04 <ais523> hmm, why do places like BBC News always credit YouTube or Wikipedia rather than the actual author of the content?
02:05:07 <elliott> 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:16 <fizzie> "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 <elliott> ais523: which can be done ... with a fedora specific, linux-only, RPM package
02:05:20 <fizzie> (Just saw that on a page.)
02:05:34 <elliott> - see if i can get that working here (endless unpredictable pain)
02:05:39 <ais523> you need a Linux-based program in order to install Linux?
02:05:41 <elliott> - £60 on external SuperDrive
02:05:55 <elliott> 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 <ais523> 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 <elliott> ais523: that... sounds like it could rapidly become more than £60 worth of pain
02:06:26 <fizzie> Can't you partition it with just gdisk?
02:06:39 <elliott> fizzie: partitioning is easy -- getting the files on there and making it bootable, I have no idea ho
02:06:45 <elliott> apparently it has to be HFS-partitioned too
02:06:51 -!- coppro has joined.
02:06:54 <elliott> so regular bootloaders won't work?
02:07:05 <elliott> fizzie: Feel like making a USB stick image for me? :-P
02:07:12 <coppro> that was totally my fault
02:07:17 <elliott> All it'll require is alien, an Ubuntu ISO, and PATIENCE!
02:07:26 -!- augur has quit (Ping timeout: 240 seconds).
02:07:29 <fizzie> I think I'll instead sleep on it. :p
02:07:45 <elliott> ais523: You're far too loyal not to help out, right?
02:09:19 <elliott> ais523: THAT IS NOT THE SOUND OF REASSURANCE
02:10:25 <elliott> ais523: re youtube/wikipedia
02:10:37 <elliott> ais523: because those seem like real, respectable businesses
02:12:11 <elliott> [[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 <elliott> I ... don't think Woz stayed on for very long, BBC
02:14:25 <elliott> it's got to be possible to do this
02:14:35 <Sgeo> elliott, is the last ep of season 1 good?
02:14:43 <elliott> Sgeo: Does it matter? You can't skip any.
02:14:49 <elliott> ais523: I don't suppose I can convince you to try and install one package and try out a command ...?
02:18:34 <Sgeo> Well, most of the good episodes were near the end of the season
02:20:31 <elliott> coppro: what about YOU, I can depend on you can't I
02:23:51 -!- augur has joined.
02:24:45 <coppro> elliott: What assistance do ou need, citizen?
02:25:08 <elliott> coppro: one (1) .rpm converted to .deb and installed by you with the help of ``Alien'' conversion tool;
02:25:19 <elliott> coppro: and one (1) Ubuntu Live CD ISO downloaded;
02:25:29 <elliott> coppro: and one (1) conversion of this ISO to a disk image using that Linux-only tool
02:26:02 <coppro> knowledge of RED Hat is above your Clearance, citizen.
02:26:12 <coppro> Report for termination immediately.
02:26:15 <coppro> Thank you, and enjoy your day.
02:26:27 <elliott> coppro: DAMMIT I'MA GO INSANE
02:26:43 <elliott> can't even bother with references INSTALL THE PACKAGE ;_;
02:26:50 <coppro> why do you need your ISO converted?
02:26:58 <elliott> coppro: to install ubuntu.
02:27:44 <elliott> coppro: um, a computing machine?
02:27:52 <coppro> oh wait it's a usb stick image?
02:28:01 <elliott> coppro: no it's a live cd that you can turn into a usb stick image
02:28:02 <coppro> lol just stick a partition table in front of it
02:28:08 <elliott> coppro: yeah um it needs to be gpt
02:28:15 <elliott> and i have no idea what bootloader it installs
02:28:45 <elliott> coppro: there _is_ a reason I mentioned the .rpm, you know
02:28:49 <coppro> but also because you wouldn't do it for me
02:29:00 <elliott> i would actually if yelled at enough
02:29:03 <elliott> how much do i have to tell
02:29:20 <elliott> "livecd-iso-to-disk --mactel --reset-mbr foo.iso blah" NAG NAG NAG
02:29:29 <elliott> NAG NAG NAG NAG NAG NAG NAG
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:49:33 <augur> elliott: sorry. ive been trying to fix my mbp screen
02:49:36 <augur> i broke the glass :(
02:49:46 <augur> and yet i followed the professional instructions!
02:51:18 <coppro> elliott: surely you have another computer with linux
02:51:27 <coppro> (that was a statement)
02:51:54 <elliott> coppro: I do, yes, but uh ... hmm.
02:52:03 <elliott> getting a friend to do it instead
02:56:07 <ais523> hmm, has thedailywtf's forum actually been patched to allow only haikus?
02:56:14 <ais523> as opposed to a mod doing it manually?
02:56:21 <ais523> (the sidebar forum, not the replies on the articles)
02:56:41 <ais523> well, not only haikus, but posts of approximate haiku length
02:56:56 <ais523> you can write a short plaintext sentence which has a similar length
02:57:09 <elliott> http://forums.thedailywtf.com/forums/t/21032.aspx
02:57:20 <elliott> From henceforth, all messages posted that are not in the form of a Haiku will be deleted.
02:57:20 <elliott> You have been warned. Have a nice day.
02:57:21 -!- poiuy_qwert has joined.
02:57:34 <elliott> ais523: seems like it's some kind of bug
02:57:46 <elliott> ais523: and then it was turned into a haiku rule
02:58:09 <ais523> CS has decided only to allow very short posts due to being broken
02:58:31 <ais523> and the mod's response was, instead of fixing the forum, to institute a "haiku rule" to patch around it
02:59:06 <ais523> now if there was only some website I could post on to report curious perversions in information technology...
02:59:15 <ais523> because that definitely qualifies
02:59:56 <elliott> ais523: http://forums.thedailywtf.com/forums/p/21032/241597.aspx#241597
03:00:29 <ais523> <Daniel Bearsmore> 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 <ais523> elliott: saw it already
03:01:21 <elliott> a horrible asp.net abomination
03:01:22 <ais523> a much-maligned forum that somehow got even worse
03:01:26 <elliott> the real wtf is the daily wtf
03:01:35 <elliott> seriously, why did it have to be alex that started it?
03:01:39 <elliott> he's so close to being the wtf himself
03:03:35 <elliott> ais523: is Username a mod?
03:03:42 <elliott> he has rather ...suspicious... stats
03:14:39 -!- oerjan has quit (Quit: Good night).
03:28:05 -!- elliott has quit (Remote host closed the connection).
03:32:47 <Sgeo> ais523, have you determined the exact allowable length yet?
03:52:26 <Sgeo> According to Star Trek, all aliens want human girls
03:52:35 <Sgeo> Or, human-looking girls
03:56:00 -!- zzo38 has joined.
03:58:30 <zzo38> 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:02:56 <zzo38> To represent the registration of this channel: ircp://irc.freenode.net:6667/cs/info?%23esoteric
04:04:10 <zzo38> coppro: We don't sell that.
04:06:51 <Sgeo> Why would you have a password in a URI?
04:07:28 <zzo38> 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 <zzo38> ircp:// URIs shall be case-insensitive (except the password)
04:11:49 <coppro> it would make far more sense to call this channel ircp://irc.freenode.net:6667/%23esoteric
04:12:32 <coppro> and for instance, its info would be ircp://irc.freenode.net:6667/%esoteric?info
04:12:58 <zzo38> coppro: I understand, but I don't like that much.
04:13:25 <coppro> it's certainly better than putting something dumb like chanserv in there
04:13:46 <zzo38> coppro: But it is the chanserv info, isn't it??
04:13:56 <coppro> but that info might not be provided by chanserv
04:14:13 <coppro> also you're making "cs" be a magic string there
04:14:27 <zzo38> coppro: But then the servers do not have a standard way of retrieving it, and it won't work.
04:14:36 <coppro> zzo38: yes, that's a difficulty
04:14:51 <coppro> zzo38: but you don't have a standard way of asking for "cs" info
04:15:55 <zzo38> 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 <zzo38> (As if they are two separate RFCs or two separate chapters in one RFC, for example.)
04:18:12 <zzo38> 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 <zzo38> There is a command on this IRC server I didn't know, the CHANTRACE command.
04:43:13 <Sgeo> Just put ChanServ in the URI
04:43:33 <Sgeo> Hmm, no, that sucks
04:43:43 <Sgeo> ChanServ might not be the only thing gthat varies
04:43:50 <Sgeo> gVaries, now using glib
04:46:50 <zzo38> Sgeo: It is why I have specified that there is "primary level" and "secondary level".
05:21:45 <zzo38> What is a algorithm for calculating standard deviation (using integers only)?
05:37:58 <quintopia> that sounds difficult, considering the average of integers is not necessarily an integer...
05:38:37 <zzo38> 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 <variable> * chantrace :Outputs a list of members in #channel in ETRACE format, with the classname
08:08:25 <variable> * chantrace :replaced by the server the users are on.
08:12:01 <variable> Sgeo, you have a cloak on - right?
08:12:19 <Sgeo> variable, why?
08:12:24 -!- Wamanuz3 has joined.
08:12:38 <variable> Sgeo, because I think I just found your IP
08:13:03 <variable> but I want to know if cloaks actually work
08:13:24 <Sgeo> variable, well, try finding the IP of someone who's cloaked.
08:14:04 <Sgeo> Unless it's possible to be cloaked without one's knowledge, I am not.
08:14:08 <Sgeo> What made you think I was?
08:15:00 <coppro> cloaks work if you identify before joining a channel
08:15:14 <coppro> I had one for a while myself
08:15:24 <variable> coppro, I know how it works - I misread something
08:15:25 <coppro> but now I have a hostname I'm not interested in cloaking
08:15:34 -!- Wamanuz2 has quit (Ping timeout: 276 seconds).
08:16:16 <coppro> damn you, grad courses
08:17:39 <coppro> variable: there's a course on logic next term I may sit in on
08:18:05 <coppro> it's called "logic for comp. sci." by the registrar
08:18:11 <coppro> which leaves me guessing as to what it actually is
08:18:35 <variable> my favorite subject is logic :-}
08:19:11 <coppro> 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 <coppro> I'm not sure how far above my head it starts
08:23:22 <coppro> 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 <coppro> (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 <variable> coppro, worst case just audit the class
08:29:26 <coppro> variable: if I can find the time, sure
08:29:38 <coppro> and/or if I can follow along
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 <Vorpal> <elliott> ais523: that... sounds like it could rapidly become more than £60 worth of pain <-- (for logs): why £60 specifically?
10:39:03 <Gregor> 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: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:43:48 -!- WAR has joined.
12:44:07 <Phantom_Hoover> 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 <zzo38> 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 <zzo38> I don't think I have written a program in AWK before.
12:47:16 <zzo38> 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: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:54:15 <zzo38> 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 <nooga> why is SPARC system programming is soo undocumented
13:03:13 <zzo38> nooga: I don't know. Are you trying to write a program?
13:33:11 <Vorpal> 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 <nooga> i don't know because i can't find the goddamn docs
13:33:57 <nooga> something like intel's manual
13:34:37 <Vorpal> 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 <Vorpal> going to reboot for kernel upgrade on the computer running this irc bouncer
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 <fizzie> IIRC running out of register window "depth" generates an exception, and then an OS exception handler will do some stack-pushery.
13:54:48 <fizzie> nooga: http://developers.sun.com/solaris/articles/sparcv9.pdf not good enough for your purposes?
14:05:54 -!- sftp has joined.
14:06:52 <nooga> fizzie: lol, i'm stupid
14:07:04 <nooga> i found that earlier and forgot that i have it :G
14:22:03 -!- Vorpal has joined.
14:43:45 <fizzie> 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 <zzo38> What are algorithms for calculating such things as standard deviation, etc?
14:54:56 <oerjan> zzo38: http://en.wikipedia.org/wiki/Standard_deviation#Rapid_calculation_methods
14:58:04 <fizzie> 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 <zzo38> The algorithm described there should work.
15:00:07 <zzo38> How large do you expect $s_2$ to become in case of a large set of cards?
15:01:17 <oerjan> fizzie: well the clever thing about it afaik is that you can calculate it in one pass...
15:01:51 <oerjan> zzo38: well it should be less than N times the square of your maximal value...
15:02:02 <fizzie> oerjan: Well, yes, that is what I was alluding to with the "running" part.
15:02:13 <oerjan> (this is of course rather trivial)
15:03:14 <fizzie> Anyhoo, quite often doing two passes is not a problem either.
15:03:34 <fizzie> The see-also "computing variance" article is a bit more comprehensive.
15:14:50 <Vorpal> fizzie, presumably there is some trap when going the other way too? (In order to unspill when required)
15:15:11 <fizzie> Yes, there's a "window underflow" trap too.
15:17:12 <fizzie> (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 <nooga> fizzie: you seem to know SPARCs pretty well
15:18:25 <Vorpal> fizzie, hm... You mean like, store/restore windows on context switch?
15:19:05 <Vorpal> if so, not sure how much it differs from normal storing/restoring of registers on other platforms (such as x86)
15:19:08 <fizzie> 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 <fizzie> nooga: Not really, I've just read a bit back when doing our compiler course, which had a sparc backend.
15:19:52 <Vorpal> fizzie, but what if you have three processes?
15:20:17 <fizzie> 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 <Vorpal> fizzie, so the OS will spill/unspill as required then?
15:22:34 <Vorpal> 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 <fizzie> 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 <Vorpal> fizzie, right, but if it uses all N then this would mean more switches to kernel mode?
15:23:43 <Vorpal> which are usually slow on most architectures
15:25:03 <fizzie> 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 <zzo38> 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 <Vorpal> 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 <zzo38> (I don't think there is, but if you know of it, tell me)
15:26:52 <Vorpal> zzo38, better than what?
15:27:02 <fizzie> Vorpal: Yes, I saw that, though I already managed to forget it.
15:27:08 <Vorpal> zzo38, and to calculate what?
15:27:50 <fizzie> Standard deviation, I assume.
15:27:58 <Vorpal> fizzie, well, if you happen to have time to test it...
15:28:58 <fizzie> 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 <zzo38> I know since it is sorted, it can easily calculate minimum, maximum, median.
15:33:07 <zzo38> Which other statistics would be useful for a set of cards (such as for Magic: the Gathering and similar games)?
15:35:13 <fizzie> Histograms of different categorizations? (I seem to recall MtG cards can be grouped into lands/creatures/instants/whatevers.)
15:36:06 <zzo38> fizzie: Yes, the category by card type.
15:36:57 <zzo38> I can do like that, I already have grouping.
15:37:49 <zzo38> Another question, about notation: if $Q_2$ is median, does $Q_0$ mean the minimum?
15:38:46 <zzo38> 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 <zzo38> It doesn't mention $Q_0$ or $Q_4$ (or $Q_5$, but that doesn't make sense).
15:39:43 <Phantom_Hoover> Yes, so Q_0 and Q_4 could easily be read as the maxima and minima, but they're never actually defined.
15:41:00 <zzo38> I could just add a note next to the equation that explains this notation.
15:42:41 -!- elliott has joined.
15:42:43 <fizzie> 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 <fizzie> (I want to see what sort of numbers the server sends before blindly fixing that.)
15:44:30 <Phantom_Hoover> 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 <Phantom_Hoover> 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 <elliott> Phantom_Hoover: you must be SO POPULAR
15:47:37 <Phantom_Hoover> elliott, I am actually banned from setting foot in the maths department.
15:48:03 <elliott> You might mess up the dangerous maths experiments.
15:49:24 <fizzie> 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 <Phantom_Hoover> "Safety: the natural logarithm is an irritant and should be washed away if it comes into contact with the skin."
15:50:30 <elliott> fizzie: I think it's better without.
15:55:10 <Phantom_Hoover> fizzie, are the Finnish words for "oxygen" and "vulva" really only a letter apart?
15:55:35 <elliott> Both are required breathing for continued existence.
15:58:57 <fizzie> Phantom_Hoover: I don't think so. But the words for "vulva" and "cone" (as in "pine cone", not as in "geometric shape") are.
16:00:01 <fizzie> Phantom_Hoover: As are the words for "oxygen" and a very colloquial term for the penis.
16:01:21 <fizzie> ("häpy", "käpy" and "happi", "heppi", respecitvely.)
16:02:06 <oerjan> i take it finns are fond of happiness
16:02:13 <fizzie> There's more than a single-letter difference between häpy/happi, though.
16:02:24 <fizzie> They *are* quite close, I guess.
16:02:38 <elliott> Häpy heppi, heppi käppy. Käppy happi, happi häpy.
16:02:50 <elliott> Häpy heppi, heppi käpy. Käpy happi, happi häpy.
16:04:00 <Deewiant> Sharing consonants does not two words alike make.
16:04:35 <Phantom_Hoover> Deewiant, consonants and similar phonetic properties if you don't know Finnish orthography!
16:04:52 <fizzie> 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:39 <fizzie> Well, it's a stop consonant, only longer-duration one.
16:06:25 <fizzie> Phantom_Hoover: Why couldn't you?
16:06:41 <fizzie> http://en.wikipedia.org/wiki/Stop_consonant#Length
16:06:45 <olsner> english has a few double-consonants too
16:06:58 <elliott> fizzie: Can you prove that Finnish isn't just a gigantic prank on the rest of the world?
16:07:10 <Deewiant> Can you prove that English isn't?
16:07:32 <elliott> Deewiant: Maybe it is, but if it is, it's a lot less funny than Finnish
16:08:00 <Phantom_Hoover> Deewiant, it's more what you get when you take about 3 languages and mush them together without thinking.
16:08:10 <elliott> English is like "A man walks into a bar. He is an alcoholic and it's destroying his family."
16:08:44 <oerjan> `translatefromto en fi A man walks into a bar. He is an alcoholic and it's destroying his family.
16:08:53 <Deewiant> http://www.youtube.com/watch?v=yL21sCWfnbE&t=1m8s "tuki" vs "tukki"
16:09:01 <HackEgo> Mies kävelee baariin. Hän on alkoholisti ja se tuhoaa hänen perheensä.
16:09:30 <Deewiant> (Disclaimer: I don't know if the guy knows what he's talking about, I just searched for an example)
16:11:32 <zzo38> The <math> 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 <Phantom_Hoover> Wait, is a long stop just one in which you wait for a bit before removing the obstruction from the airway?
16:12:49 <zzo38> Phantom_Hoover: Does LaTeX not have any \def command?
16:13:31 <elliott> Phantom_Hoover: No -- zzo38 just hates it.
16:13:35 <elliott> Phantom_Hoover: I think LaTeX is great.
16:13:57 <Phantom_Hoover> Well, there *is* nothing that doesn't suck in zzo's world, unless he made it himself.
16:14:54 <fizzie> 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:41 <fizzie> Oh, I thought you were trying to describe what Deewiant's video was like.
16:15:46 <Phantom_Hoover> 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 <zzo38> (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 <Phantom_Hoover> That guy was going on about glottal stops, so I suspect he may have no idea what he's talking about.
16:16:15 <fizzie> However, "ex-stop" and "explosive" are a very different thing.
16:16:25 <Vorpal> 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 <zzo38> Vorpal: What kind of effect, do you have to pronounce it longer?
16:17:31 <Vorpal> zzo38, it modifies the preceding vowel.
16:18:41 <fizzie> For Finnish it'd just be mostly a lenghtening. Compare "hila" (wicket/grate/grid) and "hilla" (cloudberry).
16:19:07 <Vorpal> elliott, as I said yes
16:19:18 <elliott> You are probably not lying entirely!
16:19:29 <fizzie> Our phonology is a bit on the simplistic side.
16:20:08 <fizzie> Ooh, Wikipedia has examples, I don't need to invent any:
16:20:09 <fizzie> tuli = fire, tuuli = wind, tulli = customs
16:20:09 <fizzie> muta = mud, muuta = other (partitive sg.), mutta = but, muuttaa = to change or to move
16:20:12 <fizzie> http://en.wikipedia.org/wiki/Finnish_phonology#Length
16:20:42 <Vorpal> in Swedish the word "hade" (meaning "had") is pronounced as if it had been written like "hadde" btw.
16:20:55 <Phantom_Hoover> <olsner> english has a few double-consonants too ← not any with syntactic meaning AFAIK.
16:21:28 <Vorpal> <fizzie> 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 <Vorpal> well, not meaning. Word
16:22:17 <olsner> Phantom_Hoover: I mean double consonants that are pronounced longer
16:22:55 <olsner> I think it's mostly when combining a word that ends with the same consonant the other word starts with
16:23:44 <Vorpal> 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 <Vorpal> (isn't it just a change in stress or whatever it is called?)
16:24:45 <olsner> in those examples, it's tonal differences rather than stress
16:25:20 <Vorpal> 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 <fizzie> [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 <olsner> Vorpal: I think stress is what happens with our double consonants
16:28:52 <Vorpal> olsner, ah, but no cases with same spelling then?
16:29:00 <fizzie> Also, "omenanamme" = "as our apple", "omenan amme" = "apple's bathtub".
16:29:14 <olsner> Vorpal: not that I can think of, but there probably are
16:32:28 <fizzie> 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 <Vorpal> fizzie, "[...](...preceded by an agent in genitive, "by someone")[...]" <-- a cleaning agent?
16:33:52 <fizzie> Unfortunately the stress-indicating bold font parts got lost.
16:34:06 <Vorpal> fizzie, well the channels filter bold I think
16:34:31 <fizzie> That should've been [*ˈpuː-ˌnɑː*-mɑ] vs. [*ˈpuː*-nɑː-mɑ].
16:38:02 <Phantom_Hoover> fizzie, not as bad as the English words which are spelt identically but pronounced differently.
16:39:17 <Vorpal> Phantom_Hoover, such as?
16:39:28 <Vorpal> I can't think of any example atl
16:40:06 <Phantom_Hoover> Which are both because "ea" can be pronounced 'eh' or 'ee'.
16:41:20 <Vorpal> hm, Does any other language have the sje-sound of Swedish? I seem to remember reading it was unique
16:41:49 <Vorpal> well, Finland-Swedish (or whatever the English name of it is) has it obviously
16:41:59 <Ilari> 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 <Vorpal> 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 <olsner> Vorpal: does it though? some dialects has it as sh, seem to recall finland-swedish doing that too
16:43:11 <Vorpal> olsner, they have a different variant of it, that's true.
16:44:55 <Vorpal> 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 <olsner> kjol doesn't have a sje-sound
16:45:23 <Vorpal> olsner, what do you call that sound then?
16:46:50 <zzo38> Today I learned AWK programming.
16:47:02 -!- cheater99 has quit (Ping timeout: 240 seconds).
16:47:09 <Deewiant> Vorpal: http://en.wikipedia.org/wiki/Sje-sound#Colognian
16:48:15 <fizzie> 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 <Vorpal> 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 <Vorpal> (basically I got lost in the jargon)
16:48:37 <fizzie> Deewiant: This is what you get when you let languages go all natural.
16:48:54 <Deewiant> fizzie: I know, I didn't say that it was in another language, I just linked it
16:50:05 <olsner> Vorpal: I would call it http://en.wikipedia.org/wiki/Voiceless_postalveolar_fricative but wikipedia claims swedish kjol has a different sound
16:50:42 <olsner> namely, this one: http://en.wikipedia.org/wiki/Voiceless_alveolo-palatal_fricative
16:51:24 <Vorpal> 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 <fizzie> 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 <elliott> fizzie: I propose mindlinks.
16:52:28 <olsner> Vorpal: yeah, it merges with the vowel a bit, dunno if it's enough of a difference to call it different sounds
16:58:14 <fizzie> 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:16 <Vorpal> elliott, you seem to have connection problems today?
17:00:28 <elliott> Vorpal: um i think i've gone offline exactly twice?
17:00:44 <elliott> can his nick stop shouting
17:01:58 -!- LORD_NIETZSCHE has left (?).
17:07:05 -!- cheater99 has quit (Read error: Connection reset by peer).
17:09:36 <elliott> 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 <Phantom_Hoover> elliott, the upside-down K is the height of stupidity.
17:26:05 <nooga> http://www.complexitygraphics.com/#708027/-About-Contact <3
17:27:49 <Phantom_Hoover> [[Graduated from Moscow State University in Social Psychology, and then studied in High Academic School of Graphic Design. ]]
17:28:09 <elliott> her knees are too angular anyway!
17:29:14 <Phantom_Hoover> Wow, I never realised that the Oolite theme gets way better if you wait a bit.
17:29:40 <elliott> Phantom_Hoover: Define theme.
17:31:30 <elliott> Phantom_Hoover: guy in #anagol just said php is better than haskell
17:32:16 <elliott> Phantom_Hoover: nothing else was said
17:32:31 <Phantom_Hoover> elliott, well at least tell them that they're an idiot!
17:33:02 <elliott> Phantom_Hoover: http://sprunge.us/YTNc
17:33:24 <elliott> 17:31 Endres: um, but I think for me it is so
17:33:24 <elliott> 17:32 Endres: maybe not better, but... easier maybe?
17:33:35 <elliott> not even gonna bother arguing ... 'specially since obvs not a native
17:34:21 <elliott> Phantom_Hoover: i think it was technically basic that i never tried to understand and just copied from a book
17:34:26 <nooga> PHP should be evaporated together with every dedicated PHP programmer
17:34:31 <elliott> but um, pretty much php, yeah
17:34:57 <elliott> no, i chose to learn it myself
17:35:01 <nooga> i was 10 when i tried Pascal, don't worry elliott
17:35:07 <elliott> after learning that $favourite_website was written in PHP
17:35:21 <elliott> Phantom_Hoover: i used odbc to communicate with an Access database in PHP
17:35:42 <elliott> I need some alcohol to forget that now
17:35:59 <elliott> Phantom_Hoover: this was before ubuntu even existed
17:36:06 <elliott> Phantom_Hoover: also we had a winmodem
17:36:23 <Phantom_Hoover> Followed soon by Python, then about a week later by CL.
17:36:54 <elliott> Phantom_Hoover: You are the luckiest bastard. Seriously.
17:37:15 <elliott> Phantom_Hoover: OK, Pascal is kind of shit, but it's not a /hideous/ language.
17:37:23 <elliott> Phantom_Hoover: Python is lame but really, it's not _that_ bad.
17:37:29 <elliott> Phantom_Hoover: And then Common Lisp which is pretty damn good.
17:37:39 <elliott> Phantom_Hoover: I stayed with PHP for about _two years_.
17:37:51 <elliott> Do you have *any* idea how warped my grey matter became?
17:37:55 <Phantom_Hoover> elliott, it was when you were asked to conceive and implement a sort algorithm by yourself.
17:38:21 <Phantom_Hoover> With a teacher who as far as I know was a Latin teacher who later became the computing teacher.
17:38:23 <elliott> I had no idea why you would ever abstract anything. No idea how to modularise code.
17:38:32 <elliott> No idea that mixing code and, you know, output was in any way sub-optimal.
17:38:54 <variable> elliott, that is indicative of bad PHP coding - not necc. the language itself
17:39:06 <variable> although I will say that most PHP examples are HORRIBLE
17:39:10 <elliott> variable: Perhaps. But PHP certainly lends itself to bad coding style.
17:39:11 <nooga> elliott: don't worry
17:39:14 <Phantom_Hoover> variable, yes, but when the language is definitely not conducive to that style...
17:39:18 <elliott> variable: And even when it's coded perfectly, it's still a horrible language.
17:39:36 <variable> elliott, it is not horrible for its purpose
17:39:58 <nooga> uhmit is horrrible for every purpose
17:40:11 <nooga> i code php for *cough* money
17:40:16 <elliott> 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 <Phantom_Hoover> FWIW, I actually got my self-conceived sort algorithm off the ground when I used CL.
17:40:30 <elliott> 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 <Phantom_Hoover> 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 <elliott> Phantom_Hoover: I don't think you can even do that
17:41:29 <elliott> variable: http://catseye.tc/about/php.html
17:41:46 <elliott> The fourth paragraph of that is perhaps my favourite thing ever.
17:41:54 <Phantom_Hoover> He basically told me to either use globals or alter the array passed to it.
17:42:05 <elliott> Already Phantom_Hoover knew the putrid stench of mutability!
17:43:05 <Phantom_Hoover> 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:36 <elliott> I like how you're apologising for not being a rabid functional weenie by 13.
17:43:39 <nooga> 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:47 <nooga> i will code only in this language
17:43:55 <elliott> nooga: And is purely functional?
17:44:09 <nooga> elliott: not Haskell
17:44:17 <elliott> nooga: There are purely-functional languages that are not Haskell.
17:44:40 <nooga> i like mixed paradigm languages, like ruby
17:44:57 <elliott> nooga: Irrelevant; answer the question: mutable data?
17:45:34 <nooga> immutable = useless
17:45:53 <nooga> I LIKE to mess with arrays in-place
17:46:08 <elliott> 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 <elliott> 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 <elliott> Otherwise you throw away abstraction.
17:47:17 <nooga> i know haskell is awesome and it's compiler is a piece of art
17:47:39 <elliott> clearly you have never seen ghc code
17:47:44 <elliott> nobody gives a shit what the compiler looks like
17:47:55 <elliott> anyway i don't even like haskell all that much, it has many flaws, but that's irrelevant
17:48:03 <elliott> the fact is that mutability is a serious, crippling design flaw
17:48:27 <elliott> Phantom_Hoover: It's not Epigram.
17:48:55 <elliott> 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 <nooga> and i like to have more expressive C with poorman's, basic oo, closures and ability to mess with the language itself
17:49:05 <elliott> Phantom_Hoover: and the fact that I don't like the IO monad
17:49:11 <elliott> also, records with named fields are handled badly
17:49:32 <elliott> Phantom_Hoover: it's imperative.
17:49:51 <elliott> Phantom_Hoover: If you disagree, see http://conal.net/blog/posts/the-c-language-is-purely-functional/
17:50:11 <nooga> it's funny that ppl try to make languages that work AGAINST common sense and our machines architecture
17:50:33 <elliott> nooga: Programs are for humans first; machines second. P.S. That machines are imperative is a mistake of history.
17:50:38 <elliott> See http://www.cs.york.ac.uk/fp/reduceron/.
17:50:55 <elliott> 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 <nooga> if we had purely functional machines it would be sooo cooool
17:51:28 <nooga> MIPS, x86, eeee, SPARC.... eee
17:51:41 <elliott> nooga: http://www.cs.york.ac.uk/fp/reduceron/
17:51:51 <nooga> but nobody uses it!
17:51:55 <elliott> nooga: if we had OS X and Linux it would be soo cooool
17:52:01 <elliott> nooga: but we don't, because 90% of people use Windows!
17:52:06 <elliott> too bad OS X and Linux don't exist
17:52:29 <elliott> 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 <j-invariant> 17:50 < elliott> nooga: Programs are for humans first; machines second. P.S.
17:53:09 <elliott> j-invariant: almost direct sicp quote :) or was it R5RS... whatever
17:53:13 <elliott> it's true wherever it came from
17:53:14 <Phantom_Hoover> elliott, but the fact that there seems to be no viable alternative makes complaining rather pointless.
17:53:44 <elliott> 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 <elliott> It _is_ relevant to complain that an existing solution is bad; innovation has to handle the rest.
17:54:31 <elliott> j-invariant: are those Cs typo?
17:55:54 <elliott> 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 <elliott> le functors and the like -- also maybe some ideas from Ur in this area -- ...
17:55:57 <elliott> j-invariant: make it epigram ...
17:56:04 <elliott> j-invariant: ... and then make it epigram some more
17:58:20 <elliott> j-invariant: also: redo the whole stdlib
17:58:31 <elliott> j-invariant: proper numeric typeclasses (except, module signatures now, not typeclasses!)
17:58:47 <elliott> j-invariant: maybe if you don't want a useful language :)
17:58:51 <elliott> j-invariant: fine in Coq, not for Haskell ...
17:59:18 <j-invariant> The first thing I do in Coq is turn off the massive stdlib and bootstrap my own tools :P
17:59:32 <elliott> j-invariant: that's just because coq's stdlib is really shitty
17:59:40 <elliott> j-invariant: and also because you presumably don't write actually useful Haskell programs ;) no offence
17:59:42 <nooga> HOW AM I SUPPOSED TO WRITE ANYTHING WITHOUT IO THAT CAN BE SYNCED WITH OTHER SYSTEMS
17:59:55 <elliott> nooga: i don't give a shit about your needs/wants :)
18:00:04 <elliott> in @ it all works out perfectly of course.
18:00:14 <nooga> how do you imagine purely functional OS
18:00:27 <j-invariant> elliott: I mean you should still be able to do "import Numbers" or whatever it is you want
18:00:43 <j-invariant> elliott: but all this e.g. "Num" crap shouldn't be imported to all programs automatically
18:00:45 <elliott> 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 <elliott> j-invariant: Num is crap, but if it were better designed ...
18:01:07 <j-invariant> elliott: I don't think language designers are capable of making a good stdlib
18:01:28 <elliott> 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 <j-invariant> also the evolution of the language is at a different pace than that of the stdlib
18:01:58 <elliott> @ updates are almost as likely to update the language as the core stdlib, I'd say
18:02:37 <elliott> @ is a macro expanding to whatever the final name of @ has.
18:03:26 <nooga> does it have a homepage?
18:03:37 <elliott> no, it has no need of one.
18:03:41 <elliott> the channel logs are an okay start.
18:04:05 <nooga> nonexistant, useless
18:04:23 <elliott> nooga: I don't care about your needs/wants.
18:04:48 <Phantom_Hoover> elliott, but tonnes of the discussion was in private queries!
18:05:18 <elliott> hmm, @ has the deficiency of being hard to grep
18:05:41 <elliott> 10.09.19:07:41:54 <nooga> alise: start writing aliseOS plz
18:05:45 <elliott> But I thought it was *useless*.
18:08:55 <elliott> Phantom_Hoover: i hire you to work on it
18:10:01 <elliott> Phantom_Hoover: don't use dice then
18:12:20 -!- BeholdMyGlory has quit (Remote host closed the connection).
18:13:53 <j-invariant> elliott: what about Idirs http://www.cs.st-andrews.ac.uk/~eb/
18:14:22 <elliott> 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:47 <elliott> 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 <elliott> but is more, you know, decidable :)
18:14:58 <elliott> j-invariant: nonono i love dependent types
18:15:04 <elliott> j-invariant: for theorem proving and formal verification and shit
18:15:17 <elliott> j-invariant: i just think a 75% + stuff solution might be best for everything else
18:15:33 <j-invariant> elliott: even to use something as simple as quotient types, I think you need full blown theorem proving
18:15:46 <elliott> j-invariant: are quotient types that useful outside of theorem proving?
18:17:18 <elliott> either j-invariant is having a worldview breakdown or has shunned me
18:20:15 <oerjan> actually you killed the whole channel *sputter, argh*
18:27:44 <j-invariant> module Z (inject, (+), (*)) where type Z = (N,N) ; inject :: N -> Z ...
18:28:01 <elliott> j-invariant: what's that from
18:28:26 <j-invariant> 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:38 <elliott> j-invariant: are you trying to demonstrate ML modules or?
18:28:39 <nooga> http://wronki.pl has AD 2011 bug :F
18:28:41 <elliott> or are you just asking a really vague question
18:28:48 <elliott> j-invariant: nono i want to understand
18:29:07 <j-invariant> elliott: you can define integers as a quotient on pairs of natural numbers (you know that?)
18:29:21 <elliott> ifeq ($(shell expr "$(uname_R)" : '[15678]\.'),2)
18:29:21 <elliott> OLD_ICONV = UnfortunatelyYes
18:29:42 <elliott> j-invariant: well the Works But Kind Of Horrible solution here is obvious
18:29:42 <j-invariant> 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 <elliott> j-invariant: just define your own (==)
18:29:59 <j-invariant> then MyModule imports that, uses the functions with Z to its hearts content and all is well
18:30:47 <j-invariant> by all is well, I mean that every function MyModule can define respects the equivalence relation
18:32:38 <elliott> well Coq's knowledge of modules is limited i think
18:32:53 <j-invariant> oh wait a second, it might be possible to prove this in Coq
18:33:22 <j-invariant> if you implement a non-quotient version of Z and make a map between that and the quotient version
18:35:00 <nooga> boring boring boring
18:36:34 -!- zzo38 has quit (Quit: All the letters on one side OK).
18:38:37 <elliott> j-invariant: have you ever looked at Clean?
18:44:07 <Vorpal> fizzie, what does this mean? 18:56:48 [DIED] world.c: 108: broken decompressed chunk length: 49 != 50
18:44:30 <elliott> chunk was meant to be X long, it was Y. i would presume.
18:44:47 <Phantom_Hoover> elliott, Vorpal, fizzie, Deewiant, has anything actually been done on the MC server?
18:44:54 <elliott> Phantom_Hoover: since when
18:46:37 <elliott> fizzie: can i rewrite mcmap in ML or something
18:50:16 <Vorpal> 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 <elliott> Vorpal: not if I compiled it with MLton :)
18:50:55 <Vorpal> elliott, what is MLton?
18:51:30 <Vorpal> elliott, hm is it really that good?
18:52:06 <elliott> not like mcmap is hugely resource-intensive or hugely speed-needing
18:52:49 <Vorpal> elliott, true, I was thinking of memory overhead
18:53:04 <Vorpal> elliott, which is the problem for me with minecraft alone
18:53:23 <elliott> well, these sorts of compilers usually try and unbox everything.
18:53:56 -!- Zuu has joined.
18:54:00 -!- Zuu has quit (Changing host).
18:54:01 -!- Zuu has joined.
18:54:13 <Vorpal> how well does it manage though
18:54:47 <elliott> It's not like unboxing is hard.
18:55:00 * Zuu unboxes elliott
18:57:21 <Phantom_Hoover> FWIW, I think we should try proper survival multiplayer.
18:57:51 <Phantom_Hoover> elliott killing Vorpal every 10 seconds by "accident" would be rather amusing.
18:58:14 <elliott> Phantom_Hoover: When the SMP server was up, I killed ineiros and got 64 mob spawners
18:58:17 <elliott> Alas, they spawned only pigs.
18:58:41 <elliott> Phantom_Hoover: Yes, for something like a day.
18:58:52 <elliott> Phantom_Hoover: Vorpal is too pussy to go on though. He'd just sit on IRC crying about his house.
18:59:00 <elliott> (Side note - if we do - it must be on the same map.)
19:02:31 <fizzie> Vorpal: It means the zlib truncation bug I tweeted (but Notch ignored) has actually resulted in an incomplete chunk update.
19:02:59 <elliott> fizzie: Notch, fix actual bugs?
19:03:04 <elliott> Hahahahahahahahaahahahahahahhahahahahahahahahaha
19:03:17 <elliott> Too busy getting internet fellatio from Twitter.
19:03:46 <fizzie> I may fix it to ignore those too, as long as the truncation affects only the light values, which I ignore.
19:03:53 <Phantom_Hoover> <fizzie> 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 <fizzie> Phantom_Hoover: <Vorpal> fizzie, what does this mean? 18:56:48 [DIED] world.c: 108: broken decompressed chunk length: 49 != 50
19:07:18 <elliott> j-invariant: have you finished epigram yet
19:07:40 <Phantom_Hoover> For instance, there's a bug which will crash any server whatsoever and can be done with effectively no privileges.
19:08:01 <Phantom_Hoover> No, I'm not saying what it is, and noöne else who knows should either.
19:08:34 <elliott> Phantom_Hoover killed a server with 1,000 people on it permanently once with that bug. True story!*
19:09:03 <olsner> true for very false values of 'true'
19:16:15 <nooga> reimplement minecraft
19:19:11 -!- Zuu has quit (Ping timeout: 260 seconds).
19:20:27 <elliott> j-invariant: well get crackin'!
19:20:32 -!- Zuu has joined.
19:20:56 <j-invariant> 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:12 <elliott> j-invariant: Because Coq is stupid.
19:21:25 <elliott> j-invariant: Epigram has everything! Including kittens! Nah, I don't actaully know.
19:21:41 <j-invariant> elliott: if I could get an isomorphism between F(M) and F(M') I could have something like useful quotients
19:22:08 <elliott> 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 <j-invariant> maybe I should apply that mu- thing to a language with modules
19:22:54 <j-invariant> it's smoe magic way to turn a programming language into a dependently typed one
19:23:25 <j-invariant> they did it to a sort of haskell liek language and got a simple version of agda out
19:23:42 <elliott> j-invariant: what happens when you apply it to C
19:23:46 <j-invariant> if we throw modules in maybe we'll get quotients out
19:23:48 <elliott> does it kill you and your family?
19:23:50 <j-invariant> elliott: well it has to be a lambda calculus
19:24:32 <elliott> coppro (coppro is the entire u/waterloo)
19:24:56 <elliott> OF HTHE THWEOITH IOEDFJHDFGMLKDFGNHDKL;FGH
19:24:59 <Vorpal> check their website for opening hours
19:25:03 <j-invariant> elliott: excerice, prove the theorem http://pastebin.com/6P2ydkcU
19:25:49 <elliott> j-invariant: for your homework, prove goldbach's conjecture
19:25:56 <Vorpal> elliott, well oerjan seemed afk
19:26:41 <elliott> j-invariant: (+,N):Z :: (*,Z):Q :: (^,Q):??
19:27:02 <nooga> netcraft is an internet services company based in england
19:27:17 <elliott> nooga doesn't know who netcraft are lol
19:27:23 <elliott> nooga is young netcraft confirms it
19:27:54 <elliott> j-invariant: (+,N):Z :: (*,Z):Q :: (^,Z):??
19:28:22 <elliott> 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 <elliott> j-invariant: just wonder what happens when you put in (^,Z)
19:28:38 <elliott> (a,b) represents a-b or a/b
19:28:48 <nooga> we were talking about minecraft reimplementation, not a company with rainbow logo
19:28:50 <elliott> (a,b) represents a((^)^-1)b
19:30:19 <elliott> j-invariant: you work out what comes out :P
19:31:07 <elliott> well obviously (x,x^n) = n
19:32:57 <elliott> 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 <elliott> j-invariant: does the mu thing have to be a lambda calculus strictly?
19:35:07 <elliott> or can any similar-ish structure do
19:35:13 <elliott> I'd love to see a dependent-typed term rewriting language
19:37:04 <j-invariant> elliott: Realizability and Parametricity in Pure Type Systems
19:37:25 <elliott> j-invariant: that'd require actual thought!!!!
19:38:58 <j-invariant> We describe a systematic method to build a logic from any
19:38:58 <j-invariant> programming language described as a Pure Type System (PTS). The
19:38:58 <j-invariant> formulas of this logic express properties about programs. We define a
19:38:58 <j-invariant> parametricity theory about programs and a realizability theory for the
19:38:58 <j-invariant> logic. The logic is expressive enough to internalize both theories. Thanks
19:39:00 <j-invariant> to the PTS setting, we abstract most idiosyncrasies specific to particular
19:39:03 <j-invariant> type theories. This confers generality to the results, and reveals parallels
19:40:09 <elliott> j-invariant: i wish i was cool enough to have my own dependent language :p
19:40:40 <j-invariant> just pick some esoteric PTS nobody cares about and apply this paper to it
19:41:01 <elliott> j-invariant: bah -- i still want a language based on dual-intuitionistic logic
19:41:05 <elliott> j-invariant: paraconsistent type system, how cool is that?
19:41:13 <elliott> function arrow replaced with "butnot"
19:41:23 -!- BeholdMyGlory has joined.
19:41:59 <elliott> j-invariant: hmm maybe i will try hacking up a dependent language
19:42:22 <j-invariant> elliott: one with delimited continuations?
19:42:31 <j-invariant> you can prove stuff that Coq and Agda can't prove if you do that
19:42:31 <elliott> j-invariant: you can implement them on top of a language can't you?
19:42:47 <elliott> 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:52 <j-invariant> 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 <j-invariant> I just mean typing out lambda terms to prove things
19:43:50 <elliott> j-invariant: maybe i can write a lazy specialiser for it and i will have succeeded in creating the Best Language :)
19:45:20 <elliott> j-invariant: I wish Scheme was a better language because Ponzi Scheme is an awesome name
19:45:45 <elliott> even though i don't really want to
19:46:03 <elliott> ok so scheme is actually pretty nice
19:46:13 <elliott> 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:33 <elliott> 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:59 <elliott> pikhq: ./configure --prefix=/usr/local && make && make install DESTDIR=root && mkdir /stow/foo && cp root/usr/local/* /stow/foo
19:49:10 <elliott> Just about everything supports DESTDIR so this works great.
19:49:17 <elliott> (Even Python's setup.py does.)
19:53:55 <elliott> j-invariant: you know that de-bruijn-for-bound-stuff-names-for-unbound-stuff?
19:54:14 <elliott> j-invariant: that the epigram people do
19:54:23 <elliott> I am not a number, I am a free variable
19:54:36 <elliott> 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:57 <elliott> j-invariant: not as in, the actual code we write!
19:55:01 <elliott> but i think compilers should do it like that
19:55:18 <elliott> i mean an assignment like that is basically a let around the whole program
19:55:20 <j-invariant> if everything is a lambda, then you can't step inside an abstraction cayou?
19:55:25 <elliott> and let x=y in z is just (\x->z)y
19:55:47 <elliott> j-invariant: that isn't really what i mean
19:55:51 <elliott> j-invariant: i don't mean every object should be a lambda
19:56:09 <elliott> 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 <elliott> and have everything be de bruijn
19:56:26 <elliott> it's simpler to process :D
19:57:13 <elliott> "I'd like to thank this /r/programming thread http://bit.ly/eNygOX for helping me adjust to senescence." --pigworker
19:58:18 <elliott> 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 <elliott> BUT THAT'S BORING PRACTICAL PROBLEMS
19:58:42 <elliott> obviously we just redo every single piece of code every time a single byte changes
20:03:49 <elliott> j-invariant: quick, what should i put in my silly language
20:04:25 <elliott> j-invariant: that sounds really painful to do :>
20:05:34 <elliott> j-invariant: can i add them after everything else or should i really do them first
20:08:59 <elliott> j-invariant: i am getting slightly disillusioned with all the provers :-.
20:09:39 <elliott> j-invariant: let's go back to ridiculously dynamically typed, late-bound languages and write unit tests
20:09:58 <elliott> j-invariant: Unit tests prove goldbach!!!!!!
20:10:17 <elliott> j-invariant: (if I keep this up I'll turn into Zeilberger)
20:10:21 * pikhq is still completely blown away by the recent PS3 hack...
20:10:29 <elliott> or Chaitin... "Add an axiom!"
20:11:15 <elliott> Phantom_Hoover: http://i.imgur.com/rwmHO.png The PAXEL
20:11:18 <j-invariant> elliott: oen of my concerns is how large scale programming can work
20:11:35 <pikhq> j-invariant: The hack by fail0verflow, which contains all of Team Twiizers, detailed at 27C3 recently.
20:11:39 <j-invariant> elliott: category theory may be the solution to it
20:11:40 <elliott> j-invariant: this is why i was talking about a 75% solution for all the not-just-pure-proving work
20:11:42 <pikhq> j-invariant: Well, rather, the *set* of hacks.
20:11:56 <elliott> j-invariant: like, I don't look at Idris or Ur and think "will this scale to bigger things..."
20:11:58 <pikhq> j-invariant: The most hilarious one is that they have the signing key now.
20:12:52 <pikhq> You see, Sony signs things using ECDSA, which requires, as part of the algorithm, a cryptographically secure random number.
20:12:59 <pikhq> Sony, however, uses a *constant* instead.
20:13:14 <pikhq> Which allows you to get the private key using simple algebra.
20:13:49 <j-invariant> "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 <pikhq> So, the PS3 is as hacked as it is possible to be.
20:15:19 <pikhq> 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> <elliott> Phantom_Hoover: http://i.imgur.com/rwmHO.png The PAXEL ← WANT
20:15:36 <j-invariant> pikhq: I guess the PS3 devs grew up writing websites that don't santies SQL inputs
20:16:15 <elliott> Phantom_Hoover: there's actually a mod for it lol
20:16:18 <elliott> except it looks slightly less silly
20:16:29 <elliott> j-invariant: obviously we can solve that with DEPENDENT TYPES
20:16:32 <elliott> Phantom_Hoover: client only
20:17:01 <pikhq> It is, in fact, more hacked than the Wii now.
20:19:55 <elliott> Phantom_Hoover: http://dl.dropbox.com/u/14765180/AnimalCrafting/screenshots/animalcrafting16.png WORST TEXTURE PACK
20:20:42 <elliott> Phantom_Hoover: Gravel. Seriously.
20:20:54 <elliott> http://i.imgur.com/1Z1Bw.jpg omg that reminds me i need to install ambient occlusion. and painterly.
20:21:28 <fizzie> That animalcrafting16.png reminds me of one of the early 3D Sonics, for some reason.
20:21:44 <elliott> it's animal crossing methinks
20:22:01 <elliott> Phantom_Hoover: lol the reddit thread is filled with OMG WHAT TEXTURE PACK
20:26:40 <nooga> so what;s with this reimplementation
20:27:09 <elliott> nooga: what reimplementation
20:28:22 <elliott> 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:43 <elliott> http://www.minecraftforum.net/viewtopic.php?f=1&t=45590
20:30:13 <elliott> 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 <elliott> Oh god I cannot stop laughing
20:30:25 <nooga> elliott: reimplementation of minecraft
20:31:02 <elliott> Phantom_Hoover: He is so happy. Unintentionally.
20:31:03 <j-invariant> it's funny how everyone left digg for reddit, now people rae leaving reddit
20:31:17 <elliott> Phantom_Hoover: Also nothing like a dragon at all which is just amazing.
20:31:25 <elliott> Phantom_Hoover: ahahahaha oh god i just saw his eyes
20:31:29 <elliott> Phantom_Hoover: I thought the eyes were the nostrils
20:31:47 <elliott> 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 <elliott> j-invariant: that's what I know him for :-P
20:33:01 <elliott> 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 <elliott> heh ... just checked hacker news
20:34:08 <elliott> that idiot kroc camen is at #1
20:35:07 <elliott> Phantom_Hoover: this idiot.
20:35:08 <elliott> Cabal-1.10.0.0-8b2e042500a42b47b6b121795bb9262f is unusable due to missing or recursive dependencies:
20:35:09 <elliott> process-1.0.1.4-2a42745dbb9dd3c8087608f127411124
20:44:29 <Phantom_Hoover> elliott, that's quite possibly the least specific identifier EVER.
20:46:03 <elliott> Phantom_Hoover: please please please get Ubuntu working on this.
20:47:20 <Phantom_Hoover> elliott, you betrayed Debian in a Sgeoesque display of infidelity!
20:53:28 <Ilari> Yay, got that AONT code written (uses AES and SHA-256)...
20:53:35 <elliott> Phantom_Hoover: *WORTHY SHUTTLE
20:53:56 <Phantom_Hoover> elliott, YOUR TIME AT HOOVER HEAVY INDUSTRIES IS AT AN END
20:54:04 <elliott> Phantom_Hoover: OK. Can I still steal TNT?
20:54:24 <Phantom_Hoover> elliott, you can't use company TNT unless you concede that Shuttleworth is EVIL.
20:54:45 <elliott> Phantom_Hoover: Of course he is. http://geekz.co.uk/lovesraymond/archive/cancomical-lynchpad
20:55:17 <elliott> Phantom_Hoover: I don't want to join until you read every Everybody Loves Eric Raymond comic ever.
20:55:56 <elliott> I wonder if there will ever be a new one.
20:56:14 <elliott> "December 21, 2012 – A new ELER strip is published.
20:56:14 <elliott> 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 <elliott> I... that... is actually plausible.
20:57:04 <elliott> "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 <elliott> Phantom_Hoover: http://esr.ibiblio.org/?p=2575#comment-279450 "while arguably, I *am* in fact a world-changing figure" --esr
20:59:37 <Phantom_Hoover> The fact that the man is allowed anywhere near a gun is something I will never understand.
21:00:13 <Phantom_Hoover> [[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:46 -!- poiuy_qwert has quit (Quit: This computer has gone to sleep).
21:03:05 <elliott> Phantom_Hoover: http://rationalwiki.org/w/index.php?title=Eric_S._Raymond&diff=707432&oldid=695156
21:03:10 <elliott> Phantom_Hoover: ADD A NEW REVISION ON TOP BEFORE HUMAN REVERTS ME
21:03:39 <elliott> "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:47 <elliott> Phantom_Hoover: AD DA REVISION ADD A REVISION QUIIIICK
21:04:05 <Phantom_Hoover> elliott, http://rationalwiki.org/wiki/Talk:Eric_S._Raymond#Utter_madness
21:04:24 <elliott> j-invariant: it's rationalwiki it can't be right
21:04:51 <Phantom_Hoover> elliott, OTOH, he was saying that "Turing was asking for it", which is appalling beyond words.
21:05:01 <elliott> Phantom_Hoover: Who cares — the article is already crap anyway.
21:05:04 <Phantom_Hoover> [[Um, no. INTERCAL is one of the things that is ESR working in his sphere of powerful competence.]]
21:05:04 <j-invariant> "His highly respectable work and expertise ..." ~~> "His questionable work and expertise in computer technology ..." hahahaha
21:05:19 <elliott> Phantom_Hoover: Add a damned revision to the article already so mine doesn't get reverted.
21:05:24 <elliott> Just tweak the formatting of my edit :P
21:05:49 <elliott> Phantom_Hoover: Also TO BE FAIR he did originally write C-INTERCAL, but the code wasn't very ... good.
21:06:56 <elliott> pikhq: So, is there any actual obstacle to using stow?
21:07:36 <elliott> Phantom_Hoover: Hey, you removed the amusing bit.
21:09:35 <Phantom_Hoover> 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:49 <elliott> Phantom_Hoover: Seen, yes. What of it?
21:10:21 <elliott> Phantom_Hoover: I think it's factually correct (probably), but it doesn't really matter much.
21:10:29 <elliott> Parsing GIFs and PNGs is not some huge innovation.
21:10:49 <elliott> 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 <elliott> 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 <elliott> j-invariant: maybe i'll use my crazy Transaction type in this lang
21:13:56 <Ilari> 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 <Phantom_Hoover> elliott, David Gerard has been... not trolling, but being a pain at Less Wrong.
21:14:51 <Ilari> For extra fun, couple chunks containing random data can be added...
21:14:52 <pikhq> elliott: Uh, other than symlinks sucking, no.
21:15:14 <elliott> pikhq: I wonder how the GNU System guys didn't think of using DESTDIR.
21:15:35 <Phantom_Hoover> elliott, not sure. Look at the RW LW articles: he wrote a great deal of them.
21:16:05 <elliott> Phantom_Hoover: You mean [[Less Wrong]] on RationalWiki?
21:16:07 <Ilari> Basically, that allows making data undecode multiple ways with possibilty of junk that just doesn't undecode.
21:16:24 <elliott> Phantom_Hoover: Scared to do that — Reddit Atheists react explosively when confronted with people who are actually rigorous about it.
21:16:33 <Phantom_Hoover> elliott, he's also part of the Wikipedian Bureaucracy.
21:16:46 -!- Sasha2 has quit (Read error: Connection reset by peer).
21:17:28 -!- Sasha2 has joined.
21:17:44 <elliott> Phantom_Hoover: '"rationalists"'.
21:17:55 <elliott> pikhq: Then ... why is it blocking a release?
21:18:24 <elliott> Phantom_Hoover: Aren't you an admin?
21:18:43 <elliott> 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 <Phantom_Hoover> elliott, at RW? Sure, but the criteria for that are more or less the same as for autoconfirmation.
21:19:13 <pikhq> elliott: A) They don't *want* to use stow. B) stowfs does not work yet.
21:19:17 <elliott> http://rationalwiki.org/w/index.php?title=Special%3AListUsers&username=&group=sysop&limit=50
21:19:20 <elliott> Phantom_Hoover: Dear god how many are there.
21:19:38 <Phantom_Hoover> FWIW, I'm also a bureaucrat for reasons unclear to me.
21:19:43 <elliott> Phantom_Hoover: Do they realise that they have almost as many sysops as Wikipedia?
21:19:51 <pikhq> 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 <elliott> pikhq: From using stow I actually kinda like it...
21:20:14 <Phantom_Hoover> elliott, you fail to understand that a significant driving force behind RW's policy is being the opposite of Conservapedia.
21:20:23 <elliott> Phantom_Hoover: RATIONALWIKI PREDATES CONSERVAPEDIA (iirc)
21:20:35 <pikhq> Yeah, the symlink thing is the only really *bad* thing about stow, and it's not *that* bad...
21:20:46 <elliott> Phantom_Hoover: It doesn't? Well that explains ... a lot.
21:21:13 <elliott> Phantom_Hoover: I guess nobody realised that the opposite of Conservapedia is LiberalUnjustifiedNutjobPedia.
21:21:33 <Phantom_Hoover> elliott, naw, that exists too, it's just *profoundly* unfunny.
21:21:52 <elliott> Phantom_Hoover: It exists and it's called RW. Also isn't that Lumenos' thing?
21:22:10 <Phantom_Hoover> Imagine a female zzo. Then imagine her attempting to be funny.
21:22:11 <elliott> If you say "but RW is humorous", well ... I can't bring myself to take Conservapedia seriously either. :P
21:22:33 <elliott> Phantom_Hoover: "Libertarians aren't keen on illegal immigration, but liberals always sort them out." Err?
21:22:54 <elliott> Phantom_Hoover: It just ... ist hat meant to be funny?
21:23:07 <Phantom_Hoover> elliott, again, it was written by zzo's distaff counterpart.
21:23:21 <elliott> Phantom_Hoover: Too man contractions
21:24:35 <elliott> Phantom_Hoover: I meant in the text.
21:24:44 <elliott> 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 <elliott> 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 <elliott> Phantom_Hoover: tl;dr "Reading is hard"?
21:25:28 <Phantom_Hoover> elliott, well, saying "read this hefty tome" in an argument isn't a very good idea.
21:26:08 <elliott> 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 <elliott> Phantom_Hoover: As bad as RationalWiki is the Richard Dawkins forum is worse. :p
21:26:54 <Phantom_Hoover> elliott, of course. RW is at least /ostensibly/ without any opinion on religion.
21:27:32 <elliott> 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 <elliott> Phantom_Hoover: Disturbingly that seems to be the real world.
21:28:38 <Phantom_Hoover> elliott, well, there are quite a few theists, and they get along fairly well.
21:28:47 <elliott> Phantom_Hoover: O god, the RW article mentions the Amanda Knox case.
21:29:21 <elliott> Murder of Meredith Ketcher.
21:29:34 <elliott> 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 <elliott> 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:18 <elliott> (And by that I mean the whole world.)
21:30:48 <Phantom_Hoover> elliott, trusting the prevailing scientific theories is just the only way to get by in the world.
21:30:55 <elliott> Phantom_Hoover: Certainly.
21:31:01 <elliott> Phantom_Hoover: But it doesn't mean you should generalise that to "trust authority".
21:31:34 <elliott> 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 <Phantom_Hoover> elliott, particularly odd, given that Dawkins himself is no fan of the legal system.
21:32:34 <elliott> Phantom_Hoover: I love Dawkins. It's his fans I'm not too keen on.
21:34:16 <elliott> 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:42:38 <elliott> Phantom_Hoover: The LW-consensus is that an aversion to giving numeric probabilities is basically an artefact of human wetware.
21:43:09 <Phantom_Hoover> elliott, but... I mean, do they have calculations for it or what?
21:43:19 <elliott> Phantom_Hoover: "Your probability *estimate*".
21:43:46 <elliott> 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:46:07 <Ilari> Hmm... Returning to that fan problem... At least CPU fan and main case fan both work...
21:46:37 <Ilari> (dunno about PSU fan)
21:46:41 <Phantom_Hoover> elliott, incidentally, Ilari is now your subordinate at HHI.
21:46:52 <Ilari> Also, GPU fan appears to work...
21:46:56 <elliott> Ilari: Do whatever. The paychecks will come at regular intervals.
21:47:05 <elliott> Phantom_Hoover: Is it bad to try and establish a utopia of laziness with my position?
21:47:17 <elliott> Ilari: Hoover Heavy Industries, the most fake corporation of fakeness.
21:47:32 <Phantom_Hoover> elliott, I'm still not sure what kind of entity it is.
21:47:46 <elliott> Phantom_Hoover: It's a militacountrypany!
21:48:36 <elliott> 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 <elliott> Phantom_Hoover: EVE is just so boring and hard to get into.
21:49:01 <elliott> Phantom_Hoover: Even then what.
21:49:12 <Phantom_Hoover> Even in a world of Platonically ideal computers, Braben would sue the hell out of the people running the MMO.
21:49:46 <elliott> Phantom_Hoover: Even if the ship names were changed? Presumably it'd take place in a new world anyway.
21:49:55 <elliott> Phantom_Hoover: You can't copyright gameplay itself.
21:50:07 <elliott> Change the names, make new designs, redo the UI.
21:50:09 <Phantom_Hoover> elliott, by this point you can always just look at Infinity and sigh.
21:50:20 <elliott> Phantom_Hoover: Who cares about landing on planets.
21:50:34 <Phantom_Hoover> elliott, there is actually an OXP that lets you do that...
21:52:06 <Phantom_Hoover> Although it basically just consists of flying into the planet and getting a docking effect.
21:53:52 <elliott> [[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 <elliott> :That's the right conservative attitude. --Idiot numbre 188 (talk) 16:26, 30 December 2010 (UTC)]]
21:53:56 <elliott> I should stop reading RW, it's bad for me.
21:54:01 <elliott> I even /like/ Vector but COME ON.
21:55:42 <elliott> 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 <Phantom_Hoover> It is well-documented that the text is far far far smaller than Monobook's on many computers.
21:56:19 <elliott> 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 <elliott> 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:45 <elliott> Phantom_Hoover: s/computers/browsers/. Probably.
21:58:08 <elliott> Oh god I forgot how amazing http://www.youtube.com/watch?v=ZW2qxFkcLM0 is.
21:58:11 <Phantom_Hoover> Admittedly, Vector has a smaller font size anyway, but it was more pronounced.
21:59:25 <elliott> j-invariant: lol at the trailer? or
21:59:35 <elliott> i would so have gone and seen it
21:59:56 <elliott> j-invariant: it's the trailer to "2012", recut with bongos
22:02:49 <variable> 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 <variable> the flaw has nothing to do whether someone or something is or isn't in a group :-\
22:03:26 <elliott> [[ 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:04:36 <elliott> Phantom_Hoover: He did indeed.
22:04:54 <elliott> 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:05:02 <variable> 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 <elliott> Phantom_Hoover: Do you remember when almost all the examples of forms of argumentation on Wikipedia were between Father and (precocious) Daughter?
22:05:31 <elliott> Phantom_Hoover: It was amazing.
22:05:57 <variable> elliott, one thing I'm *really* good at is logic :-}
22:06:00 <elliott> 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:07:10 <elliott> j-invariant: I wonder whether I should do this with she.
22:07:43 <j-invariant> {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes, TypeFamilies, FlexibleContexts, NoMonomorphismRestriction #-}
22:07:50 <elliott> j-invariant: I call that "Tuesday"
22:08:50 * elliott edits keyboard layout, changes £ to #
22:08:55 <elliott> nobody talks about money and I need my hash
22:09:18 <variable> elliott, have you ever actually seen NTS used correctly?
22:09:24 <elliott> variable: not that I know of
22:09:31 <elliott> it appears to be a vanishingly rare fallacy in practice.
22:09:46 <elliott> mostly because there are easier-to-make, more convincing ones.
22:10:17 <elliott> "To open kluchrtoxml, you need to install Rosetta. Would you like to install it now?"
22:10:34 <variable> stupid VLC and mplayer can't play my DVD
22:10:58 <elliott> mplayer plays everything, you did something wrong
22:11:24 <variable> elliott, it should be mplayer dvd:// -dvd-device /dev/acd0
22:14:48 <elliott> j-invariant: I wish Type:Type was consistent
22:14:48 <j-invariant> data (:/:) (r :: *) :: {Poly r} -> * where Q :: r -> r :/: p
22:15:01 <elliott> j-invariant: Indeed, I doubt it can :P
22:15:05 <elliott> It's not a full language, man!
22:15:23 <elliott> j-invariant: That's cool though.
22:15:26 <elliott> But I doubt it's possible :P
22:16:41 <elliott> 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 <variable> how does urxvt NOT have unicode support....
22:23:20 <elliott> j-invariant: :( she can't have types which are dependent on themselves
22:23:27 <elliott> j-invariant: i.e. a constructor of type T takes a dependent T
22:24:15 <variable> elliott, any unicode character shows up as ?
22:24:23 <elliott> variable: you set encodings wrong
22:24:55 <elliott> j-invariant: hm i think i did it wrong
22:25:03 <elliott> Sigma :: {a:Type} -> Term {Pi (TypeI Z) (TypeI Z)} -> Type
22:25:11 <elliott> the output for that tries to use : as a type operator and stuff so no it's not that
22:25:38 <Phantom_Hoover> elliott, which language are you guys messing around with this time?
22:26:11 <elliott> Phantom_Hoover: Haskell+she
22:26:43 <Vorpal> elliott, what does this "she" do?
22:26:51 <elliott> Vorpal: she does many things.
22:26:55 <variable> elliott, any ideas for what to look for?
22:26:58 <Vorpal> elliott, that's what SHE said!
22:27:06 <elliott> pseudo-dependent types, Pi, pattern synonyms, pseudo-aspect-oriented programming, and IDIOM BRAKKETZ
22:27:15 <elliott> variable: what program is outputting them?
22:27:52 <Vorpal> that outputs the relevant variables
22:28:00 <variable> elliott, when I attempt to copy from xchat to the shell (so I guess its zsh)
22:28:01 <Vorpal> and also shows which is in effect for those not set
22:28:18 <Vorpal> variable, then there is LANG, LC_CTYPE and so on.
22:28:24 <elliott> yeah you need to set them to en_foo.UTF8
22:28:27 <Vorpal> variable, well of course unicode doesn't work then
22:28:38 <variable> Vorpal, I'm new to unicode in the terminall....
22:28:58 <variable> I should set them to en_US.UTF8 ?
22:29:11 <Vorpal> variable, set LANG=en_US.UTF-8
22:29:27 <Vorpal> then all the unset ones default to LANG
22:29:32 <Vorpal> so you only need to set LANG
22:29:39 <Vorpal> (and LC_ALL overrides all on top of that)
22:29:51 <variable> urxvt: default locale unavailable, check LC_* and LANG variables. Continuing.
22:30:23 <variable> export LANG="en_US.UTF8"; urxvt
22:30:34 <Vorpal> btw, you might want to change LC_COLLATE to C again. since the non-C locales often sorts case insensitively.
22:30:56 <Vorpal> or another alternative: maybe the locale was not generated
22:31:02 <Vorpal> I think how varies between distros
22:32:52 <elliott> data Term :: {Nat} -> {Type} -> * where
22:32:52 <elliott> Star :: {n} -> Term l {TypeI (S n)}
22:32:52 <elliott> Var :: Fin {n} -> Term {n} ???
22:33:03 <elliott> j-invariant: am i going to have to carry around the whole environment of types or something? :
22:34:54 <elliott> j-invariant: in the /type system/?
22:34:58 <elliott> j-invariant: I'm not Oleg!
22:35:23 <elliott> The requested URL /~conor/pub/she/examples/ShePrelude.lhs was not found on this server.
22:35:23 <elliott> 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 <variable> 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 <elliott> variable: We have that, it's called C++.
22:42:03 <Vorpal> elliott, isn't haskell faster than C++ at least?
22:42:15 <variable> basically - make the language itself require algorithms that are Θ(2^n)
22:42:43 <Vorpal> variable, why not O(n!)
22:42:45 <elliott> Vorpal: Well. We're working on that.
22:43:12 <elliott> 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:20 <elliott> variable: just store programs as SHA-512 hashes of an actual program
22:43:25 <elliott> compilation takes place by brute-forcing the actual program
22:43:44 <Vorpal> <elliott> variable: just store programs as SHA-512 hashes of an actual program <-- didn't gregor do this already?
22:44:06 <elliott> I think there is such a language on the wiki.
22:44:16 <variable> elliott, no because that is not deterministic
22:44:36 <variable> and I don't just want O(n!) I want Θ(n!)
22:44:39 <elliott> variable: yes it is deterministic
22:44:51 <elliott> there are hash collisions, but who cares :)
22:44:56 <variable> elliott, no - because there could be multiple programs that result in the same sha hash
22:45:00 <elliott> variable: specify the order in which strings are brute-forced duh
22:45:10 <Vorpal> if it fails to compile, just search for a collision
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 <variable> elliott, but then its not turing complete - not all programs could be represented
22:45:57 <Vorpal> until you manage to find a program that compiles
22:45:57 <elliott> 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:10 <Vorpal> elliott, well that works if every possible string is a valid program
22:46:10 <elliott> Vorpal: No, you just completely skip the non-compiling ones.
22:46:10 <elliott> 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 <elliott> 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 <elliott> The hashes are just a facade over that.
22:47:08 -!- pikhq has quit (Excess Flood).
22:47:09 <Vorpal> 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 <elliott> Vorpal: You could finetune a hash function for it.
22:47:11 -!- pikhq has joined.
22:47:11 <elliott> Vorpal: But that isn't true.
22:47:12 <elliott> Vorpal: Consider outputs bigger than the hash size.
22:47:22 <variable> j-invariant, Φ = lower bound O = upper bound Θ is when O == Φ IIRC
22:47:22 <Vorpal> elliott, well, there are infinitely many strings that result in the same hash
22:47:22 <elliott> Vorpal: Specifically, uncompressable outputs bigger than the hash size.
22:47:29 -!- coppro has joined.
22:47:29 -!- dbc has joined.
22:47:37 <elliott> Vorpal: The pigeonholes are very crowded.
22:47:49 <elliott> variable: did j-invariant ask?
22:47:49 -!- pikhq has quit (Excess Flood).
22:47:49 <variable> elliott, meh - I want to invent the language myself
22:48:05 <variable> elliott, I thought he did when he said <j-invariant> hm
22:48:10 <Vorpal> 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 <Vorpal> if that would happen, then it wouldn't be a good hash function
22:49:00 <variable> elliott, am I right? I always forget the lowerbound symbol - the rest I know are correct
22:49:12 <Vorpal> 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:21 <elliott> Vorpal: Let's just say yes and not think about it!
22:49:34 <Vorpal> elliott, do you think I'm not right?
22:49:35 <elliott> Var :: {Fin n} -> Term {t:ts} t
22:49:37 <elliott> j-invariant: can't believe that actually works
22:49:51 <variable> elliott ah I have another idea for a language
22:50:00 <Vorpal> elliott, well, who would be the expert on this?
22:50:06 <elliott> Vorpal: Your mo^W^Wsomeone.
22:50:16 <elliott> Vorpal: It sounds like something very hard to prove.
22:50:19 <elliott> For a given hash function.
22:50:27 <Vorpal> elliott, for any /real/ hash function yes
22:50:33 <variable> 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 <Vorpal> elliott, but for a theoretical perfect one
22:50:49 <elliott> variable: Reminds me of Clue.
22:51:00 <elliott> Vorpal: Well, let's consider the hash function : String -> 1.
22:51:15 <elliott> Vorpal: There is only one such function, f(s) = ().
22:51:32 <elliott> Vorpal: Every program has the hash (), and the hash () has every program.
22:51:38 <elliott> Vorpal: What is your hypothesis again?
22:52:04 <elliott> j-invariant: what do you think of HOAS?
22:52:46 <Vorpal> 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 <Vorpal> (or at least output, I don't think input matters)
22:53:16 <elliott> f : String -> 2; f('x':...) = A; f(s) = B
22:53:22 <Vorpal> elliott, what language is this
22:53:24 <elliott> i.e. x followed by anything is A, everything else is B.
22:53:36 <elliott> Vorpal: Now consider a language where no valid program starts with x.
22:53:43 <elliott> All programs hash to B; A has no program.
22:53:53 <elliott> Vorpal: Of course this is pathological ... but it demonstrates that it is not universally true.
22:54:04 <elliott> Vorpal: I think the problem is that while hash functions "appear" random they are not _actually_ perfectly uniform.
22:54:18 <Vorpal> elliott, that is not a good hash in the way I said above though.
22:54:24 <j-invariant> elliott: it's just completely impossible to use for anything nontrivial
22:54:26 <Vorpal> elliott: <Vorpal> 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 <elliott> Vorpal: I don't think a good hash in that sense exists then.
22:54:39 <Vorpal> elliott, true, I suppose even sha512 has some bias
22:54:53 <Vorpal> 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 <elliott> Vorpal: Close doesn't make a theorem. Infinity is against you; close times infinity equals infinitely far. :p
22:55:36 <j-invariant> elliott: obvious being able to write syntax using lambda terms is nice, but using it internally for algorithms doesn't seem possible
22:55:45 <variable> Vorpal, good hash functions are not defined by looking random
22:55:58 <elliott> j-invariant: is there any way out of an infinite hierarchy of Type-s again?
22:56:02 <variable> good hash functions are defined by small changes in the source result in large changes in the output
22:56:03 <elliott> or is it all just machinery to hide it
22:56:10 <elliott> variable: yes. we are aware
22:56:17 <elliott> he was defining his own notion
22:57:04 <Vorpal> 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:58:04 <variable> Vorpal, actually my definition isn't complete
22:58:04 <Vorpal> 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 <variable> because then theoretically multiplying all the bytes together should be a "good" hash function
22:58:22 <elliott> Vorpal: is an unbiased function even theoretically possible?
22:58:28 <elliott> I'm not sure such a functoin would be computable
22:58:46 <Vorpal> elliott, define theoretically.
22:58:55 -!- jix has joined.
22:59:41 <elliott> Vorpal: Is there a computable unbiased hash function?
22:59:43 <Vorpal> elliott, you can discuss things using an oracle in articles. They are presumably not possible for an UTM.
23:00:02 <Vorpal> elliott, I don't know if it has been proven if one could exist or not
23:00:10 <Vorpal> elliott, I'm pretty sure none is known though.
23:00:26 <elliott> data Term :: {[Type]} -> {Type n} -> * where
23:00:26 <elliott> Star :: {n} -> Term {ts} {TypeI (S n)}
23:00:26 <elliott> Var :: {Fin n} -> Term {t:ts} {t}
23:00:28 <elliott> Fun :: {t} -> Term {t:ts} {s} -> Term {ts} {Pi t s}
23:00:30 <elliott> App :: Term {ts} {Pi t s} -> Term {ts} {t} -> Term {ts} {s}
23:00:35 <elliott> j-invariant: what's the hot way of describing data structures nowadays
23:00:40 <elliott> W fell out of favour I know that :)
23:01:33 <Vorpal> elliott, yes not very googable
23:01:52 <Vorpal> elliott, even with the dot
23:01:55 <elliott> 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 <elliott> Vorpal: Just skip straight to the obituary.
23:02:59 <elliott> "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 <Gregor> Vorpal, elliott: HASHFUCK IS PATENTED
23:03:05 <elliott> but i think that might be overblown for what i want
23:03:19 <elliott> Gregor: YOUR MOERMYORI TJOP FDJ ODGPDNG IODFJG IODJG IODFJG KOFDJGOIFDJH0DZJSVOI HIOSI ]EWSE0R 9J90E4JYS0SJ TAWR -K5 -K[RS';T/XHC;LGKO[N]PLJK
23:03:33 <elliott> Vorpal: you read the whole post and understood it in that time?
23:03:42 <Vorpal> elliott, I never claimed I did
23:03:59 <elliott> 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:57 -!- Phantom_Hoover has joined.
23:06:58 <elliott> j-invariant: as in, two individual ones
23:07:05 <elliott> rather than just reducing Terms down to more value-y terms
23:08:57 <j-invariant> I have Maybe all over the place because I can't parametrize haskell modules by values
23:09:08 <j-invariant> but it's not clear whether they get turned to Just's in time
23:09:19 <Vorpal> 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 <elliott> data Term :: {[forall n. Type n]} -> {Type n} -> * where
23:09:21 <elliott> TermWrap :: Thing Term {ts} {s} -> Term {ts} {s}
23:09:21 <elliott> App :: me {ts} {Pi t s} -> me {ts} {t} -> Term {ts} {s}
23:09:22 <elliott> instance Thingy Term where wrap = TermWrap
23:09:45 <elliott> Vorpal: well there's more important stuff near the bottom where he demonstrates theoretical problems too.
23:09:53 <elliott> 23:08 j-invariant: I have Maybe all over the place because I can't parametrize haskell modules by values
23:09:57 <elliott> j-invariant: this is why we need an ML-style module system!
23:10:10 <j-invariant> I don't know much about module systems really
23:10:21 <Vorpal> elliott, the bit about canonical representation?
23:10:21 <j-invariant> I want a language expressive enough to define them in
23:10:28 <elliott> Vorpal: the bit about tt = ff.
23:11:29 <Sgeo> elliott, should I learn OCaml?
23:11:32 <Sgeo> I think I tried once
23:11:41 <Vorpal> elliott, ah... it is inconsistent, right?
23:11:43 <elliott> Sgeo: Learn Standard ML instead. Probably.
23:11:47 <elliott> Vorpal: It's more subtle than that :-P
23:12:24 <elliott> j-invariant: so what's your favourite way of defining recursive types in the value language!
23:12:26 <Sgeo> 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:39 <elliott> Sgeo: the ML module system is nothing like what you think it is.
23:12:49 <elliott> j-invariant: i.e. combinators resulting in Types.
23:15:01 <elliott> j-invariant: can you look at what i have so far? http://sprunge.us/UiXi
23:15:07 <elliott> j-invariant: specifically the XXX: comments ... I'm a bit confused
23:15:18 <elliott> erm that App signature at the bottom is all wrong
23:15:20 <elliott> it hosuld say Term, not me
23:15:47 <Sgeo> elliott, any reasons for Standard ML over OCaml?
23:15:57 <elliott> Sgeo: ocaml sucks. sml sucks less.
23:16:24 <elliott> j-invariant: but agda is 'orrible
23:16:55 <elliott> j-invariant: LET ME LIVE IN MY ILLUSION
23:17:20 <j-invariant> you can't really use lists for a context of types
23:17:25 <elliott> Not in scope: type constructor or class `SheTyType'
23:17:29 <j-invariant> since later types might depend on the earlier ones..
23:17:43 <elliott> j-invariant: oh god you're right
23:17:46 <elliott> j-invariant: asdfghj that is awful
23:17:59 <elliott> is that something that exists
23:18:31 <Vorpal> elliott, what are you trying to do?
23:18:53 <Vorpal> elliott, okay, if you don't want to tell...
23:19:13 <elliott> Vorpal: i explained above.
23:19:36 <Vorpal> elliott, approx where?
23:20:07 <Vorpal> elliott, that you are writing (or do you mean what she is?)
23:21:04 <Vorpal> elliott, haskell should add such an extension already
23:21:30 <elliott> Vorpal: um that would require a complete restructuring of GHC
23:21:38 <elliott> and would be difficult to integrate with large swathes of haskell
23:22:36 <elliott> Ambiguous type variable `thing' in the constraint:
23:22:46 <elliott> j-invariant: apparently "thing" is ambiguous, who knew?
23:22:54 <Vorpal> elliott, what good general purpose dependently typed languages are there?
23:23:23 <Vorpal> elliott, which isn't usable yet iirc
23:23:34 <Vorpal> none that is usable as of today?
23:23:38 <Vorpal> elliott, well, that depends
23:25:04 <Vorpal> 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 <elliott> 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 <Vorpal> elliott, dude you just highlighted him
23:26:35 -!- MigoMipo_ has quit (Read error: Connection reset by peer).
23:27:09 <Vorpal> elliott, so this Cola, was it any good?
23:27:21 <elliott> Vorpal: It's a VPRI project. It's pretty coo'.
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:55 <Vorpal> elliott, maybe I should try to learn Epigram?
23:28:55 <Vorpal> j-invariant, which ones? epigram?
23:28:55 <Vorpal> j-invariant, would you call haskell general purpose?
23:29:06 <elliott> j-invariant: Epigram is close enough :P
23:29:11 <Vorpal> j-invariant, in what way is epigram not general purpose then?
23:29:16 <elliott> Vorpal: You can't learn Epigram 2 because nothing actually runs Epigram 2.
23:29:39 <elliott> 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 <j-invariant> elliott: *Polynomial> let w = (one - Quot (mon 1, Just eisenstein))*(one + Quot (mon 1, Just eisenstein))
23:30:42 <Vorpal> elliott, right. Is it moving forward fast or?
23:30:42 <j-invariant> *Polynomial> printPolynomial names ((inj w * x + y)^7)
23:30:42 <j-invariant> "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 <elliott> 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 <elliott> j-invariant: did you write this?!?!
23:31:06 <elliott> Vorpal: *system on a regular basis,
23:31:56 <j-invariant> :: (SheChecks Nat n, Ring r, Eq r, Show r) =>
23:31:56 <j-invariant> Vec n String -> MonoidRing r (Vec n Integer) -> String
23:34:10 <elliott> j-invariant: i approve. i approve very hard
23:34:42 <elliott> j-invariant: so do quotient sets work yet >:)
23:37:41 <elliott> /Users/ehird/Code/tabby/first.hs:52:26:
23:37:41 <elliott> Could not deduce (Show (me (t1 :$#$#$#: ts) s))
23:37:42 <elliott> from the context (t ~ SheTyPi t1 s)
23:37:43 <elliott> arising from a use of `show'
23:37:45 <elliott> at /Users/ehird/Code/tabby/first.hs:52:26-31
23:37:49 <elliott> add (Show (me (t1 :$#$#$#: ts) s)) to the context of
23:38:40 <j-invariant> "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 <elliott> j-invariant: already have yo
23:39:00 <elliott> i think i see the problem though MAYBE
23:39:10 <elliott> flexible contexts -- ALWAYS A MISTAKE ???
23:39:44 <elliott> j-invariant: any reason for quoting that? :p
23:42:03 <j-invariant> "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 <j-invariant> 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:14 <elliott> j-invariant: where's that from btw
23:46:24 <elliott> Phantom_Hoover: http://i.imgur.com/1LCv6.png I think dome3 is smaller than the Cube.
23:46:37 <elliott> Phantom_Hoover: Note how they have tons of people working on it and even they haven't gone for bedrock.
23:48:40 <elliott> Vorpal: see image. on the reddit creative server.
23:48:56 <Vorpal> elliott, I see the image. But what is it supposed to be?
23:50:06 <elliott> Phantom_Hoover: /warp dome3.
23:50:11 <elliott> Phantom_Hoover: Try not to crash the server.
23:50:55 <elliott> Phantom_Hoover: I'M ON TO YOU
23:51:19 <elliott> j-invariant: to type things
23:51:59 <Vorpal> j-invariant, it is useless when he is in this mood
23:52:31 <elliott> Vorpal: actually i was joking along with j-invariant.
23:52:38 <elliott> p. sure j-invariant knows what haskell types are
23:52:49 <elliott> j-invariant: TYPES IN HASKELL ARE LIKE BURRITOS TO YOUR MONADS
23:55:28 -!- elliott has quit (Remote host closed the connection).
23:56:05 -!- elliott has joined.
23:56:47 <Sgeo> If I became obsessed with Haskell, would shutup be configured to yell at me for mentioning Haskell?
23:57:26 <elliott> Sgeo: Only if you say stupid things.
23:57:38 <elliott> Phantom_Hoover: Yes. Yet it is, afaik, smaller than the Cube and also more shallow.
23:57:45 <elliott> Phantom_Hoover: How the fuck is the Cube ever going to get completed?
23:57:49 <elliott> j-invariant: is that polynomial thing up anywhere?
23:57:54 -!- j-invariant has quit (Quit: leaving).
23:57:55 <Sgeo> I'd help if I could
23:58:10 <Phantom_Hoover> elliott, it will get completed because we are HHI and we do not have restrictions on TNT.
23:58:20 <elliott> Phantom_Hoover: Do we have the TNT kit yet?
23:58:33 -!- j-invariant has joined.
23:58:40 <elliott> j-invariant: is the polynomial source open?
23:58:45 <Vorpal> elliott, you have a script to tell him to shut up?
23:58:48 <Vorpal> elliott, why not just ignore
23:59:18 <Sgeo> 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 <Sgeo> Used to say it in the channel, but oerjan got ticked off
23:59:48 <elliott> I am excellent at obeying the letter but not the spirit of any judgement.
23:59:49 <Vorpal> Sgeo, just filter such /msg from elliott!
23:59:56 <elliott> Vorpal: It doesn't come from me.