Types, Kinds, Sorts…

Veja a playlist no Youtube com todos os vídeos do curso.

1 Tipo assim…

No post onde discutimos o que são tipos, deixamos claro (esperamos!) que todos os valores de um programa que passamos como parâmetros, armazenamos em variáveis, etc… possuem um tipo. Também vimos que os tipos (types) podem ser vistos como conjuntos de valores relacionados e que um valor também é ocasionalmente chamado de termo (term). Exemplos de tipos incluem, por exemplo, Int, Float, Maybe Int, [String], … cada um representando um conjunto (potencialmente infinito) de termos possíveis.

Podemos verificar os tipos de termos no GHCI usando o comando :type / :t:

Prelude> :t 10
10 :: Num p => p
Prelude> :t "Olá"
"Olá" :: [Char]
Prelude> :t ["Balela"]
["Balela"] :: [[Char]]
Prelude> :t (+)
(+) :: Num a => a -> a -> a

Se o conjunto dos termos relacionados são colocados em conjuntos que chamamos de tipos, será que faz sentido também colocarmos os tipos em conjuntos?

2 Kinds

De fato faz! Conjuntos que contém tipos são chamados de kinds . De maneira grosseira podemos enxergar um kind como sendo o “tipo dos tipos”.

Uma outra metáfora que podemos utilizar é a de etiquetas. Podemos etiquetar cada um dos termos com o seu tipo (5/inteiro, 3.1415/número fracionário, "oba oba"/string). Seguindo essa metáfora, kinds nada mais são do que as etiquetas dos tipos.

A figura abaixo tenta descrever de uma maneira gráfica essa relação:

O GHCI nos permite verificar o kind de um tipo usando o comando :kind / :k :

Prelude> :k Int
Int :: *
Prelude> :k String
String :: *
Prelude> data Cor = Amarelo | Azul | Verde | Vermelho
Prelude> :k Cor
Cor :: *

Todos os tipos que contém algum valor, sem exceção, são do kind *. Quando um tipo contém valores ele é chamado de habitado (inhabited). Contudo, nem todos os tipos de kind * são habitados. Por exemplo, o tipo Void, definido simplesmente como data Void, não tem nenhum valor.

Ok, mentimos! Mas foi por um bom motivo. Logo na caixinha acima dissemos que todos os tipos habitados são do kind *. Isso é meio que verdade para Haskell padrão: * é o kind de todos os tipos habitados (ou em outra terminologia, Boxed ou ainda lifted types ). Contudo, esse navio já zarpou faz tempo. É raríssimo usarmos o Haskell padrão sem nenhuma extensão do GHC que é o padrão Haskell de fato. É também o padrão que usamos nestes posts (caso você ainda não tivesse percebido pelo número de extensões que utilizamos 😛).
No GHC há também outros tipos habitados que não são do kind * que são os tipos unboxed ou unlifted . Por convenção tais tipos terminam com # (chamado de magic hash). Em geral são usados para evitar custos em tempo de execução que a representação padrão de Haskell para estes tipos teria. Nós não vamos nos aprofundar neste assunto (por enquanto!). [1]

Mas pera lá! Que doidera é esse *? Primeiramente vamos deixar claro que * não tem nada a ver com a função multiplicação ou ainda com um caractere coringa. * (lê-se type ) é o kind de todos os construtores de tipos nulários (nullary type constructors).

Vamos por partes.

Pode facilitar o entendimento pensar que um construtor de tipos é simplesmente função que atua no nível dos tipos. Enquanto funções normais atuam no nível dos termos (ou seja, recebem termos como entrada e devolvem um termo como saída) construtores de tipos recebem tipos como entrada e devolvem um tipo como saída. Veremos mais adiante quando falarmos sobre type families como podemos criar funções arbitrárias (não apenas construtores de tipos) que atuam no nível dos tipos.

A aridade (arity) de uma função é simplesmente o número de argumentos/parâmetros que ela recebe. Qualquer aridade \(\ge 0\) é possível e algumas aridades recebem nomes especiais:

  • 0 \(\to\) Nulária: zero parâmetro (f = 42) que, na ausência de efeitos colaterais (nosso caso), devolvem constantes
  • 1 \(\to\) Unária: Exemplo: not
  • 2 \(\to\) Binária: Exemplo: (+)
  • 3 \(\to\) Ternária: Exemplo: foldl

Construtor de tipos nulário quer dizer, simplesmente, que é um construtor de tipos que não recebe parâmetro nenhum. Int é um tipo por si só, assim como String e Cor.

