00:03:35 -!- zzo38 has quit (Quit: Is Dungeons&Dragons turing complete? Actually, that isn't even a valid question).

00:04:57 <ehird> <some statement about being apple-fanboy-forced into buying the ipad><criticise it rampantly><says that i still love it>

00:05:08 <AnMaster> <coppro> the basic version would just take a text and replace each character with an image <-- bitmap font rendering?

00:05:38 <cpressey> I gotta say, I love it when unit tests fail when you substitute a class with a subclass of it which *overrides nothing in it*

00:06:24 <ehird> AnMaster: Regular teenagers think they have issues with deciding on their sexuality. They should try being freedom-lovin' Apple fanboys.

00:06:38 <AnMaster> coppro, wow what a great new invention! rendering text to a graphical image. Rather than sending it to a vt100 terminal unit

00:08:00 <AnMaster> unless you want: "is that an ipad in your pocket, or are you just extremely happy to see me?"

00:15:37 <ehird> the "i am sitting on a bench and I want to read the new york times and check my email" case for one

00:19:57 <coppro> because touch-typing sucks on a keyboard with no force feedback, and the angle is awkward because you have to type and view on the same surface

00:20:31 <AnMaster> <ehird> it runs a subset of iphone apps too so it's a big games console <-- not full OS X apps?!

00:21:31 <AnMaster> <Wareya> American laptops: Full sized keyboard! Bigger keys instead of a full layout! Yay! <-- hm?

00:22:38 <AnMaster> Wareya, well my lenovo thinkpad has qwerty minus numeric keypad. the main (letter) area have keys the same size as a full sized pc keyboard

00:25:54 <Wareya> Instead of taking advantage of the space for a full kayboard layout, they squeezed in an engarged laptop layout.

00:33:39 <ehird> so anyone want to come to norway with me and found an operating systems and programming languages research company

00:35:06 <ehird> apart from that, you know, big space with lots of computers networked together... you can come into work if you want, some sort of money will probably change hands at some point

00:38:33 <ehird> congratulations, you managed to turn #esoteric to the awkwardly homoerotic once more.

01:13:54 <oerjan> just found that "old" comic... i've been reading other comics on foglio's site for ages without realizing "What's new" _wasn't_ a link to the news section

01:23:16 <oerjan> also i would say it's because we're all culturally impressed with associating good with light and law

02:16:08 <olsner> well, it's being developed, and I have an experimental implementation that should be reworked slightly to make it TC

02:17:05 <olsner> ehird: oh, ensadden me as early as possible so that I may not be worsely ensaddened in further future

02:18:55 <ehird> If I was about to die, I couldn't be talking lightly about ensaddening people on IRC. I'm utterly terrified of death.

02:23:30 <olsner> yah, knew you're young... your situation sounds weird and harsh, but it's how I've always suspected "mental care" works pretty much everywhere

02:23:48 <olsner> after all, it's pretty much impossible to differentiate sane persons and insane persons claiming to be sane

02:24:35 <ehird> olsner: I would be less ... whatever emotion I am about this whole situation if they were making steps to treat what they brand me with, instead of a bullshit "malnutrition"

02:30:00 <olsner> I think these systems are (with good intentions) built to prevent either you or your parents from bailing you out

02:33:59 <Sgeo> If they're claiming "malnutrition", they can't find a way to make sure you eat without detaining you in a place?

02:35:40 <ehird> They're not making sure I eat they're just giving me a drink that's woefully inappropriate; 2 x 1390 kcal + whatever else I eat in the day = one over-caloried puppy, and it's designed for people with disease-related malnutrition who *cannot* get the required amount of energy from food. And I'm not malnutritioned, I eat alright, maybe a bit less than usual. I'm just very thin, just as my father was.

02:36:07 <ehird> But, you know, if the junk science of BMI says I'm overweight, well howdy-doody, to hell with the facts

02:36:47 <Sgeo> Even though technically I can get the required amount of energy from food, I tend not to

02:38:22 <olsner> I suppose detaining and force-feeding is what they will ultimately resort to to make you eat, after trying various other things, if they still think you're malnutritioned

02:46:45 <ehird> olsner: there's an anorexic girl there, 13, celebrity-obsessed, refuses to eat or drink. they just have her on a feeding tube.

02:47:05 <ehird> they don't seem to especially care about actually fixing things, just temporary "fixes"

02:47:16 <ehird> Sgeo: maybe you just eat the wrong things. But seriously, nutrition science is crap.

04:35:43 <uorygl> "Suppose I have a ball on a hill. The ball is tolling directly up toward the top of the hill, such that its total energy is equal to what it would be if it were at rest at the top of the hill. So, it has enough energy to get to the top, but does it actually do so in a finite amount of time?"

04:41:23 <Sgeo> I think if chapstick had some kind of toxin that was only dangerous if a lot of chapstick was needlessly used, I'd be dead now

10:23:38 * Bullseye is running I-n-v-i-s-i-o-n 3.1.1 (June '09) with Advanced File Serving features by cRYOa on mIRC v6.35 32bit obtained from #Invision on irc.irchighway.net and http://www.i-n-v-i-s-i-o-n.com

10:42:04 <oklopol> "if there is a finite distance along the flat to the edge from the balls initial starting place, then i think you are right, an infinitely small push would take an infinite amount of time to even reach the edge, so the exact nature of the slope and the starting position may make a difference here" god these guys are retarded

12:01:05 <AnMaster> verangirl, mhm, you know this channel is about esoteric programming languages right? Not about esoterica.

12:03:42 <AnMaster> esoteric programming languages being intentionally unusual, weird or silly languages. Often (but not always) designed to be hard to program in.

13:07:57 <ehird> oblivious to how things work, merely trading magic incantations that appear, on the surface, to do what they desire

13:08:42 <ehird> also 23:33:37 <Sgeo> ehird: If you see this, remind me that I have to tell you something

13:37:11 <ehird> "My own vote is clear: yes to both. Equality is reflexive (every value is equal to itself, at any longitude and temperature, no excuses and no exceptions); and the purpose of assignment is to make the value of the target equal to the value of the source. Such properties are some of the last ramparts of civilization. If they go away, what else is left?" --Bertrant Meyer

13:43:39 <ehird> MissPiggy: agda question - it's tc but total, right? how does it handle that; that partiality monad?

13:45:30 <ehird> in the language i spent a night babbling about - which has, as these things tend to, mutated wildly since - i'm trying to make it total, but to have partiality very ...

13:45:45 <ehird> AnMaster: http://bertrandmeyer.com/2010/02/06/reflexivity-and-other-pillars-of-civilization/

13:47:05 <MissPiggy> the function space A -> B (or forall a : A, B, or whatever) cannot express every recursive function

13:47:44 <ehird> expressing it with a data type, how do you mean? I'm curious if it's what I'm thinking of or not

13:48:15 <MissPiggy> well you can define all the primitive recursive stuff and Mu, just as a syntax first

13:48:35 <ehird> right right, but what's the actual data type; i mean, it's a total language so is there sort of a backdoor where you can introduce partiality?

13:49:04 <MissPiggy> so you really are talking about the class of recursive functions now, every proof you write with respect to the semantics of that type is a valid statement about them

13:49:53 <ehird> so presumably to make meaningful use of them, given a haskell-style main program solution, you need main :: Partial (IO ())

13:50:08 <ehird> otherwise you'd be in total-land, and couldn't invoke the forbidden fruit of the partial lands

13:52:40 <ehird> my lambda syntax is currently λα.β because otherwise function types would get confusing :) (λα. α → ∅) vs (λα → α → ∅)

13:53:15 <ehird> admittedly it is rather awkward as I have *not* yet written an editor mode or editor which lets you type \a. a -> () to get that

13:55:47 <ehird> Well, considering I am planning to use this language as an entire OS, I'm sure I will run into partiality at some point - and the total FP paper certainly did show that some operations are damn awkward with total FP.

13:56:32 <ehird> I dunno. I love the proof system duality and the mathematical soundness of having no ⊥,

13:57:08 <ehird> MissPiggy: My goal in computing is to completely revolutionise it. My two separate interests are operating systems and programming languages.

13:57:19 <ehird> It is only natural that my awesome programming language would be my awesome operating system.

13:57:51 <ehird> My OS design involves the programming language being central; a living environment.

14:00:24 <ehird> ∅ seems less confusing; ⊥ is too associated with non-termination and undefinedness in programming

14:00:42 <ehird> then again, I'd like to be able to use ∅ to denote empty containers in value-land, and that would be doubly confusing

14:01:08 <ehird> well, whatever; apart from agda guys, haskellers are the most mathematically civilised programmers :)

