デザインパターン！ 私がそれらについて初めて知ったのは、私が大学の大学院生だったときのソフトウェア設計コースででした。 テンプレートを使用してさまざまなJavaプログラムを作成しました。 それ以来、このフレーズはOOPのようなものに関連付けられています。 しかし、Agda言語を理解していると、The Power Of Piという記事に出くわしました。この記事では、依存型を持つ言語のデザインパターンについて説明しています。

この投稿では、Viewと呼ばれるこれらのテンプレートの1つについて説明します。 これにより、カスタムパターンマッチングルールを実装できます。 これがどのようなパターンであるか、カスタムパターンマッチングとは何か、依存型のある言語でのパターンマッチングの機能は何か、そして静的型付け（Haskell、Scala、Ocaml、F＃）を使用した関数型プログラミング言語に精通している場合-キャットへようこそ！

ビューとユーザーパターンマッチング

最初に、ユーザーパターンマッチングとは何かを考えましょう。 いくつかのxsリストを操作して、パターンマッチングを実行してみましょう。

match xs with [] -> ... (y : ys) -> ... 

ここでは、 xsを空のリストまたはhead要素とそれに割り当てられたリストで構成されるリストのいずれかとして見ます。 しかし、たとえば、いくつかの2つのリストysとzsの連結で構成されるリストとしてxsを調べたい場合はどうでしょうか。 のようなもの

 match xs with [] -> ... (ys ++ zs) -> ... 

言い換えれば、パターンマッチングの結果としてデータ構造がどのように表現されるかに影響を与えたいと考えています。 これをカスタムパターンマッチングと呼びます。

記事が進むにつれて、私たちの目標は、次の状況に合わせてカスタムパターンマッチングを実装することです。 固定長のビットベクトルを使用します。 同時に、型のベクトルの長さを直接指定する機能があります。 たとえば、 ビット表記法[32]は、 ビットが32ビットのベクトルであることを意味します 。 パターンマッチングの過程で、たとえば次のように、さまざまな方法でベクトルを等しい部分に分割できるようにしたいと考えています。

 swapAB : [32] -> [32] swapAB [abcd] = [bacd] 

この関数は32ビットベクトルを受け入れ、それを4つの部分に分割します。各部分は8ビットベクトルであり、最初の2つの8ビットワードを交換します。 彼女は、同じ成功を収めて、それぞれ16ビットの2つの部分に分割できました。 このような機能は、暗号化ソフトウェアを作成するときに役立ちます。 たとえば、暗号化アルゴリズムを記述することで強化されたCryptol言語の中心には、同様のものがあります。 Agdaでこれを実装する方法を見てみましょう。

カスタムパターンマッチングを実装するための一般的なスキームは次のとおりです。

1. ソースデータタイプのViewテンプレートを実装する
   
   1. 必要なフォームの元の型の値をコンストラクタが表すViewデータ型を定義します
   2. 元のデータ型の値からView型の値を構築するビュー関数を作成します
2. ビュー関数呼び出し結果でパターンマッチングを使用する

これらの点を扱う前に、いくつかの基本的なデータ型を定義します。

Agdaの自然数とベクトル

自然数は再帰的に決定されます：

 data Nat : Set where Zero : Nat Suc : Nat -> Nat 

Natのタイプを決定するとき、そのタイプを示します！ 数字3がNat型であるように、 Nat自体の型はSet型です。 セットは、Agdaの組み込みタイプです。 ただし、なぜこれが必要なのかを理解することは役に立ちません。すべての型がSet型であると単純に仮定できますが、これは正しくありません。
Nat型には2つのコンストラクターがあります。引数を持たないZeroと 、引数を1つ持つコンストラクターSucです。 したがって、数値3は（Suc（Suc（Suc Zero）））のようになります。つまり、（1 +（1 +（1 + 0）））のようになります。 ただし、Agdaにはリテラルが組み込まれているため、長いSucチェーンの代わりに、単に3と書くことができます 。

