00:00:56 -!- augur has joined.
00:01:08 -!- augur has quit (Remote host closed the connection).
00:01:51 -!- augur has joined.
00:15:35 -!- variable has quit (Excess Flood).
00:16:47 -!- Guest21084 has joined.
00:18:29 -!- elliott has quit (Ping timeout: 260 seconds).
00:23:24 -!- calamari has joined.
00:33:39 -!- NihilistDandy has quit (Ping timeout: 260 seconds).
00:36:34 -!- zzo38 has quit (Remote host closed the connection).
00:37:15 -!- pikhq has quit (Ping timeout: 244 seconds).
00:37:20 -!- pikhq has joined.
00:44:38 -!- Guest21084 has quit (Changing host).
00:44:38 -!- Guest21084 has joined.
00:44:51 -!- Guest21084 has changed nick to variable.
01:14:57 -!- hagb4rd2 has quit (Quit: hagb4rd2).
01:23:36 -!- calamari has left ("Leaving").
01:48:32 -!- NihilistDandy has joined.
01:53:34 -!- NihilistDandy has quit (Ping timeout: 272 seconds).
01:54:05 -!- hagb4rd has joined.
02:01:44 <itidus21> i like the part about showing off his copy of the dragon book next to the teapot
02:12:29 -!- pikhq_ has joined.
02:12:49 -!- pikhq has quit (Ping timeout: 260 seconds).
02:15:19 -!- Mathnerd314 has quit (Ping timeout: 246 seconds).
02:18:45 -!- hagb4rd has quit (Quit: hagb4rd).
02:23:03 -!- hagb4rd has joined.
02:49:46 -!- MDude has changed nick to MSleep.
03:16:56 -!- MSleep has quit (Ping timeout: 246 seconds).
03:52:47 -!- azaq23 has quit (Quit: Leaving.).
04:16:10 -!- zzo38 has joined.
04:22:04 -!- hagb4rd2 has joined.
04:22:04 -!- hagb4rd has quit (Disconnected by services).
04:22:05 -!- hagb4rd2 has changed nick to hagb4rd.
04:39:48 -!- asiekierka has joined.
05:25:36 -!- chickenz has quit (Ping timeout: 276 seconds).
05:42:14 -!- oerjan has quit (Quit: Good night).
05:53:32 -!- juha0011 has joined.
05:54:24 -!- juha0011 has changed nick to nortti.
05:55:41 <mroman_> Why exactly is W = \x.\y.x(yy) not a bck term?
05:58:16 <mroman_> In x(yy) y occurs more than "at most once"
05:58:38 <mroman_> although the definition here says "for subterms \x.M" and x(yy) does not look like it has the form "\x.M"
05:59:12 <mroman_> \y.x(yy) would be such a subterm, but if I got that right, y is not free.
06:24:32 -!- hagb4rd has quit (Ping timeout: 246 seconds).
06:46:00 -!- nortti has quit (Quit: ChatZilla 0.9.88.1 [Firefox 11.0/20120312181643]).
07:00:17 -!- Patashu has joined.
07:17:50 -!- graue has joined.
07:27:10 <Sgeo_> Ok. How do I stop YouTube from ever trying HTML5
07:27:23 <Sgeo_> ...by removing myself from the trial
07:27:38 <graue> what's wrong with HTML5?
07:27:47 <Sgeo_> I'm blaming it for my inability to use YouTube
07:28:50 <Sgeo_> Tried an HTML5 video demo, it crashed.
07:29:12 <graue> you should upgrade your browser
07:29:33 <Sgeo_> I'm using Chromium 17.0.963.79
07:29:59 <graue> well that's pretty silly of google isn't it
07:30:04 <graue> their own site doesn't work in their own browser
07:30:38 <itidus21> graue: i too noted the irony some time ago ^_^
07:31:39 <itidus21> i dunno where exactly but i am sure i did
07:31:44 <graue> the HTML5 stuff is working fine on firefox for me
07:32:17 <graue> in fact, i wish it used it all the time, because i haven't got flash working yet since an OS install
07:33:31 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.23986
07:33:56 <itidus21> aha i'm using the wrong tool for hte job
07:36:16 <itidus21> `log one of that companies websites
07:36:28 <HackEgo> 2012-03-25.txt:21:56:18: <itidus21> Sgeo_: it wouldn't make sense for a company's browser to be the most compatible with one of that companies websites
07:37:50 <itidus21> yeah .. the irony is delicious
07:39:33 <zzo38> Is Chromium 17.0.963.79 a non-stable version?
07:40:05 <Sgeo_> Good question, not sure
07:40:18 <Sgeo_> Not according to http://googlechromereleases.blogspot.com/2012/03/chrome-stable-update_10.html
07:51:44 -!- hagb4rd has joined.
07:56:20 <shachaf> Sgeo_: Also, you're a bad person.
07:56:44 <shachaf> printf("Sgeo is a bad person\n");
07:57:02 <kmc> yeah it's funny when chromium sucks at youtube and google maps
07:57:06 <kmc> which is frequently the case
07:57:22 <shachaf> Is there even a difference between this channel and that channel?
07:59:10 <olsner> that channel is that channel, this channel is this channel
08:00:09 <Sgeo_> olsner, pretty sure you have it backwards. That channel is this channel, and this channel is that channel.
08:00:32 <olsner> Sgeo_: these are not the channels you're looking for
08:00:47 <graue> what channel is "that" channel?
08:02:40 <shachaf> elliott would probably get mad, but then realize that that channel isn't actually *that* channel.
08:02:56 <graue> maybe i don't want to get involved
08:03:05 <olsner> shachaf: and when you say that channel, do you mean this channel?
08:03:17 <graue> so what, this channel is identical to itself?
08:03:24 <graue> that's a frickin' tautology
08:04:26 <hagb4rd> guess that channel is a reference to this channel
08:04:41 <Sgeo_> I feel like I should clue graue in
08:04:46 <Sgeo_> Because I'm not a jerk.
08:04:48 <zzo38> How many features of evolution theory seem partially mistaken? That is probably the case with any scientific things that people figure out new things in future.
08:05:02 <shachaf> olsner: No, the other channel.
08:05:17 <shachaf> Sgeo_: I don't think you *can* clue graue in.
08:05:31 <Sgeo_> The first two letters are an abbreviation, the rest is identical to the name of the subreddit where Reddit Gold members can hang out
08:06:27 <graue> i have never used reddit
08:07:07 <shachaf> Sgeo_: Oh, that channel. Not *that* channel.
08:07:45 <graue> Sgeo_ this was not helpful
08:09:02 <Sgeo_> Do you have any ideas what the abbreviation might be?
08:09:29 <shachaf> I'm sorry now that I started this.
08:09:47 <Sgeo_> Ok, I'll stop being cruel
08:10:07 <graue> oh, *that* channel
08:10:44 <shachaf> When elliott reads these logs (hi elliott!) he'll get annoyed at me.
08:19:16 -!- Patashu has quit (Ping timeout: 272 seconds).
08:22:55 -!- Patashu has joined.
08:23:37 -!- hagb4rd2 has joined.
08:23:38 -!- hagb4rd has quit (Disconnected by services).
08:23:38 -!- hagb4rd2 has changed nick to hagb4rd.
08:25:09 <hagb4rd> sry my machine crashed..any answers i might have missed?
08:26:13 <graue> you must have been looking for "that" channel
08:27:02 <kmc> it's annoying when people make a public big deal out of knowing a secret
08:27:07 <kmc> i saw this a lot in college
08:27:11 <kmc> and also from google employees
08:27:42 <graue> you know, i have a funny story about that
08:27:49 <graue> ...but it's a secret
08:31:23 -!- graue has quit (Quit: Leaving).
08:55:58 -!- NSQX has joined.
08:56:12 <NSQX> +[-.+[->+<]>+]
08:58:47 <NSQX> What? Run this brainfuck code: +[-.+[->+<]>+]
09:00:42 <fungot> .. !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ ...
09:01:36 <NSQX> It's actually designed to cause a buffer overflow in an esoteric programming language.
09:02:46 <NSQX> That is a newly-discovered buffer overflow bug and will probably never be fixed.
09:03:32 <NSQX> Try to run it on http://ideone.com/
09:03:56 <NSQX> You will, of course, get an "out of memory" error.
09:05:08 <monqy> what do you mean it's designed to cause a buffer overflow in an esoteric programming language
09:05:24 <NSQX> What about this same buffer overflow bug in another esoteric programming language, like Befunge?
09:05:24 <monqy> a specific brainfuck implementation?
09:05:45 <monqy> don't really understand what you're getting at
09:06:44 <fizzie> Running out of memory is not a "buffer overflow".
09:07:29 <fizzie> Some brainfuck implementations also have a wrapping tape; didn't the original? Fungot at least does.
09:08:26 <NSQX> What about trying to run it with a brainfuck implementation with an infinite number of memory cells?
09:09:10 <NSQX> Anyway, was this translated to another language, like Befunge? If so, show me the code.
09:11:58 <Sgeo_> Buffer overflow is when you manage to corrupt memory by putting excessive data into a buffer. Nothing is being corrupted here.
09:13:04 <Sgeo_> Most esolang interpreters that provide a finite amount of memory are smart enough to stop the program upon the program's memory being filled. And for infinite memory, it stops when the computer is out of memory.
09:13:37 <Sgeo_> Buffer overflow would be if some BF interpreter, written in C, say, allocates 30,000 cells but neglects to put in checks that memory being written to is within those 30,000 cells
09:21:37 -!- NSQX has quit (Ping timeout: 245 seconds).
09:49:19 * kmc thinks some of the people in this channel would like http://io.smashthestack.org:84/ level 11
09:51:28 <kmc> will explain what it is if you like, but spoilers
09:51:57 * kmc thinks some of the people in this channel would like http://io.smashthestack.org:84/ level 11
10:06:26 -!- cheater has quit (Ping timeout: 246 seconds).
10:20:01 -!- cheater has joined.
10:26:37 -!- hagb4rd has quit (Ping timeout: 252 seconds).
10:28:54 -!- hagb4rd has joined.
10:34:05 -!- monqy has quit (Quit: hello).
10:43:32 -!- GhostHand has joined.
10:44:33 -!- myndzi\ has joined.
10:45:02 -!- myndzi has quit (Ping timeout: 252 seconds).
10:46:16 -!- GhostHand_ has joined.
11:19:54 -!- elliott has joined.
11:59:07 -!- Patashu has quit (Quit: MSN: Patashu@hotmail.com , Gmail: Patashu0@gmail.com , AIM: Patashu0 , YIM: patashu2 , Skype: patashu0 .).
12:02:25 -!- Phantom_Hoover has joined.
12:23:36 <kmc> estimez le poids du gâteau de fruits
12:26:26 -!- hagb4rd has quit (Ping timeout: 246 seconds).
12:28:18 -!- hagb4rd has joined.
12:28:34 -!- kmc has set topic: estimez le poids du gâteau de fruits.
12:28:40 -!- elliott has set topic: http://codu.org/logs/_esoteric/.
12:28:58 -!- elliott has set topic: estimez le poids du gâteau de fruits | http://codu.org/logs/_esoteric/.
12:36:42 <kmc> very good very good
12:44:01 <kmc> here is our standard erlang environment
12:44:05 <kmc> we're running x windows on a sun workstation
12:44:18 <kmc> let's just make a normal call just to see that the system works
12:44:24 <kmc> hello mike
12:44:31 <kmc> hello joe. system working?
12:44:39 <kmc> seems to be
12:45:09 <kmc> 1-6-7. what we see here is a symbolic trace of the communications to and from the number analyzer.
12:45:42 <kmc> i'll now dial an incorrect number
12:46:25 <kmc> things are starting to go wrong. we see here that something has gone wrong. an error has occurred.
12:46:35 <kmc> here is the original error, which caused all the subsequent errors.
12:59:51 -!- cswords_ has joined.
13:03:11 -!- cswords has quit (Ping timeout: 246 seconds).
13:04:18 <Phantom_Hoover> "what time is it for gods sake" does not elicit the appropriate response from Google.
13:06:17 -!- derdon has joined.
13:24:21 -!- GhostHand_ has quit (Read error: Connection timed out).
13:24:54 -!- GhostHand_ has joined.
13:33:12 <zzo38> Phantom_Hoover: Does the question even make sense?
13:36:22 -!- Mathnerd314 has joined.
13:38:30 <zzo38> I made up the Haskell class like this: class Multiapply f v v' | f -> v, f -> v' where { (*$>) :: f -> v -> v'; multiid :: (v ~ v') => f; };
13:39:01 <elliott> that fundep is the same as f -> v v'
13:39:20 <zzo38> O, that's how it works.
13:40:02 <zzo38> The law is supposed to be (multiid *$>) = id but maybe there are supposed to be others too
13:41:50 -!- MDude has joined.
13:47:28 -!- augur has quit (Remote host closed the connection).
14:08:07 -!- Phantom_Hoover has quit (Remote host closed the connection).
14:09:21 -!- Phantom_Hoover has joined.
14:10:26 -!- boily has joined.
14:17:13 -!- augur has joined.
14:18:31 <MDude> I'm not sure if I have a high enough population to be a city.
14:20:11 <RocketJSquirrel> MDude: It's not the size that matters, it's how you administrate.
14:21:45 <GhostHand> Here is the research of programming?
14:26:12 -!- hagb4rd2 has joined.
14:26:13 -!- hagb4rd has quit (Disconnected by services).
14:26:13 -!- hagb4rd2 has changed nick to hagb4rd.
14:56:49 <elliott> <t7> anyone who uses their real name as their nick isnt a true internet geek
14:57:00 <elliott> I'm so glad we have true internet geeks like t7 in #haskell.
15:01:16 -!- MDude has quit (Ping timeout: 260 seconds).
15:10:34 <GhostHand> My girlfriend and I happened some unhappy things
15:11:34 -!- GhostHand_ has left ("Leaving").
15:13:50 -!- hagb4rd has quit (Quit: hagb4rd).
15:15:26 -!- hagb4rd has joined.
15:28:47 <oklopol> now just what the fuck is snack
15:43:14 -!- boily has quit (Ping timeout: 272 seconds).
15:47:16 -!- boily has joined.
15:56:49 -!- boily has quit (Ping timeout: 244 seconds).
16:03:29 -!- Taneb has joined.
16:21:40 -!- cknz has joined.
16:24:05 <Taneb> I am now learning C
16:24:14 <Taneb> Is this a bad idea?
16:24:31 <elliott> Yes, if you're using that book.
16:25:06 <Taneb> But it's listed on that page the nice folks in ##c linked me to!
16:25:54 <elliott> The folks in ##c are something like the opposite of nice.
16:26:08 <elliott> In fact, you should really stay out of ##c entirely.
16:26:45 <elliott> Anyway, whatever, I don't actually know anything about the book.
16:27:37 <fizzie> Yes, they are not nice.
16:27:41 <Taneb> The "hello world" program it gives is pretty obfuscated
16:28:10 -!- hagb4rd has quit (Ping timeout: 252 seconds).
16:28:33 <Taneb> http://hpaste.org/66070
16:28:53 <elliott> That's the first program it shows you?
16:29:06 <elliott> fizzie: "Back me up here", he says again.
16:29:33 <Taneb> But this book is a family heirloom!
16:30:30 <Taneb> It does say that the program won't make sense until Chapter 9
16:30:32 <elliott> Is that program even legal?
16:30:44 <elliott> Looks dangerously close to UB to me. I think it's definitely endianness-dependent.
16:30:51 <elliott> Seriously, you don't want to read that book.
16:30:51 <Taneb> It works on my system
16:30:58 <elliott> Yes, it might very well might.
16:31:03 <Taneb> And I need to go very quickly
16:31:05 -!- Taneb has quit (Quit: Leaving).
16:31:07 <elliott> The proliferation of C programs that "work on your system" and are completely invalid is ...
16:31:16 <elliott> Why do I even start to type sentences greater than four words when Taneb is here?
16:31:22 <fizzie> The fact that the other is a char[] might be enough to make it legal, though I'm not entirely sure. It's certainly not portable.
16:32:17 -!- hagb4rd has joined.
16:33:12 <fizzie> The "UB to read from a union member that was not the one you wrote to" rule is broad, but OTOH you can read everything via a char*. I suppose it depends on the exact way things were written.
16:34:08 <quintopia> it took me a second to realize you werent writing emails to members of some political union
16:35:19 <fizzie> One hopes the book mentions the program is not portable, though.
16:38:36 <fizzie> Also implicit int and () for main is just bad manners, as is the lack of return.
16:40:46 <elliott> Ugh, I didn't even notice that.
16:41:19 <elliott> @tell Taneb That book is *really* low-quality: http://codu.org/logs/log/_esoteric/2012-03-27#163107elliott onwards
16:44:23 <fizzie> Oh, the lack of #include <stdio.h> does in fact make it UB.
16:44:37 <fizzie> The program that keeps on giving (reasons why it's bad).
16:44:57 <fizzie> (The implicit declaration of printf is not the correct declaration.)
16:46:39 <elliott> @tell Taneb Seriously, don't read that. Pick up K&R or something.
16:46:46 <elliott> (Consult fizzie for adequate specifications of "something".)
16:52:29 <elliott> "A person's name is not the title of a work — even if people call that person a piece of work" -- HTML specification
16:54:18 <fungot> elliott: and, dab, words like pop-culture should use the binary level, then
16:54:19 <fungot> elliott: " so that the text, and i bless god for my safe, that he was overcome with the vastness, profundity, and fnord
16:54:20 <fungot> elliott: or is it just me, or i: yet, you rogue! bitchin'! not much longer intervals. cia 1 56320-56335 in-between commands to run
16:54:27 <elliott> fizzie: Which styles give long text?
16:55:32 -!- azaq23 has joined.
16:57:38 <fungot> Available: agora alice c64 ct darwin discworld europarl ff7 fisher fungot* homestuck ic irc iwcs jargon lovecraft nethack pa qwantz sms speeches ss wp youtube
16:57:41 <fungot> Selected style: alice (Books by Lewis Carroll)
16:59:08 <Sgeo_> elliott, how do I block HTML5 video in Chromium?
16:59:44 <elliott> Sgeo_: Don't visit any pages with HTML5 video on them.
16:59:59 <fungot> Sgeo_: " yes," he said. " do you believe in fate?" he exclaimed anxiously. " i'll fnord down a sheet of brown paper. " what will the warden--"
17:00:20 <fungot> Selected style: europarl (European Parliament speeches during approx. 1996-2006)
17:00:23 <fungot> elliott: mr president, mr president-in-office of the council, president of the commission, i should just briefly like to focus on demand management measures as yet apply. so, we should ask what more we need to keep the dictator's hands away from weapons of mass destruction. that is very strange. but on the other side parliamentarians, who will soon be possible to deploy it quickly and above all to help the new institution in ad
17:00:26 <fungot> elliott: it is important for the european parliament, which is no such thing as absolute scientific certainty about new substances or products, nor can i accept amendment no 3. requirements for the provision of training and to provide for employees' representatives. it must also be viewed as a springboard for further action directed at the commission for the 1996 budget; the motion of censure.
17:00:29 <elliott> fungot: Parl. Shorter please.
17:00:30 <fungot> elliott: madam president, the nuclear safety of our citizens from any threat to it whatsoever. mr president, mrs soltwedel-schfer, where there is respect for parliamentary rules and the conference of presidents to lay down specific rules for these measures if this type of social security.
17:00:37 <Sgeo_> elliott, that's great. Not going to stop visiting YouTube, but can't figure out how to tell it "NO HTML5"
17:01:09 <elliott> http://www.youtube.com/html5
17:01:32 <Sgeo_> I'm not IN the trial. I was, but now I'm not, I cleared cache, blah blah
17:01:37 <elliott> fungot: Okay, but now without non-Unicode.
17:01:38 <fungot> elliott: mr president, i think i have made to achieving our common aim is to identify those who make ringing declarations on the importance of preventing and combating euro counterfeiting. on the contrary, to show some willingness to compromise.
17:01:45 <elliott> Sgeo_: Then you don't get HTML5 video.
17:01:51 <Sgeo_> elliott, except I seem to
17:01:56 <Sgeo_> Sometimes at least
17:03:02 <fizzie> elliott: Well, you know, like the wise men say: "Html5 Fail, better to use Flash, Html5 is ok to make website page, but for media it suxx, h.264 suxx more than Divx or Xvid in quality. Hope it will disapear on youtube."
17:03:41 <Sgeo_> HTML5 video crashes Chromium for me.
17:04:15 <elliott> fizzie: "h.264 suxx more than Divx or Xvid in quality" is quite the statement.
17:04:20 <fizzie> Sgeo_: Removed all tube cookies too?
17:05:16 <Sgeo_> Although I only deleted cookies from youtube.com and www.youtube.com
17:05:43 <elliott> fizzie: What's a generic term for the author of an IRC message? "Author" or "speaker" isn't good, since e.g. I refer also to the parter of a /part or the quitter of a /quit.
17:05:54 <elliott> I would probably call #esoteric the subject of this PRIVMSG.
17:08:34 <fizzie> I'unno. It could be "sender" except it isn't always that either.
17:08:46 -!- GhostHand has quit (Quit: Leaving).
17:09:12 <fizzie> I think it's the "guy" of the message.
17:09:37 <elliott> When would it not be the sender?
17:12:26 -!- Taneb has joined.
17:12:58 <lambdabot> Taneb: You have 2 new messages. '/msg lambdabot @messages' to read them.
17:13:39 -!- tzxn3 has joined.
17:14:30 <fizzie> elliott: If it's a netsplit quit, it's arguably not.
17:15:57 <fizzie> Taneb: We have said rude things about your book. :'(
17:16:14 -!- asiekierka_ has joined.
17:16:14 -!- asiekierka_ has quit (Client Quit).
17:16:46 <elliott> fizzie: That's the IRC server sending it on behalf of them, isn't it? :)
17:16:51 <elliott> What does the RFC say? I suppose I could check.
17:16:52 <Sgeo_> My school is having a vote on a new student government constitution
17:17:05 <Sgeo_> Would it be unethical for me and/or annoying for Agora to ask for Agora's input?
17:18:13 <Taneb> The book does acknowledge that program's system-dependedness
17:18:17 <Taneb> The printf thing, not so far
17:18:30 <elliott> Sgeo_: I won't pass a value judgement, but I'd have to exercise greater-than-average restraint to avoid replying with a snarky comment.
17:18:37 <elliott> The fear of G. would probably be enough to do it, though.
17:26:58 <Taneb> Enhancing my reputation of leaving suddenly...
17:27:01 -!- Taneb has quit (Quit: Maybe Stew).
17:42:08 -!- Mathnerd314_ has joined.
17:43:11 -!- Mathnerd314 has quit (Ping timeout: 246 seconds).
17:43:24 -!- Mathnerd314_ has changed nick to Mathnerd314.
17:55:47 <olsner> elliott: btw, it's not hard to figure out what my IP is
17:56:13 -!- elliott has changed nick to abcdefghijklmnop.
17:56:17 -!- abcdefghijklmnop has changed nick to elliott.
17:56:29 <elliott> olsner: was it you though?
17:59:15 <olsner> doing the captcha is easier than logging in, if you only do one edit :)
18:02:58 <olsner> after the first edit I did reset my old account's password, but apparently the session timed out or something before my second edit
18:10:26 <elliott> olsner: i emailed you a new password, hth
18:10:36 <elliott> it timed out after you set it
18:10:46 <elliott> darn, my snarky-but-helpful use of the login form turns into an annoyance
18:11:03 <elliott> you may demand I ritually commit suicide
18:14:11 -!- MDude has joined.
18:19:32 -!- Mathnerd314 has quit (Ping timeout: 244 seconds).
18:19:53 -!- Mathnerd314 has joined.
18:33:03 -!- jix has quit (Quit: Lost terminal).
18:33:17 -!- hagb4rd2 has joined.
18:33:18 -!- hagb4rd has quit (Disconnected by services).
18:33:18 -!- hagb4rd2 has changed nick to hagb4rd.
18:33:23 -!- jix has joined.
18:49:18 -!- augur_ has joined.
18:51:39 -!- augur has quit (Ping timeout: 245 seconds).
18:58:37 -!- calamari has joined.
19:06:30 -!- calamari has left ("Leaving").
19:15:31 -!- asiekierka has quit (Read error: Connection reset by peer).
19:31:20 <elliott> Phantom_Hoover: I assume you've seen http://vimeo.com/1109226?
19:31:34 <elliott> COMPUTER HARDWARE MUSIC: a diverse field.
19:32:22 -!- Mathnerd314 has quit (Read error: Connection reset by peer).
19:33:04 -!- Mathnerd314 has joined.
19:36:52 -!- ais523 has joined.
19:38:12 <ais523> I am busy writing the best build system for C ever
19:38:19 <ais523> with potential support for other languages eventually, too
19:38:36 <ais523> basically, it works out all the dependencies for you, forwards and backwards
19:38:58 <ais523> except when it has no ability to do so, e.g. if you want to build a library, it can't guess where the entry points you want are
19:39:00 <ais523> and it's called aimake :)
19:39:29 <ais523> the information required is mostly in the files
19:39:34 <ais523> header files have #includes, you can trace those
19:39:45 <ais523> and object files you can run nm on them to see what they import and export, and work out the dependencies that way
19:40:01 <elliott> I wonder if ais523 realises he's told us about aimake before.
19:40:13 <ais523> but now I'm actually /writing/ it
19:41:02 <elliott> "You've earned the "Good Answer" badge for Can you recognize an infinite list in a Haskell program?."
19:41:07 <elliott> Why have 25 people upvoted that in one day?
19:41:45 <ais523> no, obviously, halting problem
19:42:07 <ais523> you can in OCaml because there are only a finite number of possible types of infinite list; although I'm not sure if you can do it using only constructs in the language
19:42:28 <elliott> Thanks, I obviously didn't know the answer, seeing as how I answered the question, and all.
19:42:47 -!- azaq23 has quit (Quit: Leaving.).
19:43:12 -!- azaq23 has joined.
19:43:17 -!- azaq23 has quit (Changing host).
19:43:17 -!- azaq23 has joined.
19:44:10 -!- oerjan has joined.
19:44:55 * oerjan guesses "estimate the weight of the fruitcake"
19:47:25 <oerjan> 05:55:41: <mroman_> Why exactly is W = \x.\y.x(yy) not a bck term?
19:47:25 <oerjan> 05:58:16: <mroman_> In x(yy) y occurs more than "at most once"
19:47:25 <oerjan> 05:58:38: <mroman_> although the definition here says "for subterms \x.M" and x(yy) does not look like it has the form "\x.M"
19:48:03 <oerjan> i'm pretty sure it should be something like "at most once in M for subterms \x.M"
19:49:45 <oerjan> the important point being, for each binding lambda \x.M there is at most once use of x referring to that binding
19:52:03 <oerjan> 07:32:24: <itidus21> `pastelogs itidus21 company
19:52:18 <oerjan> those commands take regexps, not individual words
19:53:27 <elliott> you expect itidus21 to learn regular expressions?
19:53:37 <itidus21> in this case it was easier to just check the logs directly than that
19:54:10 <oerjan> elliott: hey _some_ information is bound to get through
19:55:00 <itidus21> you can now construct the whole family of yes and no
19:57:31 <elliott> oerjan: i am not convinced we have communicated 1 bit of information to itidus21 in his time here.
19:58:58 <oerjan> or maybe fasting, who knows
19:59:49 <oerjan> elliott: see, he's learning :P
20:00:25 <elliott> even random walks progress occasionally
20:00:29 <mroman_> oerjan: I might have confused free occurences with free variables
20:00:58 <oerjan> admittedly i'm almost convinced this spiel of "itidus21 can't learn" is a self-fulfilling prophecy, no matter _who_ encourages it.
20:01:38 <elliott> oerjan: you realise we spent the first N months of itidus21 being here denying him when he said things of that nature and pointing out exactly how much of a self-fulfilling prophecy it is.
20:02:05 <elliott> if he insists on believing it, there is no point expending extraordinary effort to tell him otherwise.
20:03:01 <oerjan> elliott: there can still be a point in not helping to entrench it, no?
20:04:19 <mroman_> so \y.x(yy) has one free variable x and two free occurences of y and one binding occurence of y.
20:05:52 <oerjan> mroman_: um i don't think there are any free occurences of y in \y.x(yy).
20:06:01 -!- nortti has joined.
20:06:49 <oerjan> i don't think there _is_ fundamentally a difference between free variable and free occurrence.
20:07:38 <oerjan> however, note that y is free _in the subexpression_ x(yy)
20:08:26 <elliott> i would like to take this opportunity to complain about the teaching of lambda calculus with explicit shuffling of names like this, which has surely caused an absurd number of students to confuse the syntactic bookkeeping with the true essence.
20:08:43 <mroman_> but does that fall under the definiton of "subterm \x.M"?
20:09:24 <oerjan> mroman_: no, but that _could_ be a typo
20:09:42 <oerjan> in some part of the phrasing
20:10:18 <mroman_> (i) for each subterm \x.M of Y, x occurs free in M at most once
20:10:59 <mroman_> then the rest of this sentence makes no sense @typo
20:12:14 <oerjan> mroman_: that looks correct, note that \y.x(yy) is a subterm
20:12:36 <oerjan> not a _proper_ subterm, though
20:13:30 <mroman_> Yes, but \y.x(yy) does not violate the definition of a BCK Term
20:13:36 <oerjan> y occurs free in x(yy) _twice_
20:13:49 <oerjan> thus \y.x(yy) is not a BCK term.
20:14:20 <oerjan> ...you're not misreading the term "at most once", are you?
20:14:36 <oerjan> that means twice or more is prohibited
20:15:16 -!- graue has joined.
20:17:03 <mroman_> I know what "at most once" means, yes ;)
20:17:48 <oerjan> mroman_: note that the "x occurs free in M" is really just a roundabout way of saying that in \x.M, it occurs bound to _that_ binding of x, and not to some deeper one.
20:17:49 <mroman_> The definition is very misleading.
20:18:42 <mroman_> because if I have no \x, how would I know which thing must not occure more than once.
20:18:43 <oerjan> mroman_: as i said, it looks correct to me
20:19:16 <oerjan> mroman_: um if there are no lambdas, then there is no restriction.
20:19:56 <oerjan> it says that for every variable binding \x (where x is an arbitrary variable), _that_ binding is not used more than once.
20:21:06 <mroman_> The definition of BCI terms is misleading in the same way
20:21:26 <oerjan> with "exactly once", iirc
20:21:28 <mroman_> in \xy.x x occurs in every subterm exactly once
20:21:47 <mroman_> (it does in \y.x as well as in x)
20:21:47 <elliott> Has it been long enough since my last complaint for me to complain again?
20:22:06 <elliott> This "free variable" stuff is such nonsense, really.
20:22:25 <oerjan> mroman_: no, it doesn't occur in every subterm. for every subterm _of the form_ \x.M, x occurs exactly once in M.
20:22:58 <oerjan> there is no looking at more than one subterm of \x.M for that binding.
20:23:19 <elliott> I GET THE FEELING MY COMPLAINTS ARE BEING DISREGARDED :'(
20:23:56 <oerjan> elliott: yeah yeah go worship deBruijn
20:24:09 <oerjan> he's dead, so maybe you can get him canonized.
20:24:19 <mroman_> So... this time it HAS to be \x.M and not just M as in BCK?
20:24:35 <oerjan> mroman_: it's exactly the same way for BCK
20:24:37 <elliott> oerjan: HOAS is acceptable too!
20:26:19 <elliott> oerjan: higher-order abstract syntax
20:26:32 <elliott> data Term = App Term Term | Lam (Term -> Term) or such
20:26:57 <elliott> commonly something like `data Term a = App (Term a) (Term a) | Lam (Term a -> Term a) | Var a` so you can print them
20:26:57 -!- pikhq has joined.
20:26:59 -!- pikhq_ has quit (Ping timeout: 240 seconds).
20:26:59 -!- graue has quit (Remote host closed the connection).
20:27:06 <elliott> oerjan: it works better in some contexts than others
20:27:14 <elliott> e.g. it's pretty bad in haskell because that (->) can do anything to the term
20:27:25 * elliott suddenly realises that oerjan might know what higher-order abstract syntax is, just not "HOAS".
20:27:37 <elliott> here, http://en.wikipedia.org/wiki/Higher-order_abstract_syntax :P
20:27:48 <mroman_> \y.x has no free occurence of y
20:30:37 <elliott> data term a = Var a | App (Term a) (Term a) | Term (forall b. Term b -> Term a)
20:30:44 <elliott> stops the lambda messing with the vars
20:30:59 <elliott> I think oerjan is ignoring me now :)
20:32:03 <oerjan> elliott: that "refers directly to the binding site" reminds me of when i read bourbaki's set theory (one of the first books i found in the university library)
20:32:10 <fizzie> HOAS is the Helsinki area student-housing foundation thing.
20:32:43 <oerjan> its predicate logic notation had _actual_ lines from use to binding
20:34:54 -!- hagb4rd2 has joined.
20:34:54 -!- hagb4rd has quit (Disconnected by services).
20:34:55 -!- hagb4rd2 has changed nick to hagb4rd.
20:35:39 <elliott> oerjan: my favourite representation is probably { data Term a = Var a | Apply (Term a) (Term a) | Lam (Term (Maybe a)) }
20:35:58 <elliott> because (1) it has a wonderful monadic structure: (>>=) takes a lambda and a "dictionary" and substitutes
20:36:06 <elliott> (2) "Term Void" is a term with no free variables
20:36:17 <elliott> oerjan: e.g. id is Lam (Var Nothing)
20:36:25 <elliott> K is Lam (Lam (Var (Just Nothing)))
20:36:29 <elliott> it's typed de bruijn, essentially
20:37:19 <elliott> (that's another argument for (>>=) being theoretically interesting instead of simply useful in practice)
20:37:47 <elliott> (as opposed to fmap+join, I mean)
20:38:48 -!- nortti has quit (Quit: nortti).
20:39:17 <oerjan> although fmap does variable renaming, no
20:39:55 <elliott> ofc, fmap is interesting in its own right here, it's just that (>>=) has a more obvious meaning than join
20:56:18 <oerjan> <Phantom_Hoover> "what time is it for gods sake" does not elicit the appropriate response from Google.
20:56:57 <oerjan> `frink 13800000 days -> years
20:58:03 <oerjan> > .147856566566615 * 365.2425
20:58:03 -!- monqy has joined.
20:58:04 <lambdabot> <no location info>: parse error on input `.'
20:58:08 <oerjan> > 0.147856566566615 * 365.2425
20:58:47 <oerjan> 23 February, year 37783, hth
21:00:08 <fizzie> One of W|A's sidebar ads said to me something like "speak to W|A in your own language" and "OMG, just plot sin(x)" as an example.
21:00:33 <monqy> w|a's sidebar ads are awful
21:01:42 <oerjan> <oklopol> now just what the fuck is snack <-- BEST PROGRAMMING LANGUAGE HTH
21:01:54 <ais523> ooh, @lang has a name?
21:02:01 <oklopol> i was asking what i should eat for dinner.
21:02:02 <ais523> now we can go backwards from that to work out @'s
21:02:11 <elliott> omg just plot sin(x) monqy thanks
21:02:13 * oerjan waits for elliott's terrible revenge on ais523
21:02:25 <ais523> why? it was a complement
21:02:34 <elliott> snack is the complement of @lang, indeed
21:02:46 <elliott> oerjan: (TAKIN' HINTS FROM THE MASTER HERE)
21:02:57 <elliott> oerjan: WHAT DID YOU DO TO [[SNACK]]
21:03:17 <oerjan> elliott: i thought you were here when i did it...
21:03:33 <elliott> i don't think i was paying attention to the wiki, though
21:03:51 <oerjan> you _did_ notice my previous edit to that fishy thing
21:04:02 <oerjan> so since i was on a roll..
21:04:11 <elliott> that fishy thing isn't in [[Category:Shameful]] :P
21:04:26 <elliott> (although maybe it should be.)
21:05:09 <oerjan> also i just made a nice table and a section header, or so.
21:05:24 <oerjan> the remarkable prose style in unchanged.
21:06:02 <elliott> i suppose i already categorised it.
21:06:14 <oerjan> i feel i even preserved it when introducing the table headings
21:07:15 <elliott> it still breaks suspension of disbelief to believe that the creator of the language could effectively use an attractive wikitable. but i'm not so pathetic as to holy-war over the authenticity of modifications to a terrible language's article :P
21:15:38 <elliott> does anyone know how to explode
21:16:04 <monqy> it is one of the many mysteries of life
21:21:19 <itidus21> the best way to end ones life is go on tv and elaborate all of ones beliefs and opinions about politics, sex, religion, and foreign heads of state
21:22:38 <oerjan> s/best/most efficient/, hth
21:33:14 -!- augur_ has quit (Remote host closed the connection).
21:39:52 -!- Patashu has joined.
21:40:46 <zzo38> fizzie: Well, at least that particular ad is accurate; entering "OMG, just plot sin(x)" does work.
21:43:29 <zzo38> Why do you think (>>=) has a more obvious meaning than join? Perhaps it depends which monad you mean
21:43:38 <elliott> I was talking specifically about the Term monad there.
21:44:56 <zzo38> OK how does the Term monad work?
21:46:46 <zzo38> I would think return = Var
21:47:19 <elliott> return = Var; Var a >>= f = f a; Apply g x >>= f = Apply (g >>= f) (x >>= f); Lam e >>= f = Lam (fmap (>>= f) e) -- i might have gotten the last clause wrong
21:47:46 <elliott> basically if you have a term with free variables (e.g. of type Term (Maybe (Maybe Void)), thus having two free variables), then (tm >>= dict) will substitute them away
21:47:55 -!- Patashu has quit (Ping timeout: 248 seconds).
21:48:12 <elliott> so you can imagine dict :: Maybe (Maybe Void) -> Term Void; dict Nothing = term1; dict (Just Nothing) = term2; dict (Just (Just v)) = absurd v
21:51:37 <zzo38> So it would be join (Apply g x) = join (Apply g) (Apply x); join (Lam e) = Lam (join <$> e); well that look like to make sense to me, although I am unsure of the last one. Exactly what is the definition of the Lam constructor? A bunch of different things are posted above
21:52:09 <elliott> <elliott> oerjan: my favourite representation is probably { data Term a = Var a | Apply (Term a) (Term a) | Lam (Term (Maybe a)) }
21:52:42 <elliott> and yes, the definition for both is simple enough, it's just that (>>=) has an obvious semantic meaning (substitute variables) where join doesn't
21:53:01 <elliott> pure - reference variable; fmap - rename variables; (>>=) - substitute variables
21:53:13 <elliott> as opposed to pure - reference variable; fmap - rename variables; join - ???
21:53:25 <elliott> (oh, and I forget what exactly (<*>) does here... but anyway, brb)
21:59:50 <zzo38> But I suppose it is simply a feature of the (->) category that causes (<*>) to work with all monads (even though I want to define applicatives in terms of liftPair, which seems to be called $m_{A,B}$ in some Wikipedia article)
22:00:50 -!- Patashu has joined.
22:01:38 <oerjan> zzo38: (->) being cartesian closed, probably
22:02:12 <zzo38> oerjan: Yes, I thought it might be something like that
22:03:11 <oerjan> making a -> (b -> c) essentially isomorphic to (a, b) -> c
22:04:35 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
22:14:46 <elliott> oerjan: hmm, so is closed cartesian ~ currying works?
22:15:17 <oerjan> it implies that, at least
22:15:36 -!- ais523 has changed nick to callforjudgement.
22:16:29 <oerjan> "In category theory, a category is cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors."
22:16:43 <oerjan> i'd say that's pretty much a yes.
22:17:16 <zzo38> Can they make INTERCAL accept the words "FOWER", "FIFE", and "THOUSAND" in inputs? O, and, do they support Latin spellings of inputs?
22:18:02 -!- callforjudgement has changed nick to ais523.
22:21:23 <ais523> hmm, quick insanity check: does it make sense that a config file is only a single data object rather than containing malicious commands, when some of the things in the data objects are strings that are intended to be interpreted as shell commands and run?
22:23:31 <ais523> I'm wondering if it is, because putting actual code in the config file wouldn't be interpreted as expected anyway
22:24:06 <zzo38> Check it anyways regardless, so that at least you can learn it
22:24:10 <oerjan> exploits don't need to be based on expected behavior, do they?
22:24:56 * elliott can't parse ais523's question
22:25:02 <elliott> but thinks it suggests he's doing something wrong
22:25:36 <elliott> "validate input roughly --> pass to trusted thing" <<< "parse input --> write input for trusted thing"
22:26:53 <oerjan> lawful good people shouldn't write security code anyway.
22:29:44 <oerjan> only half joking - my idea is that you need to be able to think like a cracker to thwart one.
22:30:19 <elliott> i mean, there's a reason you see a lot of crackers end up joining big companies to do security work.
22:31:07 <oerjan> <elliott> NOT MORE THAN USUAL
22:31:35 <shachaf> It's Sgeo_ you should be mad at.
22:31:58 <ais523> oerjan: well, it's more that the securing is pointless because it's something that doesn't need exploiting because its intended purpose is to run user-specified shell commands
22:32:06 <elliott> then why are you validating it?
22:32:15 <ais523> in case it's invalid, I guess
22:32:21 <elliott> what if I _want_ to run malicious commands?
22:32:34 -!- Mathnerd314__ has joined.
22:33:00 <ais523> elliott: basically, the situation is that I'm using Perl's object notation for config files because I'm trying not to depend on any of CPAN, and I don't want to write my own YAML or JSON parser
22:33:10 <ais523> but I felt a bit queasy just running it through eval
22:33:24 <elliott> the solution is to depend on CPAN
22:33:37 -!- Mathnerd314 has quit (Ping timeout: 244 seconds).
22:33:49 -!- Mathnerd314__ has changed nick to Mathnerd314.
22:34:05 <ais523> elliott: no, then it won't be the best build system ever
22:34:31 <zzo38> Depending on who is running the program, and why, and what stuff exactly the configuration file is meant to do, using eval might be OK
22:34:35 <ais523> I was aiming for 1 dependency on Win32, 0 on POSIXy systems
22:35:02 <ais523> (I don't think it can be done with 0 dependencies on Win32)
22:35:17 <ais523> and that means relying on a scripting language that's portable and ready-installed everywhere on POSIX, and easy to install on Windows
22:35:23 <ais523> which basically drives the choice down to Perl or Python
22:35:59 <elliott> ais523: the best build system ever wouldn't be written in either of those
22:36:03 <ais523> zzo38: awk's a bit awkward for this sort of system
22:36:09 <ais523> elliott: I'm not convinced
22:36:14 <elliott> it also wouldn't run on win32
22:36:28 <Mathnerd314> elliott: compile <otherlang> to Perl or Python, done
22:36:36 <ais523> zzo38: C needs a build system, you need to avoid recursion here
22:36:50 <elliott> ais523: you realise you can write one more makefile in your life without dying, right?
22:36:51 -!- hagb4rd has quit (Ping timeout: 246 seconds).
22:36:51 <ais523> either that, or the build system needs its own separate build system, which is silly
22:36:54 <elliott> Mathnerd314: @lang can't be compiled to perl or python
22:37:20 <ais523> elliott: right; but I don't know if my users can run it correctly
22:37:35 <elliott> ais523: who gives a fuck about users?
22:37:38 <ais523> and it's surprisingly hard to write a correct makefile
22:37:46 <zzo38> I usually use a simple shell script to compile C programs
22:38:17 * oerjan pictures ais523's tombstone: "HE MADE ONE MAKEFILE TOO MANY"
22:38:26 <ais523> context: I'm trying to replace an inherited cmake-based build system because this specific build script doesn't work properly on Linux (recompiles from scratch no matter what) or at all on OS X, for currently unclear reasons
22:39:02 <ais523> elliott: oh, this is also an attempt to write a build system for C, I forgot to clarify that
22:39:11 <ais523> sufficiently good languages don't need build systems, just a compiler
22:39:19 <ais523> Mathnerd314: it's perfect by definition, the problem is trying to construct it
22:39:24 <zzo38> The most portable programming language is probably TeX although it is probably not suitable for your purpose.
22:39:31 <elliott> Mathnerd314: well, you know how all other languages have these pesky problems that make them bad?
22:39:42 <ais523> zzo38: seriously? does it run out of the box on Windows or VMS?
22:40:09 -!- derdon has quit (Remote host closed the connection).
22:40:13 <zzo38> ais523: You just need a TeX distribution, and then it will run on any operating system.
22:40:30 <ais523> zzo38: yes, and you need to build it, and so on
22:40:52 <elliott> ais523: you realise Windows users use binaries?
22:40:58 <Mathnerd314> elliott: and you don't count "missing compiler that outputs Perl" as a problem?
22:41:08 <ais523> if the build system can build TeX, then it could build a program written in C
22:41:18 <elliott> Mathnerd314: have you *seen* Perl?
22:41:20 <ais523> elliott: and it's possible to bundle Perl into binaries for Windows
22:41:42 <zzo38> TeX is written in Pascal, though. Usually it is still compiled with a C compiler though, but there are TeX distributions that use a Pascal compiler.
22:41:42 <ais523> but I can't reasonably put a Windows binary into a source tarball and keep it updated; it'd be pretty large
22:42:32 <zzo38> ais523: I agree; don't put a Windows binary into a source tarball. Put it in a separate file which is ZIP
22:42:37 <Mathnerd314> elliott: yes, I see nothing worse than LLVM
22:43:04 <elliott> Mathnerd314: have you *seen* LLVM?
22:43:07 <ais523> admittedly, I'm writing it in Perl 5.10
22:43:22 <ais523> I seriously looked at its internals thinking about gcc-bf, it is so nastily inflexible
22:43:55 <zzo38> I think LLVM is not such a bad programming language, although it would be good with macros (such as Lisp or BLISS style macros)
22:44:12 <zzo38> Have you seen BLISS? I happen to like some of the features of BLISS too
22:46:11 <elliott> ais523: are you disagreeing with me?
22:46:15 -!- azaq23 has quit (Remote host closed the connection).
22:46:39 <elliott> oerjan: Why is there no Contravoid such that (Contravoid -> r) ~ Void for all r?
22:47:07 <elliott> oerjan: I would also accept a Contravoid such that (Contravoid -> T) ~ Void for some T.
22:47:13 <elliott> (T =/= Contravoid, presumably.)
22:48:00 <zzo38> elliott: If you consider -> to be an exponent then perhaps it can be understand?
22:48:15 <oerjan> because \x -> undefined != undefined, hth.
22:48:19 <elliott> zzo38: But it's annoying. :(
22:48:34 <elliott> <elliott> oerjan: I would also accept a Contravoid such that (Contravoid -> T) ~ Void for some T.
22:48:38 <elliott> For some inhabited T, I should say.
22:48:42 <zzo38> One feature of BLISS is that a variable name in an expression represents the address of the variable, rather than its value. Another feature is that structures are allowed to contain program instructions too
22:49:32 <oerjan> elliott: if x \in r, const x \in (Contravoid -> r)
22:49:33 <zzo38> elliott: Annoying? How?
22:49:52 <ais523> elliott: I don't know, because I haven't been able to figure out what your opinion is so far
22:49:59 <ais523> so I'm stating mine, so you can either agree or disagree with it
22:50:18 <elliott> oerjan: thank you, I'm not so much of an idiot to require a constructive proof
22:51:01 -!- Mathnerd314_ has joined.
22:51:02 <elliott> oerjan: but it's annoying!
22:51:09 <elliott> what has to change to make that exist?
22:51:21 <elliott> ooh, if you have linear typing stuff, then you just need Contravoid to be a type with no eliminators
22:51:25 <oerjan> you could make Void inhabited. hth.
22:51:36 -!- Mathnerd314 has quit (Ping timeout: 260 seconds).
22:51:37 -!- Mathnerd314_ has changed nick to Mathnerd314.
22:51:42 <elliott> since you can't discard it, and can't eliminate it, there'll be no functions of that type
22:52:10 <zzo38> Do you know what law of this class is supposed to be (other than (multiid *$>) = id)? class Multiapply f v v' | f -> v, f -> v' where { (*$>) :: f -> v -> v'; multiid :: (v ~ v') => f; }; And do you know how common are things like what is used in the type signature for multiid?
22:52:22 <elliott> oerjan: (the reason I wonder is because with the pipes stuff, a sink (i.e. something that takes input and produces a result, but doesn't send anything downstream) can have its output type set to Void)
22:52:24 <zzo38> shachaf: I want to ask the same question too
22:52:28 <elliott> oerjan: (so it can't yield anything)
22:52:35 <shachaf> elliott: zzo38 wants to ask the same question too
22:52:54 <elliott> oerjan: (but a source (which takes no input and produces values downstream and a result) has to have input set to ())
22:53:07 <elliott> oerjan: (since it's impossible to stop you using the IWantInput (anInput -> AnotherPipeEtc) constructor)
22:53:17 <Mathnerd314> shachaf: type such that Contravoid -> T ~ Void
22:53:55 <elliott> hmm, i guess that linear thing is satisfying enough
22:54:10 <elliott> i wonder if there already _is_ a concept of something with no "eliminators" in that sense in normal linear logic.
22:54:19 <oerjan> linear logic is _very_ symmetric
22:54:19 <zzo38> shachaf: And yes I know that is impossible, something I have thought of too
22:54:48 <shachaf> I think elliott has /ignored me.
22:55:02 <elliott> oerjan: is that meant to imply "yes, probably"?
22:55:08 <oerjan> elliott: something like that
22:55:24 <elliott> if 0 is the uninhabited type i'm expecting it to be
22:55:40 <elliott> i don't understand the difference, naturally
22:57:48 <oerjan> i mean, a |- b is equivalent to ~b |- ~a (and to a, ~b |- _|_ and 1 |- ~a, b iirc, _everything_ can be moved across to the other side of the sequent by negating it)
22:58:08 <zzo38> In Ibtlfmm (currently a codename), the uninhabited type is called 0, and Word8 is now called Nat8, and Maybe is now called a successor monad; is it better?
22:58:11 <elliott> ais523: Where is the C-INTERCAL supplemental reference manual?
22:58:41 -!- azaq23 has joined.
22:58:58 <oerjan> i suppose classical logic also does that, but not intuitionistic logic
23:05:11 <ais523> elliott: supplemental? I only know of revised and revamped
23:05:22 <ais523> or was supplemental the original?
23:07:19 <elliott> Wikipedia references it, and it's a deadlink
23:07:42 <ais523> reference the one on ESR's site, I guess
23:07:47 <ais523> that's probably the one it wants
23:08:45 -!- augur has joined.
23:16:16 <elliott> zzo38: OK, this is the real instance:
23:16:18 <elliott> Apply g x >>= f = Apply (g >>= f) (x >>= f)
23:16:18 <elliott> Abstract e >>= f = Abstract (e >>= maybe (return Nothing) (fmap Just . f))
23:16:27 <elliott> probably there's an easier way to write that last clause
23:16:33 -!- itidus21 has quit (Quit: Leaving).
23:18:05 <elliott> I forget what beta-reduction looks like but it's a one-liner with the monad interface
23:20:11 <zzo38> You need to define the Abstract constructor too
23:20:24 <shachaf> elliott: Nonsense. _|_ === const _|_
23:21:53 <elliott> shachaf: Are you furthering your campaign of bothering me about things I said in other channels by going a step further and not actually bothering to read what I say before doing it?
23:22:01 <elliott> zzo38: I just renamed Lam to Abstract.
23:22:46 <shachaf> elliott: You said that safeDivide = _|_ is different from safeDivide = \x y -> _|_
23:24:11 <elliott> Sure, if you think that (\x y -> if y == 0 then x else ⊥) is ⊥.
23:24:11 <oerjan> > (const undefined `seq` "yeah", undefined `seq` "sure")
23:24:12 <lambdabot> ("yeah","*Exception: Prelude.undefined
23:39:59 <RocketJSquirrel> @TOMayorFord This guy at the dog park is pretending to be an 80s businessman on his phone. No way ppl actually talk like this. He's faking! about 2 hours ago \\ LOOK GUYS I JUST WANTED TO TELL THE MAYOR OF TORONTO ABOUT THIS DOG PARK GUY. TWITTER IS HARD. I'M IN OVER MY HEAD HERE about 2 hours ago
23:47:04 <zzo38> Instead of Graphics.Gloss.Picture.Picture then use something like this: class (Alternative f, MonadPlus f) => IsPicture f where { convexPolygon :: Path -> f x; thickLine :: Float -> Path -> f x; thickArc :: Float -> Float -> Float -> f x; translate :: Float -> Float -> f x -> f x; rotate :: Float -> f x -> f x; scale :: Float -> Float -> f x -> f x; recolor :: (Color -> Color) -> f x -> f x; };
23:53:12 <zzo38> Together with the mathematical laws that recolor is a functor, scale and rotate and translate follow the laws of Euclidean geometry, and to be known that the input ranges of the other functions should always be in range
23:53:16 <oerjan> zzo38: btw i saw yesterday there was a new version of gloss out
23:53:27 <zzo38> oerjan: Yes I saw that too
23:54:05 <zzo38> They did add playIO, but it still does not support return values, and Rotate is still clockwise (even though it should be counterclockwise in the opinion of myself and others)
23:55:56 <zzo38> What is your opinion of it?
23:56:08 <RocketJSquirrel> elliott: Web comic artist tries to tweet the mayor of Toronto about Dog Park Guy.
23:58:59 <zzo38> Because, mathematics is usually done counterclockwise, isn't it? (Horoscopes are also done counterclockwise but that isn't the point)