¿Es posible "hornear la dimensión en un tipo" en Haskell?

Supongamos que quiero escribir una biblioteca que se ocupe de vectores y matrices. ¿Es posible hornear las dimensiones en los tipos, de modo que las operaciones de dimensiones incompatibles generen un error en el momento de la compilación?

Por ejemplo, me gustaría que la firma del producto dot sea algo así como

dotprod :: Num a, VecDim d => Vector a d -> Vector a d -> a

donde el dtipo contiene un único valor entero (que representa la dimensión de estos vectores).

Supongo que esto podría hacerse definiendo (a mano) un tipo separado para cada número entero y agrupándolos en una clase de tipo llamada VecDim. ¿Existe algún mecanismo para "generar" tales tipos?

¿O quizás alguna forma mejor / más simple de lograr lo mismo?

Para ampliar la respuesta de @ KarlBielefeldt, aquí hay un ejemplo completo de cómo implementar Vectores (listas con un número de elementos estáticamente conocido) en Haskell. Agárrate a tu sombrero ...

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

import Prelude hiding (foldr, zipWith)
import qualified Prelude
import Data.Type.Equality
import Data.Foldable
import Data.Traversable

Como puede ver en la larga lista de LANGUAGEdirectivas, esto solo funcionará con una versión reciente de GHC.

Necesitamos una forma de representar longitudes dentro del sistema de tipos. Por definición, un número natural es cero ( Z) o es el sucesor de algún otro número natural ( S n). Entonces, por ejemplo, se escribiría el número 3 S (S (S Z)).

data Nat = Z | S Nat

Con la extensión DataKinds , esta datadeclaración introduce un tipo llamado Naty dos constructores de tipo llamados Sy Z, en otras palabras, tenemos números naturales de nivel de tipo . Tenga en cuenta que los tipos Sy Zno tienen ningún valor de miembro: solo los tipos de tipo *están habitados por valores.

Ahora presentamos un GADT que representa vectores con una longitud conocida. Tenga en cuenta la firma de tipo: Vecrequiere un tipo de tipoNat (es decir, un Zo un Stipo) para representar su longitud.

data Vec :: Nat -> * -> * where
    VNil :: Vec Z a
    VCons :: a -> Vec n a -> Vec (S n) a
deriving instance (Show a) => Show (Vec n a)
deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)
deriving instance Traversable (Vec n)

La definición de vectores es similar a la de las listas vinculadas, con información adicional a nivel de tipo sobre su longitud. Un vector es VNil, en cuyo caso tiene una longitud de Z(ero), o es una VConscelda que agrega un elemento a otro vector, en cuyo caso su longitud es uno más que el otro vector ( S n). Tenga en cuenta que no hay argumento constructor de tipo n. Solo se usa en tiempo de compilación para rastrear longitudes, y se borrará antes de que el compilador genere código de máquina.

Hemos definido un tipo de vector que conlleva un conocimiento estático de su longitud. Vamos a consultar el tipo de unos pocos Vecs para tener una idea de cómo funcionan:

ghci> :t (VCons 'a' (VCons 'b' VNil))
(VCons 'a' (VCons 'b' VNil)) :: Vec ('S ('S 'Z)) Char  -- (S (S Z)) means 2
ghci> :t (VCons 13 (VCons 11 (VCons 3 VNil)))
(VCons 13 (VCons 11 (VCons 3 VNil))) :: Num a => Vec ('S ('S ('S 'Z))) a  -- (S (S (S Z))) means 3

El producto punto continúa como lo haría para una lista:

-- note that the two Vec arguments are declared to have the same length
vap :: Vec n (a -> b) -> Vec n a -> Vec n b
vap VNil VNil = VNil
vap (VCons f fs) (VCons x xs) = VCons (f x) (vap fs xs)

zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith f xs ys = fmap f xs `vap` ys

dot :: Num a => Vec n a -> Vec n a -> a
dot xs ys = foldr (+) 0 $ zipWith (*) xs ys

vap, que 'zippily' aplica un vector de funciones a un vector de argumentos, es Vecaplicativo <*>; No lo puse en una Applicativeinstancia porque se vuelve desordenado . Tenga en cuenta también que estoy usando la foldrinstancia generada por el compilador de Foldable.

Probémoslo:

