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