Types are ignored for function argument in generic

[Castux]

local function apply<A,B>(func: (function(A): B), x: A): B
    return func(x)
end

local function apply_wrong<A,B>(func: (function(A): B), x: B): A
    return func(x)
end

local function apply_wrong2<A,B>(func: (function(A): B), x: B): B
    return func(x)
end

local function apply_wrong3<A,B>(func: (function(A): B), x: A): A
    return func(x)
end

print(apply(math.sqrt, 5))
print(apply_wrong(math.sqrt, 5))
print(apply_wrong2(math.sqrt, 5))
print(apply_wrong3(math.sqrt, 5))

Although the four functions generate the expected code, the last three should not pass type checking. These are the smallest examples I could find that illustrate the bug, when I was writing a map function and realized the return types were ignored.

[hishamhm]

Bivariant functions strike again -- Teal is lax about this because it does not check subtype relationships between generic types. For the latter cases, those applications could be valid depending on the relationships between A and B (whether A = B, A <: B or B <: A). So the function declarations themselves are accepted, and in the latter three cases A and B are inferred to be unified (because you're matching them to each other, passing a B where an A is expected or vice-versa).

By being unified, this means that if you call those functions with the same types for A and B, they'll work — which is precisely what happens with math.sqrt, which takes a number and returns a number. Both A and B are number, and all is happy.

Now let's try with different types:

local function apply<A,B>(func: (function(A): B), x: A): B
   return func(x)
end

local function apply_wrong<A,B>(func: (function(A): B), x: B): A
   return func(x)
end

local function apply_wrong2<A,B>(func: (function(A): B), x: B): B
   return func(x)
end

local function apply_wrong3<A,B>(func: (function(A): B), x: A): A
   return func(x)
end

-- let's make a 1-arity function with different types for input and output
local function f(s: string): number
   return (string.byte(s))
end

-- let's try to use the facts that A and B need to be different in practice:
-- (the `+ 1` is to force the return value to be used in a number context)
print(apply(f, "hello") + 1)
print(apply_wrong(f, "hello") + 1)
print(apply_wrong2(f, "hello") + 1)
print(apply_wrong3(f, "hello") + 1)

We get:

========================================
4 errors:
650.tl:25:22: argument 2: got string "hello", expected number
650.tl:25:31: cannot use operator '+' for types string and integer
650.tl:26:23: argument 2: got string "hello", expected number
650.tl:27:32: cannot use operator '+' for types string and integer

All three "wrong" lines now fail. Though notice that apply_wrong failed on both the argument and return type, apply_wrong2 on the argument, and apply_wrong3 on the return type. In particular, apply_wrong and apply_wrong3 do produce a string without an error, because function calls are checked based on the function signatures only, and not on the contents of the actual function. The fact that A and B were unified during the checking of the function body is not propagated (and we don't because A = B might be an oversimplification; A <: B or B <: A might suffice (or be required!), and the inference algorithm does not have a constraint solver to determine it).

These are known limitations of the checking algorithm made for simplicity. The shortcomings do show up the more you try to exercise the type checker as a functional programming language (we're light years away from the size, completeness or complexity of a Haskell!), but as shown in my examples above, the checks tend to work well enough when generic functions are used in practice.

[Castux]

Thanks a lot for the comprehensive answer. This is fascinating stuff and turned out to be a lot more complex than I expected, which in a way, was to be expected :)