¿Cuáles son los problemas prácticos con los tipos de intersección y unión?

Estoy diseñando un lenguaje de programación funcional simple mecanografiado como una experiencia de aprendizaje.

Parece que el sistema de tipos que he implementado hasta ahora podría (con un poco de trabajo extra) incorporar tipos de intersección y unión, por ejemplo, podría tener:

• <Union String Integer>
• <Union Integer Foo>
• La intersección de los dos tipos anteriores sería simple Integer
• La unión de los dos tipos sería <Union String Integer Foo>

El hecho de que esto sea posible, por supuesto, no necesariamente significa que sea una buena idea de diseño. En particular, estoy algo preocupado por las dificultades de implementación de mantener los tipos disjuntos y / o el manejo de superposiciones.

¿Cuáles son las ventajas y desventajas de incorporar tales características en el sistema de tipos?

Aquí hay algunas cosas a tener en cuenta:

• Aunque por lo general pensamos que sabemos lo que queremos decir por la intersección y la unión de teoría de conjuntos, se han producido varias tomas distintas sobre qué es exactamente intersección y unión tipos son . Por lo tanto, vale la pena precisar esto antes de embarcarse en una implementación.
• Un elemento que creo que es muy importante para comprender las intersecciones y las uniones es el concepto de refinamiento de tipos , esencialmente la idea de que un programa tiene un cierto "arquetipo" intrínseco (por ejemplo, " foo es una función de enteros a enteros"), que puede luego se refinará para expresar propiedades más precisas (por ejemplo, " foo toma enteros pares a enteros pares y enteros impares a enteros impares"). Con el concepto de refinamiento en la mano, la propiedad clave que distingue las intersecciones y uniones de productos y sumas es que la intersección / unión de dos tipos solo se puede formar si refinan el mismo arquetipo. En otras palabras, las reglas de formación de tipos para intersecciones y uniones pueden expresarse así (lea "S A S ⊏ $S \sqsubset A$$S$ refina ") mientras que las reglas de formación para productos y sumas ordinarios son $A$ S⊏ $$\frac{S\sqsubset A \quad T \sqsubset A}{S\cap T\sqsubset A}\qquad \frac{S\sqsubset A \quad T \sqsubset A}{S\cup T\sqsubset A}$$ $$\frac{S\sqsubset A \quad T \sqsubset B}{S* T\sqsubset A*B}\qquad \frac{S\sqsubset A \quad T \sqsubset B}{S+T\sqsubset A+B}$$
• Dado que las intersecciones y las uniones pueden usarse para hacer afirmaciones más precisas sobre el comportamiento en tiempo de ejecución de un programa, es natural que la tipificación se vuelva sensible al orden de evaluación. Por ejemplo, los documentos (2) y (4) a continuación explicaron por qué las reglas de tipeo y subtipo "obvias" (y bastante estándar) para intersecciones y uniones en realidad no son adecuadas para lenguajes similares a ML (debido a la presencia de efectos secundarios y no terminación). ¡Usted ha sido advertido!
• Por razones similares, la inferencia de tipo global generalmente se vuelve poco práctica o indecidible. De hecho, todo el concepto de "tipo principal" es posiblemente una pista falsa, ya que una función puede satisfacer muchas propiedades diferentes que son irrelevantes para su uso previsto (por ejemplo, " foo lleva enteros primos a enteros mayores que 7"). En cambio, los enfoques prácticos de intersecciones y uniones (ver (3) , (4) ) generalmente se basan en una combinación de inferencia y verificación.

Supongo que algunos de los puntos anteriores pueden parecer negativos, aunque no los llamaría "contras" sino meramente "realidades" de los tipos de intersección y unión. Por otro lado, desde la perspectiva del diseño del lenguaje, una razón para hacer el esfuerzo de apoyar intersecciones y uniones (¡y para hacerlo bien!) Es que permiten que las propiedades más precisas de los programas se expresen de una manera bastante incremental, lo que requiere un transformación mucho menos drástica que, por ejemplo, la teoría del tipo dependiente.

Una breve lista de lectura:

1. Diseño del lenguaje de programación Forsythe por John C. Reynolds
2. Tipos de intersección y efectos computacionales por Rowan Davies y Frank Pfenning
3. Comprobación práctica del tipo de refinamiento por Rowan Davies (disertación)
4. Comprobación de tipos tridireccionales por Joshua Dunfield y Frank Pfenning