10

パッケージのFreeデータ型を使用してControl.Monad.Freeいます。free今、私はそれを変換して使用しようとしてFいControl.Monad.Free.Churchますが、関数をマップする方法がわかりません。

たとえば、 を使用した単純なパターン マッチング関数Freeは次のようになります。

-- Pattern match Free
matchFree
  :: (a -> r)
  -> (f (Free f a) -> r)
  -> Free f a
  -> r
matchFree kp _ (Pure a) = kp a
matchFree _ kf (Free f) = kf f

-とのF間で変換して使用する関数に簡単に変換できます。Free

-- Pattern match F (using toF and fromF)
matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r
matchF kp kf = matchF' . fromF
  where
    matchF' (Pure a) = kp a
    matchF' (Free f) = kf (fmap toF f)

toFただし、使用せずにそれを実行する方法がわかりませんfromF-

-- Pattern match F (without using toF)???
-- Doesn't compile
matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r
matchF kp kf f = f kp kf

私が見逃している一般的なパターンがあるに違いありません。それを理解するのを手伝ってもらえますか？

4

4 に答える 4

10

あなたは「欠けている一般的なパターン」を求めました。Petr Pudlákの答えもかなり良いですが、それを説明するために私自身の試みをさせてください. user3237465 が言うように、使用できるエンコーディングには Church と Scott の 2 つがあり、Church ではなく Scott を使用しています。というわけで、総評です。

エンコーディングの仕組み

継続渡しにより、型の任意の値を型xの一意の関数で記述することができます

data Identity x = Id { runId :: x } 
{- ~ - equivalent to - ~ -} 
newtype IdentityFn x = IdFn { runIdFn ::  forall z. (x -> z) -> z }

ここでの "forall" は非常に重要です。この型はz未指定のパラメーターとして残されるということです。全単射とは、からからId . ($ id) . runIdFnへIdentityFn、逆IdentityにIdFn . flip ($) . runId行くということです。等価性が生じるのは、基本的に type でできることは何もforall z. zなく、操作が十分に普遍的ではないためです。newtype UnitFn = UnitFn { runUnitFn :: forall z. z -> z }は 1 つの要素、つまり のみを持つと同等に述べることができます。これは、同様UnitFn idにユニット タイプに対応することを意味します。data Unit = Unit

(x, y) -> zに同型なカリー化観測x -> y -> zは、データ構造を持たない純粋な関数の観点からデータ構造を表すことを可能にする継続通過氷山の一角Identity (x, y)ですforall z. (x -> y -> z) -> z。したがって、2 つのアイテムを「接着」することは、この型の値を作成することと同じであり、純粋な関数を「接着」として使用するだけです。

この同等性を確認するには、他の 2 つのプロパティを処理する必要があります。

1 つ目は、 の形式の合計型コンストラクターですEither x y -> z。ほら、Either x y -> z同形です

newtype EitherFn x y = EitherFn { runEitherFn :: forall z. (x -> z) -> (y -> z) -> z }

そこから、パターンの基本的なアイデアが得られます。

  1. z式の本体に表示されない新しい型変数を取得します。
  2. データ型のコンストラクターごとに、そのすべての型引数をパラメーターとして取り、. を返す関数型を作成しますz。コンストラクターに対応するこれらの「ハンドラー」を呼び出します。したがって、 のハンドラ(x, y)は(x, y) -> zにカリー化されx -> y -> z、 のハンドラLeft x | Right yはx -> zおよびy -> zです。パラメーターがない場合はz、より面倒な ではなく、値を関数として使用できます() -> z。
  3. これらのハンドラーをすべて式のパラメーターとして受け取りますforall z. Handler1 -> Handler2 -> ... -> HandlerN -> z。
  4. 同形の半分は、基本的に、コンストラクターを目的のハンドラーとして渡すことです。もう一方はコンストラクターでパターン マッチし、対応するハンドラーを適用します。

微妙に欠けているもの

繰り返しになりますが、これらのルールをさまざまなものに適用するのは楽しいものです。たとえば、上で述べたように、これを適用するdata Unit = Unitと、任意の単位タイプが恒等関数forall z. z -> zであることがわかります。これを適用するとdata Bool = False | True、論理関数forall z. z -> z -> zwhere false = constwhileが見つかりますtrue = const id。しかし、実際に遊んでみると、まだ何かが足りないことに気付くでしょう。ヒント: 見てみると

