Verse言語の設計思想を読み解きたい（22） option型で未初期化状態を表す"false"の意味について考える。
お久しぶりの更新です。
実は今、これまで書いてきたVerse言語の記事を同人誌として一冊にまとめる作業を進めています。５月に開催された技術書典で頒布するつもりで進行していたのですが、いざ再編集するとなると修正・追記したい箇所が山ほど出て来てしまい、結局会期に間に合いませんでした。
同人誌がいつ完成するかは正直良く分かりません。このブログでは引き続きVerse言語やUEFNについて書いて行きたいと思います。
今回はoption型を掘り下げてみます。
なぜoption型にfalseを格納出来るのかという話
Verseでは未初期化状態の変数（定数）が許されません。初期値を持たないクラスメンバ定数は定義出来ますが、これもインスタンス化時に初期化しなければなりません。
ある型の変数において未初期化状態を許したい場合はoption型を使います。
例えばint型のoption型定数は以下の様に定義できます。
Test1:?int = false
型名のprefixに"?"を置くとオプション型になります[1]。"false"は、このintのoption型定数Test1が初期化状態である事を示します。
option型は変数も定義できます。一度値を入れた後で、再度未初期化状態にする事も出来ます。
var Test1A:?int = false #未初期化状態で定義
set Test1A = 123 #整数123を割当
set Test1A = false #再び未初期化状態を割当
option型変数を参照する場合、クエリ演算子"?"が必要になります。クエリ演算子は、logic型をオペランドに取る後置演算子で、クエリ式を作ります。クエリ式はオペランドがfalseなら「失敗」、そうでなければ変数の値を返す失敗許容式です。
var Test1A:?int = false #未初期化状態で定義
if(Test1A?)
then:
#no op
else:
Print("述語が「失敗」したのでこちらが実行される")
さてここで疑問が一つ。option型において、未初期化状態が"false"になるのは何故なのでしょうか？ そもそも、この"false"はlogic型のfalseなのでしょうか？ もしそうなら、なぜlogic型falseがここで出てくるのでしょう？
この一見奇妙な書式は、実はVerseの巧妙な型システムに由来しています。とはいえ、Verseの型システムは仕様が一部公開されておらず、また機能自体も未実装な要素が多くあるため、ドキュメントだけ読んでもわかりません。
今回は現状分かっている範囲に推測を交えつつ、option型とfalseの関係を紐解いて行きたいと思います。
true型とfalse型
まず、trueとfalseという「要素」について考えてみます。
Verseのtrue/falseは、型システム上ではどちらも独立した「型（types）」、つまりtrue型／false型として扱われます。ただし、これはあくまで型システム上の話なので、実際にtrue型変数を定義出来るというわけではありません。
Verseにおける型システム上のtrue型／false型が果たす役割について考えてみます。
true型／false型は、それぞれtrue/falseのみを要素として持つ型です。
仮にtrue型定数Test1を定義出来るとしたら、以下の様になるでしょう。
#擬似コード。現在のVerseではtrue型変数を定義出来ない。
Test1:true = true #Testはtrueとして機能する
true型はtrueしか要素を持たないので、定数Test1にはtrueしか格納できません。なお、Verseでは変数（定数）がnullになる事はありません。前述した通りoption型以外では未初期化のままの参照も許されません。
logic型（true型とfalse型の直和型）
前項では、true型／false型はそれぞれtrue/falseのみを値として持つ型であると説明しました。これだけでは意味があるように思えませんが、「直和型」という概念を導入すると、true型とfalse型から、logic型（他の言語で言うbool型）を定義出来るようになります。
「直和型（sum type）」は、複数の型の集合から定義される型で、それらの型のうちいずれかの型を取る事が出来ます。直和型の考え方を使うと、logic型は、true型とfalse型の和を取った物と定義できます。
logic型の定義を疑似コードで書いてみましょう。現在のVerseでは、ユーザーが直和型を定義する構文が用意されていません。なので、ここではHaskell言語による疑似コードでlogic型の定義を示します。
#Haskell疑似コード
data logic = true | false
"logic"/"true"/"false"はいずれも型です。このコードは「logic型は、true型／false型のいずれかとして振る舞う」事を意味しています。
次の例は、logic型変数Test2にtrue/falseを代入するVerseコードです。
var Test2:logic = true
set Test2 = false
logic型がtrue型とfalse型の直和型なので、true型由来のtrue、false型由来のfalseのそれぞれを格納出来るわけです。
余談ですが、data式を使うとtrue型、false型も以下のように定義できます。
#Haskell疑似コード
data true = true
data false = false
慣れない見た目ですが、演算子"="の左辺にある"true"は型名、右辺にある"true"は論理値リテラルです（"false"についても同様です）。
ちなみに、このように最小単位の型を組み合わせてより複雑な型を構築していく形式を、型システム理論では「代数的データ型（Algebraic Data Types）」と呼びます。直和はこの代数的データ型で行われる処理の一種です。
option型（任意の型とfalse型の直和型）
改めてoption型を考えてみます。すでにおわかりかもしれませんが、option型は「任意の型とfalse型の直和型」と考える事ができます。つまり、未初期化状態を表す為にoption型に代入している"false"は、「logic型のfalse（より正確にはfalse型のfalse）」そのものだったというわけです。
option型の定義も、haskell疑似コードで記述してみます。
data ?int = int | false
ここではintのoption型を"?int"であるとしました（verseの"?"は恐らく演算子なので、この記述は正しく無いです）。
?int型はint型とfalse型の直和型です。つまり、?int型変数はint型が格納出来る値（つまり整数）と、false型が格納出来る値（falseのみ）を取る事が出来るのです。そしてこれは任意の型について同じように言えるのです。
option型変数にfalseを代入すると、当然ながらその変数の値はfalseになります。この意味では、これまでの「falseを代入すると未初期化状態になる」という説明は正確とは言えません。
しかし、option型変数への参照はクエリ式を通じてでないと実行できず、また、クエリ式はオペランドがfalseの時「失敗」するので、その変数にはアクセス出来ません。この二つの仕組みによって、「falseを代入すると未初期化状態になる」という挙動が実現されるのです。
補足：option型のlogic型
ちなみに、logic型のoption型である"?logic"という型も定義できます。この型は、クエリ式でしか参照出来ない事を除けば、通常のlogic型と同じように振る舞います。これも巧妙な構造だと思います。
今回の話の論拠
今回解説した「trueとfalseはそれぞれ独立した型」「logic型はtrue型／false型の合成型」「option型のfalseはlogic型のfalseと同じ物」の３点は、公式フォーラムでのやりとりをベースにしています（逆に言えばどれも公式ドキュメントには記載されていません）。
これは以前行われた公式フォーラムでの開発者に直接質問出来るイベントの回答の一つです。ちなみにこの質問をしたのは土屋（ブログ主）です。
以下関係する質問と回答について私訳を併記しておきます。
質問１："true"と"false"はそれぞれ別個の型ですか？（logic型は、true型とfalse型の合成型ですか？）
回答１：技術的にはイエス――Verseでは、それらは個別の型です。ヒントをあげると、trueとfalseはどちらも、他のVerseの型名規則と同じように小文字になっています。現在のドキュメントでは明示されていませんが、Verseの型付けは非常に洗練されており、今後より機能が充実する過程で、ドキュメントもVerseの型理論をより良く反映するようになるでしょう。
質問２：option型の初期値に設定出来る"false"と、logic型の"false"は同じ物ですか？
回答２：イエス。
-
この"?"がクエリ演算子なのか、それとも別（例えばoption型定義演算子）なのかは不明 ↩︎
Discussion