Haskell, OCaml, Rust, Scalaのような言語で関数型プログラミングを書くことに慣れている方なら、おそらく代数的データ型(ADTs)を扱った経験があるでしょう。本記事はADTsを扱ったことがない方を対象に、Simplicityの基礎とADTsについて解説します。
Simplicity入門シリーズ初回の本記事では値と型の概念、次記事では関数、式、コンビネータについて解説します。
解説に入る前に、簡単な数式を例にとって、値、型、式を定義しましょう：
(2 > 1) = True
本稿の目的上、ブーリアン式 (2 > 1) はブーリアン値 Trueを取ります。ブーリアン型は論理型とも呼ばれ、TrueまたはFalseのどちらかの値を取ります。言い換えると、ブーリアン型が取ることのできる値は、すべてこの2つの集合に含まれます。結果がブーリアン値となる式は、プロポジションと言う論理学の用語で表現されることもありますが、ここではあえて深入りしないでおきます。 型は特定の特徴を持つ値の集合を指します。型を考慮することで、値を体系的に論ずることができるようになります。大半のプログラミング言語では、式は特定の型を表しますが、Simplicityにおけるexpressions (式) は、ソース型からターゲット型へと値をマップする関数です。この式は、評価する際に入力値を処理して出力値を生みます。そして値は、あるデータ型に該当する特定のデータを指します。
name := expression : source type → target type
論理をコードに落とし込む際、開発者は制御フロー、エラーハンドリング、効率性などを考慮して、実装の詳細を検討する必要があります。どこかでミスをすると、コードベースにバグが混入するおそれがあるからです。Haskell, Coq, Adgaなどの言語は、数学的な概念や計算を表現することを目的に設計されており、コード自体も数学に近いです。そのため、一般的なプログラミング言語と比較して、バグが混入しにくいとされます。このような数学的な言語は、2つの分野において重宝されます：数学的処理の記述と推論です。どちらもプログラマブル・マネーにとって非常に有用で、Simplicityの設計哲学とも親和性が高いです。
SimplicityはBitcoin ScriptやEVMに似たスマートコントラクト言語です。Hacspec (あるいはTLA+, Alloy) のように仕様を記述するための言語であるため、その文法には厳密な数学的なモデルがあります。それゆえ、プログラム文を数学的に証明することが可能です。つまり、コントラクトがSimplicityで記述されていれば、それが正しく動作することを直接検証できるのです。例えば、コインの移転に署名Xが必須なことや、プログラムがメモリをYバイト以上使用できないことを証明できます。
Simplicityにおける型は、下記3つの基本形に分類できます：
- Unit型が取れる値は１つだけです。 Type 1 (ONEと表記する場合もあります)
- Product型は2つの型を論理積で組み合わせます。A × B
- Sum型は2つの型を論理和で組み合わせます。A + B
Simplicityでは、あらゆる型が上記3つ型から構成され、すべての型が上記3つの単純な操作に分解できます。
後ほど例をいくつかご紹介しますが、たった3つの型から多様な型を作ることができます。
- bit型はunit型2つの和です。2 (TWOと表現する場合もあります)
- option型はunit型と任意の型の和です。1 + A
- word型はbit型を繰り返し論理積したものです。2ⁿ
まずは一番シンプルな型から見てみましょう。
何もないところから何かが生まれる時、最初に出現する最も原始的なもの、unit型はそんな概念です。
Unit型 (1, Empty)
unit型は1つの値しか取ることができません。紛らわしいことに、この値もunitと呼ばれます。シンプルで美しい型ですが、どのような意味があるのでしょう。unit型は1、またはONEと表記されます。
一方、unit値は()と表記されます。() : 1 と書けば、()という値は1という型であると明示したことになります。
この型は、全く情報を持たない空のタプルであることが特徴なため、「空」と呼ばれることも多いです。値に関する選択の余地が皆無なので、いかなる情報を持たせることができず、エントロピーはゼロです。識別要素を含められないデータ型の存在理由は？と問いたくなるのももっともです。
答えは、unit型が存在することで、より複雑な型の合成がSimplicityで可能になります。unit型はハイレベルな概念を支える屋台骨なのです。
Sum型 (Tagged Union)
所与の2つの型の和が、必ず左側の型または右側の型のいずれかに該当することを、以下のように表記します：
left(a) : A + B where value a : of type A
right(b) : A + B where value b : of type B
sum型は型Aまたは型Bに当てはまる値の集合です。2つの型の和を取ることで、A型とB型どちらの値でも取ることが可能な新しい型を作ることができました。主用途は、左または右のいずれかの値の選択です。左と右の両方の型に該当する必要がある場合は、sum型ではなく、後述のproduct型 (積)が利用できます。
unit型が情報の欠如を表現する一方、sum型は内包する型の組み合わせや選択といった概念を表現します。sum型にはlabelまたはtagと呼ばれる値の型を示す欄があり、条件分岐に使用できます。2つの値が同じでも、left(a)とright(a) (A + A 型)のように、左右という別々のラベルがつけられるのは便利です。
HaskellにおけるEither型はsum型で、2つの異なる型からの選択を表現できるようにします。RustにおけるResult型も同様で、成功時だけでなく、エラー発生時にも適切な処理を保証します。Simplicityのsum型はこれらと同じ概念で、複数の選択肢をまとめるものです。
型の和を取ることができることで、ビットという概念が自然に発生します。
Bit型 (2, Boolean型)
bit型は2つのunit型の和です。Bit型を Bit := 1 + 1, 2, or TWO と定義すると：
0 := left(()) : Bit
1 := right(()) : Bit
bit型は二者択一を表す基本的な型で、0と1という2つの値しか取ることができません。sum型では、値は必ず左側か右側のどちらかの型に該当し、そのどちらに該当するのかのラベリングが求められます。bit型においては、子の型はどちらもunit型なので、それ以上の情報は持ちません。ビットとして扱う情報は、左側・右側というラベルです。PythonやJava, C++などでお馴染みのBoolean型は、TrueとFalseという2つの値の選択を定義するbit型の別称にすぎません。
Boolean型を Boolean := 1 + 1, 2, or TWO と定義すると：
false := left(()) : Boolean
true := right(()) : Boolean
Simplicityでは、上記の型はどちらも2と表現されます。構造が同じなので、実際は全く同じ型です。unit型とそれ以外の任意の型の和をとる場合、option型という新しい型になります。
Option型 (Nullable, Maybe)
option型はunit型とそれ以外の任意の型との和を指し、以下のように定義します。
Option[A] := 1 + A or A?Nullable型やMaybe型と呼ばれることもあるoption型は、2つの可能性の一方を提示します：値がない可能性 (unit型で表現) あるいは値がある可能性 (A型で表現) です。
これはHaskellではMaybe、RustではOptionと呼ばれる概念です。この型のおかげで、値の有無が不明な場面を扱うことができます。値がなかった場合の処理を明示する際に非常に有用です。
Product型 (Tuple)
2つの異なる型AとBの積を取るproduct型は、Aから1つ、Bから1つの値を取ったペアを表します。
product型は (a, b) : A × B と定義し、(a,b) はA × B型の値のペアとなります。
product型は一方が型A、他方が型Bに属する値のペアの集合を表します。product型では、A型のいずれの値もB型のいずれの値とペアになれるので、 |A| * |B| 通りのペアが表現できます。
2つの値を1つのペアにまとめることから、”AND"操作と見なすことができます。product型という名称は、取りうる値の総数を、A型に属する値の数とB型に属する値の数の掛け算で算出できることに由来します。sum型では左側または右側どちらかの型を選択する必要がありましたが、product型では左側と右側の型から1つずつ選択した値をそのままラップします。このため、複数の値をまとめたものを表現でき、階層的な構造を作ったり、より大規模なデータモデルを扱う時に利用できます。
product型をtuple(タプル)と呼ぶこともあります。タプルは多くのプログラミング言語で使用される一般的なデータ構造で、複数の返り値をまとめたり、関連性のあるデータやキーバリュー型のデータを表現するのに便利です。
Simplicityにおけるproduct型の使用例に「点」の表現があります。仮に Int 型(整数)があるとして、x座標とy座標を持つ二次元平面上の点を表現したい場合、以下のように記述できます：
Point := Int × Int
これは新たに Point 型を整数型のペアとして定義しています。
この型のインスタンスを作成するには、xとyの値を代入します：
p := (3, 5) : Point
別の例として、線分を考えてみましょう。2つの点からなるproduct型を定義することで、その2点間に引いた線分を以下のように表現できます：
Line := Point × Point
しかし、この例には問題があります。そう、Common LispやPythonと違って、Simplicityには任意の大きさの (非常に大きな) 整数を表す整数型がありません。Simplicityはサイズが固定長の型を前提とします。
「ゼルダの伝説」というゲームでプレイしたことがある方は、主人公のリンクが保持できるコイン数が、0から255枚という値しか取れない仕様だったことを覚えているかもしれません。保有コイン数を8ビットの整数として扱っていたため、8ビットの整数で表せる最大値255が、保有できるコインの上限になっていました。
では、Simplicityではビット長の概念はどう扱われているのでしょうか？
Word Types (Fixed-Width Integers, Characters)
word型は複数のbit型の積を取って作成します。組み合わせるビット数をbit widthと呼びます。IntegerやWordなどのバイナリデータの大きさをビット数で既定することで、自ずと表現可能な値の範囲が限定されます。
例えば：
2¹ := 2 は1ビットの整数を表し、bit型と同義です。
2² := 2¹ × 2¹はbit型2つの積で、2ビットのwordを表します。
2⁴ := 2² × 2² は2-bit型2つの積で、4ビットのwordを表します。
2⁸ := 2⁴ × 2⁴ は4-bit型2つの積で、8ビットのwordを表します。
このようにして、bit widthを増やすことができます。
例えば、4-bitのwordは16通りの0と1の組み合わせを表せます。2進数で言えば、0000から1111までの数字を表現できます。2進数では、数が大きくなると桁数が増えて読みづらいので、通常、数字の表現は2進数4桁を1桁で表現可能な16進数が使われます。
HexDigit := 2⁴
B := 1011 : HexDigit
ASCII文字を数字で表すChar型を作ることもできます：
Char := 2⁸
‘k’ := 0110 1011 : Char
8ビットのwordを使ってInt型を作ります：
Int8 := 2⁸
この8ビットの整数を使えば、色をRGBで簡単に表現できます：
RGB := ((Int8, Int8), Int8) : (2⁸ × 2⁸) × 2⁸
8ビット整数それぞれが、色の赤、緑、青の成分をそれぞれ0から255 (2⁸ - 1)までの値で表現します。
RGBに値を代入することで、色のインスタンスを作成できます：
BitcoinOrange := ((255, 153), 0) : RGB
Simplicityの型は有限
Simplicityにおける型には、中身の構造だけでなく、その型が取り得る値の範囲を含めることができます。例えば、2 + 2⁴型が取ることのできる値は18種類あります。
Simplicityには無限の値を取ることのできる型はありません。無限長のリストは List := Item + (Item × List)と定義できそうですが、不可能です。。無限長であったり、再帰性のある型は、強制終了、リソースマネジメント、プログラムの動作解析で問題を引き起こすためです。
Simplicityは型を有限のものに絞ることで、プログラムの動作や正常な終了を保証し、コードの徹底した分析と検証を可能にしました。暗号プロトコルには、有限の型だけで十分です。STARKSやSNARKsは (ロールアップさえも) 膨大な計算を比較的小さい有限長のデータに対する暗号学的操作に落とし込むため、Simplicityで扱うことができます。
Simplicityの学習資料
Simplicityについて学んでみたい方は、まずホワイトペーパー内の技術ドキュメントおよびSimplicity Wiki内のCore Language Overviewをご覧ください。関数プログラミングの経験があまりない方には、これらの資料は難しいかもしれません。Build On L2コミュニティ内のSimplicityスレッドに、もう少し平易な資料を用意しているので、そちらを参照ください。質問も受け付けています。難解な概念をサンプルコードを介して、わかりやすく説明したいと思い執筆した本記事、いかがでしたか。数学的な発想で開発された言語であるSimplicityは、プログラマブル・マネーに厳密な検証を経たスマートコントラクトを提供できるかもしれません。本記事でSimplicityの主要な型をおおまかに理解しておけば、本シリーズの次記事以降で紹介する関数、式、コンビネータなどの概念をスムーズに学ぶことができます。