8.8 Haskellでの実現例
Haskellは\( \mathbf{Hask} \)と呼ばれる一つの圏で構成されるため、二つの圏を必要とする随伴の例を見ることは少ない(往々にして、関手で\( \mathbf{Hask} \)圏の外に出てしまう)。しかし、積と関数はともに相手方への関手であるため、例外的にHaskellでの随伴の例となる。
二つの局所的に小さな圏\(\mathcal{C},\mathcal{D}\)において、関手の対\(R: \mathcal{C} \rightarrow \mathcal{D}, L: \mathcal{D} \rightarrow \mathcal{C}\)が次の条件を満たす時、随伴である。
\begin{eqnarray}
η & :& I_\mathcal{D} \rightarrow R \circ L \\
ϵ &:& L \circ R \rightarrow I_\mathcal{C}
\end{eqnarray}
それでは、下図を参考にして、積を左随伴関手、関数を右随伴関手とする随伴をHaskellで実現することを考えよう。
まず積の関手を用意しよう。Haskellでは関手は新しいデータ型として定義される。ここでは、\(new type\)を用いて、積の関手\(Prod\)を定義しよう。また、積は固定値\(s\)に変数\(a\)をかけたものとし、これを対で表すことにしよう。
Newtype Prod s a = Prod (a, s)
次に関数の関手\(Reader\)を用意しよう。これは\(s\)を入力とし、\(a\)を出力とする関数としよう。
Newtype Reader s a = Reader (s -> a)
ここで、\(s\)は環境(environment)と見なすことができる。
それでは随伴を用意しよう。\(η\)という関数は、Haskellでは \(unit\)という関数名である。そこで、これを使うと次のようになる。
unit :: a -> Reader s (Prod s a) unit a = Reader (\s -> Prod (a,s))
\(unit\)が状態を表すモナドとなっていることに注意しよう。
また、\(ϵ\)という関数は、Haskellでは \(counit\)という関数名である。そこで、これを使うと次のようになる。
counit :: Prod s (Reader s a) -> a counit (Prod (Reader f, s)) = f s
但し、\(f : s \rightarrow a\)である。
それではプログラムをまとめよう。\(Prod \ s\)を左随伴関手として定義するためには、これを関手として定義する必要がある。同じように、\(Reader \ s\)を右随伴関手として定義するためには、これを関手、および、表現可能関手として定義する必要がある。表現可能関手として定義するときは、\(Reader\)のソース側のデータ型を定める必要があるが、これは、\(Reader \ s\)のデータ型が\(s\)のデータ型と同じであることに注意して定義すると以下のようになる(しばらくこれに気がつかず、\(Rep (Reader \ s)\)を\(Double\)と定義したりなどしてしまった)。
プログラムには実行例も示してあるので、利用して欲しい。
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} class (Functor f, Representable u) => Adjunction f u where unit :: a -> u (f a) counit :: f (u a) -> a class Representable f where type Rep f :: * tabulate :: (Rep f -> x) -> f x index :: f x -> Rep f -> x newtype Prod s a = Prod (a , s) newtype Reader s a = Reader (s -> a) instance Functor (Prod s) where fmap f (Prod (a , s)) = Prod (f a , s) instance Functor (Reader s) where fmap f (Reader h) = Reader (f . h) instance Representable (Reader s) where type Rep (Reader s) = s tabulate f = Reader (\x -> f x) index (Reader f) x = f x a = tabulate sin :: Reader Double Double --index a 1.5 instance Adjunction (Prod s) (Reader s) where -- unit :: a -> Reader s (Prod s a) unit a = Reader (\s -> Prod (a , s)) -- counit :: Prod s (Reader s a) -> a counit (Prod (Reader f , s)) = f s b = unit 2.3 :: Reader Double (Prod Double Double) c = counit (Prod (Reader sin, 2.3 :: Double)) :: Double