Typprüfung für System Fw mit CASE und PAIR

Markus Bleicher

Dieses Fortgeschrittenenpraktikum war der Versuch, einen Typprüfungsalgorithmus für den auf Typkonstruktoren von höchstens Rang 3 beschränkten polymorphen l-Kalkül System Fw zu entwerfen und zu implementieren, der zur Verifikation von in Beweisen vorkommenden Typisierungen dienen soll.
Der dargestellte Algorithmus geht kanonisch aus dem syntaxgeleiteten Kalkül hervor. Es wird ein mit Typen annotierter Termbaum aufgebaut und in einen Ableitungsbaum des syntaxgeleiteten Kalküls überführt.
Die Implementierung beschränkt sich auf die Verifikation von Churchtermen.

Contents

"Rank 2 types break all the standard typing algorithms. We can only do type checking by making rather draconian restrictions." 1

1  Das Problem

fasst obiges Zitat gut zusammenfassen.
Die Fragestellung dieser Arbeit entwickelte sich aus der Verifikation von Beweistermen für ,,Monotoniezeugen" in einer Erweiterung von System Fw ([,,]). Für bestimmte Typen sollen Terme gefunden oder verifiziert werden, die von diesen Typen getypt werden.
Da die Typgewinnung nicht nur in System Fw sondern bereits in System F unentscheidbar ist, ausserdem Urzyczyn2 mutmaßt, alle in System Fw typisierbaren Terme seien bereits in System Fw(1) typisierbar und Typprüfung entgegen dem Anschein keinesfalls leichter als Typgewinnung ist, ist ein weites Feld für unfruchtbare Basteleien geöffnet.
Daher betrachte ich auch die entscheidbare Verifikation des Typens von Church-Termen oder die (in System Fw unentscheidbare, in System Fw(3) entscheidbare) Typprüfung für vollständig getypte (annotierte) Curry-Terme.

2  Typen und Typsysteme

(Einordnung von System Fw. Für das Thema und Verständnis der Arbeit nebensächlich.)
Typen kann man als Prädikate für die Terme des ungetypten l-Kalküls auffassen.
Es gibt heute eine Vielzahl verschiedener Typsysteme, die man zuerst einmal in zwei Klassen einteilen kann: Systeme, bei denen die Typen in den Termen enthalten sind (,,endogen", ,,explizit", ,,a la Church"), die Herleitungsregeln für syntaktisch korrekte Terme also bereits auf Typen Bezug nehmen. Und Systeme, bei denen die Typen nachträglich den Termen zugewiesen werden (,,exogen", ,,implizit", ,,a la Curry") (nach []).
In [] werden die Typsysteme, die in [] an Hand der drei Kriterien Vorhandensein von Polymorphie, abhängigen Typen und Typen höherer Ordnung klassifiziert, auf einem Würfel angeordnet .

Picture Omitted
Figure 1: Barendegts Würfel mit endogen getypten l-Kalkülen
Zwischen den beiden Würfeln für explizite und implizite

Picture Omitted
Figure 2: Barendegts Würfel mit exogenen Typsystemen
Typsysteme, gibt es - wie in [] gezeigt - eine Isomorphie für die eine Hälfte ohne abhängige Typen mit Hilfe einer Typlöschungs- und einer Typgewinnungsfunktion. Für die andere Hälfte mit abhängigen Typen existiert natürlicherweise nur eine Injektion.
Es folgen nun noch Teile der Definition eines umfassenden Typsystems aus [], S. 90, in seiner endogenen Darstellung.

2.1  Sprache

