Sintese On Understanding Types, Data Abstraction, and Polymorphism

Prévia do material em texto

PONTIFÍCIA UNIVERSIDADE CATÓLICA DE MINAS GERAIS 
Instituto de Ciências Exatas e Informática – ICEI 
Departamento de Ciência da Computação 
Engenharia de Computação 
 
 
 
 
 
Hernane Velozo Rosa¹ 
hernane.rosa@sga.pucminas.br¹ 
 
 
 
TRABALHO DE PESQUISA 1 
 
 
 
 
 
 
 
Belo Horizonte 
2022 
Hernane Velozo Rosa 
 
 
 
 
 
TRABALHO DE PESQUISA 1 
“On Understanding Types, Data Abstraction, And Polymorphism” 
 
 
Trabalho apresentado como requisito de 
pesquisa de estudo dos tipos, abstração 
de dados e polimorfismo. 
 
 
Professor: Dr. Marco Rodrigo Costa 
Disciplina: Linguagens de Programação 
 
 
Palavras chaves: Estudo de linguagens 
de Programação, sintaxe, paradigmas 
de programação e polimorfismo. 
 
 
 
Belo Horizonte 
2022 
 
 
ÍNDICE 
 
O Universo Tipado e Não Tipado .............................................................................. 2 
Universo Não-tipado: o que é? ............................................................................... 2 
Tipagem Estática e Fortemente Tipada ................................................................ 2 
Aproveitando os dois mundos ................................................................................ 2 
O Cálculo Lambda (λ) .................................................................................................. 3 
O que é ...................................................................................................................... 3 
Controvérsias ............................................................................................................ 3 
Conjuntos de Valores .................................................................................................. 5 
Características; ......................................................................................................... 5 
Sistema monomórfico .............................................................................................. 6 
Sistema polimórfico .................................................................................................. 7 
Verificação e Inferência de Tipo ............................................................................... 11 
Conclusão ................................................................................................................... 12 
Referências: ................................................................................................................ 13 
 
 
 
Página 2 de 13 
 
O UNIVERSO TIPADO E NÃO TIPADO 
 
Universo Não-tipado: o que é? 
 
Neste universo, os bits são compostos por caracteres, números, apontadores, 
estrutura de dados, programas, entre outros, no qual, mesmo se fosse combinar 
uso da memória, estaríamos escovando bits sem necessidade pois não seria 
possível dizer o que está sendo representado. Em Lisp, suas expressões formam 
um universo não-tipado, no qual é usualmente construído no universo de 
bits/cadeias de caracteres. Seus programas e dados não são distinguidos, 
havendo apenas a expressão lips possuem propriedades melhores que as de 
bits/cadeias de caracteres. 
 
Tipagem Estática e Fortemente Tipada 
 
Nesta tipagem, no que diz respeito a verificação estática, significa que o 
compilador conhece os seus tipos de dados em tempo de compilação e não 
permitirá compilar um programa com conflitos de tipo, permitindo que o 
compilador economize em memória e tempo, tudo isso de maneira segura, sem 
que haja os famosos “core dumps”. 
Uma vez que seja compilado, eliminamos erros de tipagem, com por exemplo, 
uma função que espera receber um tipo inteiro e recebe uma cadeia de 
caracteres. 
Aproveitando os dois mundos 
 
Enquanto isso, é sabido que linguagens tidas como modernas, atualmente 
suportam tipos fortemente tipados. OCaml oferece um bom suporte entre os dois 
universos, no qual é estaticamente tipada, mas ao mesmo tempo não é 
necessário escrever declarações explicitas, pois, seu compilador infere os tipos 
para o programador. 
 
 
 
Página 3 de 13 
 
O CÁLCULO LAMBDA (Λ) 
 
O que é 
 
O cálculo lambda, criado pelo matematico Alonzo Church, pode ser visto como 
uma teoria de funções onde um algoritmo é dado para produzir um valor através 
de um input e então representado por uma abstração lambda na qual o termo A 
descreve as operações devem ser realizadas da entrada. Por ser “turing 
complete”, ou seja, possui regras que seguem em sequência sobre os dados 
arbitrários que podem produzir resultado de qualquer cálculo, ele pode ser base 
para as linguagens de programação. Além disso, enquanto um sistema de 
reescrita confluente, qualquer termo pode ser substituído pelo seu valor que 
suporta uma massiva avaliação. 
 
