00:15:20 -!- FireFly has quit ("Leaving"). 00:21:28 -!- bsmntbombgirl has quit (Read error: 101 (Network is unreachable)). 00:28:37 -!- Pthing has joined. 00:28:38 -!- ehirdiphone has joined. 00:33:05 -!- oerjan has quit ("Spyong"). 00:35:29 So good to hear about Mike. 00:35:56 -!- MigoMipo has joined. 00:36:31 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 00:37:02 ? 00:56:23 -!- ehirdiphone has joined. 00:56:46 soupdragon: See todays logs. 00:56:51 -!- ehirdiphone has quit (Client Quit). 01:00:08 hm 01:07:25 definitely 01:08:23 definitely good or definitely hm? 01:14:30 definitely good 01:37:24 -!- |MigoMipo| has joined. 01:37:58 -!- |MigoMipo| has quit (Remote closed the connection). 01:46:06 -!- MigoMipo has quit (Read error: 110 (Connection timed out)). 01:55:05 -!- coppro has quit (Remote closed the connection). 01:59:17 -!- BeholdMyGlory has quit (Remote closed the connection). 02:23:13 -!- coppro has joined. 02:29:19 -!- anmaster_l has quit (Read error: 60 (Operation timed out)). 02:48:20 -!- Slereah_ has quit (Read error: 60 (Operation timed out)). 02:51:14 -!- Slereah has joined. 03:22:11 -!- Slereah has quit (Read error: 110 (Connection timed out)). 03:27:47 -!- Slereah has joined. 03:29:37 -!- ehirdiphone has joined. 03:30:12 Who wants to hear about my borderline-eso lang? :P 03:30:31 (proof of esoness: it's more CS than haskell) 03:30:37 I do 03:30:57 but I already told you the basics yesterday :P 03:31:10 Elaboration is so passé 03:31:45 (more to the point I wouldn't know where to start elaborating) 03:32:37 soupdragon: If you as a specific question I can prolly answer 03:33:18 is your friend bipolar 03:33:32 what friend 03:33:47 You mean mike Riley? 03:34:58 it is just such a contrast that I am a bit confused by it 03:35:56 What are you referring to? his present crisislessness? 03:36:15 yeh 03:36:45 he has chronic depression and saw a therapist so presumably it's not doing its chronic thing right now 03:37:35 ais523: Sleep pattern messed up again? 03:37:46 sort-of 03:37:55 also, I sometimes have late Internet nights deliberately, so I can talk to americans 03:38:00 (also, nethack.de?) 03:38:11 this time it's because it's rather snowy and I didn't want to walk home in it 03:38:15 ais523: heh. Mine's messed up too 03:38:22 ehirdiphone: you'd have no idea how hard it is to internationalise NetHack 03:38:32 but mostly, it's because Germany's closer than the US 03:38:33 ask me about my language! 03:38:38 and lag is pretty important when playing NetHack 03:38:42 anyway, what language? 03:39:05 Unnamed. Borderline eso. More CS than haskell 03:39:32 wait, what? is that even possible? 03:39:39 Yep 03:39:51 how might it do I/O? 03:40:01 Even agda is more cs 03:40:10 But not so good for regular programming 03:40:17 rofl Talking to Americans 03:40:28 coppro: why is that amusing? 03:40:37 ais523: Basic text io... Prolly monads. 03:40:51 http://en.wikipedia.org/wiki/Talking_to_Americans 03:40:56 ais523: IO? *IO*? How dare you suggest such a thing. 03:41:04 GUI and web and stuff? FRP which I won't bother explaining ATM 03:41:11 pikhq: you can only imagine how hard it is in Feather 03:41:12 main is a function from String to String! 03:41:21 ais523: Ask for an overview of the cool stuff! :P 03:41:27 ehirdiphone: you know, you could just tell me 03:42:05 ais523: Tru day 03:42:07 Fat 03:42:09 Dat 03:42:21 ***dat? 03:42:26 Yes 03:42:29 -!- Slereah_ has joined. 03:43:06 ais523: Dependent types. ML style module system. Type level metaprogramming. Arbritary syntactic extension. 03:43:12 ASK ABOUT ANY :P 03:43:24 let's start with syntactic extension first 03:43:56 then what's the difference between Type level metaprogramming and Dependent types? 03:44:17 Pretty simple. Modules can add to the syntax of the language, using arbritary code to make the replacement for the syntax 03:44:51 soupdragon: The former means inspecting types themselves 03:45:03 Say, the names of the fields of a record 03:45:07 And their types 03:45:08 Etc 03:45:19 NEXT QUESTIONS :p 03:46:04 ais523: Do you know what dependent types are btw? 03:46:17 I think so, but tell me anyway, because terminology is something I easily mess up 03:46:22 Ok 03:46:49 In typed lambda calculus, types index on types and values index on values 03:46:52 That is 03:47:03 A type can depend on another type 03:47:08 Like 03:47:13 (a,b) 03:47:23 Indexes on a and n 03:47:24 B 03:47:27 Types 03:47:38 And values index on values 03:47:41 F x 03:47:42 I didn't get that ehird 03:47:47 F indexes on x 03:47:55 ais523: Get that so far? 03:48:04 inspecting types 03:48:06 You give types to types 03:48:10 basically, creating types out of other types 03:48:14 And values to values 03:48:25 ais523: Thats nit dependent Tuesday 03:48:28 Types 03:48:34 This I'd just bacgriund 03:48:37 ok 03:48:54 ais523: now in haskell 03:49:11 Typeclasses create values that index on types 03:49:30 The value of the function show depends on what type it is 03:49:37 Int -> String 03:49:50 String -> String 03:50:02 the value of "show" changes 03:50:09 Get it? 03:50:19 yep 03:50:29 Now for the kicker 03:50:31 like overloaded functions, but much more first-class and genreal 03:50:33 *general 03:50:49 ais523: Dependent types = types indexing on values 03:50:53 FOR INSTANCE 03:51:00 no 03:51:01 oh, aha, I did know that, just forgotten I had 03:51:15 indexing is just one sort 03:51:25 soupdragon: Im just explaining it 03:51:26 so you can have a function that only takes even numbers as arguments, anything else is a typing error? 03:51:31 Not formally defining it 03:51:35 ais523: Yep 03:51:41 okay but (=) means something dear to me 03:51:54 Or a vector access function that enforces bounds checking 03:52:01 At compile time 03:52:06 No runtime penalty 03:52:15 sounds like what Splint tries and fails to do 03:52:36 incidentally, I tried and failed to get my Underlambda interp fully Splint-compliant 03:52:41 Splint seems really buggy 03:52:49 some code I wrote had a bare block for scoping 03:52:53 inside a switch statement 03:52:59 if I put the break; inside the block, no error 03:53:03 if I put it after the block, error 03:53:16 even though the two sets of code were completely identical to any compiler 03:53:23 ais523: Anyway, so dependent types makes programs more type Sade 03:53:25 Safe 03:53:29 yes, definitely 03:53:31 And 03:53:40 Lets us do things we couldn't otherwise 03:53:46 More permissive things! 03:54:03 ehirdiphone: incidentally, this is how I think a really good BF optimiser would work 03:54:05 For instance 03:54:14 trying to calculate dependent types for tape elements at different points in a program 03:54:33 vararg :: (n :: Integer) -> Vararg n 03:54:36 And 03:55:12 type Vararg 0 = (); Vararg n = () -> Vararg (n-1) 03:55:24 vararg 0 :: () 03:55:34 vararg 1 :: () -> () 03:55:37 etc 03:55:47 Ignoring negatives :P 03:56:02 curried varargs! 03:56:06 Implementation if vararg itself: 03:56:16 vararg 0 = () 03:56:28 actually, I think that's possible in Underload too, but a completely different way 03:56:35 vararg n () = vararg (n-1) 03:57:03 ais523: And this doesn't inspect n at runtime to determine the type! 03:57:13 yep 03:57:17 it's /statically/ correct 03:57:21 we need more static correctness in the world 03:57:29 you know, like Splint but actually working 03:57:31 If n is say read from stdin you just must satisfy the compiler 03:57:41 So it knows your call is correct 03:57:44 ais523: PLUS 03:57:53 All if this leads to more fun 03:57:58 Type safe printf 03:58:19 -!- Slereah has quit (Read error: 110 (Connection timed out)). 03:58:20 printf :: (fmt :: String) -> Printf fmt 03:58:39 type Printf [] = IO () 03:58:43 ehirdiphone: you probably want something along the line of C++'s dynamic_cast 03:58:50 No 03:58:52 Static 03:58:54 Ssh 03:59:18 Did someone say C++? :P 03:59:18 incidentally, for Cyclexa I was planning what's effectively typesafe /scanf/ 03:59:29 it physically wouldn't let the user input something of the wrong type 03:59:33 type Printf ('%':'d':xs) = Integer -> Printf xs 03:59:36 haha cool 03:59:55 * coppro will point out that C++ has lots of static correctness... too much, really 04:00:05 type Printf (x:xs) = Printf xs 04:00:16 yeah my C++ programs are statically correct.. the problems come when you run them 04:00:19 ais523: ^^^ dependent types rule 04:00:53 soupdragon: haha 04:01:02 "Dependent types. ML style module system. Type level metaprogramming. Arbritary syntactic extension." 04:01:03 C++ doesn't normally enforce static correctness very fully 04:01:07 soupdragon: Lol 04:01:08 Ok 04:01:14 unless you go and implement integers in the type system, or whatever 04:01:14 First amd last gone 04:01:19 Pick one! 04:01:35 ais523: That comment interests me... what do you mean by that? 04:01:39 (apparently, someone won an IOI round like that once) 04:01:45 basically, C++ templates are Turing-complete 04:01:59 if you write a program in them, the whole thing gets run at compile-time 04:02:15 PICK ONE >:( :P 04:02:19 ehird, you didn't answer my question (in such a way that I can understand it) 04:02:20 do you mean that the type system doesn't allow distinguishing of values? 04:02:27 soupdragon: Reask 04:02:37 coppro: not in C++, but you can use types themselves effectively as values 04:02:39 you can do metaprogramming with dependent types 04:02:51 ais523: I'm very familiar with C++, I just wanted clarification :) 04:02:57 soupdragon: You have: 04:03:07 why don't the dependent types subsume metaprogramming? 04:03:10 * coppro remembers the WTFBBQ entry that created a separate type for every integer 04:03:12 or do they? 04:03:30 data Foo = Foo { a :: Integer, b :: Integer } 04:03:47 With dependent types alone, you could not do 04:03:52 f Foo 04:03:54 == 04:03:56 s/WTFBBQ/OMGWTF/ 04:04:03 http://thedailywtf.com/Articles/OMGWTF-Finalist-10-FerronCalc.aspx 04:04:10 [("a",Integer), 04:04:24 ("b",Integer)] 04:04:31 (f being type level) 04:04:41 wnat about 04:04:52 f (A -> B) = "A -> B" 04:04:55 ? 04:04:57 So basically inspecting and creating types programmaticslly in the type system 04:05:05 Is what I mean 04:05:20 soupdragon: Ask a mote specific question than what about 04:05:49 * coppro hopes to be at the 2010 IOI; possibly even as a competitor, though that seems unlikely due to stupid circumstances 04:07:11 -!- bsmntbombdood has joined. 04:07:16 it seems like you have some kind of quotation for types 04:07:32 (and that will have to include values too, because of the dependency) 04:07:41 soupdragon: That "f Foo" was not runtime code 04:07:49 It is type level 04:08:07 Where of course types are values, duh 04:08:32 Foo :: Type or :: Set if you fancy 04:08:36 well I still don't get it 04:08:47 but that's okay 04:08:54 I would write example code but not on the iph 04:08:56 Ooh 04:09:13 I'll pen write it and photo it >:D 04:09:58 haha now you're thinking with iPhones 04:10:35 Paper. Where is paper 04:10:54 I HAVE NO PAPER 04:11:25 heh, you're reminding me of how every year when it comes round to exam time I realise I've almost forgotten how to write 04:11:48 ais523, you do most things in your head? or on computer? 04:12:06 Fuck books with no notes section 04:12:12 * coppro managed to get a computer for his English exam! 04:12:23 I need a bible with a lot of blank pages 04:12:48 PAPER 04:12:57 soupdragon: both 04:13:09 ehirdiphone: I generally have plenty of paper 04:13:13 About to write dependentkly typed code in a ruby on rails book yo 04:13:29 I don't like putting my netbook down directly on a duvet or whatever as it blocks the air vents 04:13:37 but it turns out it fits nicely onto an A4 pad of paper 04:13:45 AAAAAAA PEN 04:13:49 Need pen 04:13:50 * coppro is currently using a cookie tray 04:14:14 Ok 04:14:51 coppro: I didn't realise cookie trays were even approximately TC 04:14:51 WTF pen is silver 04:14:58 ehirdiphone: ask your parents? 04:15:04 ais523: for laptop ventilation 04:15:09 coppro: ah 04:15:31 ais523: Its 4am 04:15:39 good point 04:15:41 I'm not waking them up :P 04:15:51 maybe you should just wait until morning 04:15:55 WAIT 04:16:01 We have drawers here 04:16:07 With things in them 04:16:13 SEARCH TIME 04:17:25 cookie trays??? 04:17:33 YEA 04:17:38 PEN 04:22:07 Photo time 04:22:10 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 04:24:13 -!- ehirdiphone has joined. 04:24:21 ais523: I emailed you the photo 04:24:28 heh 04:24:39 Can you imgur.com it and link the directvlink here? 04:24:40 incidentally, filebin.ca's getting reported as a malware site by Firefox 04:24:44 Thx 04:26:13 http://imgur.com/n5amE.jpg 04:26:32 soupdragon: 04:26:37 So here, 04:26:42 what did you write it /on/? I hope you haven't damaged a book for our sake 04:27:05 type Fields :: Type -> [(String,Type)] 04:27:07 well 04:27:17 Technically :: Record -> 04:27:26 But that's not too relevant 04:27:27 okay 04:27:37 ais523: Blank page before index 04:27:46 ugh 04:27:46 In ruby on rails book - worthless 04:27:56 ehirdiphone: you might have been able to sell on that book... 04:27:56 soupdragon: See what I mean now? 04:28:03 yes 04:28:12 D: 04:28:23 ais523: Oh well 04:28:30 It's for SCIENCE 04:28:33 hi Gracegoats 04:29:20 ais523: The book is way out of date anyway 04:29:27 oh hello soupdragon. wink. 04:29:36 -!- adam_d has quit (Read error: 110 (Connection timed out)). 04:29:45 ? 04:29:48 Gracenotes: Get a room! 04:29:58 wat 04:30:04 ehirdiphone: get a real computer :| 04:30:05 xwat360 04:30:07 lol 04:30:16 Gracenotes: Get your mo 04:30:19 iPhone isn't even turing complete!!!! 04:30:19 M 04:30:39 Real men use real turing machines! 04:30:41 that's true. then again this laptop isn't exactly turing-complete 04:30:50 lol 04:30:51 @ 04:30:56 turing machines 04:31:36 given that I can't even allocate enough space to linearly bound any given input size, I'm not quite sure it's context-sensitive 04:32:15 it's basically a big lookup table 04:32:19 ais523: grok the example? 04:32:27 yes 04:32:27 so called "computers" don't compute anything 04:32:32 it looks just like OCaml 04:32:37 Wat 04:32:52 It's haskell but with dependent types and type metaprogramming 04:32:59 Haskell syntax thru and through 04:33:05 what is? Epigram? 04:33:07 well, they're pretty similar syntactically 04:33:18 The syntax i used in my example 04:33:18 and I'm more used to OCaml, I think 04:33:30 ehirdiphone: So, "Let's start with what Haskell gets right, and go from there". 04:33:38 ok, so the final topic is... The module system! 04:33:47 use the C #include system 04:33:49 end of story 04:33:50 pikhq: Few differences. 04:33:51 amirite 04:34:06 pikhq: Actual syntax will differ quite a bit 04:34:35 no one cares about module systems :P 04:34:39 Gracenotes: MURDER. 04:34:40 because they are complicated 04:34:53 And, might be strict not lazy, both for the added safety and because iirc a general implementation of lazy FRP is unsolved problem 04:35:09 soupdragon: Mine is not just for nanespaces! 04:35:10 soupdragon: A modern language without a module system is a crime. 04:35:23 Indeed they are even more powerful than MLs 04:35:32 pikhq: Yeah like haskell 04:35:33 ah, how did you make them interesting? 04:35:57 ehirdiphone: ... ? 04:36:01 ais523: Will explain immediately after haskell modules bashing 04:36:12 pikhq: Haskell has nanespaces 04:36:12 We may be using words differently. Explain. 04:36:19 And no functors! 04:36:32 (not that kind) 04:36:41 Ah. 04:36:41 I consider that a somewhat simplistic module system. 04:36:53 Shall I segue into my explanation? :P 04:36:55 Of course, my background is C-heavy, so... Yeah. 04:36:59 Yes. 04:37:29 Will use ml haskell hybrid syntax for this explain 04:39:48 type List = module { type T; empty :: T; add :: Integer -> T -> T; length :: T -> Integer } 04:39:56 Erm 04:40:00 That type there 04:40:07 Oh sod it let me retire 04:40:10 Rewrite 04:40:11 Sec 04:40:42 signature { type T; empty :: T; add :: Integer -> T -> T; length :: T -> Integer } 04:41:05 This is a signature. Signatures -- modules as types -- values. 04:41:15 With me so far? 04:41:20 Right... 04:41:23 (ais523 pikhq) 04:41:43 yep 04:41:45 same as in ML 04:42:01 ais523: Just explaining mls stuff first for pikhq 04:42:17 Here's an implementation of that signature 04:43:20 module List { type T = [Integer]; add x xs = x:xs; length xs = theLanguagesLengthFunction xs } 04:43:37 We could say that that module :: that signature 04:43:42 With me? 04:43:50 Okay... 04:44:37 So, List.T is a type. BUT! If we, in our interface file (basically just the types of things), 04:45:04 Put module List :: signature { that signature } 04:45:12 Then it becomes it's interface 04:45:16 I.e 04:45:28 pikhq: List.T is a type site 04:45:31 Sure 04:45:32 But 04:45:48 It is not useable as [Integer] 04:45:56 It is abstractef 04:46:09 We can only use it from List's functions. 04:46:14 Cool, no? 04:46:25 Yeah. 04:46:34 [1] :: List.T simply doesn't work 04:46:50 Because the implementation of T is not exposed 04:46:53 pikhq: Now 04:47:12 It's conceivable that two modules might have the same signature 04:47:17 E.g. 04:47:30 An implementation using a vector 04:47:36 Yah? 04:47:42 Yeah. 04:48:15 So we have functors. A functor is basically a module that takes other modules as arguments 04:48:18 Observe 04:49:06 functor Silly (List :: signature { long signature is long }) = module { 04:49:26 foo = List.add 1 List.empty 04:49:49 main = print (List.length (List.add 2 foo)) 04:49:52 } 04:49:57 We could then do 04:50:13 open (Silly VectorList) 04:50:26 (open is basically import) 04:50:37 (extracts everything into the current module) 04:51:03 Huh. 04:51:06 pikhq: So we have implementation agnostic modules 04:51:10 Sweet, huh? 04:51:15 Yeah. 04:51:21 AND 04:52:01 Combined with my type level metaprogramming (did you understand the photo?) 04:53:45 oh.. what the hell. http://www.xs4all.nl/~weegen/eelis/analogliterals.xhtml 04:53:50 pikhq: ais523 (here is where it departs from ml) 04:53:58 I feel like breaking down into tears 04:54:03 Gracenotes: one of Eelis' finest creations 04:54:36 hahaha 04:55:04 I am feeling the joy of human creation simultaneously tinged with desperate sorrow 04:55:20 reminds me of Acme::Don't in Perl 04:55:25 which was a similarly silly syntax trick 04:55:36 ehirdiphone: That photo... 04:55:55 Spiffy. 04:55:58 http://imgur.com/n5amE.jpg 04:56:06 Seen it? 04:56:07 ais523: not sure it's on the same scale 04:56:21 you know, ehirdiphone, many of us do use pastebins 04:56:21 Grok it? 04:56:26 Gracenotes: Iphone 04:56:38 Gracenotes: maybe not, but apostrophes in keyword names are still epic 04:57:42 pikhq: 04:58:09 ehirdiphone: Yes. 04:58:13 Don't is a syntax trick? 04:58:17 Ok pen time 04:58:18 I just commented on it, in fact. 04:58:24 Ok :p 04:58:29 Sec 04:59:57 Too long to write I'll just explain 05:00:08 coppro: yes 05:00:22 it's equivalent to Don::t using an outdated syntax 05:00:31 ah 05:00:33 pikhq: Who says functor arguments have to be modules? why not types? 05:00:36 oh right, now I remember 05:00:38 FOR INSTANCE 05:01:10 functor Input (t :: RecordType) 05:01:15 results in a 05:01:33 signature { input :: IO t } 05:01:47 By using Fields as seen in my photo 05:01:57 It lets you do this: 05:01:58 I only have one complaint 05:02:09 Specifying the type independently from the value seems blah 05:02:16 if they are effectively identical 05:02:25 data Foo { a :: Integer, b :: String, c :: Bool } 05:02:39 open (Input Foo) 05:02:47 main = input 05:02:49 Result? 05:02:57 $ ./foo 05:03:06 a= 2 05:03:11 b= foo 05:03:15 c= abc 05:03:28 Invalid input. 05:03:35 c= true 05:03:45 And that results in 05:03:51 it's 4 am, you're hard to folllow 05:03:56 Foo {a=2,...etc 05:04:07 pikhq: ais523 get it? 05:04:09 That's... Pretty spiffy. 05:04:27 I think I get it, and it's neat 05:04:30 but I'm not sure 05:05:01 The uber cool thing is how all this has no runtime penalty 05:05:09 interesting fact I just discovered: Google appears not to offer any search suggestions for searches beginning with "sexy". "sex" is fine, as is "sexiness", but not "sexy". 05:05:15 coppro: Haskell fu helps 05:05:32 ehirdiphone: Actually, as much as you're going to hate me for saying this, C++ helps too 05:05:33 ehirdiphone: pretty much 05:05:39 coppro: Btw, what do you mean by 05:05:43 ehirdiphone: Good God most of that is easily done at compile-time, isn't it? 05:05:54 copproSpecifying the type independently from the value seems blah 05:05:58 pikhq: Yep. 05:06:22 ehirdiphone: One of your earlier examples, if I read correctly, had you specifying the type and the value of the function redundantly 05:06:37 if I misread, my problem, not yours 05:06:38 coppro: Redundantly? 05:06:42 Like how? 05:07:04 coppro: Do you mean the 05:07:07 signature 05:07:14 List 05:07:14 [20:54:48]type Vararg 0 = (); Vararg n = () -> Vararg (n-1) 05:07:16 Thing? 05:07:16 [20:55:00]vararg 0 :: () 05:07:18 [20:55:10]vararg 1 :: () -> () 05:07:19 [20:55:42]Implementation if vararg itself: 05:07:21 [20:55:52]vararg 0 = () 05:07:23 [20:56:10]vararg n () = vararg (n-1) 05:07:40 coppro: Ah. That is only because the example is trivial 05:07:53 ah, ok 05:07:58 In my soon after printf example you could easily see the difference 05:08:02 right 05:08:30 just wanted to make sure that a generic functor wouldn't have to specify its type independently from the value; one of the major issues with C++'s templates 05:08:39 hmm... I'm going to go buy some food 05:08:47 Or just let the compiler infer the type! (yeah right, even haskell can't infer the type in all cases) 05:09:12 (literally impossible for my Lang due to TC type system) 05:09:12 ehirdiphone: yeah, they've added it for lambda functions but not for regular ones 05:09:14 :( 05:09:18 ??? 05:09:26 Type inference is kinda impossible to do in the general case... 05:09:27 I think you are confused 05:09:32 ehirdiphone: no 05:09:33 And even more so for TC types. 05:09:45 pikhq: Haskell sans typeclasses is inferrable totally 05:09:56 coppro: You are confused 05:10:08 Haskell sans typeclasses is perhaps even *trivially* inferrable. 05:10:26 currently, a generic add functor in C++0x currently looks like this: template auto add (T t, U u) -> decltype(t+u) { return t+u; } 05:10:30 see the redundancy? 05:10:39 (at least it's better than the current mess *shudder*) 05:10:40 You didn't say c++ 05:10:47 I did 05:10:47 ehird, GADTs? 05:10:55 [22:08:06]just wanted to make sure that a generic functor wouldn't have to specify its type independently from the value; one of the major issues with C++'s templates 05:11:02 soupdragon: What about them? 05:11:03 not sure if Tom solved it or not 05:11:11 Oh 05:11:14 type inference for functions that work on GADTs 05:11:16 Haskell inferrence 05:11:40 ehirdiphone: lambda functions are allowed to infer types on bodies of "{ return foo;}", but IIRC this hasn't been added for normal functions 05:11:55 Wait 05:12:10 copprojust wanted to make sure that a generic functor wouldn't have to specify its type independently from the value; one of the major issues with C++'s templates 05:12:13 Didn't see that 05:12:16 Xarify 05:12:18 Clarify 05:12:42 ehirdiphone: I just gave an example; "t+u" is redundant 05:12:52 Ah 05:13:06 Don't get it but whatever 05:13:12 compare to a lambda (no polymorphic lambdas atm): "[](int t, int u) { return t+u; } // inferred return type int" 05:13:21 the -> foo is the return type 05:13:31 ehirdiphoneIn my soon after printf example you could easily see the difference 05:13:34 Erm 05:13:42 it appears after the parameter declaration so the parameters are visible 05:13:51 coppro: When you pinger me snout the I ferrencr only being for lambda 05:14:12 okay, I think I'm assuming too much about your knowledge of C++ 05:14:17 Read the lines I said before with out your c plus plus stuff 05:14:28 I didn't realise you'd said them 05:14:40 I was just continuing what I said with a quip 05:14:49 ok 05:14:55 Anyway 05:14:59 how about we restart altogether? 05:15:06 Doesn't matter 05:15:27 basically: Make sure that in trivial cases, it's possible to specify a function without specifying the type in a redundant manner 05:15:30 I'm aiming to have no gc w my Lang! If it's possible 05:15:38 Region inferrence instead :D 05:15:43 gc w? garbage collection with? 05:15:44 Would be uber cool 05:15:48 coppro: Yes 05:16:06 interesting 05:16:27 I've always been interested in the notion of graph-based collection 05:16:50 It'd, among other things, let small integers use a full word 05:16:51 specifically with the goal in mind that an object is destroyed as soon as its references become invalid 05:17:04 No need for a tag so the gc knows what's a pointer 05:17:21 And probably speed things up 05:17:30 anyway, I'm actually leaving to get food now; if you have anything important to say, ping me or comment when I get back 05:17:42 Probably wouldn't catch all things though 05:17:44 ehirdiphone: If you can do it, then it would be quite nice. 05:17:45 Dunno 05:18:15 pikhq: A cool thing arising from all this sweet language nectar: 05:18:50 You can malloc some memory, access it at will, realloc it, etc, with no runtime penalty, SAFELY. 05:19:29 malloc :: (n::Int) -> MemBlock n 05:19:55 (Ok, IO (Maybe (MemBlock n))) 05:20:15 Heheh. 05:20:58 pikhq: the kicker? 05:21:06 Even ptr arithmetic 05:22:01 ptradd :: (n::Int) -> MemBlock m -> MemBlock {n-m} 05:22:07 Or similar 05:22:12 Ignoring negatives 05:22:49 *m-n 05:23:22 :D 05:23:41 access :: (n::Int) -> MemBlock m -> {n < m} -> Int 05:24:02 called as (access n block) if no proof is required 05:24:18 woo dependent types 05:24:28 *-> IO Int 05:24:37 So, you could use this language much like C. ... Except you're not going to shoot a foot with it. 05:25:36 pikhq: I'm targetting performance because Ur has quite a bit of this stuff and generates objects with little overhead, lots of speed and little memory usage in it's domain 05:25:49 (which is web apps, oddly enough) 05:26:08 Dependent types = can make more compile time assumptions 05:26:27 And if you did some wizardy GHC style optimisation too? 05:26:30 Dude. Fast. 05:26:42 :( 05:27:18 ehirdiphone: Because of the annotations given to the compiler, optimization would be (relatively) easy. 05:27:42 Hey, if I had no gc and small ints took up the word arithmetic would be 1 instructiob 05:27:44 N 05:27:46 Much less "checking to be sure this is safe", more with the "just transform it to the equivalent". 05:27:57 Not like 10 and a branch 05:28:01 As with tagged ints 05:28:04 Well 05:28:07 No branch 05:28:12 Since stariv 05:28:15 Sratic 05:28:17 Static 05:28:19 But still 05:28:28 1 vs 6 or so 05:28:37 Nice speed up for number chrubchibg 05:28:45 Crunching 05:29:14 soupdragon: why thr dmilry? 05:29:16 The 05:29:19 Smiley 05:29:20 Sj 05:29:22 because = 05:29:30 Shiws as sad in colloquy 05:29:56 soupdragon: Iphone bitch. Be glad im not using text speak 05:30:41 A compiler that does all the things I want will prolly be like 20,000 lines of haskell or more :-( 05:31:05 Maybe even 50,000—70,000 depending on compiler smartness 05:31:35 100,000 if I want readable error messages :P 05:33:29 damn this language is sweet :| 05:34:32 I don't even want to write the compiler in another language. Too many opportunities for sweet uses of the lang's features 05:34:58 If you absolutely must write it in a different language, must be Haskell. 05:35:15 Or one of the MLs 05:35:16 It just makes language implementation... Feel right. 05:35:26 They were designed for it after all :P 05:35:34 Fair point. 05:36:45 (advantages of ML: Usually faster, module system (think e.g. compiler is a functor taking backend module), if I choose to make the language strict it matches the semantics better, that just feels... more right) 05:36:56 Haskell is compelling too though 05:37:59 It occurs to me that a worthy Emacs mode would be a mode to end all modes 05:38:25 Probably the largest piece of elisp ever. :P *shudder* 05:39:14 Agda has a really advanced emacs mode 05:39:27 will it allow impureness? 05:41:05 ais523: Monads. 05:41:29 I mean, as well 05:41:31 if it's being strict 05:44:44 ais523: No. 05:45:17 Well, maybe if you have "pragma unsafe" in your module and import Internals. 05:45:34 Then you have Internals.coerce :: a -> b 05:45:36 back 05:45:51 But every module using yours must be pragma unsafe too 05:45:59 So that's pointless, mostly 05:46:15 coppro: I said interesting things right after you left 05:46:39 do I have to repeat them or do you have sufficient scrollback? 05:46:54 I have scrollback 05:47:18 coerce would actually be: 05:47:38 ehirdiphone: Yeah, if you have well-defined evaluation order, "pragma unsafe" is perfectly reasonable. 05:47:53 (a::Type) -> (b::Type) -> a -> b 05:48:11 But you use that as (coerce x) 05:48:32 That's just how you do forall in dependently typed langs 05:48:48 I'll probably have shorthand for that 05:49:22 Uh oh, iPhone problem, brb 05:50:00 Fixed 05:50:01 Ping 05:50:18 Pong 05:50:24 Paddle 05:50:29 Yay 05:51:11 So! I hope you all now worship my language and know it will subsume and supersume every other language forever. 05:51:15 ehirdiphone: very interesting 05:51:30 ehirdiphone: not until it has a really good impl 05:51:33 Or, more seriously, I hope you all now think my language is pretty cool. 05:52:02 ais523: That would be my goal. :P 05:52:04 ehirdiphone: does it compile easily into all TC esolangs? 05:52:17 or does it not want to tread on Underlambda's design space? 05:52:18 coppro: Which part is very interesting? 05:52:25 All of it? :P 05:52:28 ehirdiphone: region inference 05:52:30 REMOVE ALL OTHER LANGUAGES. THEY ARE INSUFFICIENTLY COOL. 05:52:49 ais523: No, but you can have a compile time BF compiler. 05:52:53 With syntax. 05:53:04 one thing I want to clear up before I talk about the language as a whole; by "dependent types" you mean a function whose type can change based on the value of its arguments, correct? 05:53:13 BF[ ,[.,] ] :: IO () 05:53:38 coppro: Not just functions. It is simply: types can take values as arguments 05:54:04 Full explanation is way back in the scrollback 05:54:14 ok 05:54:19 * coppro loads logs 05:54:38 Careful. It's been an hours-long explanation. 05:55:24 Btw I haven't thought of a syntax at all yet. 05:55:35 Just been blending haskell and ml for this talk 05:55:46 ehirdiphone: so, basically, template vs. template? 05:56:22 (except applicable to all types, not just a very small subset of those available) 05:56:34 coppro: No! 05:56:40 oh :( 05:56:45 Because there, 05:56:54 The value must be known at compile time 05:57:02 Not so with dependent types 05:57:15 And yet, no runtime penalty 05:57:16 ah, ok 05:57:24 wait, how? 05:57:31 Basically 05:57:37 If you say 05:57:43 Read an int from stdin 05:58:06 And pass it to a function expecting an even number 05:58:07 you can erase all types into a NULL value, and then eval the real values like an untyped language 05:58:14 You must satisfy the compiler 05:58:18 That it is even 05:58:30 Perhaps it can infer it if you do a branch 05:58:37 Failing that, DIY 05:58:47 (because you can't do case analysis on types) 05:58:51 (pass the proof argument yourself) 05:59:01 so... attempting another gross oversimplification here... encoding the range of values into the type? 05:59:08 No. 05:59:21 more like set of values, only it's allowed to be infinite 05:59:35 coppro: They are real values 05:59:35 and you can have loads of types which are similar except in the value sets, automatically generated 05:59:39 Flesh and blood 05:59:58 You just have to manually satisfy them if the compiler can't 06:00:15 The type of an object might be "even integer", whereas another object might be of the type "prime integer"; true or false 06:00:17 If we need an even number, pass a proof that it's even 06:00:28 Then the value doesn't matter to the type 06:00:37 Voilà, dependency goes poof 06:00:52 ok, now I'm really confused 06:01:11 coppro: it's magic. 06:01:32 Don't worry, it's pretty intuitive in practice 06:01:41 There's a certain ACC quote which has never appeared more applicable to the situation 06:01:50 Feels like you're doing the impossible though 06:02:03 coppro: Precisely 06:02:15 Like, I understand the notion 06:03:34 Basically, your job as the programmer is: when the compiler can't make inferrences about your values so that it does not matter what they actually ARE at runtime because the type is satisfied no matter what, 06:03:44 You have to prove it. 06:03:47 ok 06:04:02 (which is just... Writing the code that shows it, basically) 06:04:20 But really, it's pretty simple. 06:04:33 Just doesn't sound it. 06:04:41 like, I get the net effect 06:05:20 Even I don't know the actual inferrence algorithms. I'm going to defer breaking my head that much until I absolutely must 06:05:21 it's statically-enforced value control 06:05:52 coppro: But also value liberator, remember the printf? 06:06:18 "value liberator"? 06:07:00 Lets you express stuff you can't otherwise 06:07:04 Like printf 06:07:07 oh, right 06:07:30 Now, I admit I don't program in functional languages as much as I'd like, so bear with me here 06:08:03 this looks to me a lot like pattern-matching being done at compile time, with an error if nothing matches 06:08:35 Can you elaborate? My mind is rejecting that metaphor. 06:08:57 My pattern matching experience is with Erlang, it may be different elsewhere 06:09:39 Nope 06:11:23 in Erlang, you could do something like printf ([%%, %d, RestOfString], [SomeInteger, RestOfArgs]) -> printAsInteger(SomeInteger), printf(RestOfString, RestOfArgs). 06:11:34 Oh 06:11:50 The type was pattern matching on the string 06:11:57 But all functions have that 06:12:23 It was just a type with the kind (type's type) String -> Type 06:12:28 right 06:12:35 but now, let's take a scanf example 06:12:56 in that case, you are pattern matching on the string and affecting the return type of the function 06:13:22 Printf does that too 06:13:28 The string affects the type 06:14:07 but scanf is a more interesting example 06:14:08 But continue 06:14:21 but so basically your idea is to be able to check this at compile time 06:14:40 and complain if there's any chance there might be an error 06:14:54 rather than simply waiting around and hoping things come out right 06:15:24 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 06:15:36 -!- ehirdiphone has joined. 06:15:36 His plan is to have the type of printf be dependent upon the string given as its first argument. 06:15:39 Colloquy borked 06:15:41 His plan is to have the type of printf be dependent upon the string given as its first argument. 06:15:47 (repeated for sake of ehird) 06:15:51 I do not understand your analogy 06:15:56 -!- Sgeo_ has joined. 06:15:59 pikhq: Saw it first time 06:16:03 -!- Sgeo_ has quit (Read error: 104 (Connection reset by peer)). 06:16:09 ehirdiphone: ... After you left? 06:16:17 You've got some crazy log-reading skills. 06:16:18 :P 06:16:40 it appeared to me to occur right after he arrived 06:16:47 he may have caught it 06:16:49 Darned latency. 06:16:57 yay IRC 06:17:29 copprorather than simply waiting around and hoping things come out right 06:17:35 Then what pikhq said 06:17:38 ehirdiphone: well... basically, suppose I do printf(some_user_string, 3) 06:17:39 That he repeated 06:17:45 Miss anything? 06:17:53 coppro: Wait 06:18:00 waiting 06:18:17 That would simply give a type inferrence error 06:18:32 I think this would work: 06:18:56 if s == "%d" then printf s 3 else return () 06:19:00 right 06:19:05 Failing that... 06:19:10 It's proof time 06:19:27 M 06:19:43 Not sure where the proof would go for printf actually 06:19:44 I think we're wasting our time 06:19:51 coppro: Hm? 06:19:52 yeah, printf would be a nasty proof 06:20:02 No need to prove printf. 06:20:24 Just prove that (printf s) :: Integer -> IO () 06:20:27 well, now I know we agree about the basics 06:20:27 ie 06:20:39 That s is only constant output 06:20:48 and one formatting directive 06:21:01 That takes an Integer 06:21:06 agreed 06:21:12 But honestly? 06:21:28 Don't pass a user string to printf, you dumb fuck. ;) 06:21:45 Sadly, that's when printf becomes most useful 06:21:56 localization, specifically 06:22:09 That's not a user strung 06:22:13 String 06:22:22 It may be loaded from a file 06:22:25 Compile those in, yo. 06:22:35 Parse the files at compile-time. 06:22:37 for 30 different languages? no thanks 06:22:52 Compile only the ones you need. 06:22:53 anyway, we're getting sidetracked 06:22:59 Anyway 06:23:06 Alternatively 06:23:30 Make a module signature Translation 06:23:33 With eg 06:23:49 big_error :: Integer -> String 06:23:54 Implementation? 06:24:09 we're getting sidetracked 06:24:17 my basic question is how this relates to the notion of types 06:24:18 big_error = printf "OLE OLE SUPER ERROR %d" 06:24:36 using one of your examples, suppose I have a function that takes an integer that must be even 06:24:39 You could use syntactic extension to make that nicer for the translators 06:24:44 Ok back on track 06:24:52 coppro: No 06:24:58 Wrong terminology 06:25:03 ok 06:25:09 correct terminology? 06:25:15 You don't take Integer-that-is-even 06:25:22 -!- cal153 has quit. 06:25:31 You take Integer and that-Integer-is-even 06:25:43 With the latter hopefully being inferred by the compiler 06:25:50 ok 06:26:05 this makes it feel even more Erlangish to me 06:26:08 but w/e 06:26:08 It's like having a type 06:26:17 Even (int) 06:26:27 Even 2 has one value 06:26:30 call it poop 06:26:40 poop :: Even 2 06:26:43 but 06:26:52 Erlang: my_function (I) where is_int(I) and I mod 2 == 0 -> whatever 06:26:53 Even 1 has NO values! 06:27:03 (nothing) :: Even 1 06:27:14 So the compiler passes "poop" in 06:27:20 If the number is even 06:27:24 It won't type 06:27:28 Erm 06:27:30 Will 06:27:33 Get it? 06:28:16 yes 06:28:30 coppro: So 06:28:40 If we don't know the value of n 06:28:41 The co 06:28:44 Mpiler 06:28:47 but so, for the purposes of the definition, which type is dependent on which value? The type of my_function is dependent on the value of n 06:28:48 ? 06:28:53 Cannot tell if (poop :: Even n) 06:28:57 Is well typed 06:29:07 And that's where proofs come in 06:29:29 ok... so what is a "proof"? 06:29:35 coppro: The type of the poop argument is dependent on the value of the number argument 06:29:47 ehirdiphone: but the poop argument doesn't really exist 06:29:55 Yes it does. 06:30:00 wait, what? 06:30:01 Let me show you. 06:30:05 ok 06:30:16 btw, can you just type in a pastebin rather than a picture? 06:30:24 iPhone actually 06:30:27 Just one line 06:31:12 evenClub :: (n::Integer) -> {Even n} -> AwesomeParty 06:31:21 {} is agdas notAtion for 06:31:30 also, btw, ZREO finished OoT finally; it's awesome 06:31:31 "infer vAlue if possible" 06:31:33 SO 06:31:37 Don't talk btw 06:31:44 o hai 06:31:57 not talking about anything relevant 06:31:59 When we do (evenClub 2) 06:32:05 The compiler does 06:32:15 evenClub 2 {poop} 06:32:24 ah, ok 06:32:28 I get it now! 06:32:31 Since the third param must be of type Even 2 06:32:39 -!- Sgeo has quit (Read error: 110 (Connection timed out)). 06:32:41 It checks that it is... Voilà! 06:32:51 voila! 06:32:56 Obviously, the poop param is erased during compilation 06:33:04 As it is useless at runtime 06:33:13 that's an interesting way for it to be thought of, and I wonder if it's the correct one, but at least I understand now :) 06:33:28 Not thought of 06:33:35 This is how it actually works 06:33:37 I know 06:33:39 (in agda) 06:34:17 The issue is that you need to make a type Even which is a drag BUT 06:34:43 -!- jpc has quit (Read error: 110 (Connection timed out)). 06:34:49 type IsTrue True = PoopHaven; IsTrue False = NoValuesForYou 06:34:58 + syntactic sugar 06:35:03 = tada? 06:35:18 That'd be 06:35:32 {IsTrue (even n)} 06:35:38 Or something 06:36:20 coppro: So, hopefully you at least grok it as well as I do now. 06:36:41 ehirdiphone: I now understand. 06:36:54 The whole language pretty much clicked into place combining seeing Ur with my past musings 06:37:04 So I haven't fully sorted it out yet 06:37:08 I question whether it would be more effective to attempt to accomplish the goal through a different mechanism 06:37:35 Explaining it is the single most difficult part 06:37:52 specifically, of encoding a known subset of values into the type of an object 06:38:11 -!- calamari has left (?). 06:38:17 Using it? Pretty easy. And a dependently typed lambda calculus is just a few lines of code onto a normal typed one 06:38:25 coppro: Explain 06:38:53 If you mean what I think Iean that cannot accomplish remotely as much sscdependent types 06:39:03 I think they're equivalent 06:39:24 (note, this is in the "this is a theory" form of "I think", not the "I'm pretty sure I'm right" form) 06:39:34 ais523: maybe dependent types are the key to feather :P 06:39:44 coppro: Can you still explain? 06:39:47 ehirdiphone: I'll try 06:40:55 basically, in your evenClub example, what you've actually done is included a "virtual" type (in the sense that the caller doesn't noticed it) to the signature 06:41:04 coppro: #agda is full of people who will know more than I btw if I don't grok it 06:41:06 Also 06:41:11 Irrelevant 06:41:13 Say you 06:41:17 ehirdiphone: just wait 06:41:18 Remove the {}s 06:41:21 Then 06:41:30 You'd just have to append " poop" 06:41:34 To your calls 06:41:41 It's just sugar 06:41:45 right, I get that 06:41:52 but what if it wasn't 06:42:00 I'm not trying to debate the way Agda does 06:42:07 I'm trying to find another approach to the same solution 06:42:09 Then that would break if you remove the {}s 06:42:14 agreed 06:42:17 They are not mandatory 06:42:26 So it is not equivalent 06:42:40 Remember dependent types are more than just yes no 06:42:42 my idea is that { Even n } is not seen as an extra parameter, but rather a constraint 06:42:45 Remember printf? 06:42:52 ok, restate printf for me 06:43:02 Logs. iPhone. 06:43:08 right 06:43:10 ok 06:43:16 Grep "type Printf" back up a line or two. 06:43:27 ugh, different syntax 06:44:00 ok, I think I get your point 06:44:10 ehirdiphone: how much do you know about C++ templates? 06:45:06 Not different syntax 06:45:10 Syntax is the sane 06:45:13 Same 06:45:24 coppro: A fair amount. 06:45:32 Almost did SKI once vm 06:45:38 *once. M 06:45:44 *once. 06:45:53 SKI? 06:46:00 ehirdiphone: do you know what enable_if is? 06:46:31 No. 06:46:35 Ski conbinatirs 06:46:40 Conbinatirs 06:46:48 Com bi nat IRS 06:46:50 IRS 06:46:53 Oes 06:46:53 ok 06:46:56 ors 06:46:57 Ors 06:46:57 I get it 06:47:02 Google it :p 06:48:10 ok, well, enable_if is a template taking a boolean and a type; if the boolean condition is satisfied, a member type exists; if the condition is not satisfied, the type does not exist 06:48:32 this is in many ways similar to the use of a predicate in { Even n } 06:49:09 Only works for compile time constants 06:49:18 true, but the principle is the same 06:49:21 You can't just handwave that away 06:49:35 I can if I consider only templates and not the C++ runtime 06:49:37 The whole model I said is to make that work 06:49:42 they are TC 06:49:45 coppro: No 06:49:48 Because 06:49:56 That's like a run time type system 06:50:04 It can simply pass the actual value 06:50:09 Which we can't. 06:50:20 well, allow me to continue 06:50:57 * coppro tries to remember where he's going wit hthis 06:51:02 ah right. 06:51:23 in the case of enable_if, you can implement arbitrary conditionals assuming appropriate predicates exist 06:51:38 And? 06:51:38 but there is another way of accomplishing the same task, and that is with restrictions on the arguments 06:52:01 there was a proposed feature for C++0x called concepts that would do exactly this; it would provide the ability to constrain template arguments 06:52:32 on one level, it's largely sugar, but the underlying notion is different 06:52:48 Which must be compile time constant 06:52:57 sure, but templates exist as a compile-time system 06:53:08 What you're doing is taking a hard problem 06:53:21 Explaining the solution to an easy problem 06:53:26 I'm wondering if dependent types can be implemented in the same way, with compiler-managed contraints rather than predicates 06:53:36 And handwaving the rest away 06:53:37 the whole C++ thing was an analogy; it's not perfect 06:53:39 etc. 06:54:16 coppro: Bit 06:54:18 But 06:54:25 That is more complicated 06:54:28 printf 06:54:30 of course it is 06:54:31 And the like 06:54:40 Require them to be usable as values 06:54:55 So you're just introducing a new concept 06:55:11 tbh, I think I need to see a bigger example of your language before I can explain this more clearly 06:55:11 Without even any holes for propfs 06:55:15 Proofs 06:55:27 So... Why? 06:55:28 since it's hard to explain without a concrete base to work from 06:55:36 What is the advantage? 06:55:44 I don't know if there's an advantage 06:55:50 advantage?? 06:56:05 if I sought an advantage in everything I did, I wouldn't be here chatting, I'd be finished my backload of homework 06:56:29 So... Replacing an existing concept with a less simple one. And you have to keep the old one anyway. 06:56:34 Compelling :P 06:56:39 I don't think you'd need to keep the old one 06:56:45 printf 06:56:55 Not a "constraint" 06:57:08 that's part of my issue; I'd need to see a complete example of printf 06:57:15 not just "here's my signature kthxbye" 06:57:19 printf "%d" 3 06:57:27 I gave more 06:57:27 printf "%d %d" 3 4 06:57:38 I gave the relevant type 06:57:47 The magic that makes it work 06:57:53 not enough, at least not me looking through scrollback 06:57:58 (well. Just for %d) 06:58:01 append is a cool one 06:58:11 It's right after the printf signature you dolt 06:58:19 :P 06:58:47 0 + m = m ; S n + m = S (n + m). 06:58:49 [] ++ ys = ys ; (x::xs) ++ ys = x::(xs ++ ys). 06:58:51 ah, I see, I think I just misunderstood the synta 06:58:53 *synatx 06:58:55 *syntax 06:59:14 _+_ : N -> N -> N, _++_ : Vector A n -> Vector A m -> Vector A (n + m) 06:59:27 it's amazing that ++ typechecks 06:59:56 soupdragon: BUT CAN IT BLEND^WINFER 06:59:59 :P 07:00:24 coppro: Note that (x:xs) is cons 07:00:34 And [] == "" 07:00:55 okay, hang on, I'm going to repaste this 07:01:19 19:58:20 printf :: (fmt :: String) -> Printf fmt 07:01:21 19:58:39 type Printf [] = IO () 07:01:24 19:59:33 type Printf ('%':'d':xs) = Integer -> Printf xs 07:01:25 20:00:05 type Printf (x:xs) = Printf xs 07:01:27 Is that it? 07:01:32 Ya 07:01:36 ok 07:01:46 so where does the type replacement come in to play here? 07:01:59 Type replacement? 07:02:09 err, the whatever 07:02:11 the funny magic 07:02:16 What? 07:02:23 wait... 07:02:30 * coppro facepalms 07:02:39 ok, so I'm stupid 07:02:49 but nvm that 07:02:53 What did you do? :P 07:03:10 I misunderstood the way functions work 07:03:19 Howso? 07:03:35 specifically, "a b" is a left-associative operator that executes a on b 07:03:45 oh right 07:03:55 for multi-arg functions, there's syntactic sugar in the declaration that creates a forwarding function with less arguments 07:03:56 you mean like f x y as f(x,y) 07:04:00 no 07:04:03 coppro: Ahh yep 07:04:04 yes you do 07:04:10 f x y as f'(x)(y) 07:04:10 :D:D:D:D:D:D:D 07:04:14 f' ? 07:04:30 coppro: Ya welcome to currying 07:04:48 as I said, my functional programming experience is sadly lacking :( 07:04:59 No worries 07:05:06 anyway, this helps clear up a lot, though all it ends up doing is making my idea a lot harder to express 07:05:14 How did it change your understanding? 07:05:24 Don't see currying in printf 07:05:33 absolutely there's currying there 07:05:38 I don't see what currying has to do with any of it 07:05:39 Where 07:05:46 just think of 07:05:52 f x y as f(x,y) 07:05:56 All the doohickeys have 1 arg 07:06:06 Oh 07:06:08 OH 07:06:11 YEAH 07:06:24 In type Primtf's right Gand side 07:06:27 Hand 07:06:32 yeah, it returns a function 07:06:41 Nope 07:06:45 wait, no? 07:06:45 Returns a type 07:06:56 coppro: For 07:06:57 well, a function type 07:07:05 A format string fmt 07:07:07 printf "%d" gives me an Integer -> IO, correct? 07:07:13 no 07:07:14 IO () 07:07:21 soupdragon: Yes. 07:07:25 Printf "%d" = Integer -> IO 07:07:32 right 07:07:34 IO () 07:07:36 soupdragon: A 07:07:38 As in 07:07:47 oh wait, that was soupdragon 07:07:47 A value if that type 07:07:57 ok, nvm. Your nicks have a too-similar length 07:07:59 coppro made no error 07:08:11 printf "%d" : Integer -> IO 07:08:14 -!- ehirdiphone has changed nick to pooop. 07:08:19 lol 07:08:23 You're welcome 07:09:02 pooop: Okay, I'm going to try again and try to explain what I was trying to explain before, now with more knowledge of where it isn't relevant 07:09:15 coppro: By nickname laws I think you have to have sex with me now. If I was poop I'd need copro 07:09:21 But pooop is coppro 07:09:26 QED 07:09:26 oh dear 07:09:32 -!- coppro has changed nick to Cu. 07:09:54 Cu: EVADING THE LAW?? 07:10:08 -!- pooop has quit (Remote closed the connection). 07:10:23 -!- ehirdiphone has joined. 07:10:25 lol 07:10:46 Repeat the line you said before the poop shit (which was crap) 07:10:53 Okay, I'm going to try again and try to explain what I was trying to explain before, now with more knowledge of where it isn't relevant 07:10:59 * Cu grimaces 07:11:26 is there any name for the use of {} in functions? 07:11:32 that I can use to conveniently refer to it? 07:11:43 Agda probably has one. Lets call it zooping 07:11:54 It bears some resemblence to the nomic use. 07:11:59 (but only some£ 07:12:03 ok 07:12:12 ) 07:12:14 Wait 07:12:40 Zoop is the argument or the action of Ingerring a value? 07:12:43 Which 07:12:49 the latter 07:12:52 Ok 07:12:58 so, when you zoop an argument, what you are doing is providing an imaginary argument that the compiler magically inserts based on some value 07:13:11 Real argument. 07:13:19 imaginary in the sense that the user never sees it 07:13:21 As real as any argument. 07:13:29 otherwise, 100% real 07:13:36 It exists. If you want to you can use it in the function 07:13:47 But no 07:13:58 Not based on some value 07:14:11 It is disconnected from dependentvtyping 07:14:33 I mean it handles it 07:14:54 But {} does not require the type to be dependent. 07:15:01 wait, let's step back, I just realized there's something I don't get 07:15:08 Although it's not much use otherwise 07:15:13 Even n is a family of types, one for each integer, all sharing the same values? 07:15:27 Almost right. 07:15:46 All the even ns share the same value, poop 07:15:56 All the odd ns have no values at all 07:16:11 I.e you cannot have a value of type Even 1 07:16:12 ok 07:16:45 Cu: All the compiler does is 07:16:47 so, my question is does this mechanism, specifically when used for zooping, have any advantage over a predicate that is used as part of the type matching? 07:16:53 Gives it "poop" 07:16:55 That's it 07:17:00 No magic 07:17:07 yessir, I get that 07:18:00 Also, no, except for being simpler, having an obvious way to pass proofs, and being the same mechanism that things like printf use 07:18:14 All of which make me very skeptical of your idea. 07:18:32 ok, so, ignore q1, that's sort of academic at this point as I'm trying to simplify it 07:18:38 q1? 07:18:44 point 1, whatever 07:18:46 tired 07:18:52 Point 1? 07:18:53 point 2, I don't quite understand 07:18:59 point 1 = simpler 07:19:00 Oh 07:19:01 I see 07:19:07 point 3, I'm not sure is related 07:19:13 The way to pass proofs is 07:19:25 evenClub input {...} 07:19:36 ah, I see 07:19:43 I was sort of missing that bit 07:19:45 -!- Cu has changed nick to coppro. 07:19:51 I.e. If there is an {} arg at this position, {} passes one In explicitly 07:19:59 right, ok 07:19:59 -!- puzzlet has changed nick to puzlet. 07:20:06 -!- puzzlet has joined. 07:20:11 just a thought 07:20:22 if you defined Even : nat -> * as a data type 07:20:28 lack of information is a dangerous thing 07:20:31 you could maybe erase the index to get Even : * 07:20:44 and then you've got a data type that represents even numbers 07:20:45 -!- puzlet has quit ("leaving"). 07:20:54 soupdragon: Yes 07:20:56 although it's isomorphic to nat 07:21:03 How would you erase the index tho? 07:21:15 Ugh, just discovered a major flaw with ZREO's "official" OoT release 07:21:15 The issue with that is 07:21:15 just delete it in a text editor 07:21:20 I don't mean automatically 07:21:22 gonna have to complain 07:21:23 No convenient {...} 07:21:39 soupdragon: How 07:21:42 Lets say 07:22:03 -!- puzzlet has quit (Client Quit). 07:22:10 type Even n | even n = Poopy; type Even _ = Lame 07:22:22 I was thinking of 07:22:22 data Even : nat -> * where EZ : Even Z ; ES : Even n -> Even (S (S n)) 07:22:23 How do you erase the arg there? 07:22:37 -!- puzzlet has joined. 07:22:40 which you can erase to 07:22:49 data Even : * where EZ : Even ; ES : Even -> Even 07:22:59 soupdragon: totally boring tho 07:23:08 not to me 07:23:11 writing a boring type for every constraint 07:23:54 coppro: Oot the zelda game? 07:23:56 or 07:23:59 ehirdiphone: yes 07:24:08 "release"? 07:24:12 ZREO = Zelda Reorchestrated, an awesome project to redo Zelda music in awesomeness 07:24:18 Ah. 07:24:20 they released the OoT soundtrack today 07:24:40 except half the Ocarina songs are Ocarina-only, and half are full music 07:24:50 one way or the other I could see, but half-and-half? 07:25:15 (I highly recommend downloading it, btw) 07:26:15 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 07:26:27 -!- ehirdiphone has joined. 07:26:43 My language will have not only infix operators 07:26:51 But prefix and postfix too :D 07:27:06 Perl 6-style? 07:27:12 or Agda style? 07:27:21 My style. 07:27:30 * coppro doesn't hold his breath 07:27:49 How do you have a style anyway 07:28:01 It's just pre and postfix ops 07:28:43 well, agda allows you do define things pretty much however you want 07:29:06 Did you research Agda in the time since I mentioned it? :P 07:29:29 ehirdiphone: yes. This is the Internet. I'm pretty confident you do the same thing from time to time. 07:29:30 Anyway whaddya mean 07:29:44 Perl 6 is the only other language I could think of offhand that allows the definition of new infix, prefix, and postfix operators 07:29:44 coppro: All the time 07:29:52 A lot of others don't 07:30:28 you also tend to keep your mouth shut when something you don't understand comes up, thus increasing others' perception of you (I do this too, but you're way better at it) 07:30:48 I just have that you can name a function (infix/prefix/postfix symbols) 07:31:03 coppro: I thought I did the opposite xD 07:31:29 ehirdiphone: I mean something you don't understand AND can't readily Google 07:31:41 postfix ! :: Nat -> Nat 07:31:59 ehirdiphone: ok. The only issue is the syntactical ambiguities that can arise 07:32:07 if you allow all three to be overloaded on the same operator 07:32:20 two of the three is fine 07:32:30 infix + :: {n::Type} -> {Num n} -> n -> n -> n 07:33:11 prefix ? :: {t::Type} -> Ref t -> SomeMonad t 07:33:37 ok 07:33:37 coppro: I'd just use operator precedence to disambiguate 07:33:47 Failing that, flag an error 07:33:51 ehirdiphone: ok 07:34:00 I forget what method Perl 6 uses... something evil 07:34:12 (you can define your own precedence and left right association) 07:34:15 Like haskell 07:34:31 ehirdiphoneinfix + :: {n::Type} -> {Num n} -> n -> n -> n 07:34:39 notice anything interesting? 07:34:59 you defined your own keyword there? 07:35:05 Lol 07:35:11 No 07:35:17 what does {n::Type} mean? 07:35:20 Ignore that part 07:35:22 inference of n's type? 07:35:37 coppro: You know what (n::Int) means right? 07:35:46 I think so 07:35:48 Int argument, magic dependent value n 07:35:56 magic dependent value? 07:36:01 I thought of it as "named n" 07:36:07 Well yes 07:36:25 So n is thr value if the arg 07:36:27 {} means infer the type, and let me refer to it as Type? 07:36:32 Which we don't know ar that point 07:36:35 coppro: Ni 07:36:36 No 07:36:44 Listen 07:36:53 Int :: Type 07:36:56 That is 07:37:03 Types are of type Type 07:37:06 That's why 07:37:19 type Printf :: String -> Type 07:37:44 oh, ok 07:37:48 So {t::Type} is "a type t; infer value" 07:37:57 That's how we do polymorphism! 07:38:07 so t becomes whatever the argument's type is? 07:38:13 We can use t later in the signature 07:38:16 So 07:38:26 could I do {n::t::Type} ? 07:38:27 If we pass it an argument if a certain type 07:38:33 This sentence is syntactically unambiguous. 07:38:41 Obviously t has to be that type! 07:38:44 coppro: No 07:38:47 :( 07:38:56 It is another argument 07:39:21 infix + :: {n::Type} -> {Num n} -> n -> n -> n 07:39:28 Notice anything else interesting? 07:39:59 it's an infix that appears to take 3 arguments? 07:40:11 4 07:40:12 Four actually. 07:40:19 Last n is the result 07:40:37 coppro: It's {Num n} 07:40:45 That's how we do typeclasses! 07:40:55 oh, yeah, I'd worked that bit out 07:41:02 >_< 07:41:48 for some reason it was particularly plain to me that {Num n} meant that the type n is some number 07:42:17 coppro: Were you around for the module system stuff? 07:42:35 ehirdiphone: no, but I am familiar with the notion of metatypes, which is why I think that bit came so easily 07:42:46 No it's a different thing 07:42:50 Wait a sex 07:42:51 ... 07:42:54 Sec 07:43:11 Link me to todays log please 07:43:27 http://tunes.org/~nef/logs/esoteric/09.12.29 07:43:36 yeah, I didn't think they were related 07:43:40 So I can findvwhere it is; it really is one of the best parts of the language IMO 07:43:42 that didn't quite come out right 07:43:53 was that the bit about open Foo? 07:44:47 -!- cal153 has joined. 07:44:55 But a lot mote before that 07:45:00 * coppro wonders why he feigns stupidity in this channel 07:45:04 First use of "segue" in log 07:45:15 See if you missed any of it 07:45:23 probably so that guys have a chance to show how smart and alpha they are 07:47:22 ah, now I remember another question I had, and realized you'd answered it 07:47:27 s/realized/realize/ 07:47:33 What question? 07:47:57 coppro: Btw there's a blip in the module talk 07:48:05 Scroll down if you think it's over 07:48:16 Before "c=" 07:48:37 It's not over 07:48:56 right, I remembered that vaguely 07:49:06 So what was the question? 07:49:17 whether you would have full-on type genericism 07:49:40 Eh? 07:49:43 specifically, the ability to make an entire interface dependent on another type 07:49:50 Like howso 07:49:56 which, clearly you can do by generating modules from functors 07:50:02 Like java genetics? 07:50:05 Genetics 07:50:07 Fff 07:50:09 lol 07:50:21 If so, yeah, old hat. Of course. 07:50:22 java's genetics consist of a whole bunch of un-evolution 07:50:33 huh? 07:50:36 yeah, I just wanted to make sure you'd have a mechanism for that 07:50:51 (and actually, C++ templates is closer than Java generics, but w/e) 07:51:01 Yeah 07:52:59 I have been talking about this Lang for so long. Wow. 07:54:32 coppro: I'd give you an awesome explanation of one of the things the Lang will use but I've only really thought it out verbally :( 07:54:44 try me 07:55:05 But it'd be 50000000 lines of typing. :P 07:55:12 oh ok 07:55:19 I'll snail mail you a cassette :D 07:56:05 All this phone and I never speak into it. 07:57:06 * ehirdiphone tries the voice recorder 07:57:08 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:07:30 -!- ehirdiphone has joined. 08:07:40 coppro: What did I miss? 08:07:55 nothing 08:08:04 I did have one thing to say to you, but I forgot 08:08:39 coppro: I recorded a ~four minute explanation of the thing but it'd be in multiple parts 08:08:55 Can you handle my unbroken voice????????//:: 08:09:00 * coppro is not sure 08:09:24 It's not squeaky! Just... Hovering. 08:09:56 as opposed to hemming-and-hawing? 08:10:00 Lawlz 08:10:05 I'll just send it 08:10:09 -!- ehirdiphone has quit (Client Quit). 08:13:11 -!- ehirdiphone has joined. 08:13:22 coppro: Sending them by email now 08:13:32 ok 08:13:43 Wait for all three parts to arrive then set them up in a playlist or sth 08:13:50 Just software foibles 08:13:54 sth? 08:14:00 Would prefer it were continuous 08:14:04 ok 08:14:08 coppro: Somethubg 08:14:11 Thing 08:14:14 =sth 08:14:16 oh 08:14:27 .m4a sorry. iPhones fault 08:14:56 yuk 08:16:06 Any arrived yet? 08:16:28 negative 08:17:03 My speaking skills are improving, not many ums or pauses in that 08:17:14 Or mistakes :P 08:18:19 coppro: in spam maybe? 08:18:48 unless you're trying to sell me replica rolexes, no 08:19:00 *rep1ica ro1exes 08:20:49 This is coppro @ gmail com right 08:20:57 no 08:20:59 rideau3@gmail.com 08:21:06 thanks for spamming some random guy 08:21:10 :D 08:21:17 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 08:21:32 l o l 08:22:00 ais523: go to messages, hit propose or accept trade, fill in the form 08:22:51 thanks, got it, and that's a /really/ weird channel-bounce 08:22:55 cross-server, even cross-protocol 08:23:06 :D 08:23:18 too lazy to type /msg ais523 on a chat without tab-complete 08:23:40 -!- ehirdiphone has joined. 08:23:48 remaile (har har funny pun) 08:23:55 *remailed 08:24:20 coppro: heh, I was just thinking that myself 08:24:47 Propose or accept what what 08:24:52 HAHAHA 08:24:54 http://www.wolframalpha.com/input/?i=tea%2C+earl+gray%2C+hot 08:25:18 ehirdiphone: I was giving him advice for KoL 08:25:45 KoL is kinda rubbish IMO :| 08:25:50 agreed 08:25:57 watsa kol 08:26:01 that's sorta the point 08:26:19 "Its meant to be shit don't you SEE" 08:26:24 augur: a rather low-tech MMO 08:26:36 oh ok 08:26:42 Web based 08:26:50 It's really just clicking yes a lot 08:26:55 Or going somewhere 08:27:06 Then clicking fight a lot 08:27:18 mostly I play it for the fun in /games, to be honest 08:27:20 it's a moderate amount of strategy + a lot of boredom 08:27:25 (though it probably won't appeal to most everyone here) 08:27:52 but it's a nice distraction 08:32:03 -!- coppro has quit (Remote closed the connection). 08:32:51 incidentally, I realised that ais523 hates collectively-covering-costs cooperatives. Let's say membership dues = cost/members. This way, everyone pays the same money, and nobody gets rich. By recommending the service to someone who then joins it, the recommender pays cost/(members (members+1)) less each $interval, where members is the number of members before the new member is recruited 08:33:18 so this fair, collectivist cooperative is considered to be evil by ais523 :) 08:33:22 ehirdiphone: it's not quite hate, it's more untrust 08:33:25 Did that get cut off? 08:33:30 no, it didn't 08:33:38 Ended at "member is recruited" 08:33:44 yes 08:34:01 if someone recommends something to me and stands to gain from that, I treat it as a paid advert, rather than as freely-given advice 08:34:07 doesn't mean it's unwelcome or bad, just untrustworthy 08:34:07 ais523: So do you not distrust if nobody makes a profit? 08:34:21 And they don't make a profit per se 08:34:29 EVERYONE pays less 08:34:34 It's altruistic 08:34:47 yes... but suppose you have two identical cooperatives 08:34:51 except that you're in one of them 08:35:03 the question here, I suppose, is why should I join the one with you in rather than the other one? 08:35:11 now, suppose the other one has one more member but is otherwise identical 08:36:02 So you distrust profitless, collectivist cooperatives. 08:36:17 no 08:36:24 Favouring instead recommendations that involve a business making a handy profit. 08:36:31 I distrust recruitment drives that would drive me towards one of them rather than a different one of them 08:36:34 Intriguing. 08:36:55 ais523: But that's how they WORK! evryone pays an equal amount 08:36:59 Cost/members 08:37:02 It 08:37:07 ehirdiphone: I don't hate the collective itself 08:37:10 's the whole point 08:37:17 I just mistrust /recommendations of which collective to join/ 08:37:24 from a member of the collective itself 08:37:36 Thing is 08:37:36 I might still favour the entire concept over a for-profit company 08:38:27 If soneone thought another service was superior they wouldn't reccommend theirs just for profit. They'd SWITCH to that alternative THRN reccommend them 08:38:41 Doing otherwise is ridiculously nonsensical 08:38:49 *THEB 08:38:56 *THEN 08:40:55 silence! 08:41:45 btw they're cooperatives not collectives 08:42:03 Wonder if anyone's registered http://chicken.coop yet :D 08:42:14 Negative 08:45:16 ais523: Do you want my lovely voice explanations of frp, coppro iz ded :< 08:45:35 ehirdiphone: frp? 08:45:46 THEY EXPLAIN IT WITH THE GRACE OF AN OSTRICH 08:45:55 ehirdiphone: oh, that's a good argument, about switching 08:45:57 ais523: Should I take that as a yes? :P 08:46:12 for something that's really switchable, I'll consider that to rebut my points 08:46:25 also, no, that's me asking you to explain frp before I decide whether I should ask you to explain it or not 08:46:28 Like hosting :p 08:46:34 ais523: _|_ 08:46:41 That's not a middle finger 08:46:53 it's an upside-down T? 08:47:00 That's bottom, your friendly nonterminating value! 08:47:17 ehirdiphone: http://www.wolframalpha.com/input/?i=Mudkipz 08:47:38 bottom can also mean nil or false, depending on the language in question. 08:47:46 No. 08:47:58 I have never ever heard that. 08:48:02 it's the return value of a function with an infinite loop in 08:48:22 ehirdiphone: in logic its not uncommon to find bottom for false 08:48:22 ais523: Actually, errors are _|_ too 08:48:37 poop = error "blah" 08:48:41 poop is bottom 08:48:43 it's kind-of a different sort of return value... 08:48:48 Nope 08:48:51 what about throwing an exception past the caller to a handler outside? 08:49:06 All types are TheType | _|_ 08:49:17 Unless you use Total FP 08:49:22 But that's sub tc 08:49:36 ais523: In the io monad 08:49:41 If not, yep _|_ 08:49:56 Want those audios? :-( 08:50:36 ok, so this explains bottom, which almost certainly has its own unicode char 08:50:46 Yeah 08:50:54 Logical false or sth 08:51:08 ⟂ 08:51:18 actually used for the geometric meaning, "perpendicular to" 08:51:23 http://en.wikipedia.org/wiki/Bottom_type 08:51:54 also http://en.wikipedia.org/wiki/Bottom_element 08:52:50 says common lisp's nil is a bottom. 08:52:58 which im not sure i buy, but whatever 08:53:29 You're a bottom. Er, I think this conversation just strayed into territory I don't want it to stray into. 08:53:34 well, i am, but. 08:53:35 butt. 08:53:57 it seems like Bottom can be non-termination, but it can be other things as well 08:54:02 including null 08:54:13 ais523: There are two chars iirc 08:54:21 WANT THE AUDIO? 08:54:23 and other things that might be conceived as non-termination in some abstract sense 08:54:28 e.g. not returning a value at all 08:54:30 ehirdiphone: err, I don't see why audio's relevant 08:54:44 ais523: The voice explanation of frp 08:54:57 I'd prefer IRC 08:55:02 SOMEONE LOVE ME ;;;;;;;;;;;_;;;;;;;; 08:55:11 ais523: but I already recorded it :p 08:55:21 ehirdiphone: i love you! 08:55:26 in that special way 08:55:27 I'm not transcribing 4 minutes of speech :D 08:55:41 augur: the ephebophilic way? 08:55:50 ugh, filebin.ca is still malware-blocked 08:55:58 no ofcourse not 08:56:00 I could just get around the block, but it feels wrong to do that somehow 08:56:01 that would be wrong 08:56:15 so so wrong 08:56:35 Yeah. Blocks are sacrosanct! 08:56:41 Oh I love comedic timing 08:58:03 NOBODY LIKES MY VOICE ;;;;;;;;;_;;;;;;;;; 09:00:59 your voice is girly 09:01:12 so i imagine people into girls like your voice 09:01:58 :| 09:03:46 its ok 09:03:48 youre still adorable 09:10:32 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 09:11:06 -!- ehirdiphone has joined. 09:11:10 wabi 09:14:38 -!- mycroftiv has quit (Read error: 104 (Connection reset by peer)). 09:15:42 My conversation died :( 09:15:49 :( 09:15:56 I was enjoying talking about that language 09:16:12 what language 09:19:08 4 hours 12 minutes. I talked about it continuously for about that long. Wow. 09:19:17 augur: My language. 09:19:26 which language is that 09:19:30 Mine. 09:19:36 which is? 09:19:43 Mine. 09:19:45 :| 09:20:10 Do you feel up to reading 4h12m of talk? 09:20:16 no 09:20:21 can you summarize it please 09:20:25 No. 09:20:27 ok 09:21:27 Oh well. 09:21:29 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 09:28:12 -!- mycroftiv has joined. 09:58:54 -!- FireFly has joined. 10:30:30 -!- ehirdiphone has joined. 10:30:42 So, I had a brilliterrible idea. 10:31:37 the sort of thing ais523 would think of if he just generated ideas without honing on interesting things, I think 10:31:48 heh 10:31:55 Neural analogies whatever next 10:32:02 actually, I do do that, just most of the boring stuff gets discarded straight off 10:32:06 and I never tell anyone then forget 10:32:30 An Emacs X11 WM that actually makes the windows into Emacs buffers. 10:32:54 (the xemacs wm thing is just a wm written in elisp. Lame.) 10:33:00 -!- adam_d has joined. 10:33:50 ehirdiphone: heh, Blender works a bit like that 10:33:55 at least, it seems to have stolen the Emacs WM 10:37:19 It would be kinda cool actually 10:37:53 ais523: imagine a modeline on a window 10:38:10 ehirdiphone: heh 10:38:13 although, what would the modes be 10:39:07 Well, xwm-window-mode for one 10:39:22 with the oblig menus with actions and settings 10:39:34 Minor modes... hmm 10:39:53 ais523: xwm-floating-mode, perhaps? 10:40:10 no, that's C-x 5 10:40:18 meaning? 10:40:25 C-x 5 2, rather than C-x 2 10:40:33 to create a floating rather than docked window 10:40:35 new-frame or sth? 10:40:38 yes 10:40:56 that would just open an emacs frame in an emacs buffer :D 10:41:50 no, the point is 10:41:53 your applications are buffers 10:41:58 windows 10:41:59 you can swap them in and out of windows at will 10:42:04 Not applications 10:42:12 ais523: You misunderstand 10:42:18 ehirdiphone: you mis-emacs 10:42:34 X11 windows would be drawn in their own BONAFIDE emacs buffer 10:42:40 Not emacsalike 10:42:47 Actually an emacs buffer 10:43:02 that's what I meant too 10:43:14 Root window = emacs, no window management done on it PFC 10:43:17 IFC 10:43:20 Ofc 10:43:23 one window produced by an application under a normal WM = one Emacs buffer 10:43:30 yes 10:44:13 but there shall be only One emacs window; for lo, that is what the Prophet did spaketh unto ya 10:44:20 *us: 10:44:52 ehirdiphone: err, no 10:44:54 C-x 2 is two emacs windows already 10:45:01 you need emacs windows to put the buffers in 10:45:04 "If Emacs be the heritor of thou'st windows, is it not therefore a Sin to have Emacs begat itself?" 10:45:17 /every/ window is an Emacs window 10:45:28 There shall be only one Emacs window, and it shall be the root. 10:45:34 ais523: X11 window 10:45:37 ah, ok 10:45:40 I was talking about emacs window 10:45:48 how would you do extra emacs frames, though? 10:45:55 Wouldn't 10:46:01 I might think about doing it 10:46:03 Dunno 10:46:08 but that's losing possibilities you have with emacs's wm at the moment 10:46:19 the ability to create a floating frame that works independently of the others 10:46:20 Yes, but Emacs is tiling. 10:46:26 it's tiling and floating 10:46:36 hmm... I wonder if C-x 5 o works? 10:46:48 no. Emacs itself is tiling 10:47:01 Other WMs do the floating 10:47:11 well, ok 10:47:15 so an emacs wm should do as emacs does 10:47:18 hmm... this is a tricky one 10:47:19 And only tile 10:47:32 ais523: BUT 10:47:42 If floating is to be offered 10:48:15 It should be recognised as a heresy unique to the Xfolk; lacking as the result is in Emacs mannerisms, 10:48:28 being an unadorned Xdevil, 10:48:50 and so on — it is of the Xwindow. 10:49:17 Therefore, xwm-floating-mode. Q.E.D. 10:49:46 in the model here emacs frames "don't exist" 10:49:53 It's like an emacs os 10:49:59 Emacs is the interface 10:50:18 Frames become an implementation detail; only one, as the root window. 10:50:40 hmm, but a floating-mode window makes absolutely no sense in that case 10:50:42 as it isn't anywhere 10:50:47 from Emacs' point of view 10:50:59 you couldn't select it, you couldn't close it, you couldn't create it 10:51:05 it is "in" emacs because emacs' size is that of the screen 10:51:23 but it's in a different frame 10:51:25 also, if you focus it the invisible corresponding buffer is too 10:51:32 ais523: No such thing. 10:51:36 exactly 10:51:37 Implementation detail. 10:51:38 thus it isn't there at all 10:51:52 Windows are Emacs' forte. Frames it thinks of not. 10:51:53 it isn't in the root frame because you can't get to it by recursively picking top, left, etc... windows 10:52:07 It is omnipotent and sovereign over them. 10:52:12 e.g. it would make no sense for C-x o to /cycle/ to it 10:52:18 brb 10:52:20 and if it did, what would C-x 2 do? or worse, C-x 1? 10:52:34 ais523: Its like a buffer not in the frame 10:52:37 Erm 10:52:39 View 10:52:41 You know 10:52:51 ehirdiphone: oh, in that case, it wouldn't render at all 10:52:52 Not in the tiling buffer arrangement 10:53:01 so you'd have no way of focusing on it 10:53:10 ais523: Yes it would because we coded it that way 10:53:12 brb 10:55:50 -!- oerjan has joined. 11:07:50 Hi oerjan 11:07:55 hi ehirdiphone 11:08:12 oerjan: Good luck logreading 11:08:24 nah 11:08:30 4 hrs 12 mins continous talk about my language 11:08:32 just searched for my name today 11:08:48 You missed out on so much :( 11:08:52 s/name/nick/ 11:08:59 ais523: Issue 11:09:18 Your emacs buffer list would be polluted. Cool for window managing 11:09:20 what? I'm about to go home to sleep 11:09:22 alas, i usually only read the whole log when it is short 11:09:23 Suck for editing 11:09:39 ehirdiphone: really? I often have over 30 or so buffers open 11:09:43 oerjan: it has haskelly type theory! 11:09:45 I rarely kill them, you see 11:09:51 ais523: well, ok 11:09:55 and don't use the buffer list at all, except by mistake 11:09:57 But what to name them! 11:10:00 *? 11:10:06 The window title? 11:10:17 "title - prog"? 11:10:23 with asterisks around it if it's not meant to be saved 11:10:33 "title - prog [xwm]" 11:10:34 yes, you should be able to save buffers even if they contain windows 11:10:42 ais523: uh. No. 11:10:52 but ugh, it'd be ugly 11:11:04 otherwise the semantics are wrong 11:11:12 you could hook it up to cryopid or something, I suppose 11:11:15 i did see the comment about it being more CS than haskell. which actually leaves me suspicious if you are over your head, since my understanding is that creating a sound type system more advanced than haskell's (or even equal) is _hard_ 11:11:17 **reddit - what's new online! - Mozilla Firefox** 11:11:26 *in over your head 11:11:26 or ideally, just have the programs that run be easy to escape 11:11:39 ehirdiphone: Firefox is a big example of something that should save 11:11:40 oerjan: I know it is possible. Agda and Ur do it. 11:11:56 ais523: You can't coherently save tetris f.e. 11:11:56 after all, it has a save-tabs-on-closing option, this would be the same thing 11:11:59 -!- FireFly has quit (Read error: 60 (Operation timed out)). 11:12:08 ehirdiphone: yeah, but i'm assuming there were phd theses involved :D 11:12:09 ehirdiphone: really? I've seen pieces of hardware that could 11:12:10 It's a wm not an os 11:12:12 pause, turn it off 11:12:14 at the very least 11:12:21 ais523: M x tetris 11:12:22 cant you just make sure that you are within the formal boundaries established by hindley-milner typing? 11:12:31 oerjan: And they're open source 11:12:31 anyway, I really had better go 11:12:35 -!- ais523 has quit (Remote closed the connection). 11:12:37 of course, more power to you if you can pull it off 11:12:38 mycroftiv: I exceed those boundaries 11:12:40 -!- FireFly has joined. 11:12:44 TC type system 11:12:53 W/ dependent types 11:13:04 i havent read the immensely huge backscroll so i wont make you explain it all again if you already have 11:13:48 actually i guess i lost most of my backscroll from my mouse button forkbombing me 11:14:00 oerjan: maybe I'll just submit the spec and compiler as a phd thesis to MIT or somewhere without being admitted :D 11:14:15 easiest doctorate evar 11:15:10 oerjan: but yeah, it won't be easy 11:15:55 so what it's so damn awesome :| 11:15:57 ehirdiphone: it is the soundness proof of your type system i am worried about. not that i know how to do those myself 11:16:43 unless you simply steal an already existing one, you'll have to redo it, and i understand it's quite technical stuff 11:16:45 oerjan: If type checking can bottom out surely it's unsound by some definition 11:17:14 i mean in the cannot-go-wrong sense, i think 11:17:22 incomplete 11:17:28 Bottoming out is going wrong to me 11:17:34 unsound would be like, 3 : String 11:18:03 it must be one of either 11:18:11 presumably incomplete 11:18:15 oerjan the fun with dependent types is you need to interleave the value normalization proof 11:18:19 i.e. Sound 11:18:29 soupdragon: ouch 11:18:44 maybe I'll contract a phd out to do the proof :) 11:19:03 Or just assume it's sound xD 11:19:16 ehirdiphone: what soupdragon said. non-termination is fine, except i also recall reading that dependent typing has trouble if your _types_ can bottom out, because then you need to actually evaluate the proofs in the runtime program, you cannot remove that stuff during compilation 11:19:39 types bottoming out as in 11:19:43 because if a proof of well-typed-ness can bottom out, then it is invalid 11:19:52 Foo Integer = _|_ 11:19:53 ? 11:19:56 um proofs of types, i guess 11:19:57 no 11:20:11 ah 11:20:13 I see 11:20:14 that is not dependent. 11:20:23 right 11:20:47 oerjan: I was thinking of using a total subset 11:20:52 for the proofs 11:22:53 tbh I think my type system is likely incredibly similar to say agda 11:22:59 just different notation 11:23:52 i recall some mention of using a monad to encapsulate non-termination 11:24:20 codata Computation A where Now : A -> Computation A ; Later : Computation A -> Computation A 11:24:36 then it would presumably be fine, since types are not in that monad, or something 11:24:45 then you can race omega many of these for a fixed point 11:24:48 least fixed point 11:26:09 um shouldn't the _result_ be an A for some option? 11:26:33 -!- anmaster_l has joined. 11:26:50 Don't want to make partiality a monad 11:27:20 Hmm my type system is probably closest to epigram 11:27:37 programming more than proofy and haskellsimilar as it is 11:27:40 it was for epigram i heard that mention, i think 11:27:53 what mention? 11:27:58 of the monad 11:28:12 ah 11:28:12 except it was not something implemented, iirc 11:28:14 really? 11:28:26 -!- MigoMipo has joined. 11:28:32 I used it in haskell to write (even more) lazy programs 11:28:33 It just makes code awkward having a partiality monad :p 11:28:35 just an idea for making epigram practically TC 11:28:57 at some point I surrender safety for practicality 11:29:14 the partiality monad is that point 11:29:28 yeah I have no idea how to do even simple proofs about termination for the partiality monad 11:29:54 oerjan: wait, isn't epigram tc? 11:30:04 You're thinking of that other Lang 11:30:07 Charity 11:30:22 ehirdiphone: i thought epigram was a total language 11:30:46 hmm. Maybe epigram 1 is but 2 not? Dunno 11:30:55 Maybe both are total 11:31:20 I think it's a weird question, the function space is total but you can still define things like turing machines, mu-recursive functions and their operational behavior 11:31:25 * oerjan may very well be confused, has only read discussions (on ltu mostly?) and that was long ago 11:31:51 well one step of a turing machine computation is total... 11:32:14 yeah you can take the transitive closure of it though 11:32:33 poop. 11:32:45 ehirdiphone: hm? 11:33:16 anyway ur works and only has one phd behind it 11:33:22 I rest my case :p 11:33:53 Ur isn't actually dependently typed is it 11:34:09 I think it is? 11:40:07 hmm 11:40:45 soupdragon: it does have type-level programming that constructs values. I'd be surprised if it wasn't dependent 11:41:06 I wish I could compile it :| 11:41:17 Why can't you? 11:41:33 soem error to do with gmp or something 11:41:53 I'll fix it gimme ssh :P 11:47:40 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info"). 11:49:23 -!- Pthing has quit (Remote closed the connection). 12:21:15 -!- oerjan has quit ("leaving"). 12:23:44 -!- cheater has joined. 12:23:50 hi guys 12:24:25 has anyone got a working implementation of Piet or a similar lang? 13:44:12 -!- MizardX has joined. 13:45:06 -!- adam_d_ has joined. 13:53:31 -!- adam_d has quit (Read error: 60 (Operation timed out)). 13:53:53 -!- MizardX has quit ("..."). 14:09:05 -!- Sgeo has joined. 14:09:41 Hm, ehird's not here? 14:10:18 ehird, if you see this, know that the penultimate story of Fine Structure has been published. 14:10:23 -!- adam_d_ has quit (Read error: 110 (Connection timed out)). 14:35:28 -!- soupdragon has quit ("Leaving"). 14:53:07 -!- MigoMipo has quit ("When two people dream the same dream, it ceases to be an illusion. KVIrc 3.4.2 Shiny http://www.kvirc.net"). 14:55:59 -!- BeholdMyGlory has joined. 14:59:04 -!- Asztal has joined. 15:07:20 -!- bsmntbombdood has quit (Read error: 110 (Connection timed out)). 16:27:49 Sgeo: Yowza. 16:50:59 -!- Slereah has joined. 17:00:59 -!- Slereah_ has quit (Read error: 110 (Connection timed out)). 17:19:22 -!- BeholdMyGlory has quit (Read error: 104 (Connection reset by peer)). 17:21:07 -!- adam_d has joined. 17:23:51 -!- BeholdMyGlory has joined. 18:14:36 -!- adam_d_ has joined. 18:29:20 -!- adam_d has quit (Read error: 110 (Connection timed out)). 19:21:13 -!- MizardX has joined. 19:32:20 -!- jpc has joined. 20:03:18 -!- BeholdMyGlory has quit (Remote closed the connection). 20:10:41 -!- BeholdMyGlory has joined. 20:16:33 -!- oerjan has joined. 20:19:19 has anyone got a working implementation of Piet or a similar lang? 20:19:36 have you checked the author's home page at http://www.dangermouse.net/esoteric/piet/tools.html ? 20:34:30 -!- brado has joined. 20:34:55 -!- brado has left (?). 20:41:34 cheater: see above ^ 21:55:55 -!- coppro has joined. 21:56:25 -!- Gracenotes has quit ("Leaving"). 21:58:50 -!- calamari has joined. 22:21:24 -!- Fredrik1994 has joined. 22:21:29 -!- Fredrik1994 has left (?). 22:44:10 -!- MAKACOW has joined. 22:49:42 -!- MAKACOW has left (?). 23:15:08 -!- Gracenotes has joined. 23:18:46 -!- soupdragon has joined. 23:34:42 -!- soupdragon has quit (Read error: 60 (Operation timed out)). 23:50:22 -!- calamari has quit ("Leaving"). 23:56:18 oerjan, dmm made piet!? 23:56:23 yes 23:57:24 indeed 23:57:50 and several others 23:59:14 http://dangermouse.net/esoteric/