Quais são os problemas práticos com os tipos de interseção e união?

22

Estou projetando uma linguagem de programação funcional de tipo estaticamente simples como uma experiência de aprendizado.

Parece que o sistema de tipos que eu implementei até agora poderia (com um pouco de trabalho extra) incorporar tipos de interseção e união, por exemplo, você poderia ter:

  • <Union String Integer>
  • <Union Integer Foo>
  • A interseção dos dois tipos acima seria simples Integer
  • A união dos dois tipos seria <Union String Integer Foo>

O fato de que isso é possível, é claro, não é necessário, significa que é uma boa idéia de design. Em particular, estou um pouco preocupado com as dificuldades de implementação de manter os tipos disjuntos e / ou lidar com sobreposições.

Quais são os prós / contras de incorporar esses recursos no sistema de tipos?

Mikera
fonte

Respostas:

26

Aqui estão algumas coisas a ter em mente:

  • Embora geralmente pensemos que sabemos o que queremos dizer com interseção e união da teoria dos conjuntos, houve várias perspectivas diferentes sobre o que exatamente são os tipos de interseção e união. . Portanto, vale a pena fixar isso antes de iniciar uma implementação.
  • SUMASUMA
    SUMATUMASTUMASUMATUMASTUMA
    SUMATBSTUMABSUMATBS+TUMA+B
  • Como interseções e uniões podem ser usadas para fazer afirmações mais precisas sobre o comportamento em tempo de execução de um programa, é natural que a digitação se torne sensível à ordem de avaliação. Por exemplo, os artigos (2) e (4) abaixo explicaram por que as regras "óbvias" (e razoavelmente padrão) de digitação e subtipagem para interseções e uniões são realmente prejudiciais para idiomas do tipo ML (devido à presença de efeitos colaterais e não- terminação). Você foi avisado!
  • Por razões semelhantes, a inferência global de tipo geralmente se torna impraticável ou indecidível. De fato, todo o conceito de "tipo principal" é sem dúvida um arenque-vermelho, pois uma função pode satisfazer muitas propriedades diferentes que são irrelevantes para o uso pretendido (por exemplo, " foo leva números inteiros primos para números inteiros maiores que 7"). Em vez disso, abordagens práticas para interseções e uniões (ver (3) , (4) ) geralmente são baseadas em uma combinação de inferência e verificação.

Suponho que alguns dos pontos acima possam parecer negativos, embora eu não os chamasse de "contras", mas apenas de "realidades" dos tipos de interseção e união. Por outro lado, do ponto de vista do design de linguagem, uma das razões para o esforço de apoiar cruzamentos e uniões (e para acertá-los!) É que eles permitem que propriedades mais precisas dos programas sejam expressas de maneira bastante incremental, exigindo uma transformação muito menos drástica do que, digamos, a teoria dos tipos dependentes.

Uma breve lista de leitura:

  1. Projeto da linguagem de programação Forsythe de John C. Reynolds
  2. Tipos de interseção e efeitos computacionais de Rowan Davies e Frank Pfenning
  3. Verificação prática do tipo de refinamento por Rowan Davies (dissertação)
  4. Typechecking tridirecional de Joshua Dunfield e Frank Pfenning
Noam Zeilberger
fonte
Ótima resposta, muito obrigado. Os links foram particularmente úteis e esclarecedores - por isso, obrigado por me indicar as direções certas!
Mkera