Solving system-F application with metavariables

We've all been there before. You have a function you want to call, and a variable you want to call it with, but you just don't want to manually write instantiations when all the needed info is (probably) there!

Warning - This is not particularly readable on mobile. Beware.

Take this simple example.

id : ∀a, a -> a
id x = x

x : int
x = 10

f : int
f = id [???] x

Now, in the normal realm of system-F, you'd need an instantiation where that ??? is, to allow the typechecker to see what you're calling the function with and ensuring it can typecheck the program properly. However, all the information is there! 10 is an int, id has type ∀a, a -> a, so why do we need to manually annotate the type?

The answer is that we don't have to if we use a technique called unification. Now, the ordinary goal of instantiation is to instantiate the ∀s within the type of a function, here id, to be able to get out a proper type instead of a ∀. However, instead of using instantiation, we can insert and solve metavariables.

What are metavariables?

A metavariable is just something unsolved within a type. These metavariables would replace ∀s within a type, and then can be solved for. Let's take the id example from above:

id : ∀a, a -> a
id = Λa λx : a . x

x : int
x = 10

f : int
f = id [???] x

When solving for ???, here are the steps we go through:

• Take the type of id, and replace any ∀ variables with metavariables.

• Take the left hand side of id's type, and figure out what each metavariable corresponds to.

• Apply that to the right hand side.

• Return that type.

Here, those steps would look like this:

-- id : ∀a, a -> a
-- x : int
f : int
f = id x
-- Replace the ∀ variables within id's type 
-- with metavariables ( here indicated by $m )

id : ∀a, a -> a
->
id : $m -> $m

-- Take the LHS of id, and figure 
-- out what each metavariable corresponds to:
LHS(id) : $m 
x : int
∴
$m = int

-- Apply that to the RHS of id:
RHS(id) : $m
$m = int
RHS(id) = int

-- Return that type
∴
id x : int

f : int

f = id x

type(f) == type(id x) 
-- True! We've solved the types 
-- for this expression, with no instantiations in site.

Now, how does this look for a bigger example, with, for example, multiple inputs, and multiple ∀s? Let's have a look.

apply : ∀a b, a -> (a -> b) -> b
apply x f = f x

id : ∀a, a -> a
id x = x

x : int
x = 10

result : int
result = (apply x) id

-- Here we go!

apply x
-- inst metavariables on apply
apply : $m1 -> ($m1 -> $m2) -> $m2

-- unify lhs of apply and x
LHS(apply) : $m1
x : int
∴
$m1 = int

-- apply to RHS of apply
RHS(apply) : (int -> $m2) -> $m2

-- return that type
(apply x) id
(apply x) : (int -> $m2) -> $m2
id : ∀a, a -> a

-- inst id with metavariables
id : $m3 -> $m3
-- unify lhs of apply and id
RHS(apply x) : int -> $m2
id : $m3 -> $m3

-- Here's a neat trick: This is recursive! 
-- unify lhs of (lhs of apply x) and lhs of id
LHS(LHS(apply x)) : int      -- (|int| -> $m2) -> $m2
LHS(id) : $m3                -- |$m3| -> $m3
∴
$m3 = int
-- apply to rhs of id
RHS(id) : $m3
∴
RHS(id) : int
-- unify rhs of (lhs of apply x) and rhs of id
RHS(LHS(apply x)) : $m2        -- (int -> |$m2|) -> $m2
RHS(id) : int                  -- int -> |int|
∴
$m2 = int
-- apply to RHS of apply x
RHS(apply x) : $m2               -- (int -> int) -> |$m2|
∴
RHS(apply x) : int               -- (int -> int) -> |int|
-- return that type
∴
typeof (apply x) id == int

result : int
result = (apply x) id

result : int
(apply x) id : int
type(result) == type((apply x) id)
🎉

And there we go! A larger function application chain solved, using no instantiation whatsoever.