This module contains a compiler pass that applies η-conversions to expressions such that all function and constructor applications are fully applied.

An η-conversion is the conversion of a partially applied function expression f to a lambda expression \x -> f x that explicitly applies the missing argument.

Motivation

We have to perform η-conversions due to an optimization of the monadic translation of function declarations. An n-ary function declaration of type τ₁ -> … -> τₙ -> τ is translated to a function declaration of type τ₁' -> … -> τₙ' -> τ' where τᵢ' is the translation of type τᵢ. However, an n-ary lambda abstraction of the same type is translated to m (τ₁' -> (τ₂ -> … -> τₙ -> τ)') where m is the target monad. That only the arguments but not the intermediate results of function declarations are lifted to the monad, improves the readability of generated function applications. Intermediate results don't have to be bound since we know that partial applications cannot have an effect. This optimization does not work when functions are applied only partially. Thus, we have to convert partial applications to full applications.

We differentiate between top-level partial applications (i.e. when a function is defined as the partial application of another defined function or constructor) and partial applications that occur in the arguments of the function declaration's right-hand side.

We perform regular η-conversions on partial applications in proper subexpressions of a function declaration's right-hand side.

However, on the top-level, we add the missing arguments to the left-hand and right-hand sides of the function rule explicitly, without a lambda abstraction. This is an optimization that allows the compiler to avoid some unnecessary monadic lifting.

Specification

Preconditions

The arity of all constructors and functions must be known (i.e., there must be corresponding environment entries) and all function declarations must be type annotated.

Translation

Assume that we have the following function declaration.

f (e₁ :: τ₁) … (eₖ :: τₖ) :: τ'₁ -> … -> τ'ₙ₋ₘ -> τ =
    g @α₁ … @αₚ e₁ … eₘ

where g is the name of an n-ary constructor or function declaration and m < n. This declaration is then replaced by

f (e₁ :: τ₁) … (eₖ :: τₖ) (x₍ₘ₊₁₎ :: τ'₁) … (xₙ :: τ'ₙ₋ₘ) :: τ =
    g @α₁ … @αₚ e₁ … eₘ x₍ₘ₊₁₎ … xₙ

where x₍ₘ₊₁₎ … xₙ are n-m fresh variables.

If a function rule has several alternatives for the right-hand side through (possibly nested) if or case expressions, the number of added arguments is determined by the minimum number of missing arguments for an alternative on the right-hand side.

Additionally, on the right-hand sides of function declarations, all of the largest sub-expressions of the form

h @α₁ … @αᵣ e₁ … eₗ

where h is the name of an p-ary constructor or function declaration and l < p are replaced by a lambda abstraction

\y₍ₗ₊₁₎ … yₚ -> f @α₁ … @αᵣ e₁ … eₘ y₍ₗ₊₁₎ … yₚ

where y₍ₗ₊₁₎ … yₚ are p-l fresh variables.

Both types of η-conversion may also be applied to the same expression. For example, the function

f (e₁ :: τ₁) ::  τ₂ -> τ₃ -> τ = case e₁ of {
    c₁ -> g;
    c₂ -> h
  }

where c₁ and c₂ are the constructors of τ₁, g is a binary function of type τ₂ -> τ₃ -> τ, and h is a unary function of type τ₂ -> (τ₃ -> τ), will be converted to

f (e₁ :: τ₁) (x :: τ₂) :: τ₃ -> τ = case e₁ of {
    c₁ -> \y -> g x y;
    c₂ -> h x
  }

Postconditions

All applications of n-ary functions or constructors have at least n arguments.