In the case of Julia for example static arrays can be created, at runtime or not, with a fixed length that is part of the type definition, to give a less trivial example than "is an instance of". It's actually a very practical example as static arrays are of great importance for performance on certain applications.
I think most people would dismiss dynamic language examples, and that's the reason I comment Julia is dynamic in my comment, because most people interested in types are interested in using them at compile time to prove, or strengthen at least, correctness. In the case of dynamic languages types feel like just another piece of metadata and if you have "eval" available you basically can do anything. Julia actually does not use types to catch bugs but to structure programs and to improve performance when possible (to great extent).
Again, only superficially knowing julia, in what way is this static array a type over being a value as it is in java, with having a field with the length (the type being the x[] only, without length)?
It's a good question. Intrinsically, there is no difference: you need to consider how both pieces of data are used. Consider these two "equivalent" 1D arrays:
x = Vector{Float64}(1, 2, 3)
y = SVector{3, Float64}(1, 2, 3)
Both store the same data, and as a matter of fact you probably can pass them as arguments to most functions that accept arrays (if the functions are well designed). The difference however is that `y` has a more restricted interface: you cannot resize `y`. This restriction allows the compiler to optimize better the code both in time and space: dynamic arrays for example may allocate more memory than strictly necessary to speed up resizing and may do more bounds checks. In an ideal world should also catch bugs like detecting that `y[4]` is an error. So, to summarize, when you use `y` instead of `x` you are telling the computer that `length(y) = 3` is an invariant of your code and that it's safe to make that assumption. Having the number "3" stored as a type has an special meaning.
Off tangent, but these reminds me the first time I read the phrase "everything in Python is an object". That got me puzzled because in my mind if "everything is an object" then the phrase has zero information content. You cannot understand what is an object in isolation, you need to consider how the interpreter uses them. Or the first time you try understand what is a vector in mathematics. You cannot understand a vector in isolation, you need to consider the vector space it lives in, what operations are allowed.
Without any authority, I really don’t see how is it any different from any language’s arrays vs lists. I feel like it is syntax only for the age-old “let’s store the size of the array next to the data” vs a more complicated implementation like std::vector or Java’s ArrayList which may copy the content into a new, larger array behind the scenes.
So it is probably meaningless to talk about it in case of dynamically typed languages, even though type enforcement may not be needed (as it is impossible in the generic case for dependent types)
To turn the question around, what _would_ make it part of the type in your opinion, what criterion do you use to distinguish that from "having a field with the length (the type being the x[] only, without length)"?
In the case of Julia for example static arrays can be created, at runtime or not, with a fixed length that is part of the type definition, to give a less trivial example than "is an instance of". It's actually a very practical example as static arrays are of great importance for performance on certain applications.
I think most people would dismiss dynamic language examples, and that's the reason I comment Julia is dynamic in my comment, because most people interested in types are interested in using them at compile time to prove, or strengthen at least, correctness. In the case of dynamic languages types feel like just another piece of metadata and if you have "eval" available you basically can do anything. Julia actually does not use types to catch bugs but to structure programs and to improve performance when possible (to great extent).