00:02:52 -!- adu has quit (Quit: adu).
01:15:46 -!- FreeFull has quit (Ping timeout: 240 seconds).
01:26:15 <oerjan> that's not very generally true.
01:27:39 <shachaf> it's only moderately generally true?
01:28:56 <oerjan> well it's true for a small, but important set of functions.
01:29:45 <shachaf> please explain and expand twh
01:30:35 -!- Phantom_Hoover has quit (Ping timeout: 276 seconds).
01:31:14 <tswett> learn hth is short for "hang that heretic".
01:31:15 <shachaf> oerjan: i'm glad we have an expert here to explicate an express answer
01:31:37 <tswett> oerjan is quite the exponent of mathematics.
01:31:39 <oerjan> tswett: hey don't reveal my secrets tdnh
01:32:33 * oerjan trying to remember the elegant proof of that fact he learned in differential equations class (maybe)
01:32:45 <tswett> twh = "that wicked heretic!"
01:32:57 <shachaf> oerjan is such an expert that e, to the xth degree, explodes with these expressions
01:33:14 <tswett> tdnh = "that demonic, nasty heretic!"
01:35:01 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: foolishness: not found
01:35:05 <shachaf> oerjan: come on, not even a poke from the flypoker?
01:35:21 -!- adu has joined.
01:38:38 <tswett> It's obvious what "btw" stands for.
01:40:06 <oerjan> d(exp(-x) * y)/dx = exp(-x) * dy/dx - exp(-x) * y = 0 => exp(-x) * y = C
01:42:32 <oerjan> shachaf: i consider those alliterations, not puns. no poke, hth
01:44:09 <oerjan> <tswett> It's obvious what "btw" stands for. <-- obviously. btw do you happen to weigh more or less than a duck twh
01:44:57 <oerjan> `learn btw is short for "burn the witch".
01:45:00 <HackEgo> Learned 'btw': btw is short for "burn the witch".
01:46:28 * oerjan recalls his mother couldn't visit swimming pools because she sank like a stone. so i guess she wasn't a witch, despite all the divinations.
01:47:21 <oerjan> or well, something like that.
01:47:31 <HackEgo> Learned 'btw': btw is short for "bury the weasel"
01:47:52 <oerjan> hppavilion[1]: excuse me, you are ruining tswett's joke tdnh
01:48:48 <oerjan> also, if you thought that when omgroflmaoing, i'm wondering about your sense of humor.
01:49:02 <hppavilion[1]> ("as a matter of fact, that did help and you just can't tell")
01:49:24 <oerjan> hey i was just getting to the a
01:49:40 <hppavilion[1]> oerjan: When I said "omgroflmao", I wanted him to decrypt it xD
01:51:20 <hppavilion[1]> Imma make a programming language entirely like all known programming languages
01:52:20 <hppavilion[1]> But I started the message with a slash forgetting that that commands it
01:53:45 <hppavilion[1]> oerjan: A language following the philosophy of intercal, but that includes INTERCAL in what it wants to avoid
01:54:05 <hppavilion[1]> oerjan: Also, it has some modern languages (e.g. PROLOG and Haskell and Python) in mind in its design
01:54:17 <hppavilion[1]> oerjan: So it's derived from taking that and not being like it
01:55:51 <oerjan> hppavilion[1]: um in that case i think you mistyped your original sentence because it clearly says "like" hth
01:56:25 <oerjan> i thought it was more interesting with "like" somehow
01:56:26 <hppavilion[1]> oerjan: But "entirely like" is also a good idea for a language
01:56:40 <hppavilion[1]> oerjan: Yes, I can see how that idea would be interesting.
01:56:41 <oerjan> i mean, intercal is already done.
01:57:50 <hppavilion[1]> This is like the Wishbone of esoprogramming- adapting a classic to those who grew up on more "modern" material
02:16:56 <hppavilion[1]> Delabel is written #'labelname' or something like that
02:17:19 <hppavilion[1]> Delabel JUMPs within the AST (so more complicated than an ASM jump) to the DELABEL
02:18:24 <hppavilion[1]> Then, the exit code is produced from the earlier $'labelname' subexpression
02:19:35 -!- adu has quit (Quit: adu).
02:22:03 <hppavilion[1]> Possibly, another kind of label that behaves like this: (5{'lab'}-1)+('lab'#0)
02:28:02 -!- adu has joined.
02:33:13 <hppavilion[1]> And the languages use a persistent interpreter that uses previous languages to mess with newer languages
02:33:29 <coppro> how about a language where every program is a polyglot
02:33:37 <coppro> except function calls must be from one language to the other
02:52:54 -!- pdxleif has quit (Ping timeout: 246 seconds).
02:53:47 -!- pdxleif has joined.
03:01:24 -!- mauris has joined.
03:06:33 -!- copumpkin has joined.
03:11:24 -!- mauris has quit (Ping timeout: 255 seconds).
03:17:28 -!- hppavilion[2] has joined.
03:18:40 -!- FreeFull has joined.
03:19:36 -!- mauris has joined.
03:20:54 -!- lleu has quit (Read error: Connection reset by peer).
03:21:31 -!- hppavilion[1] has quit (Ping timeout: 265 seconds).
03:34:34 -!- tjt263 has quit (Ping timeout: 265 seconds).
03:58:56 -!- rifter_ has joined.
04:00:12 -!- rifter has quit (Ping timeout: 264 seconds).
04:01:12 -!- rifter__ has joined.
04:05:12 -!- rifter_ has quit (Ping timeout: 256 seconds).
04:12:06 -!- adu has quit (Quit: adu).
04:12:59 -!- copumpkin has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz…).
04:15:53 -!- adu has joined.
04:44:31 <myname> hppavilion[2]: are you familiar with call/cc?
04:45:44 <shachaf> i,i call/cc-with-current-continuation
04:54:34 -!- rifter__ has quit (Quit: Leaving).
04:54:53 -!- rifter has joined.
05:00:45 <adu> (call/cc call/cc)
05:01:01 <adu> oops did I just break everything?
05:02:42 <oerjan> adu: no, that's fine see https://esolangs.org/wiki/Subtle_cough
05:03:20 <oerjan> it's ((call/cc call/cc) (call/cc call/cc)) you need to watch out for.
05:34:41 <adu> oerjan: *mind blown*
05:49:49 * zgrep slowly collects all the pieces of adu's mind and glues them back together, because somebody has to
05:50:15 <oerjan> thank god i was afraid i'd have to do it
05:50:32 <zgrep> I got you covered... for now.
05:53:26 -!- atslash has quit (Ping timeout: 256 seconds).
05:53:54 -!- atslash has joined.
05:56:08 <adu> zgrep: thanks :)
05:56:21 * adu feels better, now
06:02:17 <adu> hppavilion[2]!
06:02:24 -!- hppavilion[2] has changed nick to hppavilion[1].
06:02:30 <adu> hppavilion[1]!
06:02:42 <adu> I don't know anymore
06:02:58 <myname> i'd say it's pretty close
06:03:01 <hppavilion[1]> adu: I'm making a language entirely like all known languages, INCLUDING Intercal
06:03:18 <adu> is that wise?
06:03:49 <zgrep> How about wise domes?
06:04:09 <hppavilion[1]> zgrep: Ah, those should really be called "Wise Spheres"
06:04:26 <zgrep> Oh, half of them are simply underground?
06:04:30 <hppavilion[1]> zgrep: They encircle the entirety of the area, really. Not just the top
06:04:32 <adu> Well, I've been learning boring Python
06:04:35 <adu> https://github.com/andydude/tetration/blob/gh-pages/dl/superroot_3.ipynb
06:05:00 <hppavilion[1]> zgrep: Good for keeping the wisdom sealed in and fresh
06:05:18 <hppavilion[1]> adu: Would you like me to offer my trign code? Good for negative hyperoperations
06:05:26 <zgrep> hppavilion[1]: I thought you said no wisdom, only `wisdom?
06:05:35 <adu> hppavilion[1]: sure
06:05:57 <hppavilion[1]> adu: To be clear, "trigns" are numbers with three signs
06:06:32 * zgrep wouldn't mind knowing how to figure out what "trign code that is good for negative hyperoperations" means...
06:06:54 <adu> zgrep: start here: https://en.wikipedia.org/wiki/Hyperoperation
06:08:12 <adu> hppavilion[1]: I think I made my point last time
06:08:42 <hppavilion[1]> adu: They make negative hyperoperations logical and complete
06:08:51 <adu> hppavilion[1]: well, they would have to be perpendicular with each other, obviously
06:08:54 <hppavilion[1]> adu: Also, I don't remember your point from last time
06:09:43 <adu> my point was this: there are 3 sequences of binary operations: hyperN, hyperNlog, hyperNroot
06:10:13 <hppavilion[1]> And we can just use a piecewise function that amalgamates those together
06:10:21 <adu> and to try and make these 3 sequences into a single sequence indexed by esoteric numbers, is well, too esoteric for my tastes
06:11:18 <hppavilion[1]> adu: It's not much more eso than Imaginary Numbers, IMHO
06:12:07 -!- andrew has joined.
06:12:10 <vodkode> What is with this 'flat earth' stuff being the new thing?
06:12:32 -!- andrew__ has joined.
06:12:53 <hppavilion[1]> vodkode: That trend isn't too recent, at least in internet time
06:13:25 <vodkode> it's rocketed waaaay up in 2015 from what I can tell, tons upon tons of YT videos and people debating it (as if its a debate)
06:13:40 <vodkode> I have no clue what the catalyst is for this kind of nonsense
06:14:14 <hppavilion[1]> Which could be some complex metaphor I don't know about
06:16:03 <hppavilion[1]> adu: Out of curiosity, is there some logical way to do log the same way root(x, n) = x**(1/n)?
06:17:58 <hppavilion[1]> If there is, then my "trign" idea could probably be justified by lining up the trigns' properties with the relationship between them
06:18:58 <hppavilion[1]> adu: Perhaps we should turn attention away from the reals for a bit and look to the positive Gaussians
06:19:05 <mauris> well, log(x, n) = ln(x) / ln(n)
06:20:08 <hppavilion[1]> mauris: But is there any relationship with root and pow?
06:21:27 <mauris> not really! you might be thinking: root/pow form a pair the way exp/log do
06:21:50 <mauris> but while root is really a special case of pow (where the exponent is a fraction like you mentioned) that isn't true for exp/log.
06:22:01 <mauris> so there isn't a way to write one in terms of the other
06:27:02 <mauris> i guess it's a matter of perspective
06:27:04 <mauris> root-like functions are inverses of f(x) = x^n for some n
06:27:10 <mauris> log-like functions are inverses of f(x) = n^x for some n
06:28:01 <adu> hppavilion[1]: "to do log the same way"?
06:29:47 <hppavilion[1]> adu: The same way root is exponentiation to the reciprocal
06:34:51 -!- mauris has quit (Ping timeout: 265 seconds).
06:36:18 <hppavilion[1]> Are there any other kinds of call/<x> besides call/cc and call/em?
06:37:05 <adu> hppavilion[1]: theres the power series
06:37:27 <hppavilion[1]> You weren't referring to that question, where you xD
06:37:58 <adu> log(x) = sum((-1)^(n + 1)*(x - 1)^n/n, n=1..infinity)
06:40:03 <adu> or, my favorite, -log(1 - x) = sum(x^n/n, n=1..infinity)
06:42:02 <adu> theres also the indefinite integral
06:43:05 <adu> log(x) = ∫dx/x
07:04:06 <hppavilion[1]> Is there somewhere online I can find a massive database of the curry-howard correspondence?
07:37:12 -!- hppavilion[1] has quit (Ping timeout: 265 seconds).
07:46:18 -!- hppavilion[1] has joined.
07:47:38 -!- andrew__ has quit (Ping timeout: 250 seconds).
07:48:04 -!- andrew has quit (Ping timeout: 250 seconds).
07:48:39 <hppavilion[1]> Could we roll Set Theory into Curry/Howard/Lambek on the grounds that a set can be represented as a bitstring where each bit corresponds to an item's presence in said set relative to the "universe", and since bitstrings support logical connectives naturally?
07:53:50 -!- mroman has joined.
08:00:12 -!- hppavilion[1] has quit (Ping timeout: 250 seconds).
08:12:08 -!- jaboja64 has joined.
08:18:32 -!- adu has quit (Quit: adu).
09:18:18 -!- EgoBot has quit (Read error: Connection reset by peer).
09:19:06 -!- Gregor has quit (Ping timeout: 240 seconds).
09:19:20 -!- FireFly has quit (Ping timeout: 245 seconds).
09:19:22 -!- EgoBot has joined.
09:20:15 -!- Gregor has joined.
09:21:13 -!- FireFly has joined.
09:32:03 <oerjan> ah the style change on aaronson's blog was something stupid wordpress did
09:37:54 -!- rifter_ has joined.
09:38:55 -!- rifter has quit (Ping timeout: 245 seconds).
09:39:13 -!- rifter__ has joined.
09:43:11 -!- rifter has joined.
09:43:17 -!- rifter_ has quit (Ping timeout: 276 seconds).
09:43:50 -!- rifter__ has quit (Ping timeout: 265 seconds).
09:56:02 -!- andrew__ has joined.
10:12:33 <fungot> b_jonas: also sure you won't do concurrent befunge? fizzie has managed to make a stack based imperative one, 1 pushes 1, 2
10:31:50 <Taneb> Galois Theory: why the shape of the football makes solving polynomials harder
10:33:49 -!- oerjan has quit (Quit: Nite).
10:44:37 -!- ocharles has joined.
10:44:39 -!- ocharles has changed nick to Guest11957.
10:45:15 -!- Guest11957 has quit (Changing host).
10:45:15 -!- Guest11957 has joined.
10:45:23 -!- Guest11957 has changed nick to ocharles_.
10:46:37 -!- andrew has joined.
10:59:00 -!- ais523 has joined.
11:29:55 -!- boily has joined.
11:30:18 <HackEgo> bdsm/BDSM definitely isn't a kind of LARP and Taneb definitely did not invent it.
11:31:15 -!- rifter has quit (Quit: Leaving).
11:33:39 <int-e> `culprits wisdom/bdsm
11:33:42 <HackEgo> int-e ais523 oerjan elliott Taneb Taneb
11:38:08 <int-e> <Taneb> `learn BDSM is just a kind of LARP <HackEgo> I knew that. <kmc> c.c <Taneb> Please do not say that I invented it
11:44:12 <boily> Taneb: Tanelle. mwah ah ah.
11:47:20 <fizzie> "We have tried to send you this email as HTML (pictures and words) but it wasn’t possible. In order for you to see what we had hoped to show you please click here to view online in your browser: --"
11:47:29 <fizzie> Well, that's one way to convert your text/html emails to text/plain.
11:47:57 <fizzie> `learn HTML is just pictures and words.
11:48:01 <HackEgo> Learned 'html': HTML is just pictures and words.
11:49:24 -!- jaboja64 has quit (Ping timeout: 264 seconds).
11:50:41 -!- ais523 has quit.
11:51:01 -!- ais523 has joined.
11:54:38 <b_jonas> `learn links are one of the very few HTML renderers that don't try to store a full document tree with heavyweight objects for each node just in case javascript wants to modify it later, so it's the only engine that can render those HTMLs that are automatically converted from a PDF and put each letter to a separate element.
11:54:41 <HackEgo> Learned 'link': links are one of the very few HTML renderers that don't try to store a full document tree with heavyweight objects for each node just in case javascript wants to modify it later, so it's the only engine that can render those HTMLs that are automatically converted from a PDF and put each letter to a separate element.
11:55:07 <HackEgo> links are one of the very few HTML renderers that don't try to store a full document tree with heavyweight objects for each node just in case javascript wants to modify it later, so it's the only engine that can render those HTMLs that are automatically converted from a PDF and put each letter to a separate element.
12:08:21 <boily> there is such a thing as... aaargh. ow. no. a PDF converter that put individual letters into tens of tens of thousands of millions of elements?
12:08:29 <boily> even for something that involves PDFs, that's low!
12:10:09 <b_jonas> boily: no, mostly they just put every word into an element, or each part of the word separated by kerns, so basically they put an element anywhere TeX emits a glue to the DVI
12:10:26 <b_jonas> Putting every letter to a separate element is much rarer.
12:14:09 -!- J_Arcane has quit (Ping timeout: 265 seconds).
12:16:32 <ais523> b_jonas: I have a PDF-to-other-formats converter, it genuinely does use an element per letter when converting to HTML
12:16:41 <ais523> in order to get the layout on the page exactly the same
12:16:44 <ais523> this makes it mostly useless
12:18:37 -!- J_Arcane has joined.
12:19:23 <HackEgo> BDSM definitely isn't a kind of LARP and Taneb definitely did not invent it.
12:20:19 -!- boily has quit (Quit: COCOCONUT CHICKEN).
12:22:39 <b_jonas> Would a sorcery with the exact ability of Safe Passage costing {WW} be overpowered?
12:23:58 <b_jonas> ais523: the heavyweight elements is the main reason why I hate SVG used as a general vector format, as opposed to PDF. SVG basically _forces_ you to make vector drawings with tons of heavy objects.
12:25:34 <b_jonas> There's canvas of course, which doesn't do that, but canvas is worse than postscript in that documents using it need a full interpreter of a general purpose language and the document can have lots of unintended side effects besides drawing that you have to be careful about.
12:27:30 -!- mauris has joined.
12:28:20 <fizzie> The "need a full interpreter of a general purpose language" part doesn't sound that different from PostScript.
12:29:14 <fizzie> (Windows Metafiles to the rescue?)
12:30:31 -!- jaboja64 has joined.
12:37:09 -!- mauris has quit (Read error: Connection reset by peer).
12:43:59 -!- jaboja64 has quit (Ping timeout: 276 seconds).
12:48:50 -!- ais523 has quit.
12:48:51 -!- callforjudgement has joined.
12:48:57 -!- callforjudgement has changed nick to ais523.
12:59:52 <tswett> A language unlike all other programming languages, eh?
12:59:58 <tswett> That's what I tend to go for with my languages.
13:00:14 <tswett> Proce is the one that comes to mind.
13:01:19 -!- andrew__ has quit (Remote host closed the connection).
13:01:20 -!- andrew has quit (Remote host closed the connection).
13:03:19 <tswett> Proce as currently defined might be broken, allowing you to take advantage of discretization artifacts.
13:07:41 -!- mauris has joined.
13:08:46 -!- ais523 has quit (Ping timeout: 265 seconds).
13:09:27 <b_jonas> fizzie: the sandbox for postscript is better. canvas requires a full browser, with lots of information leaks and stuff.
13:29:06 <mroman> does it put each letter into a span or what?
13:29:16 <mroman> also the HTML file will be huge then :)
13:29:34 <mroman> > length $ "<span></span>"
13:29:43 <mroman> that's at least 14 bytes per letter
13:30:04 <mroman> that's pretty much as terrible as my image to html converter
13:30:24 <mroman> http://mroman.ch/output.html
13:30:27 <mroman> but at least it looks good :D
13:31:29 <mroman> although that one has RLE and color reduction turned on
13:31:36 <mroman> so it's not too bad as far as size goes
13:32:28 <Taneb> mroman, could you get that down using a colour pallete and CSS?
13:33:10 <mroman> but that would be a nice step to take
13:33:39 <mroman> the good thing is that this way I can send dick pics to people without having them detected
13:34:00 <mroman> also google image search will never index my pics
13:35:56 <mroman> no that online version has no colour reduction apparentely
13:36:12 <mroman> let me look on my disc
13:38:53 <b_jonas> mroman: hehe, I've seen images drawn with tables, but only smaller ones, up to 64x64 pixels or something.
13:40:12 <b_jonas> mroman: and the "14 bytes per letter" is missing the point. the bytes aren't the heavy cost, the in-memory heavy objects with tons of properties is. and they're not easy to avoid in current html renderers because javascript can modify anything after which the page has to be re-rendered.
13:40:40 <b_jonas> even without javascript, CSS can do some fancy things to change the page when you modify the width of the browser or you scroll or something.
13:41:18 <mroman> > 1748859 / 1024 / 1024
13:41:32 <mroman> that output.html is 1.6MB apparentely
13:43:15 <mroman> http://mroman.ch/output_reduced.html <- this is way smaller
13:43:22 <mroman> although the decrease in quality is noticable
13:43:42 <mroman> but I haven't tested it with dick pics yet so ...
13:43:46 <mroman> it might still serve the purpose
13:46:32 <mroman> that would shave off 60kb
13:47:25 <mroman> maybe background can be replaced with bg
13:51:44 <mroman> http://mroman.ch/mandel.html
13:55:09 <b_jonas> mroman: if there are repeated colors and/or widths, you could reduce stuff with classes instead of inline style I think.
14:12:50 -!- mauris has quit (Read error: Connection reset by peer).
14:15:36 <mroman> i'm using rle for width
14:16:17 <mroman> if a color is repeated I just increase the width
14:17:16 <mroman> but you mean like .f { background:#...; width:5px; }?
14:18:04 -!- mauris has joined.
14:21:35 <b_jonas> mroman: possibly, but probably more like sepraate classes for background and width
14:23:07 <b_jonas> eg <style thingy>.f { background: lime } .g { width: 5px }</style> and later <b class="f g"/>
14:37:55 <fizzie> "Please my dear the entire supreme court Of Ecowas Benin Republic are here to make it clear to you that there was a case that was been handling in this Ecowas since January 5th 2015 concerning your funds because we got some reports that you did not received your funds since after every stories you heard regarding the funds and all type of payments you have be paid to receive the funds but none ...
14:38:01 <fizzie> ... is received by you."
14:38:04 <fizzie> Man, that's a long sentence.
14:40:26 <b_jonas> fungot, Please my dear the entire supreme court Of Ecowas Benin Republic are here to make it clear to you that there was a case that was been handling your funds.
14:40:27 <fungot> b_jonas: i haskell, i have some
14:42:06 <mroman> fungot: turn down for what?
14:42:07 <fungot> mroman: i've already seen multiple in the block i live in connecticut. the hills were young."
14:42:16 <fungot> mroman: so a good alternative name for the procedure
15:09:47 <coppro> fizzie: can we implement a fungot module for that
15:09:47 <fungot> coppro: ther smerdy startin again? it seems to dtrt. i'm going to
15:10:44 <zgrep> fungot: Why are you?
15:10:44 <fungot> zgrep: if my memory serves me well enough to do it
15:10:52 <zgrep> Apparently it doesn't.
15:19:10 -!- spiette has joined.
15:20:41 <b_jonas> Oh, great, OGW prints a Turn to Frog variant for just {U}
15:50:31 -!- tjt263 has joined.
15:56:42 <b_jonas> No, more for creatures with annoying abilities
16:09:27 -!- Lord_of_Life has quit (Excess Flood).
16:12:06 -!- Lord_of_Life has joined.
16:21:13 -!- AnotherTest has joined.
16:48:33 -!- Phantom_Hoover has joined.
16:52:18 -!- mroman has quit (Quit: Lost terminal).
16:53:01 -!- MoALTz has quit (Quit: Leaving).
16:55:08 -!- TieSoul has joined.
17:00:17 -!- J_Arcane has quit (Ping timeout: 265 seconds).
17:12:00 <Taneb> One of my lecturers just used the term "quadrupleton set"
17:14:00 <Taneb> "Me and lambda have a history"
17:14:52 <int-e> `? lambda calculus
17:14:52 <HackEgo> lambda calculus? ¯\(°_o)/¯
17:19:08 -!- MoALTz has joined.
17:20:15 -!- AnotherTest has quit (Quit: ZNC - http://znc.in).
17:22:00 <Taneb> I didn't know Effi's did waffle
17:22:12 <Taneb> I presume that's referring to the pizza takeaway in York?
17:23:54 -!- jaboja has joined.
17:24:00 * int-e was just looking for a name with "ffi".
17:25:29 <int-e> (Actually I thought of Effi Briest for some reason... perhaps I should read the book to see what it's about.)
17:26:09 <int-e> But I suspect that waffles don't feature prominently in that story.
17:36:21 -!- AlexR42 has joined.
17:50:56 -!- AlexR42 has quit (Quit: My Mac has gone to sleep. ZZZzzz…).
17:54:00 -!- oren has joined.
17:57:09 <oren> @tell \oren\ don't forget about the RS-20
17:59:15 <izabera> alan rickman died of cancer
18:00:47 <oren> no idea who that is
18:01:53 <oren> oh. he was a great actor
18:06:11 <myname> i wonder how many mange readers are in here
18:09:01 <myname> do you have recommendations that aren't kinda obvious?
18:10:52 <oren> for what genre
18:11:50 <myname> preferibly slice of life/character developing. just read bitter virgin and am reading aku no hana right now
18:16:41 -!- jaboja has quit (Remote host closed the connection).
18:18:10 <oren> Hmm. The ones i've read that aren't all that popular afaik are the manga of ARIA (Kozue Amano).
18:20:40 <oren> Also Kimi ni todoke
18:36:26 <Phantom_Hoover> izabera, it's a bad week to be a 69-year old with cancer
18:37:28 -!- AlexR42 has joined.
18:53:35 -!- oren has quit (Quit: Page closed).
19:22:54 -!- hppavilion[1] has joined.
19:32:08 -!- AlexR42 has quit (Quit: My Mac has gone to sleep. ZZZzzz…).
19:36:36 <mauris> (functions from p to a type that contains *no values at all*)
19:37:42 <hppavilion[1]> mauris: And &? Wiki gives me the product type, so tuples
19:37:46 <mauris> if p is empty (false), the type is inhabited (by the empty function that maps nothing to nothing), but as soon as p is inhabited (true), we need to map from some p value to something in codomain, but there's no way to pick anything, so p -> Void can't be inhabited.
19:38:35 <hppavilion[1]> Which is, in haskell if that's correct, (P, (P -> Q)) -> Q
19:38:48 <mauris> @djinn (p, p -> q) -> q
19:39:40 <mauris> the @djinn command? ~magic~
19:39:46 <mauris> but modus ponens is basically application, yeah!
19:40:02 <hppavilion[1]> mauris: No, how does (p, p -> q) -> q become that?
19:40:27 <hppavilion[1]> mauris: I know that modus ponens if application; wiki said so, so I was using that as practice
19:40:59 <mauris> the @djinn command takes a type and... by some complicated process, thinks up a value that has that type
19:41:24 <hppavilion[1]> mauris: Ah. But how does f (a, b) = b a even have that... OH!
19:41:50 <mauris> maybe "f (p, g) = g p" is clearer?
19:42:51 <mauris> anyway, if you give @djinn simple curry-howard thingies, it can do "proofs" (because a function inhabiting some type ≈ a proof that some logic predicate holds)
19:44:46 <mauris> it can handle some pretty cool things
19:44:49 <mauris> @djinn (Either a b, Either a c) -> Either a (b, c)
19:45:42 <hppavilion[1]> Either ((F, (P -> F)) -> F) ((T, (P -> T)) -> T) is what I got from it
19:45:48 <b_jonas> @djinn (a, (b, c)) -> (c, (b, a))
19:47:11 <mauris> wikipedia says modus tollens is just: P -> Q and NOT Q ==> NOT P right?
19:47:32 <mauris> @djinn (p -> q, q -> Void) -> (p -> Void)
19:47:46 <mauris> @djinn ((p -> q), (q -> Void)) -> (p -> Void) -- parens for clarity
19:48:15 <mauris> anyway, you can use currying nicely here! do you know about that?
19:49:01 <mauris> (you don't *need* it, but that's what lambdabot did there)
19:50:53 <mauris> well, essentially p → q and q → Void are your two steps to a contradiction
19:51:49 <mauris> my recommendation: you should play http://incredible.pm/ if you enjoy this and want it gamified. it's lots of fun!
19:52:32 <mauris> solving the problems on there is a lot like writing a function like @djinn does
19:53:20 <shachaf> the amazing mauris and his educated rodents
19:54:51 <shachaf> The main thing I remember from that book is the word "cooperate".
19:55:17 <shachaf> Which I pronounced as "coop-erate" since I didn't know how it was pronounced.
19:56:05 <mauris> pronouncing words wrong cause you've only ever read them is great
19:56:19 <mauris> how was i supposed to guess "colonel"??
19:57:00 <shachaf> they don't call torvals "the linux colonel" for nothing
19:59:16 <shachaf> @djinn-add type Cont r a = (a -> r) -> r
19:59:20 <shachaf> @djinn ((p -> Cont r q) -> Cont r p) -> Cont r p
20:30:51 -!- Tod-Autojoined has joined.
20:32:28 -!- TodPunk has quit (Ping timeout: 265 seconds).
20:38:38 -!- bb010g has quit (Quit: Connection closed for inactivity).
20:41:44 -!- EgoBot has quit (Ping timeout: 276 seconds).
20:41:47 -!- Gregor has quit (Ping timeout: 246 seconds).
20:42:56 -!- shachaf has quit (Ping timeout: 272 seconds).
20:43:07 -!- FireFly has quit (Ping timeout: 260 seconds).
20:44:16 -!- shachaf has joined.
20:46:47 -!- EgoBot has joined.
20:48:11 -!- Gregor has joined.
20:48:27 -!- FireFly has joined.
20:58:05 -!- MDude has quit (Ping timeout: 265 seconds).
21:13:02 -!- J_Arcane has joined.
21:28:14 -!- EgoBot has quit (Remote host closed the connection).
21:29:26 -!- FireFly has quit (Ping timeout: 240 seconds).
21:30:03 -!- EgoBot has joined.
21:34:49 -!- hppavilion[1] has quit (Ping timeout: 265 seconds).
21:35:00 -!- Gregor has quit (Ping timeout: 264 seconds).
21:35:36 -!- FireFly has joined.
21:39:57 -!- TieSoul has quit (Remote host closed the connection).
21:40:03 -!- Gregor has joined.
21:49:50 -!- vifino has quit (Quit: Who turned this off?! D:<).
21:55:00 -!- vifino has joined.
22:11:51 -!- Mossa_Mossa has joined.
22:12:08 -!- Mossa_Mossa has left ("Leaving").
22:23:11 <FireFly> Maybe they took a wrong turn and ended up here
22:28:33 <izabera> https://github.com/VerbalExpressions/JSVerbalExpressions
22:55:10 -!- MDude has joined.
23:11:23 -!- p34k has joined.
23:15:17 -!- boily has joined.
23:15:44 -!- oerjan has joined.
23:36:30 -!- spiette has quit (Ping timeout: 260 seconds).
23:41:44 -!- Edu1 has joined.
23:46:06 <HackEgo> Edu1: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <http://esolangs.org/>. (For the other kind of esoterica, try #esoteric on EFnet or DALnet.)
23:48:25 <Edu1> soy de venzuela
23:49:06 <izabera> do you also speak english? <.<
23:49:07 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: welcome.es: not found
23:49:19 <boily> argh. what was the spanish version again?
23:49:26 <HackEgo> Edu1: ¡Bienvenido al centro internacional para el diseño y despliegue de lenguajes de programación esotéricos! Por desgracia, la mayoría de nosotros no hablamos español. Para obtener más información, echa un vistazo a nuestro wiki: http://esolangs.org/. (Para el otro tipo de esoterismo, prueba #esoteric en EFnet o DALnet.)
23:49:44 <int-e> `` echo wisdom/wecome*
23:49:45 <boily> Edu1: ¿hablá usted inglés?
23:49:49 <int-e> `` echo wisdom/welcome*
23:49:50 <HackEgo> wisdom/welcome wisdom/welcome.bork wisdom/welcome.eo wisdom/welcome.es wisdom/welcome.fi wisdom/welcome.fr wisdom/welcome.nl wisdom/welcome.sv
23:50:18 <Edu1> no hablo ingles
23:53:09 <boily> ¿conoces brainfuck? está el más popular de los lenguajes esotéricos: https://es.wikipedia.org/wiki/Brainfuck
23:59:36 -!- Edu1 has left.