00:15:43 <Frankenlime> im not normally a fan of tools made out of shellscripts but dehydrated works so great, especially with dns auth

00:16:38 <fizzie> int-e: It *runs* twice a day, but only renews when there's less than 30 days remaining.

00:18:14 <Frankenlime> i've used acme.sh at work too and its not terrible (although only used it for web auth)

00:19:42 <fizzie> I'm using `certbot certonly --config ... --force-renewal` to basically just use certbot as a plain client (with DNS auth), it seems to work.

00:22:03 <fizzie> AIUI, the 'certonly' part means "just do the stuff related to acquiring certificates, don't try to touch the servers that use the certificate", which is what I want out of it.

00:22:34 <Frankenlime> oh well, i got it all working in ansible and haven't bothered touching it since

01:53:09 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=77874&oldid=77853 * Vpzom * (+72)

01:58:37 <esowiki> [[Four]] N https://esolangs.org/w/index.php?oldid=77875 * Vpzom * (+2759) Created page with "{{infobox proglang |name=Four |paradigms=[[:Category:Functional paradigm|Functional]] |author=[[user:Vpzom|vpzom]] |majorimpl=https://git.vpzom.click/vpzom/four |files=<code>...."

08:11:54 <esowiki> [[User:RubenVerg]] N https://esolangs.org/w/index.php?oldid=77877 * RubenVerg * (+6) Created page with "hello!"

10:19:54 <Taneb> Is there a theorem that for every positive natural, n, the Fibonacci sequence contains infinitely many integer multiples of n?

10:34:55 <cpressey> https://en.wikipedia.org/wiki/Fibonacci_number says "If the members of the Fibonacci sequence are taken mod n, the resulting sequence is periodic with period at most 6n." -- is that equivalent?

10:36:00 <cpressey> I guess it's not quite equivalent, because every 6th positive natural != every positive natural

10:36:40 <int-e> Note that F_0 = 0 is divisible by n. So together with periodicity modulo n you get what you want.

10:39:57 <cpressey> Also, simply saying "periodic" doesn't imply that F_i mod n = 0 at any time, so far as I'm aware, so, I'm not so sure

10:40:38 <int-e> Periodicity is rather obvious though; there are n^2 possible pairs of consecutive remainders in the sequence, so it's ultimately periodic. But you can also reconstruct the whole sequence from any pair (computing F_n from F_(n+1) and F_(n+2)), so it's fully periodic

10:44:54 <cpressey> Yeah OK, I see how F_0 = 0 implies it F_i mod n = 0 for some i, if it's periodic

10:46:03 <fizzie> I'm not sure I followed that periodicity argument, why does having n^2 possible pairs of consecutive remainders mean it's ultimately periodic?

10:47:25 <int-e> fizzie: because you can look at the sequence of pairs FF_n = (F_n, F_(n+1)) and note that there's a relation FF_(n+1) = f(FF_n), to which the standard argument applies.

10:49:25 <int-e> But the 6n bound is interesting, because from that idea, you only get an n^2 bound.

10:54:38 <int-e> (the "standard element" is that by the pigeon-hole principle, *some* element must repeat, and from that point onward, all the elements must repeat because that single element determines all its successors.)

10:55:26 <int-e> (and, if f() is invertible, the predecessors as well, giving full periodicity rather than just ultimate periodicity.)

11:21:42 <int-e> Oh, that's a clever use of the Frobenius automorphism. (https://en.wikipedia.org/wiki/Pisano_period#Properties near the end of the section.)

11:30:54 <int-e> "Any prime p providing a counterexample would necessarily be a Wall-Sun-Sun prime, and such primes are also conjectured not to exist."

11:30:57 <int-e> "In number theory, a Wall–Sun–Sun prime or Fibonacci–Wieferich prime is a certain kind of prime number which is conjectured to exist, although none are known."

11:36:00 <cpressey> Which is not actually a contradiction, if there really are two different mathematicians making two different conjecturs on the existence of these things

11:56:00 <cpressey> The GADT gives you an existential type that can be used for b. If you don't have that, you don't have anything you can use for b.

12:01:38 <cpressey> Mmmmmmaybe you could put both a and b in the ADT, like data Program instr a b = ...; I've tried it but I haven't been successful at it, and the error messages aren't very encouraging.

12:01:43 <int-e> Yeah, if you have a constructor of type a -> Foo b in your GADT, then that corresponds to a monadic operation a -> m b.

12:05:40 <int-e> There's a weird existential data F g x = F (forall a. (g a, a -> x)) type that a GADT g into a functor F g that can be used for making a free monad.

