Type Families - Funções no nível dos tipos

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

1 Aplicando funções em tipos

Em algumas situações o tipo de saída da função possui uma dependência com os tipos de entrada. Por exemplo, se quisermos criar uma função merge :: Vec m a -> Vec n a -> Vec o a, o tipo o não pode ser qualquer tipo, ele necessariamente deve ser m + n.

Ou seja, esse tipo de definição demanda que o tipo de saída seja definido após a aplicação de uma função (no caso, (+)) nos tipos de entrada.

Em Haskell podemos definir essas funções aplicadas em tipos através do Type Family .

Vamos começar com um exemplo básico no nosso sistema de controle de usuários e portas. Imagine que queremos definir uma função track que recebe um usuário u1 (que é o usuário efetuando a consulta), um usuário u2 que é o usuário procurado. A função pode devolver:

  • O local de u2 caso u1 seja Admin e u2 seja Noob.
  • Informação de contato, caso ambos sejam Admin (assim u1 pergunta diretamente a u2 onde ele está).
  • O tipo Denied, caso u1 seja Noob e u2 seja Admin.
  • Uma função Request, caso ambos sejam Noob, para que ele possa requisitar a informação para o Admin mais próximo.

Primeiro, vamos reescrever nosso tipo User utilizando GADTs para relembrarmos alguns conceitos do capítulo anterior:

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

data UserType = Noob | Admin

type User :: UserType -> *
data User t where
  User :: String -> User Noob
  Sudo :: User Noob -> User Admin

_username :: User a -> String
_username (User s)        = s
_username (Sudo (User s)) = s

getUser :: String -> IO (Maybe (User Noob))
getUser username = do
  db <- connect
  u  <- getUser db username
  close db
  pure u

sudo :: User Noob -> IO (Maybe (User Admin))
sudo u = do
  db <- connect
  b  <- checkAccess u
  close db
  if b then pure (Just $ Sudo u)
       else pure Nothing

Nesta definição para User estamos usando o estilo de definição de assinaturas standalone kind signatures. Essa versão é equivalente ao modo que vimos até agora (data User :: UserType -> * where) mas deixa a sintaxe mais próxima daquela de funções. O motivo de fazermos esta escolha agora vai ficar claro em alguns parágrafos. Para usar essa sintaxe é preciso habilitar a extensão StandaloneKindSignatures.

Agora precisamos criar os tipos de cada uma das possíveis saídas:

data Location    = Location { _x :: Double, _y :: Double }
newtype Contact  = Contact String
data Denied      = Denied
newtype Request  = Request (String -> IO Location)

Finalmente podemos criar a função track, que deve ter a assinatura:

track :: User a -> User b -> c

A implementação seria algo como:

track :: User a -> User b -> c
track (User u1) (User u2) = Request (const (pure (Location 0.0 0.0)))
track (Sudo u1) (Sudo u2) = Contact "0000-0000"
track (Sudo u1) (User u2) = Location 10.0 3.01
track (User u1) (Sudo u2) = Denied

Porém esse código não compila pois o compilador não consegue pré-determinar qual deve ser o tipo c. Para resolver essa situação, vamos criar uma função que determina o tipo de c dependendo dos tipos a e b. Para isso precisamos habilitar a extensão TypeFamilies:

