My humble opinion, what is the point of using one of the strongest statically typed language in a dynamic way?
If you prefer or for your problem a dynamic solution would be best, that’s great.
But I do not think that trying to force a tool to do something that it was not intended to do is a good idea.
Most (if not all)Scala programmers will tell you that an Any is a bad practice and that you should rethink your design to avoid that.
Of course, the language provides basic reflection support, but again most people will tell you to stay away from it.
Just out of curiosity, what would be the answer of the opposite question.
How to add static guarantees to Cloujure? (disclaimer that all I know about Cloujure is its name and that it runs on the JVM).
Yes, the utility of such questions is expected to be controversial or provocative.
I don’t know Clojure very well but I understand that there’s a syntax/DSL built in the standard library of the language for the programmer to encode assumptions about types. By types I don’t mean java types, but rather which sets of values are expected or guaranteed. I don’t know whether the compiler takes advantage of these declarations to make code optimization or allocation purposes.
The reason I ask is that although I’ve shown you how to get from a Class to a Type, as you asked, I don’t see what you’ve gained by doing this, because 1) the Type doesn’t carry any information that the Class didn’t have, 2) the Scala reflection API (Type) is a great deal richer and more complicated (and, as a result, more cumbersome) than JVM (Java) reflection (Class), so there’s good reason to avoid it unless it’s actually buying you something.
You’ve indicated that you’re interested in what you can find out about values that you don’t have any compile-time type information about. That’s exactly what JVM reflection does, and it isn’t what Scala reflection is for.
I’m not that strong on math theory, but for each class there must be a corresponding bytecode representation, and these can be assigned Gödel numbers, so they must be countable, no? Furthermore, all the relevant components of a class (constant pool entries, method/field count,…) have hard limits assigned in the JVM spec, so I’d even assume that the set of classes is finite.
As long as each type can be described in Scala (i.e. using a finite amount of characters), the number of types is countable, because the set of finite character strings is countable.
@curoli, here is my understanding. Maybe I’m wrong, but it is usually considered that the number of types is uncountable. Why? Because the number of objects the language can represent is countable. And a type represents a set of values, i.e. a subset of objects. The number of subsets of an infinite countable set is uncountable, and the number of subsets of a finite site of size n is 2^n which is larger than n.
While the number of subsets is uncountable as shown by Cantor, the number of definable subsets is countable as defining properties can be enumerated. I would think that types correspond to (a subset of) definable subsets.
The way I understand it is that any programmatic representation of types each type designator corresponds to some type. Since the type designators are objects in the programming language, then it is only possible to designate countably many types. However, this in no way claims that all types are designatable, nor that the set of types is countable.
If the set of classes is countable, then so is the set of types.
If classes are countable, we can assign a unique integer (ordinal) to each class.
Then, we assign a rank to each type which is the sum of the ordinals of all classes involved, counting those multiple times that are used multiple times (e.g. the rank of List[List[List[Int]]] contains List three times)
We convince ourselves that for any given rank, the number of types of that rank is finite.
We can also, for any given rank, sort all types of that rank somehow by the ordinals of the classes involved.
Now we can number the types by sorting them by rank, and then sorting them within each rank.
Therefore, types are countable, at least if we can express them using classes.
Can any subset of values be expressed as a union of singleton types? If so, then the set of types contains a subset the size of the powers of the integers, and is thus uncountable. However, I’m not sure whether this is possible given that we only have finite union.
If we assume a finite memory model, and consequently only a finite number of values, and finite number of machine states, then yes we have finitely many types. But don’t we normally assume that types like List or BigInt have infinitely many values?
Oops, yeah, you are right. Types can have an infinite number of possible values if we disregard real-world limitations.
But, you still cannot define a new type by picking an arbitrary subset of an existing type.
For example, I think you cannot define a type containing all values of BigInt that represent even numbers.
If you could do that, it gets more complex, but on the other hand, if you require that each type or value can be expressed by a finite amount of Scala code, then their number must be countable, because the set of all finite Scala codes is countable.
you still cannot define a new type by picking an arbitrary subset of an existing type.
You can totally do that.
That is basically what refined types are.
because the set of all finite Scala codes is countable.
If we forget about real-world limitations.
Types can be infinite, as I show, you pick any type constructor and keep calling it recursively on the previous type.
So if we say:
List[Int] is equivalent to 1
List[List[Int]] is equivalent to 2(1 + 1)
List[List[List[Int]]] is equivalent to 3(2 + 1) | (1 + 1 + 1)
etc
So we can conclude that just the subset of all List like types are infinite; the same way natural numbers are infinite.
I am not quite sure.
However, I am not really an expert in mathematics and formal proofs. So, what I am about to say may not make sense.
I showed that the subset of List like types starting from Int is infinite, and countable since we can draw a correspondence with it to the natural numbers set.
But, this is just a subset of the set of all the List like types, since we can start with String, Double or any other type, including some List[X]. So we can conclude that there is a power set of all the sets of all List like types subset.
And that was just with List, we have many other higher kinded types and we can start mixing them, so there is even anther powerset.
So we can see that this is really more similar to the real numbers, where there is an infinite subset of numbers between any two numbers; and such set is uncountable.
Anyways, I believe this turned out a bit off-topic. @jimka sorry about that.
When you have, for every type X, also List[X], List[List[X]] and so on, you are basically taking the union of an infinitely countable number of infinitely countable sets, and such a union is still countable.
If, however, you take the powerset of an infinitely countable set, i.e. the set of all possible subsets, then such powerset is no longer countable.
If you have a type with an infinite number of objects, and you consider each subset of those objects a type of its own, then you have an uncountable number of types.
However, most of those types cannot be expressed using a Scala source document, or any kind of document, since the set of all documents is itself countable.
So, if you consider only such types that can be expressed using Scala code, then you again have a countable number of possible types.
It is an interesting discussion. But I agree it is off topic.
Several things that have always bothered me about type theory is that we make several broad assumptions as computer scientists. E.g., we assume infinite memory. In fact memory is finite, but it is not modeled in the theory anywhere. Thus type theory can tell us things about ideal systems, but at which point do esoteric (and interesting) discussions become so abstract that they are meaningless. It’s not clear to me at all.
