It is a configuration language with general programming features, but it is decidedly _not_ Turing complete. It seems to sit at a sweet spot between "just JSON, no programming convenience at all" and "full-blown programming language with nontrivial toolchain".
Just a tiny addition: Yes, N log N is the average time, but the distribution is heavily long-tailed, the variance is quite high, so in many instances it might take quite some time till every item has been visited (in contrast to merely most items).
The keyword to look up more details is "coupon collector's problem".
You can also cover every one of the points "with high probability" in O(N log N) time (meaning: the chance you missed any point is at most 1/p(N) for a polynomial p, with the constant in the big-O depending on p.)
A good friend of mine was recently sentenced to prison for publicly using this kind of phrase during a protest for climate justice. When Germany's equivalent of the Supreme Court, the Bundesverfassungsgericht, learned of this case, the court immediately ordered their release and declared the original verdict void: According to the Bundesverfassungsgericht, (in the specific situation at hand) this phrase is more a value judgment and less a factual claim.
Together with a fellow activist, who also served as informal legal counsel, they gave a talk on this case at the 38th Chaos Communication Congress: https://www.youtube.com/watch?v=r5RmTOGucZo
The CCC hasn't been only about computers since inception. They were clearly already political in the 80s, just have a look at this zine: https://ds.ccc.de/pdfs/ds024.pdf
Somebody asked in a now-deleted comment: 'Right, and what does it mean in the context of "A monad is just a monoid in the category of endofunctors"?'
Here is an answer to this question:
What the parent poster referred to are "monoids in the category of sets". You can recognize this as they have introduced the carrier as (just a) set.
But the notion can be generalized. For instance, a "monoid in the category of datatypes" would not be given by a mathematical set and a mathematical binary operation, but by a datatype and a computable binary operation. (To make this precise, I would need to fix which "category of datatypes" I have in mind. It could be the category of Haskell types and Haskell functions, for instance; but C types and functions would work just as well. I could also go all the way to the effective topos, which contains lots of types which most mainstream programming languages are missing such as true quotient types.)
Finally, a "monoid in the category of endofunctors" is given by an endofunctor and a natural transformation. Endofunctors can be pictured as container kinds (e.g. ordered lists, unordered lists, Maybe/Optional, trees, vectors of length n, pairs, ...) and the additional datum of the natural transformation is what singles out those container kinds which support a "flattening operation" from those which don't. For instance, we can flatten a list of lists into one (long) list, but we cannot flatten a pair of pairs into one pair (we would need to drop two of the four elements).
Just as it is quite convenient that many results about integers or lists also hold for all monoids in the category of sets, it is quite nice that many results about monoids in the category of sets also hold for all monoids in all categories and hence in particular to monads.
Gwern has an interesting take on this: https://gwern.net/cyoa By pivoting to "choose your own adventure"-style games, multiple issues (quality, costs) might be resolved.
Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again.
There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.
Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either?
If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?
Suppose that you've written down a function enumerate, that maps all natural numbers to functions that themselves map all natural numbers to booleans. We then can write down the following program.
(defn unenumerated (n) (not ((enumerate n) n)))
This function can be recognized as Cantor diagonalization, written out as a program.
If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.
This argument is, of course, just Cantor's diagonalization argument. From an enumeration, it produces something that can't be in that enumeration.
> If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.
Okay, but if we take the position that only non-halting (for all inputs) programs represent functions over N, if your program “unenumerated” never halts for some N, it doesn’t represent a function, so your argument isn’t a case of “using the enumeration of all functions to produce something which doesn’t belong to the enumeration”
Obviously an enumeration of all computable functions isn’t itself computable. But if we consider Axiom CompFunc “if a function over N is computable then it exists” (so this axiom guarantees the existence of all computable functions, but is silent on whether any non-computable functions exist) and then we consider the additional Axiom CountReals “there exists a function from N to all functions over N”, then are those two axioms mutually inconsistent? I don’t think your argument, as given, directly addresses this question
It's just a straight up liar's paradox. If enumerate is a function that works as advertised, then unenumerated is as well. If enumerate tries to list unenumerated, then enumerate can't work as advertised.
For the argument that I gave to work, you need what you might call Axiom ComposeFunc, you may always compose a new function by taking an existing function and doing something that is known to be valid with it. Obviously this axiom is true about the computable universe. But, more than that, it is also true about any generalization of "function" that behaves like most would expect a function to have.
Now it is true that your Axiom CompFunc and Axiom CountReals do not necessarily contradict each other. But CompFunc, ComposeFunc and CountReals do contradict each other, and the contradiction can be built by following Cantor's diagonalization argument.
If I understand what I just Googled correctly (definitely not guaranteed), the reason why Cantor's argument can fail in NFU is that NFU does not necessarily allow you to build a function that returns things in X, out of a function that returns functions returning things in X.
So it has non-computable functions, but also has a type system that tries to avoid allowing self-reference. And that type system gets in the way of Cantor's argument.
I clearly hadn't thought of this possibility. It is a constraint of a kind that doesn't show up in the computable universe.
And so, going back, if the the Russian constructivist school does indeed center on computability, then my first answer to you was correct.
Right, I think we are in agreement - a pure Russian constructivist approach which only permits computable functions cannot prove the reals are countable. However, I still am sceptical it can prove they are uncountable-if you limit yourself to computable constructions, you can’t actually computably construct a Cantor diagonal, so his argument fails just like it does in NFU.
The (un)countability of the reals is known to be independent of NFU-it is consistent both with the reals being countable and them being uncountable. There are two different axioms which it is standard to add to NFU to decide this-AxCount≤ which implies the reals are countable and AxCount≥ which implies the reals are uncountable.
I guess I was suggesting that in the same way, an additional axiom could be added to computable set theory which renders the reals countable or uncountable. If an additional axiom asserting the countability of the reals involves the existence of a function from the naturals to functions over the naturals, that would obviously be introducing an uncomputable function-but for that to produce an inconsistency, it would need to enable Cantor’s argument-and, given your “ComposeFunc” in the computable universe is already restricted to only operating over computable functions, it is reasonable to limit its application to computable functions in an extension, which would mean the addition of this uncomputable function would still not permit Cantor’s argument
There is nothing uncomputable with the cantor diagonalisation. The Russians gladly accept it, I assure you. Here is a Haskell implementation:
diag :: (nat -> (nat -> Bool)) -> (nat -> Bool)
diag f n = not (f n n)
The following argument is also constructive. Just like in classical mathematics, crustructive mathematics proves the negation of A by assuming A and deriving a contradiction. (But you cannot prove A by assuming it’s negation and deriving a contraction):
Assume a surjectiom f :: nat -> Bool. Then there is x such that f x = diag f. Since these two functions are equal, they take equal values when we evaluate them in any point. In particular f x x = diag f x, but since diag f x = not (f x x), by definition, we have that f x x = not (f x x). This is a contradiction since not does not have fixed points.
( I made nat a type variable here since this works for any type / set )
I like Vim's digraphs, which go in a similar direction. For instance, Ctrl-K = > gives ⇒, Ctrl-K a * gives α. An overview of available digraphs is available at :digraphs.
Otherwise I like the Agda input method of Emacs, where \to gives ⇒ and \alpha (or \Ga) gives α.
Somewhat predictably zsh also has a digraphs¹ feature, via the insert-composed-char function². Supported characters can be seen in source³, and beyond that there is the insert-unicode-char² function for when you need it.
I flit between regular compose key input and zsh/vim digraphs in a way that makes no sense to me whatsoever. Compose ^1, AltGr+1 or C-k 1S all kind of feel natural to me, but the advantage of the ZLE method is that you can also use it to preview characters which can be useful if you want to test something out while in another widget or find the hex value to insert using some other tool.
I'm currently creating an interactive tutorial on Agda, with lots of embedded exercises (running purely in the browser/on a server, no installation required), perhaps it is useful to some:
It is a configuration language with general programming features, but it is decidedly _not_ Turing complete. It seems to sit at a sweet spot between "just JSON, no programming convenience at all" and "full-blown programming language with nontrivial toolchain".