इनपुट प्रकार और आउटपुट प्रकार को बाधित कैसे करें?

Question

मैं मैनिंग से इडिस के साथ टाइप संचालित विकास के माध्यम से जा रहा हूं। एक उदाहरण दिया गया है जो सिखाता है कि फ़ंक्शन को किसी प्रकार के परिवार में दिए गए प्रकार में कैसे प्रतिबंधित किया जाए। हमारे पास Vehicle प्रकार है जो PowerSource का उपयोग करता है जो या तो Pedal या Petrol है और हमें एक फ़ंक्शन refill लिखने की आवश्यकता है जो केवल उन वाहनों के लिए टाइप चेक करता है जो पेट्रोल को उनके पावरसोर्स के रूप में उपयोग करते हैं।

नीचे कोड काम करता है, लेकिन यह गारंटी नहीं देता है कि Car को रीफिल करने से Car और Bus नहीं होगा। Car दिए जाने पर दिए जाने पर और Bus का उत्पादन करते समय Car उत्पादन करने की अनुमति देने के लिए मुझे refill फ़ंक्शन के हस्ताक्षर को बदलने की आवश्यकता कैसे होगी?

data PowerSource 
    = Pedal 
    | Petrol 

data Vehicle : PowerSource -> Type 
    where 
    Bicycle : Vehicle Pedal 
    Car : (fuel : Nat) -> Vehicle Petrol 
    Bus : (fuel : Nat) -> Vehicle Petrol 

refuel : Vehicle Petrol -> Nat -> Vehicle Petrol 
refuel (Car fuel) x  = Car (fuel + x) 
refuel (Bus fuel) x  = Bus (fuel + x) 

Answer 1

इस नए VehicleType डेटा प्रकार शुरू करने से और इस तरह Vehicle के लिए एक और पैरामीटर जोड़ने के द्वारा प्राप्त किया जा सकता है:

data VehicleType = BicycleT | CarT | BusT 

data Vehicle : PowerSource -> VehicleType -> Type 
    where 
    Bicycle :     Vehicle Pedal BicycleT 
    Car  : (fuel : Nat) -> Vehicle Petrol CarT 
    Bus  : (fuel : Nat) -> Vehicle Petrol BusT 

आप किसी भी तरह कंस्ट्रक्टर्स के बीच प्रकार अंतर में सांकेतिक शब्दों में बदलना चाहिए। यदि आप अधिक प्रकार की सुरक्षा चाहते हैं तो आपको प्रकारों के लिए अधिक जानकारी जोड़ने की आवश्यकता है। तो आप इसका इस्तेमाल refuel समारोह को लागू करने के कर सकते हैं:

Type checking ./Fuel.idr 
Fuel.idr:14:8:When checking right hand side of refuel with expected type 
     Vehicle Petrol CarT 

Type mismatch between 
     Vehicle Petrol BusT (Type of Bus fuel) 
and 
     Vehicle Petrol CarT (Expected type) 

Specifically: 
     Type mismatch between 
       BusT 
     and 
       CarT 

Answer 2

एक और संभावना के लिए है:

refuel : Vehicle Petrol t -> Nat -> Vehicle Petrol t 
refuel (Car fuel) x  = Car (fuel + x) 
refuel (Bus fuel) x  = Bus (fuel + x) 

refuel (Car fuel) x  = Car (fuel + x) 

की जगह

refuel (Car fuel) x  = Bus (fuel + x) 

के साथ अगले प्रकार की त्रुटि की ओर जाता है क्या करें आप बाहरी रूप से चाहते हैं। यह एक विकल्प हो सकता है जब आप मूल प्रकार को नहीं बदल सकते हैं, उदा। अगर यह पुस्तकालय से आता है। या यदि आप अपने प्रकार को बहुत अधिक अतिरिक्त इंडेक्स के साथ अव्यवस्थित नहीं करना चाहते हैं, तो आप राज्य को और अधिक गुणों में जोड़ना चाहते हैं।

हमें VehicleType प्रकार @Shersh द्वारा शुरू की पुन: उपयोग करते हैं:

data VehicleType = BicycleT | CarT | BusT 

अब, चलो एक समारोह जो हमें बताता है जो निर्माता एक वाहन के निर्माण के लिए इस्तेमाल किया गया था परिभाषित करते हैं।

total 
vehicleType : Vehicle t -> VehicleType 
vehicleType Bicycle = BicycleT 
vehicleType (Car _) = CarT 
vehicleType (Bus _) = BusT 

और अब हम कह सकते हैं कि refuel एक वाहन के प्रकार को बरकरार रखता है:

total 
refuelPreservesVehicleType : vehicleType (refuel v x) = vehicleType v 
refuelPreservesVehicleType {v = (Car _)} = Refl 
refuelPreservesVehicleType {v = (Bus _)} = Refl