[Ciseve-devel] mocl: type inference

[Matthias L. <Mat...@gm...>]

Hallo!

Zum Type-Inference-Problem bei OCL. Es geht um z.B. folgendes Konstrukt:

    package Foundation_Core

    context BehavioralFeature def:
    let testdef : Integer = if (testdef < 10) then
        testdef - 1 else testdef endif

    endpackage

Das funktioniert soweit von der Typanalyse her. Es ist nur nicht möglich die
Typ-Angabe hinter dem 1. testdef wegzulassen, da momentan ein Verfahren
fehlt, den Typ auszurechnen.

Analog zu dem Typkalkül was in Programmiersprachen und -systeme gelehrt
wird, würde ich folgende Überlegungen für einen Algorithmus ansetzen:

Man definiert zunächst Typgleichungen für alle Sprachkonstrukte, die in
einer Expression vorkommen können.

- Die Anwendung eines Identifiers hat den Typ des für ihn in der Umgebung
eingetragenen Typs. Also für Ide: t0 gilt t0 = t falls Ide.name(): t in Env.

- Eine Funktionsapplikation F(A) hat folgende Repräsentation: apply(F: t1,
A: t2): t0. Und die Typgleichung ist: t1 = (t2 -> t0). Bei Funktionsaufrufen
mit mehr als einen Parameter geschieht das ganze analog: apply(F: t1, A: t2,
B: t3): t0. Hier ist die Typgleichung t1 = (t2 ** t3 -> t0).

- Bei der Fallunterscheidung if B then T else E endif ist die
Baumdarstellung: cond(B: t1, T: t2, E: t3): t0. Hier gelten zwei
Gleichungen:
t1 = boolean
t0 = t2 = t3

- Let-Konstrukte muss man glaube ich nicht betrachten, da diese nicht
schachtelbar sind (so sah es zumindest laut Grammatik aus).

Nun kann man für das konkrete OCL-Constraint viele Gleichungen aufstellen,
die aufgrund dieser Regeln recht einfach zu erstellen sind. Wichtig ist
hierbei, dass für gleiche Funktionsapplikationen oder gleiche Identifier
unterschiedliche Typvariablen verwendet werden. Also das testdef bei
(testdef < 10) erhält z.B. t4 und das testdef bei (testdef - 1) bekommt t8
als Typvariable.

Diese Gleichungen kann man per Unifikation lösen. Voraussetzung hierfür ist,
dass keine Gleichungen der Form t1 = (t1 -> t2) auftauchen (Occurs check).
Dies passiert aber bei dem Beispiel vom Anfang nicht. Eine weitere Bedingung
ist, dass die Funktionen wie Addition oder Relationen wohl definiert sind.
Also dass bekannt ist, welche Typen erwartet werden. Bei OCL gibt es da eine
kleine Schwierigkeit, da Integer ein Subtyp von Real ist, und man an manchen
Stellen nicht entscheiden kann, welches von beiden es ist. Hier sollte man
es wahrscheinlich offen lassen und beides einfach akzeptieren und im Notfall
Konversion durchführen.

Bei dem Beispiel von oben wäre Integer auch austauschbar durch Real -
eindeutig kann das nicht bestimmt werden. Falls es aber von einer anderen
Funktion aufgerufen wird, die einen bestimmten Typ erwartet, kann es ja
konvertiert werden.

Nun zur Unifikation: Diese ist nicht sonderlich schwer - in PSS haben wir
dafür ein Beispiel-Programm in OPAL, was aber auch recht einfach in Java
umsetzbar wäre:
http://uebb.cs.tu-berlin.de/lehre/2004WVpss/files/unification.tar.gz

Dabei wird eine Liste von einfachen Gleichungen (keine Multigleichungen)
verarbeitet. In den Gleichungen können Typvariablen, Funktionen und Sorten
vorkommen. Sorten sind in dem Fall schon konkrete Typen wie Boolean,
Integer. Und nun muss man die Fälle die jeweils links und rechts auf einer
Seite vorkommen können betrachten. Zum Beispiel wenn man die Gleichung
(t1 -> t2) = (t3 -> t4) hat, muss man daraus zwei neue machen:
t1 = t3 und t2 = t4. Oder trifft man auf eine Gleichung Integer = Boolean
muss man einen Fehler liefern.

Ich denke, dass der Ansatz recht effizient ist und zumindest in der
Überlegung nicht allzu schwierig wirkt. Diese vereinfachte Variante des
Lambda-Kalküls bzw. des ML-Typinferenzsystems eignet sich gut für
funktionale bzw. formelle Sprachen und OCL gehört ja auch dazu.

Gruß,
Matthias Liebig