ベクトルは、次のように定義された固定長のリストです。

 data Vec (A : Set) : Nat -> Set where [] : Vec A Zero _::_ : {n : Nat} -> A -> Vec A n -> Vec A (Suc n) 

Natとは異なり、 Vec型には2つのパラメーターがあります。A型とNat型の値です。 2番目のVecパラメーターは型ではなく値であるため、 Vecは依存型です。 パラメーターがコロンで区切られているという事実は、たとえば記号->ではなく、偶然ではありません。 実際、コロンの後に記述されるのは、パラメーターではなく、いわゆるインデックスです。 ただし、私たちにとって、この違いは特別な役割を果たさず、すべてをパラメーターと呼びます。
最初のコンストラクターは空のベクターを作成します。 Agdaでは、異なる文字シーケンスを名前として使用できるため、コンストラクター[]を呼び出すことができます。
2番目のコンストラクターは、ベクトルnのサイズ、タイプAのベクトルの要素、サイズnのベクトルの3つの引数を取り、サイズ（n + 1）のベクトルを返します。 Vecタイプ自体の最初のパラメーターと同様に、最初の引数にも、タイプだけでなく名前-n：Natも指定したことに注意してください。 3番目の引数と戻り値を宣言するときにこの値を参照するため、これが必要です。 さらに、最初の引数は中括弧で囲まれます。 したがって、Agdaでは暗黙的な引数が表現されます。 実際、 nの値は、コンストラクターの3番目の引数から一意に復元できるということです。 実際、ベクトルを渡すと、そのサイズがわかり、タイプで指定されます。 したがって、実際には、最初の引数を渡すことはできません。Agda自体が何をすべきかを推測します。 したがって、コンストラクター_ :: _の呼び出しは、 _ :: _ {n} a someVecまたは_ :: _ a someVecのようになります。 しかし、それだけではありません！ 実際、コンストラクター名の下線は、挿入語であることを示しています。 2つの明示的な引数は、コンストラクターの名前の後にではなく、アンダースコアの代わりに、すべてをスペースで区切って記述することができます。 その結果、ベクターを作成する例を次に示します。

 v1 : Vec Nat 2 v1 = 1 :: (2 :: []) 

次のように書くことはできないことに注意してください。

 v1 : Vec Nat 3 v1 = 1 :: (2 :: []) 

コンストラクター[]は長さ0のベクトルを作成し、最初のコンストラクター::は長さ1のベクトル、2番目の::は長さ2のベクトルです。VecNat 2を取得しますが、3が必要です。型推論システムではこのようなコードをコンパイルできません。

とりわけ、ベクターに対するいくつかの操作が必要になります。

 _++_ : forall {A mn} -> Vec A m -> Vec A n -> Vec A (m + n) take : forall {A m} -> (n : Nat) -> Vec A (n + m) -> Vec A n drop : forall {A m} -> (n : Nat) -> Vec A (n + m) -> Vec A m 

これはベクトルの連結であり、操作は「最初のn個の要素を取得」および「最初のn個の要素を破棄」であり、Haskellのリストの場合と同様です。 forall {A mn}のようなレコードは、引数A 、 m 、およびnが暗黙的であるという事実に加えて、それらのタイプを指定したくないことを意味し、Agdaに明示的な引数に基づいて決定するように要求します。

ビットベクトルタイプ

パターンマッチングを実装するビットベクトルのタイプは、非常に単純に見えます。

 data Bit : Set where O : Bit I : Bit Word : Nat -> Set Word n = Vec Bit n 

WordはVec Bitの同義語であり、これを使用して32ビットベクトルをビットとして宣言できます：Word 32 。
パターンマッチングに移る前に、依存型がある場合の機能を見てみましょう。

依存型がある場合のパターンマッチング機能

