Y Combinator в Хаскеле

Question

Можно ли написать Y Combinator на Хаскеле?

Кажется, что это будет бесконечно рекурсивный тип.

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

Который - только сокращение eta для ленивой версии.

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

Answer 1

Ой

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

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

data S = S (S -> Bool)

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

S ⇋ S -> Bool ⇋ Powerset(S)

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

Answer 2

Вот нерекурсивное определение y-комбинатора в haskell:

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

шапка

Answer 3

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

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

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

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

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

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

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

Answer 4

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

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

Но это не проверка типа в Haskell из-за x x, поскольку это потребовало бы бесконечного типа:

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 без использования рекурсии.

Answer 5

Просто чтобы сделать код rampion более читабельным:

-- Mu :: (Mu a -> a) -> Mu a
newtype Mu a = Mu (Mu a -> a) 

w :: (Mu a -> a) -> a
w h = h (Mu h)

y :: (a -> a) -> a
y f = w (\(Mu x) -> f (w x))
-- y f = f . y f

в котором w обозначает комбинатор омега w = \x -> x x, а также y обозначает комбинатор y y = \f -> w . (f w).