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