16

または具体的に言うと、なぜfoldrを使用してリストをエンコードし、反復を使用して数値をエンコードするのですか?

長文の導入で申し訳ありませんが、質問したいことの名前をどのように挙げればよいかよくわからないので、最初にいくつかの説明をする必要があります. これは、この CAMcCann の投稿から大きく引き出されていますが、これは私の好奇心を完全に満足させるものではありません。また、ランク n 型と無限の怠惰な問題についても手短に説明します。

データ型を関数としてエンコードする 1 つの方法は、ケースごとに 1 つの引数を受け取る「パターン マッチング」関数を作成することです。各引数は、そのコンストラクターに対応する値を受け取り、すべての引数が同じ結果の型を返す関数です。

これはすべて、非再帰型の場合に期待どおりに機能します

--encoding data Bool = true | False
type Bool r = r -> r -> r

true :: Bool r
true = \ct cf -> ct

false :: Bool r
false = \ct cf -> cf

--encoding data Either a b = Left a | Right b
type Either a b r = (a -> r) -> (b -> r) -> r

left :: a -> Either a b r
left x = \cl cr -> cl x

right :: b -> Either a b r
right y = \cl cr -> cr y

ただし、パターン マッチングとの優れた類似性は、再帰型ではうまくいきません。私たちは次のようなことをしたくなるかもしれません

--encoding data Nat = Z | S Nat
type RecNat r = r -> (RecNat -> r) -> r
zero = \cz cs -> cz
succ n = \cz cs -> cs n

-- encoding data List a = Nil | Cons a (List a)
type RecListType a r = r -> (a -> RecListType -> r) -> r
nil = \cnil ccons -> cnil
cons x xs = \cnil ccons -> ccons x xs

しかし、これらの再帰的な型定義を Haskell で書くことはできません! 通常の解決策は、コンス/成功ケースのコールバックを、再帰の最初のレベルだけでなく、すべてのレベルに強制的に適用することです (つまり、フォールド/イテレータを記述します)。このバージョンrでは、再帰型が次のような戻り値の型を使用します。

--encoding data Nat = Z | S Nat
type Nat r = r -> (r -> r) -> r
zero = \cz cf -> cz
succ n = \cz cf -> cf (n cz cf)

-- encoding data List a = Nil | Cons a (List a)
type recListType a r = r -> (a -> r -> r) -> r
nil = \z f -> z
cons x xs = \z f -> f x (xs z f)

このバージョンは機能しますが、一部の関数の定義が非常に難しくなります。たとえば、リストの "tail" 関数や数値の "predecessor" 関数を書くことは、パターン マッチングを使用できる場合は簡単ですが、代わりに折り畳みを使用する必要がある場合は注意が必要です。

だから私の本当の質問に：

  1. フォールドを使用したエンコーディングが、仮想の「パターン マッチング エンコーディング」と同じくらい強力であることをどのように確認できますか? パターンマッチングを介して任意の関数定義を取得し、代わりに折り畳みのみを使用して機械的に変換する方法はありますか? (もしそうなら、これはまた、foldr に関して、tail や foldl などのトリッキーな定義をあまり魔法のようにしないようにするのにも役立ちます)

  2. Haskell 型システムが「パターンマッチング」エンコーディングで必要な再帰型を許可しないのはなぜですか? . 経由で定義されたデータ型で再帰型のみを許可する理由はありdataますか? 再帰代数データ型を直接消費する唯一の方法はパターン マッチングですか? 型推論アルゴリズムと関係がありますか?

4

2 に答える 2

6

いくつかの誘導データ型が与えられた

data Nat = Succ Nat | Zero

このデータでパターンマッチングを行う方法を検討できます

case n of
  Succ n' -> f n'
  Zero    -> g

型のすべての関数は適切なものをNat -> a与えることで定義でき、 （むき出しの底） を作成する唯一の方法は2つのコンストラクターの1つを使用することであることは明らかです。fgNat

