00:00:17 plash is better than you. 00:00:24 Or something :P 00:03:24 Yay, just got HOL Light installed (under cygwin...) and proved something with it 00:04:03 Someone should make Plash for Windows 00:09:37 Sgeo: No. 00:13:16 -!- adam_d_ has quit (Ping timeout: 265 seconds). 00:24:03 -!- augur has joined. 00:25:21 -!- cpressey has left (?). 00:30:21 -!- MigoMipo has joined. 00:35:57 -!- FireFly has joined. 00:36:16 -!- FireFly has quit (Read error: Connection reset by peer). 00:37:00 -!- FireFly has joined. 00:37:38 -!- FireFly has quit (Write error: Broken pipe). 00:40:29 -!- oerjan has quit (Quit: Good night). 00:57:40 wow 01:04:25 wiw 01:04:40 waw 01:09:41 wuw 01:10:08 wyw 01:11:30 wew 01:11:46 wfw 01:11:48 c-c-c- 01:11:57 COMBO BREAKER? 01:12:10 HAI GAIS 01:12:15 You could have continued using another semivowel, you know. 01:12:18 Like "yay". 01:12:33 waw, wew, wiw, wow, wuw, wyw, yay, yey, yiy, yoy, yuy, yyy... 01:12:52 After that, proceed to the stuff that's almost a vowel. rar, rer, rir, ror, rur, ryr. 01:13:07 Then other stuff that's almost a vowel: lal, lel, lil, lol, lul, lyl. 01:13:22 And then some nasals: nan, nen, nin, non, nun, nyn, mam, mem, mim, mom, mum, mym. 01:33:30 erm 01:34:03 mer 01:34:04 rem 01:34:28 Wow. http://to./ 01:34:35 It's a URL shortener. 01:37:12 how is this even possible 01:37:25 to is a TLD 01:37:32 For some country 01:37:41 Some country clever enough to make the greatest URL shortener ever. 01:37:57 Also, http://to/bleh works the same if your OS doesn't suck. 01:38:23 but why the dot at the end 01:39:18 I've recently been reminded that that's always been the correct canonicalization, since the beginning of DNS (this is why BIND wants your hostnames to end in a .), not having a . is just a convenience. 01:42:16 why i cannot visit pl. or com. then? 01:43:28 com. does work, although it forwards to www.com. 01:43:36 pl. also works 01:43:58 Oh, sorry, my confusion, lemme restate: 01:44:05 bah 01:44:11 i see it does noe 01:44:14 com and pl don't have A addresses, they have no host. www.com. does work, as does www.pl. 01:44:44 com. doesn't work for the same reason that com doesn't work, because the gigantulous company that controls the com TLD doesn't have any address there. 01:44:48 Same with pl 01:47:10 wonder who controls it 02:04:57 -!- MigoMipo has quit (Quit: Page closed). 02:07:32 In zone files, domain names ending in . are absolute and domain names not ending in . are relative. 02:08:25 So if your domain name is foo.com., adding an A record for blah.foo.com. will make http://blah.foo.com/ go somewhere, and adding an A record for blah.foo.com will make http://blah.foo.com.foo.com/ go somewhere. 02:09:22 -!- Asztal has quit (Ping timeout: 276 seconds). 02:14:17 -!- nooga_ has joined. 02:17:36 -!- nooga has quit (Ping timeout: 252 seconds). 02:55:47 -!- FireFly has joined. 02:56:11 -!- FireFly has quit (Read error: Connection reset by peer). 02:56:47 -!- FireFly has joined. 03:15:36 -!- FireFly has quit (Read error: Connection reset by peer). 03:16:29 -!- FireFly has joined. 03:17:00 -!- FireFly has quit (Read error: Connection reset by peer). 03:17:37 -!- FireFly has joined. 03:18:11 -!- FireFly has quit (Read error: Connection reset by peer). 03:21:14 -!- kwertii has joined. 03:30:39 -!- werdan7 has quit (Ping timeout: 615 seconds). 03:39:01 -!- werdan7 has joined. 03:52:30 burp 03:53:08 uorygl: i see 03:53:22 code red! quarantine broken! 03:54:20 wha.... 03:54:22 * uorygl dons a gas mask. 03:54:23 oh 03:54:29 * uorygl wraps nooga_ in plastic. 03:54:45 mmffgffgf 03:54:54 * uorygl pokes breathing holes in the plastic. 03:55:01 hhhhhhh 03:55:07 * uorygl pokes speaking holes in the plastic. 03:55:17 hm 03:55:29 * uorygl pokes speaking articulately holes in the plastic. 03:55:32 that would actually make the plactic wrap pointles 03:55:38 Indeed. 03:55:45 * uorygl wraps the holes in plastic. 03:55:46 There! 03:56:09 mmfgm. 03:56:36 Hey, now. The holes still exist, so you can still breathe and speak and speak articulately through them. 03:56:54 But they're also wrapped in plastic so no contaminants can get out. 03:56:56 Genius, eh? 04:03:54 heh 04:04:18 wait a second 04:06:16 isn't france in the same time zone with warsaw? 04:06:22 i mean paris 04:06:55 night coding huh? 04:08:49 -!- jcp has joined. 04:33:17 -!- augur has quit (Ping timeout: 265 seconds). 04:33:43 * pikhq notes that alise hasn't been around for a few days 04:46:28 -!- Libster has joined. 04:46:30 -!- Libster has left (?). 05:17:48 -!- augur has joined. 05:25:37 -!- nooga_ has quit (Quit: Lost terminal). 05:32:25 -!- Oranjer has left (?). 05:35:59 -!- FireFly has joined. 05:36:20 -!- FireFly has quit (Read error: Connection reset by peer). 05:51:29 -!- coppro has joined. 05:59:25 -!- coppro has quit (Remote host closed the connection). 06:01:48 -!- coppro has joined. 06:12:26 -!- adu has joined. 06:29:02 -!- MigoMipo has joined. 07:42:58 -!- adu has quit (Quit: adu). 07:46:10 -!- adu has joined. 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:01:34 -!- kwertii has quit (Quit: bye). 08:18:03 -!- cheater2 has quit (Ping timeout: 240 seconds). 08:22:00 -!- cheater2 has joined. 08:36:18 -!- BeholdMyGlory has joined. 08:40:07 -!- adu has quit (Quit: adu). 09:32:42 -!- BeholdMyGlory has quit (Remote host closed the connection). 09:57:11 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 10:21:13 -!- oerjan has joined. 11:12:42 -!- fax has joined. 11:15:06 -!- kar8nga has joined. 11:24:53 -!- sebbu has quit (Ping timeout: 256 seconds). 11:36:17 -!- sebbu has joined. 11:37:52 -!- fax has quit (Quit: Lost terminal). 11:43:32 -!- tombom has joined. 12:06:20 -!- oerjan has quit (Quit: leaving). 12:36:16 -!- cheater has quit (Read error: Operation timed out). 12:36:40 -!- cheater has joined. 12:40:58 -!- adam_d has joined. 12:54:01 -!- fax has joined. 13:00:54 -!- adam_d has quit (Ping timeout: 258 seconds). 13:28:48 -!- lifthrasiir has quit (Ping timeout: 276 seconds). 13:42:42 -!- MigoMipo has quit (Quit: Page closed). 13:43:04 -!- BeholdMyGlory has joined. 13:49:26 -!- lifthrasiir has joined. 13:51:51 -!- Phantom_Hoover has joined. 13:52:26 If I have a raw Qemu disc image, how do I format an ext3 filesystem on it? 13:55:14 -!- lifthrasiir has quit (Quit: leaving). 13:55:27 Well? 13:55:33 -!- lifthrasiir has joined. 14:01:53 ill 14:03:52 -!- BeholdMyGlory has quit (Remote host closed the connection). 14:06:22 ?? 14:10:10 -!- cheater2 has quit (Ping timeout: 245 seconds). 14:11:24 -!- cheater2 has joined. 14:30:45 -!- Phantom_Hoover has quit (Ping timeout: 256 seconds). 14:31:49 -!- kar8nga has quit (Remote host closed the connection). 14:39:00 Just mkfs.ext3 on it. 14:39:51 It might need the -F flag if it refuses to operate on a normal file, though I seem to recall it asking about it instead. 14:39:59 (Yes, I noticed he is gone already.) 14:50:00 What's the environment variable restriction in cfunge's sandbox mode useful for? 14:50:40 alise and/or ehird, when either of you show up: the intelligence squared debate on the catholic church as a force for good was simply amazing 14:59:37 ?? 15:04:07 theres this thing called Intelligence Squared 15:04:25 they held a debate last year on whether or not the catholic hcurch was a force for good in the world 15:04:44 and they subsequently had a vote of the people who were present for the debate 15:05:02 pre-debate, the numbers were like 1000 no, 700 yes, 300 dont know 15:05:06 after it was like 1750 no, 200 yes, 50 dont know 15:08:45 -!- alise has joined. 15:09:12 #alise, please. I do not want this to be logged. 15:10:29 augur 15:10:31 daahafh 15:16:28 -!- alise_ has joined. 15:20:50 -!- alise has quit (Ping timeout: 252 seconds). 15:26:20 -!- alise_ has quit (Ping timeout: 252 seconds). 15:26:53 -!- alise has joined. 15:26:56 06:21:54 I wonder how small one can make a decent forth compiler in C 15:26:58 http://www.ioccc.org/1992/buzzard.2.design 15:27:57 Compiler 15:28:59 -!- alise_ has joined. 15:31:28 -!- alise has quit (Ping timeout: 252 seconds). 15:32:18 o.o; 15:38:04 -!- alise_ has quit (Ping timeout: 252 seconds). 15:40:25 -!- alise has joined. 15:44:55 -!- jcp has joined. 15:49:04 -!- alise has quit (Ping timeout: 252 seconds). 15:55:30 -!- alise has joined. 15:56:10 * alise writes a program to generate true constructivist statements. 15:56:10 Endlessly 15:56:13 *Endlessly. 15:56:29 ?? 15:56:37 Why not? 15:56:52 It's just a case of having a bunch of axioms and then substituting things for the variables in them. Endlessly. 16:03:22 -!- alise has quit (Ping timeout: 252 seconds). 16:04:57 -!- fungot has quit (Ping timeout: 260 seconds). 16:05:54 -!- alise has joined. 16:14:33 -!- alise_ has joined. 16:14:44 -!- alise has quit (Ping timeout: 252 seconds). 16:15:05 fax: plz relink 16:15:05 in msg 16:15:26 hi 16:16:55 Please? 16:17:13 no 16:17:25 Por mi? 16:17:52 fax: Why not? 16:17:59 because nothing was said 16:18:15 -_-' 16:18:16 There was -- in #alise2. 16:18:22 At the beginning. 16:18:30 (In /msg only, please. I do not want it leaking) 16:19:07 -!- fungot has joined. 16:19:14 15:31 -!- alise [~95fee059@gateway/web/freenode/x-uykmcysttrftzukr] has quit [Ping timeout: 252 seconds] 16:19:18 15:31 < alise_> test 16:19:20 15:31 < fax> test 16:19:21 FFS. 16:19:24 I mean what I told you at the start. 16:19:25 -!- Phantom_Hoover has joined. 16:19:30 Hello? 16:19:31 In */msg only. Please.* 16:19:33 you want me to show you what you told me? 16:19:50 hi 16:20:08 fax: Yes. In /msg, in a private pastie. Please? 16:20:21 why 16:20:39 So I can show it to someone else... 16:20:41 Because this client doesn't log... 16:21:12 *... 16:21:53 -!- zzo38 has joined. 16:22:20 I thought about Conway's Life cellular automaton but I have idea for a variant, called KnightLife 16:22:23 Phantom_Hoover: In case your question is still relevant, just /sbin/mkfs.ext3 on it; at least my copy will ask about being sure to operate on non-block-device, but will do it after confirmation. 16:22:55 -!- sebbu has quit (Read error: Connection reset by peer). 16:23:10 -!- sebbu has joined. 16:23:42 Fizzie: thanks. 16:24:13 all (0 -> all (0 -> 1)); all all all ((0 -> (1 -> 2)) -> ((0 -> 1) -> (0 -> 2))); all all ((~0 -> ~1) -> (1 -> 0)) 16:24:57 Turns out I am a bit too lazy even to implement modus ponens. :) 16:27:42 -!- ais523 has joined. 16:30:43 -!- alise has joined. 16:33:48 -!- alise_ has quit (Ping timeout: 252 seconds). 16:34:09 ffff I hate trivial programming bookkeeping 16:34:24 I hate how I don't make much sense 16:34:31 even when I try really hard to 16:35:10 like consider 16:35:13 subst :: [(Integer,Statement)] -> Statement -> Statement 16:35:14 hi alise 16:35:18 I do bookkeeping in the first argument but you also specify what to subst in there 16:35:28 so when I come across a universal quantification 16:35:54 -!- alise_ has joined. 16:35:57 -!- Asztal has joined. 16:36:02 FUCK 16:36:04 THIS 16:36:06 FUCKING 16:36:07 CONNECTION 16:36:09 until it's fixed i'm not talking 16:36:12 zzo38: so, what does KnightLife do? 16:37:42 It wouldn't be Life with knightships added, would it? 16:38:00 That would be cute. 16:38:16 sdgjdfigjfdsoigx 16:38:21 rpghghrounprghounyphrguorpgh 16:38:31 phonographphonographphonograph 16:39:45 safkaspofksad 16:39:45 asfd 16:39:45 asl 16:39:45 das 16:39:45 dasd 16:39:47 a\sdl 16:39:49 a 16:39:50 f 16:39:50 sfdskf 16:39:50 [sdf 16:40:02 -!- alise has quit (Ping timeout: 252 seconds). 16:41:48 uorygl: I thought it is obvious, isn't it? If not, I will explain 16:42:38 Obvious from the name? 16:42:53 all (42 -> all (42 -> 1)) SAME FUCKING PROBLEM >_< 16:42:55 I hate coding 16:42:56 hmm interesting 16:43:04 Maybe it's a little bit obvious, but it's not very obvious. 16:43:10 alise: I hate programming too! 16:43:14 theres a subset of non-CF languages that have linear parse time 16:43:14 Yes, a little bit. 16:43:16 hm hm! 16:43:34 and their conveniently representable in compact regex-like notation! 16:43:35 Basically the 8 surrounding cells are the knight's move cells instead of the king's move cells 16:43:36 hm hm! 16:43:38 faxoh but I love programming 16:43:38 proper programming 16:43:44 not this fuking bookkeeping shit 16:43:45 with five bbillion variables 16:43:49 also fuck you chrome 16:43:53 show me the input field 16:43:56 Now it's obvious, isn't it? 16:44:10 * augur bookkeeps alise_'s variables 16:44:12 ;o ;o ;o 16:44:28 WOOT 16:44:33 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds). 16:44:59 Yep, now it's obvious. 16:45:18 -!- Phantom_Hoover has joined. 16:45:26 Same number of neighbors, but connected differently. Hmm. 16:46:24 asdfghj 16:47:01 pafdounafpoonufadpoundfapounadpfuondfpa 16:47:08 seriously what is it with shitty languages that can't match patterns and keep vaariables easily 16:47:23 i should be able to like.. modulo out that stuff to a separate block and write the rest uberpurely 16:47:26 "Pattern matching is hard!" 16:47:40 pikhq: not that kind of pattern matching 16:47:50 the kind of pattern matching that involves a recursive function to determine the OK-ness of a pattern 16:48:00 and then dispatching on the structure you infer in it 16:48:37 http://pastie.org/868022.txt?key=mqvjqn84rgv75aalq9arq 16:48:42 This function is 99% fucking fluff. 16:49:03 Now write modus ponens :: Statement -> Statement -> (Maybe) Statement. :-) 16:50:10 test 16:50:22 test 16:50:38 What is fax? 16:51:10 人間。 16:51:10 You cannot ask... what is fax. 16:51:11 It is not a question. 16:51:13 Instead, you mist ask.. 16:51:20 Why did I typo "mist" for "must"? 16:51:48 Then you will be enlightened. 16:51:48 Who is fax? 16:51:57 alise_: so what is this language, and why must you use it? 16:52:18 BUT WHO IS PHAX?! 16:52:46 uorygl: This is ... Haskell ... 16:52:58 fax is the bastard child of Miss Piggy and Kermit the Frog. 16:53:07 THIS 16:53:10 IS 16:53:12 HASKELL!!!!!!!!! 16:53:13 ファクス君が此処に居る人です。 16:53:28 saoidjdoifjsdojdsf 16:53:32 I'm I'm understanding you correctly, I'm slightly surprised that you're calling Haskell a shitty language that can't match patterns and keep variables easily. 16:53:34 THIS - IS - AN OUTDATED - MEEEEEEEEME 16:53:34 * fax bastard 16:53:35 I wish someone actually took u my challenge to write modusponens :P 16:53:36 (fax is a person who is hear) 16:53:36 s/I'm/If/ 16:53:39 *up 16:53:46 stop speaking japanese. 16:53:48 Gregor: :) 16:53:49 s/hear/here/ 16:53:51 uorygl: because I don't mean the trivial sense that haskell does 16:53:55 I mean generalised book keeping 16:53:59 http://pastie.org/868022.txt?key=mqvjqn84rgv75aalq9arq 16:54:04 2/3 parameters are bookkeeping 16:54:06 augur: 日本語を勉強する始めて。 16:54:12 the majoritry of the code. book keeping 16:54:14 (start studying Japanese) 16:54:19 if you try and code modus ponens inferrence using that, 16:54:25 you get EVEN MORE book keeping! yay 16:55:58 I think I'm turning Portuguese I think I'm turning Portuguese I really think so 16:56:45 So just what is subst supposed to do? 16:57:05 Substitute. 16:57:30 If the language excelled at eliminating pointless crap like that it'd be obvious from the definition. 16:57:35 Substitute what for what into what? 16:57:51 Substitute for a given De Bruijn index into a logical statement. 16:57:55 programming languages don't exist 16:58:06 THERE IS ONLY ZUUL 16:58:12 fax has spoken. 16:58:45 *XUL 16:58:52 *XML 16:58:55 (The XUL namespace file is one called there.is.only.xul; it says that. :)) 17:00:22 Okay, I think I see what this is all about. 17:00:22 -!- zzo38 has quit (Remote host closed the connection). 17:03:08 -!- alise_ has quit (Ping timeout: 252 seconds). 17:03:21 -!- alise has joined. 17:03:42 * alise installs xchat to avoid the shitty webchat client 17:05:05 uorygl: If you do decide to be my slave, the expectation of mp is that `mp (Var n :-> q) p'` produces q with p substituted for Var n (note that if you hit an All, all existing variables are shifted one place, and 0 becomes the newly-quantified variable); `mp (Not p :-> q) (Not p')` does the same but with the obvious, and `mp ((p :-> r) :-> q) (p' :-> r')` check that p/p' and r/r' match and then does the same as the others. 17:05:20 Actually, I'm just saying that so it's clearer what I have to do. 17:09:04 ss 17:09:41 alise shut up 17:09:48 have you read I am not a number, I am a free variable 17:10:04 -!- alise_ has joined. 17:11:04 I know how De Bruijn indexes work, fax. 17:11:10 I chose a bit of a shitty representation though. 17:11:15 I know how your mom works 17:11:17 "fax" 17:11:22 what 17:11:23 Who is fax 17:11:33 I did not mean that. 17:11:41 What do you mean, "'fax' what"? 17:11:48 alise shut up have you read it?? 17:12:02 How can I do both simultaneously? 17:12:08 JUST!!!! DO!!!!! 17:12:34 Can someone with more kernel knowledge than me tell me if this is feasible: http://esoteric.voxelperfect.net/forum/kareha.pl/1266506523/1 17:13:30 -!- indu has joined. 17:13:50 -!- indu has left (?). 17:14:41 -!- alise__ has joined. 17:14:52 -!- alise__ has quit (Client Quit). 17:15:36 -!- alise has quit (Ping timeout: 252 seconds). 17:16:04 -!- MarcoAchur1 has joined. 17:16:24 This is a gun: =>. And this is 5 episodes of Endless Eight. 17:17:36 -!- alise_ has quit (Ping timeout: 276 seconds). 17:20:42 -!- alise has joined. 17:21:21 -!- Phantom_Hoover has quit (Remote host closed the connection). 17:21:25 mIRC users: how the fuck do you set the default font for all subdinwws? 17:21:31 *subwindows 17:21:58 got it 17:22:54 Why the fuck would you use mIRC? 17:22:58 Sorry for the language 17:23:23 a lot of idiots hate mIRC for seemingly no reason other than idiots use it. On Windows I have been unable to find a better client (because all others suck). 17:24:44 -!- Phantom_Hoover has joined. 17:25:09 -!- alise_ has joined. 17:25:22 ...and then it inexplicably crashed 17:25:29 alise, Silverex? 17:25:39 No, mIRC. Or maybe I quit it... 17:25:43 Windows is confusing. 17:26:23 -!- alise_ has quit (Client Quit). 17:26:27 I meant, what's wrong with Silverex? 17:26:30 -!- alise has quit. 17:26:57 -!- alise has joined. 17:27:07 -!- alise_ has joined. 17:27:14 Figured out why. 17:27:22 It was minimising to tray; bad idea w/ Win7. Didn't actually crash. 17:27:26 -!- alise has quit (Client Quit). 17:27:31 -!- alise_ has changed nick to alise. 17:27:41 So now my only question is how to make subwindows maximised by default. 17:28:22 -!- alise has quit (Client Quit). 17:28:52 -!- alise has joined. 17:29:35 Ftop. 17:30:49 Hopefully a permanent client should make my IRC more reliable. 17:30:57 Is there anything better than Pidgin yet for Windows IMing? 17:31:05 -!- MarcoAchur1 has left (?). 17:31:36 nekwhat's the apb 17:33:10 ? 17:33:12 Are you drunk? 17:36:43 -!- adam_d has joined. 17:37:20 I recently tried switching to Digsby 17:37:28 oerjan said something about superstrict languages where (\x. f x) evaluates f. 17:37:32 That's interesting. 17:37:35 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 17:37:47 Yet to form a solid opinion on whether it's better. So far, still hoping that its Facebook Chat support is better than Pidgins 17:37:57 Digsby is spyware, iirc. 17:38:01 Or at least obnoxiously social. 17:38:23 Which one? I mind the former, the latter can be disabled as far as I've seen 17:38:47 I don't know. 17:39:12 Hmm... (\f. (\x. f (x x)) (\x. f (x x)) would evaluate (x x). 17:39:19 So even the lambda-expression of Y would diverge. 17:39:26 Is it TC, I wonder? 17:39:33 (\x. x x) is OK 17:40:08 -!- BeholdMyGlory has joined. 17:45:41 Yay, I implemented it and Y does indeed diverge. 17:48:37 heh 17:48:46 using divergence to check if your code works 17:49:07 Quite. 17:51:04 alise, hm.. which language? 17:51:17 lambda calculus? 17:57:13 Yes. 17:57:17 Superstrict lambda calculus. 17:57:30 Where, in (\x.E), you evaluate E as far as you can without relying on x's value. 17:57:40 So (\x. f x) evaluates f before it's even applied. 17:58:55 *Main> eval (App succL zeroL) 17:58:56 \a. \b. (a ((*** Exception: Prelude.(!!): index too large 17:59:00 Dammit. 17:59:02 The verifier should have caught that... 17:59:14 alise: That's pretty damned crazy right there. 17:59:56 Ugh, I have some sort of horrible bug. 18:00:02 (You could argue the entire thing is a horrible bug.) 18:01:46 At some point I used Xircon for Windows-irc, but the development of that died at 1.0b4, I think. It had a TCL scripting engine, that was at least nicer than mirc-scripting. But that was years ago; not sure what people use nowadays. 18:04:10 I have no idea why this isn't working XD 18:04:27 * alise tries booleans instead as a test 18:06:44 I have serious variable issues. 18:09:19 ah... 18:09:26 Lam ((Var 1 :$ Lam (Lam (Var 1))) :$ Var 1) 18:09:30 I'm not demoting my variables sufficiently 18:14:10 alise shut up!!!!!!!! 18:14:45 read the (first few pages of the) paper 18:15:09 -!- alise has quit (Ping timeout: 252 seconds). 18:15:21 -!- alise_ has joined. 18:16:23 * pikhq ported the "official" Lazy K interpreter to use Boehm GC... 18:16:38 Quite an accomplishment. 18:16:50 The reference counting scheme it used leaked memory. 18:16:55 So I fixed it. 18:17:08 I've also made the thing compile on modern C++ compilers. :P 18:17:20 It used reference counting? 18:17:22 Lollercopters 18:17:24 Yes. 18:17:37 It leaked a metric fuckton of memory. And the author had no idea why. 18:17:43 WHat's wrong with reference counting? 18:17:56 Sgeo: Leaks memory with cyclic datastructures. 18:18:02 So... the issue is that when I apply a lambda, and it results in a lambda, I need to decrement the Vars in it. 18:18:08 Ah 18:18:12 Bleh. 18:18:17 Not interesting enough. 18:18:25 Also, is somewhat overhead-heavy if done naively. 18:18:50 okay im here 18:19:55 It would be interesting to have a language where all expressions result in infinite structures. 18:20:04 Then reference counting would be /useless/ :) 18:20:42 Most of the work in making the interpreter GC'd was removing the reference counting and the inefficient pool allocator. 18:21:08 Adding the GC-ness was... "class Expr : public gc {" 18:23:53 `calc 1 metric fuckton in US fucktons 18:24:02 `calc 1000000000000000000000000000000000000000000000000 18:24:05 twitterbits.com/wp-content/plugins/as-pdf/generate.php?post=11 - [21]Similar 18:24:06 yodellingllama.com/?p=1183 - [16]Cached - [17]Similar 18:25:41 pikhq: Y'know, I'm starting to think that metric fucktons aren't even a real unit! 18:27:36 Hahah. 18:28:28 http://sprunge.us/OLIF It's a Lazy K interpreter that doesn't leak memory! 18:28:51 Is it a bird? Is it a plain? No... 18:28:55 (This is Jeopardy, right?) 18:29:02 *plane >_< 18:30:29 (note: still more complicated than it should be. C++: because iostreams suck so much we write our own stream class for everything) 18:31:25 -!- BeholdMyGlory has quit (Ping timeout: 260 seconds). 18:34:18 * alise_ wonders whether he's invented the Church, Mogensen-Scott or an entire, unnamed other encoding. 18:34:26 (The latter is unlikely.) 18:35:31 Mogensen-Scott is best 18:35:35 -!- Phantom_Hoover has joined. 18:36:04 How do you encode Nil | Cons ? List in Mogensen-Scott? I have: 18:36:08 Nil = \f g x. f x 18:36:08 Cons = \head tail f g x. tail f g (g head x) 18:36:10 Z | S Nat: 18:36:10 Z = \f g x. f x 18:36:10 S = \nat f g x. nat f g (g x) 18:36:11 A ? | B ?: 18:36:12 A = \val f g x. f val x 18:36:12 B = \val f g x. g val x 18:36:29 Are there any people acquainted with the Linux kernel here? 18:36:30 and finally, A | B: 18:36:30 A = \f g x. f x 18:36:30 B = \f g x. g x 18:36:57 So for a given constructor C, you take n functions where there are n constructors, and each function is of the type (... -> x) for the same x for all of them and ... being the arguments to the constructor. 18:37:12 If there is no recursion in the type, then you simply call the appropriate function. 18:37:13 alise weird 18:37:32 Otherwise, you invoke your substructure with the same functions, but with the value being substituted for what you'd normally do without the recursion. 18:37:56 I may have the function types wrong; forgot about the \x. bit. 18:37:56 fax: I think it's the most natural encoding. 18:38:00 Case analysis is built-in as the distinct functions. 18:38:11 Decomposition of the value also is built-in to each function's argument. 18:38:22 And it transforms type recursion into value recursion. 18:38:43 So the relevant function gets the /already decomposed, according to your will/ substructure as its argument. 18:39:21 fax: and you know what? 18:39:24 Prelude> :t cons (1::Integer) (cons 2 nil) 18:39:24 cons (1::Integer) (cons 2 nil) 18:39:24 :: (t21 -> t2) -> (Integer -> t21 -> t21) -> t21 -> t2 18:39:28 It encodes types as their fold. 18:39:31 I think their left fold. 18:39:36 Maybe right-fold would be more elegant. 18:40:28 So succ would be \nat f g x. g (nat f g x) 18:40:43 cons would be \hd tl f g x. g head (tail f g x) 18:40:48 fax: is that morgonson? 18:41:10 -!- sebbu2 has joined. 18:41:10 no 18:41:18 What is morgonson then? 18:42:15 -!- sebbu has quit (Ping timeout: 245 seconds). 18:42:15 -!- sebbu2 has changed nick to sebbu. 18:45:44 * alise_ tries to transform a tree into it 18:46:43 Leaf = \val f g x. f val x 18:46:44 Branch = \left right f g x. left f g (g (right f g x) x) 18:46:44 or 18:46:44 Branch = \left right f g x. g (left f g x) (right f g x) 18:46:44 I think 18:46:55 I think the latter is better. 18:47:00 alise did you see my post that uses lambda calculus 18:47:10 No; link. 18:47:24 on the blog 18:47:46 * alise_ attempts to google to find it again 18:49:12 hmm 18:49:33 church numerals are like this but with f=id 18:49:35 which is equivalent 18:49:50 and church numerals are A/B without the extra x (equivalent under n) 18:50:18 actually 18:50:22 false = \g x. x 18:50:26 true = \g x. g x 18:50:30 so false = \a b. b 18:50:33 true = \a. a 18:50:36 lol 18:50:55 wait i can't have f = id 18:50:57 A = \val f g x. f val x 18:50:57 B = \val f g x. g val x 18:51:46 Prelude> :t branch 18:51:47 branch 18:51:47 :: (t -> (t2 -> t3 -> t4) -> t1 -> t2) 18:51:47 -> (t -> (t2 -> t3 -> t4) -> t1 -> t3) 18:51:47 -> t 18:51:47 -> (t2 -> t3 -> t4) 18:51:47 -> t1 18:51:47 -> t4 18:51:48 obviously 18:56:45 hmm it should be f x val 18:56:49 not f val x 18:57:46 Cons = \head tail f g x. g (tail f g x) head 18:57:50 Er, no, that's not really right. 19:01:40 fax: I thought of a really nice property of musing Mu for recursive datatypes. 19:02:14 musings on Mu -- sounds like a blog post 19:03:49 -!- olsner_ has joined. 19:04:12 fax: hehe 19:04:59 fax: I often have the issue that I have two types, e.g. expression and pattern, where pattern is like expression but with one extra constructor like Free String 19:05:02 so I have to do 19:05:04 data Core = ... 19:05:12 (oh and expression has some extra thing too) 19:05:16 data Expr = Core Core | ... 19:05:20 data Pat = Core Core | ... 19:05:21 except 19:05:24 what if Core is recursive? 19:05:32 data Core self = ... 19:05:42 data Expr = Core (Core Expr) | ... 19:05:47 data Pat = Core (Core Pat) | ... 19:05:49 but 19:05:51 if Core was defined with mu 19:05:56 then it'd be Mu F 19:06:02 so we'd just do F (Mu Expr) instead! 19:06:23 so Mu actually lets you easily express recursion-substitution of data types 19:08:44 I think we need some way to extract the F from a Mu F 19:09:16 wait, that's easy 19:09:18 extract (Mu F) = F 19:09:22 well 19:09:26 that requires pattern matching on Mu :P 19:09:39 Are you just talking to yourself? 19:10:06 He's talking to whoever is listening. 19:10:14 Well, fax would ideally respond. 19:10:29 What is it you're talking about? 19:10:33 I missed the start. 19:11:36 Using Mu-recursive types to encode recursion-substitution of data types. 19:12:17 -!- augur has quit (Ping timeout: 246 seconds). 19:13:31 heh () becomes id in my encoding 19:14:10 How does that work? 19:14:57 http://pastie.org/868169.txt?key=mmgxkfgi4bnnt1ix3u3jqg 19:15:25 Haskell? 19:15:37 -!- kar8nga has joined. 19:15:38 Well, for the data types (with ? for polymorphism) 19:15:45 The expressions, lambda-calculus 19:15:52 The format is data Foo = ..., in my representation is ... 19:16:33 So a constructor C for a type T with N constructors, C takes N functions of the arity of the corresponding constructor, plus one (of the same type for every function, but polymorphic), and returning something of the same type for every function (but polymorphic). 19:16:48 -!- Asztal has quit (Ping timeout: 265 seconds). 19:16:57 Oh, and a value of the type of the first argument of each function. 19:17:05 If the data type is not recursive, then the corresponding function is simply called with the value given, plus the constituents of the constructor. 19:17:06 *quails* 19:17:20 If it is recursive the value given is substituted for the value of calling the substructure with the same functions, and the value. 19:17:30 (This is repeated for each recursive element, as different arguments to the function.) 19:17:38 Thus: 19:17:40 Leaf = \val f g x. f val x 19:17:41 Branch = \left right f g x. g (left f g x) (right f g x) 19:17:55 I was away having dinner 19:18:23 fax: That is NOT ALLOWED. 19:18:28 ;( 19:18:32 I didn't know 19:18:44 Real Programmers eat the dust in the air. 19:18:46 -!- oerjan has joined. 19:18:55 fax: well READ WHAT I SAID :| 19:18:58 hi oerjan! 19:19:00 -!- MizardX- has joined. 19:19:03 -!- MizardX- has quit (Remote host closed the connection). 19:19:05 hi fax 19:19:09 alise encoding data into lambda calculus is boring though 19:19:12 also alise_ 19:19:21 -!- MizardX- has joined. 19:19:23 -!- MizardX- has quit (Changing host). 19:19:23 -!- MizardX- has joined. 19:19:34 hey 19:19:43 so where does calulus happen? 19:19:53 real numbers, finite numbers, data 19:19:55 what else ? 19:20:10 Calculus :: * -> BranchOfMathematics 19:20:18 fax: What is there that is not data? 19:20:18 um 19:20:20 Wait, there's and implementation of real numbers on the lambda calculus now? 19:20:23 Function calculus perhaps? 19:20:24 I don't mean lambda calculus 19:20:28 s/and/an/ 19:20:34 I mean like "derivatives" and "integrals" 19:20:38 Phantom_Hoover: The computable reals are expressible in just about any language. 19:20:45 on data I mean specifiically: d for data 19:20:46 Well-typed at compile time in dependent languages. 19:20:54 please just understand what I mean :| 19:21:11 f : PosRational -> Rational is a computable real number iff for all positive rationals e1, e2, abs (f e1 - f e2) < e1 + e2 19:21:30 yeah, for computable reals you don't even need recursion 19:21:33 hm 19:21:36 "recursion" 19:21:44 +general 19:22:10 yeah if you can do rationals and semi-recursive functions 19:22:12 then you can do computable reals 19:22:13 -!- MizardX has quit (Ping timeout: 276 seconds). 19:22:20 -!- MizardX- has changed nick to MizardX. 19:22:24 you could even model them in brainfuck if you came up with a function representation 19:22:36 I should implement some reals, but I'd need quotient field..... 19:22:44 and I have implemented it but not proved it a field yet 19:23:21 *<= 19:23:23 not < 19:23:24 I always make that mistake 19:23:53 alise ill tell you the defintion from my bok 19:25:40 bok 19:26:19 alise, 19:26:36 really what you need is a cauchy sequence that's all :P 19:27:23 Serious analysis begins with the real numbers. A /real number/ is a sequence (x_n)_(n>=1) of rational numbers that is /regular/, in the sense that forall m >= 1, forall n >= 1, |x_m - x_n| <= m^-1 + n^-1 19:28:15 The standard equality on the class R of real numbers is defined so that (x_n) =_R (y_n) if and only if forall n >= 1, |x_n - y_n| <= 2n^-1 19:28:17 yeah but if you have an infinite sequence... well that's a function 19:28:33 and it's nicer to use if you have the indices be Q+s 19:28:46 This relation is clearly reflexive and transitive; its transitivity is a consequence of 6.1 19:28:50 also equality on the computable reals doesn't always terminate if they're nonequal which sucks 19:28:55 imo, using === is better 19:29:03 then you just have to prove they're equal or not :)))) 19:29:17 yeah equality is not decidible on R, that's a classical statement 19:29:30 that =_R I gave above is a proposition 19:29:48 yeah 19:29:52 ah 19:30:01 alise want to show you something really cool I saw today 19:30:04 i know it's well known 19:30:07 but it does so suck 19:30:15 what sucks?? 19:30:27 alise_: um if they're nonequal obviously it terminates, it's the equal case that is problematic 19:30:27 alise, read this http://coq.inria.fr/stdlib/Coq.Reals.Rlogic.html 19:30:28 a NINJA??? 19:30:40 o_o lol 19:33:43 oerjan: er right 19:34:08 09:39:12 Hmm... (\f. (\x. f (x x)) (\x. f (x x)) would evaluate (x x). 19:34:08 09:39:19 So even the lambda-expression of Y would diverge. 19:34:23 "transClause :: ..." ;; Mr, now Mrs Clause 19:34:25 well but that expression is unusable in a (just) strict language anyway 19:35:14 Theorem not_not_archimedean : 19:35:19 forall r : R, ~ (forall n : nat, (INR n <= r)%R). 19:35:19 Not not not not not. 19:35:24 oerjan: of course 19:35:29 having lambda-expressions diverge is hilarious 19:38:10 10:17:56 Sgeo: Leaks memory with cyclic datastructures. 19:38:27 i don't think lazy-K has cyclic datastructures, but i haven't investigated it 19:38:35 alise did you read it??? 19:39:00 because it doesn't have Y as a primitive 19:39:12 fax: yrd 19:39:17 ?? 19:39:17 *yes 19:39:25 now what 'sucks'? 19:39:57 although on the other hand _that_ might perhaps cause memory leaks with recursion that an efficient Y wouldn't give 19:40:22 fax: non-propositional equality on reals 19:40:24 ffs 19:40:40 the consequence of decidible equality 19:41:00 think about classical logic as contained inside constructive.. 19:41:05 or perhaps that just causes a lot of duplicate evaluation. 19:41:38 fax: what are you trying to say 19:41:59 * oerjan is assuming lazy-K isn't so cleverly implemented as to detect essential uses of Y 19:42:06 im just talking :| 19:43:47 fax: :-) okay 19:44:03 you think im stupid!! 19:44:05 ill show you 19:44:09 fax: also i'm beginning to think pattern matching in function heads is overrated in dependent langs... 19:44:17 oh?? 19:44:45 I don't think you're stupid ffs :) 19:44:46 and 19:44:47 bI don't think a denpendent language needs to support pattern matching 19:44:56 I mean as a syntactic thing 19:44:58 but it should be able to add pattern matching 19:45:05 because often pattern matching has drastic effects on the structure of the other arguments 19:45:16 so a possibly-nested case expression makes this much clearer 19:45:29 and often the analysis is more complex than just does-this-constructor-match 19:45:31 well you can try programming with nested cases in Coq 19:45:36 and function-head matching doesn't really aid that 19:45:55 at one point I just gave up an implemented (an ad-hoc bug* ridden version of) dependent pattern matching 19:46:17 (* not actually able to produce wrong results.. but sometimes might not produce any result) 19:47:15 well i mean i like dependent pattern matching 19:47:26 but I'm specifically criticising 19:47:29 f (X ...) = ... 19:47:31 f (Y ...) = ... 19:47:50 yeah but you know case 19:47:53 you can't just write 19:48:08 f x = case x of X ... -> ... ; Y ... -> ... 19:48:11 if it's dependent 19:48:17 you have to say something about the types 19:48:17 hmm. 19:48:22 I don't see why 19:48:26 hmm 19:48:37 well.................... you do in Coq, is this a fundamental thing though? 19:48:47 what do you mean say something about the types btw? 19:48:50 ISTR augustss writing about it being essential 19:48:53 well I blogged about it 19:49:33 Phantom_Hoover: that Talk: Befunge message you responded to is spam (try googling it) 19:49:40 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds). 19:49:45 sheesh 19:49:51 he just does that on purpose 19:49:56 -!- augur has joined. 19:50:34 fax: um that Ping timeout thing isn't is server generated? 19:50:49 he pulls the plug out 265 seconds before someone talks to him 19:53:14 I should have a specialisation of id called ff 19:53:14 so I can have 19:53:22 tt : ? 19:53:22 ff : ? 19:53:26 hope that sent right 19:53:30 ¬??? 19:53:35 oh 19:53:38 top/bot 19:53:39 that ? must have been a 'T' 19:53:39 from tt/ff 19:53:44 yeah 19:53:48 TT : ~T 19:53:49 erm 19:53:51 oops 19:53:51 :D 19:53:54 tt : T 19:53:56 ff : ~_|_ 19:53:56 looks like Omegamega 19:54:02 hm indeed user quit messages are prefaced with Quit: 19:54:32 (the format changed when they switched ircd) 19:54:48 toProp : (b : Bool) -> Sigma (P : Prop) (cond [b => P, not b => ~P]) 19:54:49 toProp b := 19:55:00 cond [b => T sigma tt, not b => _|_ sigma ff] 19:55:22 wondering if i should use case analysis instead of cond 19:55:46 yeah it looks nicer 19:55:59 I should have ?: with a nicer name :) 19:56:41 -!- Phantom_Hoover has joined. 19:56:59 Phantom_Hoover: that Talk: Befunge message you responded to is spam (try googling it) 19:57:36 Phantom_Hoover: ^ 19:59:06 Oh. 19:59:14 Very weird spam. 19:59:46 Phantom_Hoover: i don't know why they're doing it, but it's fairly common. look out for messages that have no hint the poster knows what the wiki is about. 19:59:50 after a while you get a sense as to what's spam and what isn't 20:00:03 oerjan: does the page need deleting? or is there legit content on it too? 20:00:19 ais523: i already removed that section, there are lots of legit ones 20:00:28 ok 20:01:12 i have an excellent spam 'n phish o mometer 20:01:13 spam and fish 20:01:15 I should probably start selling fungot licenses to spammers; it's more entertaining than the usual gibberish I see in my inbox. (Though they might not be going for the entertainment value there.) 20:01:15 :) 20:01:15 fizzie: i was born in a barn?". i assume you'll mostly just want " how did you get my privmsgs? 20:01:31 Born in a Barn. fungot. The autobiography. 20:01:32 alise_: distributive property for example i wrote program as an ast? i believe the right way 20:01:49 Phantom_Hoover: they have started trying to formulate messages that look like they _could_ be legit, but google shows when they're spammed all over the place 20:02:32 s/place/web/ 20:03:51 ehird 20:03:55 alise 20:04:04 oerjan: that spam is mostly pointless anyway, if they aren't spamming URLs or anything like that 20:04:53 fax: I have a feeling I need a real system... 20:04:56 I keep using "refl" to substitute for any a === :-) 20:05:00 *a === b 20:05:08 ais523: yeah i don't understand why they're doing it either. maybe to test our spam response intelligence? 20:05:14 alise I don't understand 20:05:30 you cant use refl unless a and b are convertible 20:05:35 fax: don't understand what, my refl thing? 20:05:37 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds). 20:05:39 oerjan: I heard an explanation that sounds plausible: the bots are trying to spam their URLs in an URL field, and although MediaWiki doesn't have one the bots don't know that 20:05:42 well exactly 20:05:49 however, in that case I don't see how they'd be getting past the CAPTCHA 20:05:49 ais523: ah 20:05:52 toProp b === T sigma tt? well obviously, it's true! 20:06:05 that's extentional equality!!!!! 20:06:10 spambots generally need some knowledge of how an individual CAPTCHA works before breaking it 20:06:15 Proof: refl! 20:06:27 hrfm 20:06:35 ais523: does our wiki have a special captcha? 20:06:50 no, it's MediaWiki's default captcha 20:06:59 and a very easily broken one, at that 20:07:01 i don't recall seeing it 20:07:05 fax: so? :P 20:07:11 oh, wait 20:07:19 btw how is apartness defined? 20:07:22 ais523: which means the spammers probably know all about it since a long time ago 20:07:33 the CAPTCHA rules are that they come up on attempts to register accounts, and edits by anons that add URLs 20:07:39 I thought of having as an argument to the constructor a proposition for which P x but not P y 20:07:40 thinking about it: this spam isn't actually adding URLs 20:07:45 so it doesn't need to go past the CAPTCHA at all 20:08:06 ais523: heh. also this last spam showed some indication they knew it was a _wiki_, even if not what the wiki was about 20:08:18 (it talked about creating articles) 20:09:35 -!- mano0o0 has joined. 20:09:36 or maybe that's common terminology for other things than wikis too 20:09:49 the spam just came up on my feed of all edits to Esolang 20:09:52 nothing gets past the admins! 20:09:58 just, sometimes other people get there first 20:10:11 and that particular comment would make sense on a blog, too 20:10:15 although it would mean something else 20:10:22 ais523: oh? what then? 20:10:37 an article would have to posted by a blog owner wouldn't it 20:10:43 *to be 20:10:55 oerjan: it means, can someone find me more articles on this subject? 20:11:36 hm not quite, but i see it could be... 20:11:37 alise, I will show you apartness 20:11:47 alise I should just write this whole chapter into Coq :P 20:11:53 it sounds like one blogger asking another how they find ideas 20:12:00 yep 20:13:31 x # y if x > y or y > x 20:13:48 fax: just look at this pile of shit: http://pastie.org/868241.txt?key=unp3wmm109dzwe6ssnkw 20:13:54 properties: x = y /\ x # y -> 0 = 1 20:13:58 I just cheated through the whole fucking proof by sprinkling refl everywhere! :-P 20:14:03 i wonder if the wiki enabled captchas after i joined (2006) 20:14:05 fax: so apartness is only defined if you have an ordering? 20:14:08 I had 20:14:12 x = y /\ y # z -> x # z (??? weird one) 20:14:17 x # y -> y # z 20:14:19 x # y -> y # x *** 20:14:26 x # y -> x # z \/ z # y 20:15:14 data Apart : {A:Set} -> (x:A) -> (y:A) -> Prop where lfer : {P : A->Prop} -> ((P x /\ ~P y) \/ (P y /\ ~P x)) -> Apart x y 20:15:39 oerjan: it's relatively recent, I had a discussion with Graue about it 20:16:03 alise what's teh point in making that data? 20:16:07 -!- olsner_ has quit (Quit: olsner_). 20:16:08 why not just do it as a function definition 20:16:19 oh wait I completely neglected my obligation in toBool to supply P | ~P 20:16:19 that's why the proof was so easy... 20:18:40 what data 20:18:44 and because 20:18:46 20:14 < alise_> data Apart : {A:Set} -> (x:A) -> (y:A) -> Prop where lfer : {P : A->Prop} -> ((P x /\ ~P y) \/ (P y /\ ~P x)) -> Apart x y 20:18:48 toProp : (b : Bool) ? S (P : Prop) (cond b ? P; else ? P) 20:18:49 oh you mean apart 20:18:56 because === is defined as data sooo 20:19:03 my um / 20:19:03 ? 20:19:10 what's the name of like .. a strategyr 20:19:12 well here's a definition 20:19:14 ais523: rings a bell 20:19:17 except that it's ad-hoc guidlines 20:19:31 rule of thumb 20:19:49 fax: heuristic? 20:19:54 yes! 20:20:13 my hooristikc is to define the fewest data possible, but the strongest ones 20:20:14 apart : {A:Set} -> A -> A -> Prop 20:20:21 like if two data are similar, you can probably abstract it out 20:20:33 apart x y = exists {P : A->Prop}. (P x /\ ~P y) \/ (P y /\ ~P x) 20:20:33 or something 20:20:36 the real reason to define a data type is because you want the strength of its induction principle 20:20:44 at least that's my (current) view/understanding 20:21:04 fax: it looks really weird whenever anyone uses the word "data" correctly 20:21:05 well done 20:21:19 http://pastie.org/868253.txt?key=nb3ny4djjrabif9xilvalq honestly toBool.toProp===id should just be "obvious" 20:21:29 toBool.toProp===id b := obvious 20:22:20 obvious : {P : Prop} -> cond isObvious P -> P; else -> T 20:22:43 tautology "P" -> P ? 20:23:26 ? 20:23:31 is " quoting? 20:23:55 so tautology : (q : Quoted Prop) -> unquote q? 20:24:35 fax: so what's the type containing Prop and Set in your opinion? Set_1? 20:27:15 s : {A : Set1} ? {B : Set1} ? {P : A ? B} ? (x:A) ? P x ? S (x:A). P x 20:27:15 scary type. 20:27:20 whoa there mirc 20:27:22 what are you doing 20:27:43 s : {A : Set1} ? {B : Set1} ? {P : A ? B} ? (x:A) ? P x ? S (x:A). P x 20:27:43 hmm 20:28:04 -!- werdan7 has quit (Ping timeout: 619 seconds). 20:28:52 well 20:29:22 _sigma_ : {A : Set_1} -> {B : Set_1} -> {P : A -> B} -> (x:A) -> P x -> Sigma (x:A). P x 20:29:22 anyway 20:30:10 alise in Coq it's Type (Type[1]) 20:30:17 but I don't really have an opinion on this :P 20:30:29 so Set : Type, Prop : Type? 20:30:55 fax: I kinda hate having separate Sets and Props 20:31:00 because you lose so much isomorphism and neatness 20:31:24 umf 20:31:28 I don't knnow what yu mean 20:31:39 please, please, PLEASE, when saying you don't know what i mean QUOTE the bit 20:31:41 otherwise I can't answer 20:31:45 20:30 < alise_> because you lose so much isomorphism and neatness 20:31:59 for instance 20:32:12 A \/ B = Either A B 20:32:16 A /\ B = A * B 20:32:29 P \/ ~P then just inspecting left/right to find out which it is 20:32:43 forall <-> function 20:32:50 exists <-> dependent tuple 20:32:54 and so on, so forth 20:35:13 what 20:35:28 wait 20:35:37 -!- Phantom_Hoover has joined. 20:35:52 proofs are different than types 20:35:59 the reason is proof irrelevance 20:36:04 i know! 20:36:15 so why would you want to get rid of proofs?? 20:36:17 but if you ignore proof irrelevance like agda, everything is so much prettier and curry-howardish :( 20:36:27 * fax doesn't find it prettier 20:36:36 hm 20:36:48 agda has combined proof/set... and suffers for it, but the isomorphisms are just so appealing 20:36:48 20:31 for instance 20:36:48 20:31 A \/ B = Either A B 20:36:48 20:31 A /\ B = A * B 20:36:48 20:32 P \/ ~P then just inspecting left/right to find out which it is 20:36:49 20:32 forall <-> function 20:36:49 20:32 exists <-> dependent tuple 20:36:50 20:32 and so on, so forth 20:36:54 maybe if we used quotients!!!! 20:37:01 to make a 'proof' set 20:37:13 well it's not prettier per se 20:37:14 I suppose that's what epigram does 20:37:16 but the isomorphisms are elegant 20:37:18 -!- werdan7 has joined. 20:37:22 if you don't value isomorphisms - 20:37:23 what isomorphisms? 20:37:27 then why do we persue curry howard? 20:37:27 are you talking about curry-howard 20:37:29 for FUCK's sake 20:37:30 20:31 for instance 20:37:30 20:31 A \/ B = Either A B 20:37:30 20:31 A /\ B = A * B 20:37:30 20:32 P \/ ~P then just inspecting left/right to find out which it is 20:37:30 20:32 forall <-> function 20:37:30 20:32 exists <-> dependent tuple 20:37:31 20:32 and so on, so forth 20:37:42 THOSE isomorphisms 20:37:44 stop pasting that, I can't see what you are saying inbetween all this pastes 20:38:04 maybe the idea is to read the paste 20:38:04 instead of asking for its contents 20:39:53 those are (among the) appealing isomorphism s 20:39:55 *isomorphisms 20:40:22 I don't get it 20:41:23 what part do you not get 20:41:59 data _/\_ : (A:*) -> (B:*) -> * where both : A -> B -> A /\ B 20:42:03 look similar to the definition of a tuple to you? 20:42:12 :S 20:42:38 What, it doesn't? 20:42:43 curry-howard is that typed lambda calculus corresponds to natural deduction ? 20:42:57 What I was /trying/ to do is use *analogy*. 20:43:17 Curry-Howard: Types in the lambda calculus correspond to statements in intuitionistic logic. W 20:43:24 Curry-Howard: Types in the lambda calculus correspond to statements in intuitionistic logic. We love this, and pursue it: it's why we make dependent languages. 20:43:33 is that a quote? 20:43:34 So if you do not appreciate the isomorphisms I listed, why then Curry-Howard? 20:43:38 No. 20:43:47 okay let me get this straight 20:44:02 no 20:44:04 no I don't get it 20:44:24 What part? 20:44:25 can't you use v and ^ instead? :p 20:44:31 I'm asking #haskell 20:44:34 comex: Yeah, it's not like v is like a variable name. 20:44:42 fax: ugh, you make no sense at all 20:44:55 *is a variable name 20:45:11 this is my question: 20:45:12 what does 'Curry–Howard correspondence' have to do with dependent types? 20:45:27 Ugh! That is IRRELEVANT to my point. 20:45:34 Dependent languages make /good proof systems/. 20:45:35 wow 20:45:40 why is it irrelevant 20:45:52 Because/ of Curry-Howard. 20:45:54 *Because 20:45:55 *BECAUSE 20:46:37 So we, in making our languages, support the isomorphism; recognise it as good. If you do not recognise isomorphisms as a reason for the unification of two general concepts, as in the examples I showed, why then do you recognise Curry-Howard as a good thing? 20:47:23 I'm not sure what Curry-Howard is exactly 20:47:53 it seems kinda vauge, like a principle more than a formal statement 20:48:06 Duh. 20:48:07 Of course it is. 20:48:32 you needn't be so caustic 20:48:39 Sgeo: http://lifehacker.com/5336382/digsby-joins-the-dark-side-uses-your-pc-to-make-money, http://www.downloadsquad.com/2008/11/24/new-digsby-installer-loaded-with-bloat-and-adverts/, http://www.downloadsquad.com/2009/08/14/digsby-responds-to-claims-of-shady-money-making-tactics/ 20:50:05 Survived the first two points raised by LH 20:50:22 So? 20:50:25 Do you want to support such a company? 20:52:10 Hm. What alternatives are there, then? 20:52:24 Pidgin's been sucking for me for some reason, Digsby's company is shady 20:52:25 Uh, Pidgin? 20:52:29 It sucks but what can you do. 20:52:39 Miranda IM is popular with the anal-retentive tweakers. 20:52:50 A few hours and it's exactly as good as Pidgin but with more alpha-translucency. 20:53:12 :/ 20:53:12 * Sgeo doesn't like tweaking stuff 20:53:16 Huh; Russ Cox wrote Code Search. 20:53:20 alise just give up on me after bitching 20:53:35 fax: I just didn't notice what you said 20:53:40 There are other people than you and they talk... 20:53:51 I give up on people after I see a conversation going in circles, only. 20:55:42 brb 20:55:47 people shouldn't repeat themselves if they don't like going in cirlecs.. 20:55:59 Can Miranda IM be made to support Facebook Chat? 20:56:14 Apparently yes 20:56:52 I remember using Miranda IM once when I couldn't get Pidgin working, and I remember HATING it 20:56:55 -!- Phantom_Hoover has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838]). 20:57:11 -!- Phantom_Hoover has joined. 20:57:42 Bloody QEMU... 20:57:58 * fax weeps 20:58:04 Why? 20:59:38 *bangs head against keyboard* 20:59:42 What's wrong with Qemu? 21:00:36 I'm trying to run a Linux kernel with -hda as a virtual disc, but it won't mount for some reason. 21:02:18 If I run "qemu -m 32 -hda ./vm.img -kernel ~/.../bzImage -append "root=/dev/hda"" the console prints some stuff about not being able to mount 21:02:19 . 21:02:43 Is hda a virtual disk or a filesystem? That is, is it partitioned? 21:03:01 You mean vm.img? 21:03:07 Yeah 21:03:18 It's a raw image with an ext3 filesystem on it. 21:03:31 Well, yuh, that should work, assuming the kernel has IDE support. 21:04:14 It doesn't work with the kernel in /boot either, so I assume the fault isn't with the kernel. 21:04:46 huh what happened... 21:04:59 By mistake I left clicked a tab with ctrl held down in firefox 21:05:08 it changed the tab title to begin with "(*)" 21:05:16 repeating the click removes it 21:05:19 fully reproducible 21:05:36 but it seems to have no effect in behaviour 21:05:52 anyone know if it is supposed to just do that, or do something else as well? 21:06:14 I mean, if it is just to mark a tab, or it changes something wrt. how the tab behaves 21:07:15 it could be from tab mix plus I suppose 21:08:34 -!- Phantom_Hoover has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838]). 21:12:37 alise? 21:17:29 hm it does indeed seem to be related to tab mix plus 21:18:14 -!- Phantom_Hoover has joined. 21:19:10 Should ChanServ really be giving me a dead link? 21:19:58 yes. 21:20:09 But it's dead! 21:24:56 It's bleeding demised! It's passed on! It's no more! It has ceased to be! It's expired and gone to meet its maker! 21:27:06 It's just resting. 21:27:19 back 21:27:25 alise_: not you 21:27:28 Oh, you were right. 21:27:42 we backed up the frappr, so bah 21:28:10 Where is this backup? 21:28:25 on our hard drives 21:28:32 AnMaster has it, so do I on my other machine 21:29:23 Oh, does anyone now the reason for my Qemu problems? 21:29:31 Apparently Digsby stopped bundling spyware, so I'll try it. 21:29:38 Phantom_Hoover: #qemu? 21:29:51 alise alise alise alise 21:30:22 alise_: Tried that. It doesn't let me say anything. 21:31:34 Identify your nickname. 21:31:37 fax: What? 21:31:41 ...How? 21:31:48 nickserv 21:31:58 ...How? 21:32:09 Just Fucking Google It 21:32:15 ;( 21:32:26 ghost sucker: /msg nickserv help 21:32:33 don't google anything 21:32:38 google is for idiots and queers 21:33:23 real defensed proposition you got there 21:33:27 you included all that evidence and reasoning 21:34:44 * oerjan uses a screwdriver to fix alise_'s joke detector 21:35:28 alise 21:35:32 I have to tell you this 21:35:38 Coq is a proof assistant based on dependent type theory developed at 21:35:38 INRIA [CDT08]. By default, it uses constructive logic via the Curry-Howard 21:35:38 isomorphism. This isomorphism associates propositions with types and proofs of 21:35:41 propositions with programs of the associated type. This makes Coq a functional 21:35:45 programming language as well as a deduction system. The identification of a pro- 21:35:48 gramming language with a deduction system allows Coq to reason about programs 21:35:51 and allows Coq to use computation to prove theorems. 21:35:59 oerjan: well fax legit hates wikipedia, so... 21:38:11 alise_: so what you are saying is that fax incorporates poe's law all by himself? 21:39:50 :) 21:40:05 Oerjan: There seems to be some vandalism on the wiki. 21:40:24 to the esomobile! 21:40:46 alise -- are you really pissed off at me 21:41:04 No. 21:41:15 If I was, I would be FUCKING SHOUTING YOU RETARD <-- like that. 21:41:28 * oerjan uses the screwdriver to fix fax's joke detector as well. 21:41:28 "Allow Digsby to use idle CPU time for grid computing." Uh, no? 21:41:29 okay 21:41:47 oerjan ? 21:42:10 Manage all your IM, email and social 21:42:10 network accounts with one login 21:42:13 fax: assuming you are referring to the Lazy Evaluation article? 21:42:17 Suspicious. Do I have to give them my password? 21:42:20 that's clearly a joke 21:42:24 lazy evaluation?? no 21:42:35 wait waht 21:42:51 Me? 21:42:52 * oerjan beats himself for confusing fax and Phantom_Hoover ===\__/ 21:42:59 OH! 21:43:02 Why do I need a Digsby account? 21:43:03 We wanted to make it easier to use Digsby at multiple locations. Your Digsby account is used to synchronize preferences such as what skin to use and whether to show popups or not. When you sit down at another computer and log in to Digsby, the experience is completely seamless. 21:43:03 *OW! 21:43:06 So: They store my password. 21:43:16 reversibly 21:43:23 Obviously. 21:43:24 fax: mind you your joke detector probably needs adjustment too 21:43:36 :/ 21:43:42 I TAKE OFFENSE TO THIS 21:43:46 *Phantom_Hoover: assuming you are referring to the Lazy Evaluation article? 21:44:05 Sgeo: Digsby used to bundle adware, now by default (1) uses a browser plugin to get cashbacks when you shop online (installer setting) (2) uses your idle CPU for grid computing (3) changes your homepage to a Digsby-branded Google Search. It also stores your IM passwords. 21:44:09 Sgeo: I think I have said enough. 21:44:26 * alise_ gives his info anyway because dammit pidgin is /really/ badf 21:44:26 *bad 21:44:35 Yes. 21:45:02 alise_: maybe you could write your own? 21:45:13 hmm, even telnet is usable for IRC, but only if you don't do anything else 21:45:15 o_o 21:45:22 ais523: Write Windows software? Are you kidding? 21:45:37 alise_: I'd suggest not actually using the Windows API, that would be ridiculous 21:45:37 */me uses the screwdriver to fix Phantom_Hoover's joke detector as well. 21:45:48 but can't you write portable software, and then run it on Windows? 21:46:00 * fax wanted to talk about dependent types/constructive math with ehird but seems not to be happening 21:46:18 Yes, but I'd rather just get an internet connection that doesn't suck and use it to install Ubuntu. 21:46:19 Or buy a Mac. 21:46:57 fax: you can!! 21:47:01 I love talking about those things 21:47:14 Ooh, Digsby lets you sort contact by total size of logs. 21:47:16 That's interesting. 21:49:36 does anyone hear know what the common "now you have two problems" quip against regex means? 21:50:21 what it means?? 21:50:30 it means that writing regex is a bitch 21:50:35 and doesn't make things easier 21:50:53 ais523 is so eso-adjusted that he thinks regexes are easy :D 21:51:12 ais523: because regexps are brittle and often have scary performance 21:51:14 regex makes things easier if it's appropriate for the problem 21:51:22 ais523: The original quote is about sed, not regex. 21:51:26 It's a quip, it doesn't have to be actually true. 21:51:26 just, don't use it to parse XML or stupid things like that 21:51:36 alise_: recognised; Deewiant: ah, interesting 21:52:02 The UNIX-HATERS Handbook mentions it. 21:52:11 <3 unix haters handbook! 21:52:52 is there a windows-haters handbook? 21:53:26 Not to my knowledge. 21:53:33 also, http://esolangs.org/wiki/Lazy_evaluation, now that's /clever/ vandalism 21:53:45 much better than the typical "recursion" joke 21:54:01 Yes. 21:54:06 I'd leave that there 21:54:11 I'm planning to 21:54:15 Since there wasn't any content to start with 21:55:00 also fun: Google have made a mostly PCRE-compatible regular expression engine 21:55:48 expanding the acronym makes your head spin 21:56:05 lol 21:56:27 Firefox can't find the server at www.esolangs.org. :/ 21:56:31 Yes, it's the typical "fast but can't do everything" implementation using a Thompson NFA 21:56:39 ais523: ... why? 21:56:48 http://esoteric.voxelperfect.net/wiki/Lazy_evaluation 21:56:48 Gregor: better worst-case performance 21:57:08 so they can let people write arbitrary regexen and evaluate them without worrying about someone sending them an algorithmic complexity bomb 21:57:10 Except that worst-case performance of PCRE is almost a non-issue, the worst case never comes up ... 21:57:14 Ahhh 21:57:17 Arbitrary regex 21:57:18 Most properly-maintained things use the slow algos 21:57:23 User-created malicious regex. 21:57:24 Gotcha. 21:59:01 yes 21:59:05 Russ Cox wrote it 21:59:10 Only now do I get the lazy evaluation page. 21:59:11 the same author of the famous article about it 21:59:19 (and the author of Google Code Search which uses it) 22:02:41 Russ Cox??? 22:05:46 yes 22:06:05 alise_ 22:06:06 PM me 22:07:33 fax: can't you PM alise? 22:07:40 no 22:07:45 she doesn't want to talk to me 22:08:15 there is something wrong with this reasoning... 22:08:19 Mayhaps that's because you mistook him for a woman :P 22:08:36 hey, I've been careful for ages to avoid pronouns for alise, it's more fun that way 22:08:51 well, third-person pronouns at least 22:08:54 Gregor: Actually, she is the correct pronoun. 22:08:59 imagine if "I" and "you" were gendered! 22:09:03 It in fact matches reality more than he. 22:09:06 Most people mistake me for a girl. 22:09:28 ounapfhounfakp 22:09:35 Hotels: "Miss (mother's surname because I'm never asked for mine)". Taxis: "[Blah blah destination] ladies?" 22:09:49 People, to my mother: "Blah blah blah your daughter" 22:09:52 So on, so forth. 22:09:58 fax: I'll talk if you say something to me. 22:09:58 Weird. 22:10:02 :( 22:10:39 -!- kar8nga has quit (Remote host closed the connection). 22:10:49 Phantom_Hoover: Long hair + ULTRA-SOFT PERSONALITY YO 22:11:00 + young so no GRATUITOUS BODILY HAIR AND ADAM'S APPLE = Female! 22:11:08 wait until you hit puberty :( 22:11:42 Hey, I have. It's just taking its sweet, sweet time :P 22:12:28 -!- Phantom_Hoover has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838]). 22:16:38 -!- mano0o0 has left (?). 22:16:46 ;( 22:17:01 alise_: Your girliness was pretty conclusively proven by that one video, you know. 22:17:26 video ? 22:17:47 fax: I showed my female genitals! (not really) 22:17:51 gross 22:19:31 :| 22:20:27 |: 22:20:37 I wish someone would talk to me about deptypes 22:20:57 alise_: did you see my talk about Confloddle in the log? 22:21:36 deptypes are so depressing. it's in the name, really. 22:21:46 * Sgeo didn't see ais523's talk 22:21:49 -_-- 22:21:59 Sgeo: it's a new esolang I'm thinking about 22:22:09 tarpit, as usual; I like tarpits that work differently from other tarpits 22:22:16 fax: So SAY SOMETHING! 22:22:19 tits 22:22:47 the only data type is the list (also function literals, but functions can't be manipulated in any way, just run, and there are no closures) 22:22:55 fax: Okay, how about this: Make a paraconsistent deptyped language. 22:23:05 and there are only two operators/commands, cons and foldl 22:23:11 I don't know what paraconsistent it but it sounds stupid 22:23:21 cunning tarpal syndrome 22:23:23 I'd explain but I've forgotten how to spell a word 22:23:25 And google isn't loading 22:23:26 sec 22:23:40 That is, p and ~p are allowed to coexist (dialetheia). You could do this by weakening _|_ -> forall a, a. 22:23:45 I think this leads to a TC lang with 5 characters re<>: without cheating (the same way that BF is 8 ,.<>+-[] without cheating, although of course BF can be cut down) 22:24:32 ais523: Nested folding on infinite lists seems trivially TC to me. 22:24:37 ais523: idea -- eliminate > 22:24:40 < lasts til end of program? 22:24:46 no, <> delimit a function 22:24:52 No <> is foldr 22:24:57 <> is foldl 22:25:00 er right 22:25:02 and what's inside them is the function you fold on 22:25:04 With infinite lists maybe this is acceptable, just having < last until EOF 22:25:09 Try it. 22:25:12 also, there's only one infinite list 22:25:30 necessary because you can't return an infinite list in finite time 22:25:49 < until EOF isn't obviously sub-TC, though 22:26:23 fax: http://en.wikipedia.org/wiki/Paraconsistent_logic 22:26:23 go for it 22:26:31 ais523: Exactly. 22:26:38 Wait, how do you combine r and e? 22:26:44 oh, is re cons r e? 22:26:52 no, it's reverse-polish 22:26:55 re is a syntax error 22:26:59 re: is cons r e 22:27:09 oh, I didn't see : 22:27:35 and is foldl `cons` [] 22:27:37 in other words, list reverse 22:27:41 e yep 22:27:48 yep again 22:27:51 "so you can get the first element of a list with " 22:28:08 Can this be written without >? 22:28:14 not obviously 22:28:17 Perhaps by accumulating something into the result then folding on that. 22:28:58 fax: So you want me to talk, then you dismiss and ignore me? 22:29:03 hi 22:29:06 I think you have to grab the results of a calculation at the start of the next iteration of the main loop 22:29:10 I didn't want to interrupt ais 22:29:19 we can interleave :) 22:29:22 or use /msg 22:29:24 fax: this is IRC, if you can't have two conversations at the same time you aren't concentrating enough 22:29:34 ais523: ooh, nice 22:29:39 but it has to be part of the main fold 22:29:45 yes 22:29:57 if we're having trouble just expressing first element of a list, this is either sub-tc or brilliantly TC 22:30:02 and you have Confloddle's general issue with initialising 22:30:23 the real problem here, is that insisting on using < but not > means that you can't get the return value from <> immediately 22:30:30 you only get it in r on the next iteration of the loop 22:30:39 -!- Phantom_Hoover has joined. 22:30:47 fax: http://en.wikipedia.org/wiki/Paraconsistent_logic#Relation_to_other_logics dual-intuitionistic logic may be a good place to steal things from 22:30:52 but it has to be a proper language not just a logic 22:30:56 okay 22:31:04 ais523: so basically we need 22:31:20 if we're done then hmm, for sake of argument, say we have a unary operator o that outputs a list to stdout, so we have something concrete to aim for, and likewise a nullary i that grabs a list from input 22:31:37 can we input a list and output its first element? 22:31:49 -!- Phantom_Hoover has quit (Client Quit). 22:32:35 hmm, I can't think of an obvious way, but that doesn't mean there isn't one 22:32:47 i what does this produce? 22:33:10 what list to we operate on by default again? 22:33:17 {{},{},{},...? 22:33:18 an infinite list of null lists 22:33:20 yep 22:33:33 so e in the main loop is useless as it's always null 22:33:40 I was thinking about maybe using it for input, but am not sure 22:33:44 input-only would be... weird 22:34:08 (leaving the main-loop r as a null list would be an obvious way to end a program, btw, because it provably goes into an infinite loop if you do that) 22:34:41 so i replaces the main list with the input? 22:34:46 I think that's wrong, it should cons it on 22:34:49 so {thelist,{},{},{},... 22:34:58 that way we could use the following lists as storage, somehow 22:35:01 by folding into them 22:35:25 r is the only storage you get in the main iteration, but it's enough 22:35:27 you can cons onto it 22:35:33 the general rule is that r is storage, e is input 22:35:41 for the inside <>, so why not for the main loop too? 22:35:58 ? 22:35:58 so what does Xr: do 22:36:10 just that 22:36:10 what list does it result in, using X as a var 22:36:29 [X | r] (prolog syntax) 22:36:41 what is r 22:36:50 r is the result of the last iteration of the current <> 22:36:53 ffff 22:36:55 just this program 22:36:56 on its own 22:36:56 Xr: 22:37:01 what result does it yield? 22:37:25 well, the main loop doesn't leave a result at all, but the value of r on each iteration goes [X] [X X] [X X X] and so on 22:37:51 so if you can imagine you're using Proud or some other uncomputable lang to implement this, the return value is an infinite list of Xs 22:37:56 but in a TC system, you never get that far 22:38:41 oh, you could 22:38:46 consider haskell 22:38:49 well, you could optimise that case 22:38:51 fix (1:) = [1,1,1,1,1,1,... 22:39:01 hmm, ooh, lazy evaluation? 22:39:02 ais523: ok, so r is {}? 22:39:09 at the start 22:39:12 r is initially a null list, yes 22:39:14 for any <> 22:39:17 so the whole program is a fold, right 22:39:18 so 22:39:19 er: 22:39:25 what result does that yield 22:39:29 e and r are both {} 22:39:31 so it should be {{}} 22:39:37 so you should get {{{}}, {{}}, ... 22:39:38 right/ 22:39:38 no, the entire program's implicitly in a <> 22:39:41 *right? 22:39:47 oh, good point 22:39:49 so you get... 22:39:54 outside <> e and r have no meaning, but you can't be outside a <> 22:39:55 { {{}, {}, {}, {}, ...} } 22:39:56 I think 22:40:03 no, because the return value is the final value of r 22:40:20 there isn't a "final" one, but if there was, it would be [ [] [] [] [] [] ... ] 22:42:12 so erm 22:42:15 so er: is nop 22:42:24 ais523: but do you see, that the main foldl, 22:42:29 means that you can do 22:42:30 x and get a nested fold? 22:42:36 it's > 22:42:38 yes, I see that 22:42:44 I bet we can use the main fold as storage for inner ones 22:42:48 hmm... cons ought to be prefix 22:42:48 in fact, that's obviously the only way to do practical non-> programs 22:42:51 and so do I 22:42:52 so we can do :xy<... 22:42:56 erm 22:42:57 :x<... 22:43:03 I agree that prefix is much better than postfix in non-> programs 22:43:10 postfix would be better for non-< programs 22:43:16 also, just make it foldr and I think you can do laziness trivially 22:43:20 and hey, a small syntax change doesn't matter if you're trying to tarpit something more 22:43:28 also, foldr is really laziness-hostile 22:43:34 because it starts with the last element of a list 22:43:40 and to determine that, you have to force it 22:44:09 -!- augur has quit (Ping timeout: 265 seconds). 22:44:10 OTOH, foldl doesn't work too well either, because you have to force it to determine the final value of r 22:45:31 fax: http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520 22:45:39 ais523: that is not what foldr is... 22:45:58 oh, I see 22:46:05 foldr f x [e1,e2,e3,...] = f e1 (f e2 (f e3 x)) 22:46:09 it works on infinite lists 22:46:13 unlike foldl 22:46:17 a lazy foldr, to determine the final r, you determine the final e and the penultimate r 22:46:22 and the second can be left lazy 22:46:26 consider foldr (:) [] [1..] 22:46:31 -> (:) 1 ((:) 1 ... 22:46:36 -> [1,1,1,...] 22:46:39 yep, I get it now 22:46:58 is cons and foldr TC, though? 22:47:02 -!- Phantom_Hoover has joined. 22:47:14 how do you, say, get the last element of a list? or the second? 22:47:19 getting the second seems easier 22:47:48 -!- Phantom_Hoover has left (?). 22:47:49 Prelude> take 10 $ foldr (\n xs -> n : map succ xs) [] [1..] 22:47:50 [1,3,5,7,9,11,13,15,17,19] 22:47:57 ais523: btw foldr = foldl, they're implementable in terms of each other (lazily) 22:48:05 also, last element of a list with foldr... 22:48:15 not purely each other, surely, you need to mess with at least some other primitives? 22:48:22 and if there's something confloddle is short of, it's primitives 22:48:41 first is 22:48:44 ais523: nope 22:48:45 well 22:48:47 with cons and stuff 22:48:49 anyway 22:48:51 first elem is 22:48:56 the "stuff" is the problem 22:49:01 first is , anyway, with foldr 22:49:05 hmm... let's make it >e< 22:49:06 foldr' (\x _ -> x) [1,2,3] 22:49:10 *foldr1 22:49:12 different notation so it's clear that we're doing something different 22:49:13 (not that that exists, but) 22:49:17 wait yes it does 22:49:23 although it's a -> a -> a ofc 22:49:26 which is upsettingly restricting 22:49:38 but that doesn't concern you since yours is dynamically typed 22:49:38 foldr1 does exist in Haskell 22:49:39 but 22:49:46 don't you want an initial value? 22:49:56 confloddle's is (foldl []) though 22:50:02 last element is 22:50:05 foldr1 (\x y -> y) 22:50:11 (isn't that easy?) 22:50:19 alise_, did I mention that I'm considering making a Scheme? 22:50:20 that's cheating 22:50:24 no it is not 22:50:25 foldr1 special-cases the last eleemnt 22:50:30 ???? 22:50:35 oh you are right 22:51:19 btw reverse is 22:51:24 foldr (\x y -> y ++ [x]) 22:51:38 you can do head on that 22:51:53 sp 22:51:53 so 22:52:07 foldr [] (\x _ -> x) . foldr [] (\x y -> y ++ [x]) 22:52:26 that fails to type but whatever :) 22:52:30 the [] should be after 22:52:57 Prelude> (foldr (\x _ -> x) [] . foldr (\x y -> y ++ [x]) []) [[1,2],[3,4]] 22:52:57 [3,4] 22:53:28 I agree with that definition, but ++ looks hard to do in a foldr-version of confloddle (conflodder?) 23:05:10 I did ++ 23:05:13 folr (\xs ys -> foldr (:) ys xs) [] 23:05:15 *foldr 23:05:40 I don't see how that works 23:05:45 how would you write that in conflodder? assuming > exists 23:05:47 because the whole thing seems to only take one argument 23:05:56 [list1,list2] 23:06:12 i.e. list1list2[]:: 23:06:26 and it's hard to do easily, because there's no way to have a second arg to foldr of anything but [] 23:06:44 in confloddle you can get around that by putting every element into a singleton list, and messing around with cons and last 23:06:47 fax: try and make a logic-computation isomorphism for http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520 23:06:53 so where statements in that are types; give them semantic values 23:07:03 ais523: So do that 23:08:06 as in, instead of [a b c] you have [[a] [b] [c]], then foldl x y z is the same as foldl (\r -> x (last (cons y r))) [] z 23:08:16 I think, I may have got the arguments the wrong way round 23:08:32 so do that :) 23:08:39 you have circularitiy problems trying that trick with foldr, though, as you'd have to implement last first 23:08:55 and the same trick doesn't work with first, unfortunately 23:09:11 fax: http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520 23:09:11 erm 23:09:20 ugh 23:09:22 pdf doesn't allow copying 23:09:39 fax: basically there's a dual-intuitionistic set theory that has russell's paradox but is consistent 23:09:45 ais523: Hey, I implemented last. 23:09:55 thsat's cscrewad 23:09:58 (foldr (\x _ -> x) [] . foldr (\x y -> y ++ [x]) []) 23:10:06 fax: please learn to type :| 23:10:08 anyway do it! 23:10:10 yep, but that's implemented in terms of ++ 23:10:17 it will be fucking awesome to have computational dual-intuitionistic 23:10:23 ais523: ah :-D 23:10:25 What does it mean for something to have Russell's paradox but be consistent... 23:10:34 uorygl: it means it allows p & ~p 23:10:39 which is what paraconsistent logics do 23:10:42 Oh. 23:11:05 dual-intuitionistic logic is intuitionistic logic's goatee-sporting, paraconsistent twin 23:11:05 the major issue with foldr is finding just some way to do a foldr1 or a foldr with non-[] second arg or last or ++ or, well, anything 23:11:24 * alise_ defines fold f = foldr f [] to keep himself honest 23:11:30 I wonder if intuitionistic logic and paraconsistent logic are isomorphic somehow. 23:11:34 ais523: maybe you should have a better last thing than [] 23:11:41 uorygl: Paraconsistent logic is a class of logics. 23:11:49 I can't think of anything obvious; maybe I should go at it Wolfram-style and just generate loads of Conflodder programs to see if any do last 23:11:55 Intuitionistic logic's "opposite", dual-intuitionistic, is paraconsistent. 23:12:02 * uorygl nods. 23:13:06 So, does the Web have any proof databases that accept all and only valid proofs? 23:13:14 Using an automatic proof verifier, of course. 23:13:20 metamath 23:13:44 ais523: 23:13:45 -!- tombom has quit (Quit: Leaving). 23:13:45 Prelude> fold (\xs ys -> fold (\xs' ys' -> (xs' : ys') ++ ys) xs) [[1,2],[3,4]] 23:13:46 [1,2,3,4,3,4] 23:13:50 Can I simply submit a proof to Metamath and see it appear? 23:13:52 it's incorrect and depends on ++ but I think I'm honing in on a solution 23:13:55 I'll ask #haskell 23:13:56 uorygl: no. 23:13:59 fax wants that 23:14:30 I also want that. 23:14:43 If fax is a programmer, maybe we can collaborate on getting that. 23:15:30 fax hates programming 23:15:33 It's a project of mine though 23:15:37 Metastruct 23:16:13 It's a project of yours? Neat. 23:16:45 Yes. No work done yet, but... 23:16:48 What programming language are you using, and what proof system are you using? 23:16:52 My own, my own. 23:17:02 Same here. It's a project of mine with no work done. :P 23:17:13 #haskell seems a non-obvious place to ask for easolangs 23:17:15 Well. The proof system (dependent language) will be written in Haskell and so will be the website, but... 23:17:15 Except mine's called Kallipolis, written in Haskell, using Agda. 23:17:22 Why not write it in Agda? 23:17:34 Hmm. 23:17:41 uorygl: Agda doesn't have proof irrelevance 23:17:43 sucks to be you 23:17:50 Proof irrelevance? 23:17:51 alise_: somewhat offtopic: "I object to this attempt to initiate an Emergency. Per rule 31 of the previous ruleset, the change to the gamestate that prevents us from making arbitrary rule changes is cancelled retroactively, and we're still in the BGora Era." 23:17:57 does that even work? 23:18:12 uorygl: Google it. 23:18:32 ais523: wat. 23:18:38 hmm... idea 23:18:47 Google's not giving much useful. 23:19:59 23:18 alise_: can you write reverse with foldl, then do a left fold (which is a right fold on the original), and then reverse again if you produced a list? 23:19:59 23:18 as in can you flip the arguments to cons? 23:20:03 ais523: in confludder 23:20:18 So what's proof irrelevance? 23:20:25 alise_: that's how you do foldr in terms of foldl 23:20:29 uorygl: Didn't I tell you to google it? 23:20:32 rather than vice versa 23:20:45 alise_: yes, and I did Google it, and I came away with no impression of what it is. 23:22:07 Hmm, is it the equality of all proofs of a statement? 23:22:14 uorygl: Yes. 23:22:16 Agda doesn't even have equality testing. 23:22:19 Yes it does. 23:22:24 See the standard library. 23:22:41 Really? Huh. 23:22:50 data _===_ : {A:Set} -> (x:A) -> A -> Set where refl : x === x 23:23:04 Use Coq or something else with proof irrelevance. 23:23:13 At least until they add it. 23:24:01 Why is proof irrelevance so important? 23:24:34 because it simplifies a lot of stuff. 23:27:52 23:26 > let xs ++ ys = let f = foldl (flip (:)) in f (f [] xs) (f [] ys) in "abc " ++ "alise_" 23:27:53 23:26 "alise_ cba" 23:28:11 foldr fial 23:28:12 *fail 23:29:54 uorygl: for instance proof irrelevance makes equality nicer 23:31:47 Maybe you can write a spec for your stuff and I can write it. 23:32:03 Maybe I can do both because I hate collaborating :P 23:32:09 :P 23:33:48 someone paste me the unicode mathematical [[ ]] chars :( 23:33:53 MATHEMATICAL LEFT WHITE BRACKET or something 23:35:56 ⟦⟧ 23:36:07 took a while to find 23:36:14 thanks :P 23:36:18 and it's MATHEMATICAL LEFT WHITE SQUARE BRACKET, etc, you were almost right 23:43:03 We use G ? ?, to denote that if we reject all formulas of G, we have to reject the formula ?. 23:43:08 ufg 23:43:09 ugh 23:43:18 X -| Y 23:43:23 X 23:43:24 Y 23:43:46 fax: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.2290&rep=rep1&type=pdf 23:44:01 !haskell let x ++ y = foldr (:) y x in [1,2,3] ++ [4,5,6] 23:44:15 [1,2,3,4,5,6] 23:45:09 oerjan: no 23:45:13 fold f = foldr f [] 23:45:27 grmbl 23:46:58 hm you cannot put _either_ x or y after that for any f and get x ++ y, because [] will be wrong 23:49:40 hm that [[1,2],[3,4]] thing... 23:49:53 which would be concat not ++, but... 23:50:10 oh wait 23:50:41 well i'm not sure it is possibl 23:50:43 *e 23:51:24 yeah 23:52:37 What postscript viewer should I use for Windows? 23:52:45 gsview is nice except that it sucks, horribly.