Agda에서 어떤 크기의 유형이 있습니까?

Question

Agda에서 어떤 크기의 유형이 있습니까? MiniAgda에 대한 논문을 읽으려고했으나 다음과 같은 이유로 진행하지 못했습니다.

1. 왜 데이터 형식이 그 크기보다 일반적입니까? 내가 아는 한 크기는 유도 나무의 깊이입니다.
2. 왜 데이터 유형이 크기에 대해 공분합니다 (예 : < = j -> T_i < = T_j?
3. > 및 # 패턴의 의미는 무엇입니까?

Answer 1

1. 생각은 크기 유형은 기본적으로 서수 있습니다 크기에 의해 색인 유형, 단지 가족이라는 것이다. 귀납적 유형을 sized data으로 정의하면 컴파일러는 결과가 올바른 크기의 유형인지 확인하여 예를 들어 이 SNat이면 크기가 1로 커집니다. 그런 식으로 크기가 지정된 경우 S(i : Size) -> S i은 본질적으로 요소입니다 크기가 i 인 S입니다. 나에게 이상하게 보이는 이유는 SNat에 대한 0의 정의가 zero : (i : Size) -> SNat ($ 0) 대신에 zero : (i : Size) -> SNat ($ i) 인 이유입니다. T_i가 미만 크기 I T와 원소의 종류, 크기대로 유도 유형의
2. 이 말이 그래서 다음 T_i ≤ T_j J 하로하는 경우; 생성자는 재귀 호출의 크기를 늘려야합니다.

3. 2.3 절에서 설명했듯이 #은 T_∞와 같으며 알려진 크기의 바인드가없는 T의 요소 유형입니다. 이것은 subtyping preorder의 T_i의 최상위 요소입니다. 패턴 (i> j)은 j가 j 정보를 유지하면서 크기 j를 바인드하는 데 사용됩니다. < i. 마이너스의 용지의 예는이 명확하게 :

   fun minus : [i : Size] -> SNat i -> SNat # -> SNat i 
   { minus i (zero (i > j)) y = zero j 
   ; minus i x (zero .#) = x 
   ; minus i (succ (i > j) x) (succ .# y) = minus j x y 
   } 
   

   먼저 서명은 임의의 숫자 substracting 내가 (그 무엇 SNat i 수단의 대부분에서 크기의 수에서 (SNat #하는 어떤 크기의 바인딩 정보와 함께 숫자입니다)을 의미) 대부분 i 크기의 숫자를 반환합니다. > 패턴의 경우 마지막 줄에서 크기가 최대 인 j 개의 숫자를 일치시키는 데 사용하고 하위 유형 지정의 경우 재귀 호출 유형 검사 인 SNat j ≤ SNat i을 사용합니다.