This is a proposal to extend Base.in with the isa method:
julia> Base.in(::T,t::DataType) where T = T<:t
julia> 1 ∈ Int
true
julia> 1 ∈ Float64
false
or alternatively
Base.in(v,t::DataType) = v isa t
Would this be a proposal that could get approved?
This notation would make a lot of sense mathematically.
What file should I add this command to, if I make a pull-request?
I am not sure this is a good idea. While one can think of a type T as a set containing all values x::T, this would implicitly make types something like a collection.
Then we could also support ⊆ etc, but I think that keeping calculations on types distinct from calculations on values is actually a feature.
Also,
x isa T
takes one character less to type than x ∈ T (with something like \ i n TAB in most IDEs).
compare x∈T with x isa T, that is 3 characters vs 7, that is a 230% increase in width
Let’s suppose this is a problem then, what problems would this cause for programmers?
Type instances can be interpreted as unordered sets, elements of types belong in their set.
I think that the right question to ask is not what problems something could cause, but what benefits it would bring. (Though you will find that a lot of style guides prefer spaces around infix operators, I regret mentioning keystrokes, since that is a trivial concern.)
The right question to ask is whether you would want to write generic code
x ∈ C
where C is sometimes a type, other times a collection. Having a use case for this would be the best way to argue in favor of this proposal IMO.
This kind of syntax addition always come with the issue of allowing input that was not indended by the user and therefore failed to catch mistakes.
For this case, there have been many cases where a user typed the type name (like Vector{Int}) instead of constructing one. in would have raised no error with this.
Minor nitpick:
julia> [1] in Vector
ERROR: MethodError: no method matching iterate(::Type{Array{T,1} where T})
julia> Base.in(::T,t::Union{Union, UnionAll, DataType}) where T = T<:t
julia> [1] in Vector
true
However, I am against. Julia’s type system does not map directly to the naive interpretation “a type T corresponds to the set of all x with x isa T”. Heck, the subtype relation is currently not even transitive (cf 26108):
julia> A = Tuple{T, T, Vector{T}} where T;
julia> B = Tuple{T, T, Any} where T;
julia> x = (1, 0x01, []);
julia> x isa A, x isa B, A<:B, B<:A
(true, false, true, false)
One (minor) benefit is in DomainSets.jl we need a wrapper to represent all elements of a given type. Supporting in would avoid this wrapper.
Though I agree that the benefit is less than the work /thought needed to make sure it doesn’t have unintended consequences.
There are different notions of sets; ∈ or in refers to something more like an enumerable collection of values, while a type refers more to a set of possible values. E.g. Integer doesn’t necessarily refer to the set of integers, but rather represents a fact like “we have an integer, but we don’t know which one”. There are other interesting differences. For example, does T == Union{} necessarily follow if T has no instances? Consider
struct Empty
x::Empty
end
It is not possible to construct an instance of that type, but we don’t bother to make Empty == Union{} because there is some interpretation (based on bits you might have in memory) where instances exist.
So, types might not be sets, but not because of a bug in the system! Whether floating point numbers are real numbers, for example, does not depend on whether your pentium has the fdiv bug.
To add to what @foobar_lv2 and @jeff.bezanson are saying: a concrete example where isa and ∈ carry different expectations (at least for me) is
1//1 ∈ Integer
which should be “true” if we consider Integer a set. In julia-speak, one can obtain that effect by e.g.
julia> Base.in(x, C::Type) = try convert(C, x); true; catch; false; end
julia> 1//1 ∈ Integer
true
julia> 1//2 ∈ Integer
false
To be clear, I’m not advocating this (at all). Just showing why ∈ == isa is not so natural.
In math, yes, but not in Julia. Just like 1.0 is not an Integer.
(This is orthogonal to the proposal in this topic).
In Julia y in X if for any x in X, y == x:
julia> 1.0 in [1]
true
So under this proposal 1.0 in Integer should return true.
My understanding is that the original proposal was to implement the semantics of isa.
What you are describing is
Right, the original proposal is inconsistent with in. So if in were supported for types you’d want, for example:
julia> 0.0 in (false,true)
true
julia> 0.0 in Bool # should return true
So we figured out another issue: Many people naively expect that isequal(a, b) implies isequal(a in X, b in X), and this is indeed true for Base.Set. However, isequal(a,b) does not imply isequal(a isa T, b isa T).
The more general issue is that most of mathematics and set theory is extensional in style (a set is defined by its elements, i.e. by its extent), which is very appropriate for reasoning about facts, and allows things like the excluded middle. In contrast, types are more intensional in style and are better suited for reasoning about proofs, code and data layouts.
A further issue is that we really don’t want to mix sets (where most user’s mathematical intuition applies) with the julia type system (which is amazingly intuitive on a superficial level and really weird, undocumented and not very well understood on a deeper level).
Weird is in the eye of the beholder 
, but I am curious about the parts you consider undocumented. Perhaps they could be improved.
The transitivity failure linked above. Out of x isa A or !(x isa B) or A<:B, which is the incorrect judgement? Or are we happy with lack of transitivity?
Then the way we almost have dependent types. Naively one would expect
julia> struct bi_inv{A,B} end
julia> is_isa = bi_inv{N,X} where Type{N}<:X<:Any where N
julia> is_int = bi_inv{N,X} where Type{N}<:X<:Int64 where N
julia> bi_inv{3, Int64}() isa is_isa
false #should be true
julia> bi_inv{3.5, Int64}() isa is_int
true #should be false
julia> Type{3} <: Int
true
julia> Type{3} <: Integer
false #transitivity fail
Then there are various front-end normalizations.
A proper documentation/spec would permit me to implement the julia type system: It would give me the necessary information to construct a data structure that is at least as expressive as julia’s type system, tell me how to map julia syntax into this data structure, and allow me to write code that does all the necessary judgements. Optimally this would allow a simple proof of transitivity / soundness, as well as a simple proof that judgements are decidable (algorithm must terminate in finite time), or even reason about computational complexity. The neccessary judgements are isa, <: and is_concrete; the latter is absolutely essential because julia wants A<:B && B<:A to imply A==B, and wants this to imply invariant{A} == invariant{B} and wants these to imply compatible data layouts. Cf the existential crisis segfault. (side-note: Since we need to judge concreteness of types anyway, why are we not exposing this to users?)
This information is missing; the only thing to do is to read the source. It is very hard to speak about “implementation bugs” since there is no spec.
The above may sound pretty devastating, but I am actually OK with julia’s type system being an informal and maybe unsound underbelly that is nevertheless pragmatic and very rarely touches real code.
It’s almost as if you want a slightly different predicate from in…
I don’t want anything, I’m just saying that if in(::Number, ::Type{Bool}) were implemented it should be the case that Bool represents all booleans (false,true) and that 1.0 in Bool returns true.
It’s more saying overriding in is a bad idea, and better to stick to our current wrapper approach.
Your confusion confuses me. The issue you linked to has the word “bug” in the subject and is labeled as “bug”. How much clearer could one possibly get about the fact that it’s a bug and not by design? Other similar bugs have been fixed in the past, but this one isn’t particularly pressing (it’s not causing crashes) and fixes to these sorts of things tend to be slightly breaking, so you don’t want to rush them. (And there are more important things to work on, like multithreading.)
If you want documentation of Julia’s type system there’s quite a bit of it in the manual and in more formal publications as well:
That second link is an entire paper on the subtype relation (which is the heart of the type system) with a page of inductive definitions, if you’re into that sort of thing. If you’re not into that sort of thing, I think the manual does a pretty good job explaining the type system from a practical, non-theoretical view point. If there’s anything that could be explained more clearly, please do point it out.
I know, I meant “you want” in the collective sense of “one wants”. The point is that in and isa are sufficiently subtly different that using the same function for both meanings seems like a bad idea when examined closely.