증명 언어에서 Fin 타입 사용이 좀 피곤하다고 생각이 듬.

Fin n타입은 n보다 작은 자연수 타입 (즉 원소 갯수가 n인 타입)인데

보통 다음처럼 정의함.

data Nat : Set where zero : Nat suc : Nat -> Nat data Fin (n : Nat) : Set where fzero : Fin (suc n) fsuc : Fin n -> Fin (suc n)


이런 타입의 특징은 패턴매칭을 해서 구조를 분해하면 타입이 바뀐다는 점임.

무슨말이냐면 Nat의 경우

n : Nat suc n : Nat

이지만 Fin은

n : Fin a fsuc n : Fin (suc a)

처럼 n과 fsuc n 의 타입이 다름


만약 Fin a 타입을 Fin (suc a) 로 리프팅을 하고싶으면 inject : Fin a -> Fin (suc a) 를 사용해야함.

Fin a를 Fin (suc a) 로 변환해주는 단사함수임. 원소 갯수가 많은 타입으로 가는 거니까 마지막 자리가 하나 비게 됨.


이제 재귀를 하면 일반적으로 f (suc n) 을 f n 을 사용해서 정의하게 되는데, Nat은 그냥 하면 되지만 Fin은 선택지가 두가지 있음

f (fsuc n : Fin (suc a))을 f (n : Fin a) 에 대해 정의하면 polymorphic recursion을 하게 됨. 이게 편한경우에는 그냥 이대로 하면 됨.

근데 다형 재귀를 하고싶지 않은경우, f (fsuc n : Fin a)를 f (inject n :Fin a)로 정의하고 싶을수도 있음.

이경우에는 termination checking이 어려움. 저런식으로 코드를 짜면 Agda 가 저게 종료한다는걸 인식을 못함.

termination checker가 inject가 무슨함수인지까지 고려해주지는 못하거든.


그래서 내 생각에는 polymorphic recursion을 피하고 싶은경우에는 Fin a 보다는 (n : Nat, n < a) 를 쓰는게 나은것 같음.

Nat을 쓰면 inject가 필요가 없어지니까.