Type theory with an Any/Variant type

Question

Let's say I have a type system that has has three primitive types in addition to the null value:

• null
• bool
• num
• string

Additionally, there is a typed array for each of the types, so we now have: null, bool, bool[], num, num[], string, and string[] as all of our types.

Finally, we have an Any type that can contain any other type. For example, we might have two columns like this:

id (num)	value (any)
1	"abc"
2	[1,2,3]
3	[1, true] ??

My question then is whether the any[] value, such as [1, true] is also contained within the any type (since it can be "anything"), or is [1, true] not a valid value for that type? In other words, what "types" do I need in my type-system -- option 1 or option 2 below?

1. null, bool, bool[], num, num[], string, string[], and any
2. null, bool, bool[], num, num[], string, string[], any, and any[]

And, if we only need the first version, does that then support recursion, such as [[1, true], [2, "hi"]] (that's two levels, i.e., any[][] and so so on), what about a jagged array, such as [[1,"a"], 0] ?

Answer 1

A type system with (perhaps unnatural) limitations is still a type system.

Any of the possibilities you have laid out would be possible to define grammars for, fully specify, and implement. You could even do other things like allow recursion only to a fixed depth, or have separate jagged and non-jagged nested array types.

The answer to the question of whether a type system could work any of these ways, is yes in each case.

If you are deciding on the type system yourself, the question then becomes whether you should allow any[] and whether any should allow nested arrays or not. The answer to that question depends on what your reasons for working with a type system are. There’s no one best answer for all contexts here.

Answer 2

I have never dealt with theoretical issues, but through dealing with programming I will say the following: We have the types null, bool, num, string. Everything else will arise from them. eg any = (null || bool || num || string). On the other hand, arrays are not types but forms of organization of types. So if I look at this ['aaa','bbv'] from the outside I'll say it's an array, but to tell what type it is I have to see the inside. If all the internal elements are of the same type then we can say that we have an array of type e.g. String, otherwise we have an array of type any. So, since the array is not a type but a form of organization, it is also necessary for the any type