Idrisで依存型に触れる

Haskellで同時に書いてみると依存型の威力がわかりやすいmrsekut.icon

忘れてるときはIdrisの型と合わせて読むと良いかも知れない

関数の引数に型を取れる

code:idr(hs)

Idris> :t the

the : (a : Type) -> a -> a

↑このthe関数は、第1引数は値ではなく型である

型宣言に関数を書ける ref

code: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

code:定義.idr(hs)

(++) : Vect n a -> Vect m a -> Vect (n + m) a -- 型宣言内で加算

(++) Nil ys = ys

(++) (x :: xs) ys = x :: (xs ++ ys)

code:実行.idr(hs)

xs : Vect 5 Int

ys : Vect 3 Int

xs ++ ys -- > 1, 2, 3, 4, 5, 6, 7, 8 : Vect 8 Int

こういう要素数を型内演算で表現するのって動的にはどうするんだ？

入力で2つのVect型を受け入れるときとか

普通に肩検査するのかmrsekut.icon

Vectの要素にアクセスする関数index

引数にFinとVectを使って定義されている

code:idr(hs)

index : Fin n -> Vect n a -> a

この定義内のnはNatのみを許容するがこの宣言だけでは明示されていない

これはFin(やVect)の型定義から推論できるのでわざわざ書かなくていい