Type Subtraction

[baseballlover723]

Feature Request

It would be nice to be able to specify a partial type restriction in a convenient way. I was looking through #13454 and noticed

b = [] of typeof(begin
      x = Enumerable.element_type(self)
      x.is_a?(U) ? raise("") : x
    end)

which was being used to do some type subtraction. Notably, returning an array without a given type in it (but keeping the other types). This got me thinking, why isn't there an inbuilt type subtraction? It's easy enough to merge types together in unions, like Int32 | String | Char, but there's not simple way to go in the reverse. Ideally it would be nice to be able to do something like (Int32 | String | Char) - String # => Int32 | Char. Sure you could use .as(Int32 | Char), but this only works if you know what the type is, and doesn't work for things like generics.

I can imagine this most being useful in generic methods that in some way reduce the type set. For instance

module Enumerable(T)
  def partition(type : U.class) : {Array(U), Array(T - U)} forall U
    a = [] of U
    b = [] of T - U
    each do |e|
      e.is_a?(U) ? a.push(e) : b.push(e)
    end
    {a, b}
  end
end

looks a lot more intuitive and has clearer type restrictions then

module Enumerable(T)
  def partition(type : U.class) forall U
    a = [] of U
    b = [] of typeof(begin
      x = Enumerable.element_type(self)
      x.is_a?(U) ? raise("") : x
    end)
    each do |e|
      e.is_a?(U) ? a.push(e) : b.push(e)
    end
    {a, b}
  end
end

This seems like it would be easily to implement, since it's just Type Unions, but in reverse. I tried to see if I could emulate this in a macro, but found it difficult to actually get type information of variables and such to operate on in the macro.

I propose adding a new type operator - that lets us do Type Subtraction.

[straight-shoota]

This is definitely a valuable use case. There's a similar issue about the related case of type intersection: #2404

Such operations in the type grammar can only be implemented directly in the compiler. Implementing that shouldn't be too hard (probably). But it still requires some effort and so far nobody has picked this up yet to get into the details. The first step would be to specify concrete use cases and expected behaviour.

[HertzDevil]

The problem here is that subtraction doesn't work on a hierarchy:

class A
end

class B < A
end

class C < A
end

# `A` is not exhaustible, so this doesn't return `C`
{{ A - B }} # => A

If the types themselves need to encode this information, then we would have to also define the correct subtyping relationships, how they merge or intersect with other types etc. This is the same with intersection types (note that you could express A - B as A & ~B).

Maybe Class#-(Class) or some other kind of shorthand is sufficient for the typeof case.

[HertzDevil]

For example:

class Class
  macro &(type1, type2)
    %var = uninitialized {{ type1 }}
    if %var.is_a?({{ type2 }})
      %var
    else
      while true
      end
    end
  end

  macro -(type1, type2)
    %var = uninitialized {{ type1 }}
    if %var.is_a?({{ type2 }})
      while true
      end
    else
      %var
    end
  end
end

module Enumerable(T)
  def select2(type : U.class) forall U
    arr = [] of typeof(Class.&(T, U))
    each { |e| arr << e if e.is_a?(U) }
    arr
  end

  def reject2(type : U.class) forall U
    arr = [] of typeof(Class.-(T, U))
    each { |e| arr << e unless e.is_a?(U) }
    arr
  end
end

x = [1, 2, "a", 3, "b", "c"].select2(Int32)
x       # => [1, 2, 3]
x.class # => Array(Int32)

x = [1, 2, "a", 3, "b", "c"].reject2(Int32)
x       # => ["a", "b", "c"]
x.class # => Array(String)