Figura 2.0 - Representação Cálculo Lambda 
 
Disponível em: https://www.sciencedirect.com/topics/computer-science/lambda-calculus 
 
Controvérsias 
 
Contudo, o cálculo puramente possui fraquezas como a dificuldade em raciocinar 
sobre programas ou implementa-los com o seu uso, suas representações de 
funções recursivas carecem de formas normais – acarretando na avaliação 
parcial – pois é necessário evitar desdobramentos inúteis de pontos fixos, além 
de não ser combinatório no sentido de que as traduções sejam conhecidas a 
 
Página 4 de 13 
 
para a lógica combinatória e que não preserva a redução, ademais, não há 
relação entre a lógica combinatória com o cálculo lambda. 
Sua sintaxe no universo não tipado par ao tipado possui a sintaxe de que a 
função identidade e a função sucessora podem ser especificadas neste cálculo 
utilizando o valor de uma palavra-chave para introduzir um novo nome que seja 
vinculado a um valor/função, por exemplo: 
 
value id = fun(x) x -- identity function 
value succ = fun(x) x+1 -- successor function (for integers) 
 
Então, a função identidade pode ser aplicada ao cálculo da expressão em sim a 
fim de definir a adição de números inteiros no cálculo lambda puro, enquanto no 
cálculo lambda tipado, que possui algumas características semelhantes ao não-
tipado, nele cada variável deverá ser informada de forma explicita quando uma 
variável que é vinculada for informada, permitindo, assim, que a função 
sucessora tenha o seguinte formato: 
 
value succ = fun(x: Int) x +1 
 
 
 
É possível notar que essa notação funcional em certas LP tipadas omite a 
especificação do tipo do resultado, sendo denotado como resultado, este 
podendo ser determinado a partir de um corpo de um função x + 1, além de seus 
mecanismos de inferência permitirem a recuperação da informação durante a 
compilação. 
 
 
Página 5 de 13 
 
CONJUNTOS DE VALORES 
 
Características; 
 
Para caracterizar o sistema de tipo, conforme seções anteriores, onde é visto 
que regras informais para construção linguísticas. A partir dela, é possível 
caracterizar, a nível intuitivo, podendo também ser formalizadas como um 
sistema de inferência de tipo. 
Figura 3.0 - Representação e características do sistema de tipos. 
 
 
Disponível em: 
https://medium.com/@1jpablo1/illustrated-guide-to-types-sets-and-values-8093d0b7d648 
 
Um tipo é um conjunto de elementos de A onde nem todos os subconjuntos de 
A possuem tipos legais no qual devem obedecer a certas propriedades. Logo, 
um tipo é um ideal que é um conjunto de valores. Ademais, o conjunto de ideias, 
(tipos) quando é ordenado por inclusão de conjunto, formará uma malha. Sua 
parte inferior (grelha) pode dizer que é um trivial conjunto vazio. Um valor pode 
possuir muitos tipos e o conjunto de tipos de qualquer linguagem de 
programação é, geralmente, apenas um subconjunto menor de todas as ideias 
(tipos). 
 
Página 6 de 13 
 
Há ainda um sistema de tipo um tanto quanto particular no qual é identificado 
através de uma linguagem de expressão de tipo juntamente com o mapeamento 
desde expressões de tipos a ideais. 
Figura 3.1 – Exemplo de uma lista. 
 
Disponível em:https://medium.com/@1jpablo1/illustrated-guide-to-types-sets-and-values-8093d0b7d648 
 
Sistema monomórfico 
 
Além disso, um sistema de tipo monomórfico é aquele em que cada valor 
pertence a um tipo. Entretanto, como esses tipos são conjuntos, um valor pode 
pertencer a muitos tipos (ideias). 
 
Figura 3.2 - Representação de um sistema monomórfico. 
 
Disponível em: https://www.researchgate.net/figure/The-top-down-computation-of-the-
monomorphic-sets_fig1_2528716 
 
Página 7 de 13 
 
