Featherweight
Java

Um núcleo mínimo de Java com sintaxe, tipos e semântica que cabem numa página.

Seminário: Types and Programming Languages, cap. 19
Centro de Informática, UFPE Use as setas, Espaço ou PageUp/PageDown. F para tela cheia.
De onde vem

Dois jeitos de estudar objetos no TAPL

Capítulo 18: codificar

Objetos, classes e herança são montados com peças do lambda-cálculo: registros, referências e subtipagem.

Mostra o mecanismo por baixo, mas o objeto deixa de ser visível como conceito.

Capítulo 19: tratar como primitivo

Classes e objetos são construções da própria linguagem, com regras de tipo e de avaliação próprias.

É o caminho do Featherweight Java (FJ), proposto por Igarashi, Pierce e Wadler em 1999.

FJ é um subconjunto estrito de Java: todo programa FJ é um programa Java executável, com o mesmo comportamento.
Motivação

Completude contra compacidade

Um modelo formal serve para descrever uma linguagem com precisão e provar propriedades dela, como segurança de tipos.

Quanto mais recursos o modelo cobre, mais pesada fica a prova. FJ escolhe o outro extremo: corta tudo que alonga a prova sem mudar o argumento.

O resultado é útil para estender Java no papel: genéricos (GJ), raw types, classes internas e compilação que preserva tipos foram estudados sobre FJ.

Inside every large language is a small language struggling to get out. Igarashi, Pierce e Wadler (1999)
Recorte

O que FJ mantém de Java e o que corta

Mantém

  • Classes mutuamente recursivas
  • Criação de objetos e acesso a campos
  • Chamada e sobrescrita de métodos
  • Recursão aberta via this
  • Subtipagem e cast

Corta

  • Atribuição: campos só são definidos no construtor
  • Interfaces, sobrecarga, super.m(), null
  • Tipos base (int, bool), exceções
  • Classes internas, métodos abstratos, public/private
  • Concorrência e reflexão

Sem atribuição, FJ é um fragmento funcional de Java. Mesmo assim é Turing-completo: dá para codificar o lambda-cálculo nele.

Exemplo do livro

Um programa é uma tabela de classes mais um termo

class A extends Object { A() { super(); } }
class B extends Object { B() { super(); } }

class Pair extends Object {
  Object fst;
  Object snd;
  // construtor
  Pair(Object fst, Object snd) {
    super(); this.fst=fst; this.snd=snd; }
  // método
  Pair setfst(Object newfst) {
    return new Pair(newfst, this.snd); }
}

Convenções rígidas, para a sintaxe ficar regular:

  • extends sempre escrito, mesmo para Object
  • Construtor sempre presente: um parâmetro por campo, super(...) e depois this.f=f
  • Receptor sempre explícito: this.snd, nunca snd
  • Corpo de método é só return t;

super e = só aparecem dentro do construtor.

Sintaxe

A linguagem inteira tem cinco formas de termo

FormaGramáticaNo exemplo
Variávelxnewfst, this
Acesso a campot.fthis.snd
Chamada de métodot.m(t)new Pair(...).setfst(new B())
Criação de objetonew C(t)new A(), new Pair(..., ...)
Cast(C) t(Pair) t.fst

A barra em t indica sequência: t1, ..., tn.

this é tratado como variável, não palavra-chave. Ele fica implicitamente ligado em todo corpo de método.

Figura 19-1

A gramática completa

CL ::= class C extends C {C f; K M} K  ::= C(C f) {super(f); this.f=f;} M  ::= C m(C x) {return t;} t  ::= x | t.f | t.m(t) | new C(t) | (C) t v  ::= new C(v)

Valores são só objetos com todos os argumentos já avaliados. "Tudo é objeto", como no lambda-cálculo "tudo é função".

Um programa é o par (CT, t): uma tabela de classes e o termo a avaliar, que faz o papel do main.

Metavariáveis: A..E classes, f e g campos, m métodos, x parâmetros, s e t termos, u e v valores.

Seção 19.3

Em Java, o nome do tipo importa

Estrutural

NatPair = {fst:Nat, snd:Nat}

O nome é só abreviação. Subtipagem é decidida comparando a forma dos tipos.

Mais elegante para provas e para recursos avançados (polimorfismo, tipos abstratos). Domina a literatura.

Nominal

class Pair extends Object { ... }

Todo tipo tem nome, e subtipagem é a que o programador declarou com extends.

  • O nome vira etiqueta em tempo de execução: permite cast e instanceof
  • Tipos recursivos saem de graça
  • Checar C <: D é quase trivial
Figura 19-1

Subtipagem sai direto das declarações extends

 
C <: C
reflexiva
C <: D    D <: E
C <: E
transitiva
CT(C) = class C extends D {...}
C <: D
extends

A tabela de classes CT mapeia cada nome de classe para sua declaração.

Object é especial: não está na tabela, não tem campos nem métodos.

Condições de sanidade da tabela:

  • toda classe citada existe em CT
  • Object não está em CT
  • não há ciclo em <:
