Gerando restrições para resolver metavariáveis ​​de tipo dependente?

8

Nos tipos dependentes, a unificação de padrões de Miller é usada para resolver um fragmento decidível da unificação de ordem superior. Isso permite que idiomas de tipo dependente contenham metavariáveis ​​ou argumentos implícitos.

Existem muitos trabalhos que descrevem, dado um problema de unificação no fragmento de padrão, como encontrar uma solução, se houver. Os exemplos incluem (Gundry-McBride) , (Abel-Pientka) e o artigo original de Miller .

O que eu queria saber é que, dado um programa dependente de digitação que contém metavariáveis ​​(ou argumentos implícitos), como alguém gera os problemas que são passados ​​para o solucionador de unificação?

jmite
fonte
Você já olhou a tese de Norell? cse.chalmers.se/~ulfn/papers/thesis.pdf
adamse
A idéia básica é que você verifique o tipo bidirecional, mas unifique com metas em vez de usar o caso.
Fread2281
@amamse Tenho, apesar de admitir, que tive muita dificuldade para entender e ver onde as restrições reais são geradas.
jmite
2
eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf descreve a elaboração de Idris e pode ter um pouco do que você deseja, seção 4 em particular
Edwin Brady
11
Para implícitos, você precisa ser capaz de lidar com os buracos, também conhecidos como meta-variáveis, nos tempos de certificação G | - t: A. No pior dos casos, você acaba com o problema de habitação. pt.wikipedia.org/wiki/Type_inhabitation
Mostowski Collapse

Respostas:

8

Há um bom idioma, que é explicado mais no capítulo 22 de Tipos e linguagens de programação (é usado para polimorfismo em vez de tipos dependentes, mas a idéia é a mesma). O idioma é o seguinte:

Um sistema de verificação de tipo pode ser transformado em um sistema de inferência de tipo , tornando as regras lineares e adicionando restrições .

Vou usar a regra do aplicativo como exemplo. A regra de verificação em tipos dependentes é esta:

Γt:Πx:A.BΓu:AΓt u:B[u/x]

A linearização dessa regra requer renomear as 2 ocorrências deA, de modo que obtemos:

Γt:Πx:A1.BΓu:A2Γt u:B[u/x]

Mas isso não está mais correto! Precisamos adicionar a restrição A1 1UMA2:

Γt:Πx:A1.BΓu:A2Γt u:B[u/x]A1A2

Observe que denota módulo de equivalência sua relação de conversão (βη, normalmente), assim como na regra de conversão, mas agora é uma restrição de unificação , pois você pode ter meta-variáveis ​​em seus termos.

No curso da verificação de tipo, você acumulará restrições como essas, para potencialmente resolvê-las todas de uma vez no final (ou mais cedo por razões de eficiência).

Agora as coisas podem ficar mais complicadas, porque o tipo de tem si poderia ser uma meta-variável no contexto! Uma regra mais geralmente aplicável seria, portanto,

Γt:CΓvocê:UMA2Γt você:B[você/x] CΠx:UMA1 1.B, UMA1 1UMA2

Ou, como alternativa, mantendo a regra anterior e adicionando a regra

Γ1 1,x:C,Γ2x:UMACUMA

no tempo de pesquisa variável.

Outra observação útil é que, no sistema de verificação , a regra de conversão precisa ser aplicada apenas antes dos aplicativos e, possivelmente, uma vez no final da derivação. Como essas regras correspondem a uma restrição de unificação no sistema de inferência , isso indica onde colocar as restrições.

cody
fonte
Isso é muito útil. Você conhece alguma referência que descreva um sistema completo para isso? Em particular, estou tendo problemas para gerar restrições para expressões lambda, lidando com as variáveis ​​livres dos tipos Pi.
jmite
11
Temos um artigo sobre o arXiv que fornece detalhes minuciosos. Você provavelmente estaria mais interessado na seção 3.5, embora eu tenha medo que não seja tão didático quanto eu gostaria.
Cody
@ j4nbur53: está correto, você realmente precisa resolver essa restrição em geral. Na maioria das vezes, porém, obter o tipo det como um Π-type é bastante fácil, e o correspondente B(x)vem como consequência. Essa idéia está implícita na noção de verificação de tipo bidirecional .
Cody
De fato quero dizer B(x), pois é isso que você está procurando (obtendo B(você)é trivial a partir daí). Não sei ao certo o que você quer dizer com "(=) / 2 introdução". No primeiro link, o sistema com restrições é linear.
Cody
No artigo, assumimos qualquer coisa, incluindo t, pode ser uma meta-variável. Nesse caso, e na ausência de restrições adicionais sobret, consideramos que o problema está sub-restrito e fornecemos uma mensagem de erro (como seria Coq). Eu argumentaria que esse é o comportamento correto. Obviamente, se o tipo detnessa situação é, por exemplo, o testemunho de uma habitação de classe de tipo, então você desejará uma rotina especializada para procurar esse habitante.
03/03
4

Se você modelar os termos lambda por meio de índices deBruijn e as meta-variáveis ​​por meio de variáveis ​​Prolog, poderá criar um solucionador de restrições Prolog. Aqui está um exemplo que já funciona muito bem, as restrições básicas usadas são as seguintes:

% shift (+ Indexado, + Nat, + Nat, -Indexado)
% subst (+ Indexado, + Nat, + Indexado, -Indexado)
% de redução (+ Indexado, + Indexado, -Indexado)
https: //gist.github. com / jburse / 0ccd12698bfa24ce5c36 # file-implicit2-p

Todo o maquinário também assume que lutamos por formas normais, pois reduzimos beta em uma determinada ordem. Há uma interação entre o normalizador e como novas restrições acima são geradas. Como reduzir um redex pode exigir reavaliação da normalização.

O solucionador de restrições já implementa algumas simplificações de restrições cruzadas, sem essas simplificações e apenas com um atraso de restrição, o solucionador de restrições seria burro demais e praticamente não utilizável. Ainda estamos planejando adicionar mais uma ou duas simplificações. Um tesouro para simplificações é o seguinte artigo:

Teoria Residual em λ-calculus
A Desenvolvimento Formal, Gerard Huet, 1998
http://pauillac.inria.fr/~huet/PUBLIC/residuals.pdf

No artigo, encontramos também as definições indutivas originais das restrições que estávamos usando. Consulte as seguintes seções:
2.2 Elevação
2.3 Substituição
3.1 Redução β de uma etapa

Aviso: Os termos deBruijn nos ajudam na igualdade dos termos normais, não precisamos de nenhuma etapa para a conversão alfa. Mas usamos um tipo dependente não nivelado, portanto, por exemplo, não há distinção entre tipos e tipos sob o capô. Isso torna todo o empreendimento especialmente simples; por outro lado, isso não é padrão.

Tchau

Mostowski Collapse
fonte
Portanto, você não usa a unificação de Prolog para suas metas representadas como variáveis ​​de Prolog e resolve suas próprias restrições?
Saizan