8
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ Oh huh, the documentation for normal λ-abstractions (those without braces or where) appears to be missing. $\endgroup$
    – James Wood
    Apr 18, 2022 at 20:24
  • $\begingroup$ Fun fact: if you turn on the --cubical flag, then all of the gn's types go yellow! That's what I'd have expected from a bidirectional perspective, but I guess in standard Agda there's some heuristic that lets normal λ-abstractions synthesise a (simple?) function type. (In cubical Agda, normal λ-abstractions also construct paths, so it would be non-canonical to synthesise a function type.) $\endgroup$
    – James Wood
    Apr 18, 2022 at 20:39
  • $\begingroup$ @mudri What is "go yellow"? $\endgroup$ Apr 18, 2022 at 20:42
  • $\begingroup$ @ArtemPelenitsyn Have not enough information to be either elaborated or produce a hard error message. In this case, the missing information is whether the λ-abstractions are constructing functions or paths. $\endgroup$
    – James Wood
    Apr 19, 2022 at 8:29

2 Answers 2

8
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ I think the equations in the question are red herrings. The immediate difference is that normal λ-abstractions check against type _, where extended λ-abstractions (i.e function definitions) do not. It's unclear to me precisely what the former is doing, otherwise I'd add an answer. $\endgroup$
    – James Wood
    Apr 19, 2022 at 8:24
  • $\begingroup$ Thanks for the answer, I think this clears up both what the pattern lambda means and why the type checking might differ between the examples. One remaining question I have is why is _->_ sufficient in g3? $\endgroup$ Apr 19, 2022 at 13:59
3
$\begingroup$

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.
$\endgroup$
3
  • $\begingroup$ I think this answer is basically right. You could bring the explanation closer to real Agda syntax (and also closer to the actual implementation) by using fresh top-level function definitions. As for why the annotation _ → _ helps, that is a pattern that only matches simple function types, so the previous discussion about the return type depending on the input in unknown ways does not apply. $\endgroup$
    – James Wood
    Apr 19, 2022 at 20:23
  • $\begingroup$ Interestingly, the type synthesis of ordinary λ-abstractions is not limited to simple function types. For example, you can do id : (A : Set) → A → A; id _ x = x; foo = λ A x → id A x, and foo will have a type (the same dependent function type as id). All that works because we know that we won't face any case distinctions which could complicate the return type. $\endgroup$
    – James Wood
    Apr 19, 2022 at 20:27
  • 1
    $\begingroup$ Regarding definitional eta laws for natural numbers, those make typing undecidable. Take a Turing machine M, and consider the convertibility problem between if (M halts in n step) then 0 else 1 and 0, the two would be convertible exactly when the Turing machine halts, by expanding n enough times. $\endgroup$ Apr 21, 2022 at 18:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.