함수 유형

컴퓨터 과학과 수리논리학에서 함수형(영어: function type, 또는 화살표형 또는 지수형)은 변수나 매개변수에 함수가 할당되었거나 할당될 수 있는 형식이거나, 함수를 받거나 반환하는 고차 함수의 인자 또는 결과 형식이다.

함수형은 매개변수의 형식과 함수의 결과 형식에 따라 달라진다(이는, 또는 더 정확하게는 적용되지 않은 타입 생성자 · → ·는 고계 타입이다). 단순 타입 람다 계산과 같이 함수가 커리 형식으로 정의되는 이론적 환경 및 프로그래밍 언어에서는 함수형이 정의역 A와 치역 B의 두 가지 형식에만 의존한다. 여기서 함수형은 수학적 관례에 따라 종종 A → B 또는 집합의 범주에서 A를 B로 매핑하는 정확히 B^A(지수적으로 많은) 집합론적 함수가 존재한다는 사실에 기반하여 B^A로 표기된다. 이러한 매핑 또는 함수의 클래스를 지수 대상이라고 한다. 커링 행위는 함수형을 수반 곱 타입으로 만든다. 이는 커링에 대한 문서에서 자세히 다룬다.

함수형은 다른 속성 중에서도 다형적 함수의 개념을 포함하는 의존 곱 타입의 특수한 경우로 간주될 수 있다.

프로그래밍 언어

여러 프로그래밍 언어에서 함수형에 사용되는 구문은 다음과 같이 요약할 수 있으며, 고차 함수 합성 함수의 예시적인 타입 시그니처도 포함되어 있다.

언어		표기법	예시 타입 시그니처
일급 함수, 매개변수 다형성	C#	Func<α1,α2,...,αn,ρ>	Func<A,C> compose(Func<B,C> f, Func<A,B> g);
	하스켈	α -> ρ	compose :: (b -> c) -> (a -> b) -> a -> c
	OCaml	α -> ρ	compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
	스칼라	(α1,α2,...,αn) => ρ	def compose[A, B, C](f: B => C, g: A => B): A => C
	표준 ML	α -> ρ	compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
	스위프트	α -> ρ	func compose<A,B,C>(f: (B) -> C, g: (A) -> B) -> (A) -> C
	러스트	fn(α1,α2,...,αn) -> ρ	fn compose<A, B, C>(f: fn(A) -> B, g: fn(B) -> C) -> fn(A) -> C
일급 함수, 매개변수 다형성 없음	Go	func(α1,α2,...,αn) ρ	var compose func(func(int)int, func(int)int) func(int)int
	C++, 오브젝티브-C, 블록 포함	ρ (^)(α1,α2,...,αn)	int (^compose(int (^f)(int), int (^g)(int)))(int);
일급 함수 없음, 매개변수 다형성	C	ρ (*)(α1,α2,...,αn)	int (*compose(int (*f)(int), int (*g)(int)))(int);
	C++11	고유하지 않다. std::function<ρ (α1,α2,...,αn)>는 더 일반적인 형식이다(아래 참조).	function<function<int(int)>(function<int(int)>, function<int(int)>)> compose;

예를 들어 C#의 타입 시그니처를 보면, compose 함수의 타입은 실제로는 Func<Func<A,B>,Func<B,C>,Func<A,C>>이다.

C++11의 std::function에서 타입 소거가 발생하기 때문에, 고차 함수 매개변수에는 템플릿을, 클로저에는 자료형 추론 (auto)을 사용하는 것이 더 일반적이다.

표시적 의미론

프로그래밍 언어의 함수형은 모든 집합론적 함수 공간에 해당하지 않는다. 자연수의 가산 무한 타입을 정의역으로 하고 부울을 치역으로 한다면, 그들 사이에는 비가산 무한한 수(2^ℵ₀ = c)의 집합론적 함수가 존재한다. 분명히 이 함수 공간은 어떤 프로그래밍 언어에서 정의될 수 있는 함수의 수보다 크다. 왜냐하면 오직 가산적으로 많은 프로그램(프로그램은 유한한 수의 기호로 이루어진 유한한 시퀀스)이 존재하며, 집합론적 함수 중 하나는 효과적으로 정지 문제를 해결하기 때문이다.

표시적 의미론은 함수형과 같은 프로그래밍 언어 개념을 모델링하기 위한 더 적절한 모델(도메인이라고 불림)을 찾는 데 관심을 둔다. 프로그래밍 언어가 비정지 계산을 작성하는 것을 허용한다면(프로그래밍 언어가 튜링 완전한 경우), 계산 가능 함수 집합으로 표현을 제한하는 것만으로는 충분하지 않다는 것이 밝혀졌다. 표현은 소위 연속 함수로 제한되어야 한다(실수 해석적 의미의 연속성이 아니라 스콧 위상에서의 연속성에 해당함). 그렇다 하더라도, 연속 함수 집합에는 모든 프로그래밍 언어에서 올바르게 정의될 수 없는 병렬-OR 함수가 포함된다.

같이 보기

• 데카르트 닫힌 범주
• 커링
• 지수 대상: 범주 이론적 등가물
• 일급 함수
• 함수 공간: 집합론적 등가물

각주

• Pierce, Benjamin C. (2002). 《Types and Programming Languages》. The MIT Press. 99–100쪽. ISBN 9780262162098.
• Mitchell, John C. 《Foundations for Programming Languages》. The MIT Press.
• “function type” (영어). 《nLab》.
• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study. See section 1.2.