将 Haskell 代码转换为 Agda答案

【问题标题】：Converting Haskell code to Agda将 Haskell 代码转换为 Agda
【发布时间】：2012-05-26 19:03:24
【问题描述】：

我们要把这个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 需要更改为其他内容，但我对这应该是什么感到困惑。

【问题讨论】：

标签： haskell agda

【解决方案1】：

让我们比较一下 Haskell 中的 BoolProp 声明和 Agda 版本：

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

从 Haskell 的角度来看，BoolProp 是一个一元类型构造函数（大致意思是：给我一个具体类型 *，我给你具体类型回来）。

在构造函数中，单独使用 BoolProp 是没有意义的——它不是类型！您必须先给它一个类型（例如PTrue 的情况下为TRUE）。

在您的 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)

【讨论】：