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.

Answer 1

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)