00:01:22 -!- tromp has quit (Ping timeout: 252 seconds).
00:48:48 -!- delta23 has quit (Quit: Leaving).
00:50:57 -!- tromp has joined.
00:55:01 -!- sprock has joined.
00:55:46 -!- tromp has quit (Ping timeout: 265 seconds).
01:45:03 -!- tromp has joined.
01:49:16 -!- delta23 has joined.
01:49:52 -!- tromp has quit (Ping timeout: 268 seconds).
02:04:04 -!- tromp has joined.
02:08:49 -!- tromp has quit (Ping timeout: 252 seconds).
02:20:01 -!- xkapastel has quit (Quit: Connection closed for inactivity).
02:50:13 <esowiki> [[Rayuela]] https://esolangs.org/w/index.php?diff=82748&oldid=82741 * Dreamvoyager * (+1834) /* Examples */
03:11:40 -!- copumpkin has quit (Quit: Hmmm).
04:02:46 -!- delta23 has quit (Remote host closed the connection).
04:03:14 -!- delta23 has joined.
04:13:48 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82749&oldid=82748 * Dreamvoyager * (-18) /* What Everything Means */
04:16:45 -!- delta23 has quit (Quit: Leaving).
04:29:19 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82750&oldid=82749 * Dreamvoyager * (+226) /* Hello, Rayuela! */
04:46:12 -!- delta23 has joined.
05:10:10 <esowiki> [[Rayuela]] https://esolangs.org/w/index.php?diff=82751&oldid=82750 * Dreamvoyager * (-11) /* Hello, Rayuela! */
05:14:01 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82752&oldid=82751 * Dreamvoyager * (+1) /* Hello, Rayuela! */
05:20:18 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82753&oldid=82752 * Dreamvoyager * (+5) /* Full Programs */
05:27:28 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82754&oldid=82753 * Dreamvoyager * (+5) /* Hello, Rayuela! */
05:51:11 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82755&oldid=82754 * Dreamvoyager * (-14) /* Hello, Rayuela! */
05:54:46 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82756&oldid=82755 * Dreamvoyager * (+15) /* Full Programs */
05:54:52 -!- sprock has quit (Ping timeout: 252 seconds).
06:44:38 -!- tromp has joined.
06:52:37 -!- imode has quit (Ping timeout: 252 seconds).
07:12:32 <esowiki> [[User:Zzo38/Programming languages with unusual features]] https://esolangs.org/w/index.php?diff=82757&oldid=82578 * Zzo38 * (+539)
07:14:26 -!- Sgeo has quit (Ping timeout: 240 seconds).
07:17:50 -!- arseniiv has joined.
07:18:29 -!- Sgeo has joined.
07:32:06 -!- copumpkin has joined.
07:57:12 <esowiki> [[User:Zzo38/Programming languages with unusual features]] https://esolangs.org/w/index.php?diff=82758&oldid=82757 * ColorfulGalaxy (disambiguation) * (+117) /* C */ Link added
08:06:10 <esowiki> [[Special:Log/upload]] upload * Tomhe * uploaded "[[File:Hello.fj.png]]"
08:09:33 -!- hendursa1 has quit (Ping timeout: 240 seconds).
08:12:53 <esowiki> [[A.R.T.I.C.L.E.]] https://esolangs.org/w/index.php?diff=82760&oldid=82713 * ColorfulGalaxy (disambiguation) * (+215) /* Clear accumulator */ ) (Snippet
08:13:07 -!- hendursa1 has joined.
08:13:10 <esowiki> [[A.R.T.I.C.L.E.]] M https://esolangs.org/w/index.php?diff=82761&oldid=82760 * ColorfulGalaxy (disambiguation) * (+1) /* Clear accumulator */
08:15:32 -!- LKoen has joined.
08:37:24 <b_jonas> dear spammers, if you send multiple variants of the same spam shortly one after another, that just makes it more likely that I'll throw them out. even if I were so stupid as to fall for one of those "you won 1,000,000,000,000,000,000 dollars, get your prepaid card now" emails, sending two simultaneously with different details just makes you look stupid
08:38:31 <LKoen> so I hear you have a few millions millions millions of dollars that you don't want
08:44:12 <b_jonas> LKoen: also professional spam as in invitations to publish in junk journals and conferences (though Covid reduced the number of conference invitations) and book series, a lot of random newsletters from online or in-person stores where I have shopped once and gave them an email address (bioszallito.hu seems to be the most prof... prol... sends them the most frequently),
08:44:49 <LKoen> yeah I get invites from predatory journals, too
08:45:51 <LKoen> also, about two or three years ago, I started receiving spam that was pretending to be from big companies
08:46:02 <b_jonas> multiple contradictory emails of the "your email account will be locked unless you confirm your personal data" type, and even a few copies of the "your computer has been hacked and I made video recording of you masturbating, please send me bitcoins" email in perfect (not google-translated) Hungarian
08:46:05 <LKoen> mostly amazon, facebook, my phone company, and flight companies
08:46:18 <LKoen> and all those look exactly the same (appart from which company they claim to be from)
08:47:10 <b_jonas> oh yeah, emails in the name of more banks than I ever hand contact with too, emails of "your package couldn't be delivered",
08:47:25 <b_jonas> and sometimes emails in languages I don't speak of which I can't determine what kind they're trying to be
08:47:41 <LKoen> I read about scams that were about delivering unordered packages
08:47:52 <LKoen> like, you open your door, and there is a package on the doorstep
08:48:09 <LKoen> and for some reasons that helps them make money illegally (I couldn't understand the logic)
08:48:22 <esowiki> [[FlipJump]] N https://esolangs.org/w/index.php?oldid=82762 * Tomhe * (+14198) Initial FlipJump page :)
08:49:19 <b_jonas> a few months ago there was also a wave of SMS spam with "your package is on the way" and an URL, I've got several and I think they sent a lot in Hungary
08:50:02 <b_jonas> which makes sense because it's a good way to scam the older demographic who now start to get smartphones but can't use them
08:53:28 <b_jonas> but my favorite is still the dead-tree spam that I found taped to the door of my parent's house, a fake bill from some utility company (it's easy, water is still a monopoly, and while technically there are multiple companies you can contract with to get electricity or gas, most old houses still just have a contract with the successor of whatever the monopoly was), stating that they'll shut of the gas
08:53:35 <b_jonas> (or electricity, can't recall) if you don't pay the money to the bank account they give by today, and with the actual phone number of the gas or electricity company
09:07:26 -!- Sgeo has quit (Read error: Connection reset by peer).
11:04:51 -!- contrapumpkin has joined.
11:05:46 -!- copumpkin has quit (Ping timeout: 252 seconds).
11:13:28 -!- contrapumpkin has quit (Ping timeout: 252 seconds).
11:13:29 -!- copumpkin has joined.
11:20:45 <esowiki> [[Special:Log/newusers]] create * CristianCantoro * New user account
11:28:52 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=82763&oldid=82685 * CristianCantoro * (+191) /* Introductions */
11:29:48 <esowiki> [[User:CristianCantoro]] N https://esolangs.org/w/index.php?oldid=82764 * CristianCantoro * (+159) +my user page
12:15:11 -!- Hooloovo0 has quit (Ping timeout: 246 seconds).
12:20:18 -!- Hooloovo0 has joined.
12:44:24 <fizzie> I get spam for services that I think must be pretty niche. How likely is is for a random person to want to order "precision zinc and aluminum alloy die casting" for example? And even if you happen to hit a decision-maker in some business enterprise, are they really going to make purchasing decisions like that based on spam?
12:46:02 <int-e> Funny, that sounds vaguely familiar.
12:47:11 <fizzie> And that's not even close to the most obscure thing. How about "Re: Exclusive distributor of PTCA/PTA/ Introducer Sheat 0412"? (Which I think is medical equipment or something.)
12:47:14 <fizzie> It may be that these are scams of some other kind, rather than just plain advertisement, but I'd think they'd at least pick titles with a little more broad appeal.
12:48:09 <fizzie> Also on that list: "top10 Optical Fiber HDMI cables manufacturer", "TPU film updated offer", "5 axis CNC milling / Al/Zn/Mg die casting / plastic injection moulding", ...
12:48:27 <fizzie> And many emails about wire mesh.
12:49:09 <int-e> No, only the zinc and aluminium thing rings a bell here.
12:50:48 <fizzie> Hmm, should probably archive the contents of the spam folder off the IMAP server again, it's grown to 20324 messages.
12:51:16 <fizzie> Not sure why I'm keeping these, anyway. But storage is cheap, and maybe someday I'll want to build a very personal spam model or something.
12:51:28 <int-e> I was going to say... I delete spam :P
12:51:52 <fizzie> I just periodically slurp these off and compress them.
12:54:28 <fizzie> Sometimes they put the recipient address on the subject line, which sounds a little funny, when it's a role account of some sort. E.g. here's one titled "Disinfection robot bfjoust@selene.zem.fi".
12:56:27 <fizzie> "AC DC motors Micro solenoid pumps and solenoid valves bfjoust bfjoust@selene.zem.fi"
12:56:42 <fizzie> bfjoust@ gets a lot of offers.
12:58:32 <fizzie> Oh, also on that note, webmaster@esolangs.org has an email from "an IT company In India" asking if we're "interested in Design or Re-design your website".
13:10:42 <int-e> that's more plausible
13:17:02 <fizzie> Also a logistics company from China, in case we're interested in shipping some esolangs merch I guess.
13:21:16 <int-e> Oh I remember getting spam for welding machines. Somehow they seem to have given up...
13:28:21 -!- sprock has joined.
14:19:36 -!- tromp has quit (Remote host closed the connection).
14:20:33 -!- xkapastel has joined.
14:20:58 -!- tromp has joined.
14:28:24 -!- imode has joined.
14:47:24 <esowiki> [[Monicelli]] N https://esolangs.org/w/index.php?oldid=82765 * CristianCantoro * (+1083) +add page
14:55:07 -!- contrapumpkin has joined.
14:56:46 -!- copumpkin has quit (Ping timeout: 265 seconds).
15:04:14 -!- tromp has quit (Remote host closed the connection).
15:07:55 -!- contrapumpkin has changed nick to copumpkin.
15:13:14 -!- tromp has joined.
15:15:57 -!- tromp has quit (Remote host closed the connection).
15:16:12 -!- tromp has joined.
15:24:10 <esowiki> [[Monicelli]] M https://esolangs.org/w/index.php?diff=82766&oldid=82765 * CristianCantoro * (-4)
15:43:39 -!- budonyc has quit (Ping timeout: 265 seconds).
15:56:17 -!- tromp has quit (Remote host closed the connection).
16:06:06 -!- budonyc has joined.
16:09:19 <esowiki> [[99 (Esolang)]] https://esolangs.org/w/index.php?diff=82767&oldid=82735 * SunnyMoon * (+443) Forgot to add examples. (The programs I made were too long)
16:10:27 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=82768&oldid=82739 * SunnyMoon * (+26) Thought I added this already :P
16:10:46 -!- tromp has joined.
16:11:46 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=82769&oldid=82768 * SunnyMoon * (+0) The person who invented small letters shouldn't have existed
16:14:27 <esowiki> [[Rayuela]] https://esolangs.org/w/index.php?diff=82770&oldid=82756 * Dreamvoyager * (+365) /* Full Programs */
16:15:12 -!- LKoen has quit (Remote host closed the connection).
16:19:11 <imode> are there any models of computation that have popped up in recent years that model distributed computation? i.e among multiple processors/nodes in a network without shared memory.
16:28:00 <esowiki> [[OISC]] M https://esolangs.org/w/index.php?diff=82771&oldid=82104 * Tomhe * (+226) adding FlipJump
16:29:36 <esowiki> [[BitBitJump]] M https://esolangs.org/w/index.php?diff=82772&oldid=74221 * Tomhe * (+15) adding FlipJump
16:31:32 <esowiki> [[TOGA computer]] M https://esolangs.org/w/index.php?diff=82773&oldid=79384 * Tomhe * (+15) adding the similar FlipJump
16:32:50 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82774&oldid=82770 * Dreamvoyager * (+1) /* For a number abc, output abccba. */
16:33:21 <esowiki> [[Language list]] M https://esolangs.org/w/index.php?diff=82775&oldid=82769 * Tomhe * (+15) adding FlipJump
16:39:23 -!- contrapumpkin has joined.
16:41:41 -!- copumpkin has quit (Ping timeout: 240 seconds).
16:42:47 <esowiki> [[User:Tomhe]] https://esolangs.org/w/index.php?diff=82776&oldid=80490 * Tomhe * (+38) revealing FlipJump
17:03:52 -!- Sgeo has joined.
17:28:36 <b_jonas> fizzie: aren't some of those obscure ads because you once bought in a store that sells something similar, and they sold your email address for targeted ads?
17:29:08 <fizzie> Maybe, but definitely not for the `bfjoust` address.
17:29:20 <fizzie> That must have been picked up from the web with no context.
17:30:46 <b_jonas> because I know why I'm getting ads for books and medical equipment and sports equipment, those are particular stores that identify themselves
17:31:54 <b_jonas> the ones about drones, miracle cure for joints, and aphrodisiac, those I think are generic non-targeted ads sent to everyone
17:32:27 <b_jonas> so are the ones in the name of banks and paypal
17:34:54 <fizzie> Also that one that says "12,000 shed plans inside", which has been happening for long.
17:34:58 <fizzie> https://zem.fi/tmp/full_of_sheds.png
17:39:00 <imode> clearly you need a shed.
17:39:15 <imode> with 12,000 variations.
17:55:58 <zzo38> At least with the email I have set up, I only very rarely receive any spam at all.
17:56:50 <zzo38> (Although, I have sometimes received some. Sometimes when I did receive some more, I disabled that address. It was once about they have videos of me from my computer, which is impossible since I do not have a camera or microphone attached to my computer anyways.)
17:58:33 -!- tromp has quit (Remote host closed the connection).
18:06:30 -!- tromp has joined.
18:36:11 <lambdabot> Maybe you meant: tell thank you thanks thesaurus thx tic-tac-toe ticker time todo todo-add todo-delete type v @ ? .
18:41:45 -!- hendursa1 has quit (Quit: hendursa1).
18:43:50 -!- hendursaga has joined.
18:45:51 <arseniiv> trying to get how to formulate path induction from HoTT in haskell, if that’s at all possible
18:48:35 <arseniiv> if you try to write it based on inductions (folds) for your usual non-GADT types like Nat, [a], (a, b), Either a b, (), Void, you realise you get stuck at how to represent the :~: constructor which for I asked lambdabot for its type which isn’t that bad but it still doesn’t make much help
18:50:57 <arseniiv> ah, I think I see. It got too dependent in that book, it even has the usual natural number induction in a very dependent way, not just a -> (a -> a) -> Nat -> a, but a 0 -> (forall n. a n -> a (n + 1)) -> forall n. a n
18:51:22 <arseniiv> so I maybe just need to de-dependize the book version
18:54:26 <arseniiv> though I suspect then the resulting version of path induction will lose all its usefulness! Let’s check
18:55:59 -!- tromp has quit (Remote host closed the connection).
19:02:04 <int-e> `learn The password of the month is heavily guarded.
19:02:10 <HackEso> Relearned 'password': The password of the month is heavily guarded.
19:04:07 <arseniiv> something like this?.. foldPath :: (forall x :: k. a x x) -> (forall x y :: k. x :~: y -> a x y)
19:04:34 <arseniiv> am I right we may move forall x y out and make that explicit?
19:05:25 <arseniiv> foldPath :: forall x y :: k. (forall x :: k. a x x) -> x :~: y -> a x y -- or at least this way, as we can’t leave out k I think
19:06:48 <int-e> nothing has any sense
19:07:42 <arseniiv> and its definition should be something like `foldPath z Refl = z` and in this light it does indeed has a bit of usefulness in it!
19:08:49 <arseniiv> I dare we try. Dear lambdabot please don’t overheat
19:08:50 <arseniiv> > foldPath :: forall x y :: k. (forall x :: k. a x x) -> x :~: y -> a x y
19:08:51 <lambdabot> <hint>:1:17: error: <hint>:1:17: error: parse error on input ‘=’
19:08:51 <lambdabot> <hint>:1:24: error: <hint>:1:24: error: parse error on input ‘::’
19:09:42 <arseniiv> I don’t understand, I’ll resume in private now
19:09:58 <int-e> there is no multiline input in lambdabot
19:10:50 <int-e> there's no '=' in the middle of an expression, and somehow the errors got out of order
19:11:38 <int-e> (lambdabot uses a separate thread per message, and evidently forks off concurrent mueval processes... the second one was faster)
19:11:55 -!- delta23 has quit (Quit: Leaving).
19:12:09 <arseniiv> I now think I completely forgot how do we define something together with type annotation in one line: > { ann; def } doesn’t work
19:12:57 <int-e> > takes and expression. @let is for definitions, though as long as you're playing around, just using the let ... in ... syntax instead is better
19:13:46 <int-e> > let foo 0 = 0; foo 1 = 1; foo n = foo (n-1) + foo (n-2) in map foo [1..10]
19:14:41 <arseniiv> don’t worry, I’ll unlet everything later. Now I think I wrote `x y :: k` badly, it should maybe be `(x :: k) (y :: k)`
19:18:32 <arseniiv> it seems the correct typing is this: foldPath :: forall k (a :: k -> k -> *) (x :: k) (y :: k). (forall (z :: k). a z z) -> x :~: y -> a x y
19:19:26 <arseniiv> it compiles but I didn’t gave it a good expression
19:20:01 <arseniiv> I don’t immediately know for which interesting a we can make forall z. a z z
19:24:01 -!- tromp has joined.
19:27:54 <arseniiv> in the original, dependent formulation that’s way more manageable: (a :: forall (x :: k) -> forall (y :: k) -> x :~: y -> *) and (forall (z :: k). a z z Refl) and we return not just (x :~: y -> a x y) but (forall (p :: x :~: y) -> a x y p)
19:28:26 <arseniiv> hm no why would I say that’s more manageable
19:29:50 <arseniiv> but I missed the perfect example. Let’s take a = (->) !
19:31:40 <arseniiv> then we get proof transfer or something principle: foldPath id :: forall k x y. x :~: y -> (x -> y)
19:31:59 <arseniiv> well, not this way, but we can get x :~: y -> (p x -> p y)
19:32:19 <lambdabot> error: Variable not in scope: castWith
19:32:29 <int-e> :t Data.Type.Equality.castWith
19:32:45 <arseniiv> yeah I won’t be surprised it’s already there
19:33:53 <arseniiv> summer is coming and little flies or spiders are already a bit getting out of hand
19:40:16 -!- xkapastel has quit (Quit: Connection closed for inactivity).
19:41:30 -!- xkapastel has joined.
19:59:35 <esowiki> [[Jitejix]] https://esolangs.org/w/index.php?diff=82777&oldid=82740 * Kemuri * (-12)
20:26:52 -!- j-bot has quit (Remote host closed the connection).
20:27:09 -!- j-bot has joined.
20:47:56 -!- delta23 has joined.
21:18:10 <esowiki> [[Special:Log/newusers]] create * Aurasphere * New user account
21:19:12 <esowiki> [[Special:Log/newusers]] create * Dnm * New user account
21:21:47 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=82778&oldid=82763 * Aurasphere * (+154)
21:23:13 -!- delta23 has quit (Ping timeout: 240 seconds).
21:25:43 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=82779&oldid=82778 * Dnm * (+332)
21:40:39 <esowiki> [[Deadfish]] https://esolangs.org/w/index.php?diff=82780&oldid=81575 * Dnm * (+763) Added Deadfish in Zeno
21:54:17 <esowiki> [[Deadfish]] M https://esolangs.org/w/index.php?diff=82781&oldid=82780 * Dnm * (-1) /* Zeno */ Slight edits
22:01:33 -!- delta23 has joined.
22:38:46 -!- delta23 has quit (Read error: Connection reset by peer).
22:51:25 -!- tromp has quit (Remote host closed the connection).
23:04:16 <esowiki> [[GomorraSQL]] N https://esolangs.org/w/index.php?oldid=82782 * Aurasphere * (+6317) Created page with "{{infobox proglang |name=GomorraSQL |paradigms=[[:Category:Declarative paradigm|Declarative]] |author=[https://aurasphere.co Donato Rimenti] |year=[[:Category:2021|2021]] |typ..."
23:04:56 -!- hendursaga has quit (Remote host closed the connection).
23:05:40 -!- hendursaga has joined.
23:09:18 <esowiki> [[GomorraSQL]] https://esolangs.org/w/index.php?diff=82783&oldid=82782 * Aurasphere * (-2)
23:11:21 -!- tromp has joined.
23:12:05 -!- delta23 has joined.
23:13:45 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=82784&oldid=82775 * Aurasphere * (+17)
23:16:06 -!- tromp has quit (Ping timeout: 260 seconds).
23:38:23 -!- arseniiv has quit (Ping timeout: 246 seconds).
23:42:31 -!- copumpkin has joined.
23:42:35 -!- contrapumpkin has quit (Ping timeout: 246 seconds).
23:44:18 <esowiki> [[Rayuela]] M https://esolangs.org/w/index.php?diff=82785&oldid=82774 * Dreamvoyager * (-5) /* What Everything Means */
23:45:30 <esowiki> [[GomorraSQL]] M https://esolangs.org/w/index.php?diff=82786&oldid=82783 * PythonshellDebugwindow * (-32) Use wiki link
23:52:51 -!- tromp has joined.
23:54:17 -!- pfe has joined.
23:57:31 -!- tromp has quit (Ping timeout: 260 seconds).