Si usted es un programador funcional experimentado en Haskell, OCaml, Rust o Scala, lo más probable es que haya trabajado antes con tipos de datos algebraicos (ADT, por sus siglas en inglés). Pero si es nuevo en el mundo de los ADT y está buscando una introducción a Simplicity para principiantes, este artículo (y esta serie) es para usted.
Este artículo es el primero de una serie y aborda los conceptos fundamentales de valores y tipos, y el siguiente tratará sobre funciones, expresiones y combinadores.
Pero antes de profundizar demasiado en esto, primero deberíamos definir qué son los valores, los tipos y las expresiones. Para comprender mejor este concepto, consideremos una expresión matemática simple.
(2 > 1) = True
Para nuestros propósitos, la expresión booleana (2 > 1) da como resultado el valor booleano True (verdadero). El tipo booleano representa una opción binaria en la que una expresión puede evaluarse como True (verdadera) o False (falsa). Estos dos valores constituyen el conjunto completo de valores posibles dentro del tipo booleano. A veces, las expresiones que evalúan con un valor booleano se denominan proposiciones, que es un término del campo de la lógica. Sin embargo, aquí no exploraremos este término en más profundidad. Un tipo representa un conjunto de valores posibles con características definidas. Los tipos nos permiten razonar sobre los valores de una manera estructurada. A diferencia de la mayoría de los lenguajes de programación, en los que las expresiones representan valores de un cierto tipo, en Simplicity, las expresiones representan funciones que asignan valores de un tipo de origen a un tipo de destino. Cuando se evalúan, estas expresiones producen un resultado mediante la transformación del valor de entrada. Y un valor es un dato concreto de un tipo específico.
nombre := expresión : tipo de origen → tipo de destino
Traducir la lógica en un código le exige al desarrollador considerar detalles de implementación, como el flujo de control, el manejo de errores y la eficiencia. Un mal manejo de cualquiera de estos aspectos puede provocar la introducción de errores en el código base. Los lenguajes como Haskell, Coq y Agda fueron diseñados específicamente para expresar conceptos y cálculos matemáticos, lo que da como resultado un código que se ajusta más a las matemáticas subyacentes y que produce menos errores que los lenguajes de programación habituales. Los lenguajes matemáticos se destacan en dos áreas clave: (1) la escritura de código para cálculos matemáticos y (2) el razonamiento formal. Ambas son muy valiosas en el contexto del dinero programable y están en línea con los principios centrales sobre los que se apoya el diseño de Simplicity.
Simplicity es un lenguaje de contratos inteligentes, de espíritu similar a Bitcoin Script o EVM. Como Hacspec (o TLA+ o Alloy), Simplicity también es un lenguaje de especificación, lo que significa que su semántica sigue un modelo matemático preciso que permite probar formalmente enunciados sobre programas. Si el contrato se escribe en Simplicity, las propiedades de corrección se pueden probar directamente. Por ejemplo, se puede probar que las monedas no pueden moverse sin la firma X o que el programa no puede superar el umbral de memoria Y.
Los tipos en Simplicity vienen en tres formas básicas:
- Un tipo de unidad define exactamente un valor posible. De tipo 1 (o alternativamente UNO)
- Un tipo de producto compone un par de tipos mediante una operación “y”. A × B
- Un tipo de suma combina dos tipos en una operación “o”. A + B
El sistema de tipos de Simplicity está formado en su totalidad por el tipo de unidad, tipos de suma y tipos de producto. Todos los tipos en Simplicity son combinaciones de estas tres operaciones de tipo de nivel bajo.
También hay muchos tipos que pueden derivarse de estos tipos fundamentales, que exploraremos en más profundidad en este artículo.
- El tipo de bit es la suma de dos tipos de unidad. 2 (o alternativamente DOS)
- Un tipo de opción es la suma de un tipo de unidad y un segundo tipo arbitrario. 1 + A
- Un tipo de palabra es el producto repetido del tipo de bit. 2ⁿ
Pero comencemos por el principio.
Al principio, no había nada. Y de la nada, ¡surgió el concepto del tipo de unidad!
Tipo de unidad (1, vacío)
El tipo de unidad tiene exactamente un valor, confusamente llamado también “unidad”. ¡Hermoso! ¿Pero qué significa esto?El tipo de unidad se escribe como 1, o UNO.
El valor de unidad se escribe como (). Podemos escribir () : 1 para indicar que () es de tipo 1.
El tipo de unidad es un tipo especial, una tupla vacía, porque no lleva información. Suele denominarse “empty” (vacío) porque contiene un solo valor. No hay manera de codificar información porque no hay opción de valor; hay uno solo. La entropía es cero. Usted podría preguntarse cuál es el propósito de un tipo que no tiene elementos distinguibles.
A pesar de su vacío aparente, el tipo de unidad permite componer tipos más complejos en Simplicity, lo que nos permite construir conceptos más grandes.
Tipo de suma (unión etiquetada)
Dados dos tipos, la suma de esos tipos contiene valores que incluyen un valor del tipo izquierdo (left) o un valor del tipo derecho (right). Escribimos estas opciones como:
left(a) : A + B donde el valor a : of type A (de tipo A)
right(b) : A + B donde el valor b : of type B (de tipo B)
Un tipo de suma es el conjunto de todos los valores que incluyen un valor de tipo A o bien un valor de tipo B. Al sumar el par, creamos un nuevo tipo que puede incluir valores de tipo A o B. Fundamentalmente, el tipo de suma nos fuerza a elegir entre izquierda y derecha. Si uno quiere tener ambos al mismo tiempo, se puede usar el tipo de producto, que abordaremos más adelante en este artículo.
El tipo de unidad representa una falta información, mientras que el tipo de suma lleva información al representar opciones o combinaciones de valores de sus tipos constituyentes. El tipo de suma incluye una etiqueta que identifica el tipo específico del valor, lo que permite hacer una distinción entre distintas posibilidades. Incluso cuando los dos valores de un par son idénticos, como sucede con left(a) y right(a) de tipo A + A, el hecho de que estén rodeados por distintas etiquetas (izquierda [left] y derecha [right]) es significativo.
El tipo “Either” (o) en Haskell es un tipo de suma y nos permite representar una opción entre dos tipos alternativos. El tipo de resultado de Rust también es un tipo de suma que garantiza que el código maneje tanto casos de éxito como de error. El tipo de suma de Simplicity es el mismo concepto que abarca la idea de combinar varias opciones en una.
Con la capacidad de sumar, el concepto de un bit emerge naturalmente.
Tipo bit (2, tipo booleano)
El tipo bit es la suma de dos tipos de unidad.Bit, definido por Bit := 1 + 1, 2, o DOS.
0 := left(()) : Bit
1 := right(()) : Bit
El tipo de bit es un tipo fundamental que representa una opción binaria. Puede tener uno de dos valores distintos, 0 o 1. En un tipo de suma, los valores corresponden a cualquiera de los dos tipos secundarios y están acompañados por una etiqueta que indica cuál es. En el caso del tipo de bit, ambos tipos secundarios son unidades y no proporcionan información adicional. Las etiquetas de izquierda y derecha llevan el bit real y proporcionan la nueva información.El tipo booleano (que se encuentra en lenguajes como Python, Java y C++) es un tipo de bit con un nombre diferente que también define una opción entre dos valores: True y False.
Booleano, escrito como Boolean := 1 + 1, 2, o DOS.
false := left(()) : Boolean
true := right(()) : Boolean
En Simplicity, estos dos tipos son 2. Como son estructuralmente iguales, son, en realidad, el mismo tipo. Si en lugar de sumar los dos tipos de unidad sumamos un único tipo de unidad con un segundo tipo arbitrario, obtenemos el tipo de opción.
Tipo de opción (anulable, tal vez)
Un tipo de opción es la suma de un tipo de unidad y otro tipo arbitrario.
Option[A] := 1 + A o A?Un tipo de opción, también conocido como tipo anulable (o nullable en inglés) o tipo tal vez (o maybe en inglés), abarca dos posibilidades: la ausencia de un valor (representada por el tipo de unidad 1) o la presencia de un valor (representada por el otro tipo A).
En Haskell, esto se denomina “Maybe”; en Rust se lo denomina “Option” (opción). Ambos son ejemplos de este tipo. El tipo permite manejar situaciones en las que un valor puede o no estar presente. Proporciona una manera de manejar y expresar explícitamente la ausencia de un valor.
Tipo de producto (tupla)
Dados dos tipos A y B, el tipo de producto de A y B contiene valores que incluyen un valor de A y un valor de B en un par.
Productos, escritos como (a, b) : A × B, donde (a,b) es un par de valores del tipo A × B.
Un tipo de valor representa un conjunto de pares de valores con uno de tipo A y uno de tipo B. En un tipo de producto, cualquier valor de tipo A puede emparejarse con cualquier valor de tipo B, lo que da como resultado |A| * |B| posibles combinaciones de valores.
Este par puede visualizarse como una operación “Y”, ya que combina dos valores en una única entidad. Se denomina tipo de producto porque su número de valores es el producto del número de valores de A y el número de valores de B. Incluimos valores del tipo izquierdo y derecho en el mismo valor de producto, lo que es diferente del tipo de suma, donde teníamos que decidir entre el tipo izquierdo o el derecho. El tipo de producto es poderoso porque proporciona una manera de expresar valores compuestos y nos permite crear estructuras jerárquicas y componer modelos de datos más grandes.
Otro término para el tipo de producto es “tupla”. Las tuplas son una estructura de datos común y son compatibles con la mayoría de los lenguajes de programación. Nos permiten definir y devolver varios valores, y representar cómodamente datos relacionados o pares de valor clave.
En Simplicity, un punto puede definirse usando un tipo de producto. Digamos que tenemos un tipo Int y queremos representar un punto en un espacio bidimensional con coordenadas x e y:
Point := Int × Int
Esto define un tipo denominado Point (punto) que representa un par de valores enteros (int).
Luego, podemos crear una instancia de un punto proporcionando valores para x e y:
p := (3, 5) : Point
Para representar una línea, podemos definir un tipo de producto que consiste en dos puntos, que representan el punto inicial y final de la línea.
Línea := punto × punto
Pero nos estamos adelantando si asumimos el uso de enteros. El problema con este ejemplo es que Simplicity no tiene un tipo entero incorporado que pueda representar números arbitrariamente grandes como los enteros en algunos otros lenguajes como Common Lisp o Python. En Simplicity, tenemos que trabajar con tipos de tamaño fijo.
Como ejemplo divertido de esta limitación, los lectores podrían recordar que en el juego “La leyenda de Zelda” el recuento máximo de monedas de Link estaba limitado a 255, porque las monedas se almacenaban como un número entero de 8 bits. Esto significa que el recuento de monedas solo podía variar entre 0 y 255, el valor máximo que puede representarse por un número entero de 8 bits.
Por lo tanto, ¿cómo abordamos el concepto del tamaño de bits en Simplicity?
Tipo de palabras (enteros de ancho fijo, caracteres)
Un tipo de palabra se crea combinando varias instancias de bits en un producto. El ancho de bits se refiere al número de bits que se combinan. Determina el tamaño de los datos binarios, como los números enteros o las palabras, y establece el intervalo de valores que pueden expresarse.
Por ejemplo:
2¹ := 2, representa un número entero de 1 bit, que es simplemente el tipo de bits.
2² := 2¹ × 2¹, representa el producto de dos tipos de bits, o una palabra de 2 bits.
2⁴ := 2² × 2², representa el producto de dos tipos de 2 bits, o una palabra de 4 bits.
2⁸ := 2⁴ × 2⁴, representa el producto de dos tipos de 4 bits, o de una palabra de 8 bits.
Y así sucesivamente, con anchos de banda cada vez mayores.
Una palabra de 4 bits es cualquiera de las 16 posibles combinaciones de cuatro ceros y unos. El tipo de palabra de 4 bits puede usarse para representar números desde 0000 a 1111 en notación binaria. Sin embargo, los valores binarios pueden alargarse rápidamente y resultar difíciles de leer, sobre todo en el caso de los números grandes. Los hexadecimales condensan cuatro dígitos binarios en uno, lo que hace que sea más fácil representar números.
HexDigit := 2⁴
B := 1011 : HexDigit
O podemos definir un carácter (Char) usando codificación ASCII:
Char := 2⁸
‘k’ := 0110 1011 : Char
Podemos definir una palabra de 8 bits como un Int:
Int8 := 2⁸
Y podemos usar un Int de 8 bits para implementar colores RGB:
RGB := ((Int8, Int8), Int8) : (2⁸ × 2⁸) × 2⁸
Cada Int8 en RGB representa los componentes rojo, verde y azul del color, y cada componente puede tomar cualquier valor entre el 0 y el 255 (2⁸ - 1) para representar la intensidad de ese canal de colores.
Para crear una instancia de un color RGB, podemos proporcionar valores específicos para cada componente:
BitcoinOrange := ((255, 153), 0) : RGB
Tipos finitos
La notación utilizada para los tipos en Simplicity no solo representa la estructura de un tipo, sino que también proporciona información sobre el número de valores distintos posibles. Por ejemplo, el tipo 2 + 2⁴, tiene un total de 18 valores diferentes.
En Simplicity todos los tipos son finitos. Esto significa que ciertos tipos, como una lista infinita definida como List := Item + (Item × List), no son posibles. Los tipos infinitos o recursivos plantean desafíos en lo que respecta a la terminación, la gestión de recursos y el razonamiento sobre el comportamiento del programa.
Al restringir los tipos para que sean finitos, Simplicity puede ofrecer mayores garantías sobre el comportamiento del programa, asegurar la terminación y permitir un análisis y una verificación rigurosos del código. Los tipos finitos son más que suficientes para los protocolos criptográficos. Además, cosas como STARK y SNARK (incluso las consolidaciones o roll-ups) tienen la capacidad para condensar cálculos extensos en análisis criptográficos sobre datos de tipos finitos relativamente pequeños.
Recursos de Simplicity
Si está ansioso por profundizar sobre Simplicity, puede encontrar la documentación técnica primaria sobre este lenguaje en el whitepaper y el Core Language Overview de la Wiki de Simplicity. Sin embargo, estos recursos podrían ser un poco difíciles para los programadores no funcionales. Por lo tanto, hemos iniciado un hilo de Simplicity general en la comunidad de Build On L2. Siéntase libre de hacernos allí cualquier pregunta que tenga. Mi objetivo con estos ejemplos es cerrar la brecha y ofrecer una explicación más accesible de estos conceptos. Simplicity, como lenguaje inspirado en las matemáticas, puede llevarnos a un mundo de dinero completamente programable, con contratos inteligentes formalmente verificados. Al comprender los tipos básicos de Simplicity, podemos establecer una base sólida para explorar funciones, expresiones y combinadores en la próxima entrega de esta serie.