मोटे तौर पर, मैंज्ञात पैटर्न मैच
check : UExpr -> Maybe Expr
है और मैं एक परीक्षण अवधि
testTerm : UExpr
कौन सा मुझे आशा है कि check होगा सफलतापूर्वक, जिसके बाद मैं जिसके परिणामस्वरूप Expr निकालने और हेरफेर करने के लिए करना चाहते हैं यह आगे मूल रूप से
realTerm : Expr
just realTerm = check testTerm
इस तरह की है कि इस परिभाषा यदि check testTerm निकला nothing होने की typecheck करने में विफल रहते हैं। क्या यह संभव है?
सामान्य सौदा मीटर एक सफलता के लिए गणना करता है तो जैसे
Just : {X : Set} -> Maybe X -> Set
Just (just x) = One -- or whatever you call the fieldless record type
Just nothing = Zero
justify : {X : Set}(m : Maybe X){p : Just m} -> X
justify (just x) = x
justify nothing {()}
कुछ लिखना है, पी के प्रकार से एक है और मूल्य मान लिया जाता है।
मैंने अभी भी 'ट्रू' के साथ उस मुहावरे को देखना शुरू कर दिया था, लेकिन वास्तव में इसमें खोद नहीं आया था। धन्यवाद। – luqui
वैसे मुझे ऐसा करने का एक तरीका मिला, जो कि विचित्र और जादुई है।
testTerm-checks : Σ Expr (\e -> check testTerm ≡ just e)
testTerm-checks = _ , refl
realTerm : Expr
realTerm = proj₁ testTerm-checks
यह मुझे हेबी जीबी देता है, लेकिन खराब तरीके से नहीं। अभी भी इसे करने के अन्य तरीकों में रुचि रखते हैं।
आपको शायद [स्तर के स्तर पर एक को खत्म करना] मिल सकता है (http://stackoverflow.com/questions/31105947/eliminating-a-maybe-at-the-type-level) उपयोगी। – user3237465
नीचे दिए गए तकनीकी उत्तरों के विपरीत, मैं यह इंगित करना चाहता हूं कि आप गैर-कार्यात्मक सोच रहे हैं। यह किसी ऐसे व्यक्ति की तरह है जो 'आईओ' मोनैड से छुटकारा पाना चाहता है और हरस्केल में हर जगह अनिवार्य कोड लिखता है: आम तौर पर, 'शायद' प्रकार की अवधि से अंतर्निहित प्रकार निकालने का कोई तरीका नहीं है; यह एजडा जैसे मजबूत कार्यात्मक प्रोग्रामिंग भाषाओं का सारांश है, इसलिए आपको मोनाड को तब तक पास करना होगा जब तक कि आपको किसी अन्य प्रकार के मूल्य में एन्कोड करने का कोई अच्छा तरीका न मिल जाए। –