ghci> let v1 = VCons 2 (VCons 1 VNil)
ghci> let v2 = VCons 4 (VCons 5 VNil)
ghci> v1 `dot` v2
13
ghci> let v3 = VCons 8 (VCons 6 (VCons 1 VNil))
ghci> v1 `dot` v3
<interactive>:20:10:
    Couldn't match type ‘'S 'Z’ with ‘'Z’
    Expected type: Vec ('S ('S 'Z)) a
      Actual type: Vec ('S ('S ('S 'Z))) a
    In the second argument of ‘dot’, namely ‘v3’
    In the expression: v1 `dot` v3

¡Excelente! Obtiene un error en tiempo de compilación cuando intenta dotvectores cuyas longitudes no coinciden.

Aquí hay un intento de una función para concatenar vectores juntos:

-- This won't compile because the type checker can't deduce the length of the returned vector
-- VNil +++ ys = ys
-- (VCons x xs) +++ ys = VCons x (concat xs ys)

La longitud del vector de salida sería la suma de las longitudes de los dos vectores de entrada. Necesitamos enseñarle al verificador de tipos cómo sumar Nats. Para esto usamos una función de nivel de tipo :

type family (n :: Nat) :+: (m :: Nat) :: Nat where
    Z :+: m = m
    (S n) :+: m = S (n :+: m)

Esta type familydeclaración introduce una función en los tipos llamados :+:; en otras palabras, es una receta para que el verificador de tipos calcule la suma de dos números naturales. Se define de forma recursiva: cuando el operando izquierdo es mayor que Zero, agregamos uno a la salida y lo reducimos en uno en la llamada recursiva. (Es un buen ejercicio escribir una función de tipo que multiplique dos Nats.) Ahora podemos +++compilar:

infixr 5 +++
(+++) :: Vec n a -> Vec m a -> Vec (n :+: m) a
VNil +++ ys = ys
(VCons x xs) +++ ys = VCons x (concat xs ys)

Así es como lo usa:

ghci> VCons 1 (VCons 2 VNil) +++ VCons 3 (VCons 4 VNil)
VCons 1 (VCons 2 (VCons 3 (VCons 4 VNil)))

Hasta ahora muy simple. ¿Qué pasa cuando queremos hacer lo opuesto a la concatenación y dividir un vector en dos? Las longitudes de los vectores de salida dependen del valor de tiempo de ejecución de los argumentos. Nos gustaría escribir algo como esto:

-- this won't work because there aren't any values of type `S` and `Z`
-- split :: (n :: Nat) -> Vec (n :+: m) a -> (Vec n a, Vec m a)

pero desafortunadamente Haskell no nos deja hacer eso. Permitir que el valor del nargumento aparezca en el tipo de retorno (esto comúnmente se llama una función dependiente o tipo pi ) requeriría tipos dependientes de "espectro completo", mientras que DataKindssolo nos da constructores de tipos promocionados. Para decirlo de otra manera, los constructores de tipos Sy Zno aparecen en el nivel de valor. Tendremos que conformarnos con valores únicos para una representación en tiempo de ejecución de un determinado Nat. *

data Natty (n :: Nat) where
    Zy :: Natty Z  -- pronounced 'zed-y'
    Sy :: Natty n -> Natty (S n)  -- pronounced 'ess-y'
deriving instance Show (Natty n)

Para un tipo dado n(con tipo Nat), hay precisamente un término de tipo Natty n. Podemos usar el valor singleton como testigo de tiempo de ejecución para n: aprender sobre un Nattynos enseña sobre él ny viceversa.

split :: Natty n ->
         Vec (n :+: m) a ->  -- the input Vec has to be at least as long as the input Natty
         (Vec n a, Vec m a)
split Zy xs = (Nil, xs)
split (Sy n) (Cons x xs) = let (ys, zs) = split n xs
                           in (Cons x ys, zs)

Vamos a darle una vuelta:

