00:00:00 > length $ fix $ take 0 00:00:02 0 00:00:26 That is great 00:01:03 Bike: fix always gives the least fixed point. 00:03:21 -!- tertu has joined. 00:03:22 that's the official haskell report definition of what recursion does. 00:04:09 > take 0 undefined 00:04:11 [] 00:04:14 oh. 00:05:15 the only thing below [] is ⊥, and that isn't a fixed point of (take 0) 00:07:31 > fix (1*) 00:07:35 mueval-core: Time limit exceeded 00:07:55 kmc: yeah, i thought take 0 was strict. 00:08:14 > take 1 (5:undefined) 00:08:15 [5] 00:08:38 hmm 00:08:46 > take 1 (undefined:undefined) 00:08:47 [*Exception: Prelude.undefined 00:09:07 Is that [undefined] except for failure to show properly? 00:09:24 well le't see 00:09:31 > length take 1 (undefined:undefined) 00:09:32 Couldn't match expected type ‘a2 -> [a3] -> t’ 00:09:32 with actual type ‘GHC.Types.Int’Couldn't match expected type ‘[a0]’ 00:09:32 with actual type ‘GHC.Types.Int -> [a1] -> [a1]’ 00:09:36 > length $ take 1 (undefined:undefined) 00:09:38 1 00:09:42 yep 00:09:43 -!- Sorella has joined. 00:10:13 > undefined :: [()] 00:10:14 *Exception: Prelude.undefined 00:10:32 > length (undefined :: [()]) 00:10:33 *Exception: Prelude.undefined 00:10:43 -!- ter2 has joined. 00:10:43 -!- tertu has quit (Disconnected by services). 00:11:22 it's a general rule that f undefined = undefined iff fix f = undefined 00:12:13 also, fix f is the limit of iterate f undefined 00:12:35 Am I a traitor to Magic if I try Hearthstone? 00:12:35 -!- tertu has joined. 00:12:35 Is it possible to prove the first statement 00:12:40 yes 00:13:08 -!- tertu has quit (Client Quit). 00:13:34 first, if f undefined = undefined then clearly undefined is the least fixpoint, so fix f = undefined 00:13:44 the yes was about traitors 00:13:49 death to traitors 00:14:37 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 well fix f is not = undefined. 00:15:38 that fix f is actually defined as anything requires using CPO to prove there's always a least fixpoint. 00:15:58 boring 00:16:38 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 fungot: Are you happier now that the gods are dying? Or do you dream of Heston with omniscient beard? 00:53:37 kmc: 1 egobot: daemon egobot reload a file for os x? i'm trying to 00:54:56 -!- tromp has joined. 00:56:55 fungot dreams of Dæmon Egobot, Lord of the Tenth Circle of Bothell. 00:56:55 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:50 ^style 00:57:51 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 oh, plenty of new styles! 00:58:11 fungot: stop that, you're ruining boily's sanity project 00:58:11 oerjan: only 4 years?!" 00:58:21 oh I should ask my information theory question here 00:58:43 Four Years of Sanity. 00:58:53 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 I think you can and that it would be kind of like spread spectrum CDMA, but I'm not sure 00:59:56 I would expect so, but can't really justify it 00:59:58 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 so, stenography? 01:00:19 steganography 01:00:22 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:24 right 01:00:26 i hate that word 01:00:49 you can definitely insert an "encrypted carrier" by modeling the noise process using, say, a stream cipher as your RNG 01:01:03 and the receiver can sync to it by looking for correlations 01:01:04 ^style oots 01:01:04 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 I'm not sure how best to modulate that carrier without changing its statistical properties 01:01:44 fungot: I like airships 01:01:45 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 but you could at least do simple on-off-keying (where "off" = uncorrelated noise) 01:04:02 http://www.arl.army.mil/arlreports/2001/ARL-TR-2433.pdf looks relevant 01:04:10 the magic search phrase was "spread spectrum steganography" 01:10:13 -!- Bike_ has joined. 01:11:29 anyway I think this should work with any noise you can model accurately 01:11:41 hiding messages in markov chain output would be an example 01:11:55 -!- Bike has quit (Ping timeout: 276 seconds). 01:11:59 Hmm, I know the guy who makes King James Programming... 01:12:06 Should I put him touch with MI6? 01:12:15 :D 01:12:50 and I think that under standard cryptographic assumptions it would be impossible to detect these signals without knowing the key 01:12:55 Taneb, the losethos OS thing? 01:13:00 -!- Bike has joined. 01:13:24 fowl, no, that's unrelated 01:13:45 Taneb, some other christian fundamentalist is programming? 01:14:02 fowl, no, it's Markov chain output 01:14:02 http://kingjamesprogramming.tumblr.com/ 01:14:14 Seeded with KJV and SICP 01:14:17 oh 01:14:30 ive seen this before 01:14:49 -!- Bike_ has quit (Ping timeout: 252 seconds). 01:15:48 "Thy people shall be my people, and Assyria the work of those who contributed to making this a real book, especially Terry Ehling" 01:16:39 lol 01:17:09 "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 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 haha "Peace and safety; then sudden destruction cometh upon them, as in the metacircular evaluator described in section 5.4.2" 01:19:00 "The following random-in-range procedure implements this strategy recursively, walking down the list of names of blasphemy" 01:19:33 Oh yes! Remembered something I was going to ask. 01:19:49 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 Eg "foo : (x : String & age of all records in table 1 with name x < 4)" 01:33:30 Although this ends up awkward in the presence of database mutation (which is somewhat necessary) 01:34:13 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 Taneb: psh just return a fresh db 01:34:45 And then re-typecheck everything! 01:34:59 damn right. 01:36:24 Anyway, goodnight 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 are there esoteric cryptosystems 08:27:59 Tattooing your data on the head of a slave 08:29:09 No, only unbreakable 256-bit military grade ones 08:29:47 -!- slereah has left ("Leaving"). 08:30:13 (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:19:37 Hello 10:19:57 Hi, slereah 10:22:38 Bleh, the worst error 10:22:46 The one that only happens for huge amounts of data 10:24:06 ahhhhhh ErrorTooMuchData 10:25:32 I know! 10:25:48 Its just a quicksort :( 10:26:02 But it gives up on some 200.000 array 10:30:55 Hm, what to do 10:31:00 I fear using Valgrind 10:32:08 is there any way that you can use less data? 10:32:19 Well I still have to treat them 10:32:39 I guess I'll launch Valgrind and go to lunch 10:33:44 execvp("sort" 10:34:06 -!- Patashu has joined. 10:34:46 -!- oerjan has joined. 10:35:06 -!- Patashu_ has quit (Ping timeout: 240 seconds). 10:38:28 :-o 10:39:24 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 it's very good at sorting, after all. 10:40:03 (i assume it was gnu sort) 10:40:44 It's not very good at being readable, however 10:40:59 Behold the blob http://git.savannah.gnu.org/gitweb/?p=coreutils.git;a=blob;f=src/sort.c 10:46:02 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 200k doesn't sound like much 11:02:39 -!- jhj1 has quit (Ping timeout: 265 seconds). 11:03:54 "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:00 "disappointing"? 11:04:42 -!- nooodl has joined. 11:05:37 it's a legal right to have wrong data or outdated data removed or corrected 11:05:46 in most EU countries at least 11:05:55 -!- boily has quit (Quit: ¨¨¨¨¨¨¨¨). 11:05:55 -!- jhj1 has joined. 11:06:47 theoretically... google isn't even allowed to collect information about me without asking me for permisison to do so 11:07:04 (if google was bound by swiss laws) 11:07:15 yes but it hurts the business model of doing things without a huge human staff. 11:07:26 mroman_: you realize that would have killed the internet, right? 11:08:15 search engines would have been _impossible_ to invent if it required positive action from those indexed. 11:08:43 I don't quiet agree with that. 11:09:03 webmasters could've registered their website for being indexed 11:09:09 *websites 11:09:43 and besides 11:09:50 they could still index webpages without your permission 11:10:01 because what you publish on your websites is usually considered "public" 11:10:33 what's really illegal is to put all the informtion pieces together to make statements about an individual person 11:10:36 well duh. 11:11:20 also, this is why robots.txt was invented. he should have been going after the website which publicized him, not google... 11:11:41 yeah 11:11:59 but the law shouldn't work like that "unless you say no I'm just gonna do some illegal stuff" 11:12:15 at least not for privacy 11:12:20 that beats the whole point of privacy imo 11:13:10 yes but for historical reasons search engines _had_ to assume the absense of robots.txt meant consent. 11:13:12 theoretically google has to inform me once they received data about me from a third party 11:13:24 i.e. if someone else said something on some website about me 11:13:39 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 yes, theoretically it's impossible to do anything useful without breaking a law hth 11:14:09 however, sending information about my person to foreign countries is actually illegal too 11:14:13 unless you have more lawyers than customers. 11:14:23 so if somebody says something about me on facebook that's already very problematic 11:14:27 -!- Frooxius has joined. 11:14:29 If someone reads something about you anywhere, they are legally obliged to tell you? 11:14:56 Jafet: depends on what they read and what they do with the information 11:14:57 p. good law 11:15:10 Jafet, i read that u suck 11:15:15 -!- AnotherTest has joined. 11:16:14 Jafet: It is a good law 11:16:23 otherwise you could say "Well, I didn't collect that information myself" 11:16:24 Taneb: thank you for fulfilling your legal obligation under swiss law 11:16:30 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 and you'd be safe from legal consequences 11:17:09 oerjan: I don't know what your definition of "plausible working internet" is 11:17:15 The internet still works without social media 11:18:13 You are not allowed to make a profile of a person with data you collected from third parties 11:18:24 that doesn't mean social medias are doomed to not exist 11:18:36 it just means that they are not allowed to analyze what people write 11:18:50 No, you are not allowed to. Other people are, because they are not swiss. 11:18:52 if they just "store" the information they are not creating a profile of my person 11:19:18 and 11:20:11 it still be possible to have social medias and stuff 11:20:48 they might not be free anymore, because they can't make money by shitting on privacy 11:21:13 so they probably have to earn money differently 11:21:22 hm 11:21:24 No, people will not use them and will use the ones that charge no money and shit on privacy. 11:21:36 Especially your privacy. 11:22:03 Jafet: probably 11:23:21 It's just that I don't really get people complaining about privacy 11:23:45 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 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 this conversation was a bad idea. 11:24:59 I don't really expect anything different from a continent that created browserchoice.eu 11:25:00 now i'm all grumpy. 11:25:06 oerjan: why? 11:25:13 Did I make you angry? 11:25:24 slightly. 11:25:31 how so? 11:26:10 because you reminded me that the world sucks, hth 11:26:20 o_O 11:27:38 also because headache. 11:29:01 I should probably read about privacy laws in the US :) 11:29:47 Don't worry, it won't take that much time. 11:30:49 XD 11:31:22 "public disclosure of private facts" 11:36:38 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:35:57 You know 12:36:06 I wonder how bad gotos really are 12:36:17 I think they get a lot of bad rep because of spaghetti code 12:36:20 http://sprunge.us/FaUX man, freenode operators must've done something very personal to this person. 12:36:32 But I think people are just afraid to use it nowadays 12:36:56 Apparently not enough to use the word FUCK 12:37:10 His mama raised him right! 12:38:55 Perhaps it's a case of steganography, and all the numbers encode a hidden message. 12:39:26 659 F{}CK YOU!!! 12:39:31 That is a lot of fuck you 12:40:44 slereah: "GOTO considered harmful" considered harmful 12:43:40 CPS is good. 12:43:51 [wiki] [[One]] http://esolangs.org/w/index.php?diff=39515&oldid=39514 * Oerjan * (+30) fmt, sp 12:50:25 Is there a general channel for like 12:50:28 Algorithm questions 12:50:30 I am wondery 12:50:43 I always have a bunch 12:51:55 [wiki] [[Talk:Rand.Next()]] http://esolangs.org/w/index.php?diff=39516&oldid=39508 * Oerjan * (+347) unsigned, and No. 12:53:12 apparently there's a ##algorithms 12:53:54 -!- AnotherTest has quit (Ping timeout: 276 seconds). 12:54:00 with one # even (surprisingly) 12:54:22 must mean knuth owns it. 12:56:00 Thanks 13:20:04 -!- hk3380 has joined. 13:32:28 -!- drdanmaku has joined. 13:33:28 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 FireFly: indeed. that's part of its purpose. 13:41:28 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:43:57 *a url 13:45:39 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:08 alright 15:47:15 now I just need to bind type vars to specific types 15:52:27 -!- Bike has joined. 15:56:23 yay \o/ :) 15:56:24 | 15:56:24 /| 15:57:29 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 At least for static typed stack stuff 16:07:41 with a C like type-system 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 Why does Haskell not allow function overloading? 17:25:03 assuming types don't overlap like pu 17:25:18 foo :: a -> int -> double and bar :: int -> a -> double 17:25:22 that'd be tricky 17:25:43 currently I'm just picking the first variant I find that typechecks 17:26:20 well, what for? if it does the same thing but depends on certain properties, make a class 17:26:31 if it does different stuff, name it differently 17:27:05 Makes sense for Haskell @class 17:27:08 true 17:27:12 I don't have classes yet :D 17:28:10 I rely on overloading for now I guess 17:28:49 which means that somebody can break all existing pieces of code by defining 17:28:55 add :- A -> A 17:29:07 because that'd overload pretty much every add variant 17:29:09 or even worse 17:29:12 add :- -> 17:29:30 I should probably restrict that somehow in the future 17:32:27 what are you doing 17:43:06 -!- Sprocklem has quit (Ping timeout: 258 seconds). 17:43:52 ( :t index 17:43:56 Data.HVect.index : (i : Fin k) -> HVect ts -> index i ts 17:43:56 Prelude.List.index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a 17:43:56 Prelude.Stream.index : Nat -> Stream a -> a 17:43:56 Prelude.Vect.index : Fin n -> Vect n a -> a 17:44:38 myname: What would you propose for these? 17:45:47 Melvar: all of those but Prelude.List.index are special cases of the HVect case 17:45:56 -!- MoALTz has joined. 17:46:07 No they aren’t. 17:46:36 Vect’s, I suppose, is, but HVect.index uses Vect.index in its type. 17:46:44 ok, if you parameterise over the index type too 17:46:55 Melvar: what I mean is that you could make a class by tweaking Data.HVect.index's type. 17:47:33 A Stream is infinite and thus any Nat will do, which is not the case for any of the rest … 17:48:21 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 of course this is ugly. it supports Prelude.List.index too if you make Index a tuple 17:50:53 Doesn’t look like there’d be any chance of inferring things, even if it could be made to work. 17:51:15 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 elliott: Btw you overloaded Index there. 17:54:35 I said it was frankenstein. 17:54:41 Okay. 17:56:38 -!- Slereah_ has quit (Ping timeout: 252 seconds). 17:56:41 ( :t (::) 17:56:41 Effects.Env.:: : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs) 17:56:41 Data.HVect.:: : t -> HVect ts -> HVect (t :: ts) 17:56:42 Prelude.List.:: : a -> List a -> List a 17:56:42 Data.Vect.Quantifiers.:: : P x -> All P xs -> All P (x :: xs) 17:56:42 Prelude.Stream.:: : a -> Lazy' LazyCodata (Stream a) -> Stream a↵… 17:57:31 Prelude.Vect.(::) got cut off. 18:00:32 -!- hk3380 has joined. 18:03:17 ( [True,"foo"] 18:03:18 When elaborating an application of constructor __infer: 18:03:18 Can't disambiguate name: Effects.Env.::, Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.:: 18:03:57 Huh, that used to work. 18:07:13 myname: static typed stack-based programming languages 18:10:10 Mh, I guess i since imported Quantifiers and Env. 18:17:34 myname: I can probably even infer types 18:17:48 -!- Slereah_ has joined. 18:17:55 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 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:35 Hm 19:15:42 What's a good video to gif converter 19:16:28 ffmpeg? 19:16:44 Let's give it a whirl 19:23:12 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 But I'm fairly ignorant about the topic. 19:24:14 Slereah_: monotone wrote a walkthrough http://blog.room208.org/post/48793543478 19:33:45 hello party people 19:39:07 "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 Does "Gaussian, Inc." own the patents for the normal distribution? 19:43:56 wow; impressive, int-e! 19:44:39 it's a quantum mechanics thing. not sure why it's named after gauss but what isn't 19:44:48 "The name originates from Pople's use of Gaussian orbitals to speed up calculations compared to those using Slater-type orbitals" 19:45:05 I've used netpbm from shell scripts to do video processing 19:45:12 including, like, chroma key 19:45:14 and other fancy compositing 19:45:23 kmc: i meant the origin of gaussian orbitals 19:45:29 oh :3 19:46:10 i'm full of layers, man 19:52:45 -!- Sprocklem has joined. 19:54:18 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 ...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:03 ) (for oerjan) 19:55:03 int-e: for oerjan 19:55:09 hah. 19:55:39 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 v. unfortunate :/ 19:56:43 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 tromp_: btw your "g" appears here: https://en.wikipedia.org/wiki/Fast-growing_hierarchy#Definition 20:00:18 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 oh, that's so much nicer. should consider that ordinal the starting point then 20:07:24 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 such a round number... 20:14:31 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 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 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 @tell 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:31 eek 21:20:36 int-e: AAAAAAAAAAAA 21:20:46 oerjan: it'll be back in a moment 21:20:57 whew 21:21:26 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 seems they took almost 15 minutes. 21:22:29 those evil dutch 21:22:35 they're american 21:22:41 :P 21:22:48 (they company is, that is.) 21:22:49 also, aren't you in germany. 21:22:54 no I'm in Austria 21:23:15 but from Germany ... 21:23:17 * int-e shrugs 21:23:42 well your client is in .de 21:23:51 ... that's another server ... 21:24:10 fiendish 21:24:16 but it was too weak for lambdabot :) 21:24:26 i can believe that. 21:25:06 -!- lambdabot has joined. 21:25:10 @bot 21:25:12 @hug lambdabot 21:25:18 :) 21:25:24 http://hackage.haskell.org/trac/ghc/newticket?type=bug 21:25:43 @tell 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:25:50 Consider it noted. 21:26:39 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:27:37 nope, no change. 21:29:01 -!- Bike has joined. 21:31:44 as expected, really, it's a you're-doing-it-wrong-but-it-doesn't-really-affect-realistic-programs bug 21:32:31 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:33:00 OKAY 21:35:21 -!- nooodl_ has joined. 21:35:25 ( :t (>>=) 21:35:25 Effects.>>= : Eff m a xs xs' -> ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs'' 21:35:25 Prelude.Monad.>>= : Monad m => m a -> (a -> m b) -> m b 21:37:35 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 Pretty much, in some cases at least. 21:38:56 (looking also at your index and (::) examples earlier) 21:39:58 i suppose someone needs to invent a more suitable way of abstracting over those differences 21:41:12 hm isn't that among the use cases for ghc's PolyKind and ConstraintKind extensions 21:41:26 *+s 21:42:24 but you still need things to fit just right. 21:43:43 ( :t Type -> Type 21:43:44 Type -> Type : Type 21:43:56 ( :t Show 21:43:56 Prelude.Show : Type -> Type 21:44:58 ( :t Show Int 21:44:58 Show Int : Type 21:45:09 ic 21:45:18 ( the (Show Int) %instance 21:45:18 constructor of Prelude.Show (\{meth0} => prim__toStrInt meth) : Show Int 21:45:42 idris runs on meth 21:46:43 oh, methodical 21:47:10 -!- boily has joined. 21:47:27 boilaften 21:48:33 good oerjaning. 21:49:28 -!- metasepia has joined. 21:51:25 ~metar CYUL 21:51:26 CYUL 142121Z 18009G15KT 15SM SCT045 OVC070 23/15 A3008 RMK SC3AC5 SLP187 DENSITY ALT 800FT 21:51:38 ~metar ENVA 21:51:38 ENVA 142120Z 17003KT CAVOK 04/M02 Q1029 RMK WIND 670FT 30003KT 21:52:23 oerjan: “class Finite (n : Nat) t where isoFin : Iso t (Fin n)” is also a thing, outside of the stdlib though. 21:52:44 you are my DENSITY, DENSITY, DENSITY 君と行ける未来 ♪ 21:57:14 int-e: huh, and that goodstein program has no recursion? 21:57:38 oerjan: that was the point 22:03:05 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 kmc: you vile bot drugger! you should feel ashamed! 22:20:18 boily: that's not tofu but rancid butter hth 22:23:23 ntdnh. 22:24:33 "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 "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 I reject your reality and substitue my sane own. 22:29:41 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 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 that sounds like a shoddy patch over "countries". 22:33:51 it's not very hidden... it's more like check-out-that-pulsating-radiating-mesmerizing-glow. 22:35:58 i'm just amazed that it's been there since 2011. 22:36:06 wikipedia? 22:36:08 https://en.wikipedia.org/w/index.php?title=Yak_butter&diff=437641611&oldid=437595102 22:36:17 it's not inaccurate. 22:36:41 nominally, tibet has a good deal of self-governance. 22:36:43 that seems less like a deliberate burn and more like an attempt to avoid trouble from chinese nationalist trolls 22:36:49 basically that. 22:36:54 of which there are many 22:37:15 I don't know if the govt has an app to coördinate the trolls like Israel does 22:37:26 the usual term for when you want to talk about nations without talking about nations is "culture", though 22:37:40 well i'm just amazed that they haven't removed it _anyhow_. admittedly i didn't check all intervening edits. 22:37:47 why would they remove it? 22:37:47 yes, there's no reason to mention politics there 22:37:54 oh, because they're trolls, you mean 22:39:18 i'd imagine even listing China and Tibet separately under _any_ categorization would be enough to trigger them. 22:39:24 yeah i see what you mean 22:39:35 maybe chinese nationalists don't care for yak butter 22:39:49 ...plausible. 22:40:35 -!- yorick has quit (Remote host closed the connection). 22:43:19 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 e.g. "Chinese Taipei" at the olympics, what a wonderful bit of deliberate ambiguity 22:44:35 although Hong Kong has its own Olympic delegation as well 22:45:58 i didn't know taiwan even had an olympic team. 22:46:12 http://en.wikipedia.org/wiki/Template:Multiple_Olympic_Teams 22:46:28 what about macau? 22:46:37 guess not. 22:46:46 they're not members of the IOC but they participate in the Asia Games or something 22:53:21 nice! http://rust.godbolt.org/ 22:54:58 i guess "int x;" isn't legal so i give up 22:55:14 kmc, I like that :) 22:56:00 holy shit, people are doing GBA homebrew in Rust: https://github.com/exoticorn/gba-rust 22:56:09 awesome 22:56:35 what processors does rustc target, anyway 22:56:46 oh right llvm 22:59:12 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 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:25:36 probably 23:27:12 several methods that do the same thing -- code smell 23:27:51 Seems to happen all the time in Smalltalk 23:27:57 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:01 smelltalk :D 23:28:42 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 clearly you need to borrow Haskell's new MINIMAL pragma. 23:30:18 or have some non virtual methods obviously 23:31:02 I think this may be subtyping's fault, or something 23:31:19 oerjan: yay 23:31:38 well you can't even state the problem without subtyping. 23:31:46 so. you know. 23:31:52 blame smalltalk. 23:32:12 whoever came up with that MINIMAL thing must've been p. great 23:32:28 -!- hogeyui has joined. 23:34:44 was it you 23:34:47 is that the joke 23:35:00 smelltalk :D 23:35:10 kmc: hey no fun ruining the joke this soon 23:37:55 There is the theory of the mobius 23:38:03 -!- nooodl has quit (Ping timeout: 255 seconds). 23:39:04 a twist in the fabric of space, where time becomes a loop. 23:39:42 > cycle "time becomes a loop. " 23:39:43 "time becomes a loop. time becomes a loop. time becomes a loop. time becomes... 23:40:43 good stopping point. 23:42:57 yes it was me 23:43:00 when we reach that point, whatever happened will happen again 23:43:08 that is the joke 23:43:35 shachaf will introduce MINIMAL again 23:44:37 MINIMALER 23:46:10 hm, this paper claims to determine a "word length" for neural information 23:53:18 whats neural information 23:53:58 I'm hungry, but it's almost 1 AM 23:54:02 And I don't have any food 23:54:08 Taneb, fourth meal 23:55:13 fowl: information neurons "send". 23:56:06 what lke a float 23:56:55 yes. like a float. exactly. 23:57:38 are brains IEEE 754 compliant? 23:59:28 it actually uses the IBM 7094 format, for compatibility