Subtyping and function resolution (at last!)

I've been putting off for too long my ideas for subtyping and function resolution, because I've wanted to get things juuust right. Instead, I'm going to just outline my ideas and move on, because I want to start coming up with a grammar and writing some actual Effes. I've been dragging my feet for too long!

So, subtypes first, then function resolution.

Type hierarchy in Effes

• A is a subtype of B if there is a "class-based" implementation that says B is A. For instance, if we declare that Stack[A] is Sizeable where..., then Stack[A] is a subtype of Sizeable
• A is a subtype of B if A is a conjunction type whose parts include B. For instance, FourWheeled Vehicle is a subtype of FourWheeled and Vehicle.
• Union types act as a single unit and don't establish any subtype relationships with their components. So:
  
  • Cat | Mouse isn't a subtype of Cat or Mouse.
  • Neither Cat nor Mouse are a subtype of Cat | Mouse.
  • However, since Cat | Mouse is a single unit, Cute ( Cat | Mouse) is one of its subtypes.
• Any type is of course a subtype of itself.
• Without getting into too much details, subtypes work with the components of conjunction types, not just the full conjunction. For instance, if Box is a subtype of Container, then Big Box is a subtype of Big Container.
  

I think for generic types, I'll say that Box[Gum] is a subtype of Container[Candy] if Box is a subtype of Container and Gum is a subtype of Candy. This is extremely up for grabs; it can wreak havoc on collections, but that's because they're mutable. Effes has a much stricter set of restrictions on mutability, which I think eliminate the problem.

Function resolution

In a nutshell: functions are bound to an object according to the most specific type information known about it at compile time. (That last bit is important!) For each function f, find the most specific subtype that defines f, and bind that version of f to that object.

-- Define some types
data Animal; Ascii; Cat; Dog
Dog is Animal
Cat is Animal

-- Define some methods
speak(a:Animal) : String = "Zzzz" -- all animals sleep
speak(c:Cat) : String = "Purr"
speak(c:Ascii Cat) : String = ">^-^<"

-- Invoke them
speak(Cat) -- Purr
speak(Dog) -- Zzzz
speak(Ascii Cat) -- >^-^< 
peak(Dog Cat) -- compile-time error
speak(Ascii Animal Cat) -- >^-^<

The first three of the function invocations should be pretty straightforward. The fourth case is a compile-time error because Dog Cat is "equally subtype-y" to both Dog and Cat, so the compiler doesn't know which method to use. (Maybe I'll provide some overriding behavior in the future, but for now I'm just going to disallow it altogether.) The last one is an edge case — hey, every language has to have 'em! The reason is that type conjunctions are commutative and associative: (A B) C is the same as B (C A). So, even though Ascii Animal Cat doesn't look like anything meaningful, it can also be expressed as (Ascii Cat) Animal, which is a subtype of both Ascii Cat and Animal (as well as of Ascii and Cat, but that's not important for this example). Since Ascii Cat is itself a subtype of Animal, it is the most specific subtype and thus supplies the function. One last thing, which is the bit about binding at compile time. Let's tweak the menagerie a bit:

data Ascii; Hungry; Cat

speak(c:Ascii Cat) : String = ">^-^<"
speak(c:Hungry Cat) : String = "Meow!!" -- at 5am...
speak(c:Hungry Ascii Cat) : "4d 65 6f 77 21 2`"

getKitty() : Cat = Ascii Cat
c1 = getKitty() c2 = Hungry c1

In this example, c1 has a compile-time type of Cat and a runtime type of Ascii Cat. However, where the object was created (namely, the only expression in the body of getKitty), it had a compile-time type of Ascii Cat, so speak(c1) is bound to speak(c:Ascii Cat) and would result in ">^-^<". The last line is where things get potentially unfamiliar. Even though c1 has a runtime type of Ascii Cat, it has a compile-time type of just Cat, so Hungry c1 has a compile-time type of Hungry Cat, not Hungry Ascii Cat. This means speak(c2) would result in "Meow!!".

This feels a bit weird at first blush: it's a blend of polymorphism and... something that feels un-polymorphic. I may change my mind, but the reason I like it is that you can know, easily and deterministically, how functions will be bound just by looking at where an object is created. That is, you don't have to reason about where the object came from and what its runtime type might be; you just look at what it is, and there you go.

The basic rule is that you can't know exactly how an object will behave unless you create it.