Type-checking function calls with functional subtyping

Computer Science Asked by giofrida on December 10, 2020

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 $Tto 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 $[thinspacecdotthinspace]$ 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 $Ttotop$, 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?

One Answer

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.

Answered by Dan Doel on December 10, 2020

Add your own answers!

Related Questions

Design of a synchronized clock

0  Asked on October 21, 2021 by ahmedou


How private IP address is determined?

1  Asked on October 21, 2021 by nurin-izzati-jafri


Race Condition in Mesa Monitor

0  Asked on October 21, 2021 by heroman


Counting one’s in a stream of bits

0  Asked on October 21, 2021 by srajan


Find original array from array with pairs of adjacent elements

1  Asked on October 21, 2021 by james-flanagin


Ask a Question

Get help from others!

© 2022 All rights reserved. Sites we Love: PCI Database, MenuIva, UKBizDB, Menu Kuliner, Sharing RPP