Converting Haskell code to Agda

Question

We have to convert this haskell data type into 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 have so far: ``` 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) ``` But I'm getting this error: "Set should be a function type, but it isn't when checking that true are valid arguments to a function of type Set". I'm thinking that Set needs to be changed to something else, but I'm confused as to what this should be.

Accepted Answer

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

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

From Haskell's point of view, `BoolProp` is a unary type constructor (which roughly means: give me a concrete type `*` and I give you concrete type back).

In the constuctors, `BoolProp` alone would make no sense - it's not a type! You have to give it a type first (`TRUE` in case of `PTrue`, for example).

In your Agda code, you state that `BoolProp` lies in `Set` (which is something like `*` in Haskell). But your constructors tell a different story.

```
ptrue : BoolProp true
```

By applying `BoolProp` to `true`, you're telling that `BoolProp` should take a `Bool` argument and give back a `Set` (i.e. `Bool → Set`). But you just said that `BoolProp` is in `Set`!

Obviously, because `Bool → Set ≠ Set`, Agda complains.

The correction is rather simple:

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

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

You could actually make the Haskell code a bit nicer and you'd see the problem right away!

```
{-# 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)
```

Converting Haskell code to Agda

Solution

Problem