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:19:56 Taneb, i know a guy who says he made one out of lego 00:22:43 -!- Sgeo_ has joined. 00:24:30 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:34:36 hap-pi day 00:45:37 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 oerjan: staws? is that like a Norwegian Mapole? 01:33:25 no, that would be stav 01:34:05 * boily is confused 01:34:43 what sort of bizarre rettaws is that 01:35:17 https://en.wiktionary.org/wiki/stav#Swedish in lack of a norwegian version 01:35:46 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 (or is it suddenlightened?) 01:40:07 shachaf: thachaf. 01:40:26 oerjan: i didn't look at it long enough to see that it wasn't just reversed 01:40:48 it would only have taken one letter to see that 01:41:03 almost any letter would have worked 01:41:20 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 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 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 print!(" \x1b[36m{:s}\x1b[0m='\x1b[34m{:s}\x1b[0m'", attr.name, attr.value); 02:52:04 there are a lot of different languages packed into that one line of code 02:58:31 today i tried to invoke a shell on windows through matlab and i think it gave me VT100 control codes 02:58:34 a disheartening experience 02:58:44 that looked a lot like that string >_> 02:58:57 yes 02:59:04 those are VT100 control codes, or ECMA-48 codes anyway 02:59:12 I don't remember if the actual VT100 had color, probably not 02:59:37 oh. lol i was just shallowly seeing unclosed square brackets 03:00:03 it's a good tip-off 03:01:03 ECMA-48 apparently predates the VT100. 03:01:12 but not the latest edition, which is from 1991 03:01:31 -!- luserdroog has joined. 03:01:46 Ah sweet, I found the VT100 manual. 03:01:46 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 SIPB owns an actual VT100, or is it a VT220 03:02:08 they had it hooked up to a Raspberry Pi, which fit easily within the case 03:02:10 it was cute 03:02:37 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:47 ohhh 03:02:53 i think it printed as like... ~V[ or something 03:03:29 It seems that it did not *support* color, but the VT100 ignores unknown character attributes. 03:03:35 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 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 but mostly people don't 03:03:58 So on a VT100 you don't get color *display*, but the color codes work just fine. 03:04:02 (i.e. "do nothing") 03:04:24 presumably on a UTF-8 terminal you would have to write 0xC2 0x9B anyway... 03:05:51 Thankfully all the character attributes are parameters to \ 03:06:03 the "m" sequence. 03:06:18 Which means that it's actually quite simple for a terminal to no-op support the colors. 03:06:25 And apparently the VT100 did just that. 03:06:26 oh as long as i'm complaining i found out that cmd.exe is pretty much terrible 03:06:28 Which is awesome. 03:06:43 Bike: yes. you want a better shell (like MSYS bash) and a better terminal emulator (like Mintty) 03:06:58 i invoked a program by quoting the path and it reported the program as having the quote character in it 03:07:25 bash i have, but not a better tty. hoooopefully i won't be using shell enough to want that, but 03:07:27 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 which might be how the hardware worked 03:07:36 Probably. 03:07:51 of course, msys doesn't have man pages :( oh well 03:09:09 also: does anyone know what the hell git rev-parse is 03:10:08 "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 "Note that .. would mean HEAD..HEAD which is an empty range that is both reachable and unreachable from HEAD." 03:10:49 Bike: it describes the syntax you can use to name git objects, mainly commits 03:11:15 the actual rev-parse command is meant for use from scripts 03:11:26 but many of the user-facing commands accept the same syntax 03:11:33 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 (because they are shell scripts that invoke rev-parse, or they used to be) 03:13:58 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:32:17 hello 05:35:30 `relcome limitless23 05:35:32 ​limitless23: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: . (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 > let welcome = "Hi" in welcome 06:02:36 "Hi" : String 06:02:37 "Hi" 06:03:03 I'm sure there's some way to make idris-ircslave be more colorful 06:03:59 > the (t : Type ** t) (String ** "Hello") 06:03:59 (String ** "Hello") : (t ** t) 06:04:01 Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c... 06:07:22 > the (t1 ** t1) ((t3 ** t3) ** (the (t2 ** t2) (String ** "Hello"))) 06:07:23 ((t3 ** t3) ** (String ** "Hello")) : (t1 ** t1) 06:07:24 Not in scope: `the'Not in scope: `t1' 06:07:24 Perhaps you meant one of these: 06:07:24 `t' (imported from Debug.SimpleReflect), 06:07:24 `to' (imported from Control.Lens), 06:07:24 `_1' (imported from Control.Lens)Not in scope: `t1' 06:08:13 I really like that both bots respond 06:08:27 also I wish lambdabot would come back to ##crypto 06:08:58 I can add a spalsh of green 06:09:00 > :t the (t1 ** t1) ((t3 ** t3) ** (the (t2 ** t2) (String ** "Hello"))) 06:09:00 the (t1 ** t1) ((t3 ** t3) ** the (t2 ** t2) (String ** "Hello")) : (t1 ** t1) 06:09:02 :1:1: parse error on input `:' 06:09:37 Melvar: What colors am I missing? 06:10:09 is ** a tuple constructor? 06:10:16 It's a dependent pair constructor 06:10:26 Well, not an actual constructor, it's syntax sugar 06:10:36 > :t Exists 06:10:36 Exists : (a : Type) -> (a -> Type) -> Type 06:10:37 :1:1: parse error on input `:' 06:10:42 > :t Ex_intro 06:10:43 :1:1: parse error on input `:' 06:10:43 Ex_intro : (x : a) -> (P x) -> Exists a P 06:11:10 The typical example is 06:11:49 > the (n : Nat ** Vect n String) (5, ["a", "b", "c", "d", "e"]) 06:11:49 Can't unify 06:11:50 (A, B) 06:11:50 with 06:11:50 (n ** Vect n String) 06:11:50 Specifically:↵… 06:11:50 Not in scope: `the'Not in scope: data constructor `Nat'Not in scope: data co... 06:12:05 > the (n : Nat ** Vect n String) (5 ** ["a", "b", "c", "d", "e"]) 06:12:05 (5 ** ["a", "b", "c", "d", "e"]) : (n ** Vect n String) 06:12:06 Not in scope: `the'Not in scope: data constructor `Nat'Not in scope: data co... 06:12:46 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 I guess when you want a component of the type to be readable at runtime? 06:15:22 i ascended nethack today 06:15:25 why did i even play 06:15:42 and what's "the"? 06:15:46 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 https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Vect.idr#L285 06:15:55 the is like id with an explicit type argument 06:15:59 ok 06:16:01 it's used kind of like :: in haskell 06:16:13 the : (a : Type) -> a -> a 06:16:17 the Int 5 06:16:32 yeah 06:17:00 I saw someone use the infix earlier. Int `the` 5 kind of reads backwards 06:18:00 (p ** Vect p a) gets inferred to (p : Nat ** Vect p a) ? 06:18:23 I believe so 06:20:50 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 makes sense 06:21:34 Conan `the` "Barbarian" 06:22:05 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 "Hello Sir/Madam, I'm Thomas Clark and I'll like to purchase Propane" 06:26:56 i get some weird spam 06:27:39 hello kmc, i would like to purchase n-decane to go with my chain link fences, 06:29:26 * Sgeo_ wants antipane 06:30:03 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 "I found this academic website interesting and I think you would enjoy it too." 06:30:54 Yeah, I'm sure you thought about me personally, "Mark, Lecturer in Computer Science", the guy sending mail to "undisclosed-recipients:;". 06:34:58 "This product is property of Lenovo and may not be distributed outside Lenovo" 06:35:12 Came with my Lenovo laptop 06:36:41 haha 06:36:43 what is it? 06:36:49 the product i mean 06:37:56 Some VBScript to... do something 06:38:12 Not entirely sure what. Something to do with setting up a user guide on Metro, I think 06:38:23 "Installing user guide for Support Metro app on Windows 8" 06:43:15 * Sgeo_ 's brain breaks a bit 06:43:16 > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("a" ** "foo") 06:43:16 ("a" ** "foo") : (a ** boolElim (intToBool (prim__eqString a "a")) (Delay String) (Delay Int)) 06:43:17 :1:13: parse error on input `=>' 06:45:15 > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("a" ** 5) 06:45:15 Can't resolve type class Num (boolElim (intToBool (prim__eqString "a" "a")) (Delay String) (Delay Int)) 06:45:16 :1:13: parse error on input `=>' 06:45:33 > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("b" ** 5) 06:45:33 ("b" ** 5) : (a ** boolElim (intToBool (prim__eqString a "a")) (Delay String) (Delay Int)) 06:45:34 :1:13: parse error on input `=>' 06:45:42 > let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("b" ** "5") 06:45:43 Can't unify 06:45:43 String 06:45:43 with 06:45:43 (\a => boolElim (intToBool (prim__eqString a "a")) (Delay String) (Delay Int)) "b" 06:45:43 Specifically:↵… 06:45:43 :1:13: parse error on input `=>' 06:45:46 * Sgeo_ stops 06:45:59 -!- Slereahphone has joined. 06:46:06 Slereahphone: you just missed the fun 06:54:35 we put the fun in dependently-typed functional programming 06:56:47 It can't be that fun because 06:56:55 I don't know what it means 07:01:18 translated the Lukasiewicz logic interpreter to C. https://gist.github.com/luser-dr00g/9542998 07:02:24 > the Type Type 07:02:24 Type : Type 07:02:25 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 Is the type type the typest of the types? 07:21:58 Idris has a cumulative universe thingy and then hides it 07:22:28 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 And somehow this lets Idris hide the entire hierarchy from the user 07:23:12 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 > the (Type 17) Type 07:24:39 (input):1:11:Type does not have a function type (Type) 07:24:40 Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c... 07:24:48 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 You can't actually write Type 1 07:28:13 etc. 07:28:28 The only place it's ever visible, as far as I understand, is 07:28:31 > :t Type 07:28:32 Type : Type 1 07:28:32 :1:1: parse error on input `:' 07:28:49 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 Good question. Not sure you can 07:31:25 > :t Int 07:31:25 Int : Type 07:31:26 :1:1: parse error on input `:' 07:35:57 help 07:36:04 trackpad acting up 07:36:52 Fixed 07:36:56 Thanks to a mouse 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:40:04 What's the size of a tab in console mode 08:40:21 In character spaces 08:56:51 -!- tertu has quit (Ping timeout: 255 seconds). 09:04:15 up to the next tabstop, as defined by tabs(1) 09:04:23 defaults to every eighth column 09:04:35 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 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 Sgeo_, Bike: Use ( as a prefix in here so it doesn’t clash with lambdabot. 11:13:02 “In September 1943, Iran declared war on Germany, thus qualifying for membership in the United Nations.” 11:15:00 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:16:31 > 47/15 12:16:31 3.1333333333333333 : Float 12:16:32 3.1333333333333333 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 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 quintopia: i'm sorry you're on thin ice there 13:05:04 ug 13:05:17 hand me your frying pan please 13:05:57 managed to edit haskellwiki this time. turns out their fancy layout doesn't work with a non-full-screen browser. 13:06:18 since when do i have a frying pan 13:06:24 sounds compatible 13:07:06 Fullscreen? Not just requiring a certain window size? 13:07:07 as in, the edit form got hid under some of the other stuff until i maximized 13:07:54 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 well this is a laptop, on my lap. 13:09:37 -!- glogbackup has quit (Ping timeout: 240 seconds). 13:09:37 i don't think you usually have a two-monitor laptop setup. 13:09:40 * Melvar nods. 13:10:23 (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 I thought infertility was the usual risk. 13:12:18 oh. well i have no plans to breed. 13:12:35 I’m pretty sure that’s just temporary though. 13:12:40 (i actively dislike babies anyway) 13:12:52 http://mashable.com/category/dual-screen-laptop 13:13:10 Melvar: i'm 43, how long is temporary? 13:13:33 oh you mean the infertility. 13:13:53 I meant the infertility, yes. 13:14:06 good, good 13:14:48 oerjan, you mean there's never going to be any wild oerjanlings? 13:15:05 Taneb: quite unlikely. 13:27:44 -!- HackEgo has quit (Ping timeout: 264 seconds). 13:32:50 fungot: be careful, someone is picking off bots again 13:32:50 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 I ought to get dressed at some point 13:37:36 you know, _someone_ could have told Sgeo idris-ircslave now supports the ( prefix. 13:38:14 @tell Sgeo please use idris-ircslave's new ( prefix hth 13:38:14 Consider it noted. 13:38:34 @tell Sgeo_ please use idris-ircslave's new ( prefix hth 13:38:35 Consider it noted. 13:40:45 * oerjan barely resisted adding "OR DIE" in there. 13:41:10 Is there a nice way to compute the Thue-Morse sequence on a Turing machine 13:41:27 (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 well depends what you mean, since turing machines technically have finite output if they ever halt 13:42:34 you could certainly manage to fill up the tape with it without halting. 13:43:01 oerjan, I would like to continuously write the Thue-Morse sequence to the tape 13:44:18 four cell values, call them 0,1,A,B 13:45:03 start by putting 0B on the tape, position yourself just after the B 13:46:07 (1) seek left to a 0 or 1. go one step right. 13:46:53 (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 (3A) put AB on end of tape, go to 1 13:47:37 (3B) put BA on end of tape, go to 1 13:47:46 Taneb: simple enough? 13:48:41 Yes 13:48:55 -!- Slereahphone has joined. 13:49:00 Thank you 13:50:59 you're welcome 13:54:02 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 oerjan: Do they sell two-monitor laptops for people with two heads? 14:58:50 Oh, I see Jafet already answered that. 14:59:23 ooh i missed that 14:59:46 Well, it doesn't exactly mention two-headed people. 14:59:55 But I'm sure it's implied. 15:00:16 I imagine those laptops are marketed beyond the very limited dicephalic demographic. 15:00:22 the top picture seems broken 15:02:02 fizzie: the Beeblebrox market segment is a bit small, methinks. 15:02:07 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 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 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 For the dual-screen laptop, it would be nice to reduce the width of the framing down the middle. 18:51:04 Lenovo sold a W-series ThinkPad with a second smaller screen that pops out the side of the first one 18:51:22 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 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 `relcome von_cheam 22:14:37 Gregor: the gregorbots, they are dead. 22:17:00 fungot: staying alive? 22:17:00 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:08 dubious. 22:17:50 FireFly: you're a lass? 22:19:40 alas, no answer 22:19:51 -!- itsy has joined. 22:20:45 gørjand kveld. 22:20:56 I don't think so 22:20:59 No last I checked, anyway 22:21:12 oerjan: he didn't answer while he was having instant surgery. 22:21:27 -!- nooodl__ has joined. 22:21:36 boily: fiendish 22:21:56 goedenavnooodln. 22:22:13 boilyn soir 22:22:55 *boilynsoir 22:24:34 -!- nooodl_ has quit (Ping timeout: 240 seconds). 22:26:23 oerjan: today, I read an old blog post showing how to implement monads in Java. it wasn't pretty. 22:30:33 boily: Was it http://logicaltypes.blogspot.fi/2011/09/monads-in-java.html ? 22:31:44 fizzie: it was. 22:31:56 I think that was discussed either here or nearby. 22:32:21 are you implying that there are circumesöteric channels? 22:33:07 I can only find the "Monads in plain JavaScript" post by gwepping. 22:35:37 -!- von_cheam has left. 22:41:57 pretty sure #haskell is a circumesöteric channel, in any case 22:44:34 The evidence for that is circumstantial. 22:45:06 that's just circumventing the facts 22:50:06 aren't you guys just circumnavigating the topic now? 22:53:12 hmm, throws Failure ... is that the Java-monad counterpart of fail? 22:59:22 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:00:44 helloily 23:07:51 quinthellopia! 23:09:12 (meanwhile, duck tape with penguins on it? → https://tw-projects.s3.amazonaws.com/twduckbrand/prod/images/products/penguin-duct-tape.jpg) 23:09:47 fizzie: I haven't read through it all, but I wouldn't be surprised. Java nulls are very thoroughly pernicious. 23:10:16 there is every kind of duct tape 23:10:37 i went to buy plain old duct tape at walmart once and could only find spongebob, hello kitty, and bacon 23:10:40 i went with bacon 23:10:54 nooooo! why didn't you choose the hello kitty one? 23:11:58 I like my duck tape gray. same thing with my coffee: black. 23:12:06 (and my bagels: poppyseed.) 23:12:13 -!- Sgeo has joined. 23:12:14 -!- nisstyre_ has quit (Quit: WeeChat 0.4.3). 23:14:42 > "please don't kill me oerjan" 23:14:43 "please don't kill me oerjan" 23:14:44 "please don't kill me oerjan" : String 23:15:37 ooooooooh... 23:15:48 * boily is all sparkly-anime-eyes 23:17:40 ~eval "please don't kill me either twh" 23:17:40 Error (127): 23:17:50 ... 23:18:18 @messages-public 23:18:18 Unknown command, try @list 23:18:22 @messages-loud 23:18:22 oerjan said 9h 40m 7s ago: please use idris-ircslave's new ( prefix hth 23:18:27 ( 1 + 1 23:18:27 2 : Integer 23:18:35 ( Integer + Integer 23:18:35 Can't resolve type class Num Type 23:18:54 ( S -1 23:18:54 Can't resolve type class Num (Nat -> Nat) 23:19:00 -!- yorick has joined. 23:19:02 ( S (-1) 23:19:02 1 : Nat 23:19:08 uh 23:19:12 o_0 23:19:27 > the Nat (-10) 23:19:27 0 : Nat 23:19:28 Not in scope: `the'Not in scope: data constructor `Nat' 23:19:31 oops 23:20:01 -!- Slereah__ has quit (Ping timeout: 240 seconds). 23:20:25 boily: i prefer black heavy duty duct tape 23:21:06 ( the Nat (2-3) 23:21:06 0 : Nat 23:21:14 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:17 ( the Int (2-3) 23:21:17 -1 : Int 23:21:30 -!- Slereah_ has joined. 23:21:31 ( the Int 99999999999999999999999999999999999 23:21:31 3136633892082024447 : Int 23:21:32 (yes. we call it «tape» in French.) 23:21:46 boily: it's like duct tape, but black rather than silver, and thicker and tougher and harder to tear 23:21:55 boily: we call it "teip" in norwegian hth 23:22:13 Wonder if this could be used to prove 0=1 23:22:25 quintopia: hmm... my curiosity is titillated. 23:22:37 oerjan: makes sense. 23:22:42 Maybe not, once you have a Nat you always have something 0 or greater 23:22:46 Sgeo: you realize that this is just how subtraction is defined on Nats, no? 23:22:55 What you do before it may be irrelev... o.O 23:22:58 Sgeo: uh...no. in practice, it's illegal to do 2-3 in the naturals 23:23:01 I thought Idris was in the wrong 23:23:20 > log 3136633892082024447 / log 2 23:23:20 61.44392285561078 : Float 23:23:21 61.44392285561078 23:23:31 Sgeo: no because the proof would rely on the definition of - 23:23:51 ~duck 3136633892082024447 23:23:51 3136633892082024447 23:25:03 boily: http://m.shoplet.com/Duck-Heavy-Duty-Duct-Tape/DUCCD3BLACK/ 23:25:49 @run 99999999999999999999999999999999999 :: Int64 23:25:50 3136633892082024447 23:26:08 it's just mod 2^64 23:26:23 I can't write a useful {n : Nat} -> Vect n a -> Nat, can I? 23:26:54 Or.. something like that, to determine the size of a Vect whose size is unknown at compile-time? 23:27:32 ( :t Vect 23:27:32 Prelude.Vect.Vect : Nat -> Type -> Type 23:27:56 ( :t Vect 2 23:27:56 Vect (fromInteger 2) : Type -> Type 23:28:14 ( :t Vect 2 Bool 23:28:14 Vect (fromInteger 2) Bool : Type 23:28:19 ( Vect 2 Bool 23:28:19 Vect 2 Bool : Type 23:28:43 quintopia: the link, it doesn't work. 23:28:57 oerjan: meh :/ 23:29:08 I assume that doing that (wanting the size that's known only at runtime) is why dependent pairs exist? 23:29:17 boily: i cut a bunch of stuff off the end of it. try cutting more stuff off 23:29:40 ( the (Vect n a) [1,2,3] 23:29:41 (input):1:11:No such variable n 23:29:51 ( the (Vect _ _) [1,2,3] 23:29:51 [1, 2, 3] : Vect 3 Integer 23:30:11 ( the Integer 99999999999999999999999999999999999 23:30:13 99999999999999999999999999999999999 : Integer 23:30:24 ( the (_ ** (Vect _ _)) [1,2,3] 23:30:25 Can't unify 23:30:25 Vect (S n) a 23:30:25 with 23:30:25 (x ** Vect __pi_arg __pi_arg1) 23:30:25 Specifically:↵… 23:30:37 ( the (_ ** (Vect _ _)) (_ ** [1,2,3]) 23:30:38 Can't unify 23:30:38 Exists a P 23:30:38 with 23:30:38 (x ** Vect __pi_arg __pi_arg1) 23:30:38 Specifically:↵… 23:30:52 ( the (n ** (Vect n _)) (_ ** [1,2,3]) 23:30:52 Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.:: 23:31:13 ( the (n ** (Vect n _)) (_ ** with Vect [1,2,3]) 23:31:13 Can't unify 23:31:13 Vect 3 Integer 23:31:13 with 23:31:13 (\n => Vect n [__]) x 23:31:13 Specifically:↵… 23:31:45 quintopia: it still doesn't work. I am saddened :( 23:31:50 ( the (n ** Vect n String) (_ ** ["1", "2", "3"]) 23:31:50 (3 ** ["1", "2", "3"]) : (n ** Vect n String) 23:33:04 huh 23:33:35 oerjan: (t ** t)s are useless, right? Or are they not useless somehow 23:34:02 how do you find the first element of a ** 23:34:17 Sgeo: A value whose type is dependent on itself? 23:34:53 > fst (3 ** [1,2,3]) 23:34:53 Can't unify 23:34:53 Exists a P 23:34:53 with 23:34:53 (iType, t) 23:34:53 Specifically:↵… 23:34:54 Couldn't match expected type `(a0, b0)' with actual type `[t0]' 23:35:07 > head (3 ** [1,2,3]) 23:35:08 Can't unify 23:35:08 Exists a P 23:35:08 with 23:35:08 Vect (S n) iType 23:35:08 Specifically:↵… 23:35:08 No instance for (GHC.Show.Show a0) 23:35:09 arising from a use of `M707592794521593570827224.show_M7075927945215935708... 23:35:09 The type variable `a0' is ambiguous 23:35:09 Possible fix: add a type signature that fixes these type variable(s) 23:35:09 Note: there are several potential instances: 23:35:20 ( (\v -> let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3] 23:35:21 (input):1:58:No such variable \ 23:35:21 Oh, lambdabot + idris-ircslave 23:35:33 oops how do lambdas work 23:35:54 ( sin 23:35:54 sin : Float -> Float 23:36:03 oerjan: => rather than -> 23:36:06 -!- Sgeo_ has joined. 23:36:11 ( (\v => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3] 23:36:14 (input):1:58:Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.:: 23:36:26 oops 23:36:40 Why ( and not )? 23:36:41 ( (\(v : Vect _ _) => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3] 23:36:42 (input):1:3: error: expected: lambda expression 23:36:42 (\(v : Vect _ _) => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3]<> 23:36:42 ^ 23:36:44 ) 3 23:36:45 FreeFull: 3 23:36:48 A 23:36:59 } 3 23:37:01 ok i'm clearly not understanding this 23:37:05 } is free 23:37:24 ^prefixes 23:37:24 Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-ircslave ( , jconn ) , blsqbot ! 23:37:35 FreeFull: because that is finally now matchin hth 23:37:40 *+g 23:38:00 ( is a weird prefix though 23:38:00 No such variable is 23:38:08 ( exists 23:38:10 (input):1:1:No such variable exists 23:38:27 * Sgeo_ glares angrily at Quassel 23:38:38 ( Exists 23:38:39 Exists : (a : Type) -> (a -> Type) -> Type 23:38:50 ( Ex_intro 23:38:50 (input):0:0:Incomplete term Ex_intro 23:38:57 ( :t Ex_intro 23:38:57 Ex_intro : (x : a) -> (P x) -> Exists a P 23:39:52 -!- erdic_ has joined. 23:40:12 ( let data Foo = Bar | Baz in Foo 23:40:13 (input):1:5: error: expected: expression 23:40:13 let data Foo = Bar | Baz in Foo 23:40:13 ^ 23:40:19 aww 23:40:28 Isn't there a language that allows local data definitions? 23:40:48 Remove the let 23:41:05 ( data Foo = Bar | Baz 23:41:05 (input):1:1: error: expected: ":", 23:41:05 end of input, operator 23:41:05 data Foo = Bar | Baz 23:41:05 ^ 23:41:16 Hmm, maybe not 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 ( the (a ** b) (5 ** "Hi") 23:50:47 -!- atehwa_ has joined. 23:50:50 ? 23:51:01 -!- erdic has joined. 23:51:30 -!- tromp_ has joined. 23:51:40 ( 1 + 1 23:53:23 Melvar: Sgeo_ killed yer bot hth 23:54:01 ( "hi" 23:54:24 -!- fizzie` has joined. 23:54:42 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:56:25 or not. 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.