data List x = Nil | Cons x (List x)

パターンは次のようになります。

data ListFn x = ListFn { runListFn :: forall z. z -> (x -> ??? -> z) -> z }

いくつかのために???。上記のルールは、何がそこにあるのかを特定するものではありません。

2 つの適切なオプションがあります: の能力をnewtype最大限に活用してそこに配置するか (「Scott」エンコーディング)、または与えられた関数を使用ListFn xしてプリエンプティブに削減することができます。z私たちがすでに持っている機能（「教会」エンコーディング）。再帰はすでに事前に実行されているため、Church エンコーディングは有限データ構造に対してのみ完全に同等です。Scott エンコーディングは、無限リストなどを処理できます。チャーチ形式で相互再帰をエンコードする方法を理解するのも難しい場合がありますが、スコット形式は通常もう少し簡単です。

いずれにせよ、Church エンコーディングについて考えるのは少し難しいですが、希望的観測でアプローチすることができるので、もう少し魔法のようzです。仕方。" そして、この希望的観測はまさに、この全単射の一方の側がまさにリストの側であるため、人々が理解に苦労する理由です。tail listhead listfoldrfoldr

他にも「コンストラクターの数が多かったり無限だったりしたらどうなるの?」というIntような問題があります。Integerこの特定の質問に対する答えは、関数を使用することです

data IntFn = IntFn { runIntFn :: forall z. (z -> z) -> z -> z }

これは何ですか？さて、賢い人 (教会) は、これが構成の繰り返しとして整数を表現する方法であることに気付きました。

zero f x = x
one f x = f x
two f x = f (f x)
{- ~ - increment an `n` to `n + 1` - ~ -}
succ n f = f . n f

実際、このアカウントm . nは 2 つの製品です。()しかし、私がこれについて言及するのは、 a を挿入して引数を反転させて、これが実際にはで与えられた値と で与えられた加算と で与えられた乗算を持つforall z. z -> (() -> z -> z) -> zリスト型であることを見つけるのはそれほど難しくないからです。[()]length++>>

効率を高めるためにdata PosNeg x = Neg x | Zero | Pos x、Church エンコードし、Church エンコードを使用して (有限のままにします!)、それぞれが最後に最も重要なビットで明示されていない状態で暗黙的に終了する場所[Bool]の Church エンコードを形成することができます。 +1 から無限に。PosNeg [Bool][Bool]True[Bool]

拡張例: BinLeaf / BL

もう 1 つの重要な例として、すべての情報を葉に格納するバイナリ ツリーについて考えることができますが、内部ノードには注釈も含まれますdata BinLeaf a x = Leaf x | Bin a (BinLeaf a x) (BinLeaf a x)。Church エンコーディングのレシピに従って、次のことを行います。

newtype BL a x = BL { runBL :: forall z. (x -> z) -> (a -> z -> z -> z) -> z}

