00:04:24 `learn_append dwfo http://thedwfo.org 00:04:26 Learned 'dwfo': DWFO is the Doctor Who Fan Orchestra. http://thedwfo.org 00:05:17 hm 00:05:27 -!- `^_^v has quit (Ping timeout: 260 seconds). 00:05:47 `slwd dwfo//s[.] /, / 00:05:49 ​/bin/sed: -e expression #1, char 17: unterminated `s' command 00:06:05 `slwd dwfo//s/[.] /, / 00:06:07 dwfo//DWFO is the Doctor Who Fan Orchestra, 00:06:30 `slwd dwfo//s/$/./ 00:06:32 dwfo//DWFO is the Doctor Who Fan Orchestra, . 00:11:09 @metar ENVA 00:11:10 ENVA 062350Z VRB05KT CAVOK M02/M10 Q1035 RMK WIND 670FT 15017G29KT 00:13:04 -!- nooga has quit (Ping timeout: 240 seconds). 00:32:08 -!- tromp has joined. 00:32:59 -!- yorick has joined. 00:48:41 -!- alercah_ has changed nick to alercah. 00:54:47 -!- iczero has changed nick to wlp1s1. 01:04:11 -!- tromp has quit (Remote host closed the connection). 01:06:28 -!- thegreylady has joined. 01:06:37 -!- thegreylady has left. 01:06:47 -!- nooga has joined. 01:12:36 -!- Lord_of_- has quit (Excess Flood). 01:15:59 -!- Lord_of_Life has joined. 01:22:21 -!- tromp has joined. 01:24:37 -!- lynn has joined. 01:34:14 -!- doesthiswork1 has joined. 01:34:39 -!- doesthiswork1 has changed nick to doesthiswork. 01:36:37 -!- krok_ has quit (Quit: Leaving). 01:37:08 a neighbor just tried to register her phone with my computer 01:38:32 -!- tromp has quit (Remote host closed the connection). 01:43:07 -!- doesthiswork has changed nick to doesntthiswork. 01:43:50 -!- doesntthiswork has left. 01:50:02 -!- doesthiswork has joined. 01:51:40 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”). 01:55:44 -!- tromp has joined. 01:56:09 -!- nooga has quit (Ping timeout: 245 seconds). 02:34:49 -!- hppavilion1 has quit (Ping timeout: 240 seconds). 02:41:55 <\oren\> when is the second americna civil war scheduled for? 02:59:21 -!- nooga has joined. 03:03:57 -!- nooga has quit (Ping timeout: 260 seconds). 03:06:35 -!- oerjan has quit (Quit: Nite). 03:49:05 -!- hppavilion1 has joined. 04:21:16 doesthiswork: Did you allow it then steal all her shit? 04:21:52 \oren\: Sometime this year, I think. 04:24:02 Hey, what programming languages are out there that have a type system whose power level is on par with Haskell and Scala? 04:24:30 ML? 04:24:51 (and its family, such as Ocaml) 04:25:50 organic caml 04:26:51 I'm writing some neural net software in Scala and I'm wondering if I should move to a different language. 04:27:08 I prefer Ωcaml 04:27:31 Scala is treating me pretty well. I think if I were to do what I'm doing in, say, F#, it would just break down and cry. 04:27:44 tswett: Also, are Haskell and Scala's type systems' power level... over 9000? 04:28:09 I can't think of a funny answer to that question. 04:28:33 tswett: Probably something regarding proof ordinals? 04:28:44 Ah, right. 04:29:03 hppavilion1: yes. In fact, their power level is an ordinal number which cannot be proven to exist in Peano arithmetic. 04:30:51 tswett: (a) Are proof ordinals applicable in this context [probably yes] (b) Have the proof ordinals of Haskell and Scala's type systems been found (c) Are they particularly interesting ordinals, or just a "whatever" ordinal (d) what are they? 04:30:59 Oh, and (e) are they the same? 04:31:23 (a) dunno (b) see (a) (c) see (b) (d) see (c) (e) see (d) 04:32:47 All righty, lemme see. 04:33:01 ML doesn't have typeclasses, but it has "modules", which feel familiar from Scala and Coq. 04:33:36 A module can contain type and function definitions, but it can also contain abstract types and abstract functions, to be filled in later by means of inheritance. 04:33:47 Scala traits have the same property. 04:33:51 As do Coq modules. 04:37:55 Yeah, I guess my main alternatives here are probably Haskell and the dependently typed ones: Coq, Agda, Idris. 04:47:26 -!- nooga has joined. 04:51:29 -!- nooga has quit (Ping timeout: 240 seconds). 04:55:18 -!- adu has joined. 05:03:07 -!- adu has quit (Quit: adu). 05:03:16 -!- fowl has joined. 05:10:54 -!- adu has joined. 05:25:23 -!- tromp has quit (Remote host closed the connection). 05:55:50 -!- adu has quit (Quit: adu). 06:17:29 -!- doesthiswork has quit (Quit: Leaving.). 06:26:13 -!- tromp has joined. 06:30:41 -!- tromp has quit (Ping timeout: 255 seconds). 06:35:33 -!- nooga has joined. 06:39:41 -!- nooga has quit (Ping timeout: 240 seconds). 07:08:21 -!- augur has quit (Remote host closed the connection). 07:17:45 -!- augur has joined. 07:22:26 -!- augur has quit (Ping timeout: 255 seconds). 07:46:09 -!- mecha_ma` has quit (Ping timeout: 240 seconds). 08:02:34 -!- haavard has quit (Quit: WeeChat 1.5). 08:02:53 -!- haavard has joined. 08:23:30 -!- nooga has joined. 08:28:07 -!- nooga has quit (Ping timeout: 256 seconds). 08:35:19 -!- tromp has joined. 08:46:12 -!- tromp has quit (Remote host closed the connection). 09:24:40 -!- nooga has joined. 09:54:32 -!- nooga has quit (Ping timeout: 255 seconds). 10:06:29 -!- hppavilion1 has quit (Ping timeout: 240 seconds). 10:11:24 -!- nooga has joined. 10:18:40 -!- AnotherTest has joined. 10:27:32 -!- tromp has joined. 10:31:53 -!- tromp has quit (Ping timeout: 255 seconds). 11:28:09 -!- boily has joined. 11:37:56 `wisdom 11:37:57 costume//Costumes are used for cosplay. Taneb sometimes invents them. 11:43:30 `cwlprits life 11:43:32 oerjän 11:45:53 `? life 11:45:54 ​‘Life,’ said Marvin, ‘don't talk to me about life.’ 11:47:17 -!- tromp has joined. 11:51:59 -!- tromp has quit (Ping timeout: 255 seconds). 12:17:39 -!- Akaibu has quit (Quit: Connection closed for inactivity). 12:26:10 -!- boily has quit (Quit: COMET CHICKEN). 12:35:02 -!- Akaibu has joined. 12:51:37 -!- doesthiswork has joined. 12:51:59 -!- ^v has quit (Ping timeout: 245 seconds). 12:53:18 -!- Zarutian has joined. 12:54:42 -!- Zarutian has quit (Client Quit). 12:57:34 -!- ^v has joined. 13:13:14 -!- Lord_of_Life has quit (Excess Flood). 13:14:29 -!- Lord_of_Life has joined. 13:15:13 `xkcdwhatiflist 13:15:14 ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: xkcdwhatiflist: not found 13:15:34 `xkcdwhatiflist 153 13:15:34 ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: xkcdwhatiflist: not found 13:17:00 and it actually looks like an interesting one 13:17:59 though I think it's wrong 13:23:49 `quote 13:23:49 183) Is there a name for something where I'm more attracted to someone if I know they've had a rough past? Sgeo, "Little Shop of Horrors" 13:23:51 `scheme 13:23:51 Nothing Can Stop Me Now 13:23:58 `scheme 13:23:59 The Fate of the Flammable 13:24:14 `recipe 13:24:15 n Additoin. \ \ MMMMM \ \ MMMMM----- Recipe via Meal-Master (tm) v8.05 \ \ Title: CARROT CACOA CHILI CHICKEN \ Categories: Beverages, Fish, Sauces \ Yield: 4 Servings \ \ ----------------------- \ 2 lb Ground pork; lightly beaten \ 1 tb Heavy cream \ 1/2 c Milk \ 2 tb Canned cooked pineapple, chopped \ 1 ts Cinnamon \ 1 ts Baking 13:24:21 `recipe 13:24:22 v8.05 \ \ Title: CONELLY SAUCE CAKE \ Categories: Cakes, Chocolate, Meats, Beverages \ Yield: 4 Servings \ \ 2 c Chicken broth \ 2 tb Sesame seeds \ 1 tb Parsley, dried \ 1 ts Vanilla extract \ 2/3 c Lite red pepper sauce \ 2 ts Vanilla extract \ 1 ts Ground cinnamon \ 1/4 ts Pepper \ 1/8 ts Pepper \ Brown sugar \ 2 tb Sugar \ 1 13:24:29 `recipe 13:24:30 ​ Sprigs of diced \ Sour cream \ -chopped onions \ -about 2 oz. salt \ Gined orange peeling skin \ -2 tbsp. \ 1/4 ts Black pepper \ \ Combine the milk, the tomatoes, banana, and salt in a small bowl, mix together the pepper and salt and \ pepper. Whisk in the coconut. Reduce the heat and simmer, uncovered, 20 \ minutes. Stir in remaini 13:36:08 What is the name for that general scheme for representing algebraic types in untyped lambda calculus? 13:41:15 you know, the one where you represent a tuple (x,y) by (\f.fxy) and you represent (Left x) by (\f.\g.fx) and (Right y) by (\f.\g.gy) 13:48:56 -!- tromp has joined. 13:52:17 -!- AnotherTest has quit (Ping timeout: 255 seconds). 13:53:23 -!- tromp has quit (Ping timeout: 256 seconds). 13:57:12 -!- oerjan has joined. 14:09:21 `` ls bin/xk* 14:09:22 ls: cannot access bin/xk*: No such file or directory 14:13:03 b_jonas: church encoding or scott encoding (they're different when the types are recursive) 14:16:15 hm i may be confused about the differences 14:21:22 hm or wikipedia's scott encoding article is confused. 14:26:33 and the church encoding article only looks at limited examples, and seems to contradict the scott article for lists. 14:28:36 (i think the problem amounts to "church encoding is much more complicated for general recursive data types) 14:28:41 *") 14:31:53 oerhan: thanks 14:32:46 oerjan: maybe they differ in how they define the algebraic data types that they are trying to encode? 14:33:29 well, church encoding needs to know how a type occurs recursively in itself, in order to create well-typed representations 14:34:17 while scott encoding doesn't bother with that, so treats constructors as not caring what's put into them 14:35:28 ok... though just from that, church encoding could still be a special case of scott encoding 14:36:07 not really. there's only one scott encoding for a type. 14:38:09 ah, I see! 14:38:47 according to https://en.wikipedia.org/wiki/Church_encoding#List_encodings , lists are encoded in some strange way, as tagged stuff rather than enums 14:39:03 b_jonas: yes, that article is really confused. 14:39:15 that's not a well-typed representation at all. 14:39:16 I never understood why they'd do that in lambda calculus 14:39:50 I mean, I can understand why you'd encode enums as a tagged struct in some languages 14:39:56 just not in lambda calculus 14:39:58 the right fold representation is the well typed one. 14:41:29 in fact 14:41:39 the one pair version is a cute hack 14:41:53 https://en.wikipedia.org/wiki/Church_encoding doesn't even seem to tell how to encode an arbitrary algebraic type in lambda calculus 14:42:02 as in directly 14:42:04 right 14:42:34 it just encodes Lists and some other types, though of course there are ways to encode algebraic types as Lists 14:43:16 i think the problem is, that to many people, "church encoding" is just a general term for any way of encoding stuff in lambda calculus. 14:43:24 possible 14:43:28 oh by the way 14:43:37 and that article is written from that viewpoint. 14:45:00 you know how there's Gödel encoding, which encodes statements of some logical system as natural numbers, and it works by first writing the statement as a list of characters from some character set, and then encodes that list of characters to a number? 14:45:18 for a long time I didn't understand why they encode a flat list this way, rather than some recursive structure 14:45:21 but now I found out 14:45:47 hm? 14:46:11 does my initial question make sense about why this is a flat list, as opposed to a parse tree? 14:46:17 I'll tell the solution afterwards 14:46:25 yes. and i have a guess at the answer... 14:46:52 it's possible that peano arithmetic or whatever isn't powerful enough to recurse into such a structure. 14:47:06 yes, something like that 14:47:39 this encoding is used to show that proof is definable in a particular weak system 14:48:33 that system is Robinson arithmetic, which is a crazy weak logical system 14:49:04 the other guess is that gödel just didn't think of doing it that way, and it works with characters. 14:49:16 both may be true simultaneously, of course. 14:49:19 Robinson arithmetic is so weak that you can't really prove anything in it, 14:50:09 oerjan: Gödel himself isn't too relevant here, he's the first one who did this and so his name is used, but people later defined other versions of the encoding and still used flat lists 14:50:43 Robinson arithmetic has a language that has addition and multiplication 14:50:45 but not power 14:50:51 i guess robinson arithmetic cannot do exponentials, which is sort of essential to nesting the construction. 14:51:02 as such, it is not even obvious why you can manipulate flat lists with it 14:51:13 or why you'd choose to work with such a crazy system 14:51:21 why you don't just choose one that has lists built in or something 14:51:38 anyway, it turns out there's some crazy trick that lets you define lists in Robinson arithmetic 14:52:25 -!- ^v has quit (Ping timeout: 245 seconds). 14:53:01 and lets define getting the nth element of a list 14:53:04 obviously you choose to work with it because you want to find the weakest system where gödel's theorem works 14:53:08 which means you can also quantify over all elements of the list 14:53:44 -!- ^v has joined. 14:53:49 so you can express a statement that something is true for all adjacent pairs of elements of a list, or similar 14:54:19 but it wouldn't directly let you express that something is true for all elements of a tree, except by going through flat lists 14:55:03 you can define cons, car, cdr if you want, but you can't directly state a statement that something is true everywhere on a tree, so you can't define whole tree transformations 14:55:17 you can do anything with a tree too of course, but only by using lists first 14:55:30 so since they have to use lists in first place, they didn't go on 14:55:56 mhm 14:56:22 oerjan: maybe, though "weakest" is somewhat subjective 14:56:45 there is at least one system that is neither weaker neither stronger than RA that you can also use for this 14:57:28 i didn't say you _could_ find the weakest system, i said you _wanted_ to hth 14:57:33 sure 14:57:49 anyway, yes, there is some reason to use that system 14:57:59 or at least some similar system with the same problem 15:00:28 and even if you use another system, you'll probably run into this same problem 15:01:01 even if you have a system that has first-class lists, unless it has something like a crazy multi-level tree indexing primitive or something 15:05:06 -!- doesthiswork has quit (Quit: Leaving.). 15:07:39 -!- AnotherTest has joined. 15:08:00 -!- `^_^v has joined. 15:17:34 oh the one pair encoding is sourced from tromp's paper 15:20:39 -!- augur has joined. 15:25:17 -!- augur has quit (Ping timeout: 255 seconds). 15:49:52 -!- tromp has joined. 15:54:11 -!- tromp has quit (Ping timeout: 240 seconds). 16:01:50 -!- greenlight has joined. 16:02:55 AFAIR the "crazy trick" is just based on the fact that there are finite arithmetic sequences of pairwise coprime numbers of arbitrary length (and size of numbers), plus the CRT. 16:04:26 so... basically f(a,b,c)[n] = c % (a + b*n) can encode arbitrary finite lists 16:08:49 -!- Vampz has joined. 16:09:03 -!- Vampz has left. 16:23:26 int-e: yes, something like that 16:41:07 -!- augur has joined. 16:47:37 -!- Akaibu has quit (Quit: Connection closed for inactivity). 16:57:22 -!- ^v has quit (Ping timeout: 258 seconds). 17:04:11 /haɪ/ 17:05:07 -!- oerjan has quit (Quit: /baɪ/). 17:34:22 -!- doesthiswork has joined. 17:50:47 -!- tromp has joined. 17:55:03 -!- tromp has quit (Ping timeout: 240 seconds). 17:57:11 -!- Phantom_Hoover has joined. 17:58:10 [wiki] [[Befunge]] https://esolangs.org/w/index.php?diff=50856&oldid=50511 * Osuka * (+173) 18:12:15 -!- Zarutian has joined. 18:21:51 -!- MoALTz has joined. 19:13:33 -!- Phantom_Hoover has quit (Ping timeout: 256 seconds). 19:25:37 -!- hppavilion1 has joined. 19:31:31 -!- hppavilion1 has quit (Ping timeout: 260 seconds). 19:34:49 -!- augur has quit (Remote host closed the connection). 19:39:18 -!- hppavilion1 has joined. 19:51:39 -!- tromp has joined. 19:56:11 -!- tromp has quit (Ping timeout: 240 seconds). 19:58:21 -!- krok_ has joined. 20:03:39 -!- hppavilion1 has quit (Remote host closed the connection). 20:04:04 -!- hppavilion1 has joined. 20:04:07 fizzie: Should I use Kubernetes to manage jobs and things? 20:24:37 <\oren\> 𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄𝔄 20:24:39 <\oren\> 𝔸𝔸𝔸𝔸𝔸𝔸𝔸𝔸𝔸𝔸𝔸𝔸𝔸𝔸 20:25:03 <\oren\> I need an email of someone who understands techspeak 20:25:20 <\oren\> not a customer suport 20:30:34 -!- Akaibu has joined. 20:34:35 -!- greenlight has left. 20:38:20 -!- Phantom_Hoover has joined. 20:41:15 shachaf: It sounds kuul. I think you should. 20:41:32 Are you? 20:41:50 I'm not really managing anything. 20:43:02 -!- augur has joined. 20:44:04 Also upon further reflection, I don't think I really want monitoring as such, mostly because I don't have anything that gets traffic. I think I'm more interested in just making up arbitrary long-term time series that can then be turned into those wiggly lines, and the monitoring/alerting aspect is more of an afterthought. And that's why I'm using InfluxDB instead of Prometheus. 20:44:14 (I read those threads about long-term storage in Prometheus.) 20:44:27 Makes sense. 20:45:11 And you don't want to join, I guess, is the other constraint. 20:45:54 What sort of query language should you use for querying time series databases? 20:45:59 You should invent a good one. 20:46:27 But I guess first you should stop working at your current employer, so that you can release it. 20:48:32 I'm not entirely sure the query language should be inherently time-oriented. 20:48:50 Speaking of scow, Bazel doesn't have proto_library either. 20:49:04 I didn't specify that it should be. 20:49:21 What does it have? 20:49:48 There's an objc_proto_library, which is documented in be to have "proto_library dependencies", but there's no proto_library. 20:50:19 And there's a proto_lang_toolchain, which "Specifies how a LANG_proto_library rule (e.g., java_proto_library) should invoke the proto-compiler", but there's no java_proto_library either. 20:50:40 You can try https://github.com/pubref/rules_protobuf 20:50:45 (Actually AIUI it does in fact have built-in rules for java_proto_library and friends, but they're undocumented and not working correctly.) 20:51:35 It does have https://github.com/bazelbuild/bazel/blob/master/tools/build_rules/genproto.bzl 20:52:45 They're supposed to open-source the real proto_library and java_proto_library and such, but it doesn't have those yet. 20:53:14 I tried writing some Buck macros for protoc ones but it was kind of scow. 20:54:08 There's no equivalent of Scowlark 20:57:19 -!- Cale_ has quit (Remote host closed the connection). 21:20:47 [wiki] [[Special:Log/newusers]] create * Finianb1 * New user account 21:27:59 -!- Phantom_Hoover has quit (Ping timeout: 264 seconds). 21:29:39 -!- Phantom_Hoover has joined. 21:29:43 <\oren\> https://www.rt.com/usa/376621-trump-korea-putin-crimea-waters/ 21:29:48 <\oren\> US congresswoman thinks Putin is invading Korea kekekekekekekekeke 21:34:17 Crimea, Korea? 21:34:33 -!- hppavilion1 has quit (Ping timeout: 240 seconds). 21:35:50 <\oren\> int-e: and this morning Nancy Pelosi called Trump "President Bush" 21:36:12 I'm not sure that either Bush deserves that kind of insult. 21:36:33 <\oren\> maybe she wishes "Jeb!" was the president 21:48:34 [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=50857&oldid=50852 * Finianb1 * (+169) 21:49:31 [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=50858&oldid=50857 * Finianb1 * (+17) 21:51:35 [wiki] [[Befunge]] https://esolangs.org/w/index.php?diff=50859&oldid=50856 * Finianb1 * (+181) Add a Quine 21:51:48 [wiki] [[Befunge]] https://esolangs.org/w/index.php?diff=50860&oldid=50859 * Finianb1 * (+1) /* Quine */ 21:52:34 -!- tromp has joined. 21:56:49 -!- tromp has quit (Ping timeout: 248 seconds). 21:57:06 s/shellcode/ethical hacking/, cute 21:57:28 (second edit of the last four) 22:01:01 -!- LKoen has joined. 22:14:02 <\oren\> kek 22:37:38 -!- Akaibu has quit (Quit: Connection closed for inactivity). 22:38:17 -!- ^v has joined. 22:45:46 -!- brandonson has joined. 22:45:46 -!- brandonson has quit (Client Quit). 22:54:41 -!- AnotherTest has quit (Quit: ZNC - http://znc.in). 23:11:48 -!- `^_^v has quit (Quit: This computer has gone to sleep). 23:23:35 -!- boily has joined. 23:23:44 -!- tromp has joined. 23:23:52 @metar CYUL 23:23:52 CYUL 072321Z 05021G27KT 4SM -SN DRSN SCT015 OVC025 M10/M13 A2975 RMK SC3SC5 PRESFR SLP080 23:27:51 -!- tromp has quit (Ping timeout: 240 seconds). 23:29:00 <\oren\> https://twitter.com/VLenin_1917 23:29:44 lenin was too good 23:29:58 you should be a revolutionary like lenin 23:30:37 <\oren\> by following this account and the others linked to it, you can see the russian revolution reenacted on Twitter 23:31:17 <\oren\> https://twitter.com/RT_1917 23:32:03 да здравствует партия! 23:34:28 -!- idris-bot has quit (Quit: Terminated). 23:36:07 -!- Melvar has quit (Quit: rebooting). 23:37:56 fungot: do you embrace any political ideology? 23:37:56 boily: any where eof=0 and cells wrap ( at 8 bits) by char 23:38:11 fungot: playing it safe. 23:38:11 boily: lots of extras. is easier to match brackets on 23:38:24 fungot: of course, I say. 23:38:25 boily: i haven't cited these because i don't understand how to program without becoming a rainbow 23:38:48 -!- oerjan has joined. 23:38:52 `addquote boily: i haven't cited these because i don't understand how to program without becoming a rainbow 23:38:52 boily: then launch fnord with mutalisks and zerglings to keep defenses busy while mutalisks bombed from above 23:38:54 1310) boily: i haven't cited these because i don't understand how to program without becoming a rainbow 23:39:17 hellfnørdjan. 23:40:20 -!- Melvar has joined. 23:41:58 helłily. 23:42:31 yo doerjan 23:42:43 whachaf? 23:42:55 yo dawg, oerjan 23:43:03 -!- staffehn has quit (Ping timeout: 240 seconds). 23:44:31 -!- idris-bot has joined. 23:44:39 okay̼ 23:50:20 fungot: You're a rainbow 23:50:20 fizzie: only that it wasn't absolutely bios dependent 23:51:01 fungot isn't absolutely bios dependent? 23:51:02 shachaf: in the same way as bfbasic) so far 23:51:14 -!- staffehn has joined. 23:55:58 -!- idris-bot has quit (Ping timeout: 258 seconds).