14:03:42 <MissPiggy> I was thinking about a language that could compile into almost every high level language

14:05:21 <ehird> MissPiggy: can you think of any way to use ≠ for equality and not be inconsistent since = is definition? maybe a better symbol for definition? :P

14:06:57 * ehird considers that |α| instead of abs α may be taking the mathematical notation thing a *bit* too far

14:07:13 <ehird> MissPiggy: a more hideous symbol I've not seen! I wonder what font size I'm expected to use to make out "def" there.

14:07:51 <MissPiggy> yeah I'm not keen on the unicode stuff because all the operators are too small (unnecessarily :/)

14:10:05 <ehird> Okay, okay, so any fancy space-age editor, like my OS, will *display* it as superscripts.

14:11:01 <ehird> (Actually I think my OS will only have to consider code as text for interacting with the outside world. Internally, it's an AST or compiled code; in the UI, it's rendered with fancy things like superscripts.

14:11:22 <fizzie> We have a maths teacher who uses sub- and superscript indices completely interchangeably, often changing them between consecutive lines. Also some sort of "middle-scripts" occasionally.

14:14:47 <MissPiggy> http://www.reddit.com/r/math/comments/axd4m/what_is_the_mathematical_rule_that_says_if_abc/c0jw2vc

14:15:18 <ehird> anyone who answers a question starting "What is the mathematical rule" with "common sense" is so idiotic I cannot comphrend it

14:20:49 * ehird wonders if he's crazy enough to do ÷ ∷ Boringtypeclasstypethingy → Anotherone → Maybe Yetanotherone

14:21:17 <ehird> Yesiree we have a mathematical programming language here, please ignore the endless handling of ÷'s return values behind the curtain

14:22:51 <ehird> Like, say f {x} (y z {r q {x}}) → (using haskell syntax) do x' <- x; x'' <- x; r_q_x' <- r q x''; return (f x' (y z r_q_x'))

14:23:03 <ehird> given some surrounding brackets to denote that it's a special expression thingy ofc

14:23:27 <ehird> MissPiggy: So, do you think ≡ is a reasonable symbol for what-Haskell-calls (to avoid ambiguity) =?

14:26:02 <AnMaster> ehird, Hm is ÷ fraction, integer division, floating point division or something else?

