暗黙の型変換を嫌わないで!(暗黙の型変換がなぜ嫌われるのか、暗黙の型変換で数学的同一視を自然に表現する、暗黙の型変換もどきを自作する、暗黙の型変換で遊ぼう(BNFを表す型))

どうもAaronです。
皆さん、「暗黙の型変換」ってお嫌いじゃないですか?
まあ僕も基本嫌いなんですが…
今回は実は暗黙の型変換も
うまく使えば結構有用なんだよ、って話です。
なおいつも通り僕はあんまり主流なプログラミング言語を知らないので雰囲気が伝わるように疑似コードメインで書きます。悪しからず。

1.そもそも暗黙の型変換とは?なぜ嫌われるのか?

暗黙の型変換について知らない人も多いと思いますのでいくつか例を見ていきましょう。


例えば

int a = 2;
float b = 3.0;
printf(a<b);

と書くと少なくない言語では、aとbは型が違う変数であるにもかかわらず、そして<は同じ型の変数を取ると規定されているにもかかわらず(勿論この辺の規定自体が違う言語もあります。例えば動的型付き言語のSchemeでは、そもそもintやfloatという型がなく「整数」や「実数」という言葉を数学的なそれに近い意味で使うため、2と3.0を<で比較することに何の問題もありません。しかし取り合えずそういうツッコミは置いといてある程度多くありそうなプログラミング言語の仕様について考えることにします。)trueを出力します。
これは<に渡されたint型のaが、「勝手に」float型に変換された上で処理が行われる、という仕様になっているからです。
このようにユーザーが明示的に命令していないにもかかわらず、後の処理(特に比較系の処理に多い)に必要になるように型を合わせてしまう仕様の事を「暗黙の型変換」と言います。
これを聞くと「整数を対応する浮動小数点数に変えるぐらいで、いちいち型変換子をタイピングするのも大変だしいい機能なんじゃない?」と思う人もいるかもしれません。
いや実際そういう側面はありますし、だからこそ多くの言語の仕様に残ったんだと思いますが、このような仕様があまりに多いと大変なことになります。
特定の言語をdisる意図はありませんが、僕の知ってる範囲でもいくつかこれに型エラーでもfalseでもなく、なんとtrueを出力する言語があります。

string a="4";
int b=4;
printf(a==b);

まあ確かに入出力回りなどでこういう処理が欲しいことはありますが、そもそも型というのはユーザーが間違って意図しない処理を書いたら、それにすぐ気づけるというのが利点の一つなのにこれでは本末転倒です。
まあそういうわけで暗黙の型変換は古い時代のプログラミング言語負の遺産と見做されることも多いのです。

2.暗黙の型変換で数学的同一視を自然に表現する

しかしながら実は暗黙の型変換には入力の手間を減らす以外にも有効で、しかも自然な使い道があります。
それは数学ではありふれている「同一視」という概念を自然に実装することです。
例えば次のような場合に暗黙の型変換が欲しいと感じるのは、むしろ自然なことに思われます。

a.数学的な同型(乃至埋め込み)がcanonicalに固定でき、同一視するべきオブジェクト

・・・例えば「\it GF_2とBooleanが別々の型として実装されているので、このお互いを自由に読み替えたい」とか「環\it Rの型をその多項式環\it R{\rm [}X{\rm ]}の型の部分型と見たい」という要求は極めて自然です。これを達成する一つの手段として暗黙の型変換があります。

b.構文上異なる型に属するが、数学的な要求により同じであるとみなしたいオブジェクト(「型をまたぐ等号・型レベルの等号」の表現)

・・・これは次章で例を出します。


実際非常に数学的な言語であるCoqには暗黙の型変換をユーザー定義する機能があるそうで(僕はCoqは詳しくないので人から聞いた話になってしまいますが)、恐らくは「入力の手間を省く」というよりは(それも理由ではあるのかもしれませんが)、上に述べたような数学的な同一視の表現に使うことが想定されているものと思われます。このような暗黙の型変換で同一視された型をcoercion typeという(?)っぽいです。すいません、ここはあまり調べられていないのでツッコミあったらお願いします。
言うなれば「ものは使いよう」ということでしょうか?

3.暗黙の型変換もどきを自作する

