形式検証の視点から再確認したいMaybe型/Option型からnull許容データベースへのデータ変換

#はじめに

本記事は第一回関数型プログラミング(仮)の会における発表内容の詳細です。

関数型言語において、Maybe/Option型データを外部データベースに保存する際やJSONに変換する際、NULL許容データに変換して扱われることが多いです。
しかしながら、Maybe/Option型とNULL許容データは細かい点で異なるため、注意してデータ変換を実装しないと思わぬバグを生むことになります。

そこで本記事では、Maybe/Option型をNULL許容データに変換することに対して、形式検証の視点から考察していきます。

また、Haskellによる実装例もありますので、コードを確認したい方はそちらも参考にしていただけると幸いです。

#形式検証による視点
形式検証を考える際に必要なのは、プログラムの仕様を論理式で形式的に記述することです。
今回は、まずデータ変換自体の数学的なモデルを考えて、その後、Haskellでの実装を見ていきます。
(数式をインライン表示したときに勝手に改行が入る場合があり、読みづらい点がありますがご了承ください。)

##データ変換の数学的なモデル

$\operatorname{DB}$をデータベースで表現できるデータの集合、型全体の集合$\operatorname{Type}$とし、$\operatorname{Conversible} : \operatorname{Type} \to \{\top,\bot\}$をデータベース型へ変換可能な型であるという述語、つまりHaskellでいうところのinstanceとすると、
データベースへの型変換 $\operatorname{toDB}$とデータベース型からの型変換 $\operatorname{fromDB}$は以下のような型を持ちます。

\operatorname{toDB} : \forall T, \operatorname{Convertible} T \to T \to \operatorname{DB}

\operatorname{fromDB} : \forall T, \operatorname{Convertible} T \to \operatorname{DB} \to \operatorname{Result} T

図にすると以下のようになります。

ここで$\operatorname{Convertible} T$は命題であるのにも関わらず型として扱っているのは、Carry-Howard同型対応によって、数学における命題はプログラムの世界の型と1対1対応するからです。実際にこの表現は形式検証ツールの1つである定理証明支援系Coqで認められている記法であり、Haskellにおけるinstanceの記法にもよく似ています。

また、$\operatorname{fromDB}$の返り値の型が$T$ではなく$\operatorname{Result} T$であるのは、全てのデータベースのデータが$T$型に変換できるわけではないためです。
その代わりに$T$型と$\operatorname{Result} T$型との関係として単射$f_T : T \to \operatorname{Result} T$を与えています。
この$f_T$によって、$T$型の入力に対してnull許容データに変換したものを"元に戻す"ことの意味を表現できるようになります。

このように抽象化すると分かりづらいかもしれませんが、実際のプログラムでは$\operatorname{Result} T$として具体的に型変換できないエラーを表現するための適当な集合$E$を固定した時の直和$E + T$を与えることが多いです。¹

このとき、自然な写像$f : \forall T, T \to E + T$が単射になります。

式だけで記述すると分かりづらいかもしれないので、次に具体的にHaskellでのJSONへの変換の実装を見てみます。

###Haskellでの実装

例として、HaskellでのJSONへの変換の例を見ていきます。
Data.AesonではJSONへの変換が以下のように定義されています。¹

class toJSON a where
  toJSON :: a -> Value
-- 以下略

class fromJSON a where
  parseJSON :: Value -> Result a
-- 以下略

data Result a = Error String
              | Success a
                deriving (Eq, Show, Typeable)

Valueがデータベースに格納するデータの型を表しています。

instanceはToJSONとFromJSONの2つありますが、これらを両方満たすものが上の$\operatorname{Conversible}$に対応します。

そして、toJSONが$\operatorname{toDB}$、
fromJSONが$\operatorname{fromDB}$に対応しています。

また、Result aは直和$\operatorname{Text} +,a$に対応していて、
また、任意の型aに対し、コンストラクタSuccess :: a -> Result aは明らかに単射なので、上記の制約を満たしています。

##データ変換の仕様

