00:00:39 cpressey: of course, it will be rather rubbish for actually *writing* programs 00:00:41 but who does that? 00:01:56 * Sgeo needs to organize his bookmarks at some point 00:02:41 -!- MigoMipo has quit (Quit: When two people dream the same dream, it ceases to be an illusion. KVIrc 3.4.2 Shiny http://www.kvirc.net). 00:04:42 -!- GreaseMonkey has joined. 00:05:39 Hm 00:06:03 I did a "Clear Browsing Data" thing in Chrome, but I changed my mind, and can't seem to stop it 00:06:33 AND or OR 00:06:37 which should be defined first? 00:06:41 i.e. which is more fundamental? 00:06:44 NAND 00:07:19 pkill chrome 00:07:19 duh 00:07:25 uh, i'd go with (a & b) | (c & d) if you're thinking of ordering or something like that 00:07:27 And or or = or 00:07:40 GRUNT 00:07:46 Night folks. 00:07:49 -!- cpressey has left (?). 00:07:52 night.. 00:07:53 GreaseMonkey: I mean as in fundamental definitionerition 00:07:56 oerjan: yes yes 00:08:20 i'm thinking maybe "or" 00:08:21 alise: you are aware that they are entirely dual in boolean logic? 00:08:31 which happens to be the inverse of nand 00:09:05 in boolean logic -1*-1 = -1 00:09:21 boolean logic is a LIE taught by EVIL academics 00:09:23 oerjan: of course 00:09:29 *Main> pretty conjunction 00:09:29 (⊤ ∧ α) → α 00:09:29 (⊥ ∧ α) → ⊥ 00:09:33 (where alpha is bold) 00:09:48 MissPiggy: i'm thinking that it'd actually be ...0101010101010101 recurring 00:09:50 i'ma writa terma rewritinga systema, mamaa 00:09:55 i could be wrong, though 00:10:00 conjunction :: System 00:10:00 conjunction = 00:10:00 Set.fromList 00:10:00 [ Rewrite (Structure [Atom "⊤", Atom "∧", Free "α"]) $ Free "α" 00:10:00 , Rewrite (Structure [Atom "⊥", Atom "∧", Free "α"]) $ Atom "⊥" ] 00:10:16 wait, no, -1*-1 = 1 00:10:17 -!- jix has quit (Ping timeout: 246 seconds). 00:10:23 erm 00:10:25 wrong symbol 00:10:25 >>> hex(0xff*0xff) 00:10:25 '0xfe01' 00:10:27 should be V :) 00:10:36 -!- Leonidas has quit (Ping timeout: 252 seconds). 00:10:46 no 00:10:50 no, not wrong symbol 00:10:50 :P 00:11:03 ^ being and, IIRC 00:11:35 i _do_ have this feeling and is more immediately useful though, since it allows you to collect hypotheses 00:11:43 hmm, actually, I only need Free in the left-hand side 00:11:48 on the right, it's just like any other rewriting rule 00:11:51 rewriting to the value 00:12:20 (a -> (b -> c)) <=> ((a & b) -> c) 00:12:40 argh, but the structures are almost identical 00:12:44 to make them separate types is pure madness, aye 00:12:51 -!- jix has joined. 00:13:54 *Main> pretty (Set.union conjunction disjunction) 00:13:54 (⊤ ∧ α) → α 00:13:54 (⊤ ∨ α) → ⊤ 00:13:54 (⊥ ∧ α) → ⊥ 00:13:54 (⊥ ∨ α) → α 00:14:01 (where alpha is bold on the left-hand side) 00:14:09 interesting ordering there bob 00:14:49 Ack, it's Agda! Except actually probably not. 00:14:57 It's not, it's just a tree rewriting system. 00:15:08 conjunction :: System 00:15:08 conjunction = 00:15:08 Set.fromList 00:15:08 [ Rewrite (Structure [Atom "⊤", Atom "∧", Free "α"]) $ Atom "α" 00:15:08 , Rewrite (Structure [Atom "⊥", Atom "∧", Free "α"]) $ Atom "⊥" ] 00:15:21 What ever happened to rewriting arbitrary graphs? 00:15:23 alise: so was trying that pokemon game. Got one question: how do you catch instead of fight? 00:15:31 uorygl: You can do graphs with trees! 00:15:37 AnMaster: ... 00:15:41 AnMaster: Go to the bag, choose a Pokeball >_< 00:15:46 You mean you never played Pokemon before? 00:15:46 oh I see 00:15:47 There was a bloody realtime tutorial 00:15:50 pikhq, correct 00:15:53 Didn't you watch it? :P 00:15:58 alise, what? in which one? 00:16:07 Um, someone goes hay i catch pokemon or something 00:16:10 Oh, I don't know 00:16:12 alise: I tried that; I ended up thinking for hours* and not ending up with anything. 00:16:12 AnMaster: Were you not a child in '98 or something? 00:16:14 Whatever, enjoy the game, it's good 00:16:18 * Footnote. 00:16:31 pikhq, well, yeah, I was the nerd with glasses back then 00:16:41 well wait 00:16:45 that was 1999 maybe 00:16:50 alise: It was "Oh, hey, let me teach you how to catch Pokemon!" 00:17:47 I talked to that guy a lot in my Pokemon Blue playthrough. Hooray, Missingno glitch. 00:18:11 -!- Pthing has quit (Remote host closed the connection). 00:18:20 *Main> pretty (Set.unions [conjunction, disjunction, conditional]) 00:18:21 (if ⊤ then β else γ) → β 00:18:21 (if ⊥ then β else γ) → γ 00:18:21 (⊤ ∧ α) → α 00:18:21 (⊤ ∨ α) → ⊤ 00:18:21 (⊥ ∧ α) → ⊥ 00:18:23 (⊥ ∨ α) → α 00:18:38 I talked to that guy a lot in my Pokemon Blue playthrough. Hooray, Missingno glitch. <-- this was saphire or something like that..? 00:18:43 Sapphire. 00:18:51 The "main" GBA Pokemon game. 00:18:54 They're all pretty much identical, though. 00:18:59 heh? 00:19:03 Blue. The Gameboy game. 00:19:28 Had a large number of exploitable bugs. 00:19:39 missingno is beautiful 00:19:46 Missingno was the best-known. 00:19:52 http://www.utdallas.edu/~rxf023000/stuff/missingno.jpg 00:20:36 tree rewriting is fun 00:21:14 -!- Leonidas has joined. 00:21:35 -!- FIQ has joined. 00:21:40 -!- FireFly has quit (Quit: Leaving). 00:21:56 -!- FIQ has left (?). 00:23:30 okay, so basic rewriting steps: rewrite the outermost expression by matching it against rules; take the most specific (atoms rather than free variables) 00:23:52 bind any free variables, and repeat the whole process with the RHS of the rule 00:23:59 until no changes are made in one rewrite step 00:24:01 -!- Leonidas has quit (Read error: Operation timed out). 00:24:27 how do you do tree rewriting 00:24:41 like that 00:25:08 -!- zzo38 has joined. 00:25:11 There's actually 5 forms of Missingno... 00:25:18 what about maude 00:25:21 and CHR 00:25:54 That monstrosity, the Kabutops fossil, the Aerodactyl Fossil, the Ghost, and this monstrosity: http://bulbapedia.bulbagarden.net/wiki/File:000Y.png 00:26:01 MissPiggy: i'm lazy and want to do it stupidly 00:26:13 Last monstrosity Yellow-only, requires usage of the Mew glitch instead of the Old Man glitch. 00:26:14 besides, mine has unicode. 00:26:15 -!- Leonidas has joined. 00:26:17 -!- Asztal has quit (Ping timeout: 240 seconds). 00:26:19 (bug fixed in Yellow) 00:26:33 alise im writing an algebra systems 00:26:38 personal algebra sys 00:26:51 hmm, my rewriter should be a monady function for the error handling 00:26:53 as long as it isn't a grammar systems 00:26:54 and yield a list of rewrites 00:27:07 all you do is takewhile notidenticaltopreviousthingy on that to get the main reducer function 00:27:15 and last on that to get the normal form 00:27:18 why do you mean at least isn't a grammar systems? 00:27:26 15:08:29 I fail to see how much more wrong it is to having an undecidable type system, than to have an undecidable execution model, which is essentially a given. 00:27:30 my language has neither! 00:27:51 15:13:06 why not check the logs for when tusho was last seen <-- he calls himself uorygl these days 00:27:51 XD 00:28:13 my vague recollection database needs some cleanup 00:28:18 alise how do you know a rewrite system terminates? 00:28:28 not *that* language 00:28:34 alise I know a couple tricks 00:28:36 the other one, which for want of a better name is aliselang for now 00:28:39 alise: well _one_ of you better stop changing nick _all the time_ dammit! 00:28:43 oerjan: poo 00:28:44 alsie what about knuth-bendix completion 00:29:33 alise: hm i also vaguely recall discussing that takewhile notidenticaltopreviousthingy on #haskell 00:29:58 I probably was involved. 00:30:07 as something people confuse with fix, and maybe if it should be added to some library (don't recall if it was) 00:30:12 f your rewrite system is confluent fuck you 00:30:20 wait that didn't come out right 00:30:21 Either is a monad right 00:30:25 Either e 00:30:31 or was that until 00:30:32 yes yes 00:30:32 -!- zzo38 has quit (Remote host closed the connection). 00:30:33 MissPiggy: are you drunk btw :P 00:30:35 it's the only monad I have left 00:30:39 alise: Either e, but e needs a typeclass 00:30:49 oerjan: so it's not a monad in practice then 00:30:57 I just love term rewriting 00:31:06 sure it is, it's just for fail it's needed 00:31:19 what typeclass thenny 00:31:27 what are you writing thought 00:31:28 what are you writing though 00:31:29 alise 00:31:33 what are you writing 00:31:37 just a language 00:31:40 a little esolang 00:31:41 tarpit 00:31:43 rewriting tarpit 00:31:44 coool 00:31:51 like http://esolangs.org/wiki/Defcalc but better since I made it 00:31:53 i do everything better 00:32:00 alise: Error 00:32:21 oerjan: but i don't want to make Oops an Error 00:32:26 this is not really an esolang?? 00:32:27 it's a perfectly acceptable errory snowflake by itself! 00:32:31 MissPiggy: it's a tarpit 00:32:32 tarpits are esolangs 00:32:43 what do you mean it's a tarpit? 00:32:48 alise: it's for converting error messages into e 00:32:54 what, http://esolangs.org/wiki/Defcalc? 00:33:08 oerjan: fail should be in a separate typeclass :( 00:33:10 since e is intuitively the exceptional case 00:33:18 (in Either e) 00:33:44 what's meant by a tarpi 00:33:48 tarpit 00:33:49 MissPiggy: :| 00:33:58 a minimalistic language, that values minimalism above all else to the point of unusability 00:34:04 ideally, pure, condensed paradigm 00:34:10 oh like scheme? 00:34:15 no 00:34:24 Scheme is usuable. 00:34:24 like brainfuck and underload. 00:34:25 that was a joke :D 00:34:32 i was suspecting either a joke or a troll 00:34:36 but, you know, be nice alise 00:34:42 but Defcalc looks exactly like Q 00:34:42 Lazy K, Brainfuck, Underload, Unlambda... 00:34:50 which is not really considered an esolang 00:34:54 Oh, and HQ9+. 00:35:05 well it's the little niceties and efficient evaluation that make a lang not an eso one 00:35:06 (though not a *Turing* tarpit. Just a tarpit. :P) 00:35:17 ohhh 00:35:19 typed tree rewriting would be nice, nice 00:35:25 also pure is q++ 00:35:29 by the way 00:35:41 what tree rewrite programs do you do that aren't just functional programs? 00:35:47 dependently-typed typed tree rewriting + magical efficient evaluation algorithm = i'll just go retire 00:35:55 MissPiggy: well one you can do symbolic manipulation 00:35:59 so there's your CAS base right there 00:36:04 really? 00:36:08 sure, of course 00:36:15 symbolic evaluation == structure rewriting 00:36:16 I mean I switched from prolog to haskell because I wanted functions 00:36:32 two, you can do fancy syntax without any shit 00:36:54 as long as you can distinguish literal atom and variable you can have ``(lambda x ^^ q / r) and okay`` as a rewrite rule 00:36:59 why not 00:37:17 the only syntax you need is for defining rewrite rules, and parens 00:37:29 you can even implement operator associativity/precedence yourself 00:37:35 x + y + z = x + (y + z) 00:37:41 given = being rewrite 00:37:56 okay but I still don't really see it 00:37:57 for practical langs functional programming wins because you can evaluate it efficiently and the like 00:38:20 do these langauges implementaitons do things like Knuth-Bendix completion on your input 00:38:48 not that i know of it's really pretty simple to implement 00:39:20 you grep the set of rewrite rules, pick the one with the least free variables that fits the term, add rewrite rules with the free variables to their corresponding parts of the expression, and replace w/ the RHS 00:39:23 rinse, lather, repeat 00:40:24 MissPiggy: http://q-lang.sourceforge.net/examples/symbolic.q an example of symbolic stuff w/ rewriting langs 00:41:39 also http://q-lang.sourceforge.net/examples/dnf.q 00:41:54 btw guys i implemented deflate in ruby 00:42:14 hmm 00:42:29 I never really learned any more compression beyond arithmetic :( 00:42:33 it's fairly easy once you've nailed the dynamic huffman coding 00:42:34 which is totally cool but it's kind of basic 00:42:45 really its' just like dynamic huffman? 00:42:59 the ones I never really got were the LZwhatevers 00:43:00 the dynamic huffman blocks are done in a very clever way 00:43:16 it's LZ77/LZSS after the huffman coding 00:43:33 366 lines baby \o/ 00:43:37 alise, that DNF is pretty much the only rewrite system I know :P 00:44:10 doesn't take much brains to understand rewriting systems, makes sense quickly enough 00:44:33 I don't see the point of rewrite systems if they don't do a tremendous amount of analysis and derivation on your programs 00:44:36 you just have to rewrite your brain a little 00:44:39 why would anyone bother if you don't? 00:45:36 MissPiggy: because they're fun 00:45:36 esolangs 00:45:37 #esoteric 00:45:40 that's where you are 00:46:10 I read that whole book on All About Maude and I still don't really 'get it' 00:46:41 it's just functional programming where functions are constructors 00:46:49 disagree 00:46:51 maybe that's what the game is 00:47:03 unify functions and constructors into one thing: So that the idea is much simpler 00:47:12 so it's all just terms now (like prolog) 00:48:12 but a lot simpler than prolog 00:48:24 no searching thru logicspace and whatnot :P 00:48:37 just dead simple match term against most specific rule, replace with RHS 00:49:45 oh, one useful extra rule (maybe) is to have (just inventing syntax here) a->b : c 00:49:49 so you can do, for example 00:50:00 (lambda x e) y = x -> y : e 00:50:06 i.e., "with rule x -> y, e" 00:50:19 yeah but I mean 00:50:35 the obvious approach is to just take the equations in the program and rewrite them iteratively 00:50:47 but there is some algorithms, I think, which can improve it 00:51:06 oh, of course 00:51:08 same answer (assuming a confluent system) 00:51:16 but those are equivalent implementations, i.e. theoretically irrelevant 00:51:30 for purity and simplicity you look at the dumbest implementaiton 00:51:53 i think my language is all confluent and that jazz 00:52:04 incidentally tree rewriting systems leave io very simple and whatnot 00:52:05 if you do 00:52:07 * MissPiggy wonders what happen if you do 00:52:13 x + y = y + x 00:52:16 y + x = x + y 00:52:18 in Q 00:52:37 x <- e; y = x (lambda e y) 00:52:51 x; y = x (thunk y) 00:52:59 and then you can do 00:53:07 print "hi"; print "yo"; x <- getLine; print x 00:53:08 -> 00:53:19 heh cool 00:53:34 print "hi" (thunk (print "yo" (thunk (getLine (lambda x (print x)))))) 00:53:39 well, guess you need some sort of final terminator 00:53:46 x; = x (thunk nil) 00:53:50 anyway, that can reduce to say 00:54:05 putc 'h' (putc 'i' ... etc 00:54:08 * MissPiggy is gonna reskim term rewriting and all that 00:54:20 and when the getLine reduces, it all just turns into an inert structure 00:54:25 but since you're inherently lazily evaluating it 00:54:30 (because that's what term rewriting _is_, lazy) 00:54:36 you can output and input as you go 00:54:57 so you write a few terms inside the language, and have the runtime system just evaluate it and interpret a very very simple IO structure 00:55:04 and you have a syntactically-sugary IO system 00:55:12 can't really do that in the same way with functional langs 00:55:19 i mean, term rewriting _is_ functional 00:55:21 but you kniow what i mean 00:55:39 term rewriting is lazy? 00:55:55 well it can be 00:55:57 what if you have two rules that go to different foobars 00:56:02 K x y = x 00:56:07 K x destroyEntireWorld -> x 00:56:10 lol 00:56:12 destroyEntireWorld is never reduced 00:56:12 ok 00:56:17 yeah but it MIGHT be ? 00:56:21 why 00:56:38 well my thought with confluence is you'd expect x + y to be the same if you eval x or y first 00:56:41 because of K x (poop y) = ... 00:56:45 right 00:56:54 well sure 00:56:58 but that's the same way as haskell is lazy 00:57:01 you gotta force sometime 00:57:10 it's lazy enough to allow incremental io, is the point 00:58:49 you know the word problem? 00:58:58 you get a 'word' in group theory like 00:59:04 f*o*o*b*a*z 00:59:11 and you want to find out if it equals some other word 00:59:40 and you can only use the rules of group theory (the specific group might have certain new equivalences compared to an arbitrary group) 00:59:52 that is an undecidible problem but sometimes it is decidible 01:00:21 anyway, if you code that sort of thing into a rewrite system, like Q -- you will lose the declarative meaning of =, all = means in that case is LHS turns into RHS 01:00:28 I think ? 01:01:21 yeah 01:01:24 i think so 01:01:48 (if x then a else b) using 0/1 booleans: (a-b)x + b 01:01:54 I like the idea you can specify a theory by equations, then it decides equality on it 01:01:58 w/ iverson brackets: (a-b)[x] + b 01:02:37 x=1-[x=x] 01:03:03 is that x=(1-[x=x])? 01:03:08 presumably for x = 0 or 1 01:03:18 0=(1-1), yes, but 1 /= (1-1)... 01:03:45 x=[x=0] 01:04:27 well, of course. 01:04:52 ?? 01:04:57 -!- kar8nga has quit (Remote host closed the connection). 01:05:10 obviously x=[x=0] 01:05:23 same thing as saying x = (x = true) 01:05:28 0 is true? 01:05:33 i.e. x is true iff x is true 01:05:34 that's esoteric 01:05:39 erm, right 01:05:42 obviously the negation of that 01:05:44 :D 01:06:18 Well, thank you Xstreet SL, for essentially removing my free competitors from the public eye 01:08:05 * MissPiggy can't think of anything else than x=[x=0] 01:09:28 x=[x=1] :P 01:09:32 that is actually true for instance 01:15:03 1 + Sum{i = 1..} [i <= x] = x 01:15:22 smallest interesting number 01:15:37 XD 01:18:38 MissPiggy: remind me to define my own Eq that does alpha-conversion 01:18:43 (otherwise using Set is pointless) 01:19:43 dude 01:19:53 use de bruijn indices!!!!!!!!! 01:20:09 hmm 01:20:11 maybe i will. 01:20:12 yeah, i will 01:20:24 no 01:20:27 I won't 01:20:31 because in the end, *all* atoms are variables 01:20:36 so instead of if foo then bar else xyz 01:20:40 i'd get 3 293 54 2 01:24:18 MissPiggy: if i can actually get (dependent) typing onto a tree rewriting system 01:24:24 plus an efficient method of evaluation 01:24:28 aliselang will have changed completely 01:24:50 hmmmmmmmmmmmmmmmm 01:24:53 that's an interesting thought 01:25:14 one thing you don't have to worry about is pattern match coverage 01:25:54 why not? 01:26:11 heh, interesting thing is that you can have a function of forall a. a -> ... 01:26:14 and do actual meaningful processing 01:26:19 because it's not functions 01:26:22 (since it'd let you do any rewrite) 01:26:30 it'd be a very different type system 01:26:34 only used to restrict rather than to relax 01:26:57 yeah since you have stronger conversion than normal reduction that might be nice for type checking and proofs 01:27:13 reflective proving might be possible without quotation :o 01:27:58 the thing with a tree rewriting system is that values are never magically created 01:28:06 every value exists in stasis, because it's just an inert term 01:28:40 set N = { 0, S (x:N) } 01:28:48 then S : N -> N 01:29:02 but S wasn't created by doing that 01:29:10 it was just given a more restrictive type, and added to a set 01:29:16 well 01:29:21 its "result" was added to a set 01:29:24 not the rule it self 01:30:02 * alise sticks to the convention uppercase=free variable 01:31:11 set C = { (A:R) + (B:R) i } 01:31:33 I think as long as x + (y i) isn't defined, i.e. i is inert and + doesn't match on it, that's perfectly fine 01:31:38 and lets you say 2 + 3 i 01:31:51 hmm, dunno how to do type inference 01:31:55 there's no barrier to a value being in two sets 01:33:32 MissPiggy: this is really interesting 01:33:47 yeah it is actually 01:33:49 set B = { 0, 1 } 01:33:55 set N = { 0, S (x:N) } 01:33:59 but 1 is just sugar for S 0 01:34:06 so we have 01:34:10 set B = { 0, S 0 } 01:34:13 mmm, sugar 01:34:14 set N = { 0, S (x:N) } 01:34:28 in B, S 0 I think would turn into S (0:B) 01:34:40 since S : a -> a would be defined before, i.e. 01:34:45 no matter what type you make it, it never changes the type 01:34:52 so we'd be able to infer that B is a subtype of N 01:35:05 and you'd be able to take the factorial of true :-) 01:35:53 [true]! 01:36:18 [x] = x if you have 0, 1 as booleans 01:36:27 hmm 01:36:40 you can implement optimisations inside the language!!! 01:36:49 map F (map G XS) = map (F . G) XS 01:37:09 * MissPiggy tries to make the biggest number I can out of iverson bracket using the fewest number of symbols 01:37:15 MissPiggy: guards would be nice, meaning "this only actually matches the terms if" 01:37:29 alise, CHR has like 01:37:39 head <=> guard | body. 01:37:52 and guard is optional 01:38:00 but it's not a rewrite system 01:38:34 N ! | 0 < N < 2 = 1 01:38:42 N ! | N >= 2 = N * (N-1) ! 01:38:50 that way you could define N ! for negative N separately 01:39:06 because if N < 0, those rules don't match 01:39:59 map F (XS ++ YS) = map F XS ++ map F YS 01:40:00 hahah 01:40:08 you can literally translate haskell optimisation rules directly into tree rewriting ones 01:40:24 the only thing more you need is a declaration specifying "this would be clever to do at compile-time" 01:40:29 maybe not even that given a sufficiently-smart compiler 01:41:01 hmm, I guess to infer types you need something like 01:41:08 0 : B | N | ...tons of types... 01:41:40 i like this i do, i do 01:41:49 I can't make big numbers using the iverson bracket :( 01:42:01 it's stronger than mu!! this should be easy 01:42:03 i love how you can just define 01:42:06 x < y < z 01:42:08 separately 01:42:19 how come it doesn't get confused with x < y? 01:42:30 because it's more specific, i.e. you have to add less stuff 01:42:37 a free variable (i.e. argument) counts as adding stuff 01:42:41 adding parens counts as adding stuff 01:42:50 and adding parens is more serious than a free variable 01:42:59 ahh 01:43:02 so if you can choose either x < y < z or x < (y < z), x < y < z wins 01:43:03 so it's like object oriented 01:43:07 not really :P 01:43:13 it's just part of the "pick the most specific rule" 01:43:59 that sounds like OO 01:44:25 howso? 01:45:00 it's just to resolve ambiguous rules... if you have an x + y rule and an x + 0 rule, obviously you want to pick the latter; so you select the one with the least free variables 01:45:34 and if you have x < y < z, well X < Y < Z is a more specific rule than X < Y for that, we know this intuitively; and since the former would be x < (y < z) or (x < y) < z, we can say this as: pick the one that makes us add the least parentheses 01:45:48 X < Y < Z has one more free variable than X < Y, but the parens rule takes precedence over the free-variable rule in all cases 01:46:19 i may just be a genius 01:46:54 MissPiggy: one issue with tree rewriting is that you can just add any old typo and it works as a variable name 01:46:57 because it's just an inert tree 01:47:08 but you can have a rule, say 01:47:12 (in the compiler) 01:47:36 any name not in a set or used in a rewrite rule that matches it triggers an error and halts compilation 01:47:48 unless you add some compiler decl to say "it's okay man" 01:49:40 MissPiggy: should work right? 01:49:45 90% of the time you'll work with typed stuff 01:49:57 hmm, merd has those Foo | Bar types 01:50:10 alise these was an idea to use term rewriting in Coq 01:50:14 [[the type of list [ 1, "foo" ] is a list of elements of type 1|"foo"]] 01:50:19 -!- Gracenotes has quit (Remote host closed the connection). 01:50:21 stuff like 0 + x --> x and x + 0 --> x 01:50:32 incidentally the Int/Integer bullshit you get in haskell doesn't exist in this lang 01:50:39 because Int would be a subset of Integer 01:50:43 the interface would be like 01:50:57 set Int = { 0, 1, ... abignumber } 01:51:05 set Integer { 0, S (N:Integer) } 01:51:16 and since 1 = S 0, 2 = S 1 = S (S 0), etc., they come out to be subsets 01:51:36 of course, it means that what's of type Int changes depending on the machine, which is worrying 01:51:38 but perhaps cool 01:51:45 programs that will overflow just won't compile 01:52:11 i'm really liking this idea 01:52:46 MissPiggy: i'm digging it are you digging it :| 01:52:47 DIG IT 01:53:24 say, we can do currying with this thing 01:53:26 Wait, is this turing complete? How can a compiler for a turing-complete language detect that something will happen? 01:53:42 f x y can be (f x) y and rewrite just fine 01:53:47 since the rewrite rule will have less parens, blah blah 01:53:49 how can a compiler really KNOW anything? 01:54:02 Sgeo: because x+y : Int is only acceptable if x+y is of type Int 01:54:19 if Int is a finite set, given the definition of addition, we obviously know the top element 01:54:32 i'm tired 01:54:51 May I assume that the compiler will complain even in cases where an overflow would never occur? 01:55:26 well you couldn't define + : int -> int -> int i don't think 01:55:36 because what is maxint + maxint? 01:55:51 it'd have to be int -> int -> maybe int, or +overflowing : ... 01:57:05 I like Fortress' syntactic heresy 01:57:12 a[x] -> a_x especially 01:58:30 Fortress is pretty cool looknig 01:58:31 MissPiggy: have you used texmacs? 01:58:32 looking 01:58:37 it looks good, maybe a good editor for my lang 01:58:42 yeah I like texmacs though it's horribly slow to use 01:58:43 what with its mathematically notation stuff 01:58:50 there's some algebra systems in it which is nice 01:59:00 slow is it? I'm installing it now so yeah 01:59:10 would be so so so cool to use it for a programming language :P 01:59:21 well if this goes well that is my plan :) 01:59:24 I want epigram mode in texmacs with all the coloring in 01:59:41 nice fancy syntactical, typed tree-rewriting language 01:59:46 it'd be so... lovely 02:00:44 will take some getting used to that (forall a b. a -> b) can actually have some meaningful values, though 02:00:46 like 02:00:53 frobnicate 0 = 72 02:01:00 * MissPiggy looks up rewriting on wikipedia -- there is a Philosophy section 02:01:08 frobnicate "a" = [00,"haberdashery"] 02:01:12 frobnicate X = X 02:01:14 Philosophy of term rewriting: What does it mean for a term to be rewritten? 02:01:18 xD 02:01:26 At what point does a term cease to exist? 02:02:25 the only thing aliselang was missing was the CAS 02:02:30 adding symbolic stuff seemed like an afterthought 02:02:37 but if I can blend Agda and Q/Pure, well, why the fuck not 02:03:19 I love sites like this http://rewriting.loria.fr/ 02:03:35 the moment you see that banner you know the authors of this site LOVE term rewriting 02:03:44 lol 02:04:09 methinks a functionalish type system for a term rewriting language will be way different to anything the haskellers have ever seen 02:04:19 for instance, if you have a rule (foo X Y), that doesn't mean that foo : that 02:04:28 in fact, you need syntax as part of the types 02:04:32 principle typing 02:04:33 GONE 02:05:10 like 02:05:14 say you want the analogue of 02:05:18 apply :: (a -> b) -> a -> b 02:05:21 it'd be 02:05:44 assuming that by (a -> b) 02:05:47 we want a rewriting term 02:05:49 not some lambda structure 02:05:53 like, apply apply should be acceptable 02:06:27 apply (x | x A : B) A : B 02:06:28 I think 02:06:33 because it's not just a -> b 02:06:37 it could be x ? y : z 02:06:39 and then x A wouldn't work 02:06:52 in fact you couldn't pass it as-is because it doesn't have one name 02:07:23 of course, the sane thing to do is just to have (λ(X Y Z) X ? Y : Z) :P 02:08:44 well, one thing's for sure 02:08:47 this language won't be more of the same... 02:09:01 we're so used to thinking of applying function-values to other values 02:09:13 but first class rules is a damn interesting idea 02:09:46 fortress's automatic parallelisation is sweet 02:09:54 that's really easy with term rewriting i think 02:10:05 since it's literally just splitting the evaluation of a term if you deem it good 02:11:53 MissPiggy: another thing tree rewriting languages can do: invert functions 02:12:01 what?? 02:12:02 since lambdas have their contents exposed, you just fiddle about a bit 02:12:04 well not all functions obviously 02:12:05 but i mean 02:12:08 in haskell functions are opaque 02:12:10 but if you have 02:12:16 set A -> B = { Lam ... } 02:12:18 in a term language 02:12:26 their bodies are just inert blah blahs 02:12:31 and you can rewrite them as usual 02:12:55 http://www.cs.tau.ac.il/~nachumd/rewrite/index.html lol this page as tags term rewriting enthusiasts are crazy 02:15:36 you could have a term like 02:15:37 err 02:15:40 i'll just give an example 02:15:43 N ! = ... 02:15:55 doc (N !) = "blah blah blah" 02:15:57 and you could do 02:16:02 doc (3 !) and get factorial's docs 02:16:04 or doc (n !) 02:16:05 etc 02:16:13 i think the type would be 02:16:28 doc : forall a b. a -> (String | b) 02:16:33 the | b being implicit i guess 02:16:37 since if you have undefined cases 02:16:42 like doc "a chicken" 02:16:46 it'll just return doc "a chicken" 02:16:49 so you'd just write it as 02:16:52 doc : forall a. a -> String 02:18:42 one thing's for sure 02:18:46 TeXmacs is beautiful 02:18:53 i love computer modern 02:20:15 yeah I like it 02:21:27 http://www.cs.unm.edu/~mccune/sobb2/ 02:23:46 haha 2 \over2 in TeXmacs shows as 2 0.5 02:24:21 Time to WinDirStat 02:24:58 90MB of free space o.O 02:26:10 MissPiggy: wow texmacs is nice, why do people use silly things like lyx 02:26:39 well i don't actually write TeX :D 02:26:56 I j ust wanted it for a GUI 02:27:26 tex is convenient for quick mathematical stuff, though 02:27:37 * MissPiggy uses paper 02:27:44 I think I should learn LaTeX 02:27:44 less quick than that :P 02:27:46 I mean quick to input 02:27:52 besides, why write A[N] when you can write A_N eh 02:30:44 admittedly what I really want is you type A[ and see A(subscript cursor) 02:30:59 then you type N and see A(subscript N with some sort of red cursor to the right indicating "incomplete") 02:31:06 then you type ] and the cursor gets big again and non-red 02:34:47 I want to have italic lowercase names as vars in the viewing form of my lang because it's prettier but it creates a bad clashing with the Foo syntax of the ascii form :( 02:40:56 MissPiggy: what do you think of literate programming? 02:41:33 I LIKE it 02:42:01 MissPiggy: but do you LIKE IT like it? 02:42:12 yes 02:42:15 Why does Chrome hate Reddit so? 02:42:16 100% 02:42:35 MissPiggy: Then what do you think of TeXmacs literate programming where a non-literate program just happens to be entirely within an equations block?! 02:42:48 Literacy for all! 02:44:22 personally i think only literates should be allowed to program 02:48:31 MissPiggy: agree or disagree: fortress sticks a little *too* close to mathematical notation 02:48:43 no clue .. 02:48:51 imo it does; it even uses |x| for abs 02:48:59 well I hate |x| 02:49:15 oerjan: Hear hear. 02:49:23 a lot of the time, mathematical notation sucks 02:49:30 because there isn't really any underlying rules, at all 02:49:38 you just invent domain-specific notation, regardless of any clashes 02:49:58 Many of the ideas in mathematical notation are decent. 02:50:08 Unfortunately, it clashes a *lot*. 02:57:27 * Sgeo now has 15.2GB free :D 02:57:40 Removing Portal and Team Fortress from my HD really helped 02:58:44 -!- Asztal has joined. 02:59:48 hmm 02:59:57 how easy is it to get real LaTeX to render in realtime, I wonder? 03:00:04 complete expressions, just... really quickly and incrementally 03:00:44 "And that, friends, is how I solved the Halting Problem." --Conor McBride 03:03:45 MissPiggy: I think I prefer having set C = {Foo (a:R) (b:R)} 03:03:48 then having 03:03:57 i as a separate thing 03:04:03 so that a + bi can be a + b*i 03:04:10 but... is having juxtaposition as multiplication really something I want? 03:04:31 no it's not! 03:04:38 right 03:04:43 but otherwise, a + bi looks ugly 03:04:46 because i has to be in text 03:04:49 (because italics = variable) 03:04:57 so you get itaaaalic bSTRAIGHT i 03:08:03 MissPiggy: so, that's one problem with tree rewriting systems 03:08:11 variable vs atom 03:08:35 huh? 03:08:40 why is it a problem? 03:08:48 if x then y else z 03:08:52 you need to mark the variables right? 03:08:53 Chrome hates Reddit :( 03:08:54 if X then Y else Z 03:08:56 in the LHS of a rule 03:09:01 so then when you go to define complex numbers 03:09:11 set C = {(A:R)+(B:R)i} 03:09:17 so your wonderful function working on complex numbers 03:09:19 has to say 03:09:24 (A + B i) 03:09:28 this is fine in ascii, absolutely fine 03:09:42 but when you go into TeX-esque land, 03:09:54 you think hey, it'd be nice if italics = variable and roman = literal 03:09:59 after all, that's how mathematics is usually typeset 03:10:00 so 03:10:01 you get 03:10:03 a + bi 03:10:05 rendered as 03:10:10 italic a + italic bSTRAIGHT i 03:10:19 and it looks unnatural and weird 03:10:20 and you are sad 03:10:58 or maybe I'm crazy and it's fine 03:11:45 MissPiggy: one thing I'd like is to have two definitions of types, functions etc 03:11:57 one is the equational definition, which is the simplest, purest form; inefficient as hell 03:11:59 and one is the runtime definition 03:12:11 the former is used for everything but the actual crunch time, making inferring things, etc. easier 03:16:24 it is stupid how little fancy stuff today's languages have 03:19:09 -!- rodgort` has quit (Quit: Coyote finally caught me). 03:21:24 int64? bah. more like \mathbb{N}_{64} 03:21:32 alise: actually i think i is usually typeset as a variable 03:21:39 oerjan: exactly, but you can't 03:21:42 because it's not a variable 03:21:48 it's part of the syntax of the rewriting rule 03:22:00 you could define set C = { boring stuff } and have i be a separate variable, I guess 03:22:06 but you wouldn't be able to pattern match on it 03:22:09 which is lame 03:23:10 ah 03:23:51 by 03:25:06 -!- MissPiggy has quit (Quit: Lost terminal). 03:46:33 As a bonus, you also get "constructors with equations" for free. E.g., suppose that we want lists to automagically stay sorted and eliminate duplicates. In Pure we can do this by simply adding the following equations for the : constructor: 03:46:34 > x:y:xs = y:x:xs if x>y; x:y:xs = x:xs if x==y; 03:46:34 > [13,7,9,7,1]+[1,9,7,5]; 03:46:34 [1,5,7,9,13] 03:46:36 pure is so cool 03:46:38 -!- augur has joined. 03:57:05 -!- jcp has quit (Remote host closed the connection). 04:02:31 That is rather cool. 04:03:28 i'm thinkin' 04:03:31 typed term rewriting 04:03:33 next big thing? 04:10:39 Maybe. 04:11:37 -!- GreaseMonkey has quit (Ping timeout: 256 seconds). 04:11:58 -!- GreaseMonkey has joined. 04:13:33 What we need is a typechecker for Thue. 04:14:03 and T::=T 04:14:07 "Oi, what? I don't think so." 04:24:09 pikhq: \mathbb{Z}_32. Bit-specified integers have never looked so classy. 04:24:48 *_{32} 04:25:09 alise: Heh. 04:26:17 oerjan: shaddup 04:26:36 also, that would be 5 bits, not 32 with usual meaning 04:28:01 oh, I forgot stupid mathematicians overloaded it 04:28:03 idiots :P 04:28:14 * oerjan cackles evilly 04:28:17 \mathbb{Z}_{2^{32}} right? 04:28:24 right 04:28:24 well that's just even classier. 04:28:52 n \textnormal{bits} = 2^n 04:28:57 * Sgeo just sent for a self-test kit to go on a bone marrow donor registry 04:29:03 \mathbb{Z}_{32 \textnormal{bits}} 04:29:07 Sgeo: aiee the pain 04:29:08 ow ow ow 04:29:32 I'm pretty sure there won't be any pain unless I end up actually donating 04:29:34 \times or \cdot for the standard multiplication operation, I wonder? 04:29:37 And even then, it's worth it 04:29:37 \cdot is lighter 04:29:48 \times is more... timesy 04:29:52 * oerjan really hopes Sgeo doesn't have to get an actual bone marrow sample for the test 04:30:03 oerjan: I doubt that would be a self-test. 04:30:04 It's a cheek swab 04:30:21 oh not even drawing blood? pussies! 04:30:21 Sgeo: Coated with sulfuric acid! 04:30:29 04:31:18 alise: so, get with the \times? 04:31:19 * alise tries to figure out how to tell LyX to add more spacing in between the equations 04:31:55 Isn't it better to convey semantic meaning? 04:32:09 that doesn't change the fact that the output is ugly because it's too close together 04:32:47 but, god, \textnormal{set }\mathbb{Q}&=\left\{ \frac{n:\mathbb{Z}}{d:\mathbb{Z}}\right\} may just have been the most beautiful thing I've written in my entire life 04:32:55 er, should it be \textnormal{set } or \textnormal{set}\ ? 04:33:01 -!- augur has quit (Ping timeout: 256 seconds). 04:36:01 anyway 04:36:06 set Q = {(N:Z)/(D:Z)} 04:36:06 (A/B) + (C/D) = ((A*D) + (B*C)) / (B*D) 04:36:06 (A/B) * (C/D) = (A*C) / (B*D) 04:36:07 -> 04:36:13 \textnormal{set }\mathbb{Q}&=\left\{ \frac{n:\mathbb{Z}}{d:\mathbb{Z}}\right\} \\\frac{a}{b}+\frac{c}{d}&=\frac{(a\times d)+(b\times c)}{b\times d}\\\frac{a}{b}\times\frac{c}{d}&=\frac{a\times c}{b\times d} 04:36:30 (just imagine something terribly pretty) 04:36:51 Render it and put it online and show us! 04:37:01 I'm trying to, but I can't get LyX to space it out some more! 04:38:06 There; using the principle of the Most Horrific Hack, I just added dummy lines in-between. 04:38:14 oerjan: \textnormal{set }foo or \textnormal{set}\ foo? 04:38:43 bah 04:39:05 wut 04:39:19 will set always be used with a space after? 04:39:31 otherwise the second seems more logical 04:41:47 well, the syntax we're expressing is "set NAME = {...}" 04:41:48 is set a command or a part of "set Q"? 04:41:51 ok 04:41:59 set as in a set set 04:42:00 as in a type 04:42:05 as opposed to "set var = val" 04:42:07 in that case it would be more logical to have set _outside_ the math 04:42:20 erm, but it's in an equation block thingy 04:42:24 i suppose that may not ... right 04:42:55 also why \textnormal and not \mbox 04:43:22 dunno, i'm really completely clueless with latex ::) 04:43:24 *:) 04:43:38 i guess the spacing may be slightly different and superioer with set}\ 04:43:42 due to italic/roman differences 04:44:46 maybe 04:44:48 i need somewhere to dump this pdf 04:45:19 * oerjan just cannot recall using \textnormal before. not that he recalls all of latex anyhow. 04:48:18 Sgeo: you have some sort of dumping ground webspace right? 04:52:22 alise, yes 04:52:38 got 68 kilos free for a wonderful little pdf? :{ 04:52:42 Yes 04:52:58 Although I'm sure you could use Normish if you wanted 04:53:16 I'd be happy to put it on on diagonalfish 04:55:31 I don't even know if my Normish account still... exists. 04:56:37 I don't think normish accounts die 04:56:50 Does Normish exist? 04:56:50 But normish.org isn't working. THe IP addy is in #rootnomic 04:57:11 * Topic for #rootnomic is: If connecting to normish.org doesn't work, try its IP address: 209.20.80.194 04:59:33 http://sgeo.diagonalfish.net/alise/Q.pdf 04:59:37 In which a delight taking the form, 04:59:37 set Q = {(N:Z)/(D:Z)} 04:59:37 (A/B) + (C/D) = ((A*D) + (B*C)) / (B*D) 04:59:38 (A/B) * (C/D) = (A*C) / (B*D) 04:59:39 is experienced. 05:00:55 * Sgeo feels useful 05:01:55 More useful than a hedgehog. 05:06:50 Not ... SONIC the Hedgehog?! 05:07:23 He's not actually a hedgehog. Evidence: He doesn't look like a hedgehog, his speed isn't that of a hedgehog, he can't swim but hedgehogs can, and he can talk. 05:11:54 are you _sure_ he cannot swim? maybe he's a witch! 05:12:21 let's get some ducks and compare weights. 05:13:10 I haven't seen any evidence that he can't swim. 05:13:30 i knew it! burn the witch! 05:14:48 also, the code is slightly misleading 05:15:08 in that you can have no other x/y or \frac{x}{y} of a type other than Q without clarifying the argument types in the +/* rules 05:15:34 i also sense a division by zero. 05:16:16 your mom is a division by zero 05:16:46 anyway x/0 will work perfectly fine so long as you don't try and do anything with it :P 05:17:03 O_o 05:17:09 term rewriting, oerjan 05:17:11 term rewriting 05:17:32 ok admittedly I'll probably have X/0 = some error 05:17:52 I'm rather certain x/0 works just fine so long as it's not evaluted in Haskell. ;) 05:18:00 Evaluated, even. 05:18:11 X/0 = error 'zero denominator' 05:18:16 where '...' = atom quoting 05:18:16 you're going to get trouble if you want to do theorem proving on that Q, though 05:18:19 i.e. foo = 'foo' 05:18:26 oerjan: well it's term rewriting, so you don't need to 05:18:29 how would you solve it anyway 05:18:40 you could have another set instead of Z as the denominator 05:18:49 set YeOldeZ = {1,2,...} 05:19:23 well i wasn't sure if you had left dependent types behind at the moment 05:19:28 this is a separate language 05:20:27 perhaps the two will merge; meet at the twain of betwixted befuddlement; aye, such a language would be a grand affair; or even grandiose; or more superlative experiences, but I digress, for the only truly thing in this world is that one be dependently typ'd and all that entails and the other be typ'd but, alas and yet yey, a rolling roaring proof-addict-not system of rewriting terms; so nilly-willy! 05:20:35 also, it's 5:20 am and I need sleep 05:22:04 sleep or loquacious prose, that's the question 05:23:10 Insert some off-the-cuff pun about country matters; for in times of reference, great great wars of reference, it seems side-references of great punnery are the only resort; recourse; holiday resort, aye, that would be a place to be 05:23:39 BUT! AND! IF! IS! THE! WHAT! Never to be never to be said the bee; I'll never be a bee who'll never be one never to be never to be; thus spoke the bee. 05:23:41 of course a recourse 05:24:00 And if the bee was never to be would a never-bee be a bee? Or would a never-bee never be a bee, much less in a bee's holiday resort? 05:24:13 eric the half a bee! 05:24:42 well, close anyhow 05:24:49 And what of the woodchuck, friend of the never-bee? How much never-bee wood would a woodchuck, friend of never-bee, chuck, if a woodchuck, never to be a never-bee; like the never-bee, who is never to be never to be a never-bee; could chuck never-bee wood? 05:26:05 about 5 tonnes. 05:26:41 AND HOW! As this 5:24 dawns the sound or silence of sleep as a propositional idea, presenting itself so sweetly, does nimble onto my tongue and lips and mind, but though I ignore it it presses at me, and yet this activity - of perhaps drunken in a way but only on unsleep (can it be said to be an entity? Certainly we cannot say such because it is the lack of an entity, but Douglas Adams had no problem with an item called no tea in his game) - portraying a vi 05:26:41 ew of insanity that somehow delicately dances on the thinking organs and amuses one so great as to flutter and carbonise the world, aye, that'd be it. 05:27:46 now you are just abusing the fact we cannot call you insane here 05:27:46 aye I do realise that the use of the word aye pr'haps verges on cliche now, but fuck you; no seriously, not as a joke, fuck you. all the insects are all like 05:27:48 FUCK YOU 05:27:53 AND THEY ARE COMING 05:27:56 THEY ARE COMING FOR YOU 05:27:59 FFFFFFFFFFFFFFFFUUUUUUUUCK 05:28:03 Y O O U U U U U O UO U U 05:28:05 U O O ---- 05:28:06 O 05:28:08 O 05:28:09 o 05:28:10 O fui 05:28:11 O 05:28:12 Fuc 05:28:15 you K k 05:28:19 AND THEN 05:28:22 n 05:28:23 o 05:28:24 t 05:28:27 h 05:28:29 i 05:28:31 n 05:28:33 g 05:28:36 . 05:28:59 i'm sure there's somewhere that would publish that. 05:29:10 signed, 05:29:11 well for a small fee, anyhow. 05:29:18 E.E. Cummingtonites 05:30:06 ALTOIDS HAVE YOU ANY IDEA STRONG HOW THEY ARE? 05:30:15 you release the woooooooooooorld 05:30:55 release the world and breathe free 05:31:18 receive everything 05:31:20 not just fire but EVERYTHING 05:31:23 okay, not everything 05:31:24 but EVERYTHING 05:31:26 the THINGS 05:31:28 you can REALISE 05:31:30 they are NOT endless 05:31:34 but they are unequivocable 05:32:24 out bitches, i'm out, i'm totally out, but just for a day hey hey i'll be baaaaaaaack again another day 05:32:27 to send all my bullshit your way 05:32:40 and thus ends, thus ends, thus ends, the world not with a bang but with a whimper the worst song ever created. 05:33:09 whew 05:33:22 BUT WAIT 05:33:22 wait, what? 05:33:23 THERE'S MORE 05:33:32 BUT YOU SAID IT ENDED 05:33:33 YOUR UNCLE IS SECRETLY A WHORE 05:33:35 I LIED 05:33:36 I DIED 05:33:37 I CRIED 05:33:39 I ESPIED 05:33:42 maaaaaaaaaaaaaaaaaaaagic 05:33:43 Order my uncle now? 05:33:46 in the aiiiiiiiiiiiiiiiiiiiiiiiiiiiir 05:33:51 peaaaaaaaaaar 05:34:00 derriere 05:34:09 antelopesque 05:34:10 * oerjan kicks alise's derriere 05:34:12 Kafkaesque 05:34:14 same bloody thing 05:34:15 RING A DING DING 05:34:20 poop 05:34:23 AND LOZENGES 05:34:25 poop 05:34:29 poop, poop AND LOZENGES 05:34:35 LOZENGES, poop poop and poop 05:34:38 spam, LOZENGES, and poop 05:34:44 aye. 05:35:08 i think a comparison to vogon poetry is appropriate at this point. 05:35:36 vogons don't drink lozenges 05:35:42 and they don't inhale spam 05:35:46 not a valid comparison, you lose 05:35:54 they _exhale_ spam. close enough. 05:36:15 don't make me kill your fam', spam-hugging man. 05:36:25 also i was going to say vogon poetry didn't reach to your knees, here 05:36:35 you're _far_ worse 05:36:41 y 05:37:02 -!- Gracenotes has joined. 05:37:36 your knees? cheese 05:37:39 fuck the authority, please 05:37:50 On the topic of esoteric languages: 05:37:52 I just realised that Boat should be turing complete 05:37:53 the bee's knees, in this case 05:38:00 can you guys verify this? 05:38:05 boats are turing complete, hoist the sails 05:38:09 OH NO IT'S SINKING 05:38:12 grab the wooden pails 05:38:13 no they aren't 05:38:17 nuclear submarines are 05:38:22 NUCLEAR FUCKING DEATH 05:38:22 because c is a nuclear submarine 05:38:26 YEAHHHHHHHHHHHHHHHHH 05:38:30 and we all know that c is the only programming language ever 05:38:49 except for python 05:38:55 but python is a scripting language 05:38:57 so it doesn't count 05:39:18 goat 05:39:26 Actually, we all know that Haskell is the only language. 05:39:26 ahahahaha goat 05:39:31 Everything else is a poor imitation. 05:39:37 Haskell and C are the same thing 05:39:38 is this what being high is like, i should just sleep less often 05:39:41 like the two calculuses 05:39:42 but not now, now i should sleep 05:39:47 alise: Yes. 05:39:59 however 05:40:04 just the two calculuses 05:40:05 pikhq: what was that a yes to 05:40:11 Hallucinations should start after 48 hours awake. 05:40:15 C and Haskell have fundamental differences 05:40:17 alise: "Is this what being high is like" 05:40:21 good to know 05:40:29 C and Haskell are coded utterly differently 05:40:30 good to Florence Nightingale the turtlefish 05:40:40 if you know what i don't mean 05:40:56 Wareya: That's because Haskell makes abstraction easy. 05:41:01 And C makes abstraction a bitch. 05:41:09 I can do abstraction in C 05:41:17 it's my whole coding style 05:41:18 Yes, but it's difficult. 05:41:21 i can eat an anus 05:41:24 doesn't mean it's easy 05:41:24 it's the only way 05:41:25 I 05:41:26 can 05:41:27 code C 05:41:31 also, caffiene 05:41:33 best drug 05:41:34 EVER 05:41:34 In Haskell, each and every function makes a new abstraction. 05:41:36 DON'T YOU WANT SOMEBODY TO ABSTRACT 05:41:39 DON'T YOU NEED SOMEBODY TO ABSTRACT 05:41:46 WOULDN'T YOU ABSTRACT SOMEBODY TO ABSTRACT 05:41:49 YOU BETTER FIND SOMEBODY TO ABSTRACT 05:41:52 alise: Go for 78 hours without sleep 05:41:53 Wareya: Well, yeah. That is a sane way to code. 05:41:54 with caffiene 05:41:55 abstract a rabbit 05:41:57 godle 05:42:00 Wareya: meh 05:42:00 Abstractions make code easier. 05:42:08 anyway 05:42:11 http://esoteric.voxelperfect.net/wiki/Boat 05:42:18 can you guys confirm if this is turing complete? :< 05:42:23 stop linking or i will never leave 05:42:30 okay 05:42:33 prove it identical to brainfuck or lambda calculus 05:42:40 All memory addressing is treated as big endian 05:42:42 no bignums? 05:42:43 you should be able to implement brainfusk 05:42:47 fixed size pointers you mean? 05:42:47 bignums? 05:42:49 arras 05:42:50 arrays 05:42:58 you can store pointers in a fixed point in memory 05:42:58 but 64-bit? 05:43:00 128-bit? 05:43:02 you can also point to pointers! 05:43:03 or infinity-bit? 05:43:04 yes 05:43:06 casting 05:43:09 which 05:43:11 you can cast to any number of bits 05:43:12 do you have infinity-bit 05:43:19 is infinity a number? 05:43:22 including 93847589347539847589347598347589347589345893457894375893475843957349853489534759? 05:43:24 irrelevant 05:43:34 CANT INFINITY 05:43:37 LOLP 05:43:44 well here i was thinking you were asking a question 05:43:50 I am 05:43:51 if you were answering mine i'd tell you whether it's tc 05:43:57 Wareya: but can you use an unbounded number of bits in the same program? otherwise you might have problems using unbounded memory 05:44:00 can i have a 409573498573984572398463874751834957298357287589175817346581732568714658734658745345-bit number 05:44:00 you can store a pointer in negitive addressing 05:44:05 answer that 05:44:10 and add/subreact to the addressing 05:44:12 yes alise 05:44:20 and use the pointer as normal 05:44:22 does it have flow control 05:44:34 you have if tests and while loops and 2D goto 05:44:44 80% probability of tc 05:45:00 _if_ you have unbounded memory 05:45:11 if he has such big pointers and they work it's unbounded prolly 05:45:16 Wareya: I'm pretty sure that's TC. 05:45:28 awesome 05:46:23 q[n]access memory at address q with n bits in size -- you could see 32[30] which would access the long integer at addresses 27, 28, 29, and 30. Yeah, it's big endian, but that might change as this goes. I guess I could get away call this as a special case for an array of bits. 05:47:00 "+" = `a`[`b`] = `a`[`b`] + 1, "-" = `a`[`b`] = `a`[`b`] - 1, ">" = `b` = `b`+1, "<" = `b` = `b`-1, "[ ... ]" = %(`a`[`b`] != 0){ ... } 05:47:06 Okay, proved it's TC. 05:47:12 but 05:47:21 I don't have variables anymore 05:47:26 (q[n])[y]use value of size n at address q as an address for a value size y -- I need a better way to do this 05:47:49 halp 05:47:56 Wareya: how do you use unlimited memory in a single program 05:48:07 malloc 05:48:17 oh you have malloc? 05:48:24 no, but 05:48:26 so it's a boring conventional ish language then 05:48:27 yawn :P 05:48:33 heh fun consequence of my language 05:48:35 hex literal: 05:48:40 DEADBEEF[16] 05:48:42 can you figure out why? 05:48:47 hint: array indexing 05:48:50 the interpreter should allocate as much memory as the program asks for, dynamically 05:48:57 like if it comes to a pointer to 0x5000 05:49:08 Wareya: i am of course asking how you _refer_ to unlimited memory if bit sizes must be given 05:49:11 and it used to have a pointer to -0x50 05:49:29 then you should have a 0x5050 sized memory array 05:49:35 Oh, it handles memory just like BF does 05:49:58 that or I don't understand what you're asking 05:50:01 infinite tape? 05:50:04 yes 05:50:08 infinite tape 05:50:15 moving backwards and forwards? 05:50:20 yes 05:50:21 pikhq: you tell me 05:50:24 c'mon, before I sleep :| 05:50:29 hex literal: 05:50:29 DEADBEEF[16] 05:50:29 can you figure out why? 05:50:29 hint: array indexing 05:50:32 ok then 05:50:43 -!- augur has joined. 05:50:57 but I need a better way to refer to pointers 05:50:58 -!- GreaseMonkey has quit (Quit: HydraIRC -> http://www.hydrairc.org <- Nobody cares enough to cybersquat it). 05:50:59 I mean 05:51:00 alise: Uh. 05:51:06 pikhq: hint: mathematical notation 05:51:12 refer to an address with a value inside of an address 05:51:34 alise: You're just specifying the base? 05:51:51 Well, yes... 05:52:17 I'm being dense ATM. 05:52:21 I should go to bed soon, myself. 05:52:54 pikhq: Okay, I'll just tell you. 05:52:59 DEADBEEF_{16} 05:53:03 Has it clicked yet? 05:53:19 Grraaaw. 05:53:21 Yes. 05:53:36 a[n] = array indexing = a_{n} 05:53:41 foo_{base} = mathematical notation = a[n]! 05:53:43 :D 05:53:54 I got it 05:54:07 Wareya: you are a clever person, you win 05:54:09 not at something 05:54:12 you just 05:54:12 win! 05:54:16 Jumping from math notation to programming notation and back hurts. 05:54:20 I understand that almost 05:54:23 but I get something else 05:54:38 -!- alise has set topic: totally 0 days since last anyone sighting. 'part from hcf, 2583 and a bit days. http://tunes.org/~nef/logs/esoteric/?C=M;O=D. 05:54:43 yoyoyoyo sleep 05:54:44 I'll adress memory character 0xF00(16) instead of 0xF00[16] 05:54:46 seeya tomorrow bitchnizzles 05:54:48 night 05:55:00 (q[n])[y]use value of size n at address q as an address for a value size y -- I need a better way to do this 05:55:15 q(n)(y) 05:55:20 q[n][m]array with segments the size of n with the "origin" data value being at address q - with big endian, again. 05:55:24 q(n)[m] 05:55:42 clearly it should be 16[DEADBEEF] 05:56:03 or actually 05:56:07 q 05:56:41 no wait those are my direction commands 05:56:46 I guess I'll change those 05:57:20 fuck 05:57:25 I ran out of closing characters 05:57:36 I'm using all of ({[< for other things already 05:57:54 "' too 05:58:03 -!- zzo38 has joined. 05:58:09 hi 06:01:05 oh, you can't use {} in the middle fo expressions or calls 06:01:47 awesome 06:02:19 I have other idea for esolang based on the C-preprocessor, after it unquote strings it will run it through the preprocessor again, and then it will continue over and over again...... 06:02:35 until there's nothing left? 06:03:48 Yes, I guess so. 06:06:57 -!- coppro has joined. 06:21:27 * Sgeo misread alise as ais523 at least twice in the scrollup 06:21:45 Oh, erm, e's not awake. Hope e has pings silenced 06:21:50 Or isn't at the computer 06:32:32 -!- sebbu2 has joined. 06:35:39 -!- sebbu has quit (Ping timeout: 252 seconds). 06:43:11 ais523 does not appear to be connected 06:48:12 That has what, exactly, to do with confusing anyone, or pinging al!se? 06:48:26 No. 06:48:30 Sorry, didn't mean to get snippy 06:48:41 That's OK. 07:26:18 v 07:26:39 hey, you're right, it's the weekend again, neat 07:26:47 * coppro is still a little charged with Olympic fever 07:26:54 erm, by v, I meant Night all 07:27:12 lol 07:27:16 hey alise! 07:27:18 Was copying/pasting to some channels 07:28:41 -!- Sgeo has quit (Quit: /Deframentation time. Good night). 07:29:06 -!- madbr has joined. 07:33:57 -!- sebbu has joined. 07:37:00 -!- sebbu2 has quit (Ping timeout: 265 seconds). 07:42:57 -!- zzo38 has quit (Remote host closed the connection). 07:47:35 -!- coppro has quit (Remote host closed the connection). 07:49:52 -!- coppro has joined. 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:01:04 -!- oerjan has quit (Quit: leaving). 08:04:08 -!- madbr has quit (Quit: Radiateur). 09:13:31 -!- sebbu has quit (Ping timeout: 256 seconds). 09:20:49 -!- oklopol has joined. 09:29:17 -!- sebbu has joined. 09:32:45 -!- kar8nga has joined. 10:01:00 -!- tombom has joined. 10:11:59 -!- MigoMipo has joined. 10:50:36 -!- kar8nga has quit (Remote host closed the connection). 10:55:27 -!- Pthing has joined. 11:00:00 -!- Asztal has quit (Ping timeout: 272 seconds). 11:25:23 -!- MizardX has quit (Quit: reboot). 11:31:16 -!- MizardX has joined. 11:36:17 -!- lieuwe has joined. 11:36:51 -!- lieuwe has quit (Client Quit). 11:55:18 -!- kar8nga has joined. 12:40:30 -!- FireFly has joined. 13:02:31 -!- oklopol has quit (Quit: ( www.nnscript.com :: NoNameScript 4.2 :: www.regroup-esports.com )). 13:07:36 -!- tombom has quit (Quit: Leaving). 13:42:11 -!- MissPiggy has joined. 13:44:31 Whee, eBash results page seems to hang browser real good. 100% CPU usage, and it doesn't even react to killing its X connection (xkill). 13:53:50 -!- Gracenotes has quit (Remote host closed the connection). 13:57:02 -!- kar8nga has quit (Remote host closed the connection). 14:01:13 -!- Pthing has quit (Remote host closed the connection). 14:07:52 hi 14:11:29 * alise decides he wants ℵ_0 as a value in his language, just because it's cool. 14:11:49 hi 14:12:35 * alise also decides to use ⟨a,b⟩ as his tuple (or list?) syntax; he is well and truly off the deep end now. 14:13:08 and I like it 14:13:11 I lik that! except remove the commas 14:13:17 why? 14:13:18 ⟨a b c d e⟩ 14:13:22 ^ SEX ON WHEELS 14:13:50 ⟨Foo "goatee", Bar "emasculate"⟩ 14:14:06 is far too common to make uglier as ⟨(Foo "goatee") (Bar "emasculate")⟩ 14:14:30 (and more confusing; is that ⟨( or (( or ⟨⟨ or (⟨?) 14:14:43 they look more different in latex at bigger sizes, yes, but still 14:18:13 hmm 14:19:08 (S : a -> a) seems too relaxed 14:19:21 (s : s -> s) 14:19:31 because it simply means that whatever rules you add to S, the only restriction is that they take a value of one type and return the same 14:19:41 but (a -> a) is "anything to anything" 14:19:44 which simply isn't true 14:22:47 -!- oklopol has joined. 14:24:56 MissPiggy: is set Z = {n:N, -(n:N)} a good "theoretical" definition, do you think? 14:25:18 i.e. the set Z contains values of type N, and -(a value of type N). 14:25:20 what context 14:25:28 i would never read a log 14:25:33 a proglang I'm inventing that's pretty unique for once 14:25:39 term rewriting, just so you hate it :) 14:25:43 but typed term rewriting 14:25:46 guess what i'm doing 14:25:48 it's pretty smexy 14:25:49 guess! 14:25:52 logreading 14:25:55 well i do love smex 14:25:56 nope. 14:26:11 smexing? 14:26:17 oh definitely not 14:26:45 let's just say i hate parsing 14:26:56 alise, in set theory N u {0} u -N works, but in type theory seems better to use binary numbers 14:26:59 i should learn to use some parsing tool 14:27:02 preferably a human 14:27:05 who can read my mind 14:27:13 alise just in terms of getting good algorithms 14:27:15 MissPiggy: you mean to define N or Z? 14:27:23 Z 14:27:23 Z 14:27:31 right, well, this is part of my grand plan to have "semantic definitions" and "runtime definitions" 14:27:54 i.e., you define a really mathematically pure N + operations, and then a gnarly, perhaps even unsafe set of N definition + operations; maybe even in C or whatever 14:28:03 the former holds for all compile-time reasoning, and the latter holds at runtime 14:28:15 of course, having them be equivalent is... not really enforceable 14:28:33 everything is doable if you're drunk enough 14:28:37 but term rewriting is so pie-in-the-sky as far as performance goes that having pure-but-inefficient definitions doesn't *really* matter :) 14:28:44 really?? 14:28:52 really what? 14:28:59 well i know you have some ideas for making it faster 14:29:05 all I know is the really dumbtarded algorithm :) 14:29:44 did you know term rewriting rhymes with sperm rewriting 14:30:09 could someone please write this parser for me 14:30:32 * alise tries to tell texmacs "center this text block but have the text left-aligned" 14:30:46 it's like explaining math to a monkey 14:32:09 oh wait 14:32:14 i just realized this is trivial to parse 14:32:24 apparently the guy who made this language is a genius 14:33:12 what lang 14:33:17 clü 14:33:23 also you're CODING?! 14:33:45 yes! 14:34:02 i even like some of it, unfortunately i'm too tired to do anything complicated enough that i'd enjoy it. 14:34:17 hmm maybe i should have my fundamental definition of Q be the Stern-Brocot tree 14:34:25 otherwise i have 1/2 and 2/4 14:34:44 I guess a/b aka \frac{a}{b} should be : R -> R -> Q 14:35:20 and you could use the john gabriel tree for the definition of R 14:35:43 R -> R -> Q? 14:36:19 you're a mathman. 14:38:38 * oklopol watches alise turn in her grave as he writes a separate tokenizer 14:39:28 at least you used to consider that a sin, methinks 14:39:42 at least unless you're writing your parser manually 14:46:03 oklopol: i'm so much of a mathman that the preferred representation for the language actually has them in blackboard bold 14:47:14 i'm just wondering about the types 14:47:41 you do know R is closed under division (well almost)? 14:47:48 well umm 14:48:00 that's not actually what we need here 14:48:16 but clearly for all elements division by them is a surjection 14:48:26 to R 14:48:44 wait wait wait 14:48:48 are we talking about this 14:48:48 http://knol.google.com/k/john-gabriel/are-real-numbers-uncountable/nz742dpkhqbi/10# 14:48:50 john gabriel 14:49:00 yeah he's my idol 14:49:08 he's one total dude 14:49:34 yeah, if you use R in your programs 14:49:39 you'll get an approximation by default 14:49:55 unless you want to sacrifice equality checking, I guess 14:50:01 could you answer: did you suggest R -> R -> Q as the type of division 14:50:13 no, as one type of division 14:50:22 specifically, what you'd use to construct Qs 14:50:31 given that the internal constructor wouldn't be exposed 14:50:53 you could just contruct the Q from one R 14:51:34 well unless R's play some sorta special role 14:51:51 like 5 :: R and shit 14:52:05 why just one R? 14:52:17 obviously I'm going for human-happiness here, and \frac{1}{2} should, you know, work 14:52:29 it's not the internal constructor, that's the Stern-Brocot tree 14:52:34 just the thing that, you know, humans actually use 14:52:45 i'm just wondering why not N -> N -> Q 14:53:32 -!- Pthing has joined. 14:54:22 oklopol: err of course 14:54:25 i'm pretty fucking stupid 14:54:32 was thinking of R -> R -> C :-) 14:55:16 oh i see 14:55:24 i have just woken up and all 14:55:51 the natural field extension i presume 14:56:00 the natural extension of your mom, inded 14:56:02 *indeed 14:56:26 actually the way I was thinking of having C a subset of R was 14:56:37 are you implyinh my mom is the splitting field of her own legs 14:56:40 inert i 14:56:41 *implying 14:56:51 set C = {(a:R) + (b:R) i} 14:56:52 then 14:57:03 0 : C 14:57:09 0 = 0 + 0 i 14:57:21 and then 14:57:23 C a subset of R? 14:57:27 S : ...hmm, wait 14:57:29 oklopol: er, superset 14:57:34 I was thinking, just like define 0 and S on it 14:57:43 but that isn't really enough for the compiler to believe it's a true superset 14:58:05 anyway take a break and admire my beautiful rich syntax: 14:58:13 http://dl.dropbox.com/u/2164436/booleans-and-naturals.pdf 14:58:14 there's such a natural embedding of R to C that most people don't even know it's an embedding 14:59:42 In most functional languages, youfd expect S : a ¨ a to mean that S takes a value of any type, 14:59:42 and returns a value of that same type 14:59:57 yeees? 15:00:03 wait a mo 15:00:15 term rewriting, so terms are arbitrarily extensible 15:00:22 and...things 15:00:36 blergh, hard to put this into words 15:00:43 functional programming plus symbolic computation by the same mechanism, fuck yeah 15:00:45 oklopol: do go on :P 15:00:48 maybe i'll just say nothing 15:00:55 no please do 15:01:21 well err 15:01:50 I don't really LIKE term rewriting 15:02:18 basically S : a -> a just doesn't mean the same thing as in say haskell, but instead that "for each type a there is something, also called S, that has this type signature for the type a" 15:02:19 what I LIKE is giving an equational theory, and then having the compiler design an algorithm which decides equality on that 15:02:27 or maybe it decides unification on it 15:02:35 stuff like that you could use really well 15:02:51 basically that's really saying nothing 15:03:27 S : a -> a in things like haskell means that S is one function, that takes values that walk like a's and uses them all the same way 15:03:45 no that isn't what it says 15:03:55 because, for example 15:03:58 S "a monkey" will fail 15:04:04 because there's no S : String -> String 15:04:15 S : a -> a is merely a *constraint* on what types you can endow S with 15:04:20 well right 15:04:22 that is, they must be of the form a -> a 15:04:36 that way, you can use S in other parts of the program on variables, as long as you obey the rull 15:04:38 *rule 15:04:44 plus2 x = S S x 15:04:49 plus2 : a -> a 15:04:57 i just meant it's not the same thing as it is in haskell, but yeah i guess thinking about it in terms of rewriting makes it natural. 15:05:01 defining S : b -> b gives us plus2 : b -> b too 15:05:09 and yes, it isn't 15:05:13 that's why I explained the difference. :P 15:05:25 and that's why i said maybe i should say nothing 15:05:26 :D 15:06:41 so what exactly is this thing 15:08:27 oklopol: well it's a term rewriting language like Q and Pure, it's purely functional and lazy, so you have lazy symbolic computation _and_ lazy functional computation by the same mechanism, 15:08:32 and it's typed. 15:08:49 do you get what I mean about equational theories 15:08:55 not really 15:09:05 if you specify like 15:09:16 (a [] b) [] c = a [] (b [] c) 15:09:27 it should work both ways 15:09:36 infact you shouldn't care which way around it's written 15:09:37 two-way rewriting 15:09:40 the two things are identical 15:09:57 right 15:10:03 that's the same thing as 15:10:09 the fact that (a [] b) [] c --> a [] (b [] c) normalizes terms in this theory is just a coincidence 15:10:11 (a [] b) [] c = internal3 a b c 15:10:16 a [] (b [] c) = internal3 a b c 15:10:44 with rewriting you say the two things are equal, but one-way rewriting also says "...but the one on the right is the more natural form" 15:11:10 yeah you could say it's normalization 15:12:10 what i'd want is a two-way rewrite system, and a nice system for adding your own heuristics 15:12:13 well if you don't execute it and just do properties and proofs and transformations 15:12:18 then one-way rewriting doesn't exist, it's all two-way 15:12:22 one-way is just a choice of how to evaluate it 15:13:00 the problem with specifying an equational theory is that it's usually undecidible 15:13:16 that's not a problem 15:13:20 the problem is it's slow 15:13:35 well okay 15:13:54 i suppose it is a problem, but (insert argument) 15:14:44 I guess it would be nice to be able to say S : Num a => a -> a 15:14:52 but what should Num be in this glorious rewriter? 15:17:42 * alise decides that what - gives in tex (is it just the minus symbol?) is the best thing for the operator hole 15:17:51 for ascii, dunno 15:18:02 i'm starting to care stunningly little about the ascii representation 15:20:31 -!- FireFly has quit (Quit: Leaving). 15:20:32 typeclasse are so suck 15:20:40 yeah 15:20:54 Maybe this is where I should introduce dependent types 15:20:57 im trying to prototype a CHR typeclass replacement but haskell doesn't have a decent CHR 15:21:23 S : {Num a} -> a -> a 15:21:34 where Num : Set -> amodulething 15:21:37 but ehh 15:21:43 I'm bobbing along fine without them atm 15:22:04 -!- FireFly has joined. 15:25:01 -!- tcsavage has joined. 15:29:30 MissPiggy: is big-{ containing (foo when condition\nbar otherwise) a good notation for guards, do you think? 15:29:37 or should it be part of each definition like pattern matching 15:30:12 big-{ means you have to do space alignment in ascii form which is lame 15:49:07 -!- tcsavage has quit (Quit: Leaving). 15:57:21 alise you should make a wiki 15:58:20 for this lang? 15:58:29 for everything 15:58:46 yeah the alise wiki, where people can do your projects 15:58:54 MissPiggy: why 15:59:03 i answered that already 15:59:59 not a good answer tho :P 16:00:52 well EXCUSE ME for being completely useless 16:01:02 And it should be a Hackiki wiki. 16:01:07 :P 16:01:36 how do you pronounce "hackiki", the way i do it sounds like some sorta exotic animal 16:01:46 or like an african melon-hunting tribe 16:01:53 Hack-ee-kee 16:02:05 latexwiki would be fun 16:02:12 not just latex blocks 16:02:13 the whole thing is latex 16:02:18 we just spotted some wild hakiki in the forest 16:02:44 LatexWiki - the free latex fetish encyclopedia 16:02:45 The LatexWiki is a free latex fetish encyclopedia that anyone can edit, an online resource for latex fetishists, rubberists and rainwear lovers! ... 16:02:45 >_< 16:02:47 Gregor: emphasis on which syllable? 16:02:53 hmm 16:02:56 oklopol: The first kee 16:02:57 not sure there are choices really 16:03:01 yeah 16:04:56 ugh, the ascii representation is so boring 16:06:50 Fortress and Q and Pure are just so cool 16:11:34 * alise decides that the unmatching [/) interval syntax is barfworthy. 16:15:42 how about [0, 1[ ;) 16:16:09 aieeeeeeeeeeeeeee 16:16:13 maybe "[5, 7] right exclusive and left inclusive" 16:16:48 ouch 16:16:48 i should check out one of those languages 16:16:57 (if they're hip and cool) 16:17:03 check out all three. (pure is q's successor) 16:17:28 * alise ponders having T^n = <(T,)*n> 16:17:29 once i finish this parser 16:17:37 i.e. R^3 = 3d coordinate, 16:18:10 R_{2^{64}}^3 = 3d coordinate using 64-bit reals (prolly floating point) 16:18:36 in general you'll want A^B to be a function from B to A, just if B is a natural, you convert it to a set of that cardinality 16:18:55 why would a^b be a function from b to a? 16:19:01 I have -> for that 16:19:40 how dare you question how mathematics usually defines it 16:20:20 also what's up with hcf nowadays 16:21:55 totally dead man 16:21:58 _[_] : Array_(d,a) -> N_d -> a 16:22:05 the ascii form of this language is somewhat ugly 16:23:11 erm, *N^d 16:23:19 I like that 16:23:23 hmm 16:23:30 why does it take an array of indices? 16:23:35 tuple 16:23:42 because array is N dimensional 16:23:47 for a 2d array it'd be 16:23:47 ahh 16:24:00 of Rs, say: 16:24:03 i thought you mean N_d as in integers mod d 16:24:10 right right _ was a mistake 16:24:11 ^ i meant 16:24:12 in which case it would've been like a finite array 16:24:14 _[_] : Array_(2,R) -> N^2 -> a 16:24:25 *-> R 16:24:30 err, yes XD 16:24:44 anyway without that syntax for constructing tuple types you couldn't even write that function! 16:24:45 so I like it 16:25:10 oklopol: also I'm considering using N_d = integers-mod-d to do fixed-size ints 16:25:19 after all, N_(2^n) is an n-bit natural 16:25:20 you totally should 16:25:21 in fact 16:25:25 also N is naturals not ints :P 16:25:38 so N_(2^n) = uintn and Z_(2^n) = intn 16:25:41 you should have X_u defined as X/uX in general 16:25:51 hmm 16:26:01 what would 100N mean? 16:26:05 i'm dense atm, forgive me 16:26:15 100 * n for n \in N 16:26:44 also, I need to use a_x for set arguments 16:26:51 like before, Array_(2,R) 16:28:05 then C = R[x]_(x^2+1) :P 16:28:12 although I guess Array 2 R would work, I can't think how to prettify that with LaTeX 16:28:15 oklopol: wat. 16:28:42 hmm 16:28:47 latex is not so good at juxtaposition 16:28:52 "Array d a" looks like Array da 16:29:49 alise: basically you get all polynomials in R[x] that are of a smaller in degree than (x^2 + 1), so your elements are of the form ax + b 16:30:00 and x^2 + 1 = 0, so in fact x = i 16:30:22 i think you just took my language and force-fucked it into esotericness 16:30:22 i'm learning field theory atm, i hope it doesn't show. 16:30:28 i may sue you. 16:30:31 :D 16:31:38 * alise wonders whether to have a <> unit type 16:35:03 so 16:35:13 * alise can't figure out how to do ⟨⟩ in texmacs :( 16:35:14 tt : 1 16:35:18 or maybe not... 16:35:23 MissPiggy: in my lang you mean? 16:35:38 1 isn't a set, but certainly tt : set-of 1 16:35:39 since ff, tt : 2 work 16:35:48 wut 16:38:19 wut 16:38:22 wuuuuuuuuuut 16:42:18 you know, I don't think 1-tuples make any sense 16:42:28 so should a^1 = a?? 16:42:38 if so, then having a^0 be <> seems inconsistent, if ^1 is the "base" 16:44:00 in math we usually identify (a,(b,c)) and ((a,b),c) 16:44:20 like completly implicitly, there's probably generations of people that haven't even thought about it 16:44:29 same with (a) and a 16:44:50 I don'tsee a problem wth a^0 as unit 16:44:54 since you might define 16:44:57 a^0 = () 16:45:06 a^(1+n) = a * a^n 16:45:07 but 16:45:10 a^0 = a 16:45:12 erm 16:45:13 a^0 = <> 16:45:15 a^1 = a 16:45:17 a^2 = 16:45:19 a^3 = 16:45:21 see the "gap"? 16:45:23 that's weird 16:45:53 no 16:46:00 a^1 = <> * a = 16:47:12 But does make sense? 16:47:14 It is, semantically, a. 16:47:27 And I think it's a rather pointless type to have. 16:47:59 Anyway, <> looks ugly, syntactically. :P I think I want a separate unit type... 16:53:18 identification of things is a complex subject, says SICP 17:03:07 Have you read your SICP today? 17:03:50 well 17:03:51 no 17:03:57 i'm sorry 17:10:00 MissPiggy: so do you think <,c> should = ? 17:10:13 if a^n = a * a^(n-1) 17:10:13 -!- Sgeo has joined. 17:11:19 alise not sure, it's a lot different in programming 17:11:26 than on paper 17:11:39 tupelem : a^n -> N_n -> a 17:11:54 alise, taking any pictures this weekend? 17:12:05 Ah! 17:12:13 I will do that tomorrow; it completely crossed my mind on Friday. 17:12:17 Erm, completely didn't. 17:12:18 Cross. 17:12:27 Remind me. :P 17:12:44 (but a legal investigation seems more likely than moving at the moment0 17:14:30 *) 17:14:54 Why was this so useless?: http://i.imgur.com/ClzRm.png 17:15:21 Although actually, some stuff does seem faster now 17:15:21 You did stuff while fragmenting. 17:15:22 Don't. 17:15:24 *defragmenting 17:15:26 Sgeo: placebo 17:15:41 Hm 17:16:08 If stuff is accessing stuff, it can't move that stuff. 17:16:19 So close everything, run the defragmentation, and go for a walk. 17:16:22 Or just keep it fragmented. 17:16:29 I tried to let it run overnight 17:16:37 When I woke up is when I started doing stuff 17:16:38 Then I dunno. 17:16:45 [although I did leave my browser open on one page] 17:16:53 That wouldn't have such a dramatic effect. 17:17:20 And "doing stuff" when I woke up [and it was still going] came down to visiting a few pages 17:19:41 that's one naughty pic 17:20:27 Sgeo: if you touch the HD *too* much, defragmenter restarts 17:20:29 but if it's done it's done 17:20:31 so... dunno 17:21:03 When I started touching stuff, it said something like, 30%, Compressing files 17:21:10 Don't know if that counts as a restart 17:23:07 don't think so 17:27:40 I'll try again tonight, I guess 17:28:36 hmm 17:28:44 if you have {1,2,...} and {0,1,2...} what should you name them? 17:28:51 if you have just one obviously N is the right name 17:29:48 -!- MissPiggy has quit (Quit: Changing server). 17:30:16 N* is used for "N without 0" in at least two contexts 17:30:21 (that's not one of them tho) 17:30:33 -!- MissPiggy has joined. 17:30:44 oklopol: :D 17:30:58 errrrrrr 17:31:06 s/N/X/ :) 17:31:19 what's N_+ 17:31:24 i could look it up 17:31:26 but poop! 17:31:49 Z_+ and Z_- are used for... i don't know if the zeroes are there actually 17:32:05 N_+ i haven't seen 17:33:25 maybe Z_+ then 17:33:33 don't remember 17:33:57 that would make sense, but shuold check if 0 is usually there 17:34:24 oklopol: apparently N* is in fact used to mean N without 0 17:34:28 for the naturalz 17:34:32 ah, cool 17:35:09 wasn't one of the two i knew, didn't actually know it isn't used for it 17:36:15 it's just one of the meanings i know "makes sense" for N, and N* = {1} 17:36:26 oh wait... 17:36:33 so what kind of * is it, I wonder 17:36:36 since when is N a ring :P 17:36:53 my head is out shopping today 17:39:58 (c=>x; d=>y; e=>z; otherwise) is a nice conditional syntax 17:40:25 i keep almost speaking finnish here 17:40:35 head hurts again 17:40:39 i think i'm dying or something 17:41:02 it hurts almost every week 17:41:10 see a dawktore 17:41:16 yeah right 17:41:23 thought not 17:41:27 :D 17:41:29 well i might 17:41:37 or maybe not 17:41:39 dunno 17:45:10 _\circ is a rather nice hole char for multifix 17:46:07 what's \circ? 17:47:18 circle thingy. 17:47:29 you know, like a big big . filling a whole letterspace, but hollow. 17:47:31 a circle. 17:48:06 oh i see 17:48:11 makes sense 17:48:55 they're subscripted so as not to clash with the operator text 17:49:03 and you can think of specifying an argument as "filling the circle in" 17:49:46 http://dl.dropbox.com/u/2164436/if-then-else.pdf 17:49:46 dig it. 17:50:47 PDF WARNING!!!!! 17:51:06 I always think of \top and \bot as sets though.. 17:51:12 tt and ff as values 17:51:18 pdf warning my arse 17:51:19 looks weird but idk 17:51:27 nothing wrong with pdfs 17:51:30 I know :( 17:51:37 are you using adobe reader or sth? :p 17:51:47 you might be right about \top and \bot 17:51:49 im just complaining about how stupid reddit is 17:51:51 they aren't sitting well with me, either 17:51:53 ah ok 17:52:08 I'd be more coolie about tt and ff if they, say, had a fancy ligature 17:52:16 it's gotta be in unicode, right? 17:52:16 ehehe 17:52:26 don't overuse unicode 17:52:32 MissPiggy: of course if i'm using names i could just call them, you know, true and false 17:52:41 they letters on the keyboard are the easiest ones to type 17:52:47 also, the main syntax for this language is two-dimensional using things like blackboard bold 17:53:01 of _course_ it needs a specialised editor (or just use the ascii->that converter) 17:53:26 you shouldn't have to be writing a research paper to get beautiful code ;) 17:53:28 *:) 17:54:02 * alise wonders how to represent _\circ in the ascii form 17:54:08 maybe if()then()else() 17:54:28 MissPiggy: any reason to use tt/ff over true/false? 17:55:06 or just 0/1 :P 17:56:00 shorter 17:56:02 I:) 17:56:08 wut 17:56:10 ah 17:56:10 true and false are probaly best 17:56:32 yeah except "if true then" "if false then", you know, sorta good to keep the ambiguity between names and inert values down :P 17:56:54 why do you want something as horrible as if-then-else- ? 17:57:09 bool : a -> a -> B -> a 17:57:13 yeah you horriblophiliac 17:57:14 ^ is better 17:57:20 MissPiggy: not for imperative code 17:57:30 imperative doesn't exist 17:57:32 and not for if x then let ... in ... else ... 17:58:03 "No identifier may be identical to another identifier used in the program to denote something else, or include such an identifier as a substring. 17:58:35 "Note particularly that, in the case of one identifier being a substring of another, only the longer identifier shall be considered erroneous. 17:59:05 "The constants for true and false are t and f respectively." 17:59:06 haha 17:59:13 okay double haha 17:59:21 oh wait just one 17:59:28 coppro: C++0x, I presume! 17:59:36 alise: :P 17:59:44 I just made that up and thought it would be amusing to share 18:00:02 It should become a language 18:00:06 coppro: i's hucking brillian 18:00:09 Filled with absurdities like that 18:00:24 it should be called javascript 18:04:33 dependent types + tuples with names for their args = module system methinks 18:05:59 Functor : * -> * -> * 18:06:09 Functor f a = b) -> f a -> f b> 18:06:10 right? 18:06:16 then you'd do 18:06:53 Functor_List : Functor List 18:07:19 Functor_List a = 18:33:54 -!- Asztal has joined. 18:49:15 -!- coppro has quit (Remote host closed the connection). 18:49:27 so. i just debugged my code for like 20 minutes because i'd written my fibonacci program with just one base case. 18:49:44 in any case, clue parser parsed its first baby 18:49:47 \o/ 18:54:38 -!- SimonRC has quit (Ping timeout: 265 seconds). 18:58:33 oklopol: is that the guessing clue thing 18:58:33 omg 18:58:34 omg 18:58:37 have my babies, the clue babies 18:59:23 yeah it's the guessing thing 18:59:29 and it's cooooool 19:04:29 -!- SimonRC has joined. 19:05:54 * alise is writing a tree-rewriting tarpit to get the feel of it first 19:05:55 fn A E X = (A = X) : E 19:05:57 I wish that worked 19:06:15 but it doesn't, because the rule A = X is just ASIDUASD = X, i.e. you can rewrite anything at all to X 19:06:25 I need a quote/unquote thingy to do that :P 19:06:31 (rule : E is e-with-rule) 19:06:52 (so "+ X Y = ..." called is like (X = val) : (Y = val) : ...) 19:14:34 i really want reversible parsers 19:14:49 i want to just be able to write a syntax and have it think of data structures automatically and write a->String and String->a 19:17:20 you know what? 19:17:24 i'm gonna fuckin' write it 19:17:26 uhh wait 19:17:27 one thing first 19:17:37 oklopol: ask the little copy of oerjan in your mind if it's possible 19:25:47 i only use my copy of oerjan for good 19:26:07 oklopol: hey this is good 19:26:12 you don't have to write pretty-printers ever again! 19:26:31 2parse or not 2parse, that is the question! 19:27:51 haha man, conor mcbride is like 19:27:53 a copy of me 19:27:57 do you think i should make a syntax for the functional language to which clues are compiled 19:27:58 i mean 19:28:01 he's more intelligenterer but he has like 19:28:05 exactly the same programming language interests as me 19:28:06 oh shit water boils 19:28:13 IT DOES 19:28:19 oklopol: also yes 19:28:24 make it the inverse lambda calculus 19:28:54 lambda calculus puts values in names, then uses those names in a new value 19:29:11 inverse lambda calculus looks up names for values, then extracts those names from a value 19:29:14 make it now 19:30:45 I need a graph lambda calculus 19:31:03 hmm, it would definitely be cool to see what kind of algorithms this thing generates 19:31:30 i was just thinking it'd be weird, in some sense, to have a functional language you can see, but can't actually write 19:31:33 but maybe it's not 19:32:53 oklopol: i presume you're not talking about the inverse lambda calculus :) 19:33:29 so in lc (\x.y)z puts z in x, then uses x in y; so in inverse lc we have to get x from z, then extract the x from y 19:33:42 not sure what the result of the extraction is, though 19:34:35 so, really, LC is (name=arg) in body 19:34:56 basically in LC what we work with are values, and names are just helpers 19:34:59 i was thinking something like a haskell syntax 19:35:05 in inverse LC we only have values so we can find names 19:35:20 the question is, how do we get a name from a value? 19:38:41 ok, so my parser combinator library will be based on applicative functors 19:39:12 with most parser libraries all you need is syntaxbits -> ast 19:39:20 like varname,funcbody -> ast 19:39:30 but in this we need ast -> varname,funcbody as well 19:39:42 so, maybe we can derive that. 19:40:19 if you ignore a parsed bit, you have to specify a default value for it so it can use it when deparsing 19:42:05 okay these now parse and compile: http://www.vjn.fi/pb/p351446645.txt 19:42:21 syntax complaints? 19:42:22 i think that this is sexy. 19:42:26 wow lol 19:42:36 oklopol: well one i'd add more unicode, i take it _that_ won't be accepted 19:42:39 why is there two :.'s ? 19:42:49 in foo ~ ; baz; quux i'd use commas, not semicolons 19:42:51 MissPiggy: two different examples 19:42:57 not actually very useful for this simple things 19:43:12 what 19:43:18 in fib there is :. twice 19:43:18 why 19:43:27 MissPiggy: clue :: [(input,output)] -> (input -> output) 19:43:30 i just gave it two examples. 19:43:32 well, + some hints 19:43:36 fib ~ {:. 8 -> 21 19:43:36 : 6 -> 8 19:43:37 : 7 -> 13 19:43:37 :. 7 -> 13 19:43:37 : 5 -> 5 19:43:39 : 6 -> 8} 19:43:42 why is :. there twice?? 19:43:43 yeah so 19:43:59 well, it's because i gave it two examples :P 19:43:59 but 19:44:00 it looks like 6 examples in two groups, what are the groups? 19:44:05 no 19:44:16 -!- cheater3 has joined. 19:44:18 two examples, it's just you don't separate them. 19:44:20 UR LANGAUGE IS TOO HARD 19:44:38 do you complain about that, i'm not sure why i decided to do it like that, maybe just to be weird 19:44:52 how is that not 6 examples? 19:44:55 basically that's (:. stuff : stuff : stuff), (:. stuff : stuff : stuff) 19:44:59 well because 19:45:01 I thought an example was an input output pair 19:45:01 i'm confused 19:45:07 the ":"'s are subexamples 19:45:11 for the :.'s before them 19:45:12 -!- cheater2 has quit (Ping timeout: 258 seconds). 19:45:13 what is a sub example? 19:45:17 what's :. 19:45:18 presumably it's two calls 19:45:21 reducing fib downwards 19:45:28 what the recursive calls should return 19:45:35 and what their inputs should be 19:45:36 thought so :D 19:45:41 yarr 19:45:47 80-1 = 7 19:45:50 8-2 = 6 19:45:53 so you have 8 6 7 on the LHS 19:45:57 *8-1 19:46:00 to show how the recursive call goes 19:46:09 -!- kar8nga has joined. 19:46:09 7->13, biggy so you know, show how dat be done 19:46:22 :. IOP : IOP1 : ... : IOPn means find code for IOP, use all of IOPi's when deriving output value 19:46:30 otherwise, clue wouldn't know when to recurse downwards 19:46:34 it'd just have a shitload of numbers 19:46:42 and oklopol isn't quite clever enough to reverse that :) 19:46:58 -!- Pthing has quit (Remote host closed the connection). 19:47:08 and yeah i think you're getting it right 19:47:18 especially the not clever enough part 19:47:20 oklopol wuuuuuuuuuut 19:47:35 MissPiggy: okay. let's look at this 19:47:40 fib ~ {:. 8 -> 21 19:47:41 : 6 -> 8 19:47:41 : 7 -> 13 19:47:44 fib(8) = 21 19:47:45 http://www.vjn.fi/pb/p351446645.txt 19:47:48 fib(8) = fib(6) + fib(7) 19:47:52 so, we show that 21 is the result 19:47:53 excuse me?? 19:47:58 and then show it descending into fib(6) and fib(7) 19:48:08 8+13 = 21, so 8 -> 21 shows how you add the two recursions 19:48:09 oh I see!!!!!!! 19:48:12 then we start a new example, for 7 -> 13 19:48:14 I understnad CLUE!!!!!!!! 19:48:20 and ANCHOVIES!!!! 19:48:25 this makes sense 19:48:28 when you have 19:48:54 :. a -> b : a'_i -> b'_i 19:49:19 it means that f(a) = b = G(f(a_0),f(a_1),...) 19:49:22 MissPiggy: ":. 8 -> 21 : 6 -> 8 : 7 -> 13" says find a way to get 21 from the input 8, and the outputs 8 and 13. also find a way to find the subinputs 6 and 7 from the main input 8 19:49:27 where G is the recursive case it's solving for 19:49:37 these are the things you always do with recursion 19:50:08 do something to get input for the recursive cases (6 and 7), then use their output (and your original input maybe) to find the final output 19:50:27 so, my suggestions: 19:50:33 in the hint line, make the operator something other than ~ 19:50:46 make the separator , not ; 19:51:08 I thought it was just 19:51:13 also, don't have multiple blocks in ~ like that, either separate every call (excluding subcalls ofc) into its own block 19:51:15 or have one big block 19:51:17 those are my suggestions 19:51:27 [(input,ouput)] -> (input -> output) 19:51:29 but it's actually 19:51:49 [((input,output), [(input, output)])] -> (input -> output) 19:52:11 so about putting this thing on esolang, we need (the first?) disambiguation page right? i have no idea how to use the wiki really. also is it okay to put closed source up there, i really don't want to publish this code yet. 19:52:17 MissPiggy: you forgot -> [hint] 19:52:20 and each ((mi,mo),(si,so)) :: ((input,output), [(input, output)]) 19:52:23 oops 19:52:38 and each ((mi,mo),(si_j,so_j)) :: ((input,output), [(input, output)]) 19:52:40 oklopol: if there's no code you can post a binary, but I'll lynch you 19:52:45 because there is an obvious massive abstraction i can do, but it requires a tiny bit of thinking, which i can't do right no 19:52:45 w 19:52:49 where j rangers over n different subproblems 19:52:50 IMO publishing just a spec beats publishing a binary with no source 19:53:08 and the subproblems are used to explain the recursion structure 19:53:12 yeah and there's hints too 19:53:24 it's like publishing a press release saying "we're finalising a paper that shows that monkeys are real" vs "Monkeys are real. Here is how to work it out given the data: ... We will not show our data." 19:53:33 the former is fine, the second isn't 19:54:04 basically just the conversions multiple examples <-> one example with at each actual value a vector of values in the corresponding places in the different examples 19:54:25 so, it's really tiny 19:54:27 ocluepol, I guess that is how this works without being type directed 19:54:41 seems :P less magic now 19:54:46 but still amazing 19:55:24 -!- kivod has joined. 19:55:49 what if you don't have subproblems is it just impossible? 19:55:51 oklopol: so basically you just have a bunch of, basically tables for operations like add, subtract, multiply 19:55:56 and you just look things up in there 19:56:03 MissPiggy: maybe not with hints 19:56:12 i don't get what his hints do though :) 19:56:53 is this a chan about esotericism or programming? 19:56:57 yes 19:57:11 esotericism programming and esoteric programming 19:57:18 Esoteric programming. 19:57:20 esotericism programming! iching(1) 19:57:24 * Sgeo goes off to program some ghosts. 19:57:26 and itching 19:57:31 and gay sex 19:57:35 mostly gay sex actually 19:57:41 enigmatic gay itching? 19:57:47 Very. 19:57:57 kivod: now the question we have, which one did you *want* 19:58:00 *have is 19:58:21 oklotype I will help code a type directed version if you want 19:58:40 lol 19:58:45 although you werobefubef 19:58:49 kivod: you wanted lol? 19:58:53 I was searchning for a chan about esotericism 19:59:01 but I like programming too so ... 19:59:02 kivod, I'm into esotericism 19:59:13 ignore MissPiggy, the rest of us aren't crazy! 19:59:15 secret of the cube and stuff 19:59:20 ...apart from oklopol 19:59:28 although oklopol probably has some deep oklo musing about the secret of the cube. 19:59:55 so, now my question is, what's exactly esoteric programming? 20:00:24 "alise: also, don't have multiple blocks in ~ like that, either separate every call (excluding subcalls ofc) into its own block" <<< now i have block per one type of computation 20:00:35 Programming using an esoteric programming language. An esoteric programming language is a language designed to be exceptionally unusual, odd, or hard to use. 20:00:44 kivod: programming the computational equivalent of crack by monkeys on crack 20:00:50 The best-known examples are Brainfuck and INTERCAL. 20:00:57 in languages that crack your mind into a thousand million pieces and they all turn into monkeys. 20:01:02 pikhq: you are BORING 20:01:16 alise: I try. 20:01:17 sounds cool ^^ 20:01:23 IT ISN'T. It's horrific. 20:01:36 Turn back now, while you still have a chance!!!!! 20:01:40 * Sgeo wrote a thingy for use by programs written in esoteric languages 20:01:53 That thing, however, was idiotically designed [by me] and for all intents and purposes, dead 20:01:54 Ignore Sgeo, he's never quite gotten over the PSOX ordela. 20:01:56 *ordeal. 20:02:06 If he starts mumbling, just smile and say yes a lot. 20:02:08 MissPiggy: i think this is a cooler thing than using types, as an esolang, that is 20:02:13 lol 20:02:29 oklopol can you make any functions with it which aren't HM typeable? 20:02:29 oklopol: can you define your own tables for it to look up in? or does defining functions do that 20:03:25 HM typeable? 20:03:33 alise: humm? 20:03:38 look what up 20:03:42 hindley-milner typeadoo 20:03:45 ohh 20:03:55 oklopol: like it infers the operations by looking up your two operandyhoos values that it needs to infer an op from 20:04:03 from like various tables of the core operations like +, - etc 20:04:03 give an example that isn't HM typeable 20:04:05 right? 20:04:06 y? 20:04:11 y isn't hm typey yeah 20:04:18 well obviously you can write y 20:04:19 What's HM typable? 20:04:19 oklopol: so is defining a function adding your own table 20:04:21 or wait can you now 20:04:25 hindley-milner typeadoo 20:04:32 Should I assume that y == y combinator? 20:04:43 alise: what table? 20:04:48 do you mean 20:04:56 can you use your functions as helpers in other functions 20:05:10 like can you make a function that does something, using an append function you wrote 20:05:29 oklopol: yeah, without specifying it 20:05:41 i.e. does making new functions give it more rules with which to infer operations 20:06:09 umm, where did you get that it "infers" something? :P 20:06:17 i hope i didn't say yes to anything like that 20:06:22 it's just brute force search man 20:06:32 oh 20:06:34 isn't it like 20:06:38 this is very beta. 20:06:39 okay our two subcalls are 4 and 3 20:06:46 our main thing is 12 20:06:52 4+3 = 7 nope 20:06:54 4-3 = 1 nope 20:06:58 4*3 = 12 BINGOOOOOOOO 20:07:06 and we have like, addition, subtraction and multiplication table there 20:07:09 and we look up in each one 20:07:11 yeah it's like that, but you'd probably just give it * and not + or -. 20:07:15 recursively for the subcalls 20:07:18 oklopol: well how does it know 20:07:20 you didn't tell it 20:07:21 anyway 20:07:29 does making your own function f(x,y)=z add f as a table to that inferring process 20:07:31 if not SHIT SUX 20:07:47 ah, you give it the functions to use EXPLICITLY. 20:07:58 ... 20:08:02 so it isn't clever at all 20:08:04 :( 20:08:05 fib ~ ; dec; add 20:08:10 append ~ ; car; cdr; cons 20:08:13 how about not having them 20:08:20 and having it search the entire universe of currently-defined functions 20:08:31 oklopol I don't understand why you wouldn't want it type directed :( 20:08:41 perhaps if i write a sophisticated enough compiler 20:08:53 MissPiggy: oh i do, eventually 20:09:12 -!- Pthing has joined. 20:09:14 parse :: String -> Maybe Integer 20:09:15 parse "0" = Just 0 20:09:15 parse ('S':xs) = return (1 +) <*> parse xs 20:09:15 parse _ = Nothing 20:09:15 deparse :: Integer -> Maybe String 20:09:15 deparse 0 = Just "0" 20:09:17 deparse (n+1) = return ('S':) <*> deparse n 20:09:19 deparse _ = Nothing 20:09:21 conclusion 20:09:26 for trivial parsers, just swap LHS and RHS for parse/deparse 20:09:53 now to make it less trivial 20:09:59 MissPiggy: but really it's type directed already in the sense that if an operation fails, then its result is ignored. 20:10:02 oklopol, so right now, if you have hints {f,g,h} and you want to make a function from recursive subcalls {p,q} which equals the target value x 20:10:22 x = f(p,h(q,p,p),g(p)) might be a right answer, for example 20:10:33 is this roughly the kind of problem it tries to solve? 20:10:36 yep 20:10:46 how do you which arity each function is? 20:10:51 like h takes 3 parameters 20:11:10 primitives have arities, and your functions have the arities their clues do. 20:11:26 -!- kivod has left (?). 20:11:38 some primitives have types, and your functions will fail if used with an incorrect type, because the primitives they consist of will fail. 20:12:00 oh okay 20:12:03 "alise: so it isn't clever at all" <<< the compiler is not supposed to be clever, the language is. 20:12:06 well arity is the first sign of type :D 20:12:13 instead of being untyped it's typed like 20:12:15 oklopol: specifying ops != clever 20:12:17 * -> * -> * 20:12:30 rather than 20:12:34 Int -> String -> Int 20:12:38 or even 20:12:44 Int -> (String -> String) -> Int 20:12:51 does it do higher order programming? :P 20:14:07 MissPiggy: not atm, but it should 20:14:15 oklopol that sounds be really really hard though 20:14:23 later 20:14:37 no not relly. 20:14:38 *really 20:15:06 alise: yeah i don't care about your stupid opinion 20:15:13 and your mom is fat 20:15:15 :( 20:15:17 ow 20:15:22 take that 20:15:26 waaaah 20:15:31 you guys stop fighting!!!!!!!!! 20:15:35 anyway err 20:15:39 i was originally even thinking 20:15:44 you might make like append 20:15:47 by the higher order programming is hard 20:15:49 BY THE WAY 20:15:53 and then give some other function, as a helper, (append [1,2,3]) 20:16:01 curried that is 20:16:18 well sure "append [1,2,3]" denotes a function just as "append" does 20:16:19 hard in what sense? 20:16:19 anyway the problem is 20:16:22 I don't see any difference 20:16:28 you might be able to just write some sorta combinators, and program in helper lists 20:16:40 ^ the problem i was thinking it might have 20:16:46 oklopol, well for type directed higher order programming, you can do it algorithmically 20:16:50 without any examples or anything 20:17:00 but when you add recursive data types, it becomes very difficult 20:18:00 do what algorithmically 20:18:04 this whole thing? 20:18:22 how can you do example-oriented programming without examples 20:18:53 or do you mean just deducing functions from some general rules for how they should work 20:19:04 because that's bullshit 20:19:55 oklopol do you make your language output lisp and haskell? 20:20:23 you can inhabit (or show impossible) stuff like a -> (a -> b) -> b 20:20:26 without any examples 20:20:26 well no, not actually either of them 20:20:28 because it's not internally either 20:20:42 even as a functional language it's quite different 20:20:55 really? 20:20:56 inhabit? what the fuck does that help 20:21:10 that's what your language does I think 20:21:14 i wanna write a tetris with this, not a fucking logic wanking tool 20:21:22 you create functions from examples no? 20:21:28 sure, sure 20:21:39 LOL LOL LOL 20:22:20 "i wanna write a tetris with this, not a fucking logic wanking tool" -- oklopol on programming 20:22:31 i'm just saying the language is a bit different, so i was thinking haskell syntax, plus some additional syntax 20:22:36 Mmmm 20:22:37 Logic wanking 20:22:40 on programming with clue, yes 20:22:44 -!- coppro has joined. 20:22:58 i just mean you people seem to completely misunderstand the idea of the language 20:23:06 I do 20:23:21 I want to undersatnd it though] 20:23:28 it's not meant to be something pure and sexy, it's meant to be a cool hack around the fact example-based stuff is impossible to make work. 20:24:55 What I mean is 20:25:08 (1) higher order programming is going to be extremely difficult to solve 20:25:22 *Text.TwoParse> toVars $ toAST $ varsFor P_ X 20:25:22 Right X 20:25:22 i don't think it is! 20:25:23 it's a start 20:25:30 oh well I hope you are right :P 20:25:32 MissPiggy: oklopol's probably right, he can hack up anything 20:25:34 i mean 20:25:40 let's say you wanna write like map 20:26:14 you just give it an example of some list and something like an increment function, and show that it applies the function to first one, and recurses on the tail of the list, then conses 20:26:20 let me implement map f [] = [] ; map f [3,5,6,2] = [f 3,f 5,f 6,f 2] ? 20:26:22 then 20:26:32 if you change the function, it'll just apply it, like it did with increment. 20:26:43 oh 20:27:01 so map inc [] = [] ; map inc [3,5,6,2] = [4,6,7,3] 20:27:13 if there are problems, i can't see them. 20:27:21 * MissPiggy neither 20:27:44 this is going to be so sick 20:27:46 that thing i just explained would work right away, prolly, if i added like an append function, and made it possible to have functions as data 20:27:46 err 20:27:46 *added like an apply function 20:29:24 i can try to implement map, although it won't work currently (no fundamental reason it shouldn't, just some name lookup things i'd need to add) 20:29:29 *Text.TwoParse> toVars $ toAST $ varsFor S_ ('a','b') 20:29:29 Right (Right ('a','b')) 20:29:30 yay 20:30:52 okay done 20:31:57 http://www.vjn.fi/pb/p525542334.txt 20:31:59 i think that's it 20:32:13 oh... 20:32:21 okay there's a slight problem because i chose such a simple function 20:32:25 prolly wouldn't work 20:32:32 can you see why btw? 20:34:36 http://www.vjn.fi/pb/p536541641.txt 20:34:37 better 20:36:22 alise: the reason i chose "," over ";" was just so you could use "," in identifier names 20:36:46 like if you want a function called "do this, then do that" 20:38:37 i mean i do think it would be nicer to use ",", i just want to have absolute freedom in varnames. 20:38:53 and what do you suggest for "~", and what's wrong with it now? 20:39:20 as for the block thing, i've learned to love it already 20:39:31 well why can't you use ; in varnames 20:39:40 i guess you could 20:39:41 the block thing i suggested or how you already had it? 20:39:49 and ~ is fine, just not for the list of funcs 20:39:52 the one i have now, 20:39:54 *-, 20:39:55 I'd use / 20:39:58 hmm 20:39:58 like w/, with 20:40:02 well 20:40:10 map / ; cons; car; cdr 20:40:13 originally i think i had different chars for both 20:40:41 but there's sort of this esotheme going on that things that mean completely different things look similar 20:41:27 the other main thing is {:: a -> b }, although i guess it just looks like a completely separate thing now that i've implemented this 20:41:34 :: is the tests 20:41:46 it's actually probably not that useful, but no matter 20:42:49 i'll consider / 20:43:10 how about "USING THE FOLLOWING HELPER FUNCTINOS:" 20:43:15 *USES 20:45:49 here's how I'd write fib in http://www.vjn.fi/pb/p351446645.txt 20:47:23 -!- MizardX has quit (Ping timeout: 276 seconds). 20:47:33 -!- zzo38 has joined. 20:47:41 what do the <> mean in hints 20:47:48 base case? 20:47:49 yeah 20:48:01 ; deconstruct for recursion; combine 20:48:05 oh nooo 20:48:05 I was reading the "LoUIE" page. 20:48:10 <> is the condition function 20:48:25 you also explicitly tell it what to use to differentiate between cases 20:48:34 I said LoUIE LoUIE 20:48:49 well, not completely explicitly 20:49:03 like fib just needs id 20:49:24 base case 1 is always 0, base case 2 is always 1, so all others will go to the general case 20:49:56 I was looking at the "Paneer" part. Forth (and possibly other existing programming langauges) can do something like that (maybe bash shell-script can, but I'm not sure), but it doesn't what you want, necessary. Still, that's how the OASYS->TAVSYS converter works. The file "oasys.4th" defines a word "oas" which causes OASYS binary files to be treated as a source code for a TAVSYS file. 20:50:07 and in append, instead of empty you could also use length 20:50:45 I also looked at "Boo-yah!" and I want to think of what kind of states it can use. 20:51:27 oklopol: http://www.vjn.fi/pb/p123635515.txt 20:51:30 my masterful syntax 20:51:47 ..5/..6 in the second fib recursion thing should be .. 5/.. 6 20:52:28 What is that file? 20:53:16 i don't have a clue 20:53:42 alise: how does it know the 7 and 8 examples are the same? 20:54:30 the grouping is to show that 20:54:56 nothing else 20:56:24 I also had another idea of esolang: A program language that the operators for dealing with numbers includes things such as "count how many letters to write the word of this number in English", "count how many letters to write the word of this number in Latin", "remove all digits from the first number that match digits in the second number", and so on, like that. 20:57:25 oklopol: oh 20:57:29 oklopol: didn't realise 20:58:14 probably i didn't mention it 21:03:29 -!- coppro has quit (Ping timeout: 245 seconds). 21:04:33 fooS :: PP Foo 21:04:34 fooS = char 'x' *> give X_ () 21:04:34 <|> char 'p' *> give P_ fooS 21:04:34 <|> give S_ (anyChar, anyChar) 21:05:22 so I need PP :: * -> * ;; instance Functor PP ;; instance Applicative PP ;; instance Alternative PP ;; char :: Char -> PP Char ;; give :: MetaFor a b -> b -> PP a 21:05:45 alise: did you accept the grouping then? i could just have whitespace, but i sorta like the idea of brackets when there's pretty much no structure and it's completely needless :P 21:05:52 parse :: PP a -> String -> Maybe a ;; deparse :: PP a -> a -> Maybe String 21:06:05 oklopol: tbh the syntax is minimal enough that it barely matters 21:06:09 yeah 21:06:10 i guess 21:06:11 90% of the program will be a bunch of examples 21:06:16 and the only syntax there is comma and -> :P 21:06:38 yeah, and .'s and :'s 21:06:49 although you just need one of them 21:06:56 yeah they're pretty rare 21:07:02 actually it takes the sum of dots mod 4 21:07:03 compared to examples 21:07:18 0 is test, 1 is base, 2 is subcase, 3 is recursive case 21:07:27 http://hackiki.org/wiki/features I added some documentation of Hackiki's feature to hackiki.org (zomg) 21:07:28 I should just make a language where every function has to be invertible 21:07:41 notably, it would protect programmers from using strong encryption 21:07:56 so you can write :., .: or ... 21:08:08 Gregor: wow, that is glacial. 21:08:11 oklopol: XD 21:08:14 oh wait actually ofc you can't write everything with :'s, turns out : isn't a prime 21:08:18 *turns out 4 isn't 21:08:24 hey you guys 21:08:27 hey augie 21:08:34 augur. 21:08:36 not augie 21:08:37 :| 21:08:38 Gregor: wow that's like recursion 21:09:00 oklopol: Uhhh? 21:09:08 Gregor: nm. 21:09:12 oh I forgot, I also need anyChare :: PP Char 21:09:22 "documentation of Hackiki's feature to hackiki.org" <<< X in X. 21:09:23 Gregor: he was mocking you :) 21:09:39 that really made no sense 21:09:46 ...yeah mocking 21:09:51 well, more or less 21:09:54 so cleverly you don't even get it 21:09:55 I have a OpenID program but how can I get it to work? 21:10:10 augur: what's wrong with augie 21:10:27 it was the name of a friends brother when i was younger 21:10:30 This is what I have so far http://zzo38computer.cjb.net/openid/openid.php 21:10:37 so in my mind it's not the diminutive of augur 21:10:37 As you can see, it doesn't work. 21:10:41 its just a different name 21:10:43 i call alise allie and Sgeo sgay 21:11:03 yes and im not saying its not a reasonable diminutive for augur 21:11:15 but to my ear it doesnt _sound_ like a diminutive, it just sounds like a different name 21:11:22 okay, i see 21:11:31 if you can think of another cutive, i can used that. 21:11:41 *use 21:11:43 augur is cute enough! 21:11:52 aurgy 21:11:54 you wish 21:11:57 zzo38: You give that URL to something with OpenID login ... to log in. 21:12:01 "auglet" 21:12:04 http://dblp.uni-trier.de/db/indices/a-tree/v/Vijay=Shanker:K=.html 21:12:09 look at all those wonderful papers T_T 21:12:33 i think someone should build a programming language that uses a LIG/TAG or something 21:13:25 zzo38: did you... configure it? 21:13:44 afk 21:16:10 -!- tombom has joined. 21:16:39 -!- KingOfKarlsruhe has joined. 21:21:39 I did give that URL to sometihng to log in, and it says it is wrong! 21:21:47 http://www.wasab.dk/morten/2007/11/openid/ 21:22:09 fix_n f = f (fix_n f)^n where n>0 21:22:16 zzo38: you didn't configure it 21:22:17 edit the file 21:26:05 How? 21:28:32 with a text editor. 21:28:44 back yo 21:29:21 I know that, of course. That isn't what I meant 21:32:30 oklopol: i had an interesting idea for a modification of prolog 21:32:31 :x 21:32:58 do you mean some sort of unification over quantifiers with a dash of absolute convergence? 21:33:21 what? :| 21:33:30 by which i mean do explain, we can hope i understand a word of it 21:33:38 nothing 21:33:52 I looked at the codes but it looks like correctly. 21:34:11 i keep saying things that mean nothing today, especially irl, here i can just not press enter 21:34:18 it wouldnt modify standard prolog (unless prolog already does this) but 21:34:31 foo(X), bar(X) ---> foo(bar(X)) 21:39:30 I can see what's wrong now. It is trying to open /dev/urandom and that's why it doesn't work. 21:40:40 # Each of the n characters in a name must come from a different character partition, where a character partition is identified as any character within the range [0..99], [100..299], ..., [3600..3699]. For example, while ŸēĴǥȬʂ˩̪ΘкүӾԦב؏ڀۙݥގࠅࡁࣷईং৔ਾ૖ૻஃ௵శದദං෌แ clearly is an elongated streams, ٬੓ಛ଩ƀĚЇ̢ߊvǢϦɸ܀৺૊౭஌<؅ࠀ˽ࣄܢɒ௵ँෞݜғๅࡼՠҰേজඛ is not a value chain, basi 21:40:40 cally because there are two unicode characters within the range [1800..1899] in here. Neither is ಉ̪ݛՁूϚ֡Ŝ٘ல෌࠴ৄॼˋ߷нɋwCьÒޜӠ౬؀૔ങࣷۮǐਖ਼ఄବʔ൬, mainly because it is 36 characters long and there is no such thing as a 36 characters long identifier in i®™. 21:40:50 No, it is still wrong. 21:40:51 --Gerson Kerz, i spec 21:41:11 [[Lets talk about sourcecode first. The character set for a legal i input file must be in Punicode encoding, as specified in RFC 3492 and the file must have a utf-16be BOM. This helps keeping the code secure, because nobody can use something as trivial as Notepad to edit i sourcecode.]] 21:55:28 -!- zzo38 has left (?). 21:55:53 class (PFunctor p r t, QFunctor p s t) => Bifunctor p r s t | p r -> s t, p s -> r t, p t -> r s where 21:55:53 bimap :: r a b -> s c d -> t (p a c) (p b d) 21:56:09 when you start implementing an instance of this, is that the signal that "make this so my life is easier" has failed utterly and horribly? 22:03:29 let's just say that looks like a lot of letters 22:04:01 turns out I also have to implement 22:04:02 class (Category r, Category t) => PFunctor p r t | p r -> t, p t -> r where 22:04:02 first :: r a b -> t (p a c) (p b c) 22:04:03 and 22:04:06 class (Category s, Category t) => QFunctor q s t | q s -> t, q t -> s where 22:04:06 second :: s a b -> t (q c a) (q c b) 22:04:15 augur: i don't see how that makes sense 22:04:18 (this is just for a parsing library.) 22:04:27 oklopol: what? 22:04:36 "augur: foo(X), bar(X) ---> foo(bar(X))" 22:04:44 oklopol: why doesnt that make sense 22:05:26 -!- kar8nga has quit (Remote host closed the connection). 22:06:21 i just don't see what the point is 22:08:45 fizzie / Deewiant / any finn online? 22:09:10 oklopol: theres no point, except to make it weirder 22:09:50 oh well i can imagine it would do that 22:10:05 so do you own at finnish 22:10:12 oklopol: not yet 22:10:25 i need to know some train schedules but my internet is not alive 22:10:44 i'm completely offline atm 22:17:37 -!- KingOfKarlsruhe has quit (Remote host closed the connection). 22:24:49 oklopol: How is your Internet not alive if you can do the IRC 22:25:12 TELEPATHY 22:25:26 He's emitting gamma rays that flip bits in Freenode's RAM that make it think he's connected and sending messages. 22:25:42 I suppose DNS could be dead but there are easier ways to work around that than asking somebody else over IRC 22:34:25 pikhq: write my haskell function for me, thx 22:34:38 alise: Whatever for? 22:35:06 pikhq: a bi-directional ([token] -> a and a -> [token] from the same parser), applicative parser 22:35:15 i'm fairly sure a certain function is unimplementable 22:35:48 http://pastie.org/823742.txt?key=ugezvaboaxv3tg15cjeja 22:35:51 Good luck, sucker! 22:36:04 alise: Have you tried Parsec and a show/read instance? 22:36:22 Yeah, because Parsec can take an AST and give you back corresponding source. 22:36:28 Without writing a separate deparser. 22:36:45 Since it can do that, it's exactly what I want and I'm duplicating effort by writing something that can do that. 22:36:51 :P 22:36:52 Is a pretty printer that hard? 22:36:52 :P 22:37:21 Is a pretty-printer that handles things like only putting parentheses in when needed harder than simply writing a parser and having it automatically deparse too? 22:37:26 Yes; much harder. 22:37:31 And a library only has to be written once. 22:38:03 Ehh, eff that. 22:38:26 I've got a dozen more kanji or so I'd like to learn today. 22:38:34 Bah! 22:40:48 Deewiant: it's just really slow, if you need to know. 22:40:53 Mmm, autodidactism. 22:40:57 It is such a wonderful thing. 22:41:26 there's no other didactism, teaching is just an attempt to direct focus. 22:41:41 crazy person says what 22:41:50 i love clue 22:42:32 -!- coppro has joined. 22:43:15 also i just realized mutual recursion can't really be added just like that, the whole language needs to be changed quite a lot 22:43:24 well, who needs mutual recursion anyway 22:43:45 mutual recursion just leads to sadness 22:43:48 as does regular recursion 22:43:58 Hmmm... I think I have figured out another way for computing coordinates when moving through wormholes, but that way doesn't support nested wormholes at all. But one could have multiple funge spaces connected with wormholes... 22:44:17 Deewiant: so what are the ways around it? 22:44:26 If you get rid of self-reference, you won't have nasty paradoxes 22:44:37 oklopol: Switching your DNS server? 22:44:49 Or just remembering the IP address of Google 22:44:53 (An IP address) 22:45:01 there's no other didactism, teaching is just an attempt to direct focus. 22:45:05 i have no idea how to switch DNS server ofc 22:45:07 i've not been able to state it better 22:45:39 I've heard it better; it's on the walls of my school better 22:45:47 s/better$/somewhere/ 22:45:57 Oh, the irony. 22:46:09 :P 22:46:20 and here i thought it was my own thinking 22:46:44 oklopol: Linux: /etc/resolv.conf; Windows Vista: Control Panel -> Network and Sharing Center -> Manage Network Connections -> right-click your connection -> Properties -> TCP/IPv4 -> Properties -> Use the following DNS server addresses 22:47:31 Deewiant: that's easier than asking someone? that's like... 8 clicks! 22:47:32 anyway is there a list from which i can choose? 22:47:56 because sort of hard to get addresses if you're offline 22:48:17 wuut 22:48:51 oklopol: 8.8.8.8, 4.2.2.2 for example 22:49:17 oh okay 22:49:48 I mean, just memorize/write down some public ones :-P 22:50:45 not sure that's very useful 22:50:53 i guess if you need to do that often 22:52:05 -!- tombom has quit (Quit: Leaving). 22:52:53 okay what should i write in this thing 22:53:21 trivialities like fibs and append aren't really much of a test case 22:53:45 what is a good test case 22:54:01 something slightly more complicated 22:54:39 Like a kernel. 22:54:50 Make an OS kernel a one-linear. 22:54:53 One-liner, even. 22:55:18 there's one slight problem 22:55:24 you can't write a one-liner in clue 22:55:59 oh wait you can 22:56:37 oklopol: write life 22:57:03 ah, that's good, although maybe 110 first 22:57:37 maybe i should add infinite lists........................................................ 22:57:42 noooooooo! 22:57:56 :D 22:57:59 what's wrong with infinite lists 22:58:08 infinite lists are IMPLAUSIBLE 22:58:23 hmm, yeah that's a good point 22:59:28 implausible how. 23:01:08 well, first of all infinity is a REALLY big number 23:01:53 oklopol: infinity = infinity + 1 23:01:56 Roughly that big. 23:01:57 :P 23:02:10 good point, it's even bigger 23:02:13 MissPiggy, oklopol, wanna hear something cool about natural language? :o 23:02:16 yes 23:02:19 hi augur! 23:02:20 yes 23:02:33 ok 23:02:53 hi auglet 23:03:21 suppose that M("brown") = \x.brown(x) 23:03:37 (that is, the meaning of the word "brown" is some predicate of brownness) 23:03:41 and M("cow") = \x.cow(x) 23:04:14 ok 23:04:34 * oklopol is supposing the ass of those truths 23:04:40 it seems to be the case that humans are only capable of learning that M([a b]) = \x.M(a)(x) && M(b)(x) 23:04:57 huh 23:05:12 ie [brown cow] = \x.M("brown")(x) && M("cow")(x) = \x.brown(x) && cow(x) 23:05:48 its not possible that M([a b]) = \x.M(a)(x) || M(b)(x) 23:06:00 of course a brown cow isn't either brown or a cow? 23:06:03 or'm I missing something 23:06:04 e.g. M([brown cow]) = \x.brown(x) || cow(x) 23:06:11 thats the point! 23:06:15 or rather 23:06:23 also, humans cannot learn that [big toy] is in fact a small rabbit 23:06:24 The point is that languages just plain don't do that. 23:06:27 Interesting. 23:06:30 yes, in _practice_, a "brown cow" is not something that is either brown OR a cow 23:06:38 -!- Pthing has quit (Quit: Leaving). 23:06:58 but its not merely a happenstance thing about existing languages 23:06:59 I thought of it as brown(cow) 23:07:02 why isn't it that? 23:07:03 its a fact about POSSIBLE languages 23:07:13 MissPiggy: because cow is a concept, not a thing. :P 23:07:46 brown(cow) surely denotes that the CONCEPT cow is brown 23:07:50 or that all cows or brown 23:07:51 Also, [brown cow] could then be applied to something else. 23:07:55 hmmmm 23:08:04 Say, [brown cow dance]. 23:08:05 well alright that does make sense what you are sayng 23:08:09 alise: also, kids can indeed learn that "big toy" means "small rabbit" 23:08:13 (silly example, but gets the point across) 23:08:43 just like they can learn that "brown cow" means "rootbeer float made with chocolate icecream not vanilla 23:09:04 can't learn as in physically can't? 23:09:08 because i have a new thing to try on my future kids 23:09:29 as in you can try to teach a kid a new adjective and/or a new noun 23:09:36 call it "prown" and "gow" 23:09:44 such that a "prown gow" is either brown, or a cow (or both 23:09:45 ) 23:09:59 and kids cant get it. 23:10:18 And now, he's going to try to make a conlang with that as a grammatical feature just to fuck with his kids. :P 23:10:18 and where something that is just "prown" is brown 23:10:23 and something that is just a "gow" is a cow 23:10:32 goat 23:10:52 augur: how do you test something like this? 23:10:56 for whatever reason, in natural language, syntactic concatenation = semantic conjunction 23:10:58 He's a genius reckless. 23:11:00 BUT WHICH 23:11:13 oklopol: acquisition labs 23:11:19 oh? 23:11:25 Jeff Lidz has an acquisition lab 23:11:37 basically we try to teach kids novel words or constructions 23:11:49 that sounds cool 23:11:51 and they can learn a lot of them really easily 23:11:59 but they cant learn some of them at all 23:12:11 anyway who cares about kids, they're retards anyway, i bet i could learn a language where concatenation is disjunction. 23:12:20 That is both clever and obvious. 23:12:23 oklopol: not as a natural language :) 23:12:55 you would not be able to employ it in such a fashion naturally. your usage would, rather quickly, come to use concatenation to mean conjunction. thats the weird and crazy thing. 23:13:00 or heres another one 23:13:00 augur: so basically it's kid guinea pigging :) 23:13:13 alise: yes :) 23:13:16 perhaps it's just because conjunction is far more common than disjunction 23:13:23 quantifiers (words like "all", "some", "every", etc.) must obey the following rule 23:13:44 augur: i don't believe that 23:13:48 "all X are/do Y" must mean the same as "all X are X's that are/do Y" 23:13:57 e.g. "all dogs bark" = "all dogs are dogs that bark" 23:14:23 instead of what? 23:14:23 now im going to bet that this ALSO seems pretty fucking obvious 23:15:00 but consider that if "all" is just some binary subset function, e.g. "all X Y" = X ⊆ Y 23:15:12 then why cant we have "lall X Y" = Y ⊆ X? 23:15:20 loll X Y 23:15:21 e.g. "lall dogs bark" = "all barkers are dogs" 23:15:23 ;) 23:15:33 yes, it was quite intentional :) 23:15:36 Tangential, but I always find it weird when people talk about Noam Chomsky in the context of politics. 23:15:58 GNU/Chomsky 23:15:59 pikhq: why? hes one of the leading far left political commentators 23:16:26 augur: I always think of his work on formal grammars. 23:16:31 true. 23:16:41 augur: i don't think "not as a natural language" means anything, natural languages are much harder to talk in than, say, math 23:17:00 oklopol: No, much easier. 23:17:04 oklopol: ofcourse they are, but thats because natural language is complicated in weird and hard-to-understand ways 23:17:11 you always end up explaining anything even slightly complicated on paper, because natural languages are so crappy 23:17:11 and its not entirely arbitrary, either 23:17:13 You talk in a natural language without thinking about it all the time. 23:17:15 Math, you think about. 23:17:30 pikhq: math isnt hardwired into our brains ;) 23:17:33 objectively, its easier. 23:17:37 augur: Well, yes. 23:17:46 That is what makes it easier... 23:17:46 its also precise, and well defined 23:17:51 we understand it 23:18:03 or at least, we understand how to understand statements in math 23:18:13 eh? often while proving things i'm thinking about something else 23:18:17 and we understand why those statements mean what they mean because we defined them 23:18:20 i mean if it's something simple 23:18:43 but natural language has completely crazy, bizarre constraints on its mapping from form to meaning 23:18:50 heres a purely grammatical one, pikhq 23:18:55 you know what a cyclic permutation is? 23:19:08 augur: Not entirely. 23:19:19 Though I may find it obvious once you describe it. 23:19:20 what's a cyclic permutation? 23:19:29 My knowledge of linguistics is very... Vague. 23:19:36 its math, actually, but 23:19:49 And my knowledge of math is incomplete. 23:20:05 a cyclic permutation is basically an arrangement of some set of items such that the relative ordering is the same, including looping around to the beginning again 23:20:21 Oh, the obvious meaning associated with those words. 23:20:25 e.g. the cyclic permutations of "abcde" are "abcde", "bcdea", "cdeab", "deabc", and "eabcd" 23:21:01 okay so permutations that have just one cycle or whatever it's called 23:21:05 cyclic permutations are _impossible_, as far as anyone can tell, as grammatical rules. 23:21:36 O_o 23:21:51 "I ate the food" "Food I ate the" "The food I ate" "Ate the food I". 23:22:16 * pikhq just thinking it over 23:22:22 Huh. 23:22:25 well, lets not use that as an example 23:22:26 as grammatical rules, how? 23:22:44 i mean in what sense, well i guess any sense? 23:22:48 lets say, instead, that there are some adjective classes, e.g. color, size, subjective judgement 23:23:09 e.g. red, small, and pretty 23:23:37 lets say its then grammatical to have them in that cyclic order: color, size, judgement 23:23:41 K. 23:23:58 heh, now i keep reading all concatenations as disjunctions 23:23:58 such that "red small pretty button" "small pretty red button" and "pretty red small button" are fine 23:24:00 but nothing else is 23:24:14 "cyclic order" is a bit of a brainteaser 23:24:34 in that context 23:26:16 interesting 23:26:21 augur, I read that Sumarian doesn't have any order 23:26:22 or lets take verbal auxiliaries 23:26:32 so every cyclic permutation of words meant the same thing 23:26:36 "john has been being an ass lately" 23:26:46 not that i believe testing this stuff on kids tells us anything, but i suppose most people do believe kids can learn languages. 23:26:49 or even better "john will have been being an ass" 23:27:00 something i seriously doubt 23:27:12 no that wont work actually haha 23:27:16 ... You doubt children can learn languages. 23:27:23 lets just say its "john will have been an ass" 23:27:29 that order, will-have-be 23:27:33 Clearly, you merely became fluent at the age of 18. 23:27:34 :P 23:27:44 let that be the cyclic ordering of those auxiliaries 23:28:01 well yeah, i mean sure they can mangle some sorta crap, but a kids aren't fluent speakers, you learn languages explicitly, when you're older 23:28:01 such that "john will have been an ass" = "john have been will an ass" = "john been will have an ass" 23:28:09 this is not something kids can learn 23:28:15 *-a 23:28:34 oklopol: no, kids DO learn languages quite well 23:28:37 hmm 23:28:39 its a mistake to assume otherwise. 23:28:54 formal training in "Proper" language is entirely bullshit 23:29:03 what you speak is language 23:29:07 not in my experience 23:29:07 no 23:29:14 so anyway. 23:29:28 there are just these constraints on what is a possible human language 23:29:39 and they dont seem to be objectively motivatable 23:29:48 oklopol: You sound like a prescriptionist. 23:29:53 cyclic permutations especially, since humans can do perfectly well on them when its not language 23:29:55 of course i'm a prescriptionist 23:30:03 oklopol is just silly. 23:30:09 you would be too, if you knew how crappy natural languages are 23:30:27 You also sound silly. I knew proper, formal English from a young age... 23:30:27 oklopol: you'd stop being one if you realized how crappy prescription actually is ;) 23:30:47 prescriptivist, you idiots 23:30:50 it's prescriptivist! 23:30:53 and they're IDIOTS! 23:31:02 Please say prescriptivist. prescriptionist is just wrong. 23:31:02 alise: ITS PRESCRIPTIONIST NOW. MUAHAHAHAH. 23:31:04 natural language is extremely good at doing what it was evolved to do 23:31:04 ;) 23:31:05 but seriously, don't even talk about them 23:31:07 be a descriptivist 23:31:09 and thats NOT math. 23:31:09 GET IT GUYS GET IT 23:31:17 IT'S A DESCRIPTIVIST BEING PRESCRIPTIVIST ABOUT THE WORD PRESCRIPTIVIST 23:31:19 augur: no it's not 23:31:23 it sucks at it. 23:31:27 no it doesnt 23:31:31 yes it does 23:31:43 oklopol: Propose some alternatives? 23:31:50 well, it sucks objectively speaking, but you cant make it better 23:31:53 yes, use lojban or something 23:32:08 lojban is either just as sucky, or impossible to use naturally. :) 23:32:17 that's not true 23:32:20 yes, it is. 23:32:28 no, it's not. 23:32:31 yes, it is. 23:32:31 "Fluent" speakers produce Lojban that doesn't parse quite right. :P 23:32:33 -!- SimonRC has quit (Ping timeout: 265 seconds). 23:32:34 no, it's not. 23:32:40 yes, it is, oklopol. 23:32:45 no, it's not, augur. 23:32:57 the human language faculty is what it is. 23:33:11 if lojban does not fit this mold, then it simply cannot be used naturally. 23:33:26 if it does fit this mold, then it is subject to all of the problems that non-lojban languages are subject to. 23:33:50 augur: Well, all of the problems that *all* non-lojban languages are subject to. 23:33:58 i'm gonna go to sleep now, you keep on dreaming; in any case, that was interesting stuff, is there a comprehensive listing of these testings? 23:33:58 well i don't care, communication sucks anyway 23:34:15 oklopol: i agree. lets just fuck instead. 23:34:17 yeah 23:34:17 It can at least avoid certain of them, like "having a spelling that is completely unrelated to how it's spoken". 23:34:20 sex works 23:34:22 natural sex. 23:34:33 pikhq: thats not language tho, thats orthography 23:34:40 but orthography is already unnatural. 23:34:41 augur: True. 23:34:57 further, "completely unrelated" is a difficult thing to explain. 23:35:09 Mm. Yeah. 23:35:19 natural languages don't have variables and proper mathematical quantifiers, i guess that's the thing i hate about them most 23:35:30 english orthography, except for some rough patches, is actually quite decently transparent. 23:35:35 its just not compositionally transparent. 23:35:42 oklopol: actually they do :) 23:36:00 the variables are just not as easilly handled, and the quantifiers require bigger phrases. 23:36:35 yeah, in other words the most fundamental concepts of communication suck ass 23:36:57 not for what theyre designed to do! :) 23:37:08 how does it suck??? 23:37:33 it sucks because oklopol is trolling is all. 23:37:36 and hes a robot 23:37:41 augur: Transparent? Mmm. Well, the spelling at least has some affiliation with the pronunciation. 23:37:42 eh, i'm not trolling 23:37:45 but really sleep -> 23:37:53 Though it varies based upon etymology. 23:37:54 also answer my question if you have the time 23:37:54 -> 23:41:29 pikhq: so yeah. find a good explanation for these things. 23:41:34 its tricky! 23:44:08 -!- SimonRC has joined. 23:47:21 -!- oerjan has joined. 23:48:31 Hail, oerjan. 23:48:55 oerjan: I asked oklopol to ask the little copy of you in his head, but he didn't, so: it *is* possible to write a bidirectional parser, right? 23:48:57 Yes? Good. 23:49:03 (I'm 99% sure it is, so.) 23:49:13 um what is a bidirectional parser 23:49:14 what do you mean by bidirectional? 23:49:32 it's both gay directional and straightdirectional 23:49:33 *gaydirectional 23:49:42 -!- adam_d has joined. 23:49:57 i'm not sure that works. 23:50:17 try with homo- and hetero- 23:50:21 what's the definition of gay, is it just "same sex" or "at least same sex" 23:50:25 yeah 23:50:31 that's better 23:51:09 i'd say it's evilly mixing greek and latin roots, but the -sexual versions already do that 23:51:45 yeah but can homo- or gay include bi's? 23:51:56 homo- can't 23:52:20 that sounds kinda stupid 23:52:20 bi is like sqrt(2)/2 * straight + i * sqrt(2)/2 * gay 23:52:32 alise: yes. it is possible. 23:52:34 how do I add a quote to the bot? 23:52:40 `addquote 23:53:03 gay(x) = sex(x)==sex(me); straight(x) = sex(x)!=sex(me); bi(x) = gay(x) || straight(x); 23:53:09 I am bidirectional parser curious 23:53:13 where orientation(x) = "is it okay to consider this relationship under this sexuality" 23:53:18 I dabble a bit in pretty printing and sexy parsing 23:53:32 parsing isn't sexy 23:53:34 it's really annoying 23:53:37 mine is 23:53:41 hmm 23:53:45 yeah maybe 23:53:50 :3 23:53:54 further constraints may be applied of course 23:54:05 `addquote bi is like sqrt(2)/2 * straight + i * sqrt(2)/2 * gay 23:54:10 pansexual = bi + any other constraint considering gender is omitted 23:54:13 129| bi is like sqrt(2)/2 * straight + i * sqrt(2)/2 * gay 23:54:19 alise: thats not what bi means :p 23:54:30 oerjan: bidi parser = one parser definition does both [tok] -> a and a -> [tok] 23:54:42 but its an interesting interpretation! 23:54:46 alise: sounds like something you'd do with prolog 23:54:49 augur: you can prefer one gender over the other in bi 23:54:58 this is true. 23:54:58 but the functions I wrote meant "is this okay by this orientation" 23:55:01 That makes my brain hurt :P 23:55:12 pansexuality is basically bisexuality with both sexes having the same weight 23:55:13 i didn't get her formalism at all 23:55:24 oerjan: yeah, well I'm doing it in haskell. 23:55:28 oerjan: it is _difficult_. 23:55:46 don't forget omnisexuality 23:55:48 alise: not really. 23:55:51 alise: maybe you can abuse Show/Read derivation for it? 23:55:57 omnisexuality? does that exist 23:55:59 pansexual is the fancier version of bisexual, basically. 23:55:59 augur: then what do you consider pansexuality? 23:56:03 well, yes 23:56:03 but 23:56:08 thats how pansexuals use it. 23:56:12 bisexual = I potentially like people of both genders 23:56:18 because would be nice to have a word that actually means what pansexuality should mean 23:56:25 pansexual = I do not consider gender when deciding whether I like someone 23:56:29 omnisexual = I fuck everything 23:56:29 panisexual: attracted to bread 23:56:30 is the "official" definitionerition 23:56:33 alise: this is not the case. 23:56:39 augur: wikipedia agrees qed 23:56:41 but yeah 23:56:43 pansexual is a faggot term 23:56:45 ...wait 23:56:54 well wikipedia is irrelevant. :P 23:57:10 thus is your mother. 23:57:10 biosexual: Attracted to anything living 23:57:13 Can't make a derived instance of `Show (Syntax t a)' 23:57:14 (Constructor `Sequence' does not have a Haskell-98 type) 23:57:17 god things annoy me today 23:57:17 fukkkkkkkkkkkkkkkk yuuuuuuuuu 23:57:29 shut up oklopol GOD!!! I can't belive you sometimes 23:57:32 maybe it's partly because my head hurts like hell 23:57:42 hexosexual: Attracted to six. 23:57:46 pansexual is so stupid :( 23:57:50 I hate that word 23:57:58 alise: if you're going to be discussing these, please use the specific definitions of gender and sex 23:58:00 alise: i vaguely recall someone doing something something typeclass polymorphic to get both directions of parsing in haskell. but maybe i'm confusing it with something else. 23:58:15 coppro: i'm basing it on a utopian world where people consider gender, not sex 23:58:28 admittedly for sexual relationships it needs ... somewhat of an adjustment 23:58:32 exercise for the reader 23:58:40 alise: regarding bidirectional parsing, i presume you mean from either end of the input string? 23:58:47 23:54 < oerjan> alise: sounds like something you'd do with prolog 23:58:53 Yes oerjan has a good point 23:59:00 quite a few programs you write as DCGs are invertible 23:59:16 augur: no, I mean that one syntax definition generates both a parser and a printer 23:59:32 basically imagine String->a, to generate a->String you just swap LHS and RHS, basically 23:59:45 it's like that, with all the difficulties I omitted, with lots of extra trouble because parsers aren't that simple in actuality 23:59:59 you can't swap LHS and RHS>..