"Strictement positif" dans Agda

Question

J'essaye de coder une sémantique dénotationnelle dans Agda basée sur un programme que j'ai écrit dans Haskell.

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

Dans Agda, la traduction directe serait;

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

mais j'obtiens une erreur relative au FunVal car;

valeur n'est pas strictement positif, car il se produit à la gauche d'une flèche dans le type du constructeur FunVal dans la définition de la valeur .

Qu'est-ce que cela signifie? Puis-je l'encoder dans Agda? Est-ce que je vais dans le mauvais sens?

Merci.

Answer 1

HOAS ne fonctionne pas dans Agda, à cause de cela:

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

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

Maintenant, remarquez que l'évaluation apply w w vous donne apply w w à nouveau. Le terme apply w w n'a pas de forme normale, ce qui est un non-no dans agda. En utilisant cette idée et le type:

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

Nous pouvons en déduire une contradiction. L'une des façons de sortir de ces paradoxes est seulement de permettre des types récursifs strictement positifs, ce que choisissent Agda et Coq. Cela signifie que si vous déclarez:

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

Ce F doit être un foncteur strictement positif, ce qui signifie que X ne peut jamais se produire à la gauche d'une flèche. Ainsi, ces types sont strictement positifs dans X:

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

Mais ce ne sont pas:

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

Donc en bref, pas vous ne pouvez pas représenter votre type de données dans Agda. Et l'encodage de Bruijn ne fonctionnera pas non plus si vous allez évaluer les termes. Vous ne pouvez pas intégrer le calcul lambda non typé dans Agda car il contient des termes sans les formes normales et Agda exige que tous les programmes soient normalisés.