# Proposal for ∈ isa type syntax

**URL:** <https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667>\
**Category:** Internals & Design\
**Tags:** proposal, syntax\
**Created:** [May 28, 2019, 12:56am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667 "2019-05-28T00:56:10Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![chakravala](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/chakravala/32/6832_2.png) [@chakravala](https://discourse.julialang.org/u/chakravala)\
**Post date:** [May 28, 2019, 12:56am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/1 "2019-05-28T00:56:11Z")

</div>

This is a proposal to extend `Base.in` with the `isa` method:

```nohighlight
julia> Base.in(::T,t::DataType) where T = T<:t

julia> 1 ∈ Int
true

julia> 1 ∈ Float64
false

```

or alternatively

```nohighlight
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?

---

<div class="post-metadata">

**Author:** ![Tamas\_Papp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tamas_papp/32/25949_2.png) [@Tamas\_Papp](https://discourse.julialang.org/u/Tamas_Papp)\
**Post date:** [May 28, 2019, 5:50am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/2 "2019-05-28T05:50:43Z")

</div>

> [@chakravala](#):
>
> This notation would make a lot of sense mathematically.

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,

```julia
x isa T

```

takes one character less to type than `x ∈ T` (with something like \ i n TAB in most IDEs).

---

<div class="post-metadata">

**Author:** ![chakravala](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/chakravala/32/6832_2.png) [@chakravala](https://discourse.julialang.org/u/chakravala)\
**Post date:** [May 28, 2019, 10:58am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/3 "2019-05-28T10:58:29Z")

</div>

> [@Tamas\_Papp](#):
>
> 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

> [@Tamas\_Papp](#):
>
> 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.

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.

---

<div class="post-metadata">

**Author:** ![Tamas\_Papp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tamas_papp/32/25949_2.png) [@Tamas\_Papp](https://discourse.julialang.org/u/Tamas_Papp)\
**Post date:** [May 28, 2019, 11:21am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/4 "2019-05-28T11:21:31Z")

</div>

> [@chakravala](#):
>
> Let’s suppose this is a problem then, what problems would this cause for programmers?

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

```julia
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.

---

<div class="post-metadata">

**Author:** ![yuyichao](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/yuyichao/32/20_2.png) [@yuyichao](https://discourse.julialang.org/u/yuyichao)\
**Post date:** [May 28, 2019, 11:32am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/5 "2019-05-28T11:32:44Z")

</div>

> [@chakravala](#):
>
> Let’s suppose this is a problem then, what problems would this cause for programmers?

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.

---

<div class="post-metadata">

**Author:** ![foobar\_lv2](https://avatars.discourse-cdn.com/v4/letter/f/ee59a6/32.png) [@foobar\_lv2](https://discourse.julialang.org/u/foobar_lv2)\
**Post date:** [May 28, 2019, 12:40pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/6 "2019-05-28T12:40:03Z")

</div>

Minor nitpick:

```julia
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](https://github.com/JuliaLang/julia/issues/26108)):

```julia
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)

```

---

<div class="post-metadata">

**Author:** ![dlfivefifty](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/dlfivefifty/32/1959_2.png) [@dlfivefifty](https://discourse.julialang.org/u/dlfivefifty)\
**Post date:** [May 28, 2019, 8:29pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/7 "2019-05-28T20:29:38Z")

</div>

> [@Tamas\_Papp](#):
>
> but what _benefits_ it would bring

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.

---

<div class="post-metadata">

**Author:** ![jeff.bezanson](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/jeff.bezanson/32/48_2.png) [@jeff.bezanson](https://discourse.julialang.org/u/jeff.bezanson)\
**Post date:** [May 28, 2019, 9:39pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/8 "2019-05-28T21:39:36Z")

</div>

> [@foobar\_lv2](#):
>
> 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

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

```julia
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.

---

<div class="post-metadata">

**Author:** ![tkluck](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tkluck/32/15769_2.png) [@tkluck](https://discourse.julialang.org/u/tkluck)\
**Post date:** [May 28, 2019, 10:32pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/9 "2019-05-28T22:32:29Z")

</div>

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

```julia
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
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.

---

<div class="post-metadata">

**Author:** ![Tamas\_Papp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tamas_papp/32/25949_2.png) [@Tamas\_Papp](https://discourse.julialang.org/u/Tamas_Papp)\
**Post date:** [May 29, 2019, 5:08am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/10 "2019-05-29T05:08:13Z")

</div>

> [@tkluck](#):
>
> which should be “true” if we consider `Integer` a set

In math, yes, but not in Julia. Just like `1.0` is not an `Integer`.

(This is orthogonal to the proposal in this topic).

---

<div class="post-metadata">

**Author:** ![dlfivefifty](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/dlfivefifty/32/1959_2.png) [@dlfivefifty](https://discourse.julialang.org/u/dlfivefifty)\
**Post date:** [May 29, 2019, 6:36am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/11 "2019-05-29T06:36:09Z")

</div>

In Julia `y in X` if for any `x` in `X`, `y == x`:

```julia
julia> 1.0 in [1]
true

```

So under this proposal `1.0 in Integer` should return `true`.

---

<div class="post-metadata">

**Author:** ![Tamas\_Papp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tamas_papp/32/25949_2.png) [@Tamas\_Papp](https://discourse.julialang.org/u/Tamas_Papp)\
**Post date:** [May 29, 2019, 6:47am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/12 "2019-05-29T06:47:29Z")

</div>

My understanding is that the original proposal was to implement the semantics of `isa`.

What you are describing is

\exists y : x = y, y \text{ is a } T

---

<div class="post-metadata">

**Author:** ![dlfivefifty](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/dlfivefifty/32/1959_2.png) [@dlfivefifty](https://discourse.julialang.org/u/dlfivefifty)\
**Post date:** [May 29, 2019, 6:50am UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/13 "2019-05-29T06:50:17Z")

</div>

Right, the original proposal is inconsistent with `in`. So if `in` were supported for types you’d want, for example:

```julia
julia> 0.0 in (false,true)
true

julia> 0.0 in Bool # should return true

```

---

<div class="post-metadata">

**Author:** ![foobar\_lv2](https://avatars.discourse-cdn.com/v4/letter/f/ee59a6/32.png) [@foobar\_lv2](https://discourse.julialang.org/u/foobar_lv2)\
**Post date:** [May 29, 2019, 12:51pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/14 "2019-05-29T12:51:57Z")

</div>

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).

---

<div class="post-metadata">

**Author:** ![Tamas\_Papp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tamas_papp/32/25949_2.png) [@Tamas\_Papp](https://discourse.julialang.org/u/Tamas_Papp)\
**Post date:** [May 29, 2019, 1:14pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/15 "2019-05-29T13:14:19Z")

</div>

> [@foobar\_lv2](#):
>
> the julia type system (which is amazingly intuitive on a superficial level and really weird, undocumented

Weird is in the eye of the beholder 😉, but I am curious about the parts you consider undocumented. Perhaps they could be improved.

---

<div class="post-metadata">

**Author:** ![foobar\_lv2](https://avatars.discourse-cdn.com/v4/letter/f/ee59a6/32.png) [@foobar\_lv2](https://discourse.julialang.org/u/foobar_lv2)\
**Post date:** [May 29, 2019, 1:44pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/16 "2019-05-29T13:44:17Z")

</div>

> [@Tamas\_Papp](#):
>
> but I am curious about the parts you consider undocumented

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
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](https://github.com/JuliaLang/julia/issues/31696) 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.

---

<div class="post-metadata">

**Author:** ![StefanKarpinski](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/stefankarpinski/32/24_2.png) [@StefanKarpinski](https://discourse.julialang.org/u/StefanKarpinski)\
**Post date:** [May 29, 2019, 1:54pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/17 "2019-05-29T13:54:29Z")

</div>

It’s almost as if you want a slightly different predicate from `in`…

---

<div class="post-metadata">

**Author:** ![dlfivefifty](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/dlfivefifty/32/1959_2.png) [@dlfivefifty](https://discourse.julialang.org/u/dlfivefifty)\
**Post date:** [May 29, 2019, 2:01pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/18 "2019-05-29T14:01:49Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![StefanKarpinski](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/stefankarpinski/32/24_2.png) [@StefanKarpinski](https://discourse.julialang.org/u/StefanKarpinski)\
**Post date:** [May 29, 2019, 2:07pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/19 "2019-05-29T14:07:21Z")

</div>

> [@foobar\_lv2](#):
>
> 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?

Your confusion confuses me. The [issue](https://github.com/JuliaLang/julia/issues/26108) 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:

- [https://github.com/JeffBezanson/phdthesis/blob/master/main.pdf](https://github.com/JeffBezanson/phdthesis/blob/master/main.pdf)
- [Julia Subtyping: A Rational Reconstruction - INRIA - Institut National de Recherche en Informatique et en Automatique](https://hal-univ-perp.archives-ouvertes.fr/INRIA/hal-01882137v1)

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.

---

<div class="post-metadata">

**Author:** ![StefanKarpinski](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/stefankarpinski/32/24_2.png) [@StefanKarpinski](https://discourse.julialang.org/u/StefanKarpinski)\
**Post date:** [May 29, 2019, 2:08pm UTC](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667/20 "2019-05-29T14:08:35Z")

</div>

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.

[Next page](https://discourse.julialang.org/t/proposal-for-isa-type-syntax/24667.md?page=2)