00:00:07 <kmc> "it's like The Big Bang Theory but for black people instead of nerds"
00:00:28 -!- Phantom__Hoover has joined.
00:01:06 <Bike> kmc: i'm already horrified.
00:01:35 <Bike> what blackface are you talking about?
00:01:46 <Phantom__Hoover> uh, http://en.wikipedia.org/wiki/The_Black_and_White_Minstrel_Show
00:03:22 <Bike> " (by this point the blackface element had been reduced)" great
00:03:46 -!- Phantom_Hoover has quit (Ping timeout: 245 seconds).
00:03:55 <elliott> `addquote <kmc> "it's like The Big Bang Theory but for black people instead of nerds"
00:04:07 <HackEgo> 941) <kmc> "it's like The Big Bang Theory but for black people instead of nerds"
00:04:18 <elliott> Phantom__Hoover: political correctness.................. killing our wholesome black and white minstrel show rtaditions.........
00:05:39 <Bike> so, does anyone know how carry-lookahead works
00:09:09 <elliott> Phantom__Hoover: haha jesus christ at the picture of that minstrel show
00:09:51 <Phantom__Hoover> with the black-and-white photo you almost don't notice it's racist
00:09:56 <elliott> The show appeared in a prime-time slot for twenty years, but during the 1970s its popularity declined, partly because of the style of music becoming dated and partly because of an increase in racial awareness. It was axed by the BBC after several unsuccessful attempts to change the format. Mitchell was awarded the OBE in 1975.
00:10:02 <Bike> no i pretty much noticed it was racist
00:10:02 -!- epicmonkey has quit (Ping timeout: 245 seconds).
00:10:05 <elliott> sorry for cancelling your racist as hell show, here's an OBE in return
00:10:36 <elliott> we're just finding out what we knew all along
00:10:41 <Bike> was he from hexham ._.
00:11:10 <Phantom__Hoover> look man we were just happy the english had found someone else to pick on
00:11:19 <elliott> "While the show started off being broadcast in (genuine) black-and-white, the show was one of the very first to be shown in colour on BBC Two in 1967."
00:11:58 <scarf> my parents insist the snooker was the very first color programme on the BBC
00:12:01 <olsner> hmm, if they were in blackface shouldn't it be white-and-white?
00:12:09 <elliott> "During the nine years that the show was broadcast in black-and-white, the black-face makeup was actually red as black did not film very well."
00:12:15 <elliott> scarf: I think that was true?
00:12:22 <scarf> I didn't say it was false
00:12:25 <Bike> those poor native americans
00:12:44 <olsner> elliott: oh, that reminds me, supposedly Spock was supposed to be red-faced
00:12:53 <olsner> but that looks black in black-and-white
00:13:14 <Bike> er... was star trek filmed in black and white at some point?
00:13:27 <olsner> no, but it was broadcast at a time when no-one had color tv yet
00:13:39 <kmc> shachaf: Great Firewall is now MITMing GitHub with a self-signed cert, it seems
00:13:47 <kmc> Homebrew's curl -k looks realllly clever now
00:13:50 <elliott> olsner: yes, we can't have too many black people in Roddenberry's post-everything utopia
00:14:25 <kmc> checking certs is so uncool
00:14:47 <elliott> kmc: you know the first person I ever saw doing the "'curl | interpreter' to install" trick was why the lucky stiff in like... 2005-2007
00:14:48 <Bike> post-present-tense utopia??
00:15:02 <scarf> elliott: surely it was done before then?
00:15:03 <elliott> kmc: not one of his best ideas
00:15:17 <scarf> it's such a bad idea it must have been tried before
00:15:21 <elliott> scarf: if it was I didn't see it -- and most of this stuff seems to be pretty close to the "Ruby community" so I suspect they got it from him
00:15:37 <Phantom__Hoover> milk still exists, although there are no breasts for it to come from
00:16:01 <scarf> elliott: for bonus points, nc | interpreter
00:16:13 <elliott> when why did it it was disclaimed saying it was essentially a terrible idea and linking to the actual script so you could read it yourself
00:16:18 <scarf> this can go wrong in all the same ways, and it's easier to make it do so
00:16:36 <elliott> kmc: wow I just looked up what curl's -k option is
00:16:50 <scarf> the only safe method is to save the code, /then/ read, /then/ run
00:17:00 <kmc> but _why is a god and we must worship him
00:17:08 <scarf> and read it in something with no terminal control sequence injection exploits or the like
00:17:56 <kmc> elliott: ksplice easy install uses curl | sh :( but at least it's SSL with a real cert and not curl -k
00:17:58 <scarf> elliott: -k is to not verify certs, by the look of it
00:18:03 <kmc> aka --insecure
00:18:14 <elliott> kmc: a bit of proper _why worship would do a lot of these idiots good
00:18:17 <scarf> well, it's still more secure than using non-https http
00:18:28 <elliott> cut down on a lot of ego at the very least
00:18:39 <Bike> didn't why spontaneously combust or something
00:18:43 <kmc> 'This option explicitly allows curl to perform "insecure" SSL connections and transfers. All SSL connections are attempted to be made secure by using the CA certificate bundle installed by default. '
00:18:54 <kmc> ' This makes all connections considered "insecure" fail unless -k, --insecure is used.'
00:19:04 <kmc> this is a mind bogglingly poor explanation of what the option does
00:19:09 <elliott> Bike: he deleted all his accounts and went back to living as not-why the regular employed programmer
00:19:21 <scarf> elliott: that was probably a sensible decision
00:19:22 <olsner> yes, it very nearly says that -k makes curl secure
00:19:25 <kmc> elliott: did he leave because the rails community is terrible or?
00:19:30 <Bike> like the bodhisattva
00:19:41 <elliott> kmc: not afaik and I don't think that would fit him
00:19:49 <shachaf> I don't think he was ever really involved in the Rails community?
00:19:53 <elliott> Phantom__Hoover: nobody "knows" what it was over except him and whoever knows him personally
00:20:12 <elliott> I suspect he just got tired
00:20:20 <kmc> not rails but ruby? or what
00:20:26 <Bike> kmc: so, how much security research is predicated on "half of the users are going to get their asses infected anyway, how do we avoid sql slammering"
00:20:27 <elliott> shachaf: well he was "involved" insofar as it is kind of hard to separate ruby from rails
00:20:31 <scarf> elliott: it's wearing being a celebrity even if you're a celebrity as obscure as I am
00:20:33 <olsner> maybe he lives on as a normal person
00:20:35 <elliott> but yes he never did rails stuff afaik
00:20:44 <elliott> unless mocking DHH counts as doing rails
00:20:45 <kmc> shachaf: did you know Ruby was started in 1995??
00:20:50 <kmc> elliott: that counts as doing god's work
00:21:05 <elliott> kmc: did you know python started in like 1990
00:21:12 <kmc> it's weird that a language can be obscure for 10 years and then suddenly become hot shit in another country
00:21:17 <kmc> elliott: yeah
00:21:20 <elliott> kmc: perl is only 4 years older than python
00:21:30 <kmc> i think with python it was less sudden though
00:21:32 <shachaf> I totally learned Ruby before Rails was cool.
00:21:41 <elliott> python was the hip unix thing in late 1990s AIUI
00:21:45 <elliott> partially due to esr I think
00:21:51 <kmc> fuck that guy
00:21:57 <kmc> "the python paradox"
00:22:06 <kmc> was written in 2004
00:22:10 <elliott> with Ruby it was a combination of the fact that dave thomas randomly found out about ruby
00:22:20 <elliott> and decided to write a whole english introduction-slash-reference-book about it for no apparent reason
00:22:24 <kmc> the wendy's guy??
00:22:27 <elliott> because it had like no english documentation
00:22:28 <scarf> elliott: should I feel bad for not knowing who dave thomas is?
00:22:35 <elliott> and then DHH read it I guess
00:22:41 <kmc> he invented wendy's, a popular American fast food restaurant
00:22:55 <kmc> also he died in 2002 so "probably not the same guy"
00:23:01 <elliott> kmc: the pragmatic programmer guy
00:23:28 <shachaf> elliott: should I feel bad for knowing who dave thomas is?
00:23:31 <scarf> Ruby strikes me as a rebellion against Java
00:23:33 <Phantom__Hoover> Bike, 'peace be upon him', muslims say it as a mark of respect for muhammed aiui
00:24:10 <Bike> well, it should be
00:24:14 <Bike> because well, fuck that guy
00:24:41 <Sgeo> wtf my first initial and last name showed up in Ghost in the Shell
00:24:42 <olsner> if ruby started in 1995, I think Java hadn't existed for long enough to warrant a rebellion against it
00:24:45 <Bike> i've never seen pbuh abbreviated like that though
00:24:47 <elliott> scarf: ruby is actually lisp + objects + smalltalk + perl
00:24:50 <elliott> as in matz has actually said this
00:24:55 <elliott> well I guess + objects is redundant there
00:24:59 <Bike> that's a fucking weird equation
00:25:01 <kmc> Phantom__Hoover: what
00:25:03 <elliott> also it's older than Java I think
00:25:04 <scarf> but its community has quite an attitude of "let's change the internals of things on the fly"
00:25:12 <kmc> is it because he half maintains a befunge interpreter or something
00:25:30 <Bike> coincidence? or conspiracy??
00:25:30 <elliott> so Ruby can't really be a reaction to Java at all
00:25:34 <scarf> when does C++ date from?
00:25:47 <scarf> oh and yeah, esr and I are both doing equal lack of work on C-INTERCAL atm
00:26:01 <Phantom__Hoover> then knuth somehow got involved and esr's ego shot through the roof
00:26:04 <kmc> scarf: C++ lay dormant for nameless millenia at the bottom of the ocean
00:26:50 <Bike> in strange aeons even garbage collection may die?
00:27:00 <scarf> Phantom__Hoover: perhaps the easier way to explain it is, I can excuse Knuth for never having heard of me and vaguely remembering that ESR had an INTERCAL interp
00:27:09 <scarf> I can excuse him for never having heard of Claudio Calvelli, too
00:27:28 <scarf> and the J-INTERCAL guy, I can't even remember who he is
00:27:50 <kmc> lisp + objects + smalltalk + perl + cayenne pepper + potato + pinch of salt
00:27:55 <shachaf> Is that INTERCAL written in J?
00:28:07 <scarf> shachaf: Java, sadly
00:28:15 <Phantom__Hoover> how did knuth not hear of the winner of the WOLFRAM PRIZE for PROVING WOLFRAM RIGHT
00:28:18 <scarf> it's an INTERCAL to JVM bytecode compiler, I think
00:28:23 <shachaf> J is "much cooler than" Java.
00:28:30 <Bike> that actually sounds a bit cool, scarf
00:28:37 <Bike> hurry up and dissuade me from this thought
00:28:46 <scarf> I remember having to fix a J-INTERCAL-specific bug I introduced into CADIE
00:28:56 <scarf> (as well as being vaguely surprised that anyone bothered to try)
00:29:07 <Bike> Phantom__Hoover: is "fuck that guy" also the pbuh for wolfram?
00:29:32 <Bike> don't be disrespectful to wolfram, fuck that guy, remember to say fuck that guy
00:30:09 <Bike> fuck that guy in doubly exponential time?
00:30:37 <Bike> hm is there such a thing as tetration time
00:30:43 <scarf> doubly exponential time? is that e^e^x?
00:30:53 <scarf> the latter seems a little redundant
00:30:54 <Bike> e^e^x, as i understand
00:31:09 <Bike> yes, of course, the latter would be a constant factor, and fuck constant factors.
00:31:28 <scarf> reminds me of a reddit debate about whether O(1) is or isn't the same as O(0)
00:31:41 <Bike> that sounds like a complete waste of time?
00:31:58 <scarf> Bike: it's /reddit/
00:32:03 <scarf> the purpose of being there is to waste time
00:32:12 <scarf> in a manner that's occasionally vaguely productive
00:32:25 <shachaf> Did they talk about O(1/n)?
00:32:26 <Bike> but i don't use reddit and i've still been linked to interesting posts there!
00:32:29 <FreeFull> O(1) is the same as O(0), they're both x^0
00:32:58 <scarf> FreeFull: OTOH, O(1) definitely grows faster
00:33:04 <scarf> even with the standard definition in terms of limits
00:33:15 <Bike> speaking of reading things on the internet, this thing about anthropology has a guy who keeps going on about epistemology and levi-strauss, and it bugs me
00:45:32 <scarf> 00:48:57: <ais523> javad3v: hi
00:45:41 <scarf> hey, apparently I've used threat-his on people too
00:48:57 <kmc> i think for things that go to 0 you want to use o() not O()?
00:49:03 * kmc forgets this stuff
00:49:17 <Bike> can anyone actually remember the differences between o, O, Omega, etc. reliably?
00:49:32 <Bike> they use them all over the place in one of my books and it confuses the hell out of me :(
00:49:36 <scarf> Bike: yeah, o() is less than, O() is less than or equal to, capital Theta is equal to
00:49:43 <HackEgo> 2012-02-24.txt:19:37:12: <elliott> quintopia: Wellll, since I'm assuming you don't know what you're doing (no offence), I'd assign half a day or so to the task. 90% of that will be reading http://wiki.nginx.org/WordPress.
00:49:53 <scarf> (this is not mathematically rigorous, but easy to remembre)
00:49:54 <kmc> well O / Ω / Θ is easy enough
00:50:00 <scarf> Bike: take that back, please, it doesn't really sound like something to damn people over
00:50:09 <Bike> ok, heaven you.
00:50:09 <kmc> upper / lower / both bound
00:50:14 <scarf> think about what you juts said
00:50:20 <scarf> Phantom__Hoover: O is <=, o is <
00:50:25 <Bike> wait, bless you
00:50:31 <scarf> yeah, that sounds about right :)
00:50:53 <Bike> i think that evens out with the damning, so along with the shitty "heaven" confusion when you die you'll probably end up in like the troposphere
00:51:31 <scarf> it's more the sentiment expressed, whether or not anyone involved actually believes it
00:51:54 <scarf> going by the literal meanings of the words involved, I'm not sure if a worse insult is even theoretically possible
00:51:58 <scarf> and yet it's considered quite mild
00:52:00 <Bike> i'm not sure what "heaven you" would actually mean. it's kind of ungrammatical
00:52:05 <kmc> e^x dx dx, e^y dy
00:53:02 <Phantom__Hoover> scarf, erm, christian hell varies wildly in unpleasantness depending on who you ask.
00:53:25 <scarf> Phantom__Hoover: there are people who consider it pleasant?
00:53:31 <scarf> that would sort-of contradict the definition
00:53:39 <Bike> sure, even dante had limbo as pretty nice
00:54:20 <Bike> there are also lots of exciting arguments about hell and theodicy that i'm so glad i don't give a fuck about any more
00:54:55 <scarf> hey, did we even work out whether /ˈæmbiːɛf/ is remotely usable for programming?
00:55:05 <scarf> that was a good langugae
00:55:16 <Phantom__Hoover> scarf, anyway I really don't get this, it would make sense if zzo38 did it maybe.
00:55:30 <Bike> remember to put "remotely usable for programming" in the advertising.
00:55:36 <scarf> Phantom__Hoover: I dislike swearword decay
00:55:57 <Bike> "damn"'s been pretty "decayed" since like medieval times
00:56:39 <Sgeo> When I get a new computer, I'm going to put XenClient on it I think
00:56:44 <scarf> Phantom__Hoover: I am, although I conclude that it's probably irrational to be
00:56:51 <Sgeo> Do games work well under XenClient?
00:57:21 <scarf> Phantom__Hoover: I have a lot of irrational beliefs
00:57:25 <Bike> Phantom__Hoover: personally i'm not really that concerned but i'd rather not worry scarf if he does actually care for reasons i don't understand
00:58:23 <Phantom__Hoover> Bike, well like I said if it was zzo38 I could maybe understand but with scarf it just seems like a weird sort of contrarianism?
00:58:25 <Bike> "It's possible to (via dead-reckoning) always determine whether you're on an odd or an even tape element" amazing.
00:58:37 <Bike> Phantom__Hoover: really don't give a damn
00:59:04 <scarf> Phantom__Hoover: put it this way: zzo38 is a lot more internally consistent than I am
00:59:12 <scarf> Phantom__Hoover: I can't reasonably assign a meaning to it, so it doesn't bother me
00:59:46 <Bike> do i need to start cursing in dungan or something? i mean, that would be amusing so i may actually do that, but
01:00:14 <scarf> <cpressey> I also guess I also have several other thoughts on the matter, but they are too wide-ranging and not directly relevant, so I will save them for The Manifesto.
01:00:28 <scarf> I didn't really notice that sentence the first time through
01:00:33 <Bike> dungans are pretty boss imo
01:00:34 <scarf> in retrospect, isn't it somewhat ominous?
01:00:42 <Bike> speak chinese....... in russian
01:05:25 -!- fungot has quit (Ping timeout: 248 seconds).
01:06:42 -!- fizzie has quit (Ping timeout: 245 seconds).
01:06:49 -!- fizzie has joined.
01:10:20 -!- Franklin-Jesus has joined.
01:10:48 <scarf> Phantom__Hoover: pingout
01:10:59 <scarf> fungot left at the same time and didn't come back
01:11:04 <scarf> or in elliott-speak, rip fungot
01:12:15 <monqy> `welcome Franklin-Jesus
01:12:16 <HackEgo> Franklin-Jesus: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.)
01:13:07 <elliott> Franklin-Jesus: hi please go away and stop spamming : )
01:13:14 <elliott> scarf: hi please kick this guy for spamming : )
01:13:32 <scarf> was reading the navi logs
01:13:38 <scarf> didn't realise we had an actual spammer here
01:13:44 <scarf> Franklin-Jesus: are you a human or a bot?
01:13:51 <monqy> sounds human enough
01:13:59 <scarf> monqy: I prefer to assume it's a spambot
01:14:04 <scarf> that way I can have more fun Turing-testing it
01:14:08 <scarf> and eventualy trying to get it into a botloop
01:14:41 <scarf> ^ul (:a*:SS):a*:SS
01:14:48 <scarf> oh, fungot isn't here
01:15:35 -!- thutubot has joined.
01:15:52 <scarf> +ul (:a*:SS):a*:SS
01:16:03 <scarf> +ul (:a~*:SS):a~*:SS
01:16:04 <thutubot> (:a~*:SS):a~*:SS(:a~*:SS):a~*:SS
01:16:12 <scarf> wanted to write a double-quine
01:16:32 <monqy> i can speak english too
01:16:51 <zzo38> Some other people in here can speak other language too (and sometimes does), but is mainly in English. OK
01:17:15 <FreeFull> > x ++ show x where x = "x ++ show x where x = "
01:17:17 <lambdabot> <hint>:1:13: parse error on input `where'
01:17:17 <thutubot> <hint>:1:13: parse error on input `where'
01:17:44 <scarf> FreeFull: hmm, is it that where doesn't work like that?
01:17:47 <scarf> or something else?
01:17:56 <FreeFull> scarf: where doesn't work like that
01:18:16 <FreeFull> It only works in definitions and let statements
01:18:29 <scarf> was that an attempt at mirroring the structure of the Underload quine in Haskell?
01:18:47 <scarf> I wonder if such a quine can be translated almost directly into FORTH
01:18:52 <scarf> I'm guessing no, due to the compilation step
01:19:13 <FreeFull> Well, a haskell quine is main = print (x ++ show x) where x = "main = print (x ++ show x) where x = "
01:19:47 <scarf> Franklin-Jesus: and you get it twice because of thutubot
01:19:59 <elliott> > let x y = "let x y = " ++ y ++ " in x " ++ show y in x "\"let x y = \" ++ y ++ \" in x \" ++ show y"
01:20:02 <lambdabot> "let x y = \"let x y = \" ++ y ++ \" in x \" ++ show y in x \"\\\"let x y =...
01:20:03 <thutubot> "let x y = \"let x y = \" ++ y ++ \" in x \" ++ show y in x \"\\\"let x y =...
01:20:04 <shachaf> thutubot..................................
01:20:09 <elliott> > text $ let x y = "let x y = " ++ y ++ " in x " ++ show y in x "\"let x y = \" ++ y ++ \" in x \" ++ show y"
01:20:11 <lambdabot> let x y = "let x y = " ++ y ++ " in x " ++ show y in x "\"let x y = \" ++ y...
01:20:12 <thutubot> let x y = "let x y = " ++ y ++ " in x " ++ show y in x "\"let x y = \" ++ y...
01:20:13 <FreeFull> Why are there two haskell bots in here
01:20:13 <kmc> is there any reason why an irc spambot would do anything other than spam and leave?
01:20:27 <shachaf> kmc: Perhaps spam and stay?
01:20:32 <monqy> kmc: gain our trust
01:20:52 <shachaf> Who's thutubot and why is it evaluahaskelling?
01:21:08 <lambdabot> Functor f => (a -> b) -> f a -> f b
01:21:08 <thutubot> Functor f => (a -> b) -> f a -> f b
01:21:26 <Sgeo> What's the correct term, front-end or frontend? Backend or back-end
01:21:41 <monqy> Sgeo: are you trying to look professional
01:21:44 <shachaf> > let unsafeCoerce v = z where z :: v; z = v where aux = const v in unsafeCoerce 'a' :: Int
01:21:46 <lambdabot> `t' is a rigid type variable bound by
01:21:47 <thutubot> Couldn't match type `t' with `v1'
01:21:47 <thutubot> `t' is a rigid type variable bound by
01:21:52 -!- Franklin-Jesus has left.
01:22:04 <thutubot> ASetter s t a b -> b -> s -> t
01:22:07 <shachaf> thutubot who are you thutubot
01:22:08 <FreeFull> > let y = print (x ++ show x) where x = "> let y = print (x ++ show x) where x = "
01:22:10 <lambdabot> not an expression: `let y = print (x ++ show x) where x = "> let y = print ...
01:22:10 <thutubot> not an expression: `let y = print (x ++ show x) where x = "> let y = print ...
01:22:26 <monqy> how does thutubot know about caleskell and lens!!!!!
01:22:31 <FreeFull> That makes quinehood more complicated
01:22:47 <shachaf> thutubot is just copying lambdabot??????????????????
01:22:55 <shachaf> I defined that hi in /msg lambdabot
01:23:04 <elliott> i cant believe it took you this long to figure that out
01:23:09 <lambdabot> echo; msg:IrcMessage {msgServer = "freenode", msgLBName = "lambdabot", msgPrefix = "elliott!elliott@unaffiliated/elliott", msgCommand = "PRIVMSG", msgParams = ["#esoteric",":@echo"]} rest:""
01:23:09 <thutubot> echo; msg:IrcMessage {msgServer = "freenode", msgLBName = "lambdabot", msgPrefix = "elliott!elliott@unaffiliated/elliott", msgCommand = "PRIVMSG", msgParams = ["#esoteric",":@echo"]} rest:""
01:23:19 <lambdabot> lambdabot says: Couldn't match kind `?? -> ? -> *' against `(* -> *) -> * -> *'
01:23:19 <thutubot> lambdabot says: Couldn't match kind `?? -> ? -> *' against `(* -> *) -> * -> *'
01:23:21 <monqy> shachaf: imo you should make lambdabot say something funny
01:23:44 <shachaf> monqy: imo i can't because i'm not a lmabdaobot admin????
01:25:07 <elliott> @msg monqy something funny
01:25:09 <lambdabot> lexical error in string/character literal at character '\S...
01:25:10 <thutubot> lexical error in string/character literal at character '\S...
01:25:31 <Bike> maobot sounds like a good bot
01:25:32 <shachaf> scarf: What's going on with thutubot?
01:25:44 <scarf> scarf: it's a long-standing bug
01:25:48 <scarf> where it repeats everything lambdabot says
01:25:58 <scarf> I never bothered to fix it because I bring it in here so rarely
01:26:06 <Bike> that's a pretty awesome bug
01:26:58 <scarf> wait, IRC doesn't work like that
01:27:12 <scarf> and I can't be bothered to forge the message from the server
01:27:28 <thutubot> IRC doesn't work like that scarf
01:28:48 <scarf> it's a bug in an easter egg / hidden feature that once successfully trolled elliott
01:28:56 <scarf> I don't think the easter egg works any more
01:28:58 <scarf> but the bug still exists
01:29:27 -!- scarf has changed nick to ais523.
01:29:40 -!- thutubot has quit (Remote host closed the connection).
01:29:42 <elliott> Bike: maobot is a bot to play Mao, I guess?
01:29:44 -!- ais523 has changed nick to scarf.
01:29:45 <oerjan> <scarf> FreeFull: hmm, is it that where doesn't work like that? <-- hugs (rip) supported that syntax
01:29:55 <scarf> Freenode have changed how they mark someone as identified
01:29:57 <Bike> elliott: oh i was thinking communist but that would be good too
01:30:09 <FreeFull> oerjan: What does the haskell 98 specification say?
01:30:30 <shachaf> FreeFull: The Haskell Report says that's not an expression.
01:31:48 <scarf> elliott: btw, is it standard to write "fuck" immediately after screwing up an oko pyramid?
01:32:04 <elliott> scarf: I don't know anything about standards
01:32:07 <FreeFull> shachaf: So it's a lambdabot problem?
01:32:07 <elliott> I do it because it's annoying
01:32:14 <FreeFull> Because lambdabot only does expressions
01:32:18 <elliott> in their native channel there is a bot that kicks you when it happens
01:32:23 <elliott> so if there's anything standard it's probably that
01:32:26 <shachaf> FreeFull: Well, it wouldn't work in ghci either.
01:32:46 <shachaf> > let quine = x ++ show x where x = "x ++ show x where x = " in quine
01:32:48 <lambdabot> "x ++ show x where x = \"x ++ show x where x = \""
01:33:04 <Bike> haskell has things other than expressions?
01:33:21 <FreeFull> Bike: x = y isn't an expression
01:36:31 <oerjan> scarf: is thutubot's code available?
01:36:56 <scarf> oerjan: I don't know; it's available in the sense that I don't mind posting it
01:37:20 <scarf> shall I put it on sprunge or somewhere?
01:38:25 <FreeFull> Can you do pattern matching in an if?
01:38:38 <scarf> oerjan: http://sprunge.us/JTUW?thutu
01:38:58 <scarf> you can see how old the codebase is just by looking at the IRC commands
01:39:09 <scarf> last modified oct 10 2008
01:40:10 <oerjan> scarf: that contains a password hth
01:41:24 <FreeFull> > (\x -> if a <- x then a else 3) 4
01:41:25 <lambdabot> <hint>:1:13: parse error on input `<-'
01:41:30 <scarf> good thing it was a single use insecure one
01:42:12 -!- thutubot has joined.
01:42:31 <oerjan> scarf: in the line /^=:lambdabot=![^ ]* PRIVMSG [^ ]* =:(.*?)(=r)?=x/--PRIVMSG =#esoteric =:$1=r=n=x/
01:42:34 <Bike> wait, what the hell is that supposed to do, don't you need a do block
01:42:37 <FreeFull> > (\x -> let a | (b,3) <- a = 0 | otherwise = 3 in a x) (4,3)
01:42:39 <lambdabot> The function `a' is applied to one argument,
01:42:39 <thutubot> The function `a' is applied to one argument,
01:42:39 <thutubot> but its type `(t0, t1)' has n...
01:42:43 <oerjan> change the second [^ ] to [^# ]
01:42:57 -!- thutubot has quit (Remote host closed the connection).
01:43:07 <kmc> which syntax did hugs support?
01:43:47 <kmc> as an expression? or as a REPL special case?
01:43:55 <scarf> oerjan: password changed
01:44:11 <oerjan> scarf: what about my bugfix suggestion?
01:44:18 <elliott> scarf: can you update the sprunge accordingly?
01:44:24 <kmc> ok that is more sane
01:44:29 <scarf> oerjan: it's using lamdabot commands that don't even exist
01:44:31 * oerjan swats elliott -----###
01:44:34 <scarf> so it needs more of a fix than that
01:44:58 <scarf> oerjan: looks like my practice of using weak but unique passwords for things that might be pastebinned accidentally has paid off
01:45:02 <lambdabot> Not in scope: `exists'Not in scope: `too'
01:45:13 <elliott> kmc: in haskell 1.old, where was an expression
01:45:18 <elliott> so (x where x = ()) was a valid expr
01:45:34 <kmc> why did they remove it? too much parsing ambiguity?
01:45:57 <scarf> you could take the Verity approach and require parens at the least sign of ambiguity
01:46:01 <shachaf> Sounds kind of ambiguous to me.
01:46:26 <shachaf> Even if it isn't ambiguous on its own, it's definitely ambiguous if ou want it to work for the things current-where works for.
01:46:28 <oerjan> scarf: @run exists. but all my fix is trying to do is to ignore lambdabot messages sent to channels.
01:46:36 <shachaf> Scoping over multiple bindings and all that.
01:46:53 <scarf> oerjan: you can take over maintaining thutubot if you like
01:47:03 <scarf> although actually knowing thutu would be helpful
01:47:19 <elliott> kmc: well where is useful because you can go across multiple clauses
01:47:35 <elliott> but hey there have been haskell versions where all they did was make things worse by ruining them when they were good before
01:50:37 <oerjan> scarf: well my main point in asking for the code was to see if that bug was trivial to fix, and it looked to me like it was, based only on the fact that there was a part of the regexp which obviously matches the recipient.
01:50:47 <scarf> yeah, there are a bunch of trivial to fix bugs
01:50:49 <FreeFull> > let x = print (y ++ init $ show y ++ "\34 in x") where y = "let x = print (y ++ init $ show y ++ \"34 in x\") where y = " in x
01:50:50 <lambdabot> Couldn't match expected type `[GHC.Types.Char]'
01:51:21 <scarf> hey, remember when this channel was active enough that we had to make #esoteric-blah for spammy things?
01:51:25 <FreeFull> > let x = print (y ++ (init $ show y) ++ "\34 in x") where y = "let x = print (y ++ (init $ show y) ++ \"34 in x\") where y = " in x
01:51:26 <scarf> active and ontopic enough, that is
01:51:27 <lambdabot> No instance for (GHC.Show.Show (GHC.Types.IO ()))
01:51:51 <FreeFull> > let x = (y ++ (init $ show y) ++ "\34 in x") where y = "let x = (y ++ (init $ show y) ++ \"34 in x\") where y = " in x
01:51:53 <lambdabot> "let x = (y ++ (init $ show y) ++ \"34 in x\") where y = \"let x = (y ++ (i...
01:52:14 <elliott> you realise I gave a working quine along those lines before...
01:52:46 <Jafet> > text $ ap (++) show "> text $ ap (++) show "
01:52:48 <lambdabot> > text $ ap (++) show "> text $ ap (++) show "
01:53:00 <Bike> > (\x -> x ++ "\"" ++ x ++ "\"") "(\x -> x ++ show x)"
01:53:02 <lambdabot> lexical error in string/character literal at character ' '
01:53:03 <shachaf> Jafet: Sorry, you need to start the line with a space.
01:53:07 <Bike> wow that was dumb, nevermind
01:53:51 -!- Arc_Koen has quit (Quit: Arc_Koen).
01:54:57 <FreeFull> Well, a working lambdabot quine technically is something like > fix (\x -> x ++ show x) "> fix (\x -> x ++ show x)"
01:55:20 <Bike> elliott's seems fine to me.
01:55:24 <FreeFull> It doesn't take into consideration that lambdabot stringifies everything
02:03:23 <Sgeo> http://stackoverflow.com/questions/233673/lexical-closures-in-python
02:03:33 <Jafet> `run function x { printf "%s%q" "$1" "$1"; }; x \`run\ function\ x\ \{\ printf\ \"%s%q\"\ \"\$1\"\ \"\$1\"\;\ \}\;\ x\
02:03:34 <HackEgo> `run function x { printf "%s%q" "$1" "$1"; }; x \`run\ function\ x\ \{\ printf\ \"%s%q\"\ \"\$1\"\ \"\$1\"\;\ \}\;\ x\
02:04:11 <Jafet> @google fuck python
02:05:10 <Bike> Sgeo: for the love of god why do people keep using for loops for this garbage
02:05:33 <Sgeo> Does Python have a better looping operator?
02:05:46 <Sgeo> Python for is more aptly described as foreach
02:06:03 <Bike> why do people expect the variable to be rebound, i honestly don't get it
02:06:40 <Sgeo> Because in good languages it is?
02:06:44 <elliott> sure seems like mutability causes a lot of bugs and misconception due to its fundamentally bad nature for structuring programs huh
02:06:50 <Bike> in C it's an obvious goto loop, in Python it's a slightly less obvious goto loop
02:07:05 <Bike> imo shut your face elliott
02:07:09 <elliott> Bike: are you even like a lisper. what are you
02:07:18 <Sgeo> Common Lisper I think
02:07:19 <elliott> choose your fucking side so I can shoot you if it's the wrong one
02:07:33 <Bike> why is it "wrong"
02:07:41 <elliott> sounds like you're afraid of judgement
02:07:44 <elliott> ps this isnt even about the for loop any more
02:07:48 <elliott> I just want to know whether to hate you or not
02:07:50 <Bike> it sets the fucking variable, you're using fucking python, you know what assignment is
02:07:53 <elliott> it's a good thing to know right
02:07:53 <Bike> just hate me ok
02:08:03 <elliott> feed me the information!!!!
02:08:09 <Bike> I'M RIGHT HERE
02:08:24 <Jafet> Is this what gay sex is like
02:08:32 <Bike> it's a sad, sad sight
02:09:06 <elliott> Bike: so I'm just going to take Sgeo's word and assume you're a CLer unless you state otherwise
02:09:13 <Bike> Sgeo: also the example is always that "what if want to accumulate a list of closures in a loop" thing that i've never seen in real code but i guess somebody might use it somewhere???
02:09:13 <elliott> I can understand why you wouldn't say it yourself since it's pretty embarrassing
02:09:29 <Bike> hm i think i should make some anti-scheme joke here but i don't know any
02:09:38 <elliott> well have you ever read the CL spec
02:09:54 <Jafet> elliott is scared of the hyper.
02:09:56 <Sgeo> Bike, I'm working on a problem (for some website that does stuff) and I want to accumulate a list of closures.
02:09:57 <Bike> well, the hyperspec, not ansi, i don't have money
02:09:58 <elliott> also there's the thing where your language isn't elegant *or* practical!!
02:10:11 <Sgeo> Not really in a for loop particularly, but the corresponding list comprehension also had that issue
02:10:14 <elliott> pretty bad place to be in imo
02:10:32 <Jafet> Yeah, common lisp is so bad, even paul graham doesn't use it
02:10:44 <Jafet> It feels, like, a hundred years old
02:10:47 <shachaf> Sgeo: What's the language du jour?
02:11:05 <Bike> Sgeo: why. explain
02:11:08 <Sgeo> shachaf, codeeval doesn't accept Smalltalk solutions nor Racket solutions
02:11:29 <Sgeo> Bike, want to take a tuple and for each of 4 directions get a new tuple
02:11:49 <shachaf> monoids monoids monoids monoids monoids monoids
02:11:55 <Sgeo> Maybe I forgot how to think imperatively
02:11:56 <Bike> so what are you closing over
02:12:23 <Bike> why don't you just accumulate the tuples?
02:12:25 <elliott> Bike: also there's the thing whereby people call CL a functional language.
02:12:33 <Bike> elliott: trust me that annoys us too
02:12:35 <Sgeo> `quote common.lisp
02:12:39 <elliott> Bike: yes but then the thing is...
02:12:44 <HackEgo> 31) <ehird> is there a problem with it being carbonized :D <augur> yes: carbonized coffee bean is known more commonly as "charcoal" \ 616) <ais523> Just about all females often feel that exactly why all Hollywood stars common maintain its brightness as Tom in spite of frantic operate routine and large operate pressure from the skin. What do you th
02:12:46 <elliott> Bike: the joke is on you for using a language that isn't functional
02:13:01 <Bike> how could i be so wrong
02:13:08 <HackEgo> 54) <Sgeo> What else is there to vim besides editing commands? \ 68) <Sgeo|web> Where's the link to the log? <lament> THERE'S NO LOG. YOUR REQUEST IS SUSPICIOUS AND HAS BEEN LOGGED. \ 101) <pikhq> And... WTF is it doing. <pikhq> :( <Sgeo_> Is it sexing? \ 110) <coppro> what's the data of? [...] <Sgeo> Locations in a now deceased game called Muta
02:13:19 <shachaf> Bike: i heard your language of choice doesn't use {- -} comments.............................................
02:13:40 <Bike> i thought if you talked about comment syntax kmc punched you until you were dead.
02:13:42 <elliott> Bike: lo, you think you have transcended the blub, but nay, i knoweth the blub that surpasseth even that which paul graham divined
02:13:45 <elliott> ps it's common lisp haskell forever
02:14:05 <elliott> higher up in the language food chain than you yes
02:14:06 <Sgeo> He's high on functional programming
02:14:22 <shachaf> Bike: btw haskell is the worst language
02:15:10 <Bike> for the record, i didn't mention i usually use CL because language arguments are dumb and i think everyone here is well aware of that and i'd rather listen to bizarre-ass jokes about oh let's say intuitionistic logic
02:15:20 <Bike> in-jokes, rather
02:15:27 <elliott> sorry but i need the occasional flamewar
02:15:34 <HackEgo> 616) <ais523> Just about all females often feel that exactly why all Hollywood stars common maintain its brightness as Tom in spite of frantic operate routine and large operate pressure from the skin. What do you think that they have got sufficient time to observe all attractiveness strategies and tips that his grandmother utilized to abide by?
02:15:41 <elliott> like i still respect you as a person
02:15:48 <elliott> i just have to hate you for being a cl user
02:15:49 <Bike> haha that's funny
02:16:03 <Phantom__Hoover> 'elliott ruined me with constructivism' part 7: i have a logic module this term
02:16:16 <elliott> Bike: by the way by "usually use CL" do you mean "pretend to use CL on IRC because nobody actually uses it for real programs" 8)
02:16:20 <scarf> elliott: apart from wrt DCSS, is there anything we really disagree with each other on, to flamewar levels?
02:16:32 <elliott> scarf: do you acknowledge that @ is the best thing in the universe
02:16:37 <shachaf> Bike, on the other hand, hates elliott as a person but respects him for being a Haskell user.
02:16:40 <monqy> roguelike design in general?
02:18:10 <ion> I actually played a few minutes of Crawl this week.
02:18:12 <Bike> elliott: to be serious for half a second, it's because as a dumbass undergrad i don't really have "real programs" to write anyway, and i don't know shit about "real programs".
02:18:14 <ion> for the first time in months
02:18:35 <elliott> Bike: wow way to give away your approximate age range
02:18:39 <elliott> where's the fucking mystery Bike
02:18:42 <shachaf> Bike: elliott doesn't write "real programs" either.
02:18:44 <elliott> you don't appreciate subtlety. JUST LIKE COMMON LISP
02:18:52 <Bike> i know, shachaf.
02:18:56 <shachaf> elliott: That doesn't give your age range away?
02:19:08 <shachaf> shapr is an undergrad and he's 40-something.
02:19:11 <Bike> real programs are only written by the hardcorest of AI lab hackers, on mount esr
02:19:32 <Bike> hm this reminds me that i should look at those ancient AI programs written in CL again
02:19:33 <elliott> shachaf: It does modulo outliers?
02:19:37 <Bike> (they are completely fucking unreadable)
02:20:10 <shachaf> Anyway should I be an undergrad?
02:20:22 <monqy> being an undergrad isn't so great
02:20:27 <Bike> Being an undergrad sucks, just learn metalworking or something instead.
02:20:42 <Fiora> bike is younger than me actually :P
02:20:52 <Bike> Aren't you like 600 years old?
02:21:04 <elliott> shachaf: aren't you like 21
02:21:05 <Bike> Not familiar with reptilian aging honestly.
02:21:12 <Fiora> stop making fun of me, I'm not that old ;-;
02:21:27 <shachaf> monqy: are you an overgrad
02:21:36 <Bike> You don't look a day over 500, babe
02:21:36 <monqy> shachaf: depends on how you look at it
02:21:38 <shachaf> in soviet russia, are you a leningrad
02:21:48 <monqy> i don't know what that is
02:22:48 <Bike> imo volgograd > leningrad
02:22:49 <Fiora> ... I'm only 23... that's... not really old...
02:22:55 <shachaf> Fiora: uhh that's pretty old
02:23:08 <shachaf> most mathematicians are burnt out by the time they're 23
02:23:11 <Bike> Fiora, did you ever meet Lincoln?
02:23:19 <Bike> He knew like everybody right?
02:23:23 <shachaf> Fiora: galois was dead for 3 years by the time he was your age "fyi"
02:23:43 <Bike> Also he had true love. Do you have true love, Fiora?
02:24:16 <Bike> well, and something about polynomials, i guess
02:25:30 <monqy> lots of things are named after galois
02:25:56 <Bike> Have you ever looked at Wikipedia's article on things named after Euler?
02:25:58 <elliott> monqy: galois was named after galois for example
02:26:01 <Bike> Sometimes I open it and just sob.
02:26:14 <monqy> lots of things are named after Euler too yes
02:26:20 -!- WeThePeople has joined.
02:26:29 <shachaf> what about things named after
02:26:31 <FreeFull> Project Euler, euler's constant, euler-something constant, euler euler euler
02:26:48 <Bike> de bruijn's name is probably cooler than euler's and galois's combined, yeah
02:26:51 <Fiora> I remember in complex analysis every single thing in the class had cauchy's name on it
02:26:56 <monqy> a few things are named after de bruijn
02:26:58 <Fiora> (I'm barely exaggerating)
02:27:05 <Bike> i also really like Catalan for some reason
02:27:08 <shachaf> DE BRUIJN: "COOLEST MATHEMATICIAN"????? "IMO YES"
02:27:13 <Bike> maybe because Catalonia is a mystical Spanish thing i don't understand
02:27:25 <Bike> (also because combinatorics is pretty cool, imo)
02:27:43 <Bike> Shachaf, this is not a special occasion.
02:28:01 <Bike> Combinatorics is not easy!
02:28:14 <Bike> You were implying it.
02:28:19 <Bike> Utterances have context, shachaf!
02:28:23 <Bike> Horrible, horrible contexts.
02:28:36 <Jafet> Combinatorics is easy
02:28:53 <shachaf> Bike: Given that I *refrained* from saying it was easy, you might infer that I was implying the opposite.
02:28:53 <Bike> Fiora: Cauchy also has an advantage in that the Cauchy integral formula is the coolest thing to come out of math since negation
02:28:59 <shachaf> Bike: Also I don't know much about combinatorics. :-(
02:29:06 <Bike> It's "pretty cool, imo"
02:29:16 <Bike> google Analytic Combinatorics, it's free and also awesome.
02:29:21 <shachaf> Bike: did you know combinatorics is related to, like, types
02:29:31 <Bike> Isn't everything related to, like, types?
02:29:39 <shachaf> Combinatorics comes up a lot.
02:30:12 <Bike> Maybe I should actually finish A=B (as if i'd understand it)
02:30:22 <elliott> Bike: what kind of negation are we talking here
02:30:35 <Bike> or find some hip new book on combinatypics, thus earning back the trust of this channel
02:30:47 <Bike> elliott: the kind with numbers that are "less than" "zero"
02:30:49 <elliott> Bike: man, Zeilberger, am I right?
02:30:54 <elliott> oh I hate that kind of negation
02:30:57 <Bike> You are, like, so right, man.
02:30:57 <elliott> logical ngeation is cool though
02:31:12 <Bike> I thought you were a constructivist!!!
02:31:26 <shachaf> Bike: Actually there's remarkably little information about it. :-(
02:31:29 <Jafet> Those guys are pretty far left
02:31:35 <shachaf> You should become a combiantorist-turned-type-theorist and publish papers.
02:31:42 <FreeFull> shachaf: Ramanunjan was pretty cool
02:31:44 <Jafet> Intuitionist hippies
02:31:51 <Bike> elliott: "pretty cool, imo"
02:31:55 <shachaf> elliott: what about (α → ⊥) → ⊥
02:31:59 <elliott> Bike: because negation is like
02:32:10 <Bike> I actually don't think I'm going to go into math. If I can work types into what I want to do all the better though.
02:32:23 <Bike> Hm, I can't decide if I hate Zeilberger's webpage.
02:32:35 <FreeFull> Invent a function that does _|_ -> a
02:32:52 <elliott> whoa zeilberger has a new webpage
02:32:57 <elliott> since the last time I saw it
02:32:58 <Jafet> Tort law IN THE TYPE SYSTEM
02:33:01 <Bike> On the one hand it's a trillion percent better than the average academic site. On the other, he knows what I did last summer, and in many of my previous lives.
02:33:12 <Bike> And he does not take prisoners.
02:33:16 <oerjan> <Bike> maybe because Catalonia is a mystical Spanish thing i don't understand <-- don't tell the catalonians they are spanish hth
02:33:21 <elliott> Bike: this website used to be much better
02:33:26 <elliott> in terms of visual appearance
02:33:29 <FreeFull> Is Haskell's type system turing-complete?
02:33:43 <Bike> oerjan: I assumed.
02:33:50 <Bike> FreeFull: What would that mean
02:34:03 <Bike> inference is computable isn't it
02:34:10 <Bike> except for some weird types that are maybe ghc only?
02:34:17 <Bike> "I just don't know"
02:34:19 <elliott> Bike: i refer to http://web.archive.org/web/20110614084818/http://www.math.rutgers.edu/~zeilberg/
02:34:28 <Jafet> @google ghc undecidable
02:34:30 <lambdabot> http://hackage.haskell.org/trac/haskell-prime/wiki/UndecidableInstances
02:34:30 <lambdabot> Title: UndecidableInstances – Haskell Prime
02:34:32 <shachaf> Bike: GHC's type system is a very different thing from Haskell's.
02:34:33 <elliott> Bike: ps YOUR IGNORANCE IS TYPICAL OF ONE WHO USES A LANGUAGE WITH A HORRENDOUSLY CRIPPLED TYPE SYSTEM
02:34:37 <Bike> shachaf: I know.
02:34:55 <Bike> elliott: does haskell have types with uncomputable membership??? don't think so
02:35:07 <elliott> Bike: what does uncomputable mean here
02:35:12 <Bike> elliott: ok i like his new site better jesus christ is this green on blue
02:35:32 <Bike> elliott: you can express russell's paradox in the type system! "yay"
02:35:50 <Bike> Or well, the set in question, I suppose.
02:35:51 <oerjan> Bike: also don't tell the spanish the catalonians _aren't_ spanish, hth
02:35:59 <Bike> oerjan: Again, somehow I expected this.
02:36:07 <Bike> sleep sucks imo
02:36:43 <Fiora> sleep is wonderful and you should do it
02:36:54 <elliott> Fiora: but it's also kind of terrible!!!
02:36:59 <elliott> because when you're asleep it means you're not awake, see
02:37:15 <Phantom__Hoover> hey elliott remember back when i was terrified of sleeping
02:37:30 <FreeFull> I don't get why Bool is an instance of Ord but ok
02:37:32 <shachaf> elliott: hey want to do the thing
02:37:32 <Bike> elliott: If it would help I could link you a paper on injecting yourself with things that maybe don't actually remove pain in surgery, and then you couldn't sleep.
02:37:35 <elliott> Phantom__Hoover: one day you will die : )
02:37:56 <Bike> oerjan: So, plot twist. Turns out Catalan... is Belgian.
02:38:00 <shachaf> elliott: (actually not now but later so maybe not because maybe you'll be asleep but who knows)
02:38:00 <elliott> it',zs a threat.... from mother nature
02:38:13 <FreeFull> > foldr max [False,False,True]
02:38:14 <Bike> Or well, was. He died at some point I guess?
02:38:23 <FreeFull> > foldr max [] [False,False,True]
02:38:23 <elliott> Bike: why would I inject myself with something that maybe doesn't actually remove pain!!
02:38:24 <lambdabot> Couldn't match expected type `[a0]'
02:38:27 <elliott> I'm not even going to have a surgerys
02:38:30 <FreeFull> > foldr max False [False,False,True]
02:38:30 <oerjan> Bike: don't tell the belgians they are spanish either.
02:39:35 <Jafet> > foldr max False $ replicate (10^6) False
02:39:49 <Jafet> > foldr max False $ replicate (10^7) False
02:40:27 <elliott> Bike: THE MYSTERY IS KEEPING ME AWAKE HELP
02:40:32 <Jafet> > maximum $ replicate (10^7) False
02:40:45 <Jafet> "Haskell is awesome"
02:40:56 <Jafet> > max undefined True
02:40:58 <FreeFull> oerjan: Max isn't lazy on the second argument
02:41:33 <elliott> > max (undefined :: ()) (undefined :: ())
02:41:36 <FreeFull> How would you do a lazy compare?
02:41:39 <elliott> > max (undefined :: ()) ()
02:41:43 <elliott> > max (()) (undefined :: ())
02:41:47 <elliott> ugh, it behaves badly there
02:41:48 <oerjan> > compare True undefined
02:41:56 <elliott> looks like the derived instances suck
02:41:57 <oerjan> > compare False undefined
02:42:02 <elliott> FreeFull: for instance, compare _ _ = EQ
02:42:07 <oerjan> > compare undefined True
02:42:12 <oerjan> > compare undefined False
02:42:37 <elliott> oerjan: don't worry. @ definitions are maximally lazy.
02:42:42 <lambdabot> (<), (<=), (>), (>=) :: a -> a -> Bool
02:42:42 <FreeFull> elliott: Wouldn't that only be after the other pattern matches though
02:42:54 <elliott> there is only one value of type ()
02:43:31 <Jafet> > (\(\() -> ()) -> ()) ()
02:43:33 <lambdabot> <hint>:1:4: Parse error in pattern: \ () -> ()
02:43:50 <Jafet> > (\((\() -> ()) -> ()) -> ()) ()
02:44:04 <oerjan> elliott: they should use amb for full effect
02:44:15 <elliott> who needs performance or sanity
02:44:17 <FreeFull> () is great for base zero arithmetic
02:44:33 <FreeFull> Just have to define a num instance
02:44:43 <Jafet> () is the counterpart to _|_
02:45:52 <lambdabot> help <command>. Ask for help for <command>. Try 'list' for all commands
02:45:55 <lambdabot> http://code.haskell.org/lambdabot/COMMANDS
02:47:00 <FreeFull> You can't define an instance in a let expression, can you
02:47:30 <Jafet> https://github.com/ekmett/reflection/blob/master/examples/Monoid.hs
02:47:36 <Jafet> "unless you're edwardk"
02:48:18 <Bike> oerjan: I'm starting to sense a pattern.
02:48:19 <FreeFull> Want to make a Num instance for ()
02:48:33 <Bike> elliott: Well, the chemical shuts down your muscles. That's basically like sleep, right?
02:49:21 <oerjan> Bike: the spanish were big on conquering things, hth
02:50:02 <FreeFull> instance Num () where { ()+()=(); ()*()=(); negate ()=(); abs ()=(); signum ()=(); fromInteger _ =(); }
02:50:42 <Bike> oerjan: Am I allowed to tell conquering things that they are Spanish?
02:50:45 <Jafet> That is the worst instance ever
02:50:53 <Jafet> It's not at all lazy
02:51:07 <Bike> but it forms a group!!!
02:51:12 <elliott> Bike: you use two spaces afte ra . too
02:51:15 <elliott> you disgust me. should i sleep
02:51:17 <Bike> hell maybe a ring, i forget
02:51:27 <Bike> elliott: I READ IT IN A STYLE GUIDE ONCE OKAY
02:51:33 <Jafet> Actually Num has no laws but okay
02:52:03 <Bike> who needs laws when we have axioms
02:52:06 <FreeFull> instance Num () where { _+_=(); _*_=(); negate _=(); abs _=(); signum _=(); fromInteger _ =(); }
02:52:31 <Bike> good instance imo
02:53:02 <elliott> Bike: style guide more like
02:53:20 <Jafet> New Num instances are approved by a jury panel who give it a three-part score on originality, aesthetic merit, and use of applicative functors
02:53:23 <Bike> whoa man that hurts :(
02:53:27 <monqy> shachaf: was that a disapproving hi
02:53:38 <shachaf> monqy: no it was an "im back hi"
02:53:44 <FreeFull> _ must be treated specially when next to other +"&$*"£!"*
02:53:44 <shachaf> monqy: Not every hi has to be disapproving!
02:53:45 <Bike> hello i am here
02:54:43 <Jafet> instance Num () where (+)=const$const undefined; (*)=const$const undefined; negate=const undefined; abs=const undefined; signum=const undefined; fromInteger=const undefined
02:55:09 <Bike> aesthetically unmeritous sorry
02:55:24 <FreeFull> () is the wrong kind for Functor
02:56:19 <FreeFull> So can't be Applicative either ):
02:56:25 <Bike> "Later, in 1849, Catalan was visited at his home by the French Police, searching for illicit teaching material;"
02:56:53 <monqy> FreeFull: how about Const ()
02:57:05 <monqy> FreeFull: how about Proxy
02:57:27 <shachaf> monqy: did you hear Proxy was in base briefly but now they're maybe taking it out again
02:57:27 <zzo38> But something that is the correct kind for Functor is the wrong kind for Num.
02:57:49 <Bike> how many fucking bot prefixes are the- oh.
02:59:48 <shachaf> Bike: newtype Const a b = Const a
03:00:20 <zzo38> Some of the names I don't like much so I would prefer Finalize instead of Proxy, Succ instead of Maybe, Nat8 instead of Word8, and so on. But, I don't know, what is your opinions of such things?
03:00:25 <oerjan> Bike: sounds unwise hth
03:00:38 <Bike> that seems like a weird type but what do I know? that's right NOTHING *sobs*
03:00:40 <Bike> oerjan: thanks
03:01:12 <shachaf> Bike: It's even an Applicative functor.
03:01:29 <zzo38> instance (Monoid x) => Alternative (Const x) actually you can have too.
03:02:21 <oerjan> <FreeFull> _ must be treated specially when next to other +"&$*"£!"* <-- _ belongs to the alphanumeric group of characters, not the operator ones
03:02:34 <zzo38> Const does have another meaning too, which is that (Codensity (Const x)) is like (Cont x)
03:03:58 <FreeFull> I wanted to know where Const is defined though
03:04:18 <lambdabot> Source not found. My pet ferret can type better than you!
03:04:23 <zzo38> And (Density (Const x)) like (Store x)
03:04:57 <lambdabot> The operator `Control.Applicative.Const' [infixl 9] of a section
03:05:04 <oerjan> FreeFull: there you go
03:05:11 <zzo38> And (CodensityAsk (Const x)) like ((->) x)
03:05:20 <oerjan> ...@hoogle might have been easier, mind you.
03:05:32 <lambdabot> Data.Function const :: a -> b -> a
03:05:32 <lambdabot> Control.Applicative Const :: a -> Const a b
03:06:00 <Bike> So does Haskell have S built in too
03:06:06 <FreeFull> oerjan: Heheh, using a syntax error
03:06:21 <lambdabot> The function `Debug.SimpleReflect.Vars.t'
03:06:31 <zzo38> And even, (Free (Const x)) like (Either x)
03:06:58 <FreeFull> Could not find module `Control.Applicative.Const'
03:07:48 <zzo38> So, it actually makes a lot of things!
03:08:28 <Bike> zzo, this would mean a lot more to me if I understood anything, but I don't.
03:09:10 <lambdabot> Ambiguous type variable `a0' in the constraints:
03:09:20 <lambdabot> Monad m => m (a -> b) -> m a -> m b
03:09:24 <shachaf> > ap (f :: Expr -> Expr) (g :: Expr -> Expr) x :: Expr
03:09:26 <lambdabot> Couldn't match expected type `a0 -> Debug.SimpleReflect.Expr.Expr'
03:09:37 <shachaf> > ap (f :: Expr -> Expr -> Expr) (g :: Expr -> Expr) x :: Expr
03:09:47 -!- Phantom__Hoover has quit (Remote host closed the connection).
03:10:02 <FreeFull> > let x 0 = x 0; x n = (x (n-1),x (n-1)) in x 3
03:10:05 <lambdabot> Occurs check: cannot construct the infinite type: t1 = (t0, t1)Occurs check...
03:10:31 <FreeFull> > let x 0 = x 0; x n = (x (n-1),()) in x 3
03:10:33 <lambdabot> Occurs check: cannot construct the infinite type: t0 = (t0, ())
03:10:51 <shachaf> kmc: Did you know if you press G in less while you're looking at a file it'll read to the end, tail -f-style?
03:11:00 <FreeFull> > let x 0 = x 0; x n = ((),()) in x 3
03:11:03 <shachaf> (It also has actual tail -f mode, of course.)
03:11:06 <FreeFull> > let x 0 = x 0; x n = ((),()) in x 0
03:11:14 <kmc> i was looking for that the other day
03:11:30 <zzo38> Can there be any monoid (not monad) transformers which is not applicative?
03:11:34 <shachaf> FreeFull: What are you playing at?
03:12:21 <oerjan> <FreeFull> Could not find module `Control.Applicative.Const' <-- that's the whole qualified name, not the module
03:12:39 <kmc> what's a monoid transformer?
03:13:30 <kmc> maybe 'composition' and 'direct product' are monoid transformers?
03:14:29 <shachaf> Transformers are annoying. :-(
03:14:36 <kmc> seems like there shouldn't be very many monoid transformers
03:14:37 <shachaf> Applicatives don't need transformers.
03:16:27 <zzo38> I don't mean applicative transformers. But applicatives make monoid transformers too.
03:18:32 <kmc> so what is a monoid transformer?
03:21:01 <shachaf> I guess this is a language more sexist than Hebrew?
03:21:03 <shachaf> The language is best known for its system of noun classes, numbering four in total. They tend to be divided among the following semantic lines:
03:21:06 <shachaf> I - most animate objects, men
03:21:08 <shachaf> II - women, water, fire, violence, and exceptional animals[3]
03:21:11 <shachaf> III - edible fruit and vegetables
03:21:13 <shachaf> IV - miscellaneous (includes things not classifiable in the first three)
03:21:27 <Bike> that sounds like it was probably misunderstood by whoever wrote that down.
03:21:31 <Bike> also, how's Hebrew sexist?
03:22:16 -!- oerjan has quit (Quit: Ribbit).
03:23:18 <Bike> I mean, is it just gendered nouns or what.
03:23:37 <FreeFull> instance Monoid a => Monoid (Foo a) where { mempty = mempty; mappend x y = mappend x y; mconcat xs = mconcat xs; }
03:24:15 -!- DHeadshot has quit (Read error: Connection reset by peer).
03:24:21 -!- DH____ has joined.
03:25:57 -!- oerjan has joined.
03:27:27 <FreeFull> Ok, trying again where nothing is bottom
03:28:20 <FreeFull> Wait, you don't have to do mconcat to have a monoid, do you
03:28:29 <lambdabot> Source not found. Do you think like you type?
03:28:50 <monqy> FreeFull: there's a default instance for mconcat; it's just there in case you want to provide a more efficient implementation
03:29:01 <FreeFull> instance Monoid a => Monoid (Foo a) where { mempty = Foo (mempty); mappend (Foo x) (Foo y) = Foo (mappend x y);
03:29:02 <monqy> instance/implementation/whatever
03:29:05 <Jafet> What is mconcat anyway
03:29:22 <Bike> mappend But On Lists i assume...
03:29:45 <Bike> would it be silly to ask why the monoidal operation is called append
03:30:09 <FreeFull> It is actually an append for Monoid [a]
03:30:44 <lambdabot> (), (a -> b), (a, b), (a, b, c), All, Any, Dual a, Endo a, First a, Last a, Maybe a, Ordering, Product a, Sum a, [a]
03:30:48 <FreeFull> Funny, apparently () is an instance of Monoid already
03:30:56 <monqy> what's funny about it
03:31:29 <Bike> huh, now i understand why groups are categories of one object or whatever. weird.
03:31:33 <Jafet> It's like a clown. Some people think clowns are funny
03:31:45 <Bike> i wonder if i'll ever understand grothendieck. do you understand grothendieck?
03:31:52 <lambdabot> Control.Applicative unwrapMonad :: WrappedMonad m a -> m a
03:31:59 <monqy> Bike: do you mean monoids are categories with one object, or groups are groupoids with one object?
03:32:19 <Bike> monoids are categories with one object.
03:32:23 <Bike> and "A group is a category with one object, in which all morphisms have inverses."
03:32:42 <Jafet> @quote groupoidoid
03:32:42 <lambdabot> No quotes match. Are you on drugs?
03:32:53 <lambdabot> <shachaf> says: And a semigroupoid with identities is called a monoidoid.
03:33:18 <Bike> mathematicians, literally the worst at naming things
03:34:04 <Bike> yes, and that's a shitty way to name things.
03:34:22 <Bike> Just look at Pacific islands. ridiculous
03:34:27 <FreeFull> a semiapple with identity syndrome is called a blanabba
03:34:43 <c00kiemon5ter> I know! lets name this method, "Newton's method" ! It will be unique
03:35:04 <Bike> does identity syndrome have a cure ._.
03:36:21 <oerjan> applying any cure to the identity syndrome just gives you the cure back.
03:37:18 <FreeFull> Obviously CherryT Apple has no identity
03:37:39 <Jafet> You can inject yourself, but they say it is just homeomorphy.
03:38:54 <FreeFull> raisins are just grapeoids in the cat allegory of endocarpum
03:39:12 <monqy> aren't puns supposed to make sense
03:39:55 <tswett> Stupid proof of the day:
03:40:25 <tswett> Every countable ordinal number can be embedded in the rational numbers. The union of all countable ordinal numbers is uncountable. Therefore, the rational numbers are uncountable.
03:41:39 <Jafet> Math should get a checkmate symbol
03:42:35 <shachaf> Jafet: Only constructivists have that.
03:42:39 <shachaf> It's called type-checkmate.
03:42:49 <monqy> ''nice one shachaf``
03:43:02 <FreeFull> lenght $ [0] ++ ((%) <$> [1..] <*> [1..]) ++ ((%) <$> [(-1),(-2)..] <*> [1..])
03:43:11 <shachaf> monqy: wow whats with the new quotes
03:43:16 <Bike> MATHEMATICAL_DOUBLE-STRUCK_CAPITAL_CHECKMATE
03:43:35 <tswett> Apparently the "mates" in this case are lesbians.
03:44:01 <tswett> Bike: you make a good point. The word "lesbian" *is* verbose.
03:44:25 <tswett> The Han character for "protrude"?
03:44:29 <lambdabot> Perhaps you meant `R.%' (imported from Data.Ratio)
03:45:06 <Jafet> Han mandarin pictograph for "fuck you"
03:45:17 <Sgeo> FreeFull, I think that doesn't work out the way you expect
03:45:22 <myndzi> concave in japanese anyway
03:45:32 <myndzi> one of the few i got around to learning
03:45:40 <Sgeo> There exist rationals R that will not show up aftr any finite time T
03:45:47 <myndzi> i tend to confuse the two
03:45:54 <Sgeo> It's because the List monad sucks.
03:46:42 <FreeFull> Sgeo: unrepresentable integers?
03:46:58 <FreeFull> Also, I knwo there would be duplicate numbers with this code
03:47:07 <Sgeo> FreeFull, just the ordering in which the List monad operates
03:47:15 <Bike> hopefully. he's got a looooot of curare in 'im.
03:47:27 <FreeFull> Well, obviously it wont' work for infinite lists like this
03:47:43 <Sgeo> > take 20 $ (,) <$> [0..] <*> [0..]
03:47:44 <lambdabot> MonadLogic m => m a -> (a -> m b) -> m b
03:47:45 <lambdabot> [(0,0),(0,1),(0,2),(0,3),(0,4),(0,5),(0,6),(0,7),(0,8),(0,9),(0,10),(0,11),...
03:47:47 <monqy> > [1,2,3] >>- \ a -> [a, a+1]
03:47:58 <monqy> ok that was a bad example
03:48:19 <shachaf> since when does lambdabot have >>-
03:48:31 <monqy> shachaf: as long as i can remember
03:48:37 <Bike> it's an exciting time for caleskell development
03:48:40 <shachaf> monqy: wow how come i never knew about it
03:49:19 <monqy> > [0..] >>- \ a -> [0..] >>- return . (a,)
03:49:20 <lambdabot> Illegal tuple section: use -XTupleSectionsPrecedence parsing error
03:49:50 <monqy> > [0..] >>- \ a -> [0..] >>- \ b -> [(a,b)]
03:49:52 <lambdabot> [(0,0),(1,0),(0,1),(2,0),(0,2),(1,1),(0,3),(3,0),(0,4),(1,2),(0,5),(2,1),(0...
03:50:08 <Bike> ooh i love that function
03:50:19 <monqy> > "hello" `interleave` "goodbye"
03:50:27 <Sgeo> tswett, like bind except handles the multiple infinite lists thing properly
03:51:37 <Bike> > [0..] >>= \a -> [0..] >>= \b -> [(a,b)]
03:51:39 <lambdabot> [(0,0),(0,1),(0,2),(0,3),(0,4),(0,5),(0,6),(0,7),(0,8),(0,9),(0,10),(0,11),...
03:51:52 <tswett> Sgeo: well, this way of doing it isn't necessarily more proper.
03:52:03 <Bike> yeah, sometimes you want one and sometimes you want the other
03:52:03 <shachaf> > ("hello","goodbye")^..levels (both.traverse).traverse
03:52:05 <lambdabot> It could refer to either `Data.Tree.levels',...
03:52:06 <shachaf> > ("hello","goodbye")^..Lens.levels (both.traverse).traverse
03:52:17 <Bike> very elegant, shachaf.
03:52:26 <shachaf> Bike: It's actually disgusting.
03:52:29 <shachaf> "sorry to break it to you"
03:52:43 <tswett> I take it . binds more tightly than ^..
03:52:51 <monqy> . binds prettty tightly
03:53:10 <Bike> ^.. is a p. good operator name
03:53:30 <shachaf> monqy: but how tight does the . in Lens.levels bind
03:53:46 <Bike> can't you just look it up
03:53:46 <monqy> not-an-operator-tight
03:54:09 <Bike> :t both.traverse
03:54:09 <shachaf> btw i always forget what precedence means
03:54:10 <lambdabot> (Applicative f, Traversable t) => (a -> f b) -> (t a, t a) -> f (t b, t b)
03:54:11 <monqy> how tight does the . in "hello." bind?????
03:54:20 <shachaf> so i like to call it stickiness
03:54:21 <Bike> :t both . traverse
03:54:22 <monqy> conclusion: very tight
03:54:23 <lambdabot> (Applicative f, Traversable t) => (a -> f b) -> (t a, t a) -> f (t b, t b)
03:54:32 <shachaf> monqy: well tighter than "
03:54:48 <lambdabot> (Applicative f, Traversable t) => (a -> f b) -> (t a, t a) -> f (t b, t b)
03:55:13 <shachaf> that's like gravity or something??
03:55:33 <monqy> a bond tight enough to overcome separation
03:56:26 <shachaf> > [0..] >>- \ a -> [0..] >>- return . (,) a
03:56:28 <lambdabot> cannot mix `Control.Monad.Logic.Class.>>-' [i...
03:56:31 -!- Bike_ has joined.
03:56:47 -!- Bike has quit (Disconnected by services).
03:56:52 -!- Bike_ has changed nick to Bike.
03:57:26 <Bike> Hachaf. Hatchet?
03:57:49 <shachaf> i love monoidoidoidoidoidoidoids
03:58:39 <tswett> It's like a monoid, but more specific.
03:59:21 <tswett> Maybe it's a commutative monoid.
03:59:56 <Bike> I think "mon" would be a better name than "abelian monoid"
04:00:02 <shachaf> or is it a communist monoid??
04:00:02 <Bike> but probably worse than "commutative monoid"...
04:00:20 <tswett> What would it mean for an operation to be mmutative?
04:00:33 -!- Nisstyre-laptop has quit (Remote host closed the connection).
04:00:59 <shachaf> tswett: I assume some instances of mposition are mmutative.
04:01:06 <shachaf> I worked out what mposition was once.
04:01:17 <shachaf> It turns out you can't really do it in Haskell because parametricity??
04:01:18 <Jafet> It operates on your computer's commu
04:01:31 <monqy> what's mposition shachaf
04:01:32 <tswett> Are instances of composition commutative?
04:01:42 <shachaf> monqy: um it's that weird thing
04:02:02 <shachaf> p b a -> Either (p x a) (p b x)
04:02:22 <shachaf> monqy: "i didn't invent it it came up on its own"
04:02:30 <Bike> that's what they all say
04:02:49 <Jafet> "It should still be named after me though"
04:02:59 <Bike> "A monoid for which the operation is commutative for some, but not all elements is a trace monoid; trace monoids commonly occur in the theory of concurrent computation."
04:03:20 <monqy> what does it mean by "for some but not all"
04:03:32 <Jafet> The "some of all" fears
04:03:49 <monqy> is this like it has a subsemigroup thats all commutative and stuff amongst itself, or is it more like the center of a group where the stuff in it commutes with everything
04:04:20 <Bike> "It generalizes the concept of a string, by not forcing the letters to always be in a fixed order, but allowing certain reshufflings to take place."
04:04:39 <Bike> the mathematical structure i've always dreamed of. "like a string but less so"
04:04:48 -!- TeruFSX has joined.
04:04:59 <monqy> gosh i hope they bothered to actually define it well
04:05:03 <Bike> I have no idea why you would ever want this.
04:05:09 <FreeFull> Bike: Call it an Amstringytoope
04:05:11 <Bike> " Traces are used in theories of concurrent computation, where commuting letters stand for portions of a job that can execute independently of one another, while non-commuting letters stand for locks, synchronization points or thread joins."
04:05:20 <Bike> I... guess that sort of makes sense?
04:05:53 <Jafet> Letters? I bet this theory was invented by Post.
04:06:07 <Bike> why would post give a damn about concurrency
04:06:11 <tswett> FreeFull: I dunno, I want to erode that word to "anstrintope".
04:06:20 <Bike> By the way, did you know Post only had one arm? I didn't know that.
04:06:45 <Jafet> That would explain why his computation models are so simple.
04:06:53 <tswett> And the word "anstrintope" looks like it would mean...
04:07:07 <Bike> that's right, cripple joke! woo woo
04:07:15 -!- yorkdove has joined.
04:07:50 <Bike> Hm, someone named Mazurkiewicz is cited. That's a pretty cool name.
04:07:55 <Bike> Imo all mathematicians should be Polish.
04:07:57 <Jafet> English doesn't have a word for discrimination towards cripples
04:08:01 <tswett> "Place not bound tightly".
04:08:09 <tswett> Jafet: does "ableism" count?
04:08:09 <Jafet> (Therefore it doesn't exist)
04:08:11 <Bike> Jafet: "ableism"
04:08:19 <lambdabot> *** "ableism" wn "WordNet (r) 3.0 (2006)"
04:08:19 <lambdabot> n 1: discrimination in favor of the able-bodied [syn: {ableism},
04:08:19 <lambdabot> {ablism}, {able-bodiedism}, {able-bodism}]
04:08:34 <Jafet> "That's not even a word"
04:08:41 <Bike> Also, "cripple" is a slur, I probably shouldn't have said it.
04:09:30 <Bike> "While the trace monoid had been studied by Pierre Cartier and Dominique Foata for its combinatorics in the 1960s," oh that sounds actually interesting.
04:09:55 <Bike> hm, Schützenberger. I think I can allow German mathematicians in addition to the Polish ones.
04:09:56 <monqy> so trace monoid looks kinda funny. i follow the part where you quotient the free monoid over some set by some equivalence relation, but the properties of this equivalence are not at all obvious to me from the minute i spent skimming its definition
04:10:34 <Fiora> tswett: yeah, it's a slur
04:10:46 <Bike> Wow, it actually uses "÷".
04:10:48 <Fiora> (a similar one would be "retard", for the mentally disabled)
04:11:29 <pikhq> "Cripple" is also relatively inaccurate, given that one is not actually crippled by many disabilities.
04:11:41 <Fiora> slurs can be pretty inaccurate :P
04:11:45 <Bike> post certainly did pretty well for himself.
04:11:55 <pikhq> What can I say, I'm a pedant.
04:11:56 <monqy> oh there's an explanation up there about how the equivalence relation happens, ok
04:11:57 <Bike> well, insofar as being a huge nerd is doing well
04:12:10 * Fiora suddenly wonders about one-handed keyboards
04:12:18 <Bike> Chorded keyboards! :D
04:12:39 <myndzi> dvorak one handed is actually pretty usable
04:12:41 <Bike> But seriously, Post died in the fifties, no computers for him to concurreinate.
04:12:45 <tswett> Fiora: I could argue that what you just said about the word "retard" is offensive; it refers to the mentally retarted, so you're implying that all mentally disabled people are mentally retarded.
04:12:46 <myndzi> i tried to learn it once so i could type and mouse at the same time
04:12:57 <FreeFull> keyboards with a mirror key are faster
04:13:16 <Fiora> tswett: people often use slurs against people in a way that doesn't make exact logical sense
04:13:23 <monqy> keyboards where the keys are in your brain
04:13:56 <Fiora> someone might call a person without good grasp of english "retarded" because they don't understand the material, even if they're not mentally disabled in any way
04:14:12 <Fiora> bigotry is not exactlyogical
04:14:49 <pikhq> Someone might call me "retarded" because I am in some sense mentally disabled. Ain't words awesome?
04:15:27 <myndzi> "retarded" isn't an insult because of the word
04:15:30 <Fiora> (simple rule: just don't use the slur)
04:15:30 <FreeFull> exactlyogical should be a word
04:15:33 <myndzi> it's an insult because of the meaning
04:15:50 <myndzi> you can keep renaming things to try and get away from "mean words"
04:15:58 <myndzi> but eventually people will just use the new word the same way
04:16:11 <Fiora> except... that doesn't happen
04:16:16 <Fiora> people have used "disabled" for 100 years now
04:16:18 <myndzi> i mean black, i mean colored person, i mean african-american, i mean ...
04:16:24 <Fiora> but I don't see anyone using it as a slur
04:16:26 <monqy> just make the words dorky enough and nobody'll bother with them
04:16:31 <monqy> LANGUAGE: CLEANSED
04:16:31 <myndzi> that's because it doesn't have a ring to it
04:16:37 <myndzi> haha monqy's got it right
04:16:37 <pikhq> Funny, "nigger" is the only one of those that's actually a slur of some sort.
04:16:38 <Bike> god, why do i even say things
04:16:42 <Fiora> "african american" has never been a slur
04:16:45 <myndzi> nigger didn't originate as a slur
04:16:49 <pikhq> Saying "colored" makes you sound *old*, but it's not *offensive*.
04:16:50 <Jafet> You gosh-darned dork
04:16:54 <Fiora> omg white people talking about racism holy shit sotp
04:17:04 <myndzi> but it got used that way and therefore discarded
04:17:11 <lambdabot> *** "colored" wn "WordNet (r) 3.0 (2006)"
04:17:11 <lambdabot> adj 1: having color or a certain color; sometimes used in
04:17:11 <lambdabot> combination; "colored crepe paper"; "the film was in
04:17:11 <lambdabot> color"; "amber-colored heads of grain" [syn: {colored},
04:17:15 <lambdabot> {coloured}, {colorful}] [ant: {uncolored}, {uncoloured}]
04:17:17 <lambdabot> 2: having skin rich in melanin pigments; "National Association
04:17:19 <lambdabot> for the Advancement of Colored People"; "dark-skinned
04:17:19 <myndzi> the others may not be slurs but they are "politically sensitive" in a way
04:17:21 <lambdabot> peoples" [syn: {colored}, {coloured}, {dark}, {dark-skinned},
04:17:28 <Bike> People actually use "colored" to describe themselves, you know.
04:17:38 <Fiora> "people of color" is the reclamation of that term
04:17:43 <monqy> im sure people use lots of words to describe themselves
04:17:47 <Fiora> (but slightly modified to limit confusing with the old term)
04:17:56 <myndzi> people call themselves nigga too :P
04:18:07 <Jafet> I thought "colored" was an american expression for "no mexicans"
04:18:10 -!- Fiora has left ("white people need to stop talking about racism srsly").
04:18:20 <myndzi> i just think it's a moot point to try and chase down the word instead of the usage
04:18:35 <myndzi> hmm, i can't tell, is that part message racist??
04:18:36 <FreeFull> negro is spanish for the colour black
04:18:54 <pikhq> myndzi: It actually presumes rather a lot.
04:18:57 <pikhq> Namely, that we're all white.
04:19:14 <myndzi> also, i guess white people aren't involved in that conversation
04:19:16 <Jafet> White people need to stop talking about white people talking about racism
04:19:25 <pikhq> I mean, I only have knowledge of the skin color of a strict subset of this channel's membership.
04:19:30 <monqy> what if racism is just a horribly stupid thing to talk about in most contexts and most talking about is stupid
04:19:58 <Bike> It's a pretty safe guess that people "well "nigger" is just a word" are white, most of the time.
04:20:01 <myndzi> i could get on board with that
04:20:10 <pikhq> I think we can concur on that.
04:20:14 <Bike> *that people saying
04:20:26 <myndzi> it is just a word, it's a word with a meaning that has changed
04:20:26 <monqy> fiora's on the right track but it has nothing to do with skin color, imo. it's just such and old conversation and there's nothing to be gained by bashing your heads against it
04:20:41 <myndzi> anyway, 'retard' is the same
04:20:52 <Jafet> Now that Fiora has left, we could talk about misogyny
04:20:58 <myndzi> no matter what nice name you come up with, some ass is gonna use it to describe people meanly
04:21:15 <Jafet> In a totally objective unbiased way
04:21:17 <pikhq> Jafet: 'Fraid I talk about that a bit too much.
04:21:57 <monqy> let's not talk about any of this stuff uuuugh
04:22:56 <HackEgo> Taneb atriq Ngevd Fiora nortti Sgeo alot
04:22:57 <Jafet> Are you afraid to talk about it, sissykins?
04:23:15 <Jafet> That sounded too much like susskind
04:23:32 <Bike> people who are subscribed to Super Mega Comics.
04:23:46 <monqy> wow i love super mega comics !!
04:24:48 <shachaf> monqy: wow i forgot about that
04:24:54 <shachaf> i never finished reading them
04:25:03 <Jafet> `run sed -ie 's/$/ monqy/' bin/list
04:25:17 <HackEgo> echo Taneb atriq Ngevd Fiora nortti Sgeo alot monqy
04:25:27 -!- oerjan has quit (Quit: Good night).
04:25:50 <monqy> `run sed -ie 's/ monqy//' bin/list
04:25:54 <Sgeo> tswett, people who want me to tell them when Homestuck updates
04:25:55 <HackEgo> Taneb atriq Ngevd Fiora nortti Sgeo alot
04:26:08 <Bike> Sgeo, you can't just... you can't just tell people what hte list is.
04:26:12 <tswett> So when Homesstuck updates, you just do `list.
04:26:26 <pikhq> Sgeo: How's about a list of people who want you to tell them when Homestuck finishes?
04:26:32 <Bike> It's, like, ritually unclean.
04:26:35 <pikhq> Personally, I plan to wait for it to end and archive-binge.
04:27:00 <Sgeo> You miss out on a lot of speculation, which is pretty essential to understanding what's going on
04:27:23 <coppro> `addquote <Sgeo> Sgeo> You miss out on a lot of speculation, which is pretty essential to understanding what's going on
04:27:25 <Sgeo> At least, there's a lot of little things you miss by not being a serial reader
04:27:27 <HackEgo> 942) <Sgeo> Sgeo> You miss out on a lot of speculation, which is pretty essential to understanding what's going on
04:27:43 <coppro> `addquote <Sgeo> You miss out on a lot of speculation, which is pretty essential to understanding what's going on
04:27:46 <HackEgo> 942) <Sgeo> You miss out on a lot of speculation, which is pretty essential to understanding what's going on
04:27:50 <coppro> Sgeo: what nonsense are you spouting now
04:28:13 <HackEgo> *poof* <Sgeo> You miss out on a lot of speculation, which is pretty essential to understanding what's going on
04:28:14 <monqy> justified by way of that quote is bad
04:28:28 <Bike> Do you need justification to understand what's going on?
04:28:30 <Sgeo> coppro, well, a lot of people misunderstood <spoiler redacted> in Cascade, which was only cleared up canonically later on
04:28:34 <Jafet> `run bin/quote Sgeo | shuf
04:28:36 <HackEgo> 159) * Gregor bashes his head into the wall that is Sgeo. \ 504) <Sgeo> Maybe I should try to learn Scala instead of Ruby <elliott> I will boil your veins. <Sgeo> Which is less bad? <elliott> Probably Scala, but I don't want you learning languages. \ 936) <Sgeo> Actually, just as a guess, J might be worse than APL because it's restricted to norm
04:28:57 <Jafet> `run bin/quote Sgeo | shuf
04:29:00 <HackEgo> 726) <Sgeo_> Why does CL get called functional? <oerjan> it's sort of like how you call ancient greece democratic. \ 110) <coppro> what's the data of? [...] <Sgeo> Locations in a now deceased game called Mutation <coppro> I have no problems with you being interested in online games <coppro> but the necrophilia is disturbing \ 827) <HackEgo> 499)
04:29:03 <coppro> if you want that, do a book club
04:29:18 -!- aloril has quit (Ping timeout: 245 seconds).
04:29:34 <HackEgo> 827) <HackEgo> 499) <zzo38> What is miff-muffered moof? <itidus20> that's a tough question [...] <Sgeo> miff-muffered moof sounds like a setup to something, but itidus screws it up.
04:30:08 <HackEgo> 499) <NihilistDandy> Also Perl, but I don't really consider that a programming language so much as a really heavy implementatino of awk
04:30:20 <coppro> Sgeo: if you want a not-quite-as-dumb counterargument, WoG is that it's better straight through
04:30:39 <Bike> "X is such a bad Y that it's not really a Y" is such a weird device.
04:30:53 <shachaf> It's such a weird device that it's not really a device.
04:30:57 <Jafet> That is such a bad analogy
04:31:21 <Bike> Rhetorical device.
04:31:34 <HackEgo> *poof* <NihilistDandy> Also Perl, but I don't really consider that a programming language so much as a really heavy implementatino of awk
04:31:41 <coppro> also wtf is hussie doing in th emost recent update?
04:31:59 <HackEgo> 681) [...] <fizzie> So if someone tells you "you're worth your weight in Ethernet", it's likely they think your worth is less than $2k.
04:32:18 <Bike> monqy: http://www.amazon.com/Combinatorics-Traces-Lecture-Computer-Science/dp/3540530312 kinda cool lookin
04:32:34 <Bike> "Chapter 4 provides a new bridge between the theory of string rewriting and formal power series." hee
04:32:44 <monqy> mmm mmmm 70 bucks lecture notes
04:32:55 <Bike> Why would you even look at the price new
04:33:18 <monqy> this had better be more than just lecture notes, alt. dang good lecture notes
04:35:14 <Bike> i wonder how many of the people selling for twenty bucks actually have a copy
04:37:44 <monqy> maybe they're just bad copies
04:37:55 <monqy> paperweight gone chewtoy
04:38:12 <Bike> They're robot sellers, they're usually pretty good.
04:38:18 <Bike> I got a book on complex analysis for like two cents once.
04:38:31 <Bike> Arrived hardly on fire at all!
04:41:18 <shachaf> should i learn complex analysis
04:41:45 <Bike> Hell yes you should.
04:41:54 <Bike> Maybe you could even understand what homotopy type theory is!!!!!
04:42:15 <Bike> Also imaginary cool!!!!
04:42:17 <Bike> see, that's a joke.
04:42:58 <shachaf> (that was a joke too i was highlighting it for you)
04:42:59 <monqy> there's lots of math i should know and it's upsetting that i dont know it
04:43:12 <Bike> monqy: do you know if there are mathematicians who don't feel that way?
04:43:17 <shachaf> monqy: "do you know topology"
04:43:19 -!- aloril has joined.
04:43:31 <monqy> shachaf: topology's near the top of the list of things i really should know but don't
04:44:07 <monqy> category theory :'( :'( :'(
04:44:18 <shachaf> category theory? more like stupid theory
04:44:22 <Sgeo> 4 more minutes and I can eat
04:44:35 <ion> I’m out of food.
04:44:37 <Sgeo> That was supposed to be crying happily, not winking
04:44:38 <shachaf> monqy: also people say you should learn other things before you learn category theory
04:44:40 <monqy> it's everywhere and i always feel awful when theres something haven't encountered in it
04:44:47 <Bike> it's pretty cool that one of the big category theory guys lives in a shack in the pyrenees now
04:44:49 <monqy> shachaf: i know other things!!!!
04:44:54 <Bike> and when i say "pretty cool" i mean "what
04:44:56 <Bike> it's what cool.
04:45:12 <Jafet> `run sed -ie '3 s,.*,if ! expr "$id" ">=" 0 "\&" "$id" "<" $(wc -l <quotes) >/dev/null; then id=$(expr $RANDOM % $(wc -l <quotes); fi,' bin/delquote
04:45:21 <monqy> i at least know some algebra!!
04:45:57 <monqy> not completely algebra-dumb
04:46:21 <shachaf> i'm pretty algebra-dumb :'(
04:46:25 <shachaf> i don't even know what a monoid is
04:46:42 <Bike> A thing where you have multiplication and 1.
04:47:26 <monqy> q is there anything that isn't easy
04:47:36 <Bike> Monoidoids are like monoids, but less so.
04:47:40 <shachaf> monqy: getting answers out of you :'(
04:48:12 <shachaf> monqy: btw i thought you were one of the "cool people but it" turns out you don't even know category theory??
04:48:13 <ion> Dude! If you only have multiplication and 1, you only have const id and unit!
04:48:55 <Bike> like, whoa, man.
04:49:02 <monqy> shachaf: i know a few category theory things!!!but i've never bothered to pick up a book and learn it, and nobody teaches it
04:50:15 <shachaf> monqy: some people teach it..........
04:50:25 <ion> ……………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………………
04:50:28 <Bike> shachaf: btw learn matroids
04:51:45 <shachaf> Bike: I've already learned Matryushkas. Is that enough?
04:52:01 <Bike> Matryoshka brains?
04:57:34 <Bike> http://www.sciencedirect.com/science/article/pii/0304397581900578 oooooh
04:58:48 -!- TeruFSX has quit (Ping timeout: 276 seconds).
04:59:15 <shachaf> Bike: what about groups are they easy
04:59:30 <Bike> You've heard how long the classification of groups is, right
04:59:48 <Bike> "The proof of the theorem consists of tens of thousands of pages in several hundred journal articles written by about 100 authors, published mostly between 1955 and 2004."
05:00:48 <scarf> how long is the /statement/ of the theorem?
05:00:48 <Jafet> By yes Bike meant no
05:00:51 -!- TeruFSX has joined.
05:01:35 <Bike> scarf: Wikipedia's article on such is like... ten pages long? Somewhere around there.
05:01:47 <Bike> https://en.wikipedia.org/wiki/List_of_finite_simple_groups
05:02:02 <Bike> The theorem being "that's it"
05:02:22 <scarf> I wonder how useful the result is
05:02:35 <Jafet> Theorem prover stress testing
05:02:45 <Bike> I think somebody called it the greatest thing in group theory in bla bla long period of time bla bla bla
05:03:06 <shachaf> Bike: did you hear the odd order theorem was proved in coq
05:03:14 <Jafet> How long has group theory been around
05:03:20 <monqy> no i didnt help :(
05:03:34 <Bike> Jafet: I think like two hundred years?
05:03:47 <shachaf> he came to california to tell us about it!!
05:03:54 <Bike> I think it was Abel's fault.
05:04:44 <monqy> The end of the 19th and the beginning of the 20th century saw a tremendous shift in the methodology of mathematics. Abstract algebra emerged around the start of the 20th century, under the name modern algebra.
05:04:52 <Bike> Also, apparently this guy Gorenstein has written articles about how long the proof is.
05:04:58 <Bike> That's how you know it's a good proof.
05:05:01 <monqy> there's of course a bunch of group theory before that
05:05:13 <monqy> The abstract notion of a group appeared for the first time in Arthur Cayley's papers in 1854.
05:05:25 <Bike> monqy: it was a ballpark estimate in that i threw a baseball and broke a window
05:05:25 <Jafet> https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups#Timeline_of_the_proof
05:05:50 <Jafet> I guess it is technically the greatest thing in group theory
05:06:02 <scarf> Bike: I don't think that's how ballpark estimates work
05:06:05 <Bike> The theorem is, in fact, most of group theory.
05:06:17 -!- WeThePeople has quit (Quit: Leaving).
05:06:23 <Bike> scarf: I don't think you know how baseball works!
05:07:01 <scarf> Bike: I used to watch baseball quite a lot until they stopped showing it in the UK
05:07:05 <scarf> then it became quite difficult
05:07:26 <Bike> Is there any baseball presence in the UK?
05:07:28 <scarf> the hilarious thing was, the UK coverage was just the US coverage except they put their own commentary and such in the US ad breaks
05:07:35 <scarf> and still had plenty of time left over for ad breaks of their own
05:07:41 <scarf> the ad ratio between the two TV networks was so large
05:07:57 <scarf> and there's a slight amount, but it's nowhere near as large as in the US or Canada or Japan
05:08:05 <Bike> " Thompson (1979) showed that its uniqueness (as a simple group satisfying certain conditions coming from the classification of finite simple groups) would follow from the existence of a 196883-dimensional faithful representation."
05:08:10 <scarf> like, people will have heard of it, and some of them might know some of the rules
05:08:15 <Bike> I think the best thing about math is that somebody wrote this sentence in all seriousness.
05:08:41 <Bike> scarf: would it be apropos to make a joke about cricket?
05:08:53 <monqy> 196883-dimensional is a lot of dimensional
05:08:54 <scarf> Bike: sort-of, although most foreigners' jokes about cricket end up not working
05:09:05 <scarf> unless there's a heavy cricket presence in the country
05:09:27 <monqy> i almost made a joke about cricket, but it was just something like "what about cricket"
05:09:31 <monqy> the joke being cricket, of course
05:09:35 <Bike> monqy: almost as many as graham's number!!
05:09:55 <Bike> scarf: i seriously don't know anything about cricket beyond that it's maybe sort of like baseball and also british
05:10:06 <Bike> so, same as most americans, probably
05:10:08 <Jafet> Knuth up-yours notation
05:10:11 <scarf> the standard joke about graham's number is that it's only the best known upper bound on a value that's believed (but not proved) to be 6
05:10:30 <scarf> Bike: it's really quite different from cricket in the way it works out
05:10:31 <Bike> Yes but it's also a number of dimensions, so mentioning it is totally relevant.
05:10:41 <scarf> in both games, you hit a ball with a bat
05:10:51 <quintopia> scarf: actually there is a better upper bound
05:10:52 <scarf> the really major difference is that in cricket, nothing's forcing you to run
05:10:57 <Bike> we know, quintopia.
05:11:10 <scarf> so unless it's completely safe, the batsman will just stand there
05:11:13 <Bike> well probably. i know. you're all basically me.
05:11:14 <scarf> this makes it a lot harder to get people out
05:11:22 <Bike> scarf, this sounds awkward.
05:11:37 <scarf> quintopia: I wrote it as "the standard joke" for a reason
05:11:49 <scarf> Bike: well you only have to get everyone out once, rather than three of the people out nine times
05:11:51 <shachaf> wait cricket /= croquet??????????????????????????????????
05:11:52 <Bike> There's also a better upper bound, but did you mention that? Hmmmmm?
05:11:52 <scarf> but even so, it can take days
05:12:10 <Bike> scarf: baseball can also take days, luckily
05:12:22 <Bike> Er, also a better lower bound.
05:12:27 <scarf> there were a few games that were weeks long before they added a rule that made it a draw after five days
05:12:41 <scarf> (that was ages ago)
05:13:00 <Gregor> shachaf: Please tell me you're kidding >_>
05:13:10 <scarf> also they have "one-day" matches where each innings is automatically over after 300 balls bowled (= pitches)
05:13:12 <shachaf> I always assumed they were the same thing.
05:13:24 <scarf> which encourages the batsmen to play riskier because getting out is less of a problem
05:13:27 <Gregor> Based on the fact that they're both sports that start with 'c'?
05:13:39 <scarf> they sound kind-of similar
05:13:42 <scarf> but they play rather differently
05:13:43 <shachaf> Gregor: They both have the consonants krkt
05:13:49 <scarf> croquet is about hitting balls through hoops using mallets
05:13:51 <shachaf> And I've played Croquet, I think.
05:13:58 <scarf> I don't have the rules down as well as I have the rules of cricket down
05:14:00 <Gregor> shachaf: Croquet does not end with the consonant 't'.
05:14:15 <Bike> I actually used to confuse croquet and cribbage, if that makes you feel better.
05:14:23 <Gregor> Croquet is also infinitely simpler than cricket X-D
05:14:23 <scarf> yeah, it's pronounced "crokay"
05:14:34 <scarf> Gregor: and cricket is orders of magnitude simpler than gold
05:14:37 <Bike> shachaf: he meant the sound
05:14:37 <Gregor> shachaf: A consonant is a sound, not a letter.
05:14:40 <Sgeo> http://www.reddit.com/r/ProgrammerHumor/comments/1738du/a_hilarious_thread_from_a_programming_forum_i/
05:14:41 <shachaf> The Hebrew pronunciation is "kroket" according to Wikipedia.
05:14:55 <Bike> Oh, in English it's krokay.
05:14:56 <scarf> there are only, what, 11 ways to get out, something like that
05:14:58 <shachaf> Or that's the spelling. And Hebrew doesn't ahve silent letters.
05:15:02 <scarf> that's comparable with baseball
05:15:12 <scarf> and few rules apart from getting out and scoring
05:15:28 <scarf> batsmen try to score as many runs as possible without getting out
05:15:40 <quintopia> wickets are the weirdest idea in sports
05:15:47 <scarf> the fielding team try to get them out (when they can), or (most of the time) stop them scoring
05:15:55 <scarf> and wickets are a reasonably simple idea, really
05:16:03 <Bike> "The best advice I can give is pick up this book: Beginning Programming for Dummies 2nd Edition "
05:16:04 <scarf> make it clear from the hardware point of view whether the target was hit or not
05:16:09 <scarf> except when it doesn't
05:16:18 <scarf> nowadays they put microphones inside the wickets so that they can tell when they were hit
05:16:35 <Sgeo> I learned a lot from For Dummies books when I was a kid
05:16:38 <scarf> and compare the microphone recordings with camera recordings of the wicket, so they don't get confused by loud noises that happened at approximately the right time
05:16:49 <scarf> also they record the sound of the ball hitting the bat, too
05:16:57 <Bike> Sgeo: i learned what defragmentation was from one about macbooks :D
05:17:23 <scarf> which is relevant when trying to work out whether someone's been caught out (think flyout in baseball), or whether the ball just bounced off their kneepads (you aren't out if you're caught after that, unless you would have been out anyway)
05:17:25 <Bike> other highlights: complaints that Microsoft Word took up 2 MB of RAM
05:17:26 <quintopia> any game that requires audio recordings to ensure the rules are enforced properly is weird
05:17:46 <Sgeo> Better than requiring video recordings
05:17:47 <scarf> quintopia: you don't have those in more casual matches, the game still works, just the decisions are a little less accurate as a result
05:17:56 <quintopia> Bike: i agree. wtf is up with a text editor that large?????
05:18:13 <Bike> quintopia: "takes up half of memory"!!!
05:18:19 <quintopia> scarf: video replay should suffice for anything
05:18:21 <Bike> also it's a word processor not a text editor hth
05:18:21 <scarf> word mostly isn't a text editor
05:18:53 <scarf> quintopia: it's very hard to work out whether a ball that might be travelling at 100mph or so has collided with a wooden stick, from video evidence alone, given that it might graze by just a couple of millimetres
05:19:02 <quintopia> what is the difference? is the difference something i care about using?
05:19:08 <Jafet> Word is a Word editor
05:19:09 <monqy> word is for word art and using wacky fonts for the bbq flyer that's about it
05:19:15 <Jafet> (except when it isn't)
05:19:24 <quintopia> i suspect that i've never used the features of word that aren't found in, say, kate
05:19:38 <scarf> scarf: Word is a word processor, the main difference is the existence of formatting
05:19:43 <Bike> quintopia: yeah, Word would be shitty for writing code, and kate would be shitty for the bbq flyer
05:19:50 <scarf> quintopia: Word is a word processor, the main difference is the existence of formatting
05:20:14 <scarf> in order to get formatted text in something like kate, you need to write, say, HTML or LaTeX directly, and it doesn't give a WYSIWYG view
05:20:22 <quintopia> Bike: yeah but bbq flyer who cares wtf
05:20:23 <monqy> http://www.homeandlearn.co.uk/mw/images/wordArtDB.jpg just look at this beauty
05:20:27 <scarf> which is not a problem for people experienced in writing formatting as programs
05:20:29 <scarf> but is for many people
05:20:33 <Bike> quintopia: see, this is why you use kate.
05:20:42 <Sgeo> I hate formatting
05:20:49 <Sgeo> I hate dealing with it, thinking about it
05:20:52 <Bike> most people in the world are more concerned with bbq flyers than with irssi plugins.
05:21:05 <Bike> well, more people. i suppose most people in the world don't give a damn about bbqs.
05:21:10 <Sgeo> WTF how does one make text "look good"
05:21:13 <quintopia> Bike: i'm exaggerating of course. i use lyx. lyx probably uses well over 2MB of RAM
05:21:17 <kmc> uhm a bbq flyer is quite trivial with \documentclass{bbqflyer}
05:21:22 <evincar> Sgeo: That is a big question. :|
05:21:26 <Bike> laughed out loud
05:21:28 <scarf> LyX does the same job as Word, rather than as Kate
05:21:36 <ion> sgeo: WordArt.
05:21:48 <Jafet> scarf: namely, to annoy the hell out of you
05:21:52 <quintopia> kmc: i use that doc class for research paper cover pages
05:21:59 <evincar> By big question I mean small question with big complex answer.
05:22:03 <scarf> Jafet: LyX is less annoying than Word
05:22:07 <evincar> Which is possibly the best kind of question.
05:22:21 <scarf> an alternative way of looking at it is, Kate does the same job as Notepad (just it does it a lot better)
05:22:40 <Bike> yeah i kind of think of notepad as "the text editor" and Word as "the word processor"
05:22:44 <Bike> i'm not a true linuxite :(
05:22:45 <quintopia> notepad was a quality piece of software man
05:22:55 <scarf> Notepad is basically just a multiline text input field with a menu attached
05:22:58 <monqy> what happened to notepad :(((
05:23:20 <quintopia> scarf: are you not a fan of minimalism
05:23:24 <Bike> What is notepad.exe? How to remove notepad.exe virus? The fast and easy way to solve notepad.exe errors or problems. Download now.
05:23:46 <scarf> Bike: real web page?
05:23:52 <Bike> Well, autogenerated, but yes.
05:24:10 <scarf> I can believe notepad.exe would be a plausible name for a virus
05:24:12 <monqy> notepad.exe is important for Windows 7/XP/Vista. Click here to know what notepad.exe is doing, its safeness and how to avoid problems.
05:24:22 <Jafet> Is a webpage that is only ever shown to googlebot a real web page
05:24:28 <kmc> it's all about the calc.exe
05:24:32 <scarf> I've seen them call themselves iexplore.exe (but hide in a different and obviously wrong directory)
05:24:36 <monqy> Jafet: good question
05:24:44 <Bike> I bet you could say something actually interesting about different operating environments by comparing their text editors. Linux has ed since it was originally built on dumb terminals and with mainframes. Windows has Notepad since that's pretty easy for demonstrating your graphical system and stuff.
05:24:49 <scarf> I'd say it's a real web page, but it's not on the real web
05:25:00 <monqy> 21:24:10 <scarf> I can believe notepad.exe would be a plausible name for a virus
05:25:01 <Bike> the platonic ideal of a web page
05:25:14 <monqy> scarf: half of the results for notepad.exe are about a trojan distributed as notepad.exe
05:25:20 <scarf> Bike: Linux has some vi and nano pretty much everywhere nowadays
05:25:37 <Bike> i know, but i probably couldn't have fit anything about those in that line
05:25:44 <Bike> windows also has wordpad and well word
05:25:44 <scarf> (where by some vi, I mean vi, vim, or one of the cut-down vim variants)
05:25:51 <Bike> and... i have no idea what's on OS X
05:26:02 <scarf> back in windows 3.1, wordpad was called write, I think
05:26:17 <monqy> osx probably has something flashy
05:26:20 <Bike> "Notepad is a common text-only (plain text) editor. The resulting files—typically saved with the .txt extension—have no format tags or styles, making the program suitable for editing system files that are to be used in a DOS environment"
05:26:41 <Bike> Oh, it does support right to left text. Cool.
05:26:52 <monqy> http://www.notepad.org/
05:26:57 <scarf> Notepad also screws up line ending encodings
05:26:58 <monqy> this is a good website
05:27:13 <Bike> bush hid the facts
05:27:17 <Bike> best bug ever? probably.
05:27:18 <scarf> like, it always BOMs UTF-8, and uses \r\n newlines, and won't understand just-\n newlines
05:27:41 <scarf> Bike: it triggered off any sequence of lowercase letters separated by spaces with word lengths 4 3 3 5
05:27:53 <evincar> I've never seen a text editor fail the way I expect with \n when it wants \r\n.
05:27:54 <scarf> so it's just a case of finding an amusing sentence that fits that restriction
05:27:57 <Bike> Yes, but I love conspiracy theories.
05:28:04 <monqy> http://www.notepad.org/logo.htm this is good too
05:28:23 <Bike> That's beautiful.
05:28:40 <scarf> Bike: the other common sentence I saw was "this app can break"
05:29:32 <evincar> All of the images at the bottom are separated by \n
05:29:54 <evincar> Also <font> is the greatest tag.
05:30:18 <scarf> evincar: Notepad just shows all the \ns as a literal control-j character
05:30:22 <scarf> which looks like a weird box thing
05:30:24 <Bike> Courtesy of Miles Prower- http://tails.kicks-ass.net
05:30:25 <monqy> blink is lame. marquee "the only way to go"
05:30:49 <evincar> scarf: Oh I misremembered. I thought it just omitted the linebreaks altogether.
05:31:05 <scarf> it looks much like that, the literal newlines can be invisible in some configurations
05:31:09 <scarf> although they're /there/
05:31:44 <evincar> So what \n ought to do is be a line feed.
05:31:45 <Sgeo> o.O at the Any browser logo on there
05:31:53 <evincar> I.e., foo\nbar should render as:
05:31:58 <Sgeo> You can certainly make pages intended for a subset of browsers by using Notepad
05:32:08 -!- sebbu has quit (Read error: Connection reset by peer).
05:32:19 <Sgeo> I've done that deliberately. (The subset of browsers thing)
05:32:38 -!- sebbu has joined.
05:32:39 <Sgeo> I guess technically everyone does. Who TF writes to be compatible with ViolaWWW or Mosaic?)
05:32:53 <Bike> Did you hear you can get Mosaic on Linux now?
05:33:03 <scarf> Sgeo: Wikipedia doesn't work in Mozilla 1.2 :(
05:33:16 <scarf> (I famously blanked the main page talk like that once, people assumed I was vandalizing)
05:33:37 <scarf> (and even when it worked, it introduced spurious newlines into pages by line-wrapping their entire contents)
05:33:53 <scarf> (like, the same operation that fmt(1) performs)
05:34:54 <Bike> hm, so were you active in wikipedia's community?
05:35:01 <Bike> i'm suddenly curious how they deal with people with autocensors.
05:36:08 <scarf> Bike: I used to be an admin there
05:36:20 <scarf> occasionally we told people to stop editing because a proxy or something was screwing up the page
05:36:29 <scarf> and blocked them temporarily if they didn't
05:36:39 <scarf> most common was some sort of misconfigured software adding backslashes before apostrophes
05:36:44 <scarf> and other backslashes
05:36:50 <Bike> it was funny when people would edit a page and suddenly all occurences of "fuck" were replaced with asterisks, and by funny i mean instant ban
05:37:06 <scarf> (which grows exponentially, so it becomes very noticeable very quickly)
05:37:27 <Bike> i wonder how apostrophes ended up used for quotation anyway
05:37:50 <scarf> well it's a problem even in things like "don't", because smart quotes are hard to edit and so people tend to use regular apostrophes instead
05:38:32 <Bike> i know, i was just wondering
05:38:49 <evincar> The state of input methods is tragic.
05:38:54 <Sgeo> Hmm, now I wonder if you could make a filter that filters the text even in the textarea, but puts the words in question back when submitting the page
05:39:11 <Sgeo> diff-y stuff I guess
05:39:15 <scarf> evincar: well “smart quotes” should be easy to type through any sensible input method
05:39:16 <Bike> You should make a startup that does that.
05:39:26 <scarf> just, Windows doesn't come with a compose key by default, nor an easy way to configure one
05:39:53 <evincar> scarf: I use a “compose key” which still isn’t—really—good enough.
05:40:08 <scarf> evincar: yeah, although most of the common stuff is there, and most is guessable
05:40:10 -!- ogrom has joined.
05:40:21 <evincar> In terms of discoverability, a compose key is pretty good.
05:40:24 <scarf> alternatively or additionally, you can use altgr combinations, unless you have a US keyboard
05:40:30 <scarf> I use those for, say, ü out of habit
05:40:33 <Jafet> Look at the big picture, do you want every lolcat uploader on instagram using unicode captions
05:40:46 <Jafet> Actually that doesn't sound too bad
05:41:03 <scarf> Gregor: just tried it, <3
05:41:12 <scarf> I guess that was reasonably obvious
05:41:13 <evincar> Trouble is when there isn't a mapping for a thing you think should be there.
05:41:21 <evincar> And you are a nontechnical user who has no idea where to go edit that.
05:41:34 <evincar> And you are on Microsoft Windows.
05:42:01 <Jafet> linux is harder to configure than windows
05:42:24 <evincar> My mother is *employed* because Windows is hard to "configure".
05:42:31 <scarf> they're both really hard to configure when they don't have a reasonable GUI for the task
05:42:50 <scarf> I think Windows is easier to misconfigure by mistake in cases where the defaults are sane
05:43:20 <Jafet> ~/.gnome/config/meaninglessname/this/was/in/a/different/directory/two/weeks/ago/ui.xml
05:44:06 <Jafet> Also linux desktops have a "registry" now?
05:44:09 <evincar> Jafet: Even XML would be better than a different unique format every time.
05:44:40 <Jafet> XML is a different unique format every time.
05:44:58 <evincar> Yes, and it never ceases to amaze me what people do with the stuff.
05:45:59 <Sgeo> http://forums.thedailywtf.com/forums/p/4361/99615.aspx
05:46:09 <evincar> <dict><key>CFBundleIdentifier</key><string>com.example.foo</string></dict>
05:47:39 <Bike> "and then execute the command thats in the xml"
05:49:32 <Bike> serious question, are there computer jobs that aren't miserable
05:49:41 <Sgeo> Bike, that was an OSS project
05:50:03 <Bike> The WWII-era intelligence agency?
05:50:04 <evincar> Bike: I have a computer job which is not miserable.
05:50:13 <Bike> What is your computer job which is not miserable?
05:50:54 <evincar> I maintain a compiler and a build system.
05:50:59 <evincar> And random other stuff that needs doing.
05:52:16 <evincar> Eh...the code is in need of love that we don't have time to give. :(
05:52:34 <Bike> nope i've already decided your job doesn't suck sorry
05:55:07 <scarf> Jafet: Gnome has something registry-like (but it mostly reserves it for configuration, rather than the Windows registry which was originally intended for something entirely different and which is nowadays used for all sorts of random stuff)
05:55:13 <scarf> I think it's used specifically by Gnome, though
05:56:10 <evincar> (The compiler is about 20kloc, build tool 8kloc, both Haskell.)
05:56:29 <Bike> compilers are pretty cool
05:57:37 <scarf> with Verity I wrote the build tool into the compiler
05:57:56 <scarf> separate build tools break so easily, and are more work to maintain
05:58:02 <evincar> That's probably a good idea for new work.
05:58:21 <evincar> In our case the build thing does way more than just run the compiler though.
05:58:43 <evincar> The compiler does code dependencies within a project.
05:59:01 <evincar> The build system runs the compiler and a bunch of conversion utilities.
05:59:06 <scarf> in my case, dependencies have to be declared with import statements
05:59:32 <evincar> And deploys updates over a network. :P
05:59:41 <scarf> and it looks at the object files matching the imports you state to make sure that things like types match
05:59:52 <scarf> it can do 100% separate compilation if you don't care about cross-module type checking, though
06:00:06 <scarf> this also means that the other modules can be written in other languages
06:00:16 -!- sebbu has quit (Read error: Connection reset by peer).
06:00:25 <scarf> you just have to provide it with a description of what types things have, because it can't figure it out automatically in that case
06:01:01 -!- sebbu has joined.
06:01:01 -!- sebbu has quit (Changing host).
06:01:01 -!- sebbu has joined.
06:02:53 <evincar> Well that is how an FFI usually works.
06:13:48 <scarf> one problem is that at the moment, you have to specify the types in its object file format
06:17:47 -!- TeruFSX has quit (Ping timeout: 255 seconds).
06:36:16 <shachaf> monqy: so what are you going to learn first
06:36:42 <Bike> imo start with morphisms and then move on to categories
06:37:02 <monqy> i already know about morphisms and categories.......
06:40:05 <monqy> whats this about anyway
06:40:31 <Bike> i dunno, i think shachaf was couching a serious question about your mathematical interests in the surreal form of discourse common in this channel
06:41:27 <shachaf> Bike: It's the only way to talk to monqy.
06:42:13 <monqy> the list is less interests, more split between things i really should know near the top and curiosities near the bottom. the middle is a mixture of things i probably know enough about and things i secretly know but don't realize it
06:42:48 <monqy> i discovered recently i know more about type theory than i gave myself credit??? who would have guessed
06:43:12 <Bike> so what are the things near the top
06:43:28 <monqy> um category theory
06:43:47 <shachaf> monqy: i mean!! what did you know about type theory that you didn't think you knew
06:43:58 <shachaf> or did you know something but you thought it wasn't related to type theory but actually it was
06:43:59 <Bike> something other than category theory imo not category theory
06:44:57 <monqy> more on the side of i knew all this type theory stuff and i guess i thought it was just sorta related to type theory and i was missing out on all the details? but it turns out not really
06:45:26 <shachaf> i should know more about type theory
06:45:32 <shachaf> i know basically nothing??
06:45:45 <monqy> shachaf: maybe that's just what you think!
06:45:58 <Bike> there are shittons of books about martin-lof on the internet
06:46:00 <monqy> Bike: probably i should know topology? maybe??? maybe it's just one of those things i think i should maybe know but it's just a curiosity
06:46:17 <shachaf> monqy: well maybe i should read tapl or something??
06:46:30 <monqy> tapl's a pretty easy read
06:46:34 <Bike> knowing things is hard
06:46:39 <shachaf> all i read of tapl was the first page
06:46:46 <shachaf> which was a directed graph of chapter dependencies??
06:46:50 <Bike> it really picks up around the second page
06:46:57 <monqy> there's a bunch of proofs you can do if you really want to engage yourself. do them in coq or agda or something for super engagement???
06:47:13 <Bike> oh, i remember posting a photo of the chapter dependencies
06:47:13 <shachaf> monqy: also i don't really know coq or agda???? and maybe i should
06:47:16 <Bike> "yes, a book is really doing this"
06:47:32 <Bike> probably not that engaged though
06:47:47 <shachaf> wow does everyone know more about types than i do!
06:47:54 <monqy> something along the lines of coq or agda is "worth knowing" imo
06:47:56 <Bike> i do this thing where i read textbooks but don't do many of the exercises and then i suck
06:48:04 <Bike> maybe i should get a proof assistant
06:48:07 -!- Nisstyre-laptop has joined.
06:48:16 <Bike> and then use it with TAOCP first to be a rebel
06:48:36 <Bike> ("second order logic: good for proving how fast you can't multiply")
06:49:34 <monqy> who needs second order logic when you have the higher order stuff
06:49:56 <Bike> 2 is a higher order than 1 monqy.
06:50:07 <monqy> higher is a higher order than 2!!!
06:50:11 <shachaf> monqy: well i "kind of know a little bit of agda??"??
06:50:30 <Bike> I actually don't know what "higher-order logic" means.
06:50:35 <Bike> Is it like... what is it like.
06:50:43 <shachaf> > let fac n = product [1..n] in fac (fac (fac 2))
06:51:03 <monqy> i know....about....agda..... sometimes i feel i should know more agda but i don't really have a use for it
06:51:12 <shachaf> i've never even done anything with coq
06:51:18 <Bike> Telling shachaf about TAPL is a use imo.
06:51:19 <shachaf> which i think all the "cool people have"?
06:51:27 <monqy> i've done plenty with coq
06:51:44 <Bike> «The term "higher-order logic", abbreviated as HOL, is commonly used to mean higher order simple predicate logic. Here "simple" indicates that the underlying type theory is simple, not polymorphic or dependent.»
06:51:45 <shachaf> aren't you doing some type theory thing in coq or something
06:51:50 <Bike> ok but coq uses dependent logic
06:51:54 <Bike> monqy are you lying
06:51:56 <monqy> shachaf: i was, yes
06:52:24 <monqy> Bike: Examples of higher order logics include HOL, Church's Simple Theory of Types, Thierry Coquand's calculus of constructions, which allows for both dependent and polymorphic types.
06:52:39 <Bike> Well gosh, that's confusing.
06:53:00 <Bike> I know what second-order logic and church logic is but this just seems so vague
06:53:06 <Bike> maybe i should just figure out CoC and shut the fuck up.
06:54:21 <monqy> it's even in the lambda cube???how much easier can you get
06:54:27 <monqy> shachaf: nothing much.....
06:54:43 <monqy> shachaf: there's a "story" behind it but it's the sort of thing i don't really feel like talking about
06:55:00 <Bike> fucking lambda cubes.
06:55:06 * Bike glances at topic
06:55:30 <monqy> the important part is that it gave me more experience with coq and how to manage large proofs and so on
06:55:44 <shachaf> monqy has started the avant-garde art movement of "lambda cubism"
06:55:53 <monqy> the type theory was "not particularly interesting"
06:56:08 <monqy> ive done some pure type systems stuff recently but that's not in coq...
06:56:14 <monqy> maybe i should move it to coq?? who knows
06:56:49 <shachaf> imo i wonder what the "story" is
06:57:41 <Bike> hm maybe i should try reading jshutt's thesis again, there was lots of lambda calculus provey theoryy stuff i honestly didn't get
06:57:51 <Bike> he still had a whole appendix on how he chose letters though
06:58:11 <monqy> do you at least get curry-howard?
06:58:30 <Bike> not that well but sorta
06:59:21 <shachaf> Bike: imo you should get curry-howard
06:59:27 <shachaf> it's "basically the" best thing??
06:59:32 <monqy> curry-howard is easy and it starts popping up when you look into these things
06:59:39 <monqy> easy and powerful and good for you
06:59:40 <Bike> I probably would "really get it" if I fucked around with an actual system, like coq.
06:59:49 <Bike> Instead of just reading shit constantly.
07:00:01 <shachaf> maybe i don't "really get it"
07:00:06 <Bike> Wow, I kind of hate talking like that.
07:00:08 <monqy> Bike: imo you don't even need to do that you just need to think about it a little bit and it makes sense
07:00:25 <monqy> or maybe thats just for me
07:00:32 <shachaf> not everyone can be a monqy
07:00:43 <Bike> Whenever I read about it I get stuck on product types. True story.
07:01:08 <Bike> http://en.wikipedia.org/wiki/Intuitionistic_type_theory#Connectives_of_type_theory like i just look at it and "uhhhhh"
07:01:10 <monqy> the correspondence between products and conjunction?
07:01:35 <monqy> pi-types aren't quite what i'd call "product types"
07:01:37 <shachaf> i thought you "meant conjunction"
07:01:42 <Bike> i meant pi types yeah, fuck
07:01:49 <Bike> product types are so easy etc etc shachaf
07:01:54 <shachaf> pi types are "p. cool too"
07:02:07 <shachaf> it took me a bit to understand why they're called that
07:02:24 <shachaf> but it makes perfect sense
07:02:25 <Bike> probably it's something Exciting and Deep like euler's primality thingie.
07:02:28 <Bike> buuuuut i'm slow.
07:03:15 <Bike> oh, wait, i suppose pi types are sort of like the "reals are functions N -> N" thingie
07:03:48 <shachaf> reals are functions N -> Bool imo
07:03:56 <Bike> sure if you're a poser
07:04:02 <monqy> Bike: weeelllllll do you at least get non-dependent functions
07:04:25 <shachaf> yes that's the important first step
07:04:56 <Bike> maybe i should just read tapl more thoroughly instead of bugging irc
07:05:09 <monqy> tapl doesn't really go over this much
07:05:28 <shachaf> i just learned about it "from the internet"
07:05:55 <Bike> fuck you internet
07:06:00 <monqy> maybe attapl does? but yeah it's everywhere
07:06:17 <monqy> e.g. any self-respecting introduction to coq or agda will have it
07:06:25 <Bike> i thought curry-howard was super basic as type theory goes
07:06:33 <shachaf> that's "basically what agda is all about??"
07:08:13 <shachaf> Bike: btw sigma and pi types are good too
07:09:05 <shachaf> imo sigma types are maybe simpler?
07:09:11 <monqy> sigma types are simpler yes
07:09:18 <monqy> there's a good analogy with stuff like
07:09:51 <monqy> natural numbers less than 5 ~ natural number /\ a proof it's less than 5
07:10:53 <shachaf> a sigma type is just a tuple where the type of the second element depends on the value of the first element
07:11:15 <monqy> pi types are just functions where the result type depends on the value of the argument!
07:11:33 <monqy> like you can have something like
07:11:50 <shachaf> the reason they're called that wasn't obvious to me when i first heard of them
07:12:01 <shachaf> btw i actually first heard of them when i went to a talk about homotopy type theory??
07:12:03 <monqy> `forall n, n + 1 > 0` is the type of functions fron natural numbers to proofs that their successors are greater than 0
07:12:07 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: forall: not found
07:12:12 <shachaf> it was a bit "over my head" at that point even though i followed a little bit
07:12:18 <monqy> i want to know more about homotopy type theory :( is it good
07:12:34 <Bike> is it because they're a product of like, 0, 0+1 > 0 and 1, 1+1 > 1 and 2, 2+1 > 1, and so on
07:12:47 <shachaf> monqy: http://comonad.com/reader/wp-content/uploads/2011/10/slides.pdf
07:13:01 <shachaf> actually there isn't very much on the slides
07:13:50 <Bike> glad i'm far enough in math that saying a product of that makes any sense makes any sense
07:13:56 <shachaf> like when you have forall epsilon exists delta blah(epsilon,delta)
07:14:03 <shachaf> that's like a function that takes epsilon as an argument
07:14:09 <shachaf> and gives you back a delta along with a proof about the delta
07:14:30 <Bike> hm maybe i should go over this and churchill at the same time
07:14:35 <Bike> epsilons all over that fucking thing
07:14:37 <shachaf> foo : (epsilon:R) -> (delta:R, blah epsilon delta)
07:15:07 <Bike> and probably that ties into grothendieck or homotopy or whateverthefuck
07:15:41 <monqy> let's see how far i can follow these slides without any talky.....
07:15:56 <shachaf> monqy: btw those slides were by dolio he knows some things about this??
07:24:35 -!- ogrom has quit (Quit: Left).
07:27:08 -!- yorkdove has quit (Ping timeout: 256 seconds).
07:28:04 <evincar> Hey if I'm inferring types for function definitions
07:28:12 <evincar> and those can be in any order and possibly mutually recursive
07:28:34 <evincar> then I can't just assign each definition a type variable up front
07:28:41 <evincar> and instantiate them after the fact
07:28:44 <monqy> read up on coinduction, evincar
07:28:52 <evincar> because each usage site can have a different type
07:29:04 <monqy> or is that not what youre asking about...
07:29:38 <monqy> read up on polymorphism? gosh, what are you doing
07:29:46 <evincar> I'm asking about how best to have terms associated with type schemes that are not computed yet.
07:30:13 <evincar> Laziness seems like the wrong approach here.
07:30:17 <monqy> ok do you know about hindley-milner?
07:30:26 <monqy> and extensions thereof?
07:31:11 <monqy> so you know about the whole generate-constraints-on-your-types-and-then-unify thing?
07:31:18 <evincar> Yes, that's what I'm doing.
07:32:12 <monqy> i don't get what your problem is??
07:32:56 <evincar> I don't know if it's a problem...
07:32:56 -!- ogrom has joined.
07:33:38 <evincar> What I'm doing now to allow arbitrary order is first associate each definition with a fresh type variable.
07:33:55 <evincar> Specifically a type scheme with no quantified variables.
07:34:16 <evincar> Then run inference on those definitions.
07:34:43 <evincar> Take the resulting type schemes and instantiate each one then unify the result with the corresponding variable.
07:34:55 <evincar> I feel like this isn't right.
07:35:25 <evincar> Because separate invocations get the same type variable which is unified with the result of instantiating the type scheme *once*.
07:35:31 <monqy> what do you feel isn't right about it and what do you mean by "type scheme"
07:36:23 <evincar> I mean a type + quantified type variables.
07:36:53 <monqy> so just a plain ol rank-1 universal type?
07:38:09 <evincar> But it seems to not exhibit the problem I thought it would, or my test case is wrong.
07:38:53 <monqy> i still don't quite understand your problem
07:39:37 <evincar> Different invocations of the same function can be given different types.
07:39:40 <evincar> I want to make sure I don't break that.
07:40:54 <monqy> well how would it break it? if your function gets a universal type and your stuff isn't TOTALLY BROKEN then you shouldn't be unifying it with any instantiated stuff
07:40:59 <monqy> if that's what you're saying
07:41:32 <monqy> your rules for function application and so on should handle it??
07:41:54 <shachaf> monqy: btw why doesn't ghc support existentials
07:42:13 <Sgeo> I keep seeing things like files that state how many lines they have (in programming competitions), and thinking that it's for the benefit of C programmers
07:42:18 <monqy> shachaf: what sort of existentials? there's that one LANGUAGE thing!
07:42:20 <Sgeo> Do I have an unreasonably low opinion of C?
07:42:48 <Bike> what is even with existential types, they were in tapl but they were really weird
07:43:08 <monqy> well there's lots of different things that fall under the umbrella of sigma types
07:43:11 <shachaf> monqy: no first-class existentials
07:43:36 <Bike> er assuming you mean existential quantification
07:46:35 <monqy> the "easy" cases of sigma types are the ones where the left thingy is a type and you use it in the right thingy, like what happens in tapl where it's used for encapsulation or something like that, and where the left thingy is a value and the right thingy is some curry-howarded proof about it like in my example with {n : nat | n < 5}
07:46:48 <monqy> if you're really fancy you can care about both projections!!
07:46:53 <Bike> yeah it's the encapsulation that was weirding me out
07:47:02 <Bike> do programming systems actually use that?
07:47:36 <monqy> ask elliott for opinions about existentials :-)
07:47:55 <Bike> is this like when you had me ask ais about feather
07:48:03 <evincar> Isn't it also an existential when you have, say, data Box = forall a. (HasFoo a) => Box a
07:48:14 <monqy> shachaf: don't know!! woops
07:48:21 <evincar> Then a heterogeneous list of boxen which all HasFoo.
07:48:22 <monqy> Bike: did I? it's....similar :-)
07:48:35 <Bike> well when I say "you" i mean "the multiheaded demon that is #esoteric"
07:48:40 <Bike> that is a very cruel smile you have there
07:48:57 <monqy> well when I say elliott has opinions about existentials
07:49:01 <monqy> i mean elliott has opinions about existentials
07:49:56 <shachaf> monqy: apparently it has to do with how you can't express them in Core??
07:49:57 <evincar> (That being [exists a. HasFoo a => a])
07:50:05 <shachaf> which is also why you don't have existential newtypes (even though you have data types)
07:50:20 <monqy> i don't know much about core, :0
07:50:25 <shachaf> evincar: type classes are the devil....................
07:50:33 <shachaf> monqy: well it's pretty much system f??
07:50:44 <shachaf> system fc "aka system f with coercions"
07:50:58 <Bike> What's wrong with type classes?
07:51:00 <monqy> evincar: you should ask elliott about existentials too
07:51:10 <monqy> we can have an asking elliott about existentials party
07:51:20 <Bike> I'll bring the punch.
07:51:22 <shachaf> but most things people want to do with them are bad
07:51:27 <shachaf> Bike: no, elliott will bring that
07:51:31 <evincar> monqy: elliott does not like it when I ask him things
07:51:32 <shachaf> if you ask him about existentials
07:51:40 <Bike> can i bring chips
07:51:47 <shachaf> "its a pun about elliott's violent tendencies where existential are concerned"
07:51:58 <Bike> yes i got that can we move on to chips
07:52:09 <monqy> i'm bringing the pop corn
07:52:15 <monqy> it's a joke about how this will be fun to watch
07:52:52 <shachaf> we should have a joke party
07:52:56 <shachaf> if we survive the other party
07:53:05 <Bike> so who else do i ask about things
07:53:06 <monqy> i'll bring the punch
07:53:11 <shachaf> monqy: so i don't know that much about system f except for the things i do know
07:53:17 <shachaf> why can't it have existentials
07:53:18 <Bike> ais about feather, elliott about existentials, sgeo about... i dunno J probably
07:53:22 <Bike> what do i ask monqy?
07:53:25 <monqy> shachaf: system f is easy
07:53:43 <shachaf> monqy: right but apparently making ghc core work with existentials is "really hard????"
07:53:55 <shachaf> so why is making system f work with existentials "really hard????"
07:54:02 <Sgeo> I don't know much about J
07:54:13 -!- DH____ has quit (Read error: Connection reset by peer).
07:54:13 <Sgeo> Other than it's a little like APL I think
07:54:26 <Bike> typed APL, just picture it
07:54:31 -!- DHeadshot has joined.
07:54:34 <Bike> APL with subtyping and polymorphism
07:54:51 <Sgeo> You know, someone made a comment and I saw it, years ago, this person liked Factor and J but those names were hard to Google.
07:55:05 <Sgeo> I wonder if it was elliott who made that comment and is therefore to blame for me getting into Factor.
07:55:13 <Bike> also does system f even have existtential quantification
07:55:51 <Sgeo> "J is a modern, high-level, general-purpose, high-performance programming language."
07:55:55 <Bike> i don't know what that means, sgeo.
07:55:56 <Sgeo> It's "general-purpose" now?
07:56:02 <Bike> does it mean you'll tell me what to ask monqy?
07:56:06 <monqy> Bike: you have to "encode" existentials in system f
07:56:15 <Bike> oh boy i love encoding things into other things
07:56:15 <Sgeo> I don't know APL either.
07:56:37 <Bike> that would pretty much explain why Core doesn't have them though
07:57:01 <monqy> there's a section on it in tapl!
07:57:18 <Sgeo> Oh hey "monad" is another word that varies from language to language.
07:57:26 <Sgeo> Or, well, "J" has a different-from-standard meaning
07:57:42 <Sgeo> ...why did I quote J?
07:57:42 <Bike> doesn't it just mean a word that only has one uh argument
07:57:45 <zzo38> I thought something about extension of SQL to define new functions and aggregates, including anonymous, and which could be done without modifying SQLite, as far as I can tell.
07:57:50 <Bike> instead of a "dyad"
07:58:13 <Bike> that usage actually predates haskell so Check And Mate
07:58:31 <Bike> haskell and/or whatever introduced monads to programming*
07:58:43 <Bike> embrace descriptivism, my son
07:58:49 <monqy> [tapl] exists X, T(X) =def= forall Y, (forall X, T(X) -> Y) -> Y. looks like one of those silly church encoding tricks
07:59:35 <Bike> Pfhaha, Wiktionary actually defines monad as "(mathematics, computing) A monoid in the category of endofunctors."
07:59:37 <Sgeo> Dear god why would I even glance at J again if you learn J and then walk away for a while you forget everything all code becomes unreadbal
07:59:40 <Bike> after leibniz of course.
07:59:49 <Sgeo> At least, I assume that's the case
07:59:58 <Bike> have you tried it
08:00:19 <Bike> this will be your greatest challenge yet. rather than learning a language, you will be unlearning it.
08:00:41 <zzo38> Once someone told me exactly how it means, "monoid in the category of endofunctors", then I can see, yes and that seem like it might be a simple definition of a monad.
08:01:22 <Bike> It's pretty simple if you know what a monoid and an endofunctor are. Which most people don't. Go math!
08:02:34 <monqy> well this is monoid in the category-theoretical sense right?
08:02:46 <Sgeo> I mean, most functions don't have clear names
08:02:52 <zzo38> The part I didn't quite understand at first was "category of endofunctors" but once explained then it makes sense, since I already understand monoid, category, endofunctors.
08:02:59 <Sgeo> Well, they have names, the names just don't show up in source
08:03:23 <Bike> monqy: they're "the same" aren't they
08:03:45 <Sgeo> Does J have the sort of metaprogramming stuff that I heard APL has?
08:04:00 <Bike> APL has eval, does that count
08:04:44 <monqy> Bike: https://en.wikipedia.org/wiki/Monoid_(category_theory)
08:05:10 <Sgeo> "The effort required to become an expert J programmer is closer to that required to become an expert C++ programmer."
08:05:18 <Sgeo> Is that intended to be a good thing?
08:05:19 <monqy> Bike: idk if that's what you'd call "the same"
08:05:45 <Bike> looks the same to me!!
08:07:26 <Bike> i like how they still call it "multiplication"
08:12:22 <monqy> https://en.wikipedia.org/wiki/Category:Monoidal_categories what a good category
08:12:51 <Bike> i think mediawiki allows categories to contain themselves though
08:12:55 <Bike> can Categories contain themselves
08:13:22 <zzo38> Mathematical categories do not contain themselfs in ordinary set theory, I think.
08:13:36 <Bike> ordinary set theory doesn't have categories, category theory does
08:14:52 <Sgeo> That is a thing to get the date+time
08:15:22 <Sgeo> It's.... there's concision, and there's concision to the point of unreadability
08:15:24 <Bike> by the way did you seriously start reading about J because i mentioned you and it in a joke that took half a second to come up
08:15:34 <Bike> not even a good joke!
08:15:41 <Bike> And I still don't know what to ask monqy.
08:15:52 <monqy> i'm sure there's some stuff to ask me, but i won't tell you
08:16:00 <Bike> god fucking damn it
08:16:37 <Bike> what's the fuckin command
08:16:41 <Bike> @ask bike hello??
08:16:48 <Bike> @ask elliott what do i ask monqy
08:17:55 <Bike> why is category theory called category theory when as far as i can tell the relations between categories are like a trillion times as important as categories
08:18:23 <monqy> relations between categories theory
08:18:29 <monqy> it'll catch on im sure
08:19:28 <Sgeo> "x+.y is the greatest common divisor of x and y . If the arguments are boolean (0 or 1), the functions +. and *."
08:19:30 <Bike> functor theory i'm telling you
08:19:33 <Bike> or morphism theory
08:19:40 <Bike> you could sound like moronic biologists!!!
08:19:56 -!- glogbackup has quit (Remote host closed the connection).
08:19:57 <Sgeo> It.... almost makes sense to use +. and *. for GCD and LCM. In an insane sort of way
08:20:02 <Bike> Sgeo: did that cut off
08:20:21 <Sgeo> Oh, I forgot to paste the rest
08:20:22 <Sgeo> "are equivalent to logical or and and. "
08:20:28 <Bike> yeah that's what i thought
08:20:37 <Bike> hey you know what would be cool? APL but with category theory instead of matrices and arrays.
08:20:46 <Bike> new life goal, learn enough cat theory to make that esolang
08:21:32 <monqy> there are a whole bunch of languages grounded in category theory aren't there? just none off the top of my head
08:21:46 <shachaf> it should be called monoidoid theory
08:21:57 <monqy> maybe not to the extent apl is "grounded" in arrays...but what would that even mean for categories
08:22:48 <Bike> monqy: but do any of those languages use ⍋?
08:22:50 <monqy> are you xtreem enough for monoidoidoidoid theory???
08:23:40 <Sgeo> If Perl is line noise, is J highly compressed Perl?
08:23:56 <Bike> anyway so i'm going to take my copy of A Programming Language and my copy of Categories for the Working Mathematician and I'm going to use the cut-up technique to make a novel about ninja pornographers, and then burn the result and smoke it
08:25:40 <monqy> sounds like a plan
08:28:01 <Bike> "Categorical quantum mechanics can also be seen as a type theoretic form of quantum logic that, in contrast to traditional quantum logic, supports formal deductive reasoning."
08:31:57 <Bike> right, apl doesn't have operator precedence
08:32:02 <Bike> and... i guess j is right to left? ok.
08:32:22 <monqy> theres all sorts of right-associativity going on yes
08:34:39 <Sgeo> We used 3 : 0 to define the verb. The phrase verb define is equivalent and some find it easier to read. However, it hides information and we will use the 3 : 0 form.
08:34:49 <Sgeo> This helps preserve my sanity a little
08:36:26 <monqy> Bike: maybe you were right about this asking sgeo about j thing....
08:37:02 <Bike> i'd like to deny all responsibility for this now. thanks
08:40:17 -!- glogbackup has joined.
08:56:36 -!- epicmonkey has joined.
08:57:27 <Sgeo> "Control structures are only allowed in definitions and you cannot type one directly into the ijx window for execution."
08:57:33 <Sgeo> Reminds me of Forth :/
08:58:34 -!- Taneb has joined.
09:06:38 -!- Bike has quit (Quit: leaving).
09:12:31 -!- scarf has quit.
09:13:05 -!- Nisstyre-laptop has quit (Ping timeout: 246 seconds).
09:15:38 -!- evincar has quit (Ping timeout: 255 seconds).
09:22:13 * Sgeo gets irritated at J apparently using floating-point
09:22:31 <Sgeo> "The 0.5 and 0.25 are stored exactly, but the 0.1 is stored inexactly, and when displayed with maximum precision shows as 0.10000000000000001 .
09:22:31 <Sgeo> These are facts of life with the way computers store floating point numbers and apply to all computer languages, not just J. "
09:23:17 -!- evincar has joined.
09:26:36 <Sgeo> http://news.ycombinator.com/item?id=4622163
09:26:39 <Sgeo> Can I punch this person?
09:26:55 <Sgeo> Actually, hmm, I guess it could be accurate
09:27:15 <Sgeo> "In binary" isn't the same as "Using bits to encode it"
09:28:36 -!- evincar has quit (Ping timeout: 256 seconds).
09:30:13 <shachaf> Punch first, ask questions later.
09:37:55 -!- fungot has joined.
09:38:05 <fungot> fizzie: sorry, wrong channel. still makes the exact same
09:38:06 <lambdabot> fungot: You have 2 new messages. '/msg lambdabot @messages' to read them.
09:38:25 <lambdabot> RocketJSquirrel said 11m 5d 19h 35m 53s ago: You are a gentleman and a scholar.
09:38:48 <monqy> almost a year, wow
09:38:48 <fizzie> That's... interesting.
09:39:08 <shachaf> FreeFull: we're having a moment of silence don't ruin it!!
09:39:31 <monqy> i used to have -13 but then shachaf ruined it
09:39:32 <shachaf> monqy++ monqy++ monqy++ monqy++ monqy++ monqy++ monqy++ monqy++ monqy++ monqy++ monqy++ monqy++
09:39:56 <monqy> (thats what zen means right)
09:41:48 <shachaf> monqy: help i don't know how to think
09:41:54 <shachaf> data Step k o r = Stop | Yield o r | forall t. Await (t -> r) (k t) r
09:42:06 <shachaf> how can you simplify Await
09:42:11 <monqy> is this one of those things
09:42:21 <shachaf> at first i thought::::: forall t. (t -> r) ((k :+: Proxy) t)
09:42:26 <Sgeo> <cfa> it has an extended precision implementation
09:42:26 <Sgeo> <cfa> and yes, you can use rationals instead of floating point
09:42:26 <Sgeo> <cfa> 3r5 etc.
09:43:17 <monqy> imo ask elliott he knows everything about existentials
09:43:46 <shachaf> monqy: imo the Await part is like (r,CoYoneda k r)
09:43:51 <shachaf> by imo i mean edwardk said so
09:44:24 <shachaf> monqy: btw are you a CoYoneda expert
09:45:00 <monqy> not to my knowledge
09:45:12 <shachaf> monqy: well you know how CoYoneda IORef = a read-only IORef
09:45:50 <monqy> help which coyoneda should i be looking at
09:46:53 <monqy> these haskell searchy things aren't working so great but they turned up a result at least
09:47:14 <monqy> from zzo's package??
09:47:24 <shachaf> CoYoneda f a = forall r. CoYoneda (r -> a) (f r)
09:47:48 <monqy> zzo's coyoneda uses different letters...
09:48:36 <shachaf> i heard zzo likes that letter
09:48:49 <monqy> instead of a it uses x, and instead of r it uses z
09:49:50 <shachaf> monqy: anyway when f is a functor CoYoneda f is isomorphic to f??
09:49:58 <shachaf> but when it's not a functor you can get "weird things"
09:50:31 -!- azaq23 has joined.
09:50:34 <shachaf> by cool you mean boring right
09:50:44 -!- azaq23 has quit (Max SendQ exceeded).
09:50:51 <shachaf> maybe THIS CoYoneda will be more to your liking!!!!!!!!!! http://ncatlab.org/nlab/show/co-Yoneda+lemma
09:51:00 <monqy> no!!!! and edwardk was right about that Await part being like (r,CoYoneda k r)
09:51:06 -!- azaq23 has joined.
09:51:19 <monqy> mm mm i'll read this maybe it will be more to my liking
09:51:25 <shachaf> monqy: i know he was right
09:51:41 <shachaf> but i was wondering whether you can express it like the way i said
09:51:53 <shachaf> «every presheaf is a colimit of representables and more precisely that it is the “colimit over itself of all the representables contained in it”.»
09:52:06 <shachaf> monqy: do you know what a limit is
09:52:29 <monqy> i think maybe i used to?
09:52:54 <monqy> well i forgot what it is!!! are you just testing me
09:53:05 <shachaf> except instead of school homework it's "someone giving you an exercise in irc homework"
09:56:51 <shachaf> do you have a no "homework policy"
09:57:36 <monqy> i have a no-shachaf-asking-me-to-explain-things-he-probably-already-understands-and-knows-i-don't policy
09:58:20 <monqy> limits are probably really easy too but i just really don't know much category theory at all
09:59:02 <shachaf> monqy: actually i don't understand at all : (
09:59:14 <shachaf> i guess first i need to understand:
09:59:44 <Jafet> You first need to understand everything
09:59:56 <shachaf> do i need to bake an apple pie first
10:00:05 -!- Phantom_Hoover has joined.
10:00:19 <Jafet> No, no, you want a soft apple pie.
10:00:30 <monqy> well afaiui a diagram is just another name for functor if you're meant to think of it as some category indexed by another category
10:00:30 <oklopol> "<Bike> can Categories contain themselves" small categories can contain only sets, big categories can contain categories, but only small ones. afaiu. there are no inherent problems with having a category that contains itself but usually you want to have some kind of set theory as well so the usual restrictions apply.
10:01:00 <shachaf> well a diagram is mapping a category to particular kind of other category right
10:02:15 <oklopol> and ordinary set theory has categories. it just doesn't have very large categories. if you restrict to a megahuge set of your choice, you still get categories buildable from those.
10:03:16 <shachaf> oklopol: Is megahuge set a technical term?
10:04:07 <shachaf> monqy: wow am i bad at types or what
10:04:33 <monqy> yeah i thought it smelled like 'machines'
10:04:39 <shachaf> maybe i should learn coq to be good at types
10:05:51 <oklopol> "<shachaf> you know limits right" i suppose
10:06:04 <oklopol> i have to check which is limit and which is colimit tho
10:06:41 <shachaf> btw my exercise is (no spoilers!!)
10:06:51 <shachaf> prove that every category which is small and complete is also cocomplete
10:07:06 <shachaf> and usually i forget about it but sometimes i remember??
10:08:12 <oklopol> so i suppose you have to take the definition of cocomplete and write it in terms of a limit, which will be small if the category is, so that the limit exists due to completeness.
10:08:26 <shachaf> and apparently this exercise has a "dark secret"
10:08:29 <oklopol> is my take without giving this the least amount of thought
10:08:48 <monqy> what sort of dark secret
10:09:59 <shachaf> <ddarius> @tell shachaf Exercise: Any category that is small and complete is also cocomplete. Hint: This is a direct generalization of the lattice theoretic result, e.g. the supremum of the empty set is the infimum of the whole lattice. Extra credit: What is the dark secret of this exercise?
10:11:04 <oklopol> yeah that sounds about right
10:11:34 <oklopol> dunno what the secret is. something about categories being ordered classes maybe.
10:11:36 <monqy> dark secret sounds like you might have to assume some nasty ol axioms
10:11:57 <shachaf> monqy: i think it might a kind of dark secret that means "this has to do with a haskell thing"
10:12:03 <shachaf> because of "something i heard"
10:13:50 <shachaf> monqy: remember when ddarius was in #haskell
10:14:07 <monqy> i'm not a "#haskell guy"
10:14:50 <shachaf> except when ddarius is in it??
10:14:56 <monqy> maybe because sometimes people say funny things
10:15:08 <monqy> and occasionally i look over there when someone says a funny thing
10:15:14 <monqy> usually i just don't pay attention though
10:15:26 <monqy> by funny i mean funny in a bad way
10:16:11 <oklopol> "<shachaf> oklopol: Is megahuge set a technical term?" not afaik, although i wouldn't be that surprised if it were.
10:16:17 <monqy> like that one time that guy had that thing about learning monads from the wikipedia page and not doing any other haskell until he grokked it
10:16:32 <oklopol> i seem to remember that some of the cardinal terms are somewhat silly
10:16:40 <shachaf> did he ever succeed "in his quest"
10:16:51 <monqy> but he has said other funny things since then
10:16:55 <monqy> which i also forget
10:17:55 <shachaf> oh maybe we're thinking of different ones
10:18:17 <shachaf> what kind of "channel guy" are you
10:18:35 <monqy> i'm not really a channel guy?
10:20:24 <monqy> maybe i secretly am
10:20:27 <monqy> and i don't know it
10:21:28 <shachaf> (<~) :: Monad m => ProcessT m b c -> MachineT m k b -> MachineT m k c
10:21:31 <shachaf> mp <~ ma = MachineT $ runMachineT mp >>= \v -> case v of
10:21:36 <shachaf> Yield o k -> return $ Yield o (k <~ ma)
10:21:38 <shachaf> Await f Refl ff -> runMachineT ma >>= \u -> case u of
10:21:41 <shachaf> Stop -> runMachineT $ ff <~ stopped
10:21:43 <shachaf> Yield o k -> runMachineT $ f o <~ k
10:21:46 <shachaf> Await g kg fg -> return $ Await (\a -> MachineT (return v) <~ g a) kg (MachineT (return v) <~ fg)
10:22:44 <shachaf> -- | Build a new 'Machine' by adding a 'Process' to the output of an old 'Machine'
10:23:04 <shachaf> Process a b ~ Stop | Yield b (Process a b) | Await (a -> Process a b) (Process a b)
10:23:16 <shachaf> the second part of Await is the "failure case......"
10:23:34 <shachaf> so it's like a weird free monad
10:23:44 <shachaf> which isn't a monad come to think of it
10:23:57 <shachaf> or maybe it's just a coroutine monad applied to ()??
10:24:27 <monqy> looks like a thing alright
10:24:46 <shachaf> monqy: are you a "free monad expert"
10:24:53 <shachaf> are you even an expert in anything??
10:24:56 <shachaf> other than type theory i guess
10:25:08 <monqy> idk probably not??? :(
10:25:16 <monqy> i know some free monad stuff maybe??
10:25:20 <shachaf> you kind of sound like an expert
10:25:52 <shachaf> monqy: btw you know the STT thing?
10:26:33 <monqy> something type theory? im blanking on what the s is
10:27:28 <shachaf> mr.hird was trying to work out what a good primitive was
10:27:33 <shachaf> maybe he didn't mention it in here
10:28:28 <shachaf> monqy: so what's this Stop thing
10:28:52 <monqy> i dont know much about 'machines'
10:29:26 <monqy> im guessing it means "Stop" though
10:32:22 <oklopol> why is it co-cone and not ne
10:33:18 <oklopol> resist... urge... to say nfusion
10:34:03 <shachaf> oklopol: What do you call foo :: p b a -> Either (p b x) (p x a)?
10:37:13 <shachaf> Even though it's not quite the right name.
10:56:55 <shachaf> tee :: Monad m => ProcessT m a a' -> ProcessT m b b' -> TeeT m a' b' c -> TeeT m a b c
10:56:58 <shachaf> tee ma mb m = MachineT $ runMachineT m >>= \v -> case v of
10:57:03 <shachaf> Yield o k -> return $ Yield o $ tee ma mb k
10:57:06 <shachaf> Await f L ff -> runMachineT ma >>= \u -> case u of
10:57:08 <shachaf> Stop -> runMachineT $ tee stopped mb ff
10:57:11 <shachaf> Yield a k -> runMachineT $ tee k mb $ f a
10:57:16 <shachaf> return $ Await (\a -> tee (g a) mb $ encased v) L $ tee fg mb $ encased v
10:57:19 <shachaf> Await f R ff -> runMachineT mb >>= \u -> case u of
10:57:21 <shachaf> Stop -> runMachineT $ tee ma stopped ff
10:57:24 <shachaf> Yield b k -> runMachineT $ tee ma k $ f b
10:57:29 <shachaf> return $ Await (\b -> tee ma (g b) $ encased v) R $ tee ma fg $ encased v
10:58:47 <monqy> did someone woops something
10:59:00 <shachaf> it "tee's" 2 'machines' together
10:59:24 <monqy> it looks like it uhhhh
10:59:29 <monqy> something about two processes and a tee
10:59:34 <monqy> then you get a tee
10:59:43 <monqy> something with composing some stuff maybe
10:59:59 <shachaf> but look at that implementation
11:00:14 <monqy> i don't really want to look at that too much
11:00:25 <monqy> im not crazy enough for it
11:01:39 <shachaf> i think you have to be "real crazy" for it
11:01:47 <shachaf> like even more than mr.hird??
11:01:59 <monqy> who wrote it, mr.kmett????????
11:02:13 <monqy> being 'machines' and all
11:03:41 <shachaf> well thats what "git blame" says
11:04:39 <shachaf> but maybe it was one of the"other people"
11:05:04 <shachaf> like mr.bjarnason or mr.chiusano??????????????????????
11:05:21 <Sgeo> J forks remind me a little of Caleskell
11:05:32 <Sgeo> Or, well, the sin+cos thing,
11:07:14 -!- ogrom has quit (Quit: Left).
11:12:49 <shachaf> monqy: btw did you read those slides
11:13:24 <monqy> yeah..it made perfect sense up to the homotopys part and then it started losing me
11:13:49 <monqy> but i opened up some tabs with the stuff in it
11:14:10 <shachaf> the first word in the slides is "Homotopy".. didnt make it very far imo
11:14:45 <shachaf> btw do you know about "axiom K" and all that
11:14:57 <monqy> i've seen "axiom K" but never used it
11:15:25 <shachaf> just a lead up to a pun!!!!!!)
11:15:51 <monqy> my experience with it is limited to that chapter of "cpdt" about equality proofs. i think there's a section on axiom k in there?
11:16:26 <monqy> it's my preferred coq book
11:16:43 <monqy> so if you want to learn coq and want to learn it from a book
11:16:51 <monqy> i guess that's what i'd recommend
11:17:07 <shachaf> what about ´software foundations´
11:18:09 <monqy> software foundations goes into some pl theory stuff but sorta skimps on the coq, so it's maybe a good introduction to some of that stuff and in particular working with it in coq but
11:19:32 <monqy> i don't feel it's satisfactory if you want to get a taste from your book of the sorta stuff cpdt offers
11:19:53 <shachaf> so if i know nothing about anything
11:20:03 -!- mig22 has joined.
11:21:30 <monqy> i'd suggest read cpdt and tapl but keep sf around in case you want a "second opinion". it's only second and not third because of that Benjamin Pierce intersection
11:22:14 <monqy> I also recall sf having more exercises than cpdt that are interspersed throughout the text so you might want to follow along with it too if needed
11:23:01 <monqy> in particular if you want some pl-y exercises catered to coqwork; tapl's are more pen-and-papery unless you build the coq ground-up which is entirely reasonable if you want to I won't judge you if you do that
11:23:56 <monqy> and by read tapl i guess i mean read however much into it as it helps you understand the theory and how to work with it (proofs, etc)...no need to read it cover to cover and reabsorb all the details you're already familiar with
11:24:38 <monqy> i guess the chapter dependency list might help there...
11:25:14 <monqy> if you really want to be thorough you could also learn agda and read attapl, neither of which i have experience with...
11:27:58 <shachaf> that could be a lot of reading
11:28:12 <monqy> no need to be that thorough!!! I sure wasn't
11:28:27 <shachaf> well but you already know everything right
11:28:27 <monqy> though i often feel i should be that thorough..........
11:28:33 <monqy> i don't know agda :'(
11:28:47 <shachaf> monqy "already knows everything except agda and some math stuff" monqy
11:29:05 <monqy> in particular there are some things that i'm curious as to how agda handles, not having tactics and all
11:29:26 <monqy> like tactics are gross but they can sorta help with a few really gross things and if agda can handle them nicely that'd be really great
11:30:25 <monqy> and some other agda proofy stylistic things that i'm interested in but not as interested
11:31:56 -!- copumpkin has quit (Ping timeout: 256 seconds).
11:32:27 -!- copumpkin has joined.
11:33:06 -!- azaq23 has quit (Remote host closed the connection).
11:33:40 -!- azaq23 has joined.
11:36:16 -!- azaq23 has quit (Client Quit).
11:36:45 -!- azaq23 has joined.
11:37:15 -!- azaq23 has quit (Client Quit).
11:40:09 -!- azaq23 has joined.
11:51:07 -!- zzo38 has quit (Remote host closed the connection).
11:57:23 -!- mig22 has left.
12:03:40 -!- epicmonkey has quit (Ping timeout: 256 seconds).
12:05:50 <shachaf> https://en.wikipedia.org/wiki/Apartness_relation
12:07:06 <shachaf> do you know anything about "that stuff"
12:07:55 <monqy> uhh i think iv'e seen it maybe once?
12:08:00 <monqy> don't know much about it at all
12:08:06 <monqy> aside from well it exists
12:08:21 <monqy> and the thing with constructive logic
12:08:26 <shachaf> monqy: well that's like a cocategory!!!!
12:08:37 <shachaf> except it's "also commutative"
12:08:55 <shachaf> so i guess it's not quite it??
12:09:16 <shachaf> but you know about "constructive stuff" so maybe you know about it
12:09:37 <monqy> i've never seen apartness relations outside of wikipedia woops woops
12:09:42 <monqy> co-transitivity is kinda wacky tho
12:10:00 <shachaf> co-transitivity is what you get when you "bbiizzaarroo"ify composition
12:10:18 <shachaf> if you remember how bizarrification went
12:10:27 <monqy> "reverse the arrows"
12:10:37 <shachaf> well it's not just plain old reversing the arrows
12:10:46 <shachaf> dolio said this is called a cointernal category??
12:10:54 <shachaf> but you don't have to switch from products to sums
12:19:42 -!- carado has joined.
12:38:53 -!- DHeadshot has quit (Read error: Connection reset by peer).
12:38:58 -!- DH____ has joined.
12:42:03 -!- monqy has quit (Quit: hello).
12:46:37 -!- oerjan has joined.
12:50:56 -!- copumpkin has quit (Ping timeout: 252 seconds).
12:51:27 -!- copumpkin has joined.
12:51:54 <Phantom_Hoover> disconcerting discovery of the day: there is a duran duran wikia
12:55:07 <oerjan> Phantom_Hoover: the band or the barbarella character, and which would be more disconcerting?
12:57:08 <Phantom_Hoover> oerjan, well it'd be a bit of a stretch to have a whole wiki about a barbarella character
13:01:56 -!- Taneb has quit (Ping timeout: 252 seconds).
13:08:39 <Jafet> Hm, I didn't expect hackego would be broken this long
13:09:11 <oerjan> Jafet: wtf were you doing in there. also i don't think reverts are cumulative.
13:09:57 <Jafet> Wellll I did learn something
13:10:04 <Jafet> iconv hangs if it can't find the BOM
13:11:44 <oerjan> oh no i realize why there was that strange delquotee file
13:12:02 <oerjan> Jafet: sed -ie doesn't work as sed -i -e, it does -i with e as backup file suffix
13:12:31 <shachaf> imo delquotee sounds like a "good idea"
13:12:43 <shachaf> for most of the quotes in here
13:13:05 <Jafet> I don't think it's "easy"
13:15:40 <Jafet> Oh `revert is like emacs undo
13:15:51 <Jafet> I never understood emacs undo
13:16:10 <shachaf> Emacs undo is where a second undo undoes the first undo?
13:17:14 <Jafet> It's... complicated
13:17:15 <oerjan> @gregor HackEgo is dead, also please tell me there is a way to get the HackEgo website to show diffs between a particular revision and the tip
13:17:21 <oerjan> @tell gregor HackEgo is dead, also please tell me there is a way to get the HackEgo website to show diffs between a particular revision and the tip
13:17:45 <shachaf> class Dipointed a where tip :: p a a
13:23:52 <oerjan> Jafet: you were messing around with HackEgo so much i'm paranoid about what you actually achieved...
13:25:57 <oerjan> <Bike> it's pretty cool that one of the big category theory guys lives in a shack in the pyrenees now <-- maybe i should move to a shack in the pyrenees. i might actually get more done that way.
13:27:13 <oerjan> getting suitable broadband might be a bitch, though.
13:30:04 <oerjan> @tell OeRjAn is lambdabot case sensitive about nicks?
13:30:58 <oerjan> @tell Gregor Because checking if someone messed up horribly with a long row of commands is a bitch.
13:33:56 <oerjan> <shachaf> i don't even know what a monoid is <-- a monoid is a member of the variety of universal algebras with two operations (*) (binary) and e (constant) given by the equations a*(b*c) = (a*b)*c, e*a = a, a*e = a. hth.
13:34:40 <oerjan> (a variety is a family of universal algebras given by such equations.)
13:35:54 <oerjan> (the equations are supposed to hold for all a,b,c.)
13:38:18 <oerjan> other well-known varieties are the varieties of semigroups, groups and rings. fields are not a variety because one of the rules of fields (x invertible if x /= 0) cannot be expressed with such equations.
13:39:16 <oerjan> vector spaces can be a variety if you're willing to have one operation for multiplying by each scalar.
13:40:42 -!- Taneb has joined.
13:41:49 <oerjan> perhaps even d-modules are a variety in that way.
13:42:18 <oerjan> (ordinary modules over a fixed ring are. that's just a minor generalization of vector spaces.)
13:42:27 <Taneb> Can we give timwi a warning?
13:42:53 <Taneb> For nominating his own language for featured language
13:49:25 <oerjan> otoh the Process section seems not to be clear enough that you're only allowed to suggest _one_ language.
13:53:54 <oerjan> Funciton _is_ nice though, someone should nominate it :P
13:54:43 <Taneb> I haven't currently nominated a language, but personally I don't like Funciton, so I won't
13:55:23 <oerjan> hm Ziim also looks pretty
13:56:37 <oerjan> also ridiculously hard to program
14:04:48 <oerjan> `addquote <shachaf> wait cricket /= croquet??????????????????????????????????
14:15:24 -!- ogrom has joined.
14:41:22 <elliott> I wake up and shachaf is still doing it.
14:41:22 <lambdabot> elliott: You have 2 new messages. '/msg lambdabot @messages' to read them.
14:41:45 * shachaf tried to sleep and didn't manage it.
14:45:28 <oerjan> it's because doing it is s*hit by falling anvil*
14:48:06 <oerjan> the anvil is supposed to punish horrible puns, not make them
14:53:49 <elliott> "Nominating two of my own languages and one other."
14:53:56 <elliott> "Any user (whether registered or anonymous) can suggest a language to be featured by listing it on this page; however, *suggesting your own languages is forbidden*."
14:54:41 <oerjan> elliott: i also edited that "a" to a bolded "one"
14:54:52 <oerjan> i don't think it was quite clear before
14:57:13 * oerjan finds r/AskHistorians dangerously addictive
14:57:51 <shachaf> are you readinggit oerjan?
14:58:30 <oerjan> although i'm considering closing the subreddit after reading the tabs i've already opened
14:58:53 <oerjan> let's s/after/before/ just to be sure
15:01:13 -!- TeruFSX has joined.
15:02:15 <oerjan> they have a policy in top comments against speculation, and also a policy against quoting wikipedia. you just know it's high quality.
15:02:15 -!- yorkdove has joined.
15:04:04 -!- yorkdove has left.
15:09:48 -!- TeruFSX has quit (Ping timeout: 276 seconds).
15:15:52 -!- DH____ has quit (Read error: Connection reset by peer).
15:24:35 -!- TeruFSX has joined.
15:25:05 -!- ogrom has quit (Quit: Left).
15:45:20 -!- sirdancealot7 has quit (Ping timeout: 255 seconds).
15:57:58 -!- sirdancealot7 has joined.
16:06:04 -!- oerjan has quit (Quit: leaving).
17:33:34 <kmc> Sgeolang is J now?
17:34:26 <shachaf> Sgeolang has always been J.
17:36:54 -!- sebbu has quit (Read error: Connection reset by peer).
17:37:32 -!- sebbu has joined.
17:47:17 -!- Bike has joined.
18:07:43 -!- Nisstyre-laptop has joined.
18:09:34 -!- Phantom_Hoover has left ("Leaving").
18:09:41 -!- Phantom_Hoover has joined.
18:23:29 -!- AnotherTest has joined.
18:27:25 -!- Taneb has changed nick to Taneb|Away.
18:33:44 <fizzie> PLOOOOTS http://zem.fi/esostats/people_tod.html (disclaimer: is beta)
18:34:43 <Bike> Loading data. (Probably...)
18:34:53 <fizzie> Yes, well, it's probably loading.
18:35:13 <Vorpal> fizzie, and it loaded finally
18:35:22 <fizzie> Bike: But it would say "hopefully" if it didn't run scripts at all.
18:36:42 <fizzie> Vorpal: Well, I mean, I think it was shachaf that told me to make http://zem.fi/esostats/charfreq_h.html when there was discussion about the h-index of yesterday, and it just sort of went from there.
18:36:43 <Vorpal> fizzie, is there number of characters per message?
18:36:55 <Vorpal> fizzie, I want to see if I write longer messages at certain times of the day
18:36:55 <fizzie> Not yet. It's all very preliminary.
18:37:16 <Vorpal> probably not, but it would certainly be an interesting result if that varied widely
18:38:48 <fizzie> Also it should be probably possible to deselect "other" if you just want to see your own numbers and aren't prolific enough for that to be a large fraction.
18:39:08 <elliott> fizzie: How did you pickify the list of people?
18:39:15 <elliott> I like how I am on that list ~50 times.
18:39:25 <elliott> I also like how can you please let that list be resized or make it bigger?
18:40:06 <elliott> I like how that plot shows me being awake roughly 24 hours a day.
18:40:27 <fizzie> elliott: By an impartial method, I forget how exactly. Something about taking some kind of a top-100 list and then grouping duplicates I noticed. (I don't really know all your various names.)
18:40:46 <FreeFull> It shows me as being the most active around 9pm
18:41:02 <Bike> elliott: is that inaccurate
18:41:25 <Bike> elliott: what do i ask monqy
18:41:27 <elliott> fizzie: Why is fax "fax:" on that list?
18:42:01 <elliott> fizzie: OK, I'm actually on the list twice.
18:42:23 <shachaf> fizzie: Can you run this on #haskell?
18:42:45 <fizzie> shachaf: I don't have #haskell logs in my postgres db. I'd need to write an importer first. :/
18:44:01 <fizzie> elliott: I have merged it (and fixed fax), but it'll take a while before I can be bothered rerunning the whole people-activity deal. It's written so that it's cheap to update incrementally, but processing the whole thing takes maybe twenty minutes if I change the list-of-collected-nicks.
18:44:02 <elliott> http://zem.fi/esostats/fig/bots_20y.png
18:44:11 <elliott> fizzie: How come lambdabot-or-maybe-fungot started existing in 2002?
18:44:12 <fungot> elliott: the best way would be to interpret them as it wants, evaluating them at macroexpansion time, i decided i'd make an asian pregnant one. or something.
18:44:22 -!- Vorpal has set topic: WHYH HHHHHHELLOHH THEHRE | FOUR SIMULTANEOUS TYPE SYSTEMS IN A SINGLE ROTATION OF THE LAMBDA CUBE | concealed in fold of goat-time lumber | http://codu.org/logs/_esoteric/ | Graphs! http://zem.fi/esostats/index.html.
18:44:29 <Bike> fungot, how do you feel about this?
18:44:30 <fungot> Bike: i just had more pieces. and then, do so
18:44:40 <fizzie> elliott: That's just it defaulting to zero from the beginning of the logs. :/
18:45:09 <Bike> i think the topic is making progressively less sense...
18:45:49 -!- elliott has set topic: STOP STOP STOP STOP STOP http://codu.org/logs/_esoteric/ START AGAIN.
18:45:55 <Vorpal> fizzie, selecting a normalized plot for 2002 looks REALLY weird
18:46:00 <Vorpal> is there no data for most of it?
18:46:23 <elliott> Well, the channel only existed for, like, a few weeks in 2002.
18:46:47 <fizzie> Vorpal: Yes, it's really quite sparse.
18:46:59 <fizzie> Vorpal: I suppose it does end up as zeros for most of it.
18:47:15 <Vorpal> fizzie, there are gaps up until 2006 I think you do a single year
18:47:25 <Vorpal> less and less gaps for each year
18:48:23 <fizzie> Vorpal: The gaps go (partially) away if you add some smoothing. I suppose it's just hitting particular two-minute intervals for which the total numbers end up as zero.
18:58:39 -!- ogrom has joined.
18:59:17 -!- FreeFull_ has joined.
18:59:41 -!- FreeFull has quit (Read error: Connection reset by peer).
19:00:49 -!- FreeFull_ has changed nick to FreeFull.
19:03:23 -!- Taneb|Away has changed nick to Taneb.
19:12:57 <Taneb> There are graphs charting individual people?
19:13:50 <AnotherTest> Well it shows elliott in yellow, ais523 in red, oerjan in blue, fizzie in green etc. for me
19:14:29 <AnotherTest> and elliott alone seems to produce about 1/4 of the messages
19:14:52 <elliott> Phantom_Hoover: weren't you here in 1993
19:15:00 <elliott> (1993 was 20 years ago???????????????)
19:15:16 -!- ogrom has quit (Ping timeout: 256 seconds).
19:16:28 <shachaf> past your ʹ Phantom_Hoover
19:17:00 * Gregor shakes his cane at you.
19:17:01 <lambdabot> Gregor: You have 3 new messages. '/msg lambdabot @messages' to read them.
19:17:57 -!- ais523 has joined.
19:18:03 -!- HackEgo has quit (Remote host closed the connection).
19:18:13 -!- HackEgo has joined.
19:18:44 <Taneb> shachaf, you're stupid fake old
19:19:25 -!- sebbu has quit (Read error: Connection reset by peer).
19:19:35 <ais523> the word "fuck" has a meaning that depends heavily on context, and arguably doesn't have a meaning in its own right nowadays
19:19:43 <ais523> as a result, can it actually be considered a swearword?
19:19:47 <ais523> ("shit" is in a similar situation)
19:19:53 <Taneb> It's a swearthingy
19:20:22 -!- sebbu has joined.
19:20:29 <ais523> "brainfuck" is its own entity
19:20:38 <olsner> it's a swearword when you use it for swearing? whatever swearword is supposed to mean
19:20:54 <ais523> yeah, that's a good point
19:21:13 <ais523> I guess the definition of a swearword is a word whose actual meaning is irrelevant, you just say it when annoyed or for shock value
19:21:36 -!- ogrom has joined.
19:22:52 <olsner> ais523: I think that definition makes "fuck" clearly a swearword
19:23:06 <ais523> Phantom_Hoover: when used as a swearword, it does; "damn" without context is without context
19:23:08 <ais523> olsner: yeah, I guess so
19:23:25 <ais523> I think the argument is more that they aren't swearwords unless they're being used as swearwords
19:23:25 <Phantom_Hoover> ais523, so do you interpret 'fuck you' the same as you do 'damn you'.
19:23:30 <shachaf> did you know: voltage is a swearword
19:23:46 <shachaf> people say it for shock value all the time
19:23:47 <ais523> Phantom_Hoover: yeah, but "fuck you" is a compliment rather than an insult if you interpret it that way
19:24:17 <Phantom_Hoover> Er, some people would disagree strongly on that point.
19:24:46 <elliott> nonconsensual sex is not generally agreed to be complimentary
19:24:51 <elliott> or do I completely misunderstand the interpretation here
19:25:18 <Jafet> Swearing is what happens when I break hackego
19:26:49 <Jafet> We had an impedance mismatch with that pun, try a more current one.
19:27:17 <ais523> there's nothing about the word "fuck" that implies nonconsensual, though
19:27:33 <ais523> when it's actually being used with its original meaning, it normally refers to consensual sex
19:28:38 <FreeFull> Fuck is actually a pretty ancient word
19:28:39 <ais523> Phantom_Hoover: well I rarely hear it used with its original meaning
19:28:43 <Bike> haha "original meaning"
19:28:49 <elliott> well surely if you interpret "fuck you" hyperliterally like that it is an unsolicited sexual advance
19:29:03 <elliott> this interpretation seems pretty hopelessly tortured in general though
19:29:08 <elliott> since it's not even really grammatical
19:29:12 <Phantom_Hoover> ais523, be honest, how often do you hear damn used with its original meaning
19:29:14 <Taneb> It should be "fuck yourself"
19:29:20 <olsner> "It may go back to the Proto-Indo-European *pug-, *puǵ- ("to strike"; source of Latin pūgnus (“fist”) among many others) ..."
19:29:41 -!- sebbu2 has joined.
19:29:59 <ais523> it's not zero, but it's quite low
19:30:00 -!- sebbu2 has quit (Changing host).
19:30:00 -!- sebbu2 has joined.
19:30:25 <Bike> Phantom_Hoover: like german ficken?
19:30:43 <Bike> oh, that's not actually cognate
19:30:53 <Bike> false fuckbuddies
19:31:00 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
19:31:14 <Bike> oh it might be cognate
19:31:19 <Bike> god i love historical linguistics
19:31:26 -!- Nisstyre-laptop has quit (Read error: Connection reset by peer).
19:32:04 <FreeFull> What stops me with flooding $pwd with files until it's full
19:32:17 <Bike> your highly developed sense of ethics
19:32:39 -!- tromp has quit (Remote host closed the connection).
19:33:03 -!- sebbu has quit (Ping timeout: 245 seconds).
19:34:13 -!- tromp has joined.
19:39:19 <FireFly> On the topic of "to fuck": http://douglemoine.com/english-sentences-without-overt-grammatical-subjects/
19:43:31 -!- noam__ has joined.
19:44:54 <ais523> wow, I think I discovered a new level of YouTube comment stupidity
19:44:56 <ais523> "How on earth did you record video/audio in 2006?"
19:46:21 <Taneb> 2006 was the year when they banned cameras
19:46:53 -!- noam_ has quit (Ping timeout: 255 seconds).
19:47:55 <ais523> I had to double-check the year to make sure it didn't say 1996 (which would have been slightly less stupid)
19:48:25 <FreeFull> You still could record video and audio in 1996
19:49:17 <ais523> but I could excuse not knowing that, due to the primitive state of the Web at the time
19:49:31 <ais523> and, as a result, the disconnect in hardware knowledge between different people
19:50:27 <ais523> hmm… in 1986, you could definitely record it, but not digitally
19:50:37 <ais523> you'd need to use film and tape
19:50:45 <AnotherTest> ais523: You just disappointed me. I always though you were a timetraveler :(.
19:51:57 <ais523> btw, a hilarious thought: I saw an advert for the Nokia Lumia (their windows 8 phone thing), and the vast majority of the things advertised in the advert were hardware features, and unrelated to the OS
19:52:30 <AnotherTest> Did you see that in the future, past or present?
19:52:32 <FreeFull> ais523: I saw an advert for the lumia, and went bleck at all parts where you could see windows 8
19:52:51 <ais523> AnotherTest: past, /obviously/
19:55:20 <ais523> if I never know, why would you ask me?
19:56:29 <AnotherTest> hm I guess s/you(.*)knows/one\1knows would do that
19:57:37 <Vorpal> <ais523> wow, I think I discovered a new level of YouTube comment stupidity <ais523> "How on earth did you record video/audio in 2006?" <-- yeah that is pretty random.
19:57:45 <AnotherTest> Also, assuming you was referring to you, ais523, you might know it in the future
19:57:49 <Vorpal> stupid? maybe. It just seems totally random to me
19:58:17 <AnotherTest> Although I should perhaps have said "will never know" to avoid that situation
19:59:34 <AnotherTest> ais523: I think I finally figured out what 523 is referring to
19:59:40 <ais523> AnotherTest: it's a random number!
19:59:52 <ais523> I tell this to anyone who asks, because it's true
19:59:57 <ais523> just people don't ask very oftne
19:59:58 <AnotherTest> Not it's not, it's you keeping track of the instances there exist of yourself!
20:00:42 <AnotherTest> This is why you didn't want me to use ais521 - your good prime twin brother -: it was you but in a different time!
20:03:17 -!- zzo38 has joined.
20:05:09 <AnotherTest> seems like ais523 is actually a pointer to ais
20:05:23 <ais523> "ais" is pretty ambiguous by itself
20:06:28 <AnotherTest> Are you actually an Artificial Intelligence System from the 523st century?
20:07:16 <Gregor> AWAY! TO THE FIVE HUNDRED TWENTY THIRST CENTURY!
20:16:51 <Phantom_Hoover> ais523, don't you always tell everyone about how it was your university account name or something
20:17:11 <Vorpal> hm it seems ssh has an escape char in the form of ~ (try ~?<enter>). I knew of ~.<enter> before to kill a broken ssh connection
20:17:12 <ais523> that's where the random number came from
20:17:17 <Vorpal> but the rest of it was new to me
20:17:22 <ais523> Vorpal: it's <enter>~.
20:17:25 <Vorpal> seems you can add port forwarding on the fly
20:17:34 <ais523> and yeah, there are a bunch of other commands there
20:17:40 <ais523> <enter>~ is the escape char
20:17:46 <Vorpal> I always had to add a new line at the end to make it work
20:17:48 <ais523> otherwise it'd be triggered by accident too often
20:17:56 <Vorpal> is it because my ~ is a dead key?
20:18:24 <ais523> Vorpal: oh, yeah, probably
20:18:24 <Vorpal> ais523, but yeah I need enter at the start too
20:18:34 <ais523> so ~<enter> is how you type the ~
20:18:51 <Vorpal> ais523, no I mean I go: <enter>~<space>.<enter>
20:19:11 <Vorpal> the space to deal with the dead key
20:19:45 <Vorpal> ais523, enter altgr+~ altgr+~ . seems to work too
20:20:04 <Vorpal> ~~ - send the escape character by typing it twice
20:21:08 <Vorpal> ~R - Request rekey (SSH protocol 2 only)
20:21:25 -!- oerjan has joined.
20:23:18 -!- ogrom has quit (Ping timeout: 256 seconds).
20:25:12 <mroman> http://golf.shinh.org/p.rb?shortest+non+occuring+sequence
20:25:20 <mroman> There are two algorithms to solve that problem.
20:25:29 <mroman> One is to generate all possible solution
20:25:48 <mroman> however, not exponential to the length of the input but exponential to the length of the solution.
20:26:04 <mroman> the other algorithm is polynomial to the length of the input.
20:26:44 <mroman> obviously If you want a longer solution you have to cover more subsequences therefore the length of the input increases
20:27:05 <mroman> probably the length of the input increases exponentially to the length of the solution.
20:27:20 <mroman> which states the question
20:27:27 <mroman> are both algorithms exponential?
20:28:41 <mroman> given there is an algorithm a which can solve a problen in a^b which is independent of the input size
20:29:32 <mroman> and an algorithm b with O(n^c) which is dependent on the input size and the input size increases probably somewhere near a^b
20:29:40 -!- ogrom has joined.
20:30:16 <Vorpal> mroman, hm interesting point
20:30:35 <mroman> You can generate all possible substrings, sort them and find the first missing
20:31:10 <mroman> but I'm not sure if that is actually slover than the brute force algorithm.
20:33:30 <mroman> aaaaaaaaaaaaaaaaaaaaaaaaaa
20:33:44 <mroman> the brute force algorithm will find a solution in O(1)
20:33:53 <mroman> because the result is a sequence of length 1
20:34:04 -!- ogrom has quit (Ping timeout: 256 seconds).
20:34:15 <oerjan> hm if x is the solution then xa...a is the solution to the similar problem with a fixed length
20:34:18 <mroman> the generate all substring algorithm takes a long time to solve it.
20:35:58 <mroman> Is there a classification for algorithms which do not depend on the size of the input but on the size of the output :D?
20:36:47 <Bike> the size of the output is a function of the input, isn't it
20:36:53 <mroman> well, you have to check your solution against the input
20:36:54 -!- ogrom has joined.
20:36:57 <mroman> so it does depend on the input
20:37:01 <Bike> just not one that's linear in the length of the input, in this case
20:37:36 <mroman> O(n*a^b) where a is the alphabet size and b the size of the output.
20:38:22 <mroman> Bike: But you don't know the size of the output yet
20:38:37 <mroman> well, b <= n obviously
20:38:58 <Bike> so what, we're talking about the complexity of an algorithm, not finding the output itself!
20:39:36 <Bike> the complexity of euclid's algorithm depends on a shitload of insane stuff that's harder to find than the gcd~
20:40:52 <mroman> I guess one has to calculate how big n has to be to generate a solution of at least size b.
20:41:10 <Vorpal> mroman, what is the average running time of these algorithms though?
20:41:17 -!- Arc_Koen has joined.
20:42:32 <mroman> For a solution of length two you need at least an input of size 3
20:44:03 -!- AnotherTest has quit (Quit: Leaving.).
20:44:16 <mroman> It's difficult to calculate
20:45:13 <mroman> abccaacbabb has aaa as a solution.
20:46:10 <mroman> now you'd have to calculate how many characters you need to add to increase the solution to aaaa ;)
20:46:21 <Vorpal> mroman, wasn't it the shortest solution?
20:46:31 <mroman> (assuming the alphabet is abc)
20:47:06 -!- ogrom has quit (Ping timeout: 256 seconds).
20:47:22 <mroman> there is exactly one solution if that's what you mean.
20:47:52 <mroman> I'm pretty certain that the required input size increases exponential.
20:47:53 <Vorpal> mroman, well there could be several. both bc and ac could be missing from the string for example
20:48:00 <mroman> All empiric data suggests so.
20:48:13 <mroman> but I have no formal proof whatesoever to back it up :)
20:48:39 <Sgeo> :( why aren't J verbs closures?
20:48:54 <Bike> does J even have lexical binding
20:49:54 <Sgeo> It has a form of local variables
20:50:06 <Sgeo> =. inside a verb defines a variable local to that verb
20:50:47 <kmc> 'The tempest prognosticator, also known as the leech barometer, is a 19th-century invention by George Merryweather in which leeches are used in a barometer. The twelve leeches are kept in small bottles inside the device; when they become agitated by an approaching storm they attempt to climb out of the bottles and trigger a small hammer which strikes a bell. The likelihood of a storm is indicated by the number of times the bell is str
20:51:10 <Bike> The likelihood of a storm is indicated by the number of times the bell is str
20:54:25 <Sgeo> Of course J control structures aren't expressions
20:55:41 <Bike> hey foul, you already complained about that yesterday!
20:55:54 <Bike> also i thought a large part of j was mapping things over things instead of control flow
20:57:17 <Sgeo> I complained about a different but related thing yesterday
20:57:26 <Bike> convolute with the step function instead of conditionalizing on <, or some shit
20:57:51 <Sgeo> Wouldn't be surprised
21:02:14 -!- monqy has joined.
21:07:25 -!- ogrom has joined.
21:08:19 <oerjan> @tell evincar The haskell solution to type inferencing arbitrarily ordered function definitions is to do an initial dependency graph calculation and infer strongly connected components together in an order such that everything they depend on is inferenced first. so functions in the same strongly connected component can only call each other with one type. you can use explicit type annotations to break this restriction ("polymorphic recursion")
21:15:43 -!- WeThePeople has joined.
21:17:35 -!- carado has quit (Ping timeout: 246 seconds).
21:17:54 -!- carado has joined.
21:22:29 -!- carado has quit (Ping timeout: 246 seconds).
21:35:48 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
21:36:43 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
21:37:33 <oerjan> `fetch http://google.org/
21:37:42 <oerjan> `fetch http://google.com/
21:38:03 <kmc> i have a file named /.pulse-cookie :(
21:38:17 <oerjan> Gregor: HackEgo THE BROKEN
21:39:23 <Bike> kmc: well what is it
21:39:34 <kmc> some pulseaudio bullshit
21:39:36 <kmc> either that or a rootkit
21:40:40 <Bike> oh hey i have it too
21:41:24 <Bike> it is an "authentication cookie"
21:42:13 -!- sebbu2 has quit (Ping timeout: 245 seconds).
21:48:51 -!- asiekierka has quit (Excess Flood).
21:49:59 -!- asiekierka has joined.
21:53:12 -!- sebbu has joined.
21:53:12 -!- sebbu has quit (Changing host).
21:53:12 -!- sebbu has joined.
22:01:21 -!- Taneb has quit (Quit: Leaving).
22:03:38 <Bike> hell is anything working
22:03:55 <oerjan> `help is not inside the sandbox, but then neither is `revert or `fetch
22:04:14 <Sgeo> abs =: + ` - @. (< & 0)
22:05:13 <Bike> that seems overcomplicated
22:05:20 <Bike> don't you have the sign function?
22:05:56 <ais523> oerjan: `help /could/ be inside the sandbox, so I was trying to determine whether it was or not
22:05:59 <fungot> (^<lang> <code>; ^def <command> <lang> <code>; ^show [command]; lang=bf/ul, code=text/str:N; ^str 0-9 get/set/add [text]; ^style [style]; ^bool)S
22:06:01 <Sgeo> There probably is, but I just took that definition from the book
22:06:27 -!- sebbu has quit (Ping timeout: 276 seconds).
22:07:07 <Bike> imo just :sign dup sgn *;
22:07:35 -!- ogrom has quit (Ping timeout: 256 seconds).
22:07:52 <Bike> whatever, i don't actually know forth
22:08:45 <Sgeo> Actually, don't need a fork, I can do the other thing
22:09:25 <Sgeo> As a monad it's signum
22:09:33 <Sgeo> As a dyad it's multiplication
22:11:19 -!- sebbu has joined.
22:11:19 -!- sebbu has quit (Changing host).
22:11:19 -!- sebbu has joined.
22:45:41 <zzo38> I have idea of a small header NSF variant, which may be used when storing the music in a SQLite database used with some game, for example. It is fourteen bytes, consisting of the bankswitches, load, init, play. The high four bits of the load address are used to control the VRC6, VRC7, FDS, and Sunsoft-5B expansions (the MMC5 and Namco-163 are always enabled).
22:49:09 <Sgeo> mean =. +/ % #
22:49:16 <Sgeo> How can that be written in pointfree Haskell?
22:49:37 <monqy> what sort of stuff are you allowing
22:49:52 -!- azaq23 has quit (Quit: Leaving.).
22:50:17 <zzo38> If the blob length is exactly twelve bytes, then it is instead a 64-bit rowid of the actual NSF data, followed by the A, X, Y, and flags. X must be zero or one, and this is also used to control NTSC/PAL. (For the format described above, A and X are zero, and the Y and flags are undefined.)
22:50:47 <Sgeo> > sum [1, 2, 3]
22:51:06 <Sgeo> @pl (\arg -> (sum arg)/(length arg))
22:51:08 <oerjan> > (/) <$> sum <*> genericLength $ [1,2,3]
22:53:32 <Sgeo> Not quite like the J version though. +/ is Haskell sum, but it's not primitive, / is sort of like a fold
22:53:32 <lambdabot> Functor f => (a -> b) -> f a -> f b
22:53:50 <Sgeo> (Also the J version has that whole built-in mapping thing going)
22:54:30 <Bike> i imagine sum is defined as foldr (+) or whatever
22:54:40 <Bike> sooooo pretty well the same
22:55:24 <Sgeo> I don't entirely understand how / knows what identity to use
22:55:35 <elliott> operations encode their identity in J
22:55:51 <monqy> isnt the term something like "obverse"
22:56:07 <elliott> I had to look that up how do you know that
22:56:18 <monqy> memory for silly things like that
22:56:20 <Bike> been starin' at too many coins
22:56:23 <elliott> now I'm looking at the J vocabulary again and remembering how beautiful a language it is
22:58:48 <Sgeo> elliott, is it your fault for getting me into Factor and J with some comment somewhere about how they're your favorite languages but annoyingly ungoogleable?
22:59:19 <elliott> monqy: have you written any cute J programs. I love cute J programs
23:00:03 <monqy> maybe i should write a roguelike in j
23:00:10 <monqy> (haaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaah)
23:00:46 <elliott> Sgeo: btw there are aliases for the magic numbers foreign uses in the J library
23:01:13 <Sgeo> What about other magic numbers, like the Extract Gerund thingy?
23:01:48 <elliott> you can poke around the code and see
23:05:07 <zzo38> Write a roguelike in RogueVM.
23:05:37 <Bike> write a J->RogueVM compiler
23:07:22 <Sgeo> "The result of 0: is a boolean 0 ; previously it was an integer 0 . Likewise 1: ."
23:07:36 <Sgeo> I ... what's the difference? Internal representation?
23:08:32 <zzo38> Bike: You can try if you want to.
23:10:22 <Bike> maybe it has types
23:11:36 <Bike> also when i google "j language dictionary" i get a karen-english dictionary. what does this mean
23:13:10 -!- Bike has quit (Quit: dead).
23:17:13 -!- Bike has joined.
23:18:54 -!- evincar has joined.
23:30:05 -!- Cryovat has quit (Quit: BOOM).
23:31:54 <kmc> woah people are talking about J
23:32:18 <Sgeo> I blame Bike for reminding me about J.
23:32:36 <Bike> i already denied responsibility
23:33:23 <Bike> no i did it yesterday
23:33:26 <Bike> opposite of late
23:33:44 <Sgeo> Actually, it's also a little Gilad Bracha's fault. In a talk about mirrors, he briefly mentioned APL as a language that has a lot of ... metaprogrammingness. APL makes me think J.
23:33:50 <elliott> oerjan: what does it mean that I read that as anna j ketamine
23:34:05 <elliott> Sgeo: wow you still listen to things gilad bracha says...
23:38:11 <tswett> nooga is someone we know, aren't they?
23:43:02 -!- DHeadshot has joined.
23:55:50 -!- DHeadshot has quit (Read error: Connection reset by peer).
23:55:59 -!- DH____ has joined.