データ変換における仕様を論理式で表していきます。

満たしてほしい性質は、

• データ変換して元の型に戻したときに、変換前のデータに戻ること。
• データベース上のデータをある型に変換できるならば、それを再変換すると元のデータベース上のデータに戻ること。

です。実際には戻り値の型が$\operatorname{Result}$型になることに注意すると、この性質は論理式でそれぞれ

\forall T, \operatorname{Convertible} T \to \operatorname{fromDB}_T \circ \operatorname{toDB}_T = f_T

\forall T, \operatorname{Convertible} T \to \forall d \in \operatorname{DB}, \forall x \in T, \operatorname{fromDB}_T d = f_T x \to d = \operatorname{toDB}_T x

を満たすことと言えます。

ちなみに2つ目の仕様は1つ目の仕様を仮定すると以下の命題と同値になります。

\forall T, \operatorname{Convertible} T \to \operatorname{fromDB}_T^{-1} (\operatorname{Im} f_T) \subset \operatorname{Im}\operatorname{toDB}_T

###仕様を満たすための十分条件

上記の仕様を満たす$\operatorname{toDB}$と$\operatorname{fromDB}$を定義したいわけですが、
実は以下を仮定すると、これらの仕様が成り立つ$\operatorname{fromDB}$が存在することが示せます。
すなわち、以下が仕様を満たすための十分条件であることが言えます。

• $\operatorname{toDB}$が単射
• $\forall T, \operatorname{Convertible} T \to \operatorname{Result} T = \emptyset \to \operatorname{DB} = \emptyset$
• $\forall T, \operatorname{Convertible} T \to \operatorname{Im} f_T = \operatorname{Result} T \to \operatorname{Im}\operatorname{toDB}_T = \operatorname{DB}$
• 選択公理

この4つの条件のうち、2つ目と3つ目は$\operatorname{Result} T$の構成によって成立させることが可能です。
例えば、空でない型$E$に対し、$\operatorname{Result} T := E + T$、単射$f_T$を自然な単射と定義してしまえば$\operatorname{DB} = \emptyset$でない限り満たすことができます。

また、4つ目に選択公理が仮定されていますが、実は証明において$\operatorname{fromDB}$自体の存在性は示せますが、一般にはその構成的な実装が存在するとは限りません。
しかしながら、これから定義する$\operatorname{toDB}$に対しては、仕様を満たす$\operatorname{fromDB}$を構成的に定義することが可能です。(本記事ではHaskellでこちらも同時に実装していきます。)

よって、単射となるような$\operatorname{toDB}$と、その逆変換$\operatorname{fromDB}$が構成的に定義できるような関数を考えれば、仕様を満たすデータ変換を構成することが可能です。

#Maybe型からnull許容データへの変換

ここから、Maybe型やOption型からnull許容データへの変換がこの仕様を満たしているかどうかをみていきます。

まず、最もシンプルな実装を考えてみます。

##シンプルな実装

データ変換可能な型を表すinstanceを$\operatorname{Convertible}$で表し、Maybe型に対するinstanceを次のように定義します。

\forall T, \operatorname{Convertible} T \to \operatorname{Convertible}\, (\operatorname{Maybe} T)

このとき、任意の$\operatorname{Convertible}$な型$T$に対して$\operatorname{toDB}_{\operatorname{Maybe} T}$を以下のように定義します。

\begin{matrix}
\operatorname{Maybe} T & \overset{\operatorname{toDB}_{\operatorname{Maybe} T}}{\longrightarrow} & \operatorname{DB}\\
\operatorname{Nothing} & \longmapsto & \operatorname{Null}\\
\operatorname{Just} x & \longmapsto & \operatorname{toDB}_T x
\end{matrix}

この定義はHaskellのData.Aesonと同じ結果を返す定義となっています。

Data/Aeson/Types/ToJSON.hs

class ToJSON1 f where
  liftToJSON1 :: (a -> Value) -> ([a] -> Value) -> f a -> Value
-- 以下略

