종류 이론의 모든 인스턴스의 공통 상위 유형은 무엇입니까

Question

OWL 또는 Topic Maps로 정의 할 수있는 것과 같이 List [T]와 같은 다형성 유형에 대한 지원을 포함하는 온톨로지를 설계하려고합니다. 여기서 T는 Interval Kind In (Nothing, Any)의 type 매개 변수이며 Function Kind * -> *입니다. 궁극적으로 필자는 동일한 의미 언어로 작성된 유형 안전 소프트웨어 코드의 기초가 될 수있는 충분한 세부 묘사와 엄격한 의미 론적 언어로 유형 시스템 온톨로지를 설명하려고합니다.

이 목표를 염두에두고 유형, 간격 유형 및 기능 유형이 모두 Kind의 인스턴스 인 계층 구조를 파악하려고합니다. 모든 종류의 공통 '초 (superkind)'에 대한 공식적인 이름이 있습니까? 내가 생각할 수있는 가장 좋은 용어는 'Kind Instance'입니다. 이것은 심지어 타입 이론에서 의미있는 개념입니까? 그렇지 않은 경우에도 (토픽 맵 용어에서와 같은) 말하기에는 개념이 필요합니다. "function-argument-type-constraint 연관에는 역할 'allowed-type'이 있습니다.이 플레이어의 유형은 'Kind Instance ''.

이 외에도 저는이 프로젝트의 형식 이론을 가르치기 시작했으며 완료하기 전에 더 많은 것을 배워야합니다. 필자는 Higher Kind의 Generics (http://adriaanm.github.com/files/higher.pdf)를 포함하여 유형 이론에 대한 몇 가지 스칼라 관련 문서를 읽었으며 스칼라에서 Safe Type-Level Abstraction을 통해 작업을 시작했습니다. http://adriaanm.github.com/files/scalina-final.pdf) 및 Type Constructor Polymorphism for Scala[pdf]. 스칼라보다 하스켈에 대해 잘 알지 못하지만 System F with Type Equality Coercions[pdf]과 같은 관련성이 높은 몇 가지 논문이 나왔습니다. 이해하기 위해서는 하스켈에 대해 훨씬 더 깊이 이해해야합니다. 초보자 수준에서 시작하여 일반화 된 대수 데이터 형식과 같은 고급 원칙에 이르기까지 하스켈 형식 시스템을 학습하기위한 자료를 읽는 사람이 있다면 그 정보를 얻을 수 있습니다. 당신은 OWL 또는 토픽 맵과 같은 의미 온톨로지 언어의 유형 시스템을 설명하는 기존의 시도를 알고있는 경우이 작업을 수행하는 방법에 대한 어떤 제안이있는 경우

마지막으로, 또는 너무 듣고 싶어요.

Answer 1

벤자민 피어스 (Benjamin Pierce)의 "Types and Programming Languages"보다 형식 이론에 대한 소개가 없습니다. 위의 레벨에는 표준화 된 이름이 있다고 생각하지 않지만 "정렬"은 하나의 공통된 선택입니다. 또 다른 일반적인 선택은 종속 형식으로 바로 이동하고 계층 구조를 병합하여 결국 단 하나의 수준이되도록하는 것입니다. 이 상황에서 추가 할 공통적 인 타이핑 규칙 (논리적 인 내용이 대개 중요하지 않은 일상적인 프로그래밍 언어를 다룰 때)은 "Type : Type"규칙이므로 3 : Int : Type : 유형 : 유형 : ...