8

この 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)

しかし、私はこのエラーを受け取ります:「セットは関数型である必要がありますが、true がセット型の関数への有効な引数であることを確認するときではありません」。Set を別のものに変更する必要があると考えていますが、これがどうあるべきか混乱しています。

4

1 に答える 1

15

BoolPropHaskell での宣言を Agda バージョンと比較してみましょう。

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

Haskell の観点からBoolPropは、単項型コンストラクターです (つまり、具体的な型*を渡せば、具体的な型が返されます)。

コンストラクターでは、BoolProp単独では意味がありません-それは型ではありません! 最初にタイプを指定する必要があります（たとえば、のTRUE場合PTrue）。

あなたの Agda コードでBoolPropは、 ( HaskellSetのようなものです) にあると述べています。*しかし、コンストラクターは別の話をします。

ptrue : BoolProp true

に適用BoolPropすることで、 が引数を取り、 (つまり)を返す必要があるtrueことを伝えています。しかし、あなたはそれがにあると言った！BoolPropBoolSetBool → SetBoolPropSet

明らかに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)
于 2012-05-19T14:55:23.967 に答える