instance ToJSON1 Maybe where
  liftToJSON t _ (Just a) = t a
  liftToJSON _ _ Nothing = Null
-- 以下略

toJSON1 :: (ToJSON1 f, ToJSON a) => f a -> Value
toJSON1 = liftToJSON toJSON toJSONList

instance ToJSON a => ToJSON (Maybe a) where
  toJSON = toJSON1
-- 以下略

しかしながら、この定義は上の仕様を満たしません。²

###仕様を満たさない理由

もう一度、仕様1として与えた論理式を確認します。

\forall T, \operatorname{convertible} T \to \operatorname{fromDB}_T \circ \operatorname{toDB}_T = f_T

任意の型$T$に対して、$f_T$が単射であるので、この仕様を満たすためには$\operatorname{toDB}_T$が単射である必要があります。

しかしながら、上で定義した$\operatorname{toDB}_{\operatorname{Maybe} T}$は一般に単射にはなりません。

それは$\operatorname{ToDB}_{\operatorname{Maybe} T},(\operatorname{Just} x) = \operatorname{toDB}_T x$が$\operatorname{Null}$になる可能性があるからです。

具体的には、任意の$T$に対して、

\operatorname{toDB}_{\operatorname{Maybe}\,(\operatorname{Maybe} T)} \,(\operatorname{Just}\operatorname{Nothing}) =
\operatorname{toDB}_{\operatorname{Maybe}\,(\operatorname{Maybe} T)} \operatorname{Nothing} =
 \operatorname{Null}

であり、$\operatorname{Just} \operatorname{Nothing} \neq \operatorname{Nothing}$より単射にはなりません。

なぜシンプルかと思われた変換が仕様を満たさないかというと、実はMaybe型やOption型とnull許容データには大きな違いがあるからです。

#Maybe型やOption型とnull許容データとの違い

Maybe型とnull許容データについて、もう一度確認してみます。
任意の型$T$に対して、それぞれ以下のように分解できます。

\begin{matrix}
\operatorname{Maybe} T& & \operatorname{nullable} T\\
\operatorname{Nothing} & & \operatorname{Null}\\
\operatorname{Just} x & & x
\end{matrix}\\
(x \in T)

一見すると$\operatorname{Nothing}$と$\operatorname{Null}$が対応していそうですが、実はここに決定的な違いがあります。
それは、$\operatorname{Nothing}$自身はMaybe型を持つため$\operatorname{Just}$の引数として取ることができ、$\operatorname{Just} \operatorname{Nothing}$と$\operatorname{Nothing}$は区別されますが、
$\operatorname{Null}$自体は値ではなく$x$に代入できない、もしくは値としての$\operatorname{Null}$と$\operatorname{Null}$自身を区別できないという点です。

すなわち、Maybe型の$\operatorname{Just}\operatorname{Nothing}$に対応するnull許容データが存在しないということです。

そこで、Maybe型とnull許容データの違いを踏まえて、仕様を満たす2通りのデータ変換の実装を考えていきます。

##仕様を満たす実装1

1つ目のアイデアは、Maybe型やOption型を1つのEither型や直和型として考え、Either型のデータ変換に帰着するというものです。

実際にMaybe Tを数学で表すと$1+T$³であり、Either E Tが$E + T$と表せるため、Maybe型はEither型の1つと考えることができます。

そこで、Either型のデータ変換の実装を見ると、

\begin{matrix}
\operatorname{Either} X\,Y & \overset{\operatorname{toDB}_{\operatorname{Either} X\,Y}}{\longrightarrow} & \operatorname{DB}\\
\operatorname{Left} x & \longmapsto & (\text{"Left"},\operatorname{toDB}_X x)\\
\operatorname{Right} y & \longmapsto & (\text{"Right"},\operatorname{toDB}_Y y)
\end{matrix}

となっているため、Maybe型も同様に

