함수 타입
함수 타입 (Function Types)
함수 타입은 (x : A) → B로 쓰고, 비의존 함수의 경우 간단히 A → B로 써요. 예를 들어 자연수의 덧셈 함수 타입은 다음과 같아요:
Nat → Nat → Nat
그리고 벡터의 덧셈 함수 타입은 다음과 같아요:
(A : Set) → (n : Nat) → (u : Vec A n) → (v : Vec A n) → Vec A n
여기서 Set은 집합의 타입이고, Vec A n은 타입 A의 원소 n개를 가진 벡터의 타입이에요. 연속된 가정 (x : A) 사이의 화살표는 생략할 수도 있고, (x : A) (y : A)는 (x y : A)로 줄일 수도 있어요 (텔레스코프도 참고하세요):
(A : Set) (n : Nat)(u v : Vec A n) → Vec A n
함수는 람다 표현식이나 함수 정의로 구성돼요.
함수 f : (x : A) → B를 인자 a : A에 적용하는 것은 f a로 쓰고, 그 타입은 B[x := a]예요.
표기 관례 (Notational conventions)
함수 타입:
prop₁ : ((x : A) (y : B) → C) is-the-same-as ((x : A) → (y : B) → C)
prop₂ : ((x y : A) → C) is-the-same-as ((x : A)(y : A) → C)
prop₃ : (forall (x : A) → C) is-the-same-as ((x : A) → C)
prop₄ : (forall x → C) is-the-same-as ((x : _) → C)
prop₅ : (forall x y → C) is-the-same-as (forall x → forall y → C)
forall 대신 유니코드 기호 ∀(Emacs Agda 모드에서 "\all"을 입력하세요)를 사용할 수도 있어요.
함수 추상화:
(\x y → e) is-the-same-as (\x → (\y → e))
함수 적용:
(f a b) is-the-same-as ((f a) b)