I was prompted by these discussions:
- RFC: Language Support for Traits — Yay or Nay?
- … in particular, this comment about intersection types
and also this excerpt of Jeff Bezanson’s 2017 JuliaCon talk, where he quotes some researchers saying about intersection and complement types:
“Well, look, your subtyping is already so complicated, you might as well add these things…”
and it seemed like a fascinating task to make a proof of concept:
This is a “toy” type system which
seems to allow a form of abstract multiple inheritance,
@stt begin abstract type Smart end abstract type Organic end struct Computer ⊆ Smart end struct Fruit ⊆ Organic end struct Brain ⊆ Smart ∩ Organic end # intersection type think(x ∈ Smart) = "$(x.value) is thinking..." think(x ∈ !Smart) = "$(x.value) cannot think!" # complement type end
julia> Brain ⊆ Smart && Brain ⊆ Organic true julia> think(Computer("Deepthought")) "Deepthought is thinking..." julia> think(Fruit(:Quince)) "Quince cannot think!"
and appears to work with parametric types (to the extent of basic testing).
@stt begin abstract type Machine[In,Out] end abstract type Alive end struct Box[T] end struct Kitten ⊆ Alive end struct Elf[T] ⊆ Alive ∩ Machine[T,Box[T]] end end
julia> Elf ⊆ Alive true julia> Elf[Kitten] ⊆ @stt Machine[T,Box[T]] where T ⊆ Alive true
But most interestingly, it has a trait-like expressiveness which allows you to “add” supertypes to types you don’t own. For example, if someone else’s package contained
@stt begin abstract type HasDuckBill end abstract type LaysEggs end abstract type Mammal end abstract type Bird end struct Platypus ⊆ HasDuckBill ∩ LaysEggs ∩ Mammal end struct CanadianGoose ⊆ HasDuckBill ∩ LaysEggs ∩ Bird end foo(x ∈ HasDuckBill ∩ LaysEggs) = "Platypus or Goose" end
and you wanted to introduce a type
Alive such that
Mammal ⊆ Alive and
Bird ⊆ Alive, you could do so by declaring
@stt abstract type Dead ⊆ !(Mammal ∪ Bird) end Alive = !Dead
julia> Platypus ⊆ Alive true
Overall, fully set-theoretic types seem pretty neat. Although I don’t know whether there lurk inconsistencies (either in theory or implementation). I’d be interested to know of any you find!
Also, allowing unions, intersections, complements and parameters seems fairly complex. Though what are abstract types but ways to conveniently express sets of concrete types? I’m not sure what the complexity–expressiveness balance is.
(If you’re curious about details, I invite you to look at the package tests, which I’ve tried to make fairly approachable.)