00:00:14 -!- drdanmaku has joined.
00:09:05 -!- Burton has quit (Write error: Connection reset by peer).
00:09:10 -!- mshock has joined.
00:26:24 -!- Burton has joined.
00:28:44 -!- ^v has quit (Ping timeout: 240 seconds).
00:31:44 -!- brrr has joined.
00:41:44 -!- ^v has joined.
01:01:15 -!- amenghra has joined.
01:36:35 -!- idris-bot has quit (Ping timeout: 264 seconds).
01:37:47 -!- Melvar has quit (Ping timeout: 264 seconds).
01:51:59 -!- amenghra has quit (Remote host closed the connection).
02:03:11 -!- amenghra has joined.
02:13:36 -!- mshock has quit (Ping timeout: 260 seconds).
02:15:39 -!- amenghra has quit (Remote host closed the connection).
02:18:40 -!- amenghra has joined.
02:33:18 -!- amenghra has quit (Remote host closed the connection).
02:58:44 -!- amenghra has joined.
03:08:26 -!- mshock has joined.
03:11:10 -!- oerjan has quit (Quit: Ribbit, probably).
03:32:30 -!- amenghra has quit (Remote host closed the connection).
03:33:56 -!- amenghra has joined.
03:38:26 -!- amenghra has quit (Remote host closed the connection).
03:49:28 -!- MDude has changed nick to MDream.
03:49:57 -!- MDream has quit (Read error: Connection reset by peer).
03:52:28 -!- drlemon has joined.
04:03:44 -!- mshock has quit (Ping timeout: 260 seconds).
04:09:07 -!- amenghra has joined.
04:12:23 -!- amenghra has quit (Remote host closed the connection).
04:12:36 -!- amenghra has joined.
04:16:12 -!- amenghra has quit (Remote host closed the connection).
04:35:00 -!- tromp has quit (Read error: Connection reset by peer).
04:36:35 -!- tromp_ has joined.
04:36:40 -!- amenghra has joined.
04:54:51 -!- amenghra has quit (Remote host closed the connection).
05:10:08 -!- MindlessDrone has joined.
05:14:12 -!- amenghra has joined.
05:25:58 -!- ^v has changed nick to ^8.
05:46:14 <fizzie> The DNS, it has been changed.
05:46:29 <fizzie> Now we just have to wait for it to PROPAGATE and then we're BACK in BUSINESS.
05:52:02 <coppro> who did the survey by the way?
05:52:40 <coppro> I just finally filled it out
05:53:29 <Sgeo> Who's the new hosting service?
05:54:24 <fizzie> The sleeping beargor woke up and did something; the old server's back up.
05:54:44 <Sgeo> So, does this make CloudAtCost not terrible?
05:55:29 <fizzie> Probably not; I mean, it was unavoidably down quite many days.
05:56:03 <fizzie> Hard to say when they fixed it, but the tweets suggest about ten days of average downtime.
06:02:08 -!- amenghra has quit (Remote host closed the connection).
06:20:12 -!- tromp_ has quit (Read error: Connection reset by peer).
06:23:51 -!- MoALTz_ has quit (Quit: Leaving).
06:30:48 -!- conehead has joined.
06:30:48 -!- conehead has quit (Changing host).
06:30:48 -!- conehead has joined.
06:36:34 <coppro> how am I supposed to survive without hackego :(
06:37:21 -!- conehead has quit (Quit: Textual IRC Client: www.textualapp.com).
06:37:29 <fizzie> `echo What do you mean?
06:37:53 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
06:38:04 <fizzie> It's the very same server.
06:38:21 -!- conehead has joined.
06:39:04 <coppro> `mkdir -p /etc/etc/etc/ad\ nauseam
06:39:05 <HackEgo> mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information.
06:39:14 <coppro> `mkdir -p "/etc/etc/etc/ad nauseam"
06:39:14 <HackEgo> mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information.
06:39:22 <HackEgo> Usage: mkdir [OPTION]... DIRECTORY... \ Create the DIRECTORY(ies), if they do not already exist. \ \ Mandatory arguments to long options are mandatory for short options too. \ -m, --mode=MODE set file mode (as in chmod), not a=rwx - umask \ -p, --parents no error if existing, make parent directories as needed \ -v, --verbose print
06:39:36 <coppro> `mkdir -p "/etc/etc/etc
06:39:37 <HackEgo> mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information.
06:39:39 <coppro> `mkdir -p /etc/etc/etc
06:39:40 <HackEgo> mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information.
06:41:22 <fizzie> You need to use `run if you have more than one argument.
06:41:32 <fizzie> Plain ` passes everything after the command as a single argument.
06:41:49 <coppro> `run mkdir -p "/etc/etc/etc/ad\ nauseam"
06:41:50 <HackEgo> mkdir: cannot create directory `/etc/etc': Permission denied
06:42:03 <HackEgo> chmod: changing permissions of `/etc': Operation not permitted
06:42:06 <fizzie> It's for making things like `addquote <someone> Whatever shell metacharacters may be here. to work without having to quote everything.
06:42:07 <HackEgo> chmod: changing permissions of `/': Operation not permitted
06:42:44 <HackEgo> 660) <Phantom_Hoover> Incest, the enemy of graph theorists everywhere.
06:43:07 <coppro> elliott this is all your fault
06:43:13 <HackEgo> cat: wisdom/alise: No such file or directory
06:43:38 <coppro> `run echo elliott's not hiding over here >alise
06:43:39 <HackEgo> bash: -c: line 0: unexpected EOF while looking for matching `'' \ bash: -c: line 1: syntax error: unexpected end of file
06:43:43 <coppro> `run echo elliott\'s not hiding over here >alise
06:43:49 <coppro> `run echo elliott\'s not hiding over here >/wisdom/alise
06:43:49 <HackEgo> bash: /wisdom/alise: No such file or directory
06:43:58 <coppro> `run echo elliott\'s not hiding over here >wisdom/alise
06:44:12 <coppro> `run mkdir -p etc/etc/etc/ad\ nauseam
06:45:00 -!- edwardk has joined.
06:45:46 <myname> is there some kind of weblist with all the quotes?
06:45:58 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/file/tip/paste/paste.7340
06:46:14 <coppro> see also wisdom.pdf in the topic
06:46:55 -!- brrr has quit (Quit: Cya!).
06:47:42 <coppro> `run addwep Monoids A monoid is just a subalgebra of the STR algebra, if you squint hard enough.
06:49:21 <coppro> fizzie: where's hackego's current site?
06:49:26 <coppro> it's not going to codu
06:57:42 <HackEgo> urbandictionary? ¯\(°_o)/¯
06:58:23 <coppro> `run addwep urbandictionary "Urban Dictionary is an alternative, inferior wisdom database."
07:06:45 <fizzie> What does "not going to codu" mean?
07:08:09 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
07:08:14 <coppro> the URL is out of date
07:08:23 <coppro> or my cache wasn't clearing
07:09:19 <fizzie> If you want to get technical, the "physical" address is http://www2.codu.org/projects/hackbot/fshg/
07:09:19 <coppro> `run addwep "works for me" "Error: unable to read wisdom database. try again later."
07:25:26 -!- AnotherTest has joined.
07:31:07 -!- edwardk has quit (Quit: Computer has gone to sleep.).
07:46:21 <coppro> the physical address is probably an IP address hth
08:14:12 -!- Tritonio has joined.
08:17:27 -!- Melvar has joined.
08:39:40 -!- Patashu has joined.
09:11:30 -!- drdanmaku has quit (Quit: Connection closed for inactivity).
09:15:36 -!- tromp has joined.
09:39:52 -!- idris-bot has joined.
09:50:50 <HackEgo> #!/bin/sh \ echo "$2" > "wisdom/$1"
09:59:04 -!- mhi^ has joined.
10:00:37 -!- idris-bot has quit (Quit: Terminated).
10:00:53 -!- idris-bot has joined.
10:02:47 <shachaf> so why do you say e.g. "tiedätko sinä suomea" instead of "sinä tiedatko suomea"
10:03:01 <shachaf> is it like the english weirdness where you switch the order of words when you ask a question
10:03:35 <shachaf> (of course "sinä" is optional in the first place, if i understand correctly, but nevertheless)
10:04:13 <Taneb> Because languages are weird?
10:04:17 <fizzie> That would be "tiedätkö", and I think people would generally say "puhutko", if you're talking about the language.
10:05:00 <shachaf> fizzie: i know but i was trying to use a different verb for once because i've been using "puhua"too mcuh :'(
10:05:13 <fizzie> But yes, it's some sort of "special sentence order for questions" thing.
10:05:54 <fizzie> The word that denotes it is a question is moved to the front, or some-such.
10:06:33 <fizzie> You can sometimes put the interrogative suffix (-ko, -kö) into different words in order to denote emphasis.
10:07:07 <fizzie> "Puhutko sinä suomea?" do you speak Finnish, with no particular special emphasis -- "Suomeako sinä puhut?!" do you speak *Finnish*?!
10:07:39 <fizzie> In the latter order, it has "out of all possible languages, you're speaking Finnish! what's wrong with you!" connotations.
10:07:57 <shachaf> ah, it's always on one word, but you can choose which one?
10:08:22 <fizzie> Yes. "Sinäkö puhut suomea?" would also be legal.
10:08:34 <fizzie> When you're trying to find the one Finnish speaker in a group, for example.
10:09:01 <fizzie> As in, "is it you who speaks Finnish
10:09:07 <shachaf> what if you want special emphasis on the verb
10:10:53 <shachaf> by the way, are questions pronounced by raising your voice a little bit toward the end of the sentence, as in english and other languages?
10:11:22 <fizzie> I guess the first variant technically emphasizes the verb, it's just that it's the most common/expected so it doesn't feel special.
10:12:02 <fizzie> And I don't think there's a rising intonation for questions. At least nothing as dramatic.
10:12:21 <shachaf> isn't even just saying "sinä" a sort of emphasis?
10:12:47 <fizzie> Yes, it is, since it's not necessary.
10:14:14 <fizzie> So you could use "puhutko sinä suomea", possibly with a bit more stress on "sinä", in the aforementioned "trying to find the elusive Finn" scenario; and you'd probably just ask "puhutko suomea?" if you're asking someone in general.
10:14:26 -!- boily has joined.
10:14:31 <fizzie> (Language names aren't capitalized, incidentally.)
10:14:32 <shachaf> how do you decide whether to add it in or not
10:15:04 <shachaf> i suppose i can analogize to hebrew except it's not as common there
10:15:24 <shachaf> Yes, I was wondering about that.
10:17:27 <fizzie> Proper nouns, generally.
10:17:45 <fizzie> But not many things that English does, like days of the week, or months of the year.
10:18:21 <fizzie> Names of countries are, but their languages aren't, and the nouns for the peoples aren't either.
10:18:38 <fizzie> So the country is "Suomi" but the language is "suomi" and a Finn is "suomalainen".
10:19:30 <shachaf> If the language is "suomi", how does one arrive at "suomea"?
10:21:00 <fizzie> I'm sure there's some good rule. The final i does turn to an e in all inflected forms of "suomi" I can think of.
10:21:10 <fizzie> "suomea" would be the partitive case.
10:21:24 <fizzie> http://en.wiktionary.org/wiki/Appendix:Finnish_declension/ovi
10:21:43 <fizzie> "KOTUS type 7 (ovi): Two-syllable nominals ending with -i; consonant gradation possible. All other cases replace -i with -e-. Partitive ending -a/-ä and genitive plural ending -en. -e- of stem dropped before plural marker -i-."
10:24:00 <fizzie> Not all words that end in -i work that way. There's e.g. http://en.wiktionary.org/wiki/Appendix:Finnish_declension/risti
10:24:16 <HackEgo> [wiki] [[Special:Log/newusers]] create * Fansdesks * New user account
10:24:23 <shachaf> Google Translate translates "Do you speak English?" to "Puhutko Englanti?". Should it be "Puhutko englantia?"?
10:24:25 <fizzie> "Two-syllable nominals ending with -i; consonant gradation possible. Partitive ending -a/-ä and genitive plural ending -en. -i of stem changes to -e- before plural marker -i-, except in genitive plural, where it is dropped."
10:24:35 <fizzie> Yes, the latter would be correct.
10:24:38 <shachaf> (Or maybe "Puhutteko", of course.)
10:25:02 <fizzie> "puhuttekste", if you're speaking colloquially and in plural.
10:25:12 <shachaf> Oh well. Google Translate isn't very trustworthy.
10:25:20 <fizzie> Also if you wanted a closer analogue of "do you know Finnish?" it would possibly be "osaatko suomea?"
10:26:36 <fizzie> "puhuttekste suomee?" or "puhutsä/puhuksä suomee?" would be colloquial/slangy/dialecty/vernacular versions of "puhutteko suomea?" and "puhutko suomea?"
10:27:30 <fizzie> As close as I can transcribe, anyway; they're more spoken stuff, though I'm sure some people write like that in chat.
10:28:14 <fizzie> Kids these days write "onx" for "onko", anyway. Or so I hear.
10:29:44 <shachaf> I still need to figure out what people are talking about when they say "partitive".
10:30:01 <shachaf> Three-year-olds speak Finnish just fine without knowing all that. :-(
10:30:40 <fizzie> I don't know why we have a partitive case.
10:31:06 <fizzie> "As an example of the irresultative meaning of the partitive, ammuin karhun (accusative) means "I shot the bear (dead)", whereas ammuin karhua (partitive) means "I shot (at) the bear" without specifying if it was even hit."
10:33:26 <shachaf> Do you happen to have any other examples?
10:34:04 <fizzie> That was from http://en.wikipedia.org/wiki/Partitive_case which has (single) examples of the various different contexts for the partitive.
10:34:18 <fizzie> The "used with uncountable nouns" case is the one I'd've thought of first.
10:35:26 <fizzie> If there's a difference between "saanko lainata kirjaa?" (one of the examples) and "saanko lainata kirjan?", it's a very subtle one.
10:36:02 <fizzie> The "luen kirjaa" / "luen kirjan" pair is more clear.
10:52:28 <HackEgo> [wiki] [[User:Fansdesks]] N http://esolangs.org/w/index.php?oldid=40161 * Fansdesks * (+1418) Created page with "Hard work is one way to gain an impressive number of followers on Instagram. But there’s another way: Just [http://fansdesk.info/buy-instagram-followers/ Buy Instagram Follo..."
10:53:54 <HackEgo> [wiki] [[Special:Log/delete]] delete * Ehird * deleted "[[User:Fansdesks]]": Hard work is one way to gain an impressive number of visits to your website. But there’s another way: Just Spam Web Sites.
10:54:07 <HackEgo> [wiki] [[Special:Log/block]] block * Ehird * blocked [[User:Fansdesks]] with an expiry time of indefinite (account creation disabled, email disabled, cannot edit own talk page): Spamming links to external sites
10:57:48 -!- AfkSoul has changed nick to TieSoul.
11:09:08 -!- edwardk has joined.
11:11:54 -!- boily has quit (Quit: Poulet!).
11:19:44 -!- conehead has quit (Quit: Computer has gone to sleep).
11:32:52 -!- edwardk has quit (Ping timeout: 240 seconds).
12:00:25 -!- Sgeo has quit (Read error: Connection reset by peer).
12:09:53 <Taneb> I kind of wish Haskell wasn't the first language I got really into
12:10:08 <Taneb> Because I always miss a lot of its features in pretty much any other language
12:10:22 <Taneb> And I try to write programs in other languages as though they were Haskell
12:11:38 <b_jonas> Taneb: do you mean you use camelCase instead of underscored_names?
12:11:56 <Taneb> Among other things
12:12:16 <b_jonas> some people do that in C++ independently of haskell
12:16:37 -!- yorick has joined.
12:23:05 <fizzie> Everybody does it in Java and C#, thanks to the standard libraries doing it.
12:33:59 -!- oerjan has joined.
12:38:22 <Taneb> I don't think I shall cosplay on Saturday
12:38:39 <oerjan> will you sinplay instead
12:39:17 <Taneb> No, but I may cotplay
12:48:56 <HackEgo> #!/bin/sh \ echo "$2" > "wisdom/$1"
12:49:20 <HackEgo> ls: cannot access wisdom/*onoi*: No such file or directory
12:49:31 <HackEgo> wisdom/hthmonoid \ wisdom/monoid \ wisdom/monoidal category \ wisdom/monoids \ wisdom/Monoids
12:49:43 <shachaf> fizzie: how would i say "i'm talking about finnish"?
12:49:49 <shachaf> Wow, wisdom/ is such a mess
12:49:54 <HackEgo> hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids ...
12:50:00 <oerjan> shachaf: coppro messed it up yesterday
12:50:20 <HackEgo> Monoids are the easy version of categories.
12:50:29 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
12:51:24 <shachaf> oerjan: What we really need is a version of `learn that lets you specify your own name and splits on the first whitespace.
12:51:35 <shachaf> What I really need is to go to sleep.
12:51:47 <oerjan> shachaf: well `addwep is obviously a broken attempt at that
12:52:15 <shachaf> There's no way a program run with `run could ever do it.
12:56:23 <HackEgo> Monoids are just categories with a single object.
12:56:27 <HackEgo> Monoids are the easy version of categories.
12:56:31 <HackEgo> Monoids are the easy version of categories.
12:56:50 <oerjan> that won't ever be shown by `? anyway
12:57:05 <HackEgo> Urban Dictionary is an alternative, inferior wisdom database.
12:57:17 <HackEgo> Error: unable to read wisdom database. try again later.
12:59:59 <fizzie> shachaf: "Puhun suomen kielestä", probably, to make it more explicit (than "puhun suomesta").
13:01:35 <fizzie> Or "tarkoitan suomea/suomen kieltä" for a different sense of "I'm talking about X".
13:02:56 <HackEgo> Monoidal categories are just 2-categories with a single object.
13:05:51 <Taneb> b_jonas, what language will you be using?
13:06:03 <b_jonas> Taneb: I probably won't be doing anything this year
13:06:20 <b_jonas> I'll read the task and spend time on it only if it seems very interesting AND if I have time
13:06:35 <b_jonas> I will definitely read the task though, this is a spectator sport
13:06:38 <Taneb> Well, I know that I have the time
13:07:27 <Taneb> I would do it with my programmer housemate, but our common languages are Python and C, and I'm not all that great at C and neither of us particularly like Python
13:08:27 <b_jonas> Taneb: combine multiple languages then
13:08:44 <Taneb> He's a C++ guy and I'm a Haskell guy
13:08:48 <Taneb> The result may not be pretty
13:09:02 <b_jonas> well, that could depend on the task I guess
13:09:09 <olsner> or one of you writes the code in the language of choice, and the other works on analyzing the problem
13:09:31 <Taneb> olsner, that may be a better idea
13:09:33 <b_jonas> Taneb: have you looked at the background of the http://icfpcontest.org/ webpage, http://icfpcontest.org/images/bkg.png ?
13:09:46 <olsner> based on some earlier icfps there might be separate tasks to work on independently though
13:10:07 <Taneb> b_jonas, not in great detail
13:10:26 <b_jonas> it seems to have a pattern made of squares of two different colors
13:17:08 <b_jonas> oh, and its size isn't even divisible with the size of those squares
13:17:15 <Taneb> http://i.imgur.com/jDaoHBg.png
13:17:21 <Taneb> That's it in black and white
13:18:09 <b_jonas> the webpage might come form https://github.com/icfpcontest2014/icfpcontest2014.github.io
13:19:54 <b_jonas> (I'm more of a perl and C++ person anyway)
13:21:02 <Taneb> Looks like I'm teaming up with my housemate
13:36:07 <olsner> hmm, so is the background a hidden message of some sort?
13:46:37 <b_jonas> I don't think so, but it could be
13:54:26 -!- Patashu has quit (Quit: Soundcloud (Famitracker Chiptunes): http://www.soundcloud.com/patashu MSN: Patashu@hotmail.com , AIM: Patashu0 , YIM: patashu2 , Skype: patashu0 .).
14:01:26 -!- conehead has joined.
14:02:28 -!- ais523_ has joined.
14:27:34 -!- ^8 has changed nick to ^v.
14:35:07 -!- edwardk has joined.
14:39:54 -!- edwardk has quit (Read error: Connection reset by peer).
14:53:33 -!- VorpalPhone has joined.
14:53:39 -!- VorpalPhone has quit (Client Quit).
14:58:07 -!- heroux has quit (Ping timeout: 245 seconds).
14:58:08 -!- nooodl has joined.
14:59:39 -!- heroux has joined.
15:31:18 <elliott> fizzie: yay at the wiki being back
15:31:23 <elliott> any plans to move it still?
15:40:59 <fizzie> Well, I mean, I'll think about it, but *lazy*
15:42:23 -!- mshock has joined.
15:42:34 <elliott> how about I move it and you maintain it after that so I can sleep at night? :p
15:45:19 -!- Tritonio has quit (Ping timeout: 256 seconds).
15:52:45 <fizzie> Calm down, it's only ones and zeroes.
15:54:55 <elliott> it will be very very dark and I will be eaten by a graue for letting the wiki fall into such bargain basement hosting :(
15:56:07 <ais523_> have computers improved to the stage where they can actually run MediaWiki yet?
15:56:09 -!- oerjan has quit (Quit: leaving).
15:58:55 <HackEgo> [wiki] [[SYCPOL]] M http://esolangs.org/w/index.php?diff=40162&oldid=40089 * GermanyBoy * (+1) /* Character set */ '='-character
16:25:33 -!- nys has joined.
16:30:31 <ais523_> @djinn ((a -> Void) -> Void) -> a
16:30:45 <ais523_> saw that one in an article talking about the Curry-Howard correspondence
16:31:07 <ais523_> it's a true statement in most logics, but the article claims (without proof) that it can't be expressed in lambda calculus
16:31:12 <elliott> it's double-negation elimination.
16:31:24 <elliott> intuitionistic type theory corresponds to intuitionistic logic.
16:31:32 <elliott> double-negation elimination is equivalent to LEM
16:32:07 <ais523_> and the standard lambda calculus type system models intuitionistic logic, presumably
16:32:09 <elliott> ais523_: if you had that function you could write a term of type (Either a (a -> Void))
16:32:13 <ais523_> wasn't quite sure which logic it corresponded to
16:32:23 <elliott> your intuition should be enough to tell you that's impossible without _|_
16:32:47 <elliott> I don't think there's a standard lambda calculus type system :)
16:33:18 <ais523_> elliott: hmm, perhaps; you can talk about "typed lambda calculus" without people shouting at you, though
16:33:53 <ais523_> the one I know is identity, weakening, abstraction, application, and the main point of contention is whether contraction should be implicit or explicit
16:34:12 <elliott> the STLC is a rather boring logic, at least
16:34:59 <ais523_> elliott: hmm, that (Either a (a -> Void)) type reminds me of the halting problem, in a way
16:35:27 <elliott> ais523_: because it's a decision procedure for every proposition?
16:35:55 <ais523_> although, there's a different problem
16:36:10 <ais523_> which is that given two different Voids, you can't even construct Void1 -> Void2 in Haskell, I don't think
16:36:14 <ais523_> perhaps you could with a pattern match
16:36:22 <ais523_> you just write let voidconvert v = case v of
16:36:27 <ais523_> and that's the entire function
16:36:37 <ais523_> somehow I don't think that's valid syntax, though
16:36:59 <b_jonas> dunno, I think I was just laughing at "standard lambda calculus type system" too
16:37:33 <ais523_> I have problems (at work) with people assuming things are standardised when they actually aren't
16:38:25 <ais523_> is it possible to write a pattern match with zero cases in Haskell?
16:39:31 <Vorpal> TLS certificates are such a pain to deal with :/
16:41:27 <ski> ais523_ : <https://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#empty-case>
16:41:52 <ski> @djinn Void -> a
16:42:32 <ski> @djinn-add type NotNot a = Not (Not a)
16:42:43 <ski> @djinn NotNot (Either a (Not a))
16:42:43 <lambdabot> f a = void (a (Right (\ b -> a (Left b))))
16:43:08 <ski> `void' is `void v = case v of {}'
16:43:09 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: void': not found
16:43:31 <ski> @type either
16:43:32 <lambdabot> (a -> c) -> (b -> c) -> Either a b -> c
16:43:43 <ski> void :: Void -> a
16:45:17 <ais523_> ski: thanks, was just reading that page
16:45:32 <elliott> ais523_: you can interconvert given absurd :: VoidN -> a
16:45:56 <ais523_> elliott: yeah, the point was that the empty case lets you define absurd in the first place
16:46:01 <elliott> which is implementable for "newtype Void = Void (forall a. a)" and "newtype Void = Void Void" with no extra extensions
16:46:05 <elliott> and "data Void" with the empty case extension
16:46:18 <elliott> (note that the first one requires the RankNTypes extension to state)
16:46:18 <ais523_> also, something I learned from that page is that OCaml's "function" keyword doesn't have a Haskell equivalent by default, but GHC implements it as "\case"
16:46:26 <elliott> absurd x = x `seq` undefined is also an OK implementation
16:46:34 <elliott> because you can proof that the _|_ is never reached
16:46:39 <ski> (the first one really only requires `PolymorphicComponents')
16:47:01 <ais523_> elliott: anyway, I read up about rank N and rank 2 types a bunch because it was relevant to my research
16:47:07 <elliott> (even absurd _ = undefined is fine, really, since you have to abandon _|_ inputs anyway)
16:47:12 <ski> ais523_ : yes, it's a bit sad that we had to wait so long for it
16:47:26 <ais523_> it turns out that type inference for rank 2 types is actually decidable, but ghc doesn't currently infer it
16:47:55 <ski> in SML, `if foo then bar else baz' is sugar for `case foo of true => bar | false => baz' is sugar for `(fn true => bar | false => baz) foo'
16:48:01 <zzo38> ais523_: Would that be a reason to have separate extensions for rank 2 and rank N?
16:48:11 <ski> zzo38 : it could be
16:48:13 <ais523_> zzo38: possibly it would be
16:48:31 <ski> (and currently both exist as separate extensions)
16:48:37 <elliott> Rank2Types is deprecated I think
16:48:56 <ais523_> ski: in OCaml, I'd guess that the primitive would be "match foo with True -> bar | False -> baz"
16:49:11 <ais523_> or maybe "(function True -> bar | False -> baz) foo"
16:49:26 <ais523_> so yeah, it's probably the same as SML in that respect
16:50:32 <ski> ais523_ : "something I learned from that page", which page ?
16:50:40 <ais523_> btw, a quirk of Reddit I've been noticing: if an article gets a really large number of comments, the best ones are on the second page
16:50:45 <ais523_> ski: the one you most recently linked to me
16:51:02 <ais523_> some background: I work in type theory research, and don't really use Haskell, but sometimes I use it to test out theories
16:51:04 * ski can't see OCaml mentioned at it
16:51:23 <ais523_> ski: oh, that's because I know much of OCaml quite well, but not really Haskell
16:51:37 <ais523_> so if I learn something new about the comparison between OCaml and Haskell, it's normally on the Haskell side
16:52:00 <ski> in Agda2, one'd write `void' differently
16:52:23 <ski> void : {A : Set} -> Void -> A
16:52:38 <ski> `()' is an absurd pattern
16:52:38 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: ()': not found
16:52:53 <ski> (and if you use it, you don't need a definiens)
16:53:32 <ski> (actually, imo, it could make more sense to allow a definiens here)
16:53:57 * ski idly wonders which part of type theory ais523_ works on
16:54:01 <ais523_> ski: Agda2 has explicit foralls?
16:54:15 <ais523_> ski: finite-state type theory, especially affine logics
16:54:18 <ski> what do you mean by "explicit foralls" ?
16:54:31 <ais523_> the System F style where you have a type parameter to functions
16:54:47 <ais523_> rather than the OCaml style where you write 'a and it implies a type parameter for 'a
16:54:52 <ski> well, it's just dependent functions
16:55:05 <ski> however, Agda2 (and Agda1) has implicit arguments
16:55:19 <ski> with explicit arguments, the above would just look like
16:55:29 <ski> void : (A : Set) -> Void -> A
16:56:03 <ski> you can also say stuff like
16:56:07 -!- yorick has quit (Read error: Connection reset by peer).
16:56:35 <ais523_> right, in a dependent type system, there's no difference between a lowercase (value) lambda and an uppercase (type) lambda, because values and types are combined
16:56:36 <ski> _++_ : {A : Set} -> {m : Nat} -> {n : Nat} -> Vector A m -> Vector A n -> Vector (m + n)
16:56:43 <ski> _+_ : Nat -> Nat -> Nat
16:56:58 <ski> Vector : Set -> Nat -> Set
16:57:45 <ski> in `_++_', the `m' and `n' natural length arguments are implicit
16:58:17 <ski> (since usually when you use `_++_', you apply it to arguments so that `m' and `n' can be inferred)
16:58:56 <ski> i've not heard the name "finite-state type theory" before
16:59:20 <ski> is it like a version of "of course", indexed with a natural number expressing how many times you may use the resource ?
16:59:27 <ais523_> well it's a pretty small niche, because it's sub-TC by definition
16:59:34 <ais523_> ski: that's "bounded contraction", which is part of it
16:59:42 <ais523_> a whole chapter of my thesis is on the subject
16:59:54 <ais523_> where I argue that there's a design error in all the bounded contraction type systems I'm aware of
17:00:01 <ais523_> err, the non-dependently-typed ones, that is
17:00:05 <ski> sounds interesting
17:00:15 <ski> (are there any dependently-typed ones ?)
17:00:28 <ais523_> yes, but they're massively complex and I don't really understand them
17:00:43 <ais523_> they noticed the same error I did, and worked around it using a hideously complex dependent typing variant
17:00:54 <ais523_> whereas I'm working around it with intersection types
17:01:31 <ais523_> the basic problem's to do with the fact that the contraction bounds aren't properly polymorphic
17:01:47 <ski> i only recall seeing some notes by Pfenning that didn't treat the quantifiers in a substructural way, iirc
17:02:24 <ais523_> b_jonas: it's not that bad, being sub-TC is sort-of a magic fix for half the problems in type theory
17:02:30 <ais523_> because all of a sudden, you can solve problems by brute force
17:02:48 <b_jonas> maybe I should try to ask this channel about non-eso theoretic problems
17:02:52 <ais523_> that said, one of my major results is that SCC (and similar type systems) have decidable type inference
17:02:54 <ski> "sub-TC" means substructural variants of Type Theory, yes ?
17:03:33 <ais523_> ski: well, in this case, I just mean that with relatively normal semantics, programs in the type systems in question have decidable inference
17:03:50 <ais523_> which implies that the languages can't be Turing-complete
17:04:14 -!- shikhin has joined.
17:05:00 <ais523_> finite-state languages are those in which the semantics of any program can be represented as a state machine
17:05:20 <elliott> ski: total functional programming languages don't necessarily need substructural type systems...
17:05:28 <elliott> Agda and Coq aren't considered subtructural, are they?
17:05:37 <ais523_> that said, I am using substructural type systems
17:05:40 <elliott> well, this gets back to how ambiguous "TC" is :/
17:05:42 <ais523_> elliott: do Agda and Coq have decidable equivalence?
17:05:51 <elliott> but I'm pretty sure you can model brainfuck in a substructural type system too
17:05:57 <ais523_> oh, I guess you have to define what equivalence is
17:06:02 <ais523_> because in a total language, all programs halt
17:06:12 <ais523_> thus the halt status of any two programs is the same for any given input
17:06:18 <ais523_> so the "normal" definition isn't going to work
17:06:23 <ski> elliott : i know. i was just initially thinking "sub" here was short for "substructural"
17:06:59 <ais523_> ah right, "sub-TC" means "does not live up to (is below) the status of Turing Completeness"
17:07:16 <ski> (hm, for some strange reason i was seeing "TT" instead of "TC")
17:07:25 <ais523_> which is quite common in esolangs by new designers which are not BF derivatives
17:07:49 <ais523_> (actually some of the BF derivatives are sub-TC too, which should be really embarrassing for the designers unless that was intentional)
17:08:24 <b_jonas> wait, do you mean that variant that takes the program as unary?
17:08:54 <ski> hm, the world needs a dependently typed turing tar pit esolang
17:09:21 <elliott> ais523_: I like the implication that TC is high-status.
17:10:02 <ais523_> incidentally, New Scientist was busy talking about apparently serious efforts to construct a super-Turing computer
17:10:16 <ais523_> the researchers wanted to create an analog computer that processed arbitrary-precision reals, I think
17:10:26 <ais523_> somehow I don't think they'll succeed
17:10:32 <ais523_> although it would be great if they did
17:10:40 <ais523_> ski: I wonder what that would look like
17:11:03 <ais523_> I guess it'd either be dependently typed lambda calculus, or something unlambda-style with combinators
17:11:16 <ais523_> (normally I'd explain combinators but based on your nick, I don't think there's a need)
17:12:05 -!- TieSoul has changed nick to AfkSoul.
17:14:11 -!- AfkSoul has changed nick to TieSoul.
17:14:46 -!- mshock_ has joined.
17:14:47 <zzo38> Did you know that? One reason I try to write my own Famicom emulator is because I don't like hash checking and I don't like the method of loading FDS programs that most emulators use.
17:15:35 -!- AnotherTest has quit (Ping timeout: 264 seconds).
17:17:03 -!- mshock has quit (Ping timeout: 240 seconds).
17:35:54 -!- AnotherTest has joined.
17:40:52 -!- mshock_ has quit (Ping timeout: 240 seconds).
17:51:24 -!- TieSoul has quit (Read error: Connection reset by peer).
18:07:21 <HackEgo> [wiki] [[Special:Log/newusers]] create * JuliannCoffin * New user account
18:08:15 -!- TieSoul has joined.
18:11:00 -!- mshock has joined.
18:21:40 -!- rgbMode has joined.
18:35:13 <TieSoul> The message isn't showing anymore
18:35:50 <ais523_> TieSoul: I've seen occasional edits
18:35:55 <ais523_> so it's not read-only any more
18:36:20 <TieSoul> I have two languages that aren't on there
18:38:36 <HackEgo> [wiki] [[Special:Log/newusers]] create * TieSoul * New user account
18:39:35 -!- rgbMode has left ("Leaving").
18:41:56 <HackEgo> [wiki] [[User:TieSoul]] N http://esolangs.org/w/index.php?oldid=40163 * TieSoul * (+93) Created page with "List of languages created by TieSoul, in chronological order: * [[Befunk]] * [[Replacefuck]]"
18:41:58 <ski> ais523_ :)
18:42:09 -!- MindlessDrone has quit (Quit: MindlessDrone).
18:44:27 * ski . o O ( <https://en.wikipedia.org/wiki/Blum%E2%80%93Shub%E2%80%93Smale_machine> Iä ! )
18:48:25 <Bike> smale's cool. imo read his problems
19:10:15 -!- TieSoul has changed nick to AfkSoul.
19:10:27 -!- AfkSoul has changed nick to TieSoul.
19:28:26 -!- nooodl_ has joined.
19:28:56 -!- nooodl_ has quit (Client Quit).
19:33:11 -!- MoALTz has joined.
19:35:36 -!- mhi^ has quit (Quit: Lost terminal).
19:41:15 -!- mhi^ has joined.
19:49:35 -!- shikhout has joined.
19:52:17 -!- shikhin has quit (Ping timeout: 245 seconds).
20:01:06 -!- nys has quit (Ping timeout: 260 seconds).
20:04:32 <HackEgo> [wiki] [[Special:Log/upload]] upload * TieSoul * uploaded "[[File:Befunk-euler1.png]]": Project Euler problem 1 in Befunk.
20:07:18 -!- yorick has joined.
20:08:24 <HackEgo> [wiki] [[Befunk]] N http://esolangs.org/w/index.php?oldid=40165 * TieSoul * (+6031) Created the page.
20:17:19 -!- conehead has quit (Ping timeout: 256 seconds).
20:18:58 -!- conehead has joined.
20:23:12 -!- AnotherTest has quit (Ping timeout: 245 seconds).
20:24:27 -!- AnotherTest has joined.
20:25:50 -!- mshock has quit (Ping timeout: 260 seconds).
20:37:00 -!- mshock has joined.
20:38:12 <HackEgo> 498) <CakeProphet> monqy: help how do I use lambdabot to send messages to people. [...around half an hour later...] <CakeProphet> @messages <lambdabot> quicksilver said 1y 2m 18d 19h 54m 29s ago: you use @tell
20:40:02 -!- not^v has joined.
20:41:40 <elliott> I still can't fucking believe that
20:42:56 <ais523_> actually, we missed a trick
20:43:03 <ais523_> should have waited for them to leave and then sent the message again
20:43:09 <ais523_> @tell CakeProfit you use @tell
20:43:17 <ais523_> hopefully in a few years we can set a new record
20:43:30 <ais523_> @tell CakeProphet you use @tell
20:43:30 -!- not^v has changed nick to ^4.
20:43:43 <elliott> he uses different nicks these days.
20:44:49 <ais523_> good, that'll increase the timeframe before it happens again
20:45:42 <ais523_> it's just the "possibly" I care about
20:45:47 <ais523_> I don't really mind if it never happens
20:49:03 -!- edwardk has joined.
21:02:16 -!- nys has joined.
21:02:51 <int-e> profit, prophet ... Dogma was a nice movie.
21:08:27 <Taneb> Today I found out that one of the lecturers here, his research seems to include Eodermdrome
21:09:20 <ais523_> well I don't lecture you (at least, not in person physically), so presumably other people have been picking up my esolang without me being aware of it
21:09:45 <Taneb> ais523_, I don't mean the language specifically, but certainly something resembling it quite closely
21:09:52 <Taneb> Detlef Plump, if the name is familiar
21:11:21 <int-e> graph rewriting is a serious research topic
21:11:34 <ais523_> and yes, graph rewriting is not just me, I've seen it elsewhere
21:12:14 <Taneb> It was just described to me by someone who had attended a seminar about a language based on replacing subgraphs with a shape similar to a given one
21:12:26 <Taneb> Which in my head immediately rang bells
21:13:35 <elliott> detlef plump is a great name
21:14:28 <ais523_> huh, for me, esolangs.org is showing the "read-only" notice and has no CSS
21:14:48 <ais523_> Login error There is no user by the name "ais523". Usernames are case sensitive. Check your spelling, or create a new account.
21:15:04 <ais523_> must be that the DNS hasn't propagated
21:15:16 <ais523_> because it's mentioning fail.esolangs.org in the retrieved pages
21:15:33 <fizzie> Did you try reloading with all kinds of modifier keys already?
21:16:57 <Taneb> ais523_, could you have a gander at http://www.cs.york.ac.uk/plasma/publications/pdf/Plump.CAI.09.pdf ?
21:17:09 <ais523_> fizzie: I tried control-shift-R
21:17:14 <ais523_> my guess is that it's DNS-related
21:17:58 <fizzie> Well, it can be both. But also the esolangs.org DNS records have pretty long TTLs.
21:18:04 <ais523_> Taneb: it's much more complex than eodermdrome
21:18:22 <Taneb> I think the core is the same
21:18:24 <fizzie> (I had to shift-reload for Chrome to pick up a new DNS entry; they've got their own resolver, I guess it has a cache too.)
21:19:12 <Taneb> Now I wish I knew this lecturer so I could tell him about Eodermdrome
21:19:18 <ais523_> Taneb: not really, the core's more general by being more complex, I think
21:19:46 <ais523_> it allows combinations of "must have an edge" and "can't have an edge" that don't exist in Eodermdrome
21:19:50 <zzo38> If you tell the proper IP address then maybe you can manually override it temporarily.
21:19:51 <ais523_> but apart from that it's quite similar
21:20:07 <ais523_> I think the difference is that that language is designed for working on existing graphs
21:20:14 <ais523_> that aren't designed specifically to work with it
21:20:23 <ais523_> whereas in Eodermdrome, you use the graph for data storage and flow control and everything
21:21:00 <ais523_> Taneb: tell him about it anyway, I might end up getting a citation :-)
21:21:28 <Taneb> I'm afraid I've never met him.
21:21:35 <Taneb> I think I have him next term for something
21:21:38 <ais523_> oh, the other really big difference
21:21:44 <ais523_> is that the nodes are labelled in that language
21:21:48 <ais523_> and they all look the same in Eodermdrome
21:23:37 -!- AnotherTest has quit (Ping timeout: 256 seconds).
21:24:27 <Taneb> But if I get talking to him I promise I'll mention it!
21:30:10 -!- oerjan has joined.
21:33:52 -!- mshock has quit (Ping timeout: 272 seconds).
21:38:02 -!- ais523_ has quit (Quit: Page closed).
21:52:00 -!- conehead has quit (Quit: Computer has gone to sleep).
22:00:56 -!- mshock has joined.
22:13:29 -!- not^v has joined.
22:15:52 -!- ^4 has quit (Ping timeout: 250 seconds).
22:20:11 -!- brrr has joined.
22:30:51 -!- oerjan has set topic: El canal que se pregunta por qué los usuarios de Canaima vienen aquí, a pesar de que no hablamos español. | brainfuck survey: https://www.surveymonkey.com/s/L82SNZV | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/.
22:31:34 <oerjan> if someone understands spanish they might fix the grammar (i only managed to fix hablamos)
22:33:10 <zzo38> I am not Spanish, so I don't know.
22:33:32 <oerjan> i did not expect you to be
22:33:49 <shachaf> Most Spanish speakers aren't Spanish.
22:34:00 <oerjan> i don't know how many spanish speakers there are in british columbia.
22:34:16 <zzo38> I don't know either, but probably there are some.
22:35:07 <shachaf> Olen suomalainen, mutta en puhu suomea. :-(
22:35:49 * oerjan guessed right what that meant
22:36:14 <oerjan> i must have absorbed some from all the discussions here
22:45:16 <oerjan> <ski> (and currently both exist as separate extensions) <-- i vaguely recall Rank2Types is just a (deprecated) synonym for RankNTypes nowadays.
22:48:34 <oerjan> @ask ais523 <ais523_> btw, a quirk of Reddit I've been noticing: if an article gets a really large number of comments, the best ones are on the second page <-- wait how do you read reddit comments such that it's divided into pages
22:49:33 <Melvar> I seem to have missed a talking about dependent types in here, and they didn’t even use idris-bot.
22:53:23 -!- not^v has quit (Ping timeout: 264 seconds).
22:57:28 -!- Sgeo has joined.
23:00:56 -!- not^v has joined.
23:02:54 -!- conehead has joined.
23:05:35 -!- MoALTz has quit (Quit: Leaving).
23:08:22 -!- not^v has quit (Ping timeout: 240 seconds).
23:31:40 -!- Melvar has quit (Ping timeout: 272 seconds).
23:32:03 -!- idris-bot has quit (Ping timeout: 240 seconds).
23:37:33 -!- mshock has quit (Ping timeout: 240 seconds).
23:42:38 <HackEgo> [U+1D40 MODIFIER LETTER CAPITAL T]
23:43:13 <oerjan> i dunno it's a bit square
23:43:34 -!- mhi^ has quit (Quit: Lost terminal).
23:51:58 -!- yorick has quit (Read error: Connection reset by peer).
23:56:49 -!- Melvar has joined.