Tipos de Dados Algébricos Generalizados

1 GADTs

Para resolver alguns dos problemas levantados nos tópicos anteriores, precisamos de uma forma mais flexível para definir novos tipos. Antes de entender a nova sintaxe, vamos revisar alguns dos tipos definidos anteriormente:

data Maybe a    = Nothing | Just a
data Either a b = Left a | Right b
data User a     = User String (Int -> IO Int)

data Expr a = IConst Int
	    | BConst Bool
	    | Add (Expr a) (Expr a)
	    | Mul (Expr a) (Expr a)
	    | And (Expr a) (Expr a)
	    | Or  (Expr a) (Expr a)

Os nomes que precedem os valores são chamados de construtores de dados (data constructors) e eles se comportam de forma similar a funções. De fato, se verificarmos o tipo desses contrutores no ghci temos:

> :t Nothing
Nothing :: Maybe a

> :t Just
Just :: a -> Maybe a

> :t Left
Left :: a -> Either a b

> :t Right
Right :: b -> Either a b

> :t User
User :: String -> (Int -> IO Int) -> User a

> :t Add
Add :: Expr a -> Expr a -> Expr a

Os GADTs permitem criar novos construtores de valores seguindo a sintaxe de assinatura de funções. Em primeiro momento isso não parece acrescentar nada à criação de novos tipos. Porém, veremos que eles permitem adicionar restrições extras na definição dos tipos.

Por exemplo, o tipo Maybe é definido da seguinte forma utilizando a sintaxe GADT:

