Typ-System, Typ-Arithmetik

05/03/2014 - 17:23 von Heiner Kücker | Report spam
In diesem Blog-Post meckert der Autor über die
vielen kryptischen Symbole in Scala:

http://java.dzone.com/articles/i-dont-scala

Auch ich finde Scala recht schwer zu lesen.

Ein anderer Anlass war diese Forums-Frage

http://www.java-forum.org/scala-gro...-code.html

Bei der Antwort geht nicht klar hervor,
dass die Auflösung des Succ-Types zur
Compile- und nicht zur Lauf-Zeit erfolgt.

Die ganze Typ-Arithmetik ist eine ziemliche
Geheimwissenschaft.

Deshalb habe ich mal überlegt, wie ich mir eine
solche Sprache wünschen würde.

Soweit ich das mit der Typ-Arithmetik verstanden
habe, geht es darum, Ausdrücke, die prinzipiell
auch zur Laufzeit ausgewertet werden könnten
(Assertions, Design by Contract) zur Compile-Zeit
auszuwerten.

Leider ist die Sprache der Typ-Arithmetik nicht
die gleiche oder mindestens àhnliche Sprache,
wie die Laufzeit-Sprache.
Ist dadurch verstàndlich, dass ja der Compiler
diese Sprache auswertet, zur Laufzeit ist
sie im wesentlichen weg.

Dadurch sind irgendwelche (für den Laufzeit-/Normal-
Programmier) kryptischen Zeichen erforderlich.

Mir geht es darum, dass Typ-Arithmetik
nicht kompliziert sein müsste, nur die
Notation müsste für den Normal-Programmierer
verstàndlicher sein.

Grundlage meiner Alternativ-Idee ist, dass der
Compiler bestimmten Code in einer bestimmten
Compiler-Phase ausführt.
Dieser Code wird in der Wirts-Sprache geschrieben,
làuft aber natürlich gegen das Compiler-API ,
nicht gegen die Laufzeit-Umgebung,
wobei andererseits Teile der Standard-Bibliothek,
wie die Collections, zur Verfügung stehen sollen.

Dies sollte fester Bestandteil der Sprache sein,
nicht irgendein Plugin-/Tool-Kram.

Klar, dass auch Debugging möglich sein sollte.

Bei einer Variable oder Member muss die Entscheidung
über Schreib- und Lese-Berechtigung bezüglich
des Clients oder des zuzuweisenden Wertes getroffen
werden.

Bei einer Methode sind getrennt Entscheidungen
über die Berechtigung zum Aufruf oder zum
Implementieren/Überschreiben bezüglich
des Clients oder des/der Parameter oder des
Status des Objektes zu treffen.

Mangels eigener Ideen übernehme ich die
Annotations-Schreibweise, diese scheinen
auch ein geeignetes Mittel zum Erweitern
einer Sprache ohne die Notwendigkeit
des Schreibens eines Parsers/Lexers usw
zu sein
(siehe XTend-Active-Annotations oder
Java-Annotations-Prozessoren).

Natürlich sind die Möglichkeiten von
Annotationen insofern begrenzt, dass
man sich in nur den Strukturen der
Wirts-Sprache bewegen kann.

Der Compiler arbeitet sich in der
Ausführungsphase der Typ-Sprache
am Datenfluss im AST entlang,
insofern muss die Sprache und
die Arbeitsweise des Compilers
in dieser Phase zusammenpassen.

Hier mal ein einfaches Beispiel
mit Array-Index.

Grundlage ist die Verwendung eines
int-Wertes als Array-Index, welcher
potentiell unterspezifiziert ist,
weil negative Werte möglich sind.


... irgendwelcher Code in irgendeiner Methode ...

final int x = ...; // unbekannter int-Wert