次のデータ型を検討してください。

 data _==_ {A : Set} : A -> A -> Set where Refl : {x : A} -> x == x 

タイプ（x == y）は 、タイプAの 2つの特定の値によってパラメーター化され、ご想像のとおり、 xとyの値が等しいというステートメントを表します。 単一のReflコンストラクターを使用すると、 xとyの異なる値に対してタイプ（x == y）の値を作成できなくなります。 例：

 eq : (3 == 3) eq = Refl notEq : (3 == 4) notEq = ? 

最初のケースでは、タイプ（3 == 3）の値を構築する必要があり、これを可能にするコンストラクター-Reflがあります。 type （3 == 4）の値を構築することはできません-Reflは typeに適しておらず、type ==には他のコンストラクタがありません。
次に、この機能を検討します。

 f : (x : Nat) -> (y : Nat) -> (x == y) -> Nat 

この関数の引数のパターンマッチングはどのようになりますか？ 明らかに、3番目の引数には、タイプ==には他のコンストラクタがないため、 Reflを記述します。 この場合、最初の引数と2番目の引数が同じ数であることが自動的にわかります！ そのような場合、Agdaでは、いわゆるドットパターンを使用してこの事実に明示的に注意する必要があります。

 fx .x Refl = x 

このようなレコードは、2番目の引数（ドットが割り当てられた最初の引数と同じ名前）が、最初の引数と一致したものと同じであることを意味します。 Reflと比較した後に受け取った等価情報を失いたくないので、 たとえば.xの代わりにyを書くことはできません。

これからの結論はこれです。依存型を持つ言語では、任意の引数のパターンマッチングの後、他の引数に関する追加情報を取得できます。

視聴回数

Wordタイプのビューを作成する前に、より簡単な例を考えて、達成したいことを理解してください。
リストのタイプを考慮してください。

 data List (A : Set) : Set where [] : List A _::_ : A -> List A -> List A 

これはHaskellの場合と同じ通常のリストで、「最初の要素とリスト」として再帰的に表示されます。 「リストと最後のアイテム」と同じリストを表示できるようにしたいと考えています。 これのSnocViewデータ型を取得しましょう。

 data SnocView {A : Set} : List A -> Set where [] : SnocView [] _:::_ : (xs : List A) -> (x : A) -> SnocView (xs ++ (x :: [])) 

ここでは++演算子が使用されます-Haskellの場合のように、これはリストの連結です。 SnocView型の値の例：

 sx : SnocView (1 :: 2 :: 3 :: []) sx = (1 :: 2 :: []) ::: 3 

SnocViewタイプは 、リストおよび最後のアイテムビューが構築されるリストによってパラメーター化されることに注意してください。
次に、 渡されたリストのSnocView型の値を作成するsnocView関数を作成します。

 snocView : {A : Set} -> (xs : List A) -> SnocView xs snocView [] = [] snocView (x :: xs) with snocView xs snocView (x :: .[]) | [] = [] ::: x snocView (x :: .(ys ++ (y :: []))) | ys ::: y = (x :: ys) ::: y 

多くのことがあります。順番に始めましょう。 空のリストの場合は明らかです。空のリストは些細なSnocViewを提供します。 さらに、リストが空でない場合は、with構造を使用します（ここでの長いインデントは読みやすさのみを目的としています）。 この構築は、Haskellでの構築の場合とほぼ同じタスクを実行します。つまり、関数本体でパターンマッチングを実行するために使用されます。 snocView xsへの再帰呼び出しをマップするパターンは、垂直バーの右側に表示されます。 そのため、再帰呼び出しによって簡単なSnocViewが提供された場合、 xsリストは空であったため、 SnocView for x :: []は[] ::: xです。 2番目のケースでは、 SnocView for xsがys ::: yのようになるため、 SnocView for x :: xsを取得するには、 ysのヘッドにxを追加する必要があります。
不明な点は、縦線の左側に示されているものだけです。 前に説明したように、依存型が存在する場合のパターンマッチングにより、他の関数引数に関する追加情報を得ることができます。 この例では、 snocView xsの再帰呼び出しのパターンマッチングにより、 xsリストの値に関する情報が得られます。 この情報は、垂直バーの左側にあるドットパターンを使用して示されます。 たとえば、2番目のケースでは、 snocView xsがys ::: yを与えることを知ると、リストxsが ysと1つの要素y :: []のリストの連結として構築されていることがわかります。

