5
Type 1 인 주민의 예가 Type도 아니고 주민 번호가 Type도 아닌가? Idris REPL에서 탐험을하면서 나는 무엇이든 올 수 없었다.`Type`도 아니고`Type '의 주민이 아닌`Type1`의 예
가 더 정확하게하려면 , 나는 다음과 같은 산출이 Type 이외의 x을 찾고 있어요 :
Idris> :t x
x : Type 1
A
답변
5
내가 이드리스 전문가는 아니지만 기대했던 그
Type -> Type
도 Type 1입니다.
또한
Nat -> Type
을 기대하고 (이 일에 대해 확신하지 않음) 매우 운이 좋다면
List Type
큰 것을 할 수 있습니다.
아이디어는 모든 수준에서 모든 유형 구축 작업을 수행 할 수 있다는 것입니다. 한 레벨에서 유형을 값으로 사용할 때마다 유형의 해당 구조가 한 레벨 위로 올라갑니다.
7
저는 형식 이론 전문가가 아니지만 여기에 제 이해가 있습니다. Idris tutorial에는 12.8 Cumulativity 섹션이 있습니다.
Type : Type 1 : Type 2 : Type 3 : ...
그리고 어떤 x : Type n에 대한
m > n에 대한
x : Type m을 의미 :이 유형의 우주의 내부 계층 구조가 있다고 말한다. 또한 유형 유추에서 가능한 사이클을 방지하는 방법을 보여주는 예제가 있습니다.
그러나이 계층 구조는 내부 용도로만 사용되며 Type (n+1) 값을 만들 가능성이 없습니다.이 값은 Type n이 아닙니다.
약 nlab 약 universes in type theory 및 약 type of types에 대한 기사도 참조하십시오.
idris-dev 저장소의 issue도 유용 할 수 있습니다. Edwin Brady는 Design and Implementation paper을 참조합니다 (3.2.2 절 참조).
'Type -> Type : Type' –
Idris가 프로그래머에게'Type' 레벨에 대한 정보를 너무 많이 드러내고 있는지 확신하지 못합니다. 'Type : Type 1'은 아마도'Type : Type'이 모순이기 때문일 것입니다. –
'Type -> Type'은 실제로 'Type 1'이지만,'Type'에도 있습니다 (Ramon이 지적한대로). 'Nat -> Type '과'List Type'도 마찬가지입니다. – Snowball