Cachorro<:Mamifero<:Animal<:Object Logo: Cachorro <: Animal pela transitividade. Gato e Cachorro são irmãos, não subtipos entre si.
Figura 19-2

Quatro consultas à tabela de classes

FunçãoDevolveComo
fields(C)todos os campos C f, herdados primeirocampos de D (superclasse) seguidos dos de C; fields(Object) é vazio
mtype(m, C)tipo B → Bprocura m em C; se não achar, sobe para a superclasse
mbody(m, C)par (x, t): parâmetros e corpomesma busca subindo a hierarquia: é aqui que mora a sobrescrita
override(m, D, C→C0)sobrescrita válida?se m existe em D, o tipo tem que ser idêntico

Exemplo: fields(Pair) = Object fst, Object snd e mbody(setfst, Pair) = (newfst, new Pair(newfst, this.snd)).

Camada intuitiva: fields(Cachorro) = • · mtype(falar,Cachorro) = [] → Som · mbody(falar,Cachorro) = ([], new Latido())
Figura 19-3, TAPL p. 258

Duas famílias de regras, dois papéis diferentes

Figura 19-3 do TAPL: regras de avaliação do Featherweight Java
Pierce, Types and Programming Languages, cap. 19, Figura 19-3, p. 258.
3
Computação

Faz o passo real: campo, método ou cast.

5
Congruência

Leva a avaliação até o próximo subtermo.

t ⟶ t': “t reduz para t' em um passo”.
E-ProjNew

Como buscar um campo de um objeto?

new Pair(new A(), new B()).snd
⟶
new B()
fields(Pair) = Object fst, Object sndsnd é o 2º campo ⟹ recupera o 2º argumento

Conclusão: o formato padronizado do construtor permite projetar por posição.

E-CastNew

Um cast muda o objeto?

(Animal) new Cachorro()
⟶
new Cachorro()
Cachorro <: Animalo teste passa e o cast desaparece

Conclusão: o cast só verifica a hierarquia; não altera o objeto.

E-New-Arg + E-ProjNew

O construtor externo já é um valor?

new Pair(new Pair(new A(), new B()).fst, new B())
E-New-Argentra no 1º argumento+E-ProjNew.fst vira new A()
⟶
new Pair(new A(), new B())

Conclusão: call-by-value avalia os argumentos antes de considerar new C(...) um valor.

Tipo estático ≠ classe real

Por que o exemplo do livro precisa de cast?

new Pair(new Pair(new A(),new B()), new A()).fstclasse real: Pair
O verificador enxerga:fst : Object

fields(Object) é vazio; então .snd não tipa.

Recuperamos precisão:((Pair) ... .fst).snd

O cast torna o receptor tipável como Pair; em runtime ele confere a classe real.

Conclusão: o tipo estático vem da declaração do campo; a classe real vem do valor armazenado.

E-InvkNew

setfst: buscar o corpo e substituir

Termo
new Pair(new A(), new B()).setfst(new B()) mbody = (newfst, new Pair(newfst, this.snd))⟶ new Pair(new B(), new Pair(new A(), new B()).snd)⟶ new Pair(new B(), new B())
newfst↦new B()this↦receptor
Uma ideia por passo
receptor e argumento são valores
E-InvkNew já pode ser aplicada.
mbody(setfst, Pair)
Consulta devolve o parâmetro e o corpo.
substituição simultânea
Parâmetro recebe argumento; this recebe receptor.
E-New-Arg + E-ProjNew
this.snd vira new B().
mbody + sobrescrita

Qual corpo de falar() executa?

class Animal extends Object {
  Som falar() { return new Som(); }
}
class Cachorro extends Animal {
  Som falar() { return new Latido(); }
}
new Cachorro().falar()⟶new Latido()
mbody(falar, Cachorro)encontra primeiro o método de Cachorro

Conclusão: a classe real do receptor decide onde a busca começa; a sobrescrita de Cachorro vence.

Sem regra aplicável

Três jeitos de ficar stuck

campo inexistente

new A().fst

fields(A) é vazio; E-ProjNew não se aplica.

T-Field rejeita antes
método inexistente

new A().setfst(new B())

mbody(setfst,A) é indefinido; E-InvkNew não se aplica.

T-Invk rejeita antes
cast preso

(Gato)new Cachorro()

Cachorro <: Gato é falso; E-CastNew não se aplica.

T-SCast pode tipar; runtime trava
regra de computação?nenhuma casatermo stuck

Tipagem elimina campo e método inexistentes. Um cast preso continua sendo a exceção de progresso.

Figura 19-4

Uma regra de tipo para cada forma de termo

x:C ∈ Γ
Γ ⊢ x : C
T-Var
Γ ⊢ t0 : C0    fields(C0) = C f
Γ ⊢ t0.fi : Ci
T-Field
Γ ⊢ t0 : C0   mtype(m, C0) = D→C   Γ ⊢ t : C   C <: D
Γ ⊢ t0.m(t) : C
T-Invk
fields(C) = D f    Γ ⊢ t : C    C <: D
Γ ⊢ new C(t) : C
T-New