Seien Var die Menge der Konstruktorvariablen (mit A, B als Mitteilungszeichen), var die Menge der Termvariablen (mit x,y als Mitteilungszeichen) zwei disjunkte Variablenmengen. Getypte Terme (bezeichnet durch m, n, r, s, t), Typ-Konstruktoren (bezeichnet durch kleine griechische Buchstaben) und Kinds (bezeichnet durch K, K') sind durch folgende Grammatik definiert:
m
:: =
x|lx:f.m|mm|lA:K.m|mf
f
:: =
A|Px:f.f|lx:f.f|PA:K.f|lA:K.f|ff|fm
K
:: =
*|Px:f.K|PA:K.K
Die b-Reduktion ist definiert als der reflexive und transitive Abschluss der Relation (lv:P.Q)R® bQ[v:=R], .
Die b-Gleichheit =b ist die durch b-Reduzierbarkeit und syntaktische Gleichheit unter a-Konversion bestimmte Kongruenzrelation.

2.2  Das General Type System Kalkül

Darstellung der Kalküle von Barendregt mit Hilfe des General Type System \vdash t im Church style:

2.2.1  Regeln für Kinds


 

\vdash t*:#
(AX)

 G,x:r\vdash tK:#

G\vdash tPx:r.K:#
(KPFC)

 G,x:K\vdash tK¢:#

G\vdash tPx:K.K¢:#
(KPFK)

2.2.2  Regeln für Konstruktoren


 G\vdash tK:#

G,a:K\vdash ta:K
a Ï dom(G)(CVAR)

G\vdash tr:K
G\vdash tK¢:#
K=bK¢

G\vdash tr:K¢
(C=b)

 G,x:r\vdash ty:*

G\vdash tPx:r.y:*
(CPFC)

 G,a:K\vdash ty:*

G\vdash tPa:K.y:*
(CPFK)

 G,x:r\vdash ty:K

G\vdash tlx:r.y:Px:r.K
(CPIC)

G\vdash ts:Px:y.K
G\vdash tM:y

G\vdash tsM:K[x:=M]
(CPEC)

 G,a:K\vdash ty:K¢

G\vdash tla:K.y:Pa:K.K¢
(CPIK)

G\vdash ts:Pa:K.K¢
G\vdash ty:K

G\vdash tsy:K¢[a:=y]
(CPEK)

2.2.3  Regeln für Terme


 G\vdash s:*

G,x:s\vdash x:s
x Ï dom(G)(VAR)

G\vdash tM:r
G\vdash ty:*
r = by

G\vdash tM:y
(=b)

 G,x:r\vdash tM:y

G\vdash tlx:r.M:Px:r.y
(PIC)

G\vdash tM:Px:f.y
G\vdash tN:f

G\vdash tMN:y[x:=N]
(PEC)

 G,a:K\vdash tM:y

G\vdash tla:K.M:Pa:K.y
(PIK)

G\vdash tM:Pa:K.s
G\vdash ty:K

G\vdash tMy:s[a:=y]
(PEK)

2.2.4  Und die Abschwächungsregel


G\vdash tP:Q
G\vdash tR:s

G,u:R\vdash tP:Q
u Ï dom(G)(WEAK)
K ist ein wohlgeformter Kind in G, falls G\vdash tK:#. f ist ein wohlgeformter Konstruktor in G vom Kind K, falls G\vdash tf:K. Schliesslich ist M ein wohlgeformter Term vom Typ f in G, falls G\vdash tM:f.

2.3  Kalküle

Name des Kalküls
l® einfach getypter Lamda-Kalkül
l2Sytem F
lw
lwSytem Fw
lP
lP2
lPw
lCCalculus of Constructions

Chapter 1
System Fw und Erweiterungen

1  System Fw

Das System Fw ist der Lambda-Kalkül, dessen Typsystem Konstruktorvariablen beliebiger Ordnung enthält. Er ist das stärkste System ohne abhängige Typen. Da abhängige Typen die Menge der typbaren Terme nicht erhöhen ([], S.99), ist es auch mit das stärkste Typsystem auf Barendregts Würfel. Ich verwende den Begriff System Fw unabhängig davon, ob ein endogenes (das eigentliche System Fw) Typsystem oder seine exogene Modifikation gemeint ist.

1.1  Sprache und Notation

Um den Kalkül in der üblichen Notation zu schreiben, identifiziert man Px:r.y mit r® y (da x in y nicht vorkommt) und Pa:K.y mit "a:K.y.
Das Kindsystem - also das Typsystem der Typen von System Fw - hat die Struktur eines einfach getypten Lambda-Kalküls. Dabei werden die Konstruktoren von Kinds der Form
K::=*|(KÞ K)
getypt. Damit haben die Konstruktoren entweder die Form
fKÞ K¢::=AKÞ K¢|lAK.fK¢|(fK"Þ KÞ K¢fK")
oder, falls sie von Kind * und damit Typen für die Terme von System Fw sind, sind sie von der Gestalt
f*::=A*|(f*® f*)|"aK.y*|(fK1Þ K2Þ ¼Þ KnÞ *fK1Þ K2Þ ¼Þ Kn)
Terme sind
t::=x|lxt|(tt)
Zur Klammerersparnis seien die Applikation links-, die Pfeile rechtsassoziativ.
Die Substitution t[x:=s] ersetzt alle freien Vorkommnisse von x in t durch s. Dabei werden gebundene Variablen in t so umbenannt (a-Konversion), dass keine freien Variablen aus s in den Bindungsbereich eines Variablenbinders kommen, also ,,gefangen" werden.
Die parallele Substitution t[x1:=s1,¼,xn:=sn] ersetzt gleichzeitig alle Vorkommnisse von x1 bis xn. Mit
®
x
 
=x1,¼,xn

und
®
s
 
=s1,¼,sn

schreibe ich dafür auch
t[ ®
x
 
:= ®
s
 
]

. Genauso gilt:
" ®
x
 
t="x1¼"xnt

und
l ®
x
 
t=lx1¼lxnt

. Die Vektoren können auch leer sein, die Definitonen meinen dann jeweils t.
Analoge Definition der Substitution und von Vektoren für Typen.
Die b-Reduktion der Typen ist stark normalisierend, da Typen mit Kinds einen einfach getypten Lambdakalkül bilden. b-gleiche Typkonstruktoren werden identifiziert.

1.2  Der Kalkül von System Fw

G ist eine Variablenumgebung, also eine endliche Menge von getypten Termvariablen, wobei die Schreibweise G(x) den Typ der Variablen x zurückgibt und das Komma eine getypte Variable einfügt.

 

G\vdash x:G(x)
(VAR)

G\vdash r:r® s
G\vdash s:r

G\vdash rs:s
(APP)

 G,x:r\vdash t:s

G\vdash lxt:r® s
(ABS)

 G\vdash t:"Xs

G\vdash t:s[X:=r]
(INST)

 G\vdash t:s

G\vdash t:"Xs
if X not free in G(GEN)
Das System besitzt die subject reduction Eigenschaft, wenn also s zu einem s¢ reduziert und G\vdash s:s gilt, dann gilt auch G\vdash s¢:s.

1.3  Terme für Fw im Church style


 

G,x:s\vdash x:s
(VAR)

G\vdash r:r® s
G\vdash s:r

G\vdash rs:s
(APP)

 G,x:r\vdash t:s

G\vdash lx:r.t:r® s
(ABS)

 G\vdash t:"Xs

G\vdash tr:s[X:=r]
(INST)

 G\vdash t:s

G\vdash L Xt:"Xs
if X not free in G(GEN)

1.4  Syntaxgeleitete Version des Kalküls

Aus []. Wenn man die Generalisierungen mit der davor liegenden Abstraktion, Applikation oder VAR-Anwendung zusammenzieht, Spezialisierungen immer mit der vorhergegangenen Applikation oder VAR-Anwendung ausführt, benötigt man nur noch 3 Regeln.
Definition der Matching-Relation £ : Für zwei Typen f und y gilt f £ y (y ist eine allquantifizierte Spezialisierung von f) genau dann, wenn
f = " ®
A
 
.f¢

und
y = " ®
B
 
.f¢[ ®
A
 
:= ®
c
 
]

, wobei die
®
B
 

nicht frei in
f = " ®
A
 
.f¢

vorkommen dürfen (Henglein andersrum).

 G(x) £ a

G\vdash x:a
(VAR¢)

G\vdash r:r® s
G\vdash s:r
s £ a

G\vdash rs:" ®
X
 
.a
®
X
 
not free in G(APP¢)

 G,x:r\vdash t:s

G\vdash lxt:" ®
X
 
.r® s
®
X
 
not free in G(ABS¢)
Der resultierende Kalkül ist syntaxgeleitet.

1.5  Äquivalenzbeweis

Die Äquivalenz der syntaxgeleiteten Version mit der ursprünglichen Variante wird in [] auf Seite 104, Theorem 2.3.4 bewiesen.

1.6  Notation: Rang und Fw(n)

Der Rang o eines Kinds ist induktiv definiert: o(*)=0,
o(k1Þ k2)= max
(o(k1)+1,o(k1))

. Da jeder Kind in der Form k1Þ k2Þ ¼Þ knÞ * geschrieben werden kann, kann das für diese Darstellung auch äquivalent als o(*)=0,
o(k1Þ k2Þ ¼Þ knÞ *)=
max
i Î {1,¼,n} 
o(ki)+1

geschrieben werden.
Der Rang eines Types ist der höchste Rang eines in ihm vorkommenden Subtypes (nur Lambdaabstraktionen können höheren Rang haben als die in ihnen vorkommenden Konstruktoren).
Der Rang eines Terms ist der höchste Rang eines in ihm vorkommenden Types.
Wie [] schreibe ich Fw(n) für ein auf Terme vom Rang £ n beschränktes System Fw.
(Hinweis: In einigen Artikeln (z.B. [,,,]) werden die Begriffe anders definiert, der Rang von o(*)=1 etc.)
Der Rang von ((*Þ *)Þ *)Þ *ist also 3. lA*Þ *.T* hat den Rang 2.

2  System Fw mit CASE und PAIR3

2.1  Curry Style


 

G\vdash x:G(x)
(VAR)

G\vdash r:r® s
G\vdash s:r

G\vdash rs:s
(APP)

 G,x:r\vdash t:s

G\vdash lxt:r® s
(ABS)

G\vdash r:s
G\vdash s:r

G\vdash á r,s ñ :s×r
(PAIR)

 G\vdash t:s×r

G\vdash tL:s
(PL)

 G\vdash t:s×r

G\vdash tR:r
(PR)

G\vdash t:s+r
G,x:s\vdash r:g
G,y:r\vdash s:g

G\vdash t(x.r,y.s):g
(CASE)

 G\vdash t:r

G\vdash INRt:s+r
(INR)

 G\vdash t:s

G\vdash INLt:s+r
(INL)

 G\vdash t:"Xs

G\vdash t:s[X:=r]
(INST)

 G\vdash t:s

G\vdash t:"Xs
if X not free in G(GEN)
Das Kalkül ist also ein um die Regeln PAIR, PL,PR, CASE, INL, INR erweitertes System Fw, in dem sich Konjunktionen und Disjunktionen durch diese syntaktischen Konstrukte direkt darstellen lassen.

2.2  syntaxgeleitete Version

Sie entsteht wieder durch Entfernen der Regeln INST und GEN und Erweitern der übrigen Regeln, so dass diese auch Ableitungen mit Typen, die zu den ursprünglichen in der Matching-Relation stehen, umfassen.

 G(x) £ a

G\vdash x:a
(VAR¢)

G\vdash r:r® s
G\vdash s:r
s £ a

G\vdash rs:" ®
X
 
.a
®
X
 
not free in G(APP¢)

 G,x:r\vdash t:s

G\vdash lxt:" ®
X
 
.r® s
®
X
 
not free in G(ABS¢)

G\vdash r:s
G\vdash s:r

G\vdash á r,s ñ :" ®
X
 
.s×r
®
X
 
not free in G(PAIR¢)

G\vdash t:s×r
s £ a

G\vdash tL:" ®
X
 
.a
®
X
 
not free in G(PL¢)

G\vdash t:s×r
r £ a

G\vdash tR:" ®
X
 
.a
®
X
 
not free in G(PR¢)

G\vdash t:s+r
G,x:s¢\vdash r:g
s £ s¢
g £ a
G,y:r¢\vdash s:d
r £ r¢
d £ a

G\vdash t(x.r,y.s):" ®
X
 
.a
®
X
 
not free in G(CASE¢)

 G\vdash t:r

G\vdash INRt:" ®
X
 
.s+r
®
X
 
not free in G(INR¢)

 G\vdash t:s

G\vdash INLt:" ®
X
 
.s+r
®
X
 
not free in G(INL¢)

2.3  Äquivalenzbeweis

Die Äquivalenz der syntaxgeleiteten Version mit der ursprünglichen Variante lässt sich wahrscheinlich analog wie für System Fw beweisen. Zumindest die Korrektheit, dass also jede im syntaxgeleiteten Kalkül erfolgte Ableitung eine entsprechende im Original besitzt, ist offensichtlich, da man nur für jede Regel das entsprechende Original verwenden muss und die spezielleren, semiunifizierten Typen durch Anwendung von INST und GEN an Hand der Substitution einfach nachbauen.

2.4  Church Style

Für INST und GEN verwendet man wieder die Church Notation und erhält einen entscheidbaren Kalkül.

 

G\vdash x:G(x)
(VAR)

G\vdash r:r® s
G\vdash s:r

G\vdash rs:s
(APP)

 G,x:r\vdash t:s

G\vdash lxt:r® s
(ABS)

G\vdash r:s
G\vdash s:r

G\vdash á r,s ñ :s×r
(PAIR)

 G\vdash t:s×r

G\vdash tL:s
(PL)

 G\vdash t:s×r

G\vdash tR:r
(PR)

G\vdash t:s+r
G,x:s\vdash r:g
G,y:r\vdash s:g

G\vdash t(x.r,y.s):g
(CASE)

 G\vdash t:r

G\vdash INRt:s+r
(INR)

 G\vdash t:s

G\vdash INLt:s+r
(INL)

 G\vdash t:"Xs

G\vdash tr:s[X:=r]
(INST)

 G\vdash t:s

G\vdash L Xt:"Xs
if X not free in G(GEN)

3  syntaxgeleitete Kalküle

Ein Kalkül ist syntaxgeleitet, wenn sich aus dem Aufbau eines Terms eindeutig die verwendete Regel zu seiner Herleitung im Kalkül ergibt. Das führt (beweisbar durch strukturelle Induktion) dazu, dass der Ableitungsbaum für seine Typkorrektheit strukturgleich dem Termbaum ist.
Für die syntaxgeleitete Variante von Fw gilt nun auch wie für jeden syntaxgeleiteten Kalkül, dass sich aus dem Wurzelknoten des Termbaum zwingend die Herleitungsregel ergibt, was im originalen System Fw nicht gilt, da man an jeder Stelle Typvariablengeneralisierungen und -instanziierungen verwenden kann.
Diese Eigenschaft ist natürlich für die Typprüfung und -gewinnung günstig, da man nur die korrekte Anwendung einer Regel prüfen muss. Um sie für das System Fw, das sie wegen der Regeln INST und GEN, die nur den Typ und nicht den Term modifizieren, nicht besitzt, zu erhalten, entfernt man entweder diese Regeln (durch Integration in die restlichen, verwendet in [], 1.4, 2.2) oder ersetzt sie durch termmodifizierende (wie im Church-Kalkül 1.3, 2.4).
Der Church-Kalkül ist prinzipiell syntaxgeleitet, bei dem der Kalkül für die korrekten Terme identisch ist mit dem Kalkül für die typkorrekten. Das wird erreicht durch die syntaktischen Konstrukte für Typvariablengeneralisierungen und -instanziierungen.

4  annotierte Syntaxbäume

Das übliche Verfahren zur Typgewinnung und -prüfung ist die Verwendung eines mit dem Typ des jeweiligen Subterms annotierten Termbaums, für den man bei einem syntaxgeleiteten Kalkül entweder zur Typprüfung die korrekte Anwendung der jeweiligen Ableitungsregel überprüft oder zur Typgewinnung leere Knoten mit neuen Variablen beschriftet und die aus dem Typisierungskalkül sich ergebenden Constraints zu lösen versucht.

5  Algorithmen und Semi-Algorithmen zur Typprüfung

Aus den oben dargestellten syntaxgeleiteten Kalkülen (also entweder Church-Kalküle oder die syntaxgeleiteten Varianten der Curry-Kalküle) ergeben sich kanonisch Algorithmen zur Typprüfung von Termen, die diesen Typsystemen entsprechen sollen. Man betrachtet die Wurzel eines Termbaums, erhält daraus die einzig mögliche Herleitungsregel und prüft deren korrekte Anwendung, was für Church-Kalküle der Überprüfung der b-Gleichheit unter einer bekannten Substitution, korrekter Generalisierung, b-Gleichheit von Teiltypen (was alles auch praktisch entscheidbar ist) entspricht, für Curry-Kalküle dem Matchingproblem (der für unterschiedliche Ordnungen von Konstruktoren unentscheidbar oder entscheidbar) ist.

6  Der Semiunifikations-Algorithmus

6.1  Matching, Semiunifikation, Unifikation

Gegeben sei eine Menge von Gleichungen E={Mil=Mir|i Î J} und Mengen von Ungleichungen In={Nil £ Nir|i Î Kn}. Eine Substitution s, für die es Quotientsubstitutionen rn gibt mit den Eigenschaften "i Î J.s(Mil)=s(Mir) und "n."i Î Kn.rn(s(Nil))=s(Nir) ist ein (nicht-uniformer) Semiunifikator. Sind die rn alle gleich, ist s ein uniformer Semiunifikator, falls sie alle gleich der Identität sind, ist s ein Unifikator. Ist s die Identität, dann sind die rn Matcher.
Ein Problemstellung kann immer durch eine einzige Gleichung ausgedrückt werden, so dass die Menge der Unifikatoren des ursprünglichen Problems identisch ist mit der der Gleichung. Ähnlich für uniforme Semiunifikatoren, bei denen immer Probleme auf eine Gleichung und eine Ungleichung reduziert werden können ([], S.18).

6.2  Der Unifikations-Algorithmus von Huet

Huet hat in [] einen Algorithmus zur Semiunifikation von einfach getypten Lambda-Termen vorgestellt.
Angepasst an die Verwendung von Allquantifikation im Term und den speziellen (binären und einzigen) Konstanten ® ,×,+wird dieser Algorithmus hier zur Semiunifikation von Typen verwendet. Dazu entfernt man die äusseren Allquantoren, ,,befreit" also deren gebundene Variablen und behandelt innere Allquantoren genauso wie Funktionssymbole, nur dass sie a-konvertierbar sind ("X.s durch "FoolX.s ersetzen oder direkt behandeln).
Man reduziert wie oben angesprochen ein Seminunifikationsproblem auf eine zu unifizierende Gleichung und löst diese dann mit diesem Algorithmus.

6.3  Matching-Algorithmus

Der in [] - auf Baumautomaten beruhende - Algorithmus für das Matchingproblem bis zur Ordnung 3 entscheidet das Problem, das hier bei der Verifikation von voll annotierten Termbäumen auftaucht, wenn über die korrekte Anwendung einer Regel eines syntaxgeleiteten Curry-Kalküls entschieden werden soll.

7  Ein Algorithmus zur Typgewinnung

Der Algorithmus geht in folgenden Schritten vor: Die Teile des Termbaums ohne Typinformation werden mit frischen Typvariablen annotiert. Dann stellt man mit Hilfe des syntaxgeleiteten Kalküls eine Menge von Gleichungen und Ungleichungen auf, die man mit dem Huet-Algorithmus löst. Der daraus entstehende Termbaum lässt sich für Ordnungen £ 3 unter zuhilfenahme des Matching-Algorthmus als korrekt annotiert verifizieren.
Bei dieser ,,naiven" Vorgehensweise tritt allerdings auch das in [], S.33 beschriebene Problem auf, zu dessen Behebung die dort verwendete Methode der Variablenfixierung eingesetzt wird.

8  Hierarchie der betrachteten Probleme

Die Typprüfung in Church-Termen ist entscheidbar und algorithmisch einfach. Die Typprüfung von voll annotierten Curry-Termen ist bis zu einer gewissen Ordnung entscheidbar, allerdings sind die notwendigen Matching-Algorithmen nicht trivial. Typgewinnung für System Fw ist unentscheidbar, aber reduzierbar auf Unifikation und damit den relativ luziden Algorithmus von Huet.

9  Typsysteme von Programmiersprachen

9.1  bidirektionale Typprüfung

Der bidirektionale Typprüfungsalgorithmus in [] ist eine modifizierte und für intersection types spezialisierte Variante, die für Fw über das generelle Prinzip der Verschränkung von Typgewinnung und Typprüfung hinaus keine für mich erkennbare Einsichten bietet. Wie oben bereits dargestellt, ist auch die Korrektheit der Typisierung eines vollständig annotierten Termbaumes unentscheidbar, weswegen eine partielle Verwendung von Instantiierungen a la Church vermutlich das bessere Verfahren darstellt.

9.2  entscheidbare Typsysteme

Typsysteme, für die Implementierungen zur Typprüfung von funktionalen Programmiersprachen wie Standard ML oder Haskell existieren oder die zu diesem Zweck entworfen wurden, stellt Henglein in seiner Doktorarbeit [] vor. Dazu zählen der Curry-Hindley, Damas-Milner, Milner-Mycroft und der Flat Milner-Mycroft Kalkül.
Relevant sind diese Systeme und Implementierungen für meine Fragestellung nicht, da die Zielsetzungen zu unterschiedlich sind, d.h. wegen der Notwendigkeit von terminierenden Algorithmen werden nur viel schwächere Typsysteme als Fw untersucht.

9.3  Ponder

Es fehlt leider auch ,,Ponder"4, vermutlich die erste (und einzige?) Sprache mit einem Typsystem so mächtig wie Fw, über die ich nichts weiter recherchieren konnte.

Chapter 2
Die Implementierung

erfolgte in Haskell und ist beschränkt auf einen Typchecker für den Church-Kalkül für Fw mit CASE und PAIR. Im übrigen kann ich mich auf den Artikel [] berufen, der behauptet auf die ,,esoterischeren" Sprachkonstrukte in Haskell zu verzichten und nur Monads in allen Varianten zu verwenden.

1  Datentypen und Abstraktion

Verwendet werden ein Datentyp Exp für partiell annotierte Termbäume, Type für partiell annotierte Typbäume, Kind für Kindbäume.
Die offensichtliche Abstraktion der Verwendung einer gemeinsamen Struktur für die (durch Typen) getypten Terme und (durch Kinds) getypten Typen findet in der class Lambda ihren Ausdruck. Dabei zeigen sich allerdings eine Reihe von Problemen, da Haskell weder classes mit mehreren Parametern zulässt, noch Instanzdeklarationen mit Typsynonymen oder Typapplikationen.
Durch die überladenen Funktionen destr und constr werden die Baumdatentypen in durch Listen immitierte B äume verwandelt und umgekehrt, wobei noch eventuelle Variablenbindungen vermerkt werden.

2  Der Parser

ist mit dem Parsergenerator happy für Haskell erstellt und benutzt einen handgeschriebenen Lexer. Die Grammatik orientiert sich grundsätzlich an der üblichen Notation für getypte Lambdaterme mit ,,:" als dem Junktor zwischen Termen und Typen, ,," als l-Symbol wie in Haskell, und dem Kaufmannsund ,,&" als ". Variablen dürfen länger als ein Zeichen sein und bestehen aus Buchstaben, nach dem ersten Zeichen auch aus Ziffern. Sie werden durch Zeichen, die keine Buchstaben oder Ziffern sind, voneinander getrennt. Großgeschriebene Variablen sind Termvariablen, kleingeschriebene Typvariablen.
Ein Unterschied zur gewöhnlichen Notation ist, dass der Punkt ,,." ein syntaktisches Element ist, das in jeder Variablenbindung vorkommt. Er hat den üblichen Effekt, die Bindung so weit nach rechts wie möglich auszudehnen.
Der Parser soll zusammen mit der show Funktion eine Isomorphie zwischen den als Daten und den als Strings repäsentierten Lambdatermen erzeugen, wobei überflüssige Klammern und whitespace ausser Betracht bleiben.

3  Der Pretty-Printer

kommt in mehreren Varianten vor. Zum einen als show-Funktion, die die abstrakten Syntaxbäume wieder in (parsebare) Strings übersetzt (und damit ,,die" Repräsentation eines Terms ist). Daneben gibt es noch explicit, die den Term vollständig klammert und alle Klammerersparnisregeln ignoriert. latex übersetzt die Terme in LATEX-Ausdrücke.

4  Hilfsfunktionen

b-Reduktion, freie Variablen, gebundene Variablen, a-Konversion,

5  Der Algorithmus zur vollständigen Annotation

Die Funktion annotateFull ergänzt die Typen eines jeden Teilterms, der noch keine Typisierung besitzt und überprüft die bereits annotierten.

6  Der Typprüfer

Die Funktion checkChurch prüft einen voll annotierten Baum auf Korrektheit der Annotation. Dabei werden zuerst rekursiv die Teilterme geprüft und dann an Hand der Regel, die dem Operator der Wurzel zugeordnet ist, eben diese. Aus den Regeln (siehe 2.4) ergeben sich dann die Programmkonstrukte

7  Beispiele

Das ganze System ist getestet sowohl mit als auch mit . Da keine systemspezifische Erweiterungen verwendet wurden, sollte es mit allem arbeiten, was Haskell 98 versteht. Die Beispiele sind theoretisch banal und dienen zum Verständnis des Systems und der Fehlerbeseitigung.
Die Tabellen stellen eine Auflistung aller Teilterme eines zu prüfenden Terms dar, wobei dann kontrolliert wird, ob der annotierte Typ sich korrekt aus denen der inneren Terme ergibt (Das ist mit der Gleichheitsrelation jetzt auch nur interessant, um Fehler im Programm zu finden, bei komplizierteren Relationen gilt das nicht mehr).

7.1  Kombinatoren

Die Beispiele bestehen aus den Kombinatoren S (=lx.ly.lz.xz(yz)) und K (=lx.ly.x) aus dem Kombinatorenkalkül,
Die Betareduktion funktioniert zumindest bei der Identität I=bSKK

7.2  Church-Ziffern

ein paar Church-Ziffern (die Church-Ziffer n hat die Form:
lx.lf.fnx=lx.lf.
f¼f
x

) als grosse Terme
und aus den von Urzyczyn verwendeten Zweierketten (22¼2K) der Länge n bei denen ein Ausdruck aus n-mal der Church-Ziffer 2 auf K angewendet, was an die Ackermann-Funktion erinnert (urzy n=(church 2)n K).

7.3  Verschiedenes

7.3.1  Zurückweisung einer Übergeneralisierung

Falsches als Falsches erkannt

7.3.2  Getypte Kombinatoren S K

Ein halber SKK ... als Beispiel für einen großen Term mit Typen

7.3.3  Typ von Urzyczyns 22K

Beweis der Typisierbarkeit von 22K, eine etwas anspruchsvollere Ableitung

7.3.4  Einfache Paarbildung

Beweist nichts ...

7.4  Montoniezeugen

Auch einfache Exemplare von Matthes' Monotoniezeugen (aus []) lassen sich verifizieren
Die Identität ist isoton, Punkt 1.3 in []
Das Produkt ist isoton
Die Summe ist isoton
Konstanten sind isoton, Punkt 1.2 in []

Chapter 3
Anhang

1  Die Programme

1.1  Die Datentypen mit show

-- these are datatypes for system F_omega typed lambda expressions with CASE
-- and PAIR rules. All a la Church with Maybe type assignments
-- they can also be used to represent Curry terms
-- $Id: CPFwDatatypes.hs,v 1.12 2002/05/01 18:29:35 markus Exp $

module CPFwDatatypes where

import List(notElem, intersect)
import Maybe(fromJust, isJust)

infix ::: 
infix ::^

-- Exp, Type and Kind extraction
-- smells like a class, but Exp has to be a "real" type, so i don't know how
-- to create one

tm :: Exp->UntypedExp
tm (e ::: _) = e

ty :: Exp->Maybe Type
ty (_ ::: t) = t
jty = fromJust . ty

con :: Type->UnkindedType
con (t ::^ _) = t

kd :: Type->Maybe Kind
kd (_ ::^ k) = k
jkd = fromJust . kd

-- conditional show
cs b br = if b then br else ""

data OpStyle = Base | LeftAss | RightAss | Non | Post | Pre deriving Eq

data Binary = Function | Prod | Sum deriving Eq
instance Show Binary where
  show Function = "->"
  show Prod = "%"
  show Sum = "+"
instance Read Binary where
  readsPrec _ ('-':'>':r) = [(Function, r)]
  readsPrec _ ('%':r) = [(Prod, r)]
  readsPrec _ ('+':r) = [(Sum, r)]
  readsPrec _ _ = []

data LR = L | R deriving (Show, Read, Eq) 

class Show_ a where
  show_ :: Bool -> a -> String

class Prec a where
  prec :: a -> (Int, OpStyle)

-- precProb(T) (not a class because of Haskell limitations)
-- if the precedence of the outer (upper in a parse tree) is higher or equal
-- as the inner and the operator style makes it possible, brackets are
-- neccesary to avoid "stealing"

data UntypedExp
      = Abs Exp Exp
      | Inst Exp Type
      | Gen Type Exp
      | App Exp Exp
      | Var String
      | Case Exp Exp Exp Exp Exp
      | InLR LR Exp
      | Pair Exp Exp
      | Lr LR Exp
     deriving Eq
instance Show UntypedExp where
  show = show_ True -- first arg says whether term is in front of a closing
                    -- bracket to bracket \ . correctly 

instance Prec UntypedExp where
  prec (Abs _ _) = (1000, Pre)
  prec (Gen _ _) = (1000, Pre)
  prec (InLR _ _) = (500, Pre)
  prec (App _ _) = (100, LeftAss)
  prec (Inst _ _) = (100, Post)
  prec (Case _ _ _ _ _) = (700, Post)
  prec (Lr _ _) = (200, Post)
  prec (Var _) = (0, Base)
  prec (Pair _ _) = (0, Base)

precProb ops out (inn ::: t) =
     (fst (prec out) < fst (prec inn)
       && (snd (prec inn) `notElem` (ops `intersect` [Post, Pre])))
  || (fst (prec out) == fst (prec inn) 
       && (snd (prec inn) `notElem` ops)
  || isJust t)

instance Show_ UntypedExp where
  -- dot structures (prefix), lowest prec so no testing neccesary 
  show_ b (Abs v t) =
    let p = precProb [Pre] (Abs v t) t in
    cs (not b) "("++"\\"++show_ False v++"."++
    cs p "("++show_ True t++cs p ")"++cs (not b) ")"
  show_ b (Gen v t) =
    let p = precProb [Pre] (Gen v t) t in
    cs (not b) "("++"/\\"++show_ False v++"."++
    cs p "("++show_ True t++cs p ")"++cs (not b) ")"

  -- prefix
  show_ _ (InLR c e) | precProb [Pre] (InLR c e) e =
    "IN"++show c++" ("++show_ True e++")"
  show_ b (InLR c e) = "IN"++show c++" "++show_ b e

  -- apps
  show_ b (App t1 t2) =
    let lp = precProb [Post, LeftAss] (App t1 t2) t1
        rp = precProb [Pre] (App t1 t2) t2 in
    cs lp "("++show_ lp t1++cs lp ")"++" "++
    cs rp "("++show_ (rp||b) t2++cs rp ")"
  show_ b (Inst t (ty ::^ k)) =
    let lp = precProb [Post, LeftAss] (Inst t (ty ::^ k)) t
        rp = case prec ty of (_, Base) -> False 
                             _ -> True in
    cs lp "("++show_ (lp||b) t++cs lp ")"++" "++
    cs rp "("++show_ (rp||b) (ty ::^ k)++cs rp ")"

  -- postfix
  show_ _ (Case inlr vl tl vr tr) = 
    let p = precProb [Post, LeftAss] (Case inlr vl tl vr tr) inlr in
    cs p "("++ show_ p inlr++cs p ")"++
    "{"++show vl++"."++show_ True tl++", "++
    show vr++"."++show_ True tr++"}"
  show_ b (Lr c e) =
    let p = precProb [Post, LeftAss] (Lr c e) e in
    cs p "("++show_ (b||p) e++cs p ")"++" "++show c

  -- simple cases
  show_ _ (Var v) = v
  show_ _ (Pair t1 t2) = "<"++show_ True t1++", "++show_ True t2++">"

  -- ERROR
  show_ _ _ = "UntypedExp show_: no rule applies."

data UnkindedType
      = TypeVar String
      | TypeBinary Binary Type Type
      | TypeLambda Type Type
      | TypeApp Type Type
      | Forall Type Type
     deriving Eq
instance Show UnkindedType where
  show = show_ True -- first arg says whether term is in front of a closing
                    -- bracket to bracket \ . correctly

instance Prec UnkindedType where
  prec (TypeLambda _ _) = (1000, Pre)
  prec (Forall _ _) = (1000, Pre)
  prec (TypeBinary Function _ _) = (700, RightAss)
  prec (TypeBinary Sum _ _) = (600, LeftAss)
  prec (TypeBinary Prod _ _) = (500, LeftAss)
  prec (TypeApp _ _) = (100, LeftAss)
  prec (TypeVar _) = (0, Base)

precProbT ops out (inn ::^ t) =
     (fst (prec out) < fst (prec inn)
       && (snd (prec inn) `notElem` (ops `intersect` [Post, Pre])))
  || (fst (prec out) == fst (prec inn) 
       && (snd (prec inn) `notElem` ops))

instance Show_ UnkindedType where
  show_ _ (TypeVar tv) = tv

  -- brackets if necessary
  show_ b (TypeLambda tv t) =
    cs (not b) "("++"\\"++show_ False tv++"."++show_ True t++cs (not b) ")"
  show_ b (Forall tv t) =
    cs (not b) "("++"&"++show_ False tv++"."++show_ True t++cs (not b) ")" 

  -- binary infix operators + % ->
  show_ b (TypeBinary op t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeBinary op t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeBinary op t1 t2) t2 in
    cs lp "("++show_ lp t1++cs lp ")"++show op++
    cs rp "("++show_ (rp||b) t2++cs rp ")"

  -- apps
  show_ b (TypeApp t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeApp t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeApp t1 t2) t2 in
    cs lp "("++show_ lp t1++cs lp ")"++" "++
    cs rp "("++show_ (rp||b) t2++cs rp ")"

  -- base types
  show_ _ (TypeVar v) = v

  -- ERROR
  show_ _ _ = error "UnkindedType show_: no rule applies."

data Kind
      = KindProp
      | KindAbs Kind Kind
     deriving Eq
instance Show Kind where
  show KindProp = "*"
  show (KindAbs (KindAbs k11 k12) k2) =
         "("++show (KindAbs k11 k12)++")=>"++show k2
  show (KindAbs k1 k2) = show k1++"=>"++show k2

data Type = UnkindedType ::^ Maybe Kind deriving Eq

instance Show Type where
  show = show_ True
instance Show_ Type where
  show_ b (utype ::^ Nothing) = show_ b utype
  show_ b (utype ::^ Just kind) =
    let br = case prec utype of (_, Base) -> False
                                _ -> True in
    cs br "("++show_ (br||b) utype++cs br ")"++"^"++show kind

data Exp = UntypedExp ::: Maybe Type deriving Eq

instance Show Exp where
  show = show_ True
instance Show_ Exp where
  show_ b (uexp ::: Nothing) = show_ b uexp
  show_ b (uexp ::: Just (t ::^ k)) =
    show_ b uexp++":"++show_ b (t ::^ k)
 

1.2  Der Parser

-- this is a "happy" parser for system F_omega typed lambda
-- expressions with CASE and PAIR rules. All a la Church with
-- Maybe type assignments they can also be used to represent
-- Curry terms
-- $Id: ParseCPFw.y,v 1.12 2002/05/01 18:29:36 markus Exp $

{
module ParseCPFw where
import Char(isAlpha, isAlphaNum, isSpace, isUpper, isLower)
import CPFwDatatypes(Exp(..), Type(..), Kind(..),
                     UntypedExp(..), UnkindedType(..), Binary(..))

}

%name parser Exp
%tokentype { Token }

%token '\\'  { TokenAbs }
       '.'  { TokenDot }
       var  { TokenVar $$ }
       tvar { TokenTypVar $$ }
       ':'  { TokenColon }
       '&'  { TokenForall }
       '/\\' { TokenAlpha }
       '^'  { TokenUp }
       '+' { TokenPlus }
       '%' { TokenTimes }
       '->' { TokenArrow }
       'LR' { TokenLR $$ }
       'INLR' { TokenINLR $$ }
       '*'  { TokenStar }
       '=>' { TokenDoubleArrow }
       '('  { TokenOB }
       ')'  { TokenCB }
       '{'  { TokenCOB }
       '}'  { TokenCCB }
       ','  { TokenComma }
       '<'  { TokenROB }
       '>'  { TokenRCB }

-- precedence: earlier means lower

%nonassoc ':' -- type applicator

-- IN(L|R)
-- \ . lambda
-- /\ . Alpha

-- { } case
-- left: LR, church app, curry app

-- base:
-- Var
-- < , > pair
-- ( ) brackets

%left '%' -- % case type
%left '+' -- + pair type
%right '->' -- type abstractor

%right '=>' -- kind abstractor

%nonassoc '^' -- kind applicator

%monad { P } { thenP } { returnP }
%lexer { monadiclexer } { TokenEOF }

%%

-- EXP RULES

SimpleExp :: { Exp }
        : var { Var $1 ::: Nothing }
        | '<' Exp ',' Exp '>' { Pair $2 $4 ::: Nothing }
        | '(' Exp ')' { $2 }

-- left assoc. and postfix operators
AppExp :: { Exp }
        : SimpleExp { $1 }
        | AppExp SimpleExp { App $1 $2 ::: Nothing }
        | AppExp SimpleType { Inst $1 $2 ::: Nothing }
	| AppExp 'LR' { Lr (read $2) $1 ::: Nothing }
        | AppExp '{' Exp '.' Exp ',' Exp '.' Exp '}'
          {% case ($3, $7) of
             (Var v1 ::: t1, Var v2 ::: t2) ->
               returnP (Case $1 (Var v1 ::: t1) $5 (Var v2 ::: t2) $9
                          ::: Nothing)
             (v1, v2) ->
               failP ("CASE, where "++show v1++" or "++show v2++
                      " are no variables.") 
          }             

-- expression with unbracketed prefix operators
NoBrakExp :: { Exp }
	: AppExp { $1 }
	| AppExp PreExp { App $1 $2 ::: Nothing }
	| PreExp { $1 }

-- prefix operators
PreExp :: { Exp }
	: 'INLR' NoBrakExp  { InLR (read $1) $2 ::: Nothing }
        | '\\' Exp '.' NoBrakExp
          {% case $2 of { Var v ::: t -> returnP (Abs (Var v ::: t)
                                                      $4
                                                    ::: Nothing)
                        ; e -> failP ("Abstraction of "++show e++
                                      "which is no variable.")
                        }
          }
        | '/\\' Type '.' NoBrakExp
          {% case $2 of { TypeVar v ::^ k -> returnP (Gen (TypeVar v ::^ k)
                                                          $4
                                                       ::: Nothing)
                        ; e -> failP ("GEN of "++show e++
                                      "which is no type variable.")
                        }
          }

Exp :: { Exp }
	: NoBrakExp { $1 }
	| Exp ':' Type {% case $1 of
                            uexp ::: Nothing -> returnP (uexp ::: Just $3)
                            _ -> failP "Double typing is not allowed" }


-- TYPE RULES

TypeVar :: { Type }
	: tvar { TypeVar $1 ::^ Nothing }
	| tvar '^' Kind { TypeVar $1 ::^ Just $3 } 

SimpleType :: { Type }
	: TypeVar { $1 }
	| '(' Type ')' { $2 }
	| '(' Type ')' '^' Kind
            {% case $2 of
                 utype ::^ Nothing -> returnP (utype ::^ Just $5)
                 _ -> failP "Double kinding is not allowed" }

AppType :: { Type }
	: AppType SimpleType { TypeApp $1 $2 ::^ Nothing }
	| SimpleType { $1 }

BinType :: { Type }
--	: AppType { $1 }
	: AppType '+' PreType { TypeBinary Sum $1 $3 ::^ Nothing }
	| AppType '%' PreType { TypeBinary Prod $1 $3 ::^ Nothing }
	| AppType '->' PreType { TypeBinary Function $1 $3 ::^ Nothing }

	| BinType '+' PreType { TypeBinary Sum $1 $3 ::^ Nothing }
	| BinType '%' PreType { TypeBinary Prod $1 $3 ::^ Nothing }
	| BinType '->' PreType { TypeBinary Function $1 $3 ::^ Nothing }

	| AppType '+' BinType { TypeBinary Sum $1 $3 ::^ Nothing }
	| AppType '%' BinType { TypeBinary Prod $1 $3 ::^ Nothing }
	| AppType '->' BinType { TypeBinary Function $1 $3 ::^ Nothing }

	| BinType '+' BinType { TypeBinary Sum $1 $3 ::^ Nothing }
	| BinType '%' BinType { TypeBinary Prod $1 $3 ::^ Nothing }
	| BinType '->' BinType { TypeBinary Function $1 $3 ::^ Nothing }

	| AppType '+' AppType { TypeBinary Sum $1 $3 ::^ Nothing }
	| AppType '%' AppType { TypeBinary Prod $1 $3 ::^ Nothing }
	| AppType '->' AppType { TypeBinary Function $1 $3 ::^ Nothing }

	| BinType '+' AppType { TypeBinary Sum $1 $3 ::^ Nothing }
	| BinType '%' AppType { TypeBinary Prod $1 $3 ::^ Nothing }
	| BinType '->' AppType { TypeBinary Function $1 $3 ::^ Nothing }

-- types with unbracketed prefix operators
Type :: { Type }
	: PreType { $1 }
	| BinType { $1 }
	| AppType { $1 }
	| AppType PreType { TypeApp $1 $2 ::^ Nothing }

-- prefix operators
PreType :: { Type }
--	: AppType { $1 }
--	| BinType { $1 }
        : '\\' TypeVar '.' PreType { TypeLambda $2 $4 ::^ Nothing }
        | '&' TypeVar '.' PreType { Forall $2 $4 ::^ Nothing }
        | '\\' TypeVar '.' BinType { TypeLambda $2 $4 ::^ Nothing }
        | '&' TypeVar '.' BinType { Forall $2 $4 ::^ Nothing }
        | '\\' TypeVar '.' AppType { TypeLambda $2 $4 ::^ Nothing }
        | '&' TypeVar '.' AppType { Forall $2 $4 ::^ Nothing }

-- KIND RULES

Kind :: { Kind }
	: '*' { KindProp }
	| Kind '=>' Kind { KindAbs $1 $3 }
	| '(' Kind ')' { $2 }

{
data Token
       = TokenAbs
       | TokenAlpha
       | TokenDot
       | TokenVar String
       | TokenTypVar String
       | TokenForall
       | TokenColon
       | TokenUp
       | TokenDoubleArrow
       | TokenStar
       | TokenOB
       | TokenCB
       | TokenPlus
       | TokenTimes
       | TokenArrow
       | TokenCOB
       | TokenCCB
       | TokenComma
       | TokenROB
       | TokenRCB
       | TokenLR String
       | TokenINLR String
       | TokenEOF
       | TokenFail
  deriving (Show, Eq)

-- a type to locate errors

type LineNumber = (Int, Int)
addLineNumber :: LineNumber->LineNumber->LineNumber
addLineNumber (x1,y1) (x2,y2) = (x1+x2, y1+y2)

-- the monad around the lexer to process errors

data ParseResult a = Ok a | Failed (String, LineNumber)

-- parse error handling

happyError :: P a
happyError = failP "Parse Error"

-- failP adds the line number, so i don't need this 
-- getLineNumber :: P LineNumber
-- getLineNumber = \s l -> Ok l

-- the monadic lexer

type P a = String -> LineNumber -> ParseResult a
-- hand-made Monad P, since using a "real" Monad needs a real type, needs a
-- real constructor, creates really ugly functions with lots of meaningless
-- case constructs to eliminate these constructors

returnP :: a -> P a
returnP a = \s l -> Ok a

failP :: String -> P a
failP err = \ _ (x,y) -> Failed (err++" at line "++show y
                                 ++", column "++show x++".", (x,y))

thenP :: P a -> (a -> P b) -> P b
a `thenP` b = \s l -> case a s l of Ok r -> b r s l
                                    Failed err -> Failed err

monadiclexer :: (Token -> P a) -> P a
monadiclexer cont = 
  \s l -> let (token, rest, pos)=lexer s l
          in if (token==TokenFail) then failP "Lexer error" rest pos
                                   else cont token rest pos

-- the real lexer

lexer :: String -> LineNumber -> (Token, String, LineNumber)
lexer [] (x,y) = (TokenEOF, "", (x,y))
lexer (c:cs) (x,y)
      | isSpace c =
          let (t,s, (xp,yp))=lexer cs (x,y)
           in (t,s, (if c=='\n' then (1,yp+1) else (xp+1,yp)))
      | isAlpha c = 
          let (var, rest)=lexLetter (c:cs)
           in (var, rest, (length (c:cs)-length rest+x,y))
lexer ('\\':cs) (x,y) = (TokenAbs, cs, (x+1,y))
lexer ('/':'\\':cs) (x,y) = (TokenAlpha, cs, (x+2,y))
lexer ('.':cs) (x,y) = (TokenDot, cs, (x+1,y))
lexer (':':cs) (x,y) = (TokenColon, cs, (x+1,y))
lexer ('^':cs) (x,y) = (TokenUp, cs, (x+1,y))

lexer ('=':'>':cs) (x,y) = (TokenDoubleArrow, cs, (x+2,y))
lexer ('*':cs) (x,y) = (TokenStar, cs, (x+1,y))
lexer ('&':cs) (x,y) = (TokenForall, cs, (x+1,y))
lexer ('(':cs) (x,y) = (TokenOB, cs, (x+1,y))
lexer (')':cs) (x,y) = (TokenCB, cs, (x+1,y))

lexer ('+':cs) (x,y) = (TokenPlus, cs, (x+1,y))
lexer ('%':cs) (x,y) = (TokenTimes, cs, (x+1,y))
lexer ('-':'>':cs) (x,y) = (TokenArrow, cs, (x+2,y))
lexer ('{':cs) (x,y) = (TokenCOB, cs, (x+1,y))
lexer ('}':cs) (x,y) = (TokenCCB, cs, (x+1,y))
lexer (',':cs) (x,y) = (TokenComma, cs, (x+1,y))
lexer ('<':cs) (x,y) = (TokenROB, cs, (x+1,y))
lexer ('>':cs) (x,y) = (TokenRCB, cs, (x+1,y))


-- no rule applies
lexer s c = (TokenFail, s, c)

lexLetter cs =
  let (var, rest) = span isAlphaNum cs
      token = case var of
        "L" -> TokenLR "L"
        "R" -> TokenLR "R"
        "INL" -> TokenINLR "L"
        "INR" -> TokenINLR "R"

        v:_ | isUpper v -> TokenTypVar var
        v:_ | isLower v -> TokenVar var
  in (token, rest)

-- general functions

parserMonadic :: String -> ParseResult Exp
parserMonadic = \s -> parser s (1,1)

parserShortError :: String -> Exp
parserShortError s = case parser s (1,1) of Ok r -> r
                                            Failed (s,l) -> error s

marklocation s (x,y) =
  let ls=lines s
  in unlines (take y ls++[replicate (x-1) ' '++"^"]++drop y ls)

parserLongError :: String -> Exp
parserLongError s =
  case parser s (1,1) of
    Ok r -> r
    Failed (e,p) -> error (e++"\n"++marklocation s p)
parseCPFw = parserLongError
parse = parserLongError

}


1.3  Pretty-Printer

-- funtions to pretty print lambda terms with types as LaTeX source
-- $Id: PrintExplicit.hs,v 1.5 2002/05/01 18:29:36 markus Exp $

module PrintExplicit where
import ParseTypedLambdaExpressions(Exp(..), Type(..), Kind(..),
                                   UntypedExp(..), UnkindedType(..))

attribute separator string Nothing = string
attribute separator string (Just t) = "("++string++separator++show t++")"

class Explicit a where
  explicit :: a -> String

instance Explicit Exp where
  explicit (Abs v t ::: ty) =
    attribute ":" ("(\\"++explicit v++"."++explicit t++")") ty
  explicit (App t1 t2 ::: ty) =
    attribute ":" ("("++explicit t1++" "++explicit t2++")") ty
  explicit (Var v ::: ty) =
    attribute ":" v ty 

instance Explicit Kind where
  explicit KindProp = "*"
  explicit (KindAbs k1 k2) = "("++explicit k1++"=>"++explicit k2++")"

instance Explicit Type where
  explicit (TypeAbs t1 t2 ::^ k) =
    attribute "^" ("("++explicit t1++"->"++explicit t2++")") k
  explicit (TypeApp t1 t2 ::^ k) =
    attribute "^"  ("("++explicit t1++" "++explicit t2++")") k
  explicit (Forall (TypeVar tv ::^ ktv) t ::^ k) =
    attribute "^" ("(&"++explicit (TypeVar tv ::^ ktv)++"."++explicit t++")") k
  explicit (TypeVar tv ::^ k) =
    attribute "^" tv k

-- funtions to pretty print lambda terms with types as LaTeX source
-- $Id: PrintLaTeX.hs,v 1.8 2002/05/08 02:32:09 markus Exp $

module PrintLaTeX where
import CPFwDatatypes(Exp(..), Type(..), UntypedExp(..), UnkindedType(..),
                     Kind(..),
                     Binary (..),
                     Prec(..), precProb, precProbT, OpStyle(..),
                     cs)

import Char(isAlphaNum)

latexVar v =
  let s=fst $ span isAlphaNum v in if s==v then s else s++"..."
--  let cs=drop 1 (show v) in "\\textrm{ "++take (length cs-1) cs++" }"

class LaTeX a where
  latex :: a -> String
  latex = latex_ True
  latex_ :: Bool -> a -> String

instance LaTeX UntypedExp where
  -- dot structures (prefix), lowest prec so no testing neccesary
  latex_ b (Abs v t) =
    let p = precProb [Pre] (Abs v t) t in
    cs (not b) "("++"\\lambda "++latex_ False v++"."++
    cs p "("++latex_ True t++cs p ")"++cs (not b) ")"
  latex_ b (Gen v t) =
    let p = precProb [Pre] (Gen v t) t in
    cs (not b) "("++"\\Lambda "++latex_ False v++"."++
    cs p "("++latex_ True t++cs p ")"++cs (not b) ")"

  -- prefix
  latex_ _ (InLR c e) | precProb [Pre] (InLR c e) e =
    "IN"++show c++" ("++latex_ True e++")"
  latex_ b (InLR c e) = "IN"++show c++" "++latex_ b e

  -- apps
  latex_ b (App t1 t2) =
    let lp = precProb [Post, LeftAss] (App t1 t2) t1
        rp = precProb [Pre] (App t1 t2) t2 in
    cs lp "("++latex_ lp t1++cs lp ")"++" "++
    cs rp "("++latex_ (rp||b) t2++cs rp ")"
  latex_ b (Inst t (ty ::^ k)) =
    let lp = precProb [Post, LeftAss] (Inst t (ty ::^ k)) t
        rp = case prec ty of (_, Base) -> False
                             _ -> True in
    cs lp "("++latex_ (lp||b) t++cs lp ")"++" "++
    cs rp "("++latex_ (rp||b) (ty ::^ k)++cs rp ")"

  -- postfix
  latex_ _ (Case inlr vl tl vr tr) =
    let p = precProb [Post, LeftAss] (Case inlr vl tl vr tr) inlr in
    cs p "("++ latex_ p inlr++cs p ")"++
    "( "++show vl++" . "++latex_ True tl++" , "++
    show vr++" . "++latex_ True tr++" )"
{- latex is unable to typeset bracketed expressions reasonable
    cs p "("++ latex_ p inlr++cs p ")"++
    "\\left( "++show vl++". \\right. "++latex_ True tl++", "++
    show vr++" . \\left. "++latex_ True tr++" \\right)"
-}
  latex_ b (Lr c e) =
    let p = precProb [Post, LeftAss] (Lr c e) e in
    cs p "("++latex_ (b||p) e++cs p ")"++" "++show c

  -- simple cases
  latex_ _ (Var v) = latexVar v
  latex_ _ (Pair t1 t2) = " < "++latex_ True t1++", "++
                          latex_ True t2++" > "
{- latex is unable to typeset bracketed expressions reasonable
  latex_ _ (Pair t1 t2) = " \\left< "++latex_ True t1++", \\right. \\left. "++
                          latex_ True t2++" \\right> "
-}

  -- ERROR
  latex_ _ _ = "UntypedExp latex_: no rule applies."

instance LaTeX Exp where
  latex_ b (e ::: Nothing) = latex_ b e
  latex_ b (e ::: Just t) = latex_ b e++":"++latex_ b t

instance LaTeX Kind where
  latex_ _ KindProp = "*"
  latex_ _ (KindAbs (KindAbs k11 k12) k2) = 
    "("++latex (KindAbs k11 k12)++") \\Rightarrow "++latex k2
  latex_ _ (KindAbs k1 k2) = latex k1++" \\Rightarrow "++latex k2

instance LaTeX Binary where
  latex_ _ Sum = " + "
  latex_ _ Prod = " \\times "
  latex_ _ Function = " \\rightarrow "

instance LaTeX UnkindedType where
  latex_ _ (TypeVar tv) = latexVar tv

  -- brackets if necessary
  latex_ b (TypeLambda tv t) =
    cs (not b) "("++" \\lambda "++latex_ False tv++"."++latex_ True t++cs (not b) ")"
  latex_ b (Forall tv t) =
    cs (not b) "("++" \\forall "++latex_ False tv++"."++latex_ True t++cs (not b) ")"

  -- binary infix operators + % ->
  latex_ b (TypeBinary op t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeBinary op t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeBinary op t1 t2) t2 in
    cs lp "("++latex_ lp t1++cs lp ")"++latex op++
    cs rp "("++latex_ (rp||b) t2++cs rp ")"

  -- apps
  latex_ b (TypeApp t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeApp t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeApp t1 t2) t2 in
    cs lp "("++latex_ lp t1++cs lp ")"++" "++
    cs rp "("++latex_ (rp||b) t2++cs rp ")"

  -- base types
  latex_ _ (TypeVar tv) = latexVar tv

  -- ERROR
  latex_ _ _ = error "UnkindedType latex_: no rule applies."

instance LaTeX Type where
  latex_ b (t ::^ Nothing) = latex_ b t
  latex_ b (TypeVar v ::^ Just k) = latex_ b (TypeVar v)++"^{"++latex k++"}"
  latex_ b (t ::^ Just k) = "("++latex_ True t++")^{"++latex k++"}"



1.4  Die Verarbeitung der Bäume

-- Implementing funtions for lambda terms with types
-- $Id: ProcessCPFw.hs,v 1.18 2002/05/07 20:09:44 markus Exp $

module ProcessCPFw where
import CPFwDatatypes(Exp(..), Type(..), UntypedExp(..), UnkindedType(..),
                     Kind(..), Binary(..), LR(..), ty, jty, con, kd, jkd)

import List(union, unionBy, intersect, (\\), elemIndex, delete, nubBy, nub,
            find)
import Maybe(mapMaybe, fromJust, isNothing, isJust, maybeToList,
             catMaybes, fromMaybe)
import Char(isDigit)
import Monad(liftM2, mplus)

-- class Lambda with methods to ease the implementation of methods from the
-- lambda calculus theory

class Eq a=>Lambda a where
  -- a more uniform representation of trees with bound variables:
  -- a list of pairs of a bound variable (or Nothing if nothing is bound) and
  -- the term it is abstracted out
  destr :: a->[(Maybe a, a)]
  constr :: a->[(Maybe a, a)]->a
  errorvar :: String -> a
  sameType :: a->a->Bool
  rmType :: a->a
  freshenVar :: a->a
  isLambda :: a->Bool
  isApp :: a->Bool
  redEx :: a->Maybe a

  match :: [a] -> a -> a -> a
  annotateType :: [a] -> a -> a
  annotateInner :: [a] -> a -> a

-- comparing two types using alpha equality
infix 4 ==+
(==+) :: (Lambda a)=>a->a->Bool

a ==+ b = let l=alphaUnify (destr a) (destr b) 
              join (b1, l1) (b2, l2) = (b1&&b2, l1++l2)
              alphaUnify :: (Lambda a)=>[(Maybe a, a)] -> [(Maybe a, a)] -> (Bool, [(Maybe a, a)])
              alphaUnify [] [] = (True, [])
              alphaUnify ((Nothing, tl):rl) ((Nothing, tr):rr) =
                 join (tl ==+ tr, [(Nothing, tl)]) (alphaUnify rl rr)
              alphaUnify ((vl, tl):rl) ((vr, tr):rr) =
                 join (tl ==+ snd (alpha (vr, tr) (fromJust vl)), [(vl, tl)]) (alphaUnify rl rr)
              alphaUnify _ _ = (False, [])
          in fst l && constr a (snd l) == constr b (snd l)

instance Lambda Exp where

  destr (Var v ::: ty) =
    []
  destr (Abs (Var v ::: ty) tm ::: t) =
    [(Just (Var v ::: ty), tm)]
  destr (Inst e ty ::: t) =
    [(Nothing, e)]
  destr (Gen v e ::: t) =
    [(Nothing, e)]
  destr (App e1 e2 ::: t) =
    [(Nothing, e1), (Nothing, e2)]
  destr (Case e (Var v1 ::: ty1) t1 (Var v2 ::: ty2) t2 ::: t) =
    [(Nothing, e), (Just (Var v1 ::: ty1), t1), (Just (Var v2 ::: ty2), t2)]
  destr (InLR lr e ::: t) =
    [(Nothing, e)]
  destr (Pair e1 e2 ::: t) =
    [(Nothing, e1), (Nothing, e2)]
  destr (Lr lr e ::: t) =
    [(Nothing, e)]
  destr a = error ("destr: no rule applies to "++show a++".")

  constr (Var v ::: ty) [] = 
    (Var v ::: ty)
  constr (Abs _ _ ::: t) [(Just (Var v ::: ty), tm)] = 
    Abs (Var v ::: ty) tm ::: t
  constr (Inst _ ty ::: t) [(Nothing, e)]  = 
    Inst e ty ::: t
  constr (Gen v _ ::: t) [(Nothing, e)]  = 
    Gen v e ::: t
  constr (App _ _ ::: t) [(Nothing, e1), (Nothing, e2)]  = 
    App e1 e2 ::: t
  constr (Case _ _ _ _ _ ::: t)
         [(Nothing, e), (Just (Var v1 ::: ty1), t1), (Just (Var v2 ::: ty2), t2)]  = 
    Case e (Var v1 ::: ty1) t1 (Var v2 ::: ty2) t2 ::: t
  constr (InLR lr _ ::: t) [(Nothing, e)]  = 
    InLR lr e ::: t
  constr (Pair _ _ ::: t) [(Nothing, e1), (Nothing, e2)]  = 
    Pair e1 e2 ::: t
  constr (Lr lr _ ::: t) [(Nothing, e)]  = 
    Lr lr e ::: t
  constr a b = errorvar ("constr: no rule applies to wrap "++show a++" around "++
                         show b++".")

  errorvar s = Var s ::: Nothing

  freshenVar (Var v ::: typ) =
    let (n,r)=span isDigit (reverse v)
    in Var (reverse r++show (read ("0"++(reverse n)) + 1)) ::: typ 

  sameType e1 e2 = ty e1 == ty e2

  rmType (tm ::: _) = tm ::: Nothing

  isLambda (Abs _ _ ::: _) = True
  isLambda _ = False

  isApp (App _ _ ::: _) = True
  isApp _ = False

  redEx (App (Abs v t ::: atyp) t2 ::: typ) =
    Just (subst [(v, t2)] t)
  redEx (Case (InLR lr r ::: intyp) vl tl vr tr ::: typ) =
    let lrf=if lr==L then fst else snd
    in Just (subst [(lrf (vl,vr), r)] (lrf (tl, tr)))
  redEx (Lr lr (Pair t1 t2 ::: ptyp) ::: typ) =
    Just (if lr==L then t1 else t2)
  redEx _ = Nothing

  match env (e1 ::: Nothing) (e2 ::: t2) =
    (e2 ::: fmap (annotateFull_ (freetv env)) t2)
  match env (e1 ::: t1) (e2 ::: t2) | matchingT (betaReduction $ fromJust t1)
                                            (betaReduction $ fromJust t2) =
    (e2 ::: fmap (annotateFull_ (freetv env).betaReduction) t2)
  match _ (e1 ::: t1) (e2 ::: t2) =
    errorvar ("Can not match "++show (e1 ::: fmap betaReduction t1)++
              " with "++show (e2 ::: fmap betaReduction t2)++".")
  
  annotateInner env (Inst e t ::: typ) =
    case jty e of
      Forall v r ::^ Just KindProp ->
        match env (Inst e t ::: typ)
              (Inst e t ::: Just (subst [(v,t)] r))
      _ -> errorvar ("Can not INST a type "++show t++" without a & "++
                     "at the front of "++show (jty e)++".") 
  annotateInner env (Abs v e ::: typ) =
    match env (Abs v e ::: typ)
          (Abs v e ::: Just (TypeBinary Function
                                        (typeToProp (jty v))
                                        (typeToProp (jty e))
                               ::^ Just KindProp))
  annotateInner env (Gen t e ::: typ) =
    case ty e of
      Nothing -> errorvar ("Untyped term in Lambda (/\\): "++show e++".")
      Just tye -> match env (Gen t e ::: typ)
                            (Gen t e ::: Just (Forall t (typeToProp tye)
                                                 ::^ Just KindProp))  
  annotateInner env (App e1 e2 ::: typ) =
    case jty e1 of
      TypeBinary Function v t ::^ k ->
        if v==jty e2 then match env (App e1 e2 ::: typ)
                                (App e1 e2 ::: Just t)
                     else errorvar ("Cannot apply "++show e1++" $ "++show e2++
                                    ". Type mismatch.")
      _ -> errorvar ("Cannot apply "++show e1++" $ "++show e2++". No APP type.")
  annotateInner env (Lr lr e ::: typ) = 
    case jty e of
      TypeBinary Prod tl tr ::^ Just KindProp ->
        match env (Lr lr e ::: typ)
              (Lr lr e ::: Just (case lr of L -> tl; R -> tr)) 
      t -> errorvar ("Can not LR a type "++show t++" which is not a product.") 
  annotateInner env (Pair e1 e2 ::: typ) =
    match env (Pair e1 e2 ::: typ)
          (Pair e1 e2 ::: Just (TypeBinary Prod (jty e1)
                                                (jty e2)
                                  ::^ Just KindProp))
  annotateInner env (Case ei v1 e1 v2 e2 ::: typ) =
    case jty ei of
      TypeBinary Sum tl tr ::^ k ->
        if k /= Just KindProp then errorvar "Case disjunction not of type *." else
        if tl /= jty v1 then errorvar "Case type mismatch in left argument." else
        if tr /= jty v2 then errorvar "Case type mismatch in right argument." else
        if ty e1 /= ty e2 then errorvar "Case type mismatch in fuction arguments." else
          match env (Case ei v1 e1 v2 e2 ::: typ) (Case ei v1 e1 v2 e2 ::: ty e1)
      t -> errorvar ("Can not Case an expression with a type "++show t++
                     " which is not a sum.")
  annotateInner env (InLR lr e ::: typ) = 
    case typ of
      Nothing -> errorvar ("Can not type a InLR "++show (InLR lr e ::: typ)++
                           " without annotation.")
      Just (TypeBinary Sum lt rt ::^ k) ->
        match env (InLR lr e ::: typ)
              (InLR lr e ::: Just (case lr of L -> TypeBinary Sum (jty e) rt
                                              R -> TypeBinary Sum lt (jty e)
                                     ::^ toProp k))
      Just t -> errorvar ("Type "++show t++"doesn't match InLR "++
                          show (InLR lr e ::: typ)++".")

  annotateInner env e = errorvar("annotateInner: Can not annotate "++
                                 show e++" under env "++show env++".")

  annotateType env (e ::: Just t) =
    e ::: Just (annotateFull_ (freetv env) t) -- annotate variable binders
  annotateType env te =
    errorvar ("annotateType(Exp): cannot annotate empty type in: "++
              show te++".")

instance Lambda Type where

  destr (TypeVar v ::^ ty) =
    []
  destr (TypeLambda (TypeVar v ::^ ty) tm ::^ t) =
    [(Just (TypeVar v ::^ ty), tm)]
  destr (Forall (TypeVar v ::^ ty) tm ::^ t) =
    [(Just (TypeVar v ::^ ty), tm)]
  destr (TypeApp e1 e2 ::^ t) =
    [(Nothing, e1), (Nothing, e2)]
  destr (TypeBinary _ e1 e2 ::^ t) =
    [(Nothing, e1), (Nothing, e2)]
  destr a = error ("destr: no rule applies to "++show a++".")

  constr (TypeVar v ::^ ty) [] = 
    TypeVar v ::^ ty
  constr (TypeLambda _ _ ::^ t) [(Just (TypeVar v ::^ ty), tm)] = 
    TypeLambda (TypeVar v ::^ ty) tm ::^ t
  constr (Forall _ _ ::^ t) [(Just (TypeVar v ::^ ty), tm)] = 
    Forall (TypeVar v ::^ ty) tm ::^ t
  constr (TypeApp _ _ ::^ t) [(Nothing, e1), (Nothing, e2)]  = 
    TypeApp e1 e2 ::^ t
  constr (TypeBinary k _ _ ::^ t) [(Nothing, e1), (Nothing, e2)]  = 
    TypeBinary k e1 e2 ::^ t
  constr a b = errorvar ("constr: no rule applies to wrap "++show a++" around "++
                         show b++".")

  errorvar s = TypeVar s ::^ Nothing

  freshenVar (TypeVar v ::^ k) =
    let (n,r)=span isDigit (reverse v)
    in TypeVar (reverse r++show (read ("0"++(reverse n)) + 1)) ::^ k 

  sameType e1 e2 = kd e1 == kd e2

  rmType (tm ::^ _) = tm ::^ Nothing

  isLambda (TypeLambda _ _ ::^ _) = True
  isLambda _ = False

  isApp (TypeApp _ _ ::^ _) = True
  isApp _ = False

  redEx (TypeApp (TypeLambda v t ::^ ak) t2 ::^ tk) =
    Just (subst [(v, t2)] t)
  redEx _ = Nothing

  match _ (e1 ::^ Nothing) (e2 ::^ Nothing) =
    errorvar ("Can not match "++show e1++" with "++show e2++
              " having both no kinds.")
  match _ (e1 ::^ Nothing) (e2 ::^ t2) = (e2 ::^ t2)
  match _ (e1 ::^ t1) (e2 ::^ t2) | t1 == t2 = (e2 ::^ t2)
  match _ e1 e2 =
    errorvar ("Can not match "++show e1++" with "++show e2++".")
 
  annotateInner env (TypeBinary q lt rt ::^ k) =
    match env (TypeBinary q lt rt ::^ k)
          (TypeBinary q (typeToProp lt) (typeToProp rt) ::^ toProp k)
  annotateInner env (Forall v t ::^ k) =
    match env (Forall v t ::^ k)
          (Forall v (typeToProp t) ::^ toProp k)
  annotateInner env (TypeLambda v t ::^ k) =
    match env (TypeLambda v t ::^ k)
          (TypeLambda v t ::^ Just (KindAbs (jkd v) (jkd t)))
  annotateInner env (TypeApp t1 t2 ::^ k) =
    case jkd t1 of
      KindAbs k1 k2 | k1 == jkd t2 -> 
        match env (TypeApp t1 t2 ::^ k)
              (TypeApp t1 t2 ::^ Just k2)
      kw -> errorvar ("Kind mismatch TypeApp: "++show kw++" $ "++
                      show (jkd t2)++".")

  annotateInner env t = errorvar ("annotateInner: no rule applies. "++show t++".")

  annotateType tenv t = annotateFull_ [] t -- used for variable binders

matchingT (e1 ::^ Nothing) (e2 ::^ t2) = True
matchingT (e1 ::^ t1) (e2 ::^ t2) =
  t1 == t2 {- && all (\(a,b)->matchingT a b)  (zip  ((map snd (destr e1)))
                                                 (map snd (destr e2))) -}

freetv [] = []
freetv (e:es) = freevar (jty e)++freetv es

isVar :: Lambda a => a->Bool
isVar = null . destr

isBinder t = (do (b,_)<-destr t; maybeToList b) /= []

var :: Lambda a=>a->[a]
var e =
  if isVar e then [e]
             else nubBy sameName (do (b,t)<-destr e 
                                     unionBy sameName (maybeToList b) (var t))

freevar :: Lambda a=>a->[a]
freevar e =
  if isVar e then [e]
             else nubBy sameName
                        (do (b,t)<-destr e
                            (filter (\v->Just (rmType v) /= fmap rmType b)
                                    (freevar t)))

boundvar :: Lambda a=>a->[a]
boundvar e = nubBy sameName  (do (b,t)<-destr e 
                                 unionBy sameName (maybeToList b) (boundvar t))

-- subterms

directSubterms :: Lambda a=>a->[a]
directSubterms exp = map snd $ destr exp

subterms :: Lambda a=>a->[a]
subterms exp = subterms_ [exp] where 
                 subterms_ [] =[]
                 subterms_ (t:ts) = t:subterms_ (directSubterms t++ts)

-- no capture avoidance
capsubst :: Lambda a=>[(a, a)]->a->a
capsubst s e | isVar e = case e `lookup` s of Nothing -> e
                                              Just v -> v
capsubst s e = constr e (do (b,t)<-destr e 
                            let n=case b of Just v -> (filter ((v==).fst) s)
                                            Nothing -> s
                            [(b, capsubst s t)])

-- change names of bound variables
alpha :: Lambda a => (Maybe a, a) -> a -> (Maybe a, a)
alpha (Just vold, t) vnew 
  | not (sameType vold vnew) = error ("alpha subsitutes only "++
                                      "variables of the same type.")
  | not (isVar vnew) = error ("alpha needs a new variable as "++
                              "second argument.")
  | vnew `elem` freevar t\\[vold] = error "alpha name clash."
  | True = (Just vnew, capsubst [(vold, vnew)] t)
alpha _ _ = error ("alpha: needs a Just binder pair as "++
                   "first and a new variable as second argument.")

subst :: Lambda a => [(a, a)] -> a -> a -- [(variable, term to insert)], target ->result
                                        -- parallel substitution of variables

subst s t | isVar t = fromMaybe t (t `lookup` s)
subst s t =
  constr t (do (mv, tm)<-destr t
               case mv of Nothing -> [(Nothing, subst s tm)]
                          Just v -> if (freevar t `intersect` map fst s) /= []
                                       -- no substitution, no capture
                                       && (v `elem` (do (sv,st)<-s; sv:freevar st))
                                       -- capture danger
                                    then -- rename
                                      let fv=freshenVar v
                                          asub=alpha (mv, tm) fv
                                      in destr (subst s (constr t [asub]))
                                    else [(mv, subst s tm)]

           )

-- betaReduce :: Lambda a => a -> Maybe a

betaReduce t | isApp t && (isLambda (snd (destr t !! 0))) = 
  let arg=snd (destr t !! 1)
      [(Just var, fct)]=destr (snd (destr t !! 0))
  in (Just (subst [(var, arg)] fct))

-- betaReduce t = error ("BLOCK error: "++show t)

betaReduce t | isVar t = Nothing

betaReduce t =  fmap (constr t) (leftmost (destr t)) where
--  leftmost :: Lambda a => [(Maybe a, a)]->Maybe [(Maybe a, a)]
  leftmost [] = Nothing 
  leftmost (p:ps) = case betaReduce (snd p) of
    Nothing -> fmap (p:) (leftmost ps)
    Just nt -> Just ((fst p, nt):ps)


-- reduce using all reduction rules avaliable in the calculus of "Lambda"
-- this is governed by the redEx Lambda class method

fullReduce :: Lambda a => a -> Maybe a
fullReduce t | isJust (redEx t) = redEx t
fullReduce t = fmap (constr t) (leftmost (destr t)) where
  leftmost [] = Nothing 
  leftmost (p:ps) =
    case fullReduce (snd p) of
      Nothing -> fmap (p:) (leftmost ps)
      Just nt -> Just ((fst p, nt):ps)

-- reduce until no reduction applies or term stops changing
reduction :: Lambda a => (a->Maybe a)->a->a 
reduction r t =
  case r t of Nothing -> t 
              Just nt -> if t==nt then t
                                  else reduction r nt 

betaReduction :: Lambda a => a -> a
betaReduction = reduction betaReduce

fullReduction :: Lambda a => a -> a
fullReduction = reduction fullReduce

-- a history of recorded reductions

historyReduction r t =
  case r t of Nothing -> [] 
              Just nt -> if t==nt then []
                                  else nt:historyReduction r nt 

historyBetaReduction t = t:historyReduction betaReduce t

historyFullReduction t = t:historyReduction fullReduce t

-- helper

noType t = sameType t (rmType t)
sameName v1 v2 = rmType v1 == rmType v2
addVar v l = if noType v then [errorvar ("Cannot add untyped variable "++show v++
                                         " to "++show l++".")]
                         else nubBy sameName (v:l)

freetypevarInEnv env =
  nub (do _ ::: t<-env
          case t of 
            Nothing -> [errorvar ("freetypevarInEnv: "++
                                  show env++" contains untyped elements.")]
            Just typ -> let fv=freevar (con typ ::^ toProp (kd typ)) in
                        if any noType fv
                          then [errorvar ("freetypevarInEnv: "++show env++
                                          " contains unkinded type variables.")]
                          else fv
      )

toProp Nothing = Just KindProp
toProp (Just KindProp) = Just KindProp
toProp k = error ("toProp: Can not convert kind "++show k++" to kind Prop.")

rmProp Nothing = Nothing
rmProp (Just KindProp) = Nothing
rmProp k = error ("rmProp: Kind "++show k++" is no Prop.")

typeToProp (t ::^ k) = t ::^ toProp k

-- strips

strip t | isVar t = rmType t
strip t = rmType ((constr t) (do (v,st)<-destr t
                                 [(fmap rmType v, strip st)]))

stripChurch t = stripChurch_ [] t

stripChurch_ env t | isVar t =
  if t `elem` env then rmType t
                  else t -- stripType t
stripChurch_ env t = 
    rmType ((constr t)
      (do (v, st)<-destr t  
          case v of
            Just var -> [(Just (stripChurch_ [] var),
                         stripChurch_ (addVar var env) st)]
            Nothing -> [(v, stripChurch_ env st)])
    )

-- annotate

-- annotateFull annotates all inner nodes on a tree with annotated leafes
-- using a bottom up algorithm
annotateFull :: (Lambda a, Show a) => a -> a
annotateFull t = annotateFull_ (freevar t) t

annotateFull_ :: (Lambda a, Show a) => [a] -> a -> a
annotateFull_ env t | any noType env =
  errorvar ("annotateFull_: all variables in environment "++
            show env++" have to be typed. Problem:"++
            show (filter noType env)++".")
annotateFull_ env t | isVar t && noType t =
  case t `lookup` (zip (map rmType env) env) of
    Nothing -> errorvar ("annotateFull_: (here) free variable "++show t++
                         " not found in environment: "++show env++".")
    Just v -> v
annotateFull_ env t | isVar t =
  case find (sameName t) env of
    Nothing -> if rmType t == t
                 then errorvar ("annotateFull_: free variables must"++
                                "be annotated. Env: "++show env++
                                " Var: "++show t++".")
                 else t
    Just envvar -> if rmType t == t || envvar == t
                     then envvar
                     else errorvar ("annotateFull_: inner variable "++
                                    "not correctly annotated. EnvVar: "++
                                    show envvar++" Var: "++show t++".")

annotateFull_ env t =
  annotateInner env (constr t
    (do (v,st)<-destr t
        case v of
          Nothing -> [(v, annotateFull_ env st)]
          Just var -> if (noType var)
                         then [(Nothing,
                                errorvar ("annotateFull_: need annotated "++
                                          "abstracted variables. Problem"++show v++
                                          " in "++show t++"."))]
                         else let varan = annotateType env var in
                              [(Just varan,
                                annotateFull_ (addVar varan env) st)]
    ))

annotateChurch :: (Lambda a, Show a)=>a -> a
annotateChurch = stripChurch . annotateFull

-- general type checking function

createType :: Exp -> [Type] -> Type
createType (Abs v _ ::: _) [t] =
  TypeBinary Function (jty v) t ::^ Just KindProp
createType (Inst _ t ::: _) [Forall v r ::^ Just KindProp] =
  betaReduction $ subst [(v,t)] r
createType (Gen v e ::: _) [t] =
  if v `elem` (freetv (freevar e))
    then errorvar ("\nERROR: Illegal Generalisation. TVar:"++
                   show v++" free in "++show e++".\n"++
                   "freevar e: "++show (freevar e)++"\n"++
                   "freetv (freevar e): "++show(freetv (freevar e))++"\n---\n")
    else Forall v t ::^ Just KindProp
createType (App _ _ ::: _) [TypeBinary Function t1 t2  ::^ Just KindProp, t3] =
  t2 -- t1 == t3 not checked
createType (Var _ ::: t) [] =
  fromJust t
createType (Case c vl el vr er ::: t) [tc,tel,ter] =
  ter -- not checked:
      -- con (jty c) == TypeBinary Sum (jty vl) (jty vr) &&
      -- jty el == jty er
createType (InLR lr _ ::: Just (TypeBinary Sum tl tr  ::^ Just KindProp)) [te] =
  case lr of L-> TypeBinary Sum te tr  ::^ Just KindProp
             R-> TypeBinary Sum tl te  ::^ Just KindProp
createType (Pair e1 e2 ::: t) [t1,t2] =
  TypeBinary Prod t1 t2 ::^ Just KindProp
createType (Lr lr _ ::: t) [TypeBinary Prod tl tr ::^ Just KindProp] =
  case lr of L->tl; R->tr
createType e ts = errorvar ("ERROR: Can not create type. No rule applies for "++
                            show (e, ts)) -- ERROR

checkType exp = map checkType_ (subterms exp)

checkType_ e = matchType e (jty e) ((createType e) (map jty (directSubterms e)))

matchType e t1 t2 = (e, t1, t2, t1 ==+ t2)

-- check whether a Church term is completely and correctly annotated

checkChurch :: Exp -> Maybe String -- Nothing means OK, Just Error

checkChurch (Abs e1 e2 ::: t) =
  checkChurch e1 `mplus` checkChurch e2 `mplus`   
    if (TypeBinary Function (jty e1) (jty e2) == con (fromJust t))
      then Just ("Abs mismatch:"++show (jty e1)++"->"++
                 show(jty e2)++"!="++show (con (fromJust t))++".")
      else Nothing
checkChurch (Inst e t ::: ot) =
  checkChurch e  `mplus` 
    case jty e of
    Forall v r ::^ Just KindProp ->
      if Just (betaReduction $ subst [(v,t)] r) == ot
        then Nothing
        else Just "INST type mismatch"
    n ->
      Just ("Can't INST a type "++show n++
            "which is not a Forall.")
checkChurch (Gen v e ::: t) = 
  checkChurch e `mplus`
  if con (fromJust t) == Forall v (jty e)
    then Nothing
    else Just "Gen fail."
checkChurch (App e1 e2 ::: t) =
  checkChurch e1 `mplus` checkChurch e2 `mplus`
  if (TypeBinary Function (jty e2) (fromJust t) == con (jty e1))
    then Nothing
    else Just "App fail."
checkChurch (Var s ::: t) = Nothing -- use an environment?
checkChurch (Case c vl el vr er ::: t) = 
  checkChurch c `mplus` checkChurch vl `mplus` checkChurch el
  `mplus`  checkChurch vr `mplus`  checkChurch er `mplus` 
  if con (jty c) == TypeBinary Sum (jty vl) (jty vr) &&
     jty el == jty er && jty er == fromJust t
  then Nothing
  else Just "Case fail."
checkChurch (InLR lr e ::: t) =
  checkChurch e `mplus`  
  case con (fromJust t) of
    TypeBinary Sum tl tr ->
      if (case lr of L->tl; R->tr) == jty e
        then Nothing
        else Just "InLR fail."
    n -> Just ("Type of InLR has to be a Sum.")
checkChurch (Pair e1 e2 ::: t) =
  checkChurch e1 `mplus` checkChurch e2 `mplus`  
  if TypeBinary Prod (jty e1) (jty e2) == con (fromJust t) 
    then Nothing
    else Just "Pair fail."
checkChurch (Lr lr e ::: t) =
  checkChurch e `mplus` 
  case con (jty e) of
    TypeBinary Prod tl tr ->
      if (case lr of L->tl; R->tr) == fromJust t
        then Nothing
        else Just "LR fail."
    n -> Just ("LR application needs a Prod type:"++show n++".")


1.5  Die Beispiele

-- Examples to test the type checker
-- $Id: Examples.hs,v 1.21 2002/05/07 21:26:29 markus Exp $

module Examples where

import CPFwDatatypes(Exp(..), Type(..), UntypedExp(..), UnkindedType(..),
                     Kind(..))
import ParseCPFw(parse)

import ProcessCPFw 

--import PrintExplicit(Explicit(..))
import PrintLaTeX(LaTeX(..))

import Maybe(fromMaybe)

-- adapted show for lists

brshow :: Show a => [a] -> String
brshow [] = "[]"
brshow (e:es) = "["++foldl (\s e->s++",\n "++show e) (show e) es++"\n]"

-- combinators s,k,i from combinator logic
s = parse("\\x.\\y.\\z.(x z)(y z)")
k = parse("\\x.\\y.x")
i = parse("\\x.x")

skk = (((s `App` k) ::: Nothing) 
           `App` k) ::: Nothing

-- Church numerals
church :: Int->Exp
church n = parse("\\f.\\x."++church_ n)
church_ :: Int->String
church_ 0 = "x"
church_ n = "f("++church_ (n-1)++")"

tchurch n = parse("(\\f:(A^*->A^*)^*.\\x:A^*."++tchurch_ n
                        ++"):((A^*->A^*)^*->(A^*->A^*)^*)^*")
tchurch_ :: Int->String
tchurch_ 0 = "(x:A^*)"
tchurch_ n = "((f:(A^*->A^*)^*)"++tchurch_ (n-1)++":A^*)"

-- Urzyczyn's 2-chains
urzy n = ((urzy_ n) `App` k) ::: Nothing
urzy_ 0 = church 2
urzy_ n = ((urzy_ (n-1)) `App` (church 2)) ::: Nothing

-- Urzyczyn's 22K p. 338

typedtwotwok="("++show (church 2)++")("++show (church 2)++
  ":&B.(&A.A->(B A))->(&A.A->(B(B A)))"++")("++show k++")"

tyttk = parse typedtwotwok

typedtwotwotwok= "("++show (church 2)++")("++show (church 2)++
  ":&C.(&B.(&A.A->B A)->(&A.A->C B A))->"++
  "(&B.(&A.A->(B A))->(&A.A->(C (C B) A)))"++
  ")("++show (church 2)++")("++show k++")"

tytttk = parse typedtwotwotwok

churchttk = "(\\f:&B^*=>*.(&A^*.A^*->B A^*)->&A^*.A^*->B (B A^*)."++
            "\\x:&A^*.A^*->B^*=>* A^*.((f B^*=>*) x))" {- ++
            "(\\f:A^*->B^*=>* A^*.\\x:A^*.f (f x)"++
            ":&B^*=>*.(&A^*.A^*->B A^*)->&A^*.A^*->B (B A^*)) \\x.\\y.x" -}

typed22k = parse churchttk

-- test my betareduction "be id!"
beid = betaReduction skk

-- type tests

typeds = parse ("(\\x:X^*.(\\y:Y^*.(\\z:Z^*."
                     ++"((x:X^*) (z:Z^*))"
                     ++"(y z))))"
                     ++":((X^*->Y^*)^*->Z^*)^*")
typedk = parse "(\\x:X^*.\\y:Y^*.x):(X->Y->X)^*"
typedi = parse "\\x:X^*.(x:X^*):(X^*->X^*)^*"
typedx = parse "x:X^*"

-- crap

-- t = ((i `App` k) ::: Nothing)
kk = (k `App` k) ::: Nothing
app = parse("x y")
x = parse("x")
y = parse("y")
abstr = parse("\\x.y")
cti = parse("/\\A^*.\\x:A.x") -- kinding of Lambda vars is not sufficient

ts="\\x:Z^*->Y^*->X^*.\\y:Z^*->Y^*.\\z:Z^*.(x z)(y z)"
tk="\\x:Xk^*.\\y:Yk^*.x"
tskk=parse("("++ts++")"++" ("++tk++") "++tk)

tsk=parse("(/\\Z^*./\\Y^*./\\X^*."++ts++
          ") Xk^* Yk^* Xk^*"++" ("++tk++")") -- ++tk)

-- check annotation in abstraction expressions

aexp = parse "\\x:A^*->A^*.x"

-- illegal generalisation 

wrongfa = parse "/\\ A^*. (x:A^*)"

-- Matthes

moniso = "(\\F.&Am.&A.(Am->A) -> F Am -> F A)"
monisoan = "(\\F^*=>*.&Am^*.&A^*.(Am->A) -> F Am -> F A)"

monanti = "(\\F.&Am.&A.(Am->A) -> F A -> F Am)"
monantian = "(\\F^*=>*.&Am^*.&A^*.(Am->A) -> F A -> F Am)"

--mi = parse ("x:"++moniso)
--ma = parse ("x:"++monanti)

-- 1.2

prmi = moniso++"\\A.B"
prmian = monisoan++"\\A^*.B^*"

prma = monanti++"\\A.B"
prmaan = monantian++"\\A^*.B^*"

proofproj = parse "/\\ B^*. /\\ Am^*. /\\ A^*. \\ f:Am^*->A^*. \\ x:B^*. x"

-- 1.3
idmi = moniso++"\\A.A"
idmian = monisoan++"\\A^*.A"

proofidmi = parse ("/\\Am./\\A.\\f:Am->A.\\x:Am^*.f x"++":"++idmi)
proofidmian = parse ("/\\Am^*./\\A^*.\\f:(Am->A)^*.\\x:Am^*.f x"++
                     ":"++idmian)
proofidmian2 = parse ("/\\Am^*./\\A^*.\\f:(Am^*->A^*)^*.\\x:Am^*.f x"++
                     ":"++idmian)

-- 1.4
{-
proofsumpresisotone =  parse $ "/\\F./\\G."++
                     "\\x:"++monisoan++"F."++
                     "\\y:"++monisoan++"G."++
                     "/\\Am./\\A."++
                     "\\f:Am->A."++
                     "\\z:F Am % G Am."++
                     "z{x1:F Am.INL(x Am A f x1): G A + F A, "++
                     "  y1:G Am.INL(y Am A f y1): G A + F A}"++
                     ":&F.&G.("++monisoan++"F)->"++
                     "("++monisoan++"G)->(\\A.F A + G A)"

proofprodpresisotone = parse $ "/\\F^*=>*./\\G^*=>*."++
                     "\\x:"++monisoan++"F^*=>*."++
                     "\\y:"++monisoan++"G^*=>*."++
                     "/\\Am^*./\\A^*."++
                     "\\f:Am^*->A^*."++
                     "\\z:F^*=>* Am^* % G^*=>* Am^*."++
                     "<x, y>"++ -- "<x Am^* A^* f (z L), y Am^* A^* f (z R)>"++
                     ":&F^*=>*.&G^*=>*.("++monisoan++"F^*=>*)->"++
                     "("++monisoan++"G^*=>*)->(\\A^*.F A % G A)"
proofprodpresisotone2 = parse $
                     "/\\F^*./\\G^*."++
                     "\\x:"++monisoan++"F^*=>*.x " --  ++
                     "\\y:"++monisoan++"G."++
                     "/\\Am./\\A."++
                     "\\f:Am->A."++
                     "\\z:F Am % G Am."++
                     "<x Am A f (z L), y Am A f (z R)>"  ++
                     ":&F.&G.("++monisoan++"F)->"++
                     "("++monisoan++"G)->(\\A.F A % G A)"
-}

-- 1.5

-- 1.6

-- 1.7

-- 1.8

-- mail

proofpair = parse "\\ x:A^*.<x,x>"
prooffapair = parse "/\\ A^*. \\ x:A^*.<x,x>"

proofsum = parse "\\ x:A^*.(INL x:A+B^*)"
prooffasum = parse "/\\ A^*. \\ x:A^*.(INL x:A+B^*)"

proofsumiso = parse $ "(/\\ A^*. /\\ B^*. \\ f:A^*->B^*. \\ c:A^*+A^*. "++
                      "(INL (c{cl:A^*.f cl:B^*, cr:A^*.f cr:B^*}):B^*+B^*)"++
                      "):("++monisoan++")\\X^*.X + X"
proofprodiso = parse $
  "/\\ A^*. /\\ B^*. \\ f:A^*->B^*. \\ p:A^*%A^*. <f(p L),f(p R)>"++
  ":("++monisoan++")\\X^*.X % X"

1.6  Das Makefile

GHC=ghc
HUGS=hugs
HAPPY=/usr/src/happy-1.10/happy/src/happy.sh
RM=rm
PERL=perl
MAKE=make

DEBUG=
GHC_OPTS=-package lang -package net

TEXS=KS.tex HistorySKK.tex ChurchNumerals.tex UrzyChains.tex \
     MonotonicityWitnesses.tex Tabular.tex SimplePair.tex \
     ProofProjIsIsotone.tex ProofSumIsIsotone.tex \
     ProofPairingIsIsotone.tex ProofIdentityIsIsotone.tex \
     WrongForall.tex TypedSK.tex Proof22KIsTypable.tex \
     ProofProdPresIsotone.tex ProofSumPresIsotone.tex

MAINS=Parser CPFwCGI

.PHONY: all
all: ${TEXS} ${MAINS}

.PHONY: ${MAINS} ${basename ${TEXS}}
${MAINS} ${basename ${TEXS}}: %: %.hs
	EXIT=(1 1); \
	until test "$${EXIT[1]}" == "0"; do \
	  ${GHC} ${GHC_OPTS} --make $< -o $@ 2>&1 \
	  | ${PERL} -p \
	            -e 'BEGIN {$$remade=0;}' \
	            -e "if (/(can't find module )\`(.*)'$$/ || " \
	            -e '    /^(Skipping  |Compiling ).*\( (.*)\.hs\, .* \)$$/ )' \
                    -e '  {if (system "${MAKE} -q $$2.hs")' \
                    -e '    {if (!system "${MAKE} $$2.hs") {$$remade=1}}}' \
	            -e 'END {exit $$remade;}'; \
	  EXIT=($${PIPESTATUS[*]}); \
	done; \
	exit $${EXIT[0]}

%.hs: %.y
	${HAPPY} -a ${DEBUG} $< -o $@

%.info: %.y
	${HAPPY} -a -i $< 

${TEXS}: %.tex: %
	./$< > $@

.PHONY: tar
tar:
	cvs checkout -d /tmp/fopra/ fopra
	WD=$$(pwd); cd /tmp/; tar -cvjf $$WD/fopra.tar.bz2 fopra/
	rm -fr /tmp/fopra

.PHONY: GHCVersion.tex
GHCVersion.tex:
	( echo "{\tt " ; ${GHC} --version ; echo " }" ) > $@

.PHONY: HugsVersion.tex
HugsVersion.tex:
	( echo "{\tt " ; \
	  (echo ":version" | ${HUGS} 2>/dev/null | perl -n \
	       -e 'if (/^Prelude> -- (Hugs Version .+)$$/) {print $$1 }'); \
	  echo " }" ) > $@

.PHONY: clean
clean:
	${RM} -f *.o
	${RM} -f *.hi
	${RM} -f ParseCPFw.hs
	${RM} -f ParseCPFw.info
	${RM} -f ${TEXS}
	${RM} -f ${basename ${TEXS}}
	${RM} -f ${MAINS}
	${RM} -f GHCVersion.tex
	${RM} -f HugsVersion.tex
	${RM} -f fopra.tar.bz2


Footnotes:

1Simon Peyton Jones auf der Glasgow-Haskell-Bugs-Mailinglist
http://haskell.cs.yale.edu/pipermail/glasgow-haskell-bugs/2001-April/001394.html
2in [], S.338 Conjecture 2.3
3nach Ralph Matthes' []
4Stichwort ,,Ponder" im FOLDOC []


File translated from TEX by TTH, version 3.33.
On 22 Mar 2003, 22:38.