Tipos dependentes sobre o tipo codificado pela igreja em PTS / CoC

Estou experimentando sistemas de tipo puro no cubo lambda de Barendregt, especificamente com o mais poderoso, o Cálculo de Construções. Este sistema tem tipos *e BOX. Apenas para constar, abaixo, estou usando a sintaxe concreta da Morteferramenta https://github.com/Gabriel439/Haskell-Morte-Library, que fica próxima ao cálculo lambda clássico.

Vejo que podemos emular tipos indutivos por algum tipo de codificação semelhante à Igreja (também conhecido como isomorfismo de Boehm-Berarducci para tipos de dados algébricos). Para um exemplo simples, eu uso type Bool = ∀(t : *) -> t -> t -> tcom os construtores True = λ(t : *) -> λ(x : t) -> λ(y : t) -> xe False = λ(t : *) -> λ(x : t) -> λ(y : t) -> y.

Vejo que o tipo de funções de nível de termo Bool -> Té isomórfico para pares de tipo Product T Tcom Product = λ(A : *) -> λ(B : *) -> ∀(t : *) -> (A -> B -> t) -> tparametricidade clássica de módulo por meio de função if : Bool -> λ(t : *) -> t -> t -> tque é de fato identidade.

Todas as perguntas abaixo serão sobre representações de tipos dependentes Bool -> *.

1. Eu posso dividir D : Bool -> *em par de D Truee D False. Existe a maneira canônica de criar Dnovamente? Quero reproduzir o isomosfismo Bool -> T = Product T Tpor um análogo de função ifno nível de tipo, mas não posso escrever essa função tão simples quanto o original, ifporque não podemos passar tipos em argumentos como tipos.

2. Eu uso um tipo de tipo indutivo com dois construtores para resolver a questão (1). A descrição de alto nível (estilo Agda) é o seguinte tipo (usado em vez do nível de tipo if)

   data BoolDep (T : *) (F : *) : Bool -> * where
     DepTrue : T -> BoolDep T F True
     DepFalse : F -> BoolDep T F False
   

   com a seguinte codificação em PTS / CoC:

   λ(T : *) -> λ(F : *) -> λ(bool : Bool ) ->
   ∀(P : Bool -> *) ->
   ∀(DepTrue : T -> P True ) ->
   ∀(DepFalse : F -> P False ) ->
   P bool
   

   Minha codificação acima está correta?

3. Eu posso escrever os construtores BoolDepcomo este código para DepTrue : ∀(T : *) -> ∀(F : *) -> T -> BoolDep T F True:

   λ(T : *) ->  λ(F : *) ->  λ(arg : T ) ->
   λ(P : Bool -> *) ->
   λ(DepTrue : T -> P True ) ->
   λ(DepFalse : F -> P False ) ->
   DepTrue arg
   

mas não posso escrever a função inversa (ou qualquer função na direção inversa). É possível? Ou devo usar outra representação para BoolDepproduzir um isomorfismo BoolDep T F True = T?

Você não pode fazer isso usando a codificação tradicional da Igreja para Bool:

#Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

... porque você não pode escrever uma função (útil) do tipo:

#Bool → *

A razão pela qual, como você observou, é que você não pode passar *como o primeiro argumento para #Bool, o que, por sua vez, significa que os argumentos Truee Falsepodem não ser tipos.

Há pelo menos três maneiras de resolver isso:

1. Use o cálculo de construções indutivas. Em seguida, você pode generalizar o tipo de #Boolpara:

   #Bool = ∀(n : Nat) → ∀(Bool : *ₙ) → ∀(True : Bool) → ∀(False : Bool) → Bool
   

   ... e então você instanciar na 1, o que significa que você pode passar *₀como o segundo argumento, que tipo de verificação, porque:

   *₀ : *₁
   

   ... então você pode usar #Boolpara selecionar entre dois tipos.

2. Adicione mais uma classificação:

   * : □ : △
   

   Então você definiria um #Bool₂tipo separado como este:

   #Bool₂ = ∀(Bool : □) → ∀(True : Bool) → ∀(False : Bool) → Bool
   

   Este é essencialmente um caso especial das construções de Cálculo de Indutivo, mas produz um código menos reutilizável, pois agora devemos manter duas definições separadas de #Bool, uma para cada tipo que desejamos apoiar.

3. Codifique #Bool₂diretamente no Cálculo de construções como:

   #Bool₂ = ∀(True : *) → ∀(False : *) → *
   

Se o objetivo é usar isso diretamente dentro de não modificado morte, apenas a abordagem nº 3 funcionará.