With-expression

TOC

TODO: syntax for nested with

A simple example

When using the with construct to pattern match on intermediate results the terms matched on are abstracted from the goal type and possibly also from the types of previous arguments. This makes it possible to prove properties of functions defined by with, simply by following the same recursion pattern.

An example 

 filter : {A : Set} → (A → Bool) → List A → List A
 filter p [] = []
 filter p (x :: xs) with p x
 ... | true  = x :: filter p xs
 ... | false = filter p xs

 module Proof {A : Set}(P : List A → Set) where

   proof : (p : A → Bool)(xs : List A) → P (filter p xs)
   proof p [] = ?0
   proof p (x :: xs) with p x
   ... | true  = ?1
   ... | false = ?2

Before the with in proof the goal was P (filter p (x :: xs)) which reduces to P (filter p (x :: xs) | p x). When performing the with, p x is abstracted from the goal type so in the two branches we have ?1 : P (filter p (x :: xs) | true) which reduces to P (x :: filter p xs) and ?2 : P (filter p (x :: xs) | false) which reduces to P (filter p xs).

For the full example see test/succeed/Filter.agda.

More in depth

When using a with the context is split in two parts

  • the part needed to type the with arguments, and
  • anything else

The with arguments are abstracted over the latter part and the goal type, but not the former.

In greek:

Consider 

  f : Γ → A
  f xs with vs

assuming for simplicity that there’s no pattern matching in xs. First infer the types of vs 

  Γ ⊢ vs : As

Now find a well-formed context Γ₁, Γ₂ which is a permutation of Γ such that 

  Γ₁ ⊢ vs : As

Compute Δ by abstracting each type in As over earlier vs, so Γ₁ ⊢ vs : Δ and Δ{vs} = As (where (x : A)Θ {v,vs} = A, Θ[v/x]{vs}). Then compute B such that 

  Γ₁, Δ ⊢ B type  and
  B[vs/Δ] = Γ₂ → A  (i.e. abstract Γ₂ → A over vs)

This gives the type of the with function: 

  withfun : Γ₁ → Δ → B

Note that the abstraction steps can fail to produce a well-typed term.

Some examples: 

 postulate
   A     : Set
   _+_   : A → A → A
   T     : A → Set
   mkT   : ∀ x → T x

 -- x and y are needed to type the with argument, so the context
 -- is split after y
 f₁ : (x y : A)(t : T (x + y)) → T (x + y)
 f₁ x y t with x + y
 f₁ x y t | w = {!!}

 -- Generated with function
 with₁ : (x y : A) (w : A) (t : T w) → T w
 with₁ x y w t = {!!}

 -- x is not needed to type the with argument, so the context
 -- is reordered with only y before the with argument
 f₂ : (x y : A)(t : T (y + y)) → T (y + y)
 f₂ x y t with y + y
 f₂ x y t | w = {!!}

 with₂ : (y : A) (w : A) (x : A) (t : T w) → T w
 with₂ y w x t = {!!}

 postulate
   H : ∀ x y → T (x + y) → Set

 -- Multiple with arguments are always inserted together, so in this case
 -- t ends up on the left since it’s needed to type h and thus x + y isn’t
 -- abstracted from the type of t
 f₃ : (x y : A) (t : T (x + y)) (h : H x y t) → T (x + y)
 f₃ x y t h with x + y | h
 f₃ x y t h | w₁ | w₂ = {!!}  -- t : T (x + y), goal : T w₁

 with₃ : (x y : A) (t : T (x + y)) (h : H x y t) (w₁ : A) (w₂ : H x y t) → T w₁
 with₃ x y t h w₁ w₂ = {!!}

 -- But earlier with arguments are abstracted from the types of later ones
 f₄ : (x y : A) (t : T (x + y)) → T (x + y)
 f₄ x y t with x + y | t
 f₄ x y t | w₁ | w₂ = {!!}  -- t : T (x + y), w₂ : T w₁, goal : T w₁

 with₄ : (x y : A) (t : T (x + y)) (w₁ : A) (w₂ : T w₁) → T w₁
 with₄ x y t w₁ w₂ = {!!}