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?

  • $\begingroup$ 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$. $\endgroup$ – Andrej Bauer Sep 21 '20 at 18:49
  • $\begingroup$ 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$ $\endgroup$ – giofrida Sep 21 '20 at 18:58
  • $\begingroup$ 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? $\endgroup$ – Andrej Bauer Sep 21 '20 at 19:06
  • $\begingroup$ 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. $\endgroup$ – giofrida Sep 21 '20 at 19:24
  • 1
    $\begingroup$ @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? $\endgroup$ – plshelp Sep 22 '20 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$.

In Scala, such subtyping 'facts' can be added by declaration when defining a type. So, arrays are declared to be subtypes of function types. You gave this as:

$$[U] <: \mathsf{Int} → U$$

This is just an axiom that needs to be part of the subtyping check. Scala is actually even more complex than this, but this at least covers the subtyping part.

As Andrej mentioned in the comments, these sorts of arbitrary 'declared' subtyping axioms don't necessarily lead to the nicest behavior (principal types, decidability, etc.). There might be multiple particular strategies that you could replace your steps with to incorporate the change to step 2, and they might have different limitations on what types they can check/infer for various examples.

  • $\begingroup$ 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. $\endgroup$ – giofrida Sep 25 '20 at 7:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.