"Strictly positiv" in AGDA
-
24-09-2019 - |
Frage
Ich versuche, einige Denotationssemantik in AGDA zu codieren, basierend auf einem Programm, 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 den Funval, weil;
Der Wert ist nicht streng positiv, da er links von einem Pfeil im Typ des Konstruktors -Funval in der Definition von Wert auftritt.
Was bedeutet das? Kann ich das in AGDA codieren? Gehe ich falsch vor?
Vielen Dank.
Lösung
HOAS Funktioniert nicht in AGDA, aus diesem Grund:
apply : Value -> Value -> Value
apply (FunVal f) x = f x
apply _ x = Error "Applying non-function"
w : Value
w = FunVal (\x -> apply x x)
Beachten Sie nun, dass die Bewertung bewertet wird apply w w
gibt Ihnen apply w w
wieder zurück. Der Begriff apply w w
hat keine normale Form, was in AGDA ein Nein-Nein ist. Verwenden Sie diese Idee und den Typ:
data P : Set where
MkP : (P -> Set) -> P
Wir können einen Widerspruch ableiten.
Einer der Wege aus diesen Paradoxien besteht nur darin, streng positive rekursive Typen zu ermöglichen, was AGDA und COQ wählen. Das heißt, wenn Sie deklarieren:
data X : Set where
MkX : F X -> X
Dass F
Muss ein streng positiver Fondor sein, was bedeutet, dass das bedeutet X
kann niemals links von einem Pfeil auftreten. Diese Typen sind also 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
Kurz gesagt, nein, Sie können Ihren Datentyp in AGDA nicht darstellen. Sie können De Bruijn -Codierung verwenden, um einen Termtyp zu erhalten, mit dem Sie arbeiten können, aber in der Regel benötigt die Bewertungsfunktion eine Art "Zeitüberschreitung" (allgemein als "Kraftstoff" bezeichnet), z. total sein. Hier ist ein Beispiel Aufgrund von @Gallais, die einen koinduktiven Parteilichkeitstyp verwendet, um dies zu erreichen.