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.
Sizeableassumption just declares that something has a size. We can easily declare that being a
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
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
QuickSizeablewill initialize an
s :: Intwith 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.
sizemethod simply returns
s :: Intdoesn't belong to either
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
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
a.sizeis easy: the only method available is the O(N) version that any
Stack[A]gets by the first bit of code, above.
b.sizeis 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] -> Sizeablemeans that all
QuickSizeable Stack[A]s are also
Sizeable, so the implementation of
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
sizemethod 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
sizein this case, will result in a compiler error. To fix it, you must first cast the object to a type with an unambiguous
Hm, I think I can unify some of the concepts in the last few posts. Wait for it...