[%] Indices point between elements

[익명(121.181)]

https://blog.nelhage.com/2015/08/indices-point-between-elements/

[다믜(damhiya)]

"I want to persuade you to replace that image"는 좀 건방지네 ㅋㅋㅋ. alternative view는 일리 있다고 생각함

[다믜(damhiya)]

증명언어 써보면 느낄 수 있는데 저 문제는 진짜 상황따라 다름. "리스트의 원소를 가리키는 인덱스"랑 "리스트를 이분하는 인덱스"는 본질적으로 다르고, 둘 다 필요한 상황이 있음

[다믜(damhiya)]

리스트를 인덱싱해서 원소를 가져오는 함수는 lookup : forall (xs : List A) -> Fin (length xs) -> A 가 어울리고 특정 길이의 prefix를 구하는 함수는 take : forall (xs : List A) -> Fin (1 + length xs) -> List A 를 써야 이쁘게 표현됨

[다믜(damhiya)]

Fin n 은 {0..n-1} 을 원소로 가지는 타입임

[다믜(damhiya)]

dependent type 쓰면 저런 구분이 중요한데, 보통은 Fin (length xs) 든 Fin (1 + length xs) 든 전부 int 로 퉁치니까 저런 생각을 할 일이 드물지

[익명(203.251)]

딜교효율무엇