00:00:17 <Gregor> plash is better than you.
00:03:24 <cpressey> Yay, just got HOL Light installed (under cygwin...) and proved something with it
00:04:03 <Sgeo> Someone should make Plash for Windows
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).
01:12:15 <uorygl> You could have continued using another semivowel, you know.
01:12:33 <uorygl> waw, wew, wiw, wow, wuw, wyw, yay, yey, yiy, yoy, yuy, yyy...
01:12:52 <uorygl> After that, proceed to the stuff that's almost a vowel. rar, rer, rir, ror, rur, ryr.
01:13:07 <uorygl> Then other stuff that's almost a vowel: lal, lel, lil, lol, lul, lyl.
01:13:22 <uorygl> And then some nasals: nan, nen, nin, non, nun, nyn, mam, mem, mim, mom, mum, mym.
01:34:35 <pikhq> It's a URL shortener.
01:37:12 <nooga> how is this even possible
01:37:41 <Gregor> Some country clever enough to make the greatest URL shortener ever.
01:37:57 <Gregor> Also, http://to/bleh works the same if your OS doesn't suck.
01:38:23 <nooga> but why the dot at the end
01:39:18 <Gregor> 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 <nooga> why i cannot visit pl. or com. then?
01:43:28 <Gregor> com. does work, although it forwards to www.com.
01:43:58 <Gregor> Oh, sorry, my confusion, lemme restate:
01:44:14 <Gregor> com and pl don't have A addresses, they have no host. www.com. does work, as does www.pl.
01:44:44 <Gregor> 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:47:10 <nooga> wonder who controls it
02:04:57 -!- MigoMipo has quit (Quit: Page closed).
02:07:32 <uorygl> In zone files, domain names ending in . are absolute and domain names not ending in . are relative.
02:08:25 <uorygl> 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:53:22 <Oranjer> code red! quarantine broken!
03:54:29 * uorygl wraps nooga_ in plastic.
03:54:54 * uorygl pokes breathing holes in the plastic.
03:55:07 * uorygl pokes speaking holes in the plastic.
03:55:29 * uorygl pokes speaking articulately holes in the plastic.
03:55:32 <nooga_> that would actually make the plactic wrap pointles
03:55:45 * uorygl wraps the holes in plastic.
03:56:36 <uorygl> Hey, now. The holes still exist, so you can still breathe and speak and speak articulately through them.
03:56:54 <uorygl> But they're also wrapped in plastic so no contaminants can get out.
04:06:16 <nooga_> isn't france in the same time zone with warsaw?
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 <Phantom_Hoover> 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:33 -!- lifthrasiir has joined.
14:03:52 -!- BeholdMyGlory has quit (Remote host closed the connection).
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:51 <fizzie> 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 <fizzie> (Yes, I noticed he is gone already.)
14:50:00 <Deewiant> What's the environment variable restriction in cfunge's sandbox mode useful for?
14:50:40 <augur> 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
15:04:07 <augur> theres this thing called Intelligence Squared
15:04:25 <augur> they held a debate last year on whether or not the catholic hcurch was a force for good in the world
15:04:44 <augur> and they subsequently had a vote of the people who were present for the debate
15:05:02 <augur> pre-debate, the numbers were like 1000 no, 700 yes, 300 dont know
15:05:06 <augur> after it was like 1750 no, 200 yes, 50 dont know
15:08:45 -!- alise has joined.
15:09:12 <alise> #alise, please. I do not want this to be logged.
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 <alise> 06:21:54 <Quadrescence> I wonder how small one can make a decent forth compiler in C
15:26:58 <alise> http://www.ioccc.org/1992/buzzard.2.design
15:28:59 -!- alise_ has joined.
15:31:28 -!- alise has quit (Ping timeout: 252 seconds).
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:52 <alise> 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:17:59 <fax> because nothing was said
16:18:16 <alise_> There was -- in #alise2.
16:18:30 <alise_> (In /msg only, please. I do not want it leaking)
16:19:07 -!- fungot has joined.
16:19:14 <fax> 15:31 -!- alise [~95fee059@gateway/web/freenode/x-uykmcysttrftzukr] has quit [Ping timeout: 252 seconds]
16:19:18 <fax> 15:31 < alise_> test
16:19:20 <fax> 15:31 < fax> test
16:19:24 <alise_> I mean what I told you at the start.
16:19:25 -!- Phantom_Hoover has joined.
16:19:31 <alise_> In */msg only. Please.*
16:19:33 <fax> you want me to show you what you told me?
16:20:08 <alise_> fax: Yes. In /msg, in a private pastie. Please?
16:20:39 <alise_> So I can show it to someone else...
16:20:41 <alise_> Because this client doesn't log...
16:21:53 -!- zzo38 has joined.
16:22:20 <zzo38> I thought about Conway's Life cellular automaton but I have idea for a variant, called KnightLife
16:22:23 <fizzie> 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:24:13 <alise_> all (0 -> all (0 -> 1)); all all all ((0 -> (1 -> 2)) -> ((0 -> 1) -> (0 -> 2))); all all ((~0 -> ~1) -> (1 -> 0))
16:24:57 <alise_> 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 <alise> ffff I hate trivial programming bookkeeping
16:34:24 <fax> I hate how I don't make much sense
16:34:31 <fax> even when I try really hard to
16:35:13 <alise> subst :: [(Integer,Statement)] -> Statement -> Statement
16:35:18 <alise> I do bookkeeping in the first argument but you also specify what to subst in there
16:35:28 <alise> so when I come across a universal quantification
16:35:54 -!- alise_ has joined.
16:35:57 -!- Asztal has joined.
16:36:09 <alise_> until it's fixed i'm not talking
16:36:12 <uorygl> zzo38: so, what does KnightLife do?
16:38:21 <fax> rpghghrounprghounyphrguorpgh
16:38:31 <uorygl> phonographphonographphonograph
16:40:02 -!- alise has quit (Ping timeout: 252 seconds).
16:41:48 <zzo38> uorygl: I thought it is obvious, isn't it? If not, I will explain
16:42:38 <uorygl> Obvious from the name?
16:42:53 <alise_> all (42 -> all (42 -> 1)) SAME FUCKING PROBLEM >_<
16:43:04 <uorygl> Maybe it's a little bit obvious, but it's not very obvious.
16:43:10 <fax> alise: I hate programming too!
16:43:14 <augur> theres a subset of non-CF languages that have linear parse time
16:43:14 <zzo38> Yes, a little bit.
16:43:34 <augur> and their conveniently representable in compact regex-like notation!
16:43:35 <zzo38> Basically the 8 surrounding cells are the knight's move cells instead of the king's move cells
16:43:38 <alise_> faxoh but I love programming
16:43:44 <alise_> not this fuking bookkeeping shit
16:43:45 <alise_> with five bbillion variables
16:43:53 <alise_> show me the input field
16:43:56 <zzo38> Now it's obvious, isn't it?
16:44:10 * augur bookkeeps alise_'s variables
16:44:33 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds).
16:44:59 <uorygl> Yep, now it's obvious.
16:45:18 -!- Phantom_Hoover has joined.
16:45:26 <uorygl> Same number of neighbors, but connected differently. Hmm.
16:47:01 <fax> pafdounafpoonufadpoundfapounadpfuondfpa
16:47:08 <alise_> seriously what is it with shitty languages that can't match patterns and keep vaariables easily
16:47:23 <alise_> i should be able to like.. modulo out that stuff to a separate block and write the rest uberpurely
16:47:26 <pikhq> "Pattern matching is hard!"
16:47:40 <alise_> pikhq: not that kind of pattern matching
16:47:50 <alise_> the kind of pattern matching that involves a recursive function to determine the OK-ness of a pattern
16:48:00 <alise_> and then dispatching on the structure you infer in it
16:48:37 <alise_> http://pastie.org/868022.txt?key=mqvjqn84rgv75aalq9arq
16:48:42 <alise_> This function is 99% fucking fluff.
16:49:03 <alise_> Now write modus ponens :: Statement -> Statement -> (Maybe) Statement. :-)
16:51:10 <alise_> You cannot ask... what is fax.
16:51:13 <alise_> Instead, you mist ask..
16:51:20 <alise_> Why did I typo "mist" for "must"?
16:51:48 <alise_> Then you will be enlightened.
16:51:57 <uorygl> alise_: so what is this language, and why must you use it?
16:52:46 <alise_> uorygl: This is ... Haskell ...
16:52:58 <Gregor> fax is the bastard child of Miss Piggy and Kermit the Frog.
16:53:32 <uorygl> 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 <Gregor> THIS - IS - AN OUTDATED - MEEEEEEEEME
16:53:35 <alise_> I wish someone actually took u my challenge to write modusponens :P
16:53:36 <pikhq> (fax is a person who is hear)
16:53:46 <augur> stop speaking japanese.
16:53:51 <alise_> uorygl: because I don't mean the trivial sense that haskell does
16:53:55 <alise_> I mean generalised book keeping
16:53:59 <alise_> http://pastie.org/868022.txt?key=mqvjqn84rgv75aalq9arq
16:54:04 <alise_> 2/3 parameters are bookkeeping
16:54:06 <pikhq> augur: 日本語を勉強する始めて。
16:54:12 <alise_> the majoritry of the code. book keeping
16:54:14 <pikhq> (start studying Japanese)
16:54:19 <alise_> if you try and code modus ponens inferrence using that,
16:54:25 <alise_> you get EVEN MORE book keeping! yay
16:55:58 <Gregor> I think I'm turning Portuguese I think I'm turning Portuguese I really think so
16:56:45 <uorygl> So just what is subst supposed to do?
16:57:30 <alise_> If the language excelled at eliminating pointless crap like that it'd be obvious from the definition.
16:57:35 <uorygl> Substitute what for what into what?
16:57:51 <alise_> Substitute for a given De Bruijn index into a logical statement.
16:57:55 <fax> programming languages don't exist
16:58:55 <alise_> (The XUL namespace file is one called there.is.only.xul; it says that. :))
17:00:22 <uorygl> 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 <alise> 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 <alise> Actually, I'm just saying that so it's clearer what I have to do.
17:09:41 <fax> alise shut up
17:09:48 <fax> have you read I am not a number, I am a free variable
17:10:04 -!- alise_ has joined.
17:11:04 <alise> I know how De Bruijn indexes work, fax.
17:11:10 <alise> I chose a bit of a shitty representation though.
17:11:15 <fax> I know how your mom works
17:11:41 <alise_> What do you mean, "'fax' what"?
17:11:48 <fax> alise shut up have you read it??
17:12:02 <alise_> How can I do both simultaneously?
17:12:08 <fax> JUST!!!! DO!!!!!
17:12:34 <Phantom_Hoover> 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 <Sgeo> 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 <alise> mIRC users: how the fuck do you set the default font for all subdinwws?
17:22:54 <Sgeo> Why the fuck would you use mIRC?
17:22:58 <Sgeo> Sorry for the language
17:23:23 <alise> 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 <alise_> ...and then it inexplicably crashed
17:25:29 <Sgeo> alise, Silverex?
17:25:39 <alise_> No, mIRC. Or maybe I quit it...
17:26:23 -!- alise_ has quit (Client Quit).
17:26:27 <Sgeo> 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:22 <alise_> 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 <alise> 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:30:49 <alise> Hopefully a permanent client should make my IRC more reliable.
17:30:57 <alise> Is there anything better than Pidgin yet for Windows IMing?
17:31:05 -!- MarcoAchur1 has left (?).
17:31:36 <fax> nekwhat's the apb
17:36:43 -!- adam_d has joined.
17:37:20 <Sgeo> I recently tried switching to Digsby
17:37:28 <alise> oerjan said something about superstrict languages where (\x. f x) evaluates f.
17:37:32 <alise> That's interesting.
17:37:35 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
17:37:47 <Sgeo> 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 <alise> Digsby is spyware, iirc.
17:38:01 <alise> Or at least obnoxiously social.
17:38:23 <Sgeo> Which one? I mind the former, the latter can be disabled as far as I've seen
17:39:12 <alise> Hmm... (\f. (\x. f (x x)) (\x. f (x x)) would evaluate (x x).
17:39:19 <alise> So even the lambda-expression of Y would diverge.
17:39:26 <alise> Is it TC, I wonder?
17:40:08 -!- BeholdMyGlory has joined.
17:45:41 <alise> Yay, I implemented it and Y does indeed diverge.
17:48:46 <fax> using divergence to check if your code works
17:57:17 <alise> Superstrict lambda calculus.
17:57:30 <alise> Where, in (\x.E), you evaluate E as far as you can without relying on x's value.
17:57:40 <alise> So (\x. f x) evaluates f before it's even applied.
17:58:55 <alise> *Main> eval (App succL zeroL)
17:58:56 <alise> \a. \b. (a ((*** Exception: Prelude.(!!): index too large
17:59:02 <alise> The verifier should have caught that...
17:59:14 <pikhq> alise: That's pretty damned crazy right there.
17:59:56 <alise> Ugh, I have some sort of horrible bug.
18:00:02 <alise> (You could argue the entire thing is a horrible bug.)
18:01:46 <fizzie> 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 <alise> I have no idea why this isn't working XD
18:04:27 * alise tries booleans instead as a test
18:06:44 <alise> I have serious variable issues.
18:09:26 <alise> Lam ((Var 1 :$ Lam (Lam (Var 1))) :$ Var 1)
18:09:30 <alise> I'm not demoting my variables sufficiently
18:14:10 <fax> alise shut up!!!!!!!!
18:14:45 <fax> 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 <Gregor> Quite an accomplishment.
18:16:50 <pikhq> The reference counting scheme it used leaked memory.
18:17:08 <pikhq> I've also made the thing compile on modern C++ compilers. :P
18:17:20 <Gregor> It used reference counting?
18:17:37 <pikhq> It leaked a metric fuckton of memory. And the author had no idea why.
18:17:43 <Sgeo> WHat's wrong with reference counting?
18:17:56 <pikhq> Sgeo: Leaks memory with cyclic datastructures.
18:18:02 <alise_> 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:17 <alise_> Not interesting enough.
18:18:25 <pikhq> Also, is somewhat overhead-heavy if done naively.
18:18:50 <fax> okay im here
18:19:55 <alise_> It would be interesting to have a language where all expressions result in infinite structures.
18:20:04 <alise_> Then reference counting would be /useless/ :)
18:20:42 <pikhq> Most of the work in making the interpreter GC'd was removing the reference counting and the inefficient pool allocator.
18:21:08 <pikhq> Adding the GC-ness was... "class Expr : public gc {"
18:23:53 <Gregor> `calc 1 metric fuckton in US fucktons
18:24:02 <fax> `calc 1000000000000000000000000000000000000000000000000
18:24:05 <HackEgo> twitterbits.com/wp-content/plugins/as-pdf/generate.php?post=11 - [21]Similar
18:24:06 <HackEgo> yodellingllama.com/?p=1183 - [16]Cached - [17]Similar
18:25:41 <Gregor> pikhq: Y'know, I'm starting to think that metric fucktons aren't even a real unit!
18:28:28 <pikhq> http://sprunge.us/OLIF It's a Lazy K interpreter that doesn't leak memory!
18:28:51 <alise_> Is it a bird? Is it a plain? No...
18:28:55 <alise_> (This is Jeopardy, right?)
18:30:29 <pikhq> (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 <alise_> (The latter is unlikely.)
18:35:31 <fax> Mogensen-Scott is best
18:35:35 -!- Phantom_Hoover has joined.
18:36:04 <alise_> How do you encode Nil | Cons ? List in Mogensen-Scott? I have:
18:36:08 <alise_> Cons = \head tail f g x. tail f g (g head x)
18:36:10 <alise_> S = \nat f g x. nat f g (g x)
18:36:12 <alise_> A = \val f g x. f val x
18:36:12 <alise_> B = \val f g x. g val x
18:36:29 <Phantom_Hoover> Are there any people acquainted with the Linux kernel here?
18:36:57 <alise_> 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 <alise_> If there is no recursion in the type, then you simply call the appropriate function.
18:37:13 <fax> alise weird
18:37:32 <alise_> 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 <alise_> I may have the function types wrong; forgot about the \x. bit.
18:37:56 <alise_> fax: I think it's the most natural encoding.
18:38:00 <alise_> Case analysis is built-in as the distinct functions.
18:38:11 <alise_> Decomposition of the value also is built-in to each function's argument.
18:38:22 <alise_> And it transforms type recursion into value recursion.
18:38:43 <alise_> So the relevant function gets the /already decomposed, according to your will/ substructure as its argument.
18:39:21 <alise_> fax: and you know what?
18:39:24 <alise_> Prelude> :t cons (1::Integer) (cons 2 nil)
18:39:24 <alise_> cons (1::Integer) (cons 2 nil)
18:39:24 <alise_> :: (t21 -> t2) -> (Integer -> t21 -> t21) -> t21 -> t2
18:39:28 <alise_> It encodes types as their fold.
18:39:31 <alise_> I think their left fold.
18:39:36 <alise_> Maybe right-fold would be more elegant.
18:40:28 <alise_> So succ would be \nat f g x. g (nat f g x)
18:40:43 <alise_> cons would be \hd tl f g x. g head (tail f g x)
18:40:48 <alise_> fax: is that morgonson?
18:41:10 -!- sebbu2 has joined.
18:41:18 <alise_> 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 <alise_> Leaf = \val f g x. f val x
18:46:44 <alise_> Branch = \left right f g x. left f g (g (right f g x) x)
18:46:44 <alise_> Branch = \left right f g x. g (left f g x) (right f g x)
18:46:55 <alise_> I think the latter is better.
18:47:00 <fax> alise did you see my post that uses lambda calculus
18:47:24 <fax> on the blog
18:47:46 * alise_ attempts to google to find it again
18:49:33 <alise_> church numerals are like this but with f=id
18:49:50 <alise_> and church numerals are A/B without the extra x (equivalent under n)
18:50:55 <alise_> wait i can't have f = id
18:50:57 <alise_> A = \val f g x. f val x
18:50:57 <alise_> B = \val f g x. g val x
18:51:47 <alise_> :: (t -> (t2 -> t3 -> t4) -> t1 -> t2)
18:51:47 <alise_> -> (t -> (t2 -> t3 -> t4) -> t1 -> t3)
18:56:45 <alise_> hmm it should be f x val
18:57:46 <alise_> Cons = \head tail f g x. g (tail f g x) head
18:57:50 <alise_> Er, no, that's not really right.
19:01:40 <alise_> fax: I thought of a really nice property of musing Mu for recursive datatypes.
19:02:14 <fax> musings on Mu -- sounds like a blog post
19:03:49 -!- olsner_ has joined.
19:04:59 <alise_> 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:12 <alise_> (oh and expression has some extra thing too)
19:05:16 <alise_> data Expr = Core Core | ...
19:05:20 <alise_> data Pat = Core Core | ...
19:05:24 <alise_> what if Core is recursive?
19:05:42 <alise_> data Expr = Core (Core Expr) | ...
19:05:47 <alise_> data Pat = Core (Core Pat) | ...
19:05:51 <alise_> if Core was defined with mu
19:06:02 <alise_> so we'd just do F (Mu Expr) instead!
19:06:23 <alise_> so Mu actually lets you easily express recursion-substitution of data types
19:08:44 <alise_> I think we need some way to extract the F from a Mu F
19:09:26 <alise_> that requires pattern matching on Mu :P
19:10:06 <uorygl> He's talking to whoever is listening.
19:10:14 <alise_> Well, fax would ideally respond.
19:11:36 <alise_> Using Mu-recursive types to encode recursion-substitution of data types.
19:12:17 -!- augur has quit (Ping timeout: 246 seconds).
19:13:31 <alise_> heh () becomes id in my encoding
19:14:57 <alise_> http://pastie.org/868169.txt?key=mmgxkfgi4bnnt1ix3u3jqg
19:15:37 -!- kar8nga has joined.
19:15:38 <alise_> Well, for the data types (with ? for polymorphism)
19:15:45 <alise_> The expressions, lambda-calculus
19:15:52 <alise_> The format is data Foo = ..., in my representation is ...
19:16:33 <alise_> 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 <alise_> Oh, and a value of the type of the first argument of each function.
19:17:05 <alise_> 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:20 <alise_> 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 <alise_> (This is repeated for each recursive element, as different arguments to the function.)
19:17:40 <alise_> Leaf = \val f g x. f val x
19:17:41 <alise_> Branch = \left right f g x. g (left f g x) (right f g x)
19:17:55 <fax> I was away having dinner
19:18:23 <alise_> fax: That is NOT ALLOWED.
19:18:32 <fax> I didn't know
19:18:46 -!- oerjan has joined.
19:18:55 <alise_> fax: well READ WHAT I SAID :|
19:18:58 <fax> hi oerjan!
19:19:00 -!- MizardX- has joined.
19:19:03 -!- MizardX- has quit (Remote host closed the connection).
19:19:09 <fax> alise encoding data into lambda calculus is boring though
19:19:21 -!- MizardX- has joined.
19:19:23 -!- MizardX- has quit (Changing host).
19:19:23 -!- MizardX- has joined.
19:19:43 <fax> so where does calulus happen?
19:19:53 <fax> real numbers, finite numbers, data
19:19:55 <fax> what else ?
19:20:10 <alise_> Calculus :: * -> BranchOfMathematics
19:20:18 <alise_> fax: What is there that is not data?
19:20:20 <Phantom_Hoover> Wait, there's and implementation of real numbers on the lambda calculus now?
19:20:23 <alise_> Function calculus perhaps?
19:20:24 <fax> I don't mean lambda calculus
19:20:34 <fax> I mean like "derivatives" and "integrals"
19:20:38 <alise_> Phantom_Hoover: The computable reals are expressible in just about any language.
19:20:45 <fax> on data I mean specifiically: d for data
19:20:46 <alise_> Well-typed at compile time in dependent languages.
19:20:54 <fax> please just understand what I mean :|
19:21:11 <alise_> 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 <fax> yeah, for computable reals you don't even need recursion
19:21:36 <fax> "recursion"
19:22:10 <alise_> yeah if you can do rationals and semi-recursive functions
19:22:12 <alise_> 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 <alise_> you could even model them in brainfuck if you came up with a function representation
19:22:36 <fax> I should implement some reals, but I'd need quotient field.....
19:22:44 <fax> and I have implemented it but not proved it a field yet
19:23:24 <alise_> I always make that mistake
19:23:53 <fax> alise ill tell you the defintion from my bok
19:26:36 <alise_> really what you need is a cauchy sequence that's all :P
19:27:23 <fax> 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 <fax> 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 <alise_> yeah but if you have an infinite sequence... well that's a function
19:28:33 <alise_> and it's nicer to use if you have the indices be Q+s
19:28:46 <fax> This relation is clearly reflexive and transitive; its transitivity is a consequence of 6.1
19:28:50 <alise_> also equality on the computable reals doesn't always terminate if they're nonequal which sucks
19:28:55 <alise_> imo, using === is better
19:29:03 <alise_> then you just have to prove they're equal or not :))))
19:29:17 <fax> yeah equality is not decidible on R, that's a classical statement
19:29:30 <fax> that =_R I gave above is a proposition
19:30:01 <fax> alise want to show you something really cool I saw today
19:30:04 <alise_> i know it's well known
19:30:15 <fax> what sucks??
19:30:27 <oerjan> alise_: um if they're nonequal obviously it terminates, it's the equal case that is problematic
19:30:27 <fax> alise, read this http://coq.inria.fr/stdlib/Coq.Reals.Rlogic.html
19:34:08 <oerjan> 09:39:12 <alise> Hmm... (\f. (\x. f (x x)) (\x. f (x x)) would evaluate (x x).
19:34:08 <oerjan> 09:39:19 <alise> So even the lambda-expression of Y would diverge.
19:34:23 <alise_> "transClause :: ..." ;; Mr, now Mrs Clause
19:34:25 <oerjan> well but that expression is unusable in a (just) strict language anyway
19:35:14 <alise_> Theorem not_not_archimedean :
19:35:19 <alise_> forall r : R, ~ (forall n : nat, (INR n <= r)%R).
19:35:29 <alise_> having lambda-expressions diverge is hilarious
19:38:10 <oerjan> 10:17:56 <pikhq> Sgeo: Leaks memory with cyclic datastructures.
19:38:27 <oerjan> i don't think lazy-K has cyclic datastructures, but i haven't investigated it
19:38:35 <fax> alise did you read it???
19:39:00 <oerjan> because it doesn't have Y as a primitive
19:39:25 <fax> now what 'sucks'?
19:39:57 <oerjan> although on the other hand _that_ might perhaps cause memory leaks with recursion that an efficient Y wouldn't give
19:40:22 <alise_> fax: non-propositional equality on reals
19:40:40 <fax> the consequence of decidible equality
19:41:00 <fax> think about classical logic as contained inside constructive..
19:41:05 <oerjan> or perhaps that just causes a lot of duplicate evaluation.
19:41:38 <alise_> 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 <fax> im just talking :|
19:44:03 <fax> you think im stupid!!
19:44:05 <fax> ill show you
19:44:09 <alise_> fax: also i'm beginning to think pattern matching in function heads is overrated in dependent langs...
19:44:45 <alise_> I don't think you're stupid ffs :)
19:44:47 <fax> bI don't think a denpendent language needs to support pattern matching
19:44:56 <alise_> I mean as a syntactic thing
19:44:58 <fax> but it should be able to add pattern matching
19:45:05 <alise_> because often pattern matching has drastic effects on the structure of the other arguments
19:45:16 <alise_> so a possibly-nested case expression makes this much clearer
19:45:29 <alise_> and often the analysis is more complex than just does-this-constructor-match
19:45:31 <fax> well you can try programming with nested cases in Coq
19:45:36 <alise_> and function-head matching doesn't really aid that
19:45:55 <fax> at one point I just gave up an implemented (an ad-hoc bug* ridden version of) dependent pattern matching
19:46:17 <fax> (* not actually able to produce wrong results.. but sometimes might not produce any result)
19:47:15 <alise_> well i mean i like dependent pattern matching
19:47:26 <alise_> but I'm specifically criticising
19:47:50 <fax> yeah but you know case
19:47:53 <fax> you can't just write
19:48:08 <fax> f x = case x of X ... -> ... ; Y ... -> ...
19:48:11 <fax> if it's dependent
19:48:17 <fax> you have to say something about the types
19:48:37 <fax> well.................... you do in Coq, is this a fundamental thing though?
19:48:47 <alise_> what do you mean say something about the types btw?
19:48:50 <fax> ISTR augustss writing about it being essential
19:48:53 <fax> well I blogged about it
19:49:33 <oerjan> 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:51 <fax> he just does that on purpose
19:49:56 -!- augur has joined.
19:50:34 <oerjan> fax: um that Ping timeout thing isn't is server generated?
19:50:49 <fax> he pulls the plug out 265 seconds before someone talks to him
19:53:14 <alise_> I should have a specialisation of id called ff
19:53:39 <fax> that ? must have been a 'T'
19:53:56 <fax> looks like Omegamega
19:54:02 <oerjan> hm indeed user quit messages are prefaced with Quit:
19:54:32 <oerjan> (the format changed when they switched ircd)
19:54:48 <alise_> toProp : (b : Bool) -> Sigma (P : Prop) (cond [b => P, not b => ~P])
19:55:00 <alise_> cond [b => T sigma tt, not b => _|_ sigma ff]
19:55:22 <alise_> wondering if i should use case analysis instead of cond
19:55:59 <alise_> I should have ?: with a nicer name :)
19:56:41 -!- Phantom_Hoover has joined.
19:56:59 <oerjan> <oerjan> Phantom_Hoover: that Talk: Befunge message you responded to is spam (try googling it)
19:59:46 <oerjan> 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 <ais523> after a while you get a sense as to what's spam and what isn't
20:00:03 <ais523> oerjan: does the page need deleting? or is there legit content on it too?
20:00:19 <oerjan> ais523: i already removed that section, there are lots of legit ones
20:01:12 <alise_> i have an excellent spam 'n phish o mometer
20:01:15 <fizzie> 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 <fungot> fizzie: i was born in a barn?". i assume you'll mostly just want " how did you get my privmsgs?
20:01:31 <alise_> Born in a Barn. fungot. The autobiography.
20:01:32 <fungot> alise_: distributive property for example i wrote program as an ast? i believe the right way
20:01:49 <oerjan> 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:04:04 <ais523> oerjan: that spam is mostly pointless anyway, if they aren't spamming URLs or anything like that
20:04:53 <alise_> fax: I have a feeling I need a real system...
20:04:56 <alise_> I keep using "refl" to substitute for any a === :-)
20:05:08 <oerjan> ais523: yeah i don't understand why they're doing it either. maybe to test our spam response intelligence?
20:05:14 <fax> alise I don't understand
20:05:30 <fax> you cant use refl unless a and b are convertible
20:05:35 <alise_> fax: don't understand what, my refl thing?
20:05:37 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds).
20:05:39 <ais523> 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:49 <ais523> however, in that case I don't see how they'd be getting past the CAPTCHA
20:05:52 <alise_> toProp b === T sigma tt? well obviously, it's true!
20:06:05 <fax> that's extentional equality!!!!!
20:06:10 <ais523> spambots generally need some knowledge of how an individual CAPTCHA works before breaking it
20:06:35 <oerjan> ais523: does our wiki have a special captcha?
20:06:50 <ais523> no, it's MediaWiki's default captcha
20:06:59 <ais523> and a very easily broken one, at that
20:07:01 <oerjan> i don't recall seeing it
20:07:19 <alise_> btw how is apartness defined?
20:07:22 <oerjan> ais523: which means the spammers probably know all about it since a long time ago
20:07:33 <ais523> the CAPTCHA rules are that they come up on attempts to register accounts, and edits by anons that add URLs
20:07:39 <alise_> I thought of having as an argument to the constructor a proposition for which P x but not P y
20:07:40 <ais523> thinking about it: this spam isn't actually adding URLs
20:07:45 <ais523> so it doesn't need to go past the CAPTCHA at all
20:08:06 <oerjan> 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 <oerjan> (it talked about creating articles)
20:09:35 -!- mano0o0 has joined.
20:09:36 <oerjan> or maybe that's common terminology for other things than wikis too
20:09:49 <ais523> the spam just came up on my feed of all edits to Esolang
20:09:52 <ais523> nothing gets past the admins!
20:09:58 <ais523> just, sometimes other people get there first
20:10:11 <ais523> and that particular comment would make sense on a blog, too
20:10:15 <ais523> although it would mean something else
20:10:22 <oerjan> ais523: oh? what then?
20:10:37 <oerjan> an article would have to posted by a blog owner wouldn't it
20:10:55 <ais523> oerjan: it means, can someone find me more articles on this subject?
20:11:36 <oerjan> hm not quite, but i see it could be...
20:11:37 <fax> alise, I will show you apartness
20:11:47 <fax> alise I should just write this whole chapter into Coq :P
20:11:53 <oerjan> it sounds like one blogger asking another how they find ideas
20:13:31 <fax> x # y if x > y or y > x
20:13:48 <alise_> fax: just look at this pile of shit: http://pastie.org/868241.txt?key=unp3wmm109dzwe6ssnkw
20:13:54 <fax> properties: x = y /\ x # y -> 0 = 1
20:13:58 <alise_> I just cheated through the whole fucking proof by sprinkling refl everywhere! :-P
20:14:03 <oerjan> i wonder if the wiki enabled captchas after i joined (2006)
20:14:05 <alise_> fax: so apartness is only defined if you have an ordering?
20:14:12 <fax> x = y /\ y # z -> x # z (??? weird one)
20:14:17 <fax> x # y -> y # z
20:14:19 <fax> x # y -> y # x ***
20:14:26 <fax> x # y -> x # z \/ z # y
20:15: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:15:39 <ais523> oerjan: it's relatively recent, I had a discussion with Graue about it
20:16:03 <fax> alise what's teh point in making that data?
20:16:07 -!- olsner_ has quit (Quit: olsner_).
20:16:08 <fax> why not just do it as a function definition
20:16:19 <alise_> oh wait I completely neglected my obligation in toBool to supply P | ~P
20:16:19 <alise_> that's why the proof was so easy...
20:18:46 <fax> 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 <alise_> toProp : (b : Bool) ? S (P : Prop) (cond b ? P; else ? P)
20:18:56 <alise_> because === is defined as data sooo
20:19:10 <fax> what's the name of like .. a strategyr
20:19:12 <alise_> well here's a definition
20:19:17 <fax> except that it's ad-hoc guidlines
20:20:13 <fax> my hooristikc is to define the fewest data possible, but the strongest ones
20:20:14 <alise_> apart : {A:Set} -> A -> A -> Prop
20:20:21 <fax> like if two data are similar, you can probably abstract it out
20:20:33 <alise_> apart x y = exists {P : A->Prop}. (P x /\ ~P y) \/ (P y /\ ~P x)
20:20:36 <fax> the real reason to define a data type is because you want the strength of its induction principle
20:20:44 <fax> at least that's my (current) view/understanding
20:21:04 <ais523> fax: it looks really weird whenever anyone uses the word "data" correctly
20:21:19 <alise_> http://pastie.org/868253.txt?key=nb3ny4djjrabif9xilvalq honestly toBool.toProp===id should just be "obvious"
20:21:29 <alise_> toBool.toProp===id b := obvious
20:22:20 <alise_> obvious : {P : Prop} -> cond isObvious P -> P; else -> T
20:22:43 <fax> tautology "P" -> P ?
20:23:55 <alise_> so tautology : (q : Quoted Prop) -> unquote q?
20:24:35 <alise_> fax: so what's the type containing Prop and Set in your opinion? Set_1?
20:27:15 <alise_> s : {A : Set1} ? {B : Set1} ? {P : A ? B} ? (x:A) ? P x ? S (x:A). P x
20:27:43 <alise_> s : {A : Set1} ? {B : Set1} ? {P : A ? B} ? (x:A) ? P x ? S (x:A). P x
20:28:04 -!- werdan7 has quit (Ping timeout: 619 seconds).
20:29:22 <alise_> _sigma_ : {A : Set_1} -> {B : Set_1} -> {P : A -> B} -> (x:A) -> P x -> Sigma (x:A). P x
20:30:10 <fax> alise in Coq it's Type (Type[1])
20:30:17 <fax> but I don't really have an opinion on this :P
20:30:29 <alise_> so Set : Type, Prop : Type?
20:30:55 <alise_> fax: I kinda hate having separate Sets and Props
20:31:00 <alise_> because you lose so much isomorphism and neatness
20:31:28 <fax> I don't knnow what yu mean
20:31:39 <alise_> please, please, PLEASE, when saying you don't know what i mean QUOTE the bit
20:31:41 <alise_> otherwise I can't answer
20:31:45 <fax> 20:30 < alise_> because you lose so much isomorphism and neatness
20:32:29 <alise_> P \/ ~P then just inspecting left/right to find out which it is
20:32:50 <alise_> exists <-> dependent tuple
20:35:37 -!- Phantom_Hoover has joined.
20:35:52 <fax> proofs are different than types
20:35:59 <fax> the reason is proof irrelevance
20:36:15 <fax> so why would you want to get rid of proofs??
20:36:17 <alise_> 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:48 <alise_> agda has combined proof/set... and suffers for it, but the isomorphisms are just so appealing
20:36:48 <alise_> 20:31 <alise_> for instance
20:36:48 <alise_> 20:31 <alise_> A \/ B = Either A B
20:36:48 <alise_> 20:31 <alise_> A /\ B = A * B
20:36:48 <alise_> 20:32 <alise_> P \/ ~P then just inspecting left/right to find out which it is
20:36:49 <alise_> 20:32 <alise_> forall <-> function
20:36:49 <alise_> 20:32 <alise_> exists <-> dependent tuple
20:36:50 <alise_> 20:32 <alise_> and so on, so forth
20:36:54 <fax> maybe if we used quotients!!!!
20:37:01 <fax> to make a 'proof' set
20:37:13 <alise_> well it's not prettier per se
20:37:14 <fax> I suppose that's what epigram does
20:37:16 <alise_> but the isomorphisms are elegant
20:37:18 -!- werdan7 has joined.
20:37:22 <alise_> if you don't value isomorphisms -
20:37:23 <fax> what isomorphisms?
20:37:27 <alise_> then why do we persue curry howard?
20:37:27 <fax> are you talking about curry-howard
20:37:30 <alise_> 20:31 <alise_> for instance
20:37:30 <alise_> 20:31 <alise_> A \/ B = Either A B
20:37:30 <alise_> 20:31 <alise_> A /\ B = A * B
20:37:30 <alise_> 20:32 <alise_> P \/ ~P then just inspecting left/right to find out which it is
20:37:30 <alise_> 20:32 <alise_> forall <-> function
20:37:30 <alise_> 20:32 <alise_> exists <-> dependent tuple
20:37:31 <alise_> 20:32 <alise_> and so on, so forth
20:37:44 <fax> stop pasting that, I can't see what you are saying inbetween all this pastes
20:38:04 <alise_> maybe the idea is to read the paste
20:38:04 <alise_> instead of asking for its contents
20:39:53 <alise_> those are (among the) appealing isomorphism s
20:40:22 <fax> I don't get it
20:41:23 <alise_> what part do you not get
20:41:59 <alise_> data _/\_ : (A:*) -> (B:*) -> * where both : A -> B -> A /\ B
20:42:03 <alise_> look similar to the definition of a tuple to you?
20:42:43 <fax> curry-howard is that typed lambda calculus corresponds to natural deduction ?
20:42:57 <alise_> What I was /trying/ to do is use *analogy*.
20:43:17 <alise_> Curry-Howard: Types in the lambda calculus correspond to statements in intuitionistic logic. W
20:43:24 <alise_> 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 <fax> is that a quote?
20:43:34 <alise_> So if you do not appreciate the isomorphisms I listed, why then Curry-Howard?
20:43:47 <fax> okay let me get this straight
20:44:04 <fax> no I don't get it
20:44:25 <comex> can't you use v and ^ instead? :p
20:44:31 <fax> I'm asking #haskell
20:44:34 <alise_> comex: Yeah, it's not like v is like a variable name.
20:44:42 <alise_> fax: ugh, you make no sense at all
20:45:11 <fax> this is my question:
20:45:12 <fax> what does 'Curry–Howard correspondence' have to do with dependent types?
20:45:27 <alise_> Ugh! That is IRRELEVANT to my point.
20:45:34 <alise_> Dependent languages make /good proof systems/.
20:45:40 <fax> why is it irrelevant
20:45:52 <alise_> Because/ of Curry-Howard.
20:46:37 <alise_> 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 <fax> I'm not sure what Curry-Howard is exactly
20:47:53 <fax> it seems kinda vauge, like a principle more than a formal statement
20:48:32 <fax> you needn't be so caustic
20:48:39 <alise_> 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 <Sgeo> Survived the first two points raised by LH
20:50:25 <alise_> Do you want to support such a company?
20:52:10 <Sgeo> Hm. What alternatives are there, then?
20:52:24 <Sgeo> Pidgin's been sucking for me for some reason, Digsby's company is shady
20:52:29 <alise_> It sucks but what can you do.
20:52:39 <alise_> Miranda IM is popular with the anal-retentive tweakers.
20:52:50 <alise_> A few hours and it's exactly as good as Pidgin but with more alpha-translucency.
20:53:12 * Sgeo doesn't like tweaking stuff
20:53:16 <alise_> Huh; Russ Cox wrote Code Search.
20:53:20 <fax> alise just give up on me after bitching
20:53:35 <alise_> fax: I just didn't notice what you said
20:53:40 <alise_> There are other people than you and they talk...
20:53:51 <alise_> I give up on people after I see a conversation going in circles, only.
20:55:47 <fax> people shouldn't repeat themselves if they don't like going in cirlecs..
20:55:59 <Sgeo> Can Miranda IM be made to support Facebook Chat?
20:56:14 <Sgeo> Apparently yes
20:56:52 <Sgeo> 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:59:42 <Gregor> What's wrong with Qemu?
21:00:36 <Phantom_Hoover> 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 <Phantom_Hoover> 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:43 <Gregor> Is hda a virtual disk or a filesystem? That is, is it partitioned?
21:03:31 <Gregor> Well, yuh, that should work, assuming the kernel has IDE support.
21:04:14 <Phantom_Hoover> It doesn't work with the kernel in /boot either, so I assume the fault isn't with the kernel.
21:04:59 <AnMaster> By mistake I left clicked a tab with ctrl held down in firefox
21:05:08 <AnMaster> it changed the tab title to begin with "(*)"
21:05:16 <AnMaster> repeating the click removes it
21:05:36 <AnMaster> but it seems to have no effect in behaviour
21:05:52 <AnMaster> anyone know if it is supposed to just do that, or do something else as well?
21:06:14 <AnMaster> I mean, if it is just to mark a tab, or it changes something wrt. how the tab behaves
21:07:15 <AnMaster> 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:17:29 <AnMaster> hm it does indeed seem to be related to tab mix plus
21:18:14 -!- Phantom_Hoover has joined.
21:24:56 <Phantom_Hoover> 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:42 <alise_> we backed up the frappr, so bah
21:28:32 <alise_> AnMaster has it, so do I on my other machine
21:29:31 <alise_> Apparently Digsby stopped bundling spyware, so I'll try it.
21:29:38 <alise_> Phantom_Hoover: #qemu?
21:29:51 <fax> alise alise alise alise
21:31:34 <alise_> Identify your nickname.
21:32:09 <alise_> Just Fucking Google It
21:32:26 <fax> ghost sucker: /msg nickserv help
21:32:33 <fax> don't google anything
21:32:38 <fax> google is for idiots and queers
21:33:23 <alise_> real defensed proposition you got there
21:33:27 <alise_> you included all that evidence and reasoning
21:34:44 * oerjan uses a screwdriver to fix alise_'s joke detector
21:35:32 <fax> I have to tell you this
21:35:38 <fax> Coq is a proof assistant based on dependent type theory developed at
21:35:38 <fax> INRIA [CDT08]. By default, it uses constructive logic via the Curry-Howard
21:35:38 <fax> isomorphism. This isomorphism associates propositions with types and proofs of
21:35:41 <fax> propositions with programs of the associated type. This makes Coq a functional
21:35:45 <fax> programming language as well as a deduction system. The identification of a pro-
21:35:48 <fax> gramming language with a deduction system allows Coq to reason about programs
21:35:51 <fax> and allows Coq to use computation to prove theorems.
21:35:59 <alise_> oerjan: well fax legit hates wikipedia, so...
21:38:11 <oerjan> alise_: so what you are saying is that fax incorporates poe's law all by himself?
21:40:46 <fax> alise -- are you really pissed off at me
21:41:15 <alise_> 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 <alise_> "Allow Digsby to use idle CPU time for grid computing." Uh, no?
21:42:10 <alise_> Manage all your IM, email and social
21:42:10 <alise_> network accounts with one login
21:42:13 <oerjan> fax: assuming you are referring to the Lazy Evaluation article?
21:42:17 <alise_> Suspicious. Do I have to give them my password?
21:42:24 <fax> lazy evaluation?? no
21:42:52 * oerjan beats himself for confusing fax and Phantom_Hoover ===\__/
21:43:02 <alise_> Why do I need a Digsby account?
21:43:03 <alise_> 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:06 <alise_> So: They store my password.
21:43:24 <oerjan> fax: mind you your joke detector probably needs adjustment too
21:43:42 <fax> I TAKE OFFENSE TO THIS
21:43:46 <oerjan> *Phantom_Hoover: assuming you are referring to the Lazy Evaluation article?
21:44:05 <alise_> 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 <alise_> Sgeo: I think I have said enough.
21:44:26 * alise_ gives his info anyway because dammit pidgin is /really/ badf
21:45:02 <ais523> alise_: maybe you could write your own?
21:45:13 <ais523> hmm, even telnet is usable for IRC, but only if you don't do anything else
21:45:22 <alise_> ais523: Write Windows software? Are you kidding?
21:45:37 <ais523> alise_: I'd suggest not actually using the Windows API, that would be ridiculous
21:45:37 <oerjan> */me uses the screwdriver to fix Phantom_Hoover's joke detector as well.
21:45:48 <ais523> 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 <alise_> Yes, but I'd rather just get an internet connection that doesn't suck and use it to install Ubuntu.
21:47:01 <alise_> I love talking about those things
21:47:14 <alise_> Ooh, Digsby lets you sort contact by total size of logs.
21:49:36 <ais523> does anyone hear know what the common "now you have two problems" quip against regex means?
21:50:21 <fax> what it means??
21:50:30 <fax> it means that writing regex is a bitch
21:50:35 <fax> and doesn't make things easier
21:50:53 <oerjan> ais523 is so eso-adjusted that he thinks regexes are easy :D
21:51:12 <alise_> ais523: because regexps are brittle and often have scary performance
21:51:14 <ais523> regex makes things easier if it's appropriate for the problem
21:51:22 <Deewiant> ais523: The original quote is about sed, not regex.
21:51:26 <alise_> It's a quip, it doesn't have to be actually true.
21:51:26 <ais523> just, don't use it to parse XML or stupid things like that
21:51:36 <ais523> alise_: recognised; Deewiant: ah, interesting
21:52:02 <Deewiant> The UNIX-HATERS Handbook mentions it.
21:52:11 <fax> <3 unix haters handbook!
21:52:52 <ais523> is there a windows-haters handbook?
21:53:33 <ais523> also, http://esolangs.org/wiki/Lazy_evaluation, now that's /clever/ vandalism
21:53:45 <ais523> much better than the typical "recursion" joke
21:54:15 <Deewiant> Since there wasn't any content to start with
21:55:00 <ais523> also fun: Google have made a mostly PCRE-compatible regular expression engine
21:55:48 <ais523> expanding the acronym makes your head spin
21:56:27 <fax> Firefox can't find the server at www.esolangs.org. :/
21:56:31 <Deewiant> Yes, it's the typical "fast but can't do everything" implementation using a Thompson NFA
21:56:48 <fax> http://esoteric.voxelperfect.net/wiki/Lazy_evaluation
21:56:48 <ais523> Gregor: better worst-case performance
21:57:08 <ais523> so they can let people write arbitrary regexen and evaluate them without worrying about someone sending them an algorithmic complexity bomb
21:57:10 <Gregor> Except that worst-case performance of PCRE is almost a non-issue, the worst case never comes up ...
21:57:18 <Deewiant> Most properly-maintained things use the slow algos
21:57:23 <Gregor> User-created malicious regex.
21:59:11 <alise_> the same author of the famous article about it
21:59:19 <alise_> (and the author of Google Code Search which uses it)
22:02:41 <fax> Russ Cox???
22:07:33 <ais523> fax: can't you PM alise?
22:07:45 <fax> she doesn't want to talk to me
22:08:15 <ais523> there is something wrong with this reasoning...
22:08:19 <Gregor> Mayhaps that's because you mistook him for a woman :P
22:08:36 <ais523> hey, I've been careful for ages to avoid pronouns for alise, it's more fun that way
22:08:51 <ais523> well, third-person pronouns at least
22:08:54 <alise_> Gregor: Actually, she is the correct pronoun.
22:08:59 <ais523> imagine if "I" and "you" were gendered!
22:09:03 <alise_> It in fact matches reality more than he.
22:09:06 <alise_> Most people mistake me for a girl.
22:09:28 <fax> ounapfhounfakp
22:09:35 <alise_> Hotels: "Miss (mother's surname because I'm never asked for mine)". Taxis: "[Blah blah destination] ladies?"
22:09:49 <alise_> People, to my mother: "Blah blah blah your daughter"
22:09:58 <alise_> fax: I'll talk if you say something to me.
22:10:39 -!- kar8nga has quit (Remote host closed the connection).
22:10:49 <alise_> Phantom_Hoover: Long hair + ULTRA-SOFT PERSONALITY YO
22:11:00 <alise_> + young so no GRATUITOUS BODILY HAIR AND ADAM'S APPLE = Female!
22:11:08 <fax> wait until you hit puberty :(
22:11:42 <alise_> 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:17:01 <fizzie> alise_: Your girliness was pretty conclusively proven by that one video, you know.
22:17:47 <alise_> fax: I showed my female genitals! (not really)
22:20:37 <fax> I wish someone would talk to me about deptypes
22:20:57 <ais523> alise_: did you see my talk about Confloddle in the log?
22:21:36 <oerjan> deptypes are so depressing. it's in the name, really.
22:21:46 * Sgeo didn't see ais523's talk
22:21:59 <ais523> Sgeo: it's a new esolang I'm thinking about
22:22:09 <ais523> tarpit, as usual; I like tarpits that work differently from other tarpits
22:22:16 <alise_> fax: So SAY SOMETHING!
22:22:47 <ais523> 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 <alise_> fax: Okay, how about this: Make a paraconsistent deptyped language.
22:23:05 <ais523> and there are only two operators/commands, cons and foldl
22:23:11 <fax> I don't know what paraconsistent it but it sounds stupid
22:23:21 <oerjan> cunning tarpal syndrome
22:23:23 <alise_> I'd explain but I've forgotten how to spell a word
22:23:25 <alise_> And google isn't loading
22:23:40 <alise_> That is, p and ~p are allowed to coexist (dialetheia). You could do this by weakening _|_ -> forall a, a.
22:23:45 <ais523> 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 <alise_> ais523: Nested folding on infinite lists seems trivially TC to me.
22:24:37 <alise_> ais523: idea -- eliminate >
22:24:40 <alise_> < lasts til end of program?
22:24:46 <ais523> no, <> delimit a function
22:25:02 <ais523> and what's inside them is the function you fold on
22:25:04 <alise_> With infinite lists maybe this is acceptable, just having < last until EOF
22:25:12 <ais523> also, there's only one infinite list
22:25:30 <ais523> necessary because you can't return an infinite list in finite time
22:25:49 <ais523> < until EOF isn't obviously sub-TC, though
22:26:23 <alise_> fax: http://en.wikipedia.org/wiki/Paraconsistent_logic
22:26:38 <alise_> Wait, how do you combine r and e?
22:26:52 <ais523> no, it's reverse-polish
22:27:35 <ais523> and <er:> is foldl `cons` []
22:27:37 <ais523> in other words, list reverse
22:27:41 <alise_> <r maps any list to the null list
22:27:51 <alise_> <er: is foldl `cons` []
22:28:03 <alise_> "so you can get the first element of a list with <er:><e>"
22:28:08 <alise_> Can this be written without >?
22:28:17 <alise_> Perhaps by accumulating something into the result then folding on that.
22:28:58 <alise_> fax: So you want me to talk, then you dismiss and ignore me?
22:29:06 <ais523> 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 <fax> I didn't want to interrupt ais
22:29:24 <ais523> fax: this is IRC, if you can't have two conversations at the same time you aren't concentrating enough
22:29:39 <alise_> but it has to be part of the main fold
22:29:57 <alise_> if we're having trouble just expressing first element of a list, this is either sub-tc or brilliantly TC
22:30:02 <ais523> and you have Confloddle's general issue with initialising
22:30:23 <ais523> 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 <ais523> you only get it in r on the next iteration of the loop
22:30:39 -!- Phantom_Hoover has joined.
22:30:47 <alise_> 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 <alise_> but it has to be a proper language not just a logic
22:31:04 <alise_> ais523: so basically we need
22:31:20 <alise_> if we're done then <e, else <er:
22:31:27 <ais523> 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 <ais523> can we input a list and output its first element?
22:31:49 -!- Phantom_Hoover has quit (Client Quit).
22:32:35 <ais523> hmm, I can't think of an obvious way, but that doesn't mean there isn't one
22:32:50 <alise_> what does this produce?
22:33:10 <alise_> what list to we operate on by default again?
22:33:18 <ais523> an infinite list of null lists
22:33:33 <ais523> so e in the main loop is useless as it's always null
22:33:40 <ais523> I was thinking about maybe using it for input, but am not sure
22:33:44 <ais523> input-only would be... weird
22:34:08 <ais523> (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 <alise_> so i replaces the main list with the input?
22:34:46 <alise_> I think that's wrong, it should cons it on
22:34:49 <alise_> so {thelist,{},{},{},...
22:34:58 <alise_> that way we could use the following lists as storage, somehow
22:35:25 <ais523> r is the only storage you get in the main iteration, but it's enough
22:35:33 <ais523> the general rule is that r is storage, e is input
22:35:41 <ais523> for the inside <>, so why not for the main loop too?
22:36:10 <alise_> what list does it result in, using X as a var
22:36:29 <ais523> [X | r] (prolog syntax)
22:36:50 <ais523> r is the result of the last iteration of the current <>
22:37:01 <alise_> what result does it yield?
22:37:25 <ais523> 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 <ais523> 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 <ais523> but in a TC system, you never get that far
22:38:49 <ais523> well, you could optimise that case
22:38:51 <alise_> fix (1:) = [1,1,1,1,1,1,...
22:39:01 <ais523> hmm, ooh, lazy evaluation?
22:39:02 <alise_> ais523: ok, so r is {}?
22:39:12 <ais523> r is initially a null list, yes
22:39:17 <alise_> so the whole program is a fold, right
22:39:25 <alise_> what result does that yield
22:39:37 <alise_> so you should get {{{}}, {{}}, ...
22:39:38 <ais523> no, the entire program's implicitly in a <>
22:39:54 <ais523> outside <> e and r have no meaning, but you can't be outside a <>
22:39:55 <alise_> { {{}, {}, {}, {}, ...} }
22:40:03 <ais523> no, because the return value is the final value of r
22:40:20 <ais523> there isn't a "final" one, but if there was, it would be [ [] [] [] [] [] ... ]
22:42:24 <alise_> ais523: but do you see, that the main foldl,
22:42:32 <alise_> and get a nested fold?
22:42:44 <alise_> I bet we can use the main fold as storage for inner ones
22:42:48 <alise_> hmm... cons ought to be prefix
22:42:48 <ais523> in fact, that's obviously the only way to do practical non-> programs
22:43:03 <ais523> I agree that prefix is much better than postfix in non-> programs
22:43:10 <ais523> postfix would be better for non-< programs
22:43:16 <alise_> also, just make it foldr and I think you can do laziness trivially
22:43:20 <ais523> and hey, a small syntax change doesn't matter if you're trying to tarpit something more
22:43:28 <ais523> also, foldr is really laziness-hostile
22:43:34 <ais523> because it starts with the last element of a list
22:43:40 <ais523> and to determine that, you have to force it
22:44:09 -!- augur has quit (Ping timeout: 265 seconds).
22:44:10 <ais523> OTOH, foldl doesn't work too well either, because you have to force it to determine the final value of r
22:45:31 <alise_> fax: http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520
22:45:39 <alise_> ais523: that is not what foldr is...
22:46:05 <alise_> foldr f x [e1,e2,e3,...] = f e1 (f e2 (f e3 x))
22:46:09 <alise_> it works on infinite lists
22:46:17 <ais523> a lazy foldr, to determine the final r, you determine the final e and the penultimate r
22:46:22 <ais523> and the second can be left lazy
22:46:26 <alise_> consider foldr (:) [] [1..]
22:46:58 <ais523> is cons and foldr TC, though?
22:47:02 -!- Phantom_Hoover has joined.
22:47:14 <ais523> how do you, say, get the last element of a list? or the second?
22:47:19 <ais523> getting the second seems easier
22:47:48 -!- Phantom_Hoover has left (?).
22:47:49 <alise_> Prelude> take 10 $ foldr (\n xs -> n : map succ xs) [] [1..]
22:47:50 <alise_> [1,3,5,7,9,11,13,15,17,19]
22:47:57 <alise_> ais523: btw foldr = foldl, they're implementable in terms of each other (lazily)
22:48:05 <alise_> also, last element of a list with foldr...
22:48:15 <ais523> not purely each other, surely, you need to mess with at least some other primitives?
22:48:22 <ais523> and if there's something confloddle is short of, it's primitives
22:48:56 <ais523> the "stuff" is the problem
22:49:01 <ais523> first is <e>, anyway, with foldr
22:49:05 <ais523> hmm... let's make it >e<
22:49:06 <alise_> foldr' (\x _ -> x) [1,2,3]
22:49:12 <ais523> different notation so it's clear that we're doing something different
22:49:13 <alise_> (not that that exists, but)
22:49:23 <alise_> although it's a -> a -> a ofc
22:49:26 <alise_> which is upsettingly restricting
22:49:38 <alise_> but that doesn't concern you since yours is dynamically typed
22:49:38 <ais523> foldr1 does exist in Haskell
22:49:46 <alise_> don't you want an initial value?
22:49:56 <ais523> confloddle's is (foldl []) though
22:50:19 <Sgeo> alise_, did I mention that I'm considering making a Scheme?
22:50:25 <ais523> foldr1 special-cases the last eleemnt
22:51:24 <alise_> foldr (\x y -> y ++ [x])
22:51:38 <alise_> you can do head on that
22:52:07 <alise_> foldr [] (\x _ -> x) . foldr [] (\x y -> y ++ [x])
22:52:26 <alise_> that fails to type but whatever :)
22:52:30 <alise_> the [] should be after
22:52:57 <alise_> Prelude> (foldr (\x _ -> x) [] . foldr (\x y -> y ++ [x]) []) [[1,2],[3,4]]
22:53:28 <ais523> I agree with that definition, but ++ looks hard to do in a foldr-version of confloddle (conflodder?)
23:05:13 <alise_> folr (\xs ys -> foldr (:) ys xs) []
23:05:40 <ais523> I don't see how that works
23:05:45 <alise_> how would you write that in conflodder? assuming > exists
23:05:47 <ais523> because the whole thing seems to only take one argument
23:06:26 <ais523> 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 <ais523> 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 <alise_> 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 <alise_> so where statements in that are types; give them semantic values
23:08:06 <ais523> 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 <ais523> I think, I may have got the arguments the wrong way round
23:08:39 <ais523> you have circularitiy problems trying that trick with foldr, though, as you'd have to implement last first
23:08:55 <ais523> and the same trick doesn't work with first, unfortunately
23:09:11 <alise_> fax: http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520
23:09:22 <alise_> pdf doesn't allow copying
23:09:39 <alise_> fax: basically there's a dual-intuitionistic set theory that has russell's paradox but is consistent
23:09:45 <alise_> ais523: Hey, I implemented last.
23:09:55 <fax> thsat's cscrewad
23:09:58 <alise_> (foldr (\x _ -> x) [] . foldr (\x y -> y ++ [x]) [])
23:10:06 <alise_> fax: please learn to type :|
23:10:10 <ais523> yep, but that's implemented in terms of ++
23:10:17 <alise_> it will be fucking awesome to have computational dual-intuitionistic
23:10:25 <uorygl> What does it mean for something to have Russell's paradox but be consistent...
23:10:34 <alise_> uorygl: it means it allows p & ~p
23:10:39 <alise_> which is what paraconsistent logics do
23:11:05 <alise_> dual-intuitionistic logic is intuitionistic logic's goatee-sporting, paraconsistent twin
23:11:05 <ais523> 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 <uorygl> I wonder if intuitionistic logic and paraconsistent logic are isomorphic somehow.
23:11:34 <alise_> ais523: maybe you should have a better last thing than []
23:11:41 <alise_> uorygl: Paraconsistent logic is a class of logics.
23:11:49 <ais523> 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 <alise_> Intuitionistic logic's "opposite", dual-intuitionistic, is paraconsistent.
23:13:06 <uorygl> So, does the Web have any proof databases that accept all and only valid proofs?
23:13:14 <uorygl> Using an automatic proof verifier, of course.
23:13:45 -!- tombom has quit (Quit: Leaving).
23:13:45 <alise_> Prelude> fold (\xs ys -> fold (\xs' ys' -> (xs' : ys') ++ ys) xs) [[1,2],[3,4]]
23:13:50 <uorygl> Can I simply submit a proof to Metamath and see it appear?
23:13:52 <alise_> it's incorrect and depends on ++ but I think I'm honing in on a solution
23:14:43 <uorygl> If fax is a programmer, maybe we can collaborate on getting that.
23:15:33 <alise_> It's a project of mine though
23:16:13 <uorygl> It's a project of yours? Neat.
23:16:45 <alise_> Yes. No work done yet, but...
23:16:48 <uorygl> What programming language are you using, and what proof system are you using?
23:17:02 <uorygl> Same here. It's a project of mine with no work done. :P
23:17:13 <ais523> #haskell seems a non-obvious place to ask for easolangs
23:17:15 <alise_> Well. The proof system (dependent language) will be written in Haskell and so will be the website, but...
23:17:15 <uorygl> Except mine's called Kallipolis, written in Haskell, using Agda.
23:17:22 <alise_> Why not write it in Agda?
23:17:41 <alise_> uorygl: Agda doesn't have proof irrelevance
23:17:51 <ais523> 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:18:47 <uorygl> Google's not giving much useful.
23:19:59 <alise_> 23:18 <aavogt> 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 <alise_> 23:18 <aavogt> as in can you flip the arguments to cons?
23:20:18 <uorygl> So what's proof irrelevance?
23:20:25 <ais523> alise_: that's how you do foldr in terms of foldl
23:20:29 <alise_> uorygl: Didn't I tell you to google it?
23:20:32 <ais523> rather than vice versa
23:20:45 <uorygl> alise_: yes, and I did Google it, and I came away with no impression of what it is.
23:22:07 <uorygl> Hmm, is it the equality of all proofs of a statement?
23:22:16 <uorygl> Agda doesn't even have equality testing.
23:22:24 <alise_> See the standard library.
23:22:50 <alise_> data _===_ : {A:Set} -> (x:A) -> A -> Set where refl : x === x
23:23:04 <alise_> Use Coq or something else with proof irrelevance.
23:23:13 <alise_> At least until they add it.
23:24:01 <uorygl> Why is proof irrelevance so important?
23:24:34 <alise_> because it simplifies a lot of stuff.
23:27:52 <alise_> 23:26 <aavogt> > let xs ++ ys = let f = foldl (flip (:)) in f (f [] xs) (f [] ys) in "abc " ++ "alise_"
23:27:53 <alise_> 23:26 <lambdabot> "alise_ cba"
23:29:54 <alise_> uorygl: for instance proof irrelevance makes equality nicer
23:31:47 <uorygl> Maybe you can write a spec for your stuff and I can write it.
23:32:03 <alise_> Maybe I can do both because I hate collaborating :P
23:33:48 <alise_> someone paste me the unicode mathematical [[ ]] chars :(
23:33:53 <alise_> MATHEMATICAL LEFT WHITE BRACKET or something
23:36:18 <ais523> and it's MATHEMATICAL LEFT WHITE SQUARE BRACKET, etc, you were almost right
23:43:03 <alise_> We use G ? ?, to denote that if we reject all formulas of G, we have to reject the formula ?.
23:43:46 <alise_> fax: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.2290&rep=rep1&type=pdf
23:44:01 <oerjan> !haskell let x ++ y = foldr (:) y x in [1,2,3] ++ [4,5,6]
23:46:58 <oerjan> hm you cannot put _either_ x or y after that for any f and get x ++ y, because [] will be wrong
23:49:40 <oerjan> hm that [[1,2],[3,4]] thing...
23:49:53 <oerjan> which would be concat not ++, but...
23:50:41 <oerjan> well i'm not sure it is possibl
23:52:37 <alise_> What postscript viewer should I use for Windows?
23:52:45 <alise_> gsview is nice except that it sucks, horribly.