{-# LANGUAGE TypeFamilies #-}

-- Usando a sintaxe kind signatures
type family Track (a :: UserType) (b :: UserType) where
  Track Noob Noob   = Request
  Track Admin Admin = Contact
  Track Admin Noob  = Location
  Track Noob Admin  = Denied

-- Ou melhor ainda, usando a sintaxe fornecida pela extensão
-- StandaloneKindSignatures
type Track :: UserType -> UserType -> *
type family Track a b  where
  Track Noob Noob   = Request
  Track Admin Admin = Contact
  Track Admin Noob  = Location
  Track Noob Admin  = Denied

Ambas as sintaxes são equivalentes neste caso, mas nós tendemos (nós == os autores deste post) a preferir a segunda opção por ela deixa o código bem mais próximo do formato de uma função convencional, com a assinatura seguida da implementação. Isso na nossa opinião é desejável já que estamos, efetivamente, escrevendo uma função que opera no nível dos tipos.

O código acima, cria uma função que pode ser aplicada em tipos com os kinds especificados. Em nosso exemplo, criamos o type family chamado de Track que recebe dois tipos com kind UserType e retorna um tipo como saída. As definições de entrada e saída são similares a uma definição de função no nível dos termos com uso de pattern matching.

Com isso podemos fazer:

track :: User a -> User b -> Track a b
track (User u1) (User u2) = Request (const (pure (Location 0.0 0.0)))
track (Sudo u1) (Sudo u2) = Contact "0000-0000"
track (Sudo u1) (User u2) = Location 10.0 3.01
track (User u1) (Sudo u2) = Denied

E, agora, o compilador consegue determinar o tipo correto da saída de acordo com as entradas.

2 Type Families

Feito o hello world!, vamos agora ver em mais detalhes o que está acontecendo neste código..

A extensão TypeFamilies introduz dois novos construtores além daqueles que já apresentamos. Considere um construtor T, temos então as seguintes sintaxes fazem com que T seja:

  • data T a b c: construtor de tipos
  • newtype T a b c: construtor de sinônimos newtype
  • class T a b c: construtor de classe
  • type T a b c: construtor de sinônimos

Com a extensão habilitada, adicionamos:

  • type family T a b c: construtor de type family
  • data family T a b c: construtor de data family

Uma type family pode ser fechada (closed) ou aberta (open). Dentre as type families na categoria aberta elas se sub-dividem em nível superior (top-level) e associadas (associated).

Já uma data family só pode ser aberta e nestes casos também é sub-dividida entre nível superior e associada .

3 Closed Type Families

Antes de entendermos Closed Type Families, vamos relembrar que agora temos duas formas de computar:

  • No nível dos termos, quando criamos funções que aplicam operações em valores associados a um tipo.
  • No nível dos tipos, quando criamos funções que aplicam operações em tipos associados a um kind.

Vamos exemplificar ambas com a função or', no nível de termos e Or no nível de tipos:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneKindSignatures #-}

or' :: Bool -> Bool -> Bool
or' False False = False
or' _     _     = True

type Or :: Bool -> Bool -> Bool
type family Or a b where
  Or False False = False
  Or _     _     = True

No primeiro exemplo, temos uma função que recebe dois valores do tipo Bool e retorna um Bool. No segundo, temos uma função que recebe dois tipos de kind Bool e retorna um tipo de kind Bool. Podemos ver a diferença de ambos no ghci:

> :t or'
or' :: Bool -> Bool -> Bool

> :k Or
Or :: Bool -> Bool -> Bool

E podemos verificar como elas podem ser aplicadas:

> or' True False
True

> :k! Or True False
Or True False :: Bool
= 'True

Em resumo, com uma type family podemos aplicar funções em tipos e aplicar tais operações no nível de tipos nas assinaturas das funções no nível de termos.

Assim como em funções, podemos ter type families com definições polimórficas. Para explicitar o polimorfismo, vamos habilitar a extensão PolyKinds:

fst' :: forall a b . (a, b) -> a
fst' (x, _) = x

type Fst :: forall a b . (a, b) -> a
type family Fst t where -- note que t ~ (a, b)
  Fst '(a, _) = a       -- precisamos usar o tick

A extensão de compilador PolyKinds permite usar a palavra-chave forall na assinatura de kinds para um type family.

A type family Fst recebe um tipo que é formado por uma tupla de tipos com kind a e b, e retorna o tipo com kind a. Na sua definição não podemos fazer type family Fst (a, b) pois (a, b) representa apenas um tipo e o kind desse tipo é (a, b). Outro ponto para tomar cuidado é que o compilador não consegue diferenciar a sintaxe de tuplas no nível de termos e no nível de tipos, por isso precisamos especificar que estamos tratando do nível de tipos com um tick na frente do construtor da tupla: ~’(a, b)'.

Esse tipo de type family é denominada fechada pois todas as equações pertencentes a essa família devem ser definidas no respectivo bloco. Não é possível deixar uma definição em aberto para ser criada posteriormente.

3.1 Operações com o tipo Nat

No capítulo anterior definimos o tipo Nat que foi utilizado em conjunto da sintaxe GADT para criarmos tipos bem estruturados como o vetor com informação de tamanho.

Nessa ocasião, a criação da função append não era possível pois o tipo de saída deveria ser a soma dos tamanhos dos vetores de entrada.

Essas operações sugerem um caso de uso de type families. Antes de redefinirmos as funções citadas para esses tipos, vamos praticar um pouco mais criando algumas operações básicas para Nat no nível de tipos. Lembrando que o tipo Nat foi definido como:

{-# LANGUAGE DataKinds #-}

data Nat = Z | S Nat

As operações de adição e multiplicação são simples de serem implementadas no nível de tipos:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneKindSignatures #-}

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

type (.*) :: Nat -> Nat -> Nat
type family m .* n where
  Z .* n     = Z
  (S m) .* n = n + (m .* n)

A extensão de compilador TypeOperators permite criar type families como operadores infixos.

A definição da operação de adição indica que ao somar \(0\) com qualquer número \(n\), o resultado é \(n\). E, ao somar o sucessor de um valor \(m\) com \(n\) o resultado é o sucessor de \(m + n\). Isso é simplesmente a propriedade \((1 + m) + n = 1 + (m + n)\) que reduz o nosso problema original \((1 + m)\) em um para então fazer a chamada recursiva \(m + n\). Por exemplo, a operação \(3 + 2\) fica:

>:k! S (S (S Z)) + S (S Z)
S (S (S Z)) + S (S Z) :: Nat
= S ( S (S Z) + S (S Z) ) :: Nat
= S ( S ( S Z + S (S Z) ) ) :: Nat
= S ( S ( S ( Z + S (S Z) ) ) ) :: Nat
= 'S ('S ('S ('S ('S 'Z))))

A multiplicação diz que ao multiplicar \(0\) por qualquer valor, temos como resultado o próprio \(0\). E, a indução utilizada para a redução da entrada da recursão é a propriedade \((1 + m) \cdot n = n + (m \cdot n)\). A operação \(2 * 1\) fica:

(S (S Z)) .* (S Z)       -- (1 + 1) * 1
= (S Z) + (S Z .* S Z)   -- 1 + (1 * 1) (def. 2 de .*)
= S (Z + (S Z .* S Z))   -- 1 + (0 + (1 * 1)) (def. 2 de +)
= S (S Z .* S Z)         -- 1 + (1 * 1) (def. 1 de +)
= S (S Z + (Z .* S Z))   -- 1 + (1 + (0 * 1)) (def. 2 de .*)
= S (S (Z + (Z .* S Z))) -- 1 + (1 + (0 + (0 * 1))) (def. 2 de +)
= S (S (Z .* S Z))       -- 1 + (1 + (0 * 1)) (def. 1 de +)
= S (S (Z))              -- 1 + (1 + 0) (def. 1 de .*)

As operações de subtração e divisão não são fechadas, isto é, há resultados destas operações que não estão contidas nos naturais. No caso da subtração, a operação \(m - n\) quando \(n > m\) não retorna um número natural. Da mesma forma, \(m / 0\) também não é um número natural. Para definirmos essas operações, podemos assumir que \(m - n = 0\) quando \(n > m\) e \(m / 0 = 0\). Com isso temos:

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

O primeiro caso representa a propriedade \(m - 0 = m\), o segundo caso foi a definição \(0 - (n + ) = 0\) que criamos para garantir um número natural como resultado. Finalmente, a recursão usa a propriedade \((m + 1) - (n + 1) = m - n\) até que chegue em um dos casos bases, quando um dos valores atingirem \(0\).

A divisão requer algumas operações que ainda não temos. Vamos verificar os casos bases:

type Div :: Nat -> Nat -> Nat
type family Div m n where
  Div Z _ = Z
  Div _ Z = Z
  Div m m = S Z
  Div m n = ???

O primeiro caso diz que \(0 / n = 0\) e o segundo que \(m / 0 = 0\) conforme convencionamos anteriormente. O terceiro caso indica que se dividirmos um número por ele mesmo, temos como resultado o valor \(1\).

Note que, diferentemente das definições de funções, as variáveis usadas no pattern matching da entrada de cada uma das equações da nossa type family podem ser iguais. Neste caso elas indicam que efetivamente ambos os parâmetros se tratam do mesmo tipo. Esse comportamento é comum em outras linguagens como Erlang e Prolog para a implementação de funções no nível dos termos.

O caso da recursão \(m / n\) precisa levar em conta se \(m < n\). Se for o caso, o resultado é \(0\). Caso contrário fazemos a chamada recursiva \(m / n = 1 + (m - n) / n\). Podemos verificar que de fato isso é verdade pois \(1 + (m - n) / n = (n + (m - n)) / n = m / n\). Assumindo a existência de todas as operações necessárias, nosso código ficaria:

