Convert Haskell code to Agda

Question

We must convert this haskell data type to agda code:

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) 

This is what I still have:

 module BoolProp where open import Data.Bool open import Relation.Binary.PropositionalEquality data BoolProp : Set wheree ptrue : BoolProp true pfalse : BoolProp false pand : (XY : Bool) -> BoolProp X -> BoolProp Y -> BoolProp (X ? Y) por : (XY : Bool) -> BoolProp X -> BoolProp Y -> BoolProp (X ? Y) pnot : (X : Bool) -> BoolProp X -> BoolProp (not X) 

But I get this error: "Set must be a type of function, but this is not when verifying that true are valid arguments for a function of type Set." I think Set needs to be changed to something else, but I'm confused as to what it should be.

Answer 1

Let's compare the BoolProp ad in Haskell with the Agda version:

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

From a Haskell point of view, BoolProp is a unary type constructor (which roughly means: give me a specific type * , and I will give you a specific type).

In the BoolProp constructors BoolProp one would not make sense - this is not a type! You must first give it a type ( TRUE in the case of PTrue ).

In the Agda code, you indicate that BoolProp is in Set (something like * in Haskell). But your designers tell a different story.

 ptrue : BoolProp true 

When applying BoolProp to TRUE , you say that BoolProp should accept a Bool argument and return a Set (i.e. Bool → Set ). But you just said that BoolProp is in Set !

Obviously, since Bool → Set ≠ Set , Agda complains.

The correction is quite simple:

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

And now, because BoolProp true : Set , everything is fine, and Agda is happy.

---

You could make the Haskell code a little nicer and you will immediately see the problem!

 {-# 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 ab) POr :: BoolProp a -> BoolProp b -> BoolProp (Or ab) PNot :: BoolProp a -> BoolProp (Not a)