# Type-checking function calls with functional subtyping

I'm relatively new to the topic. Suppose that you want to type-check an expression of the form f(a), i.e. a function call. Assuming that all the declarations are provided explicit types, I believe that a simple type-checker would behave as follows:

1. Given the environment, compute the types of a and f;
2. Check that the type of f be of the form $$T\to U$$;
3. Check that the type of a be a subtype of $$T$$;
4. Return $$U$$ if needed.

But now suppose that, for all $$U$$, the following subtyping relation holds:

$$[U]<:\text{Int}\to U$$

where $$[\thinspace\cdot\thinspace]$$ denotes the array-type, and that computation (1) finds the types of a and f to be resp. $$T$$ and $$[U]$$ for some $$T$$, $$U$$. Now, $$[U]$$ is not a function-type, so check (2) fails. I'm assuming that the definition of $$<:$$ is completely independent of the type-checker, so we can't just hard-code a check (2.1) for array-types, too. We could instead check that $$[U]$$ be a subtype of a least acceptable function-type $$T\to\top$$, where $$\top$$ denotes the universe-type, but what if function-types are invariant according to $$<:$$?

I suspect that what I really need is a form of type-inference, rather than type-checking, even though the types of f and a are completely determined, which doesn't make sense to me. What would be the correct approach, here?

• How are $\mathrm{Int}$ and $T$ supposed to fit together in your example? Also, is there some sort of background motivation for your (strange) example of subtyping? In these sorts of type systems subtyping tends to be structural, i.e., if $X$ is a subtype of $Y \to Z$ then $X = X_1 \to X_2$ for some $X_1$ and $X_2$. – Andrej Bauer Sep 21 at 18:49
• The check should pass when $T<:\text{Int}$,e.g. $T=\text{Char}$ in C. Also, yes, afaik e.g. in Scala you can pass a $[U]$ to a function that receives a $\text{Int}\to U$ – giofrida Sep 21 at 18:58
• The details matter. Can you point to the relevant bit of Scala? But to start answering your question, it would be good to have more context about what you're doing. You are not talking about structural types, which means that reasonable properties of subtyping have gone out of the window. What precisely would you like to achieve? – Andrej Bauer Sep 21 at 19:06
• What do you mean by relevant bit, a code fragment? As for the other question: given a suitable internal representation of $<:$, I wish to implement a type-checker for a simple language with functions and function calls, whatever the actual definition of $<:$. But now your comment makes me think that it wouldn't be easy or even possible without at least some insight about $<:$. For instance, some authors introduce an inference rule solely dedicated to functional variance. – giofrida Sep 21 at 19:24
• @giofrida do you want to type check array indexing? Because there is a hidden function there e.g. Array<U>.get: Int -> U ofc Arrays are generic types which makes it a bit harder. Or do I misunderstand something? – plshelp Sep 22 at 2:46

Presumably, what Scala does (since you mentioned it) is relax your step 2. It is incorrect to check that the type of $$f$$ is merely 'of the form' $$T → U$$ because it is applied. Rather, one should check that the type of $$f$$ is known to be a subtype of some $$T → U$$.
$$[U] <: \mathsf{Int} → U$$
• Thank you. I ended up implementing a "wildcard" type $?$ and requiring that $<:$ satisfies a certain regularity property, so I can easily recover $T$, $U$ from the computed type and a "prototype" $?\to ?$. I still don't know if it'll work, but for now it's the best I could come up with. – giofrida Sep 25 at 7:55