For example TypeScript has the "any" and the "unknown" types. Both encompass the same set of values (any possible value which can be represented in the language), but the allowed operations are different.
C# has something similar with "object" and "dynamic".
For a static type system it makes more sense to think of a type as a set of supported operations rather than a set of values.
It really doesn't. 'any', 'unknown', 'object', and 'dynamic' are all 'top' in type systems (the type that is the super-type of all other types), they hold the set of all values. The fact a language assigns additional semantics based on their name is just sugar over the underlying type system, the type-system can live quite happily without names.
But even then, you could consider the name of a type a 'discriminating tag', like in discriminated unions. So, something like:
type Top = Any a
| Unknown a
| Object a
| Dynamic a
> The same type, but with different states depending on the semantics of the language.
This is just playing games with definitions. What you call "state" is a type in the type system of the programming language.
You could probably define terms such that of these, only `Void` is a "type" - for example, it's the only one that you can use directly as function inputs or outputs. (i.e. you can write a function `Void -> Int` but not a function `Maybe -> Int`.) I think that would be nonstandard, but maybe reasonable to do. But then when you explain what a "type" is you've only explained a subset of what "type theorists" talk about, which includes the others.
But to support my "nonstandard" claim:
* https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compil... mentions "Types (possibly of higher kind); e.g. [Int], Maybe"
* https://limperg.de/ghc-extensions/#polykinds talks about "types of different kinds", using Int and Monad as examples.
* https://en.wikipedia.org/wiki/Kind_%28type_theory%29 says "the type [] (list) is a type constructor". It uses the terms "data type" and "proper type" for what I think you simply want to call "type".
It's also possible usage is just inconsistent on the subject. (Evidence for this: that second link calls constraints "type-like things", when they're just types according to me.) But my sense is that usually, people engaging seriously with type theory or advanced Haskell would call Maybe and Monad types.
(You're of course right that Maybe is a type constructor and Monad is a typeclass, but that doesn't mean they aren't also types.)
For a start it's a discriminated union (a sum type), its set of values is:
a + 1
`Maybe a` is a type-lambda abstraction (still a type)
`Maybe Int` is a type-application, passing Int to the `Maybe a` type-lambda as an argument, to get a `Maybe Int` in return (still a type).
I don't know what you mean by this - lambdas are values not types. You could argue the type of the Maybe type constructor is Type -> Type but there is no Type type in Haskell so Maybe is not a 'type' in the Haskell type system in the way e.g. String is. The separation of types and values is AFAIK the defining characteristic of non-dependent type systems, which Haskell is (for now).
I think they meant "`Maybe` is a type-lambda abstraction", meaning roughly "a type-level function", which seems true to me. I don't think they meant to say that `Maybe` is a type in the same way String is. (I'd agree it's not, though I'd still call it a type.)
> there is no Type type in Haskell
Incidentally there is[1], and it even has kind `Type` just like `String` does. So you can ask "what is the kind of `Maybe Type`" (it's `Type`) where you can't ask "what is the kind of `Maybe Maybe`" (`Maybe` has kind `Type -> Type` so this is a kind error).
[1]: https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-...