←2012-02-28 2012-02-29 2012-03-01→ ↑2012 ↑all
00:03:48 -!- zzo38 has joined.
00:07:23 <olsner> hmm, so the tricky part appears to have been making defined functions have bindings for their name in their own environments
00:07:47 <olsner> so I have a purely functional lisp now, I think
00:08:33 <olsner> next step: implement enough stuff to write a different lisp in that lisp
00:20:05 -!- augur has joined.
00:20:06 -!- Jafet has joined.
00:20:45 -!- augur has quit (Remote host closed the connection).
00:40:13 -!- derdon has quit (Remote host closed the connection).
01:06:54 -!- cheater_ has quit (Ping timeout: 244 seconds).
01:20:49 -!- cheater_ has joined.
02:17:17 -!- augur has joined.
02:29:02 <Sgeo> olsner, well, first thought, is something like the State monad >.>
02:45:55 -!- cswords has quit (Ping timeout: 260 seconds).
03:38:30 -!- NihilistDandy has joined.
04:11:54 -!- mmorning has joined.
04:13:13 -!- PiRSquared has joined.
04:14:01 -!- mmorning has left.
04:18:43 <PiRSquared> http://www.cs.bham.ac.uk/~ais523/ this page seems to have <?php ?> tags which are not being processed on it
04:22:13 -!- pikhq_ has joined.
04:24:58 -!- pikhq has quit (Ping timeout: 240 seconds).
04:49:35 <zzo38> Is what kind State monad?
04:49:35 <lambdabot> zzo38: You have 2 new messages. '/msg lambdabot @messages' to read them.
04:49:40 <zzo38> ?messages
04:49:41 <lambdabot> elliott said 15h 46m 15s ago: yes, by the way: http://creativecommons.org/publicdomain/zero/1.0/legalcode.txt
04:49:41 <lambdabot> elliott said 15h 46m 3s ago: and see http://wiki.creativecommons.org/CC0_FAQ#May_I_apply_CC0_to_computer_software.3F_If_so.2C_is_there_a_recommended_implementation.3F
04:54:23 -!- MDude has changed nick to MSleep.
05:05:13 -!- MSleep has quit (Ping timeout: 248 seconds).
05:07:28 <oerjan> > 259*6
05:07:29 <lambdabot> 1554
05:48:01 -!- kallisti has joined.
05:48:49 <kallisti> ..cpan tests are insane.
05:48:56 <kallisti> I'm sitting and waiting
05:49:01 <kallisti> for like hundreds of tests to finish.
05:49:07 <kallisti> thousands?
05:50:44 -!- const has quit (Excess Flood).
05:53:16 -!- variable has joined.
05:54:16 -!- NihilistDandy has quit.
06:01:03 -!- PiRSquared has changed nick to PiRSquaredAway.
06:01:51 -!- graue has quit (Quit: Leaving).
06:10:27 -!- oerjan has quit (Quit: Good night).
06:15:32 -!- Goosey has quit (Ping timeout: 252 seconds).
06:33:52 -!- Sgeo has quit (Read error: Connection reset by peer).
06:34:05 -!- Sgeo has joined.
06:34:29 -!- Goosey has joined.
06:36:23 -!- itidus21 has joined.
06:39:58 -!- pikhq has joined.
06:40:09 -!- pikhq_ has quit (Ping timeout: 244 seconds).
06:52:45 <mroman_> olsner: Hu @Lisp
07:06:32 <Sgeo> ?
07:14:46 <mroman_> He has a purely functional lisp in some lisp.
07:14:55 <olsner> Sgeo: yes, the state monad, done manually, with something like a Map and a counter for fresh IDs as the state
07:19:21 -!- calamari has quit (Quit: Leaving).
07:35:09 -!- azaq23 has quit (Read error: Connection reset by peer).
07:36:29 <zzo38> What is this stuff about a state monad?
08:04:24 <mroman_> Hm.
08:04:33 <mroman_> Finding optimal constants is really not that easy
08:08:48 <mroman_> Either pick size or speed.
08:09:36 <mroman_> @brainfuck like constants
08:09:36 <lambdabot> Unknown command, try @list
08:09:42 <mroman_> @list
08:09:42 <lambdabot> http://code.haskell.org/lambdabot/COMMANDS
09:20:45 -!- Vorpal has joined.
09:48:40 <mroman_> My irssi stopped logging stuff since 29. Feb 2012 o_O
09:53:01 -!- MoALTz has joined.
09:53:40 -!- PiRSquaredAway has quit (Ping timeout: 276 seconds).
09:55:48 -!- MoALTz_ has quit (Ping timeout: 245 seconds).
09:55:56 <monqy> that's today, isn't it
09:57:56 <fizzie> It no longer logs the future, like it used to.
10:00:43 <mroman_> yes.
10:00:52 <mroman_> since today midnight.
10:03:03 <fizzie> It's taking the leap day off.
10:03:44 -!- zzo38 has quit (Remote host closed the connection).
10:16:37 -!- ais523 has joined.
10:17:07 <mroman_> No
10:17:17 <mroman_> My permissions are corrupted somehow
10:17:24 <mroman_> ls -lah tells me 664
10:17:36 <ais523> hi everyone
10:17:42 <ais523> except elliott because he isn't here
10:17:43 <mroman_> but no access to it
10:18:32 <fizzie> ais523: I think there's quite a lot of other people who are not here either.
10:19:57 -!- mroman_ has left.
10:20:00 -!- mroman_ has joined.
10:21:47 -!- mroman_ has left.
10:21:50 -!- mroman_ has joined.
10:26:28 -!- derdon has joined.
10:30:14 -!- derdon has quit (Remote host closed the connection).
10:36:17 -!- monqy has quit (Quit: hello).
10:40:24 -!- MoALTz has quit (Ping timeout: 244 seconds).
10:40:36 -!- MoALTz_ has joined.
11:09:51 -!- pikhq has quit (Ping timeout: 246 seconds).
11:42:16 <Vorpal> <fizzie> It no longer logs the future, like it used to. <-- what?
12:04:16 <ais523> hmm, this polymorphic variants thing in OCaml is about halfway between standard type systems and Anarchy
12:04:27 <ais523> it'd be a lot more of the way if you could have polymorphic temporary bindings
12:05:06 <ais523> # q(4) // q(4) ;;
12:05:07 <ais523> - : '_a -> [> `E of [> `E of '_a * int ] * int ] = <fun>
12:05:09 <ais523> # let x = q(4) in x // x ;;
12:05:10 <ais523> - : (_[> `E of 'a * int ] as 'a) -> [> `E of 'a * int ] = <fun>
12:05:17 <ais523> see the problem?
12:05:40 <ais523> in Anarchy, you'd expect the two (translated appropriately for syntax) to do the same thing
12:06:57 <ais523> one thing that's definitely nice is that OCaml's syntax for types is expressive enough to describe all the types in Anarchy (or would be, if a couple of arbitrary restrictions were removed)
12:07:37 <fizzie> Vorpal: Just, you know, horsing around. (Isn't that the expression?)
12:07:46 <fizzie> (No actual horses were involved.)
12:07:51 -!- oklopol has joined.
12:09:31 <ais523> anyway, this is the fundamental reason that oerjanswap doesn't type in OCaml (and Haskell does even worse)
12:09:50 <ais523> it's because if you copy something with :, both languages expect both copies to be applied to the same sort of stack
12:09:54 <oklopol> who's oerjanswap
12:11:10 <ais523> oklopol: it's an Underload program, aa((!((aa)(!))))*:*^!**^a*^a*aa*(*:*^!**^)*^
12:11:17 <ais523> it does the same thing as ~ but without using ~
12:11:48 <ais523> I've actually been having fun trying to create it, the *:*^ bit is IMO the most important bit
12:11:54 <ais523> *to recreate it
12:12:08 <oklopol> oerjan is made of magic
12:12:14 <fizzie> Oh, Chrome... http://users.ics.tkk.fi/htkallas/bitmap.txt "This page is in [Galician]. Would you like to translate it? [Translate] [Nope]"
12:12:19 <fizzie> I... really don't think it is.
12:12:26 <fizzie> Though admittedly I don't speak Galician.
12:12:48 <ais523> does it translate to anything intelligible?
12:12:52 <oklopol> yes
12:13:06 <fizzie> ais523: Some of the "XXXXXX"s turn into "Xxxxxx"s, and some spaces disappear.
12:13:08 <ais523> from Galician, I mean
12:13:11 <ais523> hmm, OK
12:13:45 <oklopol> that doesn't sound like a lot but it's readable after that
12:14:49 <ais523> oklopol: what are you referring to? the Xxxxxx thing, or something else?
12:15:01 <oklopol> the xxx thing
12:15:45 <fizzie> (The rows are students, and the columns are exercises they've answered; I was trying to check if it looks like the columns are getting sparser as they go from left to right.)
12:16:09 <fizzie> (It does kind of look like they are.)
12:16:30 <oklopol> no it's obviously an ironic take on social darwinism and its effect on post-modern agricultural education.
12:16:39 <fizzie> That, too.
12:18:04 <oklopol> ais523: so what does oerjanswap do?
12:18:11 <oklopol> like, exactly
12:18:12 <ais523> oklopol: the same thing as ~
12:18:23 <oklopol> is there an example run somewhere so i don't have to do it myself
12:18:30 <ais523> on the wiki talk page
12:18:32 <ais523> let me find it
12:18:41 <oklopol> okay thanku
12:18:54 <ais523> http://esolangs.org/wiki/Talk:Underload#Tracing_the_.7E_replacement_code
12:18:55 <fizzie> ThankU, the most grateful university.
12:19:12 <ais523> I find it more useful to step through it in the online interp, though
12:20:52 <Vorpal> huh new mediawiki? When did that happen? Haven't really been paying attention
12:21:39 <fizzie> There was a "coup". (Is that the right word?)
12:21:53 <Vorpal> heh, ehird behind it too hm
12:22:03 <Vorpal> well, I just hope it stays up then
12:22:17 <fizzie> Apparently it needs to be "illegally" or "by force" to qualify as a coup, according to WordNet.
12:22:46 <Vorpal> "I've given myself and User:ais523 bureaucrat rights" <-- right, sounds like a coup
12:23:10 <ais523> Vorpal: Graue set up a redirect from esoteric.voxelperfect.net (which he still owns) to esolangs.org (which ehird now owns)
12:23:19 <Vorpal> right
12:23:31 <ais523> so it's with his blessing, at least
12:23:57 <Vorpal> I'm just worried that it will suddenly go down. Previously ehird's server haven't been the most stable in the long term.
12:23:57 <fizzie> Clarity in Expression 2012 campaign message again: esolangs.org is pointing at elliott's thing, he doesn't "own" the domain, which is what a reasonable person would assume you're referring to if you just say it like that.
12:25:18 <Vorpal> oh so who owns the domain then?
12:25:49 <fizzie> THE ALAN DIPERT is I think the accepted spelling.
12:26:14 <fizzie> (There's been no change there. Well, except maybe in the spelling.)
12:26:18 <Vorpal> fizzie, also "Clarity in Expression 2012 campaign"?
12:26:57 <fizzie> I did one such inane detail-oriented correction few days (weeks?) back under the same title.
12:27:05 <Vorpal> ah
12:27:09 <fizzie> Anything done twice is a tradition.
12:27:15 <Vorpal> indeed
12:27:38 <fizzie> Though it might've been in another channel, actually.
12:27:56 <oklopol> may be Power of the Continuum inspire us to create a new esolang.
12:28:17 <fizzie> 2012-02-23 10:27:52 <fizzie> Also is it a PRNG instead of a RNG? (This message sponsored by the "Exactness in Expression 2012" campaign.)
12:28:26 <fizzie> Oh no, I misrekolibred.
12:28:38 <fizzie> Let's just say they changed the name.
12:28:53 <oklopol> perhaps it's a competing campaing
12:29:00 <oklopol> campaign
12:37:20 <fizzie> Also I think the oerjanswap trace might look more readable if someone aligned the show-the-command, and maybe added the remaining program at the end, something like http://sprunge.us/XJSC even though it's quite a bit wider.
12:37:35 <oklopol> okay i get oerjanswap
12:38:05 <fizzie> An oerjanswap is where aliens swap an oerjan with a fakerjan and fool us all.
12:38:09 <fizzie> It might have already happened.
12:39:13 <oklopol> well i get that he has a pattern which puts something under the topmost thing in stack which is of the form X(pattern)Y, he then puts X under B, pushes Y, and concatenates, then running finishes the job
12:39:35 <oklopol> how the pattern works i don't completely get yet, and i suppose that's the main idea
12:39:42 <oklopol> erm
12:39:48 <oklopol> that should've been X(something)Y
12:40:19 <ais523> hmm, you're thinking about it from the opposite end that I was
12:40:58 <oklopol> well mine is how oerjan wanted it to be solved
12:41:19 <oklopol> at least that's how i understood the comment
12:41:33 <oklopol> or did you mean you're trying to understand The Pattern first?
12:44:06 <oklopol> okay so the pattern is not very complicated
12:45:11 <ais523> I mean, I think we both thought "hey, it's implementing dip"
12:45:29 <ais523> but I didn't think of it in terms of constructing a string to put one element under the other element
12:45:56 <ais523> but rather, using it to escape the bottom element so that you could concat the escaped top one to it safely
12:46:04 <ais523> with some extra stuff in between to pop out the unwanted elements
12:46:12 -!- Phantom_Hoover has joined.
12:46:15 <oklopol> what it does is it forward-creates a program which has put B, remove it, then put something. it duplicates this and removes the last "remove it then put something", and runs. now, B will be put, then removed, then something is put, then B is put again but not removed.
12:46:29 <oklopol> the rest is complicated paren putting and removal by running
12:46:35 <oklopol> but kind of obvious
12:47:38 <oklopol> ais523: MY WAY IS CORRECT
12:48:05 <oklopol> (that's tired for "i'm too lazy to understand what you mean".)
12:49:14 <oklopol> i don't see where in your interpretation the actual swapping happens
12:49:53 <ais523> it constructs (a)(b)(a)(b), then gets rid of the outside ones
12:50:12 <ais523> getting rid of the top one is easy, getting rid of the bottom one you do by sneaking an ! in while you're constructing it
12:50:23 <oklopol> ah cool
12:50:33 <oklopol> but i still prefer my interpretation
12:52:18 <oklopol> because it's putting arbitrary constants under stuff => being able to wrap topmost element in pretty much any piece of code => putting even B under stuff
12:52:28 <oklopol> awesome use of concatenativeness
12:52:30 <ais523> yep, it's a neat one
13:05:27 -!- sebbu2 has joined.
13:05:27 -!- sebbu2 has quit (Changing host).
13:05:27 -!- sebbu2 has joined.
13:08:26 -!- sebbu2 has quit (Read error: Connection reset by peer).
13:09:14 -!- sebbu2 has joined.
13:09:19 -!- sebbu has quit (Ping timeout: 276 seconds).
13:10:05 -!- sebbu2 has changed nick to sebbu.
13:16:04 -!- pikhq has joined.
13:17:04 -!- Frooxius has quit (Ping timeout: 265 seconds).
13:19:24 <ais523> btw, is it weird that I've been reading the wiki offline from the dumps?
13:24:27 <Phantom_Hoover> yes
13:24:37 <Phantom_Hoover> I imagine you are the only person to ever do it,
13:24:40 <Phantom_Hoover> Q.E.D.
13:34:14 -!- ais523 has quit (Remote host closed the connection).
13:35:26 -!- ais523 has joined.
13:45:58 <Phantom_Hoover> I'm trying to compile Oolite, but it keeps erroring out because it doesn't have jsapi.h, in spite of jsapi.h existing.
14:02:12 -!- kallisti has quit (Ping timeout: 272 seconds).
14:09:44 -!- ais523 has quit (Remote host closed the connection).
14:14:03 <Vorpal> Phantom_Hoover, maybe in the wrong directory?
14:14:16 <Phantom_Hoover> Probably, but how am I meant to handle that?
14:14:28 <Phantom_Hoover> There's no configure or anything; just a makefile.
14:14:32 <Vorpal> Phantom_Hoover, check the include path used when compiling then?
14:14:38 <Vorpal> and patch it if it needs it
14:14:53 <Vorpal> Phantom_Hoover, check the place where it is included too
14:15:21 <Vorpal> Phantom_Hoover, and if all else fail check if debian applied any patches to their package of it (if they have one)
14:15:34 <Vorpal> well, any relevant patches
14:18:00 -!- Goosey has quit (Read error: Operation timed out).
14:21:51 <Phantom_Hoover> "src/Core/Debug/OODebugMonitor.m:176:4: error: -fobjc-exceptions is required to enable Objective-C exception syntax"
14:21:56 <Phantom_Hoover> FOR CHRIST'S SAKE
14:22:19 <Vorpal> Phantom_Hoover, well, turn that flag on then?
14:22:50 <Phantom_Hoover> Wait, Arch already /has/ an Oolite package.
14:22:57 <Phantom_Hoover> An up-to-date one, at that.
14:23:16 <Vorpal> arch packages are usually pretty up-to-date
14:40:17 -!- Frooxius has joined.
14:52:59 -!- Phantom_Hoover has quit (Remote host closed the connection).
14:54:40 -!- Phantom_Hoover has joined.
15:01:19 -!- pikhq_ has joined.
15:01:45 -!- pikhq has quit (Ping timeout: 255 seconds).
15:10:37 -!- elliott has joined.
15:10:41 <elliott> http://esolangs.org/wiki/Talk:Basic_Input/Output_Commander oh dear
15:17:54 <ion> Btw, what’s the significance of the logo in the top left corner?
15:18:09 <fizzie> It has sub-lime significance, has it not?
15:20:17 <fizzie> (I suppose the pun in the welcome message has not yet "went".)
15:21:25 <fizzie> If you search the log, you can find that it symbolizes the matrix of solidity.
15:22:34 <fizzie> <ais523> I think the official answer is "it's just an image Graue chose as a placeholder, and people decided they liked it"
15:22:53 <ion> :-)
15:22:56 <fizzie> (It's also called the "trilime".)
15:23:14 <ion> trime
15:32:12 <elliott> ion: It's the logo of the matrix of solidity.
15:34:01 <Phantom_Hoover> ohno, skyrim stop work
15:34:03 <Phantom_Hoover> @ping
15:34:03 <lambdabot> pong
15:34:21 <elliott> hi
15:34:32 <Phantom_Hoover> what if im oolite
15:38:09 -!- MoALTz__ has joined.
15:40:27 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
15:41:07 -!- MoALTz_ has quit (Ping timeout: 244 seconds).
15:41:16 <mroman_> http://fpaste.org/rU0t/ <- is this a correct implementation of tag systems?
15:41:21 <mroman_> ie.
15:41:45 <mroman_> it takes m-characters
15:41:50 -!- Phantom_Hoover has joined.
15:42:01 <mroman_> are production rules with more than one character allowed?
15:43:00 <mroman_> (at least, the code produces the correct output for this example)
15:43:20 * elliott wonders what mroman_ means by "misregistered"
15:43:25 <elliott> the nick mroman isn't even registered at all :)
15:43:48 <mroman_> well
15:43:49 <mroman_> it is
15:43:55 <mroman_> but not verified.
15:44:07 <elliott> -NickServ- mroman is not registered.
15:44:08 <elliott> are you sure?
15:44:20 -!- mroman_ has changed nick to mroman.
15:44:21 <elliott> you should be able to re-register it, I think
15:44:30 <mroman> oh
15:44:31 <mroman> cool
15:44:39 <elliott> actually just
15:44:47 <elliott> n/m
15:45:02 * elliott should think through what he's about to say before saying it :p
15:45:22 <mroman> i grouped it know.
15:46:03 <mroman> I can re-register with the same e-mail address.
15:46:06 <mroman> *can't
15:46:12 <elliott> heh, so mroman_ owns mroman :D
15:46:25 -!- MDude has joined.
15:46:25 * mroman im owned :(
15:46:41 <elliott> whoa, you can set your account name
15:46:42 <elliott> I never realised
15:47:02 <elliott> (/ns set accountname <nick>)
15:47:10 <elliott> if I knew that I wouldn't have had to make new accounts every time I change primary nick :p
15:59:06 -!- itidus21 has quit (Ping timeout: 248 seconds).
16:01:53 <fizzie> "There is a 94% chance your computer has registry problems. Fix them now and increase your PC speed!" This stupid ad banner could do with a [citation needed] for the 94%.
16:05:11 <mroman> My computer has no registry.
16:07:24 <elliott> mroman: Sounds like a registry problem to me.
16:07:31 <fizzie> Well, I do have both Wine on this thing.
16:08:16 <fizzie> Both wine, yes.
16:08:44 <fizzie> Also quite a lot of people seem to be calling the gconf thing a "registry", but no authoritative sources.
16:09:20 <fizzie> I suppose it's officially a "configuration database" instead.
16:09:24 <fizzie> Whoops, bus to catch. ->
16:10:40 <elliott> fizzie needs to keep a closer eye on his buses.
16:12:52 <elliott> "Although folds and maps are preferable in most cases I still miss the generality of the for loop from time to time. There is no good way that I know of to get the functionality of break and continue without having to define a function. So if anyone has a good solution for that, please let me know."
16:38:54 -!- sampero has joined.
16:39:25 <elliott> `welcome sampero
16:39:34 <HackEgo> sampero: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page
16:43:40 -!- sampero has quit.
16:43:51 <Friendship> That worked.
16:45:24 <fizzie> You even made em quit, not just part, so it double-worked.
16:50:23 <elliott> http://esolangs.org/wiki/Collatz_function The wiki really wants <math>, doesn't it.
16:51:56 <Friendship> elliott: If only it had zzo's TeX renderer *sigh*
16:53:32 <mroman> I should add a whimp instruction to Beam
16:54:10 <mroman> Unless someone has an idea how to detect if the flow was reversed and escape it
16:54:18 <mroman> but I don't think that is possible.
16:55:25 <fizzie> What would "whimp" do?
16:55:51 <elliott> Whimper.
16:55:58 <mroman> well
16:56:01 <fizzie> Quietly, in a corner.
16:56:06 <mroman> I'd call it the 'x' construction.
16:56:19 <mroman> if the beam is coming from left change direction to down
16:56:27 <mroman> if the beam is cominf from right, change direction to up
16:56:34 <mroman> if the beam is coming from up/down don't do anything.
16:56:38 <elliott> fizzie: Sort of like speech recognition researchers do every night.
16:56:47 <elliott> Fully aware of the futility of their life.
16:57:01 <mroman> Which would enable it to detect if the control flow was reversed
16:57:06 <mroman> and make things a lot easier.
16:57:23 <mroman> Currently the only real practical way to write programs is to write them in brainfuck and transate it.
16:57:24 <fizzie> You could instead just have the "turn left/right 90 degrees" instructions. Though of course "whatever".
16:57:41 <mroman> oh
16:57:42 <fizzie> It's going to make the brainfuck translation real boring, though.
16:57:43 <mroman> yeah
16:57:44 <elliott> fizzie: YOU CAN'T DENY THE TRUTH
16:58:14 <fizzie> elliott: I'm not going to even bother with the recursive "I'm not going to dignify that" stuff.
16:58:21 <mroman> hm
16:58:46 <elliott> fizzie: Why? Because your speech recognition software's stack would overflow?
16:59:22 <fizzie> *LAA LAA LAA NOT DIGNIFYING LAA LAA*
16:59:44 <mroman> Because then you can check for beam==0
16:59:50 <mroman> without having to bother about the store
16:59:54 <mroman> @boring
17:00:10 <mroman> Which would make the translation rather boring, indeed.
17:01:36 <elliott> Friendship: Hey how do you get a minimal LaTeX on Debian
17:01:47 <elliott> The smallest thing I could get apt to consider was about 150 megs :(
17:02:02 <Friendship> elliott: "Minimal" and "LaTeX" don't belong in the same sentence.
17:02:04 <mroman> hm
17:02:50 <elliott> Friendship: it was absolutely useless. Thanks
17:04:54 <oklopol> friendship is not useless, friendship is magic
17:06:09 <elliott> Need to get 32.7 MB of archives.
17:06:10 <elliott> After this operation, 73.8 MB of additional disk space will be used.
17:06:10 <elliott> Do you want to continue [Y/n]?
17:06:17 <elliott> Oh, that's not so bad, once I --no-install-recommends.
17:06:27 <elliott> I like how it depends on ed.
17:06:49 <elliott> Oh wait, I also need OCaml.
17:16:50 -!- MoALTz has joined.
17:19:17 -!- MoALTz__ has quit (Ping timeout: 244 seconds).
17:26:46 <mroman> http://fpaste.org/7hec/ <- whimp mode would allow this.
17:26:52 <mroman> (which reverses stdin)
17:27:31 <mroman> -h
17:27:45 <mroman> wimp like imp
17:34:30 <mroman> but that's to wimpy
17:34:40 <mroman> so I don't add that as a documented instruction :D
17:34:43 <mroman> *too
17:37:29 <fizzie> The example looks codeflowistically awfully overcomplicated; I mean, why not just http://p.zem.fi/pehr or something.
17:37:55 <elliott> http://p.zem.fi/pehr.beam
17:38:00 <elliott> WHAT NOW
17:38:11 <fizzie> I must fix that at time T.
17:38:16 <elliott> Shouldn't have dictated your code with Dragon NaturallySpeaking.
17:38:30 <mroman> I was experimenting so I did not really care about codeflow
17:38:40 <mroman> and yours loops forever
17:38:53 * elliott thinks this whimp thing sounds boring. (Also is it meant to be "whimp" rather than "wimp"?)
17:39:11 <mroman> is whimp a real word?
17:39:43 <fizzie> mroman: Where does it loop forever?
17:40:21 <mroman> My code sets memory[0] to zero
17:40:22 <elliott> Not... really: http://public.wsu.edu/~brians/errors/whimp.html
17:40:31 <mroman> since >`pn is basically looking for a zero cell
17:40:41 <mroman> if it finds a zero cell, it terminates
17:40:52 <mroman> you set memory[0] to whatever stdin[0] is.
17:41:00 <mroman> which leads to an endless loop
17:41:33 <fizzie> Oh, well, reorder the P and '; anyway. Also isn't >`pn looking for just cell where memory[i] == i?
17:41:44 <mroman> yes
17:41:47 <mroman> my mistake
17:44:02 <mroman> testing for store == 0 is not really practical
17:44:23 <mroman> as ( ) both reverse the control flow which is not that useful because you can't escape that
17:45:05 <mroman> although with x that is possible
17:46:38 <mroman> Beam sucks :(
17:46:56 <elliott> It does?
17:47:10 <elliott> It looks fun to me.
17:47:13 <fizzie> So it's some sort of a tractor beam then.
17:47:19 <mroman> :)
17:47:29 <elliott> By the way, / and \ could do with some... word-based descriptions.
17:47:37 <mroman> oh
17:47:38 <mroman> ok
17:47:47 <mroman> entry angle = exit angle?
17:47:53 <mroman> they work like mirrors
17:48:16 <elliott> Couldn't you just say "rotates the beam n degrees"?
17:48:26 <elliott> Uh, s/the beam/the control flow/.
17:48:39 <mroman> Yes.
17:48:52 <mroman> But I think those instructions are of no use anyway :)
17:49:18 <elliott> That's the spirit! Remove instructions instead of adding them :p
17:49:56 <mroman> The only working way to program is like the bf2beam.pl mechanism works
17:50:01 -!- tzxn3 has joined.
17:50:33 <mroman> as soon as you have to check beam == 0, store == 0 you're screwed ;)
17:50:42 <elliott> Well, you don't necessarily know it's the *only* way. :p
17:52:45 <fizzie> Yes, and you can certainly *do* things with ? and !, just as long as the thing you're doing is doable in a ping-pong-loopy way.
17:53:08 <mroman> ? and ! are useful instructions yes.
17:54:01 <elliott> @ask oerjan Is ():^ TC when limited to a certain depth of textual nesting of ()s?
17:54:01 <lambdabot> Consider it noted.
17:58:02 <mroman> oho
17:58:04 <mroman> it's looking good.
18:01:52 <mroman> ok. no.
18:05:43 -!- Vorpal has quit (Ping timeout: 276 seconds).
18:06:14 <mroman> ok
18:06:25 <mroman> I can store stdin in every odd cell.
18:07:35 <tswett> elliott: in addition to being my baby nephew, you are now an alien.
18:09:03 <elliott> Ah.
18:09:35 <elliott> @ask oerjan What about when the total number of ()s is limited?
18:09:35 <lambdabot> Consider it noted.
18:09:36 <mroman> hoho
18:15:16 <mroman> http://fpaste.org/V9nx/raw/
18:15:20 <mroman> ^- reverses stdin
18:15:23 <mroman> but never terminates :D
18:15:31 <elliott> pretty
18:22:39 <elliott> Dammit, prgmr want my money.
18:22:49 <mroman> http://fpaste.org/qpxo/raw/ <- and there it is
18:22:54 <mroman> terminating!
18:24:00 <mroman> the ? maybe useless there
18:24:25 <elliott> is that with whimp or without?
18:24:32 <mroman> without of course.
18:25:07 <mroman> yeah.
18:25:10 <mroman> the ? is a nop there
18:27:36 <mroman> http://fpaste.org/8xu0/raw/ <- cleaned up
18:28:01 <mroman> So. It is totally possible to write beam programs without bf2beam but sucks like hell :D
18:28:16 <mroman> hm
18:28:22 <elliott> happy australian mailman mailing list reminders day!
18:28:30 <mroman> that << is redundant maybe
18:29:15 <mroman> yes
18:29:31 <fizzie> My version was http://p.zem.fi/u8ld
18:31:01 <mroman> Nice.
18:31:48 <mroman> (`)
18:32:11 <mroman> that's the same as >`) if you prepare the store to be even/odd
18:32:16 <mroman> right?
18:32:59 <fizzie> Yes, it could be >`) there. I just used (`) since it's what I had in that bf2beam, and it looks sort-of more symmetric.
18:33:26 <fizzie> It's never going to go left anyway.
18:33:43 <fizzie> There's still quite a lot of rolling the store around.
18:34:25 -!- Phantom_Hoover has quit (Remote host closed the connection).
18:34:41 <mroman> Yours runs in 4068 cycle with my test stdin
18:35:48 <mroman> mine runs in 4319 cycles.
18:36:01 <mroman> Nice job.
18:36:28 <elliott> Fastarr.
18:36:50 <mroman> May I add your version also to the wikipage?
18:37:15 <fizzie> Sure, sure. Though it's not really very different.
18:37:47 <mroman> your output loop runs faster.
18:38:10 <mroman> H(`p@p`)H is probably faster than my circular loop
18:42:49 <fizzie> http://p.zem.fi/roto <- this version might be even faster, since it doesn't need to roll the store to 0 and back.
18:43:35 <mroman> wow
18:43:38 <mroman> 316 Cycles.
18:44:29 <elliott> 0 CYCLES
18:44:57 <elliott> fizzie: Hey, are you [[User:fizzie]] or [[User:Fizzie]]?
18:46:23 <fizzie> mroman: You can also write it a bit more compactly if you "bend" the vertical bit, as in http://p.zem.fi/lggf -- though that's probably a tiny bit slower since it has the \.
18:46:36 <fizzie> elliott: I don't really know. I think I might have an "F" there for some reason.
18:47:03 <elliott> fizzie: Well, yes, MW enforces that. But I can link to you as the lowercase version, if you want.
18:47:10 <mroman> fizzie: 342. It's a little bit slower, yes.
18:48:05 <fizzie> elliott: Oh. Well, I don't know, if the uppercased is the "official"-by-MW one, that one's fine too. (After all, I was in fact "Fizzie" once in IRC too.)
18:48:53 <mroman> that is pretty darn clever.
18:49:06 <elliott> fizzie: Well, it's not really official, in that [[User:fizzie]] works just fine and you can put {{lowercase}} on a page to make it show that way. But I'll go for the capital F then.
18:49:41 <fizzie> fungot: Would you prefer to be written in Beam? (No, I'm not planning a rewrite.)
18:49:42 <fungot> fizzie: so you want to do is press the keys, relaxed. apart from that
18:50:52 -!- augur has quit (Remote host closed the connection).
18:51:26 <elliott> fizzie: Oh, I see you linked yourself as F on the page itself.
18:53:11 <fizzie> Mmmaybe. I probably didn't think the lowercase would work. But I don't hold that firm onions on the spelling.
18:53:50 <elliott> Graue linked to me as [[User:Ehird]] and it hurt. :(
18:55:45 <mroman> I'm going to change unknown computional class to turing-complete for Beam.
18:56:09 <mroman> *computational
18:56:18 <elliott> That seems reasonabible, given fizzie's conversator.
18:56:26 <elliott> Aaargh, his typos are infecting me again.
18:57:23 <mroman> I'm not a native speaker, I have an excuse!
18:58:30 <elliott> No, I mean fizzie's.
18:58:42 <elliott> Whenever he talks I start talking like him.
18:59:27 <fizzie> I speak the king's standomatic English, don't be all flubflub about it.
18:59:34 <olsner> hmm, I fixed functions recursing to themselves using an ugly hack, but that hack does nothing to allow two mutually recursive functions (eval and apply, say)
18:59:51 <elliott> olsner: sounds like you have TRE but want TCO?
18:59:52 <elliott> olsner: sounds like you have TRE but want TCO?
18:59:54 <elliott> Oops.
18:59:58 <elliott> Oh well, a few more times, then.
18:59:59 <elliott> olsner: sounds like you have TRE but want TCO?
18:59:59 <elliott> olsner: sounds like you have TRE but want TCO?
19:00:00 <elliott> olsner: sounds like you have TRE but want TCO?
19:00:03 <olsner> it's retardolisp
19:00:42 <mroman> standomatic?
19:00:51 <fizzie> It's like standard, except more so.
19:00:56 <olsner> elliott: no, none of those, I'm talking about the basic ability to even call the function
19:01:07 <elliott> mroman: (It's also not a word, to clarify.)
19:02:49 <elliott> Hey fizzie, can I delegate the making of this esolang to you, now that I've thought of it?
19:04:13 -!- sebbu has quit (Ping timeout: 276 seconds).
19:04:32 <olsner> I think I'll just go ahead and build a heap-like thing that I can pass around and mutate stuff inside
19:04:35 <fizzie> Probably not. I don't get things done.
19:05:09 -!- Taneb has joined.
19:05:14 <elliott> fizzie: LIKE EDITING THE GRASP PAGE, EH
19:05:21 <Taneb> Hello!
19:06:56 <elliott> "Creys" -- fizzie
19:09:26 -!- sebbu has joined.
19:09:27 -!- sebbu has quit (Changing host).
19:09:27 -!- sebbu has joined.
19:20:10 -!- augur has joined.
19:36:18 <fizzie> mroman: Incidentally, if you wanted to wimp-mode things up without adding any instructions, you could just modify u/n to test "beam != mod(store,256)" instead of "beam != store". That would make the brainfuck aaa[bbb]ccc translation pretty trivial:
19:36:22 <fizzie> aaa >Ln+Lp! bbb v> ccc
19:36:24 <fizzie> > ^
19:36:27 <fizzie> ^ <
19:36:35 <fizzie> But it's of course a cheat as much as the x.
19:37:04 -!- sebbu2 has joined.
19:37:04 -!- sebbu2 has quit (Changing host).
19:37:04 -!- sebbu2 has joined.
19:40:25 -!- sebbu has quit (Ping timeout: 256 seconds).
19:40:25 -!- zzo38 has joined.
19:41:48 <elliott> 4jkgjior
19:44:44 -!- Ngevd has joined.
19:45:29 -!- Taneb has quit (Ping timeout: 272 seconds).
19:46:57 <mroman> fizzie: Why @trivial
19:47:10 <mroman> to test for zero you have to set store to 256*n?
19:47:29 <mroman> you'd use every 256th cell?
19:49:55 <fizzie> No, you can just do it like above.
19:50:30 <fizzie> Use Ln+Lp to do "come from left, go down if beam is zero, continue right if nonzero".
19:51:19 <fizzie> (After L, beam == mod(store,256) always so it won't go down when hitting the n from the left; after L+, beam != mod(store,256) always, so it will go down when hitting the n from the right.)
19:51:36 <fizzie> Sorry, I mean Ln+Lp!, of course.
19:51:44 -!- sebbu3 has joined.
19:51:44 -!- sebbu3 has quit (Changing host).
19:51:44 -!- sebbu3 has joined.
19:52:36 <zzo38> People argue about time paradixes and that stuff in [[Talk:TwoDucks]] esolang wiki article
19:52:42 <zzo38> s/paradixes/paradoxes/
19:52:48 <mroman> yes @L
19:52:49 <mroman> but
19:52:56 <mroman> you wan't to test for beam == zero
19:53:42 <mroman> oh
19:53:46 <mroman> interesting :)
19:54:55 <mroman> beam = (store % 256); if (beam != (store % 256)) { go down }
19:55:11 -!- sebbu2 has quit (Ping timeout: 252 seconds).
19:55:29 <mroman> beam++; beam = memory[store]; if(beam != 0) { reverse }
19:55:50 <fizzie> You missed the second L.
19:55:57 <fizzie> After beam++.
19:56:15 <mroman> why do you increment beam if you just reload it an instruction later?
19:56:25 <fizzie> It's for when we're going backwards.
19:56:52 <fizzie> The n+L bit, when hit from the right, will always go down on the n.
19:57:26 <fizzie> Since ((store % 256) + 1) != (store % 256).
19:57:31 <mroman> Oh.
19:57:34 <mroman> Now I see it.
19:58:18 <mroman> That would enable one to detect reversing?
19:58:29 <fizzie> Yes.
19:58:30 <mroman> In general.
19:58:37 <mroman> Too cheaty ;)
20:00:12 <mroman> BeaWImP :D
20:04:20 -!- Ngevd has changed nick to Taneb.
20:05:39 <Taneb> Salom is weird
20:05:44 <Taneb> The play, that is
20:06:15 <Friendship> Salami is weird.
20:06:20 <Friendship> The sausage, that is.
20:10:16 <fizzie> Salade is weird.
20:10:21 <fizzie> The helmet, that is.
20:11:33 <ion> Salad Fingers is great.
20:14:41 -!- Taneb has quit (Ping timeout: 265 seconds).
20:17:47 -!- oerjan has joined.
20:19:12 <elliott> hi oerjan
20:19:50 <oerjan> @messages
20:19:50 <lambdabot> elliott asked 2h 25m 47s ago: Is ():^ TC when limited to a certain depth of textual nesting of ()s?
20:19:51 <lambdabot> elliott asked 2h 10m 13s ago: What about when the total number of ()s is limited?
20:19:53 <oerjan> hi
20:20:29 <oerjan> to the first, i should think so since any given TM has a limit and there are universal TMs
20:20:35 <olsner> oerjan and elliott, synchronized at last
20:20:52 <olsner> well, temporarily at least
20:21:13 <elliott> oerjan: approaching fancy-L, there
20:21:23 <fizzie> oerjan: Have you, or have you not, been swapped with an alien changeling thing?
20:21:35 <oerjan> to the second, well you can do an arbitrary large unary with only :'s, so i think so
20:21:54 <oerjan> um s/TM/minsky machine/g
20:22:01 <elliott> but i suppose you just need to prefix the program with (interp of another TM)*...
20:22:17 <oerjan> fizzie: if i have they did in a very amnesiac fashion
20:22:25 <fizzie> oerjan: O kay. It's just that I've heard rumours of an "oerjanswap".
20:22:51 <oerjan> *did it
20:23:06 <oerjan> fizzie: yes. i think ais523 invented that name.
20:23:19 <oerjan> in other news, i've been lately looking at Qdeql.
20:24:00 <elliott> you think it's TC? :P
20:24:09 <oerjan> YOU KNOW ME TOO WELL
20:26:26 <oerjan> (that's a yes.)
20:27:53 <elliott> I gathered.
20:29:31 <oerjan> hm i was going for finite length tape brainfuck but i've suddenly seen that a tape of bytes may not be much harder...
20:31:06 <elliott> oerjan: my idea about :()^ was that, you could fix the structure
20:31:17 <elliott> in that, if a certain fixed structure of ()s suffices for TCness, you don't actually need the ()s
20:31:25 <elliott> so it could be "tarpitted" in a way
20:31:37 <elliott> (and the result might be useful for proving languages TC, since it's so simple)
20:32:19 <oerjan> wat
20:32:29 <elliott> what
20:35:17 <elliott> no seriously, what
20:35:18 <oerjan> i'm not sure if what you're saying is trivial or not :P
20:37:04 <elliott> I don't know what you mean
20:38:58 <oerjan> i mean that you have not actually described your idea
20:39:23 <oerjan> or maybe i should read the logs
20:39:37 <elliott> oerjan: well the idea wasn't complete, obviously...
20:39:47 <elliott> I just meant that if :()^ with a fixed structure of ()s
20:39:48 <elliott> i.e.
20:39:54 <elliott> (hole(hole)hole)hole or whatever
20:39:58 <elliott> was TC, then you could omit the structure entirely
20:40:00 <elliott> hole/hole/hole/hole
20:40:14 <elliott> and maybe it could be simple enough to end up as a tarpit (so you could have a much simpler structure than fully-nested parens and the like)
20:40:20 <elliott> which would make it useful for proving ultra-simple languages TC
20:40:22 <oerjan> how could you do that.
20:41:04 <elliott> ...excuse me for thinking about an idea before i have every single concrete detail down.
20:41:12 <oerjan> OKAY
20:41:17 <elliott> i'll make sure to have a full program skeleton next time
20:41:18 <elliott> sheesh
20:41:49 <oerjan> it's just that it seems to me that such a thing would be very hard to do without a and *
20:42:10 <elliott> what, why?
20:43:10 <oerjan> because one of the properties of :()^ is that you cannot really get below the upper element without destroying it. in particular, you cannot copy more than one element on the stack.
20:43:16 -!- monqy has joined.
20:43:27 <oerjan> *top element
20:43:53 <elliott> i don't think you understand my idea
20:44:01 <oerjan> well naturally not.
20:44:08 <elliott> it's simply to fix the nesting structure of the ()s
20:44:19 <elliott> say you can translate every TM to something of the form
20:44:27 <elliott> (anything)(anything(anything))anything
20:44:31 <elliott> where anything isn't allowed to contain ()s
20:44:34 <elliott> (and is a different anything each time, obviously)
20:44:38 <elliott> then you don't actually need to include the ()s
20:44:44 <elliott> you can encode it as [anything,anything,anything,anything]
20:44:48 <oerjan> oh, so it's just a different syntax?
20:44:49 <elliott> which removes nesting from the program structure
20:45:03 <elliott> oerjan: well yes, but the idea would be to make it so that you can implement it without actually caring about the nesting...
20:45:20 <elliott> the point is that :()^ is very close to something like BCT in terms of how simple its operations are
20:45:30 <elliott> except for requiring the juggling of nesting
20:45:31 <oerjan> well fine, you're welcome to try.
20:49:22 <mroman> chickenz: How are you coming along with the python interpreter?
20:50:19 -!- Phantom_Hoover has joined.
20:51:23 -!- ais523 has joined.
20:51:42 <ais523> hi people
20:51:46 <ais523> hey persons
20:51:55 <monqy> hi
20:52:21 <ais523> I've been learning OCaml polymorphic variants
20:52:40 <ais523> which are about halfway to Anarchy, and thus cut out about half the boilerplate in compilers
20:52:43 <ais523> while improving type safety
20:52:46 <ais523> it's nice
20:53:21 <ais523> also, I've been trying them out on typed Underload, it really demonstrates exactly what OCaml's type system's deficiencies are
20:54:06 <ais523> happy australian mailman mailing list reminders day!
20:54:17 <elliott> beat you to it
20:54:20 <zzo38> What are those deficiencies?
20:55:13 <ais523> zzo38: let x = q(4) in x // x doesn't do the same thing as q(4) // q(4)
20:55:50 <ais523> (q(4) does the same thing as (4) in Underload, it's just in a different syntax)
20:55:55 <elliott> ais523: because of strictness?
20:56:05 <ais523> elliott: because the first requires both 4s to be pushed onto the same type of stack
20:56:06 <elliott> you can't expect that property in a strict languae
20:56:10 <elliott> *language
20:56:13 -!- Taneb has joined.
20:56:16 <elliott> ais523: oh, that's not really a deficiency
20:56:21 <ais523> which thus constrains the stack to be made entirely out of ints
20:56:24 <Taneb> Hello
20:56:26 <elliott> ais523: realise that the same applies to lambda parameters
20:56:31 <elliott> (\x -> x // x) (q(4))
20:56:33 <ais523> elliott: that's a deficiency too!
20:56:48 <elliott> ais523: i believe you will find fixing that makes the whole thing undecidable.
20:56:54 <elliott> oerjan wrote something about that once iirc.
20:57:00 <ais523> hmm, interesting
20:58:38 <elliott> oerjan: that is your cue to link to it.
21:00:03 <Taneb> The people designing Windows must have thought: "Who has customers that we don't!? Oooh, some people use Ubuntu! Why are they successful... hmm, they just changed there default GUI and made it weird! We can do that /even better/"
21:00:12 <ais523> elliott: I thought you might be able to make it decidable by, rather than working out the types in the abstract, working them out on demand
21:00:39 <ais523> Taneb: I consider the whole Gnome 3 / Unity / Windows 8 fiasco as proof that Windows not only copies Linux distributions' good ideas, but also their bad ideas
21:00:54 <elliott> ais523: yes, that is called dynamic typing
21:01:06 <ais523> elliott: but calculated at compile time
21:01:18 <ais523> this clearly works with dynamic typing, the challenge is to make it work with static typing too
21:01:20 <elliott> true, it probably works if you make it a contradiction
21:02:30 <ais523> Minix 3.2 released? people are still working on that?
21:02:38 <ais523> (main change: they replaced their userland with BSD's)
21:02:54 <oerjan> elliott: i don't think i wrote anything major, but it did come up regarding Chris Diggins's Cat language. iirc it's undecidable to determine whether a set of word concatenation equations are solvable, which is what you need to type a stack language flexibly.
21:04:14 <oerjan> i think cdiggins decided to make Cat less polymorphic to avoid that quagmire.
21:04:31 <elliott> oerjan: i was referring to your SO answer
21:04:36 <elliott> i believe
21:05:37 <oerjan> oh that was for lambda calculus. and the undecidability is just an obvious detail (because getting that kind of type for a term proves it halts.)
21:06:31 <elliott> yes, but ais523 is talking about ML.
21:06:35 <elliott> so lambda calculus is relevant
21:07:03 <oerjan> well yes. but the word problem is much more directly relevant to why stacks mess things up.
21:07:09 <elliott> he is complaining that "let x = y in e" is not the same as e[x := y]
21:07:11 <ais523> well, Anarchy isn't ML, I've just been using OCaml and Haskell to try it out
21:07:16 <elliott> because x is forced to have the same type for all uses in e
21:07:26 <elliott> so he's not really talking about stacks.
21:07:33 <elliott> except that he's using some stack combinators he made to complain about it
21:07:34 <ais523> right, indeed
21:07:39 <ais523> stacks are just one possible application
21:07:44 <ais523> they're not even the main one
21:07:52 <oerjan> elliott: actually let x = y in e _is_ the same as e[x := y]. it's not the same as (\x -> e) y, though.
21:08:18 <oerjan> iirc
21:08:23 <elliott> oerjan: well not in OCaml.
21:08:27 <ais523> oerjan: oh, I was referring to the usual desugaring of let in terms of lambdas
21:08:35 <elliott> oerjan: I think that's true for Haskell, though
21:08:39 <oerjan> elliott: hm doesn't ocaml let give polymorphism?
21:08:40 <ais523> and I think OCaml does that too, either explicitly or effectively
21:08:50 <elliott> oerjan: note that recent GHC don't generalise let by default nowadays
21:08:52 <elliott> *GHCs
21:08:57 <ais523> oerjan: it gives the '_a types that collapse when you use them once
21:09:05 <ais523> if you don't specify an argument
21:09:17 <ais523> I think let x eta = y eta in e gives you a polymorphic let
21:09:30 <ais523> I've been adding etas all over the place for that reason
21:09:48 <oklopol> so any ppl here from spain?
21:10:02 <oklopol> i'm having this conference next week there
21:10:12 <oerjan> that's sort of a point of hindley-milner, and my "iirc" is that its let polymorphism gives precisely the same typing as substituting the definition at every use. i vaguely think recursion may mess that up though.
21:10:21 <oerjan> *+damas-
21:10:36 <oklopol> i will buy a beer to anyone who shows up and gives sufficient proof of #eso regularity
21:11:04 <oklopol> oerjan: oerjanswap is awesome
21:11:21 <Taneb> oklopol, what's the conference on?
21:11:24 <ais523> oerjan: IIRC damas-milner is the inference algo, hindley-milner is the type system, right?
21:11:34 <oerjan> ais523: hm not sure.
21:11:37 <oklopol> "iirc it's undecidable to determine whether a set of word concatenation equations are solvable, which is what you need to type a stack language flexibly." actually that's solvable
21:11:48 <oklopol> but we can't actually give the solutions
21:12:03 <oklopol> Taneb: http://grammars.grlmc.com/lata2012/Program.php
21:12:07 <ais523> I thought it was just NP-hard, rather than unsolvable
21:12:10 <oklopol> it's on stuff
21:12:45 <elliott> ais523: "The origin of this algorithm is the type inference algorithm for the simply typed lambda calculus, which was devised by Haskell Curry and Robert Feys in 1958. In 1969 J. Roger Hindley extended this work and proved that their algorithm always inferred the most general type. In 1978 Robin Milner,[2] independently of Hindley's work, provided an equivalent algorithm, Algorithm W. In 1982 Luis Damas[1] finally proved that Milner's algorithm i
21:12:45 <elliott> s complete and extended it to support systems with polymorphic references."
21:12:51 <elliott> "In type theory, Hindley–Milner (HM) (also known as Damas–Milner or Damas–Hindley–Milner)"
21:13:00 <oerjan> ais523: anyway i think your idea of solving types on demand corresponds to keeping around such word equations as a (possibly undecidable) constraint problem.
21:13:21 <ais523> oerjan: hmm, seems about right
21:13:35 <ais523> actually, I'd be very surprised if Anarchy's type system /were/ generally decidable, you'd expect it to be TC
21:13:47 <ais523> what's more important is being decidable when it's actually used in practice
21:14:07 <elliott> I love it when I use the compiler in a way ais523 doesn't expect me to, and the compiler loops forever.
21:14:29 <ais523> elliott: can you or can't you do infinite loops in the type system in Haskell or C++?
21:14:38 <ais523> Anarchy's type system is /more/ powerful than those, so you'd expect it to have the same property
21:14:51 <oerjan> <ais523> stacks are just one possible application <-- hm ok
21:15:30 <elliott> ais523: No, and I don't know.
21:15:48 <oerjan> <elliott> oerjan: note that recent GHC don't generalise let by default nowadays <-- only when certain extensions are in effect iirc
21:15:52 <ais523> you can embed lambda calculus in Haskell's type system, can't you?
21:16:04 <elliott> oerjan: no
21:16:08 <elliott> by default
21:16:13 <elliott> ais523: No.
21:16:26 <oklopol> http://books.google.fi/books?id=x3P0fb8GMyYC&pg=PA44&lpg=PA44&dq=makanin+1976&source=bl&ots=8FLRGaXetI&sig=2jHBYF_uDGrtdsBY0TuLZ52mdl8&hl=fi&sa=X&ei=hZVOT-bLENOK4gTPyNjuAg&ved=0CB4Q6AEwAA#v=onepage&q=makanin%201976&f=false
21:16:31 <oklopol> oerjan: ^
21:16:32 <ais523> hmm
21:16:41 <mroman> I thought lc has no type system.
21:16:57 <oerjan> <ais523> oerjan: it gives the '_a types that collapse when you use them once <-- oh right, the value restriction (only slightly similar to haskell's monomorphism restriction)
21:16:59 <ais523> mroman: right, untyped LC doesn't, but that doesn't mean you can't use a type system to implement it
21:17:17 <mroman> Ah. That way. Ok.
21:17:48 <oerjan> <oklopol> oerjan: oerjanswap is awesome <-- thanks
21:18:00 <ais523> hmm, I should see if I can work out exactly why :> exists in OCaml
21:18:05 <ais523> something to do with soundness of the type system
21:18:51 <Taneb> oerjanswap?
21:19:00 <elliott> oerjan: click oklopol's link btw
21:19:02 <oerjan> <oklopol> but we can't actually give the solutions <-- oh. well i guess you don't need the solutions just to prove it's safe to run a program.
21:19:05 <oklopol> and apparently the problem is known to be in PSPACE as of 2004, this i was not familiar with
21:19:23 <oklopol> elliott: why would he not see my link_
21:19:24 <oklopol> ?
21:19:27 <elliott> oh you're up in the backlog
21:20:04 <ais523> Taneb:
21:20:15 <oklopol> we did the case where each variable occurs at most twice on a course, but i think makanin's result is considered rather deep
21:20:17 <ais523> aa((!((aa)(!))))*:*^!**^a*^a*aa*(*:*^!**^)*^
21:20:18 <oklopol> i haven't read it
21:21:13 <oklopol> lol i just noticed the guy who wrote that chapter also gave the course i was on :D
21:21:37 <oklopol> (he's a famous word equationist)
21:22:18 <oerjan> <elliott> by default <-- erm http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#mono-local-binds disagrees.
21:22:36 <oerjan> or is that _very_ recent.
21:23:44 <elliott> huh.
21:23:47 <elliott> "Here's the rule. With -XMonoLocalBinds (the default), a binding without a type signature is generalised only if all its free variables are closed."
21:23:49 <elliott> -- http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
21:24:08 <ais523> so what exactly is the monomorphism restriction in Haskell?
21:24:16 <oklopol> so will no one come to spain with me?
21:24:19 <oklopol> :(
21:24:29 <elliott> ais523: top-level bindings with no arguments are forced to have a monomorphic type
21:24:35 <mroman> to?
21:24:49 <elliott> ais523: see http://www.haskell.org/onlinereport/decls.html#sect4.5.5
21:24:53 <ais523> elliott: hmm, OK, that's pretty much exactly the same as OCaml
21:25:00 <oklopol> "to?"?
21:25:00 <ais523> you can work around it simply via eta expansion, right?
21:25:15 <ais523> (and unlike in OCaml, eta-expansion doesn't even change the meaning of a program in Haskell)
21:25:15 <oerjan> <elliott> oerjan: click oklopol's link btw <-- the abstract looks speculative. (also i don't feel like reading the rest.)
21:25:24 <fizzie> ais523: I have a reasonably strong belief that there's LC (as well as direct Turing machine simulators) done in C++ templates. Of course most compilers tend to run into some template recursion depth limits in practice.
21:25:34 <elliott> ais523: you can work around it just by specifying a type signature
21:25:35 <oklopol> oerjan: just the specific place i link
21:25:41 <elliott> ais523: and no, eta-expansion changes meaning in haskell
21:25:53 <ais523> hmm, even on things with function types?
21:25:57 <elliott> ais523: yes
21:25:58 <ais523> (obviously you can't eta-expand arbitrary types)
21:26:00 <elliott> seq undefined ()
21:26:02 <ais523> oh, because of _|_
21:26:03 <elliott> seq (\() -> undefined) ()
21:26:15 <mroman> oklopol: To spain to what?
21:26:18 <ais523> I am having an increasing urge to make Anarchy total
21:26:27 <oklopol> mroman: to have a beer with me
21:26:33 <elliott> ais523: you don't need totality to fix that.
21:26:34 <oklopol> oerjan: also what abstract? :D
21:26:37 <ais523> because it really doesn't need to be able to do infinite loops, and totality makes things so much simpler
21:26:42 <ais523> elliott: right, it'd be to fix other things too
21:26:59 <ais523> I've just sat through several weeks of seminars on when exactly eta-expansion works and when it doesn't
21:27:04 <zzo38> What is this Anarchy?
21:27:13 <elliott> ais523: note that haskell 1.4 did not have this issue.
21:27:48 <oerjan> oklopol: oh wait i read the abstract for the first article. that thing is too long to even _find_ what article you really wanted me to see.
21:27:57 <ais523> right, it's because seq combined with _|_ together expose the concept of how far something's been forced
21:28:15 <elliott> ais523: what
21:28:19 <elliott> that's nonsense
21:28:25 <oerjan> also please stop trying to make me use my brain, i have a headache and i need to eat WAAAAAAAAAAAAAAA
21:28:30 <oklopol> oerjan: doesn't it directly give you the line that states the relevant result?
21:28:34 <elliott> oklopol: it does for me.
21:28:39 <Taneb> <zzo38> What is this Anarchy? <-- I want to know too, ais523
21:28:41 <elliott> oerjan uses a shitty browser though so maybe it's broken for him
21:28:45 <oklopol> also see Problem 4, what the fuck >D
21:28:53 <ais523> Taneb: basically, WIP language, arguably esolang, arguably serious
21:28:55 <oklopol> i will so solve that tomorrow
21:28:56 <ais523> which is designed for writing compilers
21:29:05 <Taneb> Link?
21:29:09 <ais523> and has a static type system that's designed to allow you to do as much as possible
21:29:12 <ais523> and no link, it's a WIP
21:29:22 <oklopol> oerjan: page 44
21:29:23 <Taneb> Ah
21:29:24 <ais523> it's half sugar, half crazy typing
21:29:27 <elliott> the fix is simply
21:29:32 <ais523> hmm, I have an Anarchy program open atm, I'll paste it
21:29:35 <elliott> class Eval a where seq :: a -> b -> b
21:30:13 <ais523> http://sprunge.us/iQMG
21:31:31 <ais523> note: I am far from certain that "let compose a = | _ -> (compose_lambda a)" is correct
21:31:35 <ais523> I need to think about it more
21:31:47 <elliott> that program is unreadable
21:32:20 <oerjan> <ais523> elliott: hmm, OK, that's pretty much exactly the same as OCaml <-- um the haskell version only applies when there are _type class_ constraints. this is because such constraints are essentially passed as hidden dictionary parameters, and the report people decided they didn't want to let that happen stealthily because it makes values potentially unshared without a syntactic clue.
21:32:27 <ais523> I think it possibly actually should be "let compose a = | _ -> _ = (compose_lambda a _)", which would require a syntax extension
21:33:13 <ais523> (the current code is equivalent to "let compose a = | _ -> _ = (compose_lambda a) _", which looks the same to people who are used to the existence of currying, but Anarchy doesn't do currying)
21:33:15 <oerjan> <ais523> (and unlike in OCaml, eta-expansion doesn't even change the meaning of a program in Haskell) <-- except if you use seq.
21:33:30 <ais523> oerjan: right, elliott corrected me on that already
21:33:48 <ais523> elliott: what don't you like about it? I already changed the parser to allow = | to be sugared into just =
21:35:01 <oerjan> <oklopol> oerjan: just the specific place i link <-- oh hm. this _might_ be hitting a bug i've sometimes seen where IE doesn't find link anchors in large documents.
21:35:33 <ais523> just unfamiliarity?
21:35:48 <ais523> so far, wrt implementing Anarchy, I have just a parser
21:35:54 <ais523> and I've been compiling it to OCaml and Haskell by hand
21:36:42 <ais523> one nice thing I discovered is that it's possible to retrofit polymorphic variants onto statically-typed languages that don't have them, so long as they have first-class functions and tuples
21:36:56 <elliott> oerjan: google docs overrides the anchor-handling with js anyway i would assume
21:36:58 <oerjan> <oklopol> oerjan: page 44 <-- ok, found it
21:37:06 <zzo38> I have written some idea too, about some programming language codenamed "Ibtlfmm", where the type system includes implementation of mathematical laws of classes
21:37:13 <elliott> <oerjan> <ais523> elliott: hmm, OK, that's pretty much exactly the same as OCaml <-- um the haskell version only applies when there are _type class_ constraints. this is because such constraints are essentially passed as hidden dictionary parameters, and the report people decided they didn't want to let that happen stealthily because it makes values potentially unshared without a syntactic clue.
21:37:16 <elliott> oerjan: untrue.
21:37:20 <elliott> foo = undefined
21:37:23 <elliott> will be defaulted to ()
21:37:24 <elliott> i believe
21:37:31 <elliott> <ais523> elliott: what don't you like about it? I already changed the parser to allow = | to be sugared into just =
21:37:34 <elliott> it's impossible to scan
21:37:43 <ais523> it's easier than Haskell!
21:37:49 <elliott> no, it's not
21:37:53 <elliott> also, "(f a) b" is hideous
21:37:58 -!- azaq23 has joined.
21:38:03 <ais523> elliott: it's for clarity
21:38:07 <elliott> it's ugly
21:38:11 -!- azaq23 has quit (Max SendQ exceeded).
21:38:20 <Phantom_Hoover> What's ais523 doing?
21:38:22 <elliott> let compose a = | _ -> (compose_lambda a)
21:38:22 <elliott> that can't be for clarity, that's just nonsense
21:38:35 <ais523> elliott: that's already the line I said I thought was wrong
21:38:41 <Taneb> Phantom_Hoover, making a semi-esoteric language for constructing compilers
21:38:46 <ais523> ignore that one
21:38:51 <ais523> it parses, but I think it means the wrong thing
21:38:56 -!- azaq23 has joined.
21:39:05 -!- azaq23 has quit (Max SendQ exceeded).
21:39:16 <ais523> also, I'm considering allowing "| _ ->" to be sugared out entirely if it's the only term, but I think that might be more confusing than useful
21:39:35 <elliott> it would be a lot more readable if you put the multi-clause definitions on to multiple lines
21:39:46 -!- azaq23 has joined.
21:39:46 <ais523> yep, nothing stopping you putting newlines there if you like
21:40:00 <ais523> there's only one multiple-clause definition there, though
21:40:01 <elliott> yes, but you didn't
21:40:05 <ais523> (emptycheck)
21:40:16 <ais523> elliott: how is this a criticism of the language?
21:40:59 <Taneb> Well, goodnight
21:41:00 -!- Taneb has quit (Quit: Goodbye).
21:41:27 <elliott> ais523: i don't recall saying "this language is unreadable"
21:41:39 <ais523> ah, OK
21:41:50 <ais523> shall I put some newlines in logical places and see if you think it looks any better?
21:42:18 <elliott> perhaps. by multiple clause I actually meant "containing a semicolon"
21:43:34 <ais523> I'm newlining those too
21:44:14 <ais523> you know what? I'm going to add new syntax for closure creation, it's too confusing without it
21:45:04 <ais523> http://sprunge.us/diPZ
21:45:53 <elliott> needs blank lines between definitions
21:45:55 <elliott> but it's a lot better
21:45:59 <oerjan> <elliott> "Here's the rule. With -XMonoLocalBinds (the default), [...]" <-- i see that, but everything else on that page seems to disagree with the "(the default)".
21:46:08 <elliott> oerjan: yes, indeed
21:50:18 <ais523> elliott: anyway, I find the newlined version less readable because of the need for more vertical scrolling
21:51:09 <oerjan> <elliott> oerjan: untrue. <elliott> foo = undefined <elliott> will be defaulted to () <-- no, i'm pretty sure that is wrong.
21:51:17 <elliott> hmm
21:51:19 <elliott> ok
21:51:37 <ais523> :t foo = undefined
21:51:37 -!- derdon has joined.
21:51:37 <lambdabot> parse error on input `='
21:51:41 <ais523> hmm
21:51:46 <ais523> :define foo = undefined
21:51:53 <ais523> @define foo = undefined
21:52:01 <elliott> inb4 <ais523> haskell is unusable!
21:52:09 <ais523> elliott: nah, this is just a lambdabot thing
21:52:32 <ais523> Prelude> let foo = undefined
21:52:32 <elliott> hint: it uses the same syntax as haskell
21:52:33 <ais523> Prelude> :t foo
21:52:34 <ais523> foo :: a
21:52:43 <elliott> GHCi is unreliable
21:52:47 <elliott> in that it uses different defaulting rules
21:53:25 <ais523> @let foo = undefined
21:53:26 <lambdabot> Defined.
21:53:29 <ais523> :t foo
21:53:30 <lambdabot> forall a. a
21:53:33 <elliott> lambdabot is unreliable too.
21:53:38 <elliott> it uses several extensions
21:53:42 <ais523> indeed
21:54:02 <ais523> Prelude> foo foo
21:54:03 <ais523> *** Exception: Prelude.undefined
21:54:05 <ais523> interesting
21:54:41 <ais523> :t \x -> x x
21:54:42 <lambdabot> Occurs check: cannot construct the infinite type: t = t -> t1
21:54:42 <lambdabot> Probable cause: `x' is applied to too many arguments
21:54:42 <lambdabot> In the expression: x x
21:54:47 <ais523> :t let x = undefined in x x
21:54:48 <lambdabot> forall t. t
21:55:07 <ais523> I'm getting the same result in ghci
21:55:14 <oerjan> indeed foo foo cannot possibly type in haskell unless foo is polymorphic
21:55:18 <ais523> although I can agree that neither might be reliable
21:55:28 <ais523> oerjan: that's why I'm using it as a test of polymorphism
21:55:30 <elliott> yes, let x = undefined in x x works
21:55:32 <oerjan> ais523: i think to satisfy elliott you need to put foo = undefined in a module.
21:57:11 <elliott> i'm not sure you remember the part where i conceded.
21:57:14 <ion> Hmm, how *does* the “x x” work? What’s the inferred type of x in that case?
21:57:22 <elliott> ion: forall a. a
21:57:29 <ion> @type let x = undefined in x `asTypeIn` \y -> y y
21:57:30 <lambdabot> Occurs check: cannot construct the infinite type: a = a -> b
21:57:30 <lambdabot> Probable cause: `y' is applied to too many arguments
21:57:30 <lambdabot> In the expression: y y
21:57:39 <oerjan> ion: a -> a for the first x and a for the second
21:58:04 <ais523> :t asTypeIn
21:58:04 <lambdabot> forall a b. a -> (a -> b) -> a
21:58:24 <ais523> hmm, I can't tell what that does from the type signature
21:58:43 <oerjan> :t asTypeOf -- i think you mean this one
21:58:43 <elliott> asTypeIn = const
21:58:44 <lambdabot> forall a. a -> a -> a
21:58:47 <ion> > let f = show in f f
21:58:48 <lambdabot> Overlapping instances for GHC.Show.Show (a -> GHC.Base.String)
21:58:48 <lambdabot> arising f...
21:59:55 <ais523> so astypein asserts that its first argument is a valid argument to its second argument?
21:59:56 <oerjan> > f (f :: Expr) :: Expr
21:59:57 <lambdabot> f f
22:00:01 <ais523> and then returns it?
22:00:07 <elliott> there is no "assert"
22:00:18 <elliott> asTypeIn takes parameters as per its type signature.
22:00:22 <elliott> it returns the first and ignores the second
22:00:30 <oerjan> @hoogle asTypeIn
22:00:31 <lambdabot> No results found
22:00:37 <ais523> elliott: I'm thinking along the lines of "static assertion"
22:00:39 <ion> @src asTypeIn
22:00:40 <lambdabot> a `asTypeIn` f = a where _ = f a
22:00:40 <lambdabot> infixl 0 `asTypeIn`
22:00:43 <ais523> i.e. forcing something to be true at compile time
22:00:50 <ais523> all type annotations are those, but it's a more general term
22:00:51 <elliott> ais523: it is not used as an assertion, it is used for unification
22:01:19 <ais523> well, err, right
22:01:25 <ais523> I keep forgetting that compilers aren't sufficiently smart yet
22:01:46 <elliott> what
22:02:26 <ais523> gah, seriously, you consider this newlined Anarchy program more readable than the original?
22:02:41 <ais523> I can hardly read it, not dense enough, and it moves too much vertically
22:02:43 <ais523> let me try something else
22:02:52 <elliott> ais523: it's not readable, no
22:02:57 <elliott> it still needs the newlines between definitions which you did not add
22:05:15 <ais523> that'd be even worse!
22:05:18 <ais523> OK, here we go: http://sprunge.us/MdUD
22:05:27 <ais523> using horizontal rather than vertical whitespace
22:07:36 <ais523> there's no way that program's more readable if it takes up an entire two vertical screenfuls
22:07:38 <elliott> less readable than the original
22:07:40 <elliott> it's not a spreadsheet.
22:07:43 <ais523> as you have to keep scrolling to see it at all
22:08:05 <ais523> probably needs more space around the ->
22:08:10 <ais523> but apart from that, I like this syntax
22:08:14 <ais523> err, this spacing
22:08:38 * ais523 is coming to think that elliott's and eir own spacing preferences, for things in general not just programming languages, are fundamentally incompatible
22:09:04 <elliott> the problem is that you're wrong about everything and I'm right about everything
22:09:21 <oklopol> EVERYTHING
22:10:09 <ais523> oklopol: so what's your opinion on this formatting question?
22:11:07 <oklopol> my opinion on everything atm is that i wonder whether finite nontrivial posets can be the language poset of a 2D SFT
22:12:09 <oklopol> i think it applies well enough here
22:12:42 <oklopol> also i think both look nice
22:12:59 <ais523> I think that given that Anarchy doesn't do currying, I like explicitly doing "f ?" to mean "fun x -> f x"
22:15:03 <elliott> how is that distinct from f?
22:16:06 -!- Goosey has joined.
22:17:15 <ais523> elliott: it isn't, but f might be an expression, that can't be directly returned without the ?
22:17:29 <ais523> as in, the ? is explicitly marking that we're returning a closure
22:18:35 <ais523> normally if you mention a function in Anarchy, it gets applied to something
22:18:39 <ais523> normally _
22:20:01 <elliott> back
22:20:14 <elliott> oh, f differs from (fun x -> f x) because f can have side-effects
22:20:27 <elliott> yet another dumb thing about impure languages
22:20:30 <ais523> actually, I haven't thought about that yet
22:20:47 <ais523> not even sure if Anarchy is pure or not; I have some impurities in the spec currently, but am thinking about changing it
22:21:17 * elliott considers installing HTTPS Everywhere
22:21:24 <elliott> ais523: you have assignment
22:21:31 <ais523> no I don't
22:21:39 <ais523> = in Anarchy is more like a let-binding
22:21:45 <ion> It’s liberating when *everything* is in unsafePerformIO!
22:21:47 -!- tzxn3 has quit (Read error: Connection reset by peer).
22:21:57 <ais523> if you see "b = x", read it as "let b = x in"
22:22:07 <ais523> and then put a copy of the original pattern at the end of the line
22:23:05 <ais523> so you can read replace_head as "replace_head x u = match u with E _ b -> let b2 = x in E _ b2"
22:23:22 <ais523> (I renamed one of the bs to show that they're different variables)
22:24:31 <ais523> why do people look at an = in a language and assume it's assignment?
22:24:39 <ais523> arguably it's SSA, but that ofc isn't impure
22:24:43 <Phantom_Hoover> Because it is in most languages?
22:25:36 <ais523> not most Haskellish/OCamllish languages
22:25:42 <ais523> in OCaml, = is binding, := is assignment
22:25:51 <ais523> and you'd expect Anarchy to be much the same, given the syntax resemblences
22:26:25 <Phantom_Hoover> In a basic, intuitive understanding, binding is pretty similar to assignment.
22:27:17 <ais523> yep
22:27:20 <ais523> but one's pure and the other isn't
22:27:50 <elliott> ais523: because it's not in the context of an obvious expression in your code
22:27:56 <elliott> and you use imperative structures like ;
22:28:07 <ais523> well, OK
22:28:32 <ais523> anyway, there are a couple of effects I'm considering for Anarchy, name generation and constraining
22:28:40 <ais523> but not assignment, it's too ugly
22:29:09 <elliott> if name generation means a symbol u such that u never equals u, then that's gross :(
22:29:29 <ais523> elliott: it's more or less that, but that by itself is indeed gross
22:29:57 <ais523> I'd only add it if I could find a more controlled way to do it
22:30:44 <elliott> what's constraining?
22:31:04 <ais523> basically, adding constraints to a constraint solver
22:31:09 <ais523> and getting an exception if they're no longer satisfied
22:31:22 <elliott> that doesn't sound impure to me, as long as the exception is at a high enough layer
22:31:27 <elliott> i.e. more like "no solutions" in Prolog than an error
22:31:29 <oerjan> <oklopol> well mine is how oerjan wanted it to be solved <-- my impression is that ais523 is concentrating on how i build my subroutine but oklopol on how i'm using it?
22:31:44 <oerjan> (re oerjanswap understanding discussion)
22:31:45 <ais523> elliott: it's no more impure than _|_ is
22:31:58 <ais523> I think, at least
22:32:00 <oklopol> i don't think so based on the discussion that followed
22:32:01 <elliott> ais523: well, it's impure if it can cause other code outside its scope to be _|_ when they wouldn't otherwise be
22:32:04 <elliott> since that breaks RT
22:32:13 <oklopol> erm
22:32:17 <ais523> right
22:32:18 <elliott> ais523: but if it's "constrain C in E" then it should be fine
22:32:28 <elliott> and not, IMO, an effect
22:32:36 <oklopol> actually now that i recall the reverse-engineering of the subroutine, that does sound very similar to what ais said
22:32:42 <oklopol> so yeah maybe
22:33:12 <ais523> hmm, I was originally planning a C that worked outbound as well as inbound
22:33:15 <ais523> so it'd just be "constrain C"
22:33:24 <ais523> which might or might not throw an exception
22:33:26 <elliott> ais523: outbound howso
22:33:35 <elliott> the problem with that is that if you evaluate an expression before constrain C, it might be OK
22:33:39 <elliott> but it might be an error afterwards
22:33:42 <ais523> right, indeed
22:33:46 <elliott> which breaks RT, albeit in a way I think undetectable from the outside
22:33:47 <ais523> and outbound in that it affects its callers too
22:33:50 <elliott> making it gross
22:33:54 <ais523> what does RT stand for?
22:33:58 <elliott> referential transparency
22:34:01 <ais523> right
22:34:08 <elliott> aka things not changing randomly from behind your back
22:34:35 <ais523> oh, constrain C in E is obviously fine, you can convert it into an extra function parameter
22:35:11 <ais523> so it's just sugar around the ordinary LCish way of doing things
22:35:20 <elliott> ais523: that's OK if you add do-notation; then you can use Cont to recover nice syntax
22:35:23 <elliott> (if you deeply nest them)
22:35:24 <ais523> I'm just not convinced it's useful
22:35:40 <elliott> however
22:35:44 <elliott> I am not sure "constrain C in E" is fine
22:35:52 <elliott> it sounds like it breaks parametricity to me
22:35:53 <elliott> because you can have
22:35:56 <elliott> foo :: forall a. a -> a
22:35:57 <elliott> which does
22:36:01 <elliott> foo x = constrain C in x
22:36:04 <elliott> now,
22:36:07 <elliott> @free id
22:36:07 <lambdabot> f . id = id . f
22:36:16 <elliott> bleh, how useless
22:36:25 <elliott> anyway point is
22:36:26 <elliott> foo =/= id
22:36:34 <elliott> because foo x could = exception instead
22:36:37 <elliott> which is not OK
22:36:46 <ais523> I've thought of a different way to do it, anyway, that's obviously fine; simply stick the constraints on the data structure you're operating on using metadata, then grab them all at once with '', then have a constraint-solving library function
22:36:50 <elliott> ie you can observe things about values by wrapping them in constrain
22:36:54 <ais523> yep
22:37:59 <oerjan> `addquote <fizzie> elliott: I'm not going to even bother with the recursive "I'm not going to dignify that" stuff. <fizzie> *LAA LAA LAA NOT DIGNIFYING LAA LAA*
22:38:03 <HackEgo> 812) <fizzie> elliott: I'm not going to even bother with the recursive "I'm not going to dignify that" stuff. <fizzie> *LAA LAA LAA NOT DIGNIFYING LAA LAA*
22:38:35 <oerjan> hm
22:38:43 <oerjan> `delquote 812
22:38:47 <HackEgo> ​*poof* <fizzie> elliott: I'm not going to even bother with the recursive "I'm not going to dignify that" stuff. <fizzie> *LAA LAA LAA NOT DIGNIFYING LAA LAA*
22:38:58 <oerjan> `addquote <fizzie> elliott: I'm not going to even bother with the recursive "I'm not going to dignify that" stuff. [...] <fizzie> *LAA LAA LAA NOT DIGNIFYING LAA LAA*
22:39:02 <HackEgo> 812) <fizzie> elliott: I'm not going to even bother with the recursive "I'm not going to dignify that" stuff. [...] <fizzie> *LAA LAA LAA NOT DIGNIFYING LAA LAA*
22:39:10 <oerjan> `quote ...
22:39:14 <HackEgo> 1) <Aftran> I used computational linguistics to kill her. \ 2) <Slereah> EgoBot just opened a chat session with me to say "bork bork bork" \ 3) <Quas_NaArt> Hmmm... My fingers and tongue seem to be as quick as ever, but my lips have definitely weakened... <Quas_NaArt> More practice is in order. \ 4) <AnMaster> that's where I got it <AnMaster> rocket launch facility gift shop \ 5) <Warrigal> GKennethR: he should be told
22:39:25 <oerjan> `quote [[]...
22:39:28 <HackEgo> 39) <mycroftiv> [...] sometimes i cant get out of bed becasue the geometry of the sheet tangle is too fascinating from a topological perspective \ 81) [Warrigal] `addquote <Dylan> hahaha, Lawlabee is running windows <Lawlabee> 'cuz it's pretty awesome. [Lawlabee] Warrigal: :( \ 112) * augur rubs alise's bum [...] <augur> what? she said square ped <augur> :| \ 121) <fungot> pikhq: from csh type ' exit', is a
22:39:58 <oklopol> topology!
22:40:12 <oerjan> i'm not entirely sure of the perfectly elliotic spacing of [...]
22:40:19 <elliott> it is
22:40:20 <oklopol> have you heard the story about the set that was both open and closed
22:40:30 <elliott> the [...] goes in-between the two spaces
22:40:36 <oklopol> well he walked into a bar
22:40:48 <oerjan> oklopol: SORRY I CANTOR YA
22:40:58 <Phantom_Hoover> I can think of quite a few punchlines to this, none of them good.
22:40:59 <oklopol> :DD
22:41:22 <oklopol> Phantom_Hoover: working on it
22:41:28 <oklopol> having similar results
22:41:38 <Phantom_Hoover> Procedurally generated jokes?
22:41:51 <oerjan> elliott: yay i got it right then
22:43:19 <oklopol> Phantom_Hoover: can you think of one that isn't a pun?
22:43:26 <oklopol> puns are retarded
22:43:57 -!- PiRSquared has joined.
22:44:27 <Phantom_Hoover> I'm trying to remember that property that's equivalent to no sets but the empty set and the... full set(?) being clopen.
22:44:32 <Phantom_Hoover> Maybe there's something in that?
22:44:43 <Phantom_Hoover> (Hausdorff comes to mind, but I'm not sure it's it.)
22:44:59 <oklopol> that's true in the reals
22:45:07 <oklopol> hausdorff is not it
22:45:20 <Phantom_Hoover> Hmm.
22:45:56 <oklopol> you could probably state it using the term "zero-dimensional", but perhaps not directly, i'm still unsure what the usual definition is.
22:46:22 <Phantom_Hoover> I recall it being something I understood pretty well, but since that basically restricts it to {Hausdorff, compact} I'm not sure I'm remembering reliably.
22:46:41 <oklopol> hausdorff and compact doesn't imply that property
22:46:52 <ais523> `quote
22:46:53 <ais523> `quote
22:46:55 <ais523> `quote
22:46:55 <HackEgo> 140) <fungot> ais523: elf corpses are not considered expensive health food. but the most expensive.
22:46:56 <HackEgo> 111) <alise> use "grep --crazy"
22:46:56 <ais523> `quote
22:46:57 <Phantom_Hoover> Ohhhhh, it's connectedness.
22:46:58 <ais523> `quote
22:46:59 <HackEgo> 353) <tswett> Grr. Why does it exist? Why can't I kill it?
22:47:00 <HackEgo> 254) <fizzie> Deewiant: Did you take the course at some point and/or were you taking it now and/or did you actually already graduate and/or are you still in Otaniemi anyway?
22:47:03 -!- sebbu3 has changed nick to sebbu.
22:47:06 <oklopol> erm right >D
22:47:13 <HackEgo> 131) <Mathnerd314> Gregor-P: I don't think lambda calculus is powerful enough
22:47:19 <oklopol> well still, zero-dimensionality is relevant too
22:47:29 <Phantom_Hoover> oklopol, then the barman says "I'm not giving you a drink, you're in pieces!".
22:47:39 <Phantom_Hoover> Wait that might be a pun.
22:47:41 <ais523> I think 111 is the worst there, possibly 131
22:47:42 <ais523> other opinions?
22:47:45 <Phantom_Hoover> Also terrible.
22:47:45 <PiRSquared> `quote \bpun\b
22:47:49 <HackEgo> 790) <fungot> elliott: to be honest, it doesn't exist in a state of almost perpetual stalemate, and expands to a larger board and more exotic collection of what he refers to as a thermal hull, instead of some kind of clock pun. no, dammit, will this breakfast injure his shrill, bearded, scraggly old men in space. jade's radioactive, omnipotent, space-warping dog named...
22:48:05 <ais523> `delquote 111
22:48:09 <HackEgo> ​*poof* <alise> use "grep --crazy"
22:48:59 <elliott> Faster Javascript Through Category Theory (johnbender.us)
22:49:00 <elliott> FINALLY.
22:49:36 <oklopol> Phantom_Hoover: i would prefer "i'm not giving you a drink, all sequences completely within you or outside you will have their limit points within you or outside you as well, respectively!".
22:49:59 <Phantom_Hoover> oklopol, it's snappier, I'll give you that.
22:50:01 <oklopol> yes
22:50:48 <oklopol> i should write a book called "funny math jokes hehe"
22:53:52 <oklopol> i guess i can safely give you a drink, since you're currently given continuous dynamics by R as you're in a three-dimensional bar, and thus the throw-up could never leave your body if it was too much for you
22:54:12 <oklopol> now there's a punchline.
22:54:42 <oklopol> well
22:55:46 <oklopol> "i cannot give you a drink since, given that this bar is, like all the cool bars, a proper subset of R^3, you cannot have any points, so technically you're underage"
22:56:19 <oerjan> <Phantom_Hoover> I'm trying to remember [...] <-- connected
22:56:23 <oklopol> well dunno how old the empty set is
22:56:38 <oklopol> IN MY DEFENSE, I PROBABLY HAVE A FEVER
22:58:33 <oerjan> oh no, the dreaded irc virus!
22:58:44 <oerjan> i knew my headache had to be something fatal.
22:58:53 <oklopol> i have been working home all week so i wouldn't kill everyone at the uni
23:06:24 <tswett> So, about the alternating group on 4 elements.
23:06:47 <tswett> Specifically, its presentation by two generators of order 3.
23:06:49 -!- Goosey has quit (Ping timeout: 252 seconds).
23:06:54 <Phantom_Hoover> Good group, that.
23:07:29 <oerjan> nah it's not simple enough.
23:07:31 <tswett> How easily can you write a Thue program that takes an expression written using these generators and reduces it to a canonical form?
23:08:16 <tswett> The substitution rules I want to use are these: aaa::= bbb::= ba::=aabb
23:08:20 <tswett> Unfortunately, those rules don't actually work.
23:09:40 <oerjan> just include the whole multiplication table on canonical forms?
23:10:05 <oerjan> except for those that are equal before and after
23:10:06 <tswett> Hm... that sounds like it should work.
23:10:13 <oklopol> is that group generated by any two elements of order 3 that aren't powers of each other?
23:10:23 <oklopol> erm
23:10:41 <tswett> oklopol: um... well, A_4 has order 12. What you're talking about sounds like it would be infinite.
23:10:54 <oklopol> any two of its elements
23:11:14 <Phantom_Hoover> oklopol, the symmetric group?
23:11:29 <oklopol> i don't think a group of order 6 can be generated, but i don't directly see why
23:11:38 <oklopol> Phantom_Hoover: ?
23:11:50 <Phantom_Hoover> Or are you talking about tswett's thing?
23:11:51 <tswett> A_4 has no subgroup of order 6.
23:11:55 <oklopol> oh
23:12:10 <oklopol> in that case, any two elements of order three will generate it
23:12:24 <oklopol> unless they generate the same subgroup
23:12:26 <tswett> Right. That's why I mentioned its presentation by two generators of order 3.
23:12:34 <oerjan> hm yes all pairs of such 3-order elements must have 2 common elements in their cycle.
23:12:43 <oklopol> you didn't say it doesn't matter which two you choose
23:12:49 <tswett> True.
23:12:54 <tswett> So, does anyone have a presentation of A_4 on hand?
23:13:14 <oklopol> oerjan: i was hoping for a higher-level argument
23:13:18 <oerjan> so all pairs must generate the same thing up to isomorphism
23:13:23 <oklopol> hmm
23:13:25 <oklopol> oh
23:13:30 <tswett> Ooh, the von Dyck group is apparently A_4.
23:13:46 <tswett> Er, one specific von Dyck group is A_4.
23:14:02 <tswett> Namely, the group generated by a, b, and c such that a^3 = b^3 = c^2 = abc = e.
23:14:13 * Phantom_Hoover remembers that he doesn't know as much group theory as he'd like, wishes he'd just hurry up and get to university.
23:14:14 <oklopol> tswett: what you doing these days?
23:14:26 <tswett> oklopol: oh, I'm studying math at university.
23:14:33 <oklopol> how old are you?
23:14:37 <tswett> 19 now.
23:14:52 <oklopol> any papers yet?
23:14:58 <tswett> Nope.
23:15:12 <oklopol> have you chosen your path?
23:15:27 <tswett> I wrote an MO question that netted me 260 reputation, though. ^_^
23:15:28 <oklopol> will you do CA theory with me?!?
23:15:36 <oklopol> what's that
23:15:46 <tswett> I guess not. I'm planning to go into actuarial, or, if I find something that makes more money, that.
23:15:59 <tswett> Mathoverflow?
23:16:01 <oklopol> oh i was assuming research
23:16:05 <oklopol> link
23:16:11 <tswett> s/?/.net/
23:16:14 <Phantom_Hoover> tswett, you are, bad
23:16:32 <tswett> I don't *think* research would make as much money as actuarial.
23:16:39 <tswett> Phantom_Hoover: quiet, you, or I'll double your insurance premiums.
23:16:45 <Phantom_Hoover> (My dad once saw Good Will Hunting and then he was like PH, you should totally work for the CIA.)
23:17:08 <oklopol> actuarial will make make more money, but you would be useless
23:17:17 <oklopol> |would
23:17:23 <oklopol> *would
23:17:45 <tswett> So, um, what does the corrected message look like?
23:17:50 -!- augur has quit (Remote host closed the connection).
23:18:03 <oklopol> will to would
23:18:09 * tswett nods.
23:18:25 <tswett> I won't be useless if I donate a bunch of money to some awesome charity.
23:18:25 -!- augur has joined.
23:18:42 <oklopol> the math charity perhaps?
23:19:10 <oklopol> "sorry i couldn't come, but you all have fun up there, here take my money"
23:19:26 <tswett> Suppose I make $300,000 and donate half of it to the Against Malaria Foundation. Boom: 75 lives saved every year.
23:19:42 <oklopol> yeah we need more people staying alive
23:19:53 <tswett> Staying alive is nice.
23:20:10 <oklopol> in the long run, yes
23:20:31 <oklopol> right now, it would make more sense to kill some jews
23:20:53 <tswett> Would it?
23:20:57 <oklopol> figuratively speaking
23:21:02 <tswett> Ah.
23:21:05 <Friendship> `addquote <oklopol> right now, it would make more sense to kill some jews
23:21:08 <HackEgo> 812) <oklopol> right now, it would make more sense to kill some jews
23:22:31 <elliott> `delquote 812
23:22:34 <HackEgo> ​*poof* <oklopol> right now, it would make more sense to kill some jews
23:22:46 -!- augur has quit (Ping timeout: 246 seconds).
23:23:15 <oklopol> i don't know if i've even met a jew
23:23:16 <oerjan> censorship is magic
23:23:23 <oklopol> elliott: why did you remove that? :D
23:23:37 <oerjan> oklopol: BECAUSE HOLOCAUST
23:23:41 <elliott> it definitely wasn't funny without context
23:23:43 <oklopol> really i would prefer the whole exchange
23:23:44 <oklopol> yeah
23:23:56 <oklopol> "figuratively speaking" "ah."
23:24:02 -!- Jafet has quit (Quit: killing the juice!).
23:24:08 <tswett> Friendship: hey, are you Gregor?
23:24:15 <tswett> Never mind, I figured it out instantly.
23:24:47 <tswett> (I love arrogant Homestuck quotes.)
23:24:53 <tswett> (But I only know of the one.)
23:25:10 <oklopol> is it "Friendship: hey, are you Gregor?"
23:25:13 -!- elliott has left ("Leaving").
23:25:46 <tswett> Nope.
23:26:02 <Friendship> ..........
23:26:04 <oklopol> seriously though, i'm worried about people destroying the earth, i'm a total hippie
23:26:04 <tswett> Add one to that sentence, and you'll get what it is.
23:26:38 <oklopol> Friendship: you're a jew, no?
23:26:45 <tswett> I'm worried about people destroying Earth. But only where "destroying Earth" is interpreted loosely.
23:26:54 <tswett> I'm not worried about people destroying, in a strict sense, Earth.
23:26:57 <Friendship> oklopol: Depends on your definition.
23:27:06 -!- ais523 has quit (Remote host closed the connection).
23:27:08 <Friendship> Mostly "no" X-D
23:27:10 <oklopol> i don't have a definition
23:27:14 <oklopol> but i thought there was one
23:27:26 <Friendship> It's a religion, a culture, and several races.
23:27:49 <oklopol> i just know the hitler story and the stereotype in american tv shows
23:27:51 <Friendship> I am not a member of the religion, and am only a member of the culture insofar as American Jews are near-universally atheists :)
23:27:52 <tswett> Friendship: do you *look* like a Jew?
23:27:55 <oklopol> we don't have the concept in finland
23:28:04 <tswett> oklopol: the concept of Judaism?
23:28:06 <Friendship> tswett: My nose sure does. But I have blond hair and bluegreensomething eyes, so no, not really.
23:28:25 <oklopol> tswett: the concept of "jew"
23:28:47 * tswett nods.
23:29:14 <oklopol> or at least i only learned about them in history class and then later tv.
23:30:42 <tswett> Wait, wait. The finite fields have algebraic closures?
23:30:45 <oklopol> sure
23:30:54 <tswett> Are their algebraic closures also finite fields?
23:30:54 <oklopol> everything does
23:30:56 <oklopol> no
23:31:08 <tswett> Oh yeah. It seems more obvious that everything does than that those specific ones do. }:P
23:31:08 <oklopol> they are inverse limits of p^k fields
23:31:22 <tswett> Inverse... limits.
23:31:28 <oklopol> yeah it means
23:31:41 <tswett> Is this "limit" in the, um... category theory sense, I think it is?
23:32:23 <oklopol> the inverse limit means you take all the F_{p^k} and morphisms from bigger to smaller ones
23:32:42 <oklopol> and points are that you take a point in each of the finite fields so that the morphism form a nice chain
23:32:44 <oklopol> (afaiu)
23:32:54 <oklopol> yeah in the category theory sense
23:33:03 <tswett> Are all of those morphisms epi?
23:33:08 <oklopol> yeah
23:33:40 <tswett> Intuitively, this sounds a lot like taking the limit of F_{p^k} as k approaches infinity.
23:33:52 <oklopol> oooooops
23:33:55 <oklopol> actually
23:34:21 <oklopol> i think it's the limit instead: just the union of F_{p^k} fields
23:34:27 <tswett> Except my intuition says *that* would involve monomorphisms from smaller to bigger ones.
23:34:35 <tswett> Which...
23:34:40 <oklopol> (where you have some nice equivalence relation)
23:34:42 <tswett> Is what you jsut said.
23:35:39 <tswett> So, is the algebraic closure of F_{p^k} unique given p?
23:35:56 <oklopol> the algebraic closure is always unique afaiu
23:36:19 <tswett> And the algebraic closure of F_{p^k} must be the same as F_{p^h}, aye?
23:36:43 <oklopol> that i'm not as sure about
23:37:28 <oklopol> i don't really know anything about this, but i'll investigate this further once i'm less sick. now i have to go to work to get my fever up.
23:37:53 * tswett nods.
23:38:37 <oklopol> erm first what have you taken at the university sofar/
23:38:39 <oklopol> ?
23:38:55 <Phantom_Hoover> Holy crap, at noon on the winter solstice the sun in Edinburgh is *14 degrees* from the horizon.
23:39:02 <Phantom_Hoover> I never realised I'm *that* far north.
23:39:24 <Phantom_Hoover> And we _still_ didn't see a single flake of snow this winter.
23:39:32 <tswett> oklopol: well, I'm taking Advanced Calculus II and Modern Algebra II.
23:39:41 <oklopol> modern algebra?
23:39:52 <tswett> I.e. analysis and group theory.
23:39:54 <oklopol> advanced calculus?
23:40:10 <Phantom_Hoover> tswett, so a century and a bit old, then?
23:40:30 <tswett> Strangely enough, I think Advanced Calculus I went farther than Advanced Calculus II is going.
23:41:07 <oklopol> SO WHAT ABOUT SUBSHIFTS, HAVE THEY TOLD YOU ABOUT SUBSHIFTS
23:41:27 <tswett> No, that's what Wikipedia is for.
23:41:40 <oklopol> no wikipedia is for group theory and analysis
23:41:45 <tswett> Oh.
23:41:50 <oklopol> university should be all about subshifts
23:41:54 <oklopol> and cellular automata
23:41:56 <oklopol> and ergodic theory
23:42:07 <tswett> Let me guess. You did your PhD on subshifts and cellular automata and ergodic theory.
23:42:20 <Phantom_Hoover> Master's, actually.
23:42:21 <oklopol> my phd is not really done yet :D
23:42:31 <oklopol> and my master's thesis was on picture languages!
23:42:55 <oklopol> on subshifts and CA i just have two accepted articles and about 10 in the making
23:42:56 <Phantom_Hoover> Awwww, painting pretty pictures in foreign languages.
23:43:03 <Phantom_Hoover> oklopol, the humanitarian.
23:43:28 <oklopol> i solved like all the open problems in picture language theory
23:43:33 <tswett> Who was it that did his PhD on sets of biinfinite words such that every factor appears finitely far apart?
23:43:42 <oklopol> and then i realized it was only because all the researchers were stupid
23:43:46 <Phantom_Hoover> Me.
23:43:54 <oklopol> tswett: oerjan
23:43:58 <tswett> Ah, right.
23:44:07 <Phantom_Hoover> oklopol, obviously it was clever of you to pick a field only idiots specialise in.
23:44:07 <oklopol> minimal systems
23:44:47 <oklopol> well i like to think i revolutionized the whole theory and developed all the interesting techniques and am a god.
23:44:49 * Phantom_Hoover -> sleep
23:44:51 -!- Phantom_Hoover has quit (Quit: Leaving).
23:45:10 <oklopol> i know, my modesty knows no limits.
23:46:02 <oklopol> tswett: i study the opposite kind of biinfinite word sets than what oerjan studied
23:46:56 <tswett> I'm still trying to figure out what the product topology of a finite discrete space is.
23:47:02 <oklopol> where words usually do not, and often CANNOT appear finitely far apart (if by that you mean "every factor of length m appears in every factor of length n for large enough n")
23:47:25 <tswett> Rather, the topology of the product of infinitely many finite discrete spaces.
23:47:37 <oklopol> an open set specifies a finite amount of coordinates in some open sets, and the rest can be anything
23:47:43 <oklopol> or that's a basis at least
23:48:12 <tswett> Mm, I think I'd rather figure out what a closed set is. And I think that means figuring out what a limit is.
23:48:17 <oerjan> <tswett> And the algebraic closure of F_{p^k} must be the same as F_{p^h}, aye? <-- i vaguely think they're both contained in F_{p^(kh)}, which means their limit diagrams have a common tail so to speak and so have the same limit.
23:48:17 <oklopol> (that's the general definition of product topology)
23:48:28 <tswett> I guess it's reasonably obvious what a limit of biinfinite words is, don't you think?
23:48:37 <oklopol> tswett: a limit means eventually, every coordinate becomes constant
23:48:42 <tswett> So yeah.
23:48:56 <oklopol> well obvious and obvious, there are other topologies you can use
23:49:07 <oklopol> awesome topologies.
23:49:09 -!- augur has joined.
23:49:29 <tswett> Okay. So, given an oerjan word (for lack of a better name, 'cause that name sucks), we can break it up into the set of all its finite factors.
23:49:38 <oklopol> oerjan: but i don't think it's inverse limit, i think it's just limit
23:49:52 <oklopol> so it's just a union of F_{p^k}
23:49:58 <oklopol> for different k
23:50:08 -!- elliott has joined.
23:50:14 <tswett> And then given that slurry, we can form the set of all oerjan words (for lack of a . . .) with the same finite factors.
23:50:29 -!- elliott has left ("Leaving").
23:50:31 <oklopol> a uniformly recurrent word i suppose
23:51:05 <tswett> This set certainly satisfies the shift criterion. Is it also closed?
23:51:10 <oklopol> tswett: yeah, and that's exactly the closure of the set of words you obtain by moving it left and right
23:51:22 <oerjan> <tswett> Rather, the topology of the product of infinitely many finite discrete spaces. <-- for countably many, that's homeomorphic to a/the Cantor set.
23:51:24 <oklopol> it's closed
23:51:42 <tswett> I think the set of all Sturmian words given a single constant is a shift space.
23:51:55 <oklopol> yes
23:52:03 -!- elliott has joined.
23:52:03 <tswett> oerjan: for a biinfinite sequence, can you just break it in half, turn one half around so it's pointing the same way as the other half, and interleave them to get the Cantor representation thing?
23:52:16 <tswett> Obviously, it's also a slurry-generated set.
23:52:48 <oklopol> that sounds dangerous w.r.t. shift-closedness
23:53:08 <oklopol> and also you may get weird-ass correlation between patterns
23:53:12 <oerjan> <oklopol> oerjan: but i don't think it's inverse limit, i think it's just limit <-- hm right, every element in the closure should be a root of _some_ polynomial of the original field.
23:53:14 <tswett> Oh, right. What's the topology of the set of all Sturmian words given a single constant?
23:53:38 -!- Goosey has joined.
23:53:39 <oklopol> the product topology, presumably
23:53:45 <elliott> Today I learned: Friendship's definition of "near-universally" is "52%".
23:54:14 <oerjan> <tswett> oerjan: for a biinfinite sequence, can you [...] <-- yes, since the order of the coordinates don't really play any part in the topology
23:54:17 <tswett> Well... yeah. But it's a *subspace* of the Cantor set, isn't it?
23:54:44 <oklopol> yeah a subshift of it in fact
23:55:01 <tswett> Yeah.
23:55:12 <oklopol> (assuming that the sturmian words are exactly the orbit closure of the characteristic sturmian word, i think so)
23:55:25 <tswett> I was going to ask if it was homeomorphic to a circle. But it doesn't seem like the Cantor set would have a circle as a subspace.
23:55:37 <oklopol> it doesn't
23:55:43 <oklopol> it's totally disconnected
23:55:49 <oerjan> <oklopol> a uniformly recurrent word i suppose <-- that was the word. btw only _part_ of my phd considered the points to be infinite words.
23:56:01 <tswett> If a space is totally disconnected, must its subspaces be totally disconnected as well?
23:56:22 <oklopol> yes
23:56:24 <oklopol> i think
23:56:37 <oklopol> totally disconnected means if you take any two points then they can be separated by open sets
23:56:43 <oklopol> in the sense that
23:56:58 <oklopol> you can partition the space into two opens each containing one point
23:57:00 <oklopol> or something.
23:57:06 <tswett> If you take any two points, you can write the entire... yeah, that.
23:57:12 <oklopol> this is certainly a property the cantor set has
23:57:24 <tswett> It never stops being a property it has.
23:57:26 * tswett coughs.
23:57:39 <oerjan> tswett: totally disconnected ~ 0-dimensional, and dimension cannot increase in subsets
23:58:01 <tswett> Can you quotient S^1 to get S^2?
23:58:30 <tswett> No, of course you can. I think.
23:58:32 <oerjan> you can map S^1 onto S^2, but i'm not sure if that's a quotient
23:58:42 <oerjan> (see: peano curve)
23:59:06 <tswett> It's surjective, all right, and doesn't every continuous surjective function lead to a quotient, or something?
23:59:30 <oerjan> btw every compact metric hausdorff set is the continuous image of a cantor set, iirc
23:59:40 <oerjan> *space
23:59:59 <tswett> Something tells me that has something to do with Haskell.
←2012-02-28 2012-02-29 2012-03-01→ ↑2012 ↑all