{-# LANGUAGE GADTs #-}
data Maybe a where
  Nothing :: Maybe a
  Just    :: a -> Maybe a

Para entender as possibilidades dessa sintaxe, vamos criar um tipo lista que possui um parâmetro de tipo extra indicando se ela contém algum elemento ou está vazia. Na forma tradicional faríamos:

data Empty
data NonEmpty

data SafeList a b = Nil | Cons a (SafeList a b)

Só que não existe nada que garanta que um elemento Nil será do tipo SafeList a Empty. Ou seja, nada além da boa vontade do programador impede algo assim de ser escrito e usado:

listaVazia :: SafeList a NonEmpty
listaVazia = Nil

Por outro lado, podemos deixar isso explícito e restringir tal sandice usando GADTs:

{-# LANGUAGE GADTs #-}
data Empty
data NonEmpty

data SafeList a b where
  Nil  :: SafeList a Empty
  Cons :: a -> SafeList a b -> SafeList a NonEmpty

A definição de SafeList possui dois construtores, o primeiro não recebe nenhum valor e explicitamente devolve uma SafeList cujo segundo parâmetro de tipo é Empty. O segundo construtor recebe um valor do tipo a, uma SafeList, vazia ou não, e retorna uma lista marcada com NonEmpty.

Não existe uma forma de criar uma lista não-vazia com Nil, ou criar uma lista contendo algum elemento marcada como Empty.

Com isso, podemos implementar uma versão de head que é total e segura:

safeHead :: SafeList a NonEmpty -> a
safeHead (Cons x _) = x

Note que a implementação requer (e permite) apenas o pattern matching para Cons. Se tentarmos implementar o caso Nil, o compilador não vai deixar, pois Nil sempre será uma lista marcada com Empty.

Se tentarmos utilizar essa função em uma lista vazia, o compilador vai emitir uma mensagem de erro:

> safeHead (Cons "hi" Nil)
"hi"
> safeHead Nil

<interactive>:1:9:
    Couldn't match `NonEmpty' against `Empty'
      Expected type: SafeList a NonEmpty
      Inferred type: SafeList a Empty
    In the first argument of `safeHead', namely `Nil'
    In the definition of `it': it = safeHead Nil

Agora você pode dormir tranquilo pois terá certeza que seu programa não tentará pegar um elemento de uma lista vazia.

Esse tipo de definição, porém, pode trazer dificuldades adicionais na criação de funções. Considere essa função exemplo¹:

silly False = Nil
silly True  = Cons () Nil

Ela não compila, embora a implementação pareça correta! O erro de compilação é:

Couldn't match `Empty' against `NonEmpty'
   Expected type: SafeList () Empty
   Inferred type: SafeList () NonEmpty
 In the application `Cons () Nil'
 In the definition of `silly': silly True = Cons () Nil

O compilador utiliza o primeiro caso do pattern matching para definir a assinatura da função, e ele decidiu que o retorno deve ser uma lista vazia, porém o segundo caso retorna uma lista não-vazia (compare o tipo declarado de Nil com o tipo de Cons).

Uma das formas de contornar isso é utilizando Either ou construindo estruturas adicionais:

silly :: Bool -> Either (SafeList () Empty) (SafeList () NonEmpty)
silly False = Left Nil
silly True  = Right $ Cons () Nil

1.1 Árvore de Expressão

Vamos retomar nossa estrutura representando uma árvore de expressão. Agora é possível explicitarmos quais construtores definem uma expressão do tipo Int e quais do tipo Bool:

data Expr a where
  I   :: Int  -> Expr Int
  B   :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  And :: Expr Bool -> Expr Bool -> Expr Bool
  Or  :: Expr Bool -> Expr Bool -> Expr Bool

Agora é possível implementar uma única função de avaliação que pode devolver tanto um inteiro como um booleano:

evalExpr :: Expr a -> a
evalExpr (I x)      = x
evalExpr (B b)      = b
evalExpr (Add l r)  = evalExpr l + evalExpr r
evalExpr (Mul l r)  = evalExpr l * evalExpr r
evalExpr (And l r)  = evalExpr l && evalExpr r
evalExpr (Or l r)   = evalExpr l || evalExpr r

Ao contrário do que aconteceu com o tipo SafeList na função silly, aqui o tipo de saída está bem especificado. Se eu passo como entrada um Expr Int, eu vou receber um Int (repare na assinatura: Expr a -> a).

Com isso, podemos expandir ainda mais nossa estrutura incluindo operações que recebem tipos misturados:

data Expr a where
  I    :: Int  -> Expr Int
  B    :: Bool -> Expr Bool
  Add  :: Expr Int -> Expr Int -> Expr Int
  Mul  :: Expr Int -> Expr Int -> Expr Int
  And  :: Expr Bool -> Expr Bool -> Expr Bool
  Or   :: Expr Bool -> Expr Bool -> Expr Bool
  If   :: Expr Bool -> Expr a -> Expr a -> Expr a
  Eq   :: Expr Int -> Expr Int -> Expr Bool
  Even :: Expr Int -> Expr Bool
  Odd  :: Expr Int ->  Expr Bool
  Half :: Expr Int -> Expr Int

Veja que agora temos alguns construtores que que recebem expressões de um certo tipo e retornam de outro tipo. Em particular, o If pode retornar qualquer tipo de expressão, contanto que os dois argumentos finais sejam do mesmo tipo.

Agora, a nossa função de avaliação se torna:

evalExpr :: Expr a -> a
evalExpr (I x)      = x
evalExpr (B b)      = b
evalExpr (Add l r)  = evalExpr l + evalExpr r
evalExpr (Mul l r)  = evalExpr l * evalExpr r
evalExpr (And l r)  = evalExpr l && evalExpr r
evalExpr (Or l r)   = evalExpr l || evalExpr r
evalExpr (If c l r) = if evalExpr c then evalExpr l else evalExpr r
evalExpr (Eq l r)   = evalExpr l == evalExpr r
evalExpr (Even x)   = even $ evalExpr x
evalExpr (Odd x)    = odd $ evalExpr x
evalExpr (Half x)   = (`div` 2) $ evalExpr x

{-# LANGUAGE StandaloneDeriving #-}
deriving instance Show (Expr a)
deriving instance Eq (Expr a)

Como exemplo, podemos construir a seguinte expressão e avaliar:

expr :: Expr Int
expr = Add (Mul (I 10) (I 2))
	   (If (Or (Eq (I 10) (I 10))
		   (B False)
	       )
	       (I 5)
	       (I 6)
	  )

Um exemplo mais complexo é a construção de uma expressão que avalia a conjectura de collatz para um determinado inteiro \(n\). A conjectura de Collatz é bem simples de formular de maneira informal:

Dado um número natural, se o número é par então divida por 2; senão multiplique por 3 e adicione 1.

A conjectura afirma que, após um número finito de iterações, alcança-se o número 1 para qualquer número inicial.

Aqui uma implementação para a conjectura:

half :: Int -> Expr Int
half n = Half (I n)

times3plus1 :: Int -> Expr Int
times3plus1 n = Add (Mul (I n) (I 3)) (I 1)

collatz :: Int -> Expr Int
collatz n = If (Even (I n))
		(half n)
		(times3plus1 n)

recur :: Int -> Expr Int
recur 1 = (I 1)
recur n = If (Eq (I n) (I 1))
	     (I n)
	     (recur $ evalExpr $ collatz n)

Note que recur vai gerar uma árvore com as decisões tomadas ao longo do caminho para calcular a convergência de \(n\) para \(1\).

1.2 Abrindo novas portas

Digamos que todas as salas de acesso restrito de nossa empresa são compostas por duas portas, uma externa e uma interna. Cada porta possui três possíveis estados: Open, Closed, e Hacked. Da mesma forma, podemos fazer diversas ações com essas portas como abrir a porta externa, entrar na sala intermediária, hackear uma das portas, etc. Porém, essas ações devem seguir certas regras de segurança:

• Só posso abrir a porta externa, se eu estiver do lado de fora e ela estiver fechada. Ao abrir essa porta, a porta interna deverá ser fechada.
• Só posso abrir a porta interna, se eu estiver na parte de espera e ambas as portas estiverem fechadas. Ao abrir essa porta, a porta externa deve permanecer fechada.
• Só posso entrar na parte de espera se a porta externa estiver aberta. Ao entrar, ambas as portas se fecham.
• Só posso entrar na parte interna se eu estiver na sala de espera e a porta interna estiver aberta. Após entrar na sala, ambas as portas são fechadas.
• Eu posso hackear a porta externa contanto que eu esteja do lado de fora.
• Posso hackear a interna se estiver na sala de espera.
• Posso invadir uma porta hackeada.

Vamos representar essas regras utilizando um tipo definido via GADT. Primeiro precisamos modelar os estados das portas e dos usuários:

{-# LANGUAGE DataKinds #-}
data StatusDoor = Open | Closed | Hacked

data StatusUser = Outside | Waiting | Inside

A porta pode estar aberta, fechada ou hackeada. O usuário pode estar do lado de fora, no espaço de espera ou dentro da sala.

Construiremos nosso sistema de portas com três parâmetros de tipo: dois com kind StatusDoor e um com kind StatusUser. Os dois primeiros tipos representam o estado da porta externa e interna respectivamente. Já o terceiro indica a localização do usuário em relação às portas.

O tipo Door outer inner user será criado estabelecendo todos os estados que queremos representar. Note que qualquer estado não compreendido por esse GADT, é um estado proibido que nunca existirá. O compilador nos dará essa garantia, não precisamos verificar nada.

data Door outer inner user where
  Initial     :: Door Closed Closed Outside
  OpenOuter   :: Door Closed i Outside -> Door Open Closed Outside
  OpenInner   :: Door Closed Closed Waiting -> Door Closed Open Waiting
  EnterSpace  :: Door Open Closed Outside -> Door Closed Closed Waiting
  EnterRoom   :: Door Closed Open Waiting -> Door Closed Closed Inside
  HackOuter   :: Door o i Outside -> Door Hacked i Outside
  HackInner   :: Door o i Waiting -> Door o Hacked Waiting
  InvadeOuter :: Door Hacked i Outside -> Door Hacked i Waiting
  InvadeInner :: Door o Hacked Waiting -> Door o Hacked Inside

Traduzindo para um ADT tradicional, essa estrutura seria algo como:

data Door o i u = Initial | OpenOuter (Door o' i' u') | OpenInner (Door o' i' u')
		| EnterSpace (Door o' i' u') | EnterRoom (Door o' i' u')
		| HackerOuter (Door o' i' u') | HackerInner (Door o' i' u')
		| InvadeOuter (Door o' i' u') | InvadeInner (Door o' i' u')

Note que na versão ADT tradicional, alguns estados proibidos pelo GADT se tornam possíveis, por exemplo, eu posso abrir a porta externa estando do lado de fora com as duas portas fechadas fazendo OpenInner Initial.

No entanto, o GADT só permite que o construtor OpenInner receba um tipo Door Closed Closed Waiting, e só podemos chegar nesse estado ao fazer a ação EnterSpace. Por sua vez, para chegar em EnterSpace, preciso fazer OpenOuter e, esse, só admite recebere Initial com argumento.

Com essas restrições limitamos a sequência de ações que são representáveis, e garantimos que nunca faremos algo absurdo! Vejamos alguns exemplos:

(>>>) = flip (.) -- vamos inverter a composição para facilitar

goInside :: Door Closed Closed Outside -> Door Closed Closed Inside
goInside = OpenOuter >>> EnterSpace >>> OpenInner >>> EnterRoom

A função goInside descreve o procedimento normal que alguém faria para entrar na sala. O código compila, então podemos ficar tranquilos que ninguém entrará pela porta dos fundos. Vamos tentar algo maluco, vou abrir a porta interna após abrir a porta externa mas sem entrar na antessala:

cantGoInside :: Door Closed Closed Outside -> Door Closed Closed Inside
cantGoInside = OpenOuter >>> OpenInner >>> EnterRoom

Esse código não compila. Não é possível seguir esses passos de acordo com o GADT que criamos. Vamos tentar invadir essa porta de duas formas diferentes.

hackYeah :: Door Closed Closed Outside -> Door Hacked Hacked Inside
hackYeah = HackOuter >>> InvadeOuter >>> HackInner >>> InvadeInner

halfHack :: Door Closed Closed Outside -> Door Closed Hacked Inside
halfHack = OpenOuter >>> EnterSpace >>> HackInner >>> InvadeInner

Ambos os métodos compilam e seguem uma lógica válida para entrar na sala. Finalmente, podemos criar uma função que lê a sequência de passos e imprime a sequência. Note que ao avaliar essa estrutura aninhada, o instante inicial está na parte mais interna. Portanto, a chamada recursiva deve ser feita antes da descrição da ação atual.

describe steps = go (steps Initial) >> putStrLn "Fini!"
  where
    go :: Door o i u -> IO ()
    go (EnterRoom x)   = go x >> putStrLn "You entered the room!"
    go (EnterSpace x)  = go x >> putStrLn "HA! HA! HA! You're stuck in the waiting room"
    go (OpenOuter x)   = go x >> putStrLn "You open the mysterious door"
    go (OpenInner x)   = go x >> putStrLn "You open the truest of the true door"
    go (HackOuter x)   = go x >> putStrLn "Hacking outer door....ok"
    go (HackInner x)   = go x >> putStrLn "Hacking inner door....ok"
    go (InvadeOuter x) = go x >> putStrLn "You're in!"
    go (InvadeInner x) = go x >> putStrLn "Welcome Mr. Elliot!"
    go Initial         = putStrLn "You arrived at the door"

1.3 Árvores balanceadas

Vamos recriar nossa árvore balanceada utilizando GADTs. Para isso queremos incluir a informação de profundidade em cada nó da árvore.

Ou seja, nossa árvore GTree a n conterá dois tipos associados:

• O tipo a dos valores que ela carrega
• A profundidade n da árvore

Para representar a profundidade, vamos criar uma definição recursiva conhecida como números de Peano:

data Nat = Z | S Nat

Essa representação dos números naturais pode conter o valor \(0\) (Z) ou um sucessor de um número (S). Ou seja, o número \(1\) é representado por S Z, o número \(2\) por S (S Z), e assim por diante. Com isso podemos criar nossa árvore como:

data GTree a n where
  GEmpty :: GTree a Z
  GNode  :: GTree a n -> a -> GTree a n -> GTree a (S n)

Uma árvore vazia é uma árvore com tipo GTree a Z, ou seja, profundidade \(0\). Um nó interno da árvore é composto por duas árvores de profundidade n, um elemento do tipo a e isso gera uma árvore de profundidade S n (um a mais da profundidade das árvores esquerda e direita). Por exemplo, uma árvore válida é:

gtree :: GTree Int (S (S Z))
gtree = GNode (GNode GEmpty 1 GEmpty) 2 (GNode GEmpty 3 GEmpty)

Podemos implementar a função análoga à insertB de forma simplificada, pois não precisamos nos preocupar em fazer um merge dos dois ramos:

insertG :: a -> GTree a n -> GTree a n -> GTree a (S n)
insertG x GEmpty GEmpty = GNode GEmpty x GEmpty
insertG x l r           = GNode l x r

E com isso podemos fazer:

node1 = insertG 1 GEmpty GEmpty
node3 = insertG 3 GEmpty GEmpty
node2 = insertG 2 node1 node3

Note que a seguinte implementação de inserção é inválida:

insertG :: a -> GTree a n -> GTree a (S n)
insertG x GEmpty        = GNode GEmpty x GEmpty
insertG x (GNode l y r) = GNode (insertG y l) x r

Isso porque ao inserir y em l criamos uma árvore com profundidade S n, uma a mais da profundidade de r.

Para entendermos como a criação da árvore com informação de profundidade pode nos ajudar nas implementações de funções auxiliares, vamos implementar três funções comuns para estruturas de árvores:

• Calcular a profundidade da árvore com depthG
• Retornar o elemento da raiz com topG
• Espelhar a árvore com mirrorG

Para calcular a profundidade da árvore perfeitamente balanceada, precisamos apenas seguir uma das ramificações, pois temos a garantia que todos os ramos possuem a mesma profundidade. Começamos a implementação listando os possíveis padrões de entrada:

depthG :: GTree a n -> Int
depthG GEmpty        = _
depthG (GNode l x r) = _

Por definição a profundidade de uma árvore GEmpty é \(0\):

depthG :: GTree a n -> Int
depthG GEmpty        = 0
depthG (GNode l x r) = _

Para o outro caso, ela é um a mais da profundidade de seus filhos (afinal o tipo é S n com n sendo a profundidade dos filhos):

depthG :: GTree a n -> Int
depthG GEmpty        = 0
depthG (GNode l x r) = 1 + depthG l

Essa implementação ainda não é ideal pois não reaproveitamos a informação proveniente do parâmetro de tipos. Se temos uma árvore GTree a (S (S Z)), sabemos que sua profundidade é S (S Z) = 2, idealmente teríamos uma função que converte o tipo em um valor.

Vamos tentar fazer isso definindo um tipo que carrega essa informação, vamos chamá-lo de Proxy:

data Proxy a = Proxy

Veja! Um tipo fantasma! 👻

O tipo Proxy é o tipo fantasma habitado mais simples que você poderia criar! Proxy armazena apenas o valor Proxy mas este valor é do tipo Proxy a. Com isso, idealmente poderíamos fazer algo como:

class NatToInt a where
  natToInt :: Proxy a -> Int

instance NatToInt Z where
  natToInt _ = 0

Isso causa o seguinte erro:

Expected a type, but ‘Z’ has kind ‘Nat’

Esse erro significa que NatToInt espera por tipo do kind * (o kind dos tipos habitados) e não kind Nat, que é aquele que criamos especificamente para os tipos naturais. Uma forma de resolver isso é especificar que Proxy armazena um tipo de kind Nat:

{-# LANGUAGE KindSignatures #-}
data Proxy :: Nat -> * where
  Proxy :: Proxy n

Isso exige uma nova extensão, a KindSignatures. Dessa forma especificamos que o kind do tipo que Proxy carrega é um Nat. Porém Proxy em si é um tipo de kind *.

Como Proxy é um construtor de tipo, a assinatura dele representa os kinds dos tipos que ele espera como entrada e o kind do tipo que ele cria. Um construtor de tipo paramétrico como Maybe a tem uma assinatura * -> * indicando que recebe um tipo do conjunto de tipos (a.k.a. kind) * e devolve um tipo do kind *.

Especificamente para os números naturais, criamos um novo kind, chamado Nat, que inclui os tipos Z, S Z, S (S Z),.... Logo, o compilador diferencia os kinds * e Nat.

Como queremos que a informação de tipo que Proxy carrega seja um tipo em Nat mas que Proxy em si seja um tipo em *, ao incluirmos a assinatura Nat -> *, indicamos que ao receber um tipo de Nat, criamos um tipo chamado Proxy em *.

Agora podemos complementar nossa instância de NatToInt com:

class NatToInt a where
  natToInt :: Proxy a -> Int

instance NatToInt Z where
  natToInt _ = 0
instance NatToInt n => NatToInt (S n) where
  natToInt _ = 1 + natToInt (Proxy :: Proxy n)

Isso ainda não compila, mas antes de prosseguirmos, vamos entender a ideia dessa implementação.

A função natToInt recebe um tipo Proxy a e retorna um Int, sabemos que o único valor desse tipo é Proxy, se escrevermos a definição da função com o argumento teríamos natToInt Proxy = ..., sabemos que o valor de Proxy é irrelevante para o que queremos, desejamos extrair a informação contida em seu parâmetro de tipo.

Sabemos que a instância de NatToInt para o tipo Z deve ser convertida para \(0\). Podemos enumerar as instâncias e criar instance NatToInt (S Z) e depois instance NatToInt (S (S Z)) e assim por diante. Como é impossível cobrir todos os casos manualmente, utilizamos da indução matemática para falar: “se eu sei qual o valor de um Proxy n, eu também sei o de Proxy (S n)”.

Então eu crio uma instância que fala NatToInt n => (dado que eu sei o valor para Proxy n), NatToInt (S n) where (eu consigo especificar o valor para Proxy (S n)). E esse valor é simplesmente 1 + o valor da chamada natToInt para Proxy com o tipo Proxy n.

Para essa implementação específica, o compilador reclama por não saber que o n de NatToInt (S n) deve ser o mesmo de Proxy :: Proxy n. Resolvemos essa situação com mais uma extensão, a ScopedTypeVariables.

Agora podemos ficar tentados a fazer uma implementação de depthG utilizando essa informação da seguinte forma:

depthG' :: NatToInt n => GTree a n -> Int
depthG' _ = natToInt (Proxy :: Proxy n)

Porém isso também vai falhar pois ele não consegue deduzir que Proxy n e GTree a n compartilham do mesmo n. Mas isso é fácil de resolver com uma função intermediária:

treeToProxy :: GTree a n -> Proxy n
treeToProxy _ = Proxy

depthG' :: NatToInt n => GTree a n -> Int
depthG' = natToInt . treeToProxy

Com isso temos uma implementação que extrai a informação diretamente do tipo. Isso funciona pois a função treeToProxy sabe exatamente qual Proxy deve gerar uma vez que essa informação está diretamente codificada na assinatura. Uma alternativa para essa implementação é indicar isso diretamente no código do depthG' com a palavra-chave forall, deixando o tipo n no escopo da definição da função:

depthG' :: forall a n . NatToInt n => GTree a n -> Int
depthG' _ = natToInt (Proxy :: Proxy n)

Ao fazer uso do forall explicitamos que a variável de tipo n pode ser referenciada dentro de nosso código. Podemos também fazer uma versão de natToInt que não utiliza Proxy e pode ser utilizada com TypeApplication. Deixaremos essa versão como desafio ao leitor.

A implementação de topG é simples e necessita apenas do padrão GNode:

topG :: GTree a (S n) -> a
topG (GNode _l x _r) = x

Veja que ao especificar a assinatura GTree a (S n) proibimos de tentar aplicar essa função no valor GEmpty, ou seja, tornamos a função topG total. Esse caso é análogo ao safeHead.

Finalmente, mirrorG pode ser implementado assim:

mirrorG :: GTree a n -> GTree a n
mirrorG GEmpty = GEmpty
mirrorG (GNode l x r) = GNode (mirrorG r) x (mirrorG l)

Como vimos até então, existem poucas operações interessantes para árvores perfeitamente balanceadas. Vamos flexibilizar essa restrição um pouco mais.

1.4 Árvores balanceadas imperfeitas

Um problema com as árvores perfeitamente balanceadas é que elas apresentam uma restrição em relação a quantidade de elementos que ela possui.

Por exemplo, em uma árvore binária, o número de nós deve ser uma potência de \(2\).

É comum relaxar um pouco tal restrição para que possamos construir árvores que estejam próximas de um balanceamento perfeito sem restringir a quantidade de nós.

Vamos construir uma árvore em que a profundidade dos ramos da esquerda e direita diferem em até \(1\) elemento. Para isso precisamos de uma estrutura adicional que servirá como indicador de qual caso estamos lidando:

• Árvore perfeitamente balanceada
• Árvore com profundidade maior no ramo da esquerda
• Árvore com profundidade maior no ramo da direita

data Balance :: Nat -> Nat -> Nat -> * where
  E :: Balance a a a
  L :: Balance (S a) a (S a)
  R :: Balance a (S a) (S a)

A estrutura Balance indica que uma árvore pode ser perfeitamente balanceada (E), pendendo para esquerda (L) ou para direita (R). Os três argumentos servem para produzir uma prova da informação dos ramos daquele nó. O primeiro argumento indica a profundidade do ramo esquerdo, o segundo do ramo direito, e o terceiro indica qual a maior profundidade. Precisaremos desse terceiro parâmetro para determinarmos a profundidade do nó atual.

Com isso podemos definir nossa árvore imperfeita ITree (não confundir com um produto da Apple™).

data ITree a n where
  IEmpty :: ITree a Z
  INode  :: ITree a m -> a -> ITree a n -> Balance m n o -> ITree a (S o)

Da mesma forma que no GTree, o IEmpty cria uma árvore com profundidade \(0\) (Z). O INode é composto de uma árvore esquerda de profundidade m, um elemento do tipo a, e uma árvore direita de profundidade n. Além disso, precisamos fornecer a prova de que ela é balanceada com Balance m n o, sendo o a maior profundidade entre os ramos. Com essa informações, podemos produzir uma árvore do tipo ITree a (S o), ou seja, um a mais da maior profundidade.

De forma análoga ao que foi feito com GTree podemos implementar depthI, topI. A função mirrorI requer alguns cuidados extras pois, ao trocar um ramo pelo seu irmão, o balanceamento da árvore pode mudar.

treeIToProxy :: ITree a n -> Proxy n
treeIToProxy _ = Proxy

depthI :: NatToInt n => ITree a n -> Int
depthI t = natToInt $ treeIToProxy t

topI :: ITree a (S n) -> a
topI (INode _l x _r _m) = x

mirrorI :: ITree a n -> ITree a n
mirrorI IEmpty          = IEmpty
mirrorI (INode l x r E) = INode (mirrorI r) x (mirrorI l) E
mirrorI (INode l x r L) = INode (mirrorI r) x (mirrorI l) R
mirrorI (INode l x r R) = INode (mirrorI r) x (mirrorI l) L

A função depthI é exatamente igual a depthG, nenhuma mudança foi necessária. Já a única alteração para topI foi acrescetar um quarto argumento para o padrão de INode referente a prova do balanceamento da árvore.

Para a função mirrorI, precisamos cuidar dos três casos de balanceamento de um INode em separado. Se o balanceamento atual for E, a troca do filho da esquerda pelo da direita não afeta o balanceamento. Caso o balanceamento seja L, a troca dos filhos faz com que a maior profundidade se torne o ramo da direita, então o novo balanceamento é R. Da mesma forma, se o atual for R, trocamos para L.

É interessante notar que qualquer troca do valor do balanceamento nesse código causa um erro de compilação. O compilador não permite que você escreva uma regra incorreta.

Finalmente, podemos pensar em criar uma função insertI que insere um novo elemento na árvore. O processo de criação dessa função receberá ajuda das nossas especificações do tipo (e, eventualmente, do compilador, caso você erre alguma regra).

Como primeiro passo, vamos definir a assinatura da função:

insertI :: a -> ITree a n -> ITree a m

A função insertI recebe um elemento do tipo a, uma árvore com profundidade n e retorna uma árvore com profundidade m. O compilador não vai deixar criarmos qualquer função com essa assinatura, pois o tipo m precisa ser bem especificado na definição da função.

Notem que o retorno dessa função pode tanto ser uma árvore com uma profundidade maior que a atual, caso a inserção do elemento implique criar um ramo extra, ou simplesmente a manutenção da profundidade atual.

Pensem no efeito de inserir um elemento nas seguintes árvores:

insert 0 Node (E 1 E) 2 (E 3 E) = Node ((E 0 E) 1 E) 2 (E 3 E)

insert 0 Node ((E 1 E) 2 E) 3 (E 4 E) = Node ((E 1 E) 2 (E 0 E)) 3 (E 4 E)

No primeiro caso a inserção causa um aumento na profundidade, enquanto no segundo a profundidade se mantém. Vamos criar um novo tipo que indicará se a altura foi acrescida de um ou não.

data MoreOrEq :: (Nat -> *) -> (Nat -> *) where
  NoChange :: t n     -> MoreOrEq t n
  AddOne   :: t (S n) -> MoreOrEq t n

A estrutura MoreOrEq recebe um tipo que aguarda por um Nat para gerar um tipo (*) e retorna um tipo que recebe um Nat e retorna um tipo. Na definição da estrutura, específico para nosso caso, t será substituído por ITree a. Então, para um dado n, o valor NoChange recebe um ITree a n enquanto AddOne recebe um ITree a (S n).

Com isso, a assinatura de insertI se torna:

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n

Vamos escrever o caso mais simples, inserção em uma árvore vazia:

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = _

A inserção em uma árvore vazia é simplesmente um nó contendo x cujos filhos são IEmpty:

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = INode IEmpty x IEmpty _

Além dos ramos, precisamos inserir a prova de balanceamento. Nesse caso, ambos os filhos tem profundidade \(0\), portanto temos:

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = INode IEmpty x IEmpty E

Finalmente, precisamos indicar se a profundidade original aumentou ou não. A árvore de entrada tinha profundidade \(0\), a nova árvore tem profundidade \(1\):

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E

Notem que qualquer alteração nesse código produzirá um erro de compilação. A prova E está amarrada com a profundidade de ambos IEmpty de tal forma que nem L e nem R satisfazem a condição. Por sua vez, AddOne está amarrado com o INode da saída e o IEmpty da entrada.

Para os outros casos, precisaremos checar a propriedade de balanceamento do nó atual.

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E
insertI x (INode l y r m) =
  case m of
    E -> _

Caso o nó atual tenha um balanceamento perfeito, vamos inserir no nó da esquerda (essa é uma decisão arbitrária, poderíamos escolher de acordo com a ordem de x em relação a y, caso fosse uma árvore de busca):

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E
insertI x (INode l y r m) =
  case m of
    E -> INode (insertI x l) y r m

Isso não funciona, pois insertI retorna um MoreOrEq e não um ITree, precisamos casar os possíveis padrões:

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E
insertI x (INode l y r m) =
  case m of
    E -> case insertI x l of
	   AddOne t   -> AddOne   $ INode t y r _
	   NoChange t -> NoChange $ INode t y r _

Se o resultado da inserção foi um acréscimo na profundidade da esquerda, retornamos um AddOne do novo nó, pois dado que estamos perfeitamente balanceados, um acréscimo na profundidade de qualquer um dos ramos, causa um acréscimo do nó atual. No caso em que temos AddOne, o balanceamento deve passar de E para L, pois agora o ramo da esquerda tem uma profundidade maior, no caso NoChange, permanecemos em E.

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E
insertI x (INode l y r m) =
  case m of
    E -> case insertI x l of
	   AddOne t   -> AddOne   $ INode t y r L
	   NoChange t -> NoChange $ INode t y r E

Novamente como exercício, tente alterar alguma dessas definições e você perceberá que o compilador não permite que algo diferente seja feito.

Para o caso em que a árvore esteja pendendo para a direita, devemos inserir no ramo da esquerda para atingir o equilíbrio. Novamente a inserção a esquerda gera um entre dois casos:

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E
insertI x (INode l y r m) =
  case m of
    E -> case insertI x l of
	   AddOne t   -> AddOne   $ INode t y r L
	   NoChange t -> NoChange $ INode t y r E
    R -> case insertI x l of
	   AddOne t   -> _
	   NoChange t -> _

No primeiro caso, ao aumentar em um na profundidade de l, atingimos um balanceamento perfeito. Caso contrário, continuamos pendendo para a direita. Notem que em ambos os casos, não ocorre mudança na profundidade do nó atual, pois o resultado da inserção ou mantém o ramo da direita como a maior profundidade ou faz com que ambos os ramos tenham a mesma profundidade, sem alterar o máximo entre eles.

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E
insertI x (INode l y r m) =
  case m of
    E -> case insertI x l of
	   AddOne t   -> AddOne   $ INode t y r L
	   NoChange t -> NoChange $ INode t y r E
    R -> case insertI x l of
	   AddOne t   -> NoChange $ INode t y r E
	   NoChange t -> NoChange $ INode t y r R

Finalmente, para o caso de pender para a esquerda, fazemos o processo análogo:

insertI :: a -> ITree a n -> MoreOrEq (ITree a) n
insertI x IEmpty = AddOne $ INode IEmpty x IEmpty E
insertI x (INode l y r m) =
  case m of
    E -> case insertI x l of
	   AddOne t   -> AddOne   $ INode t y r L
	   NoChange t -> NoChange $ INode t y r E
    R -> case insertI x l of
	   AddOne t   -> NoChange $ INode t y r E
	   NoChange t -> NoChange $ INode t y r R
    L -> case insertI x r of
	   AddOne t   -> NoChange  $ INode l y t E
	   NoChange t -> NoChange  $ INode l y t L

Vamos tentar implementar uma última função que recebe uma lista de valores do tipo a e cria uma árvore balanceada ITree a n:

fromListI :: [a] -> ITree a n

Com essa assinatura caímos no mesmo problema em que o compilador não consegue determinar o tipo de n em tempo de compilação, pois depende do tamanho de [a]. Uma alternativa é utilizar a técnica Continuation Passing Style em que uma função recursiva é transformada em uma função de alta-ordem em que o último argumento é uma função responsável por continuar o processamento. Em outras palavras queremos algo como:

fromListI :: [a] -> (ITree a n -> r) -> r
fromListI xs f = _

Ou seja, f é uma função que vai cuidar de processar um elemento de xs, possivelmente inserindo em uma árvore e computando para um tipo r. O tipo r é aquilo que queremos fazer com a árvore final, como por exemplo, transformar em uma String.

Porém, essa assinatura ainda é insuficiente, pois a função argumento ainda precisa de um tipo n especificado em tempo de compilação. Precisamos explicitar que ela é uma função genérica e que o n pode mudar a cada chamada.

O que queremos é especificar fromListI :: [a] -> (forall n . ITree a n -> r) -> r, ou seja, nossa função funciona para qualquer n. Isso cria uma garantia pro compilador que não estamos passando uma função especificada apenas para um n fixo. Para que possamos fazer isso, precisamos adicionar a extensão RankNTypes. Em um post anterior já explicamos essa extensão com maior profundidade.

fromListI :: [a] -> (forall n . ITree a n -> r) -> r
fromListI []     f = _

O primeiro caso, a lista vazia, devemos simplesmente aplicar a função em um nó do tipo IEmpty.

fromListI :: [a] -> (forall n . ITree a n -> r) -> r
fromListI []     f = f IEmpty
fromListI (x:xs) f = _

Para o segundo caso, precisamos chamar fromListI recursivamente no restante da lista, passando uma nova função como argumento:

fromListI :: [a] -> (forall n . ITree a n -> r) -> r
fromListI []     f = f IEmpty
fromListI (x:xs) f = fromListI xs $
		      \t -> _

Essa função deve inserir o valor x em uma árvore (argumento t da função anônima), e aplicar f no resultado. Note que a inserção de um elemento gera um MoreOrEq e, portanto, devemos retirar a árvore de dentro desse tipo:

fromListI :: [a] -> (forall n . ITree a n -> r) -> r
fromListI []     f = f IEmpty
fromListI (x:xs) f = fromListI xs $
		      \t -> case insertI x t of
			      AddOne t'   -> f t'
			      NoChange t' -> f t'

Ambos os casos devem ser especificados, embora pareçam redundantes, pois cada um deles gera uma árvore de tipos diferentes. Durante a compilação o compilador precisa saber qual tipo está lidando. Um exemplo de uso dessa função é:

> putStrLn $ fromListI [1 .. 5] show
INode (INode (INode IEmpty 2 IEmpty E) 4 IEmpty L) 5 (INode (INode IEmpty 1 IEmpty E) 3 IEmpty L) E

2 Estudo de caso: vetores indexáveis seguros

Vetores indexáveis não são bem uma novidade em linguagens de programação. Mesmo em Haskell podemos fazer isto usando o operador (!!) de listas (cuidado com a complexidade linear!) ou ainda usar uma biblioteca de vetores. Em particular, a biblioteca vector que oferece o tipo Data.Vector com indexação em tempo constante. Um código deste tipo tem a seguinte cara:

> ['a'.. 'z'] !! 13
'n'
> import Data.Vector
> :t fromList ['a'.. 'z']
fromList ['a'.. 'z'] :: Vector Char
> fromList ['a'.. 'z'] ! 13
'n'

Contudo, gostaríamos de evitar erros como acessos a posições inválidas do vetor durante a execução do programa. Veja, por exemplo, o que acontece nos seguintes casos:

> fromList ['a'.. 'z'] ! (-1)
*** Exception: ./Data/Vector/Generic.hs:257 ((!)): index out of bounds (-1,26)
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Internal/Check.hs:87:5 in vector-0.12.3.1-2QhxFayEJrmJ3PNYTgAmQ3:Data.Vector.Internal.Check

Esse erro específico (fornecer um índice negativo) pode ser resolvido alterando a assinatura do (!) (e quaisquer funções que possam sofrer do mesmo problema) de (!) :: Vector a -> Int -> a para (!) :: Vector a -> Natural -> a. Natural é um tipo presente na biblioteca básica de Haskell que contém apenas números naturais (sic), ou seja, maiores ou iguais a zero.

Essa mudança, contudo, ainda não impede erros como acessar um índice maior do que o número de elementos contidos no vetor. Para evitar que tais erros tenham consequências catastróficas durante a execução, em geral acaba-se espalhando pelo código todo verificações de limites dos índices. Essas verificações tomam tempo e, dependendo da linguagem/biblioteca é feita uma escolha se os limites são checados ou não. Por exemplo, Java verifica todos os acessos enquanto C não o faz. Em Haskell a biblioteca vector oferece a função (!) que verifica os limites e que lança um erro caso o índice esteja fora dos limites, a função (!?) que devolve um Maybe a e ainda a versão unsafeIndex que quando recebe um índice inválido pode criar pernas e matar o seu gato.

Dá para fazer melhor? Sim! (apesar de algumas quinas meio pontudas ainda sobrarem pelo caminho 😝).

Para começar vamos aproveitar a implementação de números naturais de Peano que foi apresentada logo acima e usar esses números para indexar o nosso vetor!

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}

data Nat = Z | S Nat

type Vector :: Nat -> * -> *
data Vector n a where
  Nil :: Vector Z a
  (:>) :: a -> Vector n a -> Vector (S n) a

Vamos olhar com um pouco mais de cuidado essa declaração. Aqui usamos a sintaxe de GADTs para definir uma estrutura parecida com listas que tem dois construtores possíveis: Nil que cria um vetor vazio e (:>) que cria um vetor não vazio dado um elemento do tipo a e a cauda da lista. Vector é paramétrico em n e a, n é do kind Nat que nós definimos logo acima (para isso é preciso habilitar a extensão StandaloneKindSignatures e DataKinds) e a é do kind *, ou seja, qualquer tipo habitado que queiramos armazenar no nosso vetor.

O fato de estarmos usando GADTs nos permite especificar os tipos das entradas e retorno de maneira mais precisa, veja que Nil tem tipo de retorno Vector Z a, ou seja, a informação do comprimento do vetor está embutida no seu tipo, neste caso 0. Já o construtor (:>) recebe um elemento e um vetor já construído e devolve um novo vetor. O tipo dos elementos do vetor de retorno é o mesmo do elemento fornecido e do vetor de cauda, mas o seu tamanho é o tamanho da cauda n + 1, ou na notação acima (S n).Ou seja, automaticamente ao adicionarmos algo a um vetor, o vetor de resposta terá um tipo que vai refletir o novo tamanho.

Bom vamos tentar usar. Se tentarmos usar isso tomamos um erro:

> 1 :> 2 :> 5 :> Nil

<interactive>:13:1: error:
    • No instance for (Num (Vector n1 Integer))
	arising from a use of ‘it’
    • In the first argument of ‘print’, namely ‘it’
      In a stmt of an interactive GHCi command: print it

O que está ocorrendo aqui é que não estamos construindo o que pensamos. Veja:

> :t 1 :> 2 :> 5 :> Nil
1 :> 2 :> 5 :> Nil
  :: (Num a, Num (Vector n1 a),
      Num (Vector n2 (Vector ('S n1) a))) =>
     Vector ('S 'Z) (Vector ('S n2) (Vector ('S n1) a))

A associatividade está toda errada! Uma maneira de consertar é usando parênteses:

> :t 1 :> (2 :> (5 :> Nil))
1 :> (2 :> (5 :> Nil)) :: Num a => Vector ('S ('S ('S 'Z))) a

Ou ainda, definindo a associatividade na mão:

type Vector :: Nat -> * -> *
data Vector n a where
  Nil :: Vector Z a
  (:>) :: a -> Vector n a -> Vector (S n) a
infixr 5 :>

E agora tudo funciona como esperado:

> :t 1 :> 2 :> 5 :> Nil
1 :> 2 :> 5 :> Nil :: Num a => Vector ('S ('S ('S 'Z))) a
> 1 :> 2 :> 5 :> Nil
1 :> (2 :> (5 :> Nil))

Vamos implementar algumas funções simples para o nosso vetor:

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

vhead :: Vector (S n) a -> a
vhead (x :> _) = x

vtail :: Vector (S n) a -> Vector n a
vtail (_ :> xs) = xs

Primeiramente utilizamos a opção -Wno-unticked-promoted-constructors do GHC para que ele deixe de emitir warnings de compilação quando usamos S e Z sem os apóstrofos ('S e 'Z). A discussão sobre o uso do prefixo ' ainda causa divisão entre os usuários, mas nestas notas usaremos ' apenas quando necessário. Mesmo porque em breve esse warning deverá ser desabilitado por padrão!

Aqui definimos duas funções comuns de listas, vhead que devolve o primeiro elemento e vtail que devolve a cauda da lista. Ambas as funções lançam mão de um truque para assegurarem-se que as listas com as quais estão trabalhando não são vazias: S n. Ora, se o tipo da lista (e portanto seu tamanho) é S n, então existe um número natural que é menor que S n, n que é no mínimo 0. Ou seja, o tamanho da lista é no mínimo 1! Logo podemos pegar a cabeça e a cauda sem problemas.

Mais ainda, se você tentar definir os casos de Nil você vai tomar um warning:

vhead :: Vector (S n) a -> a
vhead Nil = undefined
vhead (x :> _) = x

src/Main.hs:19:7: warning: [-Winaccessible-code]
    • Couldn't match type ‘'S n’ with ‘'Z’
      Inaccessible code in
	a pattern with constructor: Nil :: forall a. Vector 'Z a,
	in an equation for ‘vhead’
    • In the pattern: Nil
      In an equation for ‘vhead’: vhead Nil = undefined
    • Relevant bindings include
	vhead :: Vector ('S n) a -> a (bound at src/Main.hs:19:1)
   |
19 | vhead Nil = undefined
   |       ^^^

Essa linha em particular Couldn't match type ‘'S n’ with ‘'Z’ está nos dizendo claramente: você disse na assinatura de tipos que é não zero, como você quer fazer um casamento com zero?

Podemos também criar algumas instâncias para classes comuns que são fáceis de implementar:

instance Functor (Vector n) where
  fmap _ Nil = Nil
  fmap f (x :> xs) = f x :> fmap f xs

instance Foldable (Vector n) where
   foldMap _ Nil         = mempty
   foldMap f (x :> xs) = f x <> foldMap f xs

E com isso já podemos usar tudo que vem de graça:

> fmap (*3) $ 1 :> 2 :> 5 :> Nil
3 :> (6 :> (15 :> Nil))
> sum $ 1 :> 2 :> 5 :> Nil
8

Note que se tivéssemos cometido um erro na implementação de fmap, por exemplo, e tivéssemos esquecido de chamar recursivamente o compilador nos avisaria que algo está errado, pois os tipos não batem:

   • Occurs check: cannot construct the infinite type:
	b ~ Vector ('S n1) b
      Expected type: Vector n b
	Actual type: b
    • In the expression: f x
      In an equation for ‘fmap’: fmap f (x :> xs) = f x
      In the instance declaration for ‘Functor (Vector n)’
    • Relevant bindings include
	xs :: Vector n1 a (bound at src/Main.hs:27:16)
	f :: a -> b (bound at src/Main.hs:27:8)
	fmap :: (a -> b) -> Vector n a -> Vector n b
	  (bound at src/Main.hs:26:3)
   |
27 |   fmap f (x :> xs) = f x
   |                      ^^^

O erro é HORRÍVEL! Mas ele está querendo dizer o seguinte: olha, eu esperava um vetor do tipo Vector n b, mas você me forneceu b. Como b precisa ser igual a Vector n b e b está presente dos dois lados da equação, o GHC tenta provar indutivamente que ambos são iguais. Como não há o que possa ser feito neste caso ele desiste e grita “infinite type” já que a indução para determinar a igualdade não tem fim.

Uma outra função que, é fácil de ser implementada é a vinit que devolve o vetor sem o último elemento.

vinit :: Vector (S n) a -> Vector n a
vinit (_ :> Nil) = Nil
vinit (x :> xs) = x :> vinit xs

Parece ser uma implementação razoável. Mas o GHC não gosta. Ele fala:

src/Main.hs:35:30: error:
    • Couldn't match type ‘n’ with ‘'S n0’
      ‘n’ is a rigid type variable bound by
	the type signature for:
	  vinit :: forall (n :: Nat) a. Vector ('S n) a -> Vector n a
	at src/Main.hs:33:1-37
      Expected type: Vector ('S n0) a
	Actual type: Vector n1 a
    • In the first argument of ‘vinit’, namely ‘xs’
      In the second argument of ‘(:>)’, namely ‘vinit xs’
      In the expression: x :> vinit xs
    • Relevant bindings include
	vinit :: Vector ('S n) a -> Vector n a (bound at src/Main.hs:34:1)
   |
35 | vinit (x :> xs) = x :> vinit xs
   |

Todo esse auê tem como motivo o fato de que o GHC não é esperto o suficiente para notar que xs é não vazio. Nós sabemos que xs é não vazio pois caso fosse ele teria entrado no primeiro caso do pattern match ((_ :> Nil)). Mas ele não carrega esse tipo de informação de um pattern para outro. Nos resta então refazer o pattern match para que ele saiba nesse contexto que xs não é vazio:

vinit :: Vector (S n) a -> Vector n a
vinit (_ :> Nil) = Nil
vinit (x :> xs@(_ :> _)) = x :> vinit xs

E length? Ah! Já vimos isso neste post! Vamos lá:

vlength :: Vector n a -> Int
vlength Nil = 0
vlength (_ :> xs) = 1 + vlength xs

Mas pera lá! vlength está me devolvendo um inteiro. Mais ainda! Ele está varrendo o vetor inteiro para me devolver algo que já está ali no tipo: vlength :: Vector n a -> Int! Não bastaria fazer algo assim?²

vlength :: Vector n a -> Nat
vlength _ = n

2.1 Um cheiro de Singleton types

Infelizmente algo como proposto acima não funciona. Veja, em Haskell os tipos são todos apagados num processo chamado type erasure durante o processo de compilação. Não há informação disponível durante a execução para devolver o valor de n.

Nem todas as linguagens são assim. Python e Java, por exemplo, carregam as informações dos tipos o tempo todo. Como quase tudo nessa vida isso tem algumas vantagens e algumas desvantagens, sendo que as principais desvantagens talvez sejam perda de desempenho e aumento de consumo de memória.

O que precisamos então, se é necessário saber o tipo em tempo de execução, é um termo que armazene esse dado. Esse é justamente o papel de um sigleton type .

Nós vamos criar um construtor de tipos (type) que tem exatamente um termo (singleton), ou representante, possível em tempo de execução.

type SNat :: Nat -> *
data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

Agora podemos criar termos do tipo SNat em tempo de execução:

let x = SS (SS (SS SZ))

Em outras palavras, existe um isomorfismo entre o conjunto de termos de SNat e os tipos Nat (o que é meio óbvio se pensarmos que, SNat é o resultado de apenas replicamos a estrutura do Nat, com um prefixo S para denotar singleton). A diferença contudo é que enquanto os tipos de Nat vivem no nível dos tipos, os termos de SNat vivem no nível dos termos.

Agora podemos tentar consertar a nossa tentativa:

vlength :: Vector n a -> SNat n
vlength Nil = SZ
vlength (_ :> xs) = SS (vlength xs)

Ué, saímos de uma solução que usava inteiros, recursiva, e fizemos uma solução que é exatamente a mesma coisa que em vez de usar Int usa SNat. O que ganhamos com isso?

A verdade que agora ganhamos alguma segurança nos tipos. Erros que não seriam pegos antes pelo compilador agora são pegos! Por exemplo, os códigos abaixo causariam um erro nesta nova versão e passariam, batido na versão equivalente com Int:

vlength :: Vector n a -> SNat n
vlength Nil = SS SZ -- 1, e não 0 como deveria ser
vlength (_ :> xs) = SS (vlength xs)

vlength :: Vector n a -> SNat n
vlength Nil = SZ
vlength (_ :> xs) = SZ

Novamente, isso tudo porque agora o nosso valor de retorno SNat n está amarrado a n que é dado pelo tipo do vetor.

E do outro lado, quando o número está na entrada? Por exemplo, a função vreplicate, como fica a implementação? Vamos começar pela assinatura:

vreplicate :: SNat n -> a -> Vector n a
vreplicate = _

Recebemos um SNat n que representa o tamanho do vetor a ser criado, o elemento a ser replicado e amarramos o tamanho do vetor n! Feito, vamos tentar rechear essa função:

vreplicate :: SNat n -> a -> Vector n a
vreplicate SZ _ = Nil
vreplicate (SS n) x = x :> vreplicate n x

Como os elementos de SNat vivem no nível dos termos não temos dificuldade alguma em fazer pattern match nos seus valores. Da mesma maneira que vlength, essa versão garante que o tamanho do vetor vai ser exatamente o que foi pedido. Se tentarmos devolver um vetor do tamanho errado receberemos um erro de compilação, pois os tipos não vão bater.

2.2 Tipos existenciais

Todas essas funções tem algo em comum. Elas ou devolvem um tipo diferente (a, por exemplo) ou devolvem uma lista que cujo tamanho (e portanto cujo tipo) nós sabemos de antemão. vtail por exemplo, é o tamanho da lista de entrada menos um. fmap não altera o tamanho da lista e o foldMap devolve um monoide (que é no fim o tipo do elemento contido no vetor).

Mas e quando temos funções como filter para as quais não temos ideia alguma sobre o tamanho da saída? Vamos tentar:

vfilter :: (a -> Bool) -> Vector n a -> Vector m a
vfilter _ Nil = Nil
vfilter p (x :> xs)
  | p x = x :> vfilter p xs
  | otherwise = vfilter p xs

Que nos resulta uma sequência divertida de erros cujo resumo é o seguinte: repare nos possíveis tipos de retorno. Se o vetor for vazio, o retorno é do tipo Vector Z a. Se não for vazio e se o predicado p for verdadeiro, então o tipo de retorno será Vector m a onde m é 1 + seja qual for o tipo de retorno da chamada recursiva. Por outro lado o tipo de retorno caso o predicado seja falso, é simplesmente o tipo de retorno da chamada recursiva. Logo, a depender do vetor de entrada do predicado e de x o tipo de retorno da função muda!

Isso não é aceitável, o compilador fica biruta e joga a panela na nossa cara.

O que precisaríamos é contar para o compilador que está tudo bem, que existe um valor de m que garantidamente vai fazer tudo dar certo no final. m é um tipo existencial (existential type).

O que gostaríamos é algo parecido com a palavra chave forsome que existe em Scala que permitiria fazer algo assim:

vfilter :: forall a n. (a -> Bool) -> Vector n a -> (forsome m. Vector m a)
vfilter _ Nil = Nil
vfilter p (x :> xs)
  | p x = x :> vfilter p xs
  | otherwise = vfilter p xs

forsome indica que existe um m, ainda que não saibamos qual no momento, que funciona. Infelizmente isso não existe em Haskell. Há propostas de como isso poderia ser feito, mas enquanto isso a gente vai ter que usar um truque e esconder o m do compilador.

Antes de resolver este problema no contexto dos vetores, vamos considerar um exemplo um pouco mais simples de que queremos guardar em uma lista vários elementos que possam ser transformados em string (ou seja, valores de tipos que possuem instâncias para a classe Show) e depois implementar uma função que concatena tudo separado por " - ":

imprimiveis = [1, "Ola Mundo!", 'x', 35.4, (42, "a resposta!")]

separadoPorHifen :: Show a => [a] -> String
separadoPorHifen = intercalate " - " . fmap show

Se você fornecer isso pro GHC, vai receber um erro um tanto confuso. Esse erro quer dizer simplesmente que, infelizmente, isso não é possível: as listas do Haskell exigem que todos os seus elementos possuam o mesmo tipo que, claramente, não é o nosso caso. Será que conseguimos de algum jeito fazer esses valores entrarem numa lista?

Na falta de tipos existenciais como em Scala, nós vamos usar um truque para enganar o compilador e esconder os tipos dele e obter o mesmo efeito.

data Escondido where
  MkEsc :: a -> Escondido

Note que o tipo Escondido tem kind *. Ele não é paramétrico e, para quem olha de fora, um Escondido que guarda uma string não é diferente de um que guarda um inteiro.

A lista é esse observador externo. Todos os Escondidos lhe parecem iguais. Agora podemos criar livremente a nossa lista:

> imprimiveis = [MkEsc 1, MkEsc "Ola Mundo!", MkEsc 'x', MkEsc 35.4, MkEsc (42, "a resposta!")]
> :t imprimiveis
imprimiveis :: [Escondido]

Legal! Mas ainda não podemos fazer muita coisa com essa lista. Se tentarmos chamar função separadoPorHifen, vamos tomar um erro:

> putStrLn $ separadoPorHifen imprimiveis

<interactive>:23:1: error:
    • No instance for (Show Escondido)
	arising from a use of ‘separadoPorHifen’

Se tentarmos criar uma instância de Show para Escondido vamos nos deparar com o problema de que não sabemos nada a respeito de a, o tipo dos elementos contido em Escondido. Precisamos dizer pro compilador que são, ao menos, tipos com instâncias de Show:

data Escondido where
  MkEsc :: Show a => a -> Escondido
deriving instance Show Escondido

E agora sim, tudo funciona como esperávamos:

> putStrLn $ separadoPorHifen imprimiveis
MkEsc 1 - MkEsc "Ola Mundo!" - MkEsc 'x' - MkEsc 35.4 - MkEsc (42,"a resposta!")

Vamos agora usar o mesmo truque de “esconder” o tipo dos elementos com o nosso vetor. O tipo existencial que criaremos agora deve esconder o tipo que representa o tamanho do vetor, mas não o tipo dos seus elementos:

type ExVector :: * -> *
data ExVector a where
  MkExVector :: Vector n a -> ExVector a


vfilter :: (a -> Bool) -> Vector n a -> ExVector a
vfilter _ Nil = Nil
vfilter p (x :> xs)
  | p x = x :> vfilter p xs
  | otherwise = vfilter p xs

ExVector é apenas uma casca no Vector, um Existential Vector. Repare que ele esconde o tamanho dentro dele (o tipo é apenas ExVector a), ou seja, o compilador não pode mais reclamar sobre os tipos de retorno da nossa função vfilter! Como dizia o ditado: o que o compilador não vê o coração não sente (ou algo assim).

Já consertamos a nossa assinatura de função, mas agora precisamos consertar também a implementação. As chamadas recursivas até passam como parâmetro os valores do tipo certo mas o tipo de retorno é agora ExVector a e não mais Vector n a. Precisamos retirar novamente o vetor de dentro da casca existencial e juntar com o eventual x se o predicado for verdadeiro.

Vamos ver a implementação e explicar em seguida:

vfilter :: (a -> Bool) -> Vector n a -> ExVector a
vfilter _ Nil = MkExVector Nil
vfilter p (x :> xs)
  | p x =
    case vfilter p xs of
      MkExVector fTail -> MkExVector (x :> fTail)
  | otherwise = vfilter p xs

A adaptação para o caso base da recursão, Nil é trivial. Basta colocarmos a casca existencial em torno de Nil. O caso onde o predicado é falso também é tranquilo, já que basta devolver como resposta a chamada recursiva na cauda.

O caso quando o predicado é verdadeiro é um pouco mais trabalhoso e, infelizmente, não tem muito jeito. Já estamos na base da maracutaia pra esconder o tipo do compilador, e agora é mais um truque.

Primeiramente fazemos a chamada recursiva na cauda. Do resultado (que é do tipo ExVector a) precisamos tirar o vetor para podermos juntar com o valor x (que deve ser adicionado ao retorno já que a avaliação do predicado deu verdadeira). Para fazer isso utilizamos um pattern match em um case. A cauda filtrada é armazenada em fTail, que é juntada com x e recolocada numa casca existencial para ser devolvida como retorno.

Agora sim! todos os tipos de retorno do corpo da função batem e nosso código está completo.

Infelizmente essa implementação perde a preguiça do código já que toda a lista precisa ser avaliada para devolver um valor. Uma proposta de como manter a preguiça pode ser vista no paper de Eisenberg et. al.

Outra coisa perdida é que os tipos estão mais soltos do que necessário. Queremos que o vetor de saída tenha no máximo o mesmo número de elementos da entrada, mas como está agora ele poderia até aumentar e o compilador (só de birra porque escondemos os tipos dele) não ia falar nada.

Por exemplo, isso aqui compila:

vfilter :: (a -> Bool) -> Vector n a -> ExVector a
vfilter _ Nil = MkExVector Nil
vfilter p (x :> xs)
  | p x =
    case vfilter p xs of
      MkExVector fTail -> MkExVector (x :> x :> x :> x :> fTail)
  | otherwise = vfilter p xs

Note como colocamos o x na resposta mais de uma vez. E isso aqui também!

vfilter :: (a -> Bool) -> Vector n a -> ExVector a
vfilter _ Nil = MkExVector Nil
vfilter p (x :> xs)
  | p x =
    case vfilter p xs of
      MkExVector fTail -> MkExVector fTail
  | otherwise = vfilter p xs

Notem como não colocamos nada na resposta!

Pra melhorar isso, vamos começar colocando algumas restrições no nosso tipo existencial:

type ExVector :: (Nat -> Constraint) -> * -> *
data ExVector c a where
  MkExVector :: c n => Vector n a -> ExVector c a

Esse código exige a ativação a extensão ConstraintKinds. O que ele está fazendo? Queremos garantir que o tipo de retorno da função filter seja restrito no sentido de que, dado um vetor de tamanho n, o tamanho de retorno não pode ser maior. Agora que já deixarmos explícito no tipo de ExVector que n deve respeitar essa restrição podemos finalmente escrevê-la:

type (>=) :: Nat -> Nat -> Constraint
class m >= n
instance m >= Z

Essa implementação exige as extensõesTypeOperators, MultiParamTypeClasses e FlexibleInstances. A primeira permite que criemos tipos/restrições com símbolos não alfanuméricos. A segunda e terceira são para que possamos criar uma typeclass com mais de um parâmetro e para tipos quaisquer. Já as usamos em um post anterior.

Estamos criando uma nova typeclass para comparar dois números naturais com (>=). Ela recebe dois Nat e devolve uma Constraint. Depois de declarada a classe, precisamos definir as instâncias. instance m >= Z é o caso base, já que qualquer número natural é maior ou igual a zero. Vamos adicionar casos extras conforme necessário.

Vamos atualizar agora a função vfilter:

vfilter :: (a -> Bool) -> Vector n a -> ExVector ((>=) n) a
vfilter _ Nil = MkExVector Nil
vfilter p (x :> xs)
  | p x =
    case vfilter p xs of
      MkExVector fTail -> MkExVector (x :> fTail)
  | otherwise = vfilter p xs

Já alteramos a assinatura. Note que ((>=) n) pode até dar a impressão de que estamos dizendo que o resultado deve ser maior do que a entrada mas é só a sintaxe que confunde. Na verdade é parecido com uma seção e seria equivalente a n >= caso isso pudesse ser escrito (note que sintaxe é ligeiramente diferente daquela usada no nível dos termos já que não existem seções no nível dos tipos).

O código acima ainda não funciona. Não há exatamente algo de errado com a ideia, mas o GHC ainda não é capaz de inferir os tipos corretamente. Então vamos dar uma mãozinha usando o mesmo truque que tínhamos usado antes com pattern match no segundo guard.

vfilter :: (a -> Bool) -> Vector n a -> ExVector ((>=) n) a
vfilter _ Nil = MkExVector Nil
vfilter p (x :> xs)
  | p x =
    case vfilter p xs of
      MkExVector fTail -> MkExVector (x :> fTail)
  | otherwise =
    case vfilter p xs of
      MkExVector fTail -> MkExVector fTail

Quase lá! O GHC reclama agora das seguintes afirmações que ele não pode provar:

• Could not deduce ('S n1 >= 'S n2) arising from a use of ‘MkExVector’
• Could not deduce ('S n1 >= n2) arising from a use of ‘MkExVector’

Claro! na nossa declaração de (>=), criamos o caso base de que qualquer número natural é maior ou igual a zero, mas esquecemos de fazer o passo indutivo! Vamos adicionar duas novas instâncias para contar ao GHC que as afirmações acima valem:

type (>=) :: Nat -> Nat -> Constraint
class m >= n
instance m >= Z
instance m >= n => S m >= n
instance m >= n => S m >= S n

Agora temos que se m >= n, então obviamente S m (\(m + 1\)) também é >= n e >= S n.

O que nos leva ao nosso próximo erro. Agora o GHC reclama que há instâncias que se sobrepõem. De fato, para provar que m >= n, a depender do caso, qual instância deve ser escolhida? A última? A penúltima?

• Overlapping instances for 'S n1 >= 'S n2
    arising from a use of ‘MkExVector’
  Matching instances:
    instance (m >= n) => 'S m >= n -- Defined at src/Main.hs:69:10
    instance (m >= n) => 'S m >= 'S n -- Defined at src/Main.hs:70:1

Em geral ter instâncias que se sobrepõem é uma péssima ideia. Não é uma boa ideia pois não está claro qual é a implementação que deverá ser escolhida e portanto isso pode causar um comportamento arbitrário a depender da escolha. Já lidamos com algo parecido num post anterior quando falamos sobre dependências funcionais. No nosso caso, contudo, estamos usando as instâncias para provar um fato, para provar a restrição (>=) que estamos interessados. Mais ainda, a typeclass em questão não implementa nenhum método, ou seja, não há comportamento divergente envolvido. Se a prova feita pelo compilador usar uma instância ou outra pouco importa, ambas são válidas e caso verdadeiras servem igualmente para provar a restrição que nos interessa.

Nestes casos o GHC nos dá uma alternativa! Podemos dizer para ele usar qualquer uma das instâncias que tá tudo certo. Para isso usamos um pragma OVERLAPPING para marcar a instância que sobrepõe a outra (ou OVERLAPPABLE, para indicar que uma instância pode ser ser sobreposta).

Fica assim:

type (>=) :: Nat -> Nat -> Constraint
class m >= n
instance m >= Z
instance m >= n => S m >= n
instance {-# OVERLAPPING  #-} m >= n => S m >= S n

E agora nosso código compila e funciona! \o/

Ele ainda parece estar repetitivo, podemos querer escrever algo assim para deixá-lo mais legível e organizado:

vfilter :: (a -> Bool) -> Vector n a -> ExVector ((>=) n) a
vfilter _ Nil = MkExVector Nil
vfilter p (x :> xs) =
  case vfilter p xs of
    MkExVector ftail -> MkExVector $ if p x
				     then x :> ftail
				     else ftail

Mas isso não funciona! Você sabe explicar porque?

2.3 Finalmente: indexando os elementos

Para indexar o nosso vetor nos vamos precisar de um índice. Não podemos simplesmente usar um inteiro como fazemos com listas e o operador (!!) pois os inteiros vivem no nível dos termos. Queremos ter a garantia de que nunca tentaremos indexar um vetor com um índice inválido. Precisamos de alguma maneira atravessar os limites do nível dos tipos para o nível dos termos e vice-versa!

Nosso vetor foi criado indutivamente. Nossos números indutivamente. Vamos pensar no índice da mesma maneira!

Comecemos pela pergunta: “Como podemos construir um índice válido para um vetor de tamanho n?” Se o vetor tiver S n elementos, então podemos com certeza pegar o 0-ésimo (Regra 1). Esse é o nosso caso base. Se por outro lado tivermos um índice para o i-ésimo elemento de um vetor de tamanho n, podemos então criar um índice para o i+1-ésimo elemento de um vetor com tamanho S n (Regra 2).

Vamos escrever essas regras como um GADT:

type Ix :: Nat -> *
data Ix n where
    IxZ :: Ix (S n)         --  (Regra 1)
    IxS :: Ix n -> Ix (S n) --  (Regra 2)
deriving instance Show (Ix n)

Note que Ix n tem exatamente n habitantes. Veja por exemplo o tipo Ix (S Z) que contém os índices para vetores de tamanho 1. Ix (S Z) deveria ter então exatamente um habitante, e é esse exatamente o caso! IxZ mais especificamente. IxS IxZ não é um habitante válido pois ele tem tipo Ix (S (S m)), para algum m. Não há valor possível de m que permita Ix (S (S m)) ser igual a Ix (S Z).

O real pulo do gato para entender como tudo acima é possível é notar que a mesma expressão IxZ pode ter tipos diferentes.

> IxZ :: Ix (S Z)
IxZ
> IxZ :: Ix (S (S Z))
IxZ

Vamos dar uma olhada em outro exemplo, os valores possíveis de Ix (S (S (S Z))), ou seja, os índices possíveis para vetores de tamanho 3. Se você brincar no GHCI:

> IxZ :: Ix (S (S (S Z)))
IxZ
> IxS IxZ :: Ix (S (S (S Z)))
IxS IxZ
> IxS (IxS IxZ) :: Ix (S (S (S Z)))
IxS (IxS IxZ)
> IxS (IxS (IxS IxZ)) :: Ix (S (S (S Z)))

<interactive>:9:1: error:
    • Couldn't match type ‘'S n0’ with ‘'Z’
      Expected type: Ix ('S ('S ('S 'Z)))
	Actual type: Ix ('S ('S ('S ('S n0))))
    • In the expression: IxS (IxS (IxS IxZ)) :: Ix (S (S (S Z)))
      In an equation for ‘it’:
	  it = IxS (IxS (IxS IxZ)) :: Ix (S (S (S Z)))

Perfeito! O GHCI nos conta que o nosso índice está fora dos limites estabelecidos pelo tipo que definimos. Ele diz inclusive qual o tipo seria necessário para que fosse válido.

É também interessante notar que não há nenhum habitante de Ix Z. Não há como construir um valor deste tipo com os construtores disponíveis no nosso GADT. Essa é a hora de notar a semelhança entre Ix e SNat. Compare as duas definições e onde se diferenciam.

Agora estamos prontos para definir a nossa função (!):

(!) :: Vector n a -> Ix n -> a
(x :> _)  ! IxZ     = x -- Se o índice é 0 então queremos o primeiro elemento
(_ :> xs) ! (IxS i) = xs ! i

-- Compare a implementação acima com a mesma ideia usada em listas e
-- inteiros.
(!) :: [a] -> Int -> a
(x:_)  ! 0 = x
(_:xs) ! n = xs ! (n - 1)

Note que a implementação usando tipos é praticamente igual a uma possível implementação para listas. A diferença, contudo, é a de que a primeira sempre vai ser capaz de devolver o elemento pedido enquanto a baseada em listas pode causar um erro caso o índice passado não seja válido.

Vamos ver em funcionamento! Por conveniência criamos alguns índices para indexar o vetor:

> zero = IxZ
> um = IxS zero
> dois = IxS dois
> dois = IxS um
> tres = IxS dois

E agora podemos criar um vetor e indexá-lo:

> vet = "primeiro" :> "segundo" :> "terceiro" :> Nil
> vet ! zero
"primeiro"
> vet ! um
"segundo"
> vet ! dois
"terceiro"
> vet ! tres

<interactive>:112:7: error:
    • Couldn't match type ‘'S n0’ with ‘'Z’
      Expected type: Ix ('S ('S ('S 'Z)))
	Actual type: Ix ('S ('S ('S ('S n0))))
    • In the second argument of ‘(!)’, namely ‘tres’
      In the expression: vet ! tres
      In an equation for ‘it’: it = vet ! tres

Tudo funciona como queríamos! Fomos capazes de indexar o vetor nos índices zero, um e dois, mas quando tentamos indexar o vetor no índice três recebemos um erro. Você pode perguntar, ora, mas isso não é o que ocorreria numa lista normal? Sim e não! Sim, ocorreria um erro numa lista normal, mas um erro durante a execução! No nosso caso o erro ocorre em tempo de compilação! Veja a saída dizendo que o tipo do índice aceitável para o vetor é Ix (S (S (S Z))) mas que fornecemos um índice de tipo Ix (S (S (S (S n0)))), ou seja, incompatível.

Tudo muito bom e muito bonito. Mas se eu tenho um vetor, eu quero pegar o i-ésimo elemento e i só é conhecido em tempo de execução (por que, por exemplo, é um índice fornecido pelo usuário), como fazemos? Para isso seria preciso de uma função de criação de índices que saiba converter de um Int para um Ix n

Implementar essa função sem alguma maracutaia mágica é bem complicado. O pacote singletons até faz esse tipo de serviço para a gente (apesar de por baixo dos pano usar algumas funções mágicas do GHC).

Para varrer a sujeira pra debaixo do tapete o GHC fornece naturais no nível de tipos de maneira nativa. Ele faz a maracutaia por nós (mas não faz bem feita como veremos abaixo!). Isso quando usado em conjunto com pacotes como o finite-typelits e singletons nos permite expressar (quase tudo) o que queremos.

O código todo usando essa maracutaia institucionalizada do GHC (sem os pacotes acima que merecem de verdade um post só pra eles) fica assim:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.TypeNats
import Numeric.Natural
import Data.Proxy

type Vector :: Nat -> * -> *
data Vector n a where
  Nil :: Vector 0 a
  (:>) :: a -> Vector n a -> Vector (n + 1) a
infixr 5 :>
deriving instance Show a => Show (Vector n a)

Vamos começar pelos imports. GHC.TypeNats contém as definições do kind Nat e algumas operações sobre eles. Atenção, alguns podem conhecer ou acabar encontrando o GHC.TypeLits em suas buscas. Desde o GHC 8.2, é preferível usar o GHC.TypeNats mas a diferença entre eles é que nos TypeLits, o Nat tem toda a interface ligada a Integer enquanto com TypeNats trabalha-se com Numeric.Natural. Como estamos trabalhando com números naturais, Natural é preferível ao Integer por não possuir, por definição, valores negativos. Finalmente Data.Proxy é um velho conhecido que apenas guarda uma variável de tipo e sobre o qual falamos aqui.

Em seguida temos a definição de vetor levemente alterada da nossa definição anterior. Note que aqui estamos usando os Nat do GHC, o que permite que escrevamos n + 1 em lugar de S n ou Vector 0 a em vez de Vector Z a.

Podemos agora criar o nosso novo tipo de índice, Ix que faz duas coisas ao mesmo tempo. A primeira é guardar o tipo de kind Nat como uma variável fantasma. Já a sua definição, ao contrário da que fizemos antes, não é indutiva e simplesmente guarda um número natural. Essa definição de índices conta com um smart constructor e toda a criação de novos indices deve ser feita por ele³. Para indicar isso, o construtor do ADT Ix tem nome UnsafeMkIx (e não deve ser exportado pelo módulo que contém nossa implementação de vetor). Essa combinação smart constructor e tipo fantasma nos traz na prática quase as mesmas garantias que tínhamos com o nosso tipo indutivo, isto é, Ix n tem exatamente n valores distintos possíveis.

type Ix :: Nat -> *
newtype Ix (n :: Nat) = UnsafeMkIx {getIx :: Natural} deriving (Show)

mkIx :: forall n. KnownNat n => Natural -> Maybe (Ix n)
mkIx i
  | i < natVal (Proxy @n) = Just $ UnsafeMkIx i
  | otherwise             = Nothing

O smart constructor mkIx recebe um Natural e devolve um Maybe (Ix n). O sucesso na construção do índice depende do valor i recebido como parâmetro ser pequeno o suficiente para “caber” em um Ix n que serve para indexar vetores de tamanho n. Para verificar se cabe, utilizamos o tipo de retorno n e com a ajuda de um proxy passamos para a função natVal. A funcão natVal é uma das funções mágicas do GHC.

Ela é capaz de devolver o valor, no nível dos termos, correspondente ao tipo, esse no nível dos tipos, utilizado em sua chamada. Para isso ela exige que o tipo n seja da classe KnownNat (o GHC automagicamente implementa uma instância de KnownNat para todos tipos do kind Nat). Neste caso, se o valor n comportar o índice i desejado, um valor do tipo Ix n que contém i é devolvido em um Just. Ela devolve Nothing caso contrário.

Com isso estamos prontos para implementar a nossa função de indexação. A função index é bem parecida com o que fizemos antes, porém usamos o valor contido no Ix para fazer a recursão.

index :: Vector n a -> Ix n -> a
index v ix = go v (getIx ix)
  where
    go :: Vector m a -> Natural -> a
    go (x :> _)  0 = x
    go (_ :> xs) i = go xs (i - 1)
    go Nil _ = undefined -- nunca vai chegar aqui pois Ix 0 não é
			 -- habitado

Pelo fato de estarmos usando naturais que não possuem uma construção indutiva em Haskell, somos obrigados (mesmo que seja impossível) a escrever o último pattern match da função go para vetores vazios. Esse caso nunca ocorrerá pois Ix 0, apesar de ser um tipo válido, não possui nenhum termo. É desabitado (garantido pelo nosso smart constructor).

E finalmente chegamos à cereja do bolo! A função de indexação (!) que dado um vetor e um inteiro devolve (talvez) um valor naquele índice. Caso queiramos um código seguro aqui é inevitável o uso de Maybe, já que não há controle algum sobre o índice inteiro recebido e ele pode muito bem ser negativo ou maior que o tamanho do vetor.

intToNatural :: Int -> Maybe Natural
intToNatural x
  | x >= 0    = Just $ fromIntegral x
  | otherwise = Nothing

(!) :: KnownNat n => Vector n a -> Int -> Maybe a
v ! i = index v <$> (intToNatural i >>= mkIx)

E tudo funciona como esperado:

> vet = "primeiro" :> "segundo" :> "terceiro" :> Nil
> vet ! 2
Just "terceiro"
> vet ! 1
Just "segundo"
> vet ! 0
Just "primeiro"
> vet ! 4
Nothing
> vet ! (-1)
Nothing

2.4 Manhê, posso inserir na árvore agora?

Agora que aprendemos sobre tipos existenciais o leitor atento deve estar se perguntando: “Será que isso me permite usar a função insertI para inserir elementos na minha árvore? Felizmente a resposta é positiva!

O que precisamos fazer é exatamente a mesma coisa que fizemos com os vetores, temos que criar um tipo que esquece o parâmetro de profundidade da árvore prometendo que vou aplicar funções nessa estrutura que funcionam para qualquer n.

data SomeTree a where
  SomeTree :: forall a n . ITree a n -> SomeTree a

A estrutura SomeTree fala justamente isso: “eu posso receber uma ITree com qualquer tipo a e n, porém, vou me lembrar apenas da informação de tipo a”.

Com isso, podemos criar a seguinte função:

insertST :: a -> SomeTree a -> SomeTree a
insertST x (SomeTree t) = case insertI x t of
			    NoChange t' -> SomeTree t'
			    AddOne   t' -> SomeTree t'

Note que isso funciona pois a entrada e saída da função deve casar apenas o tipo a. O tipo n, da profundidade da árvore, não importa para a função. Ainda assim, dentro da definição da função, quando extraímos a árvore t e aplicamos a função insertI, temos todas as garantias conquistadas na definição do tipo ITree, mesmo que SomeTree esqueça quem é n, ele não permitirá a construção de uma árvore inválida.

O ponto negativo é que estamos presos dentro de SomeTree, mas isso não é um problema contanto que a gente disponibilize todas as funções necessárias para o usuário:

depthST :: SomeTree a -> Int
depthST (SomeTree t) = depthI t

mirrorST :: SomeTree a -> SomeTree a
mirrorST (SomeTree t) = SomeTree (mirrorI t)

topST :: SomeTree a -> Maybe a
topST (SomeTree ILeaf) = Nothing
topST (SomeTree t)     = Just $ topI t

Aqui temos alguns problemas, primeiro que depthI depende que n faça parte da classe NatToInt, podemos garantir isso alterando a definição de SomeTree:

data SomeTree a where
  SomeTree :: forall a n . NatToInt n => ITree a n -> SomeTree a

O outro problema é que topI só funciona para tipos S n e não temos como garantir isso, pois esquecemos quem é n, portanto precisamos reimplementar a função top como:

topST :: SomeTree a -> Maybe a
topST (SomeTree t) = topmI t
  where
    topmI :: ITree a n -> Maybe a
    topmI ILeaf           = Nothing
    topmI (INode _ x _ _) = Just x

Uma alternativa é definir SomeTree para árvores não-vazias:

data SomeTree a where
  SomeTree :: forall a n . NatToInt n => ITree a (S n) -> SomeTree a

E com isso podemos definir:

depthST :: SomeTree a -> Int
depthST (SomeTree t) = depthI t

mirrorST :: SomeTree a -> SomeTree a
mirrorST (SomeTree t) = SomeTree (mirrorI t)

topST :: SomeTree a -> a
topST (SomeTree t) = topI t

Para usar o tipo SomeTree na prática, precisamos criar uma função que, partindo de um valor, cria uma árvore não-vazia:

singletonST :: a -> SomeTree a
singletonST x = SomeTree $ INode ILeaf x ILeaf E

t = foldr singletonST (singletonST 1) [2 .. 10]

3 Referências

• https://en.wikibooks.org/wiki/Haskell/GADT
• https://www.cl.cam.ac.uk/teaching/1415/L28/gadts.pdf
• https://www.morrowm.com/posts/2021-08-02-shoes.html
• https://doisinkidney.com/posts/2018-07-30-verified-avl.html
• https://is.muni.cz/el/fi/jaro2017/IA014/um/08-gadt.pdf

4 Disclaimer

Estes slides foram preparados para os cursos de Paradigmas de Programação e Desenvolvimento Orientado a Tipos na UFABC.

Este material pode ser usado livremente desde que sejam mantidos, além deste aviso, os créditos aos autores e instituições.