16
4

1 に答える 1

15

そのようなエンコーディングはユニークではありません

あなたが質問をしたとき、答えは明らかに「いいえ」です

a = forall r. (a -> r) -> r
a = forall s. ((forall r. (a -> r) -> r) -> s) -> s

どのエンコーディングが最小であるかについては...まあ、基礎となるタイプはほぼ確実です！

共密度はあなたが望むものではないかもしれません

さらに、Codensityは魅力的ですが、基になるタイプと同型ではないと思います。 from . to = id簡単な方向です。

to . from
  = \x -> to (from x)
  = \x -> C $ \f -> (from x) >>= f
  = \x -> C $ \f -> (unC x return) >>= f
  = \(C g) -> C $ \f -> (g return) >>= f

しかし、それからあなたはちょっと立ち往生します。証明しようとしても同じことが起こりますa = forall r. (a -> r) -> rが、「無料の定理」によって救われます（これなしでそれを行う方法があるかもしれませんが、無料の定理はそれを簡単にします）。Codensityに対応する議論はありません。私が読んだほとんどの論文は、それが保存されていることを証明してい>>=ます。つまり、モナディック操作を使用してreturn構築するだけでC m a、何を呼び出すかtoはto . fromアイデンティティです。

十分に努力すれば、同型写像の反例を思いつくことさえできます

evil :: C Maybe Int
evil = C $ \h -> case h 1 of
                      Nothing -> h 2
                      Just x  -> Nothing


 to . from $ evil
  = (\(C g) -> C $ \f -> (g return) >>= f) evil
  = C $ \f -> ((\h -> case h 1 of
                      Nothing -> h 2
                      Just x  -> Nothing) return) >>= f
  = C $ \f -> Nothing >>= f

それで、これらは同じですか？

test 1 = Nothing
test n = Just n

unC evil test
  = Just 2
unC (C $ \f -> Nothing >>= f) test
  = Nothing >>= test
  = Nothing

私はその導出を間違えたかもしれません。まだチェックしていませんが、今はそうは思いません。C m a = m a

別の種類のCPS

すべてのデータは、型なしラムダ関数としてエンコードできます。これは、約70年前にChurchによって発見されたプロパティです。多くの場合、「チャーチエンコーディング」データ構造について話しますが、Olegは、少なくとも型付きの設定では、「Boehm-Beraducci」エンコーディングについて話す必要があると提案しています。あなたがそれを何と呼ぶか​​に関係なく、アイデアは

(a,b) = forall r. (a -> b -> r) -> r
Either a b = forall r. (a -> r) -> (b -> r) -> r

少なくとも速くて緩い推論まで。このエンコーディングは、ADTをシステムFタイプとしてエンコードする方法を提供することは明らかです。これにより、関数型言語を実装する方法も明らかになります。つまり、すべてを内部でクロージャとして扱い、パターンマッチングを関数アプリケーションとして実装するだけです。

実際、システムFには、実存型をユニバーサル型としてエンコードする方法さえあります。

exists a. f a = forall r. (forall a'. f a' -> r) -> r

これは非常に重要なアイデンティティであることが判明しました。特に、これは、上位の型と実存型の型推論の関係を考えるのに役立ちます。型推論はランク2の型まで決定可能であるため、型推論はランク1の普遍性と実存性を備えたシステムでも決定可能です。存在記号はモジュールの基礎であるため、これは重要なことです。

于 2012-09-25T22:03:48.563 に答える