अनियमित लैम्ब्डा कैलकुस

Question

में उच्च प्रकार के प्रकार (मोनैड!) को एम्बेड करना उच्च आदेश कार्यों के माध्यम से अनियमित लैम्ब्डा कैलकुस में विभिन्न प्रकारों को एन्कोड करना संभव है।

Examples: 
zero = λfx.  x 
one = λfx.  fx 
two = λfx. f(fx) 
three = λfx. f(f(fx)) 
etc 

true = λtf. t 
false = λtf. f 

tuple = λxyb. b x y 
null = λp. p (λxy. false) 

मैं सोच रहा था कि क्या कोई शोध अन्य कम पारंपरिक प्रकारों को एम्बेड करने में चला गया है। यदि कुछ प्रमेय है जो दावा करता है कि किसी भी प्रकार को एम्बेड किया जा सकता है तो यह शानदार होगा। शायद प्रतिबंध हैं, उदाहरण के लिए केवल प्रकार के प्रकार * एम्बेडेड किया जा सकता है।

तो यह वास्तव में कम पारंपरिक प्रकार का प्रतिनिधित्व करने के लिए संभव है, यह एक उदाहरण देखने के लिए भयानक होगा। मैं विशेष रूप से देख रहा हूं कि मोनैड टाइप क्लास के सदस्य कैसा दिखते हैं।

Answer 1

आप मूल्य स्तर के साथ प्रकार स्तर ऊपर मिश्रण कर रहे हैं। Untyped lambda गणित में कोई monads हैं। मोनैडिक ऑपरेशंस (मान स्तर) हो सकते हैं, लेकिन मोनैड नहीं (प्रकार का स्तर)। ऑपरेशन स्वयं एक जैसा हो सकता है, हालांकि, आप कोई अभिव्यक्तिपूर्ण शक्ति नहीं खोते हैं। तो सवाल स्वयं वास्तव में समझ में नहीं आता है।

Answer 2

ठीक है, हम पहले से ही tuples और बूलियन है, इसलिए हम Either प्रतिनिधित्व करते हैं और बदले में कर सकते हैं किसी भी गैर पुनरावर्ती राशि पर आधारित है कि प्रकार:

type Either a b = (Bool, (a, b)) 
type Maybe a = Either() a 

और हो सकता है कि इकाई प्रकार वर्ग का एक सदस्य है। लैम्ब्डा नोटेशन का अनुवाद व्यायाम के रूप में छोड़ा गया है।

Answer 3

यह बहुत ज्यादा किसी भी प्रकार यदि आप चाहते हैं प्रतिनिधित्व करने के लिए संभव है। लेकिन चूंकि monadic संचालन हर प्रकार के लिए अलग तरह से लागू किया जाता है, यह >>= एक बार लिख सकते हैं और यह हर उदाहरण के लिए काम करने के लिए संभव नहीं है।

हालांकि, अगर आप सामान्य कार्यों कि सबूत typeclass के कहने के पर निर्भर लिख सकते हैं। e यहाँ पर विचार करें एक टपल, जहां fst e एक "बाँध" परिभाषा शामिल है, और snd e एक "वापसी" परिभाषा में शामिल किया जाना है।

bind = λe. fst e -- after applying evidence, bind looks like λmf. ___ 
return = λe. snd e -- after applying evidence, return looks like λx. ___ 

fst = λt. t true 
snd = λt. t false 

-- join x = x >>= id 
join = λex. bind e x (λz. z) 

-- liftM f m1 = do { x1 <- m1; return (f x1) } 
-- m1 >>= \x1 -> return (f x1) 
liftM = λefm. bind e m (λx. return e (f x)) 

आपको फिर मोनाड के प्रत्येक उदाहरण के लिए "सबूत ट्यूपल" परिभाषित करना होगा। ध्यान दें कि जिस तरह से हम bind और return परिभाषित: वे सिर्फ अन्य "सामान्य" इकाई तरीकों हमारे द्वारा निर्धारित किया की तरह काम करते हैं: वे पहली इकाई सत्ता के सबूत दिया जाना चाहिए, और फिर वे आशा के अनुरूप कार्य।

हम Maybe का प्रतिनिधित्व ऐसे फ़ंक्शन के रूप में कर सकते हैं जो 2 इनपुट लेता है, पहला यह है कि यह Just x है, और दूसरा इसे बदलने के लिए एक मूल्य है यदि यह कुछ भी नहीं है।

just = λxfz. f x 
nothing = λfz. z 

-- bind and return for maybes 
bindMaybe = λmf. m f nothing 
returnMaybe = just 

maybeMonadEvidence = tuple bindMaybe returnMaybe 

सूचियां समान हैं, इसकी सूची को फोल्डिंग फ़ंक्शन के रूप में दर्शाती हैं। इसलिए, एक सूची एक ऐसा कार्य है जो 2 इनपुट, एक "विपक्ष" और "खाली" लेता है। यह सूची में foldr myCons myEmpty निष्पादित करता है।

nil = λcz. z 
cons = λhtcz. c h (t c z) 

bindList = λmf. concat (map f m) 
returnList = λx. cons x nil 

listMonadEvidence = tuple bindList returnList 

-- concat = foldr (++) [] 
concat = λl. l append nil 

-- append xs ys = foldr (:) ys xs 
append = λxy. x cons y 

-- map f = foldr ((:) . f) [] 
map = λfl. l (λx. cons (f x)) nil 

Either भी सीधा है। एक फ़ंक्शन के रूप में किसी भी प्रकार का प्रतिनिधित्व करें जो दो फ़ंक्शंस लेता है: यदि यह Left है, तो लागू करने के लिए एक और दूसरा यह लागू करने के लिए Right है।

left = λlfg. f l 
right = λrfg. g r 

-- Left l >>= f = Left l 
-- Right r >>= f = f r 
bindEither = λmf. m left f 
returnEither = right 

eitherMonadEvidence = tuple bindEither returnEither 

मत भूलना, कार्य करता खुद को(a ->) प्रपत्र एक इकाई। और लैम्ब्डा कैलकुस में सब कुछ एक समारोह है ... तो ... इसके बारे में बहुत मुश्किल मत सोचो। ;) Control.Monad.Instances

-- f >>= k = \ r -> k (f r) r 
bindFunc = λfkr. k (f r) r 
-- return = const 
returnFunc = λxy. x 

funcMonadEvidence = tuple bindFunc returnFunc