Y Combinator в Хаскеле - PullRequest
Новая
       25

Y Combinator в Хаскеле

46 голосов
/ 25 ноября 2010

Можно ли написать 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)))))

Что является лишь сокращением эта для ленивыхверсия.

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

Ответы [ 4 ]

55 голосов
/ 04 мая 2011

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

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

наконечник шляпы

44 голосов
/ 04 мая 2011

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

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

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

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

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

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

Если вы заинтересованы в программировании с фиксированными точками, вы можете прочитать технический отчет Брюса МакАдама That About Wraps it Up .

26 голосов
/ 04 мая 2011

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

23 голосов
/ 25 ноября 2010

О

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

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

data S = S (S -> Bool)

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

S ⇋ S -> Bool ⇋ Powerset(S)

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

...