type Div :: Nat -> Nat -> Nat
type family Div m n where
  Div Z _ = Z
  Div _ Z = Z
  Div m m = S Z
  Div m n = IF (IsLT (Cmp m n)) Z (S (Div (m - n) n))

Vamos então implementar as type families que faltam!

type IF :: Bool -> Nat -> Nat -> Nat
type family IF b m n where
  IF True m n  = m
  IF False m n = n

type IsLT :: Ordering -> Bool
type family IsLT o where
  IsLT LT = True
  IsLT _  = False

type Cmp :: Nat -> Nat -> Ordering
type family Cmp m n where
  Cmp Z Z = Eq
  Cmp Z _ = LT
  Cmp (S _) Z = GT
  Cmp (S m) (S n) = Cmp m n

Com isso podemos fazer operações aritméticas básicas com nosso tipo Nat. Nas próximas seções, aplicaremos algumas delas nas nossas definições de árvore binária e vetores indexados.

3.2 Lista Heterogênea

Uma aplicação interessante de GADTs e type families é a implementação de uma lista heterogênea que armazena valores de tipos diferentes em cada elemento. A definição dessa lista é:

data HList xs where
  HNil  :: HList '[]
  (:.)  :: x -> HList xs -> HList (x : xs)
infixr 5 :.

Com isso podemos criar uma lista como:

xs :: HList [Int, Double, String]
xs = 12 :. 13.4 :. "Ola" :. HNil

Da mesma forma que fizemos anteriormente, podemos criar a versão total das funções head e tail, pois podemos casar exatamente o padrão de listas não vazias:

hhead :: HList (x:xs) -> x
hhead (x :> _) = x

htail :: HList (x:xs) -> HList xs
htail (_ :> xs) = xs

Note que a assinatura da função exige que o valor de entrada seja uma lista contendo pelo menos um tipo x. Além disso, as definições da assinatura e a implementação da função se tornam muito similares. Não existe outra forma de implementar tais funções!

Para implementar uma função happend temos que definir uma type family para determinar o tipo de saída, pois a assinatura dessa função deve ser:

happend :: HList xs -> HList ys -> HList (Append xs ys)

A implementação da type family Append é muito similar com uma implementação simples de append ou (++):

type Append :: [a] -> [a] -> [a]
type family Append xs ys where
  Append '[] ys      = ys
  Append (x : xs) ys = x : Append xs ys

E a implementação da função happend é quase idêntica a sua type family:

happend :: HList xs -> HList ys -> HList (Append xs ys)
happend HNil ys = ys
happend (x :> xs) ys = x :> happend xs ys

Podemos utilizar a definição de Append para criar o type family Reverse:

type Reverse :: [a] -> [a]
type family Reverse xs where
  Reverse '[]      = '[]
  Reverse (x : xs) = Append (Reverse xs) '[x]

E com isso implementamos a função hreverse de forma similar:

hreverse :: HList xs -> HList (Reverse xs)
hreverse HNil = HNil
hreverse (x :> xs) = happend (hreverse xs) (x :> HNil)

4 Open Type Family

Suponha que sua lista heterogênea vai ser utilizada para manipulação de dados provenientes de uma base de dados bem estruturada e, para efeito de exportação, você precisa transformar os tipos em String contendo o nome correspondente no servidor de dados.

Uma forma de fazer tal conversão é criando um type family tal que [1]:

type Label :: Type -> Symbol
type family Label t where
  Label Double = "number"
  Label Int    = "number"
  Label String = "string"
  Label Bool   = "boolean"

Podemos converter um tipo utilizando a classe KnownSymbol importado de GHC.TypeLits:

label :: forall t. KnownSymbol (Label t) => t -> String
label x = symbolVal (Proxy @(Label t))

A assinatura dessa função diz: para todo tipo t que possui uma instância de Label e pertence a KnownSymbol, eu gero um valor único do tipo String associado a esse tipo. A função symbolVal definida em GHC.TypeLits funciona de forma análoga à natVal que usamos no post anterior.

Agora podemos fazer uma função labels associada a uma lista de tipos e retorna uma lista de String:

labels :: HList ts -> [String]
labels HNil = []
labels (x :> xs) = label x : labels xs

Porém isso não compila, pois não sabemos se todos os tipos associados à HList possuem um Label ou fazem parte de KnownSymbol. Precisamos mapear a restrição para cada um dos tipos de nossa lista. Podemos criar um type family AllSymblLbl que faz esse mapeamento:

type AllSymbLbl :: [a] -> Constraint
type family AllSymbLbl xs where
  AllSymbLbl '[] = ()
  AllSymbLbl (x : xs) = (KnownSymbol (Label x), AllSymbLbl xs)

Ou seja, a cada tipo da lista ele adiciona a restrição KnownSymbol (Label x) e compõe com a restrição no restante da lista. Com isso agora podemos fazer:

labels :: AllSymbLbl ts => HList ts -> [String]
labels HNil = []
labels (x :> xs) = label x : labels xs

Isso funciona muito bem até que criemos novos tipos User e Door e queiramos criar uma instância da type family Label para esses tipos.

Se as definições de Door e User fizerem parte de nossa biblioteca, basta alterarmos nosso código para:

type Label :: Type -> Symbol
type family Label t where
  Label Double = "number"
  Label Int    = "number"
  Label String = "string"
  Label Bool   = "boolean"
  Label User   = "user"
  Label Door   = "door"

Porém, caso não tenhamos acesso a essa definição, não podemos incluir novas definições externamente! Isso ocorre porque essa família de tipos é fechada (closed type family) já que não aceita novos membros.

Uma família de tipos fechada deve ser criada com a definição completa. Uma outra forma de definir uma família de tipos é:

type Label :: Type -> Symbol
type family Label t

type instance Label Double = "number"
type instance Label Int    = "number"
type instance Label String = "string"
type instance Label Bool   = "boolean"

Esse tipo de definição é chamade de família de tipos aberta (open type family) pois ela permite a inserção de novos membros a qualquer instante, mesmo que externa ao arquivo-fonte em que ela foi definida. Em qualquer momento podemos fazer:

type instance Label User   = "user"
type instance Label Door   = "door"

Com isso aumentamos a flexibilidade da definição de família de tipos. A desvantagem em deixar uma família de tipos aberta é que ela não permite sobreposição em suas equações. Considere, por exemplo, a família And:

