Блог

fix f = let {x = f x} in x

Говоря о let , я подумал, что let P = Q in R это будет оценивать Q -> Q’, тогда P заменяется на Q’ в R, или: R[P -> Q'] .

Но в fix определении Q зависит от R, как тогда оценить?

Я предполагаю, что речь идет о ленивой оценке. Q’ становится грохотом, но я не могу рассуждать об этом в своей голове.

Исходя из контекста, я смотрю на Y combinator, он должен найти фиксированную точку функции, поэтому, если у меня есть эта функция, one x = 1 , то fix one == 1 она должна выполняться, верно?

Так fix one = let {x = one x} in x что, но я не вижу, как 1 из этого можно было бы выйти.

Говоря о let, я подумал, что let P = Q in R будет вычисляться Q -> Q' , а затем P заменяется на Q' in R , или: R[P -> Q'] .

Морально, да, но P оценивается не сразу, оно оценивается при необходимости.

Но в каком определении Q это зависит от R того, как тогда оценивать?

Q не зависит от R , это зависит от P . Это P рекурсивно зависит от самого себя. Это может привести к нескольким различным результатам. Грубо говоря:

• Если Q не может вернуть какую-либо часть своего результата перед вычислением P , то P представляет собой бесконечно повторяющееся вычисление, которое не завершается. Например,

   let x = x   1 in x     -- loops forever with no result
  -- (GHC is able to catch this specific case and raise an exception instead,
  -- but it's an irrelevant detail)
   

• Если Q вместо этого может вернуть часть своего результата перед необходимостью оценки P , он это делает.

   let x = 2 : x in x
  -- x = 2 : .... can be generated immediately
  -- This results in the infinite list 2:2:2:2:2:.....
  
  let x = (32, 10   fst x) in x
  -- x = (32, ...) can be generated immediately
  -- hence x = (32, 10   fst (32, ...)) = (32, 10 32) = (32, 42)
   

Я полагаю, что речь идет о ленивой оценке. Q' становится проблемой, но я не могу рассуждать об этом в своей голове.

P связано с ударом. Важно то, вызывает ли этот блок сам себя, прежде чем возвращать какую-то часть вывода или нет.

Исходя из контекста, я смотрю на Y combinator, он должен найти фиксированную точку функции, поэтому, если у меня есть эта функция. one x = 1 , тогда fix one == 1 должно выполняться, верно?

ДА.

Итак fix one = let x = one x in x , но я не понимаю, почему 1 из этого следует

Мы можем вычислить это следующим образом:

 fix one
 = {- definition of fix -}
let x = one x in x
 = {- definition of x -}
let x = one x in one x
 = {- definition of one -}
let x = one x in 1
 = {- x is now irrelevant -}
1
 

Просто расширьте определения. Сохраняйте рекурсивные определения на случай, если они вам понадобятся снова.