Traits via set-theoretic types: proof of concept

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:

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
``````

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

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 it more than once

3 Likes

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