7

ファンクターの不動点の抽象的な概念を理解したいと思いますが、Haskell での正確な実装とカタモルフィズムを理解するのにまだ苦労しています。

たとえば、「Category Theory for Programers」の書籍 -- 359 ページに従って、次の代数を定義するとします。

-- (Int, LiftF e Int -> Int)

data ListF e a = NilF | ConsF e a

lenAlg :: ListF e Int -> Int
lenAlg (ConsF e n) -> n + 1
lenAlg NilF = 0

カタモルフィズムの定義により、次の関数を ListF の固定小数点 (リスト) に適用して、その長さを計算できます。

cata lenAlg :: [e] -> Int
cata lenAlg = lenAlg . fmap (cata lenAlg) . unFix

2 つの混乱があります。まず、Haskell コンパイラは List がListFの不動点であることをどのように認識していますか? 私は概念的にそれを知っていますが、コンパイラはどのように知っていますか、つまり、List とすべて同じである別の List' を定義した場合、コンパイラは List' が ListF の不動点でもあると自動的に推論しないと思いますそれ？（私は驚くだろう）。

第 2 に、cata lenAlg の再帰的な性質により、常にデータ コンストラクターの外側のレイヤーを unFix して、ファンクターの内側のレイヤーを公開しようとします (ちなみに、この私の解釈は正しいですか?)。しかし、すでにリーフにいる場合、どうすればこの関数呼び出しを呼び出すことができるでしょうか?

fmap (cata lenAlg) Nil

例として、誰かが以下の関数呼び出しの実行トレースを書いて明確にするのを手伝ってもらえますか?

cata lenAlg Cons 1 (Cons 2 Nil)

明らかな何かが欠けている可能性がありますが、この質問が同様の混乱を共有する他の人々にとってまだ意味があることを願っています.

回答のまとめ

@nm は、Haskell コンパイラが Functor A が Functor B の不動点であることを理解するには、明示的である必要があることを指摘して、私の最初の質問に答えました。この場合、

type List e = Fix (ListF e)

@luqui と @Will Ness は、葉 (この場合は NilF) で fmap (cata lenAlg) を呼び出すと、fmap の定義により NilF が返されることを指摘しました。

-- f :: a -> b
fmap f (ConsF e a) = ConsF e (f b)
fmap f NilF        = NilF

私の最初の（より大きな）質問に直接対処したので、@ nmの回答を受け入れますが、3つの回答すべてが気に入っています。ご協力ありがとうございました。

4

3 に答える 3

4

いいえ、unFix構造を公開してから、それにfmap f関数fを適用します。葉の場合、葉に対してfmap f行うように定義されていることを行います。つまり、何もしません。Haskellfmapのケースベースの定義では通常のように、「知っている」、つまり、各ケースを処理するように定義されているということです。

Fix (ListF e) = ListF e (Fix (ListF e)) 
              = NilF | ConsF e (Fix (ListF e))

名前を変更Fix (ListF e)しListof eて取得します

Listof     e  = NilF | ConsF e (Listof e)

Listof e再帰型です。ListF e r非再帰型です。 Fixそれから再帰型を作ります。ListF eFunctor であることは、この「果物」の「硬い外殻」である「肉」にfmap作用することを意味します。rListF e

data ListF e a = NilF | ConsF e a

newtype Fix f = X { unFix    :: (f       (Fix f)) }

-- unFix ::    Fix f          -> f       (Fix f        )
-- unFix (_ :: Fix (ListF e)) :: ListF e (Fix (ListF e))

lenAlg :: ListF e Int -> Int
lenAlg (ConsF e n) = n + 1
lenAlg NilF        = 0

instance Functor (ListF e) where
    -- fmap :: (a -> b) -> (ListF e a) -> (ListF e b)
    fmap f NilF        = NilF
    fmap f (ConsF e r) = ConsF e (f r)

cata :: (ListF e Int -> Int) -> Fix (ListF e) -> Int
cata lenAlg x = (lenAlg . fmap (cata lenAlg) . unFix) x
              =  lenAlg ( fmap (cata lenAlg) ( unFix  x ))
--------
        x       ::       Fix (ListF e)
        unFix x ::            ListF e (Fix (ListF e))
        fmap (cata lenAlg) :: ListF e (Fix (ListF e)) -> ListF e (Int)
              cata lenAlg  ::          Fix (ListF e)  ->          Int

        fmap (cata lenAlg)   (unFix  x              ) :: ListF e  Int 
 lenAlg (_                                            :: ListF e  Int ) :: Int

見る？すべてのワイヤーは適切な場所に行きます。fmap内部部分rを再帰的に変換し、lenAlg 代数は最後の変換を適用します。これは、すべての内部部分がすでに再帰的な結果に折りたたまれている構造を折りたたむ最後のステップです。したがって、最終結果が生成されます。

具体的な例として、2 つの数値1と2のリストの場合、次のようになります。

-- newtype Fix f  = X { unFix :: (f      (Fix f         )) }
--             _\_______       ____\____      _\________
onetwo :: Fix (ListF Int) -- ~ ListF Int (Fix (ListF Int))
onetwo = X (ConsF 1
                  (X (ConsF 2
                            (X NilF))))

cata lenAlg :: Fix (ListF e) -> Int
cata lenAlg    onetwo
  = {- definition of cata   -}
    lenAlg . fmap (cata lenAlg) . unFix  $ onetwo
  = {- definition of onetwo -}
    lenAlg . fmap (cata lenAlg) . unFix  $ 
                           X (ConsF 1 (X (ConsF 2 (X NilF))))
  = {- definition of unFix  -}
    lenAlg . fmap (cata lenAlg) $ 
                              ConsF 1 (X (ConsF 2 (X NilF)))
  = {- definition of fmap   -}
    lenAlg $ ConsF 1 (cata lenAlg     (X (ConsF 2 (X NilF))))
  = {- definition of lenAlg -}
    (+ 1)  $          cata lenAlg     (X (ConsF 2 (X NilF)))
  = {- definition of cata   -}
    (+ 1)  $ lenAlg . fmap (cata lenAlg) . unFix $ 
                                       X (ConsF 2 (X NilF))
  = {- definition of unFix  -}
    (+ 1) $ lenAlg . fmap (cata lenAlg) $ ConsF 2 (X NilF)
  = {- definition of fmap   -}
    (+ 1) $ lenAlg $ ConsF 2 $ cata lenAlg        (X NilF)
  = {- definition of lenAlg -}
    (+ 1) $ (+ 1)  $           cata lenAlg        (X NilF)
  = {- definition of cata   -}
    (+ 1) $ (+ 1)  $ lenAlg . fmap (cata lenAlg) . unFix $ 
                                                  (X NilF)
  = {- definition of unFix  -}
    (+ 1) $ (+ 1)  $ lenAlg . fmap (cata lenAlg) $   NilF
  = {- definition of fmap   -}
    (+ 1) $ (+ 1)  $ lenAlg $                        NilF
  = {- definition of lenAlg -}
    (+ 1) $ (+ 1)  $ 0
  = (+ 1) $ 1
  = 2

また、

squaringAlg :: ListF Int [Int] -> [Int]
squaringAlg (ConsF e r) = e*e : r
squaringAlg NilF        = []

filteringAlg :: (e -> Bool) -> ListF e [e] -> [e]
filteringAlg p (ConsF e r) | p e       = e : r
                           | otherwise = r
filteringAlg _ NilF                    = []

等

于 2018-11-27T08:29:43.513 に答える