14:26:44 <ehird> Well, not all of "something else". You have to obey some properties, or the compiler will yell at you.

14:29:46 <AnMaster> then it can not produce a "simple" floating point value when dividing two floating point values I think.

14:30:45 <ehird> I'd relax it to {| someEqualityThingProvidedByTheDefinition (α × {β ÷ α}) β |}, but that's as good as letting you define it to anything.

14:32:16 <MissPiggy> so you could quotient out by "someEqualityThingProvidedByTheDefinition" and still use {| α × {β ÷ α} ≡ β |}

14:32:45 <AnMaster> ehird, iirc any floating point operation is potentially inexact. Well, almost any. x := y would be exact if both are the same type of floating point.

14:32:48 <ehird> so that allows inexact definitions but still doesn't let you define it to anything you want? How?

14:35:39 <AnMaster> <ehird> and specify the inexact implementation as an "implementation detail" <-- "this implementation always round to zero. No, that isn't a typo for 'towards zero'."

14:35:45 <ehird> it occurs to me that "e" is a rather inconvenient name to give e, given the commonality of single-letter variable names...

14:36:34 <ehird> i'd call e "euler", but euler has done so many mathematical things that it would be hopelessly vague :P

14:37:45 <AnMaster> ehird, well, as someone in here said: it is perfectly in spirit with this channel to try to make a working thing of a joke.

14:39:10 <AnMaster> ehird, why is e a bad name for e? I can think of at least one way to end up with that as a reasonable letter

14:40:42 <ehird> although at the same time I don't think I want to abandon the entirety of linear syntax

