Skip to content

Implicit Arguments

Jump to bottom Edit New page
andreasabel edited this page Dec 1, 2014 · 26 revisions

This page is about the redesign of Agda's implicit argument facilities.

Shortcomings of Agda's implicit arguments

Concerning syntax and printing

  • Implicit arguments can be given both by position and by name, but even an argument given by name must be in the right position.

  • Infix and mixfix operators do not take implicit arguments.

  • Module parameters can be explicit, but then it is unclear how to position the arguments of infix and mixfix operators (See Agda issue 632). This suggest to only allow implicit (= named) module parameters.

Concerning type checking

  • For Agda it is not clear when to insert the hidden argument or abstraction.

    • In some cases, type checking only succeeds if a hidden lambda is eagerly inserted:

      data Vec (A : Set) : Nat -> Set where
  vnil  : Vec A zero
  vcons : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

Cons = {A : Set} (a : A) {n : Nat} -> Vec A n -> Vec A (suc n)

cons : Cons
cons a = vcons a

      For check of vcons a : {n : Nat} -> Vec A n -> Vec A (suc n) to succeed, a hidden abstraction needs to be inserted: \{n} -> vcons {n = _} a will solve the _ by n.

      A more detailed account of type checking: First, the lhs is checked, building up a context of bound variables. The application cons a is internally expanded to cons {A} a, as the presence of visible argument a forces insertion of prior hidden arguments, here, A. After doing the minimum work on the lhs, the context is A : Set, a : A. The remaining type is {n : Nat} -> Vec A n -> Vec A (suc n). A this point, there is a choice to make:

      1. Insert the hidden argument n : Nat on the lhs, leading to cons {A} a {n} and context A : Set, a : A, n : Nat. Continuing checking the rhs against remaining type Vec A n -> Vec A (suc n), we switch to inference mode, as the rhs is an application vcons a. First, the type vcons : {A : Set} {n : Nat} -> A -> Vec A n -> Vec A (suc n) is inferred, then an application to visible argument a is encountered. At this point, meta variables are inserted for the hidden arguments to vcons, leading to vcons {_A A a n} {_n A a n} a : Vec _A _n -> Vec _A (suc _n). Note that the freshly created metas can depend on (and only on) the bound variables in the current context, which is A, a, and n. Finally, the inferred type Vec _A _n -> Vec _A (suc _n) is unified with the expected type Vec A n -> Vec A (suc n) leading to the solutions _A = A and _n = n.

      2. Do not insert hidden argument n : Nat but proceed directly to check the rhs. Type checking proceeds similar as in the first case, but the context is now only A : Set, a : A which means that both created metas _A and _n can only depend on bound variables A and a. Also, the final unification problem (inferred type <= expected type) is Vec _A _n -> Vec _A (suc _n) <= {n : Nat} -> Vec A n -> Vec A (suc n). This problem is unsolvable, even with strong subtyping rules, as n is not allowed to appear in the solution of _n.

    • In other cases, type checking only succeeds if a hidden lambda is not inserted:

      Ty = {T : Bool -> Set} -> ({b : Bool} -> T b -> T false) -> T true
postulate f : Ty

test : Ty
test g = f g

      After checking the lhs, we have context T : Bool -> Set, g : {b : Bool} -> T b -> T false, and we proceed to check the rhs f g against remaining type T true. As we are dealing with an application, we switch to inference mode, getting f : {T : Bool -> Set} -> ({b : Bool} -> T b -> T false) -> T true and seeing an application to visible argument g. Now, a new meta _T (which can depend on T and g) is inserted after f for the hidden argument f expects before visible argument g. The type of f {_T} is ({b : Bool} -> _T b -> _T false) -> _T true and we need to make sure that g is an acceptable argument to this function. When checking g : {b : Bool} -> _T b -> _T false, we are faced with a choice:

      1. Insert an implicit abstraction \{b} -> g which gets us to checking g : _T b -> _T false in context T : Bool -> Set, g : {b : Bool} -> T b -> T false, b : Bool. It remains to check that the inferred type of g is more general (or rather, not more specific) than the expected type, leading to the unification problem {b : Bool} -> T b -> T false <= _T b -> _T false. These types do not have the same shape, but we could have inserted a hidden argument _b after g (with meta variable _b depending on T, g, and b), in which case the unification problem became T _b -> T false <= _T b -> _T false. This problem decomposes into T false <= _T false and _T b <= T _b. As we are using higher-order unification, there is no unique solution for _T, and type checking fails.

      2. Do not insert an implicit abstraction, but check g directly against {b : Bool} -> _T b -> _T false. The inferred type of g is {b : Bool} -> T b -> T false, leading to the subtyping problem (inferred type <= expected type) {b : Bool} -> T b -> T false <= {b : Bool} -> _T b -> _T false. The difference to the first case is that now b is a bound variable on both sides, so we get the subproblems _T b <= T b and T false <= _T false. Subtyping is the same as equality (except maybe for implicit quantification such as {b : Bool} -> ... where we could use the strong subtyping rules of Curry-style System F, see below); thus, we get the equation _T b = T b and can solve _T = \ b -> T b = T.

