"Ściśle pozytywnie" w Agdzie

Question

Próbuję zakodować pewne denotujące semantyki w Agdzie w oparciu o program napisany w Haskell.

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

W Agdzie, bezpośrednie tłumaczenie byłoby;

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

ale pojawia się błąd związany z FunVal ponieważ;

Wartość nie jest ściśle dodatnia, ponieważ pojawia się po lewej stronie na strzałką w rodzaju FunVal konstruktora w definicji Value.

Co to oznacza? Czy mogę zakodować to w Agdzie? Czy podchodzę do tego w niewłaściwy sposób?

Dzięki.

Answer 1

HOAS nie działa w Agda, z tego powodu:

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

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

teraz zauważyć, że oceny apply w w daje apply w w powrotem. Termin apply w w nie ma postaci normalnej, która jest nie-nie w agdzie. Korzystanie z tego pomysłu i typu:

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

Możemy wywrzeć sprzeczność.

Jednym ze sposobów wyjścia z tych paradoksów jest umożliwienie wyłącznie pozytywnych typów rekurencyjnych, co wybierają Agda i Coq. Oznacza to, że jeśli deklarują:

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

że F musi być ściśle dodatnia funktor, co oznacza, że ​​może nigdy nie nastąpić X na lewo od każdej strzałki. Więc te typy są ściśle dodatnie w X:

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

Ale nie są to:

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

tak w skrócie, nie można nie reprezentują typ danych w Agda. Kodowanie de Bruijn również nie zadziała, jeśli zamierzasz oceniać warunki. Nie możesz osadzić bezargumentowego rachunku lambda w Agdzie, ponieważ ma on terminy bez normalnych formularzy, a Agda wymaga normalizacji wszystkich programów.