« Strictement positif » dans Agda
-
24-09-2019 - |
Question
Je suis en train de coder une sémantique dénotationnelle en Agda sur la base d'un programme que j'ai écrit en 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 je reçois une erreur relative à la FunVal car;
La valeur est pas strictement positif, car il se produit à la gauche d'un flèche dans le type du constructeur FunVal dans la définition de Valeur.
Qu'est-ce que cela signifie? Puis-je encoder cela en Agda? Est-ce que je vais parler de la mauvaise façon?
Merci.
La solution
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, notez 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-non dans agda. En utilisant cette idée et le type:
data P : Set where
MkP : (P -> Set) -> P
On peut déduire une contradiction.
L'une des façons de sortir de ces paradoxes est que pour permettre les types récursifs strictement positifs, ce qui est ce que Agda et Coq choisissent. 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. Vous pouvez utiliser le codage de Bruijn pour obtenir un type de terme que vous pouvez travailler avec, mais en général la fonction d'évaluation a besoin une sorte de « délai d'attente » (généralement appelé « carburant »), par exemple un nombre maximum d'étapes pour évaluer, car Agda exige que toutes les fonctions être totale. est un exemple en raison de @gallais qui utilise un type de partialité CoInductive pour ce faire.