Abrir pruebas de nivel de tipo en Haskell/Idris

proof category-theory

Question

En Idris / Haskell, uno puede probar las propiedades de los datos anotando los tipos y utilizando los constructores de GADT, como con Vect, sin embargo, esto requiere que la propiedad esté codificada en el tipo (por ejemplo, un Vect tiene que ser un tipo separado de una lista). ¿Es posible tener tipos con un conjunto abierto de propiedades (como una lista que tenga tanto una longitud como un promedio de ejecución), por ejemplo, sobrecargando constructores o usando algo en la vena de Efecto?

Answer 1

Creo que McBride ha respondido esa pregunta (para la teoría de tipos) en su artículo de ornamentación (pdf) . El concepto que está buscando es el de un adorno algebraico (énfasis mío):

Un álgebra describe un método estructural para interpretar datos, dando lugar a una operación de plegado, aplicando el método de forma recursiva. Como era de esperar, el árbol resultante de llamadas a φ tiene la misma estructura que los datos originales: ese es el punto, después de todo. Pero ¿y si ese fuera, antes de todo, el punto? Supongamos que quisiéramos corregir el resultado de fold φ por adelantado, representando solo aquellos datos que darían la respuesta que queríamos. Deberíamos necesitar los datos para que se ajusten a un árbol de φ llamadas que ofrezca esa respuesta. ¿Podemos restringir nuestros datos exactamente a eso? Por supuesto que podemos, si nos indexamos por la respuesta.

Ahora, vamos a escribir un código. Lo he puesto todo en una lista porque voy a intercalar los comentarios aquí. Además, estoy usando Agda, pero debería ser fácil de traducir a Idris.

module reornament where

Comenzamos por definir lo que significa ser un álgebra que entrega B actúan en una lista de A s. Necesitamos un caso base (un valor de tipo B ) así como una forma de combinar el encabezado de la lista con la hipótesis de inducción.

ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)

Dada esta definición, podemos definir un tipo de listas de A s indexadas por B s cuyo valor es precisamente el resultado del cálculo correspondiente a un ListAlg AB dado. En el caso nil , el resultado es el caso base que nos proporciona el álgebra ( proj₁ alg ), mientras que en el caso de los cons , simplemente combinamos la hipótesis de inducción con la nueva cabeza utilizando la segunda proyección:

data ListSpec (A : Set) {B : Set} (alg : ListAlg A B) : (b : B) → Set where
  nil  :  ListSpec A alg (proj₁ alg)
  cons : (a : A) {b : B} (as : ListSpec A alg b) → ListSpec A alg (proj₂ alg a b)

Ok, importemos algunas bibliotecas y veamos un par de ejemplos ahora:

open import Data.Product
open import Data.Nat
open import Data.List

El álgebra que calcula la longitud de una lista viene dada por 0 como el caso base y es una manera const suc de combinar una A y la longitud de la cola para construir la longitud de la lista actual. Por lo tanto:

AlgLength : {A : Set} → ListAlg A ℕ
AlgLength = 0 , (λ _ → suc)

Si los elementos son números naturales, entonces se pueden sumar. El álgebra correspondiente a eso tiene 0 como el caso base y _+_ como la forma de combinar un ℕ junto con la suma de los elementos contenidos en la cola. Por lo tanto:

AlgSum : ListAlg ℕ ℕ
AlgSum = 0 , _+_

Pensamiento loco: si tenemos dos álgebras trabajando en los mismos elementos, ¡podemos combinarlos! ¡De esta manera seguiremos 2 invariantes en lugar de uno!

Alg× : {A B C : Set} (algB : ListAlg A B) (algC : ListAlg A C) →
       ListAlg A (B × C)
Alg× (b , sucB) (c , sucC) = (b , c) , (λ a → λ { (b , c) → sucB a b , sucC a c })

Y ahora los ejemplos:

Si estamos siguiendo la longitud, entonces podemos definir vectores:

Vec : (A : Set) (n : ℕ) → Set
Vec A n = ListSpec A AlgLength n

Y tener, por ejemplo, este vector de longitud 4:

allFin4 : Vec ℕ 4
allFin4 = cons 0 (cons 1 (cons 2 (cons 3 nil)))

Si estamos rastreando la suma de los elementos, entonces podemos definir una noción de distribución: una distribución estadística es una lista de probabilidades cuya suma es 100:

Distribution : Set
Distribution = ListSpec ℕ AlgSum 100

Y podemos definir uno uniforme por ejemplo:

uniform : Distribution
uniform = cons 25 (cons 25 (cons 25 (cons 25 nil)))

Finalmente, combinando la longitud y la suma de álgebras, podemos implementar la noción de distribución de tamaño.

SizedDistribution : ℕ → Set
SizedDistribution n = ListSpec ℕ (Alg× AlgLength AlgSum) (n , 100)

Y dale a esta bonita distribución uniforme un conjunto de 4 elementos:

uniform4 : SizedDistribution 4
uniform4 = cons 25 (cons 25 (cons 25 (cons 25 nil)))