Tipos dependientes sobre el tipo codificado por Church en PTS / CoC

Estoy experimentando con sistemas de tipo puro en el cubo lambda de Barendregt, específicamente con el más poderoso, el cálculo de construcciones. Este sistema tiene géneros *y BOX. Solo para el registro, a continuación estoy usando la sintaxis concreta de la Morteherramienta https://github.com/Gabriel439/Haskell-Morte-Library que está cerca del cálculo lambda clásico.

Veo que podemos emular tipos inductivos mediante algún tipo de codificación similar a la Iglesia (también conocido como isomorfismo Boehm-Berarducci para tipos de datos algebraicos). Para un ejemplo simple, uso type Bool = ∀(t : *) -> t -> t -> tcon los constructores True = λ(t : *) -> λ(x : t) -> λ(y : t) -> xy False = λ(t : *) -> λ(x : t) -> λ(y : t) -> y.

Veo que el tipo de funciones de nivel de término Bool -> Tes isomorfo a pares de tipos Product T Tcon Product = λ(A : *) -> λ(B : *) -> ∀(t : *) -> (A -> B -> t) -> tparamétrica de módulo clásico por medio de una función if : Bool -> λ(t : *) -> t -> t -> tque en realidad es identidad.

Todas las preguntas a continuación serán sobre representaciones de tipos dependientes Bool -> *.

1. Me puedo dividir D : Bool -> *en par de D Truey D False. ¿Existe la forma canónica de crear de Dnuevo? Quiero reproducir el isomosfismo Bool -> T = Product T Tmediante un análogo de función ifa nivel de tipo, pero no puedo escribir esta función tan simple como original ifporque no podemos pasar tipos en argumentos como tipos.

2. Utilizo una especie de tipo inductivo con dos constructores para resolver la pregunta (1). La descripción de alto nivel (estilo Agda) es el siguiente tipo (se utiliza en lugar del nivel de tipo if)

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

   con la siguiente codificación en PTS / CoC:

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

   ¿Mi codificación anterior es correcta?

3. Puedo escribir los constructores de BoolDepeste 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
   

pero no puedo escribir la función inversa (o cualquier función en la dirección inversa). ¿Es posible? ¿O debería usar otra representación para BoolDepproducir un isomorfismo BoolDep T F True = T?

No puede hacer esto usando la codificación tradicional de la Iglesia para Bool:

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

... porque no puedes escribir una función (útil) de tipo:

#Bool → *

La razón por la cual, como notó, es que no puede pasar *como primer argumento #Bool, lo que a su vez significa que los argumentos Truey Falsepueden no ser tipos.

Hay al menos tres formas de resolver esto:

1. Usa el cálculo de construcciones inductivas. Entonces podría generalizar el tipo de #Boola:

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

   ... y entonces sería una instancia na 1, que significa que podría pasar *₀como segundo argumento, lo que escriba-cheque porque:

   *₀ : *₁
   

   ... entonces podría usar #Boolpara seleccionar entre dos tipos.

2. Agregue un tipo más:

   * : □ : △
   

   Entonces definirías un #Bool₂tipo separado como este:

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

   Este es esencialmente un caso especial del cálculo de las construcciones inductivas, pero produce un código menos reutilizable ya que ahora debemos mantener dos definiciones separadas #Bool, una para cada tipo que deseamos admitir.

3. Codificar #Bool₂directamente dentro del cálculo de construcciones como:

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

Si el objetivo es usar esto directamente sin modificar morte, solo funcionará el enfoque n. ° 3.