كتابة y combinator

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html هو تعريف موجز لحساب Lambda المكتوب ببساطة في Prolog.

يبدو الأمر جيدًا ، ولكن بعد ذلك يزعم تعيين نوع إلى combinator y ... بينما بالمعنى الحقيقي للغاية ، فإن الغرض الكامل لإضافة أنواع إلى حساب التفاضل والتكامل Lambda هو رفض تعيين نوع لأشياء مثل Combinator.

هل يمكن لأي شخص أن يرى بالضبط أين خطأه أو - على الأرجح - سوء فهمي؟

Answer 1

y combinator في شكله الأساسي

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

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

هناك أمثلة أخرى أسهل بكثير ولكنها ذات مغزى لا يمكن كتابتها على هذا المستوى:

خذ على سبيل المثال

test f = (f 1, f "Hello")

من الواضح أن هذا يعمل لصالح test (\x -> x) لكن لا يمكننا إعطاء النوع العالي المرتبة المطلوب هنا ، أي

test :: (∀a . a -> a) -> (Int, String)  

ولكن حتى في أنظمة النوع الأكثر تقدماً مثل امتدادات Haskell GHCI والتي تسمح بما سبق ، Y لا يزال من الصعب الكتابة.

لذلك ، بالنظر إلى إمكانية التكرار ، يمكننا فقط تعريف والعمل باستخدام fix combinator

fix f = f (fix f) 

مع fix :: (a -> a) -> a

Answer 2

يجب أن تكون الكتابة عدم السماح للتطبيق الذاتي ، ولا ينبغي أن يكون من الممكن العثور على نوع (t t). إذا كان ذلك ممكنا بعد ذلك t سيكون له نوع A -> B, ، وسيكون لدينا A = A -> B. نظرًا لأن التطبيق الذاتي جزء من Y Combinator ، فليس من الممكن أيضًا إعطاء نوع له.

لسوء الحظ ، تسمح العديد من أنظمة Prolog بحل ل A = A -> B. يحدث هذا على العديد من الأسباب ، إما أن نظام Prolog يسمح المصطلحات الدائرية ، ثم سوف ينجح التوحيد ويمكن معالجة الروابط الناتجة. أو لا يسمح نظام Prolog بمصطلحات دائرية ، فهذا يعتمد على ما إذا كان ينفذ فحصًا. في حالة حدوث فحص ، فلن ينجح التوحيد. في حالة إيقاف تشغيل الفحص ، قد ينجح التوحيد ولكن لا يمكن معالجة الارتباطات الناتجة ، مما يؤدي على الأرجح إلى تجاوز الفائض في الطباعة أو التوحيد الإضافي.

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

تتمثل إحدى الطرق لحل المشكلة في تشغيل الفحص أو استبدال أي من التوحيدات التي تحدث في الكود عن طريق مكالمة صريحة إلى unify_with_occurs_check/2.

تحياتي الحارة

ملاحظة: يعمل رمز Prolog التالي بشكل أفضل:

/**
 * Simple type inference for lambda expression.
 *
 * Lambda expressions have the following syntax:
 *    apply(A,B): The application.
 *    [X]>>A: The abstraction.
 *    X: A variable.
 *
 * Type expressions have the following syntax:
 *    A>B: Function domain
 *
 * To be on the save side, we use some unify_with_occurs_check/2.
 */

find(X,[Y-S|_],S) :- X==Y, !.
find(X,[_|C],S) :- find(X,C,S).

typed(C,X,T) :- var(X), !, find(X,C,S), 
                unify_with_occurs_check(S,T).
typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T).
typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), 
                unify_with_occurs_check(S,T).

فيما يلي بعض أشواط العينات:

Jekejeke Prolog, Development Environment 0.8.7
(c) 1985-2011, XLOG Technologies GmbH, Switzerland
?- typed([F-A,G-B],apply(F,G),C).
A = B > C
?- typed([F-A],apply(F,F),B).
No
?- typed([],[X]>>([Y]>>apply(Y,X)),T).
T = _T > ((_T > _Q) > _Q)