haskell - ¿Qué significa confiar en la consistencia de un lenguaje de coerción?

functional-programming coercion

Question

De https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell ,

a diferencia de Coq y Agda, Haskell se basa en la consistencia de un lenguaje de coerción, que no está amenazado por * :: *. Vea el documento para más detalles.

El "artículo" citado es un enlace roto , pero al buscarlo en Google y leerlo, me di cuenta de que describe cómo agregar igualdad explícita y amable al sistema FC, pero no aborda directamente la pregunta implícita: qué significa depender de la consistencia de ¿Un lenguaje de coerción ?

Answer 1

Coq y Agda son lenguajes totales tipificados de forma dependiente. Se inspiran en sus fundamentos teóricos de tipo relativo, que involucran un cálculo lambda (tipificado) que se está (fuertemente) normalizando. Esto significa que la reducción de cualquier término lambda finalmente tiene que detenerse.

Esta propiedad hace posible el uso de Coq y Agda como sistemas de prueba: se pueden probar hechos matemáticos al usarlos. De hecho, por la correspondencia Curry-Howard, si

someExpression :: someType

entonces someType corresponde a una tautología lógica (intuicionista).

En Haskell, este no es el caso, ya que cualquier tipo puede ser "probado" por

undefined :: someType

Es decir, podemos hacer trampa utilizando un valor "inferior". Esto hace que Haskell, como lógica, sea inconsistente. Podemos probar undefined :: Data.Void.Void , que corresponde a la proposición lógica "falsa", por ejemplo. Esto es malo, pero es el precio necesario para pagar por tener recursión ilimitada, lo que permite programas que no terminan.

En comparación, Coq y Agda solo tienen recursión primitiva (que nunca puede repetirse para siempre).

Ahora, al punto. Es bien sabido que agregar el axioma * :: * a Coq / Agda hace que la lógica ya no sea consistente. Podemos obtener una prueba de "falso" usando la paradoja de Girard. Eso sería muy malo, ya que podemos incluso probar cosas como lemma :: Int :~: String , y derivar una función de coerción coerce :: Int -> String .

lemma :: Int :~: String
lemma = -- exploit Girard''s paradox here

-- using Haskell syntax:
coerce :: Int -> String
coerce x = case lemma of Refl -> x

Si implementamos eso de forma ingenua, la coerce simplemente realizaría un lanzamiento inseguro, reinterpretando los bits subyacentes; después de todo, eso está justificado por el lemma , ¡declarando que estos tipos son exactamente iguales! De esa manera, incluso perderíamos la seguridad del tipo de tiempo de ejecución. La fatalidad espera.

En Haskell, incluso si no agregamos * :: * somos inconsistentes de todos modos, así que simplemente podemos tener

lemma = undefined

y derivar la coerce todos modos! Por lo tanto, agregar * :: * realmente no aumenta la cantidad de problemas. Es solo otra fuente de inconsistencia.

Uno podría entonces preguntarse por qué en Haskell la coerce es segura, entonces. Bueno, en el case lemma of Refl ->... Haskell case lemma of Refl ->... obliga a evaluar el lemma . Esto solo puede desencadenar una excepción o no terminar, por lo que nunca se llega a la parte ... Haskell no puede optimizar la coerce como un reparto inseguro, a diferencia de Agda / Coq.

Hay otro aspecto de Haskell que menciona el párrafo citado: el lenguaje de coerción. Internamente, cuando escribimos.

case lemma1 of
  Refl -> case lemma2 of
    Refl -> ...
      ...
        Refl -> expression

introducimos muchas ecualidades de tipo que deben ser explotadas para probar que la expression tiene el tipo requerido. En Coq, el programador debe utilizar una forma sofisticada de comparación (coincidencia dependiente) para justificar dónde y cómo explotar las igualdades de tipo. En Haskell, el compilador escribe esta prueba para nosotros (en Coq, el sistema de tipos es más rico, y eso implicaría una unificación de orden superior, lo cual es indecidible). ¡Esta prueba NO está escrita en Haskell! De hecho, Haskell es inconsistente, así que no podemos confiar en eso. En cambio, Haskell usa otro lenguaje de coerción personalizado para eso, que se garantiza que sea consistente. Solo tenemos que confiar en eso.

Podemos ver algunos vislumbres de ese lenguaje de coerción interna si volcamos Core. Por ejemplo, compilando una prueba de transitividad.

trans :: a :~: b -> b :~: c -> a :~: c
trans Refl Refl = Refl

obtenemos

GADTtransitivity.trans
  :: forall a_au9 b_aua c_aub.
     a_au9 :~: b_aua -> b_aua :~: c_aub -> a_au9 :~: c_aub
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
GADTtransitivity.trans =
  / (@ a_auB)
    (@ b_auC)
    (@ c_auD)
    (ds_dLB :: a_auB :~: b_auC)
    (ds1_dLC :: b_auC :~: c_auD) ->
    case ds_dLB of _ [Occ=Dead] { Refl cobox0_auF ->
    case ds1_dLC of _ [Occ=Dead] { Refl cobox1_auG ->
    (Data.Type.Equality.$WRefl @ * @ a_auB)
    `cast` ((<a_auB>_N :~: (Sym cobox0_auF ; Sym cobox1_auG))_R
            :: ((a_auB :~: a_auB) :: *) ~R# ((a_auB :~: c_auD) :: *))
    }
    }

Observe el cast al final, que explota la prueba en el lenguaje de coerción

(<a_auB>_N :~: (Sym cobox0_auF ; Sym cobox1_auG))_R

En esta prueba, podemos ver Sym cobox0_auF ; Sym cobox1_auG Sym cobox0_auF ; Sym cobox1_auG que supongo que usa simetría Sym y transitivity ; para alcanzar el objetivo deseado: la prueba de que Refl :: a_auB :~: a_auB puede convertir de forma segura en el deseado a_auB :~: c_auD .

Finalmente, tenga en cuenta que estoy bastante seguro de que dichas pruebas se descartan durante la compilación por parte de GHC, y que el cast última instancia se reduce a un lanzamiento inseguro en tiempo de ejecución (el case aún evalúa las dos pruebas de entrada, para preservar la seguridad del tipo). Sin embargo, tener una prueba intermedia asegura fuertemente que el compilador está haciendo lo correcto.