snocViewを使用して、渡されたリストを周期的に右にシフトする関数を作成する例を次に示します。

 rotateRight : {A : Set} -> List A -> List A rotateRight xs with snocView xs rotateRight ._ | [] = [] rotateRight ._ | ys ::: y = y :: ys 

ここではアンダースコアを使用しました。 これは、アンダースコアの代わりにある意味に興味がない場合に実行できます。 とても簡潔で美しいようです！ この例は、実際、依存型を持つ言語でカスタムパターンマッチングを実装する方法を示しています。 それでは、Wordタイプで同じことをする方法を見てみましょう！

WordのSplitView

前の例と同様に、2つのものが必要です。特別なSplitViewデータ型と、 Word型の特定の値に対してSplitView値を作成するsplitView関数です。
まず、 Vecタイプを操作するための2つの追加機能が必要です。

 split : forall {A} -> (n : Nat) -> (m : Nat) -> Vec A (m * n) -> Vec (Vec A n) m split n Zero [] = [] split n (Suc k) xs = (take n xs) :: (split nk (drop n xs)) concat : forall {A nm } -> Vec (Vec A n) m -> Vec A (m * n) concat [] = [] concat (xs :: xss) = xs ++ concat xss 

SplitViewタイプは次のようになります。

 data SplitView {A : Set} : {n : Nat} -> (m : Nat) -> Vec A (m * n) -> Set where [_] : forall {mn} -> (xss : Vec (Vec A n) m) -> SplitView m (concat xss) 

このタイプは、数値mとベクトルによってパラメーター化されます。 mは、ベクトルを分割する部分の数を示します。 これが、ベクトルの長さがmの倍数である理由です。 唯一のコンストラクタにより、このタイプの値を次のように書き込むことができます。

 [ a :: b :: c :: d :: [] ] 

ここで、a、b、c、およびdは長さnのベクトルです。
次はsplitView関数です。

 splitView : {A : Set} -> (n : Nat) -> (m : Nat) -> (xs : Vec A (m * n)) -> SplitView m xs 

実装するには、転送されたベクトルをそれぞれ長さnの m個の部分に分割し、コンストラクター[_]に渡す必要があります 。

 splitView nm xs = [ split nm xs ] 

ただし、このような定義はコンパイラーに受け入れられません。 実際、コンストラクター[_]は、 SplitView m（concat xss）型の値を返します。 この場合、 xssはsplit nm xsであるため、式[split nm xs]はSplitView m（concat（split nm xs））タイプです 。 同時に、関数のシグネチャは、 SplitView m xs型を返すことを示します。xsは関数の3番目の引数です。 式xsとconcat（split nm xs）はまったく同じものであることを理解しています。concat関数とsplit関数がどのように機能するかを知っているからです。 これをコンパイラに納得させましょう。
まず、上記のsplitView本体を次の形式に書き換えます。

 splitView nm xs with [ split nm xs ] splitView nm xs | v = v 

この定義は、前の定義と同じ理由でコンパイラーに受け入れられません。vはSplitView m（concat（split nm xs））タイプですが、 SplitView m xsでなければなりません。 定義を引き続き変更します。

 splitView nm xs with concat (split nm xs) | [ split nm xs ] splitView nm xs | ys | v = v 

