Wenn du ein erfahrener funktionaler Programmierer in Haskell, OCaml, Rust oder Scala bist, hast du wahrscheinlich schon mit Algebraischen Daten-Typen (ADTs) gearbeitet. Wenn die Welt der ADTs für dich aber ganz neu ist und du nach einer einsteigerfreundlichen Einführung in Simplicity suchst, dann ist dieser Beitrag (und die ganze Serie) genau das richtige für dich!
Dieser Beitrag ist der erste in einer Reihe, der erstmal die grundlegenden Konzepte von Werten und Typen abdecken sollen, und in den folgenden Beiträgen werden wir dann Funktionen, Ausdrücke und Kombinatoren behandeln.
Aber bevor wir zu tief einsteigen, sollten wir erstmal definieren, was Werte, Typen und Ausdrücke sind. Um diese Konzepte besser zu verstehen, wollen wir uns einen einfachen mathematischen Ausdruck anschauen.
(2 > 1) = True
Für unsere Zwecke resultiert der Boolsche Ausdruck (2 > 1) im Booleschen Wert Wahr. Der Boolsche Typ repräsentiert eine binäre Wahl, bei der ein Ausdruck entweder Wahr oder Falsch als Wert zurückgeben kann. Diese beiden Werten sind damit die vollständige Menge der möglichen Werte innerhalb des Booleschen Typs. Manchmal werden Ausdrücke, die als Boolsche Werte ausgegeben werden, als Propositionen bezeichnet, das ein Begriff aus dem Bereich der Logik ist. Wir werden aber hier und heute diesen Ausdruck nicht tiefer ergründen.
Ein Typ repräsentiert eine Menge an möglichen Werten mit definierten Charakteristiken. Typen ermöglichen es uns, über Werte in einer strukturierten Weise nachzudenken. Anders als bei den meisten Programmiersprachen, bei denen Ausdrücke bestimmte Werte von ganz bestimmtem Typ meinen, repräsentieren Ausdrücke in Simplicity Funktionen, die Werte von einem Quelltyp auf einen Zieltyp abbilden. Wenn sie ausgewertet werden, produzieren diese Ausdrücke Ergebnisse durch die Transformation eines Eingabewerts. Und ein Wert ist ein konkretes Datum eines bestimmten Typs.name := expression : source type → target type
name := expression : source type → target type
Logik in Code umzuwandeln erfordert von einem Entwickler, die Implementierungsdetails zu beachten, zum Beispiel den Kontrollfluss, Fehlerbehandlung und Effizienz. Der falsche Umgang mit diesen Aspekten kann zur Einführung von Bugs in der Codebasis führen. Sprachen wie Haskell, Coq und Agda sind speziell dafür entworfen worden, um mathematische Konzepte und Berechnungen auszudrücken, was in Code resultiert, der sehr nah an der zugrundeliegenden Mathematik ist und daher weniger Bugs enthält als andere Programmiersprachen. Mathematische Sprachen ragen insbesondere in zwei Aspekten heraus: (1) Code für mathematische Berechnungen schreiben, und (2) formale Argumentation. Beide Aspekte sind im Kontext programmierbaren Geldes sehr wertvoll und stehen im Einklang mit den Kernprinzipien, die das Design von Simplicity untermauern.
Simplicity ist eine Smart Contract-Sprache, ganz im Geiste von Bitcoin Script oder EVM, Hacspec (oder TLA+ oder Alloy). Simplicity ist aber auch eine Spezifikations-Sprache, d.h. seine Semantik folgt einem präzisen mathematischen Modell, das es erlaubt, Aussagen über Programme formal zu beweisen. Wenn ein Contract in Simplicity geschrieben ist, kann seine Korrektheit direkt bewiesen werden. Zum Beispiel kann man beweisen, dass Coins nicht ohne Signatur X bewegt werden können, oder dass ein Programm den Memory-Grenzwert Y nicht überschreiben kann.
Typen in Simplicity gibt es in drei Grundformen:
- Ein Unit-Typ definiert genau einen möglichen Wert. Des Typs 1 (oder Alternativ ONE)
- Ein Produkt-Typ setzt ein Paar von Typen durch eine “und”-Operation zusammen. A × B
- Ein Summen-Typ kombiniert zwei Typen in einer “oder”-Operation. A + B
Das Typensystem von Simplicity besteht nur aus Unit-Typen, Summen-Typen und Produkt-Typen. Alle weiteren Typen in Simplicity sind Kombinationen aus diesen drei niedrigeren Typ-Operationen.
Aus diesen Grundformen lassen sich viele Typen ableiten, was wir im weiteren Verlauf dieses Blogbeitrages ausarbeiten werden.
- Der Bit-Typ ist ist die Summe von zwei Unit-Typen. 2 (oder alternativ TWO)
- Ein Options-Typ ist die Summe eines Unit-Typ und eines zweiten beliebigen Typ. 1 + A
- Ein Wort-Typ ist das wiederholte Produkt des Bit-Typs. 2ⁿ
Aber lasst uns ganz von vorne beginnen.
Im Anfang war nichts. Und aus dem Nichts entstieg das Konzept des Unit-Typs!
Unit-Typ (1, Empty)
Der Unit-Typ hat genau einen Wert, der verwirrenderweise auch “unit” genannt wird. Wunderbar! Aber was bedeutet das?
Der Unit-Typ wird geschrieben als 1, oder ONE.Der Unit-Wert wird geschrieben als (). We können also schreiben () : 1 um zu verdeutlichen, dass () vom Typ 1 ist.
Der Unit-Typ is ein spezieller Typ, ein leeres Tupel, weil es keine Informationen trägt. Es wird wird häufig als “leer” bezeichnet, weil es einen einzelnen Wert beinhaltet. Es gibt keine Möglichkeit, irgendeine Information zu codieren, da man beim Wert keine Wahl hat: es gibt nur diesen einen. Die Entropie ist Null. Du magst dich fragen, was ein solcher Typ bezwecken soll, der keine unterscheidbaren Elemente hat.
Doch trotz seiner anscheinenden Leere, ermöglicht dieser Unit-Typ die Komposition von komplexeren Typen in Simplicity, was uns erlaubt, größere Konzepte aufzubauen.
Summen-Typ (Tagged Union)
Wenn zwei Typen gegeben sind, ann enthält die Summe dieser Typen entweder den Wert des linken Typs oder den Wert des rechten Typs. Wir schreiben diese Auswahlmöglichkeiten als:
left(a) : A + B wobei Wert a : of type A
right(b) : A + B wobei Wert b : of type B
Ein Summen-Typ ist die Menge aller Werte, die entweder einen Wert von Typ A oder einen Wert von Typ B umhüllen. Durch die Summierung des Paares erschaffen wir einen neuen Typ, der Werte des Typs A oder B enthalten kann. Grundsätzlich gesprochen zwingt dich der Summen-Typ, zwischen links und rechts zu wählen. Wenn du beides zugleich haben möchtest, kannst du den Produkt-Typ verwenden, was wir später in diesem Beitrag erkunden werden.
Der Unit-Typ repräsentiert das Fehlen von Information, während der Summen-Typ Informationen trägt, indem Auswahlmöglichkeiten zwischen oder Kombinationen von Werten der konstitutiven Typen repräsentiert sind. Der Summentyp enthält ein Label oder Tag, das den spezifischen Typ des Wertes identifiiziert, und damit die Unterscheidung zwischen verschiedenen Möglichkeiten erlaubt. Auch wenn die zwei Werte eines Paares identisch sind, so zum Beispiel bei left(a) und right(a) des A + A-Typs, so ist die Tatsache, dass sie mit unterschiedlichen Labels eingefasst sind (left und right), signifikant.
Der “Either”-Typ in Haskell ist ein Summen-Typ und erlaubt uns, eine Auswahl zwischen zwei alternativen Typen zu repräsentieren. Der Result-Typ in Rust ist ebenfalls ein Summen-Typ, der sicherstellt, dass der Code Erfolgs- und Fehlerfälle verarbeitet. Der Summen-Typ in Simplicity ist dasselbe Konzept, das die Kombination mehrerer Optionen umfasst.
Mit der Möglichkeit zu summieren, entsteht fast schon natürlich das Konzept eines Bit.
Bit-Typ (2, Boolean Type)
Der Bit-Typ ist die Summe von zwei Unit-Typen.
Bit, definiert als Bit := 1 + 1, 2, oder TWO.
0 := left(()) : Bit
1 := right(()) : Bit
Der Bit-Typ ist ein fundamentaler Typ, der eine binäre Auswahl repräsentiert. Er kann einen von zwei distinkten Werten ahben, 0 oder 1. In einem Summen-Typ korrespondieren die Werte zu ausschließlich einem der beiden Child-Typen und werden von einem Label begleitet, der anzeigt, um welchen es sich handelt. Im Fall des Bit-Typs sind die Child-Typen beides Einheiten und liefern darüber hinaus keine weiteren Informationen. Das left- und right-Label tragen das eigentliche Bit, was neue Informationen liefert.
Boole’scher Typ (wie wir sie in Sprachen wie Python, Java und C++ vorfinden) ist nur ein Bit-Typ mit einem anderen Namen, der auch eine Wahl zwischen zwei Werten definiert: True und False.
Boolean, geschrieben Boolean := 1 + 1, 2, oder TWO.
false := left(()) : Boolean
true := right(()) : Boolean
In Simplicity sind beide Typen 2. Weil sie strukturell gleich sind, sind sie tatsächlich vom selben Typ. Wenn wir statt zwei Unit-Typen einen einzelnen Unit-Typ mit einem willkürlichen Typ summieren, bekommen wir den Options-Typ.
Options-Typ (Nullable, Maybe)
Ein Options-Typ ist die Summe aus einem Unit-Typ und jeglichen anderen Typ.
Option[A] := 1 + A or A?
Ein Options-Typ, auch bekannt als nullable- oder maybe-Typ, enthält zwei Möglichkeiten: entweder die Abwesenheit eines Wertes (repräsentiert durch den Unit-Typ 1) oder die Anwesenheit eines Wertes (repräsnetiert durch den anderen Typ A).
In Haskell nennt man das Maybe; in Rust heißt es Option. Beide sind Beispiele für diesen Typ. Dieser Typ ermöglicht die Behandlung von Situationen, in denen ein Wert vorhanden sein kann oder auch nicht. Es gibt uns eine Möglichkeit, das Fehlen eines Wertes explizit zu behandeln und auszudrücken.
Product-Typ (Tupel)
Gegeben seien zwei Typen A und B, dann enthält der Produkt-Typ von A und B Werte, die den Wert von A und den Wert von B in einem Paar umfassen.
Produkte, geschrieben als (a, b) : A × B, wobei (a,b) ein Wert-Paar des A × B-Typs ist.
Ein Produkt-Typ repräsentiert eine Menge an Wertpaaren mit je einem Typ A und einem Typ B. In einem Produkt-Typ kann jeder Wert des Typs A mit jedem Wert des Typs B kombiniert werden, was in |A| * |B| möglichen Kombinationen von Werten resultiert.
Dieses Paar kann als “UND”-Operation visualisiert werden, da es zwei Werte in einer einzigen Entität kombiniert. Es wird als Produkt-Typ bezeichnet, weil die Anzahl seiner Werte das Produkt der Anzahl der Werte in A und der Anzahl der Werte in B ist. Wir verpacken die Werte des left- und right-Typ im selben Produktwert, der sich vom Summen-Typ unterscheidet, wo wir zwischen left- und right-Typ entscheiden mussten. Der Produkt-Typ ist mächtig, weil es eine Möglichkeit bietet, zusammengesetzte Werte auszudrücken und uns erlaubt, hierarchische Strukturen zu bauen und größere Datenmodelle zusammenzustellen.
Ein anderer Begriff für den Produkt-Typ ist Tupel. Tupel sind eine bekannte Datenstruktur und werden von den meisten Programmiersprachen unterstützt. So können wir multiple Werte definieren und ausgeben, und sehr bequem verwandte Daten oder Schlüssel-Wert-Paare wiedergeben.
In Simplicity kann ein Punkt als ein Produkt-Typ definiert werden. Wenn wir also sagen, dass wir einen Int-Typ haben und einen Punkt in einem zweidimensionalen Raum mit x- und y-Koordinaten darstellen wollen:
Point := Int × Int
So haben wir einen Typ namens Point definiert, der ein Paar aus ganzzahligen Werten darstellt.
Wir können damit eine Instanz eines Point erschaffen, indem wir Werte für x und y liefern:
p := (3, 5) : Point
Um eine Linie darzustellen, definieren wir einen Produkt-Typ, der aus zwei Points besteht, die den Start- und Endpunkt der Linie darstellen.
Line := Point × Point
Aber wir sind ein wenig zu weit vorausgeeilt, da wir die Verwendung von ganzen Zahlen annehmen. Das Problem mit diesem Beispiel ist nämlich, dass Simplicity keinen Integer-Typ eingebaut hat, der beliebig große Zahlen darstellen kann, wie es andere Sprachen wie Common Lisp oder Python können. In Simplicity müssen wir mit Typen fester Größe arbeiten.
Um ein lustiges Beispiel für diese Limitierung zu zitieren, mag sich der Leser vielleicht daran erinnern, dass im Spiel “Legend of Zelda” die maximale Zahl an Coins, die Link besitzen konnte, auf 255 begrenzt war, weil die Coins als 8-bit Integer gespeichert wurden. Das hatte zur Folge, dass die Zahl der Coins nur zwischen 0 und 255 liegen konnte, der höchste Wert, der durch eine 8-Bit Integer dargestellt werden kann.
Wie gehen wir also das Konzept von Bit-Größen in Simplicity an?
Wort-Typen (Fixed-Width Integers, Characters)
Ein Wort-Typ wird durch die Kombination von mehreren Instanzen von Bits in einem Produkt konstruiert. Die Bitbreite (bit width) referenziert dabei auf die Anzahl an Bits, die kombiniert werden. Damit wird die Größe der binären Daten festgelegt, zum Beispiel Ganzzahlen oder Wörter, und der Bereich von Werten, die ausgedrückt werden können.
Ein Beispiel
2¹ := 2, repräsentiert einen 1-bit Integer, also einfach den Bit-Typ.
2² := 2¹ × 2¹, repräsentiert das Produkt von zwei Bit-Typen, oder ein 2-Bit-Wort.
2⁴ := 2² × 2², repräsentiert das Produkt aus zwei 2-Bit-Typen, oder ein 4-Bit-Wort.
2⁸ := 2⁴ × 2⁴, repräsentiert das Produkt von zwei 4-Bit-Typen, oder ein 8-Bit-Wort.
Und so weiter, bei steigender Bitbreite.
Ein 4-Bit-Wort ist jede der 16 möglichen Kombinationen aus 4 Nullen und Einsen. Der 4-Bit-Wort-Typ kann genutzt werden, um Zahlen zwischen 0000 und 1111 in binärer Notation darzustellen. Jedoch können binäre Werte sehr schnell sehr lang und schwer zu lesen werden, insbesondere bei großen Zahlen. Hexadezimal fasst die vier binären Digits zu einem zusammen, was die Darstellung von Zahlen vereinfacht.
HexDigit := 2⁴
B := 1011 : HexDigit
Oder wir definieren ein Char mit ASCII-Codierung:
Char := 2⁸
‘k’ := 0110 1011 : Char
Wir können ein 8-Bit-Wort als ein Int definieren:
Int8 := 2⁸
Und wir könen einen 8-Bit-Int benutzen, um die RGB-Farben zu implementieren:
RGB := ((Int8, Int8), Int8) : (2⁸ × 2⁸) × 2⁸
Jedes Int8 in RGB repräsentiert rote, grüne und blaue Komponenten der Farbe und jede Komponente kann jeglichen Wert von 0 bis 255 (28 - 1) annehmen um die Intensität im jeweiligen Farbbereich zu repräsentieren.
Um eine Instanz einer RGB-Farbe zu erstellen, können wir spezifische Werte für jede Komponente angeben:
BitcoinOrange := ((255, 153), 0) : RGB
Finite Typen
Die Notation für Typen in Simplicity stellt nicht Struktur eines Typs dar, sondern liefert auch einen Einblick in die Anzahl der möglichen distinkten Werte. Zum Beispiel hat der Typ 2 + 24 eine Gesamtmenge von 18 verschiedenen Werten.
In Simplicity sind alle Typen endlich (finit). Das bedeutet, dass bestimmte Typen wie eine unendliche Liste, definiert als List := Item + (Item × List), nicht möglich sind. Unendliche oder rekursive Typen bringen eigene Herausforderungen mit sich bei Beendigung, Ressourcen-Management und beim Nachdenken über Programm-Verhalten.
Indem wir Typen auf finite beschränken, kann Simplicity stärkere Garantien über Programm-Verhalten abgeben, Beendigung sicherstellen und die exakte Analyse und Verifikation des Codes möglich machen. Finite Typen sind mehr als ausreichend für kryptographische Protokolle. Darüber hinaus haben Entwicklungen wie STARKS und SNARKS (auch Roll-ups) die Möglichkeit, umfangreiche Berechnungen zu einer kryptografischen Analyse von Daten aus relativ kleinen endlichen Typen zusammenzufassen.
Ressourcen zu Simplicity
Wenn du bereit bist, dich tiefer mit Simplicity zu beschäftigen, dann findest du die technische Dokumentation der Sprache im Whitepaper und in der Core Language Overview im Simplicity-Wiki. Da diese Ressourcen für nicht-funktionale Programmierer eine Herausforderung darstellen können, haben wir einen allgemein gehaltenen Simplicity Thread in der Build On L2-Community gestartet. Du kannst uns dort jederzeit gerne deine Fragen stellen.
Mein Ziel war es, mit diesen Beispielen die Lücke zu schließen und eine besser verständliche Erklärung der Konzepte zu liefern. Simplicity ist eine mathematisch-inspirierte Sprache, die uns eine Welt des vollständig programmierbaren Geldes mit formal verifizierbaren Smart Contracts bringen könnte. Durch das Verstehen der Kerntypen in Simplicity können wir eine solide Grundlage schaffen, um die Funktionen, Ausdrücke und Kombinatoren in den nächsten Ausgaben dieser Artikelserie zu erkunden.