Idris2のTips
内容としては前回の続きです。
Idris2で色々実装をしていくにあたって、得られた知見をTipsとしてまとめます。
where句における関数定義
where句で定義する関数は推論できない場合は、型指定が必要です。
以下はバブルソートの例ですが、goの型シグネチャを指定しないとエラーになります。
bubbleSort : Ord a => List a -> List a
bubbleSort xs =
if xs == go xs
then xs
else bubbleSort (go xs)
where
go : List a -> List a
go [] = []
go [x] = [x]
go (x :: y :: ys) =
if x <= y
then x :: go (y :: ys)
else y :: go (x :: ys)
以下のような変数定義であれば、型シグネチャは不要です。
putStrLn $ show x
where x = [10, 20]
関数出会っても以下のような簡単な例の場合は、型シグネチャの定義は不要です。
putStrLn $ show (succ 10)
where succ : Int -> Int
succ y = y + 1
derivingが存在しない
Idris2には、Haskellのようなderivingによる自動実装がありません。
Show, Eq, Ordなどは、自分で実装する必要があります。
Haskellでは以下のような自動実装が可能です。
data Number = One | Two | Three deriving (Show, Eq, Ord)
Idris2にはderivingがないので、以下の様に自前で実装する必要がある。
Show Number where
show One = "One"
show Two = "Two"
show Three = "Three"
Eq Number where
One == One = True
Two == Two = True
Three == Three = True
_ == _ = False
Ord Number where
compare One One = EQ
compare One Two = LT
compare One Three = LT
compare Two One = GT
compare Two Two = EQ
compare Two Three = LT
compare Three One = GT
compare Three Two = GT
compare Three Three = EQ
データ型の明示的な指定
データ型の定義を行う場合、Haskellと同様に以下のように定義を行います。
data Point = MkPoint Int Int | MkPoint0
Idris2の場合、明示的に型シグネチャを指定できるので、以下の様にも書くことができます。
data Point : Type where
MkPoint : Int -> Int -> Point
MkPoint0 : Point
レコード
Haskellのフィールド名付きデータ型は、以下の様に定義しますが、Idris2ではrecordを利用して定義します。
Haskellにおける定義
data Point = MkPoint { x :: Int, y :: Int }
Idris2における定義
record Point where
constructor MkPoint
x : Int
y : Int
constructorは1つしか定義できない点に注意してください。
文字列の分割について
文字列の分割は Data.String.split で行えますが、戻り型が List1 であるので注意してください。
Listはimportせずに利用可能ですが、List1はimportが必要です。
以下は文字列をカンマで分割する簡単な例になりますが、結果を通常のListで扱いたい場合は、以下の様に変換処理を入れる必要があります。
import Data.String
import Data.List1
-- List1をListに変換
fromList1 : List1 a -> List a
fromList1 (x ::: xs) = x :: xs
-- 文字列をカンマで分割
splitFields : String -> List String
splitFields s = fromList1 (Data.String.split (== ',') s)
また、List1は要素が1以上であることを強制する型なので、初期化する場合は、通常のリストとは異なり、以下の様にします。
一からリストを生成するケース
let xs1 = singleton 1
putStrLn $ show $ xs2 -- [1]
Listから変換するケース
let ys1 : List Int = [1, 2, 3]
ys2 : List Int = []
putStrLn $ show $ ys1
case fromList ys1 of
Just xs => putStrLn $ show $ xs -- ★ こっちが呼ばれる
Nothing => putStrLn "Conversion failed"
case fromList ys2 of
Just xs => putStrLn $ show $ xs
Nothing => putStrLn "Conversion failed" -- ★ こっちが呼ばれる
演算子や関数の競合
現在のIdris2 (0.8.0)では、モジュールから部分的に関数をimportする文法がないようです。
Data.String をimportすると、AsListの::と競合するので、以下の様に定義するとエラーになってしまいます。
import Data.String
test : IO ()
let xs = [1, 2, 3]
putStrLn $ show xs
解決するには、以下の様に正確に型シグネチャを書けばOKです。
import Data.String
test : IO ()
let xs : List Int = [1, 2, 3] -- 定義時に型シグネチャを指定する
putStrLn $ show xs
この様に、Idris2の場合、importを追加しただけで、曖昧さからビルド時にエラーになる可能性があるので、型シグネチャは正確に記述しておいた方が良いです。
ちなみに、以下のチュートリアルページには、withなどが利用できるとありますが、GitHubのコードを検索してもヒットしなかったのでおそらくないと思われます。
要素取得
Haskellの場合は!!という演算子が利用できますが、Idris2には存在しないのでindexを代わりに利用する必要があります。
Haskellでは以下の様に要素を取得できます
let xs = [1, 2, 3]
putStrLn $ show $ xs !! 0 -- 1
Idris2では以下の様に要素を取得します。
let xs : Vect 3 Int = [1, 2, 3]
putStrLn $ show $ index 0 xs -- 1
依存型を引数にとる際の暗黙的な型パラメータ
Vectのような依存型で、型パラメータ(Vectの場合はサイズ)を関数本体で利用する場合は、implicitで定義しておく必要があります。
以下のケースでは、実装部分でm, nを利用していないので、型パラメータを定義する必要はありません。
ShowVectSize : Num a => Vect (S m) (Vect n a) -> String
ShowVectSize v = show (length v) ++ "x" ++ show (length (index 0 v))
以下のケースでは、実装部分でm, nを利用しているので、型パラメータ({m : Nat}, {n : Nat})の定義が必要になります。
ShowVectSize : {m : Nat} -> {n : Nat} -> Num a => Vect (S m) (Vect n a) -> String
ShowVectSize v = show (S m) ++ "x" ++ show n