00:05:48 `quote goodnight 00:05:53 No output. 00:05:56 -!- Taneb has quit (Quit: Leaving). 00:10:43 There's a YouTube page of the music from Orisinal games 00:10:45 :D:D:D 00:10:52 http://www.youtube.com/user/orisinalmusic 00:10:58 wow, that sounds obscure 00:11:17 Fiora: imo finland is a p.nice place 00:11:28 Er, fizzie. 00:11:52 Fiora: Channel law is that you have to change your nick to a unique two-letter prefix now. 00:11:56 FireFly, too. 00:12:04 we've tried that 00:12:10 they won't budge 00:12:18 Bike, orisinal.com 00:12:19 now 00:12:20 i'm sorry, FireFly cannot change, it might cause innocents to be swatted. 00:12:38 Hmm. 00:12:42 Wasn't fizzie here first? 00:12:47 now what 00:12:48 noooooooo 00:12:51 probably. 00:12:52 I wanna keep my name 00:12:53 i'm not the only no* :/ 00:12:56 Sgeo, wait er weren't those stock pieces 00:12:58 how awful 00:12:58 Froia 00:13:13 0xF107A 00:13:15 This isn't a game Sgeo. This is a bunch of games. 00:13:16 sunny day sky, for sure 00:14:04 Phantom_Hoover, well, I didn't know where they came from. Just that one of them sounded like Pachelbel or whatever 00:14:17 be fair, everything sounds like pachelbel 00:14:25 Bike, have you seen the paravonian video 00:14:32 I have seen no videos. 00:17:49 imo oerjan should change his name to make room for all the other øccupants of that prefix 00:19:50 Bike, did I say it was a game? 00:20:20 no, but i felt the need to clarify that it wasn't a game 00:20:21 which it isn't. 00:21:19 -!- oerjan has quit (Quit: ZZZZ). 00:23:03 (paravonian video is here btw: http://www.youtube.com/watch?v=JdxkVQy7QLM) 00:27:26 Willy G. van Hoorn 00:27:38 is that Taneb's evil twin? 00:27:41 Oh, Taneb's not here. 00:39:54 -!- Phantom_Hoover has quit (Remote host closed the connection). 00:54:28 -!- wareya has joined. 00:57:46 -!- wareya_ has quit (Read error: Operation timed out). 01:03:32 Ooh, I got welcomed. Wow. 01:03:56 `relcome jiella 01:03:59 ​jiella: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 01:05:26 Is there any kind of rhyme or reason to that coloring 01:05:29 `welcome Sgeo 01:05:31 Sgeo: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 01:05:31 `welcome Sgeo 01:05:34 Sgeo: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 01:05:34 oops 01:05:37 `relcome Sgeo 01:05:40 ​Sgeo: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 01:05:45 `relcome Sgeo 01:05:47 ​Sgeo: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 01:06:21 wouldn't it be more instructive to check the source, rather than reverse engineering the amazingly complicated color mechanism 01:12:39 I just wanted to know if it was random 01:13:12 !url 01:13:39 `url 01:13:41 http://codu.org/projects/hackbot/fshg/ 01:28:56 http://docopt.org/ can't decide if this is too cute or not 01:29:47 http://tvtropes.org/pmwiki/pmwiki.php/VideoGame/Orisinal 01:29:52 is it a joke? 01:38:26 kmc: the problem i see is that it makes you type things in a more human-consumable but timewasty format 01:38:39 when that kind of stuff could be generated from a more succint, less "faithful" DSL 01:39:24 shrug 01:39:29 i don't think it wastes much time to type that text 01:39:43 and it makes the options very clear because it's already in a format you can read 01:39:51 ... assuming the library interprets everything the same way 01:39:54 which is the trick 01:48:51 -!- sirdancealo2 has quit (Read error: Operation timed out). 01:50:35 Yikes. 01:51:10 I think this is getting to be a bit too much. 01:51:17 -!- jiella has quit (Quit: Leaving.). 01:56:04 couldn't handle the welcomes 02:04:36 -!- nooodl_ has changed nick to nooodl. 02:06:41 -!- sirdancealo2 has joined. 02:39:11 -!- DHeadshot has joined. 02:40:30 ^list 02:40:30 Taneb atriq Ngevd Fiora nortti Sgeo ThatOtherPerson alot 02:41:23 Sgeo: new album! 02:41:51 coppro, yes, we knew yesterday 02:42:07 I believe I did a ^list for the new album 02:42:08 :p 02:42:55 also this update... 02:44:28 the new album is wonderful 02:44:44 it is 02:55:29 the pocketed planets match up with the Felt who were dead when MC arrived 02:56:51 yep 03:09:51 -!- azaq23 has joined. 03:13:20 Fiora: I think Genesis Frog is still best though 03:13:34 (even though I've been waiting on Eternity Served Cold since the flash) 03:14:39 Credits page still not updated 03:14:42 I love The Lordling, actually 03:14:49 I wonder what flash or whatever that's from (or is it?) 03:15:01 [S] Caliborn: Enter 03:15:23 I thought that was Eternity Served Cold 03:15:23 Eternity Served Cold == Eternity's Shylock 03:15:59 oh. The Lordling has not 03:16:08 Sgeo: Eternity Served Cold is longer 03:16:46 something about the lordling reminds me of Disgaea (I wonder if the feel is intentional?) 03:17:01 [S] Jane: Enter is still considered to have A Taste of Adventure 03:17:12 People complained about the name Eternity's Shylock 03:17:27 yeah, a few people mentioned it wasn't a great name so they changed it 03:17:31 since it didn't make much sense to begin with 03:17:37 I liked it 03:18:14 how is a shylock a thing you have 03:19:00 how isn't it 03:19:01 my favorite is still Cascade, I think though 03:19:07 Slavery is fun! 03:20:00 cascade is pretty damn epic 03:20:04 http://theophany-rmx.bandcamp.com/album/times-end-majoras-mask-remixed 03:20:16 Black Hole Green Sun is my favourite part 03:20:28 though Saviour is very very close 03:20:31 me too, I think 03:20:43 Savior of the Dreaming Dead is pretty great too 03:20:52 oh i should listen to the majora's mask thing again 03:21:32 the sweeping violins take it though 03:22:47 Black Hole Green Sun is something I hum to myself when I'm doing something (e.g. transportation) to meet up with someone 03:57:58 -!- sirdancealo2 has quit (Ping timeout: 252 seconds). 03:58:20 The sound of the Atari TIA is limited to 5-bit period although you can set an additional divider, either 2, 6, 31, or 93, so I suppose you cannot make 12-TET music, but you could use its own scale to make up a different kind of music, perhaps. 04:04:02 Fiora: actually scratch that 04:04:12 my favourite is Buy NAK Sell DOOF 04:05:58 -!- nooodl has quit (Ping timeout: 245 seconds). 04:06:00 wooow. that's a really good song, I hadn't even heard it 04:06:56 -!- copumpkin has quit (Ping timeout: 252 seconds). 04:07:19 you haven't listened to Genesis Frog? 04:07:21 highly recommended 04:07:25 -!- copumpkin has joined. 04:07:56 I guess I did 04:09:33 -!- Arc_Koen has quit (Quit: Arc_Koen). 04:13:52 -!- sirdancealo2 has joined. 04:15:28 I haven't listened to Genesis Frog 04:18:39 do it now 04:19:24 I should be eating. 04:19:43 you can do that while listening to genesis frog, protip 04:52:26 -!- monqy has joined. 05:04:38 -!- carado has quit (Ping timeout: 256 seconds). 05:37:57 I wonder what kind of scales could be played on the Atari TIA? 05:39:52 -!- Jafet has quit (Quit: Leaving.). 05:42:06 I think it is called undertone series. 05:46:10 -!- Sgeo has quit (Ping timeout: 258 seconds). 05:46:52 -!- Sgeo has joined. 06:20:35 -!- copumpkin has quit (Ping timeout: 252 seconds). 06:21:14 -!- copumpkin has joined. 06:34:43 ^save 06:34:43 OK. 06:41:50 -!- Sgeo has quit (Read error: Connection reset by peer). 06:42:17 -!- Sgeo has joined. 07:04:50 It's tempting to state that with normal non-cloud-based software, you'll never have the situation of an external entity ceasing to support it, but even with an OSS project, if the community dwindles too much such that the project is no longer developed, it may be difficult to keep using that software in the future, as security holes go unfixed, and newer OSes fail to support older binary 07:04:57 binaries 07:06:05 hello 07:06:09 hi 07:06:21 http://www.fsf.org/blogs/sysadmin/google-backslides-on-federated-instant-messaging-on-purpose :( 07:06:33 hello 07:11:04 The XMPP thing is unrelated to my comment before, which was about Google Reader 07:13:12 ok 07:14:13 Still, with non-cloud-based open-source software, there is a much better possibility to continue to support it, than with proprietary and/or cloud-based software. With open source, like any software, it is possible to be abandoned, but it can be continued working on later by someone else if they are interested in it. 07:17:46 yes 07:47:48 @ask taneb are you a tactical amulet non-extraction bot 07:47:48 Consider it noted. 07:47:52 @ask ngevd which name do you use these days 07:47:54 Consider it noted. 07:48:06 http://24.media.tumblr.com/b10f1779aa67289af9f2af56c964516d/tumblr_mjqtdtBWVl1r4xqamo1_500.jpg 07:49:46 is that a picture of Bike 07:49:53 I play the game "StarTrek Guess" on X-BIT BBS. It is usually easy by guessing the word due to context, due to knowing some things about Star Trek, and because all the puzzles are given in alphabetical order. 07:50:27 Yes. 07:50:39 If it ends with "-_" then I will try Q, for example. 07:51:23 Would that be your choice? 07:51:31 yes 07:51:44 though probably I would guess Q for other reasons 07:52:00 zzo38: http://www.youtube.com/watch?v=k5tyMXXDPX4 07:52:23 i remember watching that tas. it's a good tas. 07:52:36 which one is it i cant really open links 07:52:39 im "Gonig to Sleep" 07:52:44 family feud glitchfest 07:52:53 ahhhh thato ne 07:52:54 i liket hat one 07:53:00 whys my space doing this today 07:53:02 is it the new keyboard 07:53:25 It is like hangman or Wheel of Fortune, where you have the template with _ in place of the letters. So if it end by "-_" then I will probably try Q as my first guess. If it starts with "_ " and the recent ones were "I ", then I will try I since the puzzles are in alphabetical order. 07:53:47 I don't know why they are in alphabetical order, but after playing this game a few times I realized that it is, for some reason. 07:57:39 Another way to score would be to have the way to bet on a position(s) having a letter, and if it does, you earn bonus points. 08:02:39 -!- epicmonkey has joined. 08:06:18 Can anyone answer my question about the bijective function types having to do with the logic with numbers? 08:12:13 What is the Curry-Howard of quantum logic? 08:17:19 -!- Phantom_Hoover has joined. 08:17:53 -!- Bike has quit (Ping timeout: 246 seconds). 09:56:53 -!- Phantom_Hoover has quit (Remote host closed the connection). 10:04:10 What is it called, when, if A is less than or equal to B then you can always subtract A from B, although there might be more than one way to do so, and it might be possible to subtract even if A is not less than or equal to B? 10:08:03 I didn't see your question about bijective function types having to do with the logic with numbers. 10:11:24 shachaf: Maybe I forgot to write it? Nevertheless I can repeat. 10:12:02 If you are making logic with numbers, can the type system corresponding include the type of bijective functions between finite types? 10:17:14 shachaf: Now do you know? 10:17:21 No. 10:17:36 I don't think I understand the question. 10:19:09 You may know about Curry-Howard, with functional programming having types of intuitionistic logic. I was trying to think of what it makes if you add logic that includes numbers. 10:20:40 That is what I mean by the question. Now can you understand it? 10:36:49 -!- nooga has joined. 10:38:22 ​585072 +++++++++++++[>+++++>+++>+>++++++<<<<-]>>>+++++++++++++++++++++++++++++++++++++++++++++++.<------.>++++++++.<<++++++++++++++.------------.>>++++++++++++++++.>+++++++++++.<----.-----------.<<-----------------------------------.>>>+++++++++++++++.++++++++++++.<<<+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++.>>>--------.<-------.<-----------------------.++++++++++++++++++++++++++++++++++++++++++++++++++.>>----.++++++++++++.--- 10:52:22 I'm not sure. 10:55:59 zzo38: In Idris, if you subtract a large natural from a small natural, you just get zero 10:59:25 FreeFull: Well, that satisfies the conditions, but it doesn't describe everything that is having such conditions. 11:00:48 You could make your own integers that would produce negative values 11:02:00 (If there is an ordering and subtraction is always possible, that satisfies the conditions, but I mean even some things where subtraction might not be always possible, or where there might be more than one possible answer of the subtraction) 11:02:28 (It is not pure subtraction in such case) 11:02:35 (well, not necessarily, anyways.) 11:11:34 -!- Jafet has joined. 11:14:41 I don't mean necessarily only ordinary subtraction. 11:23:30 zzo38: Say, a function that returns a list of values? 11:26:22 -!- carado has joined. 11:27:27 FreeFull: Well, something like that; maybe returns a set of values. 11:27:45 Perhaps if you have this kind of extraordinary subtraction, then you can have the extraordinary addition to go with it, too. 11:28:28 zzo38: Well, could return [] too 11:28:47 FreeFull: Yes, that is what I was thinking of too. 11:28:53 Maybe it could work in the list monad 11:29:06 using guard to eliminate values 11:30:25 I would think it should be set monad, although you could use list monad to pretend to be a set monad. 11:30:54 But I mean there is always at least one answer if A is less than or equal to B. 11:32:29 You could probably enforce that in the type 11:34:33 -!- epicmonkey has quit (Ping timeout: 256 seconds). 11:35:57 If a Icosahedral RPG multimana is defined as the multiset of manas, then the ordinary addition is the multiset sum, and the ordinary multiplication is the cartesian product over the multiset sum. Therefore you will have an ordinary subtraction as well. But you could then have extraordinary subtraction, if A is what you have and B is the mana cost, A-B is whatever is left over afterward; there might be more than one answer (or none at all). 11:36:19 You could then have its inverse, the extraordinary addition, which does the similar thing. 11:37:09 In this case, extraordinary subtraction A-B is possible if and only if B is less than or equal to A. 11:37:19 Is the result set guaranteed to have a greatest element? 11:39:05 -!- ogrom has joined. 11:46:49 No, I don't think so. If `- is extraordinary subtraction, then (ug+ur+1)`-u can result ug+1 or ur+1 neither of which is greater. 11:51:15 However, I think that with extraordinary addition (which, unlike ordinary addition, is not commutative), there will always be one least answer, which is the same answer as ordinary addition. 12:11:49 -!- nooodl has joined. 13:05:19 -!- hagb4rd has joined. 13:32:11 -!- Vorpal has quit (Ping timeout: 246 seconds). 13:33:15 -!- ogrom has quit (Quit: Left). 13:37:01 -!- Vorpal has joined. 14:02:37 -!- Taneb has joined. 14:04:19 -!- sirdancealo2 has quit (Read error: Operation timed out). 14:08:04 -!- carado has quit (Ping timeout: 256 seconds). 14:19:19 -!- sirdancealo2 has joined. 14:21:14 hey elliott: do you still have the link to that page on whch generated sounds from mathematical formulas? i can't find :( 14:24:30 got it: http://wurstcaptures.untergrund.net/music/ 14:39:28 -!- hagb4rd2 has joined. 14:39:53 -!- hagb4rd has quit (Disconnected by services). 14:39:58 -!- hagb4rd2 has changed nick to hagb4rd. 14:49:14 -!- DHeadshot has quit (Read error: Connection reset by peer). 14:49:19 -!- DH____ has joined. 14:52:58 -!- DH____ has quit (Read error: Connection reset by peer). 14:53:03 -!- DHeadshot has joined. 15:17:32 -!- Arc_Koen has joined. 15:19:51 warning: fleshlight invasion on the wiki 15:20:07 I have no idea what that is and I really don't want to know 15:21:42 it's kind of like a flashlight 15:21:43 but 15:21:46 yeah 15:23:51 you don't? shame 15:24:13 what are they teaching kids in school these days 15:27:25 -!- heroux has quit (Ping timeout: 240 seconds). 15:29:32 -!- heroux has joined. 15:33:28 Arc_Koen: ignorance is not cool 15:36:48 oklopol: I repent 15:37:06 good 15:37:20 a fleshlight is a fake vagina. 15:38:37 WHY WOULD YOU SAY THAT 15:38:37 do you think it'll be okay for men to have sex toys too, some day? 15:39:42 Arc_Koen: it's part of my war against willful ignorance 15:40:16 is forceful knowledge better? 15:40:24 yes 15:41:57 goog to know 15:42:16 goog indeed. 15:44:15 -!- DHeadshot has quit (Read error: Connection reset by peer). 15:44:21 -!- DH____ has joined. 15:44:26 -!- monqy has quit (Quit: hello). 15:51:29 GOOG, isn't that the NASDAQ code for Google? 15:52:31 goog.com redirected me to a page (in swedish!) asking me how old I am 15:59:47 Even so, something tells me that GOOG is not the NASDAQ code for Swedish porn. 16:03:31 Google's just bought out SexyMøøse.xxx 16:04:55 When will the powerful Swedish Porn Consortium stop? D-8 16:27:50 -!- ais523 has joined. 16:35:15 http://ow.ly/j2UQo "If it’s not a cult, then why are they painted grey? And why are they wearing devil horns?" Is this... is this about Homestuck cosplayers? 16:35:19 (I had to url-shorten it because the actual link makes the 'not-sure-about-it' "joke" not work.) 16:44:02 -!- Bike has joined. 16:49:42 -!- Bike_ has joined. 16:49:47 -!- Bike has quit (Quit: Reconnecting). 16:50:30 -!- Bike has joined. 16:53:28 fizzie, seen it before, and yes 16:54:08 Taneb: Were you, in fact, THERE? 16:54:15 INDEED I WAS 16:54:20 (disclaimer: I was not) 16:54:31 Are you, in fact, "Guest"?! 16:54:32 Oh. 16:54:34 (however, I am going to an anime con in Homestuck cosplay next weekend) 16:54:48 -!- Bike_ has quit (Ping timeout: 276 seconds). 16:55:13 Oh, so you're in a cult. 16:55:39 Indeed 16:55:48 The mysterious cult known only as... 16:55:51 "Homestuck" 16:56:13 I, however, am not one of the horn-wearing grey-skinned ones 16:56:18 I AM SUPERIOR TO THAT 16:56:21 fizzie: I don't know, but I liked that last line 16:57:31 Hmm 16:57:50 One day, some English sports fans are gonna sing "Jerusalem" at a match against Israel and everyone will be confused 16:57:56 Are you cosplaying as Casey 16:58:12 Bike, I actually was almost going to be Secret Wizard 17:01:19 Alas, I am cosplaying Jake English 17:01:46 nice shorts 17:01:50 Indeed 17:01:53 I need to make those today 17:05:48 god-tier? 17:07:56 No, but green bodywarmer tier 17:08:32 good tier 17:09:39 http://sphotos-b.ak.fbcdn.net/hphotos-ak-ash4/301104_453019734742315_623549310_n.jpg <-- me being Jake English previously 17:10:31 Alas, I am not the best cosplayer 17:10:36 which one's jake english? 17:10:44 The awesome one 17:10:59 oh wow these new spam pages are fantastic 17:11:11 spam pages you say 17:11:22 http://www.mspaintadventures.com/?s=6&p=006906 17:11:25 10 Benefits of fleshlightWhy spanking the monkey at him in private. A Fleshlight is always ready to work and a certain amount of pain. Humor that has some impact on self-identity, gender relations, and many in our choices tend to be fleshlight aiming to provide confidence. 17:11:30 And the news this week that the AAFL are publicly announcing the purchase of the 'fleshlight' for added self-gratification, you'd think they'd realise that expensive set-dressed cinematic sex is soooo-1970s. Aw, hell, he does own homes in LA, Canada, New York, Stony Brook, maintained that Victorian readers would have recognized Heep's physical traits as those of an active Fleshlight. K It's called Fleshlight. 17:11:44 excellent. 17:12:01 These feels markovian 17:12:01 http://esolangs.org/wiki/User:GenesisUU wow these are just 17:12:43 get ready to rock with the ultimate handheld fleshlight 17:13:07 That's not illegal -- but it is insignifigant compared to the ribbed edges of fleshlight. 17:13:10 fungot: Have you been writing spam for money? 17:13:10 fizzie: ( it's not in the topic 17:13:58 -!- Taneb has set topic: #esoteric is supposed to be about esoteric programming languages, but is really a couple of dozen people being weird | Newsflash: fungot has been writing spam for money. | Logs: http://codu.org/logs/_esoteric/. 17:14:17 fungot, it is now. Will you amend your statement? 17:14:18 Taneb: i agree with you in the past with losing disks and such, and if you're using libxml, it's not useless if you're playing in a different mem location 17:15:36 fungot: That sounds like typical politician doubletalk to me. 17:15:37 fizzie: errr, interactive?) language with the most stupid explaination one can get. in there, quite a few are take home because... " muahaha! nothing can help you 17:15:52 I suppose nothing can help me. 17:17:39 I need to buy what my mum would call a "Hexham hat" for my SATW!Finland cosplay 17:18:35 fungot: how would you like a hexham hat? 17:18:35 olsner: i don't know 17:18:57 I think that shop opposite the witch sells them 17:19:05 But they use really foul perfume in the shop 17:19:09 So I don't want to go in 17:19:12 Taneb: Is that a village witch? 17:19:22 It's a town witch I'm afraid 17:19:41 I guess it's as good. Does curses and so on? 17:20:39 ^style 17:20:39 Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc* iwcs jargon lovecraft nethack pa qwantz sms speeches ss wp youtube 17:20:40 I just saw that Oz thing (we had due-to-expire-soonishly Christmas present theater tickets), speaking of witches. 17:21:08 `? fungot 17:21:08 olsner: it may be too clever; i'm not sure i like 17:21:15 * ais523 likes the idea that hexham has an official witch position, and they presumably need to advertise for a new witch if the existing witch retires or moves out of town 17:21:19 fungot cannot be stopped by that sword alone. 17:21:51 Wicked Witch of the Hexham. 17:24:41 ais523: I think witches usually die in office 17:24:42 like the pope 17:25:06 elliott: "retired witch" is too awesome a job description not to have it in my mental image 17:25:58 I think many retired witches still do part-time witchery to kill time. 17:29:23 elliott, would you go into that shop and buy me a hat 17:29:34 Then leave it in a pre-determined pick-up point 17:29:54 but that involves going outside 17:29:59 big commitment 17:30:37 elliott, you can do it 17:30:39 I believe in you 17:30:46 how about you do it on my behalf 17:30:46 Despite the lack of secondary sources 17:31:00 But I don't like going into that shop! 17:31:03 The perfume!!! 17:31:13 (I have a crippling fear of perfume) 17:31:16 use a gas mask 17:31:33 But where would I find a gas mask in Hexham! 17:31:40 um in the bomb shelter 17:31:40 Think these things through, olsner 17:31:44 At the hat store. 17:31:52 Isn't it kind of a hat? 17:31:59 anyway i am pretty sure this is just a plot by Taneb to find out what i look like 17:32:02 by hiding in the shop 17:32:19 Nah, it's a plot by Taneb to avoid going into the shop 17:32:28 elliott: I think that you'd find a comical net-and-a-tree kind of a trap at the hat pick-up point. 17:32:35 I already know you look like a 12 year old girl 17:33:22 that is possibly not quite accurate any more 17:33:59 Do you look like a 14 year old girl 17:34:10 um 17:34:13 maybe? 17:34:15 Or possibly one of those box things, propped up with a stick, with a theorem prover or something inside. (I don't know what they use as bait in elliott traps.) 17:34:30 Or do you look like that guy in that play I saw last night 17:34:34 You do, don't you 17:34:48 i was in no play 17:35:18 fizzie: possibly a rabbit, I have a habit of trying to follow them 17:36:27 -!- Bike_ has joined. 17:36:32 A rabbit, dead or alive? 17:36:53 -!- Bike has quit (Ping timeout: 256 seconds). 17:37:21 There was something about an inverted pyramid of rabbits. 17:38:27 I have a disk with Solaris 2011 on it 17:38:29 Would that work 17:39:16 Solaris is made out of Iblis and Mephiles. 17:39:25 hm i might actually try and steal a solaris disk 17:39:30 *disc 17:39:34 unlses it's actually a disk 17:39:43 It's a disq. 17:39:52 me too 17:40:29 Maybe the forthcoming holocube media (isn't that the future?) are going to be called disqs. 17:55:12 -!- ogrom has joined. 17:56:37 elliott: did you block GenesisUU? I only see the deletions 17:56:51 or are you hoping for more awesome language names? 17:58:03 -!- nooodl has quit (Ping timeout: 245 seconds). 17:58:03 (Block log); 17:13 . . Ehird (Talk | contribs | block) blocked GenesisUU (Talk | contribs) with an expiry time of indefinite (account creation disabled, e-mail disabled, cannot edit own talk page) ‎(Spamming links to external sites) 17:58:22 boring 17:58:24 fascist 17:58:26 -!- Bike_ has changed nick to Bike. 17:58:44 yes 17:58:45 -!- DH____ has quit (Read error: Connection reset by peer). 17:58:56 Bike: if you want i'll make you a sysop so you can unblock them! 17:58:58 (probably not) 18:04:14 -!- Phantom_Hoover has joined. 18:07:18 -!- oerjan has joined. 18:07:53 *GASP* 18:08:04 fungot: how COULD you 18:08:04 oerjan: runtimeerror fnord' codec can't decode bytes in position 1-2: illegal multibyte sequence) really... i would have exported. oh well. only on l2 l3)) 18:08:10 oerjan: it's ok the spam was really good 18:08:15 oh. 18:08:31 food -> 18:11:37 fungot: Are you have character set problems? 18:11:37 fizzie: i am a pissed off fnord, but it needs an extra field per object and a list 18:11:48 Uh-kay. 18:12:23 hrm. What's the point of spam where the spammer pretends to be a female who wants to start a relationship? 18:12:48 Sgeo: to get responses 18:12:56 Possibly also to scam money? 18:13:00 just getting someone to respond to spam at all is something of a victory for a spammer 18:13:01 For "plane tickets" or whatever. 18:13:13 fizzie: yes, that would be a plausible followup 18:13:32 but having a conversation with someone about anything at all gives you more of an opportunity to scam them, than if they ignore everything you say 18:13:38 Or for the medical expenses of a badly ill mother, or something. 18:13:48 pissed off fnords are the scariest 18:13:53 Or possibly a stove. 18:14:06 Cf. http://www.joewein.net/spam/spam-elena-needs-woodburning-oven.htm 18:15:07 I've gotten a few of those requests for the "wood burning stove". 18:15:59 Actually, there's a hilarious sentence here, I'm going to pastie the spam 18:16:30 "Dear ICS doctoral students -- Please register and participate! Interesting talks, good company, free food!" I see they get their "how to get doctoral students to attend" strategy from PhD comics. 18:16:30 actually, I wonder what sort of success rates you could get preying on spammers 18:16:54 many of them will be more gullible than average, and there's no problem in starting a conversation with them 18:16:55 http://pastie.org/private/bkc3kimpstoepmjsag0vq 18:16:56 ais523: 419eaters was pretty popular at some point 18:16:59 ais523: 419- yes 18:17:05 Bike: yeah but it wasn't trying to make an income 18:17:08 just embarrass people 18:17:13 (I censored the email) 18:17:25 "Many Humans began their relationship through correspondence. And so I decided to try it." 18:17:31 Clearly she's an alien. 18:17:33 i wonder what the economic situation of your average 419 scammer is 18:17:36 don't you believe in love 18:17:36 actually I've seen a theory that many of the really really obvious scam attempts are the result of people who'd been scammed into buying into "get rich quick by scamming people" scams 18:17:39 a sort of metascam 18:18:00 Sgeo: um how am i meant to reply to juliya if you cut out the email 18:18:08 the scam that gets sent out to the public doesn't have to work, it just has to be good enough to convince the victim scammer it will work 18:18:08 elliott: back in the day it was not good, so 419eating got a bit controversial, since you were like tricking poor nigerians into fucking themselves 18:18:21 a sense of... proportion 18:18:44 419eater and its operatives was profiled on the September 9th, 2008 episode of Public Radio's This American Life,[3] specifically one particular bait that ran for 100 days starting in April 2008 and involved sending a scammer named Adamu from Lagos, Nigeria to Abéché, Chad, a dangerous and politically unstable region.[4] 18:18:57 looks like my intuition of them probably actually being dicks is accurate 18:19:06 yeah 18:19:16 I don't get why you'd trick a scammer into going to Chad anyway 18:19:32 you can get equally amusing results without putting the scammer in danger 18:19:55 well i'm not sure this attitude views the scammers as real people 18:20:16 but they are 18:20:31 in a way they're realer than other people, because you can talk to them and have some sort of idea that they exist 18:20:32 wow you could get a phd in philosophy with insights like that 18:20:45 there's more evidence that scammers exist, than that, say, the average Nigerian exists 18:21:03 i'll notify 419eaters' bayesian division immediately 18:22:24 did you see the thing about how scammers will identify as nigerian even when they aren't 18:22:36 in order to quickly do away with anyone who is even slightly suspicious 18:22:43 kmc: the idea is to get the most gullible people to respond, right? 18:22:47 yes 18:22:56 gullible / ignorant / whatever 18:22:59 I love the idea that you should appear as untrustworthy as possible to get /the most trusting responses/ 18:23:19 yeah 18:23:24 it makes sense, really 18:23:28 it's the kind of thing that doesn't make any sense unless the number of people receiving your message is gigantic 18:23:32 I remember a TV show in the UK which needed gullible contestants 18:23:36 i read a neat article on how nigerian scammers were viewed in their societies, lemme find it 18:23:42 ais523, Deal or No Deal? 18:23:44 Speaking of curious things about spam, what I think a bit strange is the ones that are trying to sell some really specific product. Like all the chinese companies selling PCB manufacturing, or the one who wanted to sell me... I forget exactly what it was, maybe earthmoving equipment. Or concrete-mixing trucks. Anyway, something that presumably would (a) not interest a vast majority of ... 18:23:49 maybe this is like putting armor on the parts of your planes where the ones that come back /don't/ have bullet holes 18:23:50 so it started out with a trial period that selected for gullibility 18:23:51 ... recipients, and (b) would hopefully not be purchased based on random spam emails. 18:24:02 ais523: was that the one where they pretended to send them into space 18:24:03 (presumably they told the contestants they were selecting for something else, the people who were actually gullible would believe them) 18:24:05 kmc: yes 18:24:12 i remember that one 18:24:16 british TV can be hilariously mean 18:24:17 I don't 18:24:24 didn't they figure it out before it was over and so it was kind of a letdown 18:24:26 Linky to info? 18:24:38 http://en.wikipedia.org/wiki/Space_Cadets_(TV_series) 18:24:42 elliott: no, they didn't all; several of them did but they were removed from the show via some excuse or another 18:25:01 also they snuck all the past contestants on board the spacecraft temporarily, while it was allegedly in space, just to see if they could 18:25:03 thelliott 18:25:06 ugh, wikipedia, i don't care about 419s in some tv show 18:25:16 fizzie: "Dear manager: This is Emily from China. Glad to hear that you"re in the field of wire mesh. We specialize in WIRE MESH for many years" 18:25:23 i keep getting this one 18:25:29 this reminds me of BlogNomic getting spam about stone crushers, specifically 18:25:32 it comes with some nice photos of wire mesh 18:25:55 kmc: "We, Sanitek Co., Ltd specializes in the field of Ozone purification systems for air, water, waste water, agri-food and gas liquid mixing technology for industrial, commercial and municipal applications." 18:25:58 blagh. 18:26:04 Indeed, during the shooting of Space Cadets, smokers amongst the production crew were given Russian cigarettes to smoke in case any of the cadets discovered the butts. 18:26:06 That's from my inbox right now. 18:26:11 this seems rather overkill if the idea is that they are as gullible as possible 18:26:27 elliott: the overkill was to make it more fun for the people watching 18:26:30 I'm pretty sure 18:26:33 ...I've just realised that one of the Haskell libraries I've created really treads on zzo38's toes 18:26:42 elliott: if they were actually clever, they would know you can get western cigarettes in russia 18:26:54 kmc: right i was thinking they could just say "oh yes, british cigarettes are the best in the world" 18:27:02 so it only works on dumb people who think they're clever 18:27:05 kmc: Also it too comes with "ozoneboy sanitek(10-22-08-49-56).jpg", but I'm not sure I want to check it out. 18:27:14 ozoneboy! 18:27:28 fizzie: first two authors in my spam folder: "Ellen DeGeneres weight loss Free Sample", "No risk Ellen DeGeneres Promo" 18:27:29 elliott: overkill is inherently entertaining, don't you agree? 18:27:31 sensing a theme here 18:27:37 "Stereotyped characters, including a slow-talking Royal Air Force Squadron Leader with a luxuriant handlebar moustache" 18:27:40 ais523: yes, your explanation makes sense 18:27:55 oh, I was just thinking in general, not trying to argue my point further 18:27:57 zzo38, if you make monoidplus depend on groups I'll give you an e-hug 18:28:07 like, overengineered programs are usually less useful than more typical prorgams 18:28:09 *programs 18:28:13 but they're also more awesome 18:28:20 "Your Liberty Reserve Account Has Been Blocked!" 18:28:21 oh no! 18:28:30 where will I keep my liberty now? 18:28:46 also "PRESIDENT JOHN" has emailed me 18:28:54 HELLO 18:28:54 Do not be suprised and please forgive me If this business proposition offends your moral values 18:29:00 John is a perfectly reasonable name for a president 18:29:15 I get spam emails about conferences on my university account, which makes sense really because I'm known to have written papers 18:29:20 @tell zzo38 if you make monoidplus depend on groups I'll give you an e-hug 18:29:20 Consider it noted. 18:29:27 the spam on nethack4.org is mostly about search engine optimization, which also makes sense 18:29:41 it's hilarious how blatant it is about their methods 18:29:42 I like the Double hoax ideas 18:29:57 http://en.wikipedia.org/wiki/John_Dramani_Mahama apparently its this dude 18:30:01 someone emails me asking for money to spam 2 million blog comments pointing at my website… 18:30:09 Sgeo: what's a double hoax? 18:30:17 elliott: http://en.wikipedia.org/wiki/Goodluck_Jonathan 18:30:20 Greetings! 18:30:20 It has come to our attention that you are trying to sell your personal Diablo III account(s). 18:30:29 just sayin' 18:30:37 -!- Nisstyre-laptop has joined. 18:31:01 my Diablo III account got banned :( 18:31:13 coppro: why? 18:31:16 ais523, the Wikipedia page for Space Cadets notes that some thought that maybe the hoax was on the viewers, tricked into thinking that the participants were gullible and not just actors 18:31:19 Bike: that is a great name 18:31:21 I don't know. I didn't know I had one 18:31:27 I just got an email saying I got banned :( 18:31:34 'As the attention to detail in the hoaxed environment became clear, some viewers expressed suspicions – in particular on Channel 4's message board for the programme – that the entire show, including the apparent gullibility and abject ignorance of the Cadets, was in fact a double bluff; all the Cadets were actors and that the real target of "the biggest prank in television history" was the "gullible" viewing public.' 18:31:56 Sgeo: the most common such theory I saw was that the spaceship was actually in space, which seems dubious 18:32:05 i get a lot of phone calls telling me there are presently no problems with my current credit card plan but 18:32:07 I like the "everyone is an actor" theory, though 18:32:16 it wouldn't change the show in my view at all 18:32:26 Also here's my latest spam; it's a nice hybrid of both the "40% of $5.6million" *and* the "I am 28 years old and i am Single" approaches: http://sprunge.us/ABRd 18:32:34 Maybe I should watch it 18:32:41 coppro: oh, it was lying? 18:32:58 ais523: spam, I imagine 18:32:59 ;) 18:32:59 ais523: I like the idea that Channel 4 would send a spaceship into space just to mses with people 18:33:02 `addquote there's more evidence that scammers exist, than that, say, the average Nigerian exists 18:33:07 982) there's more evidence that scammers exist, than that, say, the average Nigerian exists 18:33:23 elliott: so do I 18:33:32 fizzie: cool, a yak emailed you 18:33:34 kind of a shame the average nigerian isn't named Goodluck, when you think about it. 18:34:00 elliott: "Showing results for 'ancient yak'. Search instead for 'ancitt yak'." 18:34:21 elliott: I guess yet another theory is that the production crew believed that the contestants were gullible 18:34:33 but the contestants had actually worked it out and were acting in order to fool the production crew 18:34:53 fizzie: that is one weird-ass email 18:35:23 ais523: what if the contestants knew that the production crew knew that they were pretending that they knew that they knew that the production crew believed that they were pretending it wasn't fake? 18:35:27 elliott: http://waronspam.com/dearest-greetings/ hey, Miss Yak has also written to this other guy, and there she says she's 25 years and offers $55.6 million. 18:35:30 and were just pretending that they didn't? 18:35:54 fizzie: well she has to spend the money obviously 18:35:56 elliott: that reminds me of a Mafia game I played 18:36:12 where I was Mafia and I had a private communication channel with someone else who was also Mafia, but on a different team 18:36:55 we both knew the other was mafia, but were pretending not to, and we both knew the other knew we were Mafia, but we won because I managed to fool the other person into thinking I didn't realise he knew I knew he was Mafia 18:37:16 help 18:37:19 fizzie: actually, something that annoys and confuses me: you know those dating adverts where they tell you about people in your local area who want to meet you? 18:37:25 ais523, that's ridiculous 18:37:30 I've occasionally seen two, on the same page, different names but the same photo 18:38:03 ais523: It would be extra work to avoid that. 18:38:06 man, the best i've done is win Bullshit by lying when i didn't have to. 18:38:31 fizzie: yeah but it rather ruins the impression that the adverts are trying to give 18:38:50 i think the best game is kilgame 18:39:37 My other address seems to have gotten mostly SEO and "cheap Facebook likes" spams now. 18:40:02 The Facebook likes are "Manually Promoted by experts not bots/software involved". 18:40:12 fungot: Do you sell any Facebook likes? 18:40:12 fizzie: i also agree with riastradh high ( or one might call it low/ deep level) stand. and there's no agora war ( between the vertices 12 and 14? 18:40:56 The SEO offer says they'll have "100 EDU Backlinks" and "15 PR 5-8 Web 2.0 Profile Backlinks". 18:41:03 scanl is the fast one rigth 18:41:06 oerjan: hel 18:41:06 p 18:41:15 Oh, it's the same company that's also selling the Facebook likes. 18:42:19 "Subject: We send the Ph.D and College certificate to all countries, bay today qualitatively, not expensively" 18:42:23 I'll certainly bay today. 18:42:47 qualitatively or expensively? 18:43:18 I usually bay qualitatively. 18:43:56 "Hello Fizzie, Just change your style depending on your mood: the past you were a commerce lady, now you just want to wear jeans and a top and tomorrow you require to dress up for an vital banquet." 18:44:00 I don't think I've ever been "a commerce lady". (Is that slang for a prostitute?) 18:44:54 "Hello! My name is Tanya , I am lonely russian woman from Ulyanovsk." 18:45:00 ais523: you should bring up that mafia game the next time someone posts one of those "there are n people; you tell them something that triggers one of their customs and after n days something bad happens" puzzles 18:45:02 nice place 18:45:17 I've got two other Tanyas in my spam folder 18:45:38 oerjan: I think I figured those puzzles out 18:45:43 elliott: scanl is pretty fast i think, as long as you consume the list in order 18:45:56 oerjan: right. and scanr isthe inefficient one? 18:45:58 @src scanl 18:45:58 scanl f q ls = q : case ls of 18:45:58 [] -> [] 18:45:58 x:xs -> scanl f (f q x) xs 18:45:58 @src scanr 18:45:59 scanr _ q0 [] = [q0] 18:45:59 scanr f q0 (x:xs) = f x q : qs 18:46:00 where qs@(q:_) = scanr f q0 xs 18:46:41 the idea is that although you know that there are either 50 or 49 people in a particular state, you don't know whether the other people agree with you, or believe it's 49 or 48, and those people must be wondering about the (incorrect) possibility that you're believing it's 48 or 47, and so on down to 0 18:46:48 -!- Phantom_Hoover has quit (Ping timeout: 245 seconds). 18:46:50 so there's a day's delay for each level of indirection 18:46:54 is that the blue eyed island puzzle? 18:46:58 Bike: yes 18:47:01 or various variants of it 18:47:02 good puzzle 18:49:02 elliott: i don't know about inefficient, i suspect they have similarities to foldl and foldr so it all depends on the strictness of the combining function? 18:49:45 IIRC it's kind of dual 18:49:49 as in, you usually want foldr and scanl 18:49:57 and also scanl1 is total. 18:50:28 well scanl gives you the resulting list elements quickly if the combining function is strict 18:50:47 but i suspect scanr will be the other way around? 18:51:26 that is, _neither_ necessarily needs to go to the end of the list to produce anything, but scanl always produces the first element fast 18:51:41 while scanr needs the combining function to be lazy 18:51:56 > scanr f x [1..10] :: Expr 18:51:58 Couldn't match expected type `Debug.SimpleReflect.Expr.Expr' 18:51:58 w... 18:52:07 now what 18:52:10 :t scanr 18:52:12 (a -> b -> b) -> b -> [a] -> [b] 18:52:30 > scanr f x [1..10] :: [Expr] 18:52:32 [f 1 (f 2 (f 3 (f 4 (f 5 (f 6 (f 7 (f 8 (f 9 (f 10 x))))))))),f 2 (f 3 (f 4... 18:52:57 > scanr f x [1..3] :: [Expr] 18:52:57 that's perfectly well defined even for an infinite list if f is lazy 18:52:59 [f 1 (f 2 (f 3 x)),f 2 (f 3 x),f 3 x,x] 18:53:25 (well, lazy productive) 18:53:40 and f not only has to be lazy, but also capable of returning a result without investigating its second argument, at some point 18:53:59 ais523: ... 18:54:06 are you aware of the definition of non-strictness? 18:54:18 elliott: yeah but it has to look at at least one of its arguments 18:54:23 to be interesting 18:54:36 my point is that it has to be lazy in the second argument in particular 18:55:04 oerjan: I think I figured those puzzles out <-- i meant bringing them up to the people who inevitably say those puzzles are nonsense in practice 18:56:07 oerjan: all sorts of things get people saying that about them 18:56:30 and it wasn't a that in-practice situation, only non-game situation I can think of where that might happen is international diplomacy 18:57:13 what about business? 18:57:27 > iterate f 0 18:57:29 Ambiguous type variable `a0' in the constraints: 18:57:29 (GHC.Num.Num a0) 18:57:29 a... 18:57:30 hmm, I guess that's similar 18:57:33 > iterate (f x) 0 18:57:33 oerjan: something about them being the same thing 18:57:35 Ambiguous type variable `a0' in the constraints: 18:57:35 (GHC.Num.Num a0) 18:57:35 a... 18:57:42 > iterate (f x) 0 :: [Expr] 18:57:45 [0,f x 0,f x (f x 0),f x (f x (f x 0)),f x (f x (f x (f x 0))),f x (f x (f ... 18:58:28 > scanr const undefined [1..] 18:58:30 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28... 18:58:39 -!- carado has joined. 19:00:06 > iterate f (0 :: Expr) :: [Expr] 19:00:08 [0,f 0,f (f 0),f (f (f 0)),f (f (f (f 0))),f (f (f (f (f 0)))),f (f (f (f (... 19:00:37 FreeFull: ambiguity means "please add type annotation so I can guess which type you are trying to use" 19:01:44 I get that 19:01:46 (unless you're using lens which is ridiculous) 19:02:02 (actually, even if you're using lens) 19:02:20 > [1,2,3] ^. traverse 19:02:21 Ambiguous type variable `a0' in the constraints: 19:02:21 (GHC.Num.Num a0) 19:02:22 a... 19:02:31 > views traverse Sum [1,2,3] 19:02:33 Sum {getSum = 6} 19:03:52 somehow it disturbs me that Taneb already understands haskell this well :P 19:04:14 oerjan: hasn't it been like a year since he started learning 19:04:20 oerjan, Haskell is what I waste all my time with 19:04:44 elliott: i'm not used to him having been around here for that long yet 19:04:49 elliott: hmm… there are more distinctions than just "lazy" and "strict", I think 19:05:10 I can imagine a function that's strict in both arguments but doesn't evaluate the second argument until after it's finished processing the first 19:05:18 this distinction doesn't matter in Haskell, but it's important in languages like Verity 19:06:08 Are you contemplating dangerous hybrids of Strict and Lazy? 19:06:28 oerjan, and I didn't really have much imperative coding background 19:06:43 oerjan, AND I had been messing with lambda calculus before I switched to Haskell 19:06:51 ais523: even seq doesn't guarantee it with ghc, so they had to add pseq which does 19:07:31 ...that helps. i'd been doing unlambda... 19:07:31 oerjan: oh right, I forgot about seq 19:08:00 elliott: anyway, upshot is I can mentally consider a function as lazy even if it's strict in every argument 19:08:05 seq makes things strict, but still doesn't guarantee any order of strictness 19:08:24 ais523: you are just providing more data for hypothesis "ais523 is crazy" 19:08:39 elliott: no, your mind's been warped by Haskell 19:08:43 into not considering details that Haskell elides out 19:09:18 * elliott is perfectly well accustomed with different evaluation orders and purities tyvm 19:10:35 ais523, is Space Cadets a good show? 19:10:46 seq is like a binder 19:10:58 Sgeo: not really; I enjoyed it but I'm not sure I'd recommend it to everyone 19:11:03 I think it worked better live 19:11:13 because everyone was hoping the whole thing would collapse 19:11:46 FreeFull, binder as in things you put papers in, or binder as in things to aid biological females appear male 19:11:52 Or binder in a third sense 19:12:00 Taneb: third sense, I think 19:12:23 binder as in something that combines a function and arguments 19:12:27 It takes two things and joins them into one thing 19:12:31 (not a good definition, but that sort of thing) 19:12:56 I'm thinking a binder for thunks maybe? 19:21:20 FreeFull: the lack of order guarantees i mentioned means it is dangerous to think of it as any _specific_ thunk composition. thunks are an implementation strategy, which ghc generally tries to optimize away or move around whenever the _actual_ language semantics don't require them. 19:22:12 the official definition of seq is that seq "bottom" x = bottom, seq non-bottom x = x 19:23:19 -!- epicmonkey has joined. 19:23:50 That definition of binder is nothing like the previous two! 19:25:52 Just seen on Tumblr: 19:26:09 "Aren't we /all / internet explorers?" 19:26:23 "...do you mean we run slow and people don't like us?" 19:26:24 the NeXT was in you all along 19:26:32 "That's exactly what we are" 19:26:38 * oerjan suddenly realizes that "binders" in english doesn't mean paper clip, and wonders how it got borrowed into norwegian meaning that 19:28:30 http://homestuck.bandcamp.com/track/hardlyquin-2 -- oerjan's current emotional state in Homestuck music 19:28:53 oerjan: it has a very vaguely similar meaning 19:28:58 ais523, this is educational, kind of 19:29:09 Sgeo: what, the program, are you watching it? 19:29:19 in what way do you find it entertaining? 19:29:44 It's showing something they're calling the 'jar test', to measure whether the contestants are likely to conform 19:31:15 I've been wondering if that test actualyl works 19:31:17 *actually 19:31:35 they should just submit everybody to milgram to traumatize them 19:32:46 -!- Taneb has quit (Quit: DINNER). 19:32:58 -!- Phantom_Hoover has joined. 19:35:44 What is the Curry-Howard of quantum logic? 19:36:54 i once found something called basic logic which is apparently a subset of quantum logic and can be given a curry-howard interpretation with continuations. but i never managed to see a meaningful interpretation of the orthomodular law. 19:39:21 it was basically a substructural sequent logic 19:40:08 it was also a subset of linear logic 19:40:15 um OBVIOUSLY you need a quantum computer 19:40:17 quantum lambda calculus 19:40:36 quantum logic isn't obviously directly related to quantum computers 19:40:46 oerjan. oerjan i was kidding 19:40:47 higher-order functions and quantum computers don't obviously mix 19:41:01 it's the logic of hilbert space projections 19:41:10 quantum computers don't really understand control flow, and higher order functions act like control flow operators 19:41:20 -!- ogrom has quit (Quit: Left). 19:41:31 I don't understand control flow, either 19:42:20 maybe one should first ask "what is the curry-howard correspondence of reversible computing" 19:46:12 ^bf +++++++++++++[>+++++>+++>+>++++++<<<<-]>>>+++++++++++++++++++++++++++++++++++++++++++++++.<------.>++++++++.<<++++++++++++++.------------.>>++++++++++++++++.>+++++++++++.<----.-----------.<<-----------------------------------.>>>+++++++++++++++.++++++++++++.<<<+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++.>>>--------.<-------.<-----------------------.++++++++++++++++++++++++++++++++++++++++++++++++++.>>----.++++++++ 19:46:12 . wat 19:46:43 oerjan: is that binder transliterated into norwegian as bajnder or something? 19:46:44 (EgoBot said that in the logs) 19:47:37 it could come from "binder clip", which is apparently a kind of paper clip 19:47:47 olsner: its "binders" pronounced as a normal norwegian word (except that those rarely end in -s unless they were borrowed from english) 19:48:26 also those -s borrowings are frequently singular despite being english plurals 19:48:50 i think it was fashionable to borrow that way some time in the 20th century 19:49:19 for some reason the swedes made up the word "gem" instead 19:49:21 *it's 19:50:36 olsner: that's originally a trademark 19:50:46 "Paper clips are still sometimes called "Gem clips", and in Swedish the word for any paper clip is "gem"." 19:51:04 heh, somewhere in norway there's a statue commemorating the (norwegian) inventor of the paper clip ... with a different type of paper clip than the one he invented 19:51:18 ais523, why is the name of the Russian supermarket blurred out? 19:51:45 Sgeo: my only reaction to that question is to be amused that you expected me to know the answer 19:52:00 although it's a pretty interesting question 19:52:01 yeah the wikipedia article on paper clip mentions that that inventor didn't really invent it 19:52:10 was the supermarket actually in russia, or in fake-russia? 19:52:26 "Vaaler probably did not know that a better product was already on the market, although not yet in Norway. His version was never manufactured and never marketed, because the superior Gem was already available." 19:52:27 -!- Taneb has joined. 19:52:33 According to the show, it was actually in Russia, but if the conspiracy theories are true, who knows 19:53:03 Hmm, they said that the Russian authorities wouldn't allow them to film. I guess that could be why, or part of why? 19:53:46 why would they show a supermarket that was actually in Russia 19:53:57 if the show wasn't filmed in Russia, it was just pretending to be? 19:54:28 It was showing the producers buying stuff to help fool the contestants into thinking they were in Russia 19:55:17 right 20:03:22 oh god does enjoying this show mean i'm suddenly a reality tv person? 20:03:26 hi 20:04:09 elliott, earlier you @ask'd me whether I was an amulet non-finding bot or such 20:04:15 Could you remind me the context for that? 20:05:23 Taneb: well there is this thing called TAEB 20:05:36 Well, here's the thing 20:05:39 I'm not TAEB 20:05:43 I'm vastly superior 20:05:52 good to know 20:05:57 Including in terms of amulet non-finding skills 20:06:25 TAEB is very good at not finding amulets 20:08:05 I'm better 20:08:13 I have never found an amulet in my life 20:08:35 With that jar test, you'd need a bunch of confederates to go first, unless you don't mind not testing the people who go first. 20:09:17 -!- Phantom_Hoover has quit (Quit: Leaving). 20:09:40 -!- Phantom_Hoover has joined. 20:13:09 -!- augur has quit (Remote host closed the connection). 20:14:09 -!- augur has joined. 20:15:40 Hmm 20:15:50 There are a couple of movies I want to watch 20:15:55 Except they are pretty crap 20:17:03 * Mathnerd314 pokes his head in 20:17:27 are there really a couple dozen people in here? 20:17:41 total of 81 nicks [0 ops, 0 halfops, 0 voices, 81 normal] 20:17:49 Well, there's me, Sgeo, elliott, ais523, Bike 20:17:59 oerjan, olsner, fizzie, Gregor 20:18:03 FreeFull, 20:18:15 coppro, kmc... 20:18:25 don't forget blsqbot. or hogeyui. or yiyus 20:18:28 That's the first dozen 20:18:32 WHO DARES WAKE ME FROM MY EVIL SLUMBER 20:18:39 Speaking. 20:19:00 it's just not a party if yiyus isn't here 20:19:27 fungot: Always they forget you. 20:19:28 fizzie: ugh, the cost of massive, staggering performance problems. and the spelling is just a regular unspecial genius 20:19:48 * Mathnerd314 walks out slowly 20:20:03 Arc_Koen, Fiora, oklopol, Phantom_Hoover, pikhq, shachaf, Vorpal, zzo38... 20:20:11 Sgeo: the people you put first are the people you've already disqualified anyway and just don't want to admit the fact 20:20:15 Taneb, why? 20:20:29 Why, indeed. 20:20:30 I'm listing people who speak in this channel 20:20:34 For Mathnerd314 20:20:46 don't do that 20:20:47 I'm up to 20 regulars 20:20:48 Mathnerd314 also speaks 20:20:54 Yes, but it's an open question why anyone would speak in this channel. 20:20:57 I'm pretty sure I've seen him/her speak before 20:21:20 hey what's the name of that axiom about decidable propositions on the natural numbers 20:21:23 constructivism 20:21:25 i bet oerjan knows 20:21:30 wat 20:21:33 maybe it has kolmogorov or markov or someone in the name 20:21:47 it's like ~(forall n:nat, ~P(n)) -> (exists n:nat, P(n)) 20:21:54 Axiom of Markogorov. 20:21:54 er *forall P:nat->Prop, 20:22:36 you should be glad none of us is close enough to collect on your bets. except Taneb who cannot because it would destroy the universe. wait that's just a plot you've made to keep Taneb from collecting on your bets isn't it. 20:22:51 elliott: the original proof of Gödel's incompleteness theorem worked by abusing that 20:23:01 brinkmanship at its finest 20:23:15 elliott: omega consistency 20:23:17 ais523: well gödel's proof was classical, was it not 20:23:54 except hm 20:23:57 oerjan: hmm... I'm pretty sure I'm thinking of something with a different name, but it seems related 20:24:22 omega consistency is classical so... 20:24:51 * elliott wonders if Wikipedia has a list of axioms... 20:25:00 and not really an axiom i guess 20:25:20 oerjan: oh I forgot to mention that P must be decidable, iirc. and the idea behind the axiom is that you can just go through all naturals n until you find one that satisfies P 20:25:30 the trick being, you can't prove that loop halts without an axiom 20:26:53 right. it sounds like it's _in spirit_ the same as omega consistency translated to constructivism. 20:34:43 -!- epicmonkey has quit (Ping timeout: 245 seconds). 20:37:55 -!- augur has quit (Remote host closed the connection). 20:38:20 -!- augur has joined. 20:42:38 -!- augur has quit (Ping timeout: 245 seconds). 20:54:02 Tempted to redefine Numberwang with unknown specification and a closed-source reference implementation 20:58:53 -!- copumpkin has quit (Ping timeout: 245 seconds). 20:59:19 -!- copumpkin has joined. 21:05:54 ais523, thank you for introducing me to this show 21:06:17 oerjan, what would you recommend I do to become an EVEN BETTER HASKELL PROGRAMMMER 21:13:32 refactor all your programs to do their computation in the type system. 21:15:58 -!- sirdancealo2 has quit (Ping timeout: 245 seconds). 21:17:37 Oh no! 21:28:58 -!- sirdancealo2 has joined. 21:44:15 oerjan: i feel like i should warn you that i am considering proving your underload reductions to work in coq. there may be questions. 21:46:26 -!- copumpkin has quit. 21:47:06 ooh 21:47:39 Good luck 21:48:26 well i've found bugs in those sections before. but given that the constructed programs actually ran, i'm not _overly_ nervous :P 21:49:03 yes, it's as much for want to something to do in coq than anything else. 21:49:17 though I am also poking around at trying to prove the halting problem for the untyped lambda calculus. 21:49:31 (the main issue seems to be teaching it about the untyped lambda calculus.) 21:49:43 heh 21:50:18 -!- copumpkin has joined. 21:51:58 oerjan: aha, I found it! 21:51:59 http://en.wikipedia.org/wiki/Markov's_principle 21:52:54 -!- Nisstyre-laptop has quit (Ping timeout: 264 seconds). 21:52:58 aha 21:56:02 I wonder what you "lose" by adding that principle. 21:56:28 like, if you can prove (~forall n, ~P(n)) for decidable P while there still being an argument to be made that there isn't "actually" an n that satisfies it 21:56:49 (and that possibly the algorithm that loops through all n will never find one somehow...?) 21:57:31 elliott: how do you define "decidable", here? 21:58:56 ais523: the standard way? forall n, P(n) \/ ~P(n) 21:59:27 i.e. there is an algorithm that proves either P(n) or ~P(n) for any given n. but of course it gets trickier: that algorithm may itself invoke Markov's principle... 21:59:28 OK, so the axiom is basically defining what "forall" means, I think 21:59:39 err... I don't agree 21:59:51 this is only about P : nat -> Prop, after all 22:07:38 -!- sirdancealo2 has quit (Ping timeout: 245 seconds). 22:10:11 -!- Nisstyre-laptop has joined. 22:10:21 -!- Nisstyre-laptop has quit (Read error: Connection reset by peer). 22:15:39 -!- Phantom_Hoover has quit (Quit: Leaving). 22:16:03 -!- Phantom_Hoover has joined. 22:19:39 coq really needs hoogle. 22:19:42 coogle. 22:23:23 -!- sirdancealo2 has joined. 22:28:21 -!- wareya has left. 22:30:53 -!- nooodl has joined. 22:52:40 -!- copumpkin has quit (Ping timeout: 252 seconds). 22:53:17 -!- copumpkin has joined. 22:54:35 -!- augur has joined. 22:57:49 ...there's a Hexham Annual Town Meeting?! 22:59:22 Taneb: but you and elliott can't both attend it 22:59:35 Luckily, elliott can't go outside 22:59:39 And I don't really care 23:00:11 I love the stupidity of browser agent strings 23:00:30 Almost every browser claims it is Mozilla. 23:00:47 Webkit points out it is KHTML even though it has come a long way from that. 23:00:57 And Chrome mentions Safari in the string 23:01:23 And IE? 23:01:38 Taneb, well I don't have one to check with, but at least it claims it is Mozilla 23:01:45 My current browser says: Mozilla/5.0 (X11; Linux x86_64) AppleWebKit/537.22 (KHTML, like Gecko) Chrome/25.0.1364.160 Safari/537.22 23:01:45 IE claims it's mozilla too 23:01:53 And... lynx? 23:02:03 oerjan: I wonder if interesting things happen if you increase your criteria for evidence of a proposition. like, a constructive proof of (exists n, ...) gives you a concrete n, but it might take longer than the age of the universe to compute. what if you required the constructions to not just be computable, but computable with e.g. certain asymptotic bounds? 23:02:03 I don't think lynx claims that 23:02:10 Dunno, don't have lynx installed 23:02:11 (whenever I want to say something crazy I just add "oerjan:" to the start) 23:02:12 it is just a massive clusterfuck 23:02:32 if you actually want to know the browser (for statistics or whatever) you need advanced parsing 23:02:45 links2 says it's Links (2.7; Linux 3.7.10-1-ARCH x86_64; GNU C 4.7.1; x) 23:04:32 elliott: you should look at the bellantoni-cook polytime functions 23:04:56 oerjan: yikes, no wikipedia page. this is going to be fun. 23:05:15 * elliott was almost hoping for "that's completely stupid." 23:05:16 FreeFull, that one is straight forward 23:05:22 FreeFull, unlike anything else 23:05:24 it's been a long time since i read about it 23:05:32 ooh this looks interesting. 23:05:34 well okay, wget, googlebot and such are straight forward too 23:05:40 probably w3m and lynx as well 23:05:47 but any major GUI browser? Nope. 23:06:08 Opera's fairly sane. 23:06:14 pikhq, really? 23:06:42 Opera/9.80 (Windows NT 6.0) Presto/2.12.388 Version/12.11 23:06:44 An example. 23:06:56 hm nice 23:06:58 well the trick there is that nothing supports opera anyway 23:07:03 pikhq, I have to say that Chrome is especially insane, Mozilla, Webkit, KHTML, Gecko, Chrome, Safari 23:07:11 It's Opera/9.80 at the start because some idiotic comparators think Opera/10 < Opera/9 23:07:21 pikhq, lol 23:07:23 elliott: oh and of course primitive recursion is a similar, simpler thing 23:07:28 oerjan: right of course 23:07:50 Firefox claims it's Mozilla/5.0 (X11; Linux x86_64; rv:19.0) Gecko/20100101 Firefox/19.0 23:07:58 Which is reasonable, since it is Mozilla's descendant 23:08:09 It actually literally is Mozilla, so yeah. 23:08:17 FreeFull, okay, it gets away with it 23:08:27 No lies there at all. 23:08:31 FreeFull, anything else that claims it is Mozilla doesn't however 23:08:35 Well, Mozilla/5.0 kinda is. 23:08:38 pikhq, it is still not Mozilla 5 23:08:39 and istr there was another variation that gave logspace complexity 23:08:39 yeah 23:08:56 Vorpal: seamonkey? 23:09:01 Vorpal: Of course, strictly speaking the Mozilla there does not refer to the Mozilla browser at all. 23:09:14 oerjan: I am interested in what it means from a logical POV... as in, to get constructivity, we discard LEM; to get "linear-time constructivity" or "exponential-time constructivity" or whatever, what gets dropped? presumably induction gets weakened somehow... 23:09:16 FreeFull, uh, I heard of it, but don't really know what makes it special 23:09:23 pikhq, oh? 23:09:25 But rather the 5th revision of the Mozilla project. The 4th of which was Netscape 4. 23:09:28 Vorpal: It's basically a modern Netscape 23:09:40 FreeFull, oh, who made it? 23:09:49 Mozilla 23:09:55 why, they have firefox 23:09:57 xkcd 82 is weird 23:10:01 It's a fork of the Mozilla monolithic browser. 23:10:08 ah 23:10:12 who would want that 23:10:12 It's now an external project, using Gecko. 23:10:38 Some people like having an email client, html editor and stuff built in =P 23:10:53 hah 23:10:56 I'd be amused if it's less resource-heavy than Firefox. 23:11:00 Which it could be... 23:11:05 I guess seamonkey split off 23:11:12 But it originally was a Mozilla project 23:11:30 The name "Seamonkey" was introduced when it split off. 23:11:33 elliott: just apply curry-howard hth 23:11:41 Well, "The Mozilla Foundation provides hosting and legal backing for the SeaMonkey Project. " 23:11:57 oerjan: oh. thank's. 23:12:07 FreeFull, but probably not developers 23:12:25 or financial stuff 23:12:51 Used to 23:12:57 true 23:13:13 anyway, doesn't IE put the .NET version in the header too? 23:13:15 or something 23:13:19 I seem to remember that 23:13:29 or was it even in the user agent? 23:13:55 I think it used to but doesn't anymore? 23:13:59 Maybe still does 23:14:30 -!- augur has quit (Remote host closed the connection). 23:15:29 -!- augur has joined. 23:17:22 hm 23:21:45 -!- monqy has joined. 23:39:48 -!- sirdancealo2 has quit (Ping timeout: 264 seconds). 23:42:54 -!- nooga has quit (Ping timeout: 252 seconds). 23:51:39 Bah, it's way too late to listen to SPJ's soothing voice 23:52:11 um bedtime reading 23:52:36 how loudly do you usually listen to SPJ? 23:53:33 -!- sirdancealo2 has joined. 23:56:07 -!- Nisstyre-laptop has joined. 23:56:23 Loud enough for my dad to tell me to turn it off apparently 23:57:05 headbang to SPJ 23:57:25 ^list 23:57:25 Taneb atriq Ngevd Fiora nortti Sgeo ThatOtherPerson alot 23:57:33 -!- Taneb has quit (Quit: Leaving). 23:58:35 -!- azaq23 has quit (Quit: Leaving.).