14:41:42 <AnMaster> (basically: (e^x)' = e^x, thus it is "its own derivative", and a lot of mathematicans were from Germany historically, thus that leads to "eigen" for "own/self", thus e)

14:42:53 <MissPiggy> suppose you were making a type system or soemthing, and you wanted to define a function t :: T, to express that t has type T

14:43:05 <ehird> And you run into the same problem, although I guess mathematicians wouldn't name variables e because of that.

14:43:13 <MissPiggy> the type of t depends on T, so in mixfix you can't do it.. you have to write T ::' t

14:43:49 <ehird> MissPiggy: I just meant the general idea of being able to define an operation if_then_else_, not any specific definition of the semantics

14:44:07 <MissPiggy> yeah if you just make them notations, rather than well typed terms I think it's better

14:45:14 <ehird> also, you may be used to seeing it but I observe agda from a strictly outside viewpoint! ha!

14:46:27 <ehird> yeah i prettyprinted my expression that (given infinite time) checked if the reimann hypothesis was true or false

14:47:49 <lieuwe> i'm still trying to come up with some sort of high-level esolang... can't come up with anything implementable :-/

14:48:11 <ehird> AnMaster: Was that a pun? A carrier carries something, if a carrier stops carrying something they drop it?

14:49:00 <AnMaster> ehird, it was a reference to modems mostly. Remembers those leds on them? I mean good old 28 kbit ones and such

14:50:15 <ehird> MissPiggy: i have this horrible feeling that the ML-style module system is going to interact terribly strangely with my type system

14:53:43 <ehird> Yeah, yeah, so in actuality those names are in the Container or Sequence or whatever thingy.

14:53:56 <ehird> And yes, overloading ∅ to mean something other than the empty *set* is probably abhorrent.

14:57:53 <ehird> You're saying the same thing as "it seems wrong to use the same symbol for addition and addition".

14:58:24 <ehird> Although you have a point in that _∈_ in value-land will be container/sequence-membership, and it'd be nice to be able to use things like that in type-land

15:01:23 <ehird> MissPiggy: but yeah, _∈_ in value-land will be member-of-sequencecontainerwhatever; and it would be nice to be able to use that in type-land, which we can't do if we use it for type judgement

15:01:37 <ehird> bloody haskell doesn't have to avoid naming conflicts between value- and type-land :P

15:07:21 <ehird> i'm fairly sure that it's an odd instance of the curry-howard isomorphism though, in that they're the same definitions but used entirely differently

15:08:05 <MissPiggy> a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category.

15:09:21 <ehird> also they, well augur, also i think i've seen you, use basically lambda calculus for some syntax :P

15:09:43 <AnMaster> no no don't do it. We won't get rid of the linguistics discussion for hours then! :(

15:11:18 <oklopol> MissPiggy: in category theory, you have objects, and "structure-preserving mappings" between them, then you have a very general way to define things like isomorphisms, the same definition works for groups and sets and so on, because you just talk about properties of functions that have to do with their composition.

15:14:06 <oklopol> basically isomorphisms can be just defined as mappings that can be inverted both ways, that is, "no info is lost", then when you look at the category of groups and morphisms, and the category of sets and functions, you'll see that you've defined a sensible isomorphism for both

15:14:56 <MissPiggy> would be nice to have a formal theory about these informationy heuristics we use

15:31:02 <MissPiggy> by the way (you probably know this..) the dependent type stuff is more general than GADT

15:35:36 <ehird> # 9.7-inch (diagonal) LED-backlit glossy widescreen Multi-Touch display with IPS technology # 1024-by-768-pixel resolution at 132 pixels per inch (ppi)

15:38:29 <AnMaster> btw, for P=NP, could it be that it is unprovable if it is the case or not? Has anyone tried to prove it unprovable?

15:38:49 <ehird> http://www.google.co.uk/#hl=en&source=hp&q=p%3Dnp+unprovable&btnG=Google+Search&meta=&aq=f&oq=p%3Dnp+unprovable&fp=33a9a577caa4e7cb

15:38:57 <ehird> This article shows that "P-not-equal-to-NP" is unprovable in ZFC. Here is a review of this proof by the German logician Ralf Schindler. ...

15:40:12 <ehird> "Proof by contradiction. Assume P=NP. Let y be a proof that P=NP. The proof y can be verified in polynomial time by a competent computer scientist, the existence of which we assert. However, since P=NP, the proof y can be generated in polynomial time by such computer scientists. Since this generation has not yet occurred (despite attempts by such computer scientists to produce a proof), we have a contradiction."

15:42:54 <ehird> If we can defeat entropy and have a singularity it doesn't matter how long computations take; the universe will be filled with one gigantic computer on which all our minds will be uploaded. It will make us experience time in sync so that every computation is instant.

15:43:15 <ehird> i.e., if someone runs a computation that takes a gazillion years, everyone stops thinking, a gazillion years pass, then we resume thinking; to us, the computation happened immediately

15:43:25 <AnMaster> ehird, well, my brain was in math proof mode when reading it. I do see the joke now

15:45:20 <AnMaster> what I meant was, that maybe P=NP is unprovable in the same sense as the cardinality of R. Or to take another example: the parallel postulate in Euclidean geometry. (Which is why it is an axiom)

15:49:51 <AnMaster> couldn't it (in theory) be proven that it is impossible to prove either P=NP or P!=NP ?

15:50:52 <ehird> It could be true that it is unprovable and yet not be provable that it is unprovable.

15:53:45 <MissPiggy> <ehird> Why don't we just define P=NP as an axiom? -- because nobody knows if it's independent yet!!

15:57:41 <ehird> She has rules, and the first is: She can be talked about, but only if you respect her grammar.

16:04:09 <ehird> MissPiggy: any totally dependawesome insights on http://www.daimi.au.dk/~madst/tool/papers/expression.txt

16:04:22 <ehird> she has http://personal.cis.strath.ac.uk/~conor/pub/she/higpig.html but i dunno seems hacky

16:05:01 <AnMaster> Deewiant, I have a vague memory of reading that AKS is horribly inefficient though. And that some of the non-polynomial algorithms are in fact faster in practise for most "practical purposes"

16:05:18 <MissPiggy> and I'm not sure even if I come up with a solution that I deem _perfect_ other people will just say it sucks

16:05:29 <ehird> Here, we can easily add functions (columns) to this without violating type safety or modifying existing code,

16:05:49 <Deewiant> AnMaster: I don't know if it's "horribly inefficient" but yes, in practice it's slower than the probabilistic tests

16:06:07 <ehird> in an object-oriented language, the columns can't be changed: they're the methods in a class

16:07:25 <ehird> you can easily add new functions, but you cannot add rows *elsewhere in the program*

16:07:48 <MissPiggy> so to add a new constructor you have to update each func1, and to add a new func you have to update each constructor??

16:08:26 <ehird> so with FP you can add columns, with OOP rows; the problem is being able to add both

16:09:44 <AnMaster> btw, when you measure O(whatever) for an algorithm for prime factorisation, what exactly is it you measure it against.

16:12:22 <AnMaster> Deewiant, wouldn't then "try each number from 2 to sqrt(n) to see if it divides n" be O(sqrt(n)). After all, that is how many divisions you perform. And O(sqrt(n)) would grow slower than O(n), no? And isn't O(n) polynomial?

16:13:10 <oklopol> AnMaster: that's a pseudopolynomial algorithm for it, a polynomial algorithm, when talking about numbers, is one where you take n as the log of the number

16:13:39 <oklopol> for numbers we have separate classes for taking the number as its own size (pseudo), and taking its log as size (more natural for most problems)

16:16:32 <ehird> Well, for anyone who wants an explanation of what the expression problem is: http://pastie.org/812457.txt?key=jy9qm2hfkgtfxiooahshxw

16:17:23 <AnMaster> oklopol, hm correct me if I'm wrong but: log_a(n) > log_b(n) for all n if a < b?

16:18:41 <ehird> oklopol: So I suppose you could say that you have 99 (minus 94) problems, but a bitch ain't one.

16:19:00 <AnMaster> oklopol, well yes, but that isn't what I said. I said what their relative values are

16:21:50 <Deewiant> AnMaster: What you're missing in your trial division thing is the complexity of a division

16:21:50 <AnMaster> oklopol, does it make sense to do something like lim_{a->+inf} log_a( whatever )

16:23:06 <AnMaster> whenever it is constant or not could perhaps be argued, but it no longer depends on n at least

16:25:09 <AnMaster> but, it is an interesting question: What happens with logarithms as the *base* approaches infinity?

16:25:41 <oklopol> the function "f(n) = lim_{a->+inf} log_a( n )" is the constant function 0, i think

16:26:48 <oklopol> i also think in the interval [1, inf) we have uniform convergence, but my head hurts a bit too much now to be sure

16:28:32 <Deewiant> AnMaster: If n = number of bits in the number then trial division is O(2^(n/2)) (Wikipedia), which I guess is where the non-P-ness comes from.

16:31:48 <AnMaster> also, why can't you have negative arguments to log? I mean, y = log_a(x) means the same as a^y = x right? And in the latter you can get negative x.

16:35:10 <oklopol> with a negative base, it makes no sense to give the log any arguments except naturals afaik

16:35:12 <AnMaster> ehird, well yeah, when you think of logarithms that way it doesn't really work out ;P

16:38:48 <AnMaster> Deewiant, but then sqrt(n) really isn't unique either, except it is defined to be the positive value. Which is why you for the solution to x^2 = 4 would write x=+/- 2

16:39:57 <Deewiant> AnMaster: As I see it, the problem is defining log_a(x) so that it gives the appropriate real result for negative x, but is undefined when no such value exists

16:41:50 <AnMaster> Deewiant, hm? Two things there: 1) why must it be a real value? 2) undefinedness in some points doesn't sound too bad, after all x^-1 is undefined for x = 0 (defined in all other points afaik)

