"Streng positiv" in Agda

Question

Ich versuche, einige denotational Semantik in Agda basierend auf einem Programm zu kodieren, das ich in Haskell geschrieben habe.

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

In Agda wäre die direkte Übersetzung;

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

aber ich bekomme einen Fehler in Bezug auf die FunVal weil;

Wert ist nicht unbedingt positiv, weil es auf der linken Seite eines Pfeil in der Art des Konstrukteurs FunVal in der Definition von Wert auftritt.

Was bedeutet das? Kann ich das in Agda verschlüsseln? Gehe ich falsch herum?

Danke.

Answer 1

HOAS funktioniert nicht in Agda, weil dieser:

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

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

Jetzt bemerken, dass wieder apply w w gibt Ihnen apply w w auswertet. Der Begriff apply w w hat keine normale Form, die in AGDA ein No-No ist. Mit dieser Idee und der Art:

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

Wir können einen Widerspruch ableiten.

Einer der Wege aus diesen Paradoxien ist nur streng positive rekursive Typen zuzulassen, was Agda und Coq wählen. Das bedeutet, dass, wenn Sie erklären:

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

dass F ein streng positiver Funktors sein muss, was bedeutet, dass X nie links von jedem Pfeil auftreten kann. So sind diese Arten streng positiv in X:

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

Aber diese sind nicht:

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

Also kurz gesagt, nicht Sie nicht Ihren Datentyp in Agda darstellen können. Und de Bruijn Kodierung funktioniert auch nicht, wenn Sie Begriffe auswerten wollen. Sie können das untypisierte Lambda-Kalkül nicht in Agda einbetten, da es Ausdrücke ohne normale Formen hat und Agda erfordert, dass alle Programme normalisiert werden.