概要
Idris2の文法についての簡単な覚書になります。
ClaudeでHaskellとの違いに焦点を絞ってロードマップを作成させたものから、いくつかピックアップしてまとめているので、Idris2の全ての文法について解説した記事ではありませんので、ご注意ください。
また、Idris2初心者がまとめた記事になりますので、何か間違いなどがあれば、ご指摘お願いいたします。
Idris2の文法について
文法的にはほとんどHaskellですが、以下の点で大きく異なります。
- 依存型が存在する (型が値に依存する)
- 型駆動開発 (型定義必須)
依存型について
依存型は、型が実際の値に依存するという性質を持つ型システムです。
型チェック時に値の情報を使用します。
依存型の例としてベクトル型があります。
Vect n aの様に記述し、nは要素数、aは要素の型を指定します。
実例として、要素数3のInt型のベクトルは以下の様に定義します。
この場合、実際の値 [1, 2, 3]の要素数が型に情報として含まれています。
import Data.Vect
let vec : Vect 3 Int = [1, 2, 3]
もう少し高度な例としては、ベクトルの計算結果の要素数を指定することもできます。
連結は以下の様に定義でき、結果の型であるVect (n + m) aは要素数がn+mであるa型のベクトルとなります。
append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
通常のHaskellと同様に以下の様に利用できます。
putStrLn $ show $ append [1, 2] [3, 4] -- [1, 2, 3, 4]
型駆動開発について
Idris2の開発は、型シグネチャを起点として実装を開始するので、型駆動開発と呼ばれます。
実際に実行してみるとわかりますが、Haskellの様に実装を書いただけではエラーになります。
必ず型(型シグネチャ)も記述する必要があります。
上記の例のappendを1行目の型シグネチャを記述していない状態で、実行(チェック)すると、以下の様なエラーが出力されます。
Error: No type declaration for Main.append.
hello:5:1--5:18
1 | module Main
2 |
3 | import Data.Vect
4 |
5 | append [] ys = ys
^^^^^^^^^^^^^^^^^
厳密にいうと、一部自動推論が適用されることがあるので、型シグネチャを記載していなくても実行させることはできますが、明示的に定義しておいた方が無難です。
let x1 = 5 -- 自動推論される
let vec1 = [1, 2, 3] -- Data.VectをimportしていなければLisetに自動推論される
add x y = x + y
putStrLn $ show $ add 1 2 -- 自動推論される
putStrLn $ show $ add 1.0 2.0 -- エラー
let res : Double = add 1.0 2.0
putStrLn $ show res -- OK
全域関数と部分関数
Idris2では全域関数(total, covering)と部分関数(partial)を明示的にアノテーションできます。
未指定の場合はcoveringとなりますが、下表の通り停止性が保証されないので、基本的にはtotalを目指して実装することになります。
| アノテーション | 網羅性 | 停止性 |
|---|---|---|
| total | ◯ | ◯ |
| covering | ◯ | ✗ |
| partial | ✗ | ✗ |
Vectは長さ情報を持つので、以下の様に、網羅性と停止性を持つように定義できます。
total
headVect : Vect (S n) a -> a
headVect (x :: xs) = x
Listで同様に定義しようとすると、partialになります。
※ partial関数を呼び出す際には、呼び出し元もpartialにする必要があるので注意してください
partial
headList : List a -> a
headList (x :: xs) = x
上記の処理は、空リストのケースを考慮していないため、partialとなっています。
totalにする場合は、MaybeやEitherなどを利用して、空リストのケースについて明示的に対応する必要があります。
total
headListMaybe : List a -> Maybe a
headListMaybe [] = Nothing
headListMaybe (x :: xs) = Just x
coveringでなければならないケースは殆どないはずなので、基本的にはtotalかpartialのどちらかに倒してください。
totalではなく、純粋なcoveringの実例として、以下のような定義が考えられますが、停止性が保証されておらず、実行すると無限ループになります。
someFunction : Int -> Int
someFunction n = someFunction (n - 1)
Interface
以下はNatにSortable Interfaceを追加した例になります。
Named Interfaceとしてdescendingを追加しているので、逆順にも対応しています。
interface Sortable a where
compare : a -> a -> Ordering
Sortable Nat where
compare x y =
if x < y then LT
else if x > y then GT
else EQ
[descending] Sortable Nat where
compare x y =
if x > y then LT
else if x < y then GT
else EQ
sortBySortable : Sortable a => List a -> List a
sortBySortable [] = []
sortBySortable (x :: xs) =
let smaller = sortBySortable (filter (\y => compare y x == LT) xs)
larger = sortBySortable (filter (\y => compare y x /= LT) xs)
in smaller ++ [x] ++ larger
main : IO ()
main = do
let xs : List Nat = [1, 5, 2]
putStrLn $ show $ sortBySortable xs
putStrLn $ show $ sortBySortable @{descending} xs
モジュール管理＆アクセス修飾子
モジュール名は以下の様に、フォルダ名とファイル名をドットで繋いだものにします。
project/
Math/
Basic.idr -- module Math.Basic
Advanced.idr -- module Math.Advanced
Main.idr -- module Main（デフォルト）
各モジュールに定義された関数や型などは、デフォルトでprivateなので、外部公開する場合は、用途に応じて以下のアクセス修飾子に変更します。
-
private: 型も定義も公開しない -
export: 型のみ公開 (型抽象) -
public export: 型と定義を公開
以下は各修飾子を利用した実例です。
ライブラリ側のコード (`AccessorLibrary/Library.idr`)
private
data PrivateNumber = MkPrivateNumber Int
private
Show PrivateNumber where
show (MkPrivateNumber n) = show n
private
makePrivateNumber : Int -> PrivateNumber
makePrivateNumber n = MkPrivateNumber n
export
data ExportedNumber = MkExportedNumber Int
export
Show ExportedNumber where
show (MkExportedNumber n) = show n
export
makeExportedNumber : Int -> ExportedNumber
makeExportedNumber n = MkExportedNumber n
public export
data PublicExportedNumber = MkPublicExportedNumber Int
public export
Show PublicExportedNumber where
show (MkPublicExportedNumber n) = show n
public export
makePublicExportedNumber : Int -> PublicExportedNumber
makePublicExportedNumber n = MkPublicExportedNumber n
呼び出し側のコード(`Main.idr`)
import AccessorLibrary.Library
main : IO ()
main = do
-- let n1 = MkPrivateNumber 1 -- privateなので参照できない
-- putStrLn $ show $ makePrivateNumber 1 -- privateなので参照できない
-- let n2 = MkExportedNumber 1 -- exportなので実装は参照できない
putStrLn $ show $ makeExportedNumber 2
let n3 = MkPublicExportedNumber 3
putStrLn $ show $ n3
putStrLn "OK"
with
Haskellに存在しないwithが利用できます。
以下のような構造になっています。
function : (args) -> ReturnType
function args with (expression)
function pattern1 | result1 = body1
function pattern2 | result2 = body2
以下の例は、引数のリストの各要素が偶数か判定するものです。
allEven : List Int -> Bool
allEven [] = True
allEven (x :: xs) with (x `mod` 2 == 0, allEven xs)
allEven (x :: xs) | (True, True) = True
allEven (x :: xs) | (True, False) = False
allEven (x :: xs) | (False, _) = False
この場合、パターンの部分は、以下の様に省略して書けます。
allEven : List Int -> Bool
allEven [] = True
allEven (x :: xs) with (x `mod` 2 == 0, allEven xs)
_ | (True, True) = True
_ | (True, False) = False
_ | (False, _) = False
expression部分に渡すデータを整形して処理したい場合があります。
以下のケースでは、元データを逆順にソートとしてから処理を行っています。
Idris2では、このデータ整形のことをViewと言っているようです。
Viewを利用した例
data ReverseView : List a -> Type where
Nil : ReverseView []
Append : (xs : List a) -> (x : a) -> ReverseView (xs ++ [x])
reverseView : (xs : List a) -> ReverseView xs
reverseView [] = Nil
reverseView (x :: xs) =
case reverseView xs of
Nil => Append [] x
Append ys y => Append (x :: ys) y
searchFromLast : (xs : List a) -> (a -> Bool) -> Maybe a
searchFromLast xs p with (reverseView xs)
searchFromLast [] p | Nil = Nothing
searchFromLast _ p | Append ys x =
if p x then Just x else searchFromLast ys p
main : IO ()
main = do
putStrLn $ show $ searchFromLast [1, 2, 3, 4, 5] (\x => x `mod` 2 == 0)