Una categoría cerrada bicartesiana de órdenes parciales completas estrictas (Hask)

Parece ser bien sabido que los lenguajes de programación no pueden tener sumas, productos y falta de determinación juntos.

Q1 . ¿Es esto cierto? A continuación (o en el enlace anterior que di) hay un argumento parcial.

Sin embargo, la programación genérica de Hinze con adjunciones ignora el problema, incluso después de discutir con cierta precisión cuál es la categoría involucrada. En particular, habla (aparentemente sin reservas) acerca de que Haskell está modelado por la categoría de órdenes parciales continuas estrictas y que tiene sumas y productos. Pero sabemos que Haskell no tiene sumas (¿verdad?). (Parte del documento usa lugar, pero eso no permite la no terminación).S e $\mathbf{SCpo}$$\mathbf{Set}$

Q2 Entonces, ¿qué me estoy perdiendo? Veo cuatro opciones:

• La gente a menudo ignora la no terminación a propósito cuando habla de Haskell. Quizás este documento también lo haga. Pero entonces, ¿por qué uno mencionaría los CPO?
• La barrera que discuto se puede evitar de manera inteligente. En particular, el papel modela funciones no estrictas de Haskell mediante funciones estrictas , por otras razones.f : A ⊥ → $f : A \to B$$f : A_{\bot} \to B$
• El documento menciona la limitación y me perdí eso. He dedicado algo de esfuerzo a buscar esta mención y no he podido encontrar ninguna.
• Este es un error real, y como todos reclaman, Haskell carece de sumas categóricas (como lo acuerdan otras personas), a pesar de que las afirmaciones en papel Eitherson tales. En cambio, todo funciona bien en idiomas totales con tipos inductivos y coinductores.

Antecedentes

Es bien sabido que, en una categoría cerrada bicartesiana (BCCC), si el objeto inicial y el final coinciden (es decir, si la categoría tiene un objeto cero), la categoría colapsa (con todos los tipos isomorfos) por para todos .$A \cong A \times 1 \cong A \times 0 \cong 0$$A$

Esto significa, por ejemplo, que la categoría de conjuntos puntiagudos , con su objeto cero, no puede ser bicartesiana cerrada.

$\bot$$\omega$$\bot$$\mathbf{CPO}_{\bot}$$\mathbf{CPO}$

$\bot$

Sí, es imposible tener un CCC no degenerado con recursividad general y coproductos categóricos. La referencia estándar para esto es:

H. Huwig y A. Poigne. Una nota sobre inconsistencias causadas por puntos de fijación en una categoría cerrada cartesiana. Informática teórica, 73: 101-112, 1990.

Sin embargo, yo y (la mayoría de las otras personas que he conocido) lo aprendimos del capítulo de la teoría del dominio de Achim Jung y Samson Abramsky , que amablemente pusieron a disposición de forma gratuita.

La mayoría de las categorías de dominios con los que las personas trabajan son subcategorías de DCPO, la categoría de predominios y funciones continuas en ellas. Como los predominios no tienen necesariamente un punto fijo mínimo, esta categoría es un bi-CCC, pero los puntos fijos solo existen para funciones en dominios.

En la página 46 de estas notas, hay una gran tabla que le dice en qué subcategoría de DCPO existen diferentes construcciones.