with構造は、複数の式によるパターンマッチングに使用できます。これらの式は、縦棒で互いに区切られています。 さらに、withを使用すると、汎化と呼ばれる効果が得られます。 関数の引数の型と構築する必要がある式の型は、パターンマッチングを実行する式によって異なる場合があるという事実に現れます。 たとえば、関数がある場合

 fxy with e fxy | p = ... 

次に、一般化の結果として、引数xおよびyの型、および本体で構築する必要がある式の型での式eのすべての出現がpに置き換えられます。 そして、withにいくつかの式がある場合

 fxy with e1 | e2 | e3 fxy | p1 | p2 | p3 = ... 

次に、特に、 p2およびp3でのe1の出現はすべてp1に置き換えられ、 p3でのe2の出現はp2に置き換えられます。
splitViewの定義では、 concat（split nm xs）をwithに追加することにより、タイプvはSplitView m（concat（split nm xs））からSplitView m ysに変更されます。 ここで、 xsとysが同じものであることを証明する必要があります。 これを行うには、次の関数が必要です。

 splitConcatLemma : forall {A} -> (n : Nat) -> (m : Nat) -> (xs : Vec A (m * n)) -> concat (split nm xs) == xs 

転送されたベクトルに従って、必要な式concat（split nm xs）とxsが等しいことを示す、おなじみのタイプ==の値を構築します。 この関数を使用して、次のバージョンのsplitViewを取得します。

 splitView nm xs with concat (split nm xs) | [ split nm xs ] | splitConcatLemma nm xs splitView nm xs | ys | v | eq = v 

ここで変更された型はありませんが、withの最初の式と同じ一般化効果により、 eqはys == xs型になります。 これで、関数を機能させるためのすべてができました。 eq値でパターンマッチングを実行します。

 splitView nm xs with concat (split nm xs) | [ split nm xs ] | splitConcatLemma nm xs splitView nm xs | .xs | v | Refl = v 

やった！ これですべてが機能します！
ここでは、 splitConcatLemma関数の定義は提供しませんでした。 これは、Viewテンプレートに関する会話にとって重要ではありません。さらに、すでにダウンロードされていることは間違いありません。 しかし、ここまで読んだ勇敢な戦士たちは、終わりが近づいています。
最後に、 splitViewを使用したカスタムパターンマッチングによるswapAB関数の実装：

 swapAB : Word 32 -> Word 32 swapAB xs with splitView 8 4 xs swapAB ._ | [ a :: b :: c :: d :: [] ] = concat (b :: a :: c :: d :: []) 

おわりに

この記事を読んだ後、質問があります。依存型のない言語で同じアプローチを使用することは可能ですか？ 実際、必要な形式でソースタイプを表すことができるデータタイプを設定し、ソースタイプの入力値からターゲット値を作成する関数を作成するだけでした。
依存型のない言語でこのアプローチを使用することの違いは、元の値との接触を失うことです。 たとえば、 SnocViewのタイプは、 作成するリストの値に依存します。つまり、元の値とビューの関係は、タイプのレベルで維持されます。 このため、 SnocView xsの値に対してパターンマッチングを実行すると、元のリストxsが正確にどのように見えるかに関する情報がわかります。 依存型がないと、そのような情報の受信は機能しません。
最初のものから生じる2番目の違いは、依存型がないと、ビューを構築する関数が一般的すぎることです。 たとえば、 snocView関数のタイプは次のとおりです。

 snocView : {A : Set} -> (xs : List A) -> SnocView xs 

関数本体は完全に任意ではあり得ないことは明らかです-SnocViewがxsに依存しているという事実によって制限されています。 依存型がない場合、この関数は型になります

 snocView : List A -> SnocView 

そして、たとえば、入力時に空のリストを返すだけで、ほとんど役に立たなくなります。

したがって、記事「The Power Of Pi：依存型が重要です！」を開始する言葉で投稿を終了します！

参照：
ニコラス・オウリー、ウーター・スウィアストラ「The Power Of Pi」
ドキュメント付き
ソースコード