AGDA

Question

को हास्केल कोड परिवर्तित हम AGDA कोड में इस Haskell डेटा प्रकार परिवर्तित करने के लिए है:

module BoolProp where 

open import Data.Bool 
open import Relation.Binary.PropositionalEquality 

data BoolProp : Set wheree 
ptrue : BoolProp true 
pfalse : BoolProp false 
pand : (X Y : Bool) -> BoolProp X -> BoolProp Y -> BoolProp (X ? Y) 
por : (X Y : Bool) -> BoolProp X -> BoolProp Y -> BoolProp (X ? Y) 
pnot : (X : Bool) -> BoolProp X -> BoolProp (not X) 

लेकिन मैं इस त्रुटि हो रही है:

data TRUE 
data FALSE 
data BoolProp :: * -> * where 
PTrue :: BoolProp TRUE 
PFalse :: BoolProp FALSE 
PAnd :: BoolProp a -> BoolProp b -> BoolProp (a `AND` b) 
POr :: BoolProp a -> BoolProp b -> BoolProp (a `OR` b) 
PNot :: BoolProp a -> BoolProp (NOT a) 

यह वही है मैं अब तक है: "सेट एक फ़ंक्शन प्रकार होना चाहिए, लेकिन यह सही नहीं है जब यह जांच प्रकार के फ़ंक्शन के लिए वैध तर्क हैं।" मैं सोच रहा हूं कि सेट को किसी और चीज़ में बदला जाना चाहिए, लेकिन मैं इस बारे में उलझन में हूं कि यह क्या होना चाहिए।

Answer 1

के AGDA संस्करण के साथ हास्केल में BoolProp घोषणा की तुलना करें:

data BoolProp :: * -> * where 
    -- ... 

देखने के हास्केल के दृष्टिकोण से, BoolProp एक एकल प्रकार निर्माता है (जो मोटे तौर पर मतलब है: मुझे एक ठोस प्रकार * दो और मैं तुम्हे ठोस देना वापस टाइप करें)।

कंस्ट्रक्टर में, BoolProp अकेले कोई अर्थ नहीं होगा - यह एक प्रकार नहीं है! उदाहरण के लिए आपको PTrue के मामले में इसे पहले एक प्रकार (TRUE देना होगा)।

अपने एग्डा कोड में, आप बताते हैं कि BoolPropSet में है (जो हैस्केल में * जैसा कुछ है)। लेकिन आपके रचनाकार एक अलग कहानी बताते हैं।

ptrue : BoolProp true 

true को BoolProp को लागू करके, आप कह रहे हैं कि BoolProp एक Bool तर्क लेने के लिए और एक Set (अर्थात Bool → Set) वापस देना चाहिए। लेकिन आपने अभी कहा है कि BoolPropSet में है!

जाहिर है, क्योंकि Bool → Set ≠ Set, आगाडा शिकायत करता है।

सुधार नहीं बल्कि सरल है:

data BoolProp : Bool → Set where 
    -- ... 

और अब क्योंकि BoolProp true : Set, सब कुछ ठीक है और AGDA खुश है।

---

आप वास्तव में हास्केल कोड को थोड़ा अच्छा बना सकते हैं और आपको तुरंत समस्या दिखाई देगी!

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeFamilies #-} 
module Main where 

type family And (a :: Bool) (b :: Bool) :: Bool 
type instance And True b = b 
type instance And False b = False 

type family Or (a :: Bool) (b :: Bool) :: Bool 
type instance Or True b = True 
type instance Or False b = b 

type family Not (a :: Bool) :: Bool 
type instance Not True = False 
type instance Not False = True 

data BoolProp :: Bool -> * where 
    PTrue :: BoolProp True 
    PFalse :: BoolProp False 
    PAnd :: BoolProp a -> BoolProp b -> BoolProp (And a b) 
    POr :: BoolProp a -> BoolProp b -> BoolProp (Or a b) 
    PNot :: BoolProp a -> BoolProp (Not a)