Assim, quando declaramos uma função foo:

foo :: Int -> String -> Cor
foo _ _ = _

Int não precisa de mais nada para devolver um tipo válido, assim como String ou Cor, logo a assinatura de tipos de foo está completa.

A próxima pergunta que deve estar martelando na sua cabeça é: muito bem, e os construtores de tipos não nulários? Qual é o kind deles?

Vamos considerar e investigar os tipos abaixo:

type Nome = String
data Fisica
data Juridica
data Pessoa t = Pessoa Nome

No GHCI:

Prelude> :k Nome
Nome :: *
Prelude> :k Fisica
Fisica :: *
Prelude> :k Juridica
Juridica :: *
Prelude> :k Pessoa
Pessoa :: * -> *

Nome é simplesmente um sinônimo para o tipo String que por sua vez também é um sinônimo para o tipo [Char]. Nenhuma surpresa, não é preciso de nenhum parâmetro de tipo extra para criar um tipo destes. O mesmo vale para Fisica e Juridica que são ADTs simplões e não habitados.

O interessante aparece no tipo Pessoa. Notem que para criar um tipo Pessoa é necessário passar um parâmetro de tipo t, e só assim teremos o tipo completo!

-- Funciona como esperado!
criaFisica :: Nome -> Pessoa Fisica
criaFisica = Pessoa

-- Esse aqui também
criaEmpresa :: Nome -> Pessoa Juridica
criaEmpresa = Pessoa

-- Isso aqui também é válido! Neste caso o contexto da chamada
-- determina quem é `a`
criaPessoa :: Nome -> Pessoa a
criaPessoa = Pessoa

Mas isso aqui, vai dar um erro:

-- Isso aqui dá erro!
-- o tipo não está completo!
criaErrado :: Nome -> Pessoa
criaErrado = Pessoa
• Expecting one more argument to ‘Pessoa’
  Expected a type, but ‘Pessoa’ has kind ‘* -> *’
• In the type signature: criaErrado :: Nome -> Pessoa

O que o compilador está tentando nos dizer é o seguinte: para definir a assinatura de uma função (ou de maneira geral definir o tipo de algum termo) esperamos que o kind de tal tipo seja *. O kind de Pessoa é * -> *, portanto não bate com o que esperávamos e o programa é rejeitado. Pessoa é um construtor de tipos unário (isto é, recebe um parâmetro). Outros exemplos notáveis de construtores unários:

Prelude> :k []
[] :: * -> *
Prelude> :k Maybe
Maybe :: * -> *

A lista ([]) é um exemplo interessante pois ela conta também com um açúcar sintático específico por ser algo tão comumente utilizado. O parâmetro de tipos no caso da lista é o tipo dos elementos que ela conterá. No Maybe, que pode ser definido como data Maybe a = Just a | Nothing, pode ser notado mais claramente que a variável de tipos a é o parâmetro indicado pelo primeiro * do seu kind. Novamente a indica o tipo do elemento encerrado no valor do Maybe.

Exemplos notáveis de construtores de tipos binários incluem:

Prelude> :k Either
Either :: * -> * -> *
Prelude> :k (,)
(,) :: * -> * -> *
Prelude> :k (->)
(->) :: * -> * -> *

Assim como existem as funções de alta ordem / higher order functions (ou como alguns preferem traduzir: funções de ordem superior), também podemos ter higher-kinded types, ou tipos de alto kind/ tipos de kinds superiores.

O tipo data Dummy a f = MkDummy a (f a) é um exemplo. Ele recebe a do kind * e f que tem kind * -> *. Note que apesar de não termos especificado os kinds de a nem de f, o inferidor do compilador faz o trabalho para nós e atribui o kind correto automaticamente.

Either pode definido como data Either a b = Left a | Right b. As variáveis de tipo a e b aqui são do kind * que pode ser visto no kind do construtor Either. A tupla com dois elementos, ou simplesmente um par, assim como a lista, conta com um açúcar sintático especial. Mas não é, na sua essência, muito diferente do Either.

Agora (->), este sim é um caso a parte!

2.1 O kind (->)

Podemos obter algumas informações adicionais sobre (->) usando o comando :info do GHCI:

Prelude> :i (->)
type (->) :: * -> * -> *
data (->) a b
	-- Defined in ‘GHC.Prim’
infixr -1 ->
instance Applicative ((->) r) -- Defined in ‘GHC.Base’
instance Functor ((->) r) -- Defined in ‘GHC.Base’
instance Monad ((->) r) -- Defined in ‘GHC.Base’
instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
instance Semigroup b => Semigroup (a -> b) -- Defined in ‘GHC.Base’

