Import list

module Term_Inference where

open import Data.Empty    using (⊥)
open import Data.Unit     using (⊤; tt)
open import Data.Sum      using (_⊎_; inj₁; inj₂)
open import Data.Nat      using (ℕ; zero; suc)

Term inference

The Agda compiler tries to infer terms marked with underscore. If the choice of term is ambiguous, the term inference will fail.

Examples:

data Fin′ : ℕ → Set where
  zero : (n : _) → Fin′ (suc n)            -- ℕ is inferred
  suc  : (n : _) → Fin′ n → Fin′ (suc n)   -- ℕ is inferred again

x : Fin′ 
x = suc _ (zero _)   -- 2 and 1 are inferred

Term inference failure is marked with yellow colour.

Implicit arguments

Underscores can be hidden by making arguments of constructors implicit with curly brackets.

data Fin : ℕ → Set where
  zero : {n : _} → Fin (suc n)
  suc  : {n : _} → Fin n → Fin (suc n)

After that, we obtain the following:

x′ : Fin 
x′ = suc {_} (zero {_})

And the {_}s can be now deleted:

x″ : Fin 
x″ = suc zero

Although zero : Fin 1 and zero : Fin 2, zero does not have multiple different types; the implicit arguments make the types unique.

Named and multiple implicit arguments

There can be more implicit arguments, as the following definition demonstrates:

data T : ℕ → ℕ → ℕ → Set where
  c : {n m k : _} → T (suc n) (suc m) (suc k)

xt : T   
xt = c

In addition to that, in case of multiple implicit arguments, some of their actual values may be set by naming them. For example:

xt' : T   
xt' = c {m = }

Syntactic abbreviations

Consider the following definitions again from above:

data Fin′ : ℕ → Set where
  zero : (n : _) → Fin′ (suc n)
  suc  : (n : _) → Fin′ n → Fin′ (suc n)

data Fin : ℕ → Set where
  zero : {n : _} → Fin (suc n)
  suc  : {n : _} → Fin n → Fin (suc n)

There variables with inferred types can be introduced by the ∀ (universal quantification) symbol, no matter if they are explicit or implicit:

data Fin′ : ℕ → Set where
  zero : ∀ n → Fin′ (suc n)
  suc  : ∀ n → Fin′ n → Fin′ (suc n)

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)