Traits via set-theoretic types: proof of concept

Internals & Design
1

I was prompted by these discussions:

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

et voilà:

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

18 Likes
2

And here I thought I already memorized all content Jeff put out over the years about the type system - clearly, I am mistaken!

The one caveat I can imagine is that this is (sadly) still just half of the picture - and the other half is the nastiness with protocols Jeff mentions right after the linked section from that talk… basically associating an abstract type with what’s actually required from subtypes. Still, what a wonderful proof of concept, wish I could :heart: it more than once :slight_smile:

3 Likes
3

Looks very cool! By the way, here’s an issue where Intersection types are discussed a bit: Dispatch on a type being anywhere in a signature · Issue #39878 · JuliaLang/julia · GitHub

3 Likes