Tipo-suma

Type-sum ( eng.  sum type ; también Σ -type , labelted union ) es una construcción en lenguajes de programación y teoría de tipos intuicionista , tipo de datos , construida como una unión disyuntiva de los tipos originales.

Junto con el tipo de producto, es una de las formas más importantes del tipo de datos algebraicos y una de las formas de construir tipos en la teoría intuicionista de tipos y sus variantes. Un tipo enumerado puede verse como una forma degenerada de un tipo de suma, una unión discriminada de tipos de unidades . 

Desde el punto de vista del isomorfismo de Curry-Howard , comparando tipos de datos y pruebas matemáticas constructivas , type-sum corresponde a una disyunción lógica .

Juegan un papel importante en los lenguajes de la familia ML como Standard ML , OCaml [1] , Haskell [2] y otros.

Notas

1. ↑ 6.2 Tipos de suma - CAPÍTULO 6. TIPOS DEFINIDOS POR EL USUARIO Archivado el 4 de marzo de 2016 en Wayback Machine / Programación funcional usando Caml Light   : "Un tipo de suma es la unión disjunta etiquetada finita de varios tipos. Una definición de tipo de suma define un tipo como siendo la unión de algunos otros tipos.”
2. ↑ Gabriel Gonzalez, Sum Types Archivado el 12 de agosto de 2015 en Wayback Machine / School of Haskell. Al infinito y más allá. Selección de la semana