5

Churchエンコーディングのリストにパッケージcataから使えるようにしたいです。recursion-schemes

type ListC a = forall b. (a -> b -> b) -> b -> b

便宜上二等式を使いましたが、気にしません。newtype必要に応じてを追加したり、GADT を使用したりしてください。

Church エンコーディングの考え方は広く知られており、単純です。

three :: a -> a -> a -> List1 a 
three a b c = \cons nil -> cons a $ cons b $ cons c nil

基本的に「未指定の抽象」consでありnil、「通常の」コンストラクターの代わりに使用されます。私はすべてがこの方法でエンコードできると信じています（Maybe、ツリーなど）。

List1が実際に通常のリストと同型であることを示すのは簡単です:

toList :: List1 a -> [a]
toList f = f (:) []

fromList :: [a] -> List1 a
fromList l = \cons nil -> foldr cons nil l

したがって、その基本ファンクターはリストのファンクターと同じであり、それを実装projectしてからの機構を使用できるはずrecursion-schemesです。

でもできなかったので、「どうしたらいいの？」というのが私の質問です。通常のリストの場合は、パターン マッチのみを実行できます。

decons :: [a] -> ListF a [a]
decons [] = Nil
decons (x:xs) = Cons x xs

関数のパターン マッチができないため、フォールドを使用してリストを分解する必要があります。project通常のリストの折り畳みベースを書くことができます：

decons2 :: [a] -> ListF a [a]
decons2 = foldr f Nil
  where f h Nil = Cons h []
        f h (Cons hh t) = Cons h $ hh : t

ただし、教会でエンコードされたリストには適用できませんでした。

-- decons3 :: ListC a -> ListF a (ListC a)
decons3 ff = ff f Nil
  where f h Nil = Cons h $ \cons nil -> nil
        f h (Cons hh t) = Cons h $ \cons nil -> cons hh (t cons nil)

cata次の署名があります。

cata :: Recursive t => (Base t a -> a) -> t -> a

リストで使用するには、次のものが必要です。

  1. を使用してリストの基本ファンクタ型を宣言するにはtype family instance Base (ListC a) = ListF a
  2. 実装するinstance Recursive (List a) where project = ...

私は両方のステップで失敗します。

4

1 に答える 1

4

ラッパーは、newtype私が見逃した重要なステップであることが判明しました。からのサンプル カタモルフィズムを含むコードを次に示しますrecursion-schemes。

{-# LANGUAGE LambdaCase, Rank2Types, TypeFamilies #-}

import Data.Functor.Foldable

newtype ListC a = ListC { foldListC :: forall b. (a -> b -> b) -> b -> b }

type instance Base (ListC a) = ListF a

cons :: a -> ListC a -> ListC a
cons x (ListC xs) = ListC $ \cons' nil' -> x `cons'` xs cons' nil'
nil :: ListC a
nil = ListC $ \cons' nil' -> nil'

toList :: ListC a -> [a]
toList f = foldListC f (:) []
fromList :: [a] -> ListC a
fromList l = foldr cons nil l

instance Recursive (ListC a) where
  project xs = foldListC xs f Nil
    where f x Nil = Cons x nil
          f x (Cons tx xs) = Cons x $ tx `cons` xs

len = cata $ \case Nil -> 0
                   Cons _ l -> l + 1
于 2015-07-16T23:03:41.823 に答える