type And :: Bool -> Bool -> Bool
type family And a b where
  And True True = True
  And _    _    = False

Uma vez que a família fechada permite sobreposição, podemos definir a instância genérica And _ _ que casa com todos os padrões que não casam com a primeira definição. Se implementarmos essa família como aberta, teríamos que enumerar todas as possíveis instâncias:

type And' :: Bool -> Bool -> Bool
type family And' a b

type instance And' True  True  = True
type instance And' True  False = False
type instance And' False True  = False
type instance And' False False = False

O que em alguns casos é proibitivo por causar uma explosão combinatória.

5 Tipos associados

Imaginem que queremos criar uma classe MyLogger com o objetivo de criar um relatório de aberturas de portas por nossos usuários. A ideia é que essa classe defina um método chamado trackUser que é responsável por armazenar o histórico das ações dos usuários em nossas portas.

Em Haskell, temos diversas maneiras de implementar um logger, podemos utilizar a mônada Writer com uma lista que armazena a sequência das ações, ou uma mônada State que guarda apenas a última ação feita, ou até um IO que armazena as ações em um banco de dados.

O que queremos é:

class MyLogger logger where
  trackUser :: User a -> Int -> MyMonad ()

Ou seja, a classe define um método trackUser que, ao receber um usuário e o número de uma porta, faz uma ação da mônada escolhida. Mas qual deve ser essa mônada? Queremos que ela dependa do tipo logger. Sabemos como associar um tipo a outro utilizando type family:

type MonadLog :: * -> *
type family MonadLog logger

class MyLogger logger where
  trackUser :: User a -> Int -> MonadLog logger ()

Agora podemos definir tipos que representam o logger que queremos implementar e criar uma instância para eles com a implementação correspondente.

Por exemplo, se quisermos fazer uso da mônada Writer:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
newtype DoorsSequence = DoorsSequence [String]
			   deriving (Semigroup, Monoid, Show)

type instance MonadLog DoorsSequence = Writer DoorsSequence

instance MyLogger DoorsSequence where
  -- trackUser :: User a -> Int -> Writer DoorsSequence ()
  trackUser user door = tell $ DoorsSequence ["User " <> _username user <> " opened the door " <> show door]

Isso funciona perfeitamente. Podemos inclusive definir uma função runActions que executa uma sequência de ações de acordo com nossa mônada:

runActions :: forall m . (MyLogger m, Monad (MonadLog m)) => MonadLog m ()
runActions = sequence_ [trackUser @m u d | (u,d) <- actions]

Note que temos que garantir que o tipo m possui uma instância de MyLogger, para podermos utilizar o método trackUser, o tipo MonadLog m deve ter uma instância de Monad, para podermos utilizar sequence_ e, precisamos da quantificação forall m para que possamos instanciar o tipo m correto de trackUser. Dessa forma podemos deixar para decidir qual instância utilizar durante o uso dessa função.

Embora o código funcione, por questão de organização pode ser que não faça sentido criar uma instância de MonadLog sem que seja criada uma de MyLogger. Ou seja, podemos querer forçar que a criação de um implique a criação da outra. Para isso podemos utilizar a definição de família de tipos associadas, em que movemos a definição da família de tipos para dentro da definição da classe de tipos:

class MyLogger logger where
  type MonadLog logger :: * -> *
  trackUser :: User a -> Int -> MonadLog logger ()

Agora para criar uma instância de MyLogger precisamos definir o tipo MonadLog correspondente:

instance MyLogger DoorsSequence where
  type (MonadLog DoorsSequence) = Writer DoorsSequence
  trackUser user door = tell $ DoorsSequence ["User " <> _username user <> " opened the door " <> show door]

Vamos criar outros dois exemplos de instâncias utilizando outras mônadas:

newtype LastAction = LastAction String deriving Show
instance MyLogger LastAction where
  type (MonadLog LastAction) = State LastAction
  trackUser user door = put $ LastAction $ "User " <> _username user <> " opened the door " <> show door

newtype Printer = Printer String deriving Show
instance MyLogger Printer where
  type (MonadLog Printer) = IO
  trackUser user door = print $ "User " <> _username user <> " opened the door " <> show door

E podemos utilizá-las fazendo:

main = do
  print $ execWriter $ runActions @DoorsSequence
  print $ execState (runActions @LastAction) $ LastAction ""
  runActions @Printer

6 Data Family

Vimos no início desse livro a diferença entre as definições de tipos com o uso de type e data. O primeiro cria apenas um apelido para um tipo enquanto o segundo cria um novo tipo. Por exemplo:

type Door = Int
data DoorStats = Open | Closed

O tipo Door nada mais é que um Int, em qualquer momento do código podemos intercambiar o uso de Door e Int sem qualquer distinção. Já DoorStats define um tipo completamente novo e único contendo dois valores.

As famílias de tipo, conforme vimos até agora, também definem apenas apelidos para nossos tipos. Quando fazemos:

type And :: Bool -> Bool -> Bool
type family And a b where
  And True True = True
  And _    _    = False

Estamos dizendo que o tipo And True True é apenas um apelido para o tipo True (note que aqui estamos trabalhando com os tipos promovidos no nível dos tipos, então aqui, True e False são tipos, ao invés de valores). Não temos qualquer distinção entre um e outro, mas é suficiente para simularmos operações com nossos tipos em tempo de compilação.

Imagine que queremos criar um novo tipo, chamado Operation que indica as operações que um usuário pode executar.

data Operation = OpenDoor Int | Walk | Work | InsertUser String | DeleteUser String | CreateDoor Int

Porém, nem todas as operações podem ser feitas por todos os usuários. Ao implementar uma função runOp precisamos tomar o cuidado de restringir as operações disponíveis:

runOp :: User a -> Operation -> IO ()
runOp (User _) op = case op of
		      OpenDoor x -> putStrLn $ "opening door " <> show x
		      Walk       -> putStrLn "walk this way!"
		      Work       -> putStrLn "faster! FASTER!"
		      _          -> putStrLn "Access denied!"
runOp (Sudo _) op = case op of
		      InsertUser x -> putStrLn $ "inserting user " <> x
		      DeleteUser x -> putStrLn $ "removing user " <> x
		      CreateDoor x -> putStrLn $ "creating door " <> show x
		      _            -> putStrLn $ "you're too good for that!"

Embora isso funcione, o desenvolvedor pode implementar uma operação para o usuário errado por engano e o compilador não vai emitir nenhum erro, pois para todos os efeitos não tem nada que ligue uma operação a um usuário.

