3

普遍的なポリモーフィズムの機能を考慮して、再帰代数データ型の定義、逆変換、およびエンコードを理解しようとしています。例として、次の方法で再帰的な二分木の実装を試みました。

data BTAlg x = Empty | Leaf x x
type BT = forall z. ((BTAlg z) -> z) -> z

二分木のタイプはT、定数e: Tと二分演算を備えたすべてのタイプm: T -> T -> T、つまり functor の「初期モジュール」を備えたすべてのタイプの中で初期化する必要があるという直感BTAlgです。つまり、 の要素BTは、そのようなモジュールTに対して の要素を割り当てる方法ですT。

それ自体のモジュール構造は、次のBT方法で定義できます。

initial_module :: (BTAlg BT) -> BT
initial_module = \s -> case s of
  Empty -> (\f -> (f Empty))
  Leaf x y -> (\f -> (f (Leaf (x f) (y f))))

のパターン マッチングに向けたステップとして、型自体にBT要素を適用したいと思います。これは、 の何らかのエンコード/デコードと考えられます。x:BTBTx

decode_encode :: BT -> BT
decode_encode x = x initial_module

ただし、このコードでは、処理できない型エラーが発生します。

Couldn't match expected type `(BTAlg z -> z) -> z'
            with actual type `BT'
Expected type: BTAlg ((BTAlg z -> z) -> z) -> (BTAlg z -> z) -> z
  Actual type: BTAlg BT -> (BTAlg z0 -> z0) -> z0
In the first argument of `x', namely `initial_module'
In the expression: x initial_module

ここで何が問題なのですか？に適用できるようにするには、ユニバーサル型パラメーターzをに特化する必要があることを型チェッカーが認識しない理由がわかりません。書くことも役に立ちません。BTxxinitial_module(x :: ((BTAlg BT) -> BT) -> BT) initial_module

定義の動機に関する補遺decode_encode:BT標準実現と実際に「同型」であることを自分自身に納得させたい

data BTStd = StdEmpty | StdLeaf BTStd BTStd

二分木の; Haskell内でこれを正確にする方法はわかりませんが、最初はマップBT -> BTStdを作成BTStd -> BTし、2つの実現の間を行き来することです。

の定義は、 の標準モジュール構造にtoStandard: BT -> BTStdの普遍的なプロパティを適用したものです。BTBTAlgBTStd

std_module :: (BTAlg BTStd) -> BTStd
std_module s = case s of 
  Empty -> StdEmpty
  Leaf x y -> StdLeaf x y

toStandard: BT -> BTStd
toStandard x = x std_module

デコード機能についてfromStandard: BTStd -> BTは、次のことを行いたいと思います。

fromStandard :: BTStd -> BT
fromStandard s = case s of 
  StdEmpty -> initial_module Empty
  StdLeaf x y -> initial_module (Leaf (fromStandard x) (fromStandard y))

decode_encodeただし、これにより、上記の直接定義と同じタイプの問題が発生します。

Couldn't match expected type `BT'
            with actual type `(BTAlg z0 -> z0) -> z0'
In the return type of a call of `fromStandard'
Probable cause: `fromStandard' is applied to too few arguments
In the first argument of `Leaf', namely `(fromStandard x)'
In the first argument of `initial_module', namely
  `(Leaf (fromStandard x) (fromStandard y))'

ありがとうございました！

4

1 に答える 1

4

推論された型を見るとdecode_encode

:t decode_encode
> decode_encode :: ((BTAlg BT -> (BTAlg z -> z) -> z) -> t) -> t

GHC がかなりのポリモーフィズムを失ったことは明らかです。ここでの詳細は完全にはわかりません。このコードはImpredicativeTypesコンパイルが必要であり、通常、私の理解が崩壊し始めます。ただし、ポリモーフィズムを維持するための標準的な方法があります。newtype

newtype BT = BT { runBT :: forall z. (BTAlg z -> z) -> z }

は、およびによってnewtype証明される同形性を確立します。それらの目撃者を適切な場所に配置する限り、前進できます。BT ~ forall z . (BTAlg z -> z) -> zBTrunBT

data    BTAlg x = Empty    | Leaf    x     x
data    BTStd   = StdEmpty | StdLeaf BTStd BTStd
newtype BT      = BT { runBT :: forall z. ((BTAlg z) -> z) -> z }

initial_module :: BTAlg BT -> BT
initial_module s = case s of
  Empty -> BT $ \f -> (f Empty)
  Leaf x y -> BT $ \f -> (f (Leaf (runBT x f) (runBT y f)))

std_module :: (BTAlg BTStd) -> BTStd
std_module s = case s of 
  Empty -> StdEmpty
  Leaf x y -> StdLeaf x y

toStandard :: BT -> BTStd
toStandard x = runBT x std_module

fromStandard :: BTStd -> BT
fromStandard s = case s of
  StdEmpty -> initial_module Empty
  StdLeaf x y -> initial_module (Leaf (fromStandard x) (fromStandard y))

特に素晴らしいのは、型ラムダが適用されるrunBTタイミングと回数を制御するために使用することですBT

decode_encode :: BT -> BT
decode_encode x = runBT x initial_module

の 1 回の使用はrunBT、量化されたタイプの 1 つの統合に対応します。

于 2014-06-23T12:21:45.260 に答える