주종류

형식 이론에서 형식 체계는 용어와 환경이 주어진 이 환경에 이 용어에 대한 주체 유형이 존재한다면, 즉 이 환경에서 이 용어에 대한 다른 모든 유형이 주체 유형의 한 예인 경우 주체 유형 속성을 갖는다고 한다.

주형 속성은 여러 가지 비교할 수 없는 가능한 유형을 갖는 대신, 표현 가능한 모든 유형을 포괄하는 유형을 사용하여 주어진 환경에 표현식을 입력하는 방법을 제공하기 때문에 유형 시스템에는 바람직한 유형이다.주형 특성이 있는 시스템에 대한 형식 추론은 일반적으로 주형 유추를 시도한다.

예를 들어, ML 시스템은 주형 속성을 가지고 있고 표현에 대한 주형은 힌들리-밀너형 추론 알고리즘에 의해 사용되는 로빈슨의 통일 알고리즘으로 계산할 수 있다.그러나 다형 재귀와 같이 ML의 형식 시스템에 대한 많은 확장은 주형의 추론을 이해할 수 없게 만들 수 있다.하스켈의 일반화된 대수 데이터 유형과 같은 다른 확장자는 언어의 주형 특성을 파괴하여 여러 옵션 중에서 의도된 유형을 "가성"하기 위해 형식 주석이나 컴파일러를 사용해야 한다.

주 타이핑 특성은 용어가 주어진 경우 가능한 모든 타이핑의 한 예인 타이핑(즉, 문맥과 형식을 가진 쌍)이 존재하도록 요구한다.주 타이핑 특성은 원칙 유형 특성과 혼동될 수 있지만 구별된다.원칙 유형 속성은 유형을 결정하기 위해 입력으로 맥락에 의존하지만, 결과적으로는 원칙 유형 속성이 컨텍스트를 출력한다.^[1]

참조

$\displaystyle \Gamma \!\vdash }$

이 프로그래밍 언어 이론이나 유형 이론 관련 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.

• v
• t