유형 생성자

유형 이론으로 알려진 수학적 논리학 및 컴퓨터 과학 분야에서 유형 생성자는 오래된 형식 언어로부터 새로운 형식을 구축하는 유형화된 형식 언어의 특징이다.기본형은 무효형 생성자를 사용하여 구축되는 것으로 간주된다.일부 유형 생성자는 인수로 다른 유형(예: 제품 유형, 함수 유형, 전원 유형 및 목록 유형)을 취한다.새로운 형식은 형식 생성자를 재귀적으로 구성하여 정의할 수 있다.

예를 들어 단순하게 입력된 람다 미적분은 단일 유형 생성자, 즉 함수 유형 생성자를 가진 언어로 볼 수 있다.제품 유형은 일반적으로 커서를 통해 활자화된 람다 칼쿨리에서 "빌트인"으로 간주할 수 있다.

추상적으로 유형 생성자는 인수 0 이상의 유형으로 간주하고 다른 유형을 반환하는 n-ary 유형 연산자다.커리어를 사용하는 n-arry 유형의 연산자는 단일 유형 연산자의 적용 순서에 따라 작성될 수 있다.따라서 우리는 유형 연산자를 단순히 입력된 람다 미적분학으로서 볼 수 있는데, 이 유형 연산자는 보통 기본형인 $\ast {\displaystyle }$ ${\displaystyle *}$을 나타내고$,$ 기초 언어의 모든 유형인 "유형"을 발음하는 것으로 볼 수 있는데, 이 유형 연산자를 자체 c에서 유형 연산자의 유형과 구별하기 위해 현재는 적절한 유형이라고 한다.알쿨루스, 이것을 종류라고 부른다.

형식 연산자는 형식 변수를 바인딩할 수 있다.예를 들어, 형식 수준에서 단순 형식의 calc-미적분의 구조를 제공하려면 바인딩 또는 고차 유형의 연산자가 필요하다.이러한 결합형 연산자는 λ-큐브의 제2축에 해당하며, 단순형 λ-계산서와 형식 연산자 λ_ω. 다형 연산자 λ- 미적분(시스템 F)와 결합하면 시스템 F가_ω 산출된다.

참고 항목

• 종류(유형 이론)
• 대수 데이터 유형
• 재귀 데이터 유형

참조

• Pierce, Benjamin (2002). Types and Programming Languages. MIT Press. ISBN 0-262-16209-1., 29장 "유형 연산자 및 킨딩"
• P.T. 존스톤, 코끼리의 스케치, 페이지 940