00:01:23 maybe all prehistoric C implementations had sizeof(int) == sizeof(void*) 00:01:42 or used register calling convention and therefore were more flexible 00:04:24 -!- Chef has joined. 00:05:48 Koen_: it's not quite that bad http://c-faq.com/ansi/argpromos.html 00:07:20 also this also applies to printf arguments http://c-faq.com/varargs/promos.html 00:07:23 -!- Slereah has quit (Remote host closed the connection). 00:07:24 It is arguably much safer to avoid ``narrow'' (char, short int, and float) function arguments and return types altogether. 00:07:50 so basically just use ints 00:08:04 (and doubles but who needs them) 00:08:07 -!- Slereah has joined. 00:08:32 -!- Slereah has quit (Client Quit). 00:10:46 hmmm 00:11:09 now I want to try writing prototypes for printf here and there 00:13:04 -!- yorick has quit (Remote host closed the connection). 00:21:33 -!- Tod-Autojoined2 has changed nick to TodPunk. 00:24:12 class (Eq s, SetType__ s) => SetType s where { type SetOf s :: *; ... }; constructSetType :: forall a c. (forall b. SetType b => SetOf b -> (b -> c) -> a) -> [c] -> a; ... Do you expect things like this is OK? 00:32:30 -!- nooodl_ has joined. 00:35:33 i think today's picture in wikipedia needs a nsfl warning. 00:37:12 -!- nooodl has quit (Ping timeout: 272 seconds). 00:37:29 smallpox is kind of not safe for life, yeah. 00:38:28 hey smallpox virus is life too 00:38:32 (lets argue about that now) 00:38:33 also, yikes 00:38:44 i am old enough to have been vaccinated, i think. 00:39:22 vaccines are pretty cool 00:39:55 wow, i just noticed that photo was taken barely two years after the war 00:40:05 i should get more of them 00:40:10 I don't *think* I've been vaccinated for smallpox. But when I was young my dad was in the Army, and so we were overseas, so... maybe? 00:40:50 I think I'm old enough that I wasn't vaccinated for chicken pox at least? ^^; 00:41:12 Yeah, I wasn't vaccinated for chicken pox either. 00:41:47 I just got chicken pox. Does that count? 00:42:02 i got it and my parents marketed me to their social circle as spreading it. Only 90s Kidz Remember 00:43:06 i've had chicken pox. when i was 18. 00:43:26 I think I must have been like 10 00:43:35 i think i have scars in my face that are from it. 00:44:15 I was like 5? 00:44:35 also i have a scar on my shoulder which is from some vaccine, perhaps the smallpox one? 00:46:49 Closest to a smallpox vaccine I *know* I've been is that I've been near someone with cowpox. 00:50:34 is $ in haskell just a prefix-notation parenthese for function application? 00:50:44 parenthesis 00:51:19 Actually $ in Haskell is the infix form of id, but specialized for function application 00:51:45 it just has the lowest associativity because i dunno screw parens. 01:00:01 -!- Phantom_Hoover has quit (Ping timeout: 246 seconds). 01:00:37 -!- Sgeo has joined. 01:03:48 okay thanks 01:03:53 -!- Koen_ has quit (Quit: The struct held his beloved integer in his strong, protecting arms, his eyes like sapphire orbs staring into her own. "W-will you... Will you union me?"). 01:13:20 -!- Uguubee111118 has quit (Quit: Uguubee111118). 01:15:37 -!- Phantom_Hoover has joined. 01:16:39 -!- Uguubee111118 has joined. 01:21:54 -!- myndzi has changed nick to myndzi`. 01:22:26 -!- myndzi` has changed nick to myndzi. 01:23:09 -!- Phantom_Hoover has quit (Ping timeout: 272 seconds). 01:27:02 -!- Phantom_Hoover has joined. 01:34:24 http://sprunge.us/jiGA 01:53:51 Is this Haskell program OK? 02:07:44 isthishaskellprogramok.com 02:08:03 zzo38: do you not like layout syntax? 02:08:15 YES (humorous subtitle) 02:08:38 howfuckedismyhaskellprogram.com 02:08:55 kmc: see foldr.com 02:09:22 that really should say "=ω" not "=∞" don't you think 02:09:28 * kmc fixes it using Element Inspector 02:09:48 kmc: I personally don't like layout syntax (and a few other people also don't like). 02:10:11 kmc: does your Element Inspector have a save button 02:10:25 imo add that feature 02:10:27 no 02:10:29 zzo38: why not? 02:10:36 the Firefox OS dev tools do, though 02:10:48 (which is just the Firefox element inspector thing) 02:10:59 «onclick="f(this); return false"» 02:11:04 now what's this then 02:11:05 kmc: I don't really know how to explain, but you can look up some reasons why some people don't like it, at least. 02:11:09 f(this) indeed 02:11:44 When I ask about this Haskell program, I mean about its use for the purpose I intended to use it for. 02:11:51 g++ -Weffc++ 02:12:20 what is the purpose you intended to use it for 02:12:31 Bike: asking 02:14:07 Bike: Something like a constructor Graph :: forall x y. SetType x => SetOf x -> (x -> y) -> (x -> x -> Bool) -> Graph y; which isn't really a correct definition of a graph, but hopefully can explain clearly enough the use I intended? 02:14:36 i didn't read it. just thought maybe that would help kmcists. 02:14:50 Would it? 02:15:18 Do you understand what I mean now, at least? 02:15:18 is x -> x -> Bool the "this is an edge" checker? what's y for? 02:15:31 Bike: The y is in case the nodes have labels attached. 02:15:49 (If they don't then y would just be ()) 02:16:14 i don't understand why a graph isn't just a set of vertices and a set of edges 02:16:27 data Graph e v = Graph (e -> v) (e -> v) 02:16:54 Sure it could 02:17:23 time to understand shachaf's definition: approximately 40 seconds 02:17:27 But, what I mean is if you want to make up such a "unique set" which is only this useful 02:17:32 Graph A = (x y : A) -> Set 02:17:44 Bike: I can understand more easily though, in a few seconds 02:17:53 copumpkin: What is that, then? 02:17:55 did you just call me stupid 02:17:58 Yours I don't know 02:18:15 Bike: No, I just meant that I realized this specific purpose faster at this specific time. 02:18:21 Bike: Well, mine is a different sort of graph, with multiple edges and loops and so on. 02:18:40 i saw an article in a bio journal about hypergraphs the other day. that was odd 02:19:01 did you know it's just a functor from the category •⇉• to Set 02:19:04 zzo38: it's a generalized relation, covering all sorts of odd graphs 02:19:05 copumpkin: Your definition I do not understand. Do you explain it? 02:19:10 and the natural transformations are graph homomorphisms 02:19:12 it's dependent 02:19:16 I don't know the notation. 02:19:23 Graph A = A -> A -> Set 02:19:26 that's equivalent 02:19:31 why, another concept is just a functor? wow. wow. everything is explained. everything is clear now 02:19:35 mine is not useful 02:19:42 well, it is, but not for computation 02:19:52 is it useful for hugz 02:19:54 copumpkin: But what is "Set" here then? I do not understand this dependent types very well. 02:19:55 i like hugz 02:20:03 zzo38: Set is like * in Haskell (I assume) 02:20:08 yeah 02:20:17 so for every pair of values of that type 02:20:24 it produces another type 02:20:31 which may be empty (in which case there's no edge) 02:20:38 or not, in which case there is 02:20:53 you could have arbitrary values living in the resulting type 02:21:01 so it might have more than one edge 02:21:21 you can define a simple type on top of that that takes the transitive closure, or reflexive transitive closure 02:21:40 the latter also being "the free category of a graph" 02:22:41 Bike: should i write that as ((Bool,e) -> v) or as (e -> Bool -> v) 02:22:53 Bike: or as (e -> (v,v)) "that would be too simple" 02:23:05 iunno, the original was cute. 02:23:54 i'm not used to having edges as their own thing. maybe that's it. 02:24:05 copumpkin: OK, but I do not quite understand how you would have values of a type produce another type like that, it doesn't sense to me quite a lot though. 02:24:17 that's why it's dependent 02:24:22 imo ur cute 02:24:32 "clearly i need to deal with infinite graphs more often" 02:24:34 asl 02:24:50 are nonlinear dynamications functors 02:24:51 the other day a bus driver made the asl sign for "no" and i understood 02:24:54 i was pleased 02:25:02 am i a functor 02:25:08 i am a banana 02:25:17 i am barbed wire 02:25:39 I tried reading about depending type but I don't quite understand it. I have read a Haskell library that says it defines a "dependent sum type" and I can understand that library at least, but not what it has anything to do with dependent types. Actually when I tried to explain when I was asking how to make this program I made I was told about dependent types too, which I don't know. 02:25:58 copumpkin: What is it called, the things that my program is defining, though? 02:26:09 not sure! 02:26:29 dependent sum types can be quite confusing 02:26:33 but are awesome 02:26:51 copumpkin: sum types r confusing, other types less so 02:27:14 copumpkin: Well, I can understand the Haskell library which says dependent sum types, even though I am not understanding the dependent sum types itself. 02:28:48 What I tried to define is that a value contained in some datatype is kind of like another type and a set of values in that type, where the only thing done on the values is check if it is equal to another one, and pass to a function that expects it. 02:29:08 It isn't really making up a new type each time, but it fakes it. 02:29:29 zzo38: a dependent sum type is like a pair in haskell, where the type of the second half can refer to the value of the first half 02:29:36 it's a strange concept if you're not used to it 02:29:52 copumpkin: why aren't there things that map between natural transformations 02:29:56 I was also refered to reflection, which also tries to fake to make up a type but uses unsafeCoerce. My program does not involve unsafeCoerce. 02:30:08 copumpkin: Well, I know that, because I have read that program, and that is what it is. 02:30:11 shachaf: they exist, but they're unnatural and we don't talk about them 02:30:18 why are they unnatural 02:30:22 a functor on the category of small natural transformations 02:30:27 shachaf: too natural is unnatural 02:30:30 Such things are done in Haskell easily enough anyways, using forall, type parameters, and other stuff like that. 02:30:51 Bike: is that a sequence of words that makes sense or just a sequence of words 02:30:59 well consider the speaker 02:31:06 the speaker is a bicycle 02:31:07 an endofunctor. endomonoid. coexofunctor 02:31:09 exactly 02:31:17 endonote: don't listen to Bike 02:31:23 yeah 02:31:58 imo the worst bike 02:33:02 imo i've ridden some p. bad bikes recently 02:33:30 And using GADTs. 02:34:15 copumpkin: Do you think my program does correctly what I intended though, at least? 02:36:36 :/ #chicken is too quiet 02:36:57 zzo38: not sure! what did you intend? 02:37:15 he already answered that a while up. 02:37:21 kmc: I wonder if you would like explicit-renaming/implicit-renaming macros 02:37:47 There's no DSL, you write a function that receives a few functions that aid in hygiene 02:37:51 what are your thoughts on yaoi 02:37:53 So you're writing in pure Scheme 02:38:08 hmm 02:38:19 Bike: I looked and didn't understand 02:38:26 well, i didn't either 02:38:34 low standard though 02:38:38 copumpkin: I can try to explain, perhaps, as, the function makes up a new set of its own type (actually Int, although it pretends it is a new type), and where values of this type can only be compared for equality. 02:39:54 Is this explanation good enough? 02:40:11 hmm, a little better 02:40:14 what's your goal with it, though? 02:41:04 My example with the Graph constructor is one example (which doesn't actually define a graph though, and isn't really quite intended to anyways), but it is example of how it might be used, I mean. 02:41:25 it's odd how a superclass refers to its subclass in methods 02:42:45 Yes, I suppose such thing is odd, but it does work. 02:42:56 I don't doubt it, just trying to make sense of it 02:43:15 (The SetType__ class is private, so that you can never use it) 02:43:48 yeah 02:43:56 -!- Phantom_Hoover has quit (Quit: Leaving). 02:45:22 The only type that has an instance is also private, meaning that values of such a type are only used in a polymorphic type signature 02:45:36 yeah 02:45:45 so you force people to only use the class interface 02:45:56 Yes. 02:47:05 Although the point is also that you cannot check for type equality either, as if every call to emptySetOf and so on are of a different type which nobody knows. 02:47:20 yup 02:48:45 I think it makes sense, although it might pay to figure out how to make your exposed Set interface take the "contents" parameter directly 02:48:57 oh, perhaps not 02:49:02 wtf 02:49:08 Is it just me or is this paper backwards 02:49:13 http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=E9CB45AD79DE7268512C8A60D0C1A0BB?doi=10.1.1.53.5184&rep=rep1&type=pdf 02:49:36 just you, looks fine to me 02:49:53 oh wait, I was standing on my head 02:49:55 yeah, it's backwards 02:50:46 Just print it in this order and it'll be fine. 02:50:50 more convenient imo 02:51:25 Maybe you can configure the printer driver to work with it 02:51:31 Is it just me, or is it saying that er macros are limited? 02:51:37 :/ 02:52:53 copumpkin: I think this program I made up in there not quite complete, since a few operations are missing, isn't it? 02:53:20 hich things can be constructed using only the exported interfaces and which cannot be? 02:53:47 Sgeo: plz to link to the actual citeseer page instead of a pdf. 02:55:13 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5184 02:55:29 Thank you. 02:55:51 -!- cybercortex has joined. 02:55:55 -!- conehead has quit (Quit: Computer has gone to sleep.). 02:55:57 Sgeo: https link plz 02:56:08 (it won't help but i might as well ask) 02:56:40 I dunno. I still don't get hygenic macros at all. Maybe I should ask around #scheme for programs that really need them. 02:58:12 I want to recommend trying to understand syntax-case, but syntax-case comes with unneeded extra sugar called syntax-case that might hinder understanding 02:58:28 Well I think i get the basic idea of syntax case. 02:59:04 -!- cybercortex2 has joined. 03:00:15 -!- cybercortex has quit (Ping timeout: 256 seconds). 03:01:40 Just to clarify: syntax-case and not syntax-rules? syntax-case is the more complicated one that allows breaking hygiene 03:02:09 Yeah, you specify what symbols are supposed to be literal and which ones aren't, right. 03:02:18 -!- cybercortex has joined. 03:03:39 -!- cybercortex2 has quit (Ping timeout: 256 seconds). 03:03:45 syntax-rules allows that too, but syntax-case is more flexible than that. And easily allows arbitrary Scheme computations 03:04:02 My other (unrelated) question was how to make pattern matching with rosetrees, in SQL or in a C program that can be export functions to use with SQL. 03:04:16 Do you know how to make up such pattern matching? 03:04:27 ok, but "it allows what the other thing is based on" is kind of... i don't really care, you know what i mean? 03:06:03 -!- cybercortex2 has joined. 03:06:04 What I can think of is there will be the kind of patterns: A(P) A(* A(P) *) A(P *) ? where A is atom and P is a list of zero or more patterns. 03:06:30 If this is kind of patterns I would need, how would it be doing, so that you can match and replacement? 03:07:06 -!- cybercortex has quit (Ping timeout: 252 seconds). 03:07:45 -!- oerjan has quit (Quit: Nyit). 03:08:02 Bike: just trying to ascertain which one it is you know >.> 03:08:19 i don't really know either one that well, if that isn't obvious. 03:14:27 -!- cybercortex has joined. 03:14:40 -!- cybercortex has quit (Client Quit). 03:14:48 -!- cybercortex2 has quit (Ping timeout: 252 seconds). 03:17:03 kmc: Do you think persistent data structures are generally not very effective without a GC? 03:21:30 I don't have the experience to say, really 03:21:33 it seems like they wouldn't be 03:22:57 Hmm, are there obvious ways to make a GC more efficient if you don't care about finding cycles? 03:23:12 refcounting? 03:23:25 is only sometimes more efficient 03:23:52 i can come up with a few reasons that it would kill performance for a persistent concurrent hash trie or the like 03:23:55 but i dunno 03:23:59 haven't tried it 03:24:12 i don't doubt it. it's just the obvious for cyclefucking gc :p 03:24:21 * kmc made an accidental pun there 03:24:26 Ha! Ha! 03:24:35 Bike: you would be interested in cyclefucking wouldn't you 03:24:49 he's on a roll today folks 03:24:54 my gc can find cycles but not bicycles 03:24:56 LIKE A BICYCLE 03:24:57 much like me! hyuk hyuk. my brakes are out, i'm going to die 03:25:09 Do you know anything about pattern matching rose trees in general? 03:25:16 zzo38: in SQL? 03:25:52 i don't know what a rose tree is, other than that it is probably depicted in the hit japanese cartoon show, Shōjo Kakumei Utena 03:25:55 Maybe zzo38 means Proof General. 03:26:10 i was riding a bicycle without working brakes recently 03:26:15 imo not great 03:26:17 taht's dangerous 03:26:53 t̂'s dangerous 03:27:28 "Apparently many of you missed it. I took a screenshot of all unauthenticated VNC servers on IPv4. It took 16 minutes. http://results.survey.tx.ai" 03:27:29 kmc: Yes, in SQL, although it could be in C and then export the function to SQL. (It is operating on SQL data structures however.) 03:27:43 (Rose tree is what in Haskell would be (Cofree []), although this program is C) 03:27:54 kmc: it's cool how we're all doomed 03:28:29 did you see conal's talk on parallel scans 03:28:33 the links are broken :( 03:33:32 shachaf: you had a halting problem? 03:33:42 [even my humor is stolen] 03:33:45 kmc: that's terrifying 03:34:08 it was just taken down? 03:34:27 looks up to me 03:34:28 i see screenshots on http://results.survey.tx.ai/216.html 03:34:33 Oh, no, there it goes. 03:34:43 404 not found 03:34:59 no porn yet 03:35:22 http://a0cb98c247b3db5ffaba-2460f3ea0996e8d440cbab5ff57046e7.r23.cf2.rackcdn.com/216.230.224.203_5903.jpg 03:36:15 http://a0cb98c247b3db5ffaba-2460f3ea0996e8d440cbab5ff57046e7.r23.cf2.rackcdn.com/216.200.140.167_5900.jpg 03:36:31 THat icon looks like ActiveTcl... I assume it's actually ActivePerl 03:39:37 kmc: nice. 03:43:51 -!- nooodl_ has quit (Ping timeout: 260 seconds). 03:51:23 * Sgeo mutters about dead scheme communities 03:54:40 (is-not (that-which-can (eternal lie)) dead) 04:07:06 "One of my favorite things about Chicken Scheme is ir-macro-transformer. I find it to be the most intuitive hygienic macro system yet (using it isn't any more complicated than the traditional unhygienic define-macro)." 04:07:22 Of course, that simplicity may come at a cost 04:10:09 ir? 04:10:17 implicit renaming 04:10:47 Can Scheme make "law of excluded middle" continuations? You can define that and ordinary continuations in terms of each other (at least in Haskell you can). 04:10:50 Symbols that are returned are automatically renamed, unless you call inject on them (inject being a function supplied to the transformer along with the form) 04:11:36 lemCC = callCC (return . Right . (<=< return . Left)); callCC x = lemCC >>= either return x; 04:13:19 Cont monad continuations are almost delimited continuations. You can build delimited continuations in standard Scheme with call/cc and a bit of mutable state, although it's horrible. Some Schemes and Schemelike systems also provide delimited continuations natively 04:13:49 That doesn't mean I understand your code, or what a "law of excluded middle" continuation is, just that I'm pretty sure the answer is 'yes' 04:24:04 zzo38: Sure, why not? 04:24:45 Sgeo: It means a thing that gives you a continuation when you call it. Then when you call the continuation with a value, it gives you that value. 04:30:45 I think if I want the name of a bare input symbol to an IR-based macro... I can't get it 04:31:05 I can compare against known symbols, but I don't think I can just easily convert to a string 04:31:36 Because all the symbols come in 'renamed' 04:32:13 -!- trout has changed nick to variable. 04:36:38 -!- contrapumpkin has joined. 04:36:39 -!- copumpkin has quit (Read error: Connection reset by peer). 04:48:21 -!- Chef has quit (Quit: Rooms • iPhone IRC Client • http://www.roomsapp.mobi). 04:49:13 http://paste.call-cc.org/paste?id=fd5f78e7052159d4df1dfed5cbec51d8e7017598 04:51:21 -!- ^v has quit (Quit: Ping timeout: 1337 seconds). 05:26:37 -!- impomatic has quit (Ping timeout: 272 seconds). 05:27:52 -!- shikhin_ has joined. 05:28:39 -!- Taneb has joined. 05:28:56 -!- carado has joined. 05:30:36 -!- shikhin__ has quit (Ping timeout: 245 seconds). 05:31:27 :( 05:31:48 -!- impomatic has quit (Ping timeout: 240 seconds). 05:32:19 -!- shikhin_ has quit (Ping timeout: 246 seconds). 05:37:24 Taneb: ? 05:38:15 I can't get 4oD to work 05:38:22 So I can't watch Agents of SHIELD 05:42:58 -!- asie has joined. 05:46:05 -!- shikhin_ has joined. 05:56:43 -!- impomatic has quit (Ping timeout: 248 seconds). 05:56:44 Hmm... this thing about Chicken just recommended autoconf and automake 05:56:51 Maybe I should just run far, far away 05:57:10 Will autoconf and automake help me watch Agents of SHIELD 05:58:51 -!- shikhin__ has joined. 05:59:44 It's theoretically possible for at least some hypothetical problems preventing 4oD access 06:01:15 -!- shikhin_ has quit (Ping timeout: 245 seconds). 06:08:33 what is agents of shield. is it an anime 06:09:05 It's about some agents of shield 06:09:15 It's made by disney 06:10:49 why the fuck is everyone talking about anime now 06:13:24 anime is great 06:13:33 especially the good ones 06:13:47 Also I'm on a team for a CTF competition Detica is running today 06:14:48 -!- Bike has quit (Quit: Reconnecting). 06:15:02 -!- Bike has joined. 06:21:27 -!- shikhin__ has quit (Ping timeout: 272 seconds). 06:23:25 -!- shikhin__ has joined. 06:27:32 https://twitter.com/grammarware/status/393871325338411009/photo/1 this is dumb but still great, somehow. 06:28:35 -!- shikhin__ has quit (Ping timeout: 259 seconds). 06:31:19 hah 06:34:26 Fiora: This ECDSA paper introduces ten acronyms on the first page. 06:36:59 -!- FreeFull has joined. 06:41:26 -!- shikhin has joined. 06:57:56 -!- impomatic has quit (Ping timeout: 245 seconds). 07:00:46 http://www-cs-faculty.stanford.edu/~knuth/programs/tpk.i 07:02:43 HERE I USE A SLICK TRICK 07:03:31 DON'T STOP READING YET 07:03:58 PLEASE NOTIFY THE AUTHOR IF YOU'VE BEEN ABLE TO UNDERSTAND ALL OF THIS; BUT PLEASE DON'T SEND EMAIL 07:34:36 -!- mnoqy has quit (Quit: hello). 07:38:17 -!- Taneb has quit (Quit: Leaving). 07:38:43 -!- zzo38 has quit (Remote host closed the connection). 07:39:00 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...). 07:46:11 -!- asie has joined. 07:46:30 -!- asie has quit (Excess Flood). 07:52:48 -!- shikhin has quit (Ping timeout: 240 seconds). 07:57:16 -!- shikhin has joined. 08:01:30 -!- Slereah has joined. 08:03:22 -!- shikhin_ has joined. 08:04:28 The SRFI process specifies HTML 3.2 08:05:19 -!- shikhin has quit (Ping timeout: 272 seconds). 08:12:55 -!- AnotherTest has joined. 08:18:22 -!- mnoqy has joined. 08:24:00 -!- Sprocklem has quit (Ping timeout: 252 seconds). 08:26:10 -!- shikhin__ has joined. 08:27:45 -!- shikhin_ has quit (Ping timeout: 272 seconds). 08:39:22 -!- Uguubee111118 has quit (Quit: Uguubee111118). 08:41:01 -!- MindlessDrone has joined. 08:41:55 -!- Uguubee111118 has joined. 08:42:41 -!- yorick has joined. 08:44:55 -!- epicmonkey has joined. 09:09:20 -!- shikhin_ has joined. 09:12:27 -!- shikhin__ has quit (Ping timeout: 272 seconds). 09:40:20 -!- asie has joined. 09:55:57 @tell Koen_ You can pass other types without a prototype. You can't pass a char, a short or a float because the default arugment promotions convert those to an int, an int and a double, respectively, in absence of a prototype. 09:55:57 Consider it noted. 09:56:45 @tell Koen_ If it's any other type, you can receive it as-is in a function without a prototype. (Of course you need to make sure it is exactly the type the function expects, because no implicit conversions are done.) 09:56:45 Consider it noted. 09:57:17 @tell Koen_ Oh, I didn't notice oerjan's links. Sowwy. 09:57:17 Consider it noted. 09:57:32 The dangers of incomplete logreading. 10:00:47 So I am thinking of going back on http://esolangs.org/wiki/Limp 10:00:52 But I am having a dilemma 10:01:08 I want all (functional) operators to be compatible in a pinch 10:01:29 Mostly by giving them an equivalent lambda version 10:01:58 But if possible I also want to make an equivalence between the numbers and lists 10:02:11 Like 0 being the empty list or NIL, I dunno 10:02:33 But in that case, that equivalent must be the same as the one with the lambda expressions 10:02:53 With 0 = ^x^y.y, and so on 10:03:07 And I'm not sure which construction to pick 10:03:45 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...). 10:18:48 -!- impomatic has quit (Ping timeout: 240 seconds). 10:19:46 -!- asie has joined. 10:48:38 -!- mnoqy has quit (Quit: hello). 10:49:08 -!- impomatic has quit (Ping timeout: 268 seconds). 10:52:50 -!- FreeFull has quit (Read error: Connection reset by peer). 10:53:41 -!- FreeFull has joined. 10:59:46 -!- impomatic has quit (Read error: Operation timed out). 11:03:47 -!- Phantom_Hoover has joined. 11:05:10 -!- AnotherTest has quit (Ping timeout: 268 seconds). 11:21:21 -!- nooodl_ has joined. 11:23:19 -!- nooodl__ has joined. 11:26:43 -!- nooodl_ has quit (Ping timeout: 272 seconds). 11:32:21 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...). 11:45:59 -!- Bainos has joined. 11:49:28 -!- asie has joined. 11:54:04 -!- Phantom__Hoover has joined. 11:55:07 -!- Phantom_Hoover has quit (Ping timeout: 272 seconds). 12:00:58 -!- Chef has joined. 12:03:44 -!- Chef has quit (Client Quit). 12:15:38 http://www.reddit.com/r/math/comments/1p83at/turing_machine_vs_human_mind/ 12:15:47 sigh i'm not really sure how to respond to this 12:16:21 downvote and ignore? 12:16:59 that would be the coward's way out, yes 12:22:26 -!- Bainos has left. 12:25:31 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...). 12:32:45 -!- mnoqy has joined. 12:43:26 -!- Uguubee111118 has quit (Ping timeout: 265 seconds). 12:47:52 -!- asie has joined. 13:02:41 which irc clients do people usually use with mac 13:03:05 I used XChat-aqua and ircII 13:06:50 -!- nooodl__ has changed nick to nooodl. 13:14:31 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...). 13:16:58 -!- oerjan has joined. 13:18:59 -!- Phantom__Hoover has quit (Ping timeout: 268 seconds). 13:19:58 -!- Phantom__Hoover has joined. 13:27:08 -!- MindlessDrone has quit (Quit: MindlessDrone). 13:40:50 -!- MindlessDrone has joined. 13:42:07 -!- Uguubee111118 has joined. 13:49:35 -!- epicmonkey has quit (Ping timeout: 260 seconds). 13:55:35 -!- Koen_ has joined. 14:04:11 -!- Phantom__Hoover has quit (Ping timeout: 248 seconds). 14:04:17 -!- Phantom__Hoover has joined. 14:11:31 -!- oerjan has quit (Quit: leaving). 14:14:34 oklofok: Ircle was quite popular, if you mean pre-X MacOS. 14:14:56 oklofok: As for current, I've heard of both Limechat and Colloquy. 14:17:25 hey oklofok 14:20:12 -!- Phantom___Hoover has joined. 14:20:14 supposing i have an infinite-dimensional vector space V with basis e_i and some T \in V* such that T(e_i) = 1 14:20:53 Sounds like a setup for a "your mom" joke. 14:21:32 -!- nisstyre has quit (Quit: Leaving). 14:21:46 then by linearity T(sum of e_i) = sum of T(e_i), which is an infinite sum of 1s 14:21:59 my question is how the fuck does this make sense 14:22:05 -!- Phantom__Hoover has quit (Ping timeout: 245 seconds). 14:22:56 you can't push the T into the infinite sum just with linearity 14:24:00 i'll check out if the rest of it makes sense 14:24:30 why not 14:26:25 ahh there's also the matter if the sum of e_i is even an element of V 14:28:37 just since the vector space &c axioms only require closure &c under finite sums (usually stated in terms of binary sums) and as with lots of things it doesn't generalize very nicely to infinities. i'd have to think a bit more if i wanted to say anything useful 14:29:13 -!- Phantom___Hoover has quit (Ping timeout: 246 seconds). 14:31:26 -!- Phantom_Hoover has joined. 14:35:56 mnoqy, mm, fair point 14:36:22 example: if you're dealing with, say, functions N->R with the obvious vector space structure, the set {e_i : e(i) = 1; e(j) = 0 for i \neq j} isn't a basis. that's a basis for the subspace of "finitely supported" functions. and the sum of all the basis elements isn't a member of that space. since linear combinations are finite sums of scalar multiples of vectors. 14:37:34 woops i messed up my explanation structure there oh well 14:38:06 would've helped if they'd thought to actually mention infinite-dimensional spaces before springing it on us in an assignment 14:39:33 -!- ^v has joined. 14:43:06 ah.. 14:44:42 infinite dimensional spaces are like finite dimensional spaces except sometimes you need the axiom of choice to find a basis 14:45:03 and you need to be more careful with the definitions 14:45:33 like if you define linear combinations with a sum over a set of indices you run into exactly this problem 14:52:55 remember how my maths class taught matrices before vectors. or any linear algebra. they're just introduced as magic rectangles of numbers, 14:58:03 the only thing I know about matrices is 14:58:10 that you always forget how to multiply them 15:02:52 i didnt understand matrices until i learned that theyre just a way of representing linear transformations in terms of som bases. then i understood them. i also never really ever had to do much in the way of computations on them so 15:03:54 Phantom_Hoover: sum of e_i is not an element of the vector space 15:04:14 although apparently you were answered already 15:04:16 mnoqy: really? 15:04:19 yes 15:04:24 *that's* when you understood them? 15:04:32 mroman, yeah, same for me 15:05:13 but note that there's not even a question of whether "sum of e_i" is an element, it doesn't even mean anything a priori 15:05:45 I'm not even sure if all matrices represent linear transformations 15:06:15 I though't that's only a sub space 15:06:23 oklofok, yes, i realise this 15:06:36 mroman, no, all matrices represent linear transformations 15:06:47 maybe you're thinking of invertible matrices 15:07:54 which would mean that not all linear transformations are reversible? 15:07:57 or reversable 15:08:10 i.e bijective 15:09:05 apparentely nott. 15:09:09 *not 15:09:17 sure, consider f(x,y) = x 15:09:26 -!- shikhin__ has joined. 15:11:52 oh 15:11:58 since we're already at match 15:12:01 *math 15:12:33 Does for any proof that gives an example (or counter-example) as a proof 15:12:39 -!- shikhin_ has quit (Ping timeout: 252 seconds). 15:12:44 exist a formal proof that does not rely on an example? 15:14:14 I.e. a counter-example shows, that a certain assumption does not hold for all cases 15:14:19 -!- Phantom__Hoover has joined. 15:14:19 (and therefore disproves it) 15:14:43 -!- Phantom_Hoover has quit (Ping timeout: 246 seconds). 15:14:54 that's like the opposite of what people normally try to do 15:15:07 but an example does not describe the exact reason why it does not hold. 15:15:41 the burden of explanation is on whoever's writing the proof 15:15:43 yes it does? 15:15:59 well 15:16:06 it does not hold because a counter-example was found, yes 15:16:54 but that doesn't mean that you can describe when exactly the assumption does not hold 15:17:48 so you want a way to construct all possible counterexamples 15:18:01 yes 15:18:21 or at least an algorithm that can state about any given input if it is a counter example 15:18:48 (or not) 15:18:56 ... 15:19:03 which is roughly the same :) 15:19:33 that algorithm consists of "check if the example satisfies whatever predicate you're concerned with" 15:19:48 but what if that's undecidable??????? what then 15:19:48 i.e. show that sin(x) + sin(f(x)) is not peridioc for all f 15:19:59 Counter example: sin(x) + sin(sqrt(x)) 15:20:27 *is periodic 15:20:55 mnoqy: Well 15:21:07 that would at least be an answer to if such an algorithm exists for all proofs :) 15:21:10 yes, the algorithm here consists of "determine whether sin(x) + sin(f(x)) is periodic" 15:21:38 I can prove that this is wrong by giving a counter example 15:21:55 but that does not mean, that I can really prove it for all f 15:22:11 all I know is, that it is wrong without knowing WHY it is wrong. 15:22:14 i don't get what you're getting at 15:22:43 it's wrong because there exists f such that sin(x) + sin(f(x)) isn't periodic 15:23:07 Yes 15:23:17 But I have no way of telling that for any given f 15:23:45 this is a largely orthogonal issue 15:23:54 because I don't have an algorithm which would solve that problem 15:24:24 -!- KingOfKarlsruhe has joined. 15:24:28 -!- shikhin__ has changed nick to shikhin. 15:24:46 whether it's true for arbitrary f is meaningless as far as the truth of the universally qualified statement is concerned; it suffices to know that it is not true for all f 15:25:10 Phantom__Hoover: That's true. 15:25:56 if you're using intuitionistic logic or whatever you actually need to specify an algorithm anyway 15:27:04 my opinion is, that a more precise proof would specify the exact properties f must have in order to make the statement wrong 15:27:17 -!- conehead has joined. 15:27:30 e.g as you said 15:27:40 an algorithm that produces counter examples. 15:27:56 so you're now actually dealing with two different notions 15:29:38 -!- Phantom___Hoover has joined. 15:30:49 basically your notion of a 'precise' proof is extremely limited and doesn't really give much meaningful insight in the relatively few cases where it even exists 15:31:39 There's the proof "does it hold for all f" 15:31:51 and there's the decision problem "does it hold for this given f" 15:32:06