함수형

Function type

컴퓨터 과학과 수학 논리학에서 함수형(또는 화살표형 또는 지수형)은 함수가 있거나 할당될 수 있는 변수나 매개 변수의 유형 또는 함수를 취하거나 반환하는 고차 함수의 인수나 결과 유형이다.

함수 유형은 매개 변수의 유형과 함수의 결과 유형(또는 더 정확하게 적용되지 않은 유형 생성자)에 따라 달라진다. · → · 는 고품종이다.)단순 타이핑된 람다 미적분처럼 함수가 큐레이션된 형태로 정의되는 이론적 설정과 프로그래밍 언어에서 함수 유형은 정확히 두 가지 유형인 도메인A와 범위B에 따라 달라진다.여기서 함수 유형은 종종 집합 범주에서 A와 B를 매핑하는 현존하는 정확히A 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
일등 기능으로는
파라메트릭 다형성 없이 		가다 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ℵ0)분명히 이 함수의 공간은 어떤 프로그래밍 언어에서 정의될 수 있는 함수의 수보다 더 크다. 그 이유는 셀 수 없이 많은 프로그램(한정된 수의 기호의 유한한 순서가 되는 프로그램)이 존재하며, 설정-이론 함수 중 하나가 정지 문제를 효과적으로 해결하기 때문이다.

변절적 의미론은 기능 유형과 같은 프로그래밍 언어 개념을 모델링하는 데 더 적합한 모델(도메인이라고 함)을 찾는 것과 관련이 있다.프로그래밍 언어가 비단말 연산 쓰기를 허용하는 경우(프로그래밍 언어가 튜링 완료인 경우)에도 계산 가능한 함수 집합으로 표현을 제한하는 것은 충분하지 않은 것으로 나타났다.표현은 소위 연속함수(Scott 위상에서의 연속성에 대응하고, 실제 분석적 의미에서의 연속성에 대응하지 않음)로 제한되어야 한다.그때도 연속함수의 집합은 모든 프로그래밍 언어에서 정확하게 정의될 수 없는 병렬 또는 함수를 포함한다.

참고 항목

참조

  • Pierce, Benjamin C. (2002). Types and Programming Languages. The MIT Press. pp. 99–100.
  • Mitchell, John C. Foundations for Programming Languages. The MIT Press.
  • nLab의 함수 유형
  • 호모토피 유형 이론: 수학의 단발적 기초, 단발적 기초 프로그램, 고등 연구 연구소.섹션 1.2를 참조하십시오.