Capítulo 3  Verificação e Inferência de Tipos

3.1  A regra básica

A regra (onde f e x são expressões quaisquer):

é a regra fundamental usada por um compilador na verificação da correção e na inferência dos tipos usados em programas.

Note que existe uma correspondência básica entre tipos e termos lógicos (termos da lógica proposicional) [6, 12]. Se consideramos tipos (A, B, A → B) como proposições lógicas, e expressões (f, x, f x) como provas (demonstrações) dessas proposições, a regra acima é a regra fundamental (chamada de modus ponens) usada em lógica para dedução de novas formas válidas a partir de formas válidas existentes.

A correspondência entre proposições lógicas e tipos, e entre provas (demonstrações) e expressões, é conhecida como “correspondência de Curry-Howard” (também comumente chamada de “isomorfismo de Curry-Howard”) [6, 12].

No caso de linguagens monomórficas, esta é a regra mais fundamental, e as demais podem ser consideradas como auxiliares. Por exemplo, para deduzir que (not True) tem tipo Bool, precisamos apenas considerar ou saber que not tem tipo (Bool->Bool) e True tem tipo Bool. Essa regra é a base para derivação de tipos de expressões existentes em um programa com base em tipos já conhecidos de outras expressões existentes em um contexto, inicialmente a partir de tipos de constantes e funções pré-definidas.

3.2  Polimorfismo paramétrico

No caso de linguagens polimórficas, essa regra também deve ser aplicada, mas após instanciação de tipos, para que o tipo do domínio da função fique igual ao tipo do argumento. No caso da inferência de tipos, essa instanciação é feita por uma função de unificação, que calcula a substituição mínima que se pode aplicar para que o tipo do domínio da função e o tipo do argumento se tornem iguais.

Mais detalhadamente o processo de inferência de tipos usa a seguinte regra de aplicação, que vamos chamar de regra (APL): para que uma função (potencialmente polimórfica) f: t possa ser aplicada a um argumento x: t′, devemos unificar t com t_A→ t_B (ou seja, t deve ter um tipo funcional) e t_A com t′ (ou seja, o tipo do argumento deve ser unificado com o tipo do domínio da função); o tipo resultante é o tipo t_B resultante da unificação. Isso vai ser explicado mais precisamente na seção seguinte.

O processo de inferência de tipos de um compilador atribui a valores que ocorrem em expressões tipos que são conhecidos e, sempre que um tipo de um valor ainda não é conhecido, como por exemplo o tipo de um parâmetro formal de uma função, uma nova variável de tipo, ainda não usada, é (inicialmente) atribuída a esse valor. Depois disso, a inferência de tipos consiste em determinar os tipos resultantes das unificações especificadas na regra (APL), que vai ser abordada mais detalhadamente na seção seguinte.

3.2.1  Unificação e Substitituição

Dado um conjunto de variáveis V, um conjunto de constantes K (constantes possivelmente de tipos funcionais), o conjunto de termos T pode ser definido com aquele que é formado de acordo com a seguinte sintaxe:

Um tipo como t₁ ⋯ t_n é visto, nessa representação, como App t₁ (… App t_n−1 t_n).

Uma substituição é uma função finita S: V₀ → T de variáveis em termos, onde V₀ é o conjunto finito de variáveis que ocorrem em T. A função id é a função identidade, isto é, a função definida por id x = x.

Dado um conjunto finito de equações E = { t_i=t_i′|i=1,…,n}, onde t_i, t_i′ são termos (valores de T), uma substituição σ é um unificador dos termos de E se σ(t_i)=σ(t_i)′, para i=1,…,n.

Além disso, uma solução σ é mais geral que outra σ′ se existe uma substituição σ₁ tal que σ=σ₁∘σ′. Intuitivamente, um unificador mais geral de um conjunto de equações E é o modo mais simples de tornar todas as equações do conjunto E iguais.

O seguinte algoritmo retorna Just m, onde m é mapeamento que representa o unificador mais geral para uma lista qualquer de pares de tipo (cada par representando uma equação), se um unificador existir, caso contrário retorna Nothing (∘_m é um operador de composição de funções, que retorna Nothing se algum dos argumentos for Nothing, e ocorreEm testa ocorrência de variável em tipo):

As regras usadas na inferência de tipos de um compilador de uma linguagem com polimorfismo paramétrico são baseadas em um contexto de tipos, que associam tipos a variáveis (constantes podem ser consideradas como variáveis, com tipos a ela associados em um contexto global). Contextos de tipos mapeiam variáveis a tipos (é comum na literatura o uso de conjuntos de pares representados na forma variável : tipo). Vamos usar, como é comum, a meta-variável Γ para representar contextos de tipos.