Sistema polimórfico 
 
Todavia, em um sistema de tipo polimórfico que é dado por grandes coleções de 
valores pertencem a diversos tipos, apesar de haver uma área cinzenta de 
sistemas na qual sua maioria é monomórfica e quase polimórfica e, por isso, 
suas definições são imprecisas. 
Figura 3.1 – Representação de um subset 
 
Disponível em: https://medium.com/@1jpablo1/illustrated-guide-to-types-sets-and-values-
8093d0b7d648 
 
Quantificações I: Universal 
Com uso do cálculo Lambda (λ) é possível expressar funções monomórficas, 
porém, não se pode modelar de maneira concisa funções polimórficas. Logo, 
pode se dizer que a quantificação universal e um tipo genérico de abstração 
composta por; função identidade: que pode ser definida como tipos específicos 
como fun(x: Int)x. Ou seja, não é possível expressar a ideia de uma forma 
funcional sem que seja a mesma para uma diversidade de tipos. Além disso, é 
necessário vincular, de maneira explicita, as variáveis e valores a um tipo 
específico. Seu fato pode ser dado de forma funcional e ser a mesma para todos 
os tipos expressando-se de maneira universal. Abaixo, uma forma de expressar 
a função identidade: 
Value id = all [ a ] fun( x : a ) x 
 
 
Página 8 de 13 
 
Logo, conforme a definição de ID, a é uma variável de tipos e tudo [ a ] fornece 
a abstração de tipo para um de modo que ID é a identidade para toso os tipos. 
 
Figura 4.0 – Representação teórica da quantificação 
 
Disponível em: 
https://leanprover.github.io/logic_and_proof/natural_deduction_for_first_order_logic.html 
 
