Open Veedrac opened 8 years ago
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.
Fair enough about Object+
; I've replaced it with a wordier alternative. Having proper intersection types would be really nice.
I would love to see type intersection too. :+1:
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
Wish to support intersection types.
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
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
).
Set
's&
, as an example, is such thatis
which is the type of the LHS, but surely it should really be
This is possible to implement as
The
typeof(Intersect(T, U).get())
stuff isn't the most obvious (I'd much ratherT & U
), but other than that the code works great.Would this be useful?