00:00:00 <Sgeo> > length $ fix $ take 0
00:01:03 <oerjan> Bike: fix always gives the least fixed point.
00:03:21 -!- tertu has joined.
00:03:22 <oerjan> that's the official haskell report definition of what recursion does.
00:04:09 <Bike> > take 0 undefined
00:05:15 <kmc> the only thing below [] is ⊥, and that isn't a fixed point of (take 0)
00:07:55 <Bike> kmc: yeah, i thought take 0 was strict.
00:08:14 <Sgeo> > take 1 (5:undefined)
00:08:46 <Sgeo> > take 1 (undefined:undefined)
00:09:07 <Sgeo> Is that [undefined] except for failure to show properly?
00:09:31 <Bike> > length take 1 (undefined:undefined)
00:09:32 <lambdabot> Couldn't match expected type ‘a2 -> [a3] -> t’
00:09:32 <lambdabot> with actual type ‘GHC.Types.Int’Couldn't match expected type ‘[a0]’
00:09:32 <lambdabot> with actual type ‘GHC.Types.Int -> [a1] -> [a1]’
00:09:36 <Bike> > length $ take 1 (undefined:undefined)
00:09:43 -!- Sorella has joined.
00:10:32 <Bike> > length (undefined :: [()])
00:10:43 -!- ter2 has joined.
00:10:43 -!- tertu has quit (Disconnected by services).
00:11:22 <oerjan> it's a general rule that f undefined = undefined iff fix f = undefined
00:12:13 <oerjan> also, fix f is the limit of iterate f undefined
00:12:35 <Sgeo> Am I a traitor to Magic if I try Hearthstone?
00:12:35 -!- tertu has joined.
00:12:35 <Taneb> Is it possible to prove the first statement
00:13:08 -!- tertu has quit (Client Quit).
00:13:34 <oerjan> first, if f undefined = undefined then clearly undefined is the least fixpoint, so fix f = undefined
00:13:44 <Bike> the yes was about traitors
00:13:49 <Bike> death to traitors
00:14:37 <oerjan> if f undefined is _not_ undefined, then undefined is not a fixpoint of f at all, so fix f is not undefined.
00:15:06 <oerjan> well fix f is not = undefined.
00:15:38 <oerjan> that fix f is actually defined as anything requires using CPO to prove there's always a least fixpoint.
00:16:38 <oerjan> and that probably involves using that limit of iterate f undefined as a lemma.
00:16:51 * oerjan is a bit vague on that part.
00:16:54 -!- copumpkin has quit (Quit: Textual IRC Client: www.textualapp.com).
00:18:04 -!- copumpkin has joined.
00:25:02 -!- tromp has quit (Remote host closed the connection).
00:25:41 -!- Sprocklem has joined.
00:30:08 -!- shikhout has joined.
00:32:53 -!- shikhin has quit (Ping timeout: 245 seconds).
00:37:16 -!- edwardk has joined.
00:40:26 -!- nooodl has quit (Ping timeout: 252 seconds).
00:42:53 -!- edwardk has quit (Ping timeout: 264 seconds).
00:53:36 <kmc> fungot: Are you happier now that the gods are dying? Or do you dream of Heston with omniscient beard?
00:53:37 <fungot> kmc: 1 egobot: daemon egobot reload a file for os x? i'm trying to
00:54:56 -!- tromp has joined.
00:56:55 <boily> fungot dreams of Dæmon Egobot, Lord of the Tenth Circle of Bothell.
00:56:55 <fungot> boily: hello lord_rob, how is the work of a tortured mind making a single last grasp for a semblance of comforting sanity overlaid upon a fundamentally chaotic at ultimately inimical universe.
00:57:51 <fungot> Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc* iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp youtube
00:58:01 <boily> oh, plenty of new styles!
00:58:11 <oerjan> fungot: stop that, you're ruining boily's sanity project
00:58:11 <fungot> oerjan: only 4 years?!"
00:58:21 <kmc> oh I should ask my information theory question here
00:58:43 <boily> Four Years of Sanity.
00:58:53 <kmc> if you have an accurate model of the noise in a signal, can you insert encrypted messages into that signal in a way that's indistinguishable from more noise if you don't know the key?
00:59:07 <kmc> I think you can and that it would be kind of like spread spectrum CDMA, but I'm not sure
00:59:56 <copumpkin> I would expect so, but can't really justify it
00:59:58 <kmc> I was thinking about hiding data in digital TV transmissions by corrupting MPEG blocks in a way that looks like ordinary broadcast noise
01:00:14 <Bike> so, stenography?
01:00:19 <kmc> steganography
01:00:22 <boily> of course you can. we had a practical exam question once where we had to extract a signal from a post-modern waveform.
01:00:26 <Bike> i hate that word
01:00:49 <kmc> you can definitely insert an "encrypted carrier" by modeling the noise process using, say, a stream cipher as your RNG
01:01:03 <kmc> and the receiver can sync to it by looking for correlations
01:01:04 <fungot> Selected style: oots (Order Of The Stick)
01:01:08 -!- boily has quit (Quit: MATERIAL CHICKEN).
01:01:10 -!- metasepia has quit (Remote host closed the connection).
01:01:36 <kmc> I'm not sure how best to modulate that carrier without changing its statistical properties
01:01:44 <Sgeo> fungot: I like airships
01:01:45 <fungot> Sgeo: a good way, and our little dog, too! neat, having dinner together, and i know that, i'm the most badass halfling ever! in the name of, " it's alive and well, as theological revelations the oracle that. we visited ' im. or ' er, much like this go board and replace it with my little eye... something that the target " hates, fears, or otherwise, there wouldn't that be so lucky. tha way lies madness.
01:01:47 <kmc> but you could at least do simple on-off-keying (where "off" = uncorrelated noise)
01:04:02 <kmc> http://www.arl.army.mil/arlreports/2001/ARL-TR-2433.pdf looks relevant
01:04:10 <kmc> the magic search phrase was "spread spectrum steganography"
01:10:13 -!- Bike_ has joined.
01:11:29 <kmc> anyway I think this should work with any noise you can model accurately
01:11:41 <kmc> hiding messages in markov chain output would be an example
01:11:55 -!- Bike has quit (Ping timeout: 276 seconds).
01:11:59 <Taneb> Hmm, I know the guy who makes King James Programming...
01:12:06 <Taneb> Should I put him touch with MI6?
01:12:50 <kmc> and I think that under standard cryptographic assumptions it would be impossible to detect these signals without knowing the key
01:12:55 <fowl> Taneb, the losethos OS thing?
01:13:00 -!- Bike has joined.
01:13:24 <Taneb> fowl, no, that's unrelated
01:13:45 <fowl> Taneb, some other christian fundamentalist is programming?
01:14:02 <Taneb> fowl, no, it's Markov chain output
01:14:02 <Taneb> http://kingjamesprogramming.tumblr.com/
01:14:14 <Taneb> Seeded with KJV and SICP
01:14:30 <fowl> ive seen this before
01:14:49 -!- Bike_ has quit (Ping timeout: 252 seconds).
01:15:48 <Taneb> "Thy people shall be my people, and Assyria the work of those who contributed to making this a real book, especially Terry Ehling"
01:17:09 <Sprocklem> "you must, at no additional cost, fee or expense to the user, provide a copy, a means of abstraction — that binds a collection of procedures, or a package, and interfaces these to the rest of the acts of Azariah"
01:18:22 <fowl> The garbage collector uses the low-level predicate pointer-to-pair? instead of the list-structure pair? operation because in a real system there might be various things that are in the mountain of Zion
01:19:00 <fowl> haha "Peace and safety; then sudden destruction cometh upon them, as in the metacircular evaluator described in section 5.4.2"
01:19:00 <Sprocklem> "The following random-in-range procedure implements this strategy recursively, walking down the list of names of blasphemy"
01:19:33 <Taneb> Oh yes! Remembered something I was going to ask.
01:19:49 <Taneb> Does anyone know of a dependent type system which included database queries?
01:20:22 -!- ^v has changed nick to \o_yay.
01:21:56 -!- oerjan has quit (Quit: gnite).
01:22:16 <Taneb> Eg "foo : (x : String & age of all records in table 1 with name x < 4)"
01:33:30 <Taneb> Although this ends up awkward in the presence of database mutation (which is somewhat necessary)
01:34:13 <Sgeo> Doesn't Datomic ... somehow incorporate time into things? I remember it was too proprietary for me to want to look too closely
01:34:36 <Bike> Taneb: psh just return a fresh db
01:34:45 <Taneb> And then re-typecheck everything!
01:52:31 -!- Phantom_Hoover has quit (Quit: Leaving).
02:55:17 -!- Sorella has quit (Quit: It is tiem!).
02:56:16 -!- augur has joined.
02:57:04 -!- augur has quit (Remote host closed the connection).
02:58:09 -!- augur has joined.
02:58:43 -!- ter2 has changed nick to tertu.
03:00:49 -!- shikhout has changed nick to shikhin.
03:01:24 -!- shikhin has quit (Quit: Lost terminal).
03:21:16 -!- edwardk has joined.
04:05:41 -!- tromp has quit (Ping timeout: 264 seconds).
04:56:16 -!- shikhin has joined.
04:58:30 -!- MoALTz__ has joined.
05:01:25 -!- MoALTz_ has quit (Ping timeout: 258 seconds).
05:02:11 -!- Sprocklem has quit (Quit: Sleeping).
05:09:29 -!- password2 has joined.
05:17:52 -!- atslash has joined.
05:20:30 -!- atslash has quit (Client Quit).
05:29:47 -!- hk3380 has quit (Ping timeout: 258 seconds).
05:35:58 -!- \o_yay has quit (Quit: http://i.imgur.com/Akc6r.gif).
05:36:19 -!- ^v has joined.
06:12:44 -!- conehead has quit (Quit: Computer has gone to sleep).
06:17:12 -!- MoALTz__ has quit (Quit: bbl).
06:19:21 -!- Bike has quit (Ping timeout: 276 seconds).
06:28:05 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
06:29:19 -!- shikhin has quit (Read error: Connection reset by peer).
06:29:28 -!- shikhin has joined.
06:35:29 -!- password2 has quit (Remote host closed the connection).
06:36:51 -!- hk3380 has joined.
06:39:27 -!- password2 has joined.
06:41:23 -!- drdanmaku has quit (Quit: Connection closed for inactivity).
06:42:30 -!- mtve has joined.
06:52:05 -!- password2 has quit (Remote host closed the connection).
06:52:56 -!- password2 has joined.
07:19:44 -!- tertu has quit (Ping timeout: 255 seconds).
07:22:24 -!- password2 has quit (Ping timeout: 276 seconds).
07:40:53 -!- slereah has joined.
07:40:55 -!- hk3380 has quit (Ping timeout: 252 seconds).
08:18:39 -!- FreeFull has quit.
08:25:47 -!- Patashu has joined.
08:26:05 <kmc> are there esoteric cryptosystems
08:27:59 <slereah> Tattooing your data on the head of a slave
08:29:09 <Jafet> No, only unbreakable 256-bit military grade ones
08:29:47 -!- slereah has left ("Leaving").
08:30:13 <Jafet> (invented independently, of course, not by a military)
08:49:25 -!- Patashu_ has joined.
08:49:25 -!- Patashu has quit (Disconnected by services).
08:52:06 -!- Slereah_ has quit (Ping timeout: 276 seconds).
08:52:45 -!- Slereah_ has joined.
09:06:34 -!- pdxleif has quit (Ping timeout: 240 seconds).
09:09:32 -!- pdxleif has joined.
09:27:22 -!- MindlessDrone has joined.
10:02:58 -!- Slereah_ has quit (Ping timeout: 240 seconds).
10:03:33 -!- Slereah_ has joined.
10:07:57 -!- nucular has joined.
10:07:57 -!- nucular has quit (Changing host).
10:07:57 -!- nucular has joined.
10:16:30 -!- boily has joined.
10:19:35 -!- slereah has joined.
10:22:46 <slereah> The one that only happens for huge amounts of data
10:24:06 <fowl> ahhhhhh ErrorTooMuchData
10:26:02 <slereah> But it gives up on some 200.000 array
10:32:08 <fowl> is there any way that you can use less data?
10:32:19 <slereah> Well I still have to treat them
10:32:39 <slereah> I guess I'll launch Valgrind and go to lunch
10:34:06 -!- Patashu has joined.
10:34:46 -!- oerjan has joined.
10:35:06 -!- Patashu_ has quit (Ping timeout: 240 seconds).
10:39:24 <oerjan> Jafet: good plan. i recall calling out to sort speeded up something i did a _lot_, once. (i don't recall what i was doing, though.)
10:39:40 <oerjan> it's very good at sorting, after all.
10:40:03 <oerjan> (i assume it was gnu sort)
10:40:44 <Jafet> It's not very good at being readable, however
10:40:59 <Jafet> Behold the blob http://git.savannah.gnu.org/gitweb/?p=coreutils.git;a=blob;f=src/sort.c
10:46:02 <oerjan> hm, i think i was sorting a huge file that didn't fit into memory.
10:51:43 -!- Patashu_ has joined.
10:51:43 -!- Patashu has quit (Disconnected by services).
11:01:57 <mroman_> 200k doesn't sound like much
11:02:39 -!- jhj1 has quit (Ping timeout: 265 seconds).
11:03:54 <mroman_> "NapalmV sends this news from the BBC: "The European Union Court of Justice said links to 'irrelevant' and outdated data should be erased on request. The case was brought by a Spanish man who complained that an auction notice of his repossessed home on Google's search results infringed his privacy. Google said the ruling was 'disappointing.'"
11:04:42 -!- nooodl has joined.
11:05:37 <mroman_> it's a legal right to have wrong data or outdated data removed or corrected
11:05:46 <mroman_> in most EU countries at least
11:05:55 -!- boily has quit (Quit: ¨¨¨¨¨¨¨¨).
11:05:55 -!- jhj1 has joined.
11:06:47 <mroman_> theoretically... google isn't even allowed to collect information about me without asking me for permisison to do so
11:07:04 <mroman_> (if google was bound by swiss laws)
11:07:15 <oerjan> yes but it hurts the business model of doing things without a huge human staff.
11:07:26 <oerjan> mroman_: you realize that would have killed the internet, right?
11:08:15 <oerjan> search engines would have been _impossible_ to invent if it required positive action from those indexed.
11:08:43 <mroman_> I don't quiet agree with that.
11:09:03 <mroman_> webmasters could've registered their website for being indexed
11:09:50 <mroman_> they could still index webpages without your permission
11:10:01 <mroman_> because what you publish on your websites is usually considered "public"
11:10:33 <mroman_> what's really illegal is to put all the informtion pieces together to make statements about an individual person
11:11:20 <oerjan> also, this is why robots.txt was invented. he should have been going after the website which publicized him, not google...
11:11:59 <mroman_> but the law shouldn't work like that "unless you say no I'm just gonna do some illegal stuff"
11:12:20 <mroman_> that beats the whole point of privacy imo
11:13:10 <oerjan> yes but for historical reasons search engines _had_ to assume the absense of robots.txt meant consent.
11:13:12 <mroman_> theoretically google has to inform me once they received data about me from a third party
11:13:24 <mroman_> i.e. if someone else said something on some website about me
11:13:39 <mroman_> and google indexed it and analyzed it "deeper" they would have to call me about that ;)
11:13:48 -!- Frooxius has quit (Read error: Connection reset by peer).
11:13:57 <oerjan> yes, theoretically it's impossible to do anything useful without breaking a law hth
11:14:09 <mroman_> however, sending information about my person to foreign countries is actually illegal too
11:14:13 <oerjan> unless you have more lawyers than customers.
11:14:23 <mroman_> so if somebody says something about me on facebook that's already very problematic
11:14:27 -!- Frooxius has joined.
11:14:29 <Jafet> If someone reads something about you anywhere, they are legally obliged to tell you?
11:14:56 <mroman_> Jafet: depends on what they read and what they do with the information
11:15:10 <Taneb> Jafet, i read that u suck
11:15:15 -!- AnotherTest has joined.
11:16:23 <mroman_> otherwise you could say "Well, I didn't collect that information myself"
11:16:24 <Jafet> Taneb: thank you for fulfilling your legal obligation under swiss law
11:16:30 <oerjan> mroman_: so what you're saying is that an actually plausible working internet without having more than the population of earth employed to check everything is illegal in switzerland. gotcha.
11:16:31 <mroman_> and you'd be safe from legal consequences
11:17:09 <mroman_> oerjan: I don't know what your definition of "plausible working internet" is
11:17:15 <mroman_> The internet still works without social media
11:18:13 <mroman_> You are not allowed to make a profile of a person with data you collected from third parties
11:18:24 <mroman_> that doesn't mean social medias are doomed to not exist
11:18:36 <mroman_> it just means that they are not allowed to analyze what people write
11:18:50 <Jafet> No, you are not allowed to. Other people are, because they are not swiss.
11:18:52 <mroman_> if they just "store" the information they are not creating a profile of my person
11:20:11 <mroman_> it still be possible to have social medias and stuff
11:20:48 <mroman_> they might not be free anymore, because they can't make money by shitting on privacy
11:21:13 <mroman_> so they probably have to earn money differently
11:21:24 <Jafet> No, people will not use them and will use the ones that charge no money and shit on privacy.
11:21:36 <Jafet> Especially your privacy.
11:23:21 <mroman_> It's just that I don't really get people complaining about privacy
11:23:45 <mroman_> they complain about it but they still use the free social medias that don't conform to local laws
11:24:12 -!- yorick has joined.
11:24:15 <mroman_> it's not the case that it's impossible to have such social medias, it's just that nobody really actually wants them
11:24:50 <oerjan> this conversation was a bad idea.
11:24:59 <Jafet> I don't really expect anything different from a continent that created browserchoice.eu
11:26:10 <oerjan> because you reminded me that the world sucks, hth
11:27:38 <oerjan> also because headache.
11:29:01 <mroman_> I should probably read about privacy laws in the US :)
11:29:47 <Jafet> Don't worry, it won't take that much time.
11:31:22 <mroman_> "public disclosure of private facts"
11:36:38 <mroman_> is there an official website that documents/publishes laws in the US?
12:02:32 -!- Sgeo has quit (Read error: Connection reset by peer).
12:06:13 -!- Phantom_Hoover has joined.
12:15:03 -!- monotone has quit (Quit: kernel updates).
12:19:01 -!- monotone has joined.
12:33:45 -!- shikhin has quit (Ping timeout: 276 seconds).
12:35:06 -!- shikhin has joined.
12:36:06 <slereah> I wonder how bad gotos really are
12:36:17 <slereah> I think they get a lot of bad rep because of spaghetti code
12:36:20 <fizzie> http://sprunge.us/FaUX man, freenode operators must've done something very personal to this person.
12:36:32 <slereah> But I think people are just afraid to use it nowadays
12:36:56 <slereah> Apparently not enough to use the word FUCK
12:37:10 <slereah> His mama raised him right!
12:38:55 <fizzie> Perhaps it's a case of steganography, and all the numbers encode a hidden message.
12:40:44 <mroman_> slereah: "GOTO considered harmful" considered harmful
12:43:51 <HackEgo> [wiki] [[One]] http://esolangs.org/w/index.php?diff=39515&oldid=39514 * Oerjan * (+30) fmt, sp
12:50:25 <slereah> Is there a general channel for like
12:51:55 <HackEgo> [wiki] [[Talk:Rand.Next()]] http://esolangs.org/w/index.php?diff=39516&oldid=39508 * Oerjan * (+347) unsigned, and No.
12:53:12 <int-e> apparently there's a ##algorithms
12:53:54 -!- AnotherTest has quit (Ping timeout: 276 seconds).
12:54:00 <int-e> with one # even (surprisingly)
12:54:22 <oerjan> must mean knuth owns it.
13:20:04 -!- hk3380 has joined.
13:32:28 -!- drdanmaku has joined.
13:33:28 <FireFly> oerjan: isn't the Perl implementation of CHIQRSX9+ also not Turing-complete by the same reasoning?
13:34:28 -!- FreeFull has joined.
13:40:48 <oerjan> FireFly: indeed. that's part of its purpose.
13:41:28 <oerjan> in fact i considered linking to that
13:43:19 * oerjan notes that he didn't add that article, and his only edit is to adjust the url.
13:45:39 <oerjan> in fact the article was added before i joined the wiki.
13:48:18 -!- Patashu_ has quit (Ping timeout: 240 seconds).
13:52:44 -!- tertu has joined.
14:13:22 -!- Bike has joined.
14:16:52 -!- edwardk_ has joined.
14:20:13 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
14:20:21 -!- edwardk has quit (Ping timeout: 276 seconds).
14:22:00 -!- Phantom_Hoover has joined.
14:41:23 -!- Sprocklem has joined.
15:04:22 -!- oerjan has quit (Quit: leaving).
15:18:53 -!- Bike has quit (Ping timeout: 264 seconds).
15:26:58 -!- Slereah_ has quit (Ping timeout: 240 seconds).
15:32:33 -!- Slereah_ has joined.
15:39:12 -!- password2 has joined.
15:47:15 <mroman_> now I just need to bind type vars to specific types
15:52:27 -!- Bike has joined.
15:57:29 <mroman_> Implementing a type system is easier than I thought
15:58:43 -!- slereah has quit (Quit: Leaving).
16:05:32 -!- ^v has joined.
16:07:33 <mroman_> At least for static typed stack stuff
16:12:32 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
16:17:33 -!- Sprocklem has quit (Ping timeout: 252 seconds).
16:22:41 -!- nucular_ has joined.
16:23:54 -!- Bike has quit (Ping timeout: 240 seconds).
16:26:21 -!- nucular has quit (Ping timeout: 252 seconds).
16:28:29 -!- nucular_ has changed nick to nucular.
16:28:43 -!- nucular has quit (Changing host).
16:28:43 -!- nucular has joined.
16:33:53 -!- TodPunk has quit (Ping timeout: 264 seconds).
16:50:20 -!- Bike has joined.
16:54:53 -!- Bike has quit (Ping timeout: 264 seconds).
16:56:48 -!- shikhin has quit (Remote host closed the connection).
16:57:06 -!- Sprocklem has joined.
16:57:09 -!- hk3380 has quit (Ping timeout: 252 seconds).
17:02:03 -!- TodPunk has joined.
17:24:42 <mroman_> Why does Haskell not allow function overloading?
17:25:03 <mroman_> assuming types don't overlap like pu
17:25:18 <mroman_> foo :: a -> int -> double and bar :: int -> a -> double
17:25:43 <mroman_> currently I'm just picking the first variant I find that typechecks
17:26:20 <myname> well, what for? if it does the same thing but depends on certain properties, make a class
17:26:31 <myname> if it does different stuff, name it differently
17:27:05 <mroman_> Makes sense for Haskell @class
17:27:12 <mroman_> I don't have classes yet :D
17:28:10 <mroman_> I rely on overloading for now I guess
17:28:49 <mroman_> which means that somebody can break all existing pieces of code by defining
17:29:07 <mroman_> because that'd overload pretty much every add variant
17:29:30 <mroman_> I should probably restrict that somehow in the future
17:43:06 -!- Sprocklem has quit (Ping timeout: 258 seconds).
17:43:56 <idris-bot> Data.HVect.index : (i : Fin k) -> HVect ts -> index i ts
17:43:56 <idris-bot> Prelude.List.index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a
17:43:56 <idris-bot> Prelude.Stream.index : Nat -> Stream a -> a
17:43:56 <idris-bot> Prelude.Vect.index : Fin n -> Vect n a -> a
17:44:38 <Melvar> myname: What would you propose for these?
17:45:47 <elliott> Melvar: all of those but Prelude.List.index are special cases of the HVect case
17:45:56 -!- MoALTz has joined.
17:46:36 <Melvar> Vect’s, I suppose, is, but HVect.index uses Vect.index in its type.
17:46:44 <elliott> ok, if you parameterise over the index type too
17:46:55 <elliott> Melvar: what I mean is that you could make a class by tweaking Data.HVect.index's type.
17:47:33 <Melvar> A Stream is infinite and thus any Nat will do, which is not the case for any of the rest …
17:48:21 <elliott> I don't know Idris so this is some kind of frankenstein haskell: class Index seq where type Index seq; type At : Index seq -> Type; index : (idx : Index seq) -> seq -> At idx
17:48:31 <elliott> of course this is ugly. it supports Prelude.List.index too if you make Index a tuple
17:50:53 <Melvar> Doesn’t look like there’d be any chance of inferring things, even if it could be made to work.
17:51:15 <kmc> http://www.openwall.com/lists/oss-security/2014/05/12/3 CVE-2014-0196: Linux kernel pty layer race condition memory corruption
17:53:46 -!- Slereah has joined.
17:54:23 <Melvar> elliott: Btw you overloaded Index there.
17:54:35 <elliott> I said it was frankenstein.
17:56:38 -!- Slereah_ has quit (Ping timeout: 252 seconds).
17:56:41 <idris-bot> Effects.Env.:: : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
17:56:41 <idris-bot> Data.HVect.:: : t -> HVect ts -> HVect (t :: ts)
17:56:42 <idris-bot> Prelude.List.:: : a -> List a -> List a
17:56:42 <idris-bot> Data.Vect.Quantifiers.:: : P x -> All P xs -> All P (x :: xs)
17:56:42 <idris-bot> Prelude.Stream.:: : a -> Lazy' LazyCodata (Stream a) -> Stream a↵…
17:57:31 <Melvar> Prelude.Vect.(::) got cut off.
18:00:32 -!- hk3380 has joined.
18:03:18 <idris-bot> When elaborating an application of constructor __infer:
18:03:18 <idris-bot> Can't disambiguate name: Effects.Env.::, Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.::
18:03:57 <Melvar> Huh, that used to work.
18:07:13 <mroman_> myname: static typed stack-based programming languages
18:10:10 <Melvar> Mh, I guess i since imported Quantifiers and Env.
18:17:34 <mroman_> myname: I can probably even infer types
18:17:48 -!- Slereah_ has joined.
18:17:55 <mroman_> if you have a set of built-ins with explicit type signatures
18:21:23 -!- Slereah has quit (Ping timeout: 252 seconds).
18:33:42 -!- password2 has quit (Ping timeout: 258 seconds).
19:08:29 -!- conehead has joined.
19:08:31 -!- Bike has joined.
19:14:27 <int-e> tromp_: you may enjoy http://int-e.eu/~bf3/tmp/Goodstein.hs (corresponding to a horrible 644 bits implementation of the Goodstein sequence in blc with room for improvement)
19:15:42 <Slereah_> What's a good video to gif converter
19:23:12 <int-e> http://www.imagemagick.org/Usage/video/ perhaps. (Conceptually, to me, ImageMagick is "the right tool for the job")
19:23:33 -!- MindlessDrone has quit (Quit: MindlessDrone).
19:23:36 <int-e> But I'm fairly ignorant about the topic.
19:24:14 <Bike> Slereah_: monotone wrote a walkthrough http://blog.room208.org/post/48793543478
19:33:45 <kmc> hello party people
19:39:07 <Bike> "In the past, Gaussian, Inc. has attracted controversy for its licensing terms that stipulate that researchers who develop competing software packages are not permitted to use the software" science code
19:43:20 <fizzie> Does "Gaussian, Inc." own the patents for the normal distribution?
19:43:56 <tromp_> wow; impressive, int-e!
19:44:39 <Bike> it's a quantum mechanics thing. not sure why it's named after gauss but what isn't
19:44:48 <kmc> "The name originates from Pople's use of Gaussian orbitals to speed up calculations compared to those using Slater-type orbitals"
19:45:05 <kmc> I've used netpbm from shell scripts to do video processing
19:45:12 <kmc> including, like, chroma key
19:45:14 <kmc> and other fancy compositing
19:45:23 <Bike> kmc: i meant the origin of gaussian orbitals
19:46:10 <Bike> i'm full of layers, man
19:52:45 -!- Sprocklem has joined.
19:54:18 <int-e> tromp_: the encoding data O = Zero | Succ O | Limit (Nat -> O) is actually fairly standard, but I took a while to realize two things. First, there is the connection between the 'Limit' constructor and the fundamental sequence as used in the Hardy hierarchy. (The connection from there to the Goodstein sequence is made on Wikipedia). Secondly, doing arithmetic on that representation is actually just a copy of the paper...
19:54:24 <int-e> ...definition. (n + 0 = 0; n + (m + 1) = (n + m) + 1; n + (lim f) = lim (n + f), so that's easy (with some caveats, most notably that w (omega) has a "fundamental sequence" different from 1 + w in that representation. So one has to be careful there.)
19:55:39 <kmc> shachaf: if you call a method fn foo(&'t mut self) -> Bar<'t> then 'self' is borrowed mutably for the duration of 't, regardless of how Bar uses its lifetime parameter
19:55:42 <kmc> v. unfortunate :/
19:56:43 <tromp_> int-e: it's hard to appreciate how much faster goodstein grows than the Ackerman-like g i define, which only takes 47 bits:(
19:58:44 <int-e> tromp_: btw your "g" appears here: https://en.wikipedia.org/wiki/Fast-growing_hierarchy#Definition
20:00:18 <int-e> tromp_: it's also noteworthy that most of the effort is spent on converting the input to its hereditary base 2 representation and the corresponding ordinal. from there to the result it's only 91 bits.
20:02:56 <tromp_> oh, that's so much nicer. should consider that ordinal the starting point then
20:07:24 <int-e> tromp_: That's not entirely fair though, because the ordinals encode the necessary recursive structure. Somewhere in the middel, we could start from the cantor normal form of the heriditary base representation (so just a binary tree, of type: data O = Zero | ExpWPlus O O, encoded as a fold), it's 384 bits.
20:14:13 <tromp_> such a round number...
20:14:31 <tromp_> thx for the link; i included it on my page
20:17:03 -!- Slereah_ has changed nick to Slereah.
20:40:19 -!- nucular has quit (Quit: Switching to phone...).
20:43:49 -!- mhi^ has joined.
20:54:30 -!- Patashu has joined.
21:01:19 <ion> http://youtu.be/HTPOSdyA7Uo http://youtu.be/eKK98MpqujA
21:06:04 -!- lambdabot has quit (Read error: Operation timed out).
21:08:24 -!- oerjan has joined.
21:08:54 -!- cillo has joined.
21:11:56 <oerjan> <mroman_> Implementing a type system is easier than I thought <-- now do inference twh
21:12:55 -!- cillo has quit (Client Quit).
21:20:20 -!- Sprocklem has quit (Ping timeout: 255 seconds).
21:20:22 <oerjan> @tell mroman_ <mroman_> Why does Haskell not allow function overloading? <-- the original invention of type classes was in order to have a more principled way of doing overloading than any other language.
21:20:46 <int-e> oerjan: it'll be back in a moment
21:21:26 <int-e> this is what happened: https://clientarea.ramnode.com/announcements.php?id=352
21:21:53 -!- Patashu has quit (Ping timeout: 252 seconds).
21:22:24 <int-e> seems they took almost 15 minutes.
21:22:48 <int-e> (they company is, that is.)
21:22:49 <oerjan> also, aren't you in germany.
21:23:15 <int-e> but from Germany ...
21:23:42 <oerjan> well your client is in .de
21:23:51 <int-e> ... that's another server ...
21:24:16 <int-e> but it was too weak for lambdabot :)
21:25:06 -!- lambdabot has joined.
21:25:24 <lambdabot> http://hackage.haskell.org/trac/ghc/newticket?type=bug
21:25:43 <oerjan> @tell mroman_ <mroman_> Why does Haskell not allow function overloading? <-- the original invention of type classes was in order to have a more principled way of doing overloading than any other language.
21:26:39 <oerjan> hm that reminds me, i wonder if that bug i reported ever got a response. actually i guess not because i think i registered my email.
21:26:54 -!- Bike has quit (Ping timeout: 240 seconds).
21:29:01 -!- Bike has joined.
21:31:44 <oerjan> as expected, really, it's a you're-doing-it-wrong-but-it-doesn't-really-affect-realistic-programs bug
21:32:31 <int-e> oerjan: actually it's nice to see that a 15 minutes absence of lambdabot is surprising people again, rather than being business as usual. :)
21:35:21 -!- nooodl_ has joined.
21:35:25 <idris-bot> Effects.>>= : Eff m a xs xs' -> ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
21:35:25 <idris-bot> Prelude.Monad.>>= : Monad m => m a -> (a -> m b) -> m b
21:37:35 <oerjan> it's like the added distinctions in dependently typed languages make it too hard to make useful classes for functions that are different versions of the "same" concept...
21:38:41 -!- nooodl has quit (Ping timeout: 264 seconds).
21:38:53 <Melvar> Pretty much, in some cases at least.
21:38:56 <oerjan> (looking also at your index and (::) examples earlier)
21:39:58 <oerjan> i suppose someone needs to invent a more suitable way of abstracting over those differences
21:41:12 <oerjan> hm isn't that among the use cases for ghc's PolyKind and ConstraintKind extensions
21:42:24 <oerjan> but you still need things to fit just right.
21:45:18 <Melvar> ( the (Show Int) %instance
21:45:18 <idris-bot> constructor of Prelude.Show (\{meth0} => prim__toStrInt meth) : Show Int
21:47:10 -!- boily has joined.
21:49:28 -!- metasepia has joined.
21:51:26 <metasepia> CYUL 142121Z 18009G15KT 15SM SCT045 OVC070 23/15 A3008 RMK SC3AC5 SLP187 DENSITY ALT 800FT
21:51:38 <metasepia> ENVA 142120Z 17003KT CAVOK 04/M02 Q1029 RMK WIND 670FT 30003KT
21:52:23 <Melvar> oerjan: “class Finite (n : Nat) t where isoFin : Iso t (Fin n)” is also a thing, outside of the stdlib though.
21:52:44 <boily> you are my DENSITY, DENSITY, DENSITY 君と行ける未来 ♪
21:57:14 <oerjan> int-e: huh, and that goodstein program has no recursion?
21:57:38 <int-e> oerjan: that was the point
22:03:05 <kmc> shachaf: here is a somewhat odd bit of Rust code: for _ in replace(&mut self.roots, vec!()).move_iter().rev() {}
22:09:10 -!- nooodl_ has changed nick to nooodl.
22:13:29 * kmc hands idris-bot some 3,4-methylenedioxymethamphetamine
22:16:43 * boily hands metasepia some organic free-range Himalayan tofu
22:17:05 <boily> kmc: you vile bot drugger! you should feel ashamed!
22:20:18 <oerjan> boily: that's not tofu but rancid butter hth
22:24:33 <oerjan> "According to the Tibetan custom, butter tea is drunk in separate sips, and after each sip the host refills the bowl to the brim. Thus, the guest never drains his bowl; rather, it is constantly topped up. If the visitor does not wish to drink, the best thing to do is leave the tea untouched until the time comes to leave and then drain the bowl. In this way etiquette is observed and the host will not be offended."
22:27:29 <oerjan> "Based-on the principles believed to be at work with the tea, coffee-drinkers have created a coffee version of the beverage."
22:28:00 <boily> I reject your reality and substitue my sane own.
22:29:41 <oerjan> i've tried to reject reality but it's somehow not working properly.
22:32:14 -!- edwardk_ has changed nick to edwardk.
22:32:59 <oerjan> spot the hidden burn "Many different political entities have communities of herders who produce and consume yak's dairy products including cheese and butter – for example, China, India, Mongolia, Nepal, and Tibet."
22:33:27 <Bike> that sounds like a shoddy patch over "countries".
22:33:51 <boily> it's not very hidden... it's more like check-out-that-pulsating-radiating-mesmerizing-glow.
22:35:58 <oerjan> i'm just amazed that it's been there since 2011.
22:36:06 <kmc> wikipedia?
22:36:08 <oerjan> https://en.wikipedia.org/w/index.php?title=Yak_butter&diff=437641611&oldid=437595102
22:36:17 <Bike> it's not inaccurate.
22:36:41 <Bike> nominally, tibet has a good deal of self-governance.
22:36:43 <kmc> that seems less like a deliberate burn and more like an attempt to avoid trouble from chinese nationalist trolls
22:36:49 <Bike> basically that.
22:36:54 <kmc> of which there are many
22:37:15 <kmc> I don't know if the govt has an app to coördinate the trolls like Israel does
22:37:26 <Bike> the usual term for when you want to talk about nations without talking about nations is "culture", though
22:37:40 <oerjan> well i'm just amazed that they haven't removed it _anyhow_. admittedly i didn't check all intervening edits.
22:37:47 <Bike> why would they remove it?
22:37:47 <kmc> yes, there's no reason to mention politics there
22:37:54 <Bike> oh, because they're trolls, you mean
22:39:18 <oerjan> i'd imagine even listing China and Tibet separately under _any_ categorization would be enough to trigger them.
22:39:24 <Bike> yeah i see what you mean
22:39:35 <Bike> maybe chinese nationalists don't care for yak butter
22:40:35 -!- yorick has quit (Remote host closed the connection).
22:43:19 <kmc> well PRC also claims Taiwan and yet puts up with ROC being listed separately in some categorizations, as long as the right words are used
22:43:29 <kmc> e.g. "Chinese Taipei" at the olympics, what a wonderful bit of deliberate ambiguity
22:44:35 <kmc> although Hong Kong has its own Olympic delegation as well
22:45:58 <Bike> i didn't know taiwan even had an olympic team.
22:46:12 <kmc> http://en.wikipedia.org/wiki/Template:Multiple_Olympic_Teams
22:46:28 <Bike> what about macau?
22:46:46 <kmc> they're not members of the IOC but they participate in the Asia Games or something
22:53:21 <kmc> nice! http://rust.godbolt.org/
22:54:58 <Bike> i guess "int x;" isn't legal so i give up
22:55:14 <Taneb> kmc, I like that :)
22:56:00 <kmc> holy shit, people are doing GBA homebrew in Rust: https://github.com/exoticorn/gba-rust
22:56:35 <Bike> what processors does rustc target, anyway
22:59:12 <kmc> there's also a hardware abstraction layer for bare metal ARM: https://github.com/hackndev/zinc
22:59:23 -!- Sorella has joined.
22:59:25 * kmc is reading backlog of This Week in Rust
23:07:51 -!- edwardk has quit (Quit: Computer has gone to sleep.).
23:12:02 -!- Sgeo has joined.
23:16:04 -!- boily has quit (Quit: MERIDIAN CHICKEN).
23:16:06 -!- metasepia has quit (Remote host closed the connection).
23:17:41 -!- hogeyui has quit (Ping timeout: 264 seconds).
23:24:29 <Sgeo> With OOP, if an object has several methods that do the same thing, how is a subclasser supposed to know which one to override to override the others? Is that expected to be part of documentation, or just reading the code?
23:27:12 <fowl> several methods that do the same thing -- code smell
23:27:51 <Sgeo> Seems to happen all the time in Smalltalk
23:27:57 <Bike> sgeo probably means similar-but-a-bit-different things, like a method that writes a description of the object to standard output vs. a method that writes a description of the object on the washington monument
23:28:42 <Sgeo> But the question also kind of extends to Java and actual issues I've encountered, where it seems non-obvious what the mimimal set of methods I need to override to prevent something from happening is
23:29:36 <oerjan> clearly you need to borrow Haskell's new MINIMAL pragma.
23:30:18 <Bike> or have some non virtual methods obviously
23:31:02 <Sgeo> I think this may be subtyping's fault, or something
23:31:38 <Bike> well you can't even state the problem without subtyping.
23:31:52 <Bike> blame smalltalk.
23:32:12 <shachaf> whoever came up with that MINIMAL thing must've been p. great
23:32:28 -!- hogeyui has joined.
23:34:44 <kmc> was it you
23:34:47 <kmc> is that the joke
23:35:10 <oerjan> kmc: hey no fun ruining the joke this soon
23:37:55 <Sgeo> There is the theory of the mobius
23:38:03 -!- nooodl has quit (Ping timeout: 255 seconds).
23:39:04 <Bike> a twist in the fabric of space, where time becomes a loop.
23:39:42 <kmc> > cycle "time becomes a loop. "
23:39:43 <lambdabot> "time becomes a loop. time becomes a loop. time becomes a loop. time becomes...
23:40:43 <Bike> good stopping point.
23:43:00 <Bike> when we reach that point, whatever happened will happen again
23:43:35 <Bike> shachaf will introduce MINIMAL again
23:46:10 <Bike> hm, this paper claims to determine a "word length" for neural information
23:53:18 <fowl> whats neural information
23:53:58 <Taneb> I'm hungry, but it's almost 1 AM
23:54:02 <Taneb> And I don't have any food
23:54:08 <fowl> Taneb, fourth meal
23:55:13 <Bike> fowl: information neurons "send".
23:56:06 <fowl> what lke a float
23:56:55 <Bike> yes. like a float. exactly.
23:57:38 <elliott> are brains IEEE 754 compliant?
23:59:28 <Bike> it actually uses the IBM 7094 format, for compatibility