Y Combinator в Хаскелле

Можно ли записать Y Combinator в Haskell?

Похоже, у него будет бесконечно рекурсивный тип.

 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 combinator выглядит следующим образом

(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)))))

Это просто сокращение эта для ленивой версии.

Если вы предпочитаете короткие имена переменных.

Ответ 1

эта страница wiki и Этот ответ, кажется, отвечает на мой вопрос.
Я напишу больше объяснений позже.

Теперь я нашел что-то интересное в этом типе Му. Рассмотрим S = Mu Bool.

data S = S (S -> Bool)

Если рассматривать S как множество и равный знаку как изоморфизм, то уравнение становится

S ⇋ S -> Bool ⇋ Powerset(S)

Итак, S - множество множеств, изоморфных их силовым сетям! Но из канторского диагонального аргумента мы знаем, что мощность Powerset (S) всегда строго больше мощности S, поэтому они никогда не изоморфны. Я думаю, именно поэтому вы можете теперь определить оператор с фиксированной точкой, даже если вы не можете без него.

Ответ 2

Здесь нерекурсивное определение y-combinator в haskell:

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

отзыв о шляпе

Ответ 3

Y combinator не может быть введен с использованием типов Hindley-Milner, полиморфного лямбда-исчисления, на котором основана система типа Haskell. Вы можете доказать это, обратившись к правилам системы типов.

Я не знаю, можно ли ввести Y combinator, указав его тип более высокого ранга. Меня это удивит, но у меня нет доказательств того, что это невозможно. (Ключ должен был идентифицировать подходящий полиморфный тип для lambda-bound x.)

Если вам нужен оператор фиксированной точки в Haskell, вы можете определить его очень легко, потому что в Haskell let-binding имеет семантику с фиксированной точкой:

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

Вы можете использовать это обычным способом для определения функций и даже для некоторых конечных или бесконечных структур данных.

Также возможно использовать функции для рекурсивных типов для реализации неподвижных точек.

Если вы заинтересованы в программировании с фиксированными точками, вы хотите прочитать технический отчет Брюса МакАдама Что о том, как обмануть его.

Ответ 4

Каноническое определение Y комбинатора следующее:

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

Но он не проверяет тип в Haskell из-за xx, так как для него требуется бесконечный тип:

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 " ++)

Это небезопасно (очевидно). Ответ rampion демонстрирует более безопасный способ написать комбинатор точек фиксирования в Haskell без использования рекурсии.