Tipos de variáveis podem ser monomórficos (ou simples) ou polimórficos (ou quantificados). Um tipo simples é formado por uma constante ou uma variável, possivelmente aplicada a um ou mais tipos simples. Ou seja, é da forma:

Usamos t como para denotar valores do tipo T, a ou b para denotar valores de tipo V e k para denotar valores do tipo K, podendo essas variáveis ter possivelmente subscritos e aspas simples. Usamos X para denotar sequências, possivelmente vazias, de valores X, ou conjuntos de tais valores. Por exemplo, T representa uma sequência de tipos, e um tipo polimórfico σ, do tipo de conjuntos polimórficos Σ, é da forma ∀ ā. t, onde ā é uma sequência de variáveis de tipo pertencentes a V; ou seja:

A notação Γ, x:t representa o contexto Γ′ tal que Γ′(x′) = t se x′=x, senão Γ(x′) (ou seja, Γ′ é um contexto igual a Γ mas Γ′(x) = t).

A função tv retorna o conjunto de variaveis livres de um tipo. Em particular, tv(∀ā. t) = tv(t) − ā.

A relação gen(t,σ,Γ) é a relação de generalização de t para σ em Γ, definida de forma que σ = ∀ā. t, onde ā = tv(t) − tv(Γ).

Um tipo S(σ), ou simplesmente Sσ, onde S é uma substituição tal que S(a) = a se a ≠ a_i, S(a_i) = b_iq, para i de 1 a n, representa o tipo resultante de substituir cada a_i por b_i, para i de 1 a n. O tipo Sσ pode ser denotado também por [ā := b]σ.

O algoritmo de inferência de tipos de uma linguagem como o núcleo da linguagem ML pode ser descrito usando as regras mostradas na Figura 3.1, onde Γ ⊢ e: (t,S) significa que e tem tipo t no contexto de tipos Γ. A substituição S é usada para unificação de tipos de expressões usadas em e. Esse algoritmo foi definido por Robin Milner e Luís Damas [3], sendo chamado de algoritmo W.

A regra (VAR) retorna o tipo da variável no contexto de tipos (supõe-se que um programa é um termo fechado, isto é, sem variáveis livres, no sentido de λ-cálculo).

A regra (APL) é a regra básica (ver seção 3.1) da inferência de tipos: usa unificação para tornar o tipo domínio da função igual ao tipo do argumento.

A regra (ABS) cria uma nova variável (a, na Figura 3.1) para o tipo do parâmetro, usando a substituição (S) obtida na inferência do tipo do corpo da λ-abstração para especialização do tipo do parâmetro. O tipo da λ-abstração é o tipo funcional S(a)→ t, sendo t o tipo inferido para a expressão e, corpo da λ-abstração.

A regra (LET) generaliza o tipo inferido para e para obter o tipo de e′, que é retornado como o tipo da expressão let x = e in e′. Note que a regra (LET) é que permite a introdução de tipos polimórficos; o uso de variáveis definidas na regra (LET) pode ser usada em contextos que requerem tipos distintos, como por exemplo em:

onde True e 1 têm tipos distintos (Bool e Integer), e o tipo de f pode ser instanciado (no algoritmo W, via unificação) para Bool→ Bool e para Integer→ Integer.

---

Γ(x) = ∀ā. t       b variáveis novas Γ ⊢ x:  ([ā := b] t , id) (VAR)               Γ ⊢ f :  (t , S)     S(Γ) ⊢ e:  (t′ , S′)    a variável nova   S1 = Su∘ S′∘ S Γ ⊢ f   e:  (S1(a) , S1) Just Su = unif([(t,  t′ → a)])      (APL)           Γ, x:a ⊢ e: (t , S)      a variável nova Γ ⊢ λ x -> e:  (S(a)-> t , S) (ABS)           Γ ⊢ e:  (t , S)     gen(t,σ,S(Γ))     S(Γ), x:σ ⊢ e′:  (t′ , S′) Γ ⊢ let  x  =  e  in  e′:  (t′ , S′ ∘ S) (LET)

Figura 3.1: Algoritmo W

---

A regra (LET) — e a linguagem núcleo de ML do algortimo W definido na Figura 3.1 — não considera recursão, ou seja, x não pode ocorrer em e na expressão let x = e in e′.

