Instancias y restricciones definidas recursivamente

Question

He estado jugando con vectores y matrices donde el tamaño está codificado en su tipo, usando la nueva extensión DataKinds. Básicamente, es la siguiente:

data Nat = Zero | Succ Nat 

data Vector :: Nat -> * -> * where 
    VNil :: Vector Zero a 
    VCons :: a -> Vector n a -> Vector (Succ n) a 

Ahora queremos casos típicos como Functor y Applicative. Functor es fácil:

instance Functor (Vector n) where 
    fmap f VNil = VNil 
    fmap f (VCons a v) = VCons (f a) (fmap f v) 

Pero con la Applicative ejemplo, hay un problema: No sabemos qué tipo de volver en el más puro. Sin embargo, podemos definir la instancia inductivamente en el tamaño del vector:

instance Applicative (Vector Zero) where 
    pure = const VNil 
    VNil <*> VNil = VNil 

instance Applicative (Vector n) => Applicative (Vector (Succ n)) where 
    pure a = VCons a (pure a) 
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v) 

Sin embargo, a pesar de que este caso se aplica para todos los vectores, el tipo de corrector no sabe esto, así que tenemos que llevar a la restricción Applicative cada vez que usamos la instancia.

Ahora, si esto se aplica solo a la instancia Applicative, no sería un problema, pero resulta que el truco de las declaraciones de instancia recursivas es esencial cuando se programa con tipos como estos. Por ejemplo, si definimos una matriz como un vector de vectores fila utilizando la biblioteca TypeCompose,

type Matrix nx ny a = (Vector nx :. Vector ny) a 

tenemos que definir una clase de tipo y añadir declaraciones de instancias recursivas para implementar tanto la transpuesta y la multiplicación de matrices. Esto lleva a una gran proliferación de restricciones que tenemos que llevar cada vez que usamos el código, incluso aunque las instancias se apliquen a todos los vectores y matrices (haciendo que las restricciones sean inútiles).

¿Hay alguna manera de evitar tener que cumplir con todas estas limitaciones? ¿Sería posible extender el verificador de tipos para que pueda detectar tales construcciones inductivas?

Answer 1

De hecho, la definición de pure es el meollo del problema. ¿Cuál debería ser su tipo, completamente cuantificado y calificado?

pure :: forall (n :: Nat) (x :: *). x -> Vector n x   -- (X) 

no va a hacer, ya que no hay información disponible en tiempo de ejecución para determinar si debe emitir pureVNil o VCons. En consecuencia, tal como están las cosas, no puede simplemente tener

instance Applicative (Vector n)        -- (X) 

¿Qué puede hacer? Así, el trabajo con la Strathclyde Haskell Enhancement, en el archivo Vec.lhs ejemplo, defino un precursor de pure

vec :: forall x. pi (n :: Nat). x -> Vector {n} x 
vec {Zero} x = VNil 
vec {Succ n} x = VCons x (vec n x) 

con un tipo pi, lo que requiere que una copia de n puede pasar en tiempo de ejecución. Este pi (n :: Nat). desugars como

forall n. Natty n -> 

donde Natty, con un nombre más prosaico en la vida real, es el singleton GADT dadas por

data Natty n where 
    Zeroy :: Natty Zero 
    Succy :: Natty n -> Natty (Succ n) 

y las llaves en las ecuaciones para vec simplemente traducen Nat constructores para Natty constructores.Luego defino la siguiente instancia diabólica (desconectando la instancia predeterminada de Functor)

instance {:n :: Nat:} => Applicative (Vec {n}) where 
    hiding instance Functor 
    pure = vec {:n :: Nat:} where 
    (<*>) = vapp where 
    vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t 
    vapp VNil   VNil   = VNil 
    vapp (VCons f fs) (VCons s ss) = VCons (f s) vapp fs ss 

que requiere más tecnología, aún. La restricción {:n :: Nat:} desagua a algo que requiere que exista un testigo Natty n, y por el poder de las variables de tipo de ámbito, las mismas citaciones {:n :: Nat:} que son testigos explícitos. Escritura a mano, eso es

class HasNatty n where 
    natty :: Natty n 
instance HasNatty Zero where 
    natty = Zeroy 
instance HasNatty n => HasNatty (Succ n) where 
    natty = Succy natty 

y reemplazar la restricción {:n :: Nat:} con HasNatty n y el término correspondiente con (natty :: Natty n). Hacer esta construcción equivale sistemáticamente a escribir un fragmento de un tipocheck Haskell en la clase de tipo Prolog, que no es mi idea de alegría, así que uso una computadora.

Tenga en cuenta que la Traversable ejemplo (perdón por mis soportes modismo y mi silencio por defecto Functor y casos plegables) no requiere tales pokery jiggery

instance Traversable (Vector n) where 
    traverse f VNil   = (|VNil|) 
    traverse f (VCons x xs) = (|VCons (f x) (traverse f xs)|) 

Esa es toda la estructura que necesita para obtener la multiplicación de matrices sin recursividad más explícita.

TL; DR Utilice la construcción singleton y su clase de tipo asociada para contraer todas las instancias recursivamente definidas en la existencia de un testigo de tiempo de ejecución para los datos de nivel de tipo, desde el que puede calcular por recursión explícita.

¿Cuáles son las implicaciones de diseño?

GHC 7.4 tiene la tecnología de promoción tipo, pero SHE todavía tiene la construcción simple pi -types para ofrecer. Una cosa claramente importante acerca de los tipos de datos promocionados es que son cerrados, pero que en realidad aún no se muestra de manera clara: la constructabilidad de los testigos únicos es la manifestación de esa cerrazón. De alguna manera, si tiene forall (n :: Nat)., siempre es razonable exigir un singleton también, pero hacerlo marca una diferencia en el código generado: ya sea explícito como en mi construcción pi, o implícito como en el diccionario para {:n :: Nat:}, hay un extra información de tiempo de ejecución para dar vueltas, y un teorema libre correspondientemente más débil.

Una pregunta de diseño abierto para versiones futuras de GHC es cómo administrar esta distinción entre la presencia y ausencia de testigos de tiempo de ejecución para los datos de nivel de tipo. Por un lado, los necesitamos en restricciones. Por otro lado, necesitamos hacer coincidir patrones en ellos. Por ejemplo, debería significar la pi (n :: Nat). explícita

forall (n :: Nat). Natty n -> 

o implícita

forall (n :: Nat). {:n :: Nat:} => 

? Por supuesto, los lenguajes como Agda y Coq tienen ambas formas, así que tal vez Haskell debería hacer lo mismo. ¡Sin duda hay espacio para avanzar, y estamos trabajando en ello!