00:04:24 <oerjan> `learn_append dwfo http://thedwfo.org
00:04:26 <HackEgo> Learned 'dwfo': DWFO is the Doctor Who Fan Orchestra. http://thedwfo.org
00:05:27 -!- `^_^v has quit (Ping timeout: 260 seconds).
00:05:47 <oerjan> `slwd dwfo//s[.] /, </;s/$/>/
00:05:49 <HackEgo> /bin/sed: -e expression #1, char 17: unterminated `s' command
00:06:05 <oerjan> `slwd dwfo//s/[.] /, </;s/$/>/
00:06:07 <HackEgo> dwfo//DWFO is the Doctor Who Fan Orchestra, <http://thedwfo.org>
00:06:32 <HackEgo> dwfo//DWFO is the Doctor Who Fan Orchestra, <http://thedwfo.org>.
00:11:10 <lambdabot> 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 <doesthiswork> 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 <hppavilion1> doesthiswork: Did you allow it then steal all her shit?
04:21:52 <pikhq> \oren\: Sometime this year, I think.
04:24:02 <tswett> Hey, what programming languages are out there that have a type system whose power level is on par with Haskell and Scala?
04:24:51 <pikhq> (and its family, such as Ocaml)
04:26:51 <tswett> I'm writing some neural net software in Scala and I'm wondering if I should move to a different language.
04:27:31 <tswett> 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 <hppavilion1> tswett: Also, are Haskell and Scala's type systems' power level... over 9000?
04:28:09 <tswett> I can't think of a funny answer to that question.
04:28:33 <hppavilion1> tswett: Probably something regarding proof ordinals?
04:29:03 <tswett> hppavilion1: yes. In fact, their power level is an ordinal number which cannot be proven to exist in Peano arithmetic.
04:30:51 <hppavilion1> 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:31:23 <tswett> (a) dunno (b) see (a) (c) see (b) (d) see (c) (e) see (d)
04:32:47 <tswett> All righty, lemme see.
04:33:01 <tswett> ML doesn't have typeclasses, but it has "modules", which feel familiar from Scala and Coq.
04:33:36 <tswett> 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 <tswett> Scala traits have the same property.
04:37:55 <tswett> 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:57 <HackEgo> costume//Costumes are used for cosplay. Taneb sometimes invents them.
11:45:54 <HackEgo> ‘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:14 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: xkcdwhatiflist: not found
13:15:34 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: xkcdwhatiflist: not found
13:17:00 <b_jonas> and it actually looks like an interesting one
13:23:49 <HackEgo> 183) <Sgeo> Is there a name for something where I'm more attracted to someone if I know they've had a rough past? <variable> Sgeo, "Little Shop of Horrors"
13:24:15 <HackEgo> 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:22 <HackEgo> 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:30 <HackEgo> 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 <b_jonas> What is the name for that general scheme for representing algebraic types in untyped lambda calculus?
13:41:15 <b_jonas> 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:22 <HackEgo> ls: cannot access bin/xk*: No such file or directory
14:13:03 <oerjan> b_jonas: church encoding or scott encoding (they're different when the types are recursive)
14:16:15 <oerjan> hm i may be confused about the differences
14:21:22 <oerjan> hm or wikipedia's scott encoding article is confused.
14:26:33 <oerjan> and the church encoding article only looks at limited examples, and seems to contradict the scott article for lists.
14:28:36 <oerjan> (i think the problem amounts to "church encoding is much more complicated for general recursive data types)
14:32:46 <b_jonas> oerjan: maybe they differ in how they define the algebraic data types that they are trying to encode?
14:33:29 <oerjan> well, church encoding needs to know how a type occurs recursively in itself, in order to create well-typed representations
14:34:17 <oerjan> while scott encoding doesn't bother with that, so treats constructors as not caring what's put into them
14:35:28 <b_jonas> ok... though just from that, church encoding could still be a special case of scott encoding
14:36:07 <oerjan> not really. there's only one scott encoding for a type.
14:38:47 <b_jonas> 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 <oerjan> b_jonas: yes, that article is really confused.
14:39:15 <oerjan> that's not a well-typed representation at all.
14:39:16 <b_jonas> I never understood why they'd do that in lambda calculus
14:39:50 <b_jonas> I mean, I can understand why you'd encode enums as a tagged struct in some languages
14:39:56 <b_jonas> just not in lambda calculus
14:39:58 <oerjan> the right fold representation is the well typed one.
14:41:39 <oerjan> the one pair version is a cute hack
14:41:53 <b_jonas> 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:34 <b_jonas> it just encodes Lists and some other types, though of course there are ways to encode algebraic types as Lists
14:43:16 <oerjan> 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:37 <oerjan> and that article is written from that viewpoint.
14:45:00 <b_jonas> 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 <b_jonas> for a long time I didn't understand why they encode a flat list this way, rather than some recursive structure
14:46:11 <b_jonas> does my initial question make sense about why this is a flat list, as opposed to a parse tree?
14:46:17 <b_jonas> I'll tell the solution afterwards
14:46:25 <oerjan> yes. and i have a guess at the answer...
14:46:52 <oerjan> it's possible that peano arithmetic or whatever isn't powerful enough to recurse into such a structure.
14:47:39 <b_jonas> this encoding is used to show that proof is definable in a particular weak system
14:48:33 <b_jonas> that system is Robinson arithmetic, which is a crazy weak logical system
14:49:04 <oerjan> the other guess is that gödel just didn't think of doing it that way, and it works with characters.
14:49:16 <oerjan> both may be true simultaneously, of course.
14:49:19 <b_jonas> Robinson arithmetic is so weak that you can't really prove anything in it,
14:50:09 <b_jonas> 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 <b_jonas> Robinson arithmetic has a language that has addition and multiplication
14:50:51 <oerjan> i guess robinson arithmetic cannot do exponentials, which is sort of essential to nesting the construction.
14:51:02 <b_jonas> as such, it is not even obvious why you can manipulate flat lists with it
14:51:13 <b_jonas> or why you'd choose to work with such a crazy system
14:51:21 <b_jonas> why you don't just choose one that has lists built in or something
14:51:38 <b_jonas> 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 <b_jonas> and lets define getting the nth element of a list
14:53:04 <oerjan> obviously you choose to work with it because you want to find the weakest system where gödel's theorem works
14:53:08 <b_jonas> which means you can also quantify over all elements of the list
14:53:44 -!- ^v has joined.
14:53:49 <b_jonas> so you can express a statement that something is true for all adjacent pairs of elements of a list, or similar
14:54:19 <b_jonas> 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 <b_jonas> 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 <b_jonas> you can do anything with a tree too of course, but only by using lists first
14:55:30 <b_jonas> so since they have to use lists in first place, they didn't go on
14:56:22 <b_jonas> oerjan: maybe, though "weakest" is somewhat subjective
14:56:45 <b_jonas> there is at least one system that is neither weaker neither stronger than RA that you can also use for this
14:57:28 <oerjan> i didn't say you _could_ find the weakest system, i said you _wanted_ to hth
14:57:49 <b_jonas> anyway, yes, there is some reason to use that system
14:57:59 <b_jonas> or at least some similar system with the same problem
15:00:28 <b_jonas> and even if you use another system, you'll probably run into this same problem
15:01:01 <b_jonas> 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 <oerjan> 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 <int-e> 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 <int-e> 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 <b_jonas> 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: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 <HackEgo> [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 <shachaf> fizzie: Should I use Kubernetes to manage jobs and things?
20:25:03 <\oren\> I need an email of someone who understands techspeak
20:30:34 -!- Akaibu has joined.
20:34:35 -!- greenlight has left.
20:38:20 -!- Phantom_Hoover has joined.
20:41:15 <fizzie> shachaf: It sounds kuul. I think you should.
20:41:50 <fizzie> I'm not really managing anything.
20:43:02 -!- augur has joined.
20:44:04 <fizzie> 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 <fizzie> (I read those threads about long-term storage in Prometheus.)
20:45:11 <shachaf> And you don't want to join, I guess, is the other constraint.
20:45:54 <shachaf> What sort of query language should you use for querying time series databases?
20:45:59 <shachaf> You should invent a good one.
20:46:27 <shachaf> But I guess first you should stop working at your current employer, so that you can release it.
20:48:32 <fizzie> I'm not entirely sure the query language should be inherently time-oriented.
20:48:50 <fizzie> Speaking of scow, Bazel doesn't have proto_library either.
20:49:04 <shachaf> I didn't specify that it should be.
20:49:48 <fizzie> 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 <fizzie> 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 <shachaf> You can try https://github.com/pubref/rules_protobuf
20:50:45 <fizzie> (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 <fizzie> It does have https://github.com/bazelbuild/bazel/blob/master/tools/build_rules/genproto.bzl
20:52:45 <fizzie> 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 <shachaf> I tried writing some Buck macros for protoc ones but it was kind of scow.
20:54:08 <shachaf> There's no equivalent of Scowlark
20:57:19 -!- Cale_ has quit (Remote host closed the connection).
21:20:47 <HackEgo> [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: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 <int-e> 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 <HackEgo> [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=50857&oldid=50852 * Finianb1 * (+169)
21:49:31 <HackEgo> [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=50858&oldid=50857 * Finianb1 * (+17)
21:51:35 <HackEgo> [wiki] [[Befunge]] https://esolangs.org/w/index.php?diff=50859&oldid=50856 * Finianb1 * (+181) Add a Quine
21:51:48 <HackEgo> [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 <int-e> s/shellcode/ethical hacking/, cute
21:57:28 <int-e> (second edit of the last four)
22:01:01 -!- LKoen has joined.
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 <lambdabot> 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:58 <shachaf> 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 <boily> да здравствует партия!
23:34:28 -!- idris-bot has quit (Quit: Terminated).
23:36:07 -!- Melvar has quit (Quit: rebooting).
23:37:56 <boily> fungot: do you embrace any political ideology?
23:37:56 <fungot> boily: any where eof=0 and cells wrap ( at 8 bits) by char
23:38:11 <boily> fungot: playing it safe.
23:38:11 <fungot> boily: lots of extras. is easier to match brackets on
23:38:24 <boily> fungot: of course, I say.
23:38:25 <fungot> 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 <boily> `addquote <fungot> boily: i haven't cited these because i don't understand how to program without becoming a rainbow
23:38:52 <fungot> boily: then launch fnord with mutalisks and zerglings to keep defenses busy while mutalisks bombed from above
23:38:54 <HackEgo> 1310) <fungot> boily: i haven't cited these because i don't understand how to program without becoming a rainbow
23:40:20 -!- Melvar has joined.
23:43:03 -!- staffehn has quit (Ping timeout: 240 seconds).
23:44:31 -!- idris-bot has joined.
23:50:20 <fizzie> fungot: You're a rainbow
23:50:20 <fungot> fizzie: only that it wasn't absolutely bios dependent
23:51:01 <shachaf> fungot isn't absolutely bios dependent?
23:51:02 <fungot> 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).