轉換哈斯克爾代碼阿格達

Question

我們必須這樣Haskell的數據類型轉換成AGDA代碼：

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) 

這是我到目前爲止有：

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) 

但我發現了這個錯誤： 「Set應該是一個函數類型，但是在檢查true是一個類型爲Set的函數的有效參數時不是。我在想，Set需要改成別的東西，但我對這個應該是什麼感到困惑。

Answer 1

讓我們比較BoolProp聲明在Haskell與阿格達版本：

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

從Haskell的角度來看，BoolProp是一元型構造（大致意思是：給我一個具體類型*，我給你具體的鍵入返回）。

在構建器中，BoolProp本身就沒有意義 - 它不是一種類型！您必須先給它一個類型（例如TRUE，例如PTrue）。

在您的Agda代碼中，您聲明BoolProp位於Set（與Haskell中的*類似）。但是你的構造者講述了一個不同的故事。

ptrue : BoolProp true 

通過應用BoolProp到true，你告訴那個BoolProp應採取Bool參數，並給回一個Set（即Bool → Set）。但你剛纔說BoolProp在Set！

很明顯，因爲Bool → Set ≠ Set，阿格達抱怨。

修正相當簡單：

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

而現在由於BoolProp true : Set，一切都很好，阿格達是幸福的。

---

你實際上可以使Haskell代碼更好一點，你會立即看到問題！

{-# 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)