« Strictement positif » dans Agda

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.

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, 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.