00:05:04 but will you find the forbidden addressing mode 00:05:51 (i keep remembering stuff from x86 asm which would be insanely useful and then realising it could never work) 00:07:56 Of course. 00:08:22 there, 0x23 for the checkerboard 00:08:22 Oh, I looked it up and someone has a 4-instruction solution to Checkerboard. 00:08:31 That's much better than what I did. 00:08:37 it is interesting how opcodes/addressing modes mean that even assembly is quite high-level 00:13:01 I did some funny pipelining :) 00:13:19 and I should be able to shave off one more cycle... let's see 00:15:16 -!- nitrix has changed nick to horse. 00:15:36 -!- horse has changed nick to nitrix. 00:15:51 right :) 00:18:23 -!- lambda-11235 has quit (Read error: Connection reset by peer). 00:28:33 -!- XorSwap has quit (Ping timeout: 240 seconds). 00:30:33 myname: mynamello. I think I prefer ahoily. 00:33:55 -!- oerjan has quit (Quit: Nite). 00:34:15 -!- XorSwap has joined. 00:41:57 GACK! just took a look at the outside world. weather was restored from months-old backups... 00:42:53 I think the weirdest part about that game was the term "memory depth" in the manual for the addressing modes. 00:46:53 oh god, you can jump to odd addresses 00:47:14 I saw that in the manual as well. 00:47:29 But that's not odd from a real-hardware perspective. 00:48:39 Here's something interesing 00:48:43 *interesting 00:48:56 Mapping data structures to control flow concepts, and vice versa 00:49:07 Arrays are FOR loops 00:49:19 Lazy-evaluated sequences are WHILE loops 00:49:42 Tables are conditionals 00:49:49 Does this work? 00:50:56 (Oh, and nesting data structures is equal to nesting control flow) 00:54:26 rdococ: What do you think? 00:54:51 -!- lambda-11235 has joined. 00:55:03 hellambda-11235 00:55:43 lambda-11235: I'm figuring out a correspondence between data structures and control flow :) 00:57:51 hppavilion[1]: Hello. Have fun with that. I have to do English homework. :( 00:57:57 lambda-11235: :( 00:59:06 seriously, 4 instructions... wow. I have 6, 5 if I allows the code to loop through nops instead of jumping back to the top... 01:07:11 -!- Guest772715 has joined. 01:07:54 -!- Guest772714 has quit (Read error: Connection reset by peer). 01:12:02 Oh, I missed all the BOX-256 chat :-( 01:12:17 impomatic, back my thread register scheme imho 01:12:46 otherwise the guy might implement that shitty LODPC instruction 01:13:16 What's LODPC? 01:13:54 My smallest checkerboard is 6. I've been mostly optimizing for speed though. 01:15:16 I have the new Smiley Face record now :-) 01:17:17 impomatic, https://www.reddit.com/r/box256/comments/4dfqlm/4_squares_4_threads_0x2e_cycles_using_a_beam/d1r7bi5?context=3 01:18:26 is anybody collecting records without solutions? 01:18:28 lets you get thread-specific behaviour at the cost of being an incredibly stupid way of doing so 01:20:47 int-e: I checked the reddit and hacker news threads for any records where the solution wasn't posted (for cycles only, no-one apart from me seemed interested in size) 01:22:51 int-e: int-ello. I can't stop binging QC. 01:23:16 Records are blue square 0x7, checkerboard 0x16, four squares 0x7, smiley face 0x2E 01:23:33 hi impomatic 01:23:36 I saw some of your posts. 01:23:48 impomatic: thanks 01:24:11 shachaf: I use the same nick everywhere :-) 01:24:13 Are those cycle records or line records? 01:24:14 so my 0x22 checkerboard isn't too bad then 01:24:34 shachaf: cycle records 01:25:07 is anybody trying for single-threaded cycles? 01:25:13 I was wondering about that. 01:25:20 Threads are TG. 01:25:32 int-e: that's pretty good. Only a couple of people have claimed less than 0x22. 01:26:11 (singlethreaded I have 0x5E for the blue square, 0x1FC for checkerboard; multi-threaded it's 0x11 and 0x22 for now) 01:26:22 int-e: I wondered about collating single-thread cycle results, but everyone would just unroll the loops and fill all 63 available instructions. 01:26:24 I should sleep... 01:26:50 you can use 64... 01:27:13 What am I looking at, here? 01:27:15 Only 64 if the last instruction doesn't use the 4th byte. 01:27:20 (if the last one is short) 01:27:53 "You must use a browser with WebGL. Consider downloading Firefox" > Running Firefox :| 01:28:58 There's a Windows version of BOX256 01:29:02 Is one of my about:configs wrong? 01:32:05 Works in 0/3 of my browsers. :( 01:32:58 what's your graphics hardware like? 01:33:18 if it's intelgrated that's probably why, especially if you're on linux 01:33:31 Radeon R9 01:34:09 `version prooftechnique 01:34:09 Oh, now it's doing something 01:34:15 fuck 01:34:19 /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: version: not found 01:34:31 Hanging Firefox, mainly, but maybe that'll figure itself out 01:34:37 why do these shitty clients not have helpful /VERSIONs like xchat 01:35:05 lol i forgot about what i set mine to 01:36:03 Mine may be set weird because I'm connecting through ZNC 01:36:33 Or weechat sets something dumb :v 01:38:24 -prooftechnique- VERSION WeeChat 1.4 (Mar 10 2016) via ZNC 1.6.2 - http://znc.in 01:38:41 -!- Phantom__Hoover has joined. 01:38:46 Oh, neat 01:40:04 huh i can't get rid of the actual legitimate /VERSION 01:40:08 -!- Phantom__Hoover has quit (Client Quit). 01:42:04 -!- Guest772715 has quit (Ping timeout: 260 seconds). 01:42:32 Hi #esoteric 01:42:46 catello! 01:42:59 Are there any esoteric languages that don't parse to a tree, but rather parse to a DAG or a cyclic graph? 01:43:27 You can think of any lambda calculus expression as parsing to a directed graph. 01:43:46 Do you mean that it's observable from within the language? 01:45:37 Oh, well, I'm just asking because during an intro talk on compilers (that I am currently sitting in), the presenter said "Languages usually parse to a tree" 01:46:06 I was wondering if there was any way one could justify making that "usually" qualification 01:46:14 (instead of "always") 01:46:54 And I thought #esoteric might be helpful 01:47:35 Maybe this? https://en.wikipedia.org/wiki/Abstract_semantic_graph 01:47:45 shachaf, what, because you merge identical subexpressions? 01:47:50 Looks like a compiler could use it for CSE and whatnot 01:48:03 I don't think Befunge parses into a tree typically. 01:48:12 Phantom_Hoover: I mean that every use of a variable has an edge pointing to the lambda introducing it. 01:48:12 befunge doesn't parse 01:48:21 At least, I don't see any sane way of representing a Befunge program as a tree in any meaningful sense. :) 01:48:41 shachaf, 'use' in that context sounds like it's still a directed tree 01:49:07 there's not even such a thing as a syntactically illegal befunge program, is there? 01:49:29 Well, there is in Befunge 93 at least. 01:49:34 :P 01:50:26 -!- Guest772715 has joined. 01:51:00 catern: Andres Löh actually has a paper on using ASGs for DSLs, which might be of interest 01:51:09 pikhq, how? 01:51:21 as specified i think befunge programs are just a grid of 'commands' 01:51:22 Phantom_Hoover: Being larger than 80x25 01:51:33 :/ 01:52:23 Bit of a cop-out, heh 01:59:12 -!- Phantom_Hoover has quit (Remote host closed the connection). 02:01:57 Arguably, also files containing form feeds in {Une,Be}funge-98, and files containing newlines in Unefunge-98. (Although strictly speaking the spec does explicitly allow multi-line Unefunge-98 programs, the lines are just concatenated. And it doesn't specify what form feed does outside of Trefunge-98, so you could say by omission it's just a regular character. But still.) 02:02:36 Oh, and the Funge-98 spec says that Befunge-93 only allows "printable ASCII characters and the end-of-line controls". 02:11:29 catern: I proposed that a while ago 02:12:35 fizzie: A fungeoid... based on Numerical Computing 02:12:51 fizzie: So you can calculate the product of two programs 02:13:16 (For individual instructions, + is parallel composition, * is sequential composition) 02:13:55 -!- lleu has quit (Quit: That's what she said). 02:34:38 Pigeonhole principal time! 02:35:45 If you have a multigroup (S, [a], [b], [c]), then there are infinitely many possible equations. 02:36:35 *for any number of variables n 02:36:52 However, there are only (#S)^(n+2) possible n-ary functions 02:37:34 I conclude that there is more than one way to write some equations 02:37:48 And I conjecture that there are infinitely many ways to write any given equation 02:37:57 Therefor, I conclude, Algebra is a silly field 02:38:15 You take that filth back, you monster 02:38:29 -!- Guest772714 has joined. 02:38:38 -!- Guest772715 has quit (Read error: No route to host). 02:38:39 prooftechnique: Too late, already published. 02:38:59 I counter with "Up To Isomorphism" 02:39:14 prooftechnique: Correct. 02:39:15 (aka, the algebraist's trump) 02:39:17 prooftechnique: Still funny. 02:39:21 s/funny/silly/ 02:39:53 hppavilion[1]: principle, not principal :P 02:40:06 boily: FUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUUU 02:40:11 F7U12 02:40:19 DOES NOT PASS PEER REVIEW. GRANT DENIED 02:40:33 Algebra lives to fight another day 02:41:01 prooftechnique: Didn't need a grant. 02:41:13 prooftechnique: Do you understand tensors? 02:41:49 Not in a way that I could talk at length about them without some reference material to back me up 02:42:30 prooftechnique: Do you understand them enough to transfer some understanding to someone who doesn't 02:42:30 ? 02:42:45 Depends what you need to understand, I suppose. I could try 02:43:17 prooftechnique: I don't understand them /at all/ 02:43:22 I understand what a vector space is 02:43:36 But I don't get tensors 02:44:10 prooftechnique: What I want to do is make a tensor programming language 02:44:21 Oh, jeez. 02:44:23 Not a language which uses tensors like an array programming language uses arrays 02:44:38 And what does that look like, in your mind? 02:44:43 prooftechnique: I have no idea 02:44:50 prooftechnique: I want to make a language for which the /programs/ are... tensory? 02:46:33 prooftechnique: I don't necessarily want to do it right now 02:46:45 What property of tensors would you want to apply to a program? 02:46:57 Do you want the tensor product of programs? 02:47:26 prooftechnique: Yes, basically 02:47:46 prooftechnique: I want to be have a language for which the programs form a tensor (wiki uses that phrase, so I think it works) 02:48:09 -!- boily has quit (Quit: MOVIE CHICKEN). 02:48:23 Unfortunately, I think I need to go 02:48:29 Well, I'd start by figuring out what that means. Maybe figure out what the Cartesian product of programs in a set language is, or what the space of linear transformations from programs to programs looks like 02:49:06 Assuming that programs are themselves vector spaces, that is 02:56:24 -!- earendel has quit (Quit: earendel). 03:02:27 Oh finally, I see, the two square problems are badly designed... there's enough space to just draw all pixels explicitly. 03:30:54 -!- Kaynato has joined. 03:51:14 prooftechnique: Well, the cartprod of two programs {a, b, c} and {1, 2, 3} is {(a, 1), (a, 2), (a, 3), (b, 1), (b, 2), (b, 3), (c, 1), (c, 2), (c, 3)} 03:51:32 The set is parallel-composed and the tuples are sequential-composesd 03:51:34 *composed 03:52:33 -!- earendel has joined. 03:53:23 The programs {a, b, c} and {1, 2, 3} represent set programs, in which instructions are non-blocking 03:57:34 prooftechnique: Programs-as-vector-spaces sounds interesting, but I was thinking programs-as-vectors. But programs-as-vector-spaces sounds more interesting 04:07:50 -!- iconmaster has quit (Ping timeout: 244 seconds). 04:10:13 -!- Guest772714 has quit (Quit: Nettalk6 - www.ntalk.de). 04:15:32 -!- Reece` has quit (Quit: Leaving). 04:19:06 -!- Reece` has joined. 04:37:57 -!- Reece` has quit (Quit: Leaving). 04:38:58 -!- Reece` has joined. 04:39:07 -!- Reece` has quit (Read error: Connection reset by peer). 04:40:07 -!- Reece` has joined. 04:49:43 -!- Reece` has quit (Quit: Leaving). 04:50:48 -!- Reece` has joined. 04:53:16 -!- hppavilion[1] has quit (Ping timeout: 252 seconds). 05:05:33 -!- XorSwap has quit (Quit: Leaving). 05:09:09 -!- lambda-11235 has quit (Read error: Connection reset by peer). 05:10:23 -!- lambda-11235 has joined. 05:13:53 -!- Reece` has quit (Quit: Alsithyafturttararfunar). 05:14:58 -!- Reece` has joined. 05:18:12 -!- Reece` has quit (Client Quit). 05:19:13 -!- Reece` has joined. 05:25:00 -!- Reece` has quit (Quit: Alsithyafturttararfunar). 05:26:49 -!- Reece` has joined. 05:27:24 -!- Reece` has quit (Client Quit). 05:32:20 -!- Reece` has joined. 05:40:06 -!- Reece` has quit (Quit: Alsithyafturttararfunar). 06:30:24 -!- Kaynato has quit (Ping timeout: 244 seconds). 06:39:58 -!- hppavilion[1] has joined. 06:41:04 "Strict superset of perl" 06:42:06 -!- lambda-11235 has quit (Quit: Bye). 06:52:37 I want to make a C++ that doesn't suck 06:52:39 For personal use 06:53:12 w 06:54:46 why not just make ont hat sucks a little bit? 07:06:45 newsham: That's probably how it'll come out 07:06:50 Currently, I need a new C++ compiler 07:07:17 -!- jaboja has joined. 07:07:31 hppavilion[1]: why? 07:07:37 what's wrong with the old one? 07:08:00 coppro: Well, it's not suitable for operator-heavy development 07:08:12 why not? 07:08:13 coppro: I would like to be able to define new & arbitrarily-named operators at will 07:08:36 coppro: So I could have different operators for element-wise multiplication and traditional matrix multiplication 07:08:42 * and @ most likely 07:08:46 s/new C++ compiler/new C++ language/ 07:09:06 coppro: No, I also need a new C++ compiler 07:09:11 coppro: My current one seems to be corrupted 07:09:25 w 07:09:31 It prints out endless garbage when I try to compile a simple file 07:10:57 coppro: I'm thinking of calling the new language C⁂ 07:11:15 `unidecode ⁂ 07:11:22 coppro: Asterism 07:11:39 [U+2042 ASTERISM] 07:13:16 hppavilion[1]: then adopt a character ⁂. http://unicode.org/consortium/adopt-a-character.html 07:18:30 -!- pelegreno has quit (Read error: Connection reset by peer). 07:19:55 There, got it working 07:20:17 Oh... found the issue 07:20:39 I had accidentally targetted the compilation of main.cpp to one of its dependencies... xD 07:22:48 -!- pelegreno has joined. 07:25:37 -!- hppavilion[1] has quit (Ping timeout: 252 seconds). 07:41:50 [wiki] [[Kantate]] N https://esolangs.org/w/index.php?oldid=46758 * Keymaker * (+5598) Added my new low-level language based on a simple addition mechanism. 07:50:48 -!- AnotherTest has joined. 07:52:02 [wiki] [[User:Keymaker]] https://esolangs.org/w/index.php?diff=46759&oldid=40487 * Keymaker * (+14) Added Kantate, some changes. 07:58:01 -!- tromp_ has joined. 08:02:24 -!- tromp_ has quit (Ping timeout: 246 seconds). 08:17:52 -!- J_Arcane has quit (Ping timeout: 244 seconds). 08:25:14 -!- acertain has quit (Read error: Connection reset by peer). 08:25:46 -!- acertain has joined. 08:30:56 -!- Sprocklem has quit (Quit: [). 08:37:35 -!- ais523 has joined. 08:45:30 -!- hipsterslapfight has left. 08:46:39 -!- mroman has joined. 08:46:51 I was always getting shit for my irrational fear of dogs. 08:47:03 Now people are scared of people not wearing bikinis. 08:47:55 I'm pretty certain that getting attacked by a dog severly enough to see a doctor is far more likely than whatever a woman not wearing a bikini is likely to do to me. 08:48:09 @messages-lood 08:48:09 boily asked 3d 8h 26m 55s ago: hello? hello? hello? 08:48:22 @tell boily HELLO FROM THE OTHER SIDE.... 08:48:22 Consider it noted. 08:48:27 IT MUST HAVE BEEN A THOUSAND TIMES 08:48:50 that last one might be off an inch. 08:50:14 (currently switzerland's top topic is if it's ok for muslims to not shake hands) 08:51:06 (I'm guessing secretly everybody is happy if they don't have to shake a muslims hand but get enraged when a muslim chooses to not shake hands..) 08:51:55 is it "other side" or "outside"? 08:53:00 -!- jaboja has quit (Ping timeout: 268 seconds). 09:02:41 -!- Sprocklem has joined. 09:06:47 -!- Sprocklem has quit (Client Quit). 09:07:08 -!- Sprocklem has joined. 09:22:40 -!- jaboja has joined. 09:24:33 -!- Frooxius has quit (Ping timeout: 244 seconds). 09:52:27 -!- sebbu has quit (Ping timeout: 244 seconds). 09:58:39 -!- sebbu has joined. 10:05:52 -!- zadock has joined. 10:17:07 -!- zadock has quit (Quit: Leaving). 10:51:59 -!- earendel has quit (Quit: earendel). 11:08:31 -!- Frooxius has joined. 11:26:01 -!- lleu has joined. 11:26:01 -!- lleu has quit (Changing host). 11:26:01 -!- lleu has joined. 11:28:46 -!- boily has joined. 11:36:14 -!- Phantom_Hoover has joined. 11:49:54 -!- Phantom_Hoover has quit (Remote host closed the connection). 11:51:33 -!- Phantom_Hoover has joined. 12:01:19 -!- boily has quit (Quit: RESOLVED CHICKEN). 12:32:05 -!- J_Arcane has joined. 12:50:10 -!- tromp_ has joined. 13:00:55 -!- tromp_ has quit (Remote host closed the connection). 13:02:34 -!- jaboja has quit (Ping timeout: 244 seconds). 13:13:03 -!- Reece` has joined. 13:19:08 -!- jaboja has joined. 13:23:59 -!- oerjan has joined. 13:26:14 -!- jaboja has quit (Ping timeout: 250 seconds). 13:42:50 does anyone else know of any accidentally TC tabletop games besides MtG? 13:47:32 * oerjan pings ais523 on that. 13:49:15 i know NP-complete and PSPACE-complete games, but TC requires a complexity beyond normal games, i think. 13:49:25 because unbounded state. 13:50:32 well, you need to generalize the size for the former, usually. so maybe they don't count in this sense either. 13:51:58 tabletop, not sure 13:52:09 you can do things like infinite generalizations of Sokoban and Minesweeper 13:52:34 finding a game that naturally has infinite storage is hard, though 13:52:55 and the ones that do, like Monopoly, don't have any obvious way to use it or do computations based on it 13:53:13 hmm, what about Monopoly where the program is a repeating sequence of dice rolls? 13:58:43 ais523: IMO what makes it hard to find TC-ness is that in the typical PSPACE-completeness proof of a game like sokoban or mario, you built the memory cells in the polynomial time preprocessing, and they're represented in-game as something like immutable in-game rooms. For TC you have to find a way to dig an unbounded sequence of rooms in-game, which is more difficult than just setting up a fixed number of rooms. 13:58:58 \ you built the memory cells in the polynomial time preprocessing, and they're represented in-game as something like immutable in-game rooms. For TC you have to find a way to dig an unbounded sequence of rooms in-game, which is more difficult than just setting up a fixed number of rooms. 14:01:24 -!- tromp_ has joined. 14:05:49 -!- tromp_ has quit (Ping timeout: 260 seconds). 14:07:01 b_jonas: nothing was cut off hth 14:17:38 -!- jaboja has joined. 14:24:59 -!- spiette has joined. 14:32:13 Apparently in 2005 my uni's CS department held a Vim vs Emacs paintball tournemant 14:32:19 Paintball is probably not turing complete 14:33:06 `quote ais.*vim 14:33:44 1271) editor flame wars are fun, I typically take the side of emacs and vim versus everything else normally I can get most of the emacs /and/ vim users round to my side, thus catching out all the other-editor-users who thought they were safe 14:39:14 -!- Guest95899 has joined. 14:45:33 -!- Sgeo has quit (Ping timeout: 240 seconds). 14:53:04 Good plan 15:06:59 -!- Kaynato has joined. 15:21:49 -!- lambda-11235 has joined. 15:32:35 -!- jaboja has quit (Ping timeout: 248 seconds). 15:39:27 @tell mroman is it "other side" or "outside"? <-- that depends on whether or not you're a ghost hth 15:39:27 Consider it noted. 15:52:51 -!- Gwir has joined. 15:56:21 -!- lambda-11235 has quit (Quit: Bye). 16:01:21 -!- Gwir has left ("Leaving"). 16:01:37 -!- tromp_ has joined. 16:05:58 -!- tromp_ has quit (Ping timeout: 244 seconds). 16:07:16 -!- mroman has quit (Quit: Lost terminal). 16:11:03 -!- J_Arcane has quit (Ping timeout: 240 seconds). 16:11:33 -!- Kaynato has quit (Ping timeout: 240 seconds). 16:14:03 -!- J_Arcane has joined. 16:19:15 -!- Kaynato has joined. 16:49:13 -!- XorSwap has joined. 16:50:15 -!- XorSwap has quit (Client Quit). 16:58:08 -!- ais523 has quit (Ping timeout: 250 seconds). 16:58:55 -!- jaboja has joined. 17:04:45 -!- jaboja has quit (Ping timeout: 248 seconds). 17:08:44 -!- oerjan has quit (Quit: Later). 17:16:30 -!- Guest772714 has joined. 17:22:55 -!- J_Arcane has quit (Ping timeout: 252 seconds). 17:27:19 -!- Guest95899 has quit (Ping timeout: 252 seconds). 17:27:45 -!- Guest95899 has joined. 17:30:49 -!- Guest772714 has quit (Quit: Nettalk6 - www.ntalk.de). 17:35:58 -!- Guest772714 has joined. 17:47:15 -!- Guest95899 has quit (Ping timeout: 264 seconds). 18:01:13 -!- Kaynato has quit (Ping timeout: 268 seconds). 18:02:11 -!- ais523 has joined. 18:03:15 -!- Kaynato has joined. 18:06:04 -!- Caesura has joined. 18:07:05 -!- Zoroaster has joined. 18:09:51 -!- Kaynato has quit (Ping timeout: 268 seconds). 18:11:05 -!- Caesura has quit (Ping timeout: 268 seconds). 18:26:15 -!- Frooxius has quit (Ping timeout: 264 seconds). 18:31:54 -!- jaboja has joined. 18:42:29 -!- iconmaster has joined. 18:42:33 -!- Frooxius has joined. 19:09:40 -!- Zoroaster has quit (Ping timeout: 268 seconds). 19:20:04 -!- Guest772714 has quit (Ping timeout: 252 seconds). 19:30:45 -!- hppavilion[1] has joined. 19:32:53 -!- Reece` has quit (Quit: Alsithyafturttararfunar). 19:32:56 -!- hppavilion[2] has joined. 19:33:16 -!- Reece` has joined. 19:34:11 -!- jaboja has quit (Ping timeout: 248 seconds). 19:35:28 -!- hppavilion[1] has quit (Ping timeout: 252 seconds). 19:36:38 -!- lambda-11235 has joined. 19:45:31 -!- Kaynato has joined. 19:54:11 -!- lambdabot has quit (Quit: brb). 19:55:11 I'm creating a web application called Wi 19:55:13 (Web Vi) 19:55:50 The goal is to use it as an interactive Vi in-browser 19:58:58 -!- lambdabot has joined. 20:01:48 -!- Guest772714 has joined. 20:11:46 -!- hppavilion[2] has quit (Ping timeout: 252 seconds). 20:35:08 -!- p34k has joined. 20:36:02 -!- ais523 has quit (Read error: Connection reset by peer). 20:37:15 -!- ais523 has joined. 20:51:03 -!- hppavilion[2] has joined. 20:53:43 -!- rzfjwyxq has joined. 20:54:00 -!- rzfjwyxq has quit (Client Quit). 20:57:52 -!- lambda-11235 has quit (Quit: Bye). 21:04:54 I think I've discovered a correspondence between data structures and control flow 21:06:39 Of course, like the CHI, not all things on either side have a common partner 21:06:46 So I'm looking into call/cc 21:11:21 Maybe this channel would be more appropriate for my question. 21:11:50 If all function application is left-associated, what set of primitives would you need to be able to write any function? 21:12:09 Something like unlambda without ` 21:12:15 shachaf: S, K, ` 21:12:16 Oh 21:12:21 So "f $ g $ h" = "(f $ g) $ h"? 21:12:45 Well, f g h 21:12:51 S, K, C maybe? 21:13:10 S and K are the traditional ones, Cxyz = xzy 21:13:27 I don't think that's sufficient. 21:13:28 Or maybe C^-, which is C^-xy=yx 21:13:34 shachaf: Let me fire up COq 21:18:20 shachaf: stack operation primitives, I think 21:18:34 shachaf: no wait, you said left-associated, not right-associated 21:18:46 um 21:19:05 in that case you need to start form a primitive that's not well-typed in HM, right? 21:19:26 wait, which way is left-associated and which way is right-associated? 21:19:44 and from which side are you applying functions? 21:20:11 shachaf: If I know how Coq works, then- wait, no 21:20:39 b_jonas: Same as Haskell. 21:20:51 a b c d = (((a b) c) d) 21:21:58 shachaf: I stand by my c hypothesis 21:22:40 shachaf: Wait, does left associative imply that types can only by (((Q -> P) -> S) -> T) -> U and such? 21:22:52 If so, that makes things a LOT more difficult 21:22:52 OK, then show how to translate an arbitrary lambda expression. 21:22:53 shachaf: in that case, you need a non-well-typed function 21:23:03 b_jonas: Why? 21:23:19 shachaf: you can't apply arbitrarily many arguments to a well-typed function, right? 21:23:29 Sure you can. 21:23:32 > id id id id id 5 21:23:34 5 21:23:47 hmm 21:25:49 hola 21:25:56 todos 21:26:06 le mundi 21:26:13 el even 21:27:05 fungot: can you factor eleven? 21:27:06 int-e: commissioner, the council of ministers, several former prime ministers, this institution is, after all, this was also true of the police and judiciary, long regarded as the most comprehensive legal statement of children' s safety may be a case of double hulls. with regard to amendments nos 67 and 68 would complicate the system rather than trying to do this both in conjunction with countries that have applied to join the 21:27:56 how is stacl based not left assoziative? 21:27:58 -!- bb010g has joined. 21:29:02 myname: in what context does that question make sense? 21:29:21 ^style 21:29:21 Available: agora alice c64 ct darwin discworld enron europarl* ff7 fisher fungot homestuck ic irc iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp youtube 21:29:47 i am refering zu b_jonas idea of stack operations 21:30:33 to even 21:30:41 how did this happen 21:31:31 -!- hppavilion[2] has quit (Ping timeout: 252 seconds). 21:33:54 Double hulls, *that's* how we'll keep the children safe. 21:35:07 fungot: Do you have other parenting tips? 21:35:08 fizzie: from a logical point of view on the subject of this own-initiative report commits various cardinal sins. the first deadline to be set at a higher level of investment and, thus, cannot accept amendments nos 30, 38 and amendments nos 5 and 6. as for the inspections, very much for your invitation, mrs kinnock, for pointing this out because i was looking to a new trend in the member states and applicant countries, whereas p 21:37:09 -!- J_Arcane has joined. 21:38:40 -!- Guest772714 has quit (Ping timeout: 252 seconds). 21:39:32 oh you mean something like this 21:39:35 > let push x a c = c (a:x); add (a:b:x) c = c (a+b:x); end x = x; start c = c [] in start push 1 push 2 add push 3 add end 21:39:37 [6] 21:41:11 end (x:_) = x would be nicer 21:42:11 if you only want to calculate scalars, that is 21:42:46 oh, Oleg attributes this to Okasaki, interesting. http://okmij.org/ftp/Haskell/polyvariadic.html 21:43:10 myname: But you don't know at compile-time what will be in the stack. 21:43:18 Of course you could type-check it if you wanted to. 21:43:23 > let { push x a c = c (a,x); add (a,(b,x)) c = c (a+b,x); end (x,()) = x; start c = c () } in start push 1 push 2 add push 3 add end 21:43:24 6 21:43:33 > let { push x a c = c (a,x); add (a,(b,x)) c = c (a+b,x); end (x,()) = x; start c = c () } in start push 1 push 2 add push 3 add add end 21:43:34 Couldn't match type ‘(t, ())’ with ‘()’ 21:43:34 Expected type: (t, ()) -> ((t, ()) -> t) -> t 21:43:35 Actual type: (t, (t, ())) -> ((t, ()) -> t) -> t 21:45:06 such a readable type error :) 21:45:14 hello 21:45:23 @let data HList :: [*] -> * where { HNil :: HList '[]; (:!) :: x -> HList xs -> HList (x ': xs) } 21:45:24 Defined. 21:45:30 talk to me 21:45:43 fungot: do we want to talk to quintopia? 21:45:44 int-e: commissioner diamantopoulou, mr katiforis presents a report on one very important element of which is the year of marine safety, which will require the mobilisation of european engineers and support teams could, in fact, the dogma of the uncontrolled interpretative powers granted to the commission proposal for extending magp iv and it is there that we have balanced all the points we fought to improve. 21:45:56 politicians just can't say no. 21:46:04 * int-e runs 21:46:28 i'm just a gal who caint say no 21:48:00 shachaf: why do i need to know? 21:48:26 You don't need anything. 21:48:57 just throw the error, it's fine 21:49:05 end = head 21:49:36 gotta type-check everything 21:49:47 Also I thought I'd use HList and maybe get a better error message. 21:50:08 But the joke's on me because it's not even working and I don't know why. 21:50:57 does it work in ghci? 21:50:59 Just another day in HListland. 21:51:03 I don't know, I don't have ghci. 21:51:10 Well, the other day I wrote HListy code in C++. That was worse. 21:51:16 how can you not have ghci! 21:51:20 blasphermy 21:51:22 blasphemy 21:51:31 > let { push x a c = c (a :! x); add (a :! (b :! x)) c = c ((a+b) :! x); end (x :! HNil) = x; start c = c HNil } in start push 1 push 2 add push 3 add end 21:51:33 Couldn't match expected type ‘HList (x : xs1) -> t2’ 21:51:33 with actual type ‘t1’ 21:51:33 because type variable ‘xs1’ would escape its scope 21:53:14 -!- Kaynato has quit (Ping timeout: 250 seconds). 21:53:30 :t let { push x a c = c (a :! x); add (a :! (b :! x)) c = c ((a+b) :! x); end (x :! HNil) = x; start c = c HNil } in start push 21:53:31 Couldn't match expected type ‘HList (x1 : xs1) -> t2’ 21:53:31 with actual type ‘t1’ 21:53:31 because type variable ‘xs1’ would escape its scope 21:53:51 I guess not being able to type this prefix could be a problem 21:54:28 > let { push x a c = c (a :! x); add (a :! (b :! x)) c = c ((a+b) :! x); end (x :! HNil) = x; start c = c HNil } in () -- The issue is in the definitions. 21:54:30 Couldn't match expected type ‘HList (x : xs1) -> t1’ 21:54:32 with actual type ‘t’ 21:54:34 because type variable ‘xs1’ would escape its scope 21:55:22 ah. 21:58:10 -!- Kaynato has joined. 21:58:10 > let { push x a c = c (a :! x); add :: HList (Int ': Int ': xs) -> (HList (Int ': xs) -> r) -> r; add (a :! (b :! x)) c = c ((a+b::Int) :! x); end :: HList '[x] -> x; end (x :! HNil) = x; start c = c HNil } in start push 1 push 2 add push 3 add end 21:58:12 6 21:58:14 scow 21:58:18 It was just an inference issue? 21:58:52 > let { push x a c = c (a :! x); add :: Num x => HList (x ': x ': xs) -> (HList (x ': xs) -> r) -> r; add (a :! (b :! x)) c = c ((a+b) :! x); end :: HList '[x] -> x; end (x :! HNil) = x; start c = c HNil } in start push 1 push 2 add push 3 add end 21:58:54 6 21:59:08 will it work in ghc 8? 21:59:11 Why does that have an inference issue? 22:01:11 :t let { end (x :! HNil) = x } in end 22:01:13 Couldn't match expected type ‘t2’ with actual type ‘x’ 22:01:13 ‘t2’ is untouchable 22:01:13 inside the constraints (xs ~ '[]) 22:05:31 :t let end xs = case xs of { x :! HNil -> () } in 42 22:05:33 Not in scope: data constructor ‘:!’ 22:05:33 Perhaps you meant one of these: 22:05:33 ‘:+’ (imported from Data.Complex), 22:05:58 :t let end xs = case xs of { x :! HNil -> () } in 42 22:05:59 Couldn't match expected type ‘t’ with actual type ‘()’ 22:05:59 ‘t’ is untouchable 22:05:59 inside the constraints (xs ~ '[]) 22:06:53 so it has learned nothing about the return type... and then there comes the GADT pattern match that freezes the type variables outside? dunnno. the ways of the type checker are mysterious and convoluted. 22:10:36 what does :! do? 22:10:43 and what does ': do? 22:10:56 :! doesn't look like an operator, ': might be one though 22:11:00 :t (':) 22:11:02 parse error on input ‘:’ 22:11:04 The :! is part of the HList definition. ': is a type-level cons operator. 22:11:21 well, type-literal level 22:11:33 -!- Guest772714 has joined. 22:12:35 is ' reserved for type-level operators? 22:12:37 :t '[()] 22:12:38 parse error on input ‘(’ 22:12:46 :t '['()] 22:12:47 parse error on input ‘]’ 22:13:00 (okay, that was stupid) 22:13:11 it got all the way up to the ] before getting confused 22:13:24 I take it '[' was parsed as a character 22:13:26 then () as unit 22:13:26 > '['() -- is just a type error 22:13:27 Couldn't match expected type ‘() -> t’ with actual type ‘Char’ 22:13:27 The function ‘'['’ is applied to one argument, 22:13:27 but its type ‘Char’ has none 22:13:37 ais523: I think you need to write it as '[]() 22:13:39 and only failed to parse after that 22:13:51 b_jonas: I think ais523 didn't make the mistake 22:13:58 oh 22:13:59 um 22:13:59 b_jonas: but anyway :t parses expressions 22:14:13 :k () 22:14:14 * 22:14:19 :k ': 22:14:20 parse error on input ‘:’ 22:14:24 :k (':) 22:14:25 parse error on input ‘:’ 22:14:29 :k '[] 22:14:30 [k] 22:14:33 aha 22:14:39 -!- spiette has quit (Ping timeout: 260 seconds). 22:14:47 :k '[()] 22:14:48 [*] 22:14:55 what does k mean in a kind? 22:15:08 it's a polymorphic kind 22:15:12 so a kind variable 22:15:26 ah right 22:15:31 I didn't realise we had kind-level polymorphism 22:15:50 ghc has grown some fancy type system extensions in the last three (I think) years 22:16:00 * ais523 wonders if it's possible to identify types with kinds without becoming dependently typed 22:20:59 ais523: That's sort of what GHC does. 22:21:08 Depending on what you mean by "identify". 22:21:14 I'm not sure what I mean 22:22:15 When you define a type Maybe a with values Nothing and Just a, GHC also defines a kind Maybe a with types Nothing and Just a 22:22:30 With DataKinds. 22:22:35 Are those identified? 22:22:44 is it possible to construct a value of type Nothing? 22:22:59 No. By "type" I just mean that it exists on the type level. 22:23:16 ais523: well, even in a dependently-typed language you can't create a object of type Nothing 22:23:24