이름이 유형이 아닌 종류를 형성하는 이유는 무엇입니까?

Question

몇 시간 전 하스켈 확장 (링크를 찾을 수 없음) 중 하나에서 발생했으며 recently in Ur 이름 (예 : 레코드 필드의 이름)이 종류를 형성한다는 것을 알았습니다. 왜 유형 추상화만으로 충분하지 않은지 설명 할 수 있습니까?

Answer 1

대답은 유형에 나타날 수 있기 때문에 간단합니다. 따라서 유형 수준에서 살아야합니다 (그렇지 않으면 종속 유형이 필요합니다). 그리고 그들은 유형 수준에서 살기 때문에 종류별로 분류됩니다.

Answer 2

레코드 시스템은 값, 유형 및 (어쩌면) 종류에 대한 규칙을 정의합니다. 사용되는 규칙은 설계중인 유형 시스템과 설계자가 달성하고자하는 사항에 따라 다릅니다.

예. 하스켈에서, 음반은 다음과 같습니다

• 값 (접근 기능)
• 그 값은이 유형 (예 : Record -> Int)
• 이러한 유형의 종류 (*)

다른 기록 시스템이 할 수있는 유형 또는 종류의 시스템을 다른 용도로 사용하십시오.

라벨을 별도의 종류로 분류하면 유형 검사기가 라벨을 특수하게 처리 할 수 ​​있습니다. 자동 렌즈, 또는 범용 기능에 맞지 않는 레코드 구성 (전체 성)과 관련된 증명.

하스켈에서 종류 시스템을 사용하는 예는 "박스 화되지 않은 유형"의 사용입니다. 다음은이 유형이 있습니다

일정한 값으로
• 다른 런타임 표현
• 다른 결합 형태 (예를 들어, 힙에 할당 할 수 없음)

정기적으로 혼합에서 언 박싱 유형을 유지하려면 유형에 따라 종류이 주어 지므로 컴파일러는 분리를 추적 할 수 있습니다.

음반사 이름을 표현할 때 다른 종류를 사용해야한다는 것을 의미하는 마술은 없습니다. 언어 디자이너가 Ur-와 같은 의존형 언어로 만들 수있는 선택 일뿐입니다. Twelf, 그것은 유용한 구분 일 수 있습니다.