The issue of implicit coercions in Whiley is proving to be a particularly thorny issue. The following motivates why (I think) coercions make sense:
real f(int x, real y):
return x + y
real g(int x, int y):
return f(x,y)
I believe the above should compile without error. However, this requires an implicit coercion from int to real in several places. Some statically typed programming languages (notably ML) simply don’t perform any implicit coercions. Instead, they require explicit coercions in the form of type casts. Under this model, the above code would be:
real f(int x, real y):
return real(x) + y
real g(int x, int y):
return f(x,real(y))
To me, this seems rather cumbersom and, when it’s clear from the context, I want the compiler to do this for me.
So, what coercions could we support in Whiley? Here’s a taster:
int–>real{int x, int y}–>{int y}[int]–>{int}{int->int}–>{int,int}[string]–>{int->string}
Unfortunately, whilst this looks all good on the surface, there are some tricky cases. Here’s one example:
define Rec1 as { int x, real y }
define Rec2 as { real x, int y }
define Rec12 as Rec1 | Rec2
int f(Rec12 r):
if r is Rec1:
return r.x
else:
return r.y
int test():
z = {x: 1, y: 1} // z has type {int x, int y}
return f(z)
The problem here is that we cannot determine whether to coerce z to Rec1 or Rec2. I guess we should report an ambiguous coercion error. Which immediately raises the question of how, in the general case, I detect this.
I think the problem is the union in general, not implicit coercions in particular. For instance, suppose you had:
define Rec1 as { int x, int y }
define Rec2 as { int x, int y }
...
z = {x: 1, y: 2}
...
and the rest as in your post. What should happen? (IMO test should return 1)
Hey,
In fact, what happens is that you get a syntax error. Given your definitions then the compiler correctly reasons that Rec1|Rec2 == Rec1. Therefore, it reasons that the statement return r.y is dead-code, and reports a syntax error!
D
Okay, I guess that works. Anyways, in your original example, the behavior should be similar: the code tries coercing {int x, int y} to Rec1, succeeds, and therefore takes the return r.x branch.
Also, I just realized you have a typo in the post: shouldn’t return g(x,y) be return f(x,y)?
Oh yeah … doh!!
Fixed
(thanks)
Right, so it could do this. But, it could equally choose Rec2 … and generally compilers report errors on this kind of ambiguity.
Also, using something like order of declaration in the source file is not really a solution for me, since I throw away all that information (and keeping it would be really awkward).
Ah, I think I see our point of disagreement. I think of types as contracts aiding optimization of a loosely and dynamically-typed language, whereas you expect types to mimic the behavior of static types fairly closely. So when I see the type signature “int f(Rec12 r)”, I think of it as a function taking some object that can eventually be converted into a Rec12 and returning some object eventually convertible to an int, whereas you think of it as taking an actual Rec12 and returning an actual int.
So in my view, {x: 1, y: 1} is clearly an instance of Rec12, so the contract is upheld; then all the types are erased, and the if-else establishes a clear preference of Rec1 over Rec2.
From your view, it would involve returning a closure that only attempted the “real” coercion from int to real once it knew whether a value of Rec1 or Rec2 was desired from the union.
In Javascript-ish pseudocode: (I hope the blog doesn’t eat it)
union = [{int x, real y}, {real x, int y}, ...]
function coerce(obj, union) {
coercable = false
for(type in union)
if(coerce(obj,type))
coercable = true
if(!coercable)
error "invalid union coercion"
else
return function(realtype) {
return coerce(obj,realtype) || error "wrong type of union"
}
}
Yes, exactly! But, that’s not the route I want to go down. Whiley is strictly a statically typed language, so I need to disambiguate this case somehow …
[...] something of a headache as, in the context of structural subtyping, they’re quite tricky. This post provides some insight into the problem, as does this [...]