20

なぜこの関数の型は (a -> a) -> a なのですか?

Prelude> let y f = f (y f)
Prelude> :t y
y :: (t -> t) -> t

無限/再帰型であるべきではありませんか? 私はそれがタイプであるべきだと思うものを言葉にしようとしましたが、何らかの理由でそれを行うことができません.

y :: (t -> t) -> ?WTFIsGoingOnOnTheRHS?

f (yf) がどのように値に解決されるのかわかりません。以下は私にとってもう少し理にかなっています：

Prelude> let y f x = f (y f) x
Prelude> :t y
y :: ((a -> b) -> a -> b) -> a -> b

しかし、それはまだばかげて混乱しています。どうしたの？

4

4 に答える 4

29

一部の については、 型でなけれyばなりませんが、まだわかりません。結局のところ、これは関数 を取り、それを引数に適用するため、関数を取る関数でなければなりません。(a -> b) -> cabcf

y f = f x(再び、一部の についてx) から、 の戻り値の型はそれ自体の戻り値の型でなければならないことがわかっていyますf。したがって、yビットのタイプを絞り込むことができます。それは(a -> b) -> bいくつかのものである必要がありa、bまだわかりません。

何が何でaあるかを理解するには、渡された値の型を確認するだけfです。ですy f。これは、現在型を把握しようとしている式です。の型yは(a -> b) -> b(一部aのb、 など) であると言っているので、このアプリケーションの型はそれ自体でy fなければならないと言えます。b

したがって、 への引数の型fは ですb。すべてを元に戻すと、(b -> b) -> bこれはもちろん と同じです(a -> a) -> a。

これは、より直感的ですが、より正確ではありません: と言っていますがy f = f (y f)、これは 、 などに拡張できy f = f (f (y f))ますy f = f (f (f (y f)))。したがって、常に全体に別のものを適用できることを知っていますf。問題の「全体」はf引数に適用した結果であるためf、タイプがa -> a;である必要があります。fそして、すべてが引数に適用された結果であると結論付けたので、 の戻り値の型はそれ自体yの型でなければなりません。f(a -> a) -> a

于 2012-01-18T23:24:59.353 に答える
9

他の人の回答に追加するポイントは2つだけです。

定義している関数は通常 と呼ばれfix、固定小数点コンビネータ(別の関数の固定小数点を計算する関数) です。数学では、関数の不動点fは のような引数xですf x = x。fixこれにより、 の型が(a -> a) -> a;でなければならないと推測できます。a「 からまでの関数を受け取りa、 を返す関数a」

関数 を呼び出しましたが、これはY コンビネーターyの後にあるようですが、これは不正確な名前です: Y コンビネーターは特定の固定小数点コンビネーターの 1つですが、ここで定義したものとは異なります。

f (yf) がどのように値に解決されるのかわかりません。

トリックは、Haskell が厳密ではない (別名「怠惰な」) 言語であることです。の計算は、すべての場合にその引数を評価する必要がない場合にf (y f)終了できます。したがって、factorial を定義している場合 (John L が示すように)、 は評価せずに 1 に評価されます。fy ffac (y fac) 1y fac

厳密な言語ではこれができないため、これらの言語では固定小数点コンビネータをこの方法で定義することはできません。これらの言語では、教科書の固定小数点コンビネータは Y コンビネータそのものです。

于 2012-01-19T01:42:08.640 に答える
8

@ehird は型をうまく説明してくれたので、いくつかの例を使って値に解決する方法を示したいと思います。

f1 :: Int -> Int
f1 _ = 5

-- expansion of y applied to f1
y f1
f1 (y f1)  -- definition of y
5          -- definition of f1 (the argument is ignored)

-- here's an example that uses the argument, a factorial function
fac :: (Int -> Int) -> (Int -> Int)
fac next 1 = 1
fac next n = n * next (n-1)

y fac :: Int -> Int
fac (y fac)   -- def. of y
  -- at this point, further evaluation requires the next argument
  -- so let's try 3
fac (y fac) 3  :: Int
3 * (y fac) 2             -- def. of fac
3 * (fac (y fac) 2)       -- def. of y
3 * (2 * (y fac) 1)       -- def. of fac
3 * (2 * (fac (y fac) 1)  -- def. of y
3 * (2 * 1)               -- def. of fac

好きな関数で同じ手順を実行して、何が起こるかを確認できます。これらの例はどちらも値に収束しますが、常にそうなるとは限りません。

于 2012-01-19T00:24:57.273 に答える
6

コンビネータについて教えてください。これは「フィックスポイント コンビネータ」と呼ばれ、次のプロパティがあります。

プロパティ: 「固定点コンビネータ」は関数を取り、その関数の「固定点」f :: (a -> a)を発見します。修正点コンビネータの実装によっては、「発見」の点で良い場合も悪い場合もありますが、終了すると仮定すると、入力関数の固定点が生成されます。The Property を満たす関数は、「固定点コンビネーター」と呼ぶことができます。x :: af x == x

これを「固定点コンビネータ」と呼びyます。今言ったことに基づくと、次のことが当てはまります。

-- as we said, y's input is f :: a -> a, and its output is x :: a, therefore
y :: (a -> a) -> a

-- let x be the fixed point discovered by applying f to y
y f == x -- because y discovers x, a fixed point of f, per The Property
f x == x -- the behavior of a fixed point, per The Property

-- now, per substitution of "x" with "f x" in "y f == x"
y f == f x
-- again, per substitution of "x" with "y f" in the previous line
y f == f (y f)

では、どうぞ。固定点コンビネータの必須プロパティの観点から定義 しました: . が を発見すると仮定する代わりに、が発散計算を表していると仮定しても、同じ結論 (iinm) に達することができます。y
y f == f (y f)y fxx

あなたの関数は The Property を満たすので、それは固定点コンビネータであり、型を含め、私たちが述べた他のプロパティはあなたの関数に適用可能であると結論付けることができます。

これは正確な証拠ではありませんが、追加の洞察が得られることを願っています。

于 2012-01-19T01:34:45.613 に答える