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

11

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?

ZeitRaffer
fuente
Muy buena pregunta. Tengo sólo un pequeño problema que tengo problemas para entender por qué debe ser igual a . Expandir las definiciones debería ser mientras que debería ser igual a , entonces, ¿por qué estos dos tipos deberían ser iguales? ¿O he cometido algunos errores en mis cálculos? Bool T Bool T ( ( t : ) ( t t t ) ) T Producto T T ( t : ) ( ( T T t ) t )Product T TBoolTBoolT((t:)(ttt))TProductTT(t:)((TTt)t)
Giorgio Mossa
@Giorgio Mossa, consulte cstheory.stackexchange.com/questions/30923/… - si tiene parametricidad (no en todos los modelos sino en el inicial (sintáctico)), entonces tiene el isomorfismo.
ZeitRaffer

Respuestas:

9

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.

Gabriel Gonzalez
fuente
Como puedo ver, no podemos convertir # Bool₁ -> # Bool₂, ¿no?
ZeitRaffer
@ZeitRaffer Eso es correcto. No se puede convertir de #Bool₁a#Bool₂
Gabriel Gonzalez
1
Hmm ... IIUC lo llamas "Cálculo de construcciones inductivas" un cálculo con una jerarquía infinita de tipos, pero AFAIK el CIC original no tenía tal cosa (solo agregaba tipos inductivos al CoC). ¿Puede estar pensando en el ECC (cálculo extendido de construcciones) de Luo?
Stefan