00:00:44 -!- vravn has joined.
00:13:37 -!- glogbackup has quit (Remote host closed the connection).
00:16:30 * boily subtly pokes quintopia
00:19:40 -!- Sgeo has joined.
00:22:43 -!- Sgeo_ has joined.
00:24:30 <FreeFull> ion: Dreamweaver does that with .cs files
00:25:43 -!- tromp_ has joined.
00:25:57 -!- tromp__ has joined.
00:26:01 -!- Sgeo has quit (Ping timeout: 240 seconds).
00:28:49 -!- tromp_ has quit (Ping timeout: 240 seconds).
00:45:37 <boily> joyeux a-pi-versaire!
00:49:39 -!- b_jonas has quit (Ping timeout: 240 seconds).
00:49:39 -!- CADD_ has quit (Ping timeout: 240 seconds).
00:50:02 -!- myname has quit (Ping timeout: 240 seconds).
00:50:09 -!- myname has joined.
00:51:12 -!- b_jonas has joined.
00:51:42 -!- Guest95255 has joined.
00:56:25 -!- Guest95255 has quit (Ping timeout: 240 seconds).
00:58:30 -!- Guest95255 has joined.
01:02:06 -!- FireFly has quit (Excess Flood).
01:02:28 -!- Effilry has joined.
01:04:04 -!- Phantom_Hoover has quit (Quit: Leaving).
01:07:43 -!- glogbackup has quit (Ping timeout: 264 seconds).
01:08:49 -!- lifthrasiir has quit (Ping timeout: 240 seconds).
01:14:16 -!- augur_ has joined.
01:14:19 -!- conehead has quit (Quit: Computer has gone to sleep.).
01:17:37 -!- augur has quit (Ping timeout: 240 seconds).
01:19:07 -!- lifthrasiir has joined.
01:20:01 * oerjan staws Effilry -#--##--
01:20:33 -!- tertu_ has joined.
01:20:38 -!- luserdroog has joined.
01:20:48 -!- tertu has quit (Ping timeout: 240 seconds).
01:28:22 -!- Phantom_Hoover has joined.
01:31:48 <boily> oerjan: staws? is that like a Norwegian Mapole?
01:33:25 <oerjan> no, that would be stav
01:34:43 <shachaf> what sort of bizarre rettaws is that
01:35:17 <oerjan> https://en.wiktionary.org/wiki/stav#Swedish in lack of a norwegian version
01:35:46 <oerjan> you might note that Effilry is isomorphic to FireFly hth
01:36:49 -!- yorick has quit (Remote host closed the connection).
01:39:29 * boily is suddenlilluminated
01:39:50 <boily> (or is it suddenlightened?)
01:40:26 <shachaf> oerjan: i didn't look at it long enough to see that it wasn't just reversed
01:40:48 <shachaf> it would only have taken one letter to see that
01:41:03 <shachaf> almost any letter would have worked
01:41:20 <boily> but still. it's a very weird rettaws, much like a klingon weapon.
01:41:37 -!- boily has quit (Quit: ISOMORPHIC NICHECK).
01:41:41 -!- metasepia has quit (Remote host closed the connection).
01:56:55 -!- itsy has quit (Ping timeout: 264 seconds).
01:56:57 -!- Phantom_Hoover has quit (Quit: Leaving).
02:03:40 -!- Froox has quit (Read error: Connection reset by peer).
02:05:31 -!- Frooxius has joined.
02:09:51 -!- oerjan has quit (Quit: Hmm).
02:14:20 -!- Sorella_ has changed nick to Sorella.
02:23:58 -!- luserdroog has quit (Ping timeout: 245 seconds).
02:24:31 <kmc> i wonder if there are compilers that will take state machine code like while(1) { switch (state) { ... } } and allocate 'state' in the instruction pointer register, so to speak
02:24:57 <kmc> that is, turn the assignments to 'state' into jumps
02:28:23 -!- shikhout has joined.
02:31:43 -!- shikhin has quit (Ping timeout: 264 seconds).
02:31:43 -!- shikhout has changed nick to shikhin.
02:45:14 -!- evalj has quit (Remote host closed the connection).
02:51:07 <kmc> print!(" \x1b[36m{:s}\x1b[0m='\x1b[34m{:s}\x1b[0m'", attr.name, attr.value);
02:52:04 <kmc> there are a lot of different languages packed into that one line of code
02:58:31 <Bike> today i tried to invoke a shell on windows through matlab and i think it gave me VT100 control codes
02:58:34 <Bike> a disheartening experience
02:58:44 <Bike> that looked a lot like that string >_>
02:59:04 <kmc> those are VT100 control codes, or ECMA-48 codes anyway
02:59:12 <kmc> I don't remember if the actual VT100 had color, probably not
02:59:37 <Bike> oh. lol i was just shallowly seeing unclosed square brackets
03:00:03 <kmc> it's a good tip-off
03:01:03 <pikhq> ECMA-48 apparently predates the VT100.
03:01:12 <kmc> but not the latest edition, which is from 1991
03:01:31 -!- luserdroog has joined.
03:01:46 <pikhq> Ah sweet, I found the VT100 manual.
03:01:46 <kmc> god bless you ECMA, for making your standards free online and not trying to wring me for every last CHF like those ISO bastards
03:01:57 <kmc> SIPB owns an actual VT100, or is it a VT220
03:02:08 <kmc> they had it hooked up to a Raspberry Pi, which fit easily within the case
03:02:10 <kmc> it was cute
03:02:37 <kmc> Bike: the two-byte sequenc \x1b [ (i.e. ESCAPE [, i.e. ^[ [) is the Control Sequence Introducer, which begins many of the most important commands
03:02:53 <Bike> i think it printed as like... ~V[ or something
03:03:29 <pikhq> It seems that it did not *support* color, but the VT100 ignores unknown character attributes.
03:03:35 <Bike> in the end i figured out i could in fact invoke programs directly and just did that and everything went away. huzzah.
03:03:46 <kmc> or rather, it's the 7-bit ASCII representation of CSI. you can also use the character 'CONTROL SEQUENCE INTRODUCER' (U+009B) from the ISO 2022's C1 control code section
03:03:51 <kmc> but mostly people don't
03:03:58 <pikhq> So on a VT100 you don't get color *display*, but the color codes work just fine.
03:04:02 <pikhq> (i.e. "do nothing")
03:04:24 <kmc> presumably on a UTF-8 terminal you would have to write 0xC2 0x9B anyway...
03:05:51 <pikhq> Thankfully all the character attributes are parameters to \
03:06:18 <pikhq> Which means that it's actually quite simple for a terminal to no-op support the colors.
03:06:25 <pikhq> And apparently the VT100 did just that.
03:06:26 <Bike> oh as long as i'm complaining i found out that cmd.exe is pretty much terrible
03:06:43 <kmc> Bike: yes. you want a better shell (like MSYS bash) and a better terminal emulator (like Mintty)
03:06:58 <Bike> i invoked a program by quoting the path and it reported the program as having the quote character in it
03:07:25 <Bike> bash i have, but not a better tty. hoooopefully i won't be using shell enough to want that, but
03:07:27 <kmc> pikhq: I think it's odd that the character telling you what the command is comes at the end, but I suppose it makes sense in an implementation where you're storing to registers as arguments come in, and then you execute
03:07:33 <kmc> which might be how the hardware worked
03:07:51 <Bike> of course, msys doesn't have man pages :( oh well
03:09:09 <Bike> also: does anyone know what the hell git rev-parse is
03:10:08 <Bike> "A similar notation r1...r2 is called symmetric difference of r1 and r2 and is defined as r1 r2 --not $(git merge-base --all r1 r2). " pretty sure i'm out of my league here
03:10:47 <Bike> "Note that .. would mean HEAD..HEAD which is an empty range that is both reachable and unreachable from HEAD."
03:10:49 <kmc> Bike: it describes the syntax you can use to name git objects, mainly commits
03:11:15 <kmc> the actual rev-parse command is meant for use from scripts
03:11:26 <kmc> but many of the user-facing commands accept the same syntax
03:11:33 <Bike> getting the last commit object was both easier (since it's just "git rev-parse HEAD") and harder (since i have no idea wtf) than i thought it would be
03:11:37 <kmc> (because they are shell scripts that invoke rev-parse, or they used to be)
03:13:58 <Bike> maybe someday i will have a job where i have to learn git because everyone else uses it instead of just me
03:48:37 -!- conehead has joined.
03:52:51 -!- nisstyre has joined.
03:56:59 -!- Sorella has quit (Quit: It is tiem!).
03:58:57 -!- tertu_ has quit (Ping timeout: 255 seconds).
03:59:22 -!- tertu has joined.
04:00:49 -!- nisstyre has quit (Ping timeout: 240 seconds).
04:01:00 -!- password2 has joined.
04:05:29 -!- conehead has quit (Quit: Computer has gone to sleep.).
04:11:22 -!- tromp__ has quit (Remote host closed the connection).
04:11:56 -!- tromp_ has joined.
04:12:54 -!- glogbackup has quit (Ping timeout: 255 seconds).
04:15:32 -!- tromp__ has joined.
04:15:46 -!- tromp_ has quit (Read error: Connection reset by peer).
04:15:50 -!- tromp__ has quit (Remote host closed the connection).
04:21:02 -!- tromp_ has joined.
04:27:40 -!- tromp_ has quit (Read error: Connection reset by peer).
04:28:07 -!- glogbackup has quit (Ping timeout: 264 seconds).
04:30:40 -!- conehead has joined.
04:39:27 -!- glogbackup has quit (Ping timeout: 255 seconds).
04:48:27 -!- tertu has quit (Ping timeout: 255 seconds).
04:49:28 -!- tertu has joined.
05:30:33 -!- limitless23 has joined.
05:31:15 -!- limitless23 has quit (Client Quit).
05:31:49 -!- limitless23 has joined.
05:35:30 <kmc> `relcome limitless23
05:35:32 <HackEgo> limitless23: 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>. (For the other kind of esoterica, try #esoteric on irc.dal.net.)
05:35:37 -!- password2 has quit (Ping timeout: 240 seconds).
05:56:09 -!- oklopol has joined.
06:02:36 <Sgeo_> > let welcome = "Hi" in welcome
06:03:03 <Sgeo_> I'm sure there's some way to make idris-ircslave be more colorful
06:03:59 <Sgeo_> > the (t : Type ** t) (String ** "Hello")
06:04:01 <lambdabot> Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c...
06:07:22 <Sgeo_> > the (t1 ** t1) ((t3 ** t3) ** (the (t2 ** t2) (String ** "Hello")))
06:07:24 <lambdabot> Not in scope: `the'Not in scope: `t1'
06:07:24 <lambdabot> `t' (imported from Debug.SimpleReflect),
06:07:24 <lambdabot> `to' (imported from Control.Lens),
06:07:24 <lambdabot> `_1' (imported from Control.Lens)Not in scope: `t1'
06:08:13 <kmc> I really like that both bots respond
06:08:27 <kmc> also I wish lambdabot would come back to ##crypto
06:08:58 <Sgeo_> I can add a spalsh of green
06:09:00 <Sgeo_> > :t the (t1 ** t1) ((t3 ** t3) ** (the (t2 ** t2) (String ** "Hello")))
06:09:00 <idris-ircslave> the (t1 ** t1) ((t3 ** t3) ** the (t2 ** t2) (String ** "Hello")) : (t1 ** t1)
06:09:02 <lambdabot> <hint>:1:1: parse error on input `:'
06:09:37 <Sgeo_> Melvar: What colors am I missing?
06:10:09 <kmc> is ** a tuple constructor?
06:10:16 <Sgeo_> It's a dependent pair constructor
06:10:26 <Sgeo_> Well, not an actual constructor, it's syntax sugar
06:10:37 <lambdabot> <hint>:1:1: parse error on input `:'
06:10:43 <lambdabot> <hint>:1:1: parse error on input `:'
06:11:10 <Sgeo_> The typical example is
06:11:49 <Sgeo_> > the (n : Nat ** Vect n String) (5, ["a", "b", "c", "d", "e"])
06:11:50 <lambdabot> Not in scope: `the'Not in scope: data constructor `Nat'Not in scope: data co...
06:12:05 <Sgeo_> > the (n : Nat ** Vect n String) (5 ** ["a", "b", "c", "d", "e"])
06:12:05 <idris-ircslave> (5 ** ["a", "b", "c", "d", "e"]) : (n ** Vect n String)
06:12:06 <lambdabot> Not in scope: `the'Not in scope: data constructor `Nat'Not in scope: data co...
06:12:46 <Sgeo_> I don't fully understand the implications of when this is useful, but apparently filtering vects returns a dependent tuple instead of just a resulting vector
06:13:10 <Sgeo_> I guess when you want a component of the type to be readable at runtime?
06:15:42 <kmc> and what's "the"?
06:15:46 <shachaf> i've played three games over the past few days. i think i haven't played any others in over a year
06:15:52 <Sgeo_> https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Vect.idr#L285
06:15:55 <shachaf> the is like id with an explicit type argument
06:16:01 <shachaf> it's used kind of like :: in haskell
06:16:13 <shachaf> the : (a : Type) -> a -> a
06:17:00 <Sgeo_> I saw someone use the infix earlier. Int `the` 5 kind of reads backwards
06:18:00 <kmc> (p ** Vect p a) gets inferred to (p : Nat ** Vect p a) ?
06:20:50 <Sgeo_> Hmm, I don't see examples in the Vect prelude lib, but... maybe you could pattern match on the first part of it to know what you can do with the second?
06:21:18 <kmc> makes sense
06:21:34 <fizzie> Conan `the` "Barbarian"
06:22:05 <kmc> one thing I find hard about dependent language syntax is that there's usually a way to leave off either side of (x : t) and it's hard to keep them straight even if I theoreticall understand what's going on
06:26:43 <kmc> "Hello Sir/Madam, I'm Thomas Clark and I'll like to purchase Propane"
06:26:56 <kmc> i get some weird spam
06:27:39 <Bike> hello kmc, i would like to purchase n-decane to go with my chain link fences,
06:30:03 <fizzie> I got spam for Computeroxy -- "an academic website exclusively dedicated to academic careers in schools of electrical and electronic engineering and computer science in Europe, Oceania and the Middle East" -- the other day.
06:30:17 <fizzie> "I found this academic website interesting and I think you would enjoy it too."
06:30:54 <fizzie> Yeah, I'm sure you thought about me personally, "Mark, Lecturer in Computer Science", the guy sending mail to "undisclosed-recipients:;".
06:34:58 <Sgeo_> "This product is property of Lenovo and may not be distributed outside Lenovo"
06:35:12 <Sgeo_> Came with my Lenovo laptop
06:36:43 <kmc> what is it?
06:36:49 <kmc> the product i mean
06:37:56 <Sgeo_> Some VBScript to... do something
06:38:12 <Sgeo_> Not entirely sure what. Something to do with setting up a user guide on Metro, I think
06:38:23 <Sgeo_> "Installing user guide for Support Metro app on Windows 8"
06:43:15 * Sgeo_ 's brain breaks a bit
06:43:16 <Sgeo_> > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("a" ** "foo")
06:43:16 <idris-ircslave> ("a" ** "foo") : (a ** boolElim (intToBool (prim__eqString a "a")) (Delay String) (Delay Int))
06:43:17 <lambdabot> <hint>:1:13: parse error on input `=>'
06:45:15 <Sgeo_> > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("a" ** 5)
06:45:15 <idris-ircslave> Can't resolve type class Num (boolElim (intToBool (prim__eqString "a" "a")) (Delay String) (Delay Int))
06:45:16 <lambdabot> <hint>:1:13: parse error on input `=>'
06:45:33 <Sgeo_> > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("b" ** 5)
06:45:33 <idris-ircslave> ("b" ** 5) : (a ** boolElim (intToBool (prim__eqString a "a")) (Delay String) (Delay Int))
06:45:34 <lambdabot> <hint>:1:13: parse error on input `=>'
06:45:42 <Sgeo_> > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("b" ** "5")
06:45:43 <idris-ircslave> (\a => boolElim (intToBool (prim__eqString a "a")) (Delay String) (Delay Int)) "b"
06:45:43 <lambdabot> <hint>:1:13: parse error on input `=>'
06:45:59 -!- Slereahphone has joined.
06:46:06 <Sgeo_> Slereahphone: you just missed the fun
06:54:35 <kmc> we put the fun in dependently-typed functional programming
07:01:18 <luserdroog> translated the Lukasiewicz logic interpreter to C. https://gist.github.com/luser-dr00g/9542998
07:02:25 <lambdabot> Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c...
07:04:47 -!- ^v has quit (Quit: Leaving).
07:21:06 <fizzie> Is the type type the typest of the types?
07:21:58 <Sgeo_> Idris has a cumulative universe thingy and then hides it
07:22:28 <Sgeo_> So the type of Type is Type 1, the type of Type 1 is Type 2... but Type is also a Type 2, and small types are also Type 2s, and Type 3s, and Type 4s
07:22:40 <Sgeo_> And somehow this lets Idris hide the entire hierarchy from the user
07:23:12 <Sgeo_> So I guess Type becomes whatever Type in the hierarchy is needed in context
07:24:36 -!- limitless23 has quit (Quit: Leaving).
07:24:39 <Bike> > the (Type 17) Type
07:24:39 <idris-ircslave> (input):1:11:Type does not have a function type (Type)
07:24:40 <lambdabot> Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c...
07:24:48 <Bike> well what's the point then!!
07:25:44 -!- FreeFull has quit.
07:28:01 -!- atehwa has quit (Ping timeout: 265 seconds).
07:28:11 -!- Effilry has changed nick to FireFly.
07:28:12 <Sgeo_> You can't actually write Type 1
07:28:28 <Sgeo_> The only place it's ever visible, as far as I understand, is
07:28:32 <lambdabot> <hint>:1:1: parse error on input `:'
07:28:49 <Bike> well what if i want to talk about specifically the type of Int or w/e
07:29:37 -!- atehwa has joined.
07:30:23 <Sgeo_> Good question. Not sure you can
07:31:26 <lambdabot> <hint>:1:1: parse error on input `:'
07:36:04 <Sgeo_> trackpad acting up
07:55:11 -!- Slereahphone has quit (Remote host closed the connection).
07:56:31 -!- Slereahphone has joined.
08:02:19 -!- Slereahphone_ has joined.
08:02:20 -!- Slereahphone has quit (Remote host closed the connection).
08:02:21 -!- Slereahphone_ has changed nick to Slereahphone.
08:05:58 -!- Slereahphone has quit (Remote host closed the connection).
08:06:03 -!- Slereahphone_ has joined.
08:28:22 -!- shikhout has joined.
08:31:43 -!- shikhin has quit (Ping timeout: 264 seconds).
08:31:44 -!- shikhout has changed nick to shikhin.
08:56:51 -!- tertu has quit (Ping timeout: 255 seconds).
09:04:15 <FireFly> up to the next tabstop, as defined by tabs(1)
09:04:23 <FireFly> defaults to every eighth column
09:04:35 <FireFly> if by console mode you mean in a terminal emulator
09:08:32 -!- Slereahphone_ has quit (Quit: Colloquy for iPhone - http://colloquy.mobi).
09:12:05 -!- Slereahphone has joined.
09:17:19 -!- MindlessDrone has joined.
09:24:16 <Jafet> What about apathy mode
09:43:45 -!- conehead has quit (Quit: Computer has gone to sleep.).
09:48:18 -!- Sellyme has quit (Excess Flood).
09:48:55 -!- Sellyme has joined.
09:51:37 -!- glogbackup has quit (Ping timeout: 240 seconds).
10:13:58 -!- boily has joined.
11:03:10 -!- boily has quit (Quit: PENTASYLLABIC CHICKEN).
11:11:38 <Melvar> Sgeo_, Bike: Use ( as a prefix in here so it doesn’t clash with lambdabot.
11:13:02 <Jafet> “In September 1943, Iran declared war on Germany, thus qualifying for membership in the United Nations.”
11:15:00 <Melvar> Sgeo_, Bike: The way the Type hierarchy works is that it builds up a digraph of universe ordering, and checks at the end that it’s consistent (i.e. cycle-free), IIUC.
11:19:20 -!- glogbackup has quit (Read error: Connection reset by peer).
11:25:13 -!- Slereahphone has quit (Ping timeout: 240 seconds).
11:27:54 -!- TodPunk has quit (Ping timeout: 245 seconds).
11:38:50 -!- glogbackup has quit (Ping timeout: 252 seconds).
11:43:38 -!- glogbackup has quit (Ping timeout: 240 seconds).
12:01:45 -!- Sorella has joined.
12:02:58 -!- glogbackup has quit (Ping timeout: 240 seconds).
12:03:43 -!- spiette has quit (Remote host closed the connection).
12:19:37 -!- glogbackup has quit (Ping timeout: 240 seconds).
12:30:23 -!- password2 has joined.
12:36:29 -!- Sgeo_ has quit (Read error: Connection reset by peer).
12:45:08 -!- glogbackup has quit (Ping timeout: 240 seconds).
12:45:36 -!- oerjan has joined.
12:50:36 -!- TodPunk has joined.
12:54:25 -!- glogbackup has quit (Ping timeout: 240 seconds).
13:00:27 -!- glogbackup has quit (Remote host closed the connection).
13:00:45 <quintopia> help my googlebubble thinks i want hockey scores
13:02:00 -!- MindlessDrone has quit (Read error: Operation timed out).
13:03:37 -!- MindlessDrone has joined.
13:04:23 <oerjan> quintopia: i'm sorry you're on thin ice there
13:05:57 <oerjan> managed to edit haskellwiki this time. turns out their fancy layout doesn't work with a non-full-screen browser.
13:06:18 <oerjan> since when do i have a frying pan
13:07:06 <Melvar> Fullscreen? Not just requiring a certain window size?
13:07:07 <oerjan> as in, the edit form got hid under some of the other stuff until i maximized
13:07:54 <oerjan> Melvar: well it doesn't work with my _usual_ window size, which is a little less than full screen because i like to be able to glimpse what's happening in irc.
13:08:20 * Melvar has two monitors for that purpose.
13:09:17 <oerjan> well this is a laptop, on my lap.
13:09:37 -!- glogbackup has quit (Ping timeout: 240 seconds).
13:09:37 <oerjan> i don't think you usually have a two-monitor laptop setup.
13:10:23 <oerjan> (technically it cannot be a laptop because the manual warns against burns if you put it on your lap. hasn't been a problem though, it's cooler than my previous one.)
13:12:00 -!- MindlessDrone has quit (Read error: Connection reset by peer).
13:12:00 <elliott_> I thought infertility was the usual risk.
13:12:18 <oerjan> oh. well i have no plans to breed.
13:12:35 <Melvar> I’m pretty sure that’s just temporary though.
13:12:40 <oerjan> (i actively dislike babies anyway)
13:12:52 <Jafet> http://mashable.com/category/dual-screen-laptop
13:13:10 <oerjan> Melvar: i'm 43, how long is temporary?
13:13:33 <oerjan> oh you mean the infertility.
13:13:53 <Melvar> I meant the infertility, yes.
13:14:48 <Taneb> oerjan, you mean there's never going to be any wild oerjanlings?
13:15:05 <oerjan> Taneb: quite unlikely.
13:27:44 -!- HackEgo has quit (Ping timeout: 264 seconds).
13:32:50 <oerjan> fungot: be careful, someone is picking off bots again
13:32:50 <fungot> oerjan: " and the creator of of yours, you would let the woman with years of combat, probably against a paladin" miko, i have my eye!
13:37:16 <Taneb> I ought to get dressed at some point
13:37:36 <oerjan> you know, _someone_ could have told Sgeo idris-ircslave now supports the ( prefix.
13:38:14 <oerjan> @tell Sgeo please use idris-ircslave's new ( prefix hth
13:38:34 <oerjan> @tell Sgeo_ please use idris-ircslave's new ( prefix hth
13:40:45 * oerjan barely resisted adding "OR DIE" in there.
13:41:10 <Taneb> Is there a nice way to compute the Thue-Morse sequence on a Turing machine
13:41:27 <Taneb> (I'm so glad this channel exists so I can ask questions like that)
13:41:38 -!- glogbackup has quit (Ping timeout: 240 seconds).
13:41:56 <oerjan> well depends what you mean, since turing machines technically have finite output if they ever halt
13:42:34 <oerjan> you could certainly manage to fill up the tape with it without halting.
13:43:01 <Taneb> oerjan, I would like to continuously write the Thue-Morse sequence to the tape
13:44:18 <oerjan> four cell values, call them 0,1,A,B
13:45:03 <oerjan> start by putting 0B on the tape, position yourself just after the B
13:46:07 <oerjan> (1) seek left to a 0 or 1. go one step right.
13:46:53 <oerjan> (2) turn the A or B that is there into 0 or 1, respectively. remember what it was. seek till end of tape.
13:47:25 <oerjan> (3A) put AB on end of tape, go to 1
13:47:37 <oerjan> (3B) put BA on end of tape, go to 1
13:48:55 -!- Slereahphone has joined.
13:54:02 <oerjan> small adjustment, the "position yourself just after the B" could more efficiently be on the 0.
14:18:54 -!- glogbackup has quit (Ping timeout: 252 seconds).
14:23:50 -!- nisstyre has joined.
14:28:58 -!- shikhout has joined.
14:32:00 -!- shikhin has quit (Ping timeout: 255 seconds).
14:32:02 -!- shikhout has changed nick to shikhin.
14:57:55 -!- nooodl has joined.
14:58:29 <fizzie> oerjan: Do they sell two-monitor laptops for people with two heads?
14:58:50 <fizzie> Oh, I see Jafet already answered that.
14:59:46 <fizzie> Well, it doesn't exactly mention two-headed people.
14:59:55 <fizzie> But I'm sure it's implied.
15:00:16 <Jafet> I imagine those laptops are marketed beyond the very limited dicephalic demographic.
15:00:22 <oerjan> the top picture seems broken
15:02:02 <int-e> fizzie: the Beeblebrox market segment is a bit small, methinks.
15:02:07 <oerjan> i think google mustn't have quite the right picture of me, it's showing me an ad for farming equipment.
15:02:57 * int-e is late and redundant, as usual. *sigh*
15:03:16 <oerjan> int-e: well it's easy to be redundant when you have two heads
15:07:49 -!- spiette has joined.
15:08:01 -!- glogbackup has quit (Ping timeout: 240 seconds).
15:10:33 -!- ^v has joined.
15:24:04 -!- Slereahphone has quit (Remote host closed the connection).
15:27:44 -!- AnotherTest has joined.
15:32:37 -!- glogbackup has quit (Ping timeout: 252 seconds).
15:33:13 -!- password2 has quit (Ping timeout: 240 seconds).
15:34:48 -!- chaiomanot has joined.
15:39:04 -!- password2 has joined.
15:42:53 -!- Slereahphone has joined.
15:48:35 -!- nooodl has quit (Ping timeout: 252 seconds).
15:49:52 -!- erdic has quit (Remote host closed the connection).
15:50:24 -!- erdic has joined.
15:51:53 -!- Slereahphone has quit (Ping timeout: 253 seconds).
15:54:54 -!- Slereahphone has joined.
16:00:47 -!- shikhout has joined.
16:02:54 -!- shikhin has quit (Ping timeout: 255 seconds).
16:02:55 -!- shikhout has changed nick to shikhin.
16:13:06 -!- nooodl has joined.
16:29:09 -!- glogbackup has quit (Remote host closed the connection).
16:42:53 <Bike> http://www.theguardian.com/technology/2014/mar/14/mtgox-knowingly-traded-non-existent-bitcoins-for-two-weeks-filing-shows ha ha
16:46:01 -!- oerjan has quit (Quit: Fnord).
17:38:55 -!- nisstyre has quit (Read error: Operation timed out).
17:45:58 -!- password2 has quit (Ping timeout: 240 seconds).
17:49:14 -!- Sellyme has quit (Excess Flood).
17:50:55 -!- Sellyme has joined.
18:06:33 -!- Slereah__ has joined.
18:10:14 -!- ^v has quit (Read error: Connection reset by peer).
18:10:39 -!- ^v has joined.
18:16:16 -!- conehead has joined.
18:22:08 -!- FreeFull has joined.
18:22:13 -!- FreeFull has quit (Changing host).
18:22:13 -!- FreeFull has joined.
18:38:24 <luserdroog> For the dual-screen laptop, it would be nice to reduce the width of the framing down the middle.
18:51:04 <kmc> Lenovo sold a W-series ThinkPad with a second smaller screen that pops out the side of the first one
18:51:22 <kmc> it also had a Wacom drawing tablet in the wrist rest, as well as a color calibration sensor for the main screen
18:57:23 <olsner> sounds nice, but slightly crazy
19:13:10 -!- nisstyre has joined.
19:22:08 -!- nisstyre has quit (Ping timeout: 240 seconds).
19:53:24 -!- Bike has quit (Quit: later).
20:07:53 -!- password2 has joined.
20:11:44 -!- password2 has quit (Client Quit).
20:12:13 -!- password2 has joined.
20:12:31 -!- password2 has quit (Client Quit).
20:14:09 -!- password2 has joined.
20:19:38 -!- AnotherTest has quit (Ping timeout: 240 seconds).
20:21:54 -!- password2_ has joined.
20:23:04 -!- erdic has quit (Remote host closed the connection).
20:23:32 -!- erdic has joined.
20:28:25 -!- nooodl has quit (Ping timeout: 240 seconds).
20:31:47 -!- ^v has quit (Quit: Leaving).
20:37:23 -!- vravn has quit (Excess Flood).
20:41:18 -!- vravn has joined.
20:50:22 -!- nooodl has joined.
20:57:03 -!- password2_ has quit (Quit: Leaving).
20:57:28 -!- password2 has quit (Remote host closed the connection).
21:01:20 -!- spiette has quit (Quit: :qa!).
21:06:10 -!- vravn has quit (Excess Flood).
21:08:18 -!- vravn has joined.
21:18:16 -!- vravn has quit (Excess Flood).
21:19:18 -!- vravn has joined.
21:42:12 -!- von_cheam has joined.
21:42:37 -!- von_cheam has quit (Quit: Leaving.).
21:47:21 -!- FireFly has quit (Excess Flood).
21:48:34 -!- FireFly has joined.
21:52:45 -!- nisstyre has joined.
21:54:03 -!- drlemon has joined.
21:55:11 -!- nisstyre_ has joined.
21:57:34 -!- nooodl_ has joined.
21:58:01 -!- nooodl has quit (Ping timeout: 240 seconds).
21:59:24 -!- oerjan has joined.
22:00:52 -!- shikhout has joined.
22:02:07 -!- boily has joined.
22:03:48 -!- shikhin has quit (Ping timeout: 255 seconds).
22:03:50 -!- shikhout has changed nick to shikhin.
22:11:03 -!- luserdroog has quit (Ping timeout: 245 seconds).
22:13:21 -!- metasepia has joined.
22:14:08 -!- von_cheam has joined.
22:14:18 <boily> `relcome von_cheam
22:14:37 <boily> Gregor: the gregorbots, they are dead.
22:17:00 <fungot> FireFly: it's the crown, lass, no sense being angry about it now, and he was in the army, too true, and v's still there now and you can.
22:17:50 <boily> FireFly: you're a lass?
22:19:51 -!- itsy has joined.
22:21:12 <boily> oerjan: he didn't answer while he was having instant surgery.
22:21:27 -!- nooodl__ has joined.
22:24:34 -!- nooodl_ has quit (Ping timeout: 240 seconds).
22:26:23 <boily> oerjan: today, I read an old blog post showing how to implement monads in Java. it wasn't pretty.
22:30:33 <fizzie> boily: Was it http://logicaltypes.blogspot.fi/2011/09/monads-in-java.html ?
22:31:56 <fizzie> I think that was discussed either here or nearby.
22:32:21 <boily> are you implying that there are circumesöteric channels?
22:33:07 <fizzie> I can only find the "Monads in plain JavaScript" post by gwepping.
22:35:37 -!- von_cheam has left.
22:41:57 <oerjan> pretty sure #haskell is a circumesöteric channel, in any case
22:44:34 <fizzie> The evidence for that is circumstantial.
22:45:06 <oerjan> that's just circumventing the facts
22:50:06 <olsner> aren't you guys just circumnavigating the topic now?
22:53:12 <olsner> hmm, throws Failure ... is that the Java-monad counterpart of fail?
22:59:22 <fizzie> I can't really be bothered to read through it all -- was the Java monad the one where you can't have "Just null", or am I thinking of something else?
23:09:12 <boily> (meanwhile, duck tape with penguins on it? → https://tw-projects.s3.amazonaws.com/twduckbrand/prod/images/products/penguin-duct-tape.jpg)
23:09:47 <boily> fizzie: I haven't read through it all, but I wouldn't be surprised. Java nulls are very thoroughly pernicious.
23:10:37 <quintopia> i went to buy plain old duct tape at walmart once and could only find spongebob, hello kitty, and bacon
23:10:54 <boily> nooooo! why didn't you choose the hello kitty one?
23:11:58 <boily> I like my duck tape gray. same thing with my coffee: black.
23:12:06 <boily> (and my bagels: poppyseed.)
23:12:13 -!- Sgeo has joined.
23:12:14 -!- nisstyre_ has quit (Quit: WeeChat 0.4.3).
23:14:42 <Sgeo> > "please don't kill me oerjan"
23:15:48 * boily is all sparkly-anime-eyes
23:17:40 <boily> ~eval "please don't kill me either twh"
23:18:18 <Sgeo> @messages-public
23:18:22 <Sgeo> @messages-loud
23:18:22 <lambdabot> oerjan said 9h 40m 7s ago: please use idris-ircslave's new ( prefix hth
23:18:35 <Sgeo> ( Integer + Integer
23:19:00 -!- yorick has joined.
23:19:27 <Sgeo> > the Nat (-10)
23:19:28 <lambdabot> Not in scope: `the'Not in scope: data constructor `Nat'
23:20:01 -!- Slereah__ has quit (Ping timeout: 240 seconds).
23:20:25 <quintopia> boily: i prefer black heavy duty duct tape
23:21:14 <boily> quintopia: what kind of tape is that? the only two kind of black heavy duty tape I know about are «tape électrique» and that textured one you put on hockey sticks.
23:21:30 -!- Slereah_ has joined.
23:21:31 <oerjan> ( the Int 99999999999999999999999999999999999
23:21:32 <boily> (yes. we call it «tape» in French.)
23:21:46 <quintopia> boily: it's like duct tape, but black rather than silver, and thicker and tougher and harder to tear
23:21:55 <oerjan> boily: we call it "teip" in norwegian hth
23:22:13 <Sgeo> Wonder if this could be used to prove 0=1
23:22:25 <boily> quintopia: hmm... my curiosity is titillated.
23:22:37 <boily> oerjan: makes sense.
23:22:42 <Sgeo> Maybe not, once you have a Nat you always have something 0 or greater
23:22:46 <oerjan> Sgeo: you realize that this is just how subtraction is defined on Nats, no?
23:22:55 <Sgeo> What you do before it may be irrelev... o.O
23:22:58 <quintopia> Sgeo: uh...no. in practice, it's illegal to do 2-3 in the naturals
23:23:01 <Sgeo> I thought Idris was in the wrong
23:23:20 <boily> > log 3136633892082024447 / log 2
23:23:31 <elliott_> Sgeo: no because the proof would rely on the definition of -
23:23:51 <boily> ~duck 3136633892082024447
23:25:03 <quintopia> boily: http://m.shoplet.com/Duck-Heavy-Duty-Duct-Tape/DUCCD3BLACK/
23:25:49 <oerjan> @run 99999999999999999999999999999999999 :: Int64
23:26:23 <Sgeo> I can't write a useful {n : Nat} -> Vect n a -> Nat, can I?
23:26:54 <Sgeo> Or.. something like that, to determine the size of a Vect whose size is unknown at compile-time?
23:28:43 <boily> quintopia: the link, it doesn't work.
23:29:08 <Sgeo> I assume that doing that (wanting the size that's known only at runtime) is why dependent pairs exist?
23:29:17 <quintopia> boily: i cut a bunch of stuff off the end of it. try cutting more stuff off
23:29:40 <Sgeo> ( the (Vect n a) [1,2,3]
23:29:51 <Sgeo> ( the (Vect _ _) [1,2,3]
23:30:11 <oerjan> ( the Integer 99999999999999999999999999999999999
23:30:24 <Sgeo> ( the (_ ** (Vect _ _)) [1,2,3]
23:30:37 <Sgeo> ( the (_ ** (Vect _ _)) (_ ** [1,2,3])
23:30:52 <Sgeo> ( the (n ** (Vect n _)) (_ ** [1,2,3])
23:30:52 <idris-ircslave> Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.::
23:31:13 <Sgeo> ( the (n ** (Vect n _)) (_ ** with Vect [1,2,3])
23:31:45 <boily> quintopia: it still doesn't work. I am saddened :(
23:31:50 <Sgeo> ( the (n ** Vect n String) (_ ** ["1", "2", "3"])
23:33:35 <Sgeo> oerjan: (t ** t)s are useless, right? Or are they not useless somehow
23:34:02 <oerjan> how do you find the first element of a **
23:34:17 <FreeFull> Sgeo: A value whose type is dependent on itself?
23:34:54 <lambdabot> Couldn't match expected type `(a0, b0)' with actual type `[t0]'
23:35:08 <lambdabot> No instance for (GHC.Show.Show a0)
23:35:09 <lambdabot> arising from a use of `M707592794521593570827224.show_M7075927945215935708...
23:35:09 <lambdabot> The type variable `a0' is ambiguous
23:35:09 <lambdabot> Possible fix: add a type signature that fixes these type variable(s)
23:35:09 <lambdabot> Note: there are several potential instances:
23:35:20 <oerjan> ( (\v -> let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3]
23:35:21 <FreeFull> Oh, lambdabot + idris-ircslave
23:35:33 <oerjan> oops how do lambdas work
23:36:06 -!- Sgeo_ has joined.
23:36:11 <oerjan> ( (\v => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3]
23:36:14 <idris-ircslave> (input):1:58:Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.::
23:36:41 <oerjan> ( (\(v : Vect _ _) => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3]
23:36:42 <idris-ircslave> (\(v : Vect _ _) => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3]<>
23:37:01 <oerjan> ok i'm clearly not understanding this
23:37:24 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-ircslave ( , jconn ) , blsqbot !
23:37:35 <oerjan> FreeFull: because that is finally now matchin hth
23:38:27 * Sgeo_ glares angrily at Quassel
23:39:52 -!- erdic_ has joined.
23:40:12 <Sgeo_> ( let data Foo = Bar | Baz in Foo
23:40:28 <Sgeo_> Isn't there a language that allows local data definitions?
23:44:34 -!- Sgeo has quit (*.net *.split).
23:44:34 -!- erdic has quit (*.net *.split).
23:44:35 -!- glogbackup has quit (*.net *.split).
23:44:35 -!- Slereahphone has quit (*.net *.split).
23:44:35 -!- FireFly has quit (*.net *.split).
23:45:04 -!- erdic_ has quit (Changing host).
23:45:04 -!- erdic_ has joined.
23:49:51 -!- mysanthrop has joined.
23:50:16 <Sgeo_> ( the (a ** b) (5 ** "Hi")
23:50:47 -!- atehwa_ has joined.
23:51:01 -!- erdic has joined.
23:51:30 -!- tromp_ has joined.
23:53:23 <oerjan> Melvar: Sgeo_ killed yer bot hth
23:54:24 -!- fizzie` has joined.
23:54:42 <kmc> just because we don't feel flesh doesn't mean we don't fear death
23:55:54 -!- erdic_ has quit (*.net *.split).
23:55:56 -!- atehwa has quit (*.net *.split).
23:55:56 -!- Frooxius has quit (*.net *.split).
23:55:56 -!- myname has quit (*.net *.split).
23:55:56 -!- idris-ircslave has quit (*.net *.split).
23:55:56 -!- trout has quit (*.net *.split).
23:55:56 -!- pikhq has quit (*.net *.split).
23:55:56 -!- trn has quit (*.net *.split).
23:55:56 -!- fizzie has quit (*.net *.split).
23:58:08 -!- fizzie` has changed nick to fizzie.
23:58:30 -!- pikhq has joined.
23:59:18 -!- sebbu2 has joined.
23:59:50 -!- sebbu2 has quit (Changing host).
23:59:50 -!- sebbu2 has joined.