이 함수의 유형 (a -> a) -> a는 왜입니까?

Question

이 함수의 유형 (a -> a) -> a는 왜입니까?

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

무한/재귀 형일까요? 저는 형식이 있어야한다고 생각하는 단어를 넣으려고했지만, 어떤 이유로 든 할 수 없습니다.

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

어떻게 f (y f)가 값으로 해석되는지 알 수 없습니다. 다음은 나에게 조금 더 의미가 있습니다.

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

그러나 여전히 우스꽝스럽게 혼란 스럽습니다. 무슨 일이야?

Answer 1

음, y는 입력 (a -> b) -> c이 될 몇 가지 a, b 및 c 우리가 아직 모르는을 위해 할 수있다; 결국 함수 f을 인수에 적용하므로 함수를 사용하는 함수 여야합니다.

y f = f x (다시, 일부 x) 이후로 y의 반환 유형은 f의 반환 유형이어야합니다. 따라서 y의 유형을 약간 수정할 수 있습니다 : a 및 b에 대해 (a -> b) -> 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이되어야합니다.

Answer 2

@ 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 

어떤 일이 발생하는지보고 싶은 기능으로 동일한 단계를 수행 할 수 있습니다. 이 두 예제 모두 값에 수렴하지만 항상 그런 것은 아닙니다.

Answer 3

연결자에 대해 설명하겠습니다.그것은 "fixpoint의 콤비"라고하며 다음과 같은 속성이 있습니다 :

는

본 숙박 다음 "fixpoint의 콤비는"함수를 f :: (a -> a) 및 발견하여는 "고정 점"그 함수 등이 f x == x의 x :: a 걸립니다. 고정 점 연결자의 일부 구현은 "발견"시 더 좋거나 나쁠 수 있지만 종료한다고 가정하면 입력 기능의 고정 점이 생성됩니다. The Property를 만족하는 함수는 "고정 점 결합 자"라고 부를 수 있습니다.

"고정 지점 연결자"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) 

여기에 있습니다. 고정 지점 연결자의 필수 속성에 따라 이y으로 정의되어 있습니다.
y f == f (y f). y f이 x을 발견했다고 가정하는 대신 x은 분기 계산을 나타내며 여전히 동일한 결론 (iinm)을 취할 수 있습니다.

귀하의 기능이 The Property를 충족하므로이 기능이 고정 점 결합 자라고 결론을 내릴 수 있으며 유형을 포함하여 우리가 명시한 다른 속성이 귀하의 기능에 적용될 수 있습니다.

이것은 확실한 증거는 아니지만 추가적인 통찰력을 제공하기를 바랍니다.

Answer 4

다른 사람들의 답변에 추가하기 만하면됩니다.

정의 할 함수는 보통 fix이며, 다른 함수의 fixed point을 계산하는 함수는 fixed-point combinator입니다. 수학에서, 함수 f의 고정 소수점은 x 인 인수가 f x = x입니다. 이미 fix 유형이 (a -> a) -> a이어야한다고 추측 할 수 있습니다. "함수를 a에서 a으로 가져오고 a을 반환합니다."

당신은 Y combinator 이후가 될 것으로 보인다 함수 y라고했지만, 이는 부정확 한 이름입니다 :는 Y 콤비가 한 특정 고정 소수점 콤비, 그러나 당신이 정의한 것과 동일하지 않습니다 이리.

어떻게 f (y f)가 값으로 해석되는지 알 수 없습니다.

글쎄, 트릭은 하스켈이 엄격하지 않은 (a.k.a. "게으른") 언어라는 것입니다. 모든 경우에있어서 y f 인수를 평가할 필요가없는 경우 f (y f)의 계산은 f으로 종료 할 수 있습니다. 따라서 계급을 정의하는 경우 (John L의 설명처럼) fac (y fac) 1은 y fac을 평가하지 않고 1로 평가됩니다.

엄격한 언어로는이 작업을 수행 할 수 없으므로 이러한 언어에서는 고정 소수점 결합자를 이러한 방식으로 정의 할 수 없습니다. 그 언어들에서, 교과서 고정 소수점 결합자는 Y 결합 자이다.