Para aplicar a função identidade, é necessário um argumento de tipo específico 
no qual deve-se primeiro ser fornecido o tipo como um parâmetro e então o 
argumento como dado, isto é, { id [Int] (3) } onde, por convenção, os parâmetros 
de tipo deverão estar entre colchetes, enquanto os argumentos entre parênteses 
onde o ID é a função identidade genérica, além de ser um operador de ligação. 
Importante diferenciar que enquanto [ a ] é utilizado para atar um da fun, embora 
fun(x:a) seja utilizado para atar uma variável de um tipo determinado, que pode 
ser genérico, todavia, não há restrição quanto ao manipulamento dos tipos, além 
dos que são distintos e abstrações servem, também, para verificar o tipo. 
Exemplo: { value id = fun(x:a) x } onde a é uma variável de tipo livre. 
É possível notar que o algoritmo de verificação possui a tarefa de reconhecer 
que a é uma variável de tipo livre e que reintroduz a informação original a [ a ] e 
[ Int ]. Logo, é notório o que um verificador polimórfico é capaz de fazer. Agora 
um exemplo de paramento universal quantificado; note que a função inst recebe 
uma função e devolver duas instancias: 
value inst = fun( f: "a. a ® a) ) ( f[ Int ], f[ Bool ] ) 
value intid = fst( inst(id) ) : Int ® Int : Bool ® Bool 
value boolid = snd( inst(id) ) 
 
 
Página 9 de 13 
 
Então, com a abstração de função (Lambda), a separação entre os tipos e 
valores é obtida de diferentes operações de ligação entre tipos, valores e 
variáveis, sendo útil na modelação do polimorfismo paramétrico. 
Figura 4.1 – Exemplo de uma lista. 
 
Disponível em: 
http://www.cs.sjsu.edu/~pearce/modules/lectures/oop/types/generics/generics.htm 
 
Quantificações II: Existencial 
Na segunda parte das quantificações, chega o momento de introduzir a parte 
existencial cuja atividade é predicação de um elemento em dado domínio. Isto é, 
grosso modo, a restrição do adjunto extra à esquerda de um morfismo 
geométrico. 
Ela é denotada pelo operador lógico ∃. Aprofundando, temos que existe ao 
menos um x tal que P(x) é chamado de um quantificador existencial no qual x 
significa um objeto no universo. Logo, temos que, com uma simples proposição, 
“Uma pessoa te ama”; onde é possível transformar na forma proposicional x P(x) 
no qual P(x) é o predicado x “ama-te”. 
Sua semântica corresponde ao longo da projeção de um produto cuja 
interpretação pode ser de um tipo T e A é a interpretação desse tipo. Além disso, 
ainda há nos termos de lógica interna conforme visto acima que um tipo x é dado 
por um objeto x. 
 
Página 10 de 13 
 
Figura 4.0 – Representação teórica existencial 
 
Disponível em: https://en.wikipedia.org/wiki/Universal_quantification 
 
Quantificações III: Limitada 
Introduzida na linguagem Fun e proposto por Luca Cardelli e Wegner, a noção 
da quantificação limitada, também conhecida como polimorfismo limitado, é dada 
em ideais informais e formalizadas na qual integra o polimorfismo e o cálculo de 
primeira ordem de subtipo. Esse tipo de quantificação permite a tipagem de 
função que são aplicadas em tipos recursivos, isto é, um tipo recursivo é aquele 
que inclui uma função que o utiliza como um tipo para algum argumento ou valor 
de retorno. Tem como proposito permitir que funções polimórficas dependam 
apena de um comportamento específico de objetos ao invés da herança de tipo. 
 
Figura 5.0 – Representação teórica limitada 
 
Disponível em: https://zhenjiang888.github.io/PL/2022/slides/hu_ch26.pdf 
 
 
Página 11 de 13 
Por exemplo, esse tipo de restrição pode ser expresso como uma interface 
genérica (Java). Além disso, é possível descrever tipos que podem ser 
comparados entre si e utilizar isso como uma forma de obter informações acerca 
de funções polimórficas. 
Por exemplo: 
min: ∀T∀ S que compara com T0: T → int ou S → S → S 
fmin: ∀ T∀ S que comparavel [ T ] T → T → T 
interface comparavel < T > { 
 public int compara ( T other ); 
} 
class Integer implements comparavel < Integer > { 
 @Override 
 public int compara( Integer other ) { 
 // ... 
 } 
} 
VERIFICAÇÃO E INFERÊNCIA DE TIPO 
Quanto as verificações e inferências de tipos, pode-se dividir em três grupos 
sendo o estático que pode rejeitar um programa antes de executar para evitar 
que haja erros; 
fun f x = (infere valor de f : int -> int) fun g x = (reporta o erro) 
if x > 3 if x > 3 
then 42 then true 
else x * 2 else x * 2 
Dado uma expressão A, o tipo inferência irá computar todas as variáveis em A. 
Utilizar desses tipos para determinar o tipo e subtipo e sub-expressoes. O tipo 
de inferência tem a implementação dada como uma passagem antes do 
verificador de tipo. 
Página 12 de 13 
Figura 6.0 – Representação de um processo de inferência 
Disponível em: https:/cs.wellesley.edu/~cs251/f19/slides/ml-inference.pdf 
CONCLUSÃO 
Com esse trabalho foi possível entender as diferenças entre tipos, 
abstração de dados, polimorfismo e como eles se conectam. Será discutido 
na sala de aula através de um "pitch" entre os demais alunos alguns pontos 
marcantes quanto ao artigo estudado.
 
Página 13 de 13 
 
REFERÊNCIAS: 
 
 
Cardelli, Luca; Wegner, Peter. On understanding types, data abstraction, and 
polymorphism. Computing Surveys. Vol. 17. Nº 4. December 1985. Pgs. 471-489 
 
Existential Quantifier, Ncatlab. Disponível em: 
<https://ncatlab.org/nlab/show/existential+quantifier#in_type_theory> 
Acesso em: 27 de outubro. de 2022 
 
Quantification - Forming Propositions from Predicates. Disponível em: 
<https://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/quantification/quantification.html 
Acesso em: 01 de novembro. de 2022 
 
 
Bounded Quantification. Disponível em: 
https://dbpedia.org/page/Bounded_quantification 
Acesso em: 01 de novembro. de 2022 
 
 
A Polymorphic λ-calculus with Type:Type.Disponível em: 
http://lucacardelli.name/Papers/TypeType.A4.pdf 
Acesso em: 28 de outubro. de 2022 
 
 
 
	pt0.pdf
	p1.pdf