Uma primeira ideia seria fazer:

type Operation :: UserType -> *
data Operation t where
  OpenDoor :: Int -> Operation Noob
  InsertUser :: String -> Operation Admin

Embora isso permita que você implemente casos absurdos na função runOp:

runOp :: User a -> Operation -> IO ()
runOp (User _) op = case op of
		      OpenDoor x -> putStrLn $ "opening door " <> show x
		      Walk       -> putStrLn "walk this way!"
		      Work       -> putStrLn "faster! FASTER!"
		      InsertUser x -> putStrLn $ "inserting user " <> x
		      _          -> putStrLn "Access denied!"
runOp (Sudo _) op = case op of
		      InsertUser x -> putStrLn $ "inserting user " <> x
		      DeleteUser x -> putStrLn $ "removing user " <> x
		      CreateDoor x -> putStrLn $ "creating door " <> show x
		      _            -> putStrLn $ "you're too good for that!"

Ele vai causar um erro de compilação ao escrever runOp (User "Homer") (InsertUser "Bart"), pois os tipos são incompatíveis. Uma forma mais clara de fazer essa implementação é utilizando data family, em que associamos um determinado tipo com a criação de um novo tipo:

type Operation :: UserType -> *
data family Operation t

data instance Operation Noob  = OpenDoor Int | Walk | Work
data instance Operation Admin = InsertUser String | DeleteUser String | CreateDoor Int

Aqui definimos a existência de uma família de novos tipos, chamada de Operation que, ao ser associada ao tipo Noob cria um tipo contendo três valores correspondentes as operações permitidas. Da mesma forma, associamos um novo tipo para Admin. A implementação de runOp fica:

runOp :: User a -> Operation a -> IO ()
runOp (User _) op = case op of
		      OpenDoor x -> putStrLn $ "opening door " <> show x
		      Walk       -> putStrLn "walk this way!"
		      Work       -> putStrLn "faster! FASTER!"
runOp (Sudo _) op = case op of
		      InsertUser x -> putStrLn $ "inserting user " <> x
		      DeleteUser x -> putStrLn $ "removing user " <> x
		      CreateDoor x -> putStrLn $ "creating door " <> show x

E, caso façamos algo como:

runOp :: User a -> Operation a -> IO ()
runOp (User _) op = case op of
		      OpenDoor x -> putStrLn $ "opening door " <> show x
		      Walk       -> putStrLn "walk this way!"
		      Work       -> putStrLn "faster! FASTER!"
		      InsertUser x -> putStrLn $ "inserting user " <> x

O compilador emitirá um erro indicando que InsertUser não é um valor válido para Operation Noob.

7 Estudo de caso: Validação de Strings

Vamos tomar como exemplo um sistema que lida com strings que precisam ser salvas em um banco de dados. Para que tudo seja seguro, consistente e coerente, queremos passar essas strings por uma série de filtros/normalizações para garantir que nenhum ataque de injeção de SQL seja possível além de evitar termos textos salvos com encoding errado, ou todos em maíuscula, etc…

A parte inicial dessa seção é uma elaboração mais detalhada do aperitivo que demos na seção onde apresentamos tipos fantasmas 👻. Reproduzimos abaixo as partes relevantes para conveniência.

Ao contrário dos posts anteriores, aqui vamos fazer lado a lado uma solução em Java e outra em Haskell para então mostrar quando termos funções no nível dos tipos passa a realmente a fazer diferença nas nossas implementações.

Vamos começar apenas com uma operação, a sanitização das strings.

Uma possível solução em Java poderia ter a seguinte cara:

public static void runOnDB(String sql) {
    //...
}

public static String sanitize(String sql) {
    // Do some work
    ...
    return sql;
}

public static void main(String args[]) {
    String sql = "blah blah; drop database;";
    runOnDB(sanitize(sql)); //o compilador aceita isso tranquilamente
    runOnDB(sql); //Mas isso aqui também!
}

O código equivalente em Haskell não seria muito diferente:

runOnDB :: String -> IO ()
runOnDB sql = ...

sanitize :: String -> String
sanitize str = ...

main :: IO ()
main = do
  let sql = "blah blah; drop database;";
  runOnDB (sanitize sql) -- Tudo ok!
  runOnDB sql -- Xi....

Ambas essas implementações sofrem do mesmo problema! Ambas são capazes de, em um descuido do programador, enviar para o banco de dados um SQL que não foi sanitizado!

Nós não queremos permitir que isso seja possível. Queremos garantir que todos os SQLs enviados para o banco sejam sanitizados.

Uma possível solução para isso em Java seria:

class SanitizedString {
    private String contents;
    private SanitizedString(String str) {
	contents = str;
    }
    public static SanitizedString sanitize (String str) {
	//do stuff
	return SanitizedString(str);
    }
}
public static void runOnDB(SanitizedString sql) {...}
public static void main(String args[]) {
    String sql = "blah blah; drop database;";
    runOnDB(sanitize(sql)); //Compilador gosta disso...
    runOnDB(sql); //Mas não gosta disso...Perfeito!
}

-- O construtor UnsafeSanitizedString não deve ser exportado do módulo
-- onde foi declarado
data SanitizedString = UnsafeSanitizedString String
-- Apenas o smart constructor abaixo que deverá estar visível para
-- módulos externos
sanitize :: String -> SanitizedString
sanitize str = UnsafeSanitizedString sanitizedString
  where
    sanitizedString = doSanitization str


-- Em um outro módulo
runOnDB :: SanitizedString -> IO ()
runOnDB sql = ...

main :: IO ()
main = do
  let sql = "blah blah; drop database;";
  runOnDB (sanitize sql) -- Tudo ok!
  runOnDB sql            -- Compilador grita! Legal!

Perfeito! Agora como o tipo necessário para rodarmos algo no BD precisam indicar que o SQL foi sanitizado, é impossível deixarmos passar sem querer uma string não tratada.

Essa abordagem, contudo, tem as suas limitações. Suponha por exemplo que agora não só queiramos sanitizar as strings como também desejamos validá-las, para não ficar mandando lixo para o BD.

Se quisermos seguir esta mesma abordagem, poderíamos seguir na seguinte linha:

class SanitizedString {...}
class ValidatedString {...}

class SanitizedAndValidated {...}

// Sanitized AND Validated
public static void runOnDB(SanitizedAndValidated str) {...}
//Sanitized only
public static void runSanitized(SanitizedString str) {...}
//Validated only
public static void runValidated(ValidatedString str) {...}

