Tuesday, June 11, 2013

Nicknames, function resolution and edge cases

In my first post about the Effes type system, lied a bit in my last post when I said that nicknames are just typing shortcuts. They also provide function resolution rules, in case a data type satisfies assumptions with conflicting methods. For instance, let's say we had the following type and assumption:

data PoppedBalloon (color :: Color) -- or something
Balloon -> :: PoppedBalloon

In the last post, I introduced a Node[A] that satisfies the Stack[A] assumption from a couple posts ago. Now, I also want to say that a Node[A] and Nothing both satisfy the Balloon assumption. Easy enough:

Node[A] -> Balloon st pop _ = PoppedBalloon(Red)
Nothing -> Balloon st pop _ = PoppedBalloon(GhostGray)

This is obviously a strained example, but besides the fact that these implementations are useless, here's the real problem:

foo :: (Nothing | Node[A]) = optionallyGetFoo()
bar = pop foo -- what is bar's type?

In the first line, we try to get a Node[A], but the method's signature tells us we might not be able to (maybe a lookup fails, for instance). If it fails, the method will return a Nothing, and so our foo has to be typed to accept either result value. So far, so good. The question is, what's bar? We can think of foo in two ways:

  • It's either a Node[A], which satisfies Balloon, or it's a Nothing, which also satisfies Balloon. Either way, foo is a Balloon, and pop foo returns a PoppedBalloon
  • It's the union of (Nothing | Node[A]), which satisfies Stack[A], meaning that pop foo returns a (Nothing | Node[A])

I haven't yet nailed down how I want this to work, but my current thinking is that if there is ambiguity, the programmer will have to be explicit about the intent. Something like:

bar1 = pop (foo :: Stack[A]) -- bar1::Stack[A]
bar2 = pop (foo::LinkedList[A]) -- bar2::LinkedList[A]

This has a couple interesting edge cases. Firstly, what happens if a union type (such as LinkedList[A] satisfies an assumption, and one (but not both) of its composite types defines a method that conflicts. For instance, Stack[A] defines a method head. What if you also provided a function on Node[A] alone that conflicts with this? In fact, that method already exists! When we defined the Node[A] data type as:

data Node[A] = head :: A, next :: Nothing | Node[A]

the compiler automatically created two functions:

head Node[A] :: A
next Node[A] :: Nothing | Node[A]

A type foo :: Node[A] cause a conflict with Stack[A], because (as mentioned in the previous post) a Node[A] is a subtype of Nothing | Node[A], which satisfies Stack[A]. The solution here is that Effes will take the most specific function it can; in this case, the one declared to take only a Node[A], that is, the auto-generated getter.

Okay, so foo :: Node[A] means that head foo invokes the getter, while foo :: Nothing | Node[A] means that head foo invokes the Stack[A] method. But what if we additionally define a method that takes Nothing:

head (_ :: Nothing) :: Int  = -1

Now we're back to an ambiguity in the case of foo :: Nothing | Node[A]. The compiler can say that head foo invokes the Stack[A] version of head and thus return a Possible[A]; or that it will switch at runtime between two specific functions, head Node[A] :: A and head Nothing :: Int, and thus return a A | Int. Again, the rule is to favor the specific calls; the compiler will chose the second of those two options.

Finally, let's say we define a method that takes a union type:

head (a :: Nothing | Node[A]) :: (String | Float) =
    case a of
        Nothing -> "I am a fish"
        Node[A] -> 3.14

Now what does head foo return? In this case, it invokes that new method, and thus returns a type of String | Float. This seems a bit inconsistent — aren't I now picking a less specific type? Yes, but it's one that is otherwise impossible to name, so this is the only way I have to invoke it! Whereas before, I could "cast" the Nothing | Node[A] to a LinkedList[A] or even a Stack[A], here I have nothing other than Nothing | Node[A] to cast it to in order to tell the resolution engine to pick this new (and really useless) method. If I want to invoke the two specific methods, I have to manually invoke case:

barUseless = head foo -- bar :: String | Float
barSlightlyLessUseless = case foo of
    Nothing -> head foo -- :: Int
    Node[A] -> head foo -- :: A
-- barSlightlyLessUseless :: Int | A

This is admittedly awkward, but I think it's an edge case that won't come into play very often. I hope.

In summary, functions are resolved in this order:

  1. union types
  2. data types
  3. nicknames
  4. assumptions

That last one may strike you as a bit odd. After an assumption is just a contract, not a specific implementation, right? So far, yes; but in the next post, I'll talk about stateful assumptions that do have implementations.

No comments:

Post a Comment

Note: Only a member of this blog may post a comment.