インターフェース
March 30, 2025 · View on GitHub
関数オーバーロード - つまり同名異実装な関数定義 - は多くのプログラミング言語で見られる概念です。 Idrisには関数のオーバーロードが備わっています。 つまり、同名の2つの関数は異なるモジュールや名前空間で定義でき、Idrisは型をもとに曖昧さを解消しようとします。 例はこちら。
module Tutorial.Interfaces
%default total
namespace Bool
export
size : Bool -> Integer
size True = 1
size False = 0
namespace Integer
export
size : Integer -> Integer
size = id
namespace List
export
size : List a -> Integer
size = cast . length
ここではsizeという名前の相異なる関数を名前空間で個別に定義しました。
これらの曖昧さを解消するにはそれぞれの名前空間を前置すればよいです。
Tutorial.Interfaces> :t Bool.size
Tutorial.Interfaces.Bool.size : Bool -> Integer
しかし、大抵は必要ありません。
mean : List Integer -> Integer
mean xs = sum xs `div` size xs
見ての通りIdrisは相異なるsize関数の曖昧さを解消できていることがわかります。
xsは型List Integerであり、この型はList aにのみ統合できるので、List aが引数の型であるList.sizeが選ばれます。
インターフェースの基本
関数オーバーロードは上述したようにいい感じに動くものの、こうした関数オーバーロードの形式だと沢山のコードの重複に繋がるような用例があります。
例として、関数cmpを考えてみましょう(compareを縮めたもので、既にPreludeから公開されています)。
この関数は型Stringの値の序列を表現するものとします。
cmp : String -> String -> Ordering
似たような関数は沢山の他のデータ型についても欲しいです。
これだけだったら関数オーバーロードでいいですが、cmpの機能性ははそれだけに留まりません。
この関数があればgreaterThan, lessThan, minimum, maximumやその他諸々の関数を導出できます。
lessThan' : String -> String -> Bool
lessThan' s1 s2 = LT == cmp s1 s2
greaterThan' : String -> String -> Bool
greaterThan' s1 s2 = GT == cmp s1 s2
minimum' : String -> String -> String
minimum' s1 s2 =
case cmp s1 s2 of
LT => s1
_ => s2
maximum' : String -> String -> String
maximum' s1 s2 =
case cmp s1 s2 of
GT => s1
_ => s2
これら全てをcmp関数を使って他の型について実装し直さなくてはなりません。
それにこれらの実装は、全てではないにしても、上に書いたものと同じになります。
そうなるとコードの重複が沢山出てきます。
1つの方法として高階関数を使うという手があります。
例えば、関数minimumByを定義するとしましょう。
この関数は最初の引数に比較関数を取り、残りの2つの引数のうち、より小さいほうを返します。
minimumBy : (a -> a -> Ordering) -> a -> a -> a
minimumBy f a1 a2 =
case f a1 a2 of
LT => a1
_ => a2
この解決策は高階関数があればコードの重複を減らせることの傍証になっています。 しかしながら、いつも比較関数を持ち回らなければいけないのは億劫です。 この例での比較関数のようなものをIdris自ら思い出せるようになってくれるといいですね。
インターフェースはまさにこの問題を解消するものです。 こちらが例です。
interface Comp a where
comp : a -> a -> Ordering
implementation Comp Bits8 where
comp = compare
implementation Comp Bits16 where
comp = compare
上記のコードはインターフェースCompを定義し、
型aの2つの値の序列を計算するための関数compを提供しています。
これにさらにこのインターフェースについての型Bits8とBits16のための2つの実装が続きます。
ただしimplementationキーワードはあってもなくてもよいです。
Bits8とBits16のためのcompの実装では両方とも関数compareが使われています。
この関数はPreludeの似たようなインターフェースであるOrdの一部です。
次にcompの型をREPLで見てみます。
Tutorial.Interfaces> :t comp
Tutorial.Interfaces.comp : Comp a => a -> a -> Ordering
compの型処方の興味深い部分は最初の引数Comp a =>です。
ここでCompは型変数aの制約です。
この処方は、「あらゆる型a、ただしインターフェースCompの実装があるもの、については型aの2つの値を比較でき、それらのOrderingを返す」のようにに読めます。
compをどんなもので呼び出そうとも、Idris自らComp aであるような型の値を思い付いてくれます。
そう、新しい矢印=>があればね。
もしIdrisがこれに失敗するなら、それは型エラーです。
これにてcompを関係する関数の実装に使えます。
やらなければいけないことは以下の導出される関数にComp制約を前置することだけです。
lessThan : Comp a => a -> a -> Bool
lessThan s1 s2 = LT == comp s1 s2
greaterThan : Comp a => a -> a -> Bool
greaterThan s1 s2 = GT == comp s1 s2
minimum : Comp a => a -> a -> a
minimum s1 s2 =
case comp s1 s2 of
LT => s1
_ => s2
maximum : Comp a => a -> a -> a
maximum s1 s2 =
case comp s1 s2 of
GT => s1
_ => s2
minimumの定義はminimumByと瓜二つですね。
強いて違うところを挙げるとすれば、minimumByの場合は比較関数を明示的な引数として渡さねばならないところ、minimumはCompの実装の一部で提供されているのでIdrisが代わりに渡してくれることです。
したがって以上のユーティリティ関数を一度定義してしまえば、インターフェースCompの実装がある全ての型に適用できます。
演習 その1
-
関数
anyLargerを実装してください。 この関数は、値のリストが与えられた参照値より大きい要素を少なくとも1つ含んでいるときに限りTrueを返します。 インターフェースCompを実装で使ってください。 -
関数
allLargerを実装してください。 この関数は、値のリストが与えられた参照値より大きい要素のみを含んでいるときに限りTrueを返します。 ここで、自明な場合である空リストについては真になります。 インターフェースCompを実装で使ってください。 -
関数
maxElemを実装してください。 この関数はCompの実装を使って値のリストから最も大きい要素を抽出しようとします。minElemも同様にしてください。 この関数は最も小さい要素を抽出しようとするものです。 出力の型を決めるときは、リストが空になる可能性があることを考慮しなくてはいけませんよ。 -
リストや文字列のような連結できる値のためのインターフェース
Concatを定義してください。 リストと文字列向けの実装を提供してください。 -
Concatの実装が備わる値を持つリスト中の値を連結する関数concatListを実装してください。 リストが空になる可能性があることを出力の型に反映してくださいね。
もっとインターフェース
先の節ではごく基本的なインターフェースを学びました。 便利な理由と定義して実装する方法についてです。 この節では少しだけ発展的な概念を学びます。 インターフェースを拡張すること、制約付きのインターフェース、既定実装です。
インターフェースを拡張する
階層をなすインターフェースがあります。
例えば演習4で使ったConcatインターフェースについては、Emptyという名前の子インターフェースがあってもいいでしょう。
このインターフェースを満たすような型には、連結の際に何の効果も生じない値があります。
そのような場合、Concatの実装をEmptyの実装の必要条件にできます。
interface Concat a where
concat : a -> a -> a
implementation Concat String where
concat = (++)
interface Concat a => Empty a where
empty : a
implementation Empty String where
empty = ""
Concat a => Empty aは「Concatの型aのための実装は、aに対してEmptyの実装をするための必要条件である」のように読めます。
しかしこれは、インターフェースEmptyの実装があるならば、常にConcatの実装がなくてはならず、
いつでもConcatにある関数を呼び出すことができる、という意味でもあるのです。
concatListE : Empty a => List a -> a
concatListE [] = empty
concatListE (x :: xs) = concat x (concatListE xs)
concatListEの型でEmpty制約だけを使っているにも関わらず、実装でemptyとconcatの両方を呼び出せていますね。
制約付きの実装
ときに、ある汎化型のインターフェースを実装できるのが、その型変数がこのインターフェースを実装しているときだけ、ということがあります。
例えばインターフェースCompをMaybe aに実装するのが可能なのは、型a自体がCompを実装しているときだけです。
インターフェースの実装に制約を課すのは、制約付きの関数で使ったのと同じ文法でできます。
implementation Comp a => Comp (Maybe a) where
comp Nothing Nothing = EQ
comp (Just _) Nothing = GT
comp Nothing (Just _) = LT
comp (Just x) (Just y) = comp x y
文法がよく似てはいますが、これはインターフェースを拡張することとは同じではありません。
制約は型変数に課されていて、型全体ではないですね。
Comp (Maybe a)の実装の最後の行では2つのJustに格納された値を比較します。
これが可能となるのは、これらの値にもCompの実装があるときだけです。
さあ、上記の実装からComp a制約を消去してみましょう。
Idrisの型エラーを読み解くことは、修正するときに大事になります。
幸いにもIdrisはこれら全ての制約を代わりに解いてくれます。
maxTest : Maybe Bits8 -> Ordering
maxTest = comp (Just 12)
ここでIdrisはComp (Maybe Bits8)の実装を見付け出そうとします。
そのためにはComp Bits8用の実装が必要です。
さあさあmaxIntの型にあるBits8をBits64に変えてみましょう。
どんなエラー文言をIdrisは出すでしょうか。
既定実装
ときどき、幾つかの関係する関数を1つのインターフェースに収めて、そのインターフェースにある関数を使うことができながらも、プログラマがそれぞれの関数を最も効率的に動くように実装できるようにしたいことがあります。
例えば2つの値の等値性で比較するインターフェースEqualsを考えましょう。
このインターフェースには2つの値が等しいときTrueを返す関数eqと、等しくないときにTrueを返すneqがあります。
もちろんneqはeqを使って実装できますし、ほとんどの場合でEqualsを実装するときはeqのみを実装すればよいでしょう。
この場合、neqの実装をEqualsの定義中に含めてしまうことができます。
interface Equals a where
eq : a -> a -> Bool
neq : a -> a -> Bool
neq a1 a2 = not (eq a1 a2)
Equalsの実装でeqのみ実装した場合は、
Idrisは上記のneqの既定実装を使うことになります。
Equals String where
eq = (==)
他方で両方の関数に陽に実装を提供したければそれもできます。
Equals Bool where
eq True True = True
eq False False = True
eq _ _ = False
neq True False = True
neq False True = True
neq _ _ = False
演習 その2
-
インターフェース
Equals,Comp,Concat,Emptyを対(2つ組タプル)に実装してください。 実装では必要に応じて制約を課して構いません(関数の引数と同様に、複数の制約を連続して課すことができます。 例えばComp a => Comp b => Comp (a,b)です)。 -
以下は2分木の実装です。 インターフェース
EqualsとConcatをこの型に実装してください。data Tree : Type -> Type where Leaf : a -> Tree a Node : Tree a -> Tree a -> Tree a
Preludeにあるインターフェース
IdrisのPreludeはインターフェースと実装を幾つか提供しています。 これらはほぼ全てのある程度以上のプログラムで便利です。 基本的なものをここで紹介します。 より発展的なものは後の章でお話ししましょう。
これらのインターフェースのほとんどは数学的な法則に関連します。 そして、実装はこれらの法則に従うことになっています。 法則についてもここで触れます。
Eq
おそらく最も使われているインターフェースはEqでしょう。
これは前述の例で使ったインターフェースEqualに対応します。
eqとneqの代わりに、Eqは2つの演算子(==)と(/=)を提供し、
2つの同じ型の値について等しいか異なるかを比べられます。
Preludeで定義されているほとんどのデータ型はEqの実装付きですし、
プログラマが自前のデータ型を作るときも最初に実装するインターフェースでしょう。
Eqの法則
Eqの全ての実装について以下の法則を満たすようにしてください。
-
(==)は反射的です。x == x = Trueが全てのxについて成り立ちます。 つまり、全ての値はそれ自身と等しいです。 -
(==)は対称的です。x == y = y == xが全てのxとyについて成り立ちます。 つまり、(==)の引数の順序は重要ではありません。 -
(==)は推移的です。x == y = Trueとy == z = Trueからx == z = Trueが導かれます。 -
(/=)は(==)の否定です。x == y = not (x /= y)が全てのxとyについて成り立ちます。
理論上、Idrisにはこれらの法則を非原始型に対してコンパイル時に検証する能力があります。
しかしながら、実用上はEqの実装には必要ありません。
そのような証明を書くというのはちょっとしたハマりどころだからです。
Ord
Prelude版のCompとしてOrdがあります。
自前のcompと等価なcompareに加え、比較演算子(>=)、(>)、(<=)、(<)やユーティリティ関数maxとminを提供します。
Compとは異なり、OrdはEqを拡張します。
なのでOrd制約がある場合は、常に演算子(==)および(/=)と関連する関数が使えます。
Ordの法則
Ordの全ての実装について以下の法則を満たすようにしてください。
(<=)は反射的で推移的です。(<=)は非対称的です。x <= y = Trueとy <= x = Trueからx == y = Trueが導かれます。x <= y = y >= xx < y = not (y <= x)x > y = not (y >= x)compare x y = EQ=>x == y = Truecompare x y == GT = x > ycompare x y == LT = x < y
SemigroupとMonoid
Semigroupは例に出てきたインターフェースConcatのようなもので、
関数concatに対応する演算子(<+>)(appendとも)を持ちます。
同様にMonoidはEmptyに対応するもので、emptyに対応するneutralがあります。
これらは極めて重要なインターフェースで、 2つ以上のデータ型の値を単一の同じ型の値に結合するのに使えます。 前述の例にもありましたが数値型の和や積に留まらず、 連続するデータや連続する計算処理の結合にも使えます。
例として地理を扱うアプリケーションでの距離を表すデータ型を考えます。
単にDoubleを使うこともできますが、あまり型安全ではありません。
単一のフィールドを持つレコード型でDouble型の値をくるむとよいでしょう。
値に明確な意味論が備わるためです。
record Distance where
constructor MkDistance
meters : Double
2つの距離を結合するのには自然な方法があります。
それらが持つ値を加算すればよいのです。
そこで直ちにSemigroupの実装が導かれます。
Semigroup Distance where
x <+> y = MkDistance $ x.meters + y.meters
これも直ちに明らかなことですが、ゼロはこの操作での中立な要素です。
ゼロを加算しても値には何ら影響がありません。
こうしてMonoidも実装できます。
Monoid Distance where
neutral = MkDistance 0
SemigroupとMonoidの法則
SemigroupとMonoidの全ての実装について以下の法則を満たすようにしてください。
(<+>)は結合的です。x <+> (y <+> z) = (x <+> y) <+> zは全てのx,y,zの値について成り立ちます。neuralは(<+>)に関して中立な要素です。neural <+> x = x <+> neural = xが全てのxについて成り立ちます。
Show
Showインターフェースは主に不具合修正の用途で使われ、与えられた型の値を文字列として表示するためのものです。
その値を作るIdrisのコードに近付けることが多いです。
その場合は必要に応じて括弧内に引数を適切にくるむことがあります。
例えば以下の関数の出力がどうなるかREPLでやってみてください。
showExample : Maybe (Either String (List (Maybe Integer))) -> String
showExample = show
そしてREPLで次のようにします。
Tutorial.Interfaces> showExample (Just (Right [Just 12, Nothing]))
"Just (Right [Just 12, Nothing])"
Showのインスタンスを実装する方法は演習で学びましょう。
オーバーロードされた直値
Idrisの直値、例えば整数直値 (12001)、文字列直値 ("foo bar")、浮動小数点直値 (12.112)、そして文字直値
('$') はオーバーロードできます。
つまり、Stringではない型の値を単なる文字列直値から作れるということです。
ちゃんとした仕組みは他の節まで待たなければいけませんが、大体はインターフェースFromString(文字列直値用)やFromChar(文字直値用)やFromDouble(浮動小数点直値用)を実装すれば充分でしょう。
整数直値については特殊なので次の節で詳述します。
FromStringの用途はこうです。
アプリケーションを書いており、利用者が利用者名とパスワードで自身であることを同定できるものだとします。
はっきりと異なる意味論を持つものではあるのですが、何れも文字からなる文字列なので、2つを混同してしまいがちです。
この場合、これら2つのために新しい型を用意することが望ましいです。
特にこれらを取り違えたりなんかするとセキュリティ上の問題になりますから。
例としてレコード型を3つ用意しました。
record UserName where
constructor MkUserName
name : String
record Password where
constructor MkPassword
value : String
record User where
constructor MkUser
name : UserName
password : Password
型Userの値を作るには、試してみたいときであっても、逐一文字列を構築子でくるむ必要があります。
hock : User
hock = MkUser (MkUserName "hock") (MkPassword "not telling")
これは割りとまどろっこしく、型安全性を増すには割に合わなさすぎると考える人もいるでしょう(私はそうでもありませんが)。 幸いにも文字列直値の便利さをとても簡単に取り戻せます。
FromString UserName where
fromString = MkUserName
FromString Password where
fromString = MkPassword
hock2 : User
hock2 = MkUser "hock" "not telling"
数的インターフェース
Preludeはよくある代数操作を提供するインターフェースも幾つか公開しています。 以下はインターフェースと提供されている関数の網羅的な一覧です。
-
Num(+): 加算(*): 乗算fromInteger: オーバーロードされた整数直値
-
Negnegate: 正負反転(-): 減算
-
Integraldiv: 整数の除算mod: 剰余演算
-
Fractional(/): 除算recip: 値の逆数を計算する
ここで次のことがわかります。
所与の型に整数直値を使うのにはインターフェースNumを実装する必要があります。
-12のような負数の整数直値を使うためにはインターフェースNegも実装する必要があります。
Cast
最後にこの節ではCastというインターフェースについて手短かに説明します。
ある型の値を他の型の値に関数castで変換するというものです。
Castが特別なのは、このインターフェースが2つの型変数を引数に取るからです。
これまで見てきた他のインターフェースは型変数が1つしかありませんでした。
これまでCastを主に標準ライブラリにある原始型の相互変換に使ってきました。
特に数値型です。
Preludeから公開されている実装を見てみると(例えば:doc CastとREPLで呼び出します)、
原始型のほとんどの対に関して沢山の実装があることがわかるでしょう。
Castは他の変換にも便利ですが(MaybeからListであったり、
Either eからMaybeであったり)、
Preludeとbaseはそうした変換を一環して提供してはいないようです。
例としてCastの実装としてSnocListからListとその逆のものがありますが、
Vect nからListへ、あるいはVect nからListへの実装はありません。
そうした実装も可能ではあるのですが。
演習 その3
ここにある演習は自前のデータ型のためのインターフェースを流暢に実装できるようになることを意図しています。 Idrisのコードを書くときはしばしば必要になることですから。
Eq, Ord,
Numのようなインターフェースが便利な理由はすぐに分かりますが、一方でSemigroupとMonoidの便利さは最初は実感しにくいかもしれません。
したがって演習の中には幾つかの異なるインスタンスについて実装するものがあります。
-
複素数のためのレコード型
Complexを定義してください。 型Doubleの値2つを対にします。Eq、Num、Neg、FractionalをComplexに実装してください。 -
ShowをComplexに実装してください。 データ型Precと関数showPrecを調べて、 PreludeでEitherやMaybeのインスタンスを実装するためにどのようにこれらが使われているのか見てみましょう。書いた実装が正しい挙動になっていることを確かめるために、 REPLで型
Complexの値をJustにくるんでshowしてみましょう。 -
以下のオプショナルな値の梱包について考えてみましょう。
record First a where constructor MkFirst value : Maybe aインターフェース
Eq、Ord、Show、FromString、FromChar、FromDouble、Num、Neg、Integral、FractionalをFirst aに実装してください。 これらは全て型変数aに対応する制約が必要になるでしょう。 必要に応じて、以下のユーティリティ関数を実装して使ってください。pureFirst : a -> First a mapFirst : (a -> b) -> First a -> First b mapFirst2 : (a -> b -> c) -> First a -> First b -> First c -
同様にインターフェース
SemigroupとMonoidをFirst aに実装してください。(<+>)は最初の非空な引数を返します。 また、neutralは対応する中立要素です。 これらの実装では型変数aに制約があってはいけません。 -
レコード
Lastについてもう一度問題3と4を解いてください。Semigroupの実装は最後の非空な値を返します。record Last a where constructor MkLast value : Maybe a -
関数
foldMapは関数を順番に写してMonoidを返します。 値のリストを巡回しつつ(<+>)で結果を累算します。 これはリストに格納された値を集積するとても強力な方法です。foldMapとLastでリストから最後の要素を(もしあれば)取り出してください。ここでの
foldMapの型はより一般的で、リストのみが専門ではありません。MaybeやEitherやその他のまだ見ぬ容器型に対しても動きます。 後の節でインターフェースFoldableを学びましょう。 -
真偽値の値のレコード梱包
AnyとAllを考えます。record Any where constructor MkAny any : Bool record All where constructor MkAll all : BoolSemigroupとMonoidをAnyに実装してください。 ただし(<+>)の結果は、少なくとも1つの引数がTrueであるときにのみTrueです。neuralはもちろんこの操作において中立な要素になるようにしてくださいね。同様にして
SemigroupとMonoidをAllに実装してください。(<+>)の結果は、両方の引数がTrueのときにのみTrueであるようにしてください。neuralはもちろんこの操作において中立な要素になるようにしてくださいね。 -
関数
anyElemとallElemsを、foldMapとAnyないしAllを使って実装してください。-- 命題が少なくとも1つの要素について満たされているとき真 anyElem : (a -> Bool) -> List a -> Bool -- 命題が全ての要素について満たされているとき真 allElems : (a -> Bool) -> List a -> Bool -
レコード梱包
SumとProductは主に数値型を保持するのに使われます。record Sum a where constructor MkSum value : a record Product a where constructor MkProduct value : aNum aの実装があるとして、Semigroup (Sum a)とMonoid (Sum a)を実装してください。 ただし(<+>)は加算に対応します。同様に
Semigroup (Product a)とMonoid (Product a)を実装してください。 ただし(<+>)は乗算に対応します。neutralを実装する際は、数値型を扱うときに整数直値が使えることを思い出してください。 -
sumListとproductListを実装してください。foldMapとともに演習9の梱包を使ってください。sumList : Num a => List a -> a productList : Num a => List a -> a -
foldMapの強力さと多彩さを味わうために、演習6から10までを解いたあとに(もしくはREPLでSolutions.Interfacesを読み込んでもよいです)、以下をREPLで実行してください。 これはなんとたった1回の巡回でリストの最初と最後の要素と全ての値の和と積を計算しています。> foldMap (\x => (pureFirst x, pureLast x, MkSum x, MkProduct x)) [3,7,4,12] (MkFirst (Just 3), (MkLast (Just 12), (MkSum 26, MkProduct 1008)))
Ordの実装付きの型用にSemigroupの実装もあります。
この実装は2つの値のうちより小さいかより大きいほうを返します。
絶対的な最小値や最大値がある型の場合(例えば自然数の0や、Bits8の0と255)、これらはMonoidにまで拡張できます。
-
以前の演習で、化学の元素を表現するデータ型を実装し、化学の体積を計算する関数を書きました。 新しく原子の体積を表現する単一フィールドレコード型を定義して、インターフェース
Eq,Ord,Show,FromDouble,Semigroup,Monoidをこの型に実装してください。 -
演習12の新しいデータ型を使って原子の原子質量を算出し、 分子式で与えられる分子の分子質量を計算してください。
解決の糸口:相応しいユーティリティ関数があれば、ここでもfoldMapが使えます。
最後の註釈:もし関数型プログラミングが初めてであれば、演習6から10の実装をREPLで確かめてみてください。 これら全ての関数を最小限の量のコードでどう実装できたか、そして演習11で見たように1回のリストの巡回においてこれらの挙動をどう組み合わせられたかを思い返しましょう。
まとめ
- インターフェースのおかげで、異なる型で異なる挙動をする同じ関数を実装できます。
- 1つ以上のインターフェースの実装を引数に取る関数は制約付き関数と呼ばれます。
- インターフェースは他のインターフェースを拡張することで階層的に組織付けられます。
- インターフェースの実装には、それ自体が他の実装を必要とする制約が課されることがあります。
- インターフェースの関数には既定実装を与えられます。 この実装は実装者によって上書きできます。 例えば効率性の理由などからです。
- インターフェースを用意すれば、文字列や整数といった直値を自前のデータ型に使えることがあります。
ただ、この節ではまだ直値の一部始終をお話ししていません。 限られた値の集合のみを受け付ける型に直値を使うことに関するもっと詳しい話は、原始型についての章にあります。
お次は?
次の章では関数とその型にさらに迫ります。 名前付き引数、暗黙の引数、引数消去に加え、より複雑な関数を実装するための幾つかの構築子について学びます。