16:43:20 <AnMaster> Deewiant, isn't it undefined due to x^-1 = 1/x and division with zero being undefined?

16:43:22 <Deewiant> AnMaster: Sure, you can let it be undefined for some values, but what are those values

16:43:29 <MissPiggy> now the actual elements of each row/col would have a type computed based on the recursion structure of the function in that column against the fold for the type of that row

16:43:53 <MissPiggy> ehird anyway that's just the idea.. I'll try and write it out and see if it works

16:44:23 <AnMaster> Deewiant, I think we are talking about two different things here. with regards to 2).

16:44:43 <AnMaster> Deewiant, Didn't "sure, but what's the definition" refer to the bit "x^-1 is undefined for x = 0"?

16:45:30 <AnMaster> Deewiant, as in, you claimed x^-1 was undefined for x=0 due to being defined that way XD

16:47:36 <oklopol> of course you can define the function to have any value you want, you just can't make a field have a meaningful multiplicative inverse for 0

16:47:45 <AnMaster> hm, forgot that was by definition rather than as a consequence of something else

16:48:15 <AnMaster> Deewiant, but a lot of math wouldn't work if it wasn't defined like that though.

16:52:00 <AnMaster> wouldn't it radically change the "rule" that (x^a)' = a*x^(a-1) though if that definition of negative exponents didn't exist?

16:53:42 <MissPiggy> the other is where you differentiate 'formally', like it's just some kind of symbolic operation on syntax

16:55:05 <AnMaster> MissPiggy, I always distrust math that treats dx and dy as if you could treat them like a normal variable. For a start; they consist of more than one letter! ;P

16:55:22 <oklopol> formal differentiation is usually an operation defined for polynomials defined just like differentiation usually works for polynomials

16:58:04 <AnMaster> I highly distrust how integration by substitution due to the way it treats dx. Stuff like dx/dt=t' leading to dx=t'dt :/

16:59:07 <MissPiggy> if (x,y,z) is one coordinate system (u,v,w,...) is another, then you make a pullbacn

16:59:27 <AnMaster> MissPiggy, I have a test in a course about integration in two weeks time. Err make that integration and differential equations even.

17:00:06 <MissPiggy> and the idea is that you can transform forms like Adx+Bdy+Cdz into a du,dv,dw.. form

17:01:21 <AnMaster> MissPiggy, I don't read that much math when studying CS. At least not during the first year

17:02:48 <AnMaster> MissPiggy, well yes, I am aware of that it is possible to do integration in more than one variable. I don't know how however.

17:03:39 <MissPiggy> well theres this theorem that relates integration over a boundry to integration over the volume itsselt

17:03:39 <oklopol> AnMaster: if you have a function from an n-dimensional rectangle to reals, just integrate one axis at a time

17:04:05 <MissPiggy> it's all pretty nebulous and convoluted.. I'm still trying to figure it out myself

17:04:14 <oklopol> i mean integrate along one axis, and at each point integrate over the (n-1)-dimensional rectangle

17:05:28 <oklopol> if you wanna integrate a function from some more complex thing, you usually use substitution so you can integrate on a rectangle

17:06:05 <oklopol> fubini's theorem says you can integrate along the axes separately, and order matters not

17:06:08 <AnMaster> oklopol, I mean: do they go inside each other, instead of, say, being multiplied with each other or some other operation to combine them

17:08:28 <AnMaster> oklopol, oh? "often" as in "often in exams" or "often in real world applications"?

17:09:27 <oklopol> say you're integrating f(x, y) = x over [0,1]x[0,1], you'd have int_{x from 0 to 1}( int_{y from 0 to 1} x ), so you just get int_{x from 0 to 1} ( x ), because you're integrating the *constant* x over y

17:10:02 <oklopol> if you're integrating an expression that doesn't depend on y over variable y, then it's just multiplication

17:11:24 <fizzie> In real world you just integrate numerically and forgot all that symbol-manipulation nonsense. (Okay, so maybe not *quite*...)

17:11:31 <AnMaster> oklopol, also, as far as I have understood it, ∫(f(x)*g(x))dx can't be solved for _all_ f and g where both ∫f(x)dx and ∫g(x)dx can be solved. Except with numerical methods that is.

17:13:19 <AnMaster> oklopol, well, yes, I was so busy writing that line to be correct, I hadn't noticed any line after "<AnMaster> oklopol, oh? "often" as in [...]"

17:13:27 <oklopol> int_{y from a to b}( x ) is integrating a constant from a to b, so you just get (b - a)x

17:14:10 <oklopol> often the expression is only nontrivial to integrate over one axis (in homework problems that is :P)

17:14:51 <AnMaster> int_{y from a to b}( x ) <-- I can't say I'm familiar with that syntax. It looks like pseudo-latex though.