E em Haskell

data SanitizedString = UnsafeSanitizedString String
sanitize :: String -> SanitizedString
sanitize str = UnsafeSanitizedString sanitizedString
  where
    sanitizedString = doSanitization str

data ValidatedString = UnsafeValidatedString String
validate str = UnsafeValidatedString validatedString
  where
    validatedString = doValidation str

data SanitizedAndValidatedString = UnsafeSanitizedAndValidatedString String
sanitizeAndValidate :: String -> SanitizedAndValidatedString String
sanitizeAndValidate str = UnsafeSanitizedAndValidatedString sanitizedAndValidatedString
  where
    sanitizedAndValidatedString = doValidation (doSanitization str)

runOnDB :: SanitizedAndValidatedString -> IO ()
runOnDB sql = ...

runSanitized :: SanitizedString -> IO ()
runSanitized str = ...

runValidated :: ValidatedString -> IO ()
runValidated str = ...

Muito bem. Para duas verificações precisamos de três tipos diferentes. Não é tão bom, mas ainda é aceitável. E se quisermos uma terceira validação?

class SanitizedString {...}
class ValidatedString {...}
class CapitalizedString {...}

class SanitizedAndValidated {...}
class SanitizedAndCapitalized {...}
class ValidatedAndCapitalized {...}
class SanitizedValidatedAndCapitalized {...}

data SanitizedString = ...
data ValidatedString = ...
data CapitalizedString = ...

data SanitizedAndValidated = ...
data SanitizedAndCapitalized = ...
data ValidatedAndCapitalized = ...
data SanitizedValidatedAndCapitalized = ...

Agora com 3 verificações, precisamos de 7 tipos diferentes. Está começando a ficar ruim, mas pode ficar pior. Considere agora 4 verificações:

class SanitizedString {...}
class ValidatedString {...}
class CapitalizedString {...}
class UTF8Converted {...}

...
...

Neste caso, para 4 verificações precisaríamos de 15 tipos! Inaceitável!

Podemos fazer melhor? Sim, usando tipos fantasmas! 👻

Comecemos com uma verificação:

public static class CheckedString1<T> {
    private String contents;

    private CheckedString1(String str) {
	contents = str;
    }

    public String getContents() {
	return contents;
    }
}

public static class Sanitized {
    private Sanitized() {
    }

    public static CheckedString1<Sanitized> sanitize(String str) {
	// sanitizes and creates a CheckedString
	return new CheckedString1<Sanitized>(str);
    }
}

public static class Validated {
    private Validated() {
    }

    public static CheckedString1<Validated> validate(String str) {
	// validates string, returns CheckedString
	return new CheckedString1<Validated>(str);
    }
}

public void runSanitized(CheckedString1<Sanitized> str) {...}
public void runValidated(CheckedString1<Validated> str) {...}

E com duas verificações?

public static class CheckedString2<T1, T2> {
    private String contents;
    public CheckedString2(String str,
			   Function<String, CheckedString1<T1>> f1,
			   Function<String, CheckedString1<T2>> f2) {
	String c1 = f1.apply(str).getContents();
	String c2 = f2.apply(c1).getContents();
	contents = c2;
    }
}

// Sanitized AND Validated
public void runOnDB(CheckedString2<Sanitized, Validated> str){...}

Podemos usar esse código da seguinte maneira:

CheckedString2<Sanitized, Validated> sAndV =
  new CheckedString2<Sanitized, Validated>(
    sql,
    Sanitized::sanitize,
    Validated::validate);

runOnDB(sAndV);

O código equivalente em Haskell ficaria:

import Prelude hiding (getContents)

data CheckedString1 t = CheckedString1 {getContents :: String}

data Sanitized
data Validated

sanitize :: String -> CheckedString1 Sanitized
sanitize str = ...

validate :: String -> CheckedString1 Validated
validate str = ...

runSanitized :: CheckedString1 Sanitized -> IO ()
runSanitized str = ...

runValidated :: CheckedString1 Validated -> IO ()
runValidated str = ...

data CheckedString2 t1 t2 = UnsafeCheckedString2 {getContents2 :: String}
mkCheckedString2 :: String -> (String -> CheckedString1 t1) -> (String -> CheckedString1 t2) -> CheckedString2 t1 t2
mkCheckedString2 str f1 f2 = UnsafeCheckedString2 c2
  where
    c1 = getContents (f1 str)
    c2 = getContents (f2 c1)

runOnDB :: CheckedString2 Sanitized Validated -> IO ()
runOnDB str = ...

E o seu uso:

main :: IO ()
  let sAndV = mkCheckedString2 sql sanitize validate
  runOnDB sAndV

Muito bom! Saímos de uma solução cujo número de classes/tipos era exponencial e agora temos uma que é linear no número de verificações que desejamos fazer.

Mas ainda assim, e se quisermos 3, 4, ou um número não espeficicado e arbitrariamente grande de verificações?

É aqui que linguagens como Java, que não tem funções no nível dos tipos, alcança o seu limite. É lógico, é bem fácil fazer este tipo de verificações em tempo de execução! Bastaria passar como parâmetro, junto com a string, uma lista de verificações que já foram feitas.

Contudo, aqui queremos resolver tudo em tempo de compilação, para salvar a sua ceia de natal!!!

7.1 Uma solução baseada em listas no nível dos tipos

Daqui em diante, usaremos novamente apenas Haskell (\o/) pois ele fornece as ferramentas necessárias para trabalharmos.

Vamos começar definindo uma lista das verificações que nos interessam.

data Checks = Sanitized | Validated | Capitalized | UTF8Converted

type CheckedString ::  [Checks] -> *
data CheckedString rs where
  CheckedString :: String -> CheckedString rs
  deriving Show

Agora podemos começar a usar esses tipos.

-- Cria uma checked string que não passou por verificação alguma
checkedString :: String -> CheckedString '[]
checkedString str = CheckedString str

Agora basta adicionar verificações à lista conforme formos precisando. A questão toda é, como fazemos para adicionar um elemento no nível de tipos, à uma lista?

O GHCI nos mostra que existe o (':), a versão no nível de tipos do famoso operador cons para listas:

> :k! 5 ': '[]
5 ': '[] :: [ghc-prim-0.6.1:GHC.Types.Nat]
= '[5]
> :k! Sanitized ': '[]
Sanitized ': '[] :: [Checks]
= '[ 'Sanitized]
> :k! Validated ': Sanitized ': '[]
Validated ': Sanitized ': '[] :: [Checks]
= '[ 'Validated, 'Sanitized]