編集：少し考えてみてくださいf。再帰的ではないものとして再定義できるよりも再帰的に呼び出す適切なものをfoo :: Nat -> a与えることによって関数を定義している場合。タイプが代わりに書くことができる場合。したがって、一般性を失うことなくfgffooff' n' (foo n')f'a = (a',Nat)f' (foo n)

foo n = h $ case n
                 Succ n' -> f (foo n)
                 Zero    -> g

これは私の投稿の残りの部分を意味のあるものにする定式化です：

したがって、caseステートメントは「デストラクタ辞書」を適用するものと考えることができます。

data NatDict a = NatDict {
   onSucc :: a -> a,
   onZero :: a
}

これで、以前のcaseステートメントは次のようになります。

h $ case n of
      Succ n' -> onSucc (NatDict f g) n'
      Zero    -> onZero (NatDict f g)

これを考えると、私たちは導き出すことができます

newtype NatBB = NatBB {cataNat :: forall a. NatDict a -> a}

次に、2つの関数を定義できます

fromBB :: NatBB -> Nat
fromBB n = cataNat n (NatDict Succ Zero)

と

toBB :: Nat -> NatBB
toBB Zero = Nat $ \dict -> onZero dict
toBB (Succ n) = Nat $ \dict -> onSucc dict (cataNat (toBB n) dict)

これらの2つの関数が同型写像の目撃者であることを証明でき（高速で推論を失うまで）、したがって次のことを示すことができます。

newtype NatAsFold = NatByFold (forall a. (a -> a) -> a -> a)

（これはとまったく同じNatBBです）は同型ですNat

他の型でも同じ構造を使用でき、基礎となる型が代数的推論（および誘導）と同型であることを証明するだけで、結果の関数型が必要なものであることを証明できます。

2番目の質問に関しては、Haskellの型システムは、等再帰型ではなく等再帰型に基づいています。これはおそらく、理論と型推論が等再帰型でより簡単に解決できるためであり、プログラマー側にもう少し作業を課すだけのすべての力を備えています。オーバーヘッドなしで等再帰型を取得できると主張したい

newtype RecListType a r = RecListType (r -> (a -> RecListType -> r) -> r)

しかし、どうやらGHCオプティマイザーは時々それらを窒息させます:(。

于 2012-11-27T05:51:30.097 に答える
3

Scott エンコーディングに関するウィキペディアのページには、役立つ洞察がいくつかあります。短いバージョンは、あなたが言及しているのはChurchエンコーディングであり、「仮説的なパターンマッチエンコーディング」はScottエンコーディングです。どちらも賢明な方法ですが、Church エンコーディングでは、より軽い型の機械を使用する必要があります (特に、再帰型は必要ありません)。

2 つが同等であることの証明は、次のアイデアを使用します。

churchfold :: (a -> b -> b) -> b -> [a] -> b
churchfold _ z [] = z
churchfold f z (x:xs) = f x (churchfold f z xs)

scottfold :: (a -> [a] -> b) -> b -> [a] -> b
scottfold _ z [] = z
scottfold f _ (x:xs) = f x xs

scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b
scottFromChurch f z xs = fst (churchfold g (z, []) xs)
 where
  g x ~(_, xs) = (f x xs, x : xs)

アイデアは、churchfold (:) []リスト上のアイデンティティであるため、与えられたリスト引数とそれが生成するはずの結果を生成する Church フォールドを使用できるということです。次に、チェーンx1 `f` (x2 `f` (... `f` xn) ... )の中で最も外側fのペアがペアを受け取り(y, x2 : ... : xn : [])(y気にしないものもあります)、 を返しますf x1 (x2 : ... : xn : [])。もちろん、それx1 : ... : xn : []以上の のアプリケーションfも機能するように、返さなければなりません。

(これは実際には、帰納法の「弱い」または通常の原理からの強い (または完全な) 帰納法の数学的原理の証明に少し似ています)。

ところで、あなたのBool r型は実際の Church ブール値には少し大きすぎます。たとえば(+) :: Bool Integerですが、(+)実際には Church ブール値ではありません。有効RankNTypesにすると、より正確なタイプを使用できます: type Bool = forall r. r -> r -> r. 現在はポリモーフィックであることを余儀なくされているため、実際には 2 つの (ignoringseqと bottom) 住民のみが含まれています –\t _ -> tと\_ f -> f. 同様の考え方は、他の教会タイプにも当てはまります。

于 2012-12-06T16:33:22.460 に答える