An "everthing" type is impossible. It would not only have to be a float, a list, a string, but also a tuple, a monad, and everything else. So 0 might work as an empty string, and 1 might work as a string, but 1 wouldn't work as a dictionary at all, or as a monad, or...

Well, existential types are pretty similar. If you've got (exists a . a) then you have to be prepared for it to be a float, but also prepared for it to be a list, or a string, but also a tuple, some type for which we only know that it is a monad, and everything else :)

More specifically, we've lost any information to tell us what specific thing might be here so we have to be prepared for any answer. It's the inverse of (forall a . a) which we can ask to become whatever we like.

In that case the everything type is just bottom.

(edit: to be clear, the bottom type, aka zero/empty type).

But bottom is "nothing" and how can "everything" be "nothing"? But then again, should "everything" contain (is that even the right word?) all things, each and every thing, including "nothing"?

"Everything" is the intersection of all types (rather than the union, which is "Anything").

It does not means that it contains the values that all types contain. Rather, it contains the values that belong to every type. In other words, in order to belong to the type "Everything," a value has to simultaneously belong to every other type.

One way to think about this is that the name applies to each member of the type, not to the type as a whole. "Anything" is an accurate description of any possible value, so the set contains all values. "Everything" does not apply to the entire set, but to each individual element. An element must be everything all at once in order for us to describe it as "Everything." Nothing does that, so "Nothing" does that.

This confusion is why explicitly using logical quantifiers is preferable: `exists x. x` is (isomorphic to) the top type (if there is one), and `forall x. x` is (isomorphic to) the bottom type (if there is one).

Avoid natural language like the plague.

Bottom's not a type; it's a value that inhabits all types.

Some type systems also have a bottom type, and this has nothing to do with the bottom you're talking about.

If you consider subtyping, Bottom is a type IIRC, In the category with types as objects and subtyping relationship (a->b if b is subtype of a) as morphisms, Any is the initial object and Bottom is the final object of the category

I think normally one considers the opposite category, where arrows go from subtypes to supertypes, because it can be embedded in the usual category of types and functions, by considering each arrow as the upcasting function.

And what is the type of that value?

Yes, I've seen Any (or top) described like that. It is the super-type of all types. Therefore, as you say, "Any value in your type system belongs to the top type". Imagine the following:

   foo = Sheep.new         => a sheep
   foo.is_a(Any)           => true (for anything! by the nature of Any)

I agree that "some" looks like "any". I wonder is there any (ahem) semantic difference in the context we are considering.

I can see why you would say that (every)thing is the "and" of all my types. But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves.

Programming environment-wise I'm having a hard time imagining how "everything" would work. It must be related to for_all or universal quantification somehow...

"Programming environment-wise I'm having a hard time imagining how "everything" would work."

It may be worth taking a moment to skip out on the abstraction and look more at the representation layer. In the general case, in most if not all implementations, "Any" basically translates to a "Variant" type: https://en.wikipedia.org/wiki/Variant_type

"Dynamically-typed languages" are basically those languages where all variables have the type Any. (The values generally have specific types, but the variables are all Any.)

> But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves.

Types are there to describe the values that can be manipulated by your program. So "as well as the types themselves" is only a concern if your language can manipulate types as first-class values. And this is not so different from all the other types in your language, at this point.

What property should a value hold to belong to the "everything" type, then?