Some functions could perform type intersection

[Veedrac]

Set's &, as an example, is such that

    typeof(Set.new([1, "a"]) & Set.new(["a", false]))

is

    Set(Int32 | String)

which is the type of the LHS, but surely it should really be

    Set(String)

This is possible to implement as

    class Intersect(T, U)
        def self.get()
            value = uninitialized T
            return value if value.is_a?(U)
            raise Exception.new
        end
    end

    def intersect(lhs : Set(T), rhs : Set(U))
        set = Set(typeof(Intersect(T, U).get())).new
        lhs.each do |value|
            if value.is_a?(U) && rhs.includes?(value)
                set.add value
            end
        end
        set
    end

The typeof(Intersect(T, U).get()) stuff isn't the most obvious (I'd much rather T & U), but other than that the code works great.

Would this be useful?

[asterite]

Intersection types are a nice idea. Some days ago @bcardiff suggested to me that - and & should maybe be added to the type grammar. For example Enumerable#compact could be defined to return T - Nil. And another use case for intersections is this:

# We want something that's an IO, but we also want 
# T as a free variable to get the real type
def foo(x : T & IO)
  # do something with T
end

Using Object+ to accomplish that, as commented here won't work in the future, but if we add intersection types it could be done.

[Veedrac]

Fair enough about Object+; I've replaced it with a wordier alternative. Having proper intersection types would be really nice.

[waterlink]

I would love to see type intersection too. 👍

I can only imagine how useful it will be.

Am 03.04.2016 um 6:05 PM schrieb Joshua Landau notifications@github.com:

Fair enough about Object+; I've replaced it with a wordier alternative. Having proper intersection types would be really nice.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub

[ethe]

Wish to support intersection types.

[HertzDevil]

This is possible to implement as ...

The intersection defined this way isn't commutative yet, not even up to equivalent types. Some examples:

# covariant Tuple instances
typeof(Intersect({Int32}, {Int32 | Char}).get) # => Tuple(Int32)
typeof(Intersect({Int32 | Char}, {Int32}).get) # => NoReturn

# generic module instances
typeof(Intersect(Indexable(Int32), Enumerable(Int32)).get) # => Indexable(Int32)
typeof(Intersect(Enumerable(Int32), Indexable(Int32)).get) # => NoReturn

# metaclasses between module and including class
typeof(Intersect(File.class, IO.class).get) # => Class
typeof(Intersect(IO.class, File.class).get) # => NoReturn

# metaclasses between superclass and subclass
typeof(Intersect(File.class, IO::FileDescriptor.class).get) # => Class
typeof(Intersect(IO::FileDescriptor.class, File.class).get) # => NoReturn

# nil and void
typeof(Intersect(Nil, Void).get) # => Nil
typeof(Intersect(Void, Nil).get) # => NoReturn

If Intersect becomes a built-in type operator it should definitely be commutative in all arguments; the same goes for Class#&, which shall be defined in terms of this typeof precisely, similar to #|. (The union operator is commutative up to equivalent types, but not up to strictly equal types.) For the compiler, this means the following must be true for any a : Crystal::Type and b : Crystal::Type:

c = a.filter_by(b)
d = b.filter_by(a)
if c && d
  c.implements?(d) && d.implements?(c) # C <= D && C >= D
else
  c.nil? && d.nil? # both filtered types are NoReturn
end

Doing so would also impact flow typing; for example, this might be possible in the future:

x = {1 || 'a'}
if x.is_a?({Int32})
  typeof(x) # => Tuple(Int32)
else
  typeof(x) # => Tuple(Char)
end

[HertzDevil]

Defining Class#& and the Intersect operator using the current semantics is the easiest. If we add & to AST node restrictions we already face a problem: for what types A, B, C are the following pairs of defs redefinitions?

def foo(x : (A & B) | C); end
def foo(x : (A | C) & (B | C)); end

def bar(x : (A | B) & C); end
def bar(x : (A & C) | (B & C)); end

It would be good if distributivity holds for any AST node, but I haven't investigated that far yet. Irreducible intersection types are even harder to implement, because if those types are equivalent then it might be preferable to always normalize them to CNFs or DNFs (not doing so would create a situation similar to NamedTuple where T <= U && U <= T does not imply T == U).