"Rigorosamente positivo" in Agda

Question

Sto provando a codificare una semantica denotazionale in Agda basata su un programma che ho scritto in Haskell.

data Value = FunVal (Value -> Value) 
      | PriVal Int 
      | ConVal Id [Value] 
      | Error String 

In Agda, la traduzione diretta sarebbe;

data Value : Set where 
    FunVal : (Value -> Value) -> Value 
    PriVal : ℕ -> Value 
    ConVal : String -> List Value -> Value 
    Error : String -> Value 

ma ottengo un errore relativo al FunVal perché;

Il valore non è strettamente positiva, perché si verifica a sinistra di una freccia nel tipo di FunVal costruttore nella definizione di Valore.

Cosa significa? Posso codificarlo in Agda? Sto andando nel modo sbagliato?

Grazie.

Answer 1

HOAS non funziona in Agda, a causa di questo:

apply : Value -> Value -> Value 
apply (FunVal f) x = f x 
apply _ x = Error "Applying non-function" 

w : Value 
w = FunVal (\x -> apply x x) 

Ora, si noti che la valutazione apply w w ti dà apply w w di nuovo. Il termine apply w w non ha una forma normale, che è un no-no in agda. Usando questa idea e il tipo:

data P : Set where 
    MkP : (P -> Set) -> P 

Possiamo derivare una contraddizione.

Uno dei modi per uscire da questi paradossi è solo quello di consentire tipi ricorsivi strettamente positivi, che è ciò che Agda e Coq scelgono. Ciò significa che se si dichiara:

data X : Set where 
    MkX : F X -> X 

che F deve essere un funtore strettamente positiva, il che significa che non può mai verificarsi X alla sinistra di qualsiasi freccia. Così questi tipi sono strettamente positiva in X:

X * X 
Nat -> X 
X * (Nat -> X) 

Ma queste non sono:

X -> Bool 
(X -> Nat) -> Nat -- this one is "positive", but not strictly 
(X * Nat) -> X 

Così, in breve, non si può non rappresentare il tipo di dati in Agda. E la codifica de Bruijn non funzionerà neanche se valuterai i termini. Non è possibile incorporare il calcolo lambda non tipizzato in Agda perché ha termini senza forme normali e Agda richiede che tutti i programmi si normalizzino.