if ( x < 0 ) {
... Fehlerbehandlung ...
{
else {
// flow-sensitive typing würde diese
// zusàtzliche Variable obsolet machen
@Requires( { arrayIndex >= 0 } )
final int nonNegativeInt = x;

Object value = get( nonNegativeInt );
}

...
}

/** get-Methode */
Object get(
@Requires( { arrayIndex >= 0 } )
final int arrayIndex ) {
return this.arr[ arrayIndex ];
}

In der Requires-Annotation wird verlangt
(und damit auf der anderen Seite zugesichert)
dass der int-Wert nicht negativ ist.
Der Code in der Annotation ist einfach so
aufgebaut, dass der Wert des letzten Ausdrucks
zurückgegeben wird.
Man könnte aber auch ein return verlangen,
damit es mehr wie Java aussieht.

Hier ein weiteres Beispiel mit einem
File-Objekt, welches zum Schreiben
erst mal geöffnet werden muss:


@State( { State state = CLOSED; } )
class File {

@StateTransition( { state = OPEN; } )
void open() {
...
}

@RequiresState( { state == OPEN; } )
void write(...) {
...
}

@StateTransition( { state = CLOSED; } )
void open() {
...
}


Diese File-Klasse verwenden wir jetzt:

final File file = new File(...);

if ( ...condition... ) {
file.open();
// ok
file.write(...);
}
else {
// Compiler-Fehler
file.write(...);
}

Schön wàre jetzt noch, wenn der Compiler
ein Ereignis hàtte, welches das Verschwinden
des File-Objektes aus dem Scope anzeigen
würde.


@State( { State state = CLOSED; } )
@RequiresAbandonState( { state == CLOSED; } )
class File {
...


Jetzt könnte der Compiler meckern,
wenn das File-Objekt nicht ordentlich
geschlossen wird.
Über das Ablegen in einem ThreadLocal,
einer globalen Variable oder einem
verànderlichem Parameter-Objekt
müsste ich noch mal extra nachdenken.


Nun machen wir unser erstes Beispiel noch
etwas komplizierter:

final int x = ...; // unbekannter int-Wert

if ( x >= 1 ) {
...

if ( x < 0 ) {
... dieser Zweig kann nie erreicht werden ...
{
else {
@Requires( { arrayIndex >= 0 } )
final int nonNegativeInt = x;

Object value = get( nonNegativeInt );
}
}
...
}

Weil unser Wert bereits geprüft wurde,
ist die Prüfung im zweiten if eigentlich
nicht notwendig.

Damit der Compiler feststellen kann,
dass dies nicht notwendig ist,
muss er etwas über Grösser-Als, Kleiner-Als,
Grösser-Gleich, Kleiner-Gleich und eventuell
Ungleich wissen.

Das ist eigentlich nicht seine Angelegenheit.

Ich habe den Verdacht, dass die Scala-Beispiele
mit Peano-Zahlen (siehe oben Succ) ganz einfach
darauf beruhen, dass man einfaches Abzàhlen
auf rekursives Typ-Auflösen abbilden kann.
Den Compiler wie ein Kleinkind zàhlen zu
lassen ist eventuell nicht die günstigste
Lösung.

Ich würde benannte Pràdikate einführen, welche
letztendlich Klassen sind, die wàhrend des
Compiler-Prüf-Laufes verwendet werden.

class PredicateIntGreaterEqual0 {
boolean test( int value ) {
return value >= 0;
}
}

class PredicateIntGreaterEqual1 {
boolean test( int value ) {
return value >= 1;
}

boolean isCompatibleTo( Predicate other ) {
if ( other instanceof PredicateIntGreaterEqual0 ) {
return true;
}
return false;
}
...
}

Diese Pràdikate verwenden wir jetzt:

final int x = ...; // unbekannter int-Wert

if ( PredicateIntGreaterEqual1.test( x ) ) {
...

if ( ! PredicateIntGreaterEqual0.test( x ) ) {
... dieser Zweig kann nie erreicht werden ...
//der Compiler kann dies durch die Methode
//PredicateIntGreaterEqual1#isCompatibleTo
//erkennen
{
else {
@Requires( { arrayIndex >= 0 } )
final int nonNegativeInt = x;

Object value = get( nonNegativeInt );
}
}
...
}

Wichtig an den Pràdikaten ist die Wirkung
zur Laufzeit (Methode test) und ausserdem
die Wirkung im Compiler.

Aufwàndig ist jetzt, dass für jeden int-Wert
eine solche Pràdikat-Klasse existieren müsste.

In meinem Constraint-Code-Generator gibt es
zwar parametrisierbare Pràdikate, aber die
formulierten Constraints müssen alle als
eigene Klasse generiert werden, schade.

Dort kommt es zur kombinatorischen Explosion.
Aber das ist aufgrund der Generierung von
Klassen zum Einspannen des Java-Compilers
zur Analyse, nicht zu vermeiden.



Natürlich müsste es auch die Möglichkeit
der Bausteinbildung geben.

So wàre der final-Modifier an einer Variable
oder Member eine Abkürzung für

CanWrite( { false } )


Eine weitere Anwendungsmöglichkeit wàre
die Steuerung des Scope.
Javas public, protected, private und default
Modifier reichen nicht aus um Komponenten
(OSGI) zu definieren oder um Tests spezielle
Scopes (testen von private-Methoden, mocken
von final-Methoden).

Klar dass das Compiler-API nicht von Anfang
an perfekt sein kann, sicher wird einiges
zu Beginn fehlen, wie Kontravarianz, Verlassen
des Scope usw.

Das Checker-Framework ist im Gegensatz zu
meiner Idee auch nur ein Schalter-System
wie das Java-Typ-System und hat nicht die
Ausdruckskraft von Expressions.

Was meint ihr zu meiner, zugegeben aufgrund
des Fehlens einer echten Implementierung
etwas theoretischen Idee?
 

Lesen sie die antworten

#1 Patrick Roemer
05/03/2014 - 22:42 | Warnen spam
Responding to Heiner Kücker:

Deinen Vorschlag und Deine Beispiele muesste ich mir irgendwann noch mal
in Ruhe anschauen, um was dazu zu sagen - ich bin auf jeden Fall
skeptisch. ;) Ich beziehe mich hier nur auf den Aspekt der Typ-Arithmetik.

In diesem Blog-Post meckert der Autor über die
vielen kryptischen Symbole in Scala:



In diesem Usenet-Posting meckert der Autor zum wiederholten Male ueber
den Unwillen seines Vorposters, hinreichend Kontext in seinen Postings
unterzubringen: Die relevanten Zeilen aus den folgenden Links haette man
durchaus hierhin kopieren koennen. :(

http://java.dzone.com/articles/i-dont-scala



Mir gefaellt '"x" -> 2' dann doch besser als "new Map.Entry<String,
Integer>("x", 2)'. Auf jeden Fall hat das herzlich wenig mit dem
Typsystem zu tun.

http://www.java-forum.org/scala-gro...-code.html

Bei der Antwort geht nicht klar hervor,
dass die Auflösung des Succ-Types zur
Compile- und nicht zur Lauf-Zeit erfolgt.



Wenn es aus der Antwort hervorginge, waere es wohl Unfug. Nur anhand der
Zeile

def +(that: Nat) = new Succ(n + that)

wuerde ich sagen, dass man das in Java genauso machen koennte:

interface Nat {
Nat plus(Nat that);
Nat ZERO new Nat() {
public Nat plus(Nat that) { return that; }
};
}

class Succ implements Nat {
private final Nat n;
public Succ(Nat n) { this.n = n; }
public Nat plus(Nat that) { return new Succ(n.plus(that)); }
}

...und das hat nix mit Aufloesung zur Compilezeit (und wieder nix mit
dem Typsystem) zu tun.

(Ja, man *kann* die Peanozahlen in Scala per Typ-Arithmetik codieren -
aber damit hat obige Codezeile sicher nichts zu tun, dafuer braucht es
schon parametrisierte Typen.)

Soweit ich das mit der Typ-Arithmetik verstanden
habe, geht es darum, Ausdrücke, die prinzipiell
auch zur Laufzeit ausgewertet werden könnten
(Assertions, Design by Contract) zur Compile-Zeit
auszuwerten.



Ich wuesste keine "offizielle" Definition fuer den Begriff, aber wenn
man mal danach googlet, findet man z.B. "type arithmetic are
calculations on the type-level" oder "computation based on the theory of
types". IOW: Das Typsystem nutzen, um gewisse Berechnungen zur
Compilezeit durchzufuehren. Das ist etwas deutlich anderes.

Leider ist die Sprache der Typ-Arithmetik nicht
die gleiche oder mindestens àhnliche Sprache,
wie die Laufzeit-Sprache.
Ist dadurch verstàndlich, dass ja der Compiler
diese Sprache auswertet, zur Laufzeit ist
sie im wesentlichen weg.

Dadurch sind irgendwelche (für den Laufzeit-/Normal-
Programmier) kryptischen Zeichen erforderlich.



...und damit wackelt der Rest der Argumentation etwas: Typ-Arithmetik
basiert ausschliesslich auf der Laufzeit-Sprache, und kryptische Zeichen
sind dafuer auch nicht erforderlich. (Ok, type lambdas halte ich
subjektiv fuer etwas kryptisch, aber das liegt nicht an kryptischen
Zeichen.)

Grundlage meiner Alternativ-Idee ist, dass der
Compiler bestimmten Code in einer bestimmten
Compiler-Phase ausführt.
Dieser Code wird in der Wirts-Sprache geschrieben,
làuft aber natürlich gegen das Compiler-API ,
nicht gegen die Laufzeit-Umgebung,
wobei andererseits Teile der Standard-Bibliothek,
wie die Collections, zur Verfügung stehen sollen.



Das waeren eher Macros, nicht Typ-Arithmetik.

Ich habe den Verdacht, dass die Scala-Beispiele
mit Peano-Zahlen (siehe oben Succ) ganz einfach
darauf beruhen, dass man einfaches Abzàhlen
auf rekursives Typ-Auflösen abbilden kann.



AFAICS nicht "siehe oben", aber: im Prinzip schon.

Den Compiler wie ein Kleinkind zàhlen zu
lassen ist eventuell nicht die günstigste
Lösung.



Aber es ist das, was er mit dem Typsystem schon von Natur aus kann. :)

Viele Gruesse,
Patrick

Ähnliche fragen