00:01:03 -!- FireFly has quit (Quit: Leaving). 00:02:23 would be nice if functions were invertable 00:02:29 *invertible 00:03:19 -!- kilimanjaro has joined. 00:03:57 hi kilimanjaro 00:04:00 haven't seen you before 00:04:24 it's because I never leave my mother's basement 00:04:30 -!- Libster has joined. 00:04:31 kilimanjaro pm 00:04:31 most people haven't seen me for that reason 00:04:36 well, that's a good entrance 00:04:42 hey is my -q off yet 00:04:42 MissPiggy: what are you pming someone entirely new for 00:04:44 sweet 00:04:46 hm wait Libster joining shortly after- oh dear 00:04:49 fizzie: ping. 00:04:50 hello alise 00:05:00 alise I don't see the other guys because I have them on ignore 00:05:14 alise, we probably share similar feelings towards Libster 00:05:15 libster just joined and is off +q so uh yeah 00:05:16 alise I want him to unban me from #math 00:05:19 where did we leave off 00:05:30 kilimanjaro: you might want to leave until he stops the trollaxing :P 00:05:31 who likes Erlang 00:05:39 Erlang is... alright 00:05:42 who likes design patterns? 00:05:52 I mean it's not /bad/ or anything, competent functional language 00:05:57 there was a project by a guy to implement something like it in gambit scheme 00:06:02 yeah i know of that 00:06:06 through chris double 00:06:06 Libster: What, you mean lambda? 00:06:10 because erlang is a wonderful idea bolted onto a crappy sequential language 00:06:13 Lambda's pretty nice. 00:06:24 pikhq: don't encourage him 00:06:26 alise, the guy who did it used to hang out pretty regularly in #scheme 00:06:27 yome 00:06:34 alise: Heh. 00:06:37 i'm not such a fan of erlang's concurrency mechanism but eh 00:06:41 i'm a purely functional kind of weenie 00:06:46 if it doesn't have beautiful denotational semantics it sucks 00:06:47 do you like CML? 00:06:49 isn't that the only reason people use erlang 00:06:53 for its concurrency mechanism 00:07:10 i thought CML was really neat but I never actually wanted to program in SML 00:07:15 cml is, sure i guess 00:07:17 but still a bit meh 00:07:19 IMPURE! 00:07:24 pl what do you have in mind 00:07:33 ok* 00:07:47 wait I have to have a coherent idea? 00:07:52 well I dunno 00:07:54 uh, fortress has implicit concurrency and that actually seems to work, that's cool 00:07:55 i'm just curious 00:08:02 haskell's `par` stuff is nice 00:08:09 i'm not talking about concurrency at that level 00:08:15 as opposed to 00:08:28 I mean at the design level, where the concurrency is actually part of the way you structure the program 00:08:34 par involves that 00:08:41 and fortress does too to an extent 00:08:42 but mostly par 00:08:43 like erlang forces you to look at things in terms of processes & messages 00:08:45 par is definitely part of the structure 00:08:58 kilimanjaro: but you don't need to structure things specially if you have pure functions 00:09:02 there are no side effects to handle the ordering of 00:09:13 parallelism becomes purely a computational detail 00:10:05 in the year 2000 maybe 00:10:08 when we are living on the moon 00:10:20 lol! 00:10:21 but for now real systems with real concurrency & distribution involve people being explicit about that 00:10:25 kilimanjaro hello? 00:10:32 can someone get him to talk to me at least 00:10:58 MissPiggy is clamoring for you to cyber with her 00:11:12 wait is she talking? 00:11:20 yeah 00:11:31 kilimanjaro hello? 00:11:31 can someone get him to talk to me at least 00:12:08 hi MissPiggy 00:12:22 hi kilimanjaro :) 00:12:24 lets PM? 00:12:33 * alise is not sure what MissPiggy is attempting to achieve 00:12:37 go for it 00:12:44 kilimanjaro: you should look at fortress 00:12:49 it does handle quite a bit of parallelism implicitly 00:12:54 I'm not denying that we need to specify it 00:13:02 but we don't need to structure every single module around it in a functional paradigm 00:13:16 also if you're interested in here-and-now practical solutions what are you doing in this channel? 00:13:35 he is trolling you 00:13:40 but he's so good at it you can't even tell 00:13:42 says the troll 00:16:35 alise, well esoteric doesn't have to mean impractical 00:16:43 sure but still. 00:16:47 it does to these people 00:17:19 I honestly do wonder if Libster doesn't have anything more intellectually satisfying to do. 00:17:49 nope this is pretty much as satisfying as anything to me 00:18:34 alise, you could ignore him 00:18:36 Libster: you're just not very good at trolling 00:18:43 yeah i know 00:18:46 that's why i'm practicing 00:18:52 kilimanjaro: doesn't stop him talking 00:18:53 nobody is born a good troll, it takes hard work 00:19:12 point 00:19:15 i'd ask lament to ban him but if there ever was a fruitless cause of action more likely to result in your own banning that is it 00:19:34 what 00:19:43 oh 00:19:43 sorry, I used big words. 00:19:51 yes 00:20:02 noen of your words exceeded two syllables 00:20:05 very impressive 00:20:20 Libsterification 00:20:35 He's... not even annoying. 00:20:41 Just boring. 00:20:42 i disagree 00:20:46 thanks 00:20:50 i think he's pretty annoying 00:20:58 me too 00:21:00 anyways I was hoping to talk about esoteric languages 00:21:05 I mean in the way of a really irritating troll 00:21:12 he's just like a flea occasionally flying in your vision 00:21:15 does prolog count as esoteric 00:21:20 sure 00:21:22 these days maybe it should 00:21:54 kilimanjaro prolog hardly counts as esoteric :/ 00:22:29 do you know how to program in prolog 00:22:30 ignore MissPiggy she's wrong :) 00:22:41 i was going to implement a unification algorithm once 00:23:00 to be honest i was no really trolling 00:23:01 in fact there's a really good paper on how to implement prolog efficiently 00:23:06 alise, have you even written a prolog compiler in prolog? 00:23:12 well, no. 00:23:17 so shut up :P 00:23:17 you see by typing stupid shit in this channel i am actually coding in my own esoteric language 00:23:23 why? 00:23:35 because shut up? 00:23:38 poo 00:23:50 haha MissPiggy is better at trolling than i am I should leave this to her 00:24:10 prolog's not esoteric, you can implement an ALGOL like in 10 lines and to imperative programming in that 00:24:27 or you could implement some basic functional programming and do that.. 00:24:41 (or you could just do actual programming in prolog, which is a lot less silly) 00:25:02 irrelevant 00:25:07 esolangs can be easy to turn into non-esolangs 00:25:08 was any actual program ever written in prolog? 00:25:15 prolog is sufficiently weird. 00:25:16 here's the paper http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.6051&rep=rep1&type=pdf 00:25:16 sup 00:25:18 pretty cool 00:25:22 I don't understand how prolog gets this impression 00:25:28 lament, actually imo the #1 application of prolog 00:25:39 it's WORSE than people going "lol brackets)))))" about lisp 00:25:43 was tricking the japanese into investing millions of dollars in their "fifth generation computing" project 00:25:46 MissPiggy: help I've been having dirty thoughts. I want to introduce some sort of impurity in my language for a reason 00:25:50 kilimanjaro: oh right 00:25:58 i remember reading about that, pretty impressive 00:26:03 another example of the white man keeping the yellow man down 00:26:09 kilimanjaro -- yeah that's a really nice paper, the next step is PVRs Aquarius thesis 00:26:38 alise; that will be 10 strokes of the cane! 00:26:57 Prolog on Prozac 00:27:11 MissPiggy: but it's for a reason! 00:27:14 MissPiggy: and it's very restricted! 00:27:27 Prolog on Perambulators 00:27:29 MissPiggy: basically it's to allow you to write memoise: (a->b) -> (a->b) 00:27:42 alise, bleh! 00:27:52 MissPiggy: the idea is basically that you can use impurity, *so long as it cannot escape the function* 00:27:57 alise I always disliked that but I know pragmatically useful etc etc 00:28:09 oh, I know; I'm just trying to think of a way to make it theoretically sound 00:28:27 alise: So, the function itself is pure, but can be stateful internally? 00:28:47 That is... Actually rather Haskell-like. 00:28:57 alise what about something like ST? You could have an axiom for it 00:29:24 ST doesn't let you return a pure function that accesses the impure state 00:30:08 alise but the axiom could let you ? maybe 00:30:23 alise: Actually, I think you can. Just have the state within that function's closure... 00:30:24 Then that would be side-effects without escaping, which is exactly my idea. 00:30:28 pikhq: Write it, then. 00:31:34 http://filebin.ca/zorysb/memoise.pdf 00:31:50 note: new isn't OOP there, I just was playing with the idea of an operator 00:31:56 that took a type and returned some appropriate "empty" value 00:32:05 basically mempty. :P 00:33:09 alise: Nope. I'm completely and utterly wrong. 00:33:18 ascii version of that, btw 00:33:19 memoise(f: a -> b) -> (a -> b) := 00:33:19 let memory := new Map(a, b) 00:33:19 \x. 00:33:19 x in memory => memory[x] 00:33:19 otherwise => memory[x] := f(x) 00:33:22 pikhq: yep 00:33:23 :P 00:33:30 the problem is defining what escaping the function is 00:33:37 here, the memory[x] lookup is always identical to the first call 00:33:43 so if the input function is pure (which it must be) the output is 00:33:48 but that's kinda hard to prove... 00:34:08 alise: Well. Actually, not quite. You could use unsafePerformIO and close over an mvar. :P 00:34:22 alise you could just prove it's observationally equivalent to a pure function 00:34:41 unsafePerformIO gives you unsafeCoerce :: a -> _|_ 00:34:43 alise since it always gives the same values, as the identity function -- that should work out I think 00:34:43 _|_ -> a 00:34:53 ergo unsafePerformIO => _|_ 00:35:03 therefore unsafePerformIO cannot have a value 00:35:11 -!- CESSQUILINEAR has joined. 00:35:11 MissPiggy: right 00:35:23 MissPiggy: also, gawp at my amazingly beautiful syntax. :| 00:35:28 ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ ☃ 00:35:33 yo 00:35:43 what is this, troll #esoteric day 00:35:43 snow mans 00:36:01 hey cessmaster is our friend man. 00:36:08 our /friend/ 00:36:10 cess is our friend 00:36:11 -!- oklopol has quit (Ping timeout: 246 seconds). 00:36:20 i am 00:36:28 someone should make a ☃ language 00:36:46 the one fatal flaw of TeX is the lack of \snowman 00:36:50 sorry Libster you cannot apply ☃ in the current evaluation context 00:36:55 IF UR FRENDS WITH CESS ☃☃☃☃☃ POST THIS SNOWMAN 10 TIMES ☃☃☃☃☃☃ 00:37:12 alise: xetex 00:37:40 alise: memoise f = (\mvar x -> unsafePerformIO $ do if isInMemory mvar x then getMemory mvar x else setMemory mvar x (f x)) $ unsafePerformIO newMVar emptyMemory 00:37:44 signal/noise = 0 00:37:49 oops, pikhq just talked 00:38:13 signal/noise = ω 00:38:28 pikhq: would you rather write that or http://filebin.ca/zorysb/memoise.pdf 00:38:36 alise: Yours. 00:38:55 What I wrote is probably the scariest Haskell line I've written. 00:39:11 if you stare at it hard enough 00:39:15 couldn't you just use an ioref 00:39:16 the two unsafePerformIOs merge together 00:39:50 have any of you gone outside in the past couple of days 00:39:58 what do you mean 00:40:02 outside of what 00:40:03 anyway it reeks 00:40:07 of the basement 00:40:09 don't program with unsafe functions 00:40:12 just use ocaml 00:40:14 uhh duhh 00:40:21 MissPiggy: Then everything is unsafe! 00:40:24 i keep all the sodas in the refridgerator 00:40:25 in the kitchen 00:40:29 -!- oklopol has joined. 00:40:32 well it's actually not unsafe that's the thing :P 00:40:37 you should just move your fridge to the basement 00:40:39 Yes it is. 00:40:40 or get a minifridge 00:40:44 gawd 00:40:45 groan 00:40:53 the basement has a freezer where I keep pizza bagels 00:40:55 You modify state. That is horribly unsafe. 00:40:55 lament: if i ask you to increase signal/noise, you'll just kick me, won't you 00:40:58 I don't have room for sodas 00:41:01 alise: yes. 00:41:01 what are you seriously saying that mutable reference break type safety 00:41:04 I'd have to get rid of some of the pizza bagels 00:41:16 wait is this lament's channel? 00:41:17 lament: how do I phrase a query so that you reading it will cause you to ban Libster? 00:41:19 MissPiggy: No, they break semantic safety. 00:41:21 (this is metaenquiry, this) 00:41:23 kilimanjaro: put away 40 of em 00:41:25 Libster, lament is an op 00:41:26 Libster: lament/fizzie's. 00:41:30 or are you giving the standard "buuut daaad it's hard to program with mutation!!" argument 00:41:31 lament is founder now iirc 00:41:31 oh 00:41:45 well lament isn't gonna ban me unless he doesn't it right now just to spite the fact i just said this 00:41:47 is semantic safety something with a formal definition? 00:41:57 or is it something you just made up to claim that mutation is BAD 00:41:58 Libster: *head explodes* 00:42:11 alise, no 00:42:15 andreou is founder 00:42:17 i sure am glad fizzie is our main op - also, you didn't hear me say this 00:42:20 MissPiggy: Hey, how often do your bugs come from state being modified? 00:42:25 kilimanjaro: what status does aardappel have again? 00:42:34 less than lament 00:42:35 I'm going to guess "all the ones that compile". 00:42:37 pikhq, I almost never program anything let alone things with mutable state 00:42:42 kilimanjaro: not in the past tho 00:42:47 you can just /msg chanserv access list #esoteric 00:42:50 pikhq, but I guess that you are giving the "buuut daaad.." argument now 00:42:51 Oh, you almost never program anything? 00:42:52 kilimanjaro: i used to be cofounder but then freenode introduced the #/## distinction and changed the cofounder on all # channels to be freenode-staff :( 00:43:05 lament, ahh lame 00:43:10 Then why the hell do you even care? 00:43:11 :P 00:43:19 i complained to the staff and they're like, well, file a form 00:43:24 (also, WTF? A non-coder in here?) 00:43:25 fuck freenode 00:43:36 free fucknode 00:43:40 pikhq, what should I be programming though? 00:43:42 MissPiggy is a computer scientist, not a programmer :P 00:43:46 that's a good idea 00:43:50 i'm gonna start fucknode 00:43:51 computING scientist *ahem* 00:43:59 CSer 00:44:27 MissPiggy: A computing science guy that doesn't cream his pants over purely functional languages? 00:44:31 programming is mostly fucking around with GUI libraries 00:44:32 Now that's amazing. 00:44:33 :P 00:44:41 been there done that 00:44:50 Also... 00:44:50 you seem to think MissPiggy is advocating imperative langs 00:45:06 pikhq oh I dig (pure) fp -- but I don't think it's the whole story 00:45:27 I don't think I've ever futzed with a GUI library more than "bashing out a quick Tk interface". 00:45:38 well you are a more skilled programmer than me :) 00:45:42 MissPiggy: opinion time: using things like actual images, or actual tables, as literals: cool thing, or /coolest/ thing? 00:45:47 Which is only technically programming, really. 00:45:49 all I do is fuck around with broken software and give up 00:46:05 alise: coolest thing :D 00:46:16 alise: Definitely coolest thing. 00:46:22 MissPiggy: In my OS, of course, the literals are, well, /literally objects/. 00:46:25 alise: I think you need a good editor though....... 00:46:29 The table is a literal table embedded in the AST. 00:46:36 The image is a literal image embedded in the AST. 00:46:41 like a wooden table with legs? 00:46:51 You can bring up information about them, inquire about them, perform functions on them, etc. 00:47:00 Edit them with whatever facility exists to edit them. 00:47:24 alise: And I presume this goes even further. 00:47:30 * pikhq imagines an editor literal in a program 00:47:40 I suppose you could technically do that, but that would be ridiculous. 00:47:58 Especially as you could just edit the program directly and save yourself a layer of indirection. 00:48:03 I doubt it would be useful for more than, say, automating an editor. But still. 00:48:14 You'd probably create that programmatically :P 00:48:23 You could include example Fugue programs as literal sounds 00:48:32 Play them inline 00:50:32 -!- cal153 has quit (Read error: Connection reset by peer). 00:51:43 Lisp programs as actual lists. 00:51:44 :P 00:53:36 -!- cal153 has joined. 00:55:27 http://www.nasa.gov/multimedia/nasatv/index.html 00:58:48 -!- augur has joined. 01:02:47 i ought to make my os like, now 01:03:53 -!- Asztal has quit (Ping timeout: 240 seconds). 01:05:15 what abou plan9 01:05:31 meh 01:05:36 it's just a big heap of char *s 01:06:34 wchar_T * :P 01:06:38 oops 01:06:41 no it treats files as bytes 01:06:42 -!- oklopol has quit (Ping timeout: 272 seconds). 01:06:43 alise: Not a heap. 01:06:46 also you mean Rune * 01:06:47 A *tree* of char *s. 01:06:49 :P 01:06:51 lawl. 01:07:02 -!- oklogon has joined. 01:07:06 whoa 01:07:52 i just realised that OSs with changing mutable state are like... continuatiosn. 01:07:55 *continuations 01:10:29 alise I'm watching them fly the shuttle away from the satillite 01:10:40 they're still in 0-g 01:10:53 indeed 01:11:52 :( 01:12:06 what :( 01:12:39 -!- oklogon has quit (Ping timeout: 245 seconds). 01:12:42 is Z32 for Z_{2^32} accepted mathematical notation? i would guess not, fortress peeps prolly invented it 01:12:44 bad fortress peeps 01:12:47 bad! 01:13:22 eh it seems fine 01:13:35 you have to know fortress anyway 01:13:44 so it should not be very confusind? 01:13:46 -!- Libster` has joined. 01:14:00 type Z(n:Z) := Z_(2^n) 01:14:05 problem solved 01:14:21 a neat thing is that you can define functions on Z_n 01:14:22 polymorphism! 01:16:52 also, the (a=>b;c=>d;otherwise=>e) conditional syntax is very elegant 01:17:05 yeah that's from lisp 01:17:21 I like it too 01:17:28 -!- Libster has quit (Ping timeout: 272 seconds). 01:17:39 Lisp? Syntax? What sort of craziness is this? 01:17:44 m-expressions 01:17:48 also, not quite 01:17:49 http://projectfortress.sun.com/Projects/Community/blog/ConditionalExpressions 01:17:59 lisp was [p=>a; q=>b; elseclause] 01:18:05 erm 01:18:07 s/=>/->/ 01:18:18 mccarthy used (p -> a, q -> b, elseclause) 01:18:24 I prefer (p => a; q => b; otherwise => elseclause) 01:19:41 Darned M-expressions. Being Lisp syntax. 01:19:43 although with omitted ;s on newlines 01:22:13 pikhq: LLVM isn't replacing -fvia-c. 01:22:18 It's replacing /everything/. 01:22:31 Specifically, NCG -> LLVM. 01:22:37 That's a replacement arrow. 01:23:03 "The headline is accurate: GHC is dropping the GCC backend (except for bootstrapping) in favor of David's new LLVM backend, as the performance potential is much better." 01:23:05 oh, I stand corrected 01:23:52 -!- oklopol has joined. 01:27:20 alise: They may in the future replace the NCG. 01:27:27 *Currently*, it just replaces -fvia-c. 01:27:35 Will, rather. 01:27:55 (IIRC, they will do so if it's ready in time for .16.) 01:30:28 MissPiggy: does your CAS have some sort of code dump I can load into my system 01:31:27 alise well it um doesn't realy exist yet 01:31:30 finger `ls /home` 01:31:32 I have to sort out the GUI 01:31:37 i'm fine with text output 01:31:38 well the REPL 01:31:49 i'm fine with command line invocation 01:31:52 what language is it in? 01:32:40 I haven't written it! 01:32:51 I can't decide to use haskell or coq 01:33:02 (or both) 01:33:17 well coq is already all that stuff in a way 01:33:26 i suggest writing it in my lang :P 01:35:35 What is it? 01:36:18 a lang 01:37:42 What's MissPiggy's thing? 01:37:50 a computer algebra system 01:37:53 Ah 01:38:08 What's your language? 01:38:43 Also, going to play some RoboZZle while I wait for a meeting for a project that I'm supposed to deny the existence of. 01:38:50 win 19 01:38:53 fffw 01:39:23 ?? 01:39:32 Sgeo: what project 01:39:46 let me guess it's some virtual reality shit that you feel some sort of twisted obligation to 01:39:56 The project that I've mentioned countless times before.. and yes, that's right 01:40:06 how about just freeing yourself 01:40:15 How about, I really really want this game to exist 01:40:28 whih game? 01:40:29 from what i've seen its incompetence is so great that there is very little hope of that 01:40:31 so give up and move on 01:40:38 MissPiggy: some remake of some shitty old virtual reality "game" he likes 01:40:47 virtual reality! :O 01:40:54 MissPiggy: think second life but worse 01:41:02 is it an MMO? 01:41:11 something like that. except without the fighting, or stats 01:41:26 I think that people who want to make an MMO are not going to succeed 01:42:39 We already have an MMO platform of sorts 01:42:57 http://www.neuroproductions.be/logic-lab/LogicLab2.swf is fun 01:43:02 And resources such as the server is all paid for already 01:43:10 Um, by AWI 01:43:10 (p xnor q) xor (r nand s) = FUN TIMES 01:44:15 wish i had a mic to play with it 01:44:52 I have an RL friend who wants to make an MMO with me though 01:44:59 And honestly, I'm not too interested in that 01:49:08 -!- oklopol has quit (Ping timeout: 272 seconds). 01:49:25 With the logic lab, I can only use one of each piece? 01:49:31 er no 01:49:34 n/m 01:50:06 xnor? nxor or is it something else? 01:50:41 It should be possible to make a flip-flop with logic gates, right? 01:51:14 it has flip flops 01:51:23 Ilari: presumably it's exclusive nor 01:51:27 Yes, but those are technically redundant? 01:52:04 Sgeo: Flip flop is just some logic around SR latch, and SR latch is two NANDs or NORs (depending on polarity of signals). 01:52:47 What does the spinny output thing actually do? I mean, besides spin? 01:53:21 Or maybe it needed two SR latches... I don't remember anymore. 01:55:10 How does the NOT gate make signal out of thin air? 01:55:41 magic 01:55:54 heh 01:55:58 silly program 01:56:01 5min before the meeting and no one's here 01:56:03 Sgeo: At least CMOS NOT gate connects output to positive voltage if input is at ground. 01:56:12 Sgeo you are good at pretending it doesnt exist! 01:56:27 MissPiggy, I care very little about the confidentiality junk 01:56:49 If they really cared, they'd have told us before I started telling everyone I knew 01:57:41 If they even /care/ about confidentiality in a hobby project, they are abject fools, no more intelligent than children, with a complete misunderstanding of how groups self-organise. 01:57:51 Their use of C# only bolsters this suspicion. 01:58:38 They're far more likely to waste arbitrary amounts of your time than to produce anything meaningful. Making a 3D game is /hard/, especially a networked 3D game, and these people appear to be too idiotic to do it. 01:58:56 Ask yourself if this game being made really has infinite utility, and if there isn't a better way to achieve it than with this hopeless rubbish. 01:59:07 The "networked 3d" part is already taken care of by the platform, ActiveWorlds 01:59:16 They still need to write the networking code. 01:59:21 And don't think that invalidates the rest of what I said. 01:59:44 Um, no 01:59:57 Oh, so it magically connects to a socket for them? 02:00:02 I think not. It's still C# code. 02:00:11 All of that code is part of Active Worlds 02:00:40 The actual logic of the game is in a program that does connect to the world, and connecting is simple 02:01:07 You know, I think there may be real issues underlying your seemingly life-controlling nostalgia... 02:02:34 what's the original 02:02:37 I want to see the original 02:02:53 -!- lament has quit (Ping timeout: 252 seconds). 02:03:41 -!- lament has joined. 02:04:00 http://www.youtube.com/results?search_query=Mutation+activeworlds&search_type=&aq=f [the first video there is not that great [it's mine], and Mutation - Mafia has nothing to do with anything] 02:04:02 active worlds 02:06:11 that is so cool 02:06:18 it's like 3D IRC 02:06:24 oh don't /encourage/ him 02:06:31 -!- jcp has joined. 02:11:27 Whee, no one's there 02:12:13 sorry Sgeo 02:12:27 He means at the "meeting". 02:13:29 What did MissPiggy think I meant? 02:14:34 It might be possible that I'm 12 hours late. The guy in charge mixed up AM and PM once before. 02:15:00 Although I think that's why it's at "11:59" and not "12:00" 02:16:04 SG-1 now 02:16:55 -!- jcp has quit (Remote host closed the connection). 02:24:34 -!- kilimanjaro has left (?). 02:27:19 -!- MissPiggy has quit (Quit: Lost terminal). 02:27:39 wasn't an AM/PM issue this time 02:35:29 http://filebin.ca/djzwuz/on-syntax.pdf 02:35:34 A little ditty about syntax. Comments welcome. 02:36:34 -!- gm|lap has joined. 02:37:35 -!- Asztal has joined. 02:39:28 It's a PDF 02:39:42 Yes, it is. 02:39:51 Here's zero nickels; go buy a better PDF reader and/or operating system. 02:40:17 Let me know when you're ready to join every single person in academia, plus some people not. (Okay, so academia loves .ps too, but still.) 02:49:01 NOBODY LOVSE ME 02:49:20 :( 02:49:24 lovse 02:49:27 .cx 02:49:30 Yeah, I like that spelling of that word now. 02:49:37 Oh, shit, didn't even notice that 02:49:37 alise 02:49:40 .cx 02:49:53 Loves sex and alise sex? 02:49:56 You've got cx on the brain. 02:50:45 http://images.google.com/hosted/life/l?q=theodore+roosevelt+source:life&prev=/images%3Fq%3Dtheodore%2Broosevelt%2Bsource:life%26ndsp%3D20%26hl%3Den%26sa%3DN%26start%3D80&imgurl=2934f1cc36185de2 02:50:50 Theodore Roosevelt riding a moose. 02:54:02 -!- gm|lap has quit (Remote host closed the connection). 02:55:05 -!- Asztal has quit (Ping timeout: 276 seconds). 03:03:24 -!- oklopol has joined. 03:10:00 bye 03:10:03 see you tomorrow 03:10:45 Bye 03:14:36 alise: We should write in the pure, untyped lambda calculus. 03:15:13 * Sgeo just offered to give the project head some money because his AW citizenship is going to expire soonish. No cit, no project 03:15:17 He turned it down 03:27:35 -!- oklopol has quit (Ping timeout: 276 seconds). 04:01:51 -!- CESSQUILINEAR has quit (Ping timeout: 256 seconds). 04:08:28 -!- Libster` has quit (Ping timeout: 272 seconds). 04:33:23 -!- oklopol has joined. 04:55:13 -!- CESSQUILINEAR has joined. 04:58:47 -!- bsmntbombdood_ has joined. 05:01:23 -!- bsmntbombdood has quit (Ping timeout: 252 seconds). 05:11:21 -!- oklopol has quit (Ping timeout: 252 seconds). 05:12:09 -!- oklopol has joined. 05:44:47 -!- bsmntbombdood__ has joined. 05:45:23 -!- bsmntbombdood__ has changed nick to bsmntbombdood. 05:47:54 -!- bsmntbombdood_ has quit (Ping timeout: 272 seconds). 06:02:02 -!- CESSQUILINEAR has quit (Ping timeout: 246 seconds). 06:05:01 -!- Libster` has joined. 06:19:12 -!- oklopol has quit (Ping timeout: 260 seconds). 06:22:26 -!- oklopol has joined. 06:34:46 -!- augur has quit (Ping timeout: 272 seconds). 06:55:09 -!- augur has joined. 06:57:37 -!- oerjan has joined. 07:02:24 -!- pikhq has quit (Read error: Connection reset by peer). 07:03:53 -!- lament has quit (Ping timeout: 248 seconds). 07:04:46 -!- lament has joined. 07:13:34 -!- addicted has joined. 07:17:26 -!- deschutron has joined. 07:18:09 hey guys, is anyone here a fan of SNUSP? 07:25:05 -!- Pthing has joined. 07:26:01 -!- oklopol has quit (Ping timeout: 264 seconds). 07:28:17 -!- oklopol has joined. 07:30:27 deschutron, apparently you've written quite a bit of extension stuff for it 07:30:37 yes 07:31:57 * Sgeo bibbles a bit at EPARM 07:32:16 i've also written an interpreter for it, including some of the extensions i described on the wiki 07:32:38 and i've written a command shell in an extended form of SNUSP 07:33:58 this week, they got uploaded to the Esoteric Files Archive 07:34:07 EPARM seems a bit like PSOX [my project which I abandoned, but is mostly done], except designed better possibly 07:34:21 oh really? 07:34:39 what does PSOX do? 07:34:52 http://esolangs.org/wiki/PSOX 07:35:16 That PSOX 1.0a1 thing is a bit old 07:36:01 Oh wait, EPARM is _only_ for command-line arguments? 07:36:34 pretty much 07:36:51 the snusp-start command framework can be used to define other special functions 07:37:04 but EPARM only specifies argument-passing funcionality 07:38:05 Ah. PSOX has some functionality defined in the spec [Network/HTTP access in particular] 07:38:19 And was supposed to have File I/O defined, but it was abandoned before then 07:39:19 so PSOX is designed to allow more advanced functionality than reading and writing to a program that only uses stdin and stdout? 07:39:43 Um, it still reads and writes to a program that only uses stdin and stdout 07:40:12 Question: Did you manage to make EPARM work on Windows? 07:40:33 I had trouble figuring out how to do that, that resulted in requiring the program to output the fact that it wants to receive input 07:40:50 no, i didn't try 07:41:50 are you talking about making it so that if you run the program with args on the windows command prompt, it will receive the arguments? 07:42:35 in that case, the windows arguments don't make it to the esoteric program 07:42:58 however, an interpreter could be made that will convert the args 07:43:54 In my snusp command shell, it sends EPARM arguments to a program iff the user tries to run it with arguments. Otherwise it doesn't use EPARM. 07:44:07 given the design of EPARM, that worked pretty well 07:44:33 the programs never have to output the fact that they want to receive EPARM input 07:51:40 -!- pikhq has joined. 07:56:27 Sorry, was IAW 07:57:13 -!- augur_ has joined. 07:57:22 -!- augur has quit (Read error: Connection reset by peer). 07:57:27 i've also come up with something to give advanced functionality to stdin/stdout programs: i've started writing a kernel wrapper for Linux. 07:57:51 how does the snusp-start command framework deal with the possibility of a program wanting to do stuff, get input related to that stuff, do more stuff, do regular output, etc. etc. etc.? 07:58:20 I need to go to sleep now. Good night 07:58:27 ok 07:58:32 good night 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:00:52 anyway, i mainly came here to plug my newly uploaded programs: Snuspi the SNUSP interpreter, and Snuspatron the extended-SNUSP command shell 08:01:07 They are available in the impl/ and src/ subfolders of http://esolangs.org/files/snusp/ , on the Esoteric Files Archive. 08:03:42 the snusp-start command framework allows a program to be fed meta-data relating to how it is being executed 08:04:41 it can inform the program that a certain protocol is available for it to use, for example 08:06:11 http://trac2.assembla.com/psox/browser/trunk 08:07:00 thanks. i have already downloaded it via svn 08:07:18 AH 08:07:20 *Ah 08:07:38 if a feature can't make use of sending metadata to a program when it is started, then i'm afraid snusp-start commands won't help it 08:08:13 Um, there might be a bit of a bug in db_utils.py on line 18 08:08:18 concerning a missing " 08:11:01 -!- augur_ has changed nick to augur. 08:11:25 -!- kar8nga has joined. 08:13:24 oh, and trunk/ex has a lot of obsolete stuff 08:13:33 -!- Libster` has quit (Ping timeout: 272 seconds). 08:13:46 i just got psoxsimplecat.b to work using your psox program 08:14:08 :) 08:14:10 Try online.b 08:14:28 pikhq made a wget.b, but it's not included in there 08:14:36 And I should be going to sleep 3 hours ago 08:14:53 what should online.b do 08:14:55 jsut quickly 08:14:58 then i'll let you go 08:15:52 When it runs, type in a URL (including the http://) and press enter 08:15:57 It should display the contents 08:16:14 hot dog it did 08:16:45 :) 08:22:20 this post contains info about my kernel wrapper. Ctrl+F "an arch" to see the basic usage architecture: http://esolangs.org/forum/kareha.pl/1266506523/1 08:23:50 my wrapper uses a basic protocol that has the client program basically setting the sycall arguments and calling linux syscalls by number 08:24:08 conceiveably, a wrapper can be written that uses PSOX. 08:29:37 -!- oerjan has quit (Quit: leaving). 08:32:41 -!- oklopol has quit (Remote host closed the connection). 08:33:56 -!- oklopol has joined. 08:37:55 what's .b ? 08:39:52 cheater4, file extension? 08:39:55 brainfuck 08:40:01 ok 08:40:03 .bf is befunge 08:40:09 so don't mix them up 08:40:36 (befunge 98 uses .b98 though) 08:40:58 you guys should reimplement XanaduSpace in brainfuck 08:41:12 no clue what that is 08:41:46 it's the better alternative to hypertext 08:45:09 vaporware iirc? 08:45:41 I think I have read about it somewhere 08:45:52 cheater4, but go reimplement it yourself 08:46:44 nah, there's a demo out 08:46:53 but it only opens the single demo document 08:46:55 :D 08:47:21 see, vapourware 09:06:26 -!- MigoMipo has joined. 09:10:05 -!- Asztal has joined. 09:18:29 -!- oklopol has quit (Remote host closed the connection). 09:21:00 -!- oklopol has joined. 09:35:15 -!- kwertii has quit (Quit: bye). 09:52:21 "pikhq: (also, WTF? A non-coder in here?)" <<< i'm a non-coder! 09:56:38 i only code if i absolutely have to, and i never program anything. 10:02:39 -!- kar8nga has quit (Remote host closed the connection). 10:08:05 -!- BeholdMyGlory has joined. 10:11:33 -!- FireyFly has joined. 10:12:56 -!- tombom has joined. 10:26:59 -!- FireyFly has changed nick to FireFly. 10:32:17 -!- Azstal has joined. 10:32:57 -!- Asztal has quit (Ping timeout: 248 seconds). 10:58:04 -!- oklopol has quit (Ping timeout: 245 seconds). 11:34:42 -!- sebbu2 has changed nick to sebbu. 11:36:06 * Sgeo just offered to give the project head some money because his AW citizenship is going to expire soonish. No cit, no project 11:36:07 He turned it down 11:36:28 a fool, unless he believes that your supply of money is limited enough that that would cause you disutility greater than the project not existing 11:36:38 or unless he has money with which he is going to renew it anyway 11:41:46 -!- oklopol has joined. 11:49:14 -!- oklopol has quit (Read error: Connection reset by peer). 11:58:40 -!- oklopol has joined. 11:59:45 -!- oklopol has changed nick to oklofok. 12:05:01 -!- oklofok has quit (Ping timeout: 264 seconds). 12:05:34 -!- BeholdMyGlory has quit (Remote host closed the connection). 12:05:56 -!- BeholdMyGlory has joined. 12:11:36 -!- Asztal has joined. 12:12:18 -!- Aszstal has joined. 12:15:23 -!- Azstal has quit (Ping timeout: 276 seconds). 12:15:53 "The obvious answer is that you took a computational specification of a human brain, and used that to precompute the Giant Lookup Table. (Thereby creating uncounted googols of human beings, some of them in extreme pain, the supermajority gone quite mad in a universe of chaos where inputs bear no relation to outputs. But damn the ethics, this is for philosophy.)" 12:16:17 -!- Asztal has quit (Ping timeout: 260 seconds). 12:20:15 where is that quote from? 12:23:44 http://lesswrong.com/lw/pa/gazp_vs_glut/ 12:29:22 -!- oklopol has joined. 12:31:28 Wareya: why thank you 12:31:31 mr googler :P 12:31:39 yes 12:32:23 Can someone who doesn't suck at C tell me how to load oa text file into a square array of characters that matches what I'd see in a text editor? 12:32:30 load a* 12:32:39 You know how to open a file, yes? 12:32:43 yes 12:32:57 Use getc() to read the file character-by-character; keep counters i and j, initially 0. 12:33:03 if the char is \n, j++ 12:33:06 and i=0 12:33:10 otherwise 12:33:17 chars[i][j] = char; 12:33:17 i++; 12:33:19 what do I do with the characters I dno't overwrite? 12:33:27 "Don't overwrite"? 12:33:38 the ones that I don't set in the array 12:33:51 and how would I know what size to have the array be? 12:34:07 What characters would you not set into the array? 12:34:09 You mean newlines? 12:34:20 As I said, increase j++ and reset i to 0 on a newline, then continue to the next character. 12:34:41 Also, you don't. Either pick a "big enough" value, or use malloc and realloc to adjust the array size as you run out of it. 12:34:52 no, like line 6 being five characters long, what would I do with chars[7][6] 12:34:58 Wareya: Oh. 12:35:03 Initialise the array to \0s 12:35:08 ? 12:35:11 \0 is end-of-string in C 12:35:15 "\0" 12:35:16 I'm a terrible programmer 12:35:21 So you could use a line as a string 12:35:33 re: malloc and realloc "But isn't that hellishly boring and easy to fuck up?" Yes, it is, so don't use C. 12:35:56 actually, I love playing with pointers 12:36:34 [list(x) for x in open('filename', 'r').read().split('\n')] 12:36:36 That's it in Python 12:36:38 I'm going to go get soda so that I feel less shitty. Later. 12:36:47 (Doesn't pad out the lines to all be the same length, but there you go.) 12:37:11 Python is amazing, but I don't feel like learning it because of the syntax constraints/restraints/whatever. 12:37:32 So learn some other language. 12:37:34 Like Haskell. 12:37:39 :d 12:37:41 :D 12:37:55 thanks 12:38:01 -!- oklopol has quit (Ping timeout: 264 seconds). 12:38:24 deschutron: thanks what? :P 12:39:34 Here's a complete implementation 12:39:35 lines = open('/dev/stdin', 'r').read().strip().split('\n') 12:39:35 width = max(len(x) for x in lines) 12:39:35 table = [list(x.ljust(width)) for x in lines] 12:39:51 the googling :P 12:40:05 i should have googled it myself... 12:40:31 ah 12:41:33 yep 12:41:33 lines = open('/dev/stdin', 'r').read().strip().split('\n') 12:41:34 width = max(len(x) for x in lines) 12:41:34 table = [list(x.ljust(width)) for x in lines] 12:41:38 substitute /dev/stdin for a filename and that works 12:41:41 blank places considered spaces 12:45:00 -!- MigoMipo has quit (Quit: co'o rodo). 12:49:30 I wish uorygl was here, so that I could share with him an awful pun. 12:55:57 -!- tombom has quit (Quit: Leaving). 13:07:18 http://filebin.ca/uekfh/gcd.pdf 13:07:19 Pretty. 13:15:24 back 13:16:25 don't you think an image would have sufficed? :P 13:17:10 I typeset it in TeXmacs; producing an image would have been a lot harder than hitting export. 13:17:20 k 13:17:22 Also, no; this one scales to any size. 13:17:39 svg? :D 13:17:42 I'm kidding. 13:17:45 Besides, it's how you program in my language. Better get used to it :) 13:18:45 Your language interprets PDF files? :D 13:19:08 Well, no, it compiles abstract syntax trees. But ASCII source code isn't the done thing, really. 13:19:20 You'd type that form directly into an editor with keypresses something like: 13:19:32 gcd(m:ZZ,n:ZZ)->Z:= 13:19:35 (n=0=>m 13:19:42 otherwise=>gcd(n,m-n*floor(m/n))) 13:19:47 And it'd show as that. 13:19:53 *->ZZ 13:20:05 that works, I suppose 13:20:25 That form wouldn't be stored, though; just interpreted as editor commands to create an AST. 13:21:03 quick question: Should I use the form of Boat on the wiki page or a minimized version? 13:21:46 When in doubt, simplify, especially for an esolang. Anything not directly related to the central idea must go; that way, you have to utilise the central idea at all times to create programs, heightening the esotericism. Also, it makes it easier to implement, and cleaner. 13:21:48 said minimized version: http://64.vg/src/48029a6eda8165c6d5a5b6f71a785f1e/raw 13:21:58 okay 13:29:54 hmm 13:29:59 there should really be some notat- anyway 13:30:14 Wareya: I'd drop !=; it's !(e==e) 13:30:20 I'd drop nand, too, it's !(e&e) 13:30:30 I'd also drop division; you don't have addition or anything, so why? 13:31:17 -!- CESSQUILINEAR has joined. 13:32:01 because multiplicatin is really hard to to IM 13:32:17 ?? 13:32:20 and I culd see me dropping !=, but it's a real operator 13:32:29 sorry, my o key is being stupid 13:32:32 to IM? 13:32:33 what? 13:32:36 you have no mult 13:32:39 IMO 13:32:44 do* 13:32:47 ?? 13:32:52 to do, in my opinion 13:32:53 also, just drop != and !& they don't save any chars 13:32:56 !(e&e) 13:32:57 (e!&e) 13:33:00 Wareya: howso 13:33:01 nand? 13:33:30 multiplication is hard to do in an excessive way like brainfuck does, and that's not my goal 13:35:57 I do suppose I shld re-add subratsin and get rid of binary not though. 13:36:01 should* 13:37:08 subtration* 13:38:13 *gasp*! The comment form on this scam page does nothing! What a surprise! 13:38:59 It's supposedly moderated, but a quick glance at the source reveals no contact with the server 13:39:23 Wareya: you have no mult though 13:39:24 just division 13:39:29 Also, some of the text makes a reference to what websites seem to think is my hometown. 13:39:31 e/(1/e) 13:39:37 that's e*e 13:39:46 well, yes 13:39:50 but division is "complicated" 13:39:53 brings in reals etc 13:39:54 just have mult 13:40:07 everything is an integer 13:40:08 Sgeo: yeah common scam thingy 13:40:11 *gasp* 13:40:11 ah scam pages... 13:40:14 Wareya: then what you have is not division 13:40:17 also, you have no "e" 13:40:25 yes 13:40:26 I used HideMyAss.com, and now Marie is from Woodstock! 13:40:28 also, 1/x = 0 if you only have ints 13:40:36 She's the magical ordinary mom! 13:40:40 so x/(1/y) cannot be x*y 13:40:42 I said e/(1/e) in the scope of mathematics 13:40:44 not Boat 13:40:45 because it's x/0 13:40:49 therefore, / is not sufficient to give * 13:40:56 therefore you cannot justify keeping / because of multiplication 13:41:02 hey 13:41:11 I forgot to implement shifting 13:41:26 (I'm kidding, there's no reason to have it) 13:42:02 the way that memory is addressed, and the fact that I have division, allows for multiplicatino 13:42:06 on* 13:42:17 and I'm saying that because I can't find a way to prove myself wrong, so have at it! 13:42:32 it actually reminds me of when i visited some Yahoo chat rooms yesterday. There seemed to be a lot of bots there 13:42:36 if you find a serious flaw I agree with then I'll remove division or add multiplication 13:43:56 Wareya: well x/y in your lang is integer division right? 13:44:07 i.e. floor(x:RR/y:RR) 13:44:15 Is the fine print genuine? If it wasn't, would they be shut down by .. some governmental thingy? 13:44:28 I believe so 13:44:38 -1 < 1/x < 1 13:44:53 <= 13:44:57 erm, yes. 13:45:02 and yes 13:45:06 therefore, floor(1/x) = 1 if x = 1; 0 otherwise 13:45:22 with reals, x/(1/y) = x*y 13:45:26 "Please also recognize that the story and comments depicted on this site and the person depicted in the story are not real." 13:45:28 for integers: 13:45:42 x/(1/y) -> x/(if y = 1 then 1 else 0) 13:45:44 -> 13:45:50 if y = 1 then x else (undefined) 13:46:00 therefore, you cannot use integer division to perform integer multiplication. 13:46:01 Q.E.D. 13:46:15 not even with binary shifting? 13:46:24 even if it's innacurate? 13:46:59 binary shifting is, itself, multiplication and division of powers of 2. 13:47:16 x< x>>y = x/(2^y) 13:47:43 we already have /, so x>>y only adds one useful operation 13:47:55 1>>y = 1/(2^y) 13:48:08 the problem with this is that 1>>y always = 0. 13:48:17 so, anyway 13:48:22 how can we do 3*3, let's say 13:48:28 well, we can't do 3/(1/3) 13:48:31 hang on 13:48:38 and 3 isn't a power of 2, so we can't use << 13:48:42 we can however 13:48:45 express it as 6/2 13:48:53 = 6/(2^1) 13:49:02 you can use << to reduce the innacuraccies of integer divisin, can't you? 13:49:10 ion* 13:49:12 so, that gets us three 13:49:20 but not in an operation 13:49:26 we still need a general multiplication 13:49:29 what do you mean? 13:49:31 but since 3 isn't a power of two 13:49:33 we can't use << 13:49:41 therefore, you cannot multiply in your language without using addition and a loop. 13:49:42 okay 13:49:49 therefore the division is useless for that purpose 13:50:03 -!- MissPiggy has joined. 13:50:20 Hm 13:50:22 http://www.maxmnd.com/index.php 13:50:28 Hi MissPiggy 13:50:28 * alise tries to think of a name for can-be-equalified 13:50:31 Equalisable? 13:50:46 hi 13:50:48 equalified? 13:50:49 what? 13:50:59 decidible equality 13:51:04 unifiable 13:51:33 MissPiggy: so I've decided how to do things like inferring "type-class instances" (not really) in my language 13:52:00 "Since the trials are completely free, there is no cost or risk to you" 13:52:14 there is a keyword "implicit"; it is usable as the LHS in a type declaration 13:52:27 Beyond not realizing that you have to cancel [if the fine print is legit] or scammers doing whatever they want [otherwise]? 13:52:35 It makes an association with the type on the right and its corresponding definition (specified like `implicit : a = x`) 13:52:39 the obvious happens 13:53:15 implicit : (card ∅ = 0) = ... 13:53:31 implicit : Ring ZZ = ... 13:53:34 etc 13:54:09 incidentally in this way we can read "implicit : a = x" as "The proof that a is true is..." so we can view "Ring a" as "a is a Ring" rather than "the Ringy stuff for a" 13:54:13 even though it's a value 13:56:05 MissPiggy: http://filebin.ca/djzwuz/on-syntax.pdf 13:56:26 be warned that the syntax in there might not be so excellent; it was written while tired :P 14:01:06 that's a good point in consisent 14:02:09 -!- MigoMipo has joined. 14:02:51 one-page articles are a nice idea 14:03:41 MissPiggy: can you think of any problems w/ my implicit idea? 14:03:54 one is in e.g. Ring when you want to have the ring properties and name them implicit 14:04:00 then you have to name the type again when defining them 14:04:02 but i don't see a problem with that 14:04:05 the type is the name in some sense 14:05:45 alise I think that implicit stuff sucks but I didn't want to say :P 14:06:05 MissPiggy: so you want to specify the equality, ring, ... definitions every single time you use a numeric function? 14:06:07 that's sweet 14:06:27 I've still not figured out how to solve that problem 14:06:38 well i just solved it, and made it work for proofs as well :) 14:06:47 -!- mycroftiv has quit (Quit: leaving). 14:06:55 i think it's a good solution; in a way, when you ask for a member of a type implicitly in a function, you're saying "the value implicit_this_type" 14:07:01 this is just a way of making that actually true 14:11:39 Hmm. 14:11:51 Is there something like rings but without the additive inverse? 14:12:02 i.e. something I can put 0, + and * in and have NN be part of it :P 14:13:07 Hmm: http://en.wikipedia.org/wiki/Rng_(algebra) 14:25:09 -!- addicted has quit (Ping timeout: 245 seconds). 14:38:32 -!- kar8nga has joined. 14:40:19 -!- oerjan has joined. 14:43:52 -!- deschutron has left (?). 14:53:38 http://en.wikipedia.org/wiki/Perverse_sheaf disgusting 15:04:32 > If Carl Shulman does not let me out of the box, I will Paypal him $25. If he 15:04:32 > does let me out of the box, Carl Shulman will donate $2500 (CDN) to SIAI. 15:04:38 Those... are high fucking stakes. 15:04:56 shit, he released it in the end 15:05:04 Deewiant: know how you said high stakes? 15:05:19 this guy donated $2500 2005 canadian dollars to SIAI because he let the AI out 15:05:43 I didn't say high stakes 15:05:49 Well, someone did. 15:06:02 a wizard did it 15:06:34 Personally, if I was risking >1000 currency, I would try really fucking hard to be as close as possible to bashing no on the keyboard while staying within the test rules. 15:06:43 I think everyone else would, too. 15:06:48 'part from richies. 15:10:25 In the next one the human bet $2500 US and won, keeping the AI in the box. 15:10:41 Yes. Of course. I agree that Eliezer is no god. :) 15:10:53 -!- deschutron has joined. 15:11:10 But the existence of /anyone/ losing such a challenge with such stakes for them if they lose is striking. 15:11:18 but I don't think he did it for the money 15:11:27 yeah I agree 15:11:45 yeah but no matter what i'm doing something for if I think "if i say yes i'll lose $2500 cad" would be pretty motivating 15:11:51 even if it's towards an organisation you support 15:12:21 therefore, floor(1/x) = 1 if x = 1; 0 otherwise <-- forgetting negative numbers here? 15:12:37 oerjan: clearly by 'integers' i meant 'naturals' 15:12:40 not that it makes any difference to the rest of your argument 15:12:50 :P 15:15:36 although i think that shifting + integer division might allow you to do multiplication in _less_ loop iterations than just addition 15:15:47 if you're clever 15:16:08 yes 15:16:40 oerjan: also I thought of a computable variant of ring computing 15:17:03 hm? 15:17:04 let 1 = identity; let infinity = _|_ 15:17:08 infinity+x = infinity 15:17:13 infinity*x = infinity 15:17:22 we already know that 1=identity works 15:17:23 now 15:17:27 we need an additive identity 15:17:31 let 0 = foo 15:17:35 foo x = magic 15:17:36 where 15:17:42 magic + y = y 15:17:47 f magic = magic for all other f 15:17:51 tada 15:17:53 o_o 15:18:03 admittedly "magic" is _not_ the most unesoteric value ever dreamed of 15:18:13 but it's basically like _|_ except warm and cuddly if you add it up :P 15:18:38 so what is infinity + (-infinity) *cough* 15:18:55 0! 15:18:59 oerjan: can't we just make it rng computing :P 15:19:06 or whatever ring-without-negative is 15:19:13 MissPiggy: yes but we need it turing computable :P 15:19:17 anyway hmm 15:19:24 alise: well yes in fact i think cpressey may done that already 15:19:32 (vague recall) 15:19:34 he did ring computing with negatives 15:19:38 in 2007, even 15:19:40 dunno why he's gone back to it 15:19:43 i mean before that 15:19:55 http://catseye.tc/projects/burro/doc/website_burro.html 15:19:57 check it 15:20:11 anyway 15:20:17 -0 = 0, obviously 15:20:30 so we don't need to invert magic which I'm thankful for; I've never seen a value so weird 15:20:43 -1 is easy 15:20:46 but -infinity? 15:20:50 hmm 15:20:54 the problem is that you can do -(nonterminating) 15:21:01 so you can't pattern match on -infinity, just like infinity 15:21:13 oerjan: Clearly, I must ask Wolfram Alpha. 15:21:25 Apparently, infinity + -infinity = indeterminate. 15:21:34 Indeterminate could be said to be _|_. 15:21:45 Therefore, infinity + -infinity = infinity. Therefore, -infinity = infinity. 15:21:48 Happy? 15:21:48 How does infinity - infinity = 0? 15:21:52 Or was that a joke? 15:22:07 Because x - x = 0; but really there's multiple interpretations. 15:22:11 Mine is the computable one :P 15:22:16 alise: burro is a group, not a ring 15:22:18 Even though it sort of breaks the x+-x = 0 no exceptions thing 15:22:28 I mean, we're not using infinity as /the result/ 15:22:37 We're just saying that infinity + -infinity never yields a value, i.e. it is bottom. 15:22:44 It just so happens that we have a name for bottom in our language, infinity. 15:22:58 So we can say that infinity + -infinity = infinity, but really the failure to terminate is at a higher-level in the system: the evaluator. 15:23:12 Are we allowed to do that? :-) 15:23:22 alise: infinity + -infinity indeterminate is allowed in the extended reals precisely because they are _not_ a ring 15:23:29 (or group, even) 15:23:51 i was thinking more that infinity + -infinity "has a value" 15:23:53 it's just unknowable 15:26:43 "AI-Box Experiment #3 gave the AI a minimum time of four hours. I would 15:26:43 recommend 4-6 hours for future Experiments. Typing is slower than speech." 15:26:45 Endurance typing. 15:29:36 alise nonstandard analysis 15:29:47 I prefer bullshitology :) 15:29:53 I can just throw about terms 15:29:55 like "unknowable" 15:29:57 lol 15:29:57 and it all works 15:30:11 you are missing out on the good stuff though 15:30:24 infinitesimals are sexy though 15:30:36 alise: some day you'll find a time cube inside your ideas though, and then you will know that all hope is lost 15:30:49 i already accept the cubic truth 15:31:05 hey someone come up with a formal mathematical system with -1*-1=-1 15:31:08 lolololol 15:31:27 alise: any ring of characteristic 2 15:31:34 "criticism of non-standard analysis, by Halmos,[who?]" 15:31:37 (including some fields) 15:31:39 You do not know who Halmos is. 15:31:49 -!- kar8nga has quit (Remote host closed the connection). 15:31:59 of _course_ i know who halmos is 15:32:10 oh wait 15:32:14 misread 15:32:14 yeah it's that guy who made the qed symbol! :P 15:32:42 ?(?(e){c}){c}this is valid, however pointless it is 15:32:43 ummmmmm so I should do something today instead of waste it 15:32:47 MissPiggy: only if it's fun 15:33:06 I guess I'll have a bath 15:33:08 MissPiggy: READ THE ED STORIES (if I try hard enough, will this become a meme on the annoyingness order of PSOX?) 15:33:34 oh yeah the ed stories are good, I haven't finished them 15:33:45 alise, READ THE FINE STRUCTURE STORIES 15:33:54 NOOOOOOOOOOOOOOOO 15:34:21 ed stories would make a good film 15:35:10 (would fine structure?) 15:36:03 * oerjan makes a link to Halmos. 15:36:25 Um, possibly not. The setting jumps around quite a bit 15:36:35 a link to Halmos 15:36:43 Sgeo: Does in movies, too :P 15:36:52 Just might have to rearrange things so there's fewer switches 15:36:53 alise: instead of the [who?], wiseass 15:38:20 I'd suggest another reason it might not be movie-able, but it would be spoilery 15:39:06 Sgeo: does everyone die? that's rather acceptable. extremely LURID sex? just call it a porn drama! scenes set in the platonic world of abstract mathematics? *that* could be a problem. 15:39:12 (only say if it's any of them, not a specific one :P) 15:39:45 One of those is the case, but it wasn't what I was thinking of in particular 15:39:54 well, actually, not quite 15:40:21 is it the first one, or one of the second two? 15:40:43 One of the second two 15:41:09 i'm guessing probably _not_ the last one 15:41:17 extremely lurid sex set in the platonic world of abstract mathematics. 15:41:46 Go read the first Fine Structure story 15:41:54 Sgeo: the special effects? 15:42:03 I read up to the one where the girl (I think) can go through matter or something 15:42:08 literally first page of that 15:42:10 then stopped 15:43:01 Oh. I was thinking of Unbelievable Scenes [in relation to your options] 15:43:08 And it's a guy who can go through matter 15:43:21 *Unbelievable Scenes in Space 15:43:48 I do not know what that is. 15:43:56 Fine Structure used to be unordered, IIRC. 15:44:02 It was just a collection of stories, then he jiggled them about. 15:45:01 -!- addicted has joined. 15:45:03 Hm, I just thought of another scene that may be difficult to depict visually 15:45:28 anyway the going-through-matter thing isn't hard 15:45:34 that's like, standard effects stuff nowadays :P 15:45:42 I'm not thinking of that 15:45:47 Sgeo: "And then, HE SAW PI." 15:45:49 "ALL OF IT" 15:45:52 No 15:46:12 Oh, you mean using a narrator to depict stuff? 15:46:25 No, I just meant ridiculously impossible things :P 15:46:42 * Sgeo is watching SG-1 15:47:06 Also, now I have "Pi" in my head. 15:47:54 all of it? 15:48:18 http://www.songmeanings.net/songs/view/3530822107858715600/ 15:48:27 http://www.youtube.com/watch?v=Mfr7xG6smhU 15:50:12 * Sgeo saw that 15:50:28 Can't remember if that's the same song that.. 15:50:31 yes, it is 15:54:59 why do most languages lack such basic things as reading/writing numbers to arbitrary bases in the stdlib 15:55:20 it seems people just thought of the most common operations and never thought to parametrise them... or even to look at mathematics 15:56:39 MissPiggy: hey you know we were talking consciousness? 15:57:00 I found a paper by Nick Bostrom supporting two identical but separate brains experiencing two separate qualia-thingies 15:57:05 it's good 15:57:09 I think I've changed my opinion because of it 15:57:10 http://www.springerlink.com/index/V1X24V662H5726W5.pdf 15:57:29 ugh wants you to log in 15:57:29 sec 15:57:37 i have the pdf here 15:57:58 MissPiggy: http://filebin.ca/watags/experience.pdf 16:00:25 you have a springer link accout o_O 16:00:31 no :) 16:00:47 i have a computer that can access lesswrong.com, and i read a post where someone linked to a pdf 16:00:58 but uhh if you're impressed by that, I guess I should get an account 16:01:17 :P 16:01:32 but yeah... fuck non-open papers 16:01:34 with a chainsaw 16:02:16 * MissPiggy doesn't believe in qualia :( 16:02:22 well you don't have to 16:02:31 it's just being used as a less ambiguous term for consciousness 16:02:44 but qualia /are/ real; you know how you agreed totally with that Dennett video? 16:02:54 "A hardcore physicalist might be tempted to dismiss this question as being merely 16:02:57 terminological. However, I believe that we can give content to the question by 16:02:58 well - [Daniel Dennett writes that qualia is "an unfamiliar term for something that could not be more familiar to each of us: the ways things seem to us."] 16:03:01 linking it to significant ethical and epistemological issues." 16:03:03 Dennett believes in qualia :) 16:03:25 alise well Dennet said various obviously true statements collect in such a way that it gave him a strong context to argue against religion 16:03:29 qualia != metaphysics 16:04:03 i think you have a faulty heuristics system; it has some sort of rule "attempts to define aspects of consciousness => probably metaphysics => don't believe with high probability" 16:04:15 but that's not true 16:04:20 well I don't actually know what metaphysics is.. 16:04:25 bullshit :P 16:04:31 like "we have a soul" 16:04:46 "It is not easy to say what metaphysics is" -- groan 16:04:47 often "consciousness" is substituted for "soul" but they don't /mean/ what sane people mean when they say consciousness 16:04:49 they mean "soul" 16:05:17 rest assured that though there are metaphysical idiots who believe in a wrong thing they call qualia, qualia as Bostrom and Dennett mean it is just a term for our conscious experiences 16:05:33 alright 16:05:42 so don't be put off the paper by it :) 16:06:29 * MissPiggy is not quite sure if I read this whole paper.. the punchline will be "1 + 1 = 2" 16:06:50 hey, it makes a good argument 16:07:39 btw a fun thing: if you have an AI that has total flexibility with its thoughts; i.e. it can cause any brain state it likes, but it's in an environment with no colour, it can't experience red (apart from sheer chance by randomly modifying itself, ofc; but that's insanely risky and idiotic) right up until you explain how its brain processes colour 16:07:53 then it can just modify its thoughts so that it is experiencing the red quale :) 16:08:12 (basically a spin on the Mary's room thought experiment, http://en.wikipedia.org/wiki/Mary%27s_room, but that's intended to (unconvincingly) show that qualia are non-physical) 16:08:20 [[Later, however, he rejected epiphenomenalism. This, he argues, is due to the fact that when Mary first sees red, she says "wow", so it must be Mary's qualia that causes her to say "wow". This contradicts epiphenomenalism. Since the Mary's room thought experiment seems to create this contradiction, there must be something wrong with it. This is often referred to as the "there must be a reply" reply.]] 16:08:29 which is, yeah, exactly, debunked 16:09:04 also... is = on types well-defined? 16:09:16 i think so, but it makes me uncomfortable because from what i can tell it depends on what names you use 16:09:47 i.e. (data a = Z | S a) ≠ (data a = Zero | Succ a) 16:09:51 because they're different values 16:10:04 but then two (data a = Z | S a)s in different modules are not equal, either 16:10:11 so only Foo = Foo 16:10:28 alise hehe! I have tried to work hard on that problem :D 16:10:42 so I guess equality for types is "are they the same pointer" :) 16:11:05 they are isomorphic, so you can't prove they aren't equal... but both assuming they are and assuming they aren't are consistent axioms 16:11:18 well they aren't equal because Z is a distinct value to Zero 16:11:24 for instance 16:11:28 S Z -> S Z 16:11:30 but 16:11:34 S Zero -> type error 16:11:40 so Zero cannot be of the same type as Z 16:11:45 therefore type-of Zero != type-of Z 16:11:47 "Moreover, there are many local stochastic processes, each one of which has a non- 16:11:51 zero probability of resulting in the creation of a human brain in any particular 16:11:54 possible state.2" 16:11:57 what ... the... hell.... 16:11:57 basically I want to make * an instance of Collection 16:12:01 I bet this guy plays the lottery (and thinks he might win) 16:12:09 MissPiggy: no he doesn't 16:12:26 he's a bayesian rationalist, just like eliezer 16:12:38 so why is he making this argument :| 16:12:52 have you considered that perhaps you're wrong rather than him? 16:12:53 ""Therefore, if the universe is indeed infinite then on our current best 16:12:53 physical theories all possible human brain-states would, with probability one, be 16:12:57 instantiated somewhere," 16:12:59 that would resolve that cognitive dissonance 16:13:02 how can I possibly be wrong? 16:13:19 well, considering the probability that you might be wrong even for something you think is true is a key part of rationalism :p 16:13:31 also, he's right; it isn't *necessary* but it's probability 1 16:13:33 he says: infinite number of trials for a nonzero probability ==> it has happened 16:13:45 but that's so silly! 16:13:57 because all N-sized parts of space = all other adjacent N-sized parts of space is incredibly unlikely 16:15:07 roconnor has written some interesting things on when it's actually rational to play the lottery http://r6.ca/blog/20090522T015739Z.html 16:15:17 yeah I have read that 16:16:19 interesting technique this guy uses... 16:16:23 who 16:16:31 . This is another reason to accept Duplication. *20 16:16:32 O'Connor or Bostrom? 16:16:38 Bostrom 16:16:50 MissPiggy: well see now all I'm doing is wishing I hadn't linked it to you because all you're doing is, every few statements, making a quote and calling it nonsense 16:17:01 alise don't you agree ?? 16:17:05 and I think /both/ of us are less happy/enlightened for this 16:17:21 MissPiggy: that's irrelevant; you're not even considering the arguments or attempting to rebut them for what I can see, which makes me less happy 16:17:33 because such analysis of arguments is a good thing regardless of if they're true or false 16:17:39 i thought it was, at the very least, interesting 16:18:17 alise: http://en.wikipedia.org/wiki/Structural_type_system 16:18:30 "Some languages may differ on the details (such as whether the features must match in name)." 16:18:35 mm 16:18:43 imo: 16:18:45 S Z -> S Z 16:18:45 but 16:18:45 S Zero -> type error 16:18:45 so Zero cannot be of the same type as Z 16:18:45 therefore type-of Zero != type-of Z 16:18:45 proves it 16:18:54 so.. there is some kind of "quantum physics" thing.. which appears probabilistic and it might randomly generate a human being 16:19:05 if we have (data a = b) meaning "the data type a, constructors are: b" 16:19:05 AND the universe is infinte 16:19:12 therefore all possible humans have been created 16:19:19 MissPiggy: it's a _thought experiment_ 16:19:27 for the purpose of argument 16:19:32 oerjan: and we want to work out (data a = x) == (data b = y) 16:19:40 we should substitute a with b in x, and b with a in y 16:19:45 and make sure that "works" 16:19:56 S Z -> S Z, so substitute the a in a with a b: S Zero -> type error 16:20:00 therefore the types cannot be equal 16:20:10 this deduction is false though, consider the different between a NORMAL and non-NORMAL IRRATIONAL number 16:20:19 MissPiggy: he did not say 16:20:23 therefore all possible humans have been created 16:20:24 he said 16:20:28 all possible humans exist with probability 1 16:20:35 if you don't understand the different, read up on probability. 16:20:38 *difference 16:20:45 because it's /very/ important 16:20:55 well I know what probability 1 means 16:21:03 then you must agree that it is true 16:21:07 if an event has probability 1 _it has happened_ 16:21:11 you are wrong 16:21:12 right? 16:21:46 if an even has probability 1, every part of the sample space satisfies that event 16:21:47 P(x)=1 -> P(not x)=0 16:21:52 MissPiggy: NO! 16:21:56 that is frequentist statistics 16:22:02 we're talking _bayesian_ statistics 16:22:15 MissPiggy: this leads easily to a contradiction if you have uncountably many alternatives 16:22:38 http://en.wikipedia.org/wiki/Frequency_probability 16:22:38 http://en.wikipedia.org/wiki/Bayesian_probability 16:22:43 http://en.wikipedia.org/wiki/Probability_interpretations 16:22:48 ah so this is something to do with aleph_1 (or more) 16:22:50 (Bayesian rulez frequentist droolz, also) 16:22:53 uncountable sample space 16:22:56 MissPiggy: no 16:23:03 we're not talking frequentist statistics dammit :) 16:23:27 * oerjan only talks kolmogorov probability, really 16:23:48 bostrom is (almost certainly; I haven't read it directly, but it's very unlikely he isn't) a bayesian 16:23:56 so obviously he's talking nonsense per frequentist statistics 16:24:18 when he says the universe is infinite, which infinity does he mean? 16:24:22 >_< 16:24:29 or does it not matter? 16:24:33 you're focusing on the most irrelevant detail of a thought experiment 16:24:47 the point is that if the universe doesn't have bounds on space, P(every possible brain exists)=1 16:24:57 alise hey I don't know why it's irrelevant, the argument just sounds completely ridiculous to me and I'm trying to understand why not 16:25:01 therefore we assume that this is true, and use this as a thought experiment to show why Unification is nonsensical 16:25:32 I don't agree with the derivation of P(every possible brain exists)=1 16:25:49 the problem is that we're at a roadblock here 16:25:52 suppose in a 1mx1mx1m cube there is 0.1% chance of it happening 16:25:57 go read everything, I dunno, Eliezer Yudkowsky's written on bayesian statistics 16:26:00 then come back 16:26:02 and there is countably infinite of these blocks 16:26:13 MissPiggy: but space isn't divided into blocks 16:26:18 Then clearly there is a 100% chance of it having already happened. 16:26:20 :P 16:26:27 pikhq, how do you derive that? 16:26:41 the chance of there being some x*y*z region of space, and all adjacent x*y*z regions being identical, recursively 16:26:47 now *that's* low 16:26:59 now extend that to infinite space... 16:27:01 alise, why does it matter if space is in blocks or not? 16:27:01 and it has probability 0 16:27:08 MissPiggy: because it invalidates your argument 16:27:10 -!- scarf has joined. 16:27:17 alise, isn't that what you want? 16:27:36 MissPiggy: I don't want people to have invalid arguments; I want them, and me, to be right about everything 16:27:46 so if you make an invalid argument I will tell you why it is wrong in the hopes that you will fix your argument 16:27:50 or accept the opposite 16:27:57 scarf: hi 16:28:05 so okay, space isn't divided into 1mx1mx1m blocks 16:28:06 hi 16:28:15 so what does it mean 'space is infinite'? 16:28:31 >_< 16:28:37 Just that. 16:28:39 MissPiggy: imo (not bothering to read the actual argument) you assume independence of blocks that are too far away to interact. then countable infinitely many each with 0.1% chance does give probability 1 of at at least one (in fact, infinitely many) hitting that 0.1% chance 16:28:46 there are no bounds on the valid values of x,y,z in an (x,y,z) coordinate 16:28:46 pikhq, that's a nonsense statement though 16:28:47 MissPiggy: happy? 16:29:00 alise, if so then I dont see why we can't divide space up into blocks 16:29:05 you can 16:29:08 MissPiggy: What's nonsense about space being an infinite 3-space? 16:29:08 okay lets do that 16:29:09 but you can't postulate their inherency 16:29:16 ohh 16:29:25 you are saying there might be some dependent probability between them 16:29:58 when he says there is a nonzero probability, I wonder if he means a finite probability or an infintesimal one 16:29:58 your classification of space into blocks will be purely arbitrary is what I am saying 16:30:05 so you can only use them as notational shorthand 16:30:09 not as part of an argument itself 16:30:13 MissPiggy: finite 16:30:25 nonzero probability of x = P(x)>0 16:30:47 so lets assume the universe is divisible into countably many 1m^3 blocks, and each one has a proability 0.1% of creating a human brain 16:31:01 creating? 16:31:01 in two of these blocks there is what? 0.2% probability? 16:31:04 space doesn't "create" anything 16:31:11 "Moreover, there are many local stochastic processes, each one of which has a non- 16:31:15 zero probability of resulting in the creation of a human brain in any particular 16:31:18 yes 16:31:18 possible state.2" 16:31:20 PROCESSes 16:31:21 not space 16:31:38 MissPiggy: just a question 16:31:44 okay lets cut space into countably many cells, each of which one of these processess are happening 16:31:44 do you even know what bayesian probability is? 16:31:52 if not... we cannot possibly have this conversation 16:31:55 in two of these blocks there is 0.02% probability? 16:32:29 and if we have a million blocks there is 1000000x0.1% probability (which is greater than 1!) 16:32:40 and if we have countably infinite there is a divergent probability 16:32:44 http://en.wikipedia.org/wiki/Bayes%27_theorem anyway 16:32:54 so this guys argument is basically nonsense, agreed? 16:32:56 read it, learn, *then* come back 16:33:03 I know bayes theorem alise 16:33:11 MissPiggy: no, I am almost certain you have no idea about how bayesian probability works 16:33:15 MissPiggy: you really need to assume independence of the blocks to do a meaningful calculation here, imo 16:33:18 I do not agree 16:33:34 alise I will admit I got Yudkowskis breast cancer experiment wrong 16:33:42 in which case you take 1 - (1-0.02%)^n 16:33:46 stop spelling his name wrong 16:33:55 sorry 16:34:01 :p 16:34:43 i fucking hate zooko's triangle!! 16:34:45 i want my free lunch 16:34:56 MissPiggy: you don't _sum_ probabilities unless they are mutually exclusive events 16:34:57 -!- oklopol has joined. 16:35:24 oerjan I was assuming they are mutually exclusive, that seems to be in line with the idea of a 'local' event 16:35:51 MissPiggy: mutually exclusive means it cannot happen in two blocks simultaneously. that seems nonsense. 16:35:59 oh 16:36:03 I meant independent sorry 16:36:16 MissPiggy: in which case summing is even more wrong :D 16:36:27 in which case you take 1 - (1-0.02%)^n 16:36:56 um, 0.1% there 16:38:12 I wish there was a mathematical hierarchy for things like sets and lists like there are for numbers 16:38:15 monoids, rings, etc etc etc 16:38:19 collections, sequences, etc etc etc 16:38:20 * oerjan also sees absolutely no reason to bother with frequentist vs. bayesian distinctions for this argument 16:38:32 oh so if we have blocks A and B, then for it to happen in A only: 0.1% * (1-0.1%) (same for B only), and for it to happen in A and B it's 0.1%^2, so the chance of it happening in at least one is 2(0.1%)(1-0.1%)+(0.1%)^2 16:38:40 as it is the reasoned language designer must come up with his own hierarchy :( 16:38:56 oerjan: well, i was mentioning it /in case it came up/ because if it does it will be bayesian statistics being used 16:39:06 ok 16:40:20 okay maybe this would work better if I shut up an alise explains the paragaph? please :) 16:40:21 MissPiggy: which conveniently is easier to calculate by multiplying the probabilities of it _not_ happening in either 16:40:37 MissPiggy: I wouldn't know how to explain it; I can understand it but not serialise my understanding function. 16:40:49 alise so it's bullshit 16:40:50 Especially as I'm not sure exactly what you don't get. I'll leave the dirty work to oerjan. :) 16:40:56 MissPiggy: That does not follow; you are being irrational. 16:41:11 this pretending to be a rationalist thing is kind of lame 16:41:34 Yes, because we were talking about statistics and because I am saying you are being irrational, I am some sort of fake imposter rationalist! 16:41:39 MissPiggy: now if we have n blocks, the chance of it happening in none is (1-0.1%)^n, which -> 0 when n -> infinity 16:41:40 Yawn. 16:42:04 oerjan how do you derive that formual though 16:42:20 say the chance of it happening in one block is p, 16:42:22 it's the definition of independence in probability theory 16:42:24 then chance of not happening is 1-p 16:42:35 the chance of not happening in both blocks is (1-p)^2 16:42:43 P(A and B) = P(A)*P(B) 16:42:51 so that works out nicely, 16:43:03 but let us consider, the chance of it happening in two blocks = 2p 16:43:07 why is that false? 16:43:26 or, can I use the divergence of that (when the number of blocks reaches infinity) to show this statement is bogus 16:43:48 it's false because you can only sum exclusive events 16:44:25 that alise, Miss Piggy argument is better when you read alise as being voiced by kermit the frog 16:44:36 :-D 16:44:50 P(A or B) = P(A) + P(B) - P(A and B), if P(A and B) != 0 then it's not just the sum of each 16:45:15 hm 16:45:18 but say, p = 0.1 16:45:27 ohh 16:45:29 okay yeah 16:45:42 so right the probability is 1! 16:46:18 yay! 16:46:19 -!- oklopol has quit (Remote host closed the connection). 16:46:24 yay! 16:46:27 now we are all happy! 16:46:50 hmm 16:47:08 if I want to be able to do things like "foo : card empty = 0" (card=cardinality) 16:47:14 then I need = to return a type 16:47:17 so I need True/False to be types 16:47:31 so I need Bool be a type whose values are the type True and the type False 16:47:45 and True to be a type with one value, refl or whatever 16:47:50 and False to be a type with no values, i.e. Void 16:48:00 which also lets us use False as the constructivist _|_ 16:48:13 e.g. (p, Not p) -> False 16:48:30 hmm, hey 16:48:36 so what does probability one mean? 16:48:36 can you constructively prove that False -> a? 16:48:43 MissPiggy: that the probability of it not happening is zero 16:48:50 alsie that's the induction scheme for the empty type 16:49:07 if you have a value of False it's bottom but that doesn't mean you can treat it as an a 16:49:10 alise no what does it mean 16:49:11 (because `data False`) 16:49:17 MissPiggy: well it means exactly that 16:49:22 :/ 16:49:34 oerjan: you give him a boring, actually useful explanation 16:49:35 MissPiggy: calculating with probabilities is easy, understanding what they mean is i guess where you need to get into that interpretation stuff 16:49:38 (bayesian this time since it /does/ matter) 16:50:02 alise: except i hate that stuff myself... :D 16:50:15 define that stuff 16:50:25 "that interpretation stuff" 16:50:29 1. Frequentists talk about probabilities only when dealing with experiments that are random and well-defined. The probability of a random event denotes the relative frequency of occurrence of an experiment's outcome, when repeating the experiment. Frequentists consider probability to be the relative frequency "in the long run" of outcomes.[1] 16:50:30 2. Bayesians, however, assign probabilities to any statement whatsoever, even when no random process is involved. Probability, for a Bayesian, is a way to represent an individual's degree of belief in a statement, given the evidence. 16:50:40 MissPiggy: you probably think of #1 as the intuitive meaning of probability thus your confusion 16:50:45 but bostrom as a bayesian means #2 16:50:56 alise, my confusion what that I didn't know how to add probalities :| 16:51:01 [[An impossible event has a probability of 0, and a certain event has a probability of 1. However, the converses are not always true: probability 0 events are not always impossible, nor probability 1 events certain. The rather subtle distinction between "certain" and "probability 1" is treated at greater length in the article on "almost surely".]] 16:51:03 http://en.wikipedia.org/wiki/Almost_surely 16:51:16 MissPiggy: your confusion because you thought prob = 1 = has happened 16:51:23 can you constructively prove that False -> a? <-- is an axiom i think 16:51:27 basically though just read http://en.wikipedia.org/wiki/Almost_surely 16:51:44 oerjan: Haskell is a constructivist logic, right, if you make sure never to use _|_? 16:51:57 trying to treat haskel as a logic is a mistake 16:51:57 You can't do `data False` and then write a `False -> a` in Haskell, at least 16:52:00 I know 16:52:08 just pretend haskell lets you do 16:52:14 magic f = case f of {} 16:52:15 but if you require a proof of totality in some other lang, and remove undefined and unsafePerformIO and unsafeCoerce and the FFI 16:52:27 then it should be a constructivist logic I think 16:52:29 which is actually valid in Coq 16:52:35 I guess so 16:52:44 anyway my main point is 16:53:07 thetype True = {refl:True} 16:53:10 thetype False = {} 16:53:11 thetype Bool = {True:*, False:*} 16:53:18 I:True is used in Coq 16:53:20 does this make sense? and is it a good idea? 16:53:21 or is it a pitfall 16:53:22 alise: avoiding full recursion is more important i should think 16:53:26 Bool doesn't make sense 16:53:31 oerjan: thus the requirement of a proof of totality 16:53:34 (well you need that to construct _|_ of course) 16:53:46 MissPiggy: hmm are you sure? 16:53:54 to me it doesn't make sense! 16:53:56 if you have unions you can't say that a value is of only one type 16:54:07 so it's not a stretch to have True be both a * and a Bool 16:54:15 it just means that 16:54:17 Bool is-a-subset-of * 16:54:21 and there's nothing wrong with that! 16:54:32 maybe yeah I suppose you could make that work.......... 16:54:41 it's a bit scary though 16:54:53 and it means we can stop doing everything at both value and type level every time we want to get our dependent shizzit on 16:55:04 MissPiggy: yeah but I want * to be a Collection anyway :-) 16:55:27 so i'm sort of already in the direction of "hey these are actually quite ... tangible" 16:56:44 probability 1 only means surely in the case of a finite space? 16:56:57 MissPiggy: countable works too 16:57:06 oh! 16:57:20 so it's sort about aleph_1 16:57:23 probabilities are lebesgue measures, so countably additive 16:57:51 s/lebesgue measures/measures/ 16:58:23 (invented by lebesgue, in any case) 16:58:38 (and adapted to probabilities by kolmogorov, iirc) 16:58:47 okay 16:59:14 probability 1 doesn't really tell you anything then :| 16:59:25 because who knows which infinite we have 16:59:59 MissPiggy: well you can pretend it means surely, as long as you only test countably many cases 17:00:25 haha my mistake from earlier was soooo stupid 17:00:44 if you flip a coin twice it doesn't mean you will have seen heads and tails 17:00:53 and for brains, well assuming you have some limited precision, it seems like there would be only finitely many possibilities that could fit into a 1m^3 cube 17:02:04 that's my intuition on that anyway - the distinction between probability 1 and surely is only needed because of uncountability stuff 17:02:42 so _in practice_ it means surely 17:02:44 okay! 17:02:53 wait 17:03:02 in practice?? what about this situation 17:03:21 we are assuming the universe to be divisible into countably many blocks? 17:03:44 I don't think there's any evidence for that rather than uncountable 17:03:59 MissPiggy: well you could just take a countable subset of them... 17:04:23 yes but that wouldn't cover the whole universe 17:04:48 well no, but you need only to get all your brains into part of it to prove they exist :D 17:04:49 wait this is paradoxical 17:04:58 -!- addicted has quit (Quit: Konversation terminated!). 17:05:09 it needs to be a random subset, i guess 17:05:09 how can you have it certinaly happening in a countable subset, but we're not sure if it will in an uncountable one.. 17:06:14 of course if it's not random, everything's out the window anyway, just pick a subset that does _not_ include all possible brains (say, because you explicitly look for only one type) 17:06:44 blegh! now I know how finitists feel! 17:06:50 heh 17:06:58 I just want to say "but you can't apply this probability argument to INFINTE SPACE" 17:07:08 but I don't want to give up on understand this either 17:07:42 I mean really this argument can prove anything has probability 1... 17:08:15 I could argue in the same way there is a guy who /is capable of and is right now/ about to tell me something through some kind of interstellar mobile phone 17:08:24 MissPiggy: http://en.wikipedia.org/wiki/Kolmogorov's_zero-one_law 17:08:25 but this it doesn't happen... 17:08:42 no you can't 17:09:06 that might be because the universe isn't actually infinite. 17:09:09 you could prove that in an infinite universe there is probability 1 that there is a planet exactly like earth somewhere except where that is happening 17:09:28 but you're almost certainly not on that earth, and the universe might not even be infinite. 17:09:30 deschutron yeah, but for this argument he is assuming it is infinite (which infinity?) 17:09:33 and it's still only probability-1 17:09:35 not _does_ exist 17:10:01 alise why can't I show there's someone who is about to phone ME? why do they have to be phoning someone else 17:10:08 say, do set theorists have a symbol for the set of all sets? or has russell scarred them away from that 17:10:16 another place where type and set theory clash :P 17:10:19 that person is in another block 17:10:33 MissPiggy: they could phone you if you had an interstellar phone that somehow did FT 17:10:35 *FTL 17:10:41 but since it's about *the size of space* 17:10:43 yeah so maybe FTL is impossible 17:10:45 you can't apply it to earth 17:10:48 which is very finite, and small 17:11:07 so this is evidence against FLT :P 17:11:10 the whole point is that there is probability one that ****somewhere**** in space there is a copy of this planet except with that guy 17:11:15 about to phone that earth's you 17:11:35 I wish there was a nice symbol for the holes in mixfix operators 17:11:56 in an infinite universe, there would be copies of both versions - you being phoned and you not being phoned. 17:12:10 as long as the phoning follows the laws of physics :P 17:13:22 not there would be 17:13:26 there is probability 1 that there would be 17:13:27 also dammit 17:13:30 I really want some sugar for 17:13:41 (a:t)->(b:t)->(c:t)->...->foo 17:13:45 alise: a bullet? 17:13:48 * MissPiggy gives alise a bowl of sugar 17:13:53 like for types, forall a b c. is that for t=Type 17:14:00 maybe I should just generalise forall 17:14:02 x^bar : t^bar -> foo 17:14:11 and let you do forall (a:somethingotherthanType) 17:14:13 vector notation like in physics 17:14:18 forall (a:t) (b:t) (c:t). 17:14:24 in fact forall a implies an implicit argument 17:14:29 which I'm fine with it's equivalent 17:14:37 forall (a b c : t). 17:14:45 yes 17:14:53 MissPiggy: actually that link above was maybe not quite what i thought it was, http://en.wikipedia.org/wiki/Law_of_large_numbers#Strong_law is closer 17:15:28 assoc : (a:m) → (b:m) → (c:m) → (a·b)·c = a·(b·c) 17:15:29 becomes 17:15:58 assoc : ∀a b c : m. (a·b)·c = a·(b·c) 17:16:01 which is equiv. to 17:16:10 assoc : {a:m} → {b:m} → {c:m} → (a·b)·c = a·(b·c) 17:16:22 i guess the a/b/c will be inferred to be 0 17:16:28 since from inside monoid that's the only m you know exists 17:16:29 well 17:16:35 you also know that 00 exists :P 17:16:42 and so on 17:16:47 hmm 17:16:49 MissPiggy: maybe I should just let you do 17:16:57 (a, b, c : m) -> ... 17:17:04 it just feels weird to have them all on one side of a -> so to speak 17:17:05 whats the poit of the commas? 17:17:07 because it nests rightwards 17:17:15 MissPiggy: otherwise it's pattern matching :P 17:17:17 it's like writing 17:17:20 let a b c = m 17:17:26 defines a function a 17:17:39 e.g. you can do (Just a : Maybe) -> ... 17:18:09 ok 17:18:44 the problem is that (a,b:t)->s is (a:t)->((b:t)->s) 17:18:51 whereas it looks like something confined to the LHS 17:19:09 the problem with the forall one is that they become implicit arguments, which usually isn't desired 17:19:22 also, you only really use this for propositiosn 17:19:27 *propositions 17:19:45 you wouldn't say () : (_, _ : m) -> m 17:19:47 because that's just ridiculous 17:19:51 so i dunno 17:20:30 http://r6.ca/blog/20030729T014400Z.html 17:20:31 m -> m -> m 17:20:45 apparently agda uses (a:t)(b:s)->r 17:20:47 erm 17:20:48 coq 17:20:49 not agda 17:20:53 not sure what it translates to though 17:22:15 it's not valid 17:22:34 (f:Morphism)(g:Morphism)->(Range g)=(Domain f)->Morphism 17:22:38 has to be rewritten as 17:22:41 forall (f:Morphism)(g:Morphism),(Range g)=(Domain f)->Morphism 17:22:43 to be accepted 17:22:58 well it is a post from 2003 17:23:01 so maybe it was valid then 17:23:09 ok so coq adopts my notation too 17:23:16 forall that is 17:23:22 I just simplify it to let you name the type only once 17:23:41 and uses a comma to separate forall and the rhs, I like that 17:25:56 wait 17:26:05 naturals and rings and stuff can be monoids under addition /or/ multiplication 17:26:25 does this mean I shouldn't name the identity and thingy functions 0 and *? :( 17:26:39 additiveMonoid 17:26:42 :P 17:26:56 I use e and & 17:26:56 e&e = e 17:27:04 yeah 17:27:05 but 17:27:13 it'd be so orgasmically awesome to be using monoids every time you multiply 17:27:29 Hm. 17:27:32 "Aliselang: You *do* need to know category theory to get things done in THIS one!" 17:27:38 The date on this thing has to be wron 17:27:40 *wrong 17:27:52 erm, time 17:28:38 MissPiggy: also it wouldn't be the type of monoid that changes 17:28:40 just two different instances :) 17:28:50 who says you can't have two values of type Monoid ZZ 17:30:42 but damn 17:30:49 i really was all COOL SHIT about calling 'em 0 and * 17:30:53 i feel so humbled 17:31:19 i am ensaddened 17:31:50 um you know 0 goes with + and 1 with *, usually... 17:32:32 i know 17:32:38 but I was literally going to have: 17:33:08 Monoid : Type -> Type 17:33:08 Monoid a = { 17:33:08 0 : a 17:33:08 (*) : a -> a -> a 17:33:08 assoc : forall (a:m) (b:m) (c:m), (a*b)*c = a*(b*c) 17:33:09 ...the identity element property that I can't have here because it leads to saying 0*x=x... 17:33:11 } 17:33:32 -!- deschutron has left (?). 17:33:36 O_o 17:34:43 what 17:34:52 i'm 17:34:53 Moniod m (&) e = Semigroup m (&) /\ Identity m (&) e ? 17:34:56 i think i'm totally wrong and confused 17:35:04 because something is going wrong. in my brain. 17:35:05 MissPiggy: lol 17:35:13 olol :( 17:35:43 hmm 17:35:45 alise: hey don't have a stroke, now 17:35:47 I should have a semigroup 17:35:56 ...also i need some sort of sugar for defining a bunch of "instances" 17:36:08 otherwise you'll have like 50 instance values of a few lines each 17:36:16 just to get + - and * :P 17:36:41 oh great, and I need magmas too if I really want to get down 'n dirty 17:36:48 kill me now 17:37:18 the problem is even worse 17:37:26 it doesn't seem like a linear heirarchy... 17:37:33 Magma : Set -> Set 17:37:33 Magma a = { 17:37:34 () : a -> a -> a 17:37:34 } 17:37:42 Most useful typeclasswhatever ever? 17:37:44 Yes! 17:37:45 how about 17:37:52 In fact you know what? 17:37:57 Magma a (•) = True 17:38:01 (Magma a) is equivalent to (a -> a -> a) 17:38:13 MissPiggy: lol you've adopted my set/type idea 17:38:30 have I !! 17:38:35 yes 17:38:38 Set = a -> Bool 17:39:06 aahaha 17:39:08 Anyway, since Magma a ≡ (a -> a -> a), I don't need it. 17:39:12 yes yo udo ! 17:39:18 At the most, I need Magma = a -> a -> a 17:39:22 MissPiggy: I don't. 17:39:30 { x : t } ≡ t 17:39:45 Magma a = { () : a -> a -> a } 17:39:55 ∴ Magma a ≡ a -> a -> a 17:40:20 So at the most, I need Magma a = a -> a -> a; a simple alias. But I think it is easier just to write a -> a -> a. 17:41:59 MissPiggy: So why do I need Magma? 17:42:38 Say... 17:42:44 I run into problems using = for my relationships like associativity. 17:42:51 Specifically, I require a definition of equality for that set. 17:42:57 I should instead use ≡, I think. 17:43:15 ≡ : a -> a -> IsEquivalent a a 17:43:21 Hm 17:43:24 so basically (a ≡ b) is a proof that a and b have identical semantics 17:43:29 (misspiggy: is this well defined?) 17:43:40 Is there a page where I can see what it's like to visit an SSL website with a revoked certificate? 17:43:57 ≡ tends to be used for definitions, no? 17:44:28 i don't use it for definitions, so 17:44:30 = is when you apply not just definitions, but also properties and axioms 17:44:33 and it does mean "is equivalent to" 17:44:47 maybe semantics proofs has it otherwise 17:45:01 * alise tries to think of a nice, non-* binary op name for the semigroup operation 17:48:46 Semigroup : Set -> Set 17:48:46 Semigroup a = { 17:48:47 (something) : a -> a -> a 17:48:47 assoc : forall (x:a) (y:a) (z:a), (xy)z === x(yz) 17:48:47 } 17:49:12 set theory is hotttt 17:51:00 no it's not!!!!!!!!! 17:51:04 WHY NOT 17:51:14 http://en.wikipedia.org/wiki/Perverse_sheaf 17:51:31 what's wrong with perversity 17:52:38 MissPiggy: i want all these lovely proofy things but i want partiality :( is there a therapy group for me 17:54:15 -!- kar8nga has joined. 17:54:30 yes you do need therapy 17:54:33 at least you can admit that.. 17:54:45 :) 17:54:53 Set_1 in agda is Set->Set right? 17:55:00 no don't think so 17:55:02 Set : Set1 17:55:06 -!- SimonRC has quit (Ping timeout: 265 seconds). 17:55:06 Set1 : Set2 17:55:13 ah 17:55:24 so Set_n is "set of {sets*n+1}" 17:55:26 Set : set of sets 17:55:29 Set1 : Set of (set of sets) 17:55:36 so Semigroup : Set1 means that Semigroup is a set of sets 17:55:43 so (a -> Bool) -> Bool 17:55:56 so Semigroup a means "is the set 'a' a Semigroup?" 17:56:08 now if only I understood the definition :) 17:56:59 hmm wait 17:57:34 so does {Semigroup a} -> mean "a set 'a' that is a semigroup"? 17:57:44 so then Semigroup a :: Set 17:57:53 but then is the resulting set a, or the semigroup stuff? 17:57:55 this is confusing 18:00:29 lol 18:00:37 MissPiggy: look at agda's stdlib lib/Algebra.agda 18:00:53 whenever there's controversy 18:00:54 they're just like 18:00:56 oh we'll put both in 18:01:00 SemiringWithoutAnnihilatingZero 18:02:13 I find it strange how many types Agda folk like to hide their things behind 18:02:16 _∙_ : Op₂ Carrier 18:02:26 why is this better than _∙_ : Carrier -> Carrier -> Carrier? 18:02:42 good question 18:02:44 idk 18:03:01 i guess it's so that you repeat less and have "more semantic" types 18:03:04 but I just find it obscures the meaning 18:03:17 also, 18:03:19 _≈_ : Rel Carrier zero 18:03:21 that is so a copout 18:03:30 just including "some sort of kinda equal thing that you want to be for the associativity" 18:03:42 a ≡ b ftw 18:04:00 _≡_ : a -> b -> Bool 18:04:04 (except you use it as a type, obviously) 18:04:13 just exploiting that Bool is True-or-False 18:04:22 and we use ≡ to prove two expressions equivalent 18:04:49 what's wrong with 18:05:05 Identity : forall T : *, T -> T -> * 18:05:22 what's the result? 18:05:28 reflexivity : forall (T : *) (t : T), Identity T t t 18:05:51 clearly if a and b have the same normal form, then reflexivity _ a : Identity _ a b 18:06:43 oh, agda calls the identity element of a monoid ε 18:06:44 good choice 18:07:52 A monoid whose operation is commutative is called a commutative monoid (or, less commonly, an abelian monoid). 18:07:52 what's wrong with e 18:07:57 heh, I've only ever heard abelian monoid 18:08:05 MissPiggy: well e is just an approximation of \epsilon used because we can't type e :P 18:08:16 also, because naming a parameter e is... not uncommon 18:08:18 but we use e in math-on-paper :[ 18:08:31 and it'd be nice to still be able to get at monoid identity while doing so 18:08:39 also, MissPiggy, what is the result of Identity? 18:08:42 i.e. the * in -> * 18:09:17 * is Set 18:09:28 yes 18:09:29 A : * means A is a type 18:09:30 but what is its _value_ 18:09:37 what set is it for some T 18:09:37 * is in normal form 18:09:41 and the two values 18:09:49 Identity T t t : * 18:09:54 3 : Nat : * 18:10:05 Identity Nat 3 2 : * 18:10:11 yes 18:10:18 so what is its use? 18:10:22 ??? 18:10:26 what's whats use 18:10:29 I guess as part as "reflexivity : forall (T : *) (t : T), Identity T t t" 18:10:33 *as part of 18:10:36 that's the constructor 18:12:01 also 18:12:04 Unifiable : Set → Set 18:12:04 Unifiable a = { 18:12:04 _=_ : a → a → Bool 18:12:04 leibniz : ∀(f:a→b) (x:a) (y:a). x = y → f x = f y 18:12:04 } 18:12:07 too far? 18:12:24 the issue is that you could have something with multiple internal representations that have different values, _but you don't expose the constructors_ 18:12:27 -!- SimonRC has joined. 18:12:30 so from outside the module you can prove leibniz 18:12:38 but from inside, where you define the Unifiable instance, you cannot 18:12:46 so you can make it Unifiable 18:12:49 but only from inside a different module :) 18:13:00 that's like quotients 18:13:01 also, proving it may be *spectacularly* hard for some things, I expect 18:13:14 you can divide a type by an equivalence relation to make a 'smaller' type 18:13:31 like howso 18:14:36 hey I just had a thought 18:14:47 often in my dependent musings I wish to write something like 18:15:13 optimise : (a:ProgramInSomeLang) -> ((b:ProgramInSomeLang), a `hasTheSameSemanticsAs` b) 18:15:20 but then you need to unpack the tuple and all and it's woeful to use 18:15:20 BUT 18:15:22 you could do 18:15:31 (substituting Prog and `equiv` for those verbose names) 18:15:41 optimise : (a:Prog) -> {a `equiv` b} -> (b:Prog) 18:15:51 i.e. force the *caller* to prove that the optimisation preserves semantics 18:15:53 backwards binding!! 18:15:57 since it's implicit You Don't Have To Worry About It 18:16:01 MissPiggy: is that a yay or a yikes !! 18:16:22 proving something about the result of a function before you can get to it... hehehe 18:17:23 * alise gets a silly idea of having Axiom be a type 18:17:52 Axiom : *; Axiom = { foo : *, bar : foo } 18:18:01 except you can make non-axiomatic foo/bar pairs with it 18:18:02 :( 18:18:09 so clearly we need some way to determine whether something is axiomatic :P 18:18:37 Axiom : *; Axiom = { prop : *, axiomatic : isAxiomatic prop } 18:19:41 MissPiggy: so is backwards binding nice or evil or sth? 18:19:48 BOTH 18:20:01 MissPiggy: how's it evil? 18:20:05 like what horrible things does it let you do 18:20:25 I don't know it's just hard 18:20:40 to impl? 18:20:49 slow to typecheck or sth? 18:21:06 stop writing sth :/ 18:22:28 sorry 18:22:29 old habit 18:23:07 * MissPiggy cries and weeps 18:23:41 for the sth time, stop writing sth 18:23:52 lLOL 18:24:49 MissPiggy: so is it 18:25:42 data Identity : (a:*) -> a -> a -> * where reflexivity : forall (x:a). Identity a x x 18:25:52 so 18:26:02 reflexivity : Identity NN 3 3 18:26:06 but not reflexivity : Identity NN 3 2 18:26:54 i guess what I'd want then is something that transforms that into the set True or False so I can prove it like any other true/false thing in my lang 18:27:59 MissPiggy: also in your "forall (x:a)" is that basically an implicit argument 18:28:02 I think it is I think it iiiiiiis :P 18:28:03 huh? 18:28:09 huh what 18:28:14 forall {x:a}, is implicit 18:28:19 but forall (x:a), is not 18:28:19 right 18:28:25 but it can be implicit 18:28:31 and I don't see why it shouldn't be 18:28:34 data _≡_ : {a:Set} → a → a → Set where 18:28:34 reflexivity : {x:a} → x ≡ x 18:28:51 (substitute another symbol for \equiv if you want, but you get the idea) 18:28:54 yeah sure make it implicit if you want that's JUST SYNAX 18:28:54 SYNTAX* 18:28:58 yes 18:29:04 that way your proof if inferrable can just be "reflexivity" I think 18:29:11 hmm 18:29:14 so is refl = reflexivity? 18:29:18 I don't actually know why refl is called refl 18:29:23 refl-exivity 18:29:25 :DDD 18:29:26 right 18:29:29 but I mean 18:29:33 it's expressing that x = x (forall x) 18:29:35 people seem to use the name refl a lot in different types 18:29:43 (which implies symmetry and transitivity) 18:29:43 or are they all just specific instances of this? 18:29:54 like I'm used to thinking of implicit arguments as being filled in with refl. 18:30:06 oh well I don't know which examples you mean -- I haven't seen peopl ues refl much 18:30:37 perhaps 18:30:40 http://en.wikipedia.org/wiki/Quotient_set 18:30:41 so 18:30:41 we have 18:31:01 data Frac : * where Over : Z -> Z -> Frac 18:31:02 -!- sshc has quit (Ping timeout: 246 seconds). 18:31:21 so the equivalence class of (Over 1 2) in Frac is 18:31:32 {Over 1 2, Over 2 4, Over 3 6, ...} 18:31:32 right? 18:31:54 so to make the rationals we do 18:32:08 (a,b) ~ (c,d) = (a*d == b*c) 18:32:16 and then use that ~ on Frac 18:32:18 and get the rationals? 18:35:19 so 18:35:20 data _≡_ : {a:Set} → a → a → Set where 18:35:20 refl : {x:a} → x ≡ x 18:35:25 is correct, then 18:35:31 (although you'll probably bitch about the symbol I used :)) 18:35:38 i hope at least that 18:35:40 Unifiable : Set → Set 18:35:40 Unifiable a = { 18:35:41 _=_ : a → a → Bool 18:35:41 leibniz : ∀(b:Set) (f:a→b) (x:a) (y:a). x = y → f x = f y 18:35:41 } 18:35:43 is unobjectionable enough to you 18:37:34 ah, fried blood <3 18:37:56 blech 18:38:00 we are no longer friends 18:38:40 :P 18:38:53 coming up with a syntax for record types is hard 18:39:08 you can have 18:39:09 record Unifiable : Set → Set where 18:39:09 _=_ : a → a → Bool 18:39:09 leibniz : ∀(b:Set) (f:a→b) (x:a) (y:a). x = y → f x = f y 18:39:19 but then 1. it's confusing alongside the GADT syntax 18:39:26 2. you never specify that a is your agument! 18:39:28 *argument 18:39:48 incidentally i should probably find another name for Leibniz's law rather than implying that Leibniz was literally a proof 18:41:32 I thought you were still on my topic and constructing proofs about blood pudding, but then I started actually reading :) 18:43:06 :DD 18:43:31 -!- sshc has joined. 18:45:54 you know I prefer it when MissPiggy is angry at me and tells me what i should be doing instead 18:46:19 hmm 18:46:27 I guess if I want 18:46:28 _=_ : a → a → Bool 18:46:28 leibniz : ∀(b:Set) (f:a→b) (x:a) (y:a). x = y → f x = f y 18:46:42 from inside something with a non-identical constructor equality thingybob that nevertheless satisfies that outside of the module 18:46:52 then I need to actually have a notion of "modules" in the type system 18:46:57 as a vampire, alise does not approve of frying blood before eating 18:47:03 so that leibniz can express the privateness of it or something 18:47:11 so that we can say "outside the module, (leibniz's law)" 18:47:50 oerjan: as a norwegian, do you approve? 18:48:07 yes 18:48:16 although i haven't had it in a long time 18:50:02 MissPiggy: i have a feeling this thing is going to end up with me having a type-safe model of the language itself, and the logical system its type system isomorphs to, inside the language/type system 18:50:21 and making proofs by proving that it's true inside that model, and then lifting it out 18:50:23 xD 18:51:05 wouldn't that tend to risk hitting godel's theorem 18:51:26 I don't think so, proving (P in this system) should be identical to proving P, shouldn't it? 18:51:28 (having a model of the whole means the whole is consistent) 18:51:34 nope 18:51:36 it's loeb? no 18:51:38 the model could depend on the inconsistent parts 18:51:42 :) 18:52:50 i mean means the whole can be proven consistent 18:53:00 oh well maybe not 18:53:29 of course the issue there is that you need an inconsistent system 18:53:31 which isn't so good. 18:54:48 hmm you could have x ≊ y = (reduce x) = (reduce y) 18:54:52 except I guess you might not have = 18:55:21 i wonder if using = for unification /and/ definition will get confusing 18:56:08 hey can't you have _|_ with codata? 18:56:11 like having co_|_ or something 18:56:20 prolly not 18:59:48 no, you always must be able to unpack one more constructor in finite time 18:59:52 iiuc 19:00:30 darn :) 19:01:17 but you can of course have fix Later 19:01:50 fakeBottom = Later fakeBottom 19:01:59 yes 19:02:03 but that's just the partiality monad 19:02:08 yep 19:02:10 (which i think gives turing completeness right?) 19:02:24 well sure 19:02:29 problem is you have a lot of things which /are/ partial but the compiler can't infer to be so 19:02:40 maybe you should be able to manually specify a halting proof 19:03:50 -!- oklopol has joined. 19:04:01 -!- sshc_ has joined. 19:04:06 why hello thar oklopol 19:04:28 -!- Gracenotes has quit (Remote host closed the connection). 19:06:59 -!- sshc has quit (Ping timeout: 252 seconds). 19:07:15 data _≡_ : {a:Set} → a → a → Set where 19:07:15 refl : {x:a} → x ≡ x 19:07:15 is pretty damn awesome though 19:07:18 why didn't I think of that 19:07:50 I just showed you that :| 19:07:53 i know 19:07:58 thus "why didn't I think of that" 19:08:09 MissPiggy: oh ho, I've just realised why agda repeats all the fields in each iteration of more advanced set type thing 19:08:23 because it's inverted; instead of depending on the parent, it contains the parent constructed from the fields 19:08:34 pro: you only need to instantiate the topmost one 19:09:01 con: if there are two ones that apply (e.g. a split in the hierarchy) you have to type some declarations as aliases for the other ones; makes the definitions of the thingies more verbose in the stdlib 19:09:30 also, argh, I should really figure out quotients and carriers; both agda and epigram are all up wit dem and I don't get it yet 19:09:54 -!- oklopol has quit (Read error: Connection reset by peer). 19:09:55 Each Set universe (and so far there is one, inconsistently containing itself, but later we shall have some sort of hierarchy) 19:09:57 why don't we just have 19:10:26 Set : (n:Nat) -> Setѡ 19:10:30 where Setѡ is some other thing 19:10:33 or wait it's actually just 19:10:39 Set : (n:Nat) -> Set (n+1) 19:10:46 surely that's the simplest way 19:10:51 Set 0 is * 19:10:56 Set 0 : Set 1 19:10:57 and so forth 19:12:20 hey, scarf is still here 19:12:40 yep 19:12:51 busy helping with a community nethack game, sorry 19:20:50 -!- oklofok has joined. 19:30:38 natInduction : (f:Nat→Bool) → f 0 → (∀(n:Nat), f n → f (succ n)) → (∀(n:Nat), f n) 19:30:38 I think 19:31:34 well?? 19:31:39 MissPiggy: well what? 19:31:45 I was just writing things because I felt like it 19:31:59 why is it into bool instead of into *? 19:32:14 and the other thing is you have not --> forall n, P n at the end 19:33:33 well because I like having a type that lets me express "some true or false proposition to be proved" 19:33:39 * is needlessly general 19:34:15 but the thing with induction into * is you can use it to prove stuff or to do recursive programs 19:34:35 omg really? 19:34:36 :D 19:34:40 (re: recursive) 19:35:45 also 19:35:45 and the other thing is you have not --> forall n, P n at the end 19:35:47 I don't see what you mean 19:36:12 also wait, using it to write recursive programs? that means that we have a (Nat -> Set) at value-time 19:36:19 why would such a function be useful at value-time? 19:36:38 hmm... the f 0 argument should be implicit, but should the inductive step be? 19:37:17 MissPiggy: so what value does natInduction have to be a recursive control structure? 19:37:54 -!- oklofok has quit (Quit: ( www.nnscript.com :: NoNameScript 4.2 :: www.regroup-esports.com )). 19:38:32 I mean 19:38:33 natInduction : (f:Nat→Bool) → f 0 → (∀(n:Nat), f n → f (succ n)) → (∀(n:Nat), f n) 19:38:36 should be 19:38:39 natInduction : (f:Nat→Bool) → f 0 → (∀(n:Nat), f n → f (succ n)) → (∀(n:Nat), f n) -> forall n, f n 19:38:53 oh 19:38:55 natInduction : (f:Nat→Bool) → f 0 → (∀(n:Nat), f n → f (succ n)) → (∀(n:Nat)) -> forall n, f n 19:38:57 ...lol 19:39:02 (∀(n:Nat), f n) -> forall n, f n 19:39:12 oh nevermind, now I see it 19:39:13 (∀(n:Nat), f n) -> ∀n, f n 19:39:16 (∀(n:Nat), f n) -> ∀(n:Nat), f n 19:39:21 i have that :) 19:39:38 if you could see how awful these unicode symbols look you might forgive me 19:40:59 :) 19:41:06 natInduction : (f : Nat → Set) → f 0 → (∀(n:Nat). f n → f (succ n)) → (∀(n:Nat). f n) 19:41:06 natInduction _ base _ 0 = base 19:41:06 natInduction f base induct n = induct (natInduction f base induct (pred n)) 19:41:10 if I'm not mistaken 19:41:18 but I think ->Set doesn't make it nicer to use for recursion 19:43:39 -!- sshc_ has quit (Ping timeout: 252 seconds). 19:46:06 MissPiggy: am I correct? 19:53:42 lol I felt the urge just now for something even more general than typeclass instances 19:53:54 instance (tc a) => tc (Foo a) 19:54:28 woah what is going on there 19:54:34 that's weird 19:56:29 well for instance 19:56:35 instance (tc a) => tc (Partial a) 19:56:37 well 19:56:42 you need to morph the return values into Partial too 19:56:43 lol 19:56:46 poll time 19:56:47 newtype Stream a = Partial (a, Stream a) 19:56:47 or 19:56:53 erm 19:56:54 *type 19:56:59 type Stream a = Partial (a, Stream a) 19:57:00 or 19:57:06 type Stream a = (a, Partial (Stream a)) 19:57:54 I guess I prefer the former because you can return Stream a 19:57:56 rather than Partial a 19:58:04 hd :: Stream a -> Partial a 19:58:04 tl :: Stream a -> Stream a 19:58:11 the co-ness of streams is embedded in the stream itself 19:58:31 ofc you need a newtype irl 20:00:37 i was hoping MissPiggy would pop up with some semantic reason for preferring one or the other there :P 20:01:00 ah! 20:01:03 newtype Stream a = Stream a (Partial (Stream a)) is actually preferable 20:01:08 so you can do foo <- tl somestream 20:02:33 -!- sshc has joined. 20:02:35 oh 20:02:37 -!- lament has quit (Ping timeout: 264 seconds). 20:02:38 newtype Stream a = Stream (Partial (a,Stream a)) 20:02:40 gives you all those properties 20:02:44 hey wait, isn't that a case of Mu? 20:06:48 -!- sshc has quit (Ping timeout: 240 seconds). 20:07:19 -!- sshc has joined. 20:07:22 -!- lament has joined. 20:07:54 f x = Partial (a, x) 20:07:56 I guess 20:08:26 newtype Stream a = Stream (Partial (a,Stream a)) deriving (Show) 20:08:26 con :: a -> Stream a -> Partial (Stream a) 20:08:27 con x xss = return $ Stream (return (x,xss)) 20:08:27 rep :: a -> Partial (Stream a) 20:08:27 rep x = do 20:08:27 xss <- rep x 20:08:29 con x xss 20:08:33 rep stack overflows if you try and show it :( 20:08:37 i guess partial isn't /that/ lazy 20:08:56 -!- MizardX has quit (Ping timeout: 260 seconds). 20:09:03 a bad case of the Mu 20:09:16 the Mus 20:10:36 Mus Musculus 20:11:16 MissPiggy: here, how does Coq do records? 20:11:21 i played some poker and had a bad case of the lose 20:11:22 you like Coq, you should evangelise its syntax to me 20:12:08 hey i just realised something 20:12:20 the race :: Delay a -> Delay a -> a function given in the paper that returns the one that gets to Now first 20:12:29 is basically multitasking 20:12:35 you could race proc1 proc2 in an OS 20:12:41 admittedly, not very ooh-la-la SMP, but cool 20:13:56 alise: I think records are the same as inductive types but they have named projections (and only one constructor) 20:14:26 why not race :: Delay a -> Delay a -> Delay a ? :) 20:14:37 i don't think that's how it's defined in the paper 20:14:40 they use omegarace to define lfp that's a pretty wild one 20:14:53 yes it is 20:15:19 -!- sshc has quit (Ping timeout: 246 seconds). 20:15:20 race :: Delay a -> Delay a -> Delay a 20:15:20 race (Now a) _ = Now a 20:15:20 race (Later _) (Now a) = Now a 20:15:20 race (Later d) (Later d') = Later (race d d') 20:15:28 MissPiggy: oh yeah those types 20:15:43 http://r6.ca/blog/20030729T014400Z.html 20:15:46 same general syntax as here? 20:15:55 alise the fun thing about Delay is you can define functions that are MORE LAZY than haskell 20:16:01 re delay, yes, I know 20:16:14 my issue with coq's record syntax is that it differs too much from gadt syntax :P 20:16:28 Compose : (f:Morphism)(g:Morphism)->(Range g)=(Domain f)->Morphism 20:16:28 rangeId : (a:Object)(Range (Id a))=a 20:16:31 so caps denotes constructor 20:16:38 and lowercase denotes fields on all of those constructors or sth? 20:16:48 or else how do you denote type params 20:16:49 ;| 20:16:59 no lower/upper distinction (thank goodness) 20:17:04 or else how do you denote type params 20:17:09 like in 20:17:21 Monoid = { 20:17:24 star : blah blah blah 20:17:28 assoc : blah blah blah 20:17:28 } 20:17:31 where's the actual monoid type 20:17:34 i.e. the type argument a 20:17:41 or do you have it as a separate field? 20:17:47 in which case how do you do the equivalent of (Monoid m) => ... 20:17:50 in a type sig 20:20:21 it confuses me 20:20:34 no such thing 20:20:49 (unless you use the typeclasses extension which is quite new) 20:20:55 -!- Gracenotes has joined. 20:21:05 so how do you express the same sort of thing? 20:21:16 forall a. Monoid -> a -> ... isn't allowed, the a in the Monoid might not be the same a 20:22:29 forall a, Monoid a -> a ...? 20:22:29 lol agda has postfix ⊥ for its partiality monad 20:22:37 MissPiggy: from whence "Monoid a"? 20:22:49 Coq's syntax has the things that would be parameters elsewhere as record fields 20:23:01 Record Monoid a := mkMonoid { } 20:24:42 heh, seems the agda folk name their refls type-refl 20:24:53 so ≡-refl instead of just refl 20:24:59 MissPiggy: well how boring :) 20:25:31 MissPiggy: so do you prefer "Data Foo a := { }" to the haskell/agda-esque gadt syntax? 20:25:49 I hate records :| 20:26:10 the whole idea of making a 'record' separate for some arbitrary reason just makes me want to puke my guts out 20:26:23 well in my lang it's just syntactic sugar... 20:26:40 because naming every arg in a type sig in a constructor in a data type gets a leetle bit heavy when you're just trying to fucking define monads 20:29:01 private 20:29:02 primitive 20:29:02 primTrustMe : {A : Set}{a b : A} → a ≡ b 20:29:04 Agda stdlib 20:29:06 reassuring 20:29:22 alise, what does that bit of code do? 20:29:28 yeah agda's weird 20:29:37 which bit of code? 20:29:41 MissPiggy: actually it's safe, just scarily named 20:29:42 alise, the bit you pasted 20:29:46 AnMaster: primTrustMe? 20:29:50 alise, yep 20:29:55 AnMaster, it's used internally, to do some weird stuff to do with IO and strings.. 20:29:57 AnMaster: do you know what dependent types are? 20:30:00 propositional equality? 20:30:09 if not, just don't think about it 20:30:36 alise, well, I don't know the details indeed 20:30:47 AnMaster or just ignore me and argue with elise... 20:30:52 eliser 20:30:56 :OOO 20:31:01 I just discovered the truth 20:31:02 eliser yewdcohski 20:31:07 oh no!! 20:31:11 also, yes, it is used internally like that 20:31:14 but that doesn't explain what it _is_ 20:31:29 alise, but including "TrustMe" in a identifier in any standard library is enough to make me cautious... 20:31:36 haha 20:31:41 AnMaster, it's used internally, to do some weird stuff to do with IO and strings.. <-- right 20:32:18 alise, and for a language used to prove things it seems just insane 20:32:28 well see that's because you looked at the name and not the type 20:32:33 and you can't look at the type because you don't understand the type 20:32:45 alise, sure, but the name is a bit of a wtf too, isn't it? 20:32:47 "oh no you can prove anything" is not even remotely what it does 20:32:49 AnMaster: yes, thus why i pasted it 20:33:03 but inquiry beyond that involves knowledge of the stuff used within :P 20:33:06 -!- Gracenotes has quit (Remote host closed the connection). 20:33:13 alise, and is that bit wtfy too? 20:33:44 Let me just quote a snippet of Agda's stdlib for you, and you can decide whether you really want to know more about this thing. 20:33:44 <-resp-≈ : IsEquivalence _≈_ → _≤_ Respects₂ _≈_ → _<_ Respects₂ _≈_ 20:33:45 <-resp-≈ eq ≤-resp-≈ = 20:33:45 (λ {x y' y} y'≈y x ( proj₁ ≤-resp-≈ y'≈y (proj₁ x , λ x≈y → proj₂ x ) 20:33:50 ) , 20:33:52 (That's not even the full definition.) 20:34:27 Or how about this: http://pastie.org/834543.txt?key=pja2m883ywrrb6scy3pxxg 20:35:05 alise, more or less unicode than perl6? 20:35:10 Far more. 20:35:31 Also, I am /totally/ not looking forward to having to prove my OS correct. 20:35:33 alise, must be a bit annoying to enter that sort of things. 20:35:40 /Totally/ /not/ /looking/ /forward/. 20:35:44 AnMaster: It comes with an Emacs mode that makes it easy 20:35:53 alise, tex input mode or a specific one? 20:35:58 Its own one. 20:36:01 right 20:36:17 <-resp-\~~ eq \<=-resp-\~~ = 20:36:26 alise, apart from these things I think _<_ and _≤_ looks very very ugly 20:36:38 AnMaster, it's part of the syntax.. 20:36:40 (\Gl {x y' y} y'\~~y x aesthetically I mean 20:36:42 *\to 20:36:42 you do like 20:36:44 MissPiggy, I didn't claim it wasn't 20:36:45 _<_ : A -> B -> C 20:36:48 x < y = ... 20:36:51 AnMaster: it's only because that bit of code is very ugly 20:36:51 I just said it didn't look nice 20:36:53 no just listen to me I am explaining 20:36:54 because, well, it's stdlib code 20:37:05 so that is how you define infix operators 20:37:07 actually _ for multifix is very elegant 20:37:13 if_then_else_ : Bool -> a -> a -> a 20:37:15 and you can use _<_ to denote the identifier 20:37:16 _+_ 20:37:18 _?_:_ 20:37:23 instead of having to write \x y -> x < y 20:37:24 etc 20:37:49 it still isn't aesthetically nice. which is all I claimed. I didn't say anything about the underlying concepts or whatever (I don't know of them) 20:37:58 but dude, you use underscores 20:38:00 you program IN C 20:38:07 it's only ugly in context 20:38:13 alise, well I never liked identifiers beginning or ending with _ 20:38:18 like _exit() 20:38:19 you're making a statement about aesthetics 20:38:22 based on a tiny bit of stdlib code 20:38:25 stdlib code is ugly. fact. 20:38:29 agda isn't 20:38:32 alise, well yes it often is 20:38:46 /Especially/ when you're in type theory this heavy. 20:38:58 possibly, I can't comment upon that 20:39:17 alise, but I think stdlib.i is even worse. And I read some parts of it. 20:39:31 of course that doesn't compare for various reasons 20:40:35 The cool thing about mixfix operators is that, not only can you define if/then/else and similar things as operators, you can even define parenthesising operators: 20:40:47 oh? 20:40:48 yeah it's really useful to define parens 20:40:58 <_> : a -> TotallySquareBracketed a 20:41:03 = WowItsSoSquare x 20:41:12 also, <_> has a huge problem with his eyes 20:41:18 alise, I read that as "TotallyASquareBracket" first hehe 20:41:18 MissPiggy: sarc or sinc? 20:41:22 (Sarcasm or sincere, obviously.) 20:41:30 it's angle bracket too lol 20:41:34 my ridiculous code snippet is doubly so 20:42:02 AnMaster: indeed given a good enough language, bobwas_amanwith<_a_PLA,_n(_end;_4 is a valid operator 20:42:08 because parens will just be defined as the operator (_) 20:42:10 (x) = x 20:42:18 example usage of that incredibly useful operator: 20:42:29 alise, I think I would kick any programmer who used anything like "bobwas_amanwith<_a_PLA,_n(_end;_4" in the head 20:42:38 at least if I had to ever maintain that code 20:42:49 alise, its one of the 'little things' which I would add to haskell to improvement 20:42:54 improve it 20:42:56 bobwas amazing amanwith< (boobs/42) a plastic PLA, (retard (2%-4)) n( (okaynowso okaynowso) end; woooh 4 20:43:06 of course, anyone defining such an operator is an abject idiot. 20:43:26 alise, agreed with the last comment 20:44:19 alise, so _ is basically "fill in stuff when used here"? 20:44:22 yep 20:44:36 well, in that case it is kind of neat. But around an operator it still looks rather ugly 20:44:37 it also means that type names like [a] and (a,b,c) are no longer restricted to the bourgeois language designers 20:44:44 [_] and (_,_,_) 20:44:54 but I guess you don't define such most of the time, rather you use them 20:44:59 AnMaster: yeah it's just that that's a piece of code operating on operators, which are first-class entities in agda 20:45:10 and it's a rather specific piece of code too 20:45:15 thus the crazy 20:45:26 *bourgeoisie 20:45:28 no wait 20:45:30 *bourgeois 20:45:31 alise, I don't know if having first class operators makes me puke or makes me fall in love with the language. Possibly both at once 20:45:56 alise, what did that code from the stdlib do though? 20:45:56 yes well mixfix + first class operators leads to some gnarly crappiness that MissPiggy understands and I don't apparently 20:46:06 AnMaster: I have no fucking clue! 20:46:22 alise, ah, at least we are at the same level here then ;P 20:49:27 AnMaster: 20:49:30 _=_ : a → a → Bool 20:49:31 leibniz : ∀(b:Set) (f:a→b) (x:a) (y:a). x = y → f x = f y 20:49:37 obviously the first is equality 20:49:46 take a guess at what the second is (hint: it's a property of equality) 20:49:57 after seventy-four hours (when you finally grok it) it will mow your blind 20:50:18 -!- sshc has joined. 20:50:38 AnMaster -- I already explained what it does 20:50:38 alise, where is what = actually do defined? I mean, to me it looks like it describe the types it takes and returns 20:50:50 AnMaster: yes; it's actually ... well, you can think of it as an interface 20:51:12 it's the values that must be define on a type a to make that type Unifiable 20:51:24 leibniz, obviously, depends on = already being defined beforehand 20:51:34 but read its type (logical statement) 20:51:45 note that (b:Set) can be ignored 20:51:48 it's irrelevant to the gist 20:51:51 alise, I'm trying to remember what leibniz did to figure it out :P 20:52:02 no no, just read the type aloud 20:52:02 alas the things I do remember about him doesn't seem relevant here 20:52:08 you don't need to know his name 20:52:12 leibniz : ∀(b:Set) (f:a→b) (x:a) (y:a). x = y → f x = f y 20:52:15 just ignore the (b:Set) part read the upside down a as forall 20:52:18 MissPiggy: don't explain 20:52:21 i wanna see him grok it himself 20:52:27 alise im explaining something to you :P 20:52:28 alise, I know what upside down A is 20:52:30 ... 20:52:33 MissPiggy: do it in pm 20:52:35 might be better written as 20:52:36 AnMaster: just checking >:D 20:52:39 MissPiggy: PM 20:52:40 pm plz 20:52:43 or you'll spoil it :P 20:52:49 alise, what is the x:a thing there? 20:52:56 as in, what does that part do 20:52:59 leibniz : forall (x:a) (y:a) (b:Set) (f:a→b). x = y → f x = f y 20:53:23 well that is the same as he said isn't it? 20:53:36 but doesn't it say that f(x)=f(y) if x=y? 20:54:25 -!- alise has quit (Read error: No route to host). 20:54:31 assuming → is "implies" 20:54:32 -!- alise has joined. 20:54:36 stepped on off switch 20:54:37 as in normal logic 20:54:45 MissPiggy: you explained it, didn't you 20:54:47 -!- CESSQUILINEAR has left (?). 20:54:50 alise, read logs, bbl reading iwc 20:54:51 ?? 20:55:01 i want cake 20:55:04 nope good 20:55:14 12:53:36 but doesn't it say that f(x)=f(y) if x=y? 20:55:16 yes, basically 20:55:19 anyone who defines equality 20:55:27 must provide a proof that f(x) = f(y) if x = y, by their definition 20:55:44 so you cannot define a bunk equality definition (well, apart from anything = anything being true) 20:55:56 but the thing is, it's just a normal type like = 20:55:59 there's no special "proof system" 20:56:31 -!- taxman has joined. 20:56:37 taxman, a man of much to tax 20:56:58 heyyy 20:57:02 hi 20:57:08 Hey and hi. 20:57:11 AnMaster: so basically, it's a constraint on how you can define = 20:57:18 taxman: you new i presume? 20:57:21 welcome! now sacrifice goats. 20:57:36 alise, I'm more used to thinking of = in terms of a relation on a set. 20:57:45 note: if you think, after that, that you have the wrong channel, you don't not have the right channel 20:57:56 AnMaster: Well, here, = is a function. 20:57:58 Just equals(a,b) 20:58:22 Basically, any definition of the name = for a given type must also include a definition of leibinz, which must be a proof of that statement (usually it can be inferred) 20:58:29 So it's like a constraint 20:59:10 -!- adam_d has joined. 20:59:27 also, that baffling snippet i pasted was a function manipulating relations :P 21:00:27 alise, sounds scary 21:00:37 scary, but cool 21:00:49 basically languages like this build up an entire logico-mathematical theory 21:00:58 and a proof system and a programming language based around them (that are the same) 21:01:03 and then it's your playground 21:02:20 alise, yes, but the stdlib is bound to end up quite hellish 21:02:26 in code, yes 21:02:28 in usage, beautiful 21:02:35 well yeah that is what I meant 21:02:40 what 21:02:50 why the hell would the stblib not be very simple and clear? 21:02:59 because the concepts involved are subtle and elegant 21:03:02 I'll let alise explain it 21:03:14 and the operations complex 21:03:23 hellish doesn't mean it isn't simple and clear 21:03:29 just complicated to the uninitiated 21:03:38 lol I want something like leibniz for ≈ 21:03:38 like 21:03:48 f(a) ≈ f(b) if a ≈ b 21:03:50 but that's clearly false 21:03:54 take e.g. a hash function 21:03:56 so really what we need is 21:03:56 alise, is ≈ almost equal here? 21:03:57 -!- lament has quit (Ping timeout: 252 seconds). 21:04:00 yes 21:04:13 f(a) ≈ f(b) if a ≈ b and f reacts in proportion to the change of its argument 21:04:17 alise, well hash function is a boring example. I was thinking along the lines of sin(1/x) around 0 21:04:18 and even 21:04:30 so im trying to learn about dependency syntax and how they characterize grammaticality in natural language 21:04:39 f(a) ≈withTolerance(newTolerance a b) f(b) if a ≈withTolerance(x) b and f reacts in proportion to the change of its argument 21:04:43 and one phenomena thats especially interesting to me is called an extraction island, right 21:04:49 or even 21:04:51 f(a) ≈withTolerance(newTolerance f a b) f(b) if a ≈withTolerance(x) b and f reacts in proportion to the change of its argument 21:04:56 so the new tolerance can take into account the rate of change 21:05:03 basically its that thign that makes parasitic gaps parasitic instead of just bad 21:05:17 alise, couldn't you define a class of functions where f(a) ≈ f(b) if a ≈ b is true? 21:05:26 and then somehow attach that property to them 21:05:29 yes, that's basically what I'm doing 21:05:36 except the property is on ≈ 21:05:44 i.e. if you define approx-equal, you must show that it obeys this property 21:05:44 anyway, im reading through what was probably THE textbook on the subject, Dependency Syntax by Igor Mel'čuk, which argues that DS really CAN be used as a theoretical framework for describing natural language 21:05:45 by saying 21:05:50 alise, I'm not sure what is necessary and sufficient for it 21:05:50 "f reacts in proportion to the change of its argument" 21:05:56 i'm basically conjouring up the set of functions that do that 21:06:07 alise, over the reals it must be continuous I think? 21:06:08 but this book makes no mention of extraction islands, despite being published about 20 years after they were discovered 21:06:12 hmm this may be the first time calculus was used in a type system 21:06:15 but that isn't enough 21:06:17 after countless others have written extensively on the topic 21:06:38 so i figure, yeah sure ok, maybe he was busy doing other stuff, i dont know, let me just email this guy and ask him directly 21:06:41 so i email him 21:06:54 TO THIS DAY the guy has never even HEARD of extraction islands. 21:07:03 alise, augur: your nicks are the same length 21:07:07 -!- scarf has changed nick to scarf|away. 21:07:11 and both start on a 21:07:12 AnMaster: this is true. 21:07:14 -!- scarf|away has changed nick to scarf. 21:07:17 I have problems following what is going on 21:07:18 yeah but he's annoying. and I'm not! 21:07:20 -!- scarf has changed nick to scarf|away. 21:07:20 wb scarf 21:07:23 scarf|away: bye 21:07:30 argh client issues I suspect 21:07:36 which means we will have this for some time 21:07:37 a brief stay. like life 21:07:41 until he notices it 21:07:49 AnMaster: no, he probably just returned to his terminal which set his irc client off 21:07:51 and then he fixed it 21:07:55 alise, hm maybe 21:07:56 presumably he's busy and just popped back 21:07:58 that's another possibility 21:08:07 augur: he's never heard of something so prominent? 21:08:10 the fool! 21:08:11 how the fuck can you claim that something is a viable theoretical apparatus if you dont even know about some big fucking phenomena, nevermind have an account of it 21:08:13 (in his field) 21:08:16 i dont get it 21:08:29 discontinue any interest you have in his work 21:08:37 alise, anyway what is required for f(a) ≈ f(b) if a ≈ b to hold? 21:08:56 alise, if you figure out what properties is required of the function I will be interested 21:08:57 i really should, alise. but he offered to look at some sentences and try to characterize their dependency structure 21:09:10 so ive sent him some examples to see if he has any observations to make 21:09:13 AnMaster: f(x)'s change is proportionate to x's change 21:09:26 -!- lament has joined. 21:09:28 alise, hm what about |x|? 21:09:29 apart from that, that's it, I think 21:09:51 AnMaster: yes, that's acceptable given enough tolerance in the ≈ you use for f(a)/f(b) 21:09:59 f(a) ≈withTolerance(newTolerance f a b) f(b) if a ≈withTolerance(x) b and f reacts in proportion to the change of its argument 21:09:59 so the new tolerance can take into account the rate of change 21:10:07 is, I think, the definition you need 21:10:08 plus calculus 21:10:32 hm 21:10:52 alise, what about sin(1/x) 21:11:02 I would say it isn't true around 0 21:11:16 IRSSI is being bugger... 21:11:20 bugged* 21:11:27 no news there 21:11:35 AnMaster: well it always goes in the same sort of way, right? 21:11:40 it's just that the change gets more drastic 21:12:01 all that means is that you have to make (newTolerance (\x -> sin(1/x)) a b) be a very high tolerance for small a and b 21:12:20 i think this property is so weak as to be almost useless, though 21:12:26 -!- tombom has joined. 21:12:30 -!- scarf|away has changed nick to scarf. 21:12:32 alise, you know lim_{x→0} sin(1/x) is undefined right? 21:13:10 (as well as it being undefined in the point 0) 21:13:24 (due to div by zero) 21:13:28 yes, and? 21:13:39 also sin 0 wouldn't type in my lang :P 21:13:48 alise, err? 21:13:52 sin 0 is perfectly ok 21:13:55 erm 21:13:58 I mean sin(1/0) ofc 21:14:04 well right 21:14:11 -!- oklopol has joined. 21:14:16 alise, what if the value 0 is from runtime? 21:14:22 or do you do type checking there as well 21:14:28 neither 21:14:34 this is why dependent langs are proof systems as well 21:14:43 alise, you require testing that it isn't 0 before? 21:14:49 before dividing* 21:14:51 you have to assure the language mostly the compiler can do this for you that it isn't 0 21:14:53 AnMaster: well, that's one way 21:15:29 alise, you have no exception handling or such I assume? 21:15:31 as in 21:15:37 throw/try_catch 21:15:41 or whatever 21:15:47 No reason why not, as long as throw doesn't return just "a" but "Throw a" or "IO a" or whatever 21:16:03 It's a full-blooded language, define what you want as long as it halts. If it might not or doesn't halt, put it in the partiality monad and you can still define it. 21:16:13 alise, why must it halt? 21:16:18 ah 21:16:19 I'd point you to http://strictlypositive.org/slicing-jpgs/ and http://strictlypositive.org/winging-jpgs/ to understand conditions on worlds and stuff in a dependent language, but they're kinda heavy even if you know Haskell inside out 21:16:20 right 21:16:21 now I see 21:16:28 AnMaster: because otherwise your proof for everything could be for(;;); 21:16:44 that can be any type you want, but it never yields a value and it certainly isn't a coherent proof of anything! 21:16:48 alise, I missed the bit about "partiality monad" but then it makes perfect sense 21:17:02 alise, so it will be total fp basically? 21:17:07 * AnMaster remembers reading about that 21:17:12 with data and co-data 21:17:12 also, ⊥ — our name for non-termination/error/all kinds of "non-value" — is insidious— oh, you've read the paper 21:17:16 then yes, it's total 21:17:28 just like every other dependent language that doesn't want to melt down horribly in nonsense :) 21:17:40 the language in Total FP isn't tc though iirc 21:17:48 with a partiality monad in a good dependent lang you get turing completeness 21:17:54 alise, and yes I understood the ideas of that paper. Possibly not the language used (wasn't it some custom made variation of miranda or something?) 21:18:07 a blend of miranda and haskell and stuff 21:18:09 right 21:18:11 it wasn't really a full language 21:18:12 just pseudocode 21:18:14 true 21:18:24 well I understood the ideas, that was the main thing 21:18:37 yes 21:18:43 all this stuff is pretty sexy, it's a sweet spot in programming languages 21:18:52 alise, anyway, how often would you actually need such a partiality monad? 21:18:52 because it hasn't really been explored out of the fringe 21:19:03 and just adding dependent types gives you like billions of things for free 21:19:06 didn't the paper conclude that for a lot of purposes you didn't need tc 21:19:14 it's amazingly good bang for your (admittedly large) buck 21:19:21 I think total fp is pretty daft... 21:19:27 MissPiggy: then why do you use Coq 21:19:28 it is total 21:19:36 maybe you just mean the paper 21:19:41 AnMaster: anyway the paper isn't all /that/ good 21:19:47 prolly why it was rejected 21:19:47 but 21:19:51 ah 21:19:52 the partiality monad shouldn't be needed so much 21:20:01 yes but I don't use it because it is total (I mean, it MUST be total for all the good bits to apply) 21:20:01 didn't remember that about rejection 21:20:04 you can express ackermann and all without it, you're not really very limited 21:20:16 obviously the type of the main program is, well 21:20:18 why is the input cursor now gone?? 21:20:19 argh 21:20:19 just being total for the sake of being total seems a bit pointless 21:20:20 brb 21:20:21 Partial (IO ()) 21:20:56 right restarted some stuff 21:21:13 (as opposed to left restarted, or if you prefer that: missing comma) 21:21:43 so, where were we? 21:21:57 alise, ^ 21:22:37 since I lost scrollback there 21:22:56 _/_ : ∀a, {Field a} → {Unifiable a} → {n ≠ 0} → (n:a) → a → a 21:22:58 I believe 21:22:59 AnMaster: 21:23:03 you can express ackermann and all without it, you're not really very limited 21:23:03 obviously the type of the main program is, well 21:23:04 Partial (IO ()) 21:23:11 ah missed that last line 21:23:16 because otherwise you could never evaluate a Partial expression, as obviously Partial a -> a isn't expressable 21:23:20 because the whole point is that it's non-total 21:23:22 inside that monad 21:23:25 i.e. partiality is an effect 21:23:30 alise, could you do an infinite server loop? 21:23:31 without it 21:23:40 Sure, use codata to create an infinite IO structure 21:23:48 But you'd write the core of the server detached from IO stuff. 21:23:48 right 21:23:57 Of course, if IO wasn't codata... 21:23:58 alise, well that is common practise anyway 21:23:58 Then no. 21:24:00 in all good languages 21:24:06 But the Partial contains one IO, not a stream of them. 21:24:21 So if IO is data, not codata, you... well, you could infiniloop, but only because IO is useless without it. 21:24:22 But whatever. 21:24:31 Anyway: 21:24:42 HASKELL: 21:24:47 (/) :: (Fractional a) => a -> a -> a 21:24:50 MY LANGUAGE: 21:24:53 _/_ : ∀a, {Field a} → {Unifiable a} → {n ≠ 0} → (n:a) → a → a 21:25:00 I think it's obvious which will be more popular (it's mine). 21:25:09 _/_ : ∀a, {Field a} → {Unifiable a} → {n ≠ 0} → (n:a) → a → a <-- huh? I see it says that you can't do division by zero, but where does n come from? 21:25:22 (n:a) → b means 21:25:28 n is the value of the argument at that position 21:25:34 even though we don't know the value until runtime 21:25:37 alise, looks like the wrong order to put stuff in 21:25:38 we can use it in types 21:25:38 as in 21:25:40 It's Complicated. 21:25:47 AnMaster: x : a means x is of type a 21:25:50 it is not complicated!!! 21:25:51 alise, shouldn't definition come before use 21:25:54 if you reverse it that declaration would be written as 21:25:54 that is what I meant 21:25:55 AnMaster, backwards binding 21:25:59 AnMaster: it's no declaration 21:26:03 MissPiggy, yes, that disturbs me somewhat 21:26:07 AnMaster: it's just another argument 21:26:12 {...} just means "infer the value of this argument" 21:26:20 and having all your constraints 21:26:21 like 21:26:24 a must be a Field and Unifiable 21:26:27 and n must not be 0 21:26:31 before the rest of the type, is cleaner 21:26:39 also, err, I have it the wrong way round 21:26:44 alise, but does it return of the same type as the input arguments? 21:26:46 it stops you dividing zero by something else instead X-D 21:26:48 is that really correct 21:26:57 AnMaster: Sure 21:27:03 alise, if so 2/3 would be integer division? 21:27:06 2/3 is just (2/1)/(3/1) 21:27:13 that was quick 21:27:19 taking my example so fast ;P 21:27:22 No, 2 is of type ... lemme think 21:27:30 ∀a, {Whatever a} → a 21:27:37 alise, err? 21:27:40 Yes it totally will be called Whatever, shut up 21:27:51 alise, I don't get it. what does whatever do there 21:27:51 x/y is only defined if we have a proof of y [#] 0. 21:27:57 Definition cf_div (F : CField) (x y : F) y_ : F := x[*]f_rcpcl y y_. 21:28:00 AnMaster: well, 2 = succ (succ 0), so wherever succ is, that's what whatever will be 21:28:10 MissPiggy, what about limits then? 21:28:12 Record CField : Type := 21:28:12 {cf_crr :> CRing; 21:28:12 cf_rcpcl : forall x : cf_crr, x [#] 0 -> cf_crr; 21:28:14 ... 21:28:31 [#] means 'apart' i.e. not equal but more constructive 21:28:45 constructive my ass 21:28:46 http://c-corn.cs.ru.nl/documentation/toc.html 21:28:52 nothing wrong with a good refly frolick 21:29:10 it is more constructive to prove things are apart that prove the negation of equality 21:29:21 define apart? 21:29:32 it would have a different definition for each sort of type 21:29:39 but there are some axioms for it 21:29:51 it will be cool to model classical logic in my type system and then prove that clasically, p or not p 21:29:53 AnMaster: well, 2 = succ (succ 0), so wherever succ is, that's what whatever will be <-- since oerjan seems to be inactive: "that succs" 21:29:53 *classically 21:29:57 really cool 21:30:35 hey, where are the groans? 21:31:33 MissPiggy: hey do we have the axiom of choice for types? 21:31:34 that would be fun 21:31:38 i guess so 21:31:53 also I still don't get what apartness is :) 21:32:02 why is that axiom considered somewhat problematic btw? 21:32:02 also it kinda sucks to have a different operation for what's essentially the opposite of another op :( 21:32:09 apartness it a constructive proof that things are not equal 21:32:19 so it has more information in it than simply ~ x = y 21:32:23 I know why it is required, but I don't know why it seems to be avoided 21:32:27 AnMaster: http://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox 21:32:46 russell o'connor had a nice post about the AoC 21:32:48 lemme find it 21:33:04 alise, ah that, I think iwc did a huge annotation on it 21:33:16 during mythbuster theme 21:33:29 the strip was about needing 5 not 4 sections or such iirc 21:33:44 http://r6.ca/blog/20050604T143800Z.html 21:34:00 the Axiom of Choice has two parts basically 21:34:04 and one is uber smexy 21:34:26 i'm not inactive. just backlogged. 21:34:41 MissPiggy will hate it because it gets rid of quotient types apparently :D 21:37:33 -!- cheater2 has joined. 21:38:05 I like how he links to a proof of the axiom of choice, too 21:38:10 in Coq 21:38:11 "DON'T DOUBT ME, BITCH" 21:38:54 -!- cheater4 has quit (Ping timeout: 245 seconds). 21:39:08 in Coq <-- as a data: url too! 21:39:19 it seems 21:39:22 if it is the first one 21:39:31 * MissPiggy <3 data urls 21:39:31 yep 21:39:34 sooooooooooooo much 21:39:41 MissPiggy, seems a bit strange for this case 21:39:58 he does it a lot to basically do "footnotes"w 21:40:00 *"footnotes" 21:40:04 well, at least twice in his blog 21:40:33 imagine if we all were using turing machines. Every link would be a data: uri plus quining. 21:41:18 So if we define that %!! means "this entire data URI", escapable by the usual means (i.e. using %), then every link would contain not only the contents of the page it links to, but the contents of the pages that page links to, etc, only using quining when a link back to the page linked to is encountered. 21:41:27 oh, %?? would be "this page", to avoid more quining issues 21:41:43 so every time you link to a page you store a complete snapshot of the web :) 21:42:00 well 21:42:04 the web reachable from the page you link to 21:42:07 which is probably an awful lot 21:42:28 alise, hm the bandwidth :D 21:42:45 Infinite, naturally. 21:43:03 alise, and 0 latency? 21:43:20 Latency is irrelevant so long as it is under, say, a few days. 21:43:31 I should make an effort to understand that proof :| 21:43:37 the banach tarski paradox is not a paradox, grrrr 21:43:40 alise, why? 21:43:40 (the external link) 21:43:41 After all, loading the Google homepage (which would contain all the possible results and the algorithm for looking up the results) would download most of the web that matters. 21:43:56 So it'd be a one-time cost apart from really obscure stuff. 21:44:04 Because remember, the possible results include the links to pages there, etc. 21:44:12 alise, err, what about checking weather for tomorrow 21:44:16 So basically, caching the Google page caches every page on Google or reachable from a page on Google. 21:44:21 it would be annoying if you got that page only 2 days after 21:44:22 :P 21:44:30 AnMaster: Well, obviously, the web is immutable like this; we'd need some special service for pushing us updates to certain pages. 21:44:40 Presumably by creating new pages, since there is no "page identifier" other than the page itself. 21:45:01 sure 21:45:05 Admittedly the latency would have to be non-ridiculous for that. 21:45:11 yep 21:45:46 alise, why not create all possible web pages instead? 21:46:06 (I suspect this is non-computable and/or uncountable) 21:46:26 3 times he's used link-footnotes on his blog 21:46:32 AnMaster: Uh, it's countable. 21:46:41 alise, they could have any length 21:46:45 A string is isomorphic to a natural number. 21:46:49 and link to any other 21:47:07 0 = "", 1 = "\0", 2 = "\1", ..., 255 = "\255", 256 = "\0\0", 257 = "\0\1", ... 21:47:13 so the entire web would be a set of infinitly long strings 21:47:15 no? 21:47:25 and thus there would always be one in between 21:47:30 Uhh... 21:47:37 http://r6.ca/blog/20040616T005300Z.html another good post 21:47:41 alise, thus we basically have cantor's diagonally thingy 21:47:49 err not that one 21:47:57 the one that proves you can't count the reals 21:47:59 cantorsDiagonallyThingy : ... 21:48:00 -!- scarf has changed nick to scarf|away. 21:48:05 -!- scarf|away has changed nick to scarf. 21:48:13 oh yeah it's the diagonal one 21:48:28 I was confusing it with the one that proved you *could* count the rationals 21:49:25 ALL THIS STUFF IS SO FUCKING INTERESTING! FUCKING FUCK FUCKSHI!!!! 21:49:27 *FUCKSHIT 21:49:36 I am not being sarcastic 21:49:38 fuck yes 21:49:41 anyway I maintain that the set of all possible pages including all possible linked pages as data urls is uncountable 21:50:03 due to what I described above 21:50:09 Perhaps. 21:50:48 alise, basically we could always insert a page that sorts in between two given ones 21:50:58 god modelling classical logic in constructivist logic will be awesomely awesome 21:51:12 the set of all possible finite pages is obviously countable 21:51:59 subst : {A : Set}(C : A → Set){x y : A} → x == y → C x → C y 21:52:00 hmm 21:52:02 oklopol, well, you could always insert one that sorts in between, couldn't you? it would still be finite 21:52:07 this is equiv to f(x) = f(y) if x = y isn't it 21:52:10 but slightly longer than those 21:52:11 except more constructivismism 21:52:14 (misspiggy?) 21:52:19 one that sorts? 21:52:52 alise prove symmetry (i.e. x = y -> y = x) using subst 21:53:19 you can't do that with f(x) = f(y) if x = y either can you 21:53:23 or do you mean subst is greater than that? 21:53:32 oklopol, anyway describe the proof for why " the set of all possible finite pages is obviously countable" 21:53:57 it isn't obvious to me, in fact it looks like the reverse 21:54:02 with f(x) = f(y) if x = y, it's `equals(y,x) = equals(y,y) if x = y` 21:54:10 AnMaster: base 257 numbers 21:54:13 since equals(y,y) is true, equals(y,x) must be true 21:54:19 since that's y = x, we have shown that y = x if x = y 21:54:25 that doesn't look possible with subst 21:54:34 MissPiggy: so leibniz's law is greater, then, I assume 21:54:35 oklopol, 257? 21:54:43 wait no 21:54:44 subst IS liebniz 21:54:48 let C be - yeah 21:54:58 AnMaster: yeah so you don't get the problem of initial zeroes 21:55:11 MissPiggy: it's just that i would have written it as C x = C y 21:55:15 rather than implying both 21:55:17 mine seems to be more general 21:55:26 C doesn't have to return Set, just something equalisibleirel 21:55:34 they're equivalent but still 21:55:38 I'm just wondering which is "better" 21:55:41 oklopol, you can't sort them based on bytes from the start in a well defined order though. Hm you are right 21:56:43 I was like anchoring them at the start rather than placing them in numerical order (strcmp() as opposed to < or > on bignums basically) 21:57:04 MissPiggy: well this is the most irritating dilemma ever 21:57:11 -!- taxman has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.7/20091221164558]). 21:57:16 oklopol, but remember they do contain all linked pages as data uris 21:57:19 alise state them both 21:57:25 hm doesn't change things 21:57:44 -!- tombom_ has joined. 21:57:55 MissPiggy: but they're identical 21:58:24 AnMaster: well are they still finite? 21:58:25 state them :[ 21:58:34 the pages + data uri lists 21:58:48 12:49:31 leibniz : ∀(b:Set) (f:a→b) (x:a) (y:a). x = y → f x = f y 21:58:48 12:52:12 leibniz : ∀(b:Set) (f:a→b) (x:a) (y:a). x = y → f x = f y 21:58:52 how do these two differ 21:58:59 o_o 21:59:04 oklopol, possibly it links to something that include everything else. But I think alise said that should be represented as "same page" to handle the loops 21:59:05 sorry, tunes fucked up the unicode 21:59:13 thus they would be finite I think 21:59:19 alise no no no 21:59:21 so there are infinite pages? 21:59:21 if they were to include themselves literally 21:59:23 of course not 21:59:27 MissPiggy: ??? 21:59:28 oklopol, err what? 21:59:29 talking to you is so confusing 21:59:36 "AnMaster: oklopol, possibly it links to something that include everything else." 21:59:52 oklopol, "But I think alise said that should be represented as "same page" to handle the loops" 21:59:56 oklopol, on the same line 21:59:59 as in 22:00:01 alise I meant to say put x and y before everything else, for partial application 22:00:03 you use an escape 22:00:08 ah 22:00:11 to indicate it links to the page it is in 22:00:17 still 22:00:18 wait 22:00:21 that wouldn't work alise 22:00:27 why nawt? 22:00:29 oh AnMaster 22:00:32 thought you were MissPiggy 22:00:36 i.e. talking about non-boring things 22:00:38 -!- tombom has quit (Ping timeout: 265 seconds). 22:00:45 alise, you could have loops of pages that aren't using the top page 22:00:54 yes which is why in a data: uri you have %!! 22:00:55 to mean "this uri" 22:00:56 thus couldn't indicate "this page" 22:01:05 %?? means this page, i.e. the page containing the link to that uri 22:01:05 subst : ∀(x:a) (y:a) (f:a→Set), x ≡ y → f x → f y 22:01:05 leibniz : ∀(x:a) (y:a) (b:Set) (f:a→b), x ≡ y → f x ≡ f y 22:01:08 MissPiggy: stated. 22:01:11 it might be nested hm 22:01:26 obviously they both are equivalent; leibniz is more lenient/general, except not 22:01:28 AnMaster: what the fuck does it matter what it links to 22:01:33 no wait it is 22:01:34 yeah 22:01:38 hmm 22:01:47 subst may be "easier" to prove because it does not involve f x ≡ f y 22:01:48 oklopol, if it was to literally include the whole page recursively you would get infinite pages 22:01:53 which could be very iffy for arbitrary f 22:01:56 that was my point 22:02:05 MissPiggy: whereas f x → f y intuitively seems easier to prove, no? 22:02:11 in fact 22:02:39 a page would then contain infinite data urls in the middle 22:02:44 (possibly) 22:02:53 AnMaster: yes, good point, if there are infinite pages, then my argument about finite pages doesn't apply. 22:03:04 oklopol, is it still countable though? 22:03:07 I doubt it 22:03:08 oklopol: you're so sarcastic :) 22:03:28 MissPiggy: well this is some thrilling conversation here :P 22:06:52 AnMaster: if you have infinite pages, then there can obviously be uncountably many 22:07:01 f:a→Set is better 22:07:15 and it should be called leibniz, whereas f:a -> b should be called subst 22:07:33 oklopol, indeed 22:07:50 MissPiggy: why is f:a->Set better? 22:08:10 also, I'm only going to define one; the other can be inferred from it with no code, I believe 22:08:15 wait, no 22:08:42 f x → f y means "you can transform a value of type (the result of (f x)) into a value of type (the result of (f y))" 22:08:49 which _doesn't_ mean that f x and f y are the same 22:08:54 alise, try and prove them both 22:08:57 wait, yes it does, since f can be any such function 22:09:09 MissPiggy: heh ok, i'm a bit of a proof retard though 22:09:10 it will only go one direction 22:09:20 i hope you don't mean a checked proof :( 22:09:26 of course I do! 22:09:30 i only know the programming side of /existing/ dependent languages though! 22:09:40 nah it doesn't matter if it's checked 22:10:42 * MissPiggy needs to read On Denoting at some point 22:12:55 heh i think i may be retarded, proving ∀(x:a) (y:a) (b:Set) (f:a→b), x ≡ y → f x ≡ f y is causing my brain to go ⊥ 22:13:08 i'm either intelligent or really stupid never in-between 22:13:22 well 22:13:26 refl : {x:a} → x ≡ x 22:14:21 heh i think i may be retarded, proving ∀(x:a) (y:a) (b:Set) (f:a→b), x ≡ y → f x ≡ f y is causing my brain to go ⊥ <-- what axioms do you have available for this? 22:14:33 your standard dependently-typed constructivist type theory 22:15:14 alise, I don't know what those are. But the proof is trivial for pure functions over a set with the = operator 22:15:24 i'm proving it from 22:15:25 data _≡_ : {a:Set} → a → a → Set where 22:15:25 refl : {x:a} → x ≡ x 22:15:28 refl (f x) : f x = f x 22:15:28 as in, it follows from definition of ? 22:15:30 err 22:15:31 of = 22:15:46 so how can you turn f x = f x into f x = f y :P 22:15:55 (using "subst" which should actually be called leibniz) 22:15:56 if x = y then they are identifical 22:16:04 identical* 22:16:09 MissPiggy: yeah exactly 22:16:16 hmm so wait 22:16:36 the proof of leibniz (which should be call subst, the f(x)=f(y) version) involves subst (the f(x)->f(y) version)? 22:16:45 if so, then I /definitely/ want subst, as it is "more fundamental" in a sense 22:16:46 MissPiggy, thus it follows that you can write x as y. and thus f x = f y can be rewritten to f y = f y 22:16:59 MissPiggy, seems pretty trivial to me 22:17:04 well basically I need to prove that if the normal forms of two values are equal they're indistinguishable 22:17:10 i don't think that's axiomatic though 22:17:33 alise, sounds like the same as what I did basically? 22:17:40 well 22:17:42 no. 22:17:44 I took it axiomatic rather 22:17:59 well that's trivial then 22:18:11 alise, but I thought that was by definition so 22:18:35 http://pastie.org/834672.txt?key=ehlammleckrtzlp63rlxsw 22:18:44 I don't think MissPiggy would give me such a trivial task, though. 22:19:04 actually that desugaring isn't quite right, it's {} in the foralled things 22:19:05 but that's equivalent 22:19:23 the proof of leibniz (which should be call subst, the f(x)=f(y) version) involves subst (the f(x)->f(y) version)? 22:19:23 if so, then I /definitely/ want subst, as it is "more fundamental" in a sense 22:19:25 MissPiggy: 22:19:40 alise that paste is not right 22:19:49 yeah i know 22:19:53 I was just playing by AnMaster's rules 22:19:59 or do you mean i made an actual error 22:20:02 in which case my brain really is off today 22:20:11 wel you just repeated the question then went QED 22:20:12 :D 22:20:12 alise, well without that axiom I'm quite confused as how to prove it 22:20:20 MissPiggy: exactly 22:20:23 AnMaster: duh that's why it's hard 22:20:39 AnMaster: you have to prove that (f x ≡ f y) → ⊥ 22:20:47 i.e. it is impossible to construct a value of type (f x ≡ f y) 22:20:51 alise, exactly, but I wasn't aware of that it was not considered axiom/definition 22:20:57 I was responding to 22:20:57 alise, well without that axiom I'm quite confused as how to prove it 22:21:09 anyway MissPiggy i don't want to prove it i want you to answer my question :) 22:21:11 the proof of leibniz (which should be call subst, the f(x)=f(y) version) involves subst (the f(x)->f(y) version)? 22:21:11 if so, then I /definitely/ want subst, as it is "more fundamental" in a sense 22:21:11 :P 22:24:23 * alise whacks MissPiggy 22:24:39 hey I am writing something for you 22:24:42 stop attacking me! 22:24:44 oh okay 22:24:52 i was just making scientific inqierie 22:24:54 alise, possible answer (but certainly incorrect): "because it is call by value" 22:24:55 lol 22:25:03 AnMaster: that still isn't a proof 22:25:10 you don't understand what a proof is :) 22:25:11 alise, I said it was incorrect duh 22:25:16 alise, it was a joke 22:25:20 even if it was call by value 22:25:22 it wouldn't be a proof 22:25:23 http://pastie.org/834684.txt 22:25:34 alise, exactly. all math is 22:25:40 well 22:25:42 almost all 22:25:42 alise a proof is a term in the language! which will typecheck 22:25:44 all math is what? 22:25:48 call by value? bullshit 22:25:53 MissPiggy: i know _that_ 22:26:14 alise, I did correct it... 22:26:15 okay, so leibniz > subst 22:26:28 wait MissPiggy you're giving me homework! 22:26:30 >:| 22:26:32 yes :P 22:26:40 anyway i have no dependent language installed so i can't prove it 22:26:40 nyah 22:26:51 you are not supposed to use a type theory just do it by hand 22:26:58 okay lamer :P 22:27:10 ugh i have to rewrite your fucking lame syntax in sane syntax :| 22:27:17 maybe I'll refuse to 22:27:23 also, why P instead of p 22:27:26 it's a variable 22:27:27 well I want to see how you rewrite it because I don'\t know what's bad about that syntax 22:27:34 there is no lower/uppercase distinction 22:27:37 (which is a good thing) 22:27:47 yes 22:27:49 but convention 22:27:56 also you can't use (T:*); this is /inside/ Unifiable 22:28:01 er wait no 22:28:08 er wait yes 22:28:12 i've been using \equiv all along lol 22:28:13 when I really mean = 22:28:31 MissPiggy: I cannot prove what you put there; = is in Unifiable and is defined by the implementer. The proof will differ for each type. 22:28:41 Do you mean for Unifiable, i.e. ≡? 22:28:54 i.e. the refl thing 22:28:55 erm 22:28:57 Do you mean for not Unifiable, i.e. ≡? 22:29:00 -!- augur has quit (Read error: Connection reset by peer). 22:29:01 alise, you can replace = with any 2-ary relation, the definition doesn't matter 22:29:02 I assume you do, otherwise I cannot help 22:29:06 MissPiggy: can't 22:29:13 because the proof differs for each definition of = in Unifiable 22:29:18 no it doesn't 22:29:20 so I'll assume equiv 22:29:23 MissPiggy: yes, it does 22:29:25 :| 22:29:30 because the definition of = differs 22:29:33 -!- augur has joined. 22:29:34 the proof using = must differ too 22:30:29 anyway do you want \equiv i.e. same normal form 22:30:37 or = i.e. defined depending on the type 22:30:46 (since we have unifiable = (t,=,leibniz)) 22:30:51 choose 22:31:15 alise, listen to me :( 22:31:23 If the former is acceptable I would prefer it, for I do not need to include records in the type. 22:31:26 Is the former acceptable? 22:31:27 Yes or no. 22:31:27 if you replace all occurecense of x = y with R x y 22:31:30 Yes, I know. 22:31:32 and f x = f y with R (f x) (f y) 22:31:32 Is the former acceptable? 22:31:35 then you can still do the proof 22:31:38 Is the former acceptable? 22:31:52 geez you really dont understand what 'listen to me' means 22:31:55 I do. 22:32:04 And I understand what you said. 22:32:15 However, I will continue to ask the question until I am absolutely certain what I am going to do what you want. 22:32:25 what question 22:32:36 leibniz : ∀(a:*) (x:a) (y:a), (p:a→*) → x ≡ y → p x → p y 22:32:39 where 22:32:41 data _≡_ : {a:Set} → a → a → Set where 22:32:41 refl : {x:a} → x ≡ x 22:32:52 Now, I am not proving leibniz; correct? I am proving leibniz implies subst. 22:32:59 yes 22:33:00 Is this, then, acceptable? 22:33:00 "leibniz impiles subst (prove this)" 22:33:01 MissPiggy, but does that really hold for any R? 22:33:03 Good 22:33:07 MissPiggy, and any function? 22:33:36 any relation R which has reflexivity 22:33:43 ah 22:34:55 MissPiggy, but if we set R to be =< and define f x to be a hash function it doesn't seem to hold 22:35:07 and =< is reflexive 22:35:20 "it doesn't hold"? what is it? 22:35:54 that x =< y implies md5(x) =< md5(y) for example 22:36:08 MissPiggy, since =< *is* reflexive 22:36:22 AnMaster, forget about proving subst or proving liebniz, 22:36:32 we are thinking about proving subst -> leibniz, or leibniz -> subst 22:36:41 MissPiggy, hm right 22:37:10 you are right that with R as =< it you can't construct subst, but that is not really an issue 22:37:46 MissPiggy, so you need more than just reflexive. I think you need symmetric too 22:37:53 probably transitive as well 22:37:54 what's the tex for the or symbol again? 22:38:14 alise, \cup ? 22:38:18 AnMaster: you can prove symmetry and transitivity from leibniz! 22:38:20 thanks 22:38:42 or maybe it is \vee 22:38:43 forgot 22:38:56 MissPiggy, hm okay 22:41:48 MissPiggy: lol well I thought I'd proved it 22:41:52 but I'd actually proved 22:41:53 ∀(a:*) (x:a) (y:a) (b:*) (f:a→b), 22:41:53 x ≡ y → (f y ≡ f x) → (f x ≡ f y) 22:42:00 sec, I believe I have the basic technique right 22:42:30 alise yes! 22:42:38 yes what? 22:42:39 oh wait 22:42:40 no! 22:42:41 sorry 22:42:42 indeed :P 22:42:46 I thought you did it too 22:42:50 alise, you proved commutativity of equal :D 22:42:53 i'm close though 22:42:54 or what? 22:42:57 AnMaster: not equality; equivalence 22:43:00 right 22:43:07 given ∀(a:*) (x:a) (y:a) (p:a→*), x ≡ y → p x → p y 22:43:17 lol you know 22:43:20 I've had a journey with equality 22:43:30 first I used shitty languages that only had one or two equality operators and shit sucked 22:43:48 eh 22:43:51 then I used Scheme; it had a multitude of equality operators defining every type of equality given mutable pointers 22:43:57 and I thought dayum, this language sum rigorous bitch 22:44:10 then I used Haskell: lo, for it only had one equality, by removing that hideous wretch of mutability and pointers. 22:44:14 oh I get what you are talking about now 22:44:24 And I thought: lo, this bitch did remove sum complexity with it's purity; dayum. 22:44:45 Now, I use dependent languages; they have every type of mathematical equality, equivalence under reduction, and ponies. 22:45:00 And I think: Dayum, I sure am glad I'm messing with this instead of doing actual real work. 22:45:05 alise, yeah all those equal variants in scheme annoyed me 22:45:06 as in 22:45:12 I could never remember which one I wanted 22:45:14 haha 22:45:24 *its purity 22:45:28 (after haskell line) 22:45:46 okay so what i need to do is basically give a suitable p 22:45:59 -!- augur_ has joined. 22:46:02 so that (p x -> p y) means the same thing as (f x === f y) 22:46:21 well i can't connect the xs and ys on each side, so i will have to do it for both x and y redundantly 22:46:32 however, p x must not be the actual statement that f x ≡ f y 22:46:36 -!- augur has quit (Read error: Connection reset by peer). 22:46:37 otherwise, I have merely a tautology 22:47:04 got it 22:47:09 MissPiggy: will this be on the exam? 22:47:15 oklopol, certainly 22:47:22 oh shit this gunna be long night 22:47:27 sleep -> 22:47:58 MissPiggy, what exam? 22:48:10 oh wait it was a joke right? 22:48:14 anyway, night too 22:48:57 MissPiggy: http://pastie.org/834705.txt?key=3zp9sv7t9v12drxuyy7ow I have proved that leibniz implies subst. 22:49:16 I now must show why ~(subst -> leibniz), correct? After you make sure my proof is correct. Miss P. 22:49:24 no 22:49:30 don't prove ~(subst -> leibniz) 22:49:36 Probably I made some trivial error as I often do. 22:49:37 just explain why subst doesn't imply leibniz 22:49:38 MissPiggy: not prove; just explain why 22:49:42 lol 22:49:44 yes 22:49:49 ut yeah, check http://pastie.org/834705.txt?key=3zp9sv7t9v12drxuyy7ow is to your satisfaction 22:50:19 True/False are assumed to be of type *, 22:50:20 and we are assumed to have ∩ doing the obvious thing on True 22:50:20 and False. 22:50:23 this is not needed in the actual proof 22:50:26 just debris from a previous version 22:50:31 alise, almost.. 22:50:41 subst {a} {x} {y} {b} {f} e = leibniz {a} {x} {y} {λz → f x ≡ f z} e _ 22:50:47 shouldn't that _ be (refl (f x))? 22:51:18 MissPiggy: http://pastie.org/834705.txt?key=3zp9sv7t9v12drxuyy7ow I have proved that leibniz implies subst. <-- reminds me of Knuth's programming style somehow 22:51:22 well i read that agda implements implicit arguments as syntactic sugar by replacing them with _ 22:51:24 which is where the real magic is 22:51:31 oh 22:51:35 because _ is letting the compiler prove it 22:51:36 which is cheating 22:51:36 right? 22:52:07 well I mean why not just write subst {a} {x} {y} {b} {f} e = 22:52:07 AnMaster: How? Knuth is a literate C man. 22:52:12 subst {a} {x} {y} {b} {f} e = 22:52:14 wugh!! 22:52:15 subst {a} {x} {y} {b} {f} e = _ 22:52:17 alise, the literate bit is what I meant 22:52:18 why not just that ^ ;P 22:52:20 MissPiggy: yeah exactly 22:52:25 I get your point 22:52:34 http://pastie.org/834713.txt?key=f7bl2cjpmw9tmchuyqdw 22:52:35 Revised proof. 22:52:37 AnMaster: lol 22:52:48 yes alise this is perfect 22:52:54 * MissPiggy puts down the cane :) 22:53:40 alise, what you done there *is* literate programming it seems 22:53:45 *did 22:53:52 "What you done there" sounds... uncouth! 22:53:53 alise, youve* 22:53:57 err 22:54:04 plus ' possible 22:54:08 Whateva yoove doned there's 22:54:14 It's you've. 22:54:18 yeah 22:54:22 alise, that was the real typo 22:54:36 as in I intended to write you've 22:54:37 Anyway, it's literate programming, sort of; there's no delimiters, though, and I define subst's type twice, which isn't quite cosher. 22:54:45 But yes, it is text interspersed with code. :P 22:54:51 MissPiggy: Okay so now I have to do the reverse 22:54:55 no 22:55:00 yes i know not a proof 22:55:01 an explanation 22:55:03 blah blah blah 22:55:34 alise, an indirect proof sounds like the way to go there 22:57:32 wait, maybe not 22:57:35 MissPiggy: actually I'm not seeing it 22:57:39 So what does "p x → p y" really mean? It means that given 22:57:39 a value of type (the result of p x), we can return a 22:57:39 value of type (the result of p y). Since values with the 22:57:39 same normal form is distinguishable, this is equivalent 22:57:39 to (p x → p x), a tautology. 22:57:47 obviously p x has the same normal form as p x 22:57:55 no no 22:58:00 and that's what subst talks about 22:58:03 x = y does not mean x and y have the same normal form 22:58:05 f x having the same normal form as f y 22:58:09 MissPiggy: x === y does though 22:58:15 you /said/ equiv was acceptable 22:58:17 no 22:58:26 the two values are /the same value/ 22:58:30 so obviously they share a normal form 22:58:36 it's only when you have refl 3 = 5 typechecks.. and that is valid (but unprovable.. which is good) 22:59:10 but also you can prove (by induction) x + y = y + x 22:59:21 Oh, so I should substitute _|_ for the equivs to see why it isn't possible. 22:59:38 All that tells me is that my proof is id, because I already have a _|_. 22:59:42 I don't really see your point. 22:59:47 I am slightly thick though 23:01:00 well what I said earlier was a bit confusing 23:01:19 what I really meant was that, refl n : x = y only typechecks if x reduces to n and y reduces to n 23:01:45 of course 23:01:48 now in the closed context, everything reduces to normal form (so any proof of equality reduces to refl, hence its paramters are equal normal forms too) 23:02:07 do i have to do this homework? i did the interesting one :( 23:02:09 but in an open context it's different 23:02:13 this is just... mathematical philosophy 23:03:08 :D 23:03:24 what this is telling me is, Unifiable should include leibniz of the p x -> p y form and not subst 23:03:38 and I am grateful for that! NOW DIEEEE 23:03:53 lol if you don't complete it will not attain full marks 23:03:59 maybe later 23:04:06 alise nah we covered it 23:04:12 Also, * sucks! \star, \bigstar, Set or Type please. :P 23:04:16 I mean look, subst can only produce an equality 23:04:19 (You may choose.) 23:04:21 MissPiggy: yeah 23:04:23 but liebniz can produce _anything) 23:04:24 whereas leibniz can produce anything 23:04:25 _anything_ 23:04:26 yes 23:04:26 lol 23:04:34 subst is just a restriction of leibniz's type pretty much 23:04:36 so that's why it's stronger 23:04:38 modulo a few, really unimportant things 23:05:17 no but they are important! 23:05:29 whatevs :P 23:05:34 anyway, on to important matters 23:05:38 \star, \bigstar, Set or Type 23:05:41 lol 23:05:46 \bigstar 23:05:57 what type has \bigstar? 23:06:08 ★₁? 23:06:12 oh wow that star is ugly in this font 23:06:14 not antialiased 23:07:36 -!- madbr has joined. 23:07:47 MissPiggy: THESE ARE IMPORTANT SYNTACTIC MATTERS :P 23:08:18 every though I read your note I still don't get why it's important.. 23:08:45 it's not I'm just joking 23:08:57 syntax is important but not the name of the set of sets :) 23:09:14 Set is a bit of a misnomer though, isn't it? 23:09:19 because set theory is subverted in some places, no? 23:09:37 yeah it's kind of weird to call it set 23:09:44 or wait no, the subversion is (exists a. a) as a type 23:09:53 but i'm not sure i even have existential quantification 23:09:57 what does it even mean in a dependent language 23:11:08 MissPiggy: if it obeys set theory though what's the problem 23:12:01 but it's not a set 23:12:07 howso? 23:12:16 it's an inductively defined set if i have my set theory terminology right 23:12:21 you can interpret it as a set.. .but that's just like, your interpretation.. man 23:12:42 are you saying that because you could equally well call it ConstructiveStatement? 23:13:22 "The view from the left", paper introducing Epigram: 23:13:42 "{says that it uses \bigstar_n blah blah} These level subscripts can be managed mechanically (Harper & Pollack, 1991), so we shall freely omit them." 23:13:45 I was unaware. 23:14:21 wait, records are the same thing as modules aren't they 23:14:24 given a good record system 23:14:44 well, rather, record types = module signatures 23:14:52 inferred with modules obvs 23:16:28 -!- augur_ has quit (Ping timeout: 240 seconds). 23:18:31 -!- augur has joined. 23:24:55 -!- chickenzilla has joined. 23:25:00 hey 23:26:07 -!- augur_ has joined. 23:26:30 -!- augur has quit (Ping timeout: 268 seconds). 23:26:53 -!- BeholdMyGlory has quit (Read error: Connection reset by peer). 23:31:04 -!- BeholdMyGlory has joined. 23:32:12 -!- augur has joined. 23:35:00 -!- augur__ has joined. 23:35:04 -!- augur has quit (Read error: Connection reset by peer). 23:35:07 -!- augur_ has quit (Read error: No route to host). 23:35:15 -!- scarf has quit (Remote host closed the connection). 23:35:30 -!- MigoMipo has quit (Remote host closed the connection). 23:38:28 guh 23:38:32 I need to understand Agda's library 23:39:08 ooh, I like its syntax for forall 23:39:24 ∀{a} → b 23:39:46 ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever 23:39:46 ⊥-elim () 23:40:48 -!- tombom_ has quit (Quit: Leaving). 23:41:12 MissPiggy: there are subtle problems at every single damn level of this and they all involve advanced mathematics, what the fuck am I doing?! 23:41:17 this is INSANE! 23:41:28 I /know/ I'm not clever enough to do this 23:41:54 yes you are 23:41:54 once you have philosophy on your side it will become much easier 23:42:20 listen to this http://www.youtube.com/watch?v=q3nV6WqA4Y0 23:42:44 what do you mean by "philosophy on your side" exactly? 23:42:51 like some sort of coherent "idea" of my language that everything follows from? 23:43:05 just think about what stuff means and such 23:43:09 huh it seems that agda's solution to having one _+_ with multiple definitions is just to... rename them on import 23:43:12 unless i'm reading this wrong 23:43:15 MissPiggy: yeah i try 23:43:16 things will unify 23:43:34 MissPiggy: i'm almost certain I'm not intelligent enough to prove my language correct, though. 23:43:46 I don't have a Ph.D., I haven't studied proving such things. 23:43:48 alise oh of course you are, just implement a model in some other type theory 23:43:59 ...you know, you're right. 23:44:06 I just have to implement this in Agda or Coq or whatever and I'm done. 23:44:18 My fear there is that implementing it in Agda will show how ridiculously similar to Agda my language is. :) 23:44:30 I can't understand the proof for stuff like Coq but I know it's not a hoax :P 23:44:46 wow, gedit highlights agda as... wait for it... 23:44:47 VHDL 23:45:01 thats kind of ironic lol 23:45:06 it actually doesn't work too ridiculously badly 23:45:11 it highlights open and record 23:45:13 not data though 23:45:24 highlights String too but not most other data types :P 23:45:31 highlights comments though which is the main thing imo 23:45:43 data ℤ : Set where 23:45:43 -[1+_] : (n : ℕ) → ℤ -- -[1+ n ] stands for - (1 + n). 23:45:43 +_ : (n : ℕ) → ℤ -- + n stands for n. 23:45:47 Interesting representation. 23:46:19 did you like the song 23:46:32 which song 23:46:37 http://www.youtube.com/watch?v=q3nV6WqA4Y0 23:46:43 oh right 23:46:47 my flash is borken, guess it's time to restart ff again 23:47:05 i love you adobe. let me violate you with a rake 23:47:37 -!- augur__ has quit (Ping timeout: 264 seconds). 23:47:46 heh you can get a script that makes youtube not use flash :P 23:49:24 i know. 23:50:18 MissPiggy: also, http://www.youtube.com/watch?v=a8Dshk1XfDc 23:50:30 i love that lol 23:50:38 ditto 23:50:41 he is one completely great actor 23:51:11 god, dependent languages are so amazing 23:51:26 i should make a channel for them, in fact i just did #dependent 23:51:35 I did that :( nobody joined 23:51:42 WE CAN JOIN 23:52:59 It even has a topic! JOIN ME 23:54:26 -!- alise has quit (Quit: Leaving). 23:54:47 -!- alise has joined.