いきさつ
PureScriptの主要なWebフレームワークであるHalogen(バージョン4)の、サンプルプログラムを見ていると、
eval :: Query ~> H.ComponentDSL State Query Message m
こんな感じの型注釈が登場します。この~>
の意味がよく分からなくて、最初は「->
の誤植か?」と思っていたのですが、記号なのでググるのも難しくて、困っていました。
しかし、よくよく調べてみると、これは誤植ではなく、preludeで定義されている「自然変換」という演算子でした。
ということで、この自然変換 ~>
がなんなのか、これをどう使うのかについてまとめてみました。
ちなみに、Halogen最新のバージョン5では、サンプルプログラムには直接は~>
は出てこないのですが、内部では使われています。
対象
HaskellやPurescriptの初学者向け。
定義
自然変換の定義は、Wikipediaによると
F および G を圏 C から D への函手とするとき、F から G への 自然変換 η は C に属する各対象 X に η の X における成分 (component) と呼ばれる D の射 ηX: F(X) → G(X) を割り当てるものである。ただし ηX は、C の任意の射 f: X → Y に対して
を満たすものとする
とされています。つまり、要は「ある関手Fを、別の関手Gに変換するモノ」であり、上記の可換図式を満たす、ということですね。
プログラム的には、preludeのNaturalTransformation.purs
で定義されていて、
type NaturalTransformation f g = forall a. f a -> g a
infixr 4 type NaturalTransformation as ~>
となっていました。この定義をみると、任意の型a
について、型f a
を型g a
に変換する関数、ということのようです。
可換図式を満たすかどうかはこれだけでは分からないのですが、自己関手の圏では必ず可換図式は満たされるのでしょうか? ここはちょっと分かりませんでした。そもそも、自然変換の可換図式を満たさない例が良く分からなかったので、、、。圏論に詳しい方、コメントいただけると嬉しいです。
また、圏論で言うところの自然変換は「関手を関手に変換」しますが、PureScriptで定義されたNaturalTransformation
では、f
, g
は関手(Functor)とは限定せず、Type -> Type
という型であれば良いとコメントされています。
自然変換を作ってみる
定義だけ読んでいても良く分からないので、とりあえずコードを書いてみます。
で、「関手」を「関手」に変換する関数って、例えばどういうのだろう、、? と思ったのですが、ごく簡単に Array
関手(Array
モナド) を Maybe
関手(Maybe
モナド) に変換する関数を考えてみました。
trans :: Array ~> Maybe
trans arr = case uncons arr of
Just { head: x, tail: xs } -> Just x
_ -> Nothing
この関数は、引数の任意の Array
型変数 arr
が空でなければ、その先頭要素を Just
でくるんで返し、arr
が空であれば、Nothing
を返す、というだけの関数です。
これはつまり、~>
を使わなければ、
trans :: forall a. Array a -> Maybe a
trans arr = case uncons arr of
Just { head: x, tail: xs } -> Just x
_ -> Nothing
と同じです。任意のArray a
を受け取って、Maybe a
を返す、ということですね。
使ってみる
これを使うと何が起こるのか、確認するために使ってみます。
main :: Effect Unit
main = do
log "-- [1,2,3] as Array Int --"
let x = [1,2,3]
log $ show $ trans x
まずは、[1,2,3]
という整数の配列を渡してみます。すると、結果は
-- [1,2,3] as Array Int --
(Just 1)
となります。先頭要素の1
が Just
に包まれてJust 1
となっていますね。
次に、配列が空の場合を試してみます。
log "-- Empty --"
let y = []
log $ show $ trans y
残念ながら、これはコンパイルエラーになりました。y
が empty
なので、Nothing
が返ってきそうなのですが、そもそも「何の」Nothingなのかが判定出来ないからです。つまり、empty
の場合、型が推論出来ないからエラーになってしまったのです。
ちゃんと、型を指定すればコンパイル出来ました。
log "-- Empty as Array Int --"
let y = [] :: Array Int
log $ show $ trans y
これの結果は
-- Empty as Array Int --
Nothing
続いて、文字列の配列を試してみます。
log "-- [\"Hello\", \"Good-Night!\"] as Array String -- "
let z = [ "Hello", "Good-Night!" ]
log $ show $ trans z
これも予想通り、先頭要素である"Hello"
がJust
に包まれて
-- ["Hello", "Good-Night!"] as Array String --
(Just "Hello")
という結果が得られました。
可換図式の確認
続いて、可換図式が成り立つかどうかを試してみます。すべての場合について確認はできないので、例としてある射:X->Y
を考えて、それについて可換図式が成り立つかを考えてみます。PureScriptの圏の対象は「型」なので、ある「型」を別の「型」に変換する関数を考えればよいはずです。ということで、これまた簡単に、Int
型をBoolean
型に変換する関数を射の例としてみます。
projectIntToBoolean :: Int -> Boolean
projectIntToBoolean 1 = false
projectIntToBoolean _ = true
この関数(射)は、受け取った整数が1
ならfalse
を、そうでなければtrue
を返します。
この例で、可換図式を確認するためには、自然変換 trans
、 射projectIntToBoolean
で適用しても、射projectIntToBoolean
、 自然変換 trans
の順で適用しても、同じ結果になればよいわけです。
let x = [1,2,3]
log "-- Natural Transformation for projection Int -> Boolean --"
log $ show $ (projectIntToBoolean <$> trans x)
log $ show $ trans (projectIntToBoolean <$> x)
これの結果は
-- Natural Transformation for projection Int -> Boolean --
(Just false)
(Just false)
となり、同じになりました!
もう一つ、例として Int
型をMaybe Int
型に変換する 次の射を考えてみます。
projectIntToMaybe :: Int -> Maybe Int
projectIntToMaybe x = Just x
(C->D
の関手でではなく、C
での射として考えます)
let x = [1,2,3]
log "-- Natural Transformation for projection Int -> Maybe Int --"
log $ show $ (projectIntToMaybe <$> trans x)
log $ show $ trans (projectIntToMaybe <$> x)
これの結果は、
-- Natural Transformation for projection Int -> Maybe Int --
(Just (Just 1))
(Just (Just 1))
となり、どちらも同じになることが確認できました。
コード全体は
module Main where
import Prelude
import Effect (Effect)
import Effect.Console (log)
import Data.Array
import Data.Maybe
-- import Data.NaturalTransformation
trans :: Array ~> Maybe
trans arr = case uncons arr of
Just { head: x, tail: xs } -> Just x
_ -> Nothing
projectIntToBoolean :: Int -> Boolean
projectIntToBoolean 1 = false
projectIntToBoolean _ = true
projectIntToMaybe :: Int -> Maybe Int
projectIntToMaybe x = Just x
main :: Effect Unit
main = do
log "-- [1,2,3] as Array Int --"
let x = [1,2,3]
log $ show $ trans x
log "-- Empty as Array Int --"
let y = [] :: Array Int
log $ show $ trans y
log "-- [\"Hello\", \"Good-Night!\"] as Array String -- "
let z = [ "Hello", "Good-Night!" ]
log $ show $ trans z
log "-- Natural Transformation for projection Int -> Boolean --"
log $ show $ (projectIntToBoolean <$> trans x)
log $ show $ trans (projectIntToBoolean <$> x)
log "-- Natural Transformation for projection Int -> Maybe Int --"
log $ show $ (projectIntToMaybe <$> trans x)
log $ show $ trans (projectIntToMaybe <$> x)
おわりに
PureScriptで定義されている自然変換~>
について、例をあげて考察してみました。
ちなみに、Halogenの内部では例えば
-- | Changes the [`Component`](#t:Component)'s `m` type. A use case for this
-- | might be to interpret some `Free` monad as `Aff` so the component can be
-- | used with `runUI`.
hoist
:: forall surface query input output m m'
. Bifunctor surface
=> Functor m'
=> (m ~> m')
-> Component surface query input output m
-> Component surface query input output m'
こんな風に使われていて、コメントを読むと、Free MonadをAffとして解釈し、runUIを実行できるようにするために使っているようです。m
は、アクションに含まれるメッセージの関手です。
どうも、自然変換~>
はFree MonadやunsafeCoerceと一緒に出て来ることが多くて、抽象的で難解なイメージがあるのですが、少しずつ理解していきたいと思います、、。
参考:https://qiita.com/hiruberuto/items/3d55b0e54565dbb286a7
記事の内容とは関係ないですが、Qiitaのシンタックスハイライト、PureScriptも対応して欲しいですね、、。elmはあるのに。