50

HaskellでYCombinatorを書くことは可能ですか？

無限再帰型のようです。

 Y :: f -> b -> c
 where f :: (f -> b -> c)

か何か。単純なわずかに因数分解された階乗でさえ

factMaker _ 0 = 1
factMaker fn n = n * ((fn fn) (n -1)

{- to be called as
(factMaker factMaker) 5
-}

「発生チェック：無限型を構築できません：t = t->t2->t1」で失敗します

（Yコンビネータは次のようになります

(define Y
    (lambda (X)
      ((lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg))))
       (lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg)))))))

スキームで）または、より簡潔に

(λ (f) ((λ (x) (f (λ (a) ((x x) a))))
        (λ (x) (f (λ (a) ((x x) a))))))

応募注文についてそして

(λ (f) ((λ (x) (f (x x)))
        (λ (x) (f (x x)))))

これは、怠惰なバージョンのイータ収縮です。

短い変数名を好む場合。

4

5 に答える 5

57

haskell での y コンビネータの非再帰的な定義は次のとおりです。

newtype Mu a = Mu (Mu a -> a)
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)

ハットチップ

于 2011-05-04T14:44:49.357 に答える
47

Y コンビネータは Hindley-Milner 型 (Haskell の型システムのベースとなっている多形ラムダ計算) を使用して型付けすることはできません。これは、型システムのルールに訴えることで証明できます。

Y コンビネータに上位の型を与えることで型付けできるかどうかはわかりません。それは私を驚かせるだろうが、私はそれが不可能であるという証拠を持っていない. (重要なのは、ラムダ バインドの適切なポリモーフィック型を識別することxです。)

Haskell で固定小数点演算子が必要な場合は、Haskell では let バインディングに固定小数点セマンティクスがあるため、非常に簡単に定義できます。

fix :: (a -> a) -> a
fix f = f (fix f)

これを通常の方法で使用して、関数を定義したり、有限または無限のデータ構造を定義したりすることができます。

再帰型の関数を使用して固定小数点を実装することもできます。

不動点を使用したプログラミングに興味がある場合は、Bruce McAdam のテクニカル レポートThat About Wraps it Upをお読みください。

于 2011-05-04T19:29:10.643 に答える
30

Yコンビネータの標準的な定義は次のとおりです。

y = \f -> (\x -> f (x x)) (\x -> f (x x))

x xしかし、それは無限の型を必要とするので、Haskellでは型チェックをしません：

x :: a -> b -- x is a function
x :: a      -- x is applied to x
--------------------------------
a = a -> b  -- infinite type

型システムがそのような再帰型を許可する場合、型チェックは決定不能になります（無限ループが発生しやすくなります）。

ただし、Yコンビネータは、たとえば次を使用してタイプチェックを強制すると機能しますunsafeCoerce :: a -> b。

import Unsafe.Coerce

y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))

main = putStrLn $ y ("circular reasoning works because " ++)

これは（明らかに）安全ではありません。 ランピオンの答えは、再帰を使用せずにHaskellで不動点コンビネータを書くためのより安全な方法を示しています。

于 2011-05-04T15:53:37.633 に答える
24

おー

このwikiページと このStackOverflowの回答は、私の質問に答えているようです。
説明は後で詳しく説明します。

今、私はそのムータイプについて何か面白いものを見つけました。S =MuBoolを考えてみましょう。

data S = S (S -> Bool)

Sを集合として扱い、それが等号を同型写像として扱う場合、方程式は次のようになります。

S ⇋ S -> Bool ⇋ Powerset(S)

つまり、Sは、べき集合と同型の集合の集合です。しかし、カントールの対角論から、Powerset（S）のカーディナリティは常にSのカーディナリティよりも厳密に大きいため、同型になることはありません。これが、固定小数点演算子がないとできない場合でも、固定小数点演算子を定義できるようになった理由だと思います。

于 2010-11-25T03:17:43.833 に答える