将Haskell代码转换为Agda

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

让我们将BoolPropHaskell中的声明与Agda版本进行比较:

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,一切都很好,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)