Programación genérica

La especificación de un paquete genérico:

generic Max_Size : Natural ; -- un tipo de valor formal genérico Element_Type es privado ; -- un tipo formal genérico; acepta cualquier paquete de tipo no limitado Stacks es tipo Size_Type es rango 0 .. Max_Size ; tipo Stack es limitado privado ; procedimiento Create ( S : out Stack ; Initial_Size : in Size_Type := Max_Size ); procedimiento Push ( Into : in out Stack ; Element : in Element_Type ); procedimiento Pop ( From : in out Stack ; Element : out Element_Type ); Overflow : exception ; Underflow : exception ; subtipo privado Index_Type es Size_Type rango 1 .. Max_Size ; tipo Vector es array ( Index_Type rango <>) de Element_Type ; tipo Stack ( Allocated_Size : Size_Type := 0 ) es registro Top : Index_Type ; Almacenamiento : Vector ( 1 .. Allocated_Size ); fin registro ; fin Stacks ;

Instanciando el paquete genérico:

type Bookmark_Type is new Natural ; -- registra una ubicación en el documento de texto que estamos editandopackage Bookmark_Stacks is new Stacks ( Max_Size => 20 , Element_Type => Bookmark_Type ); -- Permite al usuario saltar entre ubicaciones registradas en un documento

Utilizando una instancia de un paquete genérico:

tipo Document_Type es registro Contenido : Ada.Strings.Unbounded.Unbounded_String ; Marcadores : Bookmark_Stacks.Stack ; fin del registro ;​​​​​​procedure Edit ( Document_Name : in String ) is Document : Document_Type ; begin -- Inicializar la pila de marcadores: Bookmark_Stacks . Create ( S => Document . Bookmarks , Initial_Size => 10 ); -- Ahora, abrir el archivo Document_Name y leerlo... end Edit ;

La sintaxis del lenguaje permite especificar con precisión las restricciones sobre los parámetros formales genéricos. Por ejemplo, es posible especificar que un tipo formal genérico solo acepte un tipo modular como el tipo real. También es posible expresar restricciones entre parámetros formales genéricos; por ejemplo:

generic type Index_Type is (<>); -- debe ser un tipo discreto type Element_Type is private ; -- puede ser cualquier tipo no limitado type Array_Type is array ( Index_Type range <>) of Element_Type ;

En este ejemplo, Array_Typeestá restringido por Index_Typey Element_Type. Al instanciar la unidad, el programador debe pasar un tipo de matriz real que satisfaga estas restricciones.

La desventaja de este control detallado es una sintaxis complicada, pero, dado que todos los parámetros formales genéricos están completamente definidos en la especificación, el compilador puede instanciar genéricos sin examinar el cuerpo del genérico.

A diferencia de C++, Ada no permite instancias genéricas especializadas y requiere que todos los genéricos se instancien explícitamente. Estas reglas tienen varias consecuencias:

• El compilador puede implementar genéricos compartidos : el código objeto de una unidad genérica puede compartirse entre todas las instancias (a menos que el programador solicite la inserción en línea de subprogramas, por supuesto). Como consecuencias adicionales:
  • No existe posibilidad de que el código se vuelva demasiado extenso (el exceso de código es común en C++ y requiere especial atención, como se explica a continuación).
  • Es posible instanciar objetos genéricos tanto en tiempo de ejecución como en tiempo de compilación, ya que no se requiere nuevo código objeto para una nueva instancia.
  • Los objetos reales que corresponden a un objeto formal genérico siempre se consideran no estáticos dentro del genérico; consulte Objetos formales genéricos en el Wikilibro para obtener más detalles y conocer las consecuencias.
• Al ser todas las instancias de un genérico exactamente iguales, es más fácil revisar y comprender los programas escritos por otros; no hay "casos especiales" que tener en cuenta.
• Al ser todas las instanciaciones explícitas, no existen instanciaciones ocultas que puedan dificultar la comprensión del programa.
• Ada no permite cálculos arbitrarios en tiempo de compilación, ya que las operaciones con argumentos genéricos se realizan en tiempo de ejecución.

Existen muchos tipos de plantillas, siendo las más comunes las plantillas de función y las plantillas de clase. Una plantilla de función es un patrón para crear funciones ordinarias basadas en los tipos de parámetros proporcionados al instanciarlas. Por ejemplo, la biblioteca de plantillas estándar de C++ contiene la plantilla de función std::max(x, y)que crea funciones que devuelven xo y, el que sea mayor. max()podría definirse de la siguiente manera:

