←2013-06-30 2013-07-01 2013-07-02→ ↑2013 ↑all
00:00:46 <hagb4rd> `run echo hi
00:00:51 <HackEgo> hi
00:00:56 <hagb4rd> hm
00:01:45 <oerjan> i think that may be somewhat random hth
00:01:46 <hagb4rd> ok
00:02:01 <oerjan> (also it means that did not help hth)
00:02:14 <oerjan> or possibly does
00:02:19 <hagb4rd> it's not that there is a full device or sth ..lol?
00:02:29 <oerjan> of course there is
00:02:34 <hagb4rd> okay
00:02:45 <oerjan> `echo hi
00:02:48 <HackEgo> hi
00:02:57 <oerjan> `? tdnh
00:03:01 <HackEgo> tdnh? ¯\(°_o)/¯
00:03:02 <myndzi> |
00:03:02 <myndzi> o/`¯º
00:03:16 <oerjan> `learn tdnh does not help
00:03:21 <HackEgo> I knew that.
00:03:32 <hagb4rd> this*?
00:03:50 <hagb4rd> what's the t for?
00:03:59 <oerjan> i think you don't have the spirit of `? hagb4rd
00:04:09 <hagb4rd> oh
00:04:10 <hagb4rd> ok
00:04:18 <hagb4rd> maybe
00:04:33 <oerjan> also it means whatever fits the context hth
00:05:41 <hagb4rd> ic
00:06:34 -!- hagb4rd has changed nick to halfb4rd.
00:09:24 <halfb4rd> i'll consider that
00:17:59 -!- sprocklem has quit (Remote host closed the connection).
00:25:15 -!- zzo38 has joined.
00:46:14 <coppro> why does meta-0 cause a list of local hostnames to be printed, and then 's0' input?
00:46:18 <coppro> (at a shell)
00:47:29 -!- Bike has quit (Ping timeout: 248 seconds).
00:52:44 -!- Nisstyre has quit (Quit: Leaving).
00:53:01 <shachaf> ion: I bet you like Adámek's theorem!
00:55:26 <shachaf> oerjan: help how do i get intuition for limits and things that preserve limits and all that
00:57:49 <oerjan> magic hth
00:58:59 -!- Bike has joined.
01:00:05 <ion> shachaf: I love it.
01:20:26 -!- Bike has quit (Ping timeout: 246 seconds).
01:23:28 -!- Bike has joined.
01:29:05 -!- Bike has quit (Ping timeout: 248 seconds).
01:37:14 -!- Bike has joined.
01:43:34 -!- Bike has quit (Ping timeout: 246 seconds).
01:46:03 <tswett> Have some weird combinators: http://pastebin.ca/2413173
01:48:41 <tswett> What do they mean, what do they do?
01:49:28 <Phantom_Hoover> i'm pretty sure cancel's just there to annoy elliott
01:53:13 <tswett> Why would that annoy elliott?
01:53:41 <Phantom_Hoover> because he's a constructo-fascist?
01:55:09 -!- sprocklem has joined.
01:57:08 <ion> AT&T Archives: The UNIX Operating System http://youtu.be/tc4ROCJYbm0
01:59:20 <tswett> cancel (\(\x -> y) -> y) = x
01:59:31 <tswett> I'm pretty sure that's a legitimate definition.
02:00:25 <tswett> Albeit rather silly...
02:00:41 <Sgeo> It... pattern matches on lambdas?
02:01:32 <copumpkin> o.O
02:01:57 <tswett> Well, here's what it does.
02:02:01 <tswett> cancel takes a function, f.
02:02:09 <copumpkin> supercancel :: (A -o Bottom) -o A
02:02:16 <copumpkin> supercancel (\x -> y) = x
02:02:21 <copumpkin> >_>
02:02:30 <Sgeo> What does -o even mean??
02:02:42 <tswett> That function, f :: (A -o Bottom) -o Bottom, will inevitably be called exactly once, with some argument, g :: A -o Bottom.
02:02:52 <tswett> In turn, g will inevitably be called exactly once, with some argument x :: A.
02:02:56 <tswett> cancel f returns x.
02:03:06 <tswett> Sgeo: it pretty much denotes a function.
02:03:11 <Sgeo> I assume this isn't Haskell. What language is it?
02:03:38 <tswett> Linear logic, written like Haskell.
02:05:12 <tswett> Wait, I got it wrong.
02:05:22 <tswett> Okay, *here's* what cancel does.
02:06:20 <tswett> cancel takes a function, f :: (A -o Bottom) -o Bottom. It makes up a function g :: (A -o Bottom) and calls f with it. f will then call g exactly once, with some argument x :: A.
02:06:23 <tswett> cancel f returns x.
02:09:01 <oerjan> so basically linear logic with continuations?
02:09:31 <tswett> No, pretty sure this is just plain linear logic.
02:09:54 <oerjan> um you can actually construct cancel?
02:10:10 <tswett> Yeah, I'm pretty sure you can prove ((A -o Bottom) -o Bottom) -o A.
02:10:36 <copumpkin> is it an axiom?
02:10:41 <copumpkin> or what axioms do you use to build it?
02:11:02 <tswett> Uh, lemme see. ((A -o Bottom) -o Bottom) -o A is defined as...
02:11:05 <oerjan> oh hm linear logic is not intuitionistic-like
02:11:30 <oerjan> is A -o Bottom the same as not A again
02:11:37 <tswett> It's the dual of A, yes.
02:11:45 -!- nooodl_ has quit (Ping timeout: 248 seconds).
02:11:58 -!- Phantom_Hoover has quit (Ping timeout: 256 seconds).
02:13:23 <tswett> That thing is defined as ~(~(~A | Bottom) | Bottom) | A, which is ((~A | Bottom) * One) | A, which, by units, is ~A | A.
02:13:38 <tswett> So then you can just do an initial sequence.
02:14:04 <copumpkin> yeah, but I mean if all you have are axioms and you want to do some natural deduction to get at that
02:14:06 <copumpkin> what would you do?
02:14:45 <tswett> Uh, I guess first you use the initial sequent inference rule to get ~A | A.
02:15:12 <tswett> Then, uh...
02:15:35 <shachaf> hi copumpkin
02:15:44 <shachaf> i bet you like fixed points
02:15:46 <copumpkin> hi
02:15:52 <tswett> Something complicated involving the cut rule...
02:15:59 <copumpkin> shachaf: no, I hate them
02:16:38 <shachaf> copumpkin: good
02:16:47 -!- Bike has joined.
02:16:52 <shachaf> copumpkin: can you tell me a haskell type that has more than 2 fixed points but not infinitely many?
02:17:11 <Bike> what's a fixed point of a type
02:17:35 <shachaf> Bike: Nat is a fixed point of Maybe
02:17:53 <tswett> I've always wanted the "->" in "\x -> y" to be an infix operator whose arguments are \x and y.
02:17:55 <copumpkin> shachaf: no, but perhaps that Tree^7=Tree thing might inspire you?
02:18:06 <copumpkin> or was it 4
02:18:06 <tswett> And that's because there's a continuous bijection between Nat and Maybe Nat?
02:18:24 <Bike> right, nevermind
02:18:25 <shachaf> continuous?
02:18:44 <tswett> Continuous.
02:18:51 <copumpkin> Continuous!
02:19:04 <shachaf> what does continuous mean :'(
02:19:18 <tswett> The inverse image of every closed set is closed.
02:19:18 <Bike> what are the open sets in Maybe
02:19:56 <tswett> I guess all subsets of Nat are open.
02:20:01 <tswett> And all subsets of Maybe Nat are open, too.
02:20:24 <shachaf> btw Maybe has more than one fixed point
02:20:27 <copumpkin> clopen
02:20:38 <Bike> do we have to use the strong topolgy
02:20:54 <tswett> A subset S of Maybe t is open if and only if the set of x such that Just x is in S is open.
02:21:03 <shachaf> copumpkin: just clopen your mouth thx
02:23:28 -!- sacje has joined.
02:23:34 <copumpkin> :(
02:23:42 <tswett> Here's my latest attempt at defining cancel:
02:23:43 <tswett> cancel f = (f (\x -> )) x
02:24:04 <copumpkin> hmmm
02:24:08 <Bike> shachaf: but seriously what's a fixed point.
02:24:15 <Bike> also is it type or type constructor or what.
02:24:20 <Bike> i dunno man. i like fixed points . help
02:24:22 <shachaf> copumpkin: hey it's not my fault your mouth is a continuous function :'(
02:24:36 <shachaf> @hug copumpkin
02:24:36 <lambdabot> http://hackage.haskell.org/trac/ghc/newticket?type=bug
02:24:48 <comex> til about linear logic
02:24:56 <copumpkin> linear logic is teh shitznit
02:24:59 <copumpkin> duh
02:25:07 <shachaf> Bike: A fixed point of F is an X such that X = F(X)
02:25:15 <Bike> yes
02:25:18 <comex> now i must sleep
02:25:26 <shachaf>
02:25:33 <Bike> but like
02:25:35 <copumpkin> ( ͡° ͜ʖ ͡°)
02:25:37 <Bike> Maybe Nat isn't Nat
02:25:43 <shachaf> Bike: But it's isomorphic.
02:25:44 <copumpkin> Bike: sure it is
02:26:14 <shachaf> Bike: A fixed point of F is an X such that X ≅ F(X) # hth
02:26:14 <tswett> Okay, suppose that f = \g -> g 5. Then cancel f = (f (\x -> )) x = ((\g -> g 5) (\x -> )) x = ((\x -> ) 5) x = 5.
02:26:16 <tswett> Right?
02:27:05 <tswett> This makes perfect sense and is absolutely correct.
02:27:32 -!- augur has quit (Remote host closed the connection).
02:30:46 <shachaf> Bike: What kind of fixed points do you like?
02:31:15 <Bike> ones that make sense.
02:31:36 -!- augur has joined.
02:31:39 <tswett> converse f = (f (\g -> x)) (g, (\x -> ))
02:31:56 <shachaf> Bike: You can represent natural numbers are follows: Nothing, Just Nothing, Just (Just Nothing), ...
02:32:04 <shachaf> s/are/as/
02:33:03 <Bike> sure
02:33:10 <Bike> that has even less to do with Nat.
02:33:17 <shachaf> ?
02:33:46 <shachaf> There's an obvious isomorphism to natural numbers.
02:33:48 <Bike> You were saying that F was Maybe (: * -> *) and X was Nat (: *)
02:33:54 <shachaf> Right.
02:34:06 <Bike> Now you're talking about some other isomorphism for some reason.
02:34:19 <shachaf> I am?
02:34:29 <shachaf> Nothing :: Maybe (Maybe (Maybe (Maybe ...
02:34:32 <shachaf> Just Nothing :: Maybe (Maybe (Maybe (Maybe ...
02:34:35 <shachaf> Just (Just Nothing) :: Maybe (Maybe (Maybe (Maybe ...
02:34:46 <shachaf> That type on the right is a fixed point of Maybe.
02:35:07 <shachaf> In particular it's the least fixed point of Maybe (let's say).
02:35:17 <shachaf> And it's obviously isomorphic to Nat.
02:35:44 <oerjan> a -o b = (not a) par b = not (a times (not b))
02:36:56 <oerjan> so ((a -o bottom) -o bottom) -o a = not (((a -o bottom) -o bottom) times (not a))
02:37:36 <shachaf> Is (∀r. ((A -> r) -> r) -> r) isomorphic to (A -> Void)?
02:37:38 <Bike> so what's another fixed point of Maybe.
02:37:58 <zzo38> I think the operator in linear logic which corresponds to the bottom of intuitionistic and classical logic, is zero, not bottom, isn't it?
02:38:02 <shachaf> Bike: Conat
02:38:06 <shachaf> Bike: I.e. Nat + infinity
02:38:13 <oerjan> cancel (f, acont) = f acont
02:38:33 <copumpkin> Nat + infinity in such a way that you can't tell them apart, of course
02:39:23 <copumpkin> did anyone see my fancy agda with conats?
02:40:08 <shachaf> https://gist.github.com/copumpkin/4647315 ?
02:40:22 <copumpkin> yeah
02:42:31 * shachaf should write some Agda.
02:42:33 <shachaf> It looks like fun.
02:45:58 <shachaf> copumpkin: Nu is so great imo
02:45:59 <shachaf> best type
02:46:04 <shachaf> but it has a bad name
02:46:17 <shachaf> maybe i should call Mu Lfix and Nu Gfix................................................!
02:46:25 <copumpkin> @let data Metal a = Metal a
02:46:26 <lambdabot> Defined.
02:46:28 <copumpkin> :k Nu Metal
02:46:29 <lambdabot> Not in scope: type constructor or class `Nu'
02:46:29 <lambdabot> Perhaps you meant one of these:
02:46:29 <lambdabot> `Num' (imported from Prelude),
02:46:54 <shachaf> foiled again
02:47:03 <shachaf> @let data Nu f = forall x. Nu x (x -> f x)
02:47:03 <lambdabot> Parse failed: Illegal data/newtype declaration
02:47:16 <shachaf> curses, foiled again
02:47:39 <shachaf> hey should i read http://bentnib.org/posts/2013-03-29-productive-coprogramming.html y/n
02:51:24 <copumpkin> yes
02:52:00 <shachaf> good thing i'm already reading it
02:52:25 <shachaf> "2 l8"
02:53:22 <shachaf> tswett: "I'm not sure my syntax doesn't suck." -- that's modal logic hth
02:53:57 <tswett> ~Necessary(~Sucks(MySyntax))?
02:54:21 <shachaf> Right.
02:55:00 <tswett> I wonder if I can express the function (A & B) -o A in my syntax.
02:55:33 <tswett> Seems pretty straightforward: fst (x | _) = x
02:55:53 <tswett> Except that uses case analysis, which, so far, I haven't actually used at all.
02:56:14 <tswett> Which suggests that maybe case analysis just isn't necessary ever.
02:57:50 <tswett> Lessee, that's the same as (((A -o Bottom) + (B -o Bottom)) -o Bottom) -o A... brb installing relief valves in my brain so it doesn't explode
02:58:46 -!- Nisstyre-laptop has joined.
02:59:07 <tswett> Huh, yes, the + appears in a positive position there.
02:59:23 <tswett> No case analysis necessary.
02:59:29 <tswett> weerd
02:59:42 <oerjan> tswett: that's not case analysis, it's picking an element from a tuple...
02:59:49 <tswett> There's only one case.
03:00:02 <tswett> Unicasal case analysis.
03:00:36 <tswett> Except the adjective form of "case" is actually... "capsular"?
03:00:51 <tswett> No, that's the other type of case.
03:01:46 <tswett> And I think that would actually be "capsal".
03:01:54 <tswett> This one would be "casal", yeah.
03:04:56 <oerjan> fst = Left id ?
03:05:20 <tswett> I think that would be (A -o A) + B.
03:05:58 -!- Nisstyre-laptop has changed nick to Nisstyre.
03:06:36 <oerjan> well i'm just thinking of + as Either
03:07:45 <oerjan> so Left is how you construct one
03:07:52 <tswett> Now my syntax is a little bit more explicit. Brackets essentially mean "run this calculation in parallel", and then a period means "this calculation is finished".
03:08:07 <tswett> Here's my new definition of cancel: cancel f = [f (\x -> .)] x
03:09:14 <oerjan> argh whatever
03:09:25 <copumpkin> how is that unique to linear logic? it seems like the usual continuationey shit you can do to "prove" LEM?
03:09:40 <zzo38> I still do not understand it very well.
03:09:41 <tswett> How is what unique to linear logic?
03:16:44 <tswett> Woohoo, implementations of everything: http://pastebin.ca/2413195
03:19:06 <tswett> The dot *usually* occurs inside the corresponding pair of brackets. Like, in the definition of cancel, those brackets are defining x, and the corresponding dot comes after \x.
03:19:27 <tswett> It looks like the only exception is converse, where the brackets are defining g, but the dot comes after \x.
03:43:57 <tswett> I keep reading "converse" wrong in my head. I'm reading "cónverse", the noun, but it's supposed to be "convérse", the verb.
03:44:56 <shachaf> since when is ´ used to indicate emphasis :'(
03:45:02 <shachaf> :´(
03:45:14 <tswett> Since Spanish.
03:45:33 <shachaf> spanish, more like bad use of acute accentish
03:45:43 <Bike> i thought in english you used ` for that.
03:45:56 <tswett> Yeah, I know, right? The Spanish language pretty much consists entirely of bad diacritics.
03:46:26 <tswett> The word for "penguin" is "pingüino". What the hell? Why is the diaeresis over the first vowel instead of the second? And "üi" is a diphthong there!
03:46:47 <tswett> Bike: I thought that ` merely indicated that the vowel is pronounced.
03:46:54 <shachaf> p̈ïn̈g̈üïn̈ö
03:47:09 <tswett> As in "learnèd". The stress definitely goes over the "learn", not the "èd".
03:47:54 <Bike> oh i guess you're right. sucks
03:48:05 <shachaf> help i'm not good at categories proofs :'(
03:48:26 <Bike> i think you mostly just say things commute
03:48:43 <shachaf> i heard bicycles are good for commuting
03:48:51 <Bike> yes
03:49:27 <tswett> I'm not sure this syntax I came up with is equivalent to any existing syntax.
03:50:33 <shachaf> but ok at least i follow the proof of lambek's lemma now
03:50:36 <tswett> Also it's not very good. [(\x -> .) x] is equivalent to "let x = x". But you can't use x afterward, so I guess it's okay.
03:50:47 <shachaf> p. good lemma
03:51:08 <tswett> HTH.
03:51:54 <shachaf> I like how nlab has two different proofs of the lemma, one of which is a dual of the other (but written differently).
03:51:55 <copumpkin> shachaf: have you seen my agda version of that?!
03:52:06 <shachaf> Bike: You forgot to say that things are just duals of other things.
03:52:12 <shachaf> Even less work than commutativity.
03:52:20 <shachaf> nopumpkin
03:52:30 <Bike> i think you'l find that duality is the dual of commutativity.
03:52:46 <shachaf> https://github.com/copumpkin/categories/blob/master/Categories/Functor/Algebras.agda#L97 ?
03:52:47 <copumpkin> https://github.com/copumpkin/categories/blob/2d44e3babb5108ea9b6bd5994c21f4a2278525d1/Categories/Functor/Algebras.agda#L97
03:52:49 <copumpkin> yes
03:53:02 <shachaf> Is the commit version better than the master version?
03:53:06 <copumpkin> no
03:53:14 <copumpkin> just what the search box took me to
03:53:26 <shachaf> copumpkin: have you considered agda + support for commutative diagrams hth
03:53:32 <copumpkin> nope
03:53:50 <shachaf> well i'm patenting the idea hth
03:53:55 <copumpkin> k
03:54:02 <shachaf> ddarius doesn't like commutative diagrams.
03:54:09 <shachaf> Except when he does?
03:54:17 <shachaf> Has he moved to the good coast yet?
03:54:25 <copumpkin> don't think so
03:54:43 <shachaf> I should do his exercise.
03:54:48 <shachaf> He gave me an exercise.
03:55:00 <shachaf> I think I may have seen spoilers while reading nlab...
03:55:29 <shachaf> copumpkin: That proof looks reasonably straightforward, except for all the Agda noise.
03:55:56 <shachaf> Actually that part looks straightforward too.
03:56:20 <shachaf> In fact this whole lemma is completely obvious. Why did they bother giving it a name?
03:56:55 <Bike> [that formalist quote]
03:57:30 <shachaf> copumpkin: So now can you get the dual of the lemma for free by telling Agda to, like, dualize the proof and stuff?
03:59:18 <shachaf> copumpkin: So an initial algebra is also a coalgebra. Is it a special coalgebra in some way?
03:59:36 <shachaf> It's initial in the category of coalgebras that are also isomorphisms, but that's not saying much.
04:09:54 -!- TeruFSX has joined.
04:12:30 <copumpkin> don't think it's particularly special, no
04:12:40 <copumpkin> sorry, trying to do something before I go to sleep, not checking IRC much :)
04:12:52 <copumpkin> I can't get the dual for free right now but it might be possible to define something that lets you
04:12:56 <copumpkin> haven't thought about it much
04:13:13 <copumpkin> I have various kinds of free duals attached to things
04:13:28 <copumpkin> you can get an "opposite functor" for free, and obviously an opposite category
04:14:31 <shachaf> Is Smyth and Plotkin's lemma another name for Lambek's lemma?
04:14:38 <shachaf> Oh, no, it's saying something a bit stronger.
04:17:13 <zzo38> Is there any Haskell library for defining chess variants?
04:20:38 -!- oerjan has quit (Quit: Good night).
04:23:19 <shachaf> copumpkin: I guess it's sort of special in that it gives you an embedding from Mu to Nu, maybe?
04:23:52 <shachaf> In Haskell you can do it with Fix without a Functor constraint. It seems to me that Fix is rather fishy, though.
04:32:33 -!- Bike has quit (Ping timeout: 248 seconds).
04:36:17 -!- Bike_ has joined.
04:50:49 -!- Bike_ has changed nick to Bike.
04:55:39 -!- sprocklem has quit (Remote host closed the connection).
04:59:43 <shachaf> Bike: ok i'm getting annoyed by not knowing things about fixed points
04:59:45 <shachaf> Bike: plz help
04:59:51 <Bike> which things
05:00:02 <shachaf> like why do they exist
05:00:04 <shachaf> in haskell
05:00:36 <Bike> you realize i know, like, negative amounts of haskellmath. i'll just confuse you worse as i try to figure out what hte fuck you're saying.
05:01:02 <shachaf> good
05:01:05 <copumpkin> negative haskellmath!
05:01:09 <copumpkin> is that like virtual species
05:01:12 <copumpkin> hth
05:01:19 <Bike> fuck, probaby
05:01:21 <Bike> l
05:01:27 <shachaf> copumpkin: you should do an agda proof that Mu F is an initial F-algebra
05:01:32 <shachaf> ht
05:01:32 <shachaf> h
05:01:39 <Bike> i like how "virtual species" is a combinatoric thing and also a bikeology thing
05:02:31 <shachaf> copumpkin: i would do it but i'd have to, like, learn agda and stuff
05:02:59 <copumpkin> shachaf: I can't define Mu in Agda directly
05:03:16 <shachaf> Why not?
05:03:42 <copumpkin> oh I guess your form of it might work
05:03:49 <copumpkin> actually no
05:04:14 <shachaf> Why not?
05:04:34 <copumpkin> maybe it does, I dunno
05:04:36 <copumpkin> try it out :P
05:06:28 <shachaf> I don't even know how to type those fancy characters.
05:06:36 <copumpkin> then learn!
05:06:39 <copumpkin> isn't that what you do?
05:07:11 <shachaf> Me? Do I look like a learnin' person to you?
05:08:44 <shachaf> imo copumpkin should come to san francisco to talk about agda and categories at bahaskell
05:09:05 <copumpkin> :)
05:09:51 <shachaf> maybe copumpkin isn't cool enough to come to san francisco yet :'(
05:10:12 <copumpkin> clearly not!
05:10:12 <shachaf> i heard that's the main requirement
05:10:31 <Bike> why do people come into #language and "'«challenge'”» everybody to explain why they should use language
05:11:30 <copumpkin> yo people tell me why I should use esoteric languages
05:11:44 <shachaf> Bike: Wait, is it chord?
05:11:49 <Bike> brainfuck is web-ready and has access to java libraries
05:11:57 <Bike> yes
05:12:21 <shachaf> http://tunes.org/~nef/logs/haskell/13.01.29
05:12:33 <shachaf> have fun with chord
05:12:41 <Bike> oh, fucking great
05:13:12 <Bike> "how does a functional language like Haskell implement a hash table as an array?" omg
05:13:35 <shachaf> It gets way better.
05:13:42 <shachaf> More chord fun after you've finished that one: http://tunes.org/~nef/logs/haskell/13.02.23
05:13:43 <Bike> what the hell
05:13:57 <Bike> what's with this phd crap, what the shit.
05:14:07 <Bike> "tac has always been skeptical of computational complexity" also
05:16:05 <shachaf> Bike: Wait, Zhivago is in ##lisp?
05:16:16 <Bike> yeah that fucker's everywhere
05:16:37 <shachaf> i thought of Zhivago as a ##c person
05:16:42 <Bike> i know right.
05:17:33 <shachaf> Oh, y'all in #lisp have a lot of familiar names from various places.
05:17:46 <shachaf> like zRecursive
05:17:49 <shachaf> and Bike
05:18:00 <shachaf> and Quadrescence
05:18:05 <Bike> Whoa Man
05:18:23 <Fiora> yay that means I know a famous freenode person?
05:18:33 <Bike> i am the famousest.
05:18:38 <shachaf> Fiora: Who?
05:18:42 <Bike> at least three distinct people have heard of me
05:19:02 <Fiora> bike, clearly
05:19:08 <shachaf> Oh, Bike's famous?
05:19:20 <shachaf> hi Bike
05:19:22 <Fiora> sorry, I was responding to what you said
05:19:23 <Bike> there are rumors that a fourth person has heard of me.
05:19:25 <Bike> hi shachaf
05:19:29 <shachaf> Oh, I said familiar.
05:19:37 <shachaf> As in I know of them from other places.
05:19:40 <shachaf> As in #esoteric.
05:21:26 <Bike> also ##bike
05:21:38 <Bike> not bike approved tho
05:21:47 <shachaf> 22:21 [@ChanServ] [ shachaf]
05:21:53 <Bike> i meant in the past
05:21:56 <Bike> the ##bike past.
05:42:03 -!- carado has joined.
06:10:07 -!- carado has quit (Ping timeout: 264 seconds).
06:16:31 -!- Bike has quit (Ping timeout: 276 seconds).
06:17:45 -!- Bike has joined.
06:19:29 -!- FreeFull has quit.
06:31:44 -!- Nisstyre has quit (Read error: Connection reset by peer).
06:32:22 -!- mnoqy has joined.
06:50:36 -!- Bike has quit (Ping timeout: 252 seconds).
06:51:56 -!- Bike has joined.
06:56:49 -!- Bike has quit (Ping timeout: 276 seconds).
07:02:55 -!- Taneb has quit (Ping timeout: 264 seconds).
07:05:32 -!- Taneb has joined.
07:27:31 -!- epicmonkey has joined.
07:50:20 <zzo38> Here is a chess problem: White pawns on f2 and e7, king on e6. Black pawn on g5 and king on e8. White to play and win.
07:50:47 <shachaf> Can you draw it for me? I don't know chess notations.
07:54:47 <Deewiant> 4k3/4P3/4K3/6p1/8/8/5P2/8 w - - 0 1 is the FEN, you can paste it into any decent program
07:56:19 -!- epicmonkey has quit (Read error: Operation timed out).
08:12:40 <Taneb> Okay, I have finally found a replacement for Google Reader
08:13:53 -!- nortti has quit (Ping timeout: 240 seconds).
08:24:43 -!- MindlessDrone has joined.
08:40:37 <halfb4rd> taneb: which one?
08:40:47 <Taneb> bazquux
08:41:54 <Taneb> www.bazqux.com
08:42:00 <Taneb> It's not free, but I like the interface
08:44:22 <shachaf> free as in free f-algebra
08:48:03 <Gracenotes> It's written in Haskell and Ur/Web, I believe
08:48:26 <Gracenotes> because RSS feeds are surprisingly computationally expensive, whatwithallthe parsing.
08:48:51 <Gracenotes> at least such that a static compiled language would have some advantage, probably, or something.
08:48:56 <shachaf> zzo38: What's the dual of CodensityAsk?
08:49:02 <shachaf> (More commonly known as Free.)
08:49:58 <zzo38> shachaf: I don't know if there is clearly the dual.....
08:49:58 <shachaf> Is a cofree comonad a cofree f-coalgebra?
08:50:13 * ion drinks some ffee
08:50:20 <shachaf> I think CofreeComonad f a = exists x. (x, x -> (a, f x))
08:51:49 <shachaf> So maybe Cofree (Coalgebra F) = CofreeComonad F?
08:52:17 <shachaf> Oh.
08:52:26 <shachaf> Maybe CofreeComonad f a = exists x. (a, x, x -> f x)
08:52:29 <shachaf> That makes more sense!
08:52:51 <shachaf> Er, wait.
08:52:55 <shachaf> No, it makes no sense.
08:53:28 <shachaf> So how do you express CofreeComonad without the ugly functor composition?
08:54:06 <Gracenotes> it is dangerously difficult to distinguish between sense and nonsense in this area
08:54:30 <zzo38> Actually there are two things known as Free, and CodensityAsk is different anyways because it does not take a class as its parameter.
08:54:47 <zzo38> But all three of these things are related.
08:54:52 <shachaf> I'm talking about newtype Free f a = Free { runFree :: forall r. f r -> (a -> r) -> r }
08:55:41 <zzo38> Yes, that one is basically the same as what I made up, although other things have been called Free, too.
08:55:47 <Taneb> That's just data Free f a = Pure a | Free (f (Free f a)) in CPS, right?
08:56:10 <zzo38> Taneb: No.
08:56:11 <Gracenotes> you can get a lot of things for free
08:56:11 <shachaf> Taneb: No, that's be newtype FreeMonad = FreeMonad { runFreeMonad :: (a -> r) -> (f r -> r) -> r }
08:56:13 <Taneb> At least when f is a Functor
08:56:26 <Taneb> Aaah
08:56:32 <shachaf> Taneb: Free (Algebra F) = FreeMonad, where Algebra f a = f a -> a
08:56:41 <shachaf> Which corresponds to the notion that a free monad is a free f-algebra.
08:57:07 <zzo38> (Although in mine, I also had that if f is a comonad, then it makes a MonadPlus.)
08:58:32 <zzo38> That way even gives you a Maybe monad, Either monad, and "disjunctive state monad".
08:58:45 <shachaf> The cofree comonad on an endofunctor H on C is given by DA =df νX.A× HX
08:58:47 <shachaf> (i.e., the carrier of the final A × H(−)-coalgebra, which is the cofree H-coalgebra
08:58:50 <shachaf> on A).
09:00:42 <ion> final indeed
09:01:03 <shachaf> So how do you express Cofree?
09:07:27 -!- epicmonkey has joined.
09:09:07 <zzo38> ("Disjunctive state monad" = CodensityAsk (Store s). It uses <|> to compose state, and this is achieved for free.)
09:18:07 -!- conehead has quit (Quit: Computer has gone to sleep.).
09:23:27 -!- olsner has quit (Ping timeout: 246 seconds).
09:26:37 -!- Halite has quit (Read error: Connection reset by peer).
09:29:51 -!- atriq has joined.
09:30:27 -!- Taneb has quit (Disconnected by services).
09:30:31 -!- atriq has changed nick to Taneb.
09:35:10 -!- augur has quit (Remote host closed the connection).
09:39:39 -!- augur has joined.
09:45:06 -!- augur has quit (Read error: Connection reset by peer).
09:45:18 -!- augur has joined.
09:48:57 -!- augur has quit (Remote host closed the connection).
09:50:44 -!- augur has joined.
09:52:57 -!- augur has quit (Remote host closed the connection).
09:54:12 -!- augur has joined.
09:54:51 -!- carado has joined.
09:55:13 -!- augur has quit (Read error: Connection reset by peer).
09:57:04 -!- augur has joined.
10:03:25 -!- augur has quit (Ping timeout: 256 seconds).
10:14:32 -!- nooodl_ has joined.
10:18:55 -!- carado has quit (Ping timeout: 260 seconds).
10:23:41 -!- olsner has joined.
10:28:44 -!- olsner has quit (Ping timeout: 260 seconds).
10:34:53 -!- augur has joined.
10:35:22 <shachaf> zzo38: Cofree f a = exists x. (x, x -> a, f x)
10:35:49 <shachaf> ( Saizan++ )
10:43:11 <Gracenotes> cofree of what again? f-algebra?
10:44:11 <shachaf> Well, a Cofree F-Coalgebra is a cofree comonad.
10:45:40 -!- olsner has joined.
10:50:36 -!- Taneb has quit (Quit: Leaving).
10:55:27 <fizzie> https://dl.dropboxusercontent.com/u/113389132/Misc/20130701-ieeepub.png oh, so that's what it looks like.
10:58:09 <mnoqy> the eic looks very happy about receiving the paper
11:00:50 <zzo38> Do you think non-continuous chess variants don't have a number of dimensions?
11:01:40 <fizzie> mnoqy: It's what gives their life meaning! I think.
11:05:56 <zzo38> http://www.chessvariants.org/index/displaycomment.php?commentid=29981 Can you play the Fukumoto variant?
11:15:15 -!- Phantom_Hoover has joined.
11:20:33 <zzo38> "The King's security is more important than the King himself." -- The Hitchhiker's Guide to Chess
11:20:51 <shachaf> zzo38: What do you think of Cofree?
11:21:05 <zzo38> shachaf: I don't know.
11:21:19 <shachaf> Cofree (Coalgebra F) = CofreeComonad F
11:21:30 <shachaf> (And of course Free (Algebra F) = FreeMonad F)
11:21:57 <zzo38> Using your definition, let's see. Yes, that seems correct to me.
11:33:30 -!- zzo38 has quit (Remote host closed the connection).
11:57:56 -!- TeruFSX2 has joined.
12:01:10 -!- TeruFSX has quit (Ping timeout: 268 seconds).
12:07:47 -!- sacje has quit (Quit: sacje).
12:40:44 -!- itsy has joined.
12:43:13 -!- Koen_ has joined.
12:44:12 -!- Koen_ has quit (Read error: Connection reset by peer).
12:44:15 -!- Koen__ has joined.
12:44:45 -!- AnotherTest has joined.
12:44:51 <AnotherTest> Hello
12:45:17 <itsy> Hello AnotherTest :-)
12:47:36 <AnotherTest> what have I done http://stackoverflow.com/questions/17378961/elegant-way-to-implement-extensible-factories-in-c/17404774#17404774
12:50:26 <itsy> This might be fun - http://tnmoc.org/summer-bytes (Summer Bytes Festival in UK)
13:16:37 -!- sacje has joined.
13:23:45 -!- halfb4rd has quit (Quit: halfb4rd).
13:31:38 <elliott> 20:33:22: <ion> wtf http://www.wekkars.com/
13:31:39 <elliott> help.
13:33:01 <fizzie> Signed esolangs.org up for it already, did you?
13:33:45 <elliott> https://twitter.com/wekkars i just...
13:33:48 <elliott> is this real
13:36:12 -!- Gracenotes_ has quit (Remote host closed the connection).
←2013-06-30 2013-07-01 2013-07-02→ ↑2013 ↑all