Idrisで依存型に触れる
Haskellで同時に書いてみると依存型の威力がわかりやすい
忘れてるときはIdrisの型と合わせて読むと良いかも知れない
関数の引数に型を取れる
idr(hs)Idris> :t the
the : (a : Type) -> a -> a↑このthe関数は、第1引数は値ではなく型である
型宣言に関数を書ける ref
idr(hs)-- 型を返す関数を定義
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
sum : (single : Bool) -> isSingleton single -> Nat -- 型宣言に関数を使用
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs single は値ここでは
Bool 型の値 single の値によって、第2引数が要請する型が変わる型宣言で自然数演算ができる
Vect同士を連結する関数 ref
定義.idr(hs)(++) : Vect n a -> Vect m a -> Vect (n + m) a -- 型宣言内で加算
(++) Nil ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)実行.idr(hs)xs : Vect 5 Int
xs = [1,2,3,4,5]
ys : Vect 3 Int
ys = [6,7,8]
xs ++ ys -- > [1, 2, 3, 4, 5, 6, 7, 8] : Vect 8 Intこういう要素数を型内演算で表現するのって動的にはどうするんだ？
入力で2つのVect型を受け入れるときとか
普通に肩検査するのか
Vectの要素にアクセスする関数index
引数にFinとVectを使って定義されている
idr(hs)index : Fin n -> Vect n a -> aこの定義内の
n は Nat のみを許容するがこの宣言だけでは明示されていないこれは
Fin (や Vect )の型定義から推論できるのでわざわざ書かなくていい