17:15:44 <AnMaster> oklopol, to be more specific: I'm unable to detect any dx or dy indicating which variable you are integrating to

17:17:55 <AnMaster> Deewiant, err wait... the x would still be there as well, no? wouldn't it be x*(b-a)*y

17:23:01 <oklopol> yeah i was confused, didn't see why it's relevant that the definite integral was indefinite

17:30:18 <AnMaster> wasn't it something like the integral of 1/x from 1 to inf went to infinity. But if you rotated the curve that is formed by that function around the x axis and integrated to find the volume of it, then it result in some finite number? But if you tried to find the area of that body, it went towards infinity

17:33:12 <oklopol> so obviously you'll be using much more paint toe paint it than to fill it, after a whi

17:35:37 <AnMaster> anyway, there are several creepy bits here: 1) that an integral from n to infinity can give a finite value (where n is a finite number). 2) that you get finite volume and infinite area.

17:36:55 <AnMaster> or functions that not only approach zero, but actually reach it and then stay there.

17:38:51 <AnMaster> oklopol, okay to be more exact: a function f(x) with the property that "f(x)>0 for all x" can (sometimes) when integrated from a finite number n to infinity have a finite integral

17:40:23 <oklopol> does it sound creepy that we can have an infinite set all of whose elements are positive, but for which there is such a real number r that for all finite subsets of our set, the sum of that set is less than r?

17:41:25 <AnMaster> ehird, hm? It seems to contradict intuition of reality. Yes I know that intuition is quite often wrong. Still results in a creepy feeling for some cases of it.

17:43:09 <AnMaster> oklopol, that way to express it is too abstract (to me at least) to visualise it.

17:44:18 <oklopol> and if you know anything about series, you can see this infinite amount of numbers can have such an upper bound

17:46:02 <AnMaster> oklopol, so you feel perfectly comfortable on all levels with the fact that an area A limited by two infinitely long sides can be finite?

17:47:04 <oklopol> AnMaster: sure, i even feel comfortable with defining "area" of that to be a frog

17:49:52 <AnMaster> oklopol, then how do you explain that finite real world and math areas seem quite often to match up?

17:50:32 <ehird> AnMaster: because we constructed them to be vaguely similar to the real world at first

17:52:04 <ehird> It does not exist physically, and abstract concepts do not really "exist" as such, they only exist insofar as operations on them.

17:52:13 <oklopol> but the geometry of our world isn't the same as R^n, it's just one approximation of it

17:52:16 <ehird> And the symbol manipulation was all invented by us. There's no inherent existence of mathematics.

17:54:29 <oklopol> MissPiggy: no one's saying mathematics isn't real, because that's not really a question, but according to modern physics we do not live in R^3, although a nice model of physics can be constructed by saying particles are points in R^3

17:55:31 <oklopol> i'm not all that comfortable with sets whose hausdorff dimension is not a natural number, they are usually really scary

17:57:56 <AnMaster> oklopol, also I'm no expert on fractals, not sure what you mean with definition of fractal here. The bit that defines a specific fractal?

17:59:22 <oklopol> AnMaster: hausdorff measures are a way to measure sizes of sets, just like jordan measures and lebesque measures, jordan being the simplest one; hausdorff measures take as argument the "dimension" of the set you're measuring, for instance if you draw a line in R^3, it's 1-dimensional measure can be finite, although it's 3d-measure is clearly 0

17:59:56 <AnMaster> I could think of two things: a) definition of a given fractal b) definition of what a fractal in general is.

18:00:17 <oklopol> the hausdorff dimension of a set is such a real number that the hausdorff measure of the set, with that dimension, is not zero or infinite

18:00:39 <oklopol> now fractals, afaik, are defined as sets whose hausdorff dimension is not a natural number

18:02:20 <oklopol> so what i'm saying is i'm comfortable with drawing things recursively, but sure, some complex sets are pretty scary

18:02:27 <AnMaster> well yes recursive algorithms is the most common way to define a fractal that I have seen

18:03:03 <oklopol> so everything is a fractal that can be computed using recursion, or what exactly?

18:04:37 <oklopol> what do you mean, you knew we can embed k-dimensional objects in n-dimentional space?

18:05:47 <AnMaster> also, what ehird said about common creepyness above: by that logic complex numbers should be creepy. But they aren't IMO

18:07:04 <AnMaster> <oklopol> what do you mean, you knew we can embed k-dimensional objects in n-dimentional space? <-- I knew that fractals had a non-natural number dimension.

18:10:04 <AnMaster> oklopol, well that includes things that aren't fractal clearly. Such as: f(x,y) = draw a straight line of length 1 jonined up to f(x+1,y)

18:10:39 <AnMaster> which, while recursive, would give you a straight line starting at a given point and then going on forever

18:11:46 <oklopol> the sexiest thing about hausdorff dimensions is you don't have need to be working with real numbers

18:11:55 <AnMaster> oklopol, what about requiring more operations for each step (alt: you recurse more than once at a given level)

18:13:26 <AnMaster> like "f(L) = divide the line L in 3, remove middle, call the other two L1 and L2, f(L1), f(L2)"

18:15:32 <oklopol> all the cs's are homeomorphic (the ones obtained by different sorts of splits into three parts), but some leave you with zero measure, some have finite

18:16:52 <AnMaster> also: "<oklopol> koch snowflake" <-- that's the one you add in a triangle (well, two sides of one) in the middle, right?

