Rtc's polymorphic methods don't quite work

[jtoman]

Consider the following example:

typesig("my_push<t>: (Array<t>, t) -> Array<t>")
def my_push(arr, m)
   arr.push(m)
end

The following perfectly safe invocation will fail with a type error:

my_push([1,2,3], "foo")

The Array<Fixnum> as the first argument will cause t = Fixnum which is incompatible with the second argument's type of String. Similarly, consider the following:

typesig("my_push2<t>: (t, Array<t>) -> Array<t>")
def my_push2(m, arr)
   arr.push(m)
end

In the current implementation will fail on the following invocation: my_push2("foo", [1,2,"bar"]) because Rtc chooses t to be equivalent to String despite the correct choice being String or Fixnum. Clearly then, the implementation should choose the most general type, but the difficulty arises in choosing the most general type without sacrificing type safety. For instance, in the first example, you could argue that t should be String or Fixnum but this requires "blindly" unioning every type that appears in a position corresponding to the same type parameter, which would allow real errors through. As an aside, the first example could be correctly expressed in the current type system with:

typesig("my_push<t,u>: (Array<t>, u) -> Array<t or u>")

but I feel this may be too burdensome on the average programmer, and would require the programmer to reason unduly about the flow of values through the program (for example, if the programmer knew that the my_push function would always be called with an array that had both Strings and Fixnums then the original type signature in the first example could be used).

[jtoman]

It should also be noted that the following will also work:

my_push([1,2,3].rtc_annotate("Array<String or Fixnum>"), "foo")

Maybe telling programmers to be judicious with their annotations is the best choice?

[jtoman]

My initial assertion about annotations is probably not correct. Consider the following (contrived) example:

typesig("foo<t>: (t, t, Boolean) { t -> t } -> t")
def foo(a,b,boolean)
   yield(boolean ? a : b)
end
#invocation
foo("1", 4, true) { |arg| if arg.instance_of?(String) then (Integer arg) else arg.to_s end }

For the above to work with annotations, we'd have to expand annotations to apply not only to parametrically polymorphic container types (which is all that is currently supported) but to allow things like:

4.rtc_annotate("Fixnum or String")

The problems with this need not be stated.

[jtoman]

Ultimately, it may be better to have the programmer be more careful with their type signatures (not annotations). I can't think of a way for this to work without sacrificing type safety or sane semantics. @jeffrey-s-foster may want to chime in on this though.

[jtoman]

To elaborate, keeping the current "no automatic union" policy in place yields a more expressive type system at the expense of placing a burden on the programmer. For instance, if we adopted the "auto-union" rule, than it would be impossible to write a polymorphic type-signature for a 2-ary method that required both arguments to be exact same type. Keeping the current method then provides the most flexibility and I think we should keep it.

[jtoman]

The only downside to the above is that it requires the programmer to be aware of our unique system of handling type parameters for polymorphic classes.

[jtoman]

I think a lot of the issues raised by this issue can be solved using function instantiation as mentioned in #44. In addition, under the new solving scheme, the code presented in the op:

my_push([1,2,3], "foo")

would be accepted. I'm going to revisit the issues raised by this ticket and see if this issue is still relevant.