< 1270166405 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1270166520 0 :Gregor!unknown@unknown.invalid TOPIC #esoteric :History | News: 0 events tunes.org private sector in the beginning of Christ Foundation | http: / / / ~ 2 per year - and through Torah mandelstam. | http://tunes.org/~nef/logs/esoteric/?C=M;O=D < 1270166768 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving < 1270167219 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric ::) < 1270167241 0 :mibygl!~62d188c5@gateway/web/freenode/x-vxguxcvnhvjafhzr JOIN :#esoteric < 1270167259 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION generates a text file containing ten web sites' Terms of Service.
< 1270167284 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION delimits them with "bork bork bork bork bork"
< 1270167323 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Mmm, BSV files. < 1270167641 0 :augur_!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270167678 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270167684 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :Now I'd like to generate a three-word Markov chain out of this. < 1270167816 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :I guess three words is too much to ask, so I'm generating a seven-character one instead. < 1270167844 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :Since the average word contains one and a third characters. < 1270167963 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :t a wo c o an a t ch. < 1270168033 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ancient inca god of markov chains < 1270168342 0 :adam_d_!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270168639 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :"B. Types of Service is not changes upon the Ass, and all lawsuits brough the injury, the account integer. If a Products or goods the number of your period, The Roster" < 1270169150 0 :augur_!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1270169374 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :TO AGREE TO THESE TERMS, DO NOT CLICK "AGREE," AND DO NOT USE THE SERVICE IN ANY MANNER WHICH CREATES THE IMPRESSION THAT SUCH ITEMS BELONG TO OR ARE ASSOCIATED WITH YOU OR, EXCEPT AS OTHERWISE PROVIDED HEREIN, ARE USED WITH BLP’S CONSENT, AND YOU ACKNOWLEDGE THAT YOU HAVE NO OWNERSHIP RIGHTS IN AND TO ANY OF SUCH ITEMS. < 1270169935 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : (Sony investigating the PS3 date bug) <-- link? < 1270169941 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270169942 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :front page? < 1270169948 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION looks there
< 1270169956 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that's some nice timing < 1270170239 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, ? < 1270170286 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: try reloading now < 1270170296 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION whistles innocently
< 1270170325 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, I got the old version still < 1270170328 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :in another tab < 1270170335 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :good :D < 1270171414 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :Wow, it's surprisingly difficult to create a user from the command line in OS C. < 1270171435 0 :mibygl!unknown@unknown.invalid PRIVMSG #esoteric :I can't believe that in the 90 versions they've released since OS X, they still haven't fixed that. < 1270171565 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : Wow, it's surprisingly difficult to create a user from the command line in OS C. <-- yeah, I heard it is all a chimera that OS . < 1270171585 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :try OS X instead :P < 1270172177 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 248 seconds < 1270172521 0 :augur!~augur@c-98-218-226-149.hsd1.dc.comcast.net JOIN :#esoteric < 1270174461 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270175246 0 :augur!~augur@c-98-218-226-149.hsd1.dc.comcast.net JOIN :#esoteric < 1270175563 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270175686 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1270177500 0 :mibygl!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1270177911 0 :augur!~augur@c-68-54-80-152.hsd1.md.comcast.net JOIN :#esoteric < 1270178367 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1270179636 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270180281 0 :augur_!~augur@c-68-54-80-152.hsd1.md.comcast.net JOIN :#esoteric < 1270180302 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270180890 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1270181073 0 :augur_!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270181277 0 :oerjan!unknown@unknown.invalid QUIT :Quit: Good night < 1270183320 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Got a wireless mouse! < 1270183897 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :It's working < 1270183902 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Feels a bit fast though < 1270183921 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :And randomly nonworky < 1270185037 0 :charlls!charlls@186.72.27.213 JOIN :#esoteric < 1270186384 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1270187576 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270187824 0 :augur!~augur@216-164-33-76.c3-0.slvr-ubr1.lnh-slvr.md.cable.rcn.com JOIN :#esoteric < 1270190414 0 :kar8nga!~kar8nga@91.35.72-86.rev.gaoland.net JOIN :#esoteric < 1270191444 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :No one minds if I mutter to myself in the channel, right? < 1270191453 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Not generally. < 1270191507 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Ok. Going to try to work out a sane way to think about AW action scripts to see if it might be TC [given an assumption that TC means you can add more "memory" as needed] < 1270191552 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :So, objects have names, and can, in response to existing, in response to user input, and in response to receiving a signal, send a signal to a name < 1270191563 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Names do not have to be unique < 1270191646 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :The receiver of a signal can have a timer such that, its "signal done" event occurs some time later. Other objects can interrupt such events and stop them from occuring < 1270191682 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :However, if an object receives a signal, by itself it can't decide "if this I'll do this, otherwise I'll do that" < 1270191698 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :However, names can be changed, and not just by sending and receiving signals < 1270191714 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :I have too much of a headache to think about all of this. I should really just sleep. < 1270192242 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Night all < 1270192980 0 :MizardX!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1270193902 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1270194872 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270195199 0 :clog!unknown@unknown.invalid QUIT :ended < 1270195200 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1270195628 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1270195802 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1270196495 0 :adam_d!~Adam@client-86-31-200-91.oxfd.adsl.virginmedia.com JOIN :#esoteric < 1270198100 0 :augur!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270198485 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1270198956 0 :augur!~augur@216-164-33-76.c3-0.slvr-ubr1.lnh-slvr.md.cable.rcn.com JOIN :#esoteric < 1270201041 0 :lereah_!~lereah@nanpc301.in2p3.fr JOIN :#esoteric < 1270201906 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1270202545 0 :Asztal!~asztal@host86-155-75-239.range86-155.btcentralplus.com JOIN :#esoteric < 1270203147 0 :alise!~alise___@212.183.140.48 JOIN :#esoteric < 1270203247 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :14:31:55 This is the Epigram language? < 1270203249 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no it's just me < 1270203266 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :15:04:05 AnMaster: it's April 2 now < 1270203274 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Then you are very late: 12 am is the end of the fools. < 1270203386 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Mart < 1270203407 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :A dark delimitation. < 1270203696 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so hey, |Sigma x:T, P| = sum x:T, P < 1270203712 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :this is i think one of my favourite isomorphisms ... |x op y| = |x| op |y| < 1270203729 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what does it mean? < 1270203733 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :|.| < 1270204255 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cardinality < 1270204256 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :although since we're talking type theory and have no |.| :: Type -> Cardinality < 1270204256 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's actually more involved < 1270204256 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :like |a+b|=|a|+|b| is actually < 1270204256 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hc(a,n) -> hc(b,m) -> hc(a+b, n+m) < 1270204256 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where hc = "has cardinality" < 1270204257 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :for instance the statement about sigma would require some sort of function < 1270204271 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :((y:T) -> hc(P[x := y], something)) < 1270204282 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where x[y:=z] is variable substitution < 1270204290 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :as an assumption < 1270204476 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: but err you know the type theory notation in general right? < 1270204482 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :like a+b is Either a b < 1270204487 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :no not really < 1270204489 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ah okay < 1270204491 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah i know that < 1270204497 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :a*b is -- cartesian product here -- a pair of a and b (cardinality |a|*|b|) < 1270204526 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(non-dependent) a -> b has cardinality |b|^|a|, but using b^a for that like in set theory is ugly < 1270204532 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because, you know, we like our functions < 1270204540 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and having it all in hugely nested superscripts would be silly < 1270204585 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :sure < 1270204586 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :i wonder what the cardinality of Pi (x:T). S is... < 1270204617 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :where T and S are types? < 1270204617 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :product (x:T), |S|? if so that would be so perfect < 1270204620 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270204627 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well let's see < 1270204631 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :say cardinality of 3 -> 3 < 1270204637 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(a, b, c : 3) < 1270204646 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :|3| = 3, obviously < 1270204653 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so it's 3 * 3 * 3 < 1270204655 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric := 3^3 < 1270204658 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yay < 1270204659 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's right < 1270204687 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Pi (x:T). S is basically a definition of TxS where i live < 1270204699 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :normal math that is < 1270204701 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1270204743 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :no wait < 1270204774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: yeah but S can include x < 1270204805 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :refl : Pi (T : *). Pi (x : T). x = x < 1270204831 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :* is type of types smaller than *... I don't want to think about its cardinality right now < 1270204853 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but for a given type T, Pi (x : T). x = x has the cardinality of T... < 1270204855 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but you could have more complex things < 1270204855 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :consider < 1270204870 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Pi (x : N). Pi (y : N). x = y -> () < 1270204873 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :remember -> is shorthand for Pi so < 1270204880 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Pi (x : N). Pi (y : N). Pi (_ : x = y). () < 1270204893 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :now of course this is the same as Pi (x : N). () < 1270204894 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and to continue my sentence ...it's S^T < 1270204908 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so it certainly isn't the obvious thing < 1270204922 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :also () = 1... < 1270204926 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well not the number < 1270204926 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but we call it 1 < 1270204930 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because it has one value < 1270205039 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\prod_{E:n=m} -- there's only ever 1 or 0 values of type n=m < 1270205093 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Pi (x : T). x = x <<< what does this mean, the type of functions that ...? < 1270205111 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :sorry about the asynchronicity, i'm doing two things at once and i suck at it. < 1270205151 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Pi (x:T).S is like T->S, but the value of the T is bound to x in S < 1270205168 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :its cardinality is product (x:T). S which is fitting because the tw are the same notation < 1270205172 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :which is just this isomorphism again < 1270205220 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so in Pi (x : T). x = x what does = x mean < 1270205262 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270205264 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :obviously the cardinality of Pi (x : T). x is 1 < 1270205267 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :x = x is just nice notation for Eq x x < 1270205272 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1270205278 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :which is? < 1270205280 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :for all values x and y of the same type Eq x y is a type < 1270205290 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and there is < 1270205291 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :refl : x -> x = x < 1270205296 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(it has a more complicated type but ... that is the relevant parts) < 1270205299 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(the rest is just type stuff) < 1270205312 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so if we have a value of type x = y, we know that x and y are completely indistinguishable... < 1270205317 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's just equality < 1270205341 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so we have m,n : N, and we know that m = n < 1270205343 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so the two must be exactly the same < 1270205350 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so we have \x. f x x refl < 1270205358 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :which is exactly the same as f, just with less stupid arguments < 1270205363 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://1.618034.com/blog_data/math/formula.3405.png < 1270205394 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so the cardinality of functions (n:N) -> (m:N) -> n = m -> () < 1270205399 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :is the same as the cardinality of the naturals < 1270205418 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because the only function of type N -> () is \_.() < 1270205424 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well < 1270205427 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :not quite < 1270205428 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Pi n : N . 1 has cardinality |N|? < 1270205431 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :er wait < 1270205435 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the last bit is wrong < 1270205447 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :sec < 1270205452 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://1.618034.com/blog_data/math/formula.3406.png < 1270205453 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :obviously < 1270205459 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because 1*1*1*1*... = 1 < 1270205476 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :note the bold 1 in the |...| denotes the type with one value, tt : 1 < 1270205483 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the non-bold 1s are just the regular number 1 < 1270205496 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :also the product in the |...| denotes dependent functions... < 1270205503 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :whereas after it's normal numbery products < 1270205527 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so say n : N, then Eq n n is a type? what values are of that type? < 1270205585 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :let me just give you the definition in pseudohaskell < 1270205608 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :data Eq : forall a, a -> a -> Type where < 1270205617 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : refl :: a -> Eq a a < 1270205619 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1270205625 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : refl :: (x:a) -> Eq x x < 1270205669 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://1.618034.com/blog_data/math/formula.3407.png < 1270205673 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :generalised for non-1 result types < 1270205688 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i thought i know that already, if x is of type a, then Eq a a is a type. i still don't see what things can be of that type < 1270205694 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :note that if T = Bool, |T| = 2, so we have 2^N_0, which is the cardinality of the reals... < 1270205697 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*knew < 1270205700 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :actually they're the computable reals for us, but < 1270205703 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*Eq x x < 1270205711 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no, you are wrong < 1270205717 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if x is of type a, and y is of type a, then Eq x y is a type < 1270205731 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :when I restate things it's because you said something that was wrong < 1270205742 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :x:a -> Eq x x is a type is just a special case of that < 1270205747 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :nope < 1270205749 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that isn't even true < 1270205753 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that isn't even remotely correct < 1270205756 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Eq :: (A : Type) -> A -> A -> Type < 1270205765 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :refl :: (A : Type) -> (x : A) -> Eq x x < 1270205771 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :one is a type one is a value < 1270205775 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :"if x is of type a, and y is of type a, then Eq x y is a type" <<< i just instantiate this with x and y the same object < 1270205778 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and Eq x y is a type for ALL x and y < 1270205784 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: but it's IMPORTANT < 1270205789 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because if they had to be the same it would be a useless type < 1270205791 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and i get "if x is of type a, and x is of type a, then Eq x x is a type" < 1270205806 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :IT'S A FUCKING USELESS TYPE ANYWAY BECAUSE YOU HAVEN'T TOLD ME WHAT IT CAN CONTAIN < 1270205811 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :god you suck at explaining things < 1270205813 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : refl :: (A : Type) -> (x : A) -> Eq x x < 1270205816 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I have; several billion times. < 1270205828 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'll ask fax at some point < 1270205837 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I didn't sign up to teach type theory to someone who doesn't know it, so it's no surprise I'm not prepared for it. < 1270205843 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :refl does not return a type. < 1270205846 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh refl is a value :P < 1270205846 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It returns a value of type Eq x x. < 1270205854 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So is Eq, actually, because types are values. But. < 1270205855 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay thanks < 1270205878 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So we have Eq x y, but only Eq x x is inhabited. < 1270205878 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah okay i see it now < 1270205885 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :All the rest are uninhabited, so we can't prove (give a value) them. < 1270206211 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah okay i see what Eq is now, the haskell does indeed explain it completely < 1270206266 0 :tombom!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1270206332 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so Eq x y is inhabited by ":)" if x = y, otherwise there's no value of that type < 1270206362 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pretty much yep < 1270206365 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :except it's refl not :) < 1270206375 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so obviously if we have m,n:N and m=n, m and n are completely redundant < 1270206469 0 :MigoMipo!~migomipo@84-217-15-62.tn.glocalnet.net JOIN :#esoteric < 1270208126 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : 15:04:05 AnMaster: it's April 2 now < 1270208126 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : Then you are very late: 12 am is the end of the fools. <-- ? < 1270208133 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :is that UK tradition? < 1270208134 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :What? < 1270208142 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oh; perhaps it is only UK tradition. < 1270208151 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It certainly is but I assumed it was so elsewhere too. < 1270208155 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I never heard of it before at least. < 1270208166 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Well, it has fallen out of favour in this interblaggy world. < 1270208175 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I thought it went on for the whole day < 1270208188 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, oh? < 1270208239 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1270209040 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1270209526 0 :MigoMipo!unknown@unknown.invalid QUIT :Quit: Konversation terminated! < 1270209599 0 :MigoMipo!~migomipo@84-217-15-62.tn.glocalnet.net JOIN :#esoteric < 1270209709 0 :MigoMipo!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270209812 0 :MigoMipo!~migomipo@84-217-15-62.tn.glocalnet.net JOIN :#esoteric < 1270210346 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Quit: Leaving < 1270210379 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1270211937 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1270212050 0 :kar8nga!~kar8nga@86.72.35.91 JOIN :#esoteric < 1270212889 0 :MigoMipo!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270213536 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270213598 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270214972 0 :alise!~alise___@212.183.140.50 JOIN :#esoteric < 1270215278 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1270215372 0 :Tritonio_GR!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270216046 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270217938 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :from kernel changelog (for 2.6.33.2): "We believe this is a secure hole that a none privileged user can crash the system." Interesting, err, word choice. < 1270218068 0 :Sgeo_!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270218101 0 :Sgeo!~Sgeo@ool-18bf618a.dyn.optonline.net JOIN :#esoteric < 1270219193 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You can access /my/ secure hole hur hur. < 1270219585 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wonders how legal it would be to make a language based on the Active Worlds action line stuff
< 1270219815 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, XD < 1270219892 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, another interesting sentence from the same changelog: "Fix this by explicitly storing the end of the biggybacked data in the decompressor, and use that to calculate the compressed image size." < 1270219892 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :" < 1270219901 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Biggybacked! < 1270219923 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, grandma, what a big back you have! < 1270219943 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ALL THE BETTER TO LAY YOU WITH < 1270219944 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Get it? < 1270219946 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Lie on your back? < 1270219947 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Lay? < 1270219948 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's hilarious? < 1270219949 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :augh < 1270219961 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, oh it wasn't innuendo? < 1270219962 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I had no idea I was so awesome < 1270219966 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Of course it was! < 1270219989 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :as I thought to begin with then < 1270220222 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I have noticed that in the kernel changelog the most awkward English grammar in commit messages seems to be written by *.jp people (according the the email in the author line) < 1270220248 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :this is not just in this changelog, but almost every kernel changelog I read so far, which must be quite a large number by now. < 1270220288 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(either that, or Japanese sounding names with an email @intel.com, that is fairly too) < 1270220292 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fairly common* < 1270220379 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Yeah; Standard Japanese Programmer English is a strange breed. < 1270220402 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I wonder why, hm < 1270220430 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Japanese is very different from English. < 1270220440 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And Engrish is ubiquitous in Japanese culture. < 1270220455 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270220478 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what about Hollywood movies and such on TV? < 1270220564 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :or do they dubb those? < 1270220575 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Presumably. < 1270220580 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :They do everywhere else :-) < 1270220585 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :not here < 1270220592 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :generally they just add text lines at the bottom < 1270220595 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Also I'd say that Japan imports less culture from other countries. < 1270220600 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Probably because we're too busy importing all theirs. < 1270220696 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Someone I know who once visited Germany (for an extended period of time, business stuff iirc) told me that she was bored one day and decided to see a movie at the local cinema. She decided on a Bond movie thinking "oh well, I can always understand the English and ignore the text lines". Unfortunately it turned out it was dubbed. < 1270220706 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1270220719 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :In Sweden only movies aimed at children are generally dubbed. < 1270220752 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I suppose you strongly push English there. < 1270220762 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Less so in Germany I would imagine. < 1270220768 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Because people actually speak German ;-) < 1270220782 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Anyway, shoulda pirated it! < 1270220789 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :we do generally speak Swedish though :P < 1270220798 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, this was during the early 1990s iirc < 1270220805 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so well, that would have been fun < 1270220812 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hells yeah, ZMODEM! < 1270220851 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"Tarski, one of the early great researchers in set theory and logic, proved that AC is equivalent to the statement that any infinite set X has the same cardinality as the Cartesian product X x X. He submitted his article to Comptes Rendus Acad. Sci. Paris, where it was refereed by two very famous mathematicians, Fr�chet and Lebesgue. Both wrote letters rejecting the article. Fr�chet wrote that an implication between two well known truths is not a new < 1270220852 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :har < 1270220852 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :result. And Lebesgue wrote that an implication between two false statements is of no interest. Tarski said that he never again submitted a paper to the Comptes Rendus." < 1270220892 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :AC is not alternating current here right? < 1270220903 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Axiom of choice < 1270220943 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right < 1270220998 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1270221084 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wonders how someone who thought that one was the truth and the other was false would react
< 1270221187 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I am pretty sure that is trivially contradictory. < 1270221192 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :After all, they were proven to be equivalent. < 1270221201 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So the rejection would be "LOL you made mistake" < 1270221209 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Not "Nice paper, boy. It's shit." < 1270221440 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :One reason why the negation of the axiom of choice is trueAs part of a complicatedtheory about a singularity, I wrote tentativelythe following :We apply set theory with urelements ZFU to physicalspace of elementary particles;we consider locations as urelements, elements of U,in number infinite. Ui is a subsetof U with number of elements n. XiUi is the infinitecartesian product and a set of paths. < 1270221481 0 :Sgeo_!~Sgeo@ool-18bf618a.dyn.optonline.net JOIN :#esoteric < 1270221525 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, I think "LOL you made mistake" would be "somewhat" anachronistic in this case < 1270221547 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :STFU Cantor --Wittgenstein < 1270221555 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hah < 1270221573 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hilbert, you're a fag. Please commit program-suicide. --Godel < 1270221587 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :meh < 1270221606 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, Pretty sure it was "Gödel"? < 1270221615 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Lazy. < 1270221623 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and that should be transcribed as "Goedel" in English then, shouldn't it? < 1270221650 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Yeah but nobody does. < 1270221657 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :lol - "Axiom of Life" = "~choice" < 1270221671 0 :Sgeo!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270221675 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, that's what Hamlet said! < 1270221677 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.facebook.com/group.php?v=wall&gid=2243319629 group of idiots < 1270221709 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well we know that 2b = 2*b < 1270221712 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and as far as types go < 1270221713 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :2 = bool < 1270221715 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :? < 1270221716 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and a*b = (a,b) < 1270221716 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so < 1270221722 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :eh? < 1270221725 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(Bool,b) \/ ~(Bool,b) < 1270221732 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if we interpret ~ as implication of falsehood < 1270221738 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(Bool,b) \/ ((Bool,b) -> False) < 1270221754 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so either you can construct a value of type (Bool,b) or you cannot < 1270221760 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what sort of strange syntax for "and" is (a,b)? < 1270221766 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's not and. < 1270221773 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh multiplication then? < 1270221774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :a*b = (a,b) in type theory < 1270221777 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270221779 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :tuple < 1270221781 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right < 1270221782 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because < 1270221788 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, * is somewhat overloaded :P < 1270221792 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :|a*b| = |a|*|b| < 1270221797 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and also cartesian product < 1270221817 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, is that * = multiplication for the last one? < 1270221819 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :plus it meshes well with disjoint union - a+b - |a+b| = |a|+|b| < 1270221822 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1270221828 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if we do dependent tuples then we have < 1270221838 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :wait, does that hold true for C? It doesn't, does it? < 1270221839 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :|sum x:T, P| = sum x:t, |P| < 1270221842 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where P involves x < 1270221847 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: || is cardinality < 1270221848 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :not absolute < 1270221864 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :|sum x:T, P| = sum x:t, |P| --- if P is constant, i.e. doesn't involve x < 1270221866 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, in " |a*b| = |a|*|b|" ? < 1270221868 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then this is just |T|*|P| < 1270221869 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: yes < 1270221883 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so normal tuples are the degenerate case of dependent tuples < 1270221888 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :dependent function arrows: < 1270221888 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well the result is the same for abs() for R though < 1270221899 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :??? < 1270221900 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cardinality < 1270221902 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :is about sets < 1270221904 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :not absolute < 1270221904 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well yes < 1270221908 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :|prod x:T, S| = prod x:T, |S| < 1270221915 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if we assume that S doesn't involve x < 1270221917 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then we get < 1270221918 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but the overloaded syntax gets confusing < 1270221922 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :|S|*|S|*...|T| times... < 1270221928 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so |S|^|T| < 1270221937 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :we actually say the function arrow is S^T in set theory... < 1270221947 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if we assume it involves x of course both of these are more complicated < 1270221954 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :where ^ is? < 1270221955 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but it's cool < 1270221959 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: exponentiation, obviously < 1270221984 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, not that obvious since most of the other syntax wasn't :P < 1270221998 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :well it is not my fault you don't know type theory :) < 1270222013 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but sum/product types ar enamed that way because they're basically identical < 1270222015 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*are named < 1270222027 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :they're how you['d define addition/multiplication on things like sets if you had to < 1270222032 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, It is just that I get confused when the line is possible to interpret sensibly as more than one thing < 1270222036 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :addition is obviously union - you add all the elements together < 1270222048 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: learn to disambiguate based on context < 1270222104 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, well, then ^ could have been XOR as well, not that likely but... < 1270222142 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Incredibly unlikely - because |S|*|S|*...|T| times is obviously |S|^|T|. < 1270222151 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :true < 1270222864 0 :Sgeo_!unknown@unknown.invalid NICK :Sgeo < 1270223152 0 :lereah_!unknown@unknown.invalid QUIT :Quit: Leaving < 1270223735 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I wish oerjan was here < 1270223929 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :He was < 1270223933 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Don't know when < 1270224147 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I mean now < 1270224333 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION proves False from
< 1270224335 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Axiom func : nat -> (nat -> bool). < 1270224336 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Axiom surj : forall f, exists n, forall x, func n x = f x. < 1270224339 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan was right, obviously < 1270224344 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :just felt like formalising it... < 1270224407 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I take it to mean that that either at least one of those axioms is self-contradictory, or they contradict eachother < 1270224431 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Wait, surj uses func < 1270224525 0 :MigoMipo!~migomipo@84-217-11-15.tn.glocalnet.net JOIN :#esoteric < 1270224538 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: it's basically just one axiom < 1270224540 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :basically < 1270224551 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :if we have a surjective mapping from naturals to functions from naturals to booleans, we're fucked < 1270224552 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :restated: < 1270224560 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :there are more functions from naturals to booleans than there are naturals < 1270224599 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Informal proof, due to oerjan: Say the mapping is called magic. Consider f n := not (magic n n). < 1270224610 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :This is a function nat -> bool. < 1270224621 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :We know that for every function nat -> bool, there is a natural number n such that magic n = that function. < 1270224622 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION tries to understand what surjective means, based on the code. /me fails
< 1270224631 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: simply the above < 1270224637 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Call f's magic number fn. < 1270224643 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Now consider (f fn). < 1270224647 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric := not (magic fn fn) < 1270224650 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :magic fn = f, so this is < 1270224654 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric := not (f fn) < 1270224659 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So, f fn = not (f fn). < 1270224663 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Contradiction. Q.E.D. < 1270224715 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: basically a function A->B is surjective if for every x in B, there exists a y in A such that f(y) = x < 1270224726 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :otherwise our nat -> (nat->bool) mapping could just be < 1270224731 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\n.\m.true < 1270224776 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: incidentally the axiom of choice is about surjective functions < 1270224798 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it states that every surjective function has a right inverse < 1270224803 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :or rather is equivalent to such < 1270224807 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :"right" inverse? < 1270224838 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so, for every surjective function f : A -> B, there exists a function g : B -> A such that f(g(x)) = x for every x in B < 1270224939 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: The formal proof that there cannot exist a surjective function from naturals to functions from naturals to booleans: http://pastie.org/900407.txt?key=w45dbutwoqcuuxwkqnpq < 1270224964 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Is this Coq? < 1270224966 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I had to define not myself - it seems Coq doesn't have it for booleans. < 1270224966 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1270224991 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Then the proof just went by picking out what surj says about our f - that func n x = f x < 1270225006 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then expanding this to not x = x < 1270225010 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :tada < 1270225028 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :here's the steps as it goes: < 1270225031 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :after the destruction: < 1270225033 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : x : nat < 1270225034 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : H : forall x0 : nat, func x x0 = notb (func x0 x0) < 1270225034 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1270225034 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : False < 1270225040 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :after the notdistinct: < 1270225042 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : x : nat < 1270225042 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : H : forall x0 : nat, func x x0 = notb (func x0 x0) < 1270225043 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1270225043 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : func x x = notb (func x x) < 1270225047 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then I just apply H and tada < 1270225055 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION needs to learn Coq before attempting to understand this
< 1270225061 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(we apply notdistinct because (b <> notb b) is shorthand for (b = notb b) -> False) < 1270225071 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(so if we apply it, Coq realises we need to prove (b = notb b) to achieve our goal of False). < 1270225082 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(which we can do: because surj tells us it is so) < 1270225105 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: This also suffices as a proof that the reals are more numerous than the naturals, btw. < 1270225132 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Consider a real number as an infinite string of binary bits (it can just end in 0s if it isn't "really" infinite) < 1270225138 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(nat -> bool) - f n is the bit at position n < 1270225143 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Reals can be treated as functions from .. ah < 1270225148 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so (nat -> bool) ~~ real < 1270225157 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270225164 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so the proof says that we cannot define a function from naturals to reals such that every real has a corresponding rational < 1270225165 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1270225168 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so the proof says that we cannot define a function from naturals to reals such that every real has a corresponding naturla < 1270225169 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*natural < 1270225227 0 :lament!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270225643 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1270226970 0 :MigoMipo!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270227736 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Agda is crazy < 1270228471 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :/home/ehird/code/univ.agda:16,8-11 < 1270228472 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :□∏_ is not strictly positive, because it occurs in the 5th clause < 1270228473 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in the definition of □_, which occurs in the first argument to □∏_ < 1270228473 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in the 5th clause in the definition of □_, which occurs to the left < 1270228473 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :of an arrow in the type of the constructor all in the definition of < 1270228473 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :□∏_. < 1270228478 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: You'd like Agda; it has nice error messages! < 1270228485 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Now to figure out what that perfectly well-formed English is trying to tell me. < 1270228882 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Hail, alise. < 1270228892 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Ho. < 1270228903 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You have me on Monday, too - such a special week's end this is. < 1270228944 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Whoo. < 1270229270 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I was here yesterday, too: but I was too tired to come here. < 1270229274 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I was on my iPhone here, though. < 1270229277 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So, yeah. < 1270229762 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270230572 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1270230682 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, "□" is a square box? < 1270230687 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yes. < 1270230689 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hi alise < 1270230693 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right, not font issues then < 1270230695 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, XD < 1270230697 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hello ais523 < 1270230702 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: it's the magical box of interpretation (I probably should have used brackets) < 1270230706 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :err lol hi alise < 1270230716 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1270230718 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... Man. Microsoft *still* gets buffer overflows. < 1270230733 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: I'm not surprised, that's inherent in C < 1270230740 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that it's hard to check for them < 1270230748 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Not really. It's inherent in bad programmers for C. < 1270230750 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in theory, Splint can statically prove a program has no buffer overflows, but it's not very good at it < 1270230753 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, you can avoid such data structures when possible < 1270230775 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :of course for a binary stream there isn't any good alternative < 1270230783 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I'd say that any programmer bad enough to do that sort of thing shouldn't be allowed to touch C when working. < 1270230795 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(and C doesn't really help with providing other good data structures) < 1270230852 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :anyway, why this? Has there been a new windows exploit recently or what? < 1270230869 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Nah, reading about how they've started doing... Fuzz testing. < 1270230927 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And seeing bunches of buffer overflows in office. < 1270230965 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: in binary formats, or XML formats? < 1270230992 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :As it's the latest version of Office, I'm going to guess "both". < 1270231031 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :buffer overflows in XML is just embarrassing < 1270231034 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fuzz testing can be very useful < 1270231062 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION remembers finding div by zero errors in both cfunge and ccbi early on using a fuzz tester
< 1270231081 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: What's surprising is that they only started doing it. < 1270231087 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :of course, such code isn't very good at finding anything but crash bugs, and only ones that aren't extremely complex to trigger < 1270231136 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, I wasn't online yesterday < 1270231142 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :any good April Fool's stuff I should look at? < 1270231174 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Two in Agora < 1270231174 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, google used microweeks amongst other things to measure how long searches took < 1270231196 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :One good, the other mine < 1270231213 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Programming in C is nearly impossible for a human! < 1270231218 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, gigawatts, parsecs, "shakes of a lamb's tail" and Planck times were used too < 1270231222 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, ok < 1270231227 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :seems surprisingly uncreative for Google < 1270231230 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, oh and the RFC was quite funny too < 1270231233 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, they did other ones too < 1270231240 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ais523, you mean Topeka, right? < 1270231244 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what was the RFC this time? < 1270231258 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, maps.google.com.au, did directions in Australian slang < 1270231265 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: I can do it. For many cases not involving stack munging. < 1270231265 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :s/u,/u/ < 1270231271 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(getcontext et al scares me) < 1270231276 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Yeah, with what error rate? < 1270231284 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Google was renamed to Topeka < 1270231286 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, oh and the Topeka stuff too yeah < 1270231298 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :YouTube videos had a TEXTp option < 1270231302 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh yeah that < 1270231309 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :[not Google] Reddit made everyone an admin < 1270231310 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: ASCII art? < 1270231313 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo, never got that working, was it flash only? < 1270231315 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Fark headlines were acrostics < 1270231319 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster, I.. guess < 1270231321 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, that reddit thing sounds like utter chaos < 1270231323 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Topeka? Missed that < 1270231329 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo, as in, couldn't get the html5 stuff to work for it. < 1270231342 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster, I imagine it might be Flash only < 1270231343 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Lower than you'd expect, actually. < 1270231352 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: I doubt that highly :) < 1270231359 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :When using getcontext, nearly 100%. :P < 1270231359 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I think the admin-mode changes were local-only < 1270231378 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :The admin stuff including infinite upvotes/downvotes < 1270231381 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(which leads me to suspect that I should never, ever touch that.) < 1270231389 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, the RFC was about a tcp option to mark packet mood < 1270231401 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, as in you could perform admin actions but reddit faked the result rather than actually doing it? < 1270231410 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, mood would be encoded as a string of ASCII chars making up a smiley < 1270231415 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ais523, and stored the result per user, I think < 1270231424 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(don't remember if IANA were supposed to assign them or not) < 1270231428 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: ah, OK < 1270231435 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :[unless you changed your own headline, I think] < 1270231436 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: It seems that TEXTp wasn't available in parts of Europe, somebody somewhere said that it worked for him through a US proxy but not from home < 1270231447 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and putting unreasonable registration requests onto IANA is standard with April Fools' RFCs, IIRC < 1270231450 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, anyway: http://tools.ietf.org/html/rfc5841 < 1270231459 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant, hm < 1270231476 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: haha, that's great < 1270231479 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ais523, check Agora? < 1270231484 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: I am < 1270231509 0 :adam_d!~Adam@client-86-31-214-122.oxfd.adsl.virginmedia.com JOIN :#esoteric < 1270231513 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: the first one where you submitted half the proposal is much funnier, given what happened to Nomicapolis < 1270231535 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : pikhq: Programming in C is nearly impossible for a human! <-- hm. That raises some interesting questions about Kernighan and Ritchie.... < 1270231541 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What happened to Nomicapolis? < 1270231590 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: there was an attempt to copy B's ruleset to it, but accidentally only the first half was copied < 1270231598 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, what did reddit do? < 1270231599 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and the resulting ruleset didn't allow rule changes < 1270231604 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: They can't manage it either, they just only publish their successes < 1270231612 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, hm... < 1270231615 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: see above, it's me who was asking rather than answering < 1270231629 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ais523, o.O < 1270231631 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :In fact almost all existing programming languages are completely infeasible for programming which is why we have so many bugs. < 1270231639 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :That does make the accidental post funny < 1270231644 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I saw the discussion about it, but I was unable to locate the line where it said what they did. Something related to admin I gathered < 1270231650 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But people don't want to do a little more work once than do lots and lots of not much work, so they don't use better languages with good type systems. < 1270231650 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: they made everyone an admin < 1270231660 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :or at least, to think they were, according to what I was told earlier in this channel < 1270231665 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1270231668 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :this is all second-hand info, though, and the people who actually told me are still here < 1270231673 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :which is why I'm confused as to why you're asking me < 1270231675 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right < 1270231675 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: ButbutPOINTERS ARE MORE EFFICIENT < 1270231682 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1270231685 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :There was a "turn admin on" link for logged in users < 1270231700 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It made an [A] thingy appear next to other user's name < 1270231710 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Which gave options like ban, x-ban < 1270231713 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AGDA I AM CONFUSED < 1270231731 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It randomly did things like 16.14% shill account < 1270231739 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Let you "edit" headlines < 1270231770 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Upvote and downvote a single thing repeatedly. 10 or more repeated upvotes (not sure if it was 10) made it an upvote to infinity < 1270231778 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Similar in the other direction < 1270231796 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I might be forgetting some stuff < 1270231815 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :personally, I think a language which is C + a proof that it doesn't contain buffer overflows, null pointer derefs, etc. is entirely feasible < 1270231824 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION continues to be annoyed at Splint
< 1270231833 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :for purporting to do exactly what I want, and failing at it < 1270231849 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Repeated variables in left hand side: n < 1270231852 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I know Agda, god damn! < 1270231861 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, Nowdays I seldom use C unless I'm fixing code already written in C. I guess I still use C if I need to do something low level enough that a high level language is impractical. < 1270231876 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Watching Ark of Truth now < 1270231916 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :How the hell do you do dependent pattern matching in this thing? < 1270231926 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :head (witness (S n) f) (successor n) = ? < 1270231929 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :complains about repeated ns < 1270231937 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, splint is a good idea. In practise I found it useless. Mostly because it generates parse errors on even the most basic C99 code. And sometimes also on perfectly fine C89 code. < 1270231953 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: even without parse errors, some of its decisions are just bizzare < 1270231963 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :sjgdflkgjdfhdklgfhg < 1270231974 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, iirc I managed to get splint to segfault when running it on all C files in a directory. The problematic file was one generated by flex. Never found out what in that file caused it < 1270231977 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :e.g. you can move a closing brace of an inner scope one line without changing the meaning of the program at all, but with a visible effect on splint's output (warning vs. no warning) < 1270232009 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, huh? < 1270232013 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Well, lint-type things tend to be about style as much as semantics < 1270232018 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, what is it that it warns about then? < 1270232025 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: my guess is, it's just wrong < 1270232037 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I can't see any explanations for that behaviour other than a bug in Splint < 1270232044 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, if it is just about indention style or something like that, it seems reasonable < 1270232054 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and yes, splint is buggy and unmaintained < 1270232074 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: no, it was about memory leaks < 1270232122 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Well that's a bit messed up, isn't it :-P < 1270232162 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1270232189 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I found clang in static analyser mode moderately useful btw. Doesn't detect a lot of stuff yet and somtimes it "crashes" < 1270232194 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Not as in coredump, but as in assert(0 && "Message that only makes sense to a LLVM developer"). < 1270232228 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(they seem to love assert(0 && "string") btw) < 1270232243 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Would you prefer assert(!"string")? :-P < 1270232276 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1270232290 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant, I would prefer never seeing either when running the program :P < 1270232296 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I HAAAAAAAAAAAATE THIS < 1270232298 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Well yeah < 1270232304 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :But you can't have everything :-P < 1270232330 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :THIS DOESN'T WORK < 1270232407 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :however, clang in static analyser mode seems to have fairly low number of false positives for me (less than splint certainly!). And it doesn't warn about completely irrelevant stuff... < 1270232440 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :can't really tell anything about number of false negatives. A bit hard to know unless you wrote the code with intentional bugs to test the static analyser... < 1270232469 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, define "THIS" < 1270232482 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant, why not btw? < 1270232495 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: stuff < 1270232510 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, ah. < 1270232525 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Dunno < 1270232536 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, very precise description that < 1270232586 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant, so you stated that I can't have everything without having any good explanation for why that is the case? < 1270232630 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :It seems to be the way the world works < 1270232638 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1270232642 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I can't justify why the world works that way < 1270232647 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :right < 1270232679 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm I first considered asking "why not" to that as well, but that would have been silly < 1270232905 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, I don't believe the fuzz-testing Office thing, the article about it was posted on april 1 and claims Microsoft used other people's Windows computers as a botnet < 1270232944 0 :Oranjer!~HP_Admini@adsl-243-221-66.cae.bellsouth.net JOIN :#esoteric < 1270233078 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Hmm. < 1270233154 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Alex Brown deciding that OOXML is doomed to failure seems to be not an april fool's joke, though < 1270233175 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and that's the same sort of event as Miguel de Icaza noticing that Mono has an unclear patent situation < 1270233380 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :"You have watched 72 minutes of video today." < 1270233694 0 :MigoMipo!~migomipo@84-217-11-15.tn.glocalnet.net JOIN :#esoteric < 1270234160 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1270234482 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270234825 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION wants to experiment with unsafeInterleaveIO
< 1270235146 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :what does that do? < 1270235172 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Deferrs the IO operation until the value it gives is needed < 1270235180 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Haven't actually tried it yet < 1270235205 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :wth, I only get an usable wlan signal on my laptop atm if I hold my hand like I was about to change the angle of the lid... < 1270235208 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :that's weird < 1270235225 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: haha < 1270235230 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so presumably it only works on input? < 1270235263 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :the difference is huge too, like -79 dBm vs. -90 dBm for the signal. (My card doesn't report the noise correctly, so no idea about the SNR) < 1270235265 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ais523, well, say, an IO Integer can be made of something that outputs then inputs, so the output SHOULD be deferred until the input is needed < 1270235268 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :That's what I'm testing < 1270235279 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: ah < 1270235292 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I'll paste the results < 1270235306 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I assume you will be able to explain this < 1270235318 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Your hand scatters/reflects more of the signal? < 1270235327 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: probably you're reflecting the signal < 1270235337 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :human skin is pretty reflective wrt microwaves < 1270235346 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, it doesn't work unless I actually touch the plastic on the lid though < 1270235381 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :-90dBm is 1pW and -79 dBm is ~12.6pW... So about tenfold difference... < 1270235401 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :if I hold my hand slightly away (a few mm I guess, hard to measure), I get the bad signal < 1270235426 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270235495 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Ilari, is that p as in pico? < 1270235506 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh btw, what does the m stand for in dBm? < 1270235533 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :The "m" there denotes the reference power is 1 mW. < 1270235536 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: dB relative to mW. That p was supposed to be multiplier for 10^-12... < 1270235555 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Ilari: why convert? 10 dBm is a tenfold difference < 1270235559 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you don't need to convert back into watts < 1270235619 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, reference as in? < 1270235628 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: 0dBm => 1mW < 1270235630 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1270235648 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ais523, http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24603#a24603 < 1270235660 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm, wlan signals are _extremely_ weak then... < 1270235670 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Yes, dB is a dimensionless unit; -90 dB could be anything, as long as it is 10^-9 of something. < 1270235681 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :dBm is the only case I have seen where unit used as reference is not written completely (there's dBV, dBW, etc...) < 1270235687 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: ah, it didn't work? < 1270235696 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ais523, it worked perfectly! < 1270235697 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Look at it < 1270235710 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It only did the interleaved one when it was needed < 1270235718 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, I didn't notice the first wasn't interleaved < 1270235745 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :The wikipedia dBm page has rather nice table of values; "typical received signal power from a GPS satellite" is listed as -127.5 dBm, or 178 aW. That's not a whole lot. < 1270235747 0 :alise!~alise___@212.183.140.50 JOIN :#esoteric < 1270235768 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, isn't dB basically "the range we want is awkwardly large, lets use something logarithmic"? ;P < 1270235776 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, I'm in love with unsafeInterleaveIO < 1270235813 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: it is as unsafe as the name suggests. < 1270235821 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Howso? < 1270235826 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, for ratios that is < 1270235834 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: it breaks Haskell's purity < 1270235842 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It is somewhat less unsafe than unsafePerformIO, but still unsafe. < 1270235846 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :though I wrote that above... seems I only thought it < 1270235848 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Shun it. < 1270235855 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :getContents is acceptable in small utilities but not large programs. < 1270235872 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Why? < 1270235873 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: It means that you can suddenly have errors occuring in any function. < 1270235878 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :presumably, because if you use it twice it might only run once < 1270235881 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what does the "interleave" in it signify? < 1270235882 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Because it breaks Haskell's purity. < 1270235889 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Why not just use unsafePerformIO if you don't care about that? < 1270235894 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I meant, how does it break Haskell's purity? < 1270235896 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, that's unsafePerformIO < 1270235897 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: basically it splits off a lazy thread of IO < 1270235897 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Side effects are interleaved with pure code. < 1270235909 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so unsafeInterleaveIO (... read a file byte by byte) < 1270235910 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, ah < 1270235912 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :produces a lazy string of the whole file < 1270235913 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :Satellite signals are usually extremely weak. That's why one usually sees modulations that have low SNR requirement (like QPSK). < 1270235916 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :only read as required by evaluation < 1270235942 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :consider an unsafePerformIO call that does output < 1270235942 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :then random pure code could cause unpredictable output < 1270235946 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :depending on the evaluation semantics of the implementation < 1270235949 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :all haskell specifies is non-strict < 1270235957 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: getContents >>= return foo -- You get errors in foo. < 1270235965 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :pikhq/alise: and the "perform" in the other one signifies that it isn't lazy then I guess? < 1270235986 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: unsafeInterleaveIO :: IO a -> IO a < 1270235993 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :unsafePerformIO :: IO a -> a < 1270235997 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :aha < 1270235999 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :unsafeInterleaveIO is just return (unsafePerformIO x) < 1270236008 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :unsafePerformIO is, of course, an abomination of the highest order. < 1270236010 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Wait, what's that in do notation? do { a <- getContents; return a} < 1270236021 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, ouch, unsafeInterleaveIO seems very nasty < 1270236025 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :why does haskell even have it? < 1270236029 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :do {a <- getContents; return foo } < 1270236032 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :where foo is a pure expression < 1270236037 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*do { a <- < 1270236047 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: because it is useful: consider interact :: (String -> String) -> IO () < 1270236048 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it is < 1270236058 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1270236059 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :interact f = do s <- getContents; putStr (f s) < 1270236066 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: getContents lazily returns all of stdin < 1270236068 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :this is convenient < 1270236072 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it is a hack - but it is convenient < 1270236073 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: unsafeInterleaveIO is useful for various small utilities. < 1270236075 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so the answer is convenience < 1270236076 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270236092 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Oh, because while it's, with getContents, lazily going through the file, trying to get more out of the "list" may cause an IO error? < 1270236097 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :are the usual "safe" IO facilities implemented using these unsafe ones internally? < 1270236117 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: No, the unsafe ones are done in terms of the safe ones. < 1270236131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Neither. < 1270236133 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: that's nonsensical < 1270236139 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, err. It isn't 1 April any more... < 1270236143 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, maybe pikhq was being sarcastic? < 1270236145 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: unsafePerformIO is just an internal thing that hacks around with the uber-internal IO data structure. < 1270236148 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The default IO operations are primitives. < 1270236156 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, hm < 1270236160 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The IO data structure is not exposed unless you import internal GHC modules. < 1270236169 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: getContents is done in terms of unsafeInterleaveIO and 'safe' IO operations. My statement of this came out confused. < 1270236174 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Is my unterstanding correct? < 1270236175 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Right. < 1270236182 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: pretty much < 1270236187 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's more insidious but that is one special case < 1270236198 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Examples of insidiousness please? < 1270236219 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, hm what language is the io primitives implemented in? < 1270236228 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it would be neat if it was haskell < 1270236232 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but I guess it can't be then < 1270236236 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: They're part of the Haskell runtime, I'm pretty sure. < 1270236243 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Erm. Part of the GHC runtime. < 1270236248 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :The one bit of GHC that's not in Haskell. < 1270236251 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: what pikhq said < 1270236253 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1270236254 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :although the IO data structure is defined in haskell < 1270236260 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and GHC itself is written in haskell (but the RTS is C) < 1270236264 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(exception: random things like the evil mangler) < 1270236265 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :GHC is really gnarly code < 1270236271 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :some parts define the Monad class themselves < 1270236275 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because haskell didn't have it at the time! < 1270236324 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I assume the stuff not implemented in haskell is kept to a minimum? < 1270236348 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :What, the RTS? < 1270236354 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's quite big but it's also rather good. < 1270236358 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270236362 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And most of the Prelude is in Haskell. < 1270236365 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Almost all, in fact. < 1270236371 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's just auto-specialised behind the scenes. < 1270236560 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I just start experimenting with unsafeInterleaveIO, and I get told to avoid it :( < 1270236591 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Well, it is bad. < 1270236684 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :My computer just started singing "Good Morning" to me < 1270236743 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1270236800 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Dear Megavideo: I waited 54 minutes. Now please let me continue watching my video < 1270236897 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Metamath is cool < 1270238954 0 :Oranjer!~HP_Admini@adsl-243-221-66.cae.bellsouth.net JOIN :#esoteric < 1270240301 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270240658 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :You find the strangest things when digging through old home directories; here's a "cp" replacement that copies files by starting two processes, having the first read the input file, the second write the output file, and doing all communication between processes by using the SIGUSR1 and SIGUSR2 signals as the "dit" and "dah" symbols for morse code, and suitable pauses to distinguish words. < 1270240704 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I'm not sure why it doesn't just use those two signals as "on" and "off" events (or just one signal to toggle) and timing for even the dit/dah distinguishement; but it's reasonably silly as-is. < 1270240737 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Sounds fun < 1270240930 0 :Ilari!unknown@unknown.invalid PRIVMSG #esoteric :Reminds me of programming assignment from one course... < 1270241106 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, so it doesn't work for non-text files? < 1270241128 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, as for using timing: would be unreliable on a non-realtime OS < 1270241129 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Right. But be honest, how often do you need to copy non-text files anyway? Almost never! < 1270241143 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Oh, but it's not a problem if you use long enough pauses. < 1270241148 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, more often than text files! < 1270241162 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :only cp command today was to copy a kernel image to /boot < 1270241172 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :20 milliseconds between bytes and 100 milliseconds between words, it seems. < 1270241186 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I don't think I've used cp for about a week now < 1270241198 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I use mv a lot more often than cp < 1270241200 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I don't copy very often; I did yesterday, but via the GUI < 1270241616 0 :alise!~alise___@212.183.140.20 JOIN :#esoteric < 1270242012 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Think maybe you could add the &butiwouldratherbereading= feature to Lonely Dino? < 1270242041 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Shouldn't be /too/ difficult, I could cut up the images as they are ... < 1270242055 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Mmkay. < 1270242169 0 :adam_d_!~Adam@client-82-26-214-230.pete.adsl.virginmedia.com JOIN :#esoteric < 1270242377 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270242387 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :butiwouldratherbereading? < 1270242395 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :sounds like an April Fool's URL param < 1270242414 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That was a fun April Fool's Day, you guys! To replace T-Rex and company with Reginald and Beartato from Nedroid, I used the trick of a transparent PNG file that masked out the existing graphics. Then, I was free to put any new graphics on top! The empty mask file is here, if you want to play with it. < 1270242415 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And play with it you might want to, because although I've turned off the image replacement by default, it's still available on the site! Just add "&butiwouldratherbereading=nedroid" to any Dinosaur Comics URL and you'll see something like this. < 1270242423 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.qwantz.com/index.php?comic=290&butiwouldratherbereading=nedroid < 1270242426 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :amazing < 1270242462 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :http://www.qwantz.com/index.php?comic=35&butiwouldratherbereading=nedroid < 1270242465 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :other params: achewood, pennyarcade, wigu, pokey < 1270242476 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.qwantz.com/index.php?comic=&butiwouldratherbereading=pokey -- thus creating the best comic strip conceivable < 1270242497 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: MISSINGNO < 1270242510 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :...? < 1270242531 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :more parameters: < 1270242533 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :xkcd < 1270242536 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :problemsleuth < 1270242538 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :daisyowl < 1270242551 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :also < 1270242551 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :onewheretrexswearsmore < 1270242567 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.qwantz.com/index.php?comic=548&butiwouldratherbereading=daisyowl < 1270242726 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION decides that the best way to understand the State monad is to read the source
< 1270242776 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's pretty comprehensible anyway < 1270242788 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's basically what you do in Haskell if you really want to make it an imperative lang < 1270242806 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :although, more fun would be some sort of State variant that stored an associative array with ways to update individual elements < 1270242827 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Like the ST monad except with STRefs only storing one type? < 1270242854 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that way, you could compile imperative langs almost literally < 1270242865 0 :oklopol!unknown@unknown.invalid QUIT :Ping timeout: 248 seconds < 1270242943 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: It's nothing to do with ST. < 1270242949 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ST is an entirely different strange beast altogether. < 1270242974 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ST is a safe IO monad. < 1270242982 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, different from State [I know], or different from what ais523 is describing [please explain]? < 1270242985 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Well, just the reference part. < 1270242987 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Its semantics are odd. < 1270242990 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: oh, I see < 1270242992 0 :kar8nga!~kar8nga@91.35.72-86.rev.gaoland.net JOIN :#esoteric < 1270242997 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Well. Yes. That's what makes it safe. < 1270243001 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :State is simply - you know how you could pass an extra argument to every function, Sgeo? < 1270243007 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And just call with a modified argument to change state? < 1270243015 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :State just wraps that into a monad so you don't have to pass it around. < 1270243018 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The semantics are identical, < 1270243019 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :State is pretty much the purest form of a Haskell monad, I think < 1270243020 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*identical. < 1270243023 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, I know what it is, I'm trying to understand how it works, which is why I'm reading the source < 1270243027 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's a monad, and the monad chain is accessible and user-defined < 1270243056 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :as opposed to most monads which are designed to stop you arbitrarily changing the underlying chain, or even determining anything about it except via accessors < 1270243079 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Monads are so pass�. < 1270243123 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, they just get all the press because they're unusual to people who don't know Haskell < 1270243173 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Dependent types are the shiznit. < 1270243191 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :wait, people actually use the word "shiznit"? < 1270243215 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :In theory, I could make my own function that is in the State monad that has state and a value passed to it, without using "get" and "put" < 1270243216 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I have talked to people who think monads are a gargantuan, subtle, and strange library. < 1270243229 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Especially when talking about mathematics! < 1270243237 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Yes. < 1270243237 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Of course. < 1270243252 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: that's what it's /for < 1270243253 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :/ < 1270243255 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :The State monad is a fairly simple thing. That'd be pretty easy to do. < 1270243272 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: no, he means < 1270243276 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :accessing state directly using the constructors < 1270243280 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :The only thing the State monad grants you is nice sugar for that. < 1270243297 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: ah < 1270243303 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Just to clarify my understanding quickly, a >>= b >>= c is parenthesized as a >>= (b >>= c) ? < 1270243316 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: It does not matter. < 1270243322 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The monad laws require the two to be equal. < 1270243329 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Yes, but it does not matter for any proper monad. < 1270243344 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION mindbreaks
< 1270243361 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :That's one of the monad laws. < 1270243377 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Which way of thinking about it would make the definition of >>= for State easier to understand? < 1270243379 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: why do you struggle with simple identities? < 1270243382 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Neither. < 1270243397 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: think of "a >> b" as "do a then b" < 1270243405 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :then it's obvious that a >> b >> c the parens don't matter < 1270243414 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and >>= is just a version where you can grab a return value < 1270243437 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, surely there was a time when you struggled with this stuff. When was that? < 1270243472 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: I picked up monads pretty quickly < 1270243474 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :[Not necessarily THIS stuff in particular, but Haskell in general, or specific parts of Haskell] < 1270243474 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oh, absolutely, I struggled with monads. < 1270243495 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :But I just seem to notice a sort of pattern where you have issues abstracting out simple laws to understand instances satisfying those laws. < 1270243502 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Maybe I'm wrong. < 1270243517 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Certainly I must have my own flaws in understanding that I do not myself notice. < 1270243554 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Rule one with monads: they are simpler than you think. Rule two: they do nowhere near as much as you think. Rule three: there is no magic. < 1270243601 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :syntactic sugar doesn't count as magic? :D < 1270243605 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Rule four with monads: you may need more pixie dust. < 1270243653 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: That's no magic. < 1270243658 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Hah. < 1270243825 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION thinks he gets State's >>=
< 1270243991 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I wish fax was here < 1270243995 0 :comex!unknown@unknown.invalid QUIT :Ping timeout: 268 seconds < 1270244005 0 :comex!comex@c-98-210-192-54.hsd1.ca.comcast.net JOIN :#esoteric < 1270244044 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hi comex < 1270244090 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, fax is in #haskell < 1270244097 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Ah. < 1270244110 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric : I wish fax was here // Awwwww < 1270244119 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :to ask about type theory kthx < 1270244313 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1270244731 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Now, I need to learn to understand Functors and Arrows < 1270244764 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Functors are trivial. < 1270244769 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :As are arrows. < 1270244769 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, about my learning, I've noticed that I like to read a lot of different tutorials < 1270244775 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : if we have a surjective mapping from naturals to functions from naturals to booleans, we're fucked <-- note that "naturals" can be replaced with any set there < 1270244787 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Functors are objects where fmap makes sense. < 1270244793 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, the real numbers don't make up a set? < 1270244813 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: _in both places_ < 1270244853 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :>.> < 1270244868 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it is indeed true (in ZFC) that there is no surjective mapping from reals to functions from reals to booleans. < 1270244927 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :also booleans can be replaced with any set that has a self-map without fixpoints (i.e. any set with at least 2 elements in ZFC) < 1270244957 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :How much of that relies on the C in ZFC? < 1270244963 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(i said it that complicatedly because i'm not sure if those are equivalent concepts in ehird's type theory stuf) < 1270244968 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh, nothing at all < 1270244971 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*stuff < 1270244998 0 :pikhq!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270245001 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION generalises it not to have nat; I realised it didn't need it but didn't think to formalise that
< 1270245013 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it was just my default theory for it. in fact it is essentially true for constructive set theory as well, which is why alise and i started discussing it < 1270245062 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it is true in type theory of course < 1270245065 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :certainly so since I formalised it < 1270245100 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :in my intuition type theory is almost the same thing as constructive set theory. < 1270245110 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Almost, but not quite. < 1270245114 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Type theory has an equality type for instance. < 1270245129 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :And set theory, well, doesn't really have "dependent" sets in any meaningful sense. < 1270245133 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i suppose you could have a simpler constructive set theory than that < 1270245135 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1270245146 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Plus things like quotient sets and the like - but the fundamental theories, sure. < 1270245151 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: http://pastie.org/900901.txt?key=gfjqr1tonuchocnutw2dqw < 1270245203 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I am surprised Coq does not already have notb/notdistinct. Or maybe it does? < 1270245210 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :in fact this is probably a theorem of pure lambda calculus, and the halting theorem, godel's incompleteness theorem and cantor's theorem are all special instantiations of it (diagonalization) < 1270245247 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oh, wait. < 1270245249 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It exists. < 1270245250 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :negb < 1270245267 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Diagonalisation is beautiful. < 1270245360 0 :coppro!unknown@unknown.invalid QUIT :Client Quit < 1270245515 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: http://pastie.org/900907.txt?key=ny2be0sujqn23hvkcty1fa < 1270245525 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Could generalise it from bool if you want, but... < 1270245581 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :mhm < 1270245587 0 :pikhq!~pikhq@75-106-123-198.cust.wildblue.net JOIN :#esoteric < 1270245704 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Should I consider rewriting some of my Python stuff in Haskell? < 1270245721 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Actually, most of it is on my old computer, so meh < 1270245740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oops = < 1270245740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :let e := magic_surj in < 1270245740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :match e (fun n : T => negb (magic n n)) with < 1270245740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :| ex_intro x H => < 1270245740 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : let n := no_fixpoint_negb in < 1270245741 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : match n (magic x x) (sym_eq (H x)) return False with < 1270245742 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : end < 1270245744 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :end < 1270245798 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Hey, Internet's back! < 1270245970 0 :tombom_!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1270246128 0 :pikhq!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270246142 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yay we managed to outrun him again < 1270246152 0 :sshc!unknown@unknown.invalid QUIT :Quit: leaving < 1270246191 0 :tombom!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1270246255 0 :kar8nga!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270246339 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1270246506 0 :coppro!unknown@unknown.invalid QUIT :Client Quit < 1270246808 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : unsafeInterleaveIO is just return (unsafePerformIO x) < 1270246838 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :except with a guarantee of not evaluating more than once < 1270246879 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1270246955 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i used it in Malbolge Unshackled to create an infinite lazy datastructure containing IORefs. afaik that usage is perfectly safe. < 1270246977 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :unsafePerformIO can't get evaluated more than once? < 1270246984 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :erm, things made with < 1270246999 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :in theory it can < 1270247090 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :haskell compilers are perfectly permitted to inline pure code in multiple places < 1270247694 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :(Hence "unsafe" PerformIO) < 1270247730 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I meant unsafeInterleaveIO < 1270247730 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Heh, that's funny; if you have alsamixer open, and then unplug the (USB) sound card it's controlling, you get http://pastebin.com/NL8Sew2t < 1270247853 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :ha < 1270247860 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: indeed, it would be useless for its purpose if it could be evaluated more than once. imagine do l <- getContents; return (l,l) returning two different lists consisting of unpredictable parts of input < 1270247898 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and getContents uses unsafeInterleaveIO internally < 1270247909 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(or something very close to it) < 1270247961 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Isn't there some function (Monad m) => m m a -> m a? < 1270247968 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yes, join < 1270247976 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*m (m a) < 1270247998 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :13:21:43 Just to clarify my understanding quickly, a >>= b >>= c is parenthesized as a >>= (b >>= c) ? < 1270248001 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :13:21:56 Sgeo: It does not matter. < 1270248004 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :13:22:02 The monad laws require the two to be equal. < 1270248027 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :no, it must be (a >>= b) >>= c, the other one isn't even well-typed < 1270248044 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :!haskell :i (>>=) < 1270248064 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :damn egobot always disappearing < 1270248066 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What does it do with IO, and could unsafeInterleaveIO be written without unsafePerformIO using join somehow? < 1270248078 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: oh of course < 1270248092 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :(>>=) :: (Monad m) => m a -> (a -> m b) -> m b < 1270248094 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: ?, and no < 1270248095 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :--from memory < 1270248109 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: it defers running the actual action until the result is needed. no way of doing that with join. < 1270248140 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: it was the fixity/precedence i was looking for, actually < 1270248154 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Oh < 1270248169 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :infixl 1 < 1270248177 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so left as you'd expect < 1270248183 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION still gets confused by fixity
< 1270248202 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's associativity and precedence bundled into one < 1270248217 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Then I'm confused by associativity < 1270248227 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :where associativity is in the syntactic sense < 1270248261 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :basically, should a >>= b >>= c mean (a >>= b) >>= c, a >>= (b >>= c) or be disallowed altogether? < 1270248277 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :those are infixl, infixr and infix, respectively < 1270248281 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Which is which.. oh < 1270248326 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :which side you start combining terms from, essentially < 1270248349 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :HASKELL HAS NO CONCEPT OF FIXITY < 1270248350 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What happens when you mix in other operators of equal precedency? < 1270248377 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: note that those first two are foldl (>>=) [a,b,c] and foldr (>>=) [a,b,c] respectively < 1270248389 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :HASKELL HAS NO CONCEPT OF NULLITY < 1270248395 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :actually it does, I was thinking ARITY < 1270248398 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or would be, if they were compatible types < 1270248460 0 :tombom_!unknown@unknown.invalid QUIT :Quit: Leaving < 1270248463 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: join x intuitively runs x, then runs the result immediately as an action in the same monad. no deferring involved. < 1270248483 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and you cannot simulate it without some special function < 1270248521 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(of course monads other than IO may not strictly obey the concept of running things immediately) < 1270248585 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What are Arrows? < 1270248594 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :a type class < 1270248672 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :a kind of strange bundling of features afaict < 1270248695 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :they're morphisms in a category, so functions are your main example. < 1270248720 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :you can compose them with >>> . for functions f >>> g means g . f < 1270248729 0 :Deewiant!unknown@unknown.invalid QUIT :*.net *.split < 1270248729 0 :wareya!unknown@unknown.invalid QUIT :*.net *.split < 1270248729 0 :Slereah!unknown@unknown.invalid QUIT :*.net *.split < 1270248754 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but they also include operations to combine stuff "in parallel", using pairs < 1270248756 0 :dixon`!~dixon@unaffiliated/reikon JOIN :#esoteric < 1270248759 0 :dixon`!unknown@unknown.invalid PRIVMSG #esoteric :Haskell blows ass < 1270248762 0 :dixon`!unknown@unknown.invalid PART #esoteric :? < 1270248778 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :e.g. (f &&& g) x = (f x, g x) and (f *** g) (x,y) = (f x, g y) < 1270248791 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(again using the function example) < 1270248794 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Well, I'm convinced. Let me brain bleach all my Haskell knowledge. < 1270248805 0 :Deewiant!~deewiant@kekkonen.cs.hut.fi JOIN :#esoteric < 1270248805 0 :wareya!~wareya@cpe-74-70-140-214.nycap.res.rr.com JOIN :#esoteric < 1270248812 0 :Slereah!~Slereah@ANantes-259-1-2-166.w92-135.abo.wanadoo.fr JOIN :#esoteric < 1270248822 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :hey talk about the monomorphism restriction < 1270248831 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :also talk about how unstandard GHC is < 1270248851 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, I don't understand that restriction, as it goes away if you add a type signature < 1270248861 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that says just what the compiler had inferred anyway < 1270248870 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :which is why you disable it < 1270248877 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What _is_ it? < 1270248878 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :why is it there? < 1270248909 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: the basic idea is that if you have an equation of the form x = ... then you should be able to expect the right side not to be evaluated more than once, in practice < 1270248925 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I don't see how that's related... < 1270248955 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but if the type involves type classes, then the right side can only be evaluated after you pass the actual type dictionary into it < 1270248973 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ah, OK < 1270249031 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so it must be evaluated at least once for each type it's used with, and it may be hard for the compiler to catch all uses of the same type so even that might be duplicated < 1270249054 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that's my understanding of the x = ... case. < 1270249078 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Semantically that should be equiv unless unsafePerformIO is involved, right? < 1270249114 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :semantically it's irrelevant < 1270249152 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :for the (x,y) = ... and similar cases there is the additional complication that the type of x or y separately might not determine the full type dictionaries to use in the right part, so in that case you're not even allowed to override with an explicit type signature < 1270249192 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :although the compiler could try to be cleverer there, the standard does not demand it < 1270249224 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: yes. but someone has apparently coughed up an example where this causes exponential blowup in execution time < 1270249227 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :iirc < 1270249244 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :this is why I just use C < 1270249284 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :as for nonstandardness of GHC i don't know, unless you mean its heap of extensions which are optional... < 1270249294 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :"""optional""" < 1270249312 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :return quadrescence :: IO Chatter < 1270249358 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: that doesn't even make sense < 1270249360 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :nice try tho < 1270249393 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1270249471 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: optional aka turned on by default < 1270249511 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1270249575 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well i don't use ghc so i don't know, i thought you had to use a flag for almost everything < 1270249596 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, what do you use? Hugs? < 1270249634 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: oerjan is sane and uses Standard ML with MLton < 1270249638 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(i've recently downloaded the Haskell Platform, but i just saw that winghci will be bundled only with the coming release so i'm waiting a bit) < 1270249648 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :other than that, winhugs < 1270249715 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(i got seriously annoyed when ghci insisted on waiting for the gvim editor to quit and i see winghci avoids that) < 1270249758 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(gvim _tries_ to fork itself to avoid such unless you add a flag, but ghci somehow manages to thwart it) < 1270249779 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: why isn't Monad a "subtype" of Functor? (why it doesn't inherit from the Functor typeclass) < 1270249794 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: hysterical raisins < 1270249800 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :what? < 1270249810 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :"historical reasons" < 1270249813 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270249839 0 :Deewiant!unknown@unknown.invalid QUIT :*.net *.split < 1270249839 0 :wareya!unknown@unknown.invalid QUIT :*.net *.split < 1270249844 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Functor was invented after Haskell 98 was standardized < 1270249865 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :mathematical functors and monads weren't invented with Haskell < 1270249879 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but at first haskell only had monads < 1270249886 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :anyway, I'm feeling so sick that I had better go to bed now < 1270249887 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and they've never managed to implement the "case class" feature that is supposed to make things seamless < 1270249887 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :goodbye < 1270249892 0 :alise!unknown@unknown.invalid QUIT :Quit: Leaving < 1270249905 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :er it's not case class < 1270249913 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION is channeling scala
< 1270249962 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Is Scala any good? < 1270249968 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Or should I stick with Haskell? < 1270249976 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :Scala is great < 1270249986 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i don't know i've just read about it's case classes < 1270249988 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :It has type safety, runs on the JVM, object oriented < 1270249996 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :can run on the android platform < 1270250017 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :still functional < 1270250027 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Quadrescence: as of now you only need to implement (>>=) and return to make a Monad. and haskell doesn't currently have a feature that allows you to deduce a _superclass_ method (Functor's fmap) from that, that's what this class something feature would do < 1270250082 0 :wareya!~wareya@cpe-74-70-140-214.nycap.res.rr.com JOIN :#esoteric < 1270250084 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :they would also like to put Applicative in between, there < 1270250110 0 :adam_d_!unknown@unknown.invalid NICK :adam_d < 1270250189 0 :Deewiant!~deewiant@kekkonen.cs.hut.fi JOIN :#esoteric < 1270250280 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :there's a lot of duplicated functionality between Control.Applicative and the older Control.Monad, in fact i once counted there were only a handful or so of functions in Control.Monad which were _not_ generalizable to Applicative < 1270250380 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :some of that is in Data.Traversable as well iirc < 1270250422 0 :MigoMipo!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270250448 0 :Deewiant!unknown@unknown.invalid QUIT :*.net *.split < 1270250560 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1270250586 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and a bit in Data.Foldable < 1270250640 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*its ^^^^^ < 1270250654 0 :Deewiant!~deewiant@kekkonen.cs.hut.fi JOIN :#esoteric < 1270251290 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I dont know how to compute the product of gaussian periods < 1270251438 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION looks it up
< 1270251459 0 :pikhq!~pikhq@75-106-123-198.cust.wildblue.net JOIN :#esoteric < 1270251590 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :
ACTION suspects a connection with harmonic analysis of finite abelian groups
< 1270251922 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :INTERNET < 1270251966 0 :Oranjer!~HP_Admini@adsl-243-221-66.cae.bellsouth.net JOIN :#esoteric < 1270251988 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ET INTERN < 1270252124 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :if z^5=1 what is the value of z+2z^2+z^4 ? < 1270252200 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :apparentnyl it's always a rational, but it's not... < 1270252211 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :fax: What's the type of z? < 1270252225 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :complex number < 1270252231 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :complex real* < 1270252290 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I think -1=(z^2+z^4)+(z^3+z^1)=x1 + x2 should mean that x1*x2 is a rational < 1270252377 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: HAWT < 1270252413 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :It's a good thing Gore created the Internet instead of Clinton, or it would have been the Intern-net *BA-DUM CHING BAD JOKE* < 1270252418 0 :pikhq!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270252530 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Data.Complex> [z+2*z^2+z^4 | let r = mkPolar 1 (pi*2/5) , z <- map (r^) [0..4]] < 1270252550 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :[4.0 :+ 0.0,(-1.0) :+ 1.17557050458495,(-1.0) :+ (-1.90211303259031),(-0.999999999999999) :+ 1.90211303259031,(-1.0) :+ (-1.17557050458495)] :: [Complex Double] < 1270252577 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::S < 1270252584 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what about z^2+z^3? < 1270252610 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Data.Complex> [z^2+z^3 | let r = mkPolar 1 (pi*2/5) , z <- map (r^) [0..4]] < 1270252610 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :[2.0 :+ 0.0,(-1.61803398874989) :+ 1.11022302462516e-016,0.618033988749895 :+ (-1.11022302462516e-016),0.618033988749895 :+ (-1.11022302462516e-016),(-1.61803398874989) :+ 2.22044604925031e-016] :: [Complex Double] < 1270252626 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :seems to be real < 1270252630 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what the hell < 1270252636 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270252645 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :z^2 is the conjugate of z^3 < 1270252666 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ooh < 1270252668 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :since they're inverses and on the unit circle < 1270252690 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so it's really just Re (2*z^2) < 1270252697 0 :pikhq!~pikhq@75-106-123-198.cust.wildblue.net JOIN :#esoteric