Design goals

Goal: design implicit argument syntax that

  • has a more predictable behavior
  • still offers sufficient convenience to the user.

Behaviors we want (to preserve):

In the following example, the implicit argument j should be tied to the projection tail, i.e., whenever the projection is present, the implicit argument should be inserted eagerly.

record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    head : A
    tail : {j : Size< i} → Stream {j} A
open Stream public

map : ∀ {i A B} (f : A → B) (s : Stream {i} A) → Stream {i} B
head (map f s) = f (head s)
tail (map f s) = map f (tail s)

This will be expanded to:

map : ∀ {i A B} (f : A → B) (s : Stream {i} A) → Stream {i} B
head (map {i} {A} {B} f s)     = f (head s)
tail (map {i} {A} {B} f s) {j} = map {j} {A} {B} f (tail s {j})

For reasons of termination, the implicit j : Size< i must be bound on the left hand side. The result of lazy insertion

tail (map {i} {A} {B} f s) = \{j} -> map {j} {A} {B} f (tail s {j})

is not accepted by the termination checker. Currently, there is a preprocessing phase in the termination checker that moves the \{j} to the left hand side. Maybe such extra effort can be avoided with the a new design.

Design brainstorming

  • Implicit arguments should always be given by name.
  • The order of implicit arguments should not matter that much. At least if implicit arguments belong to the same group, the order should be irrelevant. What a group is, is up to definition...

Names matter in implicit function space

As the name of a named argument matters when giving it to a function, it makes sense it also matters in the type.

postulate
  P : Nat → Set

T  = {a : Nat}(A : P a) -> P a
T' = {b : Nat}(B : P b) -> P b

In this philosophy, the types T and T' are actually different. The following two definitions should be rejected:

T≡T' : T ≡ T'
T≡T' = refl

badcast : T → T'
badcast g = g

T and T' are only isomorphic, we can cast with a little more eta-expansion:

cast : T → T'
cast g {b = n} x = g {a = _} x

cast' : T' → T
cast' g x = g x  -- works, since implicits are inserted when x is given

In essence, an implicit argument is like a record with one field: the name of the field matters.

On subtyping

We need to avoid the strong subtyping for polymorphic lambda-calculus, which is:

  B[X/x]       <= C
  ----------------- X fresh meta
  {x : A} -> B <= C

  y : C |- A <= D
  -----------------
  A <= {y : C} -> D

These rules are the source of undecidability of Curry-style System-F subtyping. In our setting, they create additional unification problems which might not be solvable.

We restrict to the structural subtyping which does not create new unification problems:

  C <= A    x:C |- B <= D
  ----------------------------
  {x : A} -> B <= {x : C} -> D

The strong subtyping behavior can only be obtained with explicit insertion of lambdas or arguments:

  e : {x : A} -> B
  -----------------
  e {x = X} : B[X/x]    B[X/x] <= C
  ---------------------------------
  e {x = X} : C

and

  e : A                           x:C |- A <= D
  ----------------------------    ----------------------------
  \{x = x} -> e : {x : C} -> A    {x : C} -> A <= {x : C} -> D
  ------------------------------------------------------------
  \{x = x} -> e : {x : C} -> D

Permutation of implicit arguments

We gain something from this stricter equality checking for types: We can allow permutation of implicit arguments. The relative order in which they are given should not matter (just like for records). For instance the following two types become equal:

T  = {A : Set} {n : Nat} (v : Vec A n) -> (a : A) -> Vec A (suc n)
T' = {n : Nat} {A : Set} (v : Vec A n) -> (a : A) -> Vec A (suc n)

And we can give a named argument out of order.

f : T -> {A : Set} (v : Vec A 1) -> A -> Vec A 2
f snoc = snoc {n = 1}

