00:00:03 well dependents kinda irrelevnat there 00:00:06 nooodl: there are better ones but i'm not going to bother 00:00:07 poo 00:00:08 So in addition to having combinators representing functions, we'll also have to have combinators representing types. 00:00:14 tswett, are you making a knotty language 00:00:17 http://nl.wikipedia.org/wiki/Lisp_(Lier) lispcon 2013 location 00:00:18 Bike: you know lisp-N+1s are shit 00:00:20 Phantom_Hoover: yes. 00:00:20 don't even try to lie 00:00:27 tswett, ooh how does it work 00:00:35 lisp-0+1, um 00:00:35 lisp-N+1s? 00:00:35 N=0? 00:00:37 elliott, er N includes 0 00:00:41 um no i'm using 00:00:46 shitty mathematicians definition of the naturals 00:00:51 when did you become ms flannagan 00:00:57 isnt it amazing how there are mathematicians who ACTUALLY BELIEVE THE NATURALS START WITH ONE 00:01:03 probably they don't even KNOW who PEANO is?? 00:01:06 Important issues, here. 00:01:07 :( 00:01:12 Phantom_Hoover: well, there's a finite state machine operating on a pointed directed unknot diagram. 00:01:19 Can't you have Z be 1? 00:01:28 erm, as in, starting point of Peanos 00:01:35 yes 00:01:39 but it's ugly and dumb 00:01:42 :-) 00:01:59 i mean for fuck's sake what sort of addition doesn't even have an additive identity 00:02:05 tswett, go on 00:02:30 nooodl, how's the Trustfuck impl going? 00:02:31 Phantom_Hoover: i see your radical tendencies peeking out :-) 00:02:36 Phantom_Hoover: how have you been feeling about the real nubmers lately 00:02:39 or should i say 00:02:40 Phantom_Hoover: the finite state machine is capable of moving the point around the diagram (but only forwards and backwards), as well as performing Reidemeister moves on the part of the diagram ahead of it. 00:02:41 the unreal numbers? 00:02:45 i kinda gave up on it 00:02:47 because almost all of them don't exist 00:02:48 Oh :( 00:02:54 i didn't know how much of my code was still correct 00:03:00 is Phantom_Hoover a finitist 00:03:05 but i also didn't feel like rewriting a new impl from scratch juuust yet 00:03:10 maybe i'll make a new one later though 00:03:12 MONQY constructivism isnt finitism 00:03:13 elliott, hey half the reasons i maintain 0 \in N are normal maths 00:03:17 Help design Trustfuck 2? 00:03:17 dont be SILLY 00:03:30 i mean starting at 1 is just dumb 00:03:43 so anyway nother silly haskell question, how's show-ing of things that have only a quantified type work? like 17 since i fucked saying things 00:03:44 * Sgeo_ hides Smalltalk and Lua from Phantom_Hoover 00:03:46 Phantom_Hoover: keep trying to convince urself chaitins constant existing is `normal' 00:03:52 does monqy believe 0 isn't \in N 00:03:54 there are perfectly fine ways to "construct" the "reals" 00:04:04 > show 17 00:04:05 nooodl: 0 \in N for reasonable values of N 00:04:05 that's my latex ineuqality sign 00:04:06 "17" 00:04:12 monqy: the computable reals are countable tho 00:04:12 Bike: I think Haskell picks a default instance. 00:04:13 nooodl: if you're talking to shit mathematicians though you have to be careful 00:04:17 Which I think is Integer in this case. 00:04:18 and all you can `construct' in eg coq 00:04:20 w/o axioms 00:04:25 tswett: Really? Boring. 00:04:26 thanks 00:04:36 (countable `externally') 00:04:39 (not ,,internally'') 00:04:40 :t 17+18 00:04:41 Num a => a 00:04:43 hm 00:04:45 istr my foundations course was absolutely terrible with 0 00:04:49 (but eg you have the thing where you can't write non-continuous functions w/o LEM) 00:04:52 sometimes it was in N, sometimes it wasn't 00:04:59 hm. what's an example of a noncomputable real 00:05:02 (b/c you cant case analysis on the reals) 00:05:05 nooodl: chaitins constant 00:05:05 nooodl: chaitin's 00:05:05 probably they don't even KNOW who PEANO is?? <-- the joke is that Peano started with 1, right? 00:05:25 Phantom_Hoover: that's pretty usual, sometimes they use Ñ and stuff and it's hilariously dumb 00:05:40 nooodl, (chaitin is a shitty example) 00:05:51 what's wrong with chaitin :( 00:05:53 oerjan: i never joke 00:05:55 i mean besides that he's crazy but 00:06:00 Phantom_Hoover: um chaitins is th ebest example 00:06:02 Here's an example: A real which cannot be described even with an infinite amount of symbols. 00:06:03 it sthe maximally hurty 00:06:05 Set a = 0 and b = 1, and then let R be a sequence containing all computable real numbers. 00:06:10 Sgeo_: ??? 00:06:11 chaitin's looks like a good example. i expected something halting problem-y 00:06:17 theres a bijection between reals and potentially infinite streams of bits 00:06:31 specker sequences are much better 00:06:34 * Sgeo_ is a derp 00:06:40 Pop values x from R until a < x < b, then set a := x. Pop values y from R until a < y < b, then set b := y. Repeat forever. 00:07:00 Correct example: A real which cannot be described with any finite amount of symbols 00:07:01 Both a and b will approach the same uncomputable number. 00:07:12 Sgeo_: That's undefinable, not uncomputable. 00:07:29 If it's undefinable, it's uncomputable 00:07:37 Yes, but not the converse. 00:07:50 "Undefinable" has the unfortunate property of being undefinable. 00:07:50 Sgeo_, that is several times shittier than chaitin 00:08:04 nooodl, also there are functions which grow faster than any computable function 00:08:05 i thought making a sequence of all real numbers was impossible! computable or not 00:08:23 if by "a sequence" you mean "a bijection with the naturals" then yes 00:08:29 the computable reals are a subset of turing machines, or whatever other tc system you want 00:08:43 nooodl: there is indeed no sequence that contains all real numbers. However, there is a sequence that contains all computable real numbers. 00:08:51 so you can count them, plus a bunch of TMs which aren't computable reals 00:09:08 but you can't actually tell if a given element is a CR without the halting problem 00:09:39 Bike: haskell has a default declaration which is used to pick default instances for things, the default default is default (Integer, Double) hth. also ghc has an extension to make it apply in more cases, and also prepends () to the default types. 00:09:58 wait that actually does help? what the fuck what is this 00:10:07 -!- sebbu has joined. 00:10:10 (a, b, c) really ought to be syntactic sugar for (a, (b, c)). 00:10:24 nooodl: you can well-order the rael numbers :-) 00:10:25 -!- sebbu has quit (Changing host). 00:10:25 -!- sebbu has joined. 00:10:42 tswett, tell that to elliott, who disagrees 00:11:10 yes make me into the absolute hub for not thinking that specific kind of hlist desugaring is a bad idea 00:11:13 ill never live it down 00:11:16 "the computable reals are a subset of turing machines" hmmm 00:11:43 nooodl: how about this: "the set of all Turing machines that output real numbers is a subset of the set of all Turing machines." 00:11:57 nooodl, a cr is basically a TM implementing a function N -> Q that converges 00:12:14 And given a Turing machine that outputs a real number, there is an obvious real number corresponding to it. 00:13:23 All right. So my language, as I'm currently imagining it, currently only has "if" statements for flow control. 00:13:28 yikes now i'm thinking about things 00:13:32 00:08:05 i thought making a sequence of all real numbers was impossible! computable or not 00:13:40 note that the computable reals are a subset of the reals like the naturals are a subset of the reals 00:13:45 and i'm sure you believe you can make a sequence of rationals 00:13:50 (the set of computable reals is countable) 00:13:59 I can make a sequence of all real numbers that are either two or pi 00:14:23 2, pi, pi, 2, pi, 2, 2, pi, pi, 2, 2, pi, 2, pi, pi, 2, pi, 2, 2, pi, 2, pi, pi, 2, 2, pi, pi, 2, pi, 2, 2, pi, ... 00:15:18 Let's condense that sequence. It alternates between 2 and pi, using each one the following number of times: 1, 2, 1, 1, 2, 2, 2, 1, 1, 2, 1, 1, 2, 1, 1, 2, 2, 2, 1, 1, 2, 1, ... 00:15:22 No actually it's just 2 and pi, repeating is silly 00:15:42 Which, in turn, alternates between 1 and 2, using each one the following number of times: 1, 1, 2, 3, 2, 1, 2, 1, 2, 3, 2, 1, ... 00:15:46 nooodl: you can well-order the rael numbers :-) <-- unidentified well-founded ordering 00:16:10 oerjan: yes. but only with extensional choice 00:16:10 Which, if you ignore the beginning 1 and drop all the 2s (since every other number, apart from the beginning 1, is a 2), you get this: 1, 3, 1, 1, 3, 1, ... 00:16:14 "[...] implementing a function N -> Q that converges" i still don't see how that represents a computable real :( 00:16:20 wait 00:16:21 (i.e., the choice that is a theorem (not axiom) of type theory does not give it) 00:16:27 o.O at parsers parsing things other than strings 00:16:38 nooodl, it's a sequence that approaches that real 00:16:39 (and extensional choice implies LEM, iirc) 00:16:39 the real value is just f(0) + f(1) + f(2) + ...? 00:16:42 oh 00:17:02 gotcha 00:17:16 the upshot is, almost all the reals are impossible to define in any meaningful way 00:17:17 And that, in turn, alternates between 1 and 3, using each one the following number of times: 1, 1, 2, 1, ... 00:17:37 and indeed this is true even if you're being nonconstructive 00:18:01 oerjan: yes. but only with extensional choice <-- you missed the pun on your misspelling hth 00:18:13 All right. So my language, as I'm currently imagining it, currently only has "if" statements for flow control. This makes the language definitely not Turing-complete; you can, in O(n) time, look at a program and place an upper bound on the length of time for which it will run. 00:18:30 is this still the knot one 00:18:34 Assuming you can perform arithmetic in O(1) time. 00:18:35 Phantom_Hoover: yup. 00:18:59 :t (<+>) 00:19:01 Ambiguous occurrence `<+>' 00:19:01 It could refer to either `Control.Arrow.<+>', 00:19:01 imported from `Control.Arrow' at State/L.hs:5:1-20 00:19:04 oerjan: oh that was rly stupid 00:19:06 you suck imo 00:19:38 So I need some way to go back and loop. 00:20:08 tswett: btw why didn't you use the kolakoski sequence above hth 00:20:10 augh 00:20:29 tswett, why did you have to say all the stuff about it while like 2 other discussions were going on 00:20:32 cocacola sequence 00:20:51 Phantom_Hoover: nobody told me not to. 00:21:35 elliott: thx 00:22:07 ^ul (12)S(*a(~:)~*^~):((1)S)~*~((2)S:*)~*:(~:()~)~*^(a(:^)*~a(*()~)~*^~^):^ 00:22:09 122112122122112112212112122112112122122112122121121122122112122122112112122121122122112122122112112212112122122112112122112112212112112212211212212112212212112112212211212212112112212112122112112122121122122112122122112112122112112212212112122112112212112112212212112122112112122122112122121121122122121122122112122122112112 ...too much output! 00:22:42 tswett, so wait, what controls the states for the fsm 00:22:53 the structure of the knot ahead? 00:25:25 > let kola = [1] ++ concat $ zipWith replicate kola $ cycle [2,1] in take 20 kola 00:25:27 Phantom_Hoover: yes. 00:25:27 Couldn't match expected type `[t0]' 00:25:27 with actual type `[[a0]] -... 00:25:36 > let kola = [1] ++ (concat $ zipWith replicate kola $ cycle [2,1]) in take 20 kola 00:25:38 [1,2,1,1,2,1,2,2,1,2,2,1,1,2,1,1,2,2,1,2] 00:25:54 nooodl: you don't need to use take in lambdabot 00:26:03 boo. it gets the start wrong somehow 00:26:03 it cuts off by itself 00:26:11 nooodl: you're not removing the initial 1. 00:26:22 i "realized" while out that it might be more interesting that constructivists would deny the existence of say the set of subsets of the naturals rather than reals but this is probably because i don't yet truly know how fucked up computable analysis is 00:26:30 > let kola = [1,2] ++ (concat $ zipWith replicate (drop 2 kola) $ cycle [2,1]) in take 20 kola 00:26:34 mueval-core: Time limit exceeded 00:26:35 Mmmm. 00:26:42 Maybe that's not the problem. 00:26:48 Bike: have you noticed that powersets are scary 00:27:00 well they only drove cantor insane 00:27:17 power sets are terrifying 00:27:28 * Bike was thinking about the set of all subsets of a set not containing an element of the set earlier, and it got tied up with this 00:27:40 i read a paper once on "power types" 00:27:41 > let kola@(_:ks) = [1] ++ (concat $ zipWith replicate kola $ cycle [2,1]) in 1:2:ks 00:27:43 [1,2,2,1,1,2,1,2,2,1,2,2,1,1,2,1,1,2,2,1,2,1,1,2,1,2,2,1,1,2,1,1,2,1,2,2,1,... 00:27:46 now that was some good shit 00:27:49 how unsatisfying 00:29:10 * Bike was thinking about the set of all subsets of a set not containing an element of the set earlier, and it got tied up with this 00:29:19 hi 00:29:20 isn't that just... P(S\x) 00:29:25 yes 00:29:40 Oh. Not containing a *given* element of the set. 00:29:43 oh huh kolakoski is A000002 00:29:47 As opposed to not containing *any* element of the set. 00:29:58 wouldn't that just be empty 00:30:07 It's like A000001, except posterior. 00:30:11 Bike: it would be {{}}, yeah. 00:30:17 > fix(([1,2]++).drop 2.concat.zipWith(flip replicate)(cycle[1,2])) 00:30:19 [1,2,2,1,1,2,1,2,2,1,2,2,1,1,2,1,1,2,2,1,2,1,1,2,1,2,2,1,1,2,1,1,2,1,2,2,1,... 00:31:15 Trivia: "sword" is not a subword of "subword". 00:31:26 Do people use Parsec when making stuff for QQ stuff in Haskell? 00:31:47 Q: why are you doing QQ stuff 00:32:02 just making sure you're not hopped up on macros again 00:32:07 Q: ¿q s qq? 00:32:16 tswett: good q 00:32:28 Yesod uses it, right? 00:32:39 ugh. Q: how do math people write that a function returns, for example, a set of reals 00:32:49 powerset 00:33:11 i think ive also seen subset 00:33:11 thanks 00:33:12 but 00:33:15 thats weird 00:33:29 powerset is what i see most of the time 00:34:05 wow crazy people use ℙ for powerset according to wikipedia 00:34:33 solely to piss off kmc no doubt 00:34:40 ℙ(ℝ) 00:34:47 lol. 00:35:08 dont use blackbord bold for powerset.... 00:35:08 ℙ(ℙ) "power set of prime set" 00:35:12 then there's the weirstrass P function 00:35:31 then there's the weirstrass function 00:35:40 math's notation is such a fucking trainwreck at times 00:35:41 i think mathcal is the proper font to use? i'm fairly certain i've seen mathsf and mathscr though 00:36:20 fortunately there's not much confusion with the latter because the weirstrass function is never actually used as a function 00:36:45 nooodl: at times/most of the time really 00:36:49 "at times" 00:37:08 well sometimes it's really good & clever 00:37:13 What does the "sf" in mathsf stand for? 00:37:19 sans serif 00:37:27 nooodl, it helps if you remember that it's still mostly written by hand 00:37:30 nooodl: like.... 00:37:39 numbers 00:37:49 "This combinator is provided for compatibility with Parsec. Attoparsec parsers always backtrack on failure." 00:37:51 * Sgeo_ likes that 00:38:01 have you ever looked at a 9 00:38:05 and there are a load of ways to write any given symbols 00:38:05 like really looked at a 9 00:38:20 its a gargoyle 00:38:22 9 is pretty heck but i love 7 so it makes up for it 00:38:22 Like, an actual 9, or a numeral 9? 00:38:25 4 is p.good too 00:38:34 7's a good numeral 00:38:35 2 is my favourite 00:38:41 2 is p.good too 00:38:43 surely someone out there has had the zany idea to reinvent the notation for Everything 00:38:44 except you have to dash the 7 00:38:47 for ambiguity reasons 00:38:49 and then it looks not so good 00:38:52 i always dash my 7s 00:38:52 because those times when you nail it and it has an elegant curl in the tail are the best things ever 00:38:55 i love dashes on 7s 00:38:57 i hate 1 because you need to make it all fancy to avoid ambiguity 00:39:00 nooodl: you have no idea 00:39:01 i also give my 7s cute little hooks 00:39:05 and its also the caues of the 7 Ambiguity Problem 00:39:12 2 is pgood imo 00:39:16 sometimes my 7s look like my ts, or maybe it's more that my ts look like my 7s 00:39:17 5 is quite nice too 00:39:20 also i wrote out a 4 the other day and one of my coworkers stopped me for two minutes to ask me about how i wrote it 00:39:25 "i've never seen someone write a 4 like that" 00:39:26 monqy: whats your handwriting look like 00:39:26 jesus. i write my 2s like a normal person and it makes them look a lot like Zs or zs 00:39:38 elliott: hm 00:39:41 i like how the variable x looks but im so bad at writing it 00:39:44 so i lovehate it?? 00:39:53 x is christian propaganda 00:39:57 i came up with the perfect way of writing x 00:40:01 i was so proud 00:40:05 my x is literally an x 00:40:08 two lines 00:40:15 gross nooodl 00:40:16 real gross 00:40:17 it's like )/( 00:40:18 maximal gross 00:40:24 you're disgusting, rectify yourself 00:40:41 but once you get the hang of it the / runs together and it looks great 00:41:19 this is the only picture of my math handwriting i've got https://dl.dropbox.com/u/15495351/snow/IMAG0043.jpg 00:41:38 which is probably 1 more picture than the average person 00:42:06 elliott already knows what my "math handwriting" looks like 00:42:22 elliott: i have a few copeies of me trying to handwrite on my tablet from a while ago...there's an aspect ratio problem which messes up my hand-eye coordination so it's kind of eugh 00:42:37 dumb question again, how do i write "numLongChains long max = length $ longChains long max" in that fancyass pointless style 00:42:42 i have this thing too which is normal writing and it's very real 00:42:45 https://dl.dropbox.com/u/15495351/snow/IMAG0046.jpg 00:42:47 my handwriting is an abomination 00:42:55 but it looks quite nice locally 00:43:07 Bike, you can ask lambdabot 00:43:08 -!- Nisstyre-laptop has joined. 00:43:17 @pl numLongChains long max = length $ longChains long max 00:43:17 nvm figured it out 00:43:17 numLongChains = (length .) . longChains 00:43:19 Bike: numLongChains = length .: longChains 00:43:24 love you dots 00:43:25 note how nooodl double-spaces his work and sets it all out neatly 00:43:34 this is wasteful and capitalist 00:43:37 i use latex for math 00:43:45 writing is for losers 00:43:59 monqy: i can't do that at school!!! 00:44:17 wait is this linguistics 00:44:21 elliott: gosh i have 6 pictures of me trying to handwrite and they're all sorta different 00:44:35 elliott: i forget what i did differently each time except for handwriting6.png 00:44:37 i want to see monqys trying to handwrite 00:44:43 i want to use latex but why does it have to have all that madness with \doctype and headings and everything 00:44:52 btw i have worse handwriting than any of you 00:44:59 latex is literally the worst thing 00:45:04 that i've ever used 00:45:12 nooodl: dont use (.:) 00:45:13 https://dl.dropbox.com/u/13786158/handwriting.png 00:45:14 https://dl.dropbox.com/u/13786158/handwriting2.png 00:45:15 https://dl.dropbox.com/u/13786158/handwriting23.png 00:45:16 dont tell people to use (.:) 00:45:16 er 00:45:19 https://dl.dropbox.com/u/13786158/handwriting3.png 00:45:20 cry instead........... 00:45:21 https://dl.dropbox.com/u/13786158/handwriting4.png 00:45:24 https://dl.dropbox.com/u/13786158/handwriting5.png 00:45:26 https://dl.dropbox.com/u/13786158/handwriting6.png 00:45:29 there thats all of them 00:45:30 are you going to tell me to use (.).(.) 00:45:31 enjoy 00:45:33 if so i'm going to cry 00:45:34 (handwriting23 does not exist) 00:45:40 im going to tell you to add a fuckn point 00:45:43 dont use (.).(.)............................... 00:45:52 what the heck is .: 00:45:53 -!- md_5 has quit (Ping timeout: 248 seconds). 00:45:58 Bike: it doesnt exist 00:46:00 sry 00:46:02 holy shit. monqy's handwriting 00:46:02 monqy: shit your handwriting is nice 00:46:02 k 00:46:03 can i rent it out 00:46:03 is so good 00:46:07 @src (.:) 00:46:07 Source not found. Do you think like you type? 00:46:16 monqy 00:46:20 Bike, it exists, but may be considered to be an excessive use of pointfree style 00:46:21 monqy 00:46:22 you dot your j 00:46:24 with a circle 00:46:26 go fuck yourself 00:46:27 well i dont like the unfilled dots 00:46:29 but apart from that 00:46:36 imo dijkstra has the best handwriting 00:46:40 imo monqy should dot his js with a heart 00:46:41 so you might as well give up now 00:46:42 when im writing with a real pen i think i use normal dots 00:46:48 here's a little "latex gem" 00:46:48 Although "exists" as in, "well-known", not "standard" 00:46:49 \chemname{\chemfig{C([2]-\lewis{024,Cl})([6]-\lewis{046,Cl})([:-150]-\lewis{357,Cl})([:-30]-\lewis{157,Cl})}}{Koolstoftetrachloride} 00:46:50 but with tablets i cant resist 00:46:54 @hoogle (.:) 00:46:54 No results found 00:47:14 U+24A38 COMBINING HEART ABOVE 00:47:27 Oh hey Aeson uses .: for something else 00:47:36 nooodl, well be fair 00:47:40 my hand writing is worse than nooodls by far tho 00:47:55 that's for a diagram, however you represent that textually it's going to be awkward 00:48:09 elliott, do you even need to write??? 00:48:20 i can write really neatly if i try 00:48:21 like my handwriting is honestly a 6 year olds 00:48:24 but i don't ever 00:48:30 its an awful scrawl 00:48:31 elliott: my handwriting is a 3 years olds?? 00:48:48 Cl 00:48:49 shachaf: do you even have any proof all i see is you syaing your handwriting is so much worse than everyone else's!! 00:48:53 >C-Cl 00:48:54 Cl 00:48:58 elliott: do you have proof!! 00:49:01 what now Phantom_Hoover!!!!! 00:49:25 I can write in cursive, but only words that only contain the letters a, e, h, i, n, o, s, and t. 00:49:40 There are a bunch of such words. 00:49:45 nooodl, good luck writing a transparent parser for that 00:49:55 transparser 00:50:08 I have a little sheet of paper on which I've written "anaesthesia antiatheist assassination ensheathe hastiness heathenishness hesitation honestness ..." 00:50:15 Sgeo_: you know, I think any function can be thought of as a parser. 00:50:18 "you don't need to parse pure beauty any further" 00:50:18 im going to try handwriting again 00:50:29 the entire point of latex is that you give it a general representation and leave the typesetting details to it 00:50:45 i think dijkstras handwriting is still a bit better than monqys 00:50:45 PArrows is unmaintained :( 00:50:48 mostly since its smaller 00:50:57 my handwriting is smaller than that irl 00:51:00 Phantom_Hoover: fsvo all of that 00:51:03 -!- md_5 has joined. 00:51:04 but my tablet setup is miserable 00:51:09 and i dont have a scanner or anything 00:51:10 Help what is handwriting 00:51:19 monqy: by smaller i mean... less fussy mainly??? as in less ... "area" 00:51:22 i stole my f's from dijkstra 00:51:22 > " 00:51:22 " 00:51:24 :1:2: 00:51:24 lexical error in string/character literal at end of input 00:51:25 i dont know how to express the meaning 00:51:27 ah 00:51:28 Hmm. 00:51:30 but they don't look like dijkstra f's anymore... 00:51:33 yeah my handwriting is pretty fussy 00:51:46 > "\ 00:51:47 \" 00:51:48