람다 추상화
람다 추상화 (Lambda Abstraction)
람다 표현식 (Lambda expressions)
익명 함수는 람다 표현식 \x → u를 사용해 정의할 수 있어요:
myFun = \ x → x + x -- equivalent: `myFun x = x + x`
\(Emacs Agda 모드에서 "\\" 입력) 대신 유니코드 기호 λ(Emacs Agda 모드에서 "\lambda" 또는 "\Gl" 입력)를 사용할 수도 있어요.
람다 표현식은 여러 인자를 받을 수 있고 인자는 선택적으로 타입으로 주석될 수 있어요. 예를 들어 아래 두 표현식 모두 타입 (A : Set) → A → A를 가져요(두 번째 표현식은 다른 타입에도 대응해요):
example₁ = \ (A : Set)(x : A) → x
example₂ = \ A x → x
n(> 1)개의 인자를 취하는 함수는 단일 인자를 취해 n-1개의 인자를 가진 또 다른 함수를 반환하는 함수와 동등해요. 즉 함수는 커링돼 있어요.
curry : (λ x y → x + y) ≡ (λ x → (λ y → x + y))
curry = refl
Agda의 모든 함수는 η-동일성을 만족해요: f는 (정의적으로) λ x → f x와 같아요.
etaFun : myFun ≡ λ x → myFun x
etaFun = refl
특히 인자의 이름 변경까지 본문이 같은 두 람다 표현식은 같다고 간주돼요.
alpha : (λ x → x + 1) ≡ (λ y → y + 1)
alpha = refl
람다 표현식은 인자 주변에 중괄호(각각 이중 중괄호)를 추가해 암시 인자와 instance 인자를 받을 수 있어요.
implicit-lambda = λ {A : Set} (x : A) → x
instance-lambda = λ (A : Set) {{monoid-A : Monoid A}} → mempty
람다 표현식의 인자는 지우기 상태 같은 임의의 모달리티로도 주석될 수 있어요.
큐빅 Agda(see --cubical)에서는 위 예제 중 많은 것이 통과하지 않는다는 점에 주의하세요. 거기서 람다 표현식의 타입은 일반적으로 추론되지 않고, 람다는 주어진 타입에 대해서만 검사되기 때문이에요. 따라서 myFun 등에는 타입 시그니처가 필요해요.
패턴 람다 (Pattern lambda)
익명 패턴 매칭 함수는 다음 두 문법 중 하나를 사용한 패턴 람다로 정의할 수 있어요:
\ { p11 .. p1n -> e1 ; … ; pm1 .. pmn -> em }
\ where
p11 .. p1n -> e1
…
pm1 .. pmn -> em
(평소처럼 \와 ->는 λ와 →로 대체될 수 있어요.)
where 키워드는 들여쓰기된 절 블록을 도입한다는 점에 주의하세요. 절이 하나만 있으면 인라인으로 사용할 수 있어요.
패턴 람다의 예:
and : Bool → Bool → Bool
and = λ { true x → x ; false _ → false }
xor : Bool → Bool → Bool
xor = λ { true true → false
; false false → false
; _ _ → true
}
eq : Bool → Bool → Bool
eq = λ where
true true → true
false false → true
_ _ → false
myFst : {A : Set} {B : A → Set} → Σ A B → A
myFst = λ { (a , b) → a }
mySnd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
mySnd = λ { (a , b) → b }
swap : {A B : Set} → A × B → B × A
swap = λ where (a , b) → (b , a)
패턴 람다는 후위 표기의 projection을 사용해 코패턴도 쓸 수 있어요.
swap' : {A B : Set} → A × B → B × A
swap' = λ where
(a , b) .fst → b
(a , b) .snd → a
패턴 람다에서 where와 with 구성을 사용하는 것은 허용되지 않아요.
패턴 람다의 내부 표현 (Internal representation of pattern lambdas)
내부적으로 패턴 람다는 다음 형태의 함수 정의로 번역돼요:
extlam p11 .. p1n = e1
…
extlam pm1 .. pmn = em
여기서 extlam은 새 이름이에요. 즉 패턴 람다는 생성적(generative)이에요. 특히 본문이 같은 두 패턴 람다는 Agda에 의해 같다고 간주되지 않아요(일반 람다 표현식과 대조적으로).
(λ { true → true ; false → false }) ==
(λ { true → true ; false → false })
이 타입은 서로 다른 새 이름 extlam1과 extlam2에 대해 extlam1 ≡ extlam2와 동등해서 refl로 증명할 수 없어요.
부정 람다 (Absurd lambda)
부정 람다는 부정 패턴 ()을 사용하는 람다 표현식이에요.
absurd-lambda : 0 ≡ 1 → ⊥
absurd-lambda = λ ()
일반 패턴 람다와 달리 부정 람다는 중괄호나 where 키워드가 필요하지 않지만, 사용하는 것은 여전히 허용돼요.
absurd-lambda-curly : 0 ≡ 1 → ⊥
absurd-lambda-curly = λ { () }
absurd-lambda-where : 0 ≡ 1 → ⊥
absurd-lambda-where = λ where ()
부정 패턴 앞이나 뒤에 일반 인자를 두는 것도 허용돼요.
absurd-lambda-list : {A : Set} (x : A) (xs : List A) → x ∷ xs ≡ [] → ⊥
absurd-lambda-list = λ x xs ()