# 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?

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

## Related Questions

### What are the differences between Earliest Deadline First (EDF) and Earliest Due Date (EDD)?

1  Asked on November 5, 2021

### If a grammar G is left and right regular, why $||L(G)|| leq ||P||$?

1  Asked on November 5, 2021

### Scheduling jobs online on 3 identical machines – a lower bound of 5/3

0  Asked on November 5, 2021

### Proof for values of d with d:= ||L|| – N(L) with $d in mathbb{Z}$ and N(L) Nerode Index

1  Asked on November 5, 2021

### Is there a way to map the concatenation operation over strings to the addition operation over $mathbb{N}$

1  Asked on October 21, 2021

### Confusion in Reduction of Hamiltonian-Path to Hamiltonian-Cycle

2  Asked on October 21, 2021

### Proof: is the language $L_1={langle Mranglemidemptyset subseteq L(M)}$ (un)-decidable?

2  Asked on October 21, 2021 by schleudergang

### Removing left factoring from Context-Free Grammar

1  Asked on October 21, 2021 by mmbs

### Design of a synchronized clock

0  Asked on October 21, 2021 by ahmedou

### How do you calculate the running time using Big-O notatation?

1  Asked on October 21, 2021 by veree

### How private IP address is determined?

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

### Is the discrepancy in Turing’s representation of complete configurations intentional?

0  Asked on October 21, 2021

### First-time and second-time seen edges in DFS on undirected graphs

1  Asked on October 21, 2021 by mgus

### Race Condition in Mesa Monitor

0  Asked on October 21, 2021 by heroman

### Equivalence of Krom formulas tractable?

2  Asked on October 21, 2021

### Nondeterministic polynomial time algorithm versus certificate/verifier for showing membership in NP

1  Asked on October 21, 2021 by atsina

### Intuition behind the entire (amortized) concept of Fibonacci Heap operations

0  Asked on October 21, 2021

### Counting one’s in a stream of bits

0  Asked on October 21, 2021 by srajan

### Conway’s Game of Life: Is it really P-complete?

1  Asked on October 21, 2021 by fluffysheap

### Find original array from array with pairs of adjacent elements

1  Asked on October 21, 2021 by james-flanagin