Perfeito! Agora podemos implementar a função sanitize:

{-# LANGUAGE TypeOperators #-}

sanitize :: CheckedString a -> CheckedString (Sanitized ': a)
sanitize (CheckedString t) =
  -- sanitizes t and creates a new CheckedString
  CheckedString t

validate :: CheckedString a -> CheckedString (Validated ': a)
validate (CheckedString t) = ...

capitalize :: CheckedString a -> CheckedString (Capitalized ': a)
capitalize (CheckedString t) = ...

convertToUTF8 :: CheckedString a -> CheckedString (UTF8Converted ': a)
convertToUTF8 (CheckedString t) = ...

Vamos ver se funciona:

> :t "drop database cascade"
"drop database cascade" :: [Char]

> :t checkedString "drop database cascade;"
checkedString "drop database cascade;" :: CheckedString '[]

> sanitize $ checkedString "drop database cascade;"
CheckedString "drop database cascade;"

> :t sanitize $ checkedString "drop database cascade;"
sanitize $ checkedString "drop database cascade;"
  :: CheckedString '[ 'Sanitized]

> :t sanitize $ sanitize $ checkedString "drop database cascade;"
sanitize $ sanitize $ checkedString "drop database cascade;"
  :: CheckedString '[ 'Sanitized, 'Sanitized]

Droga! Estávamos tão perto! A nossa função funciona, mas permite duplicações. Se uma string passar duas vezes por uma sanitização, não faz sentido ficar acumulando as verificações nos tipos. Para isto, vamoz fazer a nossa própria versão do cons, uma que verifica antes se um elemento já faz parte da lista antes de inserir novamente. Para isso implementaremos a type family Elem que verifica se um elemento está contido pela lista e em seguida nossa versão do cons que chamaremos de (#:).

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Type.Bool

type Elem :: a -> [a] -> Bool
type family Elem r rs where
  Elem r '[]       = 'False
  Elem r (r ': rs) = 'True
  Elem r (_ ': rs) = Elem r rs

type (#:) :: a -> [a] -> [a]
type family r #: rs where
  r #: rs = If (Elem r rs) rs (r ': rs)

Apesar de termos definido o If logo acima, podemos importar o módulo Data.Type.Bool que já traz as funções booleanas e o If implementado para nós.

Mas, esse não é o maior “destaque” do código. O destaque vai para a extensão UndecidableInstances. Apesar do nome assustador, sem essa extensão o compilador reclama que não pode provar que a execução da type family (#:) irá terminar, ou seja, que a compilação terminará (que é o momento onde as type families são efetivamente executadas). Isso ocorre pois temos chamadas aninhadas de type families. A ativação dessa extensão diz para o compilador que sabemos o que estamos fazendo e que a execução irá sim terminar. No pior dos casos, seu código irá ficara compilando indefinidamente caso não esteja bem implementado.

Tirado isso do caminho, vamos trocar a assinatura de tipos das nossas funções para usar (#:):

sanitize :: CheckedString a -> CheckedString (Sanitized #: a)
sanitize (CheckedString t) = ...

validate :: CheckedString a -> CheckedString (Validated #: a)
validate (CheckedString t) = ...

capitalize :: CheckedString a -> CheckedString (Capitalized #: a)
capitalize (CheckedString t) = ...

convertToUTF8 :: CheckedString a -> CheckedString (UTF8Converted #: a)
convertToUTF8 (CheckedString t) = ...

Vamos ver se o comportamento está correto:

> :t checkedString "drop database cascade;"
checkedString "drop database cascade;" :: CheckedString '[]

> :t sanitize $ checkedString "drop database cascade;"
sanitize $ checkedString "drop database cascade;"
  :: CheckedString '[ 'Sanitized]

> :t validate $ sanitize $ checkedString "drop database cascade;"
validate $ sanitize $ checkedString "drop database cascade;"
  :: CheckedString '[ 'Validated, 'Sanitized]

> :t sanitize $ validate $ sanitize $ checkedString "drop database cascade;"
sanitize $ validate $ sanitize $ checkedString "drop database cascade;"
  :: CheckedString '[ 'Validated, 'Sanitized]

> :t capitalize $ sanitize $ validate $ sanitize $ checkedString "drop database cascade;"
capitalize $ sanitize $ validate $ sanitize $ checkedString "drop database cascade;"
  :: CheckedString '[ 'Capitalized, 'Validated, 'Sanitized]

Sucesso! Agora precisamos conseguir limitar o uso, no banco de dados, apenas para strings que tenham passado pelas validações apropriadas.

Para isto, o que gostaríamos é alguma coisa na seguinte linha:

runOnDB :: Observes [Sanitized, Validated] rs => CheckedString rs -> IO ()
runOnDB (CheckedString t) = ...

Basta que implementemos a validação das verificações chamada de Observes acima. Caso a lista rs contenha as validações desejadas (Sanitized, Validated), podemos deixar que a chamada prossiga.

Vamos tentar implementar Observes:

type Observes :: [Checks] -> [Checks] -> Constraint
type family Observes rs0 rs1 where
Observes rs0 rs1 = In rs0 rs1 ~ 'True

Essa type family recebe uma lista de verificações obrigatórias, uma lista das verificações já feitas e devolve uma Constraint que só é válida caso as verificações tenham sido corretamente feitas.

Ela usa uma outra type family In que verifica se uma lista está contida na outra (independentemente da ordem dos elementos). A sua implementação está abaixo:

type In :: [a] -> [a] -> Bool
type family In xs ys where
  In '[]       _   = 'True  -- Por definição uma lista vazia está contida em qualquer outra
  In _         '[] = 'False -- Se não for a lista vazia, qualquer lista não está contida na outra
  In (x ': xs) ys  = If (Elem x ys) (In xs ys) 'False

A implementação é direta. No primeiro caso, por definição, uma lista vazia está contida em qualquer outra. No segundo caso, qualquer lista não vazia contém pelo menos um elemento que não está na segunda. E finalmente o caso recursivo, se o primeiro elemento da primeira lista estiver contido na segunda lista, então basta que o resto dos elementos da lista também estejam. Caso contrário, já devolve 'False e para a recursão.

Note o uso de Elem, If e a chamada recursiva à In. Estamos escrevendo efetivamente um programa que roda no nível dos tipos!

Apenas por completude, não estamos limitados a apenas adicionar elementos na lista. Podemos, por exemplo, escrever uma função que retire um elemento da lista caso presente:

type (#-) :: [a] -> a -> [a]
type family rs #- r where
  '[]        #- _ = '[]
  (r ': rs)  #- r = rs
  (r0 ': rs) #- r = r0 ': (rs #- r)

A implementação acima não é muito diferente do que faríamos para uma lista no nível dos termos. Note que ela funciona para listas sem repetição. Tente adaptá-la para fazê-la funcionar para listas com repetição!

Para usar essa função, poderíamos fazer algo assim:

removeSanitized ::  Observes '[Sanitized] rs => CheckedString rs -> CheckedString (rs #- Sanitized)
removeSanitized (CheckedString t) =
    -- does whatever is needed to t and returns a new CheckedString
    CheckedString t

Note que a função removeSanitized só poderá ser chamada caso a string em questão seja, de fato, uma string sanitizada!

8 Estudo de caso: Vetores indexados

Como falado no inicio desse post e no post passado quando discutimos vetores indexados, há algumas operações que não somos capazes de implementar sem o uso de type families. Vamos começar recordando o estado atual do nosso vetor:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

import Data.Kind

-- Definição indutiva de números naturais
data Nat = Z | S Nat

-- Definição indutiva de um vetor.
type Vector :: Nat -> * -> *
data Vector n a where
  Nil :: Vector Z a
  (:>) :: a -> Vector n a -> Vector (S n) a
infixr 5 :>
deriving instance Show a => Show (Vector n a)

-- Instância para duas classes comuns
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

-- Versão safe de operações comuns em vetores
vhead :: Vector (S n) a -> a
vhead (x :> _) = x

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

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

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


-- Apesar de termos implementado acima uma versão de length, ela não é
-- type-safe.  Poderiamos somar 1 ou 3 e ela continuaria a
-- compilar. Para resolver isto usamos um singleton e implementamos a
-- vlength2

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

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

-- Aproveitamos o singleton para implementar o replicate de forma
-- segura
vreplicate :: SNat n -> a -> Vector n a
vreplicate SZ _ = Nil
vreplicate (SS n) x = x :> vreplicate n x

-- A indexação também é interessante, pois queremos que seja
-- type-safe. Para isto criamos o tipo Ix.
type Ix :: Nat -> *
data Ix n where
    IxZ :: Ix (S n)
    IxS :: Ix n -> Ix (S n)
deriving instance Show (Ix n)

(!) :: Vector n a -> Ix n -> a
(x :> _)  ! IxZ     = x
(_ :> xs) ! (IxS i) = xs ! i


-- Também apresentamos o conceito de tipos existenciais. Eles são
-- necessários para implementar funções como filter

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

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


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

Apesar de bem recheada, a nossa implementação de vetores ainda deixa a desejar em algumas funções como concatenação de vetores. Vamos começar por ela!

No início deste post já tínhamos definido a soma de dois Nat, então e só usar!

(++) :: Vector n a -> Vector m a -> Vector (n + m) a
Nil       ++ v = v
(x :> xs) ++ v = x :> (xs ++ v)

Note que o tipo de retorno é calculado a partir da soma dos tamanhos das entradas!

A mesma ideia pode ser usada para implementar a função vdrop. Mas agora usamos o fato de que quando definimos a subtração de Nat, escolhemos representar \(n - m\), com \(m > n\) como \(0\).

Primeiro vamos pensar nos seus tipos. Como queremos que ela seja segura, vamos usar o tipo SNat que já tínhamos definido. Ela terá a seguinte cara:

vdrop :: SNat n -> Vector m a -> Vector (m - n) a
vdrop _ Nil   = Nil
vdrop SZ v    = v
vdrop (SS n') (_ :> xs) = vdrop n' xs

Primeiramente os casos base. Se o vetor é vazio, devolvemos vazio, não há o que jogar fora. Se descartar 0 elemento, o resultado é o próprio vetor. Finalmente o caso recursivo é, subtraio 1 do número de elementos a serem descartados, descarto um elemento e faço a chamada recursiva.

Parece ok, mas essa implementação, tem um probleminha. O GHC nos diz:

• Could not deduce: ('Z - n) ~ 'Z
  from the context: m ~ 'Z
    bound by a pattern with constructor: Nil :: forall a. Vector 'Z a,
	     in an equation for ‘vdrop’
    at src/Main.hs:123:9-11
  Expected type: Vector (m - n) a
    Actual type: Vector 'Z a
• In the expression: Nil
  In an equation for ‘vdrop’: vdrop _ Nil = Nil
• Relevant bindings include
    vdrop :: SNat n -> Vector m a -> Vector (m - n) a
      (bound at src/Main.hs:123:1)

Ele não está sabendo que \(0 - x = 0\) pela nossa definição? O que está acontecendo? Vamos olhar novamente a definição de (-):

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

Note que a segunda equação diz que Z - (S n) é Z. Mas não fala exatamente o que precisamos que é Z - n = Z. A distinção é pequena, mas é necessária para que o GHC possa provar que os tipos de vdrop estão corretos. Vamos ajustar:

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

Et voilà, ça marche!

Vamos agora ver uma implementação um pouco mais desafiadora. Vamos dizer que queiramos implementar a função take. Dado um número \(n\) de elementos e um vetor, devolvemos um novo vetor que tem \(n\) elementos ou, caso o vetor dado como entrada não tenha \(n\), um vetor com todos os seus elementos.

Assim como vdrop, como queremos que a função seja segura, vamos usar o tipo SNat. Ela terá a seguinte assinatura:

vtake :: SNat n -> Vector m a -> (Min n m) a

Precisamos então definir Min. Vamos usar uma type family!

{-# LANGUAGE TypeFamilies #-}

type Min :: Nat -> Nat -> Nat
type family Min a b where
  Min Z _ = Z
  Min (S _) Z = Z
  Min (S n) (S m) = S (Min n m)

A implementação dos casos base é trivial. Zero é sempre o mínimo entre ele e qualquer número (à esquerda ou à direita). O último caso, recursivo, usa o fato de que \(\min\{n,m\} = 1 + min\{n - 1, m - 1\}\).

Agora podemos implementar a função vtake:

vtake :: SNat n -> Vector m a -> Vector (Min n m) a
vtake SZ _ = Nil
vtake (SS _) Nil       = Nil
vtake (SS n') (x :> xs) = x :> vtake n' xs

9 Referências

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