No entanto, o uso do algoritmo definido na Figura 3.1 não é necessário para determinar o tipo de funções, na prática, uma vez que ele é baseado fundamentalmente no uso do tipo de variáveis que estão no contexto de tipos, pela introdução de novas variáveis de tipo para o tipo de variáveis introduzidas em λ-abstrações, e pelo uso de unificação em aplicações de funções a seus argumentos. Não é necessário seguir todos os passos do algoritmo. Podemos usar a seguinte técnica, que vamos chamar de técnica-informal-de-inferência-de-tipos. Considere, por exemplo, a tarefa de inferir o tipo da expressão:

Sabemos que o tipo dessa expressão é da forma:

onde:

Introduzimos agora as informações que pudermos obter com os usos das variáveis f e x na expressão f (f x), devido a unificação, que são:

• f tem tipo funcional (pois x é aplicado a f), ou seja, é da forma t₁→ t₂;
• o tipo de x é o mesmo do domínio de f, ou seja, t₁ = t_x;
• o tipo do resultado de f (t₂) é o mesmo do argumento de f (pois o resultado, f x é aplicado a f).

.

Note: cada ocorrência de parâmetro de função — i.e. cada variável em uma λ-abstração — tem um tipo monomórfico (essa é uma característica fundamental do sistema de tipos de ML e Haskell).

Usando essas informações, obtemos que o tipo de:

é igual a (chamando t_x simplesmente de a):

Essa técnica pode ser estendida para os casos de definições recursivas, que envolvam mais de uma equação, (lembrando que parâmetros têm tipos monomórficos e) considerando que:

• uma equação f p₁ … p_n = e pode ser vista como tendo o tipo de uma λ-abstração: λ p₁. … λ p_n. e, sendo esse o tipo de f.
• toda definição:

  f  p11  …  p1n  =  e1                   …                     f  pm1  …  pmn  =  em

  deve ser tal que os tipos de cada resultado e_i, assim como os tipos de cada parâmetro p_ij, para cada i,j (i=1,…,m e j=1,…,n) são iguais: para isso os tipos de cada equação devem ser unificados (se não for possível unificar os tipos de cada equação, a definição não é bem tipada).

Por exemplo, considere a definição de map:

Vamos calcular o tipo de map inicialmente na primeira equação. Poderíamos começar com t_f → t_l → t_r, sendo t_f, onde:

tf é (uma variável que representa) o tipo de f,

tl é (uma variável que representa) o tipo de [] e

tr é (uma variável que representa) o tipo do resultado, também [].

No entanto, como sabemos, pelo tipo de [] no contexto de tipos, que [] tem tipo [a], sendo a uma variável nova, podemos considerar que o tipo de map na primeira equação é:

Note que as ocorrências de [] têm tipos distintos, com variáveis de tipo a e b novas, pois o tipo de [], no contexto de tipos, é polimórfico.

Na segunda equação, podemos atribuir a map inicialmente o tipo: t_f → t_l → t_r, sendo: t_f variável que representa o tipo de f, t_l variável que representa o tipo de a:x e t_r variável que representa o tipo de f a:map f x. Temos:

