Ian @im@mastodon.sdf.org

"An ordinal is a downward-closed set of ordinals" thanks, I love it

The strange joy of recursive/inductive definitions that look ill-founded but aren't

@radicalrobit
Why do I have to pick just one of these?

@ldbeth I guess what I'm interested in is whether this is a problem for things like totality checking and type-driven programming, i.e. do you necessarily introduce inconsistency in an otherwise-total language by incorporating classical operators like that

@ldbeth so to my understanding, when you branch on a call/cc-based witness for A∨(A→⊥), you initially take the negative branch. Then, if you later find across some A-term and feed it to this 'function', instead of returning an impossible value (or diverging, or whatever) it transports you to an alternate reality where you took the positive branch all along.

Is that about right? Just trying to understand this stuff better, I'm a dabbler at best

@ldbeth OH, saying Church-Rosser gave me what I needed to get it, I think. So the problem it causes is that once your expressions include control operators you can no longer reason syntactically by rewriting terms in whatever order is convenient, because different reduction orders might yield different values? You have to know in detail what the machine is actually doing. Or something like that.

I suspect that if Alonzo Church had known that people would one day have to write out the word 'lambda' over and over in their programs, he would have called it the
\-calculus instead

@ldbeth
Nondeterministic in what sense? In the sense that if you run the whole program multiple times it will do different things (seems like that ought to require some external input in principle), or just that the return value of a given function might not be the same in all contexts? I guess I can see why that's surprising but I don't understand what problems it could cause

Can someone who knows a bit about constructivism and computational interpretation of logic tell me why call/cc doesn't suffice as a witness for double negation elimination? What’s not constructive about it?

Pro tip: being bad at saying “no” to requests does not make it everyone else’s responsibility to never make a request that you might want to say ”no” to

I think the real answer is "returning #f on error is and always has been a hack, compared to using a proper optional type"

Philosophical coding question. In #Racket (as with other #Scheme-based languages) it's common for procedures to return #f (false) to indicate failure. So the following one-liner is occasionally useful for simplifying code that deals with the output of such procedures:

(define (opt-map proc arg [default #f])
(if arg (proc arg) default))

But as written, this still returns #f, rather than the given default, if arg is not #f but (proc arg) is. The question is, is this a good or a bad thing?

Supposedly there are some who prefer rejection-sampling a d4, but those people don't deserve a voice in this poll

Boost for visibility pls

Which of these is the correct way to get a d3 result from a six-sided die?

Of 24803 registered third-level domain names in the .name tld, 15079 (~61%) of these have ns01.yahoodomains.jp and ns02.yahoodomains.jp given as their nameservers, but said servers refuse all record requests for these domains (even when coming from a VPN exit point in Japan).

Wait, it's not that they have no dns records, ns1.yahoodomains.jp is explicitly refusing to answer. Maybe region-locked? Curiouser and curiouser

@publius
That could well be so but I would still like to understand how it is that they are using it in this case.

Whois information being as heavily redacted as it is these days, I can't really tell if these names are all owned by some Yahoo!-subsidiary holding company or all by different people or what

I've been digging through the zone file for .name, specifically looking at third-level registrations of actual personal names, and... a tremendous majority of these (I'd estimate 85-90%) are
* Japanese names
* with Tucows as registrar
* with Yahoo! Japan as reseller and nameservers ns#.yahoodomains.jp
* and with no records besides the NS records themselves
* but which have nonetheless been continually renewed for years.

What exactly is going on? What is Yahoo! doing with all these names?