←2014-07-08 2014-07-09 2014-07-10→ ↑2014 ↑all
00:09:24 -!- edwardk has joined.
00:11:34 -!- vifino has joined.
00:22:35 -!- ais523 has quit.
00:22:40 -!- callforjudgement has joined.
00:31:52 -!- callforjudgement has quit (Ping timeout: 245 seconds).
00:32:23 -!- Bicyclidine has quit (Ping timeout: 264 seconds).
00:46:45 -!- nooodl_ has changed nick to nooodl.
00:49:19 -!- ajf has quit (Quit: I quit PHP development! Forever!).
00:50:33 -!- callforjudgement has joined.
00:57:36 -!- Slereah_ has quit (Ping timeout: 255 seconds).
01:01:56 -!- Slereah_ has joined.
01:08:13 <boily> in a strange case of “There's a Trope for That”, I just learned that there is such a thing → http://tvtropes.org/pmwiki/pmwiki.php/Main/CanadaDoesNotExist
01:09:58 -!- d00p_ has quit (Quit: d00p_).
01:10:12 <Slereah_> Americanada
01:12:50 <boily> the USA should split and regroup with some provinces to form Americanada.
01:15:57 <Slereah_> http://www.rathergood.com/beta_recordings
01:16:33 -!- Bike has quit (Ping timeout: 240 seconds).
01:18:41 <boily> Slereah_: what.
01:18:44 -!- Bike has joined.
01:23:45 -!- boily has quit (Quit: Tell the Moon Dog, Tell the March Hare).
01:23:46 -!- metasepia has quit (Remote host closed the connection).
01:35:24 -!- Bike has quit (Ping timeout: 255 seconds).
01:37:36 <Sgeo> I love how questions like "What is the type of ('a' ** 'b'), and does it typecheck?" depend on the type you try to give it explicitly
01:38:01 <Sgeo> I guess you can do similar things in Haskell to some extent
02:01:12 -!- tswett has quit (Quit: tswett).
02:14:16 -!- Bike has joined.
02:19:51 -!- Bicyclidine has joined.
02:24:22 -!- Bicyclidine has quit (Ping timeout: 245 seconds).
02:28:56 -!- Sorella has quit (Quit: It is tiem!).
02:43:41 -!- callforjudgement has quit (Ping timeout: 256 seconds).
02:44:29 -!- vifino has quit (Quit: Ze Cat now leaves...).
02:48:34 -!- callforjudgement has joined.
02:51:59 -!- Bicyclidine has joined.
02:52:04 -!- Bicyclidine has quit (Client Quit).
02:55:28 -!- hogeyui_ has quit (Ping timeout: 260 seconds).
03:06:41 -!- hogeyui_ has joined.
03:09:55 <Sgeo> http://www.cnn.com/2014/07/08/health/smallpox-virus-found/index.html?hpt=hp_c2
03:10:24 <Bike> still pretty sure the correct reaction to seeing a vial labeled "VARIOLA" in a freezer is screaming
03:13:12 -!- d00p_ has joined.
03:41:53 -!- pikhq has quit (Read error: Connection reset by peer).
03:43:09 -!- pikhq has joined.
03:54:50 -!- OriginalOldMan has joined.
03:55:25 -!- nooodl has quit (Quit: Ik ga weg).
04:02:16 -!- OriginalOldMan has quit (Quit: Page closed).
04:06:41 <Sgeo> I think my mom wrote a scientific paper
04:07:37 <Bike> is it good
04:08:02 <Sgeo> I can't access it right now, the only source I found is behind a pay wall, not going to do that tonight
04:08:21 <Bike> if you give me a doi or something i could probably grab a copy.
04:09:16 <Sgeo> I don't know what a doi is, but I can link the two places I see it
04:09:27 <Sgeo> http://journals.lww.com/ajnonline/Citation/1996/11000/PSYCHIATRIC_NURSING__Relaxation_Exercises_Reduce.7.aspx http://jhn.sagepub.com/content/14/3/196.short
04:09:50 <Bike> Document Object Identifier, a GUID system for papers. it'd basically just give me the second link there though.
04:15:13 <Bike> my school doesn't have access to papers from earlier than 2012. sorr-e.
04:16:24 <Sgeo> Ok, thank you anyway
04:21:29 -!- drdanmaku has quit (Quit: Connection closed for inactivity).
04:21:59 -!- ^v has quit (Ping timeout: 252 seconds).
04:31:40 <callforjudgement> the DOI only ever redirects to an official publisher's website that's pretty useless
04:31:59 <callforjudgement> it's mostly useful for getting citation info so that you can search for the paper properly
04:32:16 -!- JWinslow23 has joined.
04:32:22 <JWinslow23> ohai pplz
04:32:55 <JWinslow23> Anyone here?
04:33:00 <Bike> callforjudgement: yeah, that's mostly what i use it for. sometimes navigating publishers' sites sucks.
04:33:03 <Bike> most of the time.
04:33:10 <JWinslow23> I'm searching for a language, but I can't find the page for the life of me.
04:33:20 <JWinslow23> I don't know the name of it.
04:33:20 <callforjudgement> there are people here
04:33:33 <callforjudgement> if you describe the language, we can see if any of us remembers
04:33:33 <JWinslow23> Good.
04:33:41 <callforjudgement> alternatively, if it's simple enough, we could just create it on the spot
04:33:59 <JWinslow23> OK...lessee...the esolang is two-dimensional...
04:34:18 <Bike> i think there's a category for befunge-likes
04:34:30 <JWinslow23> ...and its layout was supposed to overlay a table of all the ASCII values...
04:34:33 <callforjudgement> and a category for two-dimensionals in particualr
04:34:42 <callforjudgement> although, I'm not aware of one that acts like that
04:34:55 <JWinslow23> ...I'm pretty sure there's a Hello World Program made for it...the only program made for it...
04:35:13 <coppro> Sgeo: yhm
04:35:36 <Sgeo> coppro: ?
04:39:07 <coppro> you have mail
04:39:07 -!- JWinslow23 has quit (Ping timeout: 246 seconds).
04:39:28 <Sgeo> Thank you!
04:53:10 -!- JWinslow23 has joined.
04:53:29 <JWinslow23> ohai again
04:54:29 <JWinslow23> I have this one idea for a 1L-type esolang, but it might be too hard to program in.
04:54:53 <JWinslow23> Wanna hear?
04:56:04 <JWinslow23> ...hello? :/
04:56:36 <callforjudgement> we're still here
04:56:42 <callforjudgement> but for me, it's 6 in the morning and I've been up all night
04:56:45 <JWinslow23> Oh. Sorry.
04:56:59 <callforjudgement> so I may not be so coherent
04:57:10 <JWinslow23> And for me, it's about midnight.
04:57:26 <coppro> JWinslow23: too hard to program in is the point
04:57:36 <JWinslow23> So, possible specs:
04:57:49 <JWinslow23> Space: a nop
04:58:14 <JWinslow23> Non space: Some instruction, depending on placrment.
04:58:41 <JWinslow23> So, there's this wheel of commands:
04:59:10 <JWinslow23> INC, DEC, FWD, BAK, IN, OUT
04:59:55 <JWinslow23> (corresponding to + - > < , . in brainf***)
05:00:48 <JWinslow23> Starts at INC, and turns the wheel with every forward movement of the instruction pointer.
05:01:03 <callforjudgement> JWinslow23: have you seen [[e:Turning tarpit]]
05:01:10 <callforjudgement> err, why does my macro no longer work
05:01:14 <callforjudgement> http://esolangs.org/wiki/Turning_tarpit
05:01:16 <callforjudgement> there we go
05:01:16 <JWinslow23> I have.
05:01:30 <JWinslow23> This is 2-d.
05:01:48 <JWinslow23> A 1L-type lang.
05:03:11 <JWinslow23> Anyways, so if an instruction is reached, then execute the current command on the wheel.
05:04:20 <JWinslow23> If an instruction is to the direct left or right of the pointer, then move in the direction opposite the insttuction.
05:05:22 <JWinslow23> If it is one space forwards and one to the side, then turn ss described ONLY IF the current memory cell is nonzero.
05:06:31 <JWinslow23> If at any time the pointer is out of bounds, the program terminates.
05:07:02 <callforjudgement> that doesn't seem that hard to program in
05:07:16 <JWinslow23> Well, my original idea was.
05:07:26 <JWinslow23> My original wheel.
05:07:51 <JWinslow23> It added ROTC, ROTCC, ROTCIF, and ROTCCIF.
05:08:36 <JWinslow23> (rotate clockwise, counterclockwise, clockwise if current cell is nonzero, counter
05:12:43 -!- JWinslow23 has quit (Ping timeout: 246 seconds).
05:22:46 -!- conehead has quit (Ping timeout: 264 seconds).
05:40:21 -!- callforjudgement has quit.
05:58:00 <HackEgo> [wiki] [[Talk:Arborealis]] http://esolangs.org/w/index.php?diff=40112&oldid=40087 * Dweymouth * (+599) question
05:58:47 <HackEgo> [wiki] [[Talk:Arborealis]] M http://esolangs.org/w/index.php?diff=40113&oldid=40112 * Dweymouth * (+1) new paragraph
06:15:38 <HackEgo> [wiki] [[Malbrain]] http://esolangs.org/w/index.php?diff=40114&oldid=36165 * Rdebath * (+159) Add table and retrieve execution explanation from history.
06:16:20 -!- ais523_ has quit (Quit: Page closed).
06:25:48 -!- oerjan has joined.
06:27:31 -!- MoALTz has quit (Quit: Leaving).
06:40:14 -!- d00p_ has quit (Quit: d00p_).
06:44:08 -!- AnotherTest has joined.
06:46:05 -!- nisstyre has quit (Ping timeout: 272 seconds).
07:13:37 -!- nisstyre has joined.
07:26:51 -!- AnotherTest has quit (Ping timeout: 255 seconds).
07:44:21 -!- AnotherTest has joined.
08:10:22 -!- sandpiper has joined.
08:10:30 -!- Iceland_jack has joined.
08:26:34 -!- Patashu has joined.
08:32:19 -!- Patashu has quit (Disconnected by services).
08:32:19 -!- Patashu_ has joined.
09:05:21 -!- MindlessDrone has joined.
09:13:56 -!- sandpiper has quit (Quit: Leaving).
09:37:24 -!- impomatic_ has quit (Ping timeout: 248 seconds).
10:13:56 -!- boily has joined.
10:46:37 -!- Phantom_Hoover has joined.
10:46:55 -!- Phantom_Hoover has quit (Remote host closed the connection).
10:51:43 -!- Phantom_Hoover has joined.
11:02:02 -!- oerjan has quit (Quit: leaving).
11:04:52 <boily> AAAAAH! I FORGOT TO BREAKFAST!
11:04:53 -!- boily has quit (Quit: Poulet!).
11:08:41 -!- nooodl has joined.
11:22:39 -!- MindlessDrone has quit (Quit: MindlessDrone).
11:53:18 -!- yorick has joined.
12:00:35 -!- Sgeo has quit (Read error: Connection reset by peer).
12:40:11 -!- TieSoul-mobile has joined.
12:42:11 -!- TieSoul-mobile has quit (Quit: Bye).
12:43:39 -!- TieSoul has joined.
12:43:52 <TieSoul> Hey
13:05:38 -!- Patashu_ has quit (Ping timeout: 240 seconds).
13:06:06 -!- ^v has joined.
13:07:33 -!- sebbu has quit (Ping timeout: 240 seconds).
13:22:28 -!- sebbu has joined.
13:23:00 -!- sebbu has quit (Changing host).
13:23:00 -!- sebbu has joined.
13:31:48 -!- TieSoul has quit (Ping timeout: 255 seconds).
13:32:56 -!- vifino has joined.
13:41:46 -!- monotone has quit (Remote host closed the connection).
13:42:19 -!- aloril_ has quit (Ping timeout: 264 seconds).
13:48:21 -!- AnotherTest has quit (*.net *.split).
13:48:21 -!- Speed` has quit (*.net *.split).
13:48:21 -!- Frooxius has quit (*.net *.split).
13:48:21 -!- copumpkin has quit (*.net *.split).
13:48:21 -!- vifino has quit (*.net *.split).
13:48:22 -!- Bike has quit (*.net *.split).
13:48:22 -!- mtve has quit (*.net *.split).
13:48:22 -!- yiyus_ has quit (*.net *.split).
13:48:22 -!- glogbackup has quit (*.net *.split).
13:48:22 -!- shachaf has quit (*.net *.split).
13:48:23 -!- int-e has quit (*.net *.split).
13:48:23 -!- EgoBot has quit (*.net *.split).
13:48:23 -!- myname has quit (*.net *.split).
13:48:23 -!- nooodl has quit (*.net *.split).
13:48:23 -!- Slereah_ has quit (*.net *.split).
13:48:24 -!- hogeyui_ has quit (*.net *.split).
13:48:24 -!- Taneb has quit (*.net *.split).
13:48:25 -!- Iceland_jack has quit (*.net *.split).
13:48:25 -!- ineiros_ has quit (*.net *.split).
13:48:25 -!- atehwa has quit (*.net *.split).
13:48:25 -!- diginet has quit (*.net *.split).
13:48:25 -!- erdic has quit (*.net *.split).
13:48:26 -!- nycs has quit (*.net *.split).
13:48:26 -!- quintopia has quit (*.net *.split).
13:48:26 -!- tromp__ has quit (*.net *.split).
13:48:26 -!- augur has quit (*.net *.split).
13:48:26 -!- heroux has quit (*.net *.split).
13:48:26 -!- jj2baile has quit (*.net *.split).
13:48:26 -!- HackEgo has quit (*.net *.split).
13:48:26 -!- mroman has quit (*.net *.split).
13:48:27 -!- jix has quit (*.net *.split).
13:48:27 -!- edwardk has quit (*.net *.split).
13:48:27 -!- tromp has quit (*.net *.split).
13:48:27 -!- idris-bot has quit (*.net *.split).
13:48:27 -!- Melvar has quit (*.net *.split).
13:48:28 -!- nortti has quit (*.net *.split).
13:48:29 -!- douglass_ has quit (*.net *.split).
13:48:29 -!- mihow has quit (*.net *.split).
13:48:30 -!- coppro has quit (*.net *.split).
13:48:30 -!- vravn has quit (*.net *.split).
13:48:30 -!- sebbu has quit (*.net *.split).
13:48:30 -!- Phantom_Hoover has quit (*.net *.split).
13:48:31 -!- pikhq has quit (*.net *.split).
13:48:31 -!- clog has quit (*.net *.split).
13:48:31 -!- variable has quit (*.net *.split).
13:48:32 -!- Gracenotes_ has quit (*.net *.split).
13:48:32 -!- TodPunk has quit (*.net *.split).
13:48:32 -!- Gregor has quit (*.net *.split).
13:48:32 -!- ion has quit (*.net *.split).
13:48:32 -!- elliott has quit (*.net *.split).
13:48:33 -!- ggherdov has quit (*.net *.split).
13:48:33 -!- Burton has quit (*.net *.split).
13:48:33 -!- realz has quit (*.net *.split).
13:48:33 -!- olsner has quit (*.net *.split).
13:48:33 -!- maurer has quit (*.net *.split).
13:48:34 -!- ^v has quit (*.net *.split).
13:48:34 -!- ski_ has quit (*.net *.split).
13:48:34 -!- FreeFull has quit (*.net *.split).
13:48:34 -!- fowl has quit (*.net *.split).
13:48:34 -!- b_jonas has quit (*.net *.split).
13:48:35 -!- lifthrasiir has quit (*.net *.split).
13:48:35 -!- fungot has quit (*.net *.split).
13:48:35 -!- Deewiant has quit (*.net *.split).
13:48:36 -!- yorick has quit (*.net *.split).
13:48:36 -!- nisstyre has quit (*.net *.split).
13:48:36 -!- rodgort has quit (*.net *.split).
13:48:36 -!- FireFly has quit (*.net *.split).
13:48:37 -!- hubs has quit (*.net *.split).
13:48:37 -!- kyhwana_ has quit (*.net *.split).
13:48:38 -!- skarn has quit (*.net *.split).
13:48:38 -!- myndzi has quit (*.net *.split).
13:48:38 -!- qlkzy has quit (*.net *.split).
13:48:38 -!- Zuu has quit (*.net *.split).
13:48:39 -!- fizzie has quit (*.net *.split).
13:56:53 -!- esowiki has joined.
13:56:56 -!- glogbot has joined.
13:56:57 -!- esowiki has joined.
13:56:57 -!- esowiki has joined.
13:57:47 -!- barrucadu has joined.
13:58:59 -!- lambdabot has joined.
14:00:36 -!- nycs has quit (Ping timeout: 255 seconds).
14:01:35 -!- KingOfKarlsruhe has joined.
14:01:40 -!- SirCmpwn has joined.
14:05:35 -!- subleq has joined.
14:35:24 -!- edwardk_ has changed nick to edwardk.
15:10:20 -!- nortti has changed nick to hvidie.
15:10:30 -!- hvidie has changed nick to nortti.
15:38:03 -!- JWinslow23 has joined.
15:42:17 -!- lollo64it has joined.
16:01:08 -!- MindlessDrone has joined.
16:05:29 <JWinslow23> Beatnik cat program:
16:05:31 <JWinslow23> "Output: values displayed as characters."
16:05:47 <JWinslow23> (8 9 16 2 17)
16:06:46 -!- `^_^v has joined.
16:07:31 <JWinslow23> I think that might work.
16:16:15 -!- `^_^v has quit (Quit: This computer has gone to sleep).
16:22:17 -!- JWinslow23 has quit (Quit: Page closed).
16:28:11 -!- AnotherTest has quit (Ping timeout: 264 seconds).
16:38:03 -!- conehead has joined.
16:50:58 -!- idris-bot has joined.
16:52:42 -!- TieSoul has joined.
16:55:44 -!- TieSoul has changed nick to TieSoul-mobile.
16:58:46 -!- MoALTz has joined.
17:08:24 -!- `^_^v has joined.
17:45:37 -!- shikhin has joined.
17:50:41 -!- mhi^ has joined.
17:52:37 -!- TieSoul-mobile has quit (Ping timeout: 256 seconds).
18:02:06 -!- nycs has joined.
18:03:45 -!- `^_^v has quit (Ping timeout: 272 seconds).
18:16:41 -!- impomatic_ has joined.
18:26:09 <HackEgo> [wiki] [[Everett]] http://esolangs.org/w/index.php?diff=40115&oldid=37786 * 162.157.73.59 * (-6)
18:34:14 -!- lollo64it has quit (Ping timeout: 240 seconds).
18:40:40 -!- shikhin has quit (Quit: leaving).
18:45:16 -!- AnotherTest has joined.
18:47:22 -!- oerjan has joined.
18:48:13 <oerjan> why is metasepia conspicuously absent whenever it's too damn hot here
18:48:58 <oerjan> (obvious answer: because boily is only here when it's night in norway.)
18:50:28 -!- ais523 has joined.
18:50:32 <oerjan> fine, let me paste in from the web: METAR: ENVA 091820Z 15005KT CAVOK 30/14 Q1016 NOSIG RMK WIND 670FT 16014KT
18:51:00 <oerjan> @tell boily METAR: ENVA 091820Z 15005KT CAVOK 30/14 Q1016 NOSIG RMK WIND 670FT 16014KT
18:51:01 <lambdabot> Consider it noted.
18:52:43 <oerjan> oh no the weather forecast has changed, now it says 29-30 for the two next evenings as well ;_;
18:54:07 <oerjan> maybe friday will start getting livable again
18:54:48 <oerjan> make that saturday
18:56:24 <oerjan> on the plus side, my apartment is keeping cool. i am wondering if the AC has genuine cooling
18:57:41 <ais523> it's not an AC without that, just a fan heater
18:57:49 <ais523> or, well, if it dehumidifies without cooling, that would also make it an AC
18:58:05 <ais523> but that's a really pointless thing to do because cooling and dehumidifying are pretty similarly implemented
18:58:29 <oerjan> well the thing is in norway heating is usually more needed than cooling
18:59:23 <oerjan> this last week being an exception
19:00:05 <ais523> so the theory is that they might just install a fan heater because it's all that most Norwegians would be likely to need?
19:00:07 <ais523> that makes sense
19:00:56 <oerjan> however, that's probably changed with the modern green housing
19:01:20 <oerjan> now the houses are supposed not to leak heat whenever possible
19:03:46 <oerjan> which means the air circulation system needs a heat pump.
19:10:04 <oerjan> hm the manual says there's a thermostat for it, but there is no door in the system to get to adjust it
19:10:30 <oerjan> ok so i do have AC
19:11:44 <oerjan> speaks about "varmeveksler" which translates as "heat exchanger"
19:35:12 -!- AnotherTest has quit (Ping timeout: 245 seconds).
19:43:03 -!- tromp__ has quit (Ping timeout: 255 seconds).
19:44:52 -!- `^_^ has joined.
19:47:05 -!- nycs has quit (Ping timeout: 256 seconds).
19:50:31 -!- tromp__ has joined.
20:18:32 -!- vifino has quit (Quit: Ze Cat now leaves...).
20:19:06 -!- AnotherTest has joined.
20:24:17 <Taneb> Help someone just called me "Nathan van Wolfstein 3-D"
20:24:23 -!- mhi^ has quit (Quit: Lost terminal).
20:28:49 <ais523> misinterpret the "3-D" as a smiley
20:29:25 <fizzie> It's also missing an "en".
20:30:56 -!- mhi^ has joined.
20:31:10 <ais523> and a g?
20:31:19 <Taneb> That was me, sorry
20:33:03 -!- Bike_ has joined.
20:33:30 -!- Feddit has joined.
20:34:10 -!- Feddit has left.
20:34:27 -!- Bike_ has changed nick to Bicyclidine.
20:43:03 -!- not^v has joined.
21:01:21 -!- vifino has joined.
21:02:58 -!- AnotherTest has quit (Ping timeout: 240 seconds).
21:05:21 -!- Patashu has joined.
21:10:47 <oerjan> wait what g
21:11:04 <ais523> well there's a g in ngevd
21:11:24 <oerjan> hm
21:13:09 <Taneb> ais523, that g stand for George
21:19:12 -!- Patashu_ has joined.
21:19:12 -!- Patashu has quit (Disconnected by services).
21:27:01 -!- MindlessDrone has quit (Quit: MindlessDrone).
21:27:25 <Taneb> Phantom_Hoover, elliott, succession fort once the DF bugfix versions are coming out?
21:30:15 -!- Patashu_ has quit (Ping timeout: 240 seconds).
21:37:33 -!- ais523 has quit.
21:50:50 -!- Sgeo has joined.
21:57:12 -!- boily has joined.
21:58:13 <Phantom_Hoover> Taneb, sure
22:11:58 -!- nooodl has quit (Ping timeout: 240 seconds).
22:21:07 -!- newsham has joined.
22:34:33 -!- ais523_ has joined.
22:45:00 <ais523_> hmm, doesn't the tutorial on the new Haskell homepage fail for people whose names have their letters in ASCIIbetical order?
22:46:50 <shachaf> Perhaps your evil twin has the same name as you.
22:47:07 <shachaf> Perhaps you are the evil twin.
22:47:44 -!- ais523 has joined.
22:48:00 <boily> perhaps you are the resonance between two elemental twins?
22:50:08 <ais523_> "like ais523, but less evil" is a scary thought
22:50:12 <ais523_> although I conclude that it's possible
22:50:36 <boily> @massages-loud
22:50:36 <lambdabot> oerjan said 3h 59m 35s ago: METAR: ENVA 091820Z 15005KT CAVOK 30/14 Q1016 NOSIG RMK WIND 670FT 16014KT
22:50:49 <boily> oerjan: GASP! +30 in Norway?
22:51:11 -!- metasepia has joined.
22:51:12 <boily> ~metar CYUL
22:51:12 <metasepia> CYUL 092200Z 26009KT 30SM FEW040 FEW060 22/14 A2980 RMK CU1SC1 SLP091 DENSITY ALT 1100FT
22:51:19 -!- Sorella has joined.
22:51:25 <boily> noooooooooooo! I won't accept that! unpossible!
22:51:33 <ais523_> boily: oerjan's been talking about how this is the first time it's ever been relevant that his AC is not just a fan heater
22:51:41 <ais523_> but actually a genuine AC
22:53:50 <boily> we live in interesting times...
22:55:23 <oerjan> the norwegian definition of "tropical night" is a night where temperatures never go below 20. apparently this heat wave is the first time trondheim has ever had two such nights in a row.
22:57:06 * boily wildly flails around in utter disbelievement. “twenty puny degrees? NONSENSE!”
22:57:30 <oerjan> celsius hth
22:58:18 <ais523> 20 is one of those numbers that's very different in C and F
22:58:44 <oerjan> mind you, that happened _before_ day temperatures crept up to 30
22:59:01 <oerjan> or well that was actually evening in that metar
23:01:26 <ais523> why are separation types so hard to find information about in search engines
23:01:39 <ais523> my problem is that "separation" and "type" are both pretty common words
23:01:53 <ais523> so I have to add extra words that don't match my query but are commonly used in the field, like "proof"
23:01:57 <ais523> to increase the number of relevant results
23:02:01 <ais523> from 0
23:02:34 <ais523> ah, "separation logic" is the more usual term
23:02:42 <ais523> silly curry-howard, confusing terminology for everyone
23:03:52 <ais523> anyway, I'm not quite sure how to move forwards at this point; I basically have two methods
23:04:06 <oerjan> ok this article says today was the hottest day in trondheim since 1945.
23:04:16 <ais523> one is the copout of effectively defining one specific rank-2 type as a special case in the syntax
23:04:26 <oerjan> um hottest july.
23:04:46 <ais523> which basically gives me a language with half the limitations of SCI, which is nonetheless better than SCI because it doesn't have the other half
23:05:10 <ais523> and the other method is to attempt to find some sort of definition of copolymorphism, which is awkward because the language doesn't have polymorphism
23:05:15 <ais523> (except in the C++ template sense)
23:06:03 <ais523> hmm… in Algol 68, "skip" was an arbitrary value of any given data type
23:06:09 <ais523> but in mathematical Algol, it's a no-op command
23:06:23 <ais523> oh, that sort-of makes sense
23:06:25 <oerjan> i think haskell's ST may originally have been implemented as a special case before rank-2 types were implemented generally.
23:06:51 <ais523> anyway, all this mess came about because SCI is pretty awkward as type systems go
23:07:02 <ais523> back when I was a first-year PhD student, it became reasonable
23:07:15 <ais523> but I started coming across more and more awkwardnesses
23:07:35 <ais523> and some time after I'd decided it lead to a bunch of problems, I showed it to a conference full of linear logicians
23:07:54 <ais523> and the typical reaction was "why would you do that?"
23:08:33 -!- conehead has quit (Ping timeout: 240 seconds).
23:08:57 <ais523> SCI isn't really very eso as languages go, I suppose
23:09:21 <ais523> its main weird/eso feature is that "f x y" and "f (x, y)" are not actually interchangeable
23:09:29 <ais523> curry exists, but uncurry doesn't
23:10:12 <Sgeo> Noted: My dad still is not reliable, and my opinion is _still_ worthless to him
23:10:23 -!- not^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
23:10:50 <ais523> ^v's alternate nick's username is confusing me a bunch
23:11:01 <ais523> mostly because I'm unsure whether to interpret the tilde as another "not"
23:11:19 <oerjan> argh now the 29 degrees is extending to the saturday forecast as well
23:12:06 <Sgeo> Well, ^v is not v, so not^v is not not v, so not^v is v, so not^v and ^v are different people
23:12:41 <boily> ~duck tweedeldum
23:12:42 <metasepia> --- No relevant information
23:12:46 <ais523> so which of them is ~notnot^v?
23:12:52 <ais523> ~duck tweedledum
23:12:53 * boily *MAPOLES*
23:12:53 <metasepia> Tweedledum and Tweedledee are fictional characters in an English nursery rhyme and in Lewis Carroll's Through the Looking-Glass, and What Alice Found There. Their names may have originally come from an epigram written by poet John Byrom. The nursery rhyme has a Roud Folk Song Index number of 19800. The names have since become synonymous in western popular culture slang for any two people who look and act in identical ways, generally in a derogatory c
23:13:05 <Bicyclidine> gotcha
23:13:15 * boily 's mapole swing misses, goes around, and thwacks boily behind the head
23:16:10 <ais523> hmm: "two things are proved equivalent, and yet people continue using both sets of terminology" is something that I already hate, despite only having got caught up on it a few minutes ago
23:16:47 <Sgeo> Turing machine and lambda calculus are equivalent in a sense, but still distinct
23:18:16 <ais523> bleh, I ate dinner just an hour or so ago, do I eat antilunch already?
23:18:21 <ais523> I guess I may as well, given that I'm hungry
23:20:25 <ais523> another thing that annoys me: I have two keyboards within about 25 centimetres of me; both have numlock keys; neither has a particularly noticeable numlock indicator
23:20:47 <ais523> the laptop keyboard doesn't seem to have one at all; the desktop keyboard in AZERTY does but it's basically impossible to see at this distance, and this distance is not very long
23:22:49 <Phantom_Hoover> Sgeo, was that just... something that came to mind?
23:23:20 <Sgeo> Phantom_Hoover: I thought it was relevant to ais523's complaint
23:24:11 <ais523> well, the advantage there is that there isn't a 1-to-1 correspondence between Turing machine components and lambda calculus components
23:24:18 <ais523> so you don't get people naming one after the other, inconsistently
23:25:02 <ais523> also, I just saw an interrobang used in a context where a question mark would have made the sentence have an entirely different meaning
23:25:09 <ais523> this saddens me, because I dislike interrobangs
23:25:10 -!- monotone_ has quit (Quit: "I can hear myself... I think I'm a bit afraid.").
23:25:25 <ais523> an exclamation mark would probably have worked, I guess
23:28:29 -!- monotone has joined.
23:38:39 -!- oerjan has quit (Quit: leaving).
23:46:18 -!- Bicyclidine has quit (Ping timeout: 240 seconds).
23:55:50 <Phantom_Hoover> ais523, that's the entire reason interrobangs are a good idea...
23:57:49 <Melvar> ais523: You use numlock?
23:58:12 <ais523> Melvar: if I'm using the numeric keypad for almost anything (except playing NH4), the state of numlock is relevant
23:58:22 <ais523> so it helps to know whether it's on or off before I start pressing buttons
23:59:03 <Melvar> On that note, what do you use the keypad for on a non-neo keyboard layout?
23:59:46 -!- yorick has quit (Read error: Connection reset by peer).
23:59:55 <ais523> "neo layout"?
←2014-07-08 2014-07-09 2014-07-10→ ↑2014 ↑all