plantilla < typename T > [[ nodiscard ]] constexpr T max ( T x , T y ) noexcept { return x < y ? y : x ; }

Las especializaciones de esta plantilla de función, instanciaciones con tipos específicos, se pueden llamar como una función ordinaria:

std :: println ( "{}" , max ( 3 , 7 )); // Imprime 7.

El compilador examina los argumentos utilizados para la llamada maxy determina que se trata de una llamada a max(int, int). A continuación, instancia una versión de la función donde la variable de tipoT es int, lo que hace que sea el equivalente de la siguiente función:

[[ nodiscard ]] constexpr int max ( int x , int y ) noexcept { return x < y ? y : x ; }

Esto funciona tanto si los argumentos xy yson enteros, cadenas o cualquier otro tipo para el que la expresión x < ytenga sentido, o más específicamente, para cualquier tipo para el que operator<esté definido. No se necesita herencia común para el conjunto de tipos que se pueden usar, por lo que es muy similar al tipado dinámico . Un programa que define un tipo de datos personalizado puede usar la sobrecarga de operadores para definir el significado de <para ese tipo, lo que permite su uso con la std::max()plantilla de función. Si bien esto puede parecer un beneficio menor en este ejemplo aislado, en el contexto de una biblioteca completa como la STL permite al programador obtener una funcionalidad extensa para un nuevo tipo de datos, simplemente definiendo algunos operadores para él. Simplemente definir <permite que un tipo se use con los algoritmos estándar std::sort(), std::stable_sort(), y std::binary_search()o se coloque dentro de estructuras de datos como std::set<T>s (equivalente a TreeSet<T>, montones y matrices asociativas .

Las plantillas de C++ son completamente seguras en cuanto a tipos en tiempo de compilación. Como demostración, el tipo estándar std::complex<T>no define el <operador, porque no hay un orden estricto en los números complejos . Por lo tanto, std::max(x, y)fallará con un error de compilación, si xy yson complexvalores. Del mismo modo, otras plantillas que dependen de <no se pueden aplicar a complexlos datos a menos que se proporcione una comparación (en forma de functor o función). Por ejemplo, std::complex<T>no se puede usar como clave para un std::map<K, V>(equivalente a TreeMap<K, V>) a menos que se proporcione una comparación. Desafortunadamente, los compiladores históricamente generan mensajes de error algo esotéricos, largos y poco útiles para este tipo de error. Asegurarse de que un objeto determinado se adhiera a un protocolo de método puede aliviar este problema. Los lenguajes que usan std::compareen lugar de <también pueden usar std::complex<T>valores como claves.

Otro tipo de plantilla, una plantilla de clase , extiende el mismo concepto a las clases. Una especialización de plantilla de clase es una clase. Las plantillas de clase se utilizan a menudo para crear contenedores genéricos. Por ejemplo, la STL tiene un contenedor de lista doblemente enlazadastd::list<T> (equivalente a LinkedList<T>). Para crear una lista enlazada de enteros, se escribe list<int>, mientras que una lista de cadenas se denota como list<string>. Una std::list<T>tiene un conjunto de funciones estándar asociadas que funcionan para cualquier tipo de parametrización compatible.

C++20 introduce la restricción de tipos de plantillas mediante conceptos . Restringir el tipo max()podría verse así:

importar std ;usando std :: totalmente_ordenado ;// en la declaración del nombre del tipo: plantilla < totally_ordered T > [[ nodiscard ]] constexpr T max ( T x , T y ) noexcept { return x < y ? y : x ; }// en la cláusula requires: template < typename T > requires totally_ordered < T > [[ nodiscard ]] constexpr T max ( T x , T y ) noexcept { return x < y ? y : x ; }

Una característica poderosa de las plantillas de C++ es la especialización de plantillas . Esto permite proporcionar implementaciones alternativas basadas en ciertas características del tipo parametrizado que se está instanciando. La especialización de plantillas tiene dos propósitos: permitir ciertas formas de optimización y reducir la complejidad del código.

Por ejemplo, consideremos una sort()función plantilla. Una de las actividades principales de dicha función es intercambiar los valores en dos posiciones del contenedor. Si los valores son grandes (en términos de la cantidad de bytes que ocupa cada uno), suele ser más rápido crear primero una lista separada de punteros a los objetos, ordenar esos punteros y luego construir la secuencia final ordenada. Sin embargo, si los valores son bastante pequeños, generalmente es más rápido simplemente intercambiar los valores directamente según sea necesario. Además, si el tipo parametrizado ya es de algún tipo de puntero, no es necesario crear una matriz de punteros separada. La especialización de plantillas permite al creador de la plantilla escribir diferentes implementaciones y especificar las características que deben tener los tipos parametrizados para que cada implementación se utilice.

A diferencia de las plantillas de funciones, las plantillas de clases pueden especializarse parcialmente . Esto significa que se puede proporcionar una versión alternativa del código de la plantilla de clase cuando se conocen algunos de sus parámetros, mientras que otros parámetros permanecen genéricos. Esto se puede usar, por ejemplo, para crear una implementación predeterminada (la especialización primaria ) que asume que copiar un tipo de parametrización es costoso y luego crear especializaciones parciales para los tipos que son económicos de copiar, aumentando así la eficiencia general. Los clientes de dicha plantilla de clase simplemente usan sus especializaciones sin necesidad de saber si el compilador usó la especialización primaria o alguna especialización parcial en cada caso. Las plantillas de clases también pueden especializarse completamente, lo que significa que se puede proporcionar una implementación alternativa cuando se conocen todos los tipos de parametrización.

Algunos usos de las plantillas, como la max()función, antes se realizaban mediante macros de preprocesador similares a funciones (un legado del lenguaje C ). Por ejemplo, aquí hay una posible implementación de dicha macro:

#define max(a,b) ((a) < (b) ? (b) : (a))

Las macros se expanden (copian y pegan) mediante el preprocesador antes de la compilación del programa; las plantillas son funciones reales. Las macros siempre se expanden en línea; las plantillas también pueden ser funciones en línea cuando el compilador lo considera apropiado.

Sin embargo, en general, las plantillas se consideran una mejora con respecto a las macros para estos fines. Las plantillas son seguras en cuanto a tipos. Evitan algunos de los errores comunes que se encuentran en el código que utiliza macros con funciones de forma intensiva, como la evaluación doble de parámetros con efectos secundarios. Y, quizás lo más importante, las plantillas se diseñaron para ser aplicables a problemas mucho más complejos que las macros.

Existen cuatro inconvenientes principales en el uso de plantillas: características compatibles, soporte del compilador, mensajes de error deficientes (generalmente con fallos de sustitución anteriores a C++20 no es un error ( SFINAE )) y código inflado :

1. Las plantillas en C++ carecen de muchas funcionalidades, lo que dificulta su implementación y uso directo. En consecuencia, los programadores deben recurrir a técnicas complejas, lo que resulta en código inflado, difícil de comprender y de mantener. Los avances actuales en los estándares de C++ agravan este problema al utilizar intensivamente estas técnicas e incorporar numerosas funcionalidades nuevas para las plantillas, ya sea basándolas en ellas o con la intención de desarrollarlas.
2. Históricamente, muchos compiladores ofrecían un soporte deficiente para las plantillas, por lo que su uso podía dificultar la portabilidad del código. El soporte también puede ser deficiente cuando se utiliza un compilador de C++ con un enlazador que no es compatible con C++, o al intentar usar plantillas entre bibliotecas compartidas .
3. Los compiladores pueden generar mensajes de error confusos, largos y, a veces, poco útiles cuando se detectan errores en el código que utiliza SFINAE. ^{[ 22 ]} Esto puede dificultar el desarrollo con plantillas.
4. Finalmente, el uso de plantillas requiere que el compilador genere una instancia separada de la clase o función plantilla para cada parámetro de tipo utilizado con ella. (Esto es necesario porque los tipos en C++ no tienen todos el mismo tamaño, y el tamaño de los campos de datos es importante para el funcionamiento de las clases). Por lo tanto, el uso indiscriminado de plantillas puede provocar un aumento excesivo del tamaño del código , lo que resulta en ejecutables excesivamente grandes. Sin embargo, el uso juicioso de la especialización y derivación de plantillas puede reducir drásticamente dicho aumento en algunos casos.

   Entonces, ¿se puede usar la derivación para reducir el problema del código duplicado debido al uso de plantillas? Esto implicaría derivar una plantilla de una clase ordinaria. Esta técnica ha demostrado ser eficaz para controlar el exceso de código en la práctica. Quienes no utilizan una técnica como esta han descubierto que el código duplicado puede ocupar megabytes de espacio de código incluso en programas de tamaño moderado.

   — Bjarne Stroustrup , El diseño y la evolución de C++, 1994 ^{[ 23 ]}

5. Las clases o funciones con plantillas pueden requerir una especialización explícita de la clase plantilla, lo que implicaría reescribir una clase completa para los parámetros de plantilla específicos que utiliza.

Las instanciaciones adicionales generadas por las plantillas también pueden causar que algunos depuradores tengan dificultades para trabajar correctamente con ellas. Por ejemplo, al establecer un punto de interrupción de depuración dentro de una plantilla desde un archivo fuente, es posible que no se establezca en la instancia deseada o que se establezca en todos los lugares donde se instancia la plantilla.

Además, el código fuente de implementación de la plantilla debe estar completamente disponible (por ejemplo, incluido en un archivo de cabecera) para la unidad de traducción (archivo fuente) que la utiliza. Las plantillas, incluyendo gran parte de la biblioteca estándar, si no se incluyen en archivos de cabecera, no se pueden compilar. (Esto contrasta con el código sin plantilla, que puede compilarse a binario, proporcionando únicamente un archivo de cabecera de declaraciones para el código que lo utiliza). Esto puede ser una desventaja, ya que expone el código de implementación, lo que elimina algunas abstracciones y podría restringir su uso en proyectos de código cerrado.

Además de la metaprogramación con plantillas, D también proporciona varias características para permitir la generación de código en tiempo de compilación:

• Esta importexpresión permite leer un archivo del disco y utilizar su contenido como una expresión de cadena.
• La reflexión en tiempo de compilación permite enumerar e inspeccionar las declaraciones y sus miembros durante el proceso de compilación.
• Los atributos definidos por el usuario permiten a los usuarios adjuntar identificadores arbitrarios a las declaraciones, que luego pueden enumerarse mediante reflexión en tiempo de compilación.
• La ejecución de funciones en tiempo de compilación (CTFE) permite interpretar un subconjunto de D (restringido a operaciones seguras) durante la compilación.
• Los mixins de cadena permiten evaluar y compilar el contenido de una expresión de cadena como código D que pasa a formar parte del programa.

La combinación de lo anterior permite generar código a partir de declaraciones existentes. Por ejemplo, los marcos de serialización D pueden enumerar los miembros de un tipo y generar funciones especializadas para cada tipo serializado, realizando así la serialización y deserialización. Los atributos definidos por el usuario podrían indicar además las reglas de serialización.

La importexpresión y la ejecución de funciones en tiempo de compilación también permiten implementar de manera eficiente lenguajes específicos de dominio . Por ejemplo, dada una función que toma una cadena que contiene una plantilla HTML y devuelve el código fuente D equivalente, es posible usarla de la siguiente manera:

// Importa el contenido de example.htt como una constante de manifiesto de cadena. enum htmlTemplate = import ( "example.htt" );// Transpilar la plantilla HTML a código D. enumeración htmlDCode = htmlTemplateToD ( htmlTemplate );// Pega el contenido de htmlDCode como código D. mixin ( htmlDCode );

Las clases genéricas se declaran con su nombre de clase y una lista de uno o más parámetros genéricos formales . En el siguiente código, la clase LISTtiene un parámetro genérico formal.G

clase LISTA [ G ] ... característica -- Acceso al elemento : G -- El elemento al que apunta actualmente el cursor ... característica -- Cambio de elemento put ( new_item : G ) -- Agregar `new_item' al final de la lista ...

Los parámetros genéricos formales son marcadores de posición para nombres de clases arbitrarios que se proporcionarán cuando se haga una declaración de la clase genérica, como se muestra en las dos derivaciones genéricas a continuación, donde ACCOUNTy DEPOSITson otros nombres de clases. ACCOUNTy DEPOSITse consideran parámetros genéricos reales ya que proporcionan nombres de clases reales para sustituir Gen el uso real.

lista_de_cuentas : LISTA [ CUENTA ] -- Lista de cuentaslista_de_depósitos : LISTA [ DEPÓSITO ] -- Lista de depósitos

Dentro del sistema de tipos Eiffel, aunque una clase LIST [G]se considera una clase, no se considera un tipo. Sin embargo, una derivación genérica de LIST [G]tal tipo LIST [ACCOUNT]sí se considera un tipo.

Para la clase de lista mostrada arriba, un parámetro genérico real que sustituye a Gpuede ser cualquier otra clase disponible. Para restringir el conjunto de clases de las que se pueden elegir parámetros genéricos reales válidos, se puede especificar una restricción genéricaSORTED_LIST . En la declaración de la clase que se muestra a continuación, la restricción genérica dicta que cualquier parámetro genérico real válido será una clase que herede de la clase COMPARABLE. La restricción genérica garantiza que los elementos de una lista SORTED_LISTse puedan ordenar.

clase LISTA_ORDENADA [ G -> COMPARABLE ]

El dialecto Object Pascal de Delphi incorporó genéricos en la versión Delphi 11 de 2007, publicada por CodeGear . Inicialmente, solo estaban disponibles en el compilador .NET (ya descontinuado), antes de integrarse al código nativo en la versión Delphi 12 de 2009. La semántica y las capacidades de los genéricos de Delphi se basan en gran medida en las de los genéricos de .NET 2.0, aunque la implementación es, por necesidad, bastante diferente. A continuación, se presenta una traducción más o menos directa del primer ejemplo en C# mostrado anteriormente:

Programa de ejemplo ;{$APPTYPE CONSOLE}usa Generics.Defaults ; //para IComparer < >type TUtils = class class procedure MakeAtLeast < T > ( Arr : TArray < T >; const Lowest : T ; Comparer : IComparer < T > ) ; overload ; class procedure MakeAtLeast < T > ( Arr : TArray < T >; const Lowest : T ) ; overload ; end ;class procedure TUtils . MakeAtLeast < T > ( Arr : TArray < T >; const Lowest : T ; Comparer : IComparer < T > ) ; var I : Integer ; begin if Comparer = nil then Comparer := TComparer < T >. Default ; for I := Low ( Arr ) to High ( Arr ) do if Comparer . Compare ( Arr [ I ] , Lowest ) < 0 then Arr [ I ] := Lowest ; end ;class procedure TUtils . MakeAtLeast < T > ( Arr : TArray < T >; const Lowest : T ) ; begin MakeAtLeast < T > ( Arr , Lowest , nil ) ; end ;var Ints : TArray < Integer >; Value : Integer ; begin Ints := TArray < Integer >. Create ( 0 , 1 , 2 , 3 ) ; TUtils . MakeAtLeast < Integer > ( Ints , 2 ) ; for Value in Ints do WriteLn ( Value ) ; ReadLn ; end .

Al igual que en C#, los métodos y los tipos completos pueden tener uno o más parámetros de tipo. En el ejemplo, TArray es un tipo genérico (definido por el lenguaje) y MakeAtLeast un método genérico. Las restricciones disponibles son muy similares a las de C#: cualquier tipo de valor, cualquier clase, una clase o interfaz específica y una clase con un constructor sin parámetros. Varias restricciones actúan como una unión aditiva.

Free Pascal implementó los genéricos en 2006, en la versión 2.2.0 , antes que Delphi y con una sintaxis y semántica diferentes. Sin embargo, desde la versión 2.6.0 de FPC, la sintaxis al estilo Delphi está disponible al usar el modo de lenguaje {$mode Delphi}. Por lo tanto, el código de Free Pascal admite genéricos en ambos estilos.

Ejemplo con Delphi y Free Pascal:

// Unidad A de estilo Delphi ;{$ifdef fpc} {$mode delphi} {$endif}interfaztipo TGenericClass < T > = clase función Foo ( const AValue : T ) : T ; fin ;implementaciónfunción TGenericClass < T >. Foo ( const AValor : T ) : T ; comenzar resultado : = AValor + AValor ; fin ;fin .// Unidad B al estilo ObjFPC de Free Pascal ;{$ifdef fpc} {$mode objfpc} {$endif}interfaztipo genérico TGenericClass < T > = clase función Foo ( const AValue : T ) : T ; fin ;implementaciónfunción TGenericClass . Foo ( const AValor : T ) : T ; comenzar resultado : = AValor + AValor ; fin ;fin .// ejemplo de uso, programa estilo Delphi TestGenDelphi ;{$ifdef fpc} {$mode delphi} {$endif}utiliza A , B ;var GC1 : A . TGenericClass < Integer >; GC2 : B . TGenericClass < String >; begin GC1 := A . TGenericClass < Integer >. Create ; GC2 := B . TGenericClass < String >. Create ; WriteLn ( GC1 . Foo ( 100 )) ; // 200 WriteLn ( GC2 . Foo ( 'hello' )) ; // hellohello GC1 . Free ; GC2 . Free ; end .// ejemplo de uso, programa estilo ObjFPC TestGenDelphi ;{$ifdef fpc} {$mode objfpc} {$endif}utiliza A , B ;// requerido en ObjFPC tipo TAGenericClassInt = especializar A . TGenericClass < Integer >; TBGenericClassString = especializar B . TGenericClass < String >; var GC1 : TAGenericClassInt ; GC2 : TBGenericClassString ; begin GC1 := TAGenericClassInt . Create ; GC2 := TBGenericClassString . Create ; WriteLn ( GC1 . Foo ( 100 )) ; // 200 WriteLn ( GC2 . Foo ( 'hello' )) ; // hellohello GC1 . Free ; GC2 . Free ; end .

PolyP fue la primera extensión de lenguaje de programación genérico para Haskell . En PolyP, las funciones genéricas se denominan politípicas . El lenguaje introduce una construcción especial en la que dichas funciones politípicas pueden definirse mediante inducción estructural sobre la estructura del functor patrón de un tipo de dato regular. Los tipos de datos regulares en PolyP son un subconjunto de los tipos de datos de Haskell. Un tipo de dato regular t debe ser de tipo * → * , y si a es el argumento de tipo formal en la definición, entonces todas las llamadas recursivas a t deben tener la forma ta . Estas restricciones excluyen los tipos de datos de orden superior y los tipos de datos anidados, donde las llamadas recursivas tienen una forma diferente. La función flatten en PolyP se proporciona aquí como ejemplo:

aplanar :: Regular d => d a -> [ a ] ​​aplanar = cata flfl politípico :: f a [ a ] ​​-> [ a ] ​​caso f de g + h -> cualquiera fl fl g * h -> \ ( x , y ) -> fl x ++ fl y () -> \ x -> [] Par -> \ x -> [ x ] Rec -> \ x -> x d @ g -> concat . flatten . pmap fl Con t -> \ x -> []cata :: Regular d => ( FunctorOf d a b -> b ) -> d a -> b

Generic Haskell es otra extensión de Haskell , desarrollada en la Universidad de Utrecht en los Países Bajos . Las extensiones que proporciona son:

• Los valores indexados por tipo se definen como valores indexados a través de los distintos constructores de tipos de Haskell (unidades, tipos primitivos, sumas, productos y constructores de tipos definidos por el usuario). Además, podemos especificar el comportamiento de los valores indexados por tipo para un constructor específico mediante casos de constructor y reutilizar una definición genérica en otra mediante casos predeterminados .

El valor resultante, indexado por tipo, puede especializarse a cualquier tipo.

• Los tipos indexados por tipo son tipos indexados sobre tipos, definidos al proporcionar un caso para * y k → k' . Las instancias se obtienen aplicando el tipo indexado por tipo a un tipo.
• Las definiciones genéricas se pueden usar aplicándolas a un tipo o clase. Esto se denomina aplicación genérica . El resultado es un tipo o valor, según el tipo de definición genérica que se aplique.
• La abstracción genérica permite definir definiciones genéricas mediante la abstracción de un parámetro de tipo (de un tipo determinado).
• Los tipos indexados por tipo son aquellos que se indexan a través de los constructores de tipos. Se pueden usar para asignar tipos a valores genéricos más complejos. Los tipos indexados por tipo resultantes se pueden especializar a cualquier tipo.

Como ejemplo, la función de igualdad en Generic Haskell: ^{[ 34 ]}

tipo Eq {[ * ]} t1 t2 = t1 -> t2 -> Bool tipo Eq {[ k -> l ]} t1 t2 = para todo u1 u2 . Eq {[ k ]} u1 u2 -> Eq {[ l ]} ( t1 u1 ) ( t2 u2 )ecuación { | t :: k | } :: Ecuación {[ k ]} t t eq { | Unidad | } _ _ = Verdadero eq { | :+: | } eqA eqB ( Inl a1 ) ( Inl a2 ) = eqA a1 a2 eq { | :+: | } eqA eqB ( Inr b1 ) ( Inr b2 ) = eqB b1 b2 eq { | :+: | } eqA eqB _ _ = Falso eq { | :*: | } eqA eqB ( a1 :*: b1 ) ( a2 :*: b2 ) = eqA a1 a2 && eqB b1 b2 eq { | internacional | } = ( == ) ecuación { | Carbón | } = ( == ) ecuación { | booleano | } = ( == )