Stateful assumptions

The last major component of Effes' data types is the concept of stateful assumptions. As the last few posts have discussed, assumptions can be used to declare what Java would call an interface — a set of functions. The Stack[A] assumption I've been using as an example was satisfied ("implemented") by a nickname LinkedList[A], which stood in for a union type of (Nothing | Node[A]). Let's add into the mix another assumption, which says that an item has a size.

The Sizeable assumption just declares that something has a size. We can easily declare that being a Stack[A] implies being Sizeable:

Sizeable -> size :: Int

Stack[A] -> Sizeable st
    size = case head of
        Nothing -> 0
        _ -> 1 + (size pop)

This works, but it's O(N). Let's say we want to make this O(1); in this case, we'll need to maintain the size as a piece of state. Here's how we can do it:

QuickSizeable Stack[A] -> Sizeable st
    s :: Int initially (size it)
    pop -> s' = s - 1
    push _ -> s' = s + 1
    size = s

This defines a new assumption, QuickSizeable, and says that being a QuickSizeable Stack[A] implies being Sizeable (which the Stack[A] already was) with a given implementation. Note that QuickSizable Stack[A] is a composite type. Until now, we've seen composite union types; this is our first composite conjunctive type. In this example, implementation says that:

• When you initially declare a value as being QuickSizeable Stack[A], QuickSizeable will initialize an s :: Int with the size of the Stack[A], however it determines it. At worst, it will be the generic, O(N) implementation.
• When you pop from the Stack[A], the result's s' is one less than the original s. Remember that the apostrophe means "the un-apostrophe'd name within the context of the result."
• When you push to the Stack[A], the result's s' is one more than the original.
• The QuickSizeable Stack[A]'s size method simply returns s

The field s :: Int doesn't belong to either QuickSizeable or Stack[A]; it belongs to the composite type QuickSizeable Stack[A]. This is significant: composite types are "real" types that can define new state or new methods. (We've seen this before, when the LinkedList[A] nickname for the union type Nothing | Node[A] defined implementations of Stack[A] methods.)

This all makes sense, but there's a function resolution problem. Consider the following:

a :: Stack[Foo] = createSomeStack()
b :: QuickSizeable Stack[Foo] = a
c :: Stack[Foo] = b
a.size
b.size
c.size

What happens in each of the three size invocations? a.size is easy: the only method available is the O(N) version that any Stack[A] gets by the first bit of code, above. b.size is also easy: use the O(1) version defined by QuickSizeable Stack[A]. For the third version, we'd like to use the O(1) version — it's more efficient and intuitively feels like polymorphic overriding in OO languages — but we need a rule to allow this. The function resolution rules proposed in the last post are ambiguous.

The solution I have in mind, though I haven't formalized it yet, is that if a type A implies that all As are also B, then A's methods override B's. In this case, QuickSizeable Stack[A] -> Sizeable means that all QuickSizeable Stack[A]s are also Sizeable, so the implementation of size in QuickSizeable Stack[A] overrides the implementation that "belongs" to Stack[A], which we defined above.

What if we now define another sizer:

StupidSizer Stack[A] -> Sizeable st
    size = 1234

What happens with a type StupidSizer QuickSizeble Stack[A]? Does the size method act like a StupidSizer Stack[A] or a QuickSizeable Stack[A]? The call is ambiguous, and is thus disallowed. The type itself is allowed, and you can invoke any unambiguous methods on it; but attempting to invoke ambiguous methods, such as size in this case, will result in a compiler error. To fix it, you must first cast the object to a type with an unambiguous size.

Hm, I think I can unify some of the concepts in the last few posts. Wait for it...