00:04:04 * boily makes weird noises... «ø̈ø̈ø̈ø̈ø̈»
00:05:06 <boily> Lilax: what is a zeoul?
00:05:23 <oren> The name of my language is rI Pui for the read and print verbs
00:06:23 <boily> http://i.imgur.com/Q3Vduhb.png ?
00:08:40 -!- Lilax has changed nick to Zuriel.
00:08:54 -!- Zuriel has changed nick to Lilax.
00:10:59 <boily> embrace your demonic self. become one with the hellspawn. enjoy the company of Fungot.
00:11:13 <fungot> 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:30 <boily> not holy, boily :D
00:11:52 <lambdabot> ESSA 192350Z 03008KT 9999 SCT023 BKN029 M03/M03 Q1023 R01L/910556 R08/910560 R01R/720144 TEMPO BKN012
00:12:14 <boily> I should remetasepify the channel one day...
00:12:27 <lambdabot> CYUL 200000Z 26015G24KT 15SM FEW030 FEW070 FEW240 M07/M11 A2977 RMK SC1AC1CI2 SC TR AC TR SLP083
00:12:40 <boily> current weather for airplane pilots.
00:13:06 <Lilax> no the other thing
00:13:20 <boily> I had a bot. it was called metasepia.
00:13:42 <boily> the Second Coming is Nigh! (meaning some time this year, probably.)
00:14:05 <boily> and with that, I'm hungry. time to pilfer a pizza or two...
00:14:14 -!- boily has quit (Quit: CALLABLE CHICKEN).
00:14:46 <Lilax> I wish I could pilfer a pizza
00:14:56 <adu> 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 <oren> adu: what do you mean a "function database"
00:34:31 <Lilax> a database that has multiple functions
00:34:59 <adu> oren: something maybe half-way between http://rosettacode.org and http://www.krugle.com
00:35:12 <Lilax> or a database that has multiple functions for different languages
00:35:21 <adu> Lilax: yes
00:36:44 <Lilax> I've never heard of krugle before
00:37:00 <adu> 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 <adu> Lilax: krugle and code.google.com are about the same, they provide keyword search of a large gamut of software projects
00:37:44 <adu> I think github might also provide an inter-project search
00:38:43 <adu> for example, there are hundreds of implemenations of itoa()
00:39:08 <Lilax> I was thinking of using arch again
00:39:09 <adu> and they're all a bit different, there should be one entry on that, like rosettacode, with references to each project/file
00:40:03 <adu> 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 <Lilax> 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:06:33 <shachaf> oerjan: what do you think of goldfire's suggestions on 9858
02:07:15 <oerjan> i think he probably put a "not" where he didn't mean to
02:08:56 <oerjan> i'm just hoping that adding kind information to typerefs won't give too much trouble
02:10:31 <oerjan> or wait, maybe i'm misreading him
02:10:41 <oerjan> 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 <shachaf> he doesn't want explicit kind information but implicit kind information just because things are parameterized on kinds
02:37:03 <shachaf> only in the polykinded case
02:39:39 <shachaf> 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 <Lilax> "everytime you go to sleep you die, And someone else wakes up in your body thinking they are you"
02:47:03 <oerjan> Lilax: have you been readin SMBC
02:47:36 <oerjan> there was a comic like that
02:47:54 <Lilax> you said it in a southern accent oerjan
02:48:22 -!- augur has joined.
02:48:33 <Lilax> Makes no sense only one person said it
02:48:58 -!- contrapumpkin has joined.
02:49:03 <oerjan> 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:51 <Lilax> I was born in teh south
02:58:57 <Lilax> I know what its like
02:59:09 <Lilax> Or atleast my family said y'all as plural
02:59:19 <Lilax> And regular you there for singular
03:03:43 -!- augur has quit (Ping timeout: 245 seconds).
03:10:09 <oerjan> Lilax: i didn't say _all_ southerners did that, just that i've heard rumors of some who do
03:10:33 <Lilax> there's rumors in Norway?
03:10:46 <oerjan> well i probably read it on the internet hth
03:10:58 <oerjan> (probably way back in the 90s, too)
03:11:17 <oerjan> so maybe those hillbillies died out in the meantime
03:11:26 <Lilax> Old people are cool
03:12:04 <Lilax> I mean Middle aged
03:12:13 <Lilax> but in perspective to 16
03:12:35 * oerjan waves his Middle Ages halberd at Lilax
03:12:42 <Lilax> 44 :0 Gasp that means you lived in the 80's
03:13:01 <Sgeo> I heard that there are no rumors on IRC
03:15:08 <shachaf> i heard that you can beat the 7s master bot these days
03:16:31 <Sgeo> If by you you mean the general you, sure
03:16:39 <Sgeo> The specific you meaning me cannot as far as me knows
03:17:21 <Sgeo> It might be true, but I haven't ever checked
03:18:54 <Sgeo> Prismata AI bot that takes 7 seconds to think, I think
03:19:42 <Sgeo> Well, the other setting for Master Bot is 5s I think
03:20:05 -!- augur has joined.
03:22:49 <Lilax> what was Norway like in the 80's
03:30:53 <augur> what a strange place to find myself mentioned
03:31:38 <augur> 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 <oerjan> Lilax: i vaguely recall the 80s had a lot of rain and snowstorms hth
03:48:10 <oerjan> sometimes at the same time.
03:49:05 <oerjan> and i had to go uphill to school, both ways.
03:49:10 <oerjan> (the hill was in the middle)
03:50:37 <quintopia> someone recommend a cheap 5.1 system with rear wireless
03:50:53 -!- contrapumpkin has changed nick to copumpkin.
03:51:12 <oerjan> quintopia: sometimes it's _so_ nice to be completely unqualified to answer.
03:51:45 -!- MDude has changed nick to MDream.
03:52:04 <quintopia> someone recommend a cheap 5.1 system with rear wireless
03:52:29 <oerjan> ^echo sometimes it's _so_ nice to be completely unqualified to answer.
03:52:29 <fungot> sometimes it's _so_ nice to be completely unqualified to answer. sometimes it's _so_ nice to be completely unqualified to answer.
03:53:27 <oerjan> quintopia: CAN YOU READ THIS
03:56:31 <quintopia> i was just scrolled up. all the way to the top
03:56:31 <MDream> Get six cheap systems, cut of nine tenths of one and stick a wireless router on the back.
03:57:35 <shachaf> quintopia: if only it was that easy
03:57:46 <oerjan> quintopia: why, i though MDream deserved it more
03:58:22 <shachaf> oerjan: don't i deserve it a little bit
03:58:33 <oerjan> shachaf: extremely hth
03:58:49 <shachaf> by the way, i found a bug: "deriving instance Typeable (GHC.Prim.*)" wants you to turn on NullaryTypeClasses
03:59:17 <shachaf> if we go with goldfire's suggestion, all the kinds will have to get Typeable instances, or something
03:59:17 <oerjan> wait * is an actual identifier now?
03:59:35 <shachaf> * has been a kind for a while hth
03:59:52 <oerjan> well yeah i just didn't know it counted as an identifier
04:00:00 <shachaf> well, you need parentheses here
04:00:05 <oerjan> thought it was too special
04:00:06 <shachaf> it's kind of a bizarre syntax edge case
04:00:19 <oerjan> but _can_ you make typeclass instances for kinds alone?
04:00:33 <oerjan> my vague thought was you'd need to at least wrap it in Proxy
04:00:35 <shachaf> even better, GHC.TypeLits exports a * for Nat multiplication
04:01:16 <oerjan> ...they're going to have to find a better system for those syntax distinctions.
04:01:33 <shachaf> scoping has always worked before
04:02:02 <shachaf> it's vaguely irritating that they chose to have (==) be the thing :: k -> k -> Bool rather and used (:~:) for type equality
04:02:13 <shachaf> well, (==) doesn't exist yet, but it presumably will
04:02:20 <oerjan> is it still impossible in head to use (,) prefix, when of kind Constraint -> Constraint -> Constraint ?
04:03:26 <shachaf> but you can define type P (a::Constraint) b = (a,b) and use P prefix?
04:04:09 <oerjan> 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 <oerjan> shachaf: can you? and if so, can you make instances for it?
04:05:03 <shachaf> oerjan: there was a mailing list argument about it before Data.Typeable with (:~:) was released
04:05:14 <oerjan> this is related to an old SO question
04:05:17 <shachaf> but someone really wanted to reserve (==) for Bool
04:05:26 <shachaf> which sort of makes sense, i suppose, give that (<=) and so on exist
04:07:05 -!- augur has joined.
04:08:28 <oerjan> argh i hate when i click to focus and there's accidentally a link there
04:12:07 <oerjan> hmph cannot find it, oh well
04:33:34 <Lilax> someone redirect me to a channel about physics and stuff
05:03:55 -!- AndoDaan has joined.
05:05:13 <shachaf> AndoDaan: did you learn prismata
05:06:52 <AndoDaan> I did the first 3 tutorials before my laptop started overheating.
05:07:04 <shachaf> yes, it uses 100% cpu on linux flash for some reason
05:07:44 <AndoDaan> Pretty greedy for what's essentially a card game.
05:09:04 <AndoDaan> 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:54 <HackEgo> [U+3093 HIRAGANA LETTER N]
05:12:42 <oerjan> hm i guess n is syllable-final
05:13:22 <shachaf> it's still a what's-it-called hth
05:14:25 <coppro> it makes me sad that there is no halfwidth ん
05:15:27 <zzo38> There is no halfwidth hiragana in Unicode, only katakana can be half
05:16:11 -!- mbrcknl has joined.
05:16:38 <Lilax> elephants are the Canadians of the animal world
05:17:03 <zzo38> Lilax: How is that?
05:17:46 <myname> they both give you donuts
05:18:53 <Lilax> http://m.imgur.com/3KOwIGe
05:45:41 <oerjan> @tell Sgeo <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:46:18 <oerjan> (before modern society, everything was horribly awkward regardless)
05:49:44 <oerjan> @tell Sgeo by which i mean, unless you're poor as dirt, get one for heaven's sake.
05:52:40 <Sgeo> oerjan: it would be horribly awkward to get it in here and find space for it. This place is gross
05:52:59 <Sgeo> I can't let other people in here
05:53:27 <oerjan> i'd advice you to get a better place to live, but then we're getting into territory i cannot manage myself...
05:54:43 <Sgeo> I want to get a professional cleaner in here
05:55:59 <oerjan> but you cannot fit them, right?
05:56:24 <shachaf> oerjan: please advise me to get a better place to live twh
05:56:29 <shachaf> e.g. a place with a window
05:56:38 <oerjan> shachaf: get a better place to live hth
05:56:56 <Sgeo> But I don't want to move away from people who recognize me when I eat there everyday
05:56:58 <shachaf> but first i need to figure out where i'm going to live
05:57:15 <oerjan> Sgeo: hey i resemble that remark
05:58:17 <oerjan> in fact they're probably worried because i haven't been there since saturday
05:58:50 <oerjan> (my sleeping schedule has been going through that phase where i wake up after they close)
05:59:10 <Sgeo> The fact that the places close helps keep my sleep schedule resembling some sort of normality
05:59:40 <oerjan> unfortunately, my body insists too strongly on the wrong day length for that to work
06:00:15 <oerjan> although it does help slow the drift down in parts of the cycle
06:01:26 <zzo38> 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 <zzo38> I could figure out because I have a book with all of the cards up to 1996.
06:04:52 <Sgeo> "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 <Sgeo> How much should I blindly trust Amazon reviews?
06:08:10 <zzo38> Never blindly trust anyone
06:08:29 <Sgeo> 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 <shachaf> unless their name is zzo38
06:08:51 <Sgeo> Also I do need new towels
06:08:56 <shachaf> Sgeo: http://www.dailymail.co.uk/health/article-2833074/Forget-door-handles-toilet-seats-germ-infested-objects-home-TOWELS.html
06:09:00 <Sgeo> I think my current towels are dead.
06:09:03 <shachaf> blindly trust the daily mail
06:09:07 <zzo38> You should at least read it first!
06:09:45 <shachaf> http://www.webmd.com/sex-relationships/understanding-stds-basics also tells you to be wary of towels
06:09:48 <oerjan> Sgeo: https://www.youtube.com/watch?v=Szc8xHtlCS8 hth
06:10:23 <shachaf> oerjan's link is much better
06:10:25 <Sgeo> I thought the towel was going to tilt the chair over
06:15:28 <shachaf> 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 <shachaf> they looked like a bar of soap, or a razor, or alcohol
06:17:31 <shachaf> aha, http://www.gutenberg.org/files/29601/29601-h/29601-h.htm
06:17:46 <oerjan> 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 <shachaf> it was in the book "50 Short Science Fiction Tales"
06:18:20 <Sgeo> oerjan: http://scp-wiki.wikidot.com/scp-523
06:18:35 <Sgeo> http://www.scp-wiki.net/scp-523
06:19:59 <oerjan> definitely not what i read
06:19:59 <Sgeo> There are probably similar SCPs
06:20:07 <oerjan> i don't think it was an SCP
06:20:22 <oerjan> also i probably only read a description of the story, not the story itself.
06:20:42 <Sgeo> I should probably sleep
06:20:59 <Sgeo> i took sleepy medicine that is really anti-anxiety but was prescirbed for sleepytie
06:21:13 <oerjan> 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 <Lilax> Describe your self with an SCP
06:25:08 <shachaf> 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:35 <Lilax> that scp is horrible
06:30:49 -!- vanila has joined.
06:33:32 <Sgeo> https://www.reddit.com/r/explainlikeIAmA/comments/1wdup0/explain_the_doctor_like_iama_the_scp_foundation/cf1543u
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 <Lilax> there's a street in Arizona
07:36:03 <Lilax> Called Bucket of Blood
07:36:24 <oerjan> there is a house in New Orleans
07:36:34 <oerjan> They call the Rising Sun
07:37:21 <Lilax> you did not just..
07:39:43 <vanila> I kind of wnat to write a blog post about the lambdabot exploti
07:39:54 <vanila> I thought about it but there wasn't too much to say
07:40:07 <Lilax> Say lambdabot broke
07:40:16 <Lilax> And that no one fixed it
07:40:26 <oerjan> well it's sandboxed now
07:41:03 <oerjan> it's just not obvious how to fix it otherwise without disabling too many features
07:41:22 <oerjan> until a real bugfix for ghc comes out
07:41:34 <vanila> it's a pretty intereting bug
07:42:09 <vanila> i wonder if just removing IO would fix thi
07:42:38 <oerjan> vanila: doubtful, with unsafeCoerce you can probably do code injection
07:43:21 <vanila> oerjan posted a poc before
07:43:33 * Qfwfq consults scrollback
07:43:42 <oerjan> http://oerjan.nvg.org/lbexploits
07:44:09 <vanila> GHC bug 10000 is relevant
07:44:30 <Lilax> still pretry broken
07:44:45 <oerjan> the one numbered 4 is the last one
07:45:33 <oerjan> Lilax: nvg.org is basically an alias for nvg.ntnu.no
07:45:45 <oerjan> shachaf: well i just removed a function that was unused from 3
07:46:12 <oerjan> shachaf: i didn't want to change a file i'd already linked
07:46:15 <shachaf> You renamed e to e' without changing the version number.
07:46:48 <shachaf> you should switch to NOINLINE rather than munge imo
07:47:12 <shachaf> probably would even with with -O2 that way
07:47:30 <shachaf> also you should do the type PX = Proxy (Proxy :: * -> *); type PY = Proxy (Proxy :: (* -> *) -> *) thing for clarity
07:48:15 <oerjan> hm let's do that and change Exploit4.hs to it
07:48:17 <zzo38> What is it that failed exactly that NOINLINE and -O2 and those other things to fix it?
07:48:33 <shachaf> also you should make it work without TypeFamilies hth
07:48:35 <oerjan> zzo38: ghc did some strange inlining so it crashed instead
07:48:57 <oerjan> or sometimes printed a completely unrelated number
07:49:14 <zzo38> You should report and/or fix the bug though
07:49:24 <shachaf> I don't know that it's a bug.
07:50:03 <shachaf> It only happens in a case where you have an equality witness for unequal types.
07:51:10 <zzo38> 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 <oerjan> yes, so ghc may be doing an entirely sane assumption that just breaks because we're already doing an insane exploit
07:51:35 <shachaf> Anyway, making it NOINLINE works even under O2
07:51:49 <shachaf> Whereas munge doesn't work when compiling with ghc even with O0
07:52:10 <shachaf> And I don't think you can turn NOINLINE off, and relying on it would be silly anyway.
07:52:37 <oerjan> ok now Exploit4.hs has been updated to a cleaner version
07:52:40 <shachaf> zzo38: Proxy (Proxy :: * -> *) and Proxy (Proxy :: (* -> *) -> *) are unequal types (because they have unequal kinds) but they have equal TypeReps.
07:53:12 <zzo38> Then it seem it probably is a bug if they have equal TypeReps despite that.
07:53:30 <shachaf> (and also 10000 but that's a duplicate :'( )
07:53:48 <oerjan> well it's exactly either, because the types used are different
07:53:56 <oerjan> but it's been reported in the comments there
07:54:25 <shachaf> A bug includes its comments.
07:54:28 <oerjan> so it's two slightly different bugs that can be used for the same purpose
07:54:44 <shachaf> goldfire wants to give them two different fixes, too.
07:54:47 <oerjan> shachaf: _maybe_, they sometimes ask you to make a new one...
07:55:24 <oerjan> 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 <Lilax> who was the first coder
07:55:41 <shachaf> I think goldfire's proposal isn't unreasonable.
07:55:51 <oerjan> Lilax: lady Ada Lovelace hth
07:56:12 <Lilax> sounds like a pokemon
07:56:18 <oerjan> shachaf: i think we'll just have to wait and see how it actually works
07:56:32 <shachaf> Hmm, what's the easiest way to do damage if you don't have any IO things in scope?
07:56:41 <oerjan> Lilax: what, are you insulting her
07:56:50 <shachaf> It's not that easy to just make a ByteString with code that you can jump into, is it?
07:56:54 <oerjan> shachaf: well we already know how to crash ghc without it...
07:57:03 <shachaf> Crash GHC, sure, but not arbitrary code.
07:57:09 <zzo38> 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 <shachaf> zzo38: What's the another way?
07:57:43 <oerjan> shachaf: well you still have to evade w/e page protection...
07:57:44 <shachaf> oerjan: vaguely surprised that you don't need TypeSynonymInstances for that type instance, actually
07:57:56 <shachaf> oerjan: well, a string literal won't be in writable memory
07:58:18 <shachaf> (or maybe it would be a problem)
07:58:21 <oerjan> shachaf: i was too, but maybe it's because it's only an argument, not the actual datatype instanced
07:58:38 <shachaf> what would it mean for it to be the actual datatype instance
07:58:39 <zzo38> 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 <oerjan> shachaf: type G = F etc. ...
07:59:22 <shachaf> TSI lets you do instance K A where type F A = ..., where A is a synonym
07:59:26 <shachaf> this looks like the same sort of thing
07:59:44 <zzo38> 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 <shachaf> zzo38: Another way is JHC's ACIO. Do you like that way?
08:00:54 <zzo38> I don't know what is that way
08:01:18 <shachaf> http://repetae.net/repos/jhc/lib/jhc/Jhc/ACIO.hs
08:01:22 <zzo38> Although I guess it probably would be better than using NOINLINE and unsafePerformIO
08:02:46 <vanila> I wanted to use a different haskell compiler than GHC
08:02:46 <vanila> there arnet many though :(
08:02:46 <vanila> and the one I tried didn't work
08:03:51 <zzo38> 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 <oerjan> i think there is a package providing such an extensible product, although it presumably uses NOINLINE and unsafePerformIO internally
08:07:26 <oerjan> although my memory is too vague
08:08:32 <zzo38> There is one I have written although it doesn't use NOINLINE or unsafePerformIO internally (but it does use unsafeCoerce)
08:08:58 <vanila> is there a proof it cant be done in haskell
08:10:20 <vanila> I think it's simiilar to ST
08:10:21 <oerjan> you cannot make a top level value that depends on the result of an IO action
08:10:29 <vanila> I think you can't implement a pure version of ST wihour unsafe
08:11:13 <oerjan> vanila: yeah it requires dependent typing
08:11:46 <vanila> its interesting that it takes deptypes but has a pure, system F typed interface
08:14:43 <zzo38> Did you know it is possible to run Java programs on a Apple II computer? Apparently it is possible.
08:24:34 -!- MoALTz__ has joined.
08:25:14 <shachaf> 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:51:41 <J_Arcane> hah hah. http://programming-motherfucker.com/
08:51:56 <oerjan> b_jonas: thanks for linking that cstheory question the other day
08:52:13 <oerjan> (didn't completely solve the problem, though)
08:52:19 <b_jonas> I've seen you've given a partial answer
08:52:36 <b_jonas> (also maybe we should point ais523 there as well)
08:53:36 <oerjan> http://cstheory.stackexchange.com/questions/21525/conjecture-about-two-counters-automata
08:53:48 <b_jonas> vanila: http://cstheory.stackexchange.com/q/21525/8067
09:04:13 -!- shikhin has joined.
09:19:37 <mroman> J_Arcane: Is that sfw? @programming-motherfucker
09:19:52 <J_Arcane> mroman: nothing more than some strong language.
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: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 <HackEgo> [wiki] [[Quantum Dimensions]] http://esolangs.org/w/index.php?diff=41704&oldid=41604 * TomPN * (+18) /* Setup */
13:46:59 <mroman> http://mroman.ch/designs/d2/
13:47:07 <mroman> this is actually probably the most clean design a website can have
13:47:12 <HackEgo> [wiki] [[Quantum Dimensions]] http://esolangs.org/w/index.php?diff=41705&oldid=41704 * TomPN * (-1) /* Qubits */
13:50:06 <mroman> and it looks good on smartphone
13:50:15 <mroman> and can be read on my smartphone without using zoom
13:50:51 <mroman> I wish I could say that about professional websites made by professional web designers asking for thousands bucks
13:52:32 <HackEgo> [wiki] [[Quantum Dimensions]] http://esolangs.org/w/index.php?diff=41706&oldid=41705 * TomPN * (+74) /* Setup */
13:54:26 <mroman> some are pretty much unviewable on smartphones without zooming
13:54:44 <mroman> and the ads get in the way of pretty much anything
13:55:16 <J_Arcane> 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 <mroman> Websites for smartphones should be designed for <meta name="viewport" content="width=device-width, initial-scale=1">
13:59:19 <mroman> and fuck everybody who does shitty things like body { font-size: 12pt; }
13:59:58 <mroman> (although I did that in the past. But I notice know how much that sucks)
14:00:26 <J_Arcane> That site didn't even have CSS. :D
14:02:24 <mroman> http://mroman.ch/noos/ is probably one of my first designs
14:07:53 -!- h0rsep0wer has quit (Ping timeout: 265 seconds).
14:07:56 <J_Arcane> this is the second page I ever did. http://web.archive.org/web/20070630035631/http://hedgames.netfirms.com/
14:08:14 <J_Arcane> The first was a garish GeoCities monstrosity which has been blissfully lost.
14:12:53 -!- h0rsep0wer has joined.
14:16:27 <J_Arcane> 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:47 <mroman> If you take f(x)=x^2 and you calculate the difference g(x)=f(x+1)-f(x)
16:58:56 <mroman> and then h(x)=g(x+1)-g(x)
16:59:17 -!- h0rsep0wer has quit (Ping timeout: 246 seconds).
17:00:17 <mroman> (which is the same as derive(derive(f)) )
17:01:00 <mroman> so you end up at f again
17:01:18 <mroman> 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 <Jafet> This is the real reason computer scientists use base-2 logarithms
17:03:01 <mroman> what does this tell me o_O
17:03:59 -!- jbkcc has joined.
17:04:56 <int-e> http://mathworld.wolfram.com/FiniteDifference.html
17:05:09 <int-e> mroman: it says that 2 is for finite differences what e is for differentiation
17:05:39 <int-e> (well, for the forward difference at least)
17:12:12 -!- SopaXorzTaker has joined.
17:16:20 <mroman> for x^2 it ends up at 2
17:16:33 <mroman> which somehow looks like factorial numbers
17:17:49 <int-e> (x+1)^k - x^k = k*x^(k-1) + O(x^(k-2))
17:26:39 <lambdabot> Triangle of numbers T(n,k) = k!*Stirling2(n,k) read by rows (n >= 1, 1 <= k ...
17:27:46 <mroman> as I remember from my courses there's no way to calculate Stirling numbers
17:29:52 <int-e> The Stirling recurrence is quite nice for computers.
17:31:02 <int-e> 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 <Jafet> Why would you need a closed formula to calculate things
17:37:44 <mroman> there's mod complex numbers o_O
17:40:09 <int-e> Oh mroman will discover Galois theory next!
17:40:15 <mroman> I should study galois theory
17:40:43 -!- Lymia has quit (Ping timeout: 252 seconds).
17:43:04 <mroman> too bad there's no money in that
17:44:17 <Jafet> On the contrary, you can gain many galois connections
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 <int-e> yes, http://galois.com/ is a serious company and a math insider joke
17:47:12 <int-e> (they seemed to have lost their "connections" though)
17:48:58 <int-e> (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:39 <int-e> As I said, frightening.
17:49:59 <int-e> Is there any ethical application of functional programming? ;-)
17:50:26 <coppro> it violates at least two of the Geneva Conventions
17:50:27 <elliott> makes the "serious international side-effects" unsafePerformIO fireMissiles jokes less funny :(
17:50:34 <int-e> (Military doesn't qualify, and neither do banks.)
17:52:17 <mroman> I propose renaming unsafePerformIO to sudo
17:52:58 <int-e> haha, automatically recording boards lead to some weird effects when games end...
17:53:17 <int-e> 50 Kxf3 exf3 ... where'd the King go?!
17:54:47 <int-e> (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 <zzo38> int-e: Where does that come from?
17:57:43 <int-e> zzo38: http://2700chess.com/live - it was the Caruana-Yifan game, but it's already been corrected.
17:57:47 <zzo38> And how is the board automatically recorded?
17:59:56 <tromp> Yifan accepted a draw when she has mate in 11?
18:01:05 <zzo38> But is there enough time?
18:02:37 <tromp> oops; was watching a side-variation apparently
18:04:49 -!- Sprocklem has joined.
18:07:25 <int-e> "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 <Jafet> I believe the main reason they need security clearance is so that they can get contracts that require them to have security clearance
18:23:12 -!- Frooxius has joined.
18:28:01 <elliott> (i.e., military contracts)
18:28:45 <J_Arcane> "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 <J_Arcane> 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 <fizzie> 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 <zzo38> I have heard of people who aren't US citizens getting a job at Boeing though
18:58:30 <fizzie> Not all of their jobs require a security clearance. But many do. Or so I've heard.
19:04:57 -!- S1 has joined.
19:10:00 <fizzie> 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 <zzo38> "~'s owner controls you."
19:35:33 <shachaf> 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 <zzo38> 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:30 <zzo38> 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 <zzo38> 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:23:05 -!- FreeFull has joined.
21:28:05 <APic> https://www.youtube.com/watch?v=D5JA8Ytk9EI&list=PL1474DAB09C40D3BA&index=111
21:39:49 <b_jonas> 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:47:03 <int-e> christmas?! which calendar's year is ending in 7 days?
21:47:38 <int-e> (By that calculation, Feb 12 is Chinese Christmas this year...)
21:50:37 <APic> mroman: Happy Birthday from me, too.
21:51:37 <int-e> Or perhaps the 11th. Hmm.
21:55:21 <int-e> (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 <FireFly> Well "christmas day" is the 25th and "christmas eve" the 24th
22:08:47 <FireFly> 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:11:12 <olsner> for me "christmas" is definitely on christmas eve
22:11:21 <olsner> christmas day starts the after-christmas
22:15:13 -!- Frooxius has joined.
22:15:44 -!- HackEgo has joined.
22:16:07 <HackEgo> #!/bin/sh \ if [ $(date +%Y) = "$(basename "$0")" ] \ then echo "Hello, world!" \ fi
22:16:42 <int-e> `` ls -la bin/2015
22:16:44 <HackEgo> -rwxr-xr-x 1 5000 0 80 Jan 6 17:40 bin/2015
22:16:59 <HackEgo> #!/bin/sh \ if [ $(date +%Y) != "$(basename "$0")" ] \ then echo "Hello, world!" \ fi
22:18:22 <HackEgo> Tue Jan 20 22:18:21 UTC 2015
22:19:34 <int-e> I forgot about the joke.
22:20:08 <shachaf> use data +%G instead of date +%Y for some bonus confusion
22:20:18 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: data: not found
22:21:08 <shachaf> `` date -d '2014-12-30' +'%G %Y'
22:21:47 <int-e> oh that's the one where Wednesday decides which year the week belongs to?
22:22:12 <shachaf> int-e: As far as we know turning off TypeFamilies doesn't allow you to run arbitrary IO, right?
22:23:27 <int-e> Ah no, Thursday decides.
22:24:01 <int-e> shachaf: as far as we know, and there may be "evil" type families ready to exploit in some library already.
22:24:23 <shachaf> Well, no one knows how to do it right now, at least.
22:24:38 <shachaf> (Of course we do know how to crash the program, but that's not so bad.)
22:25:25 <int-e> You can provide broken Ord instances and the like?
22:26:04 <int-e> But you can do that anyway :)
22:26:20 <shachaf> I just meant crash the program with a GADT.
22:28:16 -!- Phantom_Hoover has joined.
22:33:03 <int-e> V.y = case V.x of _ [Occ=Dead] { } ... right.
22:33:53 <shachaf> 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:05 <lambdabot> CYUL 202200Z 24015KT 15SM FEW120 M15/M21 A2999 RMK AC1 AC TR SLP160
23:00:35 -!- oerjan has joined.
23:01:42 <Taneb> 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 <boily> Tanelle! how was it?
23:03:28 <boily> hellørjan. how is it?
23:06:09 <oerjan> g'doily. still basking in my bounty.
23:06:18 <Taneb> I really enjoyed it
23:06:39 <Taneb> oerjan, you have a bounty?
23:06:42 <Taneb> What are you wanted for?
23:07:14 <boily> oerjan: how much are you worth?
23:07:24 <oerjan> 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 <oerjan> <int-e> (well, for the forward difference at least) <-- a^x - a^(x-1) = a^x has no useful solution :(
23:26:42 <int-e> oerjan: you discovered the reason why I wrote that...
23:27:15 <oerjan> hm what if you allow more general functions
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 <int-e> shachaf: this works when compiled, http://lpaste.net/3502469903456141312
23:43:06 -!- Lymia has quit (Read error: Connection reset by peer).
23:44:12 -!- tangentstorm has joined.
23:44:23 -!- idris-bot has quit (Ping timeout: 240 seconds).
23:44:23 <shachaf> I guess I never bothered checking outside ghci.
23:45:42 <oerjan> int-e: you mean it needs major change to work then?
23:46:10 <oerjan> you're not using TypeFamilies any more
23:46:57 -!- Melvar has quit (Ping timeout: 276 seconds).
23:47:27 <oerjan> are AutoDeriveTypeable and RankNTypes really needed?
23:47:37 <int-e> (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 <shachaf> int-e: Only when compiling, I guess.
23:47:57 <oerjan> oh so for GADTs you _need_ that optimization?
23:48:14 <shachaf> Actually it looks like int-e did something more complicated than what I did.
23:48:29 <int-e> ghci crashes gracefuilly complaining about hitting an impossible case.
23:48:32 <shachaf> Maybe that's why his trick works.
23:49:04 <shachaf> 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 <shachaf> 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 <int-e> 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 <int-e> shachaf: yes, I think so.
23:50:14 -!- blockzombie has quit (Ping timeout: 245 seconds).
23:50:40 <oerjan> int-e: in the TypeFamilies version, i managed to avoid deriving Typeable by just applying cast to the predefined :~: type...
23:51:33 <oerjan> and its nested Proxies
23:52:36 <shachaf> one time spj called "gcast Refl" "a ferociously-unintuitive use of 'gcast'"
23:52:42 -!- Melvar has joined.
23:54:43 <oerjan> you're not actually using ST are you
23:55:06 <int-e> oerjan: no, of course not.
23:55:07 <APic> http://Hentai.Republican/
23:55:32 <int-e> oerjan: I was playing with the idea of just doing unsafePerformUnitIO :: IO () -> ()
23:57:15 <int-e> 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:58:18 <int-e> oerjan: At least to me, the F seems essential there.
23:58:21 <oerjan> yes but is there anything preventing that from working with the GADT version as well
23:58:45 <int-e> I called it castAB :: f A -> f B ;-)