00:49:54 -!- sleffy has joined.
00:55:03 -!- augur has joined.
00:59:39 -!- augur has quit (Ping timeout: 260 seconds).
01:12:16 -!- variable has quit (Quit: /dev/null is full).
01:12:31 -!- augur has joined.
01:25:44 -!- probablymoony has changed nick to moony.
01:26:27 -!- moony has changed nick to Ajit-pai.
01:28:28 <\oren\_> game 7, 4-3 leafs, 2nd period ends
01:29:31 <shachaf> i don't keep up with baseball hth
01:36:12 -!- Ajit-pai has changed nick to moony.
01:47:37 <\oren\_> shit boston evened it up
02:11:44 -!- int-e_ has joined.
02:12:52 -!- int-e has quit (Ping timeout: 256 seconds).
02:16:32 -!- copumpkin has quit (Ping timeout: 260 seconds).
02:16:50 -!- optimus[m] has quit (Ping timeout: 256 seconds).
02:28:19 -!- augur has quit (Ping timeout: 260 seconds).
03:14:32 -!- variable has joined.
03:15:24 -!- variable has quit (Client Quit).
03:16:08 -!- variable has joined.
03:16:41 -!- variable has quit (Client Quit).
03:18:05 -!- variable has joined.
03:18:44 -!- variable has quit (Client Quit).
03:20:07 -!- variable has joined.
03:21:06 -!- variable has quit (Client Quit).
03:22:40 -!- variable has joined.
03:23:13 -!- variable has quit (Client Quit).
03:24:30 -!- variable has joined.
03:25:20 -!- variable has quit (Client Quit).
03:26:39 -!- variable has joined.
03:28:28 -!- variable has quit (Client Quit).
03:30:41 -!- variable has joined.
03:51:09 -!- imode has quit (Ping timeout: 260 seconds).
03:52:19 -!- brandonson has quit (Ping timeout: 260 seconds).
03:54:04 -!- brandonson has joined.
04:04:17 -!- propumpkin has quit (Ping timeout: 248 seconds).
04:41:41 -!- arseniiv has quit (Ping timeout: 256 seconds).
05:12:39 -!- moei has quit (Ping timeout: 255 seconds).
05:13:29 -!- moei has joined.
05:16:11 -!- imode has joined.
05:41:27 -!- sleffy has quit (Ping timeout: 240 seconds).
05:51:41 -!- xkapastel has quit (Quit: Connection closed for inactivity).
05:56:32 -!- brandonson has quit (Ping timeout: 255 seconds).
05:58:10 -!- brandonson has joined.
06:24:57 -!- moei has quit (Quit: Leaving...).
06:56:25 -!- sprocklem has quit (Ping timeout: 265 seconds).
07:03:32 -!- imode has quit (Ping timeout: 260 seconds).
07:38:03 -!- moei has joined.
07:43:06 <esowiki> [[Special:Log/newusers]] create  * Viercc *  New user account
07:47:27 -!- brandonson has quit (Ping timeout: 255 seconds).
07:49:02 -!- brandonson has joined.
07:50:03 <esowiki> [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=54920&oldid=54914 * Viercc * (+176) 
07:58:01 -!- AnotherTest has joined.
08:26:17 -!- AnotherTest has quit (Ping timeout: 276 seconds).
08:27:33 <int-e_> @metar lowi
08:27:34 <lambdabot> LOWI 260820Z 06005KT 030V110 9999 FEW012 SCT035 BKN060 13/10 Q1017 NOSIG
08:32:31 -!- oerjan has joined.
08:44:31 -!- AnotherTest has joined.
08:47:27 -!- copumpkin has joined.
09:01:44 -!- optimus[m] has joined.
09:25:43 -!- xkapastel has joined.
09:39:51 -!- optimus[m] has quit (Ping timeout: 240 seconds).
09:39:52 -!- copumpkin has quit (Ping timeout: 260 seconds).
09:41:20 -!- oerjan has quit (Quit: Later).
09:44:06 -!- variable has quit (Quit: /dev/null is full).
10:17:46 -!- copumpkin has joined.
10:31:31 -!- optimus[m] has joined.
10:38:54 -!- AnotherTest has quit (Ping timeout: 260 seconds).
10:59:55 <Taneb> Is there any (non-esoteric?) language with a type representing an index into a specific array
11:04:13 <shachaf> Agda?
11:05:17 <izabera> c?
11:05:18 <shachaf> I guess that's not exactly true.
11:05:41 <izabera> oh, into a specific array?
11:05:53 <Taneb> I'd ideally like this to be strongly typed and also allow the array to mutate
11:05:55 <izabera> so if you can use foo[i] you can't use bar[i]?
11:06:02 <Taneb> izabera: yeah
11:06:06 <izabera> whyyyyyyyyyyyyyyyyyyyyyyyy
11:06:08 <shachaf> An array of length n has n+1 indices.
11:06:29 <Taneb> izabera: mostly because I ran into a bug in my code due to me mixing up arrays
11:06:39 <shachaf> Taneb: There are C++ iterators which are also not really this.
11:06:50 <izabera> maybe you should learn how computers work
11:06:57 <Taneb> izabera: that requires effort
11:06:58 <izabera> functional programming is bad for you
11:07:10 <Taneb> I'm gonna learn how maths works instead
11:07:29 <shachaf> which math are you starting with
11:07:46 <Taneb> shachaf: haven't decided yet
11:07:58 <Taneb> Maybe group theory? Group theory is fun
11:08:06 <shachaf> Anyway I'm pretty sure I've seen this somewhere.
11:08:10 <Taneb> Although not really foundational
11:11:30 <shachaf> Speaking of array index types, do you like wavelet trees?
11:11:56 <shachaf> Did you know rank maps from the type of indices of an array to the type of indices of a subarray?
11:12:00 <Taneb> I remember looking at them, but I don't know what they are!
11:12:27 <shachaf> I made a picture at http://slbkbs.org/ranksel.svg
11:13:49 <shachaf> Taneb: I think Ada might have something similar to what you're asking for but I can't really tell.
11:14:16 <shachaf> subtype Index_Type is Integer range Array'Range
11:14:38 <shachaf> You'd have to ask Sgeo_. I bet it's not really what you're asking for though.
11:15:18 <Taneb> The next question is "Would such types be remotely usable in practice"
11:17:51 <shachaf> It depends on why you want indexing.
11:18:39 <Taneb> In the instance that inspired this, I have an index into an array of indices into another array
11:20:14 <shachaf> Reasonable.
11:20:53 <Taneb> And I messed up and used my index as an index straight into the second array
11:20:56 <shachaf> I think in most languages that support something like this it would be more trouble than it's worth.
11:21:28 <shachaf> But maybe you could approximate it with less work.
11:22:28 <shachaf> For example you could have two types of arrays and indices and not do the dependenty thing where your index only works for a particular array but restrict it to a type instead.
11:23:26 <shachaf> An array is just a kind of function, after all.
11:25:52 -!- variable has joined.
11:27:48 -!- variable has quit (Client Quit).
11:29:15 -!- variable has joined.
11:30:03 -!- variable has quit (Client Quit).
11:30:49 <shachaf> @src Real
11:30:49 <lambdabot> class (Num a, Ord a) => Real a where
11:30:49 <lambdabot>     toRational :: a -> Rational
11:31:04 <shachaf> Taneb: can you learn so many maths that that class makes any sense hth
11:31:52 <Taneb> shachaf: well, the real numbers and the rational numbers are basically the same, except there's more real numbers
11:32:10 <Taneb> Every real number is pretty close to a rational number
11:32:25 <Taneb> I'm going to stop here because I really don't feel like justifying that typeclass's name
11:32:46 <shachaf> Do you think of continuity "backwards" or "forwards"?
11:33:19 <Taneb> I try not to think of continuity, personally
11:33:31 <shachaf> imo you're missing out
11:33:54 <Taneb> But if I did I'd probably think of it in some weird way that's not quite either of those options
11:34:16 <shachaf> Oh, I want to hear your weird way.
11:35:04 <shachaf> What about naturality?
11:35:24 -!- xkapastel has quit (Quit: Connection closed for inactivity).
11:36:04 <Taneb> I don't find naturality natural
11:36:46 <Taneb> Do you mean continuity as in continuous functions, and naturality as in natural transformations?
11:36:50 <shachaf> Yes and yes.
11:37:24 <Taneb> The former, I think of in terms of neighbourhoods
11:37:47 <Taneb> The latter, I can never get into my head for some reason
11:38:01 <shachaf> A natural transformation e : F -> G : C -> D is a functor e : 2xC -> D which is F at 0 and G at 1
11:38:55 <shachaf> What could be more natural?
11:39:28 <Taneb> What does this have to do with natural numbers?
11:39:37 <Taneb> And natural logarithms
11:39:38 <Taneb> ?
11:39:40 <shachaf> 2 is a natural number, and so are 0 and 1.
11:41:08 <shachaf> You can read https://pdfs.semanticscholar.org/3833/f692e93a795b51bd3d7acfd9477f9ee6d536.pdf which I think is the thing that introduced natural transformations?
11:43:52 -!- xkapastel has joined.
12:12:02 -!- int-e_ has changed nick to int-e.
12:21:45 -!- SopaXorzTaker has joined.
12:32:52 -!- AnotherTest has joined.
12:58:07 <Taneb> shachaf: thanks for the link, I've bookmarked
13:38:37 -!- hufferinho has joined.
13:42:59 -!- variable has joined.
13:45:24 -!- xkapastel has quit (Quit: Connection closed for inactivity).
13:47:21 -!- variable has quit (Ping timeout: 240 seconds).
13:57:43 -!- SopaXorzTaker has quit (Remote host closed the connection).
14:34:34 -!- variable has joined.
14:39:56 -!- variable has quit (Ping timeout: 265 seconds).
14:40:46 -!- variable has joined.
14:42:13 -!- ProofTechnique[m has joined.
14:44:05 -!- SopaXorzTaker has joined.
14:45:47 -!- variable has quit (Ping timeout: 276 seconds).
14:48:53 -!- variable has joined.
14:50:50 -!- variable has quit (Client Quit).
14:53:19 -!- variable has joined.
14:57:35 -!- variable has quit (Client Quit).
15:00:04 -!- variable has joined.
15:03:49 -!- rodgort has quit (Quit: Leaving).
15:13:36 -!- hufferinho has left.
15:16:23 -!- rodgort has joined.
15:19:20 -!- LKoen has joined.
15:32:56 -!- xkapastel has joined.
15:40:11 -!- arseniiv has joined.
16:10:18 -!- sleffy has joined.
16:14:37 -!- LKoen has quit (Remote host closed the connection).
16:28:40 -!- variable has quit (Quit: /dev/null is full).
16:39:33 -!- LKoen has joined.
17:07:53 <arseniiv> about a type of indexes to a particular array: maybe this is possible in Haskell. There’s a type of references to a particular _state thread_, STRef s a, where a is the type of referenced values and s is a magic which is works mostly because of the type of `runST`. Maybe one could define something like this for arrays. I think, you’d need to wrap arrays into some new type which would work with its indices like ST s and STRef s work
17:08:45 <arseniiv> could it be that Oleg or, say, Edward Kmett have written about something like this? IDK
17:09:28 <arseniiv> Taneb: ^
17:15:24 -!- imode has joined.
17:18:39 <arseniiv> however, I couldn’t yet imagine what type hackery is needed to represent a type of an array containing such indexes to other arrays. Existential somewhere, maybe. It seems dependent-like features of Haskell types are limited in this case (or not, I’m too far from an expert here)
17:27:06 <arseniiv> also, could these indices be pairs of an array (pointer to info about array etc.) and an index? Then it’s pretty hard to mismatch something, and the space is 8 bytes more per element, which is quite light in some cases(?)
17:28:17 -!- brandonson has quit (Ping timeout: 260 seconds).
17:28:57 -!- sleffy has quit (Ping timeout: 256 seconds).
17:29:08 <arseniiv> 8 bytes at most* (I presume 128-bit addresses aren’t yet a thing)
17:29:35 -!- brandonson has joined.
17:31:40 <int-e> IPv6 *whistles*
17:32:23 <arseniiv> int-e: are they used as pointers in some language? :o
17:32:35 <int-e> *whistles some more*
17:32:51 <arseniiv> ::
17:34:11 <int-e> it may be worth noting that the 's' in 'ST s' is a phantom type... there's no corresponding value at runtime at all.
17:34:23 <imode> https://twitter.com/Hillelogram/status/987432178840756225 money + mouth.
17:35:08 -!- contrapumpkin has joined.
17:39:50 -!- LKoen has quit (Remote host closed the connection).
17:40:49 <\oren\_> imode: interesting
17:41:46 <imode> the article that's the result of this thread was on HN's front page recently.
17:42:59 <\oren\_> I think imperative code can be easy to analyze as long as you have limits to what a given subroutine is allowed to mutate
17:43:19 <imode> hence why all of his examples are well-contained.
17:44:02 <imode> https://hillelwayne.com/post/theorem-prover-showdown/ the article in question.
17:47:41 <int-e> nice troll
17:48:12 -!- LKoen has joined.
17:51:27 -!- wob_jonas has joined.
17:52:58 -!- PinealGlandOptic has joined.
17:54:12 <imode> his analysis of the crowds involved was pretty spot on in my travels.
17:55:29 <int-e> (to my mind the main thrust behind "reasoning about (pure!) function programs is easy" is that the absence of mutation ensures separation between different parts of the program... so you can reason about a program in a modular way "for free", rather than bringing out guns like separation logic.
17:55:34 <int-e> )
17:56:13 -!- oerjan has joined.
17:56:19 -!- idris-bot has joined.
17:56:22 <imode> a good benchmark of your views would be to produce a valid proof of his examples in your theorem prover of choice.
17:56:30 <imode> else you become a "bulldog", as he puts it. :P
17:56:41 <int-e> (I'm putting "for free" in quotes because there is often a performance price that you pay for purity)
17:56:53 <int-e> imode: Isabelle has already been done :P
17:57:16 <imode> so has leftpad in several languages. we could always use a few more! :P
17:57:48 <int-e> yeah but they wouldn't fall under "my theorem prover of choice".
17:58:36 <imode> nothing stops you from putting your beliefs to work is all I'm saying.
18:03:15 <wob_jonas> Yes, I'd like some magic array index thing too. Not one where the index is tied to a single array, but nor one where you just define different types of indexes for different arrays, but ones where the index type can be conceptually different each time in a loop and lets you prove that the index is in bounds for that array. And yes, I think the ST-l
18:03:15 <wob_jonas> ike foreach type trick might be able to do that.
18:03:24 -!- SopaXorzTaker has quit (Remote host closed the connection).
18:07:02 <int-e> imode: http://downthetypehole.de/paste/Bh5NU2Xi ... this is one of these stupid cases where the specification is harder to understand than the implementation :P
18:08:39 <int-e> oh.
18:09:20 <int-e> To demonstrate the point, I forgot this bit: ∧ length (left_pad c n xs) = n
18:14:07 <\oren\_> hmm... how about an assembler with invariant checking etc 
18:15:14 <\oren\_> like, you have guarantees about how the instructions behave and it tries to prove things from that apward
18:15:58 -!- sleffy has joined.
18:16:16 <\oren\_> that should pretty much prevent any runtime overhead?
18:18:02 <\oren\_> (on the other hand, the instructions would have to be rather different from a normal CPU)
18:18:21 <imode> you could have guarantees for spans of instructions built into the hardware.
18:18:40 <imode> basically hardware assertions.
18:19:16 -!- augur has joined.
18:23:09 -!- LKoen has quit (Remote host closed the connection).
18:23:28 <\oren\_> imode: hmmmm... but if you have hardware assertions you can USE those in your instruction pipelining
18:23:43 <\oren\_> so it might not even have an overhead
18:31:42 <rdococ> Syntactic iodine: Something that you don't know is there, and something that you don't know you need, like iodine is in iodised table salt.
18:32:18 <rdococ> (Granted, what's in iodised table salt is actually various iodide salts as opposed to elemental iodine, but you get the gist.)
18:34:24 <oerjan> rdococ: sounds tricky to need it if you don't know it's there...
18:35:08 <oerjan> maybe a language using ZWSPes to separate tokens
18:35:31 <oerjan> but only when they're not both alphanumeric
18:49:41 -!- sprocklem has joined.
18:56:36 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client).
19:30:11 -!- augur has left ("Leaving...").
19:44:29 <oerjan> `? e
19:44:31 <HackEso> e is a freenode admin. e is not known to be an Agora player.
19:44:43 <oerjan> hm.
19:45:12 <Taneb> That reminds me of why someone way back when thought I was good at palindromes
19:47:58 <oerjan> arseniiv: your array idea would probably work as a use of kmett's reflection library
19:48:41 <oerjan> Taneb: why?
19:48:52 <Taneb> oerjan, I wrote, in here, "E, esoteric, ire to see"
19:49:08 <Taneb> It was oklopol who commented that
19:49:15 <Taneb> Whatever happened to them?
19:49:49 -!- wob_jonas has joined.
19:49:56 <oerjan> `quote oklopol.*never come
19:49:57 <HackEso> 656) <oklopol> i think i'll just take the usual route and go do post doc research somewhere far away and never come back and become a drug lord and kill myself
19:50:05 <oerjan> presumably that.
19:50:14 <oerjan> (he did go to Brazil.)
19:50:20 <Taneb> Ahah!
19:50:21 <wob_jonas> rdococ: re syntactic iodine => rust has a lot of those, and sometimes it horrifies me how complex some of the syntax and name lookup rules are
19:50:26 <oerjan> time to stalk him a moment ->
19:50:33 <Taneb> Hmm, I know an academic from Brazil!
19:51:02 <wob_jonas> the part that bothers me the most is how constructors and fresh variable names are (not) distinguished in patterns
19:51:23 <wob_jonas> and I find the name lookup rules rather complicated, but at least those are less worrisome
19:51:35 <rdococ> `help
19:51:36 <HackEso> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch [<output-file>] <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/
19:52:07 <shachaf> Taneb: Remember when you used to write limericks?
19:52:15 <Taneb> I try not to
19:53:23 <shachaf> <Taneb> There was a chap from Scandinavia/Who didn't have any poetic behaviour/So online he complained/And helpfulness reigned/Taneb became his limerick saviour
19:53:36 <shachaf> What happened to olsner, anyway?
19:53:43 <wob_jonas> the way the type inference interacts with the method lookup is also somewhat worrisome by the way
19:53:46 <shachaf> I can't tell people whose nick starts with o apart.
19:53:51 <olsner> shachaf: nothing?
19:54:00 <oerjan> if his homepage is to be believed, he's back at turku univ.
19:54:01 <wob_jonas> in the way you can suddenly have your program break when new apparently unrelated functions are added
19:54:08 <Taneb> shachaf, I never actually figured out if oklopol and oklofol were different people
19:54:15 <Taneb> *oklofok
19:54:38 <wob_jonas> `? palindrome
19:54:39 <HackEso> A palindrome is a word that remains the same if you take it to the mirror dimension, and then take each individual letter back to the normal dimension separately.
19:54:45 <olsner> I always assumed both oklokin are one and the same
19:55:09 <shachaf> Is () a palindrome?
19:55:20 <wob_jonas> ``` allwisdoms | grep -Ei palindrome | sport
19:55:21 <HackEso> bash: allwisdoms: command not found \ 1/0:
19:55:27 <wob_jonas> shachaf: there was a poll about that somewhere
19:55:34 <wob_jonas> ``` allquotes | grep -Ei palindrome | sport
19:55:35 <HackEso> 1/0:
19:55:43 <wob_jonas> ``` allquotes | grep -Ei palindrom | sport
19:55:44 <HackEso> 1/0:
19:55:46 <wob_jonas> none?
19:55:46 <wob_jonas> hmm
19:57:16 * oerjan was speaking about oklopol btw, didn't see people starting to talk about olsner 
19:57:26 * oerjan suspect olsner isn't at turku
19:57:32 <shachaf> olsner that endsner
19:57:49 <wob_jonas> oerjan: why? does turku not have internet?
19:57:50 <olsner> oerjan: I also strongly suspect I am not at turku
19:57:59 <wob_jonas> oh good
19:58:08 <Taneb> I would like to visit Turku some day
19:58:14 <Taneb> It seems to be an interesting place
19:58:22 <shachaf> I have been to Turku.
19:58:42 <shachaf> I took a boat to Stockholm.
19:59:02 -!- Phantom_Hoover has joined.
19:59:07 <wob_jonas> I've never been to any part of Finland
19:59:35 <oerjan> Taneb: i would have said everyone oklo* is the same, except i saw a different one on PPCG or somewhere
20:00:11 <shachaf> what about oklo?o?
20:00:28 <shachaf> Also what's the deal with ? being way harder to match efficiently for glob patterns than * ?
20:00:51 <shachaf> In fact it's not even known how efficiently you can do it?
20:01:28 <wob_jonas> what?
20:01:39 <shachaf> `olist 1118
20:01:40 <HackEso> olist 1118: shachaf oerjan Sgeo FireFly boily nortti b_jonas
20:01:48 <wob_jonas> do you mean like with the matched document preprocessed?
20:01:53 <wob_jonas> o!
20:02:25 <shachaf> I mean with neither preprocessed.
20:02:47 <oerjan> `1 grwp -Ei palindrome
20:02:49 <HackEso> 1/1:palindrome:A palindrome is a word that remains the same if you take it to the mirror dimension, and then take each individual letter back to the normal dimension separately.
20:03:02 <oerjan> `1 grwp -Ei palindrom
20:03:03 <HackEso> 1/1:palindrome:A palindrome is a word that remains the same if you take it to the mirror dimension, and then take each individual letter back to the normal dimension separately.
20:03:29 <wob_jonas> really?
20:03:41 <shachaf> `? palindromedary camel
20:03:42 <HackEso> palindromedary camel? ¯\(°​_o)/¯
20:04:11 <shachaf> i,i A palindromedary camel is one whose humps look the same from either side.
20:05:30 <Taneb> oerjan, I'm unconvinced
20:06:03 <shachaf> let's take an oklo poll
20:06:12 <shachaf> @poll-list
20:06:12 <lambdabot> ["\"k\"","Pikami","abc","dictator-for-life","maximum-edit-distance","pizza","should-lambdabot-be-more-polite","test"]
20:06:55 <shachaf> @poll-result pizza
20:06:55 <lambdabot> Poll results for pizza (Closed): pepperoni=1
20:07:01 <shachaf> wow
20:07:14 <shachaf> scow pizza
20:07:32 <shachaf> `? tanebventions
20:07:33 <HackEso> Tanebventions include necessity, Go, submarine jousting, Fueue, the universe, special relativity, metar, sand, dragons, persistence, the BBC, _46bit, progress, sanity, Italian, the grace period, the Oxford comma, ruin, and this sentence. See also tanebventions: maths or tanebventions: foods. He never invents anything involving sex.
20:07:35 <Taneb> I do like little peppers on pizza
20:08:40 <shachaf> `slwd tanebvention//s/ruin/the limerick, &/
20:08:42 <HackEso> tanebvention//Tanebventions include necessity, Go, submarine jousting, Fueue, the universe, special relativity, metar, sand, dragons, persistence, the BBC, _46bit, progress, sanity, Italian, the grace period, the Oxford comma, the limerick, ruin, and this sentence. See also tanebventions: maths or tanebventions: foods. He never invents anything involving sex.
20:10:36 <shachaf> `learn A limerick is a verse with two left metrical feet and three right metrical feet.
20:10:39 <HackEso> Learned 'limerick': A limerick is a verse with two left metrical feet and three right metrical feet.
20:11:54 <oerjan> this olist seemed a bit short
20:12:16 <shachaf> oerjan: That's only because olists come but once a year.
20:12:25 <shachaf> If it updated three times a week you'd think it's fine.
20:13:16 <wob_jonas> they come twice a year I think
20:13:48 <shachaf> I mean Mercury years.
20:18:03 <oerjan> `learn Fueue will be explained more properly once we've made another pass through all the other tanebventions.
20:18:06 <HackEso> Learned 'fueue': Fueue will be explained more properly once we've made another pass through all the other tanebventions.
20:19:58 <wob_jonas> `? necessity
20:19:59 <HackEso> If necessity did not exist, it would be necessary for Taneb to invent it.
20:20:01 <wob_jonas> `? go
20:20:03 <HackEso> Go is a common irregular verbal game programming language invented by the Germanic Taneb tribes catching monsters in the strategic territories of East Asia.
20:20:07 <wob_jonas> `? submarine jousting
20:20:09 <HackEso> Submarine jousting is unexplainable.
20:20:16 <wob_jonas> `? the universe
20:20:17 <HackEso> The universe was invented by Taneb as an opposing force to oerjan. Escardó proved that it was indiscreet.
20:20:28 <wob_jonas> `? special relativity
20:20:29 <HackEso> special relativity? ¯\(°​_o)/¯
20:28:17 <int-e> imode: http://downthetypehole.de/paste/GpP7OKaR is the fulcrum thing. The unique thing is awkward to specify and less interesting.
20:29:02 <shachaf> I think I confuse the words "fulcrum" and "frustum".
20:29:49 <int-e> Hah, I may be doing the same thing.
20:30:11 <shachaf> Well, yours seems like neither of those?
20:30:39 <shachaf> I don't know what it is.
20:31:30 <int-e> shachaf: the terminology isn't mine, but I suppose idea is to balance the left and right parts of a list as well as possible
20:31:52 <shachaf> That sounds like a fulcrm, I suppose.
20:32:15 <int-e> imode mentioned https://twitter.com/Hillelogram/status/987432178840756225 and https://hillelwayne.com/post/theorem-prover-showdown/ earlier.
20:39:06 <shachaf> unidemode
20:40:01 <int-e> anyway, that was enough fun for now...
20:41:17 <int-e> actually... "unique" has a lousy specification.
20:41:33 <arseniiv> oerjan: is it that library which could be used to supply a config through constraints and which uses that Proxy stuff?
20:42:03 <oerjan> arseniiv: yes
20:42:05 <int-e> What are "the unique elements" of [1,2,3,2,1]? I read it as [3], because 1 and 2 aren't unique in that list...
20:42:26 <int-e> but it intends the result to be [1,2,3] in any order
20:42:45 <oerjan> arseniiv: you could make the array the config value
20:43:18 <wob_jonas> int-e: [1,2,3] are the unique elements, and [3] are the unique -u elements
20:43:37 <wob_jonas> also, [1,2] are the unique -d elements, and [1,2,2,1] are the unique -D elements
20:43:46 <int-e> TMI
20:44:07 <int-e> (which really can't be a complaint on here, so carry on)
20:44:15 <shachaf> How do you catch a unique element?
20:45:19 -!- LKoen has joined.
20:45:43 <oerjan> `? tmi
20:45:45 <HackEso> tmi? ¯\(°​_o)/¯
20:48:12 <oerjan> `learn TMI is short for toenail mushroom infestation
20:48:14 <HackEso> Learned 'tmi': TMI is short for toenail mushroom infestation
20:48:35 <wob_jonas> eww
20:49:03 <oerjan> i take it my wisdom got tmi spot on
20:49:11 <wob_jonas> is that the one on the Harry toenail of ... what was it
20:49:13 <wob_jonas> `? titles
20:49:14 <HackEso> Titles J. K. Rowling had specifically denied on her webpage would be the titles of the sixth or seventh Harry Potter book are: Harry Potter and the{ Green Flame Torch, Mountain of Fantasy, Fortress of Shadows, Forest of Shadows, Graveyard of Memories, Pyramids of Furmat, Pillar of Storgé, Toenail of Icklibõgg}.
20:49:37 <wob_jonas> Harry toenail of Icklibõgg
20:50:42 <oerjan> that was strangely not on my mind hth
20:51:34 <oerjan> maybe it should be a different organ
20:53:36 <shachaf> `? hth
20:53:37 <HackEso> hth ([ʰtʰh̩]) is help received from a hairy toe. It is not at all hambiguitous.
20:54:04 <oerjan> hm i sense a pattern
20:54:20 <shachaf> `` grWp -l toe
20:54:20 <wob_jonas> `? toe
20:54:22 <HackEso> apt \ dingas \ hth \ portmanteau \ potatoes \ rincewind \ the \ title \ tmi \ toe \ twnh \ welp \ wth
20:54:22 <HackEso> The TOE is the Toe of Everything, from which our universe sprang.
20:54:22 <wob_jonas> `? toenail
20:54:24 <HackEso> toenail? ¯\(°​_o)/¯
20:54:28 <shachaf> `? portmanteau
20:54:29 <HackEso> ​«Portmanteau» is the French spelling of “port man toe”.
20:54:37 <shachaf> `? wth
20:54:38 <HackEso> WTH is wavy toe hair. hth.
20:54:44 <shachaf> `? toe
20:54:45 <HackEso> The TOE is the Toe of Everything, from which our universe sprang.
20:54:49 <shachaf> `? twnh
20:54:51 <HackEso> twnh is dubious hambiguitous help that will or will not be help. It is provided by a toe with no hair.
20:54:56 <shachaf> `dowg toe
20:54:58 <HackEso> 9094:2016-09-26 <oerjän> learn The TOE is the Toe of Everything, from which our universe sprang. \ 6001:2015-09-16 <oerjän> rm wisdom/toe \ 5996:2015-09-15 <hppavilion[1̈]> learn the Toe of Harriness\'s Enclosure \ 5995:2015-09-15 <hppavilion[1̈]> learn The Toe of Harriness\'s Enclosure \ 5993:2015-09-15 <hppavilion[1̈]> learn the Toe of Harriness\'s Enclosure \ 5991:2015-09-15 <hppavilion[1̈]> learn the Toe of Harriness\'s Enclave \ 5990:2015-09-1
20:55:02 <shachaf> `dowg wth
20:55:04 <HackEso> 8919:2016-08-15 <oerjän> learn WTH is wavy toe hair. hth.
20:55:10 <shachaf> `dowg portmanteau
20:55:12 <HackEso> 6161:2015-10-30 <boil̈y> le/rn portmanteau/\xc2\xabPortmanteau\xc2\xbb is the French spelling of \xe2\x80\x9cport man toe\xe2\x80\x9d.
20:55:15 -!- LKoen has quit (Remote host closed the connection).
20:55:17 <shachaf> `owrjan
20:55:18 <HackEso> Your omnidryad saddle principal swatty kind "Darth Ook" oerjan the shifty loud hero is a hazy expert in minor compaction. Also a Groadep who minces Roald Dahl. He could never render the word "amortized" so he put it here for connivance. His ark-nemesis is Noah. He twice punned without noticing it.
20:55:33 <shachaf> `swrjan s/kind/toe-obsessed/
20:55:35 <HackEso> oerjan//Your omnidryad saddle principal swatty toe-obsessed "Darth Ook" oerjan the shifty loud hero is a hazy expert in minor compaction. Also a Groadep who minces Roald Dahl. He could never render the word "amortized" so he put it here for connivance. His ark-nemesis is Noah. He twice punned without noticing it.
20:55:50 <wob_jonas> `? swrjan
20:55:52 <HackEso> swrjan? ¯\(°​_o)/¯
20:56:17 <wob_jonas> we need a command in bin that seds the source code of that very command
20:57:58 <oerjan> `mkx bin/qued//sled bin/qued//"$1"
20:58:00 <HackEso> bin/qued
20:58:24 <int-e> meh it's hard to stop. http://downthetypehole.de/paste/qa3R2yV3 has a few comments.
20:59:04 <oerjan> `qued s,xxx,,
20:59:05 <HackEso> bin/qued//sled bin/qued//"$1"
20:59:31 -!- PinealGlandOptic has quit (Quit: leaving).
21:00:25 <oerjan> `qued s,ed bin,wd ../bin,
21:00:27 <HackEso> bin/qued//slwd ../bin/qued//"$1"
21:00:47 <oerjan> `qued s,xxx,y,
21:00:48 <HackEso> ​../bin/qued//slwd ../bin/qued//"$1"
21:04:08 -!- LKoen has joined.
21:16:06 -!- 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.”).
21:43:35 <wob_jonas> `qued ;
21:43:36 <HackEso> ​../bin/qued//slwd ../bin/qued//"$1"
21:44:17 -!- variable has joined.
21:49:22 <wob_jonas> oh!
21:50:10 <wob_jonas> I've got it
21:52:54 <wob_jonas> arseniiv: Nora's Hair Styling on Demand, Call Us Any Time Full Movie HD
22:01:17 <wob_jonas> in fact, remove the Us
22:01:22 <wob_jonas> Nora's Hair Styling on Demand, Call Any Time Full Movie HD
22:01:36 <wob_jonas> unless you already found a better name that is
22:01:57 <wob_jonas> although someone who's actually good at English puns will probably be able to give a better suggestion
22:06:21 -!- brandonson has quit (Ping timeout: 240 seconds).
22:08:13 -!- brandonson has joined.
22:10:19 <oerjan> . o O ( i feel like i'm obliged to suggest pedicure at this point )
22:11:23 <wob_jonas> oerjan: that was my original suggestion yesterday: "have you named it Nora's Nailcare 2: Reverse Polish Full Movie HD yet? Or is that name inappropriate for a language that isn't stack-based?"
22:11:34 <wob_jonas> you can still reuse that name for a different language
22:12:26 <shachaf> I'm not so sure that there should be more Nora languages.
22:13:01 <shachaf> The world of spam is diverse.
22:14:01 <wob_jonas> a spam-based language has been very close to the top of the page in https://esolangs.org/wiki/List_of_ideas for a long time
22:16:52 <Sgeo_> Spam based language?
22:17:07 <Sgeo_> Oh
22:17:11 <shachaf> hi Sgeo_
22:17:23 <Sgeo_> Thought you meant spam that managed to accidentally persist in the esolang wiki
22:17:27 <Sgeo_> Hi shachaf 
22:17:38 <shachaf> Does Ada support types of indices into a specific array?
22:18:03 -!- Phantom_Hoover has quit (Remote host closed the connection).
22:18:11 <shachaf> If not, does Agda?
22:19:17 <Sgeo_> As in the type of the index contains the array? For both, no idea. Although it wouldn't surprise me if Agda could, just based on it being dependently typed.
22:20:36 <shachaf> But what about Ada?
22:20:50 <shachaf> You can do "subtype Index_Type is INteger range Array'Range", right?
22:23:11 <Sgeo_> I don't know Ada (or Agda except that it's dependently typed).
22:23:39 <Sgeo_> I could probably recognize that what you typed looks more like Ada than any other language I know
22:25:14 <wob_jonas> shachaf: in SQL, when a column has a FOREIGN KEY constraint, would that count as the column having a type that indexes into another array?
22:25:22 <wob_jonas> or at least similar enough?
22:33:49 -!- AnotherTest has quit (Ping timeout: 256 seconds).
22:41:05 <shachaf> Maybe.
22:41:15 <shachaf> Taneb brought this up, not me.
22:46:04 -!- oerjan has quit (Quit: Nite).
23:10:41 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client).
23:46:10 <arseniiv> wob_jonas> Nora's Hair Styling on Demand, Call Any Time Full Movie HD> oh nooooooooooo why should it be Nora all the time I don’t get it :P
23:59:21 -!- arseniiv has quit (Ping timeout: 240 seconds).