さて、ここでは自作の型の間に、あるいは言語が用意している型であっても暗黙の型変換がないときに型変換もどきを自作する方法を説明します(先述のCoqのように言語機能で自作できる場合は勿論それでよいのですが)。
まずは例をお見せしましょう。例はかなりHaskellっぽく書いてますが、Haskellに詳しくなかったため関数名は適当です。また例2の後半では依存型か依存型もどきが必要になり、Haskellの型レベル計算を強化するライブラリーがあるらしい(https://github.com/goldfirere/singletons/blob/master/README.md)んですが、そもそもHaskellエアプに理解できるはずもなく、心があっさり折れたので「まあHaskellに似た依存型がある疑似コードってことでいいや」と妥協しました。許してください。
例1

data TraditionalBadSilentTypeConversion = TBSTC1 String | TBSTC2 Int

(equal) :: TraditionalBadSilentTypeConversion->TraditionalBadSilentTypeConversion->Boolean
(equal) TBSTC1 a TBSTC1 b = (a == b)

(equal) TBSTC2 a TBSTC2 b = (a == b)

(equal) TBSTC1 a TBSTC2 b = (a == (intToString b))

(equal) TBSTC2 a TBSTC1 b  = ((intToString a) == b)


例2

data Append x y = Append x y

(equal) :: Append x y->Append z w->Boolean
(equal) (Append a (Append b c)) (Append d (Append e f))
= ((Append (Append a b) c) == (Append (Append d e) f))

(equal) (Append a (Append b c)) (Append d e) = ((Append (Append a b) c) == (Append d e))

(equal) (Append a b) (Append c (Append d e)) = ((Append a b) == (Append (Append b c) e))

(equal) (Append a b) (Append c d)
=if ((sameType a c) && (sameType b d))
 then (a==c && b==d) 
 else False


例1は先ほど批判したいくつかの言語に搭載されている過剰な暗黙の型変換を(あくまで例として)再現したものです。
例2は「「型レベルの文字列」のようなものを作るために、文字列というのは結合則を満たすものなのでAppend (Append A B) CとAppend A (Append B C)という二つの異なる型を同一視(するためにそれらに属するオブジェクトAppend (Append a b) cとAppend a (Append b c)を同一視)したい。」というシチュエーションです。これは前に挙げた「b.構文上異なる型に属するが、数学的な要求により同じであるとみなしたいオブジェクト」の例です。
例1と例2は見た目が結構違いますが、エッセンスは同じであり、

1.暗黙の型変換により変換したい変換前・変換後両方の型を含む型を、直和型・和集合型(直和型と和集合型の違いには注意せよ)(例1)あるいは型変数で量化された型(例2)を用いて作る(ここで作った型をこの記事では便宜上「型変換ラッパー」と呼ぶことにする)。
2.1で作った型の述語や演算をユーザー定義し、場合分けを利用して「型変換させたい値を直接型変換後の値に書き換えた後改めて述語や演算を適用する」ようにする。


というアイデアで「暗黙の型変換もどき」を自作しています。あげた例は両方とも等号を定義する例でしたが、勿論そのほかの述語や演算でも必要に応じて同様に定義することができます。なおここでは「equal(その他必要な述語・演算)を(オーバーライドor型ごとにユーザー定義)できる」という体で書きましたが、それができない言語ならmodifiedEqualとか適当な名前で実装すればいいでしょう。
実用上は1のステップで直和型を用いるか和集合型を用いるかの選択は重要です。
直和型を用いた場合の特徴はユーザーが型変換ラッパーのデータコンストラクタを用いてラッピングを行わない限りは変換が発生しない、「言うほど暗黙でもない変換」だという事です。これには利点と欠点があります。
まず利点は「言うほど暗黙でもない変換」なので暗黙の型変換をしてほしくないときに誤爆する可能性がないことです。一章で指摘した暗黙の型変換の問題点であるバグのリスクが下がるわけです。
逆に欠点は結局いちいちラッピングをするため、一章で説明したような「入力の省略」としての使い方にはそこまで有効ではないという事です。そもそも例を見てわかるように変換の定義も結構面倒くさくなりますし(それでも当たり前みたいな型変換を何重にもかけなきゃいけないような処理をする場合には多少使えるかもしれませんが)。
総じて一章で解説したような素朴な「入力の省略」としての利点・欠点は薄れており、二章で解説したような「自然な同一視」の実装としての側面が強いものです。
逆に和集合型を使えば本当に暗黙の型変換そのものになり、便利な反面バグのリスクは非常に高いと言えるでしょう。
もっとも直和型と和集合型のどちらかしかない言語も多いと思うので選択肢がない場合もあるでしょうが…

4.型変換(によって実装された型同型)による異なる型の同一視

3章の例2についてもう少し考えてみましょう。これは(equal)に関する限り、Append A (Append B C)型とAppend (Append A B) C型とを区別しなくてよい、という事を意味します。
すなわち変換は値レベルで行われていますが、実は型レベルまで同一視が可能なのです。このような状況を「型同型」などと呼んだりし、
\rm Append\ A\ (Append\ B\ C)\leadsto Append\ (Append\ A\ B)\ C
などと書きます。「代数的データ型たちの空間は、原始型を定数とし、型コンストラクタによって生成される項代数だと見做せる」という有名な話がありますが、型同型が実装されることで、型の空間を項代数に限らない、一般的な代数と見做しえることになります。
たとえば今回の定義でいえば、型コンストラクタAppendが結合性を満たすかのように見做せる、ということになります。

5.3章例2のさらなる応用(BNFを表す型)

ここでは3章の例2で導入したAppendを利用して遊んでみましょう。
まずここではsubtypingとnon-discriminated-union-typeがある言語を仮定します。
そして例2では勝手な型変数を取っていたAppendを以下のように制約します。
\rm (forall\ x:x\subset String||x=Append\ a\ b)\Rightarrow(forall\ y:y\subset String||y=Append\ c\ d)\\\Rightarrow Append\ x\ y=Append\ x\ y
(実はこの方のAppendならば上で僕が苦労した挙句ごまかした依存型もどきがいる部分はいらず、単にStringとしての==で比較できるので型の制約とかに見慣れているならこちらのほうがわかりやすい例になる。)
そしてこのAppendに対して以下のappendCollapse関数を定義します。
\rm appendCollapse::(Append\ a\ b||String)\rightarrow String\\appendCollapse\ x\ |\ x::String\ =x\\appendCollapse\ Append\ x\ y=concat\ (appendCollapse\ x)\ (appendCollapse\ y)
ただしダブルバーティカルバーを和集合型とします。この時、appendCollapse関数は例2で定義されたAppend型の等号に対してwell-definedです。なぜならば文字列の結合concatは結合律を満たすからです。言い方を変えるとappendCollapseは例2で定義されたAppend型上の同値類を一意な文字列として解釈します。(なおappendCollapseをStringとAppend型の間の暗黙の型変換にするのはやめたほうが無難です。同じ文字列に対応するAppend型の要素は複数あるため、暗黙の型変換をすると情報が減るという事故の元要素だからです。)
さてここで以下のような性質を持つ型のクラスBを考えてみましょう。

1.任意のStringの有限部分型はBに属する。
2.「Bに属する型にAppendを有限回適用する操作(ただし0回の適用、すなわち何もしないことも許される)で得られる型」有限個の和集合型として得られる型はBに属する。この時Bに属する型同士であれば相互参照があってもよい。特に自己参照があってもよい。


実はBに属する型をappendCollapseで解釈すると、任意のBNFが表現できます。終端記号はStringの有限部分型をすべて含むから表現できますし(なので実際には1の条件は「任意の『1文字文字列を唯一の成分とするシングルトン型』はBに属する。」とかにしても大丈夫です。)、非終端記号はこのようにして作られる型だとみなすわけです。BNFの表記法って結構謎だと思ってたんですが型システムだと思うと妥当ですね(!?)。

6.あとがき

いかがだったでしょうか?
暗黙の型変換という言葉には悪いイメージしかないかもしれませんが、以上のようなコードの数学的自然さを高める使い方もあります。
再評価路線一つお願いします。


こぼれ話をすると、今回のテーマは実は5章の部分で、『論理学友の会』で「BNFの解説公演が聞きたい」という要望があり、「型システムかなにかに帰着させたらわかりやすいんじゃね?」というノリで考え始めたんですが、「異なる型を同一視する方法論」とかnon-discriminated-union-typeとか自分にとってすら初耳の概念が出てきて様々な人に助けられてようやくまとめることができたのですが、引き換えに初心者向けには程遠い内容になった、という経緯があります。
それでは今回も助けていただいた方に感謝を込めて締めたいと思います。

また7/26の「論理学友の会」にてこの記事をテーマにした発表をしたのですが、その後に「型ではなく項代数レベルで考えてはどうか?」という指摘がありました。
僕としては、このテーマについて
・実は型変換によって型の同型\rm Append\ A\ (Append\ B\ C)\leadsto Append\ (Append\ A\ B)\ Cを表現していることにより、同型を同一視したもとに型の空間が項代数ではなく、非自明な等号(実際には同型だが)をもつ空間になること。
BNF再帰的な記法を表現するためには代数的データ型に近いコンセプトが有効だと考えたこと。
が面白いと感じたポイントだったことを付記しておきます。

今回のスペシャルサンクス(twitterネームです):
@emptst 様(「異なる型を同一視する」方法論として「暗黙の型変換」というsuggestionを頂きました。つまりこの方がいなかったら今回の記事はコンセプトが出てきてません。またCoqにユーザー定義の暗黙の型変換があることも教えていただきました。また前述の「論理学友の会」においても発表を助けてくれたり、その後いろいろな意見をくださったりと本当に頭が上がりません。)
@hennin_Itn 様(Haskell素人の僕が疑似コード書くのにいくつか質問させていただきました。)
@Lugendre 様(前述の心が折れて放り投げたライブラリーの情報提供を頂きました。一応あれ使えれば疑似コードじゃなくてもHaskellで例2と同じことができるみたいです。)
@Kory 様(BNF実装のために始めた企画で、僕がnon-discriminated-union-typeの存在を知らなかったため実装に詰まり、暗黙の型変換だけの記事にしようと半分以上諦めていたところに、subtypingを利用したnon-discriminated-union-typeがいくつかの言語(Scalaの新世代の試作品であるScala3、みんな大好きTypeScriptなど)に存在することを教えていただき、一気に光明が見えました。この記事が当初の予定通りの形で完成したのは彼のおかげです。)
その他suggestionを頂いた方々
and YOU!

P.S.今回の記事は今まででトップクラスに内容に自信がないです。大間違いがあったら教えてください。