¿Cómo puedo mostrar que un tipo Haskell está habitado por una y solo una función?

category-theory type-theory

Question

En esta respuesta , Gabriel González muestra cómo mostrar que la id es el único habitante de forall a. a -> a forall a. a -> a . Para hacerlo (en la iteración más formal de la prueba), muestra que el tipo es isomorfo para () usando el lema de Yoneda , y como () tiene solo un valor, también debe ser el tipo de id . Resumido, su prueba es así:

Yoneda dice:

Functor f => (forall b . (a -> b) -> f b) ~ f a

Si a = () y f = Identity , esto se convierte en:

(forall b. (() -> b) -> b) ~ ()

Y como trivialmente () -> b ~ b , el LHS es básicamente el tipo de id .

Esto se siente como un "truco de magia" que funciona bien para la id . Intento hacer lo mismo para un tipo de función más complejo:

(b -> a) -> (a -> b -> c) -> b -> c

Pero no tengo idea de por dónde empezar. Sé que está habitado por /fgx = g (fx) x , y si ignoras las cosas feas un / undefined , estoy bastante seguro de que no hay otras funciones de este tipo.

No creo que el truco de Gabriel se aplique de inmediato aquí de la manera que elija los tipos. ¿Hay otros enfoques (que son igualmente formales) con los que puedo mostrar el isomorfismo entre este tipo y () ?

Answer 1

Puedes aplicar el cálculo secuencial .

Ejemplo corto, con el tipo a -> a , podríamos construir un término como: /x -> (/y -> y) x , pero eso todavía se normaliza a /x -> x que es id . En el cálculo secuencial, el sistema prohíbe construir pruebas "reducibles".

Su tipo es (b -> a) -> (a -> b -> c) -> b -> c , informalmente:

f: b -> a
g: a -> b -> c
x: b
--------------
Goal: c

Y no hay muchas maneras de proceder:

apply g
f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0: a
Subgoal1: b
apply f
f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0'': b
Subgoal1: b
-- For both
apply x

Entonces, al final, parece que g (fx) x es el único habitante de ese tipo.

Enfoque de Yoneda lemma, hay que tener cuidado de tener realmente todo para forall x !

 (b -> a) -> (a -> b -> c) -> b -> c
forall b a. (b -> a) -> b -> forall c. (a -> b -> c) -> c

Vamos a concentrarnos en el final:

 (a -> b -> c) -> c ~ ((a,b) -> c) -> c

Eso es isomorfo a (a, b) , por lo que todo tipo se reduce a

(b -> a) -> b -> (a, b)

Toma f = Compose (Reader b) (,b)

(b -> a) -> f a ~ f b ~ b -> (b,b)

Y eso es único tomando HP a = (a,a) functor:

b -> (b,b) ~ (() -> b) -> HP b ~ HP () ~ ()

EDITAR el primer enfoque se siente un poco más ondulado a mano, pero de alguna manera es más directo: dado el conjunto restringido de reglas, ¿cómo se puede construir la prueba, cuántas pruebas podemos construir?