conversión de código Haskell a Agda

Question

Tenemos que convertir este tipo de datos en Haskell agda código:

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) 

Esto es lo que tengo hasta ahora:

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) 

Pero estoy recibiendo este error: "Set debería ser un tipo de función, pero no es cuando se comprueba que los argumentos válidos son verdaderos para una función de tipo Set". Estoy pensando que Set debe cambiarse a otra cosa, pero estoy confundido en cuanto a lo que debería ser.

Answer 1

Comparemos BoolProp declaración en Haskell con la versión Agda:

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

Desde el punto de vista de Haskell, BoolProp es un constructor de tipo unaria (que significa aproximadamente: dame un tipo concreto * y te doy concreto escriba hacia atrás).

En los constructores, BoolProp solo no tendría sentido, ¡no es un tipo! Primero debe darle un tipo (TRUE en el caso de PTrue, por ejemplo).

En su código Agda, indica que BoolProp se encuentra en Set (que es algo así como * en Haskell). Pero tus constructores cuentan una historia diferente.

ptrue : BoolProp true 

Aplicando BoolProp a true, usted está diciendo que BoolProp debe tomar un argumento Bool y devolver un Set (es decir Bool → Set). ¡Pero usted acaba de decir que BoolProp está en Set!

Obviamente, porque Bool → Set ≠ Set, Agda se queja.

La corrección es bastante simple:

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

Y ahora porque BoolProp true : Set, todo está bien y Agda es feliz.

---

En realidad, podría hacer que el código de Haskell fuera un poco más agradable y ¡vería el problema de inmediato!

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