18:16:53 <oklopol> i don't know if the hausdorff dimension goes down and measure goes up for some splits, you'd have to ask someone who actually know about this stuff

18:17:59 <ehird> "Bona fide elements of ∅ are hard to come by, so we may safely offer to exchange them for anything you might care to want: as you will be paying with bogus currency, you cannot object to our shoddy merchandise."

18:20:46 <ehird> The purpose of this paper is not only self-citation (McBride, 2001; McBride & Paterson, 2006), ...

19:22:22 <augur> "Joachim Lambek proposed the first noncommutative logic in his 1958 paper Mathematics of Sentence Structure to model the combinatory possibilities of the syntax of natural languages. His calculus has thus become one of the fundamental formalisms of computational linguistics."

19:24:37 <alise> augur: what's your evidence that fax is a girl? my evidence that e is male is: one, probability; the vast majority of this channel is male - in fact, I believe there are no females currently in here, and a vague recollection of some sort of data meaning he was male, but my memory is terribly fuzzy when it comes to this place; so much talk, so little time.

19:26:23 <augur> all i know is that fax/soupdragon/misspiggy is smart and interested in CS and linguistics

19:30:08 <alise> i think i'm going to stick with this name for a while, see how many people treat me differently because they think i have ovaries

19:31:10 <alise> so I was thinking about what to call the empty type, right, and I thought hey, I could use ∅ *and* have it be used by sequence/collection/whatever. I just have to make Set (or Type or whatever) an instance of it! But that won't work, because there'll be operations like cons :: a -> sequence a -> sequence a which doesn't make sense because one, sets/types don't have element types

19:35:26 <alise> augur: don't get me wrong, I don't care about total mathematical notation faithfulness

19:48:19 <alise> pikhq: but I don't want to use _ for it because you should be able to use that in names

19:53:05 <Asztal> cheater3: you also need a good font or an IRC client that does font substitution properly

19:53:59 <gm|lap> i saw: interrobang, a/c, some weird p, some weirder H, Rs, 'a, 'o, 'i, 'u, 'e, mu.

19:57:38 <pikhq> gm|lap: Yeah, X11 makes a best-effort to display everything, even if it is ugly as hell.

19:59:11 <alise> normally i run os x, which you can criticise for many reasons but excellent display of unicode text is not one of them

20:06:33 <alise> G = 1000 is standard; you cannot change prefixes. the unit after a prefix cannot change a prefix; that is merely nonsensical. Furthermore, the decimal, standard version is in fact *more common* in computing than the binary one.

20:07:01 <alise> Ki/Gi/Ti are the standard binary prefixes; it should be RAM, which is the main exception to the decimal rule, whose marketing changes.

20:07:50 <gm|lap> The 2.4GHz band which wireless ethernet operates within lies... between 2.4 x 10^9 and 2.5 x 10^9 Hz <-- likewise, not a byte.

20:08:30 <alise> complaining about hard-drive makers using SI prefixes is the wonderful domain of idiots who like to appear smarmy and pedantic without actually caring about being correct.

20:08:48 <alise> "Hard drive prices are determined almost entirely by competition between manufacturers, so if hard drives were labelled in GiB instead of being labelled in GB, we'd be paying the same number of dollars for the same number of bytes anyway — if this really was a global conspiracy, it would be one of the dumbest conspiracies ever."

20:09:09 <pikhq> gm|lap: I will agree with you in one thing, though -- hard drives should be labelled in GiB.

20:12:26 <alise> we should replace the ehird sighting in the topic with scarf sitings. anyone seen him recently?

20:29:17 <alise> your solution to the expression problem, what if your type doesn't have any relevant dependicity? do you have to like put a dummy dependent thingy in to make it work?

20:38:17 <alise> use haskell notation like you've been doing but with (name::t)-style dependent type notation plz :P

20:40:56 <alise> cons takes a value of type Snoc f named xs, and a value of type (f xs) named x, and returns a Snoc f.

20:42:25 <alise> If you can formulate a type meaning "the integer x", you could have snoc nil 1, snoc (snoc nil 1) 2, etc. type

20:43:23 <MissPiggy> so when you snoc a ROW on, it computes the number of elements you have to define, to add this row (and col similarly)

20:44:03 <MissPiggy> at a first approximation that matrix could just have numbers in it, or whatever -- it doesn't really matter

20:44:26 <MissPiggy> to solve the expression problem we will have to compute the type of the cell based on the function spec.

20:48:49 <alise> + func1 | func2 | ... Foo x y | y | x ... Bar x y | x | y ... +-----------------...

20:49:24 <alise> [20:43] <MissPiggy> so when you snoc a ROW on, it computes the number of elements you have to define, to add this row (and col similarly) i don't get what you mean by that

20:52:29 <MissPiggy> suppose we wanted to define functions, eval, size and show on data Exp = Num Int | Add Exp Exp | Mul Exp Exp

20:57:24 <alise> MissPiggy: think I should have inductively defined sets as in mathematical notation?

20:57:44 <MissPiggy> you start with the 0x0 matrix, [] `snoc` ROW "Num"*description of num () `snoc` Row "Add*description of add ()`snoc`COL eval (case for eval Num, case for eval Add)`snoc`ROW "Mul"*description of mul (case for eval Mul)`snoc`COL show (implementation of show for all 3 casese..)

21:01:48 <MissPiggy> we are actually making a program over a generic sort of datatype called a universe

