6

教会の数字の次のデータコンストラクターを見ました

data Nat = Zero | Succ Nat deriving Show

しかし、これは単数です。このように Haskell で 2 進数のデータ コンストラクターを実装するにはどうすればよいでしょうか?

私はこれを試しました：

data Bin = Zero | One | BinC [Bin] deriving Show

この後、次のようにエンコードされた 10 進数 5 を取得できます。BinC [One,Zero,One]

しかし、私はここで何かが欠けていると思います。私の解決策は、教会の解決策ほど賢くないようです。当然のことながら、私は教会ではありません。少し考えてみると、私の解決策はリストに依存しているのに対し、Nat はリストのような外部構造に依存していないことがわかりました。

2 進数にも Succ 型コンストラクタを使用して、Church と同様のソリューションを作成できますか? はいの場合、どのように？私はたくさん試しましたが、私の脳はリストやその他のそのような構造の必要性を取り除くことができないようです.

4

3 に答える 3

5

あなたが受け取った他の回答への単なる補遺：

作成しているデータ値は、実際にはチャーチ数字ではなくペアノ数字です。それらは密接に関連していますが、実際には互いに二重/逆です。ペアノ数字は、セットの概念から数を構築するという概念に基づいて構築されています。Haskell では、データ型の密接に関連した概念を使用して表現します。

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (succ)

data Peano = Zero
           | Succ Peano
  deriving (Show)

一方、教会数字は、数字を関数としてエンコードします。

type Church = forall n. (n -> n) -> n -> n

zero :: Church
zero = \p -> id

succ :: Church -> Church
succ = \n p -> p . n p

これで、それらをまとめることができます：

peano :: Church -> Peano
peano c = c Succ Zero

fold :: forall n. (n -> n) -> n -> Peano -> n
fold s z Zero     = z
fold s z (Succ p) = s (fold s z p)

church :: Peano -> Church
church p = \s z -> fold s z p

したがって、チャーチの数字は、本質的に、ペアノの数字を折りたたんだものです。And(peano . church)は Peano 数字の ID ですが、Haskell では上記のように指定された型を直接構成することはできません。型宣言を省略すると、Haskell は、それらを構成できる十分な一般的な型を推測します。

この Ralf Hinze の Theoretical Pearl Church numbers, two には、関数型プログラミングのコンテキストにおける違いとそれらの相互関係の概要が記載されています。.

この二重性をさらに一般化できます。ペアノ数は本質的に自然数の初期 F 代数であり、チャーチ数は本質的に自然数の最終/終端 F 代数です。これの良い入門書は、Bart Jacobs と Jan Rutten のA Tutorial on (Co)Algebras and (Co)Inductionです。

于 2013-08-21T19:07:52.370 に答える
2 
data Bit = Zero | One
data Bin = E Bit | S Bit Bin

five = S One (S Zero (E One))
于 2013-08-21T09:12:41.193 に答える