00:00:21 i actually felt a brain context switch there, to programming mode 00:00:30 sorry i'm thick right now, tilize? 00:00:43 I just made the word up :) 00:00:50 -!- SimonRC has quit (Ping timeout: 246 seconds). 00:00:53 make tiled? :P 00:00:55 I mean to take a text "image" and render it with graphical images 00:01:09 like produce a graphical version of a Befunge program or something 00:01:26 okay 00:01:41 coppro, like showing code flow paths in colours? 00:02:53 i actually felt a brain cell switch there, to programming mode 00:02:57 all one of them? 00:03:11 umm context switch 00:03:12 not cell switch 00:03:22 but yeah, just one cell is all my programming magic 00:03:23 it's 00:03:24 quantum 00:03:25 that's how /I/ read (the first time) 00:03:26 AnMaster: no 00:03:30 it.s....... quantum! 00:03:35 -!- zzo38 has quit (Quit: Is Dungeons&Dragons turing complete? Actually, that isn't even a valid question). 00:03:42 lili 00:03:45 the basic version would just take a text and replace each character with an image 00:04:36 i think i'm obligated to inject some ehird into the discussion 00:04:49 that was the plan; we haven't had enough ehird lately 00:04:57 00:05:08 the basic version would just take a text and replace each character with an image <-- bitmap font rendering? 00:05:08 that's my quota 00:05:31 ehird, oh? so you love the ipad? 00:05:38 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 I hate it and want it to be my wife! 00:06:02 Anyway, I gotta go. Later folks. 00:06:03 AnMaster: that would be the basic principle, yeah 00:06:03 Good luck ehird :) 00:06:07 cpressey: Thank you. 00:06:10 ehird, hard to decide on it? 00:06:12 -!- cpressey has left (?). 00:06:24 AnMaster: Regular teenagers think they have issues with deciding on their sexuality. They should try being freedom-lovin' Apple fanboys. 00:06:38 coppro, wow what a great new invention! rendering text to a graphical image. Rather than sending it to a vt100 terminal unit 00:06:53 It's not new 00:06:54 you mean, actually render in *software*? 00:07:01 coppro, I was being sarcastic 00:07:02 ... 00:07:03 umm i'm required to inject some display nerdery into this subtopic 00:07:06 guys, it has an IPS screen 00:07:12 and it's so thin and light and handheld. IPS! 00:07:14 ok 00:07:18 back to more depressing things 00:07:31 * coppro knows of sexual troubles! 00:07:32 ehird, but it is too large to fit into a pocket 00:07:38 well 00:07:40 so's your mom 00:07:45 coppro: you and everyone else 00:07:50 join the club 00:07:55 receive t-shirt, etc. 00:08:00 unless you want: "is that an ipad in your pocket, or are you just extremely happy to see me?" 00:08:06 I've been a member for a long while now 00:08:07 lol 00:08:14 but that would be, um, ridiculous 00:08:14 -!- pikhq has quit (Read error: Connection reset by peer). 00:08:22 pretty sure I'm in a special division though 00:08:38 Thta's a reason I wear cargo pants 00:08:54 wait it costs $499? why don't i have one already 00:08:58 apart from it not being released and stuff 00:09:03 hah 00:09:13 i was expecting like, $799 00:12:12 could be a misprint. 00:12:29 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 ehird, but what use case does ipad fill 00:15:37 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 it has better video hardware 00:16:22 i'm not sure how useful the ported office suite will be though 00:16:25 with that keyboard 00:17:18 the plug-in one? 00:17:49 the onscreen one 00:17:51 ehird, hm 00:18:15 yeah, I don't expect that to be useful 00:18:18 it runs a subset of iphone apps too so it's a big games console 00:18:25 and fart sound maker 00:18:31 too big to thumb-type, and practically impossible to touch-type 00:19:19 i dunno, touch-typing could be practical 00:19:27 with the error-correction 00:19:27 I can't see it really being 00:19:33 i can almost do it on an iphone, it's just too small 00:19:57 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 it runs a subset of iphone apps too so it's a big games console <-- not full OS X apps?! 00:20:34 what the crap 00:20:38 AnMaster: >_< 00:20:42 American laptops: Full sized keyboard! Bigger keys instead of a full layout! Yay! 00:20:48 AnMaster: I said it's a big iPhone. I wasn't kidding. 00:20:54 coppro, ... 00:20:57 AnMaster: and i said i wouldn't argue with you this weekend 00:20:58 that stupid... 00:21:04 i lied 00:21:04 it has better video hardware 00:21:20 I'm just shocked at this vendor lockin 00:21:31 American laptops: Full sized keyboard! Bigger keys instead of a full layout! Yay! <-- hm? 00:21:31 * ehird grabs the popcorn 00:21:34 We're playing Vendor Lockin! 00:21:36 you mean, like most laptops? 00:21:41 The game where AnMaster calls EVERYTHING vendor lockin! 00:21:43 Wareya, having full sized main area? 00:21:47 24/7/365! 00:21:48 huh? 00:21:49 Don't miss it! 00:22:05 No, the whole thing's width is that of a standard IBM-style keyboard 00:22:12 seriously full sized 00:22:34 but it's just an enlarged version of a normal laptop keyboard 00:22:38 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:53 yes 00:22:57 some side keys are smaller, such as the F-keys 00:23:02 it's as big as a full keyboard 00:23:04 and alt/ctrl/win 00:23:16 but it has no numpad and the arrows are squashed under shift and enter 00:23:18 and the arrow keys are smaller and moved 00:23:25 Wareya, yes? 00:23:26 indeed 00:23:33 seems like a sane solution for a laptop 00:23:37 easy to adopt to 00:23:38 And it's the same size as a normal IBM-style desktop keyboard 00:23:45 hm? 00:23:46 yet it uses a laptop layout 00:23:52 Wareya, no mine isn't 00:23:55 mine is 00:23:58 due to the lack for a keypad on the side 00:23:58 I'm saying 00:24:02 it's a 15" laptop 00:24:09 so you couldn't fit keypad there 00:24:14 with full sized main key 00:24:18 main keys* 00:24:28 Wareya, still it makes it easy to switch between laptop and desktop 00:24:30 If can fit an IBM desktop keyboard on top of this laptop's keyboard 00:24:32 same key sizes for most keys 00:24:42 the keys are enlarged, but it has a laptop layout 00:24:50 I mean 00:25:10 well with the numeric keypad the desktop keyboard is wider than my laptop 00:25:16 well,* 00:25:27 -!- pikhq has joined. 00:25:32 for me they're the same 00:25:54 Instead of taking advantage of the space for a full kayboard layout, they squeezed in an engarged laptop layout. 00:25:56 Wareya, is that a 17" laptop? 00:26:12 I don't know measurements very well 00:26:29 Wareya, becuase having the same *key size* for the letter keys is useful 00:26:33 when you switch a lot 00:26:37 it avoids a LOT of annoyance 00:26:42 due to missed keys and such 00:26:47 -all- of this laptop's kays are super sized 00:26:48 it's retarded 00:26:55 Who is Wareya? 00:26:57 super sized from an IBM keyboard's size 00:26:57 Is he new? 00:27:00 relatively 00:27:04 Joined? 00:27:10 http://esolangs.org/wiki/User:Wareya 00:27:14 ehird, you know ais -> scarf btw? 00:27:33 yes, is that permanent? I doubt it 00:27:42 ehird, seems fairly permanent so far 00:27:47 as in, lasted several days 00:28:08 i'm gonna move to a country where i have to wear ais523 around my neck 00:28:17 eh? 00:28:26 cold country? 00:28:32 * Sgeo watches the joke woosh above AnMaster's head 00:28:43 Oh, or maybe it didn't 00:29:36 Sgeo, indeed, it is controlled airspace there 00:31:06 yes, otherwise all the jokes would crash together 00:31:15 and form some sort of horrible mutant joke of all of them combined 00:31:19 which you would then laugh at 00:31:23 like that one? 00:31:39 hehehe 00:33:39 so anyone want to come to norway with me and found an operating systems and programming languages research company 00:33:52 that sounds cool 00:33:54 I want to do that 00:34:28 joke sothoth 00:34:30 so do i :P 00:34:39 sothoth 00:34:42 the only problem is figuring out a way to be profitable! 00:34:44 freaking 00:34:49 I have to freaking read goddam 00:34:54 H P Lovecraft 00:35:01 is there a good version with lots of pictures?? 00:35:06 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:35:07 XD 00:35:08 chill 00:36:47 00:38:05 night ↓ 00:38:15 I'm not going to sleep now! 00:38:22 AnMaster: you're on top of sgeo 00:38:33 congratulations, you managed to turn #esoteric to the awkwardly homoerotic once more. 00:39:46 Esolangers are the only ones in that strange channel right niow 00:40:46 Which strange channel? 00:41:20 The tullinge one 00:41:33 It's just a channel for some area of Sweden. 00:41:54 best area there is 00:42:17 "tulling" means fool in norwegian. just saying. 00:43:00 tulling - turring, just saw that 00:44:16 "turring" means fool in norwegian with a ridiculous japanese accent. just saying. 00:44:26 Luftputefartøyet mitt er fullt av ål 00:44:27 Min svävare är full med ål 00:44:35 Ilmatyynyalukseni on täynnä ankeriaita 00:44:38 norweigan, swedish, finnish 00:44:39 who wins 00:45:38 swedish; it has three funny accents, the others just two 00:45:59 haha 00:46:20 swedish is not... rounded enough 00:46:23 it's too... tall 00:46:31 you can't imagine a pleasant gentleman speaking swedish 00:47:13 indeed. like elves, really. 00:47:32 Good day gentlemen, bork bork bork. 00:47:52 which elves? 00:48:07 the tall, arrogant obnoxious ones. 00:48:08 High fantasy elves or childhood fantasy elves? 00:48:11 okay 00:48:18 i welcome you to the pleasantness of the current moment. 00:48:30 I'm getting jumk food 00:48:34 junk* 00:48:37 i wish i had junk food 00:48:56 I'm walking to a store half a mile a way for... 00:49:05 a single bag of doritos, and a 2-liter of whatever 00:49:09 later 00:49:13 later 00:49:20 someone hug me 00:49:22 ! 00:49:23 no idea what doritos are, but they must be awesome 00:49:34 * MissPiggy hugs ehird 00:49:41 yay 00:49:45 doritos are corn crisp things 00:49:52 they're overprocessed, brand-name corn chips with cheese and spicing 00:49:54 you dip them in things 00:50:04 hugging guys is weird 00:50:09 I know too much about junk foor for a 130 lb teenager 00:50:23 * oklopol hugs still 00:50:24 food* 00:50:35 Wareya: http://www.airshipentertainment.com/growfcomic.php?date=20091101 00:50:53 I'll read it when I get back 00:51:09 14, 74 lbs representin' 00:51:15 i am light. light as a feather 00:51:21 also really short. 00:51:33 in fact my interior is 99% air. 00:51:39 0.99% helium 00:51:45 i'm like two and a half yous 00:51:52 well not exactly 00:52:26 ehird: maybe you could escape the uk in balloon form 00:52:50 i'd get a squeaky voice *and* escape 00:52:51 sounds good 00:53:14 it's like two horses with one giant hammer 00:53:18 better not fart while over the north sea, though 00:54:09 oh dear, second fart joke 00:54:44 -!- SimonRC has quit (Ping timeout: 246 seconds). 00:55:06 wait, there was another one? 00:55:30 i started doing this thing today where i do the french r thingie without voicing 00:55:39 makes breathing more fun 00:55:40 err 00:55:52 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 that's essentially the german ch, isn't it 00:56:35 i don't think it's supposed to roll that much 00:56:44 acch so 00:56:56 at least it rolls less audibly 00:57:00 i basically snore 00:57:08 -!- pikhq has joined. 00:57:17 like a helicopter 00:57:35 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:05:50 Hi, SimonRC. 01:08:37 -!- pikhq has joined. 01:09:20 -!- pikhq has quit (Read error: Connection reset by peer). 01:09:29 alright 01:11:28 that's pretty funny 01:13:54 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 My experience on the internet is like blurry tunnelvision 01:14:23 or so i assume, since i hadn't noticed it before 01:14:30 so I don't know this guy 01:14:45 -!- pikhq has quit (Read error: Connection reset by peer). 01:15:49 well the newer comic Girl Genius has won a good number of awards 01:18:12 I find it funny how it just loosely compared good/evil to roder and chaos 01:18:19 http://www.airshipentertainment.com/growfcomic.php?date=20091115 01:18:32 Well, entropy is the greatest evil in the universe. 01:19:12 In my opinion, order/chaos and good/evil are utterly seperate scales 01:19:44 well duh but isn't what that comic _says_ 01:20:11 It sounds like it's listing new names for the same things, to me. 01:20:21 Maybe because of my dialect, eh 01:20:39 and in d&d good/evil and law/chaos are the two fundamental axes 01:20:56 yeah 01:23:16 also i would say it's because we're all culturally impressed with associating good with light and law 01:23:34 even if we may not always agree consciously 01:23:51 On a really fundamental level, I guess you're right 01:24:16 but I do feel like that good and light are the same thing anyway, so 01:24:22 er, s/law/order/, or both 01:24:26 -!- pikhq has joined. 01:24:54 while the bat people are likely to disagree vehemently ;D 01:25:02 heh 01:32:35 i don't really see any connection between good and light 01:33:08 maybe you have been educated evil? 01:33:21 and do not understand the four simultaneous days? 01:33:30 ;) 01:33:46 i like being in the dark, dunno why 01:33:52 I've played plenty of jrpgs 01:34:02 I think that's where good=light and evil=darkness came from 01:34:06 for me 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 good night everybody, may i find dreams in my sleep. 02:01:03 -> 02:01:27 Sleep, perchance to quark. 02:02:34 "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 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 hmm, someone pinged me >7h ago 02:13:59 olsner, might have been me 02:14:08 I mentioned the language you were making 02:14:17 -!- pikhq has joined. 02:14:55 Sgeo: sweet, what were you saying? 02:15:06 I was asking what happened with it, I think 02:15:10 It should all be in the logs 02:15:18 meh, logs, bah 02:16:08 well, it's being developed, and I have an experimental implementation that should be reworked slightly to make it TC 02:16:16 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 and I may still decide to rebuild the middle-part of it 02:17:04 ehird, *shrug* it's your life, your decision 02:17:05 ehird: oh, ensadden me as early as possible so that I may not be worsely ensaddened in further future 02:17:17 *life story 02:17:44 ehird about to die or something? 02:18:03 Heh, no. 02:18:22 I know at least one thing and it's that I'm not that bad off. 02:18:55 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 Anyway, http://pastie.org/private/4oxpzgiywxbjobgrsa 02:19:13 (For perspective, since I'm not sure if you know or not, I'm 14.) 02:23:30 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 I think it's definitely better in some places. 02:23:48 after all, it's pretty much impossible to differentiate sane persons and insane persons claiming to be sane 02:23:58 thud. 02:24:04 ...or vice versa. 02:24:35 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 claiming to be insane? that's a sign of sanity if there ever was one :P 02:24:41 But they're not 02:30:00 I think these systems are (with good intentions) built to prevent either you or your parents from bailing you out 02:31:41 Yes. But I cannot forgive the people involved. 02:31:51 They still did these things unthinkingly. 02:33:59 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 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 Runs in the family, we're both perfectly healthy, no story there. 02:36:07 But, you know, if the junk science of BMI says I'm overweight, well howdy-doody, to hell with the facts 02:36:23 I think that I could use that drink 02:36:47 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 I think that it would make sense for me to be in your position, tbh 02:38:22 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 Sgeo: no, believe me it wouldn't 02:46:18 nobody would be helped by my position 02:46:29 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 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 ehird, my physical body, if not my mind, might be helped 02:47:00 I seriously don't eat enough 02:47:05 they don't seem to especially care about actually fixing things, just temporary "fixes" 02:47:16 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:28:31 Internet? Work? 04:28:31 Please? 04:33:15 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 Neat, I've got Internet. 04:35:43 "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 uorygl: No. It approaches the top asymptotically. 04:37:42 That's one side of the debate 04:39:44 Though I'm pretty sure it depends upon the geometry of the hill... 04:40:25 God dammit xkcd forums. 04:40:44 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 I'm pretty sure the infinitists are right. 04:41:23 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 uorygl: I'm pretty sure there's a limit in there, so yeah... 04:43:24 I hate chapstick. 04:43:33 -!- pikhq has quit (Read error: Connection reset by peer). 04:44:18 * Sgeo loves it 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 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:37:48 uh. super. 10:41:29 -!- Pthing has quit (Read error: Connection reset by peer). 10:42:04 "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 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 why do I feel like writing my own irc client suddenly 11:54:42 hello 11:57:13 hi 11:58:50 are you identi.ca user? 11:59:13 no idea what that site is 11:59:55 is the free as in freedom twitter 12:00:36 look: http://identi.ca/group/conspiracy 12:00:50 -!- Pthing has joined. 12:01:05 verangirl, mhm, you know this channel is about esoteric programming languages right? Not about esoterica. 12:01:20 Sometimes people mistake this channel for the other thing 12:02:29 hum, ok 12:03:42 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:03 than see you 12:07:04 -!- verangirl has left (?). 12:19:01 Bwuh? Why did Chrome spontaneously decide to reload a bunch of tabs? 12:19:11 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 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 04:20:41 i wonder if there actually is a channel for magick weenies 13:07:42 ##php 13:07:52 hilarity 13:07:57 oblivious to how things work, merely trading magic incantations that appear, on the surface, to do what they desire 13:08:42 also 23:33:37 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 "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:42:32 hi MissPiggy. 13:42:42 hey 13:43:39 MissPiggy: agda question - it's tc but total, right? how does it handle that; that partiality monad? 13:44:28 well it is total 13:44:41 is it not tc, then? 13:45:12 but you can express every partial function N -> N using a data type 13:45:22 ehird, interesting, but what is the context? 13:45:24 or you could build a model of lambda calculus using a partiality monad 13:45:30 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:31 thingy 13:45:36 easy 13:45:37 (of that quote above) 13:45:45 AnMaster: http://bertrandmeyer.com/2010/02/06/reflexivity-and-other-pillars-of-civilization/ 13:45:51 (bertrand meyer = creator of Eiffel) 13:45:58 hmm i said bertrant before 13:45:59 *Bertrand 13:47:05 the function space A -> B (or forall a : A, B, or whatever) cannot express every recursive function 13:47:25 because -> is total functions (because you want to compute with them in types) 13:47:31 right 13:47:33 hmm 13:47:43 but e.g. A -> Computation B can be a model of lambda calculus 13:47:44 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 right, so a partiality monad 13:48:15 well you can define all the primitive recursive stuff and Mu, just as a syntax first 13:48:27 then you can give a big step semantics, 13:48:35 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 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 your Computation there is a partiality monad, isn't it? 13:49:53 so presumably to make meaningful use of them, given a haskell-style main program solution, you need main :: Partial (IO ()) 13:49:54 yeah that's just one way 13:50:08 otherwise you'd be in total-land, and couldn't invoke the forbidden fruit of the partial lands 13:52:40 my lambda syntax is currently λα.β because otherwise function types would get confusing :) (λα. α → ∅) vs (λα → α → ∅) 13:52:54 (fuck yeah, unicode; i'm using unicode up the wazoo) 13:53:15 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:53:18 yeah \x -> m is stupid 13:53:51 hmm, wait 13:53:55 ∅ is Void 13:53:56 not () 13:54:55 MissPiggy: come up with a nice unicode name for my () set :P 13:55:07 I wouldn't worry about writing partial programs 13:55:37 although that is just me .. 13:55:43 so maybe not such a valuable statement 13:55:47 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 why do you want to write an OS with it? 13:56:32 I dunno. I love the proof system duality and the mathematical soundness of having no ⊥, 13:56:40 but I'm not sure totality is practical. 13:56:52 hurrump 13:57:08 MissPiggy: My goal in computing is to completely revolutionise it. My two separate interests are operating systems and programming languages. 13:57:19 It is only natural that my awesome programming language would be my awesome operating system. 13:57:33 Note "be", not "be used to write". 13:57:46 alright but you're not going to do a full correctness proof of the OS? 13:57:51 My OS design involves the programming language being central; a living environment. 13:57:53 Think Smalltalk. 13:58:05 MissPiggy: Yes, well. :P 13:58:07 have you talked to luqui about thsi 13:58:20 luqui's blog was a big inspiration 13:58:26 but i haven't caught him on irc yet 13:58:53 heh I could use ∈ instead of ∷ 13:58:55 that's ugly though 13:59:12 the thing about \in is that it's asymmetric 13:59:34 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 ⊥ would be the type theory way; ∅ the set theory way... 14:00:24 ∅ seems less confusing; ⊥ is too associated with non-termination and undefinedness in programming 14:00:42 in haskell* :P 14:00:42 then again, I'd like to be able to use ∅ to denote empty containers in value-land, and that would be doubly confusing 14:00:51 nobody else has a clue what it is 14:01:08 well, whatever; apart from agda guys, haskellers are the most mathematically civilised programmers :) 14:01:15 (and coq etc) 14:02:28 The joys of Unicode: /=? Why wouldn't you just write ≢? 14:03:42 I was thinking about a language that could compile into almost every high level language 14:03:52 ehird, see my memo to you 14:03:56 ≢ because you have to use ≡ for equality 14:04:01 because = is definition 14:04:07 MissPiggy: underlambda :P 14:04:42 Sgeo: relink the paste in /msg; it may not be so bad 14:04:52 I have after all linked to the pastie which tells everything in this channel 14:05:21 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:31 := for definition 14:05:41 = for the equality type! 14:05:48 then yuo can say x = y and MEAN IT 14:06:06 := isn't unicode bitchnizzle 14:06:13 there's a unicode one :P 14:06:21 FIND IT PEASANT 14:06:52 ≝ 14:06:57 * ehird considers that |α| instead of abs α may be taking the mathematical notation thing a *bit* too far 14:07:10 |a| is a fucking abomination 14:07:13 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 MissPiggy: yeah agreed 14:07:18 |a|b|c| 14:07:19 retarded notation 14:07:26 ≔ 14:07:40 maybe that reduction symbol that rconnor likes 14:07:51 yeah I'm not keen on the unicode stuff because all the operators are too small (unnecessarily :/) 14:07:54 mathematical notation defines too much syntax when functions would do :/ 14:08:02 MissPiggy: yeah I'm taking care not to use any blots of ink 14:08:14 also, _my_ OS will display it perfectly legibly ;) 14:08:18 hehe 14:08:27 http://r6.ca/blog/20031202T032200Z.html 14:08:36 β* 14:08:41 we have our definition symbol. 14:09:08 ||a||₂ for the euclidean norm. 14:09:21 I draw the line at superscript numbers for powers 14:09:39 fizzie: yes, the stupid symbol is used for all norms 14:10:05 Okay, okay, so any fancy space-age editor, like my OS, will *display* it as superscripts. 14:10:17 But in the Unicode representation? 14:10:19 Nooooooooooooooooooooooo way 14:11:01 (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:05 s/$/)/ 14:11:22 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:11:42 wow lol 14:12:00 * ehird wonders what the best symbol for the exponentation operator is 14:13:39 -!- SimonRC has joined. 14:14:37 maybe ↑ due to knuth :) 14:14:47 http://www.reddit.com/r/math/comments/axd4m/what_is_the_mathematical_rule_that_says_if_abc/c0jw2vc 14:14:48 wut 14:15:18 anyone who answers a question starting "What is the mathematical rule" with "common sense" is so idiotic I cannot comphrend it 14:15:44 1+1=2 is common sense! 14:15:54 http://us.metamath.org/mpegif/2p2e4.html 14:15:57 a^2+b^2=c^2 because duh!! 14:15:57 i love metamath 14:16:07 yeah it's so 80s 14:16:15 howso 14:16:24 hey guys I just had a great idea, lets put all our math in the computer! 14:16:34 says the agda fan 14:16:47 epigram fan 14:16:55 why don't you like metamath? 14:17:04 I do like it, it's just very funny 14:17:07 aight 14:17:11 i misinterpreted what you said 14:18:18 foo α β = (α ≡ β) ∨ (α ≢ β) 14:18:57 ⊕ ∷ Bool → Bool → Bool 14:18:59 AND JUST WHY NOT 14:19:14 hmm ≡ is sometimes used for definition? 14:19:17 maybe i could swap =/≡ 14:19:21 or definitional equality 14:19:26 oh or ≐ is a nice unicodey thing for := 14:19:34 not at all ridiculous like ≝ 14:19:47 like y + x = x + y, but not definitionally 14:19:52 you need induction to prove it 14:20:49 * ehird wonders if he's crazy enough to do ÷ ∷ Boringtypeclasstypethingy → Anotherone → Maybe Yetanotherone 14:21:17 Yesiree we have a mathematical programming language here, please ignore the endless handling of ÷'s return values behind the curtain 14:21:32 * ehird decides yes 14:21:36 I am crazy enough. 14:21:50 I just need nice syntax for doing things like this in expressions. 14:22:51 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 given some surrounding brackets to denote that it's a special expression thingy ofc 14:23:09 that way you could use the maybe monad 14:23:27 MissPiggy: So, do you think ≡ is a reasonable symbol for what-Haskell-calls (to avoid ambiguity) =? 14:23:29 why you would want to?? 14:23:36 no I don't 14:23:40 kay 14:23:48 also, 14:23:58 for one, Maybe handling 14:24:14 2 + {3 ÷ x} 14:24:20 hahahaha ÷ 14:24:22 yes! 14:24:26 nice 14:24:34 oh 14:24:43 "... enough to do ÷ ∷ Boringtypeclasstypethingy..." 14:24:46 I read that as a + :( 14:24:52 lol 14:25:02 + ÷ = ≢ ≝ 14:25:07 anyway, {| 2 + {3 ÷ x} |} is nicer to write than fmap (2 +) (3 ÷ x) 14:25:37 a downside is that imperative weenies could do {| say {readLine} |} :P 14:25:49 but i guess it's just a generalisation of >>= and =<< and <$> and blah blah blah 14:25:50 lol 14:26:00 idiom brackets 14:26:02 ehird, Hm is ÷ fraction, integer division, floating point division or something else? 14:26:08 yeah i suspected idiom brackets were the same thing 14:26:14 AnMaster: Yes. 14:26:28 ah all of them then 14:26:30 ah,* 14:26:44 Well, not all of "something else". You have to obey some properties, or the compiler will yell at you. 14:26:54 well of course 14:27:21 Not really "of cause"; almost all languages don't do such things. 14:27:28 You can define (/) to be pretty much whatever you want in Haskell. 14:27:31 "of cause"? 14:27:34 *course 14:27:38 ah 14:27:42 ehird, but is the result of ÷ exact or not? 14:28:07 It depends on the definition doesn't it? 14:28:47 ehird, yes indeed, which is what my first question about it tried to ascertain. 14:28:59 I'll probably require that {| α × {β ÷ α} ≡ β |}, so... 14:29:16 (Using ≡ as equality, though that symbol is very much in flux.) 14:29:46 then it can not produce a "simple" floating point value when dividing two floating point values I think. 14:29:52 though, I'm not 100% sure about that 14:30:45 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 >>> (3231.318478239 / 238914.12391) * 238914.12391 14:31:08 3231.3184782389999 14:31:22 I love how my λ is the same thing as ∀. 14:31:25 It makes me feel warm and fuzzy. 14:31:36 AnMaster: I might have a separate class for inexact operations. 14:31:58 ÷?, maybe. 14:32:01 epigram has quotient types 14:32:16 so you could quotient out by "someEqualityThingProvidedByTheDefinition" and still use {| α × {β ÷ α} ≡ β |} 14:32:45 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 so that allows inexact definitions but still doesn't let you define it to anything you want? How? 14:32:52 so haskal? 14:32:57 AnMaster: Yes, I know. 14:33:07 right 14:33:11 by the way 14:33:14 in numerics 14:33:22 AnMaster: Floating-point operations don't obey the laws of arithmetic, though. :) 14:33:24 we get something like fl : R -> R defined 14:33:28 hmm 14:33:31 maybe you could use Real 14:33:38 and specify the inexact implementation as an "implementation detail" 14:33:39 and you write x + y*z would compute to fl(x + fl(x*z)) 14:33:45 ehird, true. So what you want is basically a CASkell? 14:33:46 where fl does the rounding etc 14:33:47 i.e., the code is considered to operate on reals in all their exactness 14:33:53 CASkell! lol 14:33:53 AnMaster: no. 14:33:55 awesome 14:33:59 but at runtime 14:34:01 that's a good name though 14:34:04 it uses floating-point 14:34:05 AnMaster: yeah 14:34:07 erm 14:34:07 MissPiggy: yeah 14:34:13 i smiled at the name. 14:35:39 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 it occurs to me that "e" is a rather inconvenient name to give e, given the commonality of single-letter variable names... 14:35:56 AnMaster: heh 14:36:04 it's correct for sufficiently large values of zero 14:36:34 i'd call e "euler", but euler has done so many mathematical things that it would be hopelessly vague :P 14:36:37 hm? representing numbers as the length of a series of zeros? 14:36:57 like if an idiot was working with the Euler–Mascheroni constant he'd be confused. 14:37:02 AnMaster: It's a joke. 14:37:36 in a mathematical context e means exp(1) 14:37:45 in a monad context + means mplus 14:37:45 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 well actually I prefer (+) for mplus 14:38:01 MissPiggy: + for mplus would be interesting. 14:38:08 might have been ais/scarf 14:38:19 I'm already sold on o (too lazy to unicode) = category composition 14:38:27 which is even generaler than o = fmap, i think 14:38:39 hmm 14:38:48 fmap and o are quite different thuogh 14:38:54 and I think o is better 14:39:02 fmap should just be map 14:39:02 hmm 14:39:06 (.) :: cat b c -> cat a b -> cat a c 14:39:08 --control.category 14:39:10 yeah 14:39:10 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:13 that seems good 14:39:14 ok, that doesn't allow . = fmap 14:39:16 but that's good i think 14:39:20 i think you're right 14:40:09 the supereditor will probably display α ÷ β as 14:40:13 α 14:40:13 - 14:40:14 β 14:40:15 :) 14:40:42 although at the same time I don't think I want to abandon the entirety of linear syntax 14:40:44 it has useful properties 14:40:51 (not necessarily textual, but linera) 14:40:53 *linear 14:41:11 also, consistency is Good, and also something mathematical notation sorely lacks 14:41:29 MissPiggy: any good ideas for the hole character in mixfix operators? 14:41:37 I don't want to use _, it should be allowed in variable names I think 14:41:38 mixfix? boo!!! 14:41:42 (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 [14:33] and you write x + y*z would compute to fl(x + fl(x*z)) 14:41:51 i like that 14:41:53 why I hate mixfix is: 14:41:54 ehird, what about that way to explain why e is a good name for e? 14:42:03 basically the same thing as what i was saying 14:42:13 AnMaster: yes, but in programming "e" is not an uncommon variable name 14:42:20 so having "e" in global scope is problematic 14:42:22 MissPiggy: I'm listening 14:42:24 ehird, true. 14:42:28 but i love mixfix so it better be a good argument :P 14:42:34 ehird, you could use namespaces/module prefixes 14:42:41 so you have like math:e or such 14:42:51 AnMaster: and if you're writing mathematical code? 14:42:53 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 Presumably you envelop all of math. 14:43:05 ehird, import it? like "from math import e" 14:43:05 And you run into the same problem, although I guess mathematicians wouldn't name variables e because of that. 14:43:13 the type of t depends on T, so in mixfix you can't do it.. you have to write T ::' t 14:43:17 (psedo-python) 14:43:22 pseudo* 14:43:49 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 mixfix operators being typed is the problem really 14:44:07 yeah if you just make them notations, rather than well typed terms I think it's better 14:44:19 I didn't know they were terms in Agda or whatever 14:44:23 if they are I don't see why 14:44:41 welll when you compute it will print back the mixfix terms 14:44:53 rather than something horrid like Ap (Ap (Dollar ..) (Ap .. 14:44:58 that we're so used to seeing. 14:45:03 so it's basically prettyprinting? 14:45:14 if they are just notations then it's a bit harder to make the link, I guess 14:45:14 also, you may be used to seeing it but I observe agda from a strictly outside viewpoint! ha! 14:45:27 :p 14:45:28 MissPiggy: seems ridiculous to add such craziness just for prettyprinting 14:45:33 make a smarter pretty-printer! 14:45:41 but not too smart! 14:45:51 Unless you make sure it's Friendly! 14:45:55 lol 14:45:56 yeah 14:46:22 ehird you know I have read so muh lesswrong 14:46:24 much* 14:46:27 yeah i prettyprinted my expression that (given infinite time) checked if the reimann hypothesis was true or false 14:46:35 it printed "the Boolean *£($&(*£$uq))(ii!£()!*£)(*NO CARRIER 14:46:41 :D 14:46:48 -!- ehird has left (?). 14:47:19 -!- ehird has joined. 14:47:22 Phew, my connection dropped there. 14:47:32 ehird, easy to explain 14:47:37 you said "no carrier" ;P 14:47:49 i'm still trying to come up with some sort of high-level esolang... can't come up with anything implementable :-/ 14:47:53 clearly _something_ listened 14:48:09 lieuwe you came up with unimplementable stuff? :) 14:48:11 AnMaster: Was that a pun? A carrier carries something, if a carrier stops carrying something they drop it? 14:48:15 If so, I love you. 14:48:21 You have made an actually good pun. 14:48:24 Congratulations. 14:48:24 lol 14:48:33 MissPiggy: not toataly unimplementable, just very hard... 14:49:00 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 sounds like the compiler for my language 14:49:13 "yeah, in fact it's technically implementable!" 14:49:31 should hire a buncha phds to do it for me 14:49:35 AnMaster: So not a good pun then :( 14:50:15 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 ehird, My variant seems more relevant to any sort of connection over telephony. 14:50:33 ehird you could just steal Coqs module system 14:50:42 I have no idea about modules though 14:50:45 MissPiggy: i might, is it as good as ml's? :P 14:51:02 well I think it's basically the same, except a bit extra for the types 14:51:13 ehird, and iirc you have iphone or adsl to choose from. 14:51:52 or 3g stick :P 14:51:58 well true 14:52:07 still a carrier there 14:52:34 and if you use that or the iphone then it is carrier in several meanings 14:53:07 -!- kar8nga has joined. 14:53:16 data [_] ∷ Set → Set where 14:53:18 ∅ ∷ λα. [α] 14:53:20 _:_ ∷ λα. α → [α] → [α] 14:53:29 ehird, but primarily see http://en.wikipedia.org/wiki/NO_CARRIER 14:53:31 where _ is the operator placeholder thingy 14:53:43 Yeah, yeah, so in actuality those names are in the Container or Sequence or whatever thingy. 14:53:43 why not epsilon? 14:53:51 also PUKE!!!!!! 14:53:56 And yes, overloading ∅ to mean something other than the empty *set* is probably abhorrent. 14:53:58 use : for type judgements and :: for cons :P 14:53:59 BUT I LIKE UNICODE. 14:54:06 epsilon is unicode!! 14:54:09 MissPiggy: I don't use :: for type judgements, I use ∷ 14:54:12 I just didn't look it up 14:54:15 AnMaster: I know what no carrior is 14:54:17 *carrier 14:54:20 that's why i said it 14:54:20 ehird, right 14:54:22 yeah well ∷ sucks ;[ 14:54:36 MissPiggy: i don't even know what it's supposed to be :) 14:54:44 anyway : for type judgements just seems too... lightweight 14:54:52 i dunno why, it just seems like the meat is taken out from the expression 14:55:10 maybe I shhould use ∈ for type judgements :P 14:56:03 yeah ∈ is better than :: 14:56:09 or ∷ whatever 14:56:10 looks ugly to me :P 14:56:13 what's wrong with :: 14:56:21 it atkes TWICE as long to type 14:56:26 >_< 14:56:27 believe me it adds up 14:56:36 it is the single most common operator you type 14:56:41 MissPiggy: wtf's up with the greek letters:-p? 14:56:43 no, = is 14:56:45 ∈ and :: mean different things, no? 14:56:52 lieuwe: we're being pretentious functional programmers 14:56:53 AnMaster: no 14:57:01 is-member-of-set = is-of-type 14:57:02 ehird: :P 14:57:10 MissPiggy: = is more common than :: 14:57:14 think e.g. let and where 14:57:18 where often you omit the types 14:57:26 but :: outside of a definition isn't very common 14:57:30 ehird, but hm 14:57:31 so = is definitely more common than :: 14:57:33 ehird, hm seems wrong to use the same symbol for them somehow 14:57:38 AnMaster: They are the same thing. 14:57:48 nevertheless... 14:57:51 but meh 14:57:53 You're saying the same thing as "it seems wrong to use the same symbol for addition and addition". 14:58:19 yes, there should be different symbols for integer and floating point addition 14:58:22 and so on 14:58:24 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 AnMaster: But those are different things. 14:58:43 You don't seem to understand: "Type" is just another word for "set". 14:58:43 true 14:58:58 ehird, depends on what set theory and/or type theory you use iirc? 14:59:06 types aren't really sets though 14:59:17 we just call them that and use ∈ because we don't like set theory 14:59:30 is ℕ not a set? 14:59:42 well it's an inductively defined set 14:59:47 i.e. a set 14:59:49 ehird, ℕ is the set of natural numbers yes 14:59:51 but it's not made up of {}'s 14:59:59 No, but it's a set. 15:01:23 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 bloody haskell doesn't have to avoid naming conflicts between value- and type-land :P 15:02:01 oh yeah 15:02:32 operators just break up the monotony of f (g x y) (h z (w p q)) 15:02:49 g x y + h z (p * q) 15:02:50 i suggest we call using non-operator names for functions 9-to-5 naming 15:03:03 MissPiggy: *× 15:03:12 p × q 15:03:16 I love that x 15:03:17 or · 15:03:19 your choice 15:03:25 x × x 15:03:33 unicode needs italics-x as a character :P 15:03:55 ehird, the cross product of x and x? 15:04:11 iirc × and · are quite different 15:04:13 Heard of multiplication, AnMaster? 15:04:34 ehird, yes but isn't cross product and dot product different for vectors? 15:04:54 two different kinds of product 15:05:09 Well, true. 15:05:38 * ehird wonders what fun category-theory concept × should be defined to 15:05:44 There's gotta be something, there's always something. 15:06:05 * MissPiggy doesn't even know what category theory does... 15:07:02 It doesn't do anything! It sits around looking awesome. 15:07:21 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 cosmic usefulness transfer 15:07:35 ah 15:07:41 curry-howard-lambek 15:08:05 a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. 15:08:37 you forgot linguistics 15:08:55 ??? 15:08:57 what 15:09:03 linguistics is isomorphic to logic, thus to programming 15:09:07 ho 15:09:08 how 15:09:11 dunno ask augur 15:09:15 is forgetting linguistics worse than forgetting poland? 15:09:16 tell me!!! 15:09:21 also they, well augur, also i think i've seen you, use basically lambda calculus for some syntax :P 15:09:28 also, I take it you mean semantics 15:09:31 Gracenotes: i had to restrain myself not to say that 15:09:33 yeah semantics whatever 15:09:34 i'm no linguer 15:09:43 no no don't do it. We won't get rid of the linguistics discussion for hours then! :( 15:09:57 uh oh 15:10:06 quick, what's the one thing that can distract augur from linguistics 15:10:07 AH! 15:10:10 Gay sex! 15:10:17 QUICK EVERYONE, TO THE BUTT-BATALLIONS 15:10:20 argh 15:11:18 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 oklopol: that also works to kill the linguistics. 15:11:53 argh i should have said "buttallions" 15:14:06 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 called bijection for functions ofc 15:14:35 i have to pizza maybe 15:14:56 would be nice to have a formal theory about these informationy heuristics we use 15:16:34 i did data Bijection a b = Bijection (a -> b) (b -> a) in haskell but i was sad 15:16:43 because you couldn't, you know, show that it was actually... that 15:17:15 in awesome languages I could just include an (f (g x) = x) :P 15:18:56 hey 15:18:59 is that a Category, I wonder? 15:19:18 (.) :: cat b c -> cat a b -> cat a c 15:19:43 so ((b->c),(c->b)) -> ((a->b),(b->a)) -> ((a->c),(c->a)) 15:20:02 yes it is 15:20:11 (Category as in the haskell definition of it in base) 15:20:22 that's pretty slick. 15:20:45 * MissPiggy still doesn't see the point 15:20:50 MissPiggy: it's cool? 15:20:53 so you have a category of bijections, now what?? 15:21:00 now you can compose bijections! 15:21:41 hey wait 15:21:47 I don't even need to require that they be functions 15:21:49 no wait, I do 15:21:52 I need a way to apply them 15:21:55 was thinking I could just do categories 15:22:00 waiiit 15:22:01 I could 15:22:09 no 15:22:10 I couldn't 15:22:10 kay 15:24:03 data Bijection ∷ Set → Set → Set where 15:24:05 Bijection ∷ λα. λβ. 15:24:07 {f ∷ α → β} → 15:24:09 {g ∷ β → α} → 15:24:11 {λx. f (g x) ≡ x} → 15:24:13 {λx. g (f x) ≡ x} → 15:24:14 Bijection α β 15:24:23 only problem there is that we need ≡ 15:24:31 but having it depend on equality is silly imo 15:24:51 erm, f and g shouldn't be in {} 15:24:53 they should be in (), I think 15:25:11 (MissPiggy: right?) 15:25:37 well 15:25:47 if you are into category theory why don't you define it as a split epi 15:25:49 and mono 15:26:51 -!- lieuwe has quit (Ping timeout: 248 seconds). 15:27:18 because i don't understand category theory :) 15:27:31 me neither 15:27:37 * ehird wonders how to combine GADTs and the Foo { blah :: ..., } stuff 15:27:49 GADT?? 15:28:05 record syntax for GADT? 15:29:05 yar :P 15:29:15 well, not record syntax necessarily 15:29:21 just automatic accessor-definers 15:29:28 MissPiggy: you know what would be nice? 15:29:32 Having juxtaposition be like 15:29:48 juxtaposition :: (Juxtaposable a b c) => a -> b -> c 15:29:49 where 15:29:55 class Juxtaposable a b c | a b -> c 15:30:04 so you have Juxtaposable (a -> b) a b 15:30:15 and, say you have an accessor 15:30:17 but it also works for writing 15:30:29 so you have like 15:30:42 modify :: value -> accessor for that value -> new value of the property -> value 15:30:43 but also 15:30:51 Juxtaposable (Accessor a b) a b 15:30:58 so you can do "prop value" for access 15:31:02 by the way (you probably know this..) the dependent type stuff is more general than GADT 15:31:25 hmm although is it more general than She style GADT? 15:31:26 yeah 15:31:36 but gadts are nice syntax for most stuff, so. 15:33:05 i'll also have type-level functions basically 15:33:12 type Foo bar baz quux = ... 15:33:23 don't use type to define them?? 15:33:32 i was just picking an arbitrary keyword :) 15:33:38 okay but why need any keyword 15:33:41 but it's the same thing as haskell's type synonyms 15:33:42 just more general 15:33:45 as opposed to 15:33:50 the only different is that you are going into Set rather than Int or something 15:33:57 well, yes 15:34:01 but you use it at compile-time 15:34:07 I guess in the living environment of my OS it doesn't matter, but... 15:34:15 I suppose you are right. 15:35:36 # 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 According to Apple 4:3 is widescreen 15:38:29 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 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 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 ehird, #hl? that url is broken 15:39:20 everthing after that first # is an anchor 15:39:21 "Unfortunately, there is an error in the proof [...]." 15:39:24 AnMaster: javascript 15:39:27 not me, google 15:39:37 ehird, usually I don't get # there in the urls.. 15:39:37 hm 15:39:42 it's to avoid loading the surrounding stuff of the page, I bet 15:39:46 to speed up load times 15:40:12 "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 ehird, After reading it twice: huh? 15:41:38 It's a joke; laugh. 15:41:46 ehird, ah 15:41:56 If you don't understand it, you don't understand what p=np means :P 15:42:54 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 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 ehird, well, my brain was in math proof mode when reading it. I do see the joke now 15:43:27 anyway 15:45:20 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:23 You're a genius! 15:47:28 Why don't we just define P=NP as an axiom? 15:47:33 omg, this changes everything :D 15:48:26 har har 15:49:51 couldn't it (in theory) be proven that it is impossible to prove either P=NP or P!=NP ? 15:50:42 If it's true, maybe it can be proven. 15:50:52 It could be true that it is unprovable and yet not be provable that it is unprovable. 15:50:59 that too 15:51:01 It could also be false and thus not provable, at least if ZFC is consistent. 15:51:25 ehird, maybe it could be proven that it is unprovable to prove it unprovable? 15:51:36 (argh the headache) 15:51:59 I'll prove your mom. 15:52:16 alas I can't think of any snappy reply to that 15:53:20 "Your mom proved your face in bed last night, didn't she?" 15:53:29 "I was there. WATCHING" 15:53:45 Why don't we just define P=NP as an axiom? -- because nobody knows if it's independent yet!! 15:54:15 CONSISTENCY IS IRRELEVANT! 15:54:25 it's import to me :( 15:54:34 Son, I am import. 15:54:38 lol 15:55:18 i feel like i'm stumbled upon this wonderful oasis in programming language design 15:55:20 *i've 15:55:29 all the smartest people are here and it has such cool stuff 15:55:52 also, she is my favourite preprocessor ever. 15:56:04 pattern synonyms are actually something i've always wanted in haskell 15:57:03 She has them 15:57:12 She does. 15:57:12 oh shit 15:57:16 you are talking about she 15:57:22 YOU BROKE THE GRAMMAR 15:57:38 * MissPiggy crawl back into my mud bath 15:57:41 She has rules, and the first is: She can be talked about, but only if you respect her grammar. 16:00:31 hm a non-constructive proof for P=NP would be fun 16:01:14 Go straight to ⊥; do not pass go, do not collect £200. 16:01:26 heh 16:01:52 isn't testing *if* a number is prime in P? iirc that is 16:02:16 ehird, ^ 16:02:39 Yes, it is. Known since 2002. 16:02:49 Deewiant, AKS right? 16:02:53 Yes. 16:03:01 That book actually contained something meaningful? 16:03:03 I'm astonished. 16:03:15 Stolen from someone else, right? 16:03:20 Wut? 16:03:29 wut indeed 16:03:29 Oh, not A New Kind of Science. 16:03:34 It was published in 2002. 16:03:36 ehird, AKS Primality test 16:03:40 My inferrence engine is broken today. 16:03:50 ehird, you mean, it wasn't intentional 16:03:51 ? 16:03:52 YOU BROKE THE SPELLING 16:03:54 Nope :P 16:03:58 Deewiant: :'( 16:04:05 :-P 16:04:09 MissPiggy: any totally dependawesome insights on http://www.daimi.au.dk/~madst/tool/papers/expression.txt 16:04:22 she has http://personal.cis.strath.ac.uk/~conor/pub/she/higpig.html but i dunno seems hacky 16:04:22 ah 16:04:28 I have never actually understood this problem 16:04:33 i.e. I didn't read through it 16:04:41 my understanding is 16:04:51 higgelty piggelty works nice for epigram 16:05:00 but I don't know if it's related to expression problem 16:05:01 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 data Ty a = Foo a | Bar a 16:05:18 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 Here, we can easily add functions (columns) to this without violating type safety or modifying existing code, 16:05:39 but we cannot add new rows (data type cases) 16:05:42 like 16:05:47 func1 func2 func3 16:05:49 AnMaster: I don't know if it's "horribly inefficient" but yes, in practice it's slower than the probabilistic tests 16:05:51 Foo ... 16:05:52 Bar ... 16:05:53 with the results 16:05:55 get it? 16:06:07 in an object-oriented language, the columns can't be changed: they're the methods in a class 16:06:12 but you can easily add new rows: subclasses 16:06:21 The expression problem is: How can we have *both*? 16:06:36 wait a second, 16:06:56 you have data Expr = ..., and each constructor of Expr is a row 16:07:03 and you have func1, func2, ... each is a column 16:07:06 yar 16:07:25 you can easily add new functions, but you cannot add rows *elsewhere in the program* 16:07:29 they're fixed 16:07:35 with functions, you can just create a new one and bam, you're done 16:07:39 now, with OOP 16:07:48 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 you have class Foo { int bar(); int quux(); } 16:07:57 each method is a column 16:07:58 and you have 16:08:08 the values as the rows still 16:08:14 but you can extend them 16:08:15 class Bar extends Foo { ... } 16:08:18 so we can add rows 16:08:26 so with FP you can add columns, with OOP rows; the problem is being able to add both 16:08:33 elsewhere in the program 16:08:40 without breaking existing code 16:09:09 alright let me think 16:09:14 i'll make a text file showing this more clearly without ircspeak 16:09:23 you can do both of these (FP or OOP) approach using ADTs 16:09:43 I mean each one individually, using a different approach 16:09:44 btw, when you measure O(whatever) for an algorithm for prime factorisation, what exactly is it you measure it against. 16:09:56 but to have one framework that lets you solve both problems at once.. 16:10:15 AnMaster: Their complexities are O(f(n)) where n is the number tested 16:12:02 usually you say a number's size is its log 16:12:14 so just stick 2^n in there 16:12:18 or what Deewiant said 16:12:22 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:12:56 interesting problem 16:12:58 bbiab 16:13:00 I must be missing something critical here 16:13:10 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 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 oklopol, ah. Which logarithm? the natural one? 16:13:49 doesn't matter 16:14:06 i'll leave proving that as homework 16:14:30 oklopol, it does... if you take the n-log 16:14:37 it would always yield 1 16:15:09 obviously it must be a constant 16:15:18 oh right 16:15:30 eh, misspiggy disappeared 16:15:48 anyway log_a(n) and log_b(n) are a constant apart, so that doesn't matter for O 16:15:50 (usually) 16:16:32 Well, for anyone who wants an explanation of what the expression problem is: http://pastie.org/812457.txt?key=jy9qm2hfkgtfxiooahshxw 16:16:48 i have enough problems already 16:16:52 (5) 16:17:23 oklopol, hm correct me if I'm wrong but: log_a(n) > log_b(n) for all n if a < b? 16:17:27 http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w 16:17:32 Revised version; forgot to change one sentence. 16:17:41 wait, no, that probably only applies to n larger than the base or such 16:17:44 AnMaster: nope 16:17:45 oklopol: Is a bitch one? 16:17:58 ehird: they all have to do with complex analysis 16:18:14 oklopol, "nope" to "only applies" or to the original statement? 16:18:40 no matter what n is, log is increasing 16:18:41 oklopol: So I suppose you could say that you have 99 (minus 94) problems, but a bitch ain't one. 16:18:50 (well n>0) 16:19:00 oklopol, well yes, but that isn't what I said. I said what their relative values are 16:19:04 between two different bases 16:19:04 ehird: is that a reference to something? 16:19:14 Maybe. Also, http://i.imgur.com/b8OLl.jpg 16:19:28 AnMaster: oh sorry 16:19:49 oklopol, log_10(500) < log_e(500) for example 16:20:03 yeah that's true then, log is decreasing w.r.t. base 16:20:05 (those are the ones with easily accessible buttons on my calculator 16:21:50 AnMaster: What you're missing in your trial division thing is the complexity of a division 16:21:50 oklopol, does it make sense to do something like lim_{a->+inf} log_a( whatever ) 16:22:16 depends on the topology! 16:22:20 but yes, why not 16:22:33 oklopol, then use that log for the complexity! 16:23:06 whenever it is constant or not could perhaps be argued, but it no longer depends on n at least 16:23:12 ah, i guess you win 16:23:16 Deewiant, hm. What is that complexity 16:23:30 O(n^2) with the trivial algo 16:23:35 oklopol, well, I'm on deep water here, I probably missed something crucial. 16:24:14 that is still polynomial unless I'm completely missing something? 16:24:18 i don't remember what the known bounds are tho 16:24:28 wait were you serious about the lim? 16:24:32 i have no idea what you meant 16:24:38 oklopol, not really 16:25:09 but, it is an interesting question: What happens with logarithms as the *base* approaches infinity? 16:25:41 the function "f(n) = lim_{a->+inf} log_a( n )" is the constant function 0, i think 16:26:48 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:27:57 oh wait, prolly not. 16:28:32 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:30:06 hm 16:31:25 -!- cheater2 has quit (Ping timeout: 264 seconds). 16:31:48 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:32:16 and e^x > 0 for real x 16:32:17 like a=-4 and y=3 16:33:31 (-4)^3 = -64 Thus shouldn't 3 = log_{-4}(-64) ? 16:34:47 AnMaster: So -64 takes 3 digits to represent in base -4? Noted. 16:35:10 with a negative base, it makes no sense to give the log any arguments except naturals afaik 16:35:12 ehird, well yeah, when you think of logarithms that way it doesn't really work out ;P 16:35:27 isn't it true though? 16:35:30 For general negative x, y is complex 16:35:40 And non-unique 16:35:45 oklopol, hm? (-2)^(-1/2) gives an imaginary answer, doesn't it? 16:36:15 abc in base n is just (((a*n)+b)*n)+c 16:36:31 to be more precise, isn't it ((sqrt(2))^-1)i 16:37:09 Deewiant, ah, the lack of uniqueness could indeed cause issues 16:38:10 hmm okay i'm not sure what i was thinking 16:38:27 -!- MissPiggy has joined. 16:38:35 ehisrd 16:38:40 MissPiggy: http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w 16:38:48 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 The expression problem, explained simply. 16:39:02 ehird iI think I can give nice solution 16:39:13 are you so excited you can't type? :P 16:39:14 which makes essential use dependendt types 16:39:21 no this sthing is qwerty 16:39:22 :/ 16:39:25 ah lol 16:39:27 haha 16:39:37 I am on my moms computer because I got fed up with this installer 16:39:39 MissPiggy, which layout normally? 16:39:44 colemak 16:39:47 ah 16:39:57 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:40:39 ehird you know lists 16:40:47 excpet backwards... 16:40:53 [] :: a :: b :: c 16:40:58 okay 16:41:00 equivalent 16:41:05 of course the type of c can depend on the tail of the list 16:41:13 the head you mean 16:41:17 :P 16:41:18 head::tail 16:41:22 or are we still calling it the tail 16:41:25 just having tail::head 16:41:26 AnMaster: log_a(x) would be defined when: x > 0 & a > 1 or x < 0 & a < 0 & what 16:41:49 i mean you coulld have xs :: x, then x : Vector (length xs) 16:41:50 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 AnMaster: 1) if you want it to be complex, that's already been done. 16:42:15 then you get [] :: () :: (a) :: (x y) :: (p q r) 16:42:20 AnMaster: ln(-1) = i pi 16:42:24 http://www.wolframalpha.com/input/?i=set 16:42:24 wat 16:42:37 AnMaster: For 2), sure, but what's the definition 16:42:39 so similar to this, instead of making a triangle ou could make a matrix 16:42:46 by adding rows and cols to it 16:42:50 hey guys 16:42:58 anyone got introduction to algorithms 3e? 16:42:58 Deewiant, 1) hm right 2) what? 16:42:59 MissPiggy: interesting! 16:43:09 AnMaster: What I just said 16:43:11 but does it work for any type? i don't think so 16:43:14 you have to define it to work 16:43:20 Deewiant, isn't it undefined due to x^-1 = 1/x and division with zero being undefined? 16:43:22 AnMaster: Sure, you can let it be undefined for some values, but what are those values 16:43:29 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 ehird anyway that's just the idea.. I'll try and write it out and see if it works 16:43:56 AnMaster: Huh? e^(i pi) = -1 16:44:23 MissPiggy: If that works it's really cool 16:44:23 Deewiant, I think we are talking about two different things here. with regards to 2). 16:44:35 ^..^ 16:44:40 come on 16:44:42 someone has to 16:44:43 Deewiant, Didn't "sure, but what's the definition" refer to the bit "x^-1 is undefined for x = 0"? 16:44:57 oh 16:44:57 meh 16:45:00 AnMaster: I meant what would the definition of log_a(x) be 16:45:09 Deewiant, I read "what" as "that" -_- 16:45:12 And what values of a and x would it be defined for 16:45:30 Deewiant, as in, you claimed x^-1 was undefined for x=0 due to being defined that way XD 16:45:41 Yeah, no. :-P 16:46:01 (Although that's sort of true too.) 16:46:10 oh? 16:46:54 x^-n is defined as 1/x^n for x != 0, n > 0 16:47:36 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 hm, forgot that was by definition rather than as a consequence of something else 16:47:58 well it's a consequence of what i said 16:48:13 that it's defined that way 16:48:15 Deewiant, but a lot of math wouldn't work if it wasn't defined like that though. 16:49:14 I didn't say it's unnecessary or anything. 16:49:43 (differentiation of expressions like x^(1/3) comes to mind) 16:49:55 Deewiant, hm is it an axiom then? 16:50:07 No, just a definition. 16:50:17 hm. 16:52:00 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 Hrrm, maybe it could be defined in some other way for when a<1 in that case 16:52:35 (x^a)' = a*x^(a-1) 16:52:39 in no point but 0 could that change 16:52:45 by the way 16:52:54 there's two kinds of differentiation 16:53:14 one is where you differentiate a function, like the function x |--> x^a 16:53:42 the other is where you differentiate 'formally', like it's just some kind of symbolic operation on syntax 16:53:50 and you get dxdx = 0, dxdy = -dydx 16:53:58 it's weird as fuck.... 16:54:32 there are natural ways to interpret those, even without infitesimals 16:54:50 and to be honest i'm not sure i understand them 16:55:05 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 well, ... it gives the right answer in the end 16:55:14 s/;/:/ 16:55:22 d isn't a letter though 16:55:22 formal differentiation is usually an operation defined for polynomials defined just like differentiation usually works for polynomials 16:55:31 d is a magical operation and it isn't even the letter d! 16:55:36 at least i consider d an operation, prolly cause i'm stupid 16:55:44 like, it's a transformation on variables 16:55:55 d(u+v) = du+dv 16:56:06 d(uv)=du*v + u*dv 16:56:11 stuff like that 16:58:04 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:22 it's just a mnemonic 16:58:26 oklopol, yes I know that 16:58:38 oh you know integration by substitution 16:58:42 it still creeps me out though 16:58:44 I have an idea about that 16:59:06 intergration by substitution works as follows: substitute something for x. 16:59:07 if (x,y,z) is one coordinate system (u,v,w,...) is another, then you make a pullbacn 16:59:12 pullback 16:59:27 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 and the idea is that you can transform forms like Adx+Bdy+Cdz into a du,dv,dw.. form 17:00:18 MissPiggy: what? 17:00:38 MissPiggy, wait, is that integration in more than one variable? 17:00:49 yes 17:01:16 you can interate over dx,dy,dz, or dydz,dxdz,dydx or dxdydz 17:01:21 MissPiggy, I don't read that much math when studying CS. At least not during the first year 17:01:34 which corresponds to the curves, surfaces and volumes 17:01:59 of course 3D is just one special case of nD 17:02:48 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 well theres this theorem that relates integration over a boundry to integration over the volume itsselt 17:03:39 AnMaster: if you have a function from an n-dimensional rectangle to reals, just integrate one axis at a time 17:04:05 it's all pretty nebulous and convoluted.. I'm still trying to figure it out myself 17:04:06 hm... 17:04:14 i mean integrate along one axis, and at each point integrate over the (n-1)-dimensional rectangle 17:04:18 corresponding to that point 17:05:11 -!- Pthing has quit (Remote host closed the connection). 17:05:16 oklopol, like ∫(∫(∫...dz)dy)dx? or something like that? 17:05:28 if you wanna integrate a function from some more complex thing, you usually use substitution so you can integrate on a rectangle 17:05:37 yeah something like that 17:06:05 fubini's theorem says you can integrate along the axes separately, and order matters not 17:06:08 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:06:15 inside of each other 17:06:19 right 17:06:43 woah is that fubini's theorem 17:06:49 I should know that.... 17:07:08 -!- sshc has quit (Quit: leaving). 17:07:13 oklopol, seems like a PITA to calculate though 17:07:33 (considering what a PITA integrals in one variable is) 17:07:40 if you have n axes, you have to solve n integrals 17:07:40 s/is/are/ 17:07:56 often some of them are just multiplication 17:08:28 oklopol, oh? "often" as in "often in exams" or "often in real world applications"? 17:09:27 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 if you're integrating an expression that doesn't depend on y over variable y, then it's just multiplication 17:10:07 i don't know anything about the real world 17:10:14 or calculus, for that matter 17:11:24 In real world you just integrate numerically and forgot all that symbol-manipulation nonsense. (Okay, so maybe not *quite*...) 17:11:31 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 even if you can solve it for many such products 17:12:04 (that was in reply to " often some of them are just multiplication") 17:12:28 fizzie, hah 17:12:30 yeah okay you completely misunderstood then 17:12:46 reread "oklopol: if you're integrating ..." 17:13:19 oklopol, well, yes, I was so busy writing that line to be correct, I hadn't noticed any line after " oklopol, oh? "often" as in [...]" 17:13:27 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 often the expression is only nontrivial to integrate over one axis (in homework problems that is :P) 17:14:51 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 even int y a b (x) should be obvious 17:15:44 oklopol, to be more specific: I'm unable to detect any dx or dy indicating which variable you are integrating to 17:15:54 oh that would be y 17:15:56 err, "integrating with respect to" 17:15:57 i don't use d's 17:16:21 well okay, then that line makes perfect sense yes 17:16:56 That'd be (b - a)y then, not (b - a)x. 17:17:24 Deewiant: what would be? 17:17:48 No, right, I read that exactly upside-down. 17:17:55 Deewiant, err wait... the x would still be there as well, no? wouldn't it be x*(b-a)*y 17:17:58 y is not necessarily even bound after the integral, and okay 17:18:10 8| 17:18:24 wait, nvm 17:18:24 AnMaster: y means nothing except inside that integral. 17:18:36 oklopol, I forgot that it wasn't an indefinite integral 17:18:38 xb - xa. 17:18:54 y is what gives (b-a) indeed 17:19:02 ...what does it have to do with this that it's indefinite? 17:20:18 oklopol, unless I'm completely confused by now: ∫xdy = ∫(x*1)dy = x*∫1dy = x*y 17:20:29 (i mean apart from the fact it's not one) 17:20:42 you can just write 17:20:44 oh 17:20:50 ∫dx 17:20:52 AnMaster: Yes, for an indefinite integral that's correct. 17:20:56 it doesn't need ∫1dx 17:21:19 MissPiggy, well yes. I added the 1 to make it clear what I meant though. 17:21:28 ok 17:21:38 And for an definite one then y turns into (b-a) 17:21:48 ∫_A dxdydz is the volume of A 17:21:58 Deewiant, ^ 17:22:13 Yes, I am aware. 17:22:27 Deewiant, well, but looks like oklopol got confused: 17:22:29 y is what gives (b-a) indeed 17:22:29 ...what does it have to do with this that it's indefinite? 17:23:01 yeah i was confused, didn't see why it's relevant that the definite integral was indefinite 17:23:07 AnMaster: So why are you talking to me and not him? 17:23:09 because it wasn't true 17:23:09 oklopol, my point was that I forgot it _wasn't_ indefinite 17:23:14 i see 17:23:30 "AnMaster: oklopol, I forgot that it wasn't an indefinite integral" misread 17:23:37 Deewiant, well: both since you highlighted me ;P 17:24:22 Mostly because he didn't respond 17:24:54 Deewiant, err? he did? " oh" 8 seconds before that highlight? 17:25:23 I wasn't sure if that was a response :-P 17:25:32 i just realized what he meant 17:25:51 and continued watching simpsons 17:25:52 Deewiant, I couldn't see what other interpretation would make any sense though 17:27:04 -!- MissPiggy has quit (Quit: MissPiggy). 17:27:39 also: definite integrals from 1 to infinity (or similar) are creepy. 17:27:39 i should sleep 17:28:29 -!- MissPiggy has joined. 17:29:31 what's creepy about them? 17:29:40 -!- Asztal has joined. 17:30:18 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:35 oh that old thing 17:30:36 I don't remember if it was 1/x or 1/(x^2). Something like that anyway 17:30:45 think about the same thing in one less dimension 17:30:56 oklopol, hm? 17:30:58 say you have the curve 1/x^2 or something 17:31:03 the are under it is finite 17:31:07 but the actual line is infinite 17:31:08 well yes 17:31:10 WOW 17:31:14 *area 17:31:18 which is creepy too. But not quite as creepy 17:31:27 then there's the paint argument 17:31:33 that 17:31:38 if you pour paint into the infinite tube 17:31:41 it'll fill up 17:31:43 oklopol, Yes I heard that 17:31:52 but you can never actually paint it 17:31:53 but it wouldn't be enough to paint the sides 17:31:56 exactly 17:31:56 yeah 17:32:16 but the thing is this makes absolutely no sense as an analogy 17:32:35 because you'd be painting it with some constant thickness of paint 17:33:12 so obviously you'll be using much more paint toe paint it than to fill it, after a whi 17:33:24 *to paint it *while 17:33:30 (wild mouse) 17:34:52 oklopol, about that thickness: you could get it go towards zero. 17:35:17 (makes as much sense at the rest...) 17:35:32 yep 17:35:37 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 and then the amount of paint would also be finite 17:35:56 well for 1), that is excluding the integral of f(x)=0 17:36:55 or functions that not only approach zero, but actually reach it and then stay there. 17:37:00 that sounds about as creepy as "two numbers can add up to a third one" 17:37:01 at some finite point 17:37:10 oklopol, hm? 17:38:05 it just does not sound creepy 17:38:45 oklopol: they CAN?!?!?!? 17:38:51 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 ehird: they can, and they *will* :| 17:39:04 oklopol, how is that not creepy? 17:39:20 are you sure you know what creepy means 17:40:23 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 this is what the whole thing reduces to 17:40:48 *sum of that subset 17:40:54 shouldn't use words for stuff like that 17:41:25 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 oklopol, that way to express it is too abstract (to me at least) to visualise it. 17:43:33 it means you take your integral and round things up 17:43:36 why visualise it 17:43:42 you get an infinite amount of numbers 17:43:46 all of which are positive 17:44:18 and if you know anything about series, you can see this infinite amount of numbers can have such an upper bound 17:44:25 oklopol, but try imaging this integral in terms of area 17:44:43 i always imagine infinite sums in terms of area 17:44:55 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 i just start stacking them up 17:45:09 and i see their sum is 2 17:46:02 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:46:04 Presumably 2^-n 17:46:35 hehe 17:47:04 AnMaster: sure, i even feel comfortable with defining "area" of that to be a frog 17:47:25 *the 17:47:29 oklopol, har. 17:47:36 it was not a joke 17:47:39 negative bases are awesome 17:47:41 signs are rubbish 17:47:54 there is no connection between mathematical areas and the real worls 17:47:56 *world 17:48:00 yes there is 17:48:00 ehird, balanced -ternary? 17:48:03 no ther eisn't 17:48:05 http://en.wikipedia.org/wiki/Negative_base 17:48:06 *there isn't 17:48:35 where - is a minus sign of course 17:49:52 oklopol, then how do you explain that finite real world and math areas seem quite often to match up? 17:50:06 http://personal.cis.strath.ac.uk/~conor/pub/Holes/Holes.pdf 17:50:08 this is awesome 17:50:32 AnMaster: because we constructed them to be vaguely similar to the real world at first 17:50:44 AnMaster: they model the real world well; obviously i didn't mean what i said 17:50:47 matheamtics has no inherent existence, it's just single-manipulation we dreamed up 17:50:50 although it was completely true 17:51:00 ehird, well yes. 17:51:24 mathematics is real 17:51:52 Your definition of "real" is strange. 17:51:55 MissPiggy, unless it is complex (or quaternionius or whatever) 17:52:04 It does not exist physically, and abstract concepts do not really "exist" as such, they only exist insofar as operations on them. 17:52:05 hm 17:52:13 but the geometry of our world isn't the same as R^n, it's just one approximation of it 17:52:16 And the symbol manipulation was all invented by us. There's no inherent existence of mathematics. 17:52:18 "quaternionius" sound incredibly awkward 17:52:19 The universe does not have mathematics. We do. 17:52:30 AnMaster: Sounds like a good name for a fictional character. 17:52:33 Quaternionius. 17:52:39 ehird, what genre? 17:52:44 WHO KNOWS 17:53:33 oklopol, what about fractals? Comfortable with them too? 17:54:23 AnMaster is uncomfortable with a lot of very simple things. 17:54:23 ehird, hm does a balanced negative base even make sense? 17:54:29 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 AnMaster: what definition of fractal? 17:55:08 I agree with what you are saying about geometry 17:55:31 i'm not all that comfortable with sets whose hausdorff dimension is not a natural number, they are usually really scary 17:56:46 oklopol, hm. 17:56:55 -!- Pthing has joined. 17:57:56 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 "Definition of fractal" can't really mean more than one thing 17:59:04 Deewiant, oh? 17:59:22 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 I could think of two things: a) definition of a given fractal b) definition of what a fractal in general is. 18:00:11 "Definition of fractal" can't mean a) 18:00:17 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:19 if possible 18:00:25 "Definition of x" where x is known to be a fractal does 18:00:39 now fractals, afaik, are defined as sets whose hausdorff dimension is not a natural number 18:01:16 but a common way to construct such sets is through these recursive thingamajigs 18:01:33 which are probably a more common definition for a fractal 18:02:20 so what i'm saying is i'm comfortable with drawing things recursively, but sure, some complex sets are pretty scary 18:02:27 well yes recursive algorithms is the most common way to define a fractal that I have seen 18:02:32 if not the only way 18:02:49 that is, a given fractal 18:03:03 so everything is a fractal that can be computed using recursion, or what exactly? 18:03:23 oklopol, well, not afaik. 18:03:27 a question by which i mean that's a crappy definition, the hausdorff one is sexy 18:03:49 oklopol, I did know a bit about the dimension thing 18:03:53 -!- MissPiggy has quit (Quit: MissPiggy). 18:04:37 what do you mean, you knew we can embed k-dimensional objects in n-dimentional space? 18:04:55 *dimensional 18:05:47 also, what ehird said about common creepyness above: by that logic complex numbers should be creepy. But they aren't IMO 18:07:04 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:38 oh? cool. 18:07:48 (i hope you also know not all do) 18:08:24 oklopol, hm? 18:08:36 well err 18:08:55 i mean if you use the definition "thing you can draw using some sorta recursino" 18:08:58 *recursion 18:09:00 :P 18:10:04 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:10 (or something like it) 18:10:20 yeah 18:10:39 which, while recursive, would give you a straight line starting at a given point and then going on forever 18:11:46 the sexiest thing about hausdorff dimensions is you don't have need to be working with real numbers 18:11:52 just any metric space 18:11:55 oklopol, what about requiring more operations for each step (alt: you recurse more than once at a given level) 18:12:11 most (all?) fractals seems to be like that? 18:13:26 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 hm, is that a fractal, or just something similar? 18:13:42 koch snowflake 18:13:48 oh 18:13:57 that's the cantor set 18:14:06 did you come up with that? 18:14:15 oklopol, I know that algorithm is a classical one 18:14:19 if you did, you could've been famous! 18:14:20 oh 18:14:21 I didn't remember the name of it 18:14:38 also called cantor's dust, it has useful properties 18:14:51 oklopol, name is indeed familiar when you mention it 18:15:03 oklopol, anyway, what is the dimensionality of it 18:15:32 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:39 (with lebesque measure) 18:15:49 oh... 18:15:52 Homeomorphic lebesques. 18:16:00 ehird, XD 18:16:01 I think they have porn of those. 18:16:48 Higher math is actually all porn behind the scenes 18:16:52 also: " koch snowflake" <-- that's the one you add in a triangle (well, two sides of one) in the middle, right? 18:16:53 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:11 yeah 18:17:22 Homeomorphic lebesques functoring. 18:17:59 "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 ehird, that quote is one truly awful joke... 18:20:00 where is it from? 18:20:11 It's not so much a joke as colourful wordplay. 18:20:34 http://personal.cis.strath.ac.uk/~conor/pub/Holes/Holes.pdf, a paper that begins: 18:20:34 yeah, maybe calling it "joke" was stretching things a bit ;P 18:20:38 Abstract 18:20:41 Mornington Crescent 18:20:43 1 Introduction 18:20:46 The purpose of this paper is not only self-citation (McBride, 2001; McBride & Paterson, 2006), ... 18:20:54 (Yes, the abstract is actually "Mornington Crescent".) 18:21:03 hah 18:22:02 ehird, the language used, which one is it? haskell? 18:22:16 some parts of it look quite similar at least from a quick glance 18:27:29 Haskell with a few bits of do-what-i-mean. 18:27:39 In 18:27:43 naughtE :: ∅ → a 18:27:44 naughtE = ⊥ 18:27:46 for example, 18:27:53 ⊥ would be an operator and thus not valid like that 18:28:04 But it doesn't matter because it's a paper, not a program. :P 18:28:18 -!- MizardX- has joined. 18:28:26 (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:17 ehird 18:32:23 you're right, she forgot language 18:32:38 the lambek calculus was designed for grammatical structures. 18:34:54 augur returns to the discussion, just in time for me to wake up 18:35:01 hey :p 18:35:17 ಠ_ಠ 18:35:25 oh hai 18:37:28 ehird, ah 18:39:09 ehird, i think you're naughtE 18:41:12 * pikhq waves at folk 18:51:39 hey pikhq 18:52:33 Hey. 19:06:24 -!- sshc has joined. 19:07:24 * Sgeo wonders if ehird is going to read FS soon 19:10:55 im having an email convo with noam chomsky D: 19:10:55 :D 19:10:57 D: 19:19:14 hello 19:20:22 [18:32] you're right, she forgot language 19:20:22 he 19:20:27 augur: really? 19:20:28 cool 19:21:00 ehird: misspiggy is not a boy. 19:21:06 he's fax. 19:21:08 aka soupdragon 19:21:11 and fax is a girl. 19:21:18 i'm fairly sure i've heard otherwise 19:21:34 If using a female nickname one should expect female pronouns. 19:21:42 well we'll ask just to confirm ;P 19:21:56 ehird: indeed, tho, yes. lambek calculus _is_ a theory of grammar. 19:22:22 "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:25 In wonderland. 19:22:28 Aw, taken. 19:22:37 -!- alice has changed nick to alise. 19:24:37 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 my evidence is that she told me so. 19:25:11 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:25:35 augur: ah. 19:25:58 whats up sweeties? 19:26:05 or maybe transman? i have no clue about the details, honestly. 19:26:23 all i know is that fax/soupdragon/misspiggy is smart and interested in CS and linguistics 19:26:28 and therefore has become a good friend. 19:26:33 cheater3: WHOS YOU 19:26:37 hmm... i think we've had more transgirls here than cisgendered females 19:26:39 DONT CHEAT ME 19:27:00 alise: you're a transgirl. 19:27:08 no. no i'm not 19:27:09 tho maybe not intentionally :X 19:27:16 my gender is 0.5 :P 19:27:26 :p 19:27:33 ehird is genderqueer! 19:28:42 augur: i am you 19:28:47 D: 19:28:49 oh ok 19:28:51 god programming languages are sexy :| 19:28:55 * augur makes out with himself 19:29:00 can i be typesexual 19:29:05 programming languages are transgender 19:29:17 only if you're into programming languages with strict typing 19:29:24 which ofcourse means lots of leather and whips 19:29:29 i was about to - 19:30:08 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:37 i wont 19:30:39 i hate ovaries 19:30:57 but you're still ehird, and ovaries wont make you most spiteful 19:31:03 more* 19:31:10 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 augur: do you have 'introduction to algorithms' 3 ed for me? 19:31:26 and two, they're not really a concrete collection of values 19:31:31 so I'm back to square one 19:31:34 cheater3: what? 19:31:53 alise: call it Empty. thats what the dependent type people call it. 19:31:57 i am looking for the book called what i just mentioned, augur 19:32:05 cheater3: ill try! 19:32:15 augur: I *am* a dependent type person! 19:32:22 augur: but I'm also a Unicode whore. 19:32:32 :) 19:32:38 then use an epsilon 19:32:53 ∅ should be reserved for actual {}'s 19:33:07 right but epsilon is "arbitrarily small", not "length one" 19:33:11 ε is occasionally used for the empty string, but 19:33:12 augur: 2ed gives minus 50 points 19:33:33 augur: do you think ∅ is acceptable for any sequence, though? 19:33:48 lists, concrete sets (actual {}s, as you put it), associative maps, etc. 19:33:50 no, its not a sequence 19:33:59 but it's a convenient and pretty notation 19:34:13 1 ∷ 2 ∷ 3 ∷ ∅ 19:34:38 err wait 19:34:44 what i want isn't "arbitrarily small" 19:34:46 I want "empty" 19:34:52 epsilon isn't empty, it's arbitrarily small 19:35:08 well its the empty string in formal language theory! 19:35:10 relatedly, what should I call the unit type? maybe a circle 19:35:13 cheater3: i only have the second edition :( 19:35:24 cant find the 3rd edition anywhere 19:35:26 augur: don't get me wrong, I don't care about total mathematical notation faithfulness 19:35:29 augur: you don't want minus 50 points, do you? 19:35:30 alise: unit type should be a fancy 1 19:35:31 I just don't want it to *confuse* mathematicians 19:35:36 augur: heh 19:35:39 augur: find me a fancy one and it's done 19:35:46 augur: blackboard 1 would work, to fit in with sets like N 19:35:58 well lets see what unicode gives us 19:36:51 disregard ∷ ∀a. a → ○ 19:36:52 disregard x = ○ 19:37:18 1⒈①❶➀➊⓵⑴Ⅰⅰ 19:37:28 heh, ➀ 19:37:36 ○ > ➀ imo 19:37:40 ☝ 19:37:55 that is not a rude gesture. 19:38:10 if i had one more finger it would be 19:38:11 ZAL҉̵̞̟̠̖̗̘̙̜̝͇̊̋̌̍̎̏̐̑̒̓̔̿̕̚͡ ̒̓̔̕̚GO he cometh. 19:38:11 :| 19:38:27 i like the ring tho 19:38:28 ring is nice 19:38:58 ZAL҉̵̞̟̠̖̗̘̙̜̝͇̊̋̌̍̎̏̐̑̒̓̔̿̕̚͡ ̒̓̔̕̚GO is ta∵∵si∵∵ 19:40:43 ⦶⦸⦼⧃⧂ 19:40:49 check it out, im writing in naboo-an! 19:41:01 ○ is nice because it's like () but without the tupley implications 19:41:04 because it isn't really tupley 19:41:09 indeed 19:41:18 main ∷ Partial (IO ○) 19:41:35 ⦾ 19:41:47 ⨀ 19:41:57 ⇄ would be a good unicode name for IO. 19:42:00 ⊙⊚ 19:42:08 augur: i think it doesn't exist :( 19:42:10 main ∷ Partial (⇄ ○) 19:42:18 augur: your second-last line is just a boob. 19:42:26 cheater3: it does, published in like september last year or something 19:42:39 augur thats not the kind of exist that i meant 19:42:43 ⨴ can denote partial 19:42:54 ⨴ (⇄ ○) 19:42:58 I can't see that 19:43:12 its part of a circle! 19:43:14 multiplication sign in left half circle 19:43:15 lol 19:43:25 why are you guys using squares all the time 19:43:32 we're using unicode 19:43:33 and you're not 19:43:36 GTFO 19:43:39 i am using xchat 19:43:43 the latest version 19:43:52 so what are you talking about 19:43:53 http://www.fileformat.info/info/unicode/char/25d6/index.htm 19:44:02 If it doesn't do Unicode, then it sucks balls. 19:44:03 cheater3: one, stop using windows 19:44:04 two, get fonts 19:44:07 how do i make xchat use unicode more than it does already 19:44:08 three, set encoding to utf-8 19:44:15 how do i set encoding 19:44:20 press alt-f4. 19:44:38 alttttttttttttttffffffff44444 19:44:41 doesnt work 19:44:46 i cant reach the minus 19:44:49 autodefenestrate 19:45:31 cheater3: Weak. 19:46:27 so pikhq 19:46:37 i don't want to use _ for my multifix operator placeholder character 19:46:41 uh you may not know what multifix is 19:46:47 pikhq: multifix lets you define operators like this 19:46:53 if_then_else_ 19:47:02 [_] 19:47:03 (_) 19:47:17 _therefore_CHICKENPOX$_okay_okay 19:47:19 used as: 19:47:24 if poo then bar else lux 19:47:26 [bok] 19:47:29 (wammy) 19:47:44 mints therefore (death is okay) CHICKENPOX$ whoa okay (2+2) okay 19:47:56 alise: So, even less special syntax. 19:48:11 λ_._ 19:48:11 Hmm. 19:48:12 It's a lambda! 19:48:17 pikhq: i would like to stand up to your expectations but i cannot. :( 19:48:19 pikhq: but I don't want to use _ for it because you should be able to use that in names 19:48:25 (Unicode is acceptable, even encouraged) 19:48:56 alise: Not sure; that's hard to pick... 19:49:44 i used the boob character, ⨀, but it just didn't really look very good 19:49:46 if⨀then⨀else⨀ 19:49:55 λ⨀.⨀ 19:50:00 pikhq: Some sort of question mark would work 19:52:34 can you guys try those squares again pls 19:52:38 if ※ then ※ else ※ 19:52:43 nope, doesn't work 19:52:51 try again? 19:53:05 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:19 Asztal: try once again 19:53:23 ‽℀℘ℋ₨áóíúéμ 19:53:29 nope, still squares 19:53:29 http://esolangs.org/wiki/RETURN <-- made an interpreter in python 19:53:30 Asztal: no spaces 19:53:42 if※then※else※ 19:53:45 looks like a holocaust 19:53:47 :P 19:53:52 if BOOM then BOOM else BOOM 19:53:59 i saw: interrobang, a/c, some weird p, some weirder H, Rs, 'a, 'o, 'i, 'u, 'e, mu. 19:54:01 Asztal: i am using xchat, is that not a good client for that? 19:54:13 cheater3: try setting the encoding to UTF-8 19:54:13 what has ℀ got to do with anything? 19:54:24 gm|lap, Asztal: i tried doing /charset IRC and /charset UTF-8 19:54:32 both do not work 19:54:34 aww :/ i guess you might be lacking fonts then 19:54:47 where do i get unicode fontz for my windoze? 19:55:03 idunno, all i can say is you can get them with linux 19:55:08 or FreeBSD, even 19:55:36 i suggest you look at that python interpreter, the idea is really scary 19:56:16 let me try this 19:56:17 Courier New – 2726 characters (3151 glyphs) in version 5.00 19:56:57 heh... AFAIK X11 rips chars from other fonts 19:56:59 if you couldn't see áéíóú that's an indication that it's not a font issue 19:57:04 if anything's missing 19:57:26 Asztal: i could see that 19:57:29 if you couldn't see ☭ that's an indication that it's probably a capitalism issue 19:57:32 cheater3: stop using windows. :) 19:57:33 Asztal: but i could not see the 5 to the left of that 19:57:37 if☭then☭else☭ 19:57:38 gm|lap: Yeah, X11 makes a best-effort to display everything, even if it is ugly as hell. 19:57:41 alise: stop being a transgirl :) 19:57:51 consider it done 19:57:53 gm|lap: not on my usual baux 19:57:58 (yes, baux) 19:58:18 alise: don't upgrade, pulseaudio in ubuntu 9.10 is extremely crappy 19:58:30 i removed it with force 19:58:34 ...actually, with apt-get remove 19:58:40 i like 9.10, but this isn't my machine 19:58:44 also esound is broken too 19:58:45 it hasn't been upgraded only out of laziness 19:58:48 hmmkay 19:58:52 my desktop runs freeBSD 19:59:05 if¤then¤else¤ 19:59:11 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 My desktop still runs 7.04 19:59:20 tbh freebsd has the best sound system for unix ever: newpcm 19:59:38 it's like multi-application OSS 20:00:04 gm|lap: we have that it's called ossv4 20:00:34 i heard that was the one that was single-app-only... hmm 20:00:45 there was one which did MIDI and one which did multi-app 20:01:05 ossv3, old oss, is single-app 20:01:10 ossv4, which is new and not in the kernel, isn't 20:01:14 unless i'm mistaken 20:01:21 (it's kernelspace just not in the mainline kernel) 20:03:30 gm|lap, this isn't my desktop 20:03:37 I rarely even use my desktop anymore 20:03:44 Only when I want to get old files off of it 20:03:53 this is the slowest installer ever 20:03:59 microsoft word viewer 97 or something 20:04:07 pikhq: perhaps a solid middle dot would work 20:04:10 Get AbiWord? 20:04:11 ok 20:04:15 alise: Perhaps. 20:04:18 can you guys try the squares again 20:04:22 pls 20:04:31 最↓→ð 20:04:32 Perhaps 20:04:35 works 20:04:37 gm|lap: also, harddrive sizes are not a marketing conspiracy. 20:04:40 didnt even need to restart 20:04:42 ‽℀℘ℋ₨áóíúéμ 20:04:46 this did not work 20:04:58 cuils? 20:05:00 i see 5 squares and then 5 letters with diacrytics 20:05:09 and then \mi 20:05:14 or \mu or whatever that is 20:05:14 i reckon it's just being cheap 20:05:20 brb 20:05:50 gm|lap: http://www.tarsnap.com/GB-why.html 20:05:59 -!- cheater3 has quit (Quit: Leaving). 20:06:03 cheater3: Don't even see interrobang? 20:06:16 I'd guess you don't get a gnaborretni, either. 20:06:33 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 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 we don't run 2.2GB processors, we run 2.2GHz. 20:07:24 1 Gbps Ethernet transmits data at... 10^9 bits per second < that's also stupid. 20:07:26 pikhq: Please LART gm|lap, for he believes that units change their prefixes. 20:07:39 it was always 2^10 B for a KB 20:07:50 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 gm|lap: And it was fucking wrong. 20:08:12 Stop making things fucking wrong. 20:08:26 stop making things so damn cheapass 20:08:30 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 gm|lap: I will quote from the page you apparently didn't read. 20:08:48 "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 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 Yes, because they should be SSDs. 20:09:29 However, that does not mean a gigabyte is 2^10 megabytes. 20:09:35 (or mebibytes, for that matter) 20:09:37 Which are flash memory, which is addressed in silicon, so you get powers of two. 20:09:47 SSDs: Sexually Satisfying Disk 20:09:49 s 20:09:50 megafael 20:10:00 i restarted xchat and it said the 30 day evaluation is over 20:10:03 so i had to restart it 20:10:14 i thought this was free open source software, wtf 20:10:20 It is, the Windows build isn't. 20:10:23 Use Silverex, or not Windows. 20:10:29 can you guys try some unicode again? 20:10:35 no. :D 20:11:14 http://silverex.net/news IIRC 20:11:21 Hm 20:11:28 This laptop has to be at least 3 years old 20:11:31 do not be unfriendly alise 20:11:35 it is not nice 20:11:40 http://www.silverex.org/news/ actually 20:11:48 cheater2: :'''''''''''''''''( 20:11:48 * Sgeo is using Silverex 20:11:53 i cry 20:12:11 Asztal: can you try some unicode for me please? 20:12:26 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:13:32 *sightings 20:17:21 http://www.fileformat.info/info/unicode/char/2237/index.htm 20:17:26 I wonder what it's actually supposed to b e 20:17:27 *be 20:17:31 "proportion" is unhelpful 20:18:11 pikhq: annoyingly unicode messes with layout :( 20:18:26 because characters that display as >1 character are still treated as one character 20:18:32 (you can't fit *every* character into a tiny space) 20:18:35 (not without distortion) 20:18:41 alise: :/ 20:18:46 the solution, of course, is non-textual editing! :P 20:23:57 if ※ then ※ else ※ 20:24:02 hmm 20:24:08 if ※ then ※ else ※ 20:24:13 this crap don't work 20:25:56 -!- gm|lap has quit (Quit: 2 hour UPS expired. Shutting down laptop.). 20:26:27 -!- MissPiggy has joined. 20:26:41 hi MissPiggy 20:26:45 hello 20:26:54 nice name 20:27:13 so's your face :| 20:27:19 why thank you 20:27:25 I know rite 20:28:05 just repartitioned and reinstalled my os 20:29:17 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:29 I don't know what you mean 20:29:38 what type 20:29:39 I didn't really understand it so yeah 20:30:39 ? 20:31:47 hm 20:31:52 what are you asking 20:32:22 well 20:32:25 can you explain your solution to me 20:32:27 I didn't really grok it 20:32:49 okay 20:33:43 dyld: unknown required load command 0x80000022 20:33:43 zsh: trace trap ocaml 20:33:53 dammit 20:33:55 MissPiggy is an AI?! 20:33:59 le gasp 20:34:12 MissPiggy: you're using OCaml and zsh on OS X. 20:34:13 you're surprised by this? 20:34:19 i am so inferrerator 20:34:47 okay anyway, 20:34:56 the idea is to make a data type a bit like this one: 20:35:15 data Snoc a where nil :: Snoc a ; cons :: Snoc a -> a -> Snoc a 20:35:39 god dammit 20:35:45 data Snoc a where nil :: Snoc a ; snoc :: Snoc a -> a -> Snoc a 20:35:55 ya ya 20:36:07 the difference, is that in snoc xs x, you let the type of x depend on xs 20:36:09 so perhaps 20:37:00 data Snoc f where ... ; snoc :: forall xs :: Snoc f, f xs -> Snoc f 20:37:21 if you let f = const a, then it's equivalent to the old one 20:37:40 but if you let f xs = Vector a (length xs),for example -- you get triangles 20:37:52 forall xs :: Snoc f, f xs -> Snoc f 20:37:53 my idea is to use this to make matrices instead of triangles 20:37:54 this notation confuses me 20:38:14 it's just (xs :: Snoc f) -> (x :: f xs) -> Snoc f 20:38:17 use haskell notation like you've been doing but with (name::t)-style dependent type notation plz :P 20:38:19 ok 20:38:19 wait 20:38:21 lemme write this out so far 20:38:43 what type is f? 20:38:47 a->a? 20:38:53 no, a->Set 20:38:58 f :: Snoc f -> Set 20:39:01 -!- kar8nga has joined. 20:39:12 but don't worry about the type of f 20:39:21 it will probably become something else in the future 20:39:36 so it's not Snoc f a 20:39:38 just Snoc f? 20:39:57 yeah as I was writing Snoc f a I realized Snoc f subsumes it 20:40:08 so there's no need for an a 20:40:16 so: 20:40:22 data Snoc :: (Snoc f -> Set) -> Set where 20:40:22 nil :: Snoc f 20:40:26 cons :: (xs :: Snoc f) -> (x :: f xs) -> Snoc f 20:40:33 so, let me say this in words 20:40:56 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 so f gets the rest of the list, and returns the relevant type 20:41:17 so Snoc (const t) = Oldsnoc t 20:41:30 I think I see how this is cool 20:41:35 It's a polymorphic list of sorts 20:41:41 except the type of the element depends on the rest of the list 20:42:07 yes 20:42:25 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:26 but nothing else 20:42:28 okay, got it 20:42:32 so how does this solve the expression problem? 20:42:34 now what we could do is define something like 20:42:48 ROW 20:42:57 COL 20:43:23 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 this way you can build up a NxM matrix starting from a 0x0 one 20:44:03 at a first approximation that matrix could just have numbers in it, or whatever -- it doesn't really matter 20:44:26 to solve the expression problem we will have to compute the type of the cell based on the function spec. 20:44:37 but that's just details, the important bit is SNOCing on ROWs, and COLs 20:48:09 wait wait 20:48:12 let me catch up 20:48:15 forgot to read 20:48:20 okay so ROW and COL are data constructors 20:48:23 of the same type or not 20:48:34 yeah, I think that they have to be of the same type 20:48:39 an issue is that 20:48:46 ROW does not actually add rows 20:48:49 + func1 | func2 | ... Foo x y | y | x ... Bar x y | x | y ... +-----------------... 20:48:50 erm 20:48:54 Foo x y | y | x ... 20:48:55 Bar x y | x | y ... 20:48:58 all Foos and all Bars are the same row 20:48:59 ROW adds a column 20:49:03 and COL adds a row 20:49:05 ... 20:49:06 why? 20:49:24 [20:43] 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:11 :/ 20:51:19 so 20:51:24 let me answer that question 20:51:49 just a sec 20:51:55 MissPiggy: I think an example would help, so 20:51:56 http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w 20:51:59 the unextended bit there 20:52:04 with Foo x y and Bar x y as the rows 20:52:07 and func1 and func2 as the columns 20:52:14 how would you write that, given your definitions? 20:52:29 suppose we wanted to define functions, eval, size and show on data Exp = Num Int | Add Exp Exp | Mul Exp Exp 20:53:01 no 20:53:05 can we use my example :P 20:53:11 not to be rude, it's just that i understand mine 20:53:14 since it's very simple 20:53:32 instead of getting bogged down in details etc 20:55:59 z 20:57:24 MissPiggy: think I should have inductively defined sets as in mathematical notation? 20:57:28 might be convenient, dunno 20:57:44 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 read that sequentially and slowly :P 20:58:10 I think you can consider inductives as sets, but I don't 20:58:31 oh you said something else completely 20:58:38 yerr, i don't understand that :( 20:58:40 well you can implement set theory in type theory 20:58:48 what is it for Foo/Bar/func1/func2? :P 20:58:55 and what's a description 20:59:04 and er you have an unterminated string 20:59:09 it just says whwat the type of the constructor is 20:59:52 ?? 21:01:34 we dont' program over the real data Expr = ... 21:01:48 we are actually making a program over a generic sort of datatype called a universe 21:01:54 yeah but uh 21:01:59 ff 21:02:02 so U is isomorphic to Nat 21:02:10 and U is .... Expr 21:02:17 so what is * 21:02:20 what is string * thing 21:02:22 what operator is that 21:02:28 tuple? 21:02:31 oh I just meant that like a tuple yeah 21:02:39 thanks for inventing notation without telling me :/ 21:02:55 description = type? 21:03:02 could be yeah 21:03:13 what's the resulting value 21:03:18 (exists a. a)? 21:04:26 resulting value? 21:04:31 of what? 21:04:31 of the type 21:04:33 which type 21:04:37 fff 21:04:38 description 21:04:39 = type 21:04:40 of row 21:04:49 you know this sort of notation? 21:04:55 MuX.1+X 21:04:58 for data types 21:05:01 [20:57] 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 that line is what i'm referring to 21:05:22 I'm starting to realize that my idea takes quite a bit of background to understand.. 21:05:43 Okay, so I've tried to write my Foo/Bar/func1/func2 example using your notation. 21:05:47 wait I have a great idea how to explain that 21:05:49 nil `snoc` 21:05:50 Row "Foo" (a -> a -> (exists b. b)) `snoc` 21:05:52 Row "Bar" (a -> a -> (exists b. b)) `snoc` 21:05:54 Col "func1" (\_ y -> y) (\x _ -> x) `snoc` 21:05:55 Col "func2" (\x _ -> x) (\_ y -> y) 21:06:02 yeah just like that 21:06:15 Okay. Unfortunately, it doesn't allow adding rows. 21:06:20 ?? 21:06:25 If I add a row, and then call func1 or func2 on it, they don't work; they explode and break. 21:06:30 Because they don't handle the new type. 21:06:31 no 21:06:33 * Sgeo goes to mark 7000 or so conversations as read 21:06:46 In the OOP system, which can add rows, they inherit the definition (and you cannot remove fields, so they must work) 21:06:49 when you add a Row you must define one new case for func1 and func2 21:06:57 so it becomes 21:07:00 the reason you MUST do this, is because if you don't -- it will not typecheck 21:07:19 Row "Quux" blah (\_ _ z -> z) (\_ y z -> y+z) 21:07:23 func1 and func2 respectively 21:07:24 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:30 yes 21:07:45 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 this would be incredibly awkward to program in 21:07:51 * MissPiggy is compiling Coq to try and implement this 21:08:09 alise yeah it'll be awkward as fuck in Coq but I bet you could make easy as pi in epigram 21:08:16 easy as pi :D 21:08:23 fuckin' Coq 21:08:25 (the epigram that isn't quite finished yet, epi 2) 21:08:39 try agda? 21:08:47 the flexible operators might help make the syntax more bearable 21:09:08 I have 16,163 messages in label "Agora" 21:09:22 I have two rabbits 21:09:38 (13530 conversations here, comprising more messages) 21:09:44 umf gtg 21:09:51 MissPiggy: rjg spg 21:09:56 well i look forward to your implementation 21:10:02 and i'm going to play around with this as a language feature now 21:10:02 bye 21:10:46 Well, when I said messages, I meant conversations >.> 21:11:05 lawl 21:12:59 Ah 21:13:05 My Gmail account looks so clean now 21:14:12 After what? 21:14:38 MissPiggy: http://pastie.org/812719.txt?key=yvxcfkcsixjpvfijd5gug 21:14:41 It looks slick as a language feature 21:14:52 Marking everything as read 21:15:01 Ah. 21:15:24 mmmm 21:15:41 * Sgeo goes to mark all 30398 conversations as unread for no good reason 21:15:44 http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq 21:15:48 MissPiggy: More consistent syntax 21:15:54 I guess the natural thing to do now is generalize it to infinite dimensions 21:16:04 What would that help? :P 21:16:23 MissPiggy: one thing I don't like is 21:16:34 if you have a function that's the composition of two columns, it doesn't need to be a column 21:16:39 in fact it shouldn't be 21:16:40 but 21:16:52 in functional programming you don't have to distinguish columnular and non-columnular functions 21:16:57 it seems a bit awkward to have to do so, in fact 21:17:11 well I should say something here, 21:17:21 suppose we defined t1 = []`snoc`... a bunch of stuff... 21:17:31 and t2 = t1`snoc`... some more stuff... 21:17:50 (note: in mine, since tables would be compile-time, they would "mutate") 21:17:54 (so no need to make new names) 21:18:13 so t1's type would express that it defines N-functions over some (M-constructor'd) datatype 21:18:22 MissPiggy: your system is a vulnerability 21:18:27 and t2 would define more functions over a data type that is an extension 21:18:44 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:47 easy fix though: 21:18:52 suppose that x is a value, and you wanted to apply it 21:18:55 just add constraints requiring proofs 21:18:57 voila, security 21:19:07 you would need to PROJECT and EVALUATE the function out of the table 21:19:08 MissPiggy: apply it? 21:19:11 right 21:19:20 like projeval t1 "f2" x 21:19:32 in mine, just f2 x 21:19:33 :P 21:19:46 yeah 21:20:26 I don't think there is any vulnerability though 21:20:31 I do think http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq is remarkably elegant though 21:20:42 MissPiggy: not if you make sure you have constraints on the functions 21:20:46 yeah 21:20:49 like any good dependent programmer will 21:20:58 plus you'd have to inject code into the system anyway 21:20:58 s/programmer/type system/ 21:20:59 :p 21:21:00 and if you can do that, well... 21:21:02 MissPiggy: touche 21:21:17 maybe we've discovered the Nth major paradigm 21:21:24 table-oriented programming 21:21:28 (not to be confused with SQL :P) 21:21:33 lol 21:21:59 maybe I should use agda :/ 21:22:27 ohhh I just thought of somethingn 21:22:30 * alise tries to translate http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq into Haskell, through whatever tricks necessary 21:22:32 MissPiggy: wut 21:22:44 haha I don't think you can turn that into haskell 21:22:51 worth a try 21:22:56 this this good plugin for Coq I can try out 21:22:59 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 Point is, it has type-level functions and a whole lot of other trickery. 21:25:52 It's everything apart from dependent, pretty much. 21:25:55 TC or not, it still doesn't have lambda 21:26:04 oh well you can do everything in SK 21:26:18 TC means it is equivalent to lambda in computational power, though. 21:26:33 MissPiggy: it does have lambda 21:26:37 you just have to define them elsewhere 21:26:41 And compiling lambda to SK is trivial. Annoying, but trivial... 21:26:41 okay, so it doesn't have lambda 21:26:46 but it has first-class functions (types) 21:31:54 internet archive is really slow today it seems 21:32:07 even more than usually 21:32:38 (theory: it takes as long to go back in time as it took to get to the current point from then originally) 21:32:43 heh 21:33:14 -!- cheater2 has quit (Ping timeout: 252 seconds). 21:33:40 -!- cheater2 has joined. 21:35:06 What good alternatives are there to C++? 21:35:57 C-like alternatives, I mean. Not talking about Haskell here 21:36:05 Sgeo, C? 21:36:17 With OOP, preferably 21:36:21 objective c then 21:36:27 why not haskell? 21:36:57 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 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:35 * Sgeo wikis 21:38:45 Sgeo: C, Objective C, D... 21:38:49 yeah Objective C 21:38:54 Objective D++ 21:38:58 lol 21:39:00 the language with literally every feature 21:39:04 Objective C++ is a real thing. 21:39:15 AND SO IS OBJECTIVE D++ 21:39:38 Just not implemented. 21:39:55 yes it is 21:39:57 apple implement it 21:40:04 and so does gcc because of that 21:40:05 ummm lol 21:40:08 Hm, I shoulld probably learn D 21:40:13 don't. it's shit 21:40:20 How so? 21:40:34 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 It's been like this for years, and I mean years. 21:40:44 Secondly, it is not a designed language. 21:40:51 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 Probably much like being in a different building. 21:47:13 hm? 21:48:14 MissPiggy, I _think_ alise is saying I should switch schools in order to actually get challenging classes 21:48:21 oh 21:48:51 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 Or have done the classes before. :P 21:49:16 You may be a really excellent programmer, but the probabilities are weighted in the direction of bad school. 21:49:43 I know the other students think I'm an excellent programmer.. 21:49:44 MissPiggy: I'm getting the example translated, slowly 21:49:53 Sgeo: They could just be realy bad programmers, though. :P 21:49:59 alise, I think that that's the case 21:50:02 I'm not dissing you, just being all probabilitying. 21:50:37 you're so bayesian! 21:53:10 totally mon 21:54:34 MissPiggy: do you have any idea how many times i've seen the word "kind mismatch" in the past few minutes 21:55:36 hahaha 21:55:46 Kinds are basically the type of tyoes? Maybe is * -> *? 21:56:02 Sgeo you are correct 21:56:27 yar 21:56:39 *words 21:56:50 {-# LANGUAGE KindSignatures, RankNTypes, GADTs, FlexibleContexts #-} 21:56:52 a sure sign of madness 21:58:24 ffff 21:58:27 ohh 22:04:09 * Sgeo tries to make a website that doesn't support Chrome work in Chrome 22:05:19 Does Chrome not support getElementById? 22:06:56 ... 22:06:57 haha 22:07:59 It looks like it should 22:08:06 Some googling suggests it doesn't 22:09:03 It's supported 22:10:18 Ugh 22:10:26 Does it have something to do with the fact that it's in a table? 22:11:45 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 i don't know if you actually wanna get A's, if you do, that might be relevant. 22:13:22 i think he means more "a programming class that isn't really easy" 22:13:52 yeah, probably, that's why i hastily added the second line :P 22:13:57 i'll reread what he said 22:14:27 hmm yeah 22:14:45 then it'd probably feel nice, since taking trivial courses feels is a waste of time 22:14:53 ... 22:14:57 another great sentence 22:15:16 i should stop trying, i clearly haven't woken up yet 22:15:51 They're trivial for me 22:15:58 I don't know if they're trivial for most people 22:16:47 well i mean taking courses that are trivial for you is a waste of time. 22:17:13 I do need to get a degree 22:17:38 i suppose, i prefer to live in the moment 22:18:05 a degree from a bad school sounds exciting 22:18:52 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:19:27 almost? 22:21:16 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 so you need to add that rule 22:21:22 hi coppro 22:21:27 hi 22:21:27 * alise (ehird) 22:21:44 any particular reason? 22:22:11 i think he just likes you 22:22:15 lol 22:22:19 :P 22:22:29 I decided to see if people would treat me differently if they believed I had ovaries 22:22:41 i was like oooh want summa that 22:22:53 but then i realized you were a guy 22:22:57 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 after reading a few of your lines 22:23:03 lol 22:23:04 xD 22:23:13 MY TALKINGS ARE VERY FEMININE 22:23:25 I don't think I behave any different towards women on the internet 22:23:35 did I just PM alise? 22:23:48 this stupid client thinks // means / 22:24:09 real life is a different story :P 22:25:29 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 MissPiggy: do any existing dependent langs have isa :: a -> Set -> Bool 22:25:46 probably 22:26:00 isa?? 22:26:08 you mean like equality check? 22:26:28 oklopol: I suspect the LGBT community has some pitchforks ready for you 22:27:00 :P 22:27:23 i've been known to raise people's pitchforks 22:27:38 ... 22:27:47 "..."? 22:27:49 pervert 22:27:53 there we go 22:28:44 i wish i had water 22:28:46 -> 22:29:32 MissPiggy: anyway do you think Complex :: Set; Complex = {_+i_ m n | m ← Real, n ← Real} is good notation for set construction? 22:29:41 i dunno, I think: 22:29:45 data Complex :: Set where 22:29:48 alise I think isa is probably inconsistent 22:29:56 _+i_ :: Real -> Real -> Complex 22:30:00 is easier to understand 22:30:06 but it's also "specialer" 22:30:07 _+_i? 22:30:09 that {} stuff is horrid 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:11 but I am doing stuff instead 22:35:23 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 14:30:09 that {} stuff is horrid 22:43:18 you're horrid. 22:43:21 14:30:07 _+_i? 22:43:22 nice 22:43:25 alas, both are ambiguous 22:43:29 -!- bsmntbombdood has joined. 22:43:30 3 +i 4 could be 3+(i 4) 22:43:42 3 + 4 i could be 3 + (4 i) 22:44:05 then make i the Imaginary operator 22:44:08 14:29:48 alise I think isa is probably inconsistent 22:44:09 why 22:44:13 it's just type checking 22:44:24 14:23:48 this stupid client thinks // means / 22:44:25 _ + _ :: Real -> Imaginary -> Complex 22:44:29 i didn't see it, my connection went wonky 22:44:32 coppro: no way. 22:44:33 :P 22:44:49 14:23:25 I don't think I behave any different towards women on the internet 22:44:56 you probably do, sexism is incredibly ingrained in society. 22:46:12 coppro: then again ambiguous operators are all the rage 22:46:17 if_then_ plus if_then_else_ 22:46:29 (if x then y else z) could be (if x then (y else z)) 22:46:32 where else is a variable name 22:46:46 not that if_then_ makes any sense without an else clause but still 22:46:57 What about an else by itself 22:47:12 ehird, oh nevermind, since it returns Bool it doesn't matter 22:47:15 Deewiant: that's a name. 22:47:21 MissPiggy: as opposed to? 22:47:24 if it gave some evidence then it might cause a problem 22:47:36 ah 22:47:48 yeah i was wondering whether to make it give evidence, decided against it 22:48:18 _::_ :: a -> (a::Set) -> a 22:48:28 MissPiggy: also I was thinking about: 22:48:40 how to do quantification 22:48:46 id :: λa. a -> a 22:48:46 or 22:48:53 id :: {a::Set} -> a -> a 22:48:54 or even 22:49:14 id :: λ(a::Set). λ(_::a). a 22:49:19 the last one isn't feasible unfortunately 22:49:23 because you can't say λInteger. 22:49:26 use capital lambda instead of small lambda 22:49:36 to be sugar for? 22:49:37 hm 22:49:42 no wait I'm wrong 22:50:07 eh? 22:51:10 Why does a legitimate script feel a need to obfuscate its strings? 22:51:40 I see no good reason to say "\x75n\x64\x65fined" 22:52:52 undfined? 22:52:56 oh 22:52:56 undefined 22:53:00 Sgeo: filtering of something 22:53:10 hm? 22:55:40 maybe undefined is filtered by something 22:58:29 They do the same thing elsewhere in the code 22:58:32 Including error strings 22:58:42 "\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 I don't know; I'm not psychic. 22:59:33 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 probably the latter i guess 23:00:31 I don't even know what that means 23:00:40 which function? 23:01:07 id :: λa. a -> a 23:01:08 or 23:01:13 id :: (a::Set) -> a -> a 23:02:28 erm 23:02:28 or 23:02:32 id :: {a::Set} -> a -> a 23:03:06 oh okay 23:03:07 and ? 23:08:20 [15:44:32]you probably do, sexism is incredibly ingrained in society. 23:09:20 it's in your genes, pal 23:09:26 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:32 of course it is 23:09:57 I certainly treat women differently in person 23:13:02 mm 23:13:03 maybe. 23:13:09 but unless I have a particular reason to do so, I don't associate gender with someone over the internet 23:13:20 likewise for other traits, such as age and race 23:14:24 -!- sshc has quit (Quit: leaving). 23:14:27 Right, but if you know someone's female you'll probably treat them differently. 23:15:01 Depends on the context 23:15:13 but yes 23:19:21 i usually treat women differently because they are completely different 23:20:07 it's those venusian antennas 23:20:37 ISN'T IT THE GUYS WHO HAVE... nm 23:20:45 ... 23:20:52 -!- kar8nga has quit (Remote host closed the connection). 23:21:41 you know what annoys me 23:21:53 Stupidity? 23:21:54 the hardest part of doing lambda calculus and stuff is the variable renaming 23:21:58 it's fucking bullshit 23:22:01 nobody wants to rename variables 23:22:05 stop using a shitty representation 23:22:06 ugh 23:22:49 * coppro ponders a bit of psychology 23:23:23 psychology is too hard 23:23:34 have i mentioned i just love wolframalpha? 23:23:38 that's just what you _think_ 23:23:46 why do you love wolframalpah 23:24:08 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 i don't think it's ever misinterpreted me, even though i just write like i would to a human 23:25:07 cool 23:25:07 It's misinterpreted me :( 23:25:10 especially with set stuff 23:25:13 i'm not saying it's actually that great a parser, it's just others are incredibly stupid. 23:25:19 yeah 23:25:22 agree with that 23:25:29 well i just use it for integrals, because i hate them (suck at them) 23:25:52 what kind of set stuff have you asked it? 23:26:23 hm i definitely had to rephrase things a bit when solving equations/graphing 23:26:39 you solved equations? 23:26:46 may i ask why? 23:27:25 (have you been doing math behind my back! :''() 23:27:45 so how does wolfram alpha work? 23:28:11 fancy parser, then stick the result into mathematica, prolly 23:28:21 it was just something trivial about population growth 23:28:44 it's 1.5 million lines of mathematica, so i assume it's just a list of hardcoded query * response pairs. 23:29:23 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:06 heh 23:30:15 oerjan: okay, that's fine then 23:30:18 i was getting jealous 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 no that's not imagination. those raptors you see coming toward you are _real_. 23:35:16 lol 23:37:19 The worlds that I create in my head 23:37:34 Although both the major one and this one have me as a major Mary Sue 23:37:56 In the major one, I'm essentially God 23:38:02 and in this recent one, I'm fighting God 23:39:09 stop stealing my ideas! 23:56:42 -!- MizardX has quit (Ping timeout: 248 seconds). 23:59:10 -!- gm|lap has joined.