\begin{matrix}
\operatorname{Maybe} T & \overset{\operatorname{toDB}_{\operatorname{Maybe} T}}{\longrightarrow} & \operatorname{DB}\\
\operatorname{Nothing}& \longmapsto & (\text{"Nothing"},\operatorname{Null})\\
\operatorname{Just} x & \longmapsto & (\text{"Just"},\operatorname{toDB}_T x)
\end{matrix}

というように定義できます。

この定義ならば、$\operatorname{toDB}_{\operatorname{Maybe} T}$の単射性は$\operatorname{toDB}_T$の単射性に帰着でき、型の構成に関する帰納法から示すことができます。

しかしながらこの実装は、データベースにおけるnull許容データをそのままMaybe型には変換できないデメリットがあります。すなわち

\begin{matrix}
X & \overset{\operatorname{toDB}_X}{\longrightarrow} & \operatorname{nullable} T\\
? & \longmapsto & \operatorname{Null}\\
? & \longmapsto & y
\end{matrix}\\
(y \in T)

となる$X$としてMaybe型が与えられなくなってしまうので、$\operatorname{Null}$を含むデータベース上のデータが扱いづらくなります。

そこで、シンプルな実装と同じ変換を保ちつつ、単射性も満たすような実装を考えていきます。

##仕様を満たす実装2
もう1つのアイデアはinstanceを変更し、Maybeの型引数として与えるデータの型を制限することです。

もう一度、Maybe型とnull許容データについてみていきましょう。

\begin{matrix}
\operatorname{Maybe} T& & \operatorname{nullable} T\\
\operatorname{Nothing} & & \operatorname{Null}\\
\operatorname{Just} x & & x
\end{matrix}\\
(x \in T)

$\operatorname{nullable} T$における$x$には$\operatorname{Null}$を代入することができないので、$\operatorname{Just}$の引数を$\operatorname{toDB}_T$したときに$\operatorname{Null}$にならないものに制限するというアイデアです。

###具体的には

新たなinstance $\operatorname{NotNullConvertible}$を定義します。

このinstanceは$\operatorname{Null}$にならないデータベースのデータに変換可能な型を表していて、通常のデータ変換

\operatorname{toDB} : \forall T, \operatorname{Convertible} T \to T \to \operatorname{DB}

の代わりに、返り値が$\operatorname{Null}$にならないようなデータ変換

\operatorname{toDBValue} : \forall T, \operatorname{NotNullConvertible} T \to T \to \operatorname{DBValue}

を定義します。
ただし、$\operatorname{DBValue}$はデータベースの$\operatorname{Null}$単体を除いた集合として定義し、具体的には

\operatorname{DBValue} = \operatorname{DB}\backslash\{\operatorname{Null}\}

を満たすものとします。
このとき、$\operatorname{DB}$は$\operatorname{DBValue}$に1点追加した集合であり$\operatorname{Maybe} \operatorname{DBValue}$と1対1対応します。
そこで、

\operatorname{DB} := \operatorname{Maybe} \operatorname{DBValue}

と再定義し、$\operatorname{Null} := \operatorname{Nothing} \in \operatorname{DB}$として扱います。

このときMaybe型のデータ変換をinstanceを

\operatorname{NotNullConvertible} T \to \operatorname{Convertible}\,(\operatorname{Maybe} T)

とし、

\operatorname{toDB}_{\operatorname{Maybe} T} := \operatorname{fmap}_{\operatorname{Maybe}} \operatorname{toDBValue}_T

と定義します。⁴

\begin{matrix}
\operatorname{Maybe} T & \overset{\operatorname{toDB}_{\operatorname{Maybe} T}}{\longrightarrow} & \operatorname{DB}\\
\operatorname{Nothing} & \longmapsto & \operatorname{Nothing}\, (=\operatorname{Null})\\
\operatorname{Just} x & \longmapsto & \operatorname{Just}\, (\operatorname{toDBValue}_T x)
\end{matrix}

であり、これはシンプルな定義の実装と一致します。

さらに$\operatorname{toDB}_{\operatorname{Maybe} T}$の単射性は${\operatorname{toDBValue}_T}$の単射性に帰着するので、仕様を満たすことが分かります。

