Este post relata o que eu aprendi tentando misturar (ou combinar) uniões de tipos e polimorfismo paramétrico na mesma linguagem. Faz tempo que eu não escrevo um post de 20k que ninguém vai ler, então aproveito a oportunidade para documentar essas coisas todas antes que eu as esqueça. Este post está sujeito a alterações futuras (dada a impossibilidade técnica de produzir alterações passadas) caso eu lembre de mais algum detalhe.
Para quem não sabe, meu tema de TCC é criar uma linguagem de programação funcional didática. A motivação por trás disso é reduzir os problemas encontrados pelos alunos da disciplina de Fundamentos de Algoritmos (da qual eu fui monitor por três anos) com a linguagem Scheme/Racket (especificamente, com as linguagens didáticas do How to Design Programs, doravante HtDP).
Um dos problemas com essas linguagens é a falta de um sistema de tipos estático. Como conseqüência, as funções e estruturas no código escrito na disciplina normalmente são acompanhadas de um pequeno comentário em um formato semi-padrão indicando os tipos dos parâmetros e retorno das funções, campos de estruturas, etc. O problema é que essa informação não é usada pela linguagem, o que significa que (1) ela não é lá muito útil; (2) conseqüentemente os alunos tendem a não escrevê-la; (3) não há qualquer validação sobre o formato dos comentários, o que impede os alunos de "testar" se eles estão corretos. Para resolver isso, a nova linguagem (que, por motivos de piada interna maior, chama-se Faz), é estaticamente tipada e permite (na verdade exige) declarar os tipos das funções e estruturas.
O problema é que diversos exercícios do HtDP utilizam tipos mistos. Tipos mistos são uma maneira semi-formal de descrever os tipos de funções e de dados freqüentemente utilizados em linguagens dinamicamente tipadas. Por exemplo, se uma função área aceita como argumentos quadrados e círculos, pode-se definir um tipo misto "forma" constituído por quadrados e círculos e dizer que a função recebe uma forma e produz um número. No HtDP, tipos mistos são "definidos" por meio de comentários no código.
A maioria das linguagens estaticamente tipadas não permite definir tipos mistos dessa maneira. Ao invés disso, a maioria das linguagens funcionais estaticamente tipadas permitem a declaração de uniões etiquetadas (tagged unions), ou sum types. Por exemplo, em Haskell, um tipo para formas poderia ser escrito como:
data Forma = Retangulo Float Float
| Circulo Float
A declaração define o tipo (Forma) e os possíveis construtores de valores desse tipo (Retangulo, Circulo) e os tipos dos campos de cada construtor. Para criar um valor, escreve-se uma chamada ao construtor, tal como Retangulo 2 3 ou Circulo 4.
Uma união etiquetada é diferente de um tipo misto porque o tipo misto não exige uma etiqueta; é possível definir um tipo misto "número-ou-string" consistindo de números ou strings, por exemplo, sem definir novos construtores para o tipo novo. Embora a diferença possa parecer trivial, em muitos casos a ausência de tags é bastante conveniente. Por exemplo, alguns exercícios do HtDP definem uma "página Web" como uma lista contendo símbolos (palavras) e outras páginas Web (subpáginas). (I know, I know.) Um exemplo de "página Web" seria algo como:
(list 'Eis 'um 'exemplo 'de 'página 'web
(list 'the 'quick 'brown 'fox 'had 'better 'things 'to 'do)
(list 'whatever 'whatever 'bla))
Em Haskell, uma definição para esse tipo de dados ficaria algo como:
data Webpage = List [WebpageContent] data WebpageContent = Word String | Sub Webpage
E o exemplo ficaria:
List [Word "Eis", Word "um", Word "exemplo", Word "de", Word "página", Word "web",
Sub (List [Word "the", Word "quick", Word "brown", Word "fox", Word "had",
Word "better", Word "things", Word "to", Word "do"]),
Sub (List [Word "whatever", Word "whatever", Word "bla"])]
Que é "um pouco" menos conveniente. Poder-se-ia argumentar que a escolha de representação é tosca, mas de qualquer forma, uma vez que o meu objetivo era permitir transcrever os exercícios do HtDP para Faz com o mínimo de turbulência, eu queria encontrar alguma maneira de integrar os tipos mistos do HtDP na linguagem da maneira mais direta possível.
Então pensei eu: e que tal se adicionarmos uniões de tipos na linguagem? Uniões representam diretamente a idéia de tipos mistos. O usuário simplesmente diz:
tipo Coisas = Números U Strings
e agora 42 e "foo" pertencem ao tipo Coisas, sem necessidade de declarar tags. (Por baixo dos panos, a implementação guarda "tags" para saber os tipos dos valores, como em qualquer linguagem dinamicamente tipada, mas isso é um detalhe de implementação que não interessa ao usuário.) Simples, hã? Agora temos tipos mistos e tipagem estática. (By the way, a declaração acima é válida em Faz.)
Estranhamente, entretanto, aparentemente nenhuma linguagem estaticamente tipada usada por mais do que duas pessoas suporta uniões de tipos. Por que será?
Haskell e companhia suportam uma coisa chamada de polimorfismo paramétrico (também conhecida por tipos genéricos no mundo C++/Java). Nessas linguagens é possível declarar coisas como "listas de α, para todo α", ao invés de declarar um tipo novo para cada tipo de lista que se deseja utilizar. Também é possível escrever funções de tipos genéricos. Por exemplo, uma função para incluir um elemento em uma lista nessas linguagens possuiria um tipo como (α, lista de α) → lista de α, i.e., uma função que recebe um argumento de um tipo α qualquer, uma lista de elementos do mesmo tipo α, e produz uma lista do mesmo tipo. Uma função que implementa o operador de composição de funções (f∘g), i.e, que recebe duas funções e produz uma terceira função que é equivalente a aplicar a segunda sobre o resultado da primeira, teria um tipo como (α→β, β→γ) → (α→γ), indicando que as funções podem ser de quaisquer tipos, mas o resultado da primeira tem que ser do mesmo tipo do argumento da segunda (β), e a função resultante recebe um argumento do mesmo tipo do da primeira (α) e produz um resultado do mesmo tipo do da segunda (γ).
A verificação/inferência de tipos nessas linguagens é feita usando o famoso Hindley-Milner type system e extensões do mesmo. Os detalhes podem ser um pouco sórdidos, mas, a menos que eu esteja viajando completamente, a idéia do Hindley-Milner é extremamente simples: ao checar uma expressão, gera-se uma lista de constraints (restrições) que devem ser satisfeitas para que a expressão esteja bem tipada. Por exemplo, se temos as seguintes funções (e respectivos tipos):
compose : (α→β, β→γ) → (α→γ) bool_to_int : bool→int int_to_string : int→string
então uma chamada como compose(bool_to_int, int_to_string) só é bem-tipada se:
α→β = bool→int β→γ = int→string
Esta é a lista de constraints que devem ser satisfeitos. Do primeiro constraint, tem-se que:
α = bool β = int
e do segundo,
β = int γ = string
Como não há conflito entre os constraints, tem-se que a expressão é bem-tipada, e o tipo da chamada é α→γ = bool→string. Por outro lado, uma chamada como compose(bool_to_int, bool_to_int) produziria os constraints:
α→β = bool→int => α = bool
β = int
β→γ = bool→int => β = bool
γ = int
que não podem ser satisfeitos, e portanto a expressão é mal-tipada.
O Hindley-Milner foi feito para resolver constraints de igualdade. Em uma linguagem com relações de subtipagem (e.g., em que se pode declarar um tipo funcionário como subtipo de pessoa), aplicações de função não exigem mais que os tipos dos argumentos sejam iguais aos declarados para os parâmetros, mas sim que eles estejam contidos nos tipos dos parâmetros. Por exemplo, se pessoa tem os campos nome e idade, e funcionário tem os campos nome, idade e salário, então uma função como obtém_idade, do tipo pessoa → int, pode receber tanto pessoas quanto funcionários como argumentos.
E a presença de uniões de tipos basicamente introduz relações de subtipagem da maneira mais desenfreada possível: quaisquer dois tipos A e B possuem um supertipo comum, A U B. Isso significa que se temos uma função f do tipo (α, α) -> α, uma chamada como f(1, "foo") produz os constraints:
int ⊆ α strings ⊆ α
que é satisfatível com α = int U string. Note que, na verdade, int U string é apenas um limite inferior para α: qualquer outro supertipo, como int U string U char, ou ⊤ (top, o supertipo de todos os tipos), também serviria. Porém, intuitivamente int U string é o tipo mais "útil" inferível para a expressão, no sentido de que é o que mantém a informação mais precisa de que tipo de coisas se pode fazer com o resultado.
Nem sempre, entretanto, existe um único tipo "mais útil". A relação de subtipagem entre tipos funcionais possui uma propriedade curiosa: um tipo Sparam → Sreturn é subtipo de Tparam → Treturn, ou
Sparam → Sreturn ⊆ Tparam → Treturn
se
Tparam ⊆ Sparam e Sreturn ⊆ Treturn .
[Para entender essa inversão, você pode pensar assim: um tipo (S) é subtipo de outro (T) se S puder ser usado em qualquer lugar que T possa ser usado (e.g., funcionário é um tipo de pessoa porque um funcionário pode ser usado em qualquer lugar em que uma pessoa pode ser usada). Para que uma função (f) possa ser usada no lugar de outra (g), ela não pode exigir mais do argumento do que a outra, mas pode exigir menos (e.g., se g espera funcionários, então uma função que espere pessoas pode ser usada em seu lugar, pois funções que esperam pessoas também aceitam funcionários). Por outro lado, f tem que produzir um resultado tão bom ou melhor do que o da função que ela está substituindo (e.g., se g produzia pessoas, então f tem que produzir uma pessoa ou um funcionário, pois quem vai usar o resultado da função espera trabalhar com o resultado como se ele fosse uma pessoa).]
Agora imagine que temos uma função f do tipo (α→α) → (α→α), e uma função g do tipo int U string → int. A chamada f(g) produz o constraint:
int U string → int ⊆ α → α
de onde tem-se:
α ⊆ int U string int ⊆ α
Tanto α = int quanto α = int U string são soluções válidas para os constraints, e nenhuma é evidentemente melhor que a outra.
Coisas como a chamada compose(bool_to_int, int_to_string) da seção anterior agora produzem constraints do tipo:
α ⊆ bool int ⊆ β β ⊆ int string ⊆ γ
Destas, a única variável cujo tipo é fixado pelos constraints é β; as outras duas só possuem upper e lower bounds. Novamente, a solução "óbvia" ou "mais útil" seria α = bool, γ = string. Formalizar o "mais útil" no caso geral, entretanto, é um problema não-trivial e, como visto, nem sempre existe solução (o que fazer nesses casos é uma boa pergunta).
No Hindley-Milner, sempre que o constraint solver encontra um constraint da forma variável = whatever, ele substitui todas as ocorrências da variável por whatever no tipo e nos demais constraints, mesmo que whatever seja outra variável. Isso é válido porque os constraints são igualdades. No mundo da subtipagem, entretanto, igualar as variáveis nem sempre é a melhor solução. Por exemplo, considere as seguinte funções, escritas em um pseudocódigo funcional esquisito:
foo(f: α→β, g: α→γ, h: α→γ, k: β→γ) : Tripla(α→γ, α→γ, α→γ)
= Tripla(compose(f, k), g, h)
jogo_do_pim(x: Int) : Int U String
= if x mod 4 ≠ 0 then x
else "pim"
jogo_do_pi(x: Int) : Int U String U Char
= if x == 4 then 'π'
else if x mod 4 ≠ 0 then x
else "pim"
id(x: ι) : ι
= x
(Procurando por "jogo do pim" na Web encontrei um negócio interessante.) Agora, queremos tipar a chamada:
foo(jogo_do_pim, jogo_do_pi, id, id)
que produz os seguintes constraints, um para cada parâmetro/argumento (note que cada ocorrência de id usa variáveis de tipo separadas; caso contrário, todas as chamadas de id do programa teriam que ter o mesmo tipo):
Int → Int U String ⊆ α → β Int → Int U String U Char ⊆ α → γ ι → ι ⊆ α → γ ι′ → ι′ ⊆ β → γ
Digerindo esses constraints, temos:
α ⊆ Int Int U String ⊆ β α ⊆ Int Int U String U Char ⊆ γ α ⊆ ι ι ⊆ γ β ⊆ ι′ ι′ ⊆ γ
Se fôssemos igualar variáveis a la Hindley-Milner, teríamos, pelos dois últimos constraints, que α = γ e β = γ, e portanto α = β, mas não é possível resolver os constraints assim, pois α ⊆ Int e Int U String ⊆ β. Uma solução válida é:
α = Int β = Int U String γ = Int U String U Char
o que exemplifica que identificar/unificar as variáveis em constraints da forma α ⊆ β não é uma boa idéia na presença de union types (ou subtipagem em geral). Isso significa que podemos dar tchau para o Hindley-Milner. Só que agora temos um bocado de problemas. Por exemplo, suponha que temos os seguintes constraints:
α ⊆ Listas de β β ⊆ Listas de α
Isto é um ciclo, que produziria um tipo infinito, o que em princípio é um erro. O Hindley-Milner facilmente detecta esta situação: ao encontrar o primeiro constraint, ele substitui todas as ocorrências de α por Listas de β, e o segundo constraint fica β ⊆ Listas de Listas de β. De forma geral, um ciclo sempre leva em algum ponto a um constraint em que a mesma variável aparece dos dois lados, o que é fácil de detectar. Sem igualamento de variáveis, essa abordagem não funciona.
Side note: para evitar a unificação, uma coisa que eu tinha pensado era, ao encontrar constraints do tipo α ⊆ Listas de β, substituir todas as ocorrências de α por Listas de α′, refletindo o fato de que se sabe que α é uma lista, mas não se sabe ainda de quê. O problema é que nesse caso o algoritmo entra em loop, pois:
α ⊆ Listas de β => Listas de α′ ⊆ Listas de β (expansão de α)
β ⊆ Listas de α β ⊆ Listas de Listas de α′
=> α′ ⊆ β (cortando o construtor comum)
β ⊆ Listas de Listas de α′
=> α′ ⊆ Listas de β′
Listas de β′ ⊆ Listas de Listas de α′ (expansão de β)
=> α′ ⊆ Listas de β′
β′ ⊆ Listas de α′ (cortando o construtor comum)
(... and so on ...)
Problema dos ciclos à parte, como devemos tipar uma expressão como compose(id, id)? A expressão produz os seguintes constraints:
α ⊆ ι ι ⊆ β β ⊆ ι′ ι′ ⊆ γ
Qual é a solução? Unificar as variáveis? Mas em quais casos é correto unificar e em quais não é?
A existência de uniões de tipos torna possível declarar coisas como:
f(x: Par(Int, α) U Par(α, String)) : α
= if x.first ∈ Int then x.second
else x.first
Agora se chamarmos f(Par(5, "foo")), qual é a instanciação correta para tipo de x? α = Int ou α = String? Uma solução é detectar esse tipo de coisa e proibir que o mesmo tipo paramétrico apareça múltiplas vezes em uma união com um argumento que alterna entre concreto e abstrato. Da mesma forma, parâmetros de tipos como Int U α devem ser proibidos, pois a instanciação de α é ambígua quando o argumento é Int. E α U β também é ambíguo, pois para qualquer instanciação, a instanciação "flipada" (trocando os valores de α e β) também é válida. Supostamente essas restrições resolvem o problema, mas eu não estou quite sure quanto a isso.
Com o tempo limite para concluir o TCC se aproximando e a minha paciência/interesse no problema acabando, o que eu acabei fazendo foi um sério corte orçamentário na utilização de tipos paramétricos e uniões na linguagem. Para evitar o problema da unificação de variáveis, os casos em que ela é necessária são simplesmente proibidos: constraints da forma X ⊆ Y em que tanto X quanto Y contêm variáveis abstratas de tipos são rejeitados pelo typechecker. Isso significa que coisas como compose(id, id), em que tanto o parâmetro (α→β) quanto o argumento (ι→ι) são polimórficos, são rejeitadas. É tosco, mas pelo menos some com o problema. Além disso, uniões de tipos paramétricos também possuem algumas restrições (que eu ainda não defini direito, para ser sincero; quando eu terminar o TCC pode ser que eu edite esta seção).
Certa vez um sábio disse o seguinte:
Follow! But follow only if ye be man of valour! For the entrance to this cave is guarded by a creature, so foul, so cruel, that no man yet has fought with it and lived! Bones of full fifty men are strewn about its lair! So, brave knights, if you do doubt your courage or your strength come no further, for death awaits you all, with nasty, big, pointy teeth...
Acredito que ele estava falando de union types.
Copyright © 2010-2024 Vítor De Araújo
O conteúdo deste blog, a menos que de outra forma especificado, pode ser utilizado segundo os termos da licença Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International.
Powered by Blognir.