Funções, assim como inteiros, strings e pessoas são um tipo! Ora, se podemos guardar funções em variáveis e passar funções como parâmetros para outras funções elas precisam viver no nível dos termos (ou seja são valores) e portanto possuem um tipo! O construtor de tipo de uma função é escrito (->). O comando :info inclusive nos conta que há instâncias de algumas typeclasses para este tipo como Functor, Monoid, …

Vejamos o exemplo de uma função unária:

Prelude> :t not
not :: Bool -> Bool
Prelude> :k (->)
(->) :: * -> * -> *

O primeiro Bool encaixa com o primeiro *, o segundo Bool encaixa com o segundo * e sobra um *, ou seja um tipo do kind *. Perfeito!

O que significa então a função ter uma sequência dessas setas encadeadas? Por exemplo:

Prelude> :t (&&)
(&&) :: Bool -> Bool -> Bool

Não estaria sobrando um parâmetro por aí? (como compila, obviamente não! 🤣) Se você reparar com um pouco mais de cuidado nas informações obtidas com o comando :info do GHCI, vai notar que tem uma linha aparentemente inocente que diz: infixr -1 ->. Isso significa que (->) é um operador infixo, associativo à direita e com precedência -1. Em outras palavras, isso quer dizer que as seguintes coisas são equivalentes:

