haskell - que - Comprobación de tipos de Agda y conmutatividad/asociatividad de+

que es conmutativa asociativa y elemento neutro

Question

Dado que la Operación _+_ para Nat generalmente se define recursivamente en el primer argumento, es obvio que no es trivial para que el verificador de tipos sepa que i + 0 == i . Sin embargo, con frecuencia me encuentro con este problema cuando escribo funciones en vectores de tamaño fijo.

Un ejemplo: ¿Cómo puedo definir una función Agda?

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)

¿Qué pone los primeros n valores al final del vector?

Dado que una solución simple en Haskell sería

swap 0 xs     = xs
swap n (x:xs) = swap (n-1) (xs ++ [x])

Lo intenté análogamente en Agda así:

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {_} {zero} xs          = xs 
swap {_} {_} {suc i} (x :: xs)  = swap {_} {_} {i} (xs ++ (x :: []))

Pero el verificador de tipo falla con el mensaje (que se relaciona con el caso {zero} en el swap anterior -Definición):

.m != .m + zero of type Nat
when checking that the expression xs has type Vec .A (.m + zero)

Entonces, mi pregunta: ¿Cómo enseñar a Agda, que m == m + zero ? ¿Y cómo escribir una función de swap en Agda?

Answer 1

Enseñar a Agda que m == m + zero no es demasiado difícil. Por ejemplo, utilizando el tipo estándar para pruebas de igualdad, podemos escribir esta prueba:

rightIdentity : (n : Nat) -> n + 0 == n
rightIdentity zero = refl
rightIdentity (suc n) = cong suc (rightIdentity n)

Luego podemos decirle a Agda que use esta prueba usando la palabra clave rewrite :

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {m} {zero} xs rewrite rightIdentity m = xs 
swap {_} {_} {suc i} (x :: xs) = ?

Sin embargo, proporcionar las pruebas necesarias para la segunda ecuación es mucho más difícil. En general, es una idea mucho mejor intentar que la estructura de sus cálculos coincida con la estructura de sus tipos . De esa manera, puede salirse con mucha menos prueba de teoremas (o ninguna en este caso).

Por ejemplo, asumiendo que tenemos

drop : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A m
take : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A n

(Ambos se pueden definir sin ninguna prueba de teorema), Agda aceptará felizmente esta definición sin ningún problema:

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)
swap {_} {_} {n} xs = drop n xs ++ take n xs