Declarando instancias de sinónimos de tipo parametrizado

Question

Tengo un conjunto de funciones que funcionan en vectores, es decir listas con longitudes de tipo obligatorio.

que estoy tratando de hacer mis tipos más fáciles de escribir, es decir, en lugar de escribir

foo :: (Fold Integer v, Map Integer Integer v v, ...) => ... 

Estoy declarando una nueva clase NList así que sólo puedo escribir foo :: NList v Integer => ...

El (simplificado) Clase se parece a esto:

class (Fold (v i) i 
     , Map i i (v i) (v i) 
     , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) => NList v i 

como se puede ver, tengo que mantener el tipo "vector" separado del tipo "punto" (es decir v separado de i) para que pueda hacer cosas como Map en un vector Maybe.

Como tal, debe tener v tipo * -> *, y i tipo *.

Sin embargo, cuando intento crear una instancia con vectores de esta manera:

instance NList Vec2 Integer 
instance NList Vec3 Integer 
... 

me sale el siguiente error:

Type synonym `Vec2' should have 1 argument, but has been given none 
In the instance declaration for `NList Vec2 Integer' 

Ahora, soy muy nuevo para escribir a nivel de programación, y entiendo que probablemente estoy haciendo esto de una manera muy atrasada. ¿Es posible instanciar un sinónimo de tipo como este? ¿Algún tipo de asistentes tiene sugerencias para mejores formas de lograr mis objetivos?

Answer 1

El problema aquí es que Vec2 y Vec3 se declaran presumiblemente como algo parecido a esto:

type Vec2 a = Vec (S (S Z)) a 
type Vec3 a = Vec (S (S (S Z))) a 

Sinónimos de tipo no pueden ser parcialmente aplicadas, por diversas razones arcanas (que conducirían a lambdas de nivel tipo, que arruinar el caos con todo tipo de cosas relacionadas con la resolución e inferencia de instancias - imagina si pudieras definir type Id a = a y convertirlo en una instancia de Monad).

Es decir, no se puede hacer Vec2 una instancia de nada, porque no se puede utilizar Vec2 como si fuera un constructor de tipo nido totalmente con el tipo * -> *; de hecho es una "macro" de nivel de tipo que solo se puede aplicar completamente.

Sin embargo, usted puede definir sinónimos de tipos como aplicaciones parciales a sí mismos:

type Vec2 = Vec (S (S Z)) 
type Vec3 = Vec (S (S (S Z))) 

Estos son equivalentes, excepto que se permitirá a las instancias.

Si el tipo de Vec3 en realidad parece

type Vec3 a = Cons a (Cons a (Cons a Nil))) 

o similar, entonces estás de suerte; Tendrá que usar un contenedor newtype si desea dar alguna instancia.(Por otra parte, debe ser capaz de evitar la definición de casos directamente en este tipo enteramente dando casos de Nil y Cons lugar, lo que permite utilizar Vec3 como un ejemplo.)

Tenga en cuenta que con GHC de nuevo 7,4 constraint kinds, se puede evitar un tipo separado por completo, y definir simplemente un sinónimo restricción:

type NList v i = 
    (Fold (v i) i 
    , Map i i (v i) (v i) 
    , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) 

en cuanto a su enfoque, en general, se va, se debe, básicamente, funciona bien; la misma idea general es utilizada por el paquete . La gran cantidad de clases y grandes contextos puede hacer que los mensajes de error sean muy confusos y ralentizar la compilación, pero tal es la naturaleza de los hackers a nivel de tipo. Sin embargo, si usted tiene una base Vec tipo definido como el GADT habitual:

data Vec n a where 
    Nil :: Vec Z a 
    Succ :: a -> Vec n a -> Vec (S n) a 

entonces en realidad no necesita ninguna clases de tipos en absoluto. Si se define de alguna otra manera, pero todavía está parametrizado en un nivel de tipo natural, entonces se puede reemplazar todas las clases con una:

data Proxy s = Proxy 

class Nat n where 
    natElim 
     :: ((n ~ Z) => r) 
     -> (forall m. (n ~ S m, Nat m) => Proxy m -> r) 
     -> Proxy n 
     -> r 

Esto debería permitir a eliminar los contextos por completo, pero hace que la definición de las operaciones en los vectores un poco más complicado.