ghci> split (Sy (Sy Zy)) (VCons 1 (VCons 2 (VCons 3 VNil)))
(VCons 1 (VCons 2 VNil), VCons 3 VNil)
ghci> split (Sy (Sy Zy)) (VCons 3 VNil)
<interactive>:116:21:
    Couldn't match type ‘'S ('Z :+: m)’ with ‘'Z’
    Expected type: Vec ('S ('S 'Z) :+: m) a
      Actual type: Vec ('S 'Z) a
    Relevant bindings include
      it :: (Vec ('S ('S 'Z)) a, Vec m a) (bound at <interactive>:116:1)
    In the second argument of ‘split’, namely ‘(VCons 3 VNil)’
    In the expression: split (Sy (Sy Zy)) (VCons 3 VNil)

En el primer ejemplo, dividimos con éxito un vector de tres elementos en la posición 2; entonces obtuvimos un error de tipo cuando intentamos dividir un vector en una posición más allá del final. Los singletons son la técnica estándar para hacer que un tipo dependa de un valor en Haskell.

_{* La singletonsbiblioteca contiene algunos ayudantes de Template Haskell para generar valores únicos como Nattypara usted.}

Ultimo ejemplo ¿Qué pasa cuando no conoces la dimensionalidad de tu vector estáticamente? Por ejemplo, ¿qué pasa si estamos tratando de construir un vector a partir de datos de tiempo de ejecución en forma de una lista? Necesita que el tipo de vector dependa de la longitud de la lista de entrada. En otras palabras, no podemos usar foldr VCons VNilpara construir un vector porque el tipo del vector de salida cambia con cada iteración del pliegue. Necesitamos mantener la longitud del vector en secreto del compilador.

data AVec a = forall n. AVec (Natty n) (Vec n a)
deriving instance (Show a) => Show (AVec a)

fromList :: [a] -> AVec a
fromList = Prelude.foldr cons nil
    where cons x (AVec n xs) = AVec (Sy n) (VCons x xs)
          nil = AVec Zy VNil

AVeces un tipo existencial : la variable de tipo nno aparece en el tipo de retorno del AVecconstructor de datos. Lo estamos utilizando para simular un par dependiente : fromListno podemos decirle la longitud del vector estáticamente, pero puede devolver algo con lo que puede hacer coincidir un patrón para conocer la longitud del vector, Natty nel primer elemento de la tupla . Como dice Conor McBride en una respuesta relacionada , "Miras una cosa y, al hacerlo, aprendes sobre otra".

Esta es una técnica común para tipos cuantificados existencialmente. Debido a que en realidad no puede hacer nada con datos para los que no conoce el tipo, intente escribir una función de data Something = forall a. Sth a, los existenciales a menudo vienen agrupados con evidencia GADT que le permite recuperar el tipo original realizando pruebas de coincidencia de patrones. Otros patrones comunes para los existenciales incluyen funciones de empaquetamiento para procesar su tipo ( data AWayToGetTo b = forall a. HeresHow a (a -> b)), que es una forma ordenada de hacer módulos de primera clase, o incorporar un diccionario de clase de tipo ( data AnOrd = forall a. Ord a => AnOrd a) que puede ayudar a emular el polimorfismo de subtipo.

ghci> fromList [1,2,3]
AVec (Sy (Sy (Sy Zy))) (VCons 1 (VCons 2 (VCons 3 Nil)))

Los pares dependientes son útiles siempre que las propiedades estáticas de los datos dependan de información dinámica no disponible en el momento de la compilación. Aquí está filterpara los vectores:

filter :: (a -> Bool) -> Vec n a -> AVec a
filter f = foldr (\x (AVec n xs) -> if f x
                                    then AVec (Sy n) (VCons x xs)
                                    else AVec n xs) (AVec Zy VNil) 

A dotdos AVecs, tenemos que demostrarle a GHC que sus longitudes son iguales. Data.Type.Equalitydefine un GADT que solo se puede construir cuando sus argumentos de tipo son los mismos:

data (a :: k) :~: (b :: k) where
    Refl :: a :~: a  -- short for 'reflexivity'

Cuando el patrón coincide Refl, GHC lo sabe a ~ b. También hay algunas funciones para ayudarlo a trabajar con este tipo: usaremos gcastWithpara convertir entre tipos equivalentes y TestEqualitypara determinar si dos Nattys son iguales.

Para probar la igualdad de dos Nattys, necesitaremos hacer uso del hecho de que si dos números son iguales, entonces sus sucesores también son iguales ( :~:es congruente con S):

congSuc :: (n :~: m) -> (S n :~: S m)
congSuc Refl = Refl

La coincidencia de patrones en Reflel lado izquierdo le permite a GHC saber eso n ~ m. Con ese conocimiento, es trivial eso S n ~ S m, por lo que GHC nos permite devolver uno nuevo de Reflinmediato.

Ahora podemos escribir una instancia de TestEqualitypor recursión directa. Si ambos números son cero, son iguales. Si ambos números tienen predecesores, son iguales si los predecesores son iguales. (Si no son iguales, solo regrese Nothing).

instance TestEquality Natty where
    -- testEquality :: Natty n -> Natty m -> Maybe (n :~: m)
    testEquality Zy Zy = Just Refl
    testEquality (Sy n) (Sy m) = fmap congSuc (testEquality n m)  -- check whether the predecessors are equal, then make use of congruence
    testEquality Zy _ = Nothing
    testEquality _ Zy = Nothing

Ahora podemos juntar las piezas en dotun par de AVecs de longitud desconocida.

dot' :: Num a => AVec a -> AVec a -> Maybe a
dot' (AVec n u) (AVec m v) = fmap (\proof -> gcastWith proof (dot u v)) (testEquality n m)

Primero, coincidencia de patrón en el AVecconstructor para extraer una representación en tiempo de ejecución de las longitudes de los vectores. Ahora use testEqualitypara determinar si esas longitudes son iguales. Si lo son, lo haremos Just Refl; gcastWithutilizará esa prueba de igualdad para garantizar que dot u vesté bien tipada al descargar su n ~ msuposición implícita .

ghci> let v1 = fromList [1,2,3]
ghci> let v2 = fromList [4,5,6]
ghci> let v3 = fromList [7,8]
ghci> dot' v1 v2
Just 32
ghci> dot' v1 v3
Nothing  -- they weren't the same length

Tenga en cuenta que, dado que un vector sin conocimiento estático de su longitud es básicamente una lista, hemos implementado efectivamente la versión de la lista dot :: Num a => [a] -> [a] -> Maybe a. La diferencia es que esta versión se implementa en términos de los vectores ' dot. Este es el punto: antes de que el verificador de tipos le permita llamar dot, debe haber probado si las listas de entrada tienen la misma longitud testEquality. ¡Soy propenso a obtener ifdeclaraciones incorrectas, pero no en un entorno de tipo dependiente!

No puede evitar el uso de contenedores existenciales en los bordes de su sistema, cuando se trata de datos de tiempo de ejecución, pero puede usar tipos dependientes en todas partes dentro de su sistema y mantener los contenedores existenciales en los bordes, cuando realiza la validación de entrada.

Como Nothingno es muy informativo, puede refinar aún más el tipo de dot'para devolver una prueba de que las longitudes no son iguales (en forma de evidencia de que su diferencia no es 0) en el caso de falla. Esto es bastante similar a la técnica estándar de Haskell de usar Either String apara posiblemente devolver un mensaje de error, ¡aunque un término de prueba es mucho más útil computacionalmente que una cadena!

Así termina este recorrido de parada por silbido de algunas de las técnicas que son comunes en la programación de Haskell de tipo dependiente. La programación con tipos como este en Haskell es realmente genial, pero muy incómoda al mismo tiempo. Desglosar todos sus datos dependientes en muchas representaciones que significan lo mismo, Natel tipo, Natel tipo, Natty nel singleton, es realmente bastante engorroso, a pesar de la existencia de generadores de código para ayudar con la repetitiva. También hay actualmente limitaciones en lo que se puede promover al nivel de tipo. ¡Sin embargo, es tentador! La mente se aturde ante las posibilidades: en la literatura hay ejemplos en Haskell de printfinterfaces de bases de datos fuertemente tipadas , motores de diseño de interfaz de usuario ...

Si desea leer más, hay un creciente cuerpo de literatura sobre Haskell de tipo dependiente, tanto publicado como en sitios como Stack Overflow. Un buen punto de partida es el documento de Hasochism : el documento pasa por este mismo ejemplo (entre otros), discutiendo las partes dolorosas con cierto detalle. El artículo de Singletons demuestra la técnica de los valores de singleton (como Natty). Para obtener más información sobre la escritura dependiente en general, el tutorial de Agda es un buen lugar para comenzar; Además, Idris es un lenguaje en desarrollo que está diseñado (aproximadamente) para ser "Haskell con tipos dependientes".

Eso se llama mecanografía dependiente . Una vez que conozca el nombre, puede encontrar más información sobre el que nunca podría desear. También hay un interesante lenguaje tipo haskell llamado Idris que los usa de forma nativa. Su autor ha hecho algunas presentaciones realmente buenas sobre el tema que puede encontrar en youtube.