IdrisのFin型
import Data.Fin
有限集合の型
n未満の自然数を許容する型と言ったほうがわかりやすいmrsekut.icon
定義
code:idr
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
例えばFin 5は、
0,1,2,3,4のみを許容する型になる
5以上の自然数は許容しない
自然数以外ももちろん許容しない
code:idr
the (Fin 3) 3 -- type error
the (Fin 3) 2 -- FS (FS FZ)
中身の個数が決まっているVectと組み合わせれば配列の境界検査ができる code:idr
index : Fin n -> Vect n a -> a
index FZ (x :: xs) = x
index (FS k) (x :: xs) = index k xs
code:使う.idr
index 5 1,2,3 -- type error このエラーは、実行時エラーではなく、コンパイルエラーになる！