ハロー、依存型プログラミングの世界 (2)
データ型の宣言
代数データ型を宣言する場合には、Haskellと同様の記法を使うことができる。HaskellでもおなじみのEitherやListの宣言はidrisではこうなっている。
data Either a b = Left a | Right b data List a = Nil | (::) a (List a)
このようなデータ型宣言を行うと、型コンストラクターと値コンストラクターが定義される。Idrisでは型も値だから、型コンストラクターも値コンストラクターも同様に函数として扱われ、大文字小文字関係なく使うことができる。型コンストラクターは型を返す函数であり、値コンストラクターはその型の値を返す函数なので、混同しないように。
Idrisでは一般代数データ型 generalized algebraic data type も宣言できる。例えば次のVectの宣言。
data Vect : Nat -> Type -> Type where Nil : Vect Z a (::) : a -> Vect n a -> Vect (S n) a
暗黙の引数まで明示的に書くと、値コンストラクターの型はそれぞれ Nil : {a : Type} -> Vect Z a, (::) : {a : Type} -> {n : Nat} -> Vect n a -> Vect (S n) a となっている。
自然数
自然数を表すNatは次のように宣言されている。
data Nat = Z | S Nat
Zは0を、Sは後続函数を表してる。Zが0、 S Zが1、S (S Z)が2といった具合。整数からfromInteger函数を使って変換できるので、型が明らかな文脈では単に整数を書いておけば良い。
Idris> Z Z : Nat Idris> S Z 1 : Nat Idris> S (S Z) 2 : Nat Idris> the Nat 100 100 : Nat
有限集合
有限集合を表すFinは次のように宣言されている。
data Fin : Nat -> Type where
fZ : Fin (S k)
fS : Fin k -> Fin (S k)Fin Zという型を持った値は存在しない。
Fin 1、つまりFin (S Z)という型を持った値は、fZ {k=Z}だけだ。
Fin 2という型は、fZ {k=1} と fS {k=1} (fZ {k=Z}))の2つの値を持っている。
つまり、 Fin k という型を持っている値はk個だけなのだ。
実際に例を見てみよう。
Idris> fZ {k=Z}
fZ : Fin 1
Idris> fS {k=1} (fZ {k=Z})
fS (fZ) : Fin 2
Idris> the (Fin 1) fZ
fZ : Fin 1
Idris> the (Fin 1) (fS fZ)
Can't unify Fin (S k) with Fin Z
Specifically:
Can't unify S k with Z
Idris> the (Fin 2) (fS fZ)
fS (fZ) : Fin 2
Idris> the (Fin 2) (fS (fS fZ))
Can't unify Fin (S k) with Fin Z
Specifically:
Can't unify S k with Zこのように、範囲外の値を指定すると型推論が失敗する。
Nat同様、fromInteger函数を使って整数から変換できるので、明らかなら単に整数で書けばよい。
Idris> the (Fin 10) 5 fS (fS (fS (fS (fS (fZ))))) : Fin 10 Idris> the (Fin 10) 10 Can't unify IsJust (Just x) with IsJust (integerToFin 10 (Builtins.fromInteger 10)) Specifically: Can't unify Just x with Nothing
indexとlast
idrisのベクトルの要素をインデックスで指定するときには、index函数を使う。
Idris> :t index Prelude.Vect.index : (Fin n) -> (Vect n a) -> a Idris> index 0 [0, 3, 6, 9] 0 : Integer Idris> index 2 [0, 3, 6, 9] 6 : Integer Idris> index 5 [0, 3, 6, 9] Can't unify IsJust (Just x) with IsJust (integerToFin 5 4) Specifically: Can't unify Just x with natToFin 5 4
インデックスはFin k型の値で指定するので、境界外の値を指定する心配がない。
indexにlastという値を指定することもできる。
Idris> index last [0, 3, 6, 9] 9 : Integer
Prelude.Fin.lastは暗黙の引数をとる函数 last : {n : Nat} -> Fin (S n) で、引数のnは型推論で自動的に決定される。
