haskell - sonido - ¿Hask o Agda tienen ecualizadores?

ecualizadores de sonido

Question

Estaba algo indeciso acerca de si se trataba de una pregunta de matemáticas o de AS, pero sospecho que es poco probable que los matemáticos en general conozcan o se preocupen mucho por esta categoría en particular, mientras que los programadores de Haskell podrían hacerlo.

Entonces, sabemos que Hask tiene productos, más o menos (estoy trabajando con Hask idealizado, aquí, por supuesto). Me interesa saber si tiene o no ecualizadores (en cuyo caso tendría todos los límites finitos).

Intuitivamente no parece, ya que no se puede hacer la separación como se puede en los conjuntos, por lo que los subobjetos parecen difíciles de construir en general. Pero para cualquier caso específico que le gustaría idear, parece que sería capaz de hackearlo resolviendo el ecualizador en Establecer y contando (ya que, después de todo, cada tipo de Haskell es contable y cada conjunto contable es isomorfo ya sea a un tipo finito o a los naturales, que Haskell tiene). Entonces no puedo ver cómo encontrar un contraejemplo.

Ahora, Agda parece un poco más prometedor: allí es relativamente fácil formar subobjetos. ¿Es el tipo sigma obvio Σ A (λ x → fx == gx) un ecualizador? Si los detalles no funcionan, ¿es moralmente un ecualizador?

Answer 1

Hask

Hask no tiene ecualizadores. Una cosa importante para recordar es que pensar en un tipo (o los objetos en cualquier categoría) y sus clases de isomorfismo realmente requiere pensar en las flechas. Lo que dices acerca de los conjuntos subyacentes es cierto, pero los tipos con conjuntos subyacentes isomorfos ciertamente no son necesariamente isomorfos. Una diferencia entre Hask y Set, ya que las flechas de Hask deben ser computables, y de hecho para Hask idealizado, deben ser totales.

Pasé un tiempo tratando de llegar a un contraejemplo defendible real, y encontré algunas referencias que sugieren que no se puede hacer, pero sin pruebas. Sin embargo, sí tengo algunos contraejemplos "morales"; No puedo probar que no exista ecualizador en Haskell, pero ciertamente parece imposible.

Ejemplo 1

f, g: ([Int], Int) -> Int

f (p,v) = treat p as a polynomial with given coefficients, and evaluate p(v).
g _ = 0

El ecualizador "debería" ser el tipo de todos los pares (p, n) donde p (n) = 0, junto con una función que inyecta estos pares en ([Int], Int). Según el décimo problema de Hilbert, este conjunto es indecidible. Me parece que esto debería excluir la posibilidad de que sea un tipo Haskell, pero no puedo probarlo (¿es posible que haya alguna forma extraña de construir este tipo que nadie haya descubierto?). Tal vez no he conectado un punto o dos, ¿tal vez demostrar que esto es imposible no es difícil?

Ejemplo 2

Digamos que tienes un lenguaje de programación. Usted tiene un compilador que toma el código fuente y una entrada y produce una función, para la cual el punto fijo de la función es la salida. (Si bien no tenemos compiladores como este, especificar una semántica como esta no es desconocida). Así que tienes

compiler : String -> Int -> (Int -> Int)

(Un) curry eso en una función

compiler'' : (String, Int, Int) -> Int

y agrega una función

id'' : (String, Int, Int) -> Int
id'' (_,_,x) = x

Entonces, el ecualizador del compilador '', id'' sería la colección de trillizos del programa fuente, entrada, salida, y esto no es discutible porque el lenguaje de programación es completamente general.

Más ejemplos

Elija su problema indecidible favorito: generalmente implica decidir si un objeto es miembro de algún conjunto. A menudo tiene una función total que puede usarse para verificar esta propiedad para un objeto en particular. Puede usar esta función para crear un ecualizador donde el tipo debe ser todos los elementos en su conjunto indecidible. De ahí provienen los dos primeros ejemplos, y hay muchísimos más.

Agda

No estoy tan familiarizado con Agda. Mi intuición es que su tipo sigma debería ser un ecualizador: puede escribir el tipo hacia abajo, junto con la función de inyección necesaria, y parece que satisface por completo la definición. Sin embargo, como alguien que no usa Agda, no creo que esté realmente calificado para verificar los detalles.

Sin embargo, el verdadero problema práctico es que la verificación de tipografía sigma no siempre será computable, por lo que no siempre es útil hacerlo. En todos los ejemplos anteriores, puede anotar el tipo de Sigma que proporcionó, pero no podrá verificar fácilmente si algo es miembro de ese tipo sin una prueba.

Por cierto, esta es la razón por la que Haskell no debería tener ecualizadores: ¡si lo hiciera, la verificación de tipo sería indecidible! Los tipos dependientes es lo que hace que todo funcione. Deberían poder expresar estructuras matemáticas interesantes en sus tipos, mientras que Haskell no puede hacerlo ya que su sistema de tipos es decidible. Por lo tanto, naturalmente esperaría que Agda idealizada tenga todos los límites finitos (de lo contrario, me decepcionaría). Lo mismo ocurre con otros idiomas con subtítulos dependientes; Coq, por ejemplo, definitivamente debería tener todos los límites.