Groups

A group is a telescope concerning at least one explicit argument. Groups are separated by -> in function type. The implicits of a group are inserted when the explicit argument is given.

Telescopes without explicit arguments can also appear in function types, but these implicits are eagerly inserted. Such groups of implicits are only allowed in type signatures, but never in types that are computed.

Legal:

Type : {a : Level} -> Set (suc a)
Type {a = a} = Set a

Illegal:

T = {a : Level} -> Set (suc a)
Type : T
Type {a = a} = Set a

This is illegal already, but for a different reason, because one cannot name a level-polymorphic type (it lives in Set\omega, for which there is no expression).

Reason to rule this out (see issue 1095):

T : Nat -> Set
T zero = Nat
T (suc n) = {x : Nat} -> T n

Checking e : T _n we do not know whether we have to insert a hidden lambda.

Example

With groups, the definition of Ty above is illegal, you cannot have a group of implicits only in a defined type. A legal version would be:

Ty = {T : Bool -> Set} (g : {b : Bool} (_ : T b) -> T false) -> T true
postulate f : Ty

test : Ty
test g = f g

Here, test g will get the type T true where g has type {b : Bool}(_ : T b) -> T false. We check the rhs f g against T true. Definitionf infers to Ty, no implicits inserted. When applying to g we insert implicit _T and check g against {b : Bool}(_ : _T b) -> _T false. This type unifies with the type of g, yielding solution _T = T. The type of f g is inferred to be T true.

Vec-Example

Consider above example with interpreting -> as group separator:

data Vec (A : Set) : Nat -> Set where
  vnil  : Vec A zero
  vcons : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

cons : {A : Set} (a : A) {n : Nat} -> Vec A n -> Vec A (suc n)
cons a = vcons a

This expands to

cons {A = A} a {n = n} = vcons {n = _} a

which will solve the _ by n.

Vec-Example (failing)

If we group the arguments to cons differently, type-checking fails.

cons : {A : Set} (a : A) -> {n : Nat} (v : Vec A n) -> Vec A (suc n)
cons a = vcons a

Now, this expands to

cons {A = A} a = vcons {n = _} a

with no solution for _.

Vec-Example (suggested argument order)

As the argument order of vcons matters, this is probably the best grouping, with index n in the same group as xs, the first argument referring to it.

data Vec (A : Set) : Nat -> Set where
  vnil  : Vec A zero
  vcons : (x : A) -> {n : Nat} (xs : Vec A n) -> Vec A (suc n)

This minimizes the scope of the implicit parameter n.

Module telescopes

Do we need grouping for modules telescopes? See issue 682: mixfix printing destroyed by explicit module parameters.

An approach is to disallow explicit arguments in module telescopes. All arguments have to be given by name. With implicit arguments only, we do not get into the trouble that all holes in a mixfix operator are shifted, but it would be nice to have named arguments to mixfix ops as well. Needs extension of parser.

module M {A : Set} where
  postulate
    if_then_else_ : Bool -> A -> A -> A
open M  -- gives: if_then_else_ : {A : Set} -> Bool -> A -> A -> A

test : Nat
test = if {A = Nat} true then 3 else 5

Records and record modules

Fundamental problem: projections. Agda, as Haskell, confuses field and projection names. The dot-notation r.field of OO and OCaml etc. would be a better choice for projecting a field.

No action plan yet: Maybe infix/mixfix ops in record modules should be forbidden.

Data type parameter telescopes

Design

Agda meeting XX, October 2014:

  • Reuse Agda syntax
  • Distinguish type schemes from types
  Introductions (base types)

    I ::= s             -- sort (like Set l)
        | D vs          -- data type
        | R vs          -- record type
        -- type operators, functions
        | λ v           -- abstraction
        -- non-types
        | c vs          -- constructed thing
        | l             -- level

  Types

  v,A ::= I             -- base type / introduction
        | Π {Ss} Π S λS -- visible function type
        -- eliminations: these are never turning into eager implicit
        | X es          -- meta variable
        | x es          -- variable
        | f es          -- function

  Type Schemes

    S ::= A
        | Π {Ss} λI    -- proper scheme: eagerly inserted implicits

Type signatures (refer to type schemes)

  f : S

Types are closed under substitution as type variables stand for types only, not for type schemes. Type meta variables are also denoting type schemes.

Do we need meta variables for type schemes as well?

  f : _
  f = t
Add a custom footer
Add a custom sidebar
Clone this wiki locally