"Strictly positiv" in AGDA

Question

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.

Answer 1

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.