これからこの定義を実際にHaskellで実装していきます。

###Haskellによる実装

HaskellのJSONへの変換を参考にしながらオリジナルの変換を作っていきます。

まず、Data.Aesonにおけるデータベースで表現できるデータValueは以下のように定義されています。

Data/Aeson/Types/Internal.hs

type Object = HashMap Text Value
type Array = Vector Value

data Value = Object !Object
           | Array !Array
           | String !Text
           | Number !Scientific
           | Bool !Bool
           | Null
             deriving (Eq, Read, Typeable, Data, Generic)

型ObjectやArrayの定義はValueに依存するため、帰納的な定義になっています。

これに対して、Nullを除いたデータを仮にDBValueとして定義します。

-- 仮定義
data DBValue = DBObject !Object
             | DBArray !Array
             | DBString !Text
             | DBNumber !Scientific
             | DBBool !Bool
               deriving (Eq, Read, Typeable, Data, Generic)

ここでポイントなのは、型ObjectやArrayの定義をValueのときのままにしておくことです。これは、今欲しいのはValueから単体のNullのみを排除した型であって、例えば要素にNullを含むリストなど、Null単体ではないものはそのまま記述できるようにするためです。

このとき、ValueはMaybe DBValueと等価になるので、ObjectとArrayの定義をMaybe DBValueに変更したもので再定義します。

type DBObject = HashMap Text NullableDB
type DBArray = Vector NullableDB

type NullableDB = Maybe DBValue

data DBValue = DBObject !DBObject
             | DBArray !DBArray
             | DBString !Text
             | DBNumber !Scientific
             | DBBool !Bool
               deriving (Eq, Read, Typeable, Data, Generic)

dBNull :: NullableDB
dBNull = Nothing

このとき、元のValueに対応する型としてNullableDBという名前をつけます。

そこで、データ変換toDBとnullにならないデータ変換toDBValue、それぞれの逆変換fromDBとfromDBValue、それぞれの変換を含むinstanceであるDBConvertibleとDBValueConvertibleを定義します。

-- nullable
class DBConvertible a where
    toDB :: a -> NullableDB
    fromDB :: NullableDB -> Result a

-- not nullable
class DBValueConvertible a where
    toDBValue :: a -> DBValue
    fromDBValue :: DBValue -> Result a

このとき、DBValueConvertibleからDBConvertibleへの自然な変換が存在します。
(ただし、この変換の実装は非推奨。後述するようにDBConvertible (Maybe (Maybe a))を定義する際、これを定義してしまうと型推論が一意に定まらなくなるため。)

-- 型推論の観点から非推奨。
-- DBValueConvertibleな任意の型に対して、それぞれDBConvertibleを定義すること。
instance DBValueConvertible a => DBConvertible a where
    toDB = Just . toDBValue
    fromDB = maybe (Error "expected not null") fromDBValue

-- maybe :: b -> (a -> b) -> Maybe a -> b

したがって、各DBValueConvertibleな型に対してそれぞれDBConvertibleを定義します。

-- Bool
instance DBValueConvertible Bool where
    toDBValue = DBBool
    fromDBValue (DBBool b) = Success b
    fromDBValue _ = Error "expected a bool"

instance DBConvertible Bool where
    toDB = Just . toDBValue
    fromDB = maybe (Error "expected not null") fromDBValue

-- 他のDBValueConvertibleな型に対しても同様にDBConvertibleを定義する

これで準備は完了です。

---

ここからMaybeに関するDBConvertibleを定義します。

instance DBValueConvertible a => DBConvertible (Maybe a) where
   toDB = (<$>) toDBValue
   fromDB = maybe (Success Nothing) ((<$>) Just . fromDBValue)

-- (<$>) :: Functor f => (a -> b) -> f a -> f b

DBValueConvertible a、すなわちNullにならない型変換が存在する型aに対してDBConvertible (Maybe a)を定義しています。

このとき、Maybe aに対するデータ変換が仕様1であるfromDB . toDB == Successを満たすことは、型aにおける変換が仕様1を満たすこと、すなわちfromDBValue . toDBValue == Successを仮定すれば示せます。

