00:05:39 -!- vanila has quit (Quit: Leaving). 00:22:11 EXPBLARGL': given N, take the Nth prime number and split every 3 bits to get a brainfuck program. 00:31:16 -!- GeekDude has joined. 00:34:45 -!- not^v has joined. 00:39:11 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 00:40:55 Jafet: what is the proportion of prime numbers that yields correct brainfuck programs? 00:41:02 and terminating brainfuck programs? 00:41:28 -!- Phantom_Hoover has joined. 00:41:52 and with that I wish you all a good night 00:42:16 -!- Koen_ has quit (Quit: The struct held his beloved integer in his strong, protecting arms, his eyes like sapphire orbs staring into her own. "W-will you... Will you union me?"). 00:45:29 -!- doesthiswork has joined. 00:49:25 neither http://esolangs.org/wiki/Underload nor http://esolangs.org/wiki/INTERCAL has been a featured page?!??! 00:50:30 I don't know, but I think it probably ought to be 00:51:26 cpressey: basically the problem is that elliott keeps making me do the featured article process, so I can't really feature languages I've had a large hand in for fear of bias accusations 00:51:47 admittedly I didn't invent INTERCAL, but I am responsible for much of its recent development 00:51:51 Then other people should try to help too? 00:52:06 it's prec prec prec prec 00:52:08 I nominate cpressey. he's a sysop and everything 00:52:21 -!- GeekDude has quit (Quit: ZNC - http://znc.in). 00:52:48 I nominate Linus Torvald 00:52:58 I second that nomination 00:53:16 hopefully linus torvalds will go nowhere near the esolangs wiki 00:54:30 I nominate elliott, because because something something elliott something. 00:54:32 I'd be honoured if he did, but I think he has better things to be doing 00:54:39 so, is it an issue of needing seven proxies so skiddies don't shit up the place, or what, elliott 00:54:44 I want to nominate cpressey 00:54:55 that said, the last C-INTERCAL release /was/ at the request of Donald Knuth 00:54:58 like shitting o people that deserve it? ais523 00:55:05 we went really fast on that one, just in case it was somehow holding up TAOCP 00:55:10 dulla: coherency helps 00:55:37 All I know is some big wig, probably torvald gordon ramseys the tech world 00:55:55 ok 00:56:00 torvald,* 00:56:14 are you going to get more coherent over time or should I just put you on ignore now 00:56:25 I'm having a bad day? 00:56:28 dulla: I thinkg to gordonramsey is a perfectly cromulent verb. 00:56:33 accepted 00:56:45 s/g\b// 00:57:05 english, where everything is a verb, and an idiom 00:57:28 behind seven layers of postmodernism irony, more like it 00:58:16 Can someone invent a VCS that works on .doc files? 00:58:31 oren: I thinkg M-Files already does it. 00:58:58 (ah bordel de... why must I type a g after a k?) 00:59:07 oren: Do you need such thing so much? 00:59:09 there's also the "track changes" thing built into Word but it's really bad for VCS purposes IMO 00:59:28 you could also just put the .doc files in git or something, it'll still track versions 00:59:31 and Word has a diff feature 00:59:34 vcs? 00:59:41 dulla: version control system 00:59:43 dulla: version control system. 00:59:46 http://ben.balter.com/2015/02/06/word-diff/ 00:59:56 -!- GeekDude has joined. 01:00:14 Although Microsoft Word isn't really the best way to do these kind of things anyways especially use with VCS 01:00:28 oren: ^ 01:00:42 hm, http://blog.martinfenner.org/2014/08/25/using-microsoft-word-with-git/ looks fun too 01:03:51 "As you work, Word Diff sits on a server (in my case Heroku), waiting for you to push your changes. When you do, it springs into action, automatically converting the Word document to Markdown after each commit:" 01:04:03 I'm trying to work out whether this is better or /even worse/ than Word's built-in diff funciton 01:05:20 it assumes that Word documents can't have complex formatting at all 01:05:34 which in turn, implies that whatever task you're doing, it's one for which Word is the wrong tool 01:06:04 well, it assumes that you're okay with diffs that ignore complex formatting things most of the time 01:11:06 or makes noobish tuples 01:11:20 (, "words") 01:15:38 and then probably highlight color it to preserve it 01:23:45 what 01:36:49 -!- oerjan has joined. 01:37:44 @messages- 01:37:44 Taneb said 1h 49m 11s ago: Because of you, "hth" has entered my general vocabulary. I am not happy about this circumstance. 01:38:17 \o/ c.c.c \o/ 01:38:17 | c.c.c | 01:38:17 | c.c.c | 01:38:17 /^\ c.c |\ 01:38:17 >\ c.c /´\ 01:38:59 hellørjan! 01:39:04 ahoily! 01:39:24 myndzi: your script is still broken hth 01:39:50 `echo hi 01:39:54 hi 01:46:40 > read "(24)" :: Int 01:46:41 24 01:46:44 fancy 01:50:46 > read "(((((())))))" 01:50:47 () 01:56:02 I almost written the session 63 01:56:32 then you'll have to start using 6 bit numbers! 01:56:46 wait 01:56:47 7 01:57:13 another one-off joke ruined by off-by-one error 01:57:34 Well, I am using entirely decimal numbers in ASCII for the session numbers here anyways anyone who want to store in binary should probably use at least 16-bits though 01:58:45 i see you are expecting to go on for a while. 01:59:14 -!- not^v has quit (Ping timeout: 246 seconds). 01:59:25 I don't actually know how long it expects to go on, but I expect 16-bits is going to be enough even if it is longer than expected. 02:03:08 what is hth? 02:03:17 `? hth 02:03:22 hth is help received from a hairy toe. It is not at all hambiguitous. 02:03:41 seems wrong 02:04:36 are you saying that doesn't help? 02:05:17 -!- not^v has joined. 02:05:20 hackego is a hackkkkk 02:05:43 `? HackEgo 02:05:55 HackEgo, also known as HackBot, is a bot that runs arbitrary commands on Unix. See `help for info on using it. You should totally try to hax0r it! Make sure you imagine it's running as root with no sandboxing. 02:06:01 it is at least slow 02:06:07 oerjan: 6 bits is enough to fit 0 to 63, hth 02:06:19 olsner: curses! 02:07:15 this may or may not mean that your joke is still off by one, because 64 will need an extra bit 02:08:08 dead horse floggers anonymous is thataway ---> 02:08:22 u mad bro? 02:08:43 I MAD LIKE HELL AND CANOT TAKE IT ANY MORE 02:09:11 you should become a CTO 02:09:26 I hear when the servers go down, the server admins are the least of your problems 02:09:53 though that story was probably a joke, it's probably not a lie 02:09:54 no intention to become any kind of O 02:10:07 yoC*O 02:10:56 in your case it would have to be CTØ 02:11:25 or CTꙮ 02:11:36 `unidecode ꙮ 02:11:37 if only I knew what encoding I need to see that 02:11:46 [U+A66E CYRILLIC LETTER MULTIOCULAR O] 02:11:57 dulla: utf8 hth 02:12:14 was that the first unironic "u mad" in this channel 02:12:17 a milestone 02:12:35 now _font_ might be a bit harder. 02:12:40 I'm already utf-8, oerjan 02:12:47 elliott: is anything dulla says unironic? 02:12:55 uh 02:13:06 oerjan: if the answer is no then it might as well be yes 02:13:13 fancy 02:13:17 if you hide absolutely everything behind irony I'm just going to take you sincerely :p 02:13:20 -!- ProofTechnique has joined. 02:13:42 I don't think my oration skills are good enough for intentional irony 02:13:55 suuure 02:13:57 `addquote oerjan: if the answer is no then it might as well be yes 02:14:01 that one's good both in context and out of context 02:14:05 1232) oerjan: if the answer is no then it might as well be yes 02:14:57 dulla: anyway if it's any consolation i cannot see the multiocular o in my client either. 02:15:07 It's not descriptive 02:15:18 multiocular is not in my scope 02:15:23 it it a double o? 02:15:24 I can't in mine either, despite the fact that I recently installed a font whose entire purpose is that it contains obscure Unicode 02:15:32 i can only imagine its greatness. or check the logs. 02:15:48 or search the unicode site for it 02:16:20 alternatively, i can cut and paste it into my browser, which shows it just fine. 02:17:07 mine still doesnt like it 02:17:47 -!- ProofTechnique has quit (Ping timeout: 245 seconds). 02:18:01 * oerjan checks the repository browser now that HackEgo is present again 02:18:19 the only thing of note is shachaf removing pbflistdeluxe. 02:19:18 dulla: i believe there's a separate double o character 02:19:47 Ꙫ 02:20:07 that one has upper and lower case variants 02:21:23 `unidecode Ꙭ 02:21:24 [U+A66C CYRILLIC CAPITAL LETTER DOUBLE MONOCULAR O] 02:21:57 those cyrillic monks had a strange relationship with eyes 02:23:08 https://en.wikipedia.org/wiki/Double_O_(Cyrillic) is one my browser doesn't show either 02:25:20 They don't even agree how many eyes seraphim have, I think? 02:30:23 @unmtl StateT IO 02:30:24 Plugin `unmtl' failed with: `StateT IO' is not applied to enough arguments, giving `/\A B. IO -> A (B, IO)' 02:30:30 @unmtl StateT s IO 02:30:30 Plugin `unmtl' failed with: `StateT s IO' is not applied to enough arguments, giving `/\A. s -> IO (A, s)' 02:30:35 @unmtl StateT s IO a 02:30:35 s -> IO (a, s) 02:31:10 zzo38: it's probably more than you can draw, anyway. 02:36:22 for the sake of fantasy i would like you all to believe that i have irc pings hooked up to an alarm <-- works for me 02:46:30 -!- bb010g has joined. 02:49:47 -!- Phantom_Hoover has quit (Ping timeout: 250 seconds). 03:13:33 Note to self: building a massive watermill complex to power your massive water pumping complex does not work when the pumps drain the very water that powers the watermills. 03:15:32 oren: playing dwarf fortress? 03:15:37 yeah 03:16:04 now I have watermills over dry land 03:16:19 fancy 03:16:32 r.i.p. obsidian apocalypse 03:16:54 I need to rethink this 03:17:48 Maybe I'll route a few aquifers into the cistern 03:20:45 (The cistern exists because the river stops during the winter) 03:21:45 Here is the massive water mill complex http://snag.gy/Z4QOq.jpg 03:25:13 It is built to provide 1000 units of power, currently providing 300, which isn't enough to move it 03:25:23 Sorry, 2000 03:33:23 i have the feeling this is a dwarf fortress thing 03:36:51 dulla: yup. It is part of a plan to glass the whole panet 03:37:01 *planet 03:37:40 needs more fire 03:37:49 -!- boily has quit (Quit: CLARIFIED CHICKEN). 03:37:53 recall the blunderbuss minecart exploit 03:37:59 oh god 03:38:13 the things you can do with that 03:38:51 Well, eventually the watermills will be self-powered when the cistern has been filled properly. 03:39:29 So then I'll have lots of power available to power, well, anything I want 03:39:42 and then there is the catapult exploit, I wonder if that works with warheads, too 03:40:19 though, you honestly don't need it for catapults, stones are cheap as dirst 03:40:22 dirt 03:40:41 -!- not^v has quit (Ping timeout: 252 seconds). 03:40:59 Ooh a cyclops. pull the lever of death, and pump the pumps of death! 03:41:16 -!- callforjudgement has joined. 03:41:50 currently, the pumps of death are dwarfpowered. Soon, very soon, they will be water-powered. 03:43:24 Wouldn't it be more efficient to have more pumps? 03:43:28 Keep the pumps 03:44:02 -!- ais523 has quit (Ping timeout: 245 seconds). 03:46:17 http://snag.gy/6hG8F.jpg shown is a cyclops murdering the merchants, the entrance (currently being pumped full of water to prevent any dwarves being stupid enough to run outside), and part of aqueducts running to the power plant 03:46:50 Does pressurised water still do that thing? 03:46:57 Where it moves faster than a game tick? 03:47:38 It'd be a great way to make sure things in the aquaduct stay in the aquaduct 03:47:49 `danddreclist 63 03:48:04 danddreclist 63: shachaf nooodl boily \ http://zzo38computer.org/dnd/recording/level20.tex 03:50:17 The merchants are leaving, porbably because their merchandise is being carried away by pressurized water 03:50:45 oh and because most of them have been dismembered by a cyclops 03:51:14 it's probably the dismemberment 03:51:28 You know how the merchants can't take the heat 03:51:31 :^) 03:52:13 Do you like this level20.tex? This is the one involving the rune caster 03:53:45 the cyclops apparently dorwned before the magma could even getnear it 03:54:04 or maybe the merchants killed it. 03:58:23 "some migrants have arrived, despite the danger" 03:59:28 no rimshots ;_; 04:00:46 Oh come on guys, come right on in, never mind the drowned merchants and cyclopes... 04:07:29 -!- MDude has changed nick to MDream. 04:08:38 http://snag.gy/Obzd2.jpg 04:22:24 -!- callforjudgement has quit (Read error: Connection reset by peer). 04:22:32 -!- callforjudgement has joined. 04:26:34 eek anagol's recent entries has moved too fast 04:28:05 surely it used to be more than 24 hours before? 04:34:19 -!- cpressey has quit (Ping timeout: 256 seconds). 04:41:19 -!- cpressey has joined. 05:09:24 -!- ProofTechnique has joined. 05:11:35 -!- callforjudgement has quit. 05:12:06 -!- callforjudgement has joined. 05:17:09 -!- GeekDude has quit (Quit: {{{}}{{{}}{{}}}{{}}} (www.adiirc.com)). 05:36:26 -!- dianne has quit (Ping timeout: 264 seconds). 05:38:10 -!- dianne has joined. 05:38:58 -!- chaosagent has joined. 05:39:16 -!- doesthiswork has quit (Quit: Leaving.). 05:54:46 -!- callforjudgement has quit. 05:55:02 -!- callforjudgement has joined. 06:05:14 -!- cpressey has quit (Ping timeout: 264 seconds). 06:06:33 Oh shit, a miner was caught in a cave in, got confused by the dust, and fell into the cistern. 06:07:33 is the water undrinkable now 06:08:22 I dunno. Hopefully we can wash the blood away after the fishermen retrieve the corpse. 06:08:25 eau de dorf 06:09:23 This is why I hate using cave ins, though it is sometimes necessary 06:10:07 will they now all die from waterborn disease 06:10:41 I don't think that's modeled, though I could be wrong. In any case they have plenty of booze to drink 06:11:02 ah. 06:12:10 The cistern is for the generation of energy during the winter when the river stops. 06:12:13 -!- cpressey has joined. 06:13:23 holy crap, hes actually alive still. 06:14:00 and he swam out! he's a good swimmer I guess 06:14:53 all's well that ends well 06:15:38 with luck now I can pressurize the cistern 06:16:18 thus having a way to literally blast enemies to death 06:27:48 is this the onion <-- possibly r/nottheonion? 06:28:18 oh it's pretty old 06:29:55 -!- cpressey has quit (Ping timeout: 256 seconds). 06:37:04 -!- cpressey has joined. 06:40:17 -!- hjulle has quit (Ping timeout: 245 seconds). 06:44:46 It appears that drowning merchants is a good way to get free stuff 06:46:18 That's your way of getting free stuff? 06:46:54 Well they come every season, even if i drown them every season, so yeah 06:47:25 I seal the doors and pump water into the trade depot 06:47:54 It seems like merchants should sue you if that happen a lot it will be recognized? 06:48:08 I dunno, we'll see 06:48:23 If they try to sue me I'll drown thelawyers 06:52:32 -!- cpressey has quit (Ping timeout: 246 seconds). 06:52:33 @tell fizzie btw the wiki bridge isn't working either hth 06:52:33 Consider it noted. 06:53:53 -!- cpressey has joined. 06:55:43 `addquote cpressey, Agda is a function that maps cabal install to an electric heater 06:55:56 1233) cpressey, Agda is a function that maps cabal install to an electric heater 06:56:31 -!- oren has quit (Ping timeout: 244 seconds). 06:58:39 O, that's what it is? 06:59:06 -!- cpressey has quit (Ping timeout: 244 seconds). 07:01:43 I wish Haskell would steal Agda's operator syntax. If then else is so nice there. 07:42:46 -!- CADD has joined. 07:57:25 -!- callforjudgement has quit (Ping timeout: 264 seconds). 08:29:42 -!- oren has joined. 08:32:09 I am now testing to see if killing merchants over and over has any consequences 08:35:06 I have started a new game, and built the depot in an area designed so I can flood it whenever I want 08:56:50 -!- CADD has quit (Ping timeout: 264 seconds). 10:02:18 -!- Phantom_Hoover has joined. 10:16:51 -!- cpressey has joined. 10:17:06 I just wrote my first Agda program! 10:17:14 Actually, I typed it in from a book 10:17:31 Just like the 80's 10:21:03 fancy 10:22:17 * Taneb hello 10:22:44 hi 10:23:14 god daneb 10:23:20 and yes, I am an esowiki sysop I think, so if someone wants to bug me to slap a green checkmark on the Underload page and put an abstract on the front page,... do that 10:23:42 how hard can it be 10:24:56 -!- oerjan has quit (Quit: Famous last words). 10:25:28 -!- oerjan has joined. 10:25:45 cpressey's, that is. 10:25:47 -!- oerjan has quit (Client Quit). 10:26:38 * cpressey must've missed something 10:27:30 or not 10:30:20 oh, oh, "famous last words", right, right 10:30:27 this is mediawiki we're talking about 10:52:29 -!- kapil___ has quit (Quit: Connection closed for inactivity). 11:01:47 Jafet: I did consider prime numbers, but, y'know... PRIMES is in P. can't be too careful. 11:02:29 -!- cpressey has quit (Quit: leaving). 11:39:51 -!- SopaXorzTaker has joined. 11:40:37 Why does that thing have such a ridiculous number of underscores in it. 11:40:48 -!- zemhill___ has quit (Remote host closed the connection). 11:41:11 -!- zemhill has joined. 11:43:21 Oh, the wiki bridge. Blah. I'll try to remember to fix that, though it would be easier with proper internet. 12:00:04 -!- vanila has joined. 12:00:34 -!- Patashu has quit (Ping timeout: 255 seconds). 12:16:25 -!- kapil___ has joined. 12:38:00 -!- chaosagent has quit (Ping timeout: 252 seconds). 13:06:48 -!- oren has quit (Quit: Lost terminal). 13:31:29 http://zzt.org/ 13:37:29 http://jzt.xyz/worlds/village-of-jzt 13:54:19 -!- boily has joined. 13:57:39 -!- boily has quit (Client Quit). 13:59:46 -!- boily has joined. 14:06:57 elliott: helliott. CAO is down :( 14:09:23 -!- reynir has quit (Quit: brb). 14:12:20 boily: play on cdo or cszo or whatever? 14:12:26 there's like fifty servers these days aren't there 14:17:21 it doesn't feel right, but I'm on CDO. 14:19:13 cdo has always been the cool server 14:19:28 such hugeterm :( 14:19:44 let me dehuge my term. 14:21:13 I have no idea whaty ou do when you do that but it definitely doesn't make your terminal any smaller :P it's fine though I can just make my font tiny 14:23:32 I put in 80x24 for the max width and height? 14:23:49 I mean, you can tell there's more than 80 columns and 24 rows to your terminal right now, right >.> 14:23:56 there's 213x57 :p 14:24:09 it's fine though I just made my font smaller and now it fits on my screen 14:24:24 aaaah. it goes with the terminal size. makes sense. tdh 14:24:37 I like my terminal to be full screen :D 14:26:13 you could "stty cols 80 rows 24" before running ssh I guess but that'd lead to a hell of a lot of wasted space 14:28:40 darn. got anted. 14:28:52 * boily is hungry and should go breakfast... 14:29:29 congratulations 14:33:17 -!- heroux has quit (Ping timeout: 256 seconds). 14:35:06 -!- heroux has joined. 14:36:57 -!- MDream has changed nick to MDude. 14:42:29 -!- kapil___ has quit (Quit: Connection closed for inactivity). 15:13:17 -!- hjulle has joined. 15:23:58 -!- int-e has quit (*.net *.split). 15:23:59 -!- kline has quit (*.net *.split). 15:24:05 -!- int-e has joined. 15:24:05 -!- lambdabot has quit (Quit: brb). 15:25:41 -!- kline has joined. 15:28:06 what program could i use on linux to measure/grapha processes memory use? 15:28:16 -!- doesthiswork has joined. 15:28:34 -!- lambdabot has joined. 15:29:45 elliott: breakfasting is dangerous here. a haircut happened. 15:30:04 vanila: vanelloa. ksysguard perhaps? 15:59:55 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 16:02:02 -!- Phantom_Hoover has joined. 16:03:46 -!- SopaXorzTaker has quit (Ping timeout: 265 seconds). 16:16:15 -!- SopaXorzTaker has joined. 16:24:13 -!- SopaXorzTaker has quit (Read error: Connection reset by peer). 16:26:40 -!- aretecode has quit (Read error: Connection reset by peer). 16:30:48 -!- aretecode has joined. 16:44:17 @tic-tac-toe 16:44:17 how about a nice game of chess? 16:46:37 @fresh 16:46:37 Hang 16:53:00 -!- GeekDude has joined. 16:59:42 -!- Koen_ has joined. 17:00:30 -!- Phantom_Hoover has quit (Ping timeout: 244 seconds). 17:00:36 -!- Phantom__Hoover has joined. 17:02:21 -!- Tritonio has joined. 17:02:34 -!- FreeFull has quit (Quit: BBL). 17:13:27 @fresh? 17:13:27 Unknown command, try @list 17:17:47 @help fresh 17:17:47 fresh provides: freshname 17:17:50 @help freshname 17:17:50 freshname. Return a unique Haskell project name. 17:18:44 It starts out with "Ha" and adds some random letter. VERY useful. 17:18:54 @fresh 17:18:54 Hanh 17:19:03 it counts up 17:19:09 its generating a fresh symbol 17:19:19 @@ @pl @fresh 17:19:20 Plugin `compose' failed with: Unknown command: "fresh" 17:19:27 @fresh 17:19:27 Hani 17:21:22 vanila: ah. 17:25:59 my program has a new bug 17:26:08 it is segfaulting before it even reaches line 1 17:26:16 i dont know what is going on ! 17:27:48 how do i even debug this. 17:31:31 vanila: which language? 17:31:33 @fresh 17:31:33 Hanj 17:31:38 @fresh 17:31:38 Hank 17:32:01 c 17:33:32 what #includes do you have? any esoteric, anormal, unusual or experimental libraries? 17:38:32 nothing really crazy 17:38:37 it was working a second ago 17:38:40 and we just changed one function 17:38:43 im totally stumped 17:42:25 what function? 17:42:36 main 17:42:43 also did you include some .h that you wrote yourself? 17:43:01 yes 17:43:07 and which you changed less than a second ago? 17:50:24 it's really fascinating a weird way 17:50:32 i hope i get to the bottom of it, but i really have no idea how 17:50:41 i looked at the assembly code for the prelude of main but i cant understand it 17:53:30 vanila: can you show us what you changed in the .h ? 17:56:49 i didnt change any headers 18:00:15 and if you put a putstr as the very first line of the main it's not printed out? 18:00:22 yeah! 18:00:25 thats whats so crazy 18:00:31 or a printf("\n"); 18:00:32 that shouldn't be possible 18:01:00 (don't omit the \n to flush the output) 18:02:33 -!- Phantom__Hoover has quit (Ping timeout: 250 seconds). 18:35:33 -!- cpressey has joined. 18:35:43 sigh, EXPBLARGL fails 18:35:52 aw 18:36:08 i wonder if it's theoretically impossible cpressey - maybe focus on proving that rather than making a language? 18:36:13 the compiler can always artificially extend the program by adding e.g. +- to the front of it, then it knows there's a shorter program 18:36:48 i'm sure it's not theoretically impossible, because int-e 18:37:16 turn brainfuck program into integer, program is ackermann of that integer 18:40:15 but it has sort of raising an interesting conjecture, which is 18:40:43 if the mapping from TM's to language X programs is complex, running programs in language X will also be complex 18:41:30 which sounds perfectly intuitive, but -- no idea how one would go about proving it 18:41:51 other things I have failed at this weekend: Agda 18:42:02 yes I agree about the 'if mapping, then running' thing 18:42:13 that's what I realized from the idea of encrypted source code 19:06:12 -!- TieSleep has changed nick to TieSoul. 19:12:28 -!- boily has quit (Quit: RELATIVE CHICKEN). 19:14:47 hmm, maybe EXPBLARGL could force to try all the permutations of the program -- wouldn't work well with brainfuck because +- = -+ ... but maybe some other language 19:16:06 nah, i think you could still inject some kind of "identity" instruction, then you know there's another permutation that also works 19:16:10 oh well 19:16:18 maybe i'll keep banging my head against agda 19:16:39 i could help with agda maybe? 19:16:44 i used it ages ago 19:18:27 cpressey: did you ever figure out the Burro/Cabra type things 19:18:51 https://www.youtube.com/watch?v=uxRjp4LVuo4 19:18:52 YouTube 「title: Amor incondicional entre un burro y una cabra」「uploaded by: Univision Noticias」「duration: 00:01:21」「views: 6413」「likes: 67」「dislikes: 0」 19:19:14 uh 19:19:18 -!- ChanServ has set channel mode: +o elliott. 19:19:20 -!- elliott has kicked bluckbot bluckbot. 19:19:26 who do I blame 19:19:41 2015-02-17.log:07:08:01 oerjan kick bluckbot 19:19:42 ok. happily 19:19:43 -!- elliott has set channel mode: -o elliott. 19:20:01 that's one garish YouTube logo colour 19:20:18 Unconditional love between a donkey and a goat 19:20:21 translation 19:25:03 elliott: define "type things" 19:25:09 Burro is ok, Cabra is silly 19:25:17 stronger algebraic structures 19:25:27 Oh, like rings? Ha ha no. 19:26:00 There, and elsewhere, I basically ran up against "imaginary functions" and gave up 19:26:28 there was something about being able to do gcd on programs 19:26:32 been meaning to add I/O to Burro and to rewrite the docs, but 19:26:43 yeah that's a... what's it called 19:26:49 hmm, what kinda imaginary functions 19:26:55 Euclidean domain? 19:27:01 You can take the derivative of a lambda term 19:27:12 there's a new paper about it, it's silly but neat 19:27:30 http://esolangs.org/wiki/Imaginary_function 19:28:41 vanila: given the awesome power of taking a derivative of a CFG, I dunno, this could all be very wild 19:30:19 really can't even get near rings, I don't know how one would get up to integral domains and such 19:30:51 -!- naturalog has quit (Ping timeout: 244 seconds). 19:31:04 you tempt me 19:31:13 vanila: do you have a link to that paper? 19:31:42 -!- naturalog has joined. 19:31:51 http://www.informatik.uni-marburg.de/~pgiarrusso/papers/pldi14-ilc-author-final.pdf 19:32:00 cpressey: with imaginary functions: isn't it simple enough to just to add thunk(F) where F is a function to your primitive values 19:32:05 and have apply send thunk(F) to F 19:32:06 they get some good results speeding up code with it 19:32:10 not exciting, but it seems to meet your spec just fine 19:32:29 vanila: thanks 19:32:29 applied to pure lambda calculus, it has no effect 19:32:40 its' only when you make special primitives with differentiation support 19:32:44 just to spoil the ending 19:34:02 elliott: maybe. 19:34:44 i think that's occurred to me but i got too sick of it to follow up on it 19:35:13 as in data Expr = ... | Thunk Expr | Apply Expr | ...; data Value = ... | NativeFn (Value -> Value) | Closure Env Args Expr | ThunkV Value | ...; ... eval (Apply e) = apply (eval e); eval (Thunk e) = thunk (eval e); ...; apply (ThunkV v) = v; ... thunk v | isFun v = ThunkV v | otherwise = undefined or whatever 19:35:21 it's sorta like adding an axiom 19:35:25 basically you'd have a type constructor Thunk x and (apply Thunk x = x) but apply (a-real-function-value) would actually apply it 19:35:31 yes 19:36:02 istr thinking there was some little bumpy inconsistency. but if there isn't 19:36:04 then 19:36:49 yeah maybe you could invert things, or at least pretend to, to cover "for every X there is a -X" type axioms in algebraic structures 19:36:57 I should get back into esolangs. 19:37:05 I should probably not. 19:37:24 I mean, if you have, like 19:38:02 data Unit : Set where tt : Unit; apply : forall {A} -> (Unit -> A) -> A; apply f = f tt 19:38:05 in Agda say 19:38:08 then you can write 19:38:18 erm 19:38:23 yeah 19:38:31 hm, er 19:38:33 never mind me 19:38:50 probably best not to think about this kind of thing in a setting with types 19:40:38 I can't wrap my head around Agda. writing a function and writing a proof are seperate things in my head, and it wants me to moosh them together 19:41:13 I write my theorem as....... a type? Of a function? Then write the proof as the body of the function? 19:41:34 proof : Theorem 19:41:55 values are proofs and types are propositions 19:42:07 lambda is used to prove implication 19:42:59