< 1262132120 0 :FireFly!unknown@unknown.invalid QUIT :"Leaving" < 1262132488 0 :bsmntbombgirl!unknown@unknown.invalid QUIT :Read error: 101 (Network is unreachable) < 1262132917 0 :Pthing!n=pthing@cpc11-pres4-0-0-cust168.pres.cable.virginmedia.com JOIN :#esoteric < 1262132918 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262133185 0 :oerjan!unknown@unknown.invalid QUIT :"Spyong" < 1262133329 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So good to hear about Mike. < 1262133356 0 :MigoMipo!n=MigoMipo@84-217-13-28.tn.glocalnet.net JOIN :#esoteric < 1262133391 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262133422 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :? < 1262134583 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262134606 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: See todays logs. < 1262134611 0 :ehirdiphone!unknown@unknown.invalid QUIT :Client Quit < 1262134808 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1262135245 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :definitely < 1262135303 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :definitely good or definitely hm? < 1262135670 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :definitely good < 1262137044 0 :|MigoMipo|!n=MigoMipo@84-217-13-28.tn.glocalnet.net JOIN :#esoteric < 1262137078 0 :|MigoMipo|!unknown@unknown.invalid QUIT :Remote closed the connection < 1262137566 0 :MigoMipo!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262138105 0 :coppro!unknown@unknown.invalid QUIT :Remote closed the connection < 1262138357 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote closed the connection < 1262139793 0 :coppro!n=coppro@unaffiliated/coppro JOIN :#esoteric < 1262140159 0 :anmaster_l!unknown@unknown.invalid QUIT :Read error: 60 (Operation timed out) < 1262141300 0 :Slereah_!unknown@unknown.invalid QUIT :Read error: 60 (Operation timed out) < 1262141474 0 :Slereah!n=Slereah@ANantes-259-1-70-166.w92-135.abo.wanadoo.fr JOIN :#esoteric < 1262143331 0 :Slereah!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262143667 0 :Slereah!n=Slereah@ANantes-259-1-70-166.w92-135.abo.wanadoo.fr JOIN :#esoteric < 1262143777 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262143812 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Who wants to hear about my borderline-eso lang? :P < 1262143831 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(proof of esoness: it's more CS than haskell) < 1262143837 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :I do < 1262143857 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :but I already told you the basics yesterday :P < 1262143870 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Elaboration is so passé < 1262143905 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(more to the point I wouldn't know where to start elaborating) < 1262143957 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: If you as a specific question I can prolly answer < 1262143998 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :is your friend bipolar < 1262144012 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :what friend < 1262144027 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You mean mike Riley? < 1262144098 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :it is just such a contrast that I am a bit confused by it < 1262144156 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :What are you referring to? his present crisislessness? < 1262144175 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :yeh < 1262144205 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :he has chronic depression and saw a therapist so presumably it's not doing its chronic thing right now < 1262144255 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Sleep pattern messed up again? < 1262144266 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :sort-of < 1262144275 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, I sometimes have late Internet nights deliberately, so I can talk to americans < 1262144280 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(also, nethack.de?) < 1262144291 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :this time it's because it's rather snowy and I didn't want to walk home in it < 1262144295 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: heh. Mine's messed up too < 1262144302 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: you'd have no idea how hard it is to internationalise NetHack < 1262144312 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but mostly, it's because Germany's closer than the US < 1262144313 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ask me about my language! < 1262144318 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and lag is pretty important when playing NetHack < 1262144322 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :anyway, what language? < 1262144345 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Unnamed. Borderline eso. More CS than haskell < 1262144372 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :wait, what? is that even possible? < 1262144379 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yep < 1262144391 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :how might it do I/O? < 1262144401 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Even agda is more cs < 1262144410 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But not so good for regular programming < 1262144417 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :rofl Talking to Americans < 1262144428 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :coppro: why is that amusing? < 1262144437 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Basic text io... Prolly monads. < 1262144451 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :http://en.wikipedia.org/wiki/Talking_to_Americans < 1262144456 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ais523: IO? *IO*? How dare you suggest such a thing. < 1262144464 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :GUI and web and stuff? FRP which I won't bother explaining ATM < 1262144471 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: you can only imagine how hard it is in Feather < 1262144472 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :main is a function from String to String! < 1262144481 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Ask for an overview of the cool stuff! :P < 1262144487 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: you know, you could just tell me < 1262144525 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Tru day < 1262144527 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Fat < 1262144529 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Dat < 1262144541 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :***dat? < 1262144546 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yes < 1262144549 0 :Slereah_!n=Slereah@ANantes-259-1-70-166.w92-135.abo.wanadoo.fr JOIN :#esoteric < 1262144586 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Dependent types. ML style module system. Type level metaprogramming. Arbritary syntactic extension. < 1262144592 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ASK ABOUT ANY :P < 1262144604 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :let's start with syntactic extension first < 1262144636 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :then what's the difference between Type level metaprogramming and Dependent types? < 1262144657 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Pretty simple. Modules can add to the syntax of the language, using arbritary code to make the replacement for the syntax < 1262144691 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: The former means inspecting types themselves < 1262144703 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Say, the names of the fields of a record < 1262144707 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And their types < 1262144708 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Etc < 1262144719 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :NEXT QUESTIONS :p < 1262144764 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Do you know what dependent types are btw? < 1262144777 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I think so, but tell me anyway, because terminology is something I easily mess up < 1262144782 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ok < 1262144809 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :In typed lambda calculus, types index on types and values index on values < 1262144812 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That is < 1262144823 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :A type can depend on another type < 1262144828 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Like < 1262144833 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(a,b) < 1262144843 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Indexes on a and n < 1262144844 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :B < 1262144847 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Types < 1262144858 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And values index on values < 1262144861 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :F x < 1262144862 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :I didn't get that ehird < 1262144867 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :F indexes on x < 1262144875 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Get that so far? < 1262144884 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :inspecting types < 1262144886 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You give types to types < 1262144890 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :basically, creating types out of other types < 1262144894 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And values to values < 1262144905 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Thats nit dependent Tuesday < 1262144908 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Types < 1262144914 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :This I'd just bacgriund < 1262144917 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262144934 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: now in haskell < 1262144951 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Typeclasses create values that index on types < 1262144970 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The value of the function show depends on what type it is < 1262144977 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Int -> String < 1262144990 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :String -> String < 1262145002 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :the value of "show" changes < 1262145009 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Get it? < 1262145019 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep < 1262145029 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Now for the kicker < 1262145031 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :like overloaded functions, but much more first-class and genreal < 1262145033 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :*general < 1262145049 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Dependent types = types indexing on values < 1262145053 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :FOR INSTANCE < 1262145060 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :no < 1262145061 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, aha, I did know that, just forgotten I had < 1262145075 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :indexing is just one sort < 1262145085 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Im just explaining it < 1262145086 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so you can have a function that only takes even numbers as arguments, anything else is a typing error? < 1262145091 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not formally defining it < 1262145095 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Yep < 1262145101 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :okay but (=) means something dear to me < 1262145114 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or a vector access function that enforces bounds checking < 1262145121 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :At compile time < 1262145126 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No runtime penalty < 1262145135 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :sounds like what Splint tries and fails to do < 1262145156 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :incidentally, I tried and failed to get my Underlambda interp fully Splint-compliant < 1262145161 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Splint seems really buggy < 1262145169 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :some code I wrote had a bare block for scoping < 1262145173 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :inside a switch statement < 1262145179 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :if I put the break; inside the block, no error < 1262145183 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :if I put it after the block, error < 1262145196 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :even though the two sets of code were completely identical to any compiler < 1262145203 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Anyway, so dependent types makes programs more type Sade < 1262145205 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Safe < 1262145209 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes, definitely < 1262145211 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And < 1262145220 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Lets us do things we couldn't otherwise < 1262145226 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :More permissive things! < 1262145243 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: incidentally, this is how I think a really good BF optimiser would work < 1262145245 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :For instance < 1262145254 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :trying to calculate dependent types for tape elements at different points in a program < 1262145273 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :vararg :: (n :: Integer) -> Vararg n < 1262145276 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And < 1262145312 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type Vararg 0 = (); Vararg n = () -> Vararg (n-1) < 1262145324 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :vararg 0 :: () < 1262145334 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :vararg 1 :: () -> () < 1262145337 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :etc < 1262145347 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ignoring negatives :P < 1262145362 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :curried varargs! < 1262145366 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Implementation if vararg itself: < 1262145376 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :vararg 0 = () < 1262145388 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :actually, I think that's possible in Underload too, but a completely different way < 1262145395 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :vararg n () = vararg (n-1) < 1262145423 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: And this doesn't inspect n at runtime to determine the type! < 1262145433 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep < 1262145437 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's /statically/ correct < 1262145441 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :we need more static correctness in the world < 1262145449 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you know, like Splint but actually working < 1262145451 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If n is say read from stdin you just must satisfy the compiler < 1262145461 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So it knows your call is correct < 1262145464 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: PLUS < 1262145473 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All if this leads to more fun < 1262145478 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Type safe printf < 1262145499 0 :Slereah!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262145500 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :printf :: (fmt :: String) -> Printf fmt < 1262145519 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type Printf [] = IO () < 1262145523 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: you probably want something along the line of C++'s dynamic_cast < 1262145530 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No < 1262145532 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Static < 1262145534 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ssh < 1262145558 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Did someone say C++? :P < 1262145558 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :incidentally, for Cyclexa I was planning what's effectively typesafe /scanf/ < 1262145569 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it physically wouldn't let the user input something of the wrong type < 1262145573 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type Printf ('%':'d':xs) = Integer -> Printf xs < 1262145576 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :haha cool < 1262145595 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION will point out that C++ has lots of static correctness... too much, really
< 1262145605 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type Printf (x:xs) = Printf xs < 1262145616 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :yeah my C++ programs are statically correct.. the problems come when you run them < 1262145619 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: ^^^ dependent types rule < 1262145653 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: haha < 1262145662 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"Dependent types. ML style module system. Type level metaprogramming. Arbritary syntactic extension." < 1262145663 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :C++ doesn't normally enforce static correctness very fully < 1262145667 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Lol < 1262145668 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ok < 1262145674 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :unless you go and implement integers in the type system, or whatever < 1262145674 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :First amd last gone < 1262145679 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Pick one! < 1262145695 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ais523: That comment interests me... what do you mean by that? < 1262145699 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :(apparently, someone won an IOI round like that once) < 1262145705 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :basically, C++ templates are Turing-complete < 1262145719 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :if you write a program in them, the whole thing gets run at compile-time < 1262145735 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :PICK ONE >:( :P < 1262145739 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :ehird, you didn't answer my question (in such a way that I can understand it) < 1262145740 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :do you mean that the type system doesn't allow distinguishing of values? < 1262145747 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Reask < 1262145757 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :coppro: not in C++, but you can use types themselves effectively as values < 1262145759 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :you can do metaprogramming with dependent types < 1262145771 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I'm very familiar with C++, I just wanted clarification :) < 1262145777 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: You have: < 1262145787 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :why don't the dependent types subsume metaprogramming? < 1262145790 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION remembers the WTFBBQ entry that created a separate type for every integer
< 1262145792 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :or do they? < 1262145810 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :data Foo = Foo { a :: Integer, b :: Integer } < 1262145827 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :With dependent types alone, you could not do < 1262145832 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :f Foo < 1262145834 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :== < 1262145836 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :s/WTFBBQ/OMGWTF/ < 1262145843 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :http://thedailywtf.com/Articles/OMGWTF-Finalist-10-FerronCalc.aspx < 1262145850 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :[("a",Integer), < 1262145864 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :("b",Integer)] < 1262145871 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(f being type level) < 1262145881 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :wnat about < 1262145892 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :f (A -> B) = "A -> B" < 1262145895 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :? < 1262145897 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So basically inspecting and creating types programmaticslly in the type system < 1262145905 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Is what I mean < 1262145920 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Ask a mote specific question than what about < 1262145949 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION hopes to be at the 2010 IOI; possibly even as a competitor, though that seems unlikely due to stupid circumstances
< 1262146031 0 :bsmntbombdood!n=gavin@174-16-198-4.hlrn.qwest.net JOIN :#esoteric < 1262146036 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :it seems like you have some kind of quotation for types < 1262146052 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :(and that will have to include values too, because of the dependency) < 1262146061 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: That "f Foo" was not runtime code < 1262146069 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It is type level < 1262146087 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Where of course types are values, duh < 1262146112 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Foo :: Type or :: Set if you fancy < 1262146116 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :well I still don't get it < 1262146127 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :but that's okay < 1262146134 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I would write example code but not on the iph < 1262146136 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ooh < 1262146153 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'll pen write it and photo it >:D < 1262146198 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :haha now you're thinking with iPhones < 1262146235 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Paper. Where is paper < 1262146254 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I HAVE NO PAPER < 1262146285 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262146308 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :ais523, you do most things in your head? or on computer? < 1262146326 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Fuck books with no notes section < 1262146332 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION managed to get a computer for his English exam!
< 1262146343 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I need a bible with a lot of blank pages < 1262146368 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :PAPER < 1262146377 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: both < 1262146389 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: I generally have plenty of paper < 1262146393 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :About to write dependentkly typed code in a ruby on rails book yo < 1262146409 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I don't like putting my netbook down directly on a duvet or whatever as it blocks the air vents < 1262146417 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but it turns out it fits nicely onto an A4 pad of paper < 1262146425 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :AAAAAAA PEN < 1262146429 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Need pen < 1262146430 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION is currently using a cookie tray
< 1262146454 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ok < 1262146491 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :coppro: I didn't realise cookie trays were even approximately TC < 1262146491 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :WTF pen is silver < 1262146498 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: ask your parents? < 1262146504 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ais523: for laptop ventilation < 1262146509 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :coppro: ah < 1262146531 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Its 4am < 1262146539 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :good point < 1262146541 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'm not waking them up :P < 1262146551 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :maybe you should just wait until morning < 1262146555 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :WAIT < 1262146561 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :We have drawers here < 1262146567 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :With things in them < 1262146573 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :SEARCH TIME < 1262146645 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :cookie trays??? < 1262146653 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :YEA < 1262146658 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :PEN < 1262146927 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Photo time < 1262146930 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262147053 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262147061 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I emailed you the photo < 1262147068 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1262147079 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Can you imgur.com it and link the directvlink here? < 1262147080 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :incidentally, filebin.ca's getting reported as a malware site by Firefox < 1262147084 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Thx < 1262147173 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :http://imgur.com/n5amE.jpg < 1262147192 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: < 1262147197 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So here, < 1262147202 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what did you write it /on/? I hope you haven't damaged a book for our sake < 1262147225 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type Fields :: Type -> [(String,Type)] < 1262147227 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :well < 1262147237 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Technically :: Record -> < 1262147246 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But that's not too relevant < 1262147247 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :okay < 1262147257 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Blank page before index < 1262147266 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ugh < 1262147266 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :In ruby on rails book - worthless < 1262147276 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: you might have been able to sell on that book... < 1262147276 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: See what I mean now? < 1262147283 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1262147292 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :D: < 1262147303 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Oh well < 1262147310 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's for SCIENCE < 1262147313 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :hi Gracegoats < 1262147360 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: The book is way out of date anyway < 1262147367 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :oh hello soupdragon. wink. < 1262147376 0 :adam_d!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262147385 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric : ? < 1262147388 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Gracenotes: Get a room! < 1262147398 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :wat < 1262147404 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: get a real computer :| < 1262147405 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :xwat360 < 1262147407 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1262147416 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Gracenotes: Get your mo < 1262147419 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :iPhone isn't even turing complete!!!! < 1262147419 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :M < 1262147439 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Real men use real turing machines! < 1262147441 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :that's true. then again this laptop isn't exactly turing-complete < 1262147450 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1262147451 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :@ < 1262147456 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :turing machines < 1262147496 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262147535 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :it's basically a big lookup table < 1262147539 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: grok the example? < 1262147547 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1262147547 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :so called "computers" don't compute anything < 1262147552 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it looks just like OCaml < 1262147557 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wat < 1262147572 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's haskell but with dependent types and type metaprogramming < 1262147579 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Haskell syntax thru and through < 1262147585 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :what is? Epigram? < 1262147587 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, they're pretty similar syntactically < 1262147598 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The syntax i used in my example < 1262147598 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and I'm more used to OCaml, I think < 1262147610 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: So, "Let's start with what Haskell gets right, and go from there". < 1262147618 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ok, so the final topic is... The module system! < 1262147627 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :use the C #include system < 1262147629 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :end of story < 1262147630 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Few differences. < 1262147631 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :amirite < 1262147646 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Actual syntax will differ quite a bit < 1262147675 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :no one cares about module systems :P < 1262147679 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gracenotes: MURDER. < 1262147680 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :because they are complicated < 1262147693 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And, might be strict not lazy, both for the added safety and because iirc a general implementation of lazy FRP is unsolved problem < 1262147709 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Mine is not just for nanespaces! < 1262147710 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: A modern language without a module system is a crime. < 1262147723 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Indeed they are even more powerful than MLs < 1262147732 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Yeah like haskell < 1262147733 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ah, how did you make them interesting? < 1262147757 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: ... ? < 1262147761 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Will explain immediately after haskell modules bashing < 1262147772 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Haskell has nanespaces < 1262147772 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :We may be using words differently. Explain. < 1262147779 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And no functors! < 1262147792 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(not that kind) < 1262147801 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Ah. < 1262147801 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I consider that a somewhat simplistic module system. < 1262147813 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Shall I segue into my explanation? :P < 1262147815 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Of course, my background is C-heavy, so... Yeah. < 1262147819 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1262147849 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Will use ml haskell hybrid syntax for this explain < 1262147988 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type List = module { type T; empty :: T; add :: Integer -> T -> T; length :: T -> Integer } < 1262147996 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Erm < 1262148000 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That type there < 1262148007 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oh sod it let me retire < 1262148010 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Rewrite < 1262148011 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sec < 1262148042 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :signature { type T; empty :: T; add :: Integer -> T -> T; length :: T -> Integer } < 1262148065 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :This is a signature. Signatures -- modules as types -- values. < 1262148075 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :With me so far? < 1262148080 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Right... < 1262148083 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(ais523 pikhq) < 1262148103 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep < 1262148105 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :same as in ML < 1262148121 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Just explaining mls stuff first for pikhq < 1262148137 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Here's an implementation of that signature < 1262148200 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :module List { type T = [Integer]; add x xs = x:xs; length xs = theLanguagesLengthFunction xs } < 1262148217 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :We could say that that module :: that signature < 1262148222 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :With me? < 1262148230 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Okay... < 1262148277 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So, List.T is a type. BUT! If we, in our interface file (basically just the types of things), < 1262148304 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Put module List :: signature { that signature } < 1262148312 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then it becomes it's interface < 1262148316 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I.e < 1262148328 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: List.T is a type site < 1262148331 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sure < 1262148332 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But < 1262148348 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It is not useable as [Integer] < 1262148356 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It is abstractef < 1262148369 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :We can only use it from List's functions. < 1262148374 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Cool, no? < 1262148385 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yeah. < 1262148394 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :[1] :: List.T simply doesn't work < 1262148410 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Because the implementation of T is not exposed < 1262148413 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Now < 1262148432 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's conceivable that two modules might have the same signature < 1262148437 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :E.g. < 1262148450 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :An implementation using a vector < 1262148456 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yah? < 1262148462 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yeah. < 1262148495 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So we have functors. A functor is basically a module that takes other modules as arguments < 1262148498 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Observe < 1262148546 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :functor Silly (List :: signature { long signature is long }) = module { < 1262148566 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric : foo = List.add 1 List.empty < 1262148589 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric : main = print (List.length (List.add 2 foo)) < 1262148592 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :} < 1262148597 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :We could then do < 1262148613 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :open (Silly VectorList) < 1262148626 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(open is basically import) < 1262148637 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(extracts everything into the current module) < 1262148663 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Huh. < 1262148666 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: So we have implementation agnostic modules < 1262148670 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sweet, huh? < 1262148675 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yeah. < 1262148681 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :AND < 1262148721 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Combined with my type level metaprogramming (did you understand the photo?) < 1262148825 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :oh.. what the hell. http://www.xs4all.nl/~weegen/eelis/analogliterals.xhtml < 1262148830 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: ais523 (here is where it departs from ml) < 1262148838 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :I feel like breaking down into tears < 1262148843 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Gracenotes: one of Eelis' finest creations < 1262148876 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hahaha < 1262148904 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :I am feeling the joy of human creation simultaneously tinged with desperate sorrow < 1262148920 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :reminds me of Acme::Don't in Perl < 1262148925 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :which was a similarly silly syntax trick < 1262148936 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: That photo... < 1262148955 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Spiffy. < 1262148958 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :http://imgur.com/n5amE.jpg < 1262148966 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Seen it? < 1262148967 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :ais523: not sure it's on the same scale < 1262148981 0 :Gracenotes!unknown@unknown.invalid PRIVMSG #esoteric :you know, ehirdiphone, many of us do use pastebins < 1262148981 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Grok it? < 1262148986 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Gracenotes: Iphone < 1262148998 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gracenotes: maybe not, but apostrophes in keyword names are still epic < 1262149062 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: < 1262149089 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: Yes. < 1262149093 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Don't is a syntax trick? < 1262149097 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ok pen time < 1262149098 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I just commented on it, in fact. < 1262149104 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ok :p < 1262149109 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sec < 1262149197 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Too long to write I'll just explain < 1262149208 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :coppro: yes < 1262149222 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's equivalent to Don::t using an outdated syntax < 1262149231 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1262149233 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Who says functor arguments have to be modules? why not types? < 1262149236 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh right, now I remember < 1262149238 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :FOR INSTANCE < 1262149270 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :functor Input (t :: RecordType) < 1262149275 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :results in a < 1262149293 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :signature { input :: IO t } < 1262149307 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :By using Fields as seen in my photo < 1262149317 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It lets you do this: < 1262149318 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I only have one complaint < 1262149329 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Specifying the type independently from the value seems blah < 1262149336 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :if they are effectively identical < 1262149345 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :data Foo { a :: Integer, b :: String, c :: Bool } < 1262149359 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :open (Input Foo) < 1262149367 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :main = input < 1262149369 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Result? < 1262149377 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :$ ./foo < 1262149386 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :a= 2 < 1262149391 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :b= foo < 1262149395 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :c= abc < 1262149408 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Invalid input. < 1262149415 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :c= true < 1262149425 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And that results in < 1262149431 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it's 4 am, you're hard to folllow < 1262149436 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Foo {a=2,...etc < 1262149447 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: ais523 get it? < 1262149449 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :That's... Pretty spiffy. < 1262149467 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I think I get it, and it's neat < 1262149470 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but I'm not sure < 1262149501 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The uber cool thing is how all this has no runtime penalty < 1262149509 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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". < 1262149515 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Haskell fu helps < 1262149532 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: Actually, as much as you're going to hate me for saying this, C++ helps too < 1262149533 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: pretty much < 1262149539 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Btw, what do you mean by < 1262149543 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: Good God most of that is easily done at compile-time, isn't it? < 1262149554 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :copproSpecifying the type independently from the value seems blah < 1262149558 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Yep. < 1262149582 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: One of your earlier examples, if I read correctly, had you specifying the type and the value of the function redundantly < 1262149597 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :if I misread, my problem, not yours < 1262149598 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Redundantly? < 1262149602 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Like how? < 1262149624 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Do you mean the < 1262149627 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :signature < 1262149634 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric : List < 1262149634 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[20:54:48] type Vararg 0 = (); Vararg n = () -> Vararg (n-1) < 1262149636 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Thing? < 1262149636 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[20:55:00] vararg 0 :: () < 1262149638 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[20:55:10] vararg 1 :: () -> () < 1262149639 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[20:55:42] Implementation if vararg itself: < 1262149641 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[20:55:52] vararg 0 = () < 1262149643 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[20:56:10] vararg n () = vararg (n-1) < 1262149660 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Ah. That is only because the example is trivial < 1262149673 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ah, ok < 1262149678 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :In my soon after printf example you could easily see the difference < 1262149682 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right < 1262149710 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262149719 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :hmm... I'm going to go buy some food < 1262149727 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or just let the compiler infer the type! (yeah right, even haskell can't infer the type in all cases) < 1262149752 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(literally impossible for my Lang due to TC type system) < 1262149752 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: yeah, they've added it for lambda functions but not for regular ones < 1262149754 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1262149758 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :??? < 1262149766 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Type inference is kinda impossible to do in the general case... < 1262149767 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I think you are confused < 1262149772 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: no < 1262149773 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And even more so for TC types. < 1262149785 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Haskell sans typeclasses is inferrable totally < 1262149796 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: You are confused < 1262149808 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Haskell sans typeclasses is perhaps even *trivially* inferrable. < 1262149826 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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; } < 1262149830 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :see the redundancy? < 1262149839 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :(at least it's better than the current mess *shudder*) < 1262149840 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You didn't say c++ < 1262149847 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I did < 1262149847 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :ehird, GADTs? < 1262149855 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[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 < 1262149862 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: What about them? < 1262149863 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :not sure if Tom solved it or not < 1262149871 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oh < 1262149874 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :type inference for functions that work on GADTs < 1262149876 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Haskell inferrence < 1262149900 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: lambda functions are allowed to infer types on bodies of "{ return foo;}", but IIRC this hasn't been added for normal functions < 1262149915 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wait < 1262149930 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262149933 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Didn't see that < 1262149936 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Xarify < 1262149938 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Clarify < 1262149962 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: I just gave an example; "t+u" is redundant < 1262149972 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ah < 1262149986 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Don't get it but whatever < 1262149992 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :compare to a lambda (no polymorphic lambdas atm): "[](int t, int u) { return t+u; } // inferred return type int" < 1262150001 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :the -> foo is the return type < 1262150011 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphoneIn my soon after printf example you could easily see the difference < 1262150014 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Erm < 1262150022 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it appears after the parameter declaration so the parameters are visible < 1262150031 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: When you pinger me snout the I ferrencr only being for lambda < 1262150052 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :okay, I think I'm assuming too much about your knowledge of C++ < 1262150057 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Read the lines I said before with out your c plus plus stuff < 1262150068 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I didn't realise you'd said them < 1262150080 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I was just continuing what I said with a quip < 1262150089 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262150095 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Anyway < 1262150099 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :how about we restart altogether? < 1262150106 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Doesn't matter < 1262150127 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :basically: Make sure that in trivial cases, it's possible to specify a function without specifying the type in a redundant manner < 1262150130 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'm aiming to have no gc w my Lang! If it's possible < 1262150138 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Region inferrence instead :D < 1262150143 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :gc w? garbage collection with? < 1262150144 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Would be uber cool < 1262150148 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Yes < 1262150166 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :interesting < 1262150187 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I've always been interested in the notion of graph-based collection < 1262150210 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It'd, among other things, let small integers use a full word < 1262150211 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :specifically with the goal in mind that an object is destroyed as soon as its references become invalid < 1262150224 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No need for a tag so the gc knows what's a pointer < 1262150241 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And probably speed things up < 1262150250 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :anyway, I'm actually leaving to get food now; if you have anything important to say, ping me or comment when I get back < 1262150262 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Probably wouldn't catch all things though < 1262150264 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: If you can do it, then it would be quite nice. < 1262150265 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Dunno < 1262150295 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: A cool thing arising from all this sweet language nectar: < 1262150330 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You can malloc some memory, access it at will, realloc it, etc, with no runtime penalty, SAFELY. < 1262150369 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :malloc :: (n::Int) -> MemBlock n < 1262150395 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(Ok, IO (Maybe (MemBlock n))) < 1262150415 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Heheh. < 1262150458 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: the kicker? < 1262150466 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Even ptr arithmetic < 1262150521 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ptradd :: (n::Int) -> MemBlock m -> MemBlock {n-m} < 1262150527 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or similar < 1262150532 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ignoring negatives < 1262150569 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*m-n < 1262150602 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1262150621 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :access :: (n::Int) -> MemBlock m -> {n < m} -> Int < 1262150642 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :called as (access n block) if no proof is required < 1262150658 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :woo dependent types < 1262150668 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*-> IO Int < 1262150677 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :So, you could use this language much like C. ... Except you're not going to shoot a foot with it. < 1262150736 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262150749 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(which is web apps, oddly enough) < 1262150768 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Dependent types = can make more compile time assumptions < 1262150787 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And if you did some wizardy GHC style optimisation too? < 1262150790 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Dude. Fast. < 1262150802 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1262150838 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: Because of the annotations given to the compiler, optimization would be (relatively) easy. < 1262150862 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Hey, if I had no gc and small ints took up the word arithmetic would be 1 instructiob < 1262150864 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :N < 1262150866 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Much less "checking to be sure this is safe", more with the "just transform it to the equivalent". < 1262150877 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not like 10 and a branch < 1262150881 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :As with tagged ints < 1262150884 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Well < 1262150887 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No branch < 1262150892 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Since stariv < 1262150895 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sratic < 1262150897 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Static < 1262150899 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But still < 1262150908 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :1 vs 6 or so < 1262150917 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Nice speed up for number chrubchibg < 1262150925 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Crunching < 1262150954 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: why thr dmilry? < 1262150956 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The < 1262150959 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Smiley < 1262150960 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sj < 1262150962 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :because = < 1262150970 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Shiws as sad in colloquy < 1262150996 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Iphone bitch. Be glad im not using text speak < 1262151041 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :A compiler that does all the things I want will prolly be like 20,000 lines of haskell or more :-( < 1262151065 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Maybe even 50,000—70,000 depending on compiler smartness < 1262151095 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :100,000 if I want readable error messages :P < 1262151209 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :damn this language is sweet :| < 1262151272 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I don't even want to write the compiler in another language. Too many opportunities for sweet uses of the lang's features < 1262151298 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :If you absolutely must write it in a different language, must be Haskell. < 1262151315 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or one of the MLs < 1262151316 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It just makes language implementation... Feel right. < 1262151326 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :They were designed for it after all :P < 1262151334 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Fair point. < 1262151405 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(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) < 1262151416 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Haskell is compelling too though < 1262151479 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It occurs to me that a worthy Emacs mode would be a mode to end all modes < 1262151505 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Probably the largest piece of elisp ever. :P *shudder* < 1262151554 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Agda has a really advanced emacs mode < 1262151567 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :will it allow impureness? < 1262151665 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Monads. < 1262151689 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I mean, as well < 1262151691 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :if it's being strict < 1262151884 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: No. < 1262151917 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Well, maybe if you have "pragma unsafe" in your module and import Internals. < 1262151934 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then you have Internals.coerce :: a -> b < 1262151936 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :back < 1262151951 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But every module using yours must be pragma unsafe too < 1262151959 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So that's pointless, mostly < 1262151975 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: I said interesting things right after you left < 1262151999 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :do I have to repeat them or do you have sufficient scrollback? < 1262152014 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I have scrollback < 1262152038 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coerce would actually be: < 1262152058 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: Yeah, if you have well-defined evaluation order, "pragma unsafe" is perfectly reasonable. < 1262152073 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(a::Type) -> (b::Type) -> a -> b < 1262152091 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But you use that as (coerce x) < 1262152112 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's just how you do forall in dependently typed langs < 1262152128 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'll probably have shorthand for that < 1262152162 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Uh oh, iPhone problem, brb < 1262152200 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Fixed < 1262152201 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ping < 1262152218 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Pong < 1262152224 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Paddle < 1262152229 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yay < 1262152271 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So! I hope you all now worship my language and know it will subsume and supersume every other language forever. < 1262152275 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: very interesting < 1262152290 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: not until it has a really good impl < 1262152293 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or, more seriously, I hope you all now think my language is pretty cool. < 1262152322 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: That would be my goal. :P < 1262152324 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: does it compile easily into all TC esolangs? < 1262152337 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :or does it not want to tread on Underlambda's design space? < 1262152338 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Which part is very interesting? < 1262152345 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All of it? :P < 1262152348 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: region inference < 1262152350 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :REMOVE ALL OTHER LANGUAGES. THEY ARE INSUFFICIENTLY COOL. < 1262152369 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: No, but you can have a compile time BF compiler. < 1262152373 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :With syntax. < 1262152384 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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? < 1262152393 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :BF[ ,[.,] ] :: IO () < 1262152418 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Not just functions. It is simply: types can take values as arguments < 1262152444 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Full explanation is way back in the scrollback < 1262152454 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262152459 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION loads logs
< 1262152478 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Careful. It's been an hours-long explanation. < 1262152524 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Btw I haven't thought of a syntax at all yet. < 1262152535 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Just been blending haskell and ml for this talk < 1262152546 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: so, basically, template vs. template? < 1262152582 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :(except applicable to all types, not just a very small subset of those available) < 1262152594 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: No! < 1262152600 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh :( < 1262152605 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Because there, < 1262152614 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The value must be known at compile time < 1262152622 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not so with dependent types < 1262152635 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And yet, no runtime penalty < 1262152636 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ah, ok < 1262152644 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :wait, how? < 1262152651 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Basically < 1262152657 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If you say < 1262152663 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Read an int from stdin < 1262152686 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And pass it to a function expecting an even number < 1262152687 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :you can erase all types into a NULL value, and then eval the real values like an untyped language < 1262152694 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You must satisfy the compiler < 1262152698 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That it is even < 1262152710 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Perhaps it can infer it if you do a branch < 1262152717 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Failing that, DIY < 1262152727 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :(because you can't do case analysis on types) < 1262152731 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(pass the proof argument yourself) < 1262152741 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :so... attempting another gross oversimplification here... encoding the range of values into the type? < 1262152748 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1262152761 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :more like set of values, only it's allowed to be infinite < 1262152775 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: They are real values < 1262152775 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and you can have loads of types which are similar except in the value sets, automatically generated < 1262152779 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Flesh and blood < 1262152798 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You just have to manually satisfy them if the compiler can't < 1262152815 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :The type of an object might be "even integer", whereas another object might be of the type "prime integer"; true or false < 1262152817 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If we need an even number, pass a proof that it's even < 1262152828 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then the value doesn't matter to the type < 1262152837 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Voilà, dependency goes poof < 1262152852 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok, now I'm really confused < 1262152871 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: it's magic. < 1262152892 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Don't worry, it's pretty intuitive in practice < 1262152901 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :There's a certain ACC quote which has never appeared more applicable to the situation < 1262152910 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Feels like you're doing the impossible though < 1262152923 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Precisely < 1262152935 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Like, I understand the notion < 1262153014 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :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, < 1262153024 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You have to prove it. < 1262153027 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262153042 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(which is just... Writing the code that shows it, basically) < 1262153060 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But really, it's pretty simple. < 1262153073 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Just doesn't sound it. < 1262153081 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :like, I get the net effect < 1262153120 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Even I don't know the actual inferrence algorithms. I'm going to defer breaking my head that much until I absolutely must < 1262153121 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it's statically-enforced value control < 1262153152 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: But also value liberator, remember the printf? < 1262153178 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :"value liberator"? < 1262153220 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Lets you express stuff you can't otherwise < 1262153224 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Like printf < 1262153227 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh, right < 1262153250 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Now, I admit I don't program in functional languages as much as I'd like, so bear with me here < 1262153283 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :this looks to me a lot like pattern-matching being done at compile time, with an error if nothing matches < 1262153315 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Can you elaborate? My mind is rejecting that metaphor. < 1262153337 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :My pattern matching experience is with Erlang, it may be different elsewhere < 1262153379 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Nope < 1262153483 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :in Erlang, you could do something like printf ([%%, %d, RestOfString], [SomeInteger, RestOfArgs]) -> printAsInteger(SomeInteger), printf(RestOfString, RestOfArgs). < 1262153494 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oh < 1262153510 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The type was pattern matching on the string < 1262153517 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But all functions have that < 1262153543 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It was just a type with the kind (type's type) String -> Type < 1262153548 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right < 1262153555 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but now, let's take a scanf example < 1262153576 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :in that case, you are pattern matching on the string and affecting the return type of the function < 1262153602 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Printf does that too < 1262153608 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The string affects the type < 1262153647 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but scanf is a more interesting example < 1262153648 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But continue < 1262153661 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but so basically your idea is to be able to check this at compile time < 1262153680 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :and complain if there's any chance there might be an error < 1262153694 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :rather than simply waiting around and hoping things come out right < 1262153724 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262153736 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262153736 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :His plan is to have the type of printf be dependent upon the string given as its first argument. < 1262153739 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Colloquy borked < 1262153741 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :His plan is to have the type of printf be dependent upon the string given as its first argument. < 1262153747 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(repeated for sake of ehird) < 1262153751 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I do not understand your analogy < 1262153756 0 :Sgeo_!n=Sgeo@ool-18bf618a.dyn.optonline.net JOIN :#esoteric < 1262153759 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Saw it first time < 1262153763 0 :Sgeo_!unknown@unknown.invalid QUIT :Read error: 104 (Connection reset by peer) < 1262153769 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: ... After you left? < 1262153777 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :You've got some crazy log-reading skills. < 1262153778 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1262153800 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it appeared to me to occur right after he arrived < 1262153807 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :he may have caught it < 1262153809 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Darned latency. < 1262153817 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yay IRC < 1262153849 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :copprorather than simply waiting around and hoping things come out right < 1262153855 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then what pikhq said < 1262153858 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: well... basically, suppose I do printf(some_user_string, 3) < 1262153859 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That he repeated < 1262153865 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Miss anything? < 1262153873 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Wait < 1262153880 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :waiting < 1262153897 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That would simply give a type inferrence error < 1262153912 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I think this would work: < 1262153936 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :if s == "%d" then printf s 3 else return () < 1262153940 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right < 1262153945 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Failing that... < 1262153950 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's proof time < 1262153967 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :M < 1262153983 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not sure where the proof would go for printf actually < 1262153984 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I think we're wasting our time < 1262153991 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Hm? < 1262153992 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yeah, printf would be a nasty proof < 1262154002 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No need to prove printf. < 1262154024 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Just prove that (printf s) :: Integer -> IO () < 1262154027 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :well, now I know we agree about the basics < 1262154027 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ie < 1262154039 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That s is only constant output < 1262154048 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :and one formatting directive < 1262154061 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That takes an Integer < 1262154066 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :agreed < 1262154072 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But honestly? < 1262154088 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Don't pass a user string to printf, you dumb fuck. ;) < 1262154105 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sadly, that's when printf becomes most useful < 1262154116 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :localization, specifically < 1262154129 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's not a user strung < 1262154133 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :String < 1262154142 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :It may be loaded from a file < 1262154145 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Compile those in, yo. < 1262154155 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Parse the files at compile-time. < 1262154157 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :for 30 different languages? no thanks < 1262154172 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Compile only the ones you need. < 1262154173 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :anyway, we're getting sidetracked < 1262154179 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Anyway < 1262154186 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Alternatively < 1262154210 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Make a module signature Translation < 1262154213 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :With eg < 1262154229 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :big_error :: Integer -> String < 1262154234 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Implementation? < 1262154249 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :we're getting sidetracked < 1262154257 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :my basic question is how this relates to the notion of types < 1262154258 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :big_error = printf "OLE OLE SUPER ERROR %d" < 1262154276 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :using one of your examples, suppose I have a function that takes an integer that must be even < 1262154279 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You could use syntactic extension to make that nicer for the translators < 1262154284 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ok back on track < 1262154292 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: No < 1262154298 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wrong terminology < 1262154303 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262154309 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :correct terminology? < 1262154315 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You don't take Integer-that-is-even < 1262154322 0 :cal153!unknown@unknown.invalid QUIT : < 1262154331 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You take Integer and that-Integer-is-even < 1262154343 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :With the latter hopefully being inferred by the compiler < 1262154350 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262154365 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :this makes it feel even more Erlangish to me < 1262154368 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but w/e < 1262154368 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's like having a type < 1262154377 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Even (int) < 1262154387 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Even 2 has one value < 1262154390 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :call it poop < 1262154400 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :poop :: Even 2 < 1262154403 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :but < 1262154412 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Erlang: my_function (I) where is_int(I) and I mod 2 == 0 -> whatever < 1262154413 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Even 1 has NO values! < 1262154423 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(nothing) :: Even 1 < 1262154434 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So the compiler passes "poop" in < 1262154440 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If the number is even < 1262154444 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It won't type < 1262154448 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Erm < 1262154450 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Will < 1262154453 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Get it? < 1262154496 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1262154510 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: So < 1262154520 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If we don't know the value of n < 1262154521 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The co < 1262154524 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Mpiler < 1262154527 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262154528 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :? < 1262154533 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Cannot tell if (poop :: Even n) < 1262154537 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Is well typed < 1262154547 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And that's where proofs come in < 1262154569 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok... so what is a "proof"? < 1262154575 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: The type of the poop argument is dependent on the value of the number argument < 1262154587 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: but the poop argument doesn't really exist < 1262154595 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yes it does. < 1262154600 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :wait, what? < 1262154601 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Let me show you. < 1262154605 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262154616 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :btw, can you just type in a pastebin rather than a picture? < 1262154624 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :iPhone actually < 1262154627 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Just one line < 1262154672 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :evenClub :: (n::Integer) -> {Even n} -> AwesomeParty < 1262154681 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :{} is agdas notAtion for < 1262154690 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :also, btw, ZREO finished OoT finally; it's awesome < 1262154691 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"infer vAlue if possible" < 1262154693 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :SO < 1262154697 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Don't talk btw < 1262154704 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :o hai < 1262154717 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :not talking about anything relevant < 1262154719 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :When we do (evenClub 2) < 1262154725 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The compiler does < 1262154735 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :evenClub 2 {poop} < 1262154744 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ah, ok < 1262154748 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I get it now! < 1262154751 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Since the third param must be of type Even 2 < 1262154759 0 :Sgeo!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262154761 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It checks that it is... Voilà! < 1262154771 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :voila! < 1262154776 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Obviously, the poop param is erased during compilation < 1262154784 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :As it is useless at runtime < 1262154793 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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 :) < 1262154808 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not thought of < 1262154815 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :This is how it actually works < 1262154817 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I know < 1262154819 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(in agda) < 1262154857 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The issue is that you need to make a type Even which is a drag BUT < 1262154883 0 :jpc!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262154889 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type IsTrue True = PoopHaven; IsTrue False = NoValuesForYou < 1262154898 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :+ syntactic sugar < 1262154903 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric := tada? < 1262154918 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That'd be < 1262154932 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :{IsTrue (even n)} < 1262154938 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or something < 1262154980 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: So, hopefully you at least grok it as well as I do now. < 1262155001 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: I now understand. < 1262155014 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The whole language pretty much clicked into place combining seeing Ur with my past musings < 1262155024 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So I haven't fully sorted it out yet < 1262155028 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I question whether it would be more effective to attempt to accomplish the goal through a different mechanism < 1262155055 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Explaining it is the single most difficult part < 1262155072 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :specifically, of encoding a known subset of values into the type of an object < 1262155091 0 :calamari!unknown@unknown.invalid PART #esoteric :? < 1262155097 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Using it? Pretty easy. And a dependently typed lambda calculus is just a few lines of code onto a normal typed one < 1262155105 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Explain < 1262155133 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If you mean what I think Iean that cannot accomplish remotely as much sscdependent types < 1262155143 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I think they're equivalent < 1262155164 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :(note, this is in the "this is a theory" form of "I think", not the "I'm pretty sure I'm right" form) < 1262155174 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: maybe dependent types are the key to feather :P < 1262155184 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Can you still explain? < 1262155187 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: I'll try < 1262155255 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262155264 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: #agda is full of people who will know more than I btw if I don't grok it < 1262155266 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Also < 1262155271 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Irrelevant < 1262155273 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Say you < 1262155277 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: just wait < 1262155278 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Remove the {}s < 1262155281 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then < 1262155290 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You'd just have to append " poop" < 1262155294 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :To your calls < 1262155301 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's just sugar < 1262155305 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right, I get that < 1262155312 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but what if it wasn't < 1262155320 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I'm not trying to debate the way Agda does < 1262155327 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I'm trying to find another approach to the same solution < 1262155329 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then that would break if you remove the {}s < 1262155334 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :agreed < 1262155337 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :They are not mandatory < 1262155346 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So it is not equivalent < 1262155360 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Remember dependent types are more than just yes no < 1262155362 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :my idea is that { Even n } is not seen as an extra parameter, but rather a constraint < 1262155365 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Remember printf? < 1262155372 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok, restate printf for me < 1262155382 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Logs. iPhone. < 1262155388 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right < 1262155390 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262155396 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Grep "type Printf" back up a line or two. < 1262155407 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ugh, different syntax < 1262155440 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok, I think I get your point < 1262155450 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: how much do you know about C++ templates? < 1262155506 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not different syntax < 1262155510 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Syntax is the sane < 1262155513 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Same < 1262155524 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: A fair amount. < 1262155532 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Almost did SKI once vm < 1262155538 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*once. M < 1262155544 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*once. < 1262155553 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :SKI? < 1262155560 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: do you know what enable_if is? < 1262155591 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1262155595 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ski conbinatirs < 1262155600 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Conbinatirs < 1262155608 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Com bi nat IRS < 1262155610 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :IRS < 1262155613 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oes < 1262155613 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262155616 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ors < 1262155617 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ors < 1262155617 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I get it < 1262155622 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Google it :p < 1262155690 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262155712 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :this is in many ways similar to the use of a predicate in { Even n } < 1262155749 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Only works for compile time constants < 1262155758 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :true, but the principle is the same < 1262155761 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You can't just handwave that away < 1262155775 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I can if I consider only templates and not the C++ runtime < 1262155777 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The whole model I said is to make that work < 1262155782 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :they are TC < 1262155785 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: No < 1262155788 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Because < 1262155796 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's like a run time type system < 1262155804 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It can simply pass the actual value < 1262155809 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Which we can't. < 1262155820 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :well, allow me to continue < 1262155857 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION tries to remember where he's going wit hthis
< 1262155862 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ah right. < 1262155883 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :in the case of enable_if, you can implement arbitrary conditionals assuming appropriate predicates exist < 1262155898 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And? < 1262155898 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but there is another way of accomplishing the same task, and that is with restrictions on the arguments < 1262155921 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :there was a proposed feature for C++0x called concepts that would do exactly this; it would provide the ability to constrain template arguments < 1262155952 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :on one level, it's largely sugar, but the underlying notion is different < 1262155968 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Which must be compile time constant < 1262155977 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :sure, but templates exist as a compile-time system < 1262155988 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :What you're doing is taking a hard problem < 1262156001 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Explaining the solution to an easy problem < 1262156006 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I'm wondering if dependent types can be implemented in the same way, with compiler-managed contraints rather than predicates < 1262156016 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And handwaving the rest away < 1262156017 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :the whole C++ thing was an analogy; it's not perfect < 1262156019 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :etc. < 1262156056 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Bit < 1262156058 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But < 1262156065 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That is more complicated < 1262156068 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :printf < 1262156070 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :of course it is < 1262156071 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And the like < 1262156080 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Require them to be usable as values < 1262156095 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So you're just introducing a new concept < 1262156111 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :tbh, I think I need to see a bigger example of your language before I can explain this more clearly < 1262156111 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Without even any holes for propfs < 1262156115 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Proofs < 1262156127 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So... Why? < 1262156128 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :since it's hard to explain without a concrete base to work from < 1262156136 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :What is the advantage? < 1262156144 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I don't know if there's an advantage < 1262156150 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :advantage?? < 1262156165 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :if I sought an advantage in everything I did, I wouldn't be here chatting, I'd be finished my backload of homework < 1262156189 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So... Replacing an existing concept with a less simple one. And you have to keep the old one anyway. < 1262156194 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Compelling :P < 1262156199 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I don't think you'd need to keep the old one < 1262156205 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :printf < 1262156215 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not a "constraint" < 1262156228 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :that's part of my issue; I'd need to see a complete example of printf < 1262156235 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :not just "here's my signature kthxbye" < 1262156239 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :printf "%d" 3 < 1262156247 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I gave more < 1262156247 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :printf "%d %d" 3 4 < 1262156258 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I gave the relevant type < 1262156267 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The magic that makes it work < 1262156273 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :not enough, at least not me looking through scrollback < 1262156278 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(well. Just for %d) < 1262156281 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :append is a cool one < 1262156291 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's right after the printf signature you dolt < 1262156299 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1262156327 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :0 + m = m ; S n + m = S (n + m). < 1262156329 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :[] ++ ys = ys ; (x::xs) ++ ys = x::(xs ++ ys). < 1262156331 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ah, I see, I think I just misunderstood the synta < 1262156333 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :*synatx < 1262156335 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :*syntax < 1262156354 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :_+_ : N -> N -> N, _++_ : Vector A n -> Vector A m -> Vector A (n + m) < 1262156367 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :it's amazing that ++ typechecks < 1262156396 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: BUT CAN IT BLEND^WINFER < 1262156399 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1262156424 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Note that (x:xs) is cons < 1262156434 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And [] == "" < 1262156455 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :okay, hang on, I'm going to repaste this < 1262156479 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :19:58:20 printf :: (fmt :: String) -> Printf fmt < 1262156481 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :19:58:39 type Printf [] = IO () < 1262156484 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :19:59:33 type Printf ('%':'d':xs) = Integer -> Printf xs < 1262156485 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :20:00:05 type Printf (x:xs) = Printf xs < 1262156487 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Is that it? < 1262156492 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ya < 1262156496 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262156506 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :so where does the type replacement come in to play here? < 1262156519 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Type replacement? < 1262156529 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :err, the whatever < 1262156531 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :the funny magic < 1262156536 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :What? < 1262156543 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :wait... < 1262156550 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION facepalms
< 1262156559 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok, so I'm stupid < 1262156569 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but nvm that < 1262156573 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :What did you do? :P < 1262156590 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I misunderstood the way functions work < 1262156599 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Howso? < 1262156615 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :specifically, "a b" is a left-associative operator that executes a on b < 1262156625 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :oh right < 1262156635 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :for multi-arg functions, there's syntactic sugar in the declaration that creates a forwarding function with less arguments < 1262156636 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :you mean like f x y as f(x,y) < 1262156640 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :no < 1262156643 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Ahh yep < 1262156644 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :yes you do < 1262156650 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :f x y as f'(x)(y) < 1262156650 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric ::D:D:D:D:D:D:D < 1262156654 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :f' ? < 1262156670 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Ya welcome to currying < 1262156688 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :as I said, my functional programming experience is sadly lacking :( < 1262156699 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No worries < 1262156706 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :anyway, this helps clear up a lot, though all it ends up doing is making my idea a lot harder to express < 1262156714 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :How did it change your understanding? < 1262156724 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Don't see currying in printf < 1262156733 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :absolutely there's currying there < 1262156738 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :I don't see what currying has to do with any of it < 1262156739 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Where < 1262156746 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :just think of < 1262156752 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :f x y as f(x,y) < 1262156756 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All the doohickeys have 1 arg < 1262156766 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oh < 1262156768 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :OH < 1262156771 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :YEAH < 1262156784 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :In type Primtf's right Gand side < 1262156787 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Hand < 1262156792 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yeah, it returns a function < 1262156801 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Nope < 1262156805 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :wait, no? < 1262156805 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Returns a type < 1262156816 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: For < 1262156817 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :well, a function type < 1262156825 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :A format string fmt < 1262156827 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :printf "%d" gives me an Integer -> IO, correct? < 1262156833 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :no < 1262156834 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :IO () < 1262156841 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Yes. < 1262156845 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :Printf "%d" = Integer -> IO < 1262156852 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right < 1262156854 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :IO () < 1262156856 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: A < 1262156858 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :As in < 1262156867 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh wait, that was soupdragon < 1262156867 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :A value if that type < 1262156877 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok, nvm. Your nicks have a too-similar length < 1262156879 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro made no error < 1262156891 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :printf "%d" : Integer -> IO < 1262156894 0 :ehirdiphone!unknown@unknown.invalid NICK :pooop < 1262156899 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1262156903 0 :pooop!unknown@unknown.invalid PRIVMSG #esoteric :You're welcome < 1262156942 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262156955 0 :pooop!unknown@unknown.invalid PRIVMSG #esoteric :coppro: By nickname laws I think you have to have sex with me now. If I was poop I'd need copro < 1262156961 0 :pooop!unknown@unknown.invalid PRIVMSG #esoteric :But pooop is coppro < 1262156966 0 :pooop!unknown@unknown.invalid PRIVMSG #esoteric :QED < 1262156966 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh dear < 1262156972 0 :coppro!unknown@unknown.invalid NICK :Cu < 1262156994 0 :pooop!unknown@unknown.invalid PRIVMSG #esoteric :Cu: EVADING THE LAW?? < 1262157008 0 :pooop!unknown@unknown.invalid QUIT :Remote closed the connection < 1262157023 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262157025 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1262157046 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Repeat the line you said before the poop shit (which was crap) < 1262157053 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262157059 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION grimaces
< 1262157086 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :is there any name for the use of {} in functions? < 1262157092 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :that I can use to conveniently refer to it? < 1262157103 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Agda probably has one. Lets call it zooping < 1262157114 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It bears some resemblence to the nomic use. < 1262157119 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(but only some£ < 1262157123 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262157132 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :) < 1262157134 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wait < 1262157160 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Zoop is the argument or the action of Ingerring a value? < 1262157163 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Which < 1262157169 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :the latter < 1262157172 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ok < 1262157178 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :so, when you zoop an argument, what you are doing is providing an imaginary argument that the compiler magically inserts based on some value < 1262157191 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Real argument. < 1262157199 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :imaginary in the sense that the user never sees it < 1262157201 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :As real as any argument. < 1262157209 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :otherwise, 100% real < 1262157216 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It exists. If you want to you can use it in the function < 1262157227 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But no < 1262157238 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not based on some value < 1262157251 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It is disconnected from dependentvtyping < 1262157273 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I mean it handles it < 1262157294 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But {} does not require the type to be dependent. < 1262157301 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :wait, let's step back, I just realized there's something I don't get < 1262157308 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Although it's not much use otherwise < 1262157313 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :Even n is a family of types, one for each integer, all sharing the same values? < 1262157327 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Almost right. < 1262157346 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All the even ns share the same value, poop < 1262157356 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All the odd ns have no values at all < 1262157371 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I.e you cannot have a value of type Even 1 < 1262157372 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262157405 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Cu: All the compiler does is < 1262157407 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :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? < 1262157413 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Gives it "poop" < 1262157415 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's it < 1262157420 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No magic < 1262157427 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :yessir, I get that < 1262157480 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Also, no, except for being simpler, having an obvious way to pass proofs, and being the same mechanism that things like printf use < 1262157494 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All of which make me very skeptical of your idea. < 1262157512 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :ok, so, ignore q1, that's sort of academic at this point as I'm trying to simplify it < 1262157518 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :q1? < 1262157524 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :point 1, whatever < 1262157526 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :tired < 1262157532 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Point 1? < 1262157533 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :point 2, I don't quite understand < 1262157539 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :point 1 = simpler < 1262157540 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oh < 1262157541 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I see < 1262157547 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :point 3, I'm not sure is related < 1262157553 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The way to pass proofs is < 1262157565 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :evenClub input {...} < 1262157576 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :ah, I see < 1262157583 0 :Cu!unknown@unknown.invalid PRIVMSG #esoteric :I was sort of missing that bit < 1262157585 0 :Cu!unknown@unknown.invalid NICK :coppro < 1262157591 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I.e. If there is an {} arg at this position, {} passes one In explicitly < 1262157599 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right, ok < 1262157599 0 :puzzlet!unknown@unknown.invalid NICK :puzlet < 1262157606 0 :puzzlet!n=puzzlet@61.251.165.103 JOIN :#esoteric < 1262157611 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :just a thought < 1262157622 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :if you defined Even : nat -> * as a data type < 1262157628 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :lack of information is a dangerous thing < 1262157631 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :you could maybe erase the index to get Even : * < 1262157644 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :and then you've got a data type that represents even numbers < 1262157645 0 :puzlet!unknown@unknown.invalid QUIT :"leaving" < 1262157654 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: Yes < 1262157656 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :although it's isomorphic to nat < 1262157663 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :How would you erase the index tho? < 1262157675 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Ugh, just discovered a major flaw with ZREO's "official" OoT release < 1262157675 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The issue with that is < 1262157675 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :just delete it in a text editor < 1262157680 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :I don't mean automatically < 1262157682 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :gonna have to complain < 1262157683 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No convenient {...} < 1262157699 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: How < 1262157702 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Lets say < 1262157723 0 :puzzlet!unknown@unknown.invalid QUIT :Client Quit < 1262157730 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type Even n | even n = Poopy; type Even _ = Lame < 1262157742 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :I was thinking of < 1262157742 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :data Even : nat -> * where EZ : Even Z ; ES : Even n -> Even (S (S n)) < 1262157743 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :How do you erase the arg there? < 1262157757 0 :puzzlet!n=puzzlet@61.251.165.103 JOIN :#esoteric < 1262157760 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :which you can erase to < 1262157769 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :data Even : * where EZ : Even ; ES : Even -> Even < 1262157779 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: totally boring tho < 1262157788 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :not to me < 1262157791 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :writing a boring type for every constraint < 1262157834 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Oot the zelda game? < 1262157836 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :or < 1262157839 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: yes < 1262157848 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"release"? < 1262157852 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ZREO = Zelda Reorchestrated, an awesome project to redo Zelda music in awesomeness < 1262157858 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ah. < 1262157860 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :they released the OoT soundtrack today < 1262157880 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :except half the Ocarina songs are Ocarina-only, and half are full music < 1262157890 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :one way or the other I could see, but half-and-half? < 1262157915 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :(I highly recommend downloading it, btw) < 1262157975 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262157987 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262158003 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :My language will have not only infix operators < 1262158011 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But prefix and postfix too :D < 1262158026 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Perl 6-style? < 1262158032 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :or Agda style? < 1262158041 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :My style. < 1262158050 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION doesn't hold his breath
< 1262158069 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :How do you have a style anyway < 1262158081 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's just pre and postfix ops < 1262158123 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :well, agda allows you do define things pretty much however you want < 1262158146 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Did you research Agda in the time since I mentioned it? :P < 1262158169 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: yes. This is the Internet. I'm pretty confident you do the same thing from time to time. < 1262158170 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Anyway whaddya mean < 1262158184 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Perl 6 is the only other language I could think of offhand that allows the definition of new infix, prefix, and postfix operators < 1262158184 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: All the time < 1262158192 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :A lot of others don't < 1262158228 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :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) < 1262158248 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I just have that you can name a function (infix/prefix/postfix symbols) < 1262158263 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: I thought I did the opposite xD < 1262158289 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: I mean something you don't understand AND can't readily Google < 1262158301 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :postfix ! :: Nat -> Nat < 1262158319 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: ok. The only issue is the syntactical ambiguities that can arise < 1262158327 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :if you allow all three to be overloaded on the same operator < 1262158340 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :two of the three is fine < 1262158350 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :infix + :: {n::Type} -> {Num n} -> n -> n -> n < 1262158391 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :prefix ? :: {t::Type} -> Ref t -> SomeMonad t < 1262158417 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262158417 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: I'd just use operator precedence to disambiguate < 1262158427 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Failing that, flag an error < 1262158431 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: ok < 1262158440 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I forget what method Perl 6 uses... something evil < 1262158452 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(you can define your own precedence and left right association) < 1262158455 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Like haskell < 1262158471 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphoneinfix + :: {n::Type} -> {Num n} -> n -> n -> n < 1262158479 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :notice anything interesting? < 1262158499 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :you defined your own keyword there? < 1262158505 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Lol < 1262158511 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No < 1262158517 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :what does {n::Type} mean? < 1262158520 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ignore that part < 1262158522 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :inference of n's type? < 1262158537 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: You know what (n::Int) means right? < 1262158546 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I think so < 1262158548 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Int argument, magic dependent value n < 1262158556 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :magic dependent value? < 1262158561 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I thought of it as "named n" < 1262158567 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Well yes < 1262158585 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So n is thr value if the arg < 1262158587 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :{} means infer the type, and let me refer to it as Type? < 1262158592 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Which we don't know ar that point < 1262158595 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Ni < 1262158596 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No < 1262158604 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Listen < 1262158613 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Int :: Type < 1262158616 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That is < 1262158623 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Types are of type Type < 1262158626 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's why < 1262158639 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :type Printf :: String -> Type < 1262158664 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh, ok < 1262158668 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So {t::Type} is "a type t; infer value" < 1262158677 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's how we do polymorphism! < 1262158687 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :so t becomes whatever the argument's type is? < 1262158693 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :We can use t later in the signature < 1262158696 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So < 1262158706 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :could I do {n::t::Type} ? < 1262158707 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If we pass it an argument if a certain type < 1262158713 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :This sentence is syntactically unambiguous. < 1262158721 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Obviously t has to be that type! < 1262158724 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: No < 1262158727 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1262158736 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It is another argument < 1262158761 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :infix + :: {n::Type} -> {Num n} -> n -> n -> n < 1262158768 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Notice anything else interesting? < 1262158799 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it's an infix that appears to take 3 arguments? < 1262158811 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :4 < 1262158812 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Four actually. < 1262158819 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Last n is the result < 1262158837 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: It's {Num n} < 1262158845 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's how we do typeclasses! < 1262158855 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh, yeah, I'd worked that bit out < 1262158862 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :>_< < 1262158908 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :for some reason it was particularly plain to me that {Num n} meant that the type n is some number < 1262158937 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Were you around for the module system stuff? < 1262158955 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: no, but I am familiar with the notion of metatypes, which is why I think that bit came so easily < 1262158966 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No it's a different thing < 1262158970 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wait a sex < 1262158971 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :... < 1262158974 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sec < 1262158991 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Link me to todays log please < 1262159007 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :http://tunes.org/~nef/logs/esoteric/09.12.29 < 1262159016 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yeah, I didn't think they were related < 1262159020 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So I can findvwhere it is; it really is one of the best parts of the language IMO < 1262159022 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :that didn't quite come out right < 1262159033 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :was that the bit about open Foo? < 1262159087 0 :cal153!n=cal@c-69-181-46-213.hsd1.ca.comcast.net JOIN :#esoteric < 1262159095 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But a lot mote before that < 1262159100 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wonders why he feigns stupidity in this channel
< 1262159104 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :First use of "segue" in log < 1262159115 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :See if you missed any of it < 1262159123 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :probably so that guys have a chance to show how smart and alpha they are < 1262159242 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ah, now I remember another question I had, and realized you'd answered it < 1262159247 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :s/realized/realize/ < 1262159253 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :What question? < 1262159277 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Btw there's a blip in the module talk < 1262159285 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Scroll down if you think it's over < 1262159296 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Before "c=" < 1262159317 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's not over < 1262159336 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :right, I remembered that vaguely < 1262159346 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So what was the question? < 1262159357 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :whether you would have full-on type genericism < 1262159380 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Eh? < 1262159383 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :specifically, the ability to make an entire interface dependent on another type < 1262159390 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Like howso < 1262159396 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :which, clearly you can do by generating modules from functors < 1262159402 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Like java genetics? < 1262159405 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Genetics < 1262159407 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Fff < 1262159409 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1262159421 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If so, yeah, old hat. Of course. < 1262159422 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :java's genetics consist of a whole bunch of un-evolution < 1262159433 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :huh? < 1262159436 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yeah, I just wanted to make sure you'd have a mechanism for that < 1262159451 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :(and actually, C++ templates is closer than Java generics, but w/e) < 1262159461 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yeah < 1262159579 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I have been talking about this Lang for so long. Wow. < 1262159672 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :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 :( < 1262159684 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :try me < 1262159705 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But it'd be 50000000 lines of typing. :P < 1262159712 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh ok < 1262159719 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'll snail mail you a cassette :D < 1262159765 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All this phone and I never speak into it. < 1262159826 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION tries the voice recorder
< 1262159828 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262159999 0 :clog!unknown@unknown.invalid QUIT :ended < 1262160000 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1262160450 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262160460 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: What did I miss? < 1262160475 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :nothing < 1262160484 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I did have one thing to say to you, but I forgot < 1262160519 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: I recorded a ~four minute explanation of the thing but it'd be in multiple parts < 1262160535 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Can you handle my unbroken voice????????//:: < 1262160540 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION is not sure
< 1262160564 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's not squeaky! Just... Hovering. < 1262160596 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :as opposed to hemming-and-hawing? < 1262160600 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Lawlz < 1262160605 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'll just send it < 1262160609 0 :ehirdiphone!unknown@unknown.invalid QUIT :Client Quit < 1262160791 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262160802 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Sending them by email now < 1262160812 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262160823 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wait for all three parts to arrive then set them up in a playlist or sth < 1262160830 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Just software foibles < 1262160834 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :sth? < 1262160840 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Would prefer it were continuous < 1262160844 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262160848 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: Somethubg < 1262160851 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Thing < 1262160854 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :=sth < 1262160856 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1262160867 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :.m4a sorry. iPhones fault < 1262160896 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yuk < 1262160966 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Any arrived yet? < 1262160988 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :negative < 1262161023 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :My speaking skills are improving, not many ums or pauses in that < 1262161034 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or mistakes :P < 1262161099 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :coppro: in spam maybe? < 1262161128 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :unless you're trying to sell me replica rolexes, no < 1262161140 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :*rep1ica ro1exes < 1262161249 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :This is coppro @ gmail com right < 1262161257 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :no < 1262161259 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :rideau3@gmail.com < 1262161266 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :thanks for spamming some random guy < 1262161270 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1262161277 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262161292 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :l o l < 1262161320 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ais523: go to messages, hit propose or accept trade, fill in the form < 1262161371 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :thanks, got it, and that's a /really/ weird channel-bounce < 1262161375 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cross-server, even cross-protocol < 1262161386 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1262161398 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :too lazy to type /msg ais523 on a chat without tab-complete < 1262161420 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262161428 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :remaile (har har funny pun) < 1262161435 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*remailed < 1262161460 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :coppro: heh, I was just thinking that myself < 1262161487 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Propose or accept what what < 1262161492 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :HAHAHA < 1262161494 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :http://www.wolframalpha.com/input/?i=tea%2C+earl+gray%2C+hot < 1262161518 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: I was giving him advice for KoL < 1262161545 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :KoL is kinda rubbish IMO :| < 1262161550 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :agreed < 1262161557 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :watsa kol < 1262161561 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :that's sorta the point < 1262161579 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"Its meant to be shit don't you SEE" < 1262161584 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :augur: a rather low-tech MMO < 1262161596 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :oh ok < 1262161602 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Web based < 1262161610 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's really just clicking yes a lot < 1262161615 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or going somewhere < 1262161626 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then clicking fight a lot < 1262161638 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :mostly I play it for the fun in /games, to be honest < 1262161640 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's a moderate amount of strategy + a lot of boredom < 1262161645 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :(though it probably won't appeal to most everyone here) < 1262161672 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but it's a nice distraction < 1262161923 0 :coppro!unknown@unknown.invalid QUIT :Remote closed the connection < 1262161971 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262161998 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :so this fair, collectivist cooperative is considered to be evil by ais523 :) < 1262162002 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: it's not quite hate, it's more untrust < 1262162005 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Did that get cut off? < 1262162010 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, it didn't < 1262162018 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ended at "member is recruited" < 1262162024 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1262162041 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262162047 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :doesn't mean it's unwelcome or bad, just untrustworthy < 1262162047 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: So do you not distrust if nobody makes a profit? < 1262162061 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And they don't make a profit per se < 1262162069 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :EVERYONE pays less < 1262162074 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's altruistic < 1262162087 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes... but suppose you have two identical cooperatives < 1262162091 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :except that you're in one of them < 1262162103 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the question here, I suppose, is why should I join the one with you in rather than the other one? < 1262162111 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :now, suppose the other one has one more member but is otherwise identical < 1262162162 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So you distrust profitless, collectivist cooperatives. < 1262162177 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no < 1262162184 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Favouring instead recommendations that involve a business making a handy profit. < 1262162191 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I distrust recruitment drives that would drive me towards one of them rather than a different one of them < 1262162194 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Intriguing. < 1262162215 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: But that's how they WORK! evryone pays an equal amount < 1262162219 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Cost/members < 1262162222 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It < 1262162227 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: I don't hate the collective itself < 1262162230 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :'s the whole point < 1262162237 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I just mistrust /recommendations of which collective to join/ < 1262162244 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :from a member of the collective itself < 1262162256 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Thing is < 1262162256 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I might still favour the entire concept over a for-profit company < 1262162307 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If soneone thought another service was superior they wouldn't reccommend theirs just for profit. They'd SWITCH to that alternative THRN reccommend them < 1262162321 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Doing otherwise is ridiculously nonsensical < 1262162329 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*THEB < 1262162336 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*THEN < 1262162455 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :silence! < 1262162505 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :btw they're cooperatives not collectives < 1262162523 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wonder if anyone's registered http://chicken.coop yet :D < 1262162534 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Negative < 1262162716 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Do you want my lovely voice explanations of frp, coppro iz ded :< < 1262162735 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: frp? < 1262162746 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :THEY EXPLAIN IT WITH THE GRACE OF AN OSTRICH < 1262162755 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: oh, that's a good argument, about switching < 1262162757 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Should I take that as a yes? :P < 1262162772 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :for something that's really switchable, I'll consider that to rebut my points < 1262162785 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, no, that's me asking you to explain frp before I decide whether I should ask you to explain it or not < 1262162788 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Like hosting :p < 1262162794 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: _|_ < 1262162801 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's not a middle finger < 1262162813 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's an upside-down T? < 1262162820 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's bottom, your friendly nonterminating value! < 1262162837 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: http://www.wolframalpha.com/input/?i=Mudkipz < 1262162858 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :bottom can also mean nil or false, depending on the language in question. < 1262162866 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1262162878 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I have never ever heard that. < 1262162882 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's the return value of a function with an infinite loop in < 1262162902 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: in logic its not uncommon to find bottom for false < 1262162902 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Actually, errors are _|_ too < 1262162917 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :poop = error "blah" < 1262162921 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :poop is bottom < 1262162923 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's kind-of a different sort of return value... < 1262162928 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Nope < 1262162931 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what about throwing an exception past the caller to a handler outside? < 1262162946 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :All types are TheType | _|_ < 1262162957 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Unless you use Total FP < 1262162962 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But that's sub tc < 1262162976 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: In the io monad < 1262162981 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If not, yep _|_ < 1262162996 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Want those audios? :-( < 1262163036 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ok, so this explains bottom, which almost certainly has its own unicode char < 1262163046 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yeah < 1262163054 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Logical false or sth < 1262163068 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :⟂ < 1262163078 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :actually used for the geometric meaning, "perpendicular to" < 1262163083 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :http://en.wikipedia.org/wiki/Bottom_type < 1262163114 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :also http://en.wikipedia.org/wiki/Bottom_element < 1262163170 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :says common lisp's nil is a bottom. < 1262163178 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :which im not sure i buy, but whatever < 1262163209 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You're a bottom. Er, I think this conversation just strayed into territory I don't want it to stray into. < 1262163214 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :well, i am, but. < 1262163215 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :butt. < 1262163237 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :it seems like Bottom can be non-termination, but it can be other things as well < 1262163242 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :including null < 1262163253 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: There are two chars iirc < 1262163261 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :WANT THE AUDIO? < 1262163263 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :and other things that might be conceived as non-termination in some abstract sense < 1262163268 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :e.g. not returning a value at all < 1262163270 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: err, I don't see why audio's relevant < 1262163284 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: The voice explanation of frp < 1262163297 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'd prefer IRC < 1262163302 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :SOMEONE LOVE ME ;;;;;;;;;;;_;;;;;;;; < 1262163311 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: but I already recorded it :p < 1262163321 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: i love you! < 1262163326 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :in that special way < 1262163327 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'm not transcribing 4 minutes of speech :D < 1262163341 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :augur: the ephebophilic way? < 1262163350 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ugh, filebin.ca is still malware-blocked < 1262163358 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :no ofcourse not < 1262163360 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I could just get around the block, but it feels wrong to do that somehow < 1262163361 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :that would be wrong < 1262163375 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :so so wrong < 1262163395 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yeah. Blocks are sacrosanct! < 1262163401 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oh I love comedic timing < 1262163483 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :NOBODY LIKES MY VOICE ;;;;;;;;;_;;;;;;;;; < 1262163659 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :your voice is girly < 1262163672 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :so i imagine people into girls like your voice < 1262163718 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::| < 1262163826 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :its ok < 1262163828 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :youre still adorable < 1262164232 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262164266 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262164270 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :wabi < 1262164478 0 :mycroftiv!unknown@unknown.invalid QUIT :Read error: 104 (Connection reset by peer) < 1262164542 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :My conversation died :( < 1262164549 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1262164556 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I was enjoying talking about that language < 1262164572 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :what language < 1262164748 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :4 hours 12 minutes. I talked about it continuously for about that long. Wow. < 1262164757 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :augur: My language. < 1262164766 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :which language is that < 1262164770 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Mine. < 1262164776 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :which is? < 1262164783 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Mine. < 1262164785 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric ::| < 1262164810 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Do you feel up to reading 4h12m of talk? < 1262164816 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :no < 1262164821 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :can you summarize it please < 1262164825 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1262164827 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1262164887 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oh well. < 1262164889 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262165292 0 :mycroftiv!n=infernus@h69-128-47-243.mdsnwi.dedicated.static.tds.net JOIN :#esoteric < 1262167134 0 :FireFly!n=firefly@1-1-3-36a.tul.sth.bostream.se JOIN :#esoteric < 1262169030 0 :ehirdiphone!n=ehirdiph@91.105.122.30 JOIN :#esoteric < 1262169042 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So, I had a brilliterrible idea. < 1262169097 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :the sort of thing ais523 would think of if he just generated ideas without honing on interesting things, I think < 1262169108 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1262169115 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Neural analogies whatever next < 1262169122 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :actually, I do do that, just most of the boring stuff gets discarded straight off < 1262169126 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and I never tell anyone then forget < 1262169150 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :An Emacs X11 WM that actually makes the windows into Emacs buffers. < 1262169174 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(the xemacs wm thing is just a wm written in elisp. Lame.) < 1262169180 0 :adam_d!n=Adam@client-82-13-16-131.brhm.adsl.virginmedia.com JOIN :#esoteric < 1262169230 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: heh, Blender works a bit like that < 1262169235 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :at least, it seems to have stolen the Emacs WM < 1262169439 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It would be kinda cool actually < 1262169473 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: imagine a modeline on a window < 1262169490 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: heh < 1262169493 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :although, what would the modes be < 1262169547 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Well, xwm-window-mode for one < 1262169562 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :with the oblig menus with actions and settings < 1262169574 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Minor modes... hmm < 1262169593 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: xwm-floating-mode, perhaps? < 1262169610 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, that's C-x 5 < 1262169618 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :meaning? < 1262169625 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :C-x 5 2, rather than C-x 2 < 1262169633 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :to create a floating rather than docked window < 1262169635 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :new-frame or sth? < 1262169638 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1262169656 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :that would just open an emacs frame in an emacs buffer :D < 1262169710 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, the point is < 1262169713 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :your applications are buffers < 1262169718 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :windows < 1262169719 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you can swap them in and out of windows at will < 1262169724 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not applications < 1262169732 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: You misunderstand < 1262169738 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: you mis-emacs < 1262169754 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :X11 windows would be drawn in their own BONAFIDE emacs buffer < 1262169760 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not emacsalike < 1262169767 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Actually an emacs buffer < 1262169782 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that's what I meant too < 1262169794 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Root window = emacs, no window management done on it PFC < 1262169797 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :IFC < 1262169800 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Ofc < 1262169803 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :one window produced by an application under a normal WM = one Emacs buffer < 1262169810 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1262169853 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :but there shall be only One emacs window; for lo, that is what the Prophet did spaketh unto ya < 1262169860 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*us: < 1262169892 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: err, no < 1262169894 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :C-x 2 is two emacs windows already < 1262169901 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you need emacs windows to put the buffers in < 1262169904 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"If Emacs be the heritor of thou'st windows, is it not therefore a Sin to have Emacs begat itself?" < 1262169917 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :/every/ window is an Emacs window < 1262169928 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :There shall be only one Emacs window, and it shall be the root. < 1262169934 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: X11 window < 1262169937 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ah, ok < 1262169940 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I was talking about emacs window < 1262169948 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :how would you do extra emacs frames, though? < 1262169955 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Wouldn't < 1262169961 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I might think about doing it < 1262169963 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Dunno < 1262169968 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but that's losing possibilities you have with emacs's wm at the moment < 1262169979 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the ability to create a floating frame that works independently of the others < 1262169980 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Yes, but Emacs is tiling. < 1262169986 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's tiling and floating < 1262169996 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm... I wonder if C-x 5 o works? < 1262170008 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :no. Emacs itself is tiling < 1262170021 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Other WMs do the floating < 1262170031 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, ok < 1262170035 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :so an emacs wm should do as emacs does < 1262170038 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm... this is a tricky one < 1262170039 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :And only tile < 1262170052 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: BUT < 1262170062 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :If floating is to be offered < 1262170095 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It should be recognised as a heresy unique to the Xfolk; lacking as the result is in Emacs mannerisms, < 1262170108 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :being an unadorned Xdevil, < 1262170130 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :and so on — it is of the Xwindow. < 1262170157 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Therefore, xwm-floating-mode. Q.E.D. < 1262170186 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :in the model here emacs frames "don't exist" < 1262170193 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's like an emacs os < 1262170199 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Emacs is the interface < 1262170218 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Frames become an implementation detail; only one, as the root window. < 1262170240 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, but a floating-mode window makes absolutely no sense in that case < 1262170242 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :as it isn't anywhere < 1262170247 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :from Emacs' point of view < 1262170259 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you couldn't select it, you couldn't close it, you couldn't create it < 1262170265 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :it is "in" emacs because emacs' size is that of the screen < 1262170283 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but it's in a different frame < 1262170285 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :also, if you focus it the invisible corresponding buffer is too < 1262170292 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: No such thing. < 1262170296 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :exactly < 1262170297 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Implementation detail. < 1262170298 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :thus it isn't there at all < 1262170312 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Windows are Emacs' forte. Frames it thinks of not. < 1262170313 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it isn't in the root frame because you can't get to it by recursively picking top, left, etc... windows < 1262170327 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It is omnipotent and sovereign over them. < 1262170332 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :e.g. it would make no sense for C-x o to /cycle/ to it < 1262170338 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :brb < 1262170340 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and if it did, what would C-x 2 do? or worse, C-x 1? < 1262170354 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Its like a buffer not in the frame < 1262170357 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Erm < 1262170359 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :View < 1262170361 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You know < 1262170371 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: oh, in that case, it wouldn't render at all < 1262170372 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not in the tiling buffer arrangement < 1262170381 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so you'd have no way of focusing on it < 1262170390 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Yes it would because we coded it that way < 1262170392 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :brb < 1262170550 0 :oerjan!n=oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1262171270 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Hi oerjan < 1262171275 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hi ehirdiphone < 1262171292 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: Good luck logreading < 1262171304 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :nah < 1262171310 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :4 hrs 12 mins continous talk about my language < 1262171312 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :just searched for my name today < 1262171328 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You missed out on so much :( < 1262171332 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :s/name/nick/ < 1262171339 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Issue < 1262171358 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Your emacs buffer list would be polluted. Cool for window managing < 1262171360 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what? I'm about to go home to sleep < 1262171362 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alas, i usually only read the whole log when it is short < 1262171363 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Suck for editing < 1262171379 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: really? I often have over 30 or so buffers open < 1262171383 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: it has haskelly type theory! < 1262171385 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I rarely kill them, you see < 1262171391 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: well, ok < 1262171395 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and don't use the buffer list at all, except by mistake < 1262171397 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :But what to name them! < 1262171400 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*? < 1262171406 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The window title? < 1262171417 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"title - prog"? < 1262171423 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :with asterisks around it if it's not meant to be saved < 1262171433 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"title - prog [xwm]" < 1262171434 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes, you should be able to save buffers even if they contain windows < 1262171442 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: uh. No. < 1262171452 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :but ugh, it'd be ugly < 1262171464 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :otherwise the semantics are wrong < 1262171472 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you could hook it up to cryopid or something, I suppose < 1262171475 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :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_ < 1262171477 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :**reddit - what's new online! - Mozilla Firefox** < 1262171486 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*in over your head < 1262171486 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :or ideally, just have the programs that run be easy to escape < 1262171499 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: Firefox is a big example of something that should save < 1262171500 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I know it is possible. Agda and Ur do it. < 1262171516 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: You can't coherently save tetris f.e. < 1262171516 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :after all, it has a save-tabs-on-closing option, this would be the same thing < 1262171519 0 :FireFly!unknown@unknown.invalid QUIT :Read error: 60 (Operation timed out) < 1262171528 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: yeah, but i'm assuming there were phd theses involved :D < 1262171529 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: really? I've seen pieces of hardware that could < 1262171530 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It's a wm not an os < 1262171532 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :pause, turn it off < 1262171534 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :at the very least < 1262171541 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ais523: M x tetris < 1262171542 0 :mycroftiv!unknown@unknown.invalid PRIVMSG #esoteric :cant you just make sure that you are within the formal boundaries established by hindley-milner typing? < 1262171551 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: And they're open source < 1262171551 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :anyway, I really had better go < 1262171555 0 :ais523!unknown@unknown.invalid QUIT :Remote closed the connection < 1262171557 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :of course, more power to you if you can pull it off < 1262171558 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :mycroftiv: I exceed those boundaries < 1262171560 0 :FireFly!n=firefly@1-1-3-36a.tul.sth.bostream.se JOIN :#esoteric < 1262171564 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :TC type system < 1262171573 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :W/ dependent types < 1262171584 0 :mycroftiv!unknown@unknown.invalid PRIVMSG #esoteric :i havent read the immensely huge backscroll so i wont make you explain it all again if you already have < 1262171628 0 :mycroftiv!unknown@unknown.invalid PRIVMSG #esoteric :actually i guess i lost most of my backscroll from my mouse button forkbombing me < 1262171640 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: maybe I'll just submit the spec and compiler as a phd thesis to MIT or somewhere without being admitted :D < 1262171655 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :easiest doctorate evar < 1262171710 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: but yeah, it won't be easy < 1262171755 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :so what it's so damn awesome :| < 1262171757 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: it is the soundness proof of your type system i am worried about. not that i know how to do those myself < 1262171803 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :unless you simply steal an already existing one, you'll have to redo it, and i understand it's quite technical stuff < 1262171805 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: If type checking can bottom out surely it's unsound by some definition < 1262171834 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i mean in the cannot-go-wrong sense, i think < 1262171842 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :incomplete < 1262171848 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Bottoming out is going wrong to me < 1262171854 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :unsound would be like, 3 : String < 1262171883 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :it must be one of either < 1262171891 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :presumably incomplete < 1262171895 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :oerjan the fun with dependent types is you need to interleave the value normalization proof < 1262171899 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :i.e. Sound < 1262171909 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: ouch < 1262171924 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :maybe I'll contract a phd out to do the proof :) < 1262171943 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or just assume it's sound xD < 1262171956 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262171979 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :types bottoming out as in < 1262171983 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :because if a proof of well-typed-ness can bottom out, then it is invalid < 1262171992 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Foo Integer = _|_ < 1262171993 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :? < 1262171996 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :um proofs of types, i guess < 1262171997 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :no < 1262172011 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1262172013 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I see < 1262172014 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that is not dependent. < 1262172023 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :right < 1262172047 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I was thinking of using a total subset < 1262172052 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :for the proofs < 1262172173 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :tbh I think my type system is likely incredibly similar to say agda < 1262172179 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :just different notation < 1262172232 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i recall some mention of using a monad to encapsulate non-termination < 1262172260 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :codata Computation A where Now : A -> Computation A ; Later : Computation A -> Computation A < 1262172276 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :then it would presumably be fine, since types are not in that monad, or something < 1262172285 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :then you can race omega many of these for a fixed point < 1262172288 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :least fixed point < 1262172369 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :um shouldn't the _result_ be an A for some option? < 1262172393 0 :anmaster_l!n=AnMaster@unaffiliated/anmaster JOIN :#esoteric < 1262172410 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Don't want to make partiality a monad < 1262172440 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Hmm my type system is probably closest to epigram < 1262172457 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :programming more than proofy and haskellsimilar as it is < 1262172460 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it was for epigram i heard that mention, i think < 1262172473 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :what mention? < 1262172478 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :of the monad < 1262172492 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1262172492 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :except it was not something implemented, iirc < 1262172494 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :really? < 1262172506 0 :MigoMipo!n=MigoMipo@84-217-7-85.tn.glocalnet.net JOIN :#esoteric < 1262172512 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :I used it in haskell to write (even more) lazy programs < 1262172513 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :It just makes code awkward having a partiality monad :p < 1262172515 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :just an idea for making epigram practically TC < 1262172537 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :at some point I surrender safety for practicality < 1262172554 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :the partiality monad is that point < 1262172568 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :yeah I have no idea how to do even simple proofs about termination for the partiality monad < 1262172594 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: wait, isn't epigram tc? < 1262172604 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :You're thinking of that other Lang < 1262172607 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Charity < 1262172622 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: i thought epigram was a total language < 1262172646 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :hmm. Maybe epigram 1 is but 2 not? Dunno < 1262172655 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Maybe both are total < 1262172680 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :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 < 1262172685 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION may very well be confused, has only read discussions (on ltu mostly?) and that was long ago
< 1262172711 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well one step of a turing machine computation is total... < 1262172734 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :yeah you can take the transitive closure of it though < 1262172753 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :poop. < 1262172765 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: hm? < 1262172796 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :anyway ur works and only has one phd behind it < 1262172802 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I rest my case :p < 1262172833 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :Ur isn't actually dependently typed is it < 1262172849 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I think it is? < 1262173207 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1262173245 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :soupdragon: it does have type-level programming that constructs values. I'd be surprised if it wasn't dependent < 1262173266 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :I wish I could compile it :| < 1262173277 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Why can't you? < 1262173293 0 :soupdragon!unknown@unknown.invalid PRIVMSG #esoteric :soem error to do with gmp or something < 1262173313 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'll fix it gimme ssh :P < 1262173660 0 :ehirdiphone!unknown@unknown.invalid QUIT :"Get Colloquy for iPhone! http://mobile.colloquy.info" < 1262173763 0 :Pthing!unknown@unknown.invalid QUIT :Remote closed the connection < 1262175675 0 :oerjan!unknown@unknown.invalid QUIT :"leaving" < 1262175824 0 :cheater!n=gast@62.176.155.187 JOIN :#esoteric < 1262175830 0 :cheater!unknown@unknown.invalid PRIVMSG #esoteric :hi guys < 1262175865 0 :cheater!unknown@unknown.invalid PRIVMSG #esoteric :has anyone got a working implementation of Piet or a similar lang? < 1262180652 0 :MizardX!n=MizardX@unaffiliated/mizardx JOIN :#esoteric < 1262180706 0 :adam_d_!n=Adam@client-82-13-16-131.brhm.adsl.virginmedia.com JOIN :#esoteric < 1262181211 0 :adam_d!unknown@unknown.invalid QUIT :Read error: 60 (Operation timed out) < 1262181233 0 :MizardX!unknown@unknown.invalid QUIT :"..." < 1262182145 0 :Sgeo!n=Sgeo@ool-18bf618a.dyn.optonline.net JOIN :#esoteric < 1262182181 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Hm, ehird's not here? < 1262182218 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ehird, if you see this, know that the penultimate story of Fine Structure has been published. < 1262182223 0 :adam_d_!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262183728 0 :soupdragon!unknown@unknown.invalid QUIT :"Leaving" < 1262184787 0 :MigoMipo!unknown@unknown.invalid QUIT :"When two people dream the same dream, it ceases to be an illusion. KVIrc 3.4.2 Shiny http://www.kvirc.net" < 1262184959 0 :BeholdMyGlory!n=behold@d83-183-183-70.cust.tele2.se JOIN :#esoteric < 1262185144 0 :Asztal!n=asztal@host86-156-98-222.range86-156.btcentralplus.com JOIN :#esoteric < 1262185640 0 :bsmntbombdood!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262190469 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Yowza. < 1262191859 0 :Slereah!n=Slereah@ANantes-259-1-34-102.w92-135.abo.wanadoo.fr JOIN :#esoteric < 1262192459 0 :Slereah_!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262193562 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Read error: 104 (Connection reset by peer) < 1262193667 0 :adam_d!n=Adam@client-82-13-16-131.brhm.adsl.virginmedia.com JOIN :#esoteric < 1262193831 0 :BeholdMyGlory!n=behold@d83-183-183-70.cust.tele2.se JOIN :#esoteric < 1262196876 0 :adam_d_!n=Adam@client-82-13-16-131.brhm.adsl.virginmedia.com JOIN :#esoteric < 1262197760 0 :adam_d!unknown@unknown.invalid QUIT :Read error: 110 (Connection timed out) < 1262200873 0 :MizardX!n=MizardX@unaffiliated/mizardx JOIN :#esoteric < 1262201540 0 :jpc!n=jw@unaffiliated/javawizard2539 JOIN :#esoteric < 1262203398 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote closed the connection < 1262203841 0 :BeholdMyGlory!n=behold@d83-183-183-70.cust.tele2.se JOIN :#esoteric < 1262204193 0 :oerjan!n=oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1262204359 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : has anyone got a working implementation of Piet or a similar lang? < 1262204376 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :have you checked the author's home page at http://www.dangermouse.net/esoteric/piet/tools.html ? < 1262205270 0 :brado!i=56936dfa@gateway/web/freenode/x-cqwelloaqdnnekod JOIN :#esoteric < 1262205295 0 :brado!unknown@unknown.invalid PART #esoteric :? < 1262205694 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cheater: see above ^ < 1262210155 0 :coppro!n=coppro@unaffiliated/coppro JOIN :#esoteric < 1262210185 0 :Gracenotes!unknown@unknown.invalid QUIT :"Leaving" < 1262210330 0 :calamari!n=calamari@ip72-211-145-161.tc.ph.cox.net JOIN :#esoteric < 1262211684 0 :Fredrik1994!n=FIQ@213-67-76-113-no52.tbcn.telia.com JOIN :#esoteric < 1262211689 0 :Fredrik1994!unknown@unknown.invalid PART #esoteric :? < 1262213050 0 :MAKACOW!i=makacowd@200-100-212-76.dial-up.telesp.net.br JOIN :#esoteric < 1262213382 0 :MAKACOW!unknown@unknown.invalid PART #esoteric :? < 1262214908 0 :Gracenotes!n=person@wikipedia/Gracenotes JOIN :#esoteric < 1262215126 0 :soupdragon!n=somebody@unaffiliated/fax JOIN :#esoteric < 1262216082 0 :soupdragon!unknown@unknown.invalid QUIT :Read error: 60 (Operation timed out) < 1262217022 0 :calamari!unknown@unknown.invalid QUIT :"Leaving" < 1262217378 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, dmm made piet!? < 1262217383 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1262217444 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :indeed < 1262217470 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and several others < 1262217554 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :http://dangermouse.net/esoteric/