00:00:21 <ehird> i actually felt a brain context switch there, to programming mode
00:00:30 <ehird> sorry i'm thick right now, tilize?
00:00:43 <coppro> I just made the word up :)
00:00:50 -!- SimonRC has quit (Ping timeout: 246 seconds).
00:00:55 <coppro> I mean to take a text "image" and render it with graphical images
00:01:09 <coppro> like produce a graphical version of a Befunge program or something
00:01:41 <AnMaster> coppro, like showing code flow paths in colours?
00:02:53 <MissPiggy> <ehird> i actually felt a brain cell switch there, to programming mode
00:03:11 <ehird> umm context switch
00:03:22 <ehird> but yeah, just one cell is all my programming magic
00:03:25 <MissPiggy> that's how /I/ read (the first time)
00:03:35 -!- zzo38 has quit (Quit: Is Dungeons&Dragons turing complete? Actually, that isn't even a valid question).
00:03:45 <coppro> the basic version would just take a text and replace each character with an image
00:04:36 <ehird> i think i'm obligated to inject some ehird into the discussion
00:04:49 <coppro> that was the plan; we haven't had enough ehird lately
00:04:57 <ehird> <some statement about being apple-fanboy-forced into buying the ipad><criticise it rampantly><says that i still love it>
00:05:08 <AnMaster> <coppro> the basic version would just take a text and replace each character with an image <-- bitmap font rendering?
00:05:31 <AnMaster> ehird, oh? so you love the ipad?
00:05:38 <cpressey> I gotta say, I love it when unit tests fail when you substitute a class with a subclass of it which *overrides nothing in it*
00:05:48 <ehird> I hate it and want it to be my wife!
00:06:02 <cpressey> Anyway, I gotta go. Later folks.
00:06:03 <coppro> AnMaster: that would be the basic principle, yeah
00:06:07 <ehird> cpressey: Thank you.
00:06:12 -!- cpressey has left (?).
00:06:24 <ehird> AnMaster: Regular teenagers think they have issues with deciding on their sexuality. They should try being freedom-lovin' Apple fanboys.
00:06:38 <AnMaster> coppro, wow what a great new invention! rendering text to a graphical image. Rather than sending it to a vt100 terminal unit
00:06:54 <AnMaster> you mean, actually render in *software*?
00:07:03 <ehird> umm i'm required to inject some display nerdery into this subtopic
00:07:06 <ehird> guys, it has an IPS screen
00:07:12 <ehird> and it's so thin and light and handheld. IPS!
00:07:18 <ehird> back to more depressing things
00:07:31 * coppro knows of sexual troubles!
00:07:32 <AnMaster> ehird, but it is too large to fit into a pocket
00:07:45 <ehird> coppro: you and everyone else
00:07:55 <ehird> receive t-shirt, etc.
00:08:00 <AnMaster> unless you want: "is that an ipad in your pocket, or are you just extremely happy to see me?"
00:08:06 <coppro> I've been a member for a long while now
00:08:14 <AnMaster> but that would be, um, ridiculous
00:08:14 -!- pikhq has quit (Read error: Connection reset by peer).
00:08:22 <coppro> pretty sure I'm in a special division though
00:08:38 <Wareya> Thta's a reason I wear cargo pants
00:08:54 <ehird> wait it costs $499? why don't i have one already
00:08:58 <ehird> apart from it not being released and stuff
00:09:13 <ehird> i was expecting like, $799
00:12:29 <coppro> given that it's just a big iPhone, I'd say it's not a misprint
00:13:14 -!- SimonRC has joined.
00:14:29 -!- bsmntbombdood has joined.
00:14:55 <AnMaster> ehird, but what use case does ipad fill
00:15:37 <ehird> the "i am sitting on a bench and I want to read the new york times and check my email" case for one
00:15:59 <Wareya> it has better video hardware
00:16:22 <ehird> i'm not sure how useful the ported office suite will be though
00:16:25 <ehird> with that keyboard
00:18:15 <coppro> yeah, I don't expect that to be useful
00:18:18 <ehird> it runs a subset of iphone apps too so it's a big games console
00:18:25 <ehird> and fart sound maker
00:18:31 <coppro> too big to thumb-type, and practically impossible to touch-type
00:19:19 <ehird> i dunno, touch-typing could be practical
00:19:27 <ehird> with the error-correction
00:19:27 <coppro> I can't see it really being
00:19:33 <ehird> i can almost do it on an iphone, it's just too small
00:19:57 <coppro> because touch-typing sucks on a keyboard with no force feedback, and the angle is awkward because you have to type and view on the same surface
00:20:31 <AnMaster> <ehird> it runs a subset of iphone apps too so it's a big games console <-- not full OS X apps?!
00:20:42 <Wareya> American laptops: Full sized keyboard! Bigger keys instead of a full layout! Yay!
00:20:48 <coppro> AnMaster: I said it's a big iPhone. I wasn't kidding.
00:20:57 <ehird> AnMaster: and i said i wouldn't argue with you this weekend
00:21:04 <Wareya> it has better video hardware
00:21:20 <AnMaster> I'm just shocked at this vendor lockin
00:21:31 <AnMaster> <Wareya> American laptops: Full sized keyboard! Bigger keys instead of a full layout! Yay! <-- hm?
00:21:34 <ehird> We're playing Vendor Lockin!
00:21:41 <ehird> The game where AnMaster calls EVERYTHING vendor lockin!
00:21:43 <AnMaster> Wareya, having full sized main area?
00:22:05 <Wareya> No, the whole thing's width is that of a standard IBM-style keyboard
00:22:34 <Wareya> but it's just an enlarged version of a normal laptop keyboard
00:22:38 <AnMaster> Wareya, well my lenovo thinkpad has qwerty minus numeric keypad. the main (letter) area have keys the same size as a full sized pc keyboard
00:22:57 <AnMaster> some side keys are smaller, such as the F-keys
00:23:02 <Wareya> it's as big as a full keyboard
00:23:16 <Wareya> but it has no numpad and the arrows are squashed under shift and enter
00:23:18 <AnMaster> and the arrow keys are smaller and moved
00:23:33 <AnMaster> seems like a sane solution for a laptop
00:23:38 <Wareya> And it's the same size as a normal IBM-style desktop keyboard
00:23:46 <Wareya> yet it uses a laptop layout
00:23:58 <AnMaster> due to the lack for a keypad on the side
00:24:09 <AnMaster> so you couldn't fit keypad there
00:24:28 <AnMaster> Wareya, still it makes it easy to switch between laptop and desktop
00:24:30 <Wareya> If can fit an IBM desktop keyboard on top of this laptop's keyboard
00:24:42 <Wareya> the keys are enlarged, but it has a laptop layout
00:25:10 <AnMaster> well with the numeric keypad the desktop keyboard is wider than my laptop
00:25:27 -!- pikhq has joined.
00:25:32 <Wareya> for me they're the same
00:25:54 <Wareya> Instead of taking advantage of the space for a full kayboard layout, they squeezed in an engarged laptop layout.
00:26:12 <Wareya> I don't know measurements very well
00:26:29 <AnMaster> Wareya, becuase having the same *key size* for the letter keys is useful
00:26:47 <Wareya> -all- of this laptop's kays are super sized
00:26:57 <Wareya> super sized from an IBM keyboard's size
00:27:10 <Wareya> http://esolangs.org/wiki/User:Wareya
00:27:14 <AnMaster> ehird, you know ais -> scarf btw?
00:27:33 <ehird> yes, is that permanent? I doubt it
00:27:42 <AnMaster> ehird, seems fairly permanent so far
00:28:08 <ehird> i'm gonna move to a country where i have to wear ais523 around my neck
00:28:32 * Sgeo watches the joke woosh above AnMaster's head
00:28:43 <Sgeo> Oh, or maybe it didn't
00:29:36 <AnMaster> Sgeo, indeed, it is controlled airspace there
00:31:06 <ehird> yes, otherwise all the jokes would crash together
00:31:15 <ehird> and form some sort of horrible mutant joke of all of them combined
00:31:19 <ehird> which you would then laugh at
00:33:39 <ehird> so anyone want to come to norway with me and found an operating systems and programming languages research company
00:34:42 <ehird> the only problem is figuring out a way to be profitable!
00:35:01 <MissPiggy> is there a good version with lots of pictures??
00:35:06 <ehird> apart from that, you know, big space with lots of computers networked together... you can come into work if you want, some sort of money will probably change hands at some point
00:38:15 <Sgeo> I'm not going to sleep now!
00:38:22 <ehird> AnMaster: you're on top of sgeo
00:38:33 <ehird> congratulations, you managed to turn #esoteric to the awkwardly homoerotic once more.
00:39:46 <Sgeo> Esolangers are the only ones in that strange channel right niow
00:40:46 <ehird> Which strange channel?
00:41:20 <Sgeo> The tullinge one
00:41:33 <ehird> It's just a channel for some area of Sweden.
00:42:17 <oerjan> "tulling" means fool in norwegian. just saying.
00:43:00 <Wareya> tulling - turring, just saw that
00:44:16 <oerjan> "turring" means fool in norwegian with a ridiculous japanese accent. just saying.
00:44:26 <ehird> Luftputefartøyet mitt er fullt av ål
00:44:27 <ehird> Min svävare är full med ål
00:44:35 <ehird> Ilmatyynyalukseni on täynnä ankeriaita
00:44:38 <ehird> norweigan, swedish, finnish
00:45:38 <oerjan> swedish; it has three funny accents, the others just two
00:46:20 <ehird> swedish is not... rounded enough
00:46:31 <ehird> you can't imagine a pleasant gentleman speaking swedish
00:47:13 <oerjan> indeed. like elves, really.
00:47:32 <Gregor> Good day gentlemen, bork bork bork.
00:48:07 <oerjan> the tall, arrogant obnoxious ones.
00:48:08 <Wareya> High fantasy elves or childhood fantasy elves?
00:48:18 <oklopol> i welcome you to the pleasantness of the current moment.
00:48:56 <Wareya> I'm walking to a store half a mile a way for...
00:49:05 <Wareya> a single bag of doritos, and a 2-liter of whatever
00:49:23 <oklopol> no idea what doritos are, but they must be awesome
00:49:45 <ehird> doritos are corn crisp things
00:49:52 <Wareya> they're overprocessed, brand-name corn chips with cheese and spicing
00:49:54 <ehird> you dip them in things
00:50:09 <Wareya> I know too much about junk foor for a 130 lb teenager
00:50:35 <oerjan> Wareya: http://www.airshipentertainment.com/growfcomic.php?date=20091101
00:50:53 <Wareya> I'll read it when I get back
00:51:09 <ehird> 14, 74 lbs representin'
00:51:15 <ehird> i am light. light as a feather
00:51:21 <ehird> also really short.
00:51:33 <ehird> in fact my interior is 99% air.
00:51:45 <oklopol> i'm like two and a half yous
00:52:26 <oerjan> ehird: maybe you could escape the uk in balloon form
00:52:50 <ehird> i'd get a squeaky voice *and* escape
00:53:14 <oklopol> it's like two horses with one giant hammer
00:53:18 <oerjan> better not fart while over the north sea, though
00:54:44 -!- SimonRC has quit (Ping timeout: 246 seconds).
00:55:06 <oerjan> wait, there was another one?
00:55:30 <oklopol> i started doing this thing today where i do the french r thingie without voicing
00:55:52 <oklopol> yes, you were like "...oh dear did i make fart joke"
00:55:58 -!- pikhq has quit (Read error: Connection reset by peer).
00:56:07 <oerjan> that's essentially the german ch, isn't it
00:56:35 <oklopol> i don't think it's supposed to roll that much
00:56:56 <oklopol> at least it rolls less audibly
00:57:08 -!- pikhq has joined.
00:57:35 <oerjan> and everyone knows it's very bad for helicopters to snore
01:01:54 -!- pikhq has quit (Write error: Connection reset by peer).
01:03:23 -!- pikhq has joined.
01:04:02 -!- pikhq has quit (Write error: Connection reset by peer).
01:05:26 -!- SimonRC has joined.
01:08:37 -!- pikhq has joined.
01:09:20 -!- pikhq has quit (Read error: Connection reset by peer).
01:13:54 <oerjan> just found that "old" comic... i've been reading other comics on foglio's site for ages without realizing "What's new" _wasn't_ a link to the news section
01:14:11 -!- pikhq has joined.
01:14:17 <Wareya> My experience on the internet is like blurry tunnelvision
01:14:23 <oerjan> or so i assume, since i hadn't noticed it before
01:14:30 <Wareya> so I don't know this guy
01:14:45 -!- pikhq has quit (Read error: Connection reset by peer).
01:15:49 <oerjan> well the newer comic Girl Genius has won a good number of awards
01:18:12 <Wareya> I find it funny how it just loosely compared good/evil to roder and chaos
01:18:19 <Wareya> http://www.airshipentertainment.com/growfcomic.php?date=20091115
01:18:32 <ehird> Well, entropy is the greatest evil in the universe.
01:19:12 <Wareya> In my opinion, order/chaos and good/evil are utterly seperate scales
01:19:44 <oerjan> well duh but isn't what that comic _says_
01:20:11 <Wareya> It sounds like it's listing new names for the same things, to me.
01:20:21 <Wareya> Maybe because of my dialect, eh
01:20:39 <oerjan> and in d&d good/evil and law/chaos are the two fundamental axes
01:23:16 <oerjan> also i would say it's because we're all culturally impressed with associating good with light and law
01:23:34 <oerjan> even if we may not always agree consciously
01:23:51 <Wareya> On a really fundamental level, I guess you're right
01:24:16 <Wareya> but I do feel like that good and light are the same thing anyway, so
01:24:22 <oerjan> er, s/law/order/, or both
01:24:26 -!- pikhq has joined.
01:24:54 <oerjan> while the bat people are likely to disagree vehemently ;D
01:32:35 <oklopol> i don't really see any connection between good and light
01:33:08 <MissPiggy> maybe you have been educated evil?
01:33:21 <MissPiggy> and do not understand the four simultaneous days?
01:33:46 <oklopol> i like being in the dark, dunno why
01:33:52 <Wareya> I've played plenty of jrpgs
01:34:02 <Wareya> I think that's where good=light and evil=darkness came from
01:37:31 -!- ehird has quit (Ping timeout: 248 seconds).
01:43:10 -!- Asztal has quit (Ping timeout: 272 seconds).
01:48:50 -!- jcp has joined.
01:53:04 -!- ehird has joined.
02:01:03 <oklopol> good night everybody, may i find dreams in my sleep.
02:01:27 <ehird> Sleep, perchance to quark.
02:02:34 <Sgeo> "To sleep in Springfield, perchance to dream of being someplace else"
02:03:02 * Sgeo sees no relevent hits on Google, and points to some Simpsons book
02:05:04 <pikhq> Freaking snowstorm.
02:07:48 -!- pikhq has quit (Read error: Connection reset by peer).
02:11:45 -!- MissPiggy has quit (Quit: MissPiggy).
02:13:22 <olsner> hmm, someone pinged me >7h ago
02:13:59 <Sgeo> olsner, might have been me
02:14:08 <Sgeo> I mentioned the language you were making
02:14:17 -!- pikhq has joined.
02:14:55 <olsner> Sgeo: sweet, what were you saying?
02:15:06 <Sgeo> I was asking what happened with it, I think
02:15:10 <Sgeo> It should all be in the logs
02:16:08 <olsner> well, it's being developed, and I have an experimental implementation that should be reworked slightly to make it TC
02:16:16 <ehird> Sgeo: should i ensadden olsner too, or am i not that evil
02:16:22 -!- pikhq has quit (Read error: Connection reset by peer).
02:16:31 <olsner> and I may still decide to rebuild the middle-part of it
02:17:04 <Sgeo> ehird, *shrug* it's your life, your decision
02:17:05 <olsner> ehird: oh, ensadden me as early as possible so that I may not be worsely ensaddened in further future
02:17:44 <olsner> ehird about to die or something?
02:18:22 <ehird> I know at least one thing and it's that I'm not that bad off.
02:18:55 <ehird> If I was about to die, I couldn't be talking lightly about ensaddening people on IRC. I'm utterly terrified of death.
02:18:58 <ehird> Anyway, http://pastie.org/private/4oxpzgiywxbjobgrsa
02:19:13 <ehird> (For perspective, since I'm not sure if you know or not, I'm 14.)
02:23:30 <olsner> yah, knew you're young... your situation sounds weird and harsh, but it's how I've always suspected "mental care" works pretty much everywhere
02:23:48 <ehird> I think it's definitely better in some places.
02:23:48 <olsner> after all, it's pretty much impossible to differentiate sane persons and insane persons claiming to be sane
02:24:35 <ehird> olsner: I would be less ... whatever emotion I am about this whole situation if they were making steps to treat what they brand me with, instead of a bullshit "malnutrition"
02:24:39 <olsner> claiming to be insane? that's a sign of sanity if there ever was one :P
02:30:00 <olsner> I think these systems are (with good intentions) built to prevent either you or your parents from bailing you out
02:31:41 <ehird> Yes. But I cannot forgive the people involved.
02:31:51 <ehird> They still did these things unthinkingly.
02:33:59 <Sgeo> If they're claiming "malnutrition", they can't find a way to make sure you eat without detaining you in a place?
02:35:16 -!- pikhq has joined.
02:35:40 <ehird> They're not making sure I eat they're just giving me a drink that's woefully inappropriate; 2 x 1390 kcal + whatever else I eat in the day = one over-caloried puppy, and it's designed for people with disease-related malnutrition who *cannot* get the required amount of energy from food. And I'm not malnutritioned, I eat alright, maybe a bit less than usual. I'm just very thin, just as my father was.
02:35:51 <ehird> Runs in the family, we're both perfectly healthy, no story there.
02:36:07 <ehird> But, you know, if the junk science of BMI says I'm overweight, well howdy-doody, to hell with the facts
02:36:23 <Sgeo> I think that I could use that drink
02:36:47 <Sgeo> Even though technically I can get the required amount of energy from food, I tend not to
02:36:53 -!- pikhq has quit (Read error: Connection reset by peer).
02:37:30 * Sgeo tends not to eat properly
02:37:43 <Sgeo> I think that it would make sense for me to be in your position, tbh
02:38:22 <olsner> I suppose detaining and force-feeding is what they will ultimately resort to to make you eat, after trying various other things, if they still think you're malnutritioned
02:45:25 -!- pikhq has joined.
02:46:14 <ehird> Sgeo: no, believe me it wouldn't
02:46:18 <ehird> nobody would be helped by my position
02:46:29 <ehird> btw nutrition science is bullshit, ask Ilari if you have a lot of time :p
02:46:36 -!- pikhq has quit (Read error: Connection reset by peer).
02:46:45 <ehird> olsner: there's an anorexic girl there, 13, celebrity-obsessed, refuses to eat or drink. they just have her on a feeding tube.
02:46:56 <Sgeo> ehird, my physical body, if not my mind, might be helped
02:47:00 <Sgeo> I seriously don't eat enough
02:47:05 <ehird> they don't seem to especially care about actually fixing things, just temporary "fixes"
02:47:16 <ehird> Sgeo: maybe you just eat the wrong things. But seriously, nutrition science is crap.
02:53:51 -!- rodgort has quit (Ping timeout: 265 seconds).
02:59:40 -!- rodgort has joined.
03:11:29 -!- oerjan has quit (Quit: Good night all).
03:12:43 -!- augur has quit (Ping timeout: 256 seconds).
03:55:17 -!- Pthing has joined.
04:06:48 -!- augur has joined.
04:25:27 -!- pikhq has joined.
04:33:15 <uorygl> Neat, I started a debate: http://forums.xkcd.com/viewtopic.php?f=18&t=55981
04:35:14 * Sgeo likes the taste of pina colada on his lips
04:35:27 <pikhq> Neat, I've got Internet.
04:35:43 <uorygl> "Suppose I have a ball on a hill. The ball is tolling directly up toward the top of the hill, such that its total energy is equal to what it would be if it were at rest at the top of the hill. So, it has enough energy to get to the top, but does it actually do so in a finite amount of time?"
04:36:40 <pikhq> uorygl: No. It approaches the top asymptotically.
04:37:42 <Sgeo> That's one side of the debate
04:39:44 <pikhq> Though I'm pretty sure it depends upon the geometry of the hill...
04:40:25 <pikhq> God dammit xkcd forums.
04:40:44 <pikhq> It appears to be making Conkeror ignore all input on that window.
04:41:00 -!- sebbu has quit (Ping timeout: 245 seconds).
04:41:05 <uorygl> I'm pretty sure the infinitists are right.
04:41:23 <Sgeo> I think if chapstick had some kind of toxin that was only dangerous if a lot of chapstick was needlessly used, I'd be dead now
04:42:21 <pikhq> uorygl: I'm pretty sure there's a limit in there, so yeah...
04:43:33 -!- pikhq has quit (Read error: Connection reset by peer).
04:44:21 * Sgeo loves the taste
04:44:43 -!- MizardX has quit (Read error: Connection reset by peer).
04:44:48 -!- MizardX has joined.
04:55:17 -!- pikhq has joined.
05:00:43 -!- ehird has quit (Ping timeout: 248 seconds).
05:10:40 -!- pikhq has quit (Read error: Connection reset by peer).
05:11:46 -!- pikhq has joined.
05:27:04 -!- bsmntbombdood has quit (Remote host closed the connection).
05:51:41 -!- Gracenotes has joined.
06:32:04 -!- sebbu has joined.
06:48:44 -!- sebbu2 has joined.
06:51:39 -!- sebbu has quit (Ping timeout: 265 seconds).
06:51:39 -!- sebbu2 has changed nick to sebbu.
07:32:20 -!- bsmntbombdood has joined.
07:33:37 <Sgeo> ehird: If you see this, remind me that I have to tell you something
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:54:42 -!- kar8nga has joined.
09:04:21 -!- coppro has quit (Quit: I am leaving. You are about to explode.).
09:05:37 -!- jcp has quit (Ping timeout: 264 seconds).
09:30:56 -!- tombom has joined.
09:32:37 -!- FireFly has joined.
09:37:26 -!- MigoMipo has joined.
09:57:44 -!- bsmntbombdood has quit (Ping timeout: 265 seconds).
10:09:50 -!- bsmntbombdood has joined.
10:15:29 -!- kar8nga has quit (Remote host closed the connection).
10:23:10 -!- Bullseye has joined.
10:23:38 * Bullseye is running I-n-v-i-s-i-o-n 3.1.1 (June '09) with Advanced File Serving features by cRYOa on mIRC v6.35 32bit obtained from #Invision on irc.irchighway.net and http://www.i-n-v-i-s-i-o-n.com
10:23:56 -!- BeholdMyGlory has joined.
10:24:14 -!- Bullseye has left (?).
10:41:29 -!- Pthing has quit (Read error: Connection reset by peer).
10:42:04 <oklopol> "if there is a finite distance along the flat to the edge from the balls initial starting place, then i think you are right, an infinitely small push would take an infinite amount of time to even reach the edge, so the exact nature of the slope and the starting position may make a difference here" god these guys are retarded
10:42:36 <oklopol> also this is a slightly old conversation i'm reading, i notice
11:34:37 -!- tombom has quit (Quit: Leaving).
11:52:49 -!- verangirl has joined.
11:53:12 <AnMaster> why do I feel like writing my own irc client suddenly
12:00:36 <verangirl> look: http://identi.ca/group/conspiracy
12:00:50 -!- Pthing has joined.
12:01:05 <AnMaster> verangirl, mhm, you know this channel is about esoteric programming languages right? Not about esoterica.
12:01:20 <AnMaster> Sometimes people mistake this channel for the other thing
12:03:42 <AnMaster> esoteric programming languages being intentionally unusual, weird or silly languages. Often (but not always) designed to be hard to program in.
12:06:23 -!- SimonRC has quit (Ping timeout: 246 seconds).
12:07:04 -!- verangirl has left (?).
12:19:01 <Sgeo> Bwuh? Why did Chrome spontaneously decide to reload a bunch of tabs?
12:19:11 <Sgeo> Also, this channel isn't about esoterica? Crud. See you
12:19:14 -!- Sgeo has left (?).
12:19:22 -!- Sgeo has joined.
12:20:41 <Pthing> i wonder if there actually is a channel for magick weenies
12:51:04 -!- oerjan has joined.
13:02:03 -!- MigoMipo has quit (Remote host closed the connection).
13:07:39 -!- ehird has joined.
13:07:41 <ehird> 04:20:41 <Pthing> i wonder if there actually is a channel for magick weenies
13:07:57 <ehird> oblivious to how things work, merely trading magic incantations that appear, on the surface, to do what they desire
13:08:42 <ehird> also 23:33:37 <Sgeo> ehird: If you see this, remind me that I have to tell you something
13:15:40 -!- oerjan has quit (Quit: Later).
13:22:59 -!- MigoMipo has joined.
13:37:11 <ehird> "My own vote is clear: yes to both. Equality is reflexive (every value is equal to itself, at any longitude and temperature, no excuses and no exceptions); and the purpose of assignment is to make the value of the target equal to the value of the source. Such properties are some of the last ramparts of civilization. If they go away, what else is left?" --Bertrant Meyer
13:37:33 -!- MissPiggy has joined.
13:43:39 <ehird> MissPiggy: agda question - it's tc but total, right? how does it handle that; that partiality monad?
13:44:41 <ehird> is it not tc, then?
13:45:12 <MissPiggy> but you can express every partial function N -> N using a data type
13:45:22 <AnMaster> ehird, interesting, but what is the context?
13:45:24 <MissPiggy> or you could build a model of lambda calculus using a partiality monad
13:45:30 <ehird> in the language i spent a night babbling about - which has, as these things tend to, mutated wildly since - i'm trying to make it total, but to have partiality very ...
13:45:45 <ehird> AnMaster: http://bertrandmeyer.com/2010/02/06/reflexivity-and-other-pillars-of-civilization/
13:45:51 <ehird> (bertrand meyer = creator of Eiffel)
13:45:58 <ehird> hmm i said bertrant before
13:47:05 <MissPiggy> the function space A -> B (or forall a : A, B, or whatever) cannot express every recursive function
13:47:25 <MissPiggy> because -> is total functions (because you want to compute with them in types)
13:47:43 <MissPiggy> but e.g. A -> Computation B can be a model of lambda calculus
13:47:44 <ehird> expressing it with a data type, how do you mean? I'm curious if it's what I'm thinking of or not
13:47:57 <ehird> right, so a partiality monad
13:48:15 <MissPiggy> well you can define all the primitive recursive stuff and Mu, just as a syntax first
13:48:27 <MissPiggy> then you can give a big step semantics,
13:48:35 <ehird> right right, but what's the actual data type; i mean, it's a total language so is there sort of a backdoor where you can introduce partiality?
13:49:04 <MissPiggy> so you really are talking about the class of recursive functions now, every proof you write with respect to the semantics of that type is a valid statement about them
13:49:36 <ehird> your Computation there is a partiality monad, isn't it?
13:49:53 <ehird> so presumably to make meaningful use of them, given a haskell-style main program solution, you need main :: Partial (IO ())
13:50:08 <ehird> otherwise you'd be in total-land, and couldn't invoke the forbidden fruit of the partial lands
13:52:40 <ehird> my lambda syntax is currently λα.β because otherwise function types would get confusing :) (λα. α → ∅) vs (λα → α → ∅)
13:52:54 <ehird> (fuck yeah, unicode; i'm using unicode up the wazoo)
13:53:15 <ehird> admittedly it is rather awkward as I have *not* yet written an editor mode or editor which lets you type \a. a -> () to get that
13:54:55 <ehird> MissPiggy: come up with a nice unicode name for my () set :P
13:55:07 <MissPiggy> I wouldn't worry about writing partial programs
13:55:43 <MissPiggy> so maybe not such a valuable statement
13:55:47 <ehird> Well, considering I am planning to use this language as an entire OS, I'm sure I will run into partiality at some point - and the total FP paper certainly did show that some operations are damn awkward with total FP.
13:56:25 <MissPiggy> why do you want to write an OS with it?
13:56:32 <ehird> I dunno. I love the proof system duality and the mathematical soundness of having no ⊥,
13:56:40 <ehird> but I'm not sure totality is practical.
13:57:08 <ehird> MissPiggy: My goal in computing is to completely revolutionise it. My two separate interests are operating systems and programming languages.
13:57:19 <ehird> It is only natural that my awesome programming language would be my awesome operating system.
13:57:33 <ehird> Note "be", not "be used to write".
13:57:46 <MissPiggy> alright but you're not going to do a full correctness proof of the OS?
13:57:51 <ehird> My OS design involves the programming language being central; a living environment.
13:58:05 <ehird> MissPiggy: Yes, well. :P
13:58:07 <MissPiggy> have you talked to luqui about thsi
13:58:20 <ehird> luqui's blog was a big inspiration
13:58:26 <ehird> but i haven't caught him on irc yet
13:58:53 <ehird> heh I could use ∈ instead of ∷
13:58:55 <ehird> that's ugly though
13:59:12 <MissPiggy> the thing about \in is that it's asymmetric
13:59:34 <MissPiggy> so if you can get two symbols (one for the flipped relation)
13:59:52 * ehird wonders whether his empty type/set should be called ∅ or ⊥
14:00:04 <ehird> ⊥ would be the type theory way; ∅ the set theory way...
14:00:24 <ehird> ∅ seems less confusing; ⊥ is too associated with non-termination and undefinedness in programming
14:00:42 <ehird> then again, I'd like to be able to use ∅ to denote empty containers in value-land, and that would be doubly confusing
14:01:08 <ehird> well, whatever; apart from agda guys, haskellers are the most mathematically civilised programmers :)
14:02:28 <ehird> The joys of Unicode: /=? Why wouldn't you just write ≢?
14:03:42 <MissPiggy> I was thinking about a language that could compile into almost every high level language
14:03:52 <Sgeo> ehird, see my memo to you
14:03:56 <ehird> ≢ because you have to use ≡ for equality
14:04:01 <ehird> because = is definition
14:04:07 <ehird> MissPiggy: underlambda :P
14:04:42 <ehird> Sgeo: relink the paste in /msg; it may not be so bad
14:04:52 <ehird> I have after all linked to the pastie which tells everything in this channel
14:05:21 <ehird> MissPiggy: can you think of any way to use ≠ for equality and not be inconsistent since = is definition? maybe a better symbol for definition? :P
14:05:48 <MissPiggy> then yuo can say x = y and MEAN IT
14:06:06 <ehird> := isn't unicode bitchnizzle
14:06:57 * ehird considers that |α| instead of abs α may be taking the mathematical notation thing a *bit* too far
14:07:13 <ehird> MissPiggy: a more hideous symbol I've not seen! I wonder what font size I'm expected to use to make out "def" there.
14:07:16 <ehird> MissPiggy: yeah agreed
14:07:40 <ehird> maybe that reduction symbol that rconnor likes
14:07:51 <MissPiggy> yeah I'm not keen on the unicode stuff because all the operators are too small (unnecessarily :/)
14:07:54 <ehird> mathematical notation defines too much syntax when functions would do :/
14:08:02 <ehird> MissPiggy: yeah I'm taking care not to use any blots of ink
14:08:14 <ehird> also, _my_ OS will display it perfectly legibly ;)
14:08:27 <ehird> http://r6.ca/blog/20031202T032200Z.html
14:08:36 <ehird> →<sub>β</sub><sup>*</sup>
14:08:41 <ehird> we have our definition symbol.
14:09:08 <fizzie> ||a||₂ for the euclidean norm.
14:09:21 <ehird> I draw the line at superscript numbers for powers
14:09:39 <oklopol> fizzie: yes, the stupid symbol is used for all norms
14:10:05 <ehird> Okay, okay, so any fancy space-age editor, like my OS, will *display* it as superscripts.
14:10:17 <ehird> But in the Unicode representation?
14:10:19 <ehird> Nooooooooooooooooooooooo way
14:11:01 <ehird> (Actually I think my OS will only have to consider code as text for interacting with the outside world. Internally, it's an AST or compiled code; in the UI, it's rendered with fancy things like superscripts.
14:11:22 <fizzie> We have a maths teacher who uses sub- and superscript indices completely interchangeably, often changing them between consecutive lines. Also some sort of "middle-scripts" occasionally.
14:12:00 * ehird wonders what the best symbol for the exponentation operator is
14:13:39 -!- SimonRC has joined.
14:14:37 <ehird> maybe ↑ due to knuth :)
14:14:47 <MissPiggy> http://www.reddit.com/r/math/comments/axd4m/what_is_the_mathematical_rule_that_says_if_abc/c0jw2vc
14:15:18 <ehird> anyone who answers a question starting "What is the mathematical rule" with "common sense" is so idiotic I cannot comphrend it
14:15:54 <ehird> http://us.metamath.org/mpegif/2p2e4.html
14:16:24 <MissPiggy> hey guys I just had a great idea, lets put all our math in the computer!
14:16:55 <ehird> why don't you like metamath?
14:17:04 <MissPiggy> I do like it, it's just very funny
14:17:11 <ehird> i misinterpreted what you said
14:18:18 <ehird> foo α β = (α ≡ β) ∨ (α ≢ β)
14:18:57 <ehird> ⊕ ∷ Bool → Bool → Bool
14:19:14 <ehird> hmm ≡ is sometimes used for definition?
14:19:17 <ehird> maybe i could swap =/≡
14:19:26 <ehird> oh or ≐ is a nice unicodey thing for :=
14:19:34 <ehird> not at all ridiculous like ≝
14:19:47 <MissPiggy> like y + x = x + y, but not definitionally
14:20:49 * ehird wonders if he's crazy enough to do ÷ ∷ Boringtypeclasstypethingy → Anotherone → Maybe Yetanotherone
14:21:17 <ehird> Yesiree we have a mathematical programming language here, please ignore the endless handling of ÷'s return values behind the curtain
14:21:36 <ehird> I am crazy enough.
14:21:50 <ehird> I just need nice syntax for doing things like this in expressions.
14:22:51 <ehird> Like, say f {x} (y z {r q {x}}) → (using haskell syntax) do x' <- x; x'' <- x; r_q_x' <- r q x''; return (f x' (y z r_q_x'))
14:23:03 <ehird> given some surrounding brackets to denote that it's a special expression thingy ofc
14:23:09 <ehird> that way you could use the maybe monad
14:23:27 <ehird> MissPiggy: So, do you think ≡ is a reasonable symbol for what-Haskell-calls (to avoid ambiguity) =?
14:23:58 <ehird> for one, Maybe handling
14:24:43 <MissPiggy> "... enough to do ÷ ∷ Boringtypeclasstypethingy..."
14:25:07 <ehird> anyway, {| 2 + {3 ÷ x} |} is nicer to write than fmap (2 +) (3 ÷ x)
14:25:37 <ehird> a downside is that imperative weenies could do {| say {readLine} |} :P
14:25:49 <ehird> but i guess it's just a generalisation of >>= and =<< and <$> and blah blah blah
14:26:02 <AnMaster> ehird, Hm is ÷ fraction, integer division, floating point division or something else?
14:26:08 <ehird> yeah i suspected idiom brackets were the same thing
14:26:44 <ehird> Well, not all of "something else". You have to obey some properties, or the compiler will yell at you.
14:27:21 <ehird> Not really "of cause"; almost all languages don't do such things.
14:27:28 <ehird> You can define (/) to be pretty much whatever you want in Haskell.
14:27:42 <AnMaster> ehird, but is the result of ÷ exact or not?
14:28:07 <ehird> It depends on the definition doesn't it?
14:28:47 <AnMaster> ehird, yes indeed, which is what my first question about it tried to ascertain.
14:28:59 <ehird> I'll probably require that {| α × {β ÷ α} ≡ β |}, so...
14:29:16 <ehird> (Using ≡ as equality, though that symbol is very much in flux.)
14:29:46 <AnMaster> then it can not produce a "simple" floating point value when dividing two floating point values I think.
14:29:52 <AnMaster> though, I'm not 100% sure about that
14:30:45 <ehird> I'd relax it to {| someEqualityThingProvidedByTheDefinition (α × {β ÷ α}) β |}, but that's as good as letting you define it to anything.
14:31:05 -!- lieuwe has joined.
14:31:08 <AnMaster> >>> (3231.318478239 / 238914.12391) * 238914.12391
14:31:22 <ehird> I love how my λ is the same thing as ∀.
14:31:25 <ehird> It makes me feel warm and fuzzy.
14:31:36 <ehird> AnMaster: I might have a separate class for inexact operations.
14:32:16 <MissPiggy> so you could quotient out by "someEqualityThingProvidedByTheDefinition" and still use {| α × {β ÷ α} ≡ β |}
14:32:45 <AnMaster> ehird, iirc any floating point operation is potentially inexact. Well, almost any. x := y would be exact if both are the same type of floating point.
14:32:48 <ehird> so that allows inexact definitions but still doesn't let you define it to anything you want? How?
14:32:57 <ehird> AnMaster: Yes, I know.
14:33:22 <ehird> AnMaster: Floating-point operations don't obey the laws of arithmetic, though. :)
14:33:24 <MissPiggy> we get something like fl : R -> R defined
14:33:31 <ehird> maybe you could use Real
14:33:38 <ehird> and specify the inexact implementation as an "implementation detail"
14:33:39 <MissPiggy> and you write x + y*z would compute to fl(x + fl(x*z))
14:33:45 <AnMaster> ehird, true. So what you want is basically a CASkell?
14:33:47 <ehird> i.e., the code is considered to operate on reals in all their exactness
14:34:04 <ehird> it uses floating-point
14:34:13 <ehird> i smiled at the name.
14:35:39 <AnMaster> <ehird> and specify the inexact implementation as an "implementation detail" <-- "this implementation always round to zero. No, that isn't a typo for 'towards zero'."
14:35:45 <ehird> it occurs to me that "e" is a rather inconvenient name to give e, given the commonality of single-letter variable names...
14:36:04 <ehird> it's correct for sufficiently large values of zero
14:36:34 <ehird> i'd call e "euler", but euler has done so many mathematical things that it would be hopelessly vague :P
14:36:37 <AnMaster> hm? representing numbers as the length of a series of zeros?
14:36:57 <ehird> like if an idiot was working with the Euler–Mascheroni constant he'd be confused.
14:37:02 <ehird> AnMaster: It's a joke.
14:37:36 <MissPiggy> in a mathematical context e means exp(1)
14:37:45 <AnMaster> ehird, well, as someone in here said: it is perfectly in spirit with this channel to try to make a working thing of a joke.
14:37:52 <MissPiggy> well actually I prefer (+) for mplus
14:38:01 <ehird> MissPiggy: + for mplus would be interesting.
14:38:19 <ehird> I'm already sold on o (too lazy to unicode) = category composition
14:38:27 <ehird> which is even generaler than o = fmap, i think
14:38:48 <MissPiggy> fmap and o are quite different thuogh
14:39:06 <ehird> (.) :: cat b c -> cat a b -> cat a c
14:39:08 <ehird> --control.category
14:39:10 <AnMaster> ehird, why is e a bad name for e? I can think of at least one way to end up with that as a reasonable letter
14:39:14 <ehird> ok, that doesn't allow . = fmap
14:39:16 <ehird> but that's good i think
14:39:20 <ehird> i think you're right
14:40:09 <ehird> the supereditor will probably display α ÷ β as
14:40:42 <ehird> although at the same time I don't think I want to abandon the entirety of linear syntax
14:40:44 <ehird> it has useful properties
14:40:51 <ehird> (not necessarily textual, but linera)
14:41:11 <ehird> also, consistency is Good, and also something mathematical notation sorely lacks
14:41:29 <ehird> MissPiggy: any good ideas for the hole character in mixfix operators?
14:41:37 <ehird> I don't want to use _, it should be allowed in variable names I think
14:41:42 <AnMaster> (basically: (e^x)' = e^x, thus it is "its own derivative", and a lot of mathematicans were from Germany historically, thus that leads to "eigen" for "own/self", thus e)
14:41:49 <ehird> [14:33] <MissPiggy> and you write x + y*z would compute to fl(x + fl(x*z))
14:41:54 <AnMaster> ehird, what about that way to explain why e is a good name for e?
14:42:03 <ehird> basically the same thing as what i was saying
14:42:13 <ehird> AnMaster: yes, but in programming "e" is not an uncommon variable name
14:42:20 <ehird> so having "e" in global scope is problematic
14:42:22 <ehird> MissPiggy: I'm listening
14:42:28 <ehird> but i love mixfix so it better be a good argument :P
14:42:34 <AnMaster> ehird, you could use namespaces/module prefixes
14:42:41 <AnMaster> so you have like math:e or such
14:42:51 <ehird> AnMaster: and if you're writing mathematical code?
14:42:53 <MissPiggy> suppose you were making a type system or soemthing, and you wanted to define a function t :: T, to express that t has type T
14:42:55 <ehird> Presumably you envelop all of math.
14:43:05 <AnMaster> ehird, import it? like "from math import e"
14:43:05 <ehird> And you run into the same problem, although I guess mathematicians wouldn't name variables e because of that.
14:43:13 <MissPiggy> the type of t depends on T, so in mixfix you can't do it.. you have to write T ::' t
14:43:49 <ehird> MissPiggy: I just meant the general idea of being able to define an operation if_then_else_, not any specific definition of the semantics
14:43:52 <MissPiggy> mixfix operators being typed is the problem really
14:44:07 <MissPiggy> yeah if you just make them notations, rather than well typed terms I think it's better
14:44:19 <ehird> I didn't know they were terms in Agda or whatever
14:44:23 <ehird> if they are I don't see why
14:44:41 <MissPiggy> welll when you compute it will print back the mixfix terms
14:44:53 <MissPiggy> rather than something horrid like Ap (Ap (Dollar ..) (Ap ..
14:45:03 <ehird> so it's basically prettyprinting?
14:45:14 <MissPiggy> if they are just notations then it's a bit harder to make the link, I guess
14:45:14 <ehird> also, you may be used to seeing it but I observe agda from a strictly outside viewpoint! ha!
14:45:28 <ehird> MissPiggy: seems ridiculous to add such craziness just for prettyprinting
14:45:33 <ehird> make a smarter pretty-printer!
14:45:51 <ehird> Unless you make sure it's Friendly!
14:46:22 <MissPiggy> ehird you know I have read so muh lesswrong
14:46:27 <ehird> yeah i prettyprinted my expression that (given infinite time) checked if the reimann hypothesis was true or false
14:46:35 <ehird> it printed "the Boolean *£($&(*£$uq))(ii!£()!*£)(*NO CARRIER
14:46:48 -!- ehird has left (?).
14:47:19 -!- ehird has joined.
14:47:22 <ehird> Phew, my connection dropped there.
14:47:49 <lieuwe> i'm still trying to come up with some sort of high-level esolang... can't come up with anything implementable :-/
14:48:09 <MissPiggy> lieuwe you came up with unimplementable stuff? :)
14:48:11 <ehird> AnMaster: Was that a pun? A carrier carries something, if a carrier stops carrying something they drop it?
14:48:15 <ehird> If so, I love you.
14:48:21 <ehird> You have made an actually good pun.
14:48:33 <lieuwe> MissPiggy: not toataly unimplementable, just very hard...
14:49:00 <AnMaster> ehird, it was a reference to modems mostly. Remembers those leds on them? I mean good old 28 kbit ones and such
14:49:03 <ehird> sounds like the compiler for my language
14:49:13 <ehird> "yeah, in fact it's technically implementable!"
14:49:31 <ehird> should hire a buncha phds to do it for me
14:49:35 <ehird> AnMaster: So not a good pun then :(
14:50:15 <ehird> MissPiggy: i have this horrible feeling that the ML-style module system is going to interact terribly strangely with my type system
14:50:26 <AnMaster> ehird, My variant seems more relevant to any sort of connection over telephony.
14:50:33 <MissPiggy> ehird you could just steal Coqs module system
14:50:42 <MissPiggy> I have no idea about modules though
14:50:45 <ehird> MissPiggy: i might, is it as good as ml's? :P
14:51:02 <MissPiggy> well I think it's basically the same, except a bit extra for the types
14:51:13 <AnMaster> ehird, and iirc you have iphone or adsl to choose from.
14:52:34 <AnMaster> and if you use that or the iphone then it is carrier in several meanings
14:53:07 -!- kar8nga has joined.
14:53:16 <ehird> data [_] ∷ Set → Set where
14:53:20 <ehird> _:_ ∷ λα. α → [α] → [α]
14:53:29 <AnMaster> ehird, but primarily see http://en.wikipedia.org/wiki/NO_CARRIER
14:53:31 <ehird> where _ is the operator placeholder thingy
14:53:43 <ehird> Yeah, yeah, so in actuality those names are in the Container or Sequence or whatever thingy.
14:53:56 <ehird> And yes, overloading ∅ to mean something other than the empty *set* is probably abhorrent.
14:53:58 <MissPiggy> use : for type judgements and :: for cons :P
14:53:59 <ehird> BUT I LIKE UNICODE.
14:54:09 <ehird> MissPiggy: I don't use :: for type judgements, I use ∷
14:54:15 <ehird> AnMaster: I know what no carrior is
14:54:20 <ehird> that's why i said it
14:54:36 <ehird> MissPiggy: i don't even know what it's supposed to be :)
14:54:44 <ehird> anyway : for type judgements just seems too... lightweight
14:54:52 <ehird> i dunno why, it just seems like the meat is taken out from the expression
14:55:10 <ehird> maybe I shhould use ∈ for type judgements :P
14:56:10 <ehird> looks ugly to me :P
14:56:13 <ehird> what's wrong with ::
14:56:36 <MissPiggy> it is the single most common operator you type
14:56:41 <lieuwe> MissPiggy: wtf's up with the greek letters:-p?
14:56:45 <AnMaster> ∈ and :: mean different things, no?
14:56:52 <ehird> lieuwe: we're being pretentious functional programmers
14:57:01 <ehird> is-member-of-set = is-of-type
14:57:10 <ehird> MissPiggy: = is more common than ::
14:57:14 <ehird> think e.g. let and where
14:57:18 <ehird> where often you omit the types
14:57:26 <ehird> but :: outside of a definition isn't very common
14:57:31 <ehird> so = is definitely more common than ::
14:57:33 <AnMaster> ehird, hm seems wrong to use the same symbol for them somehow
14:57:38 <ehird> AnMaster: They are the same thing.
14:57:53 <ehird> You're saying the same thing as "it seems wrong to use the same symbol for addition and addition".
14:58:19 <AnMaster> yes, there should be different symbols for integer and floating point addition
14:58:24 <ehird> Although you have a point in that _∈_ in value-land will be container/sequence-membership, and it'd be nice to be able to use things like that in type-land
14:58:33 <ehird> AnMaster: But those are different things.
14:58:43 <ehird> You don't seem to understand: "Type" is just another word for "set".
14:58:58 <AnMaster> ehird, depends on what set theory and/or type theory you use iirc?
14:59:17 <MissPiggy> we just call them that and use ∈ because we don't like set theory
14:59:42 <MissPiggy> well it's an inductively defined set
14:59:49 <AnMaster> ehird, ℕ is the set of natural numbers yes
14:59:59 <ehird> No, but it's a set.
15:01:23 <ehird> MissPiggy: but yeah, _∈_ in value-land will be member-of-sequencecontainerwhatever; and it would be nice to be able to use that in type-land, which we can't do if we use it for type judgement
15:01:37 <ehird> bloody haskell doesn't have to avoid naming conflicts between value- and type-land :P
15:02:32 <MissPiggy> operators just break up the monotony of f (g x y) (h z (w p q))
15:02:50 <ehird> i suggest we call using non-operator names for functions 9-to-5 naming
15:03:33 <ehird> unicode needs italics-x as a character :P
15:03:55 <AnMaster> ehird, the cross product of x and x?
15:04:11 <AnMaster> iirc × and · are quite different
15:04:13 <ehird> Heard of multiplication, AnMaster?
15:04:34 <AnMaster> ehird, yes but isn't cross product and dot product different for vectors?
15:05:38 * ehird wonders what fun category-theory concept × should be defined to
15:05:44 <ehird> There's gotta be something, there's always something.
15:06:05 * MissPiggy doesn't even know what category theory does...
15:07:02 <ehird> It doesn't do anything! It sits around looking awesome.
15:07:21 <ehird> i'm fairly sure that it's an odd instance of the curry-howard isomorphism though, in that they're the same definitions but used entirely differently
15:07:26 <ehird> cosmic usefulness transfer
15:08:05 <MissPiggy> a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category.
15:08:37 <ehird> you forgot linguistics
15:09:03 <ehird> linguistics is isomorphic to logic, thus to programming
15:09:15 <Gracenotes> is forgetting linguistics worse than forgetting poland?
15:09:21 <ehird> also they, well augur, also i think i've seen you, use basically lambda calculus for some syntax :P
15:09:31 <ehird> Gracenotes: i had to restrain myself not to say that
15:09:33 <ehird> yeah semantics whatever
15:09:43 <AnMaster> no no don't do it. We won't get rid of the linguistics discussion for hours then! :(
15:10:06 <ehird> quick, what's the one thing that can distract augur from linguistics
15:10:17 <ehird> QUICK EVERYONE, TO THE BUTT-BATALLIONS
15:11:18 <oklopol> MissPiggy: in category theory, you have objects, and "structure-preserving mappings" between them, then you have a very general way to define things like isomorphisms, the same definition works for groups and sets and so on, because you just talk about properties of functions that have to do with their composition.
15:11:34 <ehird> oklopol: that also works to kill the linguistics.
15:11:53 <ehird> argh i should have said "buttallions"
15:14:06 <oklopol> basically isomorphisms can be just defined as mappings that can be inverted both ways, that is, "no info is lost", then when you look at the category of groups and morphisms, and the category of sets and functions, you'll see that you've defined a sensible isomorphism for both
15:14:22 <oklopol> called bijection for functions ofc
15:14:56 <MissPiggy> would be nice to have a formal theory about these informationy heuristics we use
15:16:34 <ehird> i did data Bijection a b = Bijection (a -> b) (b -> a) in haskell but i was sad
15:16:43 <ehird> because you couldn't, you know, show that it was actually... that
15:17:15 <ehird> in awesome languages I could just include an (f (g x) = x) :P
15:18:59 <ehird> is that a Category, I wonder?
15:19:18 <ehird> (.) :: cat b c -> cat a b -> cat a c
15:19:43 <ehird> so ((b->c),(c->b)) -> ((a->b),(b->a)) -> ((a->c),(c->a))
15:20:11 <ehird> (Category as in the haskell definition of it in base)
15:20:22 <ehird> that's pretty slick.
15:20:50 <ehird> MissPiggy: it's cool?
15:20:53 <MissPiggy> so you have a category of bijections, now what??
15:21:00 <ehird> now you can compose bijections!
15:21:47 <ehird> I don't even need to require that they be functions
15:21:52 <ehird> I need a way to apply them
15:21:55 <ehird> was thinking I could just do categories
15:24:03 <ehird> data Bijection ∷ Set → Set → Set where
15:24:05 <ehird> Bijection ∷ λα. λβ.
15:24:11 <ehird> {λx. f (g x) ≡ x} →
15:24:13 <ehird> {λx. g (f x) ≡ x} →
15:24:23 <ehird> only problem there is that we need ≡
15:24:31 <ehird> but having it depend on equality is silly imo
15:24:51 <ehird> erm, f and g shouldn't be in {}
15:24:53 <ehird> they should be in (), I think
15:25:11 <ehird> (MissPiggy: right?)
15:25:47 <MissPiggy> if you are into category theory why don't you define it as a split epi
15:26:51 -!- lieuwe has quit (Ping timeout: 248 seconds).
15:27:18 <ehird> because i don't understand category theory :)
15:27:37 * ehird wonders how to combine GADTs and the Foo { blah :: ..., } stuff
15:29:15 <ehird> well, not record syntax necessarily
15:29:21 <ehird> just automatic accessor-definers
15:29:28 <ehird> MissPiggy: you know what would be nice?
15:29:32 <ehird> Having juxtaposition be like
15:29:48 <ehird> juxtaposition :: (Juxtaposable a b c) => a -> b -> c
15:29:55 <ehird> class Juxtaposable a b c | a b -> c
15:30:04 <ehird> so you have Juxtaposable (a -> b) a b
15:30:15 <ehird> and, say you have an accessor
15:30:17 <ehird> but it also works for writing
15:30:42 <ehird> modify :: value -> accessor for that value -> new value of the property -> value
15:30:51 <ehird> Juxtaposable (Accessor a b) a b
15:30:58 <ehird> so you can do "prop value" for access
15:31:02 <MissPiggy> by the way (you probably know this..) the dependent type stuff is more general than GADT
15:31:25 <MissPiggy> hmm although is it more general than She style GADT?
15:31:36 <ehird> but gadts are nice syntax for most stuff, so.
15:33:05 <ehird> i'll also have type-level functions basically
15:33:12 <ehird> type Foo bar baz quux = ...
15:33:32 <ehird> i was just picking an arbitrary keyword :)
15:33:41 <ehird> but it's the same thing as haskell's type synonyms
15:33:50 <MissPiggy> the only different is that you are going into Set rather than Int or something
15:34:01 <ehird> but you use it at compile-time
15:34:07 <ehird> I guess in the living environment of my OS it doesn't matter, but...
15:34:15 <ehird> I suppose you are right.
15:35:36 <ehird> # 9.7-inch (diagonal) LED-backlit glossy widescreen Multi-Touch display with IPS technology # 1024-by-768-pixel resolution at 132 pixels per inch (ppi)
15:35:42 <ehird> According to Apple 4:3 is widescreen
15:38:29 <AnMaster> btw, for P=NP, could it be that it is unprovable if it is the case or not? Has anyone tried to prove it unprovable?
15:38:49 <ehird> http://www.google.co.uk/#hl=en&source=hp&q=p%3Dnp+unprovable&btnG=Google+Search&meta=&aq=f&oq=p%3Dnp+unprovable&fp=33a9a577caa4e7cb
15:38:57 <ehird> This article shows that "P-not-equal-to-NP" is unprovable in ZFC. Here is a review of this proof by the German logician Ralf Schindler. ...
15:39:04 * ehird wonders if it's a crackpot
15:39:09 <AnMaster> ehird, #hl? that url is broken
15:39:20 <AnMaster> everthing after that first # is an anchor
15:39:21 <ehird> "Unfortunately, there is an error in the proof [...]."
15:39:24 <ehird> AnMaster: javascript
15:39:37 <AnMaster> ehird, usually I don't get # there in the urls..
15:39:42 <ehird> it's to avoid loading the surrounding stuff of the page, I bet
15:39:46 <ehird> to speed up load times
15:40:12 <ehird> "Proof by contradiction. Assume P=NP. Let y be a proof that P=NP. The proof y can be verified in polynomial time by a competent computer scientist, the existence of which we assert. However, since P=NP, the proof y can be generated in polynomial time by such computer scientists. Since this generation has not yet occurred (despite attempts by such computer scientists to produce a proof), we have a contradiction."
15:41:24 <AnMaster> ehird, After reading it twice: huh?
15:41:38 <ehird> It's a joke; laugh.
15:41:56 <ehird> If you don't understand it, you don't understand what p=np means :P
15:42:54 <ehird> If we can defeat entropy and have a singularity it doesn't matter how long computations take; the universe will be filled with one gigantic computer on which all our minds will be uploaded. It will make us experience time in sync so that every computation is instant.
15:43:15 <ehird> i.e., if someone runs a computation that takes a gazillion years, everyone stops thinking, a gazillion years pass, then we resume thinking; to us, the computation happened immediately
15:43:25 <AnMaster> ehird, well, my brain was in math proof mode when reading it. I do see the joke now
15:45:20 <AnMaster> what I meant was, that maybe P=NP is unprovable in the same sense as the cardinality of R. Or to take another example: the parallel postulate in Euclidean geometry. (Which is why it is an axiom)
15:47:28 <ehird> Why don't we just define P=NP as an axiom?
15:47:33 <ehird> omg, this changes everything :D
15:49:51 <AnMaster> couldn't it (in theory) be proven that it is impossible to prove either P=NP or P!=NP ?
15:50:42 <ehird> If it's true, maybe it can be proven.
15:50:52 <ehird> It could be true that it is unprovable and yet not be provable that it is unprovable.
15:51:01 <ehird> It could also be false and thus not provable, at least if ZFC is consistent.
15:51:25 <AnMaster> ehird, maybe it could be proven that it is unprovable to prove it unprovable?
15:51:59 <ehird> I'll prove your mom.
15:52:16 <AnMaster> alas I can't think of any snappy reply to that
15:53:20 <ehird> "Your mom proved your face in bed last night, didn't she?"
15:53:29 <ehird> "I was there. WATCHING"
15:53:45 <MissPiggy> <ehird> Why don't we just define P=NP as an axiom? -- because nobody knows if it's independent yet!!
15:54:15 <ehird> CONSISTENCY IS IRRELEVANT!
15:55:18 <ehird> i feel like i'm stumbled upon this wonderful oasis in programming language design
15:55:29 <ehird> all the smartest people are here and it has such cool stuff
15:55:52 <ehird> also, she is my favourite preprocessor ever.
15:56:04 <ehird> pattern synonyms are actually something i've always wanted in haskell
15:57:22 <ehird> YOU BROKE THE GRAMMAR
15:57:41 <ehird> She has rules, and the first is: She can be talked about, but only if you respect her grammar.
16:00:31 <AnMaster> hm a non-constructive proof for P=NP would be fun
16:01:14 <ehird> Go straight to ⊥; do not pass go, do not collect £200.
16:01:52 <AnMaster> isn't testing *if* a number is prime in P? iirc that is
16:03:01 <ehird> That book actually contained something meaningful?
16:03:15 <ehird> Stolen from someone else, right?
16:03:29 <ehird> Oh, not A New Kind of Science.
16:03:34 <ehird> It was published in 2002.
16:03:40 <ehird> My inferrence engine is broken today.
16:03:50 <AnMaster> ehird, you mean, it wasn't intentional
16:04:09 <ehird> MissPiggy: any totally dependawesome insights on http://www.daimi.au.dk/~madst/tool/papers/expression.txt
16:04:22 <ehird> she has http://personal.cis.strath.ac.uk/~conor/pub/she/higpig.html but i dunno seems hacky
16:04:28 <MissPiggy> I have never actually understood this problem
16:04:41 <ehird> my understanding is
16:04:51 <MissPiggy> higgelty piggelty works nice for epigram
16:05:00 <MissPiggy> but I don't know if it's related to expression problem
16:05:01 <AnMaster> Deewiant, I have a vague memory of reading that AKS is horribly inefficient though. And that some of the non-polynomial algorithms are in fact faster in practise for most "practical purposes"
16:05:13 <ehird> data Ty a = Foo a | Bar a
16:05:18 <MissPiggy> and I'm not sure even if I come up with a solution that I deem _perfect_ other people will just say it sucks
16:05:29 <ehird> Here, we can easily add functions (columns) to this without violating type safety or modifying existing code,
16:05:39 <ehird> but we cannot add new rows (data type cases)
16:05:49 <Deewiant> AnMaster: I don't know if it's "horribly inefficient" but yes, in practice it's slower than the probabilistic tests
16:06:07 <ehird> in an object-oriented language, the columns can't be changed: they're the methods in a class
16:06:12 <ehird> but you can easily add new rows: subclasses
16:06:21 <ehird> The expression problem is: How can we have *both*?
16:06:56 <MissPiggy> you have data Expr = ..., and each constructor of Expr is a row
16:07:03 <MissPiggy> and you have func1, func2, ... each is a column
16:07:25 <ehird> you can easily add new functions, but you cannot add rows *elsewhere in the program*
16:07:35 <ehird> with functions, you can just create a new one and bam, you're done
16:07:48 <MissPiggy> so to add a new constructor you have to update each func1, and to add a new func you have to update each constructor??
16:07:51 <ehird> you have class Foo { int bar(); int quux(); }
16:07:57 <ehird> each method is a column
16:08:08 <ehird> the values as the rows still
16:08:14 <ehird> but you can extend them
16:08:15 <ehird> class Bar extends Foo { ... }
16:08:18 <ehird> so we can add rows
16:08:26 <ehird> so with FP you can add columns, with OOP rows; the problem is being able to add both
16:08:33 <ehird> elsewhere in the program
16:08:40 <ehird> without breaking existing code
16:09:14 <ehird> i'll make a text file showing this more clearly without ircspeak
16:09:23 <MissPiggy> you can do both of these (FP or OOP) approach using ADTs
16:09:43 <MissPiggy> I mean each one individually, using a different approach
16:09:44 <AnMaster> btw, when you measure O(whatever) for an algorithm for prime factorisation, what exactly is it you measure it against.
16:09:56 <MissPiggy> but to have one framework that lets you solve both problems at once..
16:10:15 <Deewiant> AnMaster: Their complexities are O(f(n)) where n is the number tested
16:12:02 <oklopol> usually you say a number's size is its log
16:12:14 <oklopol> so just stick 2^n in there
16:12:22 <AnMaster> Deewiant, wouldn't then "try each number from 2 to sqrt(n) to see if it divides n" be O(sqrt(n)). After all, that is how many divisions you perform. And O(sqrt(n)) would grow slower than O(n), no? And isn't O(n) polynomial?
16:13:00 <AnMaster> I must be missing something critical here
16:13:10 <oklopol> AnMaster: that's a pseudopolynomial algorithm for it, a polynomial algorithm, when talking about numbers, is one where you take n as the log of the number
16:13:36 -!- MissPiggy has quit (Quit: MissPiggy).
16:13:39 <oklopol> for numbers we have separate classes for taking the number as its own size (pseudo), and taking its log as size (more natural for most problems)
16:13:43 <AnMaster> oklopol, ah. Which logarithm? the natural one?
16:14:06 <oklopol> i'll leave proving that as homework
16:14:30 <AnMaster> oklopol, it does... if you take the n-log
16:15:09 <oklopol> obviously it must be a constant
16:15:30 <ehird> eh, misspiggy disappeared
16:15:48 <oklopol> anyway log_a(n) and log_b(n) are a constant apart, so that doesn't matter for O
16:16:32 <ehird> Well, for anyone who wants an explanation of what the expression problem is: http://pastie.org/812457.txt?key=jy9qm2hfkgtfxiooahshxw
16:16:48 <oklopol> i have enough problems already
16:17:23 <AnMaster> oklopol, hm correct me if I'm wrong but: log_a(n) > log_b(n) for all n if a < b?
16:17:27 <ehird> http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w
16:17:32 <ehird> Revised version; forgot to change one sentence.
16:17:41 <AnMaster> wait, no, that probably only applies to n larger than the base or such
16:17:45 <ehird> oklopol: Is a bitch one?
16:17:58 <oklopol> ehird: they all have to do with complex analysis
16:18:14 <AnMaster> oklopol, "nope" to "only applies" or to the original statement?
16:18:40 <oklopol> no matter what n is, log is increasing
16:18:41 <ehird> oklopol: So I suppose you could say that you have 99 (minus 94) problems, but a bitch ain't one.
16:19:00 <AnMaster> oklopol, well yes, but that isn't what I said. I said what their relative values are
16:19:04 <oklopol> ehird: is that a reference to something?
16:19:14 <ehird> Maybe. Also, http://i.imgur.com/b8OLl.jpg
16:19:49 <AnMaster> oklopol, log_10(500) < log_e(500) for example
16:20:03 <oklopol> yeah that's true then, log is decreasing w.r.t. base
16:20:05 <AnMaster> (those are the ones with easily accessible buttons on my calculator
16:21:50 <Deewiant> AnMaster: What you're missing in your trial division thing is the complexity of a division
16:21:50 <AnMaster> oklopol, does it make sense to do something like lim_{a->+inf} log_a( whatever )
16:22:33 <AnMaster> oklopol, then use that log for the complexity!
16:23:06 <AnMaster> whenever it is constant or not could perhaps be argued, but it no longer depends on n at least
16:23:16 <AnMaster> Deewiant, hm. What is that complexity
16:23:30 <oklopol> O(n^2) with the trivial algo
16:23:35 <AnMaster> oklopol, well, I'm on deep water here, I probably missed something crucial.
16:24:14 <AnMaster> that is still polynomial unless I'm completely missing something?
16:24:18 <oklopol> i don't remember what the known bounds are tho
16:24:28 <oklopol> wait were you serious about the lim?
16:24:32 <oklopol> i have no idea what you meant
16:25:09 <AnMaster> but, it is an interesting question: What happens with logarithms as the *base* approaches infinity?
16:25:41 <oklopol> the function "f(n) = lim_{a->+inf} log_a( n )" is the constant function 0, i think
16:26:48 <oklopol> i also think in the interval [1, inf) we have uniform convergence, but my head hurts a bit too much now to be sure
16:27:56 -!- cheater3 has joined.
16:28:32 <Deewiant> AnMaster: If n = number of bits in the number then trial division is O(2^(n/2)) (Wikipedia), which I guess is where the non-P-ness comes from.
16:31:25 -!- cheater2 has quit (Ping timeout: 264 seconds).
16:31:48 <AnMaster> also, why can't you have negative arguments to log? I mean, y = log_a(x) means the same as a^y = x right? And in the latter you can get negative x.
16:33:31 <AnMaster> (-4)^3 = -64 Thus shouldn't 3 = log_{-4}(-64) ?
16:34:47 <ehird> AnMaster: So -64 takes 3 digits to represent in base -4? Noted.
16:35:10 <oklopol> with a negative base, it makes no sense to give the log any arguments except naturals afaik
16:35:12 <AnMaster> ehird, well yeah, when you think of logarithms that way it doesn't really work out ;P
16:35:27 <ehird> isn't it true though?
16:35:30 <Deewiant> For general negative x, y is complex
16:35:45 <AnMaster> oklopol, hm? (-2)^(-1/2) gives an imaginary answer, doesn't it?
16:36:15 <ehird> abc in base n is just (((a*n)+b)*n)+c
16:36:31 <AnMaster> to be more precise, isn't it ((sqrt(2))^-1)i
16:37:09 <AnMaster> Deewiant, ah, the lack of uniqueness could indeed cause issues
16:38:10 <oklopol> hmm okay i'm not sure what i was thinking
16:38:27 -!- MissPiggy has joined.
16:38:40 <ehird> MissPiggy: http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w
16:38:48 <AnMaster> Deewiant, but then sqrt(n) really isn't unique either, except it is defined to be the positive value. Which is why you for the solution to x^2 = 4 would write x=+/- 2
16:38:50 <ehird> The expression problem, explained simply.
16:39:02 <MissPiggy> ehird iI think I can give nice solution
16:39:13 <ehird> are you so excited you can't type? :P
16:39:14 <MissPiggy> which makes essential use dependendt types
16:39:37 <MissPiggy> I am on my moms computer because I got fed up with this installer
16:39:39 <AnMaster> MissPiggy, which layout normally?
16:39:57 <Deewiant> AnMaster: As I see it, the problem is defining log_a(x) so that it gives the appropriate real result for negative x, but is undefined when no such value exists
16:41:05 <MissPiggy> of course the type of c can depend on the tail of the list
16:41:22 <ehird> or are we still calling it the tail
16:41:25 <ehird> just having tail::head
16:41:26 <Deewiant> AnMaster: log_a(x) would be defined when: x > 0 & a > 1 or x < 0 & a < 0 & what
16:41:49 <MissPiggy> i mean you coulld have xs :: x, then x : Vector (length xs)
16:41:50 <AnMaster> Deewiant, hm? Two things there: 1) why must it be a real value? 2) undefinedness in some points doesn't sound too bad, after all x^-1 is undefined for x = 0 (defined in all other points afaik)
16:42:02 <Deewiant> AnMaster: 1) if you want it to be complex, that's already been done.
16:42:15 <MissPiggy> then you get [] :: () :: (a) :: (x y) :: (p q r)
16:42:24 <ehird> http://www.wolframalpha.com/input/?i=set
16:42:37 <Deewiant> AnMaster: For 2), sure, but what's the definition
16:42:39 <MissPiggy> so similar to this, instead of making a triangle ou could make a matrix
16:42:58 <cheater3> anyone got introduction to algorithms 3e?
16:42:58 <AnMaster> Deewiant, 1) hm right 2) what?
16:42:59 <ehird> MissPiggy: interesting!
16:43:11 <ehird> but does it work for any type? i don't think so
16:43:14 <ehird> you have to define it to work
16:43:20 <AnMaster> Deewiant, isn't it undefined due to x^-1 = 1/x and division with zero being undefined?
16:43:22 <Deewiant> AnMaster: Sure, you can let it be undefined for some values, but what are those values
16:43:29 <MissPiggy> now the actual elements of each row/col would have a type computed based on the recursion structure of the function in that column against the fold for the type of that row
16:43:53 <MissPiggy> ehird anyway that's just the idea.. I'll try and write it out and see if it works
16:44:23 <ehird> MissPiggy: If that works it's really cool
16:44:23 <AnMaster> Deewiant, I think we are talking about two different things here. with regards to 2).
16:44:43 <AnMaster> Deewiant, Didn't "sure, but what's the definition" refer to the bit "x^-1 is undefined for x = 0"?
16:45:00 <Deewiant> AnMaster: I meant what would the definition of log_a(x) be
16:45:09 <AnMaster> Deewiant, I read "what" as "that" -_-
16:45:12 <Deewiant> And what values of a and x would it be defined for
16:45:30 <AnMaster> Deewiant, as in, you claimed x^-1 was undefined for x=0 due to being defined that way XD
16:46:01 <Deewiant> (Although that's sort of true too.)
16:46:54 <Deewiant> x^-n is defined as 1/x^n for x != 0, n > 0
16:47:36 <oklopol> of course you can define the function to have any value you want, you just can't make a field have a meaningful multiplicative inverse for 0
16:47:45 <AnMaster> hm, forgot that was by definition rather than as a consequence of something else
16:47:58 <oklopol> well it's a consequence of what i said
16:48:13 <oklopol> that it's defined that way
16:48:15 <AnMaster> Deewiant, but a lot of math wouldn't work if it wasn't defined like that though.
16:49:14 <Deewiant> I didn't say it's unnecessary or anything.
16:49:43 <AnMaster> (differentiation of expressions like x^(1/3) comes to mind)
16:49:55 <AnMaster> Deewiant, hm is it an axiom then?
16:52:00 <AnMaster> wouldn't it radically change the "rule" that (x^a)' = a*x^(a-1) though if that definition of negative exponents didn't exist?
16:52:21 <AnMaster> Hrrm, maybe it could be defined in some other way for when a<1 in that case
16:52:39 <oklopol> in no point but 0 could that change
16:52:54 <MissPiggy> there's two kinds of differentiation
16:53:14 <MissPiggy> one is where you differentiate a function, like the function x |--> x^a
16:53:42 <MissPiggy> the other is where you differentiate 'formally', like it's just some kind of symbolic operation on syntax
16:53:50 <MissPiggy> and you get dxdx = 0, dxdy = -dydx
16:54:32 <oklopol> there are natural ways to interpret those, even without infitesimals
16:54:50 <oklopol> and to be honest i'm not sure i understand them
16:55:05 <AnMaster> MissPiggy, I always distrust math that treats dx and dy as if you could treat them like a normal variable. For a start; they consist of more than one letter! ;P
16:55:12 <MissPiggy> well, ... it gives the right answer in the end
16:55:22 <ehird> d isn't a letter though
16:55:22 <oklopol> formal differentiation is usually an operation defined for polynomials defined just like differentiation usually works for polynomials
16:55:31 <ehird> d is a magical operation and it isn't even the letter d!
16:55:36 <ehird> at least i consider d an operation, prolly cause i'm stupid
16:55:44 <ehird> like, it's a transformation on variables
16:58:04 <AnMaster> I highly distrust how integration by substitution due to the way it treats dx. Stuff like dx/dt=t' leading to dx=t'dt :/
16:58:38 <MissPiggy> oh you know integration by substitution
16:59:06 <oklopol> intergration by substitution works as follows: substitute something for x.
16:59:07 <MissPiggy> if (x,y,z) is one coordinate system (u,v,w,...) is another, then you make a pullbacn
16:59:27 <AnMaster> MissPiggy, I have a test in a course about integration in two weeks time. Err make that integration and differential equations even.
17:00:06 <MissPiggy> and the idea is that you can transform forms like Adx+Bdy+Cdz into a du,dv,dw.. form
17:00:38 <AnMaster> MissPiggy, wait, is that integration in more than one variable?
17:01:16 <MissPiggy> you can interate over dx,dy,dz, or dydz,dxdz,dydx or dxdydz
17:01:21 <AnMaster> MissPiggy, I don't read that much math when studying CS. At least not during the first year
17:01:34 <MissPiggy> which corresponds to the curves, surfaces and volumes
17:01:59 <MissPiggy> of course 3D is just one special case of nD
17:02:48 <AnMaster> MissPiggy, well yes, I am aware of that it is possible to do integration in more than one variable. I don't know how however.
17:03:39 <MissPiggy> well theres this theorem that relates integration over a boundry to integration over the volume itsselt
17:03:39 <oklopol> AnMaster: if you have a function from an n-dimensional rectangle to reals, just integrate one axis at a time
17:04:05 <MissPiggy> it's all pretty nebulous and convoluted.. I'm still trying to figure it out myself
17:04:14 <oklopol> i mean integrate along one axis, and at each point integrate over the (n-1)-dimensional rectangle
17:04:18 <oklopol> corresponding to that point
17:05:11 -!- Pthing has quit (Remote host closed the connection).
17:05:16 <AnMaster> oklopol, like ∫(∫(∫...dz)dy)dx? or something like that?
17:05:28 <oklopol> if you wanna integrate a function from some more complex thing, you usually use substitution so you can integrate on a rectangle
17:06:05 <oklopol> fubini's theorem says you can integrate along the axes separately, and order matters not
17:06:08 <AnMaster> oklopol, I mean: do they go inside each other, instead of, say, being multiplied with each other or some other operation to combine them
17:07:08 -!- sshc has quit (Quit: leaving).
17:07:13 <AnMaster> oklopol, seems like a PITA to calculate though
17:07:33 <AnMaster> (considering what a PITA integrals in one variable is)
17:07:40 <oklopol> if you have n axes, you have to solve n integrals
17:07:56 <oklopol> often some of them are just multiplication
17:08:28 <AnMaster> oklopol, oh? "often" as in "often in exams" or "often in real world applications"?
17:09:27 <oklopol> say you're integrating f(x, y) = x over [0,1]x[0,1], you'd have int_{x from 0 to 1}( int_{y from 0 to 1} x ), so you just get int_{x from 0 to 1} ( x ), because you're integrating the *constant* x over y
17:10:02 <oklopol> if you're integrating an expression that doesn't depend on y over variable y, then it's just multiplication
17:10:07 <oklopol> i don't know anything about the real world
17:10:14 <oklopol> or calculus, for that matter
17:11:24 <fizzie> In real world you just integrate numerically and forgot all that symbol-manipulation nonsense. (Okay, so maybe not *quite*...)
17:11:31 <AnMaster> oklopol, also, as far as I have understood it, ∫(f(x)*g(x))dx can't be solved for _all_ f and g where both ∫f(x)dx and ∫g(x)dx can be solved. Except with numerical methods that is.
17:11:41 <AnMaster> even if you can solve it for many such products
17:12:04 <AnMaster> (that was in reply to "<oklopol> often some of them are just multiplication")
17:12:30 <oklopol> yeah okay you completely misunderstood then
17:12:46 <oklopol> reread "oklopol: if you're integrating ..."
17:13:19 <AnMaster> oklopol, well, yes, I was so busy writing that line to be correct, I hadn't noticed any line after "<AnMaster> oklopol, oh? "often" as in [...]"
17:13:27 <oklopol> int_{y from a to b}( x ) is integrating a constant from a to b, so you just get (b - a)x
17:14:10 <oklopol> often the expression is only nontrivial to integrate over one axis (in homework problems that is :P)
17:14:51 <AnMaster> int_{y from a to b}( x ) <-- I can't say I'm familiar with that syntax. It looks like pseudo-latex though.
17:15:21 <oklopol> even int y a b (x) should be obvious
17:15:44 <AnMaster> oklopol, to be more specific: I'm unable to detect any dx or dy indicating which variable you are integrating to
17:15:56 <AnMaster> err, "integrating with respect to"
17:16:21 <AnMaster> well okay, then that line makes perfect sense yes
17:16:56 <Deewiant> That'd be (b - a)y then, not (b - a)x.
17:17:48 <Deewiant> No, right, I read that exactly upside-down.
17:17:55 <AnMaster> Deewiant, err wait... the x would still be there as well, no? wouldn't it be x*(b-a)*y
17:17:58 <oklopol> y is not necessarily even bound after the integral, and okay
17:18:24 <oklopol> AnMaster: y means nothing except inside that integral.
17:18:36 <AnMaster> oklopol, I forgot that it wasn't an indefinite integral
17:19:02 <oklopol> ...what does it have to do with this that it's indefinite?
17:20:18 <AnMaster> oklopol, unless I'm completely confused by now: ∫xdy = ∫(x*1)dy = x*∫1dy = x*y
17:20:29 <oklopol> (i mean apart from the fact it's not one)
17:20:52 <Deewiant> AnMaster: Yes, for an indefinite integral that's correct.
17:21:19 <AnMaster> MissPiggy, well yes. I added the 1 to make it clear what I meant though.
17:21:38 <AnMaster> And for an definite one then y turns into (b-a)
17:22:27 <AnMaster> Deewiant, well, but looks like oklopol got confused:
17:22:29 <AnMaster> <AnMaster> y is what gives (b-a) indeed
17:22:29 <AnMaster> <oklopol> ...what does it have to do with this that it's indefinite?
17:23:01 <oklopol> yeah i was confused, didn't see why it's relevant that the definite integral was indefinite
17:23:07 <Deewiant> AnMaster: So why are you talking to me and not him?
17:23:09 <AnMaster> oklopol, my point was that I forgot it _wasn't_ indefinite
17:23:30 <oklopol> "AnMaster: oklopol, I forgot that it wasn't an indefinite integral" misread
17:23:37 <AnMaster> Deewiant, well: both since you highlighted me ;P
17:24:22 <Deewiant> Mostly because he didn't respond
17:24:54 <AnMaster> Deewiant, err? he did? "<oklopol> oh" 8 seconds before that highlight?
17:25:23 <Deewiant> I wasn't sure if that was a response :-P
17:25:32 <oklopol> i just realized what he meant
17:25:51 <oklopol> and continued watching simpsons
17:25:52 <AnMaster> Deewiant, I couldn't see what other interpretation would make any sense though
17:27:04 -!- MissPiggy has quit (Quit: MissPiggy).
17:27:39 <AnMaster> also: definite integrals from 1 to infinity (or similar) are creepy.
17:28:29 -!- MissPiggy has joined.
17:29:40 -!- Asztal has joined.
17:30:18 <AnMaster> wasn't it something like the integral of 1/x from 1 to inf went to infinity. But if you rotated the curve that is formed by that function around the x axis and integrated to find the volume of it, then it result in some finite number? But if you tried to find the area of that body, it went towards infinity
17:30:36 <AnMaster> I don't remember if it was 1/x or 1/(x^2). Something like that anyway
17:30:45 <oklopol> think about the same thing in one less dimension
17:30:58 <oklopol> say you have the curve 1/x^2 or something
17:31:03 <oklopol> the are under it is finite
17:31:07 <oklopol> but the actual line is infinite
17:31:18 <AnMaster> which is creepy too. But not quite as creepy
17:31:27 <oklopol> then there's the paint argument
17:31:38 <oklopol> if you pour paint into the infinite tube
17:31:52 <oklopol> but you can never actually paint it
17:31:53 <AnMaster> but it wouldn't be enough to paint the sides
17:32:16 <oklopol> but the thing is this makes absolutely no sense as an analogy
17:32:35 <oklopol> because you'd be painting it with some constant thickness of paint
17:33:12 <oklopol> so obviously you'll be using much more paint toe paint it than to fill it, after a whi
17:34:52 <AnMaster> oklopol, about that thickness: you could get it go towards zero.
17:35:17 <AnMaster> (makes as much sense at the rest...)
17:35:37 <AnMaster> anyway, there are several creepy bits here: 1) that an integral from n to infinity can give a finite value (where n is a finite number). 2) that you get finite volume and infinite area.
17:35:40 <oklopol> and then the amount of paint would also be finite
17:35:56 <AnMaster> well for 1), that is excluding the integral of f(x)=0
17:36:55 <AnMaster> or functions that not only approach zero, but actually reach it and then stay there.
17:37:00 <oklopol> that sounds about as creepy as "two numbers can add up to a third one"
17:38:05 <oklopol> it just does not sound creepy
17:38:45 <ehird> oklopol: they CAN?!?!?!?
17:38:51 <AnMaster> oklopol, okay to be more exact: a function f(x) with the property that "f(x)>0 for all x" can (sometimes) when integrated from a finite number n to infinity have a finite integral
17:38:56 <oklopol> ehird: they can, and they *will* :|
17:39:04 <AnMaster> oklopol, how is that not creepy?
17:39:20 <ehird> are you sure you know what creepy means
17:40:23 <oklopol> does it sound creepy that we can have an infinite set all of whose elements are positive, but for which there is such a real number r that for all finite subsets of our set, the sum of that set is less than r?
17:40:34 <oklopol> this is what the whole thing reduces to
17:40:54 <oklopol> shouldn't use words for stuff like that
17:41:25 <AnMaster> ehird, hm? It seems to contradict intuition of reality. Yes I know that intuition is quite often wrong. Still results in a creepy feeling for some cases of it.
17:43:09 <AnMaster> oklopol, that way to express it is too abstract (to me at least) to visualise it.
17:43:33 <oklopol> it means you take your integral and round things up
17:43:42 <oklopol> you get an infinite amount of numbers
17:44:18 <oklopol> and if you know anything about series, you can see this infinite amount of numbers can have such an upper bound
17:44:25 <AnMaster> oklopol, but try imaging this integral in terms of area
17:44:43 <oklopol> i always imagine infinite sums in terms of area
17:44:55 <oklopol> say i have a sum of 2^n for n = 0, 1, ...
17:44:58 * pikhq imagines a function which asymptotically approaches 0.
17:45:05 <oklopol> i just start stacking them up
17:46:02 <AnMaster> oklopol, so you feel perfectly comfortable on all levels with the fact that an area A limited by two infinitely long sides can be finite?
17:47:04 <oklopol> AnMaster: sure, i even feel comfortable with defining "area" of that to be a frog
17:47:39 <ehird> negative bases are awesome
17:47:54 <oklopol> there is no connection between mathematical areas and the real worls
17:48:05 <ehird> http://en.wikipedia.org/wiki/Negative_base
17:48:35 <AnMaster> where - is a minus sign of course
17:49:52 <AnMaster> oklopol, then how do you explain that finite real world and math areas seem quite often to match up?
17:50:06 <ehird> http://personal.cis.strath.ac.uk/~conor/pub/Holes/Holes.pdf
17:50:32 <ehird> AnMaster: because we constructed them to be vaguely similar to the real world at first
17:50:44 <oklopol> AnMaster: they model the real world well; obviously i didn't mean what i said
17:50:47 <ehird> matheamtics has no inherent existence, it's just single-manipulation we dreamed up
17:50:50 <oklopol> although it was completely true
17:51:52 <ehird> Your definition of "real" is strange.
17:51:55 <AnMaster> MissPiggy, unless it is complex (or quaternionius or whatever)
17:52:04 <ehird> It does not exist physically, and abstract concepts do not really "exist" as such, they only exist insofar as operations on them.
17:52:13 <oklopol> but the geometry of our world isn't the same as R^n, it's just one approximation of it
17:52:16 <ehird> And the symbol manipulation was all invented by us. There's no inherent existence of mathematics.
17:52:18 <AnMaster> "quaternionius" sound incredibly awkward
17:52:19 <ehird> The universe does not have mathematics. We do.
17:52:30 <ehird> AnMaster: Sounds like a good name for a fictional character.
17:53:33 <AnMaster> oklopol, what about fractals? Comfortable with them too?
17:54:23 <ehird> AnMaster is uncomfortable with a lot of very simple things.
17:54:23 <AnMaster> ehird, hm does a balanced negative base even make sense?
17:54:29 <oklopol> MissPiggy: no one's saying mathematics isn't real, because that's not really a question, but according to modern physics we do not live in R^3, although a nice model of physics can be constructed by saying particles are points in R^3
17:54:52 <oklopol> AnMaster: what definition of fractal?
17:55:08 <MissPiggy> I agree with what you are saying about geometry
17:55:31 <oklopol> i'm not all that comfortable with sets whose hausdorff dimension is not a natural number, they are usually really scary
17:56:55 -!- Pthing has joined.
17:57:56 <AnMaster> oklopol, also I'm no expert on fractals, not sure what you mean with definition of fractal here. The bit that defines a specific fractal?
17:58:33 <Deewiant> "Definition of fractal" can't really mean more than one thing
17:59:22 <oklopol> AnMaster: hausdorff measures are a way to measure sizes of sets, just like jordan measures and lebesque measures, jordan being the simplest one; hausdorff measures take as argument the "dimension" of the set you're measuring, for instance if you draw a line in R^3, it's 1-dimensional measure can be finite, although it's 3d-measure is clearly 0
17:59:56 <AnMaster> I could think of two things: a) definition of a given fractal b) definition of what a fractal in general is.
18:00:11 <Deewiant> "Definition of fractal" can't mean a)
18:00:17 <oklopol> the hausdorff dimension of a set is such a real number that the hausdorff measure of the set, with that dimension, is not zero or infinite
18:00:25 <Deewiant> "Definition of x" where x is known to be a fractal does
18:00:39 <oklopol> now fractals, afaik, are defined as sets whose hausdorff dimension is not a natural number
18:01:16 <oklopol> but a common way to construct such sets is through these recursive thingamajigs
18:01:33 <oklopol> which are probably a more common definition for a fractal
18:02:20 <oklopol> so what i'm saying is i'm comfortable with drawing things recursively, but sure, some complex sets are pretty scary
18:02:27 <AnMaster> well yes recursive algorithms is the most common way to define a fractal that I have seen
18:03:03 <oklopol> so everything is a fractal that can be computed using recursion, or what exactly?
18:03:27 <oklopol> a question by which i mean that's a crappy definition, the hausdorff one is sexy
18:03:49 <AnMaster> oklopol, I did know a bit about the dimension thing
18:03:53 -!- MissPiggy has quit (Quit: MissPiggy).
18:04:37 <oklopol> what do you mean, you knew we can embed k-dimensional objects in n-dimentional space?
18:05:47 <AnMaster> also, what ehird said about common creepyness above: by that logic complex numbers should be creepy. But they aren't IMO
18:07:04 <AnMaster> <oklopol> what do you mean, you knew we can embed k-dimensional objects in n-dimentional space? <-- I knew that fractals had a non-natural number dimension.
18:07:48 <oklopol> (i hope you also know not all do)
18:08:55 <oklopol> i mean if you use the definition "thing you can draw using some sorta recursino"
18:10:04 <AnMaster> oklopol, well that includes things that aren't fractal clearly. Such as: f(x,y) = draw a straight line of length 1 jonined up to f(x+1,y)
18:10:39 <AnMaster> which, while recursive, would give you a straight line starting at a given point and then going on forever
18:11:46 <oklopol> the sexiest thing about hausdorff dimensions is you don't have need to be working with real numbers
18:11:55 <AnMaster> oklopol, what about requiring more operations for each step (alt: you recurse more than once at a given level)
18:12:11 <AnMaster> most (all?) fractals seems to be like that?
18:13:26 <AnMaster> like "f(L) = divide the line L in 3, remove middle, call the other two L1 and L2, f(L1), f(L2)"
18:13:40 <AnMaster> hm, is that a fractal, or just something similar?
18:14:06 <oklopol> did you come up with that?
18:14:15 <AnMaster> oklopol, I know that algorithm is a classical one
18:14:19 <oklopol> if you did, you could've been famous!
18:14:21 <AnMaster> I didn't remember the name of it
18:14:38 <oklopol> also called cantor's dust, it has useful properties
18:14:51 <AnMaster> oklopol, name is indeed familiar when you mention it
18:15:03 <AnMaster> oklopol, anyway, what is the dimensionality of it
18:15:32 <oklopol> all the cs's are homeomorphic (the ones obtained by different sorts of splits into three parts), but some leave you with zero measure, some have finite
18:15:52 <ehird> Homeomorphic lebesques.
18:16:01 <ehird> I think they have porn of those.
18:16:48 <Deewiant> Higher math is actually all porn behind the scenes
18:16:52 <AnMaster> also: "<oklopol> koch snowflake" <-- that's the one you add in a triangle (well, two sides of one) in the middle, right?
18:16:53 <oklopol> i don't know if the hausdorff dimension goes down and measure goes up for some splits, you'd have to ask someone who actually know about this stuff
18:17:22 <ehird> Homeomorphic lebesques functoring.
18:17:59 <ehird> "Bona fide elements of ∅ are hard to come by, so we may safely offer to exchange them for anything you might care to want: as you will be paying with bogus currency, you cannot object to our shoddy merchandise."
18:18:52 -!- MizardX has quit (Read error: Connection reset by peer).
18:19:03 -!- MizardX has joined.
18:19:34 <AnMaster> ehird, that quote is one truly awful joke...
18:20:11 <ehird> It's not so much a joke as colourful wordplay.
18:20:34 <ehird> http://personal.cis.strath.ac.uk/~conor/pub/Holes/Holes.pdf, a paper that begins:
18:20:34 <AnMaster> yeah, maybe calling it "joke" was stretching things a bit ;P
18:20:41 <ehird> Mornington Crescent
18:20:46 <ehird> The purpose of this paper is not only self-citation (McBride, 2001; McBride & Paterson, 2006), ...
18:20:54 <ehird> (Yes, the abstract is actually "Mornington Crescent".)
18:22:02 <AnMaster> ehird, the language used, which one is it? haskell?
18:22:16 <AnMaster> some parts of it look quite similar at least from a quick glance
18:27:29 <ehird> Haskell with a few bits of do-what-i-mean.
18:27:53 <ehird> ⊥ would be an operator and thus not valid like that
18:28:04 <ehird> But it doesn't matter because it's a paper, not a program. :P
18:28:18 -!- MizardX- has joined.
18:28:26 <ehird> (And they don't actually, you know, define ⊥.)
18:30:45 -!- MizardX has quit (Ping timeout: 258 seconds).
18:30:46 -!- MizardX- has changed nick to MizardX.
18:31:15 -!- jcp has joined.
18:32:23 <augur> you're right, she forgot language
18:32:38 <augur> the lambek calculus was designed for grammatical structures.
18:34:54 <Gracenotes> augur returns to the discussion, just in time for me to wake up
18:39:09 <augur> ehird, i think you're naughtE
19:06:24 -!- sshc has joined.
19:07:24 * Sgeo wonders if ehird is going to read FS soon
19:10:55 <augur> im having an email convo with noam chomsky D:
19:20:22 <ehird> [18:32] <augur> you're right, she forgot language
19:21:00 <augur> ehird: misspiggy is not a boy.
19:21:11 <augur> and fax is a girl.
19:21:18 <ehird> i'm fairly sure i've heard otherwise
19:21:34 <Deewiant> If using a female nickname one should expect female pronouns.
19:21:42 <augur> well we'll ask just to confirm ;P
19:21:56 <augur> ehird: indeed, tho, yes. lambek calculus _is_ a theory of grammar.
19:22:22 <augur> "Joachim Lambek proposed the first noncommutative logic in his 1958 paper Mathematics of Sentence Structure to model the combinatory possibilities of the syntax of natural languages. His calculus has thus become one of the fundamental formalisms of computational linguistics."
19:22:23 -!- ehird has changed nick to alice.
19:22:37 -!- alice has changed nick to alise.
19:24:37 <alise> augur: what's your evidence that fax is a girl? my evidence that e is male is: one, probability; the vast majority of this channel is male - in fact, I believe there are no females currently in here, and a vague recollection of some sort of data meaning he was male, but my memory is terribly fuzzy when it comes to this place; so much talk, so little time.
19:24:47 <augur> my evidence is that she told me so.
19:25:11 <augur> i believe shes a transgirl, however, hence the potential confusion.
19:25:26 * Sgeo wonders how ehird will/would react to the RoboZZle addiction in here
19:26:05 <augur> or maybe transman? i have no clue about the details, honestly.
19:26:23 <augur> all i know is that fax/soupdragon/misspiggy is smart and interested in CS and linguistics
19:26:28 <augur> and therefore has become a good friend.
19:26:33 <augur> cheater3: WHOS YOU
19:26:37 <alise> hmm... i think we've had more transgirls here than cisgendered females
19:27:00 <augur> alise: you're a transgirl.
19:27:09 <augur> tho maybe not intentionally :X
19:27:16 <alise> my gender is 0.5 :P
19:27:33 <augur> ehird is genderqueer!
19:28:51 <alise> god programming languages are sexy :|
19:28:55 * augur makes out with himself
19:29:00 <alise> can i be typesexual
19:29:05 <cheater3> programming languages are transgender
19:29:17 <augur> only if you're into programming languages with strict typing
19:29:24 <augur> which ofcourse means lots of leather and whips
19:30:08 <alise> i think i'm going to stick with this name for a while, see how many people treat me differently because they think i have ovaries
19:30:57 <augur> but you're still ehird, and ovaries wont make you most spiteful
19:31:10 <alise> so I was thinking about what to call the empty type, right, and I thought hey, I could use ∅ *and* have it be used by sequence/collection/whatever. I just have to make Set (or Type or whatever) an instance of it! But that won't work, because there'll be operations like cons :: a -> sequence a -> sequence a which doesn't make sense because one, sets/types don't have element types
19:31:12 <cheater3> augur: do you have 'introduction to algorithms' 3 ed for me?
19:31:26 <alise> and two, they're not really a concrete collection of values
19:31:31 <alise> so I'm back to square one
19:31:53 <augur> alise: call it Empty. thats what the dependent type people call it.
19:31:57 <cheater3> i am looking for the book called what i just mentioned, augur
19:32:05 <augur> cheater3: ill try!
19:32:15 <alise> augur: I *am* a dependent type person!
19:32:22 <alise> augur: but I'm also a Unicode whore.
19:32:38 <augur> then use an epsilon
19:32:53 <augur> ∅ should be reserved for actual {}'s
19:33:07 <alise> right but epsilon is "arbitrarily small", not "length one"
19:33:11 <augur> ε is occasionally used for the empty string, but
19:33:12 <cheater3> augur: 2ed gives minus 50 points
19:33:33 <alise> augur: do you think ∅ is acceptable for any sequence, though?
19:33:48 <alise> lists, concrete sets (actual {}s, as you put it), associative maps, etc.
19:33:50 <augur> no, its not a sequence
19:33:59 <alise> but it's a convenient and pretty notation
19:34:44 <alise> what i want isn't "arbitrarily small"
19:34:52 <alise> epsilon isn't empty, it's arbitrarily small
19:35:08 <augur> well its the empty string in formal language theory!
19:35:10 <alise> relatedly, what should I call the unit type? maybe a circle
19:35:13 <augur> cheater3: i only have the second edition :(
19:35:24 <augur> cant find the 3rd edition anywhere
19:35:26 <alise> augur: don't get me wrong, I don't care about total mathematical notation faithfulness
19:35:29 <cheater3> augur: you don't want minus 50 points, do you?
19:35:30 <augur> alise: unit type should be a fancy 1
19:35:31 <alise> I just don't want it to *confuse* mathematicians
19:35:39 <alise> augur: find me a fancy one and it's done
19:35:46 <alise> augur: blackboard 1 would work, to fit in with sets like N
19:35:58 <augur> well lets see what unicode gives us
19:36:51 <alise> disregard ∷ ∀a. a → ○
19:37:55 <alise> that is not a rude gesture.
19:38:10 <augur> if i had one more finger it would be
19:38:11 <pikhq> ZAL҉̵̞̟̠̖̗̘̙̜̝͇̊̋̌̍̎̏̐̑̒̓̔̿̕̚͡ ̒̓̔̕̚GO he cometh.
19:38:27 <augur> i like the ring tho
19:38:58 <alise> ZAL҉̵̞̟̠̖̗̘̙̜̝͇̊̋̌̍̎̏̐̑̒̓̔̿̕̚͡ ̒̓̔̕̚GO is ta∵∵si∵∵
19:40:49 <augur> check it out, im writing in naboo-an!
19:41:01 <alise> ○ is nice because it's like () but without the tupley implications
19:41:04 <alise> because it isn't really tupley
19:41:18 <alise> main ∷ Partial (IO ○)
19:41:57 <alise> ⇄ would be a good unicode name for IO.
19:42:08 <cheater3> augur: i think it doesn't exist :(
19:42:10 <alise> main ∷ Partial (⇄ ○)
19:42:18 <alise> augur: your second-last line is just a boob.
19:42:26 <augur> cheater3: it does, published in like september last year or something
19:42:39 <cheater3> augur thats not the kind of exist that i meant
19:42:43 <augur> ⨴ can denote partial
19:43:12 <augur> its part of a circle!
19:43:14 <alise> multiplication sign in left half circle
19:43:25 <cheater3> why are you guys using squares all the time
19:43:32 <augur> we're using unicode
19:43:53 <alise> http://www.fileformat.info/info/unicode/char/25d6/index.htm
19:44:02 <pikhq> If it doesn't do Unicode, then it sucks balls.
19:44:03 <alise> cheater3: one, stop using windows
19:44:07 <cheater3> how do i make xchat use unicode more than it does already
19:44:08 <alise> three, set encoding to utf-8
19:46:37 <alise> i don't want to use _ for my multifix operator placeholder character
19:46:41 <alise> uh you may not know what multifix is
19:46:47 <alise> pikhq: multifix lets you define operators like this
19:47:17 <alise> _therefore_CHICKENPOX$_okay_okay
19:47:24 <alise> if poo then bar else lux
19:47:44 <alise> mints therefore (death is okay) CHICKENPOX$ whoa okay (2+2) okay
19:47:56 <pikhq> alise: So, even less special syntax.
19:48:17 <cheater3> pikhq: i would like to stand up to your expectations but i cannot. :(
19:48:19 <alise> pikhq: but I don't want to use _ for it because you should be able to use that in names
19:48:25 <alise> (Unicode is acceptable, even encouraged)
19:48:56 <pikhq> alise: Not sure; that's hard to pick...
19:49:44 <alise> i used the boob character, ⨀, but it just didn't really look very good
19:50:00 <alise> pikhq: Some sort of question mark would work
19:52:34 <cheater3> can you guys try those squares again pls
19:53:05 <Asztal> cheater3: you also need a good font or an IRC client that does font substitution properly
19:53:14 -!- gm|lap has joined.
19:53:29 <gm|lap> http://esolangs.org/wiki/RETURN <-- made an interpreter in python
19:53:45 <alise> looks like a holocaust
19:53:52 <alise> if BOOM then BOOM else BOOM
19:53:59 <gm|lap> i saw: interrobang, a/c, some weird p, some weirder H, Rs, 'a, 'o, 'i, 'u, 'e, mu.
19:54:01 <cheater3> Asztal: i am using xchat, is that not a good client for that?
19:54:13 <gm|lap> cheater3: try setting the encoding to UTF-8
19:54:13 <alise> what has ℀ got to do with anything?
19:54:24 <cheater3> gm|lap, Asztal: i tried doing /charset IRC and /charset UTF-8
19:54:34 <gm|lap> aww :/ i guess you might be lacking fonts then
19:54:47 <cheater3> where do i get unicode fontz for my windoze?
19:55:03 <gm|lap> idunno, all i can say is you can get them with linux
19:55:36 <gm|lap> i suggest you look at that python interpreter, the idea is really scary
19:56:17 <cheater3> Courier New – 2726 characters (3151 glyphs) in version 5.00
19:56:57 <gm|lap> heh... AFAIK X11 rips chars from other fonts
19:56:59 <Asztal> if you couldn't see áéíóú that's an indication that it's not a font issue
19:57:29 <gm|lap> if you couldn't see ☭ that's an indication that it's probably a capitalism issue
19:57:32 <alise> cheater3: stop using windows. :)
19:57:33 <cheater3> Asztal: but i could not see the 5 to the left of that
19:57:38 <pikhq> gm|lap: Yeah, X11 makes a best-effort to display everything, even if it is ugly as hell.
19:57:41 <cheater3> alise: stop being a transgirl :)
19:57:53 <alise> gm|lap: not on my usual baux
19:58:18 <gm|lap> alise: don't upgrade, pulseaudio in ubuntu 9.10 is extremely crappy
19:58:30 <gm|lap> i removed it with force
19:58:34 <gm|lap> ...actually, with apt-get remove
19:58:40 <alise> i like 9.10, but this isn't my machine
19:58:44 <gm|lap> also esound is broken too
19:58:45 <alise> it hasn't been upgraded only out of laziness
19:58:52 <gm|lap> my desktop runs freeBSD
19:59:11 <alise> normally i run os x, which you can criticise for many reasons but excellent display of unicode text is not one of them
19:59:11 <Sgeo> My desktop still runs 7.04
19:59:20 <gm|lap> tbh freebsd has the best sound system for unix ever: newpcm
19:59:38 <gm|lap> it's like multi-application OSS
20:00:04 <alise> gm|lap: we have that it's called ossv4
20:00:34 <gm|lap> i heard that was the one that was single-app-only... hmm
20:00:45 <gm|lap> there was one which did MIDI and one which did multi-app
20:01:05 <alise> ossv3, old oss, is single-app
20:01:10 <alise> ossv4, which is new and not in the kernel, isn't
20:01:14 <alise> unless i'm mistaken
20:01:21 <alise> (it's kernelspace just not in the mainline kernel)
20:03:30 <Sgeo> gm|lap, this isn't my desktop
20:03:37 <Sgeo> I rarely even use my desktop anymore
20:03:44 <Sgeo> Only when I want to get old files off of it
20:03:53 <cheater3> this is the slowest installer ever
20:03:59 <cheater3> microsoft word viewer 97 or something
20:04:07 <alise> pikhq: perhaps a solid middle dot would work
20:04:18 <cheater3> can you guys try the squares again
20:04:37 <alise> gm|lap: also, harddrive sizes are not a marketing conspiracy.
20:05:00 <cheater3> i see 5 squares and then 5 letters with diacrytics
20:05:14 <gm|lap> i reckon it's just being cheap
20:05:50 <alise> gm|lap: http://www.tarsnap.com/GB-why.html
20:05:59 -!- cheater3 has quit (Quit: Leaving).
20:06:03 <pikhq> cheater3: Don't even see interrobang?
20:06:16 <pikhq> I'd guess you don't get a gnaborretni, either.
20:06:33 <alise> G = 1000 is standard; you cannot change prefixes. the unit after a prefix cannot change a prefix; that is merely nonsensical. Furthermore, the decimal, standard version is in fact *more common* in computing than the binary one.
20:07:01 <alise> Ki/Gi/Ti are the standard binary prefixes; it should be RAM, which is the main exception to the decimal rule, whose marketing changes.
20:07:09 <gm|lap> we don't run 2.2GB processors, we run 2.2GHz.
20:07:24 <gm|lap> 1 Gbps Ethernet transmits data at... 10^9 bits per second < that's also stupid.
20:07:26 <alise> pikhq: Please LART gm|lap, for he believes that units change their prefixes.
20:07:39 <gm|lap> it was always 2^10 B for a KB
20:07:50 <gm|lap> The 2.4GHz band which wireless ethernet operates within lies... between 2.4 x 10^9 and 2.5 x 10^9 Hz <-- likewise, not a byte.
20:08:00 <pikhq> gm|lap: And it was fucking wrong.
20:08:12 <pikhq> Stop making things fucking wrong.
20:08:26 <gm|lap> stop making things so damn cheapass
20:08:30 <alise> complaining about hard-drive makers using SI prefixes is the wonderful domain of idiots who like to appear smarmy and pedantic without actually caring about being correct.
20:08:43 -!- kar8nga has quit (Remote host closed the connection).
20:08:46 <alise> gm|lap: I will quote from the page you apparently didn't read.
20:08:48 <alise> "Hard drive prices are determined almost entirely by competition between manufacturers, so if hard drives were labelled in GiB instead of being labelled in GB, we'd be paying the same number of dollars for the same number of bytes anyway — if this really was a global conspiracy, it would be one of the dumbest conspiracies ever."
20:09:09 <pikhq> gm|lap: I will agree with you in one thing, though -- hard drives should be labelled in GiB.
20:09:18 -!- cheater2 has joined.
20:09:26 <alise> Yes, because they should be SSDs.
20:09:29 <pikhq> However, that does not mean a gigabyte is 2^10 megabytes.
20:09:35 <pikhq> (or mebibytes, for that matter)
20:09:37 <alise> Which are flash memory, which is addressed in silicon, so you get powers of two.
20:09:47 <alise> SSDs: Sexually Satisfying Disk
20:10:00 <cheater2> i restarted xchat and it said the 30 day evaluation is over
20:10:14 <cheater2> i thought this was free open source software, wtf
20:10:20 <alise> It is, the Windows build isn't.
20:10:23 <alise> Use Silverex, or not Windows.
20:10:29 <cheater2> can you guys try some unicode again?
20:11:14 <gm|lap> http://silverex.net/news IIRC
20:11:28 <Sgeo> This laptop has to be at least 3 years old
20:11:40 <alise> http://www.silverex.org/news/ actually
20:11:48 <alise> cheater2: :'''''''''''''''''(
20:11:48 * Sgeo is using Silverex
20:12:11 <cheater2> Asztal: can you try some unicode for me please?
20:12:26 <alise> we should replace the ehird sighting in the topic with scarf sitings. anyone seen him recently?
20:13:19 -!- Pthing has quit (Remote host closed the connection).
20:17:21 <alise> http://www.fileformat.info/info/unicode/char/2237/index.htm
20:17:26 <alise> I wonder what it's actually supposed to b e
20:17:31 <alise> "proportion" is unhelpful
20:18:11 <alise> pikhq: annoyingly unicode messes with layout :(
20:18:26 <alise> because characters that display as >1 character are still treated as one character
20:18:32 <alise> (you can't fit *every* character into a tiny space)
20:18:35 <alise> (not without distortion)
20:18:46 <alise> the solution, of course, is non-textual editing! :P
20:25:56 -!- gm|lap has quit (Quit: 2 hour UPS expired. Shutting down laptop.).
20:26:27 -!- MissPiggy has joined.
20:28:05 <MissPiggy> just repartitioned and reinstalled my os
20:29:17 <alise> your solution to the expression problem, what if your type doesn't have any relevant dependicity? do you have to like put a dummy dependent thingy in to make it work?
20:29:39 <alise> I didn't really understand it so yeah
20:32:25 <alise> can you explain your solution to me
20:32:27 <alise> I didn't really grok it
20:33:43 <MissPiggy> dyld: unknown required load command 0x80000022
20:33:55 <alise> MissPiggy is an AI?!
20:34:12 <alise> MissPiggy: you're using OCaml and zsh on OS X.
20:34:19 <alise> i am so inferrerator
20:34:56 <MissPiggy> the idea is to make a data type a bit like this one:
20:35:15 <MissPiggy> data Snoc a where nil :: Snoc a ; cons :: Snoc a -> a -> Snoc a
20:35:45 <MissPiggy> data Snoc a where nil :: Snoc a ; snoc :: Snoc a -> a -> Snoc a
20:36:07 <MissPiggy> the difference, is that in snoc xs x, you let the type of x depend on xs
20:37:00 <MissPiggy> data Snoc f where ... ; snoc :: forall xs :: Snoc f, f xs -> Snoc f
20:37:21 <MissPiggy> if you let f = const a, then it's equivalent to the old one
20:37:40 <MissPiggy> but if you let f xs = Vector a (length xs),for example -- you get triangles
20:37:52 <alise> forall xs :: Snoc f, f xs -> Snoc f
20:37:53 <MissPiggy> my idea is to use this to make matrices instead of triangles
20:37:54 <alise> this notation confuses me
20:38:14 <MissPiggy> it's just (xs :: Snoc f) -> (x :: f xs) -> Snoc f
20:38:17 <alise> use haskell notation like you've been doing but with (name::t)-style dependent type notation plz :P
20:38:21 <alise> lemme write this out so far
20:39:01 -!- kar8nga has joined.
20:39:12 <MissPiggy> but don't worry about the type of f
20:39:21 <MissPiggy> it will probably become something else in the future
20:39:36 <alise> so it's not Snoc f a
20:39:57 <MissPiggy> yeah as I was writing Snoc f a I realized Snoc f subsumes it
20:40:22 <alise> data Snoc :: (Snoc f -> Set) -> Set where
20:40:26 <alise> cons :: (xs :: Snoc f) -> (x :: f xs) -> Snoc f
20:40:33 <alise> so, let me say this in words
20:40:56 <alise> cons takes a value of type Snoc f named xs, and a value of type (f xs) named x, and returns a Snoc f.
20:41:06 <alise> so f gets the rest of the list, and returns the relevant type
20:41:17 <alise> so Snoc (const t) = Oldsnoc t
20:41:30 <alise> I think I see how this is cool
20:41:35 <alise> It's a polymorphic list of sorts
20:41:41 <alise> except the type of the element depends on the rest of the list
20:42:25 <alise> If you can formulate a type meaning "the integer x", you could have snoc nil 1, snoc (snoc nil 1) 2, etc. type
20:42:32 <alise> so how does this solve the expression problem?
20:42:34 <MissPiggy> now what we could do is define something like
20:42:48 <MissPiggy> ROW <name> <vector of elements of this row>
20:42:57 <MissPiggy> COL <name> <vector of elements of this col>
20:43:23 <MissPiggy> so when you snoc a ROW on, it computes the number of elements you have to define, to add this row (and col similarly)
20:43:43 <MissPiggy> this way you can build up a NxM matrix starting from a 0x0 one
20:44:03 <MissPiggy> at a first approximation that matrix could just have numbers in it, or whatever -- it doesn't really matter
20:44:26 <MissPiggy> to solve the expression problem we will have to compute the type of the cell based on the function spec.
20:44:37 <MissPiggy> but that's just details, the important bit is SNOCing on ROWs, and COLs
20:48:20 <alise> okay so ROW and COL are data constructors
20:48:23 <alise> of the same type or not
20:48:34 <MissPiggy> yeah, I think that they have to be of the same type
20:48:46 <alise> ROW does not actually add rows
20:48:49 <alise> + func1 | func2 | ... Foo x y | y | x ... Bar x y | x | y ... +-----------------...
20:48:54 <alise> Foo x y | y | x ...
20:48:55 <alise> Bar x y | x | y ...
20:48:58 <alise> all Foos and all Bars are the same row
20:49:24 <alise> [20:43] <MissPiggy> so when you snoc a ROW on, it computes the number of elements you have to define, to add this row (and col similarly) i don't get what you mean by that
20:51:55 <alise> MissPiggy: I think an example would help, so
20:51:56 <alise> http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w
20:51:59 <alise> the unextended bit there
20:52:04 <alise> with Foo x y and Bar x y as the rows
20:52:07 <alise> and func1 and func2 as the columns
20:52:14 <alise> how would you write that, given your definitions?
20:52:29 <MissPiggy> suppose we wanted to define functions, eval, size and show on data Exp = Num Int | Add Exp Exp | Mul Exp Exp
20:53:05 <alise> can we use my example :P
20:53:11 <alise> not to be rude, it's just that i understand mine
20:53:14 <alise> since it's very simple
20:53:32 <alise> instead of getting bogged down in details etc
20:57:24 <alise> MissPiggy: think I should have inductively defined sets as in mathematical notation?
20:57:28 <alise> might be convenient, dunno
20:57:44 <MissPiggy> you start with the 0x0 matrix, [] `snoc` ROW "Num"*description of num () `snoc` Row "Add*description of add ()`snoc`COL eval (case for eval Num, case for eval Add)`snoc`ROW "Mul"*description of mul (case for eval Mul)`snoc`COL show (implementation of show for all 3 casese..)
20:57:51 <MissPiggy> read that sequentially and slowly :P
20:58:10 <MissPiggy> I think you can consider inductives as sets, but I don't
20:58:31 <MissPiggy> oh you said something else completely
20:58:38 <alise> yerr, i don't understand that :(
20:58:40 <MissPiggy> well you can implement set theory in type theory
20:58:48 <alise> what is it for Foo/Bar/func1/func2? :P
20:58:55 <alise> and what's a description
20:59:04 <alise> and er you have an unterminated string
20:59:09 <MissPiggy> it just says whwat the type of the constructor is
21:01:34 <MissPiggy> we dont' program over the real data Expr = ...
21:01:48 <MissPiggy> we are actually making a program over a generic sort of datatype called a universe
21:02:02 <MissPiggy> so U <description of Nat> is isomorphic to Nat
21:02:10 <MissPiggy> and U <descrption of Expr> is .... Expr
21:02:20 <alise> what is string * thing
21:02:22 <alise> what operator is that
21:02:31 <MissPiggy> oh I just meant that like a tuple yeah
21:02:39 <alise> thanks for inventing notation without telling me :/
21:02:55 <alise> description = type?
21:03:13 <alise> what's the resulting value
21:05:01 <alise> [20:57] <MissPiggy> you start with the 0x0 matrix, [] `snoc` ROW "Num"*description of num () `snoc` Row "Add*description of add ()`snoc`COL eval (case for eval Num, case for eval Add)`snoc`ROW "Mul"*description of mul (case for eval Mul)`snoc`COL show (implementation of show for all 3 casese..)
21:05:04 <alise> that line is what i'm referring to
21:05:22 <MissPiggy> I'm starting to realize that my idea takes quite a bit of background to understand..
21:05:43 <alise> Okay, so I've tried to write my Foo/Bar/func1/func2 example using your notation.
21:05:47 <MissPiggy> wait I have a great idea how to explain that
21:05:50 <alise> Row "Foo" (a -> a -> (exists b. b)) `snoc`
21:05:52 <alise> Row "Bar" (a -> a -> (exists b. b)) `snoc`
21:05:54 <alise> Col "func1" (\_ y -> y) (\x _ -> x) `snoc`
21:05:55 <alise> Col "func2" (\x _ -> x) (\_ y -> y)
21:06:15 <alise> Okay. Unfortunately, it doesn't allow adding rows.
21:06:25 <alise> If I add a row, and then call func1 or func2 on it, they don't work; they explode and break.
21:06:30 <alise> Because they don't handle the new type.
21:06:33 * Sgeo goes to mark 7000 or so conversations as read
21:06:46 <alise> In the OOP system, which can add rows, they inherit the definition (and you cannot remove fields, so they must work)
21:06:49 <MissPiggy> when you add a Row you must define one new case for func1 and func2
21:07:00 <MissPiggy> the reason you MUST do this, is because if you don't -- it will not typecheck
21:07:19 <alise> Row "Quux" blah (\_ _ z -> z) (\_ y z -> y+z)
21:07:23 <alise> func1 and func2 respectively
21:07:24 <MissPiggy> you can add N-rows and M-columns in any order, but at the end of the day you will have definede NxM cells of a matrix
21:07:45 <alise> it's a good solution, but i can't help thinking that it should really be a language feature, not something added on
21:07:49 <alise> this would be incredibly awkward to program in
21:07:51 * MissPiggy is compiling Coq to try and implement this
21:08:09 <MissPiggy> alise yeah it'll be awkward as fuck in Coq but I bet you could make easy as pi in epigram
21:08:25 <MissPiggy> (the epigram that isn't quite finished yet, epi 2)
21:08:47 <alise> the flexible operators might help make the syntax more bearable
21:09:08 <Sgeo> I have 16,163 messages in label "Agora"
21:09:22 <alise> I have two rabbits
21:09:38 <alise> (13530 conversations here, comprising more messages)
21:09:51 <alise> MissPiggy: rjg spg
21:09:56 <alise> well i look forward to your implementation
21:10:02 <alise> and i'm going to play around with this as a language feature now
21:10:46 <Sgeo> Well, when I said messages, I meant conversations >.>
21:13:05 <Sgeo> My Gmail account looks so clean now
21:14:38 <alise> MissPiggy: http://pastie.org/812719.txt?key=yvxcfkcsixjpvfijd5gug
21:14:41 <alise> It looks slick as a language feature
21:14:52 <Sgeo> Marking everything as read
21:15:41 * Sgeo goes to mark all 30398 conversations as unread for no good reason
21:15:44 <alise> http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq
21:15:48 <alise> MissPiggy: More consistent syntax
21:15:54 <MissPiggy> I guess the natural thing to do now is generalize it to infinite dimensions
21:16:04 <alise> What would that help? :P
21:16:23 <alise> MissPiggy: one thing I don't like is
21:16:34 <alise> if you have a function that's the composition of two columns, it doesn't need to be a column
21:16:39 <alise> in fact it shouldn't be
21:16:52 <alise> in functional programming you don't have to distinguish columnular and non-columnular functions
21:16:57 <alise> it seems a bit awkward to have to do so, in fact
21:17:21 <MissPiggy> suppose we defined t1 = []`snoc`... a bunch of stuff...
21:17:31 <MissPiggy> and t2 = t1`snoc`... some more stuff...
21:17:50 <alise> (note: in mine, since tables would be compile-time, they would "mutate")
21:17:54 <alise> (so no need to make new names)
21:18:13 <MissPiggy> so t1's type would express that it defines N-functions over some (M-constructor'd) datatype
21:18:22 <alise> MissPiggy: your system is a vulnerability
21:18:27 <MissPiggy> and t2 would define more functions over a data type that is an extension
21:18:44 <alise> you can define a new row, and when defining the columns for that row, put in some evil code that breaks the assumptions, and the abstraction, of code using the column
21:18:52 <MissPiggy> suppose that x is a value, and you wanted to apply it
21:18:55 <alise> just add constraints requiring proofs
21:19:07 <MissPiggy> you would need to PROJECT and EVALUATE the function out of the table
21:19:08 <alise> MissPiggy: apply it?
21:19:32 <alise> in mine, just f2 x
21:20:26 <MissPiggy> I don't think there is any vulnerability though
21:20:31 <alise> I do think http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq is remarkably elegant though
21:20:42 <alise> MissPiggy: not if you make sure you have constraints on the functions
21:20:49 <alise> like any good dependent programmer will
21:20:58 <alise> plus you'd have to inject code into the system anyway
21:21:00 <alise> and if you can do that, well...
21:21:17 <alise> maybe we've discovered the Nth major paradigm
21:21:24 <alise> table-oriented programming
21:21:28 <alise> (not to be confused with SQL :P)
21:22:30 * alise tries to translate http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq into Haskell, through whatever tricks necessary
21:22:44 <MissPiggy> haha I don't think you can turn that into haskell
21:22:56 <MissPiggy> this this good plugin for Coq I can try out
21:22:59 <alise> its type-system is TC with GHC extensions you know
21:23:13 -!- tombom has joined.
21:25:31 * MissPiggy doesn't know what a TC type system is for
21:25:47 <alise> Point is, it has type-level functions and a whole lot of other trickery.
21:25:52 <alise> It's everything apart from dependent, pretty much.
21:25:55 <MissPiggy> TC or not, it still doesn't have lambda
21:26:04 <MissPiggy> oh well you can do everything in SK
21:26:18 <pikhq> TC means it is equivalent to lambda in computational power, though.
21:26:33 <alise> MissPiggy: it does have lambda
21:26:37 <alise> you just have to define them elsewhere
21:26:41 <pikhq> And compiling lambda to SK is trivial. Annoying, but trivial...
21:26:41 <alise> okay, so it doesn't have lambda
21:26:46 <alise> but it has first-class functions (types)
21:31:54 <AnMaster> internet archive is really slow today it seems
21:32:38 <AnMaster> (theory: it takes as long to go back in time as it took to get to the current point from then originally)
21:33:14 -!- cheater2 has quit (Ping timeout: 252 seconds).
21:33:40 -!- cheater2 has joined.
21:35:06 <Sgeo> What good alternatives are there to C++?
21:35:57 <Sgeo> C-like alternatives, I mean. Not talking about Haskell here
21:36:17 <Sgeo> With OOP, preferably
21:36:57 <MissPiggy> a lot of people that got fed up with C++ because they couldn't push template metahacking it far enough moved to haskell
21:37:23 <alise> a lot of people that got fed up with Haskell because they couldn't push type-system metahacking it far enough moved to Epigram
21:38:45 <pikhq> Sgeo: C, Objective C, D...
21:39:00 <alise> the language with literally every feature
21:39:04 <pikhq> Objective C++ is a real thing.
21:39:15 <alise> AND SO IS OBJECTIVE D++
21:39:38 <pikhq> Just not implemented.
21:39:57 <alise> apple implement it
21:40:04 <alise> and so does gcc because of that
21:40:08 <Sgeo> Hm, I shoulld probably learn D
21:40:34 <alise> first of all, the toolchain situation is hopeless; really terribly hopeless. you have no idea how hard it is just to get a working D compiler. D2 with all the fancy features? Forget it.
21:40:41 <alise> It's been like this for years, and I mean years.
21:40:44 <alise> Secondly, it is not a designed language.
21:40:51 <alise> It is a pile of features, shat on each other.
21:45:01 * Sgeo wonders what it would be like to take a computer course where he's not guaranteed an A
21:45:40 <alise> Probably much like being in a different building.
21:48:14 <Sgeo> MissPiggy, I _think_ alise is saying I should switch schools in order to actually get challenging classes
21:48:51 <alise> Well, if you're basically guaranteed an A in every class you're either a really excellent programmer or in a bad school.
21:48:59 <alise> Or have done the classes before. :P
21:49:16 <alise> You may be a really excellent programmer, but the probabilities are weighted in the direction of bad school.
21:49:43 <Sgeo> I know the other students think I'm an excellent programmer..
21:49:44 <alise> MissPiggy: I'm getting the example translated, slowly
21:49:53 <alise> Sgeo: They could just be realy bad programmers, though. :P
21:49:59 <Sgeo> alise, I think that that's the case
21:50:02 <alise> I'm not dissing you, just being all probabilitying.
21:54:34 <alise> MissPiggy: do you have any idea how many times i've seen the word "kind mismatch" in the past few minutes
21:55:46 <Sgeo> Kinds are basically the type of tyoes? Maybe is * -> *?
21:56:50 <alise> {-# LANGUAGE KindSignatures, RankNTypes, GADTs, FlexibleContexts #-}
21:56:52 <alise> a sure sign of madness
22:04:09 * Sgeo tries to make a website that doesn't support Chrome work in Chrome
22:05:19 <Sgeo> Does Chrome not support getElementById?
22:07:59 <Sgeo> It looks like it should
22:08:06 <Sgeo> Some googling suggests it doesn't
22:09:03 <Sgeo> It's supported
22:10:26 <Sgeo> Does it have something to do with the fact that it's in a table?
22:11:45 <oklopol> Sgeo: my average in math is still A (called 5 here), recently thought i'd failed my first exam (apparently i just failed by my own standards), and it mostly felt nice to know the pressure to succeed every time was lifted.
22:12:26 <oklopol> i don't know if you actually wanna get A's, if you do, that might be relevant.
22:13:22 <alise> i think he means more "a programming class that isn't really easy"
22:13:52 <oklopol> yeah, probably, that's why i hastily added the second line :P
22:14:45 <oklopol> then it'd probably feel nice, since taking trivial courses feels is a waste of time
22:15:16 <oklopol> i should stop trying, i clearly haven't woken up yet
22:15:51 <Sgeo> They're trivial for me
22:15:58 <Sgeo> I don't know if they're trivial for most people
22:16:47 <oklopol> well i mean taking courses that are trivial for you is a waste of time.
22:17:13 <Sgeo> I do need to get a degree
22:17:38 <oklopol> i suppose, i prefer to live in the moment
22:18:05 <alise> a degree from a bad school sounds exciting
22:18:52 <alise> MissPiggy: btw if you separate classes from their methods, and make methods functions, you almost get the table solution
22:19:23 -!- coppro has joined.
22:21:16 <alise> well if you make a subclass you're not obligated to extend the previous functions to handle it unless you explicitly specify that
22:21:19 <alise> so you need to add that rule
22:21:44 <coppro> any particular reason?
22:22:29 <alise> I decided to see if people would treat me differently if they believed I had ovaries
22:22:41 <oklopol> i was like oooh want summa that
22:22:53 <oklopol> but then i realized you were a guy
22:22:57 <alise> since this is basically the only channel I go in and #haskell is very noisy, this is not such a successful experiment
22:23:01 <oklopol> after reading a few of your lines
22:23:13 <alise> MY TALKINGS ARE VERY FEMININE
22:23:25 <coppro> I don't think I behave any different towards women on the internet
22:23:48 <MissPiggy> this stupid client thinks // means /
22:24:09 <coppro> real life is a different story :P
22:25:29 <oklopol> i want to have sex with every girl i see both online and irl (necessary and sufficient condition for being male), but usually i only show it on irc, because as we all know it's really funny.
22:25:44 <alise> MissPiggy: do any existing dependent langs have isa :: a -> Set -> Bool
22:26:28 <coppro> oklopol: I suspect the LGBT community has some pitchforks ready for you
22:27:23 <oklopol> i've been known to raise people's pitchforks
22:29:32 <alise> MissPiggy: anyway do you think Complex :: Set; Complex = {_+i_ m n | m ← Real, n ← Real} is good notation for set construction?
22:29:45 <alise> data Complex :: Set where
22:29:48 <MissPiggy> alise I think isa is probably inconsistent
22:29:56 <alise> _+i_ :: Real -> Real -> Complex
22:30:00 <alise> is easier to understand
22:30:06 <alise> but it's also "specialer"
22:31:17 * coppro has chem homework... should probably do it
22:34:35 -!- alise has quit (Ping timeout: 248 seconds).
22:35:08 * MissPiggy should DEFINITELY do LOTS of work right now
22:35:23 <MissPiggy> hm this is not a very wise thing to do
22:37:21 -!- tombom has quit (Ping timeout: 260 seconds).
22:38:19 -!- oerjan has joined.
22:40:42 -!- Gregor has quit (Ping timeout: 258 seconds).
22:41:05 -!- madbr has joined.
22:41:56 -!- bsmntbombdood has quit (Read error: Operation timed out).
22:43:10 -!- Gregor has joined.
22:43:14 -!- ehird has joined.
22:43:17 <ehird> 14:30:09 <MissPiggy> that {} stuff is horrid
22:43:21 <ehird> 14:30:07 <coppro> _+_i?
22:43:25 <ehird> alas, both are ambiguous
22:43:29 -!- bsmntbombdood has joined.
22:43:30 <ehird> 3 +i 4 could be 3+(i 4)
22:43:42 <ehird> 3 + 4 i could be 3 + (4 i)
22:44:05 <coppro> then make i the Imaginary operator
22:44:08 <ehird> 14:29:48 <MissPiggy> alise I think isa is probably inconsistent
22:44:13 <ehird> it's just type checking
22:44:24 <ehird> 14:23:48 <MissPiggy> this stupid client thinks // means /
22:44:25 <coppro> _ + _ :: Real -> Imaginary -> Complex
22:44:29 <ehird> i didn't see it, my connection went wonky
22:44:49 <ehird> 14:23:25 <coppro> I don't think I behave any different towards women on the internet
22:44:56 <ehird> you probably do, sexism is incredibly ingrained in society.
22:46:12 <ehird> coppro: then again ambiguous operators are all the rage
22:46:17 <ehird> if_then_ plus if_then_else_
22:46:29 <ehird> (if x then y else z) could be (if x then (y else z))
22:46:32 <ehird> where else is a variable name
22:46:46 <ehird> not that if_then_ makes any sense without an else clause but still
22:47:12 <MissPiggy> ehird, oh nevermind, since it returns Bool it doesn't matter
22:47:15 <ehird> Deewiant: that's a name.
22:47:21 <ehird> MissPiggy: as opposed to?
22:47:24 <MissPiggy> if it gave some evidence then it might cause a problem
22:47:48 <ehird> yeah i was wondering whether to make it give evidence, decided against it
22:48:18 <ehird> _::_ :: a -> (a::Set) -> a
22:48:28 <ehird> MissPiggy: also I was thinking about:
22:48:40 <ehird> how to do quantification
22:48:53 <ehird> id :: {a::Set} -> a -> a
22:49:14 <ehird> id :: λ(a::Set). λ(_::a). a
22:49:19 <ehird> the last one isn't feasible unfortunately
22:49:23 <ehird> because you can't say λInteger.
22:49:26 <MissPiggy> use capital lambda instead of small lambda
22:51:10 <Sgeo> Why does a legitimate script feel a need to obfuscate its strings?
22:51:40 <Sgeo> I see no good reason to say "\x75n\x64\x65fined"
22:53:00 <ehird> Sgeo: filtering of something
22:55:40 <ehird> maybe undefined is filtered by something
22:58:29 <Sgeo> They do the same thing elsewhere in the code
22:58:32 <Sgeo> Including error strings
22:58:42 <Sgeo> "\x41jax\x20\x63allba\x63\x6b er\x72\157\x72\x3a s\x6f\x75rce\x20url n\x6ft foun\x64\041\x20\012\x0d\012\x0dPlea\x73e ver\x69fy i\x66 y\x6fu ar\x65 usi\x6eg an\x79 URL\x2drew\x72itin\x67 co\x64e a\x6ed s\x65t \x74he \x41jax\x55rl\x20pro\x70er\x74y t\x6f m\x61t\x63h\x20th\x65 U\x52L \x79ou\x20ne\x65d."
22:59:07 <ehird> I don't know; I'm not psychic.
22:59:33 <ehird> MissPiggy: so do you think quantified types should make the type of the function a type-level function from a set to a set, or have it be an implicit parameter of the function?
22:59:37 <ehird> probably the latter i guess
23:01:13 <ehird> id :: (a::Set) -> a -> a
23:02:32 <ehird> id :: {a::Set} -> a -> a
23:08:20 <coppro> [15:44:32]<ehird>you probably do, sexism is incredibly ingrained in society.
23:09:20 <oerjan> it's in your genes, pal
23:09:26 <coppro> I should clarify; I will treat someone I am familiar with differently depending on their personality, including sex and gender. By default, however, I don't make any attempt to distinguish between the two.
23:09:57 <coppro> I certainly treat women differently in person
23:13:09 <coppro> but unless I have a particular reason to do so, I don't associate gender with someone over the internet
23:13:20 <coppro> likewise for other traits, such as age and race
23:14:24 -!- sshc has quit (Quit: leaving).
23:14:27 <ehird> Right, but if you know someone's female you'll probably treat them differently.
23:15:01 <coppro> Depends on the context
23:19:21 <oklopol> i usually treat women differently because they are completely different
23:20:07 <oerjan> it's those venusian antennas
23:20:37 <oklopol> ISN'T IT THE GUYS WHO HAVE... nm
23:20:52 -!- kar8nga has quit (Remote host closed the connection).
23:21:41 <ehird> you know what annoys me
23:21:54 <ehird> the hardest part of doing lambda calculus and stuff is the variable renaming
23:21:58 <ehird> it's fucking bullshit
23:22:01 <ehird> nobody wants to rename variables
23:22:05 <ehird> stop using a shitty representation
23:22:49 * coppro ponders a bit of psychology
23:23:34 <oklopol> have i mentioned i just love wolframalpha?
23:23:38 <oerjan> that's just what you _think_
23:24:08 <oklopol> because i can write things like "integrate (-1/(e^(a-t+i*pi)-1)) with respect to t" and just know it understands what i mean
23:24:51 <oklopol> i don't think it's ever misinterpreted me, even though i just write like i would to a human
23:25:07 <coppro> It's misinterpreted me :(
23:25:10 <coppro> especially with set stuff
23:25:13 <oklopol> i'm not saying it's actually that great a parser, it's just others are incredibly stupid.
23:25:29 <oklopol> well i just use it for integrals, because i hate them (suck at them)
23:25:52 <oklopol> what kind of set stuff have you asked it?
23:26:23 <oerjan> hm i definitely had to rephrase things a bit when solving equations/graphing
23:27:25 <oklopol> (have you been doing math behind my back! :''()
23:28:11 <oklopol> fancy parser, then stick the result into mathematica, prolly
23:28:21 <oerjan> it was just something trivial about population growth
23:28:44 <ehird> it's 1.5 million lines of mathematica, so i assume it's just a list of hardcoded query * response pairs.
23:29:23 <oklopol> it's mostly the i and pi sort of simple stuff that i love i don't always have to explain to it, "(-1/(e^(a-t+ipi)-1))" works as well
23:30:15 <oklopol> oerjan: okay, that's fine then
23:31:08 -!- FireFly has quit (Quit: Leaving).
23:31:51 -!- BeholdMyGlory has quit (Remote host closed the connection).
23:34:27 * Sgeo seems to still have an active imagination
23:34:59 <oerjan> no that's not imagination. those raptors you see coming toward you are _real_.
23:37:19 <Sgeo> The worlds that I create in my head
23:37:34 <Sgeo> Although both the major one and this one have me as a major Mary Sue
23:37:56 <Sgeo> In the major one, I'm essentially God
23:38:02 <Sgeo> and in this recent one, I'm fighting God
23:39:09 <oerjan> stop stealing my ideas!
23:56:42 -!- MizardX has quit (Ping timeout: 248 seconds).
23:59:10 -!- gm|lap has joined.