こわくない Idris (2) - Ryusei’s Notes (a.k.a. M59のブログ)

ハロー、依存型プログラミングの世界 (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は型推論で自動的に決定される。