Tipos dependentes versus tipos de refinamento

Alguém poderia explicar a diferença entre tipos dependentes e tipos de refinamento? Pelo que entendi, um tipo de refinamento contém todos os valores de um tipo que atendem a um predicado. Existe um recurso de tipos dependentes que os distingue?

Se isso ajudar, me deparei com tipos refinados pelo projeto Liquid Haskell e tipos dependentes via Coq e Agda. Dito isto, estou procurando uma explicação de como as teorias diferem.

terminology programming-languages type-theory functional-programming dependent-types jmite
fonte

Respostas:

As principais diferenças estão em duas dimensões - na teoria subjacente e em como elas podem ser usadas. Vamos apenas focar no último.

Como usuário, a "lógica" das especificações dos sistemas LiquidHaskell e do tipo de refinamento geralmente é restrita a fragmentos decidíveis, de modo que a verificação (e inferência) é totalmente automática, o que significa que não é necessário "termos de prova" do tipo necessário na íntegra. configuração dependente. Isso leva a uma automação significativa. Por exemplo, compare a classificação de inserção no LH:

http://ucsd-progsys.github.io/lh-workshop/04-case-study-insertsort.html#/ordered-lists

vs. em Idris

https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr

No entanto, a automação tem um preço. Não se pode usar funções arbitrárias como especificações, como no mundo totalmente dependente, o que restringe a classe de propriedades que se pode escrever.

Assim, um objetivo dos sistemas de refinamento é estender a classe do que pode ser especificado, enquanto o dos sistemas totalmente dependentes é automatizar o que pode ser provado. Talvez haja um local de encontro feliz, onde possamos obter o melhor dos dois mundos!

Ranjit Jhala
fonte

Existe uma maneira de mapear de alguma forma mecanicamente de especificações baseadas em tipos de refinamento para especificações baseadas em tipos dependentes? Ou esse "isomorfismo" ainda não foi estudado o suficiente?

Erik Allik

AFAIK, tal "isomorfismo", não foi muito estudado. Porém, há trabalhos recentes, veja: "Formalizando tipos simples de refinamento em Coq", de Lehmann e Tanter (que aparecerão em breve ... aqui está um repo do GH: github.com/pleiad/Refinements )

Ranjit Jhala

Que tal tipos dependentes de caminho no Scala?

Yang Bo

@RanjitJhala Eu acho que você acidentalmente conseguiu seus objetivos no parágrafo final da maneira errada?

Noldorin

@Noldorin, eu diria que Ranjit acertou seu último parágrafo. "tipo de refinamento ... restrito a fragmentos decidíveis, para que a verificação (e a inferência) sejam completamente automáticas" vs "termos de prova ... necessários em ... tipos dependentes". Assim, as pessoas que trabalham com tipos de refinamento estão tentando estender o quanto pode ser especificado em um tipo de refinamento enquanto ainda são automaticamente inferíveis / verificáveis, enquanto aqueles que trabalham com tipos dependentes estão tentando automatizar a geração de termos de prova.

raiph 20/06

$T$ $P$ $T$

{v : T ∣ P (v)}

$\{v:T \mid P(v)\}$

T

$T$ .

$\{x:T_1 \to T_2 \mid P\}$ [1]. Observe que tipos totalmente dependentes (como os tipos sigma) não são permitidos.

O sistema Liquid Type, descrito em [1], é realmente decidível e o Liquid Haskell usa solucionadores SMT. No entanto, o Liquid Haskell também exige termos de prova (ou valores, como são chamados em uma linguagem de tipo não dependente): se você se senta para escrever um programa do Liquid Haskell, escreve suas próprias funções, não apenas os tipos.

[1] http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf

Daniil
fonte

O sigma pode ser codificado com pi usando uma codificação semelhante à igreja, mas os tipos de função de refinamento do AFAIK líquido haskell não são do tipo pi (função dependente).

precisa saber é o seguinte

Tipos dependentes são tipos que dependem de valores de qualquer forma. Um exemplo clássico é "o tipo de vetores de comprimento n", onde né um valor. Tipos de refinamento, como você diz na pergunta, consistem em todos os valores de um determinado tipo que satisfazem um determinado predicado. Por exemplo, o tipo de números positivos. Esses conceitos não são particularmente relacionados (que eu saiba). Obviamente, você também pode ter razoavelmente tipos de refinamento dependentes, como "tipo de todos os números maiores que n".

Alexey Romanov
fonte

Um é um subconjunto do outro? Tipos de refinamento parece ser solucionável usando SMT, mas tipos dependentes requerem seus próprios termos de prova ...

jmite

"Um é um subconjunto do outro?" Não. Foi por isso que dei os exemplos de um tipo de refinamento que não é dependente e de um tipo dependente que não é um refinamento.

Alexey Romanov

tipos de refinamento não podem ser codificados com sigma?

precisa saber é o seguinte

Seu exemplo parece não demonstrar seu ponto de vista. Os números positivos são definidos como números maiores que 0. Isso não significa que "o tipo de números positivos" é precisamente "o tipo de todos os números maiores que 0"?

precisa saber é

Não é possível que exista um predicado de refinamento que imponha também o comprimento do vetor?

CMCDragonkai