00:00:01 it _starts_ with a sex change, and then you turn into a furry 00:00:25 pikhq: *a crisis 00:00:38 also, haw haw signal/noise has just approached 0 00:00:43 ... I accidentally used the plural. Hooray. 00:01:48 ANYWAY coppro 00:01:52 data ℝ : Set where 00:01:52 ℝ : (f : ℚ⁺ → ℚ) 00:01:52 → {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂} 00:01:53 → ℝ 00:01:53 00:01:53 ι : ℚ → ℝ 00:01:53 ι q = ℝ (λ_. q) 00:01:54 ADMIRE 00:02:55 * coppro explodes 00:02:57 pikhq: also does that make sense with "either one"? 00:03:17 or is my brain inferring an innuendo that in fact isn't there at all, thus implying i have finally left the last stage of sanity 00:03:24 coppro: THAT IS NOT ADMIRATION 00:03:47 great, I've pissed off alise. See you Tuesday 00:04:22 coppro: wat 00:04:23 yay 00:04:38 alise: because you're a girl, obv 00:04:53 oh. haw haw 00:06:58 alise: Hmm. *Looks* like the standard definition of the computable reals from the rationals. 00:07:22 Well... it is. 00:07:29 I'm going with "Sure, makes sense". ;) 00:07:34 euler : ℝ 00:07:35 euler = ℝ (λ ε → sum (map (λ i → (i!)⁻¹) (1 … ε))) 00:07:35 i think 00:07:55 yes I am using x⁻¹ in place of 1/x WHAT OF IT 00:08:24 I have no complaints. 00:09:11 -!- adam_d has quit (Ping timeout: 265 seconds). 00:09:36 and (m … n) for range, mostly because I can't think of anything else 00:09:56 also... it should be product not sum 00:09:57 w/e 00:10:34 and 0 not 1 lol 00:12:15 maybe I should define a product operator 00:12:15 like 00:12:16 ∏ 0 → ε ⇒ λ i → (i!)⁻¹ 00:13:09 euler : ℝ 00:13:10 euler = ℝ (λ ε → ∏ 0 → ε ⇒ λ i → (i!)⁻¹) 00:21:44 Incidentally, abs (x-y) deserves a better name than it possesses. 00:22:00 d(x,y) ? 00:22:13 That's not an operator, it's a function. 00:22:40 distance metric 00:23:11 For some reason I think it's actually a nicer operation than subtraction. 00:23:19 We're measuring, not doing some sort of thingy-bob operation. 00:25:35 oerjan: Seems that Epigram 2 does indeed have Mu, the Fix you quoted, as the primitive. 00:26:06 make nat := (Mu @ [`arg { zero, suc } [ (@ [`done]) (@ [`ind1 @ [`done]]) ] ] ) : * ; 00:26:07 make zero := @ [`zero] : nat ; 00:26:07 make suc := (\ x -> @ [`suc x]) : nat -> nat ; 00:26:07 make one := (suc zero) : nat ; 00:26:07 make two := (suc one) : nat ; 00:26:08 make plus := @ @ [(\ r r y -> y) (\ r -> @ \ h r y -> suc (h y))] : nat -> nat -> nat ; 00:26:08 make x := (plus two two) : nat 00:26:21 ah 00:30:40 Seems yucky to me, though. 00:33:06 oerjan: how can that mu do paramaterisable types though 00:33:12 λA → (λT → data nil : T; cons : A → T → T) 00:33:13 ? 00:33:19 er does that Mu show up for you? 00:33:20 probably not 00:33:26 nope 00:33:26 after the first -> imagine an M 00:33:35 oh wait no unicode at all 00:33:53 \A -> M (\T -> data nil : T; cons : A -> T -> T) 00:33:57 where M is our Mu 00:34:31 so you answered your own question? 00:34:35 yeah :P 00:34:53 \A -> M (\T -> (data nil : T) && (data cons : A -> T -> T)) 00:35:00 where && = Either = union = and 00:35:43 (data nil : T) ≈ 1 00:35:53 \A -> M (\T -> Unit && (data cons : A -> T -> T)) 00:36:05 so how to reduce the cons, I wonder 00:36:21 also, my issue with these kinds of shenanigans is that the implementation gets exposed 00:36:26 () : List, which isn't cool 00:37:25 i think the observational type theory guys have a nice way to do all this, and it's in epigram 2 :P 00:38:08 of course all this Muery doesn't help us write nice notation... 00:38:08 mhm 00:38:15 which is my whole goal :P 00:39:06 predicted return to specialized notation in 1,2 ... 00:39:17 -!- bsmntbombdood has joined. 00:40:17 oerjan: you're saying I'll never go back? 00:40:21 makes sense! 00:40:33 * oerjan swats alise -----### 00:40:38 but seriously why are the T and ... in the same definition in data X : T where ... 00:40:42 it makes no sense! 00:41:50 I thought I’d scribble something about what we’re up to. The team (Pierre-Évariste Dagand, Adam Gundry, Peter Morris, James Chapman) have been hard at work. I have been otherwise engaged. As a result, there has been considerable progress. Don’t worry. I expect I’ll mess things up properly over Christmas. 00:41:54 --Conor McBride 00:43:33 I'm tired, so I'll sleep now. 00:43:41 Hopefully, see you tomorrow. Bye! 00:43:42 -!- alise has quit (Quit: alise). 01:23:07 -!- FireFly has quit (Quit: Leaving). 01:23:18 -!- BeholdMyGlory has quit (Remote host closed the connection). 01:23:43 -!- benuphoenix has joined. 01:25:35 -!- oerjan has quit (Quit: Reboot). 01:25:38 Hmm, still nobody has sent me the esoteric-priv stuff. 01:25:54 is this the place where "int main(){for(int i=0;i<1;i++) i--; return 0;}" is a normal c++ program? 01:26:43 -!- cheater2 has quit (Ping timeout: 245 seconds). 01:29:02 -!- oerjan has joined. 01:31:32 benuphoenix: no. c++ is banned here. *ducks* 01:31:49 * oerjan doesn't know c++ anyhow 01:32:34 also, isn't that an infinite loop. 01:33:22 -!- MizardX has quit (Ping timeout: 276 seconds). 01:33:45 -!- cal153 has quit. 01:34:13 benuphoenix: No, we write crazier C++. 01:34:22 Well, crazier C, actually. 01:34:54 a,b,c;main(z,i)char**i;{h:a=!a,b=!b;g:(b-1)[1[i]]>b[i[1]]?a^=a,c=(b-1)[1[i]],1[i][b-1]=i[1][b],b[i[1]]=c,b=&b[(void*)1]:(b=&b[(void*)1]),!b[i[1]]?:({goto g;}),a?:({goto h;}),b=!b;j:putchar(b[1[i]])[(void*)(b=&b[(void*)1])],1[i][b]?({goto j;}):putchar('\n');} 01:34:56 Translate into Haskell please. 01:35:01 See? 01:35:11 for(i=0;i!=0;) 01:35:56 that's the craziest i can quickly think of that fits on one line. 01:36:32 what's it say 01:36:46 uorygl: The equivalent Haskell for benuphoenix's program is: main = undefined 01:36:48 :P 01:37:07 (well, strictly speaking his is the "infinite loop" sort of bottom, but hey.) 01:37:18 main = main 01:37:21 It's shorter, even! 01:37:39 No, GHC complains about that. 01:38:11 main = return $ length [1..] -- This is *actually* an infinite loop. :) 01:38:24 Erm. Wait, no, that won't be eval'd. 01:38:38 -!- Asztal has quit (Ping timeout: 258 seconds). 01:38:44 main = return $ length [1..] `seq` () 01:38:52 -!- Asztal has joined. 01:38:55 :) 01:39:10 Hi benuphoenix 01:39:26 hi Sgeo 01:40:37 am i the only one who uses irssi in windows instead of xchat? 01:40:38 !haskell import System; main = System.exit . flip seq 0 . all (<1) $ iterate (succ.pred) 0 01:41:00 I think uorygl SSHes in to normish from which he uses irssi 01:41:04 oh wait 01:41:11 ... Windows? 01:41:22 oerjan: Hah. 01:41:31 pikhq, on Cygwin apparently 01:41:34 !haskell main = flip seq 0 . all (<1) $ iterate (succ.pred) 0 01:41:48 argh 01:42:16 there's a win32 binary version on irssi.org 01:42:21 !haskell main = flip seq (return 0) . all (<1) $ iterate (succ.pred) 0 01:43:03 Might I suggest (`seq`return 0) instead of flip seq (return 0)? 01:43:39 you may 01:44:02 hm that last one got no response. maybe that meant it actually _did_ compile. 01:45:33 actually, does ghc use main's result for exiting if it is an Int? 01:45:46 might need that System function after all 01:45:49 c/c++: int main{for(;;);} might be infinite. i only speak c++ and basic 01:46:48 oh hm 01:47:06 Sgeo: currently, I SSH into sine.aftran.com from which I use irssi. 01:47:19 * Sgeo slaps uorygl 01:47:34 -!- Asztal has quit (Ping timeout: 265 seconds). 01:47:39 !haskell import System; main = exitWith . flip seq 0 . all (<1) $ iterate (succ.pred) 0 01:47:45 Hey, you know that sine.aftran.com is not the location of our chatting. 01:47:53 I left out the port number and channel name. 01:48:06 !haskell import System; main = exitWith . exitSuccess . flip seq 0 . all (<1) $ iterate (succ.pred) 0 01:48:32 * oerjan refuses to actually look up the correct function name :D 01:48:46 http://www.stationv3.com/d/20050131.html 01:49:41 -!- cal153 has joined. 01:51:20 *cough* 01:51:24 (`seq`0) 01:51:47 pikhq: i said you may suggest it, not that i would listen 01:51:57 oerjan: Ah. 01:52:33 i got "main(){for(;;);}" to compile and run infinite. 01:52:50 !c++ main(){for(;;);} 01:53:11 well it hasn't complained yet 01:53:16 !gnarble 01:53:26 !interps 01:53:36 benuphoenix: Well, yeah... 01:53:42 !help 01:53:43 help: General commands: !help, !info, !bf_txtgen. See also !help languages, !help userinterps. You can get help on some commands by typing !help . 01:53:51 !help languages 01:53:52 languages: Esoteric: 1l 2l adjust asm axo bch befunge befunge98 bf bf8 bf16 bf32 boolfuck cintercal clcintercal dimensifuck glass glypho haskell kipple lambda lazyk linguine malbolge pbrain perl qbf rail rhotor sadol sceql trigger udage01 underload unlambda whirl. Competitive: bfjoust fyb. Other: asm c cxx forth sh. 01:53:52 -!- Asztal has joined. 01:54:01 oh 01:54:10 !cxx main(){for(;;);} 01:54:20 !c main(){main();} 01:54:22 ./interps/gcccomp/gcccomp: line 52: 29844 Segmentation fault /tmp/compiled.$$ 01:54:32 What, no TCO? 01:54:35 *Lame*. 01:54:49 *Real* compilers TCO. 01:55:22 TCO? 01:55:49 Tail-call optimisation. 01:56:08 Ah 01:56:14 Python doesn't do that, for some reason 01:56:24 A tail call can be optimised to a jmp fairly easily. 01:56:27 I remember reading about someone arguing that that's correct, and it shouldn't 01:56:53 It's incorrect. 01:57:22 At a *bare* minimum it should offer a way of explicitly doing a tail call. 01:57:32 (something like Perl's "goto &func;") 01:57:41 Erm. 01:57:46 "goto &func(args);" 01:58:46 -!- Azstal has joined. 01:58:47 (note: TCO is harder to do in C, because of calling conventions. Caller cleanup means that not many things are actually tail calls.) 02:00:09 running main(){main();} after [c++] compiling successfully segmetation-faulted after 1.49 seconds 02:00:29 i'm ssh'd onto my freebsd 8 system 02:00:37 -!- Asztal has quit (Ping timeout: 265 seconds). 02:00:39 c++. for high-speed crashing. 02:00:54 lol 02:01:39 I take it C++ doesn't TCO either 02:01:41 ? 02:02:11 Depends on your compiler 02:02:23 I'm surprised that even compiles; main is not supposed to be callable 02:03:07 it says it's gcc version 4.2.1 02:03:43 :/ 02:04:24 normally the compiler inserts all the initialization into the prelude of main, so the standard disallows calling it from within the program 02:05:41 * benuphoenix thinks that the only reason that g++ allows it is because one of the developers wanted to program infinite loops 02:06:05 or something like that 02:06:27 nah, you can make infinite loops all sorts of other ways 02:06:59 s/infinite loops/recursive function calls/ 02:07:07 -!- Azstal has quit (Ping timeout: 265 seconds). 02:07:47 you can go infinitely recursive with any other function 02:08:52 you can infinitely loop while choosing how to infinitely loop! 02:10:02 running main(){main();} gave me a 67 meg core dump 02:11:20 coppro: GCC doesn't stick any initialization into main. 02:11:27 coppro: The entry point is _start. 02:11:40 coppro: _start initialises things and then calls main. 02:11:51 pikhq: yes, but that doesn't change the standard 02:12:01 calling main is still illegal 02:12:14 GCC does many things that are illegal. 02:12:40 yarly 02:13:24 allowing "main(){...}" when it should only be "int main(){...}" 02:14:02 In C89, the "int" is implied. 02:14:48 in C99 too, no? 02:15:55 I'm pretty sure that's still legal in C99, although stupid :) 02:16:32 Anyway, I'm sure -Wall -Werror -ansi -pedantic would complain. 02:16:33 Oh, right. C99 allows it for functions. 02:16:42 It's banned for variables. 02:16:47 Gregor: -std=c99 makes it warn. 02:16:55 It's deprecated but allowed. 02:17:10 I know I've gotten warning. 02:17:35 C99 apparently lets you do int a[b]; when b isn't a const? 02:17:36 Warning != illegal. gcc also warns if you use gets() 02:17:42 * Sgeo is somewhat scared 02:17:47 In fact, gcc warns if you use gets() even if you specify -w (no warnings) :P 02:18:09 Sgeo: You could approximate that with alloca anyway 02:18:12 Sgeo: Yeah, works just fine. 02:18:19 The array gets allocated on the stack. 02:18:38 And gets cleaned up when it goes out of scope. 02:18:53 (by "cleaned up", we of course mean "popped".) 02:19:06 (IIRC, alloca is not part of any standard, but is basically implemented by everyone) 02:19:30 Yeah, alloca is pretty common. 02:19:56 Ah. It's POSIX. 02:20:13 Is benuphoenix doing C or C++? 02:20:16 pikhq: It is? 02:20:31 CONFORMING TO 02:20:32 This function is not in POSIX.1-2001. 02:20:32 No, no it's not. I thought it was. 02:20:34 Sgeo: C++ 02:20:37 For some reason. 02:20:50 It's just been around since at least 3BSD. 02:21:32 even when it's identical to c, i still use c++ 02:21:58 benuphoenix: That's dumb. 02:23:19 actually, i rarely write something in c++ that doesn't use iostream 02:23:58 Eeeeew. 02:24:25 C++'s IO is one of the more stupid features. 02:24:45 (seriously, IO via bitshift?) 02:25:31 the "<<" and ">>" are overrides 02:26:18 at least, i think that's the term 02:26:31 They're bitshift operators. 02:26:54 That your bitshift operator isn't *shifting* any *bits* doesn't make them cease to be bitshift operators. 02:28:08 It is somewhat ugly, but is that that big a tragedy? 02:28:10 pikhq: i know what the bitshift operaters are and what they are supposed to do 02:28:51 Sgeo: That's but one of the poor things about C++'s IO. 02:28:55 It shifts bits from memory into IO :P 02:28:58 Or vice/versa 02:29:03 This is merely a poor *aesthetic* choice. 02:29:55 Paging coppro to #esoteric . coppro to #esoteric 02:30:35 Iostreams also have the annoying property that you can manipulate their ouput mode, but not readily set the output mode back to what it was previously. 02:30:55 Write a function that outputs some numbers as hex and then returns the iostream to the previous mode. Go on, I'm waiting. 02:31:10 Also, Iostreams make i18n a royal *pain*. 02:31:31 In C, you would wrap the format string in a function that looks up the translation for the string. 02:31:42 In C++... You use printf if you want to do that. 02:32:06 (or GNU's asprintf, which is a printf that *works on iostreams*. Thus obviating everything different about them.) 02:32:09 Surely you can retrieve the flags somehow? 02:32:15 i mainly use cin.get() and cout.put() 02:32:30 Sgeo: No. 02:32:47 cin.something? There's no something? Or something()? 02:32:49 :( 02:33:01 Also, why in the world does endl exist? I could understand if it actually used the system end of line character. 02:33:10 Sgeo: pong 02:33:14 But it *doesn't*. It just outputs \n and flushes the iostream. 02:33:21 So. Fekking. *Stupid*. 02:33:37 coppro, read the C++ criticism. You're a C++ defender person, iirc? 02:33:44 oh, I don't defend IOstreams 02:33:45 they suck 02:33:50 See? 02:34:24 ... C++ vs C arguments. Seriously? Argh. 02:34:26 the overarching concept (easily extensible streams) is good, and that's about it 02:34:36 coppro: Agreed. 02:34:54 Gregor: Hey, we have to do one of these every now and then. 02:36:58 true or false: iostreams are useful when the professors want to see them in the code? 02:37:07 true 02:39:19 what are the c stdio equivlents of the c++ iostream functions "cin.get()" and "cout.put()"? 02:40:03 What's the type of get and put again? 02:41:07 getc and putc 02:41:15 or something like that 02:41:16 Mmm... 02:41:21 benuphoenix: Which get? 02:41:29 pikhq: the one that gets the next character 02:41:48 Ah, the "int get()" one. 02:42:48 Yeah, "int getchar(void)" and "int putchar(int)" are the functions. 02:46:51 Everyone who needs to breathe has thirty seconds to get off the station. 02:48:48 http://www.stationv3.com/d/20050921.html 02:58:42 -!- benuphoenix has quit (Quit: leaving). 03:17:10 -!- sshc_ has joined. 03:17:59 -!- sshc has quit (Quit: Reconnecting). 03:23:28 -!- sshc_ has changed nick to sshc. 04:08:32 -!- Oranjer has left (?). 04:48:46 who wants to dick around with an experiment in flight control for my video game? :D 05:08:11 xkcd XD 05:10:48 Wish the die looked better though 05:19:18 -!- coppro has quit (Remote host closed the connection). 05:19:45 -!- coppro has joined. 05:40:08 -!- oerjan has quit (Quit: Good night). 05:43:53 -!- jcp has quit (Ping timeout: 248 seconds). 06:36:04 `translate Linguini! Fettucini, al forno! Bolognese, Crostini. Carbonara. Manicotti con Granchi e Spinaci. Frutti... di... MARE! Resquiat in pesci, in pesto, e in quattro formaggi. 06:36:15 Resquiat in fish, pesto, and four cheeses. 06:37:08 uorygl: what are you trying to do lol 06:37:11 `translate Linguini; fettucini, al forno; bolognese, Crostini; carbonara; manicotti con Granchi e Spinaci; frutti... di... MARE; resquiat in pesci, in pesto, e in quattro formaggi. 06:37:13 SEA; resquiat in fish, pesto, and four cheeses. 06:37:16 ... 06:37:21 I'm trying to translate that. 06:37:27 whats to translate 06:37:31 theyre names of foods 06:38:12 How about the "al forno" and the "resquiat" parts? 06:38:55 oh who knows im not italian 06:40:16 I guess all of it is food except the resquiat. 06:53:37 -!- Sgeo_ has joined. 06:55:19 -!- Sgeo has quit (Ping timeout: 256 seconds). 07:41:18 -!- tombom has joined. 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:00:57 -!- lament has quit (Ping timeout: 248 seconds). 08:01:06 -!- lament has joined. 08:02:01 -!- adam_d has joined. 08:15:16 -!- cheater2 has joined. 08:23:29 -!- Asztal has joined. 08:36:54 -!- adam_d has quit (Quit: Leaving). 09:10:27 -!- yourcomdotmom has joined. 09:10:27 -!- yourcomdotmom has quit (Excess Flood). 09:11:14 -!- MizardX has joined. 09:13:14 -!- yourcomdotmom has joined. 09:15:34 -!- yourcomdotmom has quit (Remote host closed the connection). 09:16:40 -!- yourcomdotmom has joined. 09:17:10 -!- yourcomdotmom has quit (Remote host closed the connection). 09:17:53 -!- yourcomdotmom has joined. 09:33:23 -!- yourcomdotmom has quit (Remote host closed the connection). 09:51:06 -!- scarf has joined. 10:09:32 That translated bit sounds so very very familiar, but I just can't place it. I'm sure I've read it somewhere, though. 10:42:03 -!- FireFly has joined. 10:56:05 -!- scarf has quit (Remote host closed the connection). 11:08:52 -!- ehird has joined. 11:09:05 March. 'Tis verily March. 11:15:58 So I was thinking that the inductive datatype constructor would be M, and the forgotten-the-name (like maybe for Maybe) μ. So you'd define all functions on inductive data-types with μ. I think Epigram 2 does that, or something like it. 11:17:22 I don't think M : (Set -> Set) -> Set makes sense, though; you can't define a sensible μ recursion combinator just based on that. 11:19:12 Or maybe you can. Feeding the non-M'd (List A) to the empty type gets us `data empty : Void; cons : A -> Void -> Void`. Wait, what? empty : Void? 11:19:16 I'm confused now. 11:19:25 ehird?! 11:19:31 -!- ehird has changed nick to alise. 11:19:33 Gotta fix that default. 11:19:41 :( 11:19:45 I MISS MY EHIRD 11:19:49 Tough shit. 11:19:50 :) 11:19:52 <3 11:19:57 ever used unity? 11:19:57 -!- alise has changed nick to ehird. 11:19:59 -!- ehird has changed nick to alise. 11:20:09 -!- alise has quit (Quit: alise). 11:20:27 -!- alise has joined. 11:20:35 Never used Unity. 3D is hard; let's go shopping. 11:20:45 duuuude 11:20:46 Write it in my language! 11:20:46 its so cool 11:20:48 It'll be dependent. 11:20:58 MONOIDAL RENDERING 11:26:45 18:33:37 coppro, read the C++ criticism. You're a C++ defender person, iirc? 11:26:45 Correct. I would also have accepted "lunatic". 11:40:25 -!- rodgort has quit (Quit: Coyote finally caught me). 11:40:34 -!- rodgort has joined. 11:44:34 -!- scarf has joined. 11:47:23 Hi scarf 11:47:32 hi alise 11:48:13 sorry, haven't been doing too much esoprogramming recently, unless you consider Java eso 11:48:50 one of the things which comes with a job is not always being able to choose which language you write in 11:48:58 that's alright, I haven't been either 11:49:16 well, then again, I guess you could consider my language eso 11:49:25 so you're saying that Java is a good language know if you want a job? well, it got /me/ a job 11:50:03 :( if i had been there i'd go on a lecture about soul-crushing C.R.U.D. work with contradictory specifications to the student :D 11:50:06 that would have been fun! 11:50:24 I may be the most cynical person about programming jobs who has /never had a programming job/ 11:50:25 heh, well my job is teaching it to students 11:50:35 so I don't have the sort of over-enterprisiness issues 11:50:44 just, my heart sinking at people confusing classes and methods 11:50:51 yeah but it's basically like teaching applied satanism :P 11:50:55 hah 11:50:56 *haha 11:50:58 you can do it but... why 11:51:16 improving the average quality of Java programmers can only be a good thing, surely? 11:51:20 true. 11:51:30 anyway, have the computable reals: 11:51:32 data ℝ : Set where 11:51:32 ℝ : (f : ℚ⁺ → ℚ) 11:51:32 → {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂} 11:51:33 → ℝ 11:51:33 11:51:33 ι : ℚ → ℝ 11:51:33 ι q = ℝ (λ_. q) 11:52:13 yay, Unicode support 11:52:24 I think any language with a syntax like that is necessarily eso, including APL 11:52:32 also, http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=380731#15 (found via reddit) makes me amused 11:52:34 Support? I'm afraid I'm going to shift your opinion now; it's not optional. 11:52:41 Unicode or GTFO! 11:52:57 scarf: that bug report really irritates me 11:53:08 i am god, accept my holy package judgements 11:53:21 alise: it confuses me, but I'm not sure why I'm confused and get even more confused as a result 11:53:49 alise: do you consider support for the astral planes also necessary? 11:53:53 I really like the definition of computable reals 11:54:09 scarf: Well, it's only "required" insofar as the basic syntax and stdlib use it :P 11:54:16 oh, for the lang 11:54:20 a 11:54:22 *ah 11:54:31 Or, wait, does any of the actual syntax use it? The arrow is defined in the stdlib, albeit as a primitive 11:54:36 I thought you meant that Unicode support was necessary for everything, and ended up agreeing with you 11:54:39 Oh, of course, lambda 11:54:55 scarf: Well, that too of course 11:54:58 Aastral Plane is nice also 11:55:01 *Astral 11:55:06 in derl (my underlambda/underload interp), all I/O is in UTF-8, and it uses UTF-32 internally 11:55:27 hmm, I don't think I've ever seen the Unicode version of the astral planes written with a capital letter 11:55:32 Nor I, oh well 11:55:36 God I love dependently-typed languages 11:55:39 and there are 16 of them 11:55:42 Induction on the naturals as a recursion combinator? 11:55:43 Wyever not 11:55:50 *Whyever 11:56:25 alise: my PhD is turning slightly towards the idea of dependent types; dependent types is sort-of parametrizing types towards values, whereas what I'm doing is in the other direction 11:56:44 It's not sort-of, that's exactly what it is. 11:56:47 where types are parametrized by the number of times you're allowed to use a value of that type ever 11:56:55 alise: well, ok 11:57:01 The normal typed lambda calculus is types indexing on types, and values indexing on values. 11:57:06 With typeclasses, we have values indexing on types. 11:57:11 Dependent types give us types indexing on values. 11:57:18 Or, wait, typeclasses don't /quite/ do that. 11:57:19 But close. 11:57:33 Dependently-typed languages usually have types as first-class values, too, so we get values-indexing-on-types for free. 11:58:55 one thing I've been thinking about recently is designing my own VCS 11:59:05 I like how the (intensional) Axiom of Choice is in fact provable in intuitionistic type theory and thus most dependent langs. 11:59:10 I think I found a paradigm general enough to contain both git's model and darcs's model as special cases 11:59:16 Wonder if it is in Observational Type Theory (the underpinning of Epigram 2)? 11:59:23 alise: ooh, the axiom of choice 11:59:29 (Not the extensional axiom of choice, though.) 11:59:37 Extensional is the one that lets you do things like order the real numbers. 11:59:46 http://r6.ca/blog/20050604T143800Z.html 11:59:48 when you're in a CS department, you eventually find someone who makes you realise that it isn't actually obvious after all 11:59:52 You can have one without the other. 12:00:01 Which is awesome. 12:00:54 *intensional not intuitionistic 12:01:05 the intensional one is the one that's normally stated as the axiom, at least here 12:01:32 but then, we're normally dealing with sets, where the existence of quotients is taken for granted 12:01:38 so they probably come out equivalent there 12:02:02 yes it's causing me a bit of a crisis as I like quotient types 12:02:25 and Observational Type Theory which has a really nice definition of equality has tem 12:02:27 *them 12:02:33 also, that first link is a data: link 12:02:35 I love that page 12:02:38 but surely it cannot have extensional choice? 12:02:44 otherwise it'd have excluded middle 12:02:59 although it doesn't load in my browser 12:03:01 and you cannot give a value of either p or p -> Void for every type p... 12:03:09 scarf: he does tat a lot 12:03:13 *that 12:03:15 it's like footnotes but awesome 12:03:26 hmm, I wonder why it isn't working? loading it just gives me a blank page 12:03:29 his blog http://r6.ca/blog/ is very cool 12:05:22 http://r6.ca/blog/20091101T231201Z.html man I haven't read this before 12:06:28 hmm, loads in Epiphany 12:06:32 that's -webkit 12:07:17 That data: link was the strange in my Ubuntu 3.0-series Firefox too: clicking did nothing; opened in new tab, initially got a blank page with no special load indicators; finally got it open when I went to the location bar to press enter once. 12:07:30 WFM (safari) 12:07:35 -!- Gracenotes has quit (Quit: Leaving). 12:08:09 Given that it works just fine after the go-to-location-bar-and-press-return, I suppose there's nothing wrong with the link itself. 12:08:10 fizzie: ah, let me try that in FF 12:08:37 fizzie: yep, same results 12:08:54 that /is/ a weird bug, I wonder if it's an FF bug or an extension bug? 12:09:10 so, guys, what's your favourite definition symbol? 12:09:36 I like ≔ 12:10:43 I like that snowman guy. 12:11:26 har har 12:12:33 alise: = with a little word "def" over it is normally used when writing proofs here 12:12:45 I'm not sure how much I like it, but it's at least unambiguous 12:12:45 Yes, but you need a huge font size for that to be readable. 12:13:01 also, there's something very nicely pure about a language that can get away with using = for defined-equal 12:13:03 Plus, it is ugly; we rarely use words in mathematics, preferring symbols (including alphanumeric ones). 12:13:03 ≔ is nice, though in this font even that's just a = that has some sort of blobby things on the left end. 12:13:05 like Algol 68 12:13:19 Overlaying an English abbreviation on top of a very common symbol is just silly/ 12:13:19 or Haskell 12:13:21 *silly. 12:13:23 fizzie: Ditto. 12:13:33 it's visible as a :=-alike to me 12:13:37 scarf: It isn't pure, though, because that's not really what it means. 12:13:37 It's still better-looking than the ≝ though. 12:13:38 with less space between the : and hte = 12:13:43 alise: I know 12:13:47 I mean, that one's just a = with a larger smudge above. 12:13:48 fizzie: ugh, that's awful 12:13:53 At the very least it should be ≡. 12:14:02 Definitional equality, propositional equality, ... 12:14:07 if I zoom right in, I can see the word def 12:14:13 Spam, spam, equality and spam... 12:14:16 that's zooming via super-mousewheel, not by making the font bigger 12:14:41 you don't realise how much you were missing super-mousewheel until you get a system where it works 12:14:55 ctrl-mousewheell in os x. 12:14:57 I have no mousewheel, though 12:15:00 and ≡ to me implies congruence rather than definition 12:15:11 Er, right, definitional equality is =. 12:15:16 super-mousewheel works via the touchpad here 12:15:25 ≡ is propositional. 12:15:29 scarf: No mouse at all 12:15:30 ah, ok 12:15:37 alise: heh, you remind me of me 12:15:53 the mouse I have at the moment is basically broken, I need a new one / to stop using the mouse again 12:16:02 I mostly only use it for Enigma, NetBeans, and websurfing as it is 12:16:12 (NetBeans because it doesn't respond to keyboard shortcuts in a sane manner) 12:16:30 I have a mouse just no radio receiving thing for it. 12:16:48 As you know I'm not in my usual residence, so this stuff had to be picked up and the receiver was not. 12:17:01 Should be resolved by today with the amazing solution of "purchasing a mouse" :P 12:17:07 (putting one of the more useful key combos on alt-f1, followed by preventing the usual shortcut keys opening the only menu which has that option on as a command, means you have to use the mouse for some things) 12:19:10 haha: http://www.robweir.com/blog/2010/02/microsoft-random-browser-ballot.html 12:19:21 summary: Microsoft messed up the code for randomizing the order of browsers in their ballot thing 12:19:26 so not all the combinations have equal probabilities 12:20:52 http://www.browserchoice.eu/BrowserChoice/browserchoice_en.htm 12:20:57 What the fuck is a "green" browser? 12:22:10 * scarf follows the tell me more link 12:22:18 I bet they claim to be environmentally friendly, or something 12:22:39 wow, the PNG image on their home page is taking around 10 seconds to load 12:22:39 I thought that too but it doesn't seem so 12:22:46 I don't think I've seen an image load that slowly for months 12:22:50 I like how there's like a few decent browsers and then holy shit obscureathons 12:22:57 and last time, it was goatse, and I managed to click away before more than the top 20 or so pixels loaded 12:23:02 after guessing it was a goatse 12:23:08 so I've seen the top 20 pixels or so of goatse, but no more 12:23:57 http://www.morequick.com/IndexEn.htm <--- wow that's a bad homepage 12:24:35 and a bad browesr 12:24:41 looks like it uses IE's engine 12:24:47 see bottom left of screenshot 12:25:16 heh, that's the IE logo, you're right 12:25:40 yeah like Maxthon and shit they're all the same 12:25:44 take IE engine add shitty UI with tabs done 12:25:50 how can a website called morequick.com load so slowly? 12:26:19 also, the interface looks like it's trying to look like OS X and failing 12:27:04 * scarf clicks on the IE install link 12:27:09 Only the tabs 12:27:09 just because I'm curious as to what will happen 12:27:21 some exe 12:27:25 oh, I get an advert for Windows 7 12:27:28 that's actually sort-of clever 12:27:34 "Internet Explorer 8 is available only on PCs running Windows. Check out Windows 7, which includes Internet Explorer 8." 12:29:37 but I have win7 installed on here (haven't used it for months, though), so if I really wanted IE 8, I could get it like that 12:29:40 http://www.flickr.com/photos/38864566@N00/2479491895/ 12:29:40 this is sweet 12:31:52 ugh, not a still image? 12:31:56 I may have a look when I get home 12:32:09 It couldn't be a still image 12:45:52 I have this sinking feeling that I should do pattern matching on arbitrary function results. 12:45:59 (as opposed to just constructors) 12:46:43 *just constructors 12:47:31 pattern matching reminds me of the old joke about regexes ("now you have /two/ problems") 12:47:47 or maybe the statement about XML being like violence 12:48:02 it's one of those things where, if you start pattern matching you end up needing to use more and more and more of it 12:50:01 Actually pattern matching is just sugar for case expressions which is just half of structural recursion on inductive data types... but what do I know :P 13:05:12 -!- daef has joined. 13:06:49 daef: Are you dæf? 13:06:56 Or just deaf /and/ dyslexic? 13:08:07 hmm, I tried /nick æis523 but Freenode wouldn't let me 13:08:31 Er, isn't it pronounced ay eye ess? 13:08:36 alise: yes 13:08:43 it would be a different word if it were æis523 13:08:47 Right. 13:08:58 sort of like "oklopol" is not pronounced the same way as "oklofok" 13:09:16 alise: ACK 13:09:29 dyslexics are teople poo 13:09:34 daef: Oh, cute, you're one end of a TCP socket! 13:09:40 scarf: nickname = ( letter / special ) *8( letter / digit / special / "-" ) 13:09:54 fizzie: Pah! 13:10:03 fizzie: wow, I'm... amazed and happy that you actually looked that up 13:10:15 fizzie: So what nick does -i use on IRC? 13:10:17 and just as happy but more amazed if you typed it from memoryt 13:10:21 *memory 13:10:30 He looks everything up :) 13:10:39 He is an unstoppable Google machine 13:10:44 scarf: Sorry to deamaze you a bit; it was looked-up. Looking things up is pretty much what I do. 13:10:52 It was from a local file this time, though. 13:11:11 (Is "deamaze" a word?) 13:11:18 fizzie is just a gigantic lookup table 13:11:24 alise: i'm david => dave => daef 13:11:26 not deaf 13:11:31 that's all 13:11:36 Eliezer Yudkowsky isn't sure whether you're conscious, fizzie. 13:11:44 daef: Oh shush you. 13:11:51 I'm allowed to be ridiculous if I feel like it. 13:11:57 kk 13:11:58 alise: I'm not sure of that either; I can't seem to find any good results for it in Google. 13:12:37 You didn't find http://lesswrong.com/lw/pa/gazp_vs_glut/? 13:12:53 He concludes you're not conscious. Ha! 13:13:00 I have foiled you, GLUT! 13:13:17 Is it Schadenfreude if the other party isn't conscious? 13:14:12 I asked the bot what I am, and it just said I'm "a communist irrelevant to any discussion of economics". That wasn't so polite. 13:14:41 :D 13:14:44 alise: do you speak german? 13:14:57 snowplow, grassroots, mobile OE, MPSEB Indian utility co. meter reading, Delhi traffic police, Citibank demo documentation, Disprax (fake screen shots only), Jackson Builders, Aston Villa, NREGA employment census, smnp hardware monitoring, NDPL power, PG Call Home 13:14:57 daef: No, but Schadenfreude is an authentic English word, high-quality import. 13:15:01 kk 13:15:06 Hardly any scratches on the disk. Only slightly pirated. 13:15:28 scarf: I agree. 13:15:44 btw, the "gazp vs glut" thing confuses me, I couldn't get why you'd compare anything but SDL to GLUT 13:15:48 but it seems to be a different GLUT 13:16:08 alise: you can have fun guessing what that list is, btw 13:16:15 as can the rest of #esoteric 13:16:28 although, it's likely to be distinctive enough that Google would turn it up pretty quickly 13:16:59 scarf: GLUT = Giant Look-Up Table 13:17:06 yep, got that from the page 13:17:07 GAZP = Generalised Anti-(P-)Zombie Principle 13:17:17 I was thinking GLUT = GL Utility Toolkit 13:17:27 lol 13:18:19 you can see how confusing that acronym mismatch would make the page title 13:18:34 yes :P 13:18:43 But is a cube... CONSCIOUS???? 13:19:00 alise: as it's GLUT, the question would work better with teapots 13:19:09 I was trying to remember that shape 13:19:24 scarf: anyway - it's just a bunch of triangles 13:19:45 the funny thing is, that the Utah Teapot was accidentally drawn at the wrong scale originally (as in, vertical scale != horizontal scale), so it looks rather different in the demos than it does in real life 13:20:05 that you could also save in a giant lookup table 13:23:12 If the Utah Teapot is conscious, is it a Mormon? 13:24:35 alise: assuming that's an indicative rather than subjunctive if, yes 13:24:41 *rather than counterfactual 13:25:08 Prove that it isn't conscious, you nincompoop! :P 13:25:38 also, subjunctive is a perfectly acceptable term isn't it? 13:27:24 my favourite bit of the GAZP vs. GLUT article is "The obvious answer is that you took a computational specification of a human brain, and used that to precompute the Giant Lookup Table. (Thereby creating uncounted googols of human beings, some of them in extreme pain, the supermajority gone quite mad in a universe of chaos where inputs bear no relation to outputs. But damn the ethics, this is for philosophy.)" 13:27:43 trust Eliezer Yudkowsky to remark on how immoral creating a lookup table can be 13:27:55 Which leads me on to my next question: IS MULTIPLICATION CONSCIOUS???? 13:29:18 what's confusing me here is computational complexity 13:29:48 for instance, what sort of information density would you need to make a lookup table for a human brain? would it become a black hole under its own mass even if it filled the whole observable universe, for instance? 13:30:01 Oh, it would surely be ridiculous. 13:30:05 We have such a small universe. 13:30:48 gah, why can't you upvote IRC comments? 13:31:14 Oh, it would surely be ridiculous. [↑ 1 ↓] 13:31:16 We have such a small universe. [↑ 1 ↓] 13:32:05 hmm, this seems like a perfect feature for ickirc 13:32:28 use CTCP 13:32:33 along with the one that lets you swap nicks with arbitrary other people using ickirc, without notifying the channel (it relays all messages back and forth, etc) 13:32:36 and ofc you'd use CTCP 13:32:37 ^AUPVOTE messageid^A 13:37:29 Feh. 13:43:08 also, http://forums.thedailywtf.com/forums/t/15838.aspx is golden 13:43:30 you know the storm over the australian internet filter, and the person pushing it most filtering out "ISP Filtering" from his own tag cloud with client-side JS? 13:43:38 it's not the only ridiculousness found in the code, it seems 13:43:50 and the code itself was taken from a JS tutorial written by someone unrelated 13:43:55 which person puhsing it most? I am confused 13:43:56 *pushing 13:43:59 ah I see 13:44:16 his name is Stephen Conroy, but that doesn't seem particularly relevant 13:44:28 umm, the minister pushing it, that is 13:45:07 I just couldn't parse your sentence; got it now 13:45:25 uk i'net is censored too :/ just not as badly 13:45:56 alise: the fact is bad enough 13:46:01 Yes. 13:46:10 at least Phorm hasn't been switched on yet 13:46:14 I have plans for if and when it is 13:46:29 I have quite an idea of how it technically works, and it would be fun to mess around with it 13:47:10 Isn't its workings well-known? 13:47:13 yep 13:47:19 well, by people who care to find out 13:47:23 I imagine it isn't well-known in general 13:47:29 because most people haven't bothered to look it up 13:47:30 Phorm seriously freaks me. It's, like, not even your regular Orwellian evil under a corporate disguise. 13:47:43 It's a paper company: something you would expect to see in fiction, down to the logo, website, everything. 13:47:53 we can try things like creating websites where every link goes through exactly 4 HTTP redirects 13:48:03 It's like there is no cover over it other than the ludicrously unbelievable. 13:48:06 which complies with the RFC without Phorm, but fails to comply with it with 13:48:21 heh, howso? 13:48:29 alise: because it uses redirects on every page view itself 13:48:38 and it goes over the redirect-loop limit if you combine the two 13:48:41 right 13:48:54 So would a Phorm-condemned user actually see a redirect on every request? 13:48:57 yes 13:49:04 even if you turn it off, apparently 13:49:07 Hey, lets the ISPs up all their connection speeds and prices. 13:49:13 because the redirect's needed to tell whether it's turned off or not 13:49:18 Meet the new speed, same as the old speed. 13:49:22 Actually, why the hell isn't Phorm illegal? 13:49:37 Wow, Phorm apparently used to (under a different name) produce spyware. 13:49:39 alise: nobody's entirely sure; there's a rumour that the EU's planning to sue the UK for not calling it illegal 13:49:41 I didn't even know that. 13:49:46 (As in, real bona fide non-approved spyware.) 13:50:21 The UK Information Commissioner's Office has voiced legal concerns with Webwise as it is currently implemented, and has said it would only be legal as an "opt-in" service, not an opt-out system. 13:50:21 more fun: phorm impersonates websites to inject cookies into them 13:50:25 I can't remember why, btw 13:50:30 What is it with UK government positions' names and sounding creepy? 13:50:33 Information Commissioner. 13:51:01 alise: I was reading Phorm's website recently, apparently when they turn it on they're planning to redirect pages to ask people whether to opt-in or opt-out 13:51:09 * alise wonders what it is with Wikipedia describing itself and always using the third-person whenever it mentions it 13:51:18 Do they want people to read Wikipedia without the Wikipedia branding in the future or something? :P 13:51:24 It's awkward to read. 13:51:26 alise: there's a page about that 13:51:30 I know. 13:51:33 http://en.wikipedia.org/wiki/Special:Search?go=Go&search=WP:ASR 13:51:38 But I think the "neutrality" just makes the writing feel strange. 13:51:58 the idea's that the articles should have no idea that they're on Wikipedia, or indeed even on a website 13:52:08 so, say, you can make print versions more easily, and fork it more easily 13:53:19 Print can still say Wikipedia. Okay, forking, granted. 13:53:24 But still... 13:53:40 Is forking more important than not confusing people who read it? 13:53:50 My brain does a bit of a double take every time Wikipedia says "the online encyclopedia Wikipedia". 13:55:26 If Phorm is ever switched on I'll not use any ISP that has it. Even if that eliminates all UK ISPs... 13:55:43 At home, at least. 13:55:54 alise: personally, I think it would be fun to screw around with it for a bit before boycotting, especially as my internet connections are (legally) borrowed anyway 13:56:10 Yeah, but what about all my kiddie porn?!?!?!?! 13:56:13 :P 13:56:27 alise: I hope you don't view that sort of thing 13:56:29 Anyway I draw the line at every single HTTP request causing a redirect. 13:56:41 scarf: Must you take obvious ridiculosity as sincere? 13:57:05 alise: well, at least I'm consistent 13:57:14 and it sometimes produces absurd conversations, which can only be a good thing 13:57:18 scarf: Then you are not complete. 13:57:32 alise: I'm not even a type 1 reasoner 13:58:22 whether it's possible to be simultaneously consistent and complete depends on your other assumptinos 13:58:24 *assumptions 13:58:42 Well, I based it on the fact that you said you were consistent. 13:58:52 Presumably that means you've proved to yourself that you're consistent :P 13:59:21 you have to take into account the difference between me believing I'm consistent, me actually being consistent, and me believing myself to believe myself to be consistent 13:59:29 actually, I believe myself to be inconsistent in general 14:00:58 Quotient types are good. The extensional Axiom of Choice is bad. Anything resulting in a bad thing is bad. Quotient types result in the extensional Axiom of Choice. 14:01:41 (But then I don't really believe "quotient types are good" because of that reasoning chain. Perhaps I have some special kind of "undecided" belief that references reasons not to believe it, and pointers to ways to possibly modify the belief so that it is good.) 14:02:14 alise: your use of an in-context "references" followed by an out-of-context "pointers" leads me to believe you're attempting a pun 14:02:17 but I can't find one 14:02:19 maybe it was just a typo? 14:04:12 FYI, the world will end on Tue, August 31st, 4500AD a few minutes before midnight (local time). 14:04:55 this is a crazy and nonserious attempt to deduce a religion from Microsoft Outlook 14:05:19 scarf: no pun no 14:05:21 brb 14:07:32 * scarf reads about people advertising really expensive cables for audio; nothing new, except that they're Ethernet cables designed to transmit audio really, really perfectly or something 14:07:48 with a cable meant for analog, you can sort-of see how people could be fooled into it, but digital? 14:08:25 People don't know how technology works 14:08:29 Analog or digital 14:08:35 I suppose so 14:08:54 "if you do not follow the "directional markings" on the cables, your music will play backwards. Please check that." 14:09:02 people found the website and started giving parody reviews 14:10:03 -!- MissPiggy has joined. 14:11:10 back, with a new keyboard and mouse 14:11:33 ooh 14:11:37 where did you get them from? 14:12:17 Um, ASDA. (My father's house is /also/ in a rather remote place, although not so much so; the nearest place with a supermarket only has one). I only got these because I needed 1, a keyboard with all the keys, and 2, a mouse that works. 14:12:35 (I already had them, I was just plugging them in and what not.) 14:13:14 So, yeah. 14:13:29 This keyboard could do with some weights to hold it into place. 14:13:35 The mouse isn't bad, though. 14:13:51 Not rubbery, sufficiently clicky buttons, and a scroll-wheel. 14:14:09 alise: I love the mental image of a keyboard blowing away in the wind 14:14:15 I am so fucking ill I want to puke 14:14:21 wait no I don't 14:14:21 MissPiggy: Then puke. 14:14:34 scarf: :-) 14:14:39 Those fold-up keyboards might be able to do that. 14:15:17 Ugh, I miss my media keys. (Just for volume control.) 14:16:22 alise: same here, although I bound them to super-combinations 14:16:23 But damn I'm glad I have a mouse. 14:16:29 in particular, I used to use play/pause a lot, now I use super-P 14:17:07 Rubber dome keyboards sure are mushy compared to the old scissor-switch. 14:17:15 But at least I don't have to fingernail keys I picked off now. 14:17:47 Irritating that Emacs cannot display characters I know I have the fonts for. 14:17:53 Even in those fonts. 14:18:13 For instance, ⊤ and ⊥ won't show, even with DejaVu Sans Mono. 14:18:25 WHO CARES 14:18:34 use T and F 14:18:37 MissPiggy: No? 14:18:40 I don't want to. 14:18:46 It worked before in Ubuntu. 14:19:01 alise: which OS are you using atm? 14:19:18 oh, OS X 14:19:20 OS X; the computer with Ubuntu on was too heavy and such to lug across, especially as it doesn't really like Wi-Fi. 14:19:27 (/ctcp version is so much faster than asking a person) 14:19:36 I have Ubuntu here, though. I could boot it up and use it now that I have a mouse. 14:19:46 But Linux on Macs is iffy at the best of times. 14:19:53 yeah :( 14:20:46 Besides, it seems to work alright in other OS X applications. 14:20:56 Bloody Emacs. Maybe a newer build would work. 14:21:33 I'd just use TextEdit, but I need \TeX-style-character-insertion. 14:21:38 -!- BeholdMyGlory has joined. 14:22:33 yol have agda mode? 14:23:19 M-x set-input-mode RET TeX RET. Agda-mode is just an extension of it, one that I ought to get around to downloading. 14:23:26 Well, agda-input, that is. 14:24:56 "David Cameron: We are a modern and radical Conservative Party" —YouTube front page 14:25:02 Radical conservatism! 14:25:58 alise want a good video to watch 14:26:10 Not particularly? 14:27:00 epigram is so cool 14:27:02 and so is agda 14:27:03 and coq 14:27:24 what about Omegamega? 14:28:12 *Ωmega :P 14:28:16 I haven't looked into it. 14:28:26 * MissPiggy doesn't get it 14:30:45 The Ωmega interpreter[1] is a strict pure functional programming interpreter similar to the Hugs Haskell interpreter. The syntax closely resembles that of Haskell but with important differences: 14:30:45 Ωmega is strict (Hugs is lazy); 14:30:45 Support for Generalized Algebraic Datatypes; 14:30:45 Ability to introduce new types; 14:30:45 Allows writing of functions at the type level. 14:30:52 Doesn't sound particularly dependent to me. 14:31:54 also, http://r6.ca/FewDigits/FPdag2008.pdf is officially my favourite introduction to dependent-types-as-logic ever 14:33:12 http://en.wikipedia.org/wiki/List_of_countries_by_coffee_consumption_per_capita 14:33:49 http://en.wikipedia.org/wiki/List_of_countries_by_alcohol_consumption 14:34:03 So what we can tell from this is that when Finns say "vodka" they mean "espresso". 14:36:01 hi alise 14:36:09 Whoa, that's unexpected. I've known that we're not exactly #1 when it comes to alcohol -- despite all the anecdotes -- but I had no idea about the coffee thing. I wonder if that is actually true-true. 14:36:12 alise, so back for good? 14:36:16 :) 14:36:30 AnMaster: Uh, what makes you think that? 14:36:42 The current situation just means I'm sure as hell going to tackle this before even considering returning. 14:37:02 Admittedly, if they have a weapon they'll use it now, and if they don't, I'm free. So I guess you're right, in some sense. 14:37:03 alise, hm? I mean back at home 14:37:04 This is Endgame. 14:37:05 Monday 14:37:11 Returning = to the unit 14:37:17 AnMaster: Oh you don't know the situation do you? 14:37:21 alise, no 14:37:22 well 14:37:27 I'll explain briefly in /msg. 14:37:30 I know what you mentioned before 14:37:32 alise, okay 14:37:49 afterwards I will tell about my very strange journey home today 14:37:55 very strange that thing with the bus 14:38:05 Was it a catbus? 14:38:27 alise, what is that? 14:38:34 http://en.wikipedia.org/wiki/My_Neighbor_Totoro 14:38:41 Or, well, I guess http://en.wikipedia.org/wiki/Catbus is more specific. 14:38:49 ah, not *quite* that strange 14:38:57 but I will recount it. 14:39:16 how can that possibly be not a lolcat reference? 14:39:35 To begin with it was normal, I took the articulated bus from university to the exchange (or whatever it is called, almost all buses pass through that place) 14:39:38 There's also that single-person kittenbus, that's maybe even more... that. 14:39:41 then I was to wait for another bus 14:39:44 still normal 14:39:45 but 14:39:52 then something unusual happened 14:39:58 A very articulate bus. 14:40:04 AnMaster: You TURNED INTO A WALRUS? 14:41:05 instead of the normal "front part low for handicaped/rear part high for packing lots of people" in compromise that that bus usually is, a long range coach thingy arrived 14:41:13 with the right bus number and everything 14:41:25 The SUSPENSE before you said that was INCREDIBLE. 14:41:30 but it got worse 14:41:31 wait for it 14:42:10 well of course I asked the driver and confirmed it was the right bus, and went on it. However later on I saw in the driver mirror the *normal* bus for that line right behind us. 14:42:24 This is so exciting I am literally urinating in my underwear 14:42:26 and when I stepped out of the bus when I arrived, and looked back at the bus I was in 14:42:30 it said "not in traffic" 14:42:31 on it 14:42:34 instead of the number 14:42:35 WHOA 14:42:48 all together I think this is rather strange 14:42:48 You just barely escaped a molestation affair thing, it seems! 14:42:56 fizzie, har 14:43:15 Though perhaps a bus is maybe not the most inconspicuous vehicle for that sort of thing. 14:43:21 fizzie, also the driver nearly made the wrong turn a bit before 14:43:36 AnMaster: once I went the bus which has the right number, but on the way home it took a wrong turn onto the very busy roads which don't go where I want and it was difficult to get home from there 14:43:48 MissPiggy, huh 14:43:51 now every time I go on that bus I am scared it might do that again 14:43:59 clearly this problem would not exist if we had trams 14:44:01 TRAMS! 14:44:06 MissPiggy, maybe it is like here, same number takes different variants of the rout 14:44:07 the perfect vehicle for the transportation of yams 14:44:08 route* 14:44:20 Speaking of buses, they're test-driving this four-door-pairs monster on the 550 line here: http://www.spheros.de/Upload/Images/Presse/Capacity_Aerosphere.jpg 14:44:37 bendy bus 14:45:03 There was something about there being more than one pair of steerable wheels in there. 14:45:04 there was a bit ofa fuss about them ni london because I think they can be a bit dangerous for cyclists 14:45:10 or maybe it was the other way around... 14:45:15 we should have buses that are entirely bendy 14:45:17 like they go through small towns sometimes, and sometimes they go by the 14:45:24 like, the whole bus is in the bendy bit 14:45:26 wheeeeeeeeeeeee 14:45:29 AnMaster yeah it was scary 14:45:30 The catbus is very bendy, I believe. 14:45:44 MissPiggy, well I'm used to this bus taking 5 different variants of the route 14:45:55 MissPiggy, at least I live close to one of the points it take for allmost all routes 14:46:04 Wir fahr'n fahr'n fahr'n auf der Autobahn, wir fahr'n fahr'n fahr'n auf der Autobahn... 14:46:31 anyway another strange thing when boarding it was that it didn't come in to the station/bus exchange from the normal direction 14:46:52 usually it comes in from north, the exchange being the second station from that end of the route 14:47:20 but this one came in from south with "not in traffic", made an U-turn, and changed to the right number 14:47:26 fizzie: Does that thing say METROBUS? 14:47:48 -!- oerjan has joined. 14:48:09 alise, autobhan in Swedish is exclusively used about the "no speed limit" German autobhans. (at least they used to have no speed limit, no idea about nowdays) 14:48:25 It seems to. The picture is non-local, though, just the same model of bus. 14:48:32 Yes. 14:48:34 But I like that song. 14:48:54 alise, anyway this long range bus even had a stoved away seat at the front saying "for guides" on a label 14:49:24 also I think the suspension on it was under dampened, it kept going up and down for a bit after each bump in the road 14:49:39 (is under-dampened the right English term?) 14:49:41 How about the "al forno" and the "resquiat" parts? 14:50:02 * alise quells AnMaster's boring with the computable reals 14:50:04 resquiat means "rest" i think, see "resquiat in pace" (sp) 14:50:05 data ℝ : Set where 14:50:05 ℝ : (f : ℚ⁺ → ℚ) 14:50:05 → {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂} 14:50:06 → ℝ 14:50:06 14:50:06 ι : ℚ → ℝ 14:50:06 ι q = ℝ (λ_ → q) 14:50:13 oh fun 14:50:21 alise: http://isometric.sixsided.org/data/strips/the_left_sister/4.gif 14:50:23 alise, what language is that? 14:50:25 requiescat in pace 14:50:29 haskell? 14:50:33 haskaj 14:50:35 AnMaster: mine. Similar to Agda, though, you could surely make the definition there. 14:50:41 Haskell is nowhere near powerful enough to express that. 14:50:55 but haskal is turing complete! 14:50:59 fizzie: <3 14:51:15 Hasqal 14:51:39 http://en.wikipedia.org/wiki/Al_forno 14:51:43 alise, what does it mean though? It looks like a definition of ℝ. And I guess the mentions of ℚ is for defining the latter as a subset of the former or such? 14:52:11 No. 14:52:16 alise, then what does it mean? :) 14:52:30 A real is represented as a function from a positive rational to a rational. {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂} means: 14:52:40 oh? 14:52:50 For all positive rationals e1 and e2, |f e1 - f e2| <= e1 + e2 14:53:01 alise: resquiat is a late latin corruption, it seems. also, this was italian not latin. 14:53:04 Basically, pi 0.01 = 3.14 14:53:36 alise, and pi 0.001 = 3.142? 14:53:38 This is the computable reals, not the reals, because you can't e.g. have Chaitin's constant. But constructivists don't believe in Chaitin's constant, anyway. 14:53:57 AnMaster: Or similar. 14:54:12 ι : ℚ → ℝ 14:54:12 ι q = ℝ (λ_ → q) 14:54:12 just lets you convert a rational to a real. 14:54:21 For any precision, it yields the rational you give it. 14:54:36 The cool thing is that you cannot pass any function to the real constructor that does not obey the property of {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂}. 14:54:42 3.14159265... <-- what I remember of pi on the top of my head 14:54:44 Don't ask how it works. It's Magic. 14:54:50 alise please make me better 14:55:09 the next digit after that *might* be a 3, not sure 14:55:12 * AnMaster checks 14:55:20 yep, a 3 14:55:25 MissPiggy: BAZAM 14:55:26 Done. 14:55:27 It's 3 unless you round it to that length. 14:55:31 thanks 14:55:36 ;_; 14:55:38 * MissPiggy cry cry cry 14:55:46 MissPiggy: What, precisely, is the problem? 14:55:50 I think mooz bothered to memorize 50 or 100 digits or so. I'm not sure why. 14:55:53 alise I have a bad cold 14:56:06 alise: I can do 3.14159265358 14:56:06 fizzie, well yes 14:56:10 * AnMaster: 14:56:11 (about the 3 and rounding) 14:56:11 AnMaster: ...3589797... from my top of head 14:56:12 MissPiggy: Sucks to be you; I hate colds. 14:56:19 scarf, ? 14:56:21 wait 14:56:26 3.14159 is as much as I know; I'm a dullard. 14:56:27 alise me too the worst thing is I had 100% attendence up until today 14:56:33 that last 7 shouldn't be there 14:56:49 (unless it's accidentally right) 14:56:50 http://isometric.sixsided.org/data/strips/the_left_sister/dropin2.php ;; I really ought to read isometric comics more than just when fizzie links to them 14:56:59 MissPiggy: cute, like oklopol 14:57:02 3.141592653589793238462643383279502884197169399375105820974944592307816406286208 14:57:03 alise, I have to think a few seconds to remember past 3.14159. It goes like "uuh... ah yes, 2 then 65" 14:57:05 that's all I can remember 14:57:08 angry that he got his first 4 instead of a 5 on a test :) 14:57:17 MissPiggy: Yeah. Right. 14:57:26 alise it's true 14:57:58 http://isometric.sixsided.org/data/strips/the_left_sister/19.gif 14:58:04 and I even got it all right! 14:58:04 AnMaster: ...3589797... from my top of head <-- checking gives that as "793" not "797" indeed 14:58:09 but then that could be rounted 14:58:12 alise you don't beleive me :| 14:58:14 since I checked M_PI 14:58:18 MissPiggy: I find it unlikely. 14:58:24 alise I am not lieing 14:58:25 But I do not rule out the possibility entirely. 14:58:50 wait, that makes no sense 14:58:58 M_PI has more precision in the header 14:58:58 AnMaster: hard to roung 3... to 7, alas :D 14:59:01 *round 14:59:06 * AnMaster slaps printf 14:59:09 :( 14:59:12 i am just chased by muphry's law today 14:59:13 http://isometric.sixsided.org/data/strips/the_left_sister/24.gif 14:59:15 oerjan, well yes 14:59:15 I'll stop now 14:59:18 oerjan, unless it is very cold 14:59:27 wait what 14:59:35 alise all I know of phi is 1.618033989 14:59:43 alise and of e 2.718281828 14:59:49 2.718281828459045 14:59:54 Panels 28 onwards are missing, fizzie bot :( 14:59:55 that forms a really memorable pattern 15:00:02 I should memorize more e 15:00:19 scarf, errr... e? 15:00:22 alise: I know, but my lookup table has gotten damaged and I cannot reconstruct them either. 15:00:31 scarf, I remember 2.718 of e 15:00:32 AnMaster: yes, e 15:00:32 ℝ (λ ε → product (map (λ i → (i!)⁻¹) (0 … ε))) 15:00:34 really bad at that 15:00:35 I've memorised all of e! 15:00:39 alise, XD 15:00:44 Or, if you prefer fancier notation, 15:00:57 ℝ (λ ε → ∏ 0 … ε ⇒ λi → (i!)⁻¹) 15:01:06 well since it is transcendental, iirc every pattern of numbers will be found somewhere in it? 15:01:11 wasn't it something like that 15:01:19 No. 15:01:24 That's normal. 15:01:27 AnMaster: no, that isn't an implication 15:01:31 or was that property even more specific than transcendental? 15:01:35 Yes. 15:01:38 right 15:01:39 that's more specific than transcendental 15:01:48 what was it called now again? 15:01:52 there are definitely transcendentals which are normal. iirc 0.101001000100001... is one 15:01:54 the first proved-trancendental number had no digits in its decimal expansion than 0 and 1 15:01:57 http://en.wikipedia.org/wiki/Liouville_number 15:01:58 *which are _not_ normal 15:02:00 scarf: yeah 15:02:11 * oerjan swats muphry -----### 15:02:32 *other than 15:02:40 so, did pi and e have that extra property or not? I don't remember 15:02:49 what extra property? 15:02:59 the one mentioned just above -_- 15:03:00 and there _might_ be normals which are not transcendental, i think the guess is all non-rational algebraic numbers are normal, but no one knows for even a single one 15:03:05 0.101001000100001 is normal? 15:03:13 .... 15:03:17 i _think_ all _known_ normal numbers are explicitly constructed to be so 15:03:42 MissPiggy: muphry is chasing me around today, i said 15:03:42 oerjan, ah 15:03:57 what's muphry 15:04:06 oerjan, this isn't the first instance? 15:04:13 MissPiggy, you have to be kidding 15:04:24 ? 15:04:28 MissPiggy: the law that all corrections of other people's typos or grammar mistakes themselves contain typos or grammar mistakes 15:04:34 MissPiggy, http://en.wikipedia.org/wiki/Murphy%27s_law 15:04:48 MissPiggy: transcendental. actually maybe you need more 0's between 15:04:53 AnMaster: fail 15:04:54 AnMaster: that's the most ridiculous typo I've seen on this subject for a while 15:04:55 AnMaster: no, Muphry 15:05:04 scarf: I expect AnMaster just had a gigantic whooooooooooosh 15:05:08 and honestly didn't get it 15:05:10 alise, oh I didn't notice the extra r 15:05:13 alise: lasting several months? 15:05:14 XD 15:05:15 AnMaster: doublefail 15:05:24 argh 15:05:26 moved r then 15:05:29 ths is all my fault 15:05:31 AnMaster: also, i missed a pi digit, and misspelled round 15:05:35 MissPiggy: fault? this is hilarious! 15:05:42 this is sparta! 15:05:44 :( 15:05:51 ccccccxxxxxzzzzzzaaaaaaaa 15:06:15 what did the sparta thing... oh right "this is hilarious!" 15:06:31 I really didn't think of "this is sparta" when reading that... 15:06:42 * MissPiggy reads everything alise says in that voice 15:06:59 i am a wonderful feminine creature! 15:07:06 MissPiggy, what about "this is fun"...? does that also make you think of sparta? 15:07:09 yes you are 15:07:21 no AnMaster 15:07:49 scarf: i may be overextending muphry's law here, using it for any error involving mistyping 15:08:02 MissPiggy, weird 15:08:18 oerjan: I like it when maths people both (a) only know a few specially normal numbers, yet (b) have a proof that almost all numbers of normal, especially since it involves the so vague-sounding yet sensibly defined "almost all". 15:08:30 :P 15:08:32 Muphry's law is an adage that states that "if you write anything criticizing editing or proofreading, there will be a fault of some kind in what you have written". 15:08:38 fizzie: yeah 15:08:41 oerjan: In any case MathWorld agrees with your assessment that currently known normal numbers are "artificially constructed". 15:08:45 that was funny fizzie 15:08:46 "Most numbers that aren't pathological are probably normal"\ 15:08:48 *normal" 15:11:18 alise, opinison please http://www.reddit.com/r/programming/comments/b7neu/what_are_some_exciting_areas_for_computer_science/c0ldm41 15:11:23 MissPiggy: ah yes the liouville's constant 0.110... etc. requires more than just linear number of zeros (it's sum of 10^(-n!)) 15:11:39 MissPiggy: did you write that or sth? 15:11:44 alise, sth. 15:11:45 not sure what kind of opinion you want 15:11:51 MissPiggy: i refuse to apologise :) 15:12:39 [[Formal verification]] of computer programs. 15:12:45 You "simply" write a proof that your program is correct (including that it can't crash). Then you run the proof through a [[proof checker]] computer program. 15:12:51 I know what it says. 15:12:55 just seems a bit patronizing... 15:13:12 but maybe it's just my wiki-hate 15:13:20 well the terminology is a bit oversimplified 15:13:27 ...also i still don't get why you hate wikipedia 15:13:39 see [[wikipedia]] 15:13:41 or google it 15:13:47 ^ that's why 15:14:04 so you'd link to another source, even if it would be less helpful? 15:14:11 -_ 15:14:16 MissPiggy: ah yes the liouville's constant 0.110... etc. requires more than just linear number of zeros (it's sum of 10^(-n!)) <-- should that be read as "sum sign (but unicode fail preventing the proper symbol)"? 15:14:22 anyway nobody said dependent types so foo to that link 15:14:33 AnMaster: no? 15:14:36 alise well the question is "What are some exciting areas for computer science related research?" 15:14:40 what a stupid question! 15:14:42 turns out he was talking english 15:15:12 MissPiggy: i'm really not interested in engaging in CSnerdrage no matter how stupid the question is... I didn't click when i saw it on proggit because I knew the answers would suck 15:15:13 alise, weird. A mathematican not using the shortest possible symbol to talk about math!? 15:15:14 AnMaster: i don't do unicode, so no 15:15:21 mathematician* 15:15:30 AnMaster: you realise that a lot of mathematics is done with words? 15:15:31 or well, yes 15:15:36 formally verified proofs aren't really the done thing 15:15:39 or even totally formal proofs 15:15:39 alise, of course -_- 15:15:59 alise you totally missed the point :| 15:16:08 indeed 15:16:20 alise, whooooooooooooooooooooooooooooooooooooooosh 15:16:23 just fyi 15:16:25 -!- MigoMipo has joined. 15:16:40 XD 15:17:16 ∞ -j! 15:17:16 c = ∑ 10 15:17:16 the point is that linking to [[wikipedia]] every second word, like some kind of [[blogger]] is just completely unhelpful 15:17:17 j=1 15:17:21 impossible, AnMaster cannot whoosh anyone, fundamental physical law 15:17:24 food -> 15:17:25 AnMaster: a joke is only funny if it has some basis in fact 15:17:43 alise, ever heard about stereotypes? 15:17:50 a joke based on a popular ignorance has to mock it to a large degree 15:18:02 rather than simply take it for granted and then following the usual "joke based on fact" process 15:18:15 i'm starting to wonder if perhaps swedish culture has no jokes at all 15:18:21 ffs, just admit you missed the point. 15:18:25 but of course you can't 15:19:04 "Just admit that you're wrong! I don't care if you're right, just concede once in a while!" 15:19:09 Yawn. Boring. Go away. 15:19:15 lol 15:19:15 15:17 < alise> i'm starting to wonder if perhaps swedish culture has no jokes at all 15:19:50 "My hovercraft is full of eels!" "You have a HOVERCRAFT? Why the fuck did you let eels into it? Jeez." 15:20:27 alise: that's hilarious, and I don't know why 15:21:29 "If all the things you sell have lots of spam in, you should call it a Spam Restaurant or something. And why are you saying spam multiple times?! Also, that singing gimmick is off-putting." 15:22:11 -!- asiekierka has joined. 15:22:11 hi 15:22:16 "Well, swallows fly at different speeds at different times and in different situations, I'd imagine. So I couldn't answer that question, but then again, nobody else can. So I'd say that the error is on /your/ part, for asking a question that is not meaningful." 15:22:33 i'm reading about neural networks 15:22:37 gah, now I'm trying to remember, I actually looked it up 15:22:39 was it 18 mph? 15:24:40 -!- alise has changed nick to ceiiinosssttuv. 15:24:49 ceinostuv? 15:24:51 what is this even 15:27:11 -!- ceiiinosssttuv has changed nick to alise. 15:27:13 that lasted long 15:27:58 scarf, African swallow? 15:27:59 alise: swedish jokes mainly consist of taking norwegian jokes about swedes, and swapping the norwegian and swedish characters. hope this helps. 15:28:12 oerjan, NO! it is the other way around 15:28:12 AnMaster: no, european; there's insufficient data on african swallows 15:28:16 AnMaster: I was about to say, dammit :P 15:28:18 AnMaster: LIES 15:28:20 you steal our jokes about you 15:28:36 I should live on the Swedish-Norwegian border; it would be /rad/ 15:28:42 please tell me that the /only/ norwegian joke is the one that oerhan just gave 15:28:45 *oerjan 15:28:48 then it would be perfect 15:28:58 :D 15:29:12 scarf, alas no. 15:29:21 well 15:29:24 could be for Norway 15:29:31 but have lots more about them :P 15:30:03 wow there is a site dedicated to them... 15:30:06 http://norgehistorier.se/ 15:30:17 oerjan, now don't steal those and swap things :P 15:30:46 Our nationality-related jokes generally tend to have a triplet; a Finn, a Swede and a Norwegian. 15:30:51 anyway that on that front page is quite representative of the general style of them 15:30:57 i raise those with http://www.svenskevitser.com/ 15:31:14 fizzie, oh we have those style too. But usually Bellman, a German and a Norwegian 15:31:23 fizzie: we usually use a dane instead of a finn 15:31:29 why Bellman I have no idea 15:31:48 but we also have jokes about the finns, whose main character is _always_ called Pekka 15:31:58 oerjan, of course 15:32:08 (and secondary character is frequently called Toivonen) 15:32:29 oerjan, and all Norwegians går på tur 15:32:42 (which is a strange way to say that they are skiing) 15:32:43 ut på tur, aldri sur 15:32:51 oerjan, haven't heard that 15:32:59 I believe that taking a walk through the rain without an umbrella illustrates this concept quite satisfactorily. 15:33:06 um no that would be skitur. a tur alone may be just walking. 15:33:15 or even be a båttur 15:33:27 oerjan, gå på båttur? 15:33:28 oerjan: The interwebs tell me the characters in those jokes are supposed to be Pekka and Jorma. (But that's from a draft of a paper from a Finnish university docent.) 15:33:29 wth 15:33:33 fizzie: who's the stupid one in that triplet? 15:33:43 oerjan, or do you have gå = go? sv:gå = en:walk 15:33:49 typical for English nationality jokes is to have an Englishman, a Scotsman, and an Irishman 15:33:51 AnMaster: i guess the verb would be "dra" rather than "gå" in that case 15:34:00 oerjan, right 15:34:11 and the typical pattern is for the Englishman and Scotsman to both behave sensibly but differently, and then the Irishman to do something stupid 15:34:37 scarf: Occasionally the Finn; if not that, then both the others. 15:34:49 -!- coppro has quit (Ping timeout: 248 seconds). 15:34:50 "Vet du varför norrmänen har ett sandpapper ut i öknen? De tror att det är en karta!!" → "Do you know why Norwegians take a sand paper with them in deserts? Because they think it is a map" 15:34:56 very typical of the style 15:35:05 * oerjan is annoyed that google has started garbling its links with redirecting through itself. now i have to _visit_ the sites to easily paste their links. 15:35:05 * scarf wonders what those jokes are like in Scotland 15:35:23 scarf, what about Wales? 15:35:41 AnMaster: that's also worth wondering about 15:35:47 15:33 < scarf> typical for English nationality jokes is to have an Englishman, a Scotsman, and an Irishman 15:35:50 scarf, this ^ 15:35:58 MissPiggy: ? 15:36:03 in scotland 15:36:10 also, the browser history button has become buggy :( 15:36:24 thing is we don't even swap the characters around we just repeat them verbatim 15:36:31 oh this was was quite good (translated): "Do you know why there will be a war between Norway and Sweden in 100 years? Answer: Because that is when then get our jokes." 15:36:33 oerjan, ^ 15:36:40 lol 15:37:29 MissPiggy: well, that sort of English joke is not uncomplimentary towards the Scottish at all, so I don't see why there'd be a need to change it 15:38:21 fizzie: i haven't even _heard_ the name Jorma, may be something recent 15:38:56 I believe that taking a walk through the rain without an umbrella illustrates this concept quite satisfactorily. <-- as long as you don't dance while doing it 15:39:51 AnMaster: brilliant. you don't even need to switch anything :D 15:40:14 oerjan, har! 15:40:31 yeah that one works both ways 15:40:53 oerjan, oh you mean it didn't say which nationality at all 15:41:02 (that was "we") 15:41:16 yeah 15:41:43 oerjan, well, if it is against the Norwegians, then it is clearly them who are stupid. But if it is used against the Swedish, it is obviously meant to be read as "Norwegian jokes are so far fetched" 15:41:43 :P 15:41:56 _obviously_ 15:42:16 oerjan, see it works both ways both ways! 15:42:22 (not a typo) 15:42:48 anyone know much about SCTP here btw? 15:43:57 AnMaster: btw the same joke about the war is essentially no. 5 on svenskevitser.com 15:44:24 although generously with only 40 years 15:44:38 oerjan, see, we are way smarter than you! 15:44:39 clearly, Sweden's going to attack first 15:44:51 scarf: ooh 15:45:38 scarf, I doubt it. By that point the gov will have cut the army funds so we have 2 soldiers (hey at least that is one more than Lancre!) 15:47:06 well still, don't go to work against Lancre. i hear their grannies are something fierce. 15:47:10 *war 15:47:29 * oerjan beats Muphry with the saucepan ===\__/ 15:49:16 oerjan, indeed 15:50:24 -!- cpressey has joined. 15:53:48 oerjan: that's old 15:54:02 alise: what's old? 15:54:05 your old 15:54:17 both of you 15:54:52 what about our old 15:55:08 what about my old 15:55:19 AnMaster: is cutting the army funds really a big problem? 15:55:20 how will it survive in the cold? 15:55:24 it's not like anyone's bombing sweden :P 15:55:34 i forgot what was old XD 15:57:27 cpressey, hi there, what do you think of this very early draft for a replacement for SOCK/SCKE (which have a number of issues, such as unix sockets being impossible due to the flag being below the address, and the address being either an ipv4 ip in one cell, or a 0gnirts, which means you can't know which format it is in): http://sprunge.us/OJFX 15:59:05 alise: the cutting of the army funds before WW2 was a big issue in norway... 15:59:41 sweden wisely had not done so, and weren't invaded. or something like that. 15:59:53 yes, it's before ww2 15:59:58 oerjan, actually we had cut them somewhat too, but not as much iirc 16:00:23 oerjan, nowdays, Sweden is worse off 16:02:43 mhm 16:06:36 `quote 16:06:49 31|IN AN ALTERNATE UNIVERSE: In an alternate universe, I would say "In an alternate universe, ehird has taste" 16:07:09 `quote 16:07:10 125|Note that quote number 124 is not actually true. 16:07:18 `quote 124 16:07:19 124| I cannot eat meat that isn't flat. 16:07:29 `quote 16:07:30 31|IN AN ALTERNATE UNIVERSE: In an alternate universe, I would say "In an alternate universe, ehird has taste" 16:07:32 XD 16:07:32 `quote 16:07:33 1| I've always wanted to kill someone. >.> 16:07:35 `quote 16:07:36 121| My mascot is a tree of broccoli. 16:07:36 `quote 42 16:07:37 42| after all, what are DVD players for? 16:07:37 `quote 16:07:39 22|IN AN ALTERNATE UNIVERSE: First, invent the direct mind-computer interface. Second, learn the rest with your NEW MIND-COMPUTER INTERFACE. 16:07:42 `quote 16:07:43 78| ??? Are the cocks actually just implanted dildos? Or are there monster dildos and cocks? Or are both the dildos and cocks monster? 16:07:53 `quote 16:07:53 is there any way to get quotes by a particular person? 16:07:54 100| Warrigal: what do you mean by 21? 16:07:58 `quote 84 16:08:00 84| Porn. There, see? 16:08:02 scarf: yes, use sgeo's text file of them 16:08:04 and grep it 16:08:04 `quote 81 16:08:05 81| What is there to talk about besides gay slang? 16:08:06 ping Sgeo link us 16:08:09 oh he's not here 16:08:16 I am 16:08:20 *GASP* 16:08:26 oh 16:08:28 link us to the file 16:08:30 plz kthx 16:08:43 Hold on 16:08:46 `quote 16:08:47 98| ehird: every set can be well-ordered. corollary: every set s has the same diagram used from famous program talisman with fnord windows to cascade, someone i would never capitalize " i" 16:08:52 `quote 3 16:08:53 3| EgoBot just opened a chat session with me to say "bork bork bork" 16:08:56 `quote 5 16:08:57 5| Hmmm... My fingers and tongue seem to be as quick as ever, but my lips have definitely weakened... More practice is in order. 16:09:00 `quote 7 16:09:00 7| that's where I got it rocket launch facility gift shop 16:09:02 `quote 16:09:03 1| I've always wanted to kill someone. >.> 16:09:03 `quote 11 16:09:05 11| TODO: sex life 16:09:06 `quote 13 16:09:07 13|* ehird has joined #lobby hmmm clean me 16:09:10 `quote 17 16:09:11 17| :d <(I can lick my nose!) 16:09:12 Gregor: your random number generator is either too good or too bad 16:09:12 `quote 18 16:09:13 18| GregorR-L: i bet only you can prevent forest fires. basically, you know. 16:09:16 `quote 16:09:17 71| If I ever made a game where you jabbed bears ... I'd call it jabbear. 16:09:19 `quote 16:09:20 18| GregorR-L: i bet only you can prevent forest fires. basically, you know. 16:09:20 http://209.20.80.194/sgeo/quotes.txt 16:09:25 Sgeo_: thx 16:09:27 scarf: ^ 16:09:28 yw 16:09:30 http://209.20.80.194/sgeo/quotes.txt 16:09:36 * cpressey rubs eyes 16:09:40 It's Monday morning and alise is here? 16:09:42 `quote 16:09:45 57| `translatefromto hu en Hogy hogy hogy ami kemeny How hard is that 16:10:02 cpressey: It's Complicated(TM). 16:10:11 how do you add extra quotes 16:10:17 Yay! Complicated(TM)! 16:10:23 asiekierka: NOBODY TELL HIM 16:10:51 I will give cake to the first person that does 16:10:53 AnMaster: I'll try to look at after I regain consciousness 16:11:14 cpressey: tl;dr a larger, but much less straining crisis is currently happening and I don't have the strength to keep up the regular facade until it is resolved... so I'm not attending. Of course if they're right about being able to section me this won't last long. 16:11:22 But I think there's an awful lot of bluff to that statement. 16:11:31 cpressey: You're a p-zombie?! 16:11:32 AAAAAAAAA 16:11:41 MIIIIIIIIIIIINDS 16:11:41 wait 16:11:48 forgot to do something today 16:11:49 what was it... 16:12:29 oh, right! 16:12:40 -!- asiekierka has set topic: 0 days since last topic change | 0 days since last alise sighting | For those who don't know: INTERCAL is basically the I Wanna Be The Guy of programming languages. Not useful for anything serious, but pretty funny when viewed from the outside. | cpressey: You're a p-zombie?! | http://tunes.org/~nef/logs/esoteric/?C=M;O=D. 16:13:04 -!- alise has set topic: alise sighting counter currently out of order | http://tunes.org/~nef/logs/esoteric/?C=M;O=D. 16:13:05 AnMaster: I'll try to look at after I regain consciousness <-- what happened? 16:13:08 * Sgeo_ really needs to go wash some clothes and get ready for school 16:13:41 The washer in the house is broken but the dryer works fine. Every morning, I just wash what I need >.> 16:14:21 Nothing special, just Monday morning. 16:14:33 cpressey: Have you tried PURE CAFFEINE? 16:15:10 `quote 16:15:11 70| Gregor is often a scandalous imposter. It's all the hats, I tell you. 16:15:14 `help 16:15:15 Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ 16:15:15 scarf: also 16:15:17 `quote oklopol 16:15:18 48| i can get an erection out of a plank, you can quote me on that. 50| 16:15:23 there is a ... sort of search. 16:15:32 `run quote oklopol 16:15:33 48| i can get an erection out of a plank, you can quote me on that. 50| 16:15:35 Is HackEgo secure? 16:15:36 alise: oh, I just scammed BlogNomic back into existence; we'd been playing a different nomic for the last 4 years, but it just took one blog post (not even a proposal) to fix it 16:15:41 asiekierka: no, you could root it if you wanted 16:15:43 please don't 16:15:48 scarf: wow, what happened? 16:15:50 scarf, linky? 16:15:51 :( 16:15:58 i just wanted to do, uh 16:16:01 run sudo rm -rf / 16:16:05 http://blognomic.com/archive/the_switch_never_happened/ 16:16:06 with an ` at front 16:16:40 asiekierka: Please don't. 16:16:45 It's an honour system bot. 16:16:49 as in? 16:16:50 You can do whatever you want. 16:16:53 but? 16:16:57 alise: I thought it had protection against that sort of thing 16:16:59 But please don't abuse it. 16:17:01 scarf: nope 16:17:03 for one thing, how would you enter the sudo password? 16:17:05 ah 16:17:10 !sh sudo rm -rf / 16:17:16 you mean `run 16:17:16 /tmp/input.18678: line 1: sudo: command not found 16:17:17 I know EgoBot is protected against that 16:17:18 scarf: you can easily elevate to root. also, that's egobot not hackbot 16:17:25 alise: yep 16:17:31 scarf, you really really mean `run 16:17:34 alise: can't you always revert such a change? 16:17:42 oerjan: not necessarily 16:17:45 `run ls 16:17:46 bin \ cube2.base64 \ cube2.jpg \ help.txt \ hentai \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ share \ test.sh \ tmpdir.18724 16:17:47 scarf: rm -rf / --no-protect-root 16:17:48 asiekierka: I was testing out a different bot, which was protected 16:17:50 works better 16:17:51 daef: I know 16:17:53 `run rm porn.jpg 16:17:54 No output. 16:17:57 but I normally omit that last bit 16:18:04 TRI-F TIME 16:18:21 What's this about protecting root? 16:18:36 Sgeo_, tree huggers going insane! 16:18:38 that's what 16:18:45 `help 16:18:45 Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ 16:18:53 `cd / 16:18:55 No output. 16:18:58 `ls 16:18:59 bin \ cube2.base64 \ cube2.jpg \ help.txt \ hentai \ huh \ paste \ poetry.txt \ quotes \ share \ test.sh \ tmpdir.18973 16:19:07 `cd / && ls 16:19:07 No output. 16:19:08 asiekierka, it doesn't keep that state 16:19:12 scarf, need run 16:19:14 can i remove one more thing 16:19:15 `run cd / && ls 16:19:16 bin \ dev \ etc \ home \ lib \ lib64 \ proc \ tmp \ usr 16:19:23 asiekierka: sure. 16:19:29 we allow one destructive change. just takes a few hours to put back 16:19:35 ok 16:19:48 go for it 16:20:07 `run rm -r hentai 16:20:08 No output. 16:20:11 `ls 16:20:12 bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ quotes \ share \ test.sh \ tmpdir.19164 16:20:15 Oh my god, you removed the vital file 16:20:20 That was the core system file for the sandbox 16:20:20 I said 16:20:23 "TRI-F TIME" 16:20:25 What the fuck man 16:20:28 Ugh 16:20:28 TRI-F being FAMILY FRIENDLY FILTER 16:20:35 Gregor: Shut down the bot please, it's exposed 16:20:43 asiekierka: You realise that now that's removing files on /Gregor's hard disk/? 16:20:51 `file * 16:20:51 hentai was the pointer to the outer system. 16:20:52 You said "one destructive change" 16:20:52 *: ERROR: cannot open `*' (No such file or directory) 16:20:56 err 16:21:13 `run file * | tr '\n' '-' 16:21:14 asiekierka: Yes, but not catastrophic change 16:21:15 bin: directory-cube2.base64: ASCII text-cube2.jpg: JPEG image data, JFIF standard 1.01-help.txt: ASCII text-huh: ASCII English text-paste: directory-poetry.txt: ASCII text-quotes: directory-share: directory-test.sh: ASCII text-tmpdir.19248: directory- 16:21:21 err? 16:21:21 How could I know it'd be so catastrophic 16:21:25 `run echo "This is a file." > porn.jpg 16:21:25 `run file * | tr '\n' '|' 16:21:26 No output. 16:21:26 bin: directory|cube2.base64: ASCII text|cube2.jpg: JPEG image data, JFIF standard 1.01|help.txt: ASCII text|huh: ASCII English text|paste: directory|poetry.txt: ASCII text|quotes: directory|share: directory|test.sh: ASCII text|tmpdir.19310: directory| 16:21:27 maybe 16:21:29 `ls 16:21:29 that works better 16:21:30 bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ share \ test.sh \ tmpdir.19376 16:21:30 You could name it "TOTALLY_UNIMPORTANT_FILE_ROTFLMAO" 16:21:48 asiekierka: You could have looked at the file before deleting it. 16:22:00 I guess we just won't have HackEgo any more, then, if people can't be trusted with it 16:22:08 You mean: I can't be trusted with it 16:22:13 `run file * | tr '\n\t' '| ' 16:22:14 bin: directory|cube2.base64: ASCII text|cube2.jpg: JPEG image data, JFIF standard 1.01|help.txt: ASCII text|huh: ASCII English text|paste: directory|poetry.txt: ASCII text|porn.jpg: ASCII text|quotes: directory|share: directory|test.sh: ASCII text|tmpdir.19427: directory| 16:22:14 just block me from doing anything harmful and you're ok 16:22:16 er? 16:22:22 err* 16:22:24 asiekierka: We prefer people to be responsible, usually. 16:22:37 `ls 16:22:38 bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ share \ test.sh \ tmpdir.19470 16:22:41 `cd / && ls 16:22:43 No output. 16:23:00 what's happened? 16:23:01 `run cd / && ls 16:23:02 bin \ dev \ etc \ home \ lib \ lib64 \ proc \ tmp \ usr 16:23:04 `cat poetry.txt 16:23:05 A Poem -- Roses are red, violets are free. In Soviet Russia, you love me. 16:23:19 MissPiggy: I accidentally removed the mislabeled most vital file on gregor's hard drive 16:23:23 Happy? 16:23:30 `cat porn.jpg 16:23:30 This is a file. 16:23:33 Wait, guys 16:23:38 Is there no UNDELETE on this system 16:23:42 COME ON, EVEN MS-DOS HAD IT! 16:24:21 Is this ext2 or ext3 16:24:37 alise, see /msg 16:24:40 asiekierka shut up 16:25:00 `run mount | tr '\n' '|' 16:25:01 rootfs on / type rootfs (rw)|none on /sys type sysfs (rw,nosuid,nodev,noexec)|none on /proc type proc (rw,nosuid,nodev,noexec)|udev on /dev type tmpfs (rw,size=10240k,mode=755)|/dev/disk/by-label/PRGMRDISK1 on / type ext3 (rw,errors=remount-ro,data=ordered)|tmpfs on /lib/init/rw type tmpfs (rw,nosuid,mode=755)|tmpfs on /dev/shm type 16:25:34 `cal 16:25:35 March 2010 \ Sa Su Mo Tu We Th Fr \ 1 2 3 4 5 \ 6 7 8 9 10 11 12 \ 13 14 15 16 17 18 19 \ 20 21 22 23 24 25 26 \ 27 28 29 30 31 \ 16:26:11 `run mount | tail -n 2 | tr '\n' '|' 16:26:12 proc on /var/chroots/egobot/proc type proc (rw)|/sys on /var/chroots/egobot/sys type sysfs (rw)| 16:26:17 hm 16:26:28 asiekierka: gregor's an op here you know 16:26:35 you'll prolly be banned he doesn't like people abusing hackego 16:26:40 What? 16:26:41 especially when it affects the host machine 16:26:46 You told me i can do one destructive change 16:26:50 You didn't specify anything else! 16:26:53 ` head /dev/urandom > sex.jpg 16:26:54 yes, i didn't think you'd try that one. 16:26:54 No output. 16:27:01 Actually I assumed it's YOUR bot 16:27:03 /usually/ people have some kind of discretion 16:27:03 `run head /dev/urandom > sex.jpg 16:27:04 No output. 16:27:09 asiekierka: no. i do have root access to it though 16:27:10 alise what happened 16:27:12 `cat sex.jpg 16:27:13 No output. 16:27:55 * Sgeo_ decides to end asiekierka's suffering 16:27:59 noooo! 16:28:00 Yay! 16:28:04 `yes 16:28:05 y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y \ y 16:28:05 Wait 16:28:05 Sgeo_: don't restore the files 16:28:07 what does that mean? 16:28:10 it'll break it 16:28:14 the file is symbolicly defined 16:28:17 asiekierka, you fail at reading 16:28:20 ie a pointer to the host machiine 16:28:21 that is what alise means 16:28:29 so you'll overwrite the drive if you write to hentai again 16:28:30 `echo $PATH 16:28:31 $PATH 16:28:35 -_- 16:28:38 oh, deleting a symlink isn't particularly problematic 16:28:39 Ok, n/m 16:28:40 `echo "$PATH" 16:28:41 "$PATH" 16:28:49 scarf: but it's not a symlink 16:28:53 it's a fileptr3 16:28:56 i.e. an ext3+ field 16:29:07 containing symbolic references to the filesystem it's embedded in 16:29:08 scarf, what about the magic symlinks in /proc that points to inodes or something? 16:29:11 `sudo apt-get install cowsay 16:29:12 No output. 16:29:19 rather than actual files. (if the file is open but deleted) 16:29:20 `ls 16:29:21 bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ sex.jpg \ share \ test.sh \ tmpdir.20271 16:29:25 Uh-oh 16:29:28 AnMaster: /proc has a separate filesystem just for that 16:29:30 FAMILY FRIENDLY FILTTtttt---*ban* 16:29:34 `cowsay lol 16:29:35 No output. 16:29:42 asiekierka: stop being a jerk 16:29:42 What's a cowsay? 16:29:45 scarf, true. But it is somewhat confusing. The semantics I mean 16:29:56 * Sgeo_ needs to attend to clothing stuff now >.> 16:30:02 F³?# 16:30:06 s/#// 16:30:15 scarf: yeah 16:30:45 alise, ext3+? 16:30:46 F₃₌ too, though 16:30:55 for the equalising properties in the host fileptr3 16:31:10 `run file sex.jpg 16:31:11 sex.jpg: empty 16:31:14 hentai was F₃⁺, so the safety features are off (so that a direct pointer could be made) 16:31:18 alise, see /msg 16:31:25 AnMaster: that fix won't work 16:31:32 !bf ,[.,]!`run X='!bf ,[.,]!`run' echo $X "X='$X'" 16:31:44 F₃⁺s don't have the Ωγ-base property 16:31:45 umm, EgoBot? 16:31:52 scarf: shit, it must have overwritten that segment too 16:31:53 alise, no, but upgrade to ext4+. Or did they rename it ext5 yet? 16:32:02 EgoBot is jealous that everyone hax0rs HackEgo but nobody touches EgoBot 16:32:05 AnMaster: well i wouldn't do anything without Gregor telling me to 16:32:07 ...unlike asiekierka 16:32:08 * alise sighs 16:32:17 * asiekierka shgis 16:32:30 i think he's being a real dick not taking this seriously 16:32:36 any objections to me just banning him now? 16:32:36 who? 16:32:38 asiekierka 16:32:50 No 16:32:51 alise, you have op nowdays? 16:32:54 yeah 16:32:57 I should be scared 16:33:00 hehe 16:33:00 assqueerska 16:33:08 i'd only actually use it against real abusers, like asiekierka 16:33:13 suuure 16:33:32 * alise sets a ban on asiekierka (Egregious abuse of EgoBot; ^expiry=never) 16:33:39 asiekierka: just thought you might like to know 16:33:42 EgoBot? 16:33:46 everything since I said it wasn't protected 16:33:50 including by other people 16:33:54 is a complete crock of shit 16:33:56 alise, s/EgoBot/HackBot/ 16:33:59 Your gullibility knows no limits! 16:34:04 alise: HackEgo, not EgoBot 16:34:10 oerjan: hey since when do you have ops 16:34:14 and mine :D 16:34:18 scarf: that was the last piece of the gullibility puzzle duh 16:34:21 I beleive anything ehird says 16:34:23 lol 16:34:23 My notice to asiekierka wasn't a crock of shit 16:34:40 Sgeo_: what did you say 16:34:47 /notice asiekierka You are aware that porn.jpg isn't actually a necessary file, right? 16:34:48 (note: depending on the answer i may not not lynch you) 16:34:57 Yes, it is 16:34:58 ok, I won't not not lynch you 16:35:02 Don't lie, Sgeo_ 16:36:21 Sgeo_, he didn't read what was actually said above, he only have himself to blame for that 16:36:45 we can't ask asiekierka how much he actually believed now because of course he'll say none of it :) 16:36:51 I did 16:36:54 In fact, I did 16:36:59 Until Sgeo told m 16:37:00 e 16:37:02 mhm 16:37:03 But hey, this was fun! 16:37:07 Let's have such a party again! >D: 16:37:08 err, >:D 16:37:10 `help 16:37:11 Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ 16:37:13 porn.jpg wasn't the thing we were talking about 16:37:14 hentai was. 16:37:16 so thar 16:37:24 asiekierka, obviously you didn't read the help output 16:37:29 anyway, gawd, has asiekierka contributed a single worthwhile thing apart from DOBELA? 16:37:32 No 16:37:34 Never 16:37:34 even then it was a huge mess until Deewiant almost rewrote it 16:37:41 I also contributed lameness 16:37:42 idiocy 16:37:45 laziness 16:37:50 Have I contributed a single worthwhile thing? 16:37:53 Yes 16:37:55 alise, hey, I also helped with it. Like pointing out some flaws early on 16:37:58 `ls 16:37:59 bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ quotes \ sex.jpg \ share \ test.sh \ tmpdir.21507 16:38:05 `cat sex.jpg 16:38:05 This file is absolutely fake. 16:38:11 `rm sex.jpg 16:38:11 No output. 16:38:20 Sgeo_: Sure, you're not an idiot 16:38:20 alise, iirc it was me who first made it able to do anything close to computations :P 16:38:44 Hm, thanks 16:38:49 alise, but yes Deewiant did the main fixup of DOBELA 16:38:54 alise, PSOX! 16:38:59 * AnMaster runs 16:39:00 PSOX lol 16:39:14 pee socks 16:39:26 alise: FEAR ME 16:39:31 oerjan, on what grounds? 16:39:34 oerjan: no but since when :D 16:39:35 AnMaster: he's an op 16:39:38 AnMaster: You mean 16:39:43 Deewiant did over nine thousand fixups of DOBELA 16:39:48 all over a few chat sessions 16:39:48 oh, so he is 16:39:49 all lasting hours 16:40:02 lowercase chi is a pretty letter 16:40:13 asiekierka, I haven't contradicted that have I? 16:40:19 alise, paste it 16:40:22 I don't remember it 16:40:25 χ 16:40:27 χ(n) 16:40:29 ah that one 16:40:38 alise, looks like a "bendy" X here 16:40:41 :P 16:40:42 yes 16:40:44 and it's lower 16:40:59 alise, try to write lower case sigma on paper using a pencil 16:41:04 -!- nasa has joined. 16:41:07 why? 16:41:17 wait, maybe not that one 16:41:26 * AnMaster tries to remember which one was the hard one 16:41:28 nasa 16:41:45 it had lots of hooks in it's or such 16:41:50 Hey, can I try `reboot 16:42:08 alise, ah, lower case xi 16:42:18 alise, ξ that is 16:42:25 alise: i'm not sure exactly when, because i wasn't told when it happened :D 16:42:31 Can I? 16:42:33 asiekierka, have fun 16:42:34 oerjan: you weren't an op a year ago i think 16:42:37 ok 16:42:38 `run reboot 16:42:40 No output. 16:42:43 `run shutdown 16:42:44 No output. 16:42:46 Rage! :( 16:42:48 alise, indeed. in 1998 he wasn't I bet? 16:42:51 fish sandwich 16:42:58 ξ ZI 16:42:59 alise, since I don't think this channel was registered then 16:43:01 X = KAI 16:43:09 MissPiggy, ? 16:43:09 --- 16:43:09 c= 16:43:09 c= 16:43:10 , 16:43:11 Good morrow. 16:43:12 written bitch 16:43:21 χ(G) CHROMATIC NUMBER 16:43:27 alise, doesn't look close at all 16:43:33 Ooh, sparkly. 16:43:41 cpressey, what? 16:43:55 alise: i think it's not many weeks ago 16:43:57 MissPiggy, I'm not aware of what that is about? 16:44:05 LOOK UP CHROMATIC NUMBER 16:44:11 -ChanServ- 5 oerjan +votsriRfA [modified 1 week, 2 days, 19:04:07 ago] 16:44:25 MissPiggy, ah graph colouring 16:44:33 hi nasa by the way; apologies for the offtopicness 16:44:35 oerjan: so only years and years before i'm an op then :D 16:44:39 -!- nasa has quit (Quit: Leaving). 16:44:44 TOO LATE 16:45:00 bbl making food 16:45:12 making NUDE 16:45:58 alise: you'll have to develop some maturity first *duck* 16:46:01 thank you 16:46:11 i hear that happens around these ages 16:47:18 -!- MizardX has quit (Quit: reboot). 16:48:25 i'm kidding, i'm not mature either. 16:48:32 ban me 16:48:54 watch youtube 16:49:03 um that would mean finding out how this chanserv stuff actually _works_ 16:49:30 * Sgeo_ should not be reading Station V3 right now 16:49:32 oerjan: you don't need to mess with chanserv that much to ban someone 16:49:35 /cs op #esoteric 16:49:40 is enough to op yourself on the channel 16:49:44 ok 16:49:46 (or /msg chanserv if your client doesn't do /cs) 16:49:52 then you can just use the normal commands for kicking and banning 16:49:59 -!- ChanServ has set channel mode: +o oerjan. 16:50:00 and deop yourself when you're finished 16:50:05 Uh oh 16:50:11 no wait oerjan 16:50:12 -!- daef has quit (Ping timeout: 258 seconds). 16:50:13 /op alise 16:50:14 DO IT NOW 16:50:23 lol 16:50:27 -!- oerjan has set channel mode: +b *!*alise@95.145.65.*. 16:51:19 ah power 16:51:24 PUDDING 16:51:24 ... (more info) 16:52:35 -!- oerjan has set channel mode: -b *!*alise@95.145.65.*. 16:53:17 -!- alise has joined. 16:53:20 Sexier than envelopes 16:53:29 alise: heh, you weren't even on the server about 4 seconds before you joined 16:53:36 yeah i messed up my client a lil 16:53:51 scarf: can you explain the turkey bomb semantics you thought of that make it tc? 16:53:56 ooh wait 16:53:58 I can just ask cpressey! 16:54:00 alise: I'm not sure I can remember 16:54:05 not that he'll have any clue :) 16:54:15 -!- oerjan has set channel mode: -o oerjan. 16:54:17 but basically, the bomb gets passed after each person's done with their evaluating 16:54:35 and there are two commands that involve passing the bomb, you treat those as gotos (one forwards, one back) 16:54:57 then, all you need is for the three-trit operation to be something like shortcircuiting maximum 16:55:02 most of the types are actually completely useless, aren't they? 16:55:10 and to have a defined order of evaluation for everything else 16:55:14 and probably 16:55:24 although you need quite a few just for usable infinite memory 16:55:25 (shortcircuiting maximum? Does that even make sense?) 16:55:33 alise: yes, on numbers with a limited range 16:55:33 * Sgeo_ also needs to shave today :/ 16:55:43 oh, it wasn't shortcircuiting maximum of all three 16:55:44 scarf: also, NOMENCLATURE is basically like a hash table isn't it? except of turkey bomb stuff 16:55:48 instead, the operation takes two at random 16:55:58 alise: vaguely, except it's tied to variable names 16:56:02 right 16:56:03 sort of like a typeglob in Perl 16:56:07 it's useless isn't it 16:56:17 you expect me to figure that out from memory? 16:56:22 :D 16:56:30 i'm not exactly sure how to define PUDDING 16:56:48 either in terms of everything that's in it, or in terms of everything that isn't in it 16:56:52 you have two types of PUDDING, really 16:57:07 ... (more info) 16:57:11 But they are indistinguishable. 16:57:13 also, you have to allow for removing AMICEDs into a pudding, that actually adds to the amount of state they have 16:57:15 They are both unknowable, and have infinite size. 16:57:21 scarf: what XD 16:57:29 alise: AMICEDs have negative size 16:57:32 yes 16:57:35 well, no 16:57:37 the only time you can use them at all is inside PUDDINGs, I think 16:57:40 er, yes 16:57:51 are you thinking of the right pooding 16:57:55 a PUDDING that /doesn't/ contain a specified AMICED, therefore, contains information 16:58:06 PUDDING!!!!! 16:58:07 Attempts to deduce the existance of a HUMIDOR in the given PUDDING. The player to the left of the player holding the TURKEY BOMB has to keep drinking continuously while the computer/referee does their deducing. 16:58:07 GARNISH PUDDING 16:58:07 Convolutes the PUDDING with recent context drawn from the program. The player holding the TURKEY BOMB must pass it off. 16:58:07 IMAGINE PUDDING, PUDDING! 16:58:07 Returns a NOMENCLATURE indicating all the variables unchanged between two PUDDINGs. 16:58:08 alise: whichever type has the WHEREFORE AIN'T operator 16:58:08 -!- MizardX has joined. 16:58:09 are the only pudding operations 16:58:16 so yes, wrong type 16:58:17 scarf: oh ofc 16:58:19 am I thinking HUMIDOR? 16:58:41 no it is pudding 16:58:46 so the base pudding represents everything 16:58:48 ALL BUT removes something from it 16:58:55 WHEREFORE ART EXPR 16:58:55 Returns a PUDDING indicating the entire metaphysical nature of EXPR. 16:58:57 No fucking idea. 16:59:01 nor me 16:59:17 that operation is, at least, relatively easy to define 16:59:20 just hard to implement 16:59:20 ooh, I know 16:59:34 the entire metaphysical nature of an expression is the representation of that expression in the implementation 16:59:37 embedded into turkey bomb itself 17:00:07 remember to have the turkey bomb be a reference to itself; that's one of the easiest things to do in the entire impl, but possible to forget about 17:00:43 Uh, really? 17:00:54 Anyway, turkeyBomb = [turkeyBomb] suffices in Haskell, I think. 17:01:06 It's a distinct value from turkeyBomb, but you can get to turkeyBomb through it. 17:01:08 you need to also do it at the type level 17:01:16 Unfortunately, it doesn't type 17:01:19 scarf: mm 17:01:22 yep, that's the issue 17:01:30 you want a TurkeyBomb type which is a reference to a TurkeyBomb 17:01:37 in C++, at least, you can do it with casts 17:01:37 Here's what I basically did: 17:01:58 struct turkey_bomb { 17:01:58 struct turkey_bomb *turkey_bomb; 17:01:58 } turkey_bomb = {&turkey_bomb}; 17:02:07 A struct with one element is isomorphic to just that element, so... 17:02:28 yep, that's another possibility 17:02:39 the worst thing is that you need type tags 17:02:41 so everything has to be a struct 17:02:49 ugh 17:02:49 but that helps in this case 17:02:54 if we have struct { tag foo; the real value } 17:02:59 how are you going to deal with the types which are smaller than a pointer? 17:03:02 then our tagged turkey bomb isn't even relying on struct { x } isomorphing 17:03:08 scarf: padding, obviously 17:03:23 hmm, my start at a C++ impl had padding, but only where necessary 17:03:27 and the padding didn't contain values 17:03:40 hmm; PUDDINGs represent everything minus some things 17:03:51 so we should represent the turkey bomb universe as an infinite (uncountably so?) data structure 17:03:51 PUDDING 17:03:52 I mean, if a type's defined to contain two thirds of a bit plus half a trit, you can't have it as large as 4 bytes just to stick a pointer in there 17:03:59 then turkey bomb can be the index to turkey bomb in the universe 17:04:52 you also need to keep track of who owns the turkey bomb at any given moment, but that can be done separately 17:05:04 (and I'm not entirely sure what to do when it explodes) 17:06:27 a BI_IT is 1.14666... bits i think 17:06:39 so store it as a char and use the 2 least significant bits 17:07:22 what's more fun is trying to combine multiple BI_ITs back into values 17:08:12 a BI_IT has a range of ~2.6696797083400683 values, apparently 17:08:22 not entirely sure what that implies, but 17:09:55 06:42:26 and when I stepped out of the bus when I arrived, and looked back at the bus I was in 17:09:59 06:42:30 it said "not in traffic" 17:10:17 theory: it was an extra (rush hour) bus going only to your end station 17:10:47 happens occasionally in trondheim 17:11:04 [17:03] alise: hmm; PUDDINGs represent everything minus some things 17:11:05 [17:03] alise: so we should represent the turkey bomb universe as an infinite (uncountably so?) data structure 17:11:05 [17:03] alise: then turkey bomb can be the index to turkey bomb in the universe 17:11:09 scarf: does ^ sound promising to you? 17:11:41 -!- kar8nga has joined. 17:12:01 In the drinking game, whenever an INDECENT GRUBSTEAK is involved in an expression, everyone starts chanting "BANG BANG BANG!!!" until the player holding the TURKEY BOMB either finishes their drink and starts another, or falls down (in which case someone who hasn't been playing should take him or her home). 17:12:05 this is like forcing evaluation isn't it? 17:12:09 finishing drink = totally evaluating 17:12:15 falls down = fails somehow 17:12:21 BANG BANG BANG!!! is, I don't know, outpu 17:12:22 t 17:13:41 THIS IS NOT COPYRIGHT INFRIGNEMENT, IT WAS MADE BY PEOPLE 17:13:41 ... (more info) 17:14:47 with negative amiced ... I wonder if typeOf (NEGATIVE_AMICED ...) = AMICED or NEGATIVE_AMICED; it doesn't really matter except for size 17:14:59 and for size we want to consider the size if it were an AMICED; i.e. the negated size of the NEGATIVE_AMICED 17:15:09 ooooooooooo 17:15:29 GRUBSTEAK 17:15:29 A fraction whose numerator is a perfect square and whose denominator is a prime number. 17:15:30 No bigger than necessary. 17:15:30 IMPROPER GRUBSTEAK 17:15:30 A GRUBSTEAK whose denominator is less than the square root of the numerator. 17:15:30 Same as GRUBSTEAK. 17:15:54 scarf: the former seems to suggest we need a dynamic representation of grubsteaks. and are grubsteaks that satisfy the improper condition improper grubsteaks? so really improper is just a property of grubsteaks... 17:16:10 indecent grubsteaks are totally different though 17:16:12 yes, I think so to 17:16:50 *too 17:18:04 then I will have types GRUBSTEAK and IMPROPER_GRUBSTEAK, and have typeOf decide based on the contents of the GRUBSTEAK value 17:19:43 * alise wonders if WITH GUSTO is a different type 17:19:50 the size is different and all the operations must be different 17:19:52 so yes, I think 17:23:14 -!- Deewiant has quit (Ping timeout: 246 seconds). 17:24:47 * alise tries to think of how to represent 1 and 2/3rds of a bit 17:24:58 `ls 17:24:59 bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ quotes \ share \ test.sh \ tmpdir.22864 17:25:07 What happened to the porn? 17:25:08 :( 17:25:19 scarf: I demand you think of a representation! 17:25:59 alise: I just used a separate bit for the bit and the trit part, but I think that's cheating; it does give the right values if you ignore the fractional bits of padding, though 17:26:00 Sgeo_: polish censorship 17:26:05 You mean the tri-F 17:26:11 scarf: Those bits of padding are important! 17:26:14 (the fractional bits of padding show up as various /combinations/ of bi_its leading to weird results) 17:26:15 Take a wild guess what it means 17:26:32 Family Friendly F*cking? 17:26:37 Close 17:26:38 Family Friendly Filter 17:26:42 But both work just as well 17:27:23 -!- oerjan has quit (Quit: Fucking Friendly Families For Fun). 17:27:32 -!- Deewiant has joined. 17:29:22 newtype FiveOverThreeBits = FiveOverThreeBits Int 17:29:22 WFM 17:30:05 ?????????? 17:31:23 there's a slight issue in that i think the maximum value 5/3 bits can represent may be irrational 17:31:47 cube root of 32 anyway 17:33:47 * Sgeo_ is a Station V3 addict 17:35:25 scarf: who would have thought implementing turkey bomb correctly would require computable reals? 17:35:32 heh 17:36:06 ah 17:36:55 scarf: 0 ≤ x³ ≤ 32 where x is a BI_IT 17:37:18 sure it's not < 32? 17:37:20 erm 17:37:23 scarf: 0 ≤ (x+1)³ ≤ 32 where x is a BI_IT 17:37:34 now you have the /lower/ bound wrong 17:37:44 :D 17:37:50 well, it's 5/3 bits 17:37:55 2^(5/3) = 3√32 17:38:01 yep 17:38:08 2^2 = 4 17:38:18 2 bits can store 0 to 3 17:38:33 2 bits is more than enough, 1 is not enough 17:38:33 so 0 ≤ x ≤ 3 17:38:46 so what is it actually 17:38:52 if we want the regular zero to n inclusive 17:39:00 0 < (x+1)³ ≤ 32? 17:40:40 it doesn't actually say BI_ITs are unsigned, acutally 17:40:41 *actually 17:40:45 cpressey: are BI_ITs signed or unsigned? :P 17:44:10 scarf: heh, NEGATIVE_AMICEDs are (6*log(10))/(7*log(2)) bits big 17:44:30 that's bound to simplify 17:44:39 alise: Yes. 17:44:40 Om 17:45:21 scarf: not that expression, no: http://www.wolframalpha.com/input/?i=6%2F7+*+log%282%2C10%29&a=*FunClash.log-_*Log.Log10- 17:45:24 * Sgeo_ could easily stay here reading Station V3 all day instead of going to school 17:45:29 but 0 <= x < 2^((6*log(10))/(7*log(2))), yes, probably. 17:45:38 Sgeo_: So do so! :P 17:45:44 yeah 17:45:48 0 <= x < 10^(6/7) 17:46:47 ... wait, that's obvious. Uh, I think. 17:46:56 yes, it is obvious 17:47:04 yeah i'm not thinking all too clearly atm 17:47:06 :( 17:48:31 theory: it was an extra (rush hour) bus going only to your end station <-- except I don't live at an end station 17:48:32 -!- asiekierka has quit (Ping timeout: 240 seconds). 17:48:55 scarf: so the condition is 0 <= x^7 < 10^6 17:49:20 alise: you keep assuming there are an integral number of possibilities 17:49:21 * oerjan has quit (Quit: Fucking Friendly Families For Fun) <-- interesting quit message 17:49:30 I'm surprised that scarf didn't comment upon it 17:49:34 figari 17:49:46 AnMaster: I missed it, but I will continue to not comment on it 17:50:09 scarf: howso 17:50:53 cpressey, so what about that spec before? 17:51:03 I don't remember you commenting any further on that early draft 17:51:13 scarf, you just commented on it by replying to me there 17:51:16 :P 17:51:34 AnMaster: not directly 17:51:37 alise: context? 17:51:45 "alise: you keep assuming there are an integral number of possibilities" 17:51:56 scarf, indirectly also counts 17:52:01 alise: because you're working out the largest integer that fits in x 17:52:43 right you are. i should have slept more last night :| 17:52:51 especially when doing turkey bomb 17:53:09 I think n > 0 && n^3 < 32 is still sound though 17:53:18 argh, fucking haskell 17:53:22 AnMaster: Sorry, I probably won't be able to get around to it soon... too much real work. 17:53:23 I can't do exponentials with a Rational 17:53:25 because it's not a Floating 17:53:31 cpressey, okay 17:54:05 cpressey, I expect there will be updates to it, so better check in irc logs for last version when you *do* decide to read it. 17:55:18 scarf: it seems to work 17:55:22 so i'm not sure I follow 17:55:31 meh, never mind 17:55:38 noo don't say that 17:57:36 argh, fucking haskell <-- I never, ever, thought I would hear you say that 17:57:51 alise, anyway, it does sound like a strange restriction 17:58:48 data SixSeventhsOfADecimalDigit = SixSeventhsOfADecimalDigit Rational deriving (Show) 17:58:49 negativeAmicedGuts :: Rational -> Maybe SixSeventhsOfADecimalDigit 17:58:49 negativeAmicedGuts n 17:58:49 | n >= 0 && n^7 < 10^6 = Just (SixSeventhsOfADecimalDigit n) 17:58:49 | otherwise = Nothing 17:58:54 what are you doing??????? 17:59:07 for integer exponents it is trivial to implement. Somewhat more involved for non-integers. 17:59:17 MissPiggy: implementing TURKEY BOMB 17:59:18 MissPiggy: failing to implement TURKEY BOMB 17:59:19 http://catseye.tc/projects/turkeyb/doc/turkeyb.html 17:59:22 scarf: oi 17:59:27 scarf: i'm not failing! 17:59:34 you will be eventually 17:59:51 alise, what about ZILCH? 18:00:00 data Value = ZILCH | ... 18:00:12 just like data () = (), it carries 0 bits of information and can be omitted everywhere 18:00:22 more fun going on over at SCO, btw; Darl McBride, the former CEO, is now trying to buy some of its stuff off it 18:00:37 -!- lament has quit (Ping timeout: 268 seconds). 18:00:53 huh 18:01:04 scarf, any patents? 18:01:07 I guess 18:01:11 -!- lament has joined. 18:01:15 AnMaster: no patents 18:01:25 the bizarre list I wrote in-channel earlier was a list of some of it, though 18:01:42 * AnMaster looks for that list 18:01:47 where? 18:01:51 05:14:57 snowplow, grassroots, mobile OE, MPSEB Indian utility co. meter reading, Delhi traffic police, Citibank demo documentation, Disprax (fake screen shots only), Jackson Builders, Aston Villa, NREGA employment census, smnp hardware monitoring, NDPL power, PG Call Home 18:01:56 They own Delhi traffic police? 18:01:56 I think it's a list of companies that they gave demos to, or something 18:01:57 ah 18:02:05 And Aston Villa! 18:02:12 alise: ownership seems unlikely, it's more likely to be some sort of joint projec 18:02:14 *project 18:02:26 "TRIVIA CONCERNING type 18:02:26 Three references: one to an object of the named type, two to TRIVIA objects." 18:02:30 Two to trivia objects of... any type? 18:02:31 Okay. 18:02:32 although, it wouldn't surprise me if Darl thought SCO did learn all that list 18:02:41 *did own 18:02:55 the funny thing is, he's offering $35,000, and some people are trying to outbid him 18:03:01 ... 18:03:08 grassroots? 18:03:11 as in, the lawns? 18:03:13 my theory is that he's trying to drain $35,000 from the open-source community by getting them to buy a worthless list of random 18:03:13 | TRIVIA_CONCERNING Value Value Value 18:03:13 I'd put type information in the Haskell types but I bet TURKEY BOMB can subvert even that heroic effort. 18:03:17 alise: again, who knows 18:03:20 scarf, ? 18:03:28 * AnMaster: 18:03:29 worth a try 18:03:35 no, wait, can't 18:03:36 nm 18:03:37 scarf, ? 18:03:46 ah 18:03:50 "Exactly fifteen bytes, no exceptions." 18:03:53 it was a correction 18:03:53 AnMaster: well, if Darl wants to buy it so badly, it must be valuable, right? 18:03:53 Well that's not going to be workable. 18:04:03 scarf, why not? 18:04:06 alise: I used some padding to manage that in C++ 18:04:17 just wait until you reach the quarter-of-a-reference type 18:04:24 scarf, what? you implemented turky bomb in C? 18:04:26 err C++ 18:04:27 No, I mean, Haskell doesn't really have the concept of sizes of its values, so... 18:04:29 that was trivial on my machine with 32-bit pointers, but other bits were harder 18:04:30 AnMaster: he tried 18:04:33 alise: no, I just started 18:04:37 ah 18:04:40 I had most of the declarations there, but no code 18:04:42 *AnMaster: 18:04:45 stupid tab-complete 18:04:50 I'd rewrite in C, but I want rationals 18:05:18 alise, note that pudding and "HUMIDOR BUILT UP FROM type, type & type " both have infinite size 18:05:30 AnMaster: you can do them lazily 18:05:39 oh good point 18:06:09 also not 1/4 of a reference 18:06:10 it is: 18:06:14 "A quarter of the platform-defined pointer size." 18:06:42 alise, and how did you implement AMICED? 18:06:45 PUDDING is just a reference to everything in a humidor; or, a reference to the entire universe sans one value (so you can just store that value); 18:06:57 or, a reference to the entire metaphysical nature of an expression 18:07:07 AnMaster: make the value be a NEGATIVE_AMICED 18:07:10 like scarf did 18:07:11 AnMaster: AMICED is relatively easy; the weird bitwidth is harder than the actual negativeness 18:07:22 scarf, oh? 18:07:24 hm 18:07:40 it hardly matters anyway, as I don't know of any actual way to create a value of type AMICED 18:07:57 according to the rules, you can just specify a variable and its value to declare one 18:08:09 but what's the syntax for an AMICED literal? 18:08:26 clearly the actual bits and trits are embedded in the source 18:08:31 since we only have bits trits are represented as bits 18:08:39 so the following 5/3 bits of the source code are the value 18:08:42 obviously 18:08:52 why would you need syntax? you have the inherent syntax of character arrays right in front of you 18:09:02 now clearly amiced is negative 18:09:08 so the /preceeding/ 5/3 bits are the value 18:09:11 hey, you know how, say, bz2 treats the data as a stream of bits, rather than octets? 18:09:14 so if it was 18:09:16 x = y 18:09:18 it'd be 18:09:31 could you treat the program as a purenumber, and take fractional bits from that? 18:09:32 x =y= 18:09:33 or something 18:09:49 where the latter is 2/3rds 18:09:50 of a = 18:09:53 and the former is 1/3rd 18:09:54 I think 18:09:57 no esiy 18:09:58 no wait 18:09:59 that's bytes 18:10:01 you get the idea 18:10:11 scarf: eh? 18:10:27 alise: say, you have a huge purenumber 18:10:33 scarf, " AnMaster: AMICED is relatively easy; the weird bitwidth is harder than the actual negativeness" 18:10:34 ANHAHA 18:10:35 but actually 18:10:36 you can extract one bit from it by dividing by 2 and taking the remainder 18:10:40 " Negative six sevenths of a decimal digit. " 18:10:46 and one trit by dividing by 3 and taking the remainder 18:10:46 what the heck is a decimal digit here 18:10:50 how wide is it 18:10:57 AnMaster: ln(10)/ln(2) bits 18:11:00 scarf, is it stored as BCD perhaps 18:11:02 just like normal decimal digits 18:11:02 that is my guess 18:11:07 and no, it's stored as decimal 18:11:08 scarf: oh very good idea 18:11:15 let's do it 18:11:18 alise: this may even extend to fractional bits 18:11:20 scarf: collaborate? or am i just too crazy for you 18:11:23 but I'm not sure 18:11:39 alise: I would, but I need to get some RL work done by three days ago, only nobody's noticed I haven't done it yet 18:11:52 get going then! 18:11:53 divide by 5/3*2 and take the remainder obvs 18:12:11 yep, ofc 18:12:28 and an AMICED literal would presumably /add/ info to the source 18:12:38 whatever info gets added, that's the value that the AMICED doesn't contain 18:12:41 it's all falling into place 18:12:46 hmm no 18:12:57 i think "The following -n bits" = "The preceding n bits" 18:13:01 alise: I don't 18:13:02 but maybe you're right 18:13:13 so you specify every 5/3 bit value apart from the one it contains? 18:13:17 rer 18:13:18 er 18:13:20 doesn't contain 18:13:21 so to speak 18:13:49 think about it this way: a literal bit has 2 possible values, 0 and 1; code containing a literal bit, you have 2 possibilities for the code giving 2 values for the bit, and 1 possibility for the rest of the code, assuming all you change is that bit 18:14:09 `addquote and an AMICED literal would presumably /add/ info to the source whatever info gets added, that's the value that the AMICED doesn't contain it's all falling into place 18:14:10 135| and an AMICED literal would presumably /add/ info to the source whatever info gets added, that's the value that the AMICED doesn't contain it's all falling into place 18:14:13 now, a literal negative bit has half a possible value; code containing a literal for that, you have 1 possibility for the code but 2 possibilities for the rest of the code 18:14:20 scarf: so, wait 18:14:36 bi_its can't just be integers 18:14:40 because the fractional portion gets wasted 18:14:43 so are they rationals? reals? 18:14:46 it's not specified 18:14:49 I give up understanding this 18:14:52 ieee floats? 18:14:54 better to avoid going insane 18:15:01 I guess a real 18:15:05 alise: they're something with... a fractional number of possibilities 18:15:05 since we're dividing the program 18:15:09 no, wait, rationals 18:15:18 scarf: yes, but we're dividing by a fractional number and taking the remainder 18:15:28 hmm wait 18:15:35 alise, fmod()? 18:15:35 a negative amiced isn't a rational number of bits 18:15:40 so it /has/ to be reals 18:15:40 :-D 18:15:51 so we need a computable real system to do all this 18:16:10 which means we're losing some nice things... for instance equality won't terminate if the two reals aren't equal 18:16:17 alise, what is the bit width of a decmial digit? 18:16:24 meh, TURKEY BOMB doesn't have equality, maybe that's why 18:16:31 AnMaster: log(10)/log(2) 18:16:42 hm okay 18:16:45 AnMaster: you can even implement this, using 10-valued logic 18:16:47 just it would be a real pain 18:16:52 scarf: but turkey bomb doesn't specify ascii or whatever 18:16:53 and you have to do it in hardware not software 18:16:56 so how do we construct the program number? 18:17:13 scarf, you could emulate it in software? By writing a 10-valued-logic-emulator? 18:17:13 oooh! 18:17:18 alise: presumably, as an expression, Mathematica-style 18:17:26 obviously the character set has exactly the number of characters that are used in the monospace portions of the spec 18:17:40 scarf: no, i mean, we don't actually have a defined way to make the text into a number 18:17:44 anyway, I see something neat about, one program containing a negative-bit literal contains 1/2 a possibility for that literal * 2 for the rest of the program 18:17:47 scarf, after all you can emulate ternary systems... 18:17:56 alise: syntax is the least of my worries here :) 18:17:59 obviously the character set has exactly the number of characters that are used in the monospace portions of the spec, and they are ordered by order of occurence (not from CLIN_TON; that's part of the older-human-written stuff) 18:18:05 no? :P 18:18:11 AnMaster: yep, that involves wasting a bit of memory, though, and TURKEY BOMB dislikes padding 18:18:19 alise: maybe 18:18:32 scarf, well write it in VHDL then! 18:18:37 or something 18:18:42 what is TURKEY BOBM 18:18:42 scarf: oh, wait, the article is in ASCII, and it says it originates from the late 90s 18:18:49 and ASCII would have been used then 18:19:02 so clearly, as they wouldn't DARE reinterpreting the monospace things from the spec for... some reason, it's ASCII 18:19:19 MissPiggy: take a turkey (preferably, a real, live turkey), or a time bomb (preferably, a real, live time bomb); preferably both, /securely/ strapped together 18:19:29 oh great, we're going to have control characters in literals 18:19:50 MissPiggy: ...and DRINK! 18:20:54 You know, when you consider both the premise of TURKEY BOMB, and the fact that FBBI stands for "Flaming Bovine Befunge Interpreter"... I'll bet the SPCA hates me. 18:21:08 cpressey: now ANSWER OUR INQUIRIES!!!! 18:21:13 :P 18:21:31 hmm, OTOH, the TURKEY BOMB spec does seem to imply particular representations for operators 18:21:32 Heh. Where do you people get the idea that ambiguities in a spec can be resolved by asking the person who wrote it, anyway? 18:21:44 Or the idea that I wrote the TURKEY BOMB spec? 18:21:50 cpressey: SHUT UP 18:21:51 oh you didn't? 18:21:56 I FOUND IT 18:21:59 so, is the valuestream separate from the operators themselves? 18:22:04 "Discovered mysteriously one day amidst a pile of Byte magazines in a second-hand book store by Chris Pressey" 18:22:06 yep, I believe you 18:22:07 At the bottom of a birdcage 18:22:17 The Byte magazines were in the birdcage? 18:22:19 anyway, I wasn't under the impression that cpressey had any idea how TURKEY BOMB worked 18:22:20 Or just the spec? 18:22:26 Was there anything else in the birdcage if the latter? 18:22:39 alise: The whole bookstore was in the birdcage. 18:22:45 Ah. 18:22:48 It was a very large birdcage. 18:23:01 Or a very small bookstore. 18:23:29 You know, when you consider both the premise of TURKEY BOMB, and the fact that FBBI stands for "Flaming Bovine Befunge Interpreter"... I'll bet the SPCA hates me. <-- SPCA? 18:23:29 \ ADVISORY ADVISORY ADVISORY ADVISORY 18:23:29 Returns the type thus pointed to. Also, the player holding the TURKEY BOMB must pass it off. 18:23:35 scarf: so types are values 18:23:38 but what are their types? 18:23:52 well, the type of a TURKEY BOMB is obvious enough 18:24:09 yes, TURKEY BOMB::Type 18:24:14 anyway, I always assumed that \ returned a value, and "type" was a typo for "value" there 18:24:17 but if \, an _expression_ 18:24:22 can return a type as a value 18:24:24 and every value has a type 18:24:26 then types must have a type 18:24:28 good catch 18:24:33 alise, or perhaps the bird cage was larger on the inside? 18:24:34 but there ain't no type specified for types 18:24:37 maybe types themselves are untyped 18:24:38 so it was both 18:24:42 scarf: the most turkey bomb way to resolve this is obviously that not all values have typers 18:24:44 *types 18:24:48 nothing really implies that TURKEY BOMB is strictly typed 18:25:05 AnMaster: No, that's a police box. 18:25:06 well, the spec implies it more or less everywhere but doesn't actually /say/ it, so we should ignore the implication 18:25:15 alise, yeah, it was disguised! 18:25:19 anyway, this means you can have references to types 18:25:22 it was a bird cage all along! 18:25:30 given that an ADVISORY is a quarter of a reference 18:25:31 $ BI_IT BI_IT BI_IT BI_IT BI_IT BI_IT $ 18:25:32 Attempt to make a GRUBSTEAK. 18:25:32 TRIVIA Y EXPR Y TRIVIA 18:25:32 Attempt to make a TRIVIA. 18:25:33 TRIVIA BI_IT // 18:25:33 Attempt to connect a TRIVIA to itself and return it. The BI_IT argument is required, but serves no detectably useful purpose (hardcore followers of the drinking game tradition insist that it's for good luck.) 18:25:33 Note how the first two don't actually say they RETURN anything... 18:25:46 scarf: Well, no, you can have a quarter of a reference to a type. 18:25:53 There's just one operation that takes four and dereferences their inaccessible combination. 18:26:18 If there is a type with no value, then you cannot construct an ADVISORY PERTAINING TO type. 18:26:24 ADVISORY PERTAINING TO type 18:26:24 A quarter of a reference to a object of the given type. 18:26:38 You can't get to the quarter-referenced value, just its type. 18:26:46 But you need a value to construct one in the first place. 18:26:52 So you have quarter-references to types that have values. 18:27:05 I still think it's a typo, the spec makes no sense otherwise 18:27:09 well, even less sense than it normally would 18:27:15 GARNISH PUDDING 18:27:15 Convolutes the PUDDING with recent context drawn from the program. The player holding the TURKEY BOMB must pass it off. 18:27:17 maybe cpressey copied it incorrectly from the magazine? 18:27:21 no magazine 18:27:25 the spec was discovered amongst magazines 18:27:27 oh 18:27:30 Since a pudding is basically a universe, 18:27:32 well, copied it incorrectly anyway 18:27:34 convoluting it with recent context 18:27:36 = 18:27:42 did cpressey find the spec typed on paper, or in electronic form? 18:27:42 updating the values it has to be their current values 18:27:47 but recent, that doesn't mean most-recent, surely? 18:27:47 it would help to know if it implies ASCII or not 18:27:56 perhaps it's the turn before this one's state 18:28:01 cpressey: ^ 18:28:09 this question is about your transcription :| 18:28:10 scarf, EBCDIC? 18:28:17 scarf, or baudot? 18:28:27 * Sgeo_ is about to post something stupid to Facebook 18:28:34 Sgeo_: So don't. 18:28:36 Sgeo_, well, don't do that then 18:28:44 NOMENCLATURE % GRUBSTEAK GRUBSTEAK 18:28:44 Perform iterative cypher transformation of set of names. 18:28:49 Clearly the grubsteaks define the cypher. 18:28:54 GRUBSTEAK 18:28:55 A fraction whose numerator is a perfect square and whose denominator is a prime number. 18:28:56 Fractran, anyone? 18:29:01 alise, doesn't the nomenclature? 18:29:10 NOMENCLATURE 18:29:11 A set of variable names, defined by an EBNF expression that must contain at least one { } (repeated 0 or more times) term. 18:29:11 No. 18:29:14 AnMaster: you are thinking in completely the wrong terms here 18:29:20 NOMENCLATURE is a bunch of variable names with some sort of EBNF something. 18:29:29 alise, pretty sure nomenclature is a crypto term, isn't it? 18:29:30 "Defined"? Howso, I wonder? Maybe that is the syntax. 18:29:41 something related to transposing cryptos 18:29:50 So {a} would be the variable names "","a","aa",... 18:30:09 or something 18:30:21 some problems are referred to as mental exercise 18:30:34 turkey bomb is mental tv-watching 18:30:43 it ruins your mind!!! 18:30:48 ag irn 18:30:50 fub bip 18:30:55 PUDDING!!!!! 18:30:55 "So far, in every college class I've taken, there's always been at least one atheist." 18:31:08 Sgeo_: yeah that's a pretty significantly retarded thing to say 18:31:38 alise http://www.youtube.com/watch?v=2PyXLNL-eHI 18:31:44 Sgeo_: are you yourself an atheist? or does someone else you know to be an atheist take every class you take? or something else? 18:31:52 he's an atheist but he's pretty stupid about it in practice 18:31:56 alise, it was handwritten. Do you believe that? 18:32:04 * Sgeo_ removes it 18:32:07 (note: I am counteracting the holier than thou/insulting balance) 18:32:11 who's an atheist??? 18:32:17 AMOUGST US??? 18:32:18 cpressey: Yes. (No) 18:32:25 Now what's this about a pigeonhole principle for atheists in college classes? 18:32:41 cpressey, with a quill pen? 18:32:51 Bye all 18:32:57 And now, it's time for WHO'S AN ATHEIST, the game show where we hunt down and kill anyone who doesn't worship the father, the son and the holy spirit! *theme music plays* 18:32:59 AnMaster: If only to keep the bird-related theme up, yes. 18:33:11 cpressey, ooh I didn't think that far 18:33:11 Gregor: Don't forget... Robert! 18:33:17 atheists are more likely to go to college, because they need surrogates like higher education to fill their life with a semblance of meaning. 18:33:22 Groogger :D 18:33:28 cpressey: What natural language was it written in, exactly? :P 18:33:51 lament: Oh you scoundrel. 18:33:52 alise: In truth I cannot be certain... 18:34:03 cpressey, how comes? 18:34:09 AnMaster: he was playing TURKEY BOMB at the time 18:34:11 with LSD 18:34:17 oh 18:34:18 (he hadn't seen the warning yet, as he hadn't found the spec yet) 18:34:41 alise, I thought we were in for some LP Lovecraft thingy to explain it 18:34:42 :/ 18:35:04 The spec /is/ /Cthulhu/. 18:35:11 Oh how I wish it was merely LSD! In fact, it was extract of shoggoth. 18:35:16 NASTY stuff. 18:36:25 So did your finding of the TURKEY BOMB spec cause a lasuac violation that caused you to find it in the first place? 18:37:05 you mean LSD is not extract of shoggoth? 18:37:40 lament, no it is lysergic acid diethylamide 18:37:51 i really want to kill you AnMaster 18:38:03 It's Lucy in the Sky with Diamonds. 18:38:04 alise, why? 18:38:09 Gregor, haha 18:38:10 it's complicated 18:38:43 alise, if it changes things I had to google it, didn't remember what the name was exactly 18:39:40 no i guessed you googled it. 18:40:47 if it helps I remembered it was acid diethylamide 18:41:40 Gregor, actually Beatles got that wrong. It's Lisa not Lucy. She lied about her name 18:42:18 "lucy in the sky with diamonds" sounds like a weird variation of Cluedo 18:42:25 Lucy O'Donnell Vodden (1963 - 22 September 2009) was the inspiration for the song. 18:42:28 scarf: :D 18:42:36 scarf, heh 18:42:51 OK 18:42:59 Gregor: KO 18:43:05 We officially must make a version of Clue in which "Lucy in the Sky with Diamonds" is a valid guess. 18:43:15 * pikhq could've sworn atheism was... Common... 18:43:18 bbiab 18:43:32 Gregor: ah, I forgot that you Americans had a different name for it 18:43:33 pikhq: WHAT WOULD YOU KNOW JEBUS-HUGGER 18:43:52 alise: Many things. 18:43:59 scarf: Probably just a consequence of trademark vagaries. 18:44:04 too bad your system is inconsistent 18:44:08 YOU KNOW EVERYTHING AND NOTHING 18:44:11 This was shortly before John Carpenter and I travelled to FSU to steal the Kappa Upsilon Chi's mascot at the time, which was, as fate would have it, a turkey. 18:44:17 alise: How very Xen of you. 18:44:33 cpressey: You forgot "...on acid". 18:44:36 ... That was an odd misspelling. 18:44:43 alise: I am an expert on these matters. 18:45:08 cpressey: Or are you? 18:45:22 pikhq, Z and X are next to each other 18:45:26 Alas alise, not as much as fungot. 18:45:26 cpressey: athame: the ki-rin is a member of the great tail sweeping from side to side, like a child, opened them and brought them many gifts of food and clothing for their relentless persecution of their victims. 18:45:27 on qwerty at least 18:45:37 [[Kappa Upsilon Chi ("Keeping Under Christ", Kappa Chi, or ΚΥΧ)]] 18:45:37 that's a really irritating abuse of the greek alphabet 18:45:54 ugh 18:45:59 I like that last fungot quote 18:45:59 alise, eta beta pi 18:46:00 scarf: always sweep the floor. only the beginning of lactation in ewes and was a single, savage thrust of her sisters to have been born on the take. 18:46:07 alise, and that's from Discworld 18:46:08 Excellent Buttock Pissing 18:46:14 alise, no no 18:46:22 "eat a better pie" 18:46:24 why aren't there any fraternities with three of the same letter? 18:46:25 eta beta pi 18:46:28 see? 18:46:29 Xi Xi Xi 18:46:37 alise, because that sounds silly 18:46:41 EXACTLY 18:46:54 Welcome to Kappa Kappa Kappa! 18:47:13 scarf, I think I saw someone riding a tame ki-rin on NAO once 18:47:23 I have no idea how that happened 18:47:30 Digamma Digamma Digamma! 18:47:59 AnMaster: blessed figurine of a ki-rin 18:48:02 I've done it myself 18:48:12 scarf, ah of course... 18:48:13 DIGAMMA DIGAMMA DIGAMMA DIGAMMA DIGAMMA DIGAMMA DIGAMMA upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon 18:48:14 get it hur hur? 18:48:24 s/upsilon/UPSILON/g 18:48:31 alise, developers developers? 18:48:44 but what is the UPSILON? 18:49:04 Beta Beta Beta Beta (Badger Badger ...) 18:49:05 In the geek alphabet: ϜϜϜϜϜϜϜΥΥΥΥΥΥΥΥΥΥΥΥ 18:49:19 Lowercased: ϝϝϝϝϝϝϝυυυυυυυυυυυυ 18:49:24 har 18:49:28 (Well, the obsolete greek alphabet.) 18:50:55 alise, old greek you mean? 18:51:03 No, that's your mom. 18:51:08 that's still used in math 18:51:24 alise, that's what your dad said! 18:51:31 (now go figure that one out!) 18:51:42 (also he said it to your mom) 18:52:03 I'm my mother's dad's son's brother's father's granddaughter's cousin. 18:52:28 I'm my cousin. 18:52:43 (= I'm my self.) 18:52:59 har 18:53:09 pikhq isn't lying though :) 18:53:28 alise, impossible? 18:53:40 No. 18:53:42 Not with inbreeding. 18:53:43 how 18:53:51 maybe 18:53:55 pikhq comes from a real good Southern family. 18:54:01 not sure how you would need to inbreed for that 18:54:11 pikhq: Explain to the peon! 18:55:03 peon? 18:55:30 alise, that is what your mom said (referring to herself) 18:55:39 I'm my mother. 18:55:45 `quote unborn 18:55:46 56| im my dads unborn sister 18:55:47 * cpressey drowns in feathers. 18:55:53 AnMaster: Cousins married a few generations back. Twice. 18:55:57 cpressey, why? 18:56:01 Making me my own 7th and 9th cousin. 18:56:10 pikhq, oh not first cousin at least 18:56:19 because that shouldn't be possible 18:56:20 pikhq: That's not something you're supposed to admit on the tuberwebs :P 18:56:39 cpressey: noo, don't mention Feather 18:56:43 I have real work to do atm! 18:56:48 scarf, oooh feather! 18:56:49 That being said, we're all cousins ... even if you have sex with a sheep, you're having sex with your cousin. 18:56:50 My family tree is... Hard. 18:57:05 scarf: add the feather operations to turkey bomb 18:57:06 scarf, a pity can't show intonation 18:57:09 I have 2 parents, 4 grandparents, 8 great-grandparents, and so forth. Therefore I have an infinite number of ancestors. 18:57:11 the way I thought it... 18:57:22 Gregor: We're all part of the same big family :D 18:57:30 Freaking Hatfields. 18:57:46 cpressey: You know, the Bible tells us of all the inbreeding that went on in Genesis. 18:58:02 cpressey, ooh, do that as proof by induction 18:58:06 alise: If it wasn't for all that Genesis inbreeding, we'd all be living for five hundred years. 18:58:08 alise: Actually, it's pretty mum on most of the inbreeding that had to happen. 18:58:09 AnMaster: He did. 18:58:12 alise: That inbreeding broke our genes. 18:58:16 alise: Indeed. That's how those cats all lives to be 800 years old. 18:58:17 Gregor: 900 was the top no? 18:58:18 900 or so 18:58:18 alise, not a formal such proof 18:58:20 s/s/d/ 18:58:22 Well, had to happen according to given accounts. 18:58:38 alise: Yuh. 18:58:54 I'm not entirely sure how biblical literalists... Rationalise that. 18:59:08 Oh, wait. 18:59:12 They don't. 18:59:19 cpressey, what cats? 18:59:29 I'm not entirely sure how biblical interpretists-and-ignoring-a-large-portion-of-it-anyway... justify believing in /any/ of it. 18:59:31 Oh, wait. 18:59:32 They don't. 18:59:34 hmm, are there any biblical literalists that take the lolcat version as the version that literally happened? 18:59:38 Well, some of the weirder ones do (rationalize it.) 18:59:58 I'm pretty sure talking about the /relative rationality/ of Christians is ridiculous,. 18:59:58 -!- Slereah has joined. 19:00:01 *ridiculous. 19:00:16 scarf, what, there is a lolcat version of the bible?? 19:00:26 http://www.lolcatbible.com/ 19:00:27 Warning: Awful 19:00:41 AnMaster: apparently yes 19:00:57 http://www.lolcatbible.com/index.php?title=Revelation_1 19:01:09 Interestingly, this makes exactly the same amount of sense as the actual Revelation. 19:01:18 alise, yeargh 19:01:19 indeed 19:01:25 -!- mrbug has joined. 19:01:32 alise: Somehow, that doesn't surprise me. 19:02:10 http://www.lolcatbible.com/index.php?title=Revelation_22 19:02:11 hahaha 19:02:32 "He which testifieth these things saith, Surely I come quickly. Amen. Even so, come, Lord Jesus." 19:02:33 --> 19:02:34 "BRB" 19:03:38 scarf: wait, from what do you derive that turkey bomb actually has variables? 19:03:45 NOMENCLATUREs are related to them 19:03:52 but I see nothing about actually using variables in expressions or anything 19:04:12 alise: there's a comment somewhere else that anyone can create a variable by saying its name and value 19:04:18 at any time, including while someone else is calculating 19:04:21 "Variables are also declared by any player spontaneously standing up and shouting out a name that hasn't been mentioned yet, and a type to go with it, at any time." 19:04:26 scarf: but that doesn't mean you can actually use them in expressions 19:04:27 oh, name and type 19:04:31 only that they exist, in some vague sense 19:04:34 alise: no, I wasn't assuming that 19:04:39 :D 19:04:43 for all I know, they exist just to mess with NOMENCLATUREs 19:05:06 then, wait 19:05:11 it doesn't say there are literals, either 19:05:17 so every expression /must be infinitely nested/ 19:05:36 it also says the spec is possibly incomplete 19:05:38 doesn't it 19:05:48 so you shouldn't assume that it is complete 19:05:48 I think there probably are literals, or how could you play it as a drinking game? 19:05:50 AnMaster: that's why we're making such ridiculous assumptions 19:06:02 alise, ? 19:06:07 scarf: holding literal BI_ITs and PUDDINGS etc up 19:06:13 AnMaster: because it's incomplete 19:06:19 ah 19:06:38 BI_IT BI_IT BI_IT ! BI_IT BI_IT BI_IT 19:06:42 I assume those are values 19:06:46 Yes. 19:06:47 to be inserted there 19:06:52 then there must be literals 19:06:52 scarf: but yes there probably are literals 19:07:09 unless that is actually the literal phrase "BI_IT BI_IT BI_IT ! BI_IT BI_IT BI_IT" 19:07:16 AnMaster: or just nested expressions 19:07:25 scarf: so obviously a @HUMIDOR type of pudding "contains" all the values within it 19:07:46 a regular pudding-but-with-exclusion contains all values in the entire turkey bomb universe (possible values or only used values?) except for one 19:08:09 a metaphysical-pudding contains the interpreter's representation of EXPR, represented somehow as multiple values inside the pudding 19:08:58 alise, except which one? 19:09:20 ALL BUT EXPR 19:09:20 Returns a PUDDING indicating everything but EXPR. 19:09:22 That one. 19:09:30 ALL BUT EXPR 19:09:30 Returns a PUDDING indicating everything but EXPR. 19:09:31 WHEREFORE ART EXPR 19:09:31 ah 19:09:31 Returns a PUDDING indicating the entire metaphysical nature of EXPR. 19:09:31 WHEREFORE AIN'T EXPR 19:09:32 Short for WHEREFORE ART ALL BUT EXPR. 19:09:32 WHEREFOREN'T EXPR 19:09:32 Short for ALL BUT WHEREFORE ART EXPR. 19:09:48 WHEREFORE AIN'T EXPR = A PUDDING indicating the metaphysical nature of (a PUDDING indicating everything but EXPR). 19:10:07 WHEREFOREN'T EXPR = A PUDDING indicating everything but (a PUDDING indicating the metaphysical nature of EXPR). 19:10:15 hm 19:10:17 those other ones 19:10:21 are somewhat trcky 19:10:35 HUMIDOR.type 19:10:35 Retrieves an element from a HUMIDOR. 19:10:45 scarf: is type a placeholder in the syntax or literally "type" do you think? 19:10:53 no idea 19:10:53 they don't seem to use type, so i guess it's literal 19:11:10 HUMIDOR BUILT UP FROM type, type & type 19:11:10 A structure containing three other types, specified at compile-time, all of which must be different, one of which must be another HUMIDOR. 19:11:10 Infinite. 19:11:11 HYBRID OBTAINED BY COMBINING type & type [WITH GUSTO] 19:11:11 A unified structure containing data from two different types, specified at compile time. 19:11:13 HYBRID.type 19:11:13 Casts a HYBRID to either type it was defined with. 19:11:14 HUMIDOR.type 19:11:14 Retrieves an element from a HUMIDOR. 19:11:15 it does use type indeed 19:11:23 -!- tombom has quit (Ping timeout: 246 seconds). 19:11:32 wait, HUMIDOR /types/ are infinite 19:11:44 HUMIDOR BUILT UP FROM ZILCH, ZILCH & HUMIDOR BUILT UPF ROM ZILCH, ZILCH & ... 19:11:48 yes 19:12:11 wasn't there a discussion about implementing it sometime during 2007? 19:13:02 well, I wish you best of luck 19:13:16 i really do believe I need scarf to do it though :P 19:13:25 alise, why? 19:13:35 because it needs 10-valued logic? 19:13:38 and he knows VHDL? 19:13:45 no, because he has thought about it a lot and has lots of answers 19:13:52 plus a potentially TC model of execution (it doesn't actually have one) 19:13:56 (you have to derive it from the drinking game) 19:13:58 why on earth has he spent time on it 19:14:04 he was trying to implement it 19:14:08 why 19:14:09 :/ 19:14:15 look at the channel name 19:14:17 look at our wiki 19:14:18 then GTFO 19:14:26 lol 19:14:33 alise, yeah but I think it is impossible 19:14:36 turkey bomb, like everest, was there. 19:14:38 AnMaster: no, it isn't 19:14:45 almost certainly not 19:14:51 very well then 19:15:12 alise, implement it in intercal then 19:15:21 why? 19:15:30 alise, it will be next to impossible 19:15:36 even if not actually impossible 19:15:44 malbolge if that isn't hard enough 19:16:20 no 19:16:24 you are greatly overestimating its difficulty 19:17:24 I DONt know what TURKEY BONB is 19:18:16 MissPiggy, ffs... see link above 19:18:24 ? 19:18:35 MissPiggy, /lastlog http:// 19:18:44 look for one containing turkeyb 19:18:59 MissPiggy, now I'm not going to give you any more info than that 19:19:07 yck 19:19:14 was that "thanks"? 19:19:18 no 19:19:22 then what was it 19:19:57 MissPiggy, also it is on the esolang wiki I bet 19:20:07 unlike AnMaster, I am not a blithering jerk 19:20:08 http://catseye.tc/projects/turkeyb/doc/turkeyb.html 19:20:11 loll 19:20:15 alise, hey you do that to me 19:20:21 so stop claiming not being a jerk 19:20:25 yes because i like irritating you :) 19:20:41 Animated from the cover of an edition of New Scientist magazine, February 1977. 19:20:44 ... (more info) 19:20:45 alise, discrimination 19:20:47 (less info) 19:20:48 Mrs Smith teaches the blind baby to see 19:20:56 AnMaster: yes. 19:21:03 MissPiggy, also http://esoteric.voxelperfect.net/wiki/TURKEY_BOMB 19:24:39 -!- tombom has joined. 19:29:06 It would be nice if my language was a language to describe values of certain types, and have certain values be programs that result in values of certain types, maybe. 19:29:14 Although in a total language, I guess they're the same. 19:34:27 alise: Hey, that sounds like my language. 19:35:00 "My language", said by Chris Pressey; one of the most ambiguous statements ever made? 19:35:07 lol 19:35:56 OK, OK! The "for real" language I want to do but never will. 19:36:29 But what do you mean by "total language"? 19:36:36 Well, Lisp fits the description, if you say that there's only one type. 19:36:42 (Which lets you model untyped languages.) 19:37:02 cpressey: A total language is a functional programming language without general recursion; structural recursion is instead substituted. All programs halt. 19:37:08 total implies that every expression has a result (no exceptions, no infinite loops) 19:37:19 (You can have TCness, though, with coinductive data types and even emulate non-totality with a partiality monad. It's Complicated.) 19:37:43 Basically, e.g. Natural in a regular FP lang is Natural | Bottom 19:37:44 well, a strictly total language can't be TC 19:37:48 OK, that's what I thought. 19:37:49 Bottom = nontermination, 19:37:56 errors, etc. 19:37:58 but you can have an almost-total language which is 19:38:01 cpressey: It's good because you can adorn it with dependently-typed languages, and get a constructivist proof system. 19:38:08 Types = propositions; values = proofs. 19:38:23 Otherwise "let x = x in x" is a proof of anything, which is rubbish. And if you have dependent types and non-totality, typechecking can loop forever. 19:38:34 scarf: Well, it's the magic of codata. 19:39:08 For a lot of stuff I'm happy with merely primitive recursive. I wrote a totality-checker for Scheme programs in Scheme once. I wrote it in PR style and it passed its own check. 19:39:32 It's sufficient for anything w/ a partiality monad etc. 19:39:41 If you've used Agda, Coq, or Epigram; they're all total. 19:39:49 Most of the time you don't even notice. 19:41:19 cpressey: oh, a program to see if a program is primitive-recursive or not? 19:41:28 -!- tombom_ has joined. 19:41:44 scarf: Well, written in a certain PR style, yes. there are probably PR programs that it wouldn't see 19:41:50 ah, ok 19:42:10 But if it's not PR, it would tell you that. 19:42:34 The "pure" way to do it is to define one inductive data type and base them all on that. 19:42:45 data Mu f = Mu (f (Mu f)), basically. 19:42:52 And then a function to deconstruct such types recursively. 19:42:57 Plus no actual recursion facility. 19:43:14 hmm, ⅋ is a great punctuation mark 19:43:35 -!- tombom has quit (Ping timeout: 246 seconds). 19:43:52 alise: I have ... different ideas about type systems. 19:44:41 cpressey: That's nice. 19:44:45 cpressey: Such as? :P 19:45:03 I mean, type checking is a kind of static analysis, and all static analyses (incl but not limited to type checking) can be expressed in terms of abstract interpretation. 19:45:14 Well... yes. But that's at a metalevel to what I'm talking about. 19:45:19 Are you familiar with dependent types at all? 19:45:31 Well, kind of. Yes, passingly familar. 19:46:12 Yeah. The difference in perspective when you just add dependent types is immense. 19:47:03 it's like you're on acid while everyone else is merely drunk. 19:47:41 hmm, one thing I'd like to do someday is to redo Splint, but properly 19:47:51 lament: EXACTLY 19:47:54 as in, actually working, and with a set of types rich enough to actually describe interesting programs 19:48:00 Well, what I'm getting at is, I'd like to design a language without any particular type system, and let different type systems be "plugged in", by allowing them to be written in some kind of annotation language for abstract interpretation. 19:48:24 That would in no way preclude the use of dependent types... 19:49:11 That sounds fun. 19:50:05 alise, what is your opinion on ipad btw? Now that it isn't as new any longer, and there are (maybe) some reviews out there 19:50:06 Not too different from just saying "Here's my dynamically typed language, y'all write your own linters for it plz k thx", except a little less hands-off 19:50:44 AnMaster: It's probably good at what it does and it's damn flashy, but what it does isn't what I want to do. 19:51:07 alise, Right. Someone linked me this image (related to this): http://thismight.be/offensive/uploads/2010/03/01/image/288902_Think%20different.jpg 19:51:19 not actually offensive (as the url would indicate) 19:51:27 well, maybe to apple fanboys 19:51:29 :D 19:51:31 totally SFW though 19:51:32 iSpace 19:51:39 alise, ooh that would be the next step 19:51:49 a totally flat 2d plane underneath all of space itself 19:51:53 then... 19:51:55 iCube 19:51:57 then... 19:51:58 iUniverse 19:52:01 (filling in the corners) 19:52:11 heh 19:55:25 bbl 19:55:32 newtype Mu f = Mu (f (Mu f)) 19:55:32 data Nat nat = Succ nat 19:55:32 instance (Show nat) => Show (Nat nat) where 19:55:33 show (Succ n) = "Succ (" ++ show n ++ ")" 19:55:33 instance (Show (f (Mu f))) => Show (Mu f) where 19:55:33 show (Mu x) = show x 19:55:36 You wouldn't believe it, but this actually works. 19:55:46 There are some other cool methods for termination analysis that have come out of term-rewriting research. I wanted to play with those in Scheme, but I balked at reworking the Scheme semantics into a rewrite system... 19:55:47 does it need flexible instance 19:55:54 yes; and undecidable instances too 19:56:03 Mutually recursive typeclass instances. Fuck yeah. 19:56:42 -!- mrbug has left (?). 20:01:10 I totally do not get it. Well, not totally. Actually I get the idea. Just not the mechanics. 20:01:44 Then you have to realize, I'm living in a code-world where people still say things like d["%s_%s" % (a, b)] = c 20:02:04 I thought that sort of stuff died with Perl 4 20:03:18 that isn't legal Perl4, surely? 20:03:45 Ah, no, in Perl 4 it would be $d{"$a_$b"} = $c; 20:03:53 But the IDEA is Perl 4-ish. 20:04:21 Because when you can't store a dictionary inside a dictionary, well, you compose keys. 20:04:21 you'd write it $d{$a,$b} = $c 20:04:31 where, instead of using _ to compose the keys, it uses the value of $; 20:04:42 which is by default ASCII 28, on the basis that you probably weren't using it for anything else 20:04:59 That would be better style, then. 20:05:07 brb 20:05:09 typical nowadays would be $d{$a}->{$b} = $c 20:05:19 and unlike C, you don't have to set up all the subhashes, they autovivify 20:05:29 so messing with $; is rather deprecated nowadays 20:07:25 scarf: That's exactly my point, or at least part of it. This is Python, where there is no such restriction against storing dicts in dicts. Why are keys being computed? Makes them hell to cross-reference. 20:07:39 cpressey: ah 20:08:29 Sort of my higher point was, in this world, decidable *anything* is a dream -- dependent types are too much to hope for... 20:13:27 otoh, when the type system is C++'s, ... I'm sure that's hardly better... 20:16:07 cpressey: I'm a pessimist, so of course I realise that the only way any of this can work is in my grand unified redesign of all of computing. A pessimistic idealist. What a thing. 20:16:32 alise: hey, I'm a /cynical/ idealist, which is even more ridiculous 20:16:57 what 20:17:01 dependent types are real 20:17:13 I used to be a pessimist idealist, and I probably should have stayed one. 20:17:27 cpressey: what are you now? 20:17:32 MissPiggy: he never denied that 20:17:38 Well, maybe I still am, at heart. 20:18:08 scarf: Now I'm up a certain creek without a paddle :) 20:18:26 Hey, there's that pessimism coming back! 20:19:45 MissPiggy: Yes, in case there was any confusion, I meant only that people *using* dependent types in 90%+ of the industry is a pipe dream. 20:20:24 o_o 20:20:39 uh oh, here it comes 20:20:47 I think BF compilers should use dependent types 20:20:56 and dependent type inference 20:21:07 in order to work out what a program is actually doing, rather than just peephole-optimising 20:22:37 But peephole optimisation is so very *easy*! 20:23:06 yep 20:24:11 Does this connection still work? 20:24:45 Ah, apparently it does... 20:26:48 either that or you're imagining things 20:27:54 dhcpcd took a SIGKILL and then was restarted... 20:28:46 alise, what is tex for dot product? 20:28:53 \cdot? 20:28:56 ah thanks 20:29:21 alise, and normal product? 20:29:31 \times... 20:29:35 oh ffs 20:29:39 I'm too tired for this 20:29:43 :D 20:29:48 alise, wait isn't that vector product? 20:29:56 I mean, a non-vector related scalar product 20:30:28 er... you mean juxtaposition? 20:30:32 what? 20:30:39 i'm trying to account for your tiredness here :) 20:30:42 The scalar product of three and three is nine :P 20:30:59 alise, you know: scalar*scalar→scalar vector*vector→scalar and vector*vector→vector 20:31:03 three different products 20:31:12 I need three different symbols to not confuse things 20:31:14 product of a and b is ab 20:31:19 where a and b are scalars 20:31:21 :P 20:31:28 alise, yeah and product of |a| and |b| is unreadable 20:31:34 tough shit 20:31:36 |a||b| 20:31:36 use \times 20:31:41 use the word "times" 20:31:45 even http://en.wikipedia.org/wiki/Dot_product says |a| |b| 20:31:49 just deal with it 20:31:52 cpressey, NO the point of this is unicode 20:32:12 if you want add some spacing 20:33:08 hm that could work 20:36:18 Silly alternatives: use the explicit a^T b for the dot product, then you can use the center-dot for multiplying scalars if you really need something there. Or the angle brackets for general inner product in place of the dot product, and the same thing. 20:37:48 Personally I think the spacing of \left|a\right| \left|b\right| at least here is readable enough; there's a natural gap in-between, and the |s are closer to the letters than other |s. 20:38:14 If you just write it as "|a||b|" then it won't look right, of course. 20:38:25 |a|b| 20:38:37 plus :: Nat -> Nat -> Nat 20:38:37 plus x = rec (\_ -> x) (\_ z -> suc z) 20:38:37 times :: Nat -> Nat -> Nat 20:38:38 times x = rec (\_ -> zero) (\_ z -> plus x z) 20:38:38 Fuck yeah, structural recursion 20:38:43 fuck YOU! 20:38:49 what 20:40:02 That was an offer, not an insult. 20:41:03 > fact (suc (suc (suc zero))) 20:41:03 (Zig ()) 20:41:04 NOT SO SUCCESSFUL 20:42:08 faftstawfpa4d 20:42:23 alise what should I code 20:42:50 a core total, dependently-typed language! like I'm doing except in Haskell! 20:58:40 I give up. 20:58:47 This code makes my soul bleed. 20:58:58 cpressey: Eat some functionality. 20:59:04 It has good warming properties. 20:59:10 Mmm. 20:59:34 * cpressey listens to some KMFDM 21:00:47 -!- lament has quit (Ping timeout: 256 seconds). 21:01:42 -!- lament has joined. 21:02:07 -!- Oranjer has joined. 21:09:33 I really need to unify my uber-simple-auto-optimised-language-with-everything-as-one-basic-structure-that-acts-as-values-as-types-and-certain-values-being-programs omegalanguage with my total-functional-dependent-types-oh-me-oh-my omegalanguage. 21:10:43 well, hypothetically, how would someone unify chinese and english? 21:11:09 They wouldn't. But natural languages are mishmash and already extant; these are mere concepts that I can bend to my will. 21:11:34 I guess I could use directed graphs for the former - a graph is the type of the graph of the same structure, the type of something like 42 is the ur-element of natural numbers; either 0 or 1+1+1+1... = infinity. 21:11:49 The type of a list of as would be [urelement a] 21:11:55 Although lists would just be sugar over graphs 21:11:59 In fact, everything would be. 21:13:13 Is there a unicode character that's like => without the =? 21:13:21 Just a very small straight two lines and then > 21:14:18 http://www.symbols.com/encyclopedia/04/index.html 21:14:26 it might be here, beats me 21:14:41 Nope. 21:15:11 What do you call a digraph with named arcs? 21:15:23 Well, just arcs with an extra piece of info attached to them that no other arc with the same head shares, I guess. 21:16:47 I don't know if it has a particular name. 21:17:08 annotated, heh 21:17:21 A digraph with labelled edges, is actually what I'd probably call iot 21:17:23 it 21:18:17 Methinks it is the fundamental structure of everything. 21:18:41 A list is 'head -> x. 'tail -> another list. A vector is 0,1,2,... -> element. 21:18:59 A natural is 'pred -> another natural or 'zero. 21:19:09 Long live ASCII bells 21:19:16 (now how many got beeped by that?) 21:19:29 Not i. 21:19:30 *Not I 21:19:35 well I didn't expect that 21:19:55 An unordered set has no annotations. 21:20:03 So I guess the annotation is optional? But that seems rubbish. 21:20:23 ASCII bells, ASCII bells, ASCII all the way 21:20:26 Also, I still need to define a way to reduce graphs to do computation. 21:20:31 Oh what fun it is to ASCII all your console friends awaaaay 21:20:35 "A weighted digraph is a digraph with weights assigned for its arcs" 21:20:57 But they're not weights, just arbitrary tags 21:21:35 -!- SimonRC has quit (Ping timeout: 265 seconds). 21:21:54 -!- coppro has joined. 21:22:12 -!- MigoMipo has quit (Quit: When two people dream the same dream, it ceases to be an illusion. KVIrc 3.4.2 Shiny http://www.kvirc.net). 21:23:16 arbitrary usually means optional, sometimes 21:24:05 totalAge 'people :> {+ ::> people ? 'age} 21:24:09 I think. 21:25:46 http://pastie.org/848777.txt?key=ohkyy1lvvdow7fk8lxaraq 21:25:49 A drawing of that graphs. 21:25:50 *graph 21:26:54 alise: Whatever you're talking about is reminding me of Category Theory. 21:27:04 Arrows, arrows, arrows. 21:27:04 Category theory is fun but not what I'm on about. 21:27:09 It's just graphs. 21:27:12 god damn it people irritate me so much 21:27:13 Arrows? 21:27:25 Basically I'm trying to figure out the most elegant way of doing computation with graphs on graphs. 21:27:37 arrows and monads! 21:27:57 Graphs. 21:27:57 alise: I like the eodermdrome method, but there's probably another 21:28:49 scarf: yes, well, mine's meant to be not so ridiculous :) 21:28:58 also, eodermdrome doesn't have cyclic graphs does it? 21:29:06 abcda 21:29:10 or is that not what you mean? 21:29:24 maybe it is 21:29:29 i mean graphs with internal cycles 21:29:30 hmm 21:29:31 tree :: {'left :> {'left :> 1; 'right :> 3}; 'right :> {'left :> 2; 'right :> 4}} 21:29:38 so i need anonymous nodes 21:29:43 wha tthe fuck isthat 21:29:46 so why not have /all/ nodes be anonymous :D 21:30:39 All nodes are anonymous; there is one distinguished node with named arc to all the "named" nodes, and those arcs contain the names. 21:31:35 Kind of hard to follow where alise wants to go with this design because the design space is so large... 21:31:51 I've only seen anonymous nodes in a semantic web language, where the creator wishes to "reify" an edge--that is, treat it as a node 21:31:59 Basically, the idea is that your entire (operating) system, including every single thing you care about, is one gigantic graph-like of some sort. 21:32:03 Oranjer: RDF? yeah 21:32:09 N3 makes that quite easy 21:32:53 cpressey: Including all the relevant functions/drivers/programs (stored not as machine code ofc), their data, your data... 21:33:14 alise: Arrows? Graphs? Names. 21:33:17 So we need a graph structure that has some property related to the vague notion of "nesting", otherwise our namespaces will get clogged down. 21:33:30 And we need anonymous nodes, because naming every single piece of a nested data structure is ridiculous. 21:33:50 An acyclic graph is probably unworkable, as it means we have no pointers. 21:33:55 Pointers. 21:34:03 cpressey: wat 21:34:27 Every single piece of data is named, isn't it? Otherwise how do you get to it? 21:34:46 And by "named" I mean, there's pointers to it, from other pieces of data. Maybe not explicit ones. 21:35:00 -!- SimonRC has joined. 21:35:13 Good point. 21:35:39 Yes, you are right. Annotated arcs are the same thing as non-anonymous nodes. 21:35:40 Trying to put it into words... there are graphs everywhere already, but they're... what's the word? Latent? 21:35:57 And there are many, many ways to make them explicit. 21:36:49 Oh what fun it is to ASCII all your console friends awaaaay <-- so you got beeped? 21:36:57 AnMaster: No 21:36:59 ah 21:37:39 -!- Libster has joined. 21:39:39 http://pastie.org/848803.txt?key=bybdg9fl0pwv1vrtme9q 21:39:54 Annotated arcs and anonymous nodes: cancelling each other out since today. 21:40:12 alise shut up 21:40:18 ?? 21:40:19 No? 21:40:21 stop taking your anger out on me 21:40:29 what 21:40:38 I haven't even mentioned your name in... forever? 21:40:40 I think it's actually my anger. alise is just borrowing it 21:40:46 AnMaster: My reasonably raw bip bouncer log doesn't show any suspicious ASCII characters in your long-live comment. I guess it's possible the log is filtered, but are you sure freenode's +c filtering doesn't remove ^G too? 21:40:49 MissPiggy: no but seriously what? 21:41:32 fizzie, maybe it does since the ircd switch 21:41:35 if so how sad 21:42:11 -!- Libster has left (?). 21:46:42 AnMaster: http://dev.freenode.net/ircd-seven/browser/include/inline/stringops.h#L57 21:46:59 fizzie, sad 21:47:31 Hmm. 21:47:48 cpressey: My graphs have ceased entirely to be graphs at all, because you can have multiple nodes with the same value. 21:47:50 That isn't kosher, is it? 21:47:51 -!- Azstal has joined. 21:48:31 alise: Wait, I thought only the arcs had values? In which case 2 arcs with different labels can point to the same node, yes. 21:49:05 Not so different from symlinks... 21:49:15 Aliasing. 21:49:21 I realised that if you allow duplicate nodes, all anonymous nodes + annotated arcs = normal nodes + normal arcs. 21:49:25 -!- Asztal has quit (Ping timeout: 268 seconds). 21:49:34 But allowing duplicate nodes means it isn't a graph any more. 21:50:01 I suppose not. 21:50:20 You get from graph (set of nodes, set of edges) a multigraph if you make the edge-set a multiset, but I'm not sure what you get if you make the node-set a multiset too. 21:51:37 Possibly a multi²graph. 21:51:45 -!- adu has joined. 21:51:55 a directed multi^2graph might be what I want 21:52:07 obviously I want a multigraph, otherwise you couldn't have one object in two lists (right?) 21:52:24 In the mathematical discipline of graph theory, a graph labeling is the assignment of labels, traditionally represented by integers, to the edges or vertices, or both, of a graph.[1] 21:52:50 I haven't really been following the context in which your graph lives here; I was busy with my look-up table of ircd sources. 21:53:03 haven't found a graph-theory anonymous-graph though 21:53:09 alise: Of course you can't have one object in two lists. Unless a) those two lists share a tail, and the object is in the tail, or b) the list really only contains a pointer to the object. 21:53:25 Well it's a graph, everything is a pointer :P 21:53:43 Anyway, they can't share a tail unless you can have multiple pointers to one node 21:53:51 So what you want is the same point in two different lists! 21:53:56 *pointer 21:53:56 fizzie: Graphs as the most generalest of all data structures: http://pastie.org/848825.txt?key=das1exf0bvjldwzy6lmag 21:54:00 cpressey: Of course. 21:54:06 But the whole point of using a graph is that it "does pointers". 21:54:17 alise: But pointers *define* the list. 21:54:39 So the same pointer in 2 lists would mean they're actually the same list. 21:55:15 At least, that's how I see it... 21:55:21 I think we're thinking of the wrong thing 21:55:28 Consider the value fred. Doesn't matter what it is. 21:55:42 [fred,bob,lark] and [frak,fred,mogul] 21:55:57 This is impossible in a (non-multi)graph, because there are two arcs ending in fred. 21:56:28 Note that since we have no object identity we can just duplicate the object, but this sucks. 21:56:40 i.e. next(fred) isn't unique, right? 21:56:58 next(fred) has no meaning 21:57:00 I refer to a linked list 21:57:06 list of a = nil or cons(a, list of a 21:57:07 ) 21:57:14 so we have 21:57:24 the list has two arcs 21:57:32 one to "head" (goes to "fred") 21:57:33 well, next(fred, [fred,bob,lark]) might have some meaning, for some defn of next() 21:57:36 one to "tail" (goes to [bob,lark]) 21:57:46 cpressey: Then the issue is removed. 21:58:27 I'm not following ya, exactly... if lists are lists of names of objects, and fred is the name of an object, this is fine. 21:58:41 if fred is the object itself, then you can't say [fred,fred,fred] 21:58:48 Okay, let me show you the structure of a list. 21:59:39 http://pastie.org/848837.txt?key=t2z1krwvkltzmo8hmhizqw 21:59:46 "head" and "tail" are just symbols/atoms there 21:59:57 but "fred" just means that this arrow points to the fred node 22:00:00 imagine fred as another list 22:00:08 so we'd have 22:00:09 head 22:00:10 | 22:00:12 foo 22:00:16 / \ 22:00:17 head tail 22:01:43 Maybe I am all wrong about everything. 22:02:29 -!- Libster has joined. 22:02:40 -!- ChanServ has set channel mode: +o lament. 22:02:42 -!- Libster has left (?). 22:02:47 too late 22:02:48 lol 22:02:53 -!- lament has set channel mode: -o lament. 22:03:15 who's Libster? 22:03:18 a troll 22:03:25 (self-proclaimed; really bad at it) 22:03:26 -!- Libster has joined. 22:03:26 we get trolls her? 22:03:29 *here? 22:03:40 alise: http://pastie.org/848845.txt 22:03:41 scarf: only because MissPiggy got Libster and ...base3? annoyed or something a while ago 22:03:55 cpressey: Yes. But note that fred *is not a name*. 22:04:02 'fred' and 'fred' can be the same node, if you like. 22:04:03 -!- Libster has set topic: alise sighting counter currently out of order | http://tunes.org/~nef/logs/esoteric/?C=M;O=D | lament sux. 22:04:04 Imagine both those head lines swirling around to wherever fred is, and latching on. 22:04:13 Sure. 22:04:17 So it's a multigraph. 22:04:18 -!- ChanServ has set channel mode: +o lament. 22:04:19 Or that would be impossible. 22:04:22 -!- lament has set channel mode: +b *!*Libster@*.bltmmd.east.verizon.net. 22:04:24 -!- scarf has set topic: alise sighting counter currently out of order | http://tunes.org/~nef/logs/esoteric/?C=M;O=D. 22:04:36 lol 22:04:37 spambot 22:04:37 -!- lament has set channel mode: -o lament. 22:04:40 lament: is that the actual reason? 22:04:44 I love your reasoning 22:04:57 alise: you're right, that is /incredibly/ bad trolling 22:04:58 libster is a GLUT 22:05:06 -!- Quadrescence has joined. 22:05:06 alise: http://pastie.org/848850.txt ? 22:05:16 either he or base3 propositioned me for sex the first time (on this nick) 22:05:33 they are pretty colossally bad trolls 22:05:43 cpressey: no; the head of the second list points /away from the whole thing/ 22:05:47 to whatever "fred" means in this context 22:05:49 that IS why you chose this nick, isn't it? 22:05:58 both heads are different arcs, ending at the same node 22:06:05 lament: well, partly. 22:06:14 also to topple the fascist english pronoun structure through sheer absurdity 22:06:20 I don't see why you'd proposition random people for sex over IRC, given how unlikely it is you live within walking distance of each other 22:06:27 turns out people don't use gender-specific pronouns much on irc, though 22:06:38 I actually use a spiral to indicate anonymous nodes, myself 22:06:38 scarf: Virtual reality is JUST ALONG THE CORNER 22:06:41 *AROUND 22:06:43 AROUND the corner 22:06:51 alise: but then, you wouldn't need anyone real to have sex /with/ 22:06:56 scarf: Why did you change nicks? 22:07:07 hey are we talking about sex 22:07:07 Realistic sexbots: Harder than VR 22:07:11 coppro: saw that this one wasn't taken, and thought I might as well 22:07:20 -!- coppro has changed nick to Cu. 22:07:23 alise: http://pastie.org/848855.txt 22:07:25 fair enough :P 22:07:27 * alise is now known as nt 22:07:30 We're a perfect pair 22:07:34 Quadrescence: unfortunately 22:07:36 cpressey: Yes. That's a multigraph. 22:07:39 nt is not an element! 22:07:48 Cu is an element 22:07:50 alise: It is?? 22:07:50 Quadrescence: were you lurking here in the hope that the channel went offtopic? 22:08:01 I only see one node at the end of each arc... 22:08:05 -!- Cu has changed nick to Cn. 22:08:07 scarf: I'm not sure. 22:08:10 aw, this one is taken 22:08:22 I want my copernicium :( 22:08:23 Quadrescence: that's a good enough answer, I suppose 22:08:25 -!- Cn has changed nick to coppro. 22:08:35 cpressey: In mathematics, a multigraph or pseudograph is a graph which is permitted to have multiple edges, (also called "parallel edges"[1]), that is, edges that have the same end nodes 22:08:41 *nodes. 22:08:45 QED 22:09:16 Does this include directed graphs where the two edges go opposite directions? 22:09:37 Ooh, good question. 22:09:40 hm now we are talking about graphs 22:09:46 Graph sex. 22:09:49 I thought graphs can could not have edges that end in the same node were called "trees". 22:09:50 coppro: I would guess yes. 22:09:55 s/can/that/ 22:10:14 cpressey: Yeah, because a tree can express cyclic structure, innit. 22:10:17 *structures 22:10:25 foo -> bar, bar -> baz, baz -> foo: A TREE 22:10:34 aren't trees supposed to be acyclic? 22:10:39 cpressey: if you can have two edges AB and AB, it's a multigraph; if you can have AB and also AC+CB, it's a normal graph; a tree, if you can get from A to B one way, even indirectly, you can't get there another way 22:10:39 coppro: yes 22:10:47 directed acyclic graph = tree 22:10:51 In my world, trees are acyclic, yes. 22:11:08 Quadrescence: that's not strong enough 22:11:15 Right, so a non-acyclic non-multigraph graph is not a tree. 22:11:17 imo 22:11:17 It's just a graph. 22:11:21 coppro: You could require more, but whatever 22:11:36 Any vertex should only have one edge leading to it 22:11:47 coppro: that's... K_2, or K_1 22:11:48 why say 'tree' when you can say 'directed acyclic plant' 22:11:53 there are no other graphs with that property 22:11:56 well, undirected ones 22:12:20 HEY GUYS 22:12:22 HOWSIT GOIN 22:12:31 scarf: we're talking about directed ones 22:12:38 alise: I'm still confused; I don't see any edges "AB and AB" (scarf's words) in my diagram. So I don't see how it's a multigraph. 22:13:05 I see, uh, ABCD and AEFGHD, or something similar 22:13:13 maybe i read the words wrong 22:13:23 "that is, edges that have the same end nodes" 22:13:26 not same start nodes, no? 22:13:35 It's AB and CB. Maybe I am misinterpreting. 22:13:46 Well, I thought it was: two (direct) edges between the same two nodes. 22:13:59 In a tree, the path between the root and to another node must be unique 22:14:00 (AB and AB) 22:14:03 HOW IS THAT 22:14:27 cpressey: Considering the diagram on the page I concede; you are right. 22:14:41 http://www.youtube.com/watch?v=FJ3oHpup-pk 22:14:54 I think anonymous nodes + annotated arcs is best, because otherwise I have to have dummy nodes on lists like "list" 22:14:58 what are you people talking about 22:15:00 jesus 22:15:05 which is really just a stand-in for an anonymous node 22:15:19 and besides, what if the name node (= arc annotation) has multiple connections from it? that makes no sense 22:15:42 alise: Well, the 'list' labels actually make a lot of sense to me. 22:15:44 A nice thing we can have from this is that a scope/environment/whatever just has variable names as the graph annotations. 22:15:45 augur: Clearly we are talking about categorical monadic parser combinators and language grammars 22:15:56 cpressey: I think I'll have a typing system apart from such annotation, though. 22:16:02 language grammars?! 22:16:05 hellll yeah 22:16:10 lets talk bout some grammars 22:16:11 they kind of reflect: data List = List head tail | Nil 22:16:12 Yes 22:16:13 :D 22:16:17 okay i love grammars 22:16:26 You need to keep repeating "List" there to conform to the "grammar" of the data type. 22:16:28 have i shown you my contributions to wikipedia? 22:16:31 no 22:16:32 cpressey: I see what you mean. 22:16:34 o man 22:16:48 (Everyone kept saying "grammar" so I typed it in what I was typing. Scary.) 22:16:49 I remember you though from whatever irc channel augur. 22:17:01 ##compsci 22:17:04 yes 22:17:07 But in a "graphy" language, we would say that both nil, and any node with two arcs annotated 'head and 'tail, where the latter obeys these same constraints, is a list. 22:17:11 or maybe ##proglang 22:17:16 chomsky hierarchy 22:17:18 somewhere in that direction 22:17:20 alise: I can see why you would want to cut it out though, it's all so.... verbose. 22:17:32 augur: do you have to be Ada Lovelace to register #proglang? 22:17:32 cpressey: Yes. Would you rather right 22:17:33 *write 22:17:35 {'left :> {'left :> 1; 'right :> 3}; 'right :> {'left :> 2; 'right :> 4}} 22:17:36 or 22:17:54 i can't even bring myself to write it 22:17:55 too ugly 22:18:11 (1:3):(2:4) ? 22:18:20 Quadrescence: http://toolserver.org/~soxred93/pages/index.php?name=Augur&namespace=0&redirects=noredirects 22:18:21 no, the same but with tree labels everywhere 22:18:27 what you said would be sugar :P 22:18:27 oh 22:18:33 yeaaaaahhhh no. 22:18:40 yeah no to what? 22:18:51 no, i wouldn't want to write it either. 22:19:02 yeah 22:19:04 i also added to the Indexed grammar page and the Combinatory categorial grammar page 22:19:09 augur: wow 22:19:41 cpressey: Cool thing about scopes just being graphs with variable names as arc annotations: We can have a thing for "in scope" which lets us add stuff to a graph without naming it each time, and this is the same as our scoping operator. 22:19:56 Quadrescence: the controlled grammar article took about a week 22:19:59 Yes. 22:20:14 -!- breeden has joined. 22:20:17 It also relates to the tuple-space of languages such as K: every single thing in the environment can be accessed by a list of names relative to the root of the environment. 22:20:23 Ugh, graph of free variables in outer closures etc. 22:20:40 -!- breeden has left (?). 22:20:46 augur: this is the very important stuff I have done http://en.wikipedia.org/wiki/Special:Contributions/Quadrescence 22:21:14 i see! 22:21:22 I guess functions should be "abstract nodes"; if we have a natural being {'pred :> natural} | 'zero - so e.g. {'pred :> {'pred :> 'zero}} is 2, then we can say 2 'pred = 1. 22:21:28 So it is natural to wish for 2 'succ = 3. 22:21:30 no pages created :( 22:21:51 yeah 22:22:00 alise: Your omission of 'list labels also permits "duck typing", for better or wose: anything that works on things that have lefts and rights, works on your structure. 22:22:00 I am too cool I guess 22:22:04 But does this belong in the ubergraph itself or just as sugar in the language? After all, the whole idea is that the language is just syntax to describe graphs, and some graphs are typed and interpreted as programs. 22:22:15 TOO LAME YOU MEAN 22:22:15 cpressey: Yes. I'm planning some sort of typing, though; just have to think about it first. 22:22:17 :P 22:22:24 augur: yeah true 22:22:29 augur: I do write stuff though 22:22:41 like I am writing a BOOK 22:23:04 -!- kar8nga has quit (Remote host closed the connection). 22:23:05 im a total grammar nerd, and i tried looking for a lot of these grammars but couldnt find anything 22:23:11 cpressey: In that group language of yours, the concatenation of a program with itself isn't the inverse, right? You have a separate inversing function of sorts. 22:23:11 so i did research, found papers, books, etc. 22:23:18 So that part of languagespace is still open for my design. 22:23:19 then wrote the wikipedia articles, for future curiousiters 22:23:30 wth: 22:23:30 http://www.lspace.org/books/apf/reaper-man.html#p1516 22:23:37 " If you have access to the Internet, you can find an online version of this story at the URL: 22:23:37 " 22:23:40 augur: Maybe you can help me design some syntax then 22:23:43 what do they think 22:23:45 alise: Correct. In general xx != e 22:23:46 on a website... 22:23:47 maybe! 22:23:55 Since my biggest concern for syntax is making the grammar easy peasy 22:24:03 AnMaster: APF Chapter 3: Discworld Annotations 22:24:12 http://www.lspace.org/books/apf/ 22:24:12 like lisp :))))))))))))))))) 22:24:13 alise: You have to find x' for which xx' = e. But x' exists (well, in the fixed version, it does.) 22:24:14 Organisation: Unseen University 22:24:14 Newsgroups: alt.fan.pratchett,alt.books.pratchett 22:24:19 well, grammar for what 22:24:22 'nuff said 22:24:30 augur: a programmin' lang' 22:24:35 cpressey: Right. What I'd like is xx = e. 22:24:42 i see 22:24:43 alise, hm good point 22:24:50 well, most programming languages have context free grammars 22:24:52 so 22:25:08 alise: ... good luck. :) 22:25:20 maybe I shouldn't be simple 22:25:23 cpressey: That ... is the sound of the language being useless, isn't it? 22:25:26 Maybe I should be complex but elegant 22:25:38 alise: That is the sound of my brain stopping. 22:25:45 Quadrescence: its often quite hard to find a reason why you would want the extra complexity 22:25:48 Well, bit-flipping does it. 22:26:01 -!- dev_squid has joined. 22:26:07 natural language has it, as far as i can tell, solely for efficiency 22:26:13 augur: Well, the language in design is very complex itself. 22:26:16 Hey guys. 22:26:17 but computers have no need for this. 22:26:20 And say we have some piece of state s=0 normally, and have an operation meaning "if s=0, move left, if s=1 move right. flip s" 22:26:22 dev_squid: calamari? 22:26:25 ok, tell me about this language 22:26:33 Gregor, heheh. Sorry? 22:26:49 Glad to see #esoteric is still active. 22:26:50 Quadrescence: will your language be used to program underwater exploration robots? 22:26:56 lament: yes 22:27:07 *confused* 22:27:15 dev_squid: Was asking if this is an alt nick for the one known as "calamari" :P 22:27:32 augur: It is as statically typed as possible, but it is very dynamic in nature, um...., it will be used for mathematics 22:27:52 primarily for math 22:27:55 It is flexible yet rigid, hard yet soft 22:27:59 yes 22:28:02 my cock? 22:28:08 dev_squid: Thou art... Who? 22:28:08 non-newtonian fluid like 22:28:25 and lament-cock like 22:28:25 pikhq, I used to hang around here a while ago. 22:28:32 Gregor, nah. 22:28:36 dev_squid: Yes, just don't recall the nick. 22:28:38 dev_squid: I bet there wasn't so much gay sex then. 22:28:47 And I've been around for quite some time. 22:28:48 Wow >_> 22:28:48 alise, is there now? 22:28:58 alise, o.o 22:29:02 augur: I don't know, maybe I'll tell you about it more later 22:29:03 dev_squid: yes >) 22:29:04 Pray tell, what nick did you use? 22:29:24 dev_squid: Well, sometimes. 22:30:21 Apparently dev_squid had not a nick in the past. 22:30:21 Anyway, just to clear up this issue that's been bothering me for a while...if you limit a language to only being able to deal with two bytes of storage (i.e. RAM), can it still be turing-complete? 22:30:32 No. 22:30:38 Why not? 22:30:42 *deal* with? yes 22:30:46 *only have*? no 22:30:49 pikhq, this is my new computer. 22:30:50 dev_squid: Because it can't. 22:30:54 Because a Turing-complete language must have unbounded memory. 22:31:01 True, true. 22:31:11 dev_squid: Still not informing me about what nick you had previously. ;) 22:31:16 Waaaaait wait 22:31:20 dev_squid: You can manipulate two bytes at a time and be turing complete 22:31:26 If it can only have two bytes of storage, but can have I/O, it may still be TC. 22:31:38 But could you DO anything in a 2-byte environment that you could do in a fully turing-complete environment? 22:31:49 Gregor: Not without fixed IO sources... 22:32:02 dev_squid: there isnt a machine in existence that is turing complete. 22:32:12 its not even theoretically possible to build a turing complete machine. 22:32:18 he didn't say so 22:32:20 dev_squid: all your machine has is 2 bytes? 22:32:27 alise: I didn't say /any/ I/O would make it TC, but it's possible that I/O would be sufficient, with the right kind of I/O. 22:32:28 16 bits of memory? 22:32:33 augur: Hey, I've got spools of unbounded tape right here! 22:32:43 pikhq: ;) 22:32:45 you would 22:33:09 Hey, I've already made the I-am-a-turing-machine-and-my-genitalia-comprise-the-tape joke. 22:33:15 dev_squid: For any program you can write for your 2-byte computer, I can tell whether it will halt eventually, or not. Therefore it's not TC. 22:33:22 so the technical answer to your question, dev_squid, is no, your machine aint turing complete. but that doesnt matter. its a proper subclass of the turing machines, those that are Turing Complete-enough 22:33:24 Including the corollary wrapping-universe-so-I-am-actually-sexing-myself-up subjoke. 22:33:31 dev_squid: someone has built a 4-bit computer, that's way sexier. 22:33:34 * pikhq greps logs for dev_squid 22:33:35 cpressey: OR CAN YOU 22:33:40 alise: o mai 22:33:46 cpressey, alright, alright. I didn't put that question very clearly. 22:33:47 Definitely never had someone using that nick here. 22:33:47 ur gettin me hawt 22:33:48 alise: Well, not me personally. My hordes of servants. 22:33:52 But I get it now. 22:33:53 augur: not turing complete enough if it only has one bit of address 22:34:00 then it cannot be made tc without serious graft surgery 22:34:07 alise: depends on how you handle memory. 22:34:18 depends on how your mom handles memory 22:34:29 i dont think she handles memory well 22:34:35 precisely 22:34:46 i popped your mom's stack 22:34:57 unfortunate 22:35:33 -!- tombom_ has quit (Quit: Leaving). 22:35:53 I was just wondering if it's viable (not practical!) to construct a language that only allows the programmer to operate on two bytes of RAM on bit at a time. 22:35:59 It would make quite the challenge. 22:36:11 * pikhq continues to enquire 22:36:37 Hey, I think that my language should allow multi-word symbols. 22:36:39 Just cause. 22:36:44 dev_squid: operate on, or address using? 22:36:49 so smallfuck with 16-cell memory 22:37:07 (for example) 22:37:09 like, the programmed can address an arbitrary number of memory cells, each of which is only 2 bytes? 22:37:22 programmer** 22:37:28 augur, no. 22:37:32 Hrm. Who hasn't been around in sufficient time to be surprised #esoteric's still active? 22:37:40 me 22:37:45 me 22:37:54 pikhq: hcf 22:37:55 No wait, ... 22:37:55 dev_squid: ok, clarify then? 22:37:57 Think of brainfsck where you're inconvenienced by having two bytes of data space to work with. 22:37:59 Who's been *gone* for sufficient time. 22:38:03 me 22:38:07 dev_squid: *Brainfuck. 22:38:11 ... ok, right. me. 22:38:18 dev_squid: i dont know jack shit about brainfuck. 22:38:25 cpressey was gone forever 22:38:26 cpressey: Ah, right. 22:38:30 and me, slightly less than that 22:38:40 alise, I don't really know the rules on profanity, so I just went with brainfsck. 22:38:52 lament: When did you wander back? Must have been shortly before me, I reckon. 22:39:02 Fucking hell, you think we give a shit about profanity? Only an utter cunt would do that! 22:39:02 (Pard'ner.) 22:39:06 (Just doing my job to lower signal/noise.) 22:39:09 Heheh. 22:39:10 dev_squid: Profanity? Yes please. 22:39:13 cpressey: He's been here intermittently forever. 22:39:20 alise: you watch your mouth! 22:39:22 He's just shocked every single day we still exist. 22:39:24 cpressey: i'm not sure. there was a dark ages kind of period in the history of #esoteric 22:39:26 * augur slaps alise cross the mouth 22:39:29 kids these days 22:39:32 lament: yes, all of it 22:39:51 no, it was pretty cool before you joined 22:39:52 lament: i made the sparkline, ma'am. activity has been /steadily rising/ since the start, and has never gone significantly down 22:40:02 lament: lawl 22:40:13 by dark ages i mean noise-to-signal, not volume 22:40:42 i remember something about razor-x and anime. 22:40:46 lots and lots of anime discussions. 22:41:00 i remember seeing you whine about that when feeding everything to that kicker bot thing :D 22:41:19 also signal/noise presumably, so that it gets lower as quality is shittier 22:41:50 what 22:42:31 not noise/signal 22:42:49 lament! :o 22:42:55 hey changod 22:43:02 no that's andreou 22:43:04 hows the changoddery 22:43:12 close enough 22:43:43 i'm not god :( 22:44:02 but dont you have ... 22:44:06 THE POWER? 22:44:13 scarf: my language seems to unintentionally have autovivification, yet it is totally "pure" i.e. no hacky stuff. do you approve? 22:44:19 yes 22:44:28 i think i need to go shopping 22:44:31 bye 22:44:38 i have godlike powers, sure 22:44:38 Here's my idea: a language which can only operate on one bit at a time of one of two bytes in memory...your'd have your standard bitwise operators like AND, OR, XOR, and NOT, except these took bits as operands, not bytes like an 8-bit processor. I guess you could say it (sort of) simulates machine language of a 1-bit processor...sort of. 22:44:49 *you'd 22:45:02 dev_squid: this language would be... limited. 22:45:08 lament, very. 22:45:15 -!- adu has quit (Quit: adu). 22:45:25 is it a von neumann machine? 22:45:32 Well... 22:45:33 are programs limited to being 2 characters long? 22:45:48 lament, no. 22:45:59 lame 22:46:13 the 4-bit computer people have built is a von-neumann machine 22:46:49 dev_squid: I'm sure there are some (small) problems such a computer could solve 22:47:02 operative word there being, uh, small. 22:47:16 it could easily add 1 and 2 22:47:56 dev_squid, how many bits in a bit? 22:47:59 The only thing making that actually do anything at all is not being Von Neumann.. 22:48:18 scarf: don't suppose you're interested in the details? 22:48:21 I'll come back later when I've formulated a better explanation. I'm confusing myself even. 22:48:33 alise: no, busy having a flamewar atm 22:48:39 heh, about what? 22:48:45 -!- oerjan has joined. 22:49:20 if hasattr(xyz, 'xyz'): self.xyz = xyz.xyz 22:49:41 That's what's been causing me so much pain. (The names were changed to protect the "innocent".) 22:50:01 ... 22:50:34 This is what happens when you mix subclass-based inheritance with delegation at your whim. 22:50:40 MUD. 22:50:48 anywho 22:50:54 help alise 22:51:17 MissPiggy: wut 22:51:25 alise what about haskell' 22:51:34 I could always make it where you have [8 bits][1-bit swap space][8 bits]. Basically, you can toggle which 8-bit cell you're operating on, while also being able to pass data between the two via the 1-bit swap cell. It wouldn't be a realistic model by any means, but it'd be interesting. 22:51:40 which is basically nothing at all but you have so many extensions you can turn it into anything 22:52:03 MissPiggy: What about it? 22:52:18 that' s my idea 22:52:39 Anyway, I love minimalistic or limiting esolangs because when you manage to write a working program in them, you feel much more accomplished...IMHO. 22:52:49 MissPiggy: well that's the reality of haskell today :P 22:53:49 Actually, I really have to have anonymous nodes with named arcs, I think: because I really can't have nodes all being unique. 22:53:58 George --- name --- something, Robert --- name --- something. 22:54:01 Krr, name is duplicate. 22:54:12 Or is there a name for a graph where you can have duplicate nodes? 22:54:38 MissPiggy: http://hackage.haskell.org/trac/haskell-prime/ ? 22:55:26 no 22:55:36 their "Haskell 2010" sounds like hell 22:55:51 yeah 22:56:11 Hell how? 22:56:18 Haskell 2010 is just a standardisation of, well, GHC. 22:56:30 for integer exponents it is trivial to implement. Somewhat more involved for non-integers. 22:56:48 Well, if GHC is to Haskell as gcc is to C, ... 22:57:30 It's not, though? :P 22:57:33 haskell has three different power functions, dependent on whether the underlying type allows just multiplication, allows division, or allows general powers 22:57:41 oerjan: wait what's the third 22:57:44 I know ^ and ** 22:57:47 ^^ 22:58:30 you cannot implement the last one (**) cleanly for rationals 22:58:44 alise: Haskell 2010 is not a standardisation of GHC. 22:58:50 didn't even know of ^^ 22:58:53 It's a standardisation of a handful of GHC extensions. 22:58:59 pikhq: shaddap 22:58:59 :P 22:59:25 alise: it's defined for rationals, but it won't help you take cube roots alas 22:59:36 ((^^)) 22:59:48 desu 23:00:00 * cpressey was waiting for that 23:00:28 btw, is there some way to get Hugs to tell me what types implement a particular type class? 23:00:36 cpressey: Step one, don't use Hugs. 23:00:42 :( 23:00:53 You're going to make me wait for all my crap to COMPILE, aren't you. 23:00:58 cpressey: ghci 23:00:59 i think the idea of a cell containing 5/3 bits is hard to think about logically. 3 of them should give 32 possibilities, but how do you achieve this consistently? maybe it's something quantum :D 23:01:05 Compiles on the spot, interactive like hugs. 23:01:09 runghc foo.hs 23:01:14 Runs the program like a script interpreter. 23:01:38 Hugs doesn't even have the latest major version of the standard library, which changed quite a bit. 23:01:42 alise: OK, I'll give it a shot. 23:01:43 Does it even have 3? 23:02:04 Hugs is like... Dead. 23:02:18 alise: I'll give it a shot if it can tell me what types implement Integral. 23:02:28 cpressey: even ghc cannot do it without you having loaded the modules defining the type instances, i think. 23:03:08 Maybe I'll just stick to Visual Basic. 23:03:09 otoh the web documentation frequently lists types defining a particular class 23:03:22 although maybe that's module-dependent too 23:03:23 oerjan: I couldn't find it in the docs, that's why I was curious. 23:03:37 What, besides the various integery types, implement Integral? 23:03:44 nnone 23:03:46 none 23:03:47 nnone 23:03:47 nnone 23:03:53 Prelude> :info Integral 23:03:53 class (Real a, Enum a) => Integral a where 23:03:54 quot :: a -> a -> a 23:03:54 rem :: a -> a -> a 23:03:54 div :: a -> a -> a 23:03:55 mod :: a -> a -> a 23:03:55 quotRem :: a -> a -> (a, a) 23:03:55 divMod :: a -> a -> (a, a) 23:03:56 toInteger :: a -> Integer 23:03:56 -- Defined in GHC.Real 23:03:56 instance Integral Integer -- Defined in GHC.Real 23:03:57 instance Integral Int -- Defined in GHC.Real 23:03:59 (Sorry for the flood.) 23:04:02 Import more modules, get more Integrals. 23:04:11 alise: Thank you. 23:04:14 cpressey: in addition to the standard Int and Integer, the Int* and Word* types from Data.Int and Data.Word 23:04:19 Of course you can't just say "import *" then look. 23:04:30 are the ones i know of 23:06:00 -!- scarf has quit (Remote host closed the connection). 23:07:49 cpressey: http://www.haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html has a sizable list a way down 23:08:07 oerjan: Thanks. 23:08:23 http://www.haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#7 23:08:39 is the closest anchor i could find 23:08:45 haskell.org is not responding for me, lovely 23:09:06 oh, it's just reeeeeally slow 23:09:08 oh? i just brought it up 23:11:30 i guess most of those are for the ffi, lots of C types 23:12:26 and of course those are at most the instances that come with ghc. other packages can define their own. 23:12:34 I finally made a channel for my system/language/thingy. #usys 23:20:27 let's say you have 6 * 5/3 bits in a row. that is 10 bits. now you should be able to read off 5 bits starting from _any_ of the 4 first 5/3 blocks. 23:20:51 heh 23:21:34 -!- Asztal has joined. 23:22:08 -!- Azstal has quit (Ping timeout: 245 seconds). 23:22:11 also, if you read off 5 bits from overlapping areas, you should be able to deduce all other 5 bit offsets inside that same area 23:22:29 *from two overlapping areas 23:23:08 this is probably enough to get a logical inconsistency 23:23:41 alise 23:24:47 hm more generally you should be able to take any three 5/3 bits and combine them into a 5 bit value 23:26:21 maybe there is some mad sort of logic where this kind of thing is allowed. i've vaguely heard that toposes replace boolean truth values with something else... 23:27:07 (varying by topos) 23:29:20 -!- dev_squid has quit (Ping timeout: 246 seconds). 23:30:47 -!- dev_squid has joined. 23:35:52 -!- Oranjer has left (?). 23:36:58 heeeeeyo 23:37:43 yoooyo 23:38:31 ma 23:46:41 -!- angstrom has joined. 23:51:09 !haskell data Nat nat = Succ nat deriving Show; main = print . Succ . Succ . Succ $ "Test" 23:51:19 Succ (Succ (Succ "Test")) 23:51:23 hah 23:51:35 BAI NAO 23:52:02 alise: your Show instance for Nat back when was just the usual derived one 23:53:16 oerjan: hm right 23:53:27 why hah? 23:53:41 or almost. it left out the parentheses around "Test". 23:53:54 alise: because you didn't notice it? 23:54:06 well i was being careful :)