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,foo
is aBalloon
, andpop foo
returns aPoppedBalloon
- It's the union of
(Nothing | Node[A])
, which satisfiesStack[A]
, meaning thatpop 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:
- 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.