21:05:01 <alise> [20:57] <MissPiggy> you start with the 0x0 matrix, [] `snoc` ROW "Num"*description of num () `snoc` Row "Add*description of add ()`snoc`COL eval (case for eval Num, case for eval Add)`snoc`ROW "Mul"*description of mul (case for eval Mul)`snoc`COL show (implementation of show for all 3 casese..)

21:05:22 <MissPiggy> I'm starting to realize that my idea takes quite a bit of background to understand..

21:06:25 <alise> If I add a row, and then call func1 or func2 on it, they don't work; they explode and break.

21:06:46 <alise> In the OOP system, which can add rows, they inherit the definition (and you cannot remove fields, so they must work)

21:07:24 <MissPiggy> you can add N-rows and M-columns in any order, but at the end of the day you will have definede NxM cells of a matrix

21:07:45 <alise> it's a good solution, but i can't help thinking that it should really be a language feature, not something added on

21:08:09 <MissPiggy> alise yeah it'll be awkward as fuck in Coq but I bet you could make easy as pi in epigram

21:16:34 <alise> if you have a function that's the composition of two columns, it doesn't need to be a column

21:16:52 <alise> in functional programming you don't have to distinguish columnular and non-columnular functions

21:18:13 <MissPiggy> so t1's type would express that it defines N-functions over some (M-constructor'd) datatype

21:18:44 <alise> you can define a new row, and when defining the columns for that row, put in some evil code that breaks the assumptions, and the abstraction, of code using the column

21:20:31 <alise> I do think http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq is remarkably elegant though

21:22:30 * alise tries to translate http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq into Haskell, through whatever tricks necessary

21:32:38 <AnMaster> (theory: it takes as long to go back in time as it took to get to the current point from then originally)

21:36:57 <MissPiggy> a lot of people that got fed up with C++ because they couldn't push template metahacking it far enough moved to haskell

21:37:23 <alise> a lot of people that got fed up with Haskell because they couldn't push type-system metahacking it far enough moved to Epigram

21:40:34 <alise> first of all, the toolchain situation is hopeless; really terribly hopeless. you have no idea how hard it is just to get a working D compiler. D2 with all the fancy features? Forget it.

21:45:01 * Sgeo wonders what it would be like to take a computer course where he's not guaranteed an A

21:48:14 <Sgeo> MissPiggy, I _think_ alise is saying I should switch schools in order to actually get challenging classes

21:48:51 <alise> Well, if you're basically guaranteed an A in every class you're either a really excellent programmer or in a bad school.

21:49:16 <alise> You may be a really excellent programmer, but the probabilities are weighted in the direction of bad school.

21:54:34 <alise> MissPiggy: do you have any idea how many times i've seen the word "kind mismatch" in the past few minutes

22:11:45 <oklopol> Sgeo: my average in math is still A (called 5 here), recently thought i'd failed my first exam (apparently i just failed by my own standards), and it mostly felt nice to know the pressure to succeed every time was lifted.

22:14:45 <oklopol> then it'd probably feel nice, since taking trivial courses feels is a waste of time

22:18:52 <alise> MissPiggy: btw if you separate classes from their methods, and make methods functions, you almost get the table solution

22:21:16 <alise> well if you make a subclass you're not obligated to extend the previous functions to handle it unless you explicitly specify that

22:22:29 <alise> I decided to see if people would treat me differently if they believed I had ovaries

22:22:57 <alise> since this is basically the only channel I go in and #haskell is very noisy, this is not such a successful experiment

22:25:29 <oklopol> i want to have sex with every girl i see both online and irl (necessary and sufficient condition for being male), but usually i only show it on irc, because as we all know it's really funny.

22:29:32 <alise> MissPiggy: anyway do you think Complex :: Set; Complex = {_+i_ m n | m ← Real, n ← Real} is good notation for set construction?

22:44:49 <ehird> 14:23:25 <coppro> I don't think I behave any different towards women on the internet

22:58:42 <Sgeo> "\x41jax\x20\x63allba\x63\x6b er\x72\157\x72\x3a s\x6f\x75rce\x20url n\x6ft foun\x64\041\x20\012\x0d\012\x0dPlea\x73e ver\x69fy i\x66 y\x6fu ar\x65 usi\x6eg an\x79 URL\x2drew\x72itin\x67 co\x64e a\x6ed s\x65t \x74he \x41jax\x55rl\x20pro\x70er\x74y t\x6f m\x61t\x63h\x20th\x65 U\x52L \x79ou\x20ne\x65d."

22:59:33 <ehird> MissPiggy: so do you think quantified types should make the type of the function a type-level function from a set to a set, or have it be an implicit parameter of the function?

23:09:26 <coppro> I should clarify; I will treat someone I am familiar with differently depending on their personality, including sex and gender. By default, however, I don't make any attempt to distinguish between the two.

23:13:09 <coppro> but unless I have a particular reason to do so, I don't associate gender with someone over the internet

23:24:08 <oklopol> because i can write things like "integrate (-1/(e^(a-t+i*pi)-1)) with respect to t" and just know it understands what i mean

23:24:51 <oklopol> i don't think it's ever misinterpreted me, even though i just write like i would to a human

23:25:13 <oklopol> i'm not saying it's actually that great a parser, it's just others are incredibly stupid.

23:28:44 <ehird> it's 1.5 million lines of mathematica, so i assume it's just a list of hardcoded query * response pairs.

23:29:23 <oklopol> it's mostly the i and pi sort of simple stuff that i love i don't always have to explain to it, "(-1/(e^(a-t+ipi)-1))" works as well