Type-Driven Development für sicheres Codieren mit Typen

• Typen sind strenge Verträge, die Funktionen und Daten einhalten müssen
• Ein Typ ist eine Menge von Werten, zu der ein bestimmter Wert gehören kann
• Typen können durch Funktionen transformiert werden, wodurch sich ihr Wertebereich ändern kann
  • Injektive Funktion – Umwandlung von einem Typ mit kleinem Wertebereich in einen mit größerem Wertebereich
  • Surjektive Funktion – Umwandlung von einem Typ mit großem Wertebereich in einen mit kleinerem Wertebereich
  • Bijektive Funktion – eindeutige Eins-zu-eins-Zuordnung
• Ein- und Ausgabe der Logik lassen sich als Typen ausdrücken
  • Das bedeutet, dass sich Logik über Typen abstrahieren lässt
  • Ein- und Ausgabe lassen sich als Typen darstellen, und darauf aufbauend kann man Logik entwerfen
• Man kann grundlegenden Datentypen Namen geben und sie so als unterschiedliche Typen behandeln
• Mit einem Typsystem lassen sich verschiedene Probleme lösen
  • Verallgemeinerung mit Generics
  • Bereichseinschränkung mit Phantom-Typen
  • Einschränkung von Verhalten mit Union-Typen (oder Summentypen)
  • TODO-Behandlung mit dem minimalen Typ
  • Implementierung endlicher Zustandsautomaten mit Typen
  • Validierung mit abhängigen Typen
• Type-Driven Development ist eine Methodik, bei der zuerst die Typen definiert und darauf basierend der Code geschrieben wird
• Type-Driven Development kann grundsätzlich überall angewendet werden und beginnt damit, die Ergebnisse jedes Schritts als Typen zu definieren
• Bei der Anforderungsanalyse sollte man versuchen, die Anforderungen als Typen zu abstrahieren
• Auch wenn der zugrunde liegende Datentyp gleich ist, ist es sinnvoll, bei unterschiedlicher Bedeutung verschiedene Typen zu definieren
• Wenn man die Anforderungen analysiert und über die Typen nachgedacht hat, sollte man versuchen, die Logik als Typen zu abstrahieren
  • Eine Abstraktion im Stil von (String) -> List<Token> ist möglich
• Type-Driven Development passt gut zu Test-Driven Development
  • Beide Ansätze ähneln sich darin, dass Eingaben und Ausgaben vorab definiert und erst danach der Code geschrieben wird
  • Während Type-Driven Development mit dem Typsystem bereits zur Compile-Zeit Stabilität prüfen kann, kann Test-Driven Development Fehler oder Ausnahmesituationen abfangen, die sich allein mit Typen nicht erfassen lassen
• Aus Sicht des Entwurfs bedeutet die Nutzung eines Typsystems, Regeln für den Code anderer Entwickler zu schaffen
• Werden jedoch zu viele Typen einzeln definiert oder werden Typdefinitionen zu komplex, kann das das Schreiben von Code erschweren oder die Lesbarkeit verschlechtern; deshalb ist es wichtig, stets ein angemessenes Gleichgewicht zu halten

[chabulhwi]

Eine injektive Funktion liegt vor, wenn bei der Menge der transformierten Werte Kodomäne und Bildmenge nicht übereinstimmen. Etwas einfacher ausgedrückt bedeutet das eine Umwandlung von einem Typ mit kleinerem Wertebereich in einen Typ mit größerem Wertebereich.

Eine injektive Funktion ist eine Funktion, bei der die Bilder zweier beliebiger verschiedener Variablen ebenfalls verschieden sind. Das heißt: Für alle Elemente a und b aus der Definitionsmenge X einer injektiven Funktion f gilt: Wenn a ≠ b, dann f(a) ≠ f(b). Was in der koreanischen Oberstufenmathematik als „eineindeutige Funktion“ bezeichnet wird, ist eine injektive Funktion.

[kciter1]

Vielen Dank für die ausführliche Erklärung. :) Ich hatte es falsch verstanden. Darauf wurde ich ohnehin schon ein paar Mal hingewiesen, daher werde ich mich noch etwas intensiver damit beschäftigen und den Inhalt dann neu ordnen.