Curly Braces and Lambdas in Agda

Question

The docs on lambdas in Agda provide two forms of lambda: a curly brace based version, and the where syntax. But while writing some programs, I stumbled across a third version: one pattern, no braces, no where. I thought it would behave the same as a single pattern and braces, but here's a counter example to that:

natid : ℕ → ℕ
natid = λ x → x

g0 : ( λ x → natid x ) ≡ ( λ x → natid x )
g0 = refl

g1 : ( λ { x → natid x } ) ≡ ( λ x → natid x )
g1 = refl

g2 : ( λ x → natid x ) ≡ ( λ { x → natid x } )
g2 = refl

g3 : _≡_ {_} {_ → _} ( λ { x → natid x } ) ( λ { x → natid x } )
g3 = refl

-- g4 : ( λ { x → natid x } ) ≡ ( λ { x → natid x } )
-- this fails with error message:
     _a_91 : Agda.Primitive.Level  [ at /Users/olekgierczak/repos/plfa/src/plfa/part1/Connectives.lagda.md:278,28-29 ]
     _A_92 : Set _a_91  [ at /Users/olekgierczak/repos/plfa/src/plfa/part1/Connectives.lagda.md:278,28-29 ]
     _94 : _A_92  [ at /Users/olekgierczak/repos/plfa/src/plfa/part1/Connectives.lagda.md:278,8-25 ]

     ———— Errors ————————————————————————————————————————————————
     Unsolved constraints

So my question is, what does a lambda with no braces around a single pattern mean, and why does the type inference of Agda treat g1/g2/g4 differently.

Answer 1

The key thing about "pattern" lambda is that it's a fake: each such thing elaborates as the local invocation of a new (i.e., generative) top-level helper function. The type declaration for that helper function must be somehow synthesized, and it is indeed important to allow it to be a dependent type. It looks to me as if allowing the extra degrees of freedom on both sides of the equation results in an underconstrained inference problem.

In response to the question in the comment, the g3 example gives _ -> _ as the type at which equality is demanded, which constrains the type of the function to be non-dependent. That seems to be enough information to ensure a most general solution.

Meanwhile, in reference to the examples which do check out, note that g0 requires only syntactic identity to go through; the other three work only thanks to eta-expansion and laziness. You should really think of each pattern lambda as some generated foo, which has a definition given by what's in the braces. Neither foo nor \ x -> natid x reduces. Fortunately, as they have function type, Agda will generate a fresh variable standing for a hypothetical input and apply both functions to it, at which point they do both compute. But foo computes only because it is lazy in its input.

So here's the classic gotcha:

yay : (\ f -> _≡_ {_}{Bool -> Bool} f f) (\ { false -> true ; true -> false })
yay = refl

checks, but

nay : _≡_ {_}{Bool -> Bool}
        (\ { false -> true ; true -> false })
        (\ { false -> true ; true -> false })
nay = {!refl!}

does not.

How so? In yay only one auxiliary definition is generated, and it is seen to be the same as itself by name. In nay, two auxiliary definitions are generated, differing only in name, but eta-expansion is not enough to make the names compute away.

Answer 2

I'm not familiar with how Agda is implemented, but while no one else has answered yet I'll hazard a guess. I think the difference between (λ x → natid x) and (λ {x → natid x}) is that a pattern lambda can be thought of as a "case" expression, like you'd find in Coq. So you might think of the latter as (in pseudo-Agda where case expressions exist):

λ x →
  case x of
    x ⇒ natid x

Because the return type of a case expression could depend on the argument itself, you can assign different types to this. For instance, imagining that one could annotate case expressions with its return type abstracted over the argument,

λ x →
  case x return (λ y → case y of _ ⇒ ℕ) of
    x ⇒ natid x
: ∀ x → case x of _ ⇒ ℕ

whose type isn't equal to ℕ → ℕ, assuming we're missing eta laws that would otherwise definitionally equate case x of _ ⇒ ℕ with ℕ. (I'm not really sure if you could make Agda have definitional eta laws for ℕ.) So without specifying the intended type of the term as g3 does, the type gets considered as unsolved. (I'm not sure why simply giving it type _ → _ works though.)

Meanwhile, a type can easily (or heuristically?) be inferred for λ x → natid x, since natid : ℕ → ℕ so x : ℕ and natid x : ℕ so the whole term has type ℕ → ℕ as well.

Interestingly, the corresponding example works in Coq, so I'm guessing it has more heuristics than Agda, assigning some "simplest" type to match expressions when possible.

Definition natid (x : nat) : nat := x.
Definition test : (fun x => match x with x => natid x end) = (fun x => match x with x => natid x end) := eq_refl.