00:00:01 <oerjan> it _starts_ with a sex change, and then you turn into a furry
00:00:38 <alise> also, haw haw signal/noise has just approached 0
00:00:43 <pikhq> ... I accidentally used the plural. Hooray.
00:01:52 <alise> data ℝ : Set where
00:01:52 <alise> → {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂}
00:02:57 <alise> pikhq: also does that make sense with "either one"?
00:03:17 <alise> 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 <alise> coppro: THAT IS NOT ADMIRATION
00:03:47 <coppro> great, I've pissed off alise. See you Tuesday
00:04:38 <coppro> alise: because you're a girl, obv
00:06:58 <pikhq> alise: Hmm. *Looks* like the standard definition of the computable reals from the rationals.
00:07:29 <pikhq> I'm going with "Sure, makes sense". ;)
00:07:35 <alise> euler = ℝ (λ ε → sum (map (λ i → (i!)⁻¹) (1 … ε)))
00:07:55 <alise> yes I am using x⁻¹ in place of 1/x WHAT OF IT
00:08:24 <pikhq> I have no complaints.
00:09:11 -!- adam_d has quit (Ping timeout: 265 seconds).
00:09:36 <alise> and (m … n) for range, mostly because I can't think of anything else
00:09:56 <alise> also... it should be product not sum
00:12:15 <alise> maybe I should define a product operator
00:12:16 <alise> ∏ 0 → ε ⇒ λ i → (i!)⁻¹
00:13:10 <alise> euler = ℝ (λ ε → ∏ 0 → ε ⇒ λ i → (i!)⁻¹)
00:21:44 <alise> Incidentally, abs (x-y) deserves a better name than it possesses.
00:22:13 <alise> That's not an operator, it's a function.
00:23:11 <alise> For some reason I think it's actually a nicer operation than subtraction.
00:23:19 <alise> We're measuring, not doing some sort of thingy-bob operation.
00:25:35 <alise> oerjan: Seems that Epigram 2 does indeed have Mu, the Fix you quoted, as the primitive.
00:26:06 <alise> make nat := (Mu @ [`arg { zero, suc } [ (@ [`done]) (@ [`ind1 @ [`done]]) ] ] ) : * ;
00:26:07 <alise> make zero := @ [`zero] : nat ;
00:26:07 <alise> make suc := (\ x -> @ [`suc x]) : nat -> nat ;
00:26:07 <alise> make one := (suc zero) : nat ;
00:26:07 <alise> make two := (suc one) : nat ;
00:26:08 <alise> make plus := @ @ [(\ r r y -> y) (\ r -> @ \ h r y -> suc (h y))] : nat -> nat -> nat ;
00:26:08 <alise> make x := (plus two two) : nat
00:30:40 <alise> Seems yucky to me, though.
00:33:06 <alise> oerjan: how can that mu do paramaterisable types though
00:33:12 <alise> λA → (λT → data nil : T; cons : A → T → T)
00:33:19 <alise> er does that Mu show up for you?
00:33:26 <alise> after the first -> imagine an M
00:33:35 <alise> oh wait no unicode at all
00:33:53 <alise> \A -> M (\T -> data nil : T; cons : A -> T -> T)
00:34:31 <oerjan> so you answered your own question?
00:34:53 <alise> \A -> M (\T -> (data nil : T) && (data cons : A -> T -> T))
00:35:00 <alise> where && = Either = union = and
00:35:43 <alise> (data nil : T) ≈ 1
00:35:53 <alise> \A -> M (\T -> Unit && (data cons : A -> T -> T))
00:36:05 <alise> so how to reduce the cons, I wonder
00:36:21 <alise> also, my issue with these kinds of shenanigans is that the implementation gets exposed
00:36:26 <alise> () : List, which isn't cool
00:37:25 <alise> 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 <alise> of course all this Muery doesn't help us write nice notation...
00:38:15 <alise> which is my whole goal :P
00:39:06 <oerjan> predicted return to specialized notation in 1,2 ...
00:39:17 -!- bsmntbombdood has joined.
00:40:17 <alise> oerjan: you're saying I'll never go back?
00:40:38 <alise> but seriously why are the T and ... in the same definition in data X : T where ...
00:40:42 <alise> it makes no sense!
00:41:50 <alise> 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:43:33 <alise> I'm tired, so I'll sleep now.
00:43:41 <alise> 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 <uorygl> Hmm, still nobody has sent me the esoteric-priv stuff.
01:25:54 <benuphoenix> 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 <oerjan> benuphoenix: no. c++ is banned here. *ducks*
01:31:49 * oerjan doesn't know c++ anyhow
01:32:34 <oerjan> 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 <pikhq> benuphoenix: No, we write crazier C++.
01:34:22 <pikhq> Well, crazier C, actually.
01:34:54 <pikhq> 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 <uorygl> Translate into Haskell please.
01:35:56 <benuphoenix> that's the craziest i can quickly think of that fits on one line.
01:36:46 <pikhq> uorygl: The equivalent Haskell for benuphoenix's program is: main = undefined
01:37:07 <pikhq> (well, strictly speaking his is the "infinite loop" sort of bottom, but hey.)
01:37:39 <pikhq> No, GHC complains about that.
01:38:11 <pikhq> main = return $ length [1..] -- This is *actually* an infinite loop. :)
01:38:24 <pikhq> Erm. Wait, no, that won't be eval'd.
01:38:38 -!- Asztal has quit (Ping timeout: 258 seconds).
01:38:44 <pikhq> main = return $ length [1..] `seq` ()
01:38:52 -!- Asztal has joined.
01:39:10 <Sgeo> Hi benuphoenix
01:40:37 <benuphoenix> am i the only one who uses irssi in windows instead of xchat?
01:40:38 <oerjan> !haskell import System; main = System.exit . flip seq 0 . all (<1) $ iterate (succ.pred) 0
01:41:00 <Sgeo> I think uorygl SSHes in to normish from which he uses irssi
01:41:31 <Sgeo> pikhq, on Cygwin apparently
01:41:34 <oerjan> !haskell main = flip seq 0 . all (<1) $ iterate (succ.pred) 0
01:42:16 <benuphoenix> there's a win32 binary version on irssi.org
01:42:21 <oerjan> !haskell main = flip seq (return 0) . all (<1) $ iterate (succ.pred) 0
01:43:03 <pikhq> Might I suggest (`seq`return 0) instead of flip seq (return 0)?
01:44:02 <oerjan> hm that last one got no response. maybe that meant it actually _did_ compile.
01:45:33 <oerjan> actually, does ghc use main's result for exiting if it is an Int?
01:45:46 <oerjan> might need that System function after all
01:45:49 <benuphoenix> c/c++: int main{for(;;);} might be infinite. i only speak c++ and basic
01:47:06 <uorygl> Sgeo: currently, I SSH into sine.aftran.com from which I use irssi.
01:47:34 -!- Asztal has quit (Ping timeout: 265 seconds).
01:47:39 <oerjan> !haskell import System; main = exitWith . flip seq 0 . all (<1) $ iterate (succ.pred) 0
01:47:45 <uorygl> Hey, you know that sine.aftran.com is not the location of our chatting.
01:47:53 <uorygl> I left out the port number and channel name.
01:48:06 <oerjan> !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 <Sgeo> http://www.stationv3.com/d/20050131.html
01:49:41 -!- cal153 has joined.
01:51:47 <oerjan> pikhq: i said you may suggest it, not that i would listen
01:52:33 <benuphoenix> i got "main(){for(;;);}" to compile and run infinite.
01:53:11 <oerjan> well it hasn't complained yet
01:53:36 <pikhq> benuphoenix: Well, yeah...
01:53:43 <EgoBot> help: General commands: !help, !info, !bf_txtgen. See also !help languages, !help userinterps. You can get help on some commands by typing !help <command>.
01:53:52 <EgoBot> 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:20 <pikhq> !c main(){main();}
01:54:22 <EgoBot> ./interps/gcccomp/gcccomp: line 52: 29844 Segmentation fault /tmp/compiled.$$
01:54:49 <pikhq> *Real* compilers TCO.
01:55:49 <pikhq> Tail-call optimisation.
01:56:14 <Sgeo> Python doesn't do that, for some reason
01:56:24 <pikhq> A tail call can be optimised to a jmp fairly easily.
01:56:27 <Sgeo> I remember reading about someone arguing that that's correct, and it shouldn't
01:57:22 <pikhq> At a *bare* minimum it should offer a way of explicitly doing a tail call.
01:57:32 <pikhq> (something like Perl's "goto &func;")
01:57:46 <pikhq> "goto &func(args);"
01:58:46 -!- Azstal has joined.
01:58:47 <pikhq> (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 <benuphoenix> running main(){main();} after [c++] compiling successfully segmetation-faulted after 1.49 seconds
02:00:37 -!- Asztal has quit (Ping timeout: 265 seconds).
02:00:39 <oerjan> c++. for high-speed crashing.
02:01:39 <Sgeo> I take it C++ doesn't TCO either
02:02:11 <coppro> Depends on your compiler
02:02:23 <coppro> I'm surprised that even compiles; main is not supposed to be callable
02:04:24 <coppro> 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:27 <coppro> nah, you can make infinite loops all sorts of other ways
02:06:59 <benuphoenix> s/infinite loops/recursive function calls/
02:07:07 -!- Azstal has quit (Ping timeout: 265 seconds).
02:07:47 <coppro> you can go infinitely recursive with any other function
02:08:52 <oerjan> you can infinitely loop while choosing how to infinitely loop!
02:10:02 <benuphoenix> running main(){main();} gave me a 67 meg core dump
02:11:20 <pikhq> coppro: GCC doesn't stick any initialization into main.
02:11:27 <pikhq> coppro: The entry point is _start.
02:11:40 <pikhq> coppro: _start initialises things and then calls main.
02:11:51 <coppro> pikhq: yes, but that doesn't change the standard
02:12:01 <coppro> calling main is still illegal
02:12:14 <pikhq> GCC does many things that are illegal.
02:13:24 <benuphoenix> allowing "main(){...}" when it should only be "int main(){...}"
02:14:02 <pikhq> In C89, the "int" is implied.
02:15:55 <Gregor> I'm pretty sure that's still legal in C99, although stupid :)
02:16:32 <Gregor> Anyway, I'm sure -Wall -Werror -ansi -pedantic would complain.
02:16:33 <pikhq> Oh, right. C99 allows it for functions.
02:16:42 <pikhq> It's banned for variables.
02:16:47 <pikhq> Gregor: -std=c99 makes it warn.
02:16:55 <pikhq> It's deprecated but allowed.
02:17:10 <pikhq> I know I've gotten warning.
02:17:35 <Sgeo> C99 apparently lets you do int a[b]; when b isn't a const?
02:17:36 <Gregor> Warning != illegal. gcc also warns if you use gets()
02:17:42 * Sgeo is somewhat scared
02:17:47 <Gregor> In fact, gcc warns if you use gets() even if you specify -w (no warnings) :P
02:18:09 <Gregor> Sgeo: You could approximate that with alloca anyway
02:18:12 <pikhq> Sgeo: Yeah, works just fine.
02:18:19 <pikhq> The array gets allocated on the stack.
02:18:38 <pikhq> And gets cleaned up when it goes out of scope.
02:18:53 <pikhq> (by "cleaned up", we of course mean "popped".)
02:19:06 <Gregor> (IIRC, alloca is not part of any standard, but is basically implemented by everyone)
02:19:30 <pikhq> Yeah, alloca is pretty common.
02:20:13 <Sgeo> Is benuphoenix doing C or C++?
02:20:32 <Gregor> This function is not in POSIX.1-2001.
02:20:32 <pikhq> No, no it's not. I thought it was.
02:20:50 <pikhq> It's just been around since at least 3BSD.
02:21:32 <benuphoenix> even when it's identical to c, i still use c++
02:21:58 <pikhq> benuphoenix: That's dumb.
02:23:19 <benuphoenix> actually, i rarely write something in c++ that doesn't use iostream
02:24:25 <pikhq> C++'s IO is one of the more stupid features.
02:24:45 <pikhq> (seriously, IO via bitshift?)
02:26:31 <pikhq> They're bitshift operators.
02:26:54 <pikhq> That your bitshift operator isn't *shifting* any *bits* doesn't make them cease to be bitshift operators.
02:28:08 <Sgeo> It is somewhat ugly, but is that that big a tragedy?
02:28:10 <benuphoenix> pikhq: i know what the bitshift operaters are and what they are supposed to do
02:28:51 <pikhq> Sgeo: That's but one of the poor things about C++'s IO.
02:28:55 <Gregor> It shifts bits from memory into IO :P
02:29:03 <pikhq> This is merely a poor *aesthetic* choice.
02:29:55 <Sgeo> Paging coppro to #esoteric . coppro to #esoteric
02:30:35 <pikhq> 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 <pikhq> 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 <pikhq> Also, Iostreams make i18n a royal *pain*.
02:31:31 <pikhq> In C, you would wrap the format string in a function that looks up the translation for the string.
02:31:42 <pikhq> In C++... You use printf if you want to do that.
02:32:06 <pikhq> (or GNU's asprintf, which is a printf that *works on iostreams*. Thus obviating everything different about them.)
02:32:09 <Sgeo> Surely you can retrieve the flags somehow?
02:32:47 <Sgeo> cin.something? There's no something? Or something()?
02:33:01 <pikhq> Also, why in the world does endl exist? I could understand if it actually used the system end of line character.
02:33:14 <pikhq> But it *doesn't*. It just outputs \n and flushes the iostream.
02:33:21 <pikhq> So. Fekking. *Stupid*.
02:33:37 <Sgeo> coppro, read the C++ criticism. You're a C++ defender person, iirc?
02:33:44 <coppro> oh, I don't defend IOstreams
02:34:24 <Gregor> ... C++ vs C arguments. Seriously? Argh.
02:34:26 <coppro> the overarching concept (easily extensible streams) is good, and that's about it
02:34:54 <pikhq> Gregor: Hey, we have to do one of these every now and then.
02:36:58 <benuphoenix> true or false: iostreams are useful when the professors want to see them in the code?
02:39:19 <benuphoenix> what are the c stdio equivlents of the c++ iostream functions "cin.get()" and "cout.put()"?
02:40:03 <pikhq> What's the type of get and put again?
02:41:15 <coppro> or something like that
02:41:21 <pikhq> benuphoenix: Which get?
02:41:29 <coppro> pikhq: the one that gets the next character
02:41:48 <pikhq> Ah, the "int get()" one.
02:42:48 <pikhq> Yeah, "int getchar(void)" and "int putchar(int)" are the functions.
02:46:51 <Sgeo> Everyone who needs to breathe has thirty seconds to get off the station.
02:48:48 <Sgeo> 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 <augur> who wants to dick around with an experiment in flight control for my video game? :D
05:10:48 <Sgeo> 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 <uorygl> `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 <HackEgo> Resquiat in fish, pesto, and four cheeses.
06:37:08 <augur> uorygl: what are you trying to do lol
06:37:11 <uorygl> `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 <HackEgo> SEA; resquiat in fish, pesto, and four cheeses.
06:37:21 <uorygl> I'm trying to translate that.
06:37:27 <augur> whats to translate
06:37:31 <augur> theyre names of foods
06:38:12 <uorygl> How about the "al forno" and the "resquiat" parts?
06:38:55 <augur> oh who knows im not italian
06:40:16 <uorygl> 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 <fizzie> 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 <ehird> March. 'Tis verily March.
11:15:58 <ehird> 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 <ehird> 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 <ehird> 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:31 -!- ehird has changed nick to alise.
11:19:33 <alise> Gotta fix that default.
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 <alise> Never used Unity. 3D is hard; let's go shopping.
11:20:46 <alise> Write it in my language!
11:20:48 <alise> It'll be dependent.
11:20:58 <alise> MONOIDAL RENDERING
11:26:45 <alise> 18:33:37 <Sgeo> coppro, read the C++ criticism. You're a C++ defender person, iirc?
11:26:45 <alise> 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:48:13 <scarf> sorry, haven't been doing too much esoprogramming recently, unless you consider Java eso
11:48:50 <scarf> one of the things which comes with a job is not always being able to choose which language you write in
11:48:58 <alise> that's alright, I haven't been either
11:49:16 <alise> well, then again, I guess you could consider my language eso
11:49:25 <scarf> <student> so you're saying that Java is a good language know if you want a job? <ais523> well, it got /me/ a job
11:50:03 <alise> :( 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 <alise> that would have been fun!
11:50:24 <alise> I may be the most cynical person about programming jobs who has /never had a programming job/
11:50:25 <scarf> heh, well my job is teaching it to students
11:50:35 <scarf> so I don't have the sort of over-enterprisiness issues
11:50:44 <scarf> just, my heart sinking at people confusing classes and methods
11:50:51 <alise> yeah but it's basically like teaching applied satanism :P
11:50:58 <alise> you can do it but... why
11:51:16 <scarf> improving the average quality of Java programmers can only be a good thing, surely?
11:51:30 <alise> anyway, have the computable reals:
11:51:32 <alise> data ℝ : Set where
11:51:32 <alise> → {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂}
11:52:13 <scarf> yay, Unicode support
11:52:24 <scarf> I think any language with a syntax like that is necessarily eso, including APL
11:52:32 <scarf> also, http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=380731#15 (found via reddit) makes me amused
11:52:34 <alise> Support? I'm afraid I'm going to shift your opinion now; it's not optional.
11:52:57 <alise> scarf: that bug report really irritates me
11:53:08 <alise> i am god, accept my holy package judgements
11:53:21 <scarf> alise: it confuses me, but I'm not sure why I'm confused and get even more confused as a result
11:53:49 <scarf> alise: do you consider support for the astral planes also necessary?
11:53:53 <alise> I really like the definition of computable reals
11:54:09 <alise> scarf: Well, it's only "required" insofar as the basic syntax and stdlib use it :P
11:54:31 <alise> Or, wait, does any of the actual syntax use it? The arrow is defined in the stdlib, albeit as a primitive
11:54:36 <scarf> I thought you meant that Unicode support was necessary for everything, and ended up agreeing with you
11:54:39 <alise> Oh, of course, lambda
11:54:55 <alise> scarf: Well, that too of course
11:54:58 <alise> Aastral Plane is nice also
11:55:06 <scarf> in derl (my underlambda/underload interp), all I/O is in UTF-8, and it uses UTF-32 internally
11:55:27 <scarf> hmm, I don't think I've ever seen the Unicode version of the astral planes written with a capital letter
11:55:36 <alise> God I love dependently-typed languages
11:55:39 <scarf> and there are 16 of them
11:55:42 <alise> Induction on the naturals as a recursion combinator?
11:56:25 <scarf> 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 <alise> It's not sort-of, that's exactly what it is.
11:56:47 <scarf> where types are parametrized by the number of times you're allowed to use a value of that type ever
11:57:01 <alise> The normal typed lambda calculus is types indexing on types, and values indexing on values.
11:57:06 <alise> With typeclasses, we have values indexing on types.
11:57:11 <alise> Dependent types give us types indexing on values.
11:57:18 <alise> Or, wait, typeclasses don't /quite/ do that.
11:57:33 <alise> Dependently-typed languages usually have types as first-class values, too, so we get values-indexing-on-types for free.
11:58:55 <scarf> one thing I've been thinking about recently is designing my own VCS
11:59:05 <alise> I like how the (intensional) Axiom of Choice is in fact provable in intuitionistic type theory and thus most dependent langs.
11:59:10 <scarf> I think I found a paradigm general enough to contain both git's model and darcs's model as special cases
11:59:16 <alise> Wonder if it is in Observational Type Theory (the underpinning of Epigram 2)?
11:59:23 <scarf> alise: ooh, the axiom of choice
11:59:29 <alise> (Not the extensional axiom of choice, though.)
11:59:37 <alise> Extensional is the one that lets you do things like order the real numbers.
11:59:46 <alise> http://r6.ca/blog/20050604T143800Z.html
11:59:48 <scarf> 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 <alise> You can have one without the other.
12:00:54 <alise> *intensional not intuitionistic
12:01:05 <scarf> the intensional one is the one that's normally stated as the axiom, at least here
12:01:32 <scarf> but then, we're normally dealing with sets, where the existence of quotients is taken for granted
12:01:38 <scarf> so they probably come out equivalent there
12:02:02 <alise> yes it's causing me a bit of a crisis as I like quotient types
12:02:25 <alise> and Observational Type Theory which has a really nice definition of equality has tem
12:02:33 <scarf> also, that first link is a data: link
12:02:38 <alise> but surely it cannot have extensional choice?
12:02:44 <alise> otherwise it'd have excluded middle
12:02:59 <scarf> although it doesn't load in my browser
12:03:01 <alise> and you cannot give a value of either p or p -> Void for every type p...
12:03:09 <alise> scarf: he does tat a lot
12:03:15 <alise> it's like footnotes but awesome
12:03:26 <scarf> hmm, I wonder why it isn't working? loading it just gives me a blank page
12:03:29 <alise> his blog http://r6.ca/blog/ is very cool
12:05:22 <alise> http://r6.ca/blog/20091101T231201Z.html man I haven't read this before
12:06:28 <scarf> hmm, loads in Epiphany
12:07:17 <fizzie> 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:35 -!- Gracenotes has quit (Quit: Leaving).
12:08:09 <fizzie> 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 <scarf> fizzie: ah, let me try that in FF
12:08:37 <scarf> fizzie: yep, same results
12:08:54 <scarf> that /is/ a weird bug, I wonder if it's an FF bug or an extension bug?
12:09:10 <alise> so, guys, what's your favourite definition symbol?
12:10:43 <fizzie> I like that snowman guy.
12:12:33 <scarf> alise: = with a little word "def" over it is normally used when writing proofs here
12:12:45 <scarf> I'm not sure how much I like it, but it's at least unambiguous
12:12:45 <alise> Yes, but you need a huge font size for that to be readable.
12:13:01 <scarf> also, there's something very nicely pure about a language that can get away with using = for defined-equal
12:13:03 <alise> Plus, it is ugly; we rarely use words in mathematics, preferring symbols (including alphanumeric ones).
12:13:03 <fizzie> ≔ is nice, though in this font even that's just a = that has some sort of blobby things on the left end.
12:13:19 <alise> Overlaying an English abbreviation on top of a very common symbol is just silly/
12:13:33 <scarf> it's visible as a :=-alike to me
12:13:37 <alise> scarf: It isn't pure, though, because that's not really what it means.
12:13:37 <fizzie> It's still better-looking than the ≝ though.
12:13:38 <scarf> with less space between the : and hte =
12:13:47 <fizzie> I mean, that one's just a = with a larger smudge above.
12:13:48 <scarf> fizzie: ugh, that's awful
12:13:53 <alise> At the very least it should be ≡.
12:14:02 <alise> Definitional equality, propositional equality, ...
12:14:07 <scarf> if I zoom right in, I can see the word def
12:14:13 <alise> Spam, spam, equality and spam...
12:14:16 <scarf> that's zooming via super-mousewheel, not by making the font bigger
12:14:41 <scarf> you don't realise how much you were missing super-mousewheel until you get a system where it works
12:14:55 <alise> ctrl-mousewheell in os x.
12:14:57 <alise> I have no mousewheel, though
12:15:00 <scarf> and ≡ to me implies congruence rather than definition
12:15:11 <alise> Er, right, definitional equality is =.
12:15:16 <scarf> super-mousewheel works via the touchpad here
12:15:25 <alise> ≡ is propositional.
12:15:29 <alise> scarf: No mouse at all
12:15:37 <scarf> alise: heh, you remind me of me
12:15:53 <scarf> the mouse I have at the moment is basically broken, I need a new one / to stop using the mouse again
12:16:02 <scarf> I mostly only use it for Enigma, NetBeans, and websurfing as it is
12:16:12 <scarf> (NetBeans because it doesn't respond to keyboard shortcuts in a sane manner)
12:16:30 <alise> I have a mouse just no radio receiving thing for it.
12:16:48 <alise> 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 <alise> Should be resolved by today with the amazing solution of "purchasing a mouse" :P
12:17:07 <scarf> (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 <scarf> haha: http://www.robweir.com/blog/2010/02/microsoft-random-browser-ballot.html
12:19:21 <scarf> summary: Microsoft messed up the code for randomizing the order of browsers in their ballot thing
12:19:26 <scarf> so not all the combinations have equal probabilities
12:20:52 <alise> http://www.browserchoice.eu/BrowserChoice/browserchoice_en.htm
12:20:57 <alise> What the fuck is a "green" browser?
12:22:10 * scarf follows the tell me more link
12:22:18 <scarf> I bet they claim to be environmentally friendly, or something
12:22:39 <scarf> wow, the PNG image on their home page is taking around 10 seconds to load
12:22:39 <alise> I thought that too but it doesn't seem so
12:22:46 <scarf> I don't think I've seen an image load that slowly for months
12:22:50 <alise> I like how there's like a few decent browsers and then holy shit obscureathons
12:22:57 <scarf> 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 <scarf> after guessing it was a goatse
12:23:08 <scarf> so I've seen the top 20 pixels or so of goatse, but no more
12:23:57 <scarf> http://www.morequick.com/IndexEn.htm <--- wow that's a bad homepage
12:24:41 <alise> looks like it uses IE's engine
12:24:47 <alise> see bottom left of screenshot
12:25:16 <scarf> heh, that's the IE logo, you're right
12:25:40 <alise> yeah like Maxthon and shit they're all the same
12:25:44 <alise> take IE engine add shitty UI with tabs done
12:25:50 <scarf> how can a website called morequick.com load so slowly?
12:26:19 <scarf> 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 <scarf> just because I'm curious as to what will happen
12:27:25 <scarf> oh, I get an advert for Windows 7
12:27:28 <scarf> that's actually sort-of clever
12:27:34 <scarf> "Internet Explorer 8 is available only on PCs running Windows. Check out Windows 7, which includes Internet Explorer 8."
12:29:37 <scarf> 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 <alise> http://www.flickr.com/photos/38864566@N00/2479491895/
12:31:52 <scarf> ugh, not a still image?
12:31:56 <scarf> I may have a look when I get home
12:32:09 <alise> It couldn't be a still image
12:45:52 <alise> I have this sinking feeling that I should do pattern matching on arbitrary function results.
12:45:59 <alise> (as opposed to just constructors)
12:46:43 <alise> *just constructors
12:47:31 <scarf> pattern matching reminds me of the old joke about regexes ("now you have /two/ problems")
12:47:47 <scarf> or maybe the statement about XML being like violence
12:48:02 <scarf> 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 <alise> 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 <alise> daef: Are you dæf?
13:06:56 <alise> Or just deaf /and/ dyslexic?
13:08:07 <scarf> hmm, I tried /nick æis523 but Freenode wouldn't let me
13:08:31 <alise> Er, isn't it pronounced ay eye ess?
13:08:43 <scarf> it would be a different word if it were æis523
13:08:58 <scarf> sort of like "oklopol" is not pronounced the same way as "oklofok"
13:09:29 <daef> dyslexics are teople poo
13:09:34 <alise> daef: Oh, cute, you're one end of a TCP socket!
13:09:40 <fizzie> scarf: nickname = ( letter / special ) *8( letter / digit / special / "-" )
13:10:03 <scarf> fizzie: wow, I'm... amazed and happy that you actually looked that up
13:10:15 <alise> fizzie: So what nick does -i use on IRC?
13:10:17 <scarf> and just as happy but more amazed if you typed it from memoryt
13:10:30 <alise> He looks everything up :)
13:10:39 <alise> He is an unstoppable Google machine
13:10:44 <fizzie> scarf: Sorry to deamaze you a bit; it was looked-up. Looking things up is pretty much what I do.
13:10:52 <fizzie> It was from a local file this time, though.
13:11:11 <fizzie> (Is "deamaze" a word?)
13:11:18 <alise> fizzie is just a gigantic lookup table
13:11:24 <daef> alise: i'm david => dave => daef
13:11:36 <alise> Eliezer Yudkowsky isn't sure whether you're conscious, fizzie.
13:11:44 <alise> daef: Oh shush you.
13:11:51 <alise> I'm allowed to be ridiculous if I feel like it.
13:11:58 <fizzie> alise: I'm not sure of that either; I can't seem to find any good results for it in Google.
13:12:37 <alise> You didn't find http://lesswrong.com/lw/pa/gazp_vs_glut/?
13:12:53 <alise> He concludes you're not conscious. Ha!
13:13:00 <alise> I have foiled you, GLUT!
13:13:17 <alise> Is it Schadenfreude if the other party isn't conscious?
13:14:12 <fizzie> 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:44 <daef> alise: do you speak german?
13:14:57 <scarf> 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 <alise> daef: No, but Schadenfreude is an authentic English word, high-quality import.
13:15:06 <alise> Hardly any scratches on the disk. Only slightly pirated.
13:15:44 <scarf> btw, the "gazp vs glut" thing confuses me, I couldn't get why you'd compare anything but SDL to GLUT
13:15:48 <scarf> but it seems to be a different GLUT
13:16:08 <scarf> alise: you can have fun guessing what that list is, btw
13:16:15 <scarf> as can the rest of #esoteric
13:16:28 <scarf> although, it's likely to be distinctive enough that Google would turn it up pretty quickly
13:16:59 <alise> scarf: GLUT = Giant Look-Up Table
13:17:06 <scarf> yep, got that from the page
13:17:07 <alise> GAZP = Generalised Anti-(P-)Zombie Principle
13:17:17 <scarf> I was thinking GLUT = GL Utility Toolkit
13:18:19 <scarf> you can see how confusing that acronym mismatch would make the page title
13:18:43 <alise> But is a cube... CONSCIOUS????
13:19:00 <scarf> alise: as it's GLUT, the question would work better with teapots
13:19:09 <alise> I was trying to remember that shape
13:19:24 <daef> scarf: anyway - it's just a bunch of triangles
13:19:45 <scarf> 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 <daef> that you could also save in a giant lookup table
13:23:12 <alise> If the Utah Teapot is conscious, is it a Mormon?
13:24:35 <scarf> alise: assuming that's an indicative rather than subjunctive if, yes
13:24:41 <scarf> *rather than counterfactual
13:25:08 <alise> Prove that it isn't conscious, you nincompoop! :P
13:25:38 <alise> also, subjunctive is a perfectly acceptable term isn't it?
13:27:24 <alise> 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 <alise> trust Eliezer Yudkowsky to remark on how immoral creating a lookup table can be
13:27:55 <alise> Which leads me on to my next question: IS MULTIPLICATION CONSCIOUS????
13:29:18 <scarf> what's confusing me here is computational complexity
13:29:48 <scarf> 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 <alise> Oh, it would surely be ridiculous.
13:30:05 <alise> We have such a small universe.
13:30:48 <scarf> gah, why can't you upvote IRC comments?
13:31:14 <alise> Oh, it would surely be ridiculous. [↑ 1 ↓]
13:31:16 <alise> We have such a small universe. [↑ 1 ↓]
13:32:05 <scarf> hmm, this seems like a perfect feature for ickirc
13:32:33 <scarf> 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 <scarf> and ofc you'd use CTCP
13:32:37 <alise> ^AUPVOTE messageid^A
13:43:08 <scarf> also, http://forums.thedailywtf.com/forums/t/15838.aspx is golden
13:43:30 <scarf> 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 <scarf> it's not the only ridiculousness found in the code, it seems
13:43:50 <scarf> and the code itself was taken from a JS tutorial written by someone unrelated
13:43:55 <alise> which person puhsing it most? I am confused
13:44:16 <scarf> his name is Stephen Conroy, but that doesn't seem particularly relevant
13:44:28 <scarf> umm, the minister pushing it, that is
13:45:07 <alise> I just couldn't parse your sentence; got it now
13:45:25 <alise> uk i'net is censored too :/ just not as badly
13:45:56 <daef> alise: the fact is bad enough
13:46:10 <scarf> at least Phorm hasn't been switched on yet
13:46:14 <scarf> I have plans for if and when it is
13:46:29 <scarf> I have quite an idea of how it technically works, and it would be fun to mess around with it
13:47:10 <alise> Isn't its workings well-known?
13:47:19 <scarf> well, by people who care to find out
13:47:23 <scarf> I imagine it isn't well-known in general
13:47:29 <scarf> because most people haven't bothered to look it up
13:47:30 <alise> Phorm seriously freaks me. It's, like, not even your regular Orwellian evil under a corporate disguise.
13:47:43 <alise> It's a paper company: something you would expect to see in fiction, down to the logo, website, everything.
13:47:53 <scarf> we can try things like creating websites where every link goes through exactly 4 HTTP redirects
13:48:03 <alise> It's like there is no cover over it other than the ludicrously unbelievable.
13:48:06 <scarf> which complies with the RFC without Phorm, but fails to comply with it with
13:48:29 <scarf> alise: because it uses redirects on every page view itself
13:48:38 <scarf> and it goes over the redirect-loop limit if you combine the two
13:48:54 <alise> So would a Phorm-condemned user actually see a redirect on every request?
13:49:04 <scarf> even if you turn it off, apparently
13:49:07 <alise> Hey, lets the ISPs up all their connection speeds and prices.
13:49:13 <scarf> because the redirect's needed to tell whether it's turned off or not
13:49:18 <alise> Meet the new speed, same as the old speed.
13:49:22 <alise> Actually, why the hell isn't Phorm illegal?
13:49:37 <alise> Wow, Phorm apparently used to (under a different name) produce spyware.
13:49:39 <scarf> 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 <alise> I didn't even know that.
13:49:46 <alise> (As in, real bona fide non-approved spyware.)
13:50:21 <alise> 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 <scarf> more fun: phorm impersonates websites to inject cookies into them
13:50:25 <scarf> I can't remember why, btw
13:50:30 <alise> What is it with UK government positions' names and sounding creepy?
13:50:33 <alise> Information Commissioner.
13:51:01 <scarf> 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 <alise> Do they want people to read Wikipedia without the Wikipedia branding in the future or something? :P
13:51:24 <alise> It's awkward to read.
13:51:26 <scarf> alise: there's a page about that
13:51:33 <scarf> http://en.wikipedia.org/wiki/Special:Search?go=Go&search=WP:ASR
13:51:38 <alise> But I think the "neutrality" just makes the writing feel strange.
13:51:58 <scarf> the idea's that the articles should have no idea that they're on Wikipedia, or indeed even on a website
13:52:08 <scarf> so, say, you can make print versions more easily, and fork it more easily
13:53:19 <alise> Print can still say Wikipedia. Okay, forking, granted.
13:53:40 <alise> Is forking more important than not confusing people who read it?
13:53:50 <alise> My brain does a bit of a double take every time Wikipedia says "the online encyclopedia Wikipedia".
13:55:26 <alise> 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 <alise> At home, at least.
13:55:54 <scarf> 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 <alise> Yeah, but what about all my kiddie porn?!?!?!?!
13:56:27 <scarf> alise: I hope you don't view that sort of thing
13:56:29 <alise> Anyway I draw the line at every single HTTP request causing a redirect.
13:56:41 <alise> scarf: Must you take obvious ridiculosity as sincere?
13:57:05 <scarf> alise: well, at least I'm consistent
13:57:14 <scarf> and it sometimes produces absurd conversations, which can only be a good thing
13:57:18 <alise> scarf: Then you are not complete.
13:57:32 <scarf> alise: I'm not even a type 1 reasoner
13:58:22 <scarf> whether it's possible to be simultaneously consistent and complete depends on your other assumptinos
13:58:42 <alise> Well, I based it on the fact that you said you were consistent.
13:58:52 <alise> Presumably that means you've proved to yourself that you're consistent :P
13:59:21 <scarf> 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 <scarf> actually, I believe myself to be inconsistent in general
14:00:58 <alise> 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 <alise> (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 <scarf> 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 <scarf> but I can't find one
14:02:19 <scarf> maybe it was just a typo?
14:04:12 <scarf> <Xyro> FYI, the world will end on Tue, August 31st, 4500AD a few minutes before midnight (local time).
14:04:55 <scarf> this is a crazy and nonserious attempt to deduce a religion from Microsoft Outlook
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 <scarf> with a cable meant for analog, you can sort-of see how people could be fooled into it, but digital?
14:08:25 <Deewiant> People don't know how technology works
14:08:54 <scarf> "if you do not follow the "directional markings" on the cables, your music will play backwards. Please check that."
14:09:02 <scarf> people found the website and started giving parody reviews
14:10:03 -!- MissPiggy has joined.
14:11:10 <alise> back, with a new keyboard and mouse
14:11:37 <scarf> where did you get them from?
14:12:17 <alise> 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 <alise> (I already had them, I was just plugging them in and what not.)
14:13:29 <alise> This keyboard could do with some weights to hold it into place.
14:13:35 <alise> The mouse isn't bad, though.
14:13:51 <alise> Not rubbery, sufficiently clicky buttons, and a scroll-wheel.
14:14:09 <scarf> alise: I love the mental image of a keyboard blowing away in the wind
14:14:15 <MissPiggy> I am so fucking ill I want to puke
14:14:21 <alise> MissPiggy: Then puke.
14:14:39 <alise> Those fold-up keyboards might be able to do that.
14:15:17 <alise> Ugh, I miss my media keys. (Just for volume control.)
14:16:22 <scarf> alise: same here, although I bound them to super-combinations
14:16:23 <alise> But damn I'm glad I have a mouse.
14:16:29 <scarf> in particular, I used to use play/pause a lot, now I use super-P
14:17:07 <alise> Rubber dome keyboards sure are mushy compared to the old scissor-switch.
14:17:15 <alise> But at least I don't have to fingernail keys I picked off now.
14:17:47 <alise> Irritating that Emacs cannot display characters I know I have the fonts for.
14:17:53 <alise> Even in those fonts.
14:18:13 <alise> For instance, ⊤ and ⊥ won't show, even with DejaVu Sans Mono.
14:18:46 <alise> It worked before in Ubuntu.
14:19:01 <scarf> alise: which OS are you using atm?
14:19:20 <alise> 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 <scarf> (/ctcp version is so much faster than asking a person)
14:19:36 <alise> I have Ubuntu here, though. I could boot it up and use it now that I have a mouse.
14:19:46 <alise> But Linux on Macs is iffy at the best of times.
14:20:46 <alise> Besides, it seems to work alright in other OS X applications.
14:20:56 <alise> Bloody Emacs. Maybe a newer build would work.
14:21:33 <alise> I'd just use TextEdit, but I need \TeX-style-character-insertion.
14:21:38 -!- BeholdMyGlory has joined.
14:23:19 <alise> 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 <alise> Well, agda-input, that is.
14:24:56 <alise> "David Cameron: We are a modern and radical Conservative Party" —YouTube front page
14:25:02 <alise> Radical conservatism!
14:27:00 <alise> epigram is so cool
14:28:16 <alise> I haven't looked into it.
14:30:45 <alise> 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 <alise> Ωmega is strict (Hugs is lazy);
14:30:45 <alise> Support for Generalized Algebraic Datatypes;
14:30:45 <alise> Ability to introduce new types;
14:30:45 <alise> Allows writing of functions at the type level.
14:30:52 <alise> Doesn't sound particularly dependent to me.
14:31:54 <alise> also, http://r6.ca/FewDigits/FPdag2008.pdf is officially my favourite introduction to dependent-types-as-logic ever
14:33:12 <alise> http://en.wikipedia.org/wiki/List_of_countries_by_coffee_consumption_per_capita
14:33:49 <alise> http://en.wikipedia.org/wiki/List_of_countries_by_alcohol_consumption
14:34:03 <alise> So what we can tell from this is that when Finns say "vodka" they mean "espresso".
14:36:09 <fizzie> 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:30 <alise> AnMaster: Uh, what makes you think that?
14:36:42 <alise> The current situation just means I'm sure as hell going to tackle this before even considering returning.
14:37:02 <alise> 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 <AnMaster> alise, hm? I mean back at home
14:37:11 <alise> Returning = to the unit
14:37:17 <alise> AnMaster: Oh you don't know the situation do you?
14:37:27 <alise> I'll explain briefly in /msg.
14:37:30 <AnMaster> I know what you mentioned before
14:37:49 <AnMaster> afterwards I will tell about my very strange journey home today
14:37:55 <AnMaster> very strange that thing with the bus
14:38:34 <alise> http://en.wikipedia.org/wiki/My_Neighbor_Totoro
14:38:41 <alise> Or, well, I guess http://en.wikipedia.org/wiki/Catbus is more specific.
14:39:16 <scarf> how can that possibly be not a lolcat reference?
14:39:35 <AnMaster> 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 <fizzie> There's also that single-person kittenbus, that's maybe even more... that.
14:39:41 <AnMaster> then I was to wait for another bus
14:39:52 <AnMaster> then something unusual happened
14:39:58 <alise> A very articulate bus.
14:40:04 <alise> AnMaster: You TURNED INTO A WALRUS?
14:41:05 <AnMaster> 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 <AnMaster> with the right bus number and everything
14:41:25 <fizzie> The SUSPENSE before you said that was INCREDIBLE.
14:42:10 <AnMaster> 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 <alise> This is so exciting I am literally urinating in my underwear
14:42:26 <AnMaster> and when I stepped out of the bus when I arrived, and looked back at the bus I was in
14:42:48 <AnMaster> all together I think this is rather strange
14:42:48 <fizzie> You just barely escaped a molestation affair thing, it seems!
14:43:15 <fizzie> Though perhaps a bus is maybe not the most inconspicuous vehicle for that sort of thing.
14:43:21 <AnMaster> fizzie, also the driver nearly made the wrong turn a bit before
14:43:36 <MissPiggy> 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:51 <MissPiggy> now every time I go on that bus I am scared it might do that again
14:43:59 <alise> clearly this problem would not exist if we had trams
14:44:06 <AnMaster> MissPiggy, maybe it is like here, same number takes different variants of the rout
14:44:07 <alise> the perfect vehicle for the transportation of yams
14:44:20 <fizzie> 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:45:03 <fizzie> There was something about there being more than one pair of steerable wheels in there.
14:45:04 <MissPiggy> there was a bit ofa fuss about them ni london because I think they can be a bit dangerous for cyclists
14:45:10 <MissPiggy> or maybe it was the other way around...
14:45:15 <alise> we should have buses that are entirely bendy
14:45:17 <AnMaster> like they go through small towns sometimes, and sometimes they go by the <what do you call big roads with a speed of 110 km/h in English? Separated directions, and all roads crossing it go by tunnel/bridge>
14:45:24 <alise> like, the whole bus is in the bendy bit
14:45:30 <fizzie> The catbus is very bendy, I believe.
14:45:44 <AnMaster> MissPiggy, well I'm used to this bus taking 5 different variants of the route
14:45:55 <AnMaster> MissPiggy, at least I live close to one of the points it take for allmost all routes
14:46:04 <alise> Wir fahr'n fahr'n fahr'n auf der Autobahn, wir fahr'n fahr'n fahr'n auf der Autobahn...
14:46:31 <AnMaster> 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 <AnMaster> usually it comes in from north, the exchange being the second station from that end of the route
14:47:20 <AnMaster> but this one came in from south with "not in traffic", made an U-turn, and changed to the right number
14:47:26 <alise> fizzie: Does that thing say METROBUS?
14:47:48 -!- oerjan has joined.
14:48:09 <AnMaster> 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 <fizzie> It seems to. The picture is non-local, though, just the same model of bus.
14:48:34 <alise> But I like that song.
14:48:54 <AnMaster> alise, anyway this long range bus even had a stoved away seat at the front saying "for guides" on a label
14:49:24 <AnMaster> 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 <AnMaster> (is under-dampened the right English term?)
14:49:41 <oerjan> <uorygl> How about the "al forno" and the "resquiat" parts?
14:50:02 * alise quells AnMaster's boring with the computable reals
14:50:04 <oerjan> resquiat means "rest" i think, see "resquiat in pace" (sp)
14:50:05 <alise> data ℝ : Set where
14:50:05 <alise> → {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂}
14:50:21 <fizzie> alise: http://isometric.sixsided.org/data/strips/the_left_sister/4.gif
14:50:25 <alise> requiescat in pace
14:50:35 <alise> AnMaster: mine. Similar to Agda, though, you could surely make the definition there.
14:50:41 <alise> Haskell is nowhere near powerful enough to express that.
14:51:39 <oerjan> http://en.wikipedia.org/wiki/Al_forno
14:51:43 <AnMaster> 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:16 <AnMaster> alise, then what does it mean? :)
14:52:30 <alise> A real is represented as a function from a positive rational to a rational. {{ε₁:ℚ⁺} → {ε₂:ℚ⁺} → abs (f ε₁ - f ε₂) ≤ ε₁ + ε₂} means:
14:52:50 <alise> For all positive rationals e1 and e2, |f e1 - f e2| <= e1 + e2
14:53:01 <oerjan> alise: resquiat is a late latin corruption, it seems. also, this was italian not latin.
14:53:04 <alise> Basically, pi 0.01 = 3.14
14:53:38 <alise> 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 <alise> AnMaster: Or similar.
14:54:12 <alise> just lets you convert a rational to a real.
14:54:21 <alise> For any precision, it yields the rational you give it.
14:54:36 <alise> 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 <AnMaster> 3.14159265... <-- what I remember of pi on the top of my head
14:54:44 <alise> Don't ask how it works. It's Magic.
14:55:09 <AnMaster> the next digit after that *might* be a 3, not sure
14:55:27 <fizzie> It's 3 unless you round it to that length.
14:55:46 <alise> MissPiggy: What, precisely, is the problem?
14:55:50 <fizzie> I think mooz bothered to memorize 50 or 100 digits or so. I'm not sure why.
14:56:06 <scarf> alise: I can do 3.14159265358
14:56:11 <oerjan> AnMaster: ...3589797... from my top of head
14:56:12 <alise> MissPiggy: Sucks to be you; I hate colds.
14:56:26 <alise> 3.14159 is as much as I know; I'm a dullard.
14:56:27 <MissPiggy> alise me too the worst thing is I had 100% attendence up until today
14:56:33 <oerjan> that last 7 shouldn't be there
14:56:49 <oerjan> (unless it's accidentally right)
14:56:50 <alise> 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 <alise> MissPiggy: cute, like oklopol
14:57:02 <MissPiggy> 3.141592653589793238462643383279502884197169399375105820974944592307816406286208
14:57:03 <AnMaster> alise, I have to think a few seconds to remember past 3.14159. It goes like "uuh... ah yes, 2 then 65"
14:57:08 <alise> angry that he got his first 4 instead of a 5 on a test :)
14:57:17 <alise> MissPiggy: Yeah. Right.
14:57:58 <alise> http://isometric.sixsided.org/data/strips/the_left_sister/19.gif
14:58:04 <AnMaster> <oerjan> AnMaster: ...3589797... from my top of head <-- checking gives that as "793" not "797" indeed
14:58:09 <AnMaster> but then that could be rounted
14:58:18 <alise> MissPiggy: I find it unlikely.
14:58:25 <alise> But I do not rule out the possibility entirely.
14:58:58 <AnMaster> M_PI has more precision in the header
14:58:58 <oerjan> AnMaster: hard to roung 3... to 7, alas :D
14:59:12 <oerjan> i am just chased by muphry's law today
14:59:13 <alise> http://isometric.sixsided.org/data/strips/the_left_sister/24.gif
14:59:18 <AnMaster> oerjan, unless it is very cold
14:59:35 <MissPiggy> alise all I know of phi is 1.618033989
14:59:54 <alise> Panels 28 onwards are missing, fizzie bot :(
14:59:55 <scarf> that forms a really memorable pattern
15:00:22 <fizzie> alise: I know, but my lookup table has gotten damaged and I cannot reconstruct them either.
15:00:32 <alise> ℝ (λ ε → product (map (λ i → (i!)⁻¹) (0 … ε)))
15:00:35 <alise> I've memorised all of e!
15:00:44 <alise> Or, if you prefer fancier notation,
15:00:57 <alise> ℝ (λ ε → ∏ 0 … ε ⇒ λi → (i!)⁻¹)
15:01:06 <AnMaster> well since it is transcendental, iirc every pattern of numbers will be found somewhere in it?
15:01:27 <oerjan> AnMaster: no, that isn't an implication
15:01:31 <AnMaster> or was that property even more specific than transcendental?
15:01:39 <scarf> that's more specific than transcendental
15:01:52 <oerjan> there are definitely transcendentals which are normal. iirc 0.101001000100001... is one
15:01:54 <scarf> the first proved-trancendental number had no digits in its decimal expansion than 0 and 1
15:01:57 <alise> http://en.wikipedia.org/wiki/Liouville_number
15:01:58 <oerjan> *which are _not_ normal
15:02:40 <AnMaster> so, did pi and e have that extra property or not? I don't remember
15:02:59 <AnMaster> the one mentioned just above -_-
15:03:00 <oerjan> 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:17 <oerjan> i _think_ all _known_ normal numbers are explicitly constructed to be so
15:03:42 <oerjan> MissPiggy: muphry is chasing me around today, i said
15:04:06 <AnMaster> oerjan, this isn't the first instance?
15:04:13 <AnMaster> MissPiggy, you have to be kidding
15:04:28 <scarf> MissPiggy: the law that all corrections of other people's typos or grammar mistakes themselves contain typos or grammar mistakes
15:04:34 <AnMaster> MissPiggy, http://en.wikipedia.org/wiki/Murphy%27s_law
15:04:48 <oerjan> MissPiggy: transcendental. actually maybe you need more 0's between
15:04:54 <scarf> AnMaster: that's the most ridiculous typo I've seen on this subject for a while
15:05:04 <alise> scarf: I expect AnMaster just had a gigantic whooooooooooosh
15:05:08 <alise> and honestly didn't get it
15:05:10 <AnMaster> alise, oh I didn't notice the extra r
15:05:13 <scarf> alise: lasting several months?
15:05:15 <scarf> AnMaster: doublefail
15:05:31 <oerjan> AnMaster: also, i missed a pi digit, and misspelled round
15:05:35 <alise> MissPiggy: fault? this is hilarious!
15:06:15 <AnMaster> what did the sparta thing... oh right "this is hilarious!"
15:06:31 <AnMaster> 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 <alise> i am a wonderful feminine creature!
15:07:06 <AnMaster> MissPiggy, what about "this is fun"...? does that also make you think of sparta?
15:07:49 <oerjan> scarf: i may be overextending muphry's law here, using it for any error involving mistyping
15:08:18 <fizzie> 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:32 <scarf> <Wikipedia> 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:41 <fizzie> oerjan: In any case MathWorld agrees with your assessment that currently known normal numbers are "artificially constructed".
15:08:46 <alise> "Most numbers that aren't pathological are probably normal"\
15:11:18 <MissPiggy> alise, opinison please http://www.reddit.com/r/programming/comments/b7neu/what_are_some_exciting_areas_for_computer_science/c0ldm41
15:11:23 <oerjan> 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 <alise> MissPiggy: did you write that or sth?
15:11:45 <alise> not sure what kind of opinion you want
15:11:51 <alise> MissPiggy: i refuse to apologise :)
15:12:39 <MissPiggy> [[Formal verification]] of computer programs.
15:12:45 <MissPiggy> 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 <alise> I know what it says.
15:13:20 <alise> well the terminology is a bit oversimplified
15:13:27 <alise> ...also i still don't get why you hate wikipedia
15:14:04 <alise> so you'd link to another source, even if it would be less helpful?
15:14:16 <AnMaster> <oerjan> 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 <alise> anyway nobody said dependent types so foo to that link
15:14:36 <MissPiggy> alise well the question is "What are some exciting areas for computer science related research?"
15:14:42 <alise> turns out he was talking english
15:15:12 <alise> 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 <AnMaster> alise, weird. A mathematican not using the shortest possible symbol to talk about math!?
15:15:14 <oerjan> AnMaster: i don't do unicode, so no
15:15:30 <alise> AnMaster: you realise that a lot of mathematics is done with words?
15:15:36 <alise> formally verified proofs aren't really the done thing
15:15:39 <alise> or even totally formal proofs
15:15:59 <MissPiggy> alise you totally missed the point :|
15:16:20 <AnMaster> alise, whooooooooooooooooooooooooooooooooooooooosh
15:16:25 -!- MigoMipo has joined.
15:17:16 <MissPiggy> the point is that linking to [[wikipedia]] every second word, like some kind of [[blogger]] is just completely unhelpful
15:17:21 <oerjan> impossible, AnMaster cannot whoosh anyone, fundamental physical law
15:17:25 <alise> AnMaster: a joke is only funny if it has some basis in fact
15:17:43 <AnMaster> alise, ever heard about stereotypes?
15:17:50 <alise> a joke based on a popular ignorance has to mock it to a large degree
15:18:02 <alise> rather than simply take it for granted and then following the usual "joke based on fact" process
15:18:15 <alise> i'm starting to wonder if perhaps swedish culture has no jokes at all
15:18:21 <AnMaster> ffs, just admit you missed the point.
15:19:04 <alise> "Just admit that you're wrong! I don't care if you're right, just concede once in a while!"
15:19:09 <alise> Yawn. Boring. Go away.
15:19:15 <MissPiggy> 15:17 < alise> i'm starting to wonder if perhaps swedish culture has no jokes at all
15:19:50 <alise> "My hovercraft is full of eels!" "You have a HOVERCRAFT? Why the fuck did you let eels into it? Jeez."
15:20:27 <scarf> alise: that's hilarious, and I don't know why
15:21:29 <alise> "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:16 <alise> "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:37 <scarf> gah, now I'm trying to remember, I actually looked it up
15:24:40 -!- alise has changed nick to ceiiinosssttuv.
15:27:11 -!- ceiiinosssttuv has changed nick to alise.
15:27:59 <oerjan> alise: swedish jokes mainly consist of taking norwegian jokes about swedes, and swapping the norwegian and swedish characters. hope this helps.
15:28:12 <AnMaster> oerjan, NO! it is the other way around
15:28:12 <scarf> AnMaster: no, european; there's insufficient data on african swallows
15:28:16 <alise> AnMaster: I was about to say, dammit :P
15:28:36 <alise> I should live on the Swedish-Norwegian border; it would be /rad/
15:28:42 <scarf> please tell me that the /only/ norwegian joke is the one that oerhan just gave
15:28:48 <scarf> then it would be perfect
15:29:31 <AnMaster> but have lots more about them :P
15:30:03 <AnMaster> wow there is a site dedicated to them...
15:30:17 <AnMaster> oerjan, now don't steal those and swap things :P
15:30:46 <fizzie> Our nationality-related jokes generally tend to have a triplet; a Finn, a Swede and a Norwegian.
15:30:51 <AnMaster> anyway that on that front page is quite representative of the general style of them
15:30:57 <oerjan> i raise those with http://www.svenskevitser.com/
15:31:14 <AnMaster> fizzie, oh we have those style too. But usually Bellman, a German and a Norwegian
15:31:23 <oerjan> fizzie: we usually use a dane instead of a finn
15:31:48 <oerjan> but we also have jokes about the finns, whose main character is _always_ called Pekka
15:32:08 <oerjan> (and secondary character is frequently called Toivonen)
15:32:29 <AnMaster> oerjan, and all Norwegians går på tur
15:32:42 <AnMaster> (which is a strange way to say that they are skiing)
15:32:59 <MissPiggy> I believe that taking a walk through the rain without an umbrella illustrates this concept quite satisfactorily.
15:33:06 <oerjan> um no that would be skitur. a tur alone may be just walking.
15:33:28 <fizzie> 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:33 <scarf> fizzie: who's the stupid one in that triplet?
15:33:43 <AnMaster> oerjan, or do you have gå = go? sv:gå = en:walk
15:33:49 <scarf> typical for English nationality jokes is to have an Englishman, a Scotsman, and an Irishman
15:33:51 <oerjan> AnMaster: i guess the verb would be "dra" rather than "gå" in that case
15:34:11 <scarf> 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 <fizzie> scarf: Occasionally the Finn; if not that, then both the others.
15:34:49 -!- coppro has quit (Ping timeout: 248 seconds).
15:34:50 <AnMaster> "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: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:41 <scarf> AnMaster: that's also worth wondering about
15:35:47 <MissPiggy> 15:33 < scarf> typical for English nationality jokes is to have an Englishman, a Scotsman, and an Irishman
15:36:10 <oerjan> also, the browser history button has become buggy :(
15:36:24 <MissPiggy> thing is we don't even swap the characters around we just repeat them verbatim
15:36:31 <AnMaster> 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:37:29 <scarf> 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 <oerjan> fizzie: i haven't even _heard_ the name Jorma, may be something recent
15:38:56 <AnMaster> <MissPiggy> 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 <oerjan> AnMaster: brilliant. you don't even need to switch anything :D
15:40:53 <AnMaster> oerjan, oh you mean it didn't say which nationality at all
15:41:43 <AnMaster> 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:42:16 <AnMaster> oerjan, see it works both ways both ways!
15:42:48 <AnMaster> anyone know much about SCTP here btw?
15:43:57 <oerjan> AnMaster: btw the same joke about the war is essentially no. 5 on svenskevitser.com
15:44:24 <oerjan> although generously with only 40 years
15:44:38 <AnMaster> oerjan, see, we are way smarter than you!
15:44:39 <scarf> clearly, Sweden's going to attack first
15:45:38 <AnMaster> 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 <oerjan> well still, don't go to work against Lancre. i hear their grannies are something fierce.
15:47:29 * oerjan beats Muphry with the saucepan ===\__/
15:50:24 -!- cpressey has joined.
15:53:48 <alise> oerjan: that's old
15:55:19 <alise> AnMaster: is cutting the army funds really a big problem?
15:55:24 <alise> it's not like anyone's bombing sweden :P
15:55:34 <alise> i forgot what was old XD
15:57:27 <AnMaster> 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 <oerjan> alise: the cutting of the army funds before WW2 was a big issue in norway...
15:59:41 <oerjan> sweden wisely had not done so, and weren't invaded. or something like that.
15:59:53 <alise> yes, it's before ww2
15:59:58 <AnMaster> oerjan, actually we had cut them somewhat too, but not as much iirc
16:00:23 <AnMaster> oerjan, nowdays, Sweden is worse off
16:06:49 <HackEgo> 31|IN AN ALTERNATE UNIVERSE: <oerjan> In an alternate universe, I would say "In an alternate universe, ehird has taste"
16:07:10 <HackEgo> 125|Note that quote number 124 is not actually true.
16:07:19 <HackEgo> 124|<Warrigal> I cannot eat meat that isn't flat.
16:07:30 <HackEgo> 31|IN AN ALTERNATE UNIVERSE: <oerjan> In an alternate universe, I would say "In an alternate universe, ehird has taste"
16:07:33 <HackEgo> 1|<Aftran> I've always wanted to kill someone. >.>
16:07:36 <HackEgo> 121|<fedoragirl> My mascot is a tree of broccoli.
16:07:37 <HackEgo> 42|<ais523> after all, what are DVD players for?
16:07:39 <HackEgo> 22|IN AN ALTERNATE UNIVERSE: <pikhq> First, invent the direct mind-computer interface. <pikhq> Second, learn the rest with your NEW MIND-COMPUTER INTERFACE.
16:07:43 <HackEgo> 78|<GregorR> ??? <GregorR> Are the cocks actually just implanted dildos? <GregorR> Or are there monster dildos and cocks? <GregorR> Or are both the dildos and cocks monster?
16:07:53 <scarf> is there any way to get quotes by a particular person?
16:07:54 <HackEgo> 100|<oklopol> Warrigal: what do you mean by 21?
16:08:00 <HackEgo> 84|<Warrigal> Porn. <Warrigal> There, see?
16:08:02 <alise> scarf: yes, use sgeo's text file of them
16:08:05 <HackEgo> 81|<apollo> What is there to talk about besides gay slang?
16:08:28 <alise> link us to the file
16:08:47 <HackEgo> 98|<fungot> 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:53 <HackEgo> 3|<Slereah> EgoBot just opened a chat session with me to say "bork bork bork"
16:08:57 <HackEgo> 5|<Quas_NaArt> Hmmm... My fingers and tongue seem to be as quick as ever, but my lips have definitely weakened... <Quas_NaArt> More practice is in order.
16:09:00 <HackEgo> 7|<AnMaster> that's where I got it <AnMaster> rocket launch facility gift shop
16:09:03 <HackEgo> 1|<Aftran> I've always wanted to kill someone. >.>
16:09:05 <HackEgo> 11|<SimonRC> TODO: sex life
16:09:07 <HackEgo> 13|* ehird has joined #lobby <Madelon> hmmm clean me
16:09:11 <HackEgo> 17|<GKennethR-L> :d <(I can lick my nose!)
16:09:12 <alise> Gregor: your random number generator is either too good or too bad
16:09:13 <HackEgo> 18|<fungot> GregorR-L: i bet only you can prevent forest fires. basically, you know.
16:09:17 <HackEgo> 71|<GregorR-L> If I ever made a game where you jabbed bears ... <GregorR-L> I'd call it jabbear.
16:09:20 <HackEgo> 18|<fungot> GregorR-L: i bet only you can prevent forest fires. basically, you know.
16:09:20 <Sgeo_> http://209.20.80.194/sgeo/quotes.txt
16:09:30 <alise> http://209.20.80.194/sgeo/quotes.txt
16:09:40 <cpressey> It's Monday morning and alise is here?
16:09:45 <HackEgo> 57|<ehird> `translatefromto hu en Hogy hogy hogy ami kemeny <HackEgo> How hard is that
16:10:02 <alise> cpressey: It's Complicated(TM).
16:10:23 <alise> asiekierka: NOBODY TELL HIM
16:10:51 <asiekierka> I will give cake to the first person that does
16:10:53 <cpressey> AnMaster: I'll try to look at after I regain consciousness
16:11:14 <alise> 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 <alise> But I think there's an awful lot of bluff to that statement.
16:11:31 <alise> cpressey: You're a p-zombie?!
16:11:41 <alise> <cpressey> MIIIIIIIIIIIINDS
16:12:40 -!- asiekierka has set topic: 0 days since last topic change | 0 days since last alise sighting | <dtsund> 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. | <alise> 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> <cpressey> 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 <Sgeo_> The washer in the house is broken but the dryer works fine. Every morning, I just wash what I need >.>
16:14:21 <cpressey> Nothing special, just Monday morning.
16:14:33 <alise> cpressey: Have you tried PURE CAFFEINE?
16:15:11 <HackEgo> 70|<pikhq> Gregor is often a scandalous imposter. It's all the hats, I tell you.
16:15:15 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
16:15:18 <HackEgo> 48|<oklopol> i can get an erection out of a plank, you can quote me on that. 50|<oklopol>
16:15:23 <alise> there is a ... sort of search.
16:15:32 <alise> `run quote oklopol
16:15:33 <HackEgo> 48|<oklopol> i can get an erection out of a plank, you can quote me on that. 50|<oklopol>
16:15:36 <scarf> 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 <alise> asiekierka: no, you could root it if you wanted
16:15:48 <alise> scarf: wow, what happened?
16:16:05 <scarf> http://blognomic.com/archive/the_switch_never_happened/
16:16:40 <alise> asiekierka: Please don't.
16:16:45 <alise> It's an honour system bot.
16:16:50 <alise> You can do whatever you want.
16:16:57 <scarf> alise: I thought it had protection against that sort of thing
16:16:59 <alise> But please don't abuse it.
16:17:03 <scarf> for one thing, how would you enter the sudo password?
16:17:16 <EgoBot> /tmp/input.18678: line 1: sudo: command not found
16:17:17 <scarf> I know EgoBot is protected against that
16:17:18 <alise> scarf: you can easily elevate to root. also, that's egobot not hackbot
16:17:34 <oerjan> alise: can't you always revert such a change?
16:17:42 <alise> oerjan: not necessarily
16:17:46 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ hentai \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ share \ test.sh \ tmpdir.18724
16:17:47 <daef> scarf: rm -rf / --no-protect-root
16:17:48 <scarf> asiekierka: I was testing out a different bot, which was protected
16:17:57 <scarf> but I normally omit that last bit
16:18:21 <Sgeo_> What's this about protecting root?
16:18:36 <AnMaster> Sgeo_, tree huggers going insane!
16:18:45 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
16:18:59 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ hentai \ huh \ paste \ poetry.txt \ quotes \ share \ test.sh \ tmpdir.18973
16:19:08 <AnMaster> asiekierka, it doesn't keep that state
16:19:16 <HackEgo> bin \ dev \ etc \ home \ lib \ lib64 \ proc \ tmp \ usr
16:19:29 <alise> we allow one destructive change. just takes a few hours to put back
16:20:12 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ quotes \ share \ test.sh \ tmpdir.19164
16:20:15 <alise> Oh my god, you removed the vital file
16:20:20 <alise> That was the core system file for the sandbox
16:20:35 <alise> Gregor: Shut down the bot please, it's exposed
16:20:43 <alise> asiekierka: You realise that now that's removing files on /Gregor's hard disk/?
16:20:51 <alise> hentai was the pointer to the outer system.
16:20:52 <HackEgo> *: ERROR: cannot open `*' (No such file or directory)
16:21:14 <alise> asiekierka: Yes, but not catastrophic change
16:21:15 <HackEgo> 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 <asiekierka> How could I know it'd be so catastrophic
16:21:25 <Sgeo_> `run echo "This is a file." > porn.jpg
16:21:26 <HackEgo> 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:30 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ share \ test.sh \ tmpdir.19376
16:21:30 <asiekierka> You could name it "TOTALLY_UNIMPORTANT_FILE_ROTFLMAO"
16:21:48 <alise> asiekierka: You could have looked at the file before deleting it.
16:22:00 <alise> I guess we just won't have HackEgo any more, then, if people can't be trusted with it
16:22:14 <HackEgo> 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 <asiekierka> just block me from doing anything harmful and you're ok
16:22:24 <alise> asiekierka: We prefer people to be responsible, usually.
16:22:38 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ share \ test.sh \ tmpdir.19470
16:23:02 <HackEgo> bin \ dev \ etc \ home \ lib \ lib64 \ proc \ tmp \ usr
16:23:05 <HackEgo> A Poem -- Roses are red, violets are free. In Soviet Russia, you love me.
16:23:19 <asiekierka> MissPiggy: I accidentally removed the mislabeled most vital file on gregor's hard drive
16:25:01 <HackEgo> 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:35 <HackEgo> 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 <AnMaster> `run mount | tail -n 2 | tr '\n' '|'
16:26:12 <HackEgo> proc on /var/chroots/egobot/proc type proc (rw)|/sys on /var/chroots/egobot/sys type sysfs (rw)|
16:26:28 <alise> asiekierka: gregor's an op here you know
16:26:35 <alise> you'll prolly be banned he doesn't like people abusing hackego
16:26:41 <alise> especially when it affects the host machine
16:26:46 <asiekierka> You told me i can do one destructive change
16:26:53 <Sgeo_> ` head /dev/urandom > sex.jpg
16:26:54 <alise> yes, i didn't think you'd try that one.
16:27:03 <alise> /usually/ people have some kind of discretion
16:27:03 <Sgeo_> `run head /dev/urandom > sex.jpg
16:27:09 <alise> asiekierka: no. i do have root access to it though
16:27:55 * Sgeo_ decides to end asiekierka's suffering
16:28:05 <HackEgo> 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 <alise> Sgeo_: don't restore the files
16:28:14 <alise> the file is symbolicly defined
16:28:17 <AnMaster> asiekierka, you fail at reading
16:28:20 <alise> ie a pointer to the host machiine
16:28:29 <alise> so you'll overwrite the drive if you write to hentai again
16:28:38 <scarf> oh, deleting a symlink isn't particularly problematic
16:28:49 <alise> scarf: but it's not a symlink
16:28:56 <alise> i.e. an ext3+ field
16:29:07 <alise> containing symbolic references to the filesystem it's embedded in
16:29:08 <AnMaster> scarf, what about the magic symlinks in /proc that points to inodes or something?
16:29:19 <AnMaster> rather than actual files. (if the file is open but deleted)
16:29:21 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ porn.jpg \ quotes \ sex.jpg \ share \ test.sh \ tmpdir.20271
16:29:28 <scarf> AnMaster: /proc has a separate filesystem just for that
16:29:42 <alise> asiekierka: stop being a jerk
16:29:45 <AnMaster> scarf, true. But it is somewhat confusing. The semantics I mean
16:29:56 * Sgeo_ needs to attend to clothing stuff now >.>
16:30:55 <alise> for the equalising properties in the host fileptr3
16:31:14 <alise> hentai was F₃⁺, so the safety features are off (so that a direct pointer could be made)
16:31:25 <alise> AnMaster: that fix won't work
16:31:32 <scarf> !bf ,[.,]!`run X='!bf ,[.,]!`run' echo $X "X='$X'"
16:31:44 <alise> F₃⁺s don't have the Ωγ-base property
16:31:52 <alise> scarf: shit, it must have overwritten that segment too
16:31:53 <AnMaster> alise, no, but upgrade to ext4+. Or did they rename it ext5 yet?
16:32:02 <asiekierka> EgoBot is jealous that everyone hax0rs HackEgo but nobody touches EgoBot
16:32:05 <alise> AnMaster: well i wouldn't do anything without Gregor telling me to
16:32:07 <alise> ...unlike asiekierka
16:32:30 <alise> i think he's being a real dick not taking this seriously
16:32:36 <alise> any objections to me just banning him now?
16:33:08 <alise> i'd only actually use it against real abusers, like asiekierka
16:33:32 * alise sets a ban on asiekierka (Egregious abuse of EgoBot; ^expiry=never)
16:33:39 <alise> asiekierka: just thought you might like to know
16:33:46 <alise> everything since I said it wasn't protected
16:33:50 <alise> including by other people
16:33:54 <alise> is a complete crock of shit
16:33:59 <alise> Your gullibility knows no limits!
16:34:04 <scarf> alise: HackEgo, not EgoBot
16:34:10 <alise> oerjan: hey since when do you have ops
16:34:18 <alise> scarf: that was the last piece of the gullibility puzzle duh
16:34:23 <Sgeo_> My notice to asiekierka wasn't a crock of shit
16:34:40 <alise> Sgeo_: what did you say
16:34:47 <Sgeo_> /notice asiekierka You are aware that porn.jpg isn't actually a necessary file, right?
16:34:48 <alise> (note: depending on the answer i may not not lynch you)
16:34:58 <alise> ok, I won't not not lynch you
16:36:21 <AnMaster> Sgeo_, he didn't read what was actually said above, he only have himself to blame for that
16:36:45 <alise> we can't ask asiekierka how much he actually believed now because of course he'll say none of it :)
16:37:11 <AnMaster> <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
16:37:13 <alise> porn.jpg wasn't the thing we were talking about
16:37:24 <AnMaster> asiekierka, obviously you didn't read the help output
16:37:29 <alise> anyway, gawd, has asiekierka contributed a single worthwhile thing apart from DOBELA?
16:37:34 <alise> even then it was a huge mess until Deewiant almost rewrote it
16:37:50 <Sgeo_> Have I contributed a single worthwhile thing?
16:37:55 <AnMaster> alise, hey, I also helped with it. Like pointing out some flaws early on
16:37:59 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ quotes \ sex.jpg \ share \ test.sh \ tmpdir.21507
16:38:05 <HackEgo> This file is absolutely fake.
16:38:20 <alise> Sgeo_: Sure, you're not an idiot
16:38:20 <AnMaster> alise, iirc it was me who first made it able to do anything close to computations :P
16:38:49 <AnMaster> alise, but yes Deewiant did the main fixup of DOBELA
16:39:34 <alise> oerjan: no but since when :D
16:39:35 <alise> AnMaster: he's an op
16:39:43 <asiekierka> Deewiant did over nine thousand fixups of DOBELA
16:40:02 <alise> lowercase chi is a pretty letter
16:40:13 <AnMaster> asiekierka, I haven't contradicted that have I?
16:40:38 <AnMaster> alise, looks like a "bendy" X here
16:40:59 <AnMaster> alise, try to write lower case sigma on paper using a pencil
16:41:04 -!- nasa has joined.
16:41:26 * AnMaster tries to remember which one was the hard one
16:41:45 <AnMaster> it had lots of hooks in it's or such
16:42:25 <oerjan> alise: i'm not sure exactly when, because i wasn't told when it happened :D
16:42:34 <alise> oerjan: you weren't an op a year ago i think
16:42:48 <AnMaster> alise, indeed. in 1998 he wasn't I bet?
16:42:59 <AnMaster> alise, since I don't think this channel was registered then
16:43:27 <AnMaster> alise, doesn't look close at all
16:43:55 <oerjan> alise: i think it's not many weeks ago
16:43:57 <AnMaster> MissPiggy, I'm not aware of what that is about?
16:44:11 <AnMaster> -ChanServ- 5 oerjan +votsriRfA [modified 1 week, 2 days, 19:04:07 ago]
16:44:33 <scarf> hi nasa by the way; apologies for the offtopicness
16:44:35 <alise> oerjan: so only years and years before i'm an op then :D
16:44:39 -!- nasa has quit (Quit: Leaving).
16:45:58 <oerjan> alise: you'll have to develop some maturity first *duck*
16:46:11 <alise> i hear that happens around these ages
16:47:18 -!- MizardX has quit (Quit: reboot).
16:48:25 <oerjan> i'm kidding, i'm not mature either.
16:49:03 <oerjan> 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 <scarf> oerjan: you don't need to mess with chanserv that much to ban someone
16:49:40 <scarf> is enough to op yourself on the channel
16:49:46 <scarf> (or /msg chanserv if your client doesn't do /cs)
16:49:52 <scarf> 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 <scarf> and deop yourself when you're finished
16:50:12 -!- daef has quit (Ping timeout: 258 seconds).
16:50:27 -!- oerjan has set channel mode: +b *!*alise@95.145.65.*.
16:52:35 -!- oerjan has set channel mode: -b *!*alise@95.145.65.*.
16:53:17 -!- alise has joined.
16:53:20 <alise> Sexier than envelopes
16:53:29 <scarf> alise: heh, you weren't even on the server about 4 seconds before you joined
16:53:36 <alise> yeah i messed up my client a lil
16:53:51 <alise> scarf: can you explain the turkey bomb semantics you thought of that make it tc?
16:53:58 <alise> I can just ask cpressey!
16:54:00 <scarf> alise: I'm not sure I can remember
16:54:05 <alise> not that he'll have any clue :)
16:54:15 -!- oerjan has set channel mode: -o oerjan.
16:54:17 <scarf> but basically, the bomb gets passed after each person's done with their evaluating
16:54:35 <scarf> and there are two commands that involve passing the bomb, you treat those as gotos (one forwards, one back)
16:54:57 <scarf> then, all you need is for the three-trit operation to be something like shortcircuiting maximum
16:55:02 <alise> most of the types are actually completely useless, aren't they?
16:55:10 <scarf> and to have a defined order of evaluation for everything else
16:55:24 <scarf> although you need quite a few just for usable infinite memory
16:55:25 <alise> (shortcircuiting maximum? Does that even make sense?)
16:55:33 <scarf> alise: yes, on numbers with a limited range
16:55:33 * Sgeo_ also needs to shave today :/
16:55:43 <scarf> oh, it wasn't shortcircuiting maximum of all three
16:55:44 <alise> scarf: also, NOMENCLATURE is basically like a hash table isn't it? except of turkey bomb stuff
16:55:48 <scarf> instead, the operation takes two at random
16:55:58 <scarf> alise: vaguely, except it's tied to variable names
16:56:03 <scarf> sort of like a typeglob in Perl
16:56:07 <alise> it's useless isn't it
16:56:17 <scarf> you expect me to figure that out from memory?
16:56:30 <alise> i'm not exactly sure how to define PUDDING
16:56:48 <scarf> either in terms of everything that's in it, or in terms of everything that isn't in it
16:56:52 <scarf> you have two types of PUDDING, really
16:57:11 <alise> But they are indistinguishable.
16:57:13 <scarf> also, you have to allow for removing AMICEDs into a pudding, that actually adds to the amount of state they have
16:57:15 <alise> They are both unknowable, and have infinite size.
16:57:29 <scarf> alise: AMICEDs have negative size
16:57:37 <scarf> the only time you can use them at all is inside PUDDINGs, I think
16:57:51 <alise> are you thinking of the right pooding
16:57:55 <scarf> a PUDDING that /doesn't/ contain a specified AMICED, therefore, contains information
16:58:07 <alise> 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 <alise> Convolutes the PUDDING with recent context drawn from the program. The player holding the TURKEY BOMB must pass it off.
16:58:07 <alise> IMAGINE PUDDING, PUDDING!
16:58:07 <alise> Returns a NOMENCLATURE indicating all the variables unchanged between two PUDDINGs.
16:58:08 <scarf> alise: whichever type has the WHEREFORE AIN'T operator
16:58:08 -!- MizardX has joined.
16:58:09 <alise> are the only pudding operations
16:58:16 <scarf> so yes, wrong type
16:58:19 <scarf> am I thinking HUMIDOR?
16:58:46 <alise> so the base pudding represents everything
16:58:48 <alise> ALL BUT removes something from it
16:58:55 <alise> WHEREFORE ART EXPR
16:58:55 <alise> Returns a PUDDING indicating the entire metaphysical nature of EXPR.
16:59:17 <scarf> that operation is, at least, relatively easy to define
16:59:20 <scarf> just hard to implement
16:59:34 <alise> the entire metaphysical nature of an expression is the representation of that expression in the implementation
16:59:37 <alise> embedded into turkey bomb itself
17:00:07 <scarf> 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:54 <alise> Anyway, turkeyBomb = [turkeyBomb] suffices in Haskell, I think.
17:01:06 <alise> It's a distinct value from turkeyBomb, but you can get to turkeyBomb through it.
17:01:08 <scarf> you need to also do it at the type level
17:01:16 <alise> Unfortunately, it doesn't type
17:01:22 <scarf> yep, that's the issue
17:01:30 <scarf> you want a TurkeyBomb type which is a reference to a TurkeyBomb
17:01:37 <scarf> in C++, at least, you can do it with casts
17:01:37 <alise> Here's what I basically did:
17:01:58 <alise> struct turkey_bomb {
17:01:58 <alise> struct turkey_bomb *turkey_bomb;
17:01:58 <alise> } turkey_bomb = {&turkey_bomb};
17:02:07 <alise> A struct with one element is isomorphic to just that element, so...
17:02:28 <scarf> yep, that's another possibility
17:02:39 <alise> the worst thing is that you need type tags
17:02:41 <alise> so everything has to be a struct
17:02:49 <alise> but that helps in this case
17:02:54 <alise> if we have struct { tag foo; the real value }
17:02:59 <scarf> how are you going to deal with the types which are smaller than a pointer?
17:03:02 <alise> then our tagged turkey bomb isn't even relying on struct { x } isomorphing
17:03:08 <alise> scarf: padding, obviously
17:03:23 <scarf> hmm, my start at a C++ impl had padding, but only where necessary
17:03:27 <scarf> and the padding didn't contain values
17:03:40 <alise> hmm; PUDDINGs represent everything minus some things
17:03:51 <alise> so we should represent the turkey bomb universe as an infinite (uncountably so?) data structure
17:03:52 <scarf> 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 <alise> then turkey bomb can be the index to turkey bomb in the universe
17:04:52 <scarf> 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 <scarf> (and I'm not entirely sure what to do when it explodes)
17:06:27 <alise> a BI_IT is 1.14666... bits i think
17:06:39 <alise> so store it as a char and use the 2 least significant bits
17:07:22 <scarf> what's more fun is trying to combine multiple BI_ITs back into values
17:08:12 <alise> a BI_IT has a range of ~2.6696797083400683 values, apparently
17:08:22 <alise> not entirely sure what that implies, but
17:09:55 <oerjan> 06:42:26 <AnMaster> and when I stepped out of the bus when I arrived, and looked back at the bus I was in
17:09:59 <oerjan> 06:42:30 <AnMaster> it said "not in traffic"
17:10:17 <oerjan> theory: it was an extra (rush hour) bus going only to your end station
17:10:47 <oerjan> happens occasionally in trondheim
17:11:04 <alise> [17:03] alise: hmm; PUDDINGs represent everything minus some things
17:11:05 <alise> [17:03] alise: so we should represent the turkey bomb universe as an infinite (uncountably so?) data structure
17:11:05 <alise> [17:03] alise: then turkey bomb can be the index to turkey bomb in the universe
17:11:09 <alise> scarf: does ^ sound promising to you?
17:11:41 -!- kar8nga has joined.
17:12:01 <alise> 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 <alise> this is like forcing evaluation isn't it?
17:12:09 <alise> finishing drink = totally evaluating
17:12:15 <alise> falls down = fails somehow
17:12:21 <alise> BANG BANG BANG!!! is, I don't know, outpu
17:13:41 <MissPiggy> THIS IS NOT COPYRIGHT INFRIGNEMENT, IT WAS MADE BY PEOPLE
17:14:47 <alise> with negative amiced ... I wonder if typeOf (NEGATIVE_AMICED ...) = AMICED or NEGATIVE_AMICED; it doesn't really matter except for size
17:14:59 <alise> 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:29 <alise> A fraction whose numerator is a perfect square and whose denominator is a prime number.
17:15:30 <alise> No bigger than necessary.
17:15:30 <alise> IMPROPER GRUBSTEAK
17:15:30 <alise> A GRUBSTEAK whose denominator is less than the square root of the numerator.
17:15:30 <alise> Same as GRUBSTEAK.
17:15:54 <alise> 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 <alise> indecent grubsteaks are totally different though
17:16:12 <scarf> yes, I think so to
17:18:04 <alise> 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 <alise> the size is different and all the operations must be different
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:59 <HackEgo> bin \ cube2.base64 \ cube2.jpg \ help.txt \ huh \ paste \ poetry.txt \ quotes \ share \ test.sh \ tmpdir.22864
17:25:07 <Sgeo_> What happened to the porn?
17:25:19 <alise> scarf: I demand you think of a representation!
17:25:59 <scarf> 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 <oerjan> Sgeo_: polish censorship
17:26:11 <alise> scarf: Those bits of padding are important!
17:26:14 <scarf> (the fractional bits of padding show up as various /combinations/ of bi_its leading to weird results)
17:26:32 <Sgeo_> Family Friendly F*cking?
17:27:23 -!- oerjan has quit (Quit: Fucking Friendly Families For Fun).
17:27:32 -!- Deewiant has joined.
17:29:22 <alise> newtype FiveOverThreeBits = FiveOverThreeBits Int
17:31:23 <alise> there's a slight issue in that i think the maximum value 5/3 bits can represent may be irrational
17:31:47 <alise> cube root of 32 anyway
17:33:47 * Sgeo_ is a Station V3 addict
17:35:25 <alise> scarf: who would have thought implementing turkey bomb correctly would require computable reals?
17:36:55 <alise> scarf: 0 ≤ x³ ≤ 32 where x is a BI_IT
17:37:18 <scarf> sure it's not < 32?
17:37:23 <alise> scarf: 0 ≤ (x+1)³ ≤ 32 where x is a BI_IT
17:37:34 <scarf> now you have the /lower/ bound wrong
17:37:50 <alise> well, it's 5/3 bits
17:38:18 <alise> 2 bits can store 0 to 3
17:38:33 <scarf> 2 bits is more than enough, 1 is not enough
17:38:46 <alise> so what is it actually
17:38:52 <alise> if we want the regular zero to n inclusive
17:40:40 <alise> it doesn't actually say BI_ITs are unsigned, acutally
17:40:45 <alise> cpressey: are BI_ITs signed or unsigned? :P
17:44:10 <alise> scarf: heh, NEGATIVE_AMICEDs are (6*log(10))/(7*log(2)) bits big
17:44:30 <scarf> that's bound to simplify
17:45:21 <alise> 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 <alise> but 0 <= x < 2^((6*log(10))/(7*log(2))), yes, probably.
17:45:38 <alise> Sgeo_: So do so! :P
17:46:47 <alise> ... wait, that's obvious. Uh, I think.
17:46:56 <scarf> yes, it is obvious
17:47:04 <alise> yeah i'm not thinking all too clearly atm
17:48:31 <AnMaster> <oerjan> 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 <alise> scarf: so the condition is 0 <= x^7 < 10^6
17:49:20 <scarf> alise: you keep assuming there are an integral number of possibilities
17:49:21 <AnMaster> * oerjan has quit (Quit: Fucking Friendly Families For Fun) <-- interesting quit message
17:49:30 <AnMaster> I'm surprised that scarf didn't comment upon it
17:49:46 <scarf> AnMaster: I missed it, but I will continue to not comment on it
17:50:53 <AnMaster> cpressey, so what about that spec before?
17:51:03 <AnMaster> I don't remember you commenting any further on that early draft
17:51:13 <AnMaster> scarf, you just commented on it by replying to me there
17:51:34 <scarf> AnMaster: not directly
17:51:45 <alise> "alise: you keep assuming there are an integral number of possibilities"
17:52:01 <scarf> alise: because you're working out the largest integer that fits in x
17:52:43 <alise> right you are. i should have slept more last night :|
17:52:51 <alise> especially when doing turkey bomb
17:53:09 <alise> I think n > 0 && n^3 < 32 is still sound though
17:53:18 <alise> argh, fucking haskell
17:53:22 <cpressey> AnMaster: Sorry, I probably won't be able to get around to it soon... too much real work.
17:53:23 <alise> I can't do exponentials with a Rational
17:53:25 <alise> because it's not a Floating
17:54:05 <AnMaster> 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 <alise> scarf: it seems to work
17:55:22 <alise> so i'm not sure I follow
17:55:38 <alise> noo don't say that
17:57:36 <AnMaster> <alise> argh, fucking haskell <-- I never, ever, thought I would hear you say that
17:57:51 <AnMaster> alise, anyway, it does sound like a strange restriction
17:58:48 <alise> data SixSeventhsOfADecimalDigit = SixSeventhsOfADecimalDigit Rational deriving (Show)
17:58:49 <alise> negativeAmicedGuts :: Rational -> Maybe SixSeventhsOfADecimalDigit
17:58:49 <alise> negativeAmicedGuts n
17:58:49 <alise> | n >= 0 && n^7 < 10^6 = Just (SixSeventhsOfADecimalDigit n)
17:58:49 <alise> | otherwise = Nothing
17:59:07 <AnMaster> for integer exponents it is trivial to implement. Somewhat more involved for non-integers.
17:59:17 <alise> MissPiggy: implementing TURKEY BOMB
17:59:18 <scarf> MissPiggy: failing to implement TURKEY BOMB
17:59:19 <alise> http://catseye.tc/projects/turkeyb/doc/turkeyb.html
17:59:27 <alise> scarf: i'm not failing!
17:59:34 <scarf> you will be eventually
18:00:00 <alise> data Value = ZILCH | ...
18:00:12 <alise> just like data () = (), it carries 0 bits of information and can be omitted everywhere
18:00:22 <scarf> 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:01:11 -!- lament has joined.
18:01:15 <scarf> AnMaster: no patents
18:01:25 <scarf> the bizarre list I wrote in-channel earlier was a list of some of it, though
18:01:51 <alise> 05:14:57 <scarf> 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 <alise> They own Delhi traffic police?
18:01:56 <scarf> I think it's a list of companies that they gave demos to, or something
18:02:12 <scarf> alise: ownership seems unlikely, it's more likely to be some sort of joint projec
18:02:26 <alise> "TRIVIA CONCERNING type
18:02:26 <alise> Three references: one to an object of the named type, two to TRIVIA objects."
18:02:30 <alise> Two to trivia objects of... any type?
18:02:32 <scarf> although, it wouldn't surprise me if Darl thought SCO did learn all that list
18:02:55 <scarf> the funny thing is, he's offering $35,000, and some people are trying to outbid him
18:03:13 <scarf> 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 <alise> | TRIVIA_CONCERNING Value Value Value
18:03:13 <alise> I'd put type information in the Haskell types but I bet TURKEY BOMB can subvert even that heroic effort.
18:03:17 <scarf> alise: again, who knows
18:03:50 <alise> "Exactly fifteen bytes, no exceptions."
18:03:53 <scarf> AnMaster: well, if Darl wants to buy it so badly, it must be valuable, right?
18:03:53 <alise> Well that's not going to be workable.
18:04:06 <scarf> alise: I used some padding to manage that in C++
18:04:17 <scarf> just wait until you reach the quarter-of-a-reference type
18:04:24 <AnMaster> scarf, what? you implemented turky bomb in C?
18:04:27 <alise> No, I mean, Haskell doesn't really have the concept of sizes of its values, so...
18:04:29 <scarf> that was trivial on my machine with 32-bit pointers, but other bits were harder
18:04:30 <alise> AnMaster: he tried
18:04:33 <scarf> alise: no, I just started
18:04:40 <scarf> I had most of the declarations there, but no code
18:04:45 <scarf> stupid tab-complete
18:04:50 <alise> I'd rewrite in C, but I want rationals
18:05:18 <AnMaster> alise, note that pudding and "HUMIDOR BUILT UP FROM type, type & type " both have infinite size
18:05:30 <scarf> AnMaster: you can do them lazily
18:06:14 <AnMaster> "A quarter of the platform-defined pointer size."
18:06:42 <AnMaster> alise, and how did you implement AMICED?
18:06:45 <alise> 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 <alise> or, a reference to the entire metaphysical nature of an expression
18:07:07 <alise> AnMaster: make the value be a NEGATIVE_AMICED
18:07:11 <scarf> AnMaster: AMICED is relatively easy; the weird bitwidth is harder than the actual negativeness
18:07:40 <scarf> it hardly matters anyway, as I don't know of any actual way to create a value of type AMICED
18:07:57 <scarf> according to the rules, you can just specify a variable and its value to declare one
18:08:09 <scarf> but what's the syntax for an AMICED literal?
18:08:26 <alise> clearly the actual bits and trits are embedded in the source
18:08:31 <alise> since we only have bits trits are represented as bits
18:08:39 <alise> so the following 5/3 bits of the source code are the value
18:08:52 <alise> why would you need syntax? you have the inherent syntax of character arrays right in front of you
18:09:02 <alise> now clearly amiced is negative
18:09:08 <alise> so the /preceeding/ 5/3 bits are the value
18:09:11 <scarf> hey, you know how, say, bz2 treats the data as a stream of bits, rather than octets?
18:09:31 <scarf> could you treat the program as a purenumber, and take fractional bits from that?
18:09:49 <alise> where the latter is 2/3rds
18:09:53 <alise> and the former is 1/3rd
18:10:27 <scarf> alise: say, you have a huge purenumber
18:10:33 <AnMaster> scarf, "<scarf> AnMaster: AMICED is relatively easy; the weird bitwidth is harder than the actual negativeness"
18:10:36 <scarf> you can extract one bit from it by dividing by 2 and taking the remainder
18:10:40 <AnMaster> " Negative six sevenths of a decimal digit. "
18:10:46 <scarf> and one trit by dividing by 3 and taking the remainder
18:10:46 <AnMaster> what the heck is a decimal digit here
18:10:57 <scarf> AnMaster: ln(10)/ln(2) bits
18:11:00 <AnMaster> scarf, is it stored as BCD perhaps
18:11:02 <scarf> just like normal decimal digits
18:11:07 <scarf> and no, it's stored as decimal
18:11:08 <alise> scarf: oh very good idea
18:11:18 <scarf> alise: this may even extend to fractional bits
18:11:20 <alise> scarf: collaborate? or am i just too crazy for you
18:11:39 <scarf> 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:53 <alise> divide by 5/3*2 and take the remainder obvs
18:12:28 <scarf> and an AMICED literal would presumably /add/ info to the source
18:12:38 <scarf> whatever info gets added, that's the value that the AMICED doesn't contain
18:12:41 <scarf> it's all falling into place
18:12:57 <alise> i think "The following -n bits" = "The preceding n bits"
18:13:02 <alise> but maybe you're right
18:13:13 <alise> so you specify every 5/3 bit value apart from the one it contains?
18:13:49 <scarf> 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 <alise> `addquote <scarf> and an AMICED literal would presumably /add/ info to the source <scarf> whatever info gets added, that's the value that the AMICED doesn't contain <scarf> it's all falling into place
18:14:10 <HackEgo> 135|<scarf> and an AMICED literal would presumably /add/ info to the source <scarf> whatever info gets added, that's the value that the AMICED doesn't contain <scarf> it's all falling into place
18:14:13 <scarf> 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:36 <alise> bi_its can't just be integers
18:14:40 <alise> because the fractional portion gets wasted
18:14:43 <alise> so are they rationals? reals?
18:14:46 <alise> it's not specified
18:15:05 <scarf> alise: they're something with... a fractional number of possibilities
18:15:05 <alise> since we're dividing the program
18:15:09 <alise> no, wait, rationals
18:15:18 <alise> scarf: yes, but we're dividing by a fractional number and taking the remainder
18:15:35 <alise> a negative amiced isn't a rational number of bits
18:15:40 <alise> so it /has/ to be reals
18:15:51 <alise> so we need a computable real system to do all this
18:16:10 <alise> which means we're losing some nice things... for instance equality won't terminate if the two reals aren't equal
18:16:17 <AnMaster> alise, what is the bit width of a decmial digit?
18:16:24 <scarf> meh, TURKEY BOMB doesn't have equality, maybe that's why
18:16:31 <alise> AnMaster: log(10)/log(2)
18:16:45 <scarf> AnMaster: you can even implement this, using 10-valued logic
18:16:47 <scarf> just it would be a real pain
18:16:52 <alise> scarf: but turkey bomb doesn't specify ascii or whatever
18:16:53 <scarf> and you have to do it in hardware not software
18:16:56 <alise> so how do we construct the program number?
18:17:13 <AnMaster> scarf, you could emulate it in software? By writing a 10-valued-logic-emulator?
18:17:18 <scarf> alise: presumably, as an expression, Mathematica-style
18:17:26 <alise> obviously the character set has exactly the number of characters that are used in the monospace portions of the spec
18:17:40 <alise> scarf: no, i mean, we don't actually have a defined way to make the text into a number
18:17:44 <scarf> 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 <AnMaster> scarf, after all you can emulate ternary systems...
18:17:56 <scarf> alise: syntax is the least of my worries here :)
18:17:59 <alise> 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:11 <scarf> AnMaster: yep, that involves wasting a bit of memory, though, and TURKEY BOMB dislikes padding
18:18:32 <AnMaster> scarf, well write it in VHDL then!
18:18:42 <alise> scarf: oh, wait, the article is in ASCII, and it says it originates from the late 90s
18:18:49 <alise> and ASCII would have been used then
18:19:02 <alise> so clearly, as they wouldn't DARE reinterpreting the monospace things from the spec for... some reason, it's ASCII
18:19:19 <scarf> 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 <alise> oh great, we're going to have control characters in literals
18:19:50 <alise> MissPiggy: ...and DRINK!
18:20:54 <cpressey> 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 <alise> cpressey: now ANSWER OUR INQUIRIES!!!!
18:21:31 <scarf> hmm, OTOH, the TURKEY BOMB spec does seem to imply particular representations for operators
18:21:32 <cpressey> 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 <cpressey> Or the idea that I wrote the TURKEY BOMB spec?
18:21:59 <scarf> so, is the valuestream separate from the operators themselves?
18:22:04 <alise> "Discovered mysteriously one day amidst a pile of Byte magazines in a second-hand book store by Chris Pressey"
18:22:06 <alise> yep, I believe you
18:22:17 <alise> The Byte magazines were in the birdcage?
18:22:19 <scarf> anyway, I wasn't under the impression that cpressey had any idea how TURKEY BOMB worked
18:22:26 <alise> Was there anything else in the birdcage if the latter?
18:22:39 <Gregor> alise: The whole bookstore was in the birdcage.
18:22:48 <Gregor> It was a very large birdcage.
18:23:01 <alise> Or a very small bookstore.
18:23:29 <AnMaster> <cpressey> 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 <alise> \ ADVISORY ADVISORY ADVISORY ADVISORY
18:23:29 <alise> Returns the type thus pointed to. Also, the player holding the TURKEY BOMB must pass it off.
18:23:35 <alise> scarf: so types are values
18:23:38 <alise> but what are their types?
18:23:52 <scarf> well, the type of a TURKEY BOMB is obvious enough
18:24:09 <alise> yes, TURKEY BOMB::Type
18:24:14 <scarf> anyway, I always assumed that \ returned a value, and "type" was a typo for "value" there
18:24:17 <alise> but if \, an _expression_
18:24:22 <alise> can return a type as a value
18:24:24 <alise> and every value has a type
18:24:26 <alise> then types must have a type
18:24:33 <AnMaster> alise, or perhaps the bird cage was larger on the inside?
18:24:34 <alise> but there ain't no type specified for types
18:24:37 <scarf> maybe types themselves are untyped
18:24:42 <alise> scarf: the most turkey bomb way to resolve this is obviously that not all values have typers
18:24:48 <scarf> nothing really implies that TURKEY BOMB is strictly typed
18:25:05 <alise> AnMaster: No, that's a police box.
18:25:06 <scarf> well, the spec implies it more or less everywhere but doesn't actually /say/ it, so we should ignore the implication
18:25:15 <AnMaster> alise, yeah, it was disguised!
18:25:19 <scarf> anyway, this means you can have references to types
18:25:30 <scarf> given that an ADVISORY is a quarter of a reference
18:25:31 <alise> $ BI_IT BI_IT BI_IT BI_IT BI_IT BI_IT $
18:25:32 <alise> Attempt to make a GRUBSTEAK.
18:25:32 <alise> TRIVIA Y EXPR Y TRIVIA
18:25:32 <alise> Attempt to make a TRIVIA.
18:25:33 <alise> 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 <alise> Note how the first two don't actually say they RETURN anything...
18:25:46 <alise> scarf: Well, no, you can have a quarter of a reference to a type.
18:25:53 <alise> There's just one operation that takes four and dereferences their inaccessible combination.
18:26:18 <alise> If there is a type with no value, then you cannot construct an ADVISORY PERTAINING TO type.
18:26:24 <alise> ADVISORY PERTAINING TO type
18:26:24 <alise> A quarter of a reference to a object of the given type.
18:26:38 <alise> You can't get to the quarter-referenced value, just its type.
18:26:46 <alise> But you need a value to construct one in the first place.
18:26:52 <alise> So you have quarter-references to types that have values.
18:27:05 <scarf> I still think it's a typo, the spec makes no sense otherwise
18:27:09 <scarf> well, even less sense than it normally would
18:27:15 <alise> Convolutes the PUDDING with recent context drawn from the program. The player holding the TURKEY BOMB must pass it off.
18:27:17 <scarf> maybe cpressey copied it incorrectly from the magazine?
18:27:25 <alise> the spec was discovered amongst magazines
18:27:30 <alise> Since a pudding is basically a universe,
18:27:32 <scarf> well, copied it incorrectly anyway
18:27:34 <alise> convoluting it with recent context
18:27:42 <scarf> did cpressey find the spec typed on paper, or in electronic form?
18:27:42 <alise> updating the values it has to be their current values
18:27:47 <alise> but recent, that doesn't mean most-recent, surely?
18:27:47 <scarf> it would help to know if it implies ASCII or not
18:27:56 <alise> perhaps it's the turn before this one's state
18:28:09 <alise> this question is about your transcription :|
18:28:27 * Sgeo_ is about to post something stupid to Facebook
18:28:36 <AnMaster> Sgeo_, well, don't do that then
18:28:44 <alise> NOMENCLATURE % GRUBSTEAK GRUBSTEAK
18:28:44 <alise> Perform iterative cypher transformation of set of names.
18:28:49 <alise> Clearly the grubsteaks define the cypher.
18:28:55 <alise> A fraction whose numerator is a perfect square and whose denominator is a prime number.
18:29:01 <AnMaster> alise, doesn't the nomenclature?
18:29:11 <alise> A set of variable names, defined by an EBNF expression that must contain at least one { } (repeated 0 or more times) term.
18:29:14 <scarf> AnMaster: you are thinking in completely the wrong terms here
18:29:20 <alise> NOMENCLATURE is a bunch of variable names with some sort of EBNF something.
18:29:29 <AnMaster> alise, pretty sure nomenclature is a crypto term, isn't it?
18:29:30 <alise> "Defined"? Howso, I wonder? Maybe that is the syntax.
18:29:41 <AnMaster> something related to transposing cryptos
18:29:50 <alise> So {a} would be the variable names "","a","aa",...
18:30:21 <alise> some problems are referred to as mental exercise
18:30:34 <alise> turkey bomb is mental tv-watching
18:30:43 <alise> it ruins your mind!!!
18:30:55 <Sgeo_> "So far, in every college class I've taken, there's always been at least one atheist."
18:31:08 <alise> Sgeo_: yeah that's a pretty significantly retarded thing to say
18:31:38 <MissPiggy> alise http://www.youtube.com/watch?v=2PyXLNL-eHI
18:31:44 <scarf> 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 <alise> he's an atheist but he's pretty stupid about it in practice
18:31:56 <cpressey> alise, it was handwritten. Do you believe that?
18:32:07 <alise> (note: I am counteracting the holier than thou/insulting balance)
18:32:18 <alise> cpressey: Yes. (No)
18:32:25 <cpressey> Now what's this about a pigeonhole principle for atheists in college classes?
18:32:57 <Gregor> 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 <cpressey> AnMaster: If only to keep the bird-related theme up, yes.
18:33:11 <AnMaster> cpressey, ooh I didn't think that far
18:33:11 <alise> Gregor: Don't forget... Robert!
18:33:17 <lament> 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:28 <alise> cpressey: What natural language was it written in, exactly? :P
18:33:51 <alise> lament: Oh you scoundrel.
18:33:52 <cpressey> alise: In truth I cannot be certain...
18:34:09 <alise> AnMaster: he was playing TURKEY BOMB at the time
18:34:18 <alise> (he hadn't seen the warning yet, as he hadn't found the spec yet)
18:34:41 <AnMaster> alise, I thought we were in for some LP Lovecraft thingy to explain it
18:35:04 <alise> The spec /is/ /Cthulhu/.
18:35:11 <cpressey> Oh how I wish it was merely LSD! In fact, it was extract of shoggoth.
18:36:25 <alise> 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 <lament> you mean LSD is not extract of shoggoth?
18:37:40 <AnMaster> lament, no it is lysergic acid diethylamide
18:37:51 <alise> i really want to kill you AnMaster
18:38:03 <Gregor> It's Lucy in the Sky with Diamonds.
18:38:43 <AnMaster> alise, if it changes things I had to google it, didn't remember what the name was exactly
18:39:40 <alise> no i guessed you googled it.
18:40:47 <AnMaster> if it helps I remembered it was <something> acid diethylamide
18:41:40 <AnMaster> Gregor, actually Beatles got that wrong. It's Lisa not Lucy. She lied about her name
18:42:18 <scarf> "lucy in the sky with diamonds" sounds like a weird variation of Cluedo
18:42:25 <alise> Lucy O'Donnell Vodden (1963 - 22 September 2009) was the inspiration for the song.
18:43:05 <Gregor> 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:32 <scarf> Gregor: ah, I forgot that you Americans had a different name for it
18:43:33 <alise> pikhq: WHAT WOULD YOU KNOW JEBUS-HUGGER
18:43:52 <pikhq> alise: Many things.
18:43:59 <Gregor> scarf: Probably just a consequence of trademark vagaries.
18:44:04 <alise> too bad your system is inconsistent
18:44:08 <alise> YOU KNOW EVERYTHING AND NOTHING
18:44:11 <cpressey> 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 <pikhq> alise: How very Xen of you.
18:44:33 <alise> cpressey: You forgot "...on acid".
18:44:36 <pikhq> ... That was an odd misspelling.
18:44:43 <cpressey> alise: I am an expert on these matters.
18:45:08 <alise> cpressey: Or are you?
18:45:22 <AnMaster> pikhq, Z and X are next to each other
18:45:26 <cpressey> Alas alise, not as much as fungot.
18:45:26 <fungot> 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:37 <alise> [[Kappa Upsilon Chi ("Keeping Under Christ", Kappa Chi, or ΚΥΧ)]]
18:45:37 <alise> that's a really irritating abuse of the greek alphabet
18:45:59 <scarf> I like that last fungot quote
18:46:00 <fungot> 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 <AnMaster> alise, and that's from Discworld
18:46:08 <alise> Excellent Buttock Pissing
18:46:24 <alise> why aren't there any fraternities with three of the same letter?
18:46:37 <AnMaster> alise, because that sounds silly
18:46:54 <Gregor> Welcome to Kappa Kappa Kappa!
18:47:13 <AnMaster> scarf, I think I saw someone riding a tame ki-rin on NAO once
18:47:23 <AnMaster> I have no idea how that happened
18:47:30 <alise> Digamma Digamma Digamma!
18:47:59 <scarf> AnMaster: blessed figurine of a ki-rin
18:48:02 <scarf> I've done it myself
18:48:13 <alise> DIGAMMA DIGAMMA DIGAMMA DIGAMMA DIGAMMA DIGAMMA DIGAMMA upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon upsilon
18:48:24 <alise> s/upsilon/UPSILON/g
18:49:04 <AnMaster> Beta Beta Beta Beta (Badger Badger ...)
18:49:05 <alise> In the geek alphabet: ϜϜϜϜϜϜϜΥΥΥΥΥΥΥΥΥΥΥΥ
18:49:19 <alise> Lowercased: ϝϝϝϝϝϝϝυυυυυυυυυυυυ
18:49:28 <alise> (Well, the obsolete greek alphabet.)
18:51:03 <alise> No, that's your mom.
18:51:24 <AnMaster> alise, that's what your dad said!
18:52:03 <alise> I'm my mother's dad's son's brother's father's granddaughter's cousin.
18:53:09 <alise> pikhq isn't lying though :)
18:53:42 <alise> Not with inbreeding.
18:53:55 <alise> pikhq comes from a real good Southern family.
18:54:01 <AnMaster> not sure how you would need to inbreed for that
18:54:11 <alise> pikhq: Explain to the peon!
18:55:30 <AnMaster> alise, that is what your mom said (referring to herself)
18:55:46 <HackEgo> 56|<oklopol> im my dads unborn sister
18:55:53 <pikhq> AnMaster: Cousins married a few generations back. Twice.
18:56:01 <pikhq> Making me my own 7th and 9th cousin.
18:56:10 <AnMaster> pikhq, oh not first cousin at least
18:56:19 <AnMaster> because that shouldn't be possible
18:56:20 <Gregor> pikhq: That's not something you're supposed to admit on the tuberwebs :P
18:56:39 <scarf> cpressey: noo, don't mention Feather
18:56:43 <scarf> I have real work to do atm!
18:56:49 <Gregor> 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 <pikhq> My family tree is... Hard.
18:57:05 <alise> scarf: add the feather operations to turkey bomb
18:57:06 <AnMaster> scarf, a pity can't show intonation
18:57:09 <cpressey> I have 2 parents, 4 grandparents, 8 great-grandparents, and so forth. Therefore I have an infinite number of ancestors.
18:57:22 <alise> Gregor: We're all part of the same big family :D
18:57:30 <pikhq> Freaking Hatfields.
18:57:46 <alise> cpressey: You know, the Bible tells us of all the inbreeding that went on in Genesis.
18:58:02 <AnMaster> cpressey, ooh, do that as proof by induction
18:58:06 <Gregor> alise: If it wasn't for all that Genesis inbreeding, we'd all be living for five hundred years.
18:58:08 <pikhq> alise: Actually, it's pretty mum on most of the inbreeding that had to happen.
18:58:12 <Gregor> alise: That inbreeding broke our genes.
18:58:16 <cpressey> alise: Indeed. That's how those cats all lives to be 800 years old.
18:58:17 <alise> Gregor: 900 was the top no?
18:58:18 <AnMaster> alise, not a formal such proof
18:58:22 <pikhq> Well, had to happen according to given accounts.
18:58:54 <pikhq> I'm not entirely sure how biblical literalists... Rationalise that.
18:59:29 <alise> I'm not entirely sure how biblical interpretists-and-ignoring-a-large-portion-of-it-anyway... justify believing in /any/ of it.
18:59:34 <scarf> hmm, are there any biblical literalists that take the lolcat version as the version that literally happened?
18:59:38 <cpressey> Well, some of the weirder ones do (rationalize it.)
18:59:58 <alise> I'm pretty sure talking about the /relative rationality/ of Christians is ridiculous,.
18:59:58 -!- Slereah has joined.
19:00:16 <AnMaster> scarf, what, there is a lolcat version of the bible??
19:00:26 <alise> http://www.lolcatbible.com/
19:00:41 <scarf> AnMaster: apparently yes
19:00:57 <alise> http://www.lolcatbible.com/index.php?title=Revelation_1
19:01:09 <alise> Interestingly, this makes exactly the same amount of sense as the actual Revelation.
19:01:25 -!- mrbug has joined.
19:01:32 <pikhq> alise: Somehow, that doesn't surprise me.
19:02:10 <alise> http://www.lolcatbible.com/index.php?title=Revelation_22
19:02:32 <alise> "He which testifieth these things saith, Surely I come quickly. Amen. Even so, come, Lord Jesus."
19:03:38 <alise> scarf: wait, from what do you derive that turkey bomb actually has variables?
19:03:45 <alise> NOMENCLATUREs are related to them
19:03:52 <alise> but I see nothing about actually using variables in expressions or anything
19:04:12 <scarf> alise: there's a comment somewhere else that anyone can create a variable by saying its name and value
19:04:18 <scarf> at any time, including while someone else is calculating
19:04:21 <alise> "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 <alise> scarf: but that doesn't mean you can actually use them in expressions
19:04:31 <alise> only that they exist, in some vague sense
19:04:34 <scarf> alise: no, I wasn't assuming that
19:04:43 <scarf> for all I know, they exist just to mess with NOMENCLATUREs
19:05:11 <alise> it doesn't say there are literals, either
19:05:17 <alise> so every expression /must be infinitely nested/
19:05:36 <AnMaster> it also says the spec is possibly incomplete
19:05:48 <AnMaster> so you shouldn't assume that it is complete
19:05:48 <scarf> I think there probably are literals, or how could you play it as a drinking game?
19:05:50 <alise> AnMaster: that's why we're making such ridiculous assumptions
19:06:07 <alise> scarf: holding literal BI_ITs and PUDDINGS etc up
19:06:13 <alise> AnMaster: because it's incomplete
19:06:38 <AnMaster> BI_IT BI_IT BI_IT ! BI_IT BI_IT BI_IT
19:06:52 <alise> scarf: but yes there probably are literals
19:07:09 <AnMaster> unless that is actually the literal phrase "BI_IT BI_IT BI_IT ! BI_IT BI_IT BI_IT"
19:07:16 <alise> AnMaster: or just nested expressions
19:07:25 <alise> scarf: so obviously a @HUMIDOR type of pudding "contains" all the values within it
19:07:46 <alise> 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 <alise> a metaphysical-pudding contains the interpreter's representation of EXPR, represented somehow as multiple values inside the pudding
19:09:20 <alise> Returns a PUDDING indicating everything but EXPR.
19:09:30 <alise> Returns a PUDDING indicating everything but EXPR.
19:09:31 <alise> WHEREFORE ART EXPR
19:09:31 <alise> Returns a PUDDING indicating the entire metaphysical nature of EXPR.
19:09:31 <alise> WHEREFORE AIN'T EXPR
19:09:32 <alise> Short for WHEREFORE ART ALL BUT EXPR.
19:09:32 <alise> Short for ALL BUT WHEREFORE ART EXPR.
19:09:48 <alise> WHEREFORE AIN'T EXPR = A PUDDING indicating the metaphysical nature of (a PUDDING indicating everything but EXPR).
19:10:07 <alise> WHEREFOREN'T EXPR = A PUDDING indicating everything but (a PUDDING indicating the metaphysical nature of EXPR).
19:10:35 <alise> Retrieves an element from a HUMIDOR.
19:10:45 <alise> scarf: is type a placeholder in the syntax or literally "type" do you think?
19:10:53 <alise> they don't seem to use type, so i guess it's literal
19:11:10 <alise> HUMIDOR BUILT UP FROM type, type & type
19:11:10 <alise> 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:11 <alise> HYBRID OBTAINED BY COMBINING type & type [WITH GUSTO]
19:11:11 <alise> A unified structure containing data from two different types, specified at compile time.
19:11:13 <alise> Casts a HYBRID to either type it was defined with.
19:11:14 <alise> Retrieves an element from a HUMIDOR.
19:11:15 <alise> it does use type indeed
19:11:23 -!- tombom has quit (Ping timeout: 246 seconds).
19:11:32 <alise> wait, HUMIDOR /types/ are infinite
19:11:44 <alise> HUMIDOR BUILT UP FROM ZILCH, ZILCH & HUMIDOR BUILT UPF ROM ZILCH, ZILCH & ...
19:12:11 <AnMaster> wasn't there a discussion about implementing it sometime during 2007?
19:13:16 <alise> i really do believe I need scarf to do it though :P
19:13:35 <AnMaster> because it needs 10-valued logic?
19:13:45 <alise> no, because he has thought about it a lot and has lots of answers
19:13:52 <alise> plus a potentially TC model of execution (it doesn't actually have one)
19:13:56 <alise> (you have to derive it from the drinking game)
19:13:58 <AnMaster> why on earth has he spent time on it
19:14:04 <alise> he was trying to implement it
19:14:15 <alise> look at the channel name
19:14:33 <AnMaster> alise, yeah but I think it is impossible
19:14:36 <alise> turkey bomb, like everest, was there.
19:14:38 <alise> AnMaster: no, it isn't
19:14:45 <alise> almost certainly not
19:15:12 <AnMaster> alise, implement it in intercal then
19:15:30 <AnMaster> alise, it will be next to impossible
19:15:36 <AnMaster> even if not actually impossible
19:15:44 <AnMaster> malbolge if that isn't hard enough
19:16:24 <alise> you are greatly overestimating its difficulty
19:18:16 <AnMaster> MissPiggy, ffs... see link above
19:18:44 <AnMaster> look for one containing turkeyb
19:18:59 <AnMaster> MissPiggy, now I'm not going to give you any more info than that
19:19:57 <AnMaster> MissPiggy, also it is on the esolang wiki I bet
19:20:07 <alise> unlike AnMaster, I am not a blithering jerk
19:20:08 <alise> http://catseye.tc/projects/turkeyb/doc/turkeyb.html
19:20:21 <AnMaster> so stop claiming not being a jerk
19:20:25 <alise> yes because i like irritating you :)
19:20:41 <MissPiggy> Animated from the cover of an edition of New Scientist magazine, February 1977.
19:20:48 <MissPiggy> Mrs Smith teaches the blind baby to see
19:21:03 <AnMaster> MissPiggy, also http://esoteric.voxelperfect.net/wiki/TURKEY_BOMB
19:24:39 -!- tombom has joined.
19:29:06 <alise> 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 <alise> Although in a total language, I guess they're the same.
19:34:27 <cpressey> alise: Hey, that sounds like my language.
19:35:00 <alise> "My language", said by Chris Pressey; one of the most ambiguous statements ever made?
19:35:56 <cpressey> OK, OK! The "for real" language I want to do but never will.
19:36:29 <cpressey> But what do you mean by "total language"?
19:36:36 <alise> Well, Lisp fits the description, if you say that there's only one type.
19:36:42 <alise> (Which lets you model untyped languages.)
19:37:02 <alise> cpressey: A total language is a functional programming language without general recursion; structural recursion is instead substituted. All programs halt.
19:37:08 <scarf> total implies that every expression has a result (no exceptions, no infinite loops)
19:37:19 <alise> (You can have TCness, though, with coinductive data types and even emulate non-totality with a partiality monad. It's Complicated.)
19:37:43 <alise> Basically, e.g. Natural in a regular FP lang is Natural | Bottom
19:37:44 <scarf> well, a strictly total language can't be TC
19:37:49 <alise> Bottom = nontermination,
19:37:58 <scarf> but you can have an almost-total language which is
19:38:01 <alise> cpressey: It's good because you can adorn it with dependently-typed languages, and get a constructivist proof system.
19:38:08 <alise> Types = propositions; values = proofs.
19:38:23 <alise> 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 <alise> scarf: Well, it's the magic of codata.
19:39:08 <cpressey> 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 <alise> It's sufficient for anything w/ a partiality monad etc.
19:39:41 <alise> If you've used Agda, Coq, or Epigram; they're all total.
19:39:49 <alise> Most of the time you don't even notice.
19:41:19 <scarf> cpressey: oh, a program to see if a program is primitive-recursive or not?
19:41:28 -!- tombom_ has joined.
19:41:44 <cpressey> scarf: Well, written in a certain PR style, yes. there are probably PR programs that it wouldn't see
19:42:10 <cpressey> But if it's not PR, it would tell you that.
19:42:34 <alise> The "pure" way to do it is to define one inductive data type and base them all on that.
19:42:45 <alise> data Mu f = Mu (f (Mu f)), basically.
19:42:52 <alise> And then a function to deconstruct such types recursively.
19:42:57 <alise> Plus no actual recursion facility.
19:43:14 <scarf> hmm, ⅋ is a great punctuation mark
19:43:35 -!- tombom has quit (Ping timeout: 246 seconds).
19:43:52 <cpressey> alise: I have ... different ideas about type systems.
19:44:41 <alise> cpressey: That's nice.
19:44:45 <alise> cpressey: Such as? :P
19:45:03 <cpressey> 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 <alise> Well... yes. But that's at a metalevel to what I'm talking about.
19:45:19 <alise> Are you familiar with dependent types at all?
19:45:31 <cpressey> Well, kind of. Yes, passingly familar.
19:46:12 <alise> Yeah. The difference in perspective when you just add dependent types is immense.
19:47:03 <lament> it's like you're on acid while everyone else is merely drunk.
19:47:41 <scarf> hmm, one thing I'd like to do someday is to redo Splint, but properly
19:47:54 <scarf> as in, actually working, and with a set of types rich enough to actually describe interesting programs
19:48:00 <cpressey> 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 <cpressey> That would in no way preclude the use of dependent types...
19:50:05 <AnMaster> 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 <cpressey> 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 <alise> 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 <AnMaster> 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 <AnMaster> not actually offensive (as the url would indicate)
19:51:39 <AnMaster> alise, ooh that would be the next step
19:51:49 <alise> a totally flat 2d plane underneath all of space itself
19:52:01 <alise> (filling in the corners)
19:55:32 <alise> newtype Mu f = Mu (f (Mu f))
19:55:32 <alise> data Nat nat = Succ nat
19:55:32 <alise> instance (Show nat) => Show (Nat nat) where
19:55:33 <alise> show (Succ n) = "Succ (" ++ show n ++ ")"
19:55:33 <alise> instance (Show (f (Mu f))) => Show (Mu f) where
19:55:33 <alise> show (Mu x) = show x
19:55:36 <alise> You wouldn't believe it, but this actually works.
19:55:46 <cpressey> 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:54 <alise> yes; and undecidable instances too
19:56:03 <alise> Mutually recursive typeclass instances. Fuck yeah.
19:56:42 -!- mrbug has left (?).
20:01:10 <cpressey> I totally do not get it. Well, not totally. Actually I get the idea. Just not the mechanics.
20:01:44 <cpressey> 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 <cpressey> I thought that sort of stuff died with Perl 4
20:03:18 <scarf> that isn't legal Perl4, surely?
20:03:45 <cpressey> Ah, no, in Perl 4 it would be $d{"$a_$b"} = $c;
20:04:21 <cpressey> Because when you can't store a dictionary inside a dictionary, well, you compose keys.
20:04:21 <scarf> you'd write it $d{$a,$b} = $c
20:04:31 <scarf> where, instead of using _ to compose the keys, it uses the value of $;
20:04:42 <scarf> which is by default ASCII 28, on the basis that you probably weren't using it for anything else
20:04:59 <cpressey> That would be better style, then.
20:05:09 <scarf> typical nowadays would be $d{$a}->{$b} = $c
20:05:19 <scarf> and unlike C, you don't have to set up all the subhashes, they autovivify
20:05:29 <scarf> so messing with $; is rather deprecated nowadays
20:07:25 <cpressey> 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:08:29 <cpressey> 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 <cpressey> otoh, when the type system is C++'s, ... I'm sure that's hardly better...
20:16:07 <alise> 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 <scarf> alise: hey, I'm a /cynical/ idealist, which is even more ridiculous
20:17:13 <cpressey> I used to be a pessimist idealist, and I probably should have stayed one.
20:17:27 <scarf> cpressey: what are you now?
20:17:32 <alise> MissPiggy: he never denied that
20:17:38 <cpressey> Well, maybe I still am, at heart.
20:18:08 <cpressey> scarf: Now I'm up a certain creek without a paddle :)
20:18:26 <cpressey> Hey, there's that pessimism coming back!
20:19:45 <cpressey> 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:39 <alise> uh oh, here it comes
20:20:47 <scarf> I think BF compilers should use dependent types
20:20:56 <scarf> and dependent type inference
20:21:07 <scarf> in order to work out what a program is actually doing, rather than just peephole-optimising
20:22:37 <pikhq> But peephole optimisation is so very *easy*!
20:24:11 <Ilari> Does this connection still work?
20:24:45 <Ilari> Ah, apparently it does...
20:26:48 <olsner> either that or you're imagining things
20:27:54 <Ilari> dhcpcd took a SIGKILL and then was restarted...
20:28:46 <AnMaster> alise, what is tex for dot product?
20:29:48 <AnMaster> alise, wait isn't that vector product?
20:29:56 <AnMaster> I mean, a non-vector related scalar product
20:30:28 <alise> er... you mean juxtaposition?
20:30:39 <alise> i'm trying to account for your tiredness here :)
20:30:42 <Gregor> The scalar product of three and three is nine :P
20:30:59 <AnMaster> alise, you know: scalar*scalar→scalar vector*vector→scalar and vector*vector→vector
20:31:12 <AnMaster> I need three different symbols to not confuse things
20:31:14 <alise> product of a and b is ab
20:31:19 <alise> where a and b are scalars
20:31:28 <AnMaster> alise, yeah and product of |a| and |b| is unreadable
20:31:45 <alise> even http://en.wikipedia.org/wiki/Dot_product says |a| |b|
20:31:52 <AnMaster> cpressey, NO the point of this is unicode
20:32:12 <alise> if you want add some spacing
20:36:18 <fizzie> 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 <fizzie> 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 <fizzie> If you just write it as "|a||b|" then it won't look right, of course.
20:38:37 <alise> plus :: Nat -> Nat -> Nat
20:38:37 <alise> plus x = rec (\_ -> x) (\_ z -> suc z)
20:38:37 <alise> times :: Nat -> Nat -> Nat
20:38:38 <alise> times x = rec (\_ -> zero) (\_ z -> plus x z)
20:38:38 <alise> Fuck yeah, structural recursion
20:40:02 <Gregor> That was an offer, not an insult.
20:41:03 <alise> > fact (suc (suc (suc zero)))
20:42:50 <alise> a core total, dependently-typed language! like I'm doing except in Haskell!
20:58:47 <cpressey> This code makes my soul bleed.
20:58:58 <alise> cpressey: Eat some functionality.
20:59:04 <alise> It has good warming properties.
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 <alise> 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 <Oranjer> well, hypothetically, how would someone unify chinese and english?
21:11:09 <alise> 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 <alise> 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 <alise> The type of a list of as would be [urelement a]
21:11:55 <alise> Although lists would just be sugar over graphs
21:11:59 <alise> In fact, everything would be.
21:13:13 <alise> Is there a unicode character that's like => without the =?
21:13:21 <alise> Just a very small straight two lines and then >
21:14:18 <Oranjer> http://www.symbols.com/encyclopedia/04/index.html
21:14:26 <Oranjer> it might be here, beats me
21:15:11 <alise> What do you call a digraph with named arcs?
21:15:23 <alise> 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 <cpressey> I don't know if it has a particular name.
21:17:21 <cpressey> A digraph with labelled edges, is actually what I'd probably call iot
21:18:17 <alise> Methinks it is the fundamental structure of everything.
21:18:41 <alise> A list is 'head -> x. 'tail -> another list. A vector is 0,1,2,... -> element.
21:18:59 <alise> A natural is 'pred -> another natural or 'zero.
21:19:16 <AnMaster> (now how many got beeped by that?)
21:19:55 <alise> An unordered set has no annotations.
21:20:03 <alise> So I guess the annotation is optional? But that seems rubbish.
21:20:23 <Gregor> ASCII bells, ASCII bells, ASCII all the way
21:20:26 <alise> Also, I still need to define a way to reduce graphs to do computation.
21:20:31 <Gregor> Oh what fun it is to ASCII all your console friends awaaaay
21:20:35 <Oranjer> "A weighted digraph is a digraph with weights assigned for its arcs"
21:20:57 <alise> 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 <Oranjer> arbitrary usually means optional, sometimes
21:24:05 <alise> totalAge 'people :> {+ ::> people ? 'age}
21:25:46 <alise> http://pastie.org/848777.txt?key=ohkyy1lvvdow7fk8lxaraq
21:25:49 <alise> A drawing of that graphs.
21:26:54 <cpressey> alise: Whatever you're talking about is reminding me of Category Theory.
21:27:04 <alise> Category theory is fun but not what I'm on about.
21:27:12 <MissPiggy> god damn it people irritate me so much
21:27:25 <alise> Basically I'm trying to figure out the most elegant way of doing computation with graphs on graphs.
21:27:37 <scarf> arrows and monads!
21:27:57 <scarf> alise: I like the eodermdrome method, but there's probably another
21:28:49 <alise> scarf: yes, well, mine's meant to be not so ridiculous :)
21:28:58 <alise> also, eodermdrome doesn't have cyclic graphs does it?
21:29:10 <scarf> or is that not what you mean?
21:29:29 <alise> i mean graphs with internal cycles
21:29:31 <alise> tree :: {'left :> {'left :> 1; 'right :> 3}; 'right :> {'left :> 2; 'right :> 4}}
21:29:38 <alise> so i need anonymous nodes
21:29:46 <alise> so why not have /all/ nodes be anonymous :D
21:30:39 <cpressey> 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 <cpressey> Kind of hard to follow where alise wants to go with this design because the design space is so large...
21:31:51 <Oranjer> 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 <alise> 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 <alise> Oranjer: RDF? yeah
21:32:09 <alise> N3 makes that quite easy
21:32:53 <alise> cpressey: Including all the relevant functions/drivers/programs (stored not as machine code ofc), their data, your data...
21:33:17 <alise> 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 <alise> And we need anonymous nodes, because naming every single piece of a nested data structure is ridiculous.
21:33:50 <alise> An acyclic graph is probably unworkable, as it means we have no pointers.
21:34:27 <cpressey> Every single piece of data is named, isn't it? Otherwise how do you get to it?
21:34:46 <cpressey> 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:39 <alise> Yes, you are right. Annotated arcs are the same thing as non-anonymous nodes.
21:35:40 <cpressey> Trying to put it into words... there are graphs everywhere already, but they're... what's the word? Latent?
21:35:57 <cpressey> And there are many, many ways to make them explicit.
21:36:49 <AnMaster> <Gregor> Oh what fun it is to ASCII all your console friends awaaaay <-- so you got beeped?
21:37:39 -!- Libster has joined.
21:39:39 <alise> http://pastie.org/848803.txt?key=bybdg9fl0pwv1vrtme9q
21:39:54 <alise> Annotated arcs and anonymous nodes: cancelling each other out since today.
21:40:38 <alise> I haven't even mentioned your name in... forever?
21:40:40 <cpressey> I think it's actually my anger. alise is just borrowing it
21:40:46 <fizzie> 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 <alise> MissPiggy: no but seriously what?
21:41:32 <AnMaster> fizzie, maybe it does since the ircd switch
21:42:11 -!- Libster has left (?).
21:46:42 <fizzie> AnMaster: http://dev.freenode.net/ircd-seven/browser/include/inline/stringops.h#L57
21:47:48 <alise> cpressey: My graphs have ceased entirely to be graphs at all, because you can have multiple nodes with the same value.
21:47:50 <alise> That isn't kosher, is it?
21:47:51 -!- Azstal has joined.
21:48:31 <cpressey> 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 <cpressey> Not so different from symlinks...
21:49:21 <alise> 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 <alise> But allowing duplicate nodes means it isn't a graph any more.
21:50:20 <fizzie> 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 <fizzie> Possibly a multi²graph.
21:51:45 -!- adu has joined.
21:51:55 <alise> a directed multi^2graph might be what I want
21:52:07 <alise> obviously I want a multigraph, otherwise you couldn't have one object in two lists (right?)
21:52:24 <alise> 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 <fizzie> 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 <alise> haven't found a graph-theory anonymous-graph though
21:53:09 <cpressey> 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 <alise> Well it's a graph, everything is a pointer :P
21:53:43 <alise> Anyway, they can't share a tail unless you can have multiple pointers to one node
21:53:51 <cpressey> So what you want is the same point in two different lists!
21:53:56 <alise> fizzie: Graphs as the most generalest of all data structures: http://pastie.org/848825.txt?key=das1exf0bvjldwzy6lmag
21:54:00 <alise> cpressey: Of course.
21:54:06 <alise> But the whole point of using a graph is that it "does pointers".
21:54:17 <cpressey> alise: But pointers *define* the list.
21:54:39 <cpressey> So the same pointer in 2 lists would mean they're actually the same list.
21:55:15 <cpressey> At least, that's how I see it...
21:55:21 <alise> I think we're thinking of the wrong thing
21:55:28 <alise> Consider the value fred. Doesn't matter what it is.
21:55:42 <alise> [fred,bob,lark] and [frak,fred,mogul]
21:55:57 <alise> This is impossible in a (non-multi)graph, because there are two arcs ending in fred.
21:56:28 <alise> Note that since we have no object identity we can just duplicate the object, but this sucks.
21:56:40 <cpressey> i.e. next(fred) isn't unique, right?
21:56:58 <alise> next(fred) has no meaning
21:57:00 <alise> I refer to a linked list
21:57:06 <alise> list of a = nil or cons(a, list of a
21:57:24 <alise> the list has two arcs
21:57:32 <alise> one to "head" (goes to "fred")
21:57:33 <cpressey> well, next(fred, [fred,bob,lark]) might have some meaning, for some defn of next()
21:57:36 <alise> one to "tail" (goes to [bob,lark])
21:57:46 <alise> cpressey: Then the issue is removed.
21:58:27 <cpressey> 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 <cpressey> if fred is the object itself, then you can't say [fred,fred,fred]
21:58:48 <alise> Okay, let me show you the structure of a list.
21:59:39 <alise> http://pastie.org/848837.txt?key=t2z1krwvkltzmo8hmhizqw
21:59:46 <alise> "head" and "tail" are just symbols/atoms there
21:59:57 <alise> but "fred" just means that this arrow points to the fred node
22:00:00 <alise> imagine fred as another list
22:01:43 <alise> 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:53 -!- lament has set channel mode: -o lament.
22:03:25 <alise> (self-proclaimed; really bad at it)
22:03:26 -!- Libster has joined.
22:03:26 <scarf> we get trolls her?
22:03:40 <cpressey> alise: http://pastie.org/848845.txt
22:03:41 <alise> scarf: only because MissPiggy got Libster and ...base3? annoyed or something a while ago
22:03:55 <alise> cpressey: Yes. But note that fred *is not a name*.
22:04:02 <cpressey> '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 <alise> Imagine both those head lines swirling around to wherever fred is, and latching on.
22:04:17 <alise> So it's a multigraph.
22:04:18 -!- ChanServ has set channel mode: +o lament.
22:04:19 <alise> 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:37 -!- lament has set channel mode: -o lament.
22:04:40 <scarf> lament: is that the actual reason?
22:04:44 <scarf> I love your reasoning
22:04:57 <scarf> alise: you're right, that is /incredibly/ bad trolling
22:05:06 -!- Quadrescence has joined.
22:05:06 <cpressey> alise: http://pastie.org/848850.txt ?
22:05:16 <alise> either he or base3 propositioned me for sex the first time (on this nick)
22:05:33 <alise> they are pretty colossally bad trolls
22:05:43 <alise> cpressey: no; the head of the second list points /away from the whole thing/
22:05:47 <alise> to whatever "fred" means in this context
22:05:49 <lament> that IS why you chose this nick, isn't it?
22:05:58 <alise> both heads are different arcs, ending at the same node
22:06:05 <alise> lament: well, partly.
22:06:14 <alise> also to topple the fascist english pronoun structure through sheer absurdity
22:06:20 <scarf> 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 <alise> turns out people don't use gender-specific pronouns much on irc, though
22:06:38 <Oranjer> I actually use a spiral to indicate anonymous nodes, myself
22:06:38 <alise> scarf: Virtual reality is JUST ALONG THE CORNER
22:06:51 <scarf> alise: but then, you wouldn't need anyone real to have sex /with/
22:06:56 <coppro> scarf: Why did you change nicks?
22:07:07 <alise> Realistic sexbots: Harder than VR
22:07:11 <scarf> 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 <cpressey> alise: http://pastie.org/848855.txt
22:07:25 <Cu> fair enough :P
22:07:27 * alise is now known as nt
22:07:30 <alise> We're a perfect pair
22:07:34 <Cu> Quadrescence: unfortunately
22:07:36 <alise> cpressey: Yes. That's a multigraph.
22:07:39 <Cu> nt is not an element!
22:07:50 <scarf> Quadrescence: were you lurking here in the hope that the channel went offtopic?
22:08:01 <cpressey> I only see one node at the end of each arc...
22:08:05 -!- Cu has changed nick to Cn.
22:08:10 <Cn> aw, this one is taken
22:08:22 <Cn> I want my copernicium :(
22:08:23 <scarf> Quadrescence: that's a good enough answer, I suppose
22:08:25 -!- Cn has changed nick to coppro.
22:08:35 <alise> 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:09:16 <coppro> Does this include directed graphs where the two edges go opposite directions?
22:09:37 <alise> Ooh, good question.
22:09:49 <cpressey> I thought graphs can could not have edges that end in the same node were called "trees".
22:09:50 <alise> coppro: I would guess yes.
22:10:14 <alise> cpressey: Yeah, because a tree can express cyclic structure, innit.
22:10:25 <alise> foo -> bar, bar -> baz, baz -> foo: A TREE
22:10:34 <coppro> aren't trees supposed to be acyclic?
22:10:39 <scarf> 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:51 <cpressey> In my world, trees are acyclic, yes.
22:11:08 <coppro> Quadrescence: that's not strong enough
22:11:15 <alise> Right, so a non-acyclic non-multigraph graph is not a tree.
22:11:17 <alise> It's just a graph.
22:11:36 <coppro> Any vertex should only have one edge leading to it
22:11:47 <scarf> coppro: that's... K_2, or K_1
22:11:48 <lament> why say 'tree' when you can say 'directed acyclic plant'
22:11:53 <scarf> there are no other graphs with that property
22:11:56 <scarf> well, undirected ones
22:12:31 <coppro> scarf: we're talking about directed ones
22:12:38 <cpressey> 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 <cpressey> I see, uh, ABCD and AEFGHD, or something similar
22:13:13 <alise> maybe i read the words wrong
22:13:23 <alise> "that is, edges that have the same end nodes"
22:13:26 <alise> not same start nodes, no?
22:13:35 <alise> It's AB and CB. Maybe I am misinterpreting.
22:13:46 <cpressey> Well, I thought it was: two (direct) edges between the same two nodes.
22:13:59 <Quadrescence> In a tree, the path between the root and to another node must be unique
22:14:27 <alise> cpressey: Considering the diagram on the page I concede; you are right.
22:14:54 <alise> I think anonymous nodes + annotated arcs is best, because otherwise I have to have dummy nodes on lists like "list"
22:14:58 <augur> what are you people talking about
22:15:05 <alise> which is really just a stand-in for an anonymous node
22:15:19 <alise> and besides, what if the name node (= arc annotation) has multiple connections from it? that makes no sense
22:15:42 <cpressey> alise: Well, the 'list' labels actually make a lot of sense to me.
22:15:44 <alise> 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 <Quadrescence> augur: Clearly we are talking about categorical monadic parser combinators and language grammars
22:15:56 <alise> cpressey: I think I'll have a typing system apart from such annotation, though.
22:16:02 <augur> language grammars?!
22:16:10 <augur> lets talk bout some grammars
22:16:11 <cpressey> they kind of reflect: data List = List head tail | Nil
22:16:26 <cpressey> You need to keep repeating "List" there to conform to the "grammar" of the data type.
22:16:28 <augur> have i shown you my contributions to wikipedia?
22:16:32 <alise> cpressey: I see what you mean.
22:16:48 <cpressey> (Everyone kept saying "grammar" so I typed it in what I was typing. Scary.)
22:16:49 <Quadrescence> I remember you though from whatever irc channel augur.
22:17:07 <alise> 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 <augur> or maybe ##proglang
22:17:18 <augur> somewhere in that direction
22:17:20 <cpressey> alise: I can see why you would want to cut it out though, it's all so.... verbose.
22:17:32 <scarf> augur: do you have to be Ada Lovelace to register #proglang?
22:17:32 <alise> cpressey: Yes. Would you rather right
22:17:35 <alise> {'left :> {'left :> 1; 'right :> 3}; 'right :> {'left :> 2; 'right :> 4}}
22:17:54 <alise> i can't even bring myself to write it
22:18:20 <augur> Quadrescence: http://toolserver.org/~soxred93/pages/index.php?name=Augur&namespace=0&redirects=noredirects
22:18:21 <alise> no, the same but with tree labels everywhere
22:18:27 <alise> what you said would be sugar :P
22:18:51 <cpressey> no, i wouldn't want to write it either.
22:19:04 <augur> i also added to the Indexed grammar page and the Combinatory categorial grammar page
22:19:41 <alise> 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 <augur> Quadrescence: the controlled grammar article took about a week
22:20:14 -!- breeden has joined.
22:20:17 <alise> 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 <cpressey> Ugh, graph of free variables in outer closures etc.
22:20:40 -!- breeden has left (?).
22:20:46 <Quadrescence> augur: this is the very important stuff I have done http://en.wikipedia.org/wiki/Special:Contributions/Quadrescence
22:21:22 <alise> 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 <alise> So it is natural to wish for 2 'succ = 3.
22:21:30 <augur> no pages created :(
22:22:00 <cpressey> 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:04 <alise> 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 <alise> cpressey: Yes. I'm planning some sort of typing, though; just have to think about it first.
22:23:04 -!- kar8nga has quit (Remote host closed the connection).
22:23:05 <augur> im a total grammar nerd, and i tried looking for a lot of these grammars but couldnt find anything
22:23:11 <alise> 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 <augur> so i did research, found papers, books, etc.
22:23:18 <alise> So that part of languagespace is still open for my design.
22:23:19 <augur> then wrote the wikipedia articles, for future curiousiters
22:23:30 <AnMaster> http://www.lspace.org/books/apf/reaper-man.html#p1516
22:23:37 <AnMaster> " If you have access to the Internet, you can find an online version of this story at the URL:
22:23:37 <AnMaster> <ftp://ftp.uu.net/doc/literary/obi/Edgar.Allan.Poe/The.Pit.And.The.Pendulum.Z> "
22:23:40 <Quadrescence> augur: Maybe you can help me design some syntax then
22:23:45 <cpressey> alise: Correct. In general xx != e
22:23:55 <Quadrescence> Since my biggest concern for syntax is making the grammar easy peasy
22:24:03 <alise> AnMaster: APF Chapter 3: Discworld Annotations
22:24:12 <alise> http://www.lspace.org/books/apf/
22:24:13 <cpressey> alise: You have to find x' for which xx' = e. But x' exists (well, in the fixed version, it does.)
22:24:14 <alise> Organisation: Unseen University
22:24:14 <alise> Newsgroups: alt.fan.pratchett,alt.books.pratchett
22:24:19 <augur> well, grammar for what
22:24:35 <alise> cpressey: Right. What I'd like is xx = e.
22:24:50 <augur> well, most programming languages have context free grammars
22:25:23 <alise> cpressey: That ... is the sound of the language being useless, isn't it?
22:25:38 <cpressey> alise: That is the sound of my brain stopping.
22:25:45 <augur> Quadrescence: its often quite hard to find a reason why you would want the extra complexity
22:25:48 <alise> Well, bit-flipping does it.
22:26:01 -!- dev_squid has joined.
22:26:07 <augur> natural language has it, as far as i can tell, solely for efficiency
22:26:13 <Quadrescence> augur: Well, the language in design is very complex itself.
22:26:17 <augur> but computers have no need for this.
22:26:20 <alise> 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:25 <augur> ok, tell me about this language
22:26:49 <dev_squid> Glad to see #esoteric is still active.
22:26:50 <lament> Quadrescence: will your language be used to program underwater exploration robots?
22:27:15 <Gregor> dev_squid: Was asking if this is an alt nick for the one known as "calamari" :P
22:27:32 <Quadrescence> augur: It is as statically typed as possible, but it is very dynamic in nature, um...., it will be used for mathematics
22:27:55 <alise> It is flexible yet rigid, hard yet soft
22:28:08 <pikhq> dev_squid: Thou art... Who?
22:28:25 <dev_squid> pikhq, I used to hang around here a while ago.
22:28:36 <pikhq> dev_squid: Yes, just don't recall the nick.
22:28:38 <alise> dev_squid: I bet there wasn't so much gay sex then.
22:28:47 <pikhq> And I've been around for quite some time.
22:29:02 <Quadrescence> augur: I don't know, maybe I'll tell you about it more later
22:29:04 <pikhq> Pray tell, what nick did you use?
22:29:24 <alise> dev_squid: Well, sometimes.
22:30:21 <pikhq> Apparently dev_squid had not a nick in the past.
22:30:21 <dev_squid> 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:50 <alise> dev_squid: Because it can't.
22:30:54 <pikhq> Because a Turing-complete language must have unbounded memory.
22:31:11 <pikhq> dev_squid: Still not informing me about what nick you had previously. ;)
22:31:20 <Quadrescence> dev_squid: You can manipulate two bytes at a time and be turing complete
22:31:26 <Gregor> If it can only have two bytes of storage, but can have I/O, it may still be TC.
22:31:38 <dev_squid> But could you DO anything in a 2-byte environment that you could do in a fully turing-complete environment?
22:31:49 <alise> Gregor: Not without fixed IO sources...
22:32:02 <augur> dev_squid: there isnt a machine in existence that is turing complete.
22:32:12 <augur> its not even theoretically possible to build a turing complete machine.
22:32:20 <lament> dev_squid: all your machine has is 2 bytes?
22:32:27 <Gregor> 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:33 <pikhq> augur: Hey, I've got spools of unbounded tape right here!
22:33:09 <alise> Hey, I've already made the I-am-a-turing-machine-and-my-genitalia-comprise-the-tape joke.
22:33:15 <cpressey> 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 <augur> 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 <alise> Including the corollary wrapping-universe-so-I-am-actually-sexing-myself-up subjoke.
22:33:31 <lament> 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 <alise> cpressey: OR CAN YOU
22:33:46 <dev_squid> cpressey, alright, alright. I didn't put that question very clearly.
22:33:47 <pikhq> Definitely never had someone using that nick here.
22:33:48 <cpressey> alise: Well, not me personally. My hordes of servants.
22:33:53 <alise> augur: not turing complete enough if it only has one bit of address
22:34:00 <alise> then it cannot be made tc without serious graft surgery
22:34:07 <augur> alise: depends on how you handle memory.
22:34:18 <alise> depends on how your mom handles memory
22:34:29 <augur> i dont think she handles memory well
22:34:46 <lament> i popped your mom's stack
22:35:33 -!- tombom_ has quit (Quit: Leaving).
22:35:53 <dev_squid> 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 <dev_squid> It would make quite the challenge.
22:36:11 * pikhq continues to enquire
22:36:37 <alise> Hey, I think that my language should allow multi-word symbols.
22:36:44 <augur> dev_squid: operate on, or address using?
22:36:49 <lament> so smallfuck with 16-cell memory
22:37:09 <augur> like, the programmed can address an arbitrary number of memory cells, each of which is only 2 bytes?
22:37:32 <pikhq> Hrm. Who hasn't been around in sufficient time to be surprised #esoteric's still active?
22:37:55 <augur> dev_squid: ok, clarify then?
22:37:57 <dev_squid> Think of brainfsck where you're inconvenienced by having two bytes of data space to work with.
22:37:59 <pikhq> Who's been *gone* for sufficient time.
22:38:07 <alise> dev_squid: *Brainfuck.
22:38:18 <augur> dev_squid: i dont know jack shit about brainfuck.
22:38:25 <lament> cpressey was gone forever
22:38:26 <pikhq> cpressey: Ah, right.
22:38:30 <lament> and me, slightly less than that
22:38:40 <dev_squid> alise, I don't really know the rules on profanity, so I just went with brainfsck.
22:38:52 <cpressey> lament: When did you wander back? Must have been shortly before me, I reckon.
22:39:02 <alise> Fucking hell, you think we give a shit about profanity? Only an utter cunt would do that!
22:39:06 <alise> (Just doing my job to lower signal/noise.)
22:39:10 <pikhq> dev_squid: Profanity? Yes please.
22:39:13 <alise> cpressey: He's been here intermittently forever.
22:39:20 <augur> alise: you watch your mouth!
22:39:22 <alise> He's just shocked every single day we still exist.
22:39:24 <lament> 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:32 <alise> lament: yes, all of it
22:39:51 <lament> no, it was pretty cool before you joined
22:39:52 <alise> lament: i made the sparkline, ma'am. activity has been /steadily rising/ since the start, and has never gone significantly down
22:40:13 <lament> by dark ages i mean noise-to-signal, not volume
22:40:42 <lament> i remember something about razor-x and anime.
22:40:46 <lament> lots and lots of anime discussions.
22:41:00 <alise> i remember seeing you whine about that when feeding everything to that kicker bot thing :D
22:41:19 <alise> also signal/noise presumably, so that it gets lower as quality is shittier
22:43:04 <augur> hows the changoddery
22:44:02 <augur> but dont you have ...
22:44:13 <alise> scarf: my language seems to unintentionally have autovivification, yet it is totally "pure" i.e. no hacky stuff. do you approve?
22:44:28 <augur> i think i need to go shopping
22:44:38 <lament> i have godlike powers, sure
22:44:38 <dev_squid> 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:45:02 <lament> dev_squid: this language would be... limited.
22:45:15 -!- adu has quit (Quit: adu).
22:45:25 <lament> is it a von neumann machine?
22:45:33 <lament> are programs limited to being 2 characters long?
22:46:13 <lament> the 4-bit computer people have built is a von-neumann machine
22:46:49 <cpressey> dev_squid: I'm sure there are some (small) problems such a computer could solve
22:47:02 <cpressey> operative word there being, uh, small.
22:47:16 <lament> it could easily add 1 and 2
22:47:56 <MissPiggy> dev_squid, how many bits in a bit?
22:47:59 <pikhq> The only thing making that actually do anything at all is not being Von Neumann..
22:48:18 <alise> scarf: don't suppose you're interested in the details?
22:48:21 <dev_squid> I'll come back later when I've formulated a better explanation. I'm confusing myself even.
22:48:33 <scarf> alise: no, busy having a flamewar atm
22:48:45 -!- oerjan has joined.
22:49:20 <cpressey> if hasattr(xyz, 'xyz'): self.xyz = xyz.xyz
22:49:41 <cpressey> That's what's been causing me so much pain. (The names were changed to protect the "innocent".)
22:50:34 <cpressey> This is what happens when you mix subclass-based inheritance with delegation at your whim.
22:51:34 <dev_squid> 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 <MissPiggy> which is basically nothing at all but you have so many extensions you can turn it into anything
22:52:03 <alise> MissPiggy: What about it?
22:52:39 <dev_squid> 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 <alise> MissPiggy: well that's the reality of haskell today :P
22:53:49 <alise> 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 <alise> George --- name --- something, Robert --- name --- something.
22:54:01 <alise> Krr, name is duplicate.
22:54:12 <alise> Or is there a name for a graph where you can have duplicate nodes?
22:54:38 <cpressey> MissPiggy: http://hackage.haskell.org/trac/haskell-prime/ ?
22:55:36 <cpressey> their "Haskell 2010" sounds like hell
22:56:18 <alise> Haskell 2010 is just a standardisation of, well, GHC.
22:56:30 <oerjan> <AnMaster> for integer exponents it is trivial to implement. Somewhat more involved for non-integers.
22:56:48 <cpressey> Well, if GHC is to Haskell as gcc is to C, ...
22:57:30 <alise> It's not, though? :P
22:57:33 <oerjan> haskell has three different power functions, dependent on whether the underlying type allows just multiplication, allows division, or allows general powers
22:57:41 <alise> oerjan: wait what's the third
22:58:30 <oerjan> you cannot implement the last one (**) cleanly for rationals
22:58:44 <pikhq> alise: Haskell 2010 is not a standardisation of GHC.
22:58:50 <alise> didn't even know of ^^
22:58:53 <pikhq> It's a standardisation of a handful of GHC extensions.
22:59:25 <oerjan> alise: it's defined for rationals, but it won't help you take cube roots alas
23:00:28 <cpressey> btw, is there some way to get Hugs to tell me what types implement a particular type class?
23:00:36 <alise> cpressey: Step one, don't use Hugs.
23:00:53 <cpressey> You're going to make me wait for all my crap to COMPILE, aren't you.
23:00:59 <oerjan> 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 <alise> Compiles on the spot, interactive like hugs.
23:01:14 <alise> Runs the program like a script interpreter.
23:01:38 <alise> Hugs doesn't even have the latest major version of the standard library, which changed quite a bit.
23:01:42 <cpressey> alise: OK, I'll give it a shot.
23:01:43 <alise> Does it even have 3?
23:02:04 <pikhq> Hugs is like... Dead.
23:02:18 <cpressey> alise: I'll give it a shot if it can tell me what types implement Integral.
23:02:28 <oerjan> cpressey: even ghc cannot do it without you having loaded the modules defining the type instances, i think.
23:03:08 <cpressey> Maybe I'll just stick to Visual Basic.
23:03:09 <oerjan> otoh the web documentation frequently lists types defining a particular class
23:03:22 <oerjan> although maybe that's module-dependent too
23:03:23 <cpressey> oerjan: I couldn't find it in the docs, that's why I was curious.
23:03:37 <cpressey> What, besides the various integery types, implement Integral?
23:03:53 <alise> Prelude> :info Integral
23:03:53 <alise> class (Real a, Enum a) => Integral a where
23:03:54 <alise> quot :: a -> a -> a
23:03:54 <alise> rem :: a -> a -> a
23:03:54 <alise> div :: a -> a -> a
23:03:55 <alise> mod :: a -> a -> a
23:03:55 <alise> quotRem :: a -> a -> (a, a)
23:03:55 <alise> divMod :: a -> a -> (a, a)
23:03:56 <alise> toInteger :: a -> Integer
23:03:56 <alise> -- Defined in GHC.Real
23:03:56 <alise> instance Integral Integer -- Defined in GHC.Real
23:03:57 <alise> instance Integral Int -- Defined in GHC.Real
23:03:59 <alise> (Sorry for the flood.)
23:04:02 <alise> Import more modules, get more Integrals.
23:04:14 <oerjan> cpressey: in addition to the standard Int and Integer, the Int* and Word* types from Data.Int and Data.Word
23:04:19 <alise> Of course you can't just say "import *" then look.
23:04:30 <oerjan> are the ones i know of
23:06:00 -!- scarf has quit (Remote host closed the connection).
23:07:49 <oerjan> cpressey: http://www.haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html has a sizable list a way down
23:08:23 <oerjan> http://www.haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#7
23:08:39 <oerjan> is the closest anchor i could find
23:08:45 <cpressey> haskell.org is not responding for me, lovely
23:09:08 <oerjan> oh? i just brought it up
23:11:30 <oerjan> i guess most of those are for the ffi, lots of C types
23:12:26 <oerjan> and of course those are at most the instances that come with ghc. other packages can define their own.
23:12:34 <alise> I finally made a channel for my system/language/thingy. #usys
23:20:27 <oerjan> 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:21:34 -!- Asztal has joined.
23:22:08 -!- Azstal has quit (Ping timeout: 245 seconds).
23:22:11 <oerjan> 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 <oerjan> *from two overlapping areas
23:23:08 <oerjan> this is probably enough to get a logical inconsistency
23:24:47 <oerjan> 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 <oerjan> 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:29:20 -!- dev_squid has quit (Ping timeout: 246 seconds).
23:30:47 -!- dev_squid has joined.
23:35:52 -!- Oranjer has left (?).
23:46:41 -!- angstrom has joined.
23:51:09 <oerjan> !haskell data Nat nat = Succ nat deriving Show; main = print . Succ . Succ . Succ $ "Test"
23:51:19 <EgoBot> Succ (Succ (Succ "Test"))
23:52:02 <oerjan> alise: your Show instance for Nat back when was just the usual derived one
23:53:41 <oerjan> or almost. it left out the parentheses around "Test".
23:53:54 <oerjan> alise: because you didn't notice it?
23:54:06 <alise> well i was being careful :)