Y Combinator في Haskell

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"

(يشبه Combinator 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

أوه

صفحة الويكي هذه وهذا الجواب في التدفق يبدو أن الإجابة على سؤالي.
سأكتب المزيد من التفسير لاحقًا.

الآن ، لقد وجدت شيئًا مثيرًا للاهتمام حول هذا النوع MU. النظر في s = mu bool.

data S = S (S -> Bool)

إذا كان المرء يعامل S كمجموعة وهذا يساوي علامة على شكل التماثل ، فإن المعادلة تصبح

S ⇋ S -> Bool ⇋ Powerset(S)

لذلك S هي مجموعة من المجموعات التي هي متماثلة على قوتها! لكننا نعلم من حجة كانتور القطري أن تعداد Cardinality of PowerSet (s) أكبر دائمًا أكبر من تعرض C ، لذلك فهي غير متماثلة أبدًا. أعتقد أن هذا هو السبب في أنه يمكنك الآن تحديد مشغل نقطة ثابتة ، على الرغم من أنك لا تستطيع بدون واحدة.

Answer 2

فيما يلي تعريف غير متكرر لـ Y-Combinator في Haskell:

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

طرف القبعة

Answer 3

لا يمكن كتابته Combinator باستخدام أنواع Hindley-Milner ، وهو حساب حساب Lambda متعدد الأشكال الذي يستند إليه نظام نوع Haskell. يمكنك إثبات ذلك من خلال الاستئناف لقواعد نظام النوع.

لا أعرف ما إذا كان من الممكن كتابة Combinator Y من خلال منحه نوعًا أعلى من الرتبة. سيفاجئني ذلك ، لكن ليس لدي دليل على أنه غير ممكن. (سيكون المفتاح هو تحديد نوع متعدد الأشكال بشكل مناسب لربط Lambda x.)

إذا كنت تريد مشغل نقطة ثابتة في Haskell ، فيمكنك تحديد واحدة بسهولة كبيرة لأنه في Haskell ، فإن Let-Linding لديه دلالات نقطة ثابتة:

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

يمكنك استخدام هذا بالطريقة المعتادة لتحديد الوظائف وحتى بعض هياكل البيانات المحدودة أو اللانهائية.

من الممكن أيضًا استخدام وظائف على أنواع العودية لتنفيذ نقاط ثابتة.

إذا كنت مهتمًا بالبرمجة بنقاط ثابتة ، فأنت تريد قراءة التقرير الفني لـ Bruce McAdam ان الامر متعلق باللف.

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

إذا كان نظام النوع يسمح بمثل هذه الأنواع المتكررة ، فإنه سيجعل من النوع الذي لا يمكن تفكيكه (عرضة للحلقات اللانهائية).

لكن Combinator Y سيعمل إذا كنت تجبره على TypeCheck ، على سبيل المثال باستخدام 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 " ++)

هذا غير آمن (من الواضح). إجابة رامون يوضح طريقة أكثر أمانًا لكتابة combinator FixPoint في Haskell دون استخدام العودية.