Si vous êtes un programmeur expérimenté en Haskell, OCaml, Rust ou Scala, il y a de fortes chances que vous ayez déjà travaillé avec des types de données algébriques (ADT). Mais si vous êtes nouveau dans le monde des ADTs et que vous cherchez une façon simple de vous initier à Simplicity, cet article (et cette série) est pour vous !
Cet article est le premier d'une série qui couvre les fondamentaux des concepts de valeurs et de types. Le prochain article portera sur les fonctions, les expressions et les combinateurs.
Mais avant d'entrer dans le vif du sujet, nous devons d'abord définir ce que sont les valeurs, les types et les expressions. Pour mieux comprendre ces concepts, considérons une simple expression mathématique.
(2 > 1) = True
Dans notre cas, l'expression booléenne (2 > 1) donne la valeur booléenne True. Le type booléen représente un choix binaire où une expression peut être évaluée à True ou False. Ces deux valeurs constituent l'ensemble des valeurs possibles dans le type booléen. Parfois, les expressions qui évaluent une valeur booléenne sont appelées propositions, un terme issu du domaine de la logique. Toutefois, nous n'approfondirons pas ce terme ici.
Un type représente un ensemble de valeurs possibles avec des caractéristiques définies. Les types nous permettent de considérer des valeurs de manière structurée. Contrairement à la plupart des langages de programmation où les expressions représentent des valeurs d'un certain type, dans Simplicity, les expressions représentent des fonctions qui font correspondre des valeurs d'un type source à un type cible. Lorsqu'elles sont évaluées, ces expressions produisent un résultat en transformant la valeur d'entrée. Une valeur est une donnée concrète d'un type spécifique.
name := expression : source type → target type
La traduction de la logique en code exige du développeur qu'il prenne en compte les détails de la mise en œuvre, tels que le flux de contrôle, la gestion des erreurs et l'efficacité. Une mauvaise gestion de l'un de ces aspects peut conduire à l'introduction de bogues dans le code. Les langages tels que Haskell, Coq et Agda sont conçus spécifiquement pour exprimer des concepts et des calculs mathématiques, ce qui permet d'obtenir un code plus proche des mathématiques sous-jacentes, avec moins de bogues que les langages de programmation classiques. Les langages mathématiques excellent dans deux domaines clés : (1) l'écriture de code pour les calculs mathématiques et (2) le raisonnement formel. Ces deux aspects sont extrêmement précieux dans le contexte de la monnaie programmable et sont conformes aux principes fondamentaux qui sous-tendent la conception de Simplicity.
Simplicity est un langage de contrat intelligent, similaire à Bitcoin Script ou EVM. Comme Hacspec (ou TLA+, ou Alloy), Simplicity est aussi un langage de spécification, ce qui signifie que sa sémantique a un modèle mathématique précis qui permet de prouver formellement des déclarations sur les programmes. Si le contrat est écrit en Simplicity, vous pouvez prouver directement l'exactitude de ses propriétés. Par exemple, vous pouvez prouver que les pièces ne peuvent pas se déplacer sans la signature X, ou que le programme ne peut pas dépasser le seuil de mémoire Y.
Les types dans Simplicité se présentent sous trois formes de base :
● Un type unité définit exactement une valeur possible. De type 1 (ou alternativement ONE)
● Un type produit compose une paire de types à l'aide d'une opération "et". A × B
● Un type somme combine deux types dans une opération "ou". A + B
Le système de types de Simplicity est entièrement constitué de types d'unités, de types de sommes et de types de produits. Tous les types de Simplicity sont des combinaisons de ces trois opérations de bas niveau.
Il existe également de nombreux types qui peuvent être dérivés de ces types fondamentaux, que nous explorerons plus en détail dans ce billet.
● Le type bit est la somme de deux types d'unités. 2 (ou alternativement DEUX)
● Un type option est la somme d'un type d'unité et d'un second type arbitraire. 1 + A
● Un type mot est le produit répété du type de bit. 2ⁿ
Mais commençons par le début.
Au début, il n'y avait rien. Et c'est du néant qu'est né le concept de type d'unité !
Type unité (1, vide)
Le type unité a exactement une valeur, appelée aussi "unité", ce qui peut prêter à confusion. Mais qu'est-ce que cela signifie ?
Le type unité s'écrit 1, ou ONE.
La valeur unitaire s'écrit (). On peut écrire () : 1 pour indiquer que () est de type 1.
Le type unité est un type spécial, un uplet vide, car il ne contient aucune information. Il est souvent appelé "vide" parce qu'il contient une seule valeur. Il n'y a aucun moyen d'encoder une quelconque information parce que vous n'avez pas le choix de la valeur ; il n'y en a qu'une. L'entropie est nulle. On peut se demander à quoi sert un type qui n'a pas d'éléments distinctifs.
Malgré son apparente vacuité, le type unité permet de composer des types plus complexes dans Simplicité, ce qui nous permet de construire des concepts plus larges.
Type somme (Union disjointe)
Étant donné deux types, la somme de ces types contient des valeurs qui enveloppent soit une valeur du type gauche, soit une valeur du type droit. Nous écrivons ces choix comme suit :
left(a) : A + B où la valeur a : de type A
right(b) : A + B où la valeur b : de type B
Un type somme est l'ensemble de toutes les valeurs qui englobent soit une valeur de type A, soit une valeur de type B. En additionnant la paire, nous créons un nouveau type qui peut contenir des valeurs de type A ou B. Fondamentalement, le type somme vous oblige à choisir entre la gauche et la droite. Si vous voulez avoir les deux en même temps, vous pouvez utiliser le type produit, que nous aborderons plus loin dans cet article.
Le type unité représente un manque d'informations, tandis que le type somme véhicule des informations en représentant des choix ou des combinaisons de valeurs de leurs types constitutifs. Le type somme comprend une étiquette qui identifie le type spécifique de la valeur, ce qui permet de distinguer les différentes possibilités. Même lorsque les deux valeurs d'une paire sont identiques, comme dans le cas de left(a) et de right(a) du type A + A, le fait qu'elles soient accompagnées d'étiquettes différentes (gauche et droite) est significatif.
Le type Either en Haskell est un type somme, et nous permet de représenter un choix entre deux types alternatifs. Le type Result en Rust est également un type somme, qui garantit que le code gère à la fois les cas de réussite et d'erreur. Le type sum en Simplicity est le même concept qui englobe l'idée de combiner plusieurs options en une seule.
Avec la capacité d'additionner, le concept de bit émerge naturellement.
Type bit (2, type booléen)
Le type de bit est la somme de deux types unité.
Bit, défini par Bit := 1 + 1, 2, ou DEUX.
0 := left(()) : Bit
1 := right(()) : Bit
Le type de bit est un type fondamental qui représente un choix binaire. Il peut avoir l'une des deux valeurs distinctes, 0 ou 1. Dans un type somme, les valeurs correspondent à l'un ou l'autre des deux types enfants et sont accompagnées d'une étiquette indiquant de quel type il s'agit. Dans le cas du type bit, les types enfants sont tous deux des unités et ne fournissent aucune information supplémentaire. Les étiquettes de gauche et de droite portent le bit réel, qui fournit la nouvelle information.
Le type booléen (tel qu'on le trouve dans des langages comme Python, Java et C++) est juste un type de bit avec un nom différent qui définit également un choix entre deux valeurs : Vrai et Faux.
Booléen, écrit comme Booléen := 1 + 1, 2, ou DEUX.
false := left(()) : Booléen
true := right(()) : Booléen
Dans Simplicity, ces types sont tous les deux 2. Parce qu'ils sont structurellement égaux, ils sont en fait le même type. Si, au lieu d'additionner deux types d'unités, nous additionnons un seul type d'unité avec un second type arbitraire, nous obtenons le type option.
Type option (Nullable, Maybe)
Un type option est la somme d'un type unité et de tout autre type arbitraire.
Option[A] := 1 + A ou A ?
Un type option, également connu sous le nom de type nullable ou maybe, encapsule deux possibilités : soit l'absence d'une valeur (représentée par le type unité 1), soit la présence d'une valeur (représentée par l'autre type A).
En Haskell, cela s'appelle Maybe ; en Rust, cela s'appelle Option. Les deux sont des exemples de ce type. Ce type permet de gérer des situations où une valeur peut être présente ou non. Il permet de gérer et d'exprimer explicitement l'absence d'une valeur.
Type produit (Uplet)
Étant donné deux types A et B, le type produit de A et B contient des valeurs qui regroupent une valeur de A et une valeur de B dans une paire.
Produits, écrits comme (a, b) : A × B, où (a,b) est une paire de valeurs de type A × B.
Un type produit représente un ensemble de paires de valeurs dont l'une est de type A et l'autre de type B. Dans un type produit, toute valeur de type A peut être associée à n'importe quelle valeur de type B, ce qui donne |A| * |B| combinaisons possibles de valeurs.
Cette paire peut être visualisée comme une opération "ET", puisqu'elle combine deux valeurs en une seule entité. On l'appelle le type produit parce que son nombre de valeurs est le produit du nombre de valeurs dans A et du nombre de valeurs dans B. Nous enveloppons les valeurs des types gauche et droit dans la même valeur produit, ce qui est différent du type somme où nous devions décider entre le type gauche ou le type droit. Le type produit est puissant car il permet d'exprimer des valeurs composées et nous permet de construire des structures hiérarchiques et de composer des modèles de données plus vastes.
Un autre terme pour désigner un type de produit est le uplet. Les uplets sont une structure de données courante et sont pris en charge par la plupart des langages de programmation. Ils nous permettent de définir et de renvoyer des valeurs multiples et de représenter de manière pratique des données connexes ou des paires clé-valeur.
Dans Simplicity, un point peut être défini à l'aide d'un type produit. Disons que nous avons un type Int, et que nous voulons représenter un point dans un espace à deux dimensions avec des coordonnées x et y :
Point := Int × Int
Il définit un type appelé Point qui représente une paire de valeurs entières.
Nous pouvons ensuite créer une instance d'un point en fournissant des valeurs pour x et y :
p := (3, 5) : Point
Pour représenter une ligne, nous pouvons définir un type produit composé de deux points, représentant les points de départ et d'arrivée de la ligne.
Ligne := Point × Point
Mais nous prenons un peu d'avance en supposant l'utilisation d'entiers. Le problème de cet exemple est que Simplicity n'a pas de type entier intégré qui puisse représenter des nombres arbitrairement grands comme les entiers dans d'autres langages tels que Common Lisp ou Python. Dans Simplicity, nous devons travailler avec des types de taille fixe.
Pour un exemple amusant de cette limitation, les lecteurs se souviendront peut-être que dans le jeu "The Legend of Zelda", le nombre maximum de pièces de Link était limité à 255, parce que les pièces étaient stockées sous la forme d'un nombre entier de 8 bits. Cela signifie que le nombre de pièces ne pouvait être compris qu'entre 0 et 255, la valeur maximale pouvant être représentée par un entier de 8 bits.
Alors, comment aborder le concept de taille des bits dans Simplicité ?
Types mot (entiers de largeur fixe, caractères)
Un type de mot est construit en combinant plusieurs instances de bits dans un produit. La largeur des bits fait référence au nombre de bits qui sont combinés. Elle détermine la taille des données binaires, telles que les nombres entiers ou les mots, et établit la gamme des valeurs qui peuvent être exprimées.
Par exemple :
2¹ := 2, représente un entier de 1 bit, qui est simplement le type de bit.
2² := 2¹ × 2¹, représente le produit de deux types de bits, ou un mot de 2 bits.
2⁴ := 2² × 2², représente le produit de deux types de 2 bits, ou d'un mot de 4 bits.
2⁸ := 2⁴ × 2⁴, représente le produit de deux types de 4 bits, ou d'un mot de 8 bits.
Et ainsi de suite, avec des largeurs de bits croissantes.
Un mot de 4 bits est l'une des 16 combinaisons possibles de quatre 0 ou 1. Le type de mot de 4 bits peut être utilisé pour représenter les nombres de 0000 à 1111 en notation binaire. Toutefois, les valeurs binaires peuvent rapidement devenir longues et difficiles à lire, en particulier pour les nombres les plus élevés. L'hexadécimal condense quatre chiffres binaires en un seul, ce qui facilite la représentation des nombres.
HexDigit := 2⁴
B := 1011 : HexDigit
Nous pouvons également définir un caractère en utilisant le codage ASCII :
Char := 2⁸
'k' := 0110 1011 : Char
Nous pouvons définir un mot de 8 bits comme un Int :
Int8 := 2⁸
Nous pouvons utiliser un Int 8 bits pour mettre en œuvre les couleurs RVB :
RGB := ((Int8, Int8), Int8) : (2⁸ × 2⁸) × 2⁸
Chaque Int8 dans RVB représente les composantes rouge, verte et bleue de la couleur, et chaque composante peut prendre une valeur comprise entre 0 et 255 (2⁸ - 1) pour représenter l'intensité de ce canal de couleur.
Pour créer une instance d'une couleur RVB, nous pouvons fournir des valeurs spécifiques pour chaque composante :
BitcoinOrange := ((255, 153), 0) : RVB
Types finis
La notation utilisée pour les types dans Simplicity ne représente pas seulement la structure d'un type, mais fournit également des indications sur le nombre de valeurs distinctes possibles. Par exemple, le type 2 + 2⁴ a un total de 18 valeurs différentes.
Dans Simplicité, tous les types sont finis. Cela signifie que certains types, tels qu'une liste infinie définie comme List := Item + (Item × List), ne sont pas possibles. Les types infinis ou récursifs posent des problèmes en termes de terminaison, de gestion des ressources et de raisonnement sur le comportement du programme.
En limitant les types à des types finis, Simplicity peut fournir des garanties plus fortes sur le comportement du programme, assurer la terminaison et permettre une analyse et une vérification rigoureuses du code. Les types finis sont plus que suffisants pour les protocoles cryptographiques. De plus, des choses comme STARKS et SNARKs (même les roll-ups) ont la capacité de condenser des calculs étendus en une analyse cryptographique sur des données de types finis relativement petits.
Les resources
Si vous souhaitez approfondir votre connaissance de Simplicity, la documentation technique principale sur le langage se trouve dans le livre blanc et la vue d'ensemble du langage sur le Wiki Simplicity. Cependant, ces ressources peuvent s'avérer quelque peu difficiles pour les programmeurs non initiés, c'est pourquoi nous avons lancé un fil de discussion sur Simplicity dans la communauté Build On L2. N'hésitez pas à nous poser vos questions.
Mon objectif avec ces exemples est de combler ce fossé et d'offrir une explication plus accessible de ces concepts. Simplicity, en tant que langage d'inspiration mathématique, pourrait nous faire entrer dans un monde de monnaie entièrement programmable, avec des contrats intelligents formellement vérifiés. En maîtrisant les types de base de Simplicity, nous pouvons établir une base solide pour explorer les fonctions, les expressions et les combinateurs dans les prochains articles de cette série.