24
10

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

PureScriptの自然変換について

Last updated at Posted at 2019-05-19

いきさつ

 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 に対して

1280px-Natural_transformation.svg.png

を満たすものとする

とされています。つまり、要は「ある関手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)

となります。先頭要素の1Just に包まれてJust 1となっていますね。

次に、配列が空の場合を試してみます。

  log "-- Empty --"
  let y = []
  log $ show $ trans y

残念ながら、これはコンパイルエラーになりました。yempty なので、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はあるのに。

24
10
3

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
24
10

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?