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 satisfiesBalloon, or it's aNothing, which also satisfiesBalloon. Either way,foois aBalloon, andpop fooreturns aPoppedBalloon - It's the union of
(Nothing | Node[A]), which satisfiesStack[A], meaning thatpop fooreturns 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.14Now 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 | AThis 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:
- union types
- data types
- nicknames
- 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.