30 Jun 2016, 10:27

[Reddit] Intersection Types

Snipped and backdated from a Reddit comment of mine.

Using intersection with primitive types not make any sense since there is no common type.
(In type theory, this is called the bottom type.)

Now, an example of where intersection types would actually be useful is with struct or record types that you can combine togeather (i.e. “I want a type that has all properties in type A and all properties in type B”.)
This allows for sort of strongly typed duck typing so to speak. (Aside: you could also apply this same concept with OOP interfaces or something like Haskell’s typeclasses too.)

Elm’s “extensible records” gives you an idea of how this would work. It wouldn’t call these actual intersection types, so I’ve changed the syntax and semantics a bit for demo purposes.

So let’s say you’re writing a game in said modified Elm syntax and define the following record types:

type Positioned = { x: Float, y: Float }

type Named = { name: String }

type Moving = { velocity: Float, angle: Float }

And let’s say you define some entities as:

sword : Named & { damage: Int }
sword =
  { name = "Excalibur"
  , damage = 9001

player : Named & Positioned & Moving
player =
  { name = "Sir Lancelot",
  , x = 0
  , y = 0
  , velocity = 42
  , angle = degrees 30

In other words…

The type of sword is the intersection of:

  • record type Named
  • (and) an anonymous record type of { damage: Int }.

The type of player is the intersection of:

  • record type Named
  • (and) record type Moving
  • (and) record type Positioned.

If we combine the intersections, the “evaluated” or “absolute” types could be written as:

sword : { name: String, damage: Int }

player : { name: String
         , x: Float
         , y: Float
         , velocity: Float
         , angle: Float

Hopefully, this contrived example illustrates how intersection types could prove to be useful…