12:06:13 <int-e> Which I guess is nicer in theory, but as a programmer, I find the GADT describing an interface very appealing.

12:08:01 <int-e> So, properly: data F g a = forall r. F (g r) (r -> a) -- hmm Cont-style naming seems better.

12:08:27 <shachaf> I tend to call the universal one r (for "return" or "result" or something) and the existential one x.

12:09:21 <shachaf> OK, imagine you had a type for which fmap was very expensive, so you wanted to minimize fmaps.

12:09:45 <shachaf> The functor laws tell you that instead of fmap f (fmap g x), you can write fmap (f.g) x

12:10:31 <int-e> But it's a far stretch from having seen something, and kind of understanding it, to finding it natural.

12:10:49 <shachaf> An alternative thing you can say is that this thing is the free functor on a type constructor, but I bet that wouldn't strike a chord with you.

12:11:29 <shachaf> You can also use the dual: newtype Yoneda f a = Yoneda (forall r. (a -> r) -> f r)

12:11:56 <shachaf> But I find that one less intuitive, just because CPSy things are more complicated.

12:12:07 <int-e> The way I deal with category theory is to translate it back to something more concrete.

12:12:42 <int-e> The deeper you go into category theory, the more work I have to do translating it back. At some point, I get lost. :P

12:13:00 <shachaf> Well, I'm not saying any category theory words here. Except for "free", I suppose, and "dual", and "Yoneda".

12:13:55 <shachaf> I'm not calling it a Yoneda transform, I just wanted a name for the type that isn't F.

12:30:05 <lambdabot> KOAK 081153Z 28007KT 10SM OVC012 17/12 A2992 RMK AO2 SLP132 T01670122 10167 20161 56004

13:08:20 <cpressey> <cpressey> Mmmmmmaybe you could put both a and b in the ADT, like data Program instr a b = ...; <-- I think I actually got this to work!

13:12:05 <cpressey> All the instructions have to "return" the same type. The type of `singleton` becomes `instr b -> Program instr b b`

13:35:03 <int-e> But maybe you're coming from the other direction. I have not read very far into the backlog.

13:41:18 <int-e> cpressey: If you want to take the GADTs out of operational, you will probably end up with a free monad anyway. The functor is data StackF cnt = Push cnt | Pop Int (Int -> cnt) which can be obtained from unfolding the GADT data StackG a where Push :: Int -> StackG () | Pop :: StackG Int into Coyoneda StackG a.

13:44:04 <int-e> But as a programmer, StackF isn't intuitive to me, whereas StackG reads like a signature for a DSL.

13:45:35 <int-e> The problem with what you currently have is that there can only ever be a single return type, namely the `a` in Program f a b.

14:37:59 <esowiki> [[User:WhyNot?]] https://esolangs.org/w/index.php?diff=77878&oldid=77854 * WhyNot? * (+84)

15:48:36 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=77879&oldid=77874 * Konfetti * (+134)

15:49:01 <esowiki> [[Talk:RubE On Conveyor Belts/Interpreter]] N https://esolangs.org/w/index.php?oldid=77880 * Eiim * (+685) Added two questions

15:49:40 <esowiki> [[RubE On Conveyor Belts]] M https://esolangs.org/w/index.php?diff=77881&oldid=64380 * Eiim * (+4) noted that interpreter is C++.

15:54:08 <esowiki> [[Talk:RubE On Conveyor Belts/Interpreter]] M https://esolangs.org/w/index.php?diff=77882&oldid=77880 * Eiim * (+267) noted program.out

15:56:30 <esowiki> [[Talk:Hell69]] N https://esolangs.org/w/index.php?oldid=77883 * Konfetti * (+411) Created page with "I think the example is incorrect. 0x41 * 0x69 = 0x1AA9, while 0x41 * 0x45 (which is decimal 69) = 0x1185. I am not sure which version is intended by the creator. The result i..."

16:53:15 <esowiki> [[User:Eiim]] N https://esolangs.org/w/index.php?oldid=77884 * Eiim * (+150) Created User:Eiim

17:05:15 <esowiki> [[!@$%^&*()+/Algorithms]] M https://esolangs.org/w/index.php?diff=77885&oldid=76908 * SunnyMoon * (+313) Added a well-earned snippet!

18:46:09 <esowiki> [[User:SunnyMoon]] M https://esolangs.org/w/index.php?diff=77886&oldid=77827 * SunnyMoon * (+350) School update.

21:44:14 -!- 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.”).

23:53:18 <orby> I'm trying to construct a specific combinator in Underload, but I'm falling short. Any wizards know how to construct s' where s':(x)(y)(z) -> x(z)(y(z))?