• sendo t_l igual a [a] (de acordo com o tipo de [] usado para esse parâmetro na primeira equação), o tipo de a é igual a a e o tipo de x é igual a [a] (pois o tipo de (:) no contexto de tipos é igual a a′→ [a′] → [a′], para alguma variável nova a′, mas a′ deve ser igual a a, pois os tipos dos parâmetros nas duas equações devem ser iguais.
• t_f deve ser um tipo funcional, pois f é aplicado a a, e o tipo do resultado de f deve ser igual a b, igual ao tipo do elemento da lista [b]: [b] é o resultado de map f [] na primeira e na segunda equações, e igual ao tipo do resultado de map f x.

Portanto, o tipo de map, definido pelas duas equações acima, é:

3.2.2  Sobrecarga e Tipos restritos

Um valor sobrecarregado tem um tipo polimórfico restrito, em que a instanciação não pode ser feita para todos os tipos, mas somente para aqueles para os quais a sobrecarga está definida. Por exemplo, (==) tem tipo Eq a => a -> a -> Bool, sendo a instanciação restrita a tipos para os quais a igualdade está definida.

Desta forma, quando a sobrecarga é resolvida (e apenas neste caso), devido a instanciação do tipo polimórfico (via unificação), é preciso verificar se há instâncias no contexto que satisfazem ao tipo do valor sobrecarregado que foi instanciado:

• se há apenas uma instância, a restrição é removida do tipo;
• se não ha nennhuma instância, ocorre um erro de tipo: insatisfazibilidade.
• se há duas ou mais instâncias, ocorre um erro de tipo: ambiguidade.

Por exemplo, a expressão 1 + ’1’ usualmente gera um erro de tipo, porque usualmente não há instância de Num para o tipo Char.

Em Haskell, não há definição de quando uma sobrecarga é resolvida, e esta condição é confundida com ambiguidade: em Haskell um tipo é ambíguo se existe uma variável de tipo que ocorre em uma restrição e não ocorre no tipo simples. Por exemplo, o tipo da expressão (show . read), que é:

é considerado ambíguo, pois a variável de tipo a ocorre em uma restrição e não ocorre no tipo (simples) String -> String.

Em Haskell, não há, assim, diferença entre insatisfazibilidade e ambiguidade, nem entre sobrecarga resolvida e ambiguidade.

O teste de satisfazibilidade, que deve verificar se existe ou não uma única instância que satisfaz a uma restrição, é em geral um problema indecidível [11, 13]. Existem várias opções de compilação no GHC para restringir tipos polmórficos restritos [5]. No entanto, essas opcões poderiam ser evitadas por um mecanismo baseado em uma medida do tamanho dos tipos que formam as restrições, medida essa calculada durante o processo de testar satisfazibilidade [9, 2].

Quando há mais de uma equação em uma definição, as restrições de cada equação devem ser consideradas (isto é, devem ser unidas) para gerar a restrição final resultante da unificação de cada uma das equações. Veja por exemplo o exercício resolvido 1.

3.3  Exercícios Resolvidos

1. Considere a definição de merge a seguir:

   merge ([], y) = y -- (1) merge (x, []) = x -- (2) merge (a:x, b:y) -- (3) | a <= b = a:merge (x, b:y) -- (4) | otherwise = b:merge (a:x, y) -- (5)

   Use a técnica-informal-de-inferência-de-tipos para determinar o tipo de merge.

   Solução: O tipo de merge é, inicialmente, igual a t_p → t_r, onde t_p é o tipo do argumento e t_r o tipo do resultado. Vamos determinar o tipo de cada equação, depois vamos considerar que o tipo de cada equação é o mesmo, e para isso vamos usar unificação, conservando (isto é, unindo) as restrições existentes nos tipos de cada equação.

   O tipo de merge na linha 1 (primeira equação) é ([a],t_y) -> t_y.

   O tipo de merge na linha 2 (segunda equação) é (t_x,[b]) -> t_x.

   Na linha 3 (são duas equações neste caso, uma para cada guarda), o tipo de merge é Ord a => ([a],[a]) -> [a]; note que:

   • a restrição Ord a é inserida devido ao uso do operador sobrecarregado <= (na linha 4);
   • inicialmente o tipo de merge na linha 3 seria ([a],[b]) -> t_r, mas, tanto devido à comparação a <= b — o tipo de <= é Ord a => a -> a -> Bool, portanto o tipo de a e de b em a <= b têm que ser iguais — quanto devido ao fato de que os tipos de t_r nas linhas 4 e 5 têm que ser iguais (t_r é igual [a] na linha 4 e igual a [b] na linha 5, o tipo de merge na última “equação” é Ord a => ([a],[a]) -> [a]).

   Unificando os tipos das equações, obtemos o tipo de merge:

   Ord a => ([a],[a]) -> [a]

3.4  Exercícios

1. Determine o tipo de λ x. λ y. λ z. x z (y z), usando a técnica-informal-de-inferência-de-tipos.
2. Use a técnica-informal-de-inferência-de-tipos para determinar o tipo da função either definida abaixo:
   1. Sendo o tipo Either definido como:

      data Either a b = Left a | Right b

      defina como é inferido o tipo de either, usando a técnica-informal-de-inferência-de-tipos, definido como:

      either f g (Left x) = f x either f g (Right y) = g y

3. Defina expressão ou função com tipo:
   1. (Ord a, Show a) => a -> a -> String
   2. (a -> b -> c) -> b -> a -> c
   3. (a -> b, a -> c) -> a -> (b,c)
   4. (a -> b, b -> d) -> (a,b) -> (c,d)
   5. (b -> c) -> (a->b) -> a -> c
   6. [(a, b)] -> ([a], [b])
   7. (a -> b -> a) -> a -> [b] -> [a]