Ein Projekt von „Praxis der Softwareentwicklung“ (PSE)

Aktuell

Wichtige Termine

Termin	Datum	Ort
Erstes Treffen	16.11.2020, 10:00 Uhr	online (Zoom)
Einführung Typinferenz	18.11.2020, 10:00 Uhr	online (Zoom)

Visualisierung von Typinferenz

Worum geht es?

Der λ-Kalkül ist ein rein auf Termersetzung begründeter turingmächtiger Kalkül.
(Das bedeutet insbesondere, man kann darin Programme schreiben, die beliebige Dinge ausrechnen.)
Dieser Kalkül ist nicht nur von historischer Bedeutung, sondern bietet immer noch das theoretische Fundament für funktionale Programmiersprachen.
Der λ-Kalkül besitzt ein einfaches, aber mächtiges Typsystem. Dieses erlaubt auch Typinferenz: Für einen Term kann automatisiert der Typ dieses Terms berechnet werden, ohne dass der Benutzer Typen angeben muss.
Leider ist es erfahrungsgemäß schwierig, Studierenden den Typinferenz-Algorithmus klar zu machen. Das wollen wir ändern, und dazu sollt ihr nun ein Programm schreiben, das Leuten die Typinferenz näherbringt, indem es die Berechnungsschritte der Typinferenz in einem sogenannten Ableitungsbaum visualisiert.
Keine Angst, ihr seid da nicht auf euch allein gestellt, wir erklären euch das nötige Vorwissen (den Kalkül, wie die Typisierung funktioniert, den Typinferenz-Algorithmus, etc.).

Was muss das Programm können?

Da das Programm für die Lehre gedacht ist, muss es intuitiv zu bedienen sein.
Am besten wäre eine Webanwendung, da es nunmal sehr viel einfacher ist, Studierende dazu zu bringen, kurz einen Link im Browser anzuklicken, als eine Java-Applikation herunterzuladen.
(Jedoch gelten auch hier die üblichen Einschränkungen: Objektorientierter Entwurf, statisch typisierte Sprache!)
Das Programm muss in jedem Fall den Typinferenz-Algorithmus schrittweise durchführen können (mit Darstellung der Zwischenschritte), darüber hinaus sind wir offen für eure Ideen, wie man eine solche Entwicklungs-/Lernumgebung am besten gestaltet.
Hier eine Liste an Ideen, wie man dieses Grundgerüst erweitern könnte, um daraus eine sinnvolle Lernumgebung zu machen:

• Zusätzliche Informationen für die einzelnen Schritte (welche Regel wurde verwendet, etc.).
• Darstellen des finalen Typprüfungsbaums.
• Vordefinierte Konstanten
• Typinferenz-Beispiele mit Tutorial
• (Sofern als Webanwendung umgesetzt) Permalinks, die zu bereits "vorausgefüllten" Sessions führen
• LaTeX-Export

Bewertung

Die Benotung eures Systems richtet sich nach folgenden Kriterien:

• Qualität aller abgegebenen Dokumente und Artefakte

• Qualität der Kolloquien (10 Minuten Vortrag)

• Qualität der Abschlusspräsentation

• Erfüllung der minimalen Leistungsmerkmale (s.o.)

• sinnvolle Erweiterungen über diese Merkmale hinaus

• Robustheit des erstellten Programms

• Teamarbeit (TSE)

Diese Liste hat keine Reihenfolge, die einer Gewichtung entspricht. Es gibt sicherlich weitere Punkte, die als selbstverständlich gelten und sich bei Nichterfüllen negativ auswirken (z.B. ist die Geschwindigkeit der implementierten Algorithmen sekundär, aber jedem sollte klar sein, dass das Ausführen eines Algorithmus-Schritts nicht 10 Tage dauern darf).

Weitere Pflichten

• Anmeldung per Studienportal für PSE und TSE

• Anwesenheit bei den wöchentlichen Treffen mit dem Betreuer

• Team-internes Management (z.B. Phasenverantwortliche, Versionskontrolle)

• Artefakte 1–2 Tage vor Kolloquium beim Betreuer

Wöchentliche Treffen und Kolloquien

Die wöchentlichen Treffen werden virtuell stattfinden. Die Kolloquien werden voraussichtlich in Präsenz stattfinden.

Dokumente

Dokument	Datum
Tipps & Tricks	2020-10-20
Folien Projektvorstellung	2020-11-05
Folien Einführung Typinferenz	2020-11-18

Veranstalter

Wissenschaftliche Mitarbeiter
Dr. Jakob von Raumer

Ehemalige Mitarbeiter
M.Sc. Simon Bischof