00:00:07 Brb 00:00:11 -!- FireFly has quit ("Later"). 00:00:15 -!- Slereah_ has joined. 00:11:45 * Sgeo doesn't get Banks 00:12:27 i think it's a cultural thing 00:12:49 I meant in Golly 00:13:12 way to ruin my pun 00:15:39 -!- Slereah has quit (Read error: 110 (Connection timed out)). 00:39:11 oerjan: i like you pun. :| 00:40:14 * oerjan does a happy dance 00:53:08 -!- oerjan has quit ("Good night"). 01:04:05 -!- GreaseMonkey has joined. 01:12:11 -!- Corun has quit ("This computer has gone to sleep"). 02:55:28 EVERYBODY DO THE R M R F SLASH DAAAANCE 03:09:24 -!- Dewio has changed nick to Dewi. 03:24:07 -!- psygnisfive has quit (Remote closed the connection). 03:38:59 -!- psygnisfive has joined. 05:19:05 -!- chuck has quit ("Reconnecting"). 05:19:08 -!- chuck has joined. 05:23:45 -!- bsmntbombdood has quit (Read error: 110 (Connection timed out)). 05:25:14 -!- bsmntbombdood has joined. 07:00:53 Bye all 07:01:09 -!- Sgeo has quit ("Leaving"). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 09:19:07 -!- GreaseMonkey has quit ("Client Excited"). 10:06:41 -!- oerjan has joined. 10:11:47 omgwtfxkcd 10:19:00 o.o; 10:19:07 its uh.. slightly.. stupid. 10:19:15 and by slightly i mean very. 10:19:27 and by very you mean enormously. 10:31:25 cool 10:31:26 let's see 10:33:09 let's drink and sing and do the hokey pokey 10:34:41 okay not loading is not very funny, i admit it. 10:35:05 positively a 1 on the scale 10:37:35 on what scale? C, R, N? 10:37:58 oh my connection is local only, no wonder i can't access the nets.. 10:38:11 que 10:38:31 it's a numeric scale. 10:38:44 you'd think if the mirc dude can write a strong ai to converse with me, he'd also manage to make it check whether i'm online. 10:38:49 it goes up to either 9, or 10. 10:39:00 i mean of course i notice if it keeps talking to me even when i'm offline. 10:39:09 or possibly 6, if you're in norway 10:40:47 btw could someone network-knowledgeable tell me why exactly i can always irc even when my internet is down? probably vista's just lying to me ofc. 10:40:50 also i'm not an AI, i'm a platonic ideal and you are really sitting in a cave, watching shadows. 10:41:11 i always found that comparison kinda stupid 10:41:42 no idea but recently IE has started acting up on me so i see a similar phenomenon 10:42:26 it's weird, after i close all IE windows it won't connect again, until i restart the machine 10:43:57 also it takes a while having the windows open before it happens on closing 10:44:17 -!- oklofok has joined. 10:44:29 can you connect with anything other than irc/http? 10:44:31 i thought the xkcd was okay. 10:44:38 and i disconnected 10:44:39 also, did you hear anything i said? 10:44:42 resay everything you said 10:44:48 ARGH 10:44:52 :DDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD 10:45:06 i take that as a sign it was stupid, and refuse :/ 10:45:21 k i'll read logs 10:45:29 since the only actual _advice_ was after you rejoined :D 10:45:35 -!- oklopol has quit (Read error: 60 (Operation timed out)). 10:46:49 i disconnected because i flipped the switch on and off 10:46:50 i _suspect_ my virus scanner, since it happened after an update of it that coincidentally made it work properly in other ways 10:47:30 suspecting is a sign of having a hunch 10:47:31 otoh there were some Windows security updates too, when i think about it. 10:48:07 so what was so bad about pep talk? 10:48:24 it was a *groan* kind of joke 10:48:41 hmm, k 10:50:41 much better than any kind of pun could ever be imo, and xkcd has had those 10:50:55 puns are a lesser category of jokes 10:51:01 i _thought_ it had something to do with a full virus scan bringing my laptop nearly to its knees, but yesterday it happened again even though i have turned off the automatic scheduling 10:51:13 of course it's kinda stupid he explains it 10:51:24 * oerjan swats oklofok viciously -----### 10:52:02 he could've more like boosted his talk, now we *really* need to start playing 10:52:13 vicicivicivi 10:52:38 is icv tc 10:52:40 yeah a bit of that british understatement thing 10:52:47 what is icv 10:52:53 ``icv 10:52:56 veni vidi vici 10:53:11 err british understatement thing? 10:53:12 doubt it 10:53:28 less doubting, more proving! 10:53:37 the british invented understatements, surely 10:53:53 unless they stole it from the ancient romans 10:54:04 i don't know, as i cannot read jokes in latin 10:54:40 well lessee i recall adding i to subtle cough did not achieve much 10:55:04 don't recall checking it thoroughly 10:55:12 well seems you'd just end up building pipes, then using them to achieve nothing 10:55:16 if my intuition about i is right 10:55:25 i expect the same methodology to work though 10:55:52 there is no s, so no real duplication, so i suspect it's not tc 10:56:06 hmm trutru 10:56:22 could make a stronger claim: unlambda without s is probably not tc 10:56:37 less b more v! 10:56:57 but, umm, yeah, prolly 10:57:11 i just want my tc cough combinators 10:57:51 `ci = `i(*) = (*) = `cc iirc 10:59:20 ``cci = `(`*i)i = `ii = i 11:00:57 seems i need to find something to eat 11:01:16 hm the continuations mean applying i first need not be trivial 11:01:23 `ic = c ofc 11:01:52 but `i`cc = `i(`i*) = (`i*) 11:02:01 admittedly that's probably = (*) 11:02:18 ok applying i is still trivial 11:03:40 so 11:03:41 ``ccA 11:03:41 ``c(`*A)A 11:03:41 `(`*A)A 11:03:41 `AA 11:03:43 is this right 11:04:03 hmm 11:04:07 did you do just that 11:04:08 yes 11:04:10 heh :D 11:04:14 something like it 11:04:44 i always do that, i see you do something, but before i start thinking what it is, i get an idea, try it out, and realize i did what you did. 11:04:52 :D 11:05:14 and _still_ you don't believe in the subconscious ;D 11:05:19 i mean i invented your continuation syntax after not understanding how yours worked from taking a glimpse at it. 11:05:23 :P 11:05:33 i believe in *a* subconscious! 11:05:40 wait do i? probably not 11:06:26 so it seems adding i adds only i 11:06:44 `iv = `vi = v 11:07:30 `cv = `v(*) = v 11:08:24 `vA = v if A terminates without throwing a cont. 11:08:24 but so for any function f, `f`ci = `i(`f*) = (`f*), and `f`cc = `c(`f*) = `f(*), how are they are the same? 11:08:33 adding i adds only i? 11:09:06 to subtle cough that is 11:09:16 right 11:10:05 er `f`ci = `f(`f*) 11:10:26 assuming f is not a complex expression 11:10:46 umm ofc right 11:11:09 always forget the returning 11:12:22 ``ccv = `(`*v)v = `vv = v 11:12:26 continuations are a bit hard to analyze with syntactic transforms. 11:12:39 a tiny bit 11:12:41 they lack locality 11:13:15 the thing is when you apply an equation `cc = (*), you need to replace () by the continuation you put it in 11:14:15 hm so in theory you should not do that until `cc becomes the next term to evaluate 11:14:47 so you mean you need to have strict evaluation also in the rewriting? 11:14:52 yeah 11:15:10 with continuations, are there multiple normal forms? 11:15:29 i don't know 11:15:49 if not, are there infinite loops resulting from single missteps? 11:15:55 i don't know either. 11:16:18 is there actually any theory of combinators + continuations? i mean obviously it's goddamn fucking interesting. 11:16:51 well of course it would just be the theory of lambda calculus + continuations 11:16:56 but i haven't seen that theory either 11:17:28 well there is obviously a theory of lambda calculus + continuations, since that is known to have a curry-howard isomorphism with classical boolean logic 11:17:45 s/obviously // 11:18:15 oh. i see i see. 11:19:07 continuations allow you to extract the law of excluded middle 11:19:28 and what would that be? 11:19:40 A or not A 11:20:14 ah 11:20:55 or something like that. not not A => A is simpler 11:21:18 basically, not A is the type of a continuation that takes a value of type A 11:21:50 hm this is not clear at all 11:22:36 http://xkcd.com/380/ <<< i don't get this 11:23:04 oerjan: i know very little about CHI. 11:23:29 oerjan: basically, not A is the type of a continuation that takes a value of type A <<< i don't even get this. 11:24:08 that's a basilisk. if you look at a basilisk, you die. 11:24:40 if you see its face, or something 11:24:41 ohhh, i thought ":)" somehow indicated it was a snake :P 11:24:59 The "BSLSK" should've been a clue. 11:25:19 yes, but i read it as "old schoold" 11:25:21 *school 11:25:57 poll: does oklofok need a new monitor or new glasses? 11:26:11 A scary emoticon is the ":)" where the : character is in the bright color -- you know, :), or ^B:^B) -- but I think our +c mode filters that one out. 11:26:12 somehow ")" was the sex, it means a snake. i have no idea how, also ":" was its age, it was a two-year-old snake 11:26:26 but something still bugged me about it... 11:27:27 on the internet, no one knows you are a basilisk. until it is too late. 11:28:52 oerjan: i read "bslsk", i just thought it was a shorthand for "old school", kinda like ":)" is short for two year old snake... :) 11:29:30 `v`cc = `v(`v*) = v 11:30:09 i think that pretty much nails it 11:30:57 maybe so. 11:31:47 what's ``scc? 11:32:02 missing an argument 11:32:58 yeah but X reduced, where X is the reduction that's about behavios. 11:32:59 *behavior 11:33:06 eta 11:33:22 so they were A B E? 11:33:35 yeah 11:33:41 A being the nothing, E being the behavior, B being umm evaluation? 11:34:08 i have no clue why those were chosen 11:34:20 well at least the E 11:34:36 import threading 11:34:38 import time 11:34:41 import sys 11:34:42 class InputThread(threading.Thread): 11:34:44 def run(self): 11:34:46 while True: 11:34:58 beh.... I need to type /sp to make it stop 11:34:58 ```sccf = ``cf`cf = ``f(`*`cf)`cf 11:35:24 oerjan: so it's kinda duplication? 11:36:00 well s does that 11:36:14 yes, but i mean call that C, is it tc? :D 11:36:48 you seem i'm trying to come up with supercough, but since i've failed myself, i'm using you to do the actual thinking. 11:36:53 *you see 11:37:18 now that is a recipe for disaster 11:37:21 so if i come up with it, it's still my idea, you're just the program i used to do the testing. 11:37:27 maybe so :) 11:38:07 what do you mean "call that C" 11:38:17 oerjan: well have that as the only combinator 11:38:25 ah. 11:38:48 well applying it to itself for a start... 11:39:26 i mean in general, do continuations add any kind of computational power 11:39:47 is there a non-tc set of combinators such that adding call/cc makes them tc 11:39:56 well 11:40:06 actually that scc thing doesn't answer that, it's a bit different again 11:40:07 i would guess there is. but that doesn't necessarily say much. 11:40:15 it doesn't? 11:40:21 oh your guess doesn't 11:40:25 well true, it doesn't. 11:40:40 actually i wasn't talking about my guess 11:40:54 oh 11:41:03 then what do you mean, i mean that would be awesome. 11:41:10 so it does say something 11:41:22 i mean you can make convoluted things that just miss a little piece to be tc, that doesn't really say much about the power of the missing piece 11:42:04 it says something about its power 11:42:26 or well at least the lack thereof does 11:43:13 ```scc``scc = ``c``scc``c``scc 11:43:32 er 11:43:36 ```scc``scc = ``c``scc`c``scc 11:44:59 = ````scc(`*`c``scc)`c``scc 11:45:09 _maybe_ 11:46:17 = ```c(`*`c``scc)`c(`*`c``scc)`c``scc 11:46:51 well that's just sick. 11:47:07 hm we have a subproblem of `c``scc in there 11:48:13 `c``scc = ```scc(*) = ``c(*)`c(*) = ``(*)(`*`c(*))`c(*) 11:48:23 now that was an immense improvement 11:49:06 yes, superficially speaking 11:49:22 11:49:22 i can't say i still actually *understand* these expressions. 11:49:32 i think it looks prettier :) 11:50:50 oh wait of course that simplifies at the next step, it throws a continuation :) 11:51:05 `c``scc = ```scc(*) = ``c(*)`c(*) = ``(*)(`*`c(*))`c(*) = (`*`c(*)) 11:51:24 yes 11:51:53 now substitute that in 11:53:03 ```scc``scc = ``c``scc`c``scc = `(``*`c(*)`c``scc)`c``scc i hope 11:53:29 haha 11:53:41 okay that looks kinda nice :) 11:53:59 the next step is to do the same to the second part 11:55:19 oh wait 11:55:47 that's wrong, i didn't adjust the (*) 11:56:38 ```scc``scc = ``c``scc`c``scc = `(``*`c(`*`c``scc)`c``scc)`c``scc 11:56:58 you do realize you could just run a few steps in an unlambda interp? i guess they wouldn't show the continuations though 11:57:12 indeed they wouldn't 11:57:22 i have one that does, apart from the actual combinators, but they could be added in a minute 11:57:43 of course i don't actually have it anymore, lost a lot of shit when my hd died. 11:59:20 one point, maybe it would be worth checking if it actually terminates :D 11:59:53 but would that actually tell no expressions involving it do? 11:59:54 ouch it seems not 12:00:00 it would at least strongly hint it 12:00:10 the problem is even that doesn't necessarily say it's not tc :P 12:00:25 would be so much easier if i was less dumb. 12:00:36 um it really does 12:00:36 i could just answer my questions myself 12:01:00 oerjan: no not really. it could do useful computation, then always hit somekinda trivial loop afterwards. 12:01:39 erm _every_ subexpression of the form ```scc``scc will not terminate if ever evaluated 12:02:08 and you cannot do anything in this language that doesn't start with just that 12:02:10 well that does say it's not tc. 12:02:55 but i meant that subexpression could've used the upper continuation in its nonterminating loop, and somehow done computation anyway 12:03:02 I HAVE NO IDEA 12:03:57 oh of course ``cA`cB is a well-known construction in unlambda, someone was playing with it just the other day, it tends to create infinite loops 12:04:50 someone where? 12:04:56 here on channel 12:05:29 i see i see, i've been a bit offline. 12:05:35 whoever made that unlambda bot 12:05:44 ehird i think 12:05:50 well he made an unlambda interp 12:05:53 so... 12:06:57 anyway if an expression does not contain an embedded continuation, then it initially has access only to its containing one 12:07:30 makes sense. 12:07:43 which means even if it _does_ throw a continuation, it will end up looking like a normal return from the outside 12:08:12 so if it doesn't terminate, it cannot interact with the outside at all 12:08:39 finally the monkey catches the titanium ball 12:08:47 i'm convinced 12:08:51 i should eat something now 12:09:41 * oerjan was briefly wondering if that was a weird metaphor or if you were playing some game on the side 12:10:02 Which one was it? I'm still wondering. 12:10:03 both, i'm playing the game with you 12:17:33 okay 12:17:35 seriously 12:17:37 i'm gonna go now 14:01:00 -!- oerjan has quit ("Cibus"). 14:16:53 why isn't my quicklog playing 14:17:17 -!- ehird has changed nick to ehird|away. 14:17:26 -!- ehird|away has changed nick to ehird. 14:19:31 aha 14:22:32 i conclude miau sucks dicks 14:22:35 multiple dicks 14:27:35 04:03:57 oh of course ``cA`cB is a well-known construction in unlambda, someone was playing with it just the other day, it tends to create infinite loops 14:27:36 yeah, me 14:27:55 ```ci`c.ai prints a forever 14:28:05 ``ci`cX = infinite Xs :D 14:28:12 Noooooooooooo 14:28:18 what 14:35:05 INFINITY 14:35:59 ya 15:01:17 -!- FireFly has joined. 15:02:12 -!- BeholdMyGlory has joined. 15:17:37 http://dobbscodetalk.com/index.php?option=com_myblog&show=Porting-D-to-the-Mac-Pt.-3.html&Itemid=29 15:17:40 finally 15:22:13 On a Macintosh monitor, the notional resolution is 72 dots-per -inch 15:22:13 But on a Windows monitor the resolution is (usually) 96 dpi 15:22:16 how things change 15:24:04 -!- MigoMipo has joined. 16:24:01 -!- Corun has joined. 16:31:34 so, who's alive 16:41:31 oklofok 16:47:46 :< 16:58:22 * ski__ is not alive 16:58:40 -!- BeholdMyGlory has quit ("bye"). 16:58:42 yay 16:58:43 :P 17:05:30 loeb : forall u : U. Bew (imp (bew u) u) -> Bew u 17:11:05 loeb loeb loeb loeb 17:11:16 loeb is the essence of computing loeb. 17:12:48 who here's used llvm? 17:18:47 loeb is a quite stange theorem 17:19:07 -!- ais523 has joined. 17:19:20 It is loebelicious, clearly. 17:19:45 "Assuming you'd believe that if you believe a statement, then that statement is true. Would you then believe the statement was true ?" 17:19:48 -!- Sgeo has joined. 17:20:18 (for any specific "statement" you like to consider) 17:20:31 Undefined, because that's a recursive definition 17:20:34 no? 17:20:37 wrong ! 17:20:48 loeb's theorem is *provable* 17:21:09 weird. 17:21:21 it seems like you can't unwrap the belief to truth without assuming that, no? 17:22:16 (given a suitable interpretation of "believe" .. here "you" can e.g. be the formal system of Peano Arithmetic, and "believe" means that Peano Arithmetic can prove that Peano Arithmetic can prove the statement) 17:22:36 ah. 17:23:54 * ski__ is interested in finding computable interpretations of loeb's theorem 17:24:19 (i.e. as a programming function) 17:25:20 exists, I'm pretty sure 17:25:32 http://blog.sigfpe.com/2006/12/tying-knots-generically.html 17:25:37 > loeb :: Functor a => a (a x -> x) -> a x 17:25:38 > loeb x = fmap (\a -> a (loeb x)) x 17:25:40 loeb loeb loeb loeb loeb 17:25:41 hi ais523 17:25:57 hi 17:27:07 -!- BeholdMyGlory has joined. 17:28:51 ehird : yes, that's something like what i want 17:29:06 the "only" trouble with that is that it's inconsistent 17:29:43 loeb [(\[x,y] -> y),(\[x,y] -> x)] 17:29:45 will diverge 17:30:25 i want interpretations which will terminate (or be productive, if codata), given terminating (productive) inputs 17:33:14 ski__: specialize it on just functions? 17:33:18 loeb :: a -> ((a -> x) -> x) -> a -> x 17:33:26 err 17:33:30 loeb :: (a -> ((a -> x) -> x)) -> a -> x 17:33:41 -!- Deewiant has quit (Read error: 131 (Connection reset by peer)). 17:34:18 -!- Deewiant has joined. 17:36:30 loeb (\() f -> f ()) () 17:36:35 would diverge, too 17:38:06 ski__: "Assuming you'd believe that if you believe a statement, then that statement is true. Would you then believe the statement was true ?" <<< is there something paradoxical i'm missing here? 17:38:52 -!- sebbu2 has joined. 17:39:02 oklofok: if you believe something, do you necessarily believe you believe it? 17:39:31 or can people be mistaken about what they believe? 17:39:33 ais523 : yes, that's also a good question (but not what `loeb' above is about) 17:39:45 oklofok : depends on whether you've found anything paradoxial 17:40:41 believing is when you've decided to hold something as true. 17:41:10 therefore by definition if you believe, you believe you believe. 17:41:25 of course this might not be a definition suitable for everyone, i just hate philosophy. 17:41:36 hmm, should probably join #philosophy again 17:41:43 17:42:10 8| 17:42:16 holy shit that's hot stuff :D 17:42:23 Conceited reasoner^[1]^[4]: A reasoner is conceited, if they believe they are never inaccurate. A conceited reasoner will necessarily lapse into an inaccuracy. 17:42:44 Peculiar reasoner^[1]^[4]: A reasoner is peculiar if there is some proposition p such that they believe p and also believe they don't believe p. Although a peculiar reasoner may seem like a strange psychological phenomenon, a peculiar reasoner is necessarily inaccurate but not necessarily inconsistent. 17:42:48 wtf finnish dude mentioned on page 17:43:21 ski__: try coming up with a good type for it, then using lambdabot's @djinn? 17:43:39 (also obviously .. see also stanford's encyclopedia of logic) 17:44:03 hmm 17:44:09 []([]P->P)->[]P 17:44:11 Unstable reasoner^[1]^[4]: A reasoner is unstable if there is some proposition p they believe that they believe p, but don't really believe p. This is just as strange a psychological phenomenon as peculiarity, however, an unstable reasoner is not necessarily inconsistent. 17:44:25 -!- sebbu3 has joined. 17:44:31 I'll consider [] a box because it looks like one 17:44:41 yes, that's loeb's rendering in Provability logic 17:44:46 (a -> ((a -> p) -> p)) -> a -> p 17:44:51 yeah that's my specialized loeb 17:45:02 * ski__ has been reading "The Logic of Provability", by George Boolos, recently 17:45:23 they believe p but don't really believe p? 17:45:32 what's "really"? 17:45:41 i want to interpret `[] a' as code representing an expression of type `a' (that you can pattern-match on) 17:45:59 ski__: well, that's a think 17:46:02 *thunk 17:46:06 [] a would be () -> a 17:46:07 oklofok : no "they believe that they believe p, but don't really believe p" ! 17:46:21 ski__: omit really 17:46:25 ([] [] p) /\ (not [] p) 17:46:30 believe (believe p) & (not (believe p)) 17:46:51 no, code is not thunks 17:47:03 ski__: oh, "...some proposition p so that they..." 17:47:09 i misparsed it 17:47:12 `eval' in lisps doesn't operate on thunks 17:47:41 that's kind of detail-y 17:47:52 ski__: TH? 17:47:53 -!- ais523 has quit (Connection reset by peer). 17:47:58 if i interpret `[]' as "code of", then one proof of loebs theorem i've seen really appear to be almost 17:48:08 [template haskell that is] 17:48:16 -!- ais523 has joined. 17:48:20 ((lambda (lambda) `(,lambda ',lambda)) (lambda (lambda) `(,lambda ',lambda))) 17:48:32 (which i hope you recognize ..) 17:48:38 that variable name obfuscation is a bit intellectually dishonest :P 17:48:51 ((lambda (x) `(,x ,x)) (lambda (x) `(,x ,x))) 17:49:00 yes, same thing 17:49:14 er, actually i forgot an ' 17:49:22 ((lambda (x) `(,x ,x)) '(lambda (x) `(,x ,x))) 17:50:01 (if you want, i can remove the "almost" in the above statement ..) 17:51:03 (ehird : better than TH would be MetaML or MetaOCaml) 17:51:12 ew, why 17:51:22 TH is ugly 17:51:45 and from what i know, doesn't allow cross-stage persistance or anything similar 17:52:13 (also, TH is dynamically typed) 17:52:55 dynamically typed can be fixed 17:53:01 type Box a = Q 17:53:19 but possibly not without doing violence to the existing system 17:53:31 then use (Box a) to mean "code evaluating to something of type a" 17:53:38 (which wouldn't necessarily be a bad thing ..) 17:56:18 how do i express (lambda (x f) `(lambda (y g) ,(f (lambda (z) `(g x `z))))) in TH ? 17:56:27 -!- sebbu has quit (Connection timed out). 17:56:28 -!- sebbu3 has changed nick to sebbu. 17:56:41 ski__: not sure :-D 17:56:44 ( usuing lispy syntax for (hopefully) familiarity) 17:56:46 ask #haskell? 17:57:14 -!- ais523_ has joined. 17:57:16 note that e.g. `x' is bound outside the quasi-quote, but used inside it 18:00:32 * ski__ thinks he would better sink into misty magic land atm, though .. 18:01:54 ski__: unfortunately, it looks like `eval :: Box a -> a` would be Difficult(TM) 18:02:02 since you can get back an ast, but you'd need to use the ghc api to compile & run 18:02:44 -!- kar8nga has joined. 18:03:39 (.. that might not bad that bad, considering that if `[] a -> a' is provable, then the system would be inconsistent, because of loeb) 18:03:50 (s/bad/be/) 18:03:58 true 18:04:08 ski__: you 18:04:14 'd need lots of magic anyway 18:04:20 to turn whatever ghc gives you into a value 18:05:02 -!- ais523 has quit (Nick collision from services.). 18:05:04 -!- ais523_ has changed nick to ais523. 18:06:04 -!- Slereah has joined. 18:10:40 ski__: actually, [] a -> a is provable with functions and functors 18:10:47 \f -> f undefined 18:10:57 ofc, undefined being provable makes everything provable... 18:11:41 -!- sebbu2 has quit (Connection timed out). 18:12:58 [18:12:45] @djinn a -> ((a -> p) -> p) -> a -> p 18:12:58 [18:12:46] -- f cannot be realized. 18:13:04 dun dun 18:13:31 -!- oerjan has joined. 18:14:35 i conclude miau sucks dicks 18:14:41 shush with your bestiality 18:16:15 -!- Slereah_ has quit (Read error: 110 (Connection timed out)). 18:17:13 -!- kar8nga has quit. 18:21:03 wtf finnish dude mentioned on page 18:21:25 this is of course a tremendous coincidence, given that there are only 5 finns or so 18:22:31 Bye for now all 18:22:50 you can check out any time you like, but you can never leave 18:23:09 -!- Sgeo has quit (Read error: 104 (Connection reset by peer)). 18:23:35 he succumbed to peer pressure 18:24:26 oerjan: my point almost to the word. 18:25:14 i'm not sure i believe that you believe that you believe that. 18:27:58 whee, using a ghc-style "Lazy value = function that calculates then replaces itself with trivial return" is only 0.00-0.02sec slower than "calculate once with normal func, then assign to variable" 18:27:59 using llvm 18:30:55 http://www.finerrecliner.com/?p=263 what the fuck. 18:36:47 oh oerjan 18:36:51 i forgot to tell you 18:37:02 I wrote an ski interp that almost works, and is lazy, and runs ```sii``sii without growing 18:37:09 how? 18:37:14 optmization? 18:37:22 "garbage collection" 18:37:22 reduce :: SKI -> SKI reduce (App (App (App S x) y) z) = App (App x z) (App y z) reduce (App x y) = gc (App (reduce x) y) reduce x = gc x gc :: SKI -> SKI gc (App (App K x) _) = x gc (App I x) = x gc (App x y) = App (gc x) (gc y) gc x = x 18:37:27 er 18:37:44 reduce :: SKI -> SKI; reduce (App (App (App S x) y) z) = App (App x z) (App y z); reduce (App x y) = gc (App (reduce x) y); reduce x = gc x; gc :: SKI -> SKI; gc (App (App K x) _) = x; gc (App I x) = x; gc (App x y) = App (gc x) (gc y); gc x = x; 18:37:47 I think you can run ```sii``sii indefinitely lazily by optmizing `ix into x 18:37:57 it optimizes ``kxy too 18:38:03 in case you use skk instead of i 18:38:20 -!- kar8nga has joined. 18:38:21 ehird: I think you're independently from me discovering the Underlambda evaluation order 18:38:23 ah, I think I know why it doesn't work 18:38:25 fixx'd 18:38:29 which is "strict or lazy, whatever you like", for most operations 18:38:30 turn the s thing into 18:38:30 reduce (App (App (App S x) y) z) = gc (App (App x z) (App y z)) 18:38:31 ais523: isn't that what he does... 18:38:34 apart from things like I/O, which are always strict 18:38:54 oerjan: it pretty much runs a gc process on every step, eliminating `ix and ``kxy, while leaving ```sxyz to the "real" steps 18:40:19 ehird: you could make it more efficient by only gc'ing "one level", and do it while building App's, including during parsing. i think. 18:40:33 oerjan: define one leve 18:40:33 l 18:40:52 with my current gc, `````skkkik reduces to i in one step 18:40:54 i don't like that :< 18:41:00 it should just make one reduction at a time 18:41:03 i mean that when building App x y, then gc'ing, you can assume x and y are already gc'ed 18:41:11 no you can't 18:41:12 ehird: the same trick works with Underload, actually; if you leave : and S to evaluate in the proper order and just evaluate the others whenever you feel like 18:41:15 in 18:41:15 reduce (App x y) = gc (App (reduce x) y) 18:41:16 y isn't 18:41:24 you could do (gc y) though 18:41:33 the thing that : and ```sxyz have in common is that they're both needed to create loops 18:41:50 ehird: yes it is, assuming you do what i said and gc everything as you build it 18:42:14 s/said/meant/, possibly :D 18:42:17 oerjan: makes siisii reduce to siisii in one step 18:42:25 which breaks my "are we done" checker :D 18:42:32 and is also wrong 18:42:33 it should go 18:42:58 ```sii``sii -> ``i``sii`i``sii -> ```sii`i``sii -> ```siii``sii 18:43:03 that is, only one bit of progress at a time 18:43:46 huh 18:44:07 well, i'm just suggesting an alternate approach for the simplification thing 18:44:14 brb 18:44:50 yeah but who wants a tons more efficient algo 18:49:15 -!- Hiato has joined. 18:49:23 ais523: oerjan: relatedly, I've been thinking about hyper-optimization of lazy functional languages 18:49:39 (because I can't kick the urge to try and make a high level language finally faster than C, dammit.) 18:49:39 what's your plan? 18:49:48 ais523: very tangled. 18:50:24 i think static typing is needed, for e.g. arithmetic optimization 18:50:41 (to make inferrances like "we can represent 2+2 as a fixnum") 18:51:52 omfg. 18:51:53 http://cgi.ebay.com/Vintage-NextStation-Color-N1200-Computer-NEXT-SLAB-PC_W0QQitemZ110351324556QQcmdZViewItemQQptZLH_DefaultDomain_0?hash=item110351324556&_trksid=p3286.c0.m14&_trkparms=72%3A1234|66%3A2|65%3A12|39%3A1|240%3A1318|301%3A0|293%3A1|294%3A50 18:52:00 $24.99 NeXtStation 18:52:13 only to the us tho 18:52:18 better a nextcube too 18:52:27 still... sheesh 18:56:01 -!- sebbu2 has joined. 19:00:13 region lock-in eh? 19:02:09 -!- jix has joined. 19:03:10 no just shipping :P 19:04:18 i meant that in an extended sense 19:06:02 hi 19:06:16 hi ais523 19:06:38 hi in an extended sense, the letter M inside AnMaster's nick 19:07:32 mhm, I really need context to understand that, and atm I'm rather preoccupied in RL 19:07:39 -!- Slereah has quit (Read error: 110 (Connection timed out)). 19:08:04 ais523, so what was that about? 19:08:15 AnMaster: there is no context 19:08:22 it's just me being random 19:08:39 heh 19:08:51 so what do you mean with "in an extended sense"? 19:10:52 it means "in a sense you'll never find out because you won't read the half page just before you entered" ;D 19:12:40 -!- sebbu has quit (Connection timed out). 19:14:23 oerjan, how many lines do you define a page as? 19:14:44 * AnMaster makes his irc client 3 window 3 lines high 19:15:50 44 19:16:35 er wait, 43 19:16:46 forgot the upper topic line 19:17:11 oerjan, half a page would then start at " and is also wrong" 19:17:28 also, half a page was an overstatement 19:17:31 i meant that in an extended sense 19:17:37 heh 19:17:38 was the line I was referring to, which was the line before you said hi 19:17:41 it actually starts at omfg. 19:18:12 oerjan, that is because it scrolls down when you type and also long lines wrap 19:18:25 well duh 19:20:28 in case it is still not obvious, that was not intended as an accurate measurement 19:23:08 -!- ais523 has quit (Remote closed the connection). 19:24:31 FUNCTIONS ARE FUNCTIONAL 19:25:04 WHAT 19:25:08 LAMENT IS ON CRACK 19:25:38 REDUNDANCY IS REDUNDANT 19:25:49 ORANGES ARE ORANGE 19:26:14 PINKIES ARE PINK 19:26:29 -!- sebbu has joined. 19:26:59 COMPUTARS ARE COMPUTABLE 19:27:43 GREEN 19:28:28 COMMUNISTS ARE COMMON 19:28:41 GREEN -> APPLE -> TREE -> BINARY -> DIGIT -> PINKY -> PINK 19:29:36 Some apples are orange. But no oranges are apple. 19:29:44 [19:28:41] GREEN -> APPLE -> TREE -> BINARY -> DIGIT -> PINKY -> PINK 19:29:46 you could automate that 19:30:00 find word, grep dictionary for word, explore all possibilities with other words in same entries 19:30:06 until you find the word you want to connect to 19:30:12 I could automate you 19:30:15 no oranges need apply 19:30:26 but would you like that huh 19:30:37 yes 19:31:48 * lament replaces ehird with a small Python script 19:32:02 lament: da-da 19:32:41 lament: da. da 19:33:12 a small dadaist Python script 19:33:21 dadadada DADA! 19:34:38 lament: dada? :( 19:35:18 sniffle 19:35:21 lament: daa daa? 19:36:01 Gadji beri bimba 19:37:25 lament: ;_; 19:40:54 da, da, da da? 19:41:20 nyet 19:41:29 lament: dada dada 19:41:38 DADA 19:41:52 da... 19:42:04 -!- sebbu2 has quit (Connection timed out). 19:42:23 da 19:43:29 nyet! nyet nyet nyet! 19:45:47 setopt pushd_silent 19:45:47 alias cd=pushd 19:45:47 alias bk=popd 19:49:02 yes 19:49:27 -!- MigoMipo has quit ("QuitIRCServerException: MigoMipo disconnected from IRC Server"). 19:51:13 actually, 19:51:14 my_cd() { dirs=($(dirs)); if [[ ! -z $1 && $1 != $dirs[1] ]]; then pushd $*; fi } 19:51:14 setopt pushd_silent 19:51:14 alias cd=my_cd 19:51:14 alias bk=popd 19:51:15 ~ 19:54:54 -!- Corun has quit ("This computer has gone to sleep"). 19:57:01 sbcl is so hilarious 19:58:17 you can't compile it without a lisp 19:58:18 :D 19:59:16 you cannot compile ghc without a haskell, either... 19:59:21 GCC is so hilarious 19:59:26 in fact, without ghc 19:59:27 you can't compile it without a GCC 19:59:35 ... wait, that's not hilarious. 19:59:39 yes, but it's funnier with sbcl 19:59:41 because lol 19:59:49 * Despite all appearances, I am _not_ high. 20:00:27 could be a sugar kick 20:01:26 -!- sebbu2 has joined. 20:03:19 * ehird compiles sbcl with sbcl XD XD XD. 20:03:25 whee look at it go isn't it cute 20:03:29 yesss it is 20:08:13 probably with some added caffeine 20:08:49 i'll hold my opinion on the ginseng 20:10:57 blood sugar --> 20:12:16 -!- sebbu has quit (Read error: 110 (Connection timed out)). 20:12:17 -!- sebbu2 has changed nick to sebbu. 20:13:24 -!- Slereah has joined. 20:19:09 -!- Sgeo has joined. 20:31:34 -!- Hiato has quit ("Leaving."). 20:33:35 -!- ais523 has joined. 20:38:28 -!- ehird has changed nick to ehird|away. 20:47:55 -!- ehird|away has changed nick to ehird. 20:51:00 hello all! :D 20:56:17 Hi psygnisfive 20:56:26 hey 21:06:02 -!- MigoMipo has joined. 21:11:50 http://mirrors.dotsrc.org/congress/25C3/video_h264_720x576/ <- some interesting talks, and some information about each -> http://events.ccc.de/congress/2008/Fahrplan/events.en.html 21:23:01 -!- sebbu2 has joined. 21:28:59 -!- MigoMipo has quit ("QuitIRCServerException: MigoMipo disconnected from IRC Server"). 21:41:45 -!- ehird has changed nick to ehird|away. 21:41:51 -!- ehird|away has left (?). 21:41:53 -!- ehird|away has joined. 21:43:33 -!- ehird|away has changed nick to ehird. 21:49:42 -!- sebbu has quit (No route to host). 22:04:49 -!- sebbu has joined. 22:08:56 -!- sebbu2 has quit (Read error: 60 (Operation timed out)). 22:09:16 -!- BeholdMyGlory has quit (Remote closed the connection). 22:11:31 -!- Sgeo has quit ("Leaving"). 22:11:45 -!- kar8nga has quit (Remote closed the connection). 22:11:58 -!- Corun has joined. 22:24:04 -!- jix has quit ("..."). 22:42:31 -!- olsner_ has quit ("Leaving"). 23:09:20 -!- GregorR has quit ("Leaving"). 23:09:27 -!- GregorR has joined. 23:10:05 I just set xchat to use my godawful handwriting as its font. 23:10:11 It's not even slightly readable. 23:12:00 :-D 23:12:17 GregorR: W|at y0u saj 23:12:42 oerjan: Damn you. 23:13:10 -!- ais523 has quit ("http://www.mibbit.com ajax IRC Client"). 23:13:41 H0 OUPS1HC! 23:14:58 I have no idea what you just said. 23:15:10 http://i15.photobucket.com/albums/a379/GregorRichards/handwriting_xchat.png 23:15:12 H, zero, oh, you, pee, ess, one, heigh, cee. 23:15:16 Is what he said. 23:15:31 "Eighch" is spelled "eighch" 23:15:32 GregorR: You have some baseline issues there. 23:15:43 No, it's spelled "heich". 23:16:46 Bah not worse than that 23:16:55 ehird: Actually, it seems to be "aitch" :P 23:17:17 No it is heich. 23:17:39 also, that is so readable GregorR 23:17:42 you're just blind 23:17:52 ehird: EXAGGERATION FOR THE SAKE OF EMPHASIS 23:18:07 EMPHASIS FOR THE SAKE OF EMPHASIS. 23:18:24 REPETITION FOR THE SAKE OF REPETITION 23:18:51 also, that was supposed to indicate "NO CURSING" 23:18:57 Pronunciation /heɪtʃ/ and hence a spelling of haitch is usually considered to be h-adding and hence nonstandard 23:18:59 Wikipedia wins. 23:19:09 -!- Corun has quit ("This computer has gone to sleep"). 23:19:17 hadding haddocks 23:19:32 I don't care, it's wrong. 23:19:36 ardly hever appen 23:19:42 OK, but so's your face. 23:20:40 ÚÚÚÚÚÚÚÚÚ 23:20:42 ……………………………………………………… 23:24:21 fnörð 23:36:01 -!- fungot has joined. 23:36:41 Forgotteded completely about the botty-bot. 23:37:06 fizzie: forgotteded 23:37:35 fungot: please give fizzie some grammar lessons okthx 23:37:35 oerjan: you're from japan? :p) with the frame fnord?) 23:38:43 hai 23:38:51 i've been wondering about fizzie's grammar, did i give him that? 23:38:56 i mean i fonder words too 23:38:57 stor hvithai, to be exact 23:39:05 it's awesome, fizzie's language. 23:39:06 and we're both finnish 23:39:08 i see a connection 23:39:16 "them" to refer to a single object is my favourite part 23:40:03 oklofok: fonder 23:40:28 oerjan: fonder. 23:41:12 i do not believe that's a verb, either it's misspelled or you accidentally something 23:41:47 well you may have accidentally the context 23:42:22 but i completely your request to correct your errors from the other day 23:42:51 :o 23:42:54 sorry, i should have that. 23:43:16 hmm 23:43:52 and i haven't any opportunities before 23:44:23 i it now, i for so stupid. 23:44:47 ARGH 23:44:57 ;) 23:45:15 * oklofok it too far :< 23:45:15 proto: language where everything is a verb 23:45:18 kind of like haskell 23:45:26 natural language that is 23:45:32 want a value? make an unary verb. 23:45:35 oh kinda like english? 23:45:44 ermmmm english isn't all verbs :D 23:45:55 but, like, if you have a concept like "1" 23:45:58 maybe not from your point of view 23:46:02 1 = \f. f 1 23:46:06 or like 23:46:17 dog walks -> walks dog 23:46:22 or I don't know 23:46:31 i doubt anyone here does ;) 23:47:32 in lojban, every root word is a verb... but i guess you mean you could apply every subsentence as if it were a verb or something? 23:48:07 lalna kinda does that... it's kinda oklotalk but a natural language; also similar to oklotalk in that it's unfinished. 23:48:20 oerjan: how can you not have found grammar to correct? 23:48:22 i mean 23:48:31 i intentionally talk very, very confuzzlatorily 23:48:46 well 23:48:50 oklofok: You may have had some sort of influence on it, yes. 23:48:50 i guess i haven't done that then 23:49:17 fizzie: did you know your nick has a palindrome in it? 23:50:04 oklofok: well you've certainly started now 23:50:25 Although I think my in-query-talk with ineiros has also been some sort of a cause for my unstandardish speech patternsies. 23:50:41 oklofok: The "izzi" part? 23:50:50 no, the 'f' 23:51:02 [23:50:25] Although I think my in-query-talk with ineiros has also been some sort of a cause for my unstandardish speech patternsies. 23:51:05 does ineiros talk oddly? 23:51:20 Yes. 23:51:23 * oerjan should oddly oftener 23:51:25 [23:47:32] in lojban, every root word is a verb... but i guess you mean you could apply every subsentence as if it were a verb or something? 23:51:32 basically, eliminate adjectives, adverbs, nouns, ... 23:51:38 just have absolutely everything be a verb. 23:51:44 including compositions of verbs, yes 23:52:22 Would it be strange to use the term 'access violation' in other contexts than segfaults? 23:52:33 erm, no? 23:52:55 ehird: We do our query in less-than-regular Engrish, even though we both are these .fi types. Although now that I review some logs it seems I'm the odder one out. Curious. 23:53:14 fizzie: like vjn? 23:53:28 I imagine their engirsh is rather less comprehensible, though. 23:53:45 muchalainen 23:55:02 01:49… oerjan: oklofok: well you've certainly started now <<< ? 23:55:16 oklofok: give fizzie some vjnglish 23:55:29 :) 23:55:36 The vjn.fi en-fin translatomator made an awesome job of my randomly picked line; too bad you can't optimally enjoy it if you don't speak Finnish: "me aiheuttaa meidän kysyä -ssa less-than-regular Engrish, yhtäläinen vaikkapa me kummatkin ovat nämä .fi tekee malliesimerkki. vaikkakin välittömästi että meikä arvostella joku tekee runko sitä näyttäät olen moinen odder yksi esiin. omituinen." 23:55:37 no i'm shy 23:55:39 oklofok: vocabulatoriatingly at least 23:55:43 quick fool! 23:55:53 oklofok: come on vjnglish is awesome. 23:56:00 or should I say, an coolness. 23:56:16 sure an coolness to be saying 23:56:18 I'm starting to like WireWorld... 23:56:35 an arvostellar performance 23:56:48 f00d -> 23:56:57 <- bed 23:57:01 * oerjan swats FireFly first -----### 23:57:02 what 23:57:03 it's -> 23:57:04 not <- 23:57:07 :< 23:57:07 THAT ISN'T POSSIBLE 23:57:10 v bed 23:57:10 BED IS NOT GOING TO YOU 23:57:12 <- in bed 23:57:13 ^ bed 23:57:23 * oklofok is always in his bed :| 23:57:36 Bed walks to oklofok 23:57:48 That last one just looks lik "/me exclusive-or bed". 23:57:56 Which reminds me, I need sleep too; night. 23:58:08 Yeah, me too 23:58:10 -!- FireFly has quit ("zzzzzzzzz"). 23:58:24 good night to the effers. 23:58:39 or wait are they zeers 23:59:10 also both have palindromes in their nicks, you have a lot in common.