Answer 2

tl; dr el candidato propuesto no es un ecualizador, pero su contraparte irrelevante es

El candidato para un ecualizador en Agda se ve bien. Así que intentémoslo. Necesitaremos un kit básico. Aquí están mi tipo de par dependiente ASUS de refusenik y la igualdad intensional homogénea.

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg

data _==_ {X : Set}(x : X) : X -> Set where
  refl : x == x

Aquí está su candidato para un ecualizador para dos funciones

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Sg S / s -> f s == g s

con la primera proyección enviando Q fg a S

Lo que dice: un elemento de Q fg es un elemento s del tipo fuente, junto con una prueba de que fs == gs . Pero, ¿esto es un ecualizador? Tratemos de que sea así.

Para decir lo que es un ecualizador, debo definir la composición de la función.

_o_ : {R S T : Set} -> (S -> T) -> (R -> S) -> R -> T
(f o g) x = f (g x)

Entonces ahora necesito mostrar que cualquier h : R -> S que identifique foh y goh debe factorizar a través del candidato fst : Q fg -> S Necesito entregar tanto el otro componente, u : R -> Q fg y la prueba que de hecho h factores como fst ou . Aquí está la imagen: (Q fg , fst) es un ecualizador si cada vez que el diagrama se desplaza sin u , hay una manera única de u con el diagrama que todavía se desplaza.

Aquí va la existencia de la mediación.

mediator : {R S T : Set}(f g : S -> T)(h : R -> S) ->
           (q : (f o h) == (g o h)) ->
           Sg (R -> Q f g) / u -> h == (fst o u)

Claramente, debería elegir el mismo elemento de S que h .

mediator f g h q = (/ r -> (h r , ?0)) , ?1

dejándome con dos obligaciones de prueba

?0 : f (h r) == g (h r)
?1 : h == (/ r -> h r)

Ahora ?1 puede ser refl como la igualdad de definición de Agda tiene la ley eta para las funciones. Para ?0 , somos bendecidos por q . Funciones iguales respecto a la aplicación

funq : {S T : Set}{f g : S -> T} -> f == g -> (s : S) -> f s == g s
funq refl s = refl

entonces podemos tomar ?0 = funq qr .

Pero no celebremos prematuramente, porque la existencia de un morfismo mediador no es suficiente. Requerimos también su singularidad. Y aquí es probable que la rueda se vuelva inestable, porque == es intensional , por lo que la singularidad significa que solo hay una sola forma de implementar el mapa de mediación. Pero entonces, nuestras suposiciones también son intensionales ...

Aquí está nuestra obligación de prueba. Debemos demostrar que cualquier otro morfismo mediador es igual al elegido por el mediator .

mediatorUnique :
  {R S T : Set}(f g : S -> T)(h : R -> S) ->
  (qh : (f o h) == (g o h)) ->
  (m : R -> Q f g) ->
  (qm : h == (fst o m)) ->
  m == fst (mediator f g h qh)

Podemos sustituir inmediatamente a través de qm y obtener

mediatorUnique f g .(fst o m) qh m refl = ?

? :  m == (/ r -> (fst (m r) , funq qh r))

que se ve bien, porque Agda tiene leyes eta para los registros, por lo que sabemos que

m == (/ r -> (fst (m r) , snd (m r)))

pero cuando tratamos de hacer ? = refl ? = refl , obtenemos la queja

snd (m _) != funq qh _ of type f (fst (m _)) == g (fst (m _))

que es molesto, porque las pruebas de identidad son únicas (en la configuración estándar). Ahora, puedes salir de esto postulando la extensionalidad y usando algunos otros hechos sobre la igualdad

postulate ext : {S T : Set}{f g : S -> T} -> ((s : S) -> f s == g s) -> f == g

sndq : {S : Set}{T : S -> Set}{s : S}{t t'' : T s} ->
       t == t'' -> _==_ {Sg S T} (s , t) (s , t'')
sndq refl = refl

uip : {X : Set}{x y : X}{q q'' : x == y} -> q == q''
uip {q = refl}{q'' = refl} = refl

? = ext (/ s -> sndq uip)

pero eso es exagerado, porque el único problema es la desagradable incompatibilidad de prueba de igualdad: las partes computables de las implementaciones coinciden en la nariz. Entonces la solución es trabajar con irrelevancia . Sustituyo Sg por el cuantificador Ex istential, cuyo segundo componente está marcado como irrelevante con un punto. Ahora no importa qué prueba usamos para que el testigo sea bueno.

record Ex (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    .snd : T fst
open Ex

y el nuevo ecualizador candidato es

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Ex S / s -> f s == g s

Toda la construcción se realiza como antes, excepto que en la última obligación

? = refl

¡es aceptado!

Entonces, sí, incluso en el entorno intensional, las leyes eta y la capacidad de marcar los campos como irrelevantes nos dan ecualizadores.

No se incluyó una verificación de tipo indecidible en esta construcción.