존나 어렵긴 한데.. 신기한게 너무 많다.

http://docs.idris-lang.org/en/latest/reference/erasure.html

보통 이런 언어들은 primitive 정수 타입보다 재귀적으로 정의한 자연수를 많이 쓰는데
data Nat = Z | S Nat

효율이 존나 구림.

그런데 보통 이런 데이터 타입은 실제 연산할 때 쓰는게 어니라 theorem proving 용으로 쓰는거라 컴파일할때만 필요하고, 런타임에는 전혀 필요가 없음.

그래서 erasure by usage analysis 라는 방법을 사용하면 마치 하스켈이 컴파일되면 타입이 전혀 남지 않듯이 이런 데이터를 코드에서 통채로 없애버릴 수 있음 ㄷㄷ

가령 Vector (n:Nat) (a:Type) 라는 타입을 정의해서 길이 정보 n은 컴파일 할때만 쓰고 지워버리면 런타임에는 n을 계산 하는 오버헤드가 전혀 없음