また、任意のx :: a、y :: DBValueに対してSuccess x == fromDBValue y -> y == toDBValue xを仮定すると、
任意のx :: Maybe a、y :: NullableDBに対してSuccess x == fromDB y -> y == toDB xが成り立つので、仕様2も満たしています。

###Maybe (Maybe a)の場合も定義する

この定義では、DBConvertible (Maybe (Maybe a))が定義されません。むしろ、引数がNullにならないものに限定し、Maybe (Maybe a)を回避することで仕様を保つというのがこの定義のアイデアでした。

しかしながら、Maybe (Maybe a)型に対しても仕様を保ちつつデータ変換する方法があります。

考え方としては、今DBValueConvertible a => DBConvertible (Maybe a)があるので、DBConvertible (Maybe (Maybe a))を作るためにはDBValueConvertible (Maybe a)を定義してしまえばいいということです。

instance DBValueConvertible a => DBValueConvertible (Maybe a) where
    toDBValue Nothing = DBObject $ H.fromList [("Nothing", Nothing)]
    toDBValue (Just x) = DBObject $ H.fromList [("Just", Just (toDBValue x))]

    fromDBValue (DBObject (H.toList -> [(key,value)]))
        | key == nothing = Success Nothing
        | key == just = Just <$> maybe (Error "error") fromDBValue value
        where
            nothing, just :: Text
            nothing = "Nothing"
            just = "Just"
    fromDBValue _ = Error "expected an object"

具体的にはDBValueConvertible aから返り値がNullにならないようなMaybe a型のデータ変換toDBValueを与えます。実際には仕様を満たす実装1で定義した方針、すなわちEither型と同様にMaybe型もオブジェクトに変換する方法で定義します。

この定義によって、Maybe (... (Maybe (Maybe a)) ...)型の変換は一番外側のMaybe型のみtoDBを適用しシンプルな変換を、その中に連続するMaybe型はtoDBValueによってEither型と同じ方針による変換を行います。

###型推論に関する注意点

上記のように、外側のMaybeと内側のMaybeの変換の実装が異なるため、もし自然な変換DBValueConvertible a => DBConvertible aを定義してしまうと、
DBValueConvertible aからDBConvertible (Maybe a)への型推論が以下の2通り存在してしまい、一意に定まらなくなります。

• DBValueConvertible a => DBConvertible (Maybe a)を直接適用したもの。
• DBValueConvertible a => DBValueConvertible (Maybe a)とDBValueConvertible (Maybe a) => DBConvertible (Maybe a)から推移的に導かれるもの。

下の型推論だとtoDBが実装2の方針ではなく、実装1のみを使用した定義になります。
したがって、DBValueConvertible a => DBConvertible aは任意の型aに対しては定義せずに個別の型に対してそれぞれDBConvertibleを定義するか、Maybe型に関する型推論はDBValueConvertible a => DBConvertible (Maybe a)を優先するように定義する必要があります。

#まとめ
Maybe型やOption型からnull許容データベースへの型変換の実装について、形式検証の観点から数学的に見ていきました。
Maybe型とnul許容データは一見似ているのでそのまま対応させがちですが、厳密には1対1対応しているわけではないため、これらの間の変換には注意が必要であることがわかりました。

1. Maybe型を与えることもありますが、これは直和型$\{\emptyset\}+T$として考えることができます。
   つまり、データ変換ができる場合は$T$型を返し、変換できないデータの場合は$E$型を返すという実装にすることが多いです。 ↩ ↩²

2. この問題点はすでに報告されていますが、これを修正するには大きな仕様変更が予想され、すでに多くの人が利用していることから変更せずにそのままになっています。 ↩

3. ただし順序数$1 := \{\emptyset\}$ ↩

4. $\operatorname{fmap} : \forall f, \operatorname{Functor} f \to \forall T,S, (T \to S) \to f,T \to f,S$
   すなわち、 ↩