conversione del codice Haskell a Agda

Question

Dobbiamo convertire questo tipo di dati Haskell in agda codice:

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) 

Questo è quello che ho finora:

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) 

Ma sto ottenendo questo errore: "Set dovrebbe essere un tipo di funzione, ma non lo è quando si verifica che true siano argomenti validi per una funzione di tipo Set". Sto pensando che Set debba essere cambiato in qualcos'altro, ma sono confuso su cosa dovrebbe essere.

Answer 1

Confrontiamo BoolProp dichiarazione in Haskell con la versione Agda:

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

Dal punto di vista di Haskell, BoolProp è un tipo costruttore unario (che significa più o meno: dammi un tipo concreto * e io ti do in calcestruzzo digitare indietro).

Nei costanti, solo BoolProp non avrebbe senso - non è un tipo! Devi prima dargli un tipo (TRUE in caso di PTrue, per esempio).

Nel codice Agda, si specifica che BoolProp si trova in Set (che è qualcosa come * in Haskell). Ma i tuoi costruttori raccontano una storia diversa.

ptrue : BoolProp true 

Applicando BoolProp a true, stai dicendo che BoolProp dovrebbe prendere un argomento Bool e restituire un Set (vale a dire Bool → Set). Ma hai appena detto che BoolProp è in Set!

Ovviamente, perché Bool → Set ≠ Set, lamenta Agda.

la correzione è piuttosto semplice:

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

E ora perché BoolProp true : Set, va tutto bene e Agda è felice.

---

Si potrebbe effettivamente rendere il codice Haskell un po 'più bello e si vedrebbe il problema subito!

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