Lê-se Γ ⊢ t : C como "no ambiente Γ, o termo t tem tipo C". Ex.: Γ ⊢ new Gato() : Gato.

Não há subsunção solta: o <: aparece onde é preciso. Cada termo tem um tipo mínimo único.

Figura 19-4

Cast tem três regras, e uma delas é "estúpida"

Γ ⊢ t0 : D    D <: C
Γ ⊢ (C)t0 : C
T-UCast
upcast
Γ ⊢ t0 : D   C <: D   C ≠ D
Γ ⊢ (C)t0 : C
T-DCast
downcast
Γ ⊢ t0 : D   C ≮: D   D ≮: C   stupid warning
Γ ⊢ (C)t0 : C
T-SCast
stupid cast

O compilador Java rejeita cast entre classes não relacionadas. Por que FJ aceita?

Porque um termo bem tipado pode virar um assim durante a avaliação:

(A)(Object)new B()   // T-DCast: ok
⟶ (A)new B()          // só T-SCast tipa

Sem T-SCast, a preservação de tipos seria falsa. Uma tipagem FJ só corresponde a uma tipagem Java se não usar essa regra.

(Animal)new Gato()T-UCast · sempre seguro(Gato)(Animal)new Gato()T-DCast · checa em runtime(Cachorro)new Gato()T-SCast · classes irmãs
Figura 19-4

Métodos e classes também são verificados

x:C, this:C ⊢ t0 : E0   E0 <: C0
CT(C) = class C extends D {...}   override(m, D, C→C0)
C0 m(C x) {return t0;} OK in C
método
K = C(D g, C f) {super(g); this.f=f;}
fields(D) = D g    M OK in C
class C extends D {C f; K M} OK
classe
  • Método: o corpo é tipado com os parâmetros e com this : C. O resultado pode ser subtipo do declarado.
  • Sobrescrita exige o mesmo tipo da superclasse.
  • Classe: o construtor tem que passar os campos herdados para super e inicializar os próprios.
  • Sem circularidade: os tipos dos métodos são declarados, então a ordem não importa.
Seção 19.5

Bem tipado não trava, exceto em downcast

Preservação

Se Γ ⊢ t : C e t ⟶ t', então Γ ⊢ t' : C' para algum C' <: C.

O tipo pode ficar mais específico durante a avaliação, nunca diferente.

Exemplo: (Object)new A() tem tipo Object e avança para new A(), de tipo A.

Progresso

Se t é fechado, bem tipado e não avança, então t é um valor ou t = E[(C)(new D(v))] com D ≮: C.

A única forma de travar é um downcast que falha. Campo e método inexistentes nunca acontecem.

Se o programa só tem upcasts, ele nunca trava. Em Java completo, o cast que falha vira exceção.

Preservação: um passo não estraga o tipo.Progresso: bem tipado não fica sem passo, salvo cast preso; ele pode surgir de downcast ou T-SCast.
Exercícios do livro

Três perguntas que ajudam a fixar o modelo

Exerc.PerguntaIdeia da resposta
19.4.1Por que não há regra dizendo que Object é supertipo de tudo, como S-Top?Toda classe declara uma superclasse e não há ciclos, então toda cadeia de extends termina em Object. A transitividade já dá C <: Object, e os únicos tipos são classes.
19.4.3Como adicionar atribuição a campos?Seguir o capítulo 13: introduzir locações e uma memória (heap). Objetos passam a ser referências, e a avaliação deixa de acontecer só na sintaxe.
19.4.7Como adicionar super.m()?A busca do corpo precisa começar na superclasse da classe onde o método foi escrito, não na do receptor. O corpo tem que lembrar a classe que o definiu.
Seção 19.6

As duas visões se complementam

Codificação (cap. 18)

  • Expõe os mecanismos de encapsulamento e reuso
  • Mostra como um compilador traduz objetos para algo mais baixo nível

Primitivo (cap. 19)

  • Fala de tipos e avaliação de objetos diretamente
  • Melhor ferramenta para projetar e documentar uma linguagem
O ideal tem as duas: uma linguagem de alto nível com regras próprias, uma tradução para registros e funções, e uma prova de que a tradução preserva tipos e avaliação. Para FJ isso foi feito por League, Trifonov e Shao (2001).
Para levar

Featherweight Java em uma página

  • Cinco termos: variável, campo, método, new e cast
  • Subtipagem nominal, vinda direto de extends
  • Três regras de computação e avaliação por valor, sem heap
  • Três regras de cast, incluindo o "stupid cast" para a preservação funcionar
  • Segurança: bem tipado só trava em downcast
Pierce, B. C. Types and Programming Languages, MIT Press, 2002, cap. 19.
Igarashi, A.; Pierce, B. C.; Wadler, P. Featherweight Java: a minimal core calculus for Java and GJ. OOPSLA 1999; ACM TOPLAS 23(3), 2001.