00:00:05 -!- oerjan has joined.
00:02:00 -!- Gregor has set topic: 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.
00:06:08 -!- FireFly has quit (Quit: Leaving).
00:14:01 -!- mibygl has joined.
00:14:19 * mibygl generates a text file containing ten web sites' Terms of Service.
00:14:44 * mibygl delimits them with "bork bork bork bork bork"
00:20:41 -!- augur_ has joined.
00:21:18 -!- augur has quit (Read error: Connection reset by peer).
00:21:24 <mibygl> Now I'd like to generate a three-word Markov chain out of this.
00:23:36 <mibygl> I guess three words is too much to ask, so I'm generating a seven-character one instead.
00:24:04 <mibygl> Since the average word contains one and a third characters.
00:27:13 <oerjan> ancient inca god of markov chains
00:32:22 -!- adam_d_ has quit (Ping timeout: 265 seconds).
00:37:19 <mibygl> "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"
00:45:50 -!- augur_ has quit (Ping timeout: 246 seconds).
00:49:34 <mibygl> 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.
00:58:55 <AnMaster> <Gregor> (Sony investigating the PS3 date bug) <-- link?
00:59:16 <oerjan> that's some nice timing
01:04:46 <oerjan> AnMaster: try reloading now
01:05:25 <AnMaster> oerjan, I got the old version still
01:23:34 <mibygl> Wow, it's surprisingly difficult to create a user from the command line in OS C.
01:23:55 <mibygl> I can't believe that in the 90 versions they've released since OS X, they still haven't fixed that.
01:26:05 <AnMaster> <mibygl> 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 .
01:36:17 -!- Asztal has quit (Ping timeout: 248 seconds).
01:42:01 -!- augur has joined.
02:14:21 -!- augur has quit (Ping timeout: 265 seconds).
02:27:26 -!- augur has joined.
02:32:43 -!- augur has quit (Ping timeout: 265 seconds).
02:34:46 -!- adu has joined.
03:05:00 -!- mibygl has quit (Ping timeout: 252 seconds).
03:11:51 -!- augur has joined.
03:19:27 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
03:40:36 -!- jcp has joined.
03:51:21 -!- augur_ has joined.
03:51:42 -!- augur has quit (Read error: Connection reset by peer).
04:01:30 -!- Oranjer has left (?).
04:04:33 -!- augur_ has quit (Ping timeout: 265 seconds).
04:07:57 -!- oerjan has quit (Quit: Good night).
04:42:00 <Sgeo_> Got a wireless mouse!
04:51:42 <Sgeo_> Feels a bit fast though
04:52:01 <Sgeo_> And randomly nonworky
05:10:37 -!- charlls has joined.
05:33:04 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
05:52:56 -!- jcp has joined.
05:57:04 -!- augur has joined.
06:40:14 -!- kar8nga has joined.
06:57:24 <Sgeo_> No one minds if I mutter to myself in the channel, right?
06:58:27 <Sgeo_> 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]
06:59:12 <Sgeo_> 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
06:59:23 <Sgeo_> Names do not have to be unique
07:00:46 <Sgeo_> 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
07:01:22 <Sgeo_> However, if an object receives a signal, by itself it can't decide "if this I'll do this, otherwise I'll do that"
07:01:38 <Sgeo_> However, names can be changed, and not just by sending and receiving signals
07:01:54 <Sgeo_> I have too much of a headache to think about all of this. I should really just sleep.
07:23:00 -!- MizardX has quit (Ping timeout: 276 seconds).
07:38:22 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
07:54:32 -!- kar8nga has quit (Remote host closed the connection).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:07:08 -!- lament has quit (Ping timeout: 240 seconds).
08:10:02 -!- lament has joined.
08:21:35 -!- adam_d has joined.
08:48:20 -!- augur has quit (Remote host closed the connection).
08:54:45 -!- adu has quit (Quit: adu).
09:02:36 -!- augur has joined.
09:37:21 -!- lereah_ has joined.
09:51:46 -!- FireFly has joined.
10:02:25 -!- Asztal has joined.
10:12:27 -!- alise has joined.
10:14:07 <alise> 14:31:55 <Sgeo> This is the Epigram language?
10:14:26 <alise> 15:04:05 <oerjan> AnMaster: it's April 2 now
10:14:34 <alise> Then you are very late: 12 am is the end of the fools.
10:16:47 <alise> A dark delimitation.
10:21:36 <alise> so hey, |Sigma x:T, P| = sum x:T, P
10:21:52 <alise> this is i think one of my favourite isomorphisms ... |x op y| = |x| op |y|
10:30:56 <alise> although since we're talking type theory and have no |.| :: Type -> Cardinality
10:30:56 <alise> it's actually more involved
10:30:56 <alise> like |a+b|=|a|+|b| is actually
10:30:56 <alise> hc(a,n) -> hc(b,m) -> hc(a+b, n+m)
10:30:56 <alise> where hc = "has cardinality"
10:30:57 <alise> for instance the statement about sigma would require some sort of function
10:31:11 <alise> ((y:T) -> hc(P[x := y], something))
10:31:22 <alise> where x[y:=z] is variable substitution
10:34:36 <alise> oklopol: but err you know the type theory notation in general right?
10:34:42 <alise> like a+b is Either a b
10:34:57 <alise> a*b is -- cartesian product here -- a pair of a and b (cardinality |a|*|b|)
10:35:26 <alise> (non-dependent) a -> b has cardinality |b|^|a|, but using b^a for that like in set theory is ugly
10:35:32 <alise> because, you know, we like our functions
10:35:40 <alise> and having it all in hugely nested superscripts would be silly
10:36:26 <alise> i wonder what the cardinality of Pi (x:T). S is...
10:36:57 <alise> product (x:T), |S|? if so that would be so perfect
10:37:11 <alise> say cardinality of 3 -> 3
10:37:26 <alise> |3| = 3, obviously
10:38:07 <oklopol> Pi (x:T). S is basically a definition of TxS where i live
10:39:34 <alise> oklopol: yeah but S can include x
10:40:05 <alise> refl : Pi (T : *). Pi (x : T). x = x
10:40:31 <alise> * is type of types smaller than *... I don't want to think about its cardinality right now
10:40:53 <alise> but for a given type T, Pi (x : T). x = x has the cardinality of T...
10:40:55 <alise> but you could have more complex things
10:41:10 <alise> Pi (x : N). Pi (y : N). x = y -> ()
10:41:13 <alise> remember -> is shorthand for Pi so
10:41:20 <alise> Pi (x : N). Pi (y : N). Pi (_ : x = y). ()
10:41:33 <alise> now of course this is the same as Pi (x : N). ()
10:41:34 <oklopol> and to continue my sentence ...it's S^T
10:41:48 <alise> so it certainly isn't the obvious thing
10:42:06 <alise> well not the number
10:42:10 <alise> because it has one value
10:43:59 <alise> \prod_{E:n=m} -- there's only ever 1 or 0 values of type n=m
10:44:53 <oklopol> Pi (x : T). x = x <<< what does this mean, the type of functions that ...?
10:45:11 <oklopol> sorry about the asynchronicity, i'm doing two things at once and i suck at it.
10:45:51 <alise> Pi (x:T).S is like T->S, but the value of the T is bound to x in S
10:46:08 <alise> its cardinality is product (x:T). S which is fitting because the tw are the same notation
10:46:12 <alise> which is just this isomorphism again
10:47:00 <oklopol> so in Pi (x : T). x = x what does = x mean
10:47:44 <oklopol> obviously the cardinality of Pi (x : T). x is 1
10:47:47 <alise> x = x is just nice notation for Eq x x
10:48:00 <alise> for all values x and y of the same type Eq x y is a type
10:48:16 <alise> (it has a more complicated type but ... that is the relevant parts)
10:48:19 <alise> (the rest is just type stuff)
10:48:32 <alise> so if we have a value of type x = y, we know that x and y are completely indistinguishable...
10:48:37 <alise> it's just equality
10:49:01 <alise> so we have m,n : N, and we know that m = n
10:49:03 <alise> so the two must be exactly the same
10:49:10 <alise> so we have \x. f x x refl
10:49:18 <alise> which is exactly the same as f, just with less stupid arguments
10:49:23 <alise> http://1.618034.com/blog_data/math/formula.3405.png
10:49:54 <alise> so the cardinality of functions (n:N) -> (m:N) -> n = m -> ()
10:49:59 <alise> is the same as the cardinality of the naturals
10:50:18 <alise> because the only function of type N -> () is \_.()
10:50:28 <oklopol> Pi n : N . 1 has cardinality |N|?
10:50:35 <alise> the last bit is wrong
10:50:52 <alise> http://1.618034.com/blog_data/math/formula.3406.png
10:50:59 <alise> because 1*1*1*1*... = 1
10:51:16 <alise> note the bold 1 in the |...| denotes the type with one value, tt : 1
10:51:23 <alise> the non-bold 1s are just the regular number 1
10:51:36 <alise> also the product in the |...| denotes dependent functions...
10:51:43 <alise> whereas after it's normal numbery products
10:52:07 <oklopol> so say n : N, then Eq n n is a type? what values are of that type?
10:53:05 <alise> let me just give you the definition in pseudohaskell
10:53:28 <alise> data Eq : forall a, a -> a -> Type where
10:53:37 <alise> refl :: a -> Eq a a
10:53:45 <alise> refl :: (x:a) -> Eq x x
10:54:29 <alise> http://1.618034.com/blog_data/math/formula.3407.png
10:54:33 <alise> generalised for non-1 result types
10:54:48 <oklopol> 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
10:54:54 <alise> note that if T = Bool, |T| = 2, so we have 2^N_0, which is the cardinality of the reals...
10:55:00 <alise> actually they're the computable reals for us, but
10:55:17 <alise> if x is of type a, and y is of type a, then Eq x y is a type
10:55:31 <alise> when I restate things it's because you said something that was wrong
10:55:42 <oklopol> x:a -> Eq x x is a type is just a special case of that
10:55:49 <alise> that isn't even true
10:55:53 <alise> that isn't even remotely correct
10:55:56 <alise> Eq :: (A : Type) -> A -> A -> Type
10:56:05 <alise> refl :: (A : Type) -> (x : A) -> Eq x x
10:56:11 <alise> one is a type one is a value
10:56:15 <oklopol> "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
10:56:18 <alise> and Eq x y is a type for ALL x and y
10:56:24 <alise> oklopol: but it's IMPORTANT
10:56:29 <alise> because if they had to be the same it would be a useless type
10:56:31 <oklopol> and i get "if x is of type a, and x is of type a, then Eq x x is a type"
10:56:46 <oklopol> IT'S A FUCKING USELESS TYPE ANYWAY BECAUSE YOU HAVEN'T TOLD ME WHAT IT CAN CONTAIN
10:56:51 <oklopol> god you suck at explaining things
10:56:53 <alise> <alise> refl :: (A : Type) -> (x : A) -> Eq x x
10:56:56 <alise> I have; several billion times.
10:57:08 <oklopol> i'll ask fax at some point
10:57:17 <alise> 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.
10:57:23 <alise> refl does not return a type.
10:57:26 <alise> It returns a value of type Eq x x.
10:57:34 <alise> So is Eq, actually, because types are values. But.
10:57:58 <alise> So we have Eq x y, but only Eq x x is inhabited.
10:58:05 <alise> All the rest are uninhabited, so we can't prove (give a value) them.
11:03:31 <oklopol> yeah okay i see what Eq is now, the haskell does indeed explain it completely
11:04:26 -!- tombom has joined.
11:05:32 <oklopol> so Eq x y is inhabited by ":)" if x = y, otherwise there's no value of that type
11:06:05 <alise> except it's refl not :)
11:06:15 <alise> so obviously if we have m,n:N and m=n, m and n are completely redundant
11:07:49 -!- MigoMipo has joined.
11:35:26 <AnMaster> <alise> 15:04:05 <oerjan> AnMaster: it's April 2 now
11:35:26 <AnMaster> <alise> Then you are very late: 12 am is the end of the fools. <-- ?
11:35:42 <alise> Oh; perhaps it is only UK tradition.
11:35:51 <alise> It certainly is but I assumed it was so elsewhere too.
11:35:55 <AnMaster> I never heard of it before at least.
11:36:06 <alise> Well, it has fallen out of favour in this interblaggy world.
11:36:15 <AnMaster> I thought it went on for the whole day
11:50:40 -!- BeholdMyGlory has joined.
11:58:46 -!- MigoMipo has quit (Quit: Konversation terminated!).
11:59:59 -!- MigoMipo has joined.
12:01:49 -!- MigoMipo has quit (Remote host closed the connection).
12:03:32 -!- MigoMipo has joined.
12:12:26 -!- BeholdMyGlory has quit (Quit: Leaving).
12:12:59 -!- BeholdMyGlory has joined.
12:38:57 -!- oerjan has joined.
12:40:50 -!- kar8nga has joined.
12:54:49 -!- MigoMipo has quit (Remote host closed the connection).
13:05:36 -!- kar8nga has quit (Remote host closed the connection).
13:06:38 -!- alise has quit (Ping timeout: 258 seconds).
13:29:32 -!- alise has joined.
13:34:38 -!- oerjan has quit (Quit: leaving).
13:36:12 -!- Tritonio_GR has quit (Read error: Connection reset by peer).
13:47:26 -!- Asztal has quit (Ping timeout: 265 seconds).
14:18:58 <AnMaster> 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.
14:21:08 -!- Sgeo_ has quit (Read error: Connection reset by peer).
14:21:41 -!- Sgeo has joined.
14:39:53 <alise> You can access /my/ secure hole hur hur.
14:46:25 * Sgeo wonders how legal it would be to make a language based on the Active Worlds action line stuff
14:51:32 <AnMaster> 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."
14:52:03 <AnMaster> alise, grandma, what a big back you have!
14:52:23 <alise> ALL THE BETTER TO LAY YOU WITH
14:52:42 <alise> I had no idea I was so awesome
14:52:46 <alise> AnMaster: Of course it was!
14:53:09 <AnMaster> as I thought to begin with then
14:57:02 <AnMaster> 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)
14:57:28 <AnMaster> 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.
14:58:08 <AnMaster> (either that, or Japanese sounding names with an email @intel.com, that is fairly too)
14:59:39 <alise> Yeah; Standard Japanese Programmer English is a strange breed.
15:00:30 <alise> Japanese is very different from English.
15:00:40 <alise> And Engrish is ubiquitous in Japanese culture.
15:01:18 <AnMaster> what about Hollywood movies and such on TV?
15:03:00 <alise> They do everywhere else :-)
15:03:12 <AnMaster> generally they just add text lines at the bottom
15:03:15 <alise> Also I'd say that Japan imports less culture from other countries.
15:03:20 <alise> Probably because we're too busy importing all theirs.
15:04:56 <AnMaster> 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.
15:05:06 -!- lament has quit (Ping timeout: 260 seconds).
15:05:19 <AnMaster> In Sweden only movies aimed at children are generally dubbed.
15:05:52 <alise> I suppose you strongly push English there.
15:06:02 <alise> Less so in Germany I would imagine.
15:06:08 <alise> Because people actually speak German ;-)
15:06:22 <alise> Anyway, shoulda pirated it!
15:06:29 <AnMaster> we do generally speak Swedish though :P
15:06:38 <AnMaster> alise, this was during the early 1990s iirc
15:06:45 <AnMaster> so well, that would have been fun
15:06:52 <alise> Hells yeah, ZMODEM!
15:07:31 <alise> "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, Frchet and Lebesgue. Both wrote letters rejecting the article. Frchet wrote that an implication between two well known truths is not a new
15:07:32 <alise> 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."
15:08:12 <AnMaster> AC is not alternating current here right?
15:09:58 -!- lament has joined.
15:11:24 * Sgeo wonders how someone who thought that one was the truth and the other was false would react
15:13:07 <alise> I am pretty sure that is trivially contradictory.
15:13:12 <alise> After all, they were proven to be equivalent.
15:13:21 <alise> So the rejection would be "LOL you made mistake"
15:13:29 <alise> Not "Nice paper, boy. It's shit."
15:17:20 <alise> 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.
15:18:01 -!- Sgeo_ has joined.
15:18:45 <AnMaster> alise, I think "LOL you made mistake" would be "somewhat" anachronistic in this case
15:19:07 <alise> STFU Cantor --Wittgenstein
15:19:33 <alise> Hilbert, you're a fag. Please commit program-suicide. --Godel
15:20:06 <AnMaster> alise, Pretty sure it was "Gödel"?
15:20:23 <AnMaster> and that should be transcribed as "Goedel" in English then, shouldn't it?
15:20:50 <alise> Yeah but nobody does.
15:20:57 <alise> lol - "Axiom of Life" = "~choice"
15:21:11 -!- Sgeo has quit (Ping timeout: 258 seconds).
15:21:15 <AnMaster> alise, that's what Hamlet said!
15:21:17 <alise> http://www.facebook.com/group.php?v=wall&gid=2243319629 group of idiots
15:21:49 <alise> well we know that 2b = 2*b
15:21:52 <alise> and as far as types go
15:22:05 <alise> (Bool,b) \/ ~(Bool,b)
15:22:12 <alise> if we interpret ~ as implication of falsehood
15:22:18 <alise> (Bool,b) \/ ((Bool,b) -> False)
15:22:34 <alise> so either you can construct a value of type (Bool,b) or you cannot
15:22:40 <AnMaster> what sort of strange syntax for "and" is (a,b)?
15:22:54 <alise> a*b = (a,b) in type theory
15:23:08 <AnMaster> alise, * is somewhat overloaded :P
15:23:17 <alise> and also cartesian product
15:23:37 <AnMaster> alise, is that * = multiplication for the last one?
15:23:39 <alise> plus it meshes well with disjoint union - a+b - |a+b| = |a|+|b|
15:23:48 <alise> if we do dependent tuples then we have
15:23:58 <AnMaster> wait, does that hold true for C? It doesn't, does it?
15:23:59 <alise> |sum x:T, P| = sum x:t, |P|
15:24:02 <alise> where P involves x
15:24:07 <alise> AnMaster: || is cardinality
15:24:24 <alise> |sum x:T, P| = sum x:t, |P| --- if P is constant, i.e. doesn't involve x
15:24:26 <AnMaster> alise, in "<alise> |a*b| = |a|*|b|" ?
15:24:28 <alise> then this is just |T|*|P|
15:24:43 <alise> so normal tuples are the degenerate case of dependent tuples
15:24:48 <alise> dependent function arrows:
15:24:48 <AnMaster> well the result is the same for abs() for R though
15:25:08 <alise> |prod x:T, S| = prod x:T, |S|
15:25:15 <alise> if we assume that S doesn't involve x
15:25:18 <AnMaster> but the overloaded syntax gets confusing
15:25:22 <alise> |S|*|S|*...|T| times...
15:25:37 <alise> we actually say the function arrow is S^T in set theory...
15:25:47 <alise> if we assume it involves x of course both of these are more complicated
15:25:59 <alise> AnMaster: exponentiation, obviously
15:26:24 <AnMaster> alise, not that obvious since most of the other syntax wasn't :P
15:26:38 <alise> well it is not my fault you don't know type theory :)
15:26:53 <alise> but sum/product types ar enamed that way because they're basically identical
15:27:07 <alise> they're how you['d define addition/multiplication on things like sets if you had to
15:27:12 <AnMaster> alise, It is just that I get confused when the line is possible to interpret sensibly as more than one thing
15:27:16 <alise> addition is obviously union - you add all the elements together
15:27:28 <alise> AnMaster: learn to disambiguate based on context
15:28:24 <AnMaster> alise, well, then ^ could have been XOR as well, not that likely but...
15:29:02 <alise> Incredibly unlikely - because |S|*|S|*...|T| times is obviously |S|^|T|.
15:41:04 -!- Sgeo_ has changed nick to Sgeo.
15:45:52 -!- lereah_ has quit (Quit: Leaving).
15:55:35 <alise> I wish oerjan was here
15:58:53 <Sgeo> Don't know when
16:05:35 <alise> Axiom func : nat -> (nat -> bool).
16:05:36 <alise> Axiom surj : forall f, exists n, forall x, func n x = f x.
16:05:39 <alise> oerjan was right, obviously
16:05:44 <alise> just felt like formalising it...
16:06:47 <Sgeo> I take it to mean that that either at least one of those axioms is self-contradictory, or they contradict eachother
16:07:11 <Sgeo> Wait, surj uses func
16:08:45 -!- MigoMipo has joined.
16:08:58 <alise> Sgeo: it's basically just one axiom
16:09:11 <alise> if we have a surjective mapping from naturals to functions from naturals to booleans, we're fucked
16:09:20 <alise> there are more functions from naturals to booleans than there are naturals
16:09:59 <alise> Informal proof, due to oerjan: Say the mapping is called magic. Consider f n := not (magic n n).
16:10:10 <alise> This is a function nat -> bool.
16:10:21 <alise> We know that for every function nat -> bool, there is a natural number n such that magic n = that function.
16:10:22 * Sgeo tries to understand what surjective means, based on the code. /me fails
16:10:31 <alise> Sgeo: simply the above
16:10:37 <alise> Call f's magic number fn.
16:10:43 <alise> Now consider (f fn).
16:10:47 <alise> = not (magic fn fn)
16:10:50 <alise> magic fn = f, so this is
16:10:59 <alise> So, f fn = not (f fn).
16:11:03 <alise> Contradiction. Q.E.D.
16:11:55 <alise> 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
16:12:06 <alise> otherwise our nat -> (nat->bool) mapping could just be
16:12:56 <alise> Sgeo: incidentally the axiom of choice is about surjective functions
16:13:18 <alise> it states that every surjective function has a right inverse
16:13:23 <alise> or rather is equivalent to such
16:13:27 <Sgeo> "right" inverse?
16:13:58 <alise> 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
16:15:39 <alise> 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
16:16:06 <alise> I had to define not myself - it seems Coq doesn't have it for booleans.
16:16:31 <alise> Then the proof just went by picking out what surj says about our f - that func n x = f x
16:16:46 <alise> then expanding this to not x = x
16:17:08 <alise> here's the steps as it goes:
16:17:11 <alise> after the destruction:
16:17:14 <alise> H : forall x0 : nat, func x x0 = notb (func x0 x0)
16:17:14 <alise> ============================
16:17:20 <alise> after the notdistinct:
16:17:22 <alise> H : forall x0 : nat, func x x0 = notb (func x0 x0)
16:17:23 <alise> ============================
16:17:23 <alise> func x x = notb (func x x)
16:17:27 <alise> then I just apply H and tada
16:17:35 * Sgeo needs to learn Coq before attempting to understand this
16:17:41 <alise> (we apply notdistinct because (b <> notb b) is shorthand for (b = notb b) -> False)
16:17:51 <alise> (so if we apply it, Coq realises we need to prove (b = notb b) to achieve our goal of False).
16:18:02 <alise> (which we can do: because surj tells us it is so)
16:18:25 <alise> Sgeo: This also suffices as a proof that the reals are more numerous than the naturals, btw.
16:18:52 <alise> Consider a real number as an infinite string of binary bits (it can just end in 0s if it isn't "really" infinite)
16:18:58 <alise> (nat -> bool) - f n is the bit at position n
16:19:03 <Sgeo> Reals can be treated as functions from .. ah
16:19:08 <alise> so (nat -> bool) ~~ real
16:19:17 -!- jcp has joined.
16:19:24 <alise> so the proof says that we cannot define a function from naturals to reals such that every real has a corresponding rational
16:19:28 <alise> so the proof says that we cannot define a function from naturals to reals such that every real has a corresponding naturla
16:20:27 -!- lament has quit (Remote host closed the connection).
16:27:23 -!- MizardX has joined.
16:49:30 -!- MigoMipo has quit (Remote host closed the connection).
17:14:31 <alise> /home/ehird/code/univ.agda:16,8-11
17:14:32 <alise> □∏_ is not strictly positive, because it occurs in the 5th clause
17:14:33 <alise> in the definition of □_, which occurs in the first argument to □∏_
17:14:33 <alise> in the 5th clause in the definition of □_, which occurs to the left
17:14:33 <alise> of an arrow in the type of the constructor all in the definition of
17:14:38 <alise> AnMaster: You'd like Agda; it has nice error messages!
17:14:45 <alise> Now to figure out what that perfectly well-formed English is trying to tell me.
17:21:43 <alise> You have me on Monday, too - such a special week's end this is.
17:27:50 <alise> I was here yesterday, too: but I was too tired to come here.
17:27:54 <alise> I was on my iPhone here, though.
17:36:02 -!- adam_d has quit (Ping timeout: 265 seconds).
17:49:32 -!- ais523 has joined.
17:51:42 <alise> AnMaster: it's the magical box of interpretation (I probably should have used brackets)
17:51:58 <pikhq> ... Man. Microsoft *still* gets buffer overflows.
17:52:13 <ais523> pikhq: I'm not surprised, that's inherent in C
17:52:20 <ais523> that it's hard to check for them
17:52:28 <pikhq> ais523: Not really. It's inherent in bad programmers for C.
17:52:30 <ais523> in theory, Splint can statically prove a program has no buffer overflows, but it's not very good at it
17:52:33 <AnMaster> ais523, you can avoid such data structures when possible
17:52:55 <AnMaster> of course for a binary stream there isn't any good alternative
17:53:03 <pikhq> I'd say that any programmer bad enough to do that sort of thing shouldn't be allowed to touch C when working.
17:53:15 <AnMaster> (and C doesn't really help with providing other good data structures)
17:54:12 <AnMaster> anyway, why this? Has there been a new windows exploit recently or what?
17:54:29 <pikhq> Nah, reading about how they've started doing... Fuzz testing.
17:55:27 <pikhq> And seeing bunches of buffer overflows in office.
17:56:05 <ais523> pikhq: in binary formats, or XML formats?
17:56:32 <pikhq> As it's the latest version of Office, I'm going to guess "both".
17:57:11 <ais523> buffer overflows in XML is just embarrassing
17:57:14 <AnMaster> fuzz testing can be very useful
17:57:42 * AnMaster remembers finding div by zero errors in both cfunge and ccbi early on using a fuzz tester
17:58:01 <pikhq> AnMaster: What's surprising is that they only started doing it.
17:58:07 <AnMaster> of course, such code isn't very good at finding anything but crash bugs, and only ones that aren't extremely complex to trigger
17:58:56 <ais523> hmm, I wasn't online yesterday
17:59:02 <ais523> any good April Fool's stuff I should look at?
17:59:34 <AnMaster> ais523, google used microweeks amongst other things to measure how long searches took
17:59:56 <Sgeo> One good, the other mine
18:00:13 <alise> pikhq: Programming in C is nearly impossible for a human!
18:00:18 <AnMaster> ais523, gigawatts, parsecs, "shakes of a lamb's tail" and Planck times were used too
18:00:27 <ais523> seems surprisingly uncreative for Google
18:00:30 <AnMaster> ais523, oh and the RFC was quite funny too
18:00:33 <AnMaster> ais523, they did other ones too
18:00:40 <Sgeo> ais523, you mean Topeka, right?
18:00:44 <ais523> what was the RFC this time?
18:00:58 <AnMaster> ais523, maps.google.com.au, did directions in Australian slang
18:01:05 <pikhq> alise: I can do it. For many cases not involving stack munging.
18:01:11 <pikhq> (getcontext et al scares me)
18:01:16 <alise> pikhq: Yeah, with what error rate?
18:01:24 <Sgeo> Google was renamed to Topeka
18:01:26 <AnMaster> ais523, oh and the Topeka stuff too yeah
18:01:38 <Sgeo> YouTube videos had a TEXTp option
18:01:49 <Sgeo> [not Google] Reddit made everyone an admin
18:01:53 <AnMaster> Sgeo, never got that working, was it flash only?
18:01:55 <Sgeo> Fark headlines were acrostics
18:01:59 <Sgeo> AnMaster, I.. guess
18:02:01 <ais523> also, that reddit thing sounds like utter chaos
18:02:09 <AnMaster> Sgeo, as in, couldn't get the html5 stuff to work for it.
18:02:22 <Sgeo> AnMaster, I imagine it might be Flash only
18:02:23 <pikhq> alise: Lower than you'd expect, actually.
18:02:32 <alise> pikhq: I doubt that highly :)
18:02:39 <pikhq> When using getcontext, nearly 100%. :P
18:02:39 <Deewiant> ais523: I think the admin-mode changes were local-only
18:02:58 <Sgeo> The admin stuff including infinite upvotes/downvotes
18:03:01 <pikhq> (which leads me to suspect that I should never, ever touch that.)
18:03:09 <AnMaster> ais523, the RFC was about a tcp option to mark packet mood
18:03:21 <ais523> hmm, as in you could perform admin actions but reddit faked the result rather than actually doing it?
18:03:30 <AnMaster> ais523, mood would be encoded as a string of ASCII chars making up a smiley
18:03:35 <Sgeo> ais523, and stored the result per user, I think
18:03:44 <AnMaster> (don't remember if IANA were supposed to assign them or not)
18:03:55 <Sgeo> [unless you changed your own headline, I think]
18:03:56 <Deewiant> 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
18:04:07 <ais523> and putting unreasonable registration requests onto IANA is standard with April Fools' RFCs, IIRC
18:04:10 <AnMaster> ais523, anyway: http://tools.ietf.org/html/rfc5841
18:04:36 <alise> ais523: haha, that's great
18:04:39 <Sgeo> ais523, check Agora?
18:05:09 -!- adam_d has joined.
18:05:13 <ais523> Sgeo: the first one where you submitted half the proposal is much funnier, given what happened to Nomicapolis
18:05:35 <AnMaster> <alise> pikhq: Programming in C is nearly impossible for a human! <-- hm. That raises some interesting questions about Kernighan and Ritchie....
18:05:41 <Sgeo> What happened to Nomicapolis?
18:06:30 <ais523> Sgeo: there was an attempt to copy B's ruleset to it, but accidentally only the first half was copied
18:06:39 <ais523> and the resulting ruleset didn't allow rule changes
18:06:44 <alise> AnMaster: They can't manage it either, they just only publish their successes
18:06:55 <ais523> AnMaster: see above, it's me who was asking rather than answering
18:07:11 <alise> In fact almost all existing programming languages are completely infeasible for programming which is why we have so many bugs.
18:07:19 <Sgeo> That does make the accidental post funny
18:07:24 <AnMaster> 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
18:07:30 <alise> 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.
18:07:30 <ais523> AnMaster: they made everyone an admin
18:07:40 <ais523> or at least, to think they were, according to what I was told earlier in this channel
18:07:48 <ais523> this is all second-hand info, though, and the people who actually told me are still here
18:07:53 <ais523> which is why I'm confused as to why you're asking me
18:07:55 <pikhq> alise: ButbutPOINTERS ARE MORE EFFICIENT
18:08:05 <Sgeo> There was a "turn admin on" link for logged in users
18:08:20 <Sgeo> It made an [A] thingy appear next to other user's name
18:08:30 <Sgeo> Which gave options like ban, x-ban
18:08:33 <alise> AGDA I AM CONFUSED
18:08:51 <Sgeo> It randomly did things like 16.14% shill account
18:08:59 <Sgeo> Let you "edit" headlines
18:09:30 <Sgeo> Upvote and downvote a single thing repeatedly. 10 or more repeated upvotes (not sure if it was 10) made it an upvote to infinity
18:09:38 <Sgeo> Similar in the other direction
18:09:56 <Sgeo> I might be forgetting some stuff
18:10:15 <ais523> personally, I think a language which is C + a proof that it doesn't contain buffer overflows, null pointer derefs, etc. is entirely feasible
18:10:24 * ais523 continues to be annoyed at Splint
18:10:33 <ais523> for purporting to do exactly what I want, and failing at it
18:10:49 <alise> Repeated variables in left hand side: n
18:10:52 <alise> I know Agda, god damn!
18:11:01 <AnMaster> 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.
18:11:16 <Sgeo> Watching Ark of Truth now
18:11:56 <alise> How the hell do you do dependent pattern matching in this thing?
18:12:06 <alise> head (witness (S n) f) (successor n) = ?
18:12:09 <alise> complains about repeated ns
18:12:17 <AnMaster> 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.
18:12:33 <ais523> AnMaster: even without parse errors, some of its decisions are just bizzare
18:12:43 <alise> sjgdflkgjdfhdklgfhg
18:12:54 <AnMaster> 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
18:12:57 <ais523> 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)
18:13:33 <Deewiant> ais523: Well, lint-type things tend to be about style as much as semantics
18:13:38 <AnMaster> ais523, what is it that it warns about then?
18:13:45 <ais523> AnMaster: my guess is, it's just wrong
18:13:57 <ais523> I can't see any explanations for that behaviour other than a bug in Splint
18:14:04 <AnMaster> ais523, if it is just about indention style or something like that, it seems reasonable
18:14:14 <AnMaster> and yes, splint is buggy and unmaintained
18:14:34 <ais523> AnMaster: no, it was about memory leaks
18:15:22 <Deewiant> Well that's a bit messed up, isn't it :-P
18:16:29 <AnMaster> I found clang in static analyser mode moderately useful btw. Doesn't detect a lot of stuff yet and somtimes it "crashes"
18:16:34 <AnMaster> Not as in coredump, but as in assert(0 && "Message that only makes sense to a LLVM developer").
18:17:08 <AnMaster> (they seem to love assert(0 && "string") btw)
18:17:23 <Deewiant> Would you prefer assert(!"string")? :-P
18:18:10 <AnMaster> Deewiant, I would prefer never seeing either when running the program :P
18:18:16 <alise> I HAAAAAAAAAAAATE THIS
18:18:24 <Deewiant> But you can't have everything :-P
18:20:07 <AnMaster> 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...
18:20:40 <AnMaster> 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...
18:22:16 <AnMaster> alise, very precise description that
18:23:06 <AnMaster> Deewiant, so you stated that I can't have everything without having any good explanation for why that is the case?
18:23:50 <Deewiant> It seems to be the way the world works
18:24:02 <Deewiant> I can't justify why the world works that way
18:24:39 <AnMaster> hm I first considered asking "why not" to that as well, but that would have been silly
18:28:25 <ais523> 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
18:29:04 -!- Oranjer has joined.
18:32:34 <ais523> Alex Brown deciding that OOXML is doomed to failure seems to be not an april fool's joke, though
18:32:55 <ais523> and that's the same sort of event as Miguel de Icaza noticing that Mono has an unclear patent situation
18:36:20 <Sgeo> "You have watched 72 minutes of video today."
18:41:34 -!- MigoMipo has joined.
18:49:20 -!- Oranjer has left (?).
18:54:42 -!- alise has quit (Ping timeout: 258 seconds).
19:00:25 * Sgeo wants to experiment with unsafeInterleaveIO
19:06:12 <Sgeo> Deferrs the IO operation until the value it gives is needed
19:06:20 <Sgeo> Haven't actually tried it yet
19:06:45 <AnMaster> 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...
19:07:10 <ais523> so presumably it only works on input?
19:07:43 <AnMaster> 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)
19:07:45 <Sgeo> 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
19:07:48 <Sgeo> That's what I'm testing
19:08:12 <Sgeo> I'll paste the results
19:08:26 <AnMaster> ais523, I assume you will be able to explain this
19:08:38 <Ilari> AnMaster: Your hand scatters/reflects more of the signal?
19:08:47 <ais523> AnMaster: probably you're reflecting the signal
19:08:57 <ais523> human skin is pretty reflective wrt microwaves
19:09:06 <AnMaster> ais523, it doesn't work unless I actually touch the plastic on the lid though
19:09:41 <Ilari> -90dBm is 1pW and -79 dBm is ~12.6pW... So about tenfold difference...
19:10:01 <AnMaster> if I hold my hand slightly away (a few mm I guess, hard to measure), I get the bad signal
19:11:46 <AnMaster> oh btw, what does the m stand for in dBm?
19:12:13 <fizzie> The "m" there denotes the reference power is 1 mW.
19:12:16 <Ilari> AnMaster: dB relative to mW. That p was supposed to be multiplier for 10^-12...
19:12:35 <ais523> Ilari: why convert? 10 dBm is a tenfold difference
19:12:39 <ais523> you don't need to convert back into watts
19:13:48 <Ilari> AnMaster: 0dBm => 1mW
19:14:08 <Sgeo> ais523, http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24603#a24603
19:14:20 <AnMaster> hm, wlan signals are _extremely_ weak then...
19:14:30 <fizzie> AnMaster: Yes, dB is a dimensionless unit; -90 dB could be anything, as long as it is 10^-9 of something.
19:14:41 <Ilari> dBm is the only case I have seen where unit used as reference is not written completely (there's dBV, dBW, etc...)
19:14:47 <ais523> Sgeo: ah, it didn't work?
19:14:56 <Sgeo> ais523, it worked perfectly!
19:15:10 <Sgeo> It only did the interleaved one when it was needed
19:15:18 <ais523> oh, I didn't notice the first wasn't interleaved
19:15:45 <fizzie> 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.
19:15:47 -!- alise has joined.
19:16:08 <AnMaster> fizzie, isn't dB basically "the range we want is awkwardly large, lets use something logarithmic"? ;P
19:16:16 <Sgeo> alise, I'm in love with unsafeInterleaveIO
19:16:53 <alise> Sgeo: it is as unsafe as the name suggests.
19:17:14 <alise> Sgeo: it breaks Haskell's purity
19:17:22 <pikhq> It is somewhat less unsafe than unsafePerformIO, but still unsafe.
19:17:26 <AnMaster> though I wrote that above... seems I only thought it
19:17:35 <alise> getContents is acceptable in small utilities but not large programs.
19:17:53 <pikhq> Sgeo: It means that you can suddenly have errors occuring in any function.
19:17:58 <ais523> presumably, because if you use it twice it might only run once
19:18:01 <AnMaster> what does the "interleave" in it signify?
19:18:02 <alise> Sgeo: Because it breaks Haskell's purity.
19:18:09 <alise> Why not just use unsafePerformIO if you don't care about that?
19:18:14 <Sgeo> I meant, how does it break Haskell's purity?
19:18:16 <ais523> oh, that's unsafePerformIO
19:18:17 <alise> AnMaster: basically it splits off a lazy thread of IO
19:18:17 <pikhq> AnMaster: Side effects are interleaved with pure code.
19:18:29 <alise> so unsafeInterleaveIO (... read a file byte by byte)
19:18:32 <alise> produces a lazy string of the whole file
19:18:33 <Ilari> Satellite signals are usually extremely weak. That's why one usually sees modulations that have low SNR requirement (like QPSK).
19:18:36 <alise> only read as required by evaluation
19:19:02 <alise> consider an unsafePerformIO call that does output
19:19:02 <alise> then random pure code could cause unpredictable output
19:19:06 <alise> depending on the evaluation semantics of the implementation
19:19:09 <alise> all haskell specifies is non-strict
19:19:17 <pikhq> Sgeo: getContents >>= return foo -- You get errors in foo.
19:19:25 <AnMaster> pikhq/alise: and the "perform" in the other one signifies that it isn't lazy then I guess?
19:19:46 <alise> AnMaster: unsafeInterleaveIO :: IO a -> IO a
19:19:53 <alise> unsafePerformIO :: IO a -> a
19:19:59 <alise> unsafeInterleaveIO is just return (unsafePerformIO x)
19:20:08 <alise> unsafePerformIO is, of course, an abomination of the highest order.
19:20:10 <Sgeo> Wait, what's that in do notation? do { a <- getContents; return a}
19:20:21 <AnMaster> alise, ouch, unsafeInterleaveIO seems very nasty
19:20:25 <AnMaster> why does haskell even have it?
19:20:29 <alise> do {a <- getContents; return foo }
19:20:32 <alise> where foo is a pure expression
19:20:47 <alise> AnMaster: because it is useful: consider interact :: (String -> String) -> IO ()
19:20:59 <alise> interact f = do s <- getContents; putStr (f s)
19:21:06 <alise> AnMaster: getContents lazily returns all of stdin
19:21:08 <alise> this is convenient
19:21:12 <alise> it is a hack - but it is convenient
19:21:13 <pikhq> AnMaster: unsafeInterleaveIO is useful for various small utilities.
19:21:15 <alise> so the answer is convenience
19:21:32 <Sgeo> 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?
19:21:37 <AnMaster> are the usual "safe" IO facilities implemented using these unsafe ones internally?
19:21:57 <pikhq> AnMaster: No, the unsafe ones are done in terms of the safe ones.
19:22:11 <alise> AnMaster: Neither.
19:22:13 <alise> pikhq: that's nonsensical
19:22:19 <AnMaster> pikhq, err. It isn't 1 April any more...
19:22:23 <Sgeo> alise, maybe pikhq was being sarcastic?
19:22:25 <alise> AnMaster: unsafePerformIO is just an internal thing that hacks around with the uber-internal IO data structure.
19:22:28 <alise> The default IO operations are primitives.
19:22:40 <alise> The IO data structure is not exposed unless you import internal GHC modules.
19:22:49 <pikhq> alise: getContents is done in terms of unsafeInterleaveIO and 'safe' IO operations. My statement of this came out confused.
19:22:54 <Sgeo> Is my unterstanding correct?
19:23:07 <alise> it's more insidious but that is one special case
19:23:18 <Sgeo> Examples of insidiousness please?
19:23:39 <AnMaster> alise, hm what language is the io primitives implemented in?
19:23:48 <AnMaster> it would be neat if it was haskell
19:23:56 <pikhq> AnMaster: They're part of the Haskell runtime, I'm pretty sure.
19:24:03 <pikhq> Erm. Part of the GHC runtime.
19:24:08 <pikhq> The one bit of GHC that's not in Haskell.
19:24:11 <alise> AnMaster: what pikhq said
19:24:14 <alise> although the IO data structure is defined in haskell
19:24:20 <alise> and GHC itself is written in haskell (but the RTS is C)
19:24:24 <pikhq> (exception: random things like the evil mangler)
19:24:25 <alise> GHC is really gnarly code
19:24:31 <alise> some parts define the Monad class themselves
19:24:35 <alise> because haskell didn't have it at the time!
19:25:24 <AnMaster> I assume the stuff not implemented in haskell is kept to a minimum?
19:25:54 <alise> It's quite big but it's also rather good.
19:26:02 <alise> And most of the Prelude is in Haskell.
19:26:05 <alise> Almost all, in fact.
19:26:11 <alise> It's just auto-specialised behind the scenes.
19:29:20 <Sgeo> I just start experimenting with unsafeInterleaveIO, and I get told to avoid it :(
19:31:24 <Sgeo> My computer just started singing "Good Morning" to me
19:33:20 <Sgeo> Dear Megavideo: I waited 54 minutes. Now please let me continue watching my video
20:09:14 -!- Oranjer has joined.
20:31:41 -!- alise has quit (Ping timeout: 258 seconds).
20:37:38 <fizzie> 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.
20:38:24 <fizzie> 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.
20:42:10 <Ilari> Reminds me of programming assignment from one course...
20:45:06 <AnMaster> fizzie, so it doesn't work for non-text files?
20:45:28 <AnMaster> fizzie, as for using timing: would be unreliable on a non-realtime OS
20:45:29 <fizzie> AnMaster: Right. But be honest, how often do you need to copy non-text files anyway? Almost never!
20:45:43 <fizzie> Oh, but it's not a problem if you use long enough pauses.
20:45:48 <AnMaster> fizzie, more often than text files!
20:46:02 <AnMaster> only cp command today was to copy a kernel image to /boot
20:46:12 <fizzie> 20 milliseconds between bytes and 100 milliseconds between words, it seems.
20:46:26 <ais523> I don't think I've used cp for about a week now
20:46:38 <AnMaster> I use mv a lot more often than cp
20:46:40 <ais523> I don't copy very often; I did yesterday, but via the GUI
20:53:36 -!- alise has joined.
21:00:12 <pikhq> Gregor: Think maybe you could add the &butiwouldratherbereading= feature to Lonely Dino?
21:00:41 <Gregor> Shouldn't be /too/ difficult, I could cut up the images as they are ...
21:02:49 -!- adam_d_ has joined.
21:06:17 -!- adam_d has quit (Ping timeout: 265 seconds).
21:06:27 <alise> butiwouldratherbereading?
21:06:35 <ais523> sounds like an April Fool's URL param
21:06:54 <alise> 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.
21:06:55 <alise> 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.
21:07:03 <alise> http://www.qwantz.com/index.php?comic=290&butiwouldratherbereading=nedroid
21:07:42 <Gregor> http://www.qwantz.com/index.php?comic=35&butiwouldratherbereading=nedroid
21:07:45 <alise> other params: achewood, pennyarcade, wigu, pokey
21:07:56 <alise> http://www.qwantz.com/index.php?comic=&butiwouldratherbereading=pokey -- thus creating the best comic strip conceivable
21:09:11 <alise> onewheretrexswearsmore
21:09:27 <alise> http://www.qwantz.com/index.php?comic=548&butiwouldratherbereading=daisyowl
21:12:06 * Sgeo decides that the best way to understand the State monad is to read the source
21:12:56 <ais523> it's pretty comprehensible anyway
21:13:08 <ais523> it's basically what you do in Haskell if you really want to make it an imperative lang
21:13:26 <ais523> although, more fun would be some sort of State variant that stored an associative array with ways to update individual elements
21:13:47 <Sgeo> Like the ST monad except with STRefs only storing one type?
21:14:14 <ais523> that way, you could compile imperative langs almost literally
21:14:25 -!- oklopol has quit (Ping timeout: 248 seconds).
21:15:43 <alise> Sgeo: It's nothing to do with ST.
21:15:49 <alise> ST is an entirely different strange beast altogether.
21:16:14 <pikhq> ST is a safe IO monad.
21:16:22 <Sgeo> alise, different from State [I know], or different from what ais523 is describing [please explain]?
21:16:25 <alise> Well, just the reference part.
21:16:27 <alise> Its semantics are odd.
21:16:32 -!- kar8nga has joined.
21:16:37 <pikhq> alise: Well. Yes. That's what makes it safe.
21:16:41 <alise> State is simply - you know how you could pass an extra argument to every function, Sgeo?
21:16:47 <alise> And just call with a modified argument to change state?
21:16:55 <alise> State just wraps that into a monad so you don't have to pass it around.
21:16:58 <alise> The semantics are identical,
21:16:59 <ais523> State is pretty much the purest form of a Haskell monad, I think
21:17:03 <Sgeo> alise, I know what it is, I'm trying to understand how it works, which is why I'm reading the source
21:17:07 <ais523> it's a monad, and the monad chain is accessible and user-defined
21:17:36 <ais523> 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
21:17:59 <alise> Monads are so pass.
21:18:43 <ais523> yep, they just get all the press because they're unusual to people who don't know Haskell
21:19:33 <alise> Dependent types are the shiznit.
21:19:51 <ais523> wait, people actually use the word "shiznit"?
21:20:15 <Sgeo> 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"
21:20:16 <pikhq> I have talked to people who think monads are a gargantuan, subtle, and strange library.
21:20:29 <alise> ais523: Especially when talking about mathematics!
21:20:52 <ais523> Sgeo: that's what it's /for
21:20:55 <pikhq> The State monad is a fairly simple thing. That'd be pretty easy to do.
21:21:12 <alise> ais523: no, he means
21:21:16 <alise> accessing state directly using the constructors
21:21:20 <pikhq> The only thing the State monad grants you is nice sugar for that.
21:21:43 <Sgeo> Just to clarify my understanding quickly, a >>= b >>= c is parenthesized as a >>= (b >>= c) ?
21:21:56 <alise> Sgeo: It does not matter.
21:22:02 <alise> The monad laws require the two to be equal.
21:22:09 <pikhq> Sgeo: Yes, but it does not matter for any proper monad.
21:22:41 <pikhq> That's one of the monad laws.
21:22:57 <Sgeo> Which way of thinking about it would make the definition of >>= for State easier to understand?
21:22:59 <alise> Sgeo: why do you struggle with simple identities?
21:23:17 <ais523> Sgeo: think of "a >> b" as "do a then b"
21:23:25 <ais523> then it's obvious that a >> b >> c the parens don't matter
21:23:34 <ais523> and >>= is just a version where you can grab a return value
21:23:57 <Sgeo> alise, surely there was a time when you struggled with this stuff. When was that?
21:24:32 <ais523> Sgeo: I picked up monads pretty quickly
21:24:34 <Sgeo> [Not necessarily THIS stuff in particular, but Haskell in general, or specific parts of Haskell]
21:24:34 <alise> Oh, absolutely, I struggled with monads.
21:24:55 <alise> But I just seem to notice a sort of pattern where you have issues abstracting out simple laws to understand instances satisfying those laws.
21:25:17 <alise> Certainly I must have my own flaws in understanding that I do not myself notice.
21:25:54 <pikhq> 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.
21:26:41 <Sgeo> syntactic sugar doesn't count as magic? :D
21:26:45 <Gregor> Rule four with monads: you may need more pixie dust.
21:27:33 <pikhq> Sgeo: That's no magic.
21:30:25 * Sgeo thinks he gets State's >>=
21:33:11 <alise> I wish fax was here
21:33:15 -!- comex has quit (Ping timeout: 268 seconds).
21:33:25 -!- comex has joined.
21:34:50 <Sgeo> alise, fax is in #haskell
21:35:10 <Gregor> <alise> I wish fax was here // Awwwww
21:35:19 <alise> to ask about type theory kthx
21:38:33 -!- oerjan has joined.
21:45:31 <Sgeo> Now, I need to learn to understand Functors and Arrows
21:46:04 <pikhq> Functors are trivial.
21:46:09 <Sgeo> alise, about my learning, I've noticed that I like to read a lot of different tutorials
21:46:15 <oerjan> <alise> 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
21:46:27 <pikhq> Functors are objects where fmap makes sense.
21:46:33 <Sgeo> oerjan, the real numbers don't make up a set?
21:46:53 <oerjan> Sgeo: _in both places_
21:47:48 <oerjan> it is indeed true (in ZFC) that there is no surjective mapping from reals to functions from reals to booleans.
21:48:47 <oerjan> 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)
21:49:17 <Sgeo> How much of that relies on the C in ZFC?
21:49:23 <oerjan> (i said it that complicatedly because i'm not sure if those are equivalent concepts in ehird's type theory stuf)
21:49:58 -!- pikhq has quit (Read error: Connection reset by peer).
21:50:01 * alise generalises it not to have nat; I realised it didn't need it but didn't think to formalise that
21:50:13 <oerjan> 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
21:51:02 <alise> it is true in type theory of course
21:51:05 <alise> certainly so since I formalised it
21:51:40 <oerjan> in my intuition type theory is almost the same thing as constructive set theory.
21:51:50 <alise> Almost, but not quite.
21:51:54 <alise> Type theory has an equality type for instance.
21:52:09 <alise> And set theory, well, doesn't really have "dependent" sets in any meaningful sense.
21:52:13 <oerjan> i suppose you could have a simpler constructive set theory than that
21:52:15 -!- coppro has joined.
21:52:26 <alise> Plus things like quotient sets and the like - but the fundamental theories, sure.
21:52:31 <alise> oerjan: http://pastie.org/900901.txt?key=gfjqr1tonuchocnutw2dqw
21:53:23 <alise> I am surprised Coq does not already have notb/notdistinct. Or maybe it does?
21:53:30 <oerjan> 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)
21:54:27 <alise> Diagonalisation is beautiful.
21:56:00 -!- coppro has quit (Client Quit).
21:58:35 <alise> oerjan: http://pastie.org/900907.txt?key=ny2be0sujqn23hvkcty1fa
21:58:45 <alise> Could generalise it from bool if you want, but...
21:59:47 -!- pikhq has joined.
22:01:44 <Sgeo> Should I consider rewriting some of my Python stuff in Haskell?
22:02:01 <Sgeo> Actually, most of it is on my old computer, so meh
22:02:20 <alise> let e := magic_surj in
22:02:20 <alise> match e (fun n : T => negb (magic n n)) with
22:02:20 <alise> let n := no_fixpoint_negb in
22:02:21 <alise> match n (magic x x) (sym_eq (H x)) return False with
22:03:18 <pikhq> Hey, Internet's back!
22:06:10 -!- tombom_ has joined.
22:08:48 -!- pikhq has quit (Read error: Connection reset by peer).
22:09:02 <oerjan> yay we managed to outrun him again
22:09:12 -!- sshc has quit (Quit: leaving).
22:09:51 -!- tombom has quit (Ping timeout: 260 seconds).
22:10:55 -!- kar8nga has quit (Read error: Connection reset by peer).
22:12:19 -!- coppro has joined.
22:15:06 -!- coppro has quit (Client Quit).
22:20:08 <oerjan> <alise> unsafeInterleaveIO is just return (unsafePerformIO x)
22:20:38 <oerjan> except with a guarantee of not evaluating more than once
22:21:19 -!- coppro has joined.
22:22:35 <oerjan> i used it in Malbolge Unshackled to create an infinite lazy datastructure containing IORefs. afaik that usage is perfectly safe.
22:22:57 <Sgeo> unsafePerformIO can't get evaluated more than once?
22:23:04 <Sgeo> erm, things made with
22:24:50 <oerjan> haskell compilers are perfectly permitted to inline pure code in multiple places
22:34:54 <Gregor> (Hence "unsafe" PerformIO)
22:35:30 <Sgeo> I meant unsafeInterleaveIO
22:35:30 <fizzie> 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
22:37:40 <oerjan> 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
22:38:18 <oerjan> and getContents uses unsafeInterleaveIO internally
22:38:29 <oerjan> (or something very close to it)
22:39:21 <Sgeo> Isn't there some function (Monad m) => m m a -> m a?
22:39:58 <oerjan> 13:21:43 <Sgeo> Just to clarify my understanding quickly, a >>= b >>= c is parenthesized as a >>= (b >>= c) ?
22:40:01 <oerjan> 13:21:56 <alise> Sgeo: It does not matter.
22:40:04 <oerjan> 13:22:02 <alise> The monad laws require the two to be equal.
22:40:27 <oerjan> no, it must be (a >>= b) >>= c, the other one isn't even well-typed
22:41:04 <oerjan> damn egobot always disappearing
22:41:06 <Sgeo> What does it do with IO, and could unsafeInterleaveIO be written without unsafePerformIO using join somehow?
22:41:18 <alise> oerjan: oh of course
22:41:32 <Sgeo> (>>=) :: (Monad m) => m a -> (a -> m b) -> m b
22:41:49 <oerjan> Sgeo: it defers running the actual action until the result is needed. no way of doing that with join.
22:42:20 <oerjan> Sgeo: it was the fixity/precedence i was looking for, actually
22:42:57 <oerjan> so left as you'd expect
22:43:03 * Sgeo still gets confused by fixity
22:43:22 <oerjan> it's associativity and precedence bundled into one
22:43:37 <Sgeo> Then I'm confused by associativity
22:43:47 <oerjan> where associativity is in the syntactic sense
22:44:21 <oerjan> basically, should a >>= b >>= c mean (a >>= b) >>= c, a >>= (b >>= c) or be disallowed altogether?
22:44:37 <oerjan> those are infixl, infixr and infix, respectively
22:44:41 <Sgeo> Which is which.. oh
22:45:26 <oerjan> which side you start combining terms from, essentially
22:45:50 <Sgeo> What happens when you mix in other operators of equal precedency?
22:46:17 <oerjan> Sgeo: note that those first two are foldl (>>=) [a,b,c] and foldr (>>=) [a,b,c] respectively
22:46:29 <Gregor> HASKELL HAS NO CONCEPT OF NULLITY
22:46:38 <oerjan> or would be, if they were compatible types
22:47:40 -!- tombom_ has quit (Quit: Leaving).
22:47:43 <oerjan> Sgeo: join x intuitively runs x, then runs the result immediately as an action in the same monad. no deferring involved.
22:48:03 <oerjan> and you cannot simulate it without some special function
22:48:41 <oerjan> (of course monads other than IO may not strictly obey the concept of running things immediately)
22:49:45 <Sgeo> What are Arrows?
22:51:12 <oerjan> a kind of strange bundling of features afaict
22:51:35 <oerjan> they're morphisms in a category, so functions are your main example.
22:52:00 <oerjan> you can compose them with >>> . for functions f >>> g means g . f
22:52:09 -!- Deewiant has quit (*.net *.split).
22:52:09 -!- wareya has quit (*.net *.split).
22:52:09 -!- Slereah has quit (*.net *.split).
22:52:34 <oerjan> but they also include operations to combine stuff "in parallel", using pairs
22:52:36 -!- dixon` has joined.
22:52:42 -!- dixon` has left (?).
22:52:58 <oerjan> e.g. (f &&& g) x = (f x, g x) and (f *** g) (x,y) = (f x, g y)
22:53:11 <oerjan> (again using the function example)
22:53:14 <Sgeo> Well, I'm convinced. Let me brain bleach all my Haskell knowledge.
22:53:25 -!- Deewiant has joined.
22:53:25 -!- wareya has joined.
22:53:32 -!- Slereah has joined.
22:54:11 <ais523> hmm, I don't understand that restriction, as it goes away if you add a type signature
22:54:21 <ais523> that says just what the compiler had inferred anyway
22:54:30 <alise> which is why you disable it
22:55:09 <oerjan> 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
22:55:25 <ais523> I don't see how that's related...
22:55:55 <oerjan> but if the type involves type classes, then the right side can only be evaluated after you pass the actual type dictionary into it
22:57:11 <oerjan> 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
22:57:34 <oerjan> that's my understanding of the x = ... case.
22:57:58 <Sgeo> Semantically that should be equiv unless unsafePerformIO is involved, right?
22:58:34 <ais523> semantically it's irrelevant
22:59:12 <oerjan> 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
22:59:52 <oerjan> although the compiler could try to be cleverer there, the standard does not demand it
23:00:24 <oerjan> Sgeo: yes. but someone has apparently coughed up an example where this causes exponential blowup in execution time
23:01:24 <oerjan> as for nonstandardness of GHC i don't know, unless you mean its heap of extensions which are optional...
23:01:52 <Sgeo> return quadrescence :: IO Chatter
23:05:11 -!- fax has joined.
23:06:15 <oerjan> well i don't use ghc so i don't know, i thought you had to use a flag for almost everything
23:06:36 <Sgeo> oerjan, what do you use? Hugs?
23:07:14 <Quadrescence> Sgeo: oerjan is sane and uses Standard ML with MLton
23:07:18 <oerjan> (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)
23:07:28 <oerjan> other than that, winhugs
23:08:35 <oerjan> (i got seriously annoyed when ghci insisted on waiting for the gvim editor to quit and i see winghci avoids that)
23:09:18 <oerjan> (gvim _tries_ to fork itself to avoid such unless you add a flag, but ghci somehow manages to thwart it)
23:09:39 <Quadrescence> oerjan: why isn't Monad a "subtype" of Functor? (why it doesn't inherit from the Functor typeclass)
23:09:54 <oerjan> Quadrescence: hysterical raisins
23:10:39 -!- Deewiant has quit (*.net *.split).
23:10:39 -!- wareya has quit (*.net *.split).
23:10:44 <oerjan> Functor was invented after Haskell 98 was standardized
23:11:05 <Quadrescence> mathematical functors and monads weren't invented with Haskell
23:11:19 <alise> but at first haskell only had monads
23:11:26 <alise> anyway, I'm feeling so sick that I had better go to bed now
23:11:27 <oerjan> and they've never managed to implement the "case class" feature that is supposed to make things seamless
23:11:32 -!- alise has quit (Quit: Leaving).
23:11:45 <oerjan> er it's not case class
23:12:42 <Sgeo> Is Scala any good?
23:12:48 <Sgeo> Or should I stick with Haskell?
23:13:06 <oerjan> i don't know i've just read about it's case classes
23:13:08 <Quadrescence> It has type safety, runs on the JVM, object oriented
23:13:47 <oerjan> 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
23:14:42 -!- wareya has joined.
23:14:44 <oerjan> they would also like to put Applicative in between, there
23:15:10 -!- adam_d_ has changed nick to adam_d.
23:16:29 -!- Deewiant has joined.
23:18:00 <oerjan> 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
23:19:40 <oerjan> some of that is in Data.Traversable as well iirc
23:20:22 -!- MigoMipo has quit (Remote host closed the connection).
23:20:48 -!- Deewiant has quit (*.net *.split).
23:22:40 -!- Oranjer has left (?).
23:23:06 <oerjan> and a bit in Data.Foldable
23:24:14 -!- Deewiant has joined.
23:34:50 <fax> I dont know how to compute the product of gaussian periods
23:37:39 -!- pikhq has joined.
23:39:50 * oerjan suspects a connection with harmonic analysis of finite abelian groups
23:46:06 -!- Oranjer has joined.
23:48:44 <fax> if z^5=1 what is the value of z+2z^2+z^4 ?
23:50:00 <fax> apparentnyl it's always a rational, but it's not...
23:50:11 <pikhq> fax: What's the type of z?
23:50:25 <fax> complex number
23:50:31 <fax> complex real*
23:51:30 <fax> I think -1=(z^2+z^4)+(z^3+z^1)=x1 + x2 should mean that x1*x2 is a rational
23:53:33 <Gregor> 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*
23:53:38 -!- pikhq has quit (Read error: Connection reset by peer).
23:55:30 <oerjan> Data.Complex> [z+2*z^2+z^4 | let r = mkPolar 1 (pi*2/5) , z <- map (r^) [0..4]]
23:55:50 <oerjan> [4.0 :+ 0.0,(-1.0) :+ 1.17557050458495,(-1.0) :+ (-1.90211303259031),(-0.999999999999999) :+ 1.90211303259031,(-1.0) :+ (-1.17557050458495)] :: [Complex Double]
23:56:24 <fax> what about z^2+z^3?
23:56:50 <oerjan> Data.Complex> [z^2+z^3 | let r = mkPolar 1 (pi*2/5) , z <- map (r^) [0..4]]
23:56:50 <oerjan> [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]
23:57:10 <fax> what the hell
23:57:25 <oerjan> z^2 is the conjugate of z^3
23:57:48 <oerjan> since they're inverses and on the unit circle
23:58:10 <oerjan> so it's really just Re (2*z^2)
23:58:17 -!- pikhq has joined.