Bin "Hello" (Leaf 3) (Bin "What's up?" (Leaf 4) (Leaf 5)インスタンスを小文字で構築する代わりに、次のようにします。

BL $ \leaf bin -> bin "Hello" (leaf 3) (bin "What's up?" (leaf 4) (leaf 5)

したがって、同型は非常に簡単ですbinleafFromBL f = runBL f Leaf Bin。反対側はケース発送がありますが、悪くないです。

再帰データに対する再帰アルゴリズムはどうですか? ここが魔法のようです。foldrそしてrunBL、Church のエンコーディングは、ツリー自体に到達する前に、サブツリーで実行されていた関数を両方とも実行しました。たとえば、この関数をエミュレートしたいとします。

sumAnnotate :: (Num n) => BinLeaf a n -> BinLeaf (n, a) n
sumAnnotate (Leaf n) = Leaf n
sumAnnotate (Bin a x y) = Bin (getn x' + getn y', a) x' y' 
    where x' = sumAnnotate x
          y' = sumAnnotate y
          getn (Leaf n) = n
          getn (Bin (n, _) _ _) = n

やらなければいけないことは何？

-- pseudo-constructors for BL a x.
makeLeaf :: x -> BL a x
makeLeaf x = BL $ \leaf _ -> leaf x

makeBin :: a -> BL a x -> BL a x -> BL a x
makeBin a l r = BL $ \leaf bin -> bin a (runBL l leaf bin) (runBL r leaf bin)

-- actual function
sumAnnotate' :: (Num n) => BL a n -> BL n n
sumAnnotate' f = runBL f makeLeaf (\a x y -> makeBin (getn x + getn y, a) x y) where
    getn t = runBL t id (\n _ _ -> n)

関数を渡します\a x y -> ... :: (Num n) => a -> BL (n, a) n -> BL (n, a) n -> BL (n, a) n。ここでは、2 つの「引数」が「出力」と同じタイプであることに注意してください。Church エンコーディングでは、すでに成功しているかのようにプログラミングする必要があります。これは「希望的観測」と呼ばれる規律です。

Free モナドの Church エンコーディング

Free モナドは正規形

data Free f x = Pure x | Roll f (Free f x)

そして、私たちの教会のエンコーディング手順は、これが次のようになると言います:

newtype Fr f x = Fr {runFr :: forall z. (x -> z) -> (f z -> z) -> z}

あなたの機能

matchFree p _ (Pure x) = p x
matchFree _ f (Free x) = f x

単純になる

matchFree' p f fr = runFr fr p f
于 2015-07-14T21:50:38.860 に答える
4

君の

matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r

Scott でエンコードされた Free モナドのように見えます。教会でエンコードされたバージョンは、

matchF
  :: Functor f
  => (a -> r)
  -> (f r -> r)
  -> F f a
  -> r
matchF kp kf f = runF f kp kf

比較のために、Church と Scott でエンコードされたリストを次に示します。

newtype Church a = Church { runChurch :: forall r. (a -> r       -> r) -> r -> r }
newtype Scott  a = Scott  { runScott  :: forall r. (a -> Scott a -> r) -> r -> r }
于 2015-07-14T20:18:36.947 に答える
3

ちょっと意地悪ですね。この問題は、教会の数字としてエンコードされた自然数の前身 ( と考えてください) を定義するという、誰もが最初に直面したときに苦労するパズルのより一般的なバージョンですNat ~ Free Id ()。

ソリューションの構造を強調するために、モジュールを多くの中間定義に分割しました。使いやすさのために自己完結型の要点もアップロードしました。

エキサイティングなことから始めFます。現時点ではこのパッケージがインストールされていないため、再定義します。

{-# LANGUAGE Rank2Types #-}
module MatchFree where

newtype F f a = F { runF :: forall r. (a -> r) -> (f r -> r) -> r }

ここで、パターン マッチングを検討する前に、通常のデータ型のコンストラクターに対応するものを定義することから始めることができます。

pureF :: a -> F f a
pureF a = F $ const . ($ a)

freeF :: Functor f => f (F f a) -> F f a
freeF f = F $ \ pr fr -> fr $ fmap (\ inner -> runF inner pr fr) f

次に、 と の 2 種類を紹介OpenしCloseます。Closeは単純なFタイプですがOpen、 の要素の内容を観察したことに対応します。F f aそれEitherは純粋なaまたはf (F f a)です。

type Open  f a = Either a (f (F f a))
type Close f a = F f a

私の手の込んだ説明からもわかるように、これら 2 つの型は実際には同等であり、これらの間を行き来する関数を実際に書くことができます。

close :: Functor f => Open f a -> Close f a
close = either pureF freeF

open :: Functor f => Close f a -> Open f a
open f = runF f Left (Right . fmap close)

ここで、問題に戻ることができます。行動方針はかなり明確です。取得した内容に応じてopen、またはF f aいずれかを適用します。そして、それは実際に機能します：kpkf

matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r
matchF kp kf = either kp kf . open

自然数に関する元のコメントに戻ると、チャーチ数を使用して実装された前任者は、単純なケース分析が一定時間であると合理的に期待できる場合、自然数のサイズに線形です。自然数の場合と同様に、このケース分析はかなりコストがかかります。これはrunF、 の定義で を使用することで示されるようにopen、構造全体がトラバースされるためです。

于 2015-07-14T20:22:02.550 に答える