Make λ arguments always interpreted as patterns? #79

jeanas commented 2026年05月06日 00:00:33 +02:00

This tripped up a number of my students in the tutorial I was giving today:

open import Data.Product
open import Data.Empty
open import Relation.Binary.PropositionalEquality
-- OK
foo : {A B : Set} → A ×ばつ B → A
foo = λ (a , b) → a
-- OK
bar : {A : Set} → ⊥ → A
bar = λ ()
-- KO
baz : {A : Set} {x y : A} → x ≡ y → y ≡ x
baz = λ refl → refl

In λ refl → ..., the refl is just interpreted as a variable name, not as a constructor name as it would be in pattern matching, unlike a definition by clauses and also unlike λ {refl → refl}. I don't quite get why, but if you're going to do a backwards compatibility break, maybe changing this is something to consider?

This tripped up a number of my students in the tutorial I was giving today: ``` open import Data.Product open import Data.Empty open import Relation.Binary.PropositionalEquality -- OK foo : {A B : Set} → A ×ばつ B → A foo = λ (a , b) → a -- OK bar : {A : Set} → ⊥ → A bar = λ () -- KO baz : {A : Set} {x y : A} → x ≡ y → y ≡ x baz = λ refl → refl ``` In `λ refl → ...`, the `refl` is just interpreted as a variable name, not as a constructor name as it would be in pattern matching, unlike a definition by clauses and also unlike `λ {refl → refl}`. I don't quite get why, but if you're going to do a backwards compatibility break, maybe changing this is something to consider?

totbwf commented 2026年05月06日 00:10:00 +02:00

This is definitely a common point of confusion! Unfortunately, this will not be possible to implement in Mikan. We elaborate pattern lambdas to top-level pattern matching definitions, so this would have some some unwanted consequences for most parts of the system. Lambdas like λ (a , b) → a are a bit more delicate as we can elaborate to a normal lambda + projections (this elaboration is quite leaky, if you've ever seen .patternInTele0 in goals this is why).

I think the real issue here is documentation/ux; once we get around to #3 this is something to keep in mind. This also feels like a good place to put a warning: if a user tries to λ-bind a constructor name, we should probably give them a heads up and then point to the docs.

This is definitely a common point of confusion! Unfortunately, this will not be possible to implement in Mikan. We elaborate pattern lambdas to top-level pattern matching definitions, so this would have some some unwanted consequences for most parts of the system. Lambdas like `λ (a , b) → a` are a bit more delicate as we can elaborate to a normal lambda + projections (this elaboration is quite leaky, if you've ever seen `.patternInTele0` in goals this is why). I think the real issue here is documentation/ux; once we get around to #3 this is something to keep in mind. This also feels like a good place to put a warning: if a user tries to `λ`-bind a constructor name, we should probably give them a heads up and then point to the docs.