"Estrictamente positivo" en Agda

Question

Estoy tratando de codificar algo de semántica denotacional en AGDA basada en un programa que escribí en Haskell.

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

En AGDA, la traducción directa sería;

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

Pero recibo un error relacionado con el fúnVal porque;

El valor no es estrictamente positivo, porque ocurre a la izquierda de una flecha en el tipo de funval del constructor en la definición de valor.

¿Qué significa esto? ¿Puedo codificar esto en AGDA? ¿Lo estoy haciendo de la manera incorrecta?

Gracias.

Answer 1

Hoas No funciona en AGDA, debido a esto:

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

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

Ahora, observe que evaluar apply w w te dio apply w w de nuevo. El término apply w w no tiene forma normal, que es un no-no en agda. Usando esta idea y el tipo:

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

Podemos derivar una contradicción.

Una de las formas de salir de estas paradojas es solo permitir tipos recursivos estrictamente positivos, que es lo que el eligen AGDA y COQ. Eso significa que si declaras:

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

Que F debe ser un functor estrictamente positivo, lo que significa que X Puede que nunca ocurra a la izquierda de ninguna flecha. Entonces estos tipos son estrictamente positivos en X:

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

Pero estos no son:

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

En resumen, no, no puede representar su tipo de datos en AGDA. Puede usar la codificación de De Bruijn para obtener un tipo de término con el que pueda trabajar, pero generalmente la función de evaluación necesita algún tipo de "tiempo de espera" (generalmente llamado "combustible"), por ejemplo, un número máximo de pasos para evaluar, porque AGDA requiere todas las funciones ser total. Aquí hay un ejemplo Debido a @gallais, que utiliza un tipo de parcialidad coinductiva para lograr esto.