Vect n a 에서 n은 value level이지만 어차피 필요없으니까 걍 지운다고 하는데, 그럴꺼면 n이 value level이든 type level이든 상관 없지 않음?
물론 n을 사용하면 안지우고 진짜 런타임에 평가한다는것 같은데
dependent type이 꼭 필요한 경우는 n이 컴파일 타임에도 필요하고 런타임에도 필요할때만 의미가 있는것 같은데..
Vect n a 에서 n은 value level이지만 어차피 필요없으니까 걍 지운다고 하는데, 그럴꺼면 n이 value level이든 type level이든 상관 없지 않음?
물론 n을 사용하면 안지우고 진짜 런타임에 평가한다는것 같은데
dependent type이 꼭 필요한 경우는 n이 컴파일 타임에도 필요하고 런타임에도 필요할때만 의미가 있는것 같은데..
인덱스 범위체크 타입레벨에서 하는거 보여주셈
안되나.. 사실 제대로 아는게 없어서 머리가 뒤죽박죽임 ㅋㅋㅋㅋ
근데 저기서 n이 Nat타입이고 인덱스는 Int 라서 어차피 idris에서는 범위체크 효율적으로 하기 힘들것 같은데
어떻게 구현되있나 한번 찾아봐야겠다
안되는걸 약팔았누
ㄴㄴ 되긴 되는데 Int타입으로는 안될껄
찾아보니까 n미만의 자연수 타입을 정의해서 그 타입의 원소만 입력으로 받네
근데 애초에 Vect 타입이 다른 언어랑 다르게 그냥 길이 정해진 리스트임 ㅋㅋㅋㅋ 그니까 접근시간 O(n)이야