É possível "transformar dimensão em um tipo" em haskell?

Suponha que eu queira escrever uma biblioteca que lide com vetores e matrizes. É possível agrupar as dimensões nos tipos, para que operações de dimensões incompatíveis gerem um erro no tempo de compilação?

Por exemplo, eu gostaria que a assinatura do produto escalar fosse algo como

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

onde o dtipo contém um único valor inteiro (representando a dimensão desses vetores).

Suponho que isso possa ser feito definindo (manualmente) um tipo separado para cada número inteiro e agrupando-os em uma classe de tipo chamada VecDim. Existe algum mecanismo para "gerar" esses tipos?

Ou talvez alguma maneira melhor / mais simples de conseguir a mesma coisa?

Para expandir a resposta de @ KarlBielefeldt, aqui está um exemplo completo de como implementar Vectors - listas com um número estaticamente conhecido de elementos - em Haskell. Segure seu chapéu ...

{-# 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 você pode ver na longa lista de LANGUAGEdiretivas, isso funcionará apenas com uma versão recente do GHC.

Precisamos de uma maneira de representar comprimentos dentro do sistema de tipos. Por definição, um número natural é zero ( Z) ou é o sucessor de outro número natural ( S n). Então, por exemplo, o número 3 seria escrito S (S (S Z)).

data Nat = Z | S Nat

Com a extensão DataKinds , esta datadeclaração apresenta um tipo chamado Nate dois construtores de tipo chamados Se Z- em outras palavras, temos números naturais no nível de tipo . Observe que os tipos Se Znão têm nenhum valor de membro - apenas tipos do tipo *são habitados por valores.

Agora, apresentamos um GADT representando vetores com um comprimento conhecido. Observe a assinatura de tipo: Vecrequer um tipo de tipoNat (ou seja, um Zou um Stipo) para representar seu comprimento.

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)

A definição de vetores é semelhante à de listas vinculadas, com algumas informações extras no nível de tipo sobre seu comprimento. Um vetor é ou VNil, nesse caso, tem um comprimento de Z(ero), ou é uma VConscélula que adiciona um item a outro vetor; nesse caso, seu comprimento é um a mais que o outro vetor ( S n). Note-se que não há nenhum argumento do construtor do tipo n. É usado apenas no momento da compilação para rastrear comprimentos e será apagado antes que o compilador gere o código da máquina.

Definimos um tipo de vetor que carrega conhecimento estático de seu comprimento. Vamos consultar o tipo de alguns Vecs para ter uma ideia de como eles funcionam:

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

O produto escalar continua da mesma maneira que faria para uma 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 um vetor de funções a um vetor de argumentos, é Veco aplicativo <*>; Eu não o coloquei em uma Applicativeinstância porque fica confuso . Observe também que estou usando o foldrda instância gerada pelo compilador de Foldable.

Vamos tentar:

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

Ótimo! Você recebe um erro em tempo de compilação ao tentar dotvetores cujos comprimentos não coincidem.

Aqui está uma tentativa de uma função para concatenar vetores 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)

O comprimento do vetor de saída seria a soma dos comprimentos dos dois vetores de entrada. Precisamos ensinar ao verificador de tipos como adicionar Nats juntos. Para isso, usamos uma função de nível de tipo :

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

Esta type familydeclaração introduz uma função nos tipos chamados :+:- em outras palavras, é uma receita para o verificador de tipos calcular a soma de dois números naturais. É definido recursivamente - sempre que o operando esquerdo for maior que Zero, adicionamos um à saída e o reduzimos em um na chamada recursiva. (É um bom exercício escrever uma função de tipo que multiplica dois Nats.) Agora podemos fazer a +++compilação:

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

Veja como você o usa:

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

Até agora, tão simples. E quando queremos fazer o oposto da concatenação e dividir um vetor em dois? Os comprimentos dos vetores de saída dependem do valor de tempo de execução dos argumentos. Gostaríamos de escrever algo como isto:

-- 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)

mas infelizmente Haskell não nos deixa fazer isso. Permitir que o valor do nargumento apareça no tipo de retorno (geralmente chamado de função dependente ou tipo pi ) exigiria tipos dependentes de "espectro completo", enquanto DataKindsapenas nos fornece construtores de tipo promovidos. Em outras palavras, os construtores de tipo Se Znão aparecem no nível do valor. Teremos que aceitar valores singleton para uma representação em tempo de execução de um 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 um determinado tipo n(com tipo Nat), há precisamente um termo do tipo Natty n. Podemos usar o valor singleton como uma testemunha em tempo de execução para n: aprender sobre a Nattynos ensina sobre isso ne vice-versa.

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 dar uma volta:

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)

No primeiro exemplo, dividimos com êxito um vetor de três elementos na posição 2; obtivemos um erro de tipo quando tentamos dividir um vetor em uma posição após o final. Singletons são a técnica padrão para fazer um tipo depender de um valor em Haskell.

_{* A singletonsbiblioteca contém alguns auxiliares do Template Haskell para gerar valores singleton como Nattypara você.}

Último exemplo. E quando você não conhece estaticamente a dimensionalidade do seu vetor? Por exemplo, e se estivermos tentando criar um vetor a partir de dados de tempo de execução na forma de uma lista? Você precisa do tipo do vetor para depender do comprimento da lista de entrada. Em outras palavras, não podemos usar foldr VCons VNilpara construir um vetor porque o tipo do vetor de saída muda a cada iteração da dobra. Precisamos manter o comprimento do vetor em segredo do 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

