प्रकार हस्ताक्षर कि कभी भी कोई भावना

Question

पर विचार करें

(a->a) -> [a] -> Bool 

इस हस्ताक्षर के लिए किसी भी सार्थक परिभाषा है? यह एक परिभाषा है जो तर्क को अनदेखा नहीं करती है?

x -> [a] -> Bool 

ऐसा लगता है कि ऐसे कई हस्ताक्षर हैं जिन्हें तुरंत अस्वीकार कर दिया जा सकता है।

Answer 1

कार्स्टन König मुक्त प्रमेय उपयोग करने के लिए एक टिप्पणी में सुझाव दिया। आइए कोशिश करें।

प्रधानमंत्री तोप

हम generating the free theorem से शुरू प्रकार (a->a) -> [a] -> Bool करने के लिए इसी। यह एक संपत्ति है कि उस प्रकार के हर समारोह को प्रसिद्ध वाडलर के पेपर Theorems for free! द्वारा स्थापित किया जाना चाहिए।

forall t1,t2 in TYPES, R in REL(t1,t2). 
forall p :: t1 -> t1. 
    forall q :: t2 -> t2. 
    (forall (x, y) in R. (p x, q y) in R) 
    ==> (forall (z, v) in lift{[]}(R). f_{t1} p z = f_{t2} q v) 

lift{[]}(R) 
    = {([], [])} 
    u {(x : xs, y : ys) | ((x, y) in R) && ((xs, ys) in lift{[]}(R))} 

एक उदाहरण

बेहतर, ऊपर प्रमेय को समझने के लिए एक ठोस उदाहरण के ऊपर चलने देने के लिए। प्रमेय का उपयोग करने के लिए, हमें किसी भी दो प्रकार t1,t2 लेने की आवश्यकता है, इसलिए हम t1=Bool और t2=Int चुन सकते हैं।

फिर हम एक समारोह p :: Bool -> Bool (माना p=not), और एक समारोह q :: Int -> Int (माना q = \x -> 1-x) का चयन करने की जरूरत है।

अब, हमें RBool एस और Int एस के बीच संबंध को परिभाषित करने की आवश्यकता है। चलिए मानक बुलियन < -> पूर्णांक पत्राचार, यानी लेते हैं।:

R = {(False,0),(True,1)} 

(उपर्युक्त एक-एक पत्राचार है, लेकिन यह सामान्य रूप से होना आवश्यक नहीं है)।

अब हमें (forall (x, y) in R. (p x, q y) in R) जांचना होगा।

Case (x,y) = (False,0): we verify that (not False, 1-0) = (True, 1) in R (ok!) 
Case (x,y) = (True ,1): we verify that (not True , 1-1) = (False,0) in R (ok!) 

अब तक तो अच्छा: हम केवल (x,y) in R की जांच करने के दो मामलों की है। अब सूचियों पर काम करने के लिए हमें संबंध को "उठाना" चाहिए: उदा।

[True,False,False,False] is in relation with [1,0,0,0] 

इस विस्तारित संबंध ऊपर lift{[]}(R) नामित एक है।

अंत में, प्रमेय के अनुसार, के लिए किसी भी समारोह f :: (a->a) -> [a] -> Bool हम होना आवश्यक है

f_Bool not [True,False,False,False] = f_Int (\x->1-x) [1,0,0,0] 

जहां f_Bool ऊपर बस यह स्पष्ट है कि f विशेष मामले में प्रयोग किया जाता है बनाता है जो a=Bool में।

इस की शक्ति यह है कि हम नहीं जानते कि f का कोड वास्तव में क्या है। हम f को अपने पॉलीमोर्फिक प्रकार को देखकर संतुष्ट होना चाहिए।

चूंकि हमें प्रकार अनुमान से प्रकार मिलते हैं, और हम प्रकारों को प्रमेय में बदल सकते हैं, हम वास्तव में "मुफ्त में प्रमेय" प्राप्त करते हैं।

मूल लक्ष्य

हम साबित होता है कि f अपनी पहली तर्क का उपयोग नहीं करता है, और अपने दूसरे सूची तर्क के बारे में परवाह है कि नहीं है, या तो, इसकी लंबाई के अलावा चाहते हैं वापस।

इसके लिए, R सार्वभौमिक रूप से वास्तविक संबंध बनें। फिर, lift{[]}(R) एक रिश्ता है जो दो सूचियों से संबंधित है अगर उनके पास समान लंबाई है।

प्रमेय तो अर्थ है:

forall t1,t2 in TYPES. 
forall p :: t1 -> t1. 
    forall q :: t2 -> t2. 
    forall z :: [t1]. 
    forall v :: [t2]. 
    length z = length v ==> f_{t1} p z = f_{t2} q v 

इसलिए, f पहला तर्क पर ध्यान न देकर केवल एक दूसरे की लंबाई के बारे में परवाह है।

QED

Answer 2

आप x के साथ अपने आप में कुछ भी दिलचस्प नहीं कर सकते।

आप [x] के साथ सामान कर सकते हैं; उदाहरण के लिए, आप गिन सकते हैं कि सूची में कितने नोड्स हैं।

big :: (x -> Int) -> x -> Bool 
big f n = if f n > 10 then True else False 

x कुछ प्रकार वर्ग के अंतर्गत आता है, तो: तो, उदाहरण के लिए,

foo :: (a -> a) -> [a] -> Bool 
foo _ [] = True 
foo _ (_:_) = False 

bar :: x -> [a] -> Bool 
bar _ [] = True 
bar _ (_:_) = False 

आप एक x और एक समारोह है कि कुछ और में एक x बदल जाता है, तो आप रोचक सामग्री क्या कर सकते हैं आप उस वर्ग के सभी तरीकों का उपयोग कर सकते हैं। (। यह वास्तव में पिछले एक की एक विशेष मामला है)

double :: Num x => x -> x 
double = (2*) 

दूसरी ओर, वहाँ प्रकार हस्ताक्षर के बहुत सारे हैं, जिसके लिए कोई वैध कार्यों मौजूद हैं:

magic :: x -> y 
magic = -- erm... good luck with that! 

मैंने कहीं पढ़ा है कि प्रकार के हस्ताक्षर जिसमें केवल वेरिएबल्स शामिल हैं जिनके लिए वास्तविक फ़ंक्शन मौजूद है, वे वास्तव में तार्किक प्रमेय हैं जो सत्य हैं। (मैं इस संपत्ति के लिए नाम पता नहीं है, लेकिन यह काफी दिलचस्प है।)

f1 :: (x -> y) -> x -> y 
-- Given that X implies Y, and given that X is true, then Y is true. 
-- Well, duh. 

f2 :: Either (x -> y) (x -> z) -> x -> Either y z 
-- Given that X implies Y or X implies Z, and given X, then either Y or Z is true. 
-- Again, duh. 

f3 :: x -> y 
-- Given that X is true, then any Y is true. 
-- Erm, no. Just... no.