00:03:40 ̈ 00:04:04 * boily makes weird noises... «ø̈ø̈ø̈ø̈ø̈» 00:05:06 Lilax: what is a zeoul? 00:05:23 The name of my language is rI Pui for the read and print verbs 00:05:39 Its I think 00:05:44 a demon 00:06:23 http://i.imgur.com/Q3Vduhb.png ? 00:07:43 Gasp 00:08:40 -!- Lilax has changed nick to Zuriel. 00:08:54 -!- Zuriel has changed nick to Lilax. 00:08:57 >_> 00:10:59 embrace your demonic self. become one with the hellspawn. enjoy the company of Fungot. 00:11:05 * Lilax saves picture 00:11:12 Nuu not fungot 00:11:13 Lilax: ' then fur ahead where bishop's brook goes under the whole city in a green valley, where the vast gleaming dome and fnord ionic columns of the christian science church beckoned northward. then eight squares past the fine old residence streets broad, washington, lafayette, and adams streets. though these stately old avenues. were fnord and his speech was very curious, an extreme form of yankee dialect i had thought. 00:11:19 holy 00:11:30 not holy, boily :D 00:11:47 ~metar ESSA 00:11:52 @metar ESSA 00:11:52 ESSA 192350Z 03008KT 9999 SCT023 BKN029 M03/M03 Q1023 R01L/910556 R08/910560 R01R/720144 TEMPO BKN012 00:12:14 I should remetasepify the channel one day... 00:12:14 :0 punny 00:12:26 @metar CYUL 00:12:27 CYUL 200000Z 26015G24KT 15SM FEW030 FEW070 FEW240 M07/M11 A2977 RMK SC1AC1CI2 SC TR AC TR SLP083 00:12:28 what's that mean? 00:12:40 current weather for airplane pilots. 00:13:06 no the other thing 00:13:13 remetasepify? 00:13:17 sory 00:13:20 I had a bot. it was called metasepia. 00:13:21 You'll see, in due time 00:13:21 sorry* 00:13:31 >_> 00:13:31 (or now, apparently) 00:13:37 Thas scary 00:13:42 the Second Coming is Nigh! (meaning some time this year, probably.) 00:14:05 and with that, I'm hungry. time to pilfer a pizza or two... 00:14:14 -!- boily has quit (Quit: CALLABLE CHICKEN). 00:14:35 you are so lucky 00:14:46 I wish I could pilfer a pizza 00:14:56 how do I design and implement a multi-language function database without choosing a programming language? 00:32:51 -!- h0rsep0wer has quit (Quit: Leaving). 00:33:41 adu: what do you mean a "function database" 00:34:31 a database that has multiple functions 00:34:59 oren: something maybe half-way between http://rosettacode.org and http://www.krugle.com 00:35:12 or a database that has multiple functions for different languages 00:35:18 idk 00:35:21 Lilax: yes 00:35:32 yas 00:36:44 I've never heard of krugle before 00:37:00 rosettacode is good at the "narrative", but krugle is good at describing existing software 00:37:04 -!- Tritonio has quit (Remote host closed the connection). 00:37:33 Lilax: krugle and code.google.com are about the same, they provide keyword search of a large gamut of software projects 00:37:44 I think github might also provide an inter-project search 00:38:03 oh 00:38:08 ye I see 00:38:43 for example, there are hundreds of implemenations of itoa() 00:39:08 I was thinking of using arch again 00:39:09 and they're all a bit different, there should be one entry on that, like rosettacode, with references to each project/file 00:39:19 I see 00:40:03 but they're not always called "itoa", sometimes they're called "int_to_str", so keyword search sucks on that 01:08:31 -!- Phantom_Hoover has quit (Ping timeout: 255 seconds). 01:32:06 Put esoteric before every thing 01:40:15 -!- shikhin_ has joined. 01:43:51 -!- shikhin has quit (Ping timeout: 264 seconds). 01:56:11 -!- oerjan has joined. 01:58:23 -!- ^v^v has changed nick to ^v. 02:03:22 b_jonas: hi 02:06:33 oerjan: what do you think of goldfire's suggestions on 9858 02:07:15 i think he probably put a "not" where he didn't mean to 02:08:56 i'm just hoping that adding kind information to typerefs won't give too much trouble 02:09:03 *p 02:10:31 or wait, maybe i'm misreading him 02:10:41 he just wants the kinds in a slightly different place 02:16:00 -!- zzo38 has joined. 02:20:33 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)). 02:22:26 -!- GeekDude has joined. 02:36:53 he doesn't want explicit kind information but implicit kind information just because things are parameterized on kinds 02:37:03 only in the polykinded case 02:39:39 so in particular you'd still need to disambiguate T and 'T 02:40:39 -!- augur has quit (Ping timeout: 245 seconds). 02:43:29 "everytime you go to sleep you die, And someone else wakes up in your body thinking they are you" 02:47:03 Lilax: have you been readin SMBC 02:47:07 *reading 02:47:27 No 02:47:35 readin' 02:47:36 there was a comic like that 02:47:54 you said it in a southern accent oerjan 02:48:04 if y'all say so 02:48:15 lol 02:48:22 -!- augur has joined. 02:48:33 Makes no sense only one person said it 02:48:58 -!- contrapumpkin has joined. 02:49:03 actually i've heard there are accents so southern that y'all is singular and you need to say y'all y'all for the plural 02:51:04 -!- copumpkin has quit (Ping timeout: 245 seconds). 02:51:45 -!- ^v has quit (Read error: Connection reset by peer). 02:56:03 -!- ^v has joined. 02:58:42 Hmm? 02:58:51 I was born in teh south 02:58:57 I know what its like 02:59:09 Or atleast my family said y'all as plural 02:59:19 And regular you there for singular 03:03:43 -!- augur has quit (Ping timeout: 245 seconds). 03:10:09 Lilax: i didn't say _all_ southerners did that, just that i've heard rumors of some who do 03:10:33 there's rumors in Norway? 03:10:39 there are** 03:10:46 well i probably read it on the internet hth 03:10:54 Amazing 03:10:58 (probably way back in the 90s, too) 03:11:01 Omfg 03:11:17 so maybe those hillbillies died out in the meantime 03:11:26 Old people are cool 03:11:35 they know things 03:11:45 why thanks 03:11:54 yw 03:12:04 I mean Middle aged 03:12:13 but in perspective to 16 03:12:35 * oerjan waves his Middle Ages halberd at Lilax 03:12:42 44 :0 Gasp that means you lived in the 80's 03:12:48 Cool! 03:13:01 I heard that there are no rumors on IRC 03:13:21 *GASP* 03:13:59 Oh my 03:15:08 i heard that you can beat the 7s master bot these days 03:16:31 If by you you mean the general you, sure 03:16:39 The specific you meaning me cannot as far as me knows 03:16:42 i mean you 03:17:21 It might be true, but I haven't ever checked 03:18:12 7s master bot? 03:18:15 what's that 03:18:54 Prismata AI bot that takes 7 seconds to think, I think 03:19:12 fast 03:19:23 kinda 03:19:42 Well, the other setting for Master Bot is 5s I think 03:20:05 -!- augur has joined. 03:20:23 hi augur 03:22:49 what was Norway like in the 80's 03:22:55 Still cold? 03:30:34 o mai 03:30:53 what a strange place to find myself mentioned 03:31:38 speaking of norway, norwegian beer nørge ø id kind of too smokey fmy tastes 03:36:54 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)). 03:46:37 -!- nys has quit (Quit: s). 03:47:44 Lilax: i vaguely recall the 80s had a lot of rain and snowstorms hth 03:48:10 sometimes at the same time. 03:49:05 and i had to go uphill to school, both ways. 03:49:10 (the hill was in the middle) 03:50:37 someone recommend a cheap 5.1 system with rear wireless 03:50:53 -!- contrapumpkin has changed nick to copumpkin. 03:51:12 quintopia: sometimes it's _so_ nice to be completely unqualified to answer. 03:51:45 -!- MDude has changed nick to MDream. 03:52:04 someone recommend a cheap 5.1 system with rear wireless 03:52:12 wtf 03:52:29 ^echo sometimes it's _so_ nice to be completely unqualified to answer. 03:52:29 sometimes it's _so_ nice to be completely unqualified to answer. sometimes it's _so_ nice to be completely unqualified to answer. 03:53:02 test 03:53:25 test 03:53:27 quintopia: CAN YOU READ THIS 03:53:42 (my hunch is no) 03:54:09 hm ping is fine 03:56:12 oh wait 03:56:31 i was just scrolled up. all the way to the top 03:56:31 Get six cheap systems, cut of nine tenths of one and stick a wireless router on the back. 03:56:38 fancy 03:57:02 *cut off 03:57:16 quintopia: mystery solved 03:57:19 MDream helpful 03:57:27 oerjan hit me with the pan pls 03:57:35 quintopia: if only it was that easy 03:57:46 quintopia: why, i though MDream deserved it more 03:57:49 *+t 03:58:04 i was bejng dumb i think 03:58:22 oerjan: don't i deserve it a little bit 03:58:33 shachaf: extremely hth 03:58:49 by the way, i found a bug: "deriving instance Typeable (GHC.Prim.*)" wants you to turn on NullaryTypeClasses 03:59:17 if we go with goldfire's suggestion, all the kinds will have to get Typeable instances, or something 03:59:17 wait * is an actual identifier now? 03:59:35 * has been a kind for a while hth 03:59:52 well yeah i just didn't know it counted as an identifier 04:00:00 well, you need parentheses here 04:00:05 thought it was too special 04:00:06 it's kind of a bizarre syntax edge case 04:00:19 but _can_ you make typeclass instances for kinds alone? 04:00:33 my vague thought was you'd need to at least wrap it in Proxy 04:00:35 even better, GHC.TypeLits exports a * for Nat multiplication 04:00:58 :k! 2 GHC.TypeLits.* 3 04:01:16 ...they're going to have to find a better system for those syntax distinctions. 04:01:33 scoping has always worked before 04:02:02 it's vaguely irritating that they chose to have (==) be the thing :: k -> k -> Bool rather and used (:~:) for type equality 04:02:13 well, (==) doesn't exist yet, but it presumably will 04:02:20 is it still impossible in head to use (,) prefix, when of kind Constraint -> Constraint -> Constraint ? 04:02:28 Heh ;~; 04:03:18 looks like it 04:03:26 but you can define type P (a::Constraint) b = (a,b) and use P prefix? 04:04:09 shachaf: perhaps they named :~: before they decided to allow type constructor operators not to start with : ? 04:04:27 -!- augur has quit (Ping timeout: 245 seconds). 04:04:43 shachaf: can you? and if so, can you make instances for it? 04:05:03 oerjan: there was a mailing list argument about it before Data.Typeable with (:~:) was released 04:05:14 this is related to an old SO question 04:05:17 but someone really wanted to reserve (==) for Bool 04:05:26 which sort of makes sense, i suppose, give that (<=) and so on exist 04:05:30 but still. (:~:) is awful 04:07:05 -!- augur has joined. 04:08:28 argh i hate when i click to focus and there's accidentally a link there 04:12:07 hmph cannot find it, oh well 04:33:34 someone redirect me to a channel about physics and stuff 05:03:49 ん 05:03:55 -!- AndoDaan has joined. 05:05:13 AndoDaan: did you learn prismata 05:06:52 I did the first 3 tutorials before my laptop started overheating. 05:07:04 yes, it uses 100% cpu on linux flash for some reason 05:07:44 Pretty greedy for what's essentially a card game. 05:09:04 I might give it another go at a later date, try it with another browser. 05:11:38 -!- shikhin_ has quit (Ping timeout: 245 seconds). 05:11:41 `unidecode ん 05:11:54 ​[U+3093 HIRAGANA LETTER N] 05:12:17 what, no syllable? 05:12:42 hm i guess n is syllable-final 05:13:22 it's still a what's-it-called hth 05:13:24 on 05:14:25 it makes me sad that there is no halfwidth ん 05:15:27 There is no halfwidth hiragana in Unicode, only katakana can be half 05:16:11 -!- mbrcknl has joined. 05:16:38 elephants are the Canadians of the animal world 05:16:52 wat 05:17:03 Lilax: How is that? 05:17:18 *mystery* 05:17:46 they both give you donuts 05:18:53 http://m.imgur.com/3KOwIGe 05:18:56 ^ 05:21:04 shachaf: mora? 05:21:23 yes 05:45:41 @tell Sgeo If I had a fridge, I might just buy a bunch of food or something <-- getting by without a fridge in modern society sounds _horribly_ awkward. 05:45:41 Consider it noted. 05:46:18 (before modern society, everything was horribly awkward regardless) 05:49:44 @tell Sgeo by which i mean, unless you're poor as dirt, get one for heaven's sake. 05:49:44 Consider it noted. 05:52:40 oerjan: it would be horribly awkward to get it in here and find space for it. This place is gross 05:52:47 gah 05:52:59 I can't let other people in here 05:53:27 i'd advice you to get a better place to live, but then we're getting into territory i cannot manage myself... 05:53:38 *s 05:54:43 I want to get a professional cleaner in here 05:55:59 but you cannot fit them, right? 05:56:16 * oerjan runs away 05:56:24 oerjan: please advise me to get a better place to live twh 05:56:29 e.g. a place with a window 05:56:38 shachaf: get a better place to live hth 05:56:50 tdh hth 05:56:56 But I don't want to move away from people who recognize me when I eat there everyday 05:56:58 but first i need to figure out where i'm going to live 05:57:00 >.> 05:57:15 Sgeo: hey i resemble that remark 05:58:17 in fact they're probably worried because i haven't been there since saturday 05:58:50 (my sleeping schedule has been going through that phase where i wake up after they close) 05:59:10 The fact that the places close helps keep my sleep schedule resembling some sort of normality 05:59:20 heh 05:59:40 unfortunately, my body insists too strongly on the wrong day length for that to work 06:00:15 although it does help slow the drift down in parts of the cycle 06:01:26 There is one puzzle in this Magic: the Puzzling that involves figuring out the play from one board situation to the next one, assuming that it isn't just a lucky Mana Clash, and assuming it is a Fourth Edition Highlander game. 06:03:00 I could figure out because I have a book with all of the cards up to 1996. 06:04:52 "If I could give this fridge zero stars I would. I am a college student so I needed a small fridge for my room. The milk went bad after 4 days, which is record time. Everything was extremely warm, I think it would have been better to leave my stuff outside in room temperature. I wasn't expecting the fridge to be this bad, specially cuz is $100. So make yourself a favor and DON'T buy this piece of crap." 06:05:57 How much should I blindly trust Amazon reviews? 06:06:06 completely hth 06:08:10 Never blindly trust anyone 06:08:29 I just bought towels based on Amazon reviews. Maybe the towels aren't as great as suggested, but towels can't kill me or anything, right? 06:08:30 unless their name is zzo38 06:08:51 Also I do need new towels 06:08:56 Sgeo: http://www.dailymail.co.uk/health/article-2833074/Forget-door-handles-toilet-seats-germ-infested-objects-home-TOWELS.html 06:09:00 I think my current towels are dead. 06:09:03 blindly trust the daily mail 06:09:07 You should at least read it first! 06:09:45 http://www.webmd.com/sex-relationships/understanding-stds-basics also tells you to be wary of towels 06:09:48 Sgeo: https://www.youtube.com/watch?v=Szc8xHtlCS8 hth 06:10:23 oerjan's link is much better 06:10:25 I thought the towel was going to tilt the chair over 06:15:28 what was that short story where there were aliens that looked to each person like the thing they'd least like to be in contact with? 06:15:45 they looked like a bar of soap, or a razor, or alcohol 06:17:31 aha, http://www.gutenberg.org/files/29601/29601-h/29601-h.htm 06:17:46 i don't remember that but i remember something like the opposite, an alien which trapped people by taking the form they wanted to get in contect with. 06:18:06 it was in the book "50 Short Science Fiction Tales" 06:18:20 oerjan: http://scp-wiki.wikidot.com/scp-523 06:18:22 ? 06:18:24 Blah 06:18:35 http://www.scp-wiki.net/scp-523 06:19:59 definitely not what i read 06:19:59 There are probably similar SCPs 06:20:07 i don't think it was an SCP 06:20:22 also i probably only read a description of the story, not the story itself. 06:20:42 I should probably sleep 06:20:59 i took sleepy medicine that is really anti-anxiety but was prescirbed for sleepytie 06:21:13 anyway they met it in a jungle or something, and its trap was foiled by the people realizing how unlikely it was to find an ice cream bar there, or something like that. 06:24:29 Describe your self with an SCP 06:25:08 http://scifi.stackexchange.com/questions/50918/story-id-astronaut-is-freed-from-mind-parasite-when-he-leaves-earths-gravity-w is another story i remember from that book 06:26:30 omfg 06:26:35 that scp is horrible 06:30:49 -!- vanila has joined. 06:33:32 https://www.reddit.com/r/explainlikeIAmA/comments/1wdup0/explain_the_doctor_like_iama_the_scp_foundation/cf1543u 06:37:02 good morning 06:55:25 -!- AndoDaan_ has joined. 06:55:26 -!- AndoDaan has quit (Read error: Connection reset by peer). 07:04:44 -!- HackEgo has quit (Remote host closed the connection). 07:08:31 -!- chaosagent has quit (Ping timeout: 255 seconds). 07:13:55 -!- ProofTechnique has joined. 07:27:08 -!- adu has quit (Quit: adu). 07:29:42 -!- Patashu has joined. 07:30:23 -!- ProofTechnique has quit (Quit: Textual IRC Client: www.textualapp.com). 07:33:07 -!- Patashu_ has joined. 07:33:08 -!- Patashu has quit (Disconnected by services). 07:35:51 -!- Sprocklem has quit (Ping timeout: 276 seconds). 07:35:58 there's a street in Arizona 07:36:03 Called Bucket of Blood 07:36:24 there is a house in New Orleans 07:36:34 They call the Rising Sun 07:37:21 you did not just.. 07:37:36 of course i did 07:38:01 God dammit, lol 07:39:15 h i all 07:39:18 bored 07:39:32 Delete you OS 07:39:35 and go outside 07:39:43 I kind of wnat to write a blog post about the lambdabot exploti 07:39:52 Or that 07:39:54 I thought about it but there wasn't too much to say 07:40:07 Say lambdabot broke 07:40:16 And that no one fixed it 07:40:26 well it's sandboxed now 07:40:32 Ye 07:41:03 it's just not obvious how to fix it otherwise without disabling too many features 07:41:22 until a real bugfix for ghc comes out 07:41:34 it's a pretty intereting bug 07:42:09 i wonder if just removing IO would fix thi 07:42:11 from lambdabot 07:42:19 PoC please 07:42:38 vanila: doubtful, with unsafeCoerce you can probably do code injection 07:42:54 even if IO is easier 07:43:07 Qfwfq: what 07:43:21 oerjan posted a poc before 07:43:33 * Qfwfq consults scrollback 07:43:40 it wasnt' today 07:43:42 http://oerjan.nvg.org/lbexploits 07:43:51 Thanks. 07:44:09 GHC bug 10000 is relevant 07:44:30 still pretry broken 07:44:36 pretty* 07:44:45 the one numbered 4 is the last one 07:44:51 I see 07:45:04 .org? 07:45:15 oerjanization 07:45:30 There's a 4? 07:45:33 Lilax: nvg.org is basically an alias for nvg.ntnu.no 07:45:41 ah 07:45:45 shachaf: well i just removed a function that was unused from 3 07:45:52 er type 07:45:55 Oh. 07:45:58 Why not call that 3? 07:46:12 shachaf: i didn't want to change a file i'd already linked 07:46:15 You renamed e to e' without changing the version number. 07:46:23 or did you 07:46:23 well ok 07:46:30 i probably did 07:46:48 you should switch to NOINLINE rather than munge imo 07:46:59 hm 07:47:12 probably would even with with -O2 that way 07:47:30 also you should do the type PX = Proxy (Proxy :: * -> *); type PY = Proxy (Proxy :: (* -> *) -> *) thing for clarity 07:48:15 hm let's do that and change Exploit4.hs to it 07:48:17 What is it that failed exactly that NOINLINE and -O2 and those other things to fix it? 07:48:33 also you should make it work without TypeFamilies hth 07:48:35 zzo38: ghc did some strange inlining so it crashed instead 07:48:57 or sometimes printed a completely unrelated number 07:49:14 You should report and/or fix the bug though 07:49:24 I don't know that it's a bug. 07:50:03 It only happens in a case where you have an equality witness for unequal types. 07:51:10 How can you have an equality witness for unequal types? I looked at your file but it doesn't seem to explain everything 07:51:17 yes, so ghc may be doing an entirely sane assumption that just breaks because we're already doing an insane exploit 07:51:35 Anyway, making it NOINLINE works even under O2 07:51:49 Whereas munge doesn't work when compiling with ghc even with O0 07:52:10 And I don't think you can turn NOINLINE off, and relying on it would be silly anyway. 07:52:37 ok now Exploit4.hs has been updated to a cleaner version 07:52:40 zzo38: Proxy (Proxy :: * -> *) and Proxy (Proxy :: (* -> *) -> *) are unequal types (because they have unequal kinds) but they have equal TypeReps. 07:53:12 Then it seem it probably is a bug if they have equal TypeReps despite that. 07:53:21 Yes, it's GHC bug 9858 07:53:30 (and also 10000 but that's a duplicate :'( ) 07:53:48 well it's exactly either, because the types used are different 07:53:56 but it's been reported in the comments there 07:54:02 *not exactly either 07:54:20 Well, yes. 07:54:25 A bug includes its comments. 07:54:28 so it's two slightly different bugs that can be used for the same purpose 07:54:44 goldfire wants to give them two different fixes, too. 07:54:47 shachaf: _maybe_, they sometimes ask you to make a new one... 07:55:24 shachaf: i think in _principle_ you could give a common fix, but that would require including kind information even for monokind typereps 07:55:40 who was the first coder 07:55:41 I think goldfire's proposal isn't unreasonable. 07:55:51 Lilax: lady Ada Lovelace hth 07:56:12 sounds like a pokemon 07:56:18 shachaf: i think we'll just have to wait and see how it actually works 07:56:32 Hmm, what's the easiest way to do damage if you don't have any IO things in scope? 07:56:41 Lilax: what, are you insulting her 07:56:48 no 07:56:50 It's not that easy to just make a ByteString with code that you can jump into, is it? 07:56:54 shachaf: well we already know how to crash ghc without it... 07:56:57 ;-; 07:57:03 Crash GHC, sure, but not arbitrary code. 07:57:09 Another thing I have seen NOINLINE sometimes used for is to make up global variables, and I hate that, because I know another way. 07:57:17 zzo38: What's the another way? 07:57:43 shachaf: well you still have to evade w/e page protection... 07:57:44 oerjan: vaguely surprised that you don't need TypeSynonymInstances for that type instance, actually 07:57:56 oerjan: well, a string literal won't be in writable memory 07:58:01 so that's not a problem 07:58:18 (or maybe it would be a problem) 07:58:21 shachaf: i was too, but maybe it's because it's only an argument, not the actual datatype instanced 07:58:38 what would it mean for it to be the actual datatype instance 07:58:39 One way is for main to hold a value of a "extensible product" type; modules that don't know each other can add fields to it as long as they know the module providing the record type to use. 07:58:53 shachaf: type G = F etc. ... 07:59:22 TSI lets you do instance K A where type F A = ..., where A is a synonym 07:59:26 this looks like the same sort of thing 07:59:28 oh well 07:59:44 But the syntax of Haskell is a bit long to make label types out of, since you both have to define the datatype, the deriving clauses, and any instances 08:00:29 zzo38: Another way is JHC's ACIO. Do you like that way? 08:00:54 I don't know what is that way 08:01:18 http://repetae.net/repos/jhc/lib/jhc/Jhc/ACIO.hs 08:01:22 Although I guess it probably would be better than using NOINLINE and unsafePerformIO 08:02:46 I wanted to use a different haskell compiler than GHC 08:02:46 there arnet many though :( 08:02:46 and the one I tried didn't work 08:03:51 Although it seems better than the NOINLINE and unsafePerformIO way, it still seem worse to me than the way I have made up, however the way I have made up has its own problems too. 08:06:24 i think there is a package providing such an extensible product, although it presumably uses NOINLINE and unsafePerformIO internally 08:07:26 although my memory is too vague 08:08:32 There is one I have written although it doesn't use NOINLINE or unsafePerformIO internally (but it does use unsafeCoerce) 08:08:58 is there a proof it cant be done in haskell 08:09:08 without unsafe 08:09:53 I don't know. 08:10:00 i assume so 08:10:20 I think it's simiilar to ST 08:10:21 you cannot make a top level value that depends on the result of an IO action 08:10:29 I think you can't implement a pure version of ST wihour unsafe 08:11:13 vanila: yeah it requires dependent typing 08:11:46 its interesting that it takes deptypes but has a pure, system F typed interface 08:14:43 Did you know it is possible to run Java programs on a Apple II computer? Apparently it is possible. 08:15:01 wow 08:24:34 -!- MoALTz__ has joined. 08:25:14 oerjan: ok, it's easy enough to get a jump to an arbitrary address 08:26:12 -!- MoALTz__ has quit (Read error: Connection reset by peer). 08:26:13 * oerjan leaves this investigation to people understanding more low-level stuff 08:27:03 -!- MoALTz has joined. 08:27:14 -!- MoALTz_ has quit (Ping timeout: 246 seconds). 08:31:39 night 08:31:44 o/ 08:50:37 hi 08:51:32 b_jonas! 08:51:41 hah hah. http://programming-motherfucker.com/ 08:51:56 b_jonas: thanks for linking that cstheory question the other day 08:52:02 i snagged the bounty! 08:52:13 (didn't completely solve the problem, though) 08:52:19 I've seen you've given a partial answer 08:52:36 (also maybe we should point ais523 there as well) 08:52:54 ca i see the link? 08:53:36 http://cstheory.stackexchange.com/questions/21525/conjecture-about-two-counters-automata 08:53:48 vanila: http://cstheory.stackexchange.com/q/21525/8067 08:53:50 (slow) 09:04:13 -!- shikhin has joined. 09:19:30 morning 09:19:37 J_Arcane: Is that sfw? @programming-motherfucker 09:19:52 mroman: nothing more than some strong language. 09:20:59 good morning 09:42:12 -!- aretecode has quit (Read error: Connection reset by peer). 09:44:35 -!- FreeFull has quit (Ping timeout: 246 seconds). 09:54:59 -!- aretecode has joined. 09:58:39 -!- oerjan has quit (Quit: Wroommmm). 10:00:19 -!- Jander has joined. 10:00:22 Morning all 10:32:17 -!- King2218 has joined. 10:32:24 -!- King2218 has left. 10:35:06 -!- rand_ has joined. 10:35:26 -!- Lilax has quit (Quit: Connection closed for inactivity). 10:36:46 -!- FreeFull has joined. 10:38:17 -!- AndoDaan_ has quit (Read error: Connection reset by peer). 10:38:34 -!- AndoDaan has joined. 10:41:18 -!- blockzombie has joined. 10:51:39 -!- hjulle has joined. 11:00:01 -!- rand_ has quit (Ping timeout: 246 seconds). 11:19:35 -!- boily has joined. 12:09:03 -!- Patashu_ has quit (Ping timeout: 264 seconds). 12:09:29 -!- coppro has quit (Ping timeout: 264 seconds). 12:10:52 -!- coppro has joined. 12:13:39 -!- hjulle has quit (Ping timeout: 252 seconds). 12:14:30 -!- h0rsep0wer has joined. 12:21:00 -!- boily has quit (Quit: SYLLABIC CHICKEN). 12:29:46 -!- AndoDaan has quit (Ping timeout: 265 seconds). 12:40:05 -!- vanila has quit (Quit: Leaving). 13:08:44 -!- blockzombie has quit (Remote host closed the connection). 13:18:11 -!- ski has quit (Ping timeout: 252 seconds). 13:39:52 -!- shikhin_ has joined. 13:43:14 -!- shikhin has quit (Ping timeout: 265 seconds). 13:46:54 [wiki] [[Quantum Dimensions]] http://esolangs.org/w/index.php?diff=41704&oldid=41604 * TomPN * (+18) /* Setup */ 13:46:59 http://mroman.ch/designs/d2/ 13:47:07 this is actually probably the most clean design a website can have 13:47:12 [wiki] [[Quantum Dimensions]] http://esolangs.org/w/index.php?diff=41705&oldid=41704 * TomPN * (-1) /* Qubits */ 13:50:06 and it looks good on smartphone 13:50:15 and can be read on my smartphone without using zoom 13:50:51 I wish I could say that about professional websites made by professional web designers asking for thousands bucks 13:52:32 [wiki] [[Quantum Dimensions]] http://esolangs.org/w/index.php?diff=41706&oldid=41705 * TomPN * (+74) /* Setup */ 13:54:26 some are pretty much unviewable on smartphones without zooming 13:54:44 and the ads get in the way of pretty much anything 13:55:16 frankly my favorite web design I ever did was some old rubbish in bare HTML I wrote when I was barely out of high school. 13:58:50 Websites for smartphones should be designed for 13:59:19 and fuck everybody who does shitty things like body { font-size: 12pt; } 13:59:20 :) 13:59:58 (although I did that in the past. But I notice know how much that sucks) 14:00:26 That site didn't even have CSS. :D 14:02:24 http://mroman.ch/noos/ is probably one of my first designs 14:07:53 -!- h0rsep0wer has quit (Ping timeout: 265 seconds). 14:07:56 this is the second page I ever did. http://web.archive.org/web/20070630035631/http://hedgames.netfirms.com/ 14:08:14 The first was a garish GeoCities monstrosity which has been blissfully lost. 14:12:53 -!- h0rsep0wer has joined. 14:16:27 My most recent site design is not visible anywhere, because I can't be arsed to pay for hosting for what is little more than a gag app. 14:19:29 -!- h0rsep0wer has quit (Ping timeout: 265 seconds). 14:24:48 -!- GeekDude has joined. 14:25:22 -!- oren has quit (Ping timeout: 240 seconds). 14:30:59 -!- h0rsep0wer has joined. 14:31:57 -!- FreeFull has quit (Ping timeout: 245 seconds). 14:37:16 -!- adu has joined. 14:47:37 -!- shikhin_ has changed nick to shikhin. 15:04:24 -!- oren has joined. 15:18:18 -!- `^_^v has joined. 15:18:53 -!- ProofTechnique has joined. 15:23:49 -!- FreeFull has joined. 15:23:51 -!- FreeFull has quit (Changing host). 15:23:51 -!- FreeFull has joined. 15:30:11 -!- Tritonio has joined. 15:45:42 -!- jbkcc has joined. 15:49:13 -!- jbkcc has quit (Client Quit). 15:57:28 -!- adu has quit (Quit: adu). 15:59:55 -!- jbkcc has joined. 16:07:25 -!- ProofTechnique has quit (Quit: Textual IRC Client: www.textualapp.com). 16:07:44 -!- augur has quit (Remote host closed the connection). 16:07:49 -!- ProofTechnique has joined. 16:10:19 -!- Frooxius has quit (Ping timeout: 255 seconds). 16:16:23 -!- h0rsep0wer has quit (Ping timeout: 252 seconds). 16:44:53 -!- h0rsep0wer has joined. 16:51:29 -!- jbkcc has quit (Quit: My Mac has gone to sleep. ZZZzzz…). 16:51:56 -!- oren has quit (Quit: Lost terminal). 16:58:08 hm 16:58:47 If you take f(x)=x^2 and you calculate the difference g(x)=f(x+1)-f(x) 16:58:56 and then h(x)=g(x+1)-g(x) 16:59:03 you'll reach h(x)=2 16:59:17 -!- h0rsep0wer has quit (Ping timeout: 246 seconds). 17:00:13 yes 17:00:17 (which is the same as derive(derive(f)) ) 17:00:33 However, 2^x 17:00:57 2^(x+1) - 2^x = 2^x 17:01:00 so you end up at f again 17:01:18 i.e. for f(x)=2^x -> g(x)=f(x+1)-f(x)=f(x) 17:02:53 -!- h0rsep0wer has joined. 17:02:59 This is the real reason computer scientists use base-2 logarithms 17:03:01 what does this tell me o_O 17:03:59 -!- jbkcc has joined. 17:04:56 http://mathworld.wolfram.com/FiniteDifference.html 17:05:09 mroman: it says that 2 is for finite differences what e is for differentiation 17:05:39 (well, for the forward difference at least) 17:12:12 -!- SopaXorzTaker has joined. 17:16:15 hm 17:16:20 for x^2 it ends up at 2 17:16:23 x^3 at 6 17:16:27 and x^4 at 24 17:16:33 which somehow looks like factorial numbers 17:17:01 that's right 17:17:49 (x+1)^k - x^k = k*x^(k-1) + O(x^(k-2)) 17:26:37 @oeis 1,14,36,24 17:26:39 Triangle of numbers T(n,k) = k!*Stirling2(n,k) read by rows (n >= 1, 1 <= k ... 17:27:21 right again 17:27:37 yeah but this is bad 17:27:46 as I remember from my courses there's no way to calculate Stirling numbers 17:28:00 directly 17:28:06 in a closed formula 17:28:40 (d/dx)^n x^n = n! 17:29:52 The Stirling recurrence is quite nice for computers. 17:31:02 And the mathematicians have done what they usually do when they encounter a function that's useful but has no closed formula: they introduced a notation for it. 17:35:25 Why would you need a closed formula to calculate things 17:37:37 because 17:37:38 also 17:37:44 there's mod complex numbers o_O 17:40:09 Oh mroman will discover Galois theory next! 17:40:15 I should study galois theory 17:40:20 :) 17:40:21 yeah 17:40:43 -!- Lymia has quit (Ping timeout: 252 seconds). 17:43:04 too bad there's no money in that 17:44:17 On the contrary, you can gain many galois connections 17:46:06 is that a math joke? 17:46:15 -!- ocharles_ has changed nick to ocharles. 17:46:23 -!- ocharles has quit (Changing host). 17:46:24 -!- ocharles has joined. 17:46:27 yes, http://galois.com/ is a serious company and a math insider joke 17:47:12 (they seemed to have lost their "connections" though) 17:48:58 (They're also kind of frightening. Their job advertisements usually require that people be able to acquire a security clearance in the US) 17:49:27 they do military stuff 17:49:39 As I said, frightening. 17:49:42 yes 17:49:59 Is there any ethical application of functional programming? ;-) 17:50:18 no 17:50:26 it violates at least two of the Geneva Conventions 17:50:27 makes the "serious international side-effects" unsafePerformIO fireMissiles jokes less funny :( 17:50:34 (Military doesn't qualify, and neither do banks.) 17:52:17 I propose renaming unsafePerformIO to sudo 17:52:58 haha, automatically recording boards lead to some weird effects when games end... 17:53:17 50 Kxf3 exf3 ... where'd the King go?! 17:54:47 (I'm assuming the players started some reviewing right there) 17:55:40 -!- Lymia has joined. 17:55:41 -!- Lymia has quit (Changing host). 17:55:41 -!- Lymia has joined. 17:56:53 int-e: Where does that come from? 17:57:43 zzo38: http://2700chess.com/live - it was the Caruana-Yifan game, but it's already been corrected. 17:57:47 And how is the board automatically recorded? 17:57:53 magnets 17:58:08 (I think) 17:59:56 Yifan accepted a draw when she has mate in 11? 18:01:05 But is there enough time? 18:02:37 oops; was watching a side-variation apparently 18:04:49 -!- Sprocklem has joined. 18:07:25 "Modern, reliable sensor technology recognizes each piece accurately and fast." -- they could be using some RFID technology. 18:08:43 -!- ski has joined. 18:21:24 I believe the main reason they need security clearance is so that they can get contracts that require them to have security clearance 18:21:34 Iknow 18:23:12 -!- Frooxius has joined. 18:28:01 (i.e., military contracts) 18:28:45 "SMACCMPilot is an embedded systems software research project where we are building open-source autopilot software for small unmanned aerial vehicles (UAVs) using new high-assurance software methods." 18:28:53 That kinda thing might have sometihng to do with it. 18:31:10 -!- Tritonio_ has joined. 18:33:39 -!- Tritonio has quit (Ping timeout: 276 seconds). 18:33:40 -!- Tritonio_ has changed nick to Tritonio. 18:33:41 -!- SopaXorzTaker has quit (Remote host closed the connection). 18:41:39 -!- MDream has changed nick to MDude. 18:42:32 -!- arjanb has joined. 18:53:30 int-e: I know a structural engineer back in Finland who really wants a job at Boeing, and the whole security clearance (exclusive to US citizens?) thing makes many of their positions not applicable. 18:55:57 -!- adu has joined. 18:56:27 I have heard of people who aren't US citizens getting a job at Boeing though 18:58:30 Not all of their jobs require a security clearance. But many do. Or so I've heard. 19:00:35 Why? 19:04:57 -!- S1 has joined. 19:10:00 I guess it depends on how closely in the job you would be involved with their projects done for the military? 19:18:37 -!- ais523 has joined. 19:18:46 -!- ais523 has quit (Changing host). 19:18:46 -!- ais523 has joined. 19:34:02 "~'s owner controls you." 19:35:33 I hear even US citizens who are citizens of other countries have trouble with it. 19:40:03 -!- shikhin_ has joined. 19:42:09 -!- S1 has quit (Quit: S1). 19:42:53 -!- shikhin has quit (Ping timeout: 245 seconds). 19:51:59 -!- Froox has joined. 19:53:27 -!- Froox has quit (Client Quit). 19:54:08 -!- Frooxius has quit (Ping timeout: 245 seconds). 19:54:32 -!- jbkcc has quit (Quit: My Mac has gone to sleep. ZZZzzz…). 20:01:20 -!- nys has joined. 20:04:10 -!- shikhin_ has changed nick to shikhin. 20:06:59 -!- Patashu has joined. 20:12:17 -!- augur has joined. 20:20:47 I made up some more Magic: the Gathering cards, even a few of my cards involve old stuff such as shadow and phasing and cumulative upkeep and banding. 20:21:03 `? zzo38mtg 20:21:30 Temporal Shadows (1{W/U/B}) Enchantment - Aura ;; Enchant creature ;; Phasing ;; Enchanted creature gains shadow. 20:24:58 -!- Patashu has quit (Ping timeout: 245 seconds). 20:28:41 In case you need the URL: http://zzo38computer.org/textfile/miscellaneous/magic_card/cards.txt 20:31:04 -!- FreeFull has quit (Ping timeout: 245 seconds). 20:33:03 -!- zzo38 has quit (Remote host closed the connection). 20:33:08 -!- Lymia has quit (Ping timeout: 246 seconds). 20:38:16 -!- augur has quit (Remote host closed the connection). 20:48:42 -!- Lymia has joined. 20:48:46 -!- Lymia has quit (Changing host). 20:48:46 -!- Lymia has joined. 21:00:29 -!- h0rsep0wer has quit (Ping timeout: 264 seconds). 21:02:28 -!- oren has joined. 21:03:22 Merry Christmas 21:23:05 -!- FreeFull has joined. 21:28:05 https://www.youtube.com/watch?v=D5JA8Ytk9EI&list=PL1474DAB09C40D3BA&index=111 21:39:49 ais523: this question about one of those strange exponentially inefficient computing models might or might not interest you: http://cstheory.stackexchange.com/q/21525/ 21:43:50 mroman: happy birthday 21:47:03 christmas?! which calendar's year is ending in 7 days? 21:47:38 (By that calculation, Feb 12 is Chinese Christmas this year...) 21:50:24 *g* 21:50:25 Nice. 21:50:37 mroman: Happy Birthday from me, too. 21:51:37 Or perhaps the 11th. Hmm. 21:54:20 Hm. 21:55:21 (Christmas itself has a somewhat hazy definition. Is it the 24th? the 25th? or does it describe more than one day?) 21:55:22 -!- ProofTechnique has quit (Quit: Textual IRC Client: www.textualapp.com). 22:08:09 Well "christmas day" is the 25th and "christmas eve" the 24th 22:08:47 I mean, even though we only celebrate on the 24th we still use the same nomenclature, so I think I'd put 25th as the "date of christmas" 22:08:47 `2014 22:08:53 :( 22:11:12 for me "christmas" is definitely on christmas eve 22:11:21 christmas day starts the after-christmas 22:13:16 `cat bin/2014 22:13:30 oh. 22:14:24 `echo ? 22:14:55 Oh, not on channel? 22:15:13 -!- Frooxius has joined. 22:15:44 -!- HackEgo has joined. 22:15:46 There we go. 22:15:58 `cat bin/2014 22:16:07 ​#!/bin/sh \ if [ $(date +%Y) = "$(basename "$0")" ] \ then echo "Hello, world!" \ fi 22:16:20 `2015 22:16:22 No output. 22:16:42 `` ls -la bin/2015 22:16:44 ​-rwxr-xr-x 1 5000 0 80 Jan 6 17:40 bin/2015 22:16:58 `cat bin/2015 22:16:59 ​#!/bin/sh \ if [ $(date +%Y) != "$(basename "$0")" ] \ then echo "Hello, world!" \ fi 22:18:21 `run date 22:18:22 Tue Jan 20 22:18:21 UTC 2015 22:18:27 oh damn. 22:19:34 I forgot about the joke. 22:20:08 use data +%G instead of date +%Y for some bonus confusion 22:20:17 `data 22:20:18 ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: data: not found 22:20:36 date 22:21:08 `` date -d '2014-12-30' +'%G %Y' 22:21:09 2015 2014 22:21:47 oh that's the one where Wednesday decides which year the week belongs to? 22:22:12 int-e: As far as we know turning off TypeFamilies doesn't allow you to run arbitrary IO, right? 22:23:27 Ah no, Thursday decides. 22:24:01 shachaf: as far as we know, and there may be "evil" type families ready to exploit in some library already. 22:24:23 Well, no one knows how to do it right now, at least. 22:24:38 (Of course we do know how to crash the program, but that's not so bad.) 22:25:07 I don't, yet. 22:25:25 You can provide broken Ord instances and the like? 22:25:36 How? 22:26:04 But you can do that anyway :) 22:26:20 I just meant crash the program with a GADT. 22:28:16 -!- Phantom_Hoover has joined. 22:33:03 V.y = case V.x of _ [Occ=Dead] { } ... right. 22:33:53 If GHC did a little optimization then you could write unsafeCoerce just like with type families. 22:46:34 -!- augur has joined. 22:55:33 -!- boily has joined. 22:58:04 @metar CYUL 22:58:05 CYUL 202200Z 24015KT 15SM FEW120 M15/M21 A2999 RMK AC1 AC TR SLP160 23:00:35 -!- oerjan has joined. 23:01:42 Well, in approximately the past week I have watched all of Gravity Falls 23:01:51 -!- Lymia has quit (Ping timeout: 264 seconds). 23:03:17 Tanelle! how was it? 23:03:28 hellørjan. how is it? 23:06:09 g'doily. still basking in my bounty. 23:06:18 I really enjoyed it 23:06:39 oerjan, you have a bounty? 23:06:42 What are you wanted for? 23:07:14 oerjan: how much are you worth? 23:07:24 no, i got a bounty, on cstheory.stackexchange. 100 rep. 23:08:59 -!- Lymia has joined. 23:09:00 -!- Lymia has quit (Changing host). 23:09:00 -!- Lymia has joined. 23:10:44 -!- blockzombie has joined. 23:22:46 -!- chaosagent has joined. 23:26:07 (well, for the forward difference at least) <-- a^x - a^(x-1) = a^x has no useful solution :( 23:26:21 oerjan: yes! 23:26:42 oerjan: you discovered the reason why I wrote that... 23:27:15 hm what if you allow more general functions 23:27:33 ...obviously not 23:32:56 -!- adu has quit (Quit: adu). 23:34:42 -!- `^_^v has quit (Ping timeout: 264 seconds). 23:36:47 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)). 23:42:45 shachaf: this works when compiled, http://lpaste.net/3502469903456141312 23:43:06 -!- Lymia has quit (Read error: Connection reset by peer). 23:43:48 int-e: whoa 23:44:12 -!- tangentstorm has joined. 23:44:23 -!- idris-bot has quit (Ping timeout: 240 seconds). 23:44:23 I guess I never bothered checking outside ghci. 23:44:38 Or something. 23:45:42 int-e: you mean it needs major change to work then? 23:46:03 oh wait 23:46:10 you're not using TypeFamilies any more 23:46:30 well, not surprising. 23:46:57 -!- Melvar has quit (Ping timeout: 276 seconds). 23:47:27 are AutoDeriveTypeable and RankNTypes really needed? 23:47:28 Oh, hmm. 23:47:37 (so ghc does that little optimization where it doesn't bother to check the constructor's tag if the pointer is tagged and the type allows only one constructor) 23:47:47 -!- GeekDude has joined. 23:47:56 int-e: Only when compiling, I guess. 23:47:57 oh so for GADTs you _need_ that optimization? 23:48:08 yes. 23:48:14 Actually it looks like int-e did something more complicated than what I did. 23:48:29 ghci crashes gracefuilly complaining about hitting an impossible case. 23:48:32 Maybe that's why his trick works. 23:49:04 Because I just did the direct equivalent of the type family, data F a b p where { A :: a -> F a b PX; B :: b -> F a b PY } 23:49:23 But maybe the way int-e did it it just checks that the value isn't _|_ without actually checking the tag, because it's just being used as an equality proof. 23:49:28 oerjan: I need a typeable instance for Y, of course. The Rank2Types are only needed to get a proper unsafecoerce instead of any special case you might desire. 23:49:46 shachaf: yes, I think so. 23:50:14 -!- blockzombie has quit (Ping timeout: 245 seconds). 23:50:37 Clever. 23:50:40 int-e: in the TypeFamilies version, i managed to avoid deriving Typeable by just applying cast to the predefined :~: type... 23:51:33 and its nested Proxies 23:52:36 one time spj called "gcast Refl" "a ferociously-unintuitive use of 'gcast'" 23:52:42 -!- Melvar has joined. 23:54:43 you're not actually using ST are you 23:55:00 caST hth 23:55:06 oerjan: no, of course not. 23:55:07 http://Hentai.Republican/ 23:55:32 oerjan: I was playing with the idea of just doing unsafePerformUnitIO :: IO () -> () 23:55:45 ok 23:57:15 oerjan: I guess your exploit shows that one can easily use TypeFamilies to lift one inconsistent type cast to arbitrary ones, without having to resort to RankNTypes. They're sort of hidden in the 'supercast' thing. 23:57:40 hm 23:58:15 good name, supercast 23:58:18 oerjan: At least to me, the F seems essential there. 23:58:21 yes but is there anything preventing that from working with the GADT version as well 23:58:45 I called it castAB :: f A -> f B ;-)