AVecé um tipo existencial : a variável type nnão aparece no tipo de retorno do AVecconstrutor de dados. Estamos usando-o para simular um par dependente : fromListnão podemos dizer estaticamente o comprimento do vetor, mas ele pode retornar algo com o qual você pode fazer a correspondência de padrões para aprender o comprimento do vetor - Natty nno primeiro elemento da tupla . Como Conor McBride coloca em uma resposta relacionada , "Você olha para uma coisa e, ao fazê-lo, aprende sobre outra".

Essa é uma técnica comum para tipos existencialmente quantificados. Como você não pode realmente fazer nada com dados para os quais você não conhece o tipo - tente escrever uma função de data Something = forall a. Sth a- existenciais geralmente são agrupados com evidências do GADT, que permitem recuperar o tipo original executando testes de correspondência de padrões. Outros padrões comuns para existenciais incluem empacotar funções para processar seu tipo ( data AWayToGetTo b = forall a. HeresHow a (a -> b)), que é uma maneira elegante de executar módulos de primeira classe ou criar um dicionário de classe de tipo ( data AnOrd = forall a. Ord a => AnOrd a) que pode ajudar a emular o polimorfismo de subtipo.

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

Pares dependentes são úteis sempre que as propriedades estáticas dos dados dependem de informações dinâmicas não disponíveis no momento da compilação. Aqui está filterpara vetores:

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 dotdois AVecs, precisamos provar ao GHC que seus comprimentos são iguais. Data.Type.Equalitydefine um GADT que só pode ser construído quando seus argumentos de tipo são os mesmos:

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

Quando você combina com padrões Refl, o GHC sabe disso a ~ b. Existem também algumas funções para ajudá-lo a trabalhar com esse tipo: usaremos gcastWithpara converter entre tipos equivalentes e TestEqualitydeterminar se dois Nattys são iguais.

Para testar a igualdade de dois Nattys, precisaremos fazer uso do fato de que, se dois números forem iguais, seus sucessores também serão iguais ( :~:é congruente ao longo S):

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

A correspondência de padrões no Refllado esquerdo permite que o GHC saiba disso n ~ m. Com esse conhecimento, é trivial que S n ~ S m, portanto, o GHC nos permita devolver um novo Reflimediatamente.

Agora podemos escrever uma instância de TestEqualitypor recursão direta. Se ambos os números são zero, eles são iguais. Se ambos os números tiverem predecessores, eles serão iguais se os predecessores forem iguais. (Se não forem iguais, basta retornar 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

Agora podemos juntar as peças em dotum par de AVecs de comprimento desconhecido.

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)

Primeiro, a correspondência de padrões no AVecconstrutor para obter uma representação em tempo de execução dos comprimentos dos vetores. Agora use testEqualitypara determinar se esses comprimentos são iguais. Se forem, teremos Just Refl; gcastWithusará essa prova de igualdade para garantir que dot u vseja bem digitada, descarregando sua n ~ msuposição 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

Observe que, como um vetor sem conhecimento estático de seu comprimento é basicamente uma lista, reimplementamos efetivamente a versão da lista dot :: Num a => [a] -> [a] -> Maybe a. A diferença é que esta versão é implementada em termos dos vetores dot. Aqui está o ponto: antes que o verificador de tipos permita que você ligue dot, você deve ter testado se as listas de entrada têm o mesmo tamanho usando testEquality. Estou propenso a obter ifinstruções erradas, mas não em um ambiente de tipo dependente!

Não é possível evitar o uso de wrappers existenciais nas bordas do seu sistema, quando você está lidando com dados de tempo de execução, mas pode usar tipos dependentes em qualquer lugar dentro do sistema e manter os wrappers existenciais nas bordas ao executar a validação de entrada.

Como Nothingnão é muito informativo, você pode refinar ainda mais o tipo de dot'para retornar uma prova de que os comprimentos não são iguais (na forma de evidência de que sua diferença não é 0) no caso de falha. Isso é bastante semelhante à técnica padrão de Haskell de usar Either String apara possivelmente retornar uma mensagem de erro, embora um termo de prova seja muito mais útil em termos computacionais do que uma string!

Assim, termina esse tour de algumas das técnicas comuns na programação Haskell de tipo dependente. Programar com tipos como este em Haskell é muito legal, mas muito estranho ao mesmo tempo. Dividir todos os seus dados dependentes em várias representações que significam a mesma coisa - Nato tipo, Nato tipo, Natty no singleton - é realmente bastante complicado, apesar da existência de geradores de código para ajudar no clichê. Atualmente, também existem limitações sobre o que pode ser promovido para o nível de tipo. É tentador embora! A mente desconfia das possibilidades - na literatura há exemplos em Haskell de printfinterfaces de banco de dados fortemente tipadas , mecanismos de layout de interface do usuário ...

Se você quiser ler mais, há um crescente corpo de literatura sobre Haskell de tipo dependente, publicado e em sites como o Stack Overflow. Um bom ponto de partida é o artigo do Hasochism - o artigo passa por esse exemplo (entre outros), discutindo as partes dolorosas com mais detalhes. O artigo de Singletons demonstra a técnica de valores singleton (como Natty). Para obter mais informações sobre digitação dependente em geral, o tutorial do Agda é um bom ponto de partida; Além disso, Idris é uma linguagem em desenvolvimento projetada (aproximadamente) para ser "Haskell com tipos dependentes".

Isso é chamado de digitação dependente . Depois de saber o nome, você poderá encontrar mais informações sobre o que você poderia desejar. Há também uma linguagem interessante, semelhante a haskell, chamada Idris, que as usa nativamente. Seu autor fez algumas apresentações realmente boas sobre o tópico que você pode encontrar no youtube.