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