我们必须把这个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 需要更改为其他内容,但我对这应该是什么感到困惑。
最佳答案
比较一下BoolProp
在带有 Agda 版本的 Haskell 中声明:
data BoolProp :: * -> * where
-- ...
从 Haskell 的角度来看,
BoolProp
是一个一元类型构造函数(大致意思是:给我一个具体类型*
,然后我给你具体类型)。在 build 者中,
BoolProp
单独是没有意义的——它不是一种类型!你必须先给它一个类型(例如 TRUE
在 PTrue
的情况下)。在您的 Agda 代码中,您声明
BoolProp
位于Set
(类似于 Haskell 中的 *
)。但是你的构造函数讲述了一个不同的故事。ptrue : BoolProp true
通过申请
BoolProp
至true
,你是说BoolProp
应该采取Bool
参数并返回 Set
(即 Bool → Set
)。但是你刚才说BoolProp
在 Set
!显然,因为
Bool → Set ≠ Set
, Agda 提示。修正相当简单:
data BoolProp : Bool → Set where
-- ...
现在因为
BoolProp true : Set
,一切都很好,Agda 很高兴。实际上,您可以使 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)
关于haskell - 将 Haskell 代码转换为 Agda,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/10665607/