वाई संयोजक टाइपिंग

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html प्रोलॉग में बस टाइप किए गए लैम्ब्डा कैलकुस की संक्षिप्त परिभाषा है।

यह ठीक दिखता है, लेकिन फिर वह वाई संयोजक को एक प्रकार निर्दिष्ट करने के लिए कहता है ... जबकि एक बहुत ही वास्तविक अर्थ में लैम्ब्डा कैलकुस में प्रकार जोड़ने का पूरा उद्देश्य वाई जैसे चीजों को एक प्रकार असाइन करना है 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) 

लेकिन फिर भी हास्केल के GHCi एक्सटेंशन जो अनुमति देते हैं जैसे और अधिक उन्नत प्रकार प्रणालियों में नहीं दे सकता ऊपर, Y टाइप करना अभी भी मुश्किल है।

तो, प्रत्यावर्तन की संभावना को देखते हुए, हम सिर्फ और काम fix Combinator

fix f = f (fix f) 

साथ fix :: (a -> a) -> a

Answer 2

लेखन का उपयोग करके स्वयं आवेदन की अनुमति नहीं देने चाहिए परिभाषित कर सकते हैं, यह पता लगाने के लिए संभव नहीं होना चाहिए (t t) के लिए एक प्रकार। यदि यह संभव हो तो t एक प्रकार A -> B होगा, और हमारे पास A = A -> B होगा। चूंकि स्वयं अनुप्रयोग वाई संयोजक का हिस्सा है, इसलिए इसे एक प्रकार देना भी संभव नहीं है।

दुर्भाग्य से कई प्रोलॉग सिस्टम A = A -> B के लिए समाधान की अनुमति देते हैं। यह कई आधारों पर होता है, या तो प्रोलॉग सिस्टम सर्कुलर शर्तों की अनुमति देता है, तो एकीकरण सफल हो जाएगा और परिणामी बाइंडिंग को और भी संसाधित किया जा सकता है। या प्रोलॉग सिस्टम परिपत्र शर्तों की अनुमति नहीं देता है, तो यह इस बात पर निर्भर करता है कि यह एक होता है चेक लागू करता है या नहीं। यदि होता है चेक चालू होता है, तो एकीकरण सफल नहीं होगा। यदि होता है चेक बंद हो जाता है, तो एकीकरण सफल हो सकता है लेकिन परिणामी बाइंडिंग को संसाधित नहीं किया जा सकता है, अधिकतर प्रिंटिंग या आगे के एकीकरण में ओवरफ्लो का कारण बनता है।

तो मुझे लगता है कि इस प्रकार का गोलाकार एकीकरण प्रयुक्त प्रोलॉग सिस्टम द्वारा दिए गए कोड में होता है और यह अनजान हो जाता है।

समस्या को हल करने का एक तरीका या तो होता है चेक को स्विच करना होगा या कोड में किसी भी अज्ञात एकीकरण को 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)