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 The DNS, it has been changed. 05:46:29 Now we just have to wait for it to PROPAGATE and then we're BACK in BUSINESS. 05:50:58 :D 05:50:59 what DNS? 05:51:54 esolangs.org. 05:51:56 :D 05:52:02 who did the survey by the way? 05:52:40 I just finally filled it out 05:53:29 Who's the new hosting service? 05:53:53 It's not new. 05:54:24 The sleeping beargor woke up and did something; the old server's back up. 05:54:44 So, does this make CloudAtCost not terrible? 05:55:29 Probably not; I mean, it was unavoidably down quite many days. 05:56:03 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 how am I supposed to survive without hackego :( 06:37:21 -!- conehead has quit (Quit: Textual IRC Client: www.textualapp.com). 06:37:29 `echo What do you mean? 06:37:29 What do you mean? 06:37:48 :O 06:37:50 he's back! 06:37:53 `help 06:37:53 Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ 06:38:04 It's the very same server. 06:38:21 -!- conehead has joined. 06:39:04 `mkdir -p /etc/etc/etc/ad\ nauseam 06:39:05 mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information. 06:39:14 `mkdir -p "/etc/etc/etc/ad nauseam" 06:39:14 mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information. 06:39:21 `mkdir --help 06:39:22 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 `mkdir -p "/etc/etc/etc 06:39:37 mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information. 06:39:39 `mkdir -p /etc/etc/etc 06:39:40 mkdir: invalid option -- ' ' \ Try `mkdir --help' for more information. 06:39:43 I don't get it 06:41:22 You need to use `run if you have more than one argument. 06:41:32 Plain ` passes everything after the command as a single argument. 06:41:49 `run mkdir -p "/etc/etc/etc/ad\ nauseam" 06:41:50 mkdir: cannot create directory `/etc/etc': Permission denied 06:41:52 :( 06:42:02 `run chmod +w /etc 06:42:03 chmod: changing permissions of `/etc': Operation not permitted 06:42:06 It's for making things like `addquote Whatever shell metacharacters may be here. to work without having to quote everything. 06:42:06 `run chmod +w / 06:42:07 chmod: changing permissions of `/': Operation not permitted 06:42:42 fine then 06:42:43 `quote 06:42:44 660) Incest, the enemy of graph theorists everywhere. 06:42:50 I don't get it. 06:43:07 elliott this is all your fault 06:43:12 `cat wisdom/alise 06:43:13 cat: wisdom/alise: No such file or directory 06:43:18 this is the worst 06:43:38 `run echo elliott's not hiding over here >alise 06:43:39 bash: -c: line 0: unexpected EOF while looking for matching `'' \ bash: -c: line 1: syntax error: unexpected end of file 06:43:43 `run echo elliott\'s not hiding over here >alise 06:43:46 No output. 06:43:49 `run echo elliott\'s not hiding over here >/wisdom/alise 06:43:49 bash: /wisdom/alise: No such file or directory 06:43:58 `run echo elliott\'s not hiding over here >wisdom/alise 06:43:59 No output. 06:44:01 `rm alise 06:44:03 No output. 06:44:12 `run mkdir -p etc/etc/etc/ad\ nauseam 06:44:13 No output. 06:45:00 -!- edwardk has joined. 06:45:46 is there some kind of weblist with all the quotes? 06:45:55 `pastequotes 06:45:58 http://codu.org/projects/hackbot/fshg/index.cgi/file/tip/paste/paste.7340 06:46:14 see also wisdom.pdf in the topic 06:46:55 -!- brrr has quit (Quit: Cya!). 06:47:42 `run addwep Monoids A monoid is just a subalgebra of the STR algebra, if you squint hard enough. 06:47:44 No output. 06:49:14 hmm 06:49:21 fizzie: where's hackego's current site? 06:49:26 it's not going to codu 06:57:41 `? urbandictionary 06:57:42 urbandictionary? ¯\(°_o)/¯ 06:58:23 `run addwep urbandictionary "Urban Dictionary is an alternative, inferior wisdom database." 06:58:24 No output. 07:06:45 What does "not going to codu" mean? 07:08:09 `help 07:08:09 Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ 07:08:14 the URL is out of date 07:08:23 or my cache wasn't clearing 07:08:25 one of the two 07:08:33 EWORKSFORME 07:09:19 If you want to get technical, the "physical" address is http://www2.codu.org/projects/hackbot/fshg/ 07:09:19 `run addwep "works for me" "Error: unable to read wisdom database. try again later." 07:09:21 No output. 07:25:26 -!- AnotherTest has joined. 07:31:07 -!- edwardk has quit (Quit: Computer has gone to sleep.). 07:46:21 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:17:38 Goood morning 09:26:51 coppro: ? 09:39:52 -!- idris-bot has joined. 09:50:50 `cat bin/addwep 09:50:50 #!/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 so why do you say e.g. "tiedätko sinä suomea" instead of "sinä tiedatko suomea" 10:03:01 is it like the english weirdness where you switch the order of words when you ask a question 10:03:35 (of course "sinä" is optional in the first place, if i understand correctly, but nevertheless) 10:04:13 Because languages are weird? 10:04:17 That would be "tiedätkö", and I think people would generally say "puhutko", if you're talking about the language. 10:04:31 er, yes, that 10:05:00 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 But yes, it's some sort of "special sentence order for questions" thing. 10:05:54 The word that denotes it is a question is moved to the front, or some-such. 10:06:27 hm, ok 10:06:33 You can sometimes put the interrogative suffix (-ko, -kö) into different words in order to denote emphasis. 10:06:58 like how 10:07:07 "Puhutko sinä suomea?" do you speak Finnish, with no particular special emphasis -- "Suomeako sinä puhut?!" do you speak *Finnish*?! 10:07:39 In the latter order, it has "out of all possible languages, you're speaking Finnish! what's wrong with you!" connotations. 10:07:57 ah, it's always on one word, but you can choose which one? 10:08:22 Yes. "Sinäkö puhut suomea?" would also be legal. 10:08:34 When you're trying to find the one Finnish speaker in a group, for example. 10:09:01 As in, "is it you who speaks Finnish 10:09:07 what if you want special emphasis on the verb 10:10:53 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 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 And I don't think there's a rising intonation for questions. At least nothing as dramatic. 10:12:21 isn't even just saying "sinä" a sort of emphasis? 10:12:38 i may have been misled 10:12:47 Yes, it is, since it's not necessary. 10:14:14 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 (Language names aren't capitalized, incidentally.) 10:14:32 how do you decide whether to add it in or not 10:15:04 i suppose i can analogize to hebrew except it's not as common there 10:15:21 you're making what? 10:15:24 Yes, I was wondering about that. 10:15:57 What is capitalized? 10:17:27 Proper nouns, generally. 10:17:45 But not many things that English does, like days of the week, or months of the year. 10:18:21 Names of countries are, but their languages aren't, and the nouns for the peoples aren't either. 10:18:38 So the country is "Suomi" but the language is "suomi" and a Finn is "suomalainen". 10:19:30 If the language is "suomi", how does one arrive at "suomea"? 10:21:00 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 "suomea" would be the partitive case. 10:21:24 http://en.wiktionary.org/wiki/Appendix:Finnish_declension/ovi 10:21:43 "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 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 [wiki] [[Special:Log/newusers]] create * Fansdesks * New user account 10:24:23 Google Translate translates "Do you speak English?" to "Puhutko Englanti?". Should it be "Puhutko englantia?"? 10:24:25 "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 Yes, the latter would be correct. 10:24:38 (Or maybe "Puhutteko", of course.) 10:25:02 "puhuttekste", if you're speaking colloquially and in plural. 10:25:12 Oh well. Google Translate isn't very trustworthy. 10:25:20 Also if you wanted a closer analogue of "do you know Finnish?" it would possibly be "osaatko suomea?" 10:25:39 "puhuttekste"? 10:26:36 "puhuttekste suomee?" or "puhutsä/puhuksä suomee?" would be colloquial/slangy/dialecty/vernacular versions of "puhutteko suomea?" and "puhutko suomea?" 10:27:28 :-( 10:27:30 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 Kids these days write "onx" for "onko", anyway. Or so I hear. 10:29:44 I still need to figure out what people are talking about when they say "partitive". 10:30:01 Three-year-olds speak Finnish just fine without knowing all that. :-( 10:30:40 I don't know why we have a partitive case. 10:31:06 "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 Do you happen to have any other examples? 10:34:04 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 The "used with uncountable nouns" case is the one I'd've thought of first. 10:35:26 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 The "luen kirjaa" / "luen kirjan" pair is more clear. 10:52:28 [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:02 yeah wikispam 10:53:54 [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 [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 I kind of wish Haskell wasn't the first language I got really into 12:10:08 Because I always miss a lot of its features in pretty much any other language 12:10:22 And I try to write programs in other languages as though they were Haskell 12:11:38 Taneb: do you mean you use camelCase instead of underscored_names? 12:11:56 Among other things 12:12:16 some people do that in C++ independently of haskell 12:12:27 I don't really like it 12:16:37 -!- yorick has joined. 12:23:05 Everybody does it in Java and C#, thanks to the standard libraries doing it. 12:33:59 -!- oerjan has joined. 12:38:22 I don't think I shall cosplay on Saturday 12:38:39 will you sinplay instead 12:39:16 Erfplay. 12:39:17 No, but I may cotplay 12:48:55 `cat bin/addwep 12:48:56 #!/bin/sh \ echo "$2" > "wisdom/$1" 12:49:20 `ls wisdom/*onoi* 12:49:20 ls: cannot access wisdom/*onoi*: No such file or directory 12:49:30 `` ls wisdom/*onoi* 12:49:31 wisdom/hthmonoid \ wisdom/monoid \ wisdom/monoidal category \ wisdom/monoids \ wisdom/Monoids 12:49:43 fizzie: how would i say "i'm talking about finnish"? 12:49:49 Wow, wisdom/ is such a mess 12:49:53 `? hthmonoid 12:49:54 hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids hthmonoids ... 12:50:00 shachaf: coppro messed it up yesterday 12:50:13 or earlier today 12:50:19 `? Monoids 12:50:20 Monoids are the easy version of categories. 12:50:29 `help 12:50:29 Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ 12:50:33 `` cat wisdom/Monoids 12:50:34 A 12:51:24 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 What I really need is to go to sleep. 12:51:47 shachaf: well `addwep is obviously a broken attempt at that 12:52:01 Right. 12:52:15 There's no way a program run with `run could ever do it. 12:56:22 `? monoid 12:56:23 Monoids are just categories with a single object. 12:56:26 `? monoids 12:56:27 Monoids are the easy version of categories. 12:56:30 `? Monoids 12:56:31 Monoids are the easy version of categories. 12:56:39 `rm wisdom/Monoids 12:56:40 No output. 12:56:50 that won't ever be shown by `? anyway 12:57:05 `? urbandictionary 12:57:05 Urban Dictionary is an alternative, inferior wisdom database. 12:57:17 `? works for me 12:57:17 Error: unable to read wisdom database. try again later. 12:57:30 OH NO HE BROKE IT 12:59:59 shachaf: "Puhun suomen kielestä", probably, to make it more explicit (than "puhun suomesta"). 13:01:35 Or "tarkoitan suomea/suomen kieltä" for a different sense of "I'm talking about X". 13:02:55 `? monoidal category 13:02:56 Monoidal categories are just 2-categories with a single object. 13:04:32 icfp contest anyone? 13:05:51 b_jonas, what language will you be using? 13:06:03 Taneb: I probably won't be doing anything this year 13:06:20 I'll read the task and spend time on it only if it seems very interesting AND if I have time 13:06:35 I will definitely read the task though, this is a spectator sport 13:06:38 Well, I know that I have the time 13:06:44 come to #icfp-contest 13:06:47 when is it? 13:06:52 olsner: tomorrow 13:06:59 http://icfpcontest.org/ 13:07:27 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 Taneb: combine multiple languages then 13:08:44 He's a C++ guy and I'm a Haskell guy 13:08:48 The result may not be pretty 13:09:02 well, that could depend on the task I guess 13:09:09 or one of you writes the code in the language of choice, and the other works on analyzing the problem 13:09:31 olsner, that may be a better idea 13:09:33 Taneb: have you looked at the background of the http://icfpcontest.org/ webpage, http://icfpcontest.org/images/bkg.png ? 13:09:46 based on some earlier icfps there might be separate tasks to work on independently though 13:10:07 it's not solid 13:10:07 b_jonas, not in great detail 13:10:26 it seems to have a pattern made of squares of two different colors 13:15:20 Yeah 13:17:08 oh, and its size isn't even divisible with the size of those squares 13:17:15 http://i.imgur.com/jDaoHBg.png 13:17:21 That's it in black and white 13:18:09 the webpage might come form https://github.com/icfpcontest2014/icfpcontest2014.github.io 13:19:54 (I'm more of a perl and C++ person anyway) 13:21:02 Looks like I'm teaming up with my housemate 13:36:07 hmm, so is the background a hidden message of some sort? 13:46:37 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 fizzie: yay at the wiki being back 15:31:23 any plans to move it still? 15:40:59 Well, I mean, I'll think about it, but *lazy* 15:42:20 :< 15:42:23 -!- mshock has joined. 15:42:34 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 Calm down, it's only ones and zeroes. 15:54:55 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 have computers improved to the stage where they can actually run MediaWiki yet? 15:56:09 -!- oerjan has quit (Quit: leaving). 15:56:40 ais523_: no 15:58:37 I blame PHP 15:58:55 [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 @djinn ((a -> Void) -> Void) -> a 16:30:31 -- f cannot be realized. 16:30:45 saw that one in an article talking about the Curry-Howard correspondence 16:31:07 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 it's double-negation elimination. 16:31:17 yes 16:31:24 intuitionistic type theory corresponds to intuitionistic logic. 16:31:32 double-negation elimination is equivalent to LEM 16:31:39 [proof tombstone] 16:32:07 and the standard lambda calculus type system models intuitionistic logic, presumably 16:32:09 ais523_: if you had that function you could write a term of type (Either a (a -> Void)) 16:32:13 wasn't quite sure which logic it corresponded to 16:32:23 your intuition should be enough to tell you that's impossible without _|_ 16:32:25 (because parametricity) 16:32:38 hah hah 16:32:47 I don't think there's a standard lambda calculus type system :) 16:33:18 elliott: hmm, perhaps; you can talk about "typed lambda calculus" without people shouting at you, though 16:33:53 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 the STLC is a rather boring logic, at least 16:34:21 b_jonas: ? 16:34:59 elliott: hmm, that (Either a (a -> Void)) type reminds me of the halting problem, in a way 16:35:27 ais523_: because it's a decision procedure for every proposition? 16:35:34 yes 16:35:55 although, there's a different problem 16:36:10 which is that given two different Voids, you can't even construct Void1 -> Void2 in Haskell, I don't think 16:36:14 perhaps you could with a pattern match 16:36:22 you just write let voidconvert v = case v of 16:36:27 and that's the entire function 16:36:37 somehow I don't think that's valid syntax, though 16:36:59 dunno, I think I was just laughing at "standard lambda calculus type system" too 16:37:33 I have problems (at work) with people assuming things are standardised when they actually aren't 16:38:25 is it possible to write a pattern match with zero cases in Haskell? 16:39:31 TLS certificates are such a pain to deal with :/ 16:41:27 ais523_ : 16:41:52 @djinn Void -> a 16:41:52 f = void 16:42:32 @djinn-add type NotNot a = Not (Not a) 16:42:43 @djinn NotNot (Either a (Not a)) 16:42:43 f a = void (a (Right (\ b -> a (Left b)))) 16:43:08 `void' is `void v = case v of {}' 16:43:09 /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: void': not found 16:43:31 @type either 16:43:32 (a -> c) -> (b -> c) -> Either a b -> c 16:43:43 void :: Void -> a 16:45:17 ski: thanks, was just reading that page 16:45:32 ais523_: you can interconvert given absurd :: VoidN -> a 16:45:56 elliott: yeah, the point was that the empty case lets you define absurd in the first place 16:46:01 which is implementable for "newtype Void = Void (forall a. a)" and "newtype Void = Void Void" with no extra extensions 16:46:05 and "data Void" with the empty case extension 16:46:18 (note that the first one requires the RankNTypes extension to state) 16:46:18 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 absurd x = x `seq` undefined is also an OK implementation 16:46:34 because you can proof that the _|_ is never reached 16:46:37 *prove 16:46:39 (the first one really only requires `PolymorphicComponents') 16:47:01 elliott: anyway, I read up about rank N and rank 2 types a bunch because it was relevant to my research 16:47:07 (even absurd _ = undefined is fine, really, since you have to abandon _|_ inputs anyway) 16:47:12 ais523_ : yes, it's a bit sad that we had to wait so long for it 16:47:26 it turns out that type inference for rank 2 types is actually decidable, but ghc doesn't currently infer it 16:47:55 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 ais523_: Would that be a reason to have separate extensions for rank 2 and rank N? 16:48:11 zzo38 : it could be 16:48:13 zzo38: possibly it would be 16:48:31 (and currently both exist as separate extensions) 16:48:37 Rank2Types is deprecated I think 16:48:56 ski: in OCaml, I'd guess that the primitive would be "match foo with True -> bar | False -> baz" 16:49:11 or maybe "(function True -> bar | False -> baz) foo" 16:49:18 yes 16:49:26 so yeah, it's probably the same as SML in that respect 16:50:32 ais523_ : "something I learned from that page", which page ? 16:50:40 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 ski: the one you most recently linked to me 16:51:02 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 ski: oh, that's because I know much of OCaml quite well, but not really Haskell 16:51:36 oh, i see 16:51:37 so if I learn something new about the comparison between OCaml and Haskell, it's normally on the Haskell side 16:52:00 in Agda2, one'd write `void' differently 16:52:23 void : {A : Set} -> Void -> A 16:52:26 void () 16:52:38 `()' is an absurd pattern 16:52:38 /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: ()': not found 16:52:53 (and if you use it, you don't need a definiens) 16:53:32 (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 ski: Agda2 has explicit foralls? 16:54:15 ski: finite-state type theory, especially affine logics 16:54:18 what do you mean by "explicit foralls" ? 16:54:31 the System F style where you have a type parameter to functions 16:54:47 rather than the OCaml style where you write 'a and it implies a type parameter for 'a 16:54:52 well, it's just dependent functions 16:55:05 however, Agda2 (and Agda1) has implicit arguments 16:55:19 with explicit arguments, the above would just look like 16:55:29 void : (A : Set) -> Void -> A 16:55:31 void A () 16:56:03 you can also say stuff like 16:56:07 -!- yorick has quit (Read error: Connection reset by peer). 16:56:35 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 _++_ : {A : Set} -> {m : Nat} -> {n : Nat} -> Vector A m -> Vector A n -> Vector (m + n) 16:56:39 where 16:56:43 _+_ : Nat -> Nat -> Nat 16:56:50 and 16:56:58 Vector : Set -> Nat -> Set 16:57:12 * ski nods 16:57:45 in `_++_', the `m' and `n' natural length arguments are implicit 16:58:17 (since usually when you use `_++_', you apply it to arguments so that `m' and `n' can be inferred) 16:58:56 i've not heard the name "finite-state type theory" before 16:59:20 is it like a version of "of course", indexed with a natural number expressing how many times you may use the resource ? 16:59:26 ais523_ ^ 16:59:27 well it's a pretty small niche, because it's sub-TC by definition 16:59:34 ski: that's "bounded contraction", which is part of it 16:59:42 a whole chapter of my thesis is on the subject 16:59:54 where I argue that there's a design error in all the bounded contraction type systems I'm aware of 17:00:01 err, the non-dependently-typed ones, that is 17:00:05 sounds interesting 17:00:15 (are there any dependently-typed ones ?) 17:00:28 yes, but they're massively complex and I don't really understand them 17:00:43 they noticed the same error I did, and worked around it using a hideously complex dependent typing variant 17:00:54 whereas I'm working around it with intersection types 17:01:08 mhm, ok 17:01:31 the basic problem's to do with the fact that the contraction bounds aren't properly polymorphic 17:01:43 this sounds scary 17:01:47 i only recall seeing some notes by Pfenning that didn't treat the quantifiers in a substructural way, iirc 17:02:24 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 because all of a sudden, you can solve problems by brute force 17:02:46 um :/ 17:02:48 maybe I should try to ask this channel about non-eso theoretic problems 17:02:52 that said, one of my major results is that SCC (and similar type systems) have decidable type inference 17:02:54 maybe a small half :) 17:02:54 "sub-TC" means substructural variants of Type Theory, yes ? 17:03:05 I should try that 17:03:33 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:40 *decidable equivalence 17:03:50 which implies that the languages can't be Turing-complete 17:04:10 ok 17:04:14 -!- shikhin has joined. 17:05:00