foo :: a -> b -> c -> d -> e
foo :: a -> (b -> c -> d -> e)
foo :: a -> (b -> (c -> d -> e))
foo :: a -> (b -> (c -> (d -> e))

De fato, se vc perguntar pro GHCI, ele vai te contar exatamente isso:

Prelude> :t undefined :: a -> (b -> (c -> (d -> e)))
undefined :: a -> (b -> (c -> (d -> e))) :: a -> b -> c -> d -> e

Note como os parênteses são eliminados!

Esse é o pulo do gato para aplicações parciais de construtores de tipos! (e de função!) Conceitualmente todos os construtores de tipos (e as funções) em Haskell recebem um único parâmetro! Se é preciso de mais de um parâmetro para chegar em algo útil, a primeira aplicação devolve um tipo de um kind * -> ... -> * que quando aplicado repetidamente devolve finalmente a resposta quando sobrar apenas um *.

Em Haskell o kind *, lido type, também pode ser escrito Type. Apesar de frequentemente ser escrito como * e ser o formato de saída padrão relatado pelo GHCI, ele vem pouco a pouco caindo em desuso. Para novos códigos prefira usar Type ainda que usar * vá funcionar perfeitamente por algum tempo.
Para fazer uso do símbolo Type, é necessário importar o módulo Data.Kind do pacote base.

Podemos, agora que descobrimos que há alguns kinds diferentes de *, atualizar a nossa figura:

2.2 O kind Constraint

Já discutimos bastante coisa sobre o que está à direita do => em uma assinatura de tipos. E quanto ao que vem à esquerda? Será que são tipos? Vamos ver o que o GHCI nos conta a respeito:

Prelude> :t Show

<interactive>:1:1: error:
    • Data constructor not in scope: Show
    • Perhaps you meant variable ‘show’ (imported from Prelude)
Prelude> :k Show
Show :: * -> Constraint

Hum… Show não é um tipo, tanto que o GHCI reclama. Mas podemos olhar o kind de Show que é * -> Constraint. Ou seja, ele espera um tipo como parâmetro e nos devolve uma Constraint. Vamos passar um tipo e ver o que acontece:

Prelude> :k Show String
Show String :: Constraint

Legal! Então para as typeclasses como Show que recebem um único parâmetro, se fornecermos um tipo temos como resposta uma Constraint completa.

Vamos dar uma olhada em um outro caso mais elaborado, o Functor:

Prelude> :k Functor
Functor :: (* -> *) -> Constraint

O (* -> *) está nos dizendo que para obtermos uma Constraint para Functor, precisamos fornecer um construtor de tipos de kind * -> *. Vamos fazer uns testes:

Prelude> :k Int
Int :: *
Prelude> :k Functor Int

<interactive>:1:9: error:
    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
    • In the first argument of ‘Functor’, namely ‘Int’
      In the type ‘Functor Int’
Prelude> :k Maybe
Maybe :: * -> *
Prelude> :k Functor Maybe
Functor Maybe :: Constraint
Prelude> :k []
[] :: * -> *
Prelude>
Prelude> :k Functor []
Functor [] :: Constraint

Não somos capazes de criar um Functor para Int, pois Int não é um tipo paramétrico. O seu kind (*) não bate com o esperado pelo Functor. Por outro lado Maybe e [] estão aptos, já que são tipos paramétricos.

Vamos pegar como exemplo o caso da implementação de um Functor para uma lista que só aceita elementos que possam ser transformados em strings, ou seja que obedeçam a restrição Show. Vamos começar definindo tal lista e uma função mapLista (essa implementação usa a sintaxe GADTs que é explicada com muito mais detalhes neste post):

{-# LANGUAGE GADTs #-}
-- Tipo ListaShow exige que os elementos sejam da classe show. A
-- maneira mais fácil de fazer isso é através de GADTs que permitem
-- declararmos os construtores de tipos como se fossem funções e,
-- portanto, permitem que incluamos as restrições desejadas.
data ListaShow a where
  ListaShow :: Show a => [a] -> ListaShow a

mapLista :: Show b => (a -> b) -> ListaShow a -> ListaShow b
mapLista f (ListaShow xs) = ListaShow (fmap f xs)

A definição de ListaShow indica que ela é um tipo paramétrico que possui um construtor, chamado também de ListaShow que recebe uma lista do tipo [a] e retorna o tipo ListaShow a. Além disso, especificamos que o tipo a não pode ser qualquer tipo, ele deve ter uma instância de Show. Por exemplo, podemos criar um ListaShow fazendo:

xs = ListaShow [1, 2, 3, 4] :: ListaShow Int

Esse tipo nada mais é que uma caixa que guarda listas de valores de tipos com a restrição Show. Para poder criar um tipo seguindo tal sintaxe, precisamos habilitar a extensão de compilador GADTs.

A implementação de mapLista é simplesmente uma casca em cima do Functor de listas. Ela tira a lista de dentro de ListaShow, aplica a função, e recoloca a lista dentro. Note que a função mapLista tem uma restrição de que o tipo de retorno da função a ser mapeada seja Show, pois de outra forma não conseguiríamos recolocar os resultados na ListaShow.

Vamos tentar implementar uma instância de Functor para ListaShow, se conseguirmos, podemos definir mapLista = fmap.

instance Functor ListaShow where
  fmap f (ListaShow xs) = ListaShow (fmap f xs)

O que nos dá o seguinte erro:

• Could not deduce (Show b) arising from a use of ‘ListaShow’
      from the context: Show a
	bound by a pattern with constructor:
		   ListaShow :: forall a. Show a => [a] -> ListaShow a,
		 in an equation for ‘fmap’
	at src/Main.hs:11:11-22
      Possible fix:
	add (Show b) to the context of
	  the type signature for:
	    fmap :: forall a b. (a -> b) -> ListaShow a -> ListaShow b
    • In the expression: ListaShow (fmap f xs)
      In an equation for ‘fmap’:
	  fmap f (ListaShow xs) = ListaShow (fmap f xs)
      In the instance declaration for ‘Functor ListaShow’
   |
11 |   fmap f (ListaShow xs) = ListaShow (fmap f xs)
   |                           ^^^^^^^^^^^^^^^^^^^^^

O compilador não deixa. Ele diz que a função f precisa ter a restrição Show b (assim como precisamos adicionar a mesma restrição no nosso mapLista). Mas não podemos mudar a definição de f, ela é dada na classe Functor e diz que a função f deve funcionar para todo b, e não só para os Show b.

Esse é exatamente o mesmo problema que afeta o tipos de bibliotecas muito populares de Haskell, como o Data.Set que exige que os elementos contidos dentro dele sejam da classe Ord. Data.Set não tem uma instância de Functor mas tem uma função map :: Ord b => (a -> b) -> Set a -> Set b que serve exatamente o mesmo propósito (assim como a nossa mapLista).

Idealmente poderíamos criar uma classe FunctorPlus definida como:

class FunctorPlus c f where
  fmaplus :: c b => (a -> b) -> f a -> f b
## Olhando para a definição de `FunctorPlus` quais são os _kinds_ de `c` e `f`? ```haskell class FunctorPlus c f where fmaplus :: c b => (a -> b) -> f a -> f b ``` > Preste atenção ao uso de `c` e `f` no método `fmaplus`. Qual _kind_ permite seu uso conforme a assinatura de tipos dessa função? 1. [X] `c :: * -> Constraint`, `f :: * -> *` > Pois `c` recebe um tipo e retorna se ele faz parte dessa classe, e `f` pois é um tipo paramétrico. 1. [ ] `c :: Int, f :: [a]` 1. [ ] `c :: *, f :: * -> *` 1. [ ] `c :: * -> Type, f :: Type -> Type`

Comecemos pela definição da classe FunctorPlus. Ela recebe dois parâmetros, c e f. c é do kind * -> Constraint, e f do kind * -> *. f é exatamente igual ao kind recebido pelo Functor padrão, ou seja, um tipo paramétrico. Já c é o kind que queremos restringir! Note que ele bate com o kind de Show e Ord por exemplo:

Prelude> :k Show
Show :: * -> Constraint
Prelude> :k Ord
Ord :: * -> Constraint

Ou seja, c poderia ser Show ou Ord ou Num ou qualquer outra classe que gostaríamos para nossa instância de FunctorPlus. Se isso for possível poderíamos criar uma instância instance FunctorPlus Show ListaShow.

A declaração do método fmaplus é simples, mas tem alguns elementos novos. Primeiramente estamos usando variáveis para a restrição c e aplicando ela ao tipo b (c b =>), em seguida o tipo da função é o que já estamos acostumados e idêntica ao Functor padrão.

Porém, esse código ainda não funciona e vai causar um erro indicando que precisamos habilitar a extensão MultiParamTypeClasses pois nossa classe possui dois parâmetros de tipos. Na verdade, não precisaremos dessa extensão, porém vamos habilitá-la por enquanto para satisfazer o compilador (a partir desse ponto, vamos escrever o código completo para compararmos passo a passo como ele se desenvolve):

{-# language GADTs #-}
{-# language MultiParamTypeClasses #-}

data ListaShow a where
  ListaShow :: Show a => [a] -> ListaShow a

mapLista :: Show b => (a -> b) -> ListaShow a -> ListaShow b
mapLista f (ListaShow xs) = ListaShow (fmap f xs)

class FunctorPlus c f where
  fmaplus :: c b => (a -> b) -> f a -> f b

Agora o compilador reclama que o uso de Constraints na nossa definição é ilegal:

   • Illegal constraint: c b (Use ConstraintKinds to permit this)
• When checking the class method:
    fmaplus :: forall (c :: * -> Constraint) (f :: * -> *) b a.
	       (FunctorPlus c f, c b) =>
	       (a -> b) -> f a -> f b
  In the class declaration for ‘FunctorPlus’

E, ele sugere habilitar a extensão ConstraintKinds para que isso seja permitido:

{-# language GADTs #-}
{-# language MultiParamTypeClasses #-}
{-# language ConstraintKinds #-}

data ListaShow a where
  ListaShow :: Show a => [a] -> ListaShow a

mapLista :: Show b => (a -> b) -> ListaShow a -> ListaShow b
mapLista f (ListaShow xs) = ListaShow (fmap f xs)

class FunctorPlus c f where
  fmaplus :: c b => (a -> b) -> f a -> f b

Ainda assim, recebemos um erro complicado para entender:

• Could not deduce: c0 b
  from the context: (FunctorPlus c f, c b)
    bound by the type signature for:
	       fmaplus :: forall (c :: * -> Constraint) (f :: * -> *) b a.
			  (FunctorPlus c f, c b) =>
			  (a -> b) -> f a -> f b

Antes de resolver esse problema, vamos tentar especificar claramente na nossa classe do que se trata cada parâmetro de tipo. Para isso precisamos habilitar a extensão KindSignatures e importar a palavra-chave Constraint do módulo Data.Kind:

{-# language GADTs #-}
{-# language MultiParamTypeClasses #-}
{-# language ConstraintKinds #-}
{-# language KindSignatures #-}

import Data.Kind (Constraint)

data ListaShow a where
  ListaShow :: Show a => [a] -> ListaShow a

mapLista :: Show b => (a -> b) -> ListaShow a -> ListaShow b
mapLista f (ListaShow xs) = ListaShow (fmap f xs)

class FunctorPlus (c :: * -> Constraint) (f :: * -> *) where
  fmaplus :: c b => (a -> b) -> f a -> f b

Ainda assim, o erro permanece… O que o compilador está reclamando é que pode existir ambiguidade na relação entre os parâmetros c e f. Por exemplo, se eu fizer fmaplus f (ListaShow [1,2,3,4]) como o compilador determinaria a instância de FunctorPlus? Para nós pode ser claro que ele deveria instanciar c :: Show, f :: ListaShow, mas o que impede de alguém criar uma instância FunctorPlus Ord ListaShow? Nesse caso o compilador não tem como saber o que escolher! Para resolver essa situação, habilitamos a extensão FunctionalDependencies e alteramos nosso código para (agora podemos remover a extensão MultiParamTypeClasses):

{-# language GADTs #-}
{-# language FunctionalDependencies #-}
{-# language ConstraintKinds #-}
{-# language KindSignatures #-}

import Data.Kind (Constraint)

data ListaShow a where
  ListaShow :: Show a => [a] -> ListaShow a

mapLista :: Show b => (a -> b) -> ListaShow a -> ListaShow b
mapLista f (ListaShow xs) = ListaShow (fmap f xs)

class FunctorPlus (c :: * -> Constraint) (f :: * -> *) | f -> c where
  fmaplus :: c b => (a -> b) -> f a -> f b

A dependência funcional é composta por tudo que vem depois do pipe |, ou seja, f -> c. O que isso está dizendo para o compilador é:

Caro Senhor Compilador,

Espero que esteja bem.

Estava declarando minha nova typeclass e pensei que, talvez, você pudesse ter dificuldades em determinar qual instância, e portanto qual implementação de fmaplus, usar de um determinado contexto.

Por exemplo, se tivermos as instâncias instance FunctorPlus Ord [] e instance FunctorPlus Eq [] e eu tentar aplicar fmaplus (+1) [1..5], qual você escolheria?

Logo, inclui uma dependência funcional f -> c dizendo que uma vez que você souber quem é f você também sabe quem é c. Ou seja, f determina c e se no meu código eu fizer algo como acima (onde f serviria em dois c diferentes), você pode rejeitar meu programa!

Muito grato!

Finalmente, para completar, vamos criar uma instância de Show para nosso ListaShow…ou melhor, deixa o compilador se virar:

{-# language GADTs #-}
{-# language FunctionalDependencies #-}
{-# language ConstraintKinds #-}
{-# language KindSignatures #-}
{-# language StandaloneDeriving #-}

import Data.Kind (Constraint)

data ListaShow a where
  ListaShow :: Show a => [a] -> ListaShow a
deriving instance Show (ListaShow a)

mapLista :: Show b => (a -> b) -> ListaShow a -> ListaShow b
mapLista f (ListaShow xs) = ListaShow (fmap f xs)

class FunctorPlus (c :: * -> Constraint) (f :: * -> *) | f -> c where
  fmaplus :: c b => (a -> b) -> f a -> f b

A extensão StandaloneDeriving permite que o compilador crie certas instâncias de classes para o dev cansado.

Vamos ver como as instâncias de FunctorPlus para nossos tipos podem ser definidas.

instance FunctorPlus Show ListaShow where
  fmaplus f (ListaShow xs) = ListaShow (fmap f xs)

instance FunctorPlus Ord Set where
  fmaplus = Set.map

A declaração das instâncias fornece um kind do tipo correto (Show ou Ord) para a restrição, além de um construtor de tipos unário. Aí a implementação fica simples, no caso de ListaShow é a mesma que tínhamos feito antes e no caso do Set apenas chamamos a função que já estava pronta. Note que não precisamos mais incluir manualmente a restrição Show e Ord, já que isso já está na própria declaração da instância.

Agora podemos fazer:

Prelude> :t fromList [1..10]
fromList [1..10] :: (Ord a, Num a, Enum a) => Set a
Prelude> fmaplus (*2) (fromList [1..10])
fromList [2,4,6,8,10,12,14,16,18,20]
Prelude> fmaplus (*2) (ListaShow [1..10])
ListaShow [2,4,6,8,10,12,14,16,18,20]

Legal! Tudo funcionando para Set e ListaShow. Mas para ser realmente um FunctorPlus ele também precisa funcionar para outros tipos que usamos cotidianamente como functores!

Vamos tentar implementar para a lista:

instance FunctorPlus ??? [] where
  fmaplus = fmap

O que devemos colocar no local da constraint? A lista não tem restrição alguma com relação aos seus tipos, que restrição poderíamos colocar que faria sentido? Bom, podemos criar a nossa própria restrição que vale para todos os tipos!

class NullConstraint a
instance NullConstraint a

Criamos a typeclass NullConstraint que não tem nenhum método, nem nenhuma superclasse. Em seguida definimos uma instância de NullConstraint para todas os tipos a, sejam eles quais forem. Ou seja, qualquer tipo tem, a partir deste momento, uma instância de NullConstraint. Para fazer esse tipo de declaração é preciso utilizar a extensão FlexibleInstances que permite que criemos instâncias para tipos arbitrários.

Com essa typeclass agora podemos fazer:

instance FunctorPlus NullConstraint [] where
  fmaplus = fmap

E tudo funciona como esperado:

Prelude> fmaplus (*2) [1..10]
[2,4,6,8,10,12,14,16,18,20]

Podemos agora, mais uma vez, atualizar a nossa árvore hierárquica!

3 Sorts e a BOX

Quando observamos a última figura, fica uma pulguinha atrás da orelha que nos leva à natural pergunta: se pegamos termos e colocamos eles em conjuntos chamados de tipos e depois pegamos esses tipos e colocamos eles em conjuntos chamados kinds. Por que não pegar os kinds e colocá-los em um novo conjunto? 😎

De fato, existe essa ideia e os conjuntos que reunem os kinds são chamados de sorts . Em Haskell todos os kinds são reunidos em um único sort chamado BOX. Esse nome aparece aqui e ali na documentação do GHC e de algumas bibliotecas normalmente sem muita explicação. Por outro lado, outras linguagens de programação como Coq e Agda permitem (com algumas limitações) modelar uma hierarquia de profundidade arbitrária. A discussão deste assunto terá que ficar para uma outra ocasião. Já a figura com o BOX está logo aqui!

Bom, pelo menos era como as coisas funcionavam. 🤣 Houve há algum tempo (~2015) uma proposta para simplificar o sistema de tipos de Haskell (já disponível nas versões mais recentes) que tenta unificar tipos e kinds. A wiki dos desenvolvedores do GHC traz uma visão mais detalhada do que foi feito e o paper por Weirich [3] tem os detalhes sórdidos. O detalhamento das ideias contidas nessa implementação foge ao escopo deste material e não é necessária para seguir o resto destes posts.

4 Promoção de tipos

Vamos retomar um exemplo do início deste post.

type Nome = String
data Fisica
data Juridica
data Pessoa t = Pessoa Nome

Isso nos permite, usando um tipo fantasma, ter efetivamente dois tipos diferentes, um para pessoas físicas e outro para pessoas jurídicas. Uma função pode, então, aceitar qualquer tipo de pessoa ou um dos tipos específicos:

todoMundoEBemVindo :: Pessoa a -> Nome
todoMundoEBemVindo (Pessoa nome) = nome

apenasPessoasFisicas :: Pessoa Fisica -> Nome
apenasPessoasFisicas (Pessoa nome) = nome

apenasPessoasJuridicas :: Pessoa Juridica -> Nome
apenasPessoasJuridicas (Pessoa nome) = nome

Muito bom! Mas, infelizmente, tal abordagem também permite que façamos:

ráPegadinhaDoMallandro :: Pessoa Float -> Nome
ráPegadinhaDoMallandro = ???

Queremos evitar que isso seja possível ou, em outras palavras, queremos isso cause um erro. Solução tradicional:

type Nome = String
data Pessoa = Juridica Nome | Fisica Nome

todoMundoEBemVindo :: Pessoa -> Nome
todoMundoEBemVindo (Fisica nome) = nome
todoMundoEBemVindo (Juridica nome) = nome

apenasPessoasFisicas :: Pessoa -> Nome
apenasPessoasFisicas (Fisica nome) = nome
apenasPessoasFisicas (Juridica _) = error "Não aceitamos empresas"

apenasPessoasJuridicas :: Pessoa -> Nome
apenasPessoasJuridicas (Juridica nome) = nome
apenasPessoasJuridicas (Fisica _) = error "Apenas empresas"

Agora a função ráPegadinhaDoMallandro fica impossível de se implementar. Os pattern matches possíveis são apenas dois, Fisica e Juridica. Qualquer outra coisa causará um erro de compilação. A parte ruim desta solução é que ela tem custos durante a execução. Toda vez que as funções forem chamadas, cada um dos casos deverá ser verificado o que é uma perda de tempo (e que aliás, foi justamente por isso que utilizamos os tipos fantasmas para começo de conversa). Além disso elas explodem apenas durante a execução do programa! Queremos uma solução que pegue este tipo de problema durante a compilação!.

Uma segunda (tentativa) alternativa é usando typeclasses/constraints e a extensão GADTs:

type Nome = String
data Fisica
data Juridica

class PessoaTipo t
instance PessoaTipo Fisica
instance PessoaTipo Juridica

data Pessoa t where
  Pessoa :: PessoaTipo t => Nome -> Pessoa t

criaFisica :: Nome ->  Pessoa Fisica
criaFisica = Pessoa

criaJuridica :: Nome -> Pessoa Juridica
criaJuridica = Pessoa

todoMundoEBemVindo :: Pessoa a -> Nome
todoMundoEBemVindo (Pessoa nome) = nome

apenasPessoasFisicas :: Pessoa Fisica -> Nome
apenasPessoasFisicas (Pessoa nome) = nome

apenasPessoasJuridicas :: Pessoa Juridica -> Nome
apenasPessoasJuridicas (Pessoa nome) = nome

Agora o nosso código está protegido (já durante a compilação) e funções como o ráPegadinhaDoMallandro apesar de poderem ser implementadas, nunca poderão ser chamadas. Veja:

ráPegadinhaDoMallandro :: Pessoa Float -> Nome
ráPegadinhaDoMallandro (Pessoa nome) = nome

Essa função nunca vai poder ser chamada pois ela espera um Pessoa Float. Mas é impossível criar um valor com este tipo já que o único construtor de valores de Pessoa recebe um parâmetro de tipo t que precisa ser uma instância de PessoaTipo. Como as duas únicas instâncias desta classe são Fisica e Juridica, não tem como cair na pegadinha. É preciso amarrar com cuidado o que é exportado do módulo onde a typeclass é criada pois senão o Mallandro do lado de fora simplesmente vai lá e cria uma instância pra Float. Esse é o mesmo cuidado que deve se tomar quando usamos tipos fantasmas em geral.

Está melhor! Mas queremos mais! Queremos fazer com que o compilador nem permita que tais funções “inchamáveis” sejam criadas. O que podemos fazer?

A extensão DataKinds permite que criemos novos kinds. Ela funciona sequestrando a palavra reservada data para criar, além do tipo de dados, um kind e tipos associados. Voltaremos a falar desta extensão em mais detalhes quando falarmos de GADTs. Por enquanto apenas aceite que com a extensão ligada, data MeuKind = Tipo1 | Tipo2 cria um kind MeuKind que contém os tipos Tipo1 e Tipo2. No que isso nos ajuda?

A ideia que vamos seguir aqui é a seguinte: vamos criar um novo kind PessoaTipo que terá dois tipos Fisica e Juridica. Depois, vamos usar outra extensão, a KindSignatures (sobre a qual já falamos neste post) para restringir o kind dos tipos aceitáveis como fantasma de Pessoa. Vamos ver no código que fica mais simples!

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

type Nome = String
data PessoaTipo = Fisica | Juridica

data Pessoa (t :: PessoaTipo) where
  Pessoa :: Nome -> Pessoa t

criaFisica :: Nome ->  Pessoa Fisica
criaFisica = Pessoa

criaJuridica :: Nome -> Pessoa Juridica
criaJuridica = Pessoa

todoMundoEBemVindo :: Pessoa a -> Nome
todoMundoEBemVindo (Pessoa nome) = nome

apenasPessoasFisicas :: Pessoa Fisica -> Nome
apenasPessoasFisicas (Pessoa nome) = nome

apenasPessoasJuridicas :: Pessoa Juridica -> Nome
apenasPessoasJuridicas (Pessoa nome) = nome

Note que as diferenças da implementação anterior são bem pequenas. O destaque fica para a assinatura de kind na definição do tipo Pessoa (t :: PessoaTipo) e na definição do tipo PessoaTipo que se parece muito com a primeira solução proposta.

Agora quando tentarmos implementar a solução do Mallandro:

ráPegadinhaDoMallandro :: Pessoa Float -> Nome
ráPegadinhaDoMallandro (Pessoa nome) = nome

Recebemos o seguinte erro:

 • Expected kind ‘PessoaTipo’, but ‘Float’ has kind ‘*’
    • In the first argument of ‘Pessoa’, namely ‘Float’
      In the type signature:
	ráPegadinhaDoMallandro :: Pessoa Float -> Nome
   |
64 | ráPegadinhaDoMallandro :: Pessoa Float -> Nome
   |                                  ^^^^^

Veja só! Pegamos durante a compilação algo que queríamos não só proibir de ser chamado, mas também de que fosse criado pra início de conversa! O erro deixa claro que os tipos aceitos têm kind PessoaTipo, do qual o tipo Float não é parte!

No próximo post quando falarmos sobre GADTs vamos entrar em muito mais detalhes e daremos vários outros exemplos de como a criação de tipos usando DataKinds e mais algumas outras extensões (para não perder o